[VM] Rename reloc -> cenv

The renaming is internal only. I believe the name reloc is legacy and
a bit confusing now that the structure contains a full compilation
environment.

1 files changed, 84 insertions, 84 deletions

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index df5b17da3..7a27a3d20 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -399,55 +399,55 @@ let code_makeblock ~stack_size ~arity ~tag cont =
     Kpush :: nest_block tag arity cont
   end
 
-let compile_structured_constant reloc sc sz cont =
+let compile_structured_constant cenv sc sz cont =
   set_max_stack_size sz;
   Kconst sc :: cont
 
 (* compiling application *)
-let comp_args comp_expr reloc args sz cont =
+let comp_args comp_expr cenv args sz cont =
   let nargs_m_1 = Array.length args - 1 in
-  let c = ref (comp_expr reloc args.(0) (sz + nargs_m_1) cont) in
+  let c = ref (comp_expr cenv args.(0) (sz + nargs_m_1) cont) in
   for i = 1 to nargs_m_1 do
-    c := comp_expr reloc args.(i) (sz + nargs_m_1 - i) (Kpush :: !c)
+    c := comp_expr cenv args.(i) (sz + nargs_m_1 - i) (Kpush :: !c)
   done;
   !c
 
-let comp_app comp_fun comp_arg reloc f args sz cont =
+let comp_app comp_fun comp_arg cenv f args sz cont =
   let nargs = Array.length args in
-  if Int.equal nargs 0 then comp_fun reloc f sz cont
+  if Int.equal nargs 0 then comp_fun cenv f sz cont
   else
   match is_tailcall cont with
   | Some k ->
-      comp_args comp_arg reloc args sz
+      comp_args comp_arg cenv args sz
 	(Kpush ::
-	 comp_fun reloc f (sz + nargs)
+         comp_fun cenv f (sz + nargs)
 	   (Kappterm(nargs, k + nargs) :: (discard_dead_code cont)))
   | None ->
       if nargs < 4 then
-	comp_args comp_arg reloc args sz
-	  (Kpush :: (comp_fun reloc f (sz+nargs) (Kapply nargs :: cont)))
+        comp_args comp_arg cenv args sz
+          (Kpush :: (comp_fun cenv f (sz+nargs) (Kapply nargs :: cont)))
       else
 	let lbl,cont1 = label_code cont in
 	Kpush_retaddr lbl ::
-	(comp_args comp_arg reloc args (sz + 3)
-	   (Kpush :: (comp_fun reloc f (sz+3+nargs) (Kapply nargs :: cont1))))
+        (comp_args comp_arg cenv args (sz + 3)
+           (Kpush :: (comp_fun cenv f (sz+3+nargs) (Kapply nargs :: cont1))))
 
 (* Compiling free variables *)
 
-let compile_fv_elem reloc fv sz cont =
+let compile_fv_elem cenv fv sz cont =
   match fv with
-  | FVrel i -> pos_rel i reloc sz :: cont
-  | FVnamed id -> pos_named id reloc :: cont
-  | FVuniv_var i -> pos_universe_var i reloc sz :: cont
-  | FVevar evk -> pos_evar evk reloc :: cont
+  | FVrel i -> pos_rel i cenv sz :: cont
+  | FVnamed id -> pos_named id cenv :: cont
+  | FVuniv_var i -> pos_universe_var i cenv sz :: cont
+  | FVevar evk -> pos_evar evk cenv :: cont
 
-let rec compile_fv reloc l sz cont =
+let rec compile_fv cenv l sz cont =
   match l with
   | [] -> cont
-  | [fvn] -> set_max_stack_size (sz + 1); compile_fv_elem reloc fvn sz cont
+  | [fvn] -> set_max_stack_size (sz + 1); compile_fv_elem cenv fvn sz cont
   | fvn :: tl ->
-      compile_fv_elem reloc fvn sz
-	(Kpush :: compile_fv reloc tl (sz + 1) cont)
+      compile_fv_elem cenv fvn sz
+        (Kpush :: compile_fv cenv tl (sz + 1) cont)
 
 
 (* Compiling constants *)
@@ -472,58 +472,58 @@ let make_areconst n else_lbl cont =
     Kareconst (n, else_lbl)::cont
 
 (* sz is the size of the local stack *)
