## Parsing (meta-issue)

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 analysis`

would fail - must be exactly space after`case`

) - 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 (`Lemma`

, `.=.`

, `...`

, `Proof`

, `by`

, `induction`

, `QED`

- TODO: make complete list) can *never* occur in expressions.

The problem is proofs by rewriting:
from `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 `(`

`by`

here.