View on GitHub

Andromeda

Type theory with equality reflection

About the code

The structure of source code

The source code can be found in src, in the following folders:

Main evaluation loop

  1. An expression is parsed using the lexer parser/lexer.ml and the parser parser/parser.mly. The result is a top-level computation of type Input.toplevel.
  2. parser/desugar.ml converts the parsed Input entity to the corresponding Syntax entity. Desugaring discerns names into bound variables (represented as de Bruijn indices), constants, data constructors, and operations.
  3. typing/mlty.ml infers the ML-types (under construction)
  4. runtime/eval.ml evaluates Syntax.toplevel to a Runtime.toplevel. In the course of a top-level evaluation there are subordinate evaluation procedures, the most interesting of which takes a computation Syntax.comp to a Runtime.result which is either a Runtime.value or an operation.