-let rec compile_lam env reloc lam sz cont =
+let rec compile_lam env cenv lam sz cont =
   set_max_stack_size sz;
   match lam with
-  | Lrel(_, i) -> pos_rel i reloc sz :: cont
+  | Lrel(_, i) -> pos_rel i cenv sz :: cont
 
-  | Lval v -> compile_structured_constant reloc v sz cont
+  | Lval v -> compile_structured_constant cenv v sz cont
 
   | Lproj (n,kn,arg) ->
-     compile_lam env reloc arg sz (Kproj (n,kn) :: cont)
+     compile_lam env cenv arg sz (Kproj (n,kn) :: cont)
 
-  | Lvar id -> pos_named id reloc :: cont
+  | Lvar id -> pos_named id cenv :: cont
 
   | Levar (evk, args) ->
       if Array.is_empty args then
-        compile_fv_elem reloc (FVevar evk) sz cont
+        compile_fv_elem cenv (FVevar evk) sz cont
       else
-        comp_app compile_fv_elem (compile_lam env) reloc (FVevar evk) args sz cont
+        comp_app compile_fv_elem (compile_lam env) cenv (FVevar evk) args sz cont
 
-  | Lconst (kn,u) -> compile_constant env reloc kn u [||] sz cont
+  | Lconst (kn,u) -> compile_constant env cenv kn u [||] sz cont
 
   | Lind (ind,u) ->
     if Univ.Instance.is_empty u then
-      compile_structured_constant reloc (Const_ind ind) sz cont
-    else comp_app compile_structured_constant compile_universe reloc
+      compile_structured_constant cenv (Const_ind ind) sz cont
+    else comp_app compile_structured_constant compile_universe cenv
         (Const_ind ind) (Univ.Instance.to_array u) sz cont
 
   | Lsort (Sorts.Prop _ as s) ->
-    compile_structured_constant reloc (Const_sort s) sz cont
+    compile_structured_constant cenv (Const_sort s) sz cont
   | Lsort (Sorts.Type u) ->
     (* 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 =
+    let compile_get_univ cenv idx sz cont =
       set_max_stack_size sz;
-      compile_fv_elem reloc (FVuniv_var idx) sz cont
+      compile_fv_elem cenv (FVuniv_var idx) sz cont
     in
     if List.is_empty s then
-      compile_structured_constant reloc (Const_sort (Sorts.Type u)) sz cont
+      compile_structured_constant cenv (Const_sort (Sorts.Type u)) sz cont
     else
-      comp_app compile_structured_constant compile_get_univ reloc
+      comp_app compile_structured_constant compile_get_univ cenv
         (Const_sort (Sorts.Type u)) (Array.of_list s) sz cont
 
   | Llet (id,def,body) ->
-      compile_lam env reloc def sz
+      compile_lam env cenv def sz
         (Kpush ::
-         compile_lam env (push_local sz reloc) body (sz+1) (add_pop 1 cont))
+         compile_lam env (push_local sz cenv) body (sz+1) (add_pop 1 cont))
 
   | Lprod (dom,codom) ->
      let cont1 =
-       Kpush :: compile_lam env reloc dom (sz+1) (Kmakeprod :: cont) in
-     compile_lam env reloc codom sz cont1
+       Kpush :: compile_lam env cenv dom (sz+1) (Kmakeprod :: cont) in
+     compile_lam env cenv codom sz cont1
 
   | Llam (ids,body) ->
      let arity = Array.length ids in
@@ -534,12 +534,12 @@ let rec compile_lam env reloc lam sz cont =
      in
      fun_code := [Ksequence(add_grab arity lbl_fun cont_fun,!fun_code)];
      let fv = fv r_fun in
-     compile_fv reloc fv.fv_rev sz (Kclosure(lbl_fun,fv.size) :: cont)
+     compile_fv cenv fv.fv_rev sz (Kclosure(lbl_fun,fv.size) :: cont)
 
   | Lapp (f, args) ->
     begin match f with
