diff --git a/paragon.cabal b/paragon.cabal --- a/paragon.cabal +++ b/paragon.cabal @@ -1,5 +1,5 @@ Name: paragon -Version: 0.1.26 +Version: 0.1.27 License: BSD3 License-File: LICENSE Author: Niklas Broberg @@ -33,7 +33,7 @@ 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 + uniplate == 1.6, directory, filepath, haskell-src-meta, th-lift, template-haskell if flag(base4) Build-depends: base >= 4 && < 5, syb cpp-options: -DBASE4 diff --git a/src/Language/Java/Paragon/Interaction.hs b/src/Language/Java/Paragon/Interaction.hs --- a/src/Language/Java/Paragon/Interaction.hs +++ b/src/Language/Java/Paragon/Interaction.hs @@ -49,7 +49,7 @@ issueTracker = "http://code.google.com/p/paragon-java/issues/entry" versionString :: String -versionString = "0.1.26" +versionString = "0.1.27" libraryBase, typeCheckerBase :: String libraryBase = "Language.Java.Paragon" 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 @@ -1,4 +1,4 @@ -{-# LANGUAGE CPP, PatternGuards #-} +{-# LANGUAGE CPP, PatternGuards, TupleSections #-} module Language.Java.Paragon.Parser ( parser, @@ -43,13 +43,14 @@ import Language.Java.Paragon.Syntax import Language.Java.Paragon.Pretty (prettyPrint) import Language.Java.Paragon.Interaction +import Language.Java.Paragon.Monad.Base import Text.ParserCombinators.Parsec import Text.ParserCombinators.Parsec.Pos import Prelude hiding ( exp, catch, (>>), (>>=) ) import qualified Prelude as P ( (>>), (>>=) ) -import Data.Maybe ( isJust, catMaybes ) +import Data.Maybe ( isJust, catMaybes, fromJust ) --import Control.Monad ( ap ) import Control.Applicative ( (<$>) ) --import Control.Arrow ( first ) @@ -768,7 +769,7 @@ condExp :: P (Exp ()) condExp = do - ie <- infixExp + ie <- fixPrecs <$> infixExp -- TODO: precedence resolution ces <- list condExpSuffix return $ foldl (\a s -> s a) ie ces @@ -1177,18 +1178,26 @@ <|> tok KW_P_Actor >> return (ActorT ()) <|> tok KW_P_Policy >> return (PolicyT ()) + refType :: P (RefType ()) -refType = +refType = checkNoExtraEnd refTypeE + +refTypeE :: P (RefType (), Int) +refTypeE = {- trace "refTypeE" -} ( (do pt <- primType mps <- list1 arrPols - return $ ArrayType () (PrimType () pt) mps) + return $ (ArrayType () (PrimType () pt) mps, 0)) <|> - (do ct <- classType - mps <- list arrPols + (do (ct, e) <- classTypeE let baseType = ClassRefType () ct - case mps of - [] -> return baseType - _ -> return $ ArrayType () (RefType () baseType) mps) "refType" + if (e == 0) + then do + mps <- list arrPols + case mps of + [] -> return (baseType, e) + _ -> return $ (ArrayType () (RefType () baseType) mps, 0) + else return (baseType, e) + ) "refType") arrPols :: P (Maybe (Policy ())) arrPols = do @@ -1201,20 +1210,18 @@ nonArrayType = PrimType () <$> primType <|> RefType () <$> ClassRefType () <$> classType + classType :: P (ClassType ()) -classType = do - n <- nameRaw tName - tas <- lopt typeArgs - return $ ClassType () n tas ---classType = ClassType () <$> seplist1 classTypeSpec period +classType = checkNoExtraEnd classTypeE -{- -classTypeSpec :: P (Ident (), [TypeArgument ()]) -classTypeSpec = do - i <- ident - tas <- lopt typeArgs - return (i, tas) --} +classTypeE :: P (ClassType (), Int) +classTypeE = {- trace "classTypeE" $ -} do + n <- nameRaw tName + mtase <- opt typeArgsE + {- trace ("mtase: " ++ show mtase) $ -} + case mtase of + Just (tas, e) -> return (ClassType () n tas, e) + Nothing -> return (ClassType () n [] , 0) returnType :: P (ReturnType ()) returnType = tok KW_Void >> return (VoidType ()) <|> @@ -1242,36 +1249,51 @@ bounds :: P [RefType ()] bounds = tok KW_Extends >> seplist1 refType (tok Op_And) +checkNoExtraEnd :: P (a, Int) -> P a +checkNoExtraEnd pai = do + (a, e) <- pai + check (e == 0) "Unexpected >" + return a + typeArgs :: P [TypeArgument ()] -typeArgs = tok Op_LThan {- < -} >> typeArgsSuffix +typeArgs = {- trace "typeArgs" $ -} checkNoExtraEnd typeArgsE -typeArgsSuffix :: P [TypeArgument ()] -typeArgsSuffix = +typeArgsE :: P ([TypeArgument ()], Int) +typeArgsE = {- trace "typeArgsE" $ -} + do tok Op_LThan {- < -} + (as, extra) <- typeArgsSuffix + return (as, extra-1) + +typeArgsSuffix :: P ([TypeArgument ()], Int) +typeArgsSuffix = {- trace "typeArgsSuffix" $ -} (do tok Op_Query wcArg <- Wildcard () <$> opt wildcardBound - rest <- typeArgsEnd - return $ wcArg:rest) <|> + (rest, e) <- typeArgsEnd 0 + return $ (wcArg:rest, e)) <|> (do lArg <- ActualArg () <$> parens (ActualLockState () <$> seplist1 lock comma) - rest <- typeArgsEnd - return $ lArg:rest) <|> - (try $ do rt <- refType - rest <- typeArgsEnd + (rest, e) <- typeArgsEnd 0 + return (lArg:rest, e)) <|> + (try $ do (rt, er) <- refTypeE + (rest, e) <- typeArgsEnd er let tArg = case nameOfRefType rt of Just n -> ActualName () $ ambName $ flattenName n -- keep as ambiguous _ -> ActualType () rt - return $ (ActualArg () tArg):rest) <|> + return $ (ActualArg () tArg:rest, e)) <|> (do eArg <- ActualArg () . ActualExp () <$> argExp - rest <- typeArgsEnd - return $ eArg:rest) + (rest, e) <- typeArgsEnd 0 + return (eArg:rest, e)) where nameOfRefType :: RefType () -> Maybe (Name ()) nameOfRefType (ClassRefType _ (ClassType _ n tas)) = if null tas then Just n else Nothing nameOfRefType _ = Nothing -typeArgsEnd :: P [TypeArgument ()] -typeArgsEnd = - (tok Op_GThan {- > -} >> return []) <|> +typeArgsEnd :: Int -> P ([TypeArgument ()], Int) -- Int for the number of "extra" > +typeArgsEnd n | n > 0 = {- trace ("typeArgsEnd-1: " ++ show n) $ -} return ([], n) +typeArgsEnd _ = {- trace ("typeArgsEnd-2: ") $ -} + (tok Op_GThan {- > -} >> return ([], 1)) <|> + (tok Op_RShift {- >> -} >> return ([], 2)) <|> + (tok Op_RRShift {- >>> -} >> return ([], 3)) <|> (tok Comma >> typeArgsSuffix) argExp :: P (Exp ()) @@ -1558,3 +1580,35 @@ actIs = [ i | ActorParam _ i <- pars ] polIs = [ i | PolicyParam _ i <- pars ] +-------------------------------------------------------------- +-- Resolving precedences + +builtInPrecs :: [(Op (), Int)] +builtInPrecs = + map (,9) [Mult (), Div (), Rem () ] ++ + map (,8) [Add (), Sub () ] ++ + map (,7) [LShift (), RShift (), RRShift () ] ++ + map (,6) [LThan (), GThan (), LThanE (), GThanE ()] ++ + map (,5) [Equal (), NotEq () ] ++ + [(And (), 4), + (Or (), 3), + (Xor (), 2), + (CAnd (), 1), + (COr (), 0)] + +instanceOfPrec :: Int +instanceOfPrec = 6 -- same as comparison ops + +fixPrecs :: Exp () -> Exp () +fixPrecs (BinOp _ a op2 z) = + let e = fixPrecs a -- recursively fix left subtree + getPrec op = fromJust $ lookup op builtInPrecs + fixup p1 p2 y pre = + if p1 >= p2 + then BinOp () e op2 z -- already right order + else pre (fixPrecs $ BinOp () y op2 z) + in case e of + BinOp _ x op1 y -> fixup (getPrec op1) (getPrec op2) y (BinOp () x op1) + InstanceOf _ y rt -> fixup instanceOfPrec (getPrec op2) y (flip (InstanceOf ()) rt) + _ -> BinOp () e op2 z +fixPrecs e = e 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 @@ -395,8 +395,13 @@ mapM_ (typeCheckPolicyMod st) rPolExps rPol <- getReadPolicy ms check (Final () `elem` ms || (not $ includesThis rPol)) $ - "Non-final field may not reference " ++ prettyPrint (thisP :: PrgPolicy TcActor) + prettyPrint (thisP :: PrgPolicy TcActor) ++ + " may not be used as the policy of non-final fields" + check (not $ typeIncludesThis ty) $ + prettyPrint (thisP :: PrgPolicy TcActor) ++ + " may not be used in the type arguments of a field type" + -- 3. Add signature to typemap return $ VSig { varType = ty, @@ -414,6 +419,26 @@ tm { fields = Map.insert i vti (fields tm) } addField _ vd = \_ -> fail $ "Deprecated declaration: " ++ prettyPrint vd + typeIncludesThis :: TcType -> Bool + typeIncludesThis (TcRefT rt) = refTypeIncludesThis rt + typeIncludesThis _ = False + + refTypeIncludesThis :: TcRefType -> Bool + refTypeIncludesThis rTy = + case rTy of + TcArrayT arrTy arrPol -> + typeIncludesThis arrTy || includesThis arrPol + TcClsRefT (TcClassT _ targs) -> + any argIncludesThis targs + _ -> False + + argIncludesThis :: TcTypeArg -> Bool + argIncludesThis targ = + case targ of + TcActualType rt -> refTypeIncludesThis rt + TcActualPolicy p -> includesThis p + _ -> False + -- Methods typeCheckSignature st (MethodDecl _ ms tps retT i ps exns _mb) tcba | not (Typemethod () `elem` ms) = do @@ -769,7 +794,7 @@ env = CodeEnv { vars = Map.fromList parVsigs, lockstate = expLs, - returnI = error "Cannot return from constructor", + returnI = Just (voidT, top), exnsE = Map.fromList exnPols, branchPCE = (branchMap, [(pWri, writeErr)]), parBounds = pBs diff --git a/src/Language/Java/Paragon/TypeCheck/Constraints.hs b/src/Language/Java/Paragon/TypeCheck/Constraints.hs --- a/src/Language/Java/Paragon/TypeCheck/Constraints.hs +++ b/src/Language/Java/Paragon/TypeCheck/Constraints.hs @@ -25,11 +25,14 @@ splitCstrs :: Constraint -> [Constraint] -splitCstrs (LRT bs g ls p q) = map (\x -> LRT bs g ls x q) (disjoin p) - where disjoin :: (TcPolicy TcActor) -> [TcPolicy TcActor] +splitCstrs (LRT bs g ls p q) = [ LRT bs g ls x y | x <- disjoin p, y <- dismeet q ] + where disjoin, dismeet :: (TcPolicy TcActor) -> [TcPolicy TcActor] disjoin (Join p1 p2) = (disjoin p1)++(disjoin p2) disjoin (Meet p1 _p2) = disjoin p1 -- TODO: Ugly strategy!! disjoin p' = [p'] + dismeet (Meet p1 p2) = (dismeet p1)++(dismeet p2) + dismeet (Join p1 _p2) = dismeet p1 -- TODO: Ugly strategy!! + dismeet p' = [p'] 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 @@ -176,7 +176,10 @@ debugPrint $ "lookupPrefixName: " ++ prettyPrint i ++ " :: " ++ show sty tm <- getTypeMap case lookupTypeOfStateT sty tm of - Right newSig -> return (Just sty, instThis p $ tMembers newSig, p) + Right newSig -> do + debugPrint $ "\nSig before instantiation: " ++ show (tMembers newSig) + debugPrint $ "Sig after instantiation: " ++ show (instThis p (tMembers newSig)) ++ "\n" + return (Just sty, instThis p $ tMembers newSig, p) Left (Just err) -> fail err _ -> panic (monadModule ++ ".lookupPrefixName") $ "Unknown variable or field: " ++ show n @@ -195,7 +198,7 @@ -- debugPrint $ show (packages baseTm2) ++ "\n" sty <- getStateType (Just n) mPreSty ty case lookupTypeOfStateT sty baseTm2 of - Right tsig -> return (Just sty, tMembers tsig, prePol `joinWThis` p) + Right tsig -> return (Just sty, instThis p $ tMembers tsig, prePol `joinWThis` p) Left (Just err) -> fail err _ -> panic (monadModule ++ ".lookupPrefixName") $ "Unknown type: " ++ show ty @@ -625,20 +628,17 @@ updateStateType :: Maybe (Name ()) -- field/var name (if decidable) -> Maybe (TcType) -- Containing object type -> TcType -- field/var/cell type - -> Maybe TcStateType -- rhs state type (Nothing if no init) + -> TcStateType -- rhs state type -> TcCodeM TcStateType -updateStateType mN mTyO tyV mSty | tyV == actorT = do - case mSty of - Just sty | Just aid <- mActorId sty -> do - maybeM mTyO $ \tyO -> scrambleActors (Just tyO) - maybeM mN $ \n -> setActorId n aid - return sty - - | otherwise -> panic (monadModule ++ ".updateStateType") - $ "Actor state but non-actor target type: " - ++ show (tyV, sty) - Nothing -> panic (monadModule ++ ".updateStateType") - $ "No state for actor assignment: " ++ show mN +updateStateType mN mTyO tyV sty | tyV == actorT = do + case mActorId sty of + Just aid -> do + maybeM mTyO $ \tyO -> scrambleActors (Just tyO) + maybeM mN $ \n -> setActorId n aid + return sty + _ -> panic (monadModule ++ ".updateStateType") + $ "Actor state but non-actor target type: " + ++ show (tyV, sty) -- TODO {- @@ -646,11 +646,20 @@ case mSty of Just sty | Just pbs <- mPolicyPol sty -> do -} -updateStateType _mN _mTyO ty _mSty | isPrimType (stateType ty) = return $ stateType ty -updateStateType _mN _mTyO _ty (Just sty) = return sty -- BOGUS!!! -updateStateType _mN _mTyO ty Nothing = return $ stateType ty +updateStateType _mN _mTyO ty _sty | isPrimType (stateType ty) = return $ stateType ty +updateStateType mN _mTyO ty sty + | Just ct <- mClassType ty = + case sty of + TcInstance _ aids -> return $ TcInstance ct aids + _ | isNullType sty -> TcInstance ct <$> getInstanceActors mN ct + _ | isArrayType sty -> return $ TcInstance ct [] + _ -> panic (monadModule ++ ".updateStateType") + $ "Class type target but no instance type" + ++ show (ty, sty) +updateStateType _mN _mTyO _ty sty = return sty -- BOGUS!!! + -- Instance Analysis getInstanceActors :: Maybe (Name ()) -> TcClassType -> TcCodeM [ActorId] @@ -815,8 +824,6 @@ bs <- getParamPolicyBounds case lrt bs g ls p q of Left b -> do --- debugTc $ "constraint: p1: " ++ show p1 --- debugTc $ "constraint: p2: " ++ show p2 -- st <- getState check b (str {-++ "\n\nState: " ++ show st -}) Right c -> addConstraint c str diff --git a/src/Language/Java/Paragon/TypeCheck/Monad/TcDeclM.hs b/src/Language/Java/Paragon/TypeCheck/Monad/TcDeclM.hs --- a/src/Language/Java/Paragon/TypeCheck/Monad/TcDeclM.hs +++ b/src/Language/Java/Paragon/TypeCheck/Monad/TcDeclM.hs @@ -673,7 +673,7 @@ evalSrcRefType (TypeVariable _ i) = return $ TcTypeVar i evalSrcRefType (ArrayType _ t mps) = do ty <- evalSrcType t - pols <- mapM (maybe (return bottom) evalPolicy) mps + pols <- map RealPolicy <$> mapM (maybe (return bottom) evalPolicy) mps let (TcRefT arrTy) = mkArrayType ty pols return arrTy evalSrcRefType (ClassRefType _ ct) = TcClsRefT <$> evalSrcClsType ct diff --git a/src/Language/Java/Paragon/TypeCheck/Policy.hs b/src/Language/Java/Paragon/TypeCheck/Policy.hs --- a/src/Language/Java/Paragon/TypeCheck/Policy.hs +++ b/src/Language/Java/Paragon/TypeCheck/Policy.hs @@ -15,7 +15,7 @@ import Language.Java.Paragon.Syntax import Language.Java.Paragon.Pretty -import Language.Java.Paragon.Interaction +--import Language.Java.Paragon.Interaction import Language.Java.Paragon.TypeCheck.Actors import Language.Java.Paragon.TypeCheck.Locks @@ -32,8 +32,8 @@ flowAtomString :: String flowAtomString = "$FLOW$" -policyModule :: String -policyModule = typeCheckerBase ++ ".Policy" +--policyModule :: String +--policyModule = typeCheckerBase ++ ".Policy" --------------------------------------------------------------- -- Basic policies @@ -65,8 +65,9 @@ type AtomPolicy = TcPolicy TcAtom data TcMetaVar a = TcMetaVar Int (Ident ()) + deriving (Data, Typeable, Eq, Ord, Show) -- deriving (Data, Typeable) - +{- instance Data (TcMetaVar a) where gunfold = panic (policyModule ++ ": instance Data TcMetaVar (gunfold)") "Meta variables should never be reified" @@ -87,7 +88,7 @@ instance Show (TcMetaVar a) where show (TcMetaVar i _) = "$$" ++ show i - +-} data TcClause a = TcClause a [TcAtom] deriving (Eq,Ord,Show,Data,Typeable) @@ -117,7 +118,7 @@ pretty (VarPolicy mv) = pretty mv instance Pretty (TcMetaVar a) where - pretty (TcMetaVar i _) = text ("$$" ++ show i) + pretty (TcMetaVar k i) = text "$$" <> pretty i <> text (show k) instance Pretty a => Pretty (TcClause a) where pretty (TcClause h b) = pretty h <> char ':' <+> hcat (punctuate (char ',') $ map pretty b) 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 @@ -153,14 +153,14 @@ " has policy " ++ prettyPrint pA ++ "\n" ++ "Index: " ++ prettyPrint iE ++ "\n" ++ " has policy " ++ prettyPrint pI - constraint [] pA (RealPolicy pElem) $ + constraint [] pA pElem $ "Cannot update element in array resulting from expression " ++ prettyPrint arrE ++ ": policy of elements must be no less restrictive than that of the " ++ "array itself when updating\n" ++ "Array policy: " ++ prettyPrint pA ++ "\n" ++ "Element policy: " ++ prettyPrint pElem - return (tyElem, RealPolicy pElem, Just $ unStateType tyA, Nothing, Nothing, + return (tyElem, pElem, Just $ unStateType tyA, Nothing, Nothing, ArrayLhs (Just tyElem) (ArrayIndex (Just tyElem) arrE' iE')) _ -> fail $ "Cannot index non-array expression " ++ prettyPrint arrE @@ -175,7 +175,8 @@ -- Check all the necessary constraints: -- TODO: Check that _op is allowed on tyV checkM (tyV =<: tyRhs) $ - "Type mismatch: " ++ prettyPrint tyRhs ++ " <=> " ++ prettyPrint tyV + "Type mismatch: " ++ prettyPrint (unStateType tyRhs) ++ + " <=> " ++ prettyPrint tyV -- Check: E[branchPC](n) <= pV bpcs <- maybe getBranchPC_ getBranchPC mEnt constraintPC bpcs pV $ \p src -> @@ -199,7 +200,7 @@ -- "be less restrictive than the policy of the object\n" ++ -- " - styV <- updateStateType mN mtyO tyV (Just tyRhs) + styV <- updateStateType mN mtyO tyV tyRhs -- Update actor tracker if applicable {- -- TODO: This should go into updateStateType maybeM (mActorId tyRhs) $ \aid -> do @@ -231,7 +232,9 @@ extendBranchPC pC ("conditional expression dependent on expression " ++ prettyPrint c) $ do ((ty1, p1, e1'), (ty2, p2, e2')) <- (maybeM (mLocks tyC) (\ls -> applyLockMods ([], ls)) >> tcExp e1) ||| tcExp e2 - check (ty1 == ty2) $ "Types of branches don't match" + check (ty1 == ty2 + || isNullType ty1 && isRefType ty2 + || isNullType ty2 && isRefType ty1) $ "Types of branches don't match" return (ty1, pC `join` p1 `join` p2, Cond (toT ty1) c' e1' e2') @@ -299,7 +302,7 @@ check canCast $ "Wrong type at cast" when (canExn) $ -- TODO: could throw ClassCastException return () - styC <- updateStateType Nothing Nothing tyC (Just tyE) + styC <- updateStateType Nothing Nothing tyC tyE return (styC, pE, Cast (Just tyC) (notAppl t) e') tcExp (FieldAccess _ fa) = do @@ -325,35 +328,35 @@ -- Check that the remaining dimexprs each conform to -- the policy given at the level outside it (polEDims, dimEsRest) <- checkDimExprs [] [] dimEsPsRest - =<< evalMaybePol mDimP1 + =<< (RealPolicy <$> evalMaybePol mDimP1) -- Evaluate given policies for implicit dimensions - polIDims <- mapM evalMaybePol dimImplPs + polIDims <- map RealPolicy <$> mapM evalMaybePol dimImplPs -- Return the array type, and the policy of the outermost dimexpr - let ty = mkArrayType baseTy (polEDims ++ polIDims) + let ty = mkArrayType baseTy $ (polEDims ++ polIDims) dimPs' = map (fmap notAppl) $ snd $ unzip dimEsPs dimEsPs' = zip (dimE1':dimEsRest) dimPs' dimImplPs' = map (fmap notAppl) dimImplPs return (stateType ty, pol1, ArrayCreate (Just ty) (notAppl bt) dimEsPs' dimImplPs') - where checkDimExprs :: [PrgPolicy TcActor] -- Accumulated policies of earlier dimensions + where checkDimExprs :: [ActorPolicy] -- Accumulated policies of earlier dimensions -> [Exp T] -- Accumulated annotated expressions -> [(Exp (), Maybe (Policy ()))] -- Remaining dimexprs/pols - -> PrgPolicy TcActor -- Policy of previous dimension - -> TcCodeM ([PrgPolicy TcActor], [Exp T]) + -> ActorPolicy -- Policy of previous dimension + -> TcCodeM ([ActorPolicy], [Exp T]) checkDimExprs accP accE [] pPrev = return $ (reverse (pPrev:accP), reverse accE) checkDimExprs accP accE ((e,mp):emps) pPrev = do (tyE,pE,e') <- tcExp e check (isIntConvertible tyE) $ nonIntErr tyE -- Each dimexpr must satisfy the policy of the outer dim - constraintLS pE (RealPolicy pPrev) $ + constraintLS pE pPrev $ "Array dimension expression has too restrictive policy:\n" ++ "Expression: " ++ prettyPrint e ++ "\n" ++ " with policy: " ++ prettyPrint pE ++ "\n" ++ "Declared policy bound: " ++ prettyPrint pPrev - pNext <- evalMaybePol mp + pNext <- RealPolicy <$> evalMaybePol mp checkDimExprs (pPrev:accP) (e':accE) emps pNext nonIntErr :: TcStateType -> String @@ -364,7 +367,7 @@ tcExp (ArrayCreateInit _ bt dimImplPs arrInit) = do baseTy <- liftTcDeclM $ evalSrcType bt -- Evaluate given policies for implicit (all) dimensions - dimPols <- mapM evalMaybePol dimImplPs + dimPols <- map RealPolicy <$> mapM evalMaybePol dimImplPs -- Check that the initializer has the right type and policies -- of subexpressions arrInit' <- tcArrayInit baseTy dimPols arrInit @@ -385,7 +388,7 @@ "Non-integral expression of type " ++ prettyPrint tyI ++ " used as array index expression" styElem <- getStateType Nothing Nothing tyElem - return (styElem, RealPolicy pElem `join` pA `join` pI, + return (styElem, pElem `join` pA `join` pI, ArrayAccess (Just tyElem) (ArrayIndex (Just tyElem) arrE' iE')) _ -> fail $ "Cannot index non-array expression " ++ prettyPrint arrE @@ -397,10 +400,10 @@ -------------------------- -- Array initializers -tcArrayInit :: TcType -> [PrgPolicy TcActor] -> TypeCheck TcCodeM ArrayInit +tcArrayInit :: TcType -> [ActorPolicy] -> TypeCheck TcCodeM ArrayInit tcArrayInit baseType (pol1:pols) (ArrayInit _ inits) = do (ps, inits') <- unzip <$> mapM (tcVarInit baseType pols) inits - mapM_ (\(p,e) -> constraintLS p (RealPolicy pol1) $ + mapM_ (\(p,e) -> constraintLS p pol1 $ "Expression in array initializer has too restrictive policy:\n" ++ "Expression: " ++ prettyPrint e ++ " with policy: " ++ prettyPrint p ++ @@ -409,7 +412,7 @@ return $ ArrayInit Nothing inits' tcArrayInit _ [] _ = fail $ "Array initializer has too many dimensions" -tcVarInit :: TcType -> [PrgPolicy TcActor] -> VarInit () -> TcCodeM (ActorPolicy, VarInit T) +tcVarInit :: TcType -> [ActorPolicy] -> VarInit () -> TcCodeM (ActorPolicy, VarInit T) tcVarInit baseType pols (InitExp _ e) = do -- debugPrint $ "Pols: " ++ show pols -- debugPrint $ "Exp: " ++ show e 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 @@ -220,7 +220,8 @@ tyP <- liftTcDeclM $ evalSrcType t -- TODO check tyP <: "Throwable" pR <- liftTcDeclM $ getReadPolicy ms -- getParamPolicy i ms - pW <- newMetaPolVar i -- \pi, where \pi is fresh + pW <- newMetaPolVar (Ident () $ prettyPrint t) + -- \pi, where \pi is fresh addBranchPC (exnE tyP) $ -- E' = E[branchPC{tyP +-> bottom}, registerExn tyP (RealPolicy pR) pW $ do -- exns{tyP +-> (pR, \pi)}] block' <- tcBlock block @@ -418,7 +419,8 @@ debugPrint $ "\n## " ++ prettyPrint vd0 ++ " ##\n" (tyE, pE, e') <- tcExp e checkM (tyV =<: tyE) $ - "Type mismatch: " ++ prettyPrint tyE ++ " <=> " ++ prettyPrint tyV + "Type mismatch: " ++ prettyPrint (unStateType tyE) ++ + " <=> " ++ prettyPrint tyV constraintLS pE pV $ "Cannot assign result of expression " ++ prettyPrint e ++ " with policy " ++ prettyPrint pE ++ diff --git a/src/Language/Java/Paragon/TypeCheck/TypeMap.hs b/src/Language/Java/Paragon/TypeCheck/TypeMap.hs --- a/src/Language/Java/Paragon/TypeCheck/TypeMap.hs +++ b/src/Language/Java/Paragon/TypeCheck/TypeMap.hs @@ -128,7 +128,7 @@ packages = Map.empty } -hardCodedArrayTM :: TcType -> PrgPolicy TcActor -> TypeSig +hardCodedArrayTM :: TcType -> ActorPolicy -> TypeSig hardCodedArrayTM ty p = let memTM = emptyTM { fields = Map.fromList [(Ident () "length", VSig intT thisP False False True)] 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 @@ -44,7 +44,7 @@ data TcRefType = TcClsRefT TcClassType - | TcArrayT TcType (PrgPolicy TcActor) + | TcArrayT TcType ActorPolicy | TcTypeVar (Ident ()) | TcNullT deriving (Eq, Ord, Show, Data, Typeable) @@ -129,10 +129,10 @@ clsTypeToType :: TcClassType -> TcType clsTypeToType = TcRefT . TcClsRefT -arrayType :: TcType -> PrgPolicy TcActor -> TcType +arrayType :: TcType -> ActorPolicy -> TcType arrayType = (TcRefT .) . TcArrayT -mkArrayType :: TcType -> [PrgPolicy TcActor] -> TcType +mkArrayType :: TcType -> [ActorPolicy] -> TcType mkArrayType = foldr (flip arrayType) @@ -196,7 +196,10 @@ isPolicyType :: TcStateType -> Bool isPolicyType = isJust . mPolicyPol -mArrayType :: TcType -> Maybe (TcType, [PrgPolicy TcActor]) +isArrayType :: TcStateType -> Bool +isArrayType = isJust . mArrayType . unStateType + +mArrayType :: TcType -> Maybe (TcType, [ActorPolicy]) mArrayType (TcRefT (TcArrayT ty p)) = Just $ case mArrayType ty of Nothing -> (ty, [p]) @@ -332,7 +335,7 @@ TcPolicyPolT p -> text "policy[" <> pretty p <> text "]" TcLockT ls -> (hsep $ text "lock[" : punctuate (text ",") (map pretty ls)) <> text "]" TcInstance ct aids -> pretty ct <> - (hsep $ char '[' : punctuate (char ',') (map pretty aids)) <> char ']' + (hsep $ char '{' : punctuate (char ',') (map pretty aids)) <> char '}' TcType ty -> pretty ty instance Pretty TcType where