diff options
| -rw-r--r-- | kernel/constr.ml | 20 | ||||
| -rw-r--r-- | kernel/cooking.ml | 12 | ||||
| -rw-r--r-- | kernel/names.ml | 42 | ||||
| -rw-r--r-- | kernel/names.mli | 26 |
4 files changed, 81 insertions, 19 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml index e2b1d3fd9..043663f53 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -732,12 +732,10 @@ 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) -> Evar.equal e1 e2 && array_eqeq l1 l2 + | Evar (e1,l1), Evar (e2,l2) -> e1 == e2 && array_eqeq l1 l2 | Const (c1,u1), Const (c2,u2) -> c1 == c2 && 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 + | Ind (ind1,u1), Ind (ind2,u2) -> ind1 == ind2 && u1 == u2 + | Construct (cstr1,u1), Construct (cstr2,u2) -> cstr1 == cstr2 && 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)) -> @@ -815,19 +813,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.hash p') hc)) + (Proj (p', c), combinesmall 17 (combine (Projection.SyntacticOrd.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.hash c) hu)) - | Ind ((kn,i) as ind,u) -> + (Const (c', u'), combinesmall 9 (combine (Constant.SyntacticOrd.hash c) hu)) + | Ind (ind,u) -> let u', hu = sh_instance u in (Ind (sh_ind ind, u'), - combinesmall 10 (combine (ind_hash ind) hu)) - | Construct ((((kn,i),j) as c,u))-> + combinesmall 10 (combine (ind_syntactic_hash ind) hu)) + | Construct (c,u) -> let u', hu = sh_instance u in (Construct (sh_construct c, u'), - combinesmall 11 (combine (constructor_hash c) hu)) + combinesmall 11 (combine (constructor_syntactic_hash c) hu)) | Case (ci,p,c,bl) -> let p, hp = sh_rec p and c, hc = sh_rec c in diff --git a/kernel/cooking.ml b/kernel/cooking.ml index be71bd7b4..9849f156c 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.CanOrd.equal c1 c2 - | IndRef i1, IndRef i2 -> eq_ind i1 i2 - | ConstructRef c1, ConstructRef c2 -> eq_constructor c1 c2 + | 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 | _ -> false open Hashset.Combine let hash = function - | ConstRef c -> combinesmall 1 (Constant.hash c) - | IndRef i -> combinesmall 2 (ind_hash i) - | ConstructRef c -> combinesmall 3 (constructor_hash c) + | ConstRef c -> combinesmall 1 (Constant.SyntacticOrd.hash c) + | IndRef i -> combinesmall 2 (ind_syntactic_hash i) + | ConstructRef c -> combinesmall 3 (constructor_syntactic_hash c) end module RefTable = Hashtbl.Make(RefHash) diff --git a/kernel/names.ml b/kernel/names.ml index ae2b3b638..bc3393208 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -477,7 +477,7 @@ module KerPair = struct | Dual (kn,_) -> kn let same kn = Same kn - let make knu knc = if knu == knc then Same knc else Dual (knu,knc) + let make knu knc = if KerName.equal knu knc then Same knc else Dual (knu,knc) let make1 = same let make2 mp l = same (KerName.make2 mp l) @@ -524,6 +524,23 @@ 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 @@ -590,6 +607,8 @@ 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 @@ -597,15 +616,22 @@ 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 @@ -613,11 +639,16 @@ 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 @@ -805,6 +836,15 @@ 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 diff --git a/kernel/names.mli b/kernel/names.mli index 7cc444375..9a8977c92 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -305,6 +305,12 @@ 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] *) @@ -379,6 +385,12 @@ 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] *) @@ -417,16 +429,22 @@ 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_user_ord : constructor -> constructor -> int val constructor_hash : constructor -> int +val constructor_user_ord : constructor -> 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 = @@ -640,6 +658,12 @@ 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 |