From 2adc3dceeea5421b7590e29108ebc84481229df8 Mon Sep 17 00:00:00 2001 From: sebastianselander Date: Mon, 27 Mar 2023 16:53:29 +0200 Subject: [PATCH] added old tests --- tests/TestTypeCheckerHm.hs | 249 +++++++++++++++++++++++++++---------- 1 file changed, 181 insertions(+), 68 deletions(-) diff --git a/tests/TestTypeCheckerHm.hs b/tests/TestTypeCheckerHm.hs index ae298c8..b5d14c6 100644 --- a/tests/TestTypeCheckerHm.hs +++ b/tests/TestTypeCheckerHm.hs @@ -1,81 +1,180 @@ {-# LANGUAGE QualifiedDo #-} {-# LANGUAGE NoImplicitPrelude #-} -module TestTypeCheckerHm (testTypeCheckerHm) where +module Main where import Control.Monad ((<=<)) import DoStrings qualified as D import Grammar.Par (myLexer, pProgram) import Test.Hspec -import Prelude ( - Bool (..), - Either (..), - IO, - fmap, - not, - ($), - (.), - ) +import Prelude (Bool (..), Either (..), IO, mapM_, not, ($), (.)) -- import Test.QuickCheck -import TypeChecker.TypeCheckerHm (typecheck) +import TypeChecker.TypeChecker (typecheck) -testTypeCheckerHm = describe "Hillner Milner type checker test" $ do - ok1 - ok2 - bad1 - bad2 +main :: IO () +main = do + mapM_ hspec goods + mapM_ hspec bads + mapM_ hspec bes --- bad3 +goods = + [ testSatisfy + "Basic polymorphism with multiple type variables" + ( D.do + _const + "main = const 'a' 65 ;" + ) + ok + , testSatisfy + "Head with a correct signature is accepted" + ( D.do + _List + _headSig + _head + ) + ok + , testSatisfy + "Most simple inference possible" + ( D.do + _id + ) + ok + , testSatisfy + "Pattern matching on a nested list" + ( D.do + _List + "main : List (List (a)) -> Int ;" + "main xs = case xs of {" + " Cons Nil _ => 1 ;" + " _ => 0 ;" + "};" + ) + ok + ] -ok1 = - specify "Basic polymorphism with multiple type variables" $ - run - ( D.do - const - "main = const 'a' 65 ;" - ) - `shouldSatisfy` ok -ok2 = - specify "Head with a correct signature is accepted" $ - run - ( D.do - list - headSig - head - ) - `shouldSatisfy` ok +bads = + [ testSatisfy + "Infinite type unification should not succeed" + ( D.do + "main = \\x. x x ;" + ) + bad + , testSatisfy + "Pattern matching using different types should not succeed" + ( D.do + _List + "bad xs = case xs of {" + " 1 => 0 ;" + " Nil => 0 ;" + "};" + ) + bad + , testSatisfy + "Using a concrete function (data type) on a skolem variable should not succeed" + ( D.do + _Bool + _not + "f : a -> Bool () ;" + "f x = not x ;" + ) + bad + , testSatisfy + "Using a concrete function (primitive type) on a skolem variable should not succeed" + ( D.do + "plusOne : Int -> Int ;" + "plusOne x = x + 1 ;" + "f : a -> Int ;" + "f x = plusOne x ;" + ) + bad + , testSatisfy + "A function without signature used in an incompatible context should not succeed" + ( D.do + "main = _id 1 2 ;" + "_id x = x ;" + ) + bad + , testSatisfy + "Pattern matching on literal and _List should not succeed" + ( D.do + _List + "length : List (c) -> Int;" + "length _List = case _List of {" + " 0 => 0;" + " Cons x xs => 1 + length xs;" + "};" + ) + bad + , testSatisfy + "List of function Int -> Int functions should not be usable on Char" + ( D.do + _List + "main : List (Int -> Int) -> Int ;" + "main xs = case xs of {" + " Cons f _ => f 'a' ;" + " Nil => 0 ;" + " };" + ) + bad + , testSatisfy + "id with incorrect signature" + ( D.do + "id : a -> b;" + "id x = x;" + ) + bad + , testSatisfy + "incorrect type signature on id lambda" + ( D.do + "id = ((\\x. x) : a -> b);" + ) + bad + ] -bad1 = - specify "Infinite type unification should not succeed" $ - run - ( D.do - "main = \\x. x x ;" - ) - `shouldSatisfy` bad +bes = + [ testBe + "A basic arithmetic function should be able to be inferred" + ( D.do + "plusOne x = x + 1 ;" + "main x = plusOne x ;" + ) + ( D.do + "plusOne : Int -> Int ;" + "plusOne x = x + 1 ;" + "main : Int -> Int ;" + "main x = plusOne x ;" + ) + , testBe + "A basic arithmetic function should be able to be inferred" + ( D.do + "plusOne x = x + 1 ;" + ) + ( D.do + "plusOne : Int -> Int ;" + "plusOne x = x + 1 ;" + ) + , testBe + "List of function Int -> Int functions should be inferred corretly" + ( D.do + _List + "main xs = case xs of {" + " Cons f _ => f 1 ;" + " Nil => 0 ;" + " };" + ) + ( D.do + _List + "main : List (Int -> Int) -> Int ;" + "main xs = case xs of {" + " Cons f _ => f 1 ;" + " Nil => 0 ;" + " };" + ) + ] -bad2 = - specify "Pattern matching using different types should not succeed" $ - run - ( D.do - list - "bad xs = case xs of {" - " 1 => 0 ;" - " Nil => 0 ;" - "};" - ) - `shouldSatisfy` bad - -bad3 = - specify "Using a concrete function on a skolem variable should not succeed" $ - run - ( D.do - bool - _not - "f : a -> Bool () ;" - " f x = not x ;" - ) - `shouldSatisfy` bad +testSatisfy desc test satisfaction = specify desc $ run test `shouldSatisfy` satisfaction +testBe desc test shouldbe = specify desc $ run test `shouldBe` run shouldbe run = typecheck <=< pProgram . myLexer @@ -86,25 +185,26 @@ bad = not . ok -- FUNCTIONS -const = D.do +_const = D.do "const : a -> b -> a ;" "const x y = x ;" -list = D.do +_List = D.do "data List (a) where" " {" " Nil : List (a)" " Cons : a -> List (a) -> List (a)" " };" -headSig = D.do +_headSig = D.do "head : List (a) -> a ;" -head = D.do + +_head = D.do "head xs = " " case xs of {" " Cons x xs => x ;" " };" -bool = D.do +_Bool = D.do "data Bool () where {" " True : Bool ()" " False : Bool ()" @@ -116,3 +216,16 @@ _not = D.do " True => False ;" " False => True ;" "};" +_id = "id x = x ;" + +_Maybe = D.do + "data Maybe (a) where {" + " Nothing : Maybe (a)" + " Just : a -> Maybe (a)" + " };" + +_fmap = D.do + "fmap f ma = case ma of {" + " Nothing => Nothing ;" + " Just a => Just (f a) ;" + "};"