Difference between revisions of "Constrained Dynamic Parser"

From Event-B
Jump to navigationJump to search
imported>Mathieu
m
imported>Mathieu
m
Line 1: Line 1:
{TOCright}}
+
{{TOCright}}
 
This page describes the requirements for a '''generic parser''' for the [[Event-B Mathematical Language]].
 
This page describes the requirements for a '''generic parser''' for the [[Event-B Mathematical Language]].
 
It will also draft a first design proposal.
 
It will also draft a first design proposal.
Line 8: Line 8:
 
Thus, the lexical analyser and the syntaxic parser have to be extendable in a simple enough way (from a user  point of vue).
 
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 ===
+
=== Requirements Exported by the Current Language Design ===
 
==== Operator Priority ====
 
==== Operator Priority ====
 
* operator are defined by group,
 
* operator are defined by group,
Line 18: Line 18:
 
* a compatibility tables defines allowed associativity between groups (it allows to forbid a syntaxic construction like <math>f(x)^{-1}\;</math>
 
* a compatibility tables defines allowed associativity between groups (it allows to forbid a syntaxic construction like <math>f(x)^{-1}\;</math>
 
: nota: this requirement was added afterwards with consistency in mind.
 
: 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 : <math>a + b\;</math> or <math>a \vdash b : c\;</math>
 +
* prefix : <math>\neg a\;</math>
 +
* postfix : <math> R^*\;</math>
 +
* closed : <math>\|a\|\;</math>
 +
* parentheses sugar : <math>(a +b) * c\;</math>
 +
* functional postfix : <math> a \langle b \rangle\;</math>
 +
* functional prefix : <math>  \langle b \rangle f\;</math>
 +
* lambda like : <math> \lambda x\mapsto y . P | E\;</math>
 +
* Union like : <math> \Union\{ e \mid P\}</math> or <math> \Union\{ x,y . P \mid e\}</math>
 +
* sets : <math>\{a, b, c + e\}\;</math> or <math>\{ e \mid P\}\;</math> or <math>\{x,y . P \mid e\}\;</math>
 +
 +
We also like to define precisely precedences and associativity between existing and new operators.
  
 
=== Requirements exported by the dynamic feature ===
 
=== Requirements exported by the dynamic feature ===
 +
* the precedence should not be enumerated but defined by a relation, like: '+' < '*' and '*' < '**', ...
  
 
== Limitations ==
 
== Limitations ==
  
 
== Design Alternatives ==
 
== Design Alternatives ==
 +
 +
=== Make Existing Parser Extendable ===
 +
The existing parser is a LL recursive descent parser generated by the [http://www.ssw.uni-linz.ac.at/Coco/ 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 ===
 +
:* 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.
 +
:* 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]''
 +
 +
=== Pratt Parser ===
 +
:* [http://portal.acm.org/citation.cfm?id=512931 le papier original de Vaughan Pratt] (dispo en [[:Image:P41-pratt.pdf|local]])
 +
:* [http://effbot.org/zone/tdop-index.htm SImple ''Pratt'' parsing in python]
 +
:* [http://javascript.crockford.com/tdop/tdop.html ''Pratt'' parsing in javascript]
 +
 +
=== Some Existing Extendable Languages ===
 +
* [http://www.chrisseaton.com/katahdin/ Katahdin], and the associated paper [http://www.chrisseaton.com/katahdin/katahdin-thesis.pdf A Programming Language Where the Syntax and Semantics Are Mutable at Runtime] which describes the language and its implementation (in C#).
 +
* [http://itcentre.tvu.ac.uk/~clark/xmf.html XMF] whose implementation seems not be describes in details.
 +
* [http://xlr.sourceforge.net/index.html XLR: Extensible Language and Runtime], which looks like a ''pratt'' parser according to the [http://xlr.svn.sourceforge.net/viewvc/xlr/trunk/xl2/xlr/parser.cpp?revision=805&view=markup sources].
 +
* [http://www.pi-programming.org/What.html <math>\pi</math>] hose implementation seems not be describes in details (but sources availables).
  
 
== Design Proposal ==
 
== Design Proposal ==

Revision as of 13:20, 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

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.

Pratt Parser

Some Existing Extendable Languages

Design Proposal