diff --git a/CHANGELOG b/CHANGELOG new file mode 100644 --- /dev/null +++ b/CHANGELOG @@ -0,0 +1,6 @@ +2018-10-21 Ivan Perez + * Initial version. + +Copyright (c) 2014-2018, Ivan Perez. +All rights reserved. + diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright (c) 2017, Ivan Perez + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * 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. + + * Neither the name of Ivan Perez nor the names of other + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"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 COPYRIGHT +OWNER 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. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/dist/build/yampa-quicheckStub/yampa-quicheckStub-tmp/yampa-quicheckStub.hs b/dist/build/yampa-quicheckStub/yampa-quicheckStub-tmp/yampa-quicheckStub.hs new file mode 100644 --- /dev/null +++ b/dist/build/yampa-quicheckStub/yampa-quicheckStub-tmp/yampa-quicheckStub.hs @@ -0,0 +1,5 @@ +module Main ( main ) where +import Distribution.Simple.Test.LibV09 ( stubMain ) +import YampaQC ( tests ) +main :: IO () +main = stubMain tests diff --git a/src/FRP/Yampa/Debug.hs b/src/FRP/Yampa/Debug.hs new file mode 100644 --- /dev/null +++ b/src/FRP/Yampa/Debug.hs @@ -0,0 +1,20 @@ +-- | Debug FRP networks by inspecting their behaviour inside. +module FRP.Yampa.Debug where + +import Debug.Trace +import FRP.Yampa +import System.IO.Unsafe + +-- | Signal Function that prints the value passing through using 'trace'. +traceSF :: Show a => SF a a +traceSF = traceSFWith show + +-- | Signal Function that prints the value passing through using 'trace', +-- and a customizable 'show' function. +traceSFWith :: (a -> String) -> SF a a +traceSFWith f = arr (\x -> trace (f x) x) + +-- | Execute an IO action using 'unsafePerformIO' at every step, and ignore the +-- result. +traceSFWithIO :: (a -> IO b) -> SF a a +traceSFWithIO f = arr (\x -> (unsafePerformIO (f x >> return x))) diff --git a/src/FRP/Yampa/LTLFuture.hs b/src/FRP/Yampa/LTLFuture.hs new file mode 100644 --- /dev/null +++ b/src/FRP/Yampa/LTLFuture.hs @@ -0,0 +1,73 @@ +{-# LANGUAGE GADTs #-} +-- | Linear Temporal Logics based on SFs. +-- +-- This module contains a definition of LTL with Next on top of Signal +-- Functions. +-- +-- LTL predicates are parameterized over an input. A basic proposition +-- is a Signal Function that produces a boolean function. + +-- 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.Yampa.LTLFuture + ( TPred(..) + , evalT + ) + where + +import FRP.Yampa +import FRP.Yampa.Stream + +-- | Type representing future-time linear temporal logic predicates with until +-- and next. +data TPred a where + Prop :: SF a Bool -> TPred a + And :: TPred a -> TPred a -> TPred a + Or :: TPred a -> TPred a -> TPred a + Not :: TPred a -> TPred a + Implies :: TPred a -> TPred a -> TPred a + Always :: TPred a -> TPred a + Eventually :: TPred a -> TPred a + Next :: TPred a -> TPred a + Until :: TPred a -> TPred a -> TPred a + +-- | Evaluates a temporal predicate at time t=0 with a concrete sample stream. +-- +-- Returns 'True' if the temporal proposition is currently true. +evalT :: TPred a -> SignalSampleStream a -> Bool +evalT (Prop sf) = \stream -> firstSample $ 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 (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 -> case stream of + (a,[]) -> evalT t1 stream + (a1,(dt,a2):as) -> evalT t1 stream || evalT (tauApp (Eventually t1) a1 dt) (a2, as) +evalT (Until t1 t2) = \stream -> (evalT t1 stream && evalT (Next (Until t1 t2)) stream) + || evalT t2 stream +evalT (Next t1) = \stream -> case stream of + (a,[]) -> True -- This is important. It determines how + -- 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,(dt, a2):as) -> evalT (tauApp t1 a1 dt) (a2, as) + +-- | Tau-application (transportation to the future) +tauApp :: TPred a -> a -> DTime -> TPred a +tauApp pred sample dtime = tPredMap (\sf -> snd (evalFuture sf sample dtime)) pred + +-- | Apply a transformation to the leaves (to the SFs) +tPredMap :: (SF a Bool -> SF a Bool) -> TPred a -> TPred 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) diff --git a/src/FRP/Yampa/LTLPast.hs b/src/FRP/Yampa/LTLPast.hs new file mode 100644 --- /dev/null +++ b/src/FRP/Yampa/LTLPast.hs @@ -0,0 +1,78 @@ +{-# LANGUAGE Arrows #-} +-- | Past-time Linear Temporal Logics based on SFs. +-- +-- This module contains a definition of ptLTL with prev/last on top of Signal +-- Functions. +-- +-- The difference between the future time and the past time LTL is that the +-- former needs a trace for evaluation, and the latter can be embedded into a +-- signal function network without additional support for evaluation. + +module FRP.Yampa.LTLPast where + +------------------------------------------------------------------------------ +import FRP.Yampa + +-- | True if both inputs are True. +andSF :: SF (Bool, Bool) Bool +andSF = arr (uncurry (&&)) + +-- | True if either or both inputs are True. +orSF :: SF (Bool, Bool) Bool +orSF = arr (uncurry (||)) + +-- | True if the input signal is False. +notSF :: SF Bool Bool +notSF = arr not + +-- | True if the first signal is False or the second one is True. +impliesSF :: SF (Bool, Bool) Bool +impliesSF = arr $ \(i,p) -> not i || p + +-- | True a a time if the input signal has been always True so far. +sofarSF :: SF Bool Bool +sofarSF = loopPre True $ arr $ \(n,o) -> let n' = o && n in (n', n') + +-- | True at a time if the input signal has ever been True before. +everSF :: SF Bool Bool +everSF = loopPre False $ arr $ \(n,o) -> let n' = o || n in (n', n') + +-- | True if the signal was True in the last sample. False at time zero. +lastSF :: SF Bool Bool +lastSF = iPre False + +-- | Weak Until. True if the first signal is True until the second becomes +-- True, if ever. +untilSF :: SF (Bool, Bool) Bool +untilSF = switch + (loopPre True $ arr (\((i,u),o) -> let n = o && i + in ((n, if (o && u) then Event () else NoEvent), n))) + (\_ -> arr snd >>> sofarSF) + +-- -- * SF combinators that implement temporal combinators +-- +-- type SPred a = SF a Bool +-- +-- andSF' :: SPred a -> SPred a -> SPred a +-- andSF' sf1 sf2 = (sf1 &&& sf2) >>> arr (uncurry (&&)) +-- +-- orSF' :: SPred a -> SPred a -> SPred a +-- orSF' sf1 sf2 = (sf1 &&& sf2) >>> arr (uncurry (||)) +-- +-- notSF' :: SPred a -> SPred a +-- notSF' sf = sf >>> arr (not) +-- +-- implySF' :: SPred a -> SPred a -> SPred a +-- implySF' sf1 sf2 = orSF' sf2 (notSF' sf1) +-- +-- history' :: SPred a -> SPred a +-- history' sf = loopPre True $ proc (a, last) -> do +-- b <- sf -< a +-- let cur = last && b +-- returnA -< (cur, cur) +-- +-- ever' :: SPred a -> SPred a +-- ever' sf = loopPre False $ proc (a, last) -> do +-- b <- sf -< a +-- let cur = last || b +-- returnA -< (cur, cur) diff --git a/src/FRP/Yampa/QuickCheck.hs b/src/FRP/Yampa/QuickCheck.hs new file mode 100644 --- /dev/null +++ b/src/FRP/Yampa/QuickCheck.hs @@ -0,0 +1,206 @@ +{-# LANGUAGE Arrows #-} +{-# LANGUAGE MultiWayIf #-} +{-# LANGUAGE ScopedTypeVariables #-} +-- | QuickCheck generators for input streams. +-- +-- Random stream generation can be customized usin three parameters: +-- +-- - The distribution for the random time deltas ('Distribution'). +-- - The maximum and minimum bounds for the time deltas ('Range'). +-- - The maximum stream length ('Length'). +-- +-- The main function to generate streams is 'generateStream'. The specific +-- time deltas can be customized further using 'generateStreamWith'. Some +-- helper functions are provided to facilitate testing. + +-- The function uniDistStreamMaxDT had the wrong type and the name on the +-- paper was: uniDistStream. This has been fixed. + +module FRP.Yampa.QuickCheck + ( + -- * Random stream generation + generateStream + , generateStreamWith + + -- ** Parameters used to generate random input streams + , Distribution(..) + , Range + , Length + + -- ** Helpers for common cases + , uniDistStream + , uniDistStreamMaxDT + , fixedDelayStream + , fixedDelayStreamWith + ) + where + +import Control.Applicative ((<$>), pure) +import Data.Random.Normal +import FRP.Yampa +import Test.QuickCheck +import Test.QuickCheck.Gen + +import FRP.Yampa.Stream + +-- | Distributions used for time delta (DT) generation. +data Distribution = DistConstant -- ^ Constant DT for the whole stream. + | DistNormal (DTime, DTime) -- ^ Variable DT following normal distribution, + -- with an average and a standard deviation. + | DistRandom -- ^ Completely random (positive) DT. + +-- | Upper and lower bounds of time deltas for random DT generation. +type Range = (Maybe DTime, Maybe DTime) + +-- | Optional maximum length for a stream, given as a time, or a number of +-- samples. +type Length = Maybe (Either Int DTime) + + +-- | Generate a random delta according to some required specifications. +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 + +-- | 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+) <$> 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. +generateDSNormal :: DTime -> DTime -> Maybe DTime -> Maybe DTime -> Gen DTime +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 + +-- | Generate random samples up until a max time. +timeStampsUntil :: DTime -> Gen [DTime] +timeStampsUntil = timeStampsUntilWith arbitrary + +-- | 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 + where + -- | 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 + | otherwise = do d <- arb + let acc' = acc `seq` (d:acc) + acc' `seq` timeStampsUntilWith' arb acc' (ds - d) + +-- | Generate random stream. +generateStream :: Arbitrary 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 arb DistRandom (m, n) Nothing = do + l <- arbitrary + x <- arb 0 0 + ds <- vectorOfWith l (\_ -> generateDelta m n) + let f n = arb n (ds!!(n-1)) + xs <- vectorOfWith l f + return $ groupDeltas (x:xs) ds + +generateStreamWith arb DistRandom (m, n) (Just (Left l)) = do + x <- arb 0 0 + ds <- vectorOfWith l (\_ -> generateDelta m n) + let f n = arb n (ds!!(n-1)) + xs <- vectorOfWith l f + return $ groupDeltas (x:xs) ds + +generateStreamWith arb DistRandom (m, n) (Just (Right maxds)) = do + ds <- timeStampsUntilWith (generateDelta m n) maxds + let l = length ds + x <- arb 0 0 + let f n = arb n (ds!!(n-1)) + xs <- vectorOfWith l f + return $ groupDeltas (x:xs) ds + +generateStreamWith arb (DistNormal (avg, stddev)) (m, n) Nothing = do + l <- arbitrary + x <- arb 0 0 + ds <- vectorOfWith l (\_ -> generateDSNormal avg stddev m n) + let f n = arb n (ds!!(n-1)) + xs <- vectorOfWith l f + return $ groupDeltas (x:xs) ds + +generateStreamWith arb (DistNormal (avg, stddev)) (m, n) (Just (Left l)) = do + x <- arb 0 0 + ds <- vectorOfWith l (\_ -> generateDSNormal avg stddev m n) + let f n = arb n (ds!!(n-1)) + xs <- vectorOfWith l f + return $ groupDeltas (x:xs) ds + +generateStreamWith arb (DistNormal (avg, stddev)) (m, n) (Just (Right maxds)) = do + ds <- timeStampsUntilWith (generateDSNormal avg stddev m n) maxds + let l = length ds + x <- arb 0 0 + let f n = arb n (ds!!(n-1)) + xs <- vectorOfWith l f + 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 arb (x, length) = do + ys <- vectorOfWith length (\n -> arb n 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 range len = do + x <- uncurry generateDelta range + l <- case len of + Nothing -> ((1 +) . getPositive) <$> arbitrary + Just (Left l) -> pure l + Just (Right ds) -> (max 1) <$> (pure (floor (ds / x))) + return (x, l) + +-- generateStreamLenDT (Just x, Just y) (Just (Left l)) = (,) <$> choose (x, y) <*> pure l +-- generateStreamLenDT (Just x, Nothing) (Just (Left l)) = (,) <$> ((x+) <$> arbitrary) <*> pure l +-- generateStreamLenDT (Nothing, Just y) (Just (Left l)) = (,) <$> choose (0, y) <*> pure l +-- generateStreamLenDT (Just x, _) (Just (Right ts)) = (,) <$> pure x <*> pure (floor (ts / x)) +-- generateStreamLenDT (Just x, _) Nothing = (,) <$> pure x <*> arbitrary +-- generateStreamLenDT (Nothing, Nothing) Nothing = (,) <$> arbitrary <*> arbitrary +-- generateStreamLenDT (Nothing, Nothing) (Just (Left l)) = (,) <$> arbitrary <*> pure l +-- generateStreamLenDT (Nothing, Nothing) (Just (Right ds)) = f2 <$> arbitrary +-- where +-- f2 l = (ds / fromIntegral l, l) + + +-- | Generate a stream of values with uniformly distributed time deltas. +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. +uniDistStreamMaxDT :: Arbitrary a => DTime -> Gen (SignalSampleStream a) +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 + where + f' n t = return $ f (fromIntegral n * t) + +-- * Extended quickcheck generator + +-- | Generates a list of the given length. +vectorOfWith :: Int -> (Int -> Gen a) -> Gen [a] +vectorOfWith k genF = sequence [ genF i | i <- [1..k] ] diff --git a/src/FRP/Yampa/Stream.hs b/src/FRP/Yampa/Stream.hs new file mode 100644 --- /dev/null +++ b/src/FRP/Yampa/Stream.hs @@ -0,0 +1,162 @@ +{-# LANGUAGE MultiWayIf #-} +-- | Streams and stream manipulation API. +-- +-- The evaluation of Yampa SFs, especially for testing purposes, needs the +-- generation of suitable input streams. +-- +-- While some streams can be generated randomly using QuickCheck, it is +-- sometimes useful to be able to preprend or adapt an input stream. It is also +-- useful to debug programs when you have recorded input streams using Haskell +-- Titan. +-- +-- This module defines types for input streams, as well as an API to create, +-- examine and combine streams. It also provides evaluation functions that are +-- needed to apply an SF to a stream and obtain an output stream and a +-- continuation SF. +module FRP.Yampa.Stream where + +import FRP.Yampa (DTime, SF, FutureSF, evalAtZero, evalAt) + +-- * Types + +-- | A stream of samples, with their sampling times. +type SignalSampleStream a = (a, FutureSampleStream a) + +-- | A stream of future samples, with their sampling times. The difference +-- between 'SignalSampleStream' and 'FutureSampleStream' is that all elements +-- in the latter have a non-zero time delta. +type FutureSampleStream a = [(DTime, a)] + +-- * Creation + +-- | Group a series of samples with a series of time deltas. +-- +-- The first sample will have no delta. Unused samples and deltas will be +-- dropped. +groupDeltas :: [a] -> [DTime] -> SignalSampleStream a +groupDeltas (x:xs) ds = (x, zip ds xs) +groupDeltas xs ds = error $ "groupDeltas: called me with lists with lengths" ++ show (length xs) ++ " and " ++ show (length ds) + +-- * Examination + +-- | Turn a stream with sampling times into a list of values. +samples :: SignalSampleStream a -> [a] +samples (a, as) = a : map snd as + +-- | Return the first sample in a sample stream. +firstSample :: SignalSampleStream a -> a +firstSample = head . samples + +-- | Return the last sample in a sample stream. +lastSample :: SignalSampleStream a -> a +lastSample = last . samples + +-- * Manipulation + +-- | Merge two streams, using an auxilary function to merge samples that fall +-- at the exact same sampling time. +sMerge :: (a -> a -> a) -> SignalSampleStream a -> SignalSampleStream a -> SignalSampleStream a +sMerge f (x1, xs1) (x2, xs2) = (f x1 x2, sMergeTail f xs1 xs2) + where + sMergeTail :: (a -> a -> a) -> FutureSampleStream a -> FutureSampleStream a -> FutureSampleStream a + sMergeTail f [] xs2 = xs2 + sMergeTail f xs1 [] = xs1 + sMergeTail f ((dt1, x1):xs1) ((dt2, x2):xs2) + | dt1 == dt2 = (dt1, f x1 x2) : sMergeTail f xs1 xs2 + | dt1 < dt2 = (dt1, x1) : sMergeTail f xs1 ((dt2-dt1, x2):xs2) + | otherwise = (dt2, x2) : sMergeTail f ((dt1-dt2, x1):xs1) xs2 + +-- | Concatenate two sample streams, separating them by a given time delta. +sConcat :: SignalSampleStream a -> DTime -> SignalSampleStream a -> SignalSampleStream a +sConcat (x1, xs1) dt (x2, xs2) = (x1 , xs1 ++ ((dt, x2):xs2)) + +-- | Refine a stream by establishing the maximum time delta. +-- +-- If two samples are separated by a time delta bigger than the given max DT, +-- the former is replicated as many times as necessary. +sRefine :: DTime -> SignalSampleStream a -> SignalSampleStream a +sRefine maxDT (a, as) = (a, sRefineFutureStream maxDT a as) + where + sRefineFutureStream :: DTime -> a -> FutureSampleStream a -> FutureSampleStream a + sRefineFutureStream maxDT _ [] = [] + sRefineFutureStream maxDT a0 ((dt, a):as) + | dt > maxDT = (maxDT, a0) : sRefineFutureStream maxDT a0 ((dt - maxDT, a):as) + | otherwise = (dt, a) : sRefineFutureStream maxDT a as + +-- | Refine a stream by establishing the maximum time delta. +-- +-- If two samples are separated by a time delta bigger than the given max DT, +-- the auxiliary interpolation function is used to determine the intermendiate +-- sample. +sRefineWith :: (a -> a -> a) -> DTime -> SignalSampleStream a -> SignalSampleStream a +sRefineWith interpolate maxDT (a, as) = (a, refineFutureStreamWith interpolate maxDT a as) + where + refineFutureStreamWith :: (a -> a -> a) -> DTime -> a -> FutureSampleStream a -> FutureSampleStream a + refineFutureStreamWith interpolate maxDT _ [] = [] + refineFutureStreamWith interpolate maxDT a0 ((dt, a):as) + | dt > maxDT = let a' = interpolate a0 a + in (maxDT, interpolate a0 a) : refineFutureStreamWith interpolate maxDT a' ((dt - maxDT, a):as) + | otherwise = (dt, a) : refineFutureStreamWith interpolate maxDT a as + +-- | Clip a sample stream at a given number of samples. +sClipAfterFrame :: Int -> SignalSampleStream a -> SignalSampleStream a +sClipAfterFrame 0 (x,_) = (x, []) +sClipAfterFrame n (x,xs) = (x, xs') + where + xs' = take (n-1) xs + +-- | Clip a sample stream after a certain (non-zero) time. +sClipAfterTime :: DTime -> SignalSampleStream a -> SignalSampleStream a +sClipAfterTime dt (x,xs) = (x, sClipAfterTime' dt xs) + where + sClipAfterTime' dt [] = [] + sClipAfterTime' dt ((dt',x):xs) + | dt < dt' = [] + | otherwise = ((dt',x):sClipAfterTime' (dt - dt') xs) + +-- | Drop the first n samples of a signal stream. The time +-- deltas are not re-calculated. +sClipBeforeFrame :: Int -> SignalSampleStream a -> SignalSampleStream a +sClipBeforeFrame 0 (x,xs) = (x,xs) +sClipBeforeFrame n (x,[]) = (x,[]) +sClipBeforeFrame n (_,(dt,x):xs) = sClipBeforeFrame (n-1) (x, xs) + +-- | Drop the first samples of a signal stream up to a given time. The time +-- deltas are not re-calculated to match the original stream. +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' + (x',xs') + | otherwise -> sClipBeforeTime (dt - dt') (x', xs') + +-- ** Stream-based evaluation + +-- | Evaluate an SF with a 'SignalSampleStream', obtaining an output +-- stream and a continuation. +-- +-- You should never use this for actual execution in your applications, +-- only for testing. +evalSF :: SF a b + -> SignalSampleStream a + -> (SignalSampleStream b, FutureSF a b) +evalSF sf (a, as) = (outputStrm, fsf') + where (b, fsf) = evalAtZero sf a + (bs, fsf') = evalFutureSF fsf as + outputStrm = (b, bs) + +-- | Evaluate an initialised SF with a 'FutureSampleStream', obtaining +-- an output stream and a continuation. +-- +-- You should never use this for actual execution in your applications, +-- only for testing. +evalFutureSF :: FutureSF a b + -> FutureSampleStream a + -> (FutureSampleStream b, FutureSF a b) +evalFutureSF fsf [] = ([], fsf) +evalFutureSF fsf ((dt, a):as) = (outputStrm, fsf'') + where (b, fsf') = evalAt fsf dt a + (bs, fsf'') = evalFutureSF fsf' as + outputStrm = (dt, b) : bs diff --git a/tests/YampaQC.hs b/tests/YampaQC.hs new file mode 100644 --- /dev/null +++ b/tests/YampaQC.hs @@ -0,0 +1,596 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE Arrows #-} +-- TODO +-- Properties in this file have different types. +-- It's important to agree on the representation type. +-- +-- It may be a bit hard, because some elements from logic are +-- provided by QC, while others have to be defined by us. +-- For example, connectives like implication and always are +-- provided by us, and forAll is in QuickCheck. +-- +-- This makes it hard to combine, becase for this language to be +-- compositional like logic is we need to make everything accept +-- a QuickCheck predicate, which may not be possible or compatible +-- with out goals. +-- +module YampaQC where + +------------------------------------------------------------------------------ +import Data.Fixed + +import Distribution.TestSuite.QuickCheck +import Test.QuickCheck +import Test.QuickCheck.Function + +import FRP.Yampa as Yampa +import FRP.Yampa.EventS (snap) +import FRP.Yampa.Stream +import FRP.Yampa.QuickCheck +import FRP.Yampa.LTLFuture + +------------------------------------------------------------------------------ +tests :: IO [Test] +tests = return + [ testProperty "SF based on (**2) equal to SF on (^2))" prop_arr_law1 + , testProperty "Identity" prop_arr_id + , testProperty "Arrow Naturality" prop_arr_naturality + , testProperty "Naturality" prop_arr_naturality + , testProperty "Basic > Identity (1)" prop_basic_identity_1 + , testProperty "Basic > Identity (2)" prop_basic_identity_2 + , testProperty "Basic > Constant" prop_basic_constant + , testProperty "Basic > Initially" prop_basic_initially + , testProperty "Basic > Time" prop_basic_time_increasing + , testProperty "Basic > Time (fixed delay)" prop_basic_time_fixed_delay + , testProperty "Basic > localTime" prop_basic_localtime_increasing + , testProperty "Basic > localTime (fixed delay)" prop_basic_localtime_fixed_delay + , testProperty "Collections > parB" prop_broadcast + , testProperty "Arrows > Composition (1)" prop_arrow_comp_1 + , testProperty "Arrows > Composition (2)" prop_arrow_comp_2 + , testProperty "Arrows > Composition (3)" prop_arrow_comp_3 + , testProperty "Delays > Zero delay" prop_delay_1 + , testProperty "Delays > Small delay" prop_delay_2 + -- FIXME: (iperez:) delay_t3 is not here because I can't understand it. + -- Missing: delay t4 and t5 + , testProperty "Derivatives > Comparison with known derivative (1)" prop_derivative_1 + , testProperty "Derivatives > Comparison with known derivative (2)" prop_derivative_2 + -- Missing: embed + , testProperty "Events > No event" prop_event_noevent + , testProperty "Events > Now" prop_event_now + , testProperty "Events > After 0.0" prop_event_after_0 + -- Missing: a lot of event tests + , testProperty "Arrows > First (1)" prop_arrow_first_1 + , testProperty "Arrows > First (2)" prop_arrow_first_2 + , testProperty "Arrows > Second (1)" prop_arrow_second_1 + , testProperty "Arrows > Second (2)" prop_arrow_second_2 + -- Missing: first and second with integrals + -- Missing: KSwitch + + , testProperty "Arrows > Identity (0)" prop_arrow_id_0 + , testProperty "Arrows > Identity (2)" prop_arrow_id_2 + , testProperty "Arrows > Associativity" prop_arrow_assoc + , testProperty "Arrows > Function lifting composition" prop_arrow_arr_comp + , testProperty "Arrows > First" prop_arrow_first_3 + , testProperty "Arrows > Distributivity of First" prop_arrow_first_distrib + , testProperty "Arrows > Commutativity of id on first" prop_arrow_first_id_comm + , testProperty "Arrows > Nested firsts" prop_arrow_first_nested + -- Missing: Loop * + -- Missing: PSwitch + -- Missing: iPre + -- Missing: RPSwitch + -- Missing: RSwitch + -- Missing: React + -- Missing: Sscan + -- Missing: Switch + -- , testProperty "Switching > t1" prop_switch_t1 + -- Missing: Task + -- Missing: Utils + -- Missing: WFG + ] + +-- * Yampa laws + +-- ** Arrow laws +prop_arr_law1 = + forAll myStream (evalT $ prop_always_equal (arr (**2)) (arr (^2))) + where myStream :: Gen (SignalSampleStream Float) + myStream = uniDistStream + +prop_arr_id = + forAll myStream (evalT $ prop_always_equal (arr id) identity) + where myStream :: Gen (SignalSampleStream Float) + myStream = uniDistStream + +-- Yampa's internal test cases + +-- prop :: SF a b -> (a -> b -> +prop (a,b) = Prop ((identity &&& a) >>^ uncurry b) + +-- Yampa's Arrow Checks + +-- C1: Arr naturality (testSF1 (arr (+1))) +-- C2: Arr naturality (testSF2 (arr (+1))) +prop_arr_naturality = + forAll myStream $ \stream -> + forAll f $ \f' -> + evalT (Always (prop (arr (apply f'), \x y -> apply f' x == y))) + where myStream :: Gen (SignalSampleStream Float) + myStream = uniDistStream + f :: Gen (Fun Int Int) + f = arbitrary + +-- Yampa's Basic SF builders +prop_basic_identity_1 = + forAll myStream $ evalT $ Always $ prop (sf, pred) + where myStream :: Gen (SignalSampleStream Float) + myStream = uniDistStream + sf = identity + pred = (==) + +prop_basic_identity_2 = + forAll myStream (evalT $ prop_always_equal identity (arr id)) + where myStream :: Gen (SignalSampleStream Float) + myStream = uniDistStream + +prop_basic_constant = + forAll myStream $ evalT $ Always $ prop (sf, pred) + where myStream :: Gen (SignalSampleStream Float) + myStream = uniDistStream + + sf = constant 42.0 + pred = const (== 42.0) + +prop_basic_initially = + forAll myStream $ evalT $ prop (sf, pred) + where myStream :: Gen (SignalSampleStream Float) + myStream = uniDistStream + + sf = initially 42.0 + pred = const (== 42.0) + +-- | Starting with an accumulator of -1, it gets the local +-- time and outputs the time and the accumulator, updating +-- the latter with the local time at every iteration. +-- The predicate checks whether the time is always strictly +-- greater than the acc. +prop_basic_time_increasing = + forAll myStream $ evalT $ Always $ prop (sf, pred) + where myStream :: Gen (SignalSampleStream Float) + myStream = uniDistStream + + sf :: SF a (Time, Time) + sf = loopPre (-1 :: Time) sfI + + sfI :: SF (a,Time) ((Time, Time), Time) + sfI = (time *** identity) >>> arr resort + + resort :: (Time, Time) -> ((Time,Time),Time) + resort (newT, oldT) = ((newT, oldT), newT) + + pred :: a -> (Time, Time) -> Bool + pred _ (t,o) = (t > o) + +prop_basic_time_fixed_delay = + forAll myStream $ evalT $ + Always (prop (sf25msec, const (== d))) + + where myStream :: Gen (SignalSampleStream Float) + myStream = fixedDelayStream d + + sf25msec = time >>> stepDiff (-d) + + d :: Time + d = 0.25 + +prop_basic_localtime_increasing = + forAll myStream $ evalT $ Always $ prop (sf, const (uncurry (>))) + where myStream :: Gen (SignalSampleStream Float) + myStream = uniDistStream + + sf :: SF a (Time, Time) + sf = loopPre (-1 :: Time) sfI + + sfI :: SF (a,Time) ((Time, Time), Time) + sfI = (localTime *** identity) >>> arr resort + + resort :: (Time, Time) -> ((Time,Time),Time) + resort (newT, oldT) = ((newT, oldT), newT) + +prop_basic_localtime_fixed_delay = + forAll myStream $ evalT $ + Always (prop (sf25msec, const (== d))) + + where myStream :: Gen (SignalSampleStream Float) + myStream = fixedDelayStream d + + sf25msec = time >>> stepDiff (-d) + + d :: Time + d = 0.25 + +-- Par with broadcast (collection-oriented combinators) +-- TODO: Add integral to the list of SFs being tested +prop_broadcast = + forAll myStream $ evalT $ Always $ prop (sf, pred) + where myStream :: Gen (SignalSampleStream Float) + myStream = uniDistStream + + sf = parB [identity, (arr (+1))] + pred = (\x [y,z] -> x == y && (x + 1) == z) + +prop_arrow_1 = forAll myStream $ evalT $ + Always $ prop (arr id, \x y -> x == y) + where myStream :: Gen (SignalSampleStream Float) + myStream = uniDistStream + +prop_arrow_2 = forAll myStream $ evalT $ + Always $ prop (sf1 &&& sf2, const $ uncurry (==)) + where myStream :: Gen (SignalSampleStream Float) + myStream = uniDistStream + sf1 = arr (f >>> g) + sf2 = arr f >>> arr g + f = (+5) + g = (/20) + +prop_arrow_2' = + forAll f $ \f' -> + forAll g $ \g' -> + forAll myStream $ evalT $ + prop_arrow_2'' (apply f') (apply g') + + where myStream :: Gen (SignalSampleStream Int) + myStream = uniDistStream + + f, g :: Gen (Fun Int Int) + f = arbitrary + g = arbitrary + +prop_arrow_2'' f g = + Always $ prop (sf1 &&& sf2, const $ uncurry (==)) + where sf1 = arr (f >>> g) + sf2 = arr f >>> arr g + +-- Arrow composition (we use Int to avoid floating-point discrepancies) +prop_arrow_comp_1 = + forAll myStream $ evalT $ Always $ prop (sf, pred) + where myStream :: Gen (SignalSampleStream Int) + myStream = uniDistStream + + sf = arr (+1) >>> arr (+2) + pred = (\x y -> x + 3 == y) + +-- Arrow composition +prop_arrow_comp_2 = + forAll myStream $ evalT $ Always $ prop (sf, pred) + where myStream :: Gen (SignalSampleStream Float) + myStream = uniDistStream + + sf = constant 5.0 >>> arr (+1) + pred = const (== 6.0) + +-- Arrow composition +prop_arrow_comp_3 = + forAll myStream $ evalT $ Always $ prop (sf, pred) + where myStream :: Gen (SignalSampleStream Float) + myStream = fixedDelayStream 0.25 + + sf :: SF a Float + sf = constant 2.0 >>> integral >>> stepDiff (-0.5) + + pred = const (== 0.5) + +-- Delaying + +-- | Delaying by 0.0 has no effect +prop_delay_1 = + forAll myStream $ evalT $ prop_always_equal sfDelayed sf + where myStream :: Gen (SignalSampleStream Float) + myStream = uniDistStream + + sfDelayed = delay 0.0 undefined >>> sf + sf = arr (+1) + +-- | Delaying input signal by a small amount will fill in the "blank" signal +-- with the given value, which will become also the sample at the initial +-- time. +prop_delay_2 = + forAll myStream $ evalT $ + (prop (sfDelayed, (\x y -> y == initialValue))) + where myStream :: Gen (SignalSampleStream Float) + myStream = uniDistStream + + sfDelayed = delay 0.0001 initialValue + + initialValue = 17 + +prop_insert = + forAll initialValueG $ \initialValue -> + forAll finalValueG $ \finalValue -> + forAll myStream $ evalT $ + let sfStep = initialValue --> constant finalValue + + in And (prop (sfStep, const (== initialValue))) + (Next $ Always $ + (prop (sfStep, const (== finalValue)))) + + where myStream :: Gen (SignalSampleStream Float) + myStream = uniDistStream + + initialValueG :: Gen Float + initialValueG = arbitrary + + finalValueG :: Gen Float + finalValueG = arbitrary + +prop_derivative_1 = + forAll myStream $ evalT $ + Next $ Always $ prop ((sfDer &&& sfDerByHand), const close) + + where myStream :: Gen (SignalSampleStream Double) + myStream = fixedDelayStreamWith (\t -> sin(2 * pi * t)) der_step + + sfDer :: SF Time Time + sfDer = derivative + + sfDerByHand = localTime >>> arr (\t -> (2 * pi * cos (2 * pi * t))) + + close (x,y) = abs (x-y) < 0.05 + +prop_derivative_2 = + forAll myStream $ evalT $ + Next $ Always $ prop ( sfDer &&& sfDerByHand + , const close) + + where + myStream :: Gen (SignalSampleStream Double) + myStream = fixedDelayStream der_step + + sfDer :: SF Time Time + sfDer = localTime + >>> arr (\t -> sin(2*pi*t)) + >>> derivative + + sfDerByHand = localTime + >>> arr (\t -> 2*pi*cos (2*pi*t)) + + close (x,y) = abs (x-y) < 0.05 + +der_step = 0.001 + +stepDiff :: Num a => a -> SF a a +stepDiff z = loopPre z (arr (\(x,y) -> (x - y, x))) + +-- Events +prop_event_noevent = + forAll myStream $ evalT $ Always $ prop (sfNever, const (== noEvent)) + + where myStream :: Gen (SignalSampleStream Float) + myStream = uniDistStream + sfNever :: SF Float (Event Float) + sfNever = never + +prop_event_now = + forAll myStream $ evalT $ + -- (sf, p0) /\ O [] (sf, pn) + And (prop (sf, p0)) -- Initially + (Next $ Always $ prop (sf, pn)) -- After first sample + + where sf = Yampa.now 42.0 + + p0 x y = y == Event 42.0 + pn x y = y == noEvent + + myStream :: Gen (SignalSampleStream Float) + myStream = uniDistStream + +prop_event_after_0 = + forAll myStream $ evalT $ + -- (sf, p0) /\ O [] (sf, pn) + And (prop (sf, p0)) -- Initially + (Next $ Always $ prop (sf, pn)) -- After first sample + + where sf = after 0.0 42.0 + + p0 x y = y == Event 42.0 + pn x y = y == noEvent + + myStream :: Gen (SignalSampleStream Float) + myStream = uniDistStream + +prop_arrow_first_1 = + forAll myStream $ evalT $ Always $ prop (sf, pred) + where myStream :: Gen (SignalSampleStream Int) + myStream = uniDistStream + + sf = arr dup >>> first (constant 7) + pred = (\x y -> (7 :: Int, x) == y) + +prop_arrow_first_2 = + forAll myStream $ evalT $ Always $ prop (sf, pred) + where myStream :: Gen (SignalSampleStream Int) + myStream = uniDistStream + + sf = arr dup >>> first (arr (+1)) + pred = (\x y -> (x + 1, x) == y) + +prop_arrow_second_1 = + forAll myStream $ evalT $ Always $ prop (sf, pred) + where myStream :: Gen (SignalSampleStream Int) + myStream = uniDistStream + + sf = arr dup >>> second (constant 7) + pred = (\x y -> (x, 7 :: Int) == y) + +prop_arrow_second_2 = + forAll myStream $ evalT $ Always $ prop (sf, pred) + where myStream :: Gen (SignalSampleStream Int) + myStream = uniDistStream + + sf = arr dup >>> second (arr (+1)) + pred = (\x y -> (x, x + 1) == y) + +prop_arrow_id_0 = + forAll myStream $ evalT $ Always $ Prop ((sf1 &&& sf2) >>> pred) + where sf1 = arr id >>> integral + sf2 = integral + pred = arr $ uncurry (==) + + myStream :: Gen (SignalSampleStream Double) + myStream = uniDistStream + +prop_arrow_id_2 = + forAll myStream $ evalT $ Always $ Prop ((sf1 &&& sf2) >>> pred) + where sf1 = integral >>> arr id + sf2 = integral + pred = arr $ uncurry (==) + + myStream :: Gen (SignalSampleStream Double) + myStream = uniDistStream + +prop_arrow_assoc = + forAll myStream $ evalT $ Always $ Prop ((sf1 &&& sf2) >>> pred) + where sf1 = (integral >>> arr (*0.5)) >>> integral + sf2 = integral >>> (arr (*0.5) >>> integral) + pred = arr $ uncurry (==) + + myStream :: Gen (SignalSampleStream Double) + myStream = uniDistStream + +prop_arrow_arr_comp = + forAll myStream $ evalT $ Always $ Prop ((sf1 &&& sf2) >>> pred) + where sf1 = (arr ((*2.5) . (+3.0))) + sf2 = (arr (+3.0) >>> arr (*2.5)) + pred = arr (uncurry (==)) + + myStream :: Gen (SignalSampleStream Double) + myStream = uniDistStream + +prop_arrow_first_3 = + forAll myStream $ evalT $ Always $ Prop ((sf1 &&& sf2) >>> arr pred) + where sf1 = (arr dup >>> first (arr (*2.5))) + sf2 = (arr dup >>> arr (fun_prod (*2.5) id)) + pred = uncurry (==) + + myStream :: Gen (SignalSampleStream Double) + myStream = uniDistStream + +prop_arrow_first_distrib = + forAll myStream $ evalT $ Always $ Prop ((sf1 &&& sf2) >>> arr pred) + where sf1 = (arr dup >>> (first (integral >>> arr (+3.0)))) + sf2 = (arr dup >>> (first integral >>> first (arr (+3.0)))) + pred = uncurry (==) + + myStream :: Gen (SignalSampleStream Double) + myStream = uniDistStream + +prop_arrow_first_id_comm = + forAll myStream $ evalT $ Always $ Prop ((sf1 &&& sf2) >>> arr pred) + where sf1 = (arr dup >>> (first integral>>>arr (fun_prod id (+3.0)))) + sf2 = (arr dup >>> (arr (fun_prod id (+3.0))>>>first integral)) + pred = uncurry (==) + + myStream :: Gen (SignalSampleStream Double) + myStream = uniDistStream + +prop_arrow_first_nested = + forAll myStream $ evalT $ Always $ Prop ((sf1 &&& sf2) >>> arr pred) + where sf1 = (arr (\x -> ((x,x),())) >>> (first (first integral) >>> arr assoc)) + sf2 = (arr (\x -> ((x,x),())) >>> (arr assoc >>> first integral)) + + pred = uncurry (==) + + myStream :: Gen (SignalSampleStream Double) + myStream = uniDistStream + +prop_switch_t1 = + forAll myStream $ evalT $ + Always $ Prop ((switch_t1rec 42.0 &&& switch_tr) >>> arr same) + + where myStream :: Gen (SignalSampleStream Double) + myStream = fixedDelayStreamWith f 1.0 + f dt = l!!(floor dt) + l = [1.0, 1.0, 1.0, + 2.0, + 3.0, 3.0, + 4.0, 4.0, 4.0, + 5.0, + 6.0, 6.0, + 7.0, 7.0, 7.0, + 8.0] + ++ repeat 9.0 + + same = (uncurry (==)) + +-- Outputs current input, local time, and the value of the initializing +-- argument until some time has passed (determined by integrating a constant), +-- at which point an event occurs. +switch_t1a :: Double -> SF Double ((Double,Double,Double), Event ()) +switch_t1a x = (arr dup >>> second localTime >>> arr (\(a,t) -> (a,t,x))) + &&& (constant 0.5 + >>> integral + >>> (arr (>= (2.0 :: Double)) -- Used to work with no sig. + >>> edge)) + +-- This should raise an event IMMEDIATELY: no time should pass. +switch_t1b :: b -> SF a ((Double,Double,Double), Event a) +switch_t1b _ = constant (-999.0,-999.0,-999.0) &&& snap + +switch_t1rec :: Double -> SF Double (Double,Double,Double) +switch_t1rec x = + switch (switch_t1a x) $ \x -> + switch (switch_t1b x) $ \x -> + switch (switch_t1b x) $ + switch_t1rec + +switch_tr :: SF Double (Double, Double, Double) +switch_tr = proc (a) -> do + t <- localTime -< () + let mt = fromIntegral $ floor (mod' t 4.0) + v = case floor (t / 4.0) of + 0 -> 42.0 + 1 -> 3.0 + 2 -> 4.0 + 3 -> 7.0 + _ -> 9.0 + returnA -< (a, mt, v) + +infiniteSwitch sf1 sf2 input = + switched (evalAtZero sf1 input) /= switched (evalAtZero sf2 input) + where switched = isEvent . snd . fst + +switch1 = switch (simpleF) + (\_ -> switch1) + +simpleF = arr id &&& cond + where cond = arr (const (Event ())) + +delayedF = arr id &&& cond + where cond = after 1.5 (Event ()) + + +-- * Generic SF predicate building functions + +-- | Compares two SFs, resulting in true if they are always equal +prop_always_equal sf1 sf2 = + Always $ Prop ((sf1 &&& sf2) >>> arr sameResult) + where sameResult = uncurry (==) + +prop_arr_no_change f xs = + samples (fst (evalSF (arr f) xs)) == map f (samples xs) + +-- | Compares two SFs, returning true if they are close enough +prop_always_similar margin sf1 sf2 = + Always (Prop ((sf1 &&& sf2) >>> arr similar)) + where similar (x,y) = abs (x-y) <= margin + +sfMeasureIncrement :: Num b => b -> SF a b -> SF a b +sfMeasureIncrement init sf = loopPre init sf' + where sf' = (sf *** identity) >>> arr (\(n, o) -> (n - o, n)) + +fun_prod f g = \(x,y) -> (f x, g y) + +assoc :: ((a,b),c) -> (a,(b,c)) +assoc ((a,b),c) = (a,(b,c)) + +assocInv :: (a,(b,c)) -> ((a,b),c) +assocInv (a,(b,c)) = ((a,b),c) diff --git a/yampa-test.cabal b/yampa-test.cabal new file mode 100644 --- /dev/null +++ b/yampa-test.cabal @@ -0,0 +1,58 @@ +name: yampa-test +version: 0.1.0.0 +synopsis: Testing library for Yampa. +description: + Testing library for Yampa. + . + This library contains several testing and debugging facilities for Yampa. + In particular, it contains: + . + * Debugging signal functions using "Debug.Trace". + * A definition of Temporal Predicates based on LTL. + * Monitoring signal functions with ptLTL using Signal Predicates. + * A definition of Streams, and a Stream manipulation API. + * Signal/stream generators for QuickCheck. + . + A detailed explanation of these ideas is included in the ICFP 2017 paper + . + +homepage: http://github.com/ivanperez-keera/Yampa +license: BSD3 +license-file: LICENSE +author: Ivan Perez +maintainer: ivan.perez@keera.co.uk +-- copyright: +category: Testing +build-type: Simple +extra-source-files: CHANGELOG + +cabal-version: >=1.10 + +library + exposed-modules: FRP.Yampa.Debug + FRP.Yampa.LTLFuture + FRP.Yampa.LTLPast + FRP.Yampa.Stream + FRP.Yampa.QuickCheck + build-depends: base >=4 && <5, + Yampa >= 0.12, + QuickCheck, + normaldistribution + hs-source-dirs: src + default-language: Haskell2010 + +test-suite yampa-quicheck + type: detailed-0.9 + test-module: YampaQC + ghc-options: -Wall + default-language: Haskell2010 + + hs-source-dirs: tests + build-depends: + base < 5, + random, + Cabal >= 1.19, + QuickCheck, + Yampa, + yampa-test, + cabal-test-quickcheck