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

Translation from the scope language

The translation from the scope language to the default calculus involves three big features:

• Handle the transformation of context variables (in particular, functions)
• Build signatures for the scopes as functions
• Transform the list of scopes into a program

The last point is based on the inter-scope dependency carried out on the scope language by Scopelang.Dependency.

Related modules:

• Dcalc.From_scopelang Scope language to default calculus translator

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.

Autotest

This module runs the interpreter on annotated test scopes, and inserts additional assertions that the results match the obtained results into the program.

Related modules:

• Dcalc.Autotest This module scans a program for "test" scopes, detected as scopes without any undefined inputs. It runs the interpreter to compute their results, then inserts assertion in the code that ensure correctness of said results.