BooleanFormula.hs 8.08 KB
Newer Older
1 2
{-# LANGUAGE CPP #-}

3
--------------------------------------------------------------------------------
4 5 6 7 8
-- | 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.
--
9 10 11 12
{-# LANGUAGE DeriveDataTypeable, DeriveFunctor, DeriveFoldable,
             DeriveTraversable #-}

module BooleanFormula (
13
        BooleanFormula(..), LBooleanFormula,
14 15 16 17 18 19 20 21 22
        mkFalse, mkTrue, mkAnd, mkOr, mkVar,
        isFalse, isTrue,
        eval, simplify, isUnsatisfied,
        implies, impliesAtom,
        pprBooleanFormula, pprBooleanFormulaNice
  ) where

import Data.List ( nub, intersperse )
import Data.Data
23
#if __GLASGOW_HASKELL__ < 709
24 25
import Data.Foldable ( Foldable )
import Data.Traversable ( Traversable )
26
#endif
27 28 29 30

import MonadUtils
import Outputable
import Binary
31
import SrcLoc
32 33 34 35 36

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

37 38 39 40
type LBooleanFormula a = Located (BooleanFormula a)

data BooleanFormula a = Var a | And [LBooleanFormula a] | Or [LBooleanFormula a]
                      | Parens (LBooleanFormula a)
41 42 43 44 45 46 47 48 49
  deriving (Eq, Data, Typeable, Functor, Foldable, Traversable)

mkVar :: a -> BooleanFormula a
mkVar = Var

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

50
-- Convert a Bool to a BooleanFormula
51 52 53 54
mkBool :: Bool -> BooleanFormula a
mkBool False = mkFalse
mkBool True  = mkTrue

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

70
mkOr :: Eq a => [LBooleanFormula a] -> BooleanFormula a
71 72
mkOr = maybe mkTrue (mkOr' . nub) . concatMapM fromOr
  where
73
  -- See Note [Simplification of BooleanFormulas]
74 75
  fromOr (L _ (Or xs)) = Just xs
  fromOr (L _ (And [])) = Nothing
76
  fromOr x = Just [x]
77
  mkOr' [x] = unLoc x
78 79
  mkOr' xs = Or xs

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

{-
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 subexpresion 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 ()))
-}

115
----------------------------------------------------------------------
116
-- Evaluation and simplification
117 118 119 120 121 122 123 124 125 126 127 128
----------------------------------------------------------------------

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
129 130 131
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)
132 133 134 135 136 137 138

-- 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
139 140 141
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)
142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160

-- 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
161 162 163 164
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
165 166 167

implies :: Eq a => BooleanFormula a -> BooleanFormula a -> Bool
x `implies` Var y  = x `impliesAtom` y
168 169 170
x `implies` And ys = all (implies x . unLoc) ys
x `implies` Or ys  = any (implies x . unLoc) ys
x `implies` Parens y  = x `implies` (unLoc y)
171 172 173 174 175

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

176 177
-- Pretty print a BooleanFormula,
-- using the arguments as pretty printers for Var, And and Or respectively
178 179 180 181 182 183 184 185
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
186
  go p (And xs) = pprAnd p (map (go 3 . unLoc) xs)
187
  go _ (Or  []) = keyword $ text "FALSE"
188 189
  go p (Or  xs) = pprOr p (map (go 2 . unLoc) xs)
  go p (Parens x) = go p (unLoc x)
190 191 192 193 194 195

-- 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
196
  pprOr  p = cparen (p > 2) . fsep . intersperse vbar
197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216

-- 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 Outputable a => Outputable (BooleanFormula a) where
  pprPrec = pprBooleanFormula pprPrec

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

instance Binary a => Binary (BooleanFormula a) where
217 218 219 220
  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
221 222 223 224

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