diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/constr.ml | 28 | ||||
| -rw-r--r-- | kernel/cooking.ml | 12 | ||||
| -rw-r--r-- | kernel/environ.ml | 2 | ||||
| -rw-r--r-- | kernel/names.ml | 58 | ||||
| -rw-r--r-- | kernel/names.mli | 26 | ||||
| -rw-r--r-- | kernel/sorts.ml | 2 | ||||
| -rw-r--r-- | kernel/univ.ml | 22 |
7 files changed, 44 insertions, 106 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml index 644f866b35..e2b1d3fd9c 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -732,10 +732,12 @@ let hasheq t1 t2 = n1 == n2 && b1 == b2 && t1 == t2 && c1 == c2 | App (c1,l1), App (c2,l2) -> c1 == c2 && array_eqeq l1 l2 | Proj (p1,c1), Proj(p2,c2) -> p1 == p2 && c1 == c2 - | Evar (e1,l1), Evar (e2,l2) -> e1 == e2 && array_eqeq l1 l2 + | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && array_eqeq l1 l2 | Const (c1,u1), Const (c2,u2) -> c1 == c2 && u1 == u2 - | Ind (ind1,u1), Ind (ind2,u2) -> ind1 == ind2 && u1 == u2 - | Construct (cstr1,u1), Construct (cstr2,u2) -> cstr1 == cstr2 && u1 == u2 + | Ind ((sp1,i1),u1), Ind ((sp2,i2),u2) -> + sp1 == sp2 && Int.equal i1 i2 && u1 == u2 + | Construct (((sp1,i1),j1),u1), Construct (((sp2,i2),j2),u2) -> + sp1 == sp2 && Int.equal i1 i2 && Int.equal j1 j2 && u1 == u2 | Case (ci1,p1,c1,bl1), Case (ci2,p2,c2,bl2) -> ci1 == ci2 && p1 == p2 && c1 == c2 && array_eqeq bl1 bl2 | Fix ((ln1, i1),(lna1,tl1,bl1)), Fix ((ln2, i2),(lna2,tl2,bl2)) -> @@ -755,10 +757,10 @@ let hasheq t1 t2 = once and for all the table we'll use for hash-consing all constr *) module HashsetTerm = - Hashset.Make(struct type t = constr let eq = hasheq end) + Hashset.Make(struct type t = constr let equal = hasheq end) module HashsetTermArray = - Hashset.Make(struct type t = constr array let eq = array_eqeq end) + Hashset.Make(struct type t = constr array let equal = array_eqeq end) let term_table = HashsetTerm.create 19991 (* The associative table to hashcons terms. *) @@ -813,19 +815,19 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) = | Proj (p,c) -> let c, hc = sh_rec c in let p' = Projection.hcons p in - (Proj (p', c), combinesmall 17 (combine (Projection.SyntacticOrd.hash p') hc)) + (Proj (p', c), combinesmall 17 (combine (Projection.hash p') hc)) | Const (c,u) -> let c' = sh_con c in let u', hu = sh_instance u in - (Const (c', u'), combinesmall 9 (combine (Constant.SyntacticOrd.hash c) hu)) - | Ind (ind,u) -> + (Const (c', u'), combinesmall 9 (combine (Constant.hash c) hu)) + | Ind ((kn,i) as ind,u) -> let u', hu = sh_instance u in (Ind (sh_ind ind, u'), - combinesmall 10 (combine (ind_syntactic_hash ind) hu)) - | Construct (c,u) -> + combinesmall 10 (combine (ind_hash ind) hu)) + | Construct ((((kn,i),j) as 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 (constructor_hash c) hu)) | Case (ci,p,c,bl) -> let p, hp = sh_rec p and c, hc = sh_rec c in @@ -928,7 +930,7 @@ struct List.equal (==) info1.ind_tags info2.ind_tags && Array.equal (List.equal (==)) info1.cstr_tags info2.cstr_tags && info1.style == info2.style - let eq ci ci' = + let equal ci ci' = ci.ci_ind == ci'.ci_ind && Int.equal ci.ci_npar ci'.ci_npar && Array.equal Int.equal ci.ci_cstr_ndecls ci'.ci_cstr_ndecls && (* we use [Array.equal] on purpose *) @@ -970,7 +972,7 @@ module Hsorts = let hashcons huniv = function Prop c -> Prop c | Type u -> Type (huniv u) - let eq s1 s2 = + let equal s1 s2 = s1 == s2 || match (s1,s2) with (Prop c1, Prop c2) -> c1 == c2 diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 9849f156c9..be71bd7b41 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -44,15 +44,15 @@ module RefHash = 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 + | ConstRef c1, ConstRef c2 -> Constant.CanOrd.equal c1 c2 + | IndRef i1, IndRef i2 -> eq_ind i1 i2 + | ConstructRef c1, ConstructRef c2 -> eq_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) - | ConstructRef c -> combinesmall 3 (constructor_syntactic_hash c) + | ConstRef c -> combinesmall 1 (Constant.hash c) + | IndRef i -> combinesmall 2 (ind_hash i) + | ConstructRef c -> combinesmall 3 (constructor_hash c) end module RefTable = Hashtbl.Make(RefHash) diff --git a/kernel/environ.ml b/kernel/environ.ml index 109e3830c2..30b28177c9 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -162,7 +162,7 @@ let reset_context = reset_with_named_context empty_named_context_val let pop_rel_context n env = let ctxt = env.env_rel_context in { env with - env_rel_context = List.skipn n ctxt; + env_rel_context = List.firstn (List.length ctxt - n) ctxt; env_nb_rel = env.env_nb_rel - n } let fold_named_context f env ~init = diff --git a/kernel/names.ml b/kernel/names.ml index a99702d159..ae2b3b6389 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -102,7 +102,7 @@ struct let hashcons hident = function | Name id -> Name (hident id) | n -> n - let eq n1 n2 = + let equal n1 n2 = n1 == n2 || match (n1,n2) with | (Name id1, Name id2) -> id1 == id2 @@ -236,7 +236,7 @@ struct type t = _t type u = (Id.t -> Id.t) * (DirPath.t -> DirPath.t) let hashcons (hid,hdir) (n,s,dir) = (n,hid s,hdir dir) - let eq ((n1,s1,dir1) as x) ((n2,s2,dir2) as y) = + let equal ((n1,s1,dir1) as x) ((n2,s2,dir2) as y) = (x == y) || (Int.equal n1 n2 && s1 == s2 && dir1 == dir2) let hash = hash @@ -327,7 +327,7 @@ module ModPath = struct | MPfile dir -> MPfile (hdir dir) | MPbound m -> MPbound (huniqid m) | MPdot (md,l) -> MPdot (hashcons hfuns md, hstr l) - let rec eq d1 d2 = + let rec equal d1 d2 = d1 == d2 || match d1,d2 with | MPfile dir1, MPfile dir2 -> dir1 == dir2 @@ -423,7 +423,7 @@ module KerName = struct let hashcons (hmod,hdir,hstr) kn = let { modpath = mp; dirpath = dp; knlabel = l; refhash; } = kn in { modpath = hmod mp; dirpath = hdir dp; knlabel = hstr l; refhash; canary; } - let eq kn1 kn2 = + let equal kn1 kn2 = kn1.modpath == kn2.modpath && kn1.dirpath == kn2.dirpath && kn1.knlabel == kn2.knlabel let hash = hash @@ -477,7 +477,7 @@ module KerPair = struct | Dual (kn,_) -> kn let same kn = Same kn - let make knu knc = if KerName.equal knu knc then Same knc else Dual (knu,knc) + let make knu knc = if knu == knc then Same knc else Dual (knu,knc) let make1 = same let make2 mp l = same (KerName.make2 mp l) @@ -524,23 +524,6 @@ module KerPair = struct let hash x = KerName.hash (canonical x) 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) -> - let c = KerName.compare knux knuy in - if not (Int.equal c 0) then c - else KerName.compare kncx kncy - | Same _, _ -> -1 - | Dual _, _ -> 1 - let equal x y = x == y || compare x y = 0 - let hash = function - | Same kn -> KerName.hash kn - | Dual (knu, knc) -> - Hashset.Combine.combine (KerName.hash knu) (KerName.hash knc) - end - (** Default (logical) comparison and hash is on the canonical part *) let equal = CanOrd.equal let hash = CanOrd.hash @@ -552,7 +535,7 @@ module KerPair = struct let hashcons hkn = function | Same kn -> Same (hkn kn) | Dual (knu,knc) -> make (hkn knu) (hkn knc) - let eq x y = (* physical comparison on subterms *) + let equal x y = (* physical comparison on subterms *) x == y || match x,y with | Same x, Same y -> x == y @@ -607,8 +590,6 @@ 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 @@ -616,22 +597,15 @@ let ind_ord (m1, i1) (m2, i2) = 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 @@ -639,16 +613,11 @@ let constructor_ord (ind1, j1) (ind2, j2) = 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 @@ -693,7 +662,7 @@ module Hind = Hashcons.Make( type t = inductive type u = MutInd.t -> MutInd.t let hashcons hmind (mind, i) = (hmind mind, i) - let eq (mind1,i1) (mind2,i2) = mind1 == mind2 && Int.equal i1 i2 + let equal (mind1,i1) (mind2,i2) = mind1 == mind2 && Int.equal i1 i2 let hash = ind_hash end) @@ -702,7 +671,7 @@ module Hconstruct = Hashcons.Make( type t = constructor type u = inductive -> inductive let hashcons hind (ind, j) = (hind ind, j) - let eq (ind1, j1) (ind2, j2) = ind1 == ind2 && Int.equal j1 j2 + let equal (ind1, j1) (ind2, j2) = ind1 == ind2 && Int.equal j1 j2 let hash = constructor_hash end) @@ -836,22 +805,13 @@ struct let hash (c, b) = (if b then 0 else 1) + Constant.hash c - module SyntacticOrd = struct - type t = constant * bool - let compare (c, b) (c', b') = - if b = b' then Constant.SyntacticOrd.compare c c' else -1 - let equal (c, b as x) (c', b' as x') = - x == x' || b = b' && Constant.SyntacticOrd.equal c c' - let hash (c, b) = (if b then 0 else 1) + Constant.SyntacticOrd.hash c - end - module Self_Hashcons = struct type _t = t type t = _t type u = Constant.t -> Constant.t let hashcons hc (c,b) = (hc c,b) - let eq ((c,b) as x) ((c',b') as y) = + let equal ((c,b) as x) ((c',b') as y) = x == y || (c == c' && b == b') let hash = hash end diff --git a/kernel/names.mli b/kernel/names.mli index 9a8977c92f..7cc4443752 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -305,12 +305,6 @@ sig val hash : t -> int end - module SyntacticOrd : sig - val compare : t -> t -> int - val equal : t -> t -> bool - val hash : t -> int - end - val equal : t -> t -> bool (** Default comparison, alias for [CanOrd.equal] *) @@ -385,12 +379,6 @@ sig val hash : t -> int end - module SyntacticOrd : sig - val compare : t -> t -> int - val equal : t -> t -> bool - val hash : t -> int - end - val equal : t -> t -> bool (** Default comparison, alias for [CanOrd.equal] *) @@ -429,22 +417,16 @@ val inductive_of_constructor : constructor -> inductive val index_of_constructor : constructor -> int val eq_ind : inductive -> inductive -> bool val eq_user_ind : inductive -> inductive -> bool -val eq_syntactic_ind : inductive -> inductive -> bool val ind_ord : inductive -> inductive -> int val ind_hash : inductive -> int val ind_user_ord : inductive -> inductive -> int val ind_user_hash : inductive -> int -val ind_syntactic_ord : inductive -> inductive -> int -val ind_syntactic_hash : inductive -> int val eq_constructor : constructor -> constructor -> bool val eq_user_constructor : constructor -> constructor -> bool -val eq_syntactic_constructor : constructor -> constructor -> bool val constructor_ord : constructor -> constructor -> int -val constructor_hash : constructor -> int val constructor_user_ord : constructor -> constructor -> int +val constructor_hash : constructor -> int val constructor_user_hash : constructor -> int -val constructor_syntactic_ord : constructor -> constructor -> int -val constructor_syntactic_hash : constructor -> int (** Better to have it here that in Closure, since required in grammar.cma *) type evaluable_global_reference = @@ -658,12 +640,6 @@ module Projection : sig val make : constant -> bool -> t - module SyntacticOrd : sig - val compare : t -> t -> int - val equal : t -> t -> bool - val hash : t -> int - end - val constant : t -> constant val unfolded : t -> bool val unfold : t -> t diff --git a/kernel/sorts.ml b/kernel/sorts.ml index 2baf9b1335..e2854abfd3 100644 --- a/kernel/sorts.ml +++ b/kernel/sorts.ml @@ -98,7 +98,7 @@ module Hsorts = let u' = huniv u in if u' == u then c else Type u' | s -> s - let eq s1 s2 = match (s1,s2) with + let equal s1 s2 = match (s1,s2) with | (Prop c1, Prop c2) -> c1 == c2 | (Type u1, Type u2) -> u1 == u2 |_ -> false diff --git a/kernel/univ.ml b/kernel/univ.ml index 09a64d1b09..336cdb653e 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -35,7 +35,7 @@ module type Hashconsed = sig type t val hash : t -> int - val eq : t -> t -> bool + val equal : t -> t -> bool val hcons : t -> t end @@ -53,7 +53,7 @@ struct type t = _t type u = (M.t -> M.t) let hash = function Nil -> 0 | Cons (_, h, _) -> h - let eq l1 l2 = match l1, l2 with + let equal l1 l2 = match l1, l2 with | Nil, Nil -> true | Cons (x1, _, l1), Cons (x2, _, l2) -> x1 == x2 && l1 == l2 | _ -> false @@ -135,12 +135,12 @@ module HList = struct let rec remove x = function | Nil -> nil | Cons (y, _, l) -> - if H.eq x y then l + if H.equal x y then l else cons y (remove x l) let rec mem x = function | Nil -> false - | Cons (y, _, l) -> H.eq x y || mem x l + | Cons (y, _, l) -> H.equal x y || mem x l let rec compare cmp l1 l2 = match l1, l2 with | Nil, Nil -> 0 @@ -251,7 +251,7 @@ module Level = struct type _t = t type t = _t type u = unit - let eq x y = x.hash == y.hash && RawLevel.hequal x.data y.data + let equal x y = x.hash == y.hash && RawLevel.hequal x.data y.data let hash x = x.hash let hashcons () x = let data' = RawLevel.hcons x.data in @@ -398,7 +398,7 @@ struct let hashcons hdir (b,n as x) = let b' = hdir b in if b' == b then x else (b',n) - let eq l1 l2 = + let equal l1 l2 = l1 == l2 || match l1,l2 with | (b,n), (b',n') -> b == b' && n == n' @@ -417,7 +417,7 @@ struct let hcons = Hashcons.simple_hcons H.generate H.hcons Level.hcons let hash = ExprHash.hash - let eq x y = x == y || + let equal x y = x == y || (let (u,n) = x and (v,n') = y in Int.equal n n' && Level.equal u v) @@ -1293,7 +1293,7 @@ module Hconstraint = type t = univ_constraint type u = universe_level -> universe_level let hashcons hul (l1,k,l2) = (hul l1, k, hul l2) - let eq (l1,k,l2) (l1',k',l2') = + let equal (l1,k,l2) (l1',k',l2') = l1 == l1' && k == k' && l2 == l2' let hash = Hashtbl.hash end) @@ -1305,7 +1305,7 @@ module Hconstraints = type u = univ_constraint -> univ_constraint let hashcons huc s = Constraint.fold (fun x -> Constraint.add (huc x)) s Constraint.empty - let eq s s' = + let equal s s' = List.for_all2eq (==) (Constraint.elements s) (Constraint.elements s') @@ -1676,7 +1676,7 @@ struct a end - let eq t1 t2 = + let equal t1 t2 = t1 == t2 || (Int.equal (Array.length t1) (Array.length t2) && let rec aux i = @@ -2043,7 +2043,7 @@ module Huniverse_set = type u = universe_level -> universe_level let hashcons huc s = LSet.fold (fun x -> LSet.add (huc x)) s LSet.empty - let eq s s' = + let equal s s' = LSet.equal s s' let hash = Hashtbl.hash end) |