diff options
| -rw-r--r-- | kernel/declarations.ml | 2 | ||||
| -rw-r--r-- | kernel/mod_subst.ml | 34 | ||||
| -rw-r--r-- | kernel/mod_subst.mli | 2 |
3 files changed, 24 insertions, 14 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 282dad0da..fc8064d59 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -210,7 +210,7 @@ type mutual_inductive_body = { } let subst_arity sub arity = - if sub = empty_subst then arity + if is_empty_subst sub then arity else match arity with | NonPolymorphicType s -> NonPolymorphicType (subst_mps sub s) | PolymorphicArity (ctx,s) -> PolymorphicArity (subst_rel_context sub ctx,s) diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index f15bc1a77..6a7ecc442 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -57,6 +57,7 @@ module MBImap = Map.Make module Umap = struct type 'a t = 'a MPmap.t * 'a MBImap.t let empty = MPmap.empty, MBImap.empty + let is_empty (m1,m2) = MPmap.is_empty m1 && MBImap.is_empty m2 let add_mbi mbi x (m1,m2) = (m1,MBImap.add mbi x m2) let add_mp mp x (m1,m2) = (MPmap.add mp x m1, m2) let find_mp mp map = MPmap.find mp (fst map) @@ -73,6 +74,8 @@ type substitution = (module_path * delta_resolver) Umap.t let empty_subst = Umap.empty +let is_empty_subst = Umap.is_empty + let add_mbid mbid mp resolve = Umap.add_mbi mbid (mp,resolve) let add_mp mp1 mp2 resolve = Umap.add_mp mp1 (mp2,resolve) @@ -282,21 +285,25 @@ let subst_ind sub mind = | Canonical -> mind_of_delta2 resolve mind' with No_subst -> mind -let subst_con sub con = +let subst_con0 sub con = let kn1,kn2 = user_con con,canonical_con con in let mp1,dir,l = repr_kn kn1 in let mp2,_,_ = repr_kn kn2 in let rebuild_con mp1 mp2 = make_con_equiv mp1 mp2 dir l in let dup con = con, mkConst con in - try - let side,con',resolve = gen_subst_mp rebuild_con sub mp1 mp2 in - match constant_of_delta_with_inline resolve con' with - | Some t -> con', t - | None -> - match side with - | User -> dup (constant_of_delta resolve con') - | Canonical -> dup (constant_of_delta2 resolve con') - with No_subst -> dup con + let side,con',resolve = gen_subst_mp rebuild_con sub mp1 mp2 in + match constant_of_delta_with_inline resolve con' with + | Some t -> con', t + | None -> + let con'' = match side with + | User -> constant_of_delta resolve con' + | Canonical -> constant_of_delta2 resolve con' + in + if con'' == con then raise No_subst else dup con'' + +let subst_con sub con = + try subst_con0 sub con + with No_subst -> con, mkConst con (* Here the semantics is completely unclear. What does "Hint Unfold t" means when "t" is a parameter? @@ -310,7 +317,7 @@ let subst_evaluable_reference subst = function let rec map_kn f f' c = let func = map_kn f f' in match kind_of_term c with - | Const kn -> f' kn + | Const kn -> (try snd (f' kn) with No_subst -> c) | Ind (kn,i) -> let kn' = f kn in if kn'==kn then c else mkInd (kn',i) @@ -373,8 +380,9 @@ let rec map_kn f f' c = else mkCoFix (ln,(lna,tl',bl')) | _ -> c -let subst_mps sub = - map_kn (subst_ind sub) (fun con -> snd (subst_con sub con)) +let subst_mps sub c = + if is_empty_subst sub then c + else map_kn (subst_ind sub) (subst_con0 sub) c let rec replace_mp_in_mp mpfrom mpto mp = match mp with diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index 91139985b..f9b76e6ee 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -68,6 +68,8 @@ val mind_in_delta : mutual_inductive -> delta_resolver -> bool val empty_subst : substitution +val is_empty_subst : substitution -> bool + (** add_* add [arg2/arg1]\{arg3\} to the substitution with no sequential composition *) val add_mbid : |