Commit 5a52fc1d authored by André Pacak's avatar André Pacak
Browse files

tests for case construct

parent 60e8d5d5
......@@ -110,8 +110,8 @@ let' n = cons2 (Let n)
sel n = cons1 (Sel n)
inl = cons1 InL
inr = cons1 InR
-- case' :: (Term -> Name -> Term -> Name -> Term -> Parent -> Term) -> TermBuild -> TermBuild -> TermBuild -> TermBuild
-- case' cons e n1 t1 n2 t2 parent = let res = cons (e (Just res)) n1 (t1 (Just res)) n2 (t2 (Just res)) parent in res
case' e n1 t1 n2 t2 parent = let res = Case (e (Just res)) n1 (t1 (Just res)) n2 (t2 (Just res)) parent in res
instance Show Term where
......
......@@ -47,12 +47,17 @@ sharedSpec inferType = do
let res = convert $ inferType tOkLetInPairFst in res `shouldBe` B.Inferred (Prod Nat (Fun Nat Nat))
it "should infer let binding in pair(snd)" $ do
let res = convert $ inferType tOkLetInPairSnd in res `shouldBe` B.Inferred (Prod (Fun Nat Nat) Nat)
-- it "should infer selection " $ do
-- let res = convert $ inferType tOkRecord in res `shouldBe` B.Inferred (Fun (Fun Nat Nat))
it "should infer left injection " $ do
let res = convert $ inferType tOkInL in res `shouldBe` B.Inferred (Sum Nat (Fun Nat Nat))
it "should infer right injection " $ do
let res = convert $ inferType tOkInR in res `shouldBe` B.Inferred (Sum Nat (Prod Nat (Fun Nat Nat)))
it "should infer case for left injection " $ do
let res = convert $ inferType tOkCaseLeft in res `shouldBe` B.Inferred Nat
it "should infer case for right injection " $ 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 fail while inferring an arithmetic expression with an unapplied lambda expression" $ do
let res = isInferred $ convert $ inferType tFailArithmetic in res `shouldBe` False
it "should fail while inferring an application of a lambda expression without type annotation" $ do
......@@ -73,3 +78,7 @@ sharedSpec inferType = do
let res = isInferred $ convert $ inferType tFailInL in res `shouldBe` False
it "should fail while infering right injection" $ do
let res = isInferred $ convert $ inferType tFailInR in res `shouldBe` False
it "should fail while matching on left injection where returntypes are unequal" $ 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
......@@ -20,6 +20,9 @@ tOkLetInPairSnd = root $ (anno (Prod (Fun Nat Nat) Nat) (pair (lam "n" (var "n")
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)))))
tOkCaseLeft = root $ (anno Nat (case' (anno (Sum Nat (Prod Nat Nat)) (inl $ succ zero)) "a" (var "a") "b" zero))
tOkCaseRight = root $ (anno Nat (case' (anno (Sum Nat (Fun Nat Nat)) (inr $ lam "x" $ add zero $ var "x")) "a" zero "b" (app (var "b") (succ $ succ zero))))
tOkCaseLeftShadowBinding = root $ (let' "a" zero (anno Nat (case' (anno (Sum (Fun Nat Nat) Nat) (inl $ lam "x" zero)) "a" (app (var "a") zero) "b" (var "a"))))
tFailArithmetic = root $ (add (succ $ succ zero) (mult (anno (Fun Nat Nat) (lam "f" (var "f"))) (succ $ succ $ succ $ succ zero)))
tFailLambdaNoAnno = root $ (anno Nat (app (lam "b" (add (var "b") zero)) (succ $ succ zero)))
......@@ -33,3 +36,5 @@ tFailLetInPairSnd = root $ (anno (Prod Nat (Fun Nat Nat)) (pair (lam "n" $ var "
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"))))
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