{- |
Description: Definition and operations of propositional logic.
License: GNU LGPLv3
Maintainer: paul.bittner@uni-ulm.de

Definition and operations of propositional logic.
-}
module Propositions where

import Logic
import Data.List ( intercalate )

-- | Sum type similar to a grammar for building propositional formulas.
data PropositionalFormula a =
      PTrue
    | PFalse
    | PVariable a
    | PNot (PropositionalFormula a)
    | PAnd [PropositionalFormula a]
    | POr [PropositionalFormula a]
    deriving (PropositionalFormula a -> PropositionalFormula a -> Bool
(PropositionalFormula a -> PropositionalFormula a -> Bool)
-> (PropositionalFormula a -> PropositionalFormula a -> Bool)
-> Eq (PropositionalFormula a)
forall a.
Eq a =>
PropositionalFormula a -> PropositionalFormula a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PropositionalFormula a -> PropositionalFormula a -> Bool
$c/= :: forall a.
Eq a =>
PropositionalFormula a -> PropositionalFormula a -> Bool
== :: PropositionalFormula a -> PropositionalFormula a -> Bool
$c== :: forall a.
Eq a =>
PropositionalFormula a -> PropositionalFormula a -> Bool
Eq)

-- | 'PropositionalFormula's form a 'Logic'.
instance Logic (PropositionalFormula a) where
    ltrue :: PropositionalFormula a
ltrue = PropositionalFormula a
forall a. PropositionalFormula a
PTrue
    lfalse :: PropositionalFormula a
lfalse = PropositionalFormula a
forall a. PropositionalFormula a
PFalse

    lnot :: PropositionalFormula a -> PropositionalFormula a
lnot PTrue = PropositionalFormula a
forall a. PropositionalFormula a
PFalse
    lnot PFalse = PropositionalFormula a
forall a. PropositionalFormula a
PTrue
    lnot p :: PropositionalFormula a
p = PropositionalFormula a -> PropositionalFormula a
forall a. PropositionalFormula a -> PropositionalFormula a
PNot PropositionalFormula a
p
    
    land :: [PropositionalFormula a] -> PropositionalFormula a
land [] = PropositionalFormula a
forall a. PropositionalFormula a
PTrue
    land l :: [PropositionalFormula a]
l = [PropositionalFormula a] -> PropositionalFormula a
forall a. [PropositionalFormula a] -> PropositionalFormula a
PAnd [PropositionalFormula a]
l

    lor :: [PropositionalFormula a] -> PropositionalFormula a
lor [] = PropositionalFormula a
forall a. PropositionalFormula a
PFalse
    lor l :: [PropositionalFormula a]
l = [PropositionalFormula a] -> PropositionalFormula a
forall a. [PropositionalFormula a] -> PropositionalFormula a
POr [PropositionalFormula a]
l
    
    leval :: (PropositionalFormula a -> PropositionalFormula a)
-> PropositionalFormula a -> PropositionalFormula a
leval config :: PropositionalFormula a -> PropositionalFormula a
config (PNot x :: PropositionalFormula a
x) = PropositionalFormula a -> PropositionalFormula a
forall l. Logic l => l -> l
lnot (PropositionalFormula a -> PropositionalFormula a)
-> PropositionalFormula a -> PropositionalFormula a
forall a b. (a -> b) -> a -> b
$ (PropositionalFormula a -> PropositionalFormula a)
-> PropositionalFormula a -> PropositionalFormula a
forall l. Logic l => (l -> l) -> l -> l
leval PropositionalFormula a -> PropositionalFormula a
config PropositionalFormula a
x -- This should evaluate as config should only map to lvalues and lnot directly inverts PTrue and PFalse.
    leval config :: PropositionalFormula a -> PropositionalFormula a
