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
eventually :: ( Typed a, Integral a ) =>
a -> a -> Stream a -> a -> Stream Bool -> Stream Bool
eventually :: forall a.
(Typed a, Integral a) =>
a -> a -> Stream a -> a -> Stream Bool -> Stream Bool
eventually a
l a
u Stream a
clk a
dist Stream Bool
s = forall {t}.
(Num t, Eq t) =>
Stream a -> Stream Bool -> t -> Stream Bool
res Stream a
clk Stream Bool
s forall a b. (a -> b) -> a -> b
$ (a
u forall a. Integral a => a -> a -> a
`P.div` a
dist) forall a. Num a => a -> a -> a
+ a
1
where
mins :: Stream a
mins = Stream a
clk forall a. Num a => a -> a -> a
+ (forall a. Typed a => a -> Stream a
constant a
l)
maxes :: Stream a
maxes = Stream a
clk forall a. Num a => a -> a -> a
+ (forall a. Typed a => a -> Stream a
constant a
u)
res :: Stream a -> Stream Bool -> t -> Stream Bool
res Stream a
_ Stream Bool
_ t
0 = Stream Bool
false
res Stream a
c Stream Bool
s t
k =
Stream a
c forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
<= Stream a
maxes Stream Bool -> Stream Bool -> Stream Bool
&& ((Stream a
mins 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 -> t -> Stream Bool
nextRes Stream a
c Stream Bool
s t
k)
nextRes :: Stream a -> Stream Bool -> t -> Stream Bool
nextRes Stream a
c Stream Bool
s t
k = Stream a -> Stream Bool -> t -> Stream Bool
res (forall a. Typed a => Int -> Stream a -> Stream a
drop Int
1 Stream a
c) (forall a. Typed a => Int -> Stream a -> Stream a
drop Int
1 Stream Bool
s) (t
k forall a. Num a => a -> a -> a
- t
1)
eventuallyPrev :: ( Typed a, Integral a ) =>
a -> a -> Stream a -> a -> Stream Bool -> Stream Bool
eventuallyPrev :: forall a.
(Typed a, Integral a) =>
a -> a -> Stream a -> a -> Stream Bool -> Stream Bool
eventuallyPrev a
l a
u Stream a
clk a
dist Stream Bool
s = forall {t}.
(Num t, Eq t) =>
Stream a -> Stream Bool -> t -> Stream Bool
res Stream a
clk Stream Bool
s forall a b. (a -> b) -> a -> b
$ (a
u forall a. Integral a => a -> a -> a
`P.div` a
dist) forall a. Num a => a -> a -> a
+ a
1
where
mins :: Stream a
mins = Stream a
clk forall a. Num a => a -> a -> a
- (forall a. Typed a => a -> Stream a
constant a
u)
maxes :: Stream a
maxes = Stream a
clk forall a. Num a => a -> a -> a
- (forall a. Typed a => a -> Stream a
constant a
l)
res :: Stream a -> Stream Bool -> t -> Stream Bool
res Stream a
_ Stream Bool
_ t
0 = Stream Bool
false
res Stream a
c Stream Bool
s t
k =
Stream a
mins forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
<= Stream a
c Stream Bool -> Stream Bool -> Stream Bool
&& ((Stream a
c 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 -> t -> Stream Bool
nextRes Stream a
c Stream Bool
s t
k)
nextRes :: Stream a -> Stream Bool -> t -> Stream Bool
nextRes Stream a
c Stream Bool
s t
k = Stream a -> Stream Bool -> t -> Stream Bool
res ([a
0] forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream a
c) ([Bool
False] forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream Bool
s) (t
k forall a. Num a => a -> a -> a
- t
1)
always :: ( Typed a, Integral a ) =>
a -> a -> Stream a -> a -> Stream Bool -> Stream Bool
always :: forall a.
(Typed a, Integral a) =>
a -> a -> Stream a -> a -> Stream Bool -> Stream Bool
always a
l a
u Stream a
clk a
dist Stream Bool
s = forall {t}.
(Num t, Eq t) =>
Stream a -> Stream Bool -> t -> Stream Bool
res Stream a
clk Stream Bool
s forall a b. (a -> b) -> a -> b
$ (a
u forall a. Integral a => a -> a -> a
`P.div` a
dist) forall a. Num a => a -> a -> a
+ a
1
where
mins :: Stream a
mins = Stream a
clk forall a. Num a => a -> a -> a
+ (forall a. Typed a => a -> Stream a
constant a
l)
maxes :: Stream a
maxes = Stream a
clk forall a. Num a => a -> a -> a
+ (forall a. Typed a => a -> Stream a
constant a
u)
res :: Stream a -> Stream Bool -> t -> Stream Bool
res Stream a
_ Stream Bool
_ t
0 = Stream Bool
true
res Stream a
c Stream Bool
s t
k =
Stream a
c forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
> Stream a
maxes Stream Bool -> Stream Bool -> Stream Bool
|| ((Stream a
mins 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 -> t -> Stream Bool
nextRes Stream a
c Stream Bool
s t
k)
nextRes :: Stream a -> Stream Bool -> t -> Stream Bool
nextRes Stream a
c Stream Bool
s t
k = Stream a -> Stream Bool -> t -> Stream Bool
res (forall a. Typed a => Int -> Stream a -> Stream a
drop Int
1 Stream a
c) (forall a. Typed a => Int -> Stream a -> Stream a
drop Int
1 Stream Bool
s) (t
k forall a. Num a => a -> a -> a
- t
1)
alwaysBeen :: ( Typed a, Integral a ) =>
a -> a -> Stream a -> a -> Stream Bool -> Stream Bool
alwaysBeen :: forall a.
(Typed a, Integral a) =>
a -> a -> Stream a -> a -> Stream Bool -> Stream Bool
alwaysBeen a
l a
u Stream a
clk a
dist Stream Bool
s = forall {t}.
(Num t, Eq t) =>
Stream a -> Stream Bool -> t -> Stream Bool
res Stream a
clk Stream Bool
s forall a b. (a -> b) -> a -> b
$ (a
u forall a. Integral a => a -> a -> a
`P.div` a
dist) forall a. Num a => a -> a -> a
+ a
1
where
mins :: Stream a
mins = Stream a
clk forall a. Num a => a -> a -> a
- (forall a. Typed a => a -> Stream a
constant a
u)
maxes :: Stream a
maxes = Stream a
clk forall a. Num a => a -> a -> a
- (forall a. Typed a => a -> Stream a
constant a
l)
res :: Stream a -> Stream Bool -> t -> Stream Bool
res Stream a
_ Stream Bool
_ t
0 = Stream Bool
true
res Stream a
c Stream Bool
s t
k =
Stream a
c forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
< Stream a
mins Stream Bool -> Stream Bool -> Stream Bool
|| ((Stream a
c 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 -> t -> Stream Bool
nextRes Stream a
c Stream Bool
s t
k)
nextRes :: Stream a -> Stream Bool -> t -> Stream Bool
nextRes Stream a
c Stream Bool
s t
k = Stream a -> Stream Bool -> t -> Stream Bool
res ([a
0] forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream a
c) ([Bool
True] forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream Bool
s) (t
k forall a. Num a => a -> a -> a
- t
1)
until :: ( Typed a, Integral a ) =>
a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
until :: forall a.
(Typed a, Integral a) =>
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 = forall {t}.
(Num t, Eq t) =>
Stream a -> Stream Bool -> Stream Bool -> t -> Stream Bool
res Stream a
clk Stream Bool
s0 Stream Bool
s1 forall a b. (a -> b) -> a -> b
$ (a
u forall a. Integral a => a -> a -> a
`P.div` a
dist) forall a. Num a => a -> a -> a
+ a
1
where
mins :: Stream a
mins = Stream a
clk forall a. Num a => a -> a -> a
+ (forall a. Typed a => a -> Stream a
constant a
l)
maxes :: Stream a
maxes = Stream a
clk forall a. Num a => a -> a -> a
+ (forall a. Typed a => a -> Stream a
constant a
u)
res :: Stream a -> Stream Bool -> Stream Bool -> t -> Stream Bool
res Stream a
_ Stream Bool
_ Stream Bool
_ t
0 = Stream Bool
false
res Stream a
c Stream Bool
s Stream Bool
s' t
k =
Stream a
c forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
<= Stream a
maxes Stream Bool -> Stream Bool -> Stream Bool
&& ((Stream a
mins 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 -> t -> Stream Bool
nextRes Stream a
c Stream Bool
s Stream Bool
s' t
k))
nextRes :: Stream a -> Stream Bool -> Stream Bool -> t -> Stream Bool
nextRes Stream a
c Stream Bool
s Stream Bool
s' t
k = Stream a -> Stream Bool -> Stream Bool -> t -> Stream Bool
res (forall a. Typed a => Int -> Stream a -> Stream a
drop Int
1 Stream a
c) (forall a. Typed a => Int -> Stream a -> Stream a
drop Int
1 Stream Bool
s) (forall a. Typed a => Int -> Stream a -> Stream a
drop Int
1 Stream Bool
s') (t
k forall a. Num a => a -> a -> a
- t
1)
since :: ( Typed a, Integral a ) =>
a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
since :: 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
s1 = forall {t}.
(Num t, Eq t) =>
Stream a -> Stream Bool -> Stream Bool -> t -> Stream Bool
res Stream a
clk Stream Bool
s0 Stream Bool
s1 forall a b. (a -> b) -> a -> b
$ (a
u forall a. Integral a => a -> a -> a
`P.div` a
dist) forall a. Num a => a -> a -> a
+ a
1
where
mins :: Stream a
mins = Stream a
clk forall a. Num a => a -> a -> a
- (forall a. Typed a => a -> Stream a
constant a
u)
maxes :: Stream a
maxes = Stream a
clk forall a. Num a => a -> a -> a
- (forall a. Typed a => a -> Stream a
constant a
l)
res :: Stream a -> Stream Bool -> Stream Bool -> t -> Stream Bool
res Stream a
_ Stream Bool
_ Stream Bool
_ t
0 = Stream Bool
false
res Stream a
c Stream Bool
s Stream Bool
s' t
k =
Stream a
mins forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
<= Stream a
c Stream Bool -> Stream Bool -> Stream Bool
&& ((Stream a
c 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 -> t -> Stream Bool
nextRes Stream a
c Stream Bool
s Stream Bool
s' t
k))
nextRes :: Stream a -> Stream Bool -> Stream Bool -> t -> Stream Bool
nextRes Stream a
c Stream Bool
s Stream Bool
s' t
k = Stream a -> Stream Bool -> Stream Bool -> t -> Stream Bool
res ([a
0] forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream a
c) ([Bool
True] forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream Bool
s) ([Bool
False] forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream Bool
s') (t
k forall a. Num a => a -> a -> a
- t
1)
release :: ( Typed a, Integral a ) =>
a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
release :: forall a.
(Typed a, Integral a) =>
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 forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
> Stream a
clk Stream Bool -> Stream Bool -> Stream Bool
|| Stream a
clk 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
&&
(forall {t}.
(Num t, Eq t) =>
Stream a -> Stream Bool -> Stream Bool -> t -> Stream Bool
res (forall a. Typed a => Int -> Stream a -> Stream a
drop Int
1 Stream a
clk) Stream Bool
s0 (forall a. Typed a => Int -> Stream a -> Stream a
drop Int
1 Stream Bool
s1) forall a b. (a -> b) -> a -> b
$ a
u forall a. Integral a => a -> a -> a
`P.div` a
dist)
where
mins :: Stream a
mins = Stream a
clk forall a. Num a => a -> a -> a
+ (forall a. Typed a => a -> Stream a
constant a
l)
maxes :: Stream a
maxes = Stream a
clk forall a. Num a => a -> a -> a
+ (forall a. Typed a => a -> Stream a
constant a
u)
res :: Stream a -> Stream Bool -> Stream Bool -> t -> Stream Bool
res Stream a
_ Stream Bool
_ Stream Bool
_ t
0 = Stream Bool
true
res Stream a
c Stream Bool
s Stream Bool
s' t
k =
Stream Bool
s Stream Bool -> Stream Bool -> Stream Bool
|| ((Stream a
mins forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
> Stream a
c Stream Bool -> Stream Bool -> Stream Bool
|| Stream a
c 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 -> t -> Stream Bool
nextRes Stream a
c Stream Bool
s Stream Bool
s' t
k)
nextRes :: Stream a -> Stream Bool -> Stream Bool -> t -> Stream Bool
nextRes Stream a
c Stream Bool
s Stream Bool
s' t
k = Stream a -> Stream Bool -> Stream Bool -> t -> Stream Bool
res (forall a. Typed a => Int -> Stream a -> Stream a
drop Int
1 Stream a
c) (forall a. Typed a => Int -> Stream a -> Stream a
drop Int
1 Stream Bool
s) (forall a. Typed a => Int -> Stream a -> Stream a
drop Int
1 Stream Bool
s') (t
k forall a. Num a => a -> a -> a
- t
1)
trigger :: ( Typed a, Integral a ) =>
a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
trigger :: forall a.
(Typed a, Integral a) =>
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 forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
> Stream a
clk Stream Bool -> Stream Bool -> Stream Bool
|| Stream a
clk 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
&&
(forall {t}.
(Num t, Eq t) =>
Stream a -> Stream Bool -> Stream Bool -> t -> Stream Bool
res ([a
0] forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream a
clk) Stream Bool
s0 ([Bool
True] forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream Bool
s1) forall a b. (a -> b) -> a -> b
$ a
u forall a. Integral a => a -> a -> a
`P.div` a
dist)
where
mins :: Stream a
mins = Stream a
clk forall a. Num a => a -> a -> a
- (forall a. Typed a => a -> Stream a
constant a
u)
maxes :: Stream a
maxes = Stream a
clk forall a. Num a => a -> a -> a
- (forall a. Typed a => a -> Stream a
constant a
l)
res :: Stream a -> Stream Bool -> Stream Bool -> t -> Stream Bool
res Stream a
_ Stream Bool
_ Stream Bool
_ t
0 = Stream Bool
true
res Stream a
c Stream Bool
s Stream Bool
s' t
k =
Stream Bool
s Stream Bool -> Stream Bool -> Stream Bool
|| ((Stream a
mins forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
> Stream a
c Stream Bool -> Stream Bool -> Stream Bool
|| Stream a
c 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 -> t -> Stream Bool
nextRes Stream a
c Stream Bool
s Stream Bool
s' t
k)
nextRes :: Stream a -> Stream Bool -> Stream Bool -> t -> Stream Bool
nextRes Stream a
c Stream Bool
s Stream Bool
s' t
k = Stream a -> Stream Bool -> Stream Bool -> t -> Stream Bool
res ([a
0] forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream a
c) ([Bool
False] forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream Bool
s) ([Bool
True] forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream Bool
s') (t
k forall a. Num a => a -> a -> a
- t
1)
matchingUntil :: ( Typed a, Integral a ) =>
a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
matchingUntil :: forall a.
(Typed a, Integral a) =>
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 = forall {t}.
(Num t, Eq t) =>
Stream a -> Stream Bool -> Stream Bool -> t -> Stream Bool
res Stream a
clk Stream Bool
s0 Stream Bool
s1 forall a b. (a -> b) -> a -> b
$ (a
u forall a. Integral a => a -> a -> a
`P.div` a
dist) forall a. Num a => a -> a -> a
+ a
1
where
mins :: Stream a
mins = Stream a
clk forall a. Num a => a -> a -> a
+ (forall a. Typed a => a -> Stream a
constant a
l)
maxes :: Stream a
maxes = Stream a
clk forall a. Num a => a -> a -> a
+ (forall a. Typed a => a -> Stream a
constant a
u)
res :: Stream a -> Stream Bool -> Stream Bool -> t -> Stream Bool
res Stream a
_ Stream Bool
_ Stream Bool
_ t
0 = Stream Bool
false
res Stream a
c Stream Bool
s Stream Bool
s' t
k =
Stream a
c 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 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 -> t -> Stream Bool
nextRes Stream a
c Stream Bool
s Stream Bool
s' t
k)
nextRes :: Stream a -> Stream Bool -> Stream Bool -> t -> Stream Bool
nextRes Stream a
c Stream Bool
s Stream Bool
s' t
k = Stream a -> Stream Bool -> Stream Bool -> t -> Stream Bool
res (forall a. Typed a => Int -> Stream a -> Stream a
drop Int
1 Stream a
c) (forall a. Typed a => Int -> Stream a -> Stream a
drop Int
1 Stream Bool
s) (forall a. Typed a => Int -> Stream a -> Stream a
drop Int
1 Stream Bool
s') (t
k forall a. Num a => a -> a -> a
- t
1)
matchingSince :: ( Typed a, Integral a ) =>
a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
matchingSince :: forall a.
(Typed a, Integral a) =>
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 = 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)
matchingRelease :: ( Typed a, Integral a ) =>
a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
matchingRelease :: forall a.
(Typed a, Integral a) =>
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 = forall {t}.
(Num t, Eq t) =>
Stream a -> Stream Bool -> Stream Bool -> t -> Stream Bool
res Stream a
clk Stream Bool
s0 Stream Bool
s1 forall a b. (a -> b) -> a -> b
$ (a
u forall a. Integral a => a -> a -> a
`P.div` a
dist) forall a. Num a => a -> a -> a
+ a
1
where
mins :: Stream a
mins = Stream a
clk forall a. Num a => a -> a -> a
+ (forall a. Typed a => a -> Stream a
constant a
l)
maxes :: Stream a
maxes = Stream a
clk forall a. Num a => a -> a -> a
+ (forall a. Typed a => a -> Stream a
constant a
u)
res :: Stream a -> Stream Bool -> Stream Bool -> t -> Stream Bool
res Stream a
_ Stream Bool
_ Stream Bool
_ t
0 = Stream Bool
true
res Stream a
c Stream Bool
s Stream Bool
s' t
k =
Stream Bool
s Stream Bool -> Stream Bool -> Stream Bool
|| ((Stream a
mins forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
> Stream a
c Stream Bool -> Stream Bool -> Stream Bool
|| Stream a
c 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 -> t -> Stream Bool
nextRes Stream a
c Stream Bool
s Stream Bool
s' t
k)
nextRes :: Stream a -> Stream Bool -> Stream Bool -> t -> Stream Bool
nextRes Stream a
c Stream Bool
s Stream Bool
s' t
k = Stream a -> Stream Bool -> Stream Bool -> t -> Stream Bool
res (forall a. Typed a => Int -> Stream a -> Stream a
drop Int
1 Stream a
c) (forall a. Typed a => Int -> Stream a -> Stream a
drop Int
1 Stream Bool
s) (forall a. Typed a => Int -> Stream a -> Stream a
drop Int
1 Stream Bool
s') (t
k forall a. Num a => a -> a -> a
- t
1)
matchingTrigger :: ( Typed a, Integral a ) =>
a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
matchingTrigger :: forall a.
(Typed a, Integral a) =>
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 =
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)