diff options
Diffstat (limited to 'kernel/cbytegen.ml')
| -rw-r--r-- | kernel/cbytegen.ml | 34 |
1 files changed, 17 insertions, 17 deletions
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 0766f49b3..df5b17da3 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -20,7 +20,7 @@ open Cinstr open Clambda open Constr open Declarations -open Pre_env +open Environ (* Compilation of variables + computing free variables *) @@ -77,6 +77,7 @@ open Pre_env (* ai' = [A_t | accumulate | [Cfx_t | fcofixi] | arg1 | ... | argp ] *) (* If such a block is matched against, we have to force evaluation, *) (* function [fcofixi] is then applied to [ai'] [arg1] ... [argp] *) +(* (note that [ai'] is a pointer to the closure, passed as argument) *) (* Once evaluation is completed [ai'] is updated with the result: *) (* ai' <-- *) (* [A_t | accumulate | [Cfxe_t |fcofixi|result] | arg1 | ... | argp ] *) @@ -500,22 +501,19 @@ let rec compile_lam env reloc lam sz cont = | Lsort (Sorts.Prop _ as s) -> compile_structured_constant reloc (Const_sort s) sz cont | Lsort (Sorts.Type u) -> - (* We separate global and local universes in [u]. The former will be part - of the structured constant, while the later (if any) will be applied as - arguments. *) - let open Univ in begin - let u,s = Universe.compact u in - (* We assume that [Universe.type0m] is a neutral element for [Universe.sup] *) - let compile_get_univ reloc idx sz cont = - set_max_stack_size sz; - compile_fv_elem reloc (FVuniv_var idx) sz cont - in - if List.is_empty s then - compile_structured_constant reloc (Const_sort (Sorts.Type u)) sz cont - else - comp_app compile_structured_constant compile_get_univ reloc + (* We represent universes as a global constant with local universes + "compacted", i.e. as [u arg0 ... argn] where we will substitute (after + evaluation) [Var 0,...,Var n] with values of [arg0,...,argn] *) + let u,s = Univ.compact_univ u in + let compile_get_univ reloc idx sz cont = + set_max_stack_size sz; + compile_fv_elem reloc (FVuniv_var idx) sz cont + in + if List.is_empty s then + compile_structured_constant reloc (Const_sort (Sorts.Type u)) sz cont + else + comp_app compile_structured_constant compile_get_univ reloc (Const_sort (Sorts.Type u)) (Array.of_list s) sz cont - end | Llet (id,def,body) -> compile_lam env reloc def sz @@ -832,6 +830,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 () ++ @@ -875,7 +875,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 -> |