{-# LANGUAGE DerivingStrategies        #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE StandaloneDeriving        #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Test.StateMachine.Logic
-- Copyright   :  (C) 2017, ATS Advanced Telematic Systems GmbH
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  Stevan Andjelkovic <stevan.andjelkovic@strath.ac.uk>
-- Stability   :  provisional
-- Portability :  non-portable (GHC extensions)
--
-- This module defines a predicate logic-like language and its counterexample
-- semantics.
--
-----------------------------------------------------------------------------

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

-- See Yuri Gurevich's "Intuitionistic logic with strong negation" (1977).
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
showList :: [Value] -> ShowS
$cshowList :: [Value] -> ShowS
show :: Value -> String
$cshow :: Value -> String
showsPrec :: Int -> Value -> ShowS
$cshowsPrec :: Int -> 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 (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))

-- | Gather user annotations of a true logic expression.
--
-- >>> gatherAnnotations (Top .// "top")
-- ["top"]
--
-- >>> gatherAnnotations ((Bot .// "bot") .|| (Top .// "top"))
-- ["top"]
--
-- >>> gatherAnnotations (Top .// "top1" .&& Top .// "top2")
-- ["top1","top2"]
--
-- >>> gatherAnnotations (Bot .// "bot" .&& Top .// "top")
-- []
--
-- >>> gatherAnnotations (forall [1,2,3] (\i -> 0 .< i .// "positive"))
-- ["positive","positive","positive"]
--
-- >>> gatherAnnotations (forall [0,1,2,3] (\i -> 0 .< i .// "positive"))
-- []
--
-- >>> gatherAnnotations (exists [1,2,3] (\i -> 0 .< i .// "positive"))
-- ["positive"]
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 .== :: 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 ./= :: 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 .< :: 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 .<= :: 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 .> :: 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 .>= :: 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 :: 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 :: 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 :: [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 :: [a] -> (a -> Logic) -> Logic
exists = [a] -> (a -> Logic) -> Logic
forall a. Show a => [a] -> (a -> Logic) -> Logic
Exists