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

Invariants

While Dcalc is a superset of a fully-fledged simply typed lambda calculus, the Dcalc code actually generated from the previous intermediate representation obeys some strict structural invariants. Those are formalized and empirically tested in Dcalc.Invariants.

Related modules:

• Dcalc.Invariants This file makes explicit few structural invariants of the dcalc asbtract syntax tree. Those invariants have been checked on all tests and examples of catala. The behavior of the compiler on programs that don't follow those invariant in undefined.