search

CakeML / cakeml

CakeML: A Verified Implementation of ML
https://cakeml.org
Other
963 stars 84 forks source link

more readable grammar #94

Open xrchz opened 8 years ago

xrchz commented 8 years ago

The current CakeML grammar is carefully designed to be non-ambiguous, but as a result has a surprising number of non-terminals and is quite involved. For presentation purposes, it would be nice to have a (possibly ambiguous) higher-level grammar, that can then be used as the semantics, with the current grammar relegated as an implementation strategy.

See also https://lists.cakeml.org/private/dev/2015-November/001365.html

SOwens commented 8 years ago

It would be nice to have a more presentable grammar that accepts the same source programs as the real grammar. You’d also want to prove that for those source programs, the parse tree of the actual grammar is one of the parse trees of the presentable grammar. However, the semantics must use the actual grammar, not the presentable one, as it is important for the semantics to specify that 1+ 2 * 3 is 7 and not 9.

I think it’s worth having the presentable grammar for documentation purposes even if the 2 properties above are not verified, although it would be nice to verify them eventually.

tanyongkiam commented 8 years ago

The grammar (at least in grammar.txt) could also do with removal of things that aren't (currently) in the initial program. (Or the initial program needs to be extended) In particular: o, before, @ and \ in the infixes aren't available (AFAIK).