-- | Basic stuff for propositional logic: datatype, parsing and
-- printing.  'IsPropositional' is a subclass of 'IsLiteral' of
-- formula types that support binary combinations.

{-# OPTIONS_GHC -Wall #-}

{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module Data.Logic.ATP.Prop
    (
    -- * Propositional formulas
      IsPropositional((.|.), (.&.), (.<=>.), (.=>.), foldPropositional', foldCombination)
    , BinOp(..), binop
    , (⇒), (==>), (⊃), (→)
    , (⇔), (<=>), (↔), (<==>)
    , (∧), (·)
    , (∨)
    , foldPropositional
    , zipPropositional
    , convertPropositional
    , convertToPropositional
    , precedencePropositional
    , associativityPropositional
    , prettyPropositional
    , showPropositional
    , onatomsPropositional
    , overatomsPropositional
    -- * Restricted propositional formula class
    , JustPropositional
    -- * Interpretation of formulas.
    , eval
    , atoms
    -- * Truth Tables
    , TruthTable(TruthTable)
    , onallvaluations
    , truthTable
    -- * Tautologies and related concepts
    , tautology
    , unsatisfiable
    , satisfiable
    -- * Substitution
    , psubst
    -- * Dualization
    , dual
    -- * Simplification
    , psimplify
    , psimplify1
    -- * Normal forms
    , nnf
    , nenf
    , list_conj
    , list_disj
    , mk_lits
    , allsatvaluations
    , dnfSet
    , purednf
    , simpdnf
    , rawdnf
    , dnf
    , purecnf
    , simpcnf
    , cnf'
    , cnf_
    , trivial
    -- * Instance
    , Prop(P, pname)
    , PFormula(F, T, Atom, Not, And, Or, Imp, Iff)
    -- * Tests
    , testProp
    ) where

import Data.Foldable as Foldable (null)
import Data.Function (on)
import Data.Data (Data)
import Data.List as List (groupBy, intercalate, map, sortBy)
import Data.Logic.ATP.Formulas (atom_union, fromBool, IsAtom,
                                IsFormula(AtomOf, asBool, true, false, atomic, overatoms, onatoms), prettyBool)
import Data.Logic.ATP.Lib ((|=>), distrib, fpf, setAny)
import Data.Logic.ATP.Lit ((.~.), (¬), convertLiteral, convertToLiteral, IsLiteral(foldLiteral', naiveNegate, foldNegation),
                           JustLiteral, LFormula, negate, positive, )
import Data.Logic.ATP.Pretty (Associativity(InfixN, InfixR, InfixA), Doc, HasFixity(precedence, associativity),
                              Precedence, Pretty(pPrint, pPrintPrec), prettyShow, Side(Top, LHS, RHS, Unary), testParen, text,
                              notPrec, andPrec, orPrec, impPrec, iffPrec, leafPrec, boolPrec)
import Data.Map.Strict as Map (Map)
import Data.Maybe (fromMaybe)
import Data.Monoid ((<>))
import Data.Set as Set (empty, filter, fromList, intersection, isProperSubsetOf, map,
                        minView, partition, Set, singleton, toAscList, union)
import Data.String (IsString(fromString))
import Data.Typeable (Typeable)
import Prelude hiding (negate, null)
import Text.PrettyPrint.HughesPJClass (maybeParens, PrettyLevel, vcat)
import Test.HUnit

-- |A type class for propositional logic.  If the type we are writing
-- an instance for is a zero-order (aka propositional) logic type
-- there will generally by a type or a type parameter corresponding to
-- atom.  For first order or predicate logic types, it is generally
-- easiest to just use the formula type itself as the atom type, and
-- raise errors in the implementation if a non-atomic formula somehow
-- appears where an atomic formula is expected (i.e. as an argument to
-- atomic or to the third argument of foldPropositional.)
class IsLiteral formula => IsPropositional formula where
    -- | Disjunction/OR
    (.|.) :: formula -> formula -> formula
    -- | Conjunction/AND.  @x .&. y = (.~.) ((.~.) x .|. (.~.) y)@
    (.&.) :: formula -> formula -> formula
    -- | Equivalence.  @x .<=>. y = (x .=>. y) .&. (y .=>. x)@
    (.<=>.) :: formula -> formula -> formula
    -- | Implication.  @x .=>. y = ((.~.) x .|. y)@
    (.=>.) :: formula -> formula -> formula

    -- | A fold function that distributes different sorts of formula
    -- to its parameter functions, one to handle binary operators, one
    -- for negations, and one for atomic formulas.  See examples of its
    -- use to implement the polymorphic functions below.
    foldPropositional' :: (formula -> r)                     -- ^ fold on some higher order formula
                       -> (formula -> BinOp -> formula -> r) -- ^ fold on a binary operation formula.  Functions
                                                             -- of this type can be constructed using 'binop'.
                       -> (formula -> r)                     -- ^ fold on a negated formula
                       -> (Bool -> r)                        -- ^ fold on a boolean formula
                       -> (AtomOf formula -> r)              -- ^ fold on an atomic formula
                       -> formula -> r
    -- | An alternative fold function for binary combinations of formulas
    foldCombination :: (formula -> r) -- other
                    -> (formula -> formula -> r) -- disjunction
                    -> (formula -> formula -> r) -- conjunction
                    -> (formula -> formula -> r) -- implication
                    -> (formula -> formula -> r) -- equivalence
                    -> formula -> r

-- | Implication synonyms.  Note that if the -XUnicodeSyntax option is
-- turned on the operator ⇒ can not be declared/used as a function -
-- it becomes a reserved special character used in type signatures.
(⇒), (⊃), (==>), (→) :: IsPropositional formula => formula -> formula -> formula
⇒ :: forall formula.
IsPropositional formula =>
formula -> formula -> formula
(⇒) = formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(.=>.)
⊃ :: forall formula.
IsPropositional formula =>
formula -> formula -> formula
(⊃) = formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(.=>.)
==> :: forall formula.
IsPropositional formula =>
formula -> formula -> formula
(==>) = formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(.=>.)
→ :: forall formula.
IsPropositional formula =>
formula -> formula -> formula
(→) = formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(.=>.)
infixr 3 .=>., ⇒, ⊃, ==>, →

-- | If-and-only-if synonyms
(<=>), (<==>), (⇔), (↔) :: IsPropositional formula => formula -> formula -> formula
<=> :: forall formula.
IsPropositional formula =>
formula -> formula -> formula
(<=>) = formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(.<=>.)
<==> :: forall formula.
IsPropositional formula =>
formula -> formula -> formula
(<==>) = formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(.<=>.)
⇔ :: forall formula.
IsPropositional formula =>
formula -> formula -> formula
(⇔) = formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(.<=>.)
↔ :: forall formula.
IsPropositional formula =>
formula -> formula -> formula
(↔) = formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(.<=>.)
infixl 2 .<=>., <=>, <==>, ⇔, ↔

-- | And/conjunction synonyms
(∧), (·) :: IsPropositional formula => formula -> formula -> formula
∧ :: forall formula.
IsPropositional formula =>
formula -> formula -> formula
(∧) = formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(.&.)
· :: forall formula.
IsPropositional formula =>
formula -> formula -> formula
(·) = formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(.&.)
infixl 5 .&., ∧, ·

-- | Or/disjunction synonyms
(∨) :: IsPropositional formula => formula -> formula -> formula
∨ :: forall formula.
IsPropositional formula =>
formula -> formula -> formula
(∨) = formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(.|.)
infixl 4 .|., ∨

-- | Deconstruct a 'JustPropositional' formula.
foldPropositional :: JustPropositional pf =>
                     (pf -> BinOp -> pf -> r) -- ^ fold on a binary operation formula
                  -> (pf -> r)                -- ^ fold on a negated formula
                  -> (Bool -> r)              -- ^ fold on a boolean formula
                  -> (AtomOf pf -> r)         -- ^ fold on an atomic formula
                  -> pf -> r
foldPropositional :: forall pf r.
JustPropositional pf =>
(pf -> BinOp -> pf -> r)
-> (pf -> r) -> (Bool -> r) -> (AtomOf pf -> r) -> pf -> r
foldPropositional = (pf -> r)
-> (pf -> BinOp -> pf -> r)
-> (pf -> r)
-> (Bool -> r)
-> (AtomOf pf -> r)
-> pf
-> r
forall formula r.
IsPropositional formula =>
(formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
forall r.
(pf -> r)
-> (pf -> BinOp -> pf -> r)
-> (pf -> r)
-> (Bool -> r)
-> (AtomOf pf -> r)
-> pf
-> r
foldPropositional' (String -> pf -> r
forall a. HasCallStack => String -> a
error String
"JustPropositional failure")

-- | This type is used to construct the first argument of 'foldPropositional'.
data BinOp
    = (:<=>:)
    | (:=>:)
    | (:&:)
    | (:|:)
    deriving (BinOp -> BinOp -> Bool
(BinOp -> BinOp -> Bool) -> (BinOp -> BinOp -> Bool) -> Eq BinOp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BinOp -> BinOp -> Bool
== :: BinOp -> BinOp -> Bool
$c/= :: BinOp -> BinOp -> Bool
/= :: BinOp -> BinOp -> Bool
Eq, Eq BinOp
Eq BinOp =>
(BinOp -> BinOp -> Ordering)
-> (BinOp -> BinOp -> Bool)
-> (BinOp -> BinOp -> Bool)
-> (BinOp -> BinOp -> Bool)
-> (BinOp -> BinOp -> Bool)
-> (BinOp -> BinOp -> BinOp)
-> (BinOp -> BinOp -> BinOp)
-> Ord BinOp
BinOp -> BinOp -> Bool
BinOp -> BinOp -> Ordering
BinOp -> BinOp -> BinOp
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: BinOp -> BinOp -> Ordering
compare :: BinOp -> BinOp -> Ordering
$c< :: BinOp -> BinOp -> Bool
< :: BinOp -> BinOp -> Bool
$c<= :: BinOp -> BinOp -> Bool
<= :: BinOp -> BinOp -> Bool
$c> :: BinOp -> BinOp -> Bool
> :: BinOp -> BinOp -> Bool
$c>= :: BinOp -> BinOp -> Bool
>= :: BinOp -> BinOp -> Bool
$cmax :: BinOp -> BinOp -> BinOp
max :: BinOp -> BinOp -> BinOp
$cmin :: BinOp -> BinOp -> BinOp
min :: BinOp -> BinOp -> BinOp
Ord, Typeable BinOp
Typeable BinOp =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> BinOp -> c BinOp)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c BinOp)
-> (BinOp -> Constr)
-> (BinOp -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c BinOp))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BinOp))
-> ((forall b. Data b => b -> b) -> BinOp -> BinOp)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BinOp -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BinOp -> r)
-> (forall u. (forall d. Data d => d -> u) -> BinOp -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> BinOp -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> BinOp -> m BinOp)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> BinOp -> m BinOp)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> BinOp -> m BinOp)
-> Data BinOp
BinOp -> Constr
BinOp -> DataType
(forall b. Data b => b -> b) -> BinOp -> BinOp
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> BinOp -> u
forall u. (forall d. Data d => d -> u) -> BinOp -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BinOp -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BinOp -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BinOp -> m BinOp
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BinOp -> m BinOp
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BinOp
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BinOp -> c BinOp
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BinOp)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BinOp)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BinOp -> c BinOp
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BinOp -> c BinOp
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BinOp
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BinOp
$ctoConstr :: BinOp -> Constr
toConstr :: BinOp -> Constr
$cdataTypeOf :: BinOp -> DataType
dataTypeOf :: BinOp -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BinOp)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BinOp)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BinOp)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BinOp)
$cgmapT :: (forall b. Data b => b -> b) -> BinOp -> BinOp
gmapT :: (forall b. Data b => b -> b) -> BinOp -> BinOp
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BinOp -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BinOp -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BinOp -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BinOp -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> BinOp -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> BinOp -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> BinOp -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> BinOp -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BinOp -> m BinOp
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BinOp -> m BinOp
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BinOp -> m BinOp
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BinOp -> m BinOp
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BinOp -> m BinOp
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BinOp -> m BinOp
Data, Typeable, Int -> BinOp -> ShowS
[BinOp] -> ShowS
BinOp -> String
(Int -> BinOp -> ShowS)
-> (BinOp -> String) -> ([BinOp] -> ShowS) -> Show BinOp
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BinOp -> ShowS
showsPrec :: Int -> BinOp -> ShowS
$cshow :: BinOp -> String
show :: BinOp -> String
$cshowList :: [BinOp] -> ShowS
showList :: [BinOp] -> ShowS
Show, Int -> BinOp
BinOp -> Int
BinOp -> [BinOp]
BinOp -> BinOp
BinOp -> BinOp -> [BinOp]
BinOp -> BinOp -> BinOp -> [BinOp]
(BinOp -> BinOp)
-> (BinOp -> BinOp)
-> (Int -> BinOp)
-> (BinOp -> Int)
-> (BinOp -> [BinOp])
-> (BinOp -> BinOp -> [BinOp])
-> (BinOp -> BinOp -> [BinOp])
-> (BinOp -> BinOp -> BinOp -> [BinOp])
-> Enum BinOp
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: BinOp -> BinOp
succ :: BinOp -> BinOp
$cpred :: BinOp -> BinOp
pred :: BinOp -> BinOp
$ctoEnum :: Int -> BinOp
toEnum :: Int -> BinOp
$cfromEnum :: BinOp -> Int
fromEnum :: BinOp -> Int
$cenumFrom :: BinOp -> [BinOp]
enumFrom :: BinOp -> [BinOp]
$cenumFromThen :: BinOp -> BinOp -> [BinOp]
enumFromThen :: BinOp -> BinOp -> [BinOp]
$cenumFromTo :: BinOp -> BinOp -> [BinOp]
enumFromTo :: BinOp -> BinOp -> [BinOp]
$cenumFromThenTo :: BinOp -> BinOp -> BinOp -> [BinOp]
enumFromThenTo :: BinOp -> BinOp -> BinOp -> [BinOp]
Enum, BinOp
BinOp -> BinOp -> Bounded BinOp
forall a. a -> a -> Bounded a
$cminBound :: BinOp
minBound :: BinOp
$cmaxBound :: BinOp
maxBound :: BinOp
Bounded)

-- | Combine formulas with a 'BinOp', for use building the first
-- argument of 'foldPropositional'.
binop :: IsPropositional formula => formula -> BinOp -> formula -> formula
binop :: forall formula.
IsPropositional formula =>
formula -> BinOp -> formula -> formula
binop formula
f1 BinOp
(:<=>:) formula
f2 = formula
f1 formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. formula
f2
binop formula
f1 BinOp
(:=>:) formula
f2 = formula
f1 formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. formula
f2
binop formula
f1 BinOp
(:&:) formula
f2 = formula
f1 formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. formula
f2
binop formula
f1 BinOp
(:|:) formula
f2 = formula
f1 formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. formula
f2

-- | Combine two 'JustPropositional' formulas if they are similar.
zipPropositional :: (JustPropositional pf1, JustPropositional pf2) =>
                    (pf1 -> BinOp -> pf1 -> pf2 -> BinOp -> pf2 -> Maybe r) -- ^ Combine two binary operation formulas
                 -> (pf1 -> pf2 -> Maybe r)                                 -- ^ Combine two negated formulas
                 -> (Bool -> Bool -> Maybe r)                               -- ^ Combine two boolean formulas
                 -> (AtomOf pf1 -> AtomOf pf2 -> Maybe r)                   -- ^ Combine two atomic formulas
                 -> pf1 -> pf2 -> Maybe r                                   -- ^ Result is Nothing if the formulas don't unify
zipPropositional :: forall pf1 pf2 r.
(JustPropositional pf1, JustPropositional pf2) =>
(pf1 -> BinOp -> pf1 -> pf2 -> BinOp -> pf2 -> Maybe r)
-> (pf1 -> pf2 -> Maybe r)
-> (Bool -> Bool -> Maybe r)
-> (AtomOf pf1 -> AtomOf pf2 -> Maybe r)
-> pf1
-> pf2
-> Maybe r
zipPropositional pf1 -> BinOp -> pf1 -> pf2 -> BinOp -> pf2 -> Maybe r
co pf1 -> pf2 -> Maybe r
ne Bool -> Bool -> Maybe r
tf AtomOf pf1 -> AtomOf pf2 -> Maybe r
at pf1
fm1 pf2
fm2 =
    (pf1 -> BinOp -> pf1 -> Maybe r)
-> (pf1 -> Maybe r)
-> (Bool -> Maybe r)
-> (AtomOf pf1 -> Maybe r)
-> pf1
-> Maybe r
forall pf r.
JustPropositional pf =>
(pf -> BinOp -> pf -> r)
-> (pf -> r) -> (Bool -> r) -> (AtomOf pf -> r) -> pf -> r
foldPropositional pf1 -> BinOp -> pf1 -> Maybe r
co' pf1 -> Maybe r
ne' Bool -> Maybe r
tf' AtomOf pf1 -> Maybe r
at' pf1
fm1
    where
      co' :: pf1 -> BinOp -> pf1 -> Maybe r
co' pf1
l1 BinOp
op1 pf1
r1 = (pf2 -> BinOp -> pf2 -> Maybe r)
-> (pf2 -> Maybe r)
-> (Bool -> Maybe r)
-> (AtomOf pf2 -> Maybe r)
-> pf2
-> Maybe r
forall pf r.
JustPropositional pf =>
(pf -> BinOp -> pf -> r)
-> (pf -> r) -> (Bool -> r) -> (AtomOf pf -> r) -> pf -> r
foldPropositional (pf1 -> BinOp -> pf1 -> pf2 -> BinOp -> pf2 -> Maybe r
co pf1
l1 BinOp
op1 pf1
r1) (\pf2
_ -> Maybe r
forall a. Maybe a
Nothing) (\Bool
_ -> Maybe r
forall a. Maybe a
Nothing) (\AtomOf pf2
_ -> Maybe r
forall a. Maybe a
Nothing) pf2
fm2
      ne' :: pf1 -> Maybe r
ne' pf1
x1 = (pf2 -> BinOp -> pf2 -> Maybe r)
-> (pf2 -> Maybe r)
-> (Bool -> Maybe r)
-> (AtomOf pf2 -> Maybe r)
-> pf2
-> Maybe r
forall pf r.
JustPropositional pf =>
(pf -> BinOp -> pf -> r)
-> (pf -> r) -> (Bool -> r) -> (AtomOf pf -> r) -> pf -> r
foldPropositional (\pf2
_ BinOp
_ pf2
_ -> Maybe r
forall a. Maybe a
Nothing)     (pf1 -> pf2 -> Maybe r
ne pf1
x1)     (\Bool
_ -> Maybe r
forall a. Maybe a
Nothing) (\AtomOf pf2
_ -> Maybe r
forall a. Maybe a
Nothing) pf2
fm2
      tf' :: Bool -> Maybe r
tf' Bool
x1 = (pf2 -> BinOp -> pf2 -> Maybe r)
-> (pf2 -> Maybe r)
-> (Bool -> Maybe r)
-> (AtomOf pf2 -> Maybe r)
-> pf2
-> Maybe r
forall pf r.
JustPropositional pf =>
(pf -> BinOp -> pf -> r)
-> (pf -> r) -> (Bool -> r) -> (AtomOf pf -> r) -> pf -> r
foldPropositional (\pf2
_ BinOp
_ pf2
_ -> Maybe r
forall a. Maybe a
Nothing) (\pf2
_ -> Maybe r
forall a. Maybe a
Nothing)     (Bool -> Bool -> Maybe r
tf Bool
x1)     (\AtomOf pf2
_ -> Maybe r
forall a. Maybe a
Nothing) pf2
fm2
      at' :: AtomOf pf1 -> Maybe r
at' AtomOf pf1
a1 = (pf2 -> BinOp -> pf2 -> Maybe r)
-> (pf2 -> Maybe r)
-> (Bool -> Maybe r)
-> (AtomOf pf2 -> Maybe r)
-> pf2
-> Maybe r
forall pf r.
JustPropositional pf =>
(pf -> BinOp -> pf -> r)
-> (pf -> r) -> (Bool -> r) -> (AtomOf pf -> r) -> pf -> r
foldPropositional (\pf2
_ BinOp
_ pf2
_ -> Maybe r
forall a. Maybe a
Nothing) (\pf2
_ -> Maybe r
forall a. Maybe a
Nothing) (\Bool
_ -> Maybe r
forall a. Maybe a
Nothing)     (AtomOf pf1 -> AtomOf pf2 -> Maybe r
at AtomOf pf1
a1)     pf2
fm2

-- | Convert any instance of 'JustPropositional' to any 'IsPropositional' formula.
convertPropositional :: (JustPropositional pf1, IsPropositional pf2) =>
                        (AtomOf pf1 -> AtomOf pf2) -- ^ Convert an atomic formula
                     -> pf1 -> pf2
convertPropositional :: forall pf1 pf2.
(JustPropositional pf1, IsPropositional pf2) =>
(AtomOf pf1 -> AtomOf pf2) -> pf1 -> pf2
convertPropositional AtomOf pf1 -> AtomOf pf2
ca pf1
pf =
    (pf1 -> BinOp -> pf1 -> pf2)
-> (pf1 -> pf2)
-> (Bool -> pf2)
-> (AtomOf pf1 -> pf2)
-> pf1
-> pf2
forall pf r.
JustPropositional pf =>
(pf -> BinOp -> pf -> r)
-> (pf -> r) -> (Bool -> r) -> (AtomOf pf -> r) -> pf -> r
foldPropositional pf1 -> BinOp -> pf1 -> pf2
co pf1 -> pf2
ne Bool -> pf2
tf (AtomOf pf2 -> pf2
forall formula. IsFormula formula => AtomOf formula -> formula
atomic (AtomOf pf2 -> pf2)
-> (AtomOf pf1 -> AtomOf pf2) -> AtomOf pf1 -> pf2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AtomOf pf1 -> AtomOf pf2
ca) pf1
pf
    where
      co :: pf1 -> BinOp -> pf1 -> pf2
co pf1
p BinOp
(:&:) pf1
q = ((AtomOf pf1 -> AtomOf pf2) -> pf1 -> pf2
forall pf1 pf2.
(JustPropositional pf1, IsPropositional pf2) =>
(AtomOf pf1 -> AtomOf pf2) -> pf1 -> pf2
convertPropositional AtomOf pf1 -> AtomOf pf2
ca pf1
p) pf2 -> pf2 -> pf2
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. ((AtomOf pf1 -> AtomOf pf2) -> pf1 -> pf2
forall pf1 pf2.
(JustPropositional pf1, IsPropositional pf2) =>
(AtomOf pf1 -> AtomOf pf2) -> pf1 -> pf2
convertPropositional AtomOf pf1 -> AtomOf pf2
ca pf1
q)
      co pf1
p BinOp
(:|:) pf1
q = ((AtomOf pf1 -> AtomOf pf2) -> pf1 -> pf2
forall pf1 pf2.
(JustPropositional pf1, IsPropositional pf2) =>
(AtomOf pf1 -> AtomOf pf2) -> pf1 -> pf2
convertPropositional AtomOf pf1 -> AtomOf pf2
ca pf1
p) pf2 -> pf2 -> pf2
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. ((AtomOf pf1 -> AtomOf pf2) -> pf1 -> pf2
forall pf1 pf2.
(JustPropositional pf1, IsPropositional pf2) =>
(AtomOf pf1 -> AtomOf pf2) -> pf1 -> pf2
convertPropositional AtomOf pf1 -> AtomOf pf2
ca pf1
q)
      co pf1
