Commit 31d3a751 authored by André Pacak's avatar André Pacak
Browse files

additional test

parent 8ea9bad4
......@@ -98,6 +98,8 @@ sharedSpec inferType = 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 with illtyped term within" $ do
let res = isInferred $ convert $ inferType tFailRecIlltypedWithin 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
......
......@@ -47,5 +47,6 @@ tFailCaseRightShadowBinding = root $ (let' "a" zero (anno Nat (case' (anno (Sum
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)))
tFailRecIlltypedWithin = root $ (anno (Record [("a", (Fun Nat Nat)), ("b", Nat)]) (rec2 ("b", lam "x" zero) ("a", add zero (pair zero 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