Constrained Dynamic Parser: Difference between revisions

From Event-B
Jump to navigationJump to search
imported>Mathieu
mNo edit summary
imported>Mathieu
m Requirements, a bit of state of the art + some analysis
Line 45: Line 45:


=== Parser Combinator ===
=== Parser Combinator ===
:* on [http://en.wikipedia.org/wiki/Parser_combinator wikipedia]. Some implementations are referenced [here http://pdos.csail.mit.edu/~baford/packrat/].
:* with functionnal language Agda[http://wiki.portal.chalmers.se/agda/Agda] : ''[http://www.cs.nott.ac.uk/~nad/publications/danielsson-norell-mixfix.pdf Parsing Mixfix Operators]
:* with functionnal language Agda[http://wiki.portal.chalmers.se/agda/Agda] : ''[http://www.cs.nott.ac.uk/~nad/publications/danielsson-norell-mixfix.pdf Parsing Mixfix Operators]
:: Ce papier est intéressant de part son traitement de l'associativité et de la précédence des opérateurs basée sur un graphe de précédence acyclique.
:: This paper is interesting in its proposal of using an acyclic graph to define operator precedence.
:* avec le langage fonctionnel [http://user.cs.tu-berlin.de/~opal/opal-language.html OPAL] : ''[http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=8A8A8B39FFBF1AEF17C782C4822C5AF6?doi=10.1.1.58.655&rep=rep1&type=url&i=0 How To Obtain Powerful Parsers That Are Elegant and Practica]''
:* with functional language [http://user.cs.tu-berlin.de/~opal/opal-language.html OPAL] : ''[http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=8A8A8B39FFBF1AEF17C782C4822C5AF6?doi=10.1.1.58.655&rep=rep1&type=url&i=0 How To Obtain Powerful Parsers That Are Elegant and Practical]''


=== Pratt Parser ===
=== Pratt Parser ===
:* [http://portal.acm.org/citation.cfm?id=512931 le papier original de Vaughan Pratt] (dispo en [[:Image:P41-pratt.pdf|local]])
:* [http://portal.acm.org/citation.cfm?id=512931 original paper from Vaughan Pratt]
:* [http://effbot.org/zone/tdop-index.htm SImple ''Pratt'' parsing in python]
:* [http://effbot.org/zone/tdop-index.htm SImple ''Pratt'' parsing in python]
:* [http://javascript.crockford.com/tdop/tdop.html ''Pratt'' parsing in javascript]
:* [http://javascript.crockford.com/tdop/tdop.html ''Pratt'' parsing in javascript]

Revision as of 13:26, 30 January 2010

This page describes the requirements for a generic parser for the Event-B Mathematical Language. It will also draft a first design proposal.

Requirements

In order to be usable mathematical extensions require the event-b mathematical language syntax to be extendable by the final user.

Thus, the lexical analyser and the syntaxic parser have to be extendable in a simple enough way (from a user point of vue).

Requirements Exported by the Current Language Design

Operator Priority

  • operator are defined by group,
  • group of operator have a defined precedences,
  • there may be precedences defined inside groups.

Operator Associativity

  • a compatibility table defines allowed associativity inside a group,
  • a compatibility tables defines allowed associativity between groups (it allows to forbid a syntaxic construction like f(x)^{-1}\;
nota: this requirement was added afterwards with consistency in mind.

Expected Extension Schemes

We do want to at least define operators of the following form :

  • infix : a + b\; or a \vdash b : c\;
  • prefix : \neg a\;
  • postfix :  R^*\;
  • closed : \|a\|\;
  • parentheses sugar : (a +b) * c\;
  • functional postfix :  a \langle b \rangle\;
  • functional prefix :   \langle b \rangle f\;
  • lambda like :  \lambda x\mapsto y . P | E\;
  • Union like :  \Union\{ e \mid P\} or  \Union\{ x,y . P \mid e\}
  • sets : \{a, b, c + e\}\; or \{ e \mid P\}\; or \{x,y . P \mid e\}\;

We also like to define precisely precedences and associativity between existing and new operators.

Requirements exported by the dynamic feature

  • the precedence should not be enumerated but defined by a relation, like: '+' < '*' and '*' < '**', ...

Limitations

Design Alternatives

Make Existing Parser Extendable

The existing parser is a LL recursive descent parser generated by the Coco/R Compiler Generator, which makes extensive use of pre-computed lookahead, which makes it very difficult to be transformed in a sufficiently enough generic parser.

Parser Combinator

This paper is interesting in its proposal of using an acyclic graph to define operator precedence.

Pratt Parser

Some Existing Extendable Languages

Design Proposal