fregel-1.2.0: compiler/TypeChecker.hs
{-# Language TypeSynonymInstances,FlexibleInstances,MultiParamTypeClasses,FunctionalDependencies,RankNTypes,FlexibleContexts,KindSignatures,ScopedTypeVariables #-}
{-
Type-checking based on unification (2nd step)
Limitation:
- No type constraints (i.e., typeclasses)
So, (+) :: Num a => a -> a -> a is actually handled as (+) :: a -> a -> a .
Hmm... type of prev/curr is (forall b r . (forall a. Vertex a b -> r)),
and this needs higher rank types. The current implementation handles these
two specially in a dirty way.
-}
module TypeChecker where
import Spec
import Analysis (dependency')
import ASTData
import Control.Monad.State
import Control.Monad
import Data.Maybe
import Data.List
import Numeric (showHex)
import Debug.Trace
-------------------- unification ------------------------
{-
http://www.cs.cornell.edu/courses/cs3110/2011sp/lectures/lec26-type-inference/type-inference.htm
-}
{- invariant for substitutions: -}
{- no id on a lhs occurs in any term earlier in the list -}
type Substitution = [(Id, DTypeTerm)]
{- check if a variable occurs in a term -}
occurs :: Id -> DTypeTerm -> Bool
occurs x (DTypeVar y) = x == y
occurs x (DTypeTerm _ s) = any (occurs x) s
{- substitute term s for all occurrences of variable x in term t -}
subst :: (Id, DTypeTerm) -> DTypeTerm -> DTypeTerm
subst (x, s) (t@(DTypeVar y)) = if x == y then s else t
subst (x, s) (DTypeTerm f u) = DTypeTerm f (map (subst (x, s)) u)
{- apply a substitution right to left -}
apply :: Substitution -> DTypeTerm -> DTypeTerm
apply s t = foldr subst t s
{- unify one pair -}
unify_one :: DTypeTerm -> DTypeTerm -> Either String Substitution
unify_one s t =
case (s, t) of
(DTypeVar x, DTypeVar y) -> return (if x == y then [] else if x < y then [(y, s)] else [(x, t)]) -- this comparison of x and y is to ansure that a new (bigger) variable is replaced with an old (smaller) one
(DTypeTerm f sc, DTypeTerm g tc) ->
if f == g && length sc == length tc
then do res <- unify' (zip sc tc); return res
else Left ("not unifiable: head symbol conflict; " ++ show s ++" != " ++ show t )
(DTypeVar x, (DTypeTerm _ _)) ->
if occurs x t
then Left ("not unifiable: circularity; " ++ show s ++ " in " ++ show t)
else return [(x, t)]
((DTypeTerm _ _), DTypeVar x) ->
if occurs x s
then Left ("not unifiable: circularity; " ++ show t ++ " in " ++ show s)
else return [(x, s)]
{- unify a list of pairs -}
unify' :: [(DTypeTerm, DTypeTerm)] -> Either String Substitution
unify' [] = return []
unify' ((x, y) : t) =
do t2 <- unify' t
t1 <- unify_one (apply t2 x) (apply t2 y)
return (t1 ++ t2)
unify :: [(DTypeTerm, DTypeTerm)] -> Substitution
unify xs = case unify' xs of
Right s -> s
Left str -> error (str ++ "\nConstraints: \n" ++ (unlines $ map (\(a,b) -> prettyShow a++" == " ++ prettyShow b) xs))
unify'' :: [(DTypeTerm, DTypeTerm)] -> Either String Substitution
unify'' xs = case unify' xs of
Right s -> Right s
Left str -> Left (str ++ "\nConstraints: \n" ++ (unlines $ map (\(a,b) -> prettyShow a++" == " ++ prettyShow b) xs))
-------------------------- type checker --------------------
type TypeConstraint = (DTypeTerm, DTypeTerm)
type VarTypeBind' = (DVarName, (DTypeInfo, Bool))
type DEnvTC = (([VarTypeBind'], [Int], [String]), [TypeConstraint], DUnique)
class TypeCheckable a b | a -> b where
typeCheck :: a -> State DEnvTC b -- produces a new type name, assumulates type constraints, ...
setRefreshable :: VarTypeBind -> VarTypeBind'
setRefreshable (v, t) = (v, (t, True))
setUnRefreshable :: VarTypeBind -> VarTypeBind'
setUnRefreshable (v, t) = (v, (t, False))
isRefreshable :: VarTypeBind' -> Bool
isRefreshable (v, (t, b)) = b
-- access functions to the environment
addConstraint :: TypeConstraint -> State DEnvTC ()
addConstraint c =
do (env, cs, i) <- get
put (env, (c:cs), i)
getConstraints' :: DEnvTC -> [TypeConstraint]
getConstraints' (env, cs, i) = cs
getConstraints :: State DEnvTC [TypeConstraint]
getConstraints =
do (env, cs, i) <- get
put (env, [], i)
return cs
peepConstraints :: State DEnvTC [TypeConstraint]
peepConstraints =
do (env, cs, i) <- get
return cs
getNewTypeName :: DVarName -> State DEnvTC DTypeInfo
getNewTypeName os =
do (env, cs, i) <- get
let n = "t"++((showHex i ""))
put (env, cs, i+1)
return (DTypeVar n)
getVarTypeBinds :: State DEnvTC [VarTypeBind']
getVarTypeBinds =
do ((bds, ks, rs), cs, i) <- get
return bds
updateVarTypeBinds :: Substitution -> State DEnvTC ()
updateVarTypeBinds s =
do ((bds,ks,rs), cs, i) <- get
let bds' = map (\(x@(n,(t,b))) -> if not b then (n, (apply s t, b)) else x) bds
rs' = rigidTypeVars bds'
put ((bds',ks,rs'), cs, i)
addTypeBinds :: [VarTypeBind] -> State DEnvTC ()
addTypeBinds bd =
do ((bds, ks, rs), cs, i) <- get
let bds' = map setUnRefreshable bd++bds
rs' = rigidTypeVars bds'
put ((bds', length bd:ks, rs'), cs, i)
addTypeBindsRefreshable :: [VarTypeBind] -> State DEnvTC ()
addTypeBindsRefreshable bd =
do ((bds, ks, rs), cs, i) <- get
put (((map setRefreshable bd)++bds, length bd:ks, rs), cs, i)
popVarTypeBinds :: State DEnvTC [VarTypeBind]
popVarTypeBinds =
do x <- get
let ((bds, k:ks, rs), cs, i) = x
bds' = drop k bds
rs' = rigidTypeVars bds'
put ((bds', ks, rs'), cs, i)
return (map (\(n, (t, b)) -> (n, t)) (take k bds))
getRigidTypeVars :: State DEnvTC [String]
getRigidTypeVars =
do ((_, _, rs), _, _) <- get
return rs
rigidTypeVars :: [VarTypeBind'] -> [String]
rigidTypeVars = nub . sort . concatMap (\(n,(t,b)) -> if not b then collectTypeVars t else [])
lookupTypes :: [String] -> State DEnvTC [DTypeInfo]
lookupTypes ns =
do bds <- getVarTypeBinds
return (map (\n -> maybe (error ("not found: "++n)) (\(t, b) -> t) $ lookup n bds) ns)
-- adds variables with their fresh type names, returns the type names
addNames :: [DVarName] -> State DEnvTC ([DTypeInfo])
addNames ns =
do nts <- mapM getNewTypeName ns
let binds' = zip ns nts
addTypeBinds binds'
return nts
addNames' :: [DVarName] -> [DTypeInfo] -> State DEnvTC ()
addNames' ns nts =
do let binds' = zip ns nts
addTypeBinds binds'
--
initEnv' = (map setRefreshable initEnv, [], []{- everything is refreshable -})
typing0 :: (TypeCheckable a1 a, Show a) => a1 -> (a, DEnvTC)
typing0 p = runState (typeCheck p) (initEnv', [], 0)
typing'' p = let (p', env) = typing0 p
in (p', unify (getConstraints' env))
typing' p = let (p', env) = typing0 p
in (p', (getConstraints' env))
typing :: Show a => DProgramSpec a -> DProgramSpec (DTypeInfo, a)
typing p = let (p', env) = typing0 p in p'
doTyping' :: forall (t :: * -> *) b x.
(DAdditionalData2 (t (DTypeInfo, b)) (DTypeInfo, b) (DTypeInfo, b) (t (DTypeInfo, b)),
DAdditionalData (t (DTypeInfo, b)) (DTypeInfo, b),
Show x, PrettyShow x
)
=> [DTypeInfo] -> [t (DTypeInfo, b)] -> x -> State DEnvTC (([DTypeInfo], [t (DTypeInfo, b)] ), Substitution)
doTyping' ts es x =
do cs <- getConstraints
let s = unify'' cs
case s of
Right s -> do let ts' = map (apply s) ts
es' = map (mapData (\(t, a::b) -> (apply s t, a))) es
updateVarTypeBinds s
return ((ts', es'), s)
Left str -> do bds <- getVarTypeBinds
error (str ++ "\nin typing " ++ show x ++ "\n\nTerm: "++prettyShow x ++ "\nBindings: \n" ++ (unlines $ map (\(a,(t,b)) -> a ++ " :: " ++ prettyShow t ++ " , ("++show b++")") bds))
-- utility for getting type name
getType' :: forall (t :: * -> *) b . (DAdditionalData (t (DTypeInfo, b)) (DTypeInfo, b)) => (t (DTypeTerm, b)) -> DTypeTerm
getType' = fst . getData
setType :: forall (t :: * -> *) b . (DAdditionalData (t (DTypeInfo, b)) (DTypeInfo, b)) => DTypeTerm -> (t (DTypeTerm, b)) -> (t (DTypeTerm, b))
setType t p = setData (t, snd $ getData p) p
instance Show a => TypeCheckable (DProgramSpec a) (DProgramSpec (DTypeInfo, a)) where
typeCheck (DProgramSpec rs p a) =
do rs' <- {- trace (show rs) -} (mapM typeCheck rs) -- no mutual dependency among records.
p' <- typeCheck p
return (DProgramSpec rs' p' (getType' p', a))
instance Show a => TypeCheckable (DRecordSpec a) (DRecordSpec (DTypeInfo, a)) where
typeCheck (DRecordSpec c fts a) =
do dst <- mapM typeCheck (map snd fts)
let nc = head $ getNames c
tc = typeSolid nc
fts' = zipWith (\t f -> (mapData (\a -> (getType' t, a)) f, t)) dst (map fst fts)
c' = mapData (\a -> (tc, a)) c
-- add the constructor and fields to the env.
addTypeBindsRefreshable ((nc, typeFunction (map (getType'.fst) fts'++[tc])):map (\ft -> (head $ getNames $ fst ft, typeFunction [tc, getType' $ fst ft])) fts')
return (DRecordSpec c' fts' (tc, a))
{- this is for type annotations (in record definitions) -}
instance Show a => TypeCheckable (DType a) (DType (DTypeTerm, a)) where
typeCheck (DTInt a) = return (DTInt (typeDTInt, a))
typeCheck (DTBool a) = return (DTBool (typeDTBool, a))
typeCheck (DTString a) = return (DTString (typeDTString, a))
typeCheck (DTDouble a) = return (DTDouble (typeDTDouble, a))
typeCheck (DTTuple ts a) =
do ts' <- mapM typeCheck ts
let ds = map getType' ts'
return (DTTuple ts' (typeTuple ds, a))
typeCheck (DTRecord c ts a) =
do c' <- typeCheck c
ts' <- mapM typeCheck ts
let ds = map getType' ts'
return (DTRecord c' ts' (typeRecord (getName c') ds, a))
typingTypeExpression x = rec x
where
rec (DTInt a) = (typeDTInt)
rec (DTBool a) = (typeDTBool)
rec (DTString a) = (typeDTString)
rec (DTDouble a) = (typeDTDouble)
rec (DTTuple ts a) =
let ds = map rec ts
in (typeTuple ds)
rec (DTRecord c ts a) =
let ts' = map rec ts
in typeRecord (getName c) ts'
instance Show a => TypeCheckable (DConst a) (DConst (DTypeTerm, a)) where
typeCheck (DCInt c a) = return (DCInt c (typeDTInt, a))
typeCheck (DCBool c a) = return (DCBool c (typeDTBool, a))
typeCheck (DCString c a) = return (DCString c (typeDTString, a))
typeCheck (DCDouble c a) = return (DCDouble c (typeDTDouble, a))
getNamesWithType' (DGDefVC d a) = [(head $ getNames d, getType' d)]
getNamesWithType' (DGDefVI d a) = [(head $ getNames d, getType' d)]
getNamesWithType' (DGDefSmpl d a) = getNamesWithType d
getNamesWithType' (DGDefGV d a) = [(head $ getNames d, getType' d)]
getNamesWithType' (DGDefGF d a) = [(head $ getNames d, getType' d)]
getNamesWithType'' (DDefGraphVar v e (t,a)) = [(head $ getNames v, t)]
instance Show a => TypeCheckable (DProg a) (DProg (DTypeInfo, a)) where
typeCheck (x@(DProg f defs e a)) =
do tv <- getNewTypeName "" -- vertex type of g
te <- getNewTypeName "" -- edge type of g
let tg = typeGraph [tv, te]
addTypeBinds [("g", tg)] -- the input graph
-- now, typing the let bindings
defs' <- mapM (\def -> do def' <- typeCheck def; addTypeBindsRefreshable (getNamesWithType' def'); return def') defs
-- and the body
e' <- typeCheck e
tf <- getNewTypeName ""
xx <- lookupTypes ["g"]
let [tg'] = xx
addConstraint (tf, typeFunction ([tg', getType' e']))
xx <- doTyping' [tf] [e'] x
let (([tf'], [e'']), s) = xx
mapM (\x -> do popVarTypeBinds) defs
popVarTypeBinds -- of g
let f' = mapData (\a -> (tf', a)) f
defs'' = map (mapData (\(t, a::a) -> (apply s t, a))) defs'
return (DProg f' defs'' e'' (tf', a))
instance Show a => TypeCheckable (DGroundDef a) (DGroundDef (DTypeInfo, a)) where
typeCheck (DGDefVC d a) = do d' <- typeCheck d
return (DGDefVC d' (getType' d', a))
typeCheck (DGDefVI d a) = do d' <- typeCheck d
return (DGDefVI d' (getType' d', a))
typeCheck (DGDefSmpl d a) = do d' <- typeCheck d
return (DGDefSmpl d' (getType' d', a))
typeCheck (DGDefGV d a) = do d' <- typeCheck d
return (DGDefGV d' (getType' d', a))
typeCheck (DGDefGF d a) = do d' <- typeCheck d
return (DGDefGF d' (getType' d', a))
instance Show a => TypeCheckable (DDefVertComp a) (DDefVertComp (DTypeInfo, a)) where
typeCheck (x@(DDefVertComp f defs e a)) =
do tvv <- getNewTypeName "" -- vertex type of v
tve <- getNewTypeName "" -- edge type of v
tuv <- getNewTypeName "" -- vertex type of prev/curr
tres <- getNewTypeName "" -- resulting type of the function
let ttbl = typeFunction [typeVertex [tuv, tve], tres]
tv = typeVertex [tvv, tve]
addTypeBinds [("v", tv)]
addResultType tres
addTypeBindsRefreshable [("prev", ttbl), ("curr", ttbl)]
-- now, typing the let bindings and the body
-- assumption: no mutual dependency, topological sorted
defs' <- mapM (\def -> do def' <- typeCheck def; addTypeBindsRefreshable (getNamesWithType def'); return def') defs
e' <- typeCheck e
cs' <- peepConstraints
tf <- getNewTypeName ""
tres' <- getResultType
addConstraint (tres', getType' e')
xx <- lookupTypes ["v", "prev"] -- types of v etc have been updated possibly
let [tv', ttbl'] = xx
addConstraint (tf, typeFunction ([tv', ttbl', ttbl', getType' e']))
cs <- peepConstraints
xx <- doTyping' [tf] [e'] x
let (([tf'], [e'']), s) = xx
mapM (\x -> do popVarTypeBinds) defs
bds <- getVarTypeBinds
popVarTypeBinds -- of prev and curr
popVarTypeBinds -- of the result type
popVarTypeBinds -- of v
let f' = mapData (\a -> (tf', a)) f
defs'' = map (mapData (\(t, a::a) -> (apply s t, a))) defs'
--trace ("e''="++show e'' ++ "\ne'="++show e' ++ "\nbds ="++show bds ++ "\ncs ="++show cs ++ "\ntres' ="++show tres' ++ "\ntf' ="++show tf' ++ "\ntf ="++show tf ++ "\nttbl' ="++show ttbl') $
--trace ("\ntv'="++show tv'++ "\ntf' ="++show tf' ++ "\ntf ="++show tf ++ "\ncs ="++show cs++ "\ncs' ="++show cs'++ "\ne' ="++show e' ) $
return (DDefVertComp f' defs'' e'' (tf', a))
instance Show a => TypeCheckable (DDefVertInit a) (DDefVertInit (DTypeInfo, a)) where
typeCheck (x@(DDefVertInit f defs e a)) =
do tvv <- getNewTypeName "" -- vertex type of v
tve <- getNewTypeName "" -- edge type of v
let tv = typeVertex [tvv, tve]
addTypeBinds [("v", tv)]
-- now, typing the let bindings and the body
-- assumption: no mutual dependency, topological sorted
defs' <- mapM (\def -> do def' <- typeCheck def; addTypeBindsRefreshable (getNamesWithType def'); return def') defs
e' <- typeCheck e
tf <- getNewTypeName ""
xx <- lookupTypes ["v"] -- types of v etc have been updated possibly
let [tv'] = xx
addConstraint (tf, typeFunction ([tv', getType' e']))
xx <- doTyping' [tf] [e'] x
let (([tf'], [e'']), s) = xx
mapM (\x -> do popVarTypeBinds) defs
popVarTypeBinds -- of v
let f' = mapData (\a -> (tf', a)) f
defs'' = map (mapData (\(t, a::a) -> (apply s t, a))) defs'
return (DDefVertInit f' defs'' e'' (tf', a))
instance Show a => TypeCheckable (DDefGraphFun a) (DDefGraphFun (DTypeInfo, a)) where
typeCheck (x@(DDefGraphFun f v defs e a)) =
do tv <- getNewTypeName "" -- vertex type of g
te <- getNewTypeName "" -- edge type of g
let tg = typeGraph [tv, te]
nv = head $ getNames v
addTypeBinds [(nv, tg)] -- the input graph
-- now, typing the let bindings
defs' <- mapM (\def -> do def' <- typeCheck def; addTypeBindsRefreshable (getNamesWithType'' def'); return def') defs
-- and the body
e' <- typeCheck e
tf <- getNewTypeName ""
xx <- lookupTypes [nv] -- types of v etc have been updated possibly
let [tg'] = xx
addConstraint (tf, typeFunction ([tg', getType' e']))
xx <- doTyping' [tf, tg'] [e'] x
let (([tf', tg''], [e'']), s) = xx
mapM (\x -> do popVarTypeBinds) defs
popVarTypeBinds -- of v
let f' = mapData (\a -> (tf', a)) f
v' = mapData (\a -> (tg'', a)) v
defs'' = map (mapData (\(t, a::a) -> (apply s t, a))) defs'
return (DDefGraphFun f' v' defs'' e'' (tf', a))
instance Show a => TypeCheckable (DDefGraphVar a) (DDefGraphVar (DTypeInfo, a)) where
typeCheck (x@(DDefGraphVar v e a)) =
do tv <- getNewTypeName "" -- vertex type of g
te <- getNewTypeName "" -- edge type of g
let tg = typeGraph [tv, te]
nv = head $ getNames v
e' <- typeCheck e
addConstraint(tg, getType' e')
xx <- doTyping' [tg] [e'] x
let (([tg''], [e'']), s) = xx
v' = mapData (\a -> (tg'', a)) v
return (DDefGraphVar v' e'' (tg'', a))
getNamesWithType (DDefFun f vs defs e (tf, a)) = [(head $ getNames f, tf)]
getNamesWithType (DDefVar v defs e (tv, a)) = [(head $ getNames v, tv)]
getNamesWithType (DDefTuple vs defs e (tt, a)) = zip (map (head . getNames) vs) (getTupleTypes tt)
assume_just (Just a) = a
instance Show a => TypeCheckable (DSmplDef a) (DSmplDef (DTypeInfo, a)) where
typeCheck (x@(DDefFun f vs defs e a)) =
do let vns = concatMap getNames vs
nts <- mapM getNewTypeName vns
addNames' vns nts -- add the argument variables first, and get thier type names
-- assumption: no mutual dependency, topological sorted
defs' <- mapM (\def -> do def' <- typeCheck def; addTypeBindsRefreshable (getNamesWithType def'); return def') defs
e' <- typeCheck e
tf <- getNewTypeName ""
nts' <- mapM checkDefined vns
addConstraint (tf, typeFunction (nts'++[getType' e']))
xx <- doTyping' (tf:nts') [e'] x
let ((tf':nts'', [e'']),s) = xx
mapM (\x -> do popVarTypeBinds) defs
bds <- popVarTypeBinds
let f' = mapData (\a -> (tf', a)) f
vs' = map (\v -> mapData (\a -> (assume_just (lookup (getName v) (zip vns nts'')), a)) v) vs --map (\(v, vt) -> mapData (\a -> (vt, a)) v) (zip vs (map snd bds))
defs'' = map (mapData (\(t, a::a) -> (apply s t, a))) defs'
return (DDefFun f' vs' defs'' e'' (tf', a))
typeCheck (x@(DDefVar v defs e a)) =
do -- assumption: no mutual dependency, topological sorted
defs' <- mapM (\def -> do def' <- typeCheck def; addTypeBindsRefreshable (getNamesWithType def'); return def') defs
e' <- typeCheck e
tv <- getNewTypeName ""
addConstraint (tv, getType' e')
xx <- doTyping' [tv] [e'] x
let (([tv'], [e'']),s) = xx
mapM (\x -> do popVarTypeBinds) defs
let v' = mapData (\a -> (tv', a)) v
defs'' = map (mapData (\(t, a::a) -> (apply s t, a))) defs'
return (DDefVar v' defs'' e'' (tv', a))
typeCheck (x@(DDefTuple vs defs e a)) = -- buggy: type info. is not propagated to the tupled variables
do let vns = concatMap getNames vs
nts <- mapM getNewTypeName vns
addNames' vns nts -- add the argument variables first, and get thier type names
-- assumption: no mutual dependency, topological sorted
defs' <- mapM (\def -> do def' <- typeCheck def; addTypeBindsRefreshable (getNamesWithType def'); return def') defs
e' <- typeCheck e
nts' <- mapM checkDefined vns
tt <- getNewTypeName ""
addConstraint (typeTuple nts', getType' e')
xx <- doTyping' nts' [e'] x
let ((nts'', [e'']),s) = xx
mapM (\x -> do popVarTypeBinds) defs
bds <- popVarTypeBinds
let vs' = map (\v -> mapData (\a -> (assume_just (lookup (getName v) (zip vns nts'')), a)) v) vs --map (\(v, vt) -> mapData (\a -> (vt, a)) v) (zip vs (map snd bds))
defs'' = map (mapData (\(t, a::a) -> (apply s t, a))) defs'
return (DDefTuple vs' defs'' e'' (typeTuple nts'', a))
-- the type associated is the type of the target graph.
instance Show a => TypeCheckable (DTermination a) (DTermination (DTypeInfo, a)) where
typeCheck (x@(DTermF a)) =
do te <- getNewTypeName ""
tv <- getNewTypeName ""
return (DTermF ((typeGraph [tv, te]), a))
typeCheck (x@(DTermI e a)) =
do e' <- typeCheck e
addConstraint (getType' e', typeDTInt)
xx <- doTyping' [] [e'] x
let (([], [e'']), s) = xx
te <- getNewTypeName ""
tv <- getNewTypeName ""
return (DTermI e'' (typeGraph [tv, te], a))
typeCheck (x@(DTermU e a)) =
do te <- getNewTypeName ""
tv <- getNewTypeName ""
-- this type must be the same as the graph in the context (the result of giter or fregel)
-- this check will be done in the checking of giter or fregel
--- Hmm... no typechecking of g in the generator expression now (to remedy another problem)
--- agg [ exp | u <- gof v ] looks good for vertex functions, but not goot for Until.
let tg = typeGraph [tv, te]
addTypeBinds [("g", tg)]
addResultType tv
e' <- typeCheck e
addConstraint (getType' e', typeDTBool)
xx <- doTyping' [] [e'] x
let ((_, [e'']),s) = xx
popVarTypeBinds -- result
popVarTypeBinds -- g
let tg' = {- trace (show s) $ -} apply s tg
return ({- trace (show tg') -} (DTermU e'' (tg', a)))
instance Show a => TypeCheckable (DGraphExpr a) (DGraphExpr (DTypeInfo, a)) where
typeCheck (DPregel f0 ft x g a) =
do f0' <- typeCheck f0
ft' <- typeCheck ft
x' <- typeCheck x
g' <- typeCheck g
tself <- getNewTypeName ""
te <- getNewTypeName "" -- type of edges
tgv <- getNewTypeName "" -- type of vertices of the input
txv <- getNewTypeName "" -- type of vertices of something
trv <- getNewTypeName "" -- type of vertices of the result
addConstraint (getType' g', typeGraph [tgv, te]) -- g is a graph
addConstraint (getType' f0', typeFunction [typeVertex [tgv, te], trv]) -- initialization function
let ttbl = typeFunction [typeVertex [txv, te], trv] -- type of tables
addConstraint (getType' ft', typeFunction [typeVertex [tgv, te], ttbl, ttbl, trv]) -- vertex compute
addConstraint (tself, getType' x') -- the termination condition is on the result graph
addConstraint (tself, typeGraph [trv, te]) -- the result is a graph
return (DPregel f0' ft' x' g' (tself, a))
typeCheck (DGMap f g a) =
do f' <- typeCheck f
g' <- typeCheck g
tself <- getNewTypeName ""
te <- getNewTypeName "" -- type of edges
tgv <- getNewTypeName "" -- type of vertices of the input
trv <- getNewTypeName "" -- type of vertices of the result
addConstraint (getType' g', typeGraph[tgv, te]) -- g is a graph
addConstraint (tself, typeGraph[trv, te]) -- the result is a graph
addConstraint (getType' f', typeFunction [typeVertex [tgv, te], trv]) --the function type
return (DGMap f' g' (tself, a))
typeCheck (DGZip g1 g2 a) =
do g1' <- typeCheck g1
g2' <- typeCheck g2
tself <- getNewTypeName ""
te <- getNewTypeName "" -- type of edges
tv1 <- getNewTypeName "" -- type of vertices of g1
tv2 <- getNewTypeName "" -- type of vertices of g2
addConstraint (getType' g1', typeGraph[tv1, te]) -- g1 is a graph
addConstraint (getType' g2', typeGraph[tv2, te]) -- g2 is a graph
addConstraint (tself, typeGraph[typePair[tv1,tv2], te]) -- the result is a graph of pairs
return (DGZip g1' g2' (tself, a))
typeCheck (DGIter f0 ft x g a) =
do f0' <- typeCheck f0
ft' <- typeCheck ft
x' <- typeCheck x
g' <- typeCheck g
tself <- getNewTypeName ""
te <- getNewTypeName "" -- type of edges
tgv <- getNewTypeName "" -- type of vertices of the input
trv <- getNewTypeName "" -- type of vertices of the result
addConstraint (getType' g', typeGraph [tgv, te]) -- g is a graph
addConstraint (getType' f0', typeFunction [typeVertex [tgv, te], trv]) -- initialization function
addConstraint (getType' ft', typeFunction [typeGraph [trv, te], typeGraph [trv, te]]) -- graph function
addConstraint (tself, getType' x') -- the termination condition is on the result graph
addConstraint (tself, typeGraph [trv, te]) -- the result is a graph
return (DGIter f0' ft' x' g' (tself, a))
typeCheck (DGVar v a) =
do v' <- typeCheck v
return (DGVar v' (getType' v', a))
typeCheckApplication
:: forall (t :: * -> *) (u :: * -> *) b .
(DAdditionalData (t (DTypeInfo, b)) (DTypeInfo, b),
DAdditionalData (u (DTypeInfo, b)) (DTypeInfo, b),
TypeCheckable (t b) (t (DTypeInfo, b)),
TypeCheckable (u b) (u (DTypeInfo, b))) =>
t b
-> [u b]
-> State DEnvTC
((t (DTypeInfo, b)), [u (DTypeInfo, b)], DTypeInfo)
typeCheckApplication f es =
do f' <- typeCheck f
es' <- mapM typeCheck es
let tf = getType' f'
tes = map getType' es'
tself <- getNewTypeName "" -- type of this expression
addConstraint (tf, typeFunction (tes++[tself]))
return (f', es', tself)
instance Show a => TypeCheckable (DExpr a) (DExpr (DTypeInfo, a)) where
typeCheck (DIf p t e a) =
do p' <- typeCheck p
t' <- typeCheck t
e' <- typeCheck e
let tp = getType' p'
tt = getType' t'
te = getType' e'
tself <- getNewTypeName "" -- type of this expression
addConstraint (tp, typeDTBool) -- predicate must be of Bool
addConstraint (tt, te) -- then- and else-clauses must be the same
addConstraint (tself, tt) -- the type of this expression is also the same
return (DIf p' t' e' (tself, a))
typeCheck (DTuple es a) =
do es' <- mapM typeCheck es
tself <- getNewTypeName "" -- type of this expression
addConstraint (tself, typeTuple (map getType' es'))
return (DTuple es' (tself, a))
typeCheck (DFunAp f es a) =
do (f', es', tself) <- typeCheckApplication f es
return (DFunAp f' es' (tself, a))
typeCheck (DConsAp c es a) =
do (c', es', tself) <- typeCheckApplication c es
return (DConsAp c' es' (tself, a))
typeCheck (DFieldAcc t fs a) =
do t' <- typeCheck t
fs' <- mapM typeCheck fs
let tt = getType' t'
tfs = map getType' fs'
-- chain of filed accesses (function applications)
(tself, nts) <- foldM (\(t, nts) tf -> do nt <- getNewTypeName ""; addConstraint (tf, typeFunction [t, nt]); return (nt, nt:nts)) (tt, []) (tfs)
-- a type associated to a field is the type of the subexpression until the field
let fs'' = zipWith (\f nt -> let (_, a) = getData f in setData (nt, a) f) fs' (nts)
return (DFieldAcc t' fs'' (tself, a))
typeCheck (DFieldAccE e fs a) =
do e' <- typeCheck e
fs' <- mapM typeCheck fs
let te = getType' e'
tfs = map getType' fs'
-- chain of filed accesses (function applications)
(tself, nts) <- foldM (\(t, nts) tf -> do nt <- getNewTypeName ""; addConstraint (tf, typeFunction [t, nt]); return (nt, nt:nts)) (te, []) (tfs)
-- a type associated to a field is the type of the subexpression until the field
let fs'' = zipWith (\f nt -> let (_, a) = getData f in setData (nt, a) f) fs' (nts)
return (DFieldAccE e' fs'' (tself, a))
typeCheck (DAggr a' e g es a) =
do g' <- typeCheck g -- this adds new entries to the type env.
e' <- typeCheck e
a'' <- typeCheck a'
es' <- mapM typeCheck es
tself <- getNewTypeName ""
mapM (\x -> addConstraint (typeDTBool, getType' x)) es' -- a predicate must be a bool exp.
addConstraint (getType' a'', getType' e') -- the body and the aggregator are of the same type
addConstraint (getType' a'', tself)
popVarTypeBinds -- remove the entries
return (DAggr a'' e' g' es' (tself, a))
typeCheck (DVExp v a) =
do v' <- typeCheck v
return (DVExp v' (getType' v', a))
typeCheck (DCExp c a) =
do c' <- typeCheck c
return (DCExp c' (getType' c', a))
-- the type associated is the type of u
instance Show a => TypeCheckable (DGen a) (DGen (DTypeInfo, a)) where
typeCheck (DGenI a) =
do tv <- checkDefined "v"
xx <- addNames ["u", "e"]
let [tu, te] = xx
tuv <- getNewTypeName ""
tvv <- getNewTypeName ""
addConstraint (tu, tv) -- u and v has the same type
addConstraint (tu, typeVertex [tuv, te]) -- the type of u is Vertex .. ..
addConstraint (tv, typeVertex [tvv, te]) -- u and v have the same edge type
return (DGenI (typeTuple [tuv,te], a))
-- tres <- getResultType -- this is the resulting type of the function being defined
-- addConstraint (tuv, tres) -- the vertex type of u is the same as the resuting type of the function
-- addConstraint (tu, typeVertex [tuv, te]) -- the type of u is Vertex .. ..
-- addConstraint (tv, typeVertex [tvv, te]) -- u and v have the same edge type
-- return (DGenI (tres, a))
typeCheck (DGenO a) =
do tv <- checkDefined "v"
xx <- addNames ["u", "e"]
let [tu, te] = xx
tuv <- getNewTypeName ""
tvv <- getNewTypeName ""
addConstraint (tu, tv) -- u and v has the same type
addConstraint (tu, typeVertex [tuv, te]) -- the type of u is Vertex .. ..
addConstraint (tv, typeVertex [tvv, te]) -- u and v have the same edge type
return (DGenO (typeTuple [tuv, te], a))
-- tres <- getResultType -- this is the resulting type of the function being defined
-- addConstraint (tuv, tres) -- the vertex type of u is the same as the resuting type of the function
-- addConstraint (tu, typeVertex [tuv, te]) -- the type of u is Vertex .. ..
-- addConstraint (tv, typeVertex [tvv, te]) -- u and v have the same edge type
-- return (DGenO (tres, a))
typeCheck (DGenG a) =
do --tg <- checkDefined "g"
xx <- addNames ["u"]
let [tu] = xx
tuv <- getNewTypeName ""
--tgv <- getNewTypeName ""
te <- getNewTypeName ""
--addConstraint (tuv, tgv) -- u and v has the same type
addConstraint (tu, typeVertex [tuv, te]) -- the type of u is Vertex .. ..
--addConstraint (tg, typeGraph [tgv, te]) -- g is the graph of the same type
return (DGenG (tuv, a))
-- tres <- getResultType -- this is the resulting type of the function being defined
-- addConstraint (tuv, tres) -- the vertex type of u is the same as the resuting type of the function
-- addConstraint (tu, typeVertex [tuv, te]) -- the type of u is Vertex .. ..
-- addConstraint (tg, typeGraph [tgv, te]) -- g is the graph of the same type
-- return (DGenG (tres, a))
typeCheck (DGenTermG a) =
do --tg <- checkDefined "g"
xx <- addNames ["u"]
let [tu] = xx
tuv <- getNewTypeName ""
--tgv <- getNewTypeName ""
te <- getNewTypeName ""
--addConstraint (tuv, tgv) -- u and v has the same type
addConstraint (tu, typeVertex [tuv, te]) -- the type of u is Vertex .. ..
--addConstraint (tg, typeGraph [tgv, te]) -- g is the graph of the same type
return (DGenTermG (tuv, a))
-- tres <- getResultType -- this is the resulting type of the function being defined
-- addConstraint (tuv, tres) -- the vertex type of u is the same as the resuting type of the function
-- addConstraint (tu, typeVertex [tuv, te]) -- the type of u is Vertex .. ..
-- addConstraint (tg, typeGraph [tgv, te]) -- g is the graph of the same type
-- return (DGenTermG (tres, a))
-- the type associated is the type of elements of the argument list and the result
instance Show a => TypeCheckable (DAgg a) (DAgg (DTypeInfo, a)) where
typeCheck (DAggMin a) =
do t <- getNewTypeName ""
return (DAggMin (t, a)) -- forall a. [a] -> a (+ Ord a)
typeCheck (DAggMax a) =
do t <- getNewTypeName ""
return (DAggMax (t, a)) -- forall a. [a] -> a (+ Ord a)
typeCheck (DAggSum a) =
do t <- getNewTypeName ""
return (DAggSum (t, a)) -- forall a. [a] -> a (+ Num a)
typeCheck (DAggProd a) =
do t <- getNewTypeName ""
return (DAggProd (t, a)) -- forall a. [a] -> a (+ Num a)
typeCheck (DAggAnd a) =
do return (DAggAnd (typeDTBool, a)) -- [Bool] -> Bool
typeCheck (DAggOr a) =
do return (DAggOr (typeDTBool, a)) -- [Bool] -> Bool
typeCheck (DAggChoice x a) =
if isNotConstant x
then error "the default value of random aggregaor must be a constant."
else do x' <- typeCheck x
return (DAggChoice x' (getType' x', a)) -- let a be type of x, random x :: [a] -> a
typeCheck (DTupledAgg as a) =
do as' <- mapM typeCheck as
let ts = map getType' as'
t = typeTuple ts
return (DTupledAgg as' (t, a))
isNotConstant (DCExp _ _) = False
isNotConstant _ = True
instance Show a => TypeCheckable (DEdge a) (DEdge (DTypeInfo, a)) where
typeCheck (DEdge a) =
do d <- checkDefined "e"
return (DEdge (d, a))
instance Show a => TypeCheckable (DTableExpr a) (DTableExpr (DTypeInfo, a)) where
typeCheck (DPrev v a) =
do x <- typeCheckApplication (DFun "prev" a) [v]
let (_, [v'], tself) = x
return (DPrev v' (tself, a))
typeCheck (DCurr v a) =
do x <- typeCheckApplication (DFun "curr" a) [v]
let (_, [v'], tself) = x
return (DCurr v' (tself, a))
typeCheck (DVal v a) =
do x <- typeCheckApplication (DFun "val" a) [v]
let (_, [v'], tself) = x
return (DVal v' (tself, a))
-- the type of the function being defined
getResultType :: State DEnvTC DTypeInfo
getResultType =
do tres <- checkDefined resultTypeVarName
return tres
addResultType :: DTypeInfo -> State DEnvTC ()
addResultType t =
do addTypeBinds [(resultTypeVarName, t)]
-- dirty work around...
isTable n = n == "curr" || n == "prev"
tableRefresh (x@(DTypeTerm a [t1, t2])) =
do tv <- getNewTypeName ""
let (DTypeTerm _ [_, te]) = t1
y = (DTypeTerm a [typeVertex [tv,te], t2])
--trace ("table refresh: " ++ show x ++ " => " ++ show y) $
return y
checkDefined :: DVarName -> State DEnvTC DTypeInfo
checkDefined n =
do binds <- getVarTypeBinds
env <- get
case (lookup n binds) of
Just (d, r) -> if isTable n then tableRefresh d else (if r then do d' <- refresh d; rs <- getRigidTypeVars; (return d') else return d)
Nothing -> error ("\nUndefined in typechecking:: no " ++ n ++ " in " ++ show env)
-- do not use these typeChecks in field/fun/var/constructor definitions
instance Show a => TypeCheckable (DField a) (DField (DTypeInfo, a)) where
typeCheck (DField f a) =
do d <- checkDefined f
return (DField f (d, a))
-- typeCheck (DFfst a) =
-- do d <- checkDefined "_fst"
-- return (DFfst (d, a))
-- typeCheck (DFsnd a) =
-- do d <- checkDefined "_snd"
-- return (DFsnd (d, a))
removeSorted _ [] = []
removeSorted [] vs = vs
removeSorted (x@(r:rs)) (y@(v:vs)) =
if r == v then removeSorted rs vs
else if r < v then removeSorted rs y
else (v:removeSorted x vs)
refresh d =
do let vs = nub $ sort $ collectTypeVars d
rs <- getRigidTypeVars
let vs'' = removeSorted rs vs
vs' <- mapM getNewTypeName vs''
return (replaceVars (zip vs vs') d)
collectTypeVars :: DTypeTerm -> [String]
collectTypeVars (DTypeTerm x ts) = concatMap collectTypeVars ts
collectTypeVars (DTypeVar a) = [a]
replaceVars :: [(String, DTypeTerm)] -> DTypeTerm -> DTypeTerm
replaceVars tbl (DTypeTerm x ts) = DTypeTerm x (map (replaceVars tbl) ts)
replaceVars tbl (x@(DTypeVar a)) = case lookup a tbl of
(Just a') -> a'
Nothing -> x
instance Show a => TypeCheckable (DFun a) (DFun (DTypeInfo, a)) where
typeCheck (DFun f a) =
do d <- checkDefined f
return (DFun f (d, a))
typeCheck (DBinOp f a) =
do d <- checkDefined f
return (DBinOp f (d, a))
instance Show a => TypeCheckable (DVar a) (DVar (DTypeInfo, a)) where
typeCheck (DVar v a) =
do d <- checkDefined v
return (DVar v (d, a))
instance Show a => TypeCheckable (DConstructor a) (DConstructor (DTypeInfo, a)) where
typeCheck (DConstructor c a) =
do d <- checkDefined c
return (DConstructor c (d, a))
-- checking expression e has type t under the environment bs
-- returns a pair of the typed expression and substitution
typing2 :: Show a => [VarTypeBind] -> DExpr a -> DTypeInfo -> DUnique -> ((DExpr (DTypeInfo, a), Substitution), DUnique)
typing2 bs e t uid =
let (r, env') = runState (check e) env
env = ((map setRefreshable bs, [], []), [], uid)
check x =
do x' <- typeCheck x
xx <- doTyping' [] [x'] x
let ((_, [x'']),s) = xx
return (x'', s)
(_,_,uid') = env'
in (r, uid')
typing2' bs e t uid = let ((r,s), uid') = typing2 bs e t uid in ((mapData (\(t, _::a) -> DASTData t []) r, s), uid')
-- building an environment for typing the body of a program (whose input graph is "g")
-- vertex type tv and edge type te must be concrete types
buildProgEnv tv te bs = bs'
where bs' = [("g", typeGraph [tv, te])] ++ bs
-- building an environment for typing the body of a vertex-compute function, adding v, prev, curr and the result type
-- vertex type tvv and edge type tve must be concrete types
-- tuv is the type of vertices given to the tables
-- TDOO: add rigid type vars?
buildVertCompEnv tvv tve tuv tres bs = bs'
where
ttbl = typeFunction [typeVertex [tuv, tve], tres]
tv = typeVertex [tvv, tve]
bs' = [(resultTypeVarName, tres),("v", tv), ("prev", ttbl), ("curr", ttbl)]++bs