diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/constr.ml | 34 | ||||
| -rw-r--r-- | kernel/cooking.ml | 8 | ||||
| -rw-r--r-- | kernel/declareops.ml | 6 | ||||
| -rw-r--r-- | kernel/environ.ml | 63 | ||||
| -rw-r--r-- | kernel/environ.mli | 26 | ||||
| -rw-r--r-- | kernel/inductive.ml | 16 | ||||
| -rw-r--r-- | kernel/names.ml | 269 | ||||
| -rw-r--r-- | kernel/names.mli | 209 | ||||
| -rw-r--r-- | kernel/nativecode.ml | 36 | ||||
| -rw-r--r-- | kernel/nativeconv.ml | 8 | ||||
| -rw-r--r-- | kernel/nativelambda.ml | 4 | ||||
| -rw-r--r-- | kernel/nativevalues.ml | 4 | ||||
| -rw-r--r-- | kernel/primred.ml | 4 | ||||
| -rw-r--r-- | kernel/reduction.ml | 14 | ||||
| -rw-r--r-- | kernel/subtyping.ml | 2 | ||||
| -rw-r--r-- | kernel/typeops.ml | 2 | ||||
| -rw-r--r-- | kernel/vconv.ml | 4 | ||||
| -rw-r--r-- | kernel/vmemitcodes.ml | 8 | ||||
| -rw-r--r-- | kernel/vmsymtable.ml | 2 | ||||
| -rw-r--r-- | kernel/vmvalues.ml | 8 |
20 files changed, 466 insertions, 261 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml index 1837a39764..3157ec9f57 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -353,9 +353,9 @@ let isRef c = match kind c with let isRefX x c = let open GlobRef in match x, kind c with - | ConstRef c, Const (c', _) -> Constant.equal c c' - | IndRef i, Ind (i', _) -> eq_ind i i' - | ConstructRef i, Construct (i', _) -> eq_constructor i i' + | ConstRef c, Const (c', _) -> Constant.CanOrd.equal c c' + | IndRef i, Ind (i', _) -> Ind.CanOrd.equal i i' + | ConstructRef i, Construct (i', _) -> Construct.CanOrd.equal i i' | VarRef id, Var id' -> Id.equal id id' | _ -> false @@ -950,14 +950,14 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t let len = Array.length l1 in Int.equal len (Array.length l2) && leq (nargs+len) c1 c2 && Array.equal_norefl (eq 0) l1 l2 - | Proj (p1,c1), Proj (p2,c2) -> Projection.equal p1 p2 && eq 0 c1 c2 + | Proj (p1,c1), Proj (p2,c2) -> Projection.CanOrd.equal p1 p2 && eq 0 c1 c2 | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && List.equal (eq 0) l1 l2 | Const (c1,u1), Const (c2,u2) -> (* The args length currently isn't used but may as well pass it. *) - Constant.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 + Constant.CanOrd.equal c1 c2 && leq_universes (Some (GlobRef.ConstRef 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 + Construct.CanOrd.equal c1 c2 && leq_universes (Some (GlobRef.ConstructRef c1, nargs)) u1 u2 | Case (_,p1,iv1,c1,bl1), Case (_,p2,iv2,c2,bl2) -> eq 0 p1 p2 && eq_invert (eq 0) (leq_universes None) iv1 iv2 && eq 0 c1 c2 && Array.equal (eq 0) bl1 bl2 | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) -> @@ -1139,9 +1139,9 @@ 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 (ct1,_u1), Construct (ct2,_u2) -> Construct.CanOrd.compare ct1 ct2 | Construct _, _ -> -1 | _, Construct _ -> 1 | Case (_,p1,iv1,c1,bl1), Case (_,p2,iv2,c2,bl2) -> let c = f p1 p2 in @@ -1158,7 +1158,7 @@ let constr_ord_int f t1 t2 = ((Int.compare =? (Array.compare f)) ==? (Array.compare f)) ln1 ln2 tl1 tl2 bl1 bl2 | CoFix _, _ -> -1 | _, CoFix _ -> 1 - | Proj (p1,c1), Proj (p2,c2) -> (Projection.compare =? f) p1 p2 c1 c2 + | Proj (p1,c1), Proj (p2,c2) -> (Projection.CanOrd.compare =? f) p1 p2 c1 c2 | Proj _, _ -> -1 | _, Proj _ -> 1 | Int i1, Int i2 -> Uint63.compare i1 i2 | Int _, _ -> -1 | _, Int _ -> 1 @@ -1331,11 +1331,11 @@ 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'), - combinesmall 11 (combine (constructor_syntactic_hash c) hu)) + combinesmall 11 (combine (Construct.SyntacticOrd.hash c) hu)) | Case (ci,p,iv,c,bl) -> let p, hp = sh_rec p and iv, hiv = sh_invert iv @@ -1442,11 +1442,11 @@ let rec hash t = | Evar (e,l) -> combinesmall 8 (combine (Evar.hash e) (hash_term_list l)) | Const (c,u) -> - combinesmall 9 (combine (Constant.hash c) (Instance.hash 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)) + combinesmall 11 (combine (Construct.CanOrd.hash c) (Instance.hash u)) | Case (_ , p, iv, c, bl) -> combinesmall 12 (combine4 (hash c) (hash p) (hash_invert iv) (hash_term_array bl)) | Fix (_ln ,(_, tl, bl)) -> @@ -1456,7 +1456,7 @@ let rec hash t = | Meta n -> combinesmall 15 n | Rel n -> combinesmall 16 n | Proj (p,c) -> - combinesmall 17 (combine (Projection.hash p) (hash c)) + combinesmall 17 (combine (Projection.CanOrd.hash p) (hash c)) | Int i -> combinesmall 18 (Uint63.hash i) | Float f -> combinesmall 19 (Float64.hash f) | Array(u,t,def,ty) -> @@ -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..3707a75157 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -38,14 +38,14 @@ 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 - | ConstructRef c1, ConstructRef c2 -> eq_syntactic_constructor c1 c2 + | IndRef i1, IndRef i2 -> Ind.SyntacticOrd.equal i1 i2 + | ConstructRef c1, ConstructRef c2 -> Construct.SyntacticOrd.equal 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) - | ConstructRef c -> combinesmall 3 (constructor_syntactic_hash c) + | IndRef i -> combinesmall 2 (Ind.SyntacticOrd.hash i) + | ConstructRef c -> combinesmall 3 (Construct.SyntacticOrd.hash c) end module RefTable = Hashtbl.Make(RefHash) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index b9f434f179..8de7123fee 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -157,15 +157,15 @@ 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.equal c1 c2 +| NestedPrimitive c1, NestedPrimitive c2 -> Names.Constant.CanOrd.equal c1 c2 | NestedPrimitive _, _ -> false 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/environ.ml b/kernel/environ.ml index dec9e1deb8..17c5a02e2b 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -832,3 +832,66 @@ let set_retroknowledge env r = { env with retroknowledge = r } let set_native_symbols env native_symbols = { env with native_symbols } let add_native_symbols dir syms env = { env with native_symbols = DPmap.add dir syms env.native_symbols } + +module type QNameS = +sig + type t + val equal : env -> t -> t -> bool + val compare : env -> t -> t -> int + val hash : env -> t -> int +end + +module QConstant = +struct + type t = Constant.t + let equal _env c1 c2 = Constant.CanOrd.equal c1 c2 + let compare _env c1 c2 = Constant.CanOrd.compare c1 c2 + let hash _env c = Constant.CanOrd.hash c +end + +module QMutInd = +struct + type t = MutInd.t + let equal _env c1 c2 = MutInd.CanOrd.equal c1 c2 + let compare _env c1 c2 = MutInd.CanOrd.compare c1 c2 + let hash _env c = MutInd.CanOrd.hash c +end + +module QInd = +struct + type t = Ind.t + let equal _env c1 c2 = Ind.CanOrd.equal c1 c2 + let compare _env c1 c2 = Ind.CanOrd.compare c1 c2 + let hash _env c = Ind.CanOrd.hash c +end + +module QConstruct = +struct + type t = Construct.t + let equal _env c1 c2 = Construct.CanOrd.equal c1 c2 + let compare _env c1 c2 = Construct.CanOrd.compare c1 c2 + let hash _env c = Construct.CanOrd.hash c +end + +module QProjection = +struct + type t = Projection.t + let equal _env c1 c2 = Projection.CanOrd.equal c1 c2 + let compare _env c1 c2 = Projection.CanOrd.compare c1 c2 + let hash _env c = Projection.CanOrd.hash c + module Repr = + struct + type t = Projection.Repr.t + let equal _env c1 c2 = Projection.Repr.CanOrd.equal c1 c2 + let compare _env c1 c2 = Projection.Repr.CanOrd.compare c1 c2 + let hash _env c = Projection.Repr.CanOrd.hash c + end +end + +module QGlobRef = +struct + type t = GlobRef.t + let equal _env c1 c2 = GlobRef.CanOrd.equal c1 c2 + let compare _env c1 c2 = GlobRef.CanOrd.compare c1 c2 + let hash _env c = GlobRef.CanOrd.hash c +end diff --git a/kernel/environ.mli b/kernel/environ.mli index f443ba38e1..f0b40e6492 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -284,6 +284,32 @@ val template_polymorphic_ind : inductive -> env -> bool val template_polymorphic_variables : inductive -> env -> Univ.Level.t list val template_polymorphic_pind : pinductive -> env -> bool +(** {6 Name quotients} *) + +module type QNameS = +sig + type t + val equal : env -> t -> t -> bool + val compare : env -> t -> t -> int + val hash : env -> t -> int +end + +module QConstant : QNameS with type t = Constant.t + +module QMutInd : QNameS with type t = MutInd.t + +module QInd : QNameS with type t = Ind.t + +module QConstruct : QNameS with type t = Construct.t + +module QProjection : +sig + include QNameS with type t = Projection.t + module Repr : QNameS with type t = Projection.Repr.t +end + +module QGlobRef : QNameS with type t = GlobRef.t + (** {5 Modules } *) val add_modtype : module_type_body -> env -> env diff --git a/kernel/inductive.ml b/kernel/inductive.ml index d751d9875a..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,12 +467,12 @@ 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.equal c1 c2 then Some r1 else None + if Names.Constant.CanOrd.equal c1 c2 then Some r1 else None | Nested (NestedPrimitive _), _ -> None let inter_wf_paths = Rtree.inter Declareops.eq_recarg inter_recarg Norec @@ -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} @@ -644,7 +644,7 @@ let abstract_mind_lc ntyps npars lc = let is_primitive_positive_container env c = match env.retroknowledge.Retroknowledge.retro_array with - | Some c' when Constant.equal c c' -> true + | Some c' when QConstant.equal env c c' -> true | _ -> false (* [get_recargs_approx env tree ind args] builds an approximation of the recargs @@ -667,13 +667,13 @@ 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 | Const (c,_) when is_primitive_positive_container env c -> begin match dest_recarg tree with - | Nested (NestedPrimitive c') when Constant.equal c c' -> + | Nested (NestedPrimitive c') when QConstant.equal env c c' -> build_recargs_nested_primitive ienv tree (c, largs) | _ -> mk_norec end diff --git a/kernel/names.ml b/kernel/names.ml index 592b5e65f7..5b6064fa9f 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -447,6 +447,22 @@ module KNset = KNmap.Set (** {6 Kernel pairs } *) +module type EqType = +sig + type t + val compare : t -> t -> int + val equal : t -> t -> bool + val hash : t -> int +end + +module type QNameS = +sig + type t + module CanOrd : EqType with type t = t + module UserOrd : EqType with type t = t + module SyntacticOrd : EqType with type t = t +end + (** For constant and inductive names, we use a kernel name couple (kn1,kn2) where kn1 corresponds to the name used at toplevel (i.e. what the user see) and kn2 corresponds to the canonical kernel name i.e. in the environment @@ -529,6 +545,7 @@ module KerPair = struct end module SyntacticOrd = struct + type t = kernel_pair let compare x y = match x, y with | Same knx, Same kny -> KerName.compare knx kny | Dual (knux,kncx), Dual (knuy,kncy) -> @@ -599,100 +616,147 @@ 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 + +module Construct = +struct + (** Designation of a (particular) constructor of a (particular) inductive type. *) + type t = Ind.t (* designates the inductive type *) + * int (* the index of the constructor + BEWARE: indexing starts from 1. *) + + let modpath (ind, _) = Ind.modpath ind + + module CanOrd = + struct + type nonrec t = t + let equal (ind1, j1) (ind2, j2) = Int.equal j1 j2 && Ind.CanOrd.equal ind1 ind2 + let compare (ind1, j1) (ind2, j2) = + let c = Int.compare j1 j2 in + if Int.equal c 0 then Ind.CanOrd.compare ind1 ind2 else c + let hash (ind, i) = + Hashset.Combine.combine (Ind.CanOrd.hash ind) (Int.hash i) + end + + module UserOrd = + struct + type nonrec t = t + let equal (ind1, j1) (ind2, j2) = + Int.equal j1 j2 && Ind.UserOrd.equal ind1 ind2 + let compare (ind1, j1) (ind2, j2) = + let c = Int.compare j1 j2 in + if Int.equal c 0 then Ind.UserOrd.compare ind1 ind2 else c + let hash (ind, i) = + Hashset.Combine.combine (Ind.UserOrd.hash ind) (Int.hash i) + end + + module SyntacticOrd = + struct + type nonrec t = t + let equal (ind1, j1) (ind2, j2) = + Int.equal j1 j2 && Ind.SyntacticOrd.equal ind1 ind2 + let compare (ind1, j1) (ind2, j2) = + let c = Int.compare j1 j2 in + if Int.equal c 0 then Ind.SyntacticOrd.compare ind1 ind2 else c + let hash (ind, i) = + Hashset.Combine.combine (Ind.SyntacticOrd.hash ind) (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. *) +type constructor = Construct.t -let ind_modpath (mind,_) = MutInd.modpath mind -let constr_modpath (ind,_) = ind_modpath ind +let ind_modpath = Ind.modpath +let constr_modpath = Construct.modpath 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 && 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_constructor (ind1, j1) (ind2, j2) = Int.equal j1 j2 && eq_ind ind1 ind2 -let eq_user_constructor (ind1, j1) (ind2, j2) = - Int.equal j1 j2 && eq_user_ind ind1 ind2 -let eq_syntactic_constructor (ind1, j1) (ind2, j2) = - Int.equal j1 j2 && eq_syntactic_ind ind1 ind2 - -let constructor_ord (ind1, j1) (ind2, j2) = - let c = Int.compare j1 j2 in - if Int.equal c 0 then ind_ord ind1 ind2 else c -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 -let constructor_syntactic_ord (ind1, j1) (ind2, j2) = - let c = Int.compare j1 j2 in - if Int.equal c 0 then ind_syntactic_ord ind1 ind2 else c - -let constructor_hash (ind, i) = - Hashset.Combine.combine (ind_hash ind) (Int.hash i) -let constructor_user_hash (ind, i) = - Hashset.Combine.combine (ind_user_hash ind) (Int.hash 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 +let eq_ind = Ind.CanOrd.equal +let eq_user_ind = Ind.UserOrd.equal +let eq_syntactic_ind = Ind.SyntacticOrd.equal -module InductiveOrdered_env = struct - type t = inductive - let compare = ind_user_ord -end +let ind_ord = Ind.CanOrd.compare +let ind_user_ord = Ind.UserOrd.compare +let ind_syntactic_ord = Ind.SyntacticOrd.compare -module Indset = Set.Make(InductiveOrdered) -module Indset_env = Set.Make(InductiveOrdered_env) -module Indmap = Map.Make(InductiveOrdered) -module Indmap_env = Map.Make(InductiveOrdered_env) +let ind_hash = Ind.CanOrd.hash +let ind_user_hash = Ind.UserOrd.hash +let ind_syntactic_hash = Ind.SyntacticOrd.hash -module ConstructorOrdered = struct - type t = constructor - let compare = constructor_ord -end +let eq_constructor = Construct.CanOrd.equal +let eq_user_constructor = Construct.UserOrd.equal +let eq_syntactic_constructor = Construct.SyntacticOrd.equal -module ConstructorOrdered_env = struct - type t = constructor - let compare = constructor_user_ord -end +let constructor_ord = Construct.CanOrd.compare +let constructor_user_ord = Construct.UserOrd.compare +let constructor_syntactic_ord = Construct.SyntacticOrd.compare + +let constructor_hash = Construct.CanOrd.hash +let constructor_user_hash = Construct.UserOrd.hash +let constructor_syntactic_hash = Construct.SyntacticOrd.hash + +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 Constrset = Set.Make(ConstructorOrdered) -module Constrset_env = Set.Make(ConstructorOrdered_env) -module Constrmap = Map.Make(ConstructorOrdered) -module Constrmap_env = Map.Make(ConstructorOrdered_env) +module Constrset = Set.Make(Construct.CanOrd) +module Constrset_env = Set.Make(Construct.UserOrd) +module Constrmap = Map.Make(Construct.CanOrd) +module Constrmap_env = Map.Make(Construct.UserOrd) (** {6 Hash-consing of name objects } *) @@ -786,6 +850,8 @@ struct Hashset.Combine.combinesmall p.proj_arg (ind_hash p.proj_ind) module SyntacticOrd = struct + type nonrec t = t + let compare a b = let c = ind_syntactic_ord a.proj_ind b.proj_ind in if c == 0 then Int.compare a.proj_arg b.proj_arg @@ -798,6 +864,8 @@ struct Hashset.Combine.combinesmall p.proj_arg (ind_hash p.proj_ind) end module CanOrd = struct + type nonrec t = t + let compare a b = let c = ind_ord a.proj_ind b.proj_ind in if c == 0 then Int.compare a.proj_arg b.proj_arg @@ -810,6 +878,8 @@ struct Hashset.Combine.combinesmall p.proj_arg (ind_hash p.proj_ind) end module UserOrd = struct + type nonrec t = t + let compare a b = let c = ind_user_ord a.proj_ind b.proj_ind in if c == 0 then Int.compare a.proj_arg b.proj_arg @@ -876,6 +946,7 @@ struct let hash (c, b) = (if b then 0 else 1) + Repr.hash c module SyntacticOrd = struct + type nonrec t = t let compare (c, b) (c', b') = if b = b' then Repr.SyntacticOrd.compare c c' else -1 let equal (c, b as x) (c', b' as x') = @@ -883,12 +954,21 @@ struct let hash (c, b) = (if b then 0 else 1) + Repr.SyntacticOrd.hash c end module CanOrd = struct + type nonrec t = t let compare (c, b) (c', b') = if b = b' then Repr.CanOrd.compare c c' else -1 let equal (c, b as x) (c', b' as x') = x == x' || b = b' && Repr.CanOrd.equal c c' let hash (c, b) = (if b then 0 else 1) + Repr.CanOrd.hash c end + module UserOrd = struct + type nonrec t = t + let compare (c, b) (c', b') = + if b = b' then Repr.UserOrd.compare c c' else -1 + let equal (c, b as x) (c', b' as x') = + x == x' || b = b' && Repr.UserOrd.equal c c' + let hash (c, b) = (if b then 0 else 1) + Repr.UserOrd.hash c + end module Self_Hashcons = struct @@ -982,31 +1062,36 @@ module GlobRef = struct (* By default, [global_reference] are ordered on their canonical part *) - module Ordered = struct - open Constant.CanOrd + module CanOrd = struct type t = GlobRefInternal.t let compare gr1 gr2 = - GlobRefInternal.global_ord_gen compare ind_ord constructor_ord gr1 gr2 - let equal gr1 gr2 = GlobRefInternal.global_eq_gen equal eq_ind eq_constructor gr1 gr2 - let hash gr = GlobRefInternal.global_hash_gen hash ind_hash constructor_hash gr + GlobRefInternal.global_ord_gen Constant.CanOrd.compare Ind.CanOrd.compare Construct.CanOrd.compare gr1 gr2 + let equal gr1 gr2 = GlobRefInternal.global_eq_gen Constant.CanOrd.equal Ind.CanOrd.equal Construct.CanOrd.equal gr1 gr2 + let hash gr = GlobRefInternal.global_hash_gen Constant.CanOrd.hash Ind.CanOrd.hash Construct.CanOrd.hash gr end - module Ordered_env = struct - open Constant.UserOrd + module UserOrd = struct + type t = GlobRefInternal.t + let compare gr1 gr2 = + GlobRefInternal.global_ord_gen Constant.UserOrd.compare Ind.UserOrd.compare Construct.UserOrd.compare gr1 gr2 + let equal gr1 gr2 = GlobRefInternal.global_eq_gen Constant.UserOrd.equal Ind.UserOrd.equal Construct.UserOrd.equal gr1 gr2 + let hash gr = GlobRefInternal.global_hash_gen Constant.UserOrd.hash Ind.UserOrd.hash Construct.UserOrd.hash gr + end + + module SyntacticOrd = struct type t = GlobRefInternal.t let compare gr1 gr2 = - GlobRefInternal.global_ord_gen compare ind_user_ord constructor_user_ord gr1 gr2 - let equal gr1 gr2 = - GlobRefInternal.global_eq_gen equal eq_user_ind eq_user_constructor gr1 gr2 - let hash gr = GlobRefInternal.global_hash_gen hash ind_user_hash constructor_user_hash gr + GlobRefInternal.global_ord_gen Constant.SyntacticOrd.compare Ind.SyntacticOrd.compare Construct.SyntacticOrd.compare gr1 gr2 + let equal gr1 gr2 = GlobRefInternal.global_eq_gen Constant.SyntacticOrd.equal Ind.SyntacticOrd.equal Construct.SyntacticOrd.equal gr1 gr2 + let hash gr = GlobRefInternal.global_hash_gen Constant.SyntacticOrd.hash Ind.SyntacticOrd.hash Construct.SyntacticOrd.hash gr end - module Map = HMap.Make(Ordered) + module Map = HMap.Make(CanOrd) module Set = Map.Set (* Alternative sets and maps indexed by the user part of the kernel names *) - module Map_env = HMap.Make(Ordered_env) + module Map_env = HMap.Make(UserOrd) module Set_env = Map_env.Set end diff --git a/kernel/names.mli b/kernel/names.mli index ea137ad1f4..9a4ceef802 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -307,6 +307,60 @@ module KNset : CSig.SetS with type elt = KerName.t module KNpred : Predicate.S with type elt = KerName.t module KNmap : Map.ExtS with type key = KerName.t and module Set := KNset +(** {6 Signature for quotiented names} *) + +module type EqType = +sig + type t + val compare : t -> t -> int + val equal : t -> t -> bool + val hash : t -> int +end + +module type QNameS = +sig + type t + (** A type of reference that implements an implicit quotient by containing + two different names. The first one is the user name, i.e. what the user + sees when printing. The second one is the canonical name, which is the + actual absolute name of the reference. + + This mechanism is fundamentally tied to the module system of Coq. Functor + application and module inclusion are the typical ways to introduce names + where the canonical and user components differ. In particular, the two + components should be undistinguishable from the point of view of typing, + i.e. from a "kernel" ground. This aliasing only makes sense inside an + environment, but at this point this notion is not even defined so, this + dual name trick is fragile. One has to ensure many invariants when + creating such names, but the kernel is quite lenient when it comes to + checking that these invariants hold. (Read: there are soundness bugs + lurking in the module system.) + + One could enforce the invariants by splitting the names and storing that + information in the environment instead, but unfortunately, this wreaks + havoc in the upper layers. The latter are infamously not stable by + syntactic equality, in particular they might observe the difference + between canonical and user names if not packed together. + + For this reason, it is discouraged to use the canonical-accessing API + in the upper layers, notably the [CanOrd] module below. Instead, one + should use their quotiented versions defined in the [Environ] module. + Eventually all uses to [CanOrd] outside of the kernel should be removed. + + CAVEAT: name sets and maps are still exposing a canonical-accessing API + surreptitiously. *) + + module CanOrd : EqType with type t = t + (** Equality functions over the canonical name. Their use should be + restricted to the kernel. *) + + module UserOrd : EqType with type t = t + (** Equality functions over the user name. *) + + module SyntacticOrd : EqType with type t = t + (** Equality functions using both names, for low-level uses. *) +end + (** {6 Constant Names } *) module Constant: @@ -340,28 +394,12 @@ sig (** Comparisons *) - module CanOrd : sig - val compare : t -> t -> int - val equal : t -> t -> bool - val hash : t -> int - end - - module UserOrd : sig - val compare : t -> t -> int - val equal : t -> t -> bool - val hash : t -> int - end + include QNameS with type t := t - module SyntacticOrd : sig - val compare : t -> t -> int - val equal : t -> t -> bool - val hash : t -> int - end - - val equal : t -> t -> bool + val equal : t -> t -> bool [@@ocaml.deprecated "Use QConstant.equal"] (** Default comparison, alias for [CanOrd.equal] *) - val hash : t -> int + val hash : t -> int [@@ocaml.deprecated "Use QConstant.hash"] (** Hashing function *) val change_label : t -> Label.t -> t @@ -430,28 +468,12 @@ sig (** Comparisons *) - module CanOrd : sig - val compare : t -> t -> int - val equal : t -> t -> bool - val hash : t -> int - end - - module UserOrd : sig - val compare : t -> t -> int - val equal : t -> t -> bool - val hash : t -> int - end - - module SyntacticOrd : sig - val compare : t -> t -> int - val equal : t -> t -> bool - val hash : t -> int - end + include QNameS with type t := t - val equal : t -> t -> bool - (** Default comparison, alias for [CanOrd.equal] *) + val equal : t -> t -> bool [@@ocaml.deprecated "Use QMutInd.equal"] + (** Default comparison, alias for [CanOrd.equal] *) - val hash : t -> int + val hash : t -> int [@@ocaml.deprecated "Use QMutInd.hash"] (** Displaying *) @@ -473,16 +495,35 @@ 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 + + include QNameS with type t := t + +end + +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. *) +module Construct : +sig + (** Designation of a (particular) constructor of a (particular) inductive type. *) + type t = Ind.t (* designates the inductive type *) + * int (* the index of the constructor + BEWARE: indexing starts from 1. *) + + val modpath : t -> ModPath.t + + include QNameS with type t := t + +end + +type constructor = Construct.t module Indset : CSet.S with type elt = inductive module Constrset : CSet.S with type elt = constructor @@ -494,30 +535,51 @@ 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 +[@@ocaml.deprecated "Use the Construct module"] val ith_mutual_inductive : inductive -> int -> inductive 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 +[@@ocaml.deprecated "Use the Construct module"] val eq_user_constructor : constructor -> constructor -> bool +[@@ocaml.deprecated "Use the Construct module"] val eq_syntactic_constructor : constructor -> constructor -> bool +[@@ocaml.deprecated "Use the Construct module"] val constructor_ord : constructor -> constructor -> int +[@@ocaml.deprecated "Use the Construct module"] val constructor_hash : constructor -> int +[@@ocaml.deprecated "Use the Construct module"] val constructor_user_ord : constructor -> constructor -> int +[@@ocaml.deprecated "Use the Construct module"] val constructor_user_hash : constructor -> int +[@@ocaml.deprecated "Use the Construct module"] val constructor_syntactic_ord : constructor -> constructor -> int +[@@ocaml.deprecated "Use the Construct module"] val constructor_syntactic_hash : constructor -> int +[@@ocaml.deprecated "Use the Construct module"] (** {6 Hash-consing } *) @@ -558,21 +620,7 @@ module Projection : sig val make : inductive -> proj_npars:int -> proj_arg:int -> Label.t -> t - module SyntacticOrd : sig - val compare : t -> t -> int - val equal : t -> t -> bool - val hash : t -> int - end - module CanOrd : sig - val compare : t -> t -> int - val equal : t -> t -> bool - val hash : t -> int - end - module UserOrd : sig - val compare : t -> t -> int - val equal : t -> t -> bool - val hash : t -> int - end + include QNameS with type t := t val constant : t -> Constant.t (** Don't use this if you don't have to. *) @@ -583,9 +631,9 @@ module Projection : sig val arg : t -> int val label : t -> Label.t - val equal : t -> t -> bool - val hash : t -> int - val compare : t -> t -> int + val equal : t -> t -> bool [@@ocaml.deprecated "Use QProjection.equal"] + val hash : t -> int [@@ocaml.deprecated "Use QProjection.hash"] + val compare : t -> t -> int [@@ocaml.deprecated "Use QProjection.compare"] val map : (MutInd.t -> MutInd.t) -> t -> t val map_npars : (MutInd.t -> int -> MutInd.t * int) -> t -> t @@ -602,16 +650,7 @@ module Projection : sig val make : Repr.t -> bool -> t val repr : t -> Repr.t - module SyntacticOrd : sig - val compare : t -> t -> int - val equal : t -> t -> bool - val hash : t -> int - end - module CanOrd : sig - val compare : t -> t -> int - val equal : t -> t -> bool - val hash : t -> int - end + include QNameS with type t := t val constant : t -> Constant.t val mind : t -> MutInd.t @@ -623,14 +662,18 @@ module Projection : sig val unfold : t -> t val equal : t -> t -> bool + [@@ocaml.deprecated "Use QProjection.equal"] val hash : t -> int + [@@ocaml.deprecated "Use QProjection.hash"] val hcons : t -> t (** Hashconsing of projections. *) val repr_equal : t -> t -> bool + [@@ocaml.deprecated "Use an explicit projection of Repr"] (** Ignoring the unfolding boolean. *) val compare : t -> t -> int + [@@ocaml.deprecated "Use QProjection.compare"] val map : (MutInd.t -> MutInd.t) -> t -> t val map_npars : (MutInd.t -> int -> MutInd.t * int) -> t -> t @@ -656,19 +699,7 @@ module GlobRef : sig val equal : t -> t -> bool - module Ordered : sig - type nonrec t = t - val compare : t -> t -> int - val equal : t -> t -> bool - val hash : t -> int - end - - module Ordered_env : sig - type nonrec t = t - val compare : t -> t -> int - val equal : t -> t -> bool - val hash : t -> int - end + include QNameS with type t := t module Set_env : CSig.SetS with type elt = t module Map_env : Map.ExtS diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index ae070e6f8e..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.equal c1 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,9 +96,9 @@ 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.hash 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)) | Gpred (l, i) -> combinesmall 4 (combine (Option.hash Label.hash l) (Int.hash i)) | Gfixtype (l, i) -> combinesmall 5 (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) @@ -148,13 +148,13 @@ let eq_symbol sy1 sy2 = | SymbValue v1, SymbValue v2 -> (=) v1 v2 (** FIXME: how is this even valid? *) | SymbSort s1, SymbSort s2 -> Sorts.equal s1 s2 | SymbName n1, SymbName n2 -> Name.equal n1 n2 - | SymbConst kn1, SymbConst kn2 -> Constant.equal kn1 kn2 + | 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 = @@ -162,13 +162,13 @@ let hash_symbol symb = | SymbValue v -> combinesmall 1 (Hashtbl.hash v) (** FIXME *) | SymbSort s -> combinesmall 2 (Sorts.hash s) | SymbName name -> combinesmall 3 (Name.hash name) - | SymbConst c -> combinesmall 4 (Constant.hash c) + | 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 fc6afb79d4..76215b4386 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -80,17 +80,17 @@ 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.equal c1 c2 then convert_instances ~flex:true u1 u2 cu + if Constant.CanOrd.equal c1 c2 then convert_instances ~flex:true u1 u2 cu else raise NotConvertible | Asort s1, Asort s2 -> sort_cmp_universes env pb s1 s2 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/nativelambda.ml b/kernel/nativelambda.ml index 99090f0147..e98e97907a 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -433,8 +433,8 @@ module Cache = module ConstrHash = struct type t = constructor - let equal = eq_constructor - let hash = constructor_hash + let equal = Construct.CanOrd.equal + let hash = Construct.CanOrd.hash end module ConstrTable = Hashtbl.Make(ConstrHash) 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 f158cfacea..f0b4d6d362 100644 --- a/kernel/primred.ml +++ b/kernel/primred.ml @@ -12,11 +12,11 @@ type _ action_kind = type exn += IncompatibleDeclarations : 'a action_kind * 'a * 'a -> exn let check_same_types typ c1 c2 = - if not (Constant.equal c1 c2) + if not (Constant.CanOrd.equal 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 96bf370342..5589ae3483 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -283,7 +283,7 @@ let convert_constructors ctor nargs u1 u2 (s, check) = let conv_table_key infos k1 k2 cuniv = if k1 == k2 then cuniv else match k1, k2 with - | ConstKey (cst, u), ConstKey (cst', u') when Constant.equal cst cst' -> + | ConstKey (cst, u), ConstKey (cst', u') when Constant.CanOrd.equal cst cst' -> if Univ.Instance.equal u u' then cuniv else let flex = evaluable_constant cst (info_env infos) @@ -441,7 +441,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | Some s2 -> eqappr cv_pb l2r infos appr1 (lft2, (c2, (s2 :: v2))) cuniv | None -> - if Projection.Repr.equal (Projection.repr p1) (Projection.repr p2) + if Projection.Repr.CanOrd.equal (Projection.repr p1) (Projection.repr p2) && compare_stack_shape v1 v2 then let el1 = el_stack lft1 v1 in let el2 = el_stack lft2 v2 in @@ -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 @@ -704,14 +704,14 @@ and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv = | (Zlapp a1,Zlapp a2) -> Array.fold_right2 f a1 a2 cu1 | (Zlproj (c1,_l1),Zlproj (c2,_l2)) -> - if not (Projection.Repr.equal c1 c2) then + if not (Projection.Repr.CanOrd.equal c1 c2) then raise NotConvertible else cu1 | (Zlfix(fx1,a1),Zlfix(fx2,a2)) -> 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/subtyping.ml b/kernel/subtyping.ml index 76a1c190be..1a4c786e43 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -182,7 +182,7 @@ 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' || - MutInd.equal (mind_of_delta_kn reso1 kn1) + MutInd.CanOrd.equal (mind_of_delta_kn reso1 kn1) (subst_mind subst2 (MutInd.make kn2 kn2')) then () else error NotEqualInductiveAliases 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 948195797e..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 @@ -141,7 +141,7 @@ and conv_stack env k stk1 stk2 cu = conv_stack env k stk1 stk2 !rcu else raise NotConvertible | Zproj p1 :: stk1, Zproj p2 :: stk2 -> - if Projection.Repr.equal p1 p2 then conv_stack env k stk1 stk2 cu + if Projection.Repr.CanOrd.equal p1 p2 then conv_stack env k stk1 stk2 cu else raise NotConvertible | [], _ | Zapp _ :: _, _ | Zfix _ :: _, _ | Zswitch _ :: _, _ | Zproj _ :: _, _ -> raise NotConvertible diff --git a/kernel/vmemitcodes.ml b/kernel/vmemitcodes.ml index ec8601edc9..babc57794b 100644 --- a/kernel/vmemitcodes.ml +++ b/kernel/vmemitcodes.ml @@ -36,9 +36,9 @@ let eq_reloc_info r1 r2 = match r1, r2 with | Reloc_annot _, _ -> false | Reloc_const c1, Reloc_const c2 -> eq_structured_constant c1 c2 | Reloc_const _, _ -> false -| Reloc_getglobal c1, Reloc_getglobal c2 -> Constant.equal c1 c2 +| Reloc_getglobal c1, Reloc_getglobal c2 -> Constant.CanOrd.equal c1 c2 | Reloc_getglobal _, _ -> false -| Reloc_proj_name p1, Reloc_proj_name p2 -> Projection.Repr.equal p1 p2 +| Reloc_proj_name p1, Reloc_proj_name p2 -> Projection.Repr.CanOrd.equal p1 p2 | Reloc_proj_name _, _ -> false | Reloc_caml_prim p1, Reloc_caml_prim p2 -> CPrimitives.equal p1 p2 | Reloc_caml_prim _, _ -> false @@ -48,8 +48,8 @@ let hash_reloc_info r = match r with | Reloc_annot sw -> combinesmall 1 (hash_annot_switch sw) | Reloc_const c -> combinesmall 2 (hash_structured_constant c) - | Reloc_getglobal c -> combinesmall 3 (Constant.hash c) - | Reloc_proj_name p -> combinesmall 4 (Projection.Repr.hash p) + | Reloc_getglobal c -> combinesmall 3 (Constant.CanOrd.hash c) + | Reloc_proj_name p -> combinesmall 4 (Projection.Repr.CanOrd.hash p) | Reloc_caml_prim p -> combinesmall 5 (CPrimitives.hash p) module RelocTable = Hashtbl.Make(struct diff --git a/kernel/vmsymtable.ml b/kernel/vmsymtable.ml index 9d80dc578b..ae0fa38571 100644 --- a/kernel/vmsymtable.ml +++ b/kernel/vmsymtable.ml @@ -85,7 +85,7 @@ module AnnotTable = Hashtbl.Make (struct let hash = hash_annot_switch end) -module ProjNameTable = Hashtbl.Make (Projection.Repr) +module ProjNameTable = Hashtbl.Make (Projection.Repr.CanOrd) let str_cst_tbl : int SConstTable.t = SConstTable.create 31 diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index 2068133b10..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) @@ -250,7 +250,7 @@ type id_key = | EvarKey of Evar.t let eq_id_key (k1 : id_key) (k2 : id_key) = match k1, k2 with -| ConstKey c1, ConstKey c2 -> Constant.equal c1 c2 +| ConstKey c1, ConstKey c2 -> Constant.CanOrd.equal c1 c2 | VarKey id1, VarKey id2 -> Id.equal id1 id2 | RelKey n1, RelKey n2 -> Int.equal n1 n2 | EvarKey evk1, EvarKey evk2 -> Evar.equal evk1 evk2 @@ -469,7 +469,7 @@ struct let equal = eq_id_key open Hashset.Combine let hash : t -> tag = function - | ConstKey c -> combinesmall 1 (Constant.hash c) + | ConstKey c -> combinesmall 1 (Constant.CanOrd.hash c) | VarKey id -> combinesmall 2 (Id.hash id) | RelKey i -> combinesmall 3 (Int.hash i) | EvarKey evk -> combinesmall 4 (Evar.hash evk) |