|
| 1 | +{-# LANGUAGE DerivingVia #-} |
| 2 | +{-# LANGUAGE GADTs #-} |
| 3 | +{-# LANGUAGE LambdaCase #-} |
| 4 | +{-# LANGUAGE RankNTypes #-} |
| 5 | +{-# LANGUAGE StandaloneDeriving #-} |
| 6 | + |
| 7 | +-- | Self-explaining boolean predicates |
| 8 | +-- |
| 9 | +-- These can be used to provide detailed counterexamples or witnesses for |
| 10 | +-- boolean predicates that evaluate to 'False' or 'True', respectively. |
| 11 | +-- |
| 12 | +-- NOTE: to keep this as simple as possible, we do not perform any boolean |
| 13 | +-- simplifications (e.g., double negations, or De Morgan's laws) on the |
| 14 | +-- predicates while evauating them. This can be added later if needed. |
| 15 | +module Ouroboros.Consensus.Util.Pred |
| 16 | + ( Pred (..) |
| 17 | + , Evidence |
| 18 | + , evalPred |
| 19 | + , Explainable (..) |
| 20 | + , ExplanationMode (..) |
| 21 | + , ShowExplain (..) |
| 22 | + , explainShallow |
| 23 | + , explainDeep |
| 24 | + ) |
| 25 | +where |
| 26 | + |
| 27 | +import Data.Bifunctor (bimap) |
| 28 | +import Data.Typeable (Typeable, cast) |
| 29 | + |
| 30 | +{------------------------------------------------------------------------------- |
| 31 | + Self-explaining boolean predicates |
| 32 | +-------------------------------------------------------------------------------} |
| 33 | + |
| 34 | +data Pred tag where |
| 35 | + -- | Tag a predicate with some metadata |
| 36 | + (:=) :: !tag -> !(Pred tag) -> Pred tag |
| 37 | + -- | A concrete boolean value |
| 38 | + Bool :: !Bool -> Pred tag |
| 39 | + -- | Boolean negation |
| 40 | + Not :: !(Pred tag) -> Pred tag |
| 41 | + -- | Greater-than comparison |
| 42 | + (:>:) :: (Typeable a, Ord a, Show a) => !a -> !a -> Pred tag |
| 43 | + -- | Less-than-or-equal comparison |
| 44 | + (:<=:) :: (Typeable a, Ord a, Show a) => !a -> !a -> Pred tag |
| 45 | + -- | Equality comparison |
| 46 | + (:==:) :: (Typeable a, Eq a, Show a) => !a -> !a -> Pred tag |
| 47 | + -- | Conjunction |
| 48 | + (:/\:) :: !(Pred tag) -> !(Pred tag) -> Pred tag |
| 49 | + -- | Disjunction |
| 50 | + (:\/:) :: !(Pred tag) -> !(Pred tag) -> Pred tag |
| 51 | + |
| 52 | +deriving instance Show tag => Show (Pred tag) |
| 53 | + |
| 54 | +instance Eq tag => Eq (Pred tag) where |
| 55 | + (t1 := p1) == (t2 := p2) = |
| 56 | + t1 == t2 && p1 == p2 |
| 57 | + Bool b1 == Bool b2 = |
| 58 | + b1 == b2 |
| 59 | + Not p1 == Not p2 = |
| 60 | + p1 == p2 |
| 61 | + (a1 :>: b1) == (a2 :>: b2) |
| 62 | + | Just (a2', b2') <- cast (a2, b2) = |
| 63 | + a1 == a2' && b1 == b2' |
| 64 | + (a1 :<=: b1) == (a2 :<=: b2) |
| 65 | + | Just (a2', b2') <- cast (a2, b2) = |
| 66 | + a1 == a2' && b1 == b2' |
| 67 | + (a1 :==: b1) == (a2 :==: b2) |
| 68 | + | Just (a2', b2') <- cast (a2, b2) = |
| 69 | + a1 == a2' && b1 == b2' |
| 70 | + (a1 :/\: b1) == (a2 :/\: b2) = |
| 71 | + a1 == a2 && b1 == b2 |
| 72 | + (a1 :\/: b1) == (a2 :\/: b2) = |
| 73 | + a1 == a2 && b1 == b2 |
| 74 | + _ == _ = |
| 75 | + False |
| 76 | + |
| 77 | +infixr 2 := |
| 78 | + |
| 79 | +infixr 3 :\/: |
| 80 | + |
| 81 | +infixr 4 :/\: |
| 82 | + |
| 83 | +infixr 5 `Not` |
| 84 | + |
| 85 | +infix 5 :>: |
| 86 | + |
| 87 | +infix 5 :<=: |
| 88 | + |
| 89 | +infix 5 :==: |
| 90 | + |
| 91 | +-- | Sufficient evidence to show that a predicate is either true or false |
| 92 | +type Evidence a = Pred a |
| 93 | + |
| 94 | +-- | Evaluate a predicate, yielding either a counterexample or a witness. |
| 95 | +-- |
| 96 | +-- The returned value contains the minimum (modulo conjunction/disjunction |
| 97 | +-- short circuiting) evidence needed to explain the outcome. |
| 98 | +-- |
| 99 | +-- Some examples: |
| 100 | +-- |
| 101 | +-- >>> data P = A | B | C deriving Show |
| 102 | +-- >>> a = A := Bool True -- a ~ True |
| 103 | +-- >>> b = B := 2+2 :==: 5 -- b ~ False |
| 104 | +-- >>> c = C := 10 :>: 5 -- c ~ True |
| 105 | +-- |
| 106 | +-- >>> evalPred $ a :/\: c -- success because both a~True and c~True |
| 107 | +-- Right ((A := Bool True) :/\: (C := 10 :>: 5)) |
| 108 | +-- |
| 109 | +-- >>> evalPred $ a :\/: b -- success because a~True, short-circuits |
| 110 | +-- Right (A := Bool True) |
| 111 | +-- |
| 112 | +-- >>> evalPred $ a :/\: b :/\: c -- failure because b~False, short-circuits |
| 113 | +-- Left (B := 4 :==: 5) |
| 114 | +-- |
| 115 | +-- >>> evalPred $ (b :\/: a) :/\: (b :\/: c) -- success because of a~True and c~True |
| 116 | +-- Right ((A := Bool True) :/\: (C := 10 :>: 5)) |
| 117 | +-- |
| 118 | +-- >>> evalPred $ b :\/: (Not c) -- failure because both b~False and c~True |
| 119 | +-- Left ((B := 4 :==: 5) :\/: Not (C := 10 :>: 5)) |
| 120 | +-- |
| 121 | +-- >>> evalPred $ Not (a :/\: b) -- success because b~False |
| 122 | +-- Right (Not (B := 4 :==: 5)) |
| 123 | +-- |
| 124 | +-- >>> evalPred $ Not (a :/\: c) -- failure because both a~True and c~True |
| 125 | +-- Left (Not ((A := Bool True) :/\: (C := 10 :>: 5))) |
| 126 | +evalPred :: Pred tag -> Either (Evidence tag) (Evidence tag) |
| 127 | +evalPred = \case |
| 128 | + tag := p' -> |
| 129 | + lift (tag :=) id p' |
| 130 | + p@(Bool b) -> |
| 131 | + boolean b p |
| 132 | + Not p' -> |
| 133 | + lift Not negation p' |
| 134 | + p@(a :>: b) -> |
| 135 | + boolean (a > b) p |
| 136 | + p@(a :<=: b) -> |
| 137 | + boolean (a <= b) p |
| 138 | + p@(a :==: b) -> |
| 139 | + boolean (a == b) p |
| 140 | + a :/\: b -> |
| 141 | + case evalPred a of |
| 142 | + Left a' -> Left a' -- short-circuit |
| 143 | + Right a' -> |
| 144 | + case evalPred b of |
| 145 | + Right b' -> Right (a' :/\: b') |
| 146 | + Left b' -> Left b' |
| 147 | + a :\/: b -> |
| 148 | + case evalPred a of |
| 149 | + Right a' -> Right a' -- short-circuit |
| 150 | + Left a' -> |
| 151 | + case evalPred b of |
| 152 | + Right b' -> Right b' |
| 153 | + Left b' -> Left (a' :\/: b') |
| 154 | + where |
| 155 | + boolean b p |
| 156 | + | b = Right p |
| 157 | + | otherwise = Left p |
| 158 | + |
| 159 | + lift f g p = bimap f f (g (evalPred p)) |
| 160 | + |
| 161 | + negation = either Right Left |
| 162 | + |
| 163 | +{------------------------------------------------------------------------------- |
| 164 | + Explainable type class |
| 165 | +-------------------------------------------------------------------------------} |
| 166 | + |
| 167 | +-- | Explanation mode |
| 168 | +-- |
| 169 | +-- Used to control whether we want to continue explaining terms beyond tags |
| 170 | +-- * Shallow: only explain tags |
| 171 | +-- * Deep: explain full predicates |
| 172 | +data ExplanationMode = Shallow | Deep |
| 173 | + deriving (Show, Eq) |
| 174 | + |
| 175 | +-- | Provides a human-readable explanation for a value |
| 176 | +class Explainable a where |
| 177 | + explain :: ExplanationMode -> a -> String |
| 178 | + explain = explainPrec 0 |
| 179 | + |
| 180 | + explainPrec :: Int -> ExplanationMode -> a -> String |
| 181 | + explainPrec _ = explain |
| 182 | + |
| 183 | + {-# MINIMAL (explain | explainPrec) #-} |
| 184 | + |
| 185 | +-- | Shallow explanation |
| 186 | +explainShallow :: Explainable a => a -> String |
| 187 | +explainShallow = explain Shallow |
| 188 | + |
| 189 | +-- | Deep explanation |
| 190 | +explainDeep :: Explainable a => a -> String |
| 191 | +explainDeep = explain Deep |
| 192 | + |
| 193 | +-- | Default 'Explainable' instance via 'Show' to be used with 'deriving via' |
| 194 | +newtype ShowExplain a = ShowExplain a |
| 195 | + deriving stock Show |
| 196 | + |
| 197 | +instance Show a => Explainable (ShowExplain a) where |
| 198 | + explain _ (ShowExplain a) = show a |
| 199 | + |
| 200 | +deriving via ShowExplain Bool instance Explainable Bool |
| 201 | + |
| 202 | +instance Explainable a => Explainable (Pred a) where |
| 203 | + explainPrec prec mode = \case |
| 204 | + tag := p -> |
| 205 | + case mode of |
| 206 | + Shallow -> |
| 207 | + explainShallow tag |
| 208 | + Deep -> |
| 209 | + parensIf (prec > 1) $ |
| 210 | + explainShallow tag <> " := " <> explainPrec 2 mode p |
| 211 | + Bool b -> |
| 212 | + explain mode b |
| 213 | + Not p -> |
| 214 | + parensIf (prec > 4) $ |
| 215 | + "not " <> explainPrec 5 mode p |
| 216 | + a :>: b -> |
| 217 | + parensIf (prec > 4) $ |
| 218 | + show a <> " > " <> show b |
| 219 | + a :<=: b -> |
| 220 | + parensIf (prec > 4) $ |
| 221 | + show a <> " <= " <> show b |
| 222 | + a :==: b -> |
| 223 | + parensIf (prec > 4) $ |
| 224 | + show a <> " == " <> show b |
| 225 | + a :/\: b -> |
| 226 | + parensIf (prec > 3) $ |
| 227 | + explainPrec 4 mode a <> " and " <> explainPrec 3 mode b |
| 228 | + a :\/: b -> |
| 229 | + parensIf (prec > 2) $ |
| 230 | + explainPrec 3 mode a <> " or " <> explainPrec 2 mode b |
| 231 | + where |
| 232 | + parensIf :: Bool -> String -> String |
| 233 | + parensIf True s = "(" <> s <> ")" |
| 234 | + parensIf False s = s |
0 commit comments