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.
The translation from the scope language to the default calculus involves three big features:
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 translatorWhile 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.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.