Expressions

Expressions are not parsed with a context free grammar ! So we will give partial BNF rules and explain ``infix'' and ``prefix'' expressions by hand.

Here are the BNF rules with infix-expr and prefix-expr left undefined.

sort-assignment	:=	:< sort
alpha-idents-list	:=	alpha-ident
	$\vert$	alpha-ident , alpha-idents-list
atom-expr	:=	alpha-ident
	$\vert$	$ any-ident
	$\vert$	unif-var
	$\vert$	\ alpha-idents-list sort-assignment atom-expr
	$\vert$	( expr )
	$\vert$	prefix-expr
app-expr	:=	atom-expr
	$\vert$	atom-expr app-expr
expr	:=	app-expr
	$\vert$	prefix-expr
	$\vert$	infix-expr

This definition is clear except for two points:

• The juxtaposition of expression if the definition of app-expr means function application !
• The keyword \ introduces abstraction: \x x for instance, is the identity function. \x (x x) is a strange function taking one argument and applying it to itself. In fact this second expression is syntaxically valid, but it will be rejected by because it does not admit a sort.

To explain how infix-expr and prefix-expr works, we first give the following definition:

A syntax definition is a list of items and a priority. The priority is a floating point number between 0 and 10. Each item in the list is either:

• An alpha-ident. These items are name for sub-expressions.
• A string containing an any-ident, using escape sequences if necessary. These kind of items are keywords.
• A token of the form \ alpha-ident \ where the alpha-ident is used somewhere else in the list as a sub-expression. These items are ``binders''.
• The list should obey the following restrictions (except for LaTeX syntax definition):
  • The first of the second item in the list should be a keyword. If the first item is a keyword, then the syntax definition is ``prefix'' otherwise it is ``infix''.
  • A name for a sub-expression can not be followed by another name for a sub-expression nor a binder.

Remark: this definition clearly follows the definition of a syntax.

Now we can explain how a syntax definition is parsed using the following principles. It is not very easy to understand, so we will give some examples:

1. The first keyword in the definition is the ``name'' of the object described by this syntax. This name can be used directly with ``normal'' syntax prefixed by a $ sign.

   For instance, if the first keyword is the string "+", then + is the name of the object and if this object is defined, $+ is a valid expression.

2. To define the way infix-expr and prefix-expr are parsed, we will explain how they are parsed and give the same expression without using this special syntax.

3. The number of sub-expressions in the list is the ``arity'' of the object defined by the syntax.

4. To parse a syntax defined by a list, examines each item in the list:
   • If it is the $i^{\hbox{th}}$ sub-expression in the list, then parses an expression and this expression is the $i^{\hbox{th}}$ argument $a_i$ of the object. At the end, if no binder is used, parsing an object whose name is N will be equivalent to parsing $N $a_1$ ...$a_n$.

   • If it is a keyword, then parses exactly that keyword.

   • If it is a binder \x\, where x is the name of the $i^{\hbox{th}}$ sub-expression, then the variable x may appear in the $i^{\hbox{th}}$, and this $i^{\hbox{th}}$ will be prefixed with \x. At the end, parsing an object whose name is N will be equivalent to parsing N (\ $x_1,\dots,x_n\;a_1$) ...(\ $y_1,\dots,y_p\;a_n$).

   • If the first and last item in the syntax definition are sub-expressions, the priority are important: parses expression at a given priority level, initially 10. If the priority of the syntax definition is strictly greater than the priority level, then this syntax definition can not be parsed.

     When parsing the first item, if it is a sub-expression, the priority level is changed to the priority level of the syntax definition (minus $\epsilon = 1e^{-10}$ if the symbol is not left associative). Left associative symbols are defined using the keyword lInfix of Postfix.

     When parsing the last item, if it is a sub-expression, the priority level is changed to the priority level of the syntax definition (minus $\epsilon = 1e^{-10}$ if the symbol is not right associative. Right associative symbols are defined using the keyword rInfix of Prefix.

     When parsing other items, the priority is set to 10.

Examples:

• The syntax lInfix[3] x "+" y is parsed by parsing a first expression $a_1$ at priority $3$, then parsing the keyword + and finally, parsing a second expression $a_2$ at priority $3 - \epsilon$.

  Therefore, parsing $a_1$ + $a_2$ is equivalent to $+ $a_1 a_2$ and parsing $a_1$ + $a_2$ + $a_3$ is equivalent to $+ ($+ $a_1 a_2$) $a_3$.

• The syntax Prefix "{" \P\ "in" y "|" P "}" is parsed by parsing the keyword {, an identifier $x$, the keyword "in", a fist expression $a_1$, the keyword |, a second expression $a_2$ that can use the variable $x$ and the keyword }.

  Therefore, parsing { $x$ in $a_1$ | $a_2$ } is equivalent to ${ $a_1$ \x $a_2$.

• Other examples can be found in the appendix A in the description of the commands Cst and def

Remark: there are some undocumented black magic in parser. For instance, to parse $\forall x,y:N \dots$ (meaning $\forall x (N x \rightarrow \forall y (N y \rightarrow \dots))$ or $\forall x,y < z \dots$ (meaning $\forall x (x < z \rightarrow \forall y (y < z \rightarrow \dots))$, there is an obscure extension for binders.

This is really specialized code for universal and existential quantifications ... but advanturous user, looking at the definition of the existential quantifier \/ in the library file prop.phx can try to understand it (though, I think it is not possible).