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