boolsimplifier-0.1.5: Simplification tools for simple propositional formuals.

Stability experimental gershomb@gmail.com None

Data.BoolSimplifier

Description

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.

Synopsis

# Documentation

data QOrTyp Source

We'll start with three types of formulas: disjunctions, conjunctions, and atoms

Instances

 Show QOrTyp QNot QOrTyp PPConstQR QOrTyp Ord a => CombineQ a QAtomTyp QOrTyp Ord a => CombineQ a QOrTyp QAtomTyp Ord a => CombineQ a QOrTyp QOrTyp Ord a => CombineQ a QOrTyp QAndTyp Ord a => CombineQ a QAndTyp QOrTyp PPQueryRep (QueryRep QOrTyp (Ion String))

data QAndTyp Source

Instances

 Show QAndTyp QNot QAndTyp PPConstQR QAndTyp Ord a => CombineQ a QAtomTyp QAndTyp Ord a => CombineQ a QOrTyp QAndTyp Ord a => CombineQ a QAndTyp QAtomTyp Ord a => CombineQ a QAndTyp QOrTyp Ord a => CombineQ a QAndTyp QAndTyp PPQueryRep (QueryRep QAndTyp (Ion String))

data QAtomTyp Source

Instances

 QNot QAtomTyp HasClause fife QAtomTyp Ord a => CombineQ a QAtomTyp QAtomTyp Ord a => CombineQ a QAtomTyp QOrTyp Ord a => CombineQ a QAtomTyp QAndTyp Ord a => CombineQ a QOrTyp QAtomTyp Ord a => CombineQ a QAndTyp QAtomTyp PPQueryRep (QueryRep QAtomTyp (Ion String))

type family QFlipTyp t :: *Source

disjunction is the dual of conjunction and vice-versa

data QueryRep qtyp a whereSource

A formula is either an atom (of some type, e.g. `String`).

A non-atomic formula (which is either a disjunction or a conjunction) is n-ary and consists of a `Set` 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 `QFlipTyp` instance for `QAtomTyp`.

Constructors

 QAtom :: Ord a => a -> QueryRep QAtomTyp a QOp :: (Show qtyp, Ord a) => Set (QueryRep QAtomTyp a) -> Set (QueryRep (QFlipTyp qtyp) a) -> QueryRep qtyp a

Instances

 Eq a => Eq (QueryRep qtyp a) Ord a => Ord (QueryRep qtyp a) Show a => Show (QueryRep qtyp a) PPQueryRep (QueryRep qtyp String) PPQueryRep (QueryRep QAtomTyp (Ion String)) PPQueryRep (QueryRep QAndTyp (Ion String)) PPQueryRep (QueryRep QOrTyp (Ion String))

extractCs :: QueryRep qtyp a -> Set (QueryRep (QFlipTyp qtyp) a)Source

qOr :: Ord a => Set (QueryRep QAtomTyp a) -> Set (QueryRep QAndTyp a) -> QueryRep QOrTyp aSource

convenience constructors, not particularly smart

class PPQueryRep a whereSource

pretty printer class

Methods

ppQueryRep :: a -> StringSource

Instances

 PPQueryRep (QueryRep qtyp String) PPQueryRep (QueryRep QAtomTyp (Ion String)) PPQueryRep (QueryRep QAndTyp (Ion String)) PPQueryRep (QueryRep QOrTyp (Ion String))

qop :: (Ord a, Show qtyp, Show (QFlipTyp qtyp), QFlipTyp (QFlipTyp qtyp) ~ qtyp) => Set (QueryRep QAtomTyp a) -> Set (QueryRep (QFlipTyp qtyp) a) -> QueryRep qtyp aSource

smart constructor for `QOp` does following optimization: a \ (a \ b) - a, or dually: a / (a / b) - 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))Source

class HasClause fife qtyp whereSource

QueryReps can be queried for clauses within them, and clauses within them can be extracted.

Methods

hasClause :: QueryRep fife a -> QueryRep qtyp a -> BoolSource

