-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Simplification tools for simple propositional formulas.
--   
--   Normal form representation for boolean expressions. Typically
--   simplifies such expressions, but is not guaranteed to produce the
--   absolute simplest form.
@package boolsimplifier
@version 0.1.8


-- | Machinery for representing and simplifying simple propositional
--   formulas. Type families are used to maintain a simple normal form,
--   taking advantage of the duality between "And" and "Or". Additional
--   tools are provided to pull out common atoms in subformulas and
--   otherwise iterate until a simplified fixpoint. Full and general
--   simplification is NP-hard, but the tools here can take typical
--   machine-generated formulas and perform most simplifications that could
--   be spotted and done by hand by a reasonable programmer.
--   
--   While there are many functions below, only <a>qAtom</a>,
--   <a>andq</a>(s), <a>orq</a>(s), and <a>qNot</a> need be used directly
--   to build expressions. <a>simplifyQueryRep</a> performs a basic
--   simplification, <a>simplifyIons</a> works on expressions with negation
--   to handle their reduction, and <a>fixSimplifyQueryRep</a> takes a
--   function built out of any combination of basic simplifiers (you can
--   write your own ones taking into account any special properties of your
--   atoms) and runs it repeatedly until it ceases to reduce the size of
--   your target expression.
--   
--   The general notion is either that you build up an expression with
--   these combinators directly, simplify it further, and then transform it
--   to a target semantics, or that an expression in some AST may be
--   converted into a normal form expression using such combinators, and
--   then simplified and transformed back to the original AST.
--   
--   Here are some simple interactions:
--   
--   <pre>
--   Prelude Data.BoolSimplifier&gt; (qAtom "A") `orq` (qAtom "B")
--   QOp | fromList [QAtom Pos "A",QAtom Pos "B"] fromList []
--   </pre>
--   
--   <pre>
--   Prelude Data.BoolSimplifier&gt; ppQueryRep $ (qAtom "A") `orq` (qAtom "B")
--   "(A | B)"
--   </pre>
--   
--   <pre>
--   Prelude Data.BoolSimplifier&gt; ppQueryRep $ ((qAtom "A") `orq` (qAtom "B") `andq` (qAtom "A"))
--   "(A)"
--   </pre>
--   
--   <pre>
--   Prelude Data.BoolSimplifier&gt; ppQueryRep $ ((qAtom "A") `orq` (qAtom "B") `andq` (qAtom "A" `orq` qAtom "C"))
--   "((A | B) &amp; (A | C))"
--   </pre>
--   
--   <pre>
--   Prelude Data.BoolSimplifier&gt; ppQueryRep $ simplifyQueryRep $ ((qAtom "A") `orq` (qAtom "B") `andq` (qAtom "A" `orq` qAtom "C"))
--   "((A | (B &amp; C)))"
--   </pre>
module Data.BoolSimplifier

-- | We'll start with three types of formulas: disjunctions, conjunctions,
--   and atoms
data QOrTyp
data QAndTyp
data QAtomTyp

-- | disjunction is the dual of conjunction and vice-versa

-- | A formula is either an atom (of some type, e.g. <tt>String</tt>).
--   
--   A non-atomic formula (which is either a disjunction or a conjunction)
--   is n-ary and consists of a <tt>Set</tt> of atoms and a set of
--   non-atomic subformulas of dual connective, i.e. the non-atomic
--   subformulas of a disjunction must all be conjunctions. The type system
--   enforces this since there is no <tt>QFlipTyp</tt> instance for
--   <tt>QAtomTyp</tt>.
data QueryRep qtyp a
[QAtom] :: (Ord a) => a -> QueryRep QAtomTyp a
[QOp] :: (Show qtyp, Ord a) => Set (QueryRep QAtomTyp a) -> Set (QueryRep (QFlipTyp qtyp) a) -> QueryRep qtyp a
extractAs :: QueryRep qtyp a -> Set (QueryRep QAtomTyp a)
extractCs :: QueryRep qtyp a -> Set (QueryRep (QFlipTyp qtyp) a)

-- | convenience constructors, not particularly smart
qOr :: Ord a => Set (QueryRep QAtomTyp a) -> Set (QueryRep QAndTyp a) -> QueryRep QOrTyp a
qAnd :: Ord a => Set (QueryRep QAtomTyp a) -> Set (QueryRep QOrTyp a) -> QueryRep QAndTyp a

