{-# LANGUAGE DeriveDataTypeable, DeriveFunctor, DeriveFoldable,
 DeriveTraversable #-}---------------------------------------------------------------------------------- | 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.--moduleBooleanFormula(BooleanFormula (..),LBooleanFormula ,mkFalse ,mkTrue ,mkAnd ,mkOr ,mkVar ,isFalse ,isTrue ,eval ,simplify ,isUnsatisfied ,implies ,impliesAtom ,pprBooleanFormula ,pprBooleanFormulaNice )whereimportGhcPrelude importData.List(nub,intersperse)importData.DataimportMonadUtils importOutputable importBinary importSrcLoc importUnique importUniqSet ------------------------------------------------------------------------ Boolean formula type and smart constructors----------------------------------------------------------------------typeLBooleanFormula a =Located (BooleanFormula a )dataBooleanFormula a =Var a |And [LBooleanFormula a ]|Or [LBooleanFormula a ]|Parens (LBooleanFormula a )deriving(Eq,Data,Functor,Foldable,Traversable)mkVar::a ->BooleanFormula a mkVar =Var mkFalse,mkTrue::BooleanFormula a mkFalse =Or []mkTrue =And []-- Convert a Bool to a BooleanFormulamkBool::Bool->BooleanFormula a mkBool False=mkFalse mkBoolTrue=mkTrue -- Make a conjunction, and try to simplifymkAnd::Eqa =>[LBooleanFormula a ]->BooleanFormula a mkAnd =maybemkFalse (mkAnd' .nub).concatMapM fromAnd where-- See Note [Simplification of BooleanFormulas]fromAnd::LBooleanFormula a ->Maybe[LBooleanFormula a ]fromAnd (L _(And xs ))=Justxs -- assume that xs are already simplified-- otherwise we would need: fromAnd (And xs) = concat <$> traverse fromAnd xsfromAnd(L _(Or []))=Nothing-- in case of False we bail out, And [..,mkFalse,..] == mkFalsefromAndx =Just[x ]mkAnd' [x ]=unLoc x mkAnd'xs =And xs mkOr::Eqa =>[LBooleanFormula a ]->BooleanFormula a mkOr =maybemkTrue (mkOr' .nub).concatMapM fromOr where-- See Note [Simplification of BooleanFormulas]fromOr (L _(Or xs ))=Justxs fromOr(L _(And []))=NothingfromOrx =Just[x ]mkOr' [x ]=unLoc 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 subexpression 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 simplification----------------------------------------------------------------------isFalse::BooleanFormula a ->BoolisFalse (Or [])=TrueisFalse_=FalseisTrue::BooleanFormula a ->BoolisTrue (And [])=TrueisTrue_=Falseeval::(a ->Bool)->BooleanFormula a ->Booleval f (Var x )=f x evalf (And xs )=all(eval f .unLoc )xs evalf (Or xs )=any(eval f .unLoc )xs evalf (Parens x )=eval f (unLoc x )-- Simplify a boolean formula.-- The argument function should give the truth of the atoms, or Nothing if undecided.simplify::Eqa =>(a ->MaybeBool)->BooleanFormula a ->BooleanFormula a simplify f (Var a )=casef a ofNothing->Var a Justb ->mkBool b simplifyf (And xs )=mkAnd (map(\(L l x )->L l (simplify f x ))xs )simplifyf (Or xs )=mkOr (map(\(L l x )->L l (simplify f x ))xs )simplifyf (Parens x )=simplify f (unLoc x )-- Test if a boolean formula is satisfied when the given values are assigned to the atoms-- if it is, returns Nothing-- if it is not, return (Just remainder)isUnsatisfied::Eqa =>(a ->Bool)->BooleanFormula a ->Maybe(BooleanFormula a )isUnsatisfied f bf |isTrue bf' =Nothing|otherwise=Justbf' wheref' x =iff x thenJustTrueelseNothingbf' =simplify f' bf -- prop_simplify:-- eval f x == True <==> isTrue (simplify (Just . f) x)-- eval f x == False <==> isFalse (simplify (Just . f) x)-- If the boolean formula holds, does that mean that the given atom is always true?impliesAtom::Eqa =>BooleanFormula a ->a ->BoolVar x `impliesAtom `y =x ==y And xs `impliesAtom`y =any(\x ->(unLoc x )`impliesAtom `y )xs -- we have all of xs, so one of them implying y is enoughOr xs `impliesAtom`y =all(\x ->(unLoc x )`impliesAtom `y )xs Parens x `impliesAtom`y =(unLoc x )`impliesAtom `y implies::Uniquable a =>BooleanFormula a ->BooleanFormula a ->Boolimplies e1 e2 =go (Clause emptyUniqSet [e1 ])(Clause emptyUniqSet [e2 ])wherego::Uniquable a =>Clause a ->Clause a ->Boolgo l @Clause {clauseExprs=hyp :hyps }r =casehyp ofVar x |memberClauseAtoms x r ->True|otherwise->go (extendClauseAtoms l x ){clauseExprs=hyps }r Parens hyp' ->go l {clauseExprs=unLoc hyp' :hyps }r And hyps' ->go l {clauseExprs=mapunLoc hyps' ++hyps }r Or hyps' ->all(\hyp' ->go l {clauseExprs=unLoc hyp' :hyps }r )hyps' gol r @Clause {clauseExprs=con :cons }=casecon ofVar x |memberClauseAtoms x l ->True|otherwise->go l (extendClauseAtoms r x ){clauseExprs=cons }Parens con' ->go l r {clauseExprs=unLoc con' :cons }And cons' ->all(\con' ->go l r {clauseExprs=unLoc con' :cons })cons' Or cons' ->go l r {clauseExprs=mapunLoc cons' ++cons }go__=False-- A small sequent calculus proof engine.dataClause a =Clause {clauseAtoms ::UniqSet a ,clauseExprs ::[BooleanFormula a ]}extendClauseAtoms::Uniquable a =>Clause a ->a ->Clause a extendClauseAtoms c x =c {clauseAtoms=addOneToUniqSet (clauseAtomsc )x }memberClauseAtoms::Uniquable a =>a ->Clause a ->BoolmemberClauseAtoms x c =x `elementOfUniqSet `clauseAtomsc ------------------------------------------------------------------------ Pretty printing------------------------------------------------------------------------ Pretty print a BooleanFormula,-- using the arguments as pretty printers for Var, And and Or respectivelypprBooleanFormula'::(Rational->a ->SDoc )->(Rational->[SDoc ]->SDoc )->(Rational->[SDoc ]->SDoc )->Rational->BooleanFormula a ->SDoc pprBooleanFormula' pprVar pprAnd pprOr =go wherego p (Var x )=pprVar p x gop (And [])=cparen (p >0)$empty gop (And xs )=pprAnd p (map(go 3.unLoc )xs )go_(Or [])=keyword $text "FALSE"gop (Or xs )=pprOr p (map(go 2.unLoc )xs )gop (Parens x )=go p (unLoc x )-- Pretty print in source syntax, "a | b | c,d,e"pprBooleanFormula::(Rational->a ->SDoc )->Rational->BooleanFormula a ->SDoc pprBooleanFormula pprVar =pprBooleanFormula' pprVar pprAnd pprOr wherepprAnd p =cparen (p >3).fsep .punctuate comma pprOr p =cparen (p >2).fsep .interspersevbar -- Pretty print human in readable format, "either `a' or `b' or (`c', `d' and `e')"?pprBooleanFormulaNice::Outputable a =>BooleanFormula a ->SDoc pprBooleanFormulaNice =pprBooleanFormula' pprVar pprAnd pprOr 0wherepprVar _=quotes .ppr pprAnd p =cparen (p >1).pprAnd' pprAnd' []=empty pprAnd'[x ,y ]=x <+> text "and"<+> y pprAnd'xs @(_:_)=fsep (punctuate comma (initxs ))<> text ", and"<+> lastxs pprOr p xs =cparen (p >1)$text "either"<+> sep (intersperse(text "or")xs )instance(OutputableBndr a )=>Outputable (BooleanFormula a )whereppr =pprBooleanFormulaNormal pprBooleanFormulaNormal::(OutputableBndr a )=>BooleanFormula a ->SDoc pprBooleanFormulaNormal =go wherego (Var x )=pprPrefixOcc x go(And xs )=fsep $punctuate comma (map(go .unLoc )xs )go(Or [])=keyword $text "FALSE"go(Or xs )=fsep $interspersevbar (map(go .unLoc )xs )go(Parens x )=parens (go $unLoc x )------------------------------------------------------------------------ Binary----------------------------------------------------------------------instanceBinary a =>Binary (BooleanFormula a )whereput_ bh (Var x )=putByte bh 0>>put_ bh x put_bh (And xs )=putByte bh 1>>put_ bh xs put_bh (Or xs )=putByte bh 2>>put_ bh xs put_bh (Parens x )=putByte bh 3>>put_ bh x get bh =doh <-getByte bh caseh of0->Var <$>get bh 1->And <$>get bh 2->Or <$>get bh _->Parens <$>get bh