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