sifflet-2.3.0: tests/Testing/Unit/TypeCheckTests.hs
-- 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