New function [Constr.equal_with] to compare terms up to variants of [kind_of_term].

To be able to write equality up to evar instantiation instantiation.

Generalises the main function of [eq] constr over the variant of [kind_of_term] it uses. It prevents some optimisation of [Array.equal] where two physically equal arrays are considered (less or) equal. But it does not seem to have appreciable effects on efficiency.

4 files changed, 61 insertions, 23 deletions

diff --git a/kernel/constr.ml b/kernel/constr.ml
index 499f196b79..e823c01b17 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -464,15 +464,19 @@ let map_with_binders g f l c0 = match kind c0 with
     let bl' = CArray.Fun1.smartmap f l' bl in
     mkCoFix (ln,(lna,tl',bl'))
 
-
-(* [compare_head_gen_leq u s eq leq c1 c2] compare [c1] and [c2] using [eq] to compare
-   the immediate subterms of [c1] of [c2] for conversion if needed, [leq] for cumulativity,
-   [u] to compare universe instances and [s] to compare sorts; Cast's,
+(* [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
+   the structure [c2]) using [eq] to compare the immediate subterms of
+   [c1] of [c2] for conversion if needed, [leq] for cumulativity, [u]
+   to compare universe instances, and [s] to compare sorts; Cast's,
    application associativity, binders name and Cases annotations are
-   not taken into account *)
+   not taken into account. Note that as [kind1] and [kind2] are
+   potentially different, we cannot use, in recursive case, the
+   optimisation that physically equal arrays are equals (hence the
+   calls to {!Array.equal_norefl}). *)
 
-let compare_head_gen_leq eq_universes leq_sorts eq leq t1 t2 =
-  match kind t1, kind t2 with
+let compare_head_gen_with kind1 kind2 eq_universes leq_sorts eq leq t1 t2 =
+  match kind1 t1, kind2 t2 with
   | Rel n1, Rel n2 -> Int.equal n1 n2
   | Meta m1, Meta m2 -> Int.equal m1 m2
   | Var id1, Var id2 -> Id.equal id1 id2
@@ -485,8 +489,8 @@ let compare_head_gen_leq eq_universes leq_sorts eq leq t1 t2 =
   | App (Cast(c1, _, _),l1), _ -> leq (mkApp (c1,l1)) t2
   | _, App (Cast (c2, _, _),l2) -> leq t1 (mkApp (c2,l2))
   | App (c1,l1), App (c2,l2) ->
-    Int.equal (Array.length l1) (Array.length l2) &&
-      eq c1 c2 && Array.equal eq l1 l2
+      Int.equal (Array.length l1) (Array.length l2) &&
+        eq c1 c2 && Array.equal_norefl eq l1 l2
   | Proj (p1,c1), Proj (p2,c2) -> Projection.equal p1 p2 && eq c1 c2
   | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && Array.equal eq l1 l2
   | Const (c1,u1), Const (c2,u2) -> eq_constant c1 c2 && eq_universes true u1 u2
@@ -496,11 +500,20 @@ let compare_head_gen_leq eq_universes leq_sorts eq leq t1 t2 =
       eq p1 p2 && eq c1 c2 && Array.equal eq bl1 bl2
   | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) ->
       Int.equal i1 i2 && Array.equal Int.equal ln1 ln2
-      && Array.equal eq tl1 tl2 && Array.equal eq bl1 bl2
+      && Array.equal_norefl eq tl1 tl2 && Array.equal_norefl eq bl1 bl2
   | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
-      Int.equal ln1 ln2 && Array.equal eq tl1 tl2 && Array.equal eq bl1 bl2
+      Int.equal ln1 ln2 && Array.equal_norefl eq tl1 tl2 && Array.equal_norefl eq bl1 bl2
   | _ -> false
 
