Merge PR #13628: Cache meta instances in Clenv

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

8 files changed, 103 insertions, 58 deletions

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 7a5d0897b5..9580825010 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1184,11 +1184,15 @@ let vm_infer_conv ?(pb=Reduction.CUMUL) env t1 t2 =
 
 let default_plain_instance_ident = Id.of_string "H"
 
+type subst_fun = { sfun : metavariable -> EConstr.t }
+
 (* Try to replace all metas. Does not replace metas in the metas' values
  * Differs from (strong whd_meta). *)
-let plain_instance sigma s c =
+let plain_instance sigma s c = match s with
+| None -> c
+| Some s ->
   let rec irec n u = match EConstr.kind sigma u with
-    | Meta p -> (try lift n (Metamap.find p s) with Not_found -> u)
+    | Meta p -> (try lift n (s.sfun p) with Not_found -> u)
     | App (f,l) when isCast sigma f ->
         let (f,_,t) = destCast sigma f in
         let l' = Array.Fun1.Smart.map irec n l in
@@ -1197,7 +1201,7 @@ let plain_instance sigma s c =
             (* Don't flatten application nodes: this is used to extract a
                proof-term from a proof-tree and we want to keep the structure
                of the proof-tree *)
-            (try let g = Metamap.find p s in
+            (try let g = s.sfun p in
             match EConstr.kind sigma g with
             | App _ ->
                 let l' = Array.Fun1.Smart.map lift 1 l' in
@@ -1208,12 +1212,11 @@ let plain_instance sigma s c =
             with Not_found -> mkApp (f,l'))
         | _ -> mkApp (irec n f,l'))
     | Cast (m,_,_) when isMeta sigma m ->
-        (try lift n (Metamap.find (destMeta sigma m) s) with Not_found -> u)
+        (try lift n (s.sfun (destMeta sigma m)) with Not_found -> u)
     | _ ->
         map_with_binders sigma succ irec n u
   in
-  if Metamap.is_empty s then c
-  else irec 0 c
+  irec 0 c
 
 (* [instance] is used for [res_pf]; the call to [local_strong whd_betaiota]
    has (unfortunately) different subtle side effects:
@@ -1415,23 +1418,41 @@ let is_arity env sigma c =
 (*************************************)
 (* Metas *)
 
-let meta_value env evd mv =
-  let rec valrec mv =
-    match meta_opt_fvalue evd mv with
-    | Some (b,_) ->
-      let metas = Metamap.bind valrec b.freemetas in
-      instance env evd metas b.rebus
-    | None -> mkMeta mv
+type meta_instance_subst = {
+  sigma : Evd.evar_map;
+  mutable cache : EConstr.t Metamap.t;
+}
+
+let create_meta_instance_subst sigma = {
+  sigma;
+  cache = Metamap.empty;
+}
+
+let eval_subst env subst =
+  let rec ans mv =
+    try Metamap.find mv subst.cache
+    with Not_found ->
+      match meta_opt_fvalue subst.sigma mv with
+      | None -> mkMeta mv
+      | Some (b, _) ->
+        let metas =
+          if Metaset.is_empty b.freemetas then None
+          else Some { sfun = ans }
+        in
+        let res = instance env subst.sigma metas b.rebus in
+        let () = subst.cache <- Metamap.add mv res subst.cache in
+        res
   in
-  valrec mv
+  { sfun = ans }
 
-let meta_instance env sigma b =
+let meta_instance env subst b =
   let fm = b.freemetas in
   if Metaset.is_empty fm then b.rebus
   else
-    let c_sigma = Metamap.bind (fun mv -> meta_value env sigma mv) fm in
-    instance env sigma c_sigma b.rebus
+    let sfun = eval_subst env subst in
+    instance env subst.sigma (Some sfun) b.rebus
 
 let nf_meta env sigma c =
+  let sigma = create_meta_instance_subst sigma in
   let cl = mk_freelisted c in
   meta_instance env sigma { cl with rebus = cl.rebus }
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 04dfc5ffe6..0b7f43f469 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -258,7 +258,11 @@ val whd_betaiota_deltazeta_for_iota_state :
   TransparentState.t -> state_reduction_function
 
 (** {6 Meta-related reduction functions } *)
-val meta_instance : env -> evar_map -> constr freelisted -> constr
+type meta_instance_subst
+
+val create_meta_instance_subst : Evd.evar_map -> meta_instance_subst
+
+val meta_instance : env -> meta_instance_subst -> constr freelisted -> constr
 val nf_meta       : env -> evar_map -> constr -> constr
 
 exception AnomalyInConversion of exn
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index aeb3873de7..e3e5244a8c 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -33,7 +33,7 @@ let meta_type env evd mv =
   let ty =
     try Evd.meta_ftype evd mv
     with Not_found -> anomaly (str "unknown meta ?" ++ str (Nameops.string_of_meta mv) ++ str ".") in
-  meta_instance env evd ty
+  meta_instance env (create_meta_instance_subst evd) ty
 
 let inductive_type_knowing_parameters env sigma (ind,u) jl =
   let u = Unsafe.to_instance u in
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
diff --git a/tactics/equality.ml b/tactics/equality.ml
index fcdd23a9c1..633b9da053 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -154,7 +154,8 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl =
   let c1 = args.(arglen - 2) in
   let c2 = args.(arglen - 1) in
   let try_occ (evd', c') =
-    Clenv.clenv_pose_dependent_evars ~with_evars:true {eqclause with evd = evd'}
+    let clenv = Clenv.update_clenv_evd eqclause evd' in
+    Clenv.clenv_pose_dependent_evars ~with_evars:true clenv
   in
   let flags = make_flags frzevars (Tacmach.New.project gl) rewrite_unif_flags eqclause in
   let occs =
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 6fab111e6f..ace51c40d4 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -340,10 +340,8 @@ let instantiate_hint env sigma p =
   let mk_clenv (c, cty, ctx) =
     let sigma = merge_context_set_opt sigma ctx in
     let cl = mk_clenv_from_env env sigma None (c,cty) in
-    let cl = {cl with templval =
-          { cl.templval with rebus = strip_params env sigma cl.templval.rebus };
-        env = empty_env}
-    in
+    let templval = { cl.templval with rebus = strip_params env sigma cl.templval.rebus } in
+    let cl = mk_clausenv empty_env cl.evd templval cl.templtyp in
     { hint_term = c; hint_type = cty; hint_uctx = ctx; hint_clnv = cl; }
   in
   let code = match p.code.obj with
@@ -1649,14 +1647,17 @@ let connect_hint_clenv h gl =
     let emap c = Vars.subst_univs_level_constr subst c in
     let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
     (* Only metas are mentioning the old universes. *)
-    {
-      templval = Evd.map_fl emap clenv.templval;
-      templtyp = Evd.map_fl emap clenv.templtyp;
-      evd = Evd.map_metas emap evd;
-      env = Proofview.Goal.env gl;
-    }
+    Clenv.mk_clausenv
+      (Proofview.Goal.env gl)
+      (Evd.map_metas emap evd)
+      (Evd.map_fl emap clenv.templval)
+      (Evd.map_fl emap clenv.templtyp)
   | None ->
-    { clenv with evd = evd ; env = Proofview.Goal.env gl }
+    Clenv.mk_clausenv
+      (Proofview.Goal.env gl)
+      evd
+      clenv.templval
+      clenv.templtyp
 
 let fresh_hint env sigma h =
   let { hint_term = c; hint_uctx = ctx } = h in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 130e0e97c2..39c5c9562f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1301,20 +1301,18 @@ let do_replace id = function
 
 let clenv_refine_in ?err with_evars targetid id sigma0 clenv tac =
   let clenv = Clenv.clenv_pose_dependent_evars ~with_evars clenv in
-  let clenv =
-      { clenv with evd = Typeclasses.resolve_typeclasses
-          ~fail:(not with_evars) clenv.env clenv.evd }
-  in
+  let evd = Typeclasses.resolve_typeclasses ~fail:(not with_evars) clenv.env clenv.evd in
+  let clenv = Clenv.update_clenv_evd clenv evd in
   let new_hyp_typ = clenv_type clenv in
   if not with_evars then check_unresolved_evars_of_metas sigma0 clenv;
-  if not with_evars && occur_meta clenv.evd new_hyp_typ then
+  if not with_evars && occur_meta evd new_hyp_typ then
     error_uninstantiated_metas new_hyp_typ clenv;
   let new_hyp_prf = clenv_value clenv in
   let exact_tac = Logic.refiner ~check:false EConstr.Unsafe.(to_constr new_hyp_prf) in
   let naming = NamingMustBe (CAst.make targetid) in
   let with_clear = do_replace (Some id) naming in
   Tacticals.New.tclTHEN
-    (Proofview.Unsafe.tclEVARS (clear_metas clenv.evd))
+    (Proofview.Unsafe.tclEVARS (clear_metas evd))
     (Tacticals.New.tclTHENLAST
       (assert_after_then_gen ?err with_clear naming new_hyp_typ tac) exact_tac)