config (PAnd cs :: [PropositionalFormula a]
cs) = Bool -> PropositionalFormula a
forall a. Bool -> PropositionalFormula a
liftBool(Bool -> PropositionalFormula a)
-> (Bool -> Bool) -> Bool -> PropositionalFormula a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Bool -> Bool
not (Bool -> PropositionalFormula a) -> Bool -> PropositionalFormula a
forall a b. (a -> b) -> a -> b
$ (PropositionalFormula a -> Bool)
-> [PropositionalFormula a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any PropositionalFormula a -> Bool
forall a. PropositionalFormula a -> Bool
isPFalse ([PropositionalFormula a] -> Bool)
-> [PropositionalFormula a] -> Bool
forall a b. (a -> b) -> a -> b
$ (PropositionalFormula a -> PropositionalFormula a)
-> [PropositionalFormula a] -> [PropositionalFormula a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((PropositionalFormula a -> PropositionalFormula a)
-> PropositionalFormula a -> PropositionalFormula a
forall l. Logic l => (l -> l) -> l -> l
leval PropositionalFormula a -> PropositionalFormula a
config) [PropositionalFormula a]
cs
    leval config :: PropositionalFormula a -> PropositionalFormula a
config (POr cs :: [PropositionalFormula a]
cs) = Bool -> PropositionalFormula a
forall a. Bool -> PropositionalFormula a
liftBool (Bool -> PropositionalFormula a) -> Bool -> PropositionalFormula a
forall a b. (a -> b) -> a -> b
$ (PropositionalFormula a -> Bool)
-> [PropositionalFormula a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any PropositionalFormula a -> Bool
forall a. PropositionalFormula a -> Bool
isPTrue ([PropositionalFormula a] -> Bool)
-> [PropositionalFormula a] -> Bool
forall a b. (a -> b) -> a -> b
$ (PropositionalFormula a -> PropositionalFormula a)
-> [PropositionalFormula a] -> [PropositionalFormula a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((PropositionalFormula a -> PropositionalFormula a)
-> PropositionalFormula a -> PropositionalFormula a
forall l. Logic l => (l -> l) -> l -> l
leval PropositionalFormula a -> PropositionalFormula a
config) [PropositionalFormula a]
cs
    leval config :: PropositionalFormula a -> PropositionalFormula a
config p :: PropositionalFormula a
p = PropositionalFormula a -> PropositionalFormula a
config PropositionalFormula a
p

instance Functor PropositionalFormula where
    fmap :: (a -> b) -> PropositionalFormula a -> PropositionalFormula b
fmap _ PTrue = PropositionalFormula b
forall a. PropositionalFormula a
PTrue
    fmap _ PFalse = PropositionalFormula b
forall a. PropositionalFormula a
PFalse
    fmap f :: a -> b
f (PVariable a :: a
a) = b -> PropositionalFormula b
forall a. a -> PropositionalFormula a
PVariable (a -> b
f a
a)
    fmap f :: a -> b
f (PNot p :: PropositionalFormula a
p) = PropositionalFormula b -> PropositionalFormula b
forall a. PropositionalFormula a -> PropositionalFormula a
PNot ((a -> b) -> PropositionalFormula a -> PropositionalFormula b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f PropositionalFormula a
p)
    fmap f :: a -> b
f (PAnd c :: [PropositionalFormula a]
c) = [PropositionalFormula b] -> PropositionalFormula b
forall a. [PropositionalFormula a] -> PropositionalFormula a
PAnd ((PropositionalFormula a -> PropositionalFormula b)
-> [PropositionalFormula a] -> [PropositionalFormula b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> b) -> PropositionalFormula a -> PropositionalFormula b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f) [PropositionalFormula a]
c)
    fmap f :: a -> b
f (POr c :: [PropositionalFormula a]
c) = [PropositionalFormula b] -> PropositionalFormula b
forall a. [PropositionalFormula a] -> PropositionalFormula a
POr ((PropositionalFormula a -> PropositionalFormula b)
-> [PropositionalFormula a] -> [PropositionalFormula b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> b) -> PropositionalFormula a -> PropositionalFormula b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f) [PropositionalFormula a]
c)

-- | An assignment for propositional formulas, assigns variables to boolean values.
type Assignment a = a -> Bool -- Maybe this should better be implemented as a map as an Assignment always is a partial function.

-- | Evaluates a propositional formula with the given variable assignment.
eval :: Assignment a -> PropositionalFormula a -> Bool
eval :: Assignment a -> PropositionalFormula a -> Bool
eval _ PTrue = Bool
True
eval _ PFalse = Bool
False
eval config :: Assignment a
config v :: PropositionalFormula a
v@(PVariable x :: a
x) = Assignment a
config a
x
eval config :: Assignment a
config (PNot x :: PropositionalFormula a
x) = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Assignment a -> PropositionalFormula a -> Bool
forall a. Assignment a -> PropositionalFormula a -> Bool
eval Assignment a
config PropositionalFormula a
x
eval config :: Assignment a
config (PAnd cs :: [PropositionalFormula a]
cs) = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ (PropositionalFormula a -> Bool)
-> [PropositionalFormula a] -> [Bool]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Assignment a -> PropositionalFormula a -> Bool
forall a. Assignment a -> PropositionalFormula a -> Bool
eval Assignment a
config) [PropositionalFormula a]
cs
eval config :: Assignment a
config (POr cs :: [PropositionalFormula a]
cs) = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ (PropositionalFormula a -> Bool)
-> [PropositionalFormula a] -> [Bool]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Assignment a -> PropositionalFormula a -> Bool
forall a. Assignment a -> PropositionalFormula a -> Bool
eval Assignment a
config) [PropositionalFormula a]
cs

