forked from GitHub/gf-core
upgrade the testsuite to work with GHC 6.12
This commit is contained in:
@@ -1,4 +1,4 @@
|
||||
␍
|
||||
␍
|
||||
checking module Test1Abs␍
|
||||
circular definitions: A B␍
|
||||
|
||||
|
||||
checking module Test1Abs
|
||||
circular definitions: A B
|
||||
|
||||
@@ -1,4 +1,4 @@
|
||||
␍
|
||||
␍
|
||||
checking module Test2Abs␍
|
||||
circular definitions: f g␍
|
||||
|
||||
|
||||
checking module Test2Abs
|
||||
circular definitions: f g
|
||||
|
||||
@@ -1,8 +1,8 @@
|
||||
␍
|
||||
␍
|
||||
checking module TestOpers␍
|
||||
circular definitions: A B␍
|
||||
␍
|
||||
␍
|
||||
checking module TestOperTypes␍
|
||||
circular definitions: A T␍
|
||||
|
||||
|
||||
checking module TestOpers
|
||||
circular definitions: A B
|
||||
|
||||
|
||||
checking module TestOperTypes
|
||||
circular definitions: A T
|
||||
|
||||
@@ -1,4 +1,4 @@
|
||||
␍
|
||||
␍
|
||||
checking module TestParams␍
|
||||
circular definitions: A B␍
|
||||
|
||||
|
||||
checking module TestParams
|
||||
circular definitions: A B
|
||||
|
||||
@@ -1,7 +1,7 @@
|
||||
␍
|
||||
␍
|
||||
checking module TestCnc␍
|
||||
Happened in linearization type of S in TestCnc.gf, line 3:␍
|
||||
type of PTrue␍
|
||||
expected: Type␍
|
||||
inferred: PBool␍
|
||||
|
||||
|
||||
checking module TestCnc
|
||||
Happened in linearization type of S in TestCnc.gf, line 3:
|
||||
type of PTrue
|
||||
expected: Type
|
||||
inferred: PBool
|
||||
|
||||
@@ -1,37 +1,37 @@
|
||||
checking module linsCnc␍
|
||||
Warning: no linearization type for C, inserting default {s : Str}␍
|
||||
Warning: no linearization of test␍
|
||||
abstract lins {␍
|
||||
cat C Nat␍
|
||||
cat Float␍
|
||||
cat Int␍
|
||||
cat Nat␍
|
||||
cat String␍
|
||||
fun test : C zero␍
|
||||
fun zero : Nat␍
|
||||
}␍
|
||||
concrete linsCnc {␍
|
||||
productions␍
|
||||
C0 -> F0[CVar]␍
|
||||
C1 -> F1[CVar]␍
|
||||
C1 -> F2[]␍
|
||||
functions␍
|
||||
F0 := (S0) [__gfV]␍
|
||||
F1 := () [__gfV]␍
|
||||
F2 := () [zero]␍
|
||||
sequences␍
|
||||
S0 := <0,0>␍
|
||||
categories␍
|
||||
C := range [C0 .. C0]␍
|
||||
labels ["s"]␍
|
||||
Float := range [CFloat .. CFloat]␍
|
||||
labels ["s"]␍
|
||||
Int := range [CInt .. CInt]␍
|
||||
labels ["s"]␍
|
||||
Nat := range [C1 .. C1]␍
|
||||
labels []␍
|
||||
String := range [CString .. CString]␍
|
||||
labels ["s"]␍
|
||||
__gfVar := range [CVar .. CVar]␍
|
||||
labels ["s"]␍
|
||||
}␍
|
||||
checking module linsCnc
|
||||
Warning: no linearization type for C, inserting default {s : Str}
|
||||
Warning: no linearization of test
|
||||
abstract lins {
|
||||
cat C Nat
|
||||
cat Float
|
||||
cat Int
|
||||
cat Nat
|
||||
cat String
|
||||
fun test : C zero
|
||||
fun zero : Nat
|
||||
}
|
||||
concrete linsCnc {
|
||||
productions
|
||||
C0 -> F0[CVar]
|
||||
C1 -> F1[CVar]
|
||||
C1 -> F2[]
|
||||
functions
|
||||
F0 := (S0) [__gfV]
|
||||
F1 := () [__gfV]
|
||||
F2 := () [zero]
|
||||
sequences
|
||||
S0 := <0,0>
|
||||
categories
|
||||
C := range [C0 .. C0]
|
||||
labels ["s"]
|
||||
Float := range [CFloat .. CFloat]
|
||||
labels ["s"]
|
||||
Int := range [CInt .. CInt]
|
||||
labels ["s"]
|
||||
Nat := range [C1 .. C1]
|
||||
labels []
|
||||
String := range [CString .. CString]
|
||||
labels ["s"]
|
||||
__gfVar := range [CVar .. CVar]
|
||||
labels ["s"]
|
||||
}
|
||||
|
||||
@@ -1,5 +1,5 @@
|
||||
␍
|
||||
␍
|
||||
checking module Res␍
|
||||
Happened in operation my_oper in Res.gf, line 3:␍
|
||||
No definition given to the operation␍
|
||||
|
||||
|
||||
checking module Res
|
||||
Happened in operation my_oper in Res.gf, line 3:
|
||||
No definition given to the operation
|
||||
|
||||
@@ -1,5 +1,5 @@
|
||||
␍
|
||||
␍
|
||||
renaming module funpatt␍
|
||||
renaming definition of d in funpatt.gf, line 12␍
|
||||
data constructor expected but funpatt.D1 is found instead␍
|
||||
|
||||
|
||||
renaming module funpatt
|
||||
renaming of d in funpatt.gf, line 11
|
||||
data constructor expected but funpatt.D1 is found instead
|
||||
|
||||
@@ -1,4 +1,4 @@
|
||||
1␍
|
||||
␍
|
||||
1␍
|
||||
␍
|
||||
1
|
||||
|
||||
1
|
||||
|
||||
|
||||
@@ -1 +1 @@
|
||||
fun f : (Int -> Int) -> Int -> Int␍
|
||||
fun f : (Int -> Int) -> Int -> Int
|
||||
|
||||
@@ -1,5 +1,5 @@
|
||||
␍
|
||||
␍
|
||||
checking module A␍
|
||||
Prod expected for function A instead of Type␍
|
||||
in category B in A.gf, line 4␍
|
||||
|
||||
|
||||
checking module A
|
||||
Prod expected for function A instead of Type
|
||||
in category B in A.gf, line 4
|
||||
|
||||
@@ -1,5 +1,5 @@
|
||||
␍
|
||||
␍
|
||||
checking module B␍
|
||||
Prod expected for function S instead of Type␍
|
||||
in type of function f in B.gf, line 5␍
|
||||
|
||||
|
||||
checking module B
|
||||
Prod expected for function S instead of Type
|
||||
in type of function f in B.gf, line 5
|
||||
|
||||
@@ -1,5 +1,5 @@
|
||||
␍
|
||||
␍
|
||||
checking module C␍
|
||||
{Int <> S}␍
|
||||
in definition of function f in C.gf, line 6␍
|
||||
|
||||
|
||||
checking module C
|
||||
{Int <> S}
|
||||
in definition of function f in C.gf, line 6
|
||||
|
||||
@@ -1,5 +1,5 @@
|
||||
␍
|
||||
␍
|
||||
checking module A␍
|
||||
Happened in operation silly in A.gf, line 5:␍
|
||||
A function type is expected for a_Det instead of type Str␍
|
||||
|
||||
|
||||
checking module A
|
||||
Happened in operation silly in A.gf, line 5:
|
||||
A function type is expected for a_Det instead of type Str
|
||||
|
||||
@@ -1,8 +1,8 @@
|
||||
␍
|
||||
␍
|
||||
C:\gf_3\testsuite\compiler\update\ArrityCheck.gf:6:1: cannot unify the informations␍
|
||||
fun f : Int -> Int -> Int ;␍
|
||||
def f 0 = \x -> x ;␍
|
||||
and␍
|
||||
def f 1 1 = 0 ;␍
|
||||
in module ArrityCheck␍
|
||||
|
||||
|
||||
C:\gf\testsuite\compiler\update\ArrityCheck.gf:6:1: cannot unify the informations
|
||||
fun f : Int -> Int -> Int ;
|
||||
def f 0 = \x -> x ;
|
||||
and
|
||||
def f 1 1 = 0 ;
|
||||
in module ArrityCheck
|
||||
|
||||
@@ -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)
|
||||
|
||||
|
||||
@@ -1,2 +1,2 @@
|
||||
succ (succ (succ zero))␍
|
||||
␍
|
||||
succ (succ (succ zero))
|
||||
|
||||
|
||||
@@ -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
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
@@ -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
|
||||
|
||||
|
||||
@@ -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
|
||||
|
||||
Reference in New Issue
Block a user