module Logic.TemporalLogic.Macro where

import           Types

import           Macro.MetaMacro
import           Macro.Text

import           Logic.AbstractLogic.Macro

-- | The 'next' temporal logic operator
next :: Note -> Note
next = mappend $ comm0 "bigcirc"

-- | The 'until' temporal logic operator
until :: Note -> Note -> Note
until = binop $ commS "," <> mathcal "U" <> commS ","

-- | Infix version of the 'until' temporal logic operator
(.∪) :: Note -> Note -> Note
(.∪) = until

-- | Eventually
evnt :: Note -> Note
evnt = mappend $ comm0 "Diamond"

-- | Always
alws :: Note -> Note
alws = mappend $ comm0 "Box"

-- | Satisfies
  Word
          -> Note -- Position
  Formula
          -> Note
satis w p = lent $ cs [w, p]

-- | Language of a formula
  Formula
           -> Note
languageOf = (!:) "L"

 | The 'next' temporal logic operator
 | The 'until' temporal logic operator
 | Infix version of the 'until' temporal logic operator
 | Eventually
 | Always
 | Satisfies
 Position
 | Language of a formula
module Logic.TemporalLogic.Macro where

import           Types

import           Macro.MetaMacro
import           Macro.Text

import           Logic.AbstractLogic.Macro

next :: Note -> Note
next = mappend $ comm0 "bigcirc"

until :: Note -> Note -> Note
until = binop $ commS "," <> mathcal "U" <> commS ","

(.∪) :: Note -> Note -> Note
(.∪) = until

evnt :: Note -> Note
evnt = mappend $ comm0 "Diamond"

alws :: Note -> Note
alws = mappend $ comm0 "Box"

  Word
  Formula
          -> Note
satis w p = lent $ cs [w, p]

  Formula
           -> Note
languageOf = (!:) "L"
