Normalize evars during bytecode compilation (fix #13841).

Otherwise, the interpreter sees already unified evars as accumulators
rather than actual constants, thus preventing the computations from
progressing.

This was caused by 6b61b63bb8626827708024cbea1312a703a54124, which removed
evar normalization. The effect went unnoticed because the computed term is
still convertible to the reduced term, except that it is the lazy
machinery that ends up reducing it, rather than the bytecode one.
So, performances became abysmal, seemingly at random.

1 files changed, 11 insertions, 11 deletions

diff --git a/kernel/vmsymtable.ml b/kernel/vmsymtable.ml
index ae0fa38571..90ee1c5378 100644
--- a/kernel/vmsymtable.ml
+++ b/kernel/vmsymtable.ml
@@ -144,7 +144,7 @@ let slot_for_proj_name key =
     ProjNameTable.add proj_name_tbl key n;
     n
 
-let rec slot_for_getglobal env kn =
+let rec slot_for_getglobal env sigma kn =
   let (cb,(_,rk)) = lookup_constant_key kn env in
   try key rk
   with NotEvaluated ->
@@ -155,22 +155,22 @@ let rec slot_for_getglobal env kn =
       | Some code ->
          match Vmemitcodes.force code with
          | BCdefined(code,pl,fv) ->
-           let v = eval_to_patch env (code,pl,fv) in
+           let v = eval_to_patch env sigma (code,pl,fv) in
            set_global v
-         | BCalias kn' -> slot_for_getglobal env kn'
+         | BCalias kn' -> slot_for_getglobal env sigma kn'
          | BCconstant -> set_global (val_of_constant kn)
     in
 (*Pp.msgnl(str"value stored at: "++int pos);*)
     rk := Some (CEphemeron.create pos);
     pos
 
-and slot_for_fv env fv =
+and slot_for_fv env sigma fv =
   let fill_fv_cache cache id v_of_id env_of_id b =
     let v,d =
       match b with
       | None -> v_of_id id, Id.Set.empty
       | Some c ->
-          val_of_constr (env_of_id id env) c,
+          val_of_constr (env_of_id id env) sigma c,
           Environ.global_vars_set env c in
     build_lazy_val cache (v, d); v in
   let val_of_rel i = val_of_rel (nb_rel env - i) in
@@ -194,11 +194,11 @@ and slot_for_fv env fv =
   | FVuniv_var _idu ->
     assert false
 
-and eval_to_patch env (buff,pl,fv) =
+and eval_to_patch env sigma (buff,pl,fv) =
   let slots = function
     | Reloc_annot a -> slot_for_annot a
     | Reloc_const sc -> slot_for_str_cst sc
-    | Reloc_getglobal kn -> slot_for_getglobal env kn
+    | Reloc_getglobal kn -> slot_for_getglobal env sigma kn
     | Reloc_proj_name p -> slot_for_proj_name p
     | Reloc_caml_prim op -> slot_for_caml_prim op
   in
@@ -207,13 +207,13 @@ and eval_to_patch env (buff,pl,fv) =
     (* Environment should look like a closure, so free variables start at slot 2. *)
     let a = Array.make (Array.length fv + 2) crazy_val in
     a.(1) <- Obj.magic 2;
-    Array.iteri (fun i v -> a.(i + 2) <- slot_for_fv env v) fv;
+    Array.iteri (fun i v -> a.(i + 2) <- slot_for_fv env sigma v) fv;
     a in
   eval_tcode tc (get_atom_rel ()) (vm_global global_data.glob_val) vm_env
 
-and val_of_constr env c =
-  match compile ~fail_on_error:true env c with
-  | Some v -> eval_to_patch env (to_memory v)
+and val_of_constr env sigma c =
+  match compile ~fail_on_error:true env sigma c with
+  | Some v -> eval_to_patch env sigma (to_memory v)
   | None -> assert false
 
 let set_transparent_const _kn = () (* !?! *)