From 2c45ca1599010406e95e24584dfd6dfca166482e Mon Sep 17 00:00:00 2001
From: Denis Merigoux <denis.merigoux@netc.fr>
Date: Sun, 18 Jun 2023 16:08:16 +0200
Subject: [PATCH] More doc

---
 compiler/index.mld                    | 4 ++--
 compiler/lcalc/closure_conversion.ml  | 5 ++++-
 compiler/lcalc/closure_conversion.mli | 9 +++++++--
 compiler/lcalc/lcalc.mld              | 8 ++++++++
 4 files changed, 21 insertions(+), 5 deletions(-)

diff --git a/compiler/index.mld b/compiler/index.mld
index e7f9fff5..07cdb420 100644
--- a/compiler/index.mld
+++ b/compiler/index.mld
@@ -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:
diff --git a/compiler/lcalc/closure_conversion.ml b/compiler/lcalc/closure_conversion.ml
index 11622362..459fdadb 100644
--- a/compiler/lcalc/closure_conversion.ml
+++ b/compiler/lcalc/closure_conversion.ml
@@ -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 =
diff --git a/compiler/lcalc/closure_conversion.mli b/compiler/lcalc/closure_conversion.mli
index 1cc68459..01b2a637 100644
--- a/compiler/lcalc/closure_conversion.mli
+++ b/compiler/lcalc/closure_conversion.mli
@@ -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 *)
diff --git a/compiler/lcalc/lcalc.mld b/compiler/lcalc/lcalc.mld
index 9be70589..c02fd15a 100644
--- a/compiler/lcalc/lcalc.mld
+++ b/compiler/lcalc/lcalc.mld
@@ -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,