summaryrefslogtreecommitdiff
path: root/compiler/utils/BooleanFormula.hs
blob: a42bb90a1cd97fb2f86de5761fe6620951202306 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
{-# LANGUAGE DeriveDataTypeable, DeriveFunctor, DeriveFoldable,
             DeriveTraversable #-}

--------------------------------------------------------------------------------
-- | Boolean formulas without quantifiers and without negation.
-- Such a formula consists of variables, conjunctions (and), and disjunctions (or).
--
-- This module is used to represent minimal complete definitions for classes.
--
module BooleanFormula (
        BooleanFormula(..), LBooleanFormula,
        mkFalse, mkTrue, mkAnd, mkOr, mkVar,
        isFalse, isTrue,
        eval, simplify, isUnsatisfied,
        implies, impliesAtom,
        pprBooleanFormula, pprBooleanFormulaNice
  ) where

import GhcPrelude

import Data.List ( nub, intersperse )
import Data.Data

import MonadUtils
import Outputable
import Binary
import SrcLoc
import Unique
import UniqSet

----------------------------------------------------------------------
-- Boolean formula type and smart constructors
----------------------------------------------------------------------

type LBooleanFormula a = Located (BooleanFormula a)

data BooleanFormula a = Var a | And [LBooleanFormula a] | Or [LBooleanFormula a]
                      | Parens (LBooleanFormula a)
  deriving (Eq, Data, Functor, Foldable, Traversable)

mkVar :: a -> BooleanFormula a
mkVar = Var

mkFalse, mkTrue :: BooleanFormula a
mkFalse = Or []
mkTrue = And []

-- Convert a Bool to a BooleanFormula
mkBool :: Bool -> BooleanFormula a
mkBool False = mkFalse
mkBool True  = mkTrue

-- Make a conjunction, and try to simplify
mkAnd :: Eq a => [LBooleanFormula a] -> BooleanFormula a
mkAnd = maybe mkFalse (mkAnd' . nub) . concatMapM fromAnd
  where
  -- See Note [Simplification of BooleanFormulas]
  fromAnd :: LBooleanFormula a -> Maybe [LBooleanFormula a]
  fromAnd (L _ (And xs)) = Just xs
     -- assume that xs are already simplified
     -- otherwise we would need: fromAnd (And xs) = concat <$> traverse fromAnd xs
  fromAnd (L _ (Or [])) = Nothing
     -- in case of False we bail out, And [..,mkFalse,..] == mkFalse
  fromAnd x = Just [x]
  mkAnd' [x] = unLoc x
  mkAnd' xs = And xs

mkOr :: Eq a => [LBooleanFormula a] -> BooleanFormula a
mkOr = maybe mkTrue (mkOr' . nub) . concatMapM fromOr
  where
  -- See Note [Simplification of BooleanFormulas]
  fromOr (L _ (Or xs)) = Just xs
  fromOr (L _ (And [])) = Nothing
  fromOr x = Just [x]
  mkOr' [x] = unLoc x
  mkOr' xs = Or xs


{-
Note [Simplification of BooleanFormulas]
~~~~~~~~~~~~~~~~~~~~~~
The smart constructors (`mkAnd` and `mkOr`) do some attempt to simplify expressions. In particular,
 1. Collapsing nested ands and ors, so
     `(mkAnd [x, And [y,z]]`
    is represented as
     `And [x,y,z]`
    Implemented by `fromAnd`/`fromOr`
 2. Collapsing trivial ands and ors, so
     `mkAnd [x]` becomes just `x`.
    Implemented by mkAnd' / mkOr'
 3. Conjunction with false, disjunction with true is simplified, i.e.
     `mkAnd [mkFalse,x]` becomes `mkFalse`.
 4. Common subexpression elimination:
     `mkAnd [x,x,y]` is reduced to just `mkAnd [x,y]`.

This simplification is not exhaustive, in the sense that it will not produce
the smallest possible equivalent expression. For example,
`Or [And [x,y], And [x]]` could be simplified to `And [x]`, but it currently
is not. A general simplifier would need to use something like BDDs.

The reason behind the (crude) simplifier is to make for more user friendly
error messages. E.g. for the code
  > class Foo a where
  >     {-# MINIMAL bar, (foo, baq | foo, quux) #-}
  > instance Foo Int where
  >     bar = ...
  >     baz = ...
  >     quux = ...
We don't show a ridiculous error message like
    Implement () and (either (`foo' and ()) or (`foo' and ()))
-}

----------------------------------------------------------------------
-- Evaluation and simplification
----------------------------------------------------------------------

isFalse :: BooleanFormula a -> Bool
isFalse (Or []) = True
isFalse _ = False

isTrue :: BooleanFormula a -> Bool
isTrue (And []) = True
isTrue _ = False

eval :: (a -> Bool) -> BooleanFormula a -> Bool
eval f (Var x)  = f x
eval f (And xs) = all (eval f . unLoc) xs
eval f (Or xs)  = any (eval f . unLoc) xs
eval f (Parens x) = eval f (unLoc x)

-- Simplify a boolean formula.
-- The argument function should give the truth of the atoms, or Nothing if undecided.
simplify :: Eq a => (a -> Maybe Bool) -> BooleanFormula a -> BooleanFormula a
simplify f (Var a) = case f a of
  Nothing -> Var a
  Just b  -> mkBool b
simplify f (And xs) = mkAnd (map (\(L l x) -> L l (simplify f x)) xs)
simplify f (Or xs) = mkOr (map (\(L l x) -> L l (simplify f x)) xs)
simplify f (Parens x) = simplify f (unLoc x)

-- Test if a boolean formula is satisfied when the given values are assigned to the atoms
-- if it is, returns Nothing
-- if it is not, return (Just remainder)
isUnsatisfied :: Eq a => (a -> Bool) -> BooleanFormula a -> Maybe (BooleanFormula a)
isUnsatisfied f bf
    | isTrue bf' = Nothing
    | otherwise  = Just bf'
  where
  f' x = if f x then Just True else Nothing
  bf' = simplify f' bf

-- prop_simplify:
--   eval f x == True   <==>  isTrue  (simplify (Just . f) x)
--   eval f x == False  <==>  isFalse (simplify (Just . f) x)

-- If the boolean formula holds, does that mean that the given atom is always true?
impliesAtom :: Eq a => BooleanFormula a -> a -> Bool
Var x  `impliesAtom` y = x == y
And xs `impliesAtom` y = any (\x -> (unLoc x) `impliesAtom` y) xs
           -- we have all of xs, so one of them implying y is enough
Or  xs `impliesAtom` y = all (\x -> (unLoc x) `impliesAtom` y) xs
Parens x `impliesAtom` y = (unLoc x) `impliesAtom` y

implies :: Uniquable a => BooleanFormula a -> BooleanFormula a -> Bool
implies e1 e2 = go (Clause emptyUniqSet [e1]) (Clause emptyUniqSet [e2])
  where
    go :: Uniquable a => Clause a -> Clause a -> Bool
    go l@Clause{ clauseExprs = hyp:hyps } r =
        case hyp of
            Var x | memberClauseAtoms x r -> True
                  | otherwise -> go (extendClauseAtoms l x) { clauseExprs = hyps } r
            Parens hyp' -> go l { clauseExprs = unLoc hyp':hyps }     r
            And hyps'  -> go l { clauseExprs = map unLoc hyps' ++ hyps } r
            Or hyps'   -> all (\hyp' -> go l { clauseExprs = unLoc hyp':hyps } r) hyps'
    go l r@Clause{ clauseExprs = con:cons } =
        case con of
            Var x | memberClauseAtoms x l -> True
                  | otherwise -> go l (extendClauseAtoms r x) { clauseExprs = cons }
            Parens con' -> go l r { clauseExprs = unLoc con':cons }
            And cons'   -> all (\con' -> go l r { clauseExprs = unLoc con':cons }) cons'
            Or cons'    -> go l r { clauseExprs = map unLoc cons' ++ cons }
    go _ _ = False

-- A small sequent calculus proof engine.
data Clause a = Clause {
        clauseAtoms :: UniqSet a,
        clauseExprs :: [BooleanFormula a]
    }
extendClauseAtoms :: Uniquable a => Clause a -> a -> Clause a
extendClauseAtoms c x = c { clauseAtoms = addOneToUniqSet (clauseAtoms c) x }

memberClauseAtoms :: Uniquable a => a -> Clause a -> Bool
memberClauseAtoms x c = x `elementOfUniqSet` clauseAtoms c

----------------------------------------------------------------------
-- Pretty printing
----------------------------------------------------------------------

-- Pretty print a BooleanFormula,
-- using the arguments as pretty printers for Var, And and Or respectively
pprBooleanFormula' :: (Rational -> a -> SDoc)
                   -> (Rational -> [SDoc] -> SDoc)
                   -> (Rational -> [SDoc] -> SDoc)
                   -> Rational -> BooleanFormula a -> SDoc
pprBooleanFormula' pprVar pprAnd pprOr = go
  where
  go p (Var x)  = pprVar p x
  go p (And []) = cparen (p > 0) $ empty
  go p (And xs) = pprAnd p (map (go 3 . unLoc) xs)
  go _ (Or  []) = keyword $ text "FALSE"
  go p (Or  xs) = pprOr p (map (go 2 . unLoc) xs)
  go p (Parens x) = go p (unLoc x)

-- Pretty print in source syntax, "a | b | c,d,e"
pprBooleanFormula :: (Rational -> a -> SDoc) -> Rational -> BooleanFormula a -> SDoc
pprBooleanFormula pprVar = pprBooleanFormula' pprVar pprAnd pprOr
  where
  pprAnd p = cparen (p > 3) . fsep . punctuate comma
  pprOr  p = cparen (p > 2) . fsep . intersperse vbar

-- Pretty print human in readable format, "either `a' or `b' or (`c', `d' and `e')"?
pprBooleanFormulaNice :: Outputable a => BooleanFormula a -> SDoc
pprBooleanFormulaNice = pprBooleanFormula' pprVar pprAnd pprOr 0
  where
  pprVar _ = quotes . ppr
  pprAnd p = cparen (p > 1) . pprAnd'
  pprAnd' [] = empty
  pprAnd' [x,y] = x <+> text "and" <+> y
  pprAnd' xs@(_:_) = fsep (punctuate comma (init xs)) <> text ", and" <+> last xs
  pprOr p xs = cparen (p > 1) $ text "either" <+> sep (intersperse (text "or") xs)

instance (OutputableBndr a) => Outputable (BooleanFormula a) where
  ppr = pprBooleanFormulaNormal

pprBooleanFormulaNormal :: (OutputableBndr a)
                        => BooleanFormula a -> SDoc
pprBooleanFormulaNormal = go
  where
    go (Var x)    = pprPrefixOcc x
    go (And xs)   = fsep $ punctuate comma (map (go . unLoc) xs)
    go (Or [])    = keyword $ text "FALSE"
    go (Or xs)    = fsep $ intersperse vbar (map (go . unLoc) xs)
    go (Parens x) = parens (go $ unLoc x)


----------------------------------------------------------------------
-- Binary
----------------------------------------------------------------------

instance Binary a => Binary (BooleanFormula a) where
  put_ bh (Var x)    = putByte bh 0 >> put_ bh x
  put_ bh (And xs)   = putByte bh 1 >> put_ bh xs
  put_ bh (Or  xs)   = putByte bh 2 >> put_ bh xs
  put_ bh (Parens x) = putByte bh 3 >> put_ bh x

  get bh = do
    h <- getByte bh
    case h of
      0 -> Var    <$> get bh
      1 -> And    <$> get bh
      2 -> Or     <$> get bh
      _ -> Parens <$> get bh