p BinOp
(:=>:) pf1
q = ((AtomOf pf1 -> AtomOf pf2) -> pf1 -> pf2
forall pf1 pf2.
(JustPropositional pf1, IsPropositional pf2) =>
(AtomOf pf1 -> AtomOf pf2) -> pf1 -> pf2
convertPropositional AtomOf pf1 -> AtomOf pf2
ca pf1
p) pf2 -> pf2 -> pf2
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. ((AtomOf pf1 -> AtomOf pf2) -> pf1 -> pf2
forall pf1 pf2.
(JustPropositional pf1, IsPropositional pf2) =>
(AtomOf pf1 -> AtomOf pf2) -> pf1 -> pf2
convertPropositional AtomOf pf1 -> AtomOf pf2
ca pf1
q)
      co pf1
p BinOp
(:<=>:) pf1
q = ((AtomOf pf1 -> AtomOf pf2) -> pf1 -> pf2
forall pf1 pf2.
(JustPropositional pf1, IsPropositional pf2) =>
(AtomOf pf1 -> AtomOf pf2) -> pf1 -> pf2
convertPropositional AtomOf pf1 -> AtomOf pf2
ca pf1
p) pf2 -> pf2 -> pf2
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. ((AtomOf pf1 -> AtomOf pf2) -> pf1 -> pf2
forall pf1 pf2.
(JustPropositional pf1, IsPropositional pf2) =>
(AtomOf pf1 -> AtomOf pf2) -> pf1 -> pf2
convertPropositional AtomOf pf1 -> AtomOf pf2
ca pf1
q)
      ne :: pf1 -> pf2
ne pf1
p = pf2 -> pf2
forall formula. IsLiteral formula => formula -> formula
(.~.) ((AtomOf pf1 -> AtomOf pf2) -> pf1 -> pf2
forall pf1 pf2.
(JustPropositional pf1, IsPropositional pf2) =>
(AtomOf pf1 -> AtomOf pf2) -> pf1 -> pf2
convertPropositional AtomOf pf1 -> AtomOf pf2
ca pf1
p)
      tf :: Bool -> pf2
tf = Bool -> pf2
forall formula. IsFormula formula => Bool -> formula
fromBool

-- | Convert any instance of 'IsPropositional' to a 'JustPropositional' formula.  Typically the
-- ho (higher order) argument calls error if it encounters something it can't handle.
convertToPropositional :: (IsPropositional formula, JustPropositional pf) =>
                          (formula -> pf)               -- ^ Convert a higher order formula
                       -> (AtomOf formula -> AtomOf pf) -- ^ Convert an atomic formula
                       -> formula -> pf
convertToPropositional :: forall formula pf.
(IsPropositional formula, JustPropositional pf) =>
(formula -> pf) -> (AtomOf formula -> AtomOf pf) -> formula -> pf
convertToPropositional formula -> pf
ho AtomOf formula -> AtomOf pf
ca formula
fm =
    (formula -> pf)
-> (formula -> BinOp -> formula -> pf)
-> (formula -> pf)
-> (Bool -> pf)
-> (AtomOf formula -> pf)
-> formula
-> pf
forall formula r.
IsPropositional formula =>
(formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
forall r.
(formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
foldPropositional' formula -> pf
ho formula -> BinOp -> formula -> pf
co formula -> pf
ne Bool -> pf
tf (AtomOf pf -> pf
forall formula. IsFormula formula => AtomOf formula -> formula
atomic (AtomOf pf -> pf)
-> (AtomOf formula -> AtomOf pf) -> AtomOf formula -> pf
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AtomOf formula -> AtomOf pf
ca) formula
fm
    where
      co :: formula -> BinOp -> formula -> pf
co formula
p BinOp
(:&:) formula
q = ((formula -> pf) -> (AtomOf formula -> AtomOf pf) -> formula -> pf
forall formula pf.
(IsPropositional formula, JustPropositional pf) =>
(formula -> pf) -> (AtomOf formula -> AtomOf pf) -> formula -> pf
convertToPropositional formula -> pf
ho AtomOf formula -> AtomOf pf
ca formula
p) pf -> pf -> pf
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. ((formula -> pf) -> (AtomOf formula -> AtomOf pf) -> formula -> pf
forall formula pf.
(IsPropositional formula, JustPropositional pf) =>
(formula -> pf) -> (AtomOf formula -> AtomOf pf) -> formula -> pf
convertToPropositional formula -> pf
ho AtomOf formula -> AtomOf pf
ca formula
q)
      co formula
p BinOp
(:|:) formula
q = ((formula -> pf) -> (AtomOf formula -> AtomOf pf) -> formula -> pf
forall formula pf.
(IsPropositional formula, JustPropositional pf) =>
(formula -> pf) -> (AtomOf formula -> AtomOf pf) -> formula -> pf
convertToPropositional formula -> pf
ho AtomOf formula -> AtomOf pf
ca formula
p) pf -> pf -> pf
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. ((formula -> pf) -> (AtomOf formula -> AtomOf pf) -> formula -> pf
forall formula pf.
(IsPropositional formula, JustPropositional pf) =>
(formula -> pf) -> (AtomOf formula -> AtomOf pf) -> formula -> pf
convertToPropositional formula -> pf
ho AtomOf formula -> AtomOf pf
ca formula
q)
      co formula
p BinOp
(:=>:) formula
q = ((formula -> pf) -> (AtomOf formula -> AtomOf pf) -> formula -> pf
forall formula pf.
(IsPropositional formula, JustPropositional pf) =>
(formula -> pf) -> (AtomOf formula -> AtomOf pf) -> formula -> pf
convertToPropositional formula -> pf
ho AtomOf formula -> AtomOf pf
ca formula
p) pf -> pf -> pf
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. ((formula -> pf) -> (AtomOf formula -> AtomOf pf) -> formula -> pf
forall formula pf.
(IsPropositional formula, JustPropositional pf) =>
(formula -> pf) -> (AtomOf formula -> AtomOf pf) -> formula -> pf
convertToPropositional formula -> pf
ho AtomOf formula -> AtomOf pf
ca formula
q)
      co formula
p BinOp
(:<=>:) formula
q = ((formula -> pf) -> (AtomOf formula -> AtomOf pf) -> formula -> pf
forall formula pf.
(IsPropositional formula, JustPropositional pf) =>
(formula -> pf) -> (AtomOf formula -> AtomOf pf) -> formula -> pf
convertToPropositional formula -> pf
ho AtomOf formula -> AtomOf pf
ca formula
p) pf -> pf -> pf
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. ((formula -> pf) -> (AtomOf formula -> AtomOf pf) -> formula -> pf
forall formula pf.
(IsPropositional formula, JustPropositional pf) =>
(formula -> pf) -> (AtomOf formula -> AtomOf pf) -> formula -> pf
convertToPropositional formula -> pf
ho AtomOf formula -> AtomOf pf
ca formula
q)
      ne :: formula -> pf
ne formula
p = pf -> pf
forall formula. IsLiteral formula => formula -> formula
(.~.) ((formula -> pf) -> (AtomOf formula -> AtomOf pf) -> formula -> pf
forall formula pf.
(IsPropositional formula, JustPropositional pf) =>
(formula -> pf) -> (AtomOf formula -> AtomOf pf) -> formula -> pf
convertToPropositional formula -> pf
ho AtomOf formula -> AtomOf pf
ca formula
p)
      tf :: Bool -> pf
tf = Bool -> pf
forall formula. IsFormula formula => Bool -> formula
fromBool

-- | Implementation of 'precedence' for any 'JustPropostional' type.
precedencePropositional ::JustPropositional pf => pf -> Precedence
precedencePropositional :: forall pf. JustPropositional pf => pf -> Precedence
precedencePropositional = (pf -> BinOp -> pf -> a)
-> (pf -> a) -> (Bool -> a) -> (AtomOf pf -> a) -> pf -> a
forall pf r.
JustPropositional pf =>
(pf -> BinOp -> pf -> r)
-> (pf -> r) -> (Bool -> r) -> (AtomOf pf -> r) -> pf -> r
foldPropositional pf -> BinOp -> pf -> a
forall {a} {p} {p}. Num a => p -> BinOp -> p -> a
co (\pf
_ -> a
Precedence
notPrec) (\Bool
_ -> a
Precedence
boolPrec) AtomOf pf -> a
AtomOf pf -> Precedence
forall x. HasFixity x => x -> Precedence
precedence
    where
      co :: p -> BinOp -> p -> a
co p
_ BinOp
(:&:) p
_ = a
Precedence
andPrec
      co p
_ BinOp
(:|:) p
_ = a
Precedence
orPrec
      co p
_ BinOp
(:=>:) p
_ = a
Precedence
impPrec
      co p
_ BinOp
(:<=>:) p
_ = a
Precedence
iffPrec

associativityPropositional :: JustPropositional pf => pf -> Associativity
associativityPropositional :: forall pf. JustPropositional pf => pf -> Associativity
associativityPropositional = (pf -> BinOp -> pf -> Associativity)
-> (pf -> Associativity)
-> (Bool -> Associativity)
-> (AtomOf pf -> Associativity)
-> pf
-> Associativity
forall pf r.
JustPropositional pf =>
(pf -> BinOp -> pf -> r)
-> (pf -> r) -> (Bool -> r) -> (AtomOf pf -> r) -> pf -> r
foldPropositional pf -> BinOp -> pf -> Associativity
forall {p} {p}. p -> BinOp -> p -> Associativity
co (Associativity -> pf -> Associativity
forall a b. a -> b -> a
const Associativity
InfixA) (Associativity -> Bool -> Associativity
forall a b. a -> b -> a
const Associativity
InfixN) AtomOf pf -> Associativity
forall x. HasFixity x => x -> Associativity
associativity
    where
      co :: p -> BinOp -> p -> Associativity
co p
_ BinOp
(:&:) p
_ = Associativity
InfixA
      co p
_ BinOp
(:|:) p
_ = Associativity
InfixA
      co p
_ BinOp
(:=>:) p
_ = Associativity
InfixR
      co p
_ BinOp
(:<=>:) p
_ = Associativity
InfixA -- yes, InfixA: (a<->b)<->c == a<->(b<->c)

-- | Implementation of 'pPrint' for any 'JustPropostional' type.
prettyPropositional :: forall pf. JustPropositional pf =>
                       Side -> PrettyLevel -> Rational -> pf -> Doc
prettyPropositional :: forall pf.
JustPropositional pf =>
Side -> PrettyLevel -> Rational -> pf -> Doc
prettyPropositional Side
side PrettyLevel
l Rational
r pf
fm =
    Bool -> Doc -> Doc
maybeParens (Side -> Rational -> Rational -> Associativity -> Bool
forall a.
(Eq a, Ord a, Num a) =>
Side -> a -> a -> Associativity -> Bool
testParen Side
side Rational
r (pf -> Precedence
forall x. HasFixity x => x -> Precedence
precedence pf
fm) (pf -> Associativity
forall x. HasFixity x => x -> Associativity
associativity pf
fm)) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ (pf -> BinOp -> pf -> Doc)
-> (pf -> Doc) -> (Bool -> Doc) -> (AtomOf pf -> Doc) -> pf -> Doc
forall pf r.
JustPropositional pf =>
(pf -> BinOp -> pf -> r)
-> (pf -> r) -> (Bool -> r) -> (AtomOf pf -> r) -> pf -> r
foldPropositional pf -> BinOp -> pf -> Doc
co pf -> Doc
ne Bool -> Doc
tf AtomOf pf -> Doc
at pf
fm
    where
      co :: pf -> BinOp -> pf -> Doc
      co :: pf -> BinOp -> pf -> Doc
co pf
p BinOp
(:&:) pf
q = Side -> PrettyLevel -> Rational -> pf -> Doc
forall pf.
JustPropositional pf =>
Side -> PrettyLevel -> Rational -> pf -> Doc
prettyPropositional Side
LHS PrettyLevel
l (pf -> Precedence
forall x. HasFixity x => x -> Precedence
precedence pf
fm) pf
p Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text String
"∧" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<>  Side -> PrettyLevel -> Rational -> pf -> Doc
forall pf.
JustPropositional pf =>
Side -> PrettyLevel -> Rational -> pf -> Doc
prettyPropositional Side
RHS PrettyLevel
l (pf -> Precedence
forall x. HasFixity x => x -> Precedence
precedence pf
fm) pf
q
      co pf
p BinOp
(:|:) pf
q = Side -> PrettyLevel -> Rational -> pf -> Doc
forall pf.
JustPropositional pf =>
Side -> PrettyLevel -> Rational -> pf -> Doc
prettyPropositional Side
LHS PrettyLevel
l (pf -> Precedence
forall x. HasFixity x => x -> Precedence
precedence pf
fm) pf
p Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text String
"∨" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Side -> PrettyLevel -> Rational -> pf -> Doc
forall pf.
JustPropositional pf =>
Side -> PrettyLevel -> Rational -> pf -> Doc
prettyPropositional Side
RHS PrettyLevel
l (pf -> Precedence
forall x. HasFixity x => x -> Precedence
precedence pf
fm) pf
q
      co pf
p BinOp
(:=>:) pf
q = Side -> PrettyLevel -> Rational -> pf -> Doc
forall pf.
JustPropositional pf =>
Side -> PrettyLevel -> Rational -> pf -> Doc
prettyPropositional Side
LHS PrettyLevel
l (pf -> Precedence
forall x. HasFixity x => x -> Precedence
precedence pf
fm) pf
p Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text String
"⇒" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Side -> PrettyLevel -> Rational -> pf -> Doc
forall pf.
JustPropositional pf =>
Side -> PrettyLevel -> Rational -> pf -> Doc
prettyPropositional Side
RHS PrettyLevel
l (pf -> Precedence
forall x. HasFixity x => x -> Precedence
precedence pf
fm) pf
q
      co pf
p BinOp
(:<=>:) pf
q = Side -> PrettyLevel -> Rational -> pf -> Doc
forall pf.
JustPropositional pf =>
Side -> PrettyLevel -> Rational -> pf -> Doc
prettyPropositional Side
LHS PrettyLevel
l (pf -> Precedence
forall x. HasFixity x => x -> Precedence
precedence pf
fm) pf
p Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text String
"⇔" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Side -> PrettyLevel -> Rational -> pf -> Doc
forall pf.
JustPropositional pf =>
Side -> PrettyLevel -> Rational -> pf -> Doc
prettyPropositional Side
RHS PrettyLevel
l (pf -> Precedence
forall x. HasFixity x => x -> Precedence
precedence pf
fm) pf
q
      ne :: pf -> Doc
ne pf
p = String -> Doc
text String
"¬" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Side -> PrettyLevel -> Rational -> pf -> Doc
forall pf.
JustPropositional pf =>
Side -> PrettyLevel -> Rational -> pf -> Doc
prettyPropositional Side
Unary PrettyLevel
l (pf -> Precedence
forall x. HasFixity x => x -> Precedence
precedence pf
fm) pf
p
      tf :: Bool -> Doc
tf Bool
x = Bool -> Doc
prettyBool Bool
x
      at :: AtomOf pf -> Doc
at AtomOf pf
x = PrettyLevel -> Rational -> AtomOf pf -> Doc
forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
l Rational
r AtomOf pf
x

-- | Implementation of 'show' for any 'JustPropositional' type.  For clarity, show methods fully parenthesize
showPropositional :: JustPropositional pf => Side -> Int -> pf -> ShowS
showPropositional :: forall pf. JustPropositional pf => Side -> Int -> pf -> ShowS
showPropositional Side
side Int
parentPrec pf
fm =
    Bool -> ShowS -> ShowS
showParen (Side -> Int -> Int -> Associativity -> Bool
forall a.
(Eq a, Ord a, Num a) =>
Side -> a -> a -> Associativity -> Bool
testParen Side
side Int
parentPrec (pf -> Precedence
forall x. HasFixity x => x -> Precedence
precedence pf
fm) (pf -> Associativity
forall x. HasFixity x => x -> Associativity
associativity pf
fm)) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ (pf -> BinOp -> pf -> ShowS)
-> (pf -> ShowS)
-> (Bool -> ShowS)
-> (AtomOf pf -> ShowS)
-> pf
-> ShowS
forall pf r.
JustPropositional pf =>
(pf -> BinOp -> pf -> r)
-> (pf -> r) -> (Bool -> r) -> (AtomOf pf -> r) -> pf -> r
foldPropositional pf -> BinOp -> pf -> ShowS
co pf -> ShowS
ne Bool -> ShowS
tf AtomOf pf -> ShowS
at pf
fm
    where
      co :: pf -> BinOp -> pf -> ShowS
co pf
p BinOp
(:&:) pf
q = Side -> Int -> pf -> ShowS
forall pf. JustPropositional pf => Side -> Int -> pf -> ShowS
showPropositional Side
LHS (pf -> Precedence
forall x. HasFixity x => x -> Precedence
precedence pf
fm) pf
p ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" .&. " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Side -> Int -> pf -> ShowS
forall pf. JustPropositional pf => Side -> Int -> pf -> ShowS
showPropositional Side
RHS (pf -> Precedence
forall x. HasFixity x => x -> Precedence
precedence pf
fm) pf
q
      co pf
p BinOp
(:|:) pf
q = Side -> Int -> pf -> ShowS
forall pf. JustPropositional pf => Side -> Int -> pf -> ShowS
showPropositional Side
LHS (pf -> Precedence
forall x. HasFixity x => x -> Precedence
precedence pf
fm) pf
p ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" .|. " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Side -> Int -> pf -> ShowS
forall pf. JustPropositional pf => Side -> Int -> pf -> ShowS
showPropositional Side
RHS (pf -> Precedence
forall x. HasFixity x => x -> Precedence
precedence pf
fm) pf
q
      co pf
p BinOp
(:=>:) pf
q = Side -> Int -> pf -> ShowS
forall pf. JustPropositional pf => Side -> Int -> pf -> ShowS
showPropositional Side
LHS (pf -> Precedence
forall x. HasFixity x => x -> Precedence
precedence pf
fm) pf
p ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" .=>. " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Side -> Int -> pf -> ShowS
forall pf. JustPropositional pf => Side -> Int -> pf -> ShowS
showPropositional Side
RHS (pf -> Precedence
forall x. HasFixity x => x -> Precedence
precedence pf
fm) pf
q
      co pf
p BinOp
(:<=>:) pf
q = Side -> Int -> pf -> ShowS
forall pf. JustPropositional pf => Side -> Int -> pf -> ShowS
showPropositional Side
LHS (pf -> Precedence
forall x. HasFixity x => x -> Precedence
precedence pf
fm) pf
p ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" .<=>. " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Side -> Int -> pf -> ShowS
forall pf. JustPropositional pf => Side -> Int -> pf -> ShowS
showPropositional Side
RHS (pf -> Precedence
forall x. HasFixity x => x -> Precedence
precedence pf
fm) pf
q
      ne :: pf -> ShowS
ne pf
p = String -> ShowS
showString String
"(.~.) " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Side -> Int -> pf -> ShowS
forall pf. JustPropositional pf => Side -> Int -> pf -> ShowS
showPropositional Side
Unary (Int -> Int
forall a. Enum a => a -> a
succ (pf -> Precedence
forall x. HasFixity x => x -> Precedence
precedence pf
fm)) pf
p
      tf :: Bool -> ShowS
tf Bool
x = Int -> Bool -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec (pf -> Precedence
forall x. HasFixity x => x -> Precedence
precedence pf
fm) Bool
x
      at :: AtomOf pf -> ShowS
at AtomOf pf
x = String -> ShowS
showString String
"atomic " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> AtomOf pf -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec (pf -> Precedence
forall x. HasFixity x => x -> Precedence
precedence pf
fm) AtomOf pf
x

-- | Implementation of 'onatoms' for any 'JustPropositional' type.
onatomsPropositional :: JustPropositional pf => (AtomOf pf -> AtomOf pf) -> pf -> pf
onatomsPropositional :: forall pf.
JustPropositional pf =>
(AtomOf pf -> AtomOf pf) -> pf -> pf
onatomsPropositional AtomOf pf -> AtomOf pf
f pf
fm =
    (pf -> BinOp -> pf -> pf)
-> (pf -> pf) -> (Bool -> pf) -> (AtomOf pf -> pf) -> pf -> pf
forall pf r.
JustPropositional pf =>
(pf -> BinOp -> pf -> r)
-> (pf -> r) -> (Bool -> r) -> (AtomOf pf -> r) -> pf -> r
foldPropositional pf -> BinOp -> pf -> pf
co pf -> pf
ne Bool -> pf
forall formula. IsFormula formula => Bool -> formula
tf AtomOf pf -> pf
at pf
fm
    where
      co :: pf -> BinOp -> pf -> pf
co pf
p BinOp
op pf
q = pf -> BinOp -> pf -> pf
forall formula.
IsPropositional formula =>
formula -> BinOp -> formula -> formula
binop ((AtomOf pf -> AtomOf pf) -> pf -> pf
forall pf.
JustPropositional pf =>
(AtomOf pf -> AtomOf pf) -> pf -> pf
onatomsPropositional AtomOf pf -> AtomOf pf
f pf
p) BinOp
op ((AtomOf pf -> AtomOf pf) -> pf -> pf
forall pf.
JustPropositional pf =>
(AtomOf pf -> AtomOf pf) -> pf -> pf
onatomsPropositional AtomOf pf -> AtomOf pf
f pf
q)
      ne :: pf -> pf
ne pf
p = pf -> pf
forall formula. IsLiteral formula => formula -> formula
(.~.) ((AtomOf pf -> AtomOf pf) -> pf -> pf
forall pf.
JustPropositional pf =>
(AtomOf pf -> AtomOf pf) -> pf -> pf
onatomsPropositional AtomOf pf -> AtomOf pf
f pf
p)
      tf :: Bool -> formula
tf Bool
flag = Bool -> formula
forall formula. IsFormula formula => Bool -> formula
fromBool Bool
flag
      at :: AtomOf pf -> pf
at AtomOf pf
x = AtomOf pf -> pf
forall formula. IsFormula formula => AtomOf formula -> formula
atomic (AtomOf pf -> AtomOf pf
f AtomOf pf
x)

-- | Implementation of 'overatoms' for any 'JustPropositional' type.
overatomsPropositional :: JustPropositional pf => (AtomOf pf -> r -> r) -> pf -> r -> r
overatomsPropositional :: forall pf r.
JustPropositional pf =>
(AtomOf pf -> r -> r) -> pf -> r -> r
overatomsPropositional AtomOf pf -> r -> r
f pf
fof r
r0 =
    (pf -> BinOp -> pf -> r)
-> (pf -> r) -> (Bool -> r) -> (AtomOf pf -> r) -> pf -> r
forall pf r.
JustPropositional pf =>
(pf -> BinOp -> pf -> r)
-> (pf -> r) -> (Bool -> r) -> (AtomOf pf -> r) -> pf -> r
foldPropositional pf -> BinOp -> pf -> r
co pf -> r
ne (r -> Bool -> r
forall a b. a -> b -> a
const r
r0) ((AtomOf pf -> r -> r) -> r -> AtomOf pf -> r
forall a b c. (a -> b -> c) -> b -> a -> c
flip AtomOf pf -> r -> r
f r
r0) pf
fof
    where
      co :: pf -> BinOp -> pf -> r
co pf
p BinOp
_ pf
q = (AtomOf pf -> r -> r) -> pf -> r -> r
forall pf r.
JustPropositional pf =>
(AtomOf pf -> r -> r) -> pf -> r -> r
overatomsPropositional AtomOf pf -> r -> r
f pf
p ((AtomOf pf -> r -> r) -> pf -> r -> r
forall pf r.
JustPropositional pf =>
(AtomOf pf -> r -> r) -> pf -> r -> r
overatomsPropositional AtomOf pf -> r -> r
f pf
q r
r0)
      ne :: pf -> r
ne pf
fof' = (AtomOf pf -> r -> r) -> pf -> r -> r
forall pf r.
JustPropositional pf =>
(AtomOf pf -> r -> r) -> pf -> r -> r
overatomsPropositional AtomOf pf -> r -> r
f pf
fof' r
r0

-- | An instance of IsPredicate.
data Prop = P {Prop -> String
pname :: String} deriving (Prop -> Prop -> Bool
(Prop -> Prop -> Bool) -> (Prop -> Prop -> Bool) -> Eq Prop
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Prop -> Prop -> Bool
== :: Prop -> Prop -> Bool
$c/= :: Prop -> Prop -> Bool
/= :: Prop -> Prop -> Bool
Eq, Eq Prop
Eq Prop =>
(Prop -> Prop -> Ordering)
-> (Prop -> Prop -> Bool)
-> (Prop -> Prop -> Bool)
-> (Prop -> Prop -> Bool)
-> (Prop -> Prop -> Bool)
-> (Prop -> Prop -> Prop)
-> (Prop -> Prop -> Prop)
-> Ord Prop
Prop -> Prop -> Bool
Prop -> Prop -> Ordering
Prop -> Prop -> Prop
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Prop -> Prop -> Ordering
compare :: Prop -> Prop -> Ordering
$c< :: Prop -> Prop -> Bool
< :: Prop -> Prop -> Bool
$c<= :: Prop -> Prop -> Bool
<= :: Prop -> Prop -> Bool
$c> :: Prop -> Prop -> Bool
> :: Prop -> Prop -> Bool
$c>= :: Prop -> Prop -> Bool
>= :: Prop -> Prop -> Bool
$cmax :: Prop -> Prop -> Prop
max :: Prop -> Prop -> Prop
$cmin :: Prop -> Prop -> Prop
min :: Prop -> Prop -> Prop
Ord)

-- Because of the IsString instance, the Show instance can just be a String.
instance Show Prop where
    show :: Prop -> String
show (P {pname :: Prop -> String
pname = String
s}) = ShowS
forall a. Show a => a -> String
show String
s

instance IsAtom Prop

-- Allows us to say "q" instead of P "q" or P {pname = "q"}
instance IsString Prop where
    fromString :: String -> Prop
fromString = String -> Prop
P

instance Pretty Prop where
    pPrint :: Prop -> Doc
pPrint = String -> Doc
text (String -> Doc) -> (Prop -> String) -> Prop -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Prop -> String
pname

instance HasFixity Prop where
    precedence :: Prop -> Precedence
precedence (P String
_) = a
Precedence
leafPrec

-- | An instance of IsPropositional.
data PFormula atom
    = F
    | T
    | Atom atom
    | Not (PFormula atom)
    | And (PFormula atom) (PFormula atom)
    | Or (PFormula atom) (PFormula atom)
    | Imp (PFormula atom) (PFormula atom)
    | Iff (PFormula atom) (PFormula atom)
    deriving (PFormula atom -> PFormula atom -> Bool
(PFormula atom -> PFormula atom -> Bool)
-> (PFormula atom -> PFormula atom -> Bool) -> Eq (PFormula atom)
forall atom. Eq atom => PFormula atom -> PFormula atom -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall atom. Eq atom => PFormula atom -> PFormula atom -> Bool
== :: PFormula atom -> PFormula atom -> Bool
$c/= :: forall atom. Eq atom => PFormula atom -> PFormula atom -> Bool
/= :: PFormula atom -> PFormula atom -> Bool
Eq, Eq (PFormula atom)
Eq (PFormula atom) =>
(PFormula atom -> PFormula atom -> Ordering)
-> (PFormula atom -> PFormula atom -> Bool)
-> (PFormula atom -> PFormula atom -> Bool)
-> (PFormula atom -> PFormula atom -> Bool)
-> (PFormula atom -> PFormula atom -> Bool)
-> (PFormula atom -> PFormula atom -> PFormula atom)
-> (PFormula atom -> PFormula atom -> PFormula atom)
-> Ord (PFormula atom)
PFormula atom -> PFormula atom -> Bool
PFormula atom -> PFormula atom -> Ordering
PFormula atom -> PFormula atom -> PFormula atom
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall atom. Ord atom => Eq (PFormula atom)
forall atom. Ord atom => PFormula atom -> PFormula atom -> Bool
forall atom. Ord atom => PFormula atom -> PFormula atom -> Ordering
forall atom.
Ord atom =>
PFormula atom -> PFormula atom -> PFormula atom
$ccompare :: forall atom. Ord atom => PFormula atom -> PFormula atom -> Ordering
compare :: PFormula atom -> PFormula atom -> Ordering
$c< :: forall atom. Ord atom => PFormula atom -> PFormula atom -> Bool
< :: PFormula atom -> PFormula atom -> Bool
$c<= :: forall atom. Ord atom => PFormula atom -> PFormula atom -> Bool
<= :: PFormula atom -> PFormula atom -> Bool
$c> :: forall atom. Ord atom => PFormula atom -> PFormula atom -> Bool
> :: PFormula atom -> PFormula atom -> Bool
$c>= :: forall atom. Ord atom => PFormula atom -> PFormula atom -> Bool
>= :: PFormula atom -> PFormula atom -> Bool
$cmax :: forall atom.
Ord atom =>
PFormula atom -> PFormula atom -> PFormula atom
max :: PFormula atom -> PFormula atom -> PFormula atom
$cmin :: forall atom.
Ord atom =>
PFormula atom -> PFormula atom -> PFormula atom
min :: PFormula atom -> PFormula atom -> PFormula atom
Ord, ReadPrec [PFormula atom]
ReadPrec (PFormula atom)
Int -> ReadS (PFormula atom)
ReadS [PFormula atom]
(Int -> ReadS (PFormula atom))
-> ReadS [PFormula atom]
-> ReadPrec (PFormula atom)
-> ReadPrec [PFormula atom]
-> Read (PFormula atom)
forall atom. Read atom => ReadPrec [PFormula atom]
forall atom. Read atom => ReadPrec (PFormula atom)
forall atom. Read atom => Int -> ReadS (PFormula atom)
forall atom. Read atom => ReadS [PFormula atom]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: forall atom. Read atom => Int -> ReadS (PFormula atom)
readsPrec :: Int -> ReadS (PFormula atom)
$creadList :: forall atom. Read atom => ReadS [PFormula atom]
readList :: ReadS [PFormula atom]
$creadPrec :: forall atom. Read atom => ReadPrec (PFormula atom)
readPrec :: ReadPrec (PFormula atom)
$creadListPrec :: forall atom. Read atom => ReadPrec [PFormula atom]
readListPrec :: ReadPrec [PFormula atom]
Read, Typeable (PFormula atom)
Typeable (PFormula atom) =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> PFormula atom -> c (PFormula atom))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (PFormula atom))
-> (PFormula atom -> Constr)
-> (PFormula atom -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (PFormula atom)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (PFormula atom)))
-> ((forall b. Data b => b -> b) -> PFormula atom -> PFormula atom)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> PFormula atom -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> PFormula atom -> r)
-> (forall u. (forall d. Data d => d -> u) -> PFormula atom -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> PFormula atom -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> PFormula atom -> m (PFormula atom))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> PFormula atom -> m (PFormula atom))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> PFormula atom -> m (PFormula atom))
-> Data (PFormula atom)
PFormula atom -> Constr
PFormula atom -> DataType
(forall b. Data b => b -> b) -> PFormula atom -> PFormula atom
forall atom. Data atom => Typeable (PFormula atom)
forall atom. Data atom => PFormula atom -> Constr
forall atom. Data atom => PFormula atom -> DataType
forall atom.
Data atom =>
(forall b. Data b => b -> b) -> PFormula atom -> PFormula atom
forall atom u.
Data atom =>
Int -> (forall d. Data d => d -> u) -> PFormula atom -> u
forall atom u.
Data atom =>
(forall d. Data d => d -> u) -> PFormula atom -> [u]
forall atom r r'.
Data atom =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PFormula atom -> r
forall atom r r'.
Data atom =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PFormula atom -> r
forall atom (m :: * -> *).
(Data atom, Monad m) =>
(forall d. Data d => d -> m d)
-> PFormula atom -> m (PFormula atom)
forall atom (m :: * -> *).
(Data atom, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> PFormula atom -> m (PFormula atom)
forall atom (c :: * -> *).
Data atom =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (PFormula atom)
forall atom (c :: * -> *).
Data atom =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PFormula atom -> c (PFormula atom)
forall atom (t :: * -> *) (c :: * -> *).
(Data atom, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (PFormula atom))
forall atom (t :: * -> * -> *) (c :: * -> *).
(Data atom, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (PFormula atom))
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> PFormula atom -> u
forall u. (forall d. Data d => d -> u) -> PFormula atom -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PFormula atom -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PFormula atom -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> PFormula atom -> m (PFormula atom)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> PFormula atom -> m (PFormula atom)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (PFormula atom)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PFormula atom -> c (PFormula atom)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (PFormula atom))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (PFormula atom))
$cgfoldl :: forall atom (c :: * -> *).
Data atom =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PFormula atom -> c (PFormula atom)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PFormula atom -> c (PFormula atom)
$cgunfold :: forall atom (c :: * -> *).
Data atom =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (PFormula atom)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (PFormula atom)
$ctoConstr :: forall atom. Data atom => PFormula atom -> Constr
toConstr :: PFormula atom -> Constr
$cdataTypeOf :: forall atom. Data atom => PFormula atom -> DataType
dataTypeOf :: PFormula atom -> DataType
$cdataCast1 :: forall atom (t :: * -> *) (c :: * -> *).
(Data atom, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (PFormula atom))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (PFormula atom))
$cdataCast2 :: forall atom (t :: * -> * -> *) (c :: * -> *).
(Data atom, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (PFormula atom))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (PFormula atom))
$cgmapT :: forall atom.
Data atom =>
(forall b. Data b => b -> b) -> PFormula atom -> PFormula atom
gmapT :: (forall b. Data b => b -> b) -> PFormula atom -> PFormula atom
$cgmapQl :: forall atom r r'.
Data atom =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PFormula atom -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PFormula atom -> r
$cgmapQr :: forall atom r r'.
Data atom =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PFormula atom -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PFormula atom -> r
$cgmapQ :: forall atom u.
Data atom =>
(forall d. Data d => d -> u) -> PFormula atom -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> PFormula atom -> [u]
$cgmapQi :: forall atom u.
Data atom =>
Int -> (forall d. Data d => d -> u) -> PFormula atom -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> PFormula atom -> u
$cgmapM :: forall atom (m :: * -> *).
(Data atom, Monad m) =>
(forall d. Data d => d -> m d)
-> PFormula atom -> m (PFormula atom)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> PFormula atom -> m (PFormula atom)
$cgmapMp :: forall atom (m :: * -> *).
(Data atom, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> PFormula atom -> m (PFormula atom)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> PFormula atom -> m (PFormula atom)
$cgmapMo :: forall atom (m :: * -> *).
(Data atom, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> PFormula atom -> m (PFormula atom)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> PFormula atom -> m (PFormula atom)
Data, Typeable)

-- Build a Haskell expression for this formula
instance (IsPropositional (PFormula atom), Show atom) => Show (PFormula atom) where
    showsPrec :: Int -> PFormula atom -> ShowS
showsPrec Int
p PFormula atom
x = Side -> Int -> PFormula atom -> ShowS
forall pf. JustPropositional pf => Side -> Int -> pf -> ShowS
showPropositional Side
Top Int
p PFormula atom
x -- . showString " :: PFormula Prop"

instance IsAtom atom => HasFixity (PFormula atom) where
    precedence :: PFormula atom -> Precedence
precedence = PFormula atom -> a
PFormula atom -> Precedence
forall pf. JustPropositional pf => pf -> Precedence
precedencePropositional
    associativity :: PFormula atom -> Associativity
associativity = PFormula atom -> Associativity
forall pf. JustPropositional pf => pf -> Associativity
associativityPropositional

instance IsAtom atom => IsFormula (PFormula atom) where
    type AtomOf (PFormula atom) = atom
    asBool :: PFormula atom -> Maybe Bool
asBool PFormula atom
T = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
    asBool PFormula atom
F = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
    asBool PFormula atom
_ = Maybe Bool
forall a. Maybe a
Nothing
    true :: PFormula atom
true = PFormula atom
forall atom. PFormula atom
T
    false :: PFormula atom
false = PFormula atom
forall atom. PFormula atom
F
    atomic :: AtomOf (PFormula atom) -> PFormula atom
atomic = atom -> PFormula atom
AtomOf (PFormula atom) -> PFormula atom
forall atom. atom -> PFormula atom
Atom
    overatoms :: forall r.
(AtomOf (PFormula atom) -> r -> r) -> PFormula atom -> r -> r
overatoms = (AtomOf (PFormula atom) -> r -> r) -> PFormula atom -> r -> r
forall pf r.
JustPropositional pf =>
(AtomOf pf -> r -> r) -> pf -> r -> r
overatomsPropositional
    onatoms :: (AtomOf (PFormula atom) -> AtomOf (PFormula atom))
-> PFormula atom -> PFormula atom
onatoms = (AtomOf (PFormula atom) -> AtomOf (PFormula atom))
-> PFormula atom -> PFormula atom
forall pf.
JustPropositional pf =>
(AtomOf pf -> AtomOf pf) -> pf -> pf
onatomsPropositional

instance IsAtom atom => IsPropositional (PFormula atom) where
    .|. :: PFormula atom -> PFormula atom -> PFormula atom
(.|.) = PFormula atom -> PFormula atom -> PFormula atom
forall atom. PFormula atom -> PFormula atom -> PFormula atom
Or
    .&. :: PFormula atom -> PFormula atom -> PFormula atom
(.&.) = PFormula atom -> PFormula atom -> PFormula atom
forall atom. PFormula atom -> PFormula atom -> PFormula atom
And
    .=>. :: PFormula atom -> PFormula atom -> PFormula atom
(.=>.) = PFormula atom -> PFormula atom -> PFormula atom
forall atom. PFormula atom -> PFormula atom -> PFormula atom
Imp
    .<=>. :: PFormula atom -> PFormula atom -> PFormula atom
(.<=>.) = PFormula atom -> PFormula atom -> PFormula atom
forall atom. PFormula atom -> PFormula atom -> PFormula atom
Iff
    foldPropositional' :: forall r.
(PFormula atom -> r)
-> (PFormula atom -> BinOp -> PFormula atom -> r)
-> (PFormula atom -> r)
-> (Bool -> r)
-> (AtomOf (PFormula atom) -> r)
-> PFormula atom
-> r
foldPropositional' PFormula atom -> r
_ PFormula atom -> BinOp -> PFormula atom -> r
co PFormula atom -> r
ne Bool -> r
tf AtomOf (PFormula atom) -> r
at PFormula atom
fm =
        case PFormula atom
fm of
          Imp PFormula atom
p PFormula atom
q -> PFormula atom -> BinOp -> PFormula atom -> r
co PFormula atom
p BinOp
(:=>:) PFormula atom
q
          Iff PFormula atom
p PFormula atom
q -> PFormula atom -> BinOp -> PFormula atom -> r
co PFormula atom
p BinOp
(:<=>:) PFormula atom
q
          And PFormula atom
p PFormula atom
q -> PFormula atom -> BinOp -> PFormula atom -> r
co PFormula atom
p BinOp
(:&:) PFormula atom
q
          Or PFormula atom
p PFormula atom
q -> PFormula atom -> BinOp -> PFormula atom -> r
co PFormula atom
p BinOp
(:|:) PFormula atom
q
          PFormula atom
_ -> (PFormula atom -> r)
-> (PFormula atom -> r)
-> (Bool -> r)
-> (AtomOf (PFormula atom) -> r)
-> PFormula atom
-> r
forall lit r.
IsLiteral lit =>
(lit -> r)
-> (lit -> r) -> (Bool -> r) -> (AtomOf lit -> r) -> lit -> r
forall r.
(PFormula atom -> r)
-> (PFormula atom -> r)
-> (Bool -> r)
-> (AtomOf (PFormula atom) -> r)
-> PFormula atom
-> r
foldLiteral' (String -> PFormula atom -> r
forall a. HasCallStack => String -> a
error String
"IsPropositional PFormula") PFormula atom -> r
ne Bool -> r
tf AtomOf (PFormula atom) -> r
at PFormula atom
fm
    foldCombination :: forall r.
