diff --git a/dunai-test.cabal b/dunai-test.cabal --- a/dunai-test.cabal +++ b/dunai-test.cabal @@ -1,5 +1,5 @@ name: dunai-test -version: 0.1.0.0 +version: 0.7.0 synopsis: Testing library for Dunai description: Testing and debugging library for Duani. . @@ -31,7 +31,7 @@ FRP.Dunai.Stream FRP.Dunai.QuickCheck build-depends: base >= 4 && <5, - dunai >= 0.5 && <0.6, + dunai >= 0.5 && <0.8, QuickCheck, normaldistribution hs-source-dirs: src diff --git a/src/FRP/Dunai/Debug.hs b/src/FRP/Dunai/Debug.hs --- a/src/FRP/Dunai/Debug.hs +++ b/src/FRP/Dunai/Debug.hs @@ -18,4 +18,4 @@ traceMSFWithIO :: (a -> IO b) -> MSF IO a a -traceMSFWithIO f = arrM (\x -> (f x >> return x)) +traceMSFWithIO f = arrM (\x -> f x >> return x) diff --git a/src/FRP/Dunai/LTLFuture.hs b/src/FRP/Dunai/LTLFuture.hs --- a/src/FRP/Dunai/LTLFuture.hs +++ b/src/FRP/Dunai/LTLFuture.hs @@ -1,16 +1,12 @@ -{-# LANGUAGE GADTs #-} +{-# LANGUAGE GADTs #-} {-# LANGUAGE ScopedTypeVariables #-} --- TODO - --- Important question: because this FRP implement uses CPS, --- it is stateful, and sampling twice in one time period --- is not necessarily the same as sampling once. This means that --- tauApp, or next, might not work correctly. It's important to --- see what is going on there... :( - -module FRP.Dunai.LTLFuture where +module FRP.Dunai.LTLFuture + ( TPred(..) + , tPredMap + , evalT + ) + where ------------------------------------------------------------------------------- import Control.Monad.Trans.MSF.Reader import Data.MonadicStreamFunction import Data.MonadicStreamFunction.InternalCore (unMSF) @@ -30,17 +26,20 @@ Next :: TPred m a -> TPred m a Until :: TPred m a -> TPred m a -> TPred m a --- | Apply a transformation to the leaves (to the SFs) -tPredMap :: Monad m => (MSF m a Bool -> m (MSF m a Bool)) -> TPred m a -> m (TPred m a) +-- | Apply a transformation to the leaves of a temporal predicate (to the SFs). +tPredMap :: Monad m + => (MSF m a Bool -> m (MSF m a Bool)) -- ^ Transformation to apply + -> TPred m a -- ^ Temporal predicate + -> m (TPred m a) tPredMap f (Prop sf) = Prop <$> f sf -tPredMap f (And t1 t2) = And <$> (tPredMap f t1) <*> (tPredMap f t2) -tPredMap f (Or t1 t2) = Or <$> (tPredMap f t1) <*> (tPredMap f t2) -tPredMap f (Not t1) = Not <$> (tPredMap f t1) -tPredMap f (Implies t1 t2) = Implies <$> (tPredMap f t1) <*> (tPredMap f t2) -tPredMap f (Always t1) = Always <$> (tPredMap f t1) -tPredMap f (Eventually t1) = Eventually <$> (tPredMap f t1) -tPredMap f (Next t1) = Next <$> (tPredMap f t1) -tPredMap f (Until t1 t2) = Until <$> (tPredMap f t1) <*> (tPredMap f t2) +tPredMap f (And t1 t2) = And <$> tPredMap f t1 <*> tPredMap f t2 +tPredMap f (Or t1 t2) = Or <$> tPredMap f t1 <*> tPredMap f t2 +tPredMap f (Not t1) = Not <$> tPredMap f t1 +tPredMap f (Implies t1 t2) = Implies <$> tPredMap f t1 <*> tPredMap f t2 +tPredMap f (Always t1) = Always <$> tPredMap f t1 +tPredMap f (Eventually t1) = Eventually <$> tPredMap f t1 +tPredMap f (Next t1) = Next <$> tPredMap f t1 +tPredMap f (Until t1 t2) = Until <$> tPredMap f t1 <*> tPredMap f t2 -- * Temporal Evaluation @@ -48,30 +47,94 @@ -- -- Returns 'True' if the temporal proposition is currently true. evalT :: Monad m => TPred (ReaderT DTime m) a -> SignalSampleStream a -> m Bool -evalT (Prop sf) = \stream -> (myHead . fst) <$> evalSF sf stream -evalT (And t1 t2) = \stream -> (&&) <$> (evalT t1 stream) <*> (evalT t2 stream) -evalT (Or t1 t2) = \stream -> (||) <$> (evalT t1 stream) <*> (evalT t2 stream) -evalT (Not t1) = \stream -> not <$> (evalT t1 stream) -evalT (Implies t1 t2) = \stream -> (||) <$> (not <$> (evalT t1 stream)) <*> (evalT t2 stream) -evalT (Always t1) = \stream -> (&&) <$> (evalT t1 stream) <*> (evalT (Next (Always t1)) stream) -evalT (Eventually t1) = \stream -> (||) <$> (evalT t1 stream) <*> (evalT (Next (Eventually t1)) stream) -evalT (Until t1 t2) = \stream -> (||) <$> ((&&) <$> (evalT t1 stream) <*> (evalT (Next (Until t1 t2)) stream)) <*> (evalT t2 stream) -evalT (Next t1) = \stream -> case stream of - ([]) -> return False -- This is important. - (a:[]) -> return True -- This is important. It determines how - -- eventually, always and next behave at the - -- end of the stream, which affects that is and isn't - -- a tautology. It should be reviewed very carefully. - (a1:as) -> tauApp t1 a1 >>= (`evalT` as) +evalT (Prop sf) [] = return False +evalT (And t1 t2) [] = (&&) <$> evalT t1 [] <*> evalT t2 [] +evalT (Or t1 t2) [] = (||) <$> evalT t1 [] <*> evalT t2 [] +evalT (Not t1) [] = not <$> evalT t1 [] +evalT (Implies t1 t2) [] = (||) <$> (not <$> evalT t1 []) <*> evalT t2 [] +evalT (Always t1) [] = return True +evalT (Eventually t1) [] = return False +evalT (Next t1) [] = return False +evalT (Until t1 t2) [] = (||) <$> evalT t1 [] <*> evalT t2 [] +evalT op (x:xs) = do + (r, op') <- stepF op x + case (r, xs) of + (Def x, _) -> return x + (SoFar x, []) -> return x + (SoFar x, xs) -> evalT op' xs --- Tau-application (transportation to the future) -tauApp :: forall m a . Monad m => TPred (ReaderT DTime m) a -> (DTime, a) -> m (TPred (ReaderT DTime m) a) -tauApp pred (dtime, sample) = runReaderT f dtime - where - f :: ReaderT DTime m (TPred (ReaderT DTime m) a) - f = (tPredMap (\s -> snd <$> unMSF s sample) pred) +-- ** Multi-valued temporal evaluation +-- | Multi-valued logic result +data MultiRes + = Def Bool -- ^ Definite value known + | SoFar Bool -- ^ Value so far, but could change -myHead :: [a] -> a -myHead [] = error "My head: empty list" -myHead (x:_) = x +-- | Multi-valued implementation of @and@. +andM :: MultiRes -> MultiRes -> MultiRes +andM (Def False) _ = Def False +andM _ (Def False) = Def False +andM (Def True) x = x +andM x (Def True) = x +andM (SoFar False) (SoFar x) = SoFar False +andM (SoFar x) (SoFar False) = SoFar False +andM (SoFar True) (SoFar x) = SoFar x +andM (SoFar x) (SoFar True) = SoFar x + +-- | Multi-valued implementation of @or@. +orM :: MultiRes -> MultiRes -> MultiRes +orM (Def False) x = x +orM _ (Def False) = Def False +orM (Def True) x = x +orM x (Def True) = x +orM (SoFar False) (SoFar x) = SoFar False +orM (SoFar x) (SoFar False) = SoFar False +orM (SoFar True) (SoFar x) = SoFar x +orM (SoFar x) (SoFar True) = SoFar x + +-- | Perform one step of evaluation of a temporal predicate. +stepF :: Monad m + => TPred (ReaderT DTime m) a + -> (DTime, a) + -> m (MultiRes, TPred (ReaderT DTime m) a) + +stepF (Prop sf) x = do + (b, sf') <- unMSF (runReaderS sf) x + return (Def b, Prop (readerS sf')) + +stepF (Always sf) x = do + (b, sf') <- stepF sf x + case b of + Def True -> pure (SoFar True, Always sf') + Def False -> pure (Def False, Always sf') + SoFar True -> pure (SoFar True, Always sf') + SoFar False -> pure (SoFar False, Always sf') + +stepF (Eventually sf) x = do + (b, sf') <- stepF sf x + case b of + Def True -> pure (SoFar True, Always sf') + Def False -> pure (SoFar False, Always sf') + SoFar True -> pure (SoFar True, Always sf') + SoFar False -> pure (SoFar False, Always sf') + +stepF (Not sf) x = do + (b, sf') <- stepF sf x + case b of + Def x -> pure (Def (not x), Not sf') + SoFar x -> pure (SoFar (not x), Not sf') + +stepF (And sf1 sf2) x = do + (b1, sf1') <- stepF sf1 x + (b2, sf2') <- stepF sf2 x + let r = andM b1 b2 + pure (r, And sf1' sf2') + +stepF (Or sf1 sf2) x = do + (b1, sf1') <- stepF sf1 x + (b2, sf2') <- stepF sf2 x + let r = orM b1 b2 + pure (r, Or sf1' sf2') + +stepF (Implies sf1 sf2) x = + stepF (Not sf1 `Or` sf2) x diff --git a/src/FRP/Dunai/LTLPast.hs b/src/FRP/Dunai/LTLPast.hs --- a/src/FRP/Dunai/LTLPast.hs +++ b/src/FRP/Dunai/LTLPast.hs @@ -1,13 +1,35 @@ {-# LANGUAGE Arrows #-} +-- | Past LTL using MSFs. +-- +-- Add assertions inside MSFs. +-- +-- There are two ways of adding assertions to MSFs: piping the results of +-- Boolean-carrying MSFs into other MSFs, or wrapping MSFs into other MSFs +-- (using combinators). module FRP.Dunai.LTLPast where ------------------------------------------------------------------------------- import Control.Monad.Trans.MSF.Maybe import Data.Maybe import Data.MonadicStreamFunction --- * SFs that implement temporal combinators +-- * Past LTL as MSFs +-- ** Propositional MSFs + +andSF :: Monad m => MSF m (Bool, Bool) Bool +andSF = arr (uncurry (&&)) + +orSF :: Monad m => MSF m (Bool, Bool) Bool +orSF = arr (uncurry (||)) + +notSF :: Monad m => MSF m Bool Bool +notSF = arr not + +impliesSF :: Monad m => MSF m (Bool, Bool) Bool +impliesSF = arr $ \(i,p) -> not i || p + +-- ** Temporal MSFs + sofarSF :: Monad m => MSF m Bool Bool sofarSF = feedback True $ arr $ \(n,o) -> let n' = o && n in (n', n') @@ -16,33 +38,23 @@ untilSF :: Monad m => MSF m (Bool, Bool) Bool untilSF = - catchMaybe (untilMaybeB (feedback True $ arr cond)) - (snd ^>> sofarSF) + catchMaybe (untilMaybeB (feedback True $ arr cond)) + (snd ^>> sofarSF) where + untilMaybeB :: Monad m => MSF m a (b, Bool) -> MSF (MaybeT m) a b untilMaybeB msf = proc a -> do - (b,c) <- liftTransS msf -< a + (b,c) <- liftTransS msf -< a inMaybeT -< if c then Nothing else Just b - cond ((i,u),o) = let n = o && i - in ((n, (o && u)), n) + cond ((i, u), o) = ((n, o && u), n) + where + n = o && i lastSF :: Monad m => MSF m Bool Bool lastSF = iPre False -andSF :: Monad m => MSF m (Bool, Bool) Bool -andSF = arr (uncurry (&&)) - -orSF :: Monad m => MSF m (Bool, Bool) Bool -orSF = arr (uncurry (||)) - -notSF :: Monad m => MSF m Bool Bool -notSF = arr not - -impliesSF :: Monad m => MSF m (Bool, Bool) Bool -impliesSF = arr $ \(i,p) -> not i || p - -- data UnclearResult = Possibly Bool | Definitely Bool -- -- causally :: SF a Bool -> SF a UnclearResult @@ -59,12 +71,14 @@ -- clarifyResult (Possibly x) = x -- clarifyResult (Definitely x) = x --- * SF combinators that implement temporal combinators +-- * Past LTL combinators +-- | A signal predicate is an MSF whose output is a Boolean value. type SPred m a = MSF m a Bool +-- ** Propositional MSFs notSF' :: Monad m => SPred m a -> SPred m a -notSF' sf = sf >>> arr (not) +notSF' sf = sf >>> arr not andSF' :: Monad m => SPred m a -> SPred m a -> SPred m a andSF' sf1 sf2 = (sf1 &&& sf2) >>> arr (uncurry (&&)) @@ -74,6 +88,8 @@ implySF' :: Monad m => SPred m a -> SPred m a -> SPred m a implySF' sf1 sf2 = orSF' sf2 (notSF' sf1) + +-- ** Temporal MSFs history' :: Monad m => SPred m a -> SPred m a history' sf = feedback True $ proc (a, last) -> do diff --git a/src/FRP/Dunai/QuickCheck.hs b/src/FRP/Dunai/QuickCheck.hs --- a/src/FRP/Dunai/QuickCheck.hs +++ b/src/FRP/Dunai/QuickCheck.hs @@ -1,5 +1,4 @@ -{-# LANGUAGE Arrows #-} -{-# LANGUAGE MultiWayIf #-} +{-# LANGUAGE MultiWayIf #-} {-# LANGUAGE ScopedTypeVariables #-} module FRP.Dunai.QuickCheck where @@ -38,14 +37,15 @@ generateDeltas :: Distribution -> Range -> Length -> Gen DTime generateDeltas DistConstant (mn, mx) len = generateDelta mn mx generateDeltas DistRandom (mn, mx) len = generateDelta mn mx -generateDeltas (DistNormal (avg, dev)) (mn, mx) len = generateDSNormal avg dev mn mx +generateDeltas (DistNormal (avg, dev)) (mn, mx) len = + generateDSNormal avg dev mn mx -- | Generate one random delta, possibly within a range. generateDelta :: Maybe DTime -> Maybe DTime -> Gen DTime generateDelta (Just x) (Just y) = choose (x, y) -generateDelta (Just x) (Nothing) = (x+) <$> getPositive <$> arbitrary -generateDelta (Nothing) (Just y) = choose (2.2251e-308, y) -generateDelta (Nothing) (Nothing) = getPositive <$> arbitrary +generateDelta (Just x) Nothing = (x+) . getPositive <$> arbitrary +generateDelta Nothing (Just y) = choose (2.2251e-308, y) +generateDelta Nothing Nothing = getPositive <$> arbitrary -- | Generate a random delta following a normal distribution, -- and possibly within a given range. @@ -53,8 +53,8 @@ generateDSNormal avg stddev m n = suchThat gen (\x -> mx x && mn x) where gen = MkGen (\r _ -> let (x,_) = normal' (avg, stddev) r in x) - mn = maybe (\_ -> True) (<=) m - mx = maybe (\_ -> True) (>=) n + mn = maybe (const True) (<=) m + mx = maybe (const True) (>=) n -- | Generate random samples up until a max time. timeStampsUntil :: DTime -> Gen [DTime] @@ -63,10 +63,10 @@ -- | Generate random samples up until a max time, with a given time delta -- generation function. timeStampsUntilWith :: Gen DTime -> DTime -> Gen [DTime] -timeStampsUntilWith arb ds = timeStampsUntilWith' arb [] ds +timeStampsUntilWith arb = timeStampsUntilWith' arb [] where - -- | Generate random samples up until a max time, with a given time delta - -- generation function, and an initial suffix of time deltas. + -- Generate random samples up until a max time, with a given time delta + -- generation function, and an initial suffix of time deltas. timeStampsUntilWith' :: Gen DTime -> [DTime] -> DTime -> Gen [DTime] timeStampsUntilWith' arb acc ds | ds < 0 = return acc @@ -78,13 +78,22 @@ -- | Generate random stream. generateStream :: Arbitrary a - => Distribution -> Range -> Length -> Gen (SignalSampleStream a) + => Distribution + -> Range + -> Length + -> Gen (SignalSampleStream a) generateStream = generateStreamWith (\_ _ -> arbitrary) -- | Generate random stream, parameterized by the value generator. -generateStreamWith :: Arbitrary a - => (Int -> DTime -> Gen a) -> Distribution -> Range -> Length -> Gen (SignalSampleStream a) -generateStreamWith arb DistConstant range len = generateConstantStream arb =<< generateStreamLenDT range len +generateStreamWith :: (Int -> DTime -> Gen a) + -> Distribution + -> Range + -> Length + -> Gen (SignalSampleStream a) + +generateStreamWith arb DistConstant range len = + generateConstantStream arb =<< generateStreamLenDT range len + generateStreamWith arb DistRandom (m, n) Nothing = do l <- arbitrary x <- arb 0 0 @@ -132,14 +141,18 @@ return $ groupDeltas (x:xs) ds -- | Generate arbitrary stream with fixed length and constant delta. -generateConstantStream :: (Int -> DTime -> Gen a) -> (DTime, Int) -> Gen (SignalSampleStream a) +generateConstantStream :: (Int -> DTime -> Gen a) + -> (DTime, Int) + -> Gen (SignalSampleStream a) generateConstantStream arb (x, length) = do - ys <- vectorOfWith length (\n -> arb n x) + ys <- vectorOfWith length (`arb` x) let ds = repeat x return $ groupDeltas ys ds -- | Generate arbitrary stream -generateStreamLenDT :: (Maybe DTime, Maybe DTime) -> Maybe (Either Int DTime) -> Gen (DTime, Int) +generateStreamLenDT :: (Maybe DTime, Maybe DTime) + -> Maybe (Either Int DTime) + -> Gen (DTime, Int) generateStreamLenDT range len = do x <- uncurry generateDelta range l <- case len of @@ -165,17 +178,23 @@ uniDistStream :: Arbitrary a => Gen (SignalSampleStream a) uniDistStream = generateStream DistRandom (Nothing, Nothing) Nothing --- | Generate a stream of values with uniformly distributed time deltas, with a max DT. +-- | Generate a stream of values with uniformly distributed time deltas, with a +-- max DT. uniDistStreamMaxDT :: Arbitrary a => DTime -> Gen (SignalSampleStream a) -uniDistStreamMaxDT maxDT = generateStream DistRandom (Nothing, Just maxDT ) Nothing +uniDistStreamMaxDT maxDT = + generateStream DistRandom (Nothing, Just maxDT) Nothing -- | Generate a stream of values with a fixed time delta. fixedDelayStream :: Arbitrary a => DTime -> Gen (SignalSampleStream a) fixedDelayStream dt = generateStream DistConstant (Just dt, Just dt) Nothing -- | Generate a stream of values with a fixed time delta. -fixedDelayStreamWith :: Arbitrary a => (DTime -> a) -> DTime -> Gen (SignalSampleStream a) -fixedDelayStreamWith f dt = generateStreamWith f' DistConstant (Just dt, Just dt) Nothing +fixedDelayStreamWith :: Arbitrary a + => (DTime -> a) + -> DTime + -> Gen (SignalSampleStream a) +fixedDelayStreamWith f dt = + generateStreamWith f' DistConstant (Just dt, Just dt) Nothing where f' n t = return $ f (fromIntegral n * t) diff --git a/src/FRP/Dunai/Stream.hs b/src/FRP/Dunai/Stream.hs --- a/src/FRP/Dunai/Stream.hs +++ b/src/FRP/Dunai/Stream.hs @@ -24,7 +24,7 @@ -- | Turn a stream with sampling times into a list of values. samples :: SignalSampleStream a -> [a] -samples as = map snd as +samples = map snd firstSample :: SignalSampleStream a -> a firstSample = head . samples @@ -65,26 +65,25 @@ -- ** Clipping (dropping samples) -sClipAfterFrame :: Int -> SignalSampleStream a -> SignalSampleStream a -sClipAfterFrame n xs = take n xs +sClipAfterFrame :: Int -> SignalSampleStream a -> SignalSampleStream a +sClipAfterFrame = take sClipAfterTime dt [] = [] sClipAfterTime dt ((dt',x):xs) | dt < dt' = [] - | otherwise = ((dt',x):sClipAfterTime (dt - dt') xs) + | otherwise = (dt', x) : sClipAfterTime (dt - dt') xs sClipBeforeFrame :: Int -> SignalSampleStream a -> SignalSampleStream a -sClipBeforeFrame 0 (x:xs) = (x:xs) -sClipBeforeFrame n (x:[]) = (x:[]) -sClipBeforeFrame n (_:x:xs) = sClipBeforeFrame (n-1) (x:xs) +sClipBeforeFrame 0 xs@(_:_) = xs +sClipBeforeFrame n xs@[x] = xs +sClipBeforeFrame n xs = sClipBeforeFrame (n-1) xs sClipBeforeTime :: DTime -> SignalSampleStream a -> SignalSampleStream a sClipBeforeTime dt xs | dt <= 0 = xs | otherwise = case xs of - (x:[]) -> (x:[]) - (_:(dt',x'):xs') -> if | dt < dt' -> -- (dt' - dt, x'):xs' - ((dt'- dt, x'):xs') + [x] -> xs + (_:(dt',x'):xs') -> if | dt < dt' -> ((dt'- dt, x'):xs') | otherwise -> sClipBeforeTime (dt - dt') ((0,x'):xs')