-- |
-- Description: Metric Temporal Logic (MTL) over a discrete time domain.
--
-- Metric Temporal Logic (MTL) over a discrete time domain consisting of
-- sampled time values.
--
-- The operators in this module receive two additional arguments: a clock
-- stream @clk@, indicating the current time, and a distance between samples
-- @dist@.  For the purposes of explaining the MTL aspects, we ignore those
-- arguments.  If you are using streams for which you can treat time as a
-- discrete increasing number, you can safely assume that the clock is a
-- counter (i.e., @[0, 1, 2,...]@, which can be defined by the stream @counter
-- = [0] ++ counter@) and the distance between samples is @1@.

module Copilot.Library.MTL
  ( eventually, eventuallyPrev, always, alwaysBeen,
    until, release, since, Copilot.Library.MTL.trigger, matchingUntil,
    matchingRelease, matchingSince, matchingTrigger ) where

import Copilot.Language
import qualified Prelude as P
import Copilot.Library.Utils

-- It is necessary to provide a positive number of time units
-- dist to each function, where the distance between the times
-- of any two adjacent clock samples is no less than dist

-- | Eventually true in the future, within the time bounds specified.
--
-- @eventually l u clk dist s@ is true at time @t@ if and only if @s@ is true
-- at some time @t'@, where @(t + l) <= t' <= (t + u)@.
eventually :: ( Typed a, Integral a ) =>
  a -> a -> Stream a -> a -> Stream Bool -> Stream Bool
eventually :: a -> a -> Stream a -> a -> Stream Bool -> Stream Bool
eventually a
l a
u Stream a
clk a
dist Stream Bool
s = Stream a -> Stream Bool -> a -> Stream Bool
forall a.
(Num a, Eq a) =>
Stream a -> Stream Bool -> a -> Stream Bool
res Stream a
clk Stream Bool
s (a -> Stream Bool) -> a -> Stream Bool
forall a b. (a -> b) -> a -> b
$ (a
u a -> a -> a
forall a. Integral a => a -> a -> a
`P.div` a
dist) a -> a -> a
forall a. Num a => a -> a -> a
+ a
1
  where
  mins :: Stream a
mins = Stream a
clk Stream a -> Stream a -> Stream a
forall a. Num a => a -> a -> a
+ (a -> Stream a
forall a. Typed a => a -> Stream a
constant a
l)
  maxes :: Stream a
maxes = Stream a
clk Stream a -> Stream a -> Stream a
forall a. Num a => a -> a -> a
+ (a -> Stream a
forall a. Typed a => a -> Stream a
constant a
u)
  res :: Stream a -> Stream Bool -> a -> Stream Bool
res Stream a
_ Stream Bool
_ a
0 = Stream Bool
false
  res Stream a
c Stream Bool
s a
k =
    Stream a
c Stream a -> Stream a -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
<= Stream a
maxes Stream Bool -> Stream Bool -> Stream Bool
&& ((Stream a
mins Stream a -> Stream a -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
<= Stream a
c Stream Bool -> Stream Bool -> Stream Bool
&& Stream Bool
s) Stream Bool -> Stream Bool -> Stream Bool
|| Stream a -> Stream Bool -> a -> Stream Bool
nextRes Stream a
c Stream Bool
s a
k)
  nextRes :: Stream a -> Stream Bool -> a -> Stream Bool
nextRes Stream a
c Stream Bool
s a
k = Stream a -> Stream Bool -> a -> Stream Bool
res (Int -> Stream a -> Stream a
forall a. Typed a => Int -> Stream a -> Stream a
drop Int
1 Stream a
c) (Int -> Stream Bool -> Stream Bool
forall a. Typed a => Int -> Stream a -> Stream a
drop Int
1 Stream Bool
s) (a
k a -> a -> a
forall a. Num a => a -> a -> a
- a
1)

-- | True at some point in the past within the time bounds specified.
--
-- @eventuallyPrev l u clk dist s@ is true at time @t@ if and only if @s@ is
-- true at some time @t'@, where @(t - u) <= t' <= (t - l)@.
eventuallyPrev :: ( Typed a, Integral a ) =>
  a -> a -> Stream a -> a -> Stream Bool -> Stream Bool
