Rattus 0.3.1 → 0.4

raw patch · 15 files changed

+399/−290 lines, 15 filesdep +ghc-primdep ~basePVP ok

version bump matches the API change (PVP)

Dependencies added: ghc-prim

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• CHANGELOG.md +20/−0
• Rattus.cabal +12/−4
• docs/paper.pdf binary
• src/Rattus.hs +18/−21
• src/Rattus/Event.hs +28/−63
• src/Rattus/Events.hs +0/−81
• src/Rattus/Future.hs +115/−0
• src/Rattus/Plugin/Dependency.hs +13/−10
• src/Rattus/Plugin/ScopeCheck.hs +85/−64
• test/IllTyped.hs +21/−14
• test/MemoryLeak.hs +2/−4
• test/NewlyTyped.hs +52/−0
• test/Rewrite.hs +7/−8
• test/TimeLeak.hs +7/−9
• test/WellTyped.hs +19/−12

@@ -1,3 +1,23 @@+0.4+---++More general typing rules for delay, functions, and guarded recursion:++- delay and function definitions may now occur under a delay.+- Guarded recursive calls may occur at any time in the future -- not+  only exactly one time step into the future.+- As before, adv and recursive calls may only occur directly in the+  scope of delay. The scope of a delay is interrupted by adv, box,+  guarded recursive definitions, and function definitions.++Changes in the library:++- Rename applicative-style operators to avoid clash with Haskell's <*>+  operator.+- Rename types: Event -> Future; Events -> Event+++ 0.3.1 ----- 

@@ -1,6 +1,6 @@ cabal-version:       1.18 name:                Rattus-version:             0.3.1+version:             0.4 category:            FRP synopsis:            A modal FRP language description:@@ -139,7 +139,7 @@                        Rattus.Stream                        Rattus.Strict                        Rattus.Event-                       Rattus.Events+                       Rattus.Future                        Rattus.ToHaskell                        Rattus.Yampa                        @@ -153,7 +153,7 @@                        Rattus.Plugin.Utils                        Rattus.Plugin.Dependency                        Rattus.Plugin.StableSolver-  build-depends:       base >=4.12 && <5, containers, simple-affine-space, ghc >= 8.6 && < 8.11+  build-depends:       base >=4.12 && <5, containers, ghc >= 8.6 && < 8.11, ghc-prim, simple-affine-space   hs-source-dirs:      src   default-language:    Haskell2010   ghc-options:         -W@@ -180,7 +180,15 @@   main-is:             test/IllTyped.hs   default-language:    Haskell2010   build-depends:       Rattus, base-  ghc-options:         -fplugin=Rattus.Plugin -rtsopts+  ghc-options:         +                       -fplugin=Rattus.Plugin -rtsopts++Test-Suite newly-typed+  type:                exitcode-stdio-1.0+  main-is:             test/NewlyTyped.hs+  default-language:    Haskell2010+  build-depends:       Rattus, base+  ghc-options:         -fplugin=Rattus.Plugin   Test-Suite well-typed

binary file changed (622063 → 660739 bytes)

