michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

test(tests/lean): add test for '[congr]' attribute validation

Browse source
This commit is contained in:
Leonardo de Moura 2015-07-23 16:40:00 -07:00
parent 844caf32e4
commit 5f4576a7f7
3 changed files with 48 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/library/simplifier/simp_rule_set.cpp
View file

@ -309,7 +309,7 @@ void add_congr_core(environment const & env, simp_rule_sets & s, name const & n)
if (!is_constant(rhs_fn) || const_name(lhs_fn) != const_name(rhs_fn) || lhs_args.size() != rhs_args.size()) {
throw exception(sstream() << "invalid congruence rule, '" << n
<< "' resulting type is not of the form (" << const_name(lhs_fn) << " ...) "
<< " ~ (" << const_name(lhs_fn) << " ...), where ~ is '" << const_name(rel) << "'");
<< "~ (" << const_name(lhs_fn) << " ...), where ~ is '" << const_name(rel) << "'");
}
for (expr const & lhs_arg : lhs_args) {
if (is_sort(lhs_arg))
@ -357,18 +357,18 @@ void add_congr_core(environment const & env, simp_rule_sets & s, name const & n)
j++;
if (!only_found_mvars(mlocal_type(local), found_mvars)) {
throw exception(sstream() << "invalid congruence rule, '" << n
<< "' argument #" << j << " is a congruence hypothesis, but it contains "
<< "' argument #" << j << " of parameter #" << (i+1) << " contains "
<< "unresolved parameters");
}
}
if (!only_found_mvars(h_lhs, found_mvars)) {
throw exception(sstream() << "invalid congruence rule, '" << n
<< "' argument #" << j << " is not a valid hypothesis, the left-hand-side contains "
<< "' argument #" << (i+1) << " is not a valid hypothesis, the left-hand-side contains "
<< "unresolved parameters");
}
if (!is_valid_congr_hyp_rhs(h_rhs, found_mvars)) {
throw exception(sstream() << "invalid congruence rule, '" << n
<< "' argument #" << j << " is not a valid hypothesis, the right-hand-side must be "
<< "' argument #" << (i+1) << " is not a valid hypothesis, the right-hand-side must be "
<< "of the form (m l_1 ... l_n) where m is parameter that was not "
<< "'assigned/resolved' yet and l_i's are locals");
}

34
tests/lean/congr_error_msg.lean Normal file
View file

@ -0,0 +1,34 @@
open nat
definition g : nat → nat → nat :=
sorry
definition R : nat → nat → Prop :=
sorry
lemma C₁ [congr] : g 0 1 = g 1 0 := -- ERROR
sorry
lemma C₂ [congr] (a b : nat) : g a b = 0 := -- ERROR
sorry
lemma C₃ [congr] (a b : nat) : R (g a b) (g 0 0) := -- ERROR
sorry
lemma C₄ [congr] (A B : Type) : (A → B) = (λ a : nat, B → A) 0 := -- ERROR
sorry
lemma C₅ [congr] (A B : Type₁) : (A → nat) = (B → nat) := -- ERROR
sorry
lemma C₆ [congr] (A B : Type₁) : A = B := -- ERROR
sorry
lemma C₇ [congr] (a b c d : nat) : (∀ (x : nat), x > c → a = c) → g a b = g c d := -- ERROR
sorry
lemma C₈ [congr] (a b c d : nat) : (c = a) → g a b = g c d := -- ERROR
sorry
lemma C₉ [congr] (a b c d : nat) : (a = c) → (b = c) → g a b = g c d := -- ERROR
sorry

10
tests/lean/congr_error_msg.lean.expected.out Normal file
View file

@ -0,0 +1,10 @@
congr_error_msg.lean:9:0: error: invalid congruence rule, 'C₁' the left-hand-side of the congruence resulting type must be of the form (g x_1 ... x_n), where each x_i is a distinct variable or a sort
congr_error_msg.lean:12:0: error: invalid congruence rule, 'C₂' resulting type is not of the form (g ...) ~ (g ...), where ~ is 'eq'
congr_error_msg.lean:15:0: error: invalid congruence rule, 'C₃' resulting type is not of the form t ~ s, where '~' is a transitive and reflexive relation
congr_error_msg.lean:18:0: error: invalid congruence rule, 'C₄' kinds of the left-hand-side and right-hand-side of the congruence resulting type do not match
congr_error_msg.lean:21:0: error: invalid congruence rule, 'C₅' left-hand-side of the congruence resulting type must be of the form (fun/Pi (x : A), B x)
congr_error_msg.lean:24:0: error: invalid congruence rule, 'C₆' left-hand-side is not an application nor a binding
congr_error_msg.lean:27:0: error: invalid congruence rule, 'C₇' argument #2 of parameter #5 contains unresolved parameters
congr_error_msg.lean:30:0: error: invalid congruence rule, 'C₈' argument #5 is not a valid hypothesis, the left-hand-side contains unresolved parameters
congr_error_msg.lean:33:0: error: invalid congruence rule, 'C₉' argument #6 is not a valid hypothesis, the right-hand-side must be of the form (m l_1 ... l_n) where m is parameter that was not 'assigned/resolved' yet and l_i's are locals
congr_error_msg.lean: error: unknown declaration 'C₁'