eventuallyPrev :: a -> a -> Stream a -> a -> Stream Bool -> Stream Bool
eventuallyPrev a
l a
u Stream a
clk a
dist Stream Bool
s = Stream a -> Stream Bool -> a -> Stream Bool
forall a.
(Num a, Eq a) =>
Stream a -> Stream Bool -> a -> Stream Bool
res Stream a
clk Stream Bool
s (a -> Stream Bool) -> a -> Stream Bool
forall a b. (a -> b) -> a -> b
$ (a
u a -> a -> a
forall a. Integral a => a -> a -> a
`P.div` a
dist) a -> a -> a
forall a. Num a => a -> a -> a
+ a
1
  where
  mins :: Stream a
mins = Stream a
clk Stream a -> Stream a -> Stream a
forall a. Num a => a -> a -> a
- (a -> Stream a
forall a. Typed a => a -> Stream a
constant a
u)
  maxes :: Stream a
maxes = Stream a
clk Stream a -> Stream a -> Stream a
forall a. Num a => a -> a -> a
- (a -> Stream a
forall a. Typed a => a -> Stream a
constant a
l)
  res :: Stream a -> Stream Bool -> a -> Stream Bool
res Stream a
_ Stream Bool
_ a
0 = Stream Bool
false
  res Stream a
c Stream Bool
s a
k =
    Stream a
mins Stream a -> Stream a -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
<= Stream a
c Stream Bool -> Stream Bool -> Stream Bool
&& ((Stream a
c Stream a -> Stream a -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
<= Stream a
maxes Stream Bool -> Stream Bool -> Stream Bool
&& Stream Bool
s) Stream Bool -> Stream Bool -> Stream Bool
|| Stream a -> Stream Bool -> a -> Stream Bool
nextRes Stream a
c Stream Bool
s a
k)
  nextRes :: Stream a -> Stream Bool -> a -> Stream Bool
nextRes Stream a
c Stream Bool
s a
k = Stream a -> Stream Bool -> a -> Stream Bool
res ([a
0] [a] -> Stream a -> Stream a
forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream a
c) ([Bool
False] [Bool] -> Stream Bool -> Stream Bool
forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream Bool
s) (a
k a -> a -> a
forall a. Num a => a -> a -> a
- a
1)

-- | Always true in the future, within the time bounds specified.
--
-- @always l u clk dist s@ is true at time @t@ iff @s@ is true at all times
-- @t'@ where @(t + l) <= t' <= (t + u)@.
always :: ( Typed a, Integral a ) =>
  a -> a -> Stream a -> a -> Stream Bool -> Stream Bool
always :: a -> a -> Stream a -> a -> Stream Bool -> Stream Bool
always a
l a
u Stream a
clk a
dist Stream Bool
s = Stream a -> Stream Bool -> a -> Stream Bool
forall a.
(Num a, Eq a) =>
Stream a -> Stream Bool -> a -> Stream Bool
res Stream a
clk Stream Bool
s (a -> Stream Bool) -> a -> Stream Bool
forall a b. (a -> b) -> a -> b
$ (a
u a -> a -> a
forall a. Integral a => a -> a -> a
`P.div` a
dist) a -> a -> a
forall a. Num a => a -> a -> a
+ a
1
  where
  mins :: Stream a
mins = Stream a
clk Stream a -> Stream a -> Stream a
forall a. Num a => a -> a -> a
+ (a -> Stream a
forall a. Typed a => a -> Stream a
constant a
l)
  maxes :: Stream a
maxes = Stream a
clk Stream a -> Stream a -> Stream a
forall a. Num a => a -> a -> a
+ (a -> Stream a
forall a. Typed a => a -> Stream a
constant a
u)
  res :: Stream a -> Stream Bool -> a -> Stream Bool
res Stream a
_ Stream Bool
_ a
0 = Stream Bool
true
  res Stream a
c Stream Bool
s a
k =
    Stream a
