-- 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 :: a -> QueryRep QAtomTyp a
QOp :: 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 [overlap ok] Eq a => Eq (Ion a)
instance [overlap ok] Ord a => Ord (Ion a)
instance [overlap ok] Show a => Show (Ion a)
instance [overlap ok] QNot QAndTyp
instance [overlap ok] QNot QOrTyp
instance [overlap ok] QNot QAtomTyp
instance [overlap ok] PPConstQR a
instance [overlap ok] PPConstQR QOrTyp
instance [overlap ok] PPConstQR QAndTyp
instance [overlap ok] PPQueryRep (QueryRep QAtomTyp (Ion String))
instance [overlap ok] PPQueryRep (QueryRep QOrTyp (Ion String))
instance [overlap ok] PPQueryRep (QueryRep QAndTyp (Ion String))
instance [overlap ok] Ord a => CombineQ a QAtomTyp QAtomTyp
instance [overlap ok] Ord a => CombineQ a QAtomTyp QOrTyp
instance [overlap ok] Ord a => CombineQ a QAtomTyp QAndTyp
instance [overlap ok] Ord a => CombineQ a QOrTyp QAtomTyp
instance [overlap ok] Ord a => CombineQ a QOrTyp QOrTyp
instance [overlap ok] Ord a => CombineQ a QOrTyp QAndTyp
instance [overlap ok] Ord a => CombineQ a QAndTyp QAtomTyp
instance [overlap ok] Ord a => CombineQ a QAndTyp QOrTyp
instance [overlap ok] Ord a => CombineQ a QAndTyp QAndTyp
instance [overlap ok] QFlipTyp fife ~ qtyp => HasClause fife qtyp
instance [overlap ok] HasClause fife QAtomTyp
instance [overlap ok] PPQueryRep (QueryRep qtyp String)
instance [overlap ok] Show a => Show (QueryRep qtyp a)
instance [overlap ok] Ord a => Ord (QueryRep qtyp a)
instance [overlap ok] Eq a => Eq (QueryRep qtyp a)
instance [overlap ok] Show QAndTyp
instance [overlap ok] Show QOrTyp