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


-- | Normal form representation for boolean expressions. Typically simplifies such expressions, but is not guaranteed to produce the absolute simplest form.
--   
--   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


-- | Machinery for representing and simplifying simple propositional
--   formulas. Type families are used to maintain a simple normal form,
--   taking advantage of the duality between <a>And</a> and <a>Or</a>.
--   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.
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 <i>\
--   (a \</i> b) <a>-</a> a, or dually: a / (a / b) <a>-</a> 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 <i>\ b) \</i> (a <i>\ c) \</i> d <a>-</a> (a <i>\ (b \</i> 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
--   <a>polarity</a> and add handling of <a>not</a> to our simplification
--   tools.
data Ion a
Neg :: a -> Ion a
Pos :: a -> Ion a
qAtom :: Ord a => a -> QueryRep QAtomTyp (Ion a)
isEmptyQR, 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)

-- | a <i>\ (b \</i> ~b) <i>\ (c \</i> d) <a>-</a> a <i>\ (c \</i> d) a
--   <i>\ ~a </i> (b / c) <a>-</a> False (a / ~a) <i>\ (b \</i> ~b)
--   <a>-</a> True (*)
--   
--   and duals
--   
--   N.B. 0-ary / is False and 0-ary / is True
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