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

fix(tests/lean): adjust error messages in the expected output

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-10-24 19:08:35 -07:00
parent 65a514ad8a
commit 46b9b2114a
6 changed files with 311 additions and 72 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

155
tests/lean/elab1.lean.expected.out
View file

@ -1,39 +1,138 @@
Set: pp::colors
Set: pp::unicode
Assumed: f
Error (line: 4, pos: 6) type mismatch at application
f 10 ⊤
Function type:
Π (A : Type), A → A → A
Arguments types:
ℕ : Type
10 : ℕ
⊤ : Bool
Failed to solve
⊢ (?M3::1 ≈ λ x : ℕ, x) ⊕ (?M3::1 ≈ nat_to_int) ⊕ (?M3::1 ≈ nat_to_real)
(line: 4: pos: 8) Coercion for
10
Failed to solve
⊢ Bool ≺ ℕ
Substitution
⊢ Bool ≺ ?M3::0
(line: 4: pos: 6) Type of argument 3 must be convertible to the expected type in the application of
f::explicit
with arguments:
?M3::0
?M3::1 10
⊤
Assignment
⊢ ℕ ≺ ?M3::0
Substitution
⊢ (?M3::5[inst:0 (10)]) 10 ≺ ?M3::0
(line: 4: pos: 6) Type of argument 2 must be convertible to the expected type in the application of
f::explicit
with arguments:
?M3::0
?M3::1 10
⊤
Assignment
x : ℕ ⊢ λ x : ℕ, ℕ ≈ ?M3::5
Destruct/Decompose
x : ℕ ⊢ ℕ ≈ ?M3::5 x
Destruct/Decompose
⊢ ℕ → ℕ ≈ Π x : ?M3::4, ?M3::5 x
Substitution
⊢ ?M3::3 ≈ Π x : ?M3::4, ?M3::5 x
Function expected at
?M3::1 10
Assignment
⊢ ℕ → ℕ ≺ ?M3::3
Propagate type, ?M3::1 : ?M3::3
Assignment
⊢ ?M3::1 ≈ λ x : ℕ, x
assumption 0
Failed to solve
⊢ Bool ≺ ℤ
Substitution
⊢ Bool ≺ ?M3::0
(line: 4: pos: 6) Type of argument 3 must be convertible to the expected type in the application of
f::explicit
with arguments:
?M3::0
?M3::1 10
⊤
Assignment
⊢ ℤ ≺ ?M3::0
Substitution
⊢ (?M3::5[inst:0 (10)]) 10 ≺ ?M3::0
(line: 4: pos: 6) Type of argument 2 must be convertible to the expected type in the application of
f::explicit
with arguments:
?M3::0
?M3::1 10
⊤
Assignment
_ : ℕ ⊢ λ x : ℕ, ℤ ≈ ?M3::5
Destruct/Decompose
_ : ℕ ⊢ ℤ ≈ ?M3::5 _
Destruct/Decompose
⊢ ℕ → ℤ ≈ Π x : ?M3::4, ?M3::5 x
Substitution
⊢ ?M3::3 ≈ Π x : ?M3::4, ?M3::5 x
Function expected at
?M3::1 10
Assignment
⊢ ℕ → ℤ ≺ ?M3::3
Propagate type, ?M3::1 : ?M3::3
Assignment
⊢ ?M3::1 ≈ nat_to_int
assumption 1
Failed to solve
⊢ Bool ≺ ℝ
Substitution
⊢ Bool ≺ ?M3::0
(line: 4: pos: 6) Type of argument 3 must be convertible to the expected type in the application of
f::explicit
with arguments:
?M3::0
?M3::1 10
⊤
Assignment
⊢ ℝ ≺ ?M3::0
Substitution
⊢ (?M3::5[inst:0 (10)]) 10 ≺ ?M3::0
(line: 4: pos: 6) Type of argument 2 must be convertible to the expected type in the application of
f::explicit
with arguments:
?M3::0
?M3::1 10
⊤
Assignment
_ : ℕ ⊢ λ x : ℕ, ℝ ≈ ?M3::5
Destruct/Decompose
_ : ℕ ⊢ ℝ ≈ ?M3::5 _
Destruct/Decompose
⊢ ℕ → ℝ ≈ Π x : ?M3::4, ?M3::5 x
Substitution
⊢ ?M3::3 ≈ Π x : ?M3::4, ?M3::5 x
Function expected at
?M3::1 10
Assignment
⊢ ℕ → ℝ ≺ ?M3::3
Propagate type, ?M3::1 : ?M3::3
Assignment
⊢ ?M3::1 ≈ nat_to_real
assumption 2
Assumed: g
Error (line: 7, pos: 6) unsolved placeholder at term
g 10
Assumed: h
Error (line: 11, pos: 27) application type mismatch during term elaboration
h A x
Function type:
Π (A : Type), A → A
Arguments types:
A : Type
x : ?M0[lift:0:2]
Elaborator state
#0 ≈ ?M0[lift:0:2]
Failed to solve
x : ?M3::0, A : Type ⊢ ?M3::0[lift:0:2] ≺ A
(line: 11: pos: 27) Type of argument 2 must be convertible to the expected type in the application of
h
with arguments:
A
x
Assumed: eq
Error (line: 15, pos: 51) application type mismatch during term elaboration
eq C a b
Function type:
Π (A : Type), A → A → Bool
Arguments types:
C : Type
a : ?M0[lift:0:3]
b : ?M2[lift:0:2]
Elaborator state
#0 ≈ ?M2[lift:0:2]
#0 ≈ ?M0[lift:0:3]
Failed to solve
A : Type, B : Type, a : ?M3::0, b : ?M3::1, C : Type ⊢ ?M3::0[lift:0:3] ≺ C
(line: 15: pos: 51) Type of argument 2 must be convertible to the expected type in the application of
eq
with arguments:
C
a
b
Assumed: a
Assumed: b
Assumed: H

