dunai-test 0.1.0.0 → 0.7.0

raw patch · 6 files changed

+198/−101 lines, 6 filesdep ~dunaiPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: dunai

API changes (from Hackage documentation)

Files

• dunai-test.cabal +2/−2
• src/FRP/Dunai/Debug.hs +1/−1
• src/FRP/Dunai/LTLFuture.hs +108/−45
• src/FRP/Dunai/LTLPast.hs +37/−21
• src/FRP/Dunai/QuickCheck.hs +41/−22
• src/FRP/Dunai/Stream.hs +9/−10

@@ -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

@@ -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)

@@ -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

@@ -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

@@ -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) 

@@ -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')