From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

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

(limited to 'kernel/clambda.mli')

diff --git a/kernel/clambda.mli b/kernel/clambda.mli
new file mode 100644
index 00000000..827eb550
--- /dev/null
+++ b/kernel/clambda.mli
@@ -0,0 +1,30 @@
+open Names
+open Cinstr
+
+exception TooLargeInductive of Pp.t
+
+val lambda_of_constr : optimize:bool -> Pre_env.env -> Constr.t -> lambda
+
+val decompose_Llam : lambda -> Name.t array * lambda
+
+val get_alias : Pre_env.env -> Constant.t -> Constant.t
+
+val compile_prim : int -> Cbytecodes.instruction -> Constr.pconstant -> bool -> lambda array -> lambda
+
+(** spiwack: this function contains the information needed to perform
+            the static compilation of int31 (trying and obtaining
+            a 31-bit integer in processor representation at compile time) *)
+val compile_structured_int31 : bool -> Constr.t array -> lambda
+
+(** this function contains the information needed to perform
+        the dynamic compilation of int31 (trying and obtaining a
+        31-bit integer in processor representation at runtime when
+        it failed at compile time *)
+val dynamic_int31_compilation : bool -> lambda array -> lambda
+
+(*spiwack: compiling function to insert dynamic decompilation before
+           matching integers (in case they are in processor representation) *)
+val int31_escape_before_match : bool -> lambda -> lambda
+
+val eta_expand : (Pre_env.env -> Constr.t -> Constr.types -> Constr.t) Hook.value
+val eta_expand_hook : (Pre_env.env -> Constr.t -> Constr.types -> Constr.t) Hook.t
-- 
cgit v1.2.3