52
tests/lean/ex3.lean.expected.out
View file

@ -4,21 +4,41 @@
myeq Bool ⊤ ⊥
Assumed: T
Assumed: a
Error (line: 5, pos: 6) type mismatch at application
myeq Bool ⊤ a
Function type:
Π (A : Type), A → A → Bool
Arguments types:
Bool : Type
⊤ : Bool
a : T
Failed to solve
⊢ Bool ≺ T
Substitution
⊢ Bool ≺ ?M3::0
(line: 5: pos: 6) Type of argument 2 must be convertible to the expected type in the application of
myeq
with arguments:
?M3::0
⊤
a
Assignment
⊢ T ≺ ?M3::0
(line: 5: pos: 6) Type of argument 3 must be convertible to the expected type in the application of
myeq
with arguments:
?M3::0
⊤
a
Assumed: myeq2
Set: lean::pp::implicit
Error (line: 9, pos: 15) type mismatch at application
myeq2::explicit Bool ⊤ a
Function type:
Π (A : Type), A → A → Bool
Arguments types:
Bool : Type
⊤ : Bool
a : T
Failed to solve
⊢ Bool ≺ T
Substitution
⊢ Bool ≺ ?M3::0
(line: 9: pos: 15) Type of argument 2 must be convertible to the expected type in the application of
myeq2::explicit
with arguments:
?M3::0
⊤
a
Assignment
⊢ T ≺ ?M3::0
(line: 9: pos: 15) Type of argument 3 must be convertible to the expected type in the application of
myeq2::explicit
with arguments:
?M3::0
⊤
a

47
tests/lean/let4.lean.expected.out
View file