-- | Converts boolean values to their respective symbols in our definition of propositional logic.
liftBool :: Bool -> PropositionalFormula a
liftBool :: Bool -> PropositionalFormula a
liftBool True = PropositionalFormula a
forall a. PropositionalFormula a
PTrue
liftBool False = PropositionalFormula a
forall a. PropositionalFormula a
PFalse

-- | Returns /true/ iff the given propositional formula is the value 'PTrue'.
isPTrue :: PropositionalFormula a -> Bool
isPTrue :: PropositionalFormula a -> Bool
isPTrue PTrue = Bool
True
isPTrue _ = Bool
False

-- | Returns /true/ iff the given propositional formula is the value 'PFalse'.
isPFalse :: PropositionalFormula a -> Bool
isPFalse :: PropositionalFormula a -> Bool
isPFalse PFalse = Bool
True
isPFalse _ = Bool
False

-- | Returns /true/ iff the given propositional formula is a literal.
isLiteral :: PropositionalFormula a -> Bool
isLiteral :: PropositionalFormula a -> Bool
isLiteral PTrue = Bool
True
isLiteral PFalse = Bool
True
isLiteral (PVariable x :: a
x) = Bool
True
isLiteral (PNot f :: PropositionalFormula a
f) = PropositionalFormula a -> Bool
forall a. PropositionalFormula a -> Bool
isLiteral PropositionalFormula a
f
isLiteral _ = Bool
False

