Rakarake/churf
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

tests are running now

Browse source
This commit is contained in:
sebastian 2023-03-27 20:33:11 +02:00
parent 506d8733d9
commit ad2bd645d9
2 changed files with 101 additions and 95 deletions
Download patch file Download diff file Expand all files Collapse all files

183
tests/TestTypeCheckerBidir.hs
View file

@ -1,86 +1,95 @@
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# HLINT ignore "Use camelCase" #-} {-# HLINT ignore "Use camelCase" #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} {-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PatternSynonyms #-}
module TestTypeCheckerBidir (testTypeCheckerBidir) where module TestTypeCheckerBidir (testTypeCheckerBidir) where
import Test.Hspec import Test.Hspec
import Control.Monad ((<=<))
import Grammar.ErrM (Err, pattern Bad, pattern Ok)
import Grammar.Par (myLexer, pProgram)
import Renamer.Renamer (rename)
import TypeChecker.RemoveTEVar (RemoveTEVar (rmTEVar))
import TypeChecker.TypeCheckerBidir (typecheck)
import qualified TypeChecker.TypeCheckerIr as T
import Control.Monad ((<=<))
import Grammar.ErrM (Err, pattern Bad, pattern Ok)
import Grammar.Par (myLexer, pProgram)
import Renamer.Renamer (rename)
import TypeChecker.RemoveTEVar (RemoveTEVar (rmTEVar))
import TypeChecker.TypeCheckerBidir (typecheck)
import TypeChecker.TypeCheckerIr qualified as T
testTypeCheckerBidir = describe "Bidirectional type checker test" $ do testTypeCheckerBidir = describe "Bidirectional type checker test" $ do
tc_id tc_id
tc_double tc_double
tc_add_lam tc_add_lam
tc_const tc_const
tc_simple_rank2 tc_simple_rank2
tc_rank2 tc_rank2
tc_identity tc_identity
tc_pair tc_pair
tc_tree tc_tree
tc_mono_case tc_mono_case
tc_pol_case tc_pol_case
tc_id = specify "Basic identity function polymorphism" $ run tc_id =
[ "id : forall a. a -> a;" specify "Basic identity function polymorphism" $
, "id x = x;" run
, "main = id 4;" [ "id : forall a. a -> a;"
] `shouldSatisfy` ok , "id x = x;"
, "main = id 4;"
]
`shouldSatisfy` ok
tc_double = specify "Addition inference" $ run tc_double =
["double x = x + x;"] `shouldSatisfy` ok specify "Addition inference" $
run
["double x = x + x;"]
`shouldSatisfy` ok
tc_add_lam =
specify "Addition lambda inference" $
run
["four = (\\x. x + x) 2;"]
`shouldSatisfy` ok
tc_add_lam = specify "Addition lambda inference" $ run tc_const =
["four = (\\x. x + x) 2;"] `shouldSatisfy` ok specify "Basic polymorphism with multiple type variables" $
run
[ "const : forall a. forall b. a -> b -> a;"
, "const x y = x;"
, "main = const 'a' 65;"
]
`shouldSatisfy` ok
tc_simple_rank2 =
specify "Simple rank two polymorphism" $
run
[ "id : forall a. a -> a;"
, "id x = x;"
, "f : forall a. a -> (forall b. b -> b) -> a;"
, "f x g = g x;"
, "main = f 4 id;"
]
`shouldSatisfy` ok
tc_const = specify "Basic polymorphism with multiple type variables" $ run tc_rank2 =
[ "const : forall a. forall b. a -> b -> a;" specify "Rank two polymorphism is ok" $
, "const x y = x;" run
, "main = const 'a' 65;" [ "const : forall a. forall b. a -> b -> a;"
] `shouldSatisfy` ok , "const x y = x;"
, "rank2 : forall a. forall b. a -> (forall c. c -> Int) -> b -> Int;"
tc_simple_rank2 = specify "Simple rank two polymorphism" $ run , "rank2 x f y = f x + f y;"
[ "id : forall a. a -> a;" , "main = rank2 3 (\\x. const 5 x : forall a. a -> Int) 'h';"
, "id x = x;" ]
`shouldSatisfy` ok
, "f : forall a. a -> (forall b. b -> b) -> a;"
, "f x g = g x;"
, "main = f 4 id;"
] `shouldSatisfy` ok
tc_rank2 = specify "Rank two polymorphism is ok" $ run
[ "const : forall a. forall b. a -> b -> a;"
, "const x y = x;"
, "rank2 : forall a. forall b. a -> (forall c. c -> Int) -> b -> Int;"
, "rank2 x f y = f x + f y;"
, "main = rank2 3 (\\x. const 5 x : forall a. a -> Int) 'h';"
] `shouldSatisfy` ok
tc_identity = describe "(∀b. b → b) should only accept the identity function" $ do tc_identity = describe "(∀b. b → b) should only accept the identity function" $ do
specify "identityᵢₙₜ is rejected" $ run (fs ++ id_int) `shouldNotSatisfy` ok specify "identityᵢₙₜ is rejected" $ run (fs ++ id_int) `shouldNotSatisfy` ok
specify "identity is accepted" $ run (fs ++ id) `shouldSatisfy` ok specify "identity is accepted" $ run (fs ++ id) `shouldSatisfy` ok
where where
fs = fs =
[ "f : forall a. a -> (forall b. b -> b) -> a;" [ "f : forall a. a -> (forall b. b -> b) -> a;"
, "f x g = g x;" , "f x g = g x;"
, "id : forall a. a -> a;" , "id : forall a. a -> a;"
, "id x = x;" , "id x = x;"
, "id_int : Int -> Int;" , "id_int : Int -> Int;"
, "id_int x = x;" , "id_int x = x;"
] ]
@ -101,37 +110,35 @@ tc_pair = describe "Pair. Type variables in Pair a b typechecked" $ do
[ "data forall a. forall b. Pair (a b) where {" [ "data forall a. forall b. Pair (a b) where {"
, " Pair : a -> b -> Pair (a b)" , " Pair : a -> b -> Pair (a b)"
, "};" , "};"
, "main : Pair (Int Char);" , "main : Pair (Int Char);"
] ]
wrong = ["main = Pair 'a' 65;"] wrong = ["main = Pair 'a' 65;"]
correct = ["main = Pair 65 'a';"] correct = ["main = Pair 65 'a';"]
tc_tree = describe "Tree. Recursive data type" $ do tc_tree = describe "Tree. Recursive data type" $ do
specify "Wrong tree is rejected" $ run (fs ++ wrong) `shouldNotSatisfy` ok specify "Wrong tree is rejected" $ run (fs ++ wrong) `shouldNotSatisfy` ok
specify "Correct tree is accepted" $ run (fs ++ correct) `shouldSatisfy` ok specify "Correct tree is accepted" $ run (fs ++ correct) `shouldSatisfy` ok
where where
fs = fs =
[ "data forall a. Tree (a) where {" [ "data forall a. Tree (a) where {"
, " Node : a -> Tree (a) -> Tree (a) -> Tree (a)" , " Node : a -> Tree (a) -> Tree (a) -> Tree (a)"
, " Leaf : a -> Tree (a)" , " Leaf : a -> Tree (a)"
, "};" , "};"
] ]
wrong = ["tree = Node 1 (Node 2 (Node 4) (Leaf 5)) (Leaf 3);"] wrong = ["tree = Node 1 (Node 2 (Node 4) (Leaf 5)) (Leaf 3);"]
correct = ["tree = Node 1 (Node 2 (Leaf 4) (Leaf 5)) (Leaf 3);"] correct = ["tree = Node 1 (Node 2 (Leaf 4) (Leaf 5)) (Leaf 3);"]
tc_mono_case = describe "Monomorphic pattern matching" $ do tc_mono_case = describe "Monomorphic pattern matching" $ do
specify "First wrong case expression rejected" specify "First wrong case expression rejected" $
$ run wrong1 `shouldNotSatisfy` ok run wrong1 `shouldNotSatisfy` ok
specify "Second wrong case expression rejected" specify "Second wrong case expression rejected" $
$ run wrong2 `shouldNotSatisfy` ok run wrong2 `shouldNotSatisfy` ok
specify "Third wrong case expression rejected" specify "Third wrong case expression rejected" $
$ run wrong3 `shouldNotSatisfy` ok run wrong3 `shouldNotSatisfy` ok
specify "First correct case expression accepted" specify "First correct case expression accepted" $
$ run correct1 `shouldSatisfy` ok run correct1 `shouldSatisfy` ok
specify "Second correct case expression accepted" specify "Second correct case expression accepted" $
$ run correct2 `shouldSatisfy` ok run correct2 `shouldSatisfy` ok
where where
wrong1 = wrong1 =
[ "simple : Int -> Int;" [ "simple : Int -> Int;"
@ -170,16 +177,16 @@ tc_mono_case = describe "Monomorphic pattern matching" $ do
] ]
tc_pol_case = describe "Polymophic pattern matching" $ do tc_pol_case = describe "Polymophic pattern matching" $ do
specify "First wrong case expression rejected" specify "First wrong case expression rejected" $
$ run (fs ++ wrong1) `shouldNotSatisfy` ok run (fs ++ wrong1) `shouldNotSatisfy` ok
specify "Second wrong case expression rejected" specify "Second wrong case expression rejected" $
$ run (fs ++ wrong2) `shouldNotSatisfy` ok run (fs ++ wrong2) `shouldNotSatisfy` ok
specify "Third wrong case expression rejected" specify "Third wrong case expression rejected" $
$ run (fs ++ wrong3) `shouldNotSatisfy` ok run (fs ++ wrong3) `shouldNotSatisfy` ok
specify "First correct case expression accepted" specify "First correct case expression accepted" $
$ run (fs ++ correct1) `shouldSatisfy` ok run (fs ++ correct1) `shouldSatisfy` ok
specify "Second correct case expression accepted" specify "Second correct case expression accepted" $
$ run (fs ++ correct2) `shouldSatisfy` ok run (fs ++ correct2) `shouldSatisfy` ok
where where
fs = fs =
[ "data forall a. List (a) where {" [ "data forall a. List (a) where {"
@ -225,8 +232,8 @@ tc_pol_case = describe "Polymophic pattern matching" $ do
] ]
run :: [String] -> Err T.Program run :: [String] -> Err T.Program
run = rmTEVar <=< typecheck <=< pProgram . myLexer . unlines run = rmTEVar <=< typecheck <=< pProgram . myLexer . unlines
ok = \case ok = \case
Ok _ -> True Ok _ -> True
Bad _ -> False Bad _ -> False

13
tests/TestTypeCheckerHm.hs
View file

@ -7,16 +7,15 @@ import Control.Monad ((<=<))
import DoStrings qualified as D import DoStrings qualified as D
import Grammar.Par (myLexer, pProgram) import Grammar.Par (myLexer, pProgram)
import Test.Hspec import Test.Hspec
import Prelude (Bool (..), Either (..), IO, mapM_, not, ($), (.)) import Prelude (Bool (..), Either (..), IO, foldl1, mapM_, not, ($), (.), (>>))
-- import Test.QuickCheck -- import Test.QuickCheck
import TypeChecker.TypeChecker (typecheck) import TypeChecker.TypeCheckerHm (typecheck)
main :: IO () testTypeCheckerHm = describe "Hindley-Milner type checker test" $ do
main = do foldl1 (>>) goods
mapM_ hspec goods foldl1 (>>) bads
mapM_ hspec bads foldl1 (>>) bes
mapM_ hspec bes
goods = goods =
[ testSatisfy [ testSatisfy