package catala
Install
Dune Dependency
Authors
Maintainers
Sources
md5=1408a1cce45c7d5990b981e83e7589c2
sha512=eb3b923aa1f743378b4a05e30f50be5d180dc862a716270d747a90e469017f42fa5fc41352f02fbbf59cd2560f91c4f1b32cf38d80085b105d9387b0aed2039d
doc/index.html
The Catala compiler
Architecture
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 (made with an ASCII diagram tool):
+---------------+ | | | Surface AST | | | +---------------+ | | * Separate code from legislation | * Remove syntactic sugars | v +------------------+ | | | Desugared AST | | | +------------------+ | | * Build rule trees for each definition | * Order variable computations inside scope | v +--------------------+ | | | Scope language AST | | | +--------------------+ | | * Convert scopes into functions | * Thunking of subscope arguments | | v +----------------------+ | | | Default calculus AST | | | +----------------------+ | | | * Compile the default term | | v +----------------------+ | | | Lambda calculus AST | | | +----------------------+ | | * Turn expressions into statements | | v +--------------------------+ | | | Statement calculus AST | | | +--------------------------+
List of top-level modules
Each 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.
- The surface representation
- The desugared representation
- The scope language
- The default calculus
- The lambda calculus
- The statement calculus
The main compilation chain is defined in:
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 theRuntime_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: