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 | |
alpha-ident, alpha-idents-list | |||
atom-expr | := | alpha-ident | |
$ any-ident | |||
unif-var | |||
\ alpha-idents-listsort-assignmentatom-expr | |||
( expr) | |||
prefix-expr | |||
app-expr | := | atom-expr | |
atom-exprapp-expr | |||
expr | := | app-expr | |
prefix-expr | |||
infix-expr |
This definition is clear except for two points:
\
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:
\
alpha-ident\
where
the alpha-ident is used somewhere else in the list as a
sub-expression. These items are ``binders''. 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:
$
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.
N
will be equivalent to parsing $N
.... \x\
, where x
is the name
of the sub-expression, then the variable x
may appear in
the , and this will be prefixed with \x
. At the end,
parsing an object whose name is N
will be equivalent to parsing N
(\
) ...(\
). 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 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 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:
lInfix[3] x "+" y
is parsed by parsing
a first expression at priority , then parsing the keyword +
and finally, parsing a second expression at priority . Therefore, parsing +
is equivalent to $+
and parsing +
+
is equivalent to $+
($+
) .
Prefix "{" \P\ "in" y "|" P "}"
is parsed by
parsing the keyword {
, an identifier , the keyword "in", a
fist expression , the keyword |
, a second expression that can use the variable and the keyword }
. Therefore, parsing {
in
|
}
is equivalent to ${
\x
.
Cst
and def
Remark: there are some undocumented black magic in parser. For instance, to parse (meaning or (meaning , 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).