-- | pretty printer class
class PPQueryRep a
ppQueryRep :: PPQueryRep a => a -> String

-- | smart constructor for <tt>QOp</tt> does following optimization: a /\
--   (a \/ b) &lt;-&gt; a, or dually: a \/ (a /\ b) &lt;-&gt; a
qop :: (Ord a, Show qtyp, Show (QFlipTyp qtyp), QFlipTyp (QFlipTyp qtyp) ~ qtyp) => Set (QueryRep QAtomTyp a) -> Set (QueryRep (QFlipTyp qtyp) a) -> QueryRep qtyp a
extractAtomCs :: (Ord a, Show qtyp, Show (QFlipTyp qtyp), QFlipTyp (QFlipTyp qtyp) ~ qtyp) => Set (QueryRep qtyp a) -> (Set (QueryRep qtyp a), Set (QueryRep QAtomTyp a))

-- | QueryReps can be queried for clauses within them, and clauses within
--   them can be extracted.
class HasClause fife qtyp
hasClause :: HasClause fife qtyp => QueryRep fife a -> QueryRep qtyp a -> Bool
stripClause :: HasClause fife qtyp => QueryRep qtyp a -> QueryRep fife a -> QueryRep fife a

-- | convenience functions
andqs :: Ord a => (CombineQ a qtyp QAndTyp) => [QueryRep qtyp a] -> QueryRep QAndTyp a
orqs :: Ord a => (CombineQ a qtyp QOrTyp) => [QueryRep qtyp a] -> QueryRep QOrTyp a

-- | smart constructors for <tt>QueryRep</tt>
class CombineQ a qtyp1 qtyp2
andq :: CombineQ a qtyp1 qtyp2 => QueryRep qtyp1 a -> QueryRep qtyp2 a -> QueryRep QAndTyp a
orq :: CombineQ a qtyp1 qtyp2 => QueryRep qtyp1 a -> QueryRep qtyp2 a -> QueryRep QOrTyp a

-- | (a /\ b) \/ (a /\ c) \/ d &lt;-&gt; (a /\ (b \/ c)) \/ d (and also the
--   dual)
simplifyQueryRep :: (Ord a, Show (QFlipTyp qtyp), Show (QFlipTyp (QFlipTyp qtyp)), QFlipTyp (QFlipTyp qtyp) ~ qtyp) => QueryRep qtyp a -> QueryRep qtyp a

-- | Given a set of QueryReps, extracts a common clause if possible,
--   returning the clause, the terms from which the clause has been
--   extracted, and the rest.
getCommonClauseAs :: Ord a => Set (QueryRep fife a) -> Maybe (QueryRep QAtomTyp a, Set (QueryRep fife a), Set (QueryRep fife a))
getCommonClauseCs :: Ord a => Set (QueryRep fife a) -> Maybe (QueryRep (QFlipTyp fife) a, Set (QueryRep fife a), Set (QueryRep fife a))

-- | Takes any given simplifier and repeatedly applies it until it ceases
--   to reduce the size of the query reprepresentation.
fixSimplifyQueryRep :: (QueryRep qtyp a -> QueryRep qtyp a) -> QueryRep qtyp a -> QueryRep qtyp a

-- | We can wrap any underying atom dype in an Ion to give it a "polarity"
--   and add handling of "not" to our simplification tools.
data Ion a
Neg :: a -> Ion a
Pos :: a -> Ion a
qAtom :: Ord a => a -> QueryRep QAtomTyp (Ion a)
isEmptyQR :: QueryRep qtyp a -> Bool
isConstQR :: QueryRep qtyp a -> Bool
class PPConstQR qtyp
ppConstQR :: PPConstQR qtyp => QueryRep qtyp a -> String
class QNot qtyp where {
    type family QNeg qtyp;
}
qNot :: QNot qtyp => QueryRep qtyp (Ion a) -> QueryRep (QNeg qtyp) (Ion a)

