-- The Timber compiler -- -- Copyright 2008-2009 Johan Nordlander -- All rights reserved. -- -- Redistribution and use in source and binary forms, with or without -- modification, are permitted provided that the following conditions -- are met: -- -- 1. Redistributions of source code must retain the above copyright -- notice, this list of conditions and the following disclaimer. -- -- 2. Redistributions in binary form must reproduce the above copyright -- notice, this list of conditions and the following disclaimer in the -- documentation and/or other materials provided with the distribution. -- -- 3. Neither the names of the copyright holder and any identified -- contributors, nor the names of their affiliations, may be used to -- endorse or promote products derived from this software without -- specific prior written permission. -- -- THIS SOFTWARE IS PROVIDED BY THE CONTRIBUTORS ``AS IS'' AND ANY EXPRESS -- OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -- WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -- DISCLAIMED. IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE FOR -- ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -- DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS -- OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) -- HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, -- STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN -- ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE -- POSSIBILITY OF SUCH DAMAGE. module Kind where import PP import Common import Core import Env import Derive import Depend import Monad kindcheck m = kiModule m kiModule (_,ds',_,bs') (Module v ns xs ds ws bss) = do ds <- kiDeclsList env (groupTypes ds) (bss',xs1) <- derive (concatMap bvars bss ++ bvars bs') (ds' `catDecls` ds) xs let env' = addKEnv0 (ksigsOf ds) env bss <- mapM (kiBinds env') (bss++bss') return (Module v ns xs1 ds (ws++dom(concatMap tsigsOf bss')) bss) where env = addKEnv0 (ksigsOf ds') (initEnv v) -- Kind unification ------------------------------------------------------------ type KSubst = Map Int Kind type KEqs = [(Kind,Kind)] kunify :: KEqs -> M s KSubst kunify [] = return nullSubst kunify ((Star,Star):cs) = kunify cs kunify ((KVar n,k):cs) = kvarBind n k cs kunify ((k,KVar n):cs) = kvarBind n k cs kunify ((KFun k1 k2,KFun k1' k2'):cs) = kunify ((k1,k1'):(k2,k2'):cs) kunify ((k1,k2):eqs) = fail ("Kinds do not unify: " ++ render (pr k1 <+> text "and" <+> pr k2)) kvarBind n k cs | k == KVar n = kunify cs | n `elem` kvars k = fail "Infinite kind inferred" | otherwise = do s' <- kunify (subst s cs) return (s' @@ s) where s = n +-> k kindUnify cs = do s <- kunify cs return (freeVars s `zip` repeat Star @@ s) where freeVars s = nub (concat (map kvars (rng s))) kiRho env (R t) = kiType env t kiRho env (F scs t) = do css <- mapM (kiScheme env) scs cs <- kiRho env t return (concat css ++ cs) kiType env t = do (cs,k) <- kiTExp env t return ((k,Star) : cs) kiType' env t = do cs <- kiType env t s <- kunify cs return (subst s t) kiTExp env (TFun ts t) = do css <- mapM (kiType env) ts cs <- kiType env t return (cs ++ concat css, Star) kiTExp env (TId c) = return ([], findKind env c) kiTExp env (TVar n) = return ([], tvKind n) kiTExp env (TAp t t') = do (cs,k) <- kiTExp env t (cs',k') <- kiTExp env t' kv <- newKVar return ((k,KFun k' kv):cs++cs', kv) -- Handle type declarations ---------------------------------------------------- kiDeclsList env [] = return nullDecls kiDeclsList env (ds:dss) = do ds1 <- kiDecls env ds ds2 <- kiDeclsList (addKEnv0 (ksigsOf ds) env) dss return (catDecls ds1 ds2) kiDecls env t@(Types ke ds) = do css <- mapM (kiDecl (addKEnv0 ke env)) ds s <- kindUnify (concat css) `handle` \m -> errorTree m t return (Types (subst s ke) (subst s ds)) newTScope env vs = do ks <- mapM (const newKVar) vs return (addKEnv (vs `zip`ks) env) kiDecl env (i, DData vs bs ks) = do env' <- newTScope env vs cs <- kiType env' (tAp' i vs) css1 <- mapM (kiScheme env') bs css2 <- mapM (kiConstr env' . snd) ks return (cs ++ concat (css1 ++ css2)) kiDecl env (i, DRec _ vs bs ss) = do env' <- newTScope env vs cs <- kiType env' (tAp' i vs) css1 <- mapM (kiScheme env') bs css2 <- mapM (kiScheme env' . snd) ss return (cs ++ concat (css1 ++ css2)) kiDecl env (i, DType vs t) = do env' <- newTScope env vs (cs1,k1) <- kiTExp env' (tAp' i vs) (cs2,k2) <- kiTExp env' t return ((k1,k2) : cs1 ++ cs2) kiConstr env (Constr ts ps ke) = do css1 <- mapM (kiScheme env') ts css2 <- mapM (kiScheme env') ps return (concat (css1 ++ css2)) where env' = addKEnv ke env kiScheme env (Scheme t ps ke) = do cs <- kiRho env' t css <- mapM (kiScheme env') ps return (cs ++ concat css) where env' = addKEnv ke env kiTEnv env te = do css <- mapM (kiScheme env . snd) te s <- kindUnify (concat css) `handle` \m -> errorTree m te return (subst s te) kiMaybeScheme env Nothing = return [] kiMaybeScheme env (Just t) = kiScheme env t -- Handle bindings ------------------------------------------------------------- kiBinds env (Binds r te es) = do te <- kiTEnv env te es <- mapM (kiEqn env) es return (Binds r te es) -- Traverse expressions -------------------------------------------------------- kiExp env (ELam te e) = do te <- kiTEnv env te e <- kiExp env e return (ELam te e) kiExp env (EAp e es) = do e <- kiExp env e es <- mapM (kiExp env) es return (EAp e es) kiExp env (ELet bs e) = do bs <- kiBinds env bs e <- kiExp env e return (ELet bs e) kiExp env (ERec c es) = do es <- mapM (kiEqn env) es return (ERec c es) kiExp env (ECase e alts) = do e <- kiExp env e alts <- mapM (kiAlt env) alts return (ECase e alts) kiExp env (EAct e e') = do e <- kiExp env e e' <- kiExp env e' return (EAct e e') kiExp env (EReq e e') = do e <- kiExp env e e' <- kiExp env e' return (EReq e e') kiExp env (ETempl x t te c) = do t <- kiType' env t te <- kiTEnv env te c <- kiCmd env c return (ETempl x t te c) kiExp env (EDo x t c) = do t <- kiType' env t c <- kiCmd env c return (EDo x t c) kiExp env e = return e kiAlt env (p,e) = do e <- kiExp env e return (p,e) kiEqn env (v,e) = do e <- kiExp env e return (v,e) -- Traverse commands ----------------------------------------------------------- kiCmd env (CAss x e c) = do e <- kiExp env e c <- kiCmd env c return (CAss x e c) kiCmd env (CGen x t e c) = do cs <- kiType env t s <- kindUnify cs `handle` \m -> errorTree m t e <- kiExp env e c <- kiCmd env c return (CGen x (subst s t) e c) kiCmd env (CLet bs c) = do bs <- kiBinds env bs c <- kiCmd env c return (CLet bs c) kiCmd env (CRet e) = do e <- kiExp env e return (CRet e) kiCmd env (CExp e) = do e <- kiExp env e return (CExp e) -- Compute kind of general type expression ------------------------------------- kindOfType env (TFun _ _) = Star kindOfType env (TVar n) = tvKind n kindOfType env (TId c) = findKind env c kindOfType env (TAp t t') = k where KFun k' k = kindOfType env t