Extended the type unification for Rain to support type-checking things that are being poisoned (which could be either end of a channel)

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 ["<mobile>"] >> 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 [")"]

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.

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
 

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

frontends/RainTypes.hs

@@ -39,13 +39,13 @@ import TypeUnification
 import UnifyType
 import Utils
 
-lookupMapElseMutVar :: UnifyIndex -> PassM (TypeExp A.Type)
+lookupMapElseMutVar :: A.TypeRequirements -> UnifyIndex -> PassM (TypeExp A.Type)
-lookupMapElseMutVar k
+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))
+      Left n -> lookupMapElseMutVar reqs (UnifyIndex (A.nameMeta n, Right n))
-      Right (m, i) -> lookupMapElseMutVar (UnifyIndex (m, Left i))
+      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 _ (Left n)) = lookup $ UnifyIndex (A.nameMeta n, Right n)
-    sub (A.UnknownVarType (Right (m,i))) = lookup $ UnifyIndex (m,Left i)
+    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

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)
+-- | Merges two lots of attributes into a union of the requirements
-prune t =
+mergeAttr :: A.TypeRequirements -> A.TypeRequirements -> A.TypeRequirements
- case t of
+mergeAttr (A.TypeRequirements p) (A.TypeRequirements p') = A.TypeRequirements (p || p')
-   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
 
-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
+  = do t1' <- prune Nothing te1
-       t2' <- liftIO $ prune te2
+       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

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)