Lexer, parser, and type-checker

Related issue: #9.

• Lexing

  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 coqc and CoqIDE behave as intended)

  Michelson annotations are ignored by the lexer.

• Parsing

  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)

• Expansion

  The conversion from the Micheline AST to an untyped Michelson AST is defined in file src/michocoq/micheline2michelson.v.

  Most Michelson macros are supported, (UN)PAPAIR-like macros are missing.

• Typing

  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.v in which the typer is also proved to be the inverse of the untyper.

• Extraction

  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.

• TODO

  • 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.