Added comments to BooleanFormula to explain the expression simplifier. (#7633)

1 files changed, 47 insertions, 3 deletions

diff --git a/compiler/utils/BooleanFormula.hs b/compiler/utils/BooleanFormula.hs
index 3e82e75b1f..8620ef555d 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)