    -- |
    -- 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 :: 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 = Stream a -> Stream Bool -> a -> Stream Bool
    forall {t}.
    (Num t, Eq t) =>
    Stream a -> Stream Bool -> t -> 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 -> 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 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 -> 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 (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) (t
    k t -> t -> t
    forall a. Num a => a -> a -> a
    - t
    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 :: 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 = Stream a -> Stream Bool -> a -> Stream Bool
    forall {t}.
    (Num t, Eq t) =>
    Stream a -> Stream Bool -> t -> 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 -> 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 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 -> 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] [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) (t
    k t -> t -> t
    forall a. Num a => a -> a -> a
    - t
    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 :: 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 = Stream a -> Stream Bool -> a -> Stream Bool
    forall {t}.
    (Num t, Eq t) =>
    Stream a -> Stream Bool -> t -> 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 -> 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 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 -> 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 (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) (t
    k t -> t -> t
    forall a. Num a => a -> a -> a
    - t
    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 :: 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 = Stream a -> Stream Bool -> a -> Stream Bool
    forall {t}.
    (Num t, Eq t) =>
    Stream a -> Stream Bool -> t -> 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 -> 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 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 -> 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] [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) (t
    k t -> t -> t
    forall a. Num a => a -> a -> a
    - t
    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 :: 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 = Stream a -> Stream Bool -> Stream Bool -> a -> Stream Bool
    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 (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 -> 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 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 -> 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 (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') (t
    k t -> t -> t
    forall a. Num a => a -> a -> a
    - t
    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 :: 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 = Stream a -> Stream Bool -> Stream Bool -> a -> Stream Bool
    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 (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 -> 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 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 -> 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] [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') (t
    k t -> t -> t
    forall a. Num a => a -> a -> a
    - t
    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 :: 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 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 {t}.
    (Num t, Eq t) =>
    Stream a -> Stream Bool -> Stream Bool -> t -> 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 -> 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 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 -> 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 (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') (t
    k t -> t -> t
    forall a. Num a => a -> a -> a
    - t
    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 :: 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 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 {t}.
    (Num t, Eq t) =>
    Stream a -> Stream Bool -> Stream Bool -> t -> 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 -> 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 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 -> 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] [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') (t
    k t -> t -> t
    forall a. Num a => a -> a -> a
    - t
    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 :: 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 = Stream a -> Stream Bool -> Stream Bool -> a -> Stream Bool
    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 (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 -> 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 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 -> 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 (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') (t
    k t -> t -> t
    forall a. Num a => a -> a -> a
    - t
    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 :: 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 = 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 :: 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 = Stream a -> Stream Bool -> Stream Bool -> a -> Stream Bool
    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 (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 -> 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 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 -> 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 (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') (t
    k t -> t -> t
    forall a. Num a => a -> a -> a
    - t
    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 :: 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 =
      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)