(PFormula atom -> r)
-> (PFormula atom -> PFormula atom -> r)
-> (PFormula atom -> PFormula atom -> r)
-> (PFormula atom -> PFormula atom -> r)
-> (PFormula atom -> PFormula atom -> r)
-> PFormula atom
-> r
foldCombination PFormula atom -> r
other PFormula atom -> PFormula atom -> r
dj PFormula atom -> PFormula atom -> r
cj PFormula atom -> PFormula atom -> r
imp PFormula atom -> PFormula atom -> r
iff PFormula atom
fm =
        case PFormula atom
fm of
          Or PFormula atom
a PFormula atom
b -> PFormula atom
a PFormula atom -> PFormula atom -> r
`dj` PFormula atom
b
          And PFormula atom
a PFormula atom
b -> PFormula atom
a PFormula atom -> PFormula atom -> r
`cj` PFormula atom
b
          Imp PFormula atom
a PFormula atom
b -> PFormula atom
a PFormula atom -> PFormula atom -> r
`imp` PFormula atom
b
          Iff PFormula atom
a PFormula atom
b -> PFormula atom
a PFormula atom -> PFormula atom -> r
`iff` PFormula atom
b
          PFormula atom
_ -> PFormula atom -> r
other PFormula atom
fm

instance IsAtom atom => IsLiteral (PFormula atom) where
    naiveNegate :: PFormula atom -> PFormula atom
naiveNegate = PFormula atom -> PFormula atom
forall atom. PFormula atom -> PFormula atom
Not
    foldNegation :: forall r.
(PFormula atom -> r) -> (PFormula atom -> r) -> PFormula atom -> r
foldNegation PFormula atom -> r
normal PFormula atom -> r
inverted (Not PFormula atom
x) = (PFormula atom -> r) -> (PFormula atom -> r) -> PFormula atom -> r
forall lit r. IsLiteral lit => (lit -> r) -> (lit -> r) -> lit -> r
forall r.
(PFormula atom -> r) -> (PFormula atom -> r) -> PFormula atom -> r
foldNegation PFormula atom -> r
inverted PFormula atom -> r
normal PFormula atom
x
    foldNegation PFormula atom -> r
normal PFormula atom -> r
_ PFormula atom
x = PFormula atom -> r
normal PFormula atom
x
    foldLiteral' :: forall r.
(PFormula atom -> r)
-> (PFormula atom -> r)
-> (Bool -> r)
-> (AtomOf (PFormula atom) -> r)
-> PFormula atom
-> r
foldLiteral' PFormula atom -> r
ho PFormula atom -> r
ne Bool -> r
tf AtomOf (PFormula atom) -> r
at PFormula atom
fm =
        case PFormula atom
fm of
          PFormula atom
T -> Bool -> r
tf Bool
True
          PFormula atom
F -> Bool -> r
tf Bool
False
          Atom atom
a -> AtomOf (PFormula atom) -> r
at atom
AtomOf (PFormula atom)
a
          Not PFormula atom
l -> PFormula atom -> r
ne PFormula atom
l
          PFormula atom
_ -> PFormula atom -> r
ho PFormula atom
fm

instance IsAtom atom => Pretty (PFormula atom) where
    pPrintPrec :: PrettyLevel -> Rational -> PFormula atom -> Doc
pPrintPrec = Side -> PrettyLevel -> Rational -> PFormula atom -> Doc
forall pf.
JustPropositional pf =>
Side -> PrettyLevel -> Rational -> pf -> Doc
prettyPropositional Side
Top

-- | Class that indicates a formula type *only* supports Propositional
-- features - it has no way to represent quantifiers.
class IsPropositional formula => JustPropositional formula

instance IsAtom atom => JustPropositional (PFormula atom)

-- | Interpretation of formulas.
eval :: JustPropositional pf => pf -> (AtomOf pf -> Bool) -> Bool
eval :: forall pf.
JustPropositional pf =>
pf -> (AtomOf pf -> Bool) -> Bool
eval pf
fm AtomOf pf -> Bool
v =
    (pf -> BinOp -> pf -> Bool)
-> (pf -> Bool)
-> (Bool -> Bool)
-> (AtomOf pf -> Bool)
-> pf
-> Bool
forall pf r.
JustPropositional pf =>
(pf -> BinOp -> pf -> r)
-> (pf -> r) -> (Bool -> r) -> (AtomOf pf -> r) -> pf -> r
foldPropositional pf -> BinOp -> pf -> Bool
co pf -> Bool
ne Bool -> Bool
forall {a}. a -> a
tf AtomOf pf -> Bool
at pf
fm
    where
      co :: pf -> BinOp -> pf -> Bool
co pf
p BinOp
(:&:) pf
q = (pf -> (AtomOf pf -> Bool) -> Bool
forall pf.
JustPropositional pf =>
pf -> (AtomOf pf -> Bool) -> Bool
eval pf
p AtomOf pf -> Bool
v) Bool -> Bool -> Bool
&& (pf -> (AtomOf pf -> Bool) -> Bool
forall pf.
JustPropositional pf =>
pf -> (AtomOf pf -> Bool) -> Bool
eval pf
q AtomOf pf -> Bool
v)
      co pf
p BinOp
(:|:) pf
q = (pf -> (AtomOf pf -> Bool) -> Bool
forall pf.
JustPropositional pf =>
pf -> (AtomOf pf -> Bool) -> Bool
eval pf
p AtomOf pf -> Bool
v) Bool -> Bool -> Bool
|| (pf -> (AtomOf pf -> Bool) -> Bool
forall pf.
JustPropositional pf =>
pf -> (AtomOf pf -> Bool) -> Bool
eval pf
q AtomOf pf -> Bool
v)
      co pf
p BinOp
(:=>:) pf
q = Bool -> Bool
not (pf -> (AtomOf pf -> Bool) -> Bool
forall pf.
JustPropositional pf =>
pf -> (AtomOf pf -> Bool) -> Bool
eval pf
p AtomOf pf -> Bool
v) Bool -> Bool -> Bool
|| (pf -> (AtomOf pf -> Bool) -> Bool
forall pf.
JustPropositional pf =>
pf -> (AtomOf pf -> Bool) -> Bool
eval pf
q AtomOf pf -> Bool
v)
      co pf
p BinOp
(:<=>:) pf
q = (pf -> (AtomOf pf -> Bool) -> Bool
forall pf.
JustPropositional pf =>
pf -> (AtomOf pf -> Bool) -> Bool
eval pf
p AtomOf pf -> Bool
v) Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== (pf -> (AtomOf pf -> Bool) -> Bool
forall pf.
JustPropositional pf =>
pf -> (AtomOf pf -> Bool) -> Bool
eval pf
q AtomOf pf -> Bool
v)
      ne :: pf -> Bool
ne pf
p = Bool -> Bool
not (pf -> (AtomOf pf -> Bool) -> Bool
forall pf.
JustPropositional pf =>
pf -> (AtomOf pf -> Bool) -> Bool
eval pf
p AtomOf pf -> Bool
v)
      tf :: a -> a
tf = a -> a
forall {a}. a -> a
id
      at :: AtomOf pf -> Bool
at = AtomOf pf -> Bool
v

-- | Recognizing tautologies.
tautology :: JustPropositional pf => pf -> Bool
tautology :: forall pf. JustPropositional pf => pf -> Bool
tautology pf
fm = (Bool -> Bool -> Bool)
-> ((AtomOf pf -> Bool) -> Bool)
-> (AtomOf pf -> Bool)
-> Set (AtomOf pf)
-> Bool
forall atom r.
Ord atom =>
(r -> r -> r)
-> ((atom -> Bool) -> r) -> (atom -> Bool) -> Set atom -> r
onallvaluations Bool -> Bool -> Bool
(&&) (pf -> (AtomOf pf -> Bool) -> Bool
forall pf.
JustPropositional pf =>
pf -> (AtomOf pf -> Bool) -> Bool
eval pf
fm) (\AtomOf pf
_s -> Bool
False) (pf -> Set (AtomOf pf)
forall formula.
IsFormula formula =>
formula -> Set (AtomOf formula)
atoms pf
fm)

