aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/constr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/constr.ml')
-rw-r--r--kernel/constr.ml113
1 files changed, 60 insertions, 53 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 2cbcdd76e..ba7fecadf 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -654,6 +654,11 @@ 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'))
+type instance_compare_fn = global_reference -> int ->
+ Univ.Instance.t -> Univ.Instance.t -> bool
+
+type 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
the structure [c2]) using [eq] to compare the immediate subterms of
@@ -665,38 +670,42 @@ let map_with_binders g f l c0 = match kind c0 with
optimisation that physically equal arrays are equals (hence the
calls to {!Array.equal_norefl}). *)
-let compare_head_gen_leq_with kind1 kind2 eq_universes leq_sorts eq leq t1 t2 =
+let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs 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
| Sort s1, Sort s2 -> leq_sorts s1 s2
- | Cast (c1,_,_), _ -> leq c1 t2
- | _, Cast (c2,_,_) -> leq t1 c2
- | Prod (_,t1,c1), Prod (_,t2,c2) -> eq t1 t2 && leq c1 c2
- | Lambda (_,t1,c1), Lambda (_,t2,c2) -> eq t1 t2 && eq c1 c2
- | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> eq b1 b2 && eq t1 t2 && leq c1 c2
+ | 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 (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_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) -> Constant.equal c1 c2 && eq_universes true u1 u2
- | Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && eq_universes false u1 u2
- | Construct (c1,u1), Construct (c2,u2) -> eq_constructor c1 c2 && eq_universes false u1 u2
+ | 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) &&
+ eq (nargs+len) c1 c2 && Array.equal_norefl (eq 0) l1 l2
+ | Proj (p1,c1), Proj (p2,c2) -> Projection.equal p1 p2 && eq 0 c1 c2
+ | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && Array.equal (eq 0) l1 l2
+ | Const (c1,u1), Const (c2,u2) ->
+ (* The args length currently isn't used but may as well pass it. *)
+ Constant.equal c1 c2 && leq_universes (ConstRef c1) nargs u1 u2
+ | Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && leq_universes (IndRef c1) nargs u1 u2
+ | Construct (c1,u1), Construct (c2,u2) ->
+ eq_constructor c1 c2 && leq_universes (ConstructRef c1) nargs u1 u2
| Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
- eq p1 p2 && eq c1 c2 && Array.equal eq bl1 bl2
+ eq 0 p1 p2 && eq 0 c1 c2 && Array.equal (eq 0) bl1 bl2
| Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) ->
- Int.equal i1 i2 && Array.equal Int.equal ln1 ln2
- && Array.equal_norefl eq tl1 tl2 && Array.equal_norefl eq bl1 bl2
+ Int.equal i1 i2 && Array.equal Int.equal ln1 ln2
+ && Array.equal_norefl (eq 0) tl1 tl2 && Array.equal_norefl (eq 0) bl1 bl2
| CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
- Int.equal ln1 ln2 && Array.equal_norefl eq tl1 tl2 && Array.equal_norefl eq bl1 bl2
+ Int.equal ln1 ln2 && Array.equal_norefl (eq 0) tl1 tl2 && Array.equal_norefl (eq 0) bl1 bl2
| (Rel _ | Meta _ | Var _ | Sort _ | Prod _ | Lambda _ | LetIn _ | App _
- | Proj _ | Evar _ | Const _ | Ind _ | Construct _ | Case _ | Fix _
- | CoFix _), _ -> false
+ | Proj _ | Evar _ | Const _ | Ind _ | Construct _ | Case _ | Fix _
+ | CoFix _), _ -> 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,
@@ -704,8 +713,8 @@ let compare_head_gen_leq_with kind1 kind2 eq_universes leq_sorts eq leq t1 t2 =
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_leq_with kind kind eq_universes leq_sorts eq leq t1 t2
+let compare_head_gen_leq leq_universes leq_sorts eq leq t1 t2 =
+ compare_head_gen_leq_with kind kind leq_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
@@ -722,7 +731,7 @@ let compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq t1 t2 =
let compare_head_gen eq_universes eq_sorts eq t1 t2 =
compare_head_gen_leq eq_universes eq_sorts eq eq t1 t2
-let compare_head = compare_head_gen (fun _ -> Univ.Instance.equal) Sorts.equal
+let compare_head = compare_head_gen (fun _ _ -> Univ.Instance.equal) Sorts.equal
(*******************************)
(* alpha conversion functions *)
@@ -730,41 +739,41 @@ let compare_head = compare_head_gen (fun _ -> Univ.Instance.equal) Sorts.equal
(* alpha conversion : ignore print names and casts *)
-let rec eq_constr m n =
- (m == n) || compare_head_gen (fun _ -> Instance.equal) Sorts.equal eq_constr m n
+let rec eq_constr nargs m n =
+ (m == n) || compare_head_gen (fun _ _ -> Instance.equal) Sorts.equal eq_constr nargs m n
-let equal m n = eq_constr m n (* to avoid tracing a recursive fun *)
+let equal n m = eq_constr 0 m n (* to avoid tracing a recursive fun *)
let eq_constr_univs univs m n =
if m == n then true
else
- let eq_universes _ = UGraph.check_eq_instances univs in
+ let eq_universes _ _ = UGraph.check_eq_instances univs in
let eq_sorts s1 s2 = s1 == s2 || UGraph.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in
- let rec eq_constr' m n =
- m == n || compare_head_gen eq_universes eq_sorts eq_constr' m n
- in compare_head_gen eq_universes eq_sorts eq_constr' m n
+ let rec eq_constr' nargs m n =
+ m == n || compare_head_gen eq_universes eq_sorts eq_constr' nargs m n
+ in compare_head_gen eq_universes eq_sorts eq_constr' 0 m n
let leq_constr_univs univs m n =
if m == n then true
else
- let eq_universes _ = UGraph.check_eq_instances univs in
+ let eq_universes _ _ = UGraph.check_eq_instances univs in
let eq_sorts s1 s2 = s1 == s2 ||
UGraph.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in
let leq_sorts s1 s2 = s1 == s2 ||
UGraph.check_leq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in
- let rec eq_constr' m n =
- m == n || compare_head_gen eq_universes eq_sorts eq_constr' m n
+ let rec eq_constr' nargs m n =
+ m == n || compare_head_gen eq_universes eq_sorts eq_constr' nargs m n
in
- let rec compare_leq m n =
- compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' m n
- and leq_constr' m n = m == n || compare_leq m n in
- compare_leq m n
+ let rec compare_leq nargs m n =
+ compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' nargs m n
+ and leq_constr' nargs m n = m == n || compare_leq nargs m n in
+ compare_leq 0 m n
let eq_constr_univs_infer univs m n =
if m == n then true, Constraint.empty
else
let cstrs = ref Constraint.empty in
- let eq_universes strict = UGraph.check_eq_instances univs in
+ let eq_universes _ _ = UGraph.check_eq_instances univs in
let eq_sorts s1 s2 =
if Sorts.equal s1 s2 then true
else
@@ -774,17 +783,17 @@ let eq_constr_univs_infer univs m n =
(cstrs := Univ.enforce_eq u1 u2 !cstrs;
true)
in
- let rec eq_constr' m n =
- m == n || compare_head_gen eq_universes eq_sorts eq_constr' m n
+ let rec eq_constr' nargs m n =
+ m == n || compare_head_gen eq_universes eq_sorts eq_constr' nargs m n
in
- let res = compare_head_gen eq_universes eq_sorts eq_constr' m n in
+ let res = compare_head_gen eq_universes eq_sorts eq_constr' 0 m n in
res, !cstrs
let leq_constr_univs_infer univs m n =
if m == n then true, Constraint.empty
else
let cstrs = ref Constraint.empty in
- let eq_universes strict l l' = UGraph.check_eq_instances univs l l' in
+ let eq_universes _ _ l l' = UGraph.check_eq_instances univs l l' in
let eq_sorts s1 s2 =
if Sorts.equal s1 s2 then true
else
@@ -802,19 +811,17 @@ let leq_constr_univs_infer univs m n =
(cstrs := Univ.enforce_leq u1 u2 !cstrs;
true)
in
- let rec eq_constr' m n =
- m == n || compare_head_gen eq_universes eq_sorts eq_constr' m n
+ let rec eq_constr' nargs m n =
+ m == n || compare_head_gen eq_universes eq_sorts eq_constr' nargs m n
in
- let rec compare_leq m n =
- compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' m n
- and leq_constr' m n = m == n || compare_leq m n in
- let res = compare_leq m n in
+ let rec compare_leq nargs m n =
+ compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' nargs m n
+ and leq_constr' nargs m n = m == n || compare_leq nargs m n in
+ let res = compare_leq 0 m n in
res, !cstrs
-let always_true _ _ = true
-
let rec eq_constr_nounivs m n =
- (m == n) || compare_head_gen (fun _ -> always_true) always_true eq_constr_nounivs m n
+ (m == n) || compare_head_gen (fun _ _ _ _ -> true) (fun _ _ -> true) (fun _ -> eq_constr_nounivs) 0 m n
let constr_ord_int f t1 t2 =
let (=?) f g i1 i2 j1 j2=