Adding a directly typing parser

[maxkurze1]

Directly typed parser

I am proposing a parser which directly builds a typed syntax tree.

This parser uses the same syntax as the default one to serve as a drop-in replacement.
Its only difference is that it is using <{ ... }> to declare a Koika action.

Typechecking

For some reason, that is still to be investigated, the normal coq type checker fails to check some actions which are declared with this typed syntax. In these cases, users are advised to use #[program] Definition instead of normal Definitions.

I've already tried different alternatives, but none seemed to work so far. I've testing using Equations instead of Definition which did not result in any difference. Additionally, I investigated unicoq, which introduced more typechecking problems than it solved.

Syntax sugar

This typed parser includes the syntax additions proposed in #3.

[sertel]

Very cool stuff!
Great work!