LFSC Syntax Extensions

[alex-ozdemir]

Implements the following syntax extensions:

• Declaration lists are used in a few places: they are a list of arguments that can be named ((: NAME TYPE)) or anonymous (TYPE).
• New type can be declared with (declare-type NAME DECL_LIST), e.g. (declare-types holds (bool))
• New rules can be declared with (declare-rule NAME DECL_LIST RESULT), see below for an example.
• New functions can be defined with (declare-const NAME DECL_LIST RESULT), e.g. (define-const and ((: a bool) (: b bool)) (apply (apply and_fn a) b))
• Function types can be written as (-> DECL_LIST RESULT)
• Proofs are checked using (check-assuming DECL_LIST TYPE TERM), where DECL_LIST introduces assumptions, TYPE represents the proposition, and TERM represents the proof.
• Deprecate %: the symbol for assumptions. % was only valid immediately inside check commands, and is subsumed by the check-assuming command.
• provided is an alias for the side-condition invoking ^ symbol
• let is an alias for the let-binding @ symbol
• Forall is an alias for !, the dependent function type symbol.
• lam is an alias for \, the un-annotated lambda symbol.

Implementation changes:

• gave the token stream an additional lookahead space.
• Add a few helper functions for checking declaration lists and building macros.

[alex-ozdemir]

Per discussion with Andy, I've documented some of the implementation.

I've also added a wiki entry which explains the structure of the language, including the syntactic extensions here: https://github.com/CVC4/LFSC/wiki/Language-Reference.

Upon reflection, I see that there would be a fairly easy way to break up this PR, if you would like that, Andy. I could split it into a sequence of PRs where the first PR refactors the lexer a bit, and the subsequent PRs add new syntactic extensions one at a time, or in small groups. Happy to do this if you'd like. Let me know.

[ajreynol]

In the proof signature meeting today, there is a suggestion to either not include forall as syntactic sugar or to use pi instead.