aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/mod_checking.ml4
-rw-r--r--checker/modops.ml8
-rw-r--r--checker/subtyping.ml4
-rw-r--r--kernel/mod_subst.ml12
-rw-r--r--kernel/modops.ml12
-rw-r--r--kernel/names.ml8
-rw-r--r--kernel/names.mli17
-rw-r--r--kernel/nativecode.ml2
-rw-r--r--kernel/safe_typing.ml6
-rw-r--r--kernel/subtyping.ml8
-rw-r--r--library/globnames.ml4
-rw-r--r--plugins/extraction/common.ml2
-rw-r--r--plugins/extraction/extract_env.ml10
-rw-r--r--plugins/extraction/extraction.ml4
-rw-r--r--plugins/extraction/mlutil.ml3
-rw-r--r--plugins/extraction/modutil.ml2
-rw-r--r--plugins/extraction/ocaml.ml2
-rw-r--r--plugins/syntax/numbers_syntax.ml2
-rw-r--r--printing/printmod.ml6
19 files changed, 61 insertions, 55 deletions
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 169fa5ca8..bc4ea7c69 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -258,10 +258,10 @@ and check_module env mp mb =
and check_structure_field env mp lab res = function
| SFBconst cb ->
- let c = make_con mp DirPath.empty lab in
+ let c = Constant.make2 mp lab in
check_constant_declaration env c cb
| SFBmind mib ->
- let kn = make_mind mp DirPath.empty lab in
+ let kn = MutInd.make2 mp lab in
let kn = mind_of_delta res kn in
Indtypes.check_inductive env kn mib
| SFBmodule msb ->
diff --git a/checker/modops.ml b/checker/modops.ml
index 38cd09956..13e436a5e 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -67,9 +67,9 @@ let module_body_of_type mp mtb =
let rec add_signature mp sign resolver env =
let add_one env (l,elem) =
- let kn = make_kn mp DirPath.empty l in
- let con = constant_of_kn kn in
- let mind = mind_of_delta resolver (mind_of_kn kn) in
+ let kn = KerName.make2 mp l in
+ let con = Constant.make1 kn in
+ let mind = mind_of_delta resolver (MutInd.make1 kn) in
match elem with
| SFBconst cb ->
(* let con = constant_of_delta resolver con in*)
@@ -97,7 +97,7 @@ let strengthen_const mp_from l cb resolver =
match cb.const_body with
| Def _ -> cb
| _ ->
- let con = make_con mp_from DirPath.empty l in
+ let con = Constant.make2 mp_from l in
(* let con = constant_of_delta resolver con in*)
{ cb with const_body = Def (Declarations.from_val (Const con)) }
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 02006a7ac..d0d18c68c 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -35,7 +35,7 @@ type namedmodule =
constructors *)
let add_mib_nameobjects mp l mib map =
- let ind = make_mind mp DirPath.empty l in
+ let ind = MutInd.make2 mp l in
let add_mip_nameobjects j oib map =
let ip = (ind,j) in
let map =
@@ -83,7 +83,7 @@ let check_conv_error error f env a1 a2 =
(* for now we do not allow reorderings *)
let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2=
- let kn = make_mind mp1 DirPath.empty l in
+ let kn = MutInd.make2 mp1 l in
let error () = error_not_match l spec2 in
let check_conv f = check_conv_error error f in
let mib1 =
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 6d558bf3c..731475fb4 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -190,16 +190,16 @@ let kn_of_deltas resolve1 resolve2 kn =
if kn' == kn then kn_of_delta resolve2 kn else kn'
let constant_of_delta_kn resolve kn =
- Constant.make2 kn (kn_of_delta resolve kn)
+ Constant.make kn (kn_of_delta resolve kn)
let constant_of_deltas_kn resolve1 resolve2 kn =
- Constant.make2 kn (kn_of_deltas resolve1 resolve2 kn)
+ Constant.make kn (kn_of_deltas resolve1 resolve2 kn)
let mind_of_delta_kn resolve kn =
- MutInd.make2 kn (kn_of_delta resolve kn)
+ MutInd.make kn (kn_of_delta resolve kn)
let mind_of_deltas_kn resolve1 resolve2 kn =
- MutInd.make2 kn (kn_of_deltas resolve1 resolve2 kn)
+ MutInd.make kn (kn_of_deltas resolve1 resolve2 kn)
let inline_of_delta inline resolver =
match inline with
@@ -288,7 +288,7 @@ let subst_ind sub mind =
let knc' =
progress (kn_of_delta resolve) (if user then knu else knc) ~orelse:knc
in
- MutInd.make2 knu knc'
+ MutInd.make knu knc'
with No_subst -> mind
let subst_con0 sub cst =
@@ -305,7 +305,7 @@ let subst_con0 sub cst =
let knc' =
progress (kn_of_delta resolve) (if user then knu else knc) ~orelse:knc
in
- let cst' = Constant.make2 knu knc' in
+ let cst' = Constant.make knu knc' in
cst', mkConst cst'
let subst_con sub cst =
diff --git a/kernel/modops.ml b/kernel/modops.ml
index d07bacdf0..986118655 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -259,7 +259,7 @@ let add_retroknowledge mp =
let rec add_signature mp sign resolver env =
let add_one env (l,elem) =
- let kn = make_kn mp DirPath.empty l in
+ let kn = KerName.make2 mp l in
match elem with
| SFBconst cb ->
Environ.add_constant (constant_of_delta_kn resolver kn) cb env
@@ -284,7 +284,7 @@ let strengthen_const mp_from l cb resolver =
match cb.const_body with
| Def _ -> cb
| _ ->
- let kn = make_kn mp_from DirPath.empty l in
+ let kn = KerName.make2 mp_from l in
let con = constant_of_delta_kn resolver kn in
{ cb with
const_body = Def (Declarations.from_val (mkConst con));
@@ -429,8 +429,8 @@ and strengthen_and_subst_struct
(* 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 kn_from = make_kn mp_from DirPath.empty l in
- let kn_to = make_kn mp_to DirPath.empty l in
+ let kn_from = KerName.make2 mp_from l in
+ let kn_to = KerName.make2 mp_to l in
let old_name = kn_of_delta resolver kn_from in
(add_kn_delta_resolver kn_to old_name resolve_out),
item'::rest'
@@ -446,8 +446,8 @@ and strengthen_and_subst_struct
strengthen_and_subst_struct rest subst
mp_alias mp_from mp_to alias incl resolver in
if incl then
- let kn_from = make_kn mp_from DirPath.empty l in
- let kn_to = make_kn mp_to DirPath.empty l in
+ let kn_from = KerName.make2 mp_from l in
+ let kn_to = KerName.make2 mp_to l in
let old_name = kn_of_delta resolver kn_from in
(add_kn_delta_resolver kn_to old_name resolve_out),
item'::rest'
diff --git a/kernel/names.ml b/kernel/names.ml
index 7e7a048e9..976415e37 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -323,6 +323,8 @@ module KerName = struct
let make mp dir l = (mp,dir,l)
let repr kn = kn
+ let make2 mp l = (mp,DirPath.empty,l)
+
let modpath (mp,_,_) = mp
let label (_,_,l) = l
@@ -409,7 +411,7 @@ module KerPair = struct
let make knu knc = if knu == knc then Same knc else Dual (knu,knc)
let make1 = same
- let make2 = make
+ let make2 mp l = same (KerName.make2 mp l)
let make3 mp dir l = same (KerName.make mp dir l)
let repr3 kp = KerName.repr (user kp)
let label kp = KerName.label (user kp)
@@ -701,7 +703,7 @@ let kn_equal = KerName.equal
type constant = Constant.t
let constant_of_kn = Constant.make1
-let constant_of_kn_equiv = Constant.make2
+let constant_of_kn_equiv = Constant.make
let make_con = Constant.make3
let repr_con = Constant.repr3
let canonical_con = Constant.canonical
@@ -721,7 +723,7 @@ let con_with_label = Constant.change_label
type mutual_inductive = MutInd.t
let mind_of_kn = MutInd.make1
-let mind_of_kn_equiv = MutInd.make2
+let mind_of_kn_equiv = MutInd.make
let make_mind = MutInd.make3
let canonical_mind = MutInd.canonical
let user_mind = MutInd.user
diff --git a/kernel/names.mli b/kernel/names.mli
index 8181daa22..77d5ce8e6 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -207,6 +207,7 @@ sig
(** Constructor and destructor *)
val make : ModPath.t -> DirPath.t -> Label.t -> t
+ val make2 : ModPath.t -> Label.t -> t
val repr : t -> ModPath.t * DirPath.t * Label.t
(** Projections *)
@@ -235,11 +236,14 @@ sig
(** Constructors *)
- val make2 : KerName.t -> KerName.t -> t
+ val make : KerName.t -> KerName.t -> t
(** Builds a constant name from a user and a canonical kernel name. *)
val make1 : KerName.t -> t
- (** Special case of [make2] where the user name is canonical. *)
+ (** Special case of [make] where the user name is canonical. *)
+
+ val make2 : ModPath.t -> Label.t -> t
+ (** Shortcut for [(make1 (KerName.make2 ...))] *)
val make3 : ModPath.t -> DirPath.t -> Label.t -> t
(** Shortcut for [(make1 (KerName.make ...))] *)
@@ -301,11 +305,14 @@ sig
(** Constructors *)
- val make2 : KerName.t -> KerName.t -> t
+ val make : KerName.t -> KerName.t -> t
(** Builds a mutual inductive name from a user and a canonical kernel name. *)
val make1 : KerName.t -> t
- (** Special case of [make2] where the user name is canonical. *)
+ (** Special case of [make] where the user name is canonical. *)
+
+ val make2 : ModPath.t -> Label.t -> t
+ (** Shortcut for [(make1 (KerName.make2 ...))] *)
val make3 : ModPath.t -> DirPath.t -> Label.t -> t
(** Shortcut for [(make1 (KerName.make ...))] *)
@@ -595,7 +602,7 @@ type constant = Constant.t
(** @deprecated Alias type *)
val constant_of_kn_equiv : KerName.t -> KerName.t -> constant
-(** @deprecated Same as [Constant.make2] *)
+(** @deprecated Same as [Constant.make] *)
val constant_of_kn : KerName.t -> constant
(** @deprecated Same as [Constant.make1] *)
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 04a063044..7b878c53e 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1440,7 +1440,7 @@ let compile_constant_field env prefix con (code, symb, (mupds, cupds)) cb =
gl@code, !symbols_list, (mupds, cupds)
let compile_mind_field prefix mp l (code, symb, (mupds, cupds)) mb =
- let mind = make_mind mp empty_dirpath l in
+ let mind = MutInd.make2 mp l in
reset_symbols_list symb;
let code, upd = compile_mind prefix mb mind code in
let mupds = Mindmap_env.add mind upd mupds in
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index a591fb433..8a9822b18 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -482,11 +482,9 @@ let end_module l restype senv =
let add senv ((l,elem) as field) =
let new_name = match elem with
| SFBconst _ ->
- let kn = make_kn mp_sup DirPath.empty l in
- C (constant_of_delta_kn resolver kn)
+ C (constant_of_delta_kn resolver (KerName.make2 mp_sup l))
| SFBmind _ ->
- let kn = make_kn mp_sup DirPath.empty l in
- I (mind_of_delta_kn resolver kn)
+ I (mind_of_delta_kn resolver (KerName.make2 mp_sup l))
| SFBmodule _ -> M
| SFBmodtype _ -> MT (MPdot(senv.modinfo.modpath, l))
in
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 485b53729..8f46831b8 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -39,7 +39,7 @@ type namedmodule =
constructors *)
let add_mib_nameobjects mp l mib map =
- let ind = make_mind mp DirPath.empty l in
+ let ind = MutInd.make2 mp l in
let add_mip_nameobjects j oib map =
let ip = (ind,j) in
let map =
@@ -88,8 +88,8 @@ let check_conv_error error why cst f env a1 a2 =
(* for now we do not allow reorderings *)
let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2=
- let kn1 = make_kn mp1 DirPath.empty l in
- let kn2 = make_kn mp2 DirPath.empty l in
+ let kn1 = KerName.make2 mp1 l in
+ let kn2 = KerName.make2 mp2 l in
let error why = error_signature_mismatch l spec2 why in
let check_conv why cst f = check_conv_error error why cst f in
let mib1 =
@@ -180,7 +180,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
let kn2' = kn_of_delta reso2 kn2 in
if KerName.equal kn2 kn2' ||
MutInd.equal (mind_of_delta_kn reso1 kn1)
- (subst_ind subst2 (MutInd.make2 kn2 kn2'))
+ (subst_ind subst2 (MutInd.make kn2 kn2'))
then ()
else error NotEqualInductiveAliases
end;
diff --git a/library/globnames.ml b/library/globnames.ml
index 50c91cc05..a04cdea8c 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -138,9 +138,9 @@ let constr_of_global_or_constr = function
(** {6 Temporary function to brutally form kernel names from section paths } *)
-let encode_mind dir id = make_mind (MPfile dir) DirPath.empty (Label.of_id id)
+let encode_mind dir id = MutInd.make2 (MPfile dir) (Label.of_id id)
-let encode_con dir id = make_con (MPfile dir) DirPath.empty (Label.of_id id)
+let encode_con dir id = Constant.make2 (MPfile dir) (Label.of_id id)
let check_empty_section dp =
if not (DirPath.is_empty dp) then
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 073f77403..86ea93294 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -584,7 +584,7 @@ let pp_module mp =
the constants are directly turned into chars *)
let mk_ind path s =
- make_mind (MPfile (dirpath_of_string path)) DirPath.empty (Label.make s)
+ MutInd.make2 (MPfile (dirpath_of_string path)) (Label.make s)
let ind_ascii = mk_ind "Coq.Strings.Ascii" "ascii"
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index e94644821..5aee45dcc 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -219,13 +219,13 @@ let env_for_mtb_with_def env mp seb idl =
let rec extract_sfb_spec env mp = function
| [] -> []
| (l,SFBconst cb) :: msig ->
- let kn = make_con mp DirPath.empty l in
+ let kn = Constant.make2 mp l in
let s = extract_constant_spec env kn cb in
let specs = extract_sfb_spec env mp msig in
if logical_spec s then specs
else begin Visit.add_spec_deps s; (l,Spec s) :: specs end
| (l,SFBmind _) :: msig ->
- let mind = make_mind mp DirPath.empty l in
+ let mind = MutInd.make2 mp l in
let s = Sind (mind, extract_inductive env mind) in
let specs = extract_sfb_spec env mp msig in
if logical_spec s then specs
@@ -288,7 +288,7 @@ let rec extract_sfb env mp all = function
| (l,SFBconst cb) :: msb ->
(try
let vl,recd,msb = factor_fix env l cb msb in
- let vc = Array.map (make_con mp DirPath.empty) vl in
+ let vc = Array.map (Constant.make2 mp) vl in
let ms = extract_sfb env mp all msb in
let b = Array.exists Visit.needed_con vc in
if all || b then
@@ -298,7 +298,7 @@ let rec extract_sfb env mp all = function
else ms
with Impossible ->
let ms = extract_sfb env mp all msb in
- let c = make_con mp DirPath.empty l in
+ let c = Constant.make2 mp l in
let b = Visit.needed_con c in
if all || b then
let d = extract_constant env c cb in
@@ -307,7 +307,7 @@ let rec extract_sfb env mp all = function
else ms)
| (l,SFBmind mib) :: msb ->
let ms = extract_sfb env mp all msb in
- let mind = make_mind mp DirPath.empty l in
+ let mind = MutInd.make2 mp l in
let b = Visit.needed_ind mind in
if all || b then
let d = Dind (mind, extract_inductive env mind) in
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 62ce3f31d..c8f376565 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -442,7 +442,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
List.skipn mib.mind_nparams (names_prod mip0.mind_user_lc.(0)) in
assert (List.length field_names = List.length typ);
let projs = ref Cset.empty in
- let mp,d,_ = repr_mind kn in
+ let mp = MutInd.modpath kn in
let rec select_fields l typs = match l,typs with
| [],[] -> []
| _::l, typ::typs when isDummy (expand env typ) ->
@@ -450,7 +450,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
| Anonymous::l, typ::typs ->
None :: (select_fields l typs)
| Name id::l, typ::typs ->
- let knp = make_con mp d (Label.of_id id) in
+ let knp = Constant.make2 mp (Label.of_id id) in
(* Is it safe to use [id] for projections [foo.id] ? *)
if List.for_all ((=) Keep) (type2signature env typ)
then projs := Cset.add knp !projs;
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 7d95d2e17..8ecd8cd7c 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -1304,9 +1304,8 @@ let inline_test r t =
not (is_fix t2) && ml_size t < 12 && is_not_strict t)
let con_of_string s =
- let null = DirPath.empty in
match DirPath.repr (dirpath_of_string s) with
- | id :: d -> make_con (MPfile (DirPath.make d)) null (Label.of_id id)
+ | id :: d -> Constant.make2 (MPfile (DirPath.make d)) (Label.of_id id)
| [] -> assert false
let manual_inline_set =
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 01234aa18..58186e904 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -34,7 +34,7 @@ let se_iter do_decl do_spec do_mp =
let mp_w =
List.fold_left (fun mp l -> MPdot(mp,Label.of_id l)) mp_mt idl'
in
- let r = ConstRef (make_con mp_w DirPath.empty (Label.of_id l')) in
+ let r = ConstRef (Constant.make2 mp_w (Label.of_id l')) in
mt_iter mt; do_decl (Dtype(r,l,t))
| MTwith (mt,ML_With_module(idl,mp))->
let mp_mt = msid_of_mt mt in
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index dfa5ff6f9..6c3054e2c 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -650,7 +650,7 @@ and pp_module_type params = function
let mp_w =
List.fold_left (fun mp l -> MPdot(mp,Label.of_id l)) mp_mt idl'
in
- let r = ConstRef (make_con mp_w DirPath.empty (Label.of_id l)) in
+ let r = ConstRef (Constant.make2 mp_w (Label.of_id l)) in
push_visible mp_mt [];
let pp_w = str " with type " ++ ids ++ pp_global Type r in
pop_visible();
diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml
index 8d3629d35..1cce6cd70 100644
--- a/plugins/syntax/numbers_syntax.ml
+++ b/plugins/syntax/numbers_syntax.ml
@@ -18,7 +18,7 @@ open Glob_term
let make_dir l = DirPath.make (List.rev_map Id.of_string l)
let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
-let make_mind mp id = Names.make_mind mp DirPath.empty (Label.make id)
+let make_mind mp id = Names.MutInd.make2 mp (Label.make id)
let make_mind_mpfile dir id = make_mind (MPfile (make_dir dir)) id
let make_mind_mpdot dir modname id =
let mp = MPdot (MPfile (make_dir dir), Label.make modname)
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 0b8393d52..07a5d954c 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -90,9 +90,9 @@ let nametab_register_body mp fp (l,body) =
| SFBmodule _ -> () (* TODO *)
| SFBmodtype _ -> () (* TODO *)
| SFBconst _ ->
- push (Label.to_id l) (ConstRef (make_con mp DirPath.empty l))
+ push (Label.to_id l) (ConstRef (Constant.make2 mp l))
| SFBmind mib ->
- let mind = make_mind mp DirPath.empty l in
+ let mind = MutInd.make2 mp l in
Array.iteri
(fun i mip ->
push mip.mind_typename (IndRef (mind,i));
@@ -126,7 +126,7 @@ let print_body is_impl env mp (l,body) =
| SFBmind mib ->
try
let env = Option.get env in
- Printer.pr_mutual_inductive_body env (make_mind mp DirPath.empty l) mib
+ Printer.pr_mutual_inductive_body env (MutInd.make2 mp l) mib
with _ ->
(if mib.mind_finite then str "Inductive " else str "CoInductive")
++ name)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 03:52:44 +0000