diff --git a/tests/TestTypeCheckerBidir.hs b/tests/TestTypeCheckerBidir.hs index 3a20ca6..1aaaf62 100644 --- a/tests/TestTypeCheckerBidir.hs +++ b/tests/TestTypeCheckerBidir.hs @@ -1,86 +1,95 @@ +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PatternSynonyms #-} {-# HLINT ignore "Use camelCase" #-} {-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE PatternSynonyms #-} module TestTypeCheckerBidir (testTypeCheckerBidir) where -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 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 TypeChecker.TypeCheckerIr qualified as T testTypeCheckerBidir = describe "Bidirectional type checker test" $ do - tc_id - tc_double - tc_add_lam - tc_const - tc_simple_rank2 - tc_rank2 - tc_identity - tc_pair - tc_tree - tc_mono_case - tc_pol_case + tc_id + tc_double + tc_add_lam + tc_const + tc_simple_rank2 + tc_rank2 + tc_identity + tc_pair + tc_tree + tc_mono_case + tc_pol_case -tc_id = specify "Basic identity function polymorphism" $ run - [ "id : forall a. a -> a;" - , "id x = x;" - , "main = id 4;" - ] `shouldSatisfy` ok +tc_id = + specify "Basic identity function polymorphism" $ + run + [ "id : forall a. a -> a;" + , "id x = x;" + , "main = id 4;" + ] + `shouldSatisfy` ok -tc_double = specify "Addition inference" $ run - ["double x = x + x;"] `shouldSatisfy` ok +tc_double = + 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 - ["four = (\\x. x + x) 2;"] `shouldSatisfy` ok +tc_const = + 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 - [ "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_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_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 - specify "identityᵢₙₜ is rejected" $ run (fs ++ id_int) `shouldNotSatisfy` ok - specify "identity is accepted" $ run (fs ++ id) `shouldSatisfy` ok + specify "identityᵢₙₜ is rejected" $ run (fs ++ id_int) `shouldNotSatisfy` ok + specify "identity is accepted" $ run (fs ++ id) `shouldSatisfy` ok where fs = [ "f : forall a. a -> (forall b. b -> b) -> a;" , "f x g = g x;" - , "id : forall a. a -> a;" , "id x = x;" - , "id_int : Int -> Int;" , "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 {" , " Pair : a -> b -> Pair (a b)" , "};" - , "main : Pair (Int Char);" ] - wrong = ["main = Pair 'a' 65;"] + wrong = ["main = Pair 'a' 65;"] correct = ["main = Pair 65 'a';"] tc_tree = describe "Tree. Recursive data type" $ do specify "Wrong tree is rejected" $ run (fs ++ wrong) `shouldNotSatisfy` ok specify "Correct tree is accepted" $ run (fs ++ correct) `shouldSatisfy` ok where - fs = + fs = [ "data forall a. Tree (a) where {" , " Node : a -> Tree (a) -> Tree (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);"] tc_mono_case = describe "Monomorphic pattern matching" $ do - specify "First wrong case expression rejected" - $ run wrong1 `shouldNotSatisfy` ok - specify "Second wrong case expression rejected" - $ run wrong2 `shouldNotSatisfy` ok - specify "Third wrong case expression rejected" - $ run wrong3 `shouldNotSatisfy` ok - specify "First correct case expression accepted" - $ run correct1 `shouldSatisfy` ok - specify "Second correct case expression accepted" - $ run correct2 `shouldSatisfy` ok - + specify "First wrong case expression rejected" $ + run wrong1 `shouldNotSatisfy` ok + specify "Second wrong case expression rejected" $ + run wrong2 `shouldNotSatisfy` ok + specify "Third wrong case expression rejected" $ + run wrong3 `shouldNotSatisfy` ok + specify "First correct case expression accepted" $ + run correct1 `shouldSatisfy` ok + specify "Second correct case expression accepted" $ + run correct2 `shouldSatisfy` ok where wrong1 = [ "simple : Int -> Int;" @@ -170,16 +177,16 @@ tc_mono_case = describe "Monomorphic pattern matching" $ do ] tc_pol_case = describe "Polymophic pattern matching" $ do - specify "First wrong case expression rejected" - $ run (fs ++ wrong1) `shouldNotSatisfy` ok - specify "Second wrong case expression rejected" - $ run (fs ++ wrong2) `shouldNotSatisfy` ok - specify "Third wrong case expression rejected" - $ run (fs ++ wrong3) `shouldNotSatisfy` ok - specify "First correct case expression accepted" - $ run (fs ++ correct1) `shouldSatisfy` ok - specify "Second correct case expression accepted" - $ run (fs ++ correct2) `shouldSatisfy` ok + specify "First wrong case expression rejected" $ + run (fs ++ wrong1) `shouldNotSatisfy` ok + specify "Second wrong case expression rejected" $ + run (fs ++ wrong2) `shouldNotSatisfy` ok + specify "Third wrong case expression rejected" $ + run (fs ++ wrong3) `shouldNotSatisfy` ok + specify "First correct case expression accepted" $ + run (fs ++ correct1) `shouldSatisfy` ok + specify "Second correct case expression accepted" $ + run (fs ++ correct2) `shouldSatisfy` ok where fs = [ "data forall a. List (a) where {" @@ -225,8 +232,8 @@ tc_pol_case = describe "Polymophic pattern matching" $ do ] run :: [String] -> Err T.Program -run = rmTEVar <=< typecheck <=< pProgram . myLexer . unlines +run = rmTEVar <=< typecheck <=< pProgram . myLexer . unlines ok = \case - Ok _ -> True - Bad _ -> False + Ok _ -> True + Bad _ -> False diff --git a/tests/TestTypeCheckerHm.hs b/tests/TestTypeCheckerHm.hs index ce72c63..f3d8dd6 100644 --- a/tests/TestTypeCheckerHm.hs +++ b/tests/TestTypeCheckerHm.hs @@ -7,16 +7,15 @@ import Control.Monad ((<=<)) import DoStrings qualified as D import Grammar.Par (myLexer, pProgram) import Test.Hspec -import Prelude (Bool (..), Either (..), IO, mapM_, not, ($), (.)) +import Prelude (Bool (..), Either (..), IO, foldl1, mapM_, not, ($), (.), (>>)) -- import Test.QuickCheck -import TypeChecker.TypeChecker (typecheck) +import TypeChecker.TypeCheckerHm (typecheck) -main :: IO () -main = do - mapM_ hspec goods - mapM_ hspec bads - mapM_ hspec bes +testTypeCheckerHm = describe "Hindley-Milner type checker test" $ do + foldl1 (>>) goods + foldl1 (>>) bads + foldl1 (>>) bes goods = [ testSatisfy