packages feed

Rattus (empty) → 0.1.0.0

raw patch · 23 files changed

+2089/−0 lines, 23 filesdep +Rattusdep +basedep +containersbuild-type:Customsetup-changedbinary-added

Dependencies added: Rattus, base, containers, ghc, simple-affine-space

Files

+ CHANGELOG.md view
@@ -0,0 +1,3 @@+0.1.0.0+-------+initial release
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2020 Patrick Bahr++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions+are met:++1. Redistributions of source code must retain the above copyright+   notice, this list of conditions and the following disclaimer.++2. Redistributions in binary form must reproduce the above copyright+   notice, this list of conditions and the following disclaimer in the+   documentation and/or other materials provided with the distribution.++3. Neither the name of the author nor the names of his contributors+   may be used to endorse or promote products derived from this software+   without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS OR+IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE+DISCLAIMED.  IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE FOR+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS+OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT,+STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN+ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE+POSSIBILITY OF SUCH DAMAGE.
+ Rattus.cabal view
@@ -0,0 +1,159 @@+cabal-version:       1.18+name:                Rattus+version:             0.1.0.0+category:            FRP+synopsis:            A modal FRP language+description:++            This library implements the Rattus programming language as+            an embedded DSL. To this end the library provides a GHC+            plugin that performs the additional checks that are+            necessary for Rattus. What follows is a brief+            introduction to the language and its usage. A more+            detailed introduction can be found in this+            <docs/paper.pdf paper>.+            +            .+            +            Rattus is a functional reactive programming (FRP) language+            that uses modal types to ensure operational properties+            that are crucial for reactive programs: productivity (in+            each computation step, the program makes progress),+            causality (output depends only on current and earlier+            input), and no implicit space leaks (programs do not+            implicitly retain memory over time).+            +            .+            +            To ensure these properties, Rattus uses the type modality+            @O@ to express the concept of time at the type+            level. Intuitively speaking, a value of type @O a@+            represents a computation that will produce a value of type+            @a@ in the next time step. Additionally, the language also+            features the @Box@ type modality. A value of type @Box a@+            is a time-independent computation that can be executed at+            any time to produce a value of type @a@.++            .++            The core of the language is defined in the module+            "Rattus.Primitives". Note that the operations on @O@ and+            @Box@ have non-standard typing rules. Therefore, this+            library provides a compiler plugin that checks these+            non-standard typing rules. To write Rattus programs, one+            must enable this plugin via the GHC option+            @-fplugin=Rattus.Plugin@, e.g. by including the following+            line in the source file (for better error messages we also+            suggest using the option @-g2@):+            +            .+            +            > {-# OPTIONS -fplugin=Rattus.Plugin #-}+            +            .++            In addition, one must mark the functions that are written+            in Rattus:++            .+            +            > {-# ANN myFunction Rattus #-}++            .++            Or mark the whole module as a Rattus module:+            +            .++            > {-# ANN module Rattus #-}++            .++            Below is a minimal Rattus program using the+            "Rattus.Stream" module for programming with streams:++            .++            > {-# OPTIONS -fplugin=Rattus.Plugin #-}+            >     +            > import Rattus+            > import Rattus.Stream+            > +            > {-# ANN sums Rattus #-}+            > sums :: Str Int -> Str Int+            > sums = scan (box (+)) 0++homepage:            https://github.com/pa-ba/Rattus+License:             BSD3+License-file:        LICENSE+copyright:           Copyright (C) 2020 Patrick Bahr+Author:              Patrick Bahr+maintainer:          Patrick Bahr <paba@itu.dk>+stability:           experimental++build-type:          Custom++extra-source-files:  CHANGELOG.md++extra-doc-files:     docs/paper.pdf+                     +custom-setup+  setup-depends:+    base  >= 4.5 && < 5,+    Cabal >= 1.18+++library+  exposed-modules:     Rattus+                       Rattus.Stream+                       Rattus.Strict+                       Rattus.Event+                       Rattus.Events+                       Rattus.ToHaskell+                       Rattus.Yampa+                       +                       Rattus.Plugin+                       Rattus.Arrow+                       Rattus.Primitives+                       +  other-modules:       Rattus.Plugin.ScopeCheck+                       Rattus.Plugin.Strictify+                       Rattus.Plugin.Utils+                       Rattus.Plugin.StableSolver+  build-depends:       base >=4.12 && <5, containers, simple-affine-space, ghc >= 8.6+  hs-source-dirs:      src+  default-language:    Haskell2010+  ghc-options: -W -g2+  +Test-Suite memory-leak+  type:                exitcode-stdio-1.0+  main-is:             MemoryLeak.hs+  hs-source-dirs:      test+  default-language:    Haskell2010+  build-depends:       Rattus, base+  ghc-options:         -fplugin=Rattus.Plugin -rtsopts -g2++Test-Suite time-leak+  type:                exitcode-stdio-1.0+  main-is:             TimeLeak.hs+  hs-source-dirs:      test+  default-language:    Haskell2010+  build-depends:       Rattus, base+  ghc-options:         -fplugin=Rattus.Plugin -rtsopts -g2+  +Test-Suite ill-typed+  type:                exitcode-stdio-1.0+  main-is:             test/IllTyped.hs+  default-language:    Haskell2010+  build-depends:       Rattus, base+  ghc-options:         -fplugin=Rattus.Plugin -rtsopts -g2+++Test-Suite well-typed+  type:                exitcode-stdio-1.0+  main-is:             WellTyped.hs+  hs-source-dirs:      test+  default-language:    Haskell2010+  build-depends:       Rattus, base, containers+  ghc-options:         -fplugin=Rattus.Plugin -rtsopts -g2+
+ Setup.hs view
@@ -0,0 +1,29 @@+{-+Disable some errors and warnings during the haddock pass+  (caused by compiler plugins and hs-boot)+ -}+{-# OPTIONS_GHC -Wall #-}+module Main (main) where++import Distribution.Simple+import Distribution.Simple.Setup++main :: IO ()+main = defaultMainWithHooks simpleUserHooks+  { confHook = \a -> confHook simpleUserHooks a . tweakFlags }++tweakFlags :: ConfigFlags -> ConfigFlags+tweakFlags flags = flags+  { configProgramArgs = addHaddockArgs (configProgramArgs flags) }++addHaddockArgs :: [(String, [String])] -> [(String, [String])]+addHaddockArgs []+  = [("haddock", newHaddockGhcArgs)]+addHaddockArgs (("haddock", args):otherProgsArgs)+  = ("haddock", args ++ newHaddockGhcArgs) : otherProgsArgs+addHaddockArgs (progArgs:otherProgsArgs)+  = progArgs : addHaddockArgs otherProgsArgs++newHaddockGhcArgs :: [String]+newHaddockGhcArgs =+  [ "--optghc=-fobject-code" ]
+ docs/paper.pdf view

binary file changed (absent → 621417 bytes)

+ src/Rattus.hs view
@@ -0,0 +1,43 @@+{-# OPTIONS -fplugin=Rattus.Plugin #-}+++-- | The bare-bones Rattus language. To program with streams and+-- events import "Rattus.Stream" and "Rattus.Events"; to program with+-- Yampa-style signal functions import "Rattus.Yampa".++module Rattus (+  module Rattus.Primitives,+  module Rattus.Strict,+  Rattus(..),+  (|*|),+  (|**),+  (<*>),+  (<**))+  where++import Rattus.Plugin+import Rattus.Strict+import Rattus.Primitives+++import Prelude hiding ((<*>))++-- all functions in this module are in Rattus +{-# ANN module Rattus #-}+++-- | Applicative operator for 'O'.+(<*>) :: O (a -> b) -> O a -> O b+f <*> x = delay (adv f (adv x))++-- | Variant of '(<*>)' where the argument is of a stable type..+(<**) :: Stable a => O (a -> b) -> a -> O b+f <** x = delay (adv f x)++-- | Applicative operator for 'Box'.+(|*|) :: Box (a -> b) -> Box a -> Box b+f |*| x = box (unbox f (unbox x))++-- | Variant of '(|*|)' where the argument is of a stable type..+(|**) :: Stable a => Box (a -> b) -> a -> Box b+f |** x = box (unbox f x)
+ src/Rattus/Arrow.hs view
@@ -0,0 +1,66 @@+-- | This module provides a variant of the standard+-- 'Control.Arrow.Arrow' type class with a different+-- 'Control.Arrow.arr' method so that it can be implemented for signal+-- functions in Rattus.++module Rattus.Arrow where++import Prelude hiding (id)+import Rattus.Primitives+import Control.Category++-- | Variant of the standard 'Control.Arrow.Arrow' type class with a+-- different 'Control.Arrow.arr' method so that it can be implemented+-- for signal functions in Rattus.+class Category a => Arrow a where+    {-# MINIMAL arrBox, (first | (***)) #-}++    -- | Lift a function to an arrow. It is here the definition of the+    -- 'Arrow' class differs from the standard one. The function to be+    -- lifted has to be boxed.+    -- +    arrBox :: Box (b -> c) -> a b c++    -- | Send the first component of the input through the argument+    --   arrow, and copy the rest unchanged to the output.+    first :: a b c -> a (b,d) (c,d)+    first = (*** id)++    -- | A mirror image of 'first'.+    --+    --   The default definition may be overridden with a more efficient+    --   version if desired.+    second :: a b c -> a (d,b) (d,c)+    second = (id ***)++    -- | Split the input between the two argument arrows and combine+    --   their output.  Note that this is in general not a functor.+    (***) :: a b c -> a b' c' -> a (b,b') (c,c')+    f *** g = first f >>> arr swap >>> first g >>> arr swap+      where swap ~(x,y) = (y,x)++    -- | Fanout: send the input to both argument arrows and combine+    --   their output.+    --+    --   The default definition may be overridden with a more efficient+    --   version if desired.+    (&&&) :: a b c -> a b c' -> a b (c,c')+    f &&& g = arr (\b -> (b,b)) >>> f *** g+++-- | This combinator is subject to the same restrictions as the 'box'+-- primitive of Rattus. That is,+--+-- >   Γ☐ ⊢ t :: b -> c+-- > --------------------+-- >  Γ ⊢ arr t :: a b c+--+-- where Γ☐ is obtained from Γ by removing ✓ and any variables @x ::+-- 𝜏@, where 𝜏 is not a stable type.++arr :: Arrow a => (b -> c) -> a b c+arr f = arrBox (box f)++-- | The identity arrow, which plays the role of 'return' in arrow notation.+returnA :: Arrow a => a b b+returnA = arrBox (box id)
+ src/Rattus/Event.hs view
@@ -0,0 +1,107 @@+{-# OPTIONS -fplugin=Rattus.Plugin #-}+{-# LANGUAGE TypeOperators #-}++-- | Programing with single shot events, i.e. events that may occur at+-- most once.++module Rattus.Event+  ( map+  , never+  , switch+  , switchTrans+  , whenJust+  , Event(..)+  , await+  , trigger+  , triggerMap+  )++where++import Rattus+import Rattus.Stream hiding (map)++import Prelude hiding ((<*>), map)+++-- | An event may either occur now or later.+data Event a = Now !a | Wait (O (Event 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).+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)++-- | An event that will never occur.+never :: Event a+never = Wait (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 :: 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)+++-- | 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+-- @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++-- | 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)++-- | Synchronize 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+-- 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 an event as soon as 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)
+ src/Rattus/Events.hs view
@@ -0,0 +1,71 @@+{-# OPTIONS -fplugin=Rattus.Plugin #-}++-- | Programing 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).+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
+ src/Rattus/Plugin.hs view
@@ -0,0 +1,117 @@+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE DeriveDataTypeable #-}+++-- | The plugin to make it all work.++module Rattus.Plugin (plugin, Rattus(..)) where+import Rattus.Plugin.StableSolver+import Rattus.Plugin.ScopeCheck+import Rattus.Plugin.Strictify+import Rattus.Plugin.Utils++import Prelude hiding ((<>))+import GhcPlugins++import Control.Monad+import Data.Maybe+import Data.Data hiding (tyConName)++import System.Exit+++-- | Use this type to mark a Haskell function definition as a Rattus+-- function:+--+-- > {-# ANN myFunction Rattus #-}+-- +-- Or mark a whole module as consisting of Rattus functions only:+--+-- > {-# ANN module Rattus #-}+--+-- If you use the latter option, you can mark exceptions+-- (i.e. functions that should be treated as ordinary Haskell function+-- definitions) as follows:+--+-- > {-# ANN myFunction NotRattus #-}++data Rattus = Rattus | NotRattus deriving (Typeable, Data, Show, Eq)++-- | Use this to enable Rattus' plugin, either by supplying the option+-- @-fplugin=Rattus.Plugin@ directly to GHC. or by including the+-- following pragma in each source file:+-- +-- > {-# OPTIONS -fplugin=Rattus.Plugin #-}+plugin :: Plugin+plugin = defaultPlugin {+  installCoreToDos = install,+  tcPlugin = tcStable+  }+++install :: [CommandLineOption] -> [CoreToDo] -> CoreM [CoreToDo]+install _ todo = do+  return (CoreDoPluginPass "Rattus" transformProgram : todo)+++transformProgram :: ModGuts -> CoreM ModGuts+transformProgram guts = do+  newBindsM <- mapM (transform guts) (mg_binds guts)+  case sequence newBindsM of+    Nothing -> liftIO exitFailure+    Just newBinds -> return $ guts { mg_binds = newBinds }+++transform :: ModGuts -> CoreBind -> CoreM (Maybe CoreBind)+transform guts b@(Rec bs) = do+  tr <- liftM or (mapM (shouldTransform guts . fst) bs)+  if tr then+    case bs of+      [(v,e)] -> do+          --putMsg (text "check Rattus definition: " <> ppr v)+          --putMsg (ppr e)+          valid <- checkExpr (emptyCtx (Just v)) e+          if valid then do+            e' <- strictifyExpr e+            return (Just $ Rec [(v,e')])+          else return Nothing+      (v,_):_ -> do+        printMessage SevError (nameSrcSpan (varName v)) (+          text "mutual recursive definitions not supported in Rattus")+        return Nothing+      _ -> return (Just $ Rec [])+  else return (Just b)+transform guts b@(NonRec v e) = do+    tr <- shouldTransform guts v+    if tr then do+      --putMsg (text "check Rattus definition: " <> ppr v)+      --putMsg (ppr e)+      valid <- checkExpr (emptyCtx Nothing) e+      if valid then do+        e' <- strictifyExpr e+        return (Just $ NonRec v e')+      else return Nothing+    else return (Just b)++getModuleAnnotations :: Data a => ModGuts -> [a]+getModuleAnnotations guts = anns'+  where anns = filter (\a-> case ann_target a of+                         ModuleTarget m -> m == (mg_module guts)+                         _ -> False) (mg_anns guts)+        anns' = mapMaybe (fromSerialized deserializeWithData . ann_value) anns+  ++++shouldTransform :: ModGuts -> CoreBndr -> CoreM Bool+shouldTransform guts bndr = do+  l <- annotationsOn guts bndr :: CoreM [Rattus]+  return (Rattus `elem` l && not (NotRattus `elem` l) && userFunction bndr)++annotationsOn :: (Data a) => ModGuts -> CoreBndr -> CoreM [a]+annotationsOn guts bndr = do+  anns <- getAnnotations deserializeWithData guts+  return $+    lookupWithDefaultUFM anns [] (varUnique bndr) +++    getModuleAnnotations guts+
+ src/Rattus/Plugin/ScopeCheck.hs view
@@ -0,0 +1,250 @@+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE OverloadedStrings #-}+module Rattus.Plugin.ScopeCheck (checkExpr, emptyCtx) where++import Rattus.Plugin.Utils ++import Prelude hiding ((<>))+import GhcPlugins+import Control.Monad+import Data.Set (Set)+import qualified Data.Set as Set+import Data.Map (Map)+import qualified Data.Map as Map+import Data.Maybe++type LCtx = Set Var+type Hidden = Set Var++data Prim = Prim1 Prim1 | Prim2 Prim2+data Prim1 = Delay | Adv | Box | Unbox | Arr+data Prim2 = DApp | BApp | DAppP | BAppP++instance Outputable Prim1 where+  ppr Delay = "delay"+  ppr Adv = "adv"+  ppr Box = "box"+  ppr Unbox = "unbox"+  ppr Arr = "arr"+  +instance Outputable Prim2 where+  ppr DApp = "<*>"+  ppr BApp = "|*|"+  ppr DAppP = "<**"+  ppr BAppP = "|**"++instance Outputable Prim where+  ppr (Prim1 p) = ppr p+  ppr (Prim2 p) = ppr p++type RecDef = Var++data Ctx = Ctx+  { current :: LCtx,+    hidden :: Hidden,+    earlier :: Maybe LCtx,+    srcLoc :: SrcSpan,+    recDef :: Maybe RecDef,+    hiddenRecs :: Set Var,+    stableTypes :: Set Var,+    primAlias :: Map Var Prim,+    stabilized :: Bool}++primMap :: Map FastString Prim+primMap = Map.fromList+  [("Delay", Prim1 Delay),+   ("delay", Prim1 Delay),+   ("adv", Prim1 Adv),+   ("box", Prim1 Box),+   ("arr", Prim1 Arr),+   ("unbox", Prim1 Unbox),+   ("<*>", Prim2 DApp),+   ("<**", Prim2 DAppP),+   ("|*|", Prim2 BApp),+   ("|**", Prim2 BAppP)+   ]+++isPrim :: Ctx -> Var -> Maybe Prim+isPrim c v+  | Just p <- Map.lookup v (primAlias c) = Just p+  | otherwise = do+  (name,mod) <- getNameModule v+  if isRattModule mod then Map.lookup name primMap+  else Nothing++++stabilize :: Ctx -> Ctx+stabilize c = c+  {current = Set.empty,+   earlier = Nothing,+   hidden = maybe (current c) (Set.union (current c)) (earlier c),+   recDef = Nothing,+   stabilized = True}+++data Scope = Hidden | Visible | ImplUnboxed++getScope  :: Ctx -> Var -> Scope+getScope Ctx{recDef = Just v, earlier = Just _} v'+  -- recursive call under delay+  | v' == v = Visible+getScope Ctx{hiddenRecs = h} v+  -- recursive call that is out of scope+  | (Set.member v h) = Hidden+getScope c v =+  if Set.member v (hidden c) || maybe False (Set.member v) (earlier c)+  then if (isStable (stableTypes c)) (varType v) then Visible+       else Hidden+  else if Set.member v (current c) then Visible+       else if isTemporal (varType v) && isJust (earlier c) && userFunction v+            then ImplUnboxed+            else Visible++++pickFirst :: SrcSpan -> SrcSpan -> SrcSpan+pickFirst s@RealSrcSpan{} _ = s+pickFirst _ s = s++printMessage' :: Severity -> Ctx -> Var -> SDoc -> CoreM ()+printMessage' sev cxt var doc =+  printMessage sev (pickFirst (srcLoc cxt) (nameSrcSpan (varName var))) doc++printMessageCheck :: Severity -> Ctx -> Var -> SDoc -> CoreM Bool+printMessageCheck sev cxt var doc = printMessage' sev cxt var doc >>+  case sev of+    SevError -> return False+    _ -> return True++++emptyCtx :: Maybe Var -> Ctx+emptyCtx mvar=+  Ctx { current =  Set.empty,+        earlier = Nothing,+        hidden = Set.empty,+        srcLoc = UnhelpfulSpan "<no location info>",+        recDef = mvar,+        hiddenRecs = maybe Set.empty Set.singleton mvar,+        primAlias = Map.empty,+        stableTypes = Set.empty,+        stabilized = isJust mvar}+++isPrimExpr :: Ctx -> Expr Var -> Maybe (Prim,Var)+isPrimExpr c (App e (Type _)) = isPrimExpr c e+isPrimExpr c (App e e') | not $ tcIsLiftedTypeKind $ typeKind $ exprType e' = isPrimExpr c e+isPrimExpr c (Var v) = fmap (,v) (isPrim c v)+isPrimExpr c (Tick _ e) = isPrimExpr c e+isPrimExpr c (Lam v e)+  | isTyVar v || (not $ tcIsLiftedTypeKind $ typeKind $ varType v) = isPrimExpr c e+isPrimExpr _ _ = Nothing+++isStableConstr :: Type -> CoreM (Maybe Var)+isStableConstr t = +  case splitTyConApp_maybe t of+    Just (con,[args]) ->+      case getNameModule con of+        Just (name, mod) ->+          if isRattModule mod && name == "Stable"+          then return (getTyVar_maybe args)+          else return Nothing+        _ -> return Nothing                           +    _ ->  return Nothing++checkExpr :: Ctx -> Expr Var -> CoreM Bool+checkExpr c (App e e') | isType e' || (not $ tcIsLiftedTypeKind $ typeKind $ exprType e')+  = checkExpr c e+checkExpr c@Ctx{current = cur, hidden = hid, earlier = earl} (App e1 e2) =+  case isPrimExpr c e1 of+    Just (Prim1 p,v) -> case p of+      Box -> do+        when (stabilized c)  (printMessage' SevWarning c v+          (text "box nested inside another box or recursive definition can cause time leaks"))+        checkExpr (stabilize c) e2+      Arr -> do+        when (stabilized c)  (printMessage' SevWarning c v+          (text "arr nested inside a box or recursive definition can cause time leaks"))+        checkExpr (stabilize c) e2+      Unbox -> checkExpr c e2+      Delay -> case earl of+        Just _ -> printMessageCheck SevError c v (text "cannot delay more than once")+        Nothing -> checkExpr c{current = Set.empty, earlier = Just cur} e2+      Adv -> case earl of+        Just er -> checkExpr c{earlier = Nothing, current = er,+                               hidden = hid `Set.union` cur} e2+        Nothing -> printMessageCheck SevError c v (text "can only advance under delay")+    _ -> liftM2 (&&) (checkExpr c e1)  (checkExpr c e2)+checkExpr c (Case e v _ alts) =+    liftM2 (&&) (checkExpr c e) (liftM and (mapM (\ (_,vs,e)-> checkExpr (addVars vs c') e) alts))+  where c' = addVars [v] c+checkExpr c@Ctx{earlier = Just _} (Lam v _) =+  printMessageCheck SevError c v (text "lambdas may not appear under delay")+checkExpr c (Lam v e)+  | isTyVar v || (not $ tcIsLiftedTypeKind $ typeKind $ varType v) = do+      is <- isStableConstr (varType v)+      let c' = case is of+            Nothing -> c+            Just t -> c{stableTypes = Set.insert t (stableTypes c)}+      checkExpr c' e+  | otherwise = checkExpr (addVars [v] c) e+checkExpr _ (Type _)  = return True+checkExpr _ (Lit _)  = return True+checkExpr _ (Coercion _)  = return True+checkExpr c (Tick (SourceNote span _name) e) =+  checkExpr c{srcLoc = RealSrcSpan span} e+checkExpr c (Tick _ e) = checkExpr c e+checkExpr c (Cast e _) = checkExpr c e+checkExpr c (Let (NonRec v e1) e2) =+  case isPrimExpr c e1 of+    Just (p,_) -> (checkExpr (c{primAlias = Map.insert v p (primAlias c)}) e2)+    Nothing -> liftM2 (&&) (checkExpr c e1)  (checkExpr (addVars [v] c) e2)+checkExpr _ (Let (Rec ([])) _) = return True+checkExpr c (Let (Rec ([(v,e1)])) e2) = do+    when (stabilized c) (printMessage' SevWarning c v+          (text "recursive definition nested inside a box or annother recursive definition can cause time leaks"))+    r1 <- checkExpr c' e1+    r2 <- checkExpr (addVars [v] c) e2+    return (r1 && r2)+  where c' = c {current = Set.empty,+                earlier = Nothing,+                hidden = Set.insert v (maybe (current c) (Set.union (current c)) (earlier c)),+                hiddenRecs = Set.insert v (hiddenRecs c),+                recDef = Just v,+                stabilized = True}+checkExpr c (Let (Rec ((v,_):_)) _) =+          printMessageCheck SevError c v (text "mutual recursive definitions not supported in Rattus")+checkExpr c@Ctx{earlier = earl}  (Var v)+  | tcIsLiftedTypeKind $ typeKind $ varType v =+    case isPrim c v of+      Just (Prim1 _) ->+        printMessageCheck SevError c v (ppr v <> text " must be applied to an argument")+      Just (Prim2 p) ->+        let dapp = case earl of+              Just _ ->+                printMessageCheck SevError c v (ppr v <> text " may not be used under delay")+              _ -> return True+ +        in case p of+             DApp -> dapp+             DAppP -> dapp+             BApp -> return True+             BAppP -> return True+      _ -> case getScope c v of+             Hidden -> printMessageCheck SevError c v (ppr v <> text " is out of scope")+             Visible -> return True+             ImplUnboxed -> printMessageCheck SevWarning c v+                (ppr v <> text " is an external temporal function used under delay, which may cause time leaks")++  | otherwise = return True++++++addVars :: [Var] -> Ctx -> Ctx+addVars v c = c{current = Set.fromList v `Set.union` current c }+
+ src/Rattus/Plugin/StableSolver.hs view
@@ -0,0 +1,63 @@+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE CPP #-}++module Rattus.Plugin.StableSolver (tcStable) where++import Rattus.Plugin.Utils++import Prelude hiding ((<>))+import GhcPlugins+  (Type, Var, CommandLineOption,tyConSingleDataCon,+   mkCoreConApps,getTyVar_maybe)+import CoreSyn+import TcEvidence+import Class++#if __GLASGOW_HASKELL__ >= 810+import Constraint+#endif++import Data.Set (Set)+import qualified Data.Set as Set+++import TcRnTypes++++tcStable :: [CommandLineOption] -> Maybe TcPlugin+tcStable _ = Just $ TcPlugin+  { tcPluginInit = return ()+  , tcPluginSolve = \ () -> stableSolver+  , tcPluginStop = \ () -> return ()+  }++wrap :: Class -> Type -> EvTerm+wrap cls ty = EvExpr appDc+  where+    tyCon = classTyCon cls+    dc = tyConSingleDataCon tyCon+    appDc = mkCoreConApps dc [Type ty]++solveStable :: Set Var -> (Type, (Ct,Class)) -> Maybe (EvTerm, Ct)+solveStable c (ty,(ct,cl))+  | isStable c ty = Just (wrap cl ty, ct)+  | otherwise = Nothing++stableSolver :: [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult+stableSolver given _derived wanted = do+  let chSt = concatMap filterCt wanted+  let haveSt = Set.fromList $ concatMap (filterTypeVar . fst) $ concatMap filterCt given+  case mapM (solveStable haveSt) chSt of+    Just evs -> return $ TcPluginOk evs []+    Nothing -> return $ TcPluginOk [] []++  where filterCt ct@(CDictCan {cc_class = cl, cc_tyargs = [ty]})+          = case getNameModule cl of+              Just (name,mod)+                | isRattModule mod && name == "Stable" -> [(ty,(ct,cl))]+              _ -> []+        filterCt _ = []+        filterTypeVar ty = case getTyVar_maybe ty of+          Just v -> [v]+          Nothing -> []
+ src/Rattus/Plugin/Strictify.hs view
@@ -0,0 +1,72 @@+module Rattus.Plugin.Strictify where+import Prelude hiding ((<>))+import Rattus.Plugin.Utils+import GhcPlugins+++strictifyExpr :: CoreExpr -> CoreM CoreExpr+strictifyExpr (Let (NonRec b e1) e2) = do+  e1' <- strictifyExpr e1+  e2' <- strictifyExpr e2+  return (Let (NonRec b e1') e2')+strictifyExpr (Case e b t alts) = do+  e' <- strictifyExpr e+  alts' <- mapM (\(c,args,e) -> fmap (\e' -> (c,args,e')) (strictifyExpr e)) alts+  return (Case e' b t alts')+strictifyExpr (Let (Rec es) e) = do+  es' <- mapM (\ (b,e) -> strictifyExpr e >>= \e'-> return (b,e')) es+  e' <- strictifyExpr e+  return (Let (Rec es') e')+strictifyExpr (Lam b e) = do+  e' <- strictifyExpr e+  return (Lam b e')+strictifyExpr (Cast e c) = do+  e' <- strictifyExpr e+  return (Cast e' c)+strictifyExpr (Tick t e) = do+  e' <- strictifyExpr e+  return (Tick t e')+strictifyExpr e@(App e1 e2)+  | not (isType e2) && tcIsLiftedTypeKind(typeKind (exprType e2)) && not (isDelayApp e1)+    && not (isDelayApp e2) = do+  e1' <- strictifyExpr e1+  e2' <- strictifyExpr e2+  b <- mkSysLocalM (fsLit "strict") (exprType e2)+  return $ Case e2' b (exprType e) [(DEFAULT, [], App e1' (Var b))]+  | otherwise = do+  e1' <- strictifyExpr e1+  e2' <- strictifyExpr e2+  return (App e1' e2')+strictifyExpr e = return e++++isDelayApp (App e _) = isDelayApp e+isDelayApp (Cast e _) = isDelayApp e+isDelayApp (Tick _ e) = isDelayApp e+isDelayApp (Var v) = isDelayVar v+isDelayApp _ = False+++++isDelayVar :: Var -> Bool+isDelayVar v = maybe False id $ do+  let name = varName v+  mod <- nameModule_maybe name+  let occ = getOccString name+  return ((occ == "Delay" || occ == "delay") || (occ == "Box" || occ == "delay")+          && ((moduleNameString (moduleName mod) == "Rattus.Internal") ||+          moduleNameString (moduleName mod) == "Rattus.Primitives"))++isCase Case{} = True+isCase (Tick _ e) = isCase e+isCase (Cast e _) = isCase e+isCase Lam {} = True+isCase e = isType e++isTophandler (App e1 e2) = isTophandler e1 || isTophandler e2+isTophandler (Cast e _) = isTophandler e+isTophandler (Tick _ e) = isTophandler e+isTophandler e = showSDocUnsafe (ppr e) == "GHC.TopHandler.runMainIO"+
+ src/Rattus/Plugin/Utils.hs view
@@ -0,0 +1,180 @@+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+module Rattus.Plugin.Utils (+  printMessage,+  Severity(..),+  isRattModule,+  isGhcModule,+  getNameModule,+  isStable,+  isTemporal,+  userFunction,+  isType)+  where++import ErrUtils+import Prelude hiding ((<>))+import GhcPlugins+import Data.Set (Set)+import qualified Data.Set as Set+import Data.Char++isType Type {} = True+isType (App e _) = isType e+isType (Cast e _) = isType e+isType (Tick _ e) = isType e+isType _ = False++++-- printMessage :: Severity -> SDoc -> CoreM ()+-- printMessage sev doc =+--   case sev of+--     Error -> errorMsg doc+--     Warning -> warnMsg doc+++-- printMessageV :: Severity -> Var -> SDoc -> CoreM ()+-- printMessageV sev var doc =+--   let loc = nameSrcLoc (varName var)+--       doc' = ppr loc <> text ": " <> doc+--   in case sev of+--     Error -> errorMsg doc'+--     Warning -> warnMsg doc'+++printMessage :: Severity -> SrcSpan -> SDoc -> CoreM ()+printMessage sev loc doc = do+  dflags <- getDynFlags+  unqual <- getPrintUnqualified+  let sty = case sev of+                     SevError   -> err_sty+                     SevWarning -> err_sty+                     SevDump    -> dump_sty+                     _          -> user_sty+      err_sty  = mkErrStyle dflags unqual+      user_sty = mkUserStyle dflags unqual AllTheWay+      dump_sty = mkDumpStyle dflags unqual+  liftIO $ putLogMsg dflags NoReason sev loc sty doc++++rattModules :: Set FastString+rattModules = Set.fromList ["Rattus.Internal","Rattus.Primitives"+                           ,"Rattus.Stable", "Rattus.Arrow"]++isRattModule :: FastString -> Bool+isRattModule = (`Set.member` rattModules)++isGhcModule :: FastString -> Bool+isGhcModule = (== "GHC.Types")+++getNameModule :: NamedThing a => a -> Maybe (FastString, FastString)+getNameModule v = do+  let name = getName v+  mod <- nameModule_maybe name+  return (getOccFS name,moduleNameFS (moduleName mod))+++-- | The set of stable built-in types.+ghcStableTypes :: Set FastString+ghcStableTypes = Set.fromList ["Int","Bool","Float","Double","Char"]+++newtype TypeCmp = TC Type++instance Eq TypeCmp where+  (TC t1) == (TC t2) = eqType t1 t2++instance Ord TypeCmp where+  compare (TC t1) (TC t2) = nonDetCmpType t1 t2++isTemporal :: Type -> Bool+isTemporal t = isTemporalRec 0 Set.empty t+++isTemporalRec :: Int -> Set TypeCmp -> Type -> Bool+isTemporalRec d _ _ | d == 100 = False+isTemporalRec _ pr t | Set.member (TC t) pr = False+isTemporalRec d pr t = do+  let pr' = Set.insert (TC t) pr+  case splitTyConApp_maybe t of+    Nothing -> False+    Just (con,args) ->+      case getNameModule con of+        Nothing -> False+        Just (name,mod)+          -- If it's a Rattus type constructor check if it's a box+          | isRattModule mod && (name == "Box" || name == "O") -> True+          | isFunTyCon con -> or (map (isTemporalRec (d+1) pr') args)+          | isAlgTyCon con -> +            case algTyConRhs con of+              DataTyCon {data_cons = cons} -> or (map check cons)+                where check con = case dataConInstSig con args of+                        (_, _,tys) -> or (map (isTemporalRec (d+1) pr') tys)+              _ -> or (map (isTemporalRec (d+1) pr') args)+        _ -> False+++-- | Check whether the given type is stable. This check may use+-- 'Stable' constraints from the context.++isStable :: Set Var -> Type -> Bool+isStable c t = isStableRec c 0 Set.empty t++-- | Check whether the given type is stable. This check may use+-- 'Stable' constraints from the context.++isStableRec :: Set Var -> Int -> Set TypeCmp -> Type -> Bool+-- To prevent infinite recursion (when checking recursive types) we+-- keep track of previously checked types. This, however, is not+-- enough for non-regular data types. Hence we also have a counter.+isStableRec _ d _ _ | d == 100 = True+isStableRec _ _ pr t | Set.member (TC t) pr = True+isStableRec c d pr t = do+  let pr' = Set.insert (TC t) pr+  case splitTyConApp_maybe t of+    Nothing -> case getTyVar_maybe t of+      Just v -> -- if it's a type variable, check the context+        v `Set.member` c+      Nothing -> False+    Just (con,args) ->+      case getNameModule con of+        Nothing -> False+        Just (name,mod)+          -- If it's a Rattus type constructor check if it's a box+          | isRattModule mod && name == "Box" -> True+            -- If its a built-in type check the set of stable built-in types+          | isGhcModule mod -> name `Set.member` ghcStableTypes+          {- deal with type synonyms (does not seem to be necessary (??))+           | Just (subst,ty,[]) <- expandSynTyCon_maybe con args ->+             isStableRec c (d+1) pr' (substTy (extendTvSubstList emptySubst subst) ty) -}+          | isAlgTyCon con -> +            case algTyConRhs con of+              DataTyCon {data_cons = cons, is_enum = enum}+                | enum -> True+                | and $ concatMap (map isSrcStrict'+                                   . dataConSrcBangs) $ cons ->+                  and  (map check cons)+                | otherwise -> False+                where check con = case dataConInstSig con args of+                        (_, _,tys) -> and (map (isStableRec c (d+1) pr') tys)+              TupleTyCon {} -> null args+              _ -> False+        _ -> False+++          +isSrcStrict' (HsSrcBang _ _ SrcStrict) = True+isSrcStrict' _ = False+++userFunction :: Var -> Bool+userFunction v =+  case getOccString (getName v) of+    (c : _)+      | isUpper c || c == '$' || c == ':' -> False+      | otherwise -> True+    _ -> False
+ src/Rattus/Primitives.hs view
@@ -0,0 +1,88 @@+-- | The language primitives of Rattus. Note that the Rattus types+--  'delay', 'adv', and 'box' are more restrictive that the Haskell+--  types that are indicated. The more stricter Rattus typing rules+--  for these primitives are given. To ensure that your program+--  adheres to these stricter typing rules, use the plugin in+--  "Rattus.Plugin" so that GHC will check these stricter typing+--  rules.++module Rattus.Primitives+  (O+  ,Box+  ,delay+  ,adv+  ,box+  ,unbox+  ,Stable+  ) where+++-- To prevent the user from declaring instances of Stable, we do not+-- export the StableInternal class it depends on.++class StableInternal a where++-- | A type is @Stable@ if it is a strict type and the later modality+-- @O@ and function types only occur under @Box@.+--+-- For example, these types are stable: @Int@, @Box (a -> b)@, @Box (O+-- Int)@, @Box (Str a -> Str b)@.+--+-- But these types are not stable: @[Int]@ (because the list type ist+-- not strict), @Int -> Int@, (function type is not stable), @O+-- Delay@, @Str Int@.+class StableInternal a => Stable a  where++-- | The "later" type modality. A value of type @O a@ is a computation+-- that produces a value of type @a@ in the next time step. Use+-- 'delay' and 'adv' to construct and consume 'O'-types.+data O a = Delay a++-- | The "stable" type modality. A value of type @Box a@ is a+-- time-independent computation that produces a value of type @a@.+-- Use 'box' and 'unbox' to construct and consume 'Box'-types.+data Box a = Box a++-- | This is the constructor for the "later" modality 'O':+--+-- >     Γ ✓ ⊢ t :: 𝜏+-- > --------------------+-- >  Γ ⊢ delay t :: O 𝜏+--+delay :: a -> O a+delay x = Delay x+++-- | This is the eliminator for the "later" modality 'O':+--+-- >     Γ ⊢ t :: O 𝜏+-- > ---------------------+-- >  Γ ✓ Γ' ⊢ adv t :: 𝜏+--+adv :: O a -> a+adv (Delay x) = x+++-- | This is the contructor for the "stable" modality 'Box':+--+-- >     Γ☐ ⊢ t :: 𝜏+-- > --------------------+-- >  Γ ⊢ box t :: Box 𝜏+--+-- where Γ☐ is obtained from Γ by removing ✓ and any variables @x ::+-- 𝜏@, where 𝜏 is not a stable type.+++box :: a -> Box a+box x = Box x++++-- | This is the eliminator for the "stable" modality  'Box':+--+-- >   Γ ⊢ t :: Box 𝜏+-- > ------------------+-- >  Γ ⊢ unbox t :: 𝜏++unbox :: Box a -> a+unbox (Box d) = d
+ src/Rattus/Stream.hs view
@@ -0,0 +1,131 @@+{-# OPTIONS -fplugin=Rattus.Plugin #-}+{-# LANGUAGE TypeOperators #-}++-- | Programming with streams.++module Rattus.Stream+  ( map+  , hd+  , tl+  , const+  , constBox+  , shift+  , shiftMany+  , scan+  , scanMap+  , scanMap2+  , Str(..)+  , zipWith+  , zip+  , unfold+  , filter+  , integral+  )++where++import Rattus+import Prelude hiding (map, const, zipWith, zip, filter)++import Data.VectorSpace++-- | @Str a@ is a stream of values of type @a@.+data Str a = ! a ::: (O (Str a))++-- all functions in this module are in Rattus +{-# ANN module Rattus #-}++-- | Get the first element (= head) of a stream.+hd :: Str a -> a+hd (x ::: _) = x+++-- | Get the tail of a stream, i.e. the remainder after removing the+-- first element.+tl :: Str a -> O (Str a)+tl (_ ::: xs) = xs+++-- | Apply a function to each element of a stream.+map :: Box (a -> b) -> Str a -> Str b+map f (x ::: xs) = unbox f x ::: delay (map f (adv xs))++-- | Construct a stream that has the same given value at each step.+const :: Stable a => a -> Str a+const a = a ::: delay (const a)++-- | Variant of 'const' that allows any type @a@ as argument as long+-- as it is boxed.+constBox :: Box a -> Str a+constBox a = unbox a ::: delay (constBox a)++-- | Construct a stream by repeatedly applying a function to a given+-- start element. That is, @unfold (box f) x@ will produce the stream+-- @x ::: f x ::: f (f x) ::: ...@+unfold :: Stable a => Box (a -> a) -> a -> Str a+unfold f x = x ::: delay (unfold f (unbox f x))++-- | Similar to Haskell's 'scanl'.+--+-- > scan (box f) x (v1 ::: v2 ::: v3 ::: ... ) == (x `f` v1) ::: ((x `f` v1) `f` v2) ::: ...+--+-- Note: Unlike 'scanl', 'scan' starts with @x `f` v1@, not @x@.+scan :: (Stable b) => Box(b -> a -> b) -> b -> Str a -> Str b+scan f acc (a ::: as) =  acc' ::: delay (scan f acc' (adv as))+  where acc' = unbox f acc a++-- | 'scanMap' is a composition of 'map' and 'scan':+--+-- > scanMap f g x === map g . scan f x+scanMap :: (Stable b) => Box(b -> a -> b) -> Box (b -> c) -> b -> Str a -> Str c+scanMap f p acc (a ::: as) =  unbox p acc' ::: delay (scanMap f p acc' (adv as))+  where acc' = unbox f acc a++++-- | 'scanMap2' is similar to 'scanMap' but takes two input streams.+scanMap2 :: (Stable b) => Box(b -> a1 -> a2 -> b) -> Box (b -> c) -> b -> Str a1 -> Str a2 -> Str c+scanMap2 f p acc (a1 ::: as1) (a2 ::: as2) =+    unbox p acc' ::: delay (scanMap2 f p acc' (adv as1) (adv as2))+  where acc' = unbox f acc a1 a2++-- | Similar to 'Prelude.zipWith' on Haskell lists.+zipWith :: Box(a -> b -> c) -> Str a -> Str b -> Str c+zipWith f (a ::: as) (b ::: bs) = unbox f a b ::: delay (zipWith f (adv as) (adv bs))++-- | Similar to 'Prelude.zip' on Haskell lists.+zip :: Str a -> Str b -> Str (a:*b)+zip (a ::: as) (b ::: bs) =  (a :* b) ::: delay (zip (adv as) (adv bs))+++-- | Filter out elements from a stream according to a predicate.+filter :: Box(a -> Bool) -> Str a -> Str(Maybe' a)+filter p = map (box (\a -> if unbox p a then Just' a else Nothing'))++{-| Given a value a and a stream as, this function produces a stream+  that behaves like -}+shift :: Stable a => a -> Str a -> Str a+shift a (x ::: xs) = a ::: delay (shift x (adv xs))+++{-| Given a list @[a1, ..., an]@ of elements and a stream @xs@ this+  function constructs a stream that starts with the elements @a1, ...,+  an@, and then proceeds as @xs@. In particular, this means that the+  ith element of the original stream @xs@ is the (i+n)th element of+  the new stream. In other words @shiftMany@ behaves like reapeatedly+  applying @shift@ for each element in the list. -}+shiftMany :: Stable a => List a -> Str a -> Str a+shiftMany l xs = run l Nil xs where+  run :: Stable a => List a -> List a -> Str a -> Str a+  run (b :! bs) buf (x ::: xs) = b ::: delay (run bs (x :! buf) (adv xs))+  run Nil buf (x ::: xs) =+    case reverse' buf of+      b :! bs -> b ::: delay (run bs (x :! Nil) (adv xs))+      Nil -> x ::: xs+    +-- | Calculates an approximation of an integral of the stream of type+-- @Str a@ (the y-axis), where the stream of type @Str s@ provides the+-- distance between measurements (i.e. the distance along the y axis).+integral :: (Stable a, VectorSpace a s) => a -> Str s -> Str a -> Str a+integral acc (t ::: ts) (a ::: as) = acc' ::: delay (integral acc' (adv ts) (adv as))+  where acc' = acc ^+^ (t *^ a)
+ src/Rattus/Strict.hs view
@@ -0,0 +1,91 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE MultiParamTypeClasses #-}++-- | This module contains strict versions of some standard data+-- structures.++++module Rattus.Strict+  ( List(..),+    reverse',+    (:*)(..),+    Maybe'(..),+   fst',+   snd',+  )where++import Data.VectorSpace++infixr 2 :*++-- | Strict list type.+data List a = Nil | !a :! !(List a)++-- | Reverse a list.+reverse' :: List a -> List a+reverse' l =  rev l Nil+  where+    rev Nil     a = a+    rev (x:!xs) a = rev xs (x:!a)++instance Foldable List where+  +  foldMap f = run where+    run Nil = mempty+    run (x :! xs) = f x <> run xs+  foldr f = run where+    run b Nil = b+    run b (a :! as) = (run $! (f a b)) as+  foldl f = run where+    run a Nil = a+    run a (b :! bs) = (run $! (f a b)) bs+  elem a = run where+    run Nil = False+    run (x :! xs)+      | a == x = True+      | otherwise = run xs+    +  +instance Functor List where+  fmap f = run where+    run Nil = Nil+    run (x :! xs) = f x :! run xs+++-- | Strict variant of 'Maybe'.+data Maybe' a = Just' ! a | Nothing'++-- | Strict pair type.+data a :* b = !a :* !b++-- | First projection function.+fst' :: (a :* b) -> a+fst' (a:*_) = a++-- | Second projection function.+snd' :: (a :* b) -> b+snd' (_:*b) = b+++instance RealFloat a => VectorSpace (a :* a) a where+    zeroVector = 0 :* 0++    a *^ (x :* y) = (a * x) :* (a * y)++    (x :* y) ^/ a = (x / a) :* (y / a)++    negateVector (x :* y) = (-x) :* (-y)++    (x1 :* y1) ^+^ (x2 :* y2) = (x1 + x2) :* (y1 + y2)++    (x1 :* y1) ^-^ (x2 :* y2) = (x1 - x2) :* (y1 - y2)++    (x1 :* y1) `dot` (x2 :* y2) = x1 * x2 + y1 * y2++instance Functor ((:*) a) where+  fmap f (x:*y) = (x :* f y)+  +instance (Show a, Show b) => Show (a:*b) where+  show (a :* b) = "(" ++ show a ++ " :* " ++ show b ++ ")"
+ src/Rattus/ToHaskell.hs view
@@ -0,0 +1,55 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TypeFamilies #-}++-- | Helper functions to convert streams and signal functions from+-- Rattus into Haskell.++module Rattus.ToHaskell+  (runTransducer,+   runSF,+   fromStr,+   toStr,+   Trans(..)+  ) where++import System.IO.Unsafe+import Data.IORef+import Rattus.Primitives+import Rattus.Stream+import Rattus.Yampa+++-- | A state machine that takes inputs of type @a@ and produces output+-- of type @b@. In addition to the ouptut of type @b@ the underlying+-- function also returns the new state of the state machine.+data Trans a b = Trans (a -> (b, Trans a b))++-- | Turn a stream function into a state machine.+runTransducer :: (Str a -> Str b) -> Trans a b+runTransducer tr = Trans run+  where run a = unsafePerformIO $ do+          asR <- newIORef undefined+          as <- unsafeInterleaveIO $ readIORef asR+          let b ::: bs = tr (a ::: delay as)+          return (b, Trans (run' (adv bs) asR))+        run' bs asR a = unsafePerformIO $ do+          asR' <- newIORef undefined+          as' <- unsafeInterleaveIO $ readIORef asR'+          writeIORef asR (a ::: delay as')+          let b ::: bs' = bs+          return (b, Trans (run' (adv bs') asR'))++-- | Turn a signal function into a state machine from inputs of type+-- @a@ and time (since last input) to output of type @b@.+runSF :: SF a b -> Trans (a, Double) b+runSF sf = Trans (\(a,t) -> let (s, b) = stepSF sf t a in (b, runSF (adv s)))+++-- | Turns a lazy infinite list into a stream.+toStr :: [a] -> Str a+toStr (x : xs) = x ::: delay (toStr xs)+toStr _ = error "runRatt: input terminated"++-- | Turns a stream into a lazy infinite list.+fromStr :: Str a -> [a]+fromStr (x ::: xs) = x : fromStr (adv xs)
+ src/Rattus/Yampa.hs view
@@ -0,0 +1,207 @@+{-# OPTIONS -fplugin=Rattus.Plugin #-}+{-# LANGUAGE Arrows #-}+{-# LANGUAGE RebindableSyntax #-}++-- | A simply Yampa-like library for signal functions.++module Rattus.Yampa (+  SF,+  identity,+  compose,+  switch,+  rSwitch,+  constant,+  loopPre,+  stepSF,+  initially,+  integral,+  (-->),+  (-:>),+  (>--),+  (-=>),+  (>=-),+  (^>>),+  (>>^),+  (<<^),+  (^<<),+  module Rattus.Arrow, (>>>)) where++import Rattus.Primitives+import Rattus.Plugin+import Rattus.Strict++import GHC.Float+import Control.Category+import Rattus.Arrow+import Prelude hiding (id)++import Data.VectorSpace++-- all functions in this module are in Rattus +{-# ANN module Rattus #-}++type DTime = Double ++-- | Signal functions from inputs of type @a@ to outputs of type @b@.+data SF a b = SF{+  -- | Run a signal function for one step.+  stepSF :: DTime -> a -> (O(SF a b), b)}++-- | The identity signal function that does nothing.+identity :: SF a a+identity = SF (\ _ x -> (delay identity,x))++-- | Compose two signal functions.+compose :: SF b c -> SF a b -> SF a c+compose (SF sf2) (SF sf1) = SF sf+  where sf d a = let (r1, b) = sf1 d a+                     (r2, c) = sf2 d b+                 in (delay (compose (adv r2) (adv r1)), c)++-- | Compute the integral of a signal. The first argument is the+-- offset.+integral :: (Stable a, VectorSpace a s) => a -> SF a a+integral acc = SF sf'+  where sf' t a = let acc' = acc ^+^ (realToFrac t *^ a)+                  in (delay (integral acc'), acc')++-- | @switch s f@ behaves like @s@ composed with @arr fst@ until @s@+-- produces a value of the form @Just' c@ in the second+-- component. From then on it behaves like $f c@.+switch :: SF a (b, Maybe' c) -> Box (c -> SF a b) -> SF a b+switch (SF sf) f = SF sf'+  where sf' t a = let (nxt, (b,c')) =  sf t a+                  in case c' of+                       Just' c -> stepSF (unbox f c) t a+                       Nothing' -> (delay (switch (adv nxt) f), b)++-- | @rSwitch s@ behaves like @s@, but every time the second input is+-- of the form @Just' s'@ it will change behaviour to @s'@.+rSwitch :: SF a b -> SF (a, Maybe' (SF a b)) b+rSwitch (SF sf) = SF sf'+  where sf' t (a,m) = case m of+                        Just' (SF newSf) ->+                           let (nxt, b) = newSf t a+                           in (delay (rSwitch (adv nxt)),b)+                        Nothing' -> let (nxt, b) = sf t a+                                   in (delay (rSwitch (adv nxt)),b)++-- | Constant signal function.+constant :: Stable b => b -> SF a b+constant x = run+  where run = SF (\ _ _ -> (delay run,x))++-- | The output at time zero is the first argument, and from that+-- point on it behaves like the signal function passed as second+-- argument.+(-->) :: b -> SF a b -> SF a b+b --> (SF sf) = SF sf'+  where sf' d x = (fst (sf d x),b)++-- | Insert a sample in the output, and from that point on, behave+-- like the given signal function.+--+-- Note: The type of -:> is different from Yampa's: The second+-- argument must be delayed (or boxed).+(-:>) :: b -> O (SF a b) -> SF a b+b -:> sf = SF sf'+  where sf' _d _x = (sf,b)++-- | The input at time zero is the first argument, and from that point+-- on it behaves like the signal function passed as second argument.+(>--) :: a -> SF a b -> SF a b+a >-- (SF sf) = SF sf'+  where sf' d _a = sf d a+++-- | Apply a function to the first output value at time+-- zero.+(-=>) :: (b -> b) -> SF a b -> SF a b+f -=> (SF sf) = SF sf'+  where sf' d a = let (r,b) = sf d a+                  in (r,f b)+                     +-- | Apply a function to the first input value at time+-- zero.+(>=-) :: (a -> a) -> SF a b -> SF a b+f >=- (SF sf) = SF sf'+  where sf' d a = sf d (f a)++-- | Override initial value of input signal.++initially :: a -> SF a a+initially = (--> identity)++-- | Lift a function to a signal function (applied pointwise).+-- +-- Note: The type of is different from Yampa's: The function argument+-- must be boxed.+arrPrim :: Box (a -> b) -> SF a b+arrPrim f = run where+  run = SF (\ _d a -> (delay run, unbox f a ))+++-- | Apply a signal function to the first component.+firstPrim :: SF a b -> SF (a,c) (b,c)+firstPrim (SF sf) = SF sf'+  where sf' d (a,c) = let (r, b) = sf d a+                      in (delay (firstPrim (adv r)), (b,c))++-- | Apply a signal function to the second component.+secondPrim :: SF a b -> SF (c,a) (c,b)+secondPrim (SF sf) = SF sf'+  where sf' d (c,a) = let (r, b) = sf d a+                      in (delay (secondPrim (adv r)), (c,b))+++-- | Apply two signal functions in parallel.+parSplitPrim :: SF a b -> SF c d  -> SF (a,c) (b,d)+parSplitPrim (SF sf1) (SF sf2) = SF sf'+  where sf' dt (a,c) = let (r1, b) = sf1 dt a+                           (r2, d) = sf2 dt c+                       in (delay (parSplitPrim (adv r1) (adv r2)), (b,d))++-- | Apply two signal functions in parallel on the same input.+parFanOutPrim :: SF a b -> SF a c -> SF a (b, c)+parFanOutPrim (SF sf1) (SF sf2) = SF sf'+  where sf' dt a = let (r1, b) = sf1 dt a+                       (r2, c) = sf2 dt a+                   in (delay (parFanOutPrim (adv r1) (adv r2)), (b,c))++instance Category SF where+  id = identity+  (.) = compose++instance Arrow SF where+  arrBox = arrPrim+  first = firstPrim+  second = secondPrim+  (***) = parSplitPrim+  (&&&) = parFanOutPrim+++-- | Loop with an initial value for the signal being fed back.+-- +-- Note: The type of @loopPre@ is different from Yampa's as we need+-- the @O@ type here.+loopPre :: c -> SF (a,c) (b,O c) -> SF a b+loopPre c (SF sf) = SF sf'+  where sf' d a = let (r, (b,c')) = sf d (a,c)+                  in (delay (loopPre (adv c') (adv r)), b)+++-- | Precomposition with a pure function.+(^>>) :: Arrow a => Box (b -> c) -> a c d -> a b d+f ^>> a = arrBox f >>> a++-- | Postcomposition with a pure function.+(>>^) :: Arrow a => a b c -> Box (c -> d) -> a b d+a >>^ f = a >>> arrBox f++-- | Precomposition with a pure function (right-to-left variant).+(<<^) :: Arrow a => a c d -> Box (b -> c) -> a b d+a <<^ f = a <<< arrBox f++-- | Postcomposition with a pure function (right-to-left variant).+(^<<) :: Arrow a => Box (c -> d) -> a b c -> a b d+f ^<< a = arrBox f <<< a
+ test/IllTyped.hs view
@@ -0,0 +1,62 @@++module Main (module Main) where++import Rattus+import Rattus.Stream+import Prelude hiding ((<*>), map, const)++-- Uncomment the annotation below to check that the definitions in+-- this module don't type check++-- {-# ANN module Rattus #-}++bar1 :: Box (a -> b) -> Str a -> Str b+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)+++dblDelay :: Box (O (O Int))+dblDelay = box (delay (delay 1))++lambdaUnderDelay :: Box (O (O Int -> Int -> Int))+lambdaUnderDelay = box (delay (\x _ -> adv x))++leaky :: (() -> Bool) -> Str Bool+leaky p = p () ::: delay (leaky (\ _ -> hd (leaky (\ _ -> True))))++grec :: Int+grec = grec++zeros :: Box (Str Int)+zeros = box (0 ::: delay (unbox zeros))++constUnstable :: a -> Str a+constUnstable a = run+  where run = a ::: delay run++mapUnboxed :: (a -> b) -> Str a -> Str b+mapUnboxed f = run+  where run (x ::: xs) = f x ::: delay (run (adv xs))+++data Input = Input {jump :: !Bool, move :: Move}+data Move = StartLeft | EndLeft | StartRight | EndRight | NoMove++-- Input is not a stable type (it is not strict). Therefore this+-- should not type check.+constS :: Input -> Str Input+constS a = a ::: delay (constS a)+++-- Since Input is not strict, we cannot instantiate the 'const'+-- function.+-- Uncomment the definition below to check this.++-- constS' :: Input -> Str Input+-- constS' = const+++{-# ANN main NotRattus #-}+main = putStrLn "This file should not type check"
+ test/MemoryLeak.hs view
@@ -0,0 +1,84 @@+{-# LANGUAGE TypeOperators #-}+module Main (module Main) where++import Rattus+import Rattus.Stream+import Rattus.ToHaskell++import qualified Prelude+import Prelude hiding ((<*>), map)++-- If we make pairs stable, we get a memory leak:+-- cannot do this anymore. We dissallow user-supplied Stable instances+-- instance (Stable a, Stable b) => Stable (a,b)+++type Lazy a = ((),a)++{-# ANN module Rattus #-}+++lazyAdd :: (a, Int) -> ((), Int) -> ((), Int)+lazyAdd = (\ (_,x) y -> fmap (+x) y )+++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)+  where acc' = unbox f acc a+++-- Unless the strictification transformation is applied this function+-- will leak memory.+test1 :: Int -> Str (Int) -> Str (Int)+test1 = scan3 (box (+)) (box (== 0))++++-- Unless the strictification transformation is applied this function+-- will leak memory. In addition, since it uses a lazy data structure,+-- it would also leak memory unless progres/promote evaluate to normal+-- form (using deepseq).+-- test2 :: Lazy Int -> Str (Lazy Int) -> Str (Lazy Int)+-- test2 = scan3 (box lazyAdd) (box (\ (_,x) -> x == 0))++-- If we Haskell's pair types, we get a memory leak:++leaky :: Str (Lazy Int) -> Str (Lazy Int)+leaky ((_,x):::xs) = ((),1) ::: delay (leaky  (fmap ((+) x) (hd (adv xs)) ::: (tl (adv xs))))+++type Strict a = (():*a)++leakyStrict :: Str (Strict Int) -> Str (Strict Int)+leakyStrict ((_:*x):::xs) = (():*11) ::: delay (leakyStrict  (fmap ((+) x) (hd (adv xs)) ::: (tl (adv xs))))+++buffer :: Stable a => Str a -> Str (List a)+buffer = scan (box (flip (:!))) Nil+++{-# ANN recurse NotRattus #-}+recurse 0 (x : _) = print x+recurse n (_ : xs) = recurse (n-1) xs+recurse _ [] = putStrLn "the impossible happened: stream terminated"++{-# ANN main NotRattus #-}+main = do  +  let x =  fromStr $ test1 1 (toStr [1..])+  recurse 10000000 x+  +  let x = fromStr $ leakyStrict  (toStr $ Prelude.map (\ x-> (():*x)) [1..])+  recurse 10000000 x+++  let x = fromStr $ leaky (toStr $ Prelude.map (\ x-> ((),x)) [1..])+  recurse 10000000 x+  +--   -- for comparison the Haskell code below does leak+--   let x = scan2 (+) (1::Int) [1,1..]+--   recurse 10000000 x++-- {-# ANN scan2 NotRattus #-}+-- scan2 :: (Int -> Int -> Int) -> Int -> [Int] -> [Int]+-- scan2 f acc (a : as) =  (if a == 0 then acc else 0) : scan2 f (f acc a) as
+ test/TimeLeak.hs view
@@ -0,0 +1,106 @@+{-# LANGUAGE TypeOperators #-}+module Main (module Main) where++import Rattus+import Rattus.Stream+import Rattus.ToHaskell++import Prelude hiding ((<*>), map)+++{-# ANN module Rattus #-}+++nats' :: Str Int+nats' = unfold (box ((+) 1)) 0+++nats :: Str Int+nats = from  0+    where from :: Int -> Str Int+          from n = n ::: delay (from (n+1))++-- This function should cause a warning.+leakyNats :: Str Int+leakyNats = 0 ::: delay (map (box (+1)) leakyNats)++inc :: Str Int -> Str Int+inc = map (box ((+)1))++-- This function should cause a warning.++leakyNats' :: Str Int+leakyNats' = 0 ::: delay (inc leakyNats')++++altMap :: Box (a -> b) -> Box (a -> b) -> Str a -> Str b+altMap f g (x ::: xs) = unbox f x ::: delay (altMap g f (adv xs))++-- This function should cause a warning.+leakyAlt :: Str Int+leakyAlt = 0 ::: delay (altMap (box ((+)1)) (box ((+)2)) leakyAlt)++++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)))++-- This function should cause a warning.+leakyMap :: Str Int+leakyMap = 0 ::: delay (mapMap (box ((+)1)) (box ((+)2)) leakyMap)++++-- This function should cause a warning.+boxLeaky :: Str Int+boxLeaky = run (box (\() -> 1)) 1+  where run :: Box (() -> Int) -> Int -> Str Int+        run f a = (if a == 0 then unbox f () else a)+                  ::: delay (run (box (\ () -> (unbox f () + 1))) a)++-- This function should cause a warning.+boxLeaky' :: Str Int -> Str Int+boxLeaky' = run (box (\() -> 1)) 1+  where run :: Box (() -> Int) -> Int -> Str Int -> Str Int+        run f a (x ::: xs) = (if a == 0 then unbox f () else a) ::: delay (run (box (\ () -> (unbox f () + x))) a (adv xs))+++natsTrans :: Str Int -> Str Int+natsTrans (x ::: xs) = x ::: delay (map (box ((+)x)) $ natsTrans $ adv xs)+ +leakySum :: Box (Int -> Int) -> Str Int -> Str Int+leakySum f (x ::: xs) = unbox f x ::: (delay (leakySum (box (\ y -> unbox f (y + x)))) <*> xs)+++{-# ANN recurse NotRattus #-}+recurse 0 (x : _) = print x+recurse n (_ : xs) = recurse (n-1) xs+recurse _ [] = putStrLn "the impossible happened: stream terminated"++{-# ANN main NotRattus #-}+main = do+  let x = fromStr nats+  recurse 10000000 x+    +  let x = fromStr leakyNats+  recurse 10000000 x++  let x = fromStr leakyNats'+  recurse 10000000 x++  let x = fromStr leakyAlt+  recurse 10000000 x++  let x = fromStr leakyMap+  recurse 10000 x++  let x = fromStr $ natsTrans (toStr [1..])+  recurse 10000 x++  let x = fromStr $ boxLeaky' (toStr [1..])+  recurse 10000000 x++  let x = fromStr boxLeaky+  recurse 10000000 x+
+ test/WellTyped.hs view
@@ -0,0 +1,75 @@+module Main (module Main) where++import Rattus+import Rattus.Stream+import Prelude hiding ((<*>))+import Data.Set+import qualified Data.Set as Set+++{-# ANN module Rattus #-}++map1 :: Box (a -> b) -> Str a -> Str b+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)++map3 :: Box (a -> b) -> Str a -> Str b+map3 f = run+  where run (x ::: xs) = unbox f x ::: (delay run <*> xs)+++data Input a = Input {jump :: !a, move :: !Move}+data Move = StartLeft | EndLeft | StartRight | EndRight | NoMove++type Inp a b = Input a++++-- The compiler plugin should detect that Input is a stable type and+-- thus remains in scope under the delay.+constS :: Stable a => (Inp a b) -> Str (Inp a b)+constS a = a ::: delay (constS a)++-- The constraint solver plugin should detect that Input is a stable+-- type and thus 'const1' can be instantiated.+constS' :: Stable a => Inp a b -> Str (Inp a b)+constS' = const1++-- make sure that unit is recognized as stable+constU :: () -> Str ()+constU a = a ::: delay (constU a)++constU' :: () -> Str ()+constU' = const1+++const1 :: Stable a => a -> Str a+const1 a = a ::: delay (const1 a)++const2 :: Stable a => a -> Str a+const2 a = run+  where run = a ::: delay run++scan1 :: (Stable b) => Box(b -> a -> b) -> b -> Str a -> Str b+scan1 f acc (a ::: as) =  acc' ::: delay (scan1 f acc' (adv as))+  where acc' = unbox f acc a++scan2 :: (Stable b) => Box(b -> a -> b) -> b -> Str a -> Str b+scan2 f = run+  where run acc (a ::: as) = let acc' = unbox f acc a+                             in acc' ::: delay (run acc' (adv as))++scanSet :: Str Int -> Str (Set Int)+scanSet = scan1 (box (\ s x -> Set.insert x s)) Set.empty++from :: Int -> Str Int+from n  = n ::: delay (from (n+1))++alt :: Int -> Int -> Str Int+alt n m = n ::: delay (alt m n)+++{-# ANN main NotRattus #-}+main = putStrLn "This file should just type check"