From b97d6abb8190cdcb595b9bf48051cc4a98f01156 Mon Sep 17 00:00:00 2001 From: krasimir Date: Sun, 6 Sep 2009 20:31:52 +0000 Subject: hopefully complete and correct typechecker in PGF --- testsuite/runtime/eval/Test.gf | 2 +- testsuite/runtime/eval/eval.gfs | 32 ++++---- testsuite/runtime/eval/eval.gfs.gold | 36 ++++----- testsuite/runtime/paraphrase/lambda.gfs.gold | 6 +- testsuite/runtime/typecheck/Test.gf | 37 +++++++++ testsuite/runtime/typecheck/typecheck.gfs | 30 ++++++++ testsuite/runtime/typecheck/typecheck.gfs.gold | 102 +++++++++++++++++++++++++ 7 files changed, 203 insertions(+), 42 deletions(-) create mode 100644 testsuite/runtime/typecheck/Test.gf create mode 100644 testsuite/runtime/typecheck/typecheck.gfs create mode 100644 testsuite/runtime/typecheck/typecheck.gfs.gold (limited to 'testsuite/runtime') diff --git a/testsuite/runtime/eval/Test.gf b/testsuite/runtime/eval/Test.gf index 71a7dc2c2..a0131d767 100644 --- a/testsuite/runtime/eval/Test.gf +++ b/testsuite/runtime/eval/Test.gf @@ -14,7 +14,7 @@ def g0 = g2 ; fun g3 : Int -> (Int -> Int) ; def g3 3 = g ; -fun const : Int -> Int -> Int ; +fun const : Float -> String -> Float ; def const x _ = x ; cat Nat ; diff --git a/testsuite/runtime/eval/eval.gfs b/testsuite/runtime/eval/eval.gfs index dd1cede9c..557bb9f90 100644 --- a/testsuite/runtime/eval/eval.gfs +++ b/testsuite/runtime/eval/eval.gfs @@ -1,34 +1,30 @@ i testsuite/runtime/eval/Test.gf -pt -compute \x -> x 1 -pt -compute ? 1 -pt -compute (\x -> x 1) ? -pt -compute unknown_var -pt -compute unknown_var 1 -pt -compute 1 2 +pt -compute \x -> x 1 : (Int->Int)->Int +pt -compute (? : Int -> Int) 1 +pt -compute (\x -> x 1 : (Int->Int)->Int) ? pt -compute f 1 2 -pt -compute \x -> x -pt -compute ?666 +pt -compute \x -> x : Nat -> Nat +pt -compute ? : String pt -compute f -pt -compute (\x -> x 2) (f 1) -pt -compute (\x -> x 2) 1 +pt -compute (\x -> x 2 : (Int->Int)->Int) (f 1) pt -compute g 1 pt -compute g 0 -pt -compute \x -> g x +pt -compute \x -> g x : Int -> Int pt -compute g ? -pt -compute (\x -> x 5) (g2 1) -pt -compute (\x -> x 3) (\x -> x) +pt -compute (\x -> x 5 : (Int->Int)->Int) (g2 1) +pt -compute (\x -> x 3 : (Int->Int)->Int) (\x -> x) pt -compute g0 -pt -compute (\x -> x 3.2) (\x -> f x) -pt -compute g0 2.3 -pt -compute g0 ((\x -> f x) 0) 1 +pt -compute (\x -> x 32 : (Int -> Int -> Int) -> Int -> Int) (\x -> f x : Int -> Int -> Int) +pt -compute g0 23 pt -compute const 3.14 "pi" pt -compute dec (succ (succ zero)) pt -compute dec (succ ?) -pt -compute \x -> dec x +pt -compute \x -> dec x : Nat -> Nat pt -compute dec ? -pt -compute (\f -> f 0) (g3 ?) +pt -compute (\f -> f 0 : (Int -> Int) -> Int) (g3 ?) pt -compute g (g2 ? 0) pt -compute plus (succ zero) (succ zero) pt -compute dec2 0 (succ zero) +pt -compute dec2 0 err pt -compute plus err (succ zero) \ No newline at end of file diff --git a/testsuite/runtime/eval/eval.gfs.gold b/testsuite/runtime/eval/eval.gfs.gold index 861c8534c..1c6282f27 100644 --- a/testsuite/runtime/eval/eval.gfs.gold +++ b/testsuite/runtime/eval/eval.gfs.gold @@ -1,30 +1,26 @@ -\v0 -> v0 1 +\x -> x 1 -? 1 +?1 1 -? 1 +?3 1 -unknown variable unknown_var -unknown variable unknown_var -literal of function type f 1 2 -\v0 -> v0 +\x -> x -?666 +?1 f f 1 2 -literal of function type 2 g 0 -\v0 -> g v0 +\x -> g x -g ? +g ?1 5 @@ -32,29 +28,29 @@ g ? g2 -f 3.2 +f 32 -g2 2.3 - -g2 (f 0) 1 +g2 23 3.14 succ zero -? +?1 -\v0 -> dec v0 +\x -> dec x -dec ? +dec ?1 -g3 ? 0 +g3 ?3 0 -g (g2 ? 0) +g (g2 ?1 0) succ (succ zero) zero +dec2 0 err + succ err diff --git a/testsuite/runtime/paraphrase/lambda.gfs.gold b/testsuite/runtime/paraphrase/lambda.gfs.gold index 0d8f027d6..5735dc175 100644 --- a/testsuite/runtime/paraphrase/lambda.gfs.gold +++ b/testsuite/runtime/paraphrase/lambda.gfs.gold @@ -1,10 +1,10 @@ -\v0 -> v0 +\x -> x 1 -\v0 -> v0 +\x -> x -\v0 -> 2 +\x -> 2 1 diff --git a/testsuite/runtime/typecheck/Test.gf b/testsuite/runtime/typecheck/Test.gf new file mode 100644 index 000000000..8ef0e03cf --- /dev/null +++ b/testsuite/runtime/typecheck/Test.gf @@ -0,0 +1,37 @@ +abstract Test = { + +cat Nat ; +data zero : Nat ; + succ : Nat -> Nat ; + +fun plus : Nat -> Nat -> Nat ; +def plus zero n = n ; + plus (succ m) n = plus m (succ n) ; + +cat Vector Nat ; +fun vector : (n : Nat) -> Vector n ; + +fun append : (m,n : Nat) -> Vector m -> Vector n -> Vector (plus m n) ; +fun diff : (m,n : Nat) -> Vector (plus m n) -> Vector m -> Vector n ; + +cat Morph (Nat -> Nat) ; +fun mkMorph : (f : Nat -> Nat) -> Morph f ; +fun mkMorph2 : (f : Nat -> Nat) -> Vector (f zero) -> Morph f ; +fun idMorph : Morph (\x -> x) -> Nat ; + +fun f0 : (n : Nat) -> ((m : Nat) -> Vector n) -> Int ; +fun f1 : (n : Nat -> Nat) -> ((m : Nat) -> Vector (n m)) -> Int ; + +fun cmpVector : (n : Nat) -> Vector n -> Vector n -> Int ; + +fun g : ((n : Nat) -> Vector n) -> Int ; + +cat U (n,m : Nat) ; +fun u0 : (n : Nat) -> U n n ; +fun u1 : (n : Nat) -> U n (succ n) ; +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 ; + +} \ No newline at end of file diff --git a/testsuite/runtime/typecheck/typecheck.gfs b/testsuite/runtime/typecheck/typecheck.gfs new file mode 100644 index 000000000..b1231a75d --- /dev/null +++ b/testsuite/runtime/typecheck/typecheck.gfs @@ -0,0 +1,30 @@ +i testsuite/runtime/typecheck/Test.gf + +ai succ "0" +ai succ : Int 0 +ai 1 2 +ai (\x -> x 2 : (Int->Int)->Int) 1 +ai unknown_fun +ai 0 : unknown_cat +ai \x -> x +ai \x -> x : Int +ai append (succ (succ zero)) (succ zero) (vector (succ (succ zero))) (vector (succ zero)) +ai \m,n -> vector (plus m n) : (m,n : Nat) -> Vector (plus m n) +ai mkMorph (\x -> succ zero) +ai idMorph (mkMorph (\x -> x)) +ai idMorph (mkMorph (\x -> succ zero)) +ai append zero (succ zero) : Vector zero -> Vector (succ zero) -> Vector (succ zero) +ai \n,v1,n,v2 -> append ? ? v1 v2 : (n : Nat) -> Vector n -> (m : Nat) -> Vector m -> Vector (plus n m) +ai \n -> (\v1,v2 -> eqVector n v1 v2 : Vector ? -> Vector ? -> EQ) (vector ?) : (n : Nat) -> Vector n -> EQ +ai (\v1,v2 -> cmpVector ? v1 v2 : Vector ? -> Vector ? -> Int) (vector ?) +ai f0 ? vector +ai f1 ? vector +ai f1 ? (\x -> vector (succ x)) +ai mkMorph (\x -> cmpVector ? (vector x) (vector (succ x))) +ai g (\n -> vector (succ n)) +ai h ? (u0 ?) +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 diff --git a/testsuite/runtime/typecheck/typecheck.gfs.gold b/testsuite/runtime/typecheck/typecheck.gfs.gold new file mode 100644 index 000000000..ca0412fb8 --- /dev/null +++ b/testsuite/runtime/typecheck/typecheck.gfs.gold @@ -0,0 +1,102 @@ + +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 + + +Function unknown_fun is not in scope + + +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 (plus (succ (succ zero)) (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, n'1, v2 -> append n n'1 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 + -- cgit v1.2.3