{-# 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
(
IsPropositional((.|.), (.&.), (.<=>.), (.=>.), foldPropositional', foldCombination)
, BinOp(..), binop
, (⇒), (==>), (⊃), (→)
, (⇔), (<=>), (↔), (<==>)
, (∧), (·)
, (∨)
, foldPropositional
, zipPropositional
, convertPropositional
, convertToPropositional
, precedencePropositional
, associativityPropositional
, prettyPropositional
, showPropositional
, onatomsPropositional
, overatomsPropositional
, JustPropositional
, eval
, atoms
, TruthTable(TruthTable)
, onallvaluations
, truthTable
, tautology
, unsatisfiable
, satisfiable
, psubst
, dual
, psimplify
, psimplify1
, nnf
, nenf
, list_conj
, list_disj
, mk_lits
, allsatvaluations
, dnfSet
, purednf
, simpdnf
, rawdnf
, dnf
, purecnf
, simpcnf
, cnf'
, cnf_
, trivial
, Prop(P, pname)
, PFormula(F, T, Atom, Not, And, Or, Imp, Iff)
, 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
class IsLiteral formula => IsPropositional formula where
(.|.) :: formula -> formula -> formula
(.&.) :: formula -> formula -> formula
(.<=>.) :: formula -> formula -> formula
(.=>.) :: formula -> formula -> formula
foldPropositional' :: (formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula -> r
foldCombination :: (formula -> r)
-> (formula -> formula -> r)
-> (formula -> formula -> r)
-> (formula -> formula -> r)
-> (formula -> formula -> r)
-> formula -> r
(⇒), (⊃), (==>), (→) :: 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 .=>., ⇒, ⊃, ==>, →
(<=>), (<==>), (⇔), (↔) :: 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 .<=>., <=>, <==>, ⇔, ↔
(∧), (·) :: 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 .&., ∧, ·
(∨) :: IsPropositional formula => formula -> formula -> formula
∨ :: forall formula.
IsPropositional formula =>
formula -> formula -> formula
(∨) = formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(.|.)
infixl 4 .|., ∨
foldPropositional :: JustPropositional pf =>
(pf -> BinOp -> pf -> r)
-> (pf -> r)
-> (Bool -> r)
-> (AtomOf pf -> r)
-> 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")
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)
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
zipPropositional :: (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 :: 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
convertPropositional :: (JustPropositional pf1, IsPropositional pf2) =>
(AtomOf pf1 -> AtomOf pf2)
-> 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
convertToPropositional :: (IsPropositional formula, JustPropositional pf) =>
(formula -> pf)
-> (AtomOf formula -> AtomOf pf)
-> 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
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
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
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
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)
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
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)
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
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
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)
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
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 IsPropositional formula => JustPropositional formula
instance IsAtom atom => JustPropositional (PFormula atom)
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
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)
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)
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)
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])
test00 :: Test
test00 :: Test
test00 =
[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
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"))
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 = (
String
"p⇒q⇔(r∧s)∨(t⇔u∧v)",
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")))
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)
, ( (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)
, ( 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)
]
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"))
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"))
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")
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"))
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)
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"))
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"))
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"))
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 .<=>."
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"})))
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)
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")
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
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
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
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
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)
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)
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
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')
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"]
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
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
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
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
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
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")
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
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
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
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
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))
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
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,
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]