This module imports and reexports all the necessary bits.
Next there are three key Prop instances:
Then there are two Prop instances which combine the previous ones:
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.
|Produced by Haddock version 0.8|