-    | Lconst (kn,u) -> compile_constant env reloc kn u args sz cont
-    | _ -> comp_app (compile_lam env) (compile_lam env) reloc f args sz cont
+    | Lconst (kn,u) -> compile_constant env cenv kn u args sz cont
+    | _ -> comp_app (compile_lam env) (compile_lam env) cenv f args sz cont
     end
 
   | Lfix ((rec_args, init), (decl, types, bodies)) ->
@@ -571,7 +571,7 @@ let rec compile_lam env reloc lam sz cont =
 	fun_code := [Ksequence(fcode,!fun_code)]
       done;
       let fv = !rfv in
-      compile_fv reloc fv.fv_rev sz
+      compile_fv cenv fv.fv_rev sz
 	(Kclosurerec(fv.size,init,lbl_types,lbl_bodies) :: cont)
 
 
@@ -607,7 +607,7 @@ let rec compile_lam env reloc lam sz cont =
       done;
       let fv = !rfv in
       set_max_stack_size (sz + fv.size + ndef + 2);
-      compile_fv reloc fv.fv_rev sz
+      compile_fv cenv fv.fv_rev sz
 	(Kclosurecofix(fv.size, init, lbl_types, lbl_bodies) :: cont)
 
 
@@ -625,7 +625,7 @@ let rec compile_lam env reloc lam sz cont =
       let branch1, cont = make_branch cont in
       (* Compilation of the return type *)
       let fcode =
-        ensure_stack_capacity (compile_lam env reloc t sz) [Kpop sz; Kstop]
+        ensure_stack_capacity (compile_lam env cenv t sz) [Kpop sz; Kstop]
       in
       let lbl_typ,fcode = label_code fcode in
       fun_code := [Ksequence(fcode,!fun_code)];
@@ -653,7 +653,7 @@ let rec compile_lam env reloc lam sz cont =
       (* Compilation of constant branches *)
       for i = nconst - 1 downto 0 do
         let aux =
-          compile_lam env reloc branches.constant_branches.(i) sz_b (branch::!c)
+          compile_lam env cenv branches.constant_branches.(i) sz_b (branch::!c)
         in
         let lbl_b,code_b = label_code aux in
         lbl_consts.(i) <- lbl_b;
@@ -665,7 +665,7 @@ let rec compile_lam env reloc lam sz cont =
         let (ids, body) = branches.nonconstant_branches.(i) in
         let arity = Array.length ids in
         let code_b =
-          compile_lam env (push_param arity sz_b reloc)
+          compile_lam env (push_param arity sz_b cenv)
             body (sz_b+arity) (add_pop arity (branch::!c)) in
         let code_b =
             if tag < last_variant_tag then begin
@@ -703,25 +703,25 @@ let rec compile_lam env reloc lam sz cont =
         | Kbranch lbl -> Kpush_retaddr lbl ::  !c
 	| _ -> !c
       in
-      compile_lam env reloc a sz code_sw
+      compile_lam env cenv a sz code_sw
 
   | Lmakeblock (tag,args) ->
     let arity = Array.length args in
     let cont = code_makeblock ~stack_size:(sz+arity-1) ~arity ~tag cont in
-    comp_args (compile_lam env) reloc args sz cont
+    comp_args (compile_lam env) cenv args sz cont
 
   | Lprim (kn, ar, op, args) ->
-    op_compilation env ar op kn reloc args sz cont
+    op_compilation env ar op kn cenv args sz cont
 
   | Luint v ->
      (match v with
-     | UintVal i -> compile_structured_constant reloc (Const_b0 (Uint31.to_int i)) sz cont
+     | UintVal i -> compile_structured_constant cenv (Const_b0 (Uint31.to_int i)) sz cont
      | UintDigits ds ->
        let nargs = Array.length ds in
        if Int.equal nargs 31 then
          let (escape,labeled_cont) = make_branch cont in
          let else_lbl = Label.create() in
-         comp_args (compile_lam env) reloc ds sz
+         comp_args (compile_lam env) cenv ds sz
            ( Kisconst else_lbl::Kareconst(30,else_lbl)::Kcompint31::escape::Klabel else_lbl::Kmakeblock(31, 1)::labeled_cont)
        else
          let code_construct cont = (* spiwack: variant of the global code_construct
@@ -737,40 +737,40 @@ let rec compile_lam env reloc lam sz cont =
            Kclosure(lbl,0) :: cont
          in
          comp_app (fun _ _ _ cont -> code_construct cont)
-           (compile_lam env) reloc () ds sz cont
+           (compile_lam env) cenv () ds sz cont
      | UintDecomp t ->
        let escape_lbl, labeled_cont = label_code cont in
-       compile_lam env  reloc t sz ((Kisconst escape_lbl)::Kdecompint31::labeled_cont))
+       compile_lam env  cenv t sz ((Kisconst escape_lbl)::Kdecompint31::labeled_cont))
 
 
 (* spiwack : compilation of constants with their arguments.
    Makes a special treatment with 31-bit integer addition *)
