utils: detabify/dewhitespace GraphPpr
[ghc.git] / compiler / utils / BooleanFormula.hs
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 #-}
9
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
18
19 import Data.List ( nub, intersperse )
20 import Data.Data
21 import Data.Foldable ( Foldable )
22 import Data.Traversable ( Traversable )
23
24 import MonadUtils
25 import Outputable
26 import Binary
27
28 ----------------------------------------------------------------------
29 -- Boolean formula type and smart constructors
30 ----------------------------------------------------------------------
31
32 data BooleanFormula a = Var a | And [BooleanFormula a] | Or [BooleanFormula a]
33 deriving (Eq, Data, Typeable, Functor, Foldable, Traversable)
34
35 mkVar :: a -> BooleanFormula a
36 mkVar = Var
37
38 mkFalse, mkTrue :: BooleanFormula a
39 mkFalse = Or []
40 mkTrue = And []
41
42 -- Convert a Bool to a BooleanFormula
43 mkBool :: Bool -> BooleanFormula a
44 mkBool False = mkFalse
45 mkBool True = mkTrue
46
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
60
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
70
71
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]`.
88
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.
93
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 -}
105
106 ----------------------------------------------------------------------
107 -- Evaluation and simplification
108 ----------------------------------------------------------------------
109
110 isFalse :: BooleanFormula a -> Bool
111 isFalse (Or []) = True
112 isFalse _ = False
113
114 isTrue :: BooleanFormula a -> Bool
115 isTrue (And []) = True
116 isTrue _ = False
117
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
122
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)
131
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
142
143 -- prop_simplify:
144 -- eval f x == True <==> isTrue (simplify (Just . f) x)
145 -- eval f x == False <==> isFalse (simplify (Just . f) x)
146
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
152
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
157
158 ----------------------------------------------------------------------
159 -- Pretty printing
160 ----------------------------------------------------------------------
161
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)
175
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 "|")
182
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)
193
194 instance Outputable a => Outputable (BooleanFormula a) where
195 pprPrec = pprBooleanFormula pprPrec
196
197 ----------------------------------------------------------------------
198 -- Binary
199 ----------------------------------------------------------------------
200
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
205
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