c Stream a -> Stream a -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
> Stream a
maxes Stream Bool -> Stream Bool -> Stream Bool
|| ((Stream a
mins Stream a -> Stream a -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
<= Stream a
c Stream Bool -> Stream Bool -> Stream Bool
==> Stream Bool
s) Stream Bool -> Stream Bool -> Stream Bool
&& Stream a -> Stream Bool -> a -> Stream Bool
nextRes Stream a
c Stream Bool
s a
k)
  nextRes :: Stream a -> Stream Bool -> a -> Stream Bool
nextRes Stream a
c Stream Bool
s a
k = Stream a -> Stream Bool -> a -> Stream Bool
res (Int -> Stream a -> Stream a
forall a. Typed a => Int -> Stream a -> Stream a
drop Int
1 Stream a
c) (Int -> Stream Bool -> Stream Bool
forall a. Typed a => Int -> Stream a -> Stream a
drop Int
1 Stream Bool
s) (a
k a -> a -> a
forall a. Num a => a -> a -> a
- a
1)

-- | Always true in the past, within the time bounds specified.
--
-- @alwaysBeen l u clk dist s@ is true at time @t@ iff @s@ is true at all times
-- @t'@ where @(t - u) <= t' <= (t - l)@.
alwaysBeen :: ( Typed a, Integral a ) =>
  a -> a -> Stream a -> a -> Stream Bool -> Stream Bool
alwaysBeen :: a -> a -> Stream a -> a -> Stream Bool -> Stream Bool
alwaysBeen a
l a
u Stream a
clk a
dist Stream Bool
s = Stream a -> Stream Bool -> a -> Stream Bool
forall a.
(Num a, Eq a) =>
Stream a -> Stream Bool -> a -> Stream Bool
res Stream a
clk Stream Bool
s (a -> Stream Bool) -> a -> Stream Bool
forall a b. (a -> b) -> a -> b
$ (a
u a -> a -> a
forall a. Integral a => a -> a -> a
`P.div` a
dist) a -> a -> a
forall a. Num a => a -> a -> a
+ a
1
  where
  mins :: Stream a
mins = Stream a
clk Stream a -> Stream a -> Stream a
forall a. Num a => a -> a -> a
- (a -> Stream a
forall a. Typed a => a -> Stream a
constant a
u)
  maxes :: Stream a
maxes = Stream a
clk Stream a -> Stream a -> Stream a
forall a. Num a => a -> a -> a
- (a -> Stream a
forall a. Typed a => a -> Stream a
constant a
l)
  res :: Stream a -> Stream Bool -> a -> Stream Bool
res Stream a
_ Stream Bool
_ a
0 = Stream Bool
true
  res Stream a
c Stream Bool
s a
k =
    Stream a
c Stream a -> Stream a -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
< Stream a
mins Stream Bool -> Stream Bool -> Stream Bool
|| ((Stream a
c Stream a -> Stream a -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
<= Stream a
maxes Stream Bool -> Stream Bool -> Stream Bool
==> Stream Bool
s) Stream Bool -> Stream Bool -> Stream Bool
&& Stream a -> Stream Bool -> a -> Stream Bool
nextRes Stream a
c Stream Bool
s a
k)
  nextRes :: Stream a -> Stream Bool -> a -> Stream Bool
nextRes Stream a
c Stream Bool
s a
k = Stream a -> Stream Bool -> a -> Stream Bool
res ([a
0] [a] -> Stream a -> Stream a
forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream a
c) ([Bool
True] [Bool] -> Stream Bool -> Stream Bool
forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream Bool
s) (a
k a -> a -> a
forall a. Num a => a -> a -> a
- a
1)

-- | True until another stream is true, within the time bounds specified.
--
-- @until l u clk dist s0 s1@ is true at time @t@ iff there exists a @d@, with
-- @l <= d <= u@, such that @s1@ is true at time @(t + d)@, and for all times
-- @t'@ with @t <= t' < t + d@, @s0@ is true at those times.
until :: ( Typed a, Integral a ) =>
  a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
