diff options
| author | krasimir <krasimir@chalmers.se> | 2010-02-20 18:48:06 +0000 |
|---|---|---|
| committer | krasimir <krasimir@chalmers.se> | 2010-02-20 18:48:06 +0000 |
| commit | 59d640088e65002354beaa2b149f6b884731192f (patch) | |
| tree | 9074f7dc713c4860501f7f94be81735be57c7fae /testsuite | |
| parent | 45d209baf8bf1091b14393ad985278b324bcb547 (diff) | |
bugfix in PGF.TypeCheck
Diffstat (limited to 'testsuite')
| -rw-r--r-- | testsuite/runtime/typecheck/Test.gf | 2 | ||||
| -rw-r--r-- | testsuite/runtime/typecheck/typecheck.gfs | 3 | ||||
| -rw-r--r-- | testsuite/runtime/typecheck/typecheck.gfs.gold | 3 |
3 files changed, 7 insertions, 1 deletions
diff --git a/testsuite/runtime/typecheck/Test.gf b/testsuite/runtime/typecheck/Test.gf index 8ef0e03cf..9df65365e 100644 --- a/testsuite/runtime/typecheck/Test.gf +++ b/testsuite/runtime/typecheck/Test.gf @@ -34,4 +34,6 @@ fun h : (n : Nat) -> U n n -> Int ; -- fun u2 : (n : Nat) -> U (plus n zero) zero ;
-- fun h2 : (f : Nat -> Nat) -> ((n : Nat) -> U (f n) (f zero)) -> Int ;
+fun forall2 : (n : Nat) -> (Vector n -> Vector n -> Int) -> Int ;
+
}
\ No newline at end of file diff --git a/testsuite/runtime/typecheck/typecheck.gfs b/testsuite/runtime/typecheck/typecheck.gfs index 5a663aef3..60114b035 100644 --- a/testsuite/runtime/typecheck/typecheck.gfs +++ b/testsuite/runtime/typecheck/typecheck.gfs @@ -27,4 +27,5 @@ ai h ? (u1 ?) ai cmpVector (succ (succ zero)) (vector (succ (succ zero))) (append ? (succ zero) (vector ?) (vector (succ zero)))
ai diff ? (succ (succ zero)) (vector (succ (succ (succ (succ (succ zero)))))) (vector (succ (succ (succ zero))))
ai diff ? (succ (succ zero)) (vector (succ (succ (succ (succ zero))))) (vector (succ (succ (succ zero))))
-ai idMorph (mkMorph2 (\x -> ?) (vector zero))
\ No newline at end of file +ai idMorph (mkMorph2 (\x -> ?) (vector zero))
+ai <(\n -> forall2 n (\x,y -> cmpVector zero x y)) : Nat -> Int>
\ No newline at end of file diff --git a/testsuite/runtime/typecheck/typecheck.gfs.gold b/testsuite/runtime/typecheck/typecheck.gfs.gold index a43a0c216..9630aa3bf 100644 --- a/testsuite/runtime/typecheck/typecheck.gfs.gold +++ b/testsuite/runtime/typecheck/typecheck.gfs.gold @@ -69,3 +69,6 @@ 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
|