-- | Returns /true/ iff the given propositional formula is in conjunctive normal form.
isCNF :: PropositionalFormula a -> Bool
isCNF :: PropositionalFormula a -> Bool
isCNF (PAnd cs :: [PropositionalFormula a]
cs) = (PropositionalFormula a -> Bool)
-> [PropositionalFormula a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all PropositionalFormula a -> Bool
forall a. PropositionalFormula a -> Bool
isCNF [PropositionalFormula a]
cs
isCNF (POr cs :: [PropositionalFormula a]
cs) = (PropositionalFormula a -> Bool)
-> [PropositionalFormula a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all PropositionalFormula a -> Bool
forall a. PropositionalFormula a -> Bool
isLiteral [PropositionalFormula a]
cs
isCNF p :: PropositionalFormula a
p = PropositionalFormula a -> Bool
forall a. PropositionalFormula a -> Bool
isLiteral PropositionalFormula a
p

-- | Converts the given propositional formula to conjunctive normal form.
toCNF :: PropositionalFormula a -> PropositionalFormula a
toCNF :: PropositionalFormula a -> PropositionalFormula a
toCNF n :: PropositionalFormula a
n@(PNot a :: PropositionalFormula a
a) = case PropositionalFormula a
a of
    PTrue -> PropositionalFormula a
forall a. PropositionalFormula a
PFalse
    PFalse -> PropositionalFormula a
forall a. PropositionalFormula a
PTrue
    (PVariable x :: a
x) -> PropositionalFormula a
n
    (PNot x :: PropositionalFormula a
x) -> PropositionalFormula a -> PropositionalFormula a
forall a. PropositionalFormula a -> PropositionalFormula a
toCNF PropositionalFormula a
x
    (PAnd cs :: [PropositionalFormula a]
cs) -> PropositionalFormula a -> PropositionalFormula a
forall a. PropositionalFormula a -> PropositionalFormula a
toCNF (PropositionalFormula a -> PropositionalFormula a)
-> PropositionalFormula a -> PropositionalFormula a
forall a b. (a -> b) -> a -> b
$ [PropositionalFormula a] -> PropositionalFormula a
forall a. [PropositionalFormula a] -> PropositionalFormula a
POr ([PropositionalFormula a] -> PropositionalFormula a)
-> [PropositionalFormula a] -> PropositionalFormula a
forall a b. (a -> b) -> a -> b
$ (PropositionalFormula a -> PropositionalFormula a)
-> [PropositionalFormula a] -> [PropositionalFormula a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PropositionalFormula a -> PropositionalFormula a
forall l. Logic l => l -> l
lnot [PropositionalFormula a]
cs
    (POr cs :: [PropositionalFormula a]
cs) -> PropositionalFormula a -> PropositionalFormula a
forall a. PropositionalFormula a -> PropositionalFormula a
toCNF (PropositionalFormula a -> PropositionalFormula a)
-> PropositionalFormula a -> PropositionalFormula a
forall a b. (a -> b) -> a -> b
$ [PropositionalFormula a] -> PropositionalFormula a
forall a. [PropositionalFormula a] -> PropositionalFormula a
PAnd ([PropositionalFormula a] -> PropositionalFormula a)
-> [PropositionalFormula a] -> PropositionalFormula a
forall a b. (a -> b) -> a -> b
$ (PropositionalFormula a -> PropositionalFormula a)
-> [PropositionalFormula a] -> [PropositionalFormula a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PropositionalFormula a -> PropositionalFormula a
forall l. Logic l => l -> l
lnot [PropositionalFormula a]
cs
toCNF a :: PropositionalFormula a
a@(PAnd cs :: [PropositionalFormula a]
cs) = PropositionalFormula a -> PropositionalFormula a
forall a. PropositionalFormula a -> PropositionalFormula a
simplify (PropositionalFormula a -> PropositionalFormula a)
-> PropositionalFormula a -> PropositionalFormula a
forall a b. (a -> b) -> a -> b
$ [PropositionalFormula a] -> PropositionalFormula a
forall a. [PropositionalFormula a] -> PropositionalFormula a
PAnd ([PropositionalFormula a] -> PropositionalFormula a)
-> [PropositionalFormula a] -> PropositionalFormula a
forall a b. (a -> b) -> a -> b
$ (PropositionalFormula a -> PropositionalFormula a)
-> [PropositionalFormula a] -> [PropositionalFormula a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PropositionalFormula a -> PropositionalFormula a
forall a. PropositionalFormula a -> PropositionalFormula a
toCNF [PropositionalFormula a]
cs
toCNF o :: PropositionalFormula a
o@(POr cs :: [PropositionalFormula a]
cs) = PropositionalFormula a -> PropositionalFormula a
forall a. PropositionalFormula a -> PropositionalFormula a
simplify (PropositionalFormula a -> PropositionalFormula a)
-> PropositionalFormula a -> PropositionalFormula a
forall a b. (a -> b) -> a -> b
$ [PropositionalFormula a] -> PropositionalFormula a
forall a. [PropositionalFormula a] -> PropositionalFormula a
PAnd ([PropositionalFormula a] -> PropositionalFormula a)
-> [PropositionalFormula a] -> PropositionalFormula a
forall a b. (a -> b) -> a -> b
$ ([PropositionalFormula a]
 -> [PropositionalFormula a] -> [PropositionalFormula a])
-> [PropositionalFormula a]
-> [[PropositionalFormula a]]
-> [PropositionalFormula a]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr [PropositionalFormula a]
-> [PropositionalFormula a] -> [PropositionalFormula a]
forall a.
[PropositionalFormula a]
-> [PropositionalFormula a] -> [PropositionalFormula a]
cartesianOr [PropositionalFormula a
forall a. PropositionalFormula a
PFalse] ([[PropositionalFormula a]] -> [PropositionalFormula a])
-> [[PropositionalFormula a]] -> [PropositionalFormula a]
forall a b. (a -> b) -> a -> b
$ (PropositionalFormula a -> [PropositionalFormula a])
-> [PropositionalFormula a] -> [[PropositionalFormula a]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PropositionalFormula a -> [PropositionalFormula a]
forall a. PropositionalFormula a -> [PropositionalFormula a]
toCNFClauseList ([PropositionalFormula a] -> [[PropositionalFormula a]])
-> [PropositionalFormula a] -> [[PropositionalFormula a]]
forall a b. (a -> b) -> a -> b
$ (PropositionalFormula a -> PropositionalFormula a)
-> [PropositionalFormula a] -> [PropositionalFormula a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PropositionalFormula a -> PropositionalFormula a
forall a. PropositionalFormula a -> PropositionalFormula a
toCNF [PropositionalFormula a]
cs -- TODO
toCNF p :: PropositionalFormula a
p = PropositionalFormula a
p

-- | Converts the given propositional formula to conjunctive normal form if it is not already in that form.
lazyToCNF :: PropositionalFormula a -> PropositionalFormula a
lazyToCNF :: PropositionalFormula a -> PropositionalFormula a
lazyToCNF p :: PropositionalFormula a
p
    | PropositionalFormula a -> Bool
forall a. PropositionalFormula a -> Bool
isCNF PropositionalFormula a
p   = PropositionalFormula a
p
    | Bool
otherwise = PropositionalFormula a -> PropositionalFormula a
forall a. PropositionalFormula a -> PropositionalFormula a
toCNF PropositionalFormula a
p

{- |
Converts a 'PropositionalFormula' in conjunctive normal form to a list of its clauses.
The original formula can be reconstructed with PAnd (toClauseList x).
Assumes that the given formula is in CNF.
-}
toCNFClauseList :: PropositionalFormula a -> [PropositionalFormula a]
toCNFClauseList :: PropositionalFormula a -> [PropositionalFormula a]
toCNFClauseList (PAnd cs' :: [PropositionalFormula a]
cs') = [PropositionalFormula a]
cs'
toCNFClauseList p :: PropositionalFormula a
p = [PropositionalFormula a
p]

{- |
Converts a 'PropositionalFormula' in disjunctive normal form to a list of its clauses.
Assumes that the given formula is in DNF.
-}
toDNFClauseList :: PropositionalFormula a -> [PropositionalFormula a]
toDNFClauseList :: PropositionalFormula a -> [PropositionalFormula a]
toDNFClauseList (POr cs' :: [PropositionalFormula a]
cs') = [PropositionalFormula a]
cs'
toDNFClauseList p :: PropositionalFormula a
p = [PropositionalFormula a
p]

-- | Converts a 'PropositionalFormula' to negation normal form.
toNNF :: PropositionalFormula a -> PropositionalFormula a
toNNF :: PropositionalFormula a -> PropositionalFormula a
toNNF (PNot (POr cs :: [PropositionalFormula a]
cs)) = [PropositionalFormula a] -> PropositionalFormula a
forall a. [PropositionalFormula a] -> PropositionalFormula a
PAnd ([PropositionalFormula a] -> PropositionalFormula a)
-> [PropositionalFormula a] -> PropositionalFormula a
forall a b. (a -> b) -> a -> b
$ PropositionalFormula a -> PropositionalFormula a
forall a. PropositionalFormula a -> PropositionalFormula a
toNNF(PropositionalFormula a -> PropositionalFormula a)
-> (PropositionalFormula a -> PropositionalFormula a)
-> PropositionalFormula a
-> PropositionalFormula a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.PropositionalFormula a -> PropositionalFormula a
forall a. PropositionalFormula a -> PropositionalFormula a
PNot (PropositionalFormula a -> PropositionalFormula a)
-> [PropositionalFormula a] -> [PropositionalFormula a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PropositionalFormula a]
cs
toNNF (PNot (PAnd cs :: [PropositionalFormula a]
cs)) = [PropositionalFormula a] -> PropositionalFormula a
forall a. [PropositionalFormula a] -> PropositionalFormula a
POr ([PropositionalFormula a] -> PropositionalFormula a)
-> [PropositionalFormula a] -> PropositionalFormula a
forall a b. (a -> b) -> a -> b
$ PropositionalFormula a -> PropositionalFormula a
forall a. PropositionalFormula a -> PropositionalFormula a
toNNF(PropositionalFormula a -> PropositionalFormula a)
-> (PropositionalFormula a -> PropositionalFormula a)
-> PropositionalFormula a
-> PropositionalFormula a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.PropositionalFormula a -> PropositionalFormula a
forall a. PropositionalFormula a -> PropositionalFormula a
PNot (PropositionalFormula a -> PropositionalFormula a)
-> [PropositionalFormula a] -> [PropositionalFormula a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PropositionalFormula a]
cs
toNNF (PNot (PNot x :: PropositionalFormula a
x)) = PropositionalFormula a -> PropositionalFormula a
forall a. PropositionalFormula a -> PropositionalFormula a
toNNF PropositionalFormula a
x
toNNF (POr cs :: [PropositionalFormula a]
cs) = [PropositionalFormula a] -> PropositionalFormula a
forall a. [PropositionalFormula a] -> PropositionalFormula a
POr ([PropositionalFormula a] -> PropositionalFormula a)
-> [PropositionalFormula a] -> PropositionalFormula a
forall a b. (a -> b) -> a -> b
$ PropositionalFormula a -> PropositionalFormula a
forall a. PropositionalFormula a -> PropositionalFormula a
toNNF (PropositionalFormula a -> PropositionalFormula a)
-> [PropositionalFormula a] -> [PropositionalFormula a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PropositionalFormula a]
cs
toNNF (PAnd cs :: [PropositionalFormula a]
cs) = [PropositionalFormula a] -> PropositionalFormula a
forall a. [PropositionalFormula a] -> PropositionalFormula a
PAnd ([PropositionalFormula a] -> PropositionalFormula a)
-> [PropositionalFormula a] -> PropositionalFormula a
forall a b. (a -> b) -> a -> b
$ PropositionalFormula a -> PropositionalFormula a
forall a. PropositionalFormula a -> PropositionalFormula a
toNNF (PropositionalFormula a -> PropositionalFormula a)
-> [PropositionalFormula a] -> [PropositionalFormula a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PropositionalFormula a]
cs
toNNF p :: PropositionalFormula a
p = PropositionalFormula a
p

{- |
Returns a list of disjunctions such that all possible combinations of the formulas in the input lists are considered.
Like the cartesian product but instead of pairs (x, y) we produce POr [x, y].
-}
cartesianOr :: [PropositionalFormula a] -> [PropositionalFormula a] -> [PropositionalFormula a]
cartesianOr :: [PropositionalFormula a]
-> [PropositionalFormula a] -> [PropositionalFormula a]
cartesianOr l1 :: [PropositionalFormula a]
l1 l2 :: [PropositionalFormula a]
l2 = [[PropositionalFormula a] -> PropositionalFormula a
forall a. [PropositionalFormula a] -> PropositionalFormula a
POr [PropositionalFormula a
x, PropositionalFormula a
y] | PropositionalFormula a
x <- [PropositionalFormula a]
l1, PropositionalFormula a
y <- [PropositionalFormula a]
l2]

-- | Simplifies the given 'PropositionalFormula' with some basic rules (e.g., @PNot PTrue -> PFalse@).
simplify :: PropositionalFormula a -> PropositionalFormula a
simplify :: PropositionalFormula a -> PropositionalFormula a
simplify (PNot a :: PropositionalFormula a
a) = case PropositionalFormula a -> PropositionalFormula a
forall a. PropositionalFormula a -> PropositionalFormula a
simplify PropositionalFormula a
a of
    PTrue -> PropositionalFormula a
forall a. PropositionalFormula a
PFalse
    PFalse -> PropositionalFormula a
forall a. PropositionalFormula a
PTrue
    (PNot x :: PropositionalFormula a
x) -> PropositionalFormula a
x
    p :: PropositionalFormula a
p -> PropositionalFormula a -> PropositionalFormula a
forall a. PropositionalFormula a -> PropositionalFormula a
PNot PropositionalFormula a
p
simplify (PAnd cs :: [PropositionalFormula a]
cs) = case
    (PropositionalFormula a -> Bool)
-> [PropositionalFormula a] -> [PropositionalFormula a]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> (PropositionalFormula a -> Bool)
-> PropositionalFormula a
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PropositionalFormula a -> Bool
forall a. PropositionalFormula a -> Bool
isPTrue) -- Filter all Trues
    ([PropositionalFormula a] -> [PropositionalFormula a])
-> [PropositionalFormula a] -> [PropositionalFormula a]
forall a b. (a -> b) -> a -> b
$ [[PropositionalFormula a]] -> [PropositionalFormula a]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[PropositionalFormula a]] -> [PropositionalFormula a])
-> [[PropositionalFormula a]] -> [PropositionalFormula a]
forall a b. (a -> b) -> a -> b
$ (PropositionalFormula a -> [PropositionalFormula a])
-> [PropositionalFormula a] -> [[PropositionalFormula a]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (PropositionalFormula a -> [PropositionalFormula a]
forall a. PropositionalFormula a -> [PropositionalFormula a]
toCNFClauseList (PropositionalFormula a -> [PropositionalFormula a])
-> (PropositionalFormula a -> PropositionalFormula a)
-> PropositionalFormula a
-> [PropositionalFormula a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PropositionalFormula a -> PropositionalFormula a
forall a. PropositionalFormula a -> PropositionalFormula a
simplify) [PropositionalFormula a]
cs -- simplify all children and flatten the formula
    of
        [] -> PropositionalFormula a
forall a. PropositionalFormula a
PTrue
        [p :: PropositionalFormula a
p] -> PropositionalFormula a
p
        clauses :: [PropositionalFormula a]
clauses -> if (PropositionalFormula a -> Bool)
-> [PropositionalFormula a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any PropositionalFormula a -> Bool
forall a. PropositionalFormula a -> Bool
isPFalse [PropositionalFormula a]
clauses -- If any value in a disjunction is false, the disjunction becomes false.
                   then PropositionalFormula a
forall a. PropositionalFormula a
PFalse
                   else [PropositionalFormula a] -> PropositionalFormula a
forall a. [PropositionalFormula a] -> PropositionalFormula a
PAnd [PropositionalFormula a]
clauses
simplify (POr cs :: [PropositionalFormula a]
cs) = case
    (PropositionalFormula a -> Bool)
-> [PropositionalFormula a] -> [PropositionalFormula a]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> (PropositionalFormula a -> Bool)
-> PropositionalFormula a
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PropositionalFormula a -> Bool
forall a. PropositionalFormula a -> Bool
isPFalse) -- Filter all Falses
    ([PropositionalFormula a] -> [PropositionalFormula a])
-> [PropositionalFormula a] -> [PropositionalFormula a]
forall a b. (a -> b) -> a -> b
$ [[PropositionalFormula a]] -> [PropositionalFormula a]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[PropositionalFormula a]] -> [PropositionalFormula a])
-> [[PropositionalFormula a]] -> [PropositionalFormula a]
forall a b. (a -> b) -> a -> b
$ (PropositionalFormula a -> [PropositionalFormula a])
-> [PropositionalFormula a] -> [[PropositionalFormula a]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (PropositionalFormula a -> [PropositionalFormula a]
forall a. PropositionalFormula a -> [PropositionalFormula a]
toDNFClauseList (PropositionalFormula a -> [PropositionalFormula a])
-> (PropositionalFormula a -> PropositionalFormula a)
-> PropositionalFormula a
-> [PropositionalFormula a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PropositionalFormula a -> PropositionalFormula a
forall a. PropositionalFormula a -> PropositionalFormula a
simplify) [PropositionalFormula a]
cs -- simplify all children and flatten the formula
    of
        [] -> PropositionalFormula a
forall a. PropositionalFormula a
PFalse
        [p :: PropositionalFormula a
p] -> PropositionalFormula a
p
        clauses :: [PropositionalFormula a]
clauses -> if (PropositionalFormula a -> Bool)
-> [PropositionalFormula a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any PropositionalFormula a -> Bool
forall a. PropositionalFormula a -> Bool
isPTrue [PropositionalFormula a]
clauses -- If any value in a disjunction is true, the disjunction becomes true.
                   then PropositionalFormula a
forall a. PropositionalFormula a
PTrue
                   else [PropositionalFormula a] -> PropositionalFormula a
forall a. [PropositionalFormula a] -> PropositionalFormula a
POr [PropositionalFormula a]
clauses
simplify p :: PropositionalFormula a
p = PropositionalFormula a
p

{- |
Transforms a 'PropositionalFormula' in CNF to a list of its clauses.
Assumes that the given formula is in CNF.

* The first argument is a functions resolving negation, i.e. it should take an 'a' and give its negated version.
* The second argument is a function creating the value of type @a@ that should be associated with /false/ ('PFalse').
For example, @0@ could represent /false/ in propositional formulas over numerals.
(Note, if no such value exists, the /false/ function is free to produce an error.)
* The third argument is the function in CNF that should be clausified.

If still confused, try the following call and look at the result:
@
    show $ clausifyCNF (\x -> "not "++x) "false" (toCNF p)
@
where @p@ is a propositional formula over strings.
-}
clausifyCNF :: (Show a) => (a -> a) -> (() -> a) -> PropositionalFormula a -> [[a]]
clausifyCNF :: (a -> a) -> (() -> a) -> PropositionalFormula a -> [[a]]
clausifyCNF _ _ PTrue  = [[]]
clausifyCNF _ false :: () -> a
false PFalse = [[() -> a
false ()]] --error "PFalse cannot be clausifed."
clausifyCNF _ _ (PVariable v :: a
v) = [[a
v]]
clausifyCNF negator :: a -> a
negator _ n :: PropositionalFormula a
n@(PNot p :: PropositionalFormula a
p) = case PropositionalFormula a
p of
    PVariable v :: a
v -> [[a -> a
negator a
v]]
    _ -> [Char] -> [[a]]
forall a. HasCallStack => [Char] -> a
error ([Char] -> [[a]]) -> [Char] -> [[a]]
forall a b. (a -> b) -> a -> b
$ "Given formula "[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++PropositionalFormula a -> [Char]
forall a. Show a => a -> [Char]
show PropositionalFormula a
n[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++" not in CNF!"
clausifyCNF negator :: a -> a
negator false :: () -> a
false and :: PropositionalFormula a
and@(PAnd clauses :: [PropositionalFormula a]
clauses) = if PropositionalFormula a -> Bool
forall a. PropositionalFormula a -> Bool
isCNF PropositionalFormula a
and
    then [[[a]]] -> [[a]]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[[a]]] -> [[a]]) -> [[[a]]] -> [[a]]
forall a b. (a -> b) -> a -> b
$ (PropositionalFormula a -> [[a]])
-> [PropositionalFormula a] -> [[[a]]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> a) -> (() -> a) -> PropositionalFormula a -> [[a]]
forall a.
Show a =>
(a -> a) -> (() -> a) -> PropositionalFormula a -> [[a]]
clausifyCNF a -> a
negator () -> a
false) [PropositionalFormula a]
clauses
    else [Char] -> [[a]]
forall a. HasCallStack => [Char] -> a
error ([Char] -> [[a]]) -> [Char] -> [[a]]
forall a b. (a -> b) -> a -> b
$ "Given formula "[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++PropositionalFormula a -> [Char]
forall a. Show a => a -> [Char]
show PropositionalFormula a
and[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++" not in CNF!"
clausifyCNF negator :: a -> a
negator false :: () -> a
false or :: PropositionalFormula a
or@(POr literals :: [PropositionalFormula a]
literals) = if PropositionalFormula a -> Bool
forall a. PropositionalFormula a -> Bool
isCNF PropositionalFormula a
or
    then [[[a]] -> [a]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[a]] -> [a]) -> [[a]] -> [a]
forall a b. (a -> b) -> a -> b
$ [[[a]]] -> [[a]]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[[a]]] -> [[a]]) -> [[[a]]] -> [[a]]
forall a b. (a -> b) -> a -> b
$ (PropositionalFormula a -> [[a]])
-> [PropositionalFormula a] -> [[[a]]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> a) -> (() -> a) -> PropositionalFormula a -> [[a]]
forall a.
Show a =>
(a -> a) -> (() -> a) -> PropositionalFormula a -> [[a]]
clausifyCNF a -> a
negator () -> a
false) [PropositionalFormula a]
literals]
    else [Char] -> [[a]]
forall a. HasCallStack => [Char] -> a
error ([Char] -> [[a]]) -> [Char] -> [[a]]
forall a b. (a -> b) -> a -> b
$ "Given formula "[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++PropositionalFormula a -> [Char]
forall a. Show a => a -> [Char]
show PropositionalFormula a
or[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++" not in CNF!"
                            
-- -- | Default ASCII expressions for printing propositional operators.
-- instance Show a => Show (PropositionalFormula a) where
--     show PTrue = "T"
--     show PFalse = "F"
--     show (PVariable v) = show v
--     show (PNot p) = "¬"++show p
--     show (PAnd cs) = parenIf (length cs > 1) (intercalate " ^ " $ map show cs)
--     show (POr cs) = parenIf (length cs > 1) (intercalate " v " $ map show cs)

-- | UTF-8 characters for printing propositional operators.
instance Show a => Show (PropositionalFormula a) where
    show :: PropositionalFormula a -> [Char]
show PTrue = "⊤"
    show PFalse = "⊥"
    show (PVariable v :: a
v) = a -> [Char]
forall a. Show a => a -> [Char]
show a
v
    show (PNot p :: PropositionalFormula a
p) = "¬"[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++PropositionalFormula a -> [Char]
forall a. Show a => a -> [Char]
show PropositionalFormula a
p
    show (PAnd cs :: [PropositionalFormula a]
cs) = "("[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++([Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate " ∧ " ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ (PropositionalFormula a -> [Char])
-> [PropositionalFormula a] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map PropositionalFormula a -> [Char]
forall a. Show a => a -> [Char]
show [PropositionalFormula a]
cs)[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++")"
    show (POr cs :: [PropositionalFormula a]
cs) = "("[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++([Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate " ∨ " ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ (PropositionalFormula a -> [Char])
-> [PropositionalFormula a] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map PropositionalFormula a -> [Char]
forall a. Show a => a -> [Char]
show [PropositionalFormula a]
cs)[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++")"

-- -- | This visualisation is for debugging as it shows the exact expression tree.
-- instance Show a => Show (PropositionalFormula a) where
--     show PTrue = "(PTrue)"
--     show PFalse = "(PFalse)"
--     show (PVariable v) = "(PVariable "++show v++")"
--     show (PNot p) = "(PNot "++show p++")"
--     show (PAnd cs) = "(PAnd ["++(intercalate ", " $ map show cs)++"])"
--     show (POr cs) = "(POr ["++(intercalate ", " $ map show cs)++"])"