Make hash_kind and hcons produce the same hashes

kernel/hConstr.ml

@@ -240,28 +240,28 @@ let rec hash_term (t : t) =
     let u, hu = Instance.share u in
     let pms,hpms = hash_term_array pms in
     let p, hp = hcons_ctx p in
-    let iv, hiv = sh_invert iv in
+    let iv, _hiv = sh_invert iv in
     let c, hc = sh_rec c in
     let fold accu c =
       let c, h = hcons_ctx c in
       combine accu h, c
     in
     let hbl, bl = Array.fold_left_map fold 0 bl in
-    let hbl = combine (combine hc (combine hiv (combine hpms (combine hu hp)))) hbl in
-    (Case (hcons_caseinfo ci, u, pms, (p,r), iv, c, bl), combinesmall 12 hbl)
+    let h = combine5 hu hc hpms hp hbl in
+    (Case (hcons_caseinfo ci, u, pms, (p,r), iv, c, bl), combinesmall 12 h)
   | Fix (ln,(lna,tl,bl)) ->
     let bl,hbl = hash_term_array bl in
     let tl,htl = hash_term_array tl in
     let () = Array.iteri (fun i x -> Array.unsafe_set lna i (hcons_annot x)) lna in
-    let fold accu na = combine (hash_annot na) accu in
+    let fold accu na = combine accu (hash_annot na) in
     let hna = Array.fold_left fold 0 lna in
     let h = combine3 hna hbl htl in
     (Fix (ln,(lna,tl,bl)), combinesmall 13 h)
   | CoFix(ln,(lna,tl,bl)) ->
     let bl,hbl = hash_term_array bl in
     let tl,htl = hash_term_array tl in
     let () = Array.iteri (fun i x -> Array.unsafe_set lna i (hcons_annot x)) lna in
-    let fold accu na = combine (hash_annot na) accu in
+    let fold accu na = combine accu (hash_annot na) in
     let hna = Array.fold_left fold 0 lna in
     let h = combine3 hna hbl htl in
     (CoFix (ln,(lna,tl,bl)), combinesmall 14 h)
@@ -273,9 +273,7 @@ let rec hash_term (t : t) =
     let c, hc = sh_rec c in
     let p' = Projection.hcons p in
     (Proj (p', r, c), combinesmall 17 (combine (Projection.SyntacticOrd.hash p') hc))
-  | Int i as t ->
-    let (h,l) = Uint63.to_int2 i in
-    (t, combinesmall 18 (combine h l))
+  | Int i as t -> (t, combinesmall 18 (Uint63.hash i))
   | Float f as t -> (t, combinesmall 19 (Float64.hash f))
   | Array (u,t,def,ty) ->
     let u, hu = Instance.share u in
@@ -533,20 +531,20 @@ let hash_kind = let open Hashset.Combine in function
   | Prod (na,t,c) -> combinesmall 4 (combine3 (hash_annot na) t.hash c.hash)
   | Lambda (na,t,c) -> combinesmall 5 (combine3 (hash_annot na) t.hash c.hash)
   | LetIn (na,b,t,c) -> combinesmall 6 (combine4 (hash_annot na) b.hash t.hash c.hash)
-  | App (h,args) -> combinesmall 7 (Array.fold_left (fun hash c -> combine hash c.hash) h.hash args)
+  | App (h,args) ->
+    combinesmall 7 (combine (hash_array hash args) h.hash)
   | Evar _ -> assert false
   | Const (c,u) -> combinesmall 9 (combine (Constant.SyntacticOrd.hash c) (Instance.hash u))
   | Ind (ind,u) -> combinesmall 10 (combine (Ind.SyntacticOrd.hash ind) (Instance.hash u))
   | Construct (c,u) -> combinesmall 11 (combine (Construct.SyntacticOrd.hash c) (Instance.hash u))
   | Case (_,u,pms,(p,_),_,c,bl) ->
     let hash_ctx (bnd,c) =
-      Array.fold_left (fun hash na -> combine (hash_annot na) hash) c.hash bnd
+      let hna = hash_array hash_annot bnd in
+      combine hna c.hash
     in
     let hpms = hash_array hash pms in
     let hbl = hash_array hash_ctx bl in
-    let h = combine5 (Instance.hash u)
-        c.hash hpms (hash_ctx p) hbl
-    in
+    let h = combine5 (Instance.hash u) c.hash hpms (hash_ctx p) hbl in
     combinesmall 12 h
   | Fix (_,(lna,tl,bl)) ->
     combinesmall 13 (combine3 (hash_array hash_annot lna) (hash_array hash tl) (hash_array hash bl))