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

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

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

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

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

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

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

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

-- | 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 l u clk dist s0 s1 = since l u clk dist s0 (s0 && 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 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)

-- | 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 l u clk dist s0 s1 =
  Copilot.Library.MTL.trigger l u clk dist s0 (s0 || s1)