From e79b800bec660dc2724fa70c33f4e435ddbf885c Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 11 Oct 2011 09:06:05 +0000 Subject: Various simplifications about constant_of_delta and mind_of_delta Most of the time, a constant name is built from: - a kernel_name for its user part - a delta_resolver applied to this kernel_name for its canonical part With this patch we avoid building unnecessary constants for immediately amending them (cf in particular the awkward code removed in safe_typing). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14545 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/mod_subst.ml | 6 ++++++ kernel/mod_subst.mli | 2 ++ kernel/modops.ml | 57 ++++++++++++++++++++++++--------------------------- kernel/safe_typing.ml | 12 ++--------- kernel/subtyping.ml | 2 +- 5 files changed, 38 insertions(+), 41 deletions(-) (limited to 'kernel') diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index bf08841c83..275c6e6775 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -147,6 +147,9 @@ let gen_of_delta resolve x kn fix_can = if kn == new_kn then x else fix_can new_kn with _ -> x +let constant_of_delta_kn resolve kn = + gen_of_delta resolve (constant_of_kn kn) kn (constant_of_kn_equiv kn) + let constant_of_delta resolve con = let kn = user_con con in gen_of_delta resolve con kn (constant_of_kn_equiv kn) @@ -155,6 +158,9 @@ let constant_of_delta2 resolve con = let kn, kn' = canonical_con con, user_con con in gen_of_delta resolve con kn (constant_of_kn_equiv kn') +let mind_of_delta_kn resolve kn = + gen_of_delta resolve (mind_of_kn kn) kn (mind_of_kn_equiv kn) + let mind_of_delta resolve mind = let kn = user_mind mind in gen_of_delta resolve mind kn (mind_of_kn_equiv kn) diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index dd240d7f31..e06cc816da 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -44,8 +44,10 @@ val subst_dom_codom_delta_resolver : substitution -> delta_resolver -> delta_resolver (** *_of_delta return the associated name of arg2 in arg1 *) +val constant_of_delta_kn : delta_resolver -> kernel_name -> constant val constant_of_delta : delta_resolver -> constant -> constant +val mind_of_delta_kn : delta_resolver -> kernel_name -> mutual_inductive val mind_of_delta : delta_resolver -> mutual_inductive -> mutual_inductive val delta_of_mp : delta_resolver -> module_path -> module_path diff --git a/kernel/modops.ml b/kernel/modops.ml index 84d8ca67ab..967523234e 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -264,18 +264,13 @@ let add_retroknowledge mp = let rec add_signature mp sign resolver env = let add_one env (l,elem) = let kn = make_kn mp empty_dirpath l in - let con = constant_of_kn kn in - let mind = mind_of_kn kn in - match elem with - | SFBconst cb -> - let con = constant_of_delta resolver con in - Environ.add_constant con cb env - | SFBmind mib -> - let mind = mind_of_delta resolver mind in - Environ.add_mind mind mib env - | SFBmodule mb -> add_module mb env - (* adds components as well *) - | SFBmodtype mtb -> Environ.add_modtype mtb.typ_mp mtb env + match elem with + | SFBconst cb -> + Environ.add_constant (constant_of_delta_kn resolver kn) cb env + | SFBmind mib -> + Environ.add_mind (mind_of_delta_kn resolver kn) mib env + | SFBmodule mb -> add_module mb env (* adds components as well *) + | SFBmodtype mtb -> Environ.add_modtype mtb.typ_mp mtb env in List.fold_left add_one env sign @@ -293,8 +288,8 @@ let strengthen_const mp_from l cb resolver = match cb.const_body with | Def _ -> cb | _ -> - let con = make_con mp_from empty_dirpath l in - let con = constant_of_delta resolver con in + let kn = make_kn mp_from empty_dirpath l in + let con = constant_of_delta_kn resolver kn in { cb with const_body = Def (Declarations.from_val (mkConst con)); const_body_code = Cemitcodes.from_val (Cbytegen.compile_alias con) @@ -379,10 +374,9 @@ let inline_delta_resolver env inl mp mbid mtb delta = | [] -> delta | (lev,kn)::r -> let kn = replace_mp_in_kn (MPbound mbid) mp kn in - let con = constant_of_kn kn in - let con' = constant_of_delta delta con in + let con = constant_of_delta_kn delta kn in try - let constant = lookup_constant con' env in + let constant = lookup_constant con env in let l = make_inline delta r in match constant.const_body with | Undef _ | OpaqueDef _ -> l @@ -432,17 +426,18 @@ and strengthen_and_subst_struct l,SFBconst (strengthen_const mp_from l (subst_const_body subst cb) resolver) in - let con = make_con mp_from empty_dirpath l in let resolve_out,rest' = strengthen_and_subst_struct rest subst mp_alias mp_from mp_to alias incl resolver in - if incl then + if incl then (* If we are performing an inclusion we need to add the fact that the constant mp_to.l is \Delta-equivalent to resolver(mp_from.l) *) - let old_name = constant_of_delta resolver con in - (add_constant_delta_resolver - (constant_of_kn_equiv (make_kn mp_to empty_dirpath l) (canonical_con old_name)) + let kn_from = make_kn mp_from empty_dirpath l in + let kn_to = make_kn mp_to empty_dirpath l in + let old_name = constant_of_delta_kn resolver kn_from in + (add_constant_delta_resolver + (constant_of_kn_equiv kn_to (canonical_con old_name)) resolve_out), item'::rest' else @@ -453,17 +448,19 @@ and strengthen_and_subst_struct | (l,SFBmind mib) :: rest -> (*Same as constant*) let item' = l,SFBmind (subst_mind subst mib) in - let mind = make_mind mp_from empty_dirpath l in let resolve_out,rest' = strengthen_and_subst_struct rest subst mp_alias mp_from mp_to alias incl resolver in - if incl then - let old_name = mind_of_delta resolver mind in - (add_mind_delta_resolver - (mind_of_kn_equiv (make_kn mp_to empty_dirpath l) (canonical_mind old_name)) resolve_out), - item'::rest' - else - resolve_out,item'::rest' + if incl then + let kn_from = make_kn mp_from empty_dirpath l in + let kn_to = make_kn mp_to empty_dirpath l in + let old_name = mind_of_delta_kn resolver kn_from in + (add_mind_delta_resolver + (mind_of_kn_equiv kn_to (canonical_mind old_name)) + resolve_out), + item'::rest' + else + resolve_out,item'::rest' | (l,SFBmodule mb) :: rest -> let mp_from' = MPdot (mp_from,l) in let mp_to' = MPdot(mp_to,l) in diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index e5b8412ec0..3c4c50a4ae 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -475,18 +475,10 @@ let end_module l restype senv = let new_name = match elem with | SFBconst _ -> let kn = make_kn mp_sup empty_dirpath l in - let con = constant_of_kn_equiv kn - (canonical_con - (constant_of_delta resolver (constant_of_kn kn))) - in - C con + C (constant_of_delta_kn resolver kn) | SFBmind _ -> let kn = make_kn mp_sup empty_dirpath l in - let mind = mind_of_kn_equiv kn - (canonical_mind - (mind_of_delta resolver (mind_of_kn kn))) - in - I mind + I (mind_of_delta_kn resolver kn) | SFBmodule _ -> M | SFBmodtype _ -> MT (MPdot(senv.modinfo.modpath, l)) in diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 00af99d980..c141a02aa3 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -163,7 +163,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 (* the inductive types and constructors types have to be convertible *) check (fun mib -> mib.mind_nparams) (fun x -> InductiveParamsNumberField x); - begin + begin match mind_of_delta reso2 kn2 with | kn2' when kn2=kn2' -> () | kn2' -> -- cgit v1.2.3