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


-- | Boolean normal form: NNF, DNF & CNF
--   
--   The provided types that might be useful in symbolic manipulation of
--   propositional logic expressions.
@package boolean-normal-forms
@version 0.0.0.1


module Data.Algebra.Boolean.CoBoolean

-- | A class to values translable to booleans.
class CoBoolean a
toBoolean :: (CoBoolean a, Boolean b) => a -> b

-- | A polymorphic class of values translable to booleans.
class CoBoolean1 b
toBooleanWith :: (CoBoolean1 b, Boolean c) => (a -> c) -> b a -> c

-- | Less polymorphic version of <a>toBoolean</a>.
toBool :: CoBoolean a => a -> Bool

-- | Less polymorphic version of <a>toBooleanWith</a>.
toBoolWith :: CoBoolean1 b => (a -> Bool) -> b a -> Bool
instance CoBoolean1 Maybe
instance CoBoolean (Maybe a)
instance (CoBoolean f, CoBoolean g) => CoBoolean (Either f g)
instance CoBoolean Bool


module Data.Algebra.Boolean.Negable

-- | Free <a>Negable</a>.
data Neg a

-- | Positive value
Pos :: a -> Neg a

-- | Negative value
Neg :: a -> Neg a

-- | Class to represent invertible values.
--   
--   Must obey the double negation law: <tt>not (not x) = x</tt>
--   
--   The negation appears only in leafs of normal forms, and the underlying
--   proposition class might have built-in negation, thus we use
--   <a>Negable</a>.
class Negable x
not :: Negable x => x -> x
instance Typeable1 Neg
instance Eq a => Eq (Neg a)
instance Ord a => Ord (Neg a)
instance Show a => Show (Neg a)
instance Read a => Read (Neg a)
instance Functor Neg
instance (Negable a, Negable b) => Negable (Either a b)
instance (Negable a, Negable b) => Negable (a, b)
instance Monoid m => Negable (Maybe m)
instance Negable Bool
instance Negable (Neg a)
instance CoBoolean1 Neg
instance CoBoolean (Neg a)


module Data.Algebra.Boolean.FreeBoolean

-- | Free <a>Boolean</a> type, does not perform any optimizations on the
--   structure. Useful only in tests.
--   
--   Consider using <a>NNF</a>.
data FreeBoolean a
FBValue :: a -> FreeBoolean a
FBTrue :: FreeBoolean a
FBFalse :: FreeBoolean a
FBNot :: (FreeBoolean a) -> FreeBoolean a
FBAnd :: (FreeBoolean a) -> (FreeBoolean a) -> FreeBoolean a
FBOr :: (FreeBoolean a) -> (FreeBoolean a) -> FreeBoolean a
instance Typeable1 FreeBoolean
instance Eq a => Eq (FreeBoolean a)
instance Ord a => Ord (FreeBoolean a)
instance Show a => Show (FreeBoolean a)
instance Read a => Read (FreeBoolean a)
instance Functor FreeBoolean
instance Boolean (FreeBoolean a)
instance Negable (FreeBoolean a)
instance CoBoolean a => CoBoolean (FreeBoolean a)
instance CoBoolean1 FreeBoolean


module Data.Algebra.Boolean.NormalForm

-- | Class unifying different boolean normal forms.
class CoBoolean1 nf => NormalForm nf where type family NFConstraint nf a :: Constraint type instance NFConstraint nf a = ()
toNormalForm :: NormalForm nf => a -> nf a
simplify :: (NormalForm nf, NFConstraint nf a) => (a -> Maybe Bool) -> nf a -> nf a
fromFreeBoolean :: (NormalForm nf, NFConstraint nf a) => FreeBoolean a -> nf a
instance NormalForm FreeBoolean


module Data.Algebra.Boolean.NNF.Tree

-- | Boolean formula in Negation Normal Form
--   
--   <a>Boolean</a> operations will perform transformations as below:
--   
data NNF a
NNFTrue :: NNF a
NNFFalse :: NNF a
NNFValue :: a -> NNF a
NNFOr :: (NNF a) -> (NNF a) -> NNF a
NNFAnd :: (NNF a) -> (NNF a) -> NNF a
instance Typeable1 NNF
instance Eq a => Eq (NNF a)
instance Ord a => Ord (NNF a)
instance Show a => Show (NNF a)
instance Read a => Read (NNF a)
instance Functor NNF
instance NormalForm NNF
instance Negable a => Boolean (NNF a)
instance Negable a => Negable (NNF a)
instance CoBoolean1 NNF
instance CoBoolean a => CoBoolean (NNF a)


