module Language.TEval.TEvalNC where
data Typ = TInt | !Typ :> !Typ deriving (Show, Eq)
infixr 9 :>
data Term = V VarName
| L VarName Typ Term
| A Term Term
| I Int
| Term :+ Term
| IFZ Term Term Term
| Fix Term
deriving (Show, Eq)
infixl 9 `A`
type VarName = String
type TEnv = [(VarName, Typ)]
env0 :: TEnv
env0 = []
lkup :: TEnv -> VarName -> Typ
lkup env x = maybe err id $ lookup x env
where err = error $ "Unbound variable " ++ x
ext :: TEnv -> (VarName,Typ) -> TEnv
ext env xt = xt : env
teval :: TEnv -> Term -> Typ
teval env (V x) = lkup env x
teval env (L x t e) = t :> teval (ext env (x,t)) e
teval env (A e1 e2) =
let t1 = teval env e1
t2 = teval env e2
in case t1 of
t1a :> t1r | t1a == t2 -> t1r
t1a :> t1r -> error $ unwords ["Applying a function of arg type",
show t1a, "to argument of type",
show t2]
t1 -> error $ "Trying to apply a non-function: " ++ show t1
teval env (I n) = TInt
teval env (e1 :+ e2) =
let t1 = teval env e1
t2 = teval env e2
in case (t1,t2) of
(TInt, TInt) -> TInt
ts -> error $ "Trying to add non-integers: " ++ show ts
teval env (IFZ e1 e2 e3) =
let t1 = teval env e1
t2 = teval env e2
t3 = teval env e3
in case t1 of
TInt | t2 == t3 -> t2
TInt -> error $ unwords ["Branches of IFZ have different types:",
show t2, "and", show t3]
t -> error $ "Trying to compare a non-integer to 0: " ++ show t
teval env (Fix e) =
let t = teval env e
in case t of
((ta1 :> tb1) :> (ta2 :> tb2)) | ta1 == ta2 && tb1 == tb2
-> ta1 :> tb1
t -> error $ "Inappropriate type in Fix: " ++ show t
(vx,vy) = (V "x",V "y")
term1 = L "x" TInt (IFZ vx (I 1) (vx :+ (I 2)))
test1 = teval env0 term1
term2a = L "x" TInt (L "y" TInt (vx `A` vy))
test2a = teval env0 term2a
term2b = L "x" (TInt :> TInt) (L "y" TInt (vx `A` vy))
test2b = teval env0 term2b
term3 = L "x" TInt (IFZ vx (I 1) vy)
test3 = teval env0 term3
term4a = L "x" TInt (IFZ vx (I 1) (vx `A` (I 1)))
test4a = teval env0 term4a
term4b = L "x" (TInt :> TInt) (IFZ vx (I 1) (vx `A` (I 1)))
test4b = teval env0 term4b
term6 = (L "x" TInt (I 1)) `A` vy
test61 = teval env0 term6
tmul1 = L "x" TInt (L "y" TInt
(IFZ vx (I 0)
((tmul1 `A` (vx :+ (I (1))) `A` vy) :+ vy)))
testm1 = teval env0 tmul1
delta = L "y" (TInt :> TInt) (vy `A` vy)
testd = teval env0 delta
tmul = Fix (L "self" (TInt :> TInt :> TInt) (L "x" TInt (L "y" TInt
(IFZ vx (I 0)
(((V "self") `A` (vx :+ (I (1))) `A` vy) :+ vy)))))
testm21 = teval env0 tmul
testm22 = teval env0 (tmul `A` (I 2))
testm23 = teval env0 (tmul `A` (I 2) `A` (I 3))
testm24 = teval env0 (tmul `A` (I (1)) `A` (I (1)))