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