-and compile_get_global reloc (kn,u) sz cont =
+and compile_get_global cenv (kn,u) sz cont =
   set_max_stack_size sz;
   if Univ.Instance.is_empty u then
     Kgetglobal kn :: cont
   else
     comp_app (fun _ _ _ cont -> Kgetglobal kn :: cont)
-      compile_universe reloc () (Univ.Instance.to_array u) sz cont
+      compile_universe cenv () (Univ.Instance.to_array u) sz cont
 
-and compile_universe reloc uni sz cont =
+and compile_universe cenv uni sz cont =
   set_max_stack_size sz;
   match Univ.Level.var_index uni with
-  | None -> compile_structured_constant reloc (Const_univ_level uni) sz cont
-  | Some idx -> pos_universe_var idx reloc sz :: cont
+  | None -> compile_structured_constant cenv (Const_univ_level uni) sz cont
+  | Some idx -> pos_universe_var idx cenv sz :: cont
 
-and compile_constant env reloc kn u args sz cont =
+and compile_constant env cenv kn u args sz cont =
   set_max_stack_size sz;
   if Univ.Instance.is_empty u then
     (* normal compilation *)
     comp_app (fun _ _ sz cont ->
-        compile_get_global reloc (kn,u) sz cont)
-      (compile_lam env) reloc () args sz cont
+        compile_get_global cenv (kn,u) sz cont)
+      (compile_lam env) cenv () args sz cont
   else
-    let compile_arg reloc constr_or_uni sz cont =
+    let compile_arg cenv constr_or_uni sz cont =
       match constr_or_uni with
-      | ArgLambda t -> compile_lam env reloc t sz cont
-      | ArgUniv uni -> compile_universe reloc uni sz cont
+      | ArgLambda t -> compile_lam env cenv t sz cont
+      | ArgUniv uni -> compile_universe cenv uni sz cont
     in
     let u = Univ.Instance.to_array u in
     let lu = Array.length u in
@@ -779,7 +779,7 @@ and compile_constant env reloc kn u args sz cont =
         (fun i -> if i < lu then ArgUniv u.(i) else ArgLambda args.(i-lu))
     in
     comp_app (fun _ _ _ cont -> Kgetglobal kn :: cont)
-      compile_arg reloc () all sz cont
+      compile_arg cenv () all sz cont
 
 (*template for n-ary operation, invariant: n>=1,
   the operations does the following :
@@ -788,34 +788,34 @@ and compile_constant env reloc kn u args sz cont =
   3/ if at least one is not, branches to the normal behavior:
       Kgetglobal (get_alias !global_env kn) *)
 and op_compilation env n op =
-  let code_construct reloc kn sz cont =
+  let code_construct cenv kn sz cont =
      let f_cont =
          let else_lbl = Label.create () in
          Kareconst(n, else_lbl):: Kacc 0:: Kpop 1::
           op:: Kreturn 0:: Klabel else_lbl::
          (* works as comp_app with nargs = n and tailcall cont [Kreturn 0]*)
