Current implementation of parsing Cyp modules uses
- https://hackage.haskell.org/package/parsec for strucuture of modules, proofs, etc.
- https://hackage.haskell.org/package/haskell-src-exts (HSE) for everything Haskell (data declarations, type declarations, definitions of functions, terms in lemmas and proofs)
the reason certainly is
- avoid re-implementing a Haskell parser
it creates problems on the technical side
- HSE takes ages to compile
- HSE is no longer supported (suggested replacement: http://hackage.haskell.org/package/ghc-lib-parser)
but also on the design side, and that influences user-facing syntax:
Cyp's parser must slice the text at expression boundaries, since HSE' s
parseExp :: String -> ParseResult (Exp SrcSpanInfo) will consume the string completely (TODO: check). Currently the slicing happens at each
.=. (in equational proofs) and at each line break.
Result: an expression can never span more than one line.
This chunking is implemented in Cyp in ad-hoc ways, parsers sometimes look-ahead for line breaks or tokens that logically belong to other parsers.
Can we have some of the following?
- better error messages (cf. #44 )
- less forced line breaks (ideally, none)
- more flexible spacing in-line (I think currently
by case analysiswould fail - must be exactly space after
- ability to write multi-line expressions
- block comments (useful while developing proofs)
- cleaner implementation, e.g., with an extra lexer pass at the start (that does the chunking), and the no look-ahead
For the lexer: we could say that all Cyp-reserved words (
QED - TODO: make complete list) can never occur in expressions.
The problem is proofs by rewriting:
t1 \n (by foo) .=. t2, removing the line break:
t1 (by foo) .=. t2 makes
t1 (by foo) look like an expression. We must detect tokens