From 4ee0cedff7726a56ebd53125995a7ae131660b4a Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 18 Aug 2020 13:07:54 +0200
Subject: Rename VM-related kernel/cfoo files to kernel/vmfoo

---
 kernel/vmlambda.mli | 45 +++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 45 insertions(+)
 create mode 100644 kernel/vmlambda.mli

(limited to 'kernel/vmlambda.mli')

diff --git a/kernel/vmlambda.mli b/kernel/vmlambda.mli
new file mode 100644
index 0000000000..bd11c2667f
--- /dev/null
+++ b/kernel/vmlambda.mli
@@ -0,0 +1,45 @@
+open Names
+open Constr
+open Vmvalues
+open Environ
+
+type lambda =
+  | Lrel          of Name.t * int
+  | Lvar          of Id.t
+  | Levar         of Evar.t * lambda array
+  | Lprod         of lambda * lambda
+  | Llam          of Name.t Context.binder_annot array * lambda
+  | Llet          of Name.t Context.binder_annot * lambda * lambda
+  | Lapp          of lambda * lambda array
+  | Lconst        of pconstant
+  | Lprim         of pconstant option * CPrimitives.t * lambda array
+        (* No check if None *)
+  | Lcase         of case_info * reloc_table * lambda * lambda * lam_branches
+  | Lif           of lambda * lambda * lambda
+  | Lfix          of (int array * int) * fix_decl
+  | Lcofix        of int * fix_decl
+  | Lint          of int
+  | Lmakeblock    of int * lambda array
+  | Luint         of Uint63.t
+  | Lfloat        of Float64.t
+  | Lval          of structured_values
+  | Lsort         of Sorts.t
+  | Lind          of pinductive
+  | Lproj         of Projection.Repr.t * lambda
+
+and lam_branches =
+  { constant_branches : lambda array;
+    nonconstant_branches : (Name.t Context.binder_annot array * lambda) array }
+
+and fix_decl =  Name.t Context.binder_annot array * lambda array * lambda array
+
+exception TooLargeInductive of Pp.t
+
+val lambda_of_constr : optimize:bool -> env -> Constr.t -> lambda
+
+val decompose_Llam : lambda -> Name.t Context.binder_annot array * lambda
+
+val get_alias : env -> Constant.t -> Constant.t
+
+(** Dump the VM lambda code after compilation (for debugging purposes) *)
+val dump_lambda : bool ref
-- 
cgit v1.2.3