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.

Related modules:

• Dcalc.Ast Abstract syntax tree of the default calculus intermediate representation

Typing

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:

• 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.

Interpreter

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.

Related modules:

• Dcalc.Interpreter Reference interpreter for the default calculus

Optimizations

Classical optimizations passes can be performed on the Dcalc AST: partial evaluation, beta and iota-reduction, etc.

Related modules:

• Dcalc.Optimizations Optimization passes for default calculus programs and expressions