Adjustments to new LFSC grammar. #53
Conversation
doc/lfsc1_5.g4
Outdated
| @@ -89,7 +89,7 @@ type | |||
| | '(' '!' iden ntype type ')' | |||
| // Extension /////////////////////////////// | |||
| | '(' 'Forall' iden ntype type ')' | |||
| | '(' '->' ( ntype | vtype )+ type ')' | |||
| | '(' '->' '(' ( ntype | vtype )+ ')' type ')' | |||
There was a problem hiding this comment.
Surrounding the argument list in parentheses makes it clear when we are done with arguments.
This makes it easier to type-check the return type without constructing an AST for it. Without the parentheses it would be hard to avoid constructing the AST for the return type, since we wouldn't know it isn't an argument (which we would need an AST for!) until we're done processing it.
There was a problem hiding this comment.
Also, this makes -> more like declare-rule and declare-type.
| @@ -117,14 +117,14 @@ term | |||
| | rat_const | |||
| | '(' term term+ ')' | |||
| | '(' '\\' iden term ')' | |||
| | '(' '@' iden term ')' | |||
| | '(' '@' iden term term ')' | |||
There was a problem hiding this comment.
I think was just a typo.
doc/lfsc1_5.g4
Outdated
| | '(' ':' type term ')' | ||
| | '(' '%' iden type term ')' | ||
| // Extensions /////////////////// | ||
| | '(' 'lam' iden term ')' | ||
| | '(' 'let' iden term term ')' | ||
| | '(' 'proved-by' type term ')' | ||
| | '(' 'assuming' vtype+ term ')' | ||
| | '(' 'assuming' '(' (ntype | vtype)+ ')' term ')' |
There was a problem hiding this comment.
Adding parentheses is a good idea here, just like for the -> form.
It's even more important in this case, because most of the proof will likely be in the final term here, so we really don't want to construct the AST for it.
* (: instead of (id in declaration lists * check-assuming * define-const
I've implemented a version of the new LFSC syntax. Based on my implementation, I'm recommending a few changes to the grammar (rationales in comments).
Once we agree on what the grammar is, I'll port the changes to the C++ LFSC implementation.