PropLogic (empty) → 0.9
raw patch · 11 files changed
+5168/−0 lines, 11 filesdep +basedep +haskell98setup-changed
Dependencies added: base, haskell98
Files
- Costack.hs +89/−0
- DefaultPropLogic.hs +1674/−0
- FastPropLogic.hs +1278/−0
- Main.hs +127/−0
- Olist.hs +268/−0
- PropLogic.cabal +29/−0
- PropLogic.hs +190/−0
- PropLogicCore.hs +315/−0
- PropLogicTest.hs +855/−0
- Setup.lhs +5/−0
- TextDisplay.hs +338/−0
+ Costack.hs view
@@ -0,0 +1,89 @@+module Costack (+ Costack(),+ fromList, toList,+ cons, cocons,+ Costack.head, Costack.tail,+ isEmpty, empty,+ singleton, append, Costack.concat, merge,+ Costack.length,+ Costack.map, Costack.foldr,+ Costack.take, Costack.filter,+ Costack.sort, Costack.strictSort, Costack.sorted, Costack.strictSorted,+) where ---------------------------------------------------------------------------------------------------------------++ import qualified List as L++ data Costack a = COSTACK [a]+ deriving (Show, Read, Eq)++ fromList :: [a] -> Costack a+ fromList l = COSTACK l++ toList :: Costack a -> [a]+ toList (COSTACK l)= l++ cons :: a -> Costack a -> Costack a+ cons x (COSTACK yL) = COSTACK (x:yL)++ cocons :: Costack a -> a -> Costack a+ cocons (COSTACK xL) y = COSTACK (xL ++ [y])++ head :: Costack a -> a+ head (COSTACK []) = error "Costack.head -- empty costack"+ head (COSTACK (x:xL)) = x++ tail :: Costack a -> Costack a+ tail (COSTACK []) = error "Costack.tail -- empty costack"+ tail (COSTACK (x:xL)) = COSTACK xL++ isEmpty :: Costack a -> Bool+ isEmpty (COSTACK l) = null l++ empty :: Costack a+ empty = COSTACK []++ singleton :: a -> Costack a+ singleton x = COSTACK [x]++ append :: Costack a -> Costack a -> Costack a+ append (COSTACK xL) (COSTACK yL) = COSTACK (xL ++ yL)++ concat :: [Costack a] -> Costack a+ concat cL = COSTACK (Prelude.concat (Prelude.map toList cL))++ merge :: Costack (Costack a) -> Costack a+ merge c = COSTACK (Prelude.concat (Prelude.map toList (toList c)))++ length :: Costack a -> Int+ length (COSTACK xL) = Prelude.length xL++ map :: (a -> b) -> Costack a -> Costack b+ map f (COSTACK xL) = COSTACK (Prelude.map f xL)++ foldr :: (a -> b -> b) -> b -> Costack a -> b+ foldr f x (COSTACK []) = x+ foldr f x (COSTACK (y:yL)) = Costack.foldr f (f y x) (COSTACK yL)++ take :: Int -> Costack a -> Costack a+ take n (COSTACK xL) = COSTACK (Prelude.take n xL)++ filter :: (a -> Bool) -> Costack a -> Costack a+ filter p (COSTACK xL) = COSTACK (Prelude.filter p xL)++ sort :: Ord a => Costack a -> Costack a+ sort (COSTACK xL) = COSTACK (L.sort xL)++ sorted :: Ord a => Costack a -> Bool+ sorted (COSTACK xL) = iter xL+ where iter [] = True+ iter [x] = True+ iter (x:y:zL) = x < y && iter (y:zL)++ strictSort :: Ord a => Costack a -> Costack a+ strictSort (COSTACK xL) = COSTACK (L.nub (L.sort xL))++ strictSorted :: Ord a => Costack a -> Bool+ strictSorted (COSTACK xL) = iter xL+ where iter [] = True+ iter [x] = True+ iter (x:y:zL) = x <= y && iter (y:zL)
+ DefaultPropLogic.hs view
@@ -0,0 +1,1674 @@+{-# LANGUAGE TypeSynonymInstances, FlexibleInstances, MultiParamTypeClasses #-}++{- |+ This module implements the basic operations of propositional logic in a very /default/ way, i.e. the definitions and implementations+ are very intuitive and the whole module can be seen as a reconstruction and tutorial of propositional logic itself.+ However, some of these implementations are not feasible for other than very small input, because the intuitive algorithms are+ sometimes too ineffective.++ Next to some syntactical tools, we provide a common reconstruction of the semantics with an emphasis on /truth tables/.+ As a result, we obtain two default models of a propositional algebra, namely+ @PropAlg a (PropForm a)@ the propositional algebra on propositional formulas 'PropForm' and+ @PropAlg a (TruthTable a)@ the algebra on the so-called /truth tables/ 'TruthTable' (each one on a linearly ordered atom type @a@).+ Additionally, we also instantiate the predefined boolean value algebra on 'Bool' as a trivial, because atomless propositional algebra.++ Another important concept is the /normalization/. We introduce a whole range of /normalizers/ and /canonizers/ of+ propositional formulas.+-}++module DefaultPropLogic (++ -- * Syntactic operations++ -- ** Formula Deconstructors++ juncDeg,+ -- | returns a /junctor degree/ @0,1,...,,7@, in case the formulas is created with @A,F,T,N,CJ,DJ,SJ,EJ@, respectively.+ -- For example,+ --+ -- > > juncDeg (A 'x')+ -- > 0+ -- >+ -- > > juncDeg (CJ [A 'x', F])+ -- > 4++ juncArgs,+ -- | returns the list of arguments of the outer junctor of the given formula, e.g.+ --+ -- > > juncArgs (SJ [A 'x', F, CJ [A 'y', T]])+ -- > [A 'x',F,CJ [A 'y',T]]+ -- >+ -- > > juncArgs F+ -- > []+ -- >+ -- > > juncArgs (N T)+ -- > [T]+ -- >+ -- > > juncArgs (A 'x')+ -- > [A 'x']++ juncCons,+ -- | is the junction constructor, which is defined so that for every formula @p@ holds+ --+ -- > juncCons (juncDeg p) (juncArgs p) == p+ --+ -- For example,+ --+ -- > > juncCons 5 [juncCons 0 [A 'x'], juncCons 1 [], juncCons 3 [juncCons 2 []]]+ -- > DJ [A 'x',F,N T]++ -- ** Size++ atomSize,+ -- | counts the number of atoms (including multiple occurrences), i.e. each occurrence of an @A@.+ --+ -- > atomSize ( CJ [DJ [A "x", N (A "y")], DJ [A "x", A "z"], T] ) == 4+ --++ juncSize,+ -- | counts the number of bit values and junctions, i.e. each occurrence of @F@, @T@, @N@, @CJ@, @DJ@, @SJ@, @EJ@+ --+ -- > juncSize ( CJ [DJ [A "x", N (A "y")], DJ [A "x", A "z"], T] ) == 5+ --++ size,+ -- | The overall size of a formula, where+ --+ -- > (size f) = (atomSize f) + (juncSize f)+ --+ -- For example+ --+ -- > size ( CJ [DJ [A "x", N (A "y")], DJ [A "x", A "z"], T] ) == 9++ -- ** Linear syntactic order on formulas+ -- | .....................................CONTINUEHERE ....................................................++ -- * Semantics+ -- | A denotational semantics for propositional formulas is defined by the basic idea, that the /truth table/ of a formula+ -- defines its meaning. Formally speaking, if @A = {a1, ..., aN}@ is the atom set of a given formula φ, then each /valuator/,+ -- i.e. each function @ω :: A -> Bool@ turns φ into an either @True@ or @False@ value (namely @boolApply φ ω@).+ -- The summary of these @2^N@ valuator-value pairs is formalized by a function @(A -> Bool) -> Bool@, and that is what we call+ -- the /truth table/ of φ (namely @truthTable φ@).+ --+ -- For example, if φ is @a ↔ b@, then the atom set is @{a,b}@. And if @tt = truthTable φ@, then we can+ -- @display tt@ and obtain+ --+ -- > +---+---+---++ -- > | a | b | |+ -- > +---+---+---++ -- > | 0 | 0 | 1 |+ -- > +---+---+---++ -- > | 0 | 1 | 0 |+ -- > +---+---+---++ -- > | 1 | 0 | 0 |+ -- > +---+---+---++ -- > | 1 | 1 | 1 |+ -- > +---+---+---++ --+ -- Implementing this idea in Haskell is not that straight forward however, because Haskell doesn't allow type constructions like+ -- @(atoms φ) -> Bool@ for valuators and @((atoms φ) -> Bool) -> Bool@ for truth tables. So we need to make some adaptions.++ -- ** Valuators and formulas as functions+ LiteralPair,+ Valuator,+ -- | Ideally, a valuator is a finite function @{a1,...,aN} -> Bool@ and we can represent it as a list of atom-value pairs+ -- @[(a1,b1),...,(aN,bN)]@. We disambiguate and increase the efficiency of this representation, when we demand that @a1 < ... < aN@,+ -- according to a given order on the atoms. But declaring @Valuator a@ as @Olist (a, Bool)@ only makes @(a1, b1) < ... < (aN, bN)@.+ -- For example, @[('x',False),('x',True)]@ is a @Valuator Char@, but obviously not a /correct/ one, as we call it.++ correctValuator,+ -- | If the given list of literal pairs makes a correct valuator, then this argument is returned as it is. Otherwise, an error+ -- occurs. For example,+ --+ -- > > correctValuator [('x', False), ('y', True)]+ -- > [('x',False),('y',True)]+ -- >+ -- > > correctValuator [('x', False), ('x', True)]+ -- > *** Exception: correctValuator: multiple occurring atoms+ -- >+ -- > > correctValuator [('y', False), ('x', True)]+ -- > *** Exception: correctValuator: atoms are not in order++ valuate,+ -- | @valuate ω φ@ takes the formula φ and replaces its atoms by boolean values according to ω. For example,+ --+ -- > > valuate [('x', True), ('y', False)] (EJ [A 'x', N (A 'x'), A 'y', A 'z', A 'y'])+ -- > EJ [T,N T,F,A 'z',F]++ boolEval,+ -- | @boolEval ω@ evaluates a nullatomic formula ω to a boolean value according to the common semantics for the+ -- junctions @N@, @DJ@, ..., but causes an error when ω is not nullatomic. For example,+ --+ -- > > boolEval (DJ [T, F])+ -- > True+ -- >+ -- > > boolEval (CJ [T, F])+ -- > False+ -- >+ -- > > boolEval (EJ [T,T])+ -- > True+ -- >+ -- > > boolEval (CJ [T, SJ [F, F]])+ -- > True+ -- >+ -- > > boolEval (CJ [T, A 'x'])+ -- > -- error ...+ --+ -- (Note, that we also provide a generalization 'eval' of 'boolEval' below.)++ boolApply,+ -- | combines 'valuate' and 'boolEval', i.e.+ --+ -- > boolApply p v = boolEval (valuate v p)+ --+ -- For example,+ --+ -- > > boolApply (EJ [A 'x', A 'y']) [('x', True), ('y', True)]+ -- > True+ -- >+ -- > > boolApply (EJ [A 'x', A 'y']) [('x', True), ('y', False)]+ -- > False+ -- >+ -- > > boolApply (EJ [A 'x', A 'y']) [('x', True)]+ -- > -- error+ --+ -- (Note, that we also provide a generalization 'apply' of 'boolApply' below.)++ allValuators,+ -- | For example+ --+ -- > > allValuators ['y', 'x']+ -- > [[('x',False),('y',False)],[('x',False),('y',True)],[('x',True),('y',False)],[('x',True),('y',True)]]++ zeroValuators,+ -- | @zeroValuators φ@ returns all valuators @ω@ (on the atom set of @φ@) with @boolApply φ ω = False@.+ -- For example,+ --+ -- > > zeroValuators (CJ [A 'x', A 'y'])+ -- > [[('x',False),('y',False)],[('x',False),('y',True)],[('x',True),('y',False)]]++ unitValuators,+ -- | @unitValuators φ@ returns all valuators @ω@ (on the atom set of @φ@) with @boolApply φ ω = Truee@.+ -- For example,+ --+ -- > > unitValuators (CJ [A 'x', A 'y'])+ -- > [[('x',True),('y',True)]]++ -- ** Truth tables++ TruthTable,+ -- | A truth table is thus a triple @(atomList, optForm, tableBody)@, where @atomList@ is the ordered list of atoms, @optForm@ is+ -- the optional formula that is a representation for this table, and @tableBody@ holds the rows of the table.+ -- For example, if the table @tt :: TruthTable String@ is 'display'ed by+ --+ -- > +---+---+---++ -- > | x | y | |+ -- > +---+---+---++ -- > | 0 | 0 | 1 |+ -- > +---+---+---++ -- > | 0 | 1 | 0 |+ -- > +---+---+---++ -- > | 1 | 0 | 0 |+ -- > +---+---+---++ -- > | 1 | 1 | 1 |+ -- > +---+---+---++ --+ -- then @tt@ has the formal representation as+ --+ -- > (["x","y"],Nothing,[([False,False],True),([False,True],False),([True,False],False),([True,True],True)])+ --+ -- The optional formula @Maybe (PropForm String)@ is @Nothing@ in this case, and this makes it a /plain/ table.+ -- But it is common and often convenient to write the formula that represents this table in the head row as well.+ -- Such a truth table is e.g. given by+ --+ -- > (["x","y"],Just (EJ [A "x",A "y"]),[([False,False],True),([False,True],False),([True,False],False),([True,True],True)])+ --+ -- And when we 'display' it, we obtain+ --+ -- > +---+---+-----------++ -- > | x | y | [x <-> y] |+ -- > +---+---+-----------++ -- > | 0 | 0 | 1 |+ -- > +---+---+-----------++ -- > | 0 | 1 | 0 |+ -- > +---+---+-----------++ -- > | 1 | 0 | 0 |+ -- > +---+---+-----------++ -- > | 1 | 1 | 1 |+ -- > +---+---+-----------+++ correctTruthTable,+ -- | checks if the given argument makes indeed a proper truth table. If so, the argument is returned unaltered. Otherwise, an+ -- according error message is returned.++ truthTable,+ -- | returns the truth table of the given formula, with the formula itself included in the header. For example,+ --+ -- > > truthTable (EJ [A "abc", F])+ -- > (["abc"],Just (EJ [A "abc",F]),[([False],True),([True],False)])+ -- >+ -- > > display it+ -- > +-----+-----------------++ -- > | abc | [abc <-> false] |+ -- > +-----+-----------------++ -- > | 0 | 1 |+ -- > +-----+-----------------++ -- > | 1 | 0 |+ -- > +-----+-----------------+++ plainTruthTable,+ -- | as @truthTable@, but this time without the formula included. For the same example, this is+ --+ -- > > plainTruthTable (EJ [A "abc", F])+ -- > (["abc"],Nothing,[([False],True),([True],False)])+ -- >+ -- > > display it+ -- > +-----+---++ -- > | abc | |+ -- > +-----+---++ -- > | 0 | 1 |+ -- > +-----+---++ -- > | 1 | 0 |+ -- > +-----+---+++ truthTableBy,+ -- | By default, the truth table of a formula φ, i.e. the right result column of the table is constructed with+ -- @boolApply φ ω@ for the valuator @ω@ in each of the rows. Now @truthTableBy@ is a generalization of this+ -- construction and allows other functions of type @Valuator a -> Bool@ for this process, as well.++ -- ** Multiple truth tables++ -- | It is common and efficient, for example when comparing several formulas for equivalence, to write these formulas in just+ -- one table and add a result row for each formula. For example, the two formulas @¬(x → y)@ and @x ∧ ¬ y@+ -- are equivalent and we can verify that by comparing the two result columns in their tables. We call+ --+ -- > > multiTruthTable [N (SJ [A 'x', A 'y']), CJ [A 'x', N (A 'y')]]+ -- > ("xy",[N (SJ [A 'x',A 'y']),CJ [A 'x',N (A 'y')]],+ -- > [([False,False],[False,False]),([False,True],[False,False]),([True,False],[True,True]),([True,True],[False,False])])+ -- >+ -- > > display it+ -- > +-------------------------++ -- > | MultiTruthTable |+ -- > | 1. -[x -> y] |+ -- > | 2. [x * -y] |+ -- > | +---+---+------+------+ |+ -- > | | x | y | 1. | 2. | |+ -- > | +---+---+------+------+ |+ -- > | | 0 | 0 | 0 | 0 | |+ -- > | +---+---+------+------+ |+ -- > | | 0 | 1 | 0 | 0 | |+ -- > | +---+---+------+------+ |+ -- > | | 1 | 0 | 1 | 1 | |+ -- > | +---+---+------+------+ |+ -- > | | 1 | 1 | 0 | 0 | |+ -- > | +---+---+------+------+ |+ -- > +-------------------------+++ MultiTruthTable,+ -- | Similar to the type definition of 'TruthTable' as a triple @(atoms, formulaList, tableBody)@.++ correctMultiTruthTable,+ -- | returns the argument unchanged, if this is a well-formed 'MultiTruthTable' (with correct number of rows and columns etc.),+ -- and returns an error, otherwise.++ multiTruthTable,+ -- | returns the common 'MultiTruthTable' of a formula list, where the atom list is the union of the atoms of all the formulas.++ -- ** Mutual converters between syntax and semantics++ -- | With 'truthTable' we turned a 'PropForm' into a 'TruthTable'. But we can also turn a 'TruthTable' into a 'PropForm'.+ -- However, this process is not unique anymore, because there are (infinitely) many formulas to represent each truth table.+ -- Nevertheless, there are two standard ways to do so:+ --+ -- (1) Each row with a result 1 (i.e. each /unit valuator/) is turned into a /Normal Literal Conjunction/ or 'NLC' and+ -- the disjunction of them is a /Disjunctive Normal Form/ or 'DNF', which represents the table.+ --+ -- (2) Each row with a result 0 (i.e. each /zero valuator/) is turned into a /Normal Literal Disjunction/ or 'NLD' and+ -- the conjunction of them is a /Conjunctive Normal Form/ or 'CNF', which represents the table, too.+ --+ -- For example, if the 'TruthTable' is say+ --+ -- > > let tt = truthTable (EJ [A 'x', A 'y'])+ -- > > > display tt+ -- > +---+---+-----------++ -- > | x | y | [x <-> y] |+ -- > +---+---+-----------++ -- > | 0 | 0 | 1 |+ -- > +---+---+-----------++ -- > | 0 | 1 | 0 |+ -- > +---+---+-----------++ -- > | 1 | 0 | 0 |+ -- > +---+---+-----------++ -- > | 1 | 1 | 1 |+ -- > +---+---+-----------++ --+ -- then+ --+ -- > > display (truthTableToDNF tt)+ -- > [[-x * -y] + [x * y]]+ -- >+ -- > > display (truthTableToCNF tt)+ -- > [[x + -y] * [-x + y]]+ --+ -- The following functions provides the whole range of transformations for valuators, valuator lists, truth tables, and the+ -- according normal forms.++ valuatorToNLC,+ -- | For example,+ --+ -- > > valuatorToNLC [('x', True), ('y', False), ('z', True)]+ -- > CJ [A 'x',N (A 'y'),A 'z']++ valuatorToNLD,+ -- | For example,+ --+ -- > > valuatorToNLD [('x', True), ('y', False), ('z', True)]+ -- > DJ [N (A 'x'),A 'y',N (A 'z')]+ --+ -- Note, that the literal values appear inverted, e.g. @('x', True)@ becomes @N (A 'x')@.++ valuatorListToCNF,+ -- | turns each valuator of the given list into its 'NLD' and returns their overall conjunction.++ valuatorListToDNF,+ -- | turns each valuator of the given list into its 'NLC' and returns their overall disjunction.++ nlcToValuator,+ -- | Inverse operation of 'valuatorToNLC'. Undefined, if the argument is not a 'NLC'.+ -- For example+ --+ -- > > nlcToValuator (CJ [A 'x', N (A 'y')])+ -- > [('x',True),('y',False)]++ nldToValuator,+ -- | Inverse operation of 'valuatorToNLD'. Undefined, if the argument is not a 'NLD'.+ -- For example+ --+ -- > > nldToValuator (DJ [A 'x', N (A 'y')])+ -- > [('x',False),('y',True)]++ cnfToValuatorList,+ -- | Inverse operation of 'valuatorListToCNF', undefined if the argument is not a 'CNF'.++ dnfToValuatorList,+ -- | Inverse operation of 'valuatorListToDNF', undefined if the argument is not a 'DNF'.++ truthTableZeroValuators,+ -- | extracts all valuators that have a @1@ (i.e. @True@) in their result column.++ truthTableUnitValuators,+ -- | extracts all valuators that have a @0@ (i.e. @False@) in their result column.++ truthTableToDNF,+ -- | as explained above. In fact, @truthTableToDNF = valuatorListToDNF . truthTableUnitValuators@.+ -- Actually, the result is not only a 'DNF', but even a 'NaturalDNF', as described below.++ truthTableToCNF,+ -- | the dual version of 'truthTableToDNF'. Again, the result is even a 'NaturalCNF'.++ -- * Normal Forms++ -- ** Normalizations and Canonizations in general++ -- *** Definition++ -- | Let @S@ be any type (or set) and @~@ an /equivalence relation/ on @S@. A function @nf :: S -> S@ is then said to be+ --+ -- * a /normalizer/ for @~@, when @x ~ y@ iff @(nf x) ~ (nf y)@, for all @x, y :: S@.+ --+ -- * a /canonic normalizer/ or /canonizer/ for @~@, if it is a normalizer and @x ~ y@ implies @(nf x) == (nf y)@,+ -- for all @x, y :: S@.+ --+ -- If the normalizer is not a trivial one (like @id :: S -> S@), then the images @(nf x)@ for @x :: S@ alltogether are a proper+ -- subset of @S@ itself, called /normal forms/. And they are /canonic normal forms/, if they are the result of a+ -- canonizer, i.e. if no two different normal forms are equivalent.++ -- *** Normalizations in Propositional Algebras++ -- | In a propositional algebra @'PropAlg' a p@ we have three equivalence relations on the type @p@ of propositions:+ --+ -- * 'equivalent', the /semantic equivalence/ relation+ --+ -- * 'equiatomic', the /equiatomic/ or /atomic equivalence/ relation+ --+ -- * 'biequivalent', the /biequivalence/ or /theory-algebraic equivalence/ relation+ --+ -- Accordingly, we call a normalizer (or canonizer) @nf :: p -> p@ a+ --+ -- * /semantic/ normalizer, if it is a normalizer for 'equivalent',+ --+ -- * /atomic/ normalizer, if it is a normalizer for 'equiatomic'+ --+ -- * /theory-algebraic/ normalizer or /bi-normalizer/, if it is a normalizer for 'biequivalent'+ --+ -- Traditionally, a normalizer is always a semantic normalizer, and all the normalizers we further introduce in this module are+ -- of this kind. The notion of an atomic normalizer is actually quite superfluous, because it is not really relevant in practice.+ -- But in our concept of a propositional algebra 'PropAlg', two propositions are considered equal (from this abstract point of view),+ -- if they are biequivalent, i.e. if they are equivalent and also have the same atoms.++ -- *** Default semantic normalizations++ -- | In this default approach to normalizations, we only introduce important and more or less common examples and don't built+ -- propositional algebras on them. Most of the normalizers are semantic normalizer.+ --+ -- We also hope to increase the understanding by introducing the normalizer not as a function @nf :: PropForm a -> PropForm a@,+ -- but as @nf :: PropForm a -> NF a@, where @type NF a = PropForm a@ stands for the normal subset of formulas.++ -- ** Ordered Propositional Formulas++ -- | Next to the /semantic/ and /atomic/ order relations, given by `subvalent` and `subatomic`, respectively, there is+ -- also a /formal/ order '<=' defined on formulas.+ -- Different to the semantic and atomic order, this formal order is not only a partial, but even a linear order relation.+ -- In Haskell, these linear order structures are realized as instances of the 'Ord' type class, i.e. we can 'compare'+ -- formulas and check for '<', '<=', '==' between formulas etc, given that the atom type itself is ordered.+ -- The actual implementation of the formal order is irrelevant here.+ -- The only thing of importance here is that fact that we can use it and that way we can remove ambiguities and+ -- increase the effectiveness of some operations. In other words, it induces a normalization as follows.+ --+ -- (Note however, that we did not simply use @deriving@ to implement it, because we adopted the common definition+ -- of literals 'LitForm', and that would have compromised an understanding of 'NLC's and 'NLD's as ordered formulas.+ -- For example, we need @N (A 10) < A 20@ to be true.)+ --+ -- Recall from the axioms of propositional algebras, that conjunctions and disjunctions are both idempotent and commutative,+ -- i.e. we can remove multiple occurring components and arbitrarily change the component order in each conjunction and+ -- disjunction. The result is still (bi-) equivalent.+ -- For example, @CJ [A 'z', A 'x', A 'z', A 'y', A 'z']@ is (bi-)equivalent to @CJ [A 'x', A 'y', A 'z']@.++ OrdPropForm,+ -- | A propositional formula @φ@ is said to be /ordered/, if the components @φ1, φ2..., φN@ of every+ -- conjunction @CJ [φ1, φ2..., φN]@ and every disjunction @DJ [φ1, φ2..., φN]@ occurring in+ -- @φ@ are strictly ordered in the sense that @φ1 < φ2 < ... < φN@.++ isOrdPropForm,+ -- | is @True@ iff the argument is an ordered propositional formula.++ ordPropForm,+ -- | turns each formula into a (bi-)equivalent ordered form. For example,+ --+ -- > > ordPropForm (DJ [A 'x', A 'x', A 'z', A 'y', A 'x'])+ -- > DJ [A 'x',A 'y',A 'z']+ --+ -- > > ordPropForm (CJ [A 'x', T, N (A 'x'), T, F, A 'x'])+ -- > CJ [A 'x',F,T,N (A 'x')] -- because A 'x' < F < T < N (A 'x')++ -- ** Evaluated Normal Forms++ -- | It is common to avoid unary conjunctions @CJ [φ]@ and disjunctions @DJ [φ]@, both are (bi-)equivalent to @φ@+ -- itself. And a nullary @CJ []@ is usually replaced by @T@, and @DJ []@ by @F@.+ -- Nullary and unary sub- and equijunctions are less common, but they are also easily replaceable by their equivalent form @T@.+ --+ -- Another easy simplification of formulas is the involvement of @F@ or @T@ as subformulas. For example, @N F@ is obviously+ -- (bi-)equivalent to @T@, @CJ [φ, T, ψ]@ is (bi-)equivalent to @CJ [φ, ψ]@ and @CJ [φ, F, ψ]@+ -- is equivalent to @T@. Similar rules hold for the other junctions (although a little more complicated in case of @SJ@ and @EJ@).+ --+ -- The replacement of these mentioned subformulas is quite an easy and effective (semantic) normalization and we call it+ -- /evaluation/ 'eval', because it is in a certain way a generalization of the /boolean evaluation/ 'boolEval'.++ EvalNF,+ -- | A formula is called an /Evaluated Normal Form/ iff it is either @F@ or @T@ or a formula that neither has bit values+ -- nor trivial junctions.+ -- By /having bit values/ we mean that it contains @F@s or @T@s as subformulas.+ -- By /having trivial junctions/ we mean nullary or unary junctions with @CJ@, @DJ@, @SJ@, or @EJ@ as subformulas.++ isEvalNF,+ -- | checks, if the given formula is indeed an Evaluated Normal Form. For example,+ --+ -- > > isEvalNF ( T )+ -- > True+ -- > > isEvalNF ( CJ [T, A 'x'] )+ -- > False -- because the formula has a bit value T+ -- > > isEvalNF ( CJ [] )+ -- > False -- because the formula has a trivial junction, namely the nullary conjunction+ -- > > isEvalNF ( SJ [A 'x'] )+ -- > False -- because it has a trivial junction, namely an unary subjunction+ -- > > isEvalNF ( CJ [A 'x', N (A 'y)] )+ -- > True -- has neither bit values nor trivial junctions++ -- *** Generalized evaluation and application for formulas: @eval@ and @apply@++ eval,+ -- | 'eval' takes a given formula and returns an equivalent Evaluated Normal Form.+ -- This way, it is a generalization of 'boolEval', which was only defined for nullatomic formulas.+ -- More precisely, if @φ@ is a nullatomic formula, then @boolEval φ@ is @True@ (or @False@) iff @bool φ@ is+ -- @T@ (or @F@, respectively).+ -- For example+ --+ -- > > eval (N F)+ -- > T+ -- >+ -- > > eval (DJ [A 'x', F, A 'y'])+ -- > DJ [A 'x',A 'y']+ -- >+ -- > > eval (DJ [A 'x', T, A 'y'])+ -- > T+ -- >+ -- > > eval (EJ [A 'x', T])+ -- > A 'x'+ -- >+ -- > > eval (EJ [A 'x', F])+ -- > N (A 'x')+ -- >+ -- > > eval (EJ [A 'x', A 'y'])+ -- > EJ [A 'x',A 'y']+ --+ -- 'eval' is not as powerful as e.g. 'valid', i.e. it does not return 'T' for every valid input formula. For example,+ --+ -- > > eval (DJ [A 'x', N (A 'x')])+ -- > DJ [A 'x', N (A 'x')]+ --+ -- The advantage is that 'eval' is only of linear time complexity (at least if the input formula does not contain subjunctions+ -- or equijunctions; in which case the effort is somewhat greater).+ --+ -- Because the resulting formula is always equivalent to the argument formula, 'eval' is an example of a /(semantic) normalizer/+ -- (see 'EvalNF' below).++ apply,+ -- | As 'eval' is a generalization of 'boolEval', 'apply' is a generalization of 'boolApply', defined by+ -- @apply φ ω = eval (valuate ω φ)@.+ -- For example,+ --+ -- > > apply (DJ [A 'x', A 'y', A 'z']) [('y', True)]+ -- > T+ --+ -- > > apply (DJ [A 'x', A 'y', A 'z']) [('y', False)]+ -- > DJ [A 'x',A 'z']++ -- ** Literal Form(ula)s++ -- | A /literal/ is an atom with an assigned boolean value. The type for the semantic version of a literal was earlier introduced+ -- as the 'LiteralPair'. The formal version is the /literal formula/ 'LitForm', which is either an atomic formula @A x@ or a+ -- negated atomic formula @N (A x)@.+ -- This is the common definition of a literal in logic, although more close to the original idea would be the form @EJ [A x, T]@+ -- instead of @A x@ and @EJ [A x, F]@ instead of @N (A x)@. But it is common in the literature to use the+ -- shorter and (bi-)equivalent versions @A x@ and @N (A x)@, instead.+ --+ -- Of course, the literal formulas do not induce a normalization, most formulas don't have an equivalent literal formula.+ -- But literal formulas are important building blocks of the most important normalizations in propositional logic.++ LitForm,+ -- | is the type synonym for all formulas @A x@ or @N (A x)@.++ isLitForm,+ -- | checks if a formula is indeed a literal form.++ litFormAtom,+ -- | returns the atom of a literal form, e.g.+ --+ -- > > litFormAtom (A 'x')+ -- > 'x'+ --+ -- > > litFormAtom (N (A 'x'))+ -- > 'x'++ litFormValue,+ -- | returns the boolean value of a literal form, e.g.+ --+ -- > > litFormValue (A 'x')+ -- > True+ --+ -- > > litFormValue (N (A 'x'))+ -- > False++ -- ** Negation Normal Forms+ NegNormForm,+ -- | A /Negation Normal Form/ is either a literal form, or a conjunction or a disjunction of negation normal forms.+ -- This subset of propositional formulas is a normal subset in the sense that each formula has a (bi-)equivalent+ -- negation normal form.++ isNegNormForm,+ -- | checks if a given propositional formula is in negation normal form.++ negNormForm,+ -- | is the according normalizer, i.e. it returns an equivalent negation normal form.+ -- For example,+ --+ -- > > negNormForm (N (CJ [N (SJ [A 'x', A 'y']), N T, F]))+ -- > DJ [CJ [DJ [N (A 'x'),A 'y']],CJ [],CJ []]+ -- >+ -- > > negNormForm (N (CJ [N (DJ [A 'x']), N (DJ [N (A 'x')])]))+ -- > DJ [DJ [A 'x'],DJ [N (A 'x')]]+ --+ -- This conversion is based on four laws for the removal of @T@, @F@, @SJ@ and @EJ@:+ --+ -- @T ⇔ CJ[]@+ --+ -- @F ⇔ DJ[]@+ --+ -- @[φ1 → φ2 → ... → φN] ⇔ [[-φ1 + φ2] * [-φ2 + φ3] * ...]@+ --+ -- @[φ1 ↔ φ2 ↔ ... ↔ φN] ⇔ [[φ1 * φ2 * ... * φN] + [-φ1 * -φ2 * ... * -φN]]@+ --+ -- and seven laws to remove negations other than negations of atomic formulas:+ --+ -- @-T ⇔ DJ[]@+ --+ -- @-F ⇔ CJ[]@+ --+ -- @--φ ⇔ φ@+ --+ -- @-[φ1 * φ2 * ... * φN] ⇔ [-φ1 + -φ2 + ... + -φN]@+ --+ -- @-[φ1 + φ2 + ... + φN] ⇔ [-φ1 * -φ2 * ... * -φN]@+ --+ -- @-[φ1 → φ2 → ... → φN] ⇔ [[φ1 * -φ2] + [φ2 * -φ3] + ...]@+ --+ -- @-[φ1 ↔ φ2 ↔ ... ↔ φN] ⇔ [[φ1 + φ2 + ... + φN] * [-φ1 + -φ2 + ... + -φN]]@+ --+ -- Note, that each each formula does have an biequivalent negation normal form, but our normalizer only returns equivalent+ -- forms in general. For example,+ --+ -- > > negNormForm (SJ [A 'x'])+ -- > CJ [] -- i.e. the atom 'x' is lost and this result is only equivalent++ -- ** NLCs and NLDs, CNFs and DNFs++ -- | Probably the most important and best known normal forms are the /Conjunctive Normal Forms/ or /CNFs/ and the+ -- /Disjunctive Normal Forms/ or /DNFs/. These forms are mutually /dual/, as it is called.+ --+ -- Let us consider DNFs. Usually, a DNF is defined as a disjunction of conjunctions of literals. An example DNF would then be+ --+ -- > DJ [CJ [A 'x', A 'y'], CJ [N (A 'y'), A 'y'], CJ [A 'z', N (A 'x')]]+ --+ -- But our definition of a DNF is more restrictive, because we demand each literal conjunction @CJ [λ_1, ..., λ_n]@+ -- to be a /normal literal conjunction/ in the sense that the literal atoms must be strictly ordered, i.e.+ -- @'litFormAtom' λ_1 < ... < 'litFormAtom' λ_n@.+ -- And this is obviously not the case for the second and third of the three literal conjunctions of the given example.+ --+ -- Every literal conjunction can easily be converted into a NLC, unless it contains a complementary pair of literal, such as the+ -- @CJ [N (A 'y'), A 'y']@. In that case, it is equivalent to @F@, and as a component of the disjunction, it may be removed+ -- alltogether without changing the semantics.+ -- So the example formula in a proper DNF version would be+ --+ -- > DJ [CJ [A 'x', A 'y'], CJ [A 'x', N (A 'z')]]+ --+ -- Note, that NLCs, NLDs, DNFs and CNFs are further specializations of Negation Normal Forms, so it is intuitive to introduce them+ -- as subtypes via the @type@ synonym.++ NLC,+ -- | A /normal literal conjunction/ or /NLC/ is a conjunction @CJ [λ_1, ..., λ_n]@ with+ -- @λ_1,...,λ_n :: 'LitForm' a@ and @'litFormAtom' λ_1 < ... < 'litFormAtom' λ_n@.++ isNLC,+ -- | checks if the formula is indeed a NLC. For example,+ --+ -- > > isNLC (CJ [A 'a', N (A 'b'), A 'c'])+ -- > True++ NLD,+ -- | A /normal literal disjunction/ or /NLD/ is a disjunction @DJ [λ_1, ..., λ_n]@ with+ -- @λ_1,...,λ_n :: 'LitForm' a@ and @'litFormAtom' λ_1 < ... < 'litFormAtom' λ_n@.++ isNLD,+ -- | checks if the formula is a NLD.++ CNF,+ -- | A /Conjunctive Normal Form/ or /CNF/ is a conjunction @CJ [δ_1,...,δ_n]@, of NLDs @δ_1,...,δ_n@.++ isCNF,+ -- | checks if the argument is a CNF. For example,+ --+ -- > > isCNF (CJ [DJ [A 'x', A 'y'], DJ [N (A 'x'), A 'z']])+ -- > True++ DNF,+ -- | A /Disjunctive Normal Form/ or /DNF/ is a disjunction @DJ [γ_1,...,γ_n]@ of NLCs @γ_1,...,γ_n@.++ isDNF,+ -- | checks if the argument is a DNF.++ -- ** Natural DNFs and CNFs+ -- | Recall, that 'truthTable' takes a formula and returns a 'TruthTable', and that we can use 'truthTableToDNF' to convert+ -- this into a formula, again. Combining the two steps @truthTableToDNF.truthTable@ defines a normalization of formulas into+ -- DNFs we call this the /natural DNF/ of the formula.+ --+ -- Actually, it is more common to call this the /canonic DNF/, but this title is not correct in a strict understanding of+ -- our canonizer notion.+ -- For example, the two formulas @DJ [A 'x', T]@ and @DJ [A 'y', T]@ are equivalent, but their natural DNFs are different, so+ -- 'naturalDNF' is not a semantic canonizer.+ -- By the way, iIt is not an atomic canonizer either, because e.g. @DJ [A 'x', F]@ and its natural DNF @DJ[]@ don't have+ -- the same atoms.+ --+ -- A formal characterization of all the result DNFs of 'naturalDNF' says that: a 'DNF' is a 'NaturalDNF' iff all its component+ -- NLCs are of the same length (i.e. they have the same atom set).++ NaturalDNF,+ NaturalCNF,+ isNaturalDNF,+ isNaturalCNF,+ naturalDNF,+ naturalCNF,++ -- ** Prime DNFs and CNFs++ -- | Natural DNFs are not really efficient to use, except for trivial cases, because a formula of @n@ atoms comprises up to+ -- @2^n@ NLCs, each one containing @n@ literals.+ -- In an attempt to define shorter and more efficient versions of DNFs and CNFs, we come up with two different approaches:+ -- one is the /prime/, the other one is the /minimal/ normal form. The properties of these forms are very important for+ -- our whole design. Some of them might be surprising, e.g. that prime and minimal forms are only sometimes identical, and+ -- that prime forms do make (semantic) canonizations and minimal forms do not.+ -- We first define and generate these prime forms here, minimal forms are introduced further below.++ -- *** Formal definition++ -- **** Prime Disjunctive Normal Forms++ -- | Given an arbitrary 'PropForm' @φ@, a 'DNF' @Δ = DJ [γ_1,...,γ_n]@ and any 'NLC'+ -- @γ = CJ [λ_1,...,λ_k]@, all on the same atom type. We say that+ --+ -- (1) @γ@ is a /factor/ of @Δ@, if @γ ⇒ Δ@, i.e. if @γ@ is 'subvalent' to @Δ@.+ -- (Note, that each of the components @γ_1,...,γ_n@ of @Δ@ is a factor of @Δ@.)+ --+ -- (2) @γ@ is a /prime factor/ of @Δ@, if it is a factor and there is not different factor @γ'@ of @Δ@+ -- such that @γ ⇒ γ' ⇒ Δ@.+ -- In other words, we cannot delete any of the literals @λ_1,...,λ_k@ in @γ@ without violating the+ -- subvalence @γ ⇒ Δ@.+ --+ -- (3) @Δ@ is a /Prime Disjunctive Normal Form/ or /PDNF/, if the @γ_1,...,γ_n@ are exactly all the+ -- prime factors of @Δ@.+ -- To futher remove disambiguities, we also demand that @Δ@ is /ordered/, as earlier defined, which means that+ -- @γ_1 < ... < γ_n@.+ --+ -- (4) @Δ@ is /the (ordered) PDNF/ of @φ@ iff @Δ@ is an (ordered) PDNF equivalent to @Δ@.+ --+ -- It is easy to proof that every formula @Δ@ has one and only one equivalent PDNF.+ -- So this does induce a semantic /canonization/ of propositional formulas.+ -- The canonization is not a bi-canonization, however, because the normal form is not always equiatomic.+ -- For example, @DJ [CJ []]@ is the PDNF of @EJ [A 5, A 5]@, but the atom @5@ is lost.++ -- **** Prime Conjunctive Normal Forms++ -- | This is /dual/ to the previous definition, i.e. given a formula @φ@, a 'CNF' @Γ = [δ_1,...,δ_n]@ and+ -- a 'NLD' @δ = DJ [λ_1,...,λ_k]@, then+ --+ -- (1) @δ@ is a /cofactor/ of @Γ@, if @Γ ⇒ δ@.+ --+ -- (2) @δ@ is a /prime cofactor/ of @Γ@, if it is a cofactor and we cannot delete any of the literals+ -- @λ_1,...,λ_k@ in @δ@ without violating the subvalence @Γ ⇒ δ@.+ --+ -- (3) @Γ@ is a /Prime Conjunctive Normal Form/ or /PCNF/, if the @δ_1,...,δ@ are exactly the set of all its+ -- prime cofactors, and if these cofactors are ordered.+ --+ -- (4) @Γ@ is /the (ordered) PCNF/ of @φ@ iff @Γ@ is an (ordered) PCNF equivalent to @Δ@.+ --+ -- Again, each formula has a unique equivalent PCNF.++ -- *** The Haskell types and functions++ PDNF,+ -- | is the type synonym for /Prime Disjunctive Normal Forms/ or /PDNF/s.++ PCNF,+ -- | is the type synonym for /Prime Conjunctive Normal Forms/ or /PCNF/s.++ primeDNF,+ -- | is the PDNF canonizer, i.e. it turns each given formula into its unique PDNF. For example,+ --+ -- > > primeDNF (EJ [A 'x', A 'y'])+ -- > DJ [CJ [N (A 'x'),N (A 'y')],CJ [A 'x',A 'y']]+ -- >+ -- > > display it -- "it" is the previous value in a ghci session, here the PDNF+ -- > [[-x * -y] + [x * y]]+ -- >+ -- > > primeDNF T+ -- > DJ [CJ []] -- all valid/tautological formulas have this same PDNF+ --+ -- > > primeDNF F+ -- > DJ [] -- all contradictory formulas have this same PDNF++ primeCNF,+ -- | is the PCNF canonizer, i.e. the result is the unique PCNF of the given formula. For example,+ --+ -- > > primeCNF (EJ [A 'x', A 'y'])+ -- > CJ [DJ [N (A 'x'),A 'y'],DJ [A 'x',N (A 'y')]]+ -- >+ -- > > display it -- means: display the previous formulas+ -- > [[-x + y] * [x + -y]]+ -- >+ -- > > primeCNF (EJ [A 'x', A 'x'])+ -- > CJ [] -- which is the same PCNF for all tautological formulas++ -- *** The /default/ and the /fast/ generation of Prime Normal Forms++ -- Although Prime (Disjunctive/Conjunctive) Normal Forms are generally much more compact than Natural DNFs (or Natural CNFs),+ -- the naive or /default/ method to construct them is of exponential time order.+ --+ -- ..................CONTINUEHERE!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!...............................++ validates,+ -- | We say that a valuator @v@ /validates/ a formula @p@, iff the @p@-application on @v@ is valid. In other words,+ --+ -- > (validates v p) == valid (apply p v)++ falsifies,+ -- | We say that a valuator @v@ /falsifies/ a formula @p@, iff the @p@-application on @v@ is unsatisfiable. In other words,+ --+ -- > (falsifies v p) == not (satisfiable (apply p v))++ directSubvaluators,+ -- | For example,+ --+ -- > directSubvaluators [(2,True),(4,False),(6,True)] ==+ -- > [[(2,True),(4,False)],[(2,True),(6,True)],[(4,False),(6,True)]]++ allDirectSubvalidators,+ allDirectSubfalsifiers,+ primeValuators,+ coprimeValuators,++ -- *** Reference to the fast generation of Prime Normal Forms+ -- | Note, that the PropLogic package also provides functions 'pdnf' and 'pcnf' that do exactly the same as 'primeDNF' and+ -- 'primeCNF'.+ -- .... CONTINUEHERE .....++ -- ** Minimal DNFs and CNFs+ MDNF,+ MCNF,+ minimalDNFs,+ minimalCNFs,++ -- ** Simplified DNFs and CNFs+ SimpleDNF, SimpleCNF,+ simpleDNF, simpleCNF,++ -- * Propositional algebras++ -- | ..... CONTINUEHERE .....++ -- ** @PropAlg a (PropForm a)@, the Propositional Formula Algebra++ -- | ..... CONTINUEHERE .....++ ext',++ -- ** @PropAlg a (PropForm a)@, the Truth Table Algebra++ -- | ..... CONTINUEHERE .....++ -- ** @PropAlg Void Bool@, the Boolean Value Algebra++ -- | Recall, that the /boolean/ or /bit value algebra/ is a predefined, integrated of Haskell, comprising:+ --+ -- > False, True :: Bool+ -- > not :: Bool -> Bool+ -- > (&&), (||), (<), (<=), (==), (/=), (=>), (>) :: Bool -> Bool -> Bool+ -- > and, or :: [Bool] -> Bool+ -- > compare :: Bool -> Bool -> Ordering, -- where data Ordering = LT | EQ | GT+ -- > all, any :: (a -> Bool) -> [a] -> Bool+ --+ -- ..... CONTINUEHERE .....++) where ---------------------------------------------------------------------------------------------------------------++-- import++ import qualified List as L+ import qualified Olist as O+ import qualified TextDisplay as D+ import PropLogicCore++-- formula deconstructors++ juncDeg :: PropForm a -> Int+ juncDeg (A _) = 0+ juncDeg F = 1+ juncDeg T = 2+ juncDeg (N _) = 3+ juncDeg (CJ _) = 4+ juncDeg (DJ _) = 5+ juncDeg (SJ _) = 6+ juncDeg (EJ _) = 7++ juncArgs :: PropForm a -> [PropForm a]+ juncArgs (A x) = [A x]+ juncArgs F = []+ juncArgs T = []+ juncArgs (N p) = [p]+ juncArgs (CJ pL) = pL+ juncArgs (DJ pL) = pL+ juncArgs (SJ pL) = pL+ juncArgs (EJ pL) = pL++ juncCons :: Int -> [PropForm a] -> PropForm a+ juncCons 0 [A x] = A x+ juncCons 1 [] = F+ juncCons 2 [] = T+ juncCons 3 [p] = N p+ juncCons 4 pL = CJ pL+ juncCons 5 pL = DJ pL+ juncCons 6 pL = SJ pL+ juncCons 7 pL = EJ pL++-- size++ atomSize :: PropForm a -> Int+ atomSize (A a) = 1+ atomSize F = 0+ atomSize T = 0+ atomSize (N p) = atomSize p+ atomSize (CJ ps) = sum (map atomSize ps)+ atomSize (DJ ps) = sum (map atomSize ps)+ atomSize (SJ ps) = sum (map atomSize ps)+ atomSize (EJ ps) = sum (map atomSize ps)++ juncSize :: PropForm a -> Int+ juncSize (A a) = 0+ juncSize F = 1+ juncSize T = 1+ juncSize (N p) = 1 + (juncSize p)+ juncSize (CJ ps) = 1 + sum (map juncSize ps)+ juncSize (DJ ps) = 1 + sum (map juncSize ps)+ juncSize (SJ ps) = 1 + sum (map juncSize ps)+ juncSize (EJ ps) = 1 + sum (map juncSize ps)++ size :: PropForm a -> Int+ size f = (atomSize f) + (juncSize f)++-- valuators and truth tables++ type LiteralPair a = (a,Bool)++ type Valuator a = O.Olist (LiteralPair a)++ type TruthTable a = (O.Olist a, Maybe (PropForm a), [([Bool],Bool)])++ type MultiTruthTable a = (O.Olist a, [PropForm a], [([Bool], [Bool])])++-- type correctness checking++ correctValuator :: Ord a => [LiteralPair a] -> Valuator a+ correctValuator [] = []+ correctValuator [(a,b)] = [(a,b)]+ correctValuator ((a1,b1):(a2,b2):pL) = case compare a1 a2 of+ LT -> (a1,b1) : (correctValuator ((a2,b2):pL))+ EQ -> error "correctValuator: multiple occurring atoms"+ GT -> error "correctValuator: atoms are not in order"++ correctTruthTable :: Ord a => ([a], Maybe (PropForm a), [([Bool],Bool)]) -> TruthTable a+ correctTruthTable (atomL, p, rowL) =+ if O.isOlist atomL+ then if dualPower (length atomL) == length rowL+ then if Prelude.all (\ (bL,b) -> (length bL) == (length atomL)) rowL+ then if O.isOlist (fst (unzip rowL))+ then if O.included (atomList p) atomL+ then (atomL, p, rowL)+ else error "correctTruthTable -- not all atoms of the formula are in the given atom list"+ else error "correctTruthTable -- valuators are not in strict order"+ else error "correctTruthTable -- some rows are not well-formed"+ else error "correctTruthTable -- wrong number of rows"+ else error "correctTruthTable -- atom list is not in strict order"+ where dualPower n = if n == 0+ then 1+ else 2 * (dualPower (n - 1))+ atomList Nothing = []+ atomList (Just p) = atoms p++ correctMultiTruthTable :: Ord a => ([a], [PropForm a], [([Bool], [Bool])]) -> MultiTruthTable a+ correctMultiTruthTable (atomL, pL, rowL) =+ if O.isOlist atomL+ then if dualPower (length atomL) == length rowL+ then if Prelude.all (\ (bL,rL) -> ((length bL)==(length atomL) && (length rL)==(length pL))) rowL+ then if O.isOlist (fst (unzip rowL))+ then if Prelude.all (\ p -> O.included (atoms p) atomL) pL+ then (atomL, pL, rowL)+ else error "correctMultiTruthTable -- some atoms in the formulas are not in the atom list"+ else error "correctMultiTruthTable -- valuators are not in strict order"+ else error "correctMultiTruthTable -- some rows are not well-formed"+ else error "correctMultiTruthTable -- wrong number of rows"+ else error "correctMultiTruthTable -- atom list is not in strict order"+ where dualPower n = if n == 0+ then 1+ else 2 * (dualPower (n - 1))++-- Display instances++ instance D.Display a => D.Display (LiteralPair a) where+ textFrame (a,b) = D.textFrame [(a,b)]++ instance D.Display a => D.Display (Valuator a) where+ textFrame litL = D.textFrameBox (D.plainMerge (D.normalTextFrameTable (map litRow litL)))+ where boolTextFrame b = if b then ["1"] else ["0"]+ litRow (a,b) = [D.textFrame a, [" = "], boolTextFrame b]++ instance (Ord a, D.Display a) => D.Display [Valuator a] where+ textFrame vL = textFrame+ where atomL = O.olist (concat (map (fst . unzip) vL))+ headRow = map D.textFrame atomL+ bodyRow _ [] = []+ bodyRow [] (a':atomL) = [""] : (bodyRow [] atomL)+ bodyRow ((a,b):litL) (a':atomL) = case compare a a' of+ EQ -> (D.textFrame b) : (bodyRow litL atomL)+ GT -> [] : (bodyRow ((a,b):litL) atomL)+ textFrameTable = headRow : (map (\ valuator -> (bodyRow valuator atomL)) vL)+ textFrame = D.gridMerge (D.normalTextFrameTable textFrameTable)++ instance D.Display a => D.Display (TruthTable a) where+ textFrame (atomL, maybeForm, pairL) = textFrame+ where formTF = case maybeForm of+ Nothing -> [""]+ Just form -> D.textFrame form+ headRow = (map D.textFrame atomL) ++ [formTF]+ bodyRow (boolL,b) = (map D.textFrame boolL) ++ [D.textFrame b]+ textFrameTable = [headRow] ++ (map bodyRow pairL)+ textFrame = D.gridMerge (D.normalTextFrameTable textFrameTable)++ instance D.Display a => D.Display (MultiTruthTable a) where+ textFrame (atomL, formL, pairL) = textFrame'+ where ordinalList = map (\ n -> [" " ++ (show n) ++ ". "]) (take (length formL) [1..]) :: [D.TextFrame]+ formBlock = D.plainMerge (D.centerAlign (D.leftAlign (L.transpose [ordinalList, map D.textFrame formL])))+ headRow = (map D.textFrame atomL) ++ ordinalList+ bodyRow (bL1, bL2) = (map D.textFrame bL1) ++ (map D.textFrame bL2)+ textFrameTable = [headRow] ++ (map bodyRow pairL)+ tableBlock = D.gridMerge (D.normalTextFrameTable textFrameTable)+ textFrame = D.correctTextFrame (["MultiTruthTable"] ++ formBlock ++ tableBlock)+ textFrame' = D.textFrameBox textFrame++-- literal normal forms and semantic type conversion++ valuatorToNLC :: Valuator a -> NLC a+ valuatorToNLC pairL = CJ (map litForm pairL)+ where litForm (x,True) = A x+ litForm (x,False) = N (A x)++ valuatorToNLD :: Valuator a -> NLD a+ -- Note, that the literals are inverted!+ valuatorToNLD pairL = DJ (map litForm pairL)+ where litForm (x,True) = N (A x)+ litForm (x,False) = A x++ valuatorListToCNF :: [Valuator a] -> CNF a+ valuatorListToCNF vL = CJ (map valuatorToNLD vL)++ valuatorListToDNF :: [Valuator a] -> DNF a+ valuatorListToDNF vL = DJ (map valuatorToNLC vL)++ nlcToValuator :: NLC a -> Valuator a+ nlcToValuator (CJ litL) = map litPair litL+ where litPair (N (A a)) = (a,False)+ litPair (A a) = (a,True)++ nldToValuator :: NLD a -> Valuator a+ nldToValuator (DJ litL) = map litPair litL+ where litPair (N (A a)) = (a,True) -- The literal values are inverted!+ litPair (A a) = (a,False) -- The literal values are inverted!++ cnfToValuatorList :: CNF a -> [Valuator a]+ cnfToValuatorList (CJ pL) = map nldToValuator pL++ dnfToValuatorList :: DNF a -> [Valuator a]+ dnfToValuatorList (DJ pL) = map nlcToValuator pL++ truthTableZeroValuators :: TruthTable a -> [Valuator a]+ truthTableZeroValuators (atomL, _, pairL) =+ map (\ (bitL, b) -> zip atomL bitL) (filter (\ (bitL,b) -> (not b)) pairL)++ truthTableUnitValuators :: TruthTable a -> [Valuator a]+ truthTableUnitValuators (atomL, _, pairL) =+ map (\ (bitL, b) -> zip atomL bitL) (filter (\ (bitL,b) -> b) pairL)++-- valuators++ allValuators :: Ord a => [a] -> O.Olist (Valuator a)+ allValuators aL = iter (O.olist aL)+ where iter [] = [[]]+ iter (a:aL) = let vL = iter aL+ in (map (\ v -> (a,False):v) vL) ++ (map (\ v -> (a,True):v) vL)++ unitValuators :: Ord a => PropForm a -> O.Olist (Valuator a)+ unitValuators p = filter (boolApply p) (allValuators (atoms p))++ zeroValuators :: Ord a => PropForm a -> O.Olist (Valuator a)+ zeroValuators p = filter (not . (boolApply p)) (allValuators (atoms p))++-- basic propositional semantics++ valuate :: Ord a => Valuator a -> PropForm a -> PropForm a+ valuate v (A x) = case (L.lookup x v) of+ Nothing -> (A x)+ Just False -> F+ Just True -> T+ valuate v F = F+ valuate v T = T+ valuate v (N p)= N (valuate v p)+ valuate v (CJ pL) = CJ (map (valuate v) pL)+ valuate v (DJ pL) = DJ (map (valuate v) pL)+ valuate v (SJ pL) = SJ (map (valuate v) pL)+ valuate v (EJ pL) = EJ (map (valuate v) pL)++ boolEval :: PropForm a -> Bool+ boolEval p = let pairwise rel [] = True+ pairwise rel [x] = True+ pairwise rel (x:y:zL) = (rel x y) && (pairwise rel (y:zL))+ in case p of+ (A a) -> error "boolEval: only defined for nullatomic formulas"+ F -> False+ T -> True+ (N p) -> not (boolEval p)+ (CJ pL) -> and (map boolEval pL)+ (DJ pL) -> or (map boolEval pL)+ (SJ pL) -> pairwise (<=) (map boolEval pL)+ (EJ pL) -> pairwise (==) (map boolEval pL)++ boolApply :: Ord a => PropForm a -> Valuator a -> Bool+ boolApply form valuator = boolEval (valuate valuator form)++-- truth tables and propositional formulas++ truthTable :: Ord a => PropForm a -> TruthTable a+ truthTable p = theTable+ where atomL = atoms p+ vL = allValuators atomL+ makeRow v = (snd (unzip v), boolApply p v)+ theTable = (atomL, Just p, map makeRow vL)++ plainTruthTable :: Ord a => PropForm a -> TruthTable a+ plainTruthTable p = theTable+ where atomL = atoms p+ vL = allValuators atomL+ makeRow v = (snd (unzip v), boolApply p v)+ theTable = (atomL, Nothing, map makeRow vL)++ truthTableBy :: Ord a => PropForm a -> [a] -> (Valuator a -> Bool) -> TruthTable a+ truthTableBy p aL boolFun = theTable+ where atomL = O.olist aL+ vL = allValuators atomL+ makeRow v = (snd (unzip v), boolFun v)+ theTable = (atomL, Nothing, map makeRow vL)++ multiTruthTable :: Ord a => [PropForm a] -> MultiTruthTable a+ multiTruthTable pL = theTable+ where atomL = O.unionList (map atoms pL)+ vL = allValuators atomL+ makeRow v = (snd (unzip v), map (\ p -> boolApply p v) pL)+ theTable = (atomL, pL, map makeRow vL)++ truthTableToDNF :: TruthTable a -> NaturalDNF a+ truthTableToDNF = valuatorListToDNF . truthTableUnitValuators++ truthTableToCNF :: TruthTable a -> NaturalCNF a+ truthTableToCNF = valuatorListToCNF . truthTableZeroValuators++-- auxiliary atom functions++ isRedundantAtom :: (Ord a) => a -> PropForm a -> Bool+ isRedundantAtom a p = equivalent (valuate [(a,False)] p) (valuate [(a,True)] p)++ infRedTruthTable :: (Ord a) => PropForm a -> [a] -> TruthTable a+ infRedTruthTable p aL = truthTableBy p aL isValidator+ where isValidator v = valid (valuate v p)++ supRedTruthTable :: (Ord a) => PropForm a -> [a] -> TruthTable a+ supRedTruthTable p aL = truthTableBy p aL isSatisfier+ where isSatisfier v = satisfiable (valuate v p)++-------------------------------------------- NORMAL FORMS ------------------------------------------------------------++-- The syntactic order on formulas and ordered normal forms++ instance Ord a => Ord (PropForm a) where+ compare (A x) (A y) = compare x y+ compare (N (A x)) (N (A y)) = compare x y+ compare (N (A x)) (A y) = case compare x y of+ LT -> LT+ GT -> GT+ EQ -> LT+ compare (A x) (N (A y)) = case compare x y of+ LT -> LT+ GT -> GT+ EQ -> GT+ compare p q = case compare (juncDeg p) (juncDeg q) of+ LT -> LT+ GT -> GT+ EQ -> lexCompare (juncArgs p) (juncArgs q)+ where lexCompare [] [] = EQ+ lexCompare [] _ = LT+ lexCompare _ [] = GT+ lexCompare (p:pL) (q:qL) = case compare p q of+ EQ -> lexCompare pL qL+ LT -> LT+ GT -> GT++ type OrdPropForm a = PropForm a++ isOrdPropForm :: Ord a => PropForm a -> Bool+ isOrdPropForm (A a) = True+ isOrdPropForm F = True+ isOrdPropForm T = True+ isOrdPropForm (N p) = isOrdPropForm p+ isOrdPropForm (CJ pL) = (all isOrdPropForm pL) && O.isOlist pL+ isOrdPropForm (DJ pL) = (all isOrdPropForm pL) && O.isOlist pL+ isOrdPropForm (SJ pL) = (all isOrdPropForm pL)+ isOrdPropForm (EJ pL) = (all isOrdPropForm pL)++ ordPropForm :: Ord a => PropForm a -> OrdPropForm a+ ordPropForm (A a) = (A a)+ ordPropForm F = F+ ordPropForm T = T+ ordPropForm (N p) = (N p)+ ordPropForm (CJ pL) = CJ (O.olist (map ordPropForm pL))+ ordPropForm (DJ pL) = DJ (O.olist (map ordPropForm pL))+ ordPropForm (SJ pL) = SJ (map ordPropForm pL)+ ordPropForm (EJ pL) = EJ (map ordPropForm pL)++-- Eval Norm Form++ type EvalNF a = PropForm a++ hasTrivialJuncs :: PropForm a -> Bool+ hasTrivialJuncs (A _) = False+ hasTrivialJuncs F = False+ hasTrivialJuncs T = False+ hasTrivialJuncs (N p) = hasTrivialJuncs p+ hasTrivialJuncs (CJ pL) = ((length pL) < 2) || or (map hasTrivialJuncs pL)+ hasTrivialJuncs (DJ pL) = ((length pL) < 2) || or (map hasTrivialJuncs pL)+ hasTrivialJuncs (SJ pL) = ((length pL) < 2) || or (map hasTrivialJuncs pL)+ hasTrivialJuncs (EJ pL) = ((length pL) < 2) || or (map hasTrivialJuncs pL)++ hasBitValues :: PropForm a -> Bool+ hasBitValues (A _) = False+ hasBitValues F = True+ hasBitValues T = True+ hasBitValues (N p) = hasBitValues p+ hasBitValues (CJ pL) = or (map hasBitValues pL)+ hasBitValues (DJ pL) = or (map hasBitValues pL)+ hasBitValues (SJ pL) = or (map hasBitValues pL)+ hasBitValues (EJ pL) = or (map hasBitValues pL)++ isEvalNF :: PropForm a -> Bool+ isEvalNF F = True+ isEvalNF T = True+ isEvalNF p = not (hasTrivialJuncs p) && not (hasBitValues p)++-- generalized evaluation and application++ eval :: PropForm a -> EvalNF a+ eval (A a) = (A a)+ eval F = F+ eval T = T+ eval (N p) = case (eval p) of+ F -> T+ T -> F+ q -> (N q)+ eval (CJ ps) = cjEval([],ps)+ eval (DJ ps) = djEval([],ps)+ eval (SJ ps) = sjEval([],ps)+ eval (EJ ps) = ejEval([],ps)++ cjEval :: ([PropForm a],[PropForm a]) -> PropForm a+ cjEval([],[]) = T+ cjEval([p],[]) = p+ cjEval(ps,[]) = (CJ ps)+ cjEval(ps,q:qs) = case (eval q) of+ F -> F+ T -> cjEval(ps, qs)+ r -> cjEval(ps ++ [r], qs)++ djEval :: ([PropForm a],[PropForm a]) -> PropForm a+ djEval([],[]) = F+ djEval([p],[]) = p+ djEval(ps,[]) = (DJ ps)+ djEval(ps,q:qs) = case (eval q) of+ F -> djEval(ps, qs)+ T -> T+ r -> djEval(ps ++ [r], qs)++ sjEval :: ([PropForm a],[PropForm a]) -> PropForm a+ sjEval([],[]) = T+ sjEval([p],[]) = T+ sjEval(ps,[]) = (SJ ps)+ sjEval(ps,q:qs) = case (eval q) of+ F -> cjEval(map N ps, [SJ qs])+ T -> cjEval([SJ ps], qs)+ r -> sjEval(ps++[r], qs)++ ejEval :: ([PropForm a],[PropForm a]) -> PropForm a+ ejEval([],[]) = T+ ejEval([p],[]) = T+ ejEval(ps,[]) = (EJ ps)+ ejEval(ps,q:qs) = case (eval q) of+ F -> cjEval(map N ps, map N qs)+ T -> cjEval(ps, qs)+ r -> ejEval(ps ++ [r], qs)++ apply :: Ord a => PropForm a -> Valuator a -> EvalNF a+ apply form valuator = eval (valuate valuator form)++-- Literal form(ula)s++ type LitForm a = PropForm a++ isLitForm :: PropForm a -> Bool+ isLitForm p = case p of+ A a -> True+ N (A a) -> True+ _ -> False++ litFormAtom :: LitForm a -> a+ litFormAtom (A a) = a+ litFormAtom (N (A a)) = a+ litFormAtom _ = error "litFormAtom -- not a LitForm "++ litFormValue :: LitForm a -> Bool+ litFormValue (A a) = True+ litFormValue (N (A a)) = False+ litFormValue _ = error "litFormAtom -- not a LitForm "++-- Negation Normal Forms++ type NegNormForm a = PropForm a++ isNegNormForm :: PropForm a -> Bool+ isNegNormForm (A _) = True+ isNegNormForm F = True+ isNegNormForm T = True+ isNegNormForm (N (A _)) = True+ isNegNormForm (N _) = False+ isNegNormForm (CJ pL) = Prelude.all isNegNormForm pL+ isNegNormForm (DJ pL) = Prelude.all isNegNormForm pL+ isNegNormForm (SJ _) = False+ isNegNormForm (EJ _) = False++ negNormForm :: PropForm a -> NegNormForm a+ negNormForm (A a) = (A a)+ negNormForm F = DJ []+ negNormForm T = CJ []+ negNormForm (CJ pL) = CJ (map negNormForm pL)+ negNormForm (DJ pL) = DJ (map negNormForm pL)+ negNormForm (SJ pL) = let iter [] = []+ iter [p] = []+ iter (p1:p2:pL) = (DJ [negNormForm (N p1), negNormForm p2]) : iter (p2:pL)+ in CJ (iter pL)+ negNormForm (EJ pL) = DJ [CJ (map negNormForm pL), CJ (map (negNormForm . N) pL)]+ negNormForm (N (A a)) = N (A a)+ negNormForm (N F) = CJ []+ negNormForm (N T) = DJ []+ negNormForm (N (N p)) = negNormForm p+ negNormForm (N (CJ pL)) = DJ (map (negNormForm . N) pL)+ negNormForm (N (DJ pL)) = CJ (map (negNormForm . N) pL)+ negNormForm (N (SJ pL)) = let iter [] = []+ iter [p] = []+ iter (p1:p2:pL) = (CJ [negNormForm p1, negNormForm (N p2)]) : iter (p2:pL)+ in DJ (iter pL)+ negNormForm (N (EJ pL)) = CJ [DJ (map negNormForm pL), DJ (map (negNormForm . N) pL)]++-- literal forms, NLCs, NLDs, DNFs and CNFs++ type NLC a = NegNormForm a++ type NLD a = NegNormForm a++ type CNF a = NegNormForm a++ type DNF a = NegNormForm a++ isNLC :: Ord a => PropForm a -> Bool+ isNLC (CJ pL) = (all isLitForm pL) && O.isOlist (map litFormAtom pL)+ isNLC _ = False++ isNLD :: Ord a => PropForm a -> Bool+ isNLD (DJ pL) = (all isLitForm pL) && O.isOlist (map litFormAtom pL)+ isNLD _ = False++ isCNF :: Ord a => PropForm a -> Bool+ isCNF (CJ pL) = all isNLD pL+ isCNF _ = False++ isDNF :: Ord a => PropForm a -> Bool+ isDNF (DJ pL) = all isNLC pL+ isDNF _ = False++-- Natural DNFs and CNFs++ type NaturalCNF a = CNF a++ type NaturalDNF a = DNF a++ isNaturalDNF :: Ord a => PropForm a -> Bool+ isNaturalDNF (DJ pL) = isDNF (DJ pL) && (Prelude.all fullAtomSet pL)+ where fullAtomSet q = O.equal (atoms (DJ pL)) (atoms q)+ isNaturalDNF _ = False++ isNaturalCNF :: Ord a => PropForm a -> Bool+ isNaturalCNF (CJ pL) = isCNF (CJ pL) && (Prelude.all fullAtomSet pL)+ where fullAtomSet q = O.equal (atoms (CJ pL)) (atoms q)+ isNaturalCNF _ = False++ naturalDNF :: Ord a => PropForm a -> NaturalDNF a+ naturalDNF = truthTableToDNF . truthTable++ naturalCNF :: Ord a => PropForm a -> NaturalCNF a+ naturalCNF = truthTableToCNF . truthTable++-- Prime DNFs and CNFs++ type PDNF a = DNF a++ type PCNF a = CNF a++ validates :: Ord a => Valuator a -> PropForm a -> Bool+ validates v p = valid (eval (valuate v p))++ falsifies :: Ord a => Valuator a -> PropForm a -> Bool+ falsifies v p = not (satisfiable (eval (valuate v p)))++ directSubvaluators :: Valuator a -> [Valuator a]+ directSubvaluators v = iter([],v)+ where iter(_,[]) = []+ iter(u,p:w) = iter(u ++ [p],w) ++ [u ++ w]++ allDirectSubvalidators :: Ord a => Valuator a -> PropForm a -> [Valuator a]+ allDirectSubvalidators v p = filter (\ v -> (validates v p)) (directSubvaluators v)++ allDirectSubfalsifiers :: Ord a => Valuator a -> PropForm a -> [Valuator a]+ allDirectSubfalsifiers v p = filter (\ v -> (falsifies v p)) (directSubvaluators v)++ primeValuators :: Ord a => PropForm a -> [Valuator a]+ primeValuators p = iter([],[],unitValuators p)+ where iter(primes,[],[]) = reverse primes+ iter(primes,validators,[]) = iter(primes,[],L.nub validators)+ iter(primes,validators,v:vL) = case (allDirectSubvalidators v p) of+ [] -> iter(v:primes,validators,vL)+ wL -> iter(primes,validators ++ wL,vL)++ coprimeValuators :: Ord a => PropForm a -> [Valuator a]+ coprimeValuators p = iter([],[],zeroValuators p)+ where iter(coprimes,[],[]) = reverse coprimes+ iter(coprimes,falsifiers,[]) = iter(coprimes,[],L.nub falsifiers)+ iter(coprimes,falsifiers,v:vL) = case (allDirectSubfalsifiers v p) of+ [] -> iter(v:coprimes,falsifiers,vL)+ wL -> iter(coprimes,falsifiers ++ wL,vL)++ primeDNF :: Ord a => PropForm a -> PDNF a+ primeDNF = ordPropForm . valuatorListToDNF . primeValuators++ primeCNF :: Ord a => PropForm a -> PCNF a+ primeCNF = ordPropForm . valuatorListToCNF . coprimeValuators++-- Minimal DNFs and CNFs++ type MDNF a = DNF a++ type MCNF a = CNF a++ equivDirectSubDNFs :: Ord a => DNF a -> [DNF a]+ equivDirectSubDNFs (DJ nlcL) = iter nlcL []+ where iter [] nlcL' = []+ iter (nlc:nlcL) nlcL' = if subvalent nlc (DJ (nlcL ++ nlcL'))+ then (DJ (nlcL ++ nlcL')) : (iter nlcL (nlc : nlcL'))+ else iter nlcL (nlc : nlcL')++ minimalEquivalentIncludedDNFs :: Ord a => DNF a -> [DNF a]+ minimalEquivalentIncludedDNFs dnf = nextStep [] [] [dnf]+ where nextStep finalDnfs [] [] = O.olist finalDnfs+ nextStep finalDnfs nextDnfs [] = nextStep finalDnfs [] (O.olist nextDnfs)+ nextStep finalDnfs nextDnfs (dnf:dnfL) = case equivDirectSubDNFs dnf of+ [] -> nextStep (dnf:finalDnfs) nextDnfs dnfL+ dnfL' -> nextStep finalDnfs (nextDnfs ++ dnfL') dnfL++ equivDirectSubCNFs :: Ord a => CNF a -> [CNF a]+ equivDirectSubCNFs (CJ nldL) = iter nldL []+ where iter [] nldL' = []+ iter (nld:nldL) nldL' = if subvalent (CJ (nldL ++ nldL')) nld+ then (CJ (nldL ++ nldL')) : (iter nldL (nld : nldL'))+ else iter nldL (nld : nldL')++ minimalEquivalentIncludedCNFs :: Ord a => CNF a -> [CNF a]+ minimalEquivalentIncludedCNFs cnf = nextStep [] [] [cnf]+ where nextStep finalCnfs [] [] = O.olist finalCnfs+ nextStep finalCnfs nextCnfs [] = nextStep finalCnfs [] (O.olist nextCnfs)+ nextStep finalCnfs nextCnfs (cnf:cnfL) = case equivDirectSubCNFs cnf of+ [] -> nextStep (cnf:finalCnfs) nextCnfs cnfL+ cnfL' -> nextStep finalCnfs (nextCnfs ++ cnfL') cnfL++ minimalDNFs :: Ord a => PropForm a -> [MDNF a]+ minimalDNFs = minimalEquivalentIncludedDNFs . primeDNF++ minimalCNFs :: Ord a => PropForm a -> [MCNF a]+ minimalCNFs = minimalEquivalentIncludedCNFs . primeCNF++-- Simplified DNFs and CNFs++ type SimpleDNF a = PropForm a++ type SimpleCNF a = PropForm a++ simpleDNF :: Ord a => DNF a -> SimpleDNF a+ simpleDNF p = if isDNF p+ then eval p+ else error "simpleDNF -- argument is not a DNF"++ simpleCNF :: Ord a => CNF a -> SimpleCNF a+ simpleCNF p = if isCNF p+ then eval p+ else error "simpleCNF -- argument is not a CNF"++-------------------------------- PROPOSITIONAL ALGEBRAS ---------------------------------------------------------------++-- the propositional algebra of propositional formulas++ instance Ord a => PropAlg a (PropForm a) where+ at = A+ false = F+ true = T+ neg = N+ conj = CJ+ disj = DJ+ subj = SJ+ equij = EJ+ valid p = and resultColumn+ where (atomL, maybeProp, pairL) = truthTable p+ resultColumn = snd (unzip pairL)+ satisfiable p = or resultColumn+ where (atomL, maybeProp, pairL) = truthTable p+ resultColumn = snd (unzip pairL)+ subvalent p1 p2 = valid (SJ [p1,p2])+ equivalent p1 p2 = valid (EJ [p1,p2])+ covalent p1 p2 = satisfiable (CJ [p1,p2])+ disvalent p1 p2 = not (satisfiable (CJ [p1,p2]))+ properSubvalent p1 p2 = (subvalent p1 p2) && not (equivalent p1 p2)+ properDisvalent p1 p2 = (disvalent p1 p2) && satisfiable p1 && satisfiable p2+ atoms (A a) = [a]+ atoms F = []+ atoms T = []+ atoms (N p) = atoms p+ atoms (CJ pL) = O.unionList (map atoms pL)+ atoms (DJ pL) = O.unionList (map atoms pL)+ atoms (SJ pL) = O.unionList (map atoms pL)+ atoms (EJ pL) = O.unionList (map atoms pL)+ redAtoms p = filter (\ a -> isRedundantAtom a p) (atoms p)+ irrAtoms p = filter (\ a -> not (isRedundantAtom a p)) (atoms p)+ ext p aL = if null aL+ then p+ else CJ [p, DJ (T : (map A aL))]+ infRed p aL =+ let cnf = truthTableToCNF (infRedTruthTable p aL)+ in if cnf == CJ []+ then DJ (T : (map A aL))+ else cnf+ supRed p aL =+ let dnf = truthTableToDNF (supRedTruthTable p aL)+ in if dnf == DJ []+ then CJ (F : (map A aL))+ else dnf+ infElim p aL = infRed p (O.difference (atoms p) (O.olist aL))+ supElim p aL = supRed p (O.difference (atoms p) (O.olist aL))+ toPropForm = id+ fromPropForm = id++-- alternative version of the extension++ ext' :: PropForm a -> O.Olist a -> PropForm a+ ext' p aL = if null aL+ then p+ else DJ [p, CJ (F : (map A aL))]++-- the propositional algebra of truth tables++ instance Ord a => PropAlg a (TruthTable a) where+ at x = plainTruthTable (A x)+ false = plainTruthTable F+ true = plainTruthTable T+ neg (atomL, _, pairL) = (atomL, Nothing, pairL')+ where pairL' = map (\ (bL,b) -> (bL, not b)) pairL+ conj ttL = plainTruthTable (conj (map toPropForm ttL))+ disj ttL = plainTruthTable (disj (map toPropForm ttL))+ subj ttL = plainTruthTable (subj (map toPropForm ttL))+ equij ttL = plainTruthTable (equij (map toPropForm ttL))+ valid (atomL, _, pairL) = Prelude.and (snd (unzip pairL))+ satisfiable (atomL, _, pairL) = Prelude.or (snd (unzip pairL))+ subvalent tt1 tt2 = subvalent (toPropForm tt1) (toPropForm tt2)+ equivalent tt1 tt2 = equivalent (toPropForm tt1) (toPropForm tt2)+ covalent tt1 tt2 = covalent (toPropForm tt1) (toPropForm tt2)+ disvalent tt1 tt2 = disvalent (toPropForm tt1) (toPropForm tt2)+ properSubvalent tt1 tt2 = properSubvalent (toPropForm tt1) (toPropForm tt2)+ properDisvalent tt1 tt2 = properDisvalent (toPropForm tt1) (toPropForm tt2)+ atoms (atomL, _, _) = atomL+ redAtoms tt = redAtoms (toPropForm tt)+ irrAtoms tt = irrAtoms (toPropForm tt)+ ext tt aL = truthTable (ext (toPropForm tt) aL)+ infRed tt aL = truthTable (infRed (toPropForm tt) aL)+ supRed tt aL = truthTable (supRed (toPropForm tt) aL)+ infElim tt aL = truthTable (infElim (toPropForm tt) aL)+ supElim tt aL = truthTable (supElim (toPropForm tt) aL)+ toPropForm = truthTableToDNF+ fromPropForm = truthTable++-- The propositional algebra of boolean values++ newtype Void = Void Void+ deriving (Show, Read, Eq, Ord)++ instance PropAlg Void Bool where+ at _ = undefined+ false = False+ true = True+ neg = not+ conj = and+ disj = or+ subj bL = case bL of+ [] -> True+ [b] -> True+ (b1:b2:bL) -> (b1 <= b2) && subj (b2:bL)+ equij bL = case bL of+ [] -> True+ [b] -> True+ (b1:b2:bL) -> (b1 == b2) && equij (b2:bL)+ valid = id+ satisfiable = id+ subvalent = (<=)+ equivalent = (==)+ covalent = (&&)+ disvalent = (/=)+ properSubvalent = (<)+ properDisvalent _ _ = False+ atoms _ = []+ redAtoms _ = []+ irrAtoms _ = []+ ext b _ = b+ infRed b _ = b+ supRed b _ = b+ infElim b _ = b+ supElim b _ = b+ toPropForm b = if b then T else F+ fromPropForm p = if nullatomic p+ then boolEval p+ else error "fromPropForm -- formula is not nullatomic"
+ FastPropLogic.hs view
@@ -0,0 +1,1278 @@+{-# LANGUAGE TypeSynonymInstances, FlexibleInstances, MultiParamTypeClasses #-}+++-- |+-- This module defines three altenative representations for certain propositional normal forms, namely+--+-- > data XPDNF a -- a representation for Prime Disjunctive Normal Forms or PDNF's on a given atom type a+-- > data XPCNF a -- a representation for Prime Disjunctive Normal Forms or PDNF's on a given atom type a+-- > data MixForm a -- a type made of pairwise minimal DNF's and CNF's on a given atom type a+--+-- For each of these types there is a converter from and a converter to propositional formulas+--+-- > fromXPDNF :: Ord a => XPDNF a -> PropForm a toXPDNF :: Ord a => PropForm a -> XPDNF a+-- > fromXPCNF :: Ord a => XPCNF a -> PropForm a toXPCNF :: Ord a => PropForm a -> XPCNF a+-- > fromMixForm :: Ord a => MixForm a -> PropForm a toMixForm :: Ord a => PropForm a -> MixForm a+--+-- Each of these three types is turned into a propositional algebra 'PropAlg', i.e. for every ordered type @a@ of /atoms/+-- we have three instances+--+-- > PropAlg a (XPDNF a)+-- > PropAlg a (XPCNF a)+-- > PropAlg a (MixForm a)+--+-- Different to the two default propositional algebras on propositional formulas and truth tables, these three algebras comprise fast+-- function implementations and thus provide practical versions for propositional algebras, where propositions of arbitrary size+-- are processed in reasonable time.+-- In more detail the involved complexities are given in the table below (see ......).+-- It also explains, which of the three algebras should be chosen in an actual application.+--+-- Actually, this module is essentially a re-implementation of already explained concepts from "PropLogicCore" and "DefaultPropLogic"+-- and for the user it shouldn't be necessary to further explain how the algorithms work.+-- The remainder of this document is an attempt to do just that.+-- However, if you at least want an idea of what is going on here, it may suffice to read the first section with the introductory+-- example below.++{-+ This module defines three altenative representations for certain propositional normal forms, namely++ 'XPDNF' a representation for Prime Disjunctive Normal Forms 'DefaultPropLogic.PDNF',+ 'XPCNF' a representation for Prime Conjunctive Normal Forms 'DefaultPropLogic.PCNF', and+ 'MixForm' a type comprising pairwise minimal DNFs and CNFs.++ For each of these types there is a converter from and a converter to propositional formulas 'PropLogicCore.PropForm'.+ For example, for 'XPDNF' this is @fromXPDNF :: XPDNF a -> PropForm a@ and @toXPDNF :: PropForm a -> XPDNF a@.++ Each of these three types is turned into a propositional algebra, i.e. it becomes an instance of 'PropLogicCore.PropAlg'.+ Different to the two default propositional algebras on propositional formulas and truth tables (see 'DefaultPropLogic.PropForm' and 'DefaultPropLogic.TruthTable'), these three algebras comprise fast function implementations and thus provide practical versions for propositional algebras for propositions of any size, not just for formulas with very small atoms sets.+-}++module FastPropLogic (++ -- * Introductory example++ -- ** Generating a Prime Disjunctive Normal Form, the default and the fast way++ -- | Recall, that we already defined /Disjunctive Normal Forms/ and /Prime Disjunctive Normal Forms/ in "DefaultPropLogic" as+ -- special versions of propositional formulas, along with a canonizer @pdnf@ to obtain these normal forms+ --+ -- > type DNF a = PropForm a+ -- > type PDNF a = DNF a+ -- > pdnf :: PropForm a -> PDNF a+ --+ -- For a simple example formula @p@, given by+ --+ -- > > p = DJ [EJ [A "x", A "y"], N (A "z")] :: PropForm String+ --+ -- more conveniently displayed by+ --+ -- > > display p+ -- > [[x <-> y] + -z]+ --+ -- the PDNF of @p@ is then generated by+ --+ -- > > pdnf p+ -- > DJ [CJ [EJ [A "x",F],EJ [A "y",F]],CJ [EJ [A "x",T],EJ [A "y",T]],CJ [EJ [A "z",F]]]+ -- > > display (pdnf p)+ -- > [[[x <-> false] * [y <-> false]] + [[x <-> true] * [y <-> true]] + [* [z <-> false]]]+ --+ -- or more conveniently displayed in its evaluated form+ --+ -- > > display (eval (pdnf p))+ -- > [[-x * -y] + [x * y] + -z]+ --+ -- .............!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!..............................+ --+ -- (Actually, each converter pair is also part of each of the given algebras. For example, in the XPDNF instance holds:+ -- 'fromXPDNF' = 'toPropForm' and 'toXPDNF' = 'fromPropForm'.)+ --++ -- ** XPDNF as a propositional algebra+ --+ -- | ,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,++ -- ** The canonization steps+ --++ -- * Syntax+ IAtom,+ ILit,+ ILine,+ IForm,+ XLit,+ XLine,+ XForm,+ XPDNF(..), XPCNF(..),+ MixForm(..),++ -- * Conversions++ -- ** IdxPropForm -- indexed propositional formulas+ IdxPropForm,+ tr,+ -- | @tr f form@ replaces each atom form occurrence @(A x)@ in the formula @form@ by the new atom @(A (f x))@. Everything else remains.+ iTr,+ -- | @iTr [i_1,...,i_n] iform@ replaces each index @j@ in @iform@ by @i_j@. For example,+ --+ -- > > let iform = iForm [[-1,3,-4,5],[-2,-3,4,6]] :: IForm+ -- > > iform+ -- > COSTACK [COSTACK [-1,3,-4,5],COSTACK [-2,-3,4,6]]+ -- > > iTr [7,8,9,10,11,12,13] iform+ -- > COSTACK [COSTACK [-7,9,-10,11],COSTACK [-8,-9,10,12]]+ -- > > iTr [2,4] iform+ -- > -- error, because the index list [2,4] must at least be of length 6 to cover the indices 1,..,6 of iform.+ idx,+ -- | @idx [i_1,...,i_n] i_k@ returns @k@, i.e. the index of the index in the given index list.+ -- Note, that the first member of the list starts with index 1, not 0. For example,+ --+ -- > > idx [2,4,6,8] 6+ -- > 3+ nth,+ -- | @nth [i_1,...,i_n] k@ returns @i_k@, i.e. the @k@'s element in the list @[i_1,...,i_n]@, counting from @1@. For example,+ --+ -- > > nth [2,4,6,8] 3+ -- > 6++ itr,+ iUni,+ unifyIdxPropForms,+ unifyXForms,+ fromIdxPropForm,+ toIdxPropForm,+ newAtomsXForm,++ -- ** Purely syntactical conversions to propositional formulas+ iLIT, iNLC, iNLD, iCNF, iDNF,+ xLIT, xNLC, xNLD, xCNF, xDNF,++ -- ** Conversions to and from propositional formulas+ toXPDNF,+ toXPCNF,+ toM2DNF, toM2CNF,+ fromXPDNF,+ fromXPCNF,+ fromMixForm,++ -- * The IForm algebra++ -- ** Basic operations+ isIAtom,+ isILit,+ isILine,+ isIForm,+ iLine,+ iForm,+ iAtom,+ iBool,+ negLit,+ lineIndices,+ formIndices,+ lineLength,+ formLength,+ volume,+ isOrderedForm,+ orderForm,++ -- ** The propositional algebra operations+ atomForm,+ botForm,+ topForm,+ formJoinForm,+ formListJoin,+ lineMeetLine,+ lineMeetForm,+ formMeetForm,+ formListMeet,+ dualLine,+ dualForm,+ invertLine,+ invertForm,+ negLine,+ negForm,+ formCojoinLine,+ formCojoinForm,+ formAntijoinLine,+ formAntijoinForm,+ elimLine,+ elimForm,+ lineCovLine,+ lineCovForm,+ formCovForm,++ -- ** Generation of pairwise minimal, minimal and prime forms++ -- *** Generation of prime and pairwise minimal forms of two lines+ pairPartition,+ CaseSymbol(..),+ caseSymbol,+ pairPrim',+ pairMin',+ xprim',+ xmin',+ xprim,+ xmin,+ pairPrim,+ pairMin,++ -- *** Implementation of the M- and the P-Procedure+ isMinimalPair,+ allPairs,+ isPairwiseMinimal,+ cPrime,+ cPrimes,+ mrec,+ m2form,+ iformJoinM2form,+ primForm,+ iformJoinPrimForm,++ -- * The XForm operations+ xformAtoms,+ xformRedAtoms,+ xformIrrAtoms,++ -- * The propositional algebras++ -- ** XPDNF and XPCNF++ -- ** MixForm+ mixToPDNF,+ mixToPCNF,++ -- * Complexities and choice of a algebra+ -- |+ --+ -- > DefaultPropLogic. FastPropLogic+ -- > -------------------------------------- -----------------------------------+ -- > PropForm TruthTable XPDNF XPCNF MixForm+ -- > --------------------------------------------------------------------------------------------------------------------------+ -- > at+ -- > false+ -- > true+ -- > neg+ -- > conj, disj, subj, equij+ -- > valid+ -- > satisfiable+ -- > subvalent+ -- > equivalent+ -- > covalent, disvalent,+ -- > properSubvalent, properDisvalent+ -- > atoms+ -- > redAtoms, irrAtoms+ -- > nullatomic+ -- > subatomic, equiatomic+ -- > .........+ -- > .........++) where ---------------------------------------------------------------------------------------------------------------++-- import++ import qualified List as L+ import qualified TextDisplay as D+ import qualified Olist as O+ import qualified Costack as C+ import PropLogicCore+ import DefaultPropLogic (NegNormForm, negNormForm)++-- the types++ type IAtom = Int -- I-Atom++ type IdxPropForm a = (O.Olist a, PropForm IAtom) -- indexed propositional formula+ -- type IntLitNormForm = PropForm ILit -- integer literal normal form++ type ILit = Int -- I-Literal or integer literal type+ type ILine = C.Costack ILit -- I-Line or integer line type+ type IForm = C.Costack ILine -- I-Form or integer form type+ type XLit a = (O.Olist a, ILit) -- X-Literal or indexed literal type+ type XLine a = (O.Olist a, ILine) -- X-Line or indexed line type+ type XForm a = (O.Olist a, IForm) -- X-Form or indexed form type++ data XPDNF a = XPDNF (XForm a) -- Indexed/Extended Prime Disjunctive Normal Forms+ deriving (Show, Read, Eq)+ data XPCNF a = XPCNF (XForm a) -- Indexed/Extended Prime Conjunctive Normal Forms+ deriving (Show, Read, Eq)++ data MixForm a -- Mixed Forms:+ = M2DNF (XForm a) -- Pairwise Minimal Disjunctive Normal Forms+ | M2CNF (XForm a) -- Pairwise Minimal Conjunctive Normal Forms+ | PDNF (XForm a) -- Prime Disjunctive Normal Forms+ | PCNF (XForm a) -- Prime Conjunctive Normal Forms+ deriving (Show, Read, Eq)++-- display++ instance D.Display IForm where+ textFrame form = textframe+ where indices = formIndices form+ oneRow line iL = if C.isEmpty line+ then if null iL+ then []+ else [""] : (oneRow line (Prelude.tail iL))+ else case compare (iAtom (C.head line)) (Prelude.head iL) of+ GT -> [""] : (oneRow line (Prelude.tail iL))+ EQ -> if iBool (C.head line)+ then ['+' : (show (C.head line))] : (oneRow (C.tail line) (Prelude.tail iL))+ else [show (C.head line)] : (oneRow (C.tail line) (Prelude.tail iL))+ frameTable = map (\ line -> oneRow line indices) (C.toList form)+ textframe = D.gridMerge (D.normalTextFrameTable frameTable)++ instance D.Display a => D.Display (XForm a) where+ textFrame (aL, form) = textframe+ where headRow = map D.textFrame aL+ indices = [1..(length aL)] :: [IAtom]+ oneRow line iL = if C.isEmpty line+ then if null iL+ then []+ else [""] : (oneRow line (Prelude.tail iL))+ else case compare (iAtom (C.head line)) (Prelude.head iL) of+ GT -> [""] : (oneRow line (Prelude.tail iL))+ EQ -> if iBool (C.head line)+ then ['+' : (show (C.head line))] : (oneRow (C.tail line) (Prelude.tail iL))+ else [show (C.head line)] : (oneRow (C.tail line) (Prelude.tail iL))+ tableBody = map (\ line -> oneRow line indices) (C.toList form)+ textframe = D.gridMerge (D.normalTextFrameTable (headRow:tableBody))++ titledTextFrame :: D.Display a => (String,String,String) -> XForm a -> D.TextFrame+ titledTextFrame (empty, full, title) (aL,iform) =+ if null aL+ then if C.isEmpty iform+ then D.textFrameBox (D.correctTextFrame [title,empty])+ else D.textFrameBox (D.correctTextFrame [title,full])+ else let body = D.textFrame (aL,iform)+ textframe = D.textFrameBox (D.plainMerge (D.normalTextFrameTable [[[title]],[body]]))+ in textframe++ instance D.Display a => D.Display (XPDNF a) where+ textFrame (XPDNF xform) = titledTextFrame ("false", "true", "XPDNF") xform++ instance D.Display a => D.Display (XPCNF a) where+ textFrame (XPCNF xform) = titledTextFrame ("true", "false", "XPCNF") xform++ instance D.Display a => D.Display (MixForm a) where+ textFrame (M2DNF xform) = titledTextFrame ("false", "true", "M2DNF") xform+ textFrame (M2CNF xform) = titledTextFrame ("true", "false", "M2CNF") xform+ textFrame (PDNF xform) = titledTextFrame ("false", "true", "PDNF") xform+ textFrame (PCNF xform) = titledTextFrame ("true", "false", "PCNF") xform++-- order++ instance Ord ILine where+ compare left right =+ if C.isEmpty left+ then if C.isEmpty right+ then EQ+ else LT+ else if C.isEmpty right+ then GT+ else case compare (iAtom (C.head left)) (iAtom (C.head right)) of+ LT -> LT+ GT -> GT+ EQ -> case compare (iBool (C.head left)) (iBool (C.head right)) of+ LT -> LT+ GT -> GT+ EQ -> compare (C.tail left) (C.tail right)++ instance Ord IForm where+ compare form1 form2 = if C.isEmpty form1+ then if C.isEmpty form2+ then EQ+ else LT+ else if C.isEmpty form2+ then GT+ else case compare (C.head form1) (C.head form2) of+ LT -> LT+ GT -> GT+ EQ -> compare (C.tail form1) (C.tail form2)++-- convertions via IntLitNormForm++ toXPDNF :: Ord a => PropForm a -> XPDNF a+ toXPDNF p = XPDNF (aL, primForm iform)+ where (aL, iprop) = toIdxPropForm p+ iform = fromNegNF (negNormForm iprop)+ fromNegNF (A n) = atomForm n+ fromNegNF (N (A n)) = atomForm (negLit n)+ fromNegNF F = botForm+ fromNegNF T = topForm+ fromNegNF (CJ pL) = formListMeet (map fromNegNF pL)+ fromNegNF (DJ pL) = formListJoin (map fromNegNF pL)++ toXPCNF :: Ord a => PropForm a -> XPCNF a+ toXPCNF p = XPCNF (aL, primForm iform)+ where (aL, iprop) = toIdxPropForm p+ iform = fromNegNF (negNormForm iprop)+ fromNegNF (A n) = atomForm n+ fromNegNF (N (A n)) = atomForm (negLit n)+ fromNegNF F = topForm+ fromNegNF T = botForm+ fromNegNF (CJ pL) = formListJoin (map fromNegNF pL)+ fromNegNF (DJ pL) = formListMeet (map fromNegNF pL)++ fromXPDNF :: Ord a => XPDNF a -> PropForm a+ fromXPDNF (XPDNF xform) = xDNF xform++ fromXPCNF :: Ord a => XPCNF a -> PropForm a+ fromXPCNF (XPCNF xform) = xCNF xform++ toM2DNF :: Ord a => PropForm a -> MixForm a+ toM2DNF p = M2DNF (aL, m2form iform)+ where (aL, iprop) = toIdxPropForm p+ iform = fromIntLitNormForm (negNormForm iprop)+ fromIntLitNormForm (A n) = atomForm n+ fromIntLitNormForm F = botForm+ fromIntLitNormForm T = topForm+ fromIntLitNormForm (CJ pL) = formListMeet (map fromIntLitNormForm pL)+ fromIntLitNormForm (DJ pL) = formListJoin (map fromIntLitNormForm pL)++ toM2CNF :: Ord a => PropForm a -> MixForm a+ toM2CNF p = M2CNF (aL, m2form iform)+ where (aL, iprop) = toIdxPropForm p+ iform = fromIntLitNormForm (negNormForm iprop)+ fromIntLitNormForm (A n) = atomForm n+ fromIntLitNormForm F = topForm+ fromIntLitNormForm T = botForm+ fromIntLitNormForm (CJ pL) = formListJoin (map fromIntLitNormForm pL)+ fromIntLitNormForm (DJ pL) = formListMeet (map fromIntLitNormForm pL)++ fromMixForm :: Ord a => MixForm a -> PropForm a+ fromMixForm (M2DNF xform) = xDNF xform+ fromMixForm (M2CNF xform) = xCNF xform+ fromMixForm (PDNF xform) = xDNF xform+ fromMixForm (PCNF xform) = xCNF xform++-- translations, indices and unifications++ tr :: (s -> t) -> PropForm s -> PropForm t+ tr f (A x) = A (f x)+ tr f F = F+ tr f T = T+ tr f (N prop) = N (tr f prop)+ tr f (CJ propL) = CJ (map (tr f) propL)+ tr f (DJ propL) = DJ (map (tr f) propL)+ tr f (SJ propL) = SJ (map (tr f) propL)+ tr f (EJ propL) = EJ (map (tr f) propL)++ iTr :: O.Olist IAtom -> IForm -> IForm+ iTr aL form = C.map (iTr' aL 1) form+ where iTr' aL n line = if C.isEmpty line+ then line+ else case compare n (iAtom (C.head line)) of+ EQ -> if (iBool (C.head line))+ then C.cons (head aL) (iTr' (tail aL) (n + 1) (C.tail line))+ else C.cons (negLit (head aL)) (iTr' (tail aL) (n + 1) (C.tail line))+ LT -> iTr' (tail aL) (n + 1) line++ idx :: Ord a => O.Olist a -> a -> IAtom+ idx [] x = error "idx -- empty list"+ idx (y:yL) x = case compare y x of+ LT -> 1 + (idx yL x)+ EQ -> 1+ GT -> error "idx -- atom is not a list member"++ nth :: Ord a => O.Olist a -> IAtom -> a+ nth oli n = if n < 1+ then error ("nth -- undefined IAtom " ++ (show n))+ else iter (n, oli)+ where iter (i, []) = error ("nth -- index " ++ (show n) ++ " exceeds the list length")+ iter (i, (x:xL)) = if i == 1+ then x+ else iter (i - 1, xL)++ itr :: Ord a => O.Olist a -> O.Olist a -> Maybe (O.Olist IAtom)+ itr s1 s2 = iter True s1 s2 1 [] -- True means that s1 == s2+ where iter b [] [] n nL = if b then Nothing else (Just (reverse nL))+ iter b [] (y:yL) n nL = iter False [] yL (n + 1) nL+ iter b (x:xL) (y:yL) n nL = case compare x y of+ EQ -> iter b xL yL (n + 1) (n:nL)+ GT -> iter False (x:xL) yL (n + 1) nL+ LT -> error "itr -- first list is not included by second list"++ iUni :: Ord a => [O.Olist a] -> (O.Olist a, [Maybe (O.Olist IAtom)])+ iUni sL = (aL, map (\ s -> itr s aL) sL)+ where aL = O.unionList sL++ unifyIdxPropForms :: Ord a => [IdxPropForm a] -> (O.Olist a, [PropForm IAtom])+ unifyIdxPropForms pL = (aL, ipropL)+ where (aL, maybeL) = iUni (map fst pL)+ update (iprop, Nothing) = iprop+ update (iprop, Just iL) = tr (nth iL) iprop+ ipropL = map update (zip (map snd pL) maybeL)++ unifyXForms :: Ord a => [XForm a] -> (O.Olist a, [IForm])+ unifyXForms xformL = (aL, iformL)+ where (aL, maybeL) = iUni (map fst xformL)+ update (iform, Nothing) = iform+ update (iform, Just iL) = iTr iL iform+ iformL = map update (zip (map snd xformL) maybeL)++ newAtomsXForm :: Ord a => XForm a -> O.Olist a -> XForm a+ newAtomsXForm (oldAts, iform) newAts = (newAts, updateIForm (updateList oldAts newAts) iform)+ where updateList :: Ord a => O.Olist a -> O.Olist a -> [Maybe IAtom]+ updateList oldAts newAts = updateList' oldAts 1 newAts+ where updateList' [] n newAts = []+ updateList' (x:xL) n [] = L.replicate (length (x:xL)) Nothing+ updateList' (x:xL) n (y:yL) = case compare x y of+ LT -> Nothing : (updateList' xL n (y:yL))+ EQ -> (Just n) : (updateList' xL (n + 1) yL)+ GT -> updateList' (x:xL) (n + 1) yL+ updateIForm :: [Maybe IAtom] -> IForm -> IForm+ updateIForm maL iform = C.map (updateILine maL) iform+ updateILine :: [Maybe IAtom] -> ILine -> ILine+ updateILine maL iline = updateILine' 1 maL iline+ where updateILine' _ [] _ = C.empty+ updateILine' n (x:xL) iline =+ if C.isEmpty iline+ then iline+ else case compare n (iAtom (C.head iline)) of+ LT -> updateILine' (n + 1) xL iline+ EQ -> case x of+ Nothing -> updateILine' (n + 1) xL (C.tail iline)+ Just i -> if iBool (C.head iline)+ then C.cons i (updateILine' (n + 1) xL (C.tail iline))+ else C.cons (negLit i) (updateILine' (n + 1) xL (C.tail iline))++-- X-Prop conversions++ fromIdxPropForm :: Ord a => IdxPropForm a -> PropForm a+ fromIdxPropForm (s, iprop) = tr (nth s) iprop++ toIdxPropForm :: Ord a => PropForm a -> IdxPropForm a+ toIdxPropForm prop = (s, tr (idx s) prop)+ where s = propFormAtoms prop++ propFormAtoms :: Ord a => PropForm a -> O.Olist a+ propFormAtoms p = case p of+ (A a) -> [a]+ F -> []+ T -> []+ (N p) -> propFormAtoms p+ (CJ pL) -> O.unionList (map propFormAtoms pL)+ (DJ pL) -> O.unionList (map propFormAtoms pL)+ (SJ pL) -> O.unionList (map propFormAtoms pL)+ (EJ pL) -> O.unionList (map propFormAtoms pL)++-- I-Form conversion++ iLIT :: ILit -> PropForm IAtom+ iLIT l | l < 0 = N (A (negLit l))+ | l > 0 = A l+ | otherwise = error "iLIT -- zero literal"++ iNLC :: ILine -> PropForm IAtom+ iNLC line = CJ (map iLIT (C.toList line))++ iNLD :: ILine -> PropForm IAtom+ iNLD line = DJ (map iLIT (C.toList line))++ iCNF :: IForm -> PropForm IAtom+ iCNF form = CJ (map iNLD (C.toList form))++ iDNF :: IForm -> PropForm IAtom+ iDNF form = DJ (map iNLC (C.toList form))++-- X-Form conversion++ xLIT :: Ord a => XLit a -> PropForm a+ xLIT (s, l) = fromIdxPropForm (s, iLIT l)++ xNLC :: Ord a => XLine a -> PropForm a+ xNLC (s, line) = fromIdxPropForm (s, iNLC line)++ xNLD :: Ord a => XLine a -> PropForm a+ xNLD (s, line) = fromIdxPropForm (s, iNLD line)++ xCNF :: Ord a => XForm a -> PropForm a+ xCNF (s, form) = fromIdxPropForm (s, iCNF form)++ xDNF :: Ord a => XForm a -> PropForm a+ xDNF (s, form) = fromIdxPropForm (s, iDNF form)++-- type correctness and type constructors++ isIAtom :: Int -> Bool+ isIAtom n = n > 0++ isILit :: Int -> Bool+ isILit n = n /= 0++ isILine :: C.Costack Int -> Bool+ isILine x = iter (C.toList x)+ where iter [] = True+ iter [n] = isILit(n)+ iter (n1:n2:nL) = isILit(n1) && iAtom(n1) < iAtom(n2) && iter(n2:nL)++ isIForm :: C.Costack (C.Costack Int) -> Bool+ isIForm x = iter (C.toList x)+ where iter [] = True+ iter (c:cL) = (isILine c) && iter cL++ iLine :: [Int] -> ILine+ iLine iL = C.fromList (iter (zeroCheck iL))+ where iter [] = []+ iter [i] = [i]+ iter (j:i:iL) = if (abs j) < (abs i)+ then j:(iter (i:iL))+ else error ("IForm.iLine -- in literal order " ++ (show j) +++ " is not before " ++ (show i))+ zeroCheck [] = []+ zeroCheck (i:iL) = if i == 0+ then error "Iform.iLine -- there is a 0 in the list"+ else i:(zeroCheck iL)++ iForm :: [[Int]] -> IForm+ iForm iLL = C.fromList (map iLine iLL)++-- literal operations++ iAtom :: ILit -> IAtom+ iAtom = abs++ iBool :: ILit -> Bool+ iBool l | l < 0 = False+ | l > 0 = True+ | l == 0 = error "IForm.iBool -- zero literal integer"++ negLit :: ILit -> ILit+ negLit = Prelude.negate++-- index lists++ lineIndices :: ILine -> O.Olist IAtom+ lineIndices line = map iAtom (C.toList line)++ formIndices :: IForm -> O.Olist IAtom+ formIndices form = O.unionList (C.toList (C.map lineIndices form))++-- syntactic sizes++ lineLength :: ILine -> Int+ lineLength = C.length++ formLength :: IForm -> Int+ formLength = C.length++ volume :: IForm -> Int+ volume form = C.foldr (+) 0 (C.map lineLength form)++-- ordered forms++ isOrderedForm :: IForm -> Bool+ isOrderedForm form = C.strictSorted form++ orderForm :: IForm -> IForm+ orderForm form = C.strictSort form++-- the propositional algebra operations++ atomForm :: IAtom -> IForm+ atomForm atom = C.singleton (C.singleton atom)++ botForm :: IForm+ botForm = C.empty++ topForm :: IForm+ topForm = C.singleton C.empty++ formJoinForm :: IForm -> IForm -> IForm+ formJoinForm form1 form2 = C.append form1 form2++ formListJoin :: [IForm] -> IForm+ formListJoin formL = C.concat formL++ lineMeetLine :: ILine -> ILine -> IForm+ lineMeetLine line1 line2 = jrec (line1, line2, C.empty)+ where jrec (first, second, third) =+ if C.isEmpty first+ then C.singleton (C.append third second)+ else if C.isEmpty second+ then C.singleton (C.append third first)+ else case compare (iAtom (C.head first)) (iAtom (C.head second)) of+ LT -> jrec (C.tail first, second, C.cocons third (C.head first))+ GT -> jrec (first, C.tail second, C.cocons third (C.head second))+ EQ -> if (iBool (C.head first)) == (iBool (C.head second))+ then jrec (C.tail first, C.tail second, C.cocons third (C.head first))+ else C.empty++ lineMeetForm :: ILine -> IForm -> IForm+ lineMeetForm line form = formListJoin (map (lineMeetLine line) (C.toList form))++ formMeetForm :: IForm -> IForm -> IForm+ formMeetForm form1 form2 = formListJoin (map (\ line -> lineMeetForm line form2) (C.toList form1))++ formListMeet :: [IForm] -> IForm+ formListMeet [] = C.singleton C.empty+ formListMeet [form] = form+ formListMeet (form1:form2:formL) = formListMeet ((formMeetForm form1 form2) : formL)++ dualLine :: ILine -> IForm+ dualLine line = C.map C.singleton line++ dualForm :: IForm -> IForm+ dualForm form = formListMeet (map dualLine (C.toList form))++ invertLine :: ILine -> ILine+ invertLine = C.map negLit++ invertForm :: IForm -> IForm+ invertForm = C.map invertLine++ negLine :: ILine -> IForm+ negLine line = C.map (\ l -> (C.singleton (negLit l))) line++ negForm :: IForm -> IForm+ negForm form = formListMeet (map negLine (C.toList form))++ formCojoinLine :: IForm -> ILine -> IForm+ formCojoinLine form line = formJoinForm form (dualLine line)++ formCojoinForm :: IForm -> IForm -> IForm+ formCojoinForm form1 form2 = formListMeet (C.toList (C.map (formCojoinLine form1) form2))++ formAntijoinLine :: IForm -> ILine -> IForm+ formAntijoinLine form line = formJoinForm form (negLine line)++ formAntijoinForm :: IForm -> IForm -> IForm+ formAntijoinForm form1 form2 = formListMeet (C.toList (C.map (formAntijoinLine form1) form2))++ elimLine :: ILine -> O.Olist IAtom -> ILine+ elimLine line aL | C.isEmpty line = C.empty+ | O.isEmpty aL = line+ | otherwise = case compare (iAtom (C.head line)) (head aL) of+ LT -> C.cons (C.head line) (elimLine (C.tail line) aL)+ GT -> elimLine line (tail aL)+ EQ -> elimLine (C.tail line) (tail aL)++ elimForm :: IForm -> O.Olist IAtom -> IForm+ elimForm form aL = C.map (\ line -> (elimLine line aL)) form++ lineCovLine :: ILine -> ILine -> Bool+ lineCovLine line1 line2 | C.isEmpty line2 = True+ | C.isEmpty line1 = False+ | otherwise = case compare (iAtom (C.head line1)) (iAtom (C.head line2)) of+ LT -> lineCovLine (C.tail line1) line2+ GT -> False+ EQ -> if (iBool (C.head line1)) == (iBool (C.head line2))+ then lineCovLine (C.tail line1) (C.tail line2)+ else False++ lineCovForm :: ILine -> IForm -> Bool+ lineCovForm line form = if C.isEmpty form+ then False+ else if lineCovLine line (C.head form)+ then True+ else lineCovForm line (C.tail form)++ formCovForm :: IForm -> IForm -> Bool+ formCovForm form1 form2 = if C.isEmpty form1+ then True+ else if lineCovForm (C.head form1) form2+ then formCovForm (C.tail form1) form2+ else False++-- Generation of the prime and minimal form of two lines++ pairPartition :: ILine -> ILine -> (ILine,ILine,ILine,ILine)+ pairPartition line1 line2 = iter (C.empty, C.empty, C.empty, C.empty, line1, line2)+ where iter :: (ILine,ILine,ILine,ILine,ILine,ILine) -> (ILine,ILine,ILine,ILine)+ iter (piL, rhoL, sigmaL, tauL, line1, line2) =+ if C.isEmpty line1+ then (piL, rhoL, sigmaL, C.append tauL line2)+ else if C.isEmpty line2+ then (piL, rhoL, C.append sigmaL line1, tauL)+ else case compare (iAtom (C.head line1)) (iAtom (C.head line2)) of+ LT -> iter (piL, rhoL, C.cocons sigmaL (C.head line1), tauL, C.tail line1, line2)+ GT -> iter (piL, rhoL, sigmaL, C.cocons tauL (C.head line2), line1, C.tail line2)+ EQ -> if iBool (C.head line1) == iBool (C.head line2)+ then iter (C.cocons piL (C.head line1), rhoL, sigmaL, tauL, C.tail line1, C.tail line2)+ else iter (piL, C.cocons rhoL (C.head line1), sigmaL, tauL, C.tail line1, C.tail line2)++ data CaseSymbol = NOOO | NOOP | NOPO | NOPP | NIOO | NIOP | NIPO | NIPP | NMNN+ deriving (Show, Read, Eq, Ord)++ caseSymbol :: ILine -> ILine -> CaseSymbol+ caseSymbol left right+ | p >= 0 && r == 0 && s == 0 && t == 0 = NOOO+ | p >= 0 && r == 0 && s == 0 && t >= 1 = NOOP+ | p >= 0 && r == 0 && s >= 1 && t == 0 = NOPO+ | p >= 0 && r == 0 && s >= 1 && t >= 1 = NOPP+ | p >= 0 && r == 1 && s == 0 && t == 0 = NIOO+ | p >= 0 && r == 1 && s == 0 && t >= 1 = NIOP+ | p >= 0 && r == 1 && s >= 1 && t == 0 = NIPO+ | p >= 0 && r == 1 && s >= 1 && t >= 1 = NIPP+ | p >= 0 && r >= 2 && s >= 0 && t >= 0 = NMNN+ where (piL, rhoL, sigmaL, tauL) = pairPartition left right+ (p,r,s,t) = (C.length piL, C.length rhoL, C.length sigmaL, C.length tauL)++-- First version++ pairPrim' :: ILine -> ILine -> IForm+ pairPrim' left right+ | p >= 0 && r == 0 && s == 0 && t == 0 = C.singleton left+ | p >= 0 && r == 0 && s == 0 && t >= 1 = C.singleton left+ | p >= 0 && r == 0 && s >= 1 && t == 0 = C.singleton right+ | p >= 0 && r == 0 && s >= 1 && t >= 1 = C.fromList [left,right]+ | p >= 0 && r == 1 && s == 0 && t == 0 = C.singleton piL+ | p >= 0 && r == 1 && s == 0 && t >= 1 = C.fromList [left, lineMerge piL tauL]+ | p >= 0 && r == 1 && s >= 1 && t == 0 = C.fromList [lineMerge piL sigmaL, right]+ | p >= 0 && r == 1 && s >= 1 && t >= 1 = C.fromList [left, right, lineMerge piL (lineMerge sigmaL tauL)]+ | p >= 0 && r >= 2 && s >= 0 && t >= 0 = C.fromList [left, right]+ where (piL, rhoL, sigmaL, tauL) = pairPartition left right+ (p,r,s,t) = (C.length piL, C.length rhoL, C.length sigmaL, C.length tauL)+ lineMerge line1 line2 | C.isEmpty line1 = line2+ | C.isEmpty line2 = line1+ | otherwise = case compare (iAtom (C.head line1)) (iAtom (C.head line2)) of+ LT -> C.cons (C.head line1) (lineMerge (C.tail line1) line2)+ GT -> C.cons (C.head line2) (lineMerge line1 (C.tail line2))++ pairMin' :: ILine -> ILine -> IForm+ pairMin' left right = C.take 2 (pairPrim' left right)++ xprim' :: ILine -> ILine -> (CaseSymbol, IForm)+ xprim' left right = (caseSymbol left right, pairPrim' left right)++ xmin' :: ILine -> ILine -> (CaseSymbol, IForm)+ xmin' left right = (caseSymbol left right, pairMin' left right)++-- Second, fast and final version++ xprim :: ILine -> ILine -> (CaseSymbol, IForm)+ xprim left right = xprec (C.empty, left, C.empty, right, C.empty, C.empty, C.empty, 0, 0, 0)+ where xprec (left, left', right, right', c1, c2, c3, r, s, t)+ | r > 1 =+ (NMNN, C.fromList [C.append left left', C.append right right'])+ | C.isEmpty left' && r == 0 && s == 0 && C.isEmpty right' && t == 0 =+ (NOOO, C.singleton left)+ | C.isEmpty left' && r == 0 && s == 0 =+ (NOOP, C.singleton left)+ | C.isEmpty left' && r == 0 && s > 0 && C.isEmpty right' && t == 0 =+ (NOPO, C.singleton right)+ | C.isEmpty left' && r == 0 && s > 0 =+ (NOPP, C.fromList [left, C.append right right'])+ | C.isEmpty left' && r == 1 && s == 0 && C.isEmpty right' && t == 0 =+ (NIOO, C.singleton c1)+ | C.isEmpty left' && r == 1 && s == 0 =+ (NIOP, C.fromList [left, C.append c2 right'])+ | C.isEmpty left' && r == 1 && s > 0 && C.isEmpty right' && t == 0 =+ (NIPO, C.fromList [c1, C.append right right'])+ | C.isEmpty left' && r == 1 && s > 0 =+ (NIPP, C.fromList [left, C.append right right', C.append c3 right'])+ | not (C.isEmpty left') && C.isEmpty right' && r == 0 && t == 0 =+ (NOPO, C.singleton right)+ | not (C.isEmpty left') && C.isEmpty right' && r == 0 && t > 0 =+ (NOPP, C.fromList [C.append left left', right])+ | not (C.isEmpty left') && C.isEmpty right' && r == 1 && t == 0 =+ (NIPO, C.fromList [C.append c1 left', right])+ | not (C.isEmpty left') && C.isEmpty right' && r == 1 && t > 0 =+ (NIPP, C.fromList [C.append left left', right, C.append c3 left'])+ | not (C.isEmpty left') && not (C.isEmpty right') =+ let x = C.head left'+ y = C.head right'+ in case compare (iAtom x) (iAtom y) of+ LT -> xprec (C.cocons left x, C.tail left', right, right',+ C.cocons c1 x, c2, C.cocons c3 x, r, s + 1, t)+ GT -> xprec (left, left', C.cocons right y, C.tail right',+ c1, C.cocons c2 y, C.cocons c3 y, r, s, t + 1)+ EQ -> if iBool x == iBool y+ then xprec (C.cocons left x, C.tail left', C.cocons right y, C.tail right',+ C.cocons c1 x, C.cocons c2 y, C.cocons c3 y, r, s, t)+ else xprec (C.cocons left x, C.tail left', C.cocons right y, C.tail right',+ c1, c2, c3, r + 1, s, t)++{-- old version of xprim+ xprim :: ILine -> ILine -> (CaseSymbol, IForm)+ xprim left right = xprec (C.empty, left, C.empty, right, C.empty, C.empty, C.empty, 0, 0, 0)+ where xprec (left, left', right, right', cboth, cleft, cright, r, s, t) =+ if r > 1+ then (NMNN, C.fromList [C.append left left', C.append right right'])+ else if C.isEmpty left'+ then if r == 0+ then if s == 0+ then if (C.isEmpty right' && t == 0)+ then (NOOO, C.singleton left)+ else (NOOP, C.singleton left)+ else if (C.isEmpty right' && t == 0)+ then (NOPO, C.singleton right)+ else (NOPP, C.fromList [left, C.append right right'])+ else if s == 0+ then if (C.isEmpty right' && t == 0)+ then (NIOO, C.singleton cboth)+ else (NIOP, C.fromList [left, C.append cleft right'])+ else if (C.isEmpty right' && t == 0)+ then (NIPO, C.fromList [cboth, C.append right right'])+ else (NIPP, C.fromList [cboth, C.append right right', C.append cright right'])+ else if C.isEmpty right'+ then if r == 0+ then if t == 0+ then (NOPO, C.singleton right)+ else (NOPP, C.fromList [C.append left left', right])+ else if t == 0+ then (NIPO, C.fromList [C.append cboth left', right])+ else (NIPP, C.fromList [C.append left left', right, C.append cright left'])+ else case compare (iAtom (C.head left')) (iAtom (C.head right')) of+ LT -> xprec ( C.cocons left (C.head left'),+ C.tail left',+ right,+ right',+ C.cocons cboth (C.head left'),+ cleft,+ C.cocons cright (C.head left'),+ r, s+1, t)+ GT -> xprec ( left,+ left',+ C.cocons right (C.head right'),+ C.tail right',+ cboth,+ C.cocons cleft (C.head right'),+ C.cocons cright (C.head right'),+ r, s, t+1)+ EQ -> if iBool (C.head left') == iBool (C.head right')+ then xprec ( C.cocons left (C.head left'),+ C.tail left',+ C.cocons right (C.head right'),+ C.tail right',+ C.cocons cboth (C.head left'),+ C.cocons cleft (C.head left'),+ C.cocons cright (C.head right'),+ r, s, t)+ else xprec ( C.cocons left (C.head left'),+ C.tail left',+ C.cocons right (C.head right'),+ C.tail right',+ cboth, cleft, cright,+ r+1, s, t)+--}++ xmin :: ILine -> ILine -> (CaseSymbol, IForm)+ xmin left right = case xprim left right of+ (NIPP, form) -> (NIPP, C.take 2 form)+ (symb, form) -> (symb, form)++ pairPrim :: ILine -> ILine -> IForm+ pairPrim left right = snd (xprim left right)++ pairMin :: ILine -> ILine -> IForm+ pairMin left right = snd (xmin left right)++-- Pairwise minimality and complementary prime list++ isMinimalPair :: ILine -> ILine -> Bool+ isMinimalPair left right = [left, right] == C.toList (pairMin' left right)++ allPairs :: [a] -> [(a,a)]+ allPairs [] = []+ allPairs [x] = []+ allPairs (x:xL) = (iter x xL) ++ (allPairs xL)+ where iter x [] = []+ iter x (y:yL) = (x,y):(iter x yL)++ isPairwiseMinimal :: IForm -> Bool+ isPairwiseMinimal form = Prelude.all isMinPair (allPairs (C.toList form))+ where isMinPair (x,y) = isMinimalPair x y++-- C-Primes++ cPrime :: ILine -> ILine -> Maybe ILine+ cPrime left right = case xprim left right of+ (NIPP, form) -> Just (C.head (C.tail (C.tail form)))+ (symb, form) -> Nothing++ cPrimes :: IForm -> IForm+ cPrimes form = C.fromList (concat (map cp (allPairs (C.toList form))))+ where cp (left ,right) = case cPrime left right of+ Just line -> [line]+ Nothing -> []++-- The M-Procedure and functions with pairwise minimal IForm results++ mrec :: (IForm,IForm,IForm) -> IForm+ mrec (gammaL, muL, muL') =+ if C.isEmpty gammaL+ then C.append muL muL'+ else if C.isEmpty muL'+ then mrec (C.tail gammaL, C.empty, C.cons (C.head gammaL) muL)+ else case xmin (C.head gammaL) (C.head muL') of+ (NOOO, pp) -> mrec (C.tail gammaL, C.empty, C.append muL muL')+ (NOOP, pp) -> mrec (C.append (C.tail gammaL) (C.tail muL'), C.empty, C.cons (C.head gammaL) muL)+ (NOPO, pp) -> mrec (C.tail gammaL, C.empty, C.append muL muL')+ (NOPP, pp) -> mrec (gammaL, C.cocons muL (C.head muL'), C.tail muL')+ (NIOO, pp) -> mrec (C.append (C.tail gammaL) pp, C.empty, C.append muL (C.tail muL'))+ (NIOP, pp) -> mrec (C.concat [C.tail gammaL, C.tail pp, C.tail muL'], C.empty, C.cons (C.head gammaL) muL)+ (NIPO, pp) -> mrec (C.cocons (C.tail gammaL) (C.head pp), C.empty, C.append muL muL')+ (NIPP, pp) -> mrec (gammaL, C.cocons muL (C.head muL'), C.tail muL')+ (NMNN, pp) -> mrec (gammaL, C.cocons muL (C.head muL'), C.tail muL')++ m2form :: IForm -> IForm+ m2form form = mrec (form, C.empty, C.empty)++ iformJoinM2form :: IForm -> IForm -> IForm+ iformJoinM2form iform m2form = mrec (iform, C.empty, m2form)++-- The P-Procedure and functions with prime IForm results++ primFormFromOrdM2form :: IForm -> IForm+ primFormFromOrdM2form ordM2form =+ let ordM2form' = orderForm (iformJoinM2form (cPrimes ordM2form) ordM2form)+ in if ordM2form' == ordM2form+ then ordM2form'+ else primFormFromOrdM2form ordM2form'++ primForm :: IForm -> IForm+ primForm iform = primFormFromOrdM2form $ orderForm $ m2form iform++ iformJoinPrimForm :: IForm -> IForm -> IForm+ iformJoinPrimForm iform pform = primFormFromOrdM2form $ orderForm $ iformJoinM2form iform pform++{-- the following prec, primform, ordPrimForm are obsolete -----------------------------------------------------------++ prec :: (IForm, IForm, IForm, IForm) -> IForm+ prec (gammaL, muL, muL', piL)+ | C.isEmpty gammaL && C.isEmpty piL =+ C.append muL muL'+ | C.isEmpty gammaL =+ prec (piL, C.empty, C.append muL muL', C.empty)+ | C.isEmpty muL' =+ prec (C.append (C.tail gammaL) piL, C.empty, C.cons (C.head gammaL) muL, C.empty)+ | otherwise =+ case xprim (C.head gammaL) (C.head muL') of+ (NOOO, pp) -> prec (C.tail gammaL, C.empty, C.append muL muL', C.empty)+ (NOOP, pp) -> prec (C.concat [C.tail gammaL, C.tail muL', piL], C.empty, C.cons (C.head gammaL) muL, C.empty)+ (NOPO, pp) -> prec (C.tail gammaL, C.empty, C.append muL muL', C.empty)+ (NOPP, pp) -> prec (gammaL, C.cocons muL (C.head muL'), C.tail muL', piL)+ (NIOO, pp) -> prec (C.append (C.tail gammaL) pp, C.empty, C.append muL (C.tail muL'), C.empty)+ (NIOP, pp) -> prec (C.concat [C.tail gammaL, C.tail pp, C.tail muL', piL], C.empty, C.cons (C.head gammaL) muL, C.empty)+ (NIPO, pp) -> prec (C.cocons (C.tail gammaL) (C.head pp), C.empty, C.append muL muL', C.empty)+ (NIPP, pp) -> prec (gammaL, C.cocons muL (C.head muL'), C.tail muL', C.append (C.tail (C.tail pp)) piL)+ (NMNN, pp) -> prec (gammaL, C.cocons muL (C.head muL'), C.tail muL', piL)++ -- OLD VERSION --------++ prec :: (IForm, IForm, IForm, IForm) -> IForm+ prec (gammaL, muL, muL', piL) =+ if C.isEmpty gammaL+ then if C.isEmpty piL+ then C.append muL muL'+ else prec (piL, C.empty, C.append muL muL', C.empty)+ else if C.isEmpty muL'+ then prec (C.append (C.tail gammaL) piL, C.empty, C.cons (C.head gammaL) muL, C.empty)+ else case xprim (C.head gammaL) (C.head muL') of+ (NOOO, pp) ->+ prec (C.tail gammaL, C.empty, C.append muL muL', C.empty)+ (NOOP, pp) ->+ prec (C.concat [C.tail gammaL, C.tail muL', piL], C.empty, C.cons (C.head gammaL) muL, C.empty)+ (NOPO, pp) ->+ prec (C.tail gammaL, C.empty, C.append muL muL', C.empty)+ (NOPP, pp) ->+ prec (gammaL, C.cocons muL (C.head muL'), C.tail muL', piL)+ (NIOO, pp) ->+ -- old version: --!!+ -- prec (C.cocons (C.tail gammaL) (C.head pp), C.empty, C.append muL muL', C.empty)+ prec (C.cocons (C.tail gammaL) (C.head pp), C.empty, C.append muL (C.tail muL'), C.empty)+ (NIOP, pp) ->+ prec (C.concat [C.tail gammaL, C.tail pp, C.tail muL', piL], C.empty, C.cons (C.head gammaL) muL, C.empty)+ (NIPO, pp) ->+ prec (C.cocons (C.tail gammaL) (C.head pp), C.empty, C.append muL muL', C.empty)+ (NIPP, pp) ->+ prec (gammaL, C.cocons muL (C.head muL'), C.tail muL', C.append (C.tail (C.tail pp)) piL)+ (NMNN, pp) ->+ prec (gammaL, C.cocons muL (C.head muL'), C.tail muL', piL)++ primForm :: IForm -> IForm+ primForm form = prec (form, C.empty, C.empty, C.empty)++ ordPrimForm :: IForm -> IForm+ ordPrimForm = orderForm . primForm+------------------------------------------------------------------------------------------------------------------}++-- XForm operations++ xformAtoms :: Ord a => XForm a -> O.Olist a+ xformAtoms (aL,iform) = aL++ xformRedAtoms :: Ord a => XForm a -> O.Olist a+ xformRedAtoms xform = O.difference (xformAtoms xform) (xformIrrAtoms xform)++ xformIrrAtoms :: Ord a => XForm a -> O.Olist a+ xformIrrAtoms (aL, iform) = iter aL 1 (formIndices iform)+ where iter aL n [] = []+ iter (a:aL) n (i:iL) = case compare n i of+ EQ -> a : (iter aL (n + 1) iL)+ LT -> iter aL (n + 1) (i:iL)++-- The XPDNF algebra++ instance Ord a => PropAlg a (XPDNF a) where+ at x = XPDNF ([x], atomForm 1)+ false = XPDNF ([], botForm)+ true = XPDNF ([], topForm)+ neg (XPDNF (aL, iform)) = XPDNF (aL, primForm (negForm iform))+ conj pL = XPDNF (aL, primForm (formListMeet iformL))+ where (aL, iformL) = unifyXForms (map (\ (XPDNF xform) -> xform) pL)+ disj pL = XPDNF (aL, primForm (formListJoin iformL))+ where (aL, iformL) = unifyXForms (map (\ (XPDNF xform) -> xform) pL)+ subj pL = XPDNF (aL, primForm (subj' iformL))+ where (aL, iformL) = unifyXForms (map (\ (XPDNF xform) -> xform) pL)+ subj' [] = topForm+ subj' [iform] = topForm+ subj' (iform1:iform2:iformL) = formMeetForm (formJoinForm (negForm iform1) iform2) (subj' (iform2:iformL))+ equij pL = XPDNF (aL, primForm (iform))+ where (aL, iformL) = unifyXForms (map (\ (XPDNF xform) -> xform) pL)+ iform = formJoinForm (formListMeet iformL) (negForm (formListJoin iformL))+ valid (XPDNF (aL, iform)) = iform == topForm+ satisfiable (XPDNF (aL, iform)) = iform /= botForm+ subvalent (XPDNF xform1) (XPDNF xform2) = formCovForm iform1 iform2+ where (aL, [iform1, iform2]) = unifyXForms [xform1, xform2]+ equivalent = (==)+ covalent p1 p2 = satisfiable (conj [p1, p2])+ properSubvalent p1 p2 = p1 /= p2 && subvalent p1 p2+ properDisvalent p1 p2 = satisfiable p1 && satisfiable p2 && disvalent p1 p2+ atoms (XPDNF xform) = xformAtoms xform+ redAtoms (XPDNF xform) = xformRedAtoms xform+ irrAtoms (XPDNF xform) = xformIrrAtoms xform+ ext (XPDNF (xL, iform)) yL = XPDNF (yL', primForm iform')+ where (yL', iform') = newAtomsXForm (xL, iform) (O.union xL (O.olist yL))+ infRed (XPDNF (xL, iform)) yL = XPDNF (yL', iform''')+ where iform' = primForm (dualForm iform)+ (yL', iform'') = newAtomsXForm (xL, iform') (O.olist yL)+ iform''' = primForm (dualForm iform'')+ supRed (XPDNF xform) yL = XPDNF (yL', primForm iform')+ where (yL', iform') = newAtomsXForm xform (O.olist yL)+ infElim (XPDNF (xL, iform)) yL = infRed (XPDNF (xL, iform)) (O.difference xL (O.olist yL))+ supElim (XPDNF (xL, iform)) yL = supRed (XPDNF (xL, iform)) (O.difference xL (O.olist yL))+ toPropForm = fromXPDNF+ fromPropForm = toXPDNF++ instance Ord a => PropAlg a (XPCNF a) where+ at x = XPCNF ([x], atomForm 1)+ false = XPCNF ([], topForm)+ true = XPCNF ([], botForm)+ neg (XPCNF (aL, iform)) = XPCNF (aL, primForm (negForm iform))+ conj pL = XPCNF (aL, primForm (formListJoin iformL))+ where (aL, iformL) = unifyXForms (map (\ (XPCNF xform) -> xform) pL)+ disj pL = XPCNF (aL, primForm (formListMeet iformL))+ where (aL, iformL) = unifyXForms (map (\ (XPCNF xform) -> xform) pL)+ subj pL = XPCNF (aL, primForm (subj' iformL))+ where (aL, iformL) = unifyXForms (map (\ (XPCNF xform) -> xform) pL)+ subj' [] = botForm+ subj' [iform] = botForm+ subj' (iform1:iform2:iformL) = formJoinForm (formMeetForm (negForm iform1) iform2) (subj' (iform2:iformL))+ equij pL = XPCNF (aL, primForm (iform))+ where (aL, iformL) = unifyXForms (map (\ (XPCNF xform) -> xform) pL)+ iform = formMeetForm (formListJoin iformL) (negForm (formListMeet iformL))+ valid (XPCNF (aL, iform)) = iform == botForm+ satisfiable (XPCNF (aL, iform)) = iform /= topForm+ subvalent (XPCNF xform1) (XPCNF xform2) = formCovForm iform2 iform1+ where (aL, [iform1, iform2]) = unifyXForms [xform1, xform2]+ equivalent = (==)+ covalent p1 p2 = satisfiable (conj [p1, p2])+ properSubvalent p1 p2 = p1 /= p2 && subvalent p1 p2+ properDisvalent p1 p2 = satisfiable p1 && satisfiable p2 && disvalent p1 p2+ atoms (XPCNF xform) = xformAtoms xform+ redAtoms (XPCNF xform) = xformRedAtoms xform+ irrAtoms (XPCNF xform) = xformIrrAtoms xform+ ext (XPCNF (xL, iform)) yL = XPCNF (yL', primForm iform')+ where (yL', iform') = newAtomsXForm (xL, iform) (O.union xL (O.olist yL))+ infRed (XPCNF xform) yL = XPCNF (yL', primForm iform')+ where (yL', iform') = newAtomsXForm xform (O.olist yL)+ supRed (XPCNF (xL, iform)) yL = XPCNF (yL', iform''')+ where iform' = primForm (dualForm iform)+ (yL', iform'') = newAtomsXForm (xL, iform') (O.olist yL)+ iform''' = primForm (dualForm iform'')+ infElim (XPCNF (xL, iform)) yL = infRed (XPCNF (xL, iform)) (O.difference xL (O.olist yL))+ supElim (XPCNF (xL, iform)) yL = supRed (XPCNF (xL, iform)) (O.difference xL (O.olist yL))+ toPropForm = fromXPCNF+ fromPropForm = toXPCNF++ dualizeXPDNF :: Ord a => XPDNF a -> XPCNF a+ dualizeXPDNF (XPDNF (aL, iform)) = XPCNF (aL, primForm (dualForm iform))++ dualizeXPCNF :: Ord a => XPCNF a -> XPDNF a+ dualizeXPCNF (XPCNF (aL, iform)) = XPDNF (aL, primForm (dualForm iform))++-- The MixForm algebra++ instance Ord a => PropAlg a (MixForm a) where+ at x = PDNF ([x], atomForm 1) -- alernatively = PCNF ([x], atomForm 1)+ false = PDNF ([], botForm)+ true = PCNF ([], botForm)+ neg (M2DNF (aL, iform)) = M2CNF (aL, invertForm iform)+ neg (M2CNF (aL, iform)) = M2DNF (aL, invertForm iform)+ neg (PDNF (aL, iform)) = PCNF (aL, invertForm iform)+ neg (PCNF (aL, iform)) = PDNF (aL, invertForm iform)+ conj [] = true+ conj [form] = form+ conj formL = M2CNF (aL, m2form (formListJoin iformL))+ where (aL,iformL) = unifyXForms cnfL+ cnfL = map cnf formL+ cnf (M2CNF (aL,iform)) = (aL, iform)+ cnf (M2DNF (aL,iform)) = (aL, dualForm iform)+ cnf (PCNF (aL,iform)) = (aL, iform)+ cnf (PDNF (aL,iform)) = (aL, dualForm iform)+ disj [] = false+ disj [form] = form+ disj formL = M2DNF (aL, m2form (formListJoin iformL))+ where (aL,iformL) = unifyXForms dnfL+ dnfL = map dnf formL+ dnf (M2CNF (aL,iform)) = (aL, dualForm iform)+ dnf (M2DNF (aL,iform)) = (aL, iform)+ dnf (PCNF (aL,iform)) = (aL, dualForm iform)+ dnf (PDNF (aL,iform)) = (aL, iform)+ subj [] = true+ subj [form] = PCNF (atoms form, botForm)+ subj formL = fromPropForm (SJ (map toPropForm formL))+ equij [] = true+ equij [form] = PCNF (atoms form, botForm)+ equij formL = fromPropForm (EJ (map toPropForm formL))+ valid (M2DNF (aL,iform)) = primForm iform == topForm+ valid (M2CNF (aL,iform)) = iform == botForm+ valid (PDNF (aL,iform)) = iform == topForm+ valid (PCNF (aL,iform)) = iform == botForm+ satisfiable (M2DNF (aL,iform)) = iform /= botForm+ satisfiable (M2CNF (aL,iform)) = primForm iform /= topForm+ satisfiable (PDNF (aL,iform)) = iform /= botForm+ satisfiable (PCNF (aL,iform)) = iform /= topForm+ subvalent form1 form2 = valid (subj [form1, form2])+ equivalent form1 form2 = valid (equij [form1, form2])+ covalent form1 form2 = satisfiable (conj [form1, form2])+ properSubvalent form1 form2 = subvalent form1 form2 && not (equivalent form1 form2)+ properDisvalent form1 form2 = disvalent form1 form2 && satisfiable form1 && satisfiable form2+ atoms (M2DNF (aL,iform)) = aL+ atoms (M2CNF (aL,iform)) = aL+ atoms (PDNF (aL,iform)) = aL+ atoms (PCNF (aL,iform)) = aL+ redAtoms (M2DNF (aL,iform)) = xformRedAtoms (aL, primForm iform)+ redAtoms (M2CNF (aL,iform)) = xformRedAtoms (aL, primForm iform)+ redAtoms (PDNF xform) = xformRedAtoms xform+ redAtoms (PCNF xform) = xformRedAtoms xform+ irrAtoms (M2DNF (aL,iform)) = xformIrrAtoms (aL, primForm iform)+ irrAtoms (M2CNF (aL,iform)) = xformIrrAtoms (aL, primForm iform)+ irrAtoms (PDNF xform) = xformIrrAtoms xform+ irrAtoms (PCNF xform) = xformIrrAtoms xform+ ext (M2DNF xform) aL = M2DNF (newAtomsXForm xform aL)+ ext (M2CNF xform) aL = M2CNF (newAtomsXForm xform aL)+ ext (PDNF xform) aL = PDNF (newAtomsXForm xform aL)+ ext (PCNF xform) aL = PCNF (newAtomsXForm xform aL)++ infRed form yL = M2CNF (yL', m2form iform')+ where (PCNF (xL, iform)) = mixToPCNF form+ (yL',iform') = newAtomsXForm (xL, iform) (O.olist yL)+ supRed form yL = M2DNF (yL', m2form iform')+ where (PDNF (xL, iform)) = mixToPDNF form+ (yL',iform') = newAtomsXForm (xL, iform) (O.olist yL)+ infElim form yL = infRed form (O.difference (atoms form) (O.olist yL))+ supElim form yL = supRed form (O.difference (atoms form) (O.olist yL))+ toPropForm = fromMixForm+ fromPropForm = toM2DNF -- alternatively: toM2CNF++ mixToPDNF :: Ord a => MixForm a -> MixForm a+ mixToPDNF (M2DNF (aL, iform)) = PDNF (aL, primForm iform)+ mixToPDNF (M2CNF (aL, iform)) = PDNF (aL, primForm (dualForm iform))+ mixToPDNF (PDNF xform) = PDNF xform+ mixToPDNF (PCNF (aL, iform)) = PDNF (aL, primForm (dualForm iform))++ mixToPCNF :: Ord a => MixForm a -> MixForm a+ mixToPCNF (M2DNF (aL, iform)) = PCNF (aL, primForm (dualForm iform))+ mixToPCNF (M2CNF (aL, iform)) = PCNF (aL, primForm iform)+ mixToPCNF (PDNF (aL, iform)) = PCNF (aL, primForm (dualForm iform))+ mixToPCNF (PCNF xform) = PCNF xform
+ Main.hs view
@@ -0,0 +1,127 @@+{-+ compile with+ ghc --make -o PropLogic Main.hs+ and run with+ ./PropLogic ....+-}+module Main where++-- imports++ import System (getArgs)+ import qualified TextDisplay as D+ import qualified Costack as C+ import PropLogic++-- main function++ briefHelpMessage = D.correctTextFrame+ [ "Syntax of the PropLogic command: ",+ " PropLogic -- print this help ",+ " PropLogic help -- print a more detailed help (with more options) ",+ " PropLogic pdnf PROPFORM -- the Prime Disjunctive Normal Form of PROPFORM ",+ " PropLogic pcnf PROPFORM -- the Prime Conjunctive Normal Form of PROPFORM ",+ " PropLogic spdnf PROPFORM -- the Simplified Prime Disjunctive Normal Form ",+ " PropLogic scdnf PROPFORM -- the Simplified Prime Conjunctive Normal Form ",+ " PropLogic xpdnf PROPFORM -- the Extended/Indexed Prime Disjunctive Normal Form ",+ " PropLogic xpcnf PROPFORM -- the Extended/Indexed Prime Conjunctive Normal Form ",+ "where in each case, PROPFORM is a propositional formula in fancy notation and ",+ "wrapped in double quotes \"...\"." ]++ fullHelpMessage = D.correctTextFrame+ [ "+---------------------------------------------------------------------------+",+ "| (Fancy) Syntax of Propositional Formulas: |",+ "+---------------------+-----------------------------+-----------------------+",+ "| w | for every atom w | (atomic formula) |",+ "| false | | (zero or false value) |",+ "| true | | (unit or true value) |",+ "| -p | for every formula p | (negation) |",+ "| [p1 * ... * pN] | for N>=0 formulas p1,...,pN | (conjunction) |",+ "| [p1 + ... + pN] | for N>=0 formulas p1,...,pN | (disjunction) |",+ "| [p1 -> ... -> pN] | for N>=0 formulas p1,...,pN | (subjunction) |",+ "| [p1 <-> ... <-> pN] | for N>=0 formulas p1,...,pN | (equijunction) |",+ "+---------------------+-----------------------------+-----------------------+",+ "| where an atom w is any non-empty sequence of letters and digits, except |",+ "| the keywords 'true' and 'false'. |",+ "+---------------------------------------------------------------------------|",+ "",+ "Example formulas are:",+ "",+ " [-x + [z <-> true] + -x + 23 + -y + -[x -> y] + [z * -7]]",+ "",+ " [[-x + y] <-> [x -> y] <-> -[x * -y] <-> [false -> x -> y -> true]]",+ "",+ "+----------------------------------------------------------------------+",+ "| Definition of I-Forms |",+ "+----------------------------------------------------------------------+",+ "| An I-Form is a list [L1,...,Ln] of n I-Lines. Each I-Line is a list |",+ "| [I1,...,Im] of integers, so that their absolute values are in strict |",+ "| ascending order, i.e. abs(I1) < ... < abs(Im). |",+ "+----------------------------------------------------------------------+",+ "",+ "Example I-Forms are:",+ "",+ " [[-2,4,6],[1,3,5,7],[-1,2,-3,4,-5,6],[],[-3],[3],[1,2,3,4,5,6,7]]",+ "",+ " [[]]",+ "",+ "+------------------------------------------------------------------------------------+",+ "| Syntax of the PropLogic command |",+ "+---------------------------+--------------------------------------------------------+",+ "| PropLogic | print a brief overview of important command options |",+ "| PropLogic help | print a more detailed help (namely this one)lp |",+ "| PropLogic pdnf PROPFORM | the Prime Disjunctive Normal Form of PROPFORM |",+ "| PropLogic pcnf PROPFORM | the Prime Conjunctive Normal Form of PROPFORM |",+ "| PropLogic spdnf PROPFORM | the Simplified Prime Disjunctive Normal Form |",+ "| PropLogic scdnf PROPFORM | the Simplified Prime Conjunctive Normal Form |",+ "| PropLogic xpdnf PROPFORM | the Extended/Indexed Prime Disjunctive Normal Form |",+ "| PropLogic xpcnf PROPFORM | the Extended/Indexed Prime Conjunctive Normal Form |",+ "| PropLogic primForm IFORM | the Prime Normal Form of the given IFORM |",+ "| PropLogic testing X Y Z N | performs test runs of Prime Form with randomly |",+ "| | generated I-Forms. The four integer parameters are: |",+ "| | X is the number of (different) atoms of the I-Form |",+ "| | Y is the length of the randomly generated I-Form |",+ "| | Z is the average length of the I-Lines in the I-Form |",+ "| | N is the number of test runs. |",+ "+---------------------------+--------------------------------------------------------+",+ "| where |",+ "| PROPFORM is a propositional formula (see below) surrounded by double quotes, |",+ "| IFORM is an I-Form (see below) surrounded by double quotes. |",+ "+------------------------------------------------------------------------------------+",+ "",+ "Legal example calls of the PropLogic command are:",+ "",+ " PropLogic spdnf \"[-x + [z <-> true] + -x + 23 + -y + -[x -> y] + [z * -7]]\" ",+ "",+ " PropLogic primForm \"[[-2,3],[1,2,3],[1,2,-3],[-1,4],[-2,4]]\"",+ "",+ " PropLogic testing 5 20 4 100",+ "",+ "More help and other material:",+ " http://www.bucephalus.org/PropLogic",+ "" ]++ main :: IO ()+ main = do args <- getArgs+ let act = case args of+ [] -> D.printTextFrame briefHelpMessage+ ["help"] -> D.printTextFrame fullHelpMessage+ ["pdnf", form] -> pdnf form+ ["pcnf", form] -> pcnf form+ ["spdnf", form] -> spdnf form+ ["spcnf", form] -> spcnf form+ ["xpdnf", form] -> xpdnf form+ ["xpcnf", form] -> xpcnf form+ ["primForm", intLL] -> print (prim intLL)+ ["testing", x, y, z, n] -> do t <- verboseRandomPrimeTesting (read x, read y, read z) (read n)+ print t+ otherwise -> do print "Unknown arguments for PropLogic!"+ D.printTextFrame briefHelpMessage+ act+ return ()+ where prim intLL = let intLL' = (read intLL) :: [[Int]]+ iform = iForm intLL'+ pform = primForm iform+ intLL'' = map C.toList (C.toList pform)+ in intLL''+
+ Olist.hs view
@@ -0,0 +1,268 @@+{- |+ An 'Olist' is an /ordered list/. The main function of this module is the implementation of the finite subset structure of a given type @a@. Finite sets are represented as ordered lists and the basic set functions and relations like 'union', 'intersection', 'included' etc. are provided.+-}++module Olist (++ -- * The @Olist@ type++ Olist,++ -- * The construction and test for ordered lists++ olist,+ -- | For example,+ --+ -- > > olist ["b", "c", "b", "a", "c", "a"]+ -- > ["a","b","c"]+ --+ -- As the example shows, multiple occuring members are deleted.+ --+ -- (The implementation builts the ordered list with component-wise 'insert' and that is not an optimal sorting algorithm in general.+ -- But it is optimal, when the argument is an already ordered list. We use 'olist' only as a an additional safety-mechanism for+ -- functions like @ext :: p -> [a] -> p@, where in most cases the second argument will usually be an @Olist a@ value, anyway.)++ isOlist,+ -- | Checks if the given argument is ordered.++ -- * The empty list++ empty,+ -- | Returns the empty list @[]@, i.e.+ --+ -- > > Olist.empty+ -- > []+ --+ -- (Note, that there is also an @empty@ function in the @Costack@ module.)++ isEmpty,+ -- | Checks on emptiness; i.e. it is the same as the Haskell native @null@.+ --+ -- > > isEmpty [1,2,3]+ -- > False++ -- * Singular operations on ordered lists++ member,+ -- | For example,+ --+ -- > > member 7 [3,5,7,9]+ -- > True+ -- > > 4 `member` [2,3,4,5]+ -- > True++ insert,+ -- | For example,+ --+ -- > > insert 7 [3,5,9,11]+ -- > [3,5,7,9,11]+ -- > > insert 7 [3,5,7,9,11]+ -- > [3,5,7,9,11]++ delete,+ -- | For example,+ --+ -- > > delete 7 [3,5,7,9,11]+ -- > [3,5,9,11]+ -- > > delete 7 [3,5,9,11]+ -- > [3,5,9,11]++ -- * The common binary operations on sets++ -- | These functions all assume, that the arguments are actually 'Olist' values. Otherwise, the function doesn't terminate with an+ -- error, it just produces unintended results.++ included,+ -- | Implementation of ⊆ on (finite) sets. For example,+ --+ -- > > included "acd" "abcd" -- recall, that "acd" is the list ['a', 'c', 'd']+ -- > True+ -- > > [2,4] `included` [1,2,3,4,5]+ -- > True++ properlyIncluded,+ -- | Implementation of the strict version ⊂ of ⊆, i.e. the first argument must be included, but different to the second one.++ disjunct,+ -- | Two finite sets, i.e. two ordered lists are /disjunct/ iff they do not have a common member. For example+ --+ -- > > disjunct "acd" "bef"+ -- > True+ -- > > "abc" `disjunct` "bef"+ -- > False+ -- > > [] `disjunct` [1,2,3]+ -- > True++ properlyDisjunct,+ -- | Two finite sets are /properly disjunct/ iff they are disjunct and none of them is empty.+ --+ -- > > [] `properlyDisjunct` [1,2,3]+ -- > False++ equal,+ -- | The equality of two finite sets; actually it is just another name for @(==)@ on ordered lists.++ union,+ -- | The implementation of ∪, for example+ --+ -- > > [1,2,4,5] `union` [1,3,5,7]+ -- > [1,2,3,4,5,7]++ intersection,+ -- | The implementation of ∩, for example+ --+ -- > > [1,2,4,5] `intersection` [1,3,5,7]+ -- > [1,5]++ difference,+ -- | Implementation of the difference operator \ on sets. For example,+ --+ -- > > [1,2,4,5] `difference` [1,3,5,7]+ -- > [2,4]++ opposition,+ -- | The /opposition/ or /symmetric difference/ @S@∇@T@ of two sets @S@, @T@ is defined as @(S\T)∪(T\S)@. For example,+ --+ -- > > [1,2,4,5] `opposition` [1,3,5,7]+ -- > [2,3,4,7]++ unionList,+ -- | Returns the union of a list of ordered lists. For example,+ --+ -- > > unionList [[1,3,5], [1,2,3], [1,5,9]]+ -- > [1,2,3,5,9]+ -- > > unionList []+ -- > []++ intersectionList,+ -- | Returns the intersection of a list of ordered lists. The result is undefined for the empty list.+ --+ -- > > intersectionList [[1,3,5], [1,2,3], [1,5,9]]+ -- > [1]+ -- > > intersectionList []+ -- > *** Exception: Olist.intersectionList: not defined for empty list argument++) where ---------------------------------------------------------------------------------------------------------------++-- the type of ordered lists++ type Olist a = [a]++-- order list construction++ olist :: Ord a => [a] -> Olist a+ olist [] = []+ olist (a:aL) = insert a (olist aL)++ isOlist :: Ord a => [a] -> Bool+ isOlist [] = True+ isOlist [a] = True+ isOlist (a:b:cL) = (a < b) && isOlist (b:cL)++-- empty list++ empty :: Ord a => Olist a+ empty = []++ isEmpty :: Ord a => Olist a -> Bool+ isEmpty = null++-- singular operations++ member :: Ord a => a -> Olist a -> Bool+ member a [] = False+ member a (b:bL) = case compare a b of+ LT -> False+ EQ -> True+ GT -> member a bL++ insert :: Ord a => a -> Olist a -> Olist a+ insert a [] = [a]+ insert a (b:bL) = case compare a b of+ LT -> a:b:bL+ EQ -> b:bL+ GT -> b : (insert a bL)++ delete :: Ord a => a -> Olist a -> Olist a+ delete a [] = []+ delete a (b:bL) = case compare a b of+ LT -> b:bL+ EQ -> bL+ GT -> b : (delete a bL)++-- binary operations++ included :: Ord a => Olist a -> Olist a -> Bool+ included [] bL = True+ included aL [] = False+ included (a:aL) (b:bL) = case compare a b of+ LT -> False+ EQ -> included aL bL+ GT -> included (a:aL) bL++ properlyIncluded :: Ord a => Olist a -> Olist a -> Bool+ properlyIncluded [] [] = False+ properlyIncluded [] bL = True+ properlyIncluded aL [] = False+ properlyIncluded (a:aL) (b:bL) = case compare a b of+ LT -> False+ EQ -> properlyIncluded aL bL+ GT -> included (a:aL) bL++ disjunct :: Ord a => Olist a -> Olist a -> Bool+ disjunct [] bL = True+ disjunct bL [] = True+ disjunct (a:aL) (b:bL) = case compare a b of+ LT -> disjunct aL (b:bL)+ EQ -> False+ GT -> disjunct (a:aL) bL++ properlyDisjunct :: Ord a => Olist a -> Olist a -> Bool+ properlyDisjunct [] bL = False+ properlyDisjunct bL [] = False+ properlyDisjunct (a:aL) (b:bL) = case compare a b of+ LT -> disjunct aL (b:bL)+ EQ -> False+ GT -> disjunct (a:aL) bL++ equal :: Ord a => Olist a -> Olist a -> Bool+ equal = (==)++ union :: Ord a => Olist a -> Olist a -> Olist a+ union [] bL = bL+ union aL [] = aL+ union (a:aL) (b:bL) = case compare a b of+ LT -> a : (union aL (b:bL))+ EQ -> a : (union aL bL)+ GT -> b : (union (a:aL) bL)++ intersection :: Ord a => Olist a -> Olist a -> Olist a+ intersection [] bL = []+ intersection aL [] = []+ intersection (a:aL) (b:bL) = case compare a b of+ LT -> intersection aL (b:bL)+ EQ -> a : (intersection aL bL)+ GT -> intersection (a:aL) bL++ difference :: Ord a => Olist a -> Olist a -> Olist a+ difference [] bL = []+ difference aL [] = aL+ difference (a:aL) (b:bL) = case compare a b of+ LT -> a : (difference aL (b:bL))+ EQ -> difference aL bL+ GT -> difference (a:aL) bL++ opposition :: Ord a => Olist a -> Olist a -> Olist a+ opposition [] bL = bL+ opposition aL [] = aL+ opposition (a:aL) (b:bL) = case compare a b of+ LT -> a : (opposition aL (b:bL))+ EQ -> opposition aL bL+ GT -> b : (opposition (a:aL) bL)++ unionList :: Ord a => [Olist a] -> Olist a+ unionList = foldl union []++ intersectionList :: Ord a => [Olist a] -> Olist a+ intersectionList [] = error "Olist.intersectionList: not defined for empty list argument"+ intersectionList aL = foldl1 intersection aL
+ PropLogic.cabal view
@@ -0,0 +1,29 @@+Name: PropLogic+Version: 0.9+Cabal-Version: >= 1.2+Build-type: Simple+License: BSD3+-- License: PublicDomain+-- License-file: LICENSE.txt+Author: bucephalus+Maintainer: b@bucephalus.org+Stability: experimental+Homepage: http://www.bucephalus.org/PropLogic+Bug-reports: http://www-bucephalus-org.blogspot.com/PropLogic-bugs+-- Package-url: http://www.bucephalus.org/....+Category: Logic, Algorithms+Synopsis: A system for propositional logic with default and fast instances of propositional algebras.+-- Description: ....++Library+ exposed-modules:+ PropLogic, Olist, PropLogicCore, DefaultPropLogic, FastPropLogic, PropLogicTest, Main+ other-modules:+ TextDisplay, Costack+ build-depends:+ base < 5, haskell98+ extensions:+ TypeSynonymInstances, FlexibleInstances, MultiParamTypeClasses++Executable program+ Main-Is: Main.hs
+ PropLogic.hs view
@@ -0,0 +1,190 @@+{-# LANGUAGE TypeSynonymInstances, FlexibleInstances, MultiParamTypeClasses #-}++{- |+ A powerful system for /propositional logic/.+ Defines an abstract concept of a /propositional algebra/ and provides both default and fast instances.+ Emphasizes the use of /(canonic) normalizations/ in general and so-called /Prime Normal Forms/ in particular.++ <http://www.bucephalus.org/PropLogic/>++ is the homepage with additional information for a variety of users, including short and thorough introductions to the+ use of "PropLogic" and the mathematical background of the whole design.+-}++module PropLogic (++ -- * Start+ -- | The whole package is very modular in itself, according to the different perspectives we take to approach the subject+ -- (as explained below). It is possible to be more specific in an application and to import only certain parts. But the+ -- easiest and recommended way is the import of just this "PropLogic" module, which is just the summary of its main parts.+ --+ -- This package uses certain extensions to the Haskell 98 standard.+ -- In particular, the /propositional algebra/ concept is implemented as a two-parameter type class 'PropAlg'.+ -- The package is developed with GHC (the Glasgow Haskell Compiler) and that works fine.+ -- Hugs works fine as well, but it requires to be started with @hugs -98@.++ -- * The composition and modules++ -- ** Introduction+ -- | /Propositional logic/ (also called /sentential logic/) is a very standard and relatively uncomplicated system in itself.+ --+ -- The (binary) /boolean value algebra/ is one of the simplest structures at all and a standard in almost every programming language.+ -- (Recall, that it is in Haskell given by the type @Bool@, made of @True@ and @False@, the+ -- order @<=@ and the boolean junctors @not@, @&&@ and @||@.)+ -- A /propositional algebra/ is then essentially defined as the extension of this boolean value algebra with free variables,+ -- commonly called /atoms/.+ --+ -- But however dense an abstract characterization of a propositional algebra may be, most traditional introductions are more complex and+ -- start with a syntax, i.e. some choice of what /propositional formulas/ should cover, a more or less diverse semantics, together+ -- with some calculus for semantically sound and complete manipulation of formulas.++ -- ** The four main modules+ -- | In this Haskell version of propositional logic, one design principle is the separation of the different aspects in four+ -- main modules.+ --+ -- >+ -- >+ -- > PropLogicCore+ -- > / \+ -- > / \+ -- > / \+ -- > / \+ -- > DefaultPropLogic FastPropLogic+ -- > \ /+ -- > \ /+ -- > \ /+ -- > \ /+ -- > PropLogicTest+ -- >++ -- ** The abstract /core/ concepts++ module PropLogicCore,++ -- | This module comprises the abstract definition of two core concepts of propositional logic:+ --+ -- * The data type @('PropForm' a)@ of /propositional formulas/, based on a given /atom/ type @a@.+ --+ -- * The two-parameter type class @('PropAlg' a p)@ of a /propositional algebra/, where @a@ is the /atom/ type and @p@ the type of+ -- /propositions/. Operations of such a structure include a decision if two propositions are 'equivalent', if a given proposition is+ -- 'satisfiable', a converter 'toPropForm' and the inverse 'fromPropForm', which turns a propositional formula into a proposition.+ --+ -- "PropLogicCore" provides the interface for the toolbox most users would need in most real circumstances.+ -- The actual 'PropAlg' instances are implemented in the following two modules.++ -- ** Propositional logic the /default/ style and the descriptive introduction of (canonic) normalizations++ module DefaultPropLogic,++ -- | "DefaultPropLogic" on the other hand provides one (actually more than one) instance of 'PropAlg', along with a whole range of+ -- additional functionalities. For example, it introduces the concepts of /valuators/ and a /truth tables/.+ -- The title /default/ indicates the very straight forward, intuitive, and naive approach.+ -- For example, the implementation for the satisfiability+ -- function applies the naive test, if the truth table has at least one /true/ in the result column.+ -- In fact, in "DefaultPropLogic", the semantics of propositional algebra is thoroughly reconstructed and that makes this+ -- module suitable as an interactive tutorial for propositional logic itself and all the concepts of the abstract level.+ -- (There is an according introduction available online.)++ -- | The "DefaultPropLogic" introduces something else, namely a non-traditional idea of what the standard operations are.+ -- We don't bother with the introduction of a certain rule system or calculus and we don't reconstruct propositional logic as+ -- a proof system.+ -- Our approach is based on /(canonic) normalizations/ instead.+ -- In particular, we use special kinds of /DNF/s and /CNF/s (/disjunctive/ or /conjunctive normal forms/), namely+ -- /prime normal forms/, and all traditional problems come down to a single normalization.+ -- For example, a formula φ is satisfiable iff the prime DNF is not the empty disjunction,+ -- i.e. iff the call of @primeDNF φ@ returns another result than @(∨)@.+ -- All traditional problems can be solved with one single canonization such as 'primeDNF' or 'primeCNF', respectively.++ -- ** Instances of propositional algebras with /fast/ implementations++ module FastPropLogic,++ -- | Prime Normal Forms are indeed distinguished and reasonably compact semantic canonizations of propositional formulas.+ -- However, for all cases with more than just a trivial amount of atoms involved, the default implementations are not feasible,+ -- because of the exponential cost explosing of these default methods.+ -- In "FastPropLogic" we provide a complete new implementation, based on a /fast/ system of algorithms.+ -- Main goal is the construction of fast instances of the 'PropAlg' type class.++ -- ** Additional functions++ module PropLogicTest,++ -- | The independent implementations of the default and the fast approach allows us to use one as a test for the other, because+ -- they should produce the same results. To do that systematically, "PropLogicTest" has random formula generators and test for+ -- correctness.+ -- Another goal is the investigation of the actual performance of the /fast/ methods.+ -- Finally, this module contains some useful functions which use functions from both "DefaultPropLogic" and "FastPropLogic".++ -- ** Hidden modules+ -- | "TextDisplay" implements some methods for the two-dimensional treatment of plain text output. This is a useful tool, for+ -- example for the display of truth tables in interpreter sessions. It provides the 'display' function which can be applied to+ -- all the main concepts (formulas, truth tables, normal forms), for more intuitive and graphical layout than calling 'print'.+ --+ -- "Olist" has methods for treating ordered lists as finite sets.+ --+ -- "Costack" is the implementation of a /concatenable stack/, i.e. it re-defines the standard Haskell functions+ -- @(:)@, @(null)@, @head@, @tail@, and @(++)@. The concatenation @(++)@ is not a primitive function in Haskell, and a /costack/+ -- is a data structure, where all these functions are primitive.+ -- The "Costack" module is only used in the implementations of the "FastPropLogic" functions.++ -- * Propositional algebras+ -- | As mentioned already, the two core concepts in the implementation of our version of propositional logic are+ -- /propositional formulas/, given as the data type @'PropForm' a@, and the two-parameter type class @'PropAlg' a p@+ -- for the abstract notion of a /propositional algebra/.+ -- These two notions are described in more detail in the "PropLogicCore" module.++ -- ** The different instances+ -- | The actual implementation of 'PropAlg' instances is done in two other modules and in two different ways:+ --+ -- (I) In the "DefaultPropLogic" module, we implement three different propositional algebras in a standard, intuitive and straight+ -- forward way.+ --+ -- (1) @(PropAlg a ('PropForm' a))@, is the standard propositional algebra, where the propositions are actually the propositional+ -- formulas.+ --+ -- (2) @(PropAlg a ('TruthTable' a))@ is a less common, but nevertheless very intuitive propositional algebra, which is based on+ -- /truth tables/.+ --+ -- (3) @(PropAlg 'Void' 'Bool')@ instantiates the predefined algebra @Bool@ of boolean values as a propositional algebra, the+ -- one with the empty atom type @Void@. Actually, all other instances of propositional algebras are equally powerful in the+ -- sense that they can all be based on an arbitrary type @a@ of atoms. But the propositional algebra on @Bool@ is just the+ -- trivial algebra with the empty atom type and we neglect it in the comparison of the different instances below.+ --+ -- (II) In the "FastPropLogic" module defines a small variety of propositional algebras where the propositions are certain kinds of+ -- /normal forms/.+ --+ -- (1) @(PropAlg a ('XPDNF' a))@ is the algebra, where each proposition is an /indexed prime disjunctive normal form/.+ -- One distinctive feature of these forms is that they are /canonic/ in the sense that two propositions are equivalent if and only+ -- if they are equal.+ --+ -- (2) @(PropAlg a ('XPCNF' a))@ is the /dual/ version of the previous algebra, elements are /indexed prime conjunctive normal forms/.+ --+ -- (3) @(PropAlg a ('MixForm' a))@ is a variation and mix of the previous two algebras. The normal forms here may be either+ -- /conjunctive/ or /disjunctive normal forms/, they are not necessarily /prime/ normal forms, but may only be /pairwise minimal/.+ -- So in this algebra, the propositions are no longer canonic. But the advantage is that all the junctions, i.e. the boolean+ -- operations such as negation, conjunction etc. are of polynomial complexity. And in applications, where predominanty junctions+ -- are used, this implementation of a propositional algebra is faster than the previous two.++ -- ** Feasibility and performance of the fast implementations+ -- | The default instances of 'PropAlg' (i.e. on formulas and truth tables) are not feasible for other than small problems, and+ -- that is why we implemented some fast instances as well.+ -- One example for a cost explosing is the call of 'satisfiable' applied to a formula φ. If φ has say @n@ different atoms,+ -- then there are @2^n@ different valuations of these atoms and in the worst case, we need to test for all these valuations, if+ -- they make φ true or false. /Not feasible/ means /exponential in the worst input cases/.+ -- Not all functions of the algebra on formulas are not feasible in this sense.+ -- But compare to the default instances, the fast instances are called /fast/, because none of their functions is exponential.+ --+ -- In fact, we cannot claim really, that this is actually true. We don't have a proof for the non-exponentiality of the fast functions.+ -- The only criterion for the feasibility of our implementations is empirical.+ -- For more detail and empirical data about the performance of the involved functions, we refer to the home page.++) where++ import TextDisplay+ import Olist+ import Costack+ import PropLogicCore+ import DefaultPropLogic+ import FastPropLogic+ import PropLogicTest+
+ PropLogicCore.hs view
@@ -0,0 +1,315 @@+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}++{- |+ This module comprises the abstract definition of two core concepts of propositional logic:++ * The data type @('PropForm' a)@ of /propositional formulas/, based on a given /atom/ type @a@.++ * The two-parameter type class @('PropAlg' a p)@ of a /propositional algebra/, where @a@ is the /atom/ type and @p@ the type of+ /propositions/. Operations of such a structure include a decision if two propositions are 'equivalent', if a given proposition is+ 'satisfiable', a converter 'toPropForm' and the inverse 'fromPropForm', which turns a propositional formula into a proposition.+-}++module PropLogicCore (++ -- * Propositional formulas+ PropForm (..),++ -- | A typical example of a propositional formula φ in standard mathematical notation is given by+ --+ -- @¬(rain ∧ snow) ∧ (wet ↔ (rain ∨ snow)) ∧ (rain → hot) ∧ (snow → ¬ hot)@+ --+ -- The primitive elements @hot@, @rain@, @snow@ and @wet@ are the /atoms/ of φ.+ -- In Haskell, we define propositional formulas as members of the data type (@PropForm a@), where the type parameter @a@ is the+ -- chosen atom type. A suitable choice for our example would be the atom type @String@ and φ becomes a member of+ -- @PropForm String@ type, namely+ --+ -- > CJ [N (CJ [A "rain", A "snow"]), EJ [A "wet", DJ [A "rain", A "snow"]], SJ [A "rain", A "hot"], SJ [A "snow", N (A "hot")]]+ --+ -- This Haskell version is more tedious and we introduce a third notation for nicer output by making @PropForm@ an instance of the+ -- 'Display' type class. A call of @'display' φ@ then returns+ --+ -- > [-[rain * snow] * [wet <-> [rain + snow]] * [rain -> hot] * [snow -> -hot]]+ --+ -- The following overview compares the different representations:+ --+ -- > Haskell displayed as kind of formula+ -- > --------------------------------------------------------------------+ -- > A x x (without quotes) atomic formula+ -- > F false the boolean zero value+ -- > T true the boolean unit value+ -- > N p -p negation+ -- > CJ [p1,...,pN] [p1 * ... * pN] conjunction+ -- > DJ [p1,...,pN] [p1 + ... + pN] disjunction+ -- > SJ [p1,...,pN] [p1 -> ... -> pN] subjunction+ -- > EJ [p1,...,pN] [p1 <-> ... <-> pN] equijunction+ --+ -- Note, that the negation is unary, as usual, but the last four constructors are all multiary junctions, i.e. the list @[p1,...,pN]@+ -- may have any number @N@ of arguments, including @N=0@ and @N=1@.+ --+ -- @PropForm a@ is an instance of @Eq@ and @Ord@, two formulas can be compared for linear order with @<@ or @compare@ and+ -- @PropForm a@ alltogther is linearly ordered, provided that @a@ itself is.+ -- But note, that this order is a pure formal expression order does neither reflect the atomical quasi-order structure+ -- (induced by the @subatomic@ relation; see below) nor the semantical quasi-order structure (induced by @subvalent@).+ -- So this is not the order that reflects the idea of propositional logic.+ -- But we do use it however for the sorting and order of formulas to reduce ambiguities and increase+ -- the efficiency of algorithmes on certain normal forms.+ -- In "DefaultPropLogic" we introduce the normal forms 'OrdPropForm' and the normalizer 'ordPropForm'.+ --+ -- @PropForm a@ is also an instance of @'Read'@ and @'Show'@, so String conversion (and displaying results in the interpreter) are+ -- well defined. For example+ --+ -- > show (CJ [A 3, N (A 7), A 4]) == "CJ [A 3,N (A 7),A 4]"+ --+ -- Note, that reading a formula, e.g.+ --+ -- > read "SJ [A 3, A 4, T]"+ --+ -- issues a complaint due to the ambiguity of the atom type. But that can be fixed, e.g. by stating the type explicitely,+ -- as in+ --+ -- > (read "SJ [A 3, A 4, T]") :: PropForm Integer+ --++ -- ** Parsing propositional formulas on string atoms+ stringToProp,++ -- | ... CONTINUEHERE ....++ -- * Propositional algebras+ PropAlg (..),++ -- | @PropAlg a p@ is a structure, made of+ --+ -- @a@ is the /atom/ type+ --+ -- @p@ is the type of /propositions/+ --+ -- @'at' :: a -> p@ is the /atomic proposition/ constructor, similar to the constructor 'A' for atomic formulas.+ --+ -- Similar to the definition of 'PropForm', we have the same set of boolean junctors on propositions:+ -- @'false', 'true' :: p@, @'neg' :: p-> p@ and @'conj', 'disj', 'subj', 'equij' :: [p] -> p@+ --+ -- There the set of+ -- ......................................................................++) where ---------------------------------------------------------------------------------------------------------------++-- imports++ import qualified List as L+ import qualified TextDisplay as D+ import qualified Olist as O++-- the PropForm data type++ data PropForm a+ = A a+ | F+ | T+ | N (PropForm a)+ | CJ [PropForm a]+ | DJ [PropForm a]+ | SJ [PropForm a]+ | EJ [PropForm a]+ deriving (Show, Read, Eq)++-- the PropAlg class++ class Ord a => PropAlg a p | p -> a where+ -- the signature+ -- atomic proposition constructor+ at :: a -> p+ -- boolean junctors+ false :: p+ true :: p+ neg :: p -> p+ conj :: [p] -> p+ disj :: [p] -> p+ subj :: [p] -> p+ equij :: [p] -> p+ -- semantic properties and relations+ valid :: p -> Bool+ satisfiable :: p -> Bool+ contradictory :: p -> Bool+ subvalent :: p -> p -> Bool+ equivalent :: p -> p -> Bool+ covalent :: p -> p -> Bool+ disvalent :: p -> p -> Bool+ properSubvalent :: p -> p -> Bool+ properDisvalent :: p -> p -> Bool+ -- atom sets+ atoms :: p -> O.Olist a+ redAtoms :: p -> O.Olist a+ irrAtoms :: p -> O.Olist a+ -- atomic properties and relations+ nullatomic :: p -> Bool+ subatomic :: p -> p -> Bool+ equiatomic :: p -> p -> Bool+ coatomic :: p -> p -> Bool+ disatomic :: p -> p -> Bool+ properSubatomic :: p -> p -> Bool+ properDisatomic :: p -> p -> Bool+ -- atomic modifiers+ ext :: p -> [a] -> p+ infRed :: p -> [a] -> p+ supRed :: p -> [a] -> p+ infElim :: p -> [a] -> p+ supElim :: p -> [a] -> p+ -- biequivalence+ biequivalent :: p -> p -> Bool+ -- meta properties+ pointwise :: (p -> Bool) -> [p] -> Bool+ pairwise :: (p -> p -> Bool) -> [p] -> Bool+ -- formula conversions+ toPropForm :: p -> PropForm a+ fromPropForm :: PropForm a -> p+ -- some implementations+ pointwise = all+ pairwise property pL =+ case pL of+ [] -> True+ [x] -> True+ (x:xL) -> (all (property x) xL) && (pairwise property xL)+ contradictory p = not (satisfiable p)+ satisfiable p = not (contradictory p)+ covalent p1 p2 = not (disvalent p1 p2)+ disvalent p1 p2 = not (covalent p1 p2)+ nullatomic p = O.isEmpty (atoms p)+ subatomic p1 p2 = O.included (atoms p1) (atoms p2)+ equiatomic p1 p2 = O.equal (atoms p1) (atoms p2)+ coatomic p1 p2 = not (disatomic p1 p2)+ disatomic p1 p2 = O.disjunct (atoms p1) (atoms p2)+ properSubatomic p1 p2 = O.properlyIncluded (atoms p1) (atoms p2)+ properDisatomic p1 p2 = O.disjunct aL1 aL2 && not (O.isEmpty aL1) && not (O.isEmpty aL2)+ where aL1 = atoms p1+ aL2 = atoms p2+ biequivalent p1 p2 = equiatomic p1 p2 && equivalent p1 p2++-- displaying formulas++ instance D.Display a => D.Display (PropForm a) where+ textFrame form =+ let falseSymbol = "false"+ trueSymbol = "true"+ negSymbol = "-"+ conjSymbol = "*"+ disjSymbol = "+"+ subjSymbol = "->"+ equijSymbol = "<->"+ multiJuncTextFrame symb pL = case pL of+ [] -> ["[" ++ symb ++ "]"]+ [p] -> D.textFrameBracket (D.plainMerge (D.normalTextFrameTable+ [[[symb ++ " "], D.textFrame p]]))+ pL -> D.textFrameBracket (D.plainMerge (D.normalTextFrameTable+ [(L.intersperse [" " ++ symb ++ " "] (map D.textFrame pL))]))+ in case form of+ A x -> D.textFrame x+ F -> [falseSymbol]+ T -> [trueSymbol]+ N p -> D.plainMerge (D.normalTextFrameTable [[[negSymbol], D.textFrame p]])+ CJ pL -> multiJuncTextFrame conjSymbol pL+ DJ pL -> multiJuncTextFrame disjSymbol pL+ SJ pL -> multiJuncTextFrame subjSymbol pL+ EJ pL -> multiJuncTextFrame equijSymbol pL++-- parsing formulas on string atoms++ type Parser a = String -> [(a, String)]++ parseProp :: Parser (PropForm String)+ parseProp = parseAtom `plus` parseFalse `plus` parseTrue `plus` parseNeg `plus`+ parseConj `plus` parseDisj `plus` parseSubj `plus` parseEquij+ where+ -- eight functions of type Parser (PropForm String)+ parseAtom = \ inp -> [ (A out',inp') | (out',inp') <- (skipWhite atomToken) inp ]+ parseFalse = \ inp -> [ (F, inp') | (out', inp') <- (skipWhite falseToken) inp ]+ parseTrue = \ inp -> [ (T, inp') | (out', inp') <- (skipWhite trueToken) inp ]+ parseNeg = \ inp -> [ (N out2, inp2) | (out1, inp1) <- (skipWhite negToken) inp,+ (out2, inp2) <- (skipWhite parseProp) inp1 ]+ parseConj = parseJunction CJ conjToken+ parseDisj = parseJunction DJ disjToken+ parseSubj = parseJunction SJ subjToken+ parseEquij = parseJunction EJ equijToken+ -- auxiliary function+ parseJunction :: ([PropForm String] -> PropForm String) -> Parser String -> Parser (PropForm String)+ parseJunction junc token = \ inp ->+ [ (junc [], i3) | (o1,i1) <- (skipWhite leftToken) inp,+ (o2,i2) <- (skipWhite token) i1,+ (o3,i3) <- (skipWhite rightToken) i2 ]+ +++ [ (junc [o3], i4) | (o1,i1) <- (skipWhite leftToken) inp,+ (o2,i2) <- (skipWhite token) i1,+ (o3,i3) <- (skipWhite parseProp) i2,+ (o4,i4) <- (skipWhite rightToken) i3 ]+ +++ [ (junc (o2:o4:o5), i6) | (o1,i1) <- (skipWhite leftToken) inp,+ (o2,i2) <- (skipWhite parseProp) i1,+ (o3,i3) <- (skipWhite token) i2,+ (o4,i4) <- (skipWhite parseProp) i3,+ (o5,i5) <- tokenPropSeq i4,+ (o6,i6) <- (skipWhite rightToken) i5]+ where tokenPropSeq :: Parser [PropForm String]+ tokenPropSeq = \ inp -> case (skipWhite token) inp of+ [] -> [([],inp)]+ [(t,inp')] -> [ (o1:o2, i2) | (o1,i1) <- (skipWhite parseProp) inp',+ (o2,i2) <- (skipWhite tokenPropSeq) i1 ]+ -- the token parser of type Parser String+ atomToken = \ inp -> [ (out',inp') | (out',inp') <- (grab1 isAlphanum) inp,+ out' /= "false", out' /= "true" ]+ leftToken = string "[" :: Parser String+ rightToken = string "]" :: Parser String+ falseToken = string "false" :: Parser String+ trueToken = string "true" :: Parser String+ negToken = string "-" :: Parser String+ conjToken = string "*" :: Parser String+ disjToken = string "+" :: Parser String+ subjToken = string "->" :: Parser String+ equijToken = string "<->" :: Parser String+ -- the parser combinators+ string :: String -> Parser String+ string s = \ inp -> let (s1,s2,s3) = iter (s,inp,[])+ -- iter(s,inp,[]) = (s1,s2,s3) so that+ -- s1++s2=s and s1++s3=inp with s1 of maximal length+ in if null s2+ then [(s1,s3)]+ else []+ where iter ([],y,z) = (reverse z,[],y)+ iter (x,[],z) = (reverse z,x,[])+ iter (x:xL,y:yL,z) = if x == y+ then iter (xL, yL, x:z)+ else (reverse z, x:xL, y:yL)+ grab :: (Char -> Bool) -> Parser String+ grab chf = \ inp -> iter ("",inp)+ where iter (xL, []) = [(reverse xL, [])]+ iter (xL, y:yL) = if chf y+ then iter (y:xL, yL)+ else [(reverse xL, y:yL)]+ grab1 :: (Char -> Bool) -> Parser String+ grab1 chf = \ inp -> filter (\ (x,y) -> not (null x)) (grab chf inp)+ plus :: Parser a -> Parser a -> Parser a+ p `plus` q = \ inp -> (p inp ++ q inp)+ -- some character predicates of type Char -> Bool+ isDigit c = '0' <= c && c <= '9'+ isLower c = 'a' <= c && c <= 'z'+ isUpper c = 'A' <= c && c <= 'Z'+ isLetter c = isLower c || isUpper c+ isAlphanum c = isDigit c || isLetter c+ isWhite c = c == ' ' -- space char+ || c == '\n' -- newline+ || c == '\t' -- horizontal tab+ || c == '\v' -- vertical tab+ || c == '\f' -- form feed+ || c == '\r' -- carriage return+ -- white space+ whiteSpace :: Parser String+ whiteSpace = grab isWhite+ skipWhite :: Parser a -> Parser a+ skipWhite p = \ inp -> [ (out1, inp1) | (out0, inp0) <- whiteSpace inp, (out1, inp1) <- p inp0 ]++ stringToProp :: String -> PropForm String+ stringToProp inp = case parseProp inp of+ [] -> error ("stringToProp -- input is not a proper fancy formula:\n" ++ inp)+ [(form,inp')] -> form+ _ -> error ("stringToProp -- Fatal error! Input doesn't parse unambiguously:\n" ++ inp)+
+ PropLogicTest.hs view
@@ -0,0 +1,855 @@+module PropLogicTest (++ -- * Convenient abbreviations and combinations of often used functions++ -- ** Various prime form generations+ pdnf', pcnf',+ spdnf', spcnf',+ xpdnf', xpcnf',++ -- ** Various prime form generations with combined parsing and display+ pdnf, pcnf,+ spdnf, spcnf,+ xpdnf, xpcnf,++ -- * Random generation++ -- ** Auxiliary random functions (probably obsolete)++ randomListMember,+ -- | For example,+ --+ -- > > randomListMember ['a','b','c','d']+ -- > 'b'+ -- > > randomListMember ['a','b','c','d']+ -- > 'd'+ -- > > randomListMember ['a','b','c','d']+ -- > 'c'++ randomChoice,+ -- | Removes one random member from a given list and returns this member and the remaining list. For example,+ --+ -- > > randomChoice ["a", "b", "c"]+ -- > ("c",["a","b"])+ -- > > randomChoice ["a", "b", "c"]+ -- > ("b",["a","c"])+ -- > > randomChoice ["a", "b", "c"]+ -- > ("a",["b","c"])+ -- > > randomChoice ["a", "b", "c"]+ -- > ("a",["b","c"])++ shuffle,+ -- | For example,+ --+ -- > > shuffle [1,2,3,2,1]+ -- > [2,1,3,1,2]+ -- > > shuffle [1,2,3,2,1]+ -- > [1,2,3,2,1]+ -- > > shuffle [1,2,3,2,1]+ -- > [2,1,2,3,1]+ -- > > shuffle [1,2,3,2,1]+ -- > [2,3,1,1,2]+ -- > > shuffle [1,2,3,2,1]+ -- > [2,1,1,3,2]+ -- > > shuffle [1,2,3,2,1]+ -- > [1,2,1,3,2]++ randomSublist,+ -- | @randomSublist xL@ deletes a random number of members and returns the result. For example,+ --+ -- > > randomSublist [1,2,3,4,5,6,7,7,7,8,8,8]+ -- > [4]+ -- > > randomSublist [1,2,3,4,5,6,7,7,7,8,8,8]+ -- > [3,4]+ -- > > randomSublist [1,2,3,4,5,6,7,7,7,8,8,8]+ -- > [2,3,4,5,6,7,7,7,8,8]+ -- > > randomSublist [1,2,3,4,5,6,7,7,7,8,8,8]+ -- > [1,2,5,7,8]+ -- > > randomSublist [1,2,3,4,5,6,7,7,7,8,8,8]+ -- > [4,5,8,8]+ -- > > randomSublist [1,2,3,4,5,6,7,7,7,8,8,8]+ -- > [1,2,3,5,6,7,7,8,8]++ nRandomRIO,+ -- | @nRandomRIO n (lower,upper)@ returns an list of n random integers between lower and upper.+ -- For example,+ --+ -- > > nRandomRIO 10 (1,3)+ -- > [2,3,3,2,2,3,3,3,3,1]+ -- > > nRandomRIO 10 (1,3)+ -- > [3,2,1,2,2,3,3,1,1,1]+ -- > > nRandomRIO 10 (1,3)+ -- > [1,3,2,1,2,1,2,2,1,2]++ weightedRandomMember,+ -- | @weightedRandomMember@ takes a list @[(x1,n1),...,(xM,nM)]@ of @(a,Int)@ pairs and selects one of the @x1,...,xM@.+ -- The second integer value @ni@ in each pair @(xi,ni)@ represents the relative likelihood for the choice of @xi@ compare to the+ -- other values. In the following example and on the long run, @a@ is chosen 10 times more often than @b@, and @c@ isn't chosen at all.+ --+ -- > > weightedRandomMember [("a",10),("b",1),("c",0)]+ -- > "a"+ -- > > weightedRandomMember [("a",10),("b",1),("c",0)]+ -- > "a"+ -- > > weightedRandomMember [("a",10),("b",1),("c",0)]+ -- > "a"+ -- > > weightedRandomMember [("a",10),("b",1),("c",0)]+ -- > "a"+ -- > > weightedRandomMember [("a",10),("b",1),("c",0)]+ -- > "a"+ -- > > weightedRandomMember [("a",10),("b",1),("c",0)]+ -- > "a"+ -- > > weightedRandomMember [("a",10),("b",1),("c",0)]+ -- > "a"+ -- > > weightedRandomMember [("a",10),("b",1),("c",0)]+ -- > "b"+ -- > > weightedRandomMember [("a",10),("b",1),("c",0)]+ -- > "a"++ appleBasketDistribution,+ -- | @appleBasketDistribution n k@ distributes @n@ apples into @k@ baskets in the sense that the result is a random integer list+ -- of length @k@, where the sum of its components is @n@.+ --+ -- > > appleBasketDistribution 10 4+ -- > [4,2,2,2]+ -- > > appleBasketDistribution 10 4+ -- > [2,2,3,3]+ -- > > appleBasketDistribution 10 4+ -- > [3,2,1,4]+ -- > > appleBasketDistribution 10 4+ -- > [0,7,0,3]++ -- ** Random I-Forms and X-Forms++ averageLineLength,+ randomILine,+ randomIForm,+ randomXForm,++ -- ** Random DNFs and CNFs++ randomDNF,+ randomCNF,+ randomCharDNF, randomCharCNF,+ randomIntDNF, randomIntCNF,++ -- ** Random propositional formulas in general++ -- *** Size parameter++ SizeTriple,++ sizeTriple,++ -- *** Random formulas++ JunctorSymbol(..),++ JunctorWeighting,++ defaultJunctorWeighting,++ weightedRandomPropForm,++ randomPropForm,+ -- | @randomPropForm aL (aSize,jSize)@ returns a randomly generated propositional formula @p@ such that+ --+ -- > atoms p == aL+ -- > atomSize p == aSize+ -- > juncSize p == jSize+ --+ -- If @atomSize@ is smaller than the length of @aL@, an error message is returned. For example,+ --+ -- > > randomPropForm ["x", "y"] (3,3)+ -- > EJ [A "y",T,A "y",A "x",DJ []]+ -- > > randomPropForm ["x", "y"] (3,3)+ -- > EJ [SJ [A "y",A "y"],DJ [A "x"]]+ -- > > randomPropForm ["x", "y"] (3,3)+ -- > EJ [EJ [],A "x",CJ [A "y"],A "x"]+ -- > > randomPropForm ['x','y','z'] (1,1)+ -- > *** Exception: randomPropForm -- atom size smaller than ordered atom list++ randomCharProp,+ -- | @randomCharProp (aCard,aSize,jSize)@ is @randomPropForm aL (aSize,jSize)@, where @aL@ is the ordered list of the first @aCard@+ -- small characters @'a', 'b', 'c', ...@. If the atom cardinality is undefined, i.e. if not @0<=aCard<=26@, or if it exceeds @aSize@,+ -- an error message is returned.+ -- For example,+ --+ -- > > randomCharProp (3,5,5)+ -- > SJ [A 'c',EJ [A 'a',A 'c'],F,T,DJ [A 'b'],A 'c']+ -- > > randomCharProp (3,5,5)+ -- > SJ [A 'a',A 'c',DJ [T,CJ [A 'b',A 'a',A 'b'],T]]+ -- > > randomCharProp (3,5,5)+ -- > DJ [F,A 'b',SJ [F],A 'c',DJ [A 'a'],A 'c',A 'a']++ randomIntProp,++ -- * Testing++ -- ** Testing a propositional algebra++ -- *** Axioms of propositional algebras+ axiom_reflexivity_of_subvalence,+ axiom_transitivity_of_subvalence,+ axiom_criterion_for_equivalence,+ -- | CONTINUEHERE ..............................................................!!++ -- *** The summarized test function for a propositional algebra+ test_prop_alg,++ -- ** Tests for "DefaultPropLogic"++ -- *** Testing the normalizations++ -- | ...continuehere...............................++ -- *** Testing the default propositional algebras++ -- ** Tests for "FastPropLogic"++ -- *** Testing of the M- and P-procedure+ -- | continuehere ............................++ -- *** Correctness of the Prime Normal Form constructions+ -- | continuehere ...........................++ -- ** Test for the total package+ total_test,++ -- * Profiling - first version++ -- ** Measures++ Msec,+ CanonPerformance,+ Verbose,++ -- ** correctness tests (move these correctness tests)--!!!!!!!!!!1++ pnfCorrect,+ pnfCorrectRepeat,++ -- ** performance tests++ pnfPerform,+ pnfPerformRandom,+ pnfPerformRepeat,++ -- * Profiling - second version+ Seconds,+ verboseRandomPrimeTest,+ verboseRandomPrimeTesting,+ meanValue,+ standDeviation,+ normSeconds,++) where ---------------------------------------------------------------------------------------------------------------++ import Char (chr)+ import Ratio+ import Random (randomIO, randomRIO)+ import Control.Monad+ import CPUTime (getCPUTime)+ import qualified Time as T+ import qualified Olist as O+ import qualified TextDisplay as D+ import qualified Costack as C+ import PropLogicCore+ import DefaultPropLogic+ import FastPropLogic++-- convenient abbreviations++ pdnf' :: Ord a => PropForm a -> PDNF a+ pdnf' = fromXPDNF . toXPDNF++ pcnf' :: Ord a => PropForm a -> PCNF a+ pcnf' = fromXPCNF . toXPCNF++ spdnf' :: Ord a => PropForm a -> SimpleDNF a+ spdnf' = simpleDNF . pdnf'++ spcnf' :: Ord a => PropForm a -> SimpleCNF a+ spcnf' = simpleCNF . pcnf'++ xpdnf' :: Ord a => PropForm a -> XPDNF a -- this should go to the FastPropLogic module!!!!!!!!!!!!!!!!+ xpdnf' = toXPDNF++ xpcnf' :: Ord a => PropForm a -> XPCNF a -- this should go to the FastPropLogic module!!!!!!!!!!!!!!!!+ xpcnf' = toXPCNF++ pdnf :: String -> IO ()+ pdnf = D.display . pdnf' . stringToProp++ pcnf :: String -> IO ()+ pcnf = D.display . pcnf' . stringToProp++ spdnf :: String -> IO ()+ spdnf = D.display . spdnf' . stringToProp++ spcnf :: String -> IO ()+ spcnf = D.display . spcnf' . stringToProp++ xpdnf :: String -> IO ()+ xpdnf = D.display . xpdnf' . stringToProp++ xpcnf :: String -> IO ()+ xpcnf = D.display . xpcnf' . stringToProp++-- auxiliary random functions++ randomListMember :: [a] -> IO a+ randomListMember xL = do i <- randomRIO (0, length xL - 1)+ return (xL !! i)++ randomChoice :: [a] -> IO (a, [a])+ randomChoice [] = error "randomChoice -- empty list"+ randomChoice xL = do i <- randomRIO (0, length xL -1)+ let (yL, z:zL) = splitAt i xL+ return (z, yL ++ zL)++ nRandomListMember :: Int -> [a] -> IO [a]+ nRandomListMember n xL = mapM randomListMember (replicate n xL)++ randomInsert :: a -> [a] -> IO [a]+ randomInsert x xL = do i <- randomRIO (0, length xL)+ let (yL,zL) = splitAt i xL+ return (yL ++ [x] ++ zL)++ shuffle :: [a] -> IO [a]+ shuffle xL = if null xL+ then return []+ else do (y,yL) <- randomChoice xL+ zL <- shuffle yL+ return (y:zL)++ randomSublist :: [a] -> IO [a]+ randomSublist xL = do let n = length xL -1+ k <- randomRIO (0, n)+ iL <- shuffle [1..n]+ let jL = O.olist (take k iL)+ let yL = filtering xL jL 1+ return yL+ where filtering xL [] _ = []+ filtering (x:xL) (j:jL) i = if j == i+ then x : (filtering xL jL (i + 1))+ else filtering xL (j:jL) (i + 1)++ nRandomRIO :: Int -> (Int,Int) -> IO [Int]+ nRandomRIO n (lower,upper) = sequence (replicate n (randomRIO (lower,upper)))++ weightedRandomMember :: [(a,Int)] -> IO a+ weightedRandomMember pairL = do i <- randomRIO (1, sum (map snd pairL))+ return (select pairL i)+ where select ((x,k):pL) i = if i <= k+ then x+ else select pL (i - k)++ appleBasketDistribution :: Int -> Int -> IO [Int]+ appleBasketDistribution apples baskets =+ if apples < 0 || baskets < 0+ then error "appleBasketDistribution -- negative arguments"+ else if baskets == 0+ then if apples == 0+ then return []+ else error "appleBasketDistribution -- zero baskets"+ else do basketIndexList <- nRandomRIO apples (0, baskets - 1)+ return (map (\ i -> count i basketIndexList) (Prelude.take baskets (enumFrom 0)))+ where count x yL = length (filter (\ y -> y == x) yL)++-- random I-Forms and X-Forms++ averageLineLength :: IForm -> Float+ averageLineLength iform = (fromIntegral (truncate ((v / l) * 100))) / 100+ where v = fromIntegral (volume iform) :: Float+ l = fromIntegral (C.length iform) :: Float++ randomILine :: Int -> Int -> IO ILine+ randomILine atomNum averLen =+ do intLL <- mapM singleAtom [1..atomNum]+ let intL = concat intLL+ return (iLine intL)+ where singleAtom :: IAtom -> IO [ILit]+ singleAtom atom = do i <- randomRIO (1, atomNum)+ b <- randomIO :: IO Bool+ let lit = if i <= averLen+ then if b then [atom] else [negLit atom]+ else []+ return lit++ randomIForm :: Int -> Int -> Int -> IO IForm++-- randomIForm atomNum formLen averLineLen =+-- do lineL <- sequence (replicate formLen (randomILine atomNum averLineLen))+-- return (C.fromList lineL)++ randomIForm atomNum formLen averLineLen+ | atomNum < 0 = error "randomIForm -- negative number of atoms"+ | formLen < 0 = error "randomIForm -- negative I-Form length"+ | averLineLen < 0 = error "randomIForm -- negative average I-Line length"+ | atomNum < averLineLen = error "randomIForm -- atom number smaller than average I-Line length"+ | otherwise = do lineL <- sequence (replicate formLen (randomILine atomNum averLineLen))+ return (C.fromList lineL)++ randomXForm :: Ord a => [a] -> Int -> Int -> IO (XForm a)+ randomXForm atomL formLen averLineLen =+ do let ordAtomL = O.olist atomL+ let atomNum = length ordAtomL+ iform <- randomIForm atomNum formLen averLineLen+ return (ordAtomL, iform)++-- random DNFs and CNFs++ randomDNF :: Ord a => [a] -> Int -> Int -> IO (DNF a)+ randomDNF atomL formLen averLineLen = do xform <- randomXForm atomL formLen averLineLen+ return (xDNF xform)++ randomCNF :: Ord a => [a] -> Int -> Int -> IO (CNF a)+ randomCNF atomL formLen averLineLen = do xform <- randomXForm atomL formLen averLineLen+ return (xCNF xform)++ randomCharDNF :: Int -> IO (DNF Char)+ randomCharDNF atomNum = randomDNF (take atomNum ['a'..'z']) (2 * atomNum) atomNum++ randomCharCNF :: Int -> IO (CNF Char)+ randomCharCNF atomNum = randomCNF (take atomNum ['a'..'z']) (2 * atomNum) atomNum++ randomIntDNF :: Int -> IO (DNF Int)+ randomIntDNF atomNum = randomDNF (take atomNum [1..]) (2 * atomNum) atomNum++ randomIntCNF :: Int -> IO (CNF Int)+ randomIntCNF atomNum = randomCNF (take atomNum [1..]) (2 * atomNum) atomNum++-- size parameters++ type SizeTriple = (Int,Int,Int) -- = (length atoms, atomSize, juncSize)++ sizeTriple :: Ord a => PropForm a -> SizeTriple+ sizeTriple p = (Prelude.length (atoms p), atomSize p, juncSize p)++-- random formula generation with weighted junctors++ data JunctorSymbol = T_ | F_ | N_ | CJ_ | DJ_ | SJ_ | EJ_+ deriving (Eq, Ord, Show, Read)++ type JunctorWeighting = [(JunctorSymbol, Int)]++ defaultJunctorWeighting :: JunctorWeighting+ defaultJunctorWeighting = [(N_,15), (F_,1), (T_,1), (CJ_,5), (DJ_,5), (SJ_,1), (EJ_,1)]++ weightedRandomPropForm :: JunctorWeighting -> O.Olist a -> (Int, Int) -> IO (PropForm a)+ weightedRandomPropForm weighting ordAtomL (aSize,jSize)+ | aSize < 0 || jSize < 0 = error "weightedRandomPropForm -- negative size"+ | aSize == 0 && jSize == 0 = error "weightedRandomPropForm -- zero atom and junctor size"+ | aSize > 0 && length ordAtomL == 0 = error "weightedRandomPropForm -- no atoms available"+ | aSize < length ordAtomL = error "weightedRandomPropForm -- atom size smaller than ordered atom list"+ | otherwise = do aL <- nRandomListMember (aSize - (length ordAtomL)) ordAtomL+ aL <- shuffle (aL ++ ordAtomL)+ p <- iter jSize (map A aL)+ return p+ where iter :: Int -> [PropForm a] -> IO (PropForm a)+ iter jSize pL | jSize == 0 = if length pL == 1+ then return (head pL)+ else error "weightedRandomPropForm -- junctor size"+ | jSize == 1 = do x <- if length pL == 0+ then randomJunc [CJ_, DJ_, SJ_, EJ_, F_, T_]+ else randomJunc [CJ_, DJ_, SJ_, EJ_]+ p <- case x of+ F_ -> return F+ T_ -> return T+ CJ_ -> return (CJ pL)+ DJ_ -> return (DJ pL)+ SJ_ -> return (SJ pL)+ EJ_ -> return (EJ pL)+ return p+ | jSize >= 2 = do x <- if length pL == 0+ then randomJunc [F_, T_, CJ_, DJ_, SJ_, EJ_]+ else randomJunc [F_, T_, CJ_, DJ_, SJ_, EJ_, N_]+ qL <- case x of+ F_ -> do let pL' = F : pL+ pL'' <- shuffle pL'+ return pL'+ T_ -> do let pL' = T : pL+ pL'' <- shuffle pL'+ return pL'+ N_ -> do (p',pL') <- randomChoice pL+ pL'' <- shuffle ((N p') : pL')+ return pL''+ _ -> do i <- randomRIO (0, length pL - 1)+ let (pL1, pL2) = splitAt i pL+ let q = case x of+ CJ_ -> (CJ pL1)+ DJ_ -> (DJ pL1)+ SJ_ -> (SJ pL1)+ EJ_ -> (EJ pL1)+ pL' <- shuffle (q : pL2)+ return pL'+ p <- iter (jSize - 1) qL+ return p+ randomJunc :: [JunctorSymbol] -> IO JunctorSymbol+ randomJunc selection = weightedRandomMember (select selection weighting)+ where select [] _ = []+ select (x:xL) pL = (select1 x pL) : (select xL pL)+ select1 x ((y,n):pL) = if x == y+ then (y,n)+ else select1 x pL++ randomPropForm :: O.Olist a -> (Int,Int) -> IO (PropForm a)+ randomPropForm ordAtomL (aSize,jSize)+ | aSize < 0 || jSize < 0 = error "randomPropForm -- negative size"+ | aSize == 0 && jSize == 0 = error "randomPropForm -- zero atom and junctor size"+ | aSize > 0 && length ordAtomL == 0 = error "randomPropForm -- no atoms available"+ | aSize < length ordAtomL = error "randomPropForm -- atom size smaller than ordered atom list"+ | otherwise = do aL <- nRandomListMember (aSize - (length ordAtomL)) ordAtomL+ aL <- shuffle (aL ++ ordAtomL)+ p <- weightedRandomPropForm defaultJunctorWeighting aL (aSize,jSize)+ return p++ randomCharProp :: SizeTriple -> IO (PropForm Char)+ randomCharProp (aCard,aSize,jSize) =+ if aCard < 0 || aCard > 26+ then error ("randomCharProp -- " ++ (show aCard) ++ " exceeds the number of available 26 characters")+ else do let aL = take aCard charList+ p <- randomPropForm aL (aSize,jSize)+ return p+ where charList = map chr [97..122] -- all small characters 'a', ..., 'z'++ randomIntProp :: SizeTriple -> IO (PropForm Int)+ randomIntProp (aCard,aSize,jSize) = do let aL = Prelude.take aCard [1..]+ p <- randomPropForm aL (aSize,jSize)+ return p++-- axioms of propositional algebras++ -- the conversion axioms++{--+ axiom_atom_conversion :: PropAlg a p => a -> Bool+ axiom_atom_conversion a = undefined++ -- ambiguous constraint error: -----!!!!!!!!!!!!!+ -- axiom_zero_conversion :: PropAlg a p => Bool+ -- axiom_zero_conversion = fromPropForm F `biequivalent` false++ -- ambiguous constraint error: -----!!!!!!!!!!!!!+ -- axiom_unit_conversion :: PropAlg a p => Bool+ -- axiom_unit_conversion = fromPropForm T `biequivalent` true++ axiom_neg_conversion :: PropAlg a p => PropForm a -> Bool+ axiom_neg_conversion p = fromPropForm (N p) `biequivalent` neg (fromPropForm p)++ ...............etc......................+-}++ -- semantic axioms++ axiom_reflexivity_of_subvalence :: PropAlg a p => p -> Bool+ axiom_reflexivity_of_subvalence p = p `subvalent` p++ axiom_transitivity_of_subvalence :: PropAlg a p => (p,p,p) -> Bool+ axiom_transitivity_of_subvalence (p1,p2,p3) = ((p1 `subvalent` p2) && (p2 `subvalent` p3)) `subvalent` (p1 `subvalent` p3)++ axiom_criterion_for_equivalence :: PropAlg a p => (p,p) -> Bool+ axiom_criterion_for_equivalence (p1,p2) = (p1 `equivalent` p2) `equivalent` ((p1 `subvalent` p2) && (p2 `subvalent` p1))++ axiom_least_element :: PropAlg a p => p -> Bool+ axiom_least_element p = false `subvalent` p++ axiom_greatest_element :: PropAlg a p => p -> Bool+ axiom_greatest_element p = p `subvalent` true++ axiom_neutral_disjunction_element :: PropAlg a p => p -> Bool+ axiom_neutral_disjunction_element p = disj [false, p] `equivalent` p++ axiom_neutral_conjunction_element :: PropAlg a p => p -> Bool+ axiom_neutral_conjunction_element p = conj [true, p] `equivalent` p++ axiom_conjunctive_complement :: PropAlg a p => p -> Bool+ axiom_conjunctive_complement p = conj [p, neg p] `equivalent` false++ axiom_disjunctive_complement :: PropAlg a p => p -> Bool+ axiom_disjunctive_complement p = disj [p, neg p] `equivalent` true++ axiom_conjunctive_idempotency :: PropAlg a p => p -> Bool+ axiom_conjunctive_idempotency p = conj [p, p] `equivalent` p++ axiom_disjunctive_idempotency :: PropAlg a p => p -> Bool+ axiom_disjunctive_idempotency p = disj [p, p] `equivalent` p++ -- CONTINUEHERE ----------------!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!++-- test functions for propositional algebras++ test_prop_alg :: (Show a, Show p, PropAlg a p) => IO a -> IO p -> Int -> IO ()+ test_prop_alg randAtom randProp number =+ do -- generation of random arguments+ atomL <- replicateM number randAtom+ propL <- replicateM number randProp+ propL' <- replicateM number randProp+ propL'' <- replicateM number randProp+ let propPairL = zip propL propL'+ let propTripleL = zip3 propL propL' propL''+ -- test the single axioms+ test_axiom "reflexivity of the subvalence relation" axiom_reflexivity_of_subvalence propL+ test_axiom "transitivity of the subvalence relation" axiom_transitivity_of_subvalence propTripleL+ test_axiom "criterion for equivalence" axiom_criterion_for_equivalence propPairL+ -- CONTINUEHERE ...........................+ -- finish+ print "Test for propositional algebra finished successfully."+ where test_axiom :: Show a => String -> (a -> Bool) -> [a] -> IO ()+ test_axiom name axiom [] = print ("test for " ++ name ++ " passed " ++ show number ++ " times")+ test_axiom name axiom (arg:argL) = if axiom arg+ then test_axiom name axiom argL+ else error (name ++ " doesn't hold for " ++ "\n" ++ show arg)++-- test for the total package++ total_test :: Int -> IO ()+ total_test = undefined++-- measures and test parameters++ type Msec = Integer -- milliseconds++ timeDiffToMsec :: T.TimeDiff -> Msec+ timeDiffToMsec td =+ if T.tdMonth td /= 0 || T.tdYear td /= 0+ then error "timeDiffToMsec -- cannot deal with non-zero months or years"+ else (div (T.tdPicosec td) 1000000000) ++ (toInteger (T.tdSec td) * 1000) ++ (toInteger (T.tdMin td) * 1000 * 60) ++ (toInteger (T.tdHour td) * 1000 * 60 * 60) ++ (toInteger (T.tdDay td) * 1000 * 60 * 60 * 24)++ diffTimes :: T.ClockTime -> T.ClockTime -> Msec+ diffTimes t1 t2 = timeDiffToMsec (T.diffClockTimes t1 t2)++ type CanonPerformance = (SizeTriple,(Msec,SizeTriple),(Msec,SizeTriple)) -- (pre-size, (D-time, D-size), (C-time, C-size))++ type Verbose = Bool -- set True means that the according function produces additional information while in progress++-- correctness tests++ pnfCorrect :: (D.Display a, Show a, Ord a) => Verbose -> PropForm a -> IO (Either (PropForm a) CanonPerformance)+ pnfCorrect verb p =+ do return (ifVerbose (do { print "The input formula:" ; D.display p }))+ t1 <- T.getClockTime+ let fastPdnf = pdnf' $! p+ t2 <- T.getClockTime+ let fastPdnfTime = diffTimes t2 t1+ return (ifVerbose (do { print ("The fast PDNF (computed in " ++ (show fastPdnfTime) ++ " milliseconds):") ; D.display fastPdnf }))+ t1 <- T.getClockTime+ let defaultPdnf = primeDNF $! p+ t2 <- T.getClockTime+ let defaultPdnfTime = diffTimes t2 t1+ return (ifVerbose (do { print ("The default PDNF (computed in " ++ (show defaultPdnfTime) ++ " milliseconds):") ; D.display defaultPdnf }))+ t1 <- T.getClockTime+ let fastPcnf = pcnf' $! p+ t2 <- T.getClockTime+ let fastPcnfTime = diffTimes t2 t1+ return (ifVerbose (do { print ("The fast PCNF (computed in " ++ (show fastPcnfTime) ++ " milliseconds):") ; D.display fastPcnf }))+ t1 <- T.getClockTime+ let defaultPcnf = primeCNF $! p+ t2 <- T.getClockTime+ let defaultPcnfTime = diffTimes t2 t1+ return (ifVerbose (do { print ("The default PCNF (computed in " ++ (show defaultPcnfTime) ++ " milliseconds):") ; D.display defaultPcnf }))+ let result = if defaultPdnf == fastPdnf && defaultPcnf == fastPcnf+ then Right (sizeTriple p, (fastPdnfTime, sizeTriple fastPdnf), (fastPcnfTime, sizeTriple fastPcnf))+ else Left p+ return (ifVerbose (do { print "The overall result is:" ; print result }))+ return result+ where ifVerbose act = if verb then act else (putStr "")++ pnfCorrectRepeat :: Verbose -> (Int, Int, Int) -> IO (PropForm Char)+ pnfCorrectRepeat verb (aCard, aSize, jSize) =+ do p <- randomCharProp (aCard, aSize, jSize)+ r <- pnfCorrect verb p+ q <- case r of+ Left p' -> return p'+ Right _ -> do print r+ pnfCorrectRepeat verb (aCard, aSize, jSize)+ return q++-- performance tests++ pnfPerform :: (D.Display a, Show a, Ord a) => PropForm a -> IO CanonPerformance+ pnfPerform p =+ do let formSize = sizeTriple p+ t1 <- T.getClockTime+ let pdnfForm = pdnf' $! p+ let pdnfSize = sizeTriple $! pdnfForm+ t2 <- T.getClockTime+ let pdnfTime = diffTimes t2 t1+ t1 <- T.getClockTime+ let pcnfForm = pcnf' $! p+ let pcnfSize = sizeTriple $! pcnfForm+ t2 <- T.getClockTime+ let pcnfTime = diffTimes t2 t1+ return (formSize, (pdnfTime, pdnfSize), (pcnfTime, pcnfSize))++ pnfPerformRandom :: SizeTriple -> IO CanonPerformance+ pnfPerformRandom (aCard, aSize, jSize) =+ do p <- randomIntProp (aCard, aSize, jSize)+ r <- pnfPerform p+ return r++ pnfPerformRepeat :: SizeTriple -> IO ()+ pnfPerformRepeat st = do cp <- pnfPerformRandom st+ print cp+ x <- pnfPerformRepeat st+ return x++---------------------------------------------------------------------------------------------------+-- new stuff ----------- move this into the right places ------------------------------------------+---------------------------------------------------------------------------------------------------++ onePrimFormTest :: IForm -> ()+ onePrimFormTest iform = let q = primForm iform+ b1 = primeDNF (iDNF iform) == iDNF q+ b2 = primeCNF (iCNF iform) == iCNF q+ in if b1 && b2+ then ()+ else error ("onePrimFormTest dicovered an error for \n" ++ (show iform))++ primFormTesting :: Int -> Int -> Int -> IO ()+ primFormTesting atomNumber formLength averLineLen=+ do iform <- randomIForm atomNumber formLength averLineLen+ let b = onePrimFormTest iform+ putStr "."+ t <- primFormTesting atomNumber formLength averLineLen+ return t++ randomPrimForms :: Int -> Int -> Int -> IO ()+ randomPrimForms atomNumber formLen averLineLen =+ do iform <- randomIForm atomNumber formLen averLineLen+ let p = primForm iform+ let q = primForm iform+ putStr (show (formLength iform) ++ ":" ++ show (formLength p) ++ ":" ++ show (formLength q) ++ " ")+ t <- randomPrimForms atomNumber formLen averLineLen+ return t++ xprimTest :: ILine -> ILine -> Bool+ xprimTest line1 line2 = (xprim line1 line2) == (xprim' line1 line2)++ pairPrimTest :: ILine -> ILine -> Bool+ pairPrimTest line1 line2 = (pdnf == iDNF iform) && (pcnf == iCNF iform)+ where pdnf = primeDNF (DJ [iNLC line1, iNLC line2])+ pcnf = primeCNF (CJ [iNLD line1, iNLD line2])+ iform = orderForm (pairPrim line1 line2)++ xprimTesting :: Int -> Int -> IO ()+ xprimTesting atomNumber averLen =+ do line1 <- randomILine atomNumber averLen+ line2 <- randomILine atomNumber averLen+ let b = xprimTest line1 line2+ let s = if b then "." else error ("xprim and xprim' produce different results for "+ ++ (show line1) ++ " and " ++ (show line2))+ putStr s+ let b = pairPrimTest line1 line2+ let s = if b then "." else error ("pairPrim and primeDNF or primeCNF produce different PNFs for"+ ++ (show line1) ++ " and " ++ (show line2))+ putStr s+ t <- xprimTesting atomNumber averLen+ return t++ m2formTesting :: Int -> Int -> Int -> IO ()+ m2formTesting atomNumber formLen averLineLen =+ do iform <- randomIForm atomNumber formLen averLineLen+ let m = m2form iform+ putStr (show (formLength iform) ++ ":" ++ show (formLength m) ++ " ")+ t <- m2formTesting atomNumber formLen averLineLen+ return t++ verbosePProcedure :: IForm -> IO ()+ verbosePProcedure iform = iter iform 0+ where iter iform step = do putStrLn ("step: " ++ (show step) +++ "; atoms: " ++ (show (length (formIndices iform))) +++ "; length: " ++ (show (formLength iform)) +++ "; volume: " ++ (show (volume iform)) +++ ": averageLineLength: " ++ (show (averageLineLength iform)))+ let mform1 = m2form iform+ let mform2 = orderForm mform1+ r <- if mform2 == iform+ then putStrLn "DONE"+ else iter mform2 (step + 1)+ return r++ pProcedureTesting :: Int -> Int -> Int -> IO ()+ pProcedureTesting atomNumber formLen averLineLen =+ do p <- randomIForm atomNumber formLen averLineLen+ verbosePProcedure p+ t <- pProcedureTesting atomNumber formLen averLineLen+ return t++-- Profiling - second version++-- testing the prime generation of IForms with random input IForms++ type Seconds = Double++ verboseRandomPrimeTest :: (Int,Int,Int) -> IO (Int,Int,Int,Seconds)+ -- ^ @randomPrimeTest (atomNum, formLen, averLineLen) = (atomNum', formLen', vol', secs')@+ verboseRandomPrimeTest (atomNum, formLen, averLineLen) =+ do iform <- randomIForm atomNum formLen averLineLen+ putStrLn "*** The random IForm is: ***"+ print iform+ putStrLn "*** Its prime IForm is: ***"+ t1 <- getCPUTime+ let pform = primForm $! iform+ print pform+ t2 <- getCPUTime+ putStrLn "*** Result of this test ***"+ putStr "Properties of the random IForm: "+ iformDiagnosis iform+ putStr "Properties of its prime IForm: "+ iformDiagnosis pform+ let t = (fromIntegral (t2 - t1)) / 1000000000000 :: Seconds+ putStrLn ("Time to produce the prime IForm: " ++ (show t) ++ " seconds.")+ return (length (formIndices pform), formLength pform, volume pform, t)+ where iformDiagnosis :: IForm -> IO ()+ iformDiagnosis iform = putStrLn ( "atomNumber = " ++ (show (length (formIndices iform))) +++ "; formLength = " ++ (show (formLength iform)) +++ "; volume = " ++ (show (volume iform)) +++ "; averageLineLength = " ++ (show (averageLineLength iform)) )++ verboseRandomPrimeTesting :: (Int,Int,Int) -> Int -> IO (Int,Int,Seconds,Seconds,Seconds)+ -- ^ @verboseRandomPrimeTesting (atomNum, formLen, averLineLen) numberOfTests = (maxFormLen, averFormLen, maxTime, averTime, standDev)@+ verboseRandomPrimeTesting (atomNum, formLen, averLineLen) numberOfTests = iter [] numberOfTests+ where iter :: [(Int,Int,Int,Seconds)] -> Int -> IO (Int,Int,Seconds,Seconds,Seconds)+ iter qL n | n == 0 = do let (maxFormLen, averFormLen, maxTime, averTime, standDev) = evaluate qL+ D.printTextFrame $ D.textFrameBox $ D.correctTextFrame+ [ "All " ++ (show numberOfTests) ++ " tests have been performed: ",+ " Parameters for the random IForms were:",+ " atomNumber = " ++ (show atomNum),+ " formLength = " ++ (show formLen),+ " averageLineLength = " ++ (show averLineLen),+ " Result of the test series:",+ " numberOfTests = " ++ (show numberOfTests),+ " maxFormLength = " ++ (show maxFormLen),+ " averageFormLength = " ++ (show averFormLen),+ " maxTime = " ++ (show maxTime) ++ " seconds",+ " averageTime = " ++ (show averTime) ++ " seconds",+ " standardTimeDeviation = " ++ (show standDev) ++ " seconds" ]+ return (maxFormLen, averFormLen, maxTime, averTime, standDev)+ | otherwise = do putStrLn ("*** Test number " ++ (show (numberOfTests - n + 1)) +++ " of " ++ (show numberOfTests) ++ ": ***")+ q <- verboseRandomPrimeTest (atomNum, formLen, averLineLen)+ iter (q:qL) (n - 1)+ evaluate :: [(Int,Int,Int,Seconds)] -> (Int,Int,Seconds,Seconds,Seconds)+ evaluate qL = let (formLenL, timeL) = unzip (map (\ (atomNum, formLen, vol, secs) -> (formLen, secs)) qL)+ in ( maximum formLenL,+ (sum formLenL) `div` (length formLenL),+ maximum timeL,+ meanValue timeL,+ standDeviation timeL )++ meanValue :: [Seconds] -> Seconds+ meanValue timeL = (sum timeL) / (fromIntegral (length timeL))++ standDeviation :: [Seconds] -> Seconds+ standDeviation timeL = sqrt ( (sum (map (\ t -> (t - m)^2) timeL)) / (fromIntegral (length timeL)) )+ where m = meanValue timeL++ normSeconds :: Seconds -> Seconds+ normSeconds s = (fromIntegral (round (s * 1000))) / 1000++
+ Setup.lhs view
@@ -0,0 +1,5 @@+#!/usr/local/bin/runhaskell++> module Main where+> import Distribution.Simple (defaultMain)+> main = defaultMain
+ TextDisplay.hs view
@@ -0,0 +1,338 @@+{-# LANGUAGE FlexibleInstances, TypeSynonymInstances #-}++{- |+ The default representation of any type is the string and the @show@ function, which returns a string for each element+ of an instance of the @Show@ class. But sometimes, it is more intuitive, if a type is represented by a more+ three-dimensional layout. For that matter, we not only have a @show@ function for many types to come, but also a+ @textFrame@ converter, where a @TextFrame@ is basically defined as a list of strings of equal length.+ Similar to the @Show@ type class, we also define a @Display@ type class.+-}++module TextDisplay (++ -- * Text frames++ TextFrame,+ -- | A TextFrame is a list of strings. But for a /correct/ TextFrame, there are more constraints that have to hold:+ -- 1. The strings must all be of equal length.+ -- 2. There must be no white space characters in a string, other than the space character ' '.++ isNonSpaceWhite,+ -- | True if the character is any white space character, except the space character itself.++ findTextFrameError,+ -- | A TextFrame is /correct/ iff all its strings are of equal length and (isNonSpaceWhite ch) is false for all characters ch.++ correctTextFrame,+ -- | Turns the argument string list into a correct version by adding spaces. But returns an error in case any string contains a character ch with (isNonSpaceWhite ch).+ -- IMPROVE the String instance of Display: new line characters should create new lines in the text frame and what about tabs etc? !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!++ width,+ -- | The width of a TextFrame [str1,...,strN] is the maximal length of the strings str1,...,strN.+ -- In particular,+ --+ -- > (width []) == 0 (width [""]) == 0+ --++ height,+ -- | The height of a TextFrame [str1,...,strN] is N.++ printTextFrame,+ -- | prints its TextFrame argument.++ textFrameBox,+ -- | surrounds the text frame with a solid line++ textFrameBracket,+ -- | surrounds the text frame with a square bracket++ defaultTextFrame,+ -- | @(defaultTextFrame x) == [show x]@++ -- * The @Display@ type class+ Display(..),+ -- | @textFrame@ converts into a @TextFrame@.+ -- @display@ prints the text frame (actually, @display = printTextFrame . textFrame@, i.e. to define an instance of @Display@,+ -- Actually, when an instance of @Display@ is defined, only @textFrame@ needs to be specified.+++ -- * Text frame tables+ TextFrameTable,+ -- | A @TextFrameTable@ is a list of rows, where each cell is a @TextFrame@. For example,+ --+ -- > [[["aaa","aaa"],["b","b","b"]],+ -- > [["cccccccc","cccccccc"],["ddddddddd","ddddddddd","ddddddddd"],["eeeee","eeeee","eeeee","eeeee"]],+ -- > [["ff","ff"],[],["ggg","ggg","ggg","ggg"]]]+ --+ -- or, more intuitively in table layout+ --+ -- > "aaa" "b"+ -- > "aaa" "b"+ -- > "b"+ -- >+ -- > "cccccccc" "ddddddddd" "eeeee"+ -- > "cccccccc" "ddddddddd" "eeeee"+ -- > "ddddddddd" "eeeee"+ -- > "eeeee"+ -- >+ -- > "ff" "ggg"+ -- > "ff" "ggg"+ -- > "ggg"+ -- > "ggg"+ --+ columnWidthList,+ rowHeightList,+ -- | Column widths and row heights for the previous example text frame table @tft@ are given by+ --+ -- > (columnWidthList tft) == [8,9,5]+ -- > (rowHeightList tft) == [3,4,4]+ --+ correctTextFrameTable,+ -- | A @TextFrameTable@ is said to be /correct/, if+ -- (1) each row has the same amount of cells,+ -- (2) there is no column of zero width,+ -- (3) there is no row of zero height.+ -- With @correctTextFrameTable@ we remove these flaws.+ --+ bottomAlign, topAlign, centerAlign,+ leftAlign, rightAlign, middleAlign,+ -- | A @TextFrameTable@ is said to be /normal/, if it is correct and each of its @TextFrame@ cells has the width of its according column+ -- and the height of its row.+ -- To convert a text frame table into a normal one, we need to perform two steps (in arbitrary order):+ --+ -- * A row normalization, which makes all text frame cells in one row of equal height. We use three modes to achieve that:+ -- @bottomAlign@, @topAlign@ and @centerAlign@.+ --+ -- * A column normalization, which makes all text frame cells in one column of equal width. Again, we have three functions to do that:+ -- @leftAlign@, @rightAlign@, and @middleAlign@.+ --+ -- For example, given the correct text frame table @tft@, we obtain (we use @_@ for space characters):+ --+ -- > tft = leftAlign tft = middleAlign (leftAlign tft) =+ -- >+ -- > "aaa" "b" "" "aaa ____" "b________" "_____" "aaa_____" "b________" "_____"+ -- > "aaa" "b" "aaa_____" "b________" "aaa_____" "b________" "_____"+ -- > "b" "b________" "________" "b________" "_____"+ -- >+ -- > "cccccccc" "ddddddddd" "eeeee" "cccccccc" "ddddddddd" "eeeee" "________" "ddddddddd" "eeeee"+ -- > "cccccccc" "ddddddddd" "eeeee" "cccccccc" "ddddddddd" "eeeee" "cccccccc" "ddddddddd" "eeeee"+ -- > "ddddddddd" "eeeee" "ddddddddd" "eeeee" "cccccccc" "ddddddddd" "eeeee"+ -- > "eeeee" "eeeee" "________" "_________" "eeeee"+ -- >+ -- > "ff" "ggg" "ff______" "_________" "ggg__" "________" "_________" "ggg__"+ -- > "ff" "ggg" "ff______" "ggg__" "ff______" "_________" "ggg__"+ -- > "ggg" "ggg__" "ff______" "_________" "ggg__"+ -- > "ggg" "ggg__" "________" "_________" "ggg__"+ --+ --+ normalTextFrameTable,+ -- | The default way to convert any text frame table into a normal one is defined by the @normalTextFrameTable@ function,+ -- which is defined by+ --+ -- > normalTextFrameTable = middleAlign . centerAlign . correctTextFrameTable+ --+ plainMerge, gridMerge,+ -- | There is a @plainMerge@ and a @gridMerge@ to turn a normal text frame table into a single text frame. For the example,+ --+ -- > tft = plainMerge tft = gridMerge tft =+ -- >+ -- > "___aaa__" "____b____" "_____" "___aaa______b_________" "+----------+-----------+-------+"+ -- > "___aaa__" "____b____" "_____" "___aaa______b_________" "| ___aaa__ | ____b____ | _____ |"+ -- > "________" "____b____" "_____" "____________b_________" "| ___aaa__ | ____b____ | _____ |"+ -- > "________dddddddddeeeee" "| ________ | ____b____ | _____ |"+ -- > "________" "ddddddddd" "eeeee" "ccccccccdddddddddeeeee" "+----------+-----------+-------+"+ -- > "cccccccc" "ddddddddd" "eeeee" "ccccccccdddddddddeeeee" "| ________ | ddddddddd | eeeee |"+ -- > "cccccccc" "ddddddddd" "eeeee" "_________________eeeee" "| cccccccc | ddddddddd | eeeee |"+ -- > "________" "_________" "eeeee" "__________________ggg_" "| cccccccc | ddddddddd | eeeee |"+ -- > "___ff_____________ggg_" "| ________ | _________ | eeeee |"+ -- > "________" "_________" "_ggg_" "___ff_____________ggg_" "+----------+-----------+-------+"+ -- > "___ff___" "_________" "_ggg_" "__________________ggg_" "| ________ | _________ | _ggg_ |"+ -- > "___ff___" "_________" "_ggg_" "| ___ff___ | _________ | _ggg_ |"+ -- > "________" "_________" "_ggg_" "| ___ff___ | _________ | _ggg_ |"+ -- > "| ________ | _________ | _ggg_ |"+ -- > "+----------+-----------+-------+"+ --++) where ---------------------------------------------------------------------------------------------------------------++-- import++ import qualified Char as Ch+ import qualified List as L++-- basic definitions and basic functions++ type TextFrame = [String]++ isNonSpaceWhite :: Char -> Bool+ isNonSpaceWhite ch = (Ch.isSpace ch) && (ch /= ' ')++ findTextFrameError :: [String] -> Maybe String+ findTextFrameError [] = Nothing+ findTextFrameError (str:strL) = iter(length str, strL)+ where iter(n,[]) = Nothing+ iter(n,str:strL) = if any isNonSpaceWhite str+ then Just ("String contains illegat white space characters: \n" ++ str)+ else let n' = length str+ in if n' == n+ then iter(n,strL)+ else Just (concat ["Contains strings of different length (e.g. ",+ show n, " and ", show n', ")."])++ correctTextFrame :: [String] -> TextFrame+ correctTextFrame tf =+ if or (map (\ str -> any isNonSpaceWhite str) tf)+ then error "Illegal white space characters."+ else let w = width tf+ in (map (\ str -> str ++ (replicate (w - (length str)) ' ')) tf)++ width :: TextFrame -> Int+ width [] = 0+ width strL = maximum (map length strL)++ height :: TextFrame -> Int+ height = length++ printTextFrame :: TextFrame -> IO ()+ printTextFrame = putStr . unlines++ textFrameBox :: TextFrame -> TextFrame+ textFrameBox tf = [rule] ++ (map (\ str -> ("| " ++ str ++ " |")) tf) ++ [rule]+ where w = width tf+ rule = "+" ++ (replicate (w + 2) '-') ++ "+"++ textFrameBracket :: TextFrame -> TextFrame+ textFrameBracket [] = ["[]"]+ textFrameBracket [str] = [ "[" ++ str ++ "]" ]+ textFrameBracket strL = line ++ (map (\ str -> "| " ++ str ++ " |") strL) ++ line+ where line = [ "+-" ++ (replicate (width strL) ' ') ++ "-+" ]++ defaultTextFrame :: Show a => a -> TextFrame+ defaultTextFrame x = [show x]++-- the Display type class++ class Display a where+ textFrame :: a -> TextFrame+ display :: a -> IO ()+ display = printTextFrame . textFrame++ instance Display Bool where+ textFrame b = if b then ["1"] else ["0"]++ instance Display Int where+ textFrame = defaultTextFrame++ instance Display Integer where+ textFrame = defaultTextFrame++ instance Display Float where+ textFrame = defaultTextFrame++ instance Display Double where+ textFrame = defaultTextFrame++ instance Display Char where+ textFrame ch = [[ch]]++ instance Display String where+ textFrame str = [str]++ instance Display () where+ textFrame () = [""]++-- text frame tables++ type TextFrameTable = [[TextFrame]]++ columnWidthList :: TextFrameTable -> [Int]+ columnWidthList tft = iter [] tft+ where listMax [] mL = mL+ listMax nL [] = nL+ listMax (n:nL) (m:mL) = (max n m) : (listMax nL mL)+ iter nL [] = nL+ iter nL (row:tft) = iter (listMax nL (map width row)) tft++ rowHeightList :: TextFrameTable -> [Int]+ rowHeightList tft = map (\ row -> (maximum (0 : (map (\ cell -> (height cell)) row)))) tft++ correctTextFrameTable :: TextFrameTable -> TextFrameTable+ correctTextFrameTable tft = tft''''+ where colWidthL = columnWidthList tft+ rowHeightL = rowHeightList tft+ -- 1. remove empty rows+ tft' = filter (not . null) tft+ -- 2. fill up the rows to equal length+ colNumber = length colWidthL+ dummyTextFrame = [""] :: TextFrame+ fillRow row = row ++ (replicate (colNumber - (length row)) dummyTextFrame)+ tft'' = map fillRow tft' :: TextFrameTable+ -- 3. remove zero width columns+ remove [] [] = []+ remove (n:nL) (cell:row) = if n == 0+ then remove nL row+ else cell : (remove nL row)+ remove _ _ = error "correctTextFrameTable -- unexpected error!"+ tft''' = map (remove colWidthL) tft''+ -- 4. remove empty rows again+ tft'''' = filter (not . null) tft'''++ bottomAlign :: TextFrameTable -> TextFrameTable+ bottomAlign tft = allRows tft (rowHeightList tft)+ where flushBottom tf h = (replicate (h - (height tf)) (replicate (width tf) ' ')) ++ tf+ oneRow row h = map (\ cell -> (flushBottom cell h)) row+ allRows tft rowHeightList = map (\ (row,h) -> oneRow row h) (zip tft rowHeightList)++ topAlign :: TextFrameTable -> TextFrameTable+ topAlign tft = allRows tft (rowHeightList tft)+ where flushTop tf h = tf ++ (replicate (h - (height tf)) (replicate (width tf) ' '))+ oneRow row h = map (\ cell -> (flushTop cell h)) row+ allRows tft rowHeightList = map (\ (row,h) -> oneRow row h) (zip tft rowHeightList)++ centerAlign :: TextFrameTable -> TextFrameTable+ centerAlign tft = allRows tft (rowHeightList tft)+ where center tf h = let emptyRow = (replicate (width tf) ' ')+ h' = height tf+ topBlock = replicate ((h - h') `div` 2) emptyRow+ botBlock = replicate (((h - h') `div` 2) + ((h - h') `mod` 2)) emptyRow+ in topBlock ++ tf ++ botBlock+ oneRow row h = map (\ cell -> (center cell h)) row+ allRows tft rowHeightList = map (\ (row,h) -> oneRow row h) (zip tft rowHeightList)++ leftAlign :: TextFrameTable -> TextFrameTable+ leftAlign tft = map rowAlign tft+ where colWidthL = columnWidthList tft+ rowAlign row = map (\ (cell,w) -> (flushLeft cell w)) (zip row colWidthL)+ flushLeft tf n = map (\ str -> (str ++ (replicate (n - (length str)) ' '))) tf++ rightAlign :: TextFrameTable -> TextFrameTable+ rightAlign tft = map rowAlign tft+ where colWidthL = columnWidthList tft+ rowAlign row = map (\ (cell,w) -> (flushRight cell w)) (zip row colWidthL)+ flushRight tf n = map (\ str -> ((replicate (n - (length str)) ' ') ++ str)) tf++ middleAlign :: TextFrameTable -> TextFrameTable+ middleAlign tft = map rowAlign tft+ where colWidthL = columnWidthList tft+ rowAlign row = map (\ (cell,w) -> (centralize cell w)) (zip row colWidthL)+ centralize tf n = map (\ str -> (center str (length str) n)) tf+ center str l n = let d = (n - l) `div` 2+ m = (n - l) `mod` 2+ in (replicate d ' ') ++ str ++ (replicate (d + m) ' ')++ normalTextFrameTable :: TextFrameTable -> TextFrameTable+ normalTextFrameTable = middleAlign . centerAlign . correctTextFrameTable++ plainMerge :: TextFrameTable -> TextFrame+ plainMerge tft = concat (map mergeTextFrames tft)+ where mergeTextFrames tfL = map concat (L.transpose tfL)++ gridMerge :: TextFrameTable -> TextFrame+ gridMerge tft = tf+ where oneLine strL = "| " ++ (concat (L.intersperse " | " strL)) ++ " |"+ oneFrameRow row = map oneLine (L.transpose row)+ lineRow = "+-" ++ (concat (L.intersperse "-+-" (map (\ n -> (replicate n '-')) (columnWidthList tft)))) ++ "-+"+ tf = [lineRow] ++ (concat (L.intersperse [lineRow] (map oneFrameRow tft))) ++ [lineRow]+++