diff options
Diffstat (limited to 'compiler/utils')
| -rw-r--r-- | compiler/utils/BooleanFormula.hs | 50 |
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) |