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:

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:

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:

Optimizations

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

Related modules: