Skip to content

Commit

Permalink
Merge branch 'develop-yampa-test-style' into develop. Close #256.
Browse files Browse the repository at this point in the history
  • Loading branch information
ivanperez-keera committed Apr 7, 2023
2 parents 13e3e29 + feb535c commit a239f1f
Show file tree
Hide file tree
Showing 6 changed files with 255 additions and 245 deletions.
3 changes: 2 additions & 1 deletion yampa-test/CHANGELOG
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
2023-03-26 Ivan Perez <ivan.perez@keera.co.uk>
2023-04-06 Ivan Perez <ivan.perez@keera.co.uk>
* examples/: Introduce testing example from Yampa library (#257).
* src:/ Conformance with style guide (#256).

2023-02-07 Ivan Perez <ivan.perez@keera.co.uk>
* Yampa.cabal: Version bump (0.14.1) (#251).
Expand Down
20 changes: 13 additions & 7 deletions yampa-test/src/FRP/Yampa/Debug.hs
Original file line number Diff line number Diff line change
@@ -1,20 +1,26 @@
-- | Debug FRP networks by inspecting their behaviour inside.
-- |
-- Copyright : (c) Ivan Perez, 2017-2022
-- License : BSD-style (see the LICENSE file in the distribution)
-- Maintainer : ivan.perez@keera.co.uk
--
-- Debug FRP networks by inspecting their behaviour inside.
module FRP.Yampa.Debug where

import Debug.Trace
import FRP.Yampa
import System.IO.Unsafe
-- External imports
import Debug.Trace (trace)
import FRP.Yampa (SF, arr)
import System.IO.Unsafe (unsafePerformIO)

-- | 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.
-- | 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)))
traceSFWithIO f = arr (\x -> unsafePerformIO (f x >> return x))
67 changes: 39 additions & 28 deletions yampa-test/src/FRP/Yampa/LTLFuture.hs
Original file line number Diff line number Diff line change
@@ -1,31 +1,32 @@
{-# LANGUAGE GADTs #-}
-- | Linear Temporal Logics based on SFs.
-- |
-- Copyright : (c) Ivan Perez, 2017-2022
-- License : BSD-style (see the LICENSE file in the distribution)
-- Maintainer : ivan.perez@keera.co.uk
--
-- 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... :(

-- LTL predicates are parameterized over an input. A basic proposition is a
-- Signal Function that produces a boolean function.
module FRP.Yampa.LTLFuture
( TPred(..)
, evalT
)
where

import FRP.Yampa
import FRP.Yampa.Stream
-- External imports
import FRP.Yampa (DTime, SF, evalFuture)

-- Internal imports
import FRP.Yampa.Stream (SignalSampleStream, evalSF, firstSample)

-- | Type representing future-time linear temporal logic predicates with until
-- and next.
data TPred a where
SP :: SF a Bool -> TPred a
SP :: SF a Bool -> TPred a
And :: TPred a -> TPred a -> TPred a
Or :: TPred a -> TPred a -> TPred a
Not :: TPred a -> TPred a
Expand All @@ -39,31 +40,41 @@ data TPred a where
--
-- Returns 'True' if the temporal proposition is currently true.
evalT :: TPred a -> SignalSampleStream a -> Bool
evalT (SP sf) = \stream -> firstSample $ fst $ evalSF sf stream
evalT (SP 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 (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 -> 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)
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
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 (SP sf) = SP (f sf)
tPredMap f (SP sf) = SP (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)
Expand Down
51 changes: 14 additions & 37 deletions yampa-test/src/FRP/Yampa/LTLPast.hs
Original file line number Diff line number Diff line change
@@ -1,16 +1,20 @@
{-# LANGUAGE Arrows #-}
-- | Past-time Linear Temporal Logics based on SFs.
-- |
-- Copyright : (c) Ivan Perez, 2017-2022
-- License : BSD-style (see the LICENSE file in the distribution)
-- Maintainer : ivan.perez@keera.co.uk
--
-- 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
-- External imports
import FRP.Yampa (Event (..), SF, arr, iPre, loopPre, switch, (>>>))

-- | True if both inputs are True.
andSF :: SF (Bool, Bool) Bool
Expand All @@ -26,15 +30,15 @@ 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
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')
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')
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
Expand All @@ -44,34 +48,7 @@ lastSF = iPre False
-- 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)))
(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)
Loading

0 comments on commit a239f1f

Please sign in to comment.