Merge PR #13628: Cache meta instances in Clenv

Reviewed-by: mattam82
Reviewed-by: gares
Ack-by: SkySkimmer

2 files changed, 41 insertions, 21 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 387f0f6f5f..00ac5a0624 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -37,15 +37,28 @@ type clausenv = {
   env      : env;
   evd      : evar_map;
   templval : constr freelisted;
-  templtyp : constr freelisted }
+  templtyp : constr freelisted;
+  cache : Reductionops.meta_instance_subst;
+}
+
+let mk_clausenv env evd templval templtyp = {
+  env; evd; templval; templtyp; cache = create_meta_instance_subst evd;
+}
+
+let update_clenv_evd clenv evd =
+  mk_clausenv clenv.env evd clenv.templval clenv.templtyp
 
 let cl_env ce = ce.env
 let cl_sigma ce =  ce.evd
 
-let clenv_term clenv c = meta_instance clenv.env clenv.evd c
-let clenv_meta_type clenv mv = Typing.meta_type clenv.env clenv.evd mv
-let clenv_value clenv = meta_instance clenv.env clenv.evd clenv.templval
-let clenv_type clenv = meta_instance clenv.env clenv.evd clenv.templtyp
+let clenv_term clenv c = meta_instance clenv.env clenv.cache c
+let clenv_meta_type clenv mv =
+  let ty =
+    try Evd.meta_ftype clenv.evd mv
+    with Not_found -> anomaly (str "unknown meta ?" ++ str (Nameops.string_of_meta mv) ++ str ".") in
+  meta_instance clenv.env clenv.cache ty
+let clenv_value clenv = meta_instance clenv.env clenv.cache clenv.templval
+let clenv_type clenv = meta_instance clenv.env clenv.cache clenv.templtyp
 
 let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t
 
@@ -67,7 +80,8 @@ let clenv_push_prod cl =
         { templval = mk_freelisted def;
           templtyp = mk_freelisted concl;
           evd = e';
-          env = cl.env }
+          env = cl.env;
+          cache = create_meta_instance_subst e' }
     | _ -> raise NotExtensibleClause
   in clrec typ
 
@@ -109,7 +123,8 @@ let mk_clenv_from_env env sigma n (c,cty) =
   { templval = mk_freelisted (applist (c,args));
     templtyp = mk_freelisted concl;
     evd = evd;
-    env = env }
+    env = env;
+    cache = create_meta_instance_subst evd }
 
 let mk_clenv_from_n gls n (c,cty) =
   let env = Proofview.Goal.env gls in
@@ -158,7 +173,7 @@ let clenv_assign mv rhs clenv =
         clenv
     else
       let st = (Conv,TypeNotProcessed) in
-      {clenv with evd = meta_assign mv (rhs_fls.rebus,st) clenv.evd}
+      update_clenv_evd clenv (meta_assign mv (rhs_fls.rebus,st) clenv.evd)
   with Not_found ->
     user_err Pp.(str "clenv_assign: undefined meta")
 
@@ -202,19 +217,19 @@ let clenv_assign mv rhs clenv =
    In any case, we respect the order given in A.
 *)
 
-let clenv_metas_in_type_of_meta env evd mv =
-  (mk_freelisted (meta_instance env evd (meta_ftype evd mv))).freemetas
+let clenv_metas_in_type_of_meta clenv mv =
+  (mk_freelisted (meta_instance clenv.env clenv.cache (meta_ftype clenv.evd mv))).freemetas
 
 let dependent_in_type_of_metas clenv mvs =
   List.fold_right
-    (fun mv -> Metaset.union (clenv_metas_in_type_of_meta clenv.env clenv.evd mv))
+    (fun mv -> Metaset.union (clenv_metas_in_type_of_meta clenv mv))
     mvs Metaset.empty
 
 let dependent_closure clenv mvs =
   let rec aux mvs acc =
     Metaset.fold
       (fun mv deps ->
-        let metas_of_meta_type = clenv_metas_in_type_of_meta clenv.env clenv.evd mv in
+        let metas_of_meta_type = clenv_metas_in_type_of_meta clenv mv in
         aux metas_of_meta_type (Metaset.union deps metas_of_meta_type))
       mvs acc in
   aux mvs mvs
