View on GitHub

Andromeda 1

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/ and the parser parser/parser.mly. The result is a top-level computation of type Input.toplevel.
  2. parser/ 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/ infers the ML-types (under construction)
  4. runtime/ 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.