+(* [compare_head_gen_leq u s eq leq c1 c2] compare [c1] and [c2] using [eq] to compare
+   the immediate subterms of [c1] of [c2] for conversion if needed, [leq] for cumulativity,
+   [u] to compare universe instances and [s] to compare sorts; Cast's,
+   application associativity, binders name and Cases annotations are
+   not taken into account *)
+
+let compare_head_gen_leq eq_universes leq_sorts eq leq t1 t2 =
+  compare_head_gen_with kind kind  eq_universes leq_sorts eq leq t1 t2
+
 (* [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 and [s] to compare sorts; Cast's,
@@ -523,6 +536,14 @@ let rec eq_constr m n =
 
 let equal m n = eq_constr m n (* to avoid tracing a recursive fun *)
 
+let rec equal_with kind1 kind2 m n =
+  (* note that pointer equality is not sufficient to ensure equality
+     up to [eq_evars], because we may evaluates evars of [m] and [n]
+     in different evar contexts. *)
+  let req_constr m n = equal_with kind1 kind2 m n in
+  compare_head_gen_with kind1 kind2
+    (fun _ -> Instance.equal) Sorts.equal req_constr req_constr m n
+
 let eq_constr_univs univs m n =
   if m == n then true
   else 
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 622b33c71f..67d1adedf6 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -203,6 +203,14 @@ val kind : constr -> (constr, types) kind_of_term
    and application grouping *)
 val equal : constr -> constr -> bool
 
+(** [equal_with_evars k1 k2 a b] is true when [a] equals [b] modulo
+    alpha, casts, application grouping, and using [k1] to expose the
+    head of [a] and [k2] to expose the head of [b]. *)
+val equal_with :
+  (constr -> (constr,types) kind_of_term) ->
+  (constr -> (constr,types) kind_of_term) ->
+  constr -> constr -> bool
+
 (** [eq_constr_univs u a b] is [true] if [a] equals [b] modulo alpha, casts,
    application grouping and the universe equalities in [u]. *)
 val eq_constr_univs : constr Univ.check_function
diff --git a/lib/cArray.ml b/lib/cArray.ml
index 1603454304..bb1e335468 100644
--- a/lib/cArray.ml
+++ b/lib/cArray.ml
@@ -13,6 +13,7 @@ sig
   include S
   val compare : ('a -> 'a -> int) -> 'a array -> 'a array -> int
   val equal : ('a -> 'a -> bool) -> 'a array -> 'a array -> bool
+  val equal_norefl : ('a -> 'a -> bool) -> 'a array -> 'a array -> bool
   val is_empty : 'a array -> bool
   val exists : ('a -> bool) -> 'a array -> bool
   val exists2 : ('a -> 'b -> bool) -> 'a array -> 'b array -> bool
@@ -85,19 +86,22 @@ let compare cmp v1 v2 =
       in
       loop (len - 1)
 
+let equal_norefl cmp t1 t2 =
+  let len = Array.length t1 in
+  if not (Int.equal len (Array.length t2)) then false
+  else
+    let rec aux i =
+      if i < 0 then true
+      else
+        let x = uget t1 i in
+        let y = uget t2 i in
+        cmp x y && aux (pred i)
+    in
+    aux (len - 1)
+
 let equal cmp t1 t2 =
-  if t1 == t2 then true else
-    let len = Array.length t1 in
-    if not (Int.equal len (Array.length t2)) then false
-    else
-      let rec aux i =
-        if i < 0 then true
-        else
-          let x = uget t1 i in
-          let y = uget t2 i in
-          cmp x y && aux (pred i)
-      in
-      aux (len - 1)
+  if t1 == t2 then true else equal_norefl cmp t1 t2
+    
 
 let is_empty array = Int.equal (Array.length array) 0
 
diff --git a/lib/cArray.mli b/lib/cArray.mli
index 39c35e2d54..7e5c93b5da 100644
--- a/lib/cArray.mli
+++ b/lib/cArray.mli
@@ -17,6 +17,11 @@ sig
   val equal : ('a -> 'a -> bool) -> 'a array -> 'a array -> bool
   (** Lift equality to array type. *)
 
+  val equal_norefl : ('a -> 'a -> bool) -> 'a array -> 'a array -> bool
+  (** Like {!equal} but does not assume that equality is reflexive: no
+      optimisation is performed if both arrays are physically the
+      same. *)
+
   val is_empty : 'a array -> bool
   (** True whenever the array is empty. *)