diff --git a/paragon.cabal b/paragon.cabal --- a/paragon.cabal +++ b/paragon.cabal @@ -1,5 +1,5 @@ Name: paragon -Version: 0.1.10 +Version: 0.1.11 License: BSD3 License-File: LICENSE Author: Niklas Broberg @@ -32,7 +32,8 @@ Library Build-Tools: alex >= 2.3 - Build-Depends: array >= 0.1, pretty >= 1.0, cpphs >= 1.3, parsec >= 2.1 && < 3, containers >= 0.4 && < 0.5, uniplate == 1.6, directory, filepath, haskell-src-meta, th-lift, template-haskell + Build-Depends: array >= 0.1, pretty >= 1.0, cpphs >= 1.3, parsec >= 2.1 && < 3, containers >= 0.4 && < 0.5, + uniplate == 1.6, directory, filepath, haskell-src-meta, th-lift, template-haskell if flag(base4) Build-depends: base >= 4 && < 5, syb cpp-options: -DBASE4 @@ -65,6 +66,7 @@ Language.Java.Paragon.TypeCheck.Compile, Language.Java.Paragon.QuasiQuoter, Language.Java.Paragon.QuasiQuoter.Lift, + Language.Java.Paragon.QuasiQuoter.Derive, Language.Java.Paragon.PiGeneration, Language.Java.Paragon.Verbosity, Language.Java.Paragon.Annotated @@ -100,6 +102,7 @@ Language.Java.Paragon.TypeCheck.Uniq, Language.Java.Paragon.QuasiQuoter, Language.Java.Paragon.QuasiQuoter.Lift, + Language.Java.Paragon.QuasiQuoter.Derive, Language.Java.Paragon.Compile, Language.Java.Paragon.PiGeneration, Language.Java.Paragon.Verbosity diff --git a/src/Language/Java/Paragon.hs b/src/Language/Java/Paragon.hs --- a/src/Language/Java/Paragon.hs +++ b/src/Language/Java/Paragon.hs @@ -33,7 +33,7 @@ deriving (Show, Eq) versionString, usageHeader :: String -versionString = "Paragon Compiler version: 0.1.10" +versionString = "Paragon Compiler version: 0.1.11" usageHeader = "Usage: parac [OPTION...] files..." options :: [OptDescr Flag] @@ -64,7 +64,7 @@ liftE :: Show e => Either e a -> IO a liftE eea = case eea of Right a -> return a - Left e -> fail $ show e + Left e -> fail $ "\n\n" ++ show e compile :: [Flag] -> String -> IO () compile flags filePath = do diff --git a/src/Language/Java/Paragon/Parser.hs b/src/Language/Java/Paragon/Parser.hs --- a/src/Language/Java/Paragon/Parser.hs +++ b/src/Language/Java/Paragon/Parser.hs @@ -859,13 +859,14 @@ return $ \p -> QualInstanceCreation () p tas i as mcb instanceCreation :: P (Exp ()) -instanceCreation = try instanceCreationNPS <|> do +instanceCreation = {- try instanceCreationNPS <|> -} do p <- primaryNPS ss <- list primarySuffix let icp = foldl (\a s -> s a) p ss case icp of + InstanceCreation {} -> return icp QualInstanceCreation {} -> return icp - _ -> fail "" + _ -> fail "instanceCreation" {- instanceCreation = @@ -901,7 +902,7 @@ return $ \p -> PrimaryFieldAccess () p i fieldAccess :: P (FieldAccess ()) -fieldAccess = try fieldAccessNPS <|> do +fieldAccess = {- try fieldAccessNPS <|> -} do p <- primaryNPS ss <- list primarySuffix let fap = foldl (\a s -> s a) p ss @@ -962,7 +963,7 @@ return $ \p -> PrimaryMethodCall () p [] i as methodInvocationExp :: P (Exp ()) -methodInvocationExp = try (MethodInv () <$> methodInvocationNPS) <|> do +methodInvocationExp = {- try (MethodInv () <$> methodInvocationNPS) <|> -} do p <- primaryNPS ss <- list primarySuffix let mip = foldl (\a s -> s a) p ss @@ -1012,8 +1013,9 @@ arrayAccessSuffix = do e <- brackets exp return $ \ref -> ArrayIndex () ref e - -arrayAccess = try arrayAccessNPS <|> do + +arrayAccess :: P (ArrayIndex ()) +arrayAccess = {- try arrayAccessNPS <|> -} do p <- primaryNoNewArrayNPS ss <- list primarySuffix let aap = foldl (\a s -> s a) p ss @@ -1037,12 +1039,15 @@ tok KW_New t <- nonArrayType f <- (try $ do - ds <- list1 $ brackets empty + ds <- list1 $ (brackets empty >> opt (angles policy)) ai <- arrayInit - return $ \t -> ArrayCreateInit () t (length ds) ai) <|> - (do des <- list1 $ brackets exp - ds <- list $ brackets empty - return $ \t -> ArrayCreate () t des (length ds)) + return $ \t -> ArrayCreateInit () t ds ai) <|> + (do des <- list1 $ do + e <- brackets exp + p <- opt (angles policy) + return (e,p) + ds <- list $ (brackets empty >> opt (angles policy)) + return $ \t -> ArrayCreate () t des ds) return $ f t literal :: P (Literal ()) @@ -1139,13 +1144,15 @@ refType :: P (RefType ()) refType = (do pt <- primType - (mp:mps) <- list1 arrPols - return $ foldl (\f mp -> flip (ArrayType ()) mp . RefType () . f) - (flip (ArrayType ()) mp . PrimType ()) mps pt) <|> + mps <- list1 arrPols + return $ ArrayType () (PrimType () pt) mps) + <|> (do ct <- classType mps <- list arrPols - return $ foldl (\f mp -> flip (ArrayType ()) mp . RefType () . f) - (ClassRefType ()) mps ct) "refType" + let baseType = ClassRefType () ct + case mps of + [] -> return baseType + _ -> return $ ArrayType () (RefType () baseType) mps) "refType" arrPols :: P (Maybe (Policy ())) arrPols = do @@ -1232,7 +1239,8 @@ policy = postfixExpNES -- Policy <$> policyLit <|> PolicyRef <$> (tok Op_Tilde >> name) policyExp :: P (PolicyExp ()) -policyExp = PolicyLit () <$> (braces $ seplist clause semiColon) <|> +policyExp = try (PolicyLit () <$> (braces $ seplist clause semiColon)) <|> + PolicyLit () <$> (braces colon >> return []) <|> PolicyOf () <$> (tok KW_P_Policyof >> parens ident) clause :: P (Clause ()) diff --git a/src/Language/Java/Paragon/Pretty.hs b/src/Language/Java/Paragon/Pretty.hs --- a/src/Language/Java/Paragon/Pretty.hs +++ b/src/Language/Java/Paragon/Pretty.hs @@ -1,7 +1,9 @@ +{-# LANGUAGE TupleSections #-} module Language.Java.Paragon.Pretty (prettyPrint, Pretty(..)) where import Text.PrettyPrint import Data.Char (toLower) +import Control.Arrow (first) import Language.Java.Paragon.Syntax @@ -378,15 +380,19 @@ , pretty ident <> ppArgs args ] $$ maybePP mBody - pretty (ArrayCreate _ t es k) = + pretty (ArrayCreate _ t eps ps) = text "new" <+> - hcat (pretty t : map (brackets . pretty) es - ++ replicate k (text "[]")) + hcat (pretty t : + map ppArrayDim + (map (first Just) eps ++ + map (Nothing,) ps)) +-- hcat (pretty t : map (brackets . pretty) es +-- ++ replicate k (text "[]")) - pretty (ArrayCreateInit _ t k init) = - text "new" - <+> hcat (pretty t : replicate k (text "[]")) - <+> pretty init + pretty (ArrayCreateInit _ t ps init) = + text "new" + <+> hcat (pretty t : map ppArrayDim (map (Nothing,) ps)) + <+> pretty init pretty (FieldAccess _ fa) = pretty fa @@ -526,6 +532,11 @@ ppArgs :: Pretty a => [a] -> Doc ppArgs = parens . hsep . punctuate comma . map pretty +ppArrayDim :: (Maybe (Exp a), Maybe (Policy a)) -> Doc +ppArrayDim (mE, mP) = + brackets (maybe empty pretty mE) <> + maybe empty (angles . pretty) mP + ----------------------------------------------------------------------- -- Types @@ -537,8 +548,9 @@ instance Pretty (RefType a) where pretty (ClassRefType _ ct) = pretty ct pretty (TypeVariable _ i) = pretty i - pretty (ArrayType _ t mp) = - pretty t <> text "[]" <> maybe empty (ppTypeParams . return) mp + pretty (ArrayType _ ty mPols) = + pretty ty <> hcat ((flip map) mPols + (\mP -> brackets empty <> maybe empty (angles . pretty) mP)) instance Pretty (ClassType a) where pretty (ClassType _ itas) = @@ -585,9 +597,7 @@ ppTypeParams :: Pretty a => [a] -> Doc ppTypeParams [] = empty -ppTypeParams tps = char '<' - <> hsep (punctuate comma (map pretty tps)) - <> char '>' +ppTypeParams tps = angles $ hsep (punctuate comma (map pretty tps)) ppImplements :: [RefType x] -> Doc ppImplements [] = empty @@ -616,6 +626,7 @@ -- Paragon Policies instance Pretty (PolicyExp a) where + pretty (PolicyLit _ []) = braces (char ':') pretty (PolicyLit _ cs) = braces $ hcat (punctuate (char ';') $ map pretty cs) pretty (PolicyOf _ i) = text "policyof" <> parens (pretty i) pretty (PolicyTypeVar _ i) = pretty i @@ -681,3 +692,6 @@ braceBlock xs = char '{' $+$ nest 2 (vcat xs) $+$ char '}' + +angles :: Doc -> Doc +angles d = char '<' <> d <> char '>' diff --git a/src/Language/Java/Paragon/QuasiQuoter/Derive.hs b/src/Language/Java/Paragon/QuasiQuoter/Derive.hs new file mode 100644 --- /dev/null +++ b/src/Language/Java/Paragon/QuasiQuoter/Derive.hs @@ -0,0 +1,27 @@ +{-# LANGUAGE QuasiQuotes, TemplateHaskell #-} +module Language.Java.Paragon.QuasiQuoter.Derive where + +import Language.Haskell.TH +import Language.Haskell.TH.Lift + +import Data.Data (Data) + +import Control.Monad ((<=<)) + +deriveLiftAll :: [Name] -> Q [Dec] +deriveLiftAll ns = do + is <- mapM (addDataCx <=< reify) ns + deriveLiftMany' is + +addDataCx :: Info -> Q Info +addDataCx i = + case i of + TyConI (DataD dcx n vsk cons _) -> do + dp <- dataPred $ head vsk + return $ TyConI (DataD (dp:dcx) n vsk cons []) + TyConI (NewtypeD dcx n vsk con _) -> do + dp <- dataPred $ head vsk + return $ TyConI (NewtypeD (dp:dcx) n vsk con []) + _ -> error $ "Unhandled Dec: " ++ show i + where dataPred (PlainTV n) = classP ''Data [varT n] + diff --git a/src/Language/Java/Paragon/Syntax.hs b/src/Language/Java/Paragon/Syntax.hs --- a/src/Language/Java/Paragon/Syntax.hs +++ b/src/Language/Java/Paragon/Syntax.hs @@ -1,6 +1,9 @@ {-# LANGUAGE CPP, DeriveDataTypeable, DeriveFunctor, TemplateHaskell, FlexibleContexts, MultiParamTypeClasses, FlexibleInstances #-} -module Language.Java.Paragon.Syntax where +module Language.Java.Paragon.Syntax ( + module Language.Java.Paragon.Syntax, + module Language.Java.Paragon.Annotated + ) where import Data.Data @@ -329,10 +332,10 @@ | QualInstanceCreation a (Exp a) [TypeArgument a] (Ident a) [Argument a] (Maybe (ClassBody a)) -- | An array instance creation expression is used to create new arrays. The last argument denotes the number -- of dimensions that have no explicit length given. These dimensions must be given last. - | ArrayCreate a (Type a) [Exp a] Int + | ArrayCreate a (Type a) [(Exp a, Maybe (Policy a))] [Maybe (Policy a)] -- | An array instance creation expression may come with an explicit initializer. Such expressions may not -- be given explicit lengths for any of its dimensions. - | ArrayCreateInit a (Type a) Int (ArrayInit a) + | ArrayCreateInit a (Type a) [Maybe (Policy a)] (ArrayInit a) -- | A field access expression. | FieldAccess a (FieldAccess a) -- | A method invocation expression. @@ -470,7 +473,8 @@ data RefType a = ClassRefType a (ClassType a) | TypeVariable a (Ident a) - | ArrayType a (Type a) (Maybe (Policy a)) + | ArrayType a (Type a) [Maybe (Policy a)] + -- ^ The second argument to ArrayType is the base type, and should not be an array type deriving (Eq,Ord,Show,Typeable,Data,Functor) -- | A class or interface type consists of a type declaration specifier, diff --git a/src/Language/Java/Paragon/TypeCheck.hs b/src/Language/Java/Paragon/TypeCheck.hs --- a/src/Language/Java/Paragon/TypeCheck.hs +++ b/src/Language/Java/Paragon/TypeCheck.hs @@ -49,7 +49,7 @@ -- debug $ "Type checking completed!" return (CompilationUnit () pkg imps [fullTd]) case e of - Left str -> fail str + Left str -> fail $ "\n\n" ++ str Right ast -> return ast where allImps = defaultImportDecls ++ imps @@ -690,7 +690,7 @@ -- Methods typeCheckSignature st md@(MethodDecl _ ms tps retT i ps exns mb) tcba | not (Typemethod () `elem` ms) = do - --debug $ "typeCheckSignature: " ++ prettyPrint (MethodDecl ms tps retT i ps exns (MethodBody Nothing)) + -- debug $ "typeCheckSignature: " ++ prettyPrint (MethodDecl () ms tps retT i ps exns (MethodBody () Nothing)) (pTs, mti) <- withErrCtxt ("When checking signature of method " ++ prettyPrint i ++ "(" ++ concat (intersperse ", " [prettyPrint t | FormalParam _ _ t _ _ <- ps ]) ++ "):\n") $ do -- 0. Setup type params @@ -772,7 +772,7 @@ withParam (FormalParam _ _ _ _ (VarId _ i)) = withTypeMap $ \tm -> tm { fields = Map.insert i (VSig err err err err) (fields tm) } - where err = error "Use of parameter directly in modifier" -- TODO: UUUUGLY! + where err = error $ "Use of parameter " ++ prettyPrint i ++ " directly in modifier" -- TODO: UUUUGLY! @@ -874,6 +874,16 @@ checkM (liftCont $ ty <: matchTy) $ "typeCheckVarDecl: type mismatch" constraint_ pol matchPol solve cs + Just (InitArray _ arr) -> + case mArrayType matchTy of + Nothing -> fail $ "Field " ++ prettyPrint i + ++ " of non-array type " ++ prettyPrint matchTy + ++ " given literal array initializer" + Just (baseTy, pols) -> do + (_,cs) <- runTc (simpleEnv lim) st $ + tcArrayInit baseTy pols arr + solve cs +-- _ -> error $ "typeCheckVarDecl: Array syntax not yet supported" typeCheckMethodDecl :: TcState -> MemberDecl () -> TcCont r () typeCheckMethodDecl st (MethodDecl _ _ tps _ i ps _ mb) = do @@ -902,7 +912,7 @@ branchPCE = (branchMap, pWri) } - --debug $ "Using env: " ++ show env + -- debug $ "Using env: " ++ show env -- Setup the state in which to check the body parAids <- concat <$> mapM aliasIfActor (zip pars tysPs) let parAMap = Map.fromList $ map ((Name () . return) *** (\aid -> AI aid Stable)) parAids @@ -910,7 +920,6 @@ -- This little thing is what actually checks the body (endSt,cs) <- runTc env parSt $ tcMethodBody mb >> getState - -- ... and then we need to check the end result solve cs check (lMods `models` lockMods endSt) $ diff --git a/src/Language/Java/Paragon/TypeCheck/Evaluate.hs b/src/Language/Java/Paragon/TypeCheck/Evaluate.hs --- a/src/Language/Java/Paragon/TypeCheck/Evaluate.hs +++ b/src/Language/Java/Paragon/TypeCheck/Evaluate.hs @@ -52,12 +52,13 @@ return $ mpol `orUse` def -} evaluate :: Policy () -> TcCont r TcPolicy -evaluate (PolicyExp _ pe) = evalPolicyExp pe -{-evaluate (ExpName n) = do - polMap <- (policies . typemap) <$> getEnv - case Map.lookup n polMap of - Nothing -> fail $ "Unknown policy: " ++ prettyPrint n - Just p -> return p -} +evaluate = evalPolicy +{-evaluate (PolicyExp _ pe) = evalPolicyExp pe +evaluate (ExpName _ n) = -- getPolicy n +-- polMap <- (policies . typemap) <$> getEnv +-- case Map.lookup n polMap of +-- Nothing -> fail $ "Unknown policy: " ++ prettyPrint n +-- Just p -> return p evaluate (BinOp _ p1 (Add _) p2) = do pol1 <- evaluate p1 pol2 <- evaluate p2 @@ -68,7 +69,7 @@ return $ pol1 `join` pol2 evaluate (MethodInv _ mi) = evalTypeMethod mi evaluate e = fail $ "Unsupported type-level expression: " ++ prettyPrint e - +-} evalTypeMethod :: MethodInvocation () -> TcCont r TcPolicy evalTypeMethod = undefined diff --git a/src/Language/Java/Paragon/TypeCheck/Monad.hs b/src/Language/Java/Paragon/TypeCheck/Monad.hs --- a/src/Language/Java/Paragon/TypeCheck/Monad.hs +++ b/src/Language/Java/Paragon/TypeCheck/Monad.hs @@ -23,6 +23,8 @@ freshActorId, aliasActorId, scrambleActors, + getPolicy, + getExnPC, throwExn, activateExns, deactivateExn, getExnState, mergeActiveExnStates, useExnState, @@ -32,7 +34,7 @@ newMetaPolVar, - constraint, constraint_, + constraint, constraint_, constraintLS, exnConsistent, extendTypeMapP, extendTypeMapT, lookupPkgTypeMap, @@ -498,10 +500,13 @@ locksToRec :: [TcLock] -> TcPolicyRec locksToRec ls = TcPolicyRec (map (\x -> TcClause x []) (map lockToAtom ls)) - -constraint_ :: TcPolicy -> TcPolicy -> Tc r () +constraint_, constraintLS :: TcPolicy -> TcPolicy -> Tc r () constraint_ = constraint [] +constraintLS p1 p2 = do + l <- getCurrentLockState + constraint l p1 p2 + exnConsistent :: TcType -> ExnSig -> Tc r () exnConsistent exnTy (ExnSig rX wX _) = do exnMap <- exnsE <$> getEnv @@ -557,10 +562,11 @@ evalSrcRefType :: RefType () -> TcCont r TcRefType evalSrcRefType (TypeVariable _ i) = return $ TcTypeVar i -evalSrcRefType (ArrayType _ t mp) = do +evalSrcRefType (ArrayType _ t mps) = do ty <- evalSrcType t - mpol <- maybe (return Nothing) (fmap Just . evalPolicy) mp - return $ TcArrayT ty mpol + pols <- mapM (maybe (return bottom) evalPolicy) mps + let (TcRefT arrTy) = mkArrayType ty pols + return arrTy evalSrcRefType (ClassRefType _ ct) = TcClsRefT <$> evalSrcClsType ct evalSrcClsType :: ClassType () -> TcCont r TcClassType @@ -656,8 +662,10 @@ fromSrcRefType :: TypeMap -> RefType () -> TcRefType fromSrcRefType tm (ClassRefType _ ct) = TcClsRefT $ fromSrcClsType tm ct -fromSrcRefType tm (ArrayType _ t mp) = - TcArrayT (fromSrcType tm t) (fmap (fromSrcPolicy tm) mp) +fromSrcRefType tm (ArrayType _ t mps) = + let pols = map (maybe bottom (fromSrcPolicy tm)) mps + (TcRefT arrT) = mkArrayType (fromSrcType tm t) pols + in arrT fromSrcRefType tm (TypeVariable _ i) = TcTypeVar i fromSrcClsType :: TypeMap -> ClassType () -> TcClassType diff --git a/src/Language/Java/Paragon/TypeCheck/Monad/TcBase.hs b/src/Language/Java/Paragon/TypeCheck/Monad/TcBase.hs --- a/src/Language/Java/Paragon/TypeCheck/Monad/TcBase.hs +++ b/src/Language/Java/Paragon/TypeCheck/Monad/TcBase.hs @@ -62,5 +62,12 @@ liftIO ioa = TcBase $ \_ _ _ _ -> do liftM Right ioa withErrCtxt :: String -> TcBase a -> TcBase a -withErrCtxt str (TcBase f) = - TcBase $ \tm ty u ec -> f tm ty u (ec . (str ++)) +--withErrCtxt str (TcBase f) = +-- TcBase $ \tm ty u ec -> f tm ty u (ec . (str ++)) +withErrCtxt str = withErrCtxt' (. (str ++)) + +getErrCtxt :: TcBase (String -> String) +getErrCtxt = TcBase $ \_ _ _ ec -> return $ Right ec + +withErrCtxt' :: ((String -> String) -> (String -> String)) -> TcBase a -> TcBase a +withErrCtxt' strff (TcBase f) = TcBase $ \tm ty u ec -> f tm ty u (strff ec) diff --git a/src/Language/Java/Paragon/TypeCheck/Monad/TcCont.hs b/src/Language/Java/Paragon/TypeCheck/Monad/TcCont.hs --- a/src/Language/Java/Paragon/TypeCheck/Monad/TcCont.hs +++ b/src/Language/Java/Paragon/TypeCheck/Monad/TcCont.hs @@ -4,7 +4,8 @@ import Language.Java.Paragon.TypeCheck.Monad.TcBase (TcBase, runTcBase) import qualified Language.Java.Paragon.TypeCheck.Monad.TcBase - as Base (getUniqRef, getTypeMap, getThisT, withTypeMap, liftIO, withErrCtxt) + as Base (getUniqRef, getTypeMap, getThisT, withTypeMap, liftIO, + withErrCtxt, getErrCtxt, withErrCtxt') import Language.Java.Paragon.TypeCheck.Uniq (Uniq) import Language.Java.Paragon.TypeCheck.TcEnv (TypeMap) @@ -30,6 +31,7 @@ return x = TcCont $ \k -> k x TcCont f >>= h = TcCont $ \k -> f (\a -> let TcCont g = h a in g k) + fail err = liftBase (fail err) instance Functor (TcCont r) where fmap = liftM @@ -59,10 +61,20 @@ getThisT = liftBase Base.getThisT withTypeMap :: (TypeMap -> TypeMap) -> TcCont r a -> TcCont r a -withTypeMap tmf (TcCont f) = TcCont $ \k -> Base.withTypeMap tmf $ f k +withTypeMap tmf (TcCont f) = + TcCont $ \k -> do + tm <- Base.getTypeMap + Base.withTypeMap tmf $ f (\a -> Base.withTypeMap (const tm) $ k a) + +-- = TcCont $ \k -> Base.withTypeMap tmf (f return) >>= k +-- = TcCont $ \k -> Base.withTypeMap tmf $ f k + liftIO :: IO a -> TcCont r a liftIO = liftBase . Base.liftIO withErrCtxt :: String -> TcCont r a -> TcCont r a -withErrCtxt str (TcCont f) = TcCont $ \k -> Base.withErrCtxt str $ f k +withErrCtxt str (TcCont f) = + TcCont $ \k -> do + ec <- Base.getErrCtxt + Base.withErrCtxt str $ f (\a -> Base.withErrCtxt' (const ec) $ k a) diff --git a/src/Language/Java/Paragon/TypeCheck/TcExp.hs b/src/Language/Java/Paragon/TypeCheck/TcExp.hs --- a/src/Language/Java/Paragon/TypeCheck/TcExp.hs +++ b/src/Language/Java/Paragon/TypeCheck/TcExp.hs @@ -11,9 +11,9 @@ import Language.Java.Paragon.TypeCheck.TcEnv -- The relevant things should really import Language.Java.Paragon.TypeCheck.TcState -- be re-exported by .Monad ---import Control.Monad (liftM) -import Control.Applicative ( (<$>) ) import Data.List ( (\\) ) +import Control.Applicative ( (<$>) ) +import Control.Monad ( (=<<) ) import Control.Arrow ( first ) import qualified Data.Map as Map @@ -64,7 +64,10 @@ --debugTc $ "tcExp ExpName: " ++ show n -- lookupVar handles all the complexity of -- finding the correct actor id, if applicable - (ty,pol) <- lookupVar n + (ty1,pol) <- lookupVar n + ty <- if ty1 == policyT + then policyPolT <$> getPolicy n + else return ty1 --debugTc $ show (ty,pol) return (ty, pol) @@ -91,6 +94,22 @@ This _ -> Just $ thisFE fi _ -> Nothing return (tyF, pF, Just tyE, Just pE, eEnt, Nothing) + ArrayLhs _ (ArrayIndex _ arrE iE) -> do + (tyA, pA) <- tcExp arrE + case tyA of + TcRefT (TcArrayT tyElem pElem) -> do + (tyI, pI) <- tcExp iE + check (isIntConvertible tyI) $ + "Non-integral expression of type " ++ prettyPrint tyI + ++ " used as array index expression" + constraintLS pI pA + return (tyElem, pElem, Just tyA, Just pA, Nothing, Nothing) + + _ -> fail $ "Cannot index non-array expression " ++ prettyPrint arrE + ++ " of type " ++ prettyPrint tyA + + + _ -> fail $ "Lhs not supported: " ++ prettyPrint lhs (tyRhs, pRhs) <- tcExp rhs @@ -107,8 +126,7 @@ epc <- getExnPC constraint_ epc pV -- Check: pRhs <= pV modulo L - l <- getCurrentLockState - constraint l pRhs pV + constraintLS pRhs pV -- Check: pO <= pV, if pO exists maybeM mpO (\pO -> constraint_ pO pV) @@ -124,7 +142,7 @@ -- Rule NEW tcExp e@(InstanceCreation _ tas ct args mBody) = do - --debugTc $ "tcExp: " ++ show e + -- debugTc $ "tcExp: " ++ show e tyT <- liftCont $ evalSrcClsType ct -- DEBUG --debugTc $ "Type: " ++ show tyT @@ -235,16 +253,122 @@ tcExp (FieldAccess _ fa) = tcFieldAccess fa +-- Arrays + +tcExp (ArrayCreate _ bt dimEsPs dimImplPs) = do + baseTy <- liftCont $ evalSrcType bt + + -- Check the types and policies of all dimension expressions + check (not $ null dimEsPs) $ + "Array creation must have at least one dimension expression, or an explicit initializer" + let ((dimE1,mDimP1):dimEsPsRest) = dimEsPs -- at least one exists, checked above + + -- The first dimexpr will determine the policy + -- of the whole array creation expression + (ty1, pol1) <- tcExp dimE1 + -- Dimexprs must have integral-convertible types + check (isIntConvertible ty1) $ nonIntErr ty1 + + -- Check that the remaining dimexprs each conform to + -- the policy given at the level outside it + polEDims <- checkDimExprs [] dimEsPs =<< evalMaybePol mDimP1 + + -- Evaluate given policies for implicit dimensions + polIDims <- mapM evalMaybePol dimImplPs + + -- Return the array type, and the policy of the outermost dimexpr + return (mkArrayType baseTy (polEDims ++ polIDims), pol1) + + where checkDimExprs :: [TcPolicy] -> [(Exp (), Maybe (Policy ()))] -> TcPolicy -> Tc r [TcPolicy] + checkDimExprs acc [] pPrev = return $ reverse (pPrev:acc) + checkDimExprs acc ((e,mp):emps) pPrev = do + (tyE,pE) <- tcExp e + check (isIntConvertible tyE) $ nonIntErr tyE + -- Each dimexpr must satisfy the policy of the outer dim + constraintLS pE pPrev + pNext <- evalMaybePol mp + checkDimExprs (pPrev:acc) emps pNext + + nonIntErr :: TcType -> String + nonIntErr ty = + "Non-integral expression of type " ++ prettyPrint ty ++ + " used as dimension expression in array creation" + +tcExp (ArrayCreateInit _ bt dimImplPs arrInit) = do + baseTy <- liftCont $ evalSrcType bt + -- Evaluate given policies for implicit (all) dimensions + dimPols <- mapM evalMaybePol dimImplPs + -- Check that the initializer has the right type and policies + -- of subexpressions + tcArrayInit baseTy dimPols arrInit + + -- Return the specified array type + -- Literal array initializers have known length, + -- so their apparent policy is bottom + return (mkArrayType baseTy dimPols, bottom) + +tcExp (ArrayAccess _ (ArrayIndex _ arrE iE)) = do + (tyA, pA) <- tcExp arrE + case tyA of + TcRefT (TcArrayT tyElem pElem) -> do + (tyI, pI) <- tcExp iE + check (isIntConvertible tyI) $ + "Non-integral expression of type " ++ prettyPrint tyI + ++ " used as array index expression" + constraintLS pI pA + return (tyElem, pElem `join` pA) + + _ -> fail $ "Cannot index non-array expression " ++ prettyPrint arrE + ++ " of type " ++ prettyPrint tyA + + tcExp e = fail $ "tcExp: Unsupported expression: " ++ prettyPrint e -------------------------- +-- Array initializers + +tcArrayInit :: TcType -> [TcPolicy] -> ArrayInit () -> Tc r () +tcArrayInit baseType (pol1:pols) (ArrayInit _ inits) = do + ps <- mapM (tcVarInit baseType pols) inits + mapM_ (\p -> constraintLS p pol1) ps +tcArrayInit _ [] _ = fail $ "Array initializer has too many dimensions" + +tcVarInit :: TcType -> [TcPolicy] -> VarInit () -> Tc r TcPolicy +tcVarInit baseType pols (InitExp _ e) = do +-- debugTc $ "Pols: " ++ show pols +-- debugTc $ "Exp: " ++ show e + (tyE,pE) <- tcExp e + let elemType = mkArrayType baseType pols + check (tyE == elemType) $ + "Expression " ++ prettyPrint e + ++ " in array initializer has type " ++ prettyPrint tyE + ++ " but array expects elements of type " ++ prettyPrint elemType + return pE +tcVarInit baseType pols (InitArray _ arr) = do + tcArrayInit baseType pols arr + return bottom + +evalMaybePol :: Maybe (Policy ()) -> Tc r TcPolicy +evalMaybePol = maybe (return bottom) (liftCont . evalPolicy) + +-------------------------- -- Field Access tcFieldAccess :: FieldAccess () -> Tc r (TcType, TcPolicy) tcFieldAccess (PrimaryFieldAccess _ e fi) = do (tyE,pE) <- tcExp e - VSig tyF pFi _ _ <- lookupFieldT tyE fi - return (tyF, pE `join` pFi) + case tyE of + -- Ugly hack to get the oft-used "length" function working + TcRefT (TcArrayT tyElem pElem) -> + if fi == Ident () "length" + then return (intT, pE) + else fail $ "Unsupported array field: " ++ prettyPrint fi + + _ -> do + VSig tyF pFi _ _ <- lookupFieldT tyE fi + return (tyF, pE `join` pFi) + +tcFieldAccess fa = error $ "Unsupported field access: " ++ prettyPrint fa -------------------------- -- Method invocations diff --git a/src/Language/Java/Paragon/TypeCheck/TcStmt.hs b/src/Language/Java/Paragon/TypeCheck/TcStmt.hs --- a/src/Language/Java/Paragon/TypeCheck/TcStmt.hs +++ b/src/Language/Java/Paragon/TypeCheck/TcStmt.hs @@ -253,32 +253,57 @@ -- Rule BLOCKSTMT tcBlockStmts (BlockStmt _ stmt : bss) = tcStmt stmt >> tcBlockStmts bss --- Rule LOCALVARINIT -tcBlockStmts (LocalVars _ ms t [VarDecl _ (VarId _ i) (Just (InitExp _ e))] : bss) = do - (tyE, pE) <- tcExp e +-- Rule LOCALVARINIT/LOCALVARDECL +tcBlockStmts (LocalVars _ ms t vds : bss) = do + pV <- localVarPol ms tyV <- liftCont $ evalSrcType t +-- debugTc $ "Array type pre: " ++ prettyPrint t + tcLocalVars pV tyV (isFinal ms) vds $ tcBlockStmts bss + +tcBlockStmts (b:bss) = fail $ "Unsupported block statement: " ++ prettyPrint b + + + +tcLocalVars :: TcPolicy -> TcType -> Bool -> [VarDecl ()] -> Tc r () -> Tc r () +tcLocalVars _ _ _ [] cont = cont + + +-- Rule LOCALVARDECL +tcLocalVars pV tyV fin (VarDecl _ (VarId _ i) Nothing:vds) cont = do + tyV' <- if tyV == actorT + then actorIdT <$> newActorId i + else return tyV + extendVarEnv i (VSig tyV' pV False fin) $ do + tcLocalVars pV tyV fin vds cont + +-- Rule LOCALVARINIT (Exp) +tcLocalVars pV tyV fin (VarDecl _ (VarId _ i) (Just (InitExp _ e)):vds) cont = do + (tyE, pE) <- tcExp e checkM (liftCont $ tyE <: tyV) $ "Type mismatch: " ++ prettyPrint tyE ++ " <=> " ++ prettyPrint tyV - pV <- localVarPol ms + constraintLS pE pV tyV' <- case mActorId tyE of Nothing -> return tyV Just aid -> do newActorIdWith i aid return $ actorIdT aid - extendVarEnv i (VSig tyV' pV False (isFinal ms)) $ do - tcBlockStmts bss + extendVarEnv i (VSig tyV' pV False fin) $ + tcLocalVars pV tyV fin vds cont --- Rule LOCALVARDECL -tcBlockStmts (LocalVars _ ms t [VarDecl _ (VarId _ i) Nothing] : bss) = do - tyV <- liftCont $ evalSrcType t - pV <- localVarPol ms - tyV' <- if tyV == actorT - then actorIdT <$> newActorId i - else return tyV - extendVarEnv i (VSig tyV' pV False (isFinal ms)) $ do - tcBlockStmts bss - -tcBlockStmts (b:bss) = fail $ "Unsupported block statement: " ++ prettyPrint b +-- Rule LOCALVARINIT (Array) +tcLocalVars pV tyV fin (VarDecl _ (VarId _ i) (Just (InitArray _ arr)):vds) cont = do + case mArrayType tyV of + Just (tyA, pAs) -> do +-- debugTc $ "Array type post: " ++ prettyPrint tyV + tcArrayInit tyA pAs arr + extendVarEnv i (VSig tyV pV False fin) $ + tcLocalVars pV tyV fin vds cont + + Nothing -> fail $ "Variable " ++ prettyPrint i + ++ " of non-array type " ++ prettyPrint tyV + ++ " given literal array initializer" + + localVarPol :: [Modifier ()] -> Tc r TcPolicy localVarPol ms = diff --git a/src/Language/Java/Paragon/TypeCheck/Types.hs b/src/Language/Java/Paragon/TypeCheck/Types.hs --- a/src/Language/Java/Paragon/TypeCheck/Types.hs +++ b/src/Language/Java/Paragon/TypeCheck/Types.hs @@ -24,7 +24,7 @@ data TcRefType = TcClsRefT TcClassType - | TcArrayT TcType (Maybe TcPolicy) + | TcArrayT TcType TcPolicy | TcTypeVar (Ident ()) deriving (Eq, Ord, Show, Data, Typeable) @@ -87,8 +87,13 @@ clsTypeToType :: TcClassType -> TcType clsTypeToType = TcRefT . TcClsRefT +arrayType :: TcType -> TcPolicy -> TcType +arrayType = (TcRefT .) . TcArrayT +mkArrayType :: TcType -> [TcPolicy] -> TcType +mkArrayType = foldr (flip arrayType) + ----------------------------------- -- Destructors @@ -139,6 +144,12 @@ isPolicyType :: TcType -> Bool isPolicyType = isJust . mPolicyPol +mArrayType :: TcType -> Maybe (TcType, [TcPolicy]) +mArrayType (TcRefT (TcArrayT ty p)) = Just $ + case mArrayType ty of + Nothing -> (ty, [p]) + Just (ty, ps) -> (ty, p:ps) +mArrayType _ = Nothing ------------------------------------------- -- Type operations @@ -214,9 +225,16 @@ pretty tcrt = case tcrt of TcClsRefT ct -> pretty ct - TcArrayT t mp -> pretty t <> text "[]" <> maybe empty pretty mp + TcArrayT {} -> let (bt, suff) = ppArrayType (TcRefT tcrt) in bt <> suff TcTypeVar i -> pretty i +ppArrayType :: TcType -> (Doc, Doc) +ppArrayType (TcRefT (TcArrayT ty pol)) = + let (bt, suff) = ppArrayType ty + in (bt, text "[]" <> char '<' <> pretty pol <> char '>' <> suff) +ppArrayType ty = (pretty ty, empty) + + instance Pretty TcClassType where pretty (TcClassT iargs) = hcat . punctuate (char '.') $ map (\(i,tas) -> pretty i <> ppTypeParams tas) iargs @@ -228,6 +246,7 @@ pretty (TcActualLockState ls) = text "lock[]" <+> ppArgs ls instance Pretty TcPolicy where + pretty (TcPolicy []) = braces $ char ':' pretty (TcPolicy cs) = braces $ hcat (punctuate (char ';') $ map pretty cs) pretty (TcPolicyVar mv) = pretty mv pretty (TcRigidVar i) = text "policyof" <> parens (pretty i)