@@ -297,11 +312,10 @@ let meta_reducible_instance env evd b =
   else irec b.rebus
 
 let clenv_unify ?(flags=default_unify_flags ()) cv_pb t1 t2 clenv =
-  { clenv with
-      evd = w_unify ~flags clenv.env clenv.evd cv_pb t1 t2 }
+  update_clenv_evd clenv (w_unify ~flags clenv.env clenv.evd cv_pb t1 t2)
 
 let clenv_unify_meta_types ?(flags=default_unify_flags ()) clenv =
-  { clenv with evd = w_unify_meta_types ~flags:flags clenv.env clenv.evd }
+  update_clenv_evd clenv (w_unify_meta_types ~flags:flags clenv.env clenv.evd)
 
 let clenv_unique_resolver_gen ?(flags=default_unify_flags ()) clenv concl =
   if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (whd_nored clenv.env clenv.evd clenv.templtyp.rebus))) then
@@ -414,11 +428,13 @@ let fchain_flags () =
 
 let clenv_fchain ?with_univs ?(flags=fchain_flags ()) mv clenv nextclenv =
   (* Add the metavars of [nextclenv] to [clenv], with their name-environment *)
+  let evd = meta_merge ?with_univs nextclenv.evd clenv.evd in
   let clenv' =
     { templval = clenv.templval;
       templtyp = clenv.templtyp;
-      evd = meta_merge ?with_univs nextclenv.evd clenv.evd;
-      env = nextclenv.env } in
+      evd;
+      env = nextclenv.env;
+      cache = create_meta_instance_subst evd } in
   (* unify the type of the template of [nextclenv] with the type of [mv] *)
   let clenv'' =
     clenv_unify ~flags CUMUL
@@ -538,7 +554,7 @@ let clenv_assign_binding clenv k c =
   let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
   let c_typ = nf_betaiota clenv.env clenv.evd (clenv_get_type_of clenv c) in
   let status,clenv',c = clenv_unify_binding_type clenv c c_typ k_typ in
-  { clenv' with evd = meta_assign k (c,(Conv,status)) clenv'.evd }
+  update_clenv_evd clenv' (meta_assign k (c,(Conv,status)) clenv'.evd)
 
 let clenv_match_args bl clenv =
   if List.is_empty bl then
@@ -640,7 +656,7 @@ let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv =
       Typeclasses.make_unresolvables (fun x -> true) evd'
     else clenv.evd
   in
-  let clenv = { clenv with evd = evd' } in
+  let clenv = update_clenv_evd clenv evd' in
   Proofview.tclTHEN
     (Proofview.Unsafe.tclEVARS (Evd.clear_metas evd'))
     (refiner ~check:false EConstr.Unsafe.(to_constr (clenv_cast_meta clenv (clenv_value clenv))))
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index a72c8c5e1f..6e472da452 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -22,14 +22,18 @@ open Tactypes
 
 (** {6 The Type of Constructions clausale environments.} *)
 
-type clausenv = {
+type clausenv = private {
   env      : env; (** the typing context *)
   evd      : evar_map; (** the mapping from metavar and evar numbers to their
                            types and values *)
   templval : constr freelisted; (** the template which we are trying to fill
                                     out *)
-  templtyp : constr freelisted (** its type *)}
+  templtyp : constr freelisted; (** its type *)
+  cache : Reductionops.meta_instance_subst; (* Reductionops.create_meta_instance_subst evd) *)
+}
 
+val mk_clausenv : env -> evar_map -> constr freelisted -> types freelisted -> clausenv
+val update_clenv_evd : clausenv -> evar_map -> clausenv
 
 (** subject of clenv (instantiated) *)
 val clenv_value     : clausenv -> constr