Use OCaml type checker

[dariusf]

After #3, we should look into using the OCaml type checker. The logic of SMT is typed, so type information is technically needed to generate verification conditions. However, our source language is untyped. We get around this by inferring types at the pure formula level, right before translating to SMTLIB. This has made it hard to add other language features.

To fix this for good, we should run the type checker, then generate a core_lang value from a Typedtree instead of a Parsetree.

• The 5.3 frontend has support for the effect syntax we use, so we can vendor it and the type checker, and expose a small API to generate a Typedtree from a file
• Where should we track types - do we need them at every node?