diff options
| -rw-r--r-- | checker/declarations.ml | 10 | ||||
| -rw-r--r-- | kernel/mod_subst.ml | 40 | ||||
| -rw-r--r-- | kernel/names.ml | 184 | ||||
| -rw-r--r-- | kernel/names.mli | 293 | ||||
| -rw-r--r-- | kernel/subtyping.ml | 4 | ||||
| -rw-r--r-- | plugins/extraction/table.ml | 26 |
6 files changed, 372 insertions, 185 deletions
diff --git a/checker/declarations.ml b/checker/declarations.ml index 529f08cb1..2ff570a4a 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -223,6 +223,11 @@ let gen_subst_mp f sub mp1 mp2 = | None, Some (mp',resolve) -> Canonical, (f mp1 mp'), resolve | Some (mp1',_), Some (mp2',resolve2) -> Canonical, (f mp1' mp2'), resolve2 +let make_mind_equiv mpu mpc dir l = + let knu = make_kn mpu dir l in + if mpu == mpc then mind_of_kn knu + else mind_of_kn_equiv knu (make_kn mpc dir l) + let subst_ind sub mind = let kn1,kn2 = user_mind mind, canonical_mind mind in let mp1,dir,l = repr_kn kn1 in @@ -235,6 +240,11 @@ let subst_ind sub mind = | Canonical -> mind_of_delta2 resolve mind' with No_subst -> mind +let make_con_equiv mpu mpc dir l = + let knu = make_kn mpu dir l in + if mpu == mpc then constant_of_kn knu + else constant_of_kn_equiv knu (make_kn mpc dir l) + let subst_con0 sub con = let kn1,kn2 = user_con con,canonical_con con in let mp1,dir,l = repr_kn kn1 in diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 65052d0ed..6d558bf3c 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -146,8 +146,8 @@ let kn_in_delta kn resolver = | Inline _ -> false with Not_found -> false -let con_in_delta con resolver = kn_in_delta (user_con con) resolver -let mind_in_delta mind resolver = kn_in_delta (user_mind mind) resolver +let con_in_delta con resolver = kn_in_delta (Constant.user con) resolver +let mind_in_delta mind resolver = kn_in_delta (MutInd.user mind) resolver let mp_of_delta resolve mp = try Deltamap.find_mp mp resolve with Not_found -> mp @@ -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_of_kn_equiv kn (kn_of_delta resolve kn) + Constant.make2 kn (kn_of_delta resolve kn) let constant_of_deltas_kn resolve1 resolve2 kn = - constant_of_kn_equiv kn (kn_of_deltas resolve1 resolve2 kn) + Constant.make2 kn (kn_of_deltas resolve1 resolve2 kn) let mind_of_delta_kn resolve kn = - mind_of_kn_equiv kn (kn_of_delta resolve kn) + MutInd.make2 kn (kn_of_delta resolve kn) let mind_of_deltas_kn resolve1 resolve2 kn = - mind_of_kn_equiv kn (kn_of_deltas resolve1 resolve2 kn) + MutInd.make2 kn (kn_of_deltas resolve1 resolve2 kn) let inline_of_delta inline resolver = match inline with @@ -279,8 +279,8 @@ let progress f x ~orelse = if y != x then y else orelse let subst_ind sub mind = - let mpu,dir,l = repr_kn (user_mind mind) in - let mpc,_,_ = repr_kn (canonical_mind mind) in + let mpu,dir,l = MutInd.repr3 mind in + let mpc = KerName.modpath (MutInd.canonical mind) in try let mpu,mpc,resolve,user = subst_dual_mp sub mpu mpc in let knu = KerName.make mpu dir l in @@ -288,29 +288,29 @@ let subst_ind sub mind = let knc' = progress (kn_of_delta resolve) (if user then knu else knc) ~orelse:knc in - mind_of_kn_equiv knu knc' + MutInd.make2 knu knc' with No_subst -> mind -let subst_con0 sub con = - let mpu,dir,l = repr_kn (user_con con) in - let mpc,_,_ = repr_kn (canonical_con con) in +let subst_con0 sub cst = + let mpu,dir,l = Constant.repr3 cst in + let mpc = KerName.modpath (Constant.canonical cst) in let mpu,mpc,resolve,user = subst_dual_mp sub mpu mpc in - let knu = make_kn mpu dir l in - let knc = if mpu == mpc then knu else make_kn mpc dir l in + let knu = KerName.make mpu dir l in + let knc = if mpu == mpc then knu else KerName.make mpc dir l in match search_delta_inline resolve knu knc with | Some t -> (* In case of inlining, discard the canonical part (cf #2608) *) - constant_of_kn knu, t + Constant.make1 knu, t | None -> let knc' = progress (kn_of_delta resolve) (if user then knu else knc) ~orelse:knc in - let con' = constant_of_kn_equiv knu knc' in - con', mkConst con' + let cst' = Constant.make2 knu knc' in + cst', mkConst cst' -let subst_con sub con = - try subst_con0 sub con - with No_subst -> con, mkConst con +let subst_con sub cst = + try subst_con0 sub cst + with No_subst -> cst, mkConst cst (* Here the semantics is completely unclear. What does "Hint Unfold t" means when "t" is a parameter? diff --git a/kernel/names.ml b/kernel/names.ml index 8251a85e1..7e7a048e9 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -408,13 +408,32 @@ module KerPair = struct let dual knu knc = Dual (knu,knc) let make knu knc = if knu == knc then Same knc else Dual (knu,knc) + let make1 = same + let make2 = make + 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) + let modpath kp = KerName.modpath (user kp) + + let change_label kp lbl = + let (mp1,dp1,l1) = KerName.repr (user kp) + and (mp2,dp2,l2) = KerName.repr (canonical kp) in + assert (String.equal l1 l2 && DirPath.equal dp1 dp2); + if String.equal lbl l1 then kp + else + let kn = KerName.make mp1 dp1 lbl in + if mp1 == mp2 then same kn + else make kn (KerName.make mp2 dp2 lbl) + + let to_string kp = KerName.to_string (user kp) + let print kp = str (to_string kp) + let debug_to_string = function | Same kn -> "(" ^ KerName.to_string kn ^ ")" | Dual (knu,knc) -> "(" ^ KerName.to_string knu ^ "," ^ KerName.to_string knc ^ ")" - (** Default comparison is on the canonical part *) - let equal x y = x == y || KerName.equal (canonical x) (canonical y) + let debug_print kp = str (debug_to_string kp) (** For ordering kernel pairs, both user or canonical parts may make sense, according to your needs : user for the environments, canonical @@ -423,13 +442,18 @@ module KerPair = struct module UserOrd = struct type t = kernel_pair let compare x y = KerName.compare (user x) (user y) + let equal x y = x == y || KerName.equal (user x) (user y) end module CanOrd = struct type t = kernel_pair let compare x y = KerName.compare (canonical x) (canonical y) + let equal x y = x == y || KerName.equal (canonical x) (canonical y) end + (** Default comparison is on the canonical part *) + let equal = CanOrd.equal + (** Hash-consing : we discriminate only on the user part, since having the same user part implies having the same canonical part (invariant of the system). *) @@ -449,97 +473,45 @@ module KerPair = struct end -(** {6 Constant names } *) - -type constant = KerPair.t - -let canonical_con = KerPair.canonical -let user_con = KerPair.user -let constant_of_kn = KerPair.same -let constant_of_kn_equiv = KerPair.make -let make_con mp dir l = KerPair.same (KerName.make mp dir l) -let make_con_dual mpu mpc dir l = - KerPair.dual (KerName.make mpu dir l) (KerName.make mpc dir l) -let make_con_equiv mpu mpc dir l = - if mpu == mpc then make_con mpc dir l else make_con_dual mpu mpc dir l -let repr_con c = KerName.repr (user_con c) +(** {6 Constant Names} *) -let eq_constant = KerPair.equal -let con_ord = KerPair.CanOrd.compare -let con_user_ord = KerPair.UserOrd.compare +module Constant = KerPair -let con_label cst = KerName.label (user_con cst) -let con_modpath cst = KerName.modpath (user_con cst) +module Cmap = Map.Make(Constant.CanOrd) +module Cmap_env = Map.Make(Constant.UserOrd) +module Cpred = Predicate.Make(Constant.CanOrd) +module Cset = Set.Make(Constant.CanOrd) +module Cset_env = Set.Make(Constant.UserOrd) -let string_of_con cst = KerName.to_string (canonical_con cst) -let pr_con cst = str (string_of_con cst) -let debug_string_of_con = KerPair.debug_to_string -let debug_pr_con cst = str (debug_string_of_con cst) - -let con_with_label cst lbl = - let (mp1,dp1,l1) = KerName.repr (user_con cst) - and (mp2,dp2,l2) = KerName.repr (canonical_con cst) in - assert (String.equal l1 l2 && DirPath.equal dp1 dp2); - if String.equal lbl l1 - then cst - else make_con_equiv mp1 mp2 dp1 lbl - -module Cmap = Map.Make(KerPair.CanOrd) -module Cmap_env = Map.Make(KerPair.UserOrd) -module Cpred = Predicate.Make(KerPair.CanOrd) -module Cset = Set.Make(KerPair.CanOrd) -module Cset_env = Set.Make(KerPair.UserOrd) +(** {6 Names of mutual inductive types } *) +module MutInd = KerPair -(** {6 Names of mutual inductive types } *) +module Mindmap = Map.Make(MutInd.CanOrd) +module Mindset = Set.Make(MutInd.CanOrd) +module Mindmap_env = Map.Make(MutInd.UserOrd) -(** The same thing is done for mutual inductive names - it replaces also the old mind_equiv field of mutual - inductive types *) (** Beware: first inductive has index 0 *) (** Beware: first constructor has index 1 *) -type mutual_inductive = KerPair.t -type inductive = mutual_inductive * int +type inductive = MutInd.t * int type constructor = inductive * int -let mind_modpath mind = KerName.modpath (KerPair.user mind) -let ind_modpath ind = mind_modpath (fst ind) -let constr_modpath c = ind_modpath (fst c) - -let mind_of_kn = KerPair.same -let mind_of_kn_equiv = KerPair.make -let make_mind mp dir l = KerPair.same (KerName.make mp dir l) -let make_mind_dual mpu mpc dir l = - KerPair.dual (KerName.make mpu dir l) (KerName.make mpc dir l) -let make_mind_equiv mpu mpc dir l = - if mpu == mpc then make_mind mpu dir l else make_mind_dual mpu mpc dir l -let canonical_mind = KerPair.canonical -let user_mind = KerPair.user -let repr_mind mind = KerName.repr (user_mind mind) -let mind_label mind = KerName.label (user_mind mind) - -let eq_mind = KerPair.equal -let mind_ord = KerPair.CanOrd.compare -let mind_user_ord = KerPair.UserOrd.compare - -let string_of_mind mind = KerName.to_string (user_mind mind) -let pr_mind mind = str (string_of_mind mind) -let debug_string_of_mind = KerPair.debug_to_string -let debug_pr_mind con = str (debug_string_of_mind con) - -let ith_mutual_inductive (kn, _) i = (kn, i) +let ind_modpath (mind,_) = MutInd.modpath mind +let constr_modpath (ind,_) = ind_modpath ind + +let ith_mutual_inductive (mind, _) i = (mind, i) let ith_constructor_of_inductive ind i = (ind, i) let inductive_of_constructor (ind, i) = ind let index_of_constructor (ind, i) = i -let eq_ind (m1, i1) (m2, i2) = Int.equal i1 i2 && eq_mind m1 m2 +let eq_ind (m1, i1) (m2, i2) = Int.equal i1 i2 && MutInd.equal m1 m2 let ind_ord (m1, i1) (m2, i2) = let c = Int.compare i1 i2 in - if Int.equal c 0 then mind_ord m1 m2 else c + if Int.equal c 0 then MutInd.CanOrd.compare m1 m2 else c let ind_user_ord (m1, i1) (m2, i2) = let c = Int.compare i1 i2 in - if Int.equal c 0 then mind_user_ord m1 m2 else c + if Int.equal c 0 then MutInd.UserOrd.compare m1 m2 else c let eq_constructor (ind1, j1) (ind2, j2) = Int.equal j1 j2 && eq_ind ind1 ind2 let constructor_ord (ind1, j1) (ind2, j2) = @@ -549,10 +521,6 @@ let constructor_user_ord (ind1, j1) (ind2, j2) = let c = Int.compare j1 j2 in if Int.equal c 0 then ind_user_ord ind1 ind2 else c -module Mindmap = Map.Make(KerPair.CanOrd) -module Mindset = Set.Make(KerPair.CanOrd) -module Mindmap_env = Map.Make(KerPair.UserOrd) - module InductiveOrdered = struct type t = inductive let compare = ind_ord @@ -582,10 +550,10 @@ module Constrmap_env = Map.Make(ConstructorOrdered_env) (* Better to have it here that in closure, since used in grammar.cma *) type evaluable_global_reference = | EvalVarRef of Id.t - | EvalConstRef of constant + | EvalConstRef of Constant.t let eq_egr e1 e2 = match e1, e2 with - EvalConstRef con1, EvalConstRef con2 -> eq_constant con1 con2 + EvalConstRef con1, EvalConstRef con2 -> Constant.equal con1 con2 | EvalVarRef id1, EvalVarRef id2 -> Id.equal id1 id2 | _, _ -> false @@ -594,7 +562,7 @@ let eq_egr e1 e2 = match e1, e2 with module Hind = Hashcons.Make( struct type t = inductive - type u = mutual_inductive -> mutual_inductive + type u = MutInd.t -> MutInd.t let hashcons hmind (mind, i) = (hmind mind, i) let equal (mind1,i1) (mind2,i2) = mind1 == mind2 && Int.equal i1 i2 let hash = Hashtbl.hash @@ -609,8 +577,8 @@ module Hconstruct = Hashcons.Make( let hash = Hashtbl.hash end) -let hcons_con = Hashcons.simple_hcons KerPair.HashKP.generate KerName.hcons -let hcons_mind = Hashcons.simple_hcons KerPair.HashKP.generate KerName.hcons +let hcons_con = Hashcons.simple_hcons Constant.HashKP.generate KerName.hcons +let hcons_mind = Hashcons.simple_hcons MutInd.HashKP.generate KerName.hcons let hcons_ind = Hashcons.simple_hcons Hind.generate hcons_mind let hcons_construct = Hashcons.simple_hcons Hconstruct.generate hcons_ind @@ -625,7 +593,7 @@ let var_full_transparent_state = (Id.Pred.full, Cpred.empty) let cst_full_transparent_state = (Id.Pred.empty, Cpred.full) type 'a tableKey = - | ConstKey of constant + | ConstKey of Constant.t | VarKey of Id.t | RelKey of 'a @@ -639,15 +607,17 @@ type id_key = inv_rel_key tableKey let eq_id_key ik1 ik2 = if ik1 == ik2 then true else match ik1,ik2 with - | ConstKey c1, ConstKey c2 -> KerName.equal (user_con c1) (user_con c2) + | ConstKey c1, ConstKey c2 -> Constant.UserOrd.equal c1 c2 | VarKey id1, VarKey id2 -> Id.equal id1 id2 | RelKey k1, RelKey k2 -> Int.equal k1 k2 | _ -> false -let eq_con_chk cst1 cst2 = KerName.equal (user_con cst1) (user_con cst2) -let eq_mind_chk mind1 mind2 = KerName.equal (user_mind mind1) (user_mind mind2) +let eq_con_chk = Constant.UserOrd.equal +let eq_mind_chk = MutInd.UserOrd.equal let eq_ind_chk (kn1,i1) (kn2,i2) = Int.equal i1 i2 && eq_mind_chk kn1 kn2 + +(*******************************************************************) (** Compatibility layers *) (** Backward compatibility for [Id] *) @@ -725,3 +695,43 @@ let string_of_kn = KerName.to_string let pr_kn = KerName.print let kn_ord = KerName.compare let kn_equal = KerName.equal + +(** Compatibility layer for [Constant] *) + +type constant = Constant.t + +let constant_of_kn = Constant.make1 +let constant_of_kn_equiv = Constant.make2 +let make_con = Constant.make3 +let repr_con = Constant.repr3 +let canonical_con = Constant.canonical +let user_con = Constant.user +let con_label = Constant.label +let con_modpath = Constant.modpath +let eq_constant = Constant.equal +let con_ord = Constant.CanOrd.compare +let con_user_ord = Constant.UserOrd.compare +let string_of_con = Constant.to_string +let pr_con = Constant.print +let debug_string_of_con = Constant.debug_to_string +let debug_pr_con = Constant.debug_print +let con_with_label = Constant.change_label + +(** Compatibility layer for [MutInd] *) + +type mutual_inductive = MutInd.t +let mind_of_kn = MutInd.make1 +let mind_of_kn_equiv = MutInd.make2 +let make_mind = MutInd.make3 +let canonical_mind = MutInd.canonical +let user_mind = MutInd.user +let repr_mind = MutInd.repr3 +let mind_label = MutInd.label +let mind_modpath = MutInd.modpath +let eq_mind = MutInd.equal +let mind_ord = MutInd.CanOrd.compare +let mind_user_ord = MutInd.UserOrd.compare +let string_of_mind = MutInd.to_string +let pr_mind = MutInd.print +let debug_string_of_mind = MutInd.debug_to_string +let debug_pr_mind = MutInd.debug_print diff --git a/kernel/names.mli b/kernel/names.mli index e194b3856..8181daa22 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -227,74 +227,141 @@ module KNpred : Predicate.S with type elt = KerName.t module KNmap : Map.S with type key = KerName.t -(** {6 Specific paths for declarations } *) +(** {6 Constant Names } *) -type constant -type mutual_inductive +module Constant: +sig + type t -(** Beware: first inductive has index 0 *) -type inductive = mutual_inductive * int + (** Constructors *) -(** Beware: first constructor has index 1 *) -type constructor = inductive * int + val make2 : 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. *) + + val make3 : ModPath.t -> DirPath.t -> Label.t -> t + (** Shortcut for [(make1 (KerName.make ...))] *) + + (** Projections *) + + val user : t -> KerName.t + val canonical : t -> KerName.t + + val repr3 : t -> ModPath.t * DirPath.t * Label.t + (** Shortcut for [KerName.repr (user ...)] *) + + val modpath : t -> ModPath.t + (** Shortcut for [KerName.modpath (user ...)] *) + + val label : t -> Label.t + (** Shortcut for [KerName.label (user ...)] *) + + (** Comparisons *) + + module CanOrd : sig + val compare : t -> t -> int + val equal : t -> t -> bool + end + + module UserOrd : sig + val compare : t -> t -> int + val equal : t -> t -> bool + end -(** *_env modules consider an order on user part of names + val equal : t -> t -> bool + (** Default comparison, alias for [CanOrd.equal] *) + + val change_label : t -> Label.t -> t + (** Builds a new constant name with a different label *) + + (** Displaying *) + + val to_string : t -> string + val print : t -> Pp.std_ppcmds + val debug_to_string : t -> string + val debug_print : t -> Pp.std_ppcmds + +end + +(** The [*_env] modules consider an order on user part of names the others consider an order on canonical part of names*) -module Cmap : Map.S with type key = constant -module Cmap_env : Map.S with type key = constant -module Cpred : Predicate.S with type elt = constant -module Cset : Set.S with type elt = constant -module Cset_env : Set.S with type elt = constant -module Mindmap : Map.S with type key = mutual_inductive -module Mindmap_env : Map.S with type key = mutual_inductive -module Mindset : Set.S with type elt = mutual_inductive -module Indmap : Map.S with type key = inductive -module Constrmap : Map.S with type key = constructor -module Indmap_env : Map.S with type key = inductive -module Constrmap_env : Map.S with type key = constructor +module Cmap : Map.S with type key = Constant.t +module Cmap_env : Map.S with type key = Constant.t +module Cpred : Predicate.S with type elt = Constant.t +module Cset : Set.S with type elt = Constant.t +module Cset_env : Set.S with type elt = Constant.t -val constant_of_kn : KerName.t -> constant -val constant_of_kn_equiv : KerName.t -> KerName.t -> constant -val make_con : ModPath.t -> DirPath.t -> Label.t -> constant -val make_con_equiv : ModPath.t -> ModPath.t -> DirPath.t - -> Label.t -> constant -val user_con : constant -> KerName.t -val canonical_con : constant -> KerName.t -val repr_con : constant -> ModPath.t * DirPath.t * Label.t -val eq_constant : constant -> constant -> bool -val con_ord : constant -> constant -> int -val con_user_ord : constant -> constant -> int -val con_with_label : constant -> Label.t -> constant +(** {6 Inductive names} *) -val string_of_con : constant -> string -val con_label : constant -> Label.t -val con_modpath : constant -> ModPath.t -val pr_con : constant -> Pp.std_ppcmds -val debug_pr_con : constant -> Pp.std_ppcmds -val debug_string_of_con : constant -> string +module MutInd : +sig + type t + (** Constructors *) + val make2 : KerName.t -> KerName.t -> t + (** Builds a mutual inductive name from a user and a canonical kernel name. *) -val mind_of_kn : KerName.t -> mutual_inductive -val mind_of_kn_equiv : KerName.t -> KerName.t -> mutual_inductive -val make_mind : ModPath.t -> DirPath.t -> Label.t -> mutual_inductive -val make_mind_equiv : ModPath.t -> ModPath.t -> DirPath.t - -> Label.t -> mutual_inductive -val user_mind : mutual_inductive -> KerName.t -val canonical_mind : mutual_inductive -> KerName.t -val repr_mind : mutual_inductive -> ModPath.t * DirPath.t * Label.t -val eq_mind : mutual_inductive -> mutual_inductive -> bool -val mind_ord : mutual_inductive -> mutual_inductive -> int -val mind_user_ord : mutual_inductive -> mutual_inductive -> int + val make1 : KerName.t -> t + (** Special case of [make2] where the user name is canonical. *) -val string_of_mind : mutual_inductive -> string -val mind_label : mutual_inductive -> Label.t -val mind_modpath : mutual_inductive -> ModPath.t -val pr_mind : mutual_inductive -> Pp.std_ppcmds -val debug_pr_mind : mutual_inductive -> Pp.std_ppcmds -val debug_string_of_mind : mutual_inductive -> string + val make3 : ModPath.t -> DirPath.t -> Label.t -> t + (** Shortcut for [(make1 (KerName.make ...))] *) + + (** Projections *) + + val user : t -> KerName.t + val canonical : t -> KerName.t + + val repr3 : t -> ModPath.t * DirPath.t * Label.t + (** Shortcut for [KerName.repr (user ...)] *) + + val modpath : t -> ModPath.t + (** Shortcut for [KerName.modpath (user ...)] *) + + val label : t -> Label.t + (** Shortcut for [KerName.label (user ...)] *) + + (** Comparisons *) + + module CanOrd : sig + val compare : t -> t -> int + val equal : t -> t -> bool + end + + module UserOrd : sig + val compare : t -> t -> int + val equal : t -> t -> bool + end + + val equal : t -> t -> bool + (** Default comparison, alias for [CanOrd.equal] *) + (** Displaying *) + val to_string : t -> string + val print : t -> Pp.std_ppcmds + val debug_to_string : t -> string + val debug_print : t -> Pp.std_ppcmds + +end + +module Mindmap : Map.S with type key = MutInd.t +module Mindmap_env : Map.S with type key = MutInd.t +module Mindset : Set.S with type elt = MutInd.t + +(** Beware: first inductive has index 0 *) +type inductive = MutInd.t * int + +(** Beware: first constructor has index 1 *) +type constructor = inductive * int + +module Indmap : Map.S with type key = inductive +module Constrmap : Map.S with type key = constructor +module Indmap_env : Map.S with type key = inductive +module Constrmap_env : Map.S with type key = constructor val ind_modpath : inductive -> ModPath.t val constr_modpath : constructor -> ModPath.t @@ -313,22 +380,22 @@ val constructor_user_ord : constructor -> constructor -> int (** Better to have it here that in Closure, since required in grammar.cma *) type evaluable_global_reference = | EvalVarRef of Id.t - | EvalConstRef of constant + | EvalConstRef of Constant.t val eq_egr : evaluable_global_reference -> evaluable_global_reference -> bool (** {6 Hash-consing } *) -val hcons_con : constant -> constant -val hcons_mind : mutual_inductive -> mutual_inductive +val hcons_con : Constant.t -> Constant.t +val hcons_mind : MutInd.t -> MutInd.t val hcons_ind : inductive -> inductive val hcons_construct : constructor -> constructor (******) type 'a tableKey = - | ConstKey of constant + | ConstKey of Constant.t | VarKey of Id.t | RelKey of 'a @@ -347,10 +414,9 @@ type id_key = inv_rel_key tableKey val eq_id_key : id_key -> id_key -> bool -(*equalities on constant and inductive - names for the checker*) +(** equalities on constant and inductive names (for the checker) *) -val eq_con_chk : constant -> constant -> bool +val eq_con_chk : Constant.t -> Constant.t -> bool val eq_ind_chk : inductive -> inductive -> bool (** {6 Deprecated functions. For backward compatibility.} *) @@ -522,3 +588,106 @@ val pr_kn : kernel_name -> Pp.std_ppcmds val kn_ord : kernel_name -> kernel_name -> int (** @deprecated Same as [KerName.compare]. *) + +(** {5 Constant names} *) + +type constant = Constant.t +(** @deprecated Alias type *) + +val constant_of_kn_equiv : KerName.t -> KerName.t -> constant +(** @deprecated Same as [Constant.make2] *) + +val constant_of_kn : KerName.t -> constant +(** @deprecated Same as [Constant.make1] *) + +val make_con : ModPath.t -> DirPath.t -> Label.t -> constant +(** @deprecated Same as [Constant.make3] *) + +val repr_con : constant -> ModPath.t * DirPath.t * Label.t +(** @deprecated Same as [Constant.repr3] *) + +val user_con : constant -> KerName.t +(** @deprecated Same as [Constant.user] *) + +val canonical_con : constant -> KerName.t +(** @deprecated Same as [Constant.canonical] *) + +val con_modpath : constant -> ModPath.t +(** @deprecated Same as [Constant.modpath] *) + +val con_label : constant -> Label.t +(** @deprecated Same as [Constant.label] *) + +val eq_constant : constant -> constant -> bool +(** @deprecated Same as [Constant.equal] *) + +val con_ord : constant -> constant -> int +(** @deprecated Same as [Constant.CanOrd.compare] *) + +val con_user_ord : constant -> constant -> int +(** @deprecated Same as [Constant.UserOrd.compare] *) + +val con_with_label : constant -> Label.t -> constant +(** @deprecated Same as [Constant.change_label] *) + +val string_of_con : constant -> string +(** @deprecated Same as [Constant.to_string] *) + +val pr_con : constant -> Pp.std_ppcmds +(** @deprecated Same as [Constant.print] *) + +val debug_pr_con : constant -> Pp.std_ppcmds +(** @deprecated Same as [Constant.debug_print] *) + +val debug_string_of_con : constant -> string +(** @deprecated Same as [Constant.debug_to_string] *) + +(** {5 Mutual Inductive names} *) + +type mutual_inductive = MutInd.t +(** @deprecated Alias type *) + +val mind_of_kn : KerName.t -> mutual_inductive +(** @deprecated Same as [MutInd.make1] *) + +val mind_of_kn_equiv : KerName.t -> KerName.t -> mutual_inductive +(** @deprecated Same as [MutInd.make2] *) + +val make_mind : ModPath.t -> DirPath.t -> Label.t -> mutual_inductive +(** @deprecated Same as [MutInd.make3] *) + +val user_mind : mutual_inductive -> KerName.t +(** @deprecated Same as [MutInd.user] *) + +val canonical_mind : mutual_inductive -> KerName.t +(** @deprecated Same as [MutInd.canonical] *) + +val repr_mind : mutual_inductive -> ModPath.t * DirPath.t * Label.t +(** @deprecated Same as [MutInd.repr3] *) + +val eq_mind : mutual_inductive -> mutual_inductive -> bool +(** @deprecated Same as [MutInd.equal] *) + +val mind_ord : mutual_inductive -> mutual_inductive -> int +(** @deprecated Same as [MutInd.CanOrd.compare] *) + +val mind_user_ord : mutual_inductive -> mutual_inductive -> int +(** @deprecated Same as [MutInd.UserOrd.compare] *) + +val mind_label : mutual_inductive -> Label.t +(** @deprecated Same as [MutInd.label] *) + +val mind_modpath : mutual_inductive -> ModPath.t +(** @deprecated Same as [MutInd.modpath] *) + +val string_of_mind : mutual_inductive -> string +(** @deprecated Same as [MutInd.to_string] *) + +val pr_mind : mutual_inductive -> Pp.std_ppcmds +(** @deprecated Same as [MutInd.print] *) + +val debug_pr_mind : mutual_inductive -> Pp.std_ppcmds +(** @deprecated Same as [MutInd.debug_print] *) + +val debug_string_of_mind : mutual_inductive -> string +(** @deprecated Same as [MutInd.debug_to_string] *) diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 7f3ece219..485b53729 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -179,8 +179,8 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 begin let kn2' = kn_of_delta reso2 kn2 in if KerName.equal kn2 kn2' || - eq_mind (mind_of_delta_kn reso1 kn1) - (subst_ind subst2 (mind_of_kn_equiv kn2 kn2')) + MutInd.equal (mind_of_delta_kn reso1 kn1) + (subst_ind subst2 (MutInd.make2 kn2 kn2')) then () else error NotEqualInductiveAliases end; diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index aabbdc7a4..17303d80c 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -165,29 +165,27 @@ let record_fields_of_type = function (*s Recursors table. *) (* NB: here we can use the equivalence between canonical - and user constant names : Cset is fine, no need for [Cset_env] *) + and user constant names. *) -let recursors = ref Cset.empty -let init_recursors () = recursors := Cset.empty +let recursors = ref KNset.empty +let init_recursors () = recursors := KNset.empty -let add_recursors env kn = - let mk_con id = - make_con_equiv - (modpath (user_mind kn)) - (modpath (canonical_mind kn)) - DirPath.empty (Label.of_id id) +let add_recursors env ind = + let kn = MutInd.canonical ind in + let mk_kn id = + KerName.make (KerName.modpath kn) DirPath.empty (Label.of_id id) in - let mib = Environ.lookup_mind kn env in + let mib = Environ.lookup_mind ind env in Array.iter (fun mip -> let id = mip.mind_typename in - let c_rec = mk_con (Nameops.add_suffix id "_rec") - and c_rect = mk_con (Nameops.add_suffix id "_rect") in - recursors := Cset.add c_rec (Cset.add c_rect !recursors)) + let kn_rec = mk_kn (Nameops.add_suffix id "_rec") + and kn_rect = mk_kn (Nameops.add_suffix id "_rect") in + recursors := KNset.add kn_rec (KNset.add kn_rect !recursors)) mib.mind_packets let is_recursor = function - | ConstRef kn -> Cset.mem kn !recursors + | ConstRef c -> KNset.mem (Constant.canonical c) !recursors | _ -> false (*s Record tables. *) |