Commit 74d41800 authored by André Pacak's avatar André Pacak

more test cases for fo recursive types

parent 9371bf48
......@@ -4,7 +4,6 @@ import Prelude hiding (lookup,(*), (**))
import Test.Hspec
import Data.Map
import qualified Data.Map as Map
import FORecursiveTypes.Base as B
import FORecursiveTypes.TestCases
import FORecursiveTypes.Language
......@@ -21,74 +20,83 @@ class ConvertInferredToStr a where
convertToStr :: a -> String
sharedSpec :: (ConvertToBInfer m) => (Term -> m Type) -> Spec
sharedSpec inferType = do
sharedSpec infer =
describe "inferType" $ do
it "should infer Zero to be of type Nat" $ do
let res = convert $ inferType tOkZero in res `shouldBe` B.Inferred Nat
let res = convert $ infer tOkZero in res `shouldBe` B.Inferred Nat
it "should infer (Succ Zero) to be of type Nat" $ do
let res = convert $ inferType tOkSucc in res `shouldBe` B.Inferred Nat
let res = convert $ infer tOkSucc in res `shouldBe` B.Inferred Nat
it "should infer arithmetic expression to be of type Nat" $ do
let res = convert $ inferType tOkArithmetic in res `shouldBe` B.Inferred Nat
let res = convert $ infer tOkArithmetic in res `shouldBe` B.Inferred Nat
it "should infer let binding with arithmetic expression to be of type Nat" $ do
let res = convert $ inferType tOkLetBindingWithArith in res `shouldBe` B.Inferred Nat
let res = convert $ infer tOkLetBindingWithArith in res `shouldBe` B.Inferred Nat
it "should infer nested lambda expressions" $ do
let res = convert $ inferType tOkAppLambdaAnno in res `shouldBe` B.Inferred Nat
let res = convert $ infer tOkAppLambdaAnno in res `shouldBe` B.Inferred Nat
it "should infer annotated lambda to be of type (Fun Nat Nat)" $ do
let res = convert $ inferType tOkLambdaAnno in res `shouldBe` B.Inferred (Fun Nat Nat)
let res = convert $ infer tOkLambdaAnno in res `shouldBe` B.Inferred (Fun Nat Nat)
it "should infer application of lambda expression" $ do
let res = convert $ inferType tOkAnno in res `shouldBe` B.Inferred (Fun (Fun Nat Nat) (Fun (Fun Nat Nat) (Fun Nat Nat)))
let res = convert $ infer tOkAnno in res `shouldBe` B.Inferred (Fun (Fun Nat Nat) (Fun (Fun Nat Nat) (Fun Nat Nat)))
it "should infer let binding with annotation in named expression" $ do
let res = convert $ inferType tOkAnnoInBindingLet in res `shouldBe` B.Inferred Nat
let res = convert $ infer tOkAnnoInBindingLet in res `shouldBe` B.Inferred Nat
it "should infer left injection " $ do
let res = convert $ inferType tOkInL in res `shouldBe` B.Inferred (Sum Nat (Fun Nat Nat))
let res = convert $ infer 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 (Fun Nat Nat))
let res = convert $ infer tOkInR in res `shouldBe` B.Inferred (Sum Nat (Fun Nat Nat))
it "should infer case for left injection " $ do
let res = convert $ inferType tOkCaseLeft in res `shouldBe` B.Inferred Nat
let res = convert $ infer 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
let res = convert $ infer 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
let res = convert $ infer tOkCaseLeftShadowBinding in res `shouldBe` B.Inferred Nat
it "should infer injection into variant with single element " $ do
let res = convert $ inferType tOkSingleVariant in res `shouldBe` B.Inferred (Variant $ fromList [("a", Nat)])
let res = convert $ infer tOkSingleVariant in res `shouldBe` B.Inferred (Variant $ fromList [("a", Nat)])
it "should infer match against variant with single element" $ do
let res = convert $ inferType tOkMatchSingle in res `shouldBe` B.Inferred Nat
let res = convert $ infer tOkMatchSingle in res `shouldBe` B.Inferred Nat
it "should infer match against variant with two elements" $ do
let res = convert $ inferType tOkMatchTwo in res `shouldBe` B.Inferred Nat
let res = convert $ infer tOkMatchTwo in res `shouldBe` B.Inferred Nat
it "should infer match against variant with two elements where order of cases is different from order of variant" $ do
let res = convert $ inferType tOkMatchWithDifferentOrder in res `shouldBe` B.Inferred Nat
let res = convert $ infer tOkMatchWithDifferentOrder in res `shouldBe` B.Inferred Nat
it "should infer match where case shadows outer binding"$ do
let res = convert $ inferType tOkMatchShadowBinding in res `shouldBe` B.Inferred Nat
let res = convert $ infer tOkMatchShadowBinding in res `shouldBe` B.Inferred Nat
it "should infer match where bindings are and terms are the same" $ do
let res = convert $ inferType tOkCasesSameBinding in res `shouldBe` B.Inferred (Fun Nat Nat)
let res = convert $ infer tOkCasesSameBinding in res `shouldBe` B.Inferred (Fun Nat Nat)
it "should infer recursive zero of recursive nat type" $ do
let res = convert $ inferType tOkZeroRecNatType in res `shouldBe` B.Inferred (TypeVar "Nat")
let res = convert $ infer tOkZeroRecNatType in res `shouldBe` B.Inferred (TypeVar "Nat")
it "should infer recursive nested succ of recursive nat type" $ do
let res = convert $ inferType tOkNestedSuccRecNatType in res `shouldBe` B.Inferred (TypeVar "Nat")
let res = convert $ infer tOkNestedSuccRecNatType in res `shouldBe` B.Inferred (TypeVar "Nat")
it "should infer function with recursive nat type as argument and return type" $ do
let res = convert $ infer tOkPredRecNatType in res `shouldBe` B.Inferred (Fun (TypeVar "Nat") (TypeVar "Nat"))
it "should infer function with recursive with nested rec types" $ do
let res = convert $ infer tOkRecTypeContainingRecType in res `shouldBe` B.Inferred (TypeVar "Bool")
it "should infer where same name is used for a type binding and a term bind" $ do
let res = convert $ infer tOkBindingWithSameNameForTypeAndTerm in res `shouldBe` B.Inferred (TypeVar "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
let res = isInferred $ convert $ infer tFailArithmetic in res `shouldBe` False
it "should fail while inferring an application of a lambda expression without type annotation" $ do
let res = isInferred $ convert $ inferType tFailLambdaNoAnno in res `shouldBe` False
let res = isInferred $ convert $ infer tFailLambdaNoAnno in res `shouldBe` False
it "should fail while trying to infer a let binding without annotation of lambda in named expression" $ do
let res = isInferred $ convert $ inferType tFailLambdaNotAnnoInBindingLet in res `shouldBe` False
let res = isInferred $ convert $ infer tFailLambdaNotAnnoInBindingLet in res `shouldBe` False
it "should fail while infering left injection" $ do
let res = isInferred $ convert $ inferType tFailInL in res `shouldBe` False
let res = isInferred $ convert $ infer tFailInL in res `shouldBe` False
it "should fail while infering right injection" $ do
let res = isInferred $ convert $ inferType tFailInR in res `shouldBe` False
let res = isInferred $ convert $ infer 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
let res = isInferred $ convert $ infer 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
let res = isInferred $ convert $ infer tFailCaseRightShadowBinding in res `shouldBe` False
it "should fail while tagging wrong type with label" $ do
let res = isInferred $ convert $ inferType tFailWrongTypeForTaggedLabel in res `shouldBe` False
let res = isInferred $ convert $ infer tFailWrongTypeForTaggedLabel in res `shouldBe` False
it "should fail while matching against non variant type" $ do
let res = isInferred $ convert $ inferType tFailMatchNotVariant in res `shouldBe` False
let res = isInferred $ convert $ infer tFailMatchNotVariant in res `shouldBe` False
it "should fail while tagging wrong label" $ do
let res = isInferred $ convert $ inferType tFailWrongLabel in res `shouldBe` False
let res = isInferred $ convert $ infer tFailWrongLabel in res `shouldBe` False
it "should fail while matching where return types of cases are not equal" $ do
let res = isInferred $ convert $ inferType tFailMatchUnequalTypesForCases in res `shouldBe` False
let res = isInferred $ convert $ infer tFailMatchUnequalTypesForCases in res `shouldBe` False
it "should fail while infering a undefined type" $ do
let res = isInferred $ convert $ inferType tFailRecTypeNotDefined in res `shouldBe` False
let res = isInferred $ convert $ infer tFailRecTypeNotDefined in res `shouldBe` False
it "should fail while passing a wrong type to a constructor of rec nat type " $ do
let res = isInferred $ convert $ infer tFailWrongTypePassedRecNatType in res `shouldBe` False
......@@ -31,6 +31,24 @@ tOkMatchWithDifferentOrder = root $ (anno Nat (match2 (anno (Variant (fromList [
tOkMatchShadowBinding = root $ (let' "x" zero (anno Nat (match2 (anno (Variant (fromList [("a", Nat), ("b", (Fun Nat Nat))])) (tag "b" (lam "x" (var "x")))) ("a", "x", succ $ var "x") ("b", "x", (app (var "x") zero)))))
tOkCasesSameBinding = root $ (anno (Fun Nat Nat) (match2 (anno (Variant (fromList [("a", Nat), ("b", Nat)])) (tag "b" zero)) ("a", "x", (lam "y" (mult (var "y") (var "x")))) ("b", "x", (lam "y" (mult (var "y") (var "x"))))))
tOkZeroRecNatType = root $ (type' "Nat" (Variant (fromList [("zero", UnitT), ("succ", TypeVar "Nat")])) (anno (TypeVar "Nat") (tag "zero" unit)))
tOkNestedSuccRecNatType = root $ (type' "Nat" (Variant (fromList [("zero", UnitT), ("succ", TypeVar "Nat")])) (anno (TypeVar "Nat") (tag "succ" (tag "succ" (tag "succ" (tag "zero" unit))))))
tOkPredRecNatType = root $ (type' "Nat" (Variant (fromList [("zero", UnitT), ("succ", TypeVar "Nat")])) (let'
"pred"
(anno (Fun (TypeVar "Nat") (TypeVar "Nat")) (lam "x" (match2 (var "x") ("zero", "a", (tag "zero" unit)) ("succ", "p", (var "p")))))
(var "pred")))
tOkRecTypeContainingRecType = root $
(type' "Bool" (Variant (fromList [("true", UnitT), ("false", UnitT)]))
(type' "Exp" (Variant (fromList [("natexp", Nat), ("boolexp", TypeVar "Bool")]))
(app
(anno
(Fun (TypeVar "Exp") (TypeVar "Bool"))
(lam "exp" (match2 (var "exp") ("boolexp", "a", (tag "true" unit)) ("natexp", "a", (tag "false" unit)))))
(tag "boolexp" (tag "true" unit)))))
tOkBindingWithSameNameForTypeAndTerm = root $ (type' "Nat" (Variant (fromList [("zero", UnitT), ("succ", TypeVar "Nat")])) (let' "Nat" (anno (TypeVar "Nat") (tag "zero" unit)) (var "Nat")))
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)))
......@@ -49,7 +67,8 @@ tFailMatchNotVariant = root $ (anno Nat (match1 (anno Nat zero) ("a", "x", succ
tFailMatchUnequalTypesForCases = root $ (anno Nat (match2 (anno (Variant (fromList [("a", Nat), ("b", (Fun Nat Nat))])) (tag "b" (lam "x" (var "x")))) ("a", "x", succ $ var "x") ("b", "x", (var "x") )))
tOkZeroRecNatType = root $ (type' "Nat" (Variant (fromList [("zero", UnitT), ("succ", TypeVar "Nat")])) (anno (TypeVar "Nat") (tag "zero" unit)))
tOkNestedSuccRecNatType = root $ (type' "Nat" (Variant (fromList [("zero", UnitT), ("succ", TypeVar "Nat")])) (anno (TypeVar "Nat") (tag "succ" (tag "succ" (tag "succ" (tag "zero" unit))))))
tFailRecTypeNotDefined = root $ (anno (TypeVar "Int") zero)
tFailWrongTypePassedRecNatType = root $ (type' "Nat" (Variant (fromList [("zero", UnitT), ("succ", TypeVar "Nat")])) (let'
"pred"
(anno (Fun (TypeVar "Nat") (TypeVar "Nat")) (lam "x" (match2 (var "x") ("zero", "a", (tag "zero" zero)) ("succ", "p", (var "p")))))
(var "pred")))
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