-- Unit tests for type checker module Testing.Unit.TypeCheckTests (tests, runU) where import Data.Map (fromList) import Test.HUnit import Language.Sifflet.Expr import Language.Sifflet.TypeCheck import Language.Sifflet.Util import Testing.TestUtil import Testing.Unit.ParserTests (int, float) testTypeCheckValues :: Test testTypeCheckValues = let checkSucc :: String -> [Value] -> [Type] -> Assertion checkSucc alabel values types = check alabel values types (Succ values) checkFail :: String -> [Value] -> [Type] -> String -> Assertion checkFail alabel values types = check alabel values types . Fail check :: String -> [Value] -> [Type] -> SuccFail [Value] -> Assertion check alabel values types result = let names = ['x' : show i | i <- take (length values) [1..] :: [Int]] in assertEqual ("typeCheckValues: " ++ alabel) result (typeCheckValues names types values) in assertAll [checkSucc "int" [int 32] [typeNum], checkSucc "float" [float (-1.7)] [typeNum], checkSucc "list of int" [VList (map int [-7, 16, 24])] [typeList typeNum], checkSucc "list of number" [VList [float 3.5, int 7]] [typeList typeNum], checkFail "list of mixed types" [VList [float 3.5, VString "pony"]] [typeList typeNum] ("For variable x1:\n\"pony\": " ++ "number expected"), checkSucc "int bool float" [int 7, VBool False, float 3.5] [typeNum, typeBool, typeNum], checkSucc "typevars a b c" [int 7, VBool False, float 3.5] [TypeVar "a", TypeVar "b", TypeVar "c"], checkSucc "typevars a a a" [int 18, int 21, int 9] [TypeVar "a", TypeVar "a", TypeVar "a"], checkFail "typevars a not-a" [int (-21), VString "roads"] [TypeVar "a", TypeVar "a"] "For variable x2:\n\"roads\": number expected" ] testTypeVarsIn :: Test testTypeVarsIn = assertAll [assertEqual "typeVarsIn t1" ["t1"] (typeVarsIn (TypeVar "t1")) , assertEqual "typeVarsIn typeNum" [] (typeVarsIn typeNum) , assertEqual "typeVarsIn [t2]" ["t2"] (typeVarsIn (typeList (TypeVar "t2"))) , assertEqual "typeVarsIn t3 -> t4 -> t5" ["t3", "t4", "t5"] (typeVarsIn (typeFunction [TypeVar "t3", TypeVar "t4"] (TypeVar "t5"))) ] d1, d2, d3 :: Subst d1 = deltaSubst "t1" typeNum d2 = deltaSubst "t2" typeBool d3 = deltaSubst "t3" (TypeVar "t1") s1, s2 :: Subst s1 = idSubst s2 = substComp d1 d2 mapType, foldrType :: Type -> Type -> Type mapType t1 t2 = typeFunction [typeFunction [t1] t2, typeList t1] (typeList t2) foldrType t1 t2 = typeFunction [typeFunction [t1] t2, t2, typeList t1] t2 testSubst :: Test testSubst = assertAll [assertEqual "testSubst t3 to t1 in t3" (TypeVar "t1") (subst d3 (TypeVar "t3")), assertEqual "testSubst t3 to t1 in [t3]" (typeList (TypeVar "t1")) (subst d3 (typeList (TypeVar "t3"))), assertEqual "testSubst idSubst in t4" (TypeVar "t4") (subst s1 (TypeVar "t4")), -- the type of the map function assertEqual "testSubst s2 in mapType" (mapType typeNum typeBool) (subst s2 (mapType (TypeVar "t1") (TypeVar "t2"))), -- the type of the foldr function assertEqual "testSubst s2 in foldrType" (foldrType typeNum typeBool) (subst s2 (foldrType (TypeVar "t1") (TypeVar "t2"))) ] testUnify :: Test testUnify = let uni t1 t2 = case unify idSubst (t1, t2) of Succ _ -> True Fail _ -> False yes name t1 t2 = assertBool name (uni t1 t2) no name t1 t2 = assertBool name (not (uni t1 t2)) in assertAll [yes "t1 with Bool" (TypeVar "t1") typeBool , yes "t2 with Char" (TypeVar "t2") typeChar , yes "t3 with t4" (TypeVar "t3") (TypeVar "t4") , no "Bool with Char" typeBool typeChar , yes "[t1] with [t6]" (typeList (TypeVar "t1")) (typeList (TypeVar "t6")) , yes "[t1] with [[Num]]" (typeList (TypeVar "t1")) (typeList (typeList typeNum)) , no "[String] with [Num]" (typeList typeString) (typeList typeNum) , yes "t1 -> t2 with Num -> Bool" (typeFunction [TypeVar "t1"] (TypeVar "t2")) (typeFunction [typeNum] typeBool) , no "t1 -> t2 -> t3 with Num -> Bool" (typeFunction [TypeVar "t1", TypeVar "t2"] (TypeVar "t3")) (typeFunction [typeNum] typeBool) ] ts1, ts2 :: TypeScheme ts1 = TypeScheme ["t1", "t2"] (typeFunction [TypeVar "t1", TypeVar "t2", TypeVar "t3"] (TypeVar "t4")) ts2 = TypeScheme ["t1", "t2"] (typeFunction [TypeVar "t1", TypeVar "t2", typeNum] typeBool) phi34 :: Subst phi34 = case extend (deltaSubst "t3" typeNum) "t4" typeBool of Succ s -> s Fail _ -> undefined testTypeScheme :: Test testTypeScheme = assertAll [assertEqual "substTS t3 t4 in a function type" ts2 (substTS phi34 ts1) , assertEqual "schematics of ts1" ["t1", "t2"] (schematicsTS ts1) , assertEqual "unknowns of ts1" ["t3", "t4"] (unknownsTS ts1)] te1, te2 :: TypeEnv te1 = fromList [("t16", ts1)] te2 = fromList [("t16", ts2)] testTypeEnv :: Test testTypeEnv = assertAll [assertEqual "unknowns of te1" ["t3", "t4"] (unknownsTE te1) , assertEqual "unknowns of te2" [] (unknownsTE te2) , assertEqual "substTE t3 t4 in te1 is te2" te2 (substTE phi34 te1)] testNS :: NameSupply testNS = newNameSupply "t" tc0 :: Expr -> SuccFail Type tc0 expr = case tcExpr emptyTypeEnv testNS expr of Succ (_, etype, _) -> Succ etype Fail msg -> Fail msg tc1 :: Expr -> SuccFail Type tc1 expr = case tcExpr baseTypeEnv testNS expr of Succ (_, etype, _) -> Succ etype Fail msg -> Fail msg testTypeCheckExpr1 :: Test testTypeCheckExpr1 = assertAll [ -- primitive type expressions assertEqual "tc bool" (Succ typeBool) (tc0 (EBool False)) , assertEqual "tc char" (Succ typeChar) (tc0 (EChar 'c')) , assertEqual "tc num (int)" (Succ typeNum) (tc0 (eInt 21)) , assertEqual "tc num (float)" (Succ typeNum) (tc0 (eFloat 2.1)) -- variables globally bound to functions , assertEqual "tc var (+)" (Succ (typeFunction [typeNum, typeNum] typeNum)) (tc1 (ESymbol (Symbol "+"))) , assertEqual "tc var (:)" (Succ (typeFunction [TypeVar "t1", typeList (TypeVar "t1")] (typeList (TypeVar "t1")))) (tc1 (ESymbol (Symbol ":"))) , assertEqual "tc var (null)" (Succ (typeFunction [typeList (TypeVar "t1")] typeBool)) (tc1 (ESymbol (Symbol "null"))) -- if expressions , assertEqual "tc if bool num num" (Succ (typeNum)) (tc1 (EIf (EBool True) (eInt 35) (eFloat 3.5))) , assertEqual "tc if bool char char" (Succ (typeChar)) (tc1 (EIf (EBool False) (EChar 'c') (EChar 'd'))) , assertEqual "tc if bool char num" (Fail "cannot unify Char with Num") (tc1 (EIf (EBool False) (EChar 'c') (eFloat 4.1))) , assertEqual "tc if string num num" (Fail "cannot unify String with Bool") (tc1 (EIf (EString "horses") (eInt 35) (eFloat 3.5))) -- list expressions , assertEqual "tc list []" (Succ (typeList (TypeVar "t1"))) (tc1 (EList [])) , assertEqual "tc list [35]" (Succ (typeList typeNum)) (tc1 (EList [eInt 35])) , assertEqual "tc list [35, 3.5]" (Succ (typeList typeNum)) (tc1 (EList [eInt 35, eFloat 3.5])) , assertEqual "tc list [35, 'c']" (Fail "cannot unify Num with Char") (tc1 (EList [eInt 35, eChar 'c'])) , assertEqual "tc list [1..10]" (Succ (TypeCons "List" [TypeCons "Num" []])) (tc1 (EList (map eInt [1..10]))) -- lambda expressions , assertEqual "tc lambda0" (Succ (TypeVar "t1" `arrow` typeNum)) (tc1 (ELambda (Symbol "y") (ENumber 0))) , assertEqual "tc lambda1" (Succ (TypeVar "t1" `arrow` typeList (TypeVar "t2"))) (tc1 (ELambda (Symbol "z") (EList []))) , assertEqual "tc lambda2" (Succ (TypeVar "t2" `arrow` typeList (TypeVar "t2"))) (tc1 (ELambda (Symbol "z") (EList [ESymbol (Symbol "z")]))) , assertEqual "tc lambda3" (Succ (TypeVar "t1" `arrow` (TypeVar "t2" `arrow` TypeVar "t1"))) (tc1 (ELambda (Symbol "c") (ELambda (Symbol "x") (ESymbol (Symbol "c"))))) ] testTypeCheckExpr2 :: Test testTypeCheckExpr2 = let -- 1 * 2 call4 = ECall (Symbol "*") [eInt 1, eInt 2] -- (1 + 2) * (7 - 3) call5 = ECall (Symbol "*") [ECall (Symbol "+") [eInt 1, eInt 2], ECall (Symbol "-") [eInt 7, eInt 3]] -- invalid cons expression: -- 7 : ["beeswax"] call6 = ECall (Symbol ":") [eInt 7, EList [EString "beeswax"]] -- add1 lambda4 = ELambda (Symbol "x") (ePlus (ESymbol (Symbol "x")) (eInt 1)) -- function with function argument lambda5 = ELambda (Symbol "f") (EList [EApp (ESymbol (Symbol "f")) (eInt 3), EApp (ESymbol (Symbol "f")) (eFloat 4.5)]) -- function with function value lambda6 = ELambda (Symbol "n") (ELambda (Symbol "k") (ECall (Symbol "+") [ESymbol (Symbol "n"), ESymbol (Symbol "k")])) -- invalid lambda expression: -- \x -> (x + 1) : x lambda7 = ELambda (Symbol "x") (ECall (Symbol ":") [ECall (Symbol "+") [ESymbol (Symbol "x"), eInt 1], ESymbol (Symbol "x")]) in assertAll [ assertEqual "tc call4" (Succ (TypeCons "Num" [])) (tc1 call4) , assertEqual "tc call5" (Succ (TypeCons "Num" [])) (tc1 call5) , assertEqual "tc call6" (Fail "cannot unify Num with String") (tc1 call6) , assertEqual "tc lambda4" (Succ (typeNum `arrow` typeNum)) (tc1 lambda4) , assertEqual "tc lambda5" (Succ ((typeNum `arrow` TypeVar "t4") `arrow` (typeList (TypeVar "t4")))) (tc1 lambda5) , assertEqual "tc lambda6" (Succ (typeNum `arrow` (typeNum `arrow` typeNum))) (tc1 lambda6) , assertEqual "tc lambda7" (Fail ("cannot unify [Num] with Num")) (tc1 lambda7) ] testFromLambdaType :: Test testFromLambdaType = let t1 = TypeVar "t1" t2 = TypeVar "t2" t3 = TypeVar "t3" in assertAll [assertEqual "fromLambdaType t1 -> t2" (Succ ([t1], t2)) (fromLambdaType (t1 `arrow` t2)) , assertEqual "fromLambdaType t1 -> (t2 -> t3)" (Succ ([t1, t2], t3)) (fromLambdaType (t1 `arrow` (t2 `arrow` t3))) ] tests :: Test tests = TestList [TestLabel "typeVarsIn" testTypeVarsIn, TestLabel "typeCheckValues" testTypeCheckValues, TestLabel "subst" testSubst, TestLabel "unify" testUnify, TestLabel "TypeScheme" testTypeScheme, TestLabel "TypeEnv" testTypeEnv, TestLabel "tcExpr1" testTypeCheckExpr1, TestLabel "tcExpr2" testTypeCheckExpr2, TestLabel "fromLambdaType" testFromLambdaType ] runU :: IO () runU = utestloop tests