max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/type_context): fixes #1801

Browse source 
This commit also fixes the decay in error message quality reported at
c6a10b127f
This commit is contained in:
Leonardo de Moura 2017-08-22 14:03:58 -07:00
parent 971ae34521
commit e99ce26b16
6 changed files with 45 additions and 26 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

43
src/library/type_context.cpp
View file

@ -2543,6 +2543,11 @@ expr type_context::elim_delayed_abstraction(expr const & e) {
return r;
}
static bool mvar_has_user_facing_name(expr const & m) {
lean_assert(is_metavar(m));
return mlocal_name(m) != mlocal_pp_name(m);
}
lbool type_context::quick_is_def_eq(expr const & e1, expr const & e2) {
if (e1 == e2)
return l_true;
@ -2572,24 +2577,38 @@ lbool type_context::quick_is_def_eq(expr const & e1, expr const & e2) {
optional<metavar_decl> m2_decl = m_mctx.find_metavar_decl(f2);
if (m1_decl && m2_decl) {
if (m2_decl->get_context().is_subset_of(m1_decl->get_context())) {
if (!is_app(e1) || is_app(e2)) {
/* Remark:
It is easier to solve the assignment
?m2 := ?m1 a_1 ... a_n
than
?m1 a_1 ... a_n := ?m2
Reason: the first one is precise. For example,
consider the following constraint:
?m1 ?m =?= ?m2
*/
if (!is_app(e1) && is_app(e2)) {
/* ?m1 := ?m2 a_1 ... a_n */
return to_lbool(process_assignment(e1, e2));
} else if (m1_decl->get_context().is_subset_of(m2_decl->get_context())) {
lean_assert(is_app(e1) && !is_app(e2));
/* It is easier to solve the assignment
?m2 := ?m1 a_1 ... a_n
than
?m1 a_1 ... a_n := ?m2
Reason: the first one is precise. For example,
consider the following constraint:
?m1 ?m =?= ?m2
*/
return to_lbool(process_assignment(e2, e1));
lean_assert(is_app(e1) || !is_app(e2));
if ((is_app(e1) && !is_app(e2)) || /* ?m2 := ?m1 a_1 ... a_n */
(!mvar_has_user_facing_name(f2) && mvar_has_user_facing_name(f1)) /* ?m2 does not have a user facing name, but ?m1 has */
) {
/* Remark: the second case (?m2 has user facing name but ?m1 doesn't) is particularly for
the equation preprocessor. See issue #1801. */
return to_lbool(process_assignment(e2, e1));
} else {
return to_lbool(process_assignment(e1, e2));
}
} else {
lean_assert(m2_decl->get_context().is_subset_of(m1_decl->get_context()));
lean_assert(!m1_decl->get_context().is_subset_of(m2_decl->get_context()));
return to_lbool(process_assignment(e1, e2));
}
} else {
lean_assert(!m2_decl->get_context().is_subset_of(m1_decl->get_context()));
return to_lbool(process_assignment(e2, e1));
}
} else {

4
tests/lean/def_inaccessible_issue.lean.expected.out
View file

@ -1,3 +1,3 @@
map2.equations._eqn_2 :
∀ (f : bool → bool → bool) (x : ℕ) (b1 : bool) (v1 : bv x) (b2 : bool) (v2 : bv x),
map2 f (cons x b1 v1) (cons x b2 v2) = cons x (f b1 b2) (map2 f v1 v2)
∀ (f : bool → bool → bool) (n : ℕ) (b1 : bool) (v1 : bv n) (b2 : bool) (v2 : bv n),
map2 f (cons n b1 v1) (cons n b2 v2) = cons n (f b1 b2) (map2 f v1 v2)

2
tests/lean/eqn_compiler_error_msg.lean.expected.out
View file

@ -1,3 +1,3 @@
eqn_compiler_error_msg.lean:5:28: error: invalid function application in pattern, it cannot be reduced to a constructor (possible solution, mark term as inaccessible using '.( )')
.?m_1 + .?m_2
.p + .n
eqn_compiler_error_msg.lean:4:6: error: equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' for additional details)

2
tests/lean/inaccessible2.lean.expected.out
View file

@ -7,7 +7,7 @@ inaccessible2.lean:11:46: error: invalid expression
inaccessible2.lean:11:4: error: invalid application, function expected
inaccessible2.lean:11:46: error: ill-formed match/equation expression
inaccessible2.lean:11:46: error: command expected
inaccessible2.lean:14:27: error: don't know how to synthesize placeholder
inaccessible2.lean:14:21: error: don't know how to synthesize placeholder
context:
A : Sort ?,
symm : ∀ (a b : A), a = b → b = a

18
tests/lean/inject.lean.expected.out
View file

@ -3,12 +3,12 @@ lift.equations._eqn_2 : ∀ {m k : ℕ} (f : fi m → fi k) (n : ℕ), @lift m k
lift.equations._eqn_3 :
∀ {m k : ℕ} (f : fi m → fi k) (n : ℕ) (i : fi (m + n)),
@lift m k f (succ n) (@fs (m + n) i) = @fs (k + n) (@lift m k f n i)
to_nat.equations._eqn_1 : ∀ (x : ℕ), @to_nat (succ x) (@f0 x) = 0
to_nat.equations._eqn_2 : ∀ (x : ℕ) (i : fi x), @to_nat (succ x) (@fs x i) = succ (@to_nat x i)
inject.equations._eqn_1 : ∀ (x : ℕ) (i : fi x), @inject (succ x) (@fs x i) (@f0 (@to_nat x i)) = @f0 x
to_nat.equations._eqn_1 : ∀ (n : ℕ), @to_nat (succ n) (@f0 n) = 0
to_nat.equations._eqn_2 : ∀ (n : ℕ) (i : fi n), @to_nat (succ n) (@fs n i) = succ (@to_nat n i)
inject.equations._eqn_1 : ∀ (n : ℕ) (i : fi n), @inject (succ n) (@fs n i) (@f0 (@to_nat n i)) = @f0 n
inject.equations._eqn_2 :
∀ (x : ℕ) (i : fi x) (j : fi (@to_nat x i)),
@inject (succ x) (@fs x i) (@fs (@to_nat x i) j) = @fs x (@inject x i j)
∀ (n : ℕ) (i : fi n) (j : fi (@to_nat n i)),
@inject (succ n) (@fs n i) (@fs (@to_nat n i) j) = @fs n (@inject n i j)
inject'.equations._eqn_1 : ∀ (n : ℕ) (i : fi n), @inject' (succ n) (@fs n i) (@f0 (@to_nat n i)) = @f0 n
inject'.equations._eqn_2 :
∀ (n : ℕ) (i : fi n) (j : fi (@to_nat n i)),
@ -16,10 +16,10 @@ inject'.equations._eqn_2 :
raise.equations._eqn_1 : ∀ {m : ℕ} (i : fi m), @raise m 0 i = i
raise.equations._eqn_2 : ∀ {m : ℕ} (n : ℕ) (i : fi m), @raise m (succ n) i = @fs (m + n) (@raise m n i)
deg.equations._eqn_1 : ∀ (n : ℕ) (j : fi (succ n)), @deg (succ n) (@f0 (succ n)) j = @fs (succ n) j
deg.equations._eqn_2 : ∀ (x : ℕ) (i : fi (succ x)), @deg (succ x) (@fs (succ x) i) (@f0 x) = @f0 (succ x)
deg.equations._eqn_2 : ∀ (n : ℕ) (i : fi (succ n)), @deg (succ n) (@fs (succ n) i) (@f0 n) = @f0 (succ n)
deg.equations._eqn_3 :
∀ (x : ℕ) (i : fi (succ x)) (j : fi x), @deg (succ x) (@fs (succ x) i) (@fs x j) = @fs (succ x) (@deg x i j)
∀ (n : ℕ) (i : fi (succ n)) (j : fi n), @deg (succ n) (@fs (succ n) i) (@fs n j) = @fs (succ n) (@deg n i j)
deg'.equations._eqn_1 : ∀ (n : ℕ) (j : fi (succ n)), @deg' (succ n) (@f0 (succ n)) j = @fs (succ n) j
deg'.equations._eqn_2 : ∀ (x : ℕ) (i : fi (succ x)), @deg' (succ x) (@fs (succ x) i) (@f0 x) = @f0 (succ x)
deg'.equations._eqn_2 : ∀ (n : ℕ) (i : fi (succ n)), @deg' (succ n) (@fs (succ n) i) (@f0 n) = @f0 (succ n)
deg'.equations._eqn_3 :
∀ (x : ℕ) (i : fi (succ x)) (j : fi x), @deg' (succ x) (@fs (succ x) i) (@fs x j) = @fs (succ x) (@deg' x i j)
∀ (n : ℕ) (i : fi (succ n)) (j : fi n), @deg' (succ n) (@fs (succ n) i) (@fs n j) = @fs (succ n) (@deg' n i j)

2
tests/lean/offset_is_def_eq_trick.lean.expected.out
View file

@ -1 +1 @@
head.equations._eqn_1 : ∀ {α : Type u_1} (x : ℕ) (h : α) (t : Vec α x), head (Vec.cons h t) = h
head.equations._eqn_1 : ∀ {α : Type u_1} (n : ℕ) (h : α) (t : Vec α n), head (Vec.cons h t) = h