Safe Haskell	Safe
Language	Haskell2010

LTL

Description

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

data Machine a b Source #

Constructors

Stop b
Delay (Machine a b)
Ask (a -> Machine a b)

Instances

Functor (Machine a) Source #
Instance details Defined in LTL Methods fmap :: (a0 -> b) -> Machine a a0 -> Machine a b # (<$) :: a0 -> Machine a b -> Machine a a0 #

data Reason a Source #

Constructors

HitBottom String
Rejected a
BothFailed (Reason a) (Reason a)
LeftFailed (Reason a)
RightFailed (Reason a)

Instances

Show a => Show (Reason a) Source #
Instance details Defined in LTL Methods showsPrec :: Int -> Reason a -> ShowS # show :: Reason a -> String # showList :: [Reason a] -> ShowS #

data Result a Source #

Constructors

Failure (Reason a)
Success

Instances

Show a => Show (Result a) Source #
Instance details Defined in LTL Methods showsPrec :: Int -> Result a -> ShowS # show :: Result a -> String # showList :: [Result a] -> ShowS #