-- | <pre>
--   a  /\  (b \/ ~b)  /\  (c \/ d)   &lt;-&gt;   a /\ (c \/ d)
--   a  /\  ~a         /\  (b \/ c)   &lt;-&gt;   False
--          (a \/ ~a)  /\  (b \/ ~b)  &lt;-&gt;   True  (*)
--   </pre>
--   
--   and duals
--   
--   <pre>
--   N.B. 0-ary \/ is False and 0-ary /\ is True
--   </pre>
simplifyIons :: (Ord a, Show (QFlipTyp qtyp), QFlipTyp (QFlipTyp qtyp) ~ qtyp) => QueryRep qtyp (Ion a) -> QueryRep qtyp (Ion a)
maximumByNote :: String -> (a -> a -> Ordering) -> [a] -> a
instance GHC.Show.Show a => GHC.Show.Show (Data.BoolSimplifier.Ion a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Data.BoolSimplifier.Ion a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Data.BoolSimplifier.Ion a)
instance Data.BoolSimplifier.QNot Data.BoolSimplifier.QAtomTyp
instance Data.BoolSimplifier.QNot Data.BoolSimplifier.QOrTyp
instance Data.BoolSimplifier.QNot Data.BoolSimplifier.QAndTyp
instance Data.BoolSimplifier.PPQueryRep (Data.BoolSimplifier.QueryRep Data.BoolSimplifier.QAndTyp (Data.BoolSimplifier.Ion GHC.Base.String))
instance Data.BoolSimplifier.PPQueryRep (Data.BoolSimplifier.QueryRep Data.BoolSimplifier.QOrTyp (Data.BoolSimplifier.Ion GHC.Base.String))
instance Data.BoolSimplifier.PPConstQR Data.BoolSimplifier.QAndTyp
instance Data.BoolSimplifier.PPConstQR Data.BoolSimplifier.QOrTyp
instance Data.BoolSimplifier.PPConstQR a
instance Data.BoolSimplifier.PPQueryRep (Data.BoolSimplifier.QueryRep Data.BoolSimplifier.QAtomTyp (Data.BoolSimplifier.Ion GHC.Base.String))
instance GHC.Classes.Ord a => Data.BoolSimplifier.CombineQ a Data.BoolSimplifier.QAndTyp Data.BoolSimplifier.QAndTyp
instance GHC.Classes.Ord a => Data.BoolSimplifier.CombineQ a Data.BoolSimplifier.QAndTyp Data.BoolSimplifier.QOrTyp
instance GHC.Classes.Ord a => Data.BoolSimplifier.CombineQ a Data.BoolSimplifier.QAndTyp Data.BoolSimplifier.QAtomTyp
instance GHC.Classes.Ord a => Data.BoolSimplifier.CombineQ a Data.BoolSimplifier.QOrTyp Data.BoolSimplifier.QAndTyp
instance GHC.Classes.Ord a => Data.BoolSimplifier.CombineQ a Data.BoolSimplifier.QOrTyp Data.BoolSimplifier.QOrTyp
instance GHC.Classes.Ord a => Data.BoolSimplifier.CombineQ a Data.BoolSimplifier.QOrTyp Data.BoolSimplifier.QAtomTyp
instance GHC.Classes.Ord a => Data.BoolSimplifier.CombineQ a Data.BoolSimplifier.QAtomTyp Data.BoolSimplifier.QAndTyp
instance GHC.Classes.Ord a => Data.BoolSimplifier.CombineQ a Data.BoolSimplifier.QAtomTyp Data.BoolSimplifier.QOrTyp
instance GHC.Classes.Ord a => Data.BoolSimplifier.CombineQ a Data.BoolSimplifier.QAtomTyp Data.BoolSimplifier.QAtomTyp
instance Data.BoolSimplifier.HasClause fife Data.BoolSimplifier.QAtomTyp
instance Data.BoolSimplifier.QFlipTyp fife ~ qtyp => Data.BoolSimplifier.HasClause fife qtyp
instance Data.BoolSimplifier.PPQueryRep (Data.BoolSimplifier.QueryRep qtyp GHC.Base.String)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Data.BoolSimplifier.QueryRep qtyp a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Data.BoolSimplifier.QueryRep qtyp a)
instance GHC.Show.Show a => GHC.Show.Show (Data.BoolSimplifier.QueryRep qtyp a)
instance GHC.Show.Show Data.BoolSimplifier.QAndTyp
instance GHC.Show.Show Data.BoolSimplifier.QOrTyp
