From f89f0eb4717b64f10bdd0a0edc9e93b949bcb33d Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 12 Feb 2021 18:11:52 +0100
Subject: 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.
---
 kernel/vmlambda.ml | 18 ++++++++++++------
 1 file changed, 12 insertions(+), 6 deletions(-)

(limited to 'kernel/vmlambda.ml')

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
-- 
cgit v1.2.3