TestCases.hs 4.22 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55
{-# OPTIONS_GHC -Wno-orphans #-}
module FORecursiveTypes.TestCases where

import Prelude hiding (lookup,(*), (**), succ, fst, snd)

import FORecursiveTypes.Language
import Data.Map
import qualified Data.Map as Map

tOkZero = root zero
tOkSucc = root $ succ $ succ zero
tOkArithmetic = root $ (add (succ $ succ zero) (mult zero (succ $ succ $ succ $ succ zero)))
tOkLetBindingWithArith = root $ (let' "x" (add zero (succ zero)) (mult (var "x") (succ $ succ zero)))
tOkAnno = root $ (anno (Fun (Fun Nat Nat) (Fun (Fun Nat Nat) (Fun Nat Nat))) (lam "f" $ lam "g" $ lam "b" (app (var "g") (app (var "f") (var "b")))))
tOkLambdaAnno = root $ (anno (Fun Nat Nat) (lam "a" (add (var "a") zero)))
tOkAppLambdaAnno = root $ (app (anno (Fun Nat Nat) (lam "b" (add (var "b") zero))) (succ $ succ zero))
tOkAnnoInBindingLet = root $ (let' "e" (anno Nat (add zero (succ zero))) (mult (var "e") (succ zero)))

tOkInL = root $ (anno (Sum Nat (Fun Nat Nat)) (inl $ succ zero))
tOkInR = root $ (anno (Sum Nat (Fun Nat Nat)) (inr (anno (Fun Nat Nat) (lam "b" zero))))
tOkCaseLeft = root $ (anno Nat (case' (anno (Sum Nat Nat) (inl $ 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"))))

tOkSingleVariant = root $ (anno (Variant (fromList [("a", Nat)])) (tag "a" (succ zero)))
tOkTwoVariant = root $ (anno (Variant (fromList [("a", Nat), ("b", (Fun Nat Nat))])) (tag "b" (lam "x" zero)))
tOkThreeVariant = root $ (anno (Variant (fromList [("c", Nat), ("a", Nat), ("b", (Fun Nat Nat))])) (tag "b" (lam "x" zero)))
tOkMatchSingle = root $ (anno Nat (match1 (anno (Variant (fromList [("a", Nat)])) (tag "a" zero)) ("a", "x", succ $ var "x")))
tOkMatchTwo = 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", (app (var "x") zero))))
tOkMatchWithDifferentOrder = root $ (anno Nat (match2 (anno (Variant (fromList [("b", (Fun Nat Nat)), ("a", Nat)])) (tag "b" (lam "x" (var "x")))) ("a", "x", succ $ var "x") ("b", "x", (app (var "x") zero))))
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"))))))


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)))
tFailLambdaNotAnnoInBindingLet = root $ (let' "e" (lam "n" (add (var "n") (succ zero))) (mult (app (var "e") zero) (succ zero)))

tFailInL = root $ (anno (Sum Nat Nat) (inl (lam "b" zero)))
tFailInR = root $ (anno (Sum Nat Nat) (inr (lam "x" $ var "x")))
tFailCaseUnequalReturnTypes = root $ (anno (Fun Nat Nat) (case' (anno Nat (inl $ succ $ succ zero)) "a" (lam "x" (add (var "a") 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"))))


tFailWrongTypeForTaggedLabel = root $ (anno (Variant (fromList [("c", Nat), ("a", Nat), ("b", (Fun Nat Nat))])) (tag "b" zero))
tFailWrongLabel = root $ (anno (Variant (fromList [("c", Nat), ("a", Nat), ("b", (Fun Nat Nat))])) (tag "d" zero))

tFailMatchNotVariant = root $ (anno Nat (match1 (anno Nat zero) ("a", "x", succ $ var "x")))

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 $ (anno (TypeVar "Nat") (tag "zero" unit))
tOkNestedSuccRecNatType = root $ (anno (TypeVar "Nat") (tag "succ" (tag "succ" (tag "succ" (tag "zero" unit)))))

tFailRecTypeNotDefined = root $ (anno (TypeVar "Int") zero)