diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-11 09:06:05 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-11 09:06:05 +0000 |
commit | e79b800bec660dc2724fa70c33f4e435ddbf885c (patch) | |
tree | 79e24c31e9c2319649b7872b1bcb0ad6867afe09 | |
parent | 2484db1991dac3b41d70130cf4c8697cb8c4af9a (diff) |
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
-rw-r--r-- | kernel/mod_subst.ml | 6 | ||||
-rw-r--r-- | kernel/mod_subst.mli | 2 | ||||
-rw-r--r-- | kernel/modops.ml | 57 | ||||
-rw-r--r-- | kernel/safe_typing.ml | 12 | ||||
-rw-r--r-- | kernel/subtyping.ml | 2 | ||||
-rw-r--r-- | library/declare.ml | 12 | ||||
-rw-r--r-- | library/declaremods.ml | 2 | ||||
-rw-r--r-- | library/global.ml | 12 | ||||
-rw-r--r-- | library/global.mli | 4 | ||||
-rw-r--r-- | parsing/prettyp.ml | 4 | ||||
-rw-r--r-- | pretyping/indrec.ml | 3 | ||||
-rw-r--r-- | tactics/equality.ml | 2 | ||||
-rw-r--r-- | toplevel/command.ml | 2 | ||||
-rw-r--r-- | toplevel/search.ml | 4 |
14 files changed, 62 insertions, 62 deletions
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index bf08841c8..275c6e677 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 dd240d7f3..e06cc816d 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 84d8ca67a..967523234 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 e5b8412ec..3c4c50a4a 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 00af99d98..c141a02aa 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' -> diff --git a/library/declare.ml b/library/declare.ml index 906d9aa3c..10dc35b95 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -103,13 +103,13 @@ type constant_declaration = constant_entry * logical_kind let load_constant i ((sp,kn),(_,_,kind)) = if Nametab.exists_cci sp then alreadydeclared (pr_id (basename sp) ++ str " already exists"); - let con = Global.constant_of_delta (constant_of_kn kn) in + let con = Global.constant_of_delta_kn kn in Nametab.push (Nametab.Until i) sp (ConstRef con); add_constant_kind con kind (* Opening means making the name without its module qualification available *) let open_constant i ((sp,kn),_) = - let con = Global.constant_of_delta (constant_of_kn kn) in + let con = Global.constant_of_delta_kn kn in Nametab.push (Nametab.Exactly i) sp (ConstRef con) let exists_name id = @@ -162,7 +162,7 @@ let inConstant = let declare_constant_common id dhyps (cd,kind) = let (sp,kn) = add_leaf id (inConstant (cd,dhyps,kind)) in - let c = Global.constant_of_delta (constant_of_kn kn) in + let c = Global.constant_of_delta_kn kn in declare_constant_implicits c; Heads.declare_head (EvalConstRef c); Notation.declare_ref_arguments_scope (ConstRef c); @@ -184,7 +184,7 @@ let declare_inductive_argument_scopes kn mie = let inductive_names sp kn mie = let (dp,_) = repr_path sp in - let kn = Global.mind_of_delta (mind_of_kn kn) in + let kn = Global.mind_of_delta_kn kn in let names, _ = List.fold_left (fun (names, n) ind -> @@ -225,7 +225,7 @@ let cache_inductive ((sp,kn),(dhyps,mie)) = let discharge_inductive ((sp,kn),(dhyps,mie)) = - let mind = (Global.mind_of_delta (mind_of_kn kn)) in + let mind = Global.mind_of_delta_kn kn in let mie = Global.lookup_mind mind in let repl = replacement_context () in let sechyps = section_segment_of_mutual_inductive mind in @@ -261,7 +261,7 @@ let declare_mind isrecord mie = | ind::_ -> ind.mind_entry_typename | [] -> anomaly "cannot declare an empty list of inductives" in let (sp,kn as oname) = add_leaf id (inInductive ([],mie)) in - let mind = (Global.mind_of_delta (mind_of_kn kn)) in + let mind = Global.mind_of_delta_kn kn in declare_mib_implicits mind; declare_inductive_argument_scopes mind mie; !xml_declare_inductive (isrecord,oname); diff --git a/library/declaremods.ml b/library/declaremods.ml index d4712762a..95d2310ce 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -845,7 +845,7 @@ let declare_module_ interp_modtype interp_modexpr id args res mexpr_o fs = (* Undo the simulated interactive building of the module *) (* and declare the module as a whole *) Summary.unfreeze_summaries fs; - let dir,mp = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in + let mp = mp_of_kn (Lib.make_kn id) in let inl = if inl_expr = None then None else inl_res in (*PLTODO *) let mp_env,resolver = Global.add_module id entry inl in diff --git a/library/global.ml b/library/global.ml index 6548e6537..ab70bb7c3 100644 --- a/library/global.ml +++ b/library/global.ml @@ -119,15 +119,19 @@ let lookup_mind kn = lookup_mind kn (env()) let lookup_module mp = lookup_module mp (env()) let lookup_modtype kn = lookup_modtype kn (env()) -let constant_of_delta con = +let constant_of_delta_kn kn = let resolver,resolver_param = (delta_of_senv !global_env) in + (* TODO : are resolver and resolver_param orthogonal ? + the effect of resolver is lost if resolver_param isn't + trivial at that spot. *) Mod_subst.constant_of_delta resolver_param - (Mod_subst.constant_of_delta resolver con) + (Mod_subst.constant_of_delta_kn resolver kn) -let mind_of_delta mind = +let mind_of_delta_kn kn = let resolver,resolver_param = (delta_of_senv !global_env) in + (* TODO idem *) Mod_subst.mind_of_delta resolver_param - (Mod_subst.mind_of_delta resolver mind) + (Mod_subst.mind_of_delta_kn resolver kn) let exists_label id = exists_label id !global_env diff --git a/library/global.mli b/library/global.mli index 7859c51ef..1a0fabdc8 100644 --- a/library/global.mli +++ b/library/global.mli @@ -85,8 +85,8 @@ val lookup_inductive : inductive -> mutual_inductive_body * one_inductive_body val lookup_mind : mutual_inductive -> mutual_inductive_body val lookup_module : module_path -> module_body val lookup_modtype : module_path -> module_type_body -val constant_of_delta : constant -> constant -val mind_of_delta : mutual_inductive -> mutual_inductive +val constant_of_delta_kn : kernel_name -> constant +val mind_of_delta_kn : kernel_name -> mutual_inductive val exists_label : label -> bool (** Compiled modules *) diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index f530870e9..06d148ec6 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -507,7 +507,7 @@ let print_full_pure_context () = | ((_,kn),Lib.Leaf lobj)::rest -> let pp = match object_tag lobj with | "CONSTANT" -> - let con = Global.constant_of_delta (constant_of_kn kn) in + let con = Global.constant_of_delta_kn kn in let cb = Global.lookup_constant con in let typ = ungeneralized_type_of_constant_type cb.const_type in hov 0 ( @@ -525,7 +525,7 @@ let print_full_pure_context () = pr_lconstr (Declarations.force c)) ++ str "." ++ fnl () ++ fnl () | "INDUCTIVE" -> - let mind = Global.mind_of_delta (mind_of_kn kn) in + let mind = Global.mind_of_delta_kn kn in let mib = Global.lookup_mind mind in pr_mutual_inductive_body (Global.env()) mind mib ++ str "." ++ fnl () ++ fnl () diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index e1da61908..b875912fc 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -559,8 +559,7 @@ let lookup_eliminator ind_sp s = (* Try first to get an eliminator defined in the same section as the *) (* inductive type *) try - let cst =Global.constant_of_delta - (make_con mp dp (label_of_id id)) in + let cst =Global.constant_of_delta_kn (make_kn mp dp (label_of_id id)) in let _ = Global.lookup_constant cst in mkConst cst with Not_found -> diff --git a/tactics/equality.ml b/tactics/equality.ml index de2a0dacf..d21d3e767 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -251,7 +251,7 @@ let find_elim hdcncl lft2rgt dep cls args gl = let c1 = destConst pr1 in let mp,dp,l = repr_con (constant_of_kn (canonical_con c1)) in let l' = label_of_id (add_suffix (id_of_label l) "_r") in - let c1' = Global.constant_of_delta (make_con mp dp l') in + let c1' = Global.constant_of_delta_kn (make_kn mp dp l') in begin try let _ = Global.lookup_constant c1' in diff --git a/toplevel/command.ml b/toplevel/command.ml index 90376a431..e85c4299b 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -332,7 +332,7 @@ let extract_mutual_inductive_declaration_components indl = let declare_mutual_inductive_with_eliminations isrecord mie impls = let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in let (_,kn) = declare_mind isrecord mie in - let mind = Global.mind_of_delta (mind_of_kn kn) in + let mind = Global.mind_of_delta_kn kn in list_iter_i (fun i (indimpls, constrimpls) -> let ind = (mind,i) in Autoinstance.search_declaration (IndRef ind); diff --git a/toplevel/search.ml b/toplevel/search.ml index 7b5d770d2..33e8e51db 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -65,14 +65,14 @@ let gen_crible refopt (fn : global_reference -> env -> constr -> unit) = fn (VarRef id) env typ with Not_found -> (* we are in a section *) ()) | "CONSTANT" -> - let cst = Global.constant_of_delta(constant_of_kn kn) in + let cst = Global.constant_of_delta_kn kn in let typ = Typeops.type_of_constant env cst in if refopt = None || head_const typ = constr_of_global (Option.get refopt) then fn (ConstRef cst) env typ | "INDUCTIVE" -> - let mind = Global.mind_of_delta(mind_of_kn kn) in + let mind = Global.mind_of_delta_kn kn in let mib = Global.lookup_mind mind in (match refopt with | Some (IndRef ((kn',tyi) as ind)) when eq_mind mind kn' -> |