{-# 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