diff options
| -rw-r--r-- | pretyping/reductionops.ml | 55 | ||||
| -rw-r--r-- | pretyping/reductionops.mli | 6 | ||||
| -rw-r--r-- | pretyping/typing.ml | 2 | ||||
| -rw-r--r-- | proofs/clenv.ml | 8 |
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 |