aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/mod_subst.ml6
-rw-r--r--kernel/mod_subst.mli2
-rw-r--r--kernel/modops.ml57
-rw-r--r--kernel/safe_typing.ml12
-rw-r--r--kernel/subtyping.ml2
-rw-r--r--library/declare.ml12
-rw-r--r--library/declaremods.ml2
-rw-r--r--library/global.ml12
-rw-r--r--library/global.mli4
-rw-r--r--parsing/prettyp.ml4
-rw-r--r--pretyping/indrec.ml3
-rw-r--r--tactics/equality.ml2
-rw-r--r--toplevel/command.ml2
-rw-r--r--toplevel/search.ml4
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' ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 22:00:05 +0000