diff --git a/common/ShowCode.hs b/common/ShowCode.hs index 94f9f02..d5db7d0 100644 --- a/common/ShowCode.hs +++ b/common/ShowCode.hs @@ -235,7 +235,7 @@ instance ShowOccam A.Type where showOccamM A.Any = tell ["ANY"] showOccamM (A.Timer _) = tell ["TIMER"] showOccamM A.Time = tell ["TIME"] - showOccamM (A.UnknownVarType en) + showOccamM (A.UnknownVarType _ en) = do tell ["(inferred type for: "] either showName (tell . (:[]) . show) en tell [")"] @@ -294,7 +294,7 @@ instance ShowRain A.Type where -- Mobility is not explicit in Rain, but we should indicate it: showRainM (A.Mobile t) = tell [""] >> showRainM t showRainM (A.List t) = tell ["["] >> showRainM t >> tell ["]"] - showRainM (A.UnknownVarType en) + showRainM (A.UnknownVarType _ en) = do tell ["(inferred type for: "] either showName (tell . (:[]) . show) en tell [")"] diff --git a/data/AST.hs b/data/AST.hs index 52c1799..821912a 100644 --- a/data/AST.hs +++ b/data/AST.hs @@ -132,12 +132,16 @@ data Type = | Infer -- | A type that will be inferred by type unification. Either for a named -- variable, or for an anonymous, uniquely identified, expression - | UnknownVarType (Either Name (Meta, Int)) + | UnknownVarType TypeRequirements (Either Name (Meta, Int)) -- | A numeric type to be inferred later, that must be able to hold the given -- value. The Int is a unique identifier, the Integer is the number to hold | UnknownNumLitType Meta Int Integer deriving (Show, Eq, Typeable, Data) +data TypeRequirements = TypeRequirements + { mustBePoisonable :: Bool } + deriving (Show, Eq, Typeable, Data) + -- | An array dimension. -- Depending on the context, an array type may have empty dimensions, which is -- why this isn't just an Expression. diff --git a/frontends/ParseRain.hs b/frontends/ParseRain.hs index 91024b5..ddbf3fa 100644 --- a/frontends/ParseRain.hs +++ b/frontends/ParseRain.hs @@ -225,7 +225,7 @@ listLiteral :: RainParser A.Expression listLiteral = try $ do m <- sLeftQ u <- getUniqueIdentifer - let t = A.List $ A.UnknownVarType (Right (m,u)) + let t = A.List $ A.UnknownVarType (A.TypeRequirements False) (Right (m,u)) (do try sRightQ return $ A.Literal m t $ A.ListLiteral m [] <|> do e0 <- try expression @@ -270,7 +270,8 @@ range = try $ do m <- sLeftQ (A.Conversion mc A.DefaultConversion t begin) (A.Conversion mc A.DefaultConversion t end) Nothing -> do u <- getUniqueIdentifer - let t = A.List $ A.UnknownVarType (Right (m,u)) + let t = A.List $ A.UnknownVarType (A.TypeRequirements + False) (Right (m,u)) return $ A.ExprConstr m $ A.RangeConstr m t begin end diff --git a/frontends/ParseRainTest.hs b/frontends/ParseRainTest.hs index f685192..17247ed 100644 --- a/frontends/ParseRainTest.hs +++ b/frontends/ParseRainTest.hs @@ -69,10 +69,10 @@ m :: Meta m = emptyMeta inferVarType :: String -> A.Type -inferVarType = A.UnknownVarType . Left . simpleName +inferVarType = A.UnknownVarType (A.TypeRequirements False) . Left . simpleName inferExpType :: A.Type -inferExpType = A.UnknownVarType $ Right $ (emptyMeta, 818181) +inferExpType = A.UnknownVarType (A.TypeRequirements False) $ Right $ (emptyMeta, 818181) -- In the parser, integer literals have an unknown type: intLiteral :: Integer -> A.Expression diff --git a/frontends/RainTypes.hs b/frontends/RainTypes.hs index 8a5850a..21a3af6 100644 --- a/frontends/RainTypes.hs +++ b/frontends/RainTypes.hs @@ -39,13 +39,13 @@ import TypeUnification import UnifyType import Utils -lookupMapElseMutVar :: UnifyIndex -> PassM (TypeExp A.Type) -lookupMapElseMutVar k +lookupMapElseMutVar :: A.TypeRequirements -> UnifyIndex -> PassM (TypeExp A.Type) +lookupMapElseMutVar reqs k = do st <- get let m = csUnifyLookup st case Map.lookup k m of Just v -> return v - Nothing -> do r <- liftIO $ newIORef Nothing + Nothing -> do r <- liftIO $ newIORef (reqs, Nothing) let UnifyIndex (mt,_) = k v = MutVar mt r m' = Map.insert k v m @@ -66,10 +66,10 @@ typeToTypeExp m (A.Chan A.DirInput at t) = ttte m "?" (A.Chan A.DirInput at) t typeToTypeExp m (A.Chan A.DirOutput at t) = ttte m "!" (A.Chan A.DirOutput at) t typeToTypeExp m (A.Chan A.DirUnknown at t) = ttte m "channel" (A.Chan A.DirUnknown at) t typeToTypeExp m (A.Mobile t) = ttte m "MOBILE" A.Mobile t -typeToTypeExp _ (A.UnknownVarType en) +typeToTypeExp _ (A.UnknownVarType reqs en) = case en of - Left n -> lookupMapElseMutVar (UnifyIndex (A.nameMeta n, Right n)) - Right (m, i) -> lookupMapElseMutVar (UnifyIndex (m, Left i)) + Left n -> lookupMapElseMutVar reqs (UnifyIndex (A.nameMeta n, Right n)) + Right (m, i) -> lookupMapElseMutVar reqs (UnifyIndex (m, Left i)) typeToTypeExp _ (A.UnknownNumLitType m id n) = do r <- liftIO . newIORef $ Left [(m,n)] let v = NumLit m r @@ -101,6 +101,7 @@ performTypeUnification = rainOnlyPass "Rain Type Checking" <.< markParamPass <.< markAssignmentTypes <.< markCommTypes + <.< markPoisonTypes <.< markReplicators <.< markExpressionTypes $ x @@ -129,8 +130,8 @@ substituteUnknownTypes :: Map.Map UnifyIndex A.Type -> PassType substituteUnknownTypes mt = applyDepthM sub where sub :: A.Type -> PassM A.Type - sub (A.UnknownVarType (Left n)) = lookup $ UnifyIndex (A.nameMeta n, Right n) - sub (A.UnknownVarType (Right (m,i))) = lookup $ UnifyIndex (m,Left i) + sub (A.UnknownVarType _ (Left n)) = lookup $ UnifyIndex (A.nameMeta n, Right n) + sub (A.UnknownVarType _ (Right (m,i))) = lookup $ UnifyIndex (m,Left i) sub (A.UnknownNumLitType m i _) = lookup $ UnifyIndex (m, Left i) sub t = return t @@ -244,6 +245,16 @@ markConditionalTypes = checkDepthM2 checkWhile checkIf checkIf c@(A.Choice m exp _) = markUnify exp A.Bool +-- | Marks types in poison statements +markPoisonTypes :: PassType +markPoisonTypes = checkDepthM checkPoison + where + checkPoison :: Check A.Process + checkPoison (A.InjectPoison m ch) + = do u <- getUniqueIdentifer + markUnify ch $ A.UnknownVarType (A.TypeRequirements True) $ Right (m, u) + checkPoison _ = return () + -- | Checks the types in inputs and outputs, including inputs in alts markCommTypes :: PassType markCommTypes = checkDepthM2 checkInputOutput checkAltInput diff --git a/frontends/TypeUnification.hs b/frontends/TypeUnification.hs index b8f6ac7..7578d7b 100644 --- a/frontends/TypeUnification.hs +++ b/frontends/TypeUnification.hs @@ -45,6 +45,8 @@ foldCon con es = case splitEither es of -- Pearl (2001)", citeseer: http://citeseer.ist.psu.edu/451401.html -- This in turn was taken from Luca Cardelli's "Basic Polymorphic Type Checking" +-- | Given a map from keys to non-unified types and a list of pairs of types to unify, +-- gives back the resulting map from keys to actual types. unifyRainTypes :: forall k. (Ord k, Show k) => (Map.Map k (TypeExp A.Type)) -> [(k, k)] -> PassM (Map.Map k A.Type) unifyRainTypes m' prs @@ -57,8 +59,10 @@ unifyRainTypes m' prs Nothing -> error $ "Could not find type for variable in map before unification: " ++ show s + -- | Given a map containing simplified types (no mutvar/pointers or numlits + -- remaining, just actual types), turns them into the actual type representations stToMap :: Map.Map k (TypeExp A.Type) -> PassM (Map.Map k A.Type) - stToMap m = do m' <- liftIO $ mapMapWithKeyM (\k v -> prune v >>= read k) m + stToMap m = do m' <- mapMapWithKeyM (\k v -> prune Nothing v >>= liftIO . read k) m let (mapOfErrs, mapOfRes) = Map.mapEitherWithKey (const id) m' case Map.elems mapOfErrs of ((m,e):_) -> dieP m e @@ -70,7 +74,7 @@ unifyRainTypes m' prs case foldCon con (map (either (Left . snd) Right) vals') of Left e -> return $ Left (m, e) Right x -> return $ Right x - read k (MutVar m v) = readIORef v >>= \t -> case t of + read k (MutVar m v) = readIORef v >>= \(_,t) -> case t of Nothing -> return $ Left (m, "Type error in unification, " ++ "ambigious type remains for: " ++ show k) Just t' -> read k t' @@ -80,7 +84,7 @@ unifyRainTypes m' prs Right t -> return $ Right t fromTypeExp :: TypeExp A.Type -> PassM A.Type -fromTypeExp x = fromTypeExp' =<< (liftIO $ prune x) +fromTypeExp x = fromTypeExp' =<< prune Nothing x where fromTypeExp' :: TypeExp A.Type -> PassM A.Type fromTypeExp' (MutVar m _) = dieP m "Unresolved type" @@ -103,41 +107,65 @@ giveErr m msg tx ty y <- showInErr ty dieP m $ msg ++ x ++ " and " ++ y -prune :: Typeable a => TypeExp a -> IO (TypeExp a) -prune t = - case t of - MutVar _ r -> - do m <- readIORef r - case m of - Nothing -> return t - Just t2 -> - do t' <- prune t2 - writeIORef r (Just t') - return t' - _ -> return t +-- | Merges two lots of attributes into a union of the requirements +mergeAttr :: A.TypeRequirements -> A.TypeRequirements -> A.TypeRequirements +mergeAttr (A.TypeRequirements p) (A.TypeRequirements p') = A.TypeRequirements (p || p') -occursInType :: Typeable a => Ptr a -> TypeExp a -> IO Bool +-- | Checks the attributes match a non-mutvar variable +checkAttrMatch :: A.TypeRequirements -> TypeExp A.Type -> PassM () +checkAttrMatch (A.TypeRequirements False) _ = return () -- no need to check +checkAttrMatch (A.TypeRequirements True) (NumLit m _) + = dieP m "Numeric literal can never be poisonable" +checkAttrMatch (A.TypeRequirements True) t@(OperType m str _ _) + = case str of + "?" -> return () + "!" -> return () + _ -> do err <- showInErr t + dieP m $ "Type cannot be poisoned: " ++ err + +-- | Reduces chains of MutVars down to just a single pointer. +prune :: Maybe A.TypeRequirements -> TypeExp A.Type -> PassM (TypeExp A.Type) +prune attr mv@(MutVar m r) + = do (attr', x) <- liftIO $ readIORef r + let merged = maybe attr' (mergeAttr attr') attr + case x of + Nothing -> do liftIO $ writeIORef r (merged, Nothing) + return mv + Just t2 -> + do t' <- prune (Just merged) t2 + liftIO $ writeIORef r (merged, Just t') + return t' +prune Nothing t = return t +prune (Just attr) t = checkAttrMatch attr t >> return t + +-- | Checks if the given pointer occurs in the given type, returning True if so. +-- Used to stop the type checker performing infinite loops around a type-cycle. +occursInType :: Ptr A.Type -> TypeExp A.Type -> PassM Bool occursInType r t = - do t' <- prune t + do t' <- prune Nothing t case t' of MutVar _ r2 -> return $ r == r2 GenVar _ n -> return False OperType _ _ _ ts -> mapM (occursInType r) ts >>* or +-- | Unifies two types, giving an error if it's not possible unifyType :: TypeExp A.Type -> TypeExp A.Type -> PassM () unifyType te1 te2 - = do t1' <- liftIO $ prune te1 - t2' <- liftIO $ prune te2 + = do t1' <- prune Nothing te1 + t2' <- prune Nothing te2 case (t1',t2') of (MutVar _ r1, MutVar _ r2) -> if r1 == r2 then return () - else liftIO $ writeIORef r1 (Just t2') + else do attr <- liftIO $ readIORef r1 >>* fst + attr' <- liftIO $ readIORef r2 >>* fst + liftIO $ writeIORef r1 (mergeAttr attr attr', Just t2') (MutVar m r1, _) -> - do b <- liftIO $ occursInType r1 t2' + do b <- occursInType r1 t2' if b then dieP m "Infinitely recursive type formed" - else liftIO $ writeIORef r1 (Just t2') + else do attr <- liftIO $ readIORef r1 >>* fst + liftIO $ writeIORef r1 (attr, Just t2') (_,MutVar {}) -> unifyType t2' t1' (GenVar m x,GenVar _ y) -> if x == y then return () else dieP m $ "different template variables" @@ -190,6 +218,7 @@ instantiate ts x = case x of OperType m nm f xs -> OperType m nm f (map (instantiate ts) xs) GenVar _ n -> ts !! n +-- | Checks if the given number will fit in the given type willFit :: A.Type -> Integer -> Bool willFit t n = case bounds t of Just (l,h) -> l <= n && n <= h diff --git a/frontends/UnifyType.hs b/frontends/UnifyType.hs index 782bc23..692d697 100644 --- a/frontends/UnifyType.hs +++ b/frontends/UnifyType.hs @@ -24,7 +24,7 @@ import Data.IORef import qualified AST as A import Metadata -type Ptr a = IORef (Maybe (TypeExp a)) +type Ptr a = IORef (A.TypeRequirements, Maybe (TypeExp a)) data Typeable a => TypeExp a = MutVar Meta (Ptr a)