Commit 332eba9d authored by twanvl's avatar twanvl Committed by Krzysztof Gogolewski

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

parent e5751265
--------------------------------------------------------------------------------
-- | 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)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment