The architecture of the Catala compiler is inspired by CompCert or the Nanopass framework, and is structured around many intermediate representations connected by successive translations passes.
Here is the recap picture of the different intermediate representations of the Catala compiler. This process is gathered inside Driver.
|
surface/ | Parsing
. | Separate code from legislation
. v
+---------------+
| |
| Surface AST |----------> HTML, pdf
| |
+---------------+
|
v
desugared/ | Name resolution
. | Remove syntactic sugar
. | Disambiguation
v
+------------------+
| |
| Desugared AST |
| |
+------------------+
|
| Build rule trees for each definition
| Intra-scope dependency analysis
v
scopelang/ | Overload resolution
. | Thunking of subscope arguments
. v
+--------------------+
| |
| Scope language AST |
| |
+--------------------+
|
| Inter-scope dependency analysis
| Typing
v
dcalc/ | Convert scopes into functions
. v
. +----------------------+
| |
| Default calculus AST |-------> (interpret)
| |
+----------------------+
|
| Invariant checks
| Automatic backend test generation
v
lcalc/ | Compile the default terms
. v
. +----------------------+
| |
| Lambda calculus AST |----+--> (interpret)
| | |
+----------------------+ +--> OCaml
|
| Expansion of structural operators
| (optional) closure conversion
| (optional) monomorphisation
| Collision-free renaming
v
scalc/ | Turn expressions into statements
. v
. +--------------------------+
| |
| Statement calculus AST |--+--> Python
| | |
+--------------------------+ +--> C
|
+--> JavaEach of those intermediate representation is bundled into its own dune bundle module. Click on the items below if you want to dive straight into the signatures.
More documentation can be found on each intermediate representations here.
Most of these intermediate representations use a shared AST libary. The main compilation chain is defined in Driver.
Additionally, the compiler features a verification plugin that generates verification condition for proof backends. More information can be found here:
Two more modules contain additional features for the compiler:
The Catala runtimes documentation is available here:
Runtime_ocaml.Runtime The OCaml runtime.Runtime_jsoo.Runtime A js_of_ocaml wrapper around the Runtime_ocaml.Runtime.Last, it is possible to customize the backend to the compiler using a plugin mechanism. The API is defined inside the following module:
See the examples in the plugins/ subdirectory: