aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/flags.mli
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-02-16 17:53:12 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-02-23 15:51:40 +0100
commit557c5a2938f16c0601f5a0323c66b78d2da01ee9 (patch)
tree8dc727525696f27856ae241bec442769e99c8e58 /lib/flags.mli
parentaa2653b5e6877547ece7a8d3051fc67414390240 (diff)
New IR in VM: Clambda.
This intermediate representation serves two purposes: 1- It is a preliminary step for primitive machine integers, as iterators will be compiled to Clambda. 2- It makes the VM compilation passes closer to the ones of native_compute. Once we unifiy the representation of values, we should be able to factorize the lambda-code generation between the two compilers, as well as the reification code. This code was written by Benjamin Grégoire and myself.
Diffstat (limited to 'lib/flags.mli')
-rw-r--r--lib/flags.mli5
1 files changed, 5 insertions, 0 deletions
diff --git a/lib/flags.mli b/lib/flags.mli
index c82410f07..bc07dec80 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -132,3 +132,8 @@ val profile_ltac_cutoff : float ref
val dump_bytecode : bool ref
val set_dump_bytecode : bool -> unit
val get_dump_bytecode : unit -> bool
+
+(** Dump the VM lambda code after compilation (for debugging purposes) *)
+val dump_lambda : bool ref
+val set_dump_lambda : bool -> unit
+val get_dump_lambda : unit -> bool