content: {-# 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 p = case p of
    x :== y          -> x :/= y
    x :/= y          -> x :== y
    x :<  y          -> x :>= y
    x :<= y          -> x :>  y
    x :>  y          -> x :<= y
    x :>= y          -> x :<  y
    x `Member`    xs -> x `NotMember` xs
    x `NotMember` xs -> x `Member`    xs
  
  -- See Yuri Gurevich's "Intuitionistic logic with strong negation" (1977).
  strongNeg :: Logic -> Logic
  strongNeg l0 = case l0 of
    Bot              -> Top
    Top              -> Bot
    l :&& r          -> strongNeg l :|| strongNeg r
    l :|| r          -> strongNeg l :&& strongNeg r
    l :=> r          ->           l :&& strongNeg r
    Not l            -> l
    LogicPredicate p -> LogicPredicate (dual p)
    Forall xs p      -> Exists xs (strongNeg . p)
    Exists xs p      -> Forall xs (strongNeg . p)
    Boolean b        -> Boolean (not b)
    Annotate s l     -> Annotate s (strongNeg 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 Show
  
  boolean :: Logic -> Bool
  boolean l = case logic l of
    VFalse _ -> False
    VTrue    -> True
  
  logic :: Logic -> Value
  logic Bot            = VFalse BotC
  logic Top            = VTrue
  logic (l :&& r)      = case logic l of
    VFalse ce -> VFalse (Fst ce)
    VTrue     -> case logic r of
      VFalse ce' -> VFalse (Snd ce')
      VTrue      -> VTrue
  logic (l :|| r)      = case logic l of
    VTrue     -> VTrue
    VFalse ce -> case logic r of
      VTrue      -> VTrue
      VFalse ce' -> VFalse (EitherC ce ce')
  logic (l :=> r)      = case logic l of
    VFalse _ -> VTrue
    VTrue    -> case logic r of
      VTrue     -> VTrue
      VFalse ce -> VFalse (ImpliesC ce)
  logic (Not l)        = case logic (strongNeg l) of
    VTrue     -> VTrue
    VFalse ce -> VFalse (NotC ce)
  logic (LogicPredicate p) = evalLogicPredicate p
  logic (Forall xs0 p) = go xs0
    where
      go []       = VTrue
      go (x : xs) = case logic (p x) of
        VTrue     -> go xs
        VFalse ce -> VFalse (ForallC x ce)
  logic (Exists xs0 p) = go xs0 []
    where
      go []       ces = VFalse (ExistsC xs0 (reverse ces))
      go (x : xs) ces = case logic (p x) of
        VTrue     -> VTrue
        VFalse ce -> go xs (ce : ces)
  logic (Boolean b)    = if b then VTrue else VFalse BooleanC
  logic (Annotate s l) = case logic l of
    VTrue     -> VTrue
    VFalse ce -> VFalse (AnnotateC s ce)
  
  evalLogicPredicate :: LogicPredicate -> Value
  evalLogicPredicate p0 = let b = go p0 in case p0 of
    x :== y          -> b (x == y)
    x :/= y          -> b (x /= y)
    x :<  y          -> b (x <  y)
    x :<= y          -> b (x <= y)
    x :>  y          -> b (x >  y)
    x :>= y          -> b (x >= y)
    x `Member`    xs -> b (x `elem`    xs)
    x `NotMember` xs -> b (x `notElem` xs)
    where
      go :: LogicPredicate -> Bool -> Value
      go _ True  = VTrue
      go p False = VFalse (PredicateC (dual 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 = go []
    where
      go _acc Bot = []
      go acc  Top = acc
      go acc (l :&& r) | boolean l && boolean r = go (go acc l) r
                       | otherwise              = acc
      go acc (l :|| r) | boolean l = go acc l
                       | boolean r = go acc r
                       | otherwise = acc
      go acc (l :=> r) | boolean (l :=> r) = go (go acc l) r
                       | otherwise         = acc
      go acc (Not l) | not (boolean l) = go acc l
                     | otherwise       = acc
      go acc (LogicPredicate _p) = acc
      go acc (Forall xs p)
        | boolean (Forall xs p) = acc ++ concat [ go [] (p x)
                                                | x <- xs, boolean (p x)
                                                ]
        | otherwise             = acc
      go acc (Exists xs p)
        | boolean (Exists xs p) = acc ++ concat (take 1 [ go [] (p x)
                                                        | x <- xs, boolean (p x)
                                                        ])
        | otherwise             = acc
      go acc (Boolean _b)   = acc
      go acc (Annotate s l) = go (acc ++ [s]) 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
  x .== y = LogicPredicate (x :== y)
  
  (./=) :: (Eq a, Show a) => a -> a -> Logic
  x ./= y = LogicPredicate (x :/= y)
  
  (.<) :: (Ord a, Show a) => a -> a -> Logic
  x .< y = LogicPredicate (x :< y)
  
  (.<=) :: (Ord a, Show a) => a -> a -> Logic
  x .<= y = LogicPredicate (x :<= y)
  
  (.>) :: (Ord a, Show a) => a -> a -> Logic
  x .> y = LogicPredicate (x :> y)
  
  (.>=) :: (Ord a, Show a) => a -> a -> Logic
  x .>= y = LogicPredicate (x :>= y)
  
  member :: (Foldable t, Eq a, Show a, Show (t a)) => a -> t a -> Logic
  member x xs = LogicPredicate (Member x xs)
  
  notMember :: (Foldable t, Eq a, Show a, Show (t a)) => a -> t a -> Logic
  notMember x xs = LogicPredicate (NotMember x xs)
  
  (.//) :: Logic -> String -> Logic
  l .// s = Annotate s l
  
  (.&&) :: Logic -> Logic -> Logic
  (.&&) = (:&&)
  
  (.||) :: Logic -> Logic -> Logic
  (.||) = (:||)
  
  (.=>) :: Logic -> Logic -> Logic
  (.=>) = (:=>)
  
  forall :: Show a => [a] -> (a -> Logic) -> Logic
  forall = Forall
  
  exists :: Show a => [a] -> (a -> Logic) -> Logic
  exists = Exists
  