module Language.Java.Paragon.TypeCheck.TcExp where import Language.Java.Paragon.Syntax import Language.Java.Paragon.Pretty import Language.Java.Paragon.Interaction import Language.Java.Paragon.TypeCheck.Policy import Language.Java.Paragon.TypeCheck.Actors import Language.Java.Paragon.TypeCheck.Locks import Language.Java.Paragon.TypeCheck.Monad.TcCodeM import Language.Java.Paragon.TypeCheck.Monad import Language.Java.Paragon.TypeCheck.Types import Language.Java.Paragon.TypeCheck.TypeMap import Data.List ( (\\) ) import Data.Maybe (fromJust) import qualified Data.Map as Map import Control.Applicative ( (<$>) ) import Control.Arrow ( first ) tcExpModule :: String tcExpModule = typeCheckerBase ++ ".TcExp" --import qualified Data.Map as Map ----------------------------------- -- Types of literal values -- ----------------------------------- litType :: Literal () -> TcType litType (Int _ _) = intT litType (Word _ _) = longT litType (Float _ _) = floatT litType (Double _ _) = doubleT litType (Boolean _ _) = booleanT litType (Char _ _) = charT litType (String _ _) = stringT litType (Null _ ) = nullT --litType l = error $ "litType: " ++ show l ----------------------------------- -- Checking expressions -- ----------------------------------- --debugTc str = liftIO $ putStrLn $ "DEBUG: Tc: " ++ str --debugTc _ = return () tcExp :: Exp () -> TcCodeM r (TcType, TcPolicy) -- Rule PAREN tcExp (Paren _ e) = tcExp e -- Rule LIT tcExp (Lit _ l) = return (litType l, bottom) -- Rule THIS tcExp (This _) = do ty <- getThisType --debugPrint $ "getThisType: " ++ show ty return (ty, bottom) -- Rule BINOP tcExp (BinOp _ e1 op e2) = do (ty1, p1) <- tcExp e1 (ty2, p2) <- tcExp e2 tyRes <- opType op ty1 ty2 return (tyRes, p1 `join` p2) -- Rule VAR/FIELD tcExp (ExpName _ n) = case n of Name _ EName mPre i -> do (ty1, pol, _) <- lookupVar mPre i ty <- case ty1 of TcPrimT (PolicyT _) -> policyPolT <$> getPolicy n TcPrimT (ActorT _) -> actorIdT <$> getActorId n _ -> return ty1 return (ty, pol) Name _ LName mPre i -> do LSig pL arL <- lookupLock mPre i check (arL == 0) $ "Lock " ++ prettyPrint n ++ " expects " ++ show arL ++ " arguments but has been given none." return $ (lockT [TcLock n []], pL) _ -> panic (tcExpModule ++ ".tcExp:ExpName") $ "Unexpected name: " ++ show n -- Rule VARASS/FIELDASS tcExp ex@(Assign _ lhs _op rhs) = do debugPrint $ prettyPrint ex (tyV, pV, mtyO, mEnt, mN) <- case lhs of NameLhs _ n@(Name _ EName mPre iF) -> do case mPre of Nothing -> do -- VARASS (tyV, pV, _) <- lookupVar Nothing iF return (tyV, pV, Nothing, Just (varE n), Just n) Just pre -> do -- FIELDASS (Just tyO, tmO, pO) <- lookupPrefixName pre case Map.lookup iF $ fields tmO of Just (VSig tyF pF _ _ _) -> do constraint [] pO pF $ "Cannot update field " ++ prettyPrint iF ++ " of object " ++ prettyPrint pre ++ ": policy of field must be no less restrictive than that of the " ++ "object when updating\n" ++ "Object policy: " ++ prettyPrint pO ++ "\n" ++ "Field policy: " ++ prettyPrint pF return (tyF, pF, Just tyO, Just (varE n), Just n) Nothing -> fail $ "Object " ++ prettyPrint pre ++ " of type " ++ prettyPrint tyO ++ " does not have a field named " ++ prettyPrint iF NameLhs _ n -> panic (tcExpModule ++ ".tcEcp:Assign") $ "NameLhs not an EName: " ++ show n FieldLhs _ (PrimaryFieldAccess _ e fi) -> do (tyE, pE) <- tcExp e (VSig tyF pF _ _ _) <- lookupFieldT tyE fi let eEnt = case e of This _ -> Just $ thisFE fi _ -> Nothing constraint [] pE pF $ "Cannot update field " ++ prettyPrint fi ++ " of object resulting from expression " ++ prettyPrint e ++ ": policy of field must be no less restrictive than that of the " ++ "object when updating\n" ++ "Object policy: " ++ prettyPrint pE ++ "\n" ++ "Field policy: " ++ prettyPrint pF return (tyF, pF, Just tyE, 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 $ "When assigning into an array, the policy on the index " ++ "expression may be no more restrictive than the policy of " ++ "the array itself\n" ++ "Array: " ++ prettyPrint arrE ++ "\n" ++ " has policy " ++ prettyPrint pA ++ "\n" ++ "Index: " ++ prettyPrint iE ++ "\n" ++ " has policy " ++ prettyPrint pI 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, pElem, Just tyA, Nothing, Nothing) _ -> fail $ "Cannot index non-array expression " ++ prettyPrint arrE ++ " of type " ++ prettyPrint tyA _ -> fail $ "Lhs not supported: " ++ prettyPrint lhs (tyRhs, pRhs) <- tcExp rhs -- Check all the necessary constraints: -- TODO: Check that _op is allowed on tyV checkM (tyRhs <: tyV) $ "Type mismatch: " ++ prettyPrint tyRhs ++ " <=> " ++ prettyPrint tyV -- Check: E[branchPC](n) <= pV bpcs <- maybe getBranchPC_ getBranchPC mEnt constraintPC bpcs pV $ \p src -> "Assignment to " ++ prettyPrint lhs ++ " with policy " ++ prettyPrint pV ++ " not allowed in " ++ src ++ " with write effect bound " ++ prettyPrint p -- Check: exnPC(S) <= pV epcs <- getExnPC constraintPC epcs pV $ \p src -> "Assignment to " ++ prettyPrint lhs ++ " with policy " ++ prettyPrint pV ++ " not allowed in " ++ src ++ " with write effect bound " ++ prettyPrint p -- Check: pRhs <= pV modulo L constraintLS pRhs pV $ "Cannot assign result of expression " ++ prettyPrint rhs ++ " with policy " ++ prettyPrint pRhs ++ " to location " ++ prettyPrint lhs ++ " with policy " ++ prettyPrint pV -- Check: pO <= pV, if pO exists -- maybeM mpO (\pO -> constraint [] pO pV $ -- "When changing the state of an object, the policy of the changed field may not " ++ -- "be less restrictive than the policy of the object\n" ++ -- " -- Update actor tracker if applicable maybeM (mActorId tyRhs) $ \aid -> do maybeM mtyO $ \tyO -> scrambleActors (Just tyO) maybeM mN $ \n -> setActorId n aid return (tyV, pV) -- Rule CALL tcExp (MethodInv _ mi) = tcMethodOrLockInv mi -- Rule NEW tcExp e@(InstanceCreation _ tas ct args Nothing) = do -- debugPrint $ "tcExp: " ++ show e tyT <- liftTcDeclM $ evalSrcClsType ct -- DEBUG --debugPrint $ "Type: " ++ show tyT --tm <- getTypeMap --let tyTm = lookupTypeOfT (clsTypeToType tyT) tm --debugPrint $ "TypeMap: " ++ show (Map.keys $ constrs tyTm) -- END DEBUG (tysArgs, psArgs) <- unzip <$> mapM tcExp args (tps,genCti) <- lookupConstr tyT tysArgs -- TODO: Check that the arguments in tyT -- match those expected by the type -- TODO: Type argument inference check (length tps == length tas) $ "Wrong number of type arguments in instance creation expression.\n" ++ "Constructor expects " ++ show (length tps) ++ " arguments but has been given " ++ show (length tas) tArgs <- liftTcDeclM $ mapM (uncurry evalSrcTypeArg) (zip tps tas) -- tm <- getTypeMap let cti = instantiate (zip tps tArgs) genCti let (CSig psPars pW lExp lMods exns) = cti -- Check lockstates l <- getCurrentLockState check (null (lExp \\ l)) $ "Lockstate too weak when calling constructor " ++ prettyPrint ct ++ ":\n" ++ "Required lock state: " ++ prettyPrint lExp ++ "\n" ++ "Current lock state: " ++ prettyPrint l -- Check argument constraints mapM_ (\(arg,argP,parP) -> constraintLS argP parP $ "Constructor applied to argument with too restrictive policy:\n" ++ "Constructor expression: " ++ prettyPrint e ++ "\n" ++ "Argument: " ++ prettyPrint arg ++ " with policy: " ++ prettyPrint argP ++ "Declared policy bound: " ++ prettyPrint parP ) (zip3 args psArgs psPars) -- Check E[branchPC](*) <= pW bpcs <- getBranchPC_ constraintPC bpcs pW $ \p src -> "Constructor " ++ prettyPrint ct ++ " with declared write effect " ++ prettyPrint pW ++ " not allowed in " ++ src ++ " with write effect bound " ++ prettyPrint p -- Check exnPC(S) <= pW epc <- getExnPC constraintPC epc pW $ \p src -> "Constructor " ++ prettyPrint ct ++ " with declared write effect " ++ prettyPrint pW ++ " not allowed in " ++ src ++ " with write effect bound " ++ prettyPrint p -- Check Exns(X)[write] <= E[exns](X)[write] AND -- Check Exns(X)[read] >= E[exns](X)[read] mapM_ (uncurry $ exnConsistent (Right ct)) exns -- Fix outgoing state let exns' = map (first ExnType) exns activateExns exns' -- ==> S' = Sn[exns{X +-> (Sx, exns(X)[write])}] applyLockMods lMods -- ==> S'' = S'[lockMods ||>>= lMods, scrambleActors Nothing -- ==> actors scrambled] return (clsTypeToType tyT, bottom) -- Rule COND tcExp (Cond _ c e1 e2) = do (tyC, pC) <- tcExp c checkM (tyC <: booleanT) $ "Cannot convert type to boolean" extendBranchPC pC ("conditional expression dependent on expression " ++ prettyPrint c) $ do ((ty1, p1), (ty2, p2)) <- (maybeM (mLocks tyC) (\ls -> applyLockMods ([], ls)) >> tcExp e1) ||| tcExp e2 check (ty1 == ty2) $ "Types of branches don't match" return (ty1, pC `join` p1 `join` p2) tcExp (PolicyExp _ pl) = do pRep <- tcPolicyExp pl return (policyPolT pRep, bottom) tcExp (PostIncrement _ e) = do (tyE, pE) <- tcExp e check (isNumConvertible tyE) $ "Post-increment operator used at non-numeric type " ++ prettyPrint tyE return (tyE, pE) tcExp (PostDecrement _ e) = do (tyE, pE) <- tcExp e check (isNumConvertible tyE) $ "Post-decrement operator used at non-numeric type " ++ prettyPrint tyE return (tyE, pE) tcExp (PreIncrement _ e) = do (tyE, pE) <- tcExp e check (isNumConvertible tyE) $ "Pre-increment operator used at non-numeric type " ++ prettyPrint tyE return (tyE, pE) tcExp (PreDecrement _ e) = do (tyE, pE) <- tcExp e check (isNumConvertible tyE) $ "Pre-decrement operator used at non-numeric type " ++ prettyPrint tyE return (tyE, pE) -- Unary promotion prefix operator -- Rule PREP tcExp (PrePlus _ e) = do (tyE, pE) <- tcExp e check (isNumConvertible tyE) $ "Pre-plus operator used at non-numeric type " ++ prettyPrint tyE return (unaryNumPromote_ tyE, pE) tcExp (PreMinus _ e) = do (tyE, pE) <- tcExp e check (isNumConvertible tyE) $ "Pre-minus operator used at non-numeric type " ++ prettyPrint tyE return (unaryNumPromote_ tyE, pE) tcExp (PreBitCompl _ e) = do (tyE, pE) <- tcExp e check (isIntConvertible tyE) $ "Pre-complement bit operator used at non-integral type " ++ prettyPrint tyE return (unaryNumPromote_ tyE, pE) tcExp (PreNot _ e) = do (tyE, pE) <- tcExp e check (isBoolConvertible tyE) $ "Pre-complement boolean operator used at non-boolean type " ++ prettyPrint tyE return (booleanT, pE) tcExp (Cast _ t e) = do (tyE, pE) <- tcExp e tyC <- liftTcDeclM $ evalSrcType t checkM (tyE <: tyC) $ "Wrong type at cast" return (tyC, pE) tcExp (FieldAccess _ fa) = tcFieldAccess fa -- Arrays tcExp (ArrayCreate _ bt dimEsPs dimImplPs) = do baseTy <- liftTcDeclM $ 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 [] dimEsPsRest =<< 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] -- Accumulated policies of earlier dimensions -> [(Exp (), Maybe (Policy ()))] -- Remaining dimexprs/pols -> TcPolicy -- Policy of previous dimension -> TcCodeM 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 $ "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 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 <- liftTcDeclM $ 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 $ " " -- Not true: pI just adds to the outgoing level return (tyElem, pElem `join` pA `join` pI) _ -> 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 () -> TcCodeM r () tcArrayInit baseType (pol1:pols) (ArrayInit _ inits) = do ps <- mapM (tcVarInit baseType pols) inits mapM_ (\(p,e) -> constraintLS p pol1 $ "Expression in array initializer has too restrictive policy:\n" ++ "Expression: " ++ prettyPrint e ++ " with policy: " ++ prettyPrint p ++ "Declared policy bound: " ++ prettyPrint pol1 ) (zip ps inits) tcArrayInit _ [] _ = fail $ "Array initializer has too many dimensions" tcVarInit :: TcType -> [TcPolicy] -> VarInit () -> TcCodeM r TcPolicy tcVarInit baseType pols (InitExp _ e) = do -- debugPrint $ "Pols: " ++ show pols -- debugPrint $ "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 ()) -> TcCodeM r TcPolicy evalMaybePol = maybe (return bottom) (liftTcDeclM . evalPolicy) -------------------------- -- Field Access tcFieldAccess :: FieldAccess () -> TcCodeM r (TcType, TcPolicy) tcFieldAccess (PrimaryFieldAccess _ e fi) = do (tyE,pE) <- tcExp e 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 -- | Check a method invocation, which could possibly represent -- a lock query expression. tcMethodOrLockInv :: MethodInvocation () -> TcCodeM r (TcType, TcPolicy) tcMethodOrLockInv (MethodCallOrLockQuery _ (Name _ MOrLName mPre i) args) = do -- We couldn't resolve without type information whether -- this truly is a method or a lock. baseTm <- getTypeMap preTm <- case mPre of Nothing -> return baseTm Just pre -> do (_, preTm, _) <- lookupPrefixName pre return preTm let nt = case Map.lookup i $ locks preTm of Just _ -> LName Nothing -> MName tcMethodOrLockInv (MethodCallOrLockQuery () (Name () nt mPre i) args) tcMethodOrLockInv (MethodCallOrLockQuery _ nam@(Name _ LName mPre i) args) = do -- This is a lock query LSig pL arL <- lookupLock mPre i check (arL == length args) $ "Lock " ++ prettyPrint nam ++ " expects " ++ show arL ++ " arguments but has been given " ++ show (length args) (tysArgs, psArgs) <- unzip <$> mapM tcExp args mapM_ (\ty -> check (isActorType ty) $ "Trying to query lock with argument of type " ++ prettyPrint ty ++ "\n" ++ "All arguments to lock query must be of type actor") tysArgs let tyR = lockT [TcLock nam $ map (fromJust . mActorId) tysArgs] return (tyR, foldl1 join (pL:psArgs)) tcMethodOrLockInv mi = tcMethodInv mi -- | Check a true method invocation tcMethodInv :: MethodInvocation () -> TcCodeM r (TcType, TcPolicy) tcMethodInv mi = do debugPrint $ "tcMethodInv: " ++ prettyPrint mi (n, msig, args, psArgs, pE) <- case mi of MethodCallOrLockQuery _ n@(Name _ MName mPre i) args -> do -- This is a true method call (tysArgs, psArgs) <- unzip <$> mapM tcExp args (pPath, tps, msig) <- lookupMethod mPre i tysArgs check (null tps) $ "Method " ++ prettyPrint i ++ " expects " ++ show (length tps) ++ " type arguments but has been\ \ given 0" return $ (n, msig, args, psArgs, pPath) MethodCallOrLockQuery _ n _ -> panic (tcExpModule ++ ".tcMethodInv") $ "Unexpected name: " ++ show n PrimaryMethodCall _ e tas i args -> do (tyE, pE) <- tcExp e (tysArgs, psArgs) <- unzip <$> mapM tcExp args (tps, genMSig) <- lookupMethodT tyE i tysArgs tArgs <- liftTcDeclM $ mapM (uncurry evalSrcTypeArg) $ zip tps (map (ActualArg ()) tas) let msig = instantiate (zip tps tArgs) genMSig return $ (mkSimpleName MName i, msig, args, psArgs, pE) _ -> fail $ "tcMethodInv: Unsupported method call" let (MSig tyR pR psPars pW lExp lMods exns) = msig -- Check lockstates l <- getCurrentLockState check (null (lExp \\ l)) $ "Lockstate too weak when calling method " ++ prettyPrint n ++ ":\n" ++ "Required lock state: " ++ prettyPrint lExp ++ "\n" ++ "Current lock state: " ++ prettyPrint l -- Check argument constraints mapM_ (\(arg,argP,parP) -> constraintLS argP parP $ "Method applied to argument with too restrictive policy:\n" ++ "Method invocation: " ++ prettyPrint mi ++ "\n" ++ "Argument: " ++ prettyPrint arg ++ " with policy: " ++ prettyPrint argP ++ "Declared policy bound: " ++ prettyPrint parP ) (zip3 args psArgs psPars) -- Check E[branchPC](*) <= pW bpcs <- getBranchPC_ constraintPC bpcs pW $ \p src -> "Method " ++ prettyPrint n ++ " with declared write effect " ++ prettyPrint pW ++ " not allowed in " ++ src ++ " with write effect bound " ++ prettyPrint p -- Check exnPC(S) <= pW epc <- getExnPC constraintPC epc pW $ \p src -> "Method " ++ prettyPrint n ++ " with declared write effect " ++ prettyPrint pW ++ " not allowed in " ++ src ++ " with write effect bound " ++ prettyPrint p -- Check Exns(X)[write] <= E[exns](X)[write] AND -- Check Exns(X)[read] >= E[exns](X)[read] mapM_ (uncurry $ exnConsistent (Left n)) exns -- Fix outgoing state let exns' = map (first ExnType) exns activateExns exns' -- ==> S' = Sn[exns{X +-> (Sx, exns(X)[write])}] applyLockMods lMods -- ==> S'' = S'[lockMods ||>>= lMods, scrambleActors Nothing -- ==> actors scrambled] return (tyR, pE `join` pR) ----------------------------------- -- Policy expressions -- Treat them as pure compile-time for now tcPolicyExp :: PolicyExp () -> TcCodeM r TcPolicy tcPolicyExp (PolicyLit _ cs) = do tcCs <- mapM tcClause cs return $ TcPolicy tcCs tcPolicyExp pe@(PolicyOf _ i) = do (_, _, param) <- lookupVar Nothing i check param $ "policyof may only be used on parameters: " ++ prettyPrint pe return $ TcRigidVar i tcPolicyExp (PolicyTypeVar _ i) = do _ <- lookupVar Nothing i return $ TcRigidVar i tcPolicyExp (PolicyThis _) = return TcThis tcClause :: Clause () -> TcCodeM r (TcClause TcActor) tcClause (Clause _ h ats) = do tcH <- tcActor h tcAs <- mapM tcAtom ats return (TcClause tcH tcAs) tcAtom :: Atom () -> TcCodeM r TcAtom tcAtom (Atom _ n@(Name _ LName mPre i) as) = do (LSig _ ar) <- lookupLock mPre i check (length as == ar) $ "Arity mismatch in policy" tcAs <- mapM tcActor as return (TcAtom n tcAs) tcAtom (Atom _ n _) = panic (tcExpModule ++ ".tcAtom") $ "None-lock name: " ++ show n tcActor :: Actor () -> TcCodeM r TcActor tcActor (Var _ i) = return $ TcVar i tcActor (Actor _ n) = TcActor <$> tcActorName n tcActorName :: ActorName () -> TcCodeM r ActorId tcActorName (ActorName _ n) = getActorId n tcActorName (ActorTypeVar _ i) = return $ ActorTPVar i ----------------------------------- -- Types of operators -- ----------------------------------- opType :: Op () -> TcType -> TcType -> TcCodeM r TcType -- First the special cases: policy operators, and String conversion opType (Mult _) (TcPolicyPolT p1) (TcPolicyPolT p2) = return (TcPolicyPolT (p1 `join` p2)) opType (Add _) (TcPolicyPolT p1) (TcPolicyPolT p2) = return (TcPolicyPolT (p1 `meet` p2)) opType (Add _) t1 t2 | t1 == stringT || t2 == stringT = return stringT opType op t1 t2 -- Numeric operators | op `elem` (map ($()) [Mult, Div, Rem, Add, Sub]) = do check (isNumConvertible t1) $ "Numeric operator " ++ prettyPrint op ++ " used with non-numeric operand of type " ++ prettyPrint t1 check (isNumConvertible t2) $ "Numeric operator " ++ prettyPrint op ++ " used with non-numeric operand of type " ++ prettyPrint t2 return $ binaryNumPromote_ t1 t2 -- Shift operators | op `elem` (map ($()) [LShift, RShift, RRShift]) = do check (isIntConvertible t1) $ "Shift operator " ++ prettyPrint op ++ " used with non-integral operand of type " ++ prettyPrint t1 check (isIntConvertible t2) $ "Shift operator " ++ prettyPrint op ++ " used with non-integral operand of type " ++ prettyPrint t2 return $ unaryNumPromote_ t1 -- Relational operators | op `elem` (map ($()) [LThan, GThan, LThanE, GThanE]) = do check (isNumConvertible t1) $ "Numerical comparison operator " ++ prettyPrint op ++ " used with non-numeric operand of type " ++ prettyPrint t1 check (isNumConvertible t2) $ "Numerical comparison operator " ++ prettyPrint op ++ " used with non-numeric operand of type " ++ prettyPrint t2 return booleanT | op `elem` [Equal (), NotEq ()] = do case binaryNumPromote t1 t2 of Just _ -> return () _ | isBoolConvertible t1 && isBoolConvertible t2 -> return () | isRefType t1 && isRefType t2 -> return () _ -> fail $ "Equality operator " ++ prettyPrint op ++ " used with incomparable operands of types " ++ prettyPrint t1 ++ " and " ++ prettyPrint t2 return booleanT | op `elem` [And (), Or (), Xor ()] = if isBoolConvertible t1 then do check (isBoolConvertible t2) $ "Logical operator " ++ prettyPrint op ++ " used with non-boolean operand of type " ++ prettyPrint t2 return booleanT else if isIntConvertible t1 then do check (isIntConvertible t2) $ "Bitwise operator " ++ prettyPrint op ++ " used with non-integral operand of type " ++ prettyPrint t2 return $ binaryNumPromote_ t1 t2 else fail $ "Bitwise/logical operator " ++ prettyPrint op ++ " used with non-integral and non-boolean operand of type " ++ prettyPrint t1 | op `elem` [CAnd (), COr ()] = do check (isBoolConvertible t1) $ "Logical operator " ++ prettyPrint op ++ " used with non-boolean operand of type " ++ prettyPrint t1 check (isBoolConvertible t2) $ "Logical operator " ++ prettyPrint op ++ " used with non-boolean operand of type " ++ prettyPrint t2 return booleanT opType op _ _ = panic (tcExpModule ++ ".opType") $ show op {- splitName :: Name () -> (Maybe (Name ()), Name ()) splitName (Name _ is) = let (o,f) = (init is, last is) mo = if null o then Nothing else Just (Name () o) in (mo, Name () [f]) splitName _ = panic (tcExpModule ++ ".splitName") "AntiQName should not appear in AST being type-checked" -}