{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE StandaloneDeriving #-}
module Test.StateMachine.Logic
( Logic(..)
, LogicPredicate(..)
, dual
, strongNeg
, Counterexample(..)
, Value(..)
, boolean
, logic
, evalLogicPredicate
, gatherAnnotations
, (.==)
, (./=)
, (.<)
, (.<=)
, (.>)
, (.>=)
, member
, notMember
, (.//)
, (.&&)
, (.||)
, (.=>)
, forAll
, exists
)
where
import Prelude
data Logic
= Bot
| Top
| Logic :&& Logic
| Logic :|| Logic
| Logic :=> Logic
| Not Logic
| LogicPredicate LogicPredicate
| forall a. Show a => Forall [a] (a -> Logic)
| forall a. Show a => Exists [a] (a -> Logic)
| Boolean Bool
| Annotate String Logic
data LogicPredicate
= forall a. (Eq a, Show a) => a :== a
| forall a. (Eq a, Show a) => a :/= a
| forall a. (Ord a, Show a) => a :< a
| forall a. (Ord a, Show a) => a :<= a
| forall a. (Ord a, Show a) => a :> a
| forall a. (Ord a, Show a) => a :>= a
| forall t a. (Foldable t, Eq a, Show a, Show (t a)) => Member a (t a)
| forall t a. (Foldable t, Eq a, Show a, Show (t a)) => NotMember a (t a)
deriving stock instance Show LogicPredicate
dual :: LogicPredicate -> LogicPredicate
dual :: LogicPredicate -> LogicPredicate
dual LogicPredicate
p = case LogicPredicate
p of
a
x :== a
y -> a
x a -> a -> LogicPredicate
forall a. (Eq a, Show a) => a -> a -> LogicPredicate
:/= a
y
a
x :/= a
y -> a
x a -> a -> LogicPredicate
forall a. (Eq a, Show a) => a -> a -> LogicPredicate
:== a
y
a
x :< a
y -> a
x a -> a -> LogicPredicate
forall a. (Ord a, Show a) => a -> a -> LogicPredicate
:>= a
y
a
x :<= a
y -> a
x a -> a -> LogicPredicate
forall a. (Ord a, Show a) => a -> a -> LogicPredicate
:> a
y
a
x :> a
y -> a
x a -> a -> LogicPredicate
forall a. (Ord a, Show a) => a -> a -> LogicPredicate
:<= a
y
a
x :>= a
y -> a
x a -> a -> LogicPredicate
forall a. (Ord a, Show a) => a -> a -> LogicPredicate
:< a
y
a
x `Member` t a
xs -> a
x a -> t a -> LogicPredicate
forall (t :: * -> *) a.
(Foldable t, Eq a, Show a, Show (t a)) =>
a -> t a -> LogicPredicate
`NotMember` t a
xs
a
x `NotMember` t a
xs -> a
x a -> t a -> LogicPredicate
forall (t :: * -> *) a.
(Foldable t, Eq a, Show a, Show (t a)) =>
a -> t a -> LogicPredicate
`Member` t a
xs
strongNeg :: Logic -> Logic
strongNeg :: Logic -> Logic
strongNeg Logic
l0 = case Logic
l0 of
Logic
Bot -> Logic
Top
Logic
Top -> Logic
Bot
Logic
l :&& Logic
r -> Logic -> Logic
strongNeg Logic
l Logic -> Logic -> Logic
:|| Logic -> Logic
strongNeg Logic
r
Logic
l :|| Logic
r -> Logic -> Logic
strongNeg Logic
l Logic -> Logic -> Logic
:&& Logic -> Logic
strongNeg Logic
r
Logic
l :=> Logic
r -> Logic
l Logic -> Logic -> Logic
:&& Logic -> Logic
strongNeg Logic
r
Not Logic
l -> Logic
l
LogicPredicate LogicPredicate
p -> LogicPredicate -> Logic
LogicPredicate (LogicPredicate -> LogicPredicate
dual LogicPredicate
p)
Forall [a]
xs a -> Logic
p -> [a] -> (a -> Logic) -> Logic
forall a. Show a => [a] -> (a -> Logic) -> Logic
Exists [a]
xs (Logic -> Logic
strongNeg (Logic -> Logic) -> (a -> Logic) -> a -> Logic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Logic
p)
Exists [a]
xs a -> Logic
p -> [a] -> (a -> Logic) -> Logic
forall a. Show a => [a] -> (a -> Logic) -> Logic
Forall [a]
xs (Logic -> Logic
strongNeg (Logic -> Logic) -> (a -> Logic) -> a -> Logic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Logic
p)
Boolean Bool
b -> Bool -> Logic
Boolean (Bool -> Bool
not Bool
b)
Annotate String
s Logic
l -> String -> Logic -> Logic
Annotate String
s (Logic -> Logic
strongNeg Logic
l)
data Counterexample
= BotC
| Fst Counterexample
| Snd Counterexample
| EitherC Counterexample Counterexample
| ImpliesC Counterexample
| NotC Counterexample
| PredicateC LogicPredicate
| forall a. Show a => ForallC a Counterexample
| forall a. Show a => ExistsC [a] [Counterexample]
| BooleanC
| AnnotateC String Counterexample
deriving stock instance Show Counterexample
data Value
= VFalse Counterexample
| VTrue
deriving stock Int -> Value -> ShowS
[Value] -> ShowS
Value -> String
(Int -> Value -> ShowS)
-> (Value -> String) -> ([Value] -> ShowS) -> Show Value
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Value -> ShowS
showsPrec :: Int -> Value -> ShowS
$cshow :: Value -> String
show :: Value -> String
$cshowList :: [Value] -> ShowS
showList :: [Value] -> ShowS
Show
boolean :: Logic -> Bool
boolean :: Logic -> Bool
boolean Logic
l = case Logic -> Value
logic Logic
l of
VFalse Counterexample
_ -> Bool
False
Value
VTrue -> Bool
True
logic :: Logic -> Value
logic :: Logic -> Value
logic Logic
Bot = Counterexample -> Value
VFalse Counterexample
BotC
logic Logic
Top = Value
VTrue
logic (Logic
l :&& Logic
r) = case Logic -> Value
logic Logic
l of
VFalse Counterexample
ce -> Counterexample -> Value
VFalse (Counterexample -> Counterexample
Fst Counterexample
ce)
Value
VTrue -> case Logic -> Value
logic Logic
r of
VFalse Counterexample
ce' -> Counterexample -> Value
VFalse (Counterexample -> Counterexample
Snd Counterexample
ce')
Value
VTrue -> Value
VTrue
logic (Logic
l :|| Logic
r) = case Logic -> Value
logic Logic
l of
Value
VTrue -> Value
VTrue
VFalse Counterexample
ce -> case Logic -> Value
logic Logic
r of
Value
VTrue -> Value
VTrue
VFalse Counterexample
ce' -> Counterexample -> Value
VFalse (Counterexample -> Counterexample -> Counterexample
EitherC Counterexample
ce Counterexample
ce')
logic (Logic
l :=> Logic
r) = case Logic -> Value
logic Logic
l of
VFalse Counterexample
_ -> Value
VTrue
Value
VTrue -> case Logic -> Value
logic Logic
r of
Value
VTrue -> Value
VTrue
VFalse Counterexample
ce -> Counterexample -> Value
VFalse (Counterexample -> Counterexample
ImpliesC Counterexample
ce)
logic (Not Logic
l) = case Logic -> Value
logic (Logic -> Logic
strongNeg Logic
l) of
Value
VTrue -> Value
VTrue
VFalse Counterexample
ce -> Counterexample -> Value
VFalse (Counterexample -> Counterexample
NotC Counterexample
ce)
logic (LogicPredicate LogicPredicate
p) = LogicPredicate -> Value
evalLogicPredicate LogicPredicate
p
logic (Forall [a]
xs0 a -> Logic
p) = [a] -> Value
go [a]
xs0
where
go :: [a] -> Value
go [] = Value
VTrue
go (a
x : [a]
xs) = case Logic -> Value
logic (a -> Logic
p a
x) of
Value
VTrue -> [a] -> Value
go [a]
xs
VFalse Counterexample
ce -> Counterexample -> Value
VFalse (a -> Counterexample -> Counterexample
forall a. Show a => a -> Counterexample -> Counterexample
ForallC a
x Counterexample
ce)
logic (Exists [a]
xs0 a -> Logic
p) = [a] -> [Counterexample] -> Value
go [a]
xs0 []
where
go :: [a] -> [Counterexample] -> Value
go [] [Counterexample]
ces = Counterexample -> Value
VFalse ([a] -> [Counterexample] -> Counterexample
forall a. Show a => [a] -> [Counterexample] -> Counterexample
ExistsC [a]
xs0 ([Counterexample] -> [Counterexample]
forall a. [a] -> [a]
reverse [Counterexample]
ces))
go (a
x : [a]
xs) [Counterexample]
ces = case Logic -> Value
logic (a -> Logic
p a
x) of
Value
VTrue -> Value
VTrue
VFalse Counterexample
ce -> [a] -> [Counterexample] -> Value
go [a]
xs (Counterexample
ce Counterexample -> [Counterexample] -> [Counterexample]
forall a. a -> [a] -> [a]
: [Counterexample]
ces)
logic (Boolean Bool
b) = if Bool
b then Value
VTrue else Counterexample -> Value
VFalse Counterexample
BooleanC
logic (Annotate String
s Logic
l) = case Logic -> Value
logic Logic
l of
Value
VTrue -> Value
VTrue
VFalse Counterexample
ce -> Counterexample -> Value
VFalse (String -> Counterexample -> Counterexample
AnnotateC String
s Counterexample
ce)
evalLogicPredicate :: LogicPredicate -> Value
evalLogicPredicate :: LogicPredicate -> Value
evalLogicPredicate LogicPredicate
p0 = let b :: Bool -> Value
b = LogicPredicate -> Bool -> Value
go LogicPredicate
p0 in case LogicPredicate
p0 of
a
x :== a
y -> Bool -> Value
b (a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y)
a
x :/= a
y -> Bool -> Value
b (a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
y)
a
x :< a
y -> Bool -> Value
b (a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
y)
a
x :<= a
y -> Bool -> Value
b (a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
y)
a
x :> a
y -> Bool -> Value
b (a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
y)
a
x :>= a
y -> Bool -> Value
b (a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
y)
a
x `Member` t a
xs -> Bool -> Value
b (a
x a -> t a -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
xs)
a
x `NotMember` t a
xs -> Bool -> Value
b (a
x a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` t a
xs)
where
go :: LogicPredicate -> Bool -> Value
go :: LogicPredicate -> Bool -> Value
go LogicPredicate
_ Bool
True = Value
VTrue
go LogicPredicate
p Bool
False = Counterexample -> Value
VFalse (LogicPredicate -> Counterexample
PredicateC (LogicPredicate -> LogicPredicate
dual LogicPredicate
p))
gatherAnnotations :: Logic -> [String]
gatherAnnotations :: Logic -> [String]
gatherAnnotations = [String] -> Logic -> [String]
go []
where
go :: [String] -> Logic -> [String]
go [String]
_acc Logic
Bot = []
go [String]
acc Logic
Top = [String]
acc
go [String]
acc (Logic
l :&& Logic
r) | Logic -> Bool
boolean Logic
l Bool -> Bool -> Bool
&& Logic -> Bool
boolean Logic
r = [String] -> Logic -> [String]
go ([String] -> Logic -> [String]
go [String]
acc Logic
l) Logic
r
| Bool
otherwise = [String]
acc
go [String]
acc (Logic
l :|| Logic
r) | Logic -> Bool
boolean Logic
l = [String] -> Logic -> [String]
go [String]
acc Logic
l
| Logic -> Bool
boolean Logic
r = [String] -> Logic -> [String]
go [String]
acc Logic
r
| Bool
otherwise = [String]
acc
go [String]
acc (Logic
l :=> Logic
r) | Logic -> Bool
boolean (Logic
l Logic -> Logic -> Logic
:=> Logic
r) = [String] -> Logic -> [String]
go ([String] -> Logic -> [String]
go [String]
acc Logic
l) Logic
r
| Bool
otherwise = [String]
acc
go [String]
acc (Not Logic
l) | Bool -> Bool
not (Logic -> Bool
boolean Logic
l) = [String] -> Logic -> [String]
go [String]
acc Logic
l
| Bool
otherwise = [String]
acc
go [String]
acc (LogicPredicate LogicPredicate
_p) = [String]
acc
go [String]
acc (Forall [a]
xs a -> Logic
p)
| Logic -> Bool
boolean ([a] -> (a -> Logic) -> Logic
forall a. Show a => [a] -> (a -> Logic) -> Logic
Forall [a]
xs a -> Logic
p) = [String]
acc [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [String] -> Logic -> [String]
go [] (a -> Logic
p a
x)
| a
x <- [a]
xs, Logic -> Bool
boolean (a -> Logic
p a
x)
]
| Bool
otherwise = [String]
acc
go [String]
acc (Exists [a]
xs a -> Logic
p)
| Logic -> Bool
boolean ([a] -> (a -> Logic) -> Logic
forall a. Show a => [a] -> (a -> Logic) -> Logic
Exists [a]
xs a -> Logic
p) = [String]
acc [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Int -> [[String]] -> [[String]]
forall a. Int -> [a] -> [a]
take Int
1 [ [String] -> Logic -> [String]
go [] (a -> Logic
p a
x)
| a
x <- [a]
xs, Logic -> Bool
boolean (a -> Logic
p a
x)
])
| Bool
otherwise = [String]
acc
go [String]
acc (Boolean Bool
_b) = [String]
acc
go [String]
acc (Annotate String
s Logic
l) = [String] -> Logic -> [String]
go ([String]
acc [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
s]) Logic
l
infix 5 .==
infix 5 ./=
infix 5 .<
infix 5 .<=
infix 5 .>
infix 5 .>=
infix 8 `member`
infix 8 `notMember`
infixl 4 .//
infixr 3 .&&
infixr 2 .||
infixr 1 .=>
(.==) :: (Eq a, Show a) => a -> a -> Logic
a
x .== :: forall a. (Eq a, Show a) => a -> a -> Logic
.== a
y = LogicPredicate -> Logic
LogicPredicate (a
x a -> a -> LogicPredicate
forall a. (Eq a, Show a) => a -> a -> LogicPredicate
:== a
y)
(./=) :: (Eq a, Show a) => a -> a -> Logic
a
x ./= :: forall a. (Eq a, Show a) => a -> a -> Logic
./= a
y = LogicPredicate -> Logic
LogicPredicate (a
x a -> a -> LogicPredicate
forall a. (Eq a, Show a) => a -> a -> LogicPredicate
:/= a
y)
(.<) :: (Ord a, Show a) => a -> a -> Logic
a
x .< :: forall a. (Ord a, Show a) => a -> a -> Logic
.< a
y = LogicPredicate -> Logic
LogicPredicate (a
x a -> a -> LogicPredicate
forall a. (Ord a, Show a) => a -> a -> LogicPredicate
:< a
y)
(.<=) :: (Ord a, Show a) => a -> a -> Logic
a
x .<= :: forall a. (Ord a, Show a) => a -> a -> Logic
.<= a
y = LogicPredicate -> Logic
LogicPredicate (a
x a -> a -> LogicPredicate
forall a. (Ord a, Show a) => a -> a -> LogicPredicate
:<= a
y)
(.>) :: (Ord a, Show a) => a -> a -> Logic
a
x .> :: forall a. (Ord a, Show a) => a -> a -> Logic
.> a
y = LogicPredicate -> Logic
LogicPredicate (a
x a -> a -> LogicPredicate
forall a. (Ord a, Show a) => a -> a -> LogicPredicate
:> a
y)
(.>=) :: (Ord a, Show a) => a -> a -> Logic
a
x .>= :: forall a. (Ord a, Show a) => a -> a -> Logic
.>= a
y = LogicPredicate -> Logic
LogicPredicate (a
x a -> a -> LogicPredicate
forall a. (Ord a, Show a) => a -> a -> LogicPredicate
:>= a
y)
member :: (Foldable t, Eq a, Show a, Show (t a)) => a -> t a -> Logic
member :: forall (t :: * -> *) a.
(Foldable t, Eq a, Show a, Show (t a)) =>
a -> t a -> Logic
member a
x t a
xs = LogicPredicate -> Logic
LogicPredicate (a -> t a -> LogicPredicate
forall (t :: * -> *) a.
(Foldable t, Eq a, Show a, Show (t a)) =>
a -> t a -> LogicPredicate
Member a
x t a
xs)
notMember :: (Foldable t, Eq a, Show a, Show (t a)) => a -> t a -> Logic
notMember :: forall (t :: * -> *) a.
(Foldable t, Eq a, Show a, Show (t a)) =>
a -> t a -> Logic
notMember a
x t a
xs = LogicPredicate -> Logic
LogicPredicate (a -> t a -> LogicPredicate
forall (t :: * -> *) a.
(Foldable t, Eq a, Show a, Show (t a)) =>
a -> t a -> LogicPredicate
NotMember a
x t a
xs)
(.//) :: Logic -> String -> Logic
Logic
l .// :: Logic -> String -> Logic
.// String
s = String -> Logic -> Logic
Annotate String
s Logic
l
(.&&) :: Logic -> Logic -> Logic
.&& :: Logic -> Logic -> Logic
(.&&) = Logic -> Logic -> Logic
(:&&)
(.||) :: Logic -> Logic -> Logic
.|| :: Logic -> Logic -> Logic
(.||) = Logic -> Logic -> Logic
(:||)
(.=>) :: Logic -> Logic -> Logic
.=> :: Logic -> Logic -> Logic
(.=>) = Logic -> Logic -> Logic
(:=>)
forAll :: Show a => [a] -> (a -> Logic) -> Logic
forAll :: forall a. Show a => [a] -> (a -> Logic) -> Logic
forAll = [a] -> (a -> Logic) -> Logic
forall a. Show a => [a] -> (a -> Logic) -> Logic
Forall
exists :: Show a => [a] -> (a -> Logic) -> Logic
exists :: forall a. Show a => [a] -> (a -> Logic) -> Logic
exists = [a] -> (a -> Logic) -> Logic
forall a. Show a => [a] -> (a -> Logic) -> Logic
Exists