-          compile_get_global reloc kn sz (
+          compile_get_global cenv kn sz (
             Kappterm(n, n):: []) (* = discard_dead_code [Kreturn 0] *)
      in
      let lbl = Label.create () in
      fun_code := [Ksequence (add_grab n lbl f_cont, !fun_code)];
      Kclosure(lbl, 0)::cont
   in
-  fun kn reloc args sz cont ->
+  fun kn cenv args sz cont ->
   let nargs = Array.length args in
   if Int.equal nargs n then (*if it is a fully applied addition*)
     let (escape, labeled_cont) = make_branch cont in
     let else_lbl = Label.create () in
     assert (n < 4);
-    comp_args (compile_lam env) reloc args sz
+    comp_args (compile_lam env) cenv args sz
       (Kisconst else_lbl::(make_areconst (n-1) else_lbl
          (*Kaddint31::escape::Klabel else_lbl::Kpush::*)
          (op::escape::Klabel else_lbl::Kpush::
          (* works as comp_app with nargs < 4 and non-tailcall cont*)
-         compile_get_global reloc kn (sz+n) (Kapply n::labeled_cont))))
+         compile_get_global cenv kn (sz+n) (Kapply n::labeled_cont))))
   else
-    comp_app (fun reloc _ sz cont -> code_construct reloc kn sz cont)
-      (compile_lam env) reloc () args sz cont
+    comp_app (fun cenv _ sz cont -> code_construct cenv kn sz cont)
+      (compile_lam env) cenv () args sz cont
 
 
 let is_univ_copy max u =
@@ -846,11 +846,11 @@ let compile ~fail_on_error ?universes:(universes=0) env c =
   Label.reset_label_counter ();
   let cont = [Kstop] in
   try
-    let reloc, init_code =
+    let cenv, init_code =
       if Int.equal universes 0 then
         let lam = lambda_of_constr ~optimize:true env c in
-        let reloc = empty_comp_env () in
-        reloc, ensure_stack_capacity (compile_lam env reloc lam 0) cont
+        let cenv = empty_comp_env () in
+        cenv, ensure_stack_capacity (compile_lam env cenv lam 0) cont
       else
         (* We are going to generate a lambda, but merge the universe closure
          * with the function closure if it exists.
@@ -858,7 +858,7 @@ let compile ~fail_on_error ?universes:(universes=0) env c =
         let lam = lambda_of_constr ~optimize:true env c in
         let params, body = decompose_Llam lam in
         let arity = Array.length params in
-        let reloc = empty_comp_env () in
+        let cenv = empty_comp_env () in
         let full_arity = arity + universes in
         let r_fun = comp_env_fun ~univs:universes arity in
         let lbl_fun = Label.create () in
@@ -869,12 +869,12 @@ let compile ~fail_on_error ?universes:(universes=0) env c =
         fun_code := [Ksequence(add_grab full_arity lbl_fun cont_fun,!fun_code)];
         let fv = fv r_fun in
         let init_code =
-          ensure_stack_capacity (compile_fv reloc fv.fv_rev 0)
+          ensure_stack_capacity (compile_fv cenv fv.fv_rev 0)
                          (Kclosure(lbl_fun,fv.size) :: cont)
         in
-        reloc, init_code
+        cenv, init_code
     in
-    let fv = List.rev (!(reloc.in_env).fv_rev) in
+    let fv = List.rev (!(cenv.in_env).fv_rev) in
     (if !dump_bytecode then
       Feedback.msg_debug (dump_bytecodes init_code !fun_code fv)) ;
     Some (init_code,!fun_code, Array.of_list fv)
@@ -922,13 +922,13 @@ let op2_compilation op =
      fun_code := [Ksequence (add_grab 2 lbl f_cont, !fun_code)];
      Kclosure(lbl, 0)::cont
   in
-  fun normal fc _ reloc args sz cont ->
+  fun normal fc _ cenv args sz cont ->
   if not fc then raise Not_found else
   let nargs = Array.length args in
   if nargs=2 then (*if it is a fully applied addition*)
     let (escape, labeled_cont) = make_branch cont in
     let else_lbl = Label.create () in
-      comp_args compile_constr reloc args sz
+      comp_args compile_constr cenv args sz
 	(Kisconst else_lbl::(make_areconst 1  else_lbl
            (*Kaddint31::escape::Klabel else_lbl::Kpush::*)
            (op::escape::Klabel else_lbl::Kpush::
@@ -940,5 +940,5 @@ let op2_compilation op =
     code_construct normal cont
   else
     comp_app (fun _ _ _ cont -> code_construct normal cont)
-      compile_constr reloc () args sz cont *)
+      compile_constr cenv () args sz cont *)