-- | Related concepts.
unsatisfiable :: JustPropositional pf => pf -> Bool
unsatisfiable :: forall pf. JustPropositional pf => pf -> Bool
unsatisfiable = pf -> Bool
forall pf. JustPropositional pf => pf -> Bool
tautology (pf -> Bool) -> (pf -> pf) -> pf -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. pf -> pf
forall formula. IsLiteral formula => formula -> formula
(.~.)
satisfiable :: JustPropositional pf  => pf -> Bool
satisfiable :: forall pf. JustPropositional pf => pf -> Bool
satisfiable = Bool -> Bool
not (Bool -> Bool) -> (pf -> Bool) -> pf -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. pf -> Bool
forall pf. JustPropositional pf => pf -> Bool
unsatisfiable

onallvaluations :: Ord atom => (r -> r -> r) -> ((atom -> Bool) -> r) -> (atom -> Bool) -> Set atom -> r
onallvaluations :: forall atom r.
Ord atom =>
(r -> r -> r)
-> ((atom -> Bool) -> r) -> (atom -> Bool) -> Set atom -> r
onallvaluations r -> r -> r
cmb (atom -> Bool) -> r
subfn atom -> Bool
v Set atom
ats =
    case Set atom -> Maybe (atom, Set atom)
forall a. Set a -> Maybe (a, Set a)
minView Set atom
ats of
      Maybe (atom, Set atom)
Nothing -> (atom -> Bool) -> r
subfn atom -> Bool
v
      Just (atom
p, Set atom
ps) ->
          let v' :: Bool -> atom -> Bool
v' Bool
t atom
q = (if atom
q atom -> atom -> Bool
forall a. Eq a => a -> a -> Bool
== atom
p then Bool
t else atom -> Bool
v atom
q) in
          r -> r -> r
cmb ((r -> r -> r)
-> ((atom -> Bool) -> r) -> (atom -> Bool) -> Set atom -> r
forall atom r.
Ord atom =>
(r -> r -> r)
-> ((atom -> Bool) -> r) -> (atom -> Bool) -> Set atom -> r
onallvaluations r -> r -> r
cmb (atom -> Bool) -> r
subfn (Bool -> atom -> Bool
v' Bool
False) Set atom
ps) ((r -> r -> r)
-> ((atom -> Bool) -> r) -> (atom -> Bool) -> Set atom -> r
forall atom r.
Ord atom =>
(r -> r -> r)
-> ((atom -> Bool) -> r) -> (atom -> Bool) -> Set atom -> r
onallvaluations r -> r -> r
cmb (atom -> Bool) -> r
subfn (Bool -> atom -> Bool
v' Bool
True) Set atom
ps)

-- | Return the set of propositional variables in a formula.
atoms :: IsFormula formula => formula -> Set (AtomOf formula)
atoms :: forall formula.
IsFormula formula =>
formula -> Set (AtomOf formula)
atoms formula
fm = (AtomOf formula -> Set (AtomOf formula))
-> formula -> Set (AtomOf formula)
forall formula r.
(IsFormula formula, Ord r) =>
(AtomOf formula -> Set r) -> formula -> Set r
atom_union AtomOf formula -> Set (AtomOf formula)
forall a. a -> Set a
singleton formula
fm

data TruthTable a = TruthTable [a] [TruthTableRow] deriving (TruthTable a -> TruthTable a -> Bool
(TruthTable a -> TruthTable a -> Bool)
-> (TruthTable a -> TruthTable a -> Bool) -> Eq (TruthTable a)
forall a. Eq a => TruthTable a -> TruthTable a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => TruthTable a -> TruthTable a -> Bool
== :: TruthTable a -> TruthTable a -> Bool
$c/= :: forall a. Eq a => TruthTable a -> TruthTable a -> Bool
/= :: TruthTable a -> TruthTable a -> Bool
Eq, Int -> TruthTable a -> ShowS
[TruthTable a] -> ShowS
TruthTable a -> String
(Int -> TruthTable a -> ShowS)
-> (TruthTable a -> String)
-> ([TruthTable a] -> ShowS)
-> Show (TruthTable a)
forall a. Show a => Int -> TruthTable a -> ShowS
forall a. Show a => [TruthTable a] -> ShowS
forall a. Show a => TruthTable a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> TruthTable a -> ShowS
showsPrec :: Int -> TruthTable a -> ShowS
$cshow :: forall a. Show a => TruthTable a -> String
show :: TruthTable a -> String
$cshowList :: forall a. Show a => [TruthTable a] -> ShowS
showList :: [TruthTable a] -> ShowS
Show)
type TruthTableRow = ([Bool], Bool)

-- | Code to print out truth tables.
truthTable :: JustPropositional pf => pf -> TruthTable (AtomOf pf)
truthTable :: forall pf. JustPropositional pf => pf -> TruthTable (AtomOf pf)
truthTable pf
fm =
    [AtomOf pf] -> [TruthTableRow] -> TruthTable (AtomOf pf)
forall a. [a] -> [TruthTableRow] -> TruthTable a
TruthTable [AtomOf pf]
atl (([TruthTableRow] -> [TruthTableRow] -> [TruthTableRow])
-> ((AtomOf pf -> Bool) -> [TruthTableRow])
-> (AtomOf pf -> Bool)
-> Set (AtomOf pf)
-> [TruthTableRow]
forall atom r.
Ord atom =>
(r -> r -> r)
-> ((atom -> Bool) -> r) -> (atom -> Bool) -> Set atom -> r
onallvaluations [TruthTableRow] -> [TruthTableRow] -> [TruthTableRow]
forall a. Semigroup a => a -> a -> a
(<>) (AtomOf pf -> Bool) -> [TruthTableRow]
mkRow (Bool -> AtomOf pf -> Bool
forall a b. a -> b -> a
const Bool
False) Set (AtomOf pf)
ats)
    where
      ats :: Set (AtomOf pf)
ats = pf -> Set (AtomOf pf)
forall formula.
IsFormula formula =>
formula -> Set (AtomOf formula)
atoms pf
fm
      mkRow :: (AtomOf pf -> Bool) -> [TruthTableRow]
mkRow AtomOf pf -> Bool
v = [((AtomOf pf -> Bool) -> [AtomOf pf] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
List.map AtomOf pf -> Bool
v [AtomOf pf]
atl, pf -> (AtomOf pf -> Bool) -> Bool
forall pf.
JustPropositional pf =>
pf -> (AtomOf pf -> Bool) -> Bool
eval pf
fm AtomOf pf -> Bool
v)]
      atl :: [AtomOf pf]
atl = Set (AtomOf pf) -> [AtomOf pf]
forall a. Set a -> [a]
Set.toAscList Set (AtomOf pf)
ats

instance Pretty atom => Pretty (TruthTable atom) where
    pPrint :: TruthTable atom -> Doc
pPrint (TruthTable [atom]
ats [TruthTableRow]
rows) = [Doc] -> Doc
vcat (([String] -> Doc) -> [[String]] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
List.map (String -> Doc
text (String -> Doc) -> ([String] -> String) -> [String] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"|" ([String] -> String)
-> ([String] -> [String]) -> [String] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> [String]
center) [[String]]
rows'')
        where
          center :: [String] -> [String]
          center :: [String] -> [String]
center [String]
cols = ((Int, String) -> String) -> [(Int, String)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
Prelude.map ((Int -> ShowS) -> (Int, String) -> String
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Int -> ShowS
center') ([Int] -> [String] -> [(Int, String)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
colWidths [String]
cols)
          center' :: Int -> String -> String
          center' :: Int -> ShowS
center' Int
width String
s = let (Int
q, Int
r) = Int -> Int -> (Int, Int)
forall a. Integral a => a -> a -> (a, a)
divMod (Int
width Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
s) Int
2 in Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
q Char
' ' String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Int
q Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
r) Char
' '
          hdrs :: [String]
hdrs = (atom -> String) -> [atom] -> [String]
forall a b. (a -> b) -> [a] -> [b]
List.map atom -> String
forall a. Pretty a => a -> String
prettyShow [atom]
ats [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
"result"]
          rows'' :: [[String]]
rows'' = [String]
hdrs [String] -> [[String]] -> [[String]]
forall a. a -> [a] -> [a]
: ((Int, Char) -> String) -> [(Int, Char)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
List.map ((Int -> Char -> String) -> (Int, Char) -> String
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Int -> Char -> String
forall a. Int -> a -> [a]
replicate) ([Int] -> String -> [(Int, Char)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
colWidths (Char -> String
forall a. a -> [a]
repeat Char
'-')) [String] -> [[String]] -> [[String]]
forall a. a -> [a] -> [a]
: [[String]]
rows'
          rows' :: [[String]]
          rows' :: [[String]]
rows' = (TruthTableRow -> [String]) -> [TruthTableRow] -> [[String]]
forall a b. (a -> b) -> [a] -> [b]
List.map (\([Bool]
cols, Bool
result) -> (Bool -> String) -> [Bool] -> [String]
forall a b. (a -> b) -> [a] -> [b]
List.map Bool -> String
forall a. Pretty a => a -> String
prettyShow ([Bool]
cols [Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++ [Bool
result])) [TruthTableRow]
rows
          cellWidths :: [[Int]]
          cellWidths :: [[Int]]
cellWidths = ([String] -> [Int]) -> [[String]] -> [[Int]]
forall a b. (a -> b) -> [a] -> [b]
List.map ((String -> Int) -> [String] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
List.map String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length) ([String]
hdrs [String] -> [[String]] -> [[String]]
forall a. a -> [a] -> [a]
: [[String]]
rows')
          colWidths :: [Int]
          colWidths :: [Int]
colWidths = ([Int] -> Int) -> [[Int]] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
List.map ((Int -> Int -> Int) -> [Int] -> Int
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 Int -> Int -> Int
forall a. Ord a => a -> a -> a
max) ([[Int]] -> [[Int]]
forall a. [[a]] -> [[a]]
transpose [[Int]]
cellWidths)

transpose               :: [[a]] -> [[a]]
transpose :: forall a. [[a]] -> [[a]]
transpose []             = []
transpose ([]   : [[a]]
xss)   = [[a]] -> [[a]]
forall a. [[a]] -> [[a]]
transpose [[a]]
xss
transpose ((a
x:[a]
xs) : [[a]]
xss) = (a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a
h | (a
h:[a]
_) <- [[a]]
xss]) [a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
: [[a]] -> [[a]]
forall a. [[a]] -> [[a]]
transpose ([a]
xs [a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
: [ [a]
t | (a
_:[a]
t) <- [[a]]
xss])

-- | Make sure the precedence and associativity implied by the Haskell
-- infix/infixl/infixr declarations matches the precedence and
-- associativity implied by the HasFixity instances.  It would be nice
-- to define one in terms of the other, but I don't know how to query
-- the precedence and associativity of an operator, and I don't know
-- how to (successfully) generate an infix/infixl/infixr declaration
-- using template haskell (the obvious thing didn't work:
--
--    $(pure [InfixD (Fixity quantPrec TH.InfixR) '(∀)])

-- | Tests precedence handling in pretty
-- printer.  1. Need to test: associativity of like operators
-- 2. precedence of every pair of adjacent operators 3. Stuff about
-- infix operators
test00 :: Test
test00 :: Test
test00 =
{-
    TestList [testPrecedence, testAssociativity]
    where
      testPrecedence :: Test
      testPrecedence =
          TestList (
-}
    [Test] -> Test
TestList (((PFormula Prop, String) -> Test)
-> [(PFormula Prop, String)] -> [Test]
forall a b. (a -> b) -> [a] -> [b]
List.map (\(PFormula Prop
input, String
expected) -> Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> Doc -> Doc -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"precedence" (String -> Doc
text String
expected) (PFormula Prop -> Doc
forall a. Pretty a => a -> Doc
pPrint PFormula Prop
input))
                      [( PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop
q PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. PFormula Prop
r)   , String
"p∧(q∨r)" ),
                       ( (PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
q) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. PFormula Prop
r   , String
"(p∧q)∨r" ),
                       ( PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
q PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. PFormula Prop
r     , String
"(p∧q)∨r" ),
                       ( PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. PFormula Prop
q PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
r     , String
"p∨(q∧r)" ),
                       ( PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
q PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
r     , String
"p∧q∧r"   ),
                       ( PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. PFormula Prop
q PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. PFormula Prop
r     , String
"p∨q∨r"   ),
                       ( (PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. PFormula Prop
q) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. PFormula Prop
r , String
"(p⇒q)⇒r" ),
                       ( PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. (PFormula Prop
q PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. PFormula Prop
r) , String
"p⇒q⇒r"   ),
                       ( PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. PFormula Prop
q PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. PFormula Prop
r   , String
"p⇒q⇒r"   )])
    where
      byPrec :: IsPropositional formula => [[(Rational, formula -> formula -> formula)]]
      byPrec :: forall formula.
IsPropositional formula =>
[[(Rational, formula -> formula -> formula)]]
byPrec = ((Rational, formula -> formula -> formula)
 -> (Rational, formula -> formula -> formula) -> Bool)
-> [(Rational, formula -> formula -> formula)]
-> [[(Rational, formula -> formula -> formula)]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Rational -> Rational -> Bool)
-> ((Rational, formula -> formula -> formula) -> Rational)
-> (Rational, formula -> formula -> formula)
-> (Rational, formula -> formula -> formula)
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Rational, formula -> formula -> formula) -> Rational
forall a b. (a, b) -> a
fst) ([(Rational, formula -> formula -> formula)]
 -> [[(Rational, formula -> formula -> formula)]])
-> ([(Rational, formula -> formula -> formula)]
    -> [(Rational, formula -> formula -> formula)])
-> [(Rational, formula -> formula -> formula)]
-> [[(Rational, formula -> formula -> formula)]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Rational, formula -> formula -> formula)
 -> (Rational, formula -> formula -> formula) -> Ordering)
-> [(Rational, formula -> formula -> formula)]
-> [(Rational, formula -> formula -> formula)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (Rational -> Rational -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Rational -> Rational -> Ordering)
-> ((Rational, formula -> formula -> formula) -> Rational)
-> (Rational, formula -> formula -> formula)
-> (Rational, formula -> formula -> formula)
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Rational, formula -> formula -> formula) -> Rational
forall a b. (a, b) -> a
fst) ([(Rational, formula -> formula -> formula)]
 -> [[(Rational, formula -> formula -> formula)]])
-> [(Rational, formula -> formula -> formula)]
-> [[(Rational, formula -> formula -> formula)]]
forall a b. (a -> b) -> a -> b
$ [(Rational, formula -> formula -> formula)]
forall formula.
IsPropositional formula =>
[(Rational, formula -> formula -> formula)]
binops
      -- All the operators we will test, with the 'Precedence' value
      -- we assigned.  we need to make sure the 'Precedence' value
      -- matches the values in the infix/infixl/infixr declarations.
      binops :: IsPropositional formula => [(Rational, formula -> formula -> formula)]
      binops :: forall formula.
IsPropositional formula =>
[(Rational, formula -> formula -> formula)]
binops = [(Rational, formula -> formula -> formula)]
forall formula.
IsPropositional formula =>
[(Rational, formula -> formula -> formula)]
ands [(Rational, formula -> formula -> formula)]
-> [(Rational, formula -> formula -> formula)]
-> [(Rational, formula -> formula -> formula)]
forall a. [a] -> [a] -> [a]
++ [(Rational, formula -> formula -> formula)]
forall formula.
IsPropositional formula =>
[(Rational, formula -> formula -> formula)]
ors [(Rational, formula -> formula -> formula)]
-> [(Rational, formula -> formula -> formula)]
-> [(Rational, formula -> formula -> formula)]
forall a. [a] -> [a] -> [a]
++ [(Rational, formula -> formula -> formula)]
forall formula.
IsPropositional formula =>
[(Rational, formula -> formula -> formula)]
imps [(Rational, formula -> formula -> formula)]
-> [(Rational, formula -> formula -> formula)]
-> [(Rational, formula -> formula -> formula)]
forall a. [a] -> [a] -> [a]
++ [(Rational, formula -> formula -> formula)]
forall formula.
IsPropositional formula =>
[(Rational, formula -> formula -> formula)]
iffs
          where
            ands :: IsPropositional formula => [(Rational, formula -> formula -> formula)]
            ands :: forall formula.
IsPropositional formula =>
[(Rational, formula -> formula -> formula)]
ands = ((formula -> formula -> formula)
 -> (Rational, formula -> formula -> formula))
-> [formula -> formula -> formula]
-> [(Rational, formula -> formula -> formula)]
forall a b. (a -> b) -> [a] -> [b]
List.map (Rational
Precedence
andPrec,) [formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(.&.), formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(∧), formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(·)]
            ors :: IsPropositional formula => [(Rational, formula -> formula -> formula)]
            ors :: forall formula.
IsPropositional formula =>
[(Rational, formula -> formula -> formula)]
ors = ((formula -> formula -> formula)
 -> (Rational, formula -> formula -> formula))
-> [formula -> formula -> formula]
-> [(Rational, formula -> formula -> formula)]
forall a b. (a -> b) -> [a] -> [b]
List.map (Rational
Precedence
orPrec,) [formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(.|.), formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(∨)]
            imps :: IsPropositional formula => [(Rational, formula -> formula -> formula)]
            imps :: forall formula.
IsPropositional formula =>
[(Rational, formula -> formula -> formula)]
imps = ((formula -> formula -> formula)
 -> (Rational, formula -> formula -> formula))
-> [formula -> formula -> formula]
-> [(Rational, formula -> formula -> formula)]
forall a b. (a -> b) -> [a] -> [b]
List.map (Rational
Precedence
impPrec,) [formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(.=>.), formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(⇒), formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(==>), formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(→), formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(⊃)]
            iffs :: IsPropositional formula => [(Rational, formula -> formula -> formula)]
            iffs :: forall formula.
IsPropositional formula =>
[(Rational, formula -> formula -> formula)]
iffs = ((formula -> formula -> formula)
 -> (Rational, formula -> formula -> formula))
-> [formula -> formula -> formula]
-> [(Rational, formula -> formula -> formula)]
forall a b. (a -> b) -> [a] -> [b]
List.map (Rational
Precedence
iffPrec,) [formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(.<=>.), formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(<=>), formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(⇔), formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(↔)]
      preops :: IsPropositional formula => [(Rational, formula -> formula)]
      preops :: forall formula.
IsPropositional formula =>
[(Rational, formula -> formula)]
preops = [(Rational, formula -> formula)]
forall formula.
IsPropositional formula =>
[(Rational, formula -> formula)]
nots
          where
            nots :: IsPropositional formula => [(Rational, formula -> formula)]
            nots :: forall formula.
IsPropositional formula =>
[(Rational, formula -> formula)]
nots = ((formula -> formula) -> (Rational, formula -> formula))
-> [formula -> formula] -> [(Rational, formula -> formula)]
forall a b. (a -> b) -> [a] -> [b]
List.map (Rational
Precedence
notPrec,) [formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.), formula -> formula
forall formula. IsLiteral formula => formula -> formula
(¬)]
      (PFormula Prop
p, PFormula Prop
q, PFormula Prop
r) = (Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"p"), Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"q"), Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"r"))
      -- What about these?
      -- (∴)


{-
test00 = TestCase $ assertEqual "parenthesization" expected (List.map prettyShow input)
          (input, expected) = unzip [( p .&. (q .|. r)   , "p∧(q∨r)" ),
                                     ( (p .&. q) .|. r   , "(p∧q)∨r" ),
                                     ( p .&. q .|. r     , "(p∧q)∨r" ),
                                     ( p .|. q .&. r     , "p∨(q∧r)" ),
                                     ( p .&. q .&. r     , "p∧q∧r"   ),
                                     ( (p .=>. q) .=>. r , "(p⇒q)⇒r" ),
                                     ( p .=>. (q .=>. r) , "p⇒q⇒r"   ),
                                     ( p .=>. q .=>. r   , "p⇒q⇒r"   )]
-}

test01 :: Test
test01 :: Test
test01 =
    let fm :: PFormula Prop
fm = AtomOf (PFormula Prop) -> PFormula Prop
forall formula. IsFormula formula => AtomOf formula -> formula
atomic AtomOf (PFormula Prop)
Prop
"p" PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. AtomOf (PFormula Prop) -> PFormula Prop
forall formula. IsFormula formula => AtomOf formula -> formula
atomic AtomOf (PFormula Prop)
Prop
"q" PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. (AtomOf (PFormula Prop) -> PFormula Prop
forall formula. IsFormula formula => AtomOf formula -> formula
atomic AtomOf (PFormula Prop)
Prop
"r" PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. AtomOf (PFormula Prop) -> PFormula Prop
forall formula. IsFormula formula => AtomOf formula -> formula
atomic AtomOf (PFormula Prop)
Prop
"s") PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. (AtomOf (PFormula Prop) -> PFormula Prop
forall formula. IsFormula formula => AtomOf formula -> formula
atomic AtomOf (PFormula Prop)
Prop
"t" PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) (AtomOf (PFormula Prop) -> PFormula Prop
forall formula. IsFormula formula => AtomOf formula -> formula
atomic AtomOf (PFormula Prop)
Prop
"u"))) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. AtomOf (PFormula Prop) -> PFormula Prop
forall formula. IsFormula formula => AtomOf formula -> formula
atomic AtomOf (PFormula Prop)
Prop
"v") :: PFormula Prop
        input :: (String, String)
input = (PFormula Prop -> String
forall a. Pretty a => a -> String
prettyShow PFormula Prop
fm, PFormula Prop -> String
forall a. Show a => a -> String
show PFormula Prop
fm)
        expected :: (String, String)
expected = (-- Pretty printed
                    String
"p⇒q⇔(r∧s)∨(t⇔u∧v)",
                    -- Haskell expression
                    String
"atomic \"p\" .=>. atomic \"q\" .<=>. (atomic \"r\" .&. atomic \"s\") .|. (atomic \"t\" .<=>. atomic \"u\" .&. atomic \"v\")"
                    ) in
    Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> (String, String) -> (String, String) -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"Build Formula 1" (String, String)
expected (String, String)
input

test02 :: Test
test02 :: Test
test02 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> PFormula Prop -> PFormula Prop -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"Build Formula 2" PFormula Prop
expected PFormula Prop
input
    where input :: PFormula Prop
input = (Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom Prop
"fm" PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom Prop
"fm") :: PFormula Prop
          expected :: PFormula Prop
expected = (PFormula Prop -> PFormula Prop -> PFormula Prop
forall atom. PFormula atom -> PFormula atom -> PFormula atom
And (Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom Prop
"fm") (Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom Prop
"fm"))

test03 :: Test
test03 :: Test
test03 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> PFormula Prop -> PFormula Prop -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"Build Formula 3"
                                (Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom Prop
"fm" PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom Prop
"fm" PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom Prop
"fm" :: PFormula Prop)
                                (PFormula Prop -> PFormula Prop -> PFormula Prop
forall atom. PFormula atom -> PFormula atom -> PFormula atom
Or (Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom Prop
"fm") (PFormula Prop -> PFormula Prop -> PFormula Prop
forall atom. PFormula atom -> PFormula atom -> PFormula atom
And (Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom Prop
"fm") (Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom Prop
"fm")))

-- Example of use.

test04 :: Test
test04 :: Test
test04 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> [Bool] -> [Bool] -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"fixity tests" [Bool]
expected [Bool]
input
    where ([Bool]
input, [Bool]
expected) = [(Bool, Bool)] -> ([Bool], [Bool])
forall a b. [(a, b)] -> ([a], [b])
unzip (((PFormula Prop, Bool) -> (Bool, Bool))
-> [(PFormula Prop, Bool)] -> [(Bool, Bool)]
forall a b. (a -> b) -> [a] -> [b]
List.map (\ (PFormula Prop
fm, Bool
flag) -> (PFormula Prop -> (AtomOf (PFormula Prop) -> Bool) -> Bool
forall pf.
JustPropositional pf =>
pf -> (AtomOf pf -> Bool) -> Bool
eval PFormula Prop
fm AtomOf (PFormula Prop) -> Bool
Prop -> Bool
forall {a} {a}. Show a => a -> a
v0, Bool
flag)) [(PFormula Prop, Bool)]
pairs)
          v0 :: a -> a