until :: a
-> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
until a
l a
u Stream a
clk a
dist Stream Bool
s0 Stream Bool
s1 = Stream a -> Stream Bool -> Stream Bool -> a -> Stream Bool
forall a.
(Num a, Eq a) =>
Stream a -> Stream Bool -> Stream Bool -> a -> Stream Bool
res Stream a
clk Stream Bool
s0 Stream Bool
s1 (a -> Stream Bool) -> a -> Stream Bool
forall a b. (a -> b) -> a -> b
$ (a
u a -> a -> a
forall a. Integral a => a -> a -> a
`P.div` a
dist) a -> a -> a
forall a. Num a => a -> a -> a
+ a
1
  where
  mins :: Stream a
mins = Stream a
clk Stream a -> Stream a -> Stream a
forall a. Num a => a -> a -> a
+ (a -> Stream a
forall a. Typed a => a -> Stream a
constant a
l)
  maxes :: Stream a
maxes = Stream a
clk Stream a -> Stream a -> Stream a
forall a. Num a => a -> a -> a
+ (a -> Stream a
forall a. Typed a => a -> Stream a
constant a
u)
  res :: Stream a -> Stream Bool -> Stream Bool -> a -> Stream Bool
res Stream a
_ Stream Bool
_ Stream Bool
_ a
0 = Stream Bool
false
  res Stream a
c Stream Bool
s Stream Bool
s' a
k =
    Stream a
