catala/compiler/dcalc/dcalc.mld

Ignoring revisions in .git-blame-ignore-revs. Click here to bypass and see the normal blame view.

27 lines
1018 B
Plaintext
Raw Normal View History

2020-12-14 20:09:38 +03:00
{0 Default calculus}
2021-03-19 19:49:56 +03:00
This representation is the fourth in the compilation chain
(see {{: index.html#architecture} Architecture}). Its main difference
with the previous {{: desugared.html} desugared representation} is that scopes
2020-12-14 20:09:38 +03:00
have been lowered into regular functions, and enums and structs have been
2021-03-19 19:49:56 +03:00
lowered to sum and product types. The default calculus can be later compiled
to a {{: lcalc.html} lambda calculus}.
2020-12-14 20:09:38 +03:00
2022-01-19 12:54:16 +03:00
The module describing the abstract syntax tree is {!module: Dcalc.Ast}.
2021-03-19 19:49:56 +03:00
This intermediate representation corresponds to the default calculus
presented in the {{: https://arxiv.org/abs/2103.03198} Catala formalization}.
2020-12-14 20:09:38 +03:00
Related modules:
2022-01-19 12:54:16 +03:00
{!modules: Dcalc.Ast}
2023-06-02 18:17:45 +03:00
{ 1 Invariants }
2020-12-14 20:09:38 +03:00
2023-06-02 18:17:45 +03:00
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 {!module:Dcalc.Invariants}.
2020-12-14 20:09:38 +03:00
Related modules:
2023-06-02 18:17:45 +03:00
{!modules: Dcalc.Invariants}