v0 a
x = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"v0: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
x
          pairs :: [(PFormula Prop, Bool)]
          pairs :: [(PFormula Prop, Bool)]
pairs =
              [ ( PFormula Prop
forall formula. IsFormula formula => formula
true PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
forall formula. IsFormula formula => formula
false PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. PFormula Prop
forall formula. IsFormula formula => formula
false PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
forall formula. IsFormula formula => formula
true,  Bool
True)
              , ( PFormula Prop
forall formula. IsFormula formula => formula
true PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
forall formula. IsFormula formula => formula
true  PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. PFormula Prop
forall formula. IsFormula formula => formula
true  PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
forall formula. IsFormula formula => formula
false, Bool
False)
              , (   PFormula Prop
forall formula. IsFormula formula => formula
false PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
∧  PFormula Prop
forall formula. IsFormula formula => formula
true  PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
∨ PFormula Prop
forall formula. IsFormula formula => formula
true,             Bool
True)  -- "∧ binds more tightly than ∨"
              , (  (PFormula Prop
forall formula. IsFormula formula => formula
false PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
∧  PFormula Prop
forall formula. IsFormula formula => formula
true) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
∨ PFormula Prop
forall formula. IsFormula formula => formula
true,             Bool
True)
              , (   PFormula Prop
forall formula. IsFormula formula => formula
false PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
∧ (PFormula Prop
forall formula. IsFormula formula => formula
true  PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
∨ PFormula Prop
forall formula. IsFormula formula => formula
true),            Bool
False)
              , (  PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(¬) PFormula Prop
forall formula. IsFormula formula => formula
true PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
∨ PFormula Prop
forall formula. IsFormula formula => formula
true,                    Bool
True)  -- "¬ binds more tightly than ∨"
              , (  PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(¬) (PFormula Prop
forall formula. IsFormula formula => formula
true PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
∨ PFormula Prop
forall formula. IsFormula formula => formula
true),                  Bool
False)
              ]

-- Example.

test06 :: Test
test06 :: Test
test06 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> Set Prop -> Set Prop -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"atoms test" (PFormula Prop -> Set (AtomOf (PFormula Prop))
forall formula.
IsFormula formula =>
formula -> Set (AtomOf formula)
atoms (PFormula Prop -> Set (AtomOf (PFormula Prop)))
-> PFormula Prop -> Set (AtomOf (PFormula Prop))
forall a b. (a -> b) -> a -> b
$ PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
q PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. PFormula Prop
s PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
p) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. (PFormula Prop
r PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. PFormula Prop
s)) ([Prop] -> Set Prop
forall a. Ord a => [a] -> Set a
Set.fromList [String -> Prop
P String
"p",String -> Prop
P String
"q",String -> Prop
P String
"r",String -> Prop
P String
"s"])
    where (PFormula Prop
p, PFormula Prop
q, PFormula Prop
r, PFormula Prop
s) = (Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"p"), Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"q"), Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"r"), Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"s"))

-- Example.

test07 :: Test
test07 :: Test
test07 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> TruthTable Prop -> TruthTable Prop -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"truth table 1 (p. 36)" TruthTable Prop
expected TruthTable Prop
input
    where input :: TruthTable (AtomOf (PFormula Prop))
input = (PFormula Prop -> TruthTable (AtomOf (PFormula Prop))
forall pf. JustPropositional pf => pf -> TruthTable (AtomOf pf)
truthTable (PFormula Prop -> TruthTable (AtomOf (PFormula Prop)))
-> PFormula Prop -> TruthTable (AtomOf (PFormula Prop))
forall a b. (a -> b) -> a -> b
$ PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
q PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. PFormula Prop
q PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
r)
          expected :: TruthTable Prop
expected =
              ([Prop] -> [TruthTableRow] -> TruthTable Prop
forall a. [a] -> [TruthTableRow] -> TruthTable a
TruthTable
               [String -> Prop
P String
"p", String -> Prop
P String
"q", String -> Prop
P String
"r"]
               [([Bool
False,Bool
False,Bool
False],Bool
True),
               ([Bool
False,Bool
False,Bool
True],Bool
True),
               ([Bool
False,Bool
True,Bool
False],Bool
True),
               ([Bool
False,Bool
True,Bool
True],Bool
True),
               ([Bool
True,Bool
False,Bool
False],Bool
True),
               ([Bool
True,Bool
False,Bool
True],Bool
True),
               ([Bool
True,Bool
True,Bool
False],Bool
False),
               ([Bool
True,Bool
True,Bool
True],Bool
True)])
          (PFormula Prop
p, PFormula Prop
q, PFormula Prop
r) = (Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"p"), Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"q"), Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"r"))

-- Additional examples illustrating formula classes.

test08 :: Test
test08 :: Test
test08 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$
    String -> TruthTable Prop -> TruthTable Prop -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"truth table 2 (p. 39)"
                (PFormula Prop -> TruthTable (AtomOf (PFormula Prop))
forall pf. JustPropositional pf => pf -> TruthTable (AtomOf pf)
truthTable (PFormula Prop -> TruthTable (AtomOf (PFormula Prop)))
-> PFormula Prop -> TruthTable (AtomOf (PFormula Prop))
forall a b. (a -> b) -> a -> b
$  ((PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. PFormula Prop
q) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. PFormula Prop
p) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. PFormula Prop
p)
                ([Prop] -> [TruthTableRow] -> TruthTable Prop
forall a. [a] -> [TruthTableRow] -> TruthTable a
TruthTable
                 [String -> Prop
P String
"p", String -> Prop
P String
"q"]
                 [([Bool
False,Bool
False],Bool
True),
                  ([Bool
False,Bool
True],Bool
True),
                  ([Bool
True,Bool
False],Bool
True),
                  ([Bool
True,Bool
True],Bool
True)])
        where (PFormula Prop
p, PFormula Prop
q) = (Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"p"), Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"q"))

test09 :: Test
test09 :: Test
test09 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$
    String -> TruthTable Prop -> TruthTable Prop -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"truth table 3 (p. 40)" TruthTable Prop
expected TruthTable Prop
input
        where input :: TruthTable (AtomOf (PFormula Prop))
input = (PFormula Prop -> TruthTable (AtomOf (PFormula Prop))
forall pf. JustPropositional pf => pf -> TruthTable (AtomOf pf)
truthTable (PFormula Prop -> TruthTable (AtomOf (PFormula Prop)))
-> PFormula Prop -> TruthTable (AtomOf (PFormula Prop))
forall a b. (a -> b) -> a -> b
$ PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
p))
              expected :: TruthTable Prop
expected = ([Prop] -> [TruthTableRow] -> TruthTable Prop
forall a. [a] -> [TruthTableRow] -> TruthTable a
TruthTable
                          [String -> Prop
P String
"p"]
                          [([Bool
False],Bool
False),
                          ([Bool
True],Bool
False)])
              p :: PFormula Prop
p = Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"p")

-- Examples.

test10 :: Test
test10 :: Test
test10 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> Bool -> Bool -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"tautology 1 (p. 41)" Bool
True (PFormula Prop -> Bool
forall pf. JustPropositional pf => pf -> Bool
tautology (PFormula Prop -> Bool) -> PFormula Prop -> Bool
forall a b. (a -> b) -> a -> b
$ PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
p)) where p :: PFormula Prop
p = Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"p")
test11 :: Test
test11 :: Test
test11 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> Bool -> Bool -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"tautology 2 (p. 41)" Bool
False (PFormula Prop -> Bool
forall pf. JustPropositional pf => pf -> Bool
tautology (PFormula Prop -> Bool) -> PFormula Prop -> Bool
forall a b. (a -> b) -> a -> b
$ PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. PFormula Prop
q PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. PFormula Prop
p) where (PFormula Prop
p, PFormula Prop
q) = (Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"p"), Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"q"))
test12 :: Test
test12 :: Test
test12 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> Bool -> Bool -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"tautology 3 (p. 41)" Bool
False (PFormula Prop -> Bool
forall pf. JustPropositional pf => pf -> Bool
tautology (PFormula Prop -> Bool) -> PFormula Prop -> Bool
forall a b. (a -> b) -> a -> b
$ PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. PFormula Prop
q PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. PFormula Prop
q PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. (PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. PFormula Prop
q)) where (PFormula Prop
p, PFormula Prop
q) = (Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"p"), Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"q"))
test13 :: Test
test13 :: Test
test13 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> Bool -> Bool -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"tautology 4 (p. 41)" Bool
True (PFormula Prop -> Bool
forall pf. JustPropositional pf => pf -> Bool
tautology (PFormula Prop -> Bool) -> PFormula Prop -> Bool
forall a b. (a -> b) -> a -> b
$ (PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. PFormula Prop
q) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.)(PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
q)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.)PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. PFormula Prop
q)) where (PFormula Prop
p, PFormula Prop
q) = (Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"p"), Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"q"))

-- | Substitution operation.
psubst :: JustPropositional formula => Map (AtomOf formula) formula -> formula -> formula
psubst :: forall formula.
JustPropositional formula =>
Map (AtomOf formula) formula -> formula -> formula
psubst Map (AtomOf formula) formula
subfn formula
fm =
    (formula -> BinOp -> formula -> formula)
-> (formula -> formula)
-> (Bool -> formula)
-> (AtomOf formula -> formula)
-> formula
-> formula
forall pf r.
JustPropositional pf =>
(pf -> BinOp -> pf -> r)
-> (pf -> r) -> (Bool -> r) -> (AtomOf pf -> r) -> pf -> r
foldPropositional formula -> BinOp -> formula -> formula
co formula -> formula
ne Bool -> formula
tf AtomOf formula -> formula
at formula
fm
    where
      co :: formula -> BinOp -> formula -> formula
co formula
p BinOp
op formula
q = formula -> BinOp -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> BinOp -> formula -> formula
binop (Map (AtomOf formula) formula -> formula -> formula
forall formula.
JustPropositional formula =>
Map (AtomOf formula) formula -> formula -> formula
psubst Map (AtomOf formula) formula
subfn formula
p) BinOp
op (Map (AtomOf formula) formula -> formula -> formula
forall formula.
JustPropositional formula =>
Map (AtomOf formula) formula -> formula -> formula
psubst Map (AtomOf formula) formula
subfn formula
q)
      ne :: formula -> formula
ne formula
p = formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) (Map (AtomOf formula) formula -> formula -> formula
forall formula.
JustPropositional formula =>
Map (AtomOf formula) formula -> formula -> formula
psubst Map (AtomOf formula) formula
subfn formula
p)
      tf :: Bool -> formula
tf = Bool -> formula
forall formula. IsFormula formula => Bool -> formula
fromBool
      at :: AtomOf formula -> formula
at AtomOf formula
p = formula -> Maybe formula -> formula
forall a. a -> Maybe a -> a
fromMaybe (AtomOf formula -> formula
forall formula. IsFormula formula => AtomOf formula -> formula
atomic AtomOf formula
p) (Map (AtomOf formula) formula -> AtomOf formula -> Maybe formula
forall a b. Ord a => Map a b -> a -> Maybe b
fpf Map (AtomOf formula) formula
subfn AtomOf formula
p)

-- Example
test14 :: Test
test14 :: Test
test14 =
    Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> PFormula Prop -> PFormula Prop -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"pSubst (p. 41)" PFormula Prop
expected PFormula Prop
input
        where expected :: PFormula Prop
expected = (PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
q) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
q PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
q) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
q
              input :: PFormula Prop
input = Map (AtomOf (PFormula Prop)) (PFormula Prop)
-> PFormula Prop -> PFormula Prop
forall formula.
JustPropositional formula =>
Map (AtomOf formula) formula -> formula -> formula
psubst ((String -> Prop
P String
"p") Prop -> PFormula Prop -> Map Prop (PFormula Prop)
forall k a. Ord k => k -> a -> Map k a
|=> (PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
q)) (PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
q PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
q)
              (PFormula Prop
p, PFormula Prop
q) = (Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"p"), Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"q"))

-- Surprising tautologies including Dijkstra's "Golden rule".

test15 :: Test
test15 :: Test
test15 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> Bool -> Bool -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"tautology 5 (p. 43)" Bool
expected Bool
input
    where input :: Bool
input = PFormula Prop -> Bool
forall pf. JustPropositional pf => pf -> Bool
tautology (PFormula Prop -> Bool) -> PFormula Prop -> Bool
forall a b. (a -> b) -> a -> b
$ (PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. PFormula Prop
q) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. (PFormula Prop
q PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. PFormula Prop
p)
          expected :: Bool
expected = Bool
True
          (PFormula Prop
p, PFormula Prop
q) = (Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"p"), Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"q"))
test16 :: Test
test16 :: Test
test16 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> Bool -> Bool -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"tautology 6 (p. 45)" Bool
expected Bool
input
    where input :: Bool
input = PFormula Prop -> Bool
forall pf. JustPropositional pf => pf -> Bool
tautology (PFormula Prop -> Bool) -> PFormula Prop -> Bool
forall a b. (a -> b) -> a -> b
$ PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. (PFormula Prop
q PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. PFormula Prop
r) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. (PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. PFormula Prop
q PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. PFormula Prop
r)
          expected :: Bool
expected = Bool
True
          (PFormula Prop
p, PFormula Prop
q, PFormula Prop
r) = (Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"p"), Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"q"), Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"r"))
test17 :: Test
test17 :: Test
test17 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> Bool -> Bool -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"Dijkstra's Golden Rule (p. 45)" Bool
expected Bool
input
    where input :: Bool
input = PFormula Prop -> Bool
forall pf. JustPropositional pf => pf -> Bool
tautology (PFormula Prop -> Bool) -> PFormula Prop -> Bool
forall a b. (a -> b) -> a -> b
$ PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
q PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. ((PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. PFormula Prop
q) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. PFormula Prop
q)
          expected :: Bool
expected = Bool
True
          (PFormula Prop
p, PFormula Prop
q) = (Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"p"), Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"q"))
test18 :: Test
test18 :: Test
test18 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> Bool -> Bool -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"Contraposition 1 (p. 46)" Bool
expected Bool
input
    where input :: Bool
input = PFormula Prop -> Bool
forall pf. JustPropositional pf => pf -> Bool
tautology (PFormula Prop -> Bool) -> PFormula Prop -> Bool
forall a b. (a -> b) -> a -> b
$ (PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. PFormula Prop
q) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. ((PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.)PFormula Prop
q) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.)PFormula Prop
p))
          expected :: Bool
expected = Bool
True
          (PFormula Prop
p, PFormula Prop
q) = (Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"p"), Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"q"))
test19 :: Test
test19 :: Test
test19 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> Bool -> Bool -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"Contraposition 2 (p. 46)" Bool
expected Bool
input
    where input :: Bool
input = PFormula Prop -> Bool
forall pf. JustPropositional pf => pf -> Bool
tautology (PFormula Prop -> Bool) -> PFormula Prop -> Bool
forall a b. (a -> b) -> a -> b
$ (PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.)PFormula Prop
q)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. (PFormula Prop
q PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.)PFormula Prop
p))
          expected :: Bool
expected = Bool
True
          (PFormula Prop
p, PFormula Prop
q) = (Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"p"), Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"q"))
test20 :: Test
test20 :: Test
test20 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> Bool -> Bool -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"Contraposition 3 (p. 46)" Bool
expected Bool
input
    where input :: Bool
input = PFormula Prop -> Bool
forall pf. JustPropositional pf => pf -> Bool
tautology (PFormula Prop -> Bool) -> PFormula Prop -> Bool
forall a b. (a -> b) -> a -> b
$ (PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. PFormula Prop
q) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. (PFormula Prop
q PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. PFormula Prop
p)
          expected :: Bool
expected = Bool
False
          (PFormula Prop
p, PFormula Prop
q) = (Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"p"), Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"q"))

-- Some logical equivalences allowing elimination of connectives.

test21 :: Test
test21 :: Test
test21 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> [Bool] -> [Bool] -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"Equivalences (p. 47)" [Bool]
expected [Bool]
input
    where input :: [Bool]
input =
              (PFormula Prop -> Bool) -> [PFormula Prop] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
List.map PFormula Prop -> Bool
forall pf. JustPropositional pf => pf -> Bool
tautology
              [ PFormula Prop
forall formula. IsFormula formula => formula
true PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. PFormula Prop
forall formula. IsFormula formula => formula
false PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. PFormula Prop
forall formula. IsFormula formula => formula
false
              , (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.)PFormula Prop
p) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. PFormula Prop
forall formula. IsFormula formula => formula
false
              , PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
q PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. (PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. PFormula Prop
q PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. PFormula Prop
forall formula. IsFormula formula => formula
false) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. PFormula Prop
forall formula. IsFormula formula => formula
false
              , PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. PFormula Prop
q PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. (PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. PFormula Prop
forall formula. IsFormula formula => formula
false) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. PFormula Prop
q
              , (PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. PFormula Prop
q) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. ((PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. PFormula Prop
q) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. (PFormula Prop
q PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. PFormula Prop
p) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. PFormula Prop
forall formula. IsFormula formula => formula
false) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. PFormula Prop
forall formula. IsFormula formula => formula
false ]
          expected :: [Bool]
expected = [Bool
True, Bool
True, Bool
True, Bool
True, Bool
True]
          (PFormula Prop
p, PFormula Prop
q) = (Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"p"), Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"q"))

-- | Dualization.
dual :: JustPropositional pf => pf -> pf
dual :: forall pf. JustPropositional pf => pf -> pf
dual pf
fm =
    (pf -> BinOp -> pf -> pf)
-> (pf -> pf) -> (Bool -> pf) -> (AtomOf pf -> pf) -> pf -> pf
forall pf r.
JustPropositional pf =>
(pf -> BinOp -> pf -> r)
-> (pf -> r) -> (Bool -> r) -> (AtomOf pf -> r) -> pf -> r
foldPropositional pf -> BinOp -> pf -> pf
forall {formula}.
JustPropositional formula =>
formula -> BinOp -> formula -> formula
co pf -> pf
forall pf. JustPropositional pf => pf -> pf
ne Bool -> pf
forall formula. IsFormula formula => Bool -> formula
tf (\AtomOf pf
_ -> pf
fm) pf
fm
    where
      tf :: Bool -> formula
tf Bool
True = formula
forall formula. IsFormula formula => formula
false
      tf Bool
False = formula
forall formula. IsFormula formula => formula
true
      ne :: formula -> formula
ne formula
p = formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) (formula -> formula
forall pf. JustPropositional pf => pf -> pf
dual formula
p)
      co :: formula -> BinOp -> formula -> formula
co formula
p BinOp
(:&:) formula
q = formula -> formula
forall pf. JustPropositional pf => pf -> pf
dual formula
p formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. formula -> formula
forall pf. JustPropositional pf => pf -> pf
dual formula
q
      co formula
p BinOp
(:|:) formula
q = formula -> formula
forall pf. JustPropositional pf => pf -> pf
dual formula
p formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. formula -> formula
forall pf. JustPropositional pf => pf -> pf
dual formula
q
      co formula
_ BinOp
_ formula
_ = String -> formula
forall a. HasCallStack => String -> a
error String
"Formula involves connectives .=>. or .<=>."

-- Example.
test22 :: Test
test22 :: Test
test22 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> PFormula Prop -> PFormula Prop -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"Dual (p. 49)" PFormula Prop
expected PFormula Prop
input
    where input :: PFormula Prop
input = PFormula Prop -> PFormula Prop
forall pf. JustPropositional pf => pf -> pf
dual (Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"p") PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) (Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"p"))))
          expected :: PFormula Prop
expected = PFormula Prop -> PFormula Prop -> PFormula Prop
forall atom. PFormula atom -> PFormula atom -> PFormula atom
And (Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (P {pname :: String
pname = String
"p"})) (PFormula Prop -> PFormula Prop
forall atom. PFormula atom -> PFormula atom
Not (Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (P {pname :: String
pname = String
"p"})))

-- | Routine simplification.
psimplify :: IsPropositional formula => formula -> formula
psimplify :: forall formula. IsPropositional formula => formula -> formula
psimplify formula
fm =
    (formula -> formula)
-> (formula -> BinOp -> formula -> formula)
-> (formula -> formula)
-> (Bool -> formula)
-> (AtomOf formula -> formula)
-> formula
-> formula
forall formula r.
IsPropositional formula =>
(formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
forall r.
(formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
foldPropositional' formula -> formula
ho formula -> BinOp -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> BinOp -> formula -> formula
co formula -> formula
forall formula. IsPropositional formula => formula -> formula
ne Bool -> formula
tf AtomOf formula -> formula
at formula
fm
    where
      ho :: formula -> formula
ho formula
_ = formula
fm
      ne :: formula -> formula
ne formula
p = formula -> formula
forall formula. IsPropositional formula => formula -> formula
psimplify1 (formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) (formula -> formula
forall formula. IsPropositional formula => formula -> formula
psimplify formula
p))
      co :: formula -> BinOp -> formula -> formula
co formula
p BinOp
(:&:) formula
q = formula -> formula
forall formula. IsPropositional formula => formula -> formula
psimplify1 ((formula -> formula
forall formula. IsPropositional formula => formula -> formula
psimplify formula
p) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (formula -> formula
forall formula. IsPropositional formula => formula -> formula
psimplify formula
q))
      co formula
p BinOp
(:|:) formula
q = formula -> formula
forall formula. IsPropositional formula => formula -> formula
psimplify1 ((formula -> formula
forall formula. IsPropositional formula => formula -> formula
psimplify formula
p) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. (formula -> formula
forall formula. IsPropositional formula => formula -> formula
psimplify formula
q))
      co formula
p BinOp
(:=>:) formula
q = formula -> formula
forall formula. IsPropositional formula => formula -> formula
psimplify1 ((formula -> formula
forall formula. IsPropositional formula => formula -> formula
psimplify formula
p) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. (formula -> formula
forall formula. IsPropositional formula => formula -> formula
psimplify formula
q))
      co formula
p BinOp
(:<=>:) formula
q = formula -> formula
forall formula. IsPropositional formula => formula -> formula
psimplify1 ((formula -> formula
forall formula. IsPropositional formula => formula -> formula
psimplify formula
p) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. (formula -> formula
forall formula. IsPropositional formula => formula -> formula
psimplify formula
q))
      tf :: Bool -> formula
tf Bool
_ = formula
fm
      at :: AtomOf formula -> formula
at AtomOf formula
_ = formula
fm

psimplify1 :: IsPropositional formula => formula -> formula
psimplify1 :: forall formula. IsPropositional formula => formula -> formula
psimplify1 formula
fm =
    (formula -> formula)
-> (formula -> BinOp -> formula -> formula)
-> (formula -> formula)
-> (Bool -> formula)
-> (AtomOf formula -> formula)
-> formula
-> formula
forall formula r.
IsPropositional formula =>
(formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
forall r.
(formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
foldPropositional' (\formula
_ -> formula
fm) formula -> BinOp -> formula -> formula
simplifyCombine formula -> formula
simplifyNegate (\Bool
_ -> formula
fm) (\AtomOf formula
_ -> formula
fm) formula
fm
    where
      simplifyNegate :: formula -> formula
simplifyNegate formula
p = (formula -> formula)
-> (formula -> BinOp -> formula -> formula)
-> (formula -> formula)
-> (Bool -> formula)
-> (AtomOf formula -> formula)
-> formula
-> formula
forall formula r.
IsPropositional formula =>
(formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
forall r.
(formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
foldPropositional' (\formula
_ -> formula
fm) formula -> BinOp -> formula -> formula
simplifyNotCombine formula -> formula
forall {a}. a -> a
simplifyNotNegate (Bool -> formula
forall formula. IsFormula formula => Bool -> formula
fromBool (Bool -> formula) -> (Bool -> Bool) -> Bool -> formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool
not) AtomOf formula -> formula
forall {formula}. IsLiteral formula => AtomOf formula -> formula
simplifyNotAtom formula
p
      simplifyCombine :: formula -> BinOp -> formula -> formula
simplifyCombine formula
l BinOp
op formula
r =
          case (formula -> Maybe Bool
forall formula. IsFormula formula => formula -> Maybe Bool
asBool formula
l, BinOp
op , formula -> Maybe Bool
forall formula. IsFormula formula => formula -> Maybe Bool
asBool formula
r) of
            (Just Bool
True,  BinOp
(:&:), Maybe Bool
_)            -> formula
r
            (Just Bool
False, BinOp
(:&:), Maybe Bool
_)            -> Bool -> formula
forall formula. IsFormula formula => Bool -> formula
fromBool Bool
False
            (Maybe Bool
_,          BinOp
(:&:), Just Bool
True)    -> formula
l
            (Maybe Bool
_,          BinOp
(:&:), Just Bool
False)   -> Bool -> formula
forall formula. IsFormula formula => Bool -> formula
fromBool Bool
False
            (Just Bool
True,  BinOp
(:|:), Maybe Bool
_)            -> Bool -> formula
forall formula. IsFormula formula => Bool -> formula
fromBool Bool
True
            (Just Bool
False, BinOp
(:|:), Maybe Bool
_)            -> formula
r
            (Maybe Bool
_,          BinOp
(:|:), Just Bool
True)    -> Bool -> formula
forall formula. IsFormula formula => Bool -> formula
fromBool Bool
True
            (Maybe Bool
_,          BinOp
(:|:), Just Bool
False)   -> formula
l
            (Just Bool
True,  BinOp
(:=>:), Maybe Bool
_)           -> formula
r
            (Just Bool
False, BinOp
(:=>:), Maybe Bool
_)           -> Bool -> formula
forall formula. IsFormula formula => Bool -> formula
fromBool Bool
True
            (Maybe Bool
_,          BinOp
(:=>:), Just Bool
True)   -> Bool -> formula
forall formula. IsFormula formula => Bool -> formula
fromBool Bool
True
            (Maybe Bool
_,          BinOp
(:=>:), Just Bool
False)  -> formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) formula
l
            (Just Bool
False, BinOp
(:<=>:), Just Bool
False) -> Bool -> formula
forall formula. IsFormula formula => Bool -> formula
fromBool Bool
True
            (Just Bool
True,  BinOp
(:<=>:), Maybe Bool
_)          -> formula
r
            (Just Bool
False, BinOp
(:<=>:), Maybe Bool
_)          -> formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) formula
r
            (Maybe Bool
_,          BinOp
(:<=>:), Just Bool
True)  -> formula
l
            (Maybe Bool
_,          BinOp
(:<=>:), Just Bool
False) -> formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) formula
l
            (Maybe Bool, BinOp, Maybe Bool)
