LTL

This formulation of LTL is in positive normal form by construction, and trivially dualizable. This choice was driven by the following Coq formalization, showing that all the laws for LTL hold under a denotation from this structure into Coq's logic, over all finite lists:

https://github.com/jwiegley/constructive-ltl/blob/master/src/LTL.v#L69

Documentation

type LTL a = Machine a (Result a)

data Machine a b

Constructors

Stop b

Delay (Machine a b)

Ask (a -> Machine a b)

Instances

Functor (Machine a)

Defined in LTL

Methods

fmap :: (a0 -> b) -> Machine a a0 -> Machine a b

(<$) :: a0 -> Machine a b -> Machine a a0

data Reason a

Constructors

HitBottom String

Rejected a

BothFailed (Reason a) (Reason a)

LeftFailed (Reason a)

RightFailed (Reason a)

Instances

Show a => Show (Reason a)

Defined in LTL

Methods

showsPrec :: Int -> Reason a -> ShowS

show :: Reason a -> String

showList :: [Reason a] -> ShowS

Generic (Reason a)

Defined in LTL

Associated Types

type Rep (Reason a) :: Type -> Type

Methods

from :: Reason a -> Rep (Reason a) x

to :: Rep (Reason a) x -> Reason a

NFData a => NFData (Reason a)

Defined in LTL

Methods

rnf :: Reason a -> ()

type Rep (Reason a)

Defined in LTL

type Rep (Reason a) = D1 (MetaData "Reason" "LTL" "simple-ltl-1.0.0-Fb9CmHs9o9MCVdA6TpcRen" False) ((C1 (MetaCons "HitBottom" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :+: C1 (MetaCons "Rejected" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a))) :+: (C1 (MetaCons "BothFailed" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Reason a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Reason a))) :+: (C1 (MetaCons "LeftFailed" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Reason a))) :+: C1 (MetaCons "RightFailed" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Reason a))))))

data Result a

Constructors

Failure (Reason a)

Success

Instances

Show a => Show (Result a)

Defined in LTL

Methods

showsPrec :: Int -> Result a -> ShowS

show :: Result a -> String

showList :: [Result a] -> ShowS

Generic (Result a)

Defined in LTL

Associated Types

type Rep (Result a) :: Type -> Type

Methods

from :: Result a -> Rep (Result a) x

to :: Rep (Result a) x -> Result a

NFData a => NFData (Result a)

Defined in LTL

Methods

rnf :: Result a -> ()

type Rep (Result a)

Defined in LTL

type Rep (Result a) = D1 (MetaData "Result" "LTL" "simple-ltl-1.0.0-Fb9CmHs9o9MCVdA6TpcRen" False) (C1 (MetaCons "Failure" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Reason a))) :+: C1 (MetaCons "Success" PrefixI False) (U1 :: Type -> Type))

step :: Machine a b -> a -> Machine a b

run :: Machine a b -> [a] -> Machine a b

neg :: LTL a -> LTL a

top :: LTL a

bottom :: String -> LTL a

accept :: (a -> LTL a) -> LTL a

reject :: (a -> LTL a) -> LTL a

and :: LTL a -> LTL a -> LTL a

or :: LTL a -> LTL a -> LTL a

next :: LTL a -> LTL a

until :: LTL a -> LTL a -> LTL a

weakUntil :: LTL a -> LTL a -> LTL a

release :: LTL a -> LTL a -> LTL a

strongRelease :: LTL a -> LTL a -> LTL a

implies :: LTL a -> LTL a -> LTL a

eventually :: LTL a -> LTL a

always :: LTL a -> LTL a

truth :: Bool -> LTL a

test :: (a -> Bool) -> LTL a

eq :: Eq a => a -> LTL a