This module imports and reexports all the necessary bits.

The key module is Data.Proposition.Internal, this contains the PropLit and Prop classes around which the entire library is based.

Next there are three key Prop instances:

• PropSimple provides a simple (and obviously correct) implementation of the class.
• Formula is an implementation based on an abstract syntax tree of a formula, similar to the Simple version, but which tries a lot harder to perform simplifications.
• BDD is an implementation based on Binary Decision Diagrams (BDD's). These have a fast and accurate Eq test.

Then there are two Prop instances which combine the previous ones:

• PropAll carries out all operations on all the three main propositions at once. If one disagrees then an error is given - useful mainly for testing.
• PropFix operates mainly on Formula, switching to BDD for equality testing. This is intended for finding fixed points faster.

There is one module in this library which is not including by this one. Data.Proposition.Char provides a PropLit instance for Char.

We now present a short example, the code can be found in Sample.hs in the root of the darcs repo.

First step, lets import the necessary stuff:

 import Data.Predicate        -- standard import
 import Data.Predicate.Char   -- so we can place characters in a proposition

Let us define a formula:

 prop :: Prop p => p Char
 prop = propAnds [propLit 'a' `propOr` propNot (propLit 'b')
                 ,propLit 'c' `propOr` propLit 'c'
                 ,propLit 'd' `propOr` propTrue]

This example makes use of all the basic proposition operations. propLit constructs a proposition from a literal. propNot is negation of a proposition. propAnd and propAnds are the equivalents to && and and, ditto with propOr and propOrs.

We can now display this proposition as any of the standard propositions:

 Main> prop :: PropSimple Char
 (('a' v ~('b')) ^ ('c' v 'c'))

This is the basic proposition, which has done or True short-circuiting.

 Main> prop :: Formula Char
 ('c' ^ ('a' v ~'b'))

This proposition has done c || c = c transformation as well. It can also do more fancy simplifications as described by the PropLit transformation.

 Main> prop :: BDD Char
 'a' <'b' <'c' | False> | 'c'>

This final proposition is a BDD. You can read this as a tree, where left is a False choice, and right is a True choice:

                a
               / \
              b   c
             / \
            c  False

Now following the varibles will give you the logical result. Also note that the variables are ordered so 'a' will always be at the root.

We can now perform various operations on the proposition, a couple of interesting ones are:

We can now define an upperCase operation:

 upperCase x = propMap (propLit . toUpper) x

 Main> upperCase prop :: Formula Char
 ('C' ^ ('A' v ~'B'))

We can also change from one type of proposition to another:

 Main> propRebuildSimple (prop  :: BDD Char)
 ((~('a') v 'c') ^ ('a' v (~('b') ^ ('b' v 'c'))))

And we can also test whether a proposition is True or False:

 Main> propIsTrue (prop :: BDD Char)
 False
 Main> propIsFalse (prop :: BDD Char)
 False

There are lots of other operations of propositions, but these are the most common.