_                                 -> formula
fm
      simplifyNotNegate :: p -> p
simplifyNotNegate p
f = p
f
      simplifyNotCombine :: formula -> BinOp -> formula -> formula
simplifyNotCombine formula
_ BinOp
_ formula
_ = formula
fm
      simplifyNotAtom :: AtomOf formula -> formula
simplifyNotAtom AtomOf formula
x = formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) (AtomOf formula -> formula
forall formula. IsFormula formula => AtomOf formula -> formula
atomic AtomOf formula
x)

-- Example.
test23 :: Test
test23 :: Test
test23 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> PFormula Prop -> PFormula Prop -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"psimplify 1 (p. 50)" PFormula Prop
expected PFormula Prop
input
    where input :: PFormula Prop
input = PFormula Prop -> PFormula Prop
forall formula. IsPropositional formula => formula -> formula
psimplify (PFormula Prop -> PFormula Prop) -> PFormula Prop -> PFormula Prop
forall a b. (a -> b) -> a -> b
$ (PFormula Prop
forall formula. IsFormula formula => formula
true PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. (PFormula Prop
x PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. PFormula Prop
forall formula. IsFormula formula => formula
false)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) (PFormula Prop
y PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. PFormula Prop
forall formula. IsFormula formula => formula
false PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
z))
          expected :: PFormula Prop
expected = (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
x) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
y)
          x :: PFormula Prop
x = Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"x")
          y :: PFormula Prop
y = Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"y")
          z :: PFormula Prop
z = Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"z")

test24 :: Test
test24 :: Test
test24 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> PFormula Prop -> PFormula Prop -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"psimplify 2 (p. 51)" PFormula Prop
expected PFormula Prop
input
    where input :: PFormula Prop
input = PFormula Prop -> PFormula Prop
forall formula. IsPropositional formula => formula -> formula
psimplify (PFormula Prop -> PFormula Prop) -> PFormula Prop -> PFormula Prop
forall a b. (a -> b) -> a -> b
$ ((PFormula Prop
x PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. PFormula Prop
y) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. PFormula Prop
forall formula. IsFormula formula => formula
true) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
forall formula. IsFormula formula => formula
false
          expected :: PFormula Prop
expected = PFormula Prop
forall formula. IsFormula formula => formula
true
          x :: PFormula Prop
x = Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"x")
          y :: PFormula Prop
y = Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"y")

-- | Negation normal form.

nnf :: JustPropositional pf => pf -> pf
nnf :: forall pf. JustPropositional pf => pf -> pf
nnf = pf -> pf
forall pf. JustPropositional pf => pf -> pf
nnf1 (pf -> pf) -> (pf -> pf) -> pf -> pf
forall b c a. (b -> c) -> (a -> b) -> a -> c
. pf -> pf
forall formula. IsPropositional formula => formula -> formula
psimplify

nnf1 :: JustPropositional pf => pf -> pf
nnf1 :: forall pf. JustPropositional pf => pf -> pf
nnf1 pf
fm = (pf -> BinOp -> pf -> pf)
-> (pf -> pf) -> (Bool -> pf) -> (AtomOf pf -> pf) -> pf -> pf
forall pf r.
JustPropositional pf =>
(pf -> BinOp -> pf -> r)
-> (pf -> r) -> (Bool -> r) -> (AtomOf pf -> r) -> pf -> r
foldPropositional pf -> BinOp -> pf -> pf
forall {formula}.
JustPropositional formula =>
formula -> BinOp -> formula -> formula
nnfCombine pf -> pf
nnfNegate Bool -> pf
forall formula. IsFormula formula => Bool -> formula
fromBool (\AtomOf pf
_ -> pf
fm) pf
fm
    where
      -- nnfCombine :: (IsPropositional formula atom) => formula -> Combination formula -> formula
      nnfNegate :: pf -> pf
nnfNegate pf
p = (pf -> BinOp -> pf -> pf)
-> (pf -> pf) -> (Bool -> pf) -> (AtomOf pf -> pf) -> pf -> pf
forall pf r.
JustPropositional pf =>
(pf -> BinOp -> pf -> r)
-> (pf -> r) -> (Bool -> r) -> (AtomOf pf -> r) -> pf -> r
foldPropositional pf -> BinOp -> pf -> pf
forall {formula}.
JustPropositional formula =>
formula -> BinOp -> formula -> formula
nnfNotCombine pf -> pf
forall pf. JustPropositional pf => pf -> pf
nnfNotNegate (Bool -> pf
forall formula. IsFormula formula => Bool -> formula
fromBool (Bool -> pf) -> (Bool -> Bool) -> Bool -> pf
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool
not) (\AtomOf pf
_ -> pf
fm) pf
p
      nnfCombine :: formula -> BinOp -> formula -> formula
nnfCombine formula
p BinOp
(:=>:) formula
q = formula -> formula
forall pf. JustPropositional pf => pf -> pf
nnf1 (formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) formula
p) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. (formula -> formula
forall pf. JustPropositional pf => pf -> pf
nnf1 formula
q)
      nnfCombine formula
p BinOp
(:<=>:) formula
q =  (formula -> formula
forall pf. JustPropositional pf => pf -> pf
nnf1 formula
p formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. formula -> formula
forall pf. JustPropositional pf => pf -> pf
nnf1 formula
q) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. (formula -> formula
forall pf. JustPropositional pf => pf -> pf
nnf1 (formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) formula
p) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. formula -> formula
forall pf. JustPropositional pf => pf -> pf
nnf1 (formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) formula
q))
      nnfCombine formula
p BinOp
(:&:) formula
q = formula -> formula
forall pf. JustPropositional pf => pf -> pf
nnf1 formula
p formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. formula -> formula
forall pf. JustPropositional pf => pf -> pf
nnf1 formula
q
      nnfCombine formula
p BinOp
(:|:) formula
q = formula -> formula
forall pf. JustPropositional pf => pf -> pf
nnf1 formula
p formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. formula -> formula
forall pf. JustPropositional pf => pf -> pf
nnf1 formula
q

      -- nnfNotCombine :: (IsPropositional formula atom) => Combination formula -> formula
      nnfNotNegate :: pf -> pf
nnfNotNegate pf
p = pf -> pf
forall pf. JustPropositional pf => pf -> pf
nnf1 pf
p
      nnfNotCombine :: formula -> BinOp -> formula -> formula
nnfNotCombine formula
p BinOp
(:&:) formula
q = formula -> formula
forall pf. JustPropositional pf => pf -> pf
nnf1 (formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) formula
p) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. formula -> formula
forall pf. JustPropositional pf => pf -> pf
nnf1 (formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) formula
q)
      nnfNotCombine formula
p BinOp
(:|:) formula
q = formula -> formula
forall pf. JustPropositional pf => pf -> pf
nnf1 (formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) formula
p) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. formula -> formula
forall pf. JustPropositional pf => pf -> pf
nnf1 (formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) formula
q)
      nnfNotCombine formula
p BinOp
(:=>:) formula
q = formula -> formula
forall pf. JustPropositional pf => pf -> pf
nnf1 formula
p formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. formula -> formula
forall pf. JustPropositional pf => pf -> pf
nnf1 (formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) formula
q)
      nnfNotCombine formula
p BinOp
(:<=>:) formula
q = (formula -> formula
forall pf. JustPropositional pf => pf -> pf
nnf1 formula
p formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. formula -> formula
forall pf. JustPropositional pf => pf -> pf
nnf1 (formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) formula
q)) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. formula -> formula
forall pf. JustPropositional pf => pf -> pf
nnf1 (formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) formula
p) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. formula -> formula
forall pf. JustPropositional pf => pf -> pf
nnf1 formula
q

-- Example of NNF function in action.

test25 :: Test
test25 :: Test
test25 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> PFormula Prop -> PFormula Prop -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"nnf 1 (p. 53)" PFormula Prop
expected PFormula Prop
input
    where input :: PFormula Prop
input = PFormula Prop -> PFormula Prop
forall pf. JustPropositional pf => pf -> pf
nnf (PFormula Prop -> PFormula Prop) -> PFormula Prop -> PFormula Prop
forall a b. (a -> b) -> a -> b
$ (PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. PFormula Prop
q) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.)(PFormula Prop
r PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. PFormula Prop
s))
          expected :: PFormula Prop
expected = PFormula Prop -> PFormula Prop -> PFormula Prop
forall atom. PFormula atom -> PFormula atom -> PFormula atom
Or (PFormula Prop -> PFormula Prop -> PFormula Prop
forall atom. PFormula atom -> PFormula atom -> PFormula atom
And (PFormula Prop -> PFormula Prop -> PFormula Prop
forall atom. PFormula atom -> PFormula atom -> PFormula atom
Or (PFormula Prop -> PFormula Prop -> PFormula Prop
forall atom. PFormula atom -> PFormula atom -> PFormula atom
And PFormula Prop
p PFormula Prop
q) (PFormula Prop -> PFormula Prop -> PFormula Prop
forall atom. PFormula atom -> PFormula atom -> PFormula atom
And (PFormula Prop -> PFormula Prop
forall atom. PFormula atom -> PFormula atom
Not PFormula Prop
p) (PFormula Prop -> PFormula Prop
forall atom. PFormula atom -> PFormula atom
Not PFormula Prop
q)))
                        (PFormula Prop -> PFormula Prop -> PFormula Prop
forall atom. PFormula atom -> PFormula atom -> PFormula atom
And PFormula Prop
r (PFormula Prop -> PFormula Prop
forall atom. PFormula atom -> PFormula atom
Not PFormula Prop
s)))
                        (PFormula Prop -> PFormula Prop -> PFormula Prop
forall atom. PFormula atom -> PFormula atom -> PFormula atom
And (PFormula Prop -> PFormula Prop -> PFormula Prop
forall atom. PFormula atom -> PFormula atom -> PFormula atom
Or (PFormula Prop -> PFormula Prop -> PFormula Prop
forall atom. PFormula atom -> PFormula atom -> PFormula atom
And PFormula Prop
p (PFormula Prop -> PFormula Prop
forall atom. PFormula atom -> PFormula atom
Not PFormula Prop
q)) (PFormula Prop -> PFormula Prop -> PFormula Prop
forall atom. PFormula atom -> PFormula atom -> PFormula atom
And (PFormula Prop -> PFormula Prop
forall atom. PFormula atom -> PFormula atom
Not PFormula Prop
p) PFormula Prop
q))
                             (PFormula Prop -> PFormula Prop -> PFormula Prop
forall atom. PFormula atom -> PFormula atom -> PFormula atom
Or (PFormula Prop -> PFormula Prop
forall atom. PFormula atom -> PFormula atom
Not PFormula Prop
r) PFormula Prop
s))
          p :: PFormula Prop
p = Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"p")
          q :: PFormula Prop
q = Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"q")
          r :: PFormula Prop
r = Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"r")
          s :: PFormula Prop
s = Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"s")

test26 :: Test
test26 :: Test
test26 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> Bool -> Bool -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"nnf 1 (p. 53)" Bool
expected Bool
input
    where input :: Bool
input = PFormula Prop -> Bool
forall pf. JustPropositional pf => pf -> Bool
tautology (PFormula Prop -> PFormula Prop -> PFormula Prop
forall atom. PFormula atom -> PFormula atom -> PFormula atom
Iff PFormula Prop
fm PFormula Prop
fm')
          expected :: Bool
expected = Bool
True
          fm' :: PFormula Prop
fm' = PFormula Prop -> PFormula Prop
forall pf. JustPropositional pf => pf -> pf
nnf PFormula Prop
fm
          fm :: PFormula Prop
fm = (PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. PFormula Prop
q) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.)(PFormula Prop
r PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. PFormula Prop
s))
          p :: PFormula Prop
p = Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"p")
          q :: PFormula Prop
q = Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"q")
          r :: PFormula Prop
r = Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"r")
          s :: PFormula Prop
s = Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"s")

nenf :: IsPropositional formula => formula -> formula
nenf :: forall formula. IsPropositional formula => formula -> formula
nenf = formula -> formula
forall formula. IsPropositional formula => formula -> formula
nenf' (formula -> formula) -> (formula -> formula) -> formula -> formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. formula -> formula
forall formula. IsPropositional formula => formula -> formula
psimplify

-- | Simple negation-pushing when we don't care to distinguish occurrences.
nenf' :: IsPropositional formula => formula -> formula
nenf' :: forall formula. IsPropositional formula => formula -> formula
nenf' formula
fm =
    (formula -> formula)
-> (formula -> BinOp -> formula -> formula)
-> (formula -> formula)
-> (Bool -> formula)
-> (AtomOf formula -> formula)
-> formula
-> formula
forall formula r.
IsPropositional formula =>
(formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
forall r.
(formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
foldPropositional' (\formula
_ -> formula
fm) formula -> BinOp -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> BinOp -> formula -> formula
co formula -> formula
ne (\Bool
_ -> formula
fm) (\AtomOf formula
_ -> formula
fm) formula
fm
    where
      ne :: formula -> formula
ne formula
p = (formula -> formula)
-> (formula -> BinOp -> formula -> formula)
-> (formula -> formula)
-> (Bool -> formula)
-> (AtomOf formula -> formula)
-> formula
-> formula
forall formula r.
IsPropositional formula =>
(formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
forall r.
(formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
foldPropositional' (\formula
_ -> formula
fm) formula -> BinOp -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> BinOp -> formula -> formula
co' formula -> formula
forall {a}. a -> a
ne' (\Bool
_ -> formula
fm) (\AtomOf formula
_ -> formula
fm) formula
p
      co :: formula -> BinOp -> formula -> formula
co formula
p BinOp
(:&:) formula
q = formula -> formula
forall formula. IsPropositional formula => formula -> formula
nenf' formula
p formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. formula -> formula
forall formula. IsPropositional formula => formula -> formula
nenf' formula
q
      co formula
p BinOp
(:|:) formula
q = formula -> formula
forall formula. IsPropositional formula => formula -> formula
nenf' formula
p formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. formula -> formula
forall formula. IsPropositional formula => formula -> formula
nenf' formula
q
      co formula
p BinOp
(:=>:) formula
q = formula -> formula
forall formula. IsPropositional formula => formula -> formula
nenf' (formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) formula
p) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. formula -> formula
forall formula. IsPropositional formula => formula -> formula
nenf' formula
q
      co formula
p BinOp
(:<=>:) formula
q = formula -> formula
forall formula. IsPropositional formula => formula -> formula
nenf' formula
p formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. formula -> formula
forall formula. IsPropositional formula => formula -> formula
nenf' formula
q
      ne' :: p -> p
ne' p
p = p
p
      co' :: formula -> BinOp -> formula -> formula
co' formula
p BinOp
(:&:) formula
q = formula -> formula
forall formula. IsPropositional formula => formula -> formula
nenf' (formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) formula
p) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. formula -> formula
forall formula. IsPropositional formula => formula -> formula
nenf' (formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) formula
q)
      co' formula
p BinOp
(:|:) formula
q = formula -> formula
forall formula. IsPropositional formula => formula -> formula
nenf' (formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) formula
p) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. formula -> formula
forall formula. IsPropositional formula => formula -> formula
nenf' (formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) formula
q)
      co' formula
p BinOp
(:=>:) formula
q = formula -> formula
forall formula. IsPropositional formula => formula -> formula
nenf' formula
p formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. formula -> formula
forall formula. IsPropositional formula => formula -> formula
nenf' (formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) formula
q)
      co' formula
p BinOp
(:<=>:) formula
q = formula -> formula
forall formula. IsPropositional formula => formula -> formula
nenf' formula
p formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. formula -> formula
forall formula. IsPropositional formula => formula -> formula
nenf' (formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) formula
q) -- really?  how is this asymmetrical?

-- Some tautologies remarked on.

test27 :: Test
test27 :: Test
test27 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> Bool -> Bool -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"tautology 1 (p. 53)" Bool
expected Bool
input
    where input :: Bool
input = PFormula Prop -> Bool
forall pf. JustPropositional pf => pf -> Bool
tautology (PFormula Prop -> Bool) -> PFormula Prop -> Bool
forall a b. (a -> b) -> a -> b
$ (PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. PFormula Prop
p') PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop
q PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. PFormula Prop
q') PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. (PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
q PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. PFormula Prop
p' PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
q')
          expected :: Bool
expected = Bool
True
          p :: PFormula Prop
p = Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"p")
          q :: PFormula Prop
q = Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"q")
          p' :: PFormula Prop
p' = Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"p'")
          q' :: PFormula Prop
q' = Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"q'")
test28 :: Test
test28 :: Test
test28 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> Bool -> Bool -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"nnf 1 (p. 53)" Bool
expected Bool
input
    where input :: Bool
input = PFormula Prop -> Bool
forall pf. JustPropositional pf => pf -> Bool
tautology (PFormula Prop -> Bool) -> PFormula Prop -> Bool
forall a b. (a -> b) -> a -> b
$ (PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. PFormula Prop
p') PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop
q PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. PFormula Prop
q') PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. (PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. PFormula Prop
q PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. PFormula Prop
p' PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. PFormula Prop
q')
          expected :: Bool
expected = Bool
True
          p :: PFormula Prop
p = Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"p")
          q :: PFormula Prop
q = Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"q")
          p' :: PFormula Prop
p' = Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"p'")
          q' :: PFormula Prop
q' = Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"q'")

dnfSet :: (JustPropositional pf, Ord pf) => pf -> pf
dnfSet :: forall pf. (JustPropositional pf, Ord pf) => pf -> pf
dnfSet pf
fm =
    [pf] -> pf
forall (t :: * -> *) formula.
(Foldable t, IsFormula formula, IsPropositional formula) =>
t formula -> formula
list_disj (((AtomOf pf -> Bool) -> pf) -> [AtomOf pf -> Bool] -> [pf]
forall a b. (a -> b) -> [a] -> [b]
List.map (Set pf -> (AtomOf pf -> Bool) -> pf
forall pf.
(JustPropositional pf, Ord pf) =>
Set pf -> (AtomOf pf -> Bool) -> pf
mk_lits ((AtomOf pf -> pf) -> Set (AtomOf pf) -> Set pf
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map AtomOf pf -> pf
forall formula. IsFormula formula => AtomOf formula -> formula
atomic Set (AtomOf pf)
pvs)) [AtomOf pf -> Bool]
satvals)
    where
      satvals :: [AtomOf pf -> Bool]
satvals = ((AtomOf pf -> Bool) -> Bool)
-> (AtomOf pf -> Bool) -> Set (AtomOf pf) -> [AtomOf pf -> Bool]
forall atom.
Ord atom =>
((atom -> Bool) -> Bool)
-> (atom -> Bool) -> Set atom -> [atom -> Bool]
allsatvaluations (pf -> (AtomOf pf -> Bool) -> Bool
forall pf.
JustPropositional pf =>
pf -> (AtomOf pf -> Bool) -> Bool
eval pf
fm) (\AtomOf pf
_s -> Bool
False) Set (AtomOf pf)
pvs
      pvs :: Set (AtomOf pf)
pvs = pf -> Set (AtomOf pf)
forall formula.
IsFormula formula =>
formula -> Set (AtomOf formula)
atoms pf
fm

mk_lits :: (JustPropositional pf, Ord pf) => Set pf -> (AtomOf pf -> Bool) -> pf
mk_lits :: forall pf.
(JustPropositional pf, Ord pf) =>
Set pf -> (AtomOf pf -> Bool) -> pf
mk_lits Set pf
pvs AtomOf pf -> Bool
v = Set pf -> pf
forall (t :: * -> *) formula.
(Foldable t, IsFormula formula, IsPropositional formula) =>
t formula -> formula
list_conj ((pf -> pf) -> Set pf -> Set pf
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\ pf
p -> if pf -> (AtomOf pf -> Bool) -> Bool
forall pf.
JustPropositional pf =>
pf -> (AtomOf pf -> Bool) -> Bool
eval pf
p AtomOf pf -> Bool
v then pf
p else pf -> pf
forall formula. IsLiteral formula => formula -> formula
(.~.) pf
p) Set pf
pvs)

allsatvaluations :: Ord atom => ((atom -> Bool) -> Bool) -> (atom -> Bool) -> Set atom -> [atom -> Bool]
allsatvaluations :: forall atom.
Ord atom =>
((atom -> Bool) -> Bool)
-> (atom -> Bool) -> Set atom -> [atom -> Bool]
allsatvaluations (atom -> Bool) -> Bool
subfn atom -> Bool
v Set atom
pvs =
    case Set atom -> Maybe (atom, Set atom)
forall a. Set a -> Maybe (a, Set a)
Set.minView Set atom
pvs of
      Maybe (atom, Set atom)
