Generalize type of compare_head_with functions

2 files changed, 45 insertions, 32 deletions

diff --git a/kernel/constr.ml b/kernel/constr.ml
index b25f38d630..c97969c0e0 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -237,6 +237,17 @@ let mkVar id = Var id
 
 let kind c = c
 
+let rec kind_nocast_gen kind c =
+  match kind c with
+  | Cast (c, _, _) -> kind_nocast_gen kind c
+  | App (h, outer) as k ->
+    (match kind_nocast_gen kind h with
+     | App (h, inner) -> App (h, Array.append inner outer)
+     | _ -> k)
+  | k -> k
+
+let kind_nocast c = kind_nocast_gen kind c
+
 (* The other way around. We treat specifically smart constructors *)
 let of_kind = function
 | App (f, a) -> mkApp (f, a)
@@ -755,10 +766,10 @@ let map_with_binders g f l c0 = match kind c0 with
     let bl' = Array.Fun1.Smart.map f l' bl in
     mkCoFix (ln,(lna,tl',bl'))
 
-type instance_compare_fn = GlobRef.t -> int ->
-  Univ.Instance.t -> Univ.Instance.t -> bool
+type 'univs instance_compare_fn = GlobRef.t -> int ->
+  'univs -> 'univs -> bool
 
-type constr_compare_fn = int -> constr -> constr -> bool
+type 'constr constr_compare_fn = int -> 'constr -> 'constr -> bool
 
 (* [compare_head_gen_evar k1 k2 u s e eq leq c1 c2] compare [c1] and
    [c2] (using [k1] to expose the structure of [c1] and [k2] to expose
@@ -772,19 +783,16 @@ type constr_compare_fn = int -> constr -> constr -> bool
    calls to {!Array.equal_norefl}). *)
 
 let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t1 t2 =
-  match kind1 t1, kind2 t2 with
+  match kind_nocast_gen kind1 t1, kind_nocast_gen kind2 t2 with
+  | Cast _, _ | _, Cast _ -> assert false (* kind_nocast *)
   | Rel n1, Rel n2 -> Int.equal n1 n2
   | Meta m1, Meta m2 -> Int.equal m1 m2
   | Var id1, Var id2 -> Id.equal id1 id2
   | Sort s1, Sort s2 -> leq_sorts s1 s2
-  | Cast (c1, _, _), _ -> leq nargs c1 t2
-  | _, Cast (c2, _, _) -> leq nargs t1 c2
   | Prod (_,t1,c1), Prod (_,t2,c2) -> eq 0 t1 t2 && leq 0 c1 c2
   | Lambda (_,t1,c1), Lambda (_,t2,c2) -> eq 0 t1 t2 && eq 0 c1 c2
   | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> eq 0 b1 b2 && eq 0 t1 t2 && leq nargs c1 c2
   (* Why do we suddenly make a special case for Cast here? *)
-  | App (Cast (c1, _, _), l1), _ -> leq nargs (mkApp (c1, l1)) t2
-  | _, App (Cast (c2, _, _), l2) -> leq nargs t1 (mkApp (c2, l2))
   | App (c1, l1), App (c2, l2) ->
     let len = Array.length l1 in
     Int.equal len (Array.length l2) &&
diff --git a/kernel/constr.mli b/kernel/constr.mli
index ea38dabd5c..2efdae007c 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -241,6 +241,11 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term =
 val kind : constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term
 val of_kind : (constr, types, Sorts.t, Univ.Instance.t) kind_of_term -> constr
 
+val kind_nocast_gen : ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) ->
+  ('v -> ('v, 'v, 'sort, 'univs) kind_of_term)
+
+val kind_nocast : constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term
+
 (** {6 Simple case analysis} *)
 val isRel  : constr -> bool
 val isRelN : int -> constr -> bool
@@ -518,50 +523,50 @@ val iter_with_binders :
 val fold_constr_with_binders :
   ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b
 
-type constr_compare_fn = int -> constr -> constr -> bool
+type 'constr constr_compare_fn = int -> 'constr -> 'constr -> bool
 
 (** [compare_head f c1 c2] compare [c1] and [c2] using [f] to compare
    the immediate subterms of [c1] of [c2] if needed; Cast's, binders
    name and Cases annotations are not taken into account *)
 
-val compare_head : constr_compare_fn -> constr_compare_fn
+val compare_head : constr constr_compare_fn -> constr constr_compare_fn
 
 (** Convert a global reference applied to 2 instances. The int says
    how many arguments are given (as we can only use cumulativity for
    fully applied inductives/constructors) .*)
-type instance_compare_fn = GlobRef.t -> int ->
-  Univ.Instance.t -> Univ.Instance.t -> bool
+type 'univs instance_compare_fn = GlobRef.t -> int ->
+  'univs -> 'univs -> bool
 
 (** [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to
    compare the immediate subterms of [c1] of [c2] if needed, [u] to
    compare universe instances, [s] to compare sorts; Cast's, binders
    name and Cases annotations are not taken into account *)
 
-val compare_head_gen : instance_compare_fn ->
+val compare_head_gen : Univ.Instance.t instance_compare_fn ->
   (Sorts.t -> Sorts.t -> bool) ->
-  constr_compare_fn ->
-  constr_compare_fn
+  constr constr_compare_fn ->
+  constr constr_compare_fn
 
 val compare_head_gen_leq_with :
-  (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) ->
-  (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) ->
-  instance_compare_fn ->
-  (Sorts.t -> Sorts.t -> bool) ->
-  constr_compare_fn ->
-  constr_compare_fn ->
-  constr_compare_fn
+  ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) ->
+  ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) ->
+  'univs instance_compare_fn ->
+  ('sort -> 'sort -> bool) ->
+  'v constr_compare_fn ->
+  'v constr_compare_fn ->
+  'v constr_compare_fn
 
 (** [compare_head_gen_with k1 k2 u s f c1 c2] compares [c1] and [c2]
     like [compare_head_gen u s f c1 c2], except that [k1] (resp. [k2])
     is used,rather than {!kind}, to expose the immediate subterms of
     [c1] (resp. [c2]). *)
 val compare_head_gen_with :
-  (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) ->
-  (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) ->
-  instance_compare_fn ->
-  (Sorts.t -> Sorts.t -> bool) ->
-  constr_compare_fn ->
-  constr_compare_fn
+  ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) ->
+  ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) ->
+  'univs instance_compare_fn ->
+  ('sort -> 'sort -> bool) ->
+  'v constr_compare_fn ->
+  'v constr_compare_fn
 
 (** [compare_head_gen_leq u s f fle c1 c2] compare [c1] and [c2] using
     [f] to compare the immediate subterms of [c1] of [c2] for
@@ -570,11 +575,11 @@ val compare_head_gen_with :
     [s] to compare sorts for for subtyping; Cast's, binders name and
     Cases annotations are not taken into account *)
 
-val compare_head_gen_leq : instance_compare_fn ->
+val compare_head_gen_leq : Univ.Instance.t instance_compare_fn ->
   (Sorts.t -> Sorts.t -> bool) ->
-  constr_compare_fn ->
-  constr_compare_fn ->
-  constr_compare_fn
+  constr constr_compare_fn ->
+  constr constr_compare_fn ->
+  constr constr_compare_fn
 
 (** {6 Hashconsing} *)