[commit: ghc] master: Added comments to BooleanFormula to explain the expression simplifier. (#7633) (332eba9)
git at git.haskell.org
git at git.haskell.org
Tue Oct 15 20:51:49 UTC 2013
Repository : ssh://git@git.haskell.org/ghc
On branch : master
Link : http://ghc.haskell.org/trac/ghc/changeset/332eba9d3ff63365818310767a1766370343dcb0/ghc
>---------------------------------------------------------------
commit 332eba9d3ff63365818310767a1766370343dcb0
Author: Twan van Laarhoven <twanvl at gmail.com>
Date: Tue Oct 15 20:38:58 2013 +0100
Added comments to BooleanFormula to explain the expression simplifier. (#7633)
>---------------------------------------------------------------
332eba9d3ff63365818310767a1766370343dcb0
compiler/utils/BooleanFormula.hs | 50 +++++++++++++++++++++++++++++++++++---
1 file changed, 47 insertions(+), 3 deletions(-)
diff --git a/compiler/utils/BooleanFormula.hs b/compiler/utils/BooleanFormula.hs
index 3e82e75..8620ef5 100644
--- a/compiler/utils/BooleanFormula.hs
+++ b/compiler/utils/BooleanFormula.hs
@@ -1,6 +1,9 @@
--------------------------------------------------------------------------------
--- | Boolean formulas without negation (qunatifier free)
-
+-- | 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.
+--
{-# LANGUAGE DeriveDataTypeable, DeriveFunctor, DeriveFoldable,
DeriveTraversable #-}
@@ -36,13 +39,16 @@ 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 => [BooleanFormula a] -> BooleanFormula a
mkAnd = maybe mkFalse (mkAnd' . nub) . concatMapM fromAnd
where
+ -- See Note [Simplification of BooleanFormulas]
fromAnd :: BooleanFormula a -> Maybe [BooleanFormula a]
fromAnd (And xs) = Just xs
-- assume that xs are already simplified
@@ -55,14 +61,50 @@ mkAnd = maybe mkFalse (mkAnd' . nub) . concatMapM fromAnd
mkOr :: Eq a => [BooleanFormula a] -> BooleanFormula a
mkOr = maybe mkTrue (mkOr' . nub) . concatMapM fromOr
where
+ -- See Note [Simplification of BooleanFormulas]
fromOr (Or xs) = Just xs
fromOr (And []) = Nothing
fromOr x = Just [x]
mkOr' [x] = 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 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 ()))
+-}
+
----------------------------------------------------------------------
--- Evaluation and simplificiation
+-- Evaluation and simplification
----------------------------------------------------------------------
isFalse :: BooleanFormula a -> Bool
@@ -117,6 +159,8 @@ x `implies` Or ys = any (x `implies`) ys
-- 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)
More information about the ghc-commits
mailing list