-- | This module provides helpers for writing common LTL expressions.
module Cooked.Ltl.Combinators
  ( anyOf,
    allOf,
    anyOf',
    allOf',
    delay,
    delay',
    eventually,
    eventually',
    always,
    always',
  )
where

import Cooked.Ltl (Ltl (..))

-- | Same as `anyOf'`, but first wraps the elements in the input list in atomic
-- formulas.
anyOf :: [a] -> Ltl a
anyOf :: forall a. [a] -> Ltl a
anyOf = [Ltl a] -> Ltl a
forall a. [Ltl a] -> Ltl a
anyOf' ([Ltl a] -> Ltl a) -> ([a] -> [Ltl a]) -> [a] -> Ltl a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Ltl a) -> [a] -> [Ltl a]
forall a b. (a -> b) -> [a] -> [b]
map a -> Ltl a
forall a. a -> Ltl a
LtlAtom

-- | Produces an Ltl formula which consists of the disjunction of all the
-- formulas in the input list.
anyOf' :: [Ltl a] -> Ltl a
anyOf' :: forall a. [Ltl a] -> Ltl a
anyOf' [] = Ltl a
forall a. Ltl a
LtlFalsity
anyOf' [Ltl a]
xs = (Ltl a -> Ltl a -> Ltl a) -> [Ltl a] -> Ltl a
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Ltl a -> Ltl a -> Ltl a
forall a. Ltl a -> Ltl a -> Ltl a
LtlOr [Ltl a]
xs

-- | Same as `allOf'`, but first wraps the elements in the input list in atomic
-- formulas.
allOf :: [a] -> Ltl a
allOf :: forall a. [a] -> Ltl a
allOf = [Ltl a] -> Ltl a
forall a. [Ltl a] -> Ltl a
allOf' ([Ltl a] -> Ltl a) -> ([a] -> [Ltl a]) -> [a] -> Ltl a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Ltl a) -> [a] -> [Ltl a]
forall a b. (a -> b) -> [a] -> [b]
map a -> Ltl a
forall a. a -> Ltl a
LtlAtom

-- | Produces an Ltl formula which consists of the conjunction of all the
-- formulas in the input list.
allOf' :: [Ltl a] -> Ltl a
allOf' :: forall a. [Ltl a] -> Ltl a
allOf' [] = Ltl a
forall a. Ltl a
LtlTruth
allOf' [Ltl a]
xs = (Ltl a -> Ltl a -> Ltl a) -> [Ltl a] -> Ltl a
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Ltl a -> Ltl a -> Ltl a
forall a. Ltl a -> Ltl a -> Ltl a
LtlAnd [Ltl a]
xs

-- | Same as `delay'`, but first wraps the elements in the input list in atomic
-- formulas.
delay :: Integer -> a -> Ltl a
delay :: forall a. Integer -> a -> Ltl a
delay Integer
n = Integer -> Ltl a -> Ltl a
forall a. Integer -> Ltl a -> Ltl a
delay' Integer
n (Ltl a -> Ltl a) -> (a -> Ltl a) -> a -> Ltl a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Ltl a
forall a. a -> Ltl a
LtlAtom

-- | Produces an Ltl formula which consists of the delay of the input formula by
-- @n@ time steps, if @n > 0@. Otherwise, leaves the formula unchanged.
delay' :: Integer -> Ltl a -> Ltl a
delay' :: forall a. Integer -> Ltl a -> Ltl a
delay' Integer
n | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
0 = Ltl a -> Ltl a
forall a. a -> a
id
delay' Integer
n = Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
LtlNext (Ltl a -> Ltl a) -> (Ltl a -> Ltl a) -> Ltl a -> Ltl a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Ltl a -> Ltl a
forall a. Integer -> Ltl a -> Ltl a
delay' (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)

-- | Same as `eventually'`, but first wraps the elements in the input list in
-- atomic formulas.
eventually :: a -> Ltl a
eventually :: forall a. a -> Ltl a
eventually = Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
eventually' (Ltl a -> Ltl a) -> (a -> Ltl a) -> a -> Ltl a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Ltl a
forall a. a -> Ltl a
LtlAtom

-- | Produces an Ltl formula which consists the input formula eventually holds
eventually' :: Ltl a -> Ltl a
eventually' :: forall a. Ltl a -> Ltl a
eventually' = Ltl a -> Ltl a -> Ltl a
forall a. Ltl a -> Ltl a -> Ltl a
LtlUntil Ltl a
forall a. Ltl a
LtlTruth

-- |  Same as `always'`, but first wraps the elements in the input list in
-- atomic formulas.
always :: a -> Ltl a
always :: forall a. a -> Ltl a
always = Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
always' (Ltl a -> Ltl a) -> (a -> Ltl a) -> a -> Ltl a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Ltl a
forall a. a -> Ltl a
LtlAtom

-- | Produces an Ltl formula which ensures the input formula always holds
always' :: Ltl a -> Ltl a
always' :: forall a. Ltl a -> Ltl a
always' = Ltl a -> Ltl a -> Ltl a
forall a. Ltl a -> Ltl a -> Ltl a
LtlRelease Ltl a
forall a. Ltl a
LtlFalsity