{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE LambdaCase #-}
module LTL
( LTL
, Machine(..)
, Reason(..)
, Result(..)
, step
, run
, neg
, top
, bottom
, accept
, reject
, LTL.and
, LTL.or
, next
, LTL.until
, weakUntil
, release
, strongRelease
, implies
, eventually
, always
, truth
, test
, eq
) where
import Data.List (foldl')
import Prelude hiding (and, or, until)
data Machine a b
= Stop b
| Delay (Machine a b)
| Ask (a -> Machine a b)
deriving Functor
step :: Machine a b -> a -> Machine a b
step m@(Stop _) _ = m
step (Delay m) _ = m
step (Ask f) x = step (f x) x
{-# INLINE step #-}
run :: Machine a b -> [a] -> Machine a b
run = foldl' step
{-# INLINE run #-}
data Reason a
= HitBottom String
| Rejected a
| BothFailed (Reason a) (Reason a)
| LeftFailed (Reason a)
| RightFailed (Reason a)
deriving Show
data Result a
= Failure (Reason a)
| Success
deriving Show
type LTL a = Machine a (Result a)
combine :: LTL a -> LTL a -> LTL a
combine (Stop (Failure e)) _ = Stop (Failure (LeftFailed e))
combine _ (Stop (Failure e)) = Stop (Failure (RightFailed e))
combine (Delay f') (Delay g') = Delay (combine f' g')
combine (Ask f') (Ask g') = Ask (\a -> combine (f' a) (g' a))
combine f (Ask g') = Ask (\a -> combine f (g' a))
combine (Ask f') g = Ask (\a -> combine (f' a) g)
combine f' (Stop Success) = f'
combine (Stop Success) g' = g'
select :: LTL a -> LTL a -> LTL a
select (Stop (Failure e1))
(Stop (Failure e2)) = Stop (Failure (BothFailed e1 e2))
select (Stop Success) _ = Stop Success
select _ (Stop Success) = Stop Success
select (Delay f') (Delay g') = Delay (select f' g')
select (Ask f') (Ask g') = Ask (\a -> select (f' a) (g' a))
select f (Ask g') = Ask (\a -> select f (g' a))
select (Ask f') g = Ask (\a -> select (f' a) g)
select (Stop (Failure _)) g' = g'
select f' (Stop (Failure _)) = f'
neg :: LTL a -> LTL a
neg = fmap $ \case
Success -> Failure (HitBottom "neg")
Failure _ -> Success
{-# INLINE neg #-}
top :: LTL a
top = Stop Success
{-# INLINE top #-}
bottom :: String -> LTL a
bottom e = Stop (Failure (HitBottom e))
{-# INLINE bottom #-}
accept :: (a -> LTL a) -> LTL a
accept = Ask
{-# INLINE accept #-}
reject :: (a -> LTL a) -> LTL a
reject f = Ask (neg . f)
{-# INLINE reject #-}
and :: LTL a -> LTL a -> LTL a
and !p !q = combine p q
{-# INLINE and #-}
or :: LTL a -> LTL a -> LTL a
or !p = select p
{-# INLINE or #-}
next :: LTL a -> LTL a
next = Delay
{-# INLINE next #-}
until :: LTL a -> LTL a -> LTL a
until p q = go
where
go = or q (and p (next go))
{-# INLINE go #-}
{-# INLINE until #-}
weakUntil :: LTL a -> LTL a -> LTL a
weakUntil p q = (p `until` q) `and` always p
{-# INLINE weakUntil #-}
strongRelease :: LTL a -> LTL a -> LTL a
strongRelease p q = q `until` (p `or` q)
{-# INLINE strongRelease #-}
release :: LTL a -> LTL a -> LTL a
release p q = go
where
go = q `and` (p `or` (next go))
{-# INLINE go #-}
{-# INLINE release #-}
implies :: LTL a -> LTL a -> LTL a
implies p = or (neg p)
{-# INLINE implies #-}
eventually :: LTL a -> LTL a
eventually = until top
{-# INLINE eventually #-}
always :: LTL a -> LTL a
always = release (bottom "always")
{-# INLINE always #-}
truth :: Bool -> LTL a
truth b = if b then top else bottom "truth"
{-# INLINE truth #-}
test :: (a -> Bool) -> LTL a
test f = accept $ truth . f
{-# INLINE test #-}
eq :: Eq a => a -> LTL a
eq n = accept $ truth . (== n)
{-# INLINE eq #-}