Default calculus

This representation is the fourth in the compilation chain (see Architecture). Its main difference with the previous desugared representation is that scopes have been lowered into regular functions, and enums and structs have been lowered to sum and product types.

The module describing the abstract syntax tree is:

Printing helpers can be found in Dcalc.Print.

This intermediate representation corresponds to the default calculus presented in the Catala formalization.


Related modules:

  • Dcalc.Typing Typing for the default calculus. Because of the error terms, we perform type inference using the classical W algorithm with union-find unification.

This representation is where the typing is performed. Indeed, Dcalc.Typing implements the classical W algorithm corresponding to a Hindley-Milner type system, without type constraints.


Related modules:

Since this representation is currently the last of the compilation chain, an Dcalc.Interpreter module is provided to match the execution semantics of the default calculus.

Later, translations to a regular lambda calculus and/or a simple imperative language are bound to be added.