Stability | experimental |
---|---|
Maintainer | gershomb@gmail.com |
Safe Haskell | None |
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.
- data QOrTyp
- data QAndTyp
- data QAtomTyp
- type family QFlipTyp t :: *
- data QueryRep qtyp a where
- extractAs :: QueryRep qtyp a -> Set (QueryRep QAtomTyp a)
- extractCs :: QueryRep qtyp a -> Set (QueryRep (QFlipTyp qtyp) a)
- 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
- class PPQueryRep a where
- ppQueryRep :: a -> String
- 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))
- class HasClause fife qtyp where
- 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
- class CombineQ a qtyp1 qtyp2 where
- simplifyQueryRep :: (Ord a, Show (QFlipTyp qtyp), Show (QFlipTyp (QFlipTyp qtyp)), QFlipTyp (QFlipTyp qtyp) ~ qtyp) => QueryRep qtyp a -> QueryRep qtyp a
- 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))
- fixSimplifyQueryRep :: (QueryRep qtyp a -> QueryRep qtyp a) -> QueryRep qtyp a -> QueryRep qtyp a
- data Ion a
- qAtom :: Ord a => a -> QueryRep QAtomTyp (Ion a)
- isEmptyQR, isConstQR :: QueryRep qtyp a -> Bool
- class PPConstQR qtyp where
- class QNot qtyp where
- 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
Documentation
We'll start with three types of formulas: disjunctions, conjunctions, and atoms
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
.
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
ppQueryRep :: a -> StringSource
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
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.
andqs :: Ord a => CombineQ a qtyp QAndTyp => [QueryRep qtyp a] -> QueryRep QAndTyp aSource
convenience functions
class CombineQ a qtyp1 qtyp2 whereSource
smart constructors for QueryRep
andq :: QueryRep qtyp1 a -> QueryRep qtyp2 a -> QueryRep QAndTyp aSource
orq :: QueryRep qtyp1 a -> QueryRep qtyp2 a -> QueryRep QOrTyp aSource
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.
simplifyIons :: (Ord a, Show (QFlipTyp qtyp), QFlipTyp (QFlipTyp qtyp) ~ qtyp) => QueryRep qtyp (Ion a) -> QueryRep qtyp (Ion a)Source
maximumByNote :: String -> (a -> a -> Ordering) -> [a] -> aSource