upgrade the testsuite to work with GHC 6.12

This commit is contained in:
krasimir
2010-04-30 19:27:53 +00:00
parent 87cc4d7624
commit 61a1171811
21 changed files with 311 additions and 311 deletions
+64 -64
View File
@@ -1,64 +1,64 @@
\x -> x 1␍
␍
?1 1␍
␍
?3 1␍
␍
f 1 2␍
␍
\x -> x␍
␍
?1␍
␍
f␍
␍
f 1 2␍
␍
2␍
␍
g 0␍
␍
\x -> g x␍
␍
g ?1␍
␍
5␍
␍
3␍
␍
g2␍
␍
f 32␍
␍
g2 23␍
␍
3.14␍
␍
succ zero␍
␍
?1␍
␍
zeroF␍
␍
dec (succF zeroF)␍
␍
dec zeroF␍
␍
\x -> dec x␍
␍
dec ?1␍
␍
g3 ?3 0␍
␍
g (g2 ?1 0)␍
␍
succ (succ zero)␍
␍
zero␍
␍
dec2 0 err␍
␍
succ err␍
␍
\x -> dec (dec x)␍
␍
\x -> x 1
?1 1
?3 1
f 1 2
\x -> x
?1
f
f 1 2
2
g 0
\x -> g x
g ?1
5
3
g2
f 32
g2 23
3.14
succ zero
?1
zeroF
dec (succF zeroF)
dec zeroF
\x -> dec x
dec ?1
g3 ?3 0
g (g2 ?1 0)
succ (succ zero)
zero
dec2 0 err
succ err
\x -> dec (dec x)
+2 -2
View File
@@ -1,2 +1,2 @@
succ (succ (succ zero))␍
␍
succ (succ (succ zero))
+30 -30
View File
@@ -1,30 +1,30 @@
?1 is even␍
␍
␍
exists x such that x is even␍
␍
␍
a␍
␍
␍
aa a␍
␍
␍
a b␍
␍
␍
abcd is string␍
␍
␍
100 is integer␍
␍
␍
12.4 is float␍
␍
␍
xyz is string␍
␍
␍
␍
␍
␍
?1 is even
exists x such that x is even
a
aa a
a b
abcd is string
100 is integer
12.4 is float
xyz is string
+12 -12
View File
@@ -1,12 +1,12 @@
\x -> x␍
␍
1␍
␍
\x -> x␍
␍
\x -> 2␍
␍
1␍
␍
2␍
␍
\x -> x
1
\x -> x
\x -> 2
1
2
@@ -1,22 +1,22 @@
Expression: join {n1} {n2} {n3} l12 (link {n2} {n3} l23)␍
Type: Path n1 n3␍
␍
Expression: join {n1} {n2} {n3} l12 (link {n2} {n3} l23)␍
Type: Path n1 n3␍
␍
Expression: <?2 : Label {?1}>␍
Type: Label {?1}␍
␍
Expression: <?2 : Label {n1}>␍
Type: Label {n1}␍
␍
{n1} is implicit argument but not implicit argument is expected here␍
Expression: <\{_1}, x -> x : ({m} : Node) -> (n : Node) -> Node>␍
Type: ({m} : Node) -> (n : Node) -> Node␍
␍
Expression: <\{_1} -> n1 : ({m} : Node) -> Node>␍
Type: ({m} : Node) -> Node␍
␍
Expression: <\{_1} -> ?1 : ({m} : Node) -> Node>␍
Type: ({m} : Node) -> Node␍
␍
Expression: join {n1} {n2} {n3} l12 (link {n2} {n3} l23)
Type: Path n1 n3
Expression: join {n1} {n2} {n3} l12 (link {n2} {n3} l23)
Type: Path n1 n3
Expression: <?2 : Label {?1}>
Type: Label {?1}
Expression: <?2 : Label {n1}>
Type: Label {n1}
{n1} is implicit argument but not implicit argument is expected here
Expression: <\{_1}, x -> x : ({m} : Node) -> (n : Node) -> Node>
Type: ({m} : Node) -> (n : Node) -> Node
Expression: <\{_1} -> n1 : ({m} : Node) -> Node>
Type: ({m} : Node) -> Node
Expression: <\{_1} -> ?1 : ({m} : Node) -> Node>
Type: ({m} : Node) -> Node
+74 -74
View File
@@ -1,74 +1,74 @@
Couldn't match expected type Nat␍
against inferred type String␍
In the expression: "0"␍
Category Int should have 0 argument(s), but has been given 1␍
In the type: Int 0␍
A function type is expected for the expression 1 instead of type Int␍
Couldn't match expected type Int -> Int␍
against inferred type Int␍
In the expression: 1␍
unknown category of function identifier unknown_fun␍
␍
Category unknown_cat is not in scope␍
Cannot infer the type of expression \x -> x␍
A function type is expected for the expression \x -> x instead of type Int␍
Expression: append (succ (succ zero)) (succ zero) (vector (succ (succ zero))) (vector (succ zero))␍
Type: Vector (succ (succ (succ zero)))␍
␍
Expression: <\m, n -> vector (plus m n) : (m : Nat) -> (n : Nat) -> Vector (plus m n)>␍
Type: (m : Nat) -> (n : Nat) -> Vector (plus m n)␍
␍
Expression: mkMorph (\x -> succ zero)␍
Type: Morph (\x -> succ zero)␍
␍
Expression: idMorph (mkMorph (\x -> x))␍
Type: Nat␍
␍
Couldn't match expected type Morph (\x -> x)␍
against inferred type Morph (\x -> succ zero)␍
In the expression: mkMorph (\x -> succ zero)␍
Expression: <append zero (succ zero) : Vector zero -> Vector (succ zero) -> Vector (succ zero)>␍
Type: Vector zero -> Vector (succ zero) -> Vector (succ zero)␍
␍
Expression: <\n, v1, n1, v2 -> append n n1 v1 v2 : (n : Nat) -> Vector n -> (m : Nat) -> Vector m -> Vector (plus n m)>␍
Type: (n : Nat) -> Vector n -> (m : Nat) -> Vector m -> Vector (plus n m)␍
␍
Category EQ is not in scope␍
Expression: <\v1, v2 -> cmpVector ?7 v1 v2 : Vector ?7 -> Vector ?7 -> Int> (vector ?7)␍
Type: Vector ?7 -> Int␍
␍
Couldn't match expected type (m : Nat) -> Vector ?1␍
against inferred type (n : Nat) -> Vector n␍
In the expression: vector␍
Expression: f1 (\v -> v) vector␍
Type: Int␍
␍
Expression: f1 (\v -> succ v) (\x -> vector (succ x))␍
Type: Int␍
␍
Couldn't match expected type Vector x␍
against inferred type Vector (succ x)␍
In the expression: vector (succ x)␍
Couldn't match expected type Vector n␍
against inferred type Vector (succ n)␍
In the expression: vector (succ n)␍
Expression: h ?2 (u0 ?2)␍
Type: Int␍
␍
Couldn't match expected type U ?2 ?2␍
against inferred type U ?2 (succ ?2)␍
In the expression: u1 ?2␍
Meta variable(s) ?11 should be resolved␍
in the expression: cmpVector (succ (succ zero)) (vector (succ (succ zero))) (append ?11 (succ zero) (vector ?11) (vector (succ zero)))␍
Expression: diff (succ (succ (succ zero))) (succ (succ zero)) (vector (succ (succ (succ (succ (succ zero)))))) (vector (succ (succ (succ zero))))␍
Type: Vector (succ (succ zero))␍
␍
Couldn't match expected type Vector (plus (succ (succ (succ zero))) (succ (succ zero)))␍
against inferred type Vector (succ (succ (succ (succ zero))))␍
In the expression: vector (succ (succ (succ (succ zero))))␍
Couldn't match expected type Vector ?1␍
against inferred type Vector zero␍
In the expression: vector zero␍
Couldn't match expected type Vector zero␍
against inferred type Vector n␍
In the expression: x␍
Couldn't match expected type Nat
against inferred type String
In the expression: "0"
Category Int should have 0 argument(s), but has been given 1
In the type: Int 0
A function type is expected for the expression 1 instead of type Int
Couldn't match expected type Int -> Int
against inferred type Int
In the expression: 1
unknown category of function identifier unknown_fun
Category unknown_cat is not in scope
Cannot infer the type of expression \x -> x
A function type is expected for the expression \x -> x instead of type Int
Expression: append (succ (succ zero)) (succ zero) (vector (succ (succ zero))) (vector (succ zero))
Type: Vector (succ (succ (succ zero)))
Expression: <\m, n -> vector (plus m n) : (m : Nat) -> (n : Nat) -> Vector (plus m n)>
Type: (m : Nat) -> (n : Nat) -> Vector (plus m n)
Expression: mkMorph (\x -> succ zero)
Type: Morph (\x -> succ zero)
Expression: idMorph (mkMorph (\x -> x))
Type: Nat
Couldn't match expected type Morph (\x -> x)
against inferred type Morph (\x -> succ zero)
In the expression: mkMorph (\x -> succ zero)
Expression: <append zero (succ zero) : Vector zero -> Vector (succ zero) -> Vector (succ zero)>
Type: Vector zero -> Vector (succ zero) -> Vector (succ zero)
Expression: <\n, v1, n1, v2 -> append n n1 v1 v2 : (n : Nat) -> Vector n -> (m : Nat) -> Vector m -> Vector (plus n m)>
Type: (n : Nat) -> Vector n -> (m : Nat) -> Vector m -> Vector (plus n m)
Category EQ is not in scope
Expression: <\v1, v2 -> cmpVector ?7 v1 v2 : Vector ?7 -> Vector ?7 -> Int> (vector ?7)
Type: Vector ?7 -> Int
Couldn't match expected type (m : Nat) -> Vector ?1
against inferred type (n : Nat) -> Vector n
In the expression: vector
Expression: f1 (\v -> v) vector
Type: Int
Expression: f1 (\v -> succ v) (\x -> vector (succ x))
Type: Int
Couldn't match expected type Vector x
against inferred type Vector (succ x)
In the expression: vector (succ x)
Couldn't match expected type Vector n
against inferred type Vector (succ n)
In the expression: vector (succ n)
Expression: h ?2 (u0 ?2)
Type: Int
Couldn't match expected type U ?2 ?2
against inferred type U ?2 (succ ?2)
In the expression: u1 ?2
Meta variable(s) ?11 should be resolved
in the expression: cmpVector (succ (succ zero)) (vector (succ (succ zero))) (append ?11 (succ zero) (vector ?11) (vector (succ zero)))
Expression: diff (succ (succ (succ zero))) (succ (succ zero)) (vector (succ (succ (succ (succ (succ zero)))))) (vector (succ (succ (succ zero))))
Type: Vector (succ (succ zero))
Couldn't match expected type Vector (plus (succ (succ (succ zero))) (succ (succ zero)))
against inferred type Vector (succ (succ (succ (succ zero))))
In the expression: vector (succ (succ (succ (succ zero))))
Couldn't match expected type Vector ?1
against inferred type Vector zero
In the expression: vector zero
Couldn't match expected type Vector zero
against inferred type Vector n
In the expression: x