{-# LANGUAGE DeriveDataTypeable #-} module Language.Java.Paragon.TypeCheck.TypeMap where import Language.Java.Paragon.Syntax import Language.Java.Paragon.Pretty import Language.Java.Paragon.Interaction import Language.Java.Paragon.TypeCheck.Actors import Language.Java.Paragon.TypeCheck.Policy import Language.Java.Paragon.TypeCheck.Locks import Language.Java.Paragon.TypeCheck.Types import qualified Data.Map as Map import Data.Generics.Uniplate.Data import Data.Data typeMapModule :: String typeMapModule = typeCheckerBase ++ ".TypeMap" {- data FieldSig = FSig { fType :: TcType, fPol :: TcPolicy, fStatic :: Bool, fFinal :: Bool } deriving (Show, Data, Typeable) data VarSig = VarSig { vType :: TcType, vPol :: TcPolicy, vParam :: Bool, vFinal :: Bool } -} data VarFieldSig = VSig { varType :: TcType, varPol :: ActorPolicy, varParam :: Bool, varStatic :: Bool, varFinal :: Bool } deriving (Show, Data, Typeable) data MethodSig = MSig { mRetType :: TcType, mRetPol :: ActorPolicy, mPars :: [Ident ()], mParBounds :: [ActorPolicy], mWrites :: ActorPolicy, mExpects :: [TcLock], mLMods :: ([TcLock],[TcLock]), mExns :: [(TcType, ExnSig)] } deriving (Show, Data, Typeable) data ExnSig = ExnSig { exnReads :: ActorPolicy, exnWrites :: ActorPolicy, exnMods :: ([TcLock],[TcLock]) } deriving (Show, Data, Typeable) data ConstrSig = CSig { cPars :: [Ident ()], cParBounds :: [ActorPolicy], cWrites :: ActorPolicy, cExpects :: [TcLock], cLMods :: ([TcLock],[TcLock]), cExns :: [(TcType, ExnSig)] } deriving (Show, Data, Typeable) data LockSig = LSig { lPol :: ActorPolicy, lArity :: Int, lProps :: [TcClause TcAtom] } deriving (Show, Data, Typeable) data TypeSig = TSig { tType :: TcRefType, tIsClass :: Bool, tIsFinal :: Bool, tSupers :: [TcClassType], tImpls :: [TcClassType], tMembers :: TypeMap } deriving (Show, Data, Typeable) type Map = Map.Map type MethodMap = Map ([TypeParam ()], [TcType], Bool) MethodSig type ConstrMap = Map ([TypeParam ()], [TcType], Bool) ConstrSig data TypeMap = TypeMap { -- signatures fields :: Map (Ident ()) VarFieldSig, methods :: Map (Ident ()) MethodMap, constrs :: ConstrMap, locks :: Map (Ident ()) LockSig, -- known policy-level entities policies :: Map (Ident ()) (PrgPolicy TcActor), actors :: Map (Ident ()) ActorId, -- typemethod eval info typemethods :: Map (Ident ()) ([Ident ()], Block ()), -- types and packages types :: Map (Ident ()) ([TypeParam ()], [Ident ()], TypeSig), packages :: Map (Ident ()) TypeMap } deriving (Show, Data, Typeable) emptyTM :: TypeMap emptyTM = TypeMap { fields = Map.empty, methods = Map.empty, constrs = Map.empty, locks = Map.empty, policies = Map.empty, actors = Map.empty, typemethods = Map.empty, types = Map.empty, packages = Map.empty } hardCodedArrayTM :: TcType -> PrgPolicy TcActor -> TypeSig hardCodedArrayTM ty p = let memTM = emptyTM { fields = Map.fromList [(Ident () "length", VSig intT thisP False False True)] , methods = Map.fromList [] -- TODO } in TSig { tType = TcArrayT ty p, tIsClass = False, tIsFinal = False, tSupers = [], -- TODO: what's the super type of an array? tImpls = [], -- TODO: Iterable etc tMembers = memTM } clearToPkgs :: TypeMap -> TypeMap clearToPkgs tm = emptyTM { packages = packages tm } clearToTypes :: TypeMap -> TypeMap clearToTypes tm = emptyTM { packages = packages tm, types = types tm } pkgsAndTypes :: TypeMap -> Map (Ident ()) TypeMap pkgsAndTypes tm = Map.union (packages tm) -- disregard type parameters (Map.map (tMembers . (\(_,_,x) -> x)) $ types tm) merge :: TypeMap -> TypeMap -> TypeMap merge tm1 tm2 = TypeMap { fields = Map.union (fields tm1) (fields tm2), methods = Map.union (methods tm1) (methods tm2), constrs = Map.union (constrs tm1) (constrs tm2), locks = Map.union (locks tm1) (locks tm2), policies = Map.union (policies tm1) (policies tm2), actors = Map.union (actors tm1) (actors tm2), typemethods = Map.union (typemethods tm1) (typemethods tm2), types = Map.union (types tm1) (types tm2), packages = Map.union (packages tm1) (packages tm2) } -------------------------------------------- -- Working with extensions -- -------------------------------------------- extendTypeMapP :: Name () -> TypeMap -> TypeMap -> TypeMap extendTypeMapP = go . flattenName where go :: [Ident ()] -> TypeMap -> TypeMap -> TypeMap go [] _ _ = panic (typeMapModule ++ ".extendTypeMapP") "Empty ident list" go [i] leafTm tm = tm { packages = Map.insert i leafTm (packages tm) } go (i:is) leafTm tm = let mTm = packages tm eTm = case Map.lookup i mTm of Just innerTm -> innerTm Nothing -> emptyTM newTm = go is leafTm eTm in tm { packages = Map.insert i newTm mTm } extendTypeMapT :: Name () -> [TypeParam ()] -> [Ident ()] -> TypeSig -> TypeMap -> TypeMap extendTypeMapT = go . flattenName where go :: [Ident ()] -> [TypeParam ()] -> [Ident ()] -> TypeSig -> TypeMap -> TypeMap go [] _ _ _ _ = panic (typeMapModule ++ ".extendTypeMapT") "Empty ident list" go [i] tps iaps tSig tm = tm { types = Map.insert i (tps,iaps,tSig) (types tm) } go (i:is) tps iaps tSig tm = let mTm = packages tm eTm = case Map.lookup i mTm of Just innerTm -> innerTm Nothing -> emptyTM newTm = go is tps iaps tSig eTm in tm { packages = Map.insert i newTm mTm } extendTypeMapN :: Name () -> (TypeMap -> TypeMap) -> TypeMap -> TypeMap extendTypeMapN = go . flattenName where go :: [Ident ()] -> (TypeMap -> TypeMap) -> TypeMap -> TypeMap go [] _ _ = panic (typeMapModule ++ ".extendTypeMapN") "Empty ident list" go [i] tmf tm = let mTm = types tm (tps,iaps,tSig) = case Map.lookup i mTm of Just tyInfo -> tyInfo Nothing -> panic (typeMapModule ++ ".extendTypeMapN") $ "Type not yet initialized: " ++ prettyPrint i tTm = tMembers tSig newSig = tSig { tMembers = tmf tTm } in tm { types = Map.insert i (tps,iaps,newSig) mTm } go (i:is) tmf tm = let mTm = packages tm eTm = case Map.lookup i mTm of Just innerTm -> innerTm Nothing -> panic (typeMapModule ++ ".extendTypeMapN") $ "Package not yet initialized: " ++ prettyPrint i newTm = go is tmf eTm in tm { packages = Map.insert i newTm mTm } -------------------------------------- -- Working with the lookups -- -------------------------------------- -- TODO: This is an anomaly!!! lookupNamed :: (TypeMap -> Map (Ident ()) a) -> Name () -> TypeMap -> Maybe a lookupNamed recf (Name _ _ Nothing i) tm = Map.lookup i (recf tm) lookupNamed recf nam@(Name _ _ (Just pre) i) tm = do newTm <- case nameType pre of TName -> do (_tps, _iaps, tsig) <- lookupNamed types pre tm --if not (null tps) --then Nothing --else return $ tMembers tsig PName -> lookupNamed packages pre tm {- EName -> do vsig <- lookupNamed fields pre tm case lookupTypeOfT (varType vsig) tm of Left _ -> Nothing Right newTm -> return newTm -} _ -> panic (typeMapModule ++ ".lookupNamed") $ "Prefix is not a package or type: " ++ show nam Map.lookup i $ recf newTm lookupNamed _ _ _ = panic (typeMapModule ++ ".lookupNamed") "AntiQName should not appear in AST being type-checked" lookupTypeOfStateT :: TcStateType -> TypeMap -> Either (Maybe String) TypeSig lookupTypeOfStateT (TcInstance (TcClassT n tas) iaas) startTm = case n of Name _ TName _ _ -> let mSig = lookupNamed types n startTm in case mSig of Nothing -> Left Nothing Just (tps, iaps, tsig) -- TODO: Type argument inference | length tps /= length tas -> Left $ Just $ "Wrong number of type arguments in class type.\n" ++ "Type " ++ prettyPrint n ++ " expects " ++ show (length tps) ++ " arguments but has been given " ++ show (length tas) | length iaps /= length iaas -> panic (typeMapModule ++ ".lookupTypeOfStateT") $ "Too few implicit arguments: " ++ show (iaps, iaas) | otherwise -> let itps = map (ActorParam ()) iaps itas = map TcActualActor iaas in Right $ instantiate (zip (tps++itps) (tas++itas)) tsig Name _ _ _ _ -> Left Nothing _ -> panic (typeMapModule ++ ".lookupTypeOfT") $ show n lookupTypeOfStateT (TcType t) tm = case lookupTypeOfT t tm of Right (is, tsig) | null is -> Right tsig | otherwise -> panic (typeMapModule ++ ".lookupTypeOfStateT") $ "Needs implicit actor arguments: " ++ show (t, is) Left err -> Left err lookupTypeOfStateT _ _ = Left Nothing -- | lookupTypeOfT will, given a type T and a top-level type environment, -- return the type environment for T tagged with Right. -- Left denotes an error, which wraps: -- * If T is not a refType, return Nothing -- * If T is given the wrong number of type arguments, return Just errorMessage. lookupTypeOfT :: TcType -> TypeMap -> Either (Maybe String) ([Ident ()], TypeSig) lookupTypeOfT (TcRefT refT) = lookupTypeOfRefT refT lookupTypeOfT _ = const $ Left Nothing lookupTypeOfRefT :: TcRefType -> TypeMap -> Either (Maybe String) ([Ident ()], TypeSig) lookupTypeOfRefT (TcArrayT ty pol) _ = Right $ ([], hardCodedArrayTM ty pol) lookupTypeOfRefT (TcTypeVar _ ) _ = panic (typeMapModule ++ ".lookupTypeOfRefT") "TcTypeVar should have been instantiated" lookupTypeOfRefT TcNullT _ = Left $ Just $ "Cannot dereference null" lookupTypeOfRefT (TcClsRefT (TcClassT n tas)) startTm = case n of Name _ TName _ _ -> let mSig = lookupNamed types n startTm in case mSig of Nothing -> Left Nothing Just (tps, iaps, tsig) -- TODO: Type argument inference | length tps /= length tas -> Left $ Just $ "Wrong number of type arguments in class type.\n" ++ "Type " ++ prettyPrint n ++ " expects " ++ show (length tps) ++ " arguments but has been given " ++ show (length tas) -- | not (null iaps) -> panic (typeMapModule ++ ".lookupTypeOfRefT") -- $ "Too many implicit arguments: " ++ show iaps | otherwise -> Right $ (iaps, instantiate (zip tps tas) tsig) Name _ _ _ _ -> Left Nothing _ -> panic (typeMapModule ++ ".lookupTypeOfRefT") $ show n -------------------------------------- -- Type argument instantiation -- -------------------------------------- instantiate :: Data a => [(TypeParam (),TcTypeArg)] -> a -> a instantiate pas = transformBi instT . transformBi instA . transformBi instP . transformBi instLs where instT :: TcRefType -> TcRefType instT tv@(TcTypeVar i) = case lookup i typs of Just rt -> rt Nothing -> tv instT rt = rt instA :: ActorId -> ActorId instA av@(ActorTPVar i) = case lookup i as of Just a -> a Nothing -> av instA a = a instP :: ActorPolicy -> ActorPolicy instP pv@(RealPolicy (TcRigidVar i)) = case lookup i ps of Just p -> p Nothing -> pv instP p = p instLs :: [TcLock] -> [TcLock] instLs = concatMap instL instL :: TcLock -> [TcLock] instL lv@(TcLockVar i) = case lookup i locs of Just le -> le Nothing -> [lv] instL l = [l] typs = [ (i, rt) | (TypeParam _ i _, TcActualType rt) <- pas ] as = [ (i, n ) | (ActorParam _ i, TcActualActor n) <- pas ] ps = [ (i, p ) | (PolicyParam _ i, TcActualPolicy p) <- pas ] locs = [ (i, ls) | (LockStateParam _ i, TcActualLockState ls) <- pas ] instThis :: Data a => ActorPolicy -> a -> a instThis p = transformBi instThisPol where instThisPol :: ActorPolicy -> ActorPolicy instThisPol (RealPolicy q) = substThis p q instThisPol q = q