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.

7 files changed, 37 insertions, 27 deletions

diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 1432fb9310..d31d7a03b6 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -196,8 +196,9 @@ let vm_conv_gen cv_pb env univs t1 t2 =
       TransparentState.full env univs t1 t2
   else
   try
-    let v1 = val_of_constr env t1 in
-    let v2 = val_of_constr env t2 in
+    let sigma _ = assert false in
+    let v1 = val_of_constr env sigma t1 in
+    let v2 = val_of_constr env sigma t2 in
     fst (conv_val env cv_pb (nb_rel env) v1 v2 univs)
   with Not_found | Invalid_argument _ ->
     warn_bytecode_compiler_failed ();
diff --git a/kernel/vmbytegen.ml b/kernel/vmbytegen.ml
index 20de4bc81b..7d3b3469b0 100644
--- a/kernel/vmbytegen.ml
+++ b/kernel/vmbytegen.ml
@@ -840,21 +840,21 @@ let dump_bytecodes init code fvs =
      prlist_with_sep (fun () -> str "; ") pp_fv_elem fvs ++
      fnl ())
 
-let compile ~fail_on_error ?universes:(universes=0) env c =
+let compile ~fail_on_error ?universes:(universes=0) env sigma c =
   init_fun_code ();
   Label.reset_label_counter ();
   let cont = [Kstop] in
   try
     let cenv, init_code =
       if Int.equal universes 0 then
-        let lam = lambda_of_constr ~optimize:true env c in
+        let lam = lambda_of_constr ~optimize:true env sigma c in
         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.
          *)
-        let lam = lambda_of_constr ~optimize:true env c in
+        let lam = lambda_of_constr ~optimize:true env sigma c in
         let params, body = decompose_Llam lam in
         let arity = Array.length params in
         let cenv = empty_comp_env () in
@@ -896,7 +896,8 @@ let compile_constant_body ~fail_on_error env univs = function
             let con= Constant.make1 (Constant.canonical kn') in
               Some (BCalias (get_alias env con))
         | _ ->
-            let res = compile ~fail_on_error ~universes:instance_size env body in
+            let sigma _ = assert false in
+            let res = compile ~fail_on_error ~universes:instance_size env sigma body in
               Option.map (fun x -> BCdefined (to_memory x)) res
 
 (* Shortcut of the previous function used during module strengthening *)
diff --git a/kernel/vmbytegen.mli b/kernel/vmbytegen.mli
index aef7ac3d6b..c724cad5ec 100644
--- a/kernel/vmbytegen.mli
+++ b/kernel/vmbytegen.mli
@@ -15,8 +15,10 @@ open Declarations
 open Environ
 
 (** Should only be used for monomorphic terms *)
-val compile : fail_on_error:bool ->
-              ?universes:int -> env -> constr -> (bytecodes * bytecodes * fv) option
+val compile :
+  fail_on_error:bool -> ?universes:int ->
+  env -> (existential -> constr option) -> constr ->
+  (bytecodes * bytecodes * fv) option
 (** init, fun, fv *)
 
 val compile_constant_body : fail_on_error:bool ->
diff --git a/kernel/vmlambda.ml b/kernel/vmlambda.ml
index 91de58b0e6..e353348ac7 100644
--- a/kernel/vmlambda.ml
+++ b/kernel/vmlambda.ml
@@ -591,12 +591,14 @@ struct
 
   type t = {
     global_env : env;
+    evar_body : existential -> constr option;
     name_rel : Name.t Vect.t;
     construct_tbl : (constructor, constructor_info) Hashtbl.t;
   }
 
-  let make env = {
+  let make env sigma = {
     global_env = env;
+    evar_body = sigma;
     name_rel = Vect.make 16 Anonymous;
     construct_tbl = Hashtbl.create 111
   }
@@ -633,9 +635,13 @@ open Renv
 let rec lambda_of_constr env c =
   match Constr.kind c with
   | Meta _ -> raise (Invalid_argument "Vmbytegen.lambda_of_constr: Meta")
-  | Evar (evk, args) ->
-    let args = Array.map_of_list (fun c -> lambda_of_constr env c) args in
-    Levar (evk, args)
+  | Evar (evk, args as ev) ->
+      begin match env.evar_body ev with
+      | None ->
+          let args = Array.map_of_list (fun c -> lambda_of_constr env c) args in
+          Levar (evk, args)
+      | Some t -> lambda_of_constr env t
+      end
 
   | Cast (c, _, _) -> lambda_of_constr env c
 
@@ -774,8 +780,8 @@ let optimize_lambda lam =
   let lam = simplify subst_id lam in
   remove_let subst_id lam
 
-let lambda_of_constr ~optimize genv c =
-  let env = Renv.make genv in
+let lambda_of_constr ~optimize genv sigma c =
+  let env = Renv.make genv sigma in
   let ids = List.rev_map Context.Rel.Declaration.get_annot (rel_context genv) in
   Renv.push_rels env (Array.of_list ids);
   let lam = lambda_of_constr env c in
diff --git a/kernel/vmlambda.mli b/kernel/vmlambda.mli
index ad5f81638f..03d3393219 100644
--- a/kernel/vmlambda.mli
+++ b/kernel/vmlambda.mli
@@ -33,7 +33,7 @@ and fix_decl =  Name.t Context.binder_annot array * lambda array * lambda array
 
 exception TooLargeInductive of Pp.t
 
-val lambda_of_constr : optimize:bool -> env -> Constr.t -> lambda
+val lambda_of_constr : optimize:bool -> env -> (existential -> constr option) -> Constr.t -> lambda
 
 val decompose_Llam : lambda -> Name.t Context.binder_annot array * lambda
 
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 = () (* !?! *)
diff --git a/kernel/vmsymtable.mli b/kernel/vmsymtable.mli
index e480bfcec1..c6dc09d944 100644
--- a/kernel/vmsymtable.mli
+++ b/kernel/vmsymtable.mli
@@ -14,7 +14,7 @@ open Names
 open Constr
 open Environ
 
-val val_of_constr : env -> constr -> Vmvalues.values
+val val_of_constr : env -> (existential -> constr option) -> constr -> Vmvalues.values
 
 val set_opaque_const      : Constant.t -> unit
 val set_transparent_const : Constant.t -> unit