package catala
Install
dune-project
Dependency
Authors
Maintainers
Sources
md5=2615968670ac21b1d00386a9b04b3843
sha512=eff292fdd75012f26ce7b17020f5a8374eef37cd4dd6ba60338dfbe89fbcad3443d1b409e44c182b740da9f58dff7e76dcb8ddefe47f9b2b160666d1c6930143
doc/lcalc.html
Lambda calculus
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 translated into option types and operator calls.
The module describing the abstract syntax tree is:
Lcalc.Ast
Abstract syntax tree for the lambda calculus
This intermediate representation corresponds to the lambda calculus presented in the Catala formalization.
Compilation from default calculus
Lcalc.From_dcalc
compiles the default term of the default calculus
Other optional transformations
Closure conversion
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 existentialTClosureEnv
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.
Operator expansion
This transformation is intended to specialise calls to structural polymorphic operators, like =
. This doesn't affect polymorphic operators that work on boxed elements, like list or option processing.
Lcalc.Expand_op
This transformation expands the equality operator, that is polymorphic and needs code generation on the backends that don't natively support it ; note that this is a place-holder, generating inline expansions, and is planned to be replaced with a more serious implementation that generates specific functions. In particular, currently, comparison of enums is quadratic in size.
Monomorphisation
This transformation is required for backends that don't support boxed polymorphic operations. It generates specialised instances of options, tuples and arrays for every type they are actually used with.
Backends
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: