added old tests

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 (
+import Prelude (Bool (..), Either (..), IO, mapM_, not, ($), (.))
-    Bool (..),
-    Either (..),
-    IO,
-    fmap,
-    not,
-    ($),
-    (.),
- )
 
 -- import Test.QuickCheck
-import TypeChecker.TypeCheckerHm (typecheck)
+import TypeChecker.TypeChecker (typecheck)
 
-testTypeCheckerHm = describe "Hillner Milner type checker test" $ do
+main :: IO ()
-    ok1
+main = do
-    ok2
+    mapM_ hspec goods
-    bad1
+    mapM_ hspec bads
-    bad2
+    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 =
+bads =
-    specify "Basic polymorphism with multiple type variables" $
+    [ testSatisfy
-        run
+        "Infinite type unification should not succeed"
-            ( D.do
+        ( D.do
-                const
+            "main = \\x. x x ;"
-                "main = const 'a' 65 ;"
+        )
-            )
+        bad
-            `shouldSatisfy` ok
+    , testSatisfy
-ok2 =
+        "Pattern matching using different types should not succeed"
-    specify "Head with a correct signature is accepted" $
+        ( D.do
-        run
+            _List
-            ( D.do
+            "bad xs = case xs of {"
-                list
+            "   1 => 0 ;"
-                headSig
+            "   Nil => 0 ;"
-                head
+            "};"
-            )
+        )
-            `shouldSatisfy` ok
+        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 =
+bes =
-    specify "Infinite type unification should not succeed" $
+    [ testBe
-        run
+        "A basic arithmetic function should be able to be inferred"
-            ( D.do
+        ( D.do
-                "main = \\x. x x ;"
+            "plusOne x = x + 1 ;"
-            )
+            "main x = plusOne x ;"
-            `shouldSatisfy` bad
+        )
+        ( 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 =
+testSatisfy desc test satisfaction = specify desc $ run test `shouldSatisfy` satisfaction
-    specify "Pattern matching using different types should not succeed" $
+testBe desc test shouldbe = specify desc $ run test `shouldBe` run shouldbe
-        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
 
 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) ;"
+    "};"