c Stream a -> Stream a -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
<= Stream a
maxes Stream Bool -> Stream Bool -> Stream Bool
&& ((Stream a
mins Stream a -> Stream a -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
<= Stream a
c Stream Bool -> Stream Bool -> Stream Bool
&& Stream Bool
s') Stream Bool -> Stream Bool -> Stream Bool
|| (Stream Bool
s Stream Bool -> Stream Bool -> Stream Bool
&& Stream a -> Stream Bool -> Stream Bool -> a -> Stream Bool
nextRes Stream a
c Stream Bool
s Stream Bool
s' a
k))
  nextRes :: Stream a -> Stream Bool -> Stream Bool -> a -> Stream Bool
nextRes Stream a
c Stream Bool
s Stream Bool
s' a
k = Stream a -> Stream Bool -> Stream Bool -> a -> Stream Bool
res (Int -> Stream a -> Stream a
forall a. Typed a => Int -> Stream a -> Stream a
drop Int
1 Stream a
c) (Int -> Stream Bool -> Stream Bool
forall a. Typed a => Int -> Stream a -> Stream a
drop Int
1 Stream Bool
s) (Int -> Stream Bool -> Stream Bool
forall a. Typed a => Int -> Stream a -> Stream a
drop Int
1 Stream Bool
s') (a
k a -> a -> a
forall a. Num a => a -> a -> a
- a
1)

-- | True since another stream became true, within the time bounds specified.
--
-- @since l u clk dist s0 s1@ is true at time @t@ iff there exists a @d@, with
-- @l <= d <= u@, such that @s1@ is true at time @(t - d)@, and for all times
-- @t'@ with @t - d < t' <= t@, @s0@ is true at those times.
since :: ( Typed a, Integral a ) =>
  a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
since :: a
-> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
since a
l a
u Stream a
clk a
dist Stream Bool
s0 Stream Bool
s1 = Stream a -> Stream Bool -> Stream Bool -> a -> Stream Bool
forall a.
(Num a, Eq a) =>
Stream a -> Stream Bool -> Stream Bool -> a -> Stream Bool
res Stream a
clk Stream Bool
s0 Stream Bool
s1 (a -> Stream Bool) -> a -> Stream Bool
forall a b. (a -> b) -> a -> b
$ (a
u a -> a -> a
forall a. Integral a => a -> a -> a
`P.div` a
dist) a -> a -> a
forall a. Num a => a -> a -> a
+ a
1
  where
  mins :: Stream a
mins = Stream a
clk Stream a -> Stream a -> Stream a
forall a. Num a => a -> a -> a
- (a -> Stream a
forall a. Typed a => a -> Stream a
constant a
u)
  maxes :: Stream a
maxes = Stream a
clk Stream a -> Stream a -> Stream a
forall a. Num a => a -> a -> a
- (a -> Stream a
forall a. Typed a => a -> Stream a
constant a
l)
  res :: Stream a -> Stream Bool -> Stream Bool -> a -> Stream Bool
res Stream a
_ Stream Bool
_ Stream Bool
_ a
0 = Stream Bool
false
  res Stream a
c Stream Bool
s Stream Bool
s' a
k =
    Stream a
mins Stream a -> Stream a -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
<= Stream a
c Stream Bool -> Stream Bool -> Stream Bool
&& ((Stream a
c Stream a -> Stream a -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
<= Stream a
maxes Stream Bool -> Stream Bool -> Stream Bool
&& Stream Bool
s') Stream Bool -> Stream Bool -> Stream Bool
|| (Stream Bool
s Stream Bool -> Stream Bool -> Stream Bool
&& Stream a -> Stream Bool -> Stream Bool -> a -> Stream Bool
nextRes Stream a
c Stream Bool
s Stream Bool
s' a
k))
  nextRes :: Stream a -> Stream Bool -> Stream Bool -> a -> Stream Bool
nextRes Stream a
c Stream Bool
s Stream Bool
s' a
k = Stream a -> Stream Bool -> Stream Bool -> a -> Stream Bool
res ([a
0] [a] -> Stream a -> Stream a
forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream a
c) ([Bool
True] [Bool] -> Stream Bool -> Stream Bool
forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream Bool
s) ([Bool
False] [Bool] -> Stream Bool -> Stream Bool
forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream Bool
s') (a
k a -> a -> a
forall a. Num a => a -> a -> a
- a
1)

-- | True if a stream is true until another one releases it.
--
-- @release l u clk dist s0 s1@ is true at time @t@ iff for all @d@ with @l <=
-- d <= u@ where there is a sample at time @(t + d)@, @s1@ is true at time @(t
-- + d)@, or @s0@ has a true sample at some time @t'@ with @t <= t' < t + d@.
release :: ( Typed a, Integral a ) =>
  a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
release :: a
-> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
release a
l a
u Stream a
clk a
dist Stream Bool
s0 Stream Bool
s1 =
  (Stream a
mins Stream a -> Stream a -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
> Stream a
clk Stream Bool -> Stream Bool -> Stream Bool
|| Stream a
clk Stream a -> Stream a -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
> Stream a
maxes Stream Bool -> Stream Bool -> Stream Bool
|| Stream Bool
s1) Stream Bool -> Stream Bool -> Stream Bool
&&
  (Stream a -> Stream Bool -> Stream Bool -> a -> Stream Bool
forall a.
(Num a, Eq a) =>
Stream a -> Stream Bool -> Stream Bool -> a -> Stream Bool
res (Int -> Stream a -> Stream a
forall a. Typed a => Int -> Stream a -> Stream a
drop Int
1 Stream a
clk) Stream Bool
s0 (Int -> Stream Bool -> Stream Bool
forall a. Typed a => Int -> Stream a -> Stream a
drop Int
1 Stream Bool
s1) (a -> Stream Bool) -> a -> Stream Bool
forall a b. (a -> b) -> a -> b
$ a
u a -> a -> a
forall a. Integral a => a -> a -> a
`P.div` a
dist)
  where
  mins :: Stream a
mins = Stream a
clk Stream a -> Stream a -> Stream a
forall a. Num a => a -> a -> a
+ (a -> Stream a
forall a. Typed a => a -> Stream a
constant a
l)
  maxes :: Stream a
maxes = Stream a
clk Stream a -> Stream a -> Stream a
forall a. Num a => a -> a -> a
+ (a -> Stream a
forall a. Typed a => a -> Stream a
constant a
u)
  res :: Stream a -> Stream Bool -> Stream Bool -> a -> Stream Bool
res Stream a
_ Stream Bool
_ Stream Bool
_ a
0 = Stream Bool
true
  res Stream a
c Stream Bool
s Stream Bool
s' a
k =
    Stream Bool
s Stream Bool -> Stream Bool -> Stream Bool
|| ((Stream a
mins Stream a -> Stream a -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
> Stream a
c Stream Bool -> Stream Bool -> Stream Bool
|| Stream a
c Stream a -> Stream a -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
> Stream a
maxes Stream Bool -> Stream Bool -> Stream Bool
|| Stream Bool
s') Stream Bool -> Stream Bool -> Stream Bool
&& Stream a -> Stream Bool -> Stream Bool -> a -> Stream Bool
nextRes Stream a
c Stream Bool
s Stream Bool
s' a
k)
  nextRes :: Stream a -> Stream Bool -> Stream Bool -> a -> Stream Bool
nextRes Stream a
c Stream Bool
s Stream Bool
s' a
k = Stream a -> Stream Bool -> Stream Bool -> a -> Stream Bool
res (Int -> Stream a -> Stream a
forall a. Typed a => Int -> Stream a -> Stream a
drop Int
1 Stream a
c) (Int -> Stream Bool -> Stream Bool
forall a. Typed a => Int -> Stream a -> Stream a
drop Int
1 Stream Bool
s) (Int -> Stream Bool -> Stream Bool
forall a. Typed a => Int -> Stream a -> Stream a
drop Int
1 Stream Bool
s') (a
k a -> a -> a
forall a. Num a => a -> a -> a
- a
1)

-- | True if a stream is true until another one releases it.
--
-- Trigger: True at time @t@ iff for all @d@ with @l <= d <= u@ where there is
-- a sample at time @(t - d)@, @s1@ is true at time @(t - d)@, or @s0@ has a
-- true sample at some time @t'@ with @t - d < t' <= t@.
trigger :: ( Typed a, Integral a ) =>
  a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
trigger :: a
-> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
trigger a
l a
u Stream a
clk a
dist Stream Bool
s0 Stream Bool
s1 =
  (Stream a
mins Stream a -> Stream a -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
> Stream a
clk Stream Bool -> Stream Bool -> Stream Bool
|| Stream a
clk Stream a -> Stream a -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
> Stream a
maxes Stream Bool -> Stream Bool -> Stream Bool
|| Stream Bool
s1) Stream Bool -> Stream Bool -> Stream Bool
&&
  (Stream a -> Stream Bool -> Stream Bool -> a -> Stream Bool
forall a.
(Num a, Eq a) =>
Stream a -> Stream Bool -> Stream Bool -> a -> Stream Bool
res ([a
0] [a] -> Stream a -> Stream a
forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream a
clk) Stream Bool
s0 ([Bool
True] [Bool] -> Stream Bool -> Stream Bool
forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream Bool
s1) (a -> Stream Bool) -> a -> Stream Bool
forall a b. (a -> b) -> a -> b
$ a
u a -> a -> a
forall a. Integral a => a -> a -> a
`P.div` a
dist)
  where
  mins :: Stream a
mins = Stream a
clk Stream a -> Stream a -> Stream a
forall a. Num a => a -> a -> a
- (a -> Stream a
forall a. Typed a => a -> Stream a
constant a
u)
  maxes :: Stream a
maxes = Stream a
clk Stream a -> Stream a -> Stream a
forall a. Num a => a -> a -> a
- (a -> Stream a
forall a. Typed a => a -> Stream a
constant a
l)
  res :: Stream a -> Stream Bool -> Stream Bool -> a -> Stream Bool
res Stream a
_ Stream Bool
_ Stream Bool
_ a
0 = Stream Bool
true
  res Stream a
c Stream Bool
s Stream Bool
s' a
k =
    Stream Bool
s Stream Bool -> Stream Bool -> Stream Bool
|| ((Stream a
mins Stream a -> Stream a -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
> Stream a
c Stream Bool -> Stream Bool -> Stream Bool
|| Stream a
c Stream a -> Stream a -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
> Stream a
maxes Stream Bool -> Stream Bool -> Stream Bool
|| Stream Bool
s') Stream Bool -> Stream Bool -> Stream Bool
&& Stream a -> Stream Bool -> Stream Bool -> a -> Stream Bool
nextRes Stream a
c Stream Bool
s Stream Bool
s' a
k)
  nextRes :: Stream a -> Stream Bool -> Stream Bool -> a -> Stream Bool
nextRes Stream a
c Stream Bool
s Stream Bool
s' a
k = Stream a -> Stream Bool -> Stream Bool -> a -> Stream Bool
res ([a
0] [a] -> Stream a -> Stream a
forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream a
c) ([Bool
False] [Bool] -> Stream Bool -> Stream Bool
forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream Bool
s) ([Bool
True] [Bool] -> Stream Bool -> Stream Bool
forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream Bool
s') (a
k a -> a -> a
forall a. Num a => a -> a -> a
- a
1)

-- Matching Variants

-- | Matching Until: Same semantics as @until@, except with both @s1@ and @s0@
-- needing to hold at time @(t + d)@ instead of just @s1@.
matchingUntil :: ( Typed a, Integral a ) =>
  a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
matchingUntil :: a
-> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
matchingUntil a
l a
u Stream a
clk a
dist Stream Bool
s0 Stream Bool
s1 = Stream a -> Stream Bool -> Stream Bool -> a -> Stream Bool
forall a.
(Num a, Eq a) =>
Stream a -> Stream Bool -> Stream Bool -> a -> Stream Bool
res Stream a
clk Stream Bool
s0 Stream Bool
s1 (a -> Stream Bool) -> a -> Stream Bool
forall a b. (a -> b) -> a -> b
$ (a
u a -> a -> a
forall a. Integral a => a -> a -> a
`P.div` a
dist) a -> a -> a
forall a. Num a => a -> a -> a
+ a
1
  where
  mins :: Stream a
mins = Stream a
clk Stream a -> Stream a -> Stream a
forall a. Num a => a -> a -> a
+ (a -> Stream a
forall a. Typed a => a -> Stream a
constant a
l)
  maxes :: Stream a
maxes = Stream a
clk Stream a -> Stream a -> Stream a
forall a. Num a => a -> a -> a
+ (a -> Stream a
forall a. Typed a => a -> Stream a
constant a
u)
  res :: Stream a -> Stream Bool -> Stream Bool -> a -> Stream Bool
res Stream a
_ Stream Bool
_ Stream Bool
_ a
0 = Stream Bool
false
  res Stream a
c Stream Bool
s Stream Bool
s' a
k =
    Stream a
c Stream a -> Stream a -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
<= Stream a
maxes Stream Bool -> Stream Bool -> Stream Bool
&& Stream Bool
s Stream Bool -> Stream Bool -> Stream Bool
&& ((Stream a
mins Stream a -> Stream a -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
<= Stream a
c Stream Bool -> Stream Bool -> Stream Bool
&& Stream Bool
s') Stream Bool -> Stream Bool -> Stream Bool
|| Stream a -> Stream Bool -> Stream Bool -> a -> Stream Bool
nextRes Stream a
c Stream Bool
s Stream Bool
s' a
k)
  nextRes :: Stream a -> Stream Bool -> Stream Bool -> a -> Stream Bool
nextRes Stream a
c Stream Bool
s Stream Bool
s' a
k = Stream a -> Stream Bool -> Stream Bool -> a -> Stream Bool
res (Int -> Stream a -> Stream a
forall a. Typed a => Int -> Stream a -> Stream a
drop Int
1 Stream a
c) (Int -> Stream Bool -> Stream Bool
forall a. Typed a => Int -> Stream a -> Stream a
drop Int
1 Stream Bool
s) (Int -> Stream Bool -> Stream Bool
forall a. Typed a => Int -> Stream a -> Stream a
drop Int
1 Stream Bool
s') (a
k a -> a -> a
forall a. Num a => a -> a -> a
- a
1)

-- | Matching Since: Same semantics as @since@, except with both @s1@ and @s0@
-- needing to hold at time @(t - d)@ instead of just @s1@.
matchingSince :: ( Typed a, Integral a ) =>
  a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
matchingSince :: a
-> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
matchingSince a
l a
u Stream a
clk a
dist Stream Bool
s0 Stream Bool
s1 = a
-> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
forall a.
(Typed a, Integral a) =>
a
-> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
since a
l a
u Stream a
clk a
dist Stream Bool
s0 (Stream Bool
s0 Stream Bool -> Stream Bool -> Stream Bool
&& Stream Bool
s1)

-- | Matching Release: Same semantics as @release@, except with @s1@ or @s0@
-- needing to hold at time @(t + d)@ instead of just @s1@.
matchingRelease :: ( Typed a, Integral a ) =>
  a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
matchingRelease :: a
-> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
matchingRelease a
l a
u Stream a
clk a
dist Stream Bool
s0 Stream Bool
s1 = Stream a -> Stream Bool -> Stream Bool -> a -> Stream Bool
forall a.
(Num a, Eq a) =>
Stream a -> Stream Bool -> Stream Bool -> a -> Stream Bool
res Stream a
clk Stream Bool
s0 Stream Bool
s1 (a -> Stream Bool) -> a -> Stream Bool
forall a b. (a -> b) -> a -> b
$ (a
u a -> a -> a
forall a. Integral a => a -> a -> a
`P.div` a
dist) a -> a -> a
forall a. Num a => a -> a -> a
+ a
1
  where
  mins :: Stream a
mins = Stream a
clk Stream a -> Stream a -> Stream a
forall a. Num a => a -> a -> a
+ (a -> Stream a
forall a. Typed a => a -> Stream a
constant a
l)
  maxes :: Stream a
maxes = Stream a
clk Stream a -> Stream a -> Stream a
forall a. Num a => a -> a -> a
+ (a -> Stream a
forall a. Typed a => a -> Stream a
constant a
u)
  res :: Stream a -> Stream Bool -> Stream Bool -> a -> Stream Bool
res Stream a
_ Stream Bool
_ Stream Bool
_ a
0 = Stream Bool
true
  res Stream a
c Stream Bool
s Stream Bool
s' a
k =
    Stream Bool
s Stream Bool -> Stream Bool -> Stream Bool
|| ((Stream a
mins Stream a -> Stream a -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
> Stream a
c Stream Bool -> Stream Bool -> Stream Bool
|| Stream a
c Stream a -> Stream a -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
> Stream a
maxes Stream Bool -> Stream Bool -> Stream Bool
|| Stream Bool
s') Stream Bool -> Stream Bool -> Stream Bool
&& Stream a -> Stream Bool -> Stream Bool -> a -> Stream Bool
nextRes Stream a
c Stream Bool
s Stream Bool
s' a
k)
  nextRes :: Stream a -> Stream Bool -> Stream Bool -> a -> Stream Bool
nextRes Stream a
c Stream Bool
s Stream Bool
s' a
k = Stream a -> Stream Bool -> Stream Bool -> a -> Stream Bool
res (Int -> Stream a -> Stream a
forall a. Typed a => Int -> Stream a -> Stream a
drop Int
1 Stream a
c) (Int -> Stream Bool -> Stream Bool
forall a. Typed a => Int -> Stream a -> Stream a
drop Int
1 Stream Bool
s) (Int -> Stream Bool -> Stream Bool
forall a. Typed a => Int -> Stream a -> Stream a
drop Int
1 Stream Bool
s') (a
k a -> a -> a
forall a. Num a => a -> a -> a
- a
1)

-- | Matching Trigger: Same semantics as @trigger@, except with @s1@ or @s0@
-- needing to hold at time @(t - d)@ instead of just @s1@.
matchingTrigger :: ( Typed a, Integral a ) =>
  a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
matchingTrigger :: a
-> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
matchingTrigger a
l a
u Stream a
clk a
dist Stream Bool
s0 Stream Bool
s1 =
  a
-> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
forall a.
(Typed a, Integral a) =>
a
-> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
Copilot.Library.MTL.trigger a
l a
u Stream a
clk a
dist Stream Bool
s0 (Stream Bool
s0 Stream Bool -> Stream Bool -> Stream Bool
|| Stream Bool
s1)