From 332eba9d3ff63365818310767a1766370343dcb0 Mon Sep 17 00:00:00 2001
From: Twan van Laarhoven
Date: Tue, 15 Oct 2013 20:38:58 +0100
Subject: [PATCH] Added comments to BooleanFormula to explain the expression
simplifier. (#7633)

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 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)

GitLab