This commit is contained in:
Denis Merigoux 2023-06-18 16:08:16 +02:00
parent 9cf55b0edd
commit 2c45ca1599
4 changed files with 21 additions and 5 deletions

View File

@ -89,9 +89,9 @@ More documentation can be found on each intermediate representations here.
}
Most of these intermediate representations use a {{: shared_ast.html} shared AST libary}.
The main compilation chain is defined in:
The main compilation chain is defined in {!module: Driver}.
{!modules: Driver}
{!modules: Shared_ast Driver}
Additionally, the compiler features a verification plugin that generates
verification condition for proof backends. More information can be found here:

View File

@ -30,7 +30,10 @@ type 'm ctx = {
let tys_as_tanys tys = List.map (fun x -> Mark.map (fun _ -> TAny) x) tys
type 'm hoisted_closure = { name : 'm expr Var.t; closure : 'm expr }
type 'm hoisted_closure = {
name : 'm expr Var.t;
closure : 'm expr (* Starts with [EAbs]. *);
}
let rec hoist_context_free_closures :
type m. m ctx -> m expr -> m hoisted_closure list * m expr boxed =

View File

@ -14,6 +14,11 @@
License for the specific language governing permissions and limitations under
the License. *)
(** 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
{{:http://gallium.inria.fr/~fpottier/mpri/cours04.pdf#page=10} MPRI lesson}.
After closure conversion, closure hoisting is perform and all closures end
up as toplevel definitions. *)
val closure_conversion : 'm Ast.program -> 'm Ast.program Bindlib.box
(** Warning/todo: no effort was yet made to ensure correct propagation of type
annotations in the typed case *)

View File

@ -23,6 +23,14 @@ Related modules:
{!modules: Lcalc.Compile_with_exceptions Lcalc.Compile_without_exceptions}
{1 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.
{!modules: Lcalc.Closure_conversion }
{1 Backends}
The OCaml backend of the lambda calculus is merely a syntactic formatting,