Commit 8ea9bad4 authored by André Pacak's avatar André Pacak
Browse files

test cases for record types + check that term and types have same length

parent 5a52fc1d
......@@ -118,9 +118,13 @@ checkType ctx p@(Pair t1 t2 _) ty = do
checkType ctx t2 ty2
checkType ctx p@(Rec tpairs _) ty = do
typairs <- matchRecord ty (show p)
let zipped = zip tpairs typairs
let subresults = map (\((x, t), (x', tty)) -> if x == x' then checkType ctx t tty else fail "Labels of record term and record type do not match") zipped
foldl (\r e -> r >> e) (return ()) subresults
if (length tpairs) == (length typairs)
then do
let zipped = zip tpairs typairs
let subresults = map (\((x, t), (x', tty)) -> if x == x' then checkType ctx t tty else fail "Labels of record term and record type do not match") zipped
foldl (\r e -> r >> e) (return ()) subresults
else do
fail "Length of term labels and type labels does not match"
checkType ctx p@(InL t _) ty = do
(ty1, ty2) <- matchSum ty (show p)
checkType ctx t ty1
......
......@@ -241,9 +241,13 @@ checkType p@(Pair t1 t2 _) = do
checkType p@(Rec tpairs _) = do
ty <- requiredType p
typairs <- matchRecord ty (show p)
let zipped = zip tpairs typairs
let subresults = map (\((x, t), (x', tty)) -> if x == x' then checkType t else fail ["Labels of record term and record type do not match"]) zipped
foldl (\r e -> r >> e) (return ()) subresults
if (length tpairs) == (length typairs)
then do
let zipped = zip tpairs typairs
let subresults = map (\((x, t), (x', tty)) -> if x == x' then checkType t else fail ["Labels of record term and record type do not match"]) zipped
foldl (\r e -> r >> e) (return ()) subresults
else do
fail ["Length of term labels and type labels does not match"]
checkType p@(InL t _) = do
ty <- requiredType p
(ty1, ty2) <- matchSum ty (show p)
......@@ -300,8 +304,12 @@ requiredType t = case parent t of
Just p@(Rec tpairs _) -> do
ty <- requiredType p
typairs <- matchRecord ty (show p)
let zipped = zip tpairs typairs
liftSnd (liftSndFromMaybe (find (\((x, t'), (x', tty)) -> t == t' && x == x') zipped) "") ""
if (length tpairs) == (length typairs)
then do
let zipped = zip tpairs typairs
liftSnd (liftSndFromMaybe (find (\((x, t'), (x', tty)) -> t == t' && x == x') zipped) "") ""
else do
fail ["Length of term labels and type labels does not match"]
Just p@(InL term _) | t == term -> do
ty <- requiredType p
(ty1, ty2) <- matchSum ty (show p)
......
......@@ -171,9 +171,13 @@ checkType ctx p@(Pair t1 t2 _) = do
checkType ctx p@(Rec tpairs _) = do
ty <- requiredType ctx p
typairs <- matchRecord ty (show p)
let zipped = zip tpairs typairs
let subresults = map (\((x, t), (x', tty)) -> if x == x' then checkType ctx t else fail ["Labels of record term and record type do not match"]) zipped
foldl (\r e -> r >> e) (return ()) subresults
if (length tpairs) == (length typairs)
then do
let zipped = zip tpairs typairs
let subresults = map (\((x, t), (x', tty)) -> if x == x' then checkType ctx t else fail ["Labels of record term and record type do not match"]) zipped
foldl (\r e -> r >> e) (return ()) subresults
else do
fail ["Length of term labels and type labels does not match"]
-- checkType ctx p@(Rec [(x, t)] _) = do
-- ty <- requiredType ctx p
-- [(x', tty)] <- matchRecord ty (show p)
......@@ -262,8 +266,12 @@ requiredType ctx t = case parent t of
Just p@(Rec tpairs _) -> do
ty <- requiredType ctx p
typairs <- matchRecord ty (show p)
let zipped = zip tpairs typairs
liftSnd (liftSndFromMaybe (find (\((x, t'), (x', tty)) -> t == t' && x == x') zipped) "") ""
if (length tpairs) == (length typairs)
then do
let zipped = zip tpairs typairs
liftSnd (liftSndFromMaybe (find (\((x, t'), (x', tty)) -> t == t' && x == x') zipped) "") ""
else do
fail ["Length of term labels and type labels does not match"]
Just p@(InL term _) | t == term -> do
ty <- requiredType ctx p
(ty1, ty2) <- matchSum ty (show p)
......
module ExtendedTLC.ErrorList where
import Prelude hiding (lookup, Ord)
import Data.List(find)
import ExtendedTLC.Language
import Util.ErrorMessages
......@@ -94,6 +95,11 @@ inferType ctx (Snd t _) = do
ty <- inferType ctx t
(_, ty2) <- matchProd ty (show t)
return ty2
inferType ctx (Sel n t _) = do
ty <- inferType ctx t
typairs <- matchRecord ty (show t)
tyn <- liftSnd (find (\p -> fst p == n) typairs) n
return $ tyn
inferType _ t = fail $ "Cannot infer type of term " ++ show t
checkType :: Ctx -> Term -> Type -> Check
......@@ -106,9 +112,13 @@ checkType ctx p@(Pair t1 t2 _) ty = do
checkType ctx t2 ty2
checkType ctx p@(Rec tpairs _) ty = do
typairs <- matchRecord ty (show p)
let zipped = zip tpairs typairs
let subresults = map (\((x, t), (x', tty)) -> if x == x' then checkType ctx t tty else fail "Labels of record term and record type do not match") zipped
foldl (\r e -> r >> e) (return ()) subresults
if (length tpairs) == (length typairs)
then do
let zipped = zip tpairs typairs
let subresults = map (\((x, t), (x', tty)) -> if x == x' then checkType ctx t tty else fail "Labels of record term and record type do not match") zipped
foldl (\r e -> r >> e) (return ()) subresults
else do
fail "Length of term labels and type labels does not match"
checkType ctx p@(InL t _) ty = do
(ty1, ty2) <- matchSum ty (show p)
checkType ctx t ty1
......
......@@ -113,6 +113,10 @@ inr = cons1 InR
case' e n1 t1 n2 t2 parent = let res = Case (e (Just res)) n1 (t1 (Just res)) n2 (t2 (Just res)) parent in res
rec0 parent = let res = Rec [] parent in res
rec1 (l1, t1) parent = let res = Rec [(l1, (t1 (Just res)))] parent in res
rec2 (l1, t1) (l2, t2) parent = let res = Rec [(l1, (t1 (Just res))), (l2, (t2 (Just res)))] parent in res
rec3 (l1, t1) (l2, t2) (l3, t3) parent = let res = Rec [(l1, (t1 (Just res))), (l2, (t2 (Just res))), (l3, (t3 (Just res)))] parent in res
instance Show Term where
showsPrec _ (Var x _) = showString x
......@@ -136,6 +140,8 @@ instance Show Term where
showString "let " . showString n . showString " = " . showsPrec (p + 1) e . showString " in " . showsPrec (p + 1) b
showsPrec p (InL t _) = showString "InL " . showsPrec (p + 1) t
showsPrec p (InR t _) = showString "InR " . showsPrec (p + 1) t
showsPrec p (Sel n t _) = showString "Sel " . showsPrec (p + 1) t . showString "." . showString n
showsPrec p (Rec pairs _) = showString "pair"
data Type = Nat | Fun Type Type | Prod Type Type | Record [(Name, Type)] | Sum Type Type | AnyType
deriving (Show, Eq)
......
......@@ -57,6 +57,18 @@ sharedSpec inferType = do
let res = convert $ inferType tOkCaseRight in res `shouldBe` B.Inferred Nat
it "should infer case with shadowing variable name" $ do
let res = convert $ inferType tOkCaseLeftShadowBinding in res `shouldBe` B.Inferred Nat
it "should infer empty record" $ do
let res = convert $ inferType tOkRecEmpty in res `shouldBe` B.Inferred (Record [])
it "should infer record with one" $ do
let res = convert $ inferType tOkRecSingle in res `shouldBe` B.Inferred (Record [("x", (Prod Nat Nat))])
it "should infer record with two entries" $ do
let res = convert $ inferType tOkRecSimple in res `shouldBe` B.Inferred (Record [("a", Nat), ("b", (Fun Nat Nat))])
it "should infer selection of records first element" $ do
let res = convert $ inferType $ tSelectionOf "a" in res `shouldBe` B.Inferred Nat
it "should infer selection of records second element" $ do
let res = convert $ inferType $ tSelectionOf "b" in res `shouldBe` B.Inferred (Fun Nat Nat)
it "should infer selection of records third element" $ do
let res = convert $ inferType $ tSelectionOf "c" in res `shouldBe` B.Inferred (Prod Nat (Fun Nat Nat))
it "should fail while inferring an arithmetic expression with an unapplied lambda expression" $ do
let res = isInferred $ convert $ inferType tFailArithmetic in res `shouldBe` False
......@@ -82,3 +94,11 @@ sharedSpec inferType = do
let res = isInferred $ convert $ inferType tFailCaseUnequalReturnTypes in res `shouldBe` False
it "should fail while matching on right injection where binding should shadow" $ do
let res = isInferred $ convert $ inferType tFailCaseRightShadowBinding in res `shouldBe` False
it "should fail while infering record with not matching label" $ do
let res = isInferred $ convert $ inferType tFailRecSingleWrongName in res `shouldBe` False
it "should fail while infering record where type has wrong order of labels" $ do
let res = isInferred $ convert $ inferType tFailRecWrongOrder in res `shouldBe` False
it "should fail while infering record where term has more labels thatn type" $ do
let res = isInferred $ convert $ inferType tFailUnequalNumberOfLabels in res `shouldBe` False
it "should fail while selecting label that is not present in record" $ do
let res = isInferred $ convert $ inferType tFailWrongSelection in res `shouldBe` False
......@@ -17,6 +17,12 @@ tOkAppLambdaAnno = root $ (app (anno (Fun Nat Nat) (lam "b" (add (var "b") zero)
tOkAnnoInBindingLet = root $ (let' "e" (anno Nat (add zero (succ zero))) (mult (var "e") (succ zero)))
tOkLetInPairFst = root $ (anno (Prod Nat (Fun Nat Nat)) (pair (let' "e" zero (succ $ succ (var "e"))) (lam "a" (succ (var "a")))))
tOkLetInPairSnd = root $ (anno (Prod (Fun Nat Nat) Nat) (pair (lam "n" (var "n")) (let' "e" zero (succ $ succ (var "e")))))
tOkRecEmpty = root $ (anno (Record []) rec0)
tOkRecSingle = root $ (anno (Record [("x", (Prod Nat Nat))]) (rec1 ("x", (pair zero (succ $ succ zero)))))
tOkRecSimple = root $ (anno (Record [("a", Nat), ("b", (Fun Nat Nat))]) (rec2 ("a", succ $ succ $ succ zero) ("b", (lam "a" $ zero))))
tSelectionOf :: Name -> Term
tSelectionOf n = root $ (sel n (anno (Record [("a", Nat), ("b", (Fun Nat Nat)), ("c", (Prod Nat (Fun Nat Nat)))]) (rec3 ("a", zero) ("b", (lam "a" $ zero)) ("c", (pair zero (lam "x" $ var "x"))))))
tOkInL = root $ (anno (Sum Nat (Fun Nat Nat)) (inl $ succ zero))
tOkInR = root $ (anno (Sum Nat (Prod Nat (Fun Nat Nat))) (inr (pair (succ $ succ zero) (anno (Fun Nat Nat) (lam "b" zero)))))
......@@ -38,3 +44,8 @@ tFailInL = root $ (anno (Sum Nat Nat) (inl (pair zero zero)))
tFailInR = root $ (anno (Sum Nat Nat) (inr (lam "x" $ var "x")))
tFailCaseUnequalReturnTypes = root $ (anno (Prod Nat Nat) (case' (anno Nat (inl $ succ $ succ zero)) "a" (pair zero zero) "b" zero))
tFailCaseRightShadowBinding = root $ (let' "a" zero (anno Nat (case' (anno (Sum Nat (Fun Nat Nat)) (inr $ lam "x" zero)) "a" zero "b" (var "b"))))
tFailRecSingleWrongName = root $ (anno (Record [("a", Nat)]) (rec1 ("b", zero)))
tFailRecWrongOrder = root $ (anno (Record [("a", Nat), ("b", (Fun Nat Nat))]) (rec2 ("b", (lam "x" zero)) ("a", zero)))
tFailUnequalNumberOfLabels = root $ (anno (Record [("a", Nat), ("b", (Fun Nat Nat))]) (rec3 ("a", zero) ("b", (lam "x" zero)) ("c", zero)))
tFailWrongSelection = root $ (sel "x" (anno (Record [("a", Nat), ("b", (Fun Nat Nat))]) (rec2 ("a", zero) ("b", (lam "x" zero)))))
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment