diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,9 @@ +0.1.1.0 +------- + +- allow mutual guarded recursion +- improve type error messages + 0.1.0.0 ------- initial release diff --git a/Rattus.cabal b/Rattus.cabal --- a/Rattus.cabal +++ b/Rattus.cabal @@ -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 - . + . . @@ -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 + + provides more examples on how to program in Rattus. homepage: https://github.com/pa-ba/Rattus License: BSD3 diff --git a/src/Rattus/Event.hs b/src/Rattus/Event.hs --- a/src/Rattus/Event.hs +++ b/src/Rattus/Event.hs @@ -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) diff --git a/src/Rattus/Events.hs b/src/Rattus/Events.hs --- a/src/Rattus/Events.hs +++ b/src/Rattus/Events.hs @@ -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. diff --git a/src/Rattus/Plugin.hs b/src/Rattus/Plugin.hs --- a/src/Rattus/Plugin.hs +++ b/src/Rattus/Plugin.hs @@ -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 diff --git a/src/Rattus/Plugin/ScopeCheck.hs b/src/Rattus/Plugin/ScopeCheck.hs --- a/src/Rattus/Plugin/ScopeCheck.hs +++ b/src/Rattus/Plugin/ScopeCheck.hs @@ -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 "", 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") diff --git a/src/Rattus/Primitives.hs b/src/Rattus/Primitives.hs --- a/src/Rattus/Primitives.hs +++ b/src/Rattus/Primitives.hs @@ -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 :: 𝜏 -- > -------------------- diff --git a/src/Rattus/Stream.hs b/src/Rattus/Stream.hs --- a/src/Rattus/Stream.hs +++ b/src/Rattus/Stream.hs @@ -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 diff --git a/src/Rattus/ToHaskell.hs b/src/Rattus/ToHaskell.hs --- a/src/Rattus/ToHaskell.hs +++ b/src/Rattus/ToHaskell.hs @@ -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] diff --git a/test/IllTyped.hs b/test/IllTyped.hs --- a/test/IllTyped.hs +++ b/test/IllTyped.hs @@ -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)) diff --git a/test/WellTyped.hs b/test/WellTyped.hs --- a/test/WellTyped.hs +++ b/test/WellTyped.hs @@ -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