@@ -13,10 +13,10 @@   -- * Annotation   Rattus(..),   -- * Applicative operators-  (|*|),-  (|**),-  (<*>),-  (<**),+  (|#|),+  (|##),+  (<#>),+  (<##),   -- * box for stable types   box'   )@@ -26,32 +26,29 @@ import Rattus.Strict import Rattus.Primitives --import Prelude hiding ((<*>))- -- all functions in this module are in Rattus  {-# ANN module Rattus #-}   -- | Applicative operator for 'O'.-{-# INLINE (<*>) #-}-(<*>) :: O (a -> b) -> O a -> O b-f <*> x = delay (adv f (adv x))+{-# INLINE (<#>) #-}+(<#>) :: O (a -> b) -> O a -> O b+f <#> x = delay (adv f (adv x)) --- | Variant of '<*>' where the argument is of a stable type..-{-# INLINE (<**) #-}-(<**) :: Stable a => O (a -> b) -> a -> O b-f <** x = delay (adv f x)+-- | Variant of '<#>' where the argument is of a stable type..+{-# INLINE (<##) #-}+(<##) :: Stable a => O (a -> b) -> a -> O b+f <## x = delay (adv f x)  -- | Applicative operator for 'Box'.-{-# INLINE (|*|) #-}-(|*|) :: Box (a -> b) -> Box a -> Box b-f |*| x = box (unbox f (unbox x))+{-# INLINE (|#|) #-}+(|#|) :: Box (a -> b) -> Box a -> Box b+f |#| x = box (unbox f (unbox x)) --- | Variant of '|*|' where the argument is of a stable type..-{-# INLINE (|**) #-}-(|**) :: Stable a => Box (a -> b) -> a -> Box b-f |** x = box (unbox f x)+-- | Variant of '|#|' where the argument is of a stable type..+{-# INLINE (|##) #-}+(|##) :: Stable a => Box (a -> b) -> a -> Box b+f |## x = box (unbox f x)   -- | Variant of 'box' for stable types that can be safely used nested

@@ -1,17 +1,15 @@ {-# OPTIONS -fplugin=Rattus.Plugin #-}-{-# LANGUAGE TypeOperators #-} --- | Programming with single shot events, i.e. events that may occur at--- most once.+-- | Programming with many-shot events, i.e. events that may occur zero+-- or more times. + module Rattus.Event   ( map   , never   , switch   , switchTrans-  , whenJust-  , Event(..)-  , await+  , Event   , trigger   , triggerMap   )@@ -20,92 +18,59 @@  import Rattus import Rattus.Stream hiding (map)--import Prelude hiding ((<*>), map)+import qualified Rattus.Stream as Str +import Prelude hiding (map) --- | An event may either occur now or later.-data Event a = Now !a | Wait !(O (Event a))+-- | Events are simply streams of 'Maybe''s.+type Event a = Str (Maybe' a)  -- all functions in this module are in Rattus  {-# ANN module Rattus #-} --- | Apply a function to the value of the event (if it ever occurs).+-- | Apply a function to the values of the event (every time it occurs). {-# NOINLINE [1] map #-} map :: Box (a -> b) -> Event a -> Event b-map f (Now x) = Now (unbox f x)-map f (Wait x) = Wait (delay (map f) <*> x)+map f (Just' x ::: xs) =  (Just' (unbox f x)) ::: delay (map f (adv xs))+map f (Nothing' ::: xs) = Nothing' ::: delay (map f (adv xs))  -- | An event that will never occur. never :: Event a-never = Wait (delay never)-+never = Nothing' ::: delay never --- | @switch s e@ will behave like @s@ until the event @e@ occurs with--- value @s'@, in which case it will behave as @s'@.+-- | @switch s e@ will behave like @s@ but switches to @s'$ every time+-- the event 'e' occurs with some value @s'@. switch :: Str a -> Event (Str a) -> Str a-switch (x ::: xs) (Wait fas) = x ::: (delay switch <*> xs <*> fas)-switch _xs        (Now ys)   = ys ---- | Turn a stream of 'Maybe''s into an event. The event will occur--- whenever the stream has a value of the form @Just' v@, and the--- event then has value @v@.-firstJust :: Str (Maybe' a) -> Event a-firstJust (Just' x ::: _) = Now x-firstJust (Nothing' ::: xs) = Wait (delay firstJust <*> xs)---- | Turn a stream of 'Maybe''s into a stream of events. Each such--- event behaves as if created by 'firstJust'.-whenJust :: Str (Maybe' a) -> Str (Event a)-whenJust cur@(_ ::: xs) = firstJust cur ::: (delay whenJust <*> xs)+switch (x ::: xs) (Nothing' ::: fas) = x ::: delay (switch (adv xs)  (adv fas))+switch  _xs       (Just' (a ::: as) ::: fas)   = a ::: (delay switch <#> as <#> fas)   -- | Like 'switch' but works on stream functions instead of--- streams. That is, @switchTrans s e@ will behave like @s@ until the--- event @e@ occurs with value @s'@, in which case it will behave as+-- streams. That is, @switchTrans s e@ will behave like @s@ but+-- switches to @s'$ every time the event 'e' occurs with some value -- @s'@. switchTrans :: (Str a -> Str b) -> Event (Str a -> Str b) -> (Str a -> Str b) switchTrans f es as = switchTrans' (f as) es as  -- | Helper function for 'switchTrans'. switchTrans' :: Str b -> Event (Str a -> Str b) -> Str a -> Str b-switchTrans' (x ::: xs) (Wait fas) (_:::is) = x ::: (delay switchTrans' <*> xs <*> fas <*> is)-switchTrans' _xs        (Now ys)   is = ys is+switchTrans' (b ::: bs) (Nothing' ::: fs) (_:::as) = b ::: (delay switchTrans' <#> bs <#> fs <#> as)+switchTrans' _xs        (Just' f ::: fs)  as@(_:::as') = b' ::: (delay switchTrans' <#> bs' <#> fs <#> as')+  where (b' ::: bs') = f as --- | Helper function for 'await'.-await1 :: Stable a => a -> Event b -> Event (a :* b)-await1 a (Wait eb) = Wait (delay await1 <** a <*> eb)-await1 a (Now  b)  = Now  (a :* b) --- | Helper function for 'await'.-await2 :: Stable b => b -> Event a -> Event (a :* b)-await2 b (Wait ea) = Wait (delay await2 <** b <*> ea)-await2 b (Now  a)  = Now  (a :* b)---- | Synchronise two events. The resulting event occurs after both--- events have occurred (coinciding with whichever event occurred--- last.-await :: (Stable a, Stable b) => Event a -> Event b -> Event(a :* b)-await (Wait ea) (Wait eb)  = Wait (delay await <*> ea <*> eb)-await (Now a)   eb         = await1 a eb-await ea        (Now b)    = await2 b ea---- | Trigger an event as soon as the given predicate turns true on the--- given stream. The value of the event is the same as that of the+-- | Trigger an event as every time the given predicate turns true on+-- the given stream. The value of the event is the same as that of the -- stream at that time. trigger :: Box (a -> Bool) -> Str a -> Event a-trigger p (x ::: xs)-  | unbox p x  = Now x-  | otherwise  = Wait (delay (trigger p) <*> xs)-+trigger p (x ::: xs) = x' ::: (delay (trigger p) <#> xs)+  where x' = if unbox p x then Just' x else Nothing' --- | Trigger an event as soon as the given function produces a 'Just''+-- | Trigger an event every time the given function produces a 'Just'' -- value. triggerMap :: Box (a -> Maybe' b) -> Str a -> Event b-triggerMap f (x ::: xs) =-  case unbox f x of-    Just' y  -> Now y-    Nothing' -> Wait (delay (triggerMap f) <*> xs)+triggerMap = Str.map+  {-# RULES 

@@ -1,81 +0,0 @@-{-# OPTIONS -fplugin=Rattus.Plugin #-}---- | Programming with many-shot events, i.e. events that may occur zero--- or more times.---module Rattus.Events-  ( map-  , never-  , switch-  , switchTrans-  , Events-  , trigger-  , triggerMap-  )--where--import Rattus-import Rattus.Stream hiding (map)-import qualified Rattus.Stream as S--import Prelude hiding ((<*>), map)---- | Events are simply streams of 'Maybe''s.-type Events a = Str (Maybe' a)---- all functions in this module are in Rattus -{-# ANN module Rattus #-}---- | Apply a function to the values of the event (every time it occurs).-{-# NOINLINE [1] map #-}-map :: Box (a -> b) -> Events a -> Events b-map f (Just' x ::: xs) =  (Just' (unbox f x)) ::: delay (map f (adv xs))-map f (Nothing' ::: xs) = Nothing' ::: delay (map f (adv xs))---- | An event that will never occur.-never :: Events a-never = Nothing' ::: delay never---- | @switch s e@ will behave like @s@ but switches to @s'$ every time--- the event 'e' occurs with some value @s'@.-switch :: Str a -> Events (Str a) -> Str a-switch (x ::: xs) (Nothing' ::: fas) = x ::: delay (switch (adv xs)  (adv fas))-switch  _xs       (Just' (a ::: as) ::: fas)   = a ::: (delay switch <*> as <*> fas)----- | Like 'switch' but works on stream functions instead of--- streams. That is, @switchTrans s e@ will behave like @s@ but--- switches to @s'$ every time the event 'e' occurs with some value--- @s'@.-switchTrans :: (Str a -> Str b) -> Events (Str a -> Str b) -> (Str a -> Str b)-switchTrans f es as = switchTrans' (f as) es as---- | Helper function for 'switchTrans'.-switchTrans' :: Str b -> Events (Str a -> Str b) -> Str a -> Str b-switchTrans' (b ::: bs) (Nothing' ::: fs) (_:::as) = b ::: (delay switchTrans' <*> bs <*> fs <*> as)-switchTrans' _xs        (Just' f ::: fs)  as@(_:::as') = b' ::: (delay switchTrans' <*> bs' <*> fs <*> as')-  where (b' ::: bs') = f as----- | Trigger an event as every time the given predicate turns true on--- the given stream. The value of the event is the same as that of the--- stream at that time.-trigger :: Box (a -> Bool) -> Str a -> Events a-trigger p (x ::: xs) = x' ::: (delay (trigger p) <*> xs)-  where x' = if unbox p x then Just' x else Nothing'---- | Trigger an event every time the given function produces a 'Just''--- value.-triggerMap :: Box (a -> Maybe' b) -> Str a -> Events b-triggerMap = S.map----{-# RULES--  "map/map" forall f g xs.-    map f (map g xs) = map (box (unbox f . unbox g)) xs ;--#-}

@@ -0,0 +1,115 @@+{-# OPTIONS -fplugin=Rattus.Plugin #-}+{-# LANGUAGE TypeOperators #-}++-- | Programming with futures, i.e. data that will arrive at some time+-- in the future++module Rattus.Future+  ( map+  , never+  , switch+  , switchTrans+  , whenJust+  , Future(..)+  , await+  , trigger+  , triggerMap+  )++where++import Rattus+import Rattus.Stream hiding (map)++import Prelude hiding (map)+++-- | A future may either be available now or later.+data Future a = Now !a | Wait !(O (Future a))++-- all functions in this module are in Rattus +{-# ANN module Rattus #-}++-- | Apply a function to the value of the future (if it ever occurs).+{-# NOINLINE [1] map #-}+map :: Box (a -> b) -> Future a -> Future b+map f (Now x) = Now (unbox f x)+map f (Wait x) = Wait (delay (map f) <#> x)++-- | A future that will never happen.+never :: Future a+never = Wait (delay never)+++-- | @switch s e@ will behave like @s@ until the future @e@ is+-- available with value @s'@, in which case it will behave as @s'@.+switch :: Str a -> Future (Str a) -> Str a+switch (x ::: xs) (Wait fas) = x ::: (delay switch <#> xs <#> fas)+switch _xs        (Now ys)   = ys ++-- | Turn a stream of 'Maybe''s into a future. The future will occur+-- whenever the stream has a value of the form @Just' v@, and the+-- future then has value @v@.+firstJust :: Str (Maybe' a) -> Future a+firstJust (Just' x ::: _) = Now x+firstJust (Nothing' ::: xs) = Wait (delay firstJust <#> xs)++-- | Turn a stream of 'Maybe''s into a stream of futures. Each such+-- future behaves as if created by 'firstJust'.+whenJust :: Str (Maybe' a) -> Str (Future a)+whenJust cur@(_ ::: xs) = firstJust cur ::: (delay whenJust <#> xs)+++-- | Like 'switch' but works on stream functions instead of+-- streams. That is, @switchTrans s e@ will behave like @s@ until the+-- future @e@ occurs with value @s'@, in which case it will behave as+-- @s'@.+switchTrans :: (Str a -> Str b) -> Future (Str a -> Str b) -> (Str a -> Str b)+switchTrans f es as = switchTrans' (f as) es as++-- | Helper function for 'switchTrans'.+switchTrans' :: Str b -> Future (Str a -> Str b) -> Str a -> Str b+switchTrans' (x ::: xs) (Wait fas) (_:::is) = x ::: (delay switchTrans' <#> xs <#> fas <#> is)+switchTrans' _xs        (Now ys)   is = ys is++-- | Helper function for 'await'.+await1 :: Stable a => a -> Future b -> Future (a :* b)+await1 a (Wait eb) = Wait (delay await1 <## a <#> eb)+await1 a (Now  b)  = Now  (a :* b)++-- | Helper function for 'await'.+await2 :: Stable b => b -> Future a -> Future (a :* b)+await2 b (Wait ea) = Wait (delay await2 <## b <#> ea)+await2 b (Now  a)  = Now  (a :* b)++-- | Synchronise two futures. The resulting future occurs after both+-- futures have occurred (coinciding with whichever future occurred+-- last.+await :: (Stable a, Stable b) => Future a -> Future b -> Future(a :* b)+await (Wait ea) (Wait eb)  = Wait (delay await <#> ea <#> eb)+await (Now a)   eb         = await1 a eb+await ea        (Now b)    = await2 b ea++-- | Trigger a future as soon as the given predicate turns true on the+-- given stream. The value of the future is the same as that of the+-- stream at that time.+trigger :: Box (a -> Bool) -> Str a -> Future a+trigger p (x ::: xs)+  | unbox p x  = Now x+  | otherwise  = Wait (delay (trigger p) <#> xs)+++-- | Trigger a future as soon as the given function produces a 'Just''+-- value.+triggerMap :: Box (a -> Maybe' b) -> Str a -> Future b+triggerMap f (x ::: xs) =+  case unbox f x of+    Just' y  -> Now y+    Nothing' -> Wait (delay (triggerMap f) <#> xs)++{-# RULES++  "map/map" forall f g xs.+    map f (map g xs) = map (box (unbox f . unbox g)) xs ;++#-}

@@ -7,7 +7,7 @@ -- (mutual) recursive. To this end, this module also provides a -- functions to compute, bound variables and variable occurrences. -module Rattus.Plugin.Dependency (dependency, HasBV (..)) where+module Rattus.Plugin.Dependency (dependency, HasBV (..),printBinds) where   import GhcPlugins@@ -58,16 +58,16 @@         filterJust (CyclicSCC bs) = Just (CyclicSCC (catMaybes bs))  --- printBinds (AcyclicSCC bind) = liftIO (putStr "acyclic bind: ") >> printBind (fst bind) >> liftIO (putStrLn "") --- printBinds (CyclicSCC binds) = liftIO (putStr "cyclic binds: ") >> mapM_ (printBind . fst) binds >> liftIO (putStrLn "") +printBinds (AcyclicSCC bind) = liftIO (putStr "acyclic bind: ") >> printBind (fst bind) >> liftIO (putStrLn "") +printBinds (CyclicSCC binds) = liftIO (putStr "cyclic binds: ") >> mapM_ (printBind . fst) binds >> liftIO (putStrLn "")   --- printBind (L _ FunBind{fun_id = L _ name}) = ---   liftIO $ putStr $ (getOccString name ++ " ")--- printBind (L _ (AbsBinds {abs_exports = exp})) = ---   mapM_ (\ e -> liftIO $ putStr $ ((getOccString $ abe_poly e)  ++ " ")) exp--- printBind (L _ (VarBind {var_id = name})) =   liftIO $ putStr $ (getOccString name ++ " ")--- printBind _ = return ()+printBind (L _ FunBind{fun_id = L _ name}) = +  liftIO $ putStr $ (getOccString name ++ " ")+printBind (L _ (AbsBinds {abs_exports = exp})) = +  mapM_ (\ e -> liftIO $ putStr $ ((getOccString $ abe_poly e)  ++ " ")) exp+printBind (L _ (VarBind {var_id = name})) =   liftIO $ putStr $ (getOccString name ++ " ")+printBind _ = return ()  -- | Computes the variables that are bound by a given piece of syntax. @@ -186,7 +186,10 @@  instance HasFV (HsValBindsLR GhcTc GhcTc) where   getFV (ValBinds _ b _) = getFV b-  getFV _ = Set.empty+  getFV (XValBindsLR b) = getFV b++instance HasFV (NHsValBindsLR GhcTc) where+  getFV (NValBinds bs _) = foldMap (getFV . snd) bs  instance HasFV (HsBindLR GhcTc GhcTc) where   getFV FunBind {fun_matches = ms} = getFV ms

@@ -19,6 +19,8 @@ import Rattus.Plugin.Dependency import Rattus.Plugin.Annotation +import Data.IORef+ import Prelude hiding ((<>)) import GhcPlugins import TcRnTypes@@ -41,25 +43,31 @@ import qualified Data.Map as Map import Data.Set (Set) import Data.Map (Map)+import Data.List import System.Exit+import Data.Either import Data.Maybe  import Control.Monad +type ErrorMsg = (Severity,SrcSpan,SDoc)+type ErrorMsgsRef = IORef [ErrorMsg]+ -- | The current context for scope checking data Ctxt = Ctxt   {+    errorMsgs :: ErrorMsgsRef,     -- | Variables that are in scope now (i.e. occurring in the typing     -- context but not to the left of a tick)     current :: LCtxt,     -- | Variables that are in the typing context, but to the left of a     -- tick-    earlier :: Maybe LCtxt,+    earlier :: Either NoTickReason LCtxt,     -- | Variables that have fallen out of scope. The map contains the     -- reason why they have fallen out of scope.     hidden :: Hidden,-    -- | Same as 'hidden' but for recursive variables.-    hiddenRec :: Hidden,+    -- -- | Same as 'hidden' but for recursive variables.+    -- hiddenRec :: Hidden,     -- | The current location information.     srcLoc :: SrcSpan,     -- | If we are in the body of a recursively defined function, this@@ -79,19 +87,19 @@     -- (stripped of all non-stable stuff). It is set when typechecking     -- 'box', 'arr' and guarded recursion.     stabilized :: Maybe StableReason}-  deriving Show  + -- | The starting context for checking a top-level definition. For -- non-recursive definitions, the argument is @Nothing@. Otherwise, it -- contains the recursively defined variables along with the location -- of the recursive definition.-emptyCtxt :: Maybe (Set Var,SrcSpan) -> Ctxt-emptyCtxt mvar =-  Ctxt { current =  Set.empty,-         earlier = Nothing,+emptyCtxt :: ErrorMsgsRef -> Maybe (Set Var,SrcSpan) -> Ctxt+emptyCtxt em mvar =+  Ctxt { errorMsgs = em,+         current =  Set.empty,+         earlier = Left NoDelay,          hidden = Map.empty,-         hiddenRec = Map.empty,          srcLoc = UnhelpfulSpan "<no location info>",          recDef = mvar,          primAlias = Map.empty,@@ -113,8 +121,11 @@ data StableReason = StableRec SrcSpan | StableBox | StableArr deriving Show  -- | Indicates, why a variable has fallen out of scope.-data HiddenReason = Stabilize StableReason | FunDef | AdvApp deriving Show+data HiddenReason = Stabilize StableReason | FunDef | DelayApp | AdvApp deriving Show +-- | Indicates, why there is no tick+data NoTickReason = NoDelay | TickHidden HiddenReason deriving Show+ -- | Hidden context, containing variables that have fallen out of -- context along with the reason why they have. type Hidden = Map Var HiddenReason@@ -138,7 +149,7 @@ -- variables. class ScopeBind a where   -- | 'checkBind' checks whether its argument is scope-correct and in--- addition returns the the set of variables bound by it.+  -- addition returns the the set of variables bound by it.   checkBind :: GetCtxt => a -> TcM (Bool,Set Var)  @@ -158,10 +169,20 @@ -- found, the current execution is halted with 'exitFailure'. checkAll :: TcGblEnv -> TcM () checkAll env = do-  let bindDep = filter (filterBinds (tcg_mod env) (tcg_ann_env env)) (dependency (tcg_binds env))-  res <- mapM checkSCC bindDep+  let dep = dependency (tcg_binds env)+  let bindDep = filter (filterBinds (tcg_mod env) (tcg_ann_env env)) dep+  err <- liftIO (newIORef [])+  res <- mapM (checkSCC err) bindDep+  msgs <- liftIO (readIORef err)+  printAccErrMsgs msgs   if and res then return () else liftIO exitFailure ++printAccErrMsgs :: [ErrorMsg] -> TcM ()+printAccErrMsgs msgs = mapM_ printMsg (sortOn (\(_,l,_)->l) msgs)+  where printMsg (sev,loc,doc) = printMessage sev loc doc++ -- | This function checks whether a given top-level definition (either -- a single non-recursive definition or a group of mutual recursive -- definitions) is marked as Rattus code (via an annotation). In a@@ -195,7 +216,7 @@  instance Scope a => Scope (Match GhcTc a) where   check Match{m_pats=ps,m_grhss=rhs} = mod `modifyCtxt` check rhs-    where mod c = addVars (getBV ps) (if null ps then c else stabilizeLater c)+    where mod c = addVars (getBV ps) (if null ps then c else stabilizeLater FunDef c)   check XMatch{} = return True  instance Scope a => Scope (MatchGroup GhcTc a) where@@ -251,13 +272,13 @@       _ -> return (res, vs)     where check' b@(L l _) = fc l `modifyCtxt` check b           fc l c = let-            ctxHid = maybe (current c) (Set.union (current c)) (earlier c)-            recHid = maybe ctxHid (Set.union ctxHid . fst) (recDef c)+            ctxHid = either (const $ current c) (Set.union (current c)) (earlier c)             in c {current = Set.empty,-                  earlier = Nothing,+                  earlier = Left (TickHidden $ Stabilize $ StableRec l),                   hidden =  hidden c `Map.union`-                            (Map.fromSet (const (Stabilize (StableRec l))) recHid),-                  recDef = Just (vs,l),+                            (Map.fromSet (const (Stabilize (StableRec l))) ctxHid),+                  recDef = maybe (Just (vs,l)) (\(vs',_) -> Just (Set.union vs' vs,l)) (recDef c),+                   -- TODO fix location info of recDef (needs one location for each var)                   stabilized = Just (StableRec l)}            recReason :: StableReason -> SDoc@@ -324,6 +345,14 @@ arrReason StableBox = "The use of arr in the scope of box" arrReason (StableRec _) = "The use of arr in a recursive definition" +tickHidden :: HiddenReason -> SDoc+tickHidden FunDef = "a function definition"+tickHidden DelayApp = "a nested application of delay"+tickHidden AdvApp = "an application of adv"+tickHidden (Stabilize StableBox) = "an application of box"+tickHidden (Stabilize StableArr) = "an application of arr"+tickHidden (Stabilize (StableRec src)) = "a nested recursive definition (at " <> ppr src <> ")"+ instance Scope (HsExpr GhcTc) where   check (HsVar _ (L _ v))     | Just p <- isPrim v =@@ -333,8 +362,9 @@     | otherwise = case getScope v of              Hidden reason -> printMessageCheck SevError reason              Visible -> return True-             ImplUnboxed -> printMessageCheck SevWarning -                (ppr v <> text " is an external temporal function used under delay, which may cause time leaks")+             ImplUnboxed -> return True+               -- printMessageCheck SevWarning+               --  (ppr v <> text " is an external temporal function used under delay, which may cause time leaks.")   check (HsApp _ e1 e2) =     case isPrimExpr e1 of     Just (p,_) -> case p of@@ -353,16 +383,16 @@           _ -> return ch        Unbox -> check e2-      Delay -> case earlier ?ctxt of-        Just _ -> printMessageCheck SevError (text "cannot delay more than once")-        Nothing -> (\c -> c{current = Set.empty, earlier = Just (current ?ctxt)})+      Delay ->  ((\c -> c{current = Set.empty, earlier = Right (current ?ctxt)}) . stabilizeLater DelayApp)                   `modifyCtxt` check  e2       Adv -> case earlier ?ctxt of-        Just er -> mod `modifyCtxt` check e2-          where mod c =  c{earlier = Nothing, current = er,+        Right er -> mod `modifyCtxt` check e2+          where mod c =  c{earlier = Left $ TickHidden AdvApp, current = er,                            hidden = hidden ?ctxt `Map.union`                             Map.fromSet (const AdvApp) (current ?ctxt)}-        Nothing -> printMessageCheck SevError (text "can only advance under delay")+        Left NoDelay -> printMessageCheck SevError ("adv may only be used in the scope of a delay.")+        Left (TickHidden hr) -> printMessageCheck SevError ("adv may only be used in the scope of a delay. "+                            <> " There is a delay, but its scope is interrupted by " <> tickHidden hr <> ".")     _ -> liftM2 (&&) (check e1)  (check e2)   check HsUnboundVar{}  = return True   check HsConLikeOut{} = return True@@ -370,6 +400,7 @@   check HsOverLabel{} = return True   check HsIPVar{} = notSupported "implicit parameters"   check HsOverLit{} = return True+    #if __GLASGOW_HASKELL__ >= 808   check (HsAppType _ e _)@@ -385,8 +416,8 @@   check (HsWrap _ _ e) = check e   check HsLit{} = return True   check (OpApp _ e1 e2 e3) = and <$> mapM check [e1,e2,e3]-  check (HsLam _ mg) = stabilizeLater `modifyCtxt` check mg-  check (HsLamCase _ mg) = stabilizeLater `modifyCtxt` check mg+  check (HsLam _ mg) = stabilizeLater FunDef `modifyCtxt` check mg+  check (HsLamCase _ mg) = stabilizeLater FunDef `modifyCtxt` check mg   check (HsIf _ _ e1 e2 e3) = and <$> mapM check [e1,e2,e3]   check (HsCase _ e1 e2) = (&&) <$> check e1 <*> check e2   check (SectionL _ e1 e2) = (&&) <$> check e1 <*> check e2@@ -457,16 +488,13 @@ -- | This is used when checking function definitions. If the context -- is not ticked, it stays the same. Otherwise, it is stabilized -- (similar to 'box').-stabilizeLater :: Ctxt -> Ctxt-stabilizeLater c =-  if isJust (earlier c)-  then c {earlier = Nothing,-          hidden = hid,-          hiddenRec = maybe (hiddenRec c) (Map.union (hidden c) . Map.fromSet (const FunDef))-                      (fst <$> recDef c),-          recDef = Nothing}-  else c-  where hid = maybe (hidden c) (Map.union (hidden c) . Map.fromSet (const FunDef)) (earlier c)+stabilizeLater :: HiddenReason -> Ctxt -> Ctxt+stabilizeLater reason c =+  case earlier c of+    Left _ -> c+    Right earl ->+      c {earlier = Left $ TickHidden reason,+         hidden = Map.union (hidden c) $ Map.fromSet (const reason) earl}   instance Scope (ArithSeqInfo GhcTc) where@@ -526,13 +554,13 @@ -- non-recursive definition or a group of (mutual) recursive -- definitions. -checkSCC :: SCC (LHsBindLR  GhcTc GhcTc, Set Var) -> TcM Bool-checkSCC (AcyclicSCC (b,_)) = setCtxt (emptyCtxt Nothing) (check b)+checkSCC :: ErrorMsgsRef -> SCC (LHsBindLR  GhcTc GhcTc, Set Var) -> TcM Bool+checkSCC errm (AcyclicSCC (b,_)) = setCtxt (emptyCtxt errm Nothing) (check b) -checkSCC (CyclicSCC bs) = (fmap and (mapM check' bs'))+checkSCC errm (CyclicSCC bs) = (fmap and (mapM check' bs'))   where bs' = map fst bs         vs = foldMap snd bs-        check' b@(L l _) = setCtxt (emptyCtxt (Just (vs,l))) (check b)+        check' b@(L l _) = setCtxt (emptyCtxt errm (Just (vs,l))) (check b)  -- | Stabilizes the given context, i.e. remove all non-stable types -- and any tick. This is performed on checking 'box', 'arr' and@@ -541,12 +569,10 @@ stabilize :: StableReason -> Ctxt -> Ctxt stabilize sr c = c   {current = Set.empty,-   earlier = Nothing,+   earlier = Left $ TickHidden hr,    hidden = hidden c `Map.union` Map.fromSet (const hr) ctxHid,-   hiddenRec = hiddenRec c `Map.union` maybe Map.empty (Map.fromSet (const hr) . fst) (recDef c),-   recDef = Nothing,    stabilized = Just sr}-  where ctxHid = maybe (current c) (Set.union (current c)) (earlier c)+  where ctxHid = either (const $ current c) (Set.union (current c)) (earlier c)         hr = Stabilize sr  data VarScope = Hidden SDoc | Visible | ImplUnboxed@@ -559,22 +585,15 @@     Ctxt{recDef = Just (vs,_), earlier = e}       | v `Set.member` vs ->         case e of-          Just _ -> Visible-          Nothing -> Hidden ("(Mutually) recursive call to " <> ppr v <> " must occur under delay")-    _ ->-      case Map.lookup v (hiddenRec ?ctxt) of-        Just (Stabilize (StableRec rv)) -> Hidden ("Recursive call to" <> ppr v <>-                            " is not allowed as it occurs in a local recursive definiton (at " <> ppr rv <> ")")-        Just (Stabilize StableBox) -> Hidden ("Recursive call to " <> ppr v <> " is not allowed here, since it occurs under a box")-        Just (Stabilize StableArr) -> Hidden ("Recursive call to " <> ppr v <> " is not allowed here, since it occurs inside an arrow notation")-        Just FunDef -> Hidden ("Recursive call to " <> ppr v <> " is not allowed here, since it occurs in a function that is defined under delay")-        Just AdvApp -> Hidden ("This should not happen: recursive call to " <> ppr v <> " is out of scope due to adv")-        Nothing -> -          case Map.lookup v (hidden ?ctxt) of+          Right _ -> Visible+          Left NoDelay -> Hidden ("The (mutually) recursive call to " <> ppr v <> " must occur in the scope of a delay")+          Left (TickHidden hr) -> Hidden ("The (mutually) recursive call to " <> ppr v <> " must occur in the scope of a delay. "+                            <> "There is a delay, but its scope is interrupted by " <> tickHidden hr <> ".")+    _ ->  case Map.lookup v (hidden ?ctxt) of             Just (Stabilize (StableRec rv)) ->               if (isStable (stableTypes ?ctxt) (varType v)) then Visible               else Hidden ("Variable " <> ppr v <> " is no longer in scope:" $$-                       "It appears in a local recursive definiton (at " <> ppr rv <> ")"+                       "It appears in a local recursive definition (at " <> ppr rv <> ")"                        $$ "and is of type " <> ppr (varType v) <> ", which is not stable.")             Just (Stabilize StableBox) ->               if (isStable (stableTypes ?ctxt) (varType v)) then Visible@@ -583,17 +602,18 @@             Just (Stabilize StableArr) ->               if (isStable (stableTypes ?ctxt) (varType v)) then Visible               else Hidden ("Variable " <> ppr v <> " is no longer in scope:" $$-                       "It occurs under inside an arrow notation and is of type " <> ppr (varType v) <> ", which is not stable.")+                       "It occurs inside an arrow notation and is of type " <> ppr (varType v) <> ", which is not stable.")             Just AdvApp -> Hidden ("Variable " <> ppr v <> " is no longer in scope: It occurs under adv.")+            Just DelayApp -> Hidden ("Variable " <> ppr v <> " is no longer in scope due to repeated application of delay")             Just FunDef -> if (isStable (stableTypes ?ctxt) (varType v)) then Visible               else Hidden ("Variable " <> ppr v <> " is no longer in scope: It occurs in a function that is defined under a delay, is a of a non-stable type " <> ppr (varType v) <> ", and is bound outside delay")             Nothing-              | maybe False (Set.member v) (earlier ?ctxt) ->+              | either (const False) (Set.member v) (earlier ?ctxt) ->                 if isStable (stableTypes ?ctxt) (varType v) then Visible                 else Hidden ("Variable " <> ppr v <> " is no longer in scope:" $$                          "It occurs under delay" $$ "and is of type " <> ppr (varType v) <> ", which is not stable.")               | Set.member v (current ?ctxt) -> Visible-              | isTemporal (varType v) && isJust (earlier ?ctxt) && userFunction v+              | isTemporal (varType v) && isRight (earlier ?ctxt) && userFunction v                 -> ImplUnboxed               | otherwise -> Visible @@ -657,7 +677,8 @@  -- | Print a message with the current location. printMessage' :: GetCtxt => Severity -> SDoc ->  TcM ()-printMessage' sev doc = printMessage sev (srcLoc ?ctxt) doc+printMessage' sev doc =+  liftIO (modifyIORef (errorMsgs ?ctxt) ((sev ,srcLoc ?ctxt, doc) :))  -- | Print a message with the current location. Returns 'False', if -- the severity is 'SevError' and otherwise 'True.

@@ -4,9 +4,9 @@ module Main (module Main) where  import Rattus-import Rattus.Stream+import Rattus.Stream as S import Rattus.Yampa-import Prelude hiding ((<*>), map, const)+import Prelude  -- Uncomment the annotation below to check that the definitions in -- this module don't type check@@ -14,6 +14,23 @@ -- {-# ANN module Rattus #-}  ++loopIndirect :: Str Int+loopIndirect = run+  where run :: Str Int+        run = loopIndirect++        +loopIndirect' :: Str Int+loopIndirect' = let run = loopIndirect' in run+++nestedUnguard :: Str Int+nestedUnguard = run 0+  where run :: Int -> Str Int+        run 0 = nestedUnguard+        run n = n ::: delay (run (n-1))+ sfLeak :: O Int -> SF () (O Int) sfLeak  x = proc _ -> do   returnA -< x@@ -27,8 +44,8 @@ dblAdv :: O (O a) -> O a dblAdv y = delay (adv (adv y)) -dblDelay :: O (O Int)-dblDelay = delay (delay 1)+dblAdv' :: O (O a) -> O (O a)+dblAdv' y = delay (delay (adv (adv y)))  lambdaUnderDelay :: O (O Int -> Int -> Int) lambdaUnderDelay = delay (\x _ -> adv x)@@ -36,13 +53,6 @@ sneakyLambdaUnderDelay :: O (Int -> Int) sneakyLambdaUnderDelay = delay (let f _ =  adv (delay 1) in f) --lambdaUnderDelay' :: O Int -> O (Int -> O Int)-lambdaUnderDelay' x = delay (\_ -> x)--sneakyLambdaUnderDelay' :: O Int -> O (Int -> O Int)-sneakyLambdaUnderDelay' x = delay (let f _ =  x in f)- leaky :: (() -> Bool) -> Str Bool leaky p = p () ::: delay (leaky (\ _ -> hd (leaky (\ _ -> True)))) @@ -72,9 +82,6 @@  mutualLoop' :: a mutualLoop' = mutualLoop--zeros :: Box (Str Int)-zeros = box (0 ::: delay (unbox zeros))  constUnstable :: a -> Str a constUnstable a = run

@@ -1,19 +1,17 @@ {-# LANGUAGE TypeOperators #-}+ module Main (module Main) where  import Rattus import Rattus.Stream import Rattus.ToHaskell -import qualified Prelude-import Prelude hiding ((<*>), map) - {-# ANN module Rattus #-}  scan3 :: (Stable a) => Box(a -> a -> a) -> Box (a -> Bool) -> a -> Str a -> Str a scan3 f p acc (a ::: as) =  (if unbox p a then acc else a)-      ::: (delay (scan3 f p acc') <*> as)+      ::: (delay (scan3 f p acc') <#> as)   where acc' = unbox f acc a  

@@ -0,0 +1,52 @@+{-# LANGUAGE Arrows #-}+{-# LANGUAGE RebindableSyntax #-}++module Main (module Main) where++import Rattus+import Rattus.Stream as S+import Prelude++-- All of these examples should typecheck with the more relaxed typing+-- rules of Rattus that allows functions and delays under tick.++{-# ANN module Rattus #-}+++recBox :: Str Int+recBox = 0 ::: unbox (box (delay recBox))+++dblDelay :: O (O Int)+dblDelay = delay (delay 1)+++lambdaUnderDelay :: O (Int -> Int)+lambdaUnderDelay = delay (\x -> x)++advUnderLambda :: O (O Int -> O Int)+advUnderLambda = delay (\x -> delay (adv x))++sneakyLambdaUnderDelay :: O (Int -> Int)+sneakyLambdaUnderDelay = delay (let f x = x in f)++zeros :: Box (Str Int)+zeros = box (0 ::: delay (unbox zeros))++oneTwo :: Str Int+oneTwo = 1 ::: delay (2 ::: delay oneTwo)++data FStr a = Cons ! a ! (O (a -> O (FStr a)))++recFun :: Int -> FStr Int +recFun n = Cons n (delay (\ x -> delay (recFun x)))++nestedRec :: Str Int+nestedRec = run 10+  where run :: Int -> Str Int+        run 0 = 0 ::: delay (nestedRec)+        run n = n ::: delay (run (n-1))+++{-# ANN main NotRattus #-}+main = putStrLn "This file should type check"

@@ -3,16 +3,15 @@ module Main (module Main) where  import Rattus-import Rattus.Stream-import Prelude hiding ((<*>), map,zip,const)+import Rattus.Stream as Str  {-# ANN module Rattus #-}  twice :: Str Int -> Str Int-twice = map (box (+1)) . map (box (+1))+twice = Str.map (box (+1)) . Str.map (box (+1))  scanAndMap :: Str Int -> Str Int-scanAndMap xs = map (box (+1)) (scan (box (+)) 0 xs)+scanAndMap xs = Str.map (box (+1)) (scan (box (+)) 0 xs)  sums :: Str Int -> Str Int sums xs = scan (box (+)) 0 xs@@ -24,19 +23,19 @@ twiceScanMap xs = scan (box (+)) 0  (scanMap (box (+)) (box (+1)) 0 xs)  zipMap :: Str Int -> Str Int -> Str Int-zipMap xs ys = map (box (\ (x:*y) -> x + y)) (zip xs ys)+zipMap xs ys = Str.map (box (\ (x:*y) -> x + y)) (Str.zip xs ys)  constMap :: Str Int-constMap = map (box (+1)) (const 5)+constMap = Str.map (box (+1)) (Str.const 5)    apply :: O (Int -> Int -> Int) -> O Int -> O Int -> O Int-apply f x y = f <*> x <*> y+apply f x y = f <#> x <#> y   apply' :: O (Int -> Int -> Int) -> Int -> O Int -> O Int-apply' f x y = f <** x <*> y+apply' f x y = f <## x <#> y   {-# ANN main NotRattus #-}

@@ -1,13 +1,11 @@ {-# LANGUAGE TypeOperators #-}+ module Main (module Main) where  import Rattus-import Rattus.Stream+import Rattus.Stream as Str import Rattus.ToHaskell -import Prelude hiding ((<*>), map)-- {-# ANN module Rattus #-}  @@ -23,10 +21,10 @@  -- This function should cause a warning. leakyNats :: Str Int-leakyNats = 0 ::: delay (map (box (+1)) leakyNats)+leakyNats = 0 ::: delay (Str.map (box (+1)) leakyNats)  inc :: Str Int -> Str Int-inc = map (box ((+)1))+inc = Str.map (box ((+)1))  -- This function should cause a warning. @@ -45,7 +43,7 @@  -- This function should cause a warning. mapMap :: Box (a -> a) -> Box (a -> a) -> Str a -> Str a-mapMap f g (x ::: xs) = unbox f x ::: delay (map g (mapMap g f (adv xs)))+mapMap f g (x ::: xs) = unbox f x ::: delay (Str.map g (mapMap g f (adv xs)))  -- This function should cause a warning. leakyMap :: Str Int@@ -68,11 +66,11 @@  -- This function should cause a warning. natsTrans :: Str Int -> Str Int-natsTrans (x ::: xs) = x ::: delay (map (box ((+)x)) $ natsTrans $ adv xs)+natsTrans (x ::: xs) = x ::: delay (Str.map (box ((+)x)) $ natsTrans $ adv xs)  -- This function should cause a warning. leakySum :: Box (Int -> Int) -> Str Int -> Str Int-leakySum f (x ::: xs) = unbox f x ::: (delay (leakySum (box (\ y -> unbox f (y + x)))) <*> xs)+leakySum f (x ::: xs) = unbox f x ::: (delay (leakySum (box (\ y -> unbox f (y + x)))) <#> xs)   {-# ANN recurse NotRattus #-}

@@ -7,9 +7,8 @@ import Rattus import Rattus.Stream import Rattus.Yampa-import Prelude hiding ((<*>))-import Data.Set-import qualified Data.Set as Set+import Data.Set as Set+import Prelude   {-# ANN module Rattus #-}@@ -56,40 +55,40 @@ map1 f (x ::: xs) = unbox f x ::: delay (map1 f (adv xs))  map2 :: Box (a -> b) -> Str a -> Str b-map2 f (x ::: xs) = unbox f x ::: (delay map2 <** f <*> xs)+map2 f (x ::: xs) = unbox f x ::: (delay map2 <## f <#> xs)  map3 :: Box (a -> b) -> Str a -> Str b map3 f = run-  where run (x ::: xs) = unbox f x ::: (delay run <*> xs)+  where run (x ::: xs) = unbox f x ::: (delay run <#> xs)   -- local mutual recursive definition nestedMutual :: Str Int -> Str Int nestedMutual = lbar1 (box (+1))   where lbar1 :: Box (a -> b) -> Str a -> Str b-        lbar1 f (x ::: xs) = unbox f x ::: (delay (lbar2 f) <*> xs)+        lbar1 f (x ::: xs) = unbox f x ::: (delay (lbar2 f) <#> xs)          lbar2 :: Box (a -> b) -> Str a -> Str b-        lbar2 f  (x ::: xs) = unbox f x ::: (delay (lbar1 f) <*> xs)+        lbar2 f  (x ::: xs) = unbox f x ::: (delay (lbar1 f) <#> xs)    -- mutual recursive definition bar1 :: Box (a -> b) -> Str a -> Str b-bar1 f (x ::: xs) = unbox f x ::: (delay (bar2 f) <*> xs)+bar1 f (x ::: xs) = unbox f x ::: (delay (bar2 f) <#> xs)  bar2 :: Box (a -> b) -> Str a -> Str b-bar2 f  (x ::: xs) = unbox f x ::: (delay (bar1 f) <*> xs)+bar2 f  (x ::: xs) = unbox f x ::: (delay (bar1 f) <#> xs)   -- mutual recursive definition foo1,foo2 :: Box (a -> b) -> Str a -> Str b-(foo1,foo2) = (\ f (x ::: xs) -> unbox f x ::: (delay (foo2 f) <*> xs),-               \ f (x ::: xs) -> unbox f x ::: (delay (foo1 f) <*> xs))+(foo1,foo2) = (\ f (x ::: xs) -> unbox f x ::: (delay (foo2 f) <#> xs),+               \ f (x ::: xs) -> unbox f x ::: (delay (foo1 f) <#> xs))   applyDelay :: O (O (a -> b)) -> O (O a) -> O (O b)-applyDelay f x = delay (adv f <*> adv x)+applyDelay f x = delay (adv f <#> adv x)   stableDelay :: Stable a => a -> O a@@ -145,6 +144,14 @@  alt :: Int -> Int -> Str Int alt n m = n ::: delay (alt m n)+++myMap :: Str Int -> Str Int+myMap (x ::: xs) = (x + 1) ::: delay (fst' (myMap (adv xs):*nats))++nats :: Str Int+nats = 0 ::: delay (myMap nats)+   {-# ANN main NotRattus #-}