aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/constr.ml12
-rw-r--r--kernel/cooking.ml4
-rw-r--r--kernel/declareops.ml4
-rw-r--r--kernel/inductive.ml10
-rw-r--r--kernel/names.ml106
-rw-r--r--kernel/names.mli49
-rw-r--r--kernel/nativecode.ml28
-rw-r--r--kernel/nativeconv.ml6
-rw-r--r--kernel/nativevalues.ml4
-rw-r--r--kernel/primred.ml2
-rw-r--r--kernel/reduction.ml8
-rw-r--r--kernel/typeops.ml2
-rw-r--r--kernel/vconv.ml2
-rw-r--r--kernel/vmvalues.ml4
14 files changed, 152 insertions, 89 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml
index fb1e4d12da..b453a55d88 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -354,7 +354,7 @@ let isRefX x c =
let open GlobRef in
match x, kind c with
| ConstRef c, Const (c', _) -> Constant.CanOrd.equal c c'
- | IndRef i, Ind (i', _) -> eq_ind i i'
+ | IndRef i, Ind (i', _) -> Ind.CanOrd.equal i i'
| ConstructRef i, Construct (i', _) -> eq_constructor i i'
| VarRef id, Var id' -> Id.equal id id'
| _ -> false
@@ -955,7 +955,7 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t
| Const (c1,u1), Const (c2,u2) ->
(* The args length currently isn't used but may as well pass it. *)
Constant.CanOrd.equal c1 c2 && leq_universes (Some (GlobRef.ConstRef c1, nargs)) u1 u2
- | Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && leq_universes (Some (GlobRef.IndRef c1, nargs)) u1 u2
+ | Ind (c1,u1), Ind (c2,u2) -> Ind.CanOrd.equal c1 c2 && leq_universes (Some (GlobRef.IndRef c1, nargs)) u1 u2
| Construct (c1,u1), Construct (c2,u2) ->
eq_constructor c1 c2 && leq_universes (Some (GlobRef.ConstructRef c1, nargs)) u1 u2
| Case (_,p1,iv1,c1,bl1), Case (_,p2,iv2,c2,bl2) ->
@@ -1139,7 +1139,7 @@ let constr_ord_int f t1 t2 =
| App _, _ -> -1 | _, App _ -> 1
| Const (c1,_u1), Const (c2,_u2) -> Constant.CanOrd.compare c1 c2
| Const _, _ -> -1 | _, Const _ -> 1
- | Ind (ind1, _u1), Ind (ind2, _u2) -> ind_ord ind1 ind2
+ | Ind (ind1, _u1), Ind (ind2, _u2) -> Ind.CanOrd.compare ind1 ind2
| Ind _, _ -> -1 | _, Ind _ -> 1
| Construct (ct1,_u1), Construct (ct2,_u2) -> constructor_ord ct1 ct2
| Construct _, _ -> -1 | _, Construct _ -> 1
@@ -1331,7 +1331,7 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
| Ind (ind,u) ->
let u', hu = sh_instance u in
(Ind (sh_ind ind, u'),
- combinesmall 10 (combine (ind_syntactic_hash ind) hu))
+ combinesmall 10 (combine (Ind.SyntacticOrd.hash ind) hu))
| Construct (c,u) ->
let u', hu = sh_instance u in
(Construct (sh_construct c, u'),
@@ -1444,7 +1444,7 @@ let rec hash t =
| Const (c,u) ->
combinesmall 9 (combine (Constant.CanOrd.hash c) (Instance.hash u))
| Ind (ind,u) ->
- combinesmall 10 (combine (ind_hash ind) (Instance.hash u))
+ combinesmall 10 (combine (Ind.CanOrd.hash ind) (Instance.hash u))
| Construct (c,u) ->
combinesmall 11 (combine (constructor_hash c) (Instance.hash u))
| Case (_ , p, iv, c, bl) ->
@@ -1503,7 +1503,7 @@ struct
let h3 = Array.fold_left hash_bool_list 0 info.cstr_tags in
combine3 h1 h2 h3
let hash ci =
- let h1 = ind_hash ci.ci_ind in
+ let h1 = Ind.CanOrd.hash ci.ci_ind in
let h2 = Int.hash ci.ci_npar in
let h3 = Array.fold_left combine 0 ci.ci_cstr_ndecls in
let h4 = Array.fold_left combine 0 ci.ci_cstr_nargs in
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index fdcf44c943..cb33bb729c 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -38,13 +38,13 @@ struct
type t = my_global_reference
let equal gr1 gr2 = match gr1, gr2 with
| ConstRef c1, ConstRef c2 -> Constant.SyntacticOrd.equal c1 c2
- | IndRef i1, IndRef i2 -> eq_syntactic_ind i1 i2
+ | IndRef i1, IndRef i2 -> Ind.SyntacticOrd.equal i1 i2
| ConstructRef c1, ConstructRef c2 -> eq_syntactic_constructor c1 c2
| _ -> false
open Hashset.Combine
let hash = function
| ConstRef c -> combinesmall 1 (Constant.SyntacticOrd.hash c)
- | IndRef i -> combinesmall 2 (ind_syntactic_hash i)
+ | IndRef i -> combinesmall 2 (Ind.SyntacticOrd.hash i)
| ConstructRef c -> combinesmall 3 (constructor_syntactic_hash c)
end
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index ee90ad382b..8de7123fee 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -157,7 +157,7 @@ let hcons_const_body cb =
(** {6 Inductive types } *)
let eq_nested_type t1 t2 = match t1, t2 with
-| NestedInd ind1, NestedInd ind2 -> Names.eq_ind ind1 ind2
+| NestedInd ind1, NestedInd ind2 -> Names.Ind.CanOrd.equal ind1 ind2
| NestedInd _, _ -> false
| NestedPrimitive c1, NestedPrimitive c2 -> Names.Constant.CanOrd.equal c1 c2
| NestedPrimitive _, _ -> false
@@ -165,7 +165,7 @@ let eq_nested_type t1 t2 = match t1, t2 with
let eq_recarg r1 r2 = match r1, r2 with
| Norec, Norec -> true
| Norec, _ -> false
-| Mrec i1, Mrec i2 -> Names.eq_ind i1 i2
+| Mrec i1, Mrec i2 -> Names.Ind.CanOrd.equal i1 i2
| Mrec _, _ -> false
| Nested ty1, Nested ty2 -> eq_nested_type ty1 ty2
| Nested _, _ -> false
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 2b1a295620..e34b3c0b47 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -404,7 +404,7 @@ let type_case_branches env (pind,largs) pj c =
let check_case_info env (indsp,u) r ci =
let (mib,mip as spec) = lookup_mind_specif env indsp in
if
- not (eq_ind indsp ci.ci_ind) ||
+ not (Ind.CanOrd.equal indsp ci.ci_ind) ||
not (Int.equal mib.mind_nparams ci.ci_npar) ||
not (Array.equal Int.equal mip.mind_consnrealdecls ci.ci_cstr_ndecls) ||
not (Array.equal Int.equal mip.mind_consnrealargs ci.ci_cstr_nargs) ||
@@ -467,9 +467,9 @@ let inter_recarg r1 r2 = match r1, r2 with
| Norec, _ -> None
| Mrec i1, Mrec i2
| Nested (NestedInd i1), Nested (NestedInd i2)
-| Mrec i1, (Nested (NestedInd i2)) -> if Names.eq_ind i1 i2 then Some r1 else None
+| Mrec i1, (Nested (NestedInd i2)) -> if Names.Ind.CanOrd.equal i1 i2 then Some r1 else None
| Mrec _, _ -> None
-| Nested (NestedInd i1), Mrec i2 -> if Names.eq_ind i1 i2 then Some r2 else None
+| Nested (NestedInd i1), Mrec i2 -> if Names.Ind.CanOrd.equal i1 i2 then Some r2 else None
| Nested (NestedInd _), _ -> None
| Nested (NestedPrimitive c1), Nested (NestedPrimitive c2) ->
if Names.Constant.CanOrd.equal c1 c2 then Some r1 else None
@@ -556,7 +556,7 @@ let lookup_subterms env ind =
let match_inductive ind ra =
match ra with
- | Mrec i | Nested (NestedInd i) -> eq_ind ind i
+ | Mrec i | Nested (NestedInd i) -> Ind.CanOrd.equal ind i
| Norec | Nested (NestedPrimitive _) -> false
(* In {match c as z in ci y_s return P with |C_i x_s => t end}
@@ -667,7 +667,7 @@ let get_recargs_approx env tree ind args =
(* When the inferred tree allows it, we consider that we have a potential
nested inductive type *)
begin match dest_recarg tree with
- | Nested (NestedInd kn') | Mrec kn' when eq_ind (fst ind_kn) kn' ->
+ | Nested (NestedInd kn') | Mrec kn' when Ind.CanOrd.equal (fst ind_kn) kn' ->
build_recargs_nested ienv tree (ind_kn, largs)
| _ -> mk_norec
end
diff --git a/kernel/names.ml b/kernel/names.ml
index f7658df355..b36a39ac79 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -600,18 +600,63 @@ module Mindmap = HMap.Make(MutInd.CanOrd)
module Mindset = Mindmap.Set
module Mindmap_env = HMap.Make(MutInd.UserOrd)
+module Ind =
+struct
+ (** Designation of a (particular) inductive type. *)
+ type t = MutInd.t (* the name of the inductive type *)
+ * int (* the position of this inductive type
+ within the block of mutually-recursive inductive types.
+ BEWARE: indexing starts from 0. *)
+ let modpath (mind, _) = MutInd.modpath mind
+
+ module CanOrd =
+ struct
+ type nonrec t = t
+ let equal (m1, i1) (m2, i2) = Int.equal i1 i2 && MutInd.CanOrd.equal m1 m2
+ let compare (m1, i1) (m2, i2) =
+ let c = Int.compare i1 i2 in
+ if Int.equal c 0 then MutInd.CanOrd.compare m1 m2 else c
+ let hash (m, i) =
+ Hashset.Combine.combine (MutInd.CanOrd.hash m) (Int.hash i)
+ end
+
+ module UserOrd =
+ struct
+ type nonrec t = t
+ let equal (m1, i1) (m2, i2) =
+ Int.equal i1 i2 && MutInd.UserOrd.equal m1 m2
+ let compare (m1, i1) (m2, i2) =
+ let c = Int.compare i1 i2 in
+ if Int.equal c 0 then MutInd.UserOrd.compare m1 m2 else c
+ let hash (m, i) =
+ Hashset.Combine.combine (MutInd.UserOrd.hash m) (Int.hash i)
+ end
+
+ module SyntacticOrd =
+ struct
+ type nonrec t = t
+ let equal (m1, i1) (m2, i2) =
+ Int.equal i1 i2 && MutInd.SyntacticOrd.equal m1 m2
+
+ let compare (m1, i1) (m2, i2) =
+ let c = Int.compare i1 i2 in
+ if Int.equal c 0 then MutInd.SyntacticOrd.compare m1 m2 else c
+
+ let hash (m, i) =
+ Hashset.Combine.combine (MutInd.SyntacticOrd.hash m) (Int.hash i)
+ end
+
+end
+
(** Designation of a (particular) inductive type. *)
-type inductive = MutInd.t (* the name of the inductive type *)
- * int (* the position of this inductive type
- within the block of mutually-recursive inductive types.
- BEWARE: indexing starts from 0. *)
+type inductive = Ind.t
(** Designation of a (particular) constructor of a (particular) inductive type. *)
type constructor = inductive (* designates the inductive type *)
* int (* the index of the constructor
BEWARE: indexing starts from 1. *)
-let ind_modpath (mind,_) = MutInd.modpath mind
+let ind_modpath = Ind.modpath
let constr_modpath (ind,_) = ind_modpath ind
let ith_mutual_inductive (mind, _) i = (mind, i)
@@ -619,28 +664,17 @@ 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 && MutInd.equal m1 m2
-let eq_user_ind (m1, i1) (m2, i2) =
- Int.equal i1 i2 && MutInd.UserOrd.equal m1 m2
-let eq_syntactic_ind (m1, i1) (m2, i2) =
- Int.equal i1 i2 && MutInd.SyntacticOrd.equal m1 m2
-
-let ind_ord (m1, i1) (m2, i2) =
- let c = Int.compare i1 i2 in
- 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 MutInd.UserOrd.compare m1 m2 else c
-let ind_syntactic_ord (m1, i1) (m2, i2) =
- let c = Int.compare i1 i2 in
- if Int.equal c 0 then MutInd.SyntacticOrd.compare m1 m2 else c
-
-let ind_hash (m, i) =
- Hashset.Combine.combine (MutInd.hash m) (Int.hash i)
-let ind_user_hash (m, i) =
- Hashset.Combine.combine (MutInd.UserOrd.hash m) (Int.hash i)
-let ind_syntactic_hash (m, i) =
- Hashset.Combine.combine (MutInd.SyntacticOrd.hash m) (Int.hash i)
+let eq_ind = Ind.CanOrd.equal
+let eq_user_ind = Ind.UserOrd.equal
+let eq_syntactic_ind = Ind.SyntacticOrd.equal
+
+let ind_ord = Ind.CanOrd.compare
+let ind_user_ord = Ind.UserOrd.compare
+let ind_syntactic_ord = Ind.SyntacticOrd.compare
+
+let ind_hash = Ind.CanOrd.hash
+let ind_user_hash = Ind.UserOrd.hash
+let ind_syntactic_hash = Ind.SyntacticOrd.hash
let eq_constructor (ind1, j1) (ind2, j2) = Int.equal j1 j2 && eq_ind ind1 ind2
let eq_user_constructor (ind1, j1) (ind2, j2) =
@@ -665,20 +699,10 @@ let constructor_user_hash (ind, i) =
let constructor_syntactic_hash (ind, i) =
Hashset.Combine.combine (ind_syntactic_hash ind) (Int.hash i)
-module InductiveOrdered = struct
- type t = inductive
- let compare = ind_ord
-end
-
-module InductiveOrdered_env = struct
- type t = inductive
- let compare = ind_user_ord
-end
-
-module Indset = Set.Make(InductiveOrdered)
-module Indset_env = Set.Make(InductiveOrdered_env)
-module Indmap = Map.Make(InductiveOrdered)
-module Indmap_env = Map.Make(InductiveOrdered_env)
+module Indset = Set.Make(Ind.CanOrd)
+module Indset_env = Set.Make(Ind.UserOrd)
+module Indmap = Map.Make(Ind.CanOrd)
+module Indmap_env = Map.Make(Ind.UserOrd)
module ConstructorOrdered = struct
type t = constructor
diff --git a/kernel/names.mli b/kernel/names.mli
index 76be6ca105..be53830af5 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -479,11 +479,39 @@ module Mindset : CSig.SetS with type elt = MutInd.t
module Mindmap : Map.ExtS with type key = MutInd.t and module Set := Mindset
module Mindmap_env : CMap.ExtS with type key = MutInd.t
-(** Designation of a (particular) inductive type. *)
-type inductive = MutInd.t (* the name of the inductive type *)
- * int (* the position of this inductive type
- within the block of mutually-recursive inductive types.
- BEWARE: indexing starts from 0. *)
+module Ind :
+sig
+ (** Designation of a (particular) inductive type. *)
+ type t = MutInd.t (* the name of the inductive type *)
+ * int (* the position of this inductive type
+ within the block of mutually-recursive inductive types.
+ BEWARE: indexing starts from 0. *)
+ val modpath : t -> ModPath.t
+
+ module CanOrd : sig
+ type nonrec t = t
+ val compare : t -> t -> int
+ val equal : t -> t -> bool
+ val hash : t -> int
+ end
+
+ module UserOrd : sig
+ type nonrec t = t
+ val compare : t -> t -> int
+ val equal : t -> t -> bool
+ val hash : t -> int
+ end
+
+ module SyntacticOrd : sig
+ type nonrec t = t
+ val compare : t -> t -> int
+ val equal : t -> t -> bool
+ val hash : t -> int
+ end
+
+end
+
+type inductive = Ind.t
(** Designation of a (particular) constructor of a (particular) inductive type. *)
type constructor = inductive (* designates the inductive type *)
@@ -500,6 +528,8 @@ module Indmap_env : CMap.ExtS with type key = inductive and module Set := Indset
module Constrmap_env : CMap.ExtS with type key = constructor and module Set := Constrset_env
val ind_modpath : inductive -> ModPath.t
+[@@ocaml.deprecated "Use the Ind module"]
+
val constr_modpath : constructor -> ModPath.t
val ith_mutual_inductive : inductive -> int -> inductive
@@ -507,14 +537,23 @@ val ith_constructor_of_inductive : inductive -> int -> constructor
val inductive_of_constructor : constructor -> inductive
val index_of_constructor : constructor -> int
val eq_ind : inductive -> inductive -> bool
+[@@ocaml.deprecated "Use the Ind module"]
val eq_user_ind : inductive -> inductive -> bool
+[@@ocaml.deprecated "Use the Ind module"]
val eq_syntactic_ind : inductive -> inductive -> bool
+[@@ocaml.deprecated "Use the Ind module"]
val ind_ord : inductive -> inductive -> int
+[@@ocaml.deprecated "Use the Ind module"]
val ind_hash : inductive -> int
+[@@ocaml.deprecated "Use the Ind module"]
val ind_user_ord : inductive -> inductive -> int
+[@@ocaml.deprecated "Use the Ind module"]
val ind_user_hash : inductive -> int
+[@@ocaml.deprecated "Use the Ind module"]
val ind_syntactic_ord : inductive -> inductive -> int
+[@@ocaml.deprecated "Use the Ind module"]
val ind_syntactic_hash : inductive -> int
+[@@ocaml.deprecated "Use the Ind module"]
val eq_constructor : constructor -> constructor -> bool
val eq_user_constructor : constructor -> constructor -> bool
val eq_syntactic_constructor : constructor -> constructor -> bool
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 9314203e04..b5c4d6416a 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -65,11 +65,11 @@ type gname =
let eq_gname gn1 gn2 =
match gn1, gn2 with
| Gind (s1, ind1), Gind (s2, ind2) ->
- String.equal s1 s2 && eq_ind ind1 ind2
+ String.equal s1 s2 && Ind.CanOrd.equal ind1 ind2
| Gconstant (s1, c1), Gconstant (s2, c2) ->
String.equal s1 s2 && Constant.CanOrd.equal c1 c2
| Gproj (s1, ind1, i1), Gproj (s2, ind2, i2) ->
- String.equal s1 s2 && eq_ind ind1 ind2 && Int.equal i1 i2
+ String.equal s1 s2 && Ind.CanOrd.equal ind1 ind2 && Int.equal i1 i2
| Gcase (None, i1), Gcase (None, i2) -> Int.equal i1 i2
| Gcase (Some l1, i1), Gcase (Some l2, i2) -> Int.equal i1 i2 && Label.equal l1 l2
| Gpred (None, i1), Gpred (None, i2) -> Int.equal i1 i2
@@ -96,7 +96,7 @@ open Hashset.Combine
let gname_hash gn = match gn with
| Gind (s, ind) ->
- combinesmall 1 (combine (String.hash s) (ind_hash ind))
+ combinesmall 1 (combine (String.hash s) (Ind.CanOrd.hash ind))
| Gconstant (s, c) ->
combinesmall 2 (combine (String.hash s) (Constant.CanOrd.hash c))
| Gcase (l, i) -> combinesmall 3 (combine (Option.hash Label.hash l) (Int.hash i))
@@ -107,7 +107,7 @@ let gname_hash gn = match gn with
| Ginternal s -> combinesmall 8 (String.hash s)
| Grel i -> combinesmall 9 (Int.hash i)
| Gnamed id -> combinesmall 10 (Id.hash id)
-| Gproj (s, p, i) -> combinesmall 11 (combine (String.hash s) (combine (ind_hash p) i))
+| Gproj (s, p, i) -> combinesmall 11 (combine (String.hash s) (combine (Ind.CanOrd.hash p) i))
let case_ctr = ref (-1)
@@ -150,11 +150,11 @@ let eq_symbol sy1 sy2 =
| SymbName n1, SymbName n2 -> Name.equal n1 n2
| SymbConst kn1, SymbConst kn2 -> Constant.CanOrd.equal kn1 kn2
| SymbMatch sw1, SymbMatch sw2 -> eq_annot_sw sw1 sw2
- | SymbInd ind1, SymbInd ind2 -> eq_ind ind1 ind2
+ | SymbInd ind1, SymbInd ind2 -> Ind.CanOrd.equal ind1 ind2
| SymbMeta m1, SymbMeta m2 -> Int.equal m1 m2
| SymbEvar evk1, SymbEvar evk2 -> Evar.equal evk1 evk2
| SymbLevel l1, SymbLevel l2 -> Univ.Level.equal l1 l2
- | SymbProj (i1, k1), SymbProj (i2, k2) -> eq_ind i1 i2 && Int.equal k1 k2
+ | SymbProj (i1, k1), SymbProj (i2, k2) -> Ind.CanOrd.equal i1 i2 && Int.equal k1 k2
| _, _ -> false
let hash_symbol symb =
@@ -164,11 +164,11 @@ let hash_symbol symb =
| SymbName name -> combinesmall 3 (Name.hash name)
| SymbConst c -> combinesmall 4 (Constant.CanOrd.hash c)
| SymbMatch sw -> combinesmall 5 (hash_annot_sw sw)
- | SymbInd ind -> combinesmall 6 (ind_hash ind)
+ | SymbInd ind -> combinesmall 6 (Ind.CanOrd.hash ind)
| SymbMeta m -> combinesmall 7 m
| SymbEvar evk -> combinesmall 8 (Evar.hash evk)
| SymbLevel l -> combinesmall 9 (Univ.Level.hash l)
- | SymbProj (i, k) -> combinesmall 10 (combine (ind_hash i) k)
+ | SymbProj (i, k) -> combinesmall 10 (combine (Ind.CanOrd.hash i) k)
module HashedTypeSymbol = struct
type t = symbol
@@ -438,7 +438,7 @@ let rec eq_mllambda gn1 gn2 n env1 env2 t1 t2 =
eq_mllam_branches gn1 gn2 n env1 env2 br1 br2
| MLconstruct (pf1, ind1, tag1, args1), MLconstruct (pf2, ind2, tag2, args2) ->
String.equal pf1 pf2 &&
- eq_ind ind1 ind2 &&
+ Ind.CanOrd.equal ind1 ind2 &&
Int.equal tag1 tag2 &&
Array.equal (eq_mllambda gn1 gn2 n env1 env2) args1 args2
| MLint i1, MLint i2 ->
@@ -457,7 +457,7 @@ let rec eq_mllambda gn1 gn2 n env1 env2 t1 t2 =
Array.equal (eq_mllambda gn1 gn2 n env1 env2) arr1 arr2
| MLisaccu (s1, ind1, ml1), MLisaccu (s2, ind2, ml2) ->
- String.equal s1 s2 && eq_ind ind1 ind2 &&
+ String.equal s1 s2 && Ind.CanOrd.equal ind1 ind2 &&
eq_mllambda gn1 gn2 n env1 env2 ml1 ml2
| (MLlocal _ | MLglobal _ | MLprimitive _ | MLlam _ | MLletrec _ | MLlet _ |
MLapp _ | MLif _ | MLmatch _ | MLconstruct _ | MLint _ | MLuint _ |
@@ -527,7 +527,7 @@ let rec hash_mllambda gn n env t =
combinesmall 9 (hash_mllam_branches gn n env (combine3 hannot hc haccu) br)
| MLconstruct (pf, ind, tag, args) ->
let hpf = String.hash pf in
- let hcs = ind_hash ind in
+ let hcs = Ind.CanOrd.hash ind in
let htag = Int.hash tag in
combinesmall 10 (hash_mllambda_array gn n env (combine3 hpf hcs htag) args)
| MLint i ->
@@ -545,7 +545,7 @@ let rec hash_mllambda gn n env t =
| MLarray arr ->
combinesmall 15 (hash_mllambda_array gn n env 1 arr)
| MLisaccu (s, ind, c) ->
- combinesmall 16 (combine (String.hash s) (combine (ind_hash ind) (hash_mllambda gn n env c)))
+ combinesmall 16 (combine (String.hash s) (combine (Ind.CanOrd.hash ind) (hash_mllambda gn n env c)))
| MLfloat f ->
combinesmall 17 (Float64.hash f)
@@ -689,7 +689,7 @@ let eq_global g1 g2 =
eq_mllambda gn1 gn2 (Array.length lns1) env1 env2 t1 t2
| Gopen s1, Gopen s2 -> String.equal s1 s2
| Gtype (ind1, arr1), Gtype (ind2, arr2) ->
- eq_ind ind1 ind2 &&
+ Ind.CanOrd.equal ind1 ind2 &&
Array.equal (fun (tag1,ar1) (tag2,ar2) -> Int.equal tag1 tag2 && Int.equal ar1 ar2) arr1 arr2
| Gcomment s1, Gcomment s2 -> String.equal s1 s2
| _, _ -> false
@@ -720,7 +720,7 @@ let hash_global g =
let hash_aux acc (tag,ar) =
combine3 acc (Int.hash tag) (Int.hash ar)
in
- combinesmall 6 (combine (ind_hash ind) (Array.fold_left hash_aux 0 arr))
+ combinesmall 6 (combine (Ind.CanOrd.hash ind) (Array.fold_left hash_aux 0 arr))
| Gcomment s -> combinesmall 7 (String.hash s)
let global_stack = ref ([] : global list)
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 00418009c7..76215b4386 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -80,7 +80,7 @@ and conv_atom env pb lvl a1 a2 cu =
| Arel i1, Arel i2 ->
if Int.equal i1 i2 then cu else raise NotConvertible
| Aind (ind1,u1), Aind (ind2,u2) ->
- if eq_ind ind1 ind2 then convert_instances ~flex:false u1 u2 cu
+ if Ind.CanOrd.equal ind1 ind2 then convert_instances ~flex:false u1 u2 cu
else raise NotConvertible
| Aconstant (c1,u1), Aconstant (c2,u2) ->
if Constant.CanOrd.equal c1 c2 then convert_instances ~flex:true u1 u2 cu
@@ -90,7 +90,7 @@ and conv_atom env pb lvl a1 a2 cu =
| Avar id1, Avar id2 ->
if Id.equal id1 id2 then cu else raise NotConvertible
| Acase(a1,ac1,p1,bs1), Acase(a2,ac2,p2,bs2) ->
- if not (eq_ind a1.asw_ind a2.asw_ind) then raise NotConvertible;
+ if not (Ind.CanOrd.equal a1.asw_ind a2.asw_ind) then raise NotConvertible;
let cu = conv_accu env CONV lvl ac1 ac2 cu in
let tbl = a1.asw_reloc in
let len = Array.length tbl in
@@ -124,7 +124,7 @@ and conv_atom env pb lvl a1 a2 cu =
let v = mk_rel_accu lvl in
conv_val env pb (lvl + 1) (d1 v) (d2 v) cu
| Aproj((ind1, i1), ac1), Aproj((ind2, i2), ac2) ->
- if not (eq_ind ind1 ind2 && Int.equal i1 i2) then raise NotConvertible
+ if not (Ind.CanOrd.equal ind1 ind2 && Int.equal i1 i2) then raise NotConvertible
else conv_accu env CONV lvl ac1 ac2 cu
| Arel _, _ | Aind _, _ | Aconstant _, _ | Asort _, _ | Avar _, _
| Acase _, _ | Afix _, _ | Acofix _, _ | Acofixe _, _ | Aprod _, _
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 05c98e4b87..bd6241ae67 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -36,13 +36,13 @@ type annot_sw = {
(* We compare only what is relevant for generation of ml code *)
let eq_annot_sw asw1 asw2 =
- eq_ind asw1.asw_ind asw2.asw_ind &&
+ Ind.CanOrd.equal asw1.asw_ind asw2.asw_ind &&
String.equal asw1.asw_prefix asw2.asw_prefix
open Hashset.Combine
let hash_annot_sw asw =
- combine (ind_hash asw.asw_ind) (String.hash asw.asw_prefix)
+ combine (Ind.CanOrd.hash asw.asw_ind) (String.hash asw.asw_prefix)
type sort_annot = string * int
diff --git a/kernel/primred.ml b/kernel/primred.ml
index 17e5a89b74..f0b4d6d362 100644
--- a/kernel/primred.ml
+++ b/kernel/primred.ml
@@ -16,7 +16,7 @@ let check_same_types typ c1 c2 =
then raise (IncompatibleDeclarations (IncompatTypes typ, c1, c2))
let check_same_inds ind i1 i2 =
- if not (eq_ind i1 i2)
+ if not (Ind.CanOrd.equal i1 i2)
then raise (IncompatibleDeclarations (IncompatInd ind, i1, i2))
let add_retroknowledge retro action =
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 8eb1c10f70..5589ae3483 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -568,7 +568,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
(* Inductive types: MutInd MutConstruct Fix Cofix *)
| (FInd (ind1,u1 as pind1), FInd (ind2,u2 as pind2)) ->
- if eq_ind ind1 ind2 then
+ if Ind.CanOrd.equal ind1 ind2 then
if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then
let cuniv = convert_instances ~flex:false u1 u2 cuniv in
convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
@@ -588,7 +588,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
else raise NotConvertible
| (FConstruct ((ind1,j1),u1 as pctor1), FConstruct ((ind2,j2),u2 as pctor2)) ->
- if Int.equal j1 j2 && eq_ind ind1 ind2 then
+ if Int.equal j1 j2 && Ind.CanOrd.equal ind1 ind2 then
if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then
let cuniv = convert_instances ~flex:false u1 u2 cuniv in
convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
@@ -669,7 +669,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
else raise NotConvertible
| FCaseInvert (ci1,p1,_,_,br1,e1), FCaseInvert (ci2,p2,_,_,br2,e2) ->
- (if not (eq_ind ci1.ci_ind ci2.ci_ind) then raise NotConvertible);
+ (if not (Ind.CanOrd.equal ci1.ci_ind ci2.ci_ind) then raise NotConvertible);
let el1 = el_stack lft1 v1 and el2 = el_stack lft2 v2 in
let ccnv = ccnv CONV l2r infos el1 el2 in
let cuniv = ccnv (mk_clos e1 p1) (mk_clos e2 p2) cuniv in
@@ -711,7 +711,7 @@ and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv =
let cu2 = f fx1 fx2 cu1 in
cmp_rec a1 a2 cu2
| (Zlcase(ci1,l1,p1,br1,e1),Zlcase(ci2,l2,p2,br2,e2)) ->
- if not (eq_ind ci1.ci_ind ci2.ci_ind) then
+ if not (Ind.CanOrd.equal ci1.ci_ind ci2.ci_ind) then
raise NotConvertible;
let cu2 = f (l1, mk_clos e1 p1) (l2, mk_clos e2 p2) cu1 in
convert_branches l2r infos ci1 e1 e2 l1 l2 br1 br2 cu2
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index f86c12e1f1..85e24f87b7 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -413,7 +413,7 @@ let type_of_projection env p c ct =
try find_rectype env ct
with Not_found -> error_case_not_inductive env (make_judge c ct)
in
- assert(eq_ind (Projection.inductive p) ind);
+ assert(Ind.CanOrd.equal (Projection.inductive p) ind);
let ty = Vars.subst_instance_constr u pty in
substl (c :: CList.rev args) ty
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 2de902c827..1432fb9310 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -95,7 +95,7 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu =
(* Pp.(msg_debug (str "conv_atom(" ++ pr_atom a1 ++ str ", " ++ pr_atom a2 ++ str ")")) ; *)
match a1, a2 with
| Aind ((mi,_i) as ind1) , Aind ind2 ->
- if eq_ind ind1 ind2 && compare_stack stk1 stk2 then
+ if Ind.CanOrd.equal ind1 ind2 && compare_stack stk1 stk2 then
let ulen = Univ.AUContext.size (Environ.mind_context env mi) in
if ulen = 0 then
conv_stack env k stk1 stk2 cu
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index 28a7abc7c6..7b4101b9d0 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -96,7 +96,7 @@ let hash_structured_values (v : structured_values) =
let eq_structured_constant c1 c2 = match c1, c2 with
| Const_sort s1, Const_sort s2 -> Sorts.equal s1 s2
| Const_sort _, _ -> false
-| Const_ind i1, Const_ind i2 -> eq_ind i1 i2
+| Const_ind i1, Const_ind i2 -> Ind.CanOrd.equal i1 i2
| Const_ind _, _ -> false
| Const_b0 t1, Const_b0 t2 -> Int.equal t1 t2
| Const_b0 _, _ -> false
@@ -113,7 +113,7 @@ let hash_structured_constant c =
let open Hashset.Combine in
match c with
| Const_sort s -> combinesmall 1 (Sorts.hash s)
- | Const_ind i -> combinesmall 2 (ind_hash i)
+ | Const_ind i -> combinesmall 2 (Ind.CanOrd.hash i)
| Const_b0 t -> combinesmall 3 (Int.hash t)
| Const_univ_level l -> combinesmall 4 (Univ.Level.hash l)
| Const_val v -> combinesmall 5 (hash_structured_values v)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:17:47 +0000