Cache meta access in meta_instance.

4 files changed, 48 insertions, 23 deletions

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 3352bfce38..ac6bb52a2f 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1192,11 +1192,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
@@ -1205,7 +1209,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
@@ -1216,12 +1220,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:
@@ -1423,23 +1426,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 d404a7e414..b5471eff34 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -273,7 +273,11 @@ val whd_betaiota_deltazeta_for_iota_state :
   TransparentState.t -> Environ.env -> Evd.evar_map -> state -> state
 
 (** {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..f47ed0fc4b 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -42,10 +42,10 @@ type clausenv = {
 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_term clenv c = meta_instance clenv.env (create_meta_instance_subst 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_value clenv = meta_instance clenv.env (create_meta_instance_subst clenv.evd) clenv.templval
+let clenv_type clenv = meta_instance clenv.env (create_meta_instance_subst clenv.evd) clenv.templtyp
 
 let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t
 
@@ -203,7 +203,7 @@ let clenv_assign mv rhs clenv =
 *)
 
 let clenv_metas_in_type_of_meta env evd mv =
-  (mk_freelisted (meta_instance env evd (meta_ftype evd mv))).freemetas
+  (mk_freelisted (meta_instance env (create_meta_instance_subst evd) (meta_ftype evd mv))).freemetas
 
 let dependent_in_type_of_metas clenv mvs =
   List.fold_right