Lexer, parser, and type-checker
Related issue: #9.
A Micheline lexer is defined in file
src/michocoq/micheline_lexer.v, it transforms a string into a list of Micheline tokens.
Unfortunately, it seems impossible to enter a newline in a Coq string (maybe a bug in Coq).(this is a bug in ProofGeneral, both
coqcand CoqIDE behave as intended)
Michelson annotations are ignored by the lexer.
A Micheline parser is defined using Menhir in file
src/michocoq/micheline_parser.vy. It transforms a stream of Micheline tokens into a Micheline AST.
Unfortunately, the Menhir parser does not evaluate in Coq (see https://gitlab.inria.fr/fpottier/coq-menhirlib/issues/5).(fixed)
The conversion from the Micheline AST to an untyped Michelson AST is defined in file
Most Michelson macros are supported, (UN)PAPAIR-like macros are missing.
A Michelson bidirectional type-checker is defined in file
src/michocoq/typer.v. And the converse (and trivial) operation is defined in file
src/michocoq/untyper.vin which the typer is also proved to be the inverse of the untyper.
The type-checker can be extracted, it runs successfully on all non-deprecated contracts of the Tezos testsuite except those using the not-yet-supported macros.
- Replace the untyped AST by the one of Michocott,
- Define a pretty-printer,
- Prove that lexing o parsing is the inverse of pretty-printing.
- Extract the evaluator to OCaml.