Rattus 0.1.0.0 → 0.1.1.0
raw patch · 11 files changed
+165/−79 lines, 11 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
Files
- CHANGELOG.md +6/−0
- Rattus.cabal +36/−5
- src/Rattus/Event.hs +2/−2
- src/Rattus/Events.hs +1/−1
- src/Rattus/Plugin.hs +11/−12
- src/Rattus/Plugin/ScopeCheck.hs +80/−44
- src/Rattus/Primitives.hs +6/−5
- src/Rattus/Stream.hs +1/−1
- src/Rattus/ToHaskell.hs +2/−2
- test/IllTyped.hs +13/−7
- test/WellTyped.hs +7/−0
CHANGELOG.md view
@@ -1,3 +1,9 @@+0.1.1.0+-------++- allow mutual guarded recursion+- improve type error messages+ 0.1.0.0 ------- initial release
Rattus.cabal view
@@ -1,6 +1,6 @@ cabal-version: 1.18 name: Rattus-version: 0.1.0.0+version: 0.1.1.0 category: FRP synopsis: A modal FRP language description:@@ -11,7 +11,7 @@ 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>.+ <src/docs/paper.pdf paper>. . @@ -36,6 +36,31 @@ . + For example, the type of streams is defined as++ .++ > data Str a = a ::: (O (Str a))++ .++ So the head of the stream is available now, but its tail+ is only available in the next time step. Writing a @map@+ function for this type of streams, requires us to use the+ @Box@ modality:++ .++ > map :: Box (a -> b) -> Str a -> Str b+ > map f (x ::: xs) = unbox f x ::: delay (map f (adv xs))++ .++ This makes sure that the function @f@ that we give to+ @map@ is available at any time in the future.++ .+ 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@@ -52,8 +77,8 @@ . - In addition, one must mark the functions that are written- in Rattus:+ In addition, one must annotate the functions that are+ written in Rattus: . @@ -61,7 +86,7 @@ . - Or mark the whole module as a Rattus module:+ Or annotate the whole module as a Rattus module: . @@ -82,6 +107,12 @@ > {-# ANN sums Rattus #-} > sums :: Str Int -> Str Int > sums = scan (box (+)) 0++ .++ The + <docs/src/Rattus.Stream.html source code of the Rattus.Stream module>+ provides more examples on how to program in Rattus. homepage: https://github.com/pa-ba/Rattus License: BSD3
src/Rattus/Event.hs view
@@ -1,7 +1,7 @@ {-# OPTIONS -fplugin=Rattus.Plugin #-} {-# LANGUAGE TypeOperators #-} --- | Programing with single shot events, i.e. events that may occur at+-- | Programming with single shot events, i.e. events that may occur at -- most once. module Rattus.Event@@ -81,7 +81,7 @@ 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+-- | 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)
src/Rattus/Events.hs view
@@ -1,6 +1,6 @@ {-# OPTIONS -fplugin=Rattus.Plugin #-} --- | Programing with many-shot events, i.e. events that may occur zero+-- | Programming with many-shot events, i.e. events that may occur zero -- or more times.
src/Rattus/Plugin.hs view
@@ -13,6 +13,7 @@ import Prelude hiding ((<>)) import GhcPlugins +import qualified Data.Set as Set import Control.Monad import Data.Maybe import Data.Data hiding (tyConName)@@ -67,19 +68,17 @@ 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')])+ [] -> return (Just $ Rec [])+ binds -> do+ let vs = map fst binds+ let es = map snd binds+ let vs' = Set.fromList vs+ valid <- mapM (\ (v,e) -> checkExpr (emptyCtx (Just (vs', v))) e) binds+ if and valid then do+ es' <- mapM strictifyExpr es+ return (Just $ Rec (zip vs es')) 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
src/Rattus/Plugin/ScopeCheck.hs view
@@ -14,7 +14,8 @@ import Data.Maybe type LCtx = Set Var-type Hidden = Set Var+data HiddenReason = BoxApp | AdvApp | NestedRec Var+type Hidden = Map Var HiddenReason data Prim = Prim1 Prim1 | Prim2 Prim2 data Prim1 = Delay | Adv | Box | Unbox | Arr@@ -37,15 +38,15 @@ ppr (Prim1 p) = ppr p ppr (Prim2 p) = ppr p -type RecDef = Var+type RecDef = Set Var data Ctx = Ctx { current :: LCtx, hidden :: Hidden,+ hiddenRec :: Hidden, earlier :: Maybe LCtx, srcLoc :: SrcSpan,- recDef :: Maybe RecDef,- hiddenRecs :: Set Var,+ recDef :: Maybe (RecDef,Var), stableTypes :: Set Var, primAlias :: Map Var Prim, stabilized :: Bool}@@ -75,32 +76,58 @@ -stabilize :: Ctx -> Ctx-stabilize c = c+stabilize :: HiddenReason -> Ctx -> Ctx+stabilize hr c = c {current = Set.empty, earlier = Nothing,- hidden = maybe (current c) (Set.union (current c)) (earlier c),+ 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 = True}+ where ctxHid = maybe (current c) (Set.union (current c)) (earlier c) -data Scope = Hidden | Visible | ImplUnboxed+data Scope = Hidden SDoc | 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+getScope Ctx{recDef = Just (vs, recV), earlier = e} v+ | v `Set.member` vs =+ case e of+ Just _ -> Visible+ Nothing + | recV == v -> Hidden ("Recursive call to " <> ppr v <> " must occur under delay")+ | otherwise -> Hidden ("Mutually recursice call to " <> ppr v <> " must occur under delay")+ +--getScope Ctx{hiddenRecs = h} v -- recursive call that is out of scope- | (Set.member v h) = Hidden+-- | (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+ case Map.lookup v (hiddenRec c) of+ Just (NestedRec rv) -> Hidden ("Recursive call to" <> ppr v <>+ " is not allowed as it occurs in a local recursive definiton (namely of " <> ppr rv <> ")")+ Just BoxApp -> Hidden ("Recursive call to " <> ppr v <> " is not allowed since it occurs under a box")+ 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 c) of+ Just (NestedRec rv) ->+ if (isStable (stableTypes c) (varType v)) then Visible+ else Hidden ("Variable " <> ppr v <> " is no longer in scope:" $$+ "It appears in a local recursive definiton (namely of " <> ppr rv <> ")"+ $$ "and is of type " <> ppr (varType v) <> ", which is not stable.")+ Just BoxApp ->+ if (isStable (stableTypes c) (varType v)) then Visible+ else Hidden ("Variable " <> ppr v <> " is no longer in scope:" $$+ "It occurs under " <> keyword "box" $$ "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.")+ Nothing+ | maybe False (Set.member v) (earlier c) ->+ if isStable (stableTypes c) (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 c) -> Visible+ | isTemporal (varType v) && isJust (earlier c) && userFunction v+ -> ImplUnboxed+ | otherwise -> Visible @@ -120,14 +147,14 @@ -emptyCtx :: Maybe Var -> Ctx-emptyCtx mvar=+emptyCtx :: Maybe (Set Var,Var) -> Ctx+emptyCtx mvar = Ctx { current = Set.empty, earlier = Nothing,- hidden = Set.empty,+ hidden = Map.empty,+ hiddenRec = Map.empty, srcLoc = UnhelpfulSpan "<no location info>", recDef = mvar,- hiddenRecs = maybe Set.empty Set.singleton mvar, primAlias = Map.empty, stableTypes = Set.empty, stabilized = isJust mvar}@@ -162,27 +189,33 @@ case isPrimExpr c e1 of Just (Prim1 p,v) -> case p of Box -> do- when (stabilized c) (printMessage' SevWarning c v+ ch <- checkExpr (stabilize BoxApp c) e2+ -- don't bother with a warning if the scopecheck fails+ when (ch && stabilized c) (printMessage' SevWarning c v (text "box nested inside another box or recursive definition can cause time leaks"))- checkExpr (stabilize c) e2+ return ch Arr -> do- when (stabilized c) (printMessage' SevWarning c v+ ch <- checkExpr (stabilize BoxApp c) e2+ -- don't bother with a warning if the scopecheck fails+ when (ch && stabilized c) (printMessage' SevWarning c v (text "arr nested inside a box or recursive definition can cause time leaks"))- checkExpr (stabilize c) e2+ return ch+ 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+ hidden = hid `Map.union` Map.fromSet (const AdvApp) 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")+ printMessageCheck SevError c v (text "Functions may not be defined under delay."+ $$ "In order to define a function under delay, you have to wrap it in box.") checkExpr c (Lam v e) | isTyVar v || (not $ tcIsLiftedTypeKind $ typeKind $ varType v) = do is <- isStableConstr (varType v)@@ -203,20 +236,23 @@ 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+checkExpr c (Let (Rec binds) e2) = do+ r1 <- mapM (\ (v,e) -> checkExpr (c' v) e) binds+ r2 <- checkExpr (addVars vs c) e2+ let r = (and r1 && r2) + when (r && stabilized c) (printMessage' SevWarning c (head vs) (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")+ return r+ where vs = map fst binds+ vs' = Set.fromList vs+ ctxHid = maybe (current c) (Set.union (current c)) (earlier c)+ recHid = maybe ctxHid (Set.union ctxHid . fst) (recDef c)+ c' v = c {current = Set.empty,+ earlier = Nothing,+ hidden = hidden c `Map.union`+ (Map.fromSet (const (NestedRec v)) recHid),+ recDef = Just (vs',v),+ stabilized = True} checkExpr c@Ctx{earlier = earl} (Var v) | tcIsLiftedTypeKind $ typeKind $ varType v = case isPrim c v of@@ -234,7 +270,7 @@ BApp -> return True BAppP -> return True _ -> case getScope c v of- Hidden -> printMessageCheck SevError c v (ppr v <> text " is out of scope")+ Hidden reason -> printMessageCheck SevError c v reason Visible -> return True ImplUnboxed -> printMessageCheck SevWarning c v (ppr v <> text " is an external temporal function used under delay, which may cause time leaks")
src/Rattus/Primitives.hs view
@@ -17,8 +17,8 @@ ) where --- To prevent the user from declaring instances of Stable, we do not--- export the StableInternal class it depends on.+-- | To prevent the user from declaring instances of Stable, we do not+-- export the 'StableInternal' class it depends on. class StableInternal a where @@ -28,9 +28,10 @@ -- 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+-- But these types are not stable: @[Int]@ (because the list type is -- not strict), @Int -> Int@, (function type is not stable), @O--- Delay@, @Str Int@.+-- Int@, @Str Int@.+ class StableInternal a => Stable a where -- | The "later" type modality. A value of type @O a@ is a computation@@ -63,7 +64,7 @@ adv (Delay x) = x --- | This is the contructor for the "stable" modality 'Box':+-- | This is the constructor for the "stable" modality 'Box': -- -- > Γ☐ ⊢ t :: 𝜏 -- > --------------------
src/Rattus/Stream.hs view
@@ -112,7 +112,7 @@ 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+ the new stream. In other words @shiftMany@ behaves like repeatedly 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
src/Rattus/ToHaskell.hs view
@@ -20,7 +20,7 @@ -- | 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+-- of type @b@. In addition to the output 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)) @@ -48,7 +48,7 @@ -- | Turns a lazy infinite list into a stream. toStr :: [a] -> Str a toStr (x : xs) = x ::: delay (toStr xs)-toStr _ = error "runRatt: input terminated"+toStr _ = error "toStr: input terminated" -- | Turns a stream into a lazy infinite list. fromStr :: Str a -> [a]
test/IllTyped.hs view
@@ -10,24 +10,30 @@ -- {-# 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)) +sneakyLambdaUnderDelay :: Box (O (O Int -> Int -> Int))+sneakyLambdaUnderDelay = box (delay (let f x _ = adv x in f))+ leaky :: (() -> Bool) -> Str Bool leaky p = p () ::: delay (leaky (\ _ -> hd (leaky (\ _ -> True)))) -grec :: Int+grec :: a grec = grec++boxStream :: Str Int -> Box (Str Int)+boxStream s = box (0 ::: tl s)++mutualLoop :: a+mutualLoop = mutualLoop'++mutualLoop' :: a+mutualLoop' = mutualLoop zeros :: Box (Str Int) zeros = box (0 ::: delay (unbox zeros))
test/WellTyped.hs view
@@ -20,6 +20,13 @@ where run (x ::: xs) = unbox f x ::: (delay run <*> xs) +-- mutual recursive definition+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)+ data Input a = Input {jump :: !a, move :: !Move} data Move = StartLeft | EndLeft | StartRight | EndRight | NoMove