{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE LambdaCase #-}
module LTL
( LTL
, Machine(..)
, Reason(..)
, Result
, run
, neg
, top
, bottom
, accept
, reject
, LTL.and
, LTL.or
, next
, LTL.until
, weakUntil
, release
, strongRelease
, implies
, eventually
, always
, truth
, test
, is
, eq
, showResult
) where
import Control.DeepSeq
import Data.Function (fix)
import Data.List (foldl')
import GHC.Generics
import Prelude hiding (and, or, until)
newtype Machine a b = Machine { step :: a -> Either (Machine a b) b }
instance Functor (Machine a) where
fmap f (Machine k) = Machine $ either (Left . fmap f) (Right . f) . k
run :: Machine a b -> [a] -> Either (Machine a b) b
run = foldl' (either step (const . Right)) . Left
{-# INLINE run #-}
data Reason a
= HitBottom String
| Rejected a
| BothFailed (Reason a) (Reason a)
| LeftFailed (Reason a)
| RightFailed (Reason a)
deriving (Show, Generic, NFData, Functor)
type Result a = Maybe (Reason a)
type LTL a = Machine a (Result a)
top :: LTL a
top = stop Nothing
{-# INLINE top #-}
bottom :: String -> LTL a
bottom = stop . Just . HitBottom
{-# INLINE bottom #-}
neg :: LTL a -> LTL a
neg = fmap invert
{-# INLINE neg #-}
and :: LTL a -> LTL a -> LTL a
and (Machine f) g = Machine $ \a -> case f a of
Right (Just e) -> Right (Just (LeftFailed e))
Right Nothing -> step g a
Left f' -> case step g a of
Right (Just e) -> Right (Just (RightFailed e))
Right Nothing -> Left f'
Left g' -> Left $! f' `and` g'
andNext :: LTL a -> LTL a -> LTL a
andNext (Machine f) g = Machine $ \a -> case f a of
Right (Just e) -> Right (Just (LeftFailed e))
Right Nothing -> Left g
Left f' -> Left $! f' `and` g
{-# INLINE andNext #-}
or :: LTL a -> LTL a -> LTL a
or (Machine f) g = Machine $ \a -> case f a of
Right Nothing -> Right Nothing
Right (Just e1) -> case step g a of
Right (Just e2) -> Right (Just (BothFailed e1 e2))
g' -> g'
Left f' -> case step g a of
Right Nothing -> Right Nothing
Right (Just _) -> Left f'
Left g' -> Left $! f' `or` g'
orNext :: LTL a -> LTL a -> LTL a
orNext (Machine f) g = Machine $ \a -> case f a of
Right Nothing -> Right Nothing
Right (Just _) -> Left g
Left f' -> Left $! f' `or` g
{-# INLINE orNext #-}
invert :: Result a -> Result a
invert = \case
Nothing -> Just (HitBottom "neg")
Just _ -> Nothing
{-# INLINE invert #-}
stop :: Result a -> LTL a
stop = Machine . const . Right
{-# INLINE stop #-}
accept :: (a -> LTL a) -> LTL a
accept f = Machine $ \a -> step (f a) a
{-# INLINE accept #-}
reject :: (a -> LTL a) -> LTL a
reject = neg . accept
{-# INLINE reject #-}
next :: LTL a -> LTL a
next = Machine . const . Left
{-# INLINE next #-}
until :: LTL a -> LTL a -> LTL a
until p q = fix $ or q . andNext p
{-# INLINE until #-}
weakUntil :: LTL a -> LTL a -> LTL a
weakUntil p q = (p `until` q) `or` always p
{-# INLINE weakUntil #-}
release :: LTL a -> LTL a -> LTL a
release p q = fix $ and q . orNext p
{-# INLINE release #-}
strongRelease :: LTL a -> LTL a -> LTL a
strongRelease p q = (p `release` q) `and` eventually p
{-# INLINE strongRelease #-}
implies :: LTL a -> LTL a -> LTL a
implies = or . neg
{-# 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 True = top
truth False = bottom "truth"
{-# INLINE truth #-}
is :: (a -> Bool) -> LTL a
is = accept . (truth .)
{-# INLINE is #-}
test :: (a -> Bool) -> LTL a
test = is
{-# INLINE test #-}
eq :: Eq a => a -> LTL a
eq = is . (==)
{-# INLINE eq #-}
showResult :: Show a => Either (LTL a) (Result a) -> String
showResult (Left _) = "<need input>"
showResult (Right b) = show b
{-# INLINE showResult #-}