Nothing -> if (atom -> Bool) -> Bool
subfn atom -> Bool
v then [atom -> Bool
v] else []
      Just (atom
p, Set atom
ps) -> (((atom -> Bool) -> Bool)
-> (atom -> Bool) -> Set atom -> [atom -> Bool]
forall atom.
Ord atom =>
((atom -> Bool) -> Bool)
-> (atom -> Bool) -> Set atom -> [atom -> Bool]
allsatvaluations (atom -> Bool) -> Bool
subfn (\atom
a -> if atom
a atom -> atom -> Bool
forall a. Eq a => a -> a -> Bool
== atom
p then Bool
False else atom -> Bool
v atom
a) Set atom
ps) [atom -> Bool] -> [atom -> Bool] -> [atom -> Bool]
forall a. [a] -> [a] -> [a]
++
                      (((atom -> Bool) -> Bool)
-> (atom -> Bool) -> Set atom -> [atom -> Bool]
forall atom.
Ord atom =>
((atom -> Bool) -> Bool)
-> (atom -> Bool) -> Set atom -> [atom -> Bool]
allsatvaluations (atom -> Bool) -> Bool
subfn (\atom
a -> if atom
a atom -> atom -> Bool
forall a. Eq a => a -> a -> Bool
== atom
p then Bool
True else atom -> Bool
v atom
a) Set atom
ps)

-- | Disjunctive normal form (DNF) via truth tables.
list_conj :: (Foldable t, IsFormula formula, IsPropositional formula) => t formula -> formula
list_conj :: forall (t :: * -> *) formula.
(Foldable t, IsFormula formula, IsPropositional formula) =>
t formula -> formula
list_conj t formula
l | t formula -> Bool
forall a. t a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null t formula
l = formula
forall formula. IsFormula formula => formula
true
list_conj t formula
l = (formula -> formula -> formula) -> t formula -> formula
forall a. (a -> a -> a) -> t a -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(.&.) t formula
l

list_disj :: (Foldable t, IsFormula formula, IsPropositional formula) => t formula -> formula
list_disj :: forall (t :: * -> *) formula.
(Foldable t, IsFormula formula, IsPropositional formula) =>
t formula -> formula
list_disj t formula
l | t formula -> Bool
forall a. t a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null t formula
l = formula
forall formula. IsFormula formula => formula
false
list_disj t formula
l = (formula -> formula -> formula) -> t formula -> formula
forall a. (a -> a -> a) -> t a -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(.|.) t formula
l

-- This is only used in the test below, its easier to match lists than sets.
dnfList :: JustPropositional pf => pf -> pf
dnfList :: forall pf. JustPropositional pf => pf -> pf
dnfList pf
fm =
    [pf] -> pf
forall (t :: * -> *) formula.
(Foldable t, IsFormula formula, IsPropositional formula) =>
t formula -> formula
list_disj (((AtomOf pf -> Bool) -> pf) -> [AtomOf pf -> Bool] -> [pf]
forall a b. (a -> b) -> [a] -> [b]
List.map ([pf] -> (AtomOf pf -> Bool) -> pf
forall pf.
JustPropositional pf =>
[pf] -> (AtomOf pf -> Bool) -> pf
mk_lits' ((AtomOf pf -> pf) -> [AtomOf pf] -> [pf]
forall a b. (a -> b) -> [a] -> [b]
List.map AtomOf pf -> pf
forall formula. IsFormula formula => AtomOf formula -> formula
atomic (Set (AtomOf pf) -> [AtomOf pf]
forall a. Set a -> [a]
Set.toAscList Set (AtomOf pf)
pvs))) [AtomOf pf -> Bool]
satvals)
     where
       satvals :: [AtomOf pf -> Bool]
satvals = ((AtomOf pf -> Bool) -> Bool)
-> (AtomOf pf -> Bool) -> Set (AtomOf pf) -> [AtomOf pf -> Bool]
forall atom.
Ord atom =>
((atom -> Bool) -> Bool)
-> (atom -> Bool) -> Set atom -> [atom -> Bool]
allsatvaluations (pf -> (AtomOf pf -> Bool) -> Bool
forall pf.
JustPropositional pf =>
pf -> (AtomOf pf -> Bool) -> Bool
eval pf
fm) (\AtomOf pf
_s -> Bool
False) Set (AtomOf pf)
pvs
       pvs :: Set (AtomOf pf)
pvs = pf -> Set (AtomOf pf)
forall formula.
IsFormula formula =>
formula -> Set (AtomOf formula)
atoms pf
fm
       mk_lits' :: JustPropositional pf => [pf] -> (AtomOf pf -> Bool) -> pf
       mk_lits' :: forall pf.
JustPropositional pf =>
[pf] -> (AtomOf pf -> Bool) -> pf
mk_lits' [pf]
pvs' AtomOf pf -> Bool
v = [pf] -> pf
forall (t :: * -> *) formula.
(Foldable t, IsFormula formula, IsPropositional formula) =>
t formula -> formula
list_conj ((pf -> pf) -> [pf] -> [pf]
forall a b. (a -> b) -> [a] -> [b]
List.map (\ pf
p -> if pf -> (AtomOf pf -> Bool) -> Bool
forall pf.
JustPropositional pf =>
pf -> (AtomOf pf -> Bool) -> Bool
eval pf
p AtomOf pf -> Bool
v then pf
p else pf -> pf
forall formula. IsLiteral formula => formula -> formula
(.~.) pf
p) [pf]
pvs')

-- Examples.

test29 :: Test
test29 :: Test
test29 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String
-> (PFormula Prop, TruthTable Prop)
-> (PFormula Prop, TruthTable Prop)
-> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"dnf 1 (p. 56)" (PFormula Prop, TruthTable Prop)
expected (PFormula Prop, TruthTable Prop)
input
    where input :: (PFormula Prop, TruthTable Prop)
input = (PFormula Prop -> PFormula Prop
forall pf. JustPropositional pf => pf -> pf
dnfList PFormula Prop
fm, PFormula Prop -> TruthTable (AtomOf (PFormula Prop))
forall pf. JustPropositional pf => pf -> TruthTable (AtomOf pf)
truthTable PFormula Prop
fm)
          expected :: (PFormula Prop, TruthTable Prop)
expected = (((((PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
p) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
q) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
r) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. ((PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
q)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
r))) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. ((PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
q) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
r)),
                      [Prop] -> [TruthTableRow] -> TruthTable Prop
forall a. [a] -> [TruthTableRow] -> TruthTable a
TruthTable
                      [String -> Prop
P String
"p", String -> Prop
P String
"q", String -> Prop
P String
"r"]
                      [([Bool
False,Bool
False,Bool
False],Bool
False),
                       ([Bool
False,Bool
False,Bool
True],Bool
False),
                       ([Bool
False,Bool
True,Bool
False],Bool
False),
                       ([Bool
False,Bool
True,Bool
True],Bool
True),
                       ([Bool
True,Bool
False,Bool
False],Bool
True),
                       ([Bool
True,Bool
False,Bool
True],Bool
False),
                       ([Bool
True,Bool
True,Bool
False],Bool
True),
                       ([Bool
True,Bool
True,Bool
True],Bool
False)])
          fm :: PFormula Prop
fm = (PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. PFormula Prop
q PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
r) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. ((PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.)PFormula Prop
p) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.)PFormula Prop
r))
          (PFormula Prop
p, PFormula Prop
q, PFormula Prop
r) = (Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"p"), Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"q"), Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"r"))

test30 :: Test
test30 :: Test
test30 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> PFormula Prop -> PFormula Prop -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"dnf 2 (p. 56)" PFormula Prop
expected PFormula Prop
input
    where input :: PFormula Prop
input = PFormula Prop -> PFormula Prop
forall pf. JustPropositional pf => pf -> pf
dnfList (PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
q PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
r PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
s PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
t PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
u PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. PFormula Prop
u PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
v :: PFormula Prop)
          expected :: PFormula Prop
