This representation is the fifth in the compilation chain (see Architecture). Its main difference with the previous default calculus is the absence of the default term, which has been eliminated through diverse compilation schemes.
The module describing the abstract syntax tree is:
Lcalc.Ast Abstract syntax tree for the lambda calculusThis intermediate representation corresponds to the lambda calculus presented in the Catala formalization.
Lcalc.Compile_with_exceptions compiles the default term of the default calculus using catchable exceptions. This compilation scheme has been certified. Another compilation scheme that uses an option monad instead is available at Lcalc.Compile_without_exceptions.
Related modules:
Lcalc.Compile_with_exceptions Lcalc.Compile_without_exceptions To target languages that don't have support for closures, we need to convert the closures to first-class functions in function-pointer-passing style computations.
Lcalc.Closure_conversion This module performs environment-passing style closure conversion, relying on the existential TClosureEnv type and tuples for closure environments. The implementation is based on François Pottier's MPRI lesson. After closure conversion, closure hoisting is perform and all closures end up as toplevel definitions.The OCaml backend of the lambda calculus is merely a syntactic formatting, since the core of the OCaml value language is effectively a lambda calculus.
Related modules: