aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/constr.ml54
-rw-r--r--kernel/constr.mli20
-rw-r--r--library/universes.ml66
-rw-r--r--library/universes.mli8
-rw-r--r--pretyping/evarutil.ml21
-rw-r--r--pretyping/evarutil.mli7
-rw-r--r--pretyping/evd.ml3
-rw-r--r--pretyping/evd.mli4
-rw-r--r--proofs/proofview.ml14
-rw-r--r--tactics/extratactics.ml42
-rw-r--r--test-suite/bugs/closed/3593.v (renamed from test-suite/bugs/opened/3593.v)2
11 files changed, 122 insertions, 79 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml
index e823c01b1..e2b1d3fd9 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -475,7 +475,7 @@ 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_with kind1 kind2 eq_universes leq_sorts eq leq t1 t2 =
+let compare_head_gen_leq_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
@@ -512,13 +512,19 @@ let compare_head_gen_with kind1 kind2 eq_universes leq_sorts eq leq t1 t2 =
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_leq_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,
+(* [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,
application associativity, binders name and Cases annotations are
- not taken into account *)
+ not taken into account.
+
+ [compare_head_gen_with] is a variant taking kind-of-term functions,
+ to expose subterms of [c1] and [c2], as arguments. *)
+
+let compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq t1 t2 =
+ compare_head_gen_leq_with kind1 kind2 eq_universes eq_sorts eq 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
@@ -536,14 +542,6 @@ 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
@@ -567,7 +565,7 @@ let leq_constr_univs univs m n =
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
+ compare_leq m n
let eq_constr_univs_infer univs m n =
if m == n then true, Constraint.empty
@@ -578,16 +576,16 @@ let eq_constr_univs_infer univs m n =
if Sorts.equal s1 s2 then true
else
let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
- if Univ.check_eq univs u1 u2 then true
- else
- (cstrs := Univ.enforce_eq u1 u2 !cstrs;
- true)
+ if Univ.check_eq univs u1 u2 then true
+ else
+ (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
in
let res = compare_head_gen eq_universes eq_sorts eq_constr' m n in
- res, !cstrs
+ res, !cstrs
let leq_constr_univs_infer univs m n =
if m == n then true, Constraint.empty
@@ -598,18 +596,18 @@ let leq_constr_univs_infer univs m n =
if Sorts.equal s1 s2 then true
else
let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
- if Univ.check_eq univs u1 u2 then true
- else (cstrs := Univ.enforce_eq u1 u2 !cstrs;
- true)
+ if Univ.check_eq univs u1 u2 then true
+ else (cstrs := Univ.enforce_eq u1 u2 !cstrs;
+ true)
in
let leq_sorts s1 s2 =
if Sorts.equal s1 s2 then true
else
let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
- if Univ.check_leq univs u1 u2 then true
- else
- (cstrs := Univ.enforce_leq u1 u2 !cstrs;
- true)
+ if Univ.check_leq univs u1 u2 then true
+ else
+ (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
@@ -618,7 +616,7 @@ let leq_constr_univs_infer univs 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
- res, !cstrs
+ res, !cstrs
let always_true _ _ = true
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 67d1adedf..e6a3e71f8 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -203,14 +203,6 @@ 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
@@ -293,6 +285,18 @@ val compare_head_gen : (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) ->
(constr -> constr -> bool) ->
constr -> constr -> bool
+(** [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) kind_of_term) ->
+ (constr -> (constr,types) kind_of_term) ->
+ (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) ->
+ (Sorts.t -> Sorts.t -> bool) ->
+ (constr -> constr -> bool) ->
+ constr -> constr -> bool
+
(** [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
conversion, [fle] for cumulativity, [u] to compare universe
diff --git a/library/universes.ml b/library/universes.ml
index 9fddc7067..3a8ee2625 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -139,6 +139,32 @@ let eq_constr_univs_infer univs m n =
let res = Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n in
res, !cstrs
+(** Variant of [eq_constr_univs_infer] taking kind-of-term functions,
+ to expose subterms of [m] and [n], arguments. *)
+let eq_constr_univs_infer_with kind1 kind2 univs m n =
+ (* spiwack: duplicates the code of [eq_constr_univs_infer] because I
+ haven't find a way to factor the code without destroying
+ pointer-equality optimisations in [eq_constr_univs_infer].
+ Pointer equality is not sufficient to ensure equality up to
+ [kind1,kind2], because [kind1] and [kind2] may be different,
+ typically evaluating [m] and [n] in different evar maps. *)
+ let cstrs = ref Constraints.empty in
+ let eq_universes strict = Univ.Instance.check_eq univs in
+ let eq_sorts s1 s2 =
+ if Sorts.equal s1 s2 then true
+ else
+ let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
+ if Univ.check_eq univs u1 u2 then true
+ else
+ (cstrs := Constraints.add (u1, UEq, u2) !cstrs;
+ true)
+ in
+ let rec eq_constr' m n =
+ Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' m n
+ in
+ let res = Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' m n in
+ res, !cstrs
+
let leq_constr_univs_infer univs m n =
if m == n then true, Constraints.empty
else
@@ -148,18 +174,18 @@ let leq_constr_univs_infer univs m n =
if Sorts.equal s1 s2 then true
else
let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
- if Univ.check_eq univs u1 u2 then true
- else (cstrs := Constraints.add (u1, UEq, u2) !cstrs;
- true)
+ if Univ.check_eq univs u1 u2 then true
+ else (cstrs := Constraints.add (u1, UEq, u2) !cstrs;
+ true)
in
let leq_sorts s1 s2 =
if Sorts.equal s1 s2 then true
else
let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
- if Univ.check_leq univs u1 u2 then true
- else
- (cstrs := Constraints.add (u1, ULe, u2) !cstrs;
- true)
+ if Univ.check_leq univs u1 u2 then true
+ else
+ (cstrs := Constraints.add (u1, ULe, u2) !cstrs;
+ true)
in
let rec eq_constr' m n =
m == n || Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n
@@ -169,7 +195,7 @@ let leq_constr_univs_infer univs m n =
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
- res, !cstrs
+ res, !cstrs
let eq_constr_universes m n =
if m == n then true, Constraints.empty
@@ -188,7 +214,7 @@ let eq_constr_universes m n =
m == n || Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n
in
let res = Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n in
- res, !cstrs
+ res, !cstrs
let leq_constr_universes m n =
if m == n then true, Constraints.empty
@@ -216,22 +242,22 @@ let leq_constr_universes m n =
Constr.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
- res, !cstrs
+ res, !cstrs
let compare_head_gen_proj env equ eqs eqc' m n =
match kind_of_term m, kind_of_term n with
| Proj (p, c), App (f, args)
| App (f, args), Proj (p, c) ->
- (match kind_of_term f with
- | Const (p', u) when eq_constant (Projection.constant p) p' ->
- let pb = Environ.lookup_projection p env in
- let npars = pb.Declarations.proj_npars in
- if Array.length args == npars + 1 then
- eqc' c args.(npars)
- else false
- | _ -> false)
+ (match kind_of_term f with
+ | Const (p', u) when eq_constant (Projection.constant p) p' ->
+ let pb = Environ.lookup_projection p env in
+ let npars = pb.Declarations.proj_npars in
+ if Array.length args == npars + 1 then
+ eqc' c args.(npars)
+ else false
+ | _ -> false)
| _ -> Constr.compare_head_gen equ eqs eqc' m n
-
+
let eq_constr_universes_proj env m n =
if m == n then true, Constraints.empty
else
@@ -249,7 +275,7 @@ let eq_constr_universes_proj env m n =
m == n || compare_head_gen_proj env eq_universes eq_sorts eq_constr' m n
in
let res = eq_constr' m n in
- res, !cstrs
+ res, !cstrs
(* Generator of levels *)
let new_univ_level, set_remote_new_univ_level =
diff --git a/library/universes.mli b/library/universes.mli
index 252648d7d..5527da090 100644
--- a/library/universes.mli
+++ b/library/universes.mli
@@ -66,6 +66,14 @@ val to_constraints : universes -> universe_constraints -> constraints
application grouping, the universe constraints in [u] and additional constraints [c]. *)
val eq_constr_univs_infer : Univ.universes -> constr -> constr -> bool universe_constrained
+(** [eq_constr_univs_infer_With kind1 kind2 univs m n] is a variant of
+ {!eq_constr_univs_infer} taking kind-of-term functions, to expose
+ subterms of [m] and [n], arguments. *)
+val eq_constr_univs_infer_with :
+ (constr -> (constr,types) kind_of_term) ->
+ (constr -> (constr,types) kind_of_term) ->
+ Univ.universes -> constr -> constr -> bool universe_constrained
+
(** [leq_constr_univs u a b] is [true, c] if [a] is convertible to [b]
modulo alpha, casts, application grouping, the universe constraints
in [u] and additional constraints [c]. *)
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 201a16ebe..2508f4ef3 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -844,6 +844,25 @@ let subterm_source evk (loc,k) =
(loc,Evar_kinds.SubEvar evk)
-(** Term exploration up to isntantiation. *)
+(** Term exploration up to instantiation. *)
let kind_of_term_upto sigma t =
Constr.kind (Reductionops.whd_evar sigma t)
+
+(** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and
+ [u] up to existential variable instantiation and equalisable
+ universes. The term [t] is interpreted in [sigma1] while [u] is
+ interpreted in [sigma2]. The universe constraints in [sigma2] are
+ assumed to be an extention of those in [sigma1]. *)
+let eq_constr_univs_test sigma1 sigma2 t u =
+ (* spiwack: mild code duplication with {!Evd.eq_constr_univs}. *)
+ let open Evd in
+ let b, c =
+ Universes.eq_constr_univs_infer_with
+ (fun t -> kind_of_term_upto sigma1 t)
+ (fun u -> kind_of_term_upto sigma2 u)
+ (universes sigma2) t u
+ in
+ if b then
+ try let _ = add_universe_constraints sigma2 c in true
+ with Univ.UniverseInconsistency _ | UniversesDiffer -> false
+ else false
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 49036798e..f1d94b0a4 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -206,6 +206,13 @@ val flush_and_check_evars : evar_map -> constr -> constr
value of [e] in [sigma] is (recursively) used. *)
val kind_of_term_upto : evar_map -> constr -> (constr,types) kind_of_term
+(** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and
+ [u] up to existential variable instantiation and equalisable
+ universes. The term [t] is interpreted in [sigma1] while [u] is
+ interpreted in [sigma2]. The universe constraints in [sigma2] are
+ assumed to be an extention of those in [sigma1]. *)
+val eq_constr_univs_test : evar_map -> evar_map -> constr -> constr -> bool
+
(** {6 debug pretty-printer:} *)
val pr_tycon : env -> type_constraint -> Pp.std_ppcmds
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index bf519fb7c..f414d71dc 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -1304,9 +1304,6 @@ let e_eq_constr_univs evdref t u =
let evd, b = eq_constr_univs !evdref t u in
evdref := evd; b
-let eq_constr_univs_test evd t u =
- snd (eq_constr_univs evd t u)
-
(**********************************************************)
(* Accessing metas *)
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index fe785a831..eca6d60ad 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -562,10 +562,6 @@ val eq_constr_univs : evar_map -> constr -> constr -> evar_map * bool
val e_eq_constr_univs : evar_map ref -> constr -> constr -> bool
(** Syntactic equality up to universes. *)
-val eq_constr_univs_test : evar_map -> constr -> constr -> bool
-(** Syntactic equality up to universes, throwing away the (consistent) constraints
- in case of success. *)
-
(********************************************************************)
(* constr with holes and pending resolution of classes, conversion *)
(* problems, candidates, etc. *)
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 6f6263413..6e653806b 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -722,19 +722,7 @@ let give_up =
module Progress = struct
- (** equality function up to evar instantiation in heterogeneous
- contexts. *)
- (* spiwack (2015-02-19): In the previous version of progress an
- equality which considers two universes equal when it is consistent
- tu unify them ([Evd.eq_constr_univs_test]) was used. Maybe this
- behaviour has to be restored as well. This has to be established by
- practice. *)
-
- let rec eq_constr sigma1 sigma2 t1 t2 =
- Constr.equal_with
- (fun t -> Evarutil.kind_of_term_upto sigma1 t)
- (fun t -> Evarutil.kind_of_term_upto sigma2 t)
- t1 t2
+ let eq_constr = Evarutil.eq_constr_univs_test
(** equality function on hypothesis contexts *)
let eq_named_context_val sigma1 sigma2 ctx1 ctx2 =
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 891e2dba5..7f0a4c660 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -772,7 +772,7 @@ END
let eq_constr x y =
Proofview.Goal.enter (fun gl ->
let evd = Proofview.Goal.sigma gl in
- if Evd.eq_constr_univs_test evd x y then Proofview.tclUNIT ()
+ if Evarutil.eq_constr_univs_test evd evd x y then Proofview.tclUNIT ()
else Tacticals.New.tclFAIL 0 (str "Not equal"))
TACTIC EXTEND constr_eq
diff --git a/test-suite/bugs/opened/3593.v b/test-suite/bugs/closed/3593.v
index d83b90060..378db6857 100644
--- a/test-suite/bugs/opened/3593.v
+++ b/test-suite/bugs/closed/3593.v
@@ -5,6 +5,6 @@ Record prod A B := pair { fst : A ; snd : B }.
Goal forall x : prod Set Set, let f := @fst _ in f _ x = @fst _ _ x.
simpl; intros.
constr_eq (@fst Set Set x) (fst (A := Set) (B := Set) x).
- Fail Fail progress change (@fst Set Set x) with (fst (A := Set) (B := Set) x).
+ Fail progress change (@fst Set Set x) with (fst (A := Set) (B := Set) x).
reflexivity.
Qed.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-05 03:27:44 +0000