stripClause :: QueryRep qtyp a -> QueryRep fife a -> QueryRep fife aSource

Instances

 ~ * (QFlipTyp fife) qtyp => HasClause fife qtyp HasClause fife QAtomTyp

andqs :: Ord a => CombineQ a qtyp QAndTyp => [QueryRep qtyp a] -> QueryRep QAndTyp aSource

convenience functions

orqs :: Ord a => CombineQ a qtyp QOrTyp => [QueryRep qtyp a] -> QueryRep QOrTyp aSource

class CombineQ a qtyp1 qtyp2 whereSource

smart constructors for `QueryRep`

Methods

andq :: QueryRep qtyp1 a -> QueryRep qtyp2 a -> QueryRep QAndTyp aSource

orq :: QueryRep qtyp1 a -> QueryRep qtyp2 a -> QueryRep QOrTyp aSource

Instances

 Ord a => CombineQ a QAtomTyp QAtomTyp Ord a => CombineQ a QAtomTyp QOrTyp Ord a => CombineQ a QAtomTyp QAndTyp Ord a => CombineQ a QOrTyp QAtomTyp Ord a => CombineQ a QOrTyp QOrTyp Ord a => CombineQ a QOrTyp QAndTyp Ord a => CombineQ a QAndTyp QAtomTyp Ord a => CombineQ a QAndTyp QOrTyp Ord a => CombineQ a QAndTyp QAndTyp

simplifyQueryRep :: (Ord a, Show (QFlipTyp qtyp), Show (QFlipTyp (QFlipTyp qtyp)), QFlipTyp (QFlipTyp qtyp) ~ qtyp) => QueryRep qtyp a -> QueryRep qtyp aSource

(a \ b) \ (a \ c) \ d - (a \ (b \ c)) / d (and also the dual)

getCommonClauseAs :: Ord a => Set (QueryRep fife a) -> Maybe (QueryRep QAtomTyp a, Set (QueryRep fife a), Set (QueryRep fife a))Source

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.

getCommonClauseCs :: Ord a => Set (QueryRep fife a) -> Maybe (QueryRep (QFlipTyp fife) a, Set (QueryRep fife a), Set (QueryRep fife a))Source

fixSimplifyQueryRep :: (QueryRep qtyp a -> QueryRep qtyp a) -> QueryRep qtyp a -> QueryRep qtyp aSource

Takes any given simplifier and repeatedly applies it until it ceases to reduce the size of the query reprepresentation.

data Ion a Source

We can wrap any underying atom dype in an Ion to give it a polarity and add handling of not to our simplification tools.

Constructors

 Neg a Pos a

Instances

 Eq a => Eq (Ion a) Ord a => Ord (Ion a) Show a => Show (Ion a) PPQueryRep (QueryRep QAtomTyp (Ion String)) PPQueryRep (QueryRep QAndTyp (Ion String)) PPQueryRep (QueryRep QOrTyp (Ion String))

class PPConstQR qtyp whereSource

Methods

ppConstQR :: QueryRep qtyp a -> StringSource

Instances

 PPConstQR a PPConstQR QAndTyp PPConstQR QOrTyp

class QNot qtyp whereSource

Associated Types

type QNeg qtyp Source

Methods

qNot :: QueryRep qtyp (Ion a) -> QueryRep (QNeg qtyp) (Ion a)Source

Instances

 QNot QAtomTyp QNot QAndTyp QNot QOrTyp

simplifyIons :: (Ord a, Show (QFlipTyp qtyp), QFlipTyp (QFlipTyp qtyp) ~ qtyp) => QueryRep qtyp (Ion a) -> QueryRep qtyp (Ion a)Source

a \ (b \ ~b) \ (c \ d) - a \ (c \ d) a \ ~a (b / c) - False (a / ~a) \ (b \ ~b) - True (*)

and duals

N.B. 0-ary / is False and 0-ary / is True

maximumByNote :: String -> (a -> a -> Ordering) -> [a] -> aSource