Adding eq/compare/hash for syntactic view at

constant/inductive/constructor kernel_name pairs rather than viewing
them from only the user or canonical part.

Hopefully more uniformity in Constr.hasheq (using systematically == on
subterms).

A semantic change: Cooking now indexing again on full pairs of kernel
names rather than only on the canonical names, so as to preserve user
name.

Also, in pair of kernel names, ensuring the compact representation is
used as soon as both names are the same.

4 files changed, 81 insertions, 19 deletions

diff --git a/kernel/constr.ml b/kernel/constr.ml
index 7e103b1da..2a80cf201 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 f0e925582..9476e8a83 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 f5d954e9c..e9cb9fd74 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 1e79f4dde..6cfbca7ba 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -307,6 +307,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] *)
 
@@ -381,6 +387,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] *)
 
@@ -419,16 +431,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 =
@@ -642,6 +660,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