@ -1,20 +1,47 @@
Set: pp::colors
Set: pp::unicode
Error (line: 4, pos: 15) type mismatch at definition 'a', expected type
ℤ
Given type:
Bool
let b := ⊤, a : ℤ := b in a
Assumed: vector
Assumed: const
let a := 10, v1 := const a ⊤, v2 := v1 in v2 : vector Bool 10
let a := 10, v1 : vector Bool a := const a ⊤, v2 : vector Bool a := v1 in v2
let a := 10, v1 : vector Bool a := const a ⊤, v2 : vector Bool a := v1 in v2 : vector Bool 10
Error (line: 31, pos: 26) type mismatch at definition 'v2', expected type
vector ℤ a
Given type:
vector Bool a
Failed to solve
a : ℕ := 10, v1 : vector ?M3::0 a := const a ⊤ ⊢ Bool ≈ ℤ
Substitution
a : ℕ := 10, v1 : vector ?M3::0 a := const a ⊤ ⊢ ?M3::0[lift:0:1] ≈ ℤ
Destruct/Decompose
a : ℕ := 10, v1 : vector ?M3::0 a := const a ⊤ ⊢ vector (?M3::0[lift:0:1]) a ≺ vector ℤ a
(line: 31: pos: 26) Type of definition 'v2' must be convertible to expected type.
Assignment
a : ℕ := 10 ⊢ ?M3::0 ≈ Bool
Destruct/Decompose
a : ℕ := 10 ⊢ vector ?M3::0 a ≺ vector Bool a
(line: 30: pos: 26) Type of definition 'v1' must be convertible to expected type.
Assumed: foo
Coercion foo
let a := 10, v1 : vector Bool a := const a ⊤, v2 : vector ℤ a := v1 in v2 : vector ℤ 10
Failed to solve
a : ℕ := 10, v1 : vector ?M3::0 a := const a ⊤ ⊢ Bool ≈ ℤ
Substitution
a : ℕ := 10, v1 : vector ?M3::0 a := const a ⊤ ⊢ ?M3::0[lift:0:1] ≈ ℤ
Destruct/Decompose
a : ℕ := 10, v1 : vector ?M3::0 a := const a ⊤ ⊢ vector (?M3::0[lift:0:1]) a ≺ vector ℤ a
(line: 40: pos: 26) Type of definition 'v2' must be convertible to expected type.
Assignment
a : ℕ := 10 ⊢ ?M3::0 ≈ Bool
Destruct/Decompose
a : ℕ := 10 ⊢ vector ?M3::0 a ≺ vector Bool a
(line: 39: pos: 26) Type of definition 'v1' must be convertible to expected type.
Set: lean::pp::coercion
let a := 10, v1 : vector Bool a := const a ⊤, v2 : vector ℤ a := foo v1 in v2
Failed to solve
a : ℕ := 10, v1 : vector ?M3::0 a := const a ⊤ ⊢ Bool ≈ ℤ
Substitution
a : ℕ := 10, v1 : vector ?M3::0 a := const a ⊤ ⊢ ?M3::0[lift:0:1] ≈ ℤ
Destruct/Decompose
a : ℕ := 10, v1 : vector ?M3::0 a := const a ⊤ ⊢ vector (?M3::0[lift:0:1]) a ≺ vector ℤ a
(line: 48: pos: 26) Type of definition 'v2' must be convertible to expected type.
Assignment
a : ℕ := 10 ⊢ ?M3::0 ≈ Bool
Destruct/Decompose
a : ℕ := 10 ⊢ vector ?M3::0 a ≺ vector Bool a
(line: 47: pos: 26) Type of definition 'v1' must be convertible to expected type.

111
tests/lean/overload2.lean.expected.out
View file

