-- 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.1


module Data.Algebra.Boolean.CoBoolean

-- | A class to values translable to booleans.
class CoBoolean a

-- | Cast value to <a>Boolean</a>.
toBoolean :: (CoBoolean a, Boolean b) => a -> b

-- | A polymorphic class of values translable to booleans.
class CoBoolean1 b

-- | Cast value to <a>Boolean</a>.
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 Data.Algebra.Boolean.CoBoolean.CoBoolean GHC.Types.Bool
instance (Data.Algebra.Boolean.CoBoolean.CoBoolean f, Data.Algebra.Boolean.CoBoolean.CoBoolean g) => Data.Algebra.Boolean.CoBoolean.CoBoolean (Data.Either.Either f g)
instance Data.Algebra.Boolean.CoBoolean.CoBoolean (GHC.Base.Maybe a)
instance Data.Algebra.Boolean.CoBoolean.CoBoolean1 GHC.Base.Maybe


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

-- | Invert the value.
not :: Negable x => x -> x
instance GHC.Base.Functor Data.Algebra.Boolean.Negable.Neg
instance GHC.Read.Read a => GHC.Read.Read (Data.Algebra.Boolean.Negable.Neg a)
instance GHC.Show.Show a => GHC.Show.Show (Data.Algebra.Boolean.Negable.Neg a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Data.Algebra.Boolean.Negable.Neg a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Data.Algebra.Boolean.Negable.Neg a)
instance Data.Algebra.Boolean.CoBoolean.CoBoolean (Data.Algebra.Boolean.Negable.Neg a)
instance Data.Algebra.Boolean.CoBoolean.CoBoolean1 Data.Algebra.Boolean.Negable.Neg
instance Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Data.Algebra.Boolean.Negable.Neg a)
instance Data.Algebra.Boolean.Negable.Negable (Data.Algebra.Boolean.Negable.Neg a)
instance Data.Algebra.Boolean.Negable.Negable GHC.Types.Bool
instance GHC.Base.Monoid m => Data.Algebra.Boolean.Negable.Negable (GHC.Base.Maybe m)
instance (Data.Algebra.Boolean.Negable.Negable a, Data.Algebra.Boolean.Negable.Negable b) => Data.Algebra.Boolean.Negable.Negable (a, b)
instance (Data.Algebra.Boolean.Negable.Negable a, Data.Algebra.Boolean.Negable.Negable b) => Data.Algebra.Boolean.Negable.Negable (Data.Either.Either a b)


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 Data.Foldable.Foldable Data.Algebra.Boolean.FreeBoolean.FreeBoolean
instance GHC.Base.Functor Data.Algebra.Boolean.FreeBoolean.FreeBoolean
instance GHC.Read.Read a => GHC.Read.Read (Data.Algebra.Boolean.FreeBoolean.FreeBoolean a)
instance GHC.Show.Show a => GHC.Show.Show (Data.Algebra.Boolean.FreeBoolean.FreeBoolean a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Data.Algebra.Boolean.FreeBoolean.FreeBoolean a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Data.Algebra.Boolean.FreeBoolean.FreeBoolean a)
instance Data.Algebra.Boolean.CoBoolean.CoBoolean1 Data.Algebra.Boolean.FreeBoolean.FreeBoolean
instance Data.Algebra.Boolean.CoBoolean.CoBoolean a => Data.Algebra.Boolean.CoBoolean.CoBoolean (Data.Algebra.Boolean.FreeBoolean.FreeBoolean a)
instance Data.Algebra.Boolean.Negable.Negable (Data.Algebra.Boolean.FreeBoolean.FreeBoolean a)
instance Data.Algebra.Boolean.Boolean (Data.Algebra.Boolean.FreeBoolean.FreeBoolean a)
instance Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Data.Algebra.Boolean.FreeBoolean.FreeBoolean a)


module Data.Algebra.Boolean.NormalForm

-- | Class unifying different boolean normal forms.
class CoBoolean1 nf => NormalForm nf where type NFConstraint nf a :: Constraint type NFConstraint nf a = () where {
    type family NFConstraint nf a :: Constraint;
    type NFConstraint nf a = ();
}

-- | Lift a value into normal form.
toNormalForm :: NormalForm nf => a -> nf a

-- | Simplify the formula, if some terms are ⊥ or ⊤.
simplify :: (NormalForm nf, NFConstraint nf a) => (a -> Maybe Bool) -> nf a -> nf a

