{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneDeriving #-}

-- | Self-explaining boolean predicates
--
-- These can be used to provide detailed counterexamples or witnesses for
-- boolean predicates that evaluate to 'False' or 'True', respectively.
--
-- NOTE: to keep this as simple as possible, we do not perform any boolean
-- simplifications (e.g., double negations, or De Morgan's laws) on the
-- predicates while evauating them. This can be added later if needed.
module Ouroboros.Consensus.Util.Pred
  ( Pred (..)
  , Evidence (..)
  , forgetEvidence
  , evalPred
  , Explainable (..)
  , ExplanationMode (..)
  , ShowExplain (..)
  , explainShallow
  , explainDeep
  )
where

import Data.Bifunctor (bimap)
import Data.Typeable (Typeable, cast)

{-------------------------------------------------------------------------------
  Self-explaining boolean predicates
-------------------------------------------------------------------------------}

data Pred tag where
  -- | Tag a predicate with some metadata
  (:=) :: !tag -> !(Pred tag) -> Pred tag
  -- | A concrete boolean value
  Bool :: !Bool -> Pred tag
  -- | Boolean negation
  Not :: !(Pred tag) -> Pred tag
  -- | Greater-than comparison
  (:>:) :: (Typeable a, Ord a, Show a) => !a -> !a -> Pred tag
  -- | Less-than-or-equal comparison
  (:<=:) :: (Typeable a, Ord a, Show a) => !a -> !a -> Pred tag
  -- | Equality comparison
  (:==:) :: (Typeable a, Eq a, Show a) => !a -> !a -> Pred tag
  -- | Conjunction
  (:/\:) :: !(Pred tag) -> !(Pred tag) -> Pred tag
  -- | Disjunction
  (:\/:) :: !(Pred tag) -> !(Pred tag) -> Pred tag

deriving instance Show tag => Show (Pred tag)

instance Eq tag => Eq (Pred tag) where
  (tag
t1 := Pred tag
p1) == :: Pred tag -> Pred tag -> Bool
== (tag
t2 := Pred tag
p2) =
    tag
t1 tag -> tag -> Bool
forall a. Eq a => a -> a -> Bool
== tag
t2 Bool -> Bool -> Bool
&& Pred tag
p1 Pred tag -> Pred tag -> Bool
forall a. Eq a => a -> a -> Bool
== Pred tag
p2
  Bool Bool
b1 == Bool Bool
b2 =
    Bool
b1 Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
b2
  Not Pred tag
p1 == Not Pred tag
p2 =
    Pred tag
p1 Pred tag -> Pred tag -> Bool
forall a. Eq a => a -> a -> Bool
== Pred tag
p2
  (a
a1 :>: a
b1) == (a
a2 :>: a
b2)
    | Just (a
a2', a
b2') <- (a, a) -> Maybe (a, a)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast (a
a2, a
b2) =
        a
a1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
a2' Bool -> Bool -> Bool
&& a
b1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b2'
  (a
a1 :<=: a
b1) == (a
a2 :<=: a
b2)
    | Just (a
a2', a
b2') <- (a, a) -> Maybe (a, a)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast (a
a2, a
b2) =
        a
a1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
a2' Bool -> Bool -> Bool
&& a
b1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b2'
  (a
a1 :==: a
b1) == (a
a2 :==: a
b2)
    | Just (a
a2', a
b2') <- (a, a) -> Maybe (a, a)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast (a
a2, a
b2) =
        a
a1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
a2' Bool -> Bool -> Bool
&& a
b1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b2'
  (Pred tag
a1 :/\: Pred tag
b1) == (Pred tag
a2 :/\: Pred tag
b2) =
    Pred tag
a1 Pred tag -> Pred tag -> Bool
forall a. Eq a => a -> a -> Bool
== Pred tag
a2 Bool -> Bool -> Bool
&& Pred tag
b1 Pred tag -> Pred tag -> Bool
forall a. Eq a => a -> a -> Bool
== Pred tag
b2
  (Pred tag
a1 :\/: Pred tag
b1) == (Pred tag
a2 :\/: Pred tag
b2) =
    Pred tag
a1 Pred tag -> Pred tag -> Bool
forall a. Eq a => a -> a -> Bool
== Pred tag
a2 Bool -> Bool -> Bool
&& Pred tag
b1 Pred tag -> Pred tag -> Bool
forall a. Eq a => a -> a -> Bool
== Pred tag
b2
  Pred tag
_ == Pred tag
_ =
    Bool
False

infixr 2 :=

infixr 3 :\/:

infixr 4 :/\:

infixr 5 `Not`

infix 5 :>:

infix 5 :<=:

infix 5 :==:

-- | Sufficient evidence to show that a predicate is either true or false
data Evidence (res :: Bool) a where
  ETrue :: Pred a -> Evidence True a
  EFalse :: Pred a -> Evidence False a

deriving instance Show a => Show (Evidence res a)
deriving instance Eq a => Eq (Evidence res a)

-- | Forget the evidence payload, yielding just its corresponding boolean value
forgetEvidence :: Evidence res a -> Bool
forgetEvidence :: forall (res :: Bool) a. Evidence res a -> Bool
forgetEvidence (ETrue Pred a
_) = Bool
True
forgetEvidence (EFalse Pred a
_) = Bool
False

-- | Evaluate a predicate, yielding either a counterexample or a witness.
--
-- The returned value contains the minimum (modulo conjunction/disjunction
-- short circuiting) evidence needed to explain the outcome.
--
-- Some examples:
--
-- >>> data P = A | B | C deriving Show
-- >>> a = A := Bool True   -- a ~ True
-- >>> b = B := 2+2 :==: 5  -- b ~ False
-- >>> c = C := 10 :>: 5    -- c ~ True
--
-- >>> evalPred (a :/\: c) show  -- success because both a~True and c~True
-- "ETrue ((A := Bool True) :/\\: (C := 10 :>: 5))"
--
-- >>> evalPred (a :\/: b) show  -- success because a~True, short-circuits
-- "ETrue (A := Bool True)"
--
-- >>> evalPred (a :/\: b :/\: c) show  -- failure because b~False, short-circuits
-- "EFalse (B := 4 :==: 5)"
--
-- >>> evalPred ((b :\/: a) :/\: (b :\/: c)) show  -- success because of a~True and c~True
-- "ETrue ((A := Bool True) :/\\: (C := 10 :>: 5))"
--
-- >>> evalPred (b :\/: (Not c)) show  -- failure because both b~False and c~True
-- "EFalse ((B := 4 :==: 5) :\\/: Not (C := 10 :>: 5))"
--
-- >>> evalPred (Not (a :/\: b)) show  -- success because b~False
-- "ETrue (Not (B := 4 :==: 5))"
--
-- >>> evalPred (Not (a :/\: c)) show  -- failure because both a~True and c~True
-- "EFalse (Not ((A := Bool True) :/\\: (C := 10 :>: 5)))"
evalPred :: Pred tag -> (forall res. Evidence res tag -> r) -> r
evalPred :: forall tag r.
Pred tag -> (forall (res :: Bool). Evidence res tag -> r) -> r
evalPred Pred tag
x forall (res :: Bool). Evidence res tag -> r
k =
  case Pred tag -> Either (Pred tag) (Pred tag)
forall {tag}. Pred tag -> Either (Pred tag) (Pred tag)
go Pred tag
x of
    Right Pred tag
e -> Evidence 'True tag -> r
forall (res :: Bool). Evidence res tag -> r
k (Pred tag -> Evidence 'True tag
forall a. Pred a -> Evidence 'True a
ETrue Pred tag
e)
    Left Pred tag
e -> Evidence 'False tag -> r
forall (res :: Bool). Evidence res tag -> r
k (Pred tag -> Evidence 'False tag
forall a. Pred a -> Evidence 'False a
EFalse Pred tag
e)
 where
  go :: Pred tag -> Either (Pred tag) (Pred tag)
go = \case
    tag
tag := Pred tag
p' ->
      (Pred tag -> Pred tag)
-> (Either (Pred tag) (Pred tag) -> Either (Pred tag) (Pred tag))
-> Pred tag
-> Either (Pred tag) (Pred tag)
lift (tag
tag tag -> Pred tag -> Pred tag
forall tag. tag -> Pred tag -> Pred tag
:=) Either (Pred tag) (Pred tag) -> Either (Pred tag) (Pred tag)
forall a. a -> a
id Pred tag
p'
    p :: Pred tag
p@(Bool Bool
b) ->
      Bool -> Pred tag -> Either (Pred tag) (Pred tag)
forall {a}. Bool -> a -> Either a a
boolean Bool
b Pred tag
p
    Not Pred tag
p' ->
      (Pred tag -> Pred tag)
-> (Either (Pred tag) (Pred tag) -> Either (Pred tag) (Pred tag))
-> Pred tag
-> Either (Pred tag) (Pred tag)
lift Pred tag -> Pred tag
forall tag. Pred tag -> Pred tag
Not Either (Pred tag) (Pred tag) -> Either (Pred tag) (Pred tag)
forall {a} {a}. Either a a -> Either a a
negation Pred tag
p'
    p :: Pred tag
p@(a
a :>: a
b) ->
      Bool -> Pred tag -> Either (Pred tag) (Pred tag)
forall {a}. Bool -> a -> Either a a
boolean (a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
b) Pred tag
p
    p :: Pred tag
p@(a
a :<=: a
b) ->
      Bool -> Pred tag -> Either (Pred tag) (Pred tag)
forall {a}. Bool -> a -> Either a a
boolean (a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
b) Pred tag
p
    p :: Pred tag
p@(a
a :==: a
b) ->
      Bool -> Pred tag -> Either (Pred tag) (Pred tag)
forall {a}. Bool -> a -> Either a a
boolean (a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b) Pred tag
p
    Pred tag
a :/\: Pred tag
b ->
      case Pred tag -> Either (Pred tag) (Pred tag)
go Pred tag
a of
        Left Pred tag
a' -> Pred tag -> Either (Pred tag) (Pred tag)
forall a b. a -> Either a b
Left Pred tag
a' -- short-circuit
        Right Pred tag
a' ->
          case Pred tag -> Either (Pred tag) (Pred tag)
go Pred tag
b of
            Right Pred tag
b' -> Pred tag -> Either (Pred tag) (Pred tag)
forall a b. b -> Either a b
Right (Pred tag
a' Pred tag -> Pred tag -> Pred tag
forall tag. Pred tag -> Pred tag -> Pred tag
:/\: Pred tag
b')
            Left Pred tag
b' -> Pred tag -> Either (Pred tag) (Pred tag)
forall a b. a -> Either a b
Left Pred tag
b'
    Pred tag
a :\/: Pred tag
b ->
      case Pred tag -> Either (Pred tag) (Pred tag)
go Pred tag
a of
        Right Pred tag
a' -> Pred tag -> Either (Pred tag) (Pred tag)
forall a b. b -> Either a b
Right Pred tag
a' -- short-circuit
        Left Pred tag
a' ->
          case Pred tag -> Either (Pred tag) (Pred tag)
go Pred tag
b of
            Right Pred tag
b' -> Pred tag -> Either (Pred tag) (Pred tag)
forall a b. b -> Either a b
Right Pred tag
b'
            Left Pred tag
b' -> Pred tag -> Either (Pred tag) (Pred tag)
forall a b. a -> Either a b
Left (Pred tag
a' Pred tag -> Pred tag -> Pred tag
forall tag. Pred tag -> Pred tag -> Pred tag
:\/: Pred tag
b')

  boolean :: Bool -> a -> Either a a
boolean Bool
b a
p
    | Bool
b = a -> Either a a
forall a b. b -> Either a b
Right a
p
    | Bool
otherwise = a -> Either a a
forall a b. a -> Either a b
Left a
p

  lift :: (Pred tag -> Pred tag)
-> (Either (Pred tag) (Pred tag) -> Either (Pred tag) (Pred tag))
-> Pred tag
-> Either (Pred tag) (Pred tag)
lift Pred tag -> Pred tag
f Either (Pred tag) (Pred tag) -> Either (Pred tag) (Pred tag)
g Pred tag
p = (Pred tag -> Pred tag)
-> (Pred tag -> Pred tag)
-> Either (Pred tag) (Pred tag)
-> Either (Pred tag) (Pred tag)
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Pred tag -> Pred tag
f Pred tag -> Pred tag
f (Either (Pred tag) (Pred tag) -> Either (Pred tag) (Pred tag)
g (Pred tag -> Either (Pred tag) (Pred tag)
go Pred tag
p))

  negation :: Either a a -> Either a a
negation = (a -> Either a a) -> (a -> Either a a) -> Either a a -> Either a a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either a -> Either a a
forall a b. b -> Either a b
Right a -> Either a a
forall a b. a -> Either a b
Left

{-------------------------------------------------------------------------------
  Explainable type class
-------------------------------------------------------------------------------}

-- | Explanation mode
--
-- Used to control whether we want to continue explaining terms beyond tags
-- * Shallow: only explain tags
-- * Deep: explain full predicates
data ExplanationMode = Shallow | Deep
  deriving (Int -> ExplanationMode -> ShowS
[ExplanationMode] -> ShowS
ExplanationMode -> String
(Int -> ExplanationMode -> ShowS)
-> (ExplanationMode -> String)
-> ([ExplanationMode] -> ShowS)
-> Show ExplanationMode
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ExplanationMode -> ShowS
showsPrec :: Int -> ExplanationMode -> ShowS
$cshow :: ExplanationMode -> String
show :: ExplanationMode -> String
$cshowList :: [ExplanationMode] -> ShowS
showList :: [ExplanationMode] -> ShowS
Show, ExplanationMode -> ExplanationMode -> Bool
(ExplanationMode -> ExplanationMode -> Bool)
-> (ExplanationMode -> ExplanationMode -> Bool)
-> Eq ExplanationMode
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ExplanationMode -> ExplanationMode -> Bool
== :: ExplanationMode -> ExplanationMode -> Bool
$c/= :: ExplanationMode -> ExplanationMode -> Bool
/= :: ExplanationMode -> ExplanationMode -> Bool
Eq)

-- | Provides a human-readable explanation for a value
class Explainable a where
  explain :: ExplanationMode -> a -> String
  explain = Int -> ExplanationMode -> a -> String
forall a. Explainable a => Int -> ExplanationMode -> a -> String
explainPrec Int
0

  explainPrec :: Int -> ExplanationMode -> a -> String
  explainPrec Int
_ = ExplanationMode -> a -> String
forall a. Explainable a => ExplanationMode -> a -> String
explain

  {-# MINIMAL (explain | explainPrec) #-}

-- | Shallow explanation
explainShallow :: Explainable a => a -> String
explainShallow :: forall a. Explainable a => a -> String
explainShallow = ExplanationMode -> a -> String
forall a. Explainable a => ExplanationMode -> a -> String
explain ExplanationMode
Shallow

-- | Deep explanation
explainDeep :: Explainable a => a -> String
explainDeep :: forall a. Explainable a => a -> String
explainDeep = ExplanationMode -> a -> String
forall a. Explainable a => ExplanationMode -> a -> String
explain ExplanationMode
Deep

-- | Default 'Explainable' instance via 'Show' to be used with 'deriving via'
newtype ShowExplain a = ShowExplain a
  deriving stock Int -> ShowExplain a -> ShowS
[ShowExplain a] -> ShowS
ShowExplain a -> String
(Int -> ShowExplain a -> ShowS)
-> (ShowExplain a -> String)
-> ([ShowExplain a] -> ShowS)
-> Show (ShowExplain a)
forall a. Show a => Int -> ShowExplain a -> ShowS
forall a. Show a => [ShowExplain a] -> ShowS
forall a. Show a => ShowExplain a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> ShowExplain a -> ShowS
showsPrec :: Int -> ShowExplain a -> ShowS
$cshow :: forall a. Show a => ShowExplain a -> String
show :: ShowExplain a -> String
$cshowList :: forall a. Show a => [ShowExplain a] -> ShowS
showList :: [ShowExplain a] -> ShowS
Show

instance Show a => Explainable (ShowExplain a) where
  explain :: ExplanationMode -> ShowExplain a -> String
explain ExplanationMode
_ (ShowExplain a
a) = a -> String
forall a. Show a => a -> String
show a
a

deriving via ShowExplain Bool instance Explainable Bool

instance Explainable a => Explainable (Pred a) where
  explainPrec :: Int -> ExplanationMode -> Pred a -> String
explainPrec Int
prec ExplanationMode
mode = \case
    a
tag := Pred a
p ->
      case ExplanationMode
mode of
        ExplanationMode
Shallow ->
          a -> String
forall a. Explainable a => a -> String
explainShallow a
tag
        ExplanationMode
Deep ->
          Bool -> ShowS
parensIf (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1) ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
            a -> String
forall a. Explainable a => a -> String
explainShallow a
tag String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" := " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> ExplanationMode -> Pred a -> String
forall a. Explainable a => Int -> ExplanationMode -> a -> String
explainPrec Int
2 ExplanationMode
mode Pred a
p
    Bool Bool
b ->
      ExplanationMode -> Bool -> String
forall a. Explainable a => ExplanationMode -> a -> String
explain ExplanationMode
mode Bool
b
    Not Pred a
p ->
      Bool -> ShowS
parensIf (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
4) ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
        String
"not " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> ExplanationMode -> Pred a -> String
forall a. Explainable a => Int -> ExplanationMode -> a -> String
explainPrec Int
5 ExplanationMode
mode Pred a
p
    a
a :>: a
b ->
      Bool -> ShowS
parensIf (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
4) ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
        a -> String
forall a. Show a => a -> String
show a
a String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" > " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> a -> String
forall a. Show a => a -> String
show a
b
    a
a :<=: a
b ->
      Bool -> ShowS
parensIf (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
4) ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
        a -> String
forall a. Show a => a -> String
show a
a String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" <= " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> a -> String
forall a. Show a => a -> String
show a
b
    a
a :==: a
b ->
      Bool -> ShowS
parensIf (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
4) ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
        a -> String
forall a. Show a => a -> String
show a
a String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" == " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> a -> String
forall a. Show a => a -> String
show a
b
    Pred a
a :/\: Pred a
b ->
      Bool -> ShowS
parensIf (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
3) ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
        Int -> ExplanationMode -> Pred a -> String
forall a. Explainable a => Int -> ExplanationMode -> a -> String
explainPrec Int
4 ExplanationMode
mode Pred a
a String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" and " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> ExplanationMode -> Pred a -> String
forall a. Explainable a => Int -> ExplanationMode -> a -> String
explainPrec Int
3 ExplanationMode
mode Pred a
b
    Pred a
a :\/: Pred a
b ->
      Bool -> ShowS
parensIf (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
2) ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
        Int -> ExplanationMode -> Pred a -> String
forall a. Explainable a => Int -> ExplanationMode -> a -> String
explainPrec Int
3 ExplanationMode
mode Pred a
a String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" or " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> ExplanationMode -> Pred a -> String
forall a. Explainable a => Int -> ExplanationMode -> a -> String
explainPrec Int
2 ExplanationMode
mode Pred a
b
   where
    parensIf :: Bool -> String -> String
    parensIf :: Bool -> ShowS
parensIf Bool
True String
s = String
"(" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
s String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
    parensIf Bool
False String
s = String
s