-- Metric Temporal Logic (MTL) operators over a discrete time
-- domain consisting of sampled time values

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 at time t iff 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)

-- EventuallyPrev: True at time t iff 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 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)

-- AlwaysBeen: 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)

-- Until: 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
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)

-- Since: 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
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)

-- Release: 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)

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