-- | This module re-exports tree-based implementation.
module Data.Algebra.Boolean.NNF


module Data.Algebra.Boolean.DNF.Set

-- | Boolean formula in Disjunction Normal Form
--   
newtype DNF a
DNF :: Set (Set a) -> DNF a
unDNF :: DNF a -> Set (Set a)
fromDoubleList :: Ord a => [[a]] -> DNF a
toDoubleList :: DNF a -> [[a]]
fromNNF :: (Ord a, Negable a) => NNF a -> DNF a
instance Typeable1 DNF
instance Eq a => Eq (DNF a)
instance Ord a => Ord (DNF a)
instance Show a => Show (DNF a)
instance (Ord a, Read a) => Read (DNF a)
instance NormalForm DNF
instance (Ord a, Negable a) => Boolean (DNF a)
instance (Ord a, Negable a) => Negable (DNF a)
instance CoBoolean a => CoBoolean (DNF a)
instance CoBoolean1 DNF


-- | This module re-exports <tt>Set</tt>-based implementation.
module Data.Algebra.Boolean.DNF


module Data.Algebra.Boolean.CNF.Set

-- | Boolean formula in Conjunction Normal Form
--   
newtype CNF a
CNF :: Set (Set a) -> CNF a
unCNF :: CNF a -> Set (Set a)
fromDoubleList :: Ord a => [[a]] -> CNF a
toDoubleList :: CNF a -> [[a]]
fromNNF :: (Ord a, Negable a) => NNF a -> CNF a
instance Typeable1 CNF
instance Eq a => Eq (CNF a)
instance Ord a => Ord (CNF a)
instance Show a => Show (CNF a)
instance (Ord a, Read a) => Read (CNF a)
instance NormalForm CNF
instance (Ord a, Negable a) => Boolean (CNF a)
instance (Ord a, Negable a) => Negable (CNF a)
instance CoBoolean a => CoBoolean (CNF a)
instance CoBoolean1 CNF


-- | This module re-exports <tt>Set</tt>-based implementation.
module Data.Algebra.Boolean.CNF


module Data.Algebra.Boolean.NNF.Set

-- | Boolean formula in Negation Normal Form
--   
--   <a>Boolean</a> operations will perform transformations as below:
--   
data NNF a
NNFTrue :: NNF a
NNFFalse :: NNF a
NNFValue :: a -> NNF a
NNFOr :: (Set (NNF a)) -> NNF a
NNFAnd :: (Set (NNF a)) -> NNF a
instance Typeable1 NNF
instance Eq a => Eq (NNF a)
instance Ord a => Ord (NNF a)
instance Show a => Show (NNF a)
instance (Ord a, Read a) => Read (NNF a)
instance NormalForm NNF
instance (Ord a, Negable a) => Boolean (NNF a)
instance (Ord a, Negable a) => Negable (NNF a)
instance CoBoolean1 NNF
instance CoBoolean a => CoBoolean (NNF a)


module Data.Algebra.Boolean.DNF.List

-- | Boolean formula in Disjunction Normal Form
--   
newtype DNF a
DNF :: [[a]] -> DNF a
unDNF :: DNF a -> [[a]]
fromDoubleList :: [[a]] -> DNF a
toDoubleList :: DNF a -> [[a]]
fromNNF :: Negable a => NNF a -> DNF a
instance Typeable1 DNF
instance Eq a => Eq (DNF a)
instance Ord a => Ord (DNF a)
instance Show a => Show (DNF a)
instance Read a => Read (DNF a)
instance Functor DNF
instance NormalForm DNF
instance Negable a => Boolean (DNF a)
instance Negable a => Negable (DNF a)
instance CoBoolean a => CoBoolean (DNF a)
instance CoBoolean1 DNF


module Data.Algebra.Boolean.CNF.List

-- | Boolean formula in Conjunction Normal Form
--   
newtype CNF a
CNF :: [[a]] -> CNF a
unCNF :: CNF a -> [[a]]
fromDoubleList :: [[a]] -> CNF a
toDoubleList :: CNF a -> [[a]]
fromNNF :: Negable a => NNF a -> CNF a
instance Typeable1 CNF
instance Eq a => Eq (CNF a)
instance Ord a => Ord (CNF a)
instance Show a => Show (CNF a)
instance Read a => Read (CNF a)
instance Functor CNF
instance NormalForm CNF
instance Negable a => Boolean (CNF a)
instance Negable a => Negable (CNF a)
instance CoBoolean a => CoBoolean (CNF a)
instance CoBoolean1 CNF