@ -1,13 +1,108 @@
Set: pp::colors
Set: pp::unicode
Error (line: 1, pos: 10) application type mismatch, none of the overloads can be used
Candidates:
Real::add : ℝ → ℝ → ℝ
Int::add : ℤ → ℤ → ℤ
Nat::add : ℕ → ℕ → ℕ
Arguments:
1 : ℕ
⊤ : Bool
Failed to solve
⊢ (?M3::0 ≈ Nat::add) ⊕ (?M3::0 ≈ Int::add) ⊕ (?M3::0 ≈ Real::add)
(line: 1: pos: 10) Overloading at
(Real::add | Int::add | Nat::add) 1 ⊤
Failed to solve
⊢ Bool ≺ ℕ
Substitution
⊢ Bool ≺ ?M3::8
(line: 1: pos: 10) Type of argument 2 must be convertible to the expected type in the application of
?M3::0
with arguments:
?M3::1 1
⊤
Assignment
⊢ ℕ ≈ ?M3::8
Destruct/Decompose
⊢ ℕ → ℕ ≈ Π x : ?M3::8, ?M3::9 x
Substitution
⊢ (?M3::7[inst:0 (?M3::1 1)]) (?M3::1 1) ≈ Π x : ?M3::8, ?M3::9 x
(line: 1: pos: 10) Function expected at
?M3::0 (?M3::1 1) ⊤
Assignment
_ : ℕ ⊢ λ x : ℕ, ℕ → ℕ ≈ ?M3::7
Destruct/Decompose
_ : ℕ ⊢ ℕ → ℕ ≈ ?M3::7 _
Destruct/Decompose
⊢ ℕ → ℕ → ℕ ≈ Π x : ?M3::6, ?M3::7 x
Substitution
⊢ ?M3::2 ≈ Π x : ?M3::6, ?M3::7 x
(line: 1: pos: 10) Function expected at
?M3::0 (?M3::1 1) ⊤
Assignment
⊢ ℕ → ℕ → ℕ ≺ ?M3::2
Propagate type, ?M3::0 : ?M3::2
Assignment
⊢ ?M3::0 ≈ Nat::add
assumption 0
Failed to solve
⊢ Bool ≺ ℤ
Substitution
⊢ Bool ≺ ?M3::8
(line: 1: pos: 10) Type of argument 2 must be convertible to the expected type in the application of
?M3::0
with arguments:
?M3::1 1
⊤
Assignment
⊢ ℤ ≈ ?M3::8
Destruct/Decompose
⊢ ℤ → ℤ ≈ Π x : ?M3::8, ?M3::9 x
Substitution
⊢ (?M3::7[inst:0 (?M3::1 1)]) (?M3::1 1) ≈ Π x : ?M3::8, ?M3::9 x
(line: 1: pos: 10) Function expected at
?M3::0 (?M3::1 1) ⊤
Assignment
_ : ℤ ⊢ λ x : ℤ, ℤ → ℤ ≈ ?M3::7
Destruct/Decompose
_ : ℤ ⊢ ℤ → ℤ ≈ ?M3::7 _
Destruct/Decompose
⊢ ℤ → ℤ → ℤ ≈ Π x : ?M3::6, ?M3::7 x
Substitution
⊢ ?M3::2 ≈ Π x : ?M3::6, ?M3::7 x
(line: 1: pos: 10) Function expected at
?M3::0 (?M3::1 1) ⊤
Assignment
⊢ ℤ → ℤ → ℤ ≺ ?M3::2
Propagate type, ?M3::0 : ?M3::2
Assignment
⊢ ?M3::0 ≈ Int::add
assumption 2
Failed to solve
⊢ Bool ≺ ℝ
Substitution
⊢ Bool ≺ ?M3::8
(line: 1: pos: 10) Type of argument 2 must be convertible to the expected type in the application of
?M3::0
with arguments:
?M3::1 1
⊤
Assignment
⊢ ℝ ≈ ?M3::8
Destruct/Decompose
⊢ ℝ → ℝ ≈ Π x : ?M3::8, ?M3::9 x
Substitution
⊢ (?M3::7[inst:0 (?M3::1 1)]) (?M3::1 1) ≈ Π x : ?M3::8, ?M3::9 x
(line: 1: pos: 10) Function expected at
?M3::0 (?M3::1 1) ⊤
Assignment
_ : ℝ ⊢ λ x : ℝ, ℝ → ℝ ≈ ?M3::7
Destruct/Decompose
_ : ℝ ⊢ ℝ → ℝ ≈ ?M3::7 _
Destruct/Decompose
⊢ ℝ → ℝ → ℝ ≈ Π x : ?M3::6, ?M3::7 x
Substitution
⊢ ?M3::2 ≈ Π x : ?M3::6, ?M3::7 x
(line: 1: pos: 10) Function expected at
?M3::0 (?M3::1 1) ⊤
Assignment
⊢ ℝ → ℝ → ℝ ≺ ?M3::2
Propagate type, ?M3::0 : ?M3::2
Assignment
⊢ ?M3::0 ≈ Real::add
assumption 5
Assumed: R
Assumed: T
Assumed: r2t

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

@ -26,7 +26,7 @@ Definition map {A B C : Type} {n : N} (f : A → B → C) (v1 : vector A n) (v2
Definition map::explicit (A B C : Type) (n : N) (f : A → B → C) (v1 : vector A n) (v2 : vector B n) : vector C n :=
map f v1 v2
select (update (const three ⊥) two ⊤) two two_lt_three : Bool
⊤
if Bool (two = two) ⊤ ⊥
update (const three ⊥) two ⊤ : vector Bool three
--------

16
tests/lean/tst7.lean.expected.out
View file

@ -2,15 +2,13 @@
Set: pp::unicode
Assumed: f
λ (A B : Type) (a : B), f B a
Error (line: 4, pos: 40) application type mismatch during term elaboration
f B a
Function type:
Π (A : Type), A → Bool
Arguments types:
B : Type
a : ?M0[lift:0:2]
Elaborator state
#0 ≈ ?M0[lift:0:2]
Failed to solve
A : Type, a : ?M3::0, B : Type ⊢ ?M3::0[lift:0:2] ≺ B
(line: 4: pos: 40) Type of argument 2 must be convertible to the expected type in the application of
f
with arguments:
B
a
Assumed: myeq
myeq (Π (A : Type), A → A) (λ (A : Type) (a : A), a) (λ (B : Type) (b : B), b)
myeq (Π (A : Type), A → A) (λ (A : Type) (a : A), a) (λ (B : Type) (b : B), b) : Bool