expected = ((((((((((((((((((((((((((((((((((((((PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
p) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
q)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
r)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
s)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
t)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
u) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
v) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                                                    (((((((PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
p) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
q)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
r)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
s)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
t) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
u) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
v)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                                                   (((((((PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
p) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
q)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
r)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
s) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
t)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
u) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
v)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                                                  (((((((PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
p) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
q)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
r)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
s) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
t) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
u) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
v)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                                                 (((((((PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
p) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
q)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
r) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
s)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
t)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
u) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
v)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                                                (((((((PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
p) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
q)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
r) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
s)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
t) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
u) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
v)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                                               (((((((PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
p) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
q)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
r) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
s) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
t)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
u) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
v)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                                              (((((((PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
p) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
q)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
r) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
s) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
t) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
u) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
v)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                                             (((((((PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
p) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
q) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
r)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
s)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
t)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
u) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
v)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                                            (((((((PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
p) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
q) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
r)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
s)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
t) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
u) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
v)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                                           (((((((PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
p) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
q) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
r)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
s) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
t)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
u) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
v)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                                          (((((((PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
p) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
q) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
r)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
s) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
t) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
u) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
v)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                                         (((((((PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
p) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
q) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
r) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
s)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
t)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
u) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
v)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                                        (((((((PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
p) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
q) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
r) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
s)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
t) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
u) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
v)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                                       (((((((PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
p) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
q) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
r) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
s) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
t)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
u) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
v)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                                      (((((((PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
p) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
q) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
r) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
s) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
t) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
u) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
v)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                                     ((((((PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
q)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
r)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
s)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
t)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
u) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
v)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                                    ((((((PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
q)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
r)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
s)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
t) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
u) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
v)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                                   ((((((PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
q)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
r)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
s) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
t)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
u) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
v)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                                  ((((((PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
q)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
r)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
s) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
t) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
u) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
v)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                                 ((((((PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
q)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
r) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
s)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
t)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
u) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
v)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                                ((((((PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
q)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
r) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
s)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
t) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
u) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
v)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                               ((((((PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
q)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
r) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
s) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
t)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
u) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
v)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                              ((((((PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
q)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
r) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
s) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
t) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
u) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
v)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                             ((((((PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
q) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
r)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
s)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
t)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
u) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
v)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                            ((((((PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
q) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
r)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
s)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
t) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
u) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
v)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                           ((((((PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
q) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
r)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
s) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
t)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
u) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
v)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                          ((((((PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
q) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
r)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
s) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
t) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
u) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
v)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                         ((((((PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
q) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
r) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
s)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
t)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
u) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
v)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                        ((((((PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
q) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
r) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
s)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
t) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
u) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
v)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                       ((((((PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
q) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
r) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
s) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
t)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
u) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
v)) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                      ((((((PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
q) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
r) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
s) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
t) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
u) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
v))) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                     ((((((PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
q) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
r) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
s) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
t) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
u) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
v)
          [PFormula Prop
p, PFormula Prop
q, PFormula Prop
r, PFormula Prop
s, PFormula Prop
t, PFormula Prop
u, PFormula Prop
v] = (String -> PFormula Prop) -> [String] -> [PFormula Prop]
forall a b. (a -> b) -> [a] -> [b]
List.map (Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (Prop -> PFormula Prop)
-> (String -> Prop) -> String -> PFormula Prop
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Prop
P) [String
"p", String
"q", String
"r", String
"s", String
"t", String
"u", String
"v"]

-- | DNF via distribution.
distrib1 :: IsPropositional formula => formula -> formula
distrib1 :: forall formula. IsPropositional formula => formula -> formula
distrib1 formula
fm =
    (formula -> formula)
-> (formula -> formula -> formula)
-> (formula -> formula -> formula)
-> (formula -> formula -> formula)
-> (formula -> formula -> formula)
-> formula
-> formula
forall formula r.
IsPropositional formula =>
(formula -> r)
-> (formula -> formula -> r)
-> (formula -> formula -> r)
-> (formula -> formula -> r)
-> (formula -> formula -> r)
-> formula
-> r
forall r.
(formula -> r)
-> (formula -> formula -> r)
-> (formula -> formula -> r)
-> (formula -> formula -> r)
-> (formula -> formula -> r)
-> formula
-> r
foldCombination (\formula
_ -> formula
fm) (\formula
_ formula
_ -> formula
fm) formula -> formula -> formula
lhs (\formula
_ formula
_ -> formula
fm) (\formula
_ formula
_ -> formula
fm) formula
fm
    where
      -- p & (q | r) -> (p & q) | (p & r)
      lhs :: formula -> formula -> formula
lhs formula
p formula
qr = (formula -> formula)
-> (formula -> formula -> formula)
-> (formula -> formula -> formula)
-> (formula -> formula -> formula)
-> (formula -> formula -> formula)
-> formula
-> formula
forall formula r.
IsPropositional formula =>
(formula -> r)
-> (formula -> formula -> r)
-> (formula -> formula -> r)
-> (formula -> formula -> r)
-> (formula -> formula -> r)
-> formula
-> r
forall r.
(formula -> r)
-> (formula -> formula -> r)
-> (formula -> formula -> r)
-> (formula -> formula -> r)
-> (formula -> formula -> r)
-> formula
-> r
foldCombination (\formula
_ -> formula -> formula -> formula
rhs formula
p formula
qr)
                                 (\formula
q formula
r -> formula -> formula
forall formula. IsPropositional formula => formula -> formula
distrib1 (formula
p formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. formula
q) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. formula -> formula
forall formula. IsPropositional formula => formula -> formula
distrib1 (formula
p formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. formula
r))
                                 (\formula
_ formula
_ -> formula -> formula -> formula
rhs formula
p formula
qr)
                                 (\formula
_ formula
_ -> formula -> formula -> formula
rhs formula
p formula
qr)
                                 (\formula
_ formula
_ -> formula -> formula -> formula
rhs formula
p formula
qr)
                                 formula
qr
      -- (p | q) & r -> (p & r) | (q & r)
      rhs :: formula -> formula -> formula
rhs formula
pq formula
r = (formula -> formula)
-> (formula -> formula -> formula)
-> (formula -> formula -> formula)
-> (formula -> formula -> formula)
-> (formula -> formula -> formula)
-> formula
-> formula
forall formula r.
IsPropositional formula =>
(formula -> r)
-> (formula -> formula -> r)
-> (formula -> formula -> r)
-> (formula -> formula -> r)
-> (formula -> formula -> r)
-> formula
-> r
forall r.
(formula -> r)
-> (formula -> formula -> r)
-> (formula -> formula -> r)
-> (formula -> formula -> r)
-> (formula -> formula -> r)
-> formula
-> r
foldCombination (\formula
_ -> formula
fm)
                                 (\formula
p formula
q -> formula -> formula
forall formula. IsPropositional formula => formula -> formula
distrib1 (formula
p formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. formula
r) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. formula -> formula
forall formula. IsPropositional formula => formula -> formula
distrib1 (formula
q formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. formula
r))
                                 (\formula
_ formula
_ -> formula
fm)
                                 (\formula
_ formula
_ -> formula
fm)
                                 (\formula
_ formula
_ -> formula
fm)
                                 formula
pq
{-
distrib1 :: Formula atom -> Formula atom
distrib1 fm =
  case fm of
    And p (Or q r) -> Or (distrib1 (And p q)) (distrib1 (And p r))
    And (Or p q) r -> Or (distrib1 (And p r)) (distrib1 (And q r))
    _ -> fm
-}

rawdnf :: IsPropositional formula => formula -> formula
rawdnf :: forall formula. IsPropositional formula => formula -> formula
rawdnf formula
fm =
    (formula -> formula)
-> (formula -> BinOp -> formula -> formula)
-> (formula -> formula)
-> (Bool -> formula)
-> (AtomOf formula -> formula)
-> formula
-> formula
forall formula r.
IsPropositional formula =>
(formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
forall r.
(formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
foldPropositional' (\formula
_ -> formula
fm) formula -> BinOp -> formula -> formula
co (\formula
_ -> formula
fm) (\Bool
_ -> formula
fm) (\AtomOf formula
_ -> formula
fm) formula
fm
    where
      co :: formula -> BinOp -> formula -> formula
co formula
p BinOp
(:&:) formula
q = formula -> formula
forall formula. IsPropositional formula => formula -> formula
distrib1 (formula -> formula
forall formula. IsPropositional formula => formula -> formula
rawdnf formula
p formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. formula -> formula
forall formula. IsPropositional formula => formula -> formula
rawdnf formula
q)
      co formula
p BinOp
(:|:) formula
q = (formula -> formula
forall formula. IsPropositional formula => formula -> formula
rawdnf formula
p formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. formula -> formula
forall formula. IsPropositional formula => formula -> formula
rawdnf formula
q)
      co formula
_ BinOp
_ formula
_ = formula
fm
{-
rawdnf :: Ord atom => Formula atom -> Formula atom
rawdnf fm =
  case fm of
    And p q -> distrib1 (And (rawdnf p) (rawdnf q))
    Or p q -> Or (rawdnf p) (rawdnf q)
    _ -> fm
-}

-- Example.

test31 :: Test
test31 :: Test
test31 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> String -> String -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"rawdnf (p. 58)" (PFormula Prop -> String
forall a. Pretty a => a -> String
prettyShow PFormula Prop
expected) (PFormula Prop -> String
forall a. Pretty a => a -> String
prettyShow PFormula Prop
input)
    where input :: PFormula Prop
          input :: PFormula Prop
input = PFormula Prop -> PFormula Prop
forall formula. IsPropositional formula => formula -> formula
rawdnf (PFormula Prop -> PFormula Prop) -> PFormula Prop -> PFormula Prop
forall a b. (a -> b) -> a -> b
$ (PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. PFormula Prop
q PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
r) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. ((PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.)PFormula Prop
p) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.)PFormula Prop
r))
          expected :: PFormula Prop
          expected :: PFormula Prop
expected = ((AtomOf (PFormula Prop) -> PFormula Prop
forall formula. IsFormula formula => AtomOf formula -> formula
atomic (String -> Prop
P String
"p")) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.)(AtomOf (PFormula Prop) -> PFormula Prop
forall formula. IsFormula formula => AtomOf formula -> formula
atomic (String -> Prop
P String
"p"))) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                      ((AtomOf (PFormula Prop) -> PFormula Prop
forall formula. IsFormula formula => AtomOf formula -> formula
atomic (String -> Prop
P String
"q")) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (AtomOf (PFormula Prop) -> PFormula Prop
forall formula. IsFormula formula => AtomOf formula -> formula
atomic (String -> Prop
P String
"r"))) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.)(AtomOf (PFormula Prop) -> PFormula Prop
forall formula. IsFormula formula => AtomOf formula -> formula
atomic (String -> Prop
P String
"p")))) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                     ((AtomOf (PFormula Prop) -> PFormula Prop
forall formula. IsFormula formula => AtomOf formula -> formula
atomic (String -> Prop
P String
"p")) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.)(AtomOf (PFormula Prop) -> PFormula Prop
forall formula. IsFormula formula => AtomOf formula -> formula
atomic (String -> Prop
P String
"r"))) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                      ((AtomOf (PFormula Prop) -> PFormula Prop
forall formula. IsFormula formula => AtomOf formula -> formula
atomic (String -> Prop
P String
"q")) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (AtomOf (PFormula Prop) -> PFormula Prop
forall formula. IsFormula formula => AtomOf formula -> formula
atomic (String -> Prop
P String
"r"))) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.)(AtomOf (PFormula Prop) -> PFormula Prop
forall formula. IsFormula formula => AtomOf formula -> formula
atomic (String -> Prop
P String
"r"))))
          (PFormula Prop
p, PFormula Prop
q, PFormula Prop
r) = (Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"p"), Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"q"), Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"r"))

purednf :: (JustPropositional pf,
            IsLiteral lit, JustLiteral lit, Ord lit) => (AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
purednf :: forall pf lit.
(JustPropositional pf, IsLiteral lit, JustLiteral lit, Ord lit) =>
(AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
purednf AtomOf pf -> AtomOf lit
ca pf
fm =
    (pf -> BinOp -> pf -> Set (Set lit))
-> (pf -> Set (Set lit))
-> (Bool -> Set (Set lit))
-> (AtomOf pf -> Set (Set lit))
-> pf
-> Set (Set lit)
forall pf r.
JustPropositional pf =>
(pf -> BinOp -> pf -> r)
-> (pf -> r) -> (Bool -> r) -> (AtomOf pf -> r) -> pf -> r
foldPropositional pf -> BinOp -> pf -> Set (Set lit)
co (\pf
_ -> pf -> Set (Set lit)
l2f pf
fm) (\Bool
_ -> pf -> Set (Set lit)
l2f pf
fm) (\AtomOf pf
_ -> pf -> Set (Set lit)
l2f pf
fm) pf
fm
    where
      l2f :: pf -> Set (Set lit)
l2f pf
f = Set lit -> Set (Set lit)
forall a. a -> Set a
singleton (Set lit -> Set (Set lit))
-> (pf -> Set lit) -> pf -> Set (Set lit)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. lit -> Set lit
forall a. a -> Set a
singleton (lit -> Set lit) -> (pf -> lit) -> pf -> Set lit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (pf -> lit) -> (AtomOf pf -> AtomOf lit) -> pf -> lit
forall formula lit.
(IsLiteral formula, JustLiteral lit) =>
(formula -> lit)
-> (AtomOf formula -> AtomOf lit) -> formula -> lit
convertToLiteral (String -> pf -> lit
forall a. HasCallStack => String -> a
error (String -> pf -> lit) -> String -> pf -> lit
forall a b. (a -> b) -> a -> b
$ String
"purednf failure: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ pf -> String
forall a. Pretty a => a -> String
prettyShow pf
f) AtomOf pf -> AtomOf lit
ca (pf -> Set (Set lit)) -> pf -> Set (Set lit)
forall a b. (a -> b) -> a -> b
$ pf
f
      co :: pf -> BinOp -> pf -> Set (Set lit)
co pf
p BinOp
(:&:) pf
q = Set (Set lit) -> Set (Set lit) -> Set (Set lit)
forall a. Ord a => Set (Set a) -> Set (Set a) -> Set (Set a)
distrib ((AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
forall pf lit.
(JustPropositional pf, IsLiteral lit, JustLiteral lit, Ord lit) =>
(AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
purednf AtomOf pf -> AtomOf lit
ca pf
p) ((AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
forall pf lit.
(JustPropositional pf, IsLiteral lit, JustLiteral lit, Ord lit) =>
(AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
purednf AtomOf pf -> AtomOf lit
ca pf
q)
      co pf
p BinOp
(:|:) pf
q = Set (Set lit) -> Set (Set lit) -> Set (Set lit)
forall a. Ord a => Set a -> Set a -> Set a
union ((AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
forall pf lit.
(JustPropositional pf, IsLiteral lit, JustLiteral lit, Ord lit) =>
(AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
purednf AtomOf pf -> AtomOf lit
ca pf
p) ((AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
forall pf lit.
(JustPropositional pf, IsLiteral lit, JustLiteral lit, Ord lit) =>
(AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
purednf AtomOf pf -> AtomOf lit
ca pf
q)
      co pf
_ BinOp
_ pf
_ = pf -> Set (Set lit)
l2f pf
fm

-- Example.

test32 :: Test
test32 :: Test
test32 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String
-> Set (Set (LFormula Prop))
-> Set (Set (LFormula Prop))
-> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"purednf (p. 58)" Set (Set (LFormula Prop))
expected ((AtomOf (PFormula Prop) -> AtomOf (LFormula Prop))
-> PFormula Prop -> Set (Set (LFormula Prop))
forall pf lit.
(JustPropositional pf, IsLiteral lit, JustLiteral lit, Ord lit) =>
(AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
purednf AtomOf (PFormula Prop) -> AtomOf (LFormula Prop)
Prop -> Prop
forall {a}. a -> a
id PFormula Prop
fm)
    where fm :: PFormula Prop
          fm :: PFormula Prop
fm = (PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. PFormula Prop
q PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
r) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. ((PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.)PFormula Prop
p) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.)PFormula Prop
r))
          expected :: Set (Set (LFormula Prop))
          expected :: Set (Set (LFormula Prop))
expected = (Set (PFormula Prop) -> Set (LFormula Prop))
-> Set (Set (PFormula Prop)) -> Set (Set (LFormula Prop))
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ((PFormula Prop -> LFormula Prop)
-> Set (PFormula Prop) -> Set (LFormula Prop)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ((PFormula Prop -> LFormula Prop)
-> (AtomOf (PFormula Prop) -> AtomOf (LFormula Prop))
-> PFormula Prop
-> LFormula Prop
forall formula lit.
(IsLiteral formula, JustLiteral lit) =>
(formula -> lit)
-> (AtomOf formula -> AtomOf lit) -> formula -> lit
convertToLiteral (String -> PFormula Prop -> LFormula Prop
forall a. HasCallStack => String -> a
error String
"test32") AtomOf (PFormula Prop) -> AtomOf (LFormula Prop)
Prop -> Prop
forall {a}. a -> a
id)) (Set (Set (PFormula Prop)) -> Set (Set (LFormula Prop)))
-> Set (Set (PFormula Prop)) -> Set (Set (LFormula Prop))
forall a b. (a -> b) -> a -> b
$
                     [Set (PFormula Prop)] -> Set (Set (PFormula Prop))
forall a. Ord a => [a] -> Set a
Set.fromList [[PFormula Prop] -> Set (PFormula Prop)
forall a. Ord a => [a] -> Set a
Set.fromList [PFormula Prop
p, PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
p],
                                   [PFormula Prop] -> Set (PFormula Prop)
forall a. Ord a => [a] -> Set a
Set.fromList [PFormula Prop
p, PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
r],
                                   [PFormula Prop] -> Set (PFormula Prop)
forall a. Ord a => [a] -> Set a
Set.fromList [PFormula Prop
q, PFormula Prop
r, PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
p],
                                   [PFormula Prop] -> Set (PFormula Prop)
forall a. Ord a => [a] -> Set a
Set.fromList [PFormula Prop
q, PFormula Prop
r, PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
r]]
          p :: PFormula Prop
p = AtomOf (PFormula Prop) -> PFormula Prop
forall formula. IsFormula formula => AtomOf formula -> formula
atomic (String -> Prop
P String
"p")
          q :: PFormula Prop
q = AtomOf (PFormula Prop) -> PFormula Prop
forall formula. IsFormula formula => AtomOf formula -> formula
atomic (String -> Prop
P String
"q")
          r :: PFormula Prop
r = AtomOf (PFormula Prop) -> PFormula Prop
forall formula. IsFormula formula => AtomOf formula -> formula
atomic (String -> Prop
P String
"r")

-- | Filtering out trivial disjuncts (in this guise, contradictory).
trivial :: (Ord lit, IsLiteral lit) => Set lit -> Bool
trivial :: forall lit. (Ord lit, IsLiteral lit) => Set lit -> Bool
trivial Set lit
lits =
    let (Set lit
pos, Set lit
neg) = (lit -> Bool) -> Set lit -> (Set lit, Set lit)
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.partition lit -> Bool
forall formula. IsLiteral formula => formula -> Bool
positive Set lit
lits in
    (Bool -> Bool
not (Bool -> Bool) -> (Set lit -> Bool) -> Set lit -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set lit -> Bool
forall a. Set a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Set lit -> Bool) -> (Set lit -> Set lit) -> Set lit -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set lit -> Set lit -> Set lit
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set lit
neg (Set lit -> Set lit) -> (Set lit -> Set lit) -> Set lit -> Set lit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (lit -> lit) -> Set lit -> Set lit
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map lit -> lit
forall formula. IsLiteral formula => formula -> formula
(.~.)) Set lit
pos

-- Example.
test33 :: Test
test33 :: Test
test33 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String
-> Set (Set (LFormula Prop))
-> Set (Set (LFormula Prop))
-> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"trivial" Set (Set (LFormula Prop))
expected ((Set (LFormula Prop) -> Bool)
-> Set (Set (LFormula Prop)) -> Set (Set (LFormula Prop))
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Bool -> Bool
not (Bool -> Bool)
-> (Set (LFormula Prop) -> Bool) -> Set (LFormula Prop) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (LFormula Prop) -> Bool
forall lit. (Ord lit, IsLiteral lit) => Set lit -> Bool
trivial) ((AtomOf (PFormula Prop) -> AtomOf (LFormula Prop))
-> PFormula Prop -> Set (Set (LFormula Prop))
forall pf lit.
(JustPropositional pf, IsLiteral lit, JustLiteral lit, Ord lit) =>
(AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
purednf AtomOf (PFormula Prop) -> AtomOf (LFormula Prop)
Prop -> Prop
forall {a}. a -> a
id PFormula Prop
fm))
    where expected :: Set (Set (LFormula Prop))
          expected :: Set (Set (LFormula Prop))
expected = (Set (PFormula Prop) -> Set (LFormula Prop))
-> Set (Set (PFormula Prop)) -> Set (Set (LFormula Prop))
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ((PFormula Prop -> LFormula Prop)
-> Set (PFormula Prop) -> Set (LFormula Prop)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ((PFormula Prop -> LFormula Prop)
-> (AtomOf (PFormula Prop) -> AtomOf (LFormula Prop))
-> PFormula Prop
-> LFormula Prop
forall formula lit.
(IsLiteral formula, JustLiteral lit) =>
(formula -> lit)
-> (AtomOf formula -> AtomOf lit) -> formula -> lit
convertToLiteral (String -> PFormula Prop -> LFormula Prop
forall a. HasCallStack => String -> a
error String
"test32") AtomOf (PFormula Prop) -> AtomOf (LFormula Prop)
Prop -> Prop
forall {a}. a -> a
id)) (Set (Set (PFormula Prop)) -> Set (Set (LFormula Prop)))
-> Set (Set (PFormula Prop)) -> Set (Set (LFormula Prop))
forall a b. (a -> b) -> a -> b
$
                     [Set (PFormula Prop)] -> Set (Set (PFormula Prop))
forall a. Ord a => [a] -> Set a
Set.fromList [[PFormula Prop] -> Set (PFormula Prop)
forall a. Ord a => [a] -> Set a
Set.fromList [PFormula Prop
p,PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
r],
                                   [PFormula Prop] -> Set (PFormula Prop)
forall a. Ord a => [a] -> Set a
Set.fromList [PFormula Prop
q,PFormula Prop
r,PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.) PFormula Prop
p]]
          fm :: PFormula Prop
          fm :: PFormula Prop
fm = (PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. PFormula Prop
q PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
r) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. ((PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.)PFormula Prop
p) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.)PFormula Prop
r))
          p :: PFormula Prop
p = AtomOf (PFormula Prop) -> PFormula Prop
forall formula. IsFormula formula => AtomOf formula -> formula
atomic (String -> Prop
P String
"p") :: PFormula Prop
          q :: PFormula Prop
q = AtomOf (PFormula Prop) -> PFormula Prop
forall formula. IsFormula formula => AtomOf formula -> formula
atomic (String -> Prop
P String
"q") :: PFormula Prop
          r :: PFormula Prop
r = AtomOf (PFormula Prop) -> PFormula Prop
forall formula. IsFormula formula => AtomOf formula -> formula
atomic (String -> Prop
P String
"r") :: PFormula Prop

-- | With subsumption checking, done very naively (quadratic).
simpdnf :: (JustPropositional pf,
            IsLiteral lit, JustLiteral lit, Ord lit
           ) => (AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
simpdnf :: forall pf lit.
(JustPropositional pf, IsLiteral lit, JustLiteral lit, Ord lit) =>
(AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
simpdnf AtomOf pf -> AtomOf lit
ca pf
fm =
    (pf -> BinOp -> pf -> Set (Set lit))
-> (pf -> Set (Set lit))
-> (Bool -> Set (Set lit))
-> (AtomOf pf -> Set (Set lit))
-> pf
-> Set (Set lit)
forall pf r.
JustPropositional pf =>
(pf -> BinOp -> pf -> r)
-> (pf -> r) -> (Bool -> r) -> (AtomOf pf -> r) -> pf -> r
foldPropositional (\pf
_ BinOp
_ pf
_ -> Set (Set lit)
go) (\pf
_ -> Set (Set lit)
go) Bool -> Set (Set lit)
forall {a}. Bool -> Set (Set a)
tf (\AtomOf pf
_ -> Set (Set lit)
go) pf
fm
    where
      tf :: Bool -> Set (Set a)
tf Bool
False = Set (Set a)
forall a. Set a
Set.empty
      tf Bool
True = Set a -> Set (Set a)
forall a. a -> Set a
singleton Set a
forall a. Set a
Set.empty
      go :: Set (Set lit)
go = let djs :: Set (Set lit)
djs = (Set lit -> Bool) -> Set (Set lit) -> Set (Set lit)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Bool -> Bool
not (Bool -> Bool) -> (Set lit -> Bool) -> Set lit -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set lit -> Bool
forall lit. (Ord lit, IsLiteral lit) => Set lit -> Bool
trivial) ((AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
forall pf lit.
(JustPropositional pf, IsLiteral lit, JustLiteral lit, Ord lit) =>
(AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
purednf AtomOf pf -> AtomOf lit
ca (pf -> pf
forall pf. JustPropositional pf => pf -> pf
nnf pf
fm)) in
           (Set lit -> Bool) -> Set (Set lit) -> Set (Set lit)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\Set lit
d -> Bool -> Bool
not ((Set lit -> Bool) -> Set (Set lit) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
setAny (\Set lit
d' -> Set lit -> Set lit -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isProperSubsetOf Set lit
d' Set lit
d) Set (Set lit)
djs)) Set (Set lit)
djs

-- | Mapping back to a formula.
dnf :: forall pf. (JustPropositional pf, Ord pf) => pf -> pf
dnf :: forall pf. (JustPropositional pf, Ord pf) => pf -> pf
dnf pf
fm = ([pf] -> pf
forall (t :: * -> *) formula.
(Foldable t, IsFormula formula, IsPropositional formula) =>
t formula -> formula
list_disj ([pf] -> pf) -> (pf -> [pf]) -> pf -> pf
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set pf -> [pf]
forall a. Set a -> [a]
Set.toAscList (Set pf -> [pf]) -> (pf -> Set pf) -> pf -> [pf]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set pf -> pf) -> Set (Set pf) -> Set pf
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Set pf -> pf
forall (t :: * -> *) formula.
(Foldable t, IsFormula formula, IsPropositional formula) =>
t formula -> formula
list_conj (Set (Set pf) -> Set pf) -> (pf -> Set (Set pf)) -> pf -> Set pf
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
          (Set (LFormula (AtomOf pf)) -> Set pf)
-> Set (Set (LFormula (AtomOf pf))) -> Set (Set pf)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ((LFormula (AtomOf pf) -> pf)
-> Set (LFormula (AtomOf pf)) -> Set pf
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ((AtomOf (LFormula (AtomOf pf)) -> AtomOf pf)
-> LFormula (AtomOf pf) -> pf
forall lit1 lit2.
(JustLiteral lit1, IsLiteral lit2) =>
(AtomOf lit1 -> AtomOf lit2) -> lit1 -> lit2
convertLiteral AtomOf pf -> AtomOf pf
AtomOf (LFormula (AtomOf pf)) -> AtomOf pf
forall {a}. a -> a
id :: LFormula (AtomOf pf) -> pf)) (Set (Set (LFormula (AtomOf pf))) -> Set (Set pf))
-> (pf -> Set (Set (LFormula (AtomOf pf)))) -> pf -> Set (Set pf)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AtomOf pf -> AtomOf (LFormula (AtomOf pf)))
-> pf -> Set (Set (LFormula (AtomOf pf)))
forall pf lit.
(JustPropositional pf, IsLiteral lit, JustLiteral lit, Ord lit) =>
(AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
simpdnf AtomOf pf -> AtomOf pf
AtomOf pf -> AtomOf (LFormula (AtomOf pf))
forall {a}. a -> a
id) pf
fm

-- Example. (p. 56)
test34 :: Test
test34 :: Test
test34 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> (String, Bool) -> (String, Bool) -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"dnf (p. 56)" (String, Bool)
expected (String, Bool)
input
    where input :: (String, Bool)
input = (PFormula Prop -> String
forall a. Pretty a => a -> String
prettyShow (PFormula Prop -> PFormula Prop
forall pf. (JustPropositional pf, Ord pf) => pf -> pf
dnf PFormula Prop
fm), PFormula Prop -> Bool
forall pf. JustPropositional pf => pf -> Bool
tautology (PFormula Prop -> PFormula Prop -> PFormula Prop
forall atom. PFormula atom -> PFormula atom -> PFormula atom
Iff PFormula Prop
fm (PFormula Prop -> PFormula Prop
forall pf. (JustPropositional pf, Ord pf) => pf -> pf
dnf PFormula Prop
fm)))
          expected :: (String, Bool)
expected = (String
"(p∧¬r)∨(q∧r∧¬p)",Bool
True)
          fm :: PFormula Prop
fm = let (PFormula Prop
p, PFormula Prop
q, PFormula Prop
r) = (Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"p"), Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"q"), Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"r")) in
               (PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. PFormula Prop
q PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
r) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. ((PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.)PFormula Prop
p) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.)PFormula Prop
r))

-- | Conjunctive normal form (CNF) by essentially the same code. (p. 60)
purecnf :: (JustPropositional pf, JustLiteral lit, Ord lit) =>
           (AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
purecnf :: forall pf lit.
(JustPropositional pf, JustLiteral lit, Ord lit) =>
(AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
purecnf AtomOf pf -> AtomOf lit
ca pf
fm = (Set lit -> Set lit) -> Set (Set lit) -> Set (Set lit)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ((lit -> lit) -> Set lit -> Set lit
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map lit -> lit
forall formula. IsLiteral formula => formula -> formula
negate) ((AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
forall pf lit.
(JustPropositional pf, IsLiteral lit, JustLiteral lit, Ord lit) =>
(AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
purednf AtomOf pf -> AtomOf lit
ca (pf -> pf
forall pf. JustPropositional pf => pf -> pf
nnf (pf -> pf
forall formula. IsLiteral formula => formula -> formula
(.~.) pf
fm)))

simpcnf :: (JustPropositional pf, JustLiteral lit, Ord lit) =>
           (AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
simpcnf :: forall pf lit.
(JustPropositional pf, JustLiteral lit, Ord lit) =>
(AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
simpcnf AtomOf pf -> AtomOf lit
ca pf
fm =
    (pf -> BinOp -> pf -> Set (Set lit))
-> (pf -> Set (Set lit))
-> (Bool -> Set (Set lit))
-> (AtomOf pf -> Set (Set lit))
-> pf
-> Set (Set lit)
forall pf r.
JustPropositional pf =>
(pf -> BinOp -> pf -> r)
-> (pf -> r) -> (Bool -> r) -> (AtomOf pf -> r) -> pf -> r
foldPropositional (\pf
_ BinOp
_ pf
_ -> Set (Set lit)
go) (\pf
_ -> Set (Set lit)
go) Bool -> Set (Set lit)
forall {a}. Bool -> Set (Set a)
tf (\AtomOf pf
_ -> Set (Set lit)
go) pf
fm
    where
      tf :: Bool -> Set (Set a)
tf Bool
False = Set a -> Set (Set a)
forall a. a -> Set a
singleton Set a
forall a. Set a
Set.empty
      tf Bool
True = Set (Set a)
forall a. Set a
Set.empty
      go :: Set (Set lit)
go = let cjs :: Set (Set lit)
cjs = (Set lit -> Bool) -> Set (Set lit) -> Set (Set lit)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Bool -> Bool
not (Bool -> Bool) -> (Set lit -> Bool) -> Set lit -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set lit -> Bool
forall lit. (Ord lit, IsLiteral lit) => Set lit -> Bool
trivial) ((AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
forall pf lit.
(JustPropositional pf, JustLiteral lit, Ord lit) =>
(AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
purecnf AtomOf pf -> AtomOf lit
ca pf
fm) in
           (Set lit -> Bool) -> Set (Set lit) -> Set (Set lit)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\Set lit
c -> Bool -> Bool
not ((Set lit -> Bool) -> Set (Set lit) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
setAny (\Set lit
c' -> Set lit -> Set lit -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isProperSubsetOf Set lit
c' Set lit
c) Set (Set lit)
cjs)) Set (Set lit)
cjs

cnf_ :: (IsPropositional pf, Ord pf, JustLiteral lit) => (AtomOf lit -> AtomOf pf) -> Set (Set lit) -> pf
cnf_ :: forall pf lit.
(IsPropositional pf, Ord pf, JustLiteral lit) =>
(AtomOf lit -> AtomOf pf) -> Set (Set lit) -> pf
cnf_ AtomOf lit -> AtomOf pf
ca = Set pf -> pf
forall (t :: * -> *) formula.
(Foldable t, IsFormula formula, IsPropositional formula) =>
t formula -> formula
list_conj (Set pf -> pf) -> (Set (Set lit) -> Set pf) -> Set (Set lit) -> pf
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set lit -> pf) -> Set (Set lit) -> Set pf
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Set pf -> pf
forall (t :: * -> *) formula.
(Foldable t, IsFormula formula, IsPropositional formula) =>
t formula -> formula
list_disj (Set pf -> pf) -> (Set lit -> Set pf) -> Set lit -> pf
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (lit -> pf) -> Set lit -> Set pf
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ((AtomOf lit -> AtomOf pf) -> lit -> pf
forall lit1 lit2.
(JustLiteral lit1, IsLiteral lit2) =>
(AtomOf lit1 -> AtomOf lit2) -> lit1 -> lit2
convertLiteral AtomOf lit -> AtomOf pf
ca))

cnf' :: forall pf. (JustPropositional pf, Ord pf) => pf -> pf
cnf' :: forall pf. (JustPropositional pf, Ord pf) => pf -> pf
cnf' pf
fm = (Set pf -> pf
forall (t :: * -> *) formula.
(Foldable t, IsFormula formula, IsPropositional formula) =>
t formula -> formula
list_conj (Set pf -> pf) -> (pf -> Set pf) -> pf -> pf
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set pf -> pf) -> Set (Set pf) -> Set pf
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Set pf -> pf
forall (t :: * -> *) formula.
(Foldable t, IsFormula formula, IsPropositional formula) =>
t formula -> formula
list_disj (Set (Set pf) -> Set pf) -> (pf -> Set (Set pf)) -> pf -> Set pf
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set (LFormula (AtomOf pf)) -> Set pf)
-> Set (Set (LFormula (AtomOf pf))) -> Set (Set pf)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ((LFormula (AtomOf pf) -> pf)
-> Set (LFormula (AtomOf pf)) -> Set pf
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ((AtomOf (LFormula (AtomOf pf)) -> AtomOf pf)
-> LFormula (AtomOf pf) -> pf
forall lit1 lit2.
(JustLiteral lit1, IsLiteral lit2) =>
(AtomOf lit1 -> AtomOf lit2) -> lit1 -> lit2
convertLiteral AtomOf pf -> AtomOf pf
AtomOf (LFormula (AtomOf pf)) -> AtomOf pf
forall {a}. a -> a
id :: LFormula (AtomOf pf) -> pf)) (Set (Set (LFormula (AtomOf pf))) -> Set (Set pf))
-> (pf -> Set (Set (LFormula (AtomOf pf)))) -> pf -> Set (Set pf)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AtomOf pf -> AtomOf (LFormula (AtomOf pf)))
-> pf -> Set (Set (LFormula (AtomOf pf)))
forall pf lit.
(JustPropositional pf, JustLiteral lit, Ord lit) =>
(AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
simpcnf AtomOf pf -> AtomOf pf
AtomOf pf -> AtomOf (LFormula (AtomOf pf))
forall {a}. a -> a
id) pf
fm

-- Example. (p. 61)
test35 :: Test
test35 :: Test
test35 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> (String, Bool) -> (String, Bool) -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"cnf (p. 61)" (String, Bool)
expected (String, Bool)
input
    where input :: (String, Bool)
input = (PFormula Prop -> String
forall a. Pretty a => a -> String
prettyShow (PFormula Prop -> PFormula Prop
forall pf. (JustPropositional pf, Ord pf) => pf -> pf
cnf' PFormula Prop
fm), PFormula Prop -> Bool
forall pf. JustPropositional pf => pf -> Bool
tautology (PFormula Prop -> PFormula Prop -> PFormula Prop
forall atom. PFormula atom -> PFormula atom -> PFormula atom
Iff PFormula Prop
fm (PFormula Prop -> PFormula Prop
forall pf. (JustPropositional pf, Ord pf) => pf -> pf
cnf' PFormula Prop
fm)))
          expected :: (String, Bool)
expected = (String
"(p∨q)∧(p∨r)∧(¬p∨¬r)", Bool
True)
          fm :: PFormula Prop
          fm :: PFormula Prop
fm = (PFormula Prop
p PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. PFormula Prop
q PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PFormula Prop
r) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. ((PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.)PFormula Prop
p) PFormula Prop -> PFormula Prop -> PFormula Prop
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. (PFormula Prop -> PFormula Prop
forall formula. IsLiteral formula => formula -> formula
(.~.)PFormula Prop
r))
          [PFormula Prop
p, PFormula Prop
q, PFormula Prop
r] = [Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"p"), Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"q"), Prop -> PFormula Prop
forall atom. atom -> PFormula atom
Atom (String -> Prop
P String
"r")]

test36, test37 :: Test
test36 :: Test
test36 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> (String, Bool) -> (String, Bool) -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"cnf (trivial case: False)" (String, Bool)
expected (String, Bool)
input
    where input :: (String, Bool)
input = (PFormula Prop -> String
forall a. Pretty a => a -> String
prettyShow (PFormula Prop -> PFormula Prop
forall pf. (JustPropositional pf, Ord pf) => pf -> pf
cnf' PFormula Prop
fm), PFormula Prop -> Bool
forall pf. JustPropositional pf => pf -> Bool
tautology (PFormula Prop -> PFormula Prop -> PFormula Prop
forall atom. PFormula atom -> PFormula atom -> PFormula atom
Iff PFormula Prop
fm (PFormula Prop -> PFormula Prop
forall pf. (JustPropositional pf, Ord pf) => pf -> pf
cnf' PFormula Prop
fm)))
          expected :: (String, Bool)
expected = (String
"⊥", Bool
True)
          fm :: PFormula Prop
          fm :: PFormula Prop
fm = PFormula Prop
forall atom. PFormula atom
F
test37 :: Test
test37 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> (String, Bool) -> (String, Bool) -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"cnf (trivial case: True)" (String, Bool)
expected (String, Bool)
input
    where input :: (String, Bool)
input = (PFormula Prop -> String
forall a. Pretty a => a -> String
prettyShow (PFormula Prop -> PFormula Prop
forall pf. (JustPropositional pf, Ord pf) => pf -> pf
cnf' PFormula Prop
fm), PFormula Prop -> Bool
forall pf. JustPropositional pf => pf -> Bool
tautology (PFormula Prop -> PFormula Prop -> PFormula Prop
forall atom. PFormula atom -> PFormula atom -> PFormula atom
Iff PFormula Prop
fm (PFormula Prop -> PFormula Prop
forall pf. (JustPropositional pf, Ord pf) => pf -> pf
cnf' PFormula Prop
fm)))
          expected :: (String, Bool)
expected = (String
"⊤", Bool
True)
          fm :: PFormula Prop
          fm :: PFormula Prop
fm = PFormula Prop
forall atom. PFormula atom
T

testProp :: Test
testProp :: Test
testProp = String -> Test -> Test
TestLabel String
"Prop" (Test -> Test) -> Test -> Test
forall a b. (a -> b) -> a -> b
$
           [Test] -> Test
TestList [Test
test00, Test
test01, Test
test02, Test
test03, Test
test04, {-test05,-}
                     Test
test06, Test
test07, Test
test08, Test
test09, Test
test10,
                     Test
test11, Test
test12, Test
test13, Test
test14, Test
test15,
                     Test
test16, Test
test17, Test
test18, Test
test19, Test
test20,
                     Test
test21, Test
test22, Test
test23, Test
test24, Test
test25,
                     Test
test26, Test
test27, Test
test28, Test
test29, Test
test30,
                     Test
test31, Test
test32, Test
test33, Test
test34, Test
test35,
                     Test
test36, Test
test37]