rust-nbe-for-mltt

This originally started as a Rust port of Danny Gratzer's implementation of Normalization by Evaluation for Martin-Löf Type Theory, but it has a slightly different architecture and some additional language features. The algorithm for the insertion and unification of metavariables was partly taken from Andras Korvacs' Minimal TT Exampls and smalltt (although gluing is not yet implemented here). It will probably become the basis for a new front-end for Pikelet.

In traditional type checking and normalization that uses DeBruijn indices, you are required to shift variable indices whenever you open up binders. This is extremely expensive, and rules out future optimizations, like using visitors to reduce the number of intermediate allocations as the AST is traversed. This implementation avoids these problems by using a "semantic type checking" algorithm that uses DeBruijn indices for the core syntax, and DeBruijn levels in the syntax of the semantic domain.

Syntax	Binding method	Example
Concrete	Nominal	λz. (λy. y (λx. x)) (λx. z x)
Core	Nameless (DeBruijn Indices)	λ . (λ . 0 (λ . 0)) (λ . 1 0)
Domain	Nameless (DeBruijn Levels)	λ . (λ . 1 (λ . 2)) (λ . 0 1)

TODO

• Convert data types to Rust
• Port NbE and bidirectional type checking
• Add a parser for the concrete syntax
• Desugaring of concrete syntax to core syntax
• Resugaring of core syntax to concrete syntax
• Pretty printing
  • Basic pretty printing
  • Preserve pretty names through type checking and normalization
  • Unfold metavariables when pretty printing values
  • Attempt to avoid unfolding variables when pretty printing values
• Add a REPL
• Add span information to ASTs to improve diagnostics
• Pattern matching elaboration
  • Simple cases
  • Nested cases
  • Multiple scrutinees
  • Lambda case
• Dependent record types
• Primitive operations
• Unification
  • Basic unification
  • Function eta rules
  • Record eta rules
  • Pruning
  • Skolemization
• Metavariable insertion
• Integration tests
  • Parse (pass)
  • Parse (fail)
  • Elaboration (pass)
  • Elaboration (fail)
  • Normalization tests
  • Sample modules
• Error recovery in:
  • Lexer
  • Parser
  • Elaborator
  • Validator