Constrained Dynamic Parser

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 '*' < '**', ...

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

• with functionnal language Agda[1] : 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 OPAL : How To Obtain Powerful Parsers That Are Elegant and Practica

Pratt Parser

• le papier original de Vaughan Pratt (dispo en local)
• SImple Pratt parsing in python
• Pratt parsing in javascript

Some Existing Extendable Languages

• Katahdin, and the associated paper A Programming Language Where the Syntax and Semantics Are Mutable at Runtime which describes the language and its implementation (in C#).
• XMF whose implementation seems not be describes in details.
• XLR: Extensible Language and Runtime, which looks like a pratt parser according to the sources.
• $\pi$ hose implementation seems not be describes in details (but sources availables).