-- | transform from free boolean form
fromFreeBoolean :: (NormalForm nf, NFConstraint nf a) => FreeBoolean a -> nf a
instance Data.Algebra.Boolean.NormalForm.NormalForm Data.Algebra.Boolean.FreeBoolean.FreeBoolean


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 Data.Foldable.Foldable Data.Algebra.Boolean.NNF.Set.NNF
instance (GHC.Classes.Ord a, GHC.Read.Read a) => GHC.Read.Read (Data.Algebra.Boolean.NNF.Set.NNF a)
instance GHC.Show.Show a => GHC.Show.Show (Data.Algebra.Boolean.NNF.Set.NNF a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Data.Algebra.Boolean.NNF.Set.NNF a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Data.Algebra.Boolean.NNF.Set.NNF a)
instance Data.Algebra.Boolean.CoBoolean.CoBoolean a => Data.Algebra.Boolean.CoBoolean.CoBoolean (Data.Algebra.Boolean.NNF.Set.NNF a)
instance Data.Algebra.Boolean.CoBoolean.CoBoolean1 Data.Algebra.Boolean.NNF.Set.NNF
instance (GHC.Classes.Ord a, Data.Algebra.Boolean.Negable.Negable a) => Data.Algebra.Boolean.Negable.Negable (Data.Algebra.Boolean.NNF.Set.NNF a)
instance (GHC.Classes.Ord a, Data.Algebra.Boolean.Negable.Negable a) => Data.Algebra.Boolean.Boolean (Data.Algebra.Boolean.NNF.Set.NNF a)
instance Data.Algebra.Boolean.NormalForm.NormalForm Data.Algebra.Boolean.NNF.Set.NNF
instance Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Data.Algebra.Boolean.NNF.Set.NNF a)


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 Data.Foldable.Foldable Data.Algebra.Boolean.NNF.Tree.NNF
instance GHC.Base.Functor Data.Algebra.Boolean.NNF.Tree.NNF
instance GHC.Read.Read a => GHC.Read.Read (Data.Algebra.Boolean.NNF.Tree.NNF a)
instance GHC.Show.Show a => GHC.Show.Show (Data.Algebra.Boolean.NNF.Tree.NNF a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Data.Algebra.Boolean.NNF.Tree.NNF a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Data.Algebra.Boolean.NNF.Tree.NNF a)
instance Data.Algebra.Boolean.CoBoolean.CoBoolean a => Data.Algebra.Boolean.CoBoolean.CoBoolean (Data.Algebra.Boolean.NNF.Tree.NNF a)
instance Data.Algebra.Boolean.CoBoolean.CoBoolean1 Data.Algebra.Boolean.NNF.Tree.NNF
instance Data.Algebra.Boolean.Negable.Negable a => Data.Algebra.Boolean.Negable.Negable (Data.Algebra.Boolean.NNF.Tree.NNF a)
instance Data.Algebra.Boolean.Negable.Negable a => Data.Algebra.Boolean.Boolean (Data.Algebra.Boolean.NNF.Tree.NNF a)
instance Data.Algebra.Boolean.NormalForm.NormalForm Data.Algebra.Boolean.NNF.Tree.NNF
instance Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Data.Algebra.Boolean.NNF.Tree.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 Data.Foldable.Foldable Data.Algebra.Boolean.DNF.List.DNF
instance GHC.Base.Functor Data.Algebra.Boolean.DNF.List.DNF
instance GHC.Read.Read a => GHC.Read.Read (Data.Algebra.Boolean.DNF.List.DNF a)
instance GHC.Show.Show a => GHC.Show.Show (Data.Algebra.Boolean.DNF.List.DNF a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Data.Algebra.Boolean.DNF.List.DNF a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Data.Algebra.Boolean.DNF.List.DNF a)
instance Data.Algebra.Boolean.CoBoolean.CoBoolean1 Data.Algebra.Boolean.DNF.List.DNF
instance Data.Algebra.Boolean.CoBoolean.CoBoolean a => Data.Algebra.Boolean.CoBoolean.CoBoolean (Data.Algebra.Boolean.DNF.List.DNF a)
instance Data.Algebra.Boolean.Negable.Negable a => Data.Algebra.Boolean.Negable.Negable (Data.Algebra.Boolean.DNF.List.DNF a)
instance Data.Algebra.Boolean.Negable.Negable a => Data.Algebra.Boolean.Boolean (Data.Algebra.Boolean.DNF.List.DNF a)
instance Data.Algebra.Boolean.NormalForm.NormalForm Data.Algebra.Boolean.DNF.List.DNF
instance Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Data.Algebra.Boolean.DNF.List.DNF a)


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 Data.Foldable.Foldable Data.Algebra.Boolean.DNF.Set.DNF
instance (GHC.Classes.Ord a, GHC.Read.Read a) => GHC.Read.Read (Data.Algebra.Boolean.DNF.Set.DNF a)
instance GHC.Show.Show a => GHC.Show.Show (Data.Algebra.Boolean.DNF.Set.DNF a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Data.Algebra.Boolean.DNF.Set.DNF a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Data.Algebra.Boolean.DNF.Set.DNF a)
instance Data.Algebra.Boolean.CoBoolean.CoBoolean1 Data.Algebra.Boolean.DNF.Set.DNF
instance Data.Algebra.Boolean.CoBoolean.CoBoolean a => Data.Algebra.Boolean.CoBoolean.CoBoolean (Data.Algebra.Boolean.DNF.Set.DNF a)
instance (GHC.Classes.Ord a, Data.Algebra.Boolean.Negable.Negable a) => Data.Algebra.Boolean.Negable.Negable (Data.Algebra.Boolean.DNF.Set.DNF a)
instance (GHC.Classes.Ord a, Data.Algebra.Boolean.Negable.Negable a) => Data.Algebra.Boolean.Boolean (Data.Algebra.Boolean.DNF.Set.DNF a)
instance Data.Algebra.Boolean.NormalForm.NormalForm Data.Algebra.Boolean.DNF.Set.DNF
instance Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Data.Algebra.Boolean.DNF.Set.DNF a)


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


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


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 Data.Foldable.Foldable Data.Algebra.Boolean.CNF.Set.CNF
instance (GHC.Classes.Ord a, GHC.Read.Read a) => GHC.Read.Read (Data.Algebra.Boolean.CNF.Set.CNF a)
instance GHC.Show.Show a => GHC.Show.Show (Data.Algebra.Boolean.CNF.Set.CNF a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Data.Algebra.Boolean.CNF.Set.CNF a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Data.Algebra.Boolean.CNF.Set.CNF a)
instance Data.Algebra.Boolean.CoBoolean.CoBoolean1 Data.Algebra.Boolean.CNF.Set.CNF
instance Data.Algebra.Boolean.CoBoolean.CoBoolean a => Data.Algebra.Boolean.CoBoolean.CoBoolean (Data.Algebra.Boolean.CNF.Set.CNF a)
instance (GHC.Classes.Ord a, Data.Algebra.Boolean.Negable.Negable a) => Data.Algebra.Boolean.Negable.Negable (Data.Algebra.Boolean.CNF.Set.CNF a)
instance (GHC.Classes.Ord a, Data.Algebra.Boolean.Negable.Negable a) => Data.Algebra.Boolean.Boolean (Data.Algebra.Boolean.CNF.Set.CNF a)
instance Data.Algebra.Boolean.NormalForm.NormalForm Data.Algebra.Boolean.CNF.Set.CNF
instance Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Data.Algebra.Boolean.CNF.Set.CNF a)


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 Data.Foldable.Foldable Data.Algebra.Boolean.CNF.List.CNF
instance GHC.Base.Functor Data.Algebra.Boolean.CNF.List.CNF
instance GHC.Read.Read a => GHC.Read.Read (Data.Algebra.Boolean.CNF.List.CNF a)
instance GHC.Show.Show a => GHC.Show.Show (Data.Algebra.Boolean.CNF.List.CNF a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Data.Algebra.Boolean.CNF.List.CNF a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Data.Algebra.Boolean.CNF.List.CNF a)
instance Data.Algebra.Boolean.CoBoolean.CoBoolean1 Data.Algebra.Boolean.CNF.List.CNF
instance Data.Algebra.Boolean.CoBoolean.CoBoolean a => Data.Algebra.Boolean.CoBoolean.CoBoolean (Data.Algebra.Boolean.CNF.List.CNF a)
instance Data.Algebra.Boolean.Negable.Negable a => Data.Algebra.Boolean.Negable.Negable (Data.Algebra.Boolean.CNF.List.CNF a)
instance Data.Algebra.Boolean.Negable.Negable a => Data.Algebra.Boolean.Boolean (Data.Algebra.Boolean.CNF.List.CNF a)
instance Data.Algebra.Boolean.NormalForm.NormalForm Data.Algebra.Boolean.CNF.List.CNF
instance Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Data.Algebra.Boolean.CNF.List.CNF a)


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