TestCases.hs 3.44 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
module ProductTypes.TestCases where

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

import Data.Map
import qualified Data.Map as Map
import ProductTypes.Language

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)))
tOkProd = root $ (anno (Prod Nat (Prod Nat Nat)) (pair (succ $ succ zero) (pair zero (succ zero))))
tOkProjection1 = root $ fst' (anno (Prod Nat Nat) (pair (mult zero zero) (add (succ zero) zero)))
tOkProjection2 = root $ snd' (anno (Prod Nat (Prod Nat Nat)) (pair (succ $ succ zero) (pair zero (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)))
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 empty) rec0)
tOkRecSingle = root $ (anno (Record $ fromList [("x", (Prod Nat Nat))]) (rec1 ("x", (pair zero (succ $ succ zero)))))
tOkRecSimple = root $ (anno (Record $ fromList [("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 $ fromList [("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"))))))

29 30
tOkRecOtherOrder = root $ (anno (Record $ fromList [("a", Nat), ("b", (Fun Nat Nat))]) (rec2 ("b", (lam "x" zero)) ("a", zero)))

31 32 33 34 35 36 37 38 39 40 41 42 43 44
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)))
tFailProdInAdd = root $ (anno Nat (add (anno (Prod Nat Nat) (pair zero zero)) zero))
tFailLambdaInProd = root $ (anno Nat (snd' (anno (Prod Nat Nat) (pair (anno (Fun Nat Nat) (lam "a" (var "a"))) zero))))
tFailProjectionOnNat = root $ snd' $ succ $ succ zero
tFailLambdaNotAnnoInBindingLet = root $ (let' "e" (lam "n" (add (var "n") (succ zero))) (mult (app (var "e") zero) (succ zero)))

tFailLetInPairFst = root $ (anno (Prod (Fun Nat Nat) (Fun Nat Nat)) (pair (let' "e" zero $ succ $ succ $ var "e") (lam "a" $ succ $ var "a")))
tFailLetInPairSnd = root $ (anno (Prod Nat (Fun Nat Nat)) (pair (lam "n" $ var "n") (let' "e" zero $ succ $ succ $ var "e")))

tFailRecSingleWrongName = root $ (anno (Record $ fromList [("a", Nat)]) (rec1 ("b", zero)))
tFailRecIlltypedWithin = root $ (anno (Record $ fromList [("a", (Fun Nat Nat)), ("b", Nat)]) (rec2 ("b", lam "x" zero) ("a", add zero (pair zero zero))))
tFailUnequalNumberOfLabels = root $ (anno (Record $ fromList [("a", Nat), ("b", (Fun Nat Nat))]) (rec3 ("a", zero) ("b", (lam "x" zero)) ("c", zero)))
tFailWrongSelection = root $ (sel "x" (anno (Record $ fromList [("a", Nat), ("b", (Fun Nat Nat))]) (rec2 ("a", zero) ("b", (lam "x" zero)))))