never executed always true always false
1 {-# LANGUAGE DeriveDataTypeable #-}
2 {-# LANGUAGE DeriveTraversable #-}
3
4 --------------------------------------------------------------------------------
5 -- | Boolean formulas without quantifiers and without negation.
6 -- Such a formula consists of variables, conjunctions (and), and disjunctions (or).
7 --
8 -- This module is used to represent minimal complete definitions for classes.
9 --
10 module GHC.Data.BooleanFormula (
11 BooleanFormula(..), LBooleanFormula,
12 mkFalse, mkTrue, mkAnd, mkOr, mkVar,
13 isFalse, isTrue,
14 eval, simplify, isUnsatisfied,
15 implies, impliesAtom,
16 pprBooleanFormula, pprBooleanFormulaNice
17 ) where
18
19 import GHC.Prelude
20
21 import Data.List ( nub, intersperse )
22 import Data.Data
23
24 import GHC.Utils.Monad
25 import GHC.Utils.Outputable
26 import GHC.Utils.Binary
27 import GHC.Parser.Annotation ( LocatedL )
28 import GHC.Types.SrcLoc
29 import GHC.Types.Unique
30 import GHC.Types.Unique.Set
31
32 ----------------------------------------------------------------------
33 -- Boolean formula type and smart constructors
34 ----------------------------------------------------------------------
35
36 type LBooleanFormula a = LocatedL (BooleanFormula a)
37
38 data BooleanFormula a = Var a | And [LBooleanFormula a] | Or [LBooleanFormula a]
39 | Parens (LBooleanFormula a)
40 deriving (Eq, Data, Functor, Foldable, Traversable)
41
42 mkVar :: a -> BooleanFormula a
43 mkVar = Var
44
45 mkFalse, mkTrue :: BooleanFormula a
46 mkFalse = Or []
47 mkTrue = And []
48
49 -- Convert a Bool to a BooleanFormula
50 mkBool :: Bool -> BooleanFormula a
51 mkBool False = mkFalse
52 mkBool True = mkTrue
53
54 -- Make a conjunction, and try to simplify
55 mkAnd :: Eq a => [LBooleanFormula a] -> BooleanFormula a
56 mkAnd = maybe mkFalse (mkAnd' . nub) . concatMapM fromAnd
57 where
58 -- See Note [Simplification of BooleanFormulas]
59 fromAnd :: LBooleanFormula a -> Maybe [LBooleanFormula a]
60 fromAnd (L _ (And xs)) = Just xs
61 -- assume that xs are already simplified
62 -- otherwise we would need: fromAnd (And xs) = concat <$> traverse fromAnd xs
63 fromAnd (L _ (Or [])) = Nothing
64 -- in case of False we bail out, And [..,mkFalse,..] == mkFalse
65 fromAnd x = Just [x]
66 mkAnd' [x] = unLoc x
67 mkAnd' xs = And xs
68
69 mkOr :: Eq a => [LBooleanFormula a] -> BooleanFormula a
70 mkOr = maybe mkTrue (mkOr' . nub) . concatMapM fromOr
71 where
72 -- See Note [Simplification of BooleanFormulas]
73 fromOr (L _ (Or xs)) = Just xs
74 fromOr (L _ (And [])) = Nothing
75 fromOr x = Just [x]
76 mkOr' [x] = unLoc x
77 mkOr' xs = Or xs
78
79
80 {-
81 Note [Simplification of BooleanFormulas]
82 ~~~~~~~~~~~~~~~~~~~~~~
83 The smart constructors (`mkAnd` and `mkOr`) do some attempt to simplify expressions. In particular,
84 1. Collapsing nested ands and ors, so
85 `(mkAnd [x, And [y,z]]`
86 is represented as
87 `And [x,y,z]`
88 Implemented by `fromAnd`/`fromOr`
89 2. Collapsing trivial ands and ors, so
90 `mkAnd [x]` becomes just `x`.
91 Implemented by mkAnd' / mkOr'
92 3. Conjunction with false, disjunction with true is simplified, i.e.
93 `mkAnd [mkFalse,x]` becomes `mkFalse`.
94 4. Common subexpression elimination:
95 `mkAnd [x,x,y]` is reduced to just `mkAnd [x,y]`.
96
97 This simplification is not exhaustive, in the sense that it will not produce
98 the smallest possible equivalent expression. For example,
99 `Or [And [x,y], And [x]]` could be simplified to `And [x]`, but it currently
100 is not. A general simplifier would need to use something like BDDs.
101
102 The reason behind the (crude) simplifier is to make for more user friendly
103 error messages. E.g. for the code
104 > class Foo a where
105 > {-# MINIMAL bar, (foo, baq | foo, quux) #-}
106 > instance Foo Int where
107 > bar = ...
108 > baz = ...
109 > quux = ...
110 We don't show a ridiculous error message like
111 Implement () and (either (`foo' and ()) or (`foo' and ()))
112 -}
113
114 ----------------------------------------------------------------------
115 -- Evaluation and simplification
116 ----------------------------------------------------------------------
117
118 isFalse :: BooleanFormula a -> Bool
119 isFalse (Or []) = True
120 isFalse _ = False
121
122 isTrue :: BooleanFormula a -> Bool
123 isTrue (And []) = True
124 isTrue _ = False
125
126 eval :: (a -> Bool) -> BooleanFormula a -> Bool
127 eval f (Var x) = f x
128 eval f (And xs) = all (eval f . unLoc) xs
129 eval f (Or xs) = any (eval f . unLoc) xs
130 eval f (Parens x) = eval f (unLoc x)
131
132 -- Simplify a boolean formula.
133 -- The argument function should give the truth of the atoms, or Nothing if undecided.
134 simplify :: Eq a => (a -> Maybe Bool) -> BooleanFormula a -> BooleanFormula a
135 simplify f (Var a) = case f a of
136 Nothing -> Var a
137 Just b -> mkBool b
138 simplify f (And xs) = mkAnd (map (\(L l x) -> L l (simplify f x)) xs)
139 simplify f (Or xs) = mkOr (map (\(L l x) -> L l (simplify f x)) xs)
140 simplify f (Parens x) = simplify f (unLoc x)
141
142 -- Test if a boolean formula is satisfied when the given values are assigned to the atoms
143 -- if it is, returns Nothing
144 -- if it is not, return (Just remainder)
145 isUnsatisfied :: Eq a => (a -> Bool) -> BooleanFormula a -> Maybe (BooleanFormula a)
146 isUnsatisfied f bf
147 | isTrue bf' = Nothing
148 | otherwise = Just bf'
149 where
150 f' x = if f x then Just True else Nothing
151 bf' = simplify f' bf
152
153 -- prop_simplify:
154 -- eval f x == True <==> isTrue (simplify (Just . f) x)
155 -- eval f x == False <==> isFalse (simplify (Just . f) x)
156
157 -- If the boolean formula holds, does that mean that the given atom is always true?
158 impliesAtom :: Eq a => BooleanFormula a -> a -> Bool
159 Var x `impliesAtom` y = x == y
160 And xs `impliesAtom` y = any (\x -> (unLoc x) `impliesAtom` y) xs
161 -- we have all of xs, so one of them implying y is enough
162 Or xs `impliesAtom` y = all (\x -> (unLoc x) `impliesAtom` y) xs
163 Parens x `impliesAtom` y = (unLoc x) `impliesAtom` y
164
165 implies :: Uniquable a => BooleanFormula a -> BooleanFormula a -> Bool
166 implies e1 e2 = go (Clause emptyUniqSet [e1]) (Clause emptyUniqSet [e2])
167 where
168 go :: Uniquable a => Clause a -> Clause a -> Bool
169 go l@Clause{ clauseExprs = hyp:hyps } r =
170 case hyp of
171 Var x | memberClauseAtoms x r -> True
172 | otherwise -> go (extendClauseAtoms l x) { clauseExprs = hyps } r
173 Parens hyp' -> go l { clauseExprs = unLoc hyp':hyps } r
174 And hyps' -> go l { clauseExprs = map unLoc hyps' ++ hyps } r
175 Or hyps' -> all (\hyp' -> go l { clauseExprs = unLoc hyp':hyps } r) hyps'
176 go l r@Clause{ clauseExprs = con:cons } =
177 case con of
178 Var x | memberClauseAtoms x l -> True
179 | otherwise -> go l (extendClauseAtoms r x) { clauseExprs = cons }
180 Parens con' -> go l r { clauseExprs = unLoc con':cons }
181 And cons' -> all (\con' -> go l r { clauseExprs = unLoc con':cons }) cons'
182 Or cons' -> go l r { clauseExprs = map unLoc cons' ++ cons }
183 go _ _ = False
184
185 -- A small sequent calculus proof engine.
186 data Clause a = Clause {
187 clauseAtoms :: UniqSet a,
188 clauseExprs :: [BooleanFormula a]
189 }
190 extendClauseAtoms :: Uniquable a => Clause a -> a -> Clause a
191 extendClauseAtoms c x = c { clauseAtoms = addOneToUniqSet (clauseAtoms c) x }
192
193 memberClauseAtoms :: Uniquable a => a -> Clause a -> Bool
194 memberClauseAtoms x c = x `elementOfUniqSet` clauseAtoms c
195
196 ----------------------------------------------------------------------
197 -- Pretty printing
198 ----------------------------------------------------------------------
199
200 -- Pretty print a BooleanFormula,
201 -- using the arguments as pretty printers for Var, And and Or respectively
202 pprBooleanFormula' :: (Rational -> a -> SDoc)
203 -> (Rational -> [SDoc] -> SDoc)
204 -> (Rational -> [SDoc] -> SDoc)
205 -> Rational -> BooleanFormula a -> SDoc
206 pprBooleanFormula' pprVar pprAnd pprOr = go
207 where
208 go p (Var x) = pprVar p x
209 go p (And []) = cparen (p > 0) $ empty
210 go p (And xs) = pprAnd p (map (go 3 . unLoc) xs)
211 go _ (Or []) = keyword $ text "FALSE"
212 go p (Or xs) = pprOr p (map (go 2 . unLoc) xs)
213 go p (Parens x) = go p (unLoc x)
214
215 -- Pretty print in source syntax, "a | b | c,d,e"
216 pprBooleanFormula :: (Rational -> a -> SDoc) -> Rational -> BooleanFormula a -> SDoc
217 pprBooleanFormula pprVar = pprBooleanFormula' pprVar pprAnd pprOr
218 where
219 pprAnd p = cparen (p > 3) . fsep . punctuate comma
220 pprOr p = cparen (p > 2) . fsep . intersperse vbar
221
222 -- Pretty print human in readable format, "either `a' or `b' or (`c', `d' and `e')"?
223 pprBooleanFormulaNice :: Outputable a => BooleanFormula a -> SDoc
224 pprBooleanFormulaNice = pprBooleanFormula' pprVar pprAnd pprOr 0
225 where
226 pprVar _ = quotes . ppr
227 pprAnd p = cparen (p > 1) . pprAnd'
228 pprAnd' [] = empty
229 pprAnd' [x,y] = x <+> text "and" <+> y
230 pprAnd' xs@(_:_) = fsep (punctuate comma (init xs)) <> text ", and" <+> last xs
231 pprOr p xs = cparen (p > 1) $ text "either" <+> sep (intersperse (text "or") xs)
232
233 instance (OutputableBndr a) => Outputable (BooleanFormula a) where
234 ppr = pprBooleanFormulaNormal
235
236 pprBooleanFormulaNormal :: (OutputableBndr a)
237 => BooleanFormula a -> SDoc
238 pprBooleanFormulaNormal = go
239 where
240 go (Var x) = pprPrefixOcc x
241 go (And xs) = fsep $ punctuate comma (map (go . unLoc) xs)
242 go (Or []) = keyword $ text "FALSE"
243 go (Or xs) = fsep $ intersperse vbar (map (go . unLoc) xs)
244 go (Parens x) = parens (go $ unLoc x)
245
246
247 ----------------------------------------------------------------------
248 -- Binary
249 ----------------------------------------------------------------------
250
251 instance Binary a => Binary (BooleanFormula a) where
252 put_ bh (Var x) = putByte bh 0 >> put_ bh x
253 put_ bh (And xs) = putByte bh 1 >> put_ bh xs
254 put_ bh (Or xs) = putByte bh 2 >> put_ bh xs
255 put_ bh (Parens x) = putByte bh 3 >> put_ bh x
256
257 get bh = do
258 h <- getByte bh
259 case h of
260 0 -> Var <$> get bh
261 1 -> And <$> get bh
262 2 -> Or <$> get bh
263 _ -> Parens <$> get bh