diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-04-30 09:25:44 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-04-30 09:25:44 +0200 |
| commit | 8c3d9eb165b456fc83753624efe6708832e9b52f (patch) | |
| tree | f0c7050b1b2fcaa63167e8830c535d1dde982f35 /kernel | |
| parent | 14226761af6525c9848f3626cd86b0d4e47dad4d (diff) | |
| parent | ce9b17821a3be3dee7fa7e49c35edaefc658b965 (diff) | |
Merge PR #6958: [lib] Move global options to their proper place.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/cbytegen.ml | 4 | ||||
| -rw-r--r-- | kernel/cbytegen.mli | 3 | ||||
| -rw-r--r-- | kernel/clambda.ml | 4 | ||||
| -rw-r--r-- | kernel/clambda.mli | 3 |
4 files changed, 11 insertions, 3 deletions
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 70dc6867a..a771945dd 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -829,6 +829,8 @@ let is_univ_copy max u = else false +let dump_bytecode = ref false + let dump_bytecodes init code fvs = let open Pp in (str "code =" ++ fnl () ++ @@ -872,7 +874,7 @@ let compile ~fail_on_error ?universes:(universes=0) env c = reloc, init_code in let fv = List.rev (!(reloc.in_env).fv_rev) in - (if !Flags.dump_bytecode then + (if !dump_bytecode then Feedback.msg_debug (dump_bytecodes init_code !fun_code fv)) ; Some (init_code,!fun_code, Array.of_list fv) with TooLargeInductive msg -> diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli index abab58b60..1c4cdcbeb 100644 --- a/kernel/cbytegen.mli +++ b/kernel/cbytegen.mli @@ -25,3 +25,6 @@ val compile_constant_body : fail_on_error:bool -> (** Shortcut of the previous function used during module strengthening *) val compile_alias : Names.Constant.t -> body_code + +(** Dump the bytecode after compilation (for debugging purposes) *) +val dump_bytecode : bool ref diff --git a/kernel/clambda.ml b/kernel/clambda.ml index 7b637c20e..641d424e2 100644 --- a/kernel/clambda.ml +++ b/kernel/clambda.ml @@ -807,7 +807,7 @@ and lambda_of_args env start args = (*********************************) - +let dump_lambda = ref false let optimize_lambda lam = let lam = simplify subst_id lam in @@ -819,7 +819,7 @@ let lambda_of_constr ~optimize genv c = Renv.push_rels env (Array.of_list ids); let lam = lambda_of_constr env c in let lam = if optimize then optimize_lambda lam else lam in - if !Flags.dump_lambda then + if !dump_lambda then Feedback.msg_debug (pp_lam lam); lam diff --git a/kernel/clambda.mli b/kernel/clambda.mli index 89b7fd8e3..6cf46163e 100644 --- a/kernel/clambda.mli +++ b/kernel/clambda.mli @@ -25,3 +25,6 @@ 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 + +(** Dump the VM lambda code after compilation (for debugging purposes) *) +val dump_lambda : bool ref |