{-# OPTIONS_GHC -fglasgow-exts #-} -- -- Copyright (C) 2005 Stefan Wehr - http://www.stefanwehr.de -- -- This program is free software; you can redistribute it and/or -- modify it under the terms of the GNU General Public License as -- published by the Free Software Foundation; either version 2 of -- the License, or (at your option) any later version. -- -- This program is distributed in the hope that it will be useful, -- but WITHOUT ANY WARRANTY; without even the implied warranty of -- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU -- General Public License for more details. -- -- You should have received a copy of the GNU General Public License -- along with this program; if not, write to the Free Software -- Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA -- 02111-1307, USA. -- -- The code of this module is derived from Hatchet -- (http://www.cs.mu.oz.au/~bjpop/hatchet.html) module Phrac.KindInference where import qualified Control.Monad.State as StateMonad import qualified Data.Generics as Gen import qualified List import Maybe ( mapMaybe ) import qualified Phrac.Map as Map import qualified Phrac.PhracPrelude as PhracPrelude import qualified Phrac.DependAnalysis as DependAnalysis import qualified Phrac.UniqIdents as UniqIdents import Phrac.Builtins import Phrac.AbstractSyntax import Phrac.Error import Phrac.Pretty import Phrac.Symtab import Phrac.IdMap import Phrac.Substitution import Phrac.Kinds -------------------------------------------------------------------------------- type KVar = Int -- is converted to the "real" Kind after kind inference data Kind' = Kfun Kind' Kind' | KVar KVar | Star deriving (Eq,Show) kindFunAppSpec = (RightAssoc, 2) instance Pretty Kind' where pprPrec _ Star = text "*" pprPrec _ (KVar _) = text "?" pprPrec prec (Kfun k1 k2) = pprInfixOp prec kindFunAppSpec k1 (space <> text "->" <> space) k2 kindFun' :: [Kind'] -> Kind' -> Kind' kindFun' args result = foldr Kfun result args type KindEnv = IdMap Kind' Kind' Kind' Kind' [Kind'] Kind' type KindSubst = Subst KVar Kind' class Substitution KVar Kind' a => Kinds a where vars :: a -> [KVar] instance Substitution KVar Kind' Kind' where applySubst s Star = Star applySubst s (KVar kindvar) = case substLookup kindvar s of Just k -> k Nothing -> KVar kindvar applySubst s (kind1 `Kfun` kind2) = (applySubst s kind1) `Kfun` (applySubst s kind2) instance Kinds Kind' where vars Star = [] vars (KVar kindvar) = [kindvar] vars (kind1 `Kfun` kind2) = vars kind1 ++ vars kind2 instance Kinds a => Kinds [a] where vars = List.nub . concatMap vars --instance Substitution a b c => Substitution a b (d, c) where -- applySubst s (x, y) = (x, applySubst s y) --instance Kinds a => Kinds (b, a) where -- vars (x, y) = vars y -------------------------------------------------------------------------------- -- unification -- mgu :: Kind -> Kind -> Maybe Subst -- can return either a substitution or a string mgu :: Kind' -> Kind' -> Either KindSubst String mgu Star Star = Left nullSubst mgu (k1 `Kfun` k2) (k3 `Kfun` k4) = case mgu k1 k3 of Right errorMsg -> Right errorMsg Left s1 -> case mgu (applySubst s1 k2) (applySubst s1 k4) of Right errorMsg -> Right errorMsg Left s2 -> Left $ s2 `composeSubst` s1 mgu (KVar u) k = varBind u k mgu k (KVar u) = varBind u k mgu k1 k2 = Right ("attempt to unify these two kinds: " ++ showPpr k1 ++ ", " ++ showPpr k2) varBind :: KVar -> Kind' -> Either KindSubst String varBind u k | k == (KVar u) = Left nullSubst | u `elem` vars k = Right ("occurs check failed in kind inference: " ++ showPpr u ++ ", " ++ showPpr k) | otherwise = Left (u +-> k) -------------------------------------------------------------------------------- -- The kind inference monad type KI = StateMonad.StateT KIState ST data KIState = KIState { env :: KindEnv, -- the environment of kind assumptions subst :: KindSubst, -- the current substitution varnum :: Int -- to keep our supply fresh } initState = KIState { env = emptyIdMap, subst = nullSubst, varnum = 0 } liftST x = StateMonad.lift x -------------------------------------------------------------------------------- -- useful operations in the inference monad runKI :: KI a -> ST a runKI comp = StateMonad.evalStateT comp initState getSubst :: KI KindSubst getSubst = StateMonad.gets subst getVarNum :: KI Int getVarNum = StateMonad.gets varnum getEnv :: KI (KindEnv) getEnv = StateMonad.gets env modifyEnv :: (KindEnv -> KindEnv) -> KI () modifyEnv f = StateMonad.modify ( \s -> s { env = f (env s) }) getEnvVars :: KI [KVar] getEnvVars = do env <- getEnv let (a,b,c,d,e,f) = elemsIdMap env allKinds = a ++ b ++ c ++ d ++ concat e ++ f return (vars allKinds) -- returns the old varnum incVarNum :: KI Int incVarNum = do i <- getVarNum StateMonad.modify (\s -> s { varnum = i + 1 }) return i unify :: Kind' -> Kind' -> KI () unify k1 k2 = do s <- getSubst case mgu (applySubst s k1) (applySubst s k2) of Left newSubst -> extendSubst newSubst Right errorMsg -> do env <- getEnv debug ("kind inference about to fail, dumping environment:\n" ++ show (dumpIdMap env)) phasefail errorMsg unifyList :: [Kind'] -> [Kind'] -> KI () unifyList ks1 ks2 = mapM_ (uncurry unify) (zip ks1 ks2) extendSubst :: KindSubst -> KI () extendSubst subst = do oldSubst <- getSubst StateMonad.modify (\s -> s { subst = subst `composeSubst` oldSubst}) newKindVar :: KI Kind' newKindVar = do n <- incVarNum return (KVar n) newKindVars :: Int -> KI [Kind'] newKindVars n = mapM (\_ -> newKindVar) [1..n] applySubstToEnv :: KindSubst -> KI () applySubstToEnv subst = let a = applySubst subst in modifyEnv $ mapIdMap (a, a, a, a, map a, a) -- clobber all remaining variables to stars envVarsToStars :: KI () envVarsToStars = do vars <- getEnvVars let varsToStarSubst = substFromAssocs $ map (\v -> (v, Star)) vars applySubstToEnv varsToStarSubst -------------------------------------------------------------------------------- -- dependency analysis type DepGroup = [DepGroupElem] data DepGroupElem = DepGroupTypeDef TypeDef | DepGroupClassDec ClassDec deriving (Eq) instance Show DepGroupElem where show (DepGroupTypeDef td) = show (tydef_name td) show (DepGroupClassDec cd) = show (class_name cd) data DepGroupName = DepGroupTypeId TypeId | DepGroupClassId ClassId deriving (Eq,Ord,Show) nameOfElem (DepGroupClassDec clazz) = DepGroupClassId (class_name clazz) nameOfElem (DepGroupTypeDef tydef) = DepGroupTypeId (tydef_name tydef) isClassDec (DepGroupClassDec _) = True isClassDec _ = False isTypeDef (DepGroupTypeDef _) = True isTypeDef _ = False listQuery f x = Gen.everything (++) ([] `Gen.mkQ` f) x assocIdToDepGroupName :: AssocTypeId -> ST DepGroupName assocIdToDepGroupName id = do clazz <- findClassOfAssocType id return (DepGroupClassId $ class_name clazz) dependencies :: DepGroupElem -> ST [DepGroupName] dependencies (DepGroupTypeDef tydef) = -- the dependencies of a data declaration are the type constructors -- and the classes of the associated type synonyms used on the rhs let usedTypeDefs = listQuery collectTycons tydef usedAssocTysyns = listQuery collectAssocs tydef tydefNames = map DepGroupTypeId usedTypeDefs in do assocNames <- mapM assocIdToDepGroupName usedAssocTysyns return (tydefNames ++ assocNames) where collectTycons (TyConstruct id) = [id] collectTycons _ = [] collectAssocs (AssocType name _) = [name] dependencies (DepGroupClassDec cd) = -- the dependencies of a class declaration are the classes and type -- constructors and the classes of the associated type synonyms used -- inside the class let usedClasses = listQuery collectClasses cd usedTypeDefs = listQuery collectTyIds cd usedAssocTysyns = listQuery collectAssocs cd classNames = map DepGroupClassId usedClasses tydefNames = map DepGroupTypeId usedTypeDefs in do assocNames <- mapM assocIdToDepGroupName usedAssocTysyns return (tydefNames ++ assocNames ++ classNames) where collectClasses (ClassConstraint id _) = [id] collectTyIds :: TypeId -> [TypeId] collectTyIds x = [x] collectAssocs (AssocType name _) = [name] getDepGroups :: Program -> ST [DepGroup] getDepGroups (Program typeDefs classDecs _ _) = let elems = map DepGroupTypeDef typeDefs ++ map DepGroupClassDec classDecs in do deps <- mapM dependencies elems let depEnv = zip elems deps groups = DependAnalysis.getBindGroups elems nameOfElem (depsOfElem depEnv) return groups where depsOfElem env elem = case List.lookup elem env of Just l -> l -- list is empty for elements without dependencies Nothing -> panic ("no dependencies for elem " ++ show elem) -------------------------------------------------------------------------------- -- this is what gets called from outside of this module kindInference :: Program -> ST () kindInference prg@(Program typeDefs classDecs classInsts valBinds) = do groups <- getDepGroups prg runKI $ do mapM kiGroup groups mapM kiInst classInsts kiAllBinds valBinds currentSubst <- getSubst applySubstToEnv currentSubst envVarsToStars correctKinds prg correctKinds :: Program -> KI () correctKinds p = do Gen.everywhereM (Gen.mkM correct) p return () where correct :: TypeVarId -> KI TypeVarId correct id = do env <- getEnv case lookupTypeVar id env of Nothing -> panic ("correcting program but no kind found for " ++ "type variable " ++ showPpr id) Just (KVar _) -> panic ("correcting program but kind for " ++ showPpr id ++ " is still a kind variable") Just k -> do liftST $ insertKind id (translate k) return id translate Star = KindStar translate (Kfun k1 k2) = KindFun (translate k1) (translate k2) kiGroup :: DepGroup -> KI () kiGroup group = let classes = map (\ (DepGroupClassDec cd) -> cd) $ filter isClassDec group tydefs = map (\ (DepGroupTypeDef td) -> td) $ filter isTypeDef group in do mapM kiClassHead classes mapM kiTypeDefLhs tydefs mapM kiTypeDefRhs tydefs mapM kiTSigs (map class_tsigs classes) mapM kiClassConstraints (map class_constraints classes) mapM kiVSigs (map class_vsigs classes) currentSubst <- getSubst applySubstToEnv currentSubst envVarsToStars kiClassHead :: ClassDec -> KI () kiClassHead (ClassDec name args constrs tsigs vsigs _) = do varKinds <- newKindVars (length args) modifyEnv (\env -> insertClass name varKinds (insertTypeVars (zip args varKinds) env)) kiTypeDefLhs :: TypeDef -> KI () kiTypeDefLhs (TypeDef name args alts _) = do argKinds <- newKindVars (length args) let typeDefKind = kindFun' argKinds Star modifyEnv (\env -> insertType name typeDefKind (insertTypeVars (zip args argKinds) env)) -- kiClassConstraints and kiClassConstraint work only for constraints on -- type variables, i.e. constraints which are usually found in the -- context of a class declaration. kiClassConstraints = mapM kiClassConstraint kiClassConstraint :: ClassConstraint -> KI () kiClassConstraint (ClassConstraint className argTypes) = do env <- getEnv classKinds <- lookupClass className env argKinds <- mapM kiType argTypes unifyList classKinds argKinds kiTypeDefRhs :: TypeDef -> KI () kiTypeDefRhs tydef = let types = concatMap dconstr_params (tydef_alts tydef) in do kinds <- mapM kiType types mapM (\k -> unify k Star) kinds return () kiTSigs = mapM kiTSig kiTSig :: AssocTypeSig -> KI () kiTSig (AssocTypeSig id [] _) = panic ("invalid associated type synonym declaration " ++ showPpr' id) kiTSig (AssocTypeSig id params def) = do env <- getEnv n <- liftST $ getAssocIndexCount id let indices = take n params rest = drop n params indexKinds <- mapM (flip lookupTypeVar $ env) indices resultKind <- newKindVar restKinds <- case def of Nothing -> return $ take (length rest) (repeat Star) Just t -> do argKinds <- newKindVars (length rest) modifyEnv (insertTypeVars (zip rest argKinds)) k <- kiType t unify resultKind k return argKinds let assocTypeKind = kindFun' (indexKinds ++ restKinds) resultKind modifyEnv (\env -> insertAssocType id assocTypeKind (insertTypeVars (zip rest restKinds) env)) kiVSigs = mapM kiVSig kiVSig :: VSig -> KI () kiVSig (mid, tyScheme) = kiTypeScheme tyScheme kiInst :: ClassInst -> KI () kiInst ci = do let vars = freeTypeVarsList (inst_types ci) kinds <- newKindVars (length vars) modifyEnv (insertTypeVars (zip vars kinds)) argKinds <- mapM kiType (inst_types ci) env <- getEnv classArgKinds <- lookupClass (inst_class ci) env unifyList classArgKinds argKinds mapM kiConstraint (inst_constraints ci) mapM kiAssocTypeBind (inst_typeBinds ci) kiAllBinds (inst_valBinds ci) return () kiConstraint :: Constraint -> KI () kiConstraint (CC cc) = kiClassConstraint cc kiConstraint (EC ec) = do kiType (TyAssoc (eqc_left ec)) kiType (eqc_right ec) return () kiAssocTypeBind :: AssocTypeBind -> KI () kiAssocTypeBind atb = do env <- getEnv atKind <- lookupAssocType (assocBind_name atb) env indexKinds <- mapM kiType (assocBind_indices atb) let params = assocBind_params atb paramKinds <- newKindVars (length params) modifyEnv (insertTypeVars (zip params paramKinds)) resKind <- kiType (assocBind_def atb) unify atKind (kindFun' (indexKinds ++ paramKinds) resKind) kiTypeScheme :: TypeScheme -> KI () kiTypeScheme (TypeScheme quants qtype) = do quantKinds <- newKindVars (length quants) modifyEnv (insertTypeVars (zip quants quantKinds)) k <- kiQualifiedType qtype unify k Star return () kiQualifiedType :: QualifiedType -> KI Kind' kiQualifiedType (QualifiedType cs ty) = do mapM kiConstraint cs kiType ty kiType :: Type -> KI Kind' kiType (TyVar id) = do env <- getEnv lookupTypeVar id env kiType (TyApp t1 t2) = do k1 <- kiType t1 k2 <- kiType t2 resultKind <- newKindVar unify k1 (k2 `Kfun` resultKind) return resultKind kiType (TyConstruct id) = do env <- getEnv lookupType id env kiType (TyAssoc at) = do paramKinds <- mapM kiType (assoc_params at) env <- getEnv k <- lookupAssocType (assoc_name at) env resultKind <- newKindVar unify k (kindFun' paramKinds resultKind) return resultKind kiAllBinds :: Gen.Data a => a -> KI () kiAllBinds x = do Gen.everywhereM (Gen.mkM kiBind) x return () where kiBind :: ValBind -> KI ValBind kiBind vbind = do case vbind_type vbind of Just tyScheme -> kiTypeScheme tyScheme >> return vbind Nothing -> return vbind dumpKindInference :: Program -> ST Doc dumpKindInference (Program typeDefs classes _ _) = do l <- kindAssocs let vars = vcat $ mapMaybe printKind' l tsigs = concat $ map class_tsigs classes tydefKinds <- mapM kindOf typeDefs assocKinds <- mapM kindOf tsigs let tydefs = vcat $ map printKind (zip (map tydef_name typeDefs) tydefKinds) assocs = vcat $ map printKind (zip (map assocSig_name tsigs) assocKinds) return (vars $$ tydefs $$ assocs) where printKind :: Pretty v => (v,Kind) -> Doc printKind (v,k) = ppr v <+> text "::" <+> ppr k printKind' :: Pretty v => (v,Kind) -> Maybe Doc printKind' (v,k) = -- It's a hack not the print type variables starting with -- `__'. But this prevents tests from breaking -- just because of a change in the prelude. if take 2 (show (ppr v)) == "__" then Nothing else Just $ ppr v <+> text "::" <+> ppr k starStarStar = Kfun Star (Kfun Star Star) kindMap = [(funTypeConstructor, starStarStar), (pairTypeConstructor, starStarStar), (intTypeConstructor, Star), (boolTypeConstructor, Star), (unitTypeConstructor, Star)] kindOfBuiltin s = case List.lookup s kindMap of Just k -> k Nothing -> panic ("Unknown builtin: " ++ s)