Extract, parse, and implement the semantics of enums/match statements.

[mpenciak]

As a consequence of issue #100 and PR #127 a few new language features have been introduced.

Here is an outline on the possible ways to extract enums:

• We can encode extracted Noir enums as Lean inductives and instances as arms of the inductive
  • The corresponding Lampe syntax would elaborate to a closely matching Lean syntax
  • This seems like it could be a bit complicated because our reliance on PHOAS would mess with a simple 1-to-1 correspondence of types
• We can encode extracted Noir enums "algebraically" as a list of hlists of constructor types
  • Instances will be a pair of an index and a list of denotations of types in the constructor
  • This is a quick and dirty solution, but could cause some headaches when it comes to reason about enums.

In either case I believe we will need to add the semantics of tagged union types.

Depending on how enums get extracted, we can extract match statements to match the semantics:

• In the first case of (using Lean inductives) match statements would desugar to Lean match statements (this is nice because we get to use all the mechanics around Lean match statements in proofs)
• In the second case (algebraic representation) match statements would desugar to if-else blocks.