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 default calculus can be later compiled to a lambda calculus.

The module describing the abstract syntax tree is:

• Dcalc.Ast

Printing helpers can be found in Dcalc.Print.

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

Typing

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.

Interpreter

Related modules:

• Dcalc.Interpreter Reference interpreter for the default calculus

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.