1 --------------------------------------------------------------------------------
2 -- | Boolean formulas without quantifiers and without negation.
3 -- Such a formula consists of variables, conjunctions (and), and disjunctions (or).
4 --
5 -- This module is used to represent minimal complete definitions for classes.
6 --
7 {-# LANGUAGE DeriveDataTypeable, DeriveFunctor, DeriveFoldable,
8 DeriveTraversable #-}
10 module BooleanFormula (
11 BooleanFormula(..),
12 mkFalse, mkTrue, mkAnd, mkOr, mkVar,
13 isFalse, isTrue,
14 eval, simplify, isUnsatisfied,
15 implies, impliesAtom,
16 pprBooleanFormula, pprBooleanFormulaNice
17 ) where
19 import Data.List ( nub, intersperse )
20 import Data.Data
21 import Data.Foldable ( Foldable )
22 import Data.Traversable ( Traversable )
25 import Outputable
26 import Binary
28 ----------------------------------------------------------------------
29 -- Boolean formula type and smart constructors
30 ----------------------------------------------------------------------
32 data BooleanFormula a = Var a | And [BooleanFormula a] | Or [BooleanFormula a]
33 deriving (Eq, Data, Typeable, Functor, Foldable, Traversable)
35 mkVar :: a -> BooleanFormula a
36 mkVar = Var
38 mkFalse, mkTrue :: BooleanFormula a
39 mkFalse = Or []
40 mkTrue = And []
42 -- Convert a Bool to a BooleanFormula
43 mkBool :: Bool -> BooleanFormula a
44 mkBool False = mkFalse
45 mkBool True = mkTrue
47 -- Make a conjunction, and try to simplify
48 mkAnd :: Eq a => [BooleanFormula a] -> BooleanFormula a
49 mkAnd = maybe mkFalse (mkAnd' . nub) . concatMapM fromAnd
50 where
51 -- See Note [Simplification of BooleanFormulas]
52 fromAnd :: BooleanFormula a -> Maybe [BooleanFormula a]
53 fromAnd (And xs) = Just xs
54 -- assume that xs are already simplified
55 -- otherwise we would need: fromAnd (And xs) = concat <\$> traverse fromAnd xs
56 fromAnd (Or []) = Nothing -- in case of False we bail out, And [..,mkFalse,..] == mkFalse
57 fromAnd x = Just [x]
58 mkAnd' [x] = x
59 mkAnd' xs = And xs
61 mkOr :: Eq a => [BooleanFormula a] -> BooleanFormula a
62 mkOr = maybe mkTrue (mkOr' . nub) . concatMapM fromOr
63 where
64 -- See Note [Simplification of BooleanFormulas]
65 fromOr (Or xs) = Just xs
66 fromOr (And []) = Nothing
67 fromOr x = Just [x]
68 mkOr' [x] = x
69 mkOr' xs = Or xs
72 {-
73 Note [Simplification of BooleanFormulas]
74 ~~~~~~~~~~~~~~~~~~~~~~
75 The smart constructors (`mkAnd` and `mkOr`) do some attempt to simplify expressions. In particular,
76 1. Collapsing nested ands and ors, so
77 `(mkAnd [x, And [y,z]]`
78 is represented as
79 `And [x,y,z]`
80 Implemented by `fromAnd`/`fromOr`
81 2. Collapsing trivial ands and ors, so
82 `mkAnd [x]` becomes just `x`.
83 Implemented by mkAnd' / mkOr'
84 3. Conjunction with false, disjunction with true is simplified, i.e.
85 `mkAnd [mkFalse,x]` becomes `mkFalse`.
86 4. Common subexpresion elimination:
87 `mkAnd [x,x,y]` is reduced to just `mkAnd [x,y]`.
89 This simplification is not exhaustive, in the sense that it will not produce
90 the smallest possible equivalent expression. For example,
91 `Or [And [x,y], And [x]]` could be simplified to `And [x]`, but it currently
92 is not. A general simplifier would need to use something like BDDs.
94 The reason behind the (crude) simplifier is to make for more user friendly
95 error messages. E.g. for the code
96 > class Foo a where
97 > {-# MINIMAL bar, (foo, baq | foo, quux) #-}
98 > instance Foo Int where
99 > bar = ...
100 > baz = ...
101 > quux = ...
102 We don't show a ridiculous error message like
103 Implement () and (either (`foo' and ()) or (`foo' and ()))
104 -}
106 ----------------------------------------------------------------------
107 -- Evaluation and simplification
108 ----------------------------------------------------------------------
110 isFalse :: BooleanFormula a -> Bool
111 isFalse (Or []) = True
112 isFalse _ = False
114 isTrue :: BooleanFormula a -> Bool
115 isTrue (And []) = True
116 isTrue _ = False
118 eval :: (a -> Bool) -> BooleanFormula a -> Bool
119 eval f (Var x) = f x
120 eval f (And xs) = all (eval f) xs
121 eval f (Or xs) = any (eval f) xs
123 -- Simplify a boolean formula.
124 -- The argument function should give the truth of the atoms, or Nothing if undecided.
125 simplify :: Eq a => (a -> Maybe Bool) -> BooleanFormula a -> BooleanFormula a
126 simplify f (Var a) = case f a of
127 Nothing -> Var a
128 Just b -> mkBool b
129 simplify f (And xs) = mkAnd (map (simplify f) xs)
130 simplify f (Or xs) = mkOr (map (simplify f) xs)
132 -- Test if a boolean formula is satisfied when the given values are assigned to the atoms
133 -- if it is, returns Nothing
134 -- if it is not, return (Just remainder)
135 isUnsatisfied :: Eq a => (a -> Bool) -> BooleanFormula a -> Maybe (BooleanFormula a)
136 isUnsatisfied f bf
137 | isTrue bf' = Nothing
138 | otherwise = Just bf'
139 where
140 f' x = if f x then Just True else Nothing
141 bf' = simplify f' bf
143 -- prop_simplify:
144 -- eval f x == True <==> isTrue (simplify (Just . f) x)
145 -- eval f x == False <==> isFalse (simplify (Just . f) x)
147 -- If the boolean formula holds, does that mean that the given atom is always true?
148 impliesAtom :: Eq a => BooleanFormula a -> a -> Bool
149 Var x `impliesAtom` y = x == y
150 And xs `impliesAtom` y = any (`impliesAtom` y) xs -- we have all of xs, so one of them implying y is enough
151 Or xs `impliesAtom` y = all (`impliesAtom` y) xs
153 implies :: Eq a => BooleanFormula a -> BooleanFormula a -> Bool
154 x `implies` Var y = x `impliesAtom` y
155 x `implies` And ys = all (x `implies`) ys
156 x `implies` Or ys = any (x `implies`) ys
158 ----------------------------------------------------------------------
159 -- Pretty printing
160 ----------------------------------------------------------------------
162 -- Pretty print a BooleanFormula,
163 -- using the arguments as pretty printers for Var, And and Or respectively
164 pprBooleanFormula' :: (Rational -> a -> SDoc)
165 -> (Rational -> [SDoc] -> SDoc)
166 -> (Rational -> [SDoc] -> SDoc)
167 -> Rational -> BooleanFormula a -> SDoc
168 pprBooleanFormula' pprVar pprAnd pprOr = go
169 where
170 go p (Var x) = pprVar p x
171 go p (And []) = cparen (p > 0) \$ empty
172 go p (And xs) = pprAnd p (map (go 3) xs)
173 go _ (Or []) = keyword \$ text "FALSE"
174 go p (Or xs) = pprOr p (map (go 2) xs)
176 -- Pretty print in source syntax, "a | b | c,d,e"
177 pprBooleanFormula :: (Rational -> a -> SDoc) -> Rational -> BooleanFormula a -> SDoc
178 pprBooleanFormula pprVar = pprBooleanFormula' pprVar pprAnd pprOr
179 where
180 pprAnd p = cparen (p > 3) . fsep . punctuate comma
181 pprOr p = cparen (p > 2) . fsep . intersperse (text "|")
183 -- Pretty print human in readable format, "either `a' or `b' or (`c', `d' and `e')"?
184 pprBooleanFormulaNice :: Outputable a => BooleanFormula a -> SDoc
185 pprBooleanFormulaNice = pprBooleanFormula' pprVar pprAnd pprOr 0
186 where
187 pprVar _ = quotes . ppr
188 pprAnd p = cparen (p > 1) . pprAnd'
189 pprAnd' [] = empty
190 pprAnd' [x,y] = x <+> text "and" <+> y
191 pprAnd' xs@(_:_) = fsep (punctuate comma (init xs)) <> text ", and" <+> last xs
192 pprOr p xs = cparen (p > 1) \$ text "either" <+> sep (intersperse (text "or") xs)
194 instance Outputable a => Outputable (BooleanFormula a) where
195 pprPrec = pprBooleanFormula pprPrec
197 ----------------------------------------------------------------------
198 -- Binary
199 ----------------------------------------------------------------------
201 instance Binary a => Binary (BooleanFormula a) where
202 put_ bh (Var x) = putByte bh 0 >> put_ bh x
203 put_ bh (And xs) = putByte bh 1 >> put_ bh xs
204 put_ bh (Or xs) = putByte bh 2 >> put_ bh xs
206 get bh = do
207 h <- getByte bh
208 case h of
209 0 -> Var <\$> get bh
210 1 -> And <\$> get bh
211 _ -> Or <\$> get bh