In this milestone, we should make the frontend in good shape. This includes the lexer, parser and the elaborator.

Among these three, only the lexer should live in OCaml. The parser and the elaborator should live in Coq and then extract it to OCaml. We use a simple main function in OCaml to connect these components so that they can be executed.

It is not entirely clear at this moment how things should be built. One reference is probably CompCert: https://github.com/AbsInt/CompCert/tree/master/cparser
which, of course, could be an overkill for us.