module Language.TEval.TInfLetP where
import Data.List (nub)
import qualified Data.IntMap as M
import Control.Monad.State.Strict
data Typ = TInt | !Typ :> !Typ | TV TVarName deriving (Show, Eq)
infixr 9 :>
type TVarName = Int
data TypS = TypS [TVarName] Typ
deriving Show
data Term = V VarName
| L VarName Term
| A Term Term
| I Int
| Term :+ Term
| IFZ Term Term Term
| Fix Term
| Let (VarName,Term) Term
deriving (Show, Eq)
infixl 9 `A`
type VarName = String
type TEnv = [(VarName, TypS)]
env0 :: TEnv
env0 = []
lkup :: TEnv -> VarName -> TypS
lkup env x = maybe err id $ lookup x env
where err = error $ "Unbound variable " ++ x
ext :: TEnv -> (VarName,TypS) -> TEnv
ext env xt = xt : env
data TVE = TVE Int (M.IntMap Typ) deriving Show
type TVEM = State TVE
newtv :: TVEM Typ
newtv = do
TVE n s <- get
put (TVE (succ n) s)
return (TV n)
tve0 :: TVE
tve0 = TVE 0 M.empty
tvlkup :: TVE -> TVarName -> Maybe Typ
tvlkup (TVE _ s) v = M.lookup v s
tvext :: TVE -> (TVarName,Typ) -> TVE
tvext (TVE c s) (tv,t) = TVE c $ M.insert tv t s
tvdomainp :: TVE -> TVarName -> Bool
tvdomainp (TVE _ s) v = M.member v s
tvfree :: TVE -> [TVarName]
tvfree (TVE c s) = filter (\v -> not (M.member v s)) [0..c1]
tvsub :: TVE -> Typ -> Typ
tvsub tve (t1 :> t2) = tvsub tve t1 :> tvsub tve t2
tvsub tve (TV v) | Just t <- tvlkup tve v = tvsub tve t
tvsub tve t = t
tvchase :: TVE -> Typ -> Typ
tvchase tve (TV v) | Just t <- tvlkup tve v = tvchase tve t
tvchase _ t = t
unify :: Typ -> Typ -> TVE -> Either String TVE
unify t1 t2 tve = unify' (tvchase tve t1) (tvchase tve t2) tve
unify' :: Typ -> Typ -> TVE -> Either String TVE
unify' TInt TInt = Right
unify' (t1a :> t1r) (t2a :> t2r) = either Left (unify t1r t2r) . unify t1a t2a
unify' (TV v1) t2 = unifyv v1 t2
unify' t1 (TV v2) = unifyv v2 t1
unify' t1 t2 = const (Left $ unwords ["constant mismatch:",show t1,"and",
show t2])
unifyv :: TVarName -> Typ -> TVE -> Either String TVE
unifyv v1 (TV v2) tve =
if v1 == v2 then Right tve
else Right (tvext tve (v1,TV v2))
unifyv v1 t2 tve = if occurs v1 t2 tve
then Left $ unwords ["occurs check:",show (TV v1),
"in",show $ tvsub tve t2]
else Right (tvext tve (v1,t2))
occurs :: TVarName -> Typ -> TVE -> Bool
occurs v TInt _ = False
occurs v (t1 :> t2) tve = occurs v t1 tve || occurs v t2 tve
occurs v (TV v2) tve =
case tvlkup tve v2 of
Nothing -> v == v2
Just t -> occurs v t tve
tvdependentset :: TVE -> TVE -> (TVarName -> Bool)
tvdependentset tve_before tve_after =
\tv -> any (\tvb -> occurs tv (TV tvb) tve_after) tvbs
where
tvbs = tvfree tve_before
unifyM :: Typ -> Typ -> (String -> String) -> TVEM ()
unifyM t1 t2 errf = do
tve <- get
case unify t1 t2 tve of
Right tve -> put tve
Left err -> fail (errf err)
instantiate :: TypS -> TVEM Typ
instantiate (TypS tvs t) = do
tve <- associate_with_freshvars tvs
return $ tvsub tve t
where
associate_with_freshvars [] = return tve0
associate_with_freshvars (tv:tvs) = do
tve <- associate_with_freshvars tvs
tvfresh <- newtv
return $ tvext tve (tv,tvfresh)
generalize :: TVEM Typ -> TVEM TypS
generalize ta = do
tve_before <- get
t <- ta
tve_after <- get
let t' = tvsub tve_after t
let tvdep = tvdependentset tve_before tve_after
let fv = filter (not . tvdep) (nub (freevars t'))
return $ TypS fv t'
freevars :: Typ -> [TVarName]
freevars TInt = []
freevars (t1 :> t2) = freevars t1 ++ freevars t2
freevars (TV v) = [v]
teval' :: TEnv -> Term -> TVEM Typ
teval' env (V x) = instantiate (lkup env x)
teval' env (L x e) = do
tv <- newtv
te <- teval' (ext env (x,TypS [] tv)) e
return $ tv :> te
teval' env (A e1 e2) = do
t1 <- teval' env e1
t2 <- teval' env e2
t1r <- newtv
unifyM t1 (t2 :> t1r) id
return t1r
teval' env (I n) = return TInt
teval' env (e1 :+ e2) = do
t1 <- teval' env e1
t2 <- teval' env e2
unifyM t1 TInt ("Trying to add non-integers: " ++)
unifyM t2 TInt ("Trying to add non-integers: " ++)
return TInt
teval' env (IFZ e1 e2 e3) = do
t1 <- teval' env e1
t2 <- teval' env e2
t3 <- teval' env e3
unifyM t1 TInt ("Trying to compare a non-integer to 0: " ++)
unifyM t2 t3 (\err -> unwords ["Branches of IFZ have different",
"types. Unification failed:",err])
return t2
teval' env (Fix e) = do
t <- teval' env e
ta <- newtv
tb <- newtv
unifyM t ((ta :> tb) :> (ta :> tb))
("Inappropriate type in Fix: " ++)
return $ ta :> tb
teval' env (Let (x,e) eb) = do
t <- generalize $ teval' env e
teval' (ext env (x,t)) eb
teval :: TEnv -> Term -> TypS
teval tenv e = let (ts,tve) = runState (generalize $ teval' tenv e) tve0 in ts
tevalng :: TEnv -> Term -> Typ
tevalng tenv e = let (t,tve) = runState (teval' tenv e) tve0 in tvsub tve t
(vx,vy) = (V "x",V "y")
test0 = runState (teval' env0 ((L "x" (vx :+ (I 2))) `A` (I 1))) tve0
term1 = L "x" (IFZ vx (I 1) (vx :+ (I 2)))
test10 = runState (teval' env0 term1) tve0
test1 = teval env0 term1
termid = L "x" vx
testid = teval env0 termid
term2a = L "x" (L "y" (vx `A` vy))
test2a = teval env0 term2a
term3 = L "x" (IFZ vx (I 1) vy)
test3 = teval env0 term3
term4 = L "x" (IFZ vx (I 1) (vx `A` (I 1)))
test4 = teval env0 term4
term6 = (L "x" (I 1)) `A` vy
test61 = teval env0 term6
test62 = teval env0 $ (I 1) :+ vx
tmul1 = L "x" (L "y"
(IFZ vx (I 0)
((tmul1 `A` (vx :+ (I (1))) `A` vy) :+ vy)))
testm1 = teval env0 tmul1
delta = L "y" (vy `A` vy)
testd = teval env0 delta
tmul = Fix (L "self" (L "x" (L "y"
(IFZ vx (I 0)
(((V "self") `A` (vx :+ (I (1))) `A` vy) :+ vy)))))
testm21' = runState (teval' env0 tmul) tve0
testm21 = teval env0 tmul
testm22 = teval env0 (tmul `A` (I 2))
testm23 = teval env0 (tmul `A` (I 2) `A` (I 3))
testl1 = teval env0 $ Let ("x",vx) vx
testl2 = teval env0 $ Let ("x",vy) (I 1)
testl3 = teval env0 $ Let ("x",(I 1)) (vx :+ vx)
testl40 = runState (teval' env0 (L "x" (Let ("x",vx `A` (I 1)) (vx :+ (I 2)))))
tve0
testl4 = teval env0 $ L "x" (Let ("x",vx `A` (I 1)) (vx :+ (I 2)))
testl42 = teval env0 $ (L "x" (Let ("x",vx `A` (I 1)) (vx :+ (I 2))))
`A` termid
testl43 = teval env0 $ (L "x" (Let ("x",vx `A` (I 1)) (vx :+ (I 2))))
`A` term2a
testl5 = teval env0 $ L "x" (Let ("y",vx `A` (I 1)) (L "x" (vy :+ vx)))
terml51 = L "x" (Let ("y",L"f" ((V "f") `A` vx)) vy)
testl51 = teval env0 terml51
terml52 = terml51 `A` (I 10)
testl52 = teval env0 terml52
testl61 = teval env0 $ L "x" (Let ("y",vx `A` (I 1))
(Let ("z",vy :+ (I 2)) vy))
testl62 = teval env0 $ L "x" (Let ("y",vx `A` (I 1))
(Let ("z",vy :+ (I 2)) vx))
testl63 = teval env0 $ L "x" (Let ("y",vx `A` (I 1))
(Let ("z",(I 2)) vx))
testl66 = teval env0 $ L "x" (Let ("y",vx)
(Let ("z",(vy `A` (I 1) :+ (I 2))) vy))
testl67 = teval env0 $ L "x" (Let ("y",vx) ((vy `A` (I 1)) :+
(vy `A` (L "x" vx))))
testl69 = teval env0 (L "f" $
Let ("g", L "x" $ Let ("y", A (V "f") (V "x"))
(V "x"))
(V "g"))
testl6a = teval env0 (L "f" $
Let ("g", L "x" $ Let ("y", A (V "f") (V "x"))
(V "x"))
(A (V "g") (V "g")))
testl71 = teval env0 $ Let ("x",term2a) vx
testl72 = teval env0 $ Let ("x",term2a) (Let ("y",vx `A` termid)
(Let ("z",vy `A` (I 2)) vx))
testl73 = teval env0 $ Let ("x",term2a) (Let ("y",vx `A` termid)
(Let ("z",vy `A` (I 2)) vy))
testl74 = teval env0 $ Let ("x",term2a)
(Let ("y",(Let ("z",vx `A` tmul) (vx `A` termid)))
vy)
testl75 = teval env0 $ Let ("x",term2a)
(Let ("y",(Let ("z",(vx `A` termid)) (V "z")))
vy)
testl76 = teval env0 $ Let ("x",(L "y" (I 10)))
(Let ("y",vx)
(Let ("z",(vy `A` (I 1) :+ (I 2))) vy))
testl77 = teval env0 $ Let ("x",(L "y" (I 10)))
(Let ("y",vx) ((vy `A` (I 1)) :+
(vy `A` (L "x" vx))))
term2id = Let ("id",L "x" vx) (
L "f" (L "y"
((I 2) :+
((V "id" `A` (V "f")) `A` ((V "id" `A` vy) :+ (I 1))))))
test2id = teval env0 term2id
termlet = Let ("c2", L "f" (L "x" (V "f" `A` (V "f" `A` vx)))) (
Let ("inc", L "x" (vx :+ (I 1))) (
Let ("compose", L "f" (L "g" (L "x" (V "f" `A` (V "g" `A` vx))))) (
Let ("id",L "x" vx) (
V "c2" `A` (V "compose" `A` V "inc" `A` V "inc") `A` (I 10) :+
(V "c2" `A` (V "compose" `A` V "inc") `A` V "id" `A` (I 100))
))))
testlet = teval env0 termlet