Merge PR #8577: Generalize type of compare_head_with functions, and use for econstr

3 files changed, 89 insertions, 68 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 678f7c6ce6..8ab3ce821e 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -14,7 +14,23 @@ open Names
 open Constr
 open Context
 
-include Evd.MiniEConstr
+module ESorts = struct
+  include Evd.MiniEConstr.ESorts
+
+  let equal sigma s1 s2 =
+    Sorts.equal (kind sigma s1) (kind sigma s2)
+end
+
+module EInstance = struct
+  include Evd.MiniEConstr.EInstance
+
+  let equal sigma i1 i2 =
+    Univ.Instance.equal (kind sigma i1) (kind sigma i2)
+end
+
+include (Evd.MiniEConstr : module type of Evd.MiniEConstr
+         with module ESorts := ESorts
+          and module EInstance := EInstance)
 
 type types = t
 type constr = t
@@ -445,38 +461,28 @@ let fold sigma f acc c = match kind sigma c with
 let compare_gen k eq_inst eq_sort eq_constr nargs c1 c2 =
   (c1 == c2) || Constr.compare_head_gen_with k k eq_inst eq_sort eq_constr nargs c1 c2
 
-let eq_einstance sigma i1 i2 =
-  let i1 = EInstance.kind sigma (EInstance.make i1) in
-  let i2 = EInstance.kind sigma (EInstance.make i2) in
-  Univ.Instance.equal i1 i2
-
-let eq_esorts sigma s1 s2 =
-  let s1 = ESorts.kind sigma (ESorts.make s1) in
-  let s2 = ESorts.kind sigma (ESorts.make s2) in
-  Sorts.equal s1 s2
-
 let eq_constr sigma c1 c2 =
-  let kind c = kind_upto sigma c in
-  let eq_inst _ _ i1 i2 = eq_einstance sigma i1 i2 in
-  let eq_sorts s1 s2 = eq_esorts sigma s1 s2 in
+  let kind c = kind sigma c in
+  let eq_inst _ _ i1 i2 = EInstance.equal sigma i1 i2 in
+  let eq_sorts s1 s2 = ESorts.equal sigma s1 s2 in
   let rec eq_constr nargs c1 c2 =
     compare_gen kind eq_inst eq_sorts eq_constr nargs c1 c2
   in
-  eq_constr 0 (unsafe_to_constr c1) (unsafe_to_constr c2)
+  eq_constr 0 c1 c2
 
 let eq_constr_nounivs sigma c1 c2 =
-  let kind c = kind_upto sigma c in
+  let kind c = kind sigma c in
   let rec eq_constr nargs c1 c2 =
     compare_gen kind (fun _ _ _ _ -> true) (fun _ _ -> true) eq_constr nargs c1 c2
   in
-  eq_constr 0 (unsafe_to_constr c1) (unsafe_to_constr c2)
+  eq_constr 0 c1 c2
 
 let compare_constr sigma cmp c1 c2 =
-  let kind c = kind_upto sigma c in
-  let eq_inst _ _ i1 i2 = eq_einstance sigma i1 i2 in
-  let eq_sorts s1 s2 = eq_esorts sigma s1 s2 in
-  let cmp nargs c1 c2 = cmp (of_constr c1) (of_constr c2) in
-  compare_gen kind eq_inst eq_sorts cmp 0 (unsafe_to_constr c1) (unsafe_to_constr c2)
+  let kind c = kind sigma c in
+  let eq_inst _ _ i1 i2 = EInstance.equal sigma i1 i2 in
+  let eq_sorts s1 s2 = ESorts.equal sigma s1 s2 in
+  let cmp nargs c1 c2 = cmp c1 c2 in
+  compare_gen kind eq_inst eq_sorts cmp 0 c1 c2
 
 let compare_cumulative_instances cv_pb nargs_ok variances u u' cstrs =
   let open UnivProblem in
@@ -528,10 +534,10 @@ let cmp_constructors (mind, ind, cns as spec) nargs u1 u2 cstrs =
         cstrs (Univ.Instance.to_array u1) (Univ.Instance.to_array u2)
 
 let eq_universes env sigma cstrs cv_pb ref nargs l l' =
