2020-12-14 17:23:04 +03:00
|
|
|
{0 The Catala compiler}
|
|
|
|
|
|
|
|
{1 Architecture}
|
|
|
|
|
2021-03-19 19:49:56 +03:00
|
|
|
The architecture of the Catala compiler is inspired by
|
2020-12-14 17:23:04 +03:00
|
|
|
{{: https://compcert.org/} CompCert} or the {{: https://nanopass.org/} Nanopass}
|
2021-03-19 19:49:56 +03:00
|
|
|
framework, and is structured around many intermediate representations connected
|
2020-12-14 17:23:04 +03:00
|
|
|
by successive translations passes.
|
|
|
|
|
2021-03-19 19:49:56 +03:00
|
|
|
Here is the recap picture of the different intermediate representations of the
|
2020-12-14 17:23:04 +03:00
|
|
|
Catala compiler (made with an {{: https://textik.com/#c1c1fecda5209492} ASCII diagram tool}):
|
|
|
|
|
2021-03-19 19:49:56 +03:00
|
|
|
{v
|
|
|
|
+---------------+
|
|
|
|
| |
|
|
|
|
| Surface AST |
|
|
|
|
| |
|
|
|
|
+---------------+
|
|
|
|
|
|
|
|
|
|
|
|
|
|
* Separate code from legislation |
|
|
|
|
* Remove syntactic sugars |
|
|
|
|
v
|
2022-01-19 12:54:16 +03:00
|
|
|
+------------------+
|
|
|
|
| |
|
|
|
|
| Desugared AST |
|
|
|
|
| |
|
|
|
|
+------------------+
|
2021-03-19 19:49:56 +03:00
|
|
|
|
|
|
|
|
|
|
|
|
|
* Build rule trees for each definition |
|
|
|
|
* Order variable computations inside scope |
|
|
|
|
v
|
|
|
|
+--------------------+
|
|
|
|
| |
|
|
|
|
| Scope language AST |
|
|
|
|
| |
|
|
|
|
+--------------------+
|
|
|
|
|
|
|
|
|
|
|
|
|
|
* Convert scopes into functions |
|
|
|
|
* Thunking of subscope arguments |
|
|
|
|
|
|
|
|
|
v
|
2020-12-14 17:23:04 +03:00
|
|
|
+----------------------+
|
|
|
|
| |
|
|
|
|
| Default calculus AST |
|
|
|
|
| |
|
2021-03-19 19:49:56 +03:00
|
|
|
+----------------------+
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
* Compile the default term |
|
|
|
|
|
|
|
|
|
v
|
|
|
|
+----------------------+
|
|
|
|
| |
|
|
|
|
| Lambda calculus AST |
|
|
|
|
| |
|
|
|
|
+----------------------+
|
2022-01-19 12:54:16 +03:00
|
|
|
|
|
|
|
|
|
|
|
|
|
* Turn expressions into statements |
|
|
|
|
|
|
|
|
|
v
|
|
|
|
+--------------------------+
|
|
|
|
| |
|
|
|
|
| Statement calculus AST |
|
|
|
|
| |
|
|
|
|
+--------------------------+
|
2021-03-19 19:49:56 +03:00
|
|
|
v}
|
2020-12-14 17:23:04 +03:00
|
|
|
|
|
|
|
{1 List of top-level modules }
|
|
|
|
|
2021-03-19 19:49:56 +03:00
|
|
|
Each of those intermediate representation is bundled into its own `dune` bundle
|
2020-12-14 17:23:04 +03:00
|
|
|
module. Click on the items below if you want to dive straight into the signatures.
|
|
|
|
|
2022-01-19 12:54:16 +03:00
|
|
|
{!modules: Surface Desugared Scopelang Dcalc Lcalc Scalc }
|
2020-12-14 17:23:04 +03:00
|
|
|
|
|
|
|
More documentation can be found on each intermediate representations here.
|
|
|
|
|
2021-03-19 19:49:56 +03:00
|
|
|
{ul
|
2020-12-14 17:23:04 +03:00
|
|
|
{li {{: surface.html} The surface representation}}
|
|
|
|
{li {{: desugared.html} The desugared representation}}
|
|
|
|
{li {{: scopelang.html} The scope language }}
|
|
|
|
{li {{: dcalc.html} The default calculus}}
|
2021-03-19 19:49:56 +03:00
|
|
|
{li {{: lcalc.html} The lambda calculus}}
|
2022-01-21 22:16:07 +03:00
|
|
|
{li {{: scalc.html} The statement calculus}}
|
2020-12-14 17:23:04 +03:00
|
|
|
}
|
|
|
|
|
2020-12-14 20:09:38 +03:00
|
|
|
The main compilation chain is defined in:
|
|
|
|
|
2021-04-22 12:57:50 +03:00
|
|
|
{!modules: Driver}
|
2020-12-14 20:09:38 +03:00
|
|
|
|
2022-01-10 12:59:30 +03:00
|
|
|
Additionally, the compiler features a verification plugin that generates
|
|
|
|
verification condition for proof backends. More information can be found here:
|
|
|
|
|
2022-01-18 17:13:16 +03:00
|
|
|
{ul
|
|
|
|
{li {{: verification.html} Verification}}
|
|
|
|
}
|
2022-01-10 12:59:30 +03:00
|
|
|
|
2020-12-14 17:23:04 +03:00
|
|
|
Last, two more modules contain additional features for the compiler:
|
|
|
|
|
2020-12-14 20:09:38 +03:00
|
|
|
{ul
|
|
|
|
{li {{: literate.html} Literate programming}}
|
|
|
|
{li {{: utils.html} Compiler utilities}}
|
2021-04-22 12:57:50 +03:00
|
|
|
}
|