paragon 0.1.10 → 0.1.11
raw patch · 14 files changed
+350/−89 lines, 14 files
Files
- paragon.cabal +5/−2
- src/Language/Java/Paragon.hs +2/−2
- src/Language/Java/Paragon/Parser.hs +25/−17
- src/Language/Java/Paragon/Pretty.hs +26/−12
- src/Language/Java/Paragon/QuasiQuoter/Derive.hs +27/−0
- src/Language/Java/Paragon/Syntax.hs +8/−4
- src/Language/Java/Paragon/TypeCheck.hs +14/−5
- src/Language/Java/Paragon/TypeCheck/Evaluate.hs +8/−7
- src/Language/Java/Paragon/TypeCheck/Monad.hs +16/−8
- src/Language/Java/Paragon/TypeCheck/Monad/TcBase.hs +9/−2
- src/Language/Java/Paragon/TypeCheck/Monad/TcCont.hs +15/−3
- src/Language/Java/Paragon/TypeCheck/TcExp.hs +132/−8
- src/Language/Java/Paragon/TypeCheck/TcStmt.hs +42/−17
- src/Language/Java/Paragon/TypeCheck/Types.hs +21/−2
paragon.cabal view
@@ -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
src/Language/Java/Paragon.hs view
@@ -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
src/Language/Java/Paragon/Parser.hs view
@@ -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 ())
src/Language/Java/Paragon/Pretty.hs view
@@ -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 '>'
+ src/Language/Java/Paragon/QuasiQuoter/Derive.hs view
@@ -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]+
src/Language/Java/Paragon/Syntax.hs view
@@ -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,
src/Language/Java/Paragon/TypeCheck.hs view
@@ -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) $
src/Language/Java/Paragon/TypeCheck/Evaluate.hs view
@@ -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
src/Language/Java/Paragon/TypeCheck/Monad.hs view
@@ -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
src/Language/Java/Paragon/TypeCheck/Monad/TcBase.hs view
@@ -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)
src/Language/Java/Paragon/TypeCheck/Monad/TcCont.hs view
@@ -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)
src/Language/Java/Paragon/TypeCheck/TcExp.hs view
@@ -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
src/Language/Java/Paragon/TypeCheck/TcStmt.hs view
@@ -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 =
src/Language/Java/Paragon/TypeCheck/Types.hs view
@@ -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)