Commit b9983707 authored by André Pacak's avatar André Pacak
Browse files

record types contain maps and not lists, do not consider order of labeled terms

parent bfeedd2a
......@@ -7,6 +7,7 @@ category: Language
dependencies:
- base
- containers
- mtl
library:
......
module ExtendedTLC.Base where
import Prelude hiding ((>=), (<=), lookup)
import GHC.Exts (Constraint)
import Data.List(find)
import Data.Map (Map)
import qualified Data.Map as Map (lookup)
import ExtendedTLC.Language
import Util.ErrorMessages
import Util.PartialOrd
type Error = String
......@@ -50,7 +50,7 @@ matchType ty1 ty2 _
| ty1 == ty2 = return ()
matchType ty1 ty2 err = fail $ generalError (show ty1) ty2 err
matchRecord :: Type -> String -> Infer [(Name, Type)]
matchRecord :: Type -> String -> Infer (Map Name Type)
matchRecord (Record pairs) _ = return pairs
matchRecord ty err = fail $ recordError ty err
......@@ -58,9 +58,10 @@ matchSum :: Type -> String -> Infer (Type, Type)
matchSum (Sum ty1 ty2) _ = return (ty1, ty2)
matchSum ty err = fail $ sumError ty err
liftSnd :: Monad m => Maybe (a, b) -> String -> m b
liftSnd (Just (a, b)) _ = return b
liftSnd Nothing n = fail $ "Could not project " ++ n
liftMaybe :: Monad m => Maybe a -> String -> m a
liftMaybe (Just a) _ = return a
liftMaybe Nothing err = fail err
lookup :: Ctx -> Name -> Infer Type
lookup Empty x = fail $ "Unbound variable " ++ show x
......@@ -104,8 +105,7 @@ inferType ctx (Snd t _) = do
inferType ctx (Sel n t _) = do
ty <- inferType ctx t
typairs <- matchRecord ty (show t)
tyn <- liftSnd (find (\p -> fst p == n) typairs) n
return $ tyn
liftMaybe (Map.lookup n typairs) $ "Could not project" ++ (show n)
inferType _ t = fail $ "Cannot infer type of term " ++ show t
checkType :: Ctx -> Term -> Type -> Check
......@@ -118,12 +118,14 @@ checkType ctx p@(Pair t1 t2 _) ty = do
checkType ctx t2 ty2
checkType ctx p@(Rec tpairs _) ty = do
typairs <- matchRecord ty (show p)
if (length tpairs) == (length typairs)
if length tpairs == length typairs
then do
let zipped = zip tpairs typairs
let subresults = map (\((x, t), (x', tty)) -> if x == x' then checkType ctx t tty else fail "Labels of record term and record type do not match") zipped
foldl (\r e -> r >> e) (return ()) subresults
else do
let subresults = map (\(tl, t) -> do
lty <- liftMaybe (Map.lookup tl typairs) ""
checkType ctx t lty
) tpairs
foldl (>>) (return ()) subresults
else
fail "Length of term labels and type labels does not match"
checkType ctx p@(InL t _) ty = do
(ty1, ty2) <- matchSum ty (show p)
......
......@@ -7,6 +7,8 @@ module ExtendedTLC.ContinueAfterCheckFail where
import Prelude hiding (Monad(..), (>=), (<=), lookup)
import GHC.Exts (Constraint)
import Data.List(find)
import Data.Map (Map)
import qualified Data.Map as Map
import ExtendedTLC.Language
import Util.ErrorMessages
......@@ -46,8 +48,8 @@ instance (WithTop a, WithTop b) => WithTop (a, b) where
instance WithTop a => WithTop [a] where
top = [top]
instance WithTop Char where
top = '-'
instance WithTop a => WithTop (Map Name a) where
top = Map.empty
-- Had to define an own monad type class.
-- It is not possible otherwise to get the type constraint WithTop a.
......@@ -91,7 +93,7 @@ matchType :: Type -> Type -> String -> Check
matchType ty1 ty2 _ | ty1 >= ty2 = return ()
matchType ty1 ty2 err = fail [generalError (show ty1) ty2 err]
matchRecord :: Type -> String -> Infer [(Name, Type)]
matchRecord :: Type -> String -> Infer (Map Name Type)
matchRecord (Record pairs) _ = return pairs
matchRecord ty err = fail [recordError ty err]
......@@ -99,9 +101,9 @@ matchSum :: Type -> String -> Infer (Type, Type)
matchSum (Sum ty1 ty2) _ = return (ty1, ty2)
matchSum ty err = fail [sumError ty err]
liftSnd :: WithTop b => Maybe (a, b) -> String -> Infer b
liftSnd (Just (a, b)) _ = return b
liftSnd Nothing n = fail ["Could not project" ++ n]
liftMaybe :: WithTop a => Maybe a -> String -> Infer a
liftMaybe (Just a) _ = return a
liftMaybe Nothing err = fail [err]
lookup :: Ctx -> Name -> Infer Type
......@@ -145,8 +147,7 @@ inferType ctx (Snd t _) = do
inferType ctx (Sel n t _) = do
ty <- inferType ctx t
typairs <- matchRecord ty (show t)
tyn <- liftSnd (find (\p -> fst p == n) typairs) n
return $ tyn
liftMaybe (Map.lookup n typairs) $ "Could not project" ++ (show n)
inferType _ t = fail ["Cannot infer type of term " ++ show t]
checkType :: Ctx -> Term -> Type -> Check
......@@ -159,9 +160,15 @@ checkType ctx p@(Pair t1 t2 _) ty = do
checkType ctx t2 ty2
checkType ctx p@(Rec tpairs _) ty = do
typairs <- matchRecord ty (show p)
let zipped = zip tpairs typairs
let subresults = map (\((x, t), (x', tty)) -> if x == x' then checkType ctx t tty else fail ["Labels of record term and record type do not match"]) zipped
foldl (\r e -> r >> e) (return ()) subresults
if length tpairs == length typairs
then do
let subresults = map (\(tl, t) -> do
lty <- liftMaybe (Map.lookup tl typairs) ""
checkType ctx t lty
) tpairs
foldl (>>) (return ()) subresults
else
fail ["Length of term labels and type labels does not match"]
checkType ctx p@(InL t _) ty = do
(ty1, ty2) <- matchSum ty (show p)
checkType ctx t ty1
......
......@@ -7,6 +7,9 @@ module ExtendedTLC.EliminateContextArgument where
import Prelude hiding (Monad(..), (>=), (<=), lookup)
import GHC.Exts (Constraint)
import Data.List(find)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe (isJust, fromJust)
import ExtendedTLC.Language
import Util.ErrorMessages
......@@ -49,8 +52,8 @@ instance WithTop Ctx where
instance WithTop a => WithTop [a] where
top = [top]
instance WithTop Char where
top = '-'
instance WithTop a => WithTop (Map Name a) where
top = Map.empty
-- Had to define an own monad type class.
-- It is not possible otherwise to get the type constraint WithTop a.
......@@ -94,7 +97,7 @@ matchType :: Type -> Type -> String -> Check
matchType ty1 ty2 _ | ty1 >= ty2 = Inferred ()
matchType ty1 ty2 err = NotInferred [generalError (show ty1) ty2 err]
matchRecord :: Type -> String -> Infer [(Name, Type)]
matchRecord :: Type -> String -> Infer (Map Name Type)
matchRecord (Record pairs) _ = return pairs
matchRecord ty err = fail [recordError ty err]
......@@ -102,13 +105,9 @@ matchSum :: Type -> String -> Infer (Type, Type)
matchSum (Sum ty1 ty2) _ = return (ty1, ty2)
matchSum ty err = fail [sumError ty err]
liftSndFromMaybe :: WithTop b => Maybe (a, b) -> String -> Infer b
liftSndFromMaybe (Just (a, b)) _ = return b
liftSndFromMaybe Nothing n = fail ["Could not project" ++ n]
liftSnd :: WithTop b => Infer (a, b) -> String -> Infer b
liftSnd (Inferred (a, b)) _ = return b
liftSnd (NotInferred _) n = fail ["Could not project" ++ n]
liftMaybe :: WithTop a => Maybe a -> String -> Infer a
liftMaybe (Just a) _ = return a
liftMaybe Nothing err = fail [err]
-- try to inline lookup
......@@ -224,8 +223,7 @@ inferType (Snd t _) = do
inferType (Sel n t _) = do
ty <- inferType t
typairs <- matchRecord ty (show t)
tyn <- liftSndFromMaybe (find (\p -> fst p == n) typairs) n
return tyn
liftMaybe (Map.lookup n typairs) $ "Could not project" ++ (show n)
inferType t = fail ["Cannot infer type of term " ++ show t]
checkType :: Term -> Check
......@@ -241,13 +239,14 @@ checkType p@(Pair t1 t2 _) = do
checkType p@(Rec tpairs _) = do
ty <- requiredType p
typairs <- matchRecord ty (show p)
if (length tpairs) == (length typairs)
if length tpairs == length typairs
then do
let zipped = zip tpairs typairs
let subresults = map (\((x, t), (x', tty)) -> if x == x' then checkType t else fail ["Labels of record term and record type do not match"]) zipped
foldl (\r e -> r >> e) (return ()) subresults
else do
fail ["Length of term labels and type labels does not match"]
let subresults = map (\(tl, t) -> do
lty <- liftMaybe (Map.lookup tl typairs) ""
checkType t
) tpairs
foldl (>>) (return ()) subresults
else fail ["Length of term labels and type labels does not match"]
checkType p@(InL t _) = do
ty <- requiredType p
(ty1, ty2) <- matchSum ty (show p)
......@@ -257,8 +256,6 @@ checkType p@(InR t _) = do
(ty1, ty2) <- matchSum ty (show p)
checkType t
checkType p@(Case e n1 t1 n2 t2 _) = do
ety <- inferType e
(ty1, ty2) <- matchSum ety (show e)
ty <- requiredType p
checkType t1
checkType t2
......@@ -284,12 +281,6 @@ requiredType t = case parent t of
(ty1, ty2) <- matchFun ty (show t1)
return ty1
Just p@(Lam name term _) | t == term -> do
-- TODO deconstruction the context should be done up here but why is that?
-- TODO how can we detect that?
-- the idea is that we want to throw away the last binding because the outer invocation of checkType does not know
-- of this binding and a new binding is added for the inner checkType call. Thus the calculation of ty by
-- requiredType should not be passed the binding
-- because we have a context that has a additional binding
ty <- requiredType p
(ty1, ty2) <- matchFun ty (show p)
return ty2
......@@ -304,12 +295,15 @@ requiredType t = case parent t of
Just p@(Rec tpairs _) -> do
ty <- requiredType p
typairs <- matchRecord ty (show p)
if (length tpairs) == (length typairs)
if length tpairs == length typairs
then do
let zipped = zip tpairs typairs
liftSnd (liftSndFromMaybe (find (\((x, t'), (x', tty)) -> t == t' && x == x') zipped) "") ""
else do
fail ["Length of term labels and type labels does not match"]
-- TODO what happens if two labels have the same term?
-- TODO what happens if a label is used twice in a record?
let labeledterm = find (\(l, lt) -> lt == t) tpairs
if isJust labeledterm
then liftMaybe (Map.lookup (fst $ fromJust labeledterm) typairs) ""
else fail ["label associated with term not found"]
else fail ["Length of term labels and type labels does not match"]
Just p@(InL term _) | t == term -> do
ty <- requiredType p
(ty1, ty2) <- matchSum ty (show p)
......@@ -319,14 +313,11 @@ requiredType t = case parent t of
(ty1, ty2) <- matchSum ty (show p)
return ty2
Just p@(Case e n1 t1 n2 t2 _) | t == t1 -> do
-- TODO Does using deconstructed context for complete slice yield correct required?
ety <- inferType e
(ty1, ty2) <- matchSum ety (show e)
ty <- requiredType p
return ty
Just p@(Case e n1 t1 n2 t2 _) | t == t2 -> do
ety <- inferType e
(ty1, ty2) <- matchSum ety (show e)
ty <- requiredType p
return ty
_ -> fail ["Wrong arg passed"]
......@@ -7,6 +7,9 @@ module ExtendedTLC.EliminateTypeArgumentOfCheck where
import Prelude hiding (Monad(..), (>=), (<=), lookup)
import GHC.Exts (Constraint)
import Data.List(find)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe (isJust, fromJust)
import ExtendedTLC.Language
import Util.ErrorMessages
......@@ -46,8 +49,8 @@ instance (WithTop a, WithTop b) => WithTop (a, b) where
instance WithTop a => WithTop [a] where
top = [top]
instance WithTop Char where
top = '-'
instance WithTop a => WithTop (Map Name a) where
top = Map.empty
-- Had to define an own monad type class.
-- It is not possible otherwise to get the type constraint WithTop a.
......@@ -95,18 +98,13 @@ matchType :: Type -> Type -> String -> Check
matchType ty1 ty2 _ | ty1 >= ty2 = return ()
matchType ty1 ty2 err = fail [generalError (show ty1) ty2 err]
matchRecord :: Type -> String -> Infer [(Name, Type)]
matchRecord :: Type -> String -> Infer (Map Name Type)
matchRecord (Record pairs) _ = return pairs
matchRecord ty err = fail [recordError ty err]
liftSndFromMaybe :: WithTop b => Maybe (a, b) -> String -> Infer b
liftSndFromMaybe (Just (a, b)) _ = return b
liftSndFromMaybe Nothing n = fail ["Could not project" ++ n]
liftSnd :: WithTop b => Infer (a, b) -> String -> Infer b
liftSnd (Inferred (a, b)) _ = return b
liftSnd (NotInferred _) n = fail ["Could not project" ++ n]
liftMaybe :: WithTop a => Maybe a -> String -> Infer a
liftMaybe (Just a) _ = return a
liftMaybe Nothing err = fail [err]
lookup :: Ctx -> Name -> Infer Type
lookup Empty x = fail ["Unbound variable " ++ show x]
......@@ -149,8 +147,7 @@ inferType ctx (Snd t _) = do
inferType ctx (Sel n t _) = do
ty <- inferType ctx t
typairs <- matchRecord ty (show t)
tyn <- liftSndFromMaybe (find (\p -> fst p == n) typairs) n
return tyn
liftMaybe (Map.lookup n typairs) $ "Could not project" ++ (show n)
inferType _ t = fail ["Cannot infer type of term " ++ show t]
checkType :: Ctx -> Term -> Check
......@@ -164,20 +161,17 @@ checkType ctx p@(Pair t1 t2 _) = do
(ty1, ty2) <- matchProd ty (show p)
checkType ctx t1
checkType ctx t2
-- TODO with the match we enforce that the ty that was passed has the correct number of elements
-- Does zip fail when two lists with different lengths is passed?
-- Do we get this check for free in monadic style?
-- TODO: What happens if the record has no elements? Does it type check?
checkType ctx p@(Rec tpairs _) = do
ty <- requiredType ctx p
typairs <- matchRecord ty (show p)
if (length tpairs) == (length typairs)
if length tpairs == length typairs
then do
let zipped = zip tpairs typairs
let subresults = map (\((x, t), (x', tty)) -> if x == x' then checkType ctx t else fail ["Labels of record term and record type do not match"]) zipped
foldl (\r e -> r >> e) (return ()) subresults
else do
fail ["Length of term labels and type labels does not match"]
let subresults = map (\(tl, t) -> do
lty <- liftMaybe (Map.lookup tl typairs) ""
checkType ctx t
) tpairs
foldl (>>) (return ()) subresults
else fail ["Length of term labels and type labels does not match"]
-- checkType ctx p@(Rec [(x, t)] _) = do
-- ty <- requiredType ctx p
-- [(x', tty)] <- matchRecord ty (show p)
......@@ -266,12 +260,15 @@ requiredType ctx t = case parent t of
Just p@(Rec tpairs _) -> do
ty <- requiredType ctx p
typairs <- matchRecord ty (show p)
if (length tpairs) == (length typairs)
if length tpairs == length typairs
then do
let zipped = zip tpairs typairs
liftSnd (liftSndFromMaybe (find (\((x, t'), (x', tty)) -> t == t' && x == x') zipped) "") ""
else do
fail ["Length of term labels and type labels does not match"]
-- TODO what happens if two labels have the same term?
-- TODO what happens if a label is used twice in a record?
let labeledterm = find (\(l, lt) -> lt == t) tpairs
if isJust labeledterm
then liftMaybe (Map.lookup (fst $ fromJust labeledterm) typairs) ""
else fail ["label associated with term not found"]
else fail ["Length of term labels and type labels does not match"]
Just p@(InL term _) | t == term -> do
ty <- requiredType ctx p
(ty1, ty2) <- matchSum ty (show p)
......@@ -293,6 +290,7 @@ requiredType ctx t = case parent t of
(ty1, ty2) <- matchSum ety (show e)
ty <- requiredType ctx' p
return ty
_ -> fail ["Could not determine required type"]
-- checkType ctx p@(Case e n1 t1 n2 t2 _) = do
-- ety <- inferType ctx e
-- (ty1, ty2) <- matchSum ety (show e)
......
......@@ -2,6 +2,8 @@ module ExtendedTLC.ErrorList where
import Prelude hiding (lookup, Ord)
import Data.List(find)
import Data.Map (Map)
import qualified Data.Map as Map (lookup)
import ExtendedTLC.Language
import Util.ErrorMessages
......@@ -44,7 +46,7 @@ matchType :: Type -> Type -> String -> Check
matchType ty1 ty2 _ | ty1 == ty2 = return ()
matchType ty1 ty2 err = fail $ generalError (show ty1) ty2 err
matchRecord :: Type -> String -> Infer [(Name, Type)]
matchRecord :: Type -> String -> Infer (Map Name Type)
matchRecord (Record pairs) _ = return pairs
matchRecord ty err = fail $ recordError ty err
......@@ -52,10 +54,9 @@ matchSum :: Type -> String -> Infer (Type, Type)
matchSum (Sum ty1 ty2) _ = return (ty1, ty2)
matchSum ty err = fail $ sumError ty err
liftSnd :: Monad m => Maybe (a, b) -> String -> m b
liftSnd (Just (a, b)) _ = return b
liftSnd Nothing n = fail $ "Could not project " ++ n
liftMaybe :: Monad m => Maybe a -> String -> m a
liftMaybe (Just a) _ = return a
liftMaybe Nothing err = fail err
lookup :: Ctx -> Name -> Infer Type
lookup Empty x = fail $ "Unbound variable " ++ show x
......@@ -98,8 +99,7 @@ inferType ctx (Snd t _) = do
inferType ctx (Sel n t _) = do
ty <- inferType ctx t
typairs <- matchRecord ty (show t)
tyn <- liftSnd (find (\p -> fst p == n) typairs) n
return $ tyn
liftMaybe (Map.lookup n typairs) $ "Could not project" ++ (show n)
inferType _ t = fail $ "Cannot infer type of term " ++ show t
checkType :: Ctx -> Term -> Type -> Check
......@@ -112,12 +112,14 @@ checkType ctx p@(Pair t1 t2 _) ty = do
checkType ctx t2 ty2
checkType ctx p@(Rec tpairs _) ty = do
typairs <- matchRecord ty (show p)
if (length tpairs) == (length typairs)
if length tpairs == length typairs
then do
let zipped = zip tpairs typairs
let subresults = map (\((x, t), (x', tty)) -> if x == x' then checkType ctx t tty else fail "Labels of record term and record type do not match") zipped
foldl (\r e -> r >> e) (return ()) subresults
else do
let subresults = map (\(tl, t) -> do
lty <- liftMaybe (Map.lookup tl typairs) ""
checkType ctx t lty
) tpairs
foldl (>>) (return ()) subresults
else
fail "Length of term labels and type labels does not match"
checkType ctx p@(InL t _) ty = do
(ty1, ty2) <- matchSum ty (show p)
......
module ExtendedTLC.Language where
import Prelude hiding (Ord, (<=), (>=))
import Data.Map (Map)
import qualified Data.Map as Map
import Prelude hiding (Ord, (<=), (>=))
import Util.PartialOrd as PO
......@@ -143,15 +145,14 @@ instance Show Term where
showsPrec p (Sel n t _) = showString "Sel " . showsPrec (p + 1) t . showString "." . showString n
showsPrec p (Rec pairs _) = showString "pair"
data Type = Nat | Fun Type Type | Prod Type Type | Record [(Name, Type)] | Sum Type Type | AnyType
data Type = Nat | Fun Type Type | Prod Type Type | Record (Map Name Type) | Sum Type Type | SumI [Type] | AnyType
deriving (Show, Eq)
instance PO.PartialOrd Type where
_ <= AnyType = True
(Fun t1 t2) <= (Fun u1 u2) = t1 <= u1 && t2 <= u2
(Prod t1 t2) <= (Prod u1 u2) = t1 <= u1 && t2 <= u2
(Record pairs) <= (Record pairs') = all (\((x, ty), (x', ty')) -> if x == x' then ty <= ty' else False) zipped
where zipped = zip pairs pairs'
(Record pairs) <= (Record pairs') = all (\((x, ty), (x', ty')) -> if x == x' then ty <= ty' else False) zipped where zipped = zip (Map.toList pairs) (Map.toList pairs')
(Sum t1 t2) <= (Sum u1 u2) = t1 <= u1 && t2 <= u2
ty1 <= ty2 = ty1 == ty2
......
# This file was autogenerated by Stack.
# You should not edit this file by hand.
# For more information, please see the documentation at:
# https://docs.haskellstack.org/en/stable/lock_files
packages: []
snapshots:
- completed:
size: 498180
url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/13/21.yaml
sha256: eff2de19a6d4691ccbf6edc1fba858f1918683047dce0f09adede874bbd2a8f3
original: lts-13.21
......@@ -3,6 +3,8 @@ module ExtendedTLC.SharedSpecs where
import Prelude hiding (lookup,(*), (**))
import Test.Hspec
import Data.Map
import qualified Data.Map as Map
import ExtendedTLC.Base as B
import ExtendedTLC.TestCases
import ExtendedTLC.Language
......@@ -58,17 +60,19 @@ sharedSpec inferType = do
it "should infer case with shadowing variable name" $ do
let res = convert $ inferType tOkCaseLeftShadowBinding in res `shouldBe` B.Inferred Nat
it "should infer empty record" $ do
let res = convert $ inferType tOkRecEmpty in res `shouldBe` B.Inferred (Record [])
let res = convert $ inferType tOkRecEmpty in res `shouldBe` B.Inferred (Record empty)
it "should infer record with one" $ do
let res = convert $ inferType tOkRecSingle in res `shouldBe` B.Inferred (Record [("x", (Prod Nat Nat))])
let res = convert $ inferType tOkRecSingle in res `shouldBe` B.Inferred (Record $ fromList [("x", (Prod Nat Nat))])
it "should infer record with two entries" $ do
let res = convert $ inferType tOkRecSimple in res `shouldBe` B.Inferred (Record [("a", Nat), ("b", (Fun Nat Nat))])
let res = convert $ inferType tOkRecSimple in res `shouldBe` B.Inferred (Record $ fromList [("a", Nat), ("b", (Fun Nat Nat))])
it "should infer selection of records first element" $ do
let res = convert $ inferType $ tSelectionOf "a" in res `shouldBe` B.Inferred Nat
it "should infer selection of records second element" $ do
let res = convert $ inferType $ tSelectionOf "b" in res `shouldBe` B.Inferred (Fun Nat Nat)
it "should infer selection of records third element" $ do
let res = convert $ inferType $ tSelectionOf "c" in res `shouldBe` B.Inferred (Prod Nat (Fun Nat Nat))
it "should infer record where type has other order of labels" $ do
let res = convert $ inferType tOkRecOtherOrder in res `shouldBe`B.Inferred (Record $ fromList [ ("a", Nat), ("b", (Fun Nat 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
......@@ -96,8 +100,6 @@ sharedSpec inferType = do
let res = isInferred $ convert $ inferType tFailCaseRightShadowBinding in res `shouldBe` False
it "should fail while infering record with not matching label" $ 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
......
......@@ -2,6 +2,8 @@ module ExtendedTLC.TestCases where
import Prelude hiding (lookup,(*), (**), succ, fst, snd)
import Data.Map
import qualified Data.Map as Map
import ExtendedTLC.Language
tOkZero = root zero
......@@ -17,12 +19,12 @@ tOkAppLambdaAnno = root $ (app (anno (Fun Nat Nat) (lam "b" (add (var "b") 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 []) rec0)
tOkRecSingle = root $ (anno (Record [("x", (Prod Nat Nat))]) (rec1 ("x", (pair zero (succ $ succ zero)))))
tOkRecSimple = root $ (anno (Record [("a", Nat), ("b", (Fun Nat Nat))]) (rec2 ("a", succ $ succ $ succ zero) ("b", (lam "a" $ zero))))
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 [("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"))))))
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"))))))
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)))))
......@@ -45,8 +47,8 @@ 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"))))
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)))))
tFailRecSingleWrongName = root $ (anno (Record $ fromList [("a", Nat)]) (rec1 ("b", zero)))
tOkRecOtherOrder = root $ (anno (Record $ fromList [("a", Nat), ("b", (Fun Nat Nat))]) (rec2 ("b", (lam "x" zero)) ("a", 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)))))