-  if Univ.Instance.is_empty l then (assert (Univ.Instance.is_empty l'); true)
+  if EInstance.is_empty l then (assert (EInstance.is_empty l'); true)
   else
-    let l = Evd.normalize_universe_instance sigma l
-    and l' = Evd.normalize_universe_instance sigma l' in
+    let l = EInstance.kind sigma l
+    and l' = EInstance.kind sigma l' in
     let open GlobRef in
     let open UnivProblem in
     match ref with
@@ -549,7 +555,7 @@ let eq_universes env sigma cstrs cv_pb ref nargs l l' =
 
 let test_constr_universes env sigma leq m n =
   let open UnivProblem in
-  let kind c = kind_upto sigma c in
+  let kind c = kind sigma c in
   if m == n then Some Set.empty
   else
     let cstrs = ref Set.empty in
@@ -557,16 +563,16 @@ let test_constr_universes env sigma leq m n =
     let eq_universes ref nargs l l' = eq_universes env sigma cstrs Reduction.CONV ref nargs l l'
     and leq_universes ref nargs l l' = eq_universes env sigma cstrs cv_pb ref nargs l l' in
     let eq_sorts s1 s2 =
-      let s1 = ESorts.kind sigma (ESorts.make s1) in
-      let s2 = ESorts.kind sigma (ESorts.make s2) in
+      let s1 = ESorts.kind sigma s1 in
+      let s2 = ESorts.kind sigma s2 in
       if Sorts.equal s1 s2 then true
       else (cstrs := Set.add
               (UEq (Sorts.univ_of_sort s1,Sorts.univ_of_sort s2)) !cstrs;
 	    true)
     in
     let leq_sorts s1 s2 = 
-      let s1 = ESorts.kind sigma (ESorts.make s1) in
-      let s2 = ESorts.kind sigma (ESorts.make s2) in
+      let s1 = ESorts.kind sigma s1 in
+      let s2 = ESorts.kind sigma s2 in
       if Sorts.equal s1 s2 then true
       else 
         (cstrs := Set.add
@@ -587,16 +593,16 @@ let test_constr_universes env sigma leq m n =
     if res then Some !cstrs else None
 
 let eq_constr_universes env sigma m n =
-  test_constr_universes env sigma false (unsafe_to_constr m) (unsafe_to_constr n)
+  test_constr_universes env sigma false m n
 let leq_constr_universes env sigma m n =
-  test_constr_universes env sigma true (unsafe_to_constr m) (unsafe_to_constr n)
+  test_constr_universes env sigma true m n
 
 let compare_head_gen_proj env sigma equ eqs eqc' nargs m n =
-  let kind c = kind_upto sigma c in
-  match kind_upto sigma m, kind_upto sigma n with
+  let kind c = kind sigma c in
+  match kind m, kind n with
   | Proj (p, c), App (f, args)
   | App (f, args), Proj (p, c) -> 
-      (match kind_upto sigma f with
+      (match kind f with
       | Const (p', u) when Constant.equal (Projection.constant p) p' -> 
           let npars = Projection.npars p in
           if Array.length args == npars + 1 then
@@ -612,6 +618,8 @@ let eq_constr_universes_proj env sigma m n =
     let cstrs = ref Set.empty in
     let eq_universes ref l l' = eq_universes env sigma cstrs Reduction.CONV ref l l' in
     let eq_sorts s1 s2 =
+      let s1 = ESorts.kind sigma s1 in
+      let s2 = ESorts.kind sigma s2 in
       if Sorts.equal s1 s2 then true
       else
         (cstrs := Set.add
@@ -621,7 +629,7 @@ let eq_constr_universes_proj env sigma m n =
     let rec eq_constr' nargs m n =
       m == n || compare_head_gen_proj env sigma eq_universes eq_sorts eq_constr' nargs m n
     in
-    let res = eq_constr' 0 (unsafe_to_constr m) (unsafe_to_constr n) in
+    let res = eq_constr' 0 m n in
     if res then Some !cstrs else None
 
 let universes_of_constr sigma c =
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} *)