```{- |
Module      :  ./Propositional/Fold.hs
Description :  folding function for propositional formulas
Copyright   :  (c) Christian Maeder, DFKI GmbH 2009

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable

folding and simplification of propositional formulas

-}

module Propositional.Fold where

import Common.Id
import Propositional.AS_BASIC_Propositional

import qualified Data.Set as Set

data FoldRecord a = FoldRecord
{ FoldRecord a -> a -> Range -> a
foldNegation :: a -> Range -> a
, FoldRecord a -> [a] -> Range -> a
foldConjunction :: [a] -> Range -> a
, FoldRecord a -> [a] -> Range -> a
foldDisjunction :: [a] -> Range -> a
, FoldRecord a -> a -> a -> Range -> a
foldImplication :: a -> a -> Range -> a
, FoldRecord a -> a -> a -> Range -> a
foldEquivalence :: a -> a -> Range -> a
, FoldRecord a -> Range -> a
foldTrue_atom :: Range -> a
, FoldRecord a -> Range -> a
foldFalse_atom :: Range -> a
, FoldRecord a -> Token -> a
foldPredication :: Token -> a }

foldFormula :: FoldRecord a -> FORMULA -> a
foldFormula :: FoldRecord a -> FORMULA -> a
foldFormula r :: FoldRecord a
r frm :: FORMULA
frm = case FORMULA
frm of
Negation f :: FORMULA
f n :: Range
n -> FoldRecord a -> a -> Range -> a
forall a. FoldRecord a -> a -> Range -> a
foldNegation FoldRecord a
r (FoldRecord a -> FORMULA -> a
forall a. FoldRecord a -> FORMULA -> a
foldFormula FoldRecord a
r FORMULA
f) Range
n
Conjunction xs :: [FORMULA]
xs n :: Range
n -> FoldRecord a -> [a] -> Range -> a
forall a. FoldRecord a -> [a] -> Range -> a
foldConjunction FoldRecord a
r ((FORMULA -> a) -> [FORMULA] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (FoldRecord a -> FORMULA -> a
forall a. FoldRecord a -> FORMULA -> a
foldFormula FoldRecord a
r) [FORMULA]
xs) Range
n
Disjunction xs :: [FORMULA]
xs n :: Range
n -> FoldRecord a -> [a] -> Range -> a
forall a. FoldRecord a -> [a] -> Range -> a
foldDisjunction FoldRecord a
r ((FORMULA -> a) -> [FORMULA] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (FoldRecord a -> FORMULA -> a
forall a. FoldRecord a -> FORMULA -> a
foldFormula FoldRecord a
r) [FORMULA]
xs) Range
n
Implication x :: FORMULA
x y :: FORMULA
y n :: Range
n -> FoldRecord a -> a -> a -> Range -> a
forall a. FoldRecord a -> a -> a -> Range -> a
foldImplication FoldRecord a
r (FoldRecord a -> FORMULA -> a
forall a. FoldRecord a -> FORMULA -> a
foldFormula FoldRecord a
r FORMULA
x) (FoldRecord a -> FORMULA -> a
forall a. FoldRecord a -> FORMULA -> a
foldFormula FoldRecord a
r FORMULA
y) Range
n
Equivalence x :: FORMULA
x y :: FORMULA
y n :: Range
n -> FoldRecord a -> a -> a -> Range -> a
forall a. FoldRecord a -> a -> a -> Range -> a
foldEquivalence FoldRecord a
r (FoldRecord a -> FORMULA -> a
forall a. FoldRecord a -> FORMULA -> a
foldFormula FoldRecord a
r FORMULA
x) (FoldRecord a -> FORMULA -> a
forall a. FoldRecord a -> FORMULA -> a
foldFormula FoldRecord a
r FORMULA
y) Range
n
True_atom n :: Range
n -> FoldRecord a -> Range -> a
forall a. FoldRecord a -> Range -> a
foldTrue_atom FoldRecord a
r Range
n
False_atom n :: Range
n -> FoldRecord a -> Range -> a
forall a. FoldRecord a -> Range -> a
foldFalse_atom FoldRecord a
r Range
n
Predication x :: Token
x -> FoldRecord a -> Token -> a
forall a. FoldRecord a -> Token -> a
foldPredication FoldRecord a
r Token
x

mapRecord :: FoldRecord FORMULA
mapRecord :: FoldRecord FORMULA
mapRecord = FoldRecord :: forall a.
(a -> Range -> a)
-> ([a] -> Range -> a)
-> ([a] -> Range -> a)
-> (a -> a -> Range -> a)
-> (a -> a -> Range -> a)
-> (Range -> a)
-> (Range -> a)
-> (Token -> a)
-> FoldRecord a
FoldRecord
{ foldNegation :: FORMULA -> Range -> FORMULA
foldNegation = FORMULA -> Range -> FORMULA
Negation
, foldConjunction :: [FORMULA] -> Range -> FORMULA
foldConjunction = [FORMULA] -> Range -> FORMULA
Conjunction
, foldDisjunction :: [FORMULA] -> Range -> FORMULA
foldDisjunction = [FORMULA] -> Range -> FORMULA
Disjunction
, foldImplication :: FORMULA -> FORMULA -> Range -> FORMULA
foldImplication = FORMULA -> FORMULA -> Range -> FORMULA
Implication
, foldEquivalence :: FORMULA -> FORMULA -> Range -> FORMULA
foldEquivalence = FORMULA -> FORMULA -> Range -> FORMULA
Equivalence
, foldTrue_atom :: Range -> FORMULA
foldTrue_atom = Range -> FORMULA
True_atom
, foldFalse_atom :: Range -> FORMULA
foldFalse_atom = Range -> FORMULA
False_atom
, foldPredication :: Token -> FORMULA
foldPredication = Token -> FORMULA
Predication }

isNeg :: FORMULA -> Bool
isNeg :: FORMULA -> Bool
isNeg f :: FORMULA
f = case FORMULA
f of
Negation _ _ -> Bool
True
_ -> Bool
False

getLits :: Set.Set FORMULA -> Set.Set FORMULA
getLits :: Set FORMULA -> Set FORMULA
getLits = (FORMULA -> Set FORMULA -> Set FORMULA)
-> Set FORMULA -> Set FORMULA -> Set FORMULA
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ f :: FORMULA
f -> case FORMULA
f of
Negation x :: FORMULA
x _ -> FORMULA -> Set FORMULA -> Set FORMULA
forall a. Ord a => a -> Set a -> Set a
Set.insert FORMULA
x
_ -> FORMULA -> Set FORMULA -> Set FORMULA
forall a. Ord a => a -> Set a -> Set a
Set.insert FORMULA
f) Set FORMULA
forall a. Set a
Set.empty

bothLits :: Set.Set FORMULA -> Bool
bothLits :: Set FORMULA -> Bool
bothLits fs :: Set FORMULA
fs = let
(ns :: Set FORMULA
ns, ps :: Set FORMULA
ps) = (FORMULA -> Bool) -> Set FORMULA -> (Set FORMULA, Set FORMULA)
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.partition FORMULA -> Bool
isNeg Set FORMULA
fs
in Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
\$ Set FORMULA -> Bool
forall a. Set a -> Bool
Set.null (Set FORMULA -> Bool) -> Set FORMULA -> Bool
forall a b. (a -> b) -> a -> b
\$ Set FORMULA -> Set FORMULA -> Set FORMULA
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection (Set FORMULA -> Set FORMULA
getLits Set FORMULA
ns) (Set FORMULA -> Set FORMULA
getLits Set FORMULA
ps)

getConj :: FORMULA -> [FORMULA]
getConj :: FORMULA -> [FORMULA]
getConj f :: FORMULA
f = case FORMULA
f of
Conjunction xs :: [FORMULA]
xs _ -> [FORMULA]
xs
True_atom _ -> []
_ -> [FORMULA
f]

getDisj :: FORMULA -> [FORMULA]
getDisj :: FORMULA -> [FORMULA]
getDisj f :: FORMULA
f = case FORMULA
f of
Disjunction xs :: [FORMULA]
xs _ -> [FORMULA]
xs
False_atom _ -> []
_ -> [FORMULA
f]

flatConj :: [FORMULA] -> Set.Set FORMULA
flatConj :: [FORMULA] -> Set FORMULA
flatConj = [FORMULA] -> Set FORMULA
forall a. Ord a => [a] -> Set a
Set.fromList
([FORMULA] -> Set FORMULA)
-> ([FORMULA] -> [FORMULA]) -> [FORMULA] -> Set FORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FORMULA -> [FORMULA]) -> [FORMULA] -> [FORMULA]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ f :: FORMULA
f -> case FORMULA
f of
True_atom _ -> []
Conjunction fs :: [FORMULA]
fs _ -> [FORMULA]
fs
_ -> [FORMULA
f])

mkConj :: [FORMULA] -> Range -> FORMULA
mkConj :: [FORMULA] -> Range -> FORMULA
mkConj fs :: [FORMULA]
fs n :: Range
n = let s :: Set FORMULA
s = [FORMULA] -> Set FORMULA
flatConj [FORMULA]
fs in
if FORMULA -> Set FORMULA -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (Range -> FORMULA
False_atom Range
nullRange) Set FORMULA
s Bool -> Bool -> Bool
|| Set FORMULA -> Bool
bothLits Set FORMULA
s then Range -> FORMULA
False_atom Range
n else
case Set FORMULA -> [FORMULA]
forall a. Set a -> [a]
Set.toList Set FORMULA
s of
[] -> Range -> FORMULA
True_atom Range
n
[x :: FORMULA
x] -> FORMULA
x
ls :: [FORMULA]
ls -> [FORMULA] -> Range -> FORMULA
Conjunction ((Set FORMULA -> FORMULA) -> [Set FORMULA] -> [FORMULA]
forall a b. (a -> b) -> [a] -> [b]
map (([FORMULA] -> Range -> FORMULA) -> Range -> [FORMULA] -> FORMULA
forall a b c. (a -> b -> c) -> b -> a -> c
flip [FORMULA] -> Range -> FORMULA
mkDisj Range
n ([FORMULA] -> FORMULA)
-> (Set FORMULA -> [FORMULA]) -> Set FORMULA -> FORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set FORMULA -> [FORMULA]
forall a. Set a -> [a]
Set.toList)
([Set FORMULA] -> [FORMULA]) -> [Set FORMULA] -> [FORMULA]
forall a b. (a -> b) -> a -> b
\$ (FORMULA -> [Set FORMULA] -> [Set FORMULA])
-> [Set FORMULA] -> [FORMULA] -> [Set FORMULA]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((\ l :: Set FORMULA
l ll :: [Set FORMULA]
ll ->
if (Set FORMULA -> Bool) -> [Set FORMULA] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Set FORMULA -> Set FORMULA -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Set FORMULA
l) [Set FORMULA]
ll then [Set FORMULA]
ll else
Set FORMULA
l Set FORMULA -> [Set FORMULA] -> [Set FORMULA]
forall a. a -> [a] -> [a]
: (Set FORMULA -> Bool) -> [Set FORMULA] -> [Set FORMULA]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Set FORMULA -> Bool) -> Set FORMULA -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set FORMULA -> Set FORMULA -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf Set FORMULA
l) [Set FORMULA]
ll)
(Set FORMULA -> [Set FORMULA] -> [Set FORMULA])
-> (FORMULA -> Set FORMULA)
-> FORMULA
-> [Set FORMULA]
-> [Set FORMULA]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [FORMULA] -> Set FORMULA
forall a. Ord a => [a] -> Set a
Set.fromList ([FORMULA] -> Set FORMULA)
-> (FORMULA -> [FORMULA]) -> FORMULA -> Set FORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA -> [FORMULA]
getDisj) [] [FORMULA]
ls) Range
n

flatDisj :: [FORMULA] -> Set.Set FORMULA
flatDisj :: [FORMULA] -> Set FORMULA
flatDisj = [FORMULA] -> Set FORMULA
forall a. Ord a => [a] -> Set a
Set.fromList
([FORMULA] -> Set FORMULA)
-> ([FORMULA] -> [FORMULA]) -> [FORMULA] -> Set FORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FORMULA -> [FORMULA]) -> [FORMULA] -> [FORMULA]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ f :: FORMULA
f -> case FORMULA
f of
False_atom _ -> []
Disjunction fs :: [FORMULA]
fs _ -> [FORMULA]
fs
_ -> [FORMULA
f])

mkDisj :: [FORMULA] -> Range -> FORMULA
mkDisj :: [FORMULA] -> Range -> FORMULA
mkDisj fs :: [FORMULA]
fs n :: Range
n = let s :: Set FORMULA
s = [FORMULA] -> Set FORMULA
flatDisj [FORMULA]
fs in
if FORMULA -> Set FORMULA -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (Range -> FORMULA
True_atom Range
nullRange) Set FORMULA
s Bool -> Bool -> Bool
|| Set FORMULA -> Bool
bothLits Set FORMULA
s then Range -> FORMULA
True_atom Range
n else
case Set FORMULA -> [FORMULA]
forall a. Set a -> [a]
Set.toList Set FORMULA
s of
[] -> Range -> FORMULA
False_atom Range
n
[x :: FORMULA
x] -> FORMULA
x
ls :: [FORMULA]
ls -> [FORMULA] -> Range -> FORMULA
Disjunction ((Set FORMULA -> FORMULA) -> [Set FORMULA] -> [FORMULA]
forall a b. (a -> b) -> [a] -> [b]
map (([FORMULA] -> Range -> FORMULA) -> Range -> [FORMULA] -> FORMULA
forall a b c. (a -> b -> c) -> b -> a -> c
flip [FORMULA] -> Range -> FORMULA
mkConj Range
n ([FORMULA] -> FORMULA)
-> (Set FORMULA -> [FORMULA]) -> Set FORMULA -> FORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set FORMULA -> [FORMULA]
forall a. Set a -> [a]
Set.toList)
([Set FORMULA] -> [FORMULA]) -> [Set FORMULA] -> [FORMULA]
forall a b. (a -> b) -> a -> b
\$ (FORMULA -> [Set FORMULA] -> [Set FORMULA])
-> [Set FORMULA] -> [FORMULA] -> [Set FORMULA]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((\ l :: Set FORMULA
l ll :: [Set FORMULA]
ll ->
if (Set FORMULA -> Bool) -> [Set FORMULA] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Set FORMULA -> Set FORMULA -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Set FORMULA
l) [Set FORMULA]
ll then [Set FORMULA]
ll else
Set FORMULA
l Set FORMULA -> [Set FORMULA] -> [Set FORMULA]
forall a. a -> [a] -> [a]
: (Set FORMULA -> Bool) -> [Set FORMULA] -> [Set FORMULA]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Set FORMULA -> Bool) -> Set FORMULA -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set FORMULA -> Set FORMULA -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf Set FORMULA
l) [Set FORMULA]
ll)
(Set FORMULA -> [Set FORMULA] -> [Set FORMULA])
-> (FORMULA -> Set FORMULA)
-> FORMULA
-> [Set FORMULA]
-> [Set FORMULA]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [FORMULA] -> Set FORMULA
forall a. Ord a => [a] -> Set a
Set.fromList ([FORMULA] -> Set FORMULA)
-> (FORMULA -> [FORMULA]) -> FORMULA -> Set FORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA -> [FORMULA]
getConj) [] [FORMULA]
ls) Range
n

simplify :: FORMULA -> FORMULA
simplify :: FORMULA -> FORMULA
simplify = FoldRecord FORMULA -> FORMULA -> FORMULA
forall a. FoldRecord a -> FORMULA -> a
foldFormula FoldRecord FORMULA
mapRecord
{ foldNegation :: FORMULA -> Range -> FORMULA
foldNegation = \ f :: FORMULA
f n :: Range
n -> case FORMULA
f of
True_atom p :: Range
p -> Range -> FORMULA
False_atom Range
p
False_atom p :: Range
p -> Range -> FORMULA
True_atom Range
p
Negation g :: FORMULA
g _ -> FORMULA
g
s :: FORMULA
s -> FORMULA -> Range -> FORMULA
Negation FORMULA
s Range
n
, foldConjunction :: [FORMULA] -> Range -> FORMULA
foldConjunction = [FORMULA] -> Range -> FORMULA
mkConj
, foldDisjunction :: [FORMULA] -> Range -> FORMULA
foldDisjunction = [FORMULA] -> Range -> FORMULA
mkDisj
, foldImplication :: FORMULA -> FORMULA -> Range -> FORMULA
foldImplication = \ x :: FORMULA
x y :: FORMULA
y n :: Range
n -> case FORMULA
x of
False_atom p :: Range
p -> Range -> FORMULA
True_atom Range
p
_ -> if FORMULA
x FORMULA -> FORMULA -> Bool
forall a. Eq a => a -> a -> Bool
== FORMULA
y then Range -> FORMULA
True_atom Range
n else case FORMULA
x of
True_atom _ -> FORMULA
y
False_atom _ -> Range -> FORMULA
True_atom Range
n
Negation z :: FORMULA
z _ | FORMULA
z FORMULA -> FORMULA -> Bool
forall a. Eq a => a -> a -> Bool
== FORMULA
y -> FORMULA
x
_ -> case FORMULA
y of
Negation z :: FORMULA
z _ | FORMULA
z FORMULA -> FORMULA -> Bool
forall a. Eq a => a -> a -> Bool
== FORMULA
x -> FORMULA
x
_ -> FORMULA -> FORMULA -> Range -> FORMULA
Implication FORMULA
x FORMULA
y Range
n
, foldEquivalence :: FORMULA -> FORMULA -> Range -> FORMULA
foldEquivalence = \ x :: FORMULA
x y :: FORMULA
y n :: Range
n -> case FORMULA -> FORMULA -> Ordering
forall a. Ord a => a -> a -> Ordering
compare FORMULA
x FORMULA
y of
LT -> case FORMULA
y of
Negation z :: FORMULA
z _ | FORMULA
x FORMULA -> FORMULA -> Bool
forall a. Eq a => a -> a -> Bool
== FORMULA
z -> Range -> FORMULA
False_atom Range
n
_ -> FORMULA -> FORMULA -> Range -> FORMULA
Equivalence FORMULA
x FORMULA
y Range
n
EQ -> Range -> FORMULA
True_atom Range
n
GT -> case FORMULA
x of
Negation z :: FORMULA
z _ | FORMULA
z FORMULA -> FORMULA -> Bool
forall a. Eq a => a -> a -> Bool
== FORMULA
y -> Range -> FORMULA
False_atom Range
n
_ -> FORMULA -> FORMULA -> Range -> FORMULA
Equivalence FORMULA
y FORMULA
x Range
n }

elimEquiv :: FORMULA -> FORMULA
elimEquiv :: FORMULA -> FORMULA
elimEquiv = FoldRecord FORMULA -> FORMULA -> FORMULA
forall a. FoldRecord a -> FORMULA -> a
foldFormula FoldRecord FORMULA
mapRecord
{ foldEquivalence :: FORMULA -> FORMULA -> Range -> FORMULA
foldEquivalence = \ x :: FORMULA
x y :: FORMULA
y n :: Range
n ->
[FORMULA] -> Range -> FORMULA
Conjunction [FORMULA -> FORMULA -> Range -> FORMULA
Implication FORMULA
x FORMULA
y Range
n, FORMULA -> FORMULA -> Range -> FORMULA
Implication FORMULA
y FORMULA
x Range
n] Range
n }

elimImpl :: FORMULA -> FORMULA
elimImpl :: FORMULA -> FORMULA
elimImpl = FoldRecord FORMULA -> FORMULA -> FORMULA
forall a. FoldRecord a -> FORMULA -> a
foldFormula FoldRecord FORMULA
mapRecord
{ foldImplication :: FORMULA -> FORMULA -> Range -> FORMULA
foldImplication = \ x :: FORMULA
x y :: FORMULA
y n :: Range
n ->
[FORMULA] -> Range -> FORMULA
Disjunction [FORMULA -> Range -> FORMULA
Negation FORMULA
x Range
n, FORMULA
y] Range
n }

negForm :: Range -> FORMULA -> FORMULA
negForm :: Range -> FORMULA -> FORMULA
negForm r :: Range
r frm :: FORMULA
frm = case FORMULA
frm of
Negation f :: FORMULA
f _ -> case FORMULA
f of
Negation nf :: FORMULA
nf _ -> Range -> FORMULA -> FORMULA
negForm Range
r FORMULA
nf
_ -> FORMULA
f
Conjunction xs :: [FORMULA]
xs n :: Range
n -> [FORMULA] -> Range -> FORMULA
Disjunction ((FORMULA -> FORMULA) -> [FORMULA] -> [FORMULA]
forall a b. (a -> b) -> [a] -> [b]
map (Range -> FORMULA -> FORMULA
negForm Range
r) [FORMULA]
xs) Range
n
Disjunction xs :: [FORMULA]
xs n :: Range
n -> [FORMULA] -> Range -> FORMULA
Conjunction ((FORMULA -> FORMULA) -> [FORMULA] -> [FORMULA]
forall a b. (a -> b) -> [a] -> [b]
map (Range -> FORMULA -> FORMULA
negForm Range
r) [FORMULA]
xs) Range
n
True_atom n :: Range
n -> Range -> FORMULA
False_atom Range
n
False_atom n :: Range
n -> Range -> FORMULA
True_atom Range
n
_ -> FORMULA -> Range -> FORMULA
Negation FORMULA
frm Range
r

moveNegIn :: FORMULA -> FORMULA
moveNegIn :: FORMULA -> FORMULA
moveNegIn frm :: FORMULA
frm = case FORMULA
frm of
Negation f :: FORMULA
f n :: Range
n -> Range -> FORMULA -> FORMULA
negForm Range
n FORMULA
f
Conjunction xs :: [FORMULA]
xs n :: Range
n -> [FORMULA] -> Range -> FORMULA
Conjunction ((FORMULA -> FORMULA) -> [FORMULA] -> [FORMULA]
forall a b. (a -> b) -> [a] -> [b]
map FORMULA -> FORMULA
moveNegIn [FORMULA]
xs) Range
n
Disjunction xs :: [FORMULA]
xs n :: Range
n -> [FORMULA] -> Range -> FORMULA
Disjunction ((FORMULA -> FORMULA) -> [FORMULA] -> [FORMULA]
forall a b. (a -> b) -> [a] -> [b]
map FORMULA -> FORMULA
moveNegIn [FORMULA]
xs) Range
n
_ -> FORMULA
frm

distributeAndOverOr :: FORMULA -> FORMULA
distributeAndOverOr :: FORMULA -> FORMULA
distributeAndOverOr f :: FORMULA
f = case FORMULA
f of
Conjunction xs :: [FORMULA]
xs n :: Range
n -> [FORMULA] -> Range -> FORMULA
mkConj ((FORMULA -> FORMULA) -> [FORMULA] -> [FORMULA]
forall a b. (a -> b) -> [a] -> [b]
map FORMULA -> FORMULA
distributeAndOverOr [FORMULA]
xs) Range
n
Disjunction xs :: [FORMULA]
xs n :: Range
n -> if (FORMULA -> Bool) -> [FORMULA] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all FORMULA -> Bool
isPrimForm [FORMULA]
xs then [FORMULA] -> Range -> FORMULA
mkDisj [FORMULA]
xs Range
n else
FORMULA -> FORMULA
distributeAndOverOr
(FORMULA -> FORMULA) -> FORMULA -> FORMULA
forall a b. (a -> b) -> a -> b
\$ [FORMULA] -> Range -> FORMULA
mkConj (([FORMULA] -> FORMULA) -> [[FORMULA]] -> [FORMULA]
forall a b. (a -> b) -> [a] -> [b]
map ([FORMULA] -> Range -> FORMULA
`mkDisj` Range
n) ([[FORMULA]] -> [FORMULA])
-> ([[FORMULA]] -> [[FORMULA]]) -> [[FORMULA]] -> [FORMULA]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[FORMULA]] -> [[FORMULA]]
forall a. [[a]] -> [[a]]
combine ([[FORMULA]] -> [FORMULA]) -> [[FORMULA]] -> [FORMULA]
forall a b. (a -> b) -> a -> b
\$ (FORMULA -> [FORMULA]) -> [FORMULA] -> [[FORMULA]]
forall a b. (a -> b) -> [a] -> [b]
map FORMULA -> [FORMULA]
getConj [FORMULA]
xs) Range
n
_ -> FORMULA
f

cnf :: FORMULA -> FORMULA
cnf :: FORMULA -> FORMULA
cnf = FORMULA -> FORMULA
flipLiterals (FORMULA -> FORMULA) -> (FORMULA -> FORMULA) -> FORMULA -> FORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA -> FORMULA
distributeAndOverOr (FORMULA -> FORMULA) -> (FORMULA -> FORMULA) -> FORMULA -> FORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA -> FORMULA
moveNegIn (FORMULA -> FORMULA) -> (FORMULA -> FORMULA) -> FORMULA -> FORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA -> FORMULA
elimImpl (FORMULA -> FORMULA) -> (FORMULA -> FORMULA) -> FORMULA -> FORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA -> FORMULA
elimEquiv

flipLiterals :: FORMULA -> FORMULA
flipLiterals :: FORMULA -> FORMULA
flipLiterals f :: FORMULA
f = case FORMULA
f of
Negation p :: FORMULA
p@(Predication _) _ -> FORMULA
p
Predication t :: Token
t -> FORMULA -> Range -> FORMULA
Negation FORMULA
f (Range -> FORMULA) -> Range -> FORMULA
forall a b. (a -> b) -> a -> b
\$ Token -> Range
tokPos Token
t
Conjunction xs :: [FORMULA]
xs n :: Range
n -> [FORMULA] -> Range -> FORMULA
Conjunction ((FORMULA -> FORMULA) -> [FORMULA] -> [FORMULA]
forall a b. (a -> b) -> [a] -> [b]
map FORMULA -> FORMULA
flipLiterals [FORMULA]
xs) Range
n
Disjunction xs :: [FORMULA]
xs n :: Range
n -> [FORMULA] -> Range -> FORMULA
Disjunction ((FORMULA -> FORMULA) -> [FORMULA] -> [FORMULA]
forall a b. (a -> b) -> [a] -> [b]
map FORMULA -> FORMULA
flipLiterals [FORMULA]
xs) Range
n
_ -> FORMULA
f

distributeOrOverAnd :: FORMULA -> FORMULA
distributeOrOverAnd :: FORMULA -> FORMULA
distributeOrOverAnd f :: FORMULA
f = case FORMULA
f of
Disjunction xs :: [FORMULA]
xs n :: Range
n -> [FORMULA] -> Range -> FORMULA
mkDisj ((FORMULA -> FORMULA) -> [FORMULA] -> [FORMULA]
forall a b. (a -> b) -> [a] -> [b]
map FORMULA -> FORMULA
distributeOrOverAnd [FORMULA]
xs) Range
n
Conjunction xs :: [FORMULA]
xs n :: Range
n -> if (FORMULA -> Bool) -> [FORMULA] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all FORMULA -> Bool
isPrimForm [FORMULA]
xs then [FORMULA] -> Range -> FORMULA
mkConj [FORMULA]
xs Range
n else
FORMULA -> FORMULA
distributeOrOverAnd
(FORMULA -> FORMULA) -> FORMULA -> FORMULA
forall a b. (a -> b) -> a -> b
\$ [FORMULA] -> Range -> FORMULA
mkDisj (([FORMULA] -> FORMULA) -> [[FORMULA]] -> [FORMULA]
forall a b. (a -> b) -> [a] -> [b]
map ([FORMULA] -> Range -> FORMULA
`mkConj` Range
n) ([[FORMULA]] -> [FORMULA])
-> ([[FORMULA]] -> [[FORMULA]]) -> [[FORMULA]] -> [FORMULA]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[FORMULA]] -> [[FORMULA]]
forall a. [[a]] -> [[a]]
combine ([[FORMULA]] -> [FORMULA]) -> [[FORMULA]] -> [FORMULA]
forall a b. (a -> b) -> a -> b
\$ (FORMULA -> [FORMULA]) -> [FORMULA] -> [[FORMULA]]
forall a b. (a -> b) -> [a] -> [b]
map FORMULA -> [FORMULA]
getDisj [FORMULA]
xs) Range
n
_ -> FORMULA
f

dnf :: FORMULA -> FORMULA
dnf :: FORMULA -> FORMULA
dnf = FORMULA -> FORMULA
distributeOrOverAnd (FORMULA -> FORMULA) -> (FORMULA -> FORMULA) -> FORMULA -> FORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA -> FORMULA
moveNegIn (FORMULA -> FORMULA) -> (FORMULA -> FORMULA) -> FORMULA -> FORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA -> FORMULA
elimImpl (FORMULA -> FORMULA) -> (FORMULA -> FORMULA) -> FORMULA -> FORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA -> FORMULA
elimEquiv

combine :: [[a]] -> [[a]]
combine :: [[a]] -> [[a]]
combine l :: [[a]]
l = case [[a]]
l of
[] -> [[]]
h :: [a]
h : t :: [[a]]
t -> ([a] -> [[a]]) -> [[a]] -> [[a]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (((a -> [a]) -> [a] -> [[a]]) -> [a] -> (a -> [a]) -> [[a]]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (a -> [a]) -> [a] -> [[a]]
forall a b. (a -> b) -> [a] -> [b]
map [a]
h ((a -> [a]) -> [[a]]) -> ([a] -> a -> [a]) -> [a] -> [[a]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> [a] -> [a]) -> [a] -> a -> [a]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (:)) ([[a]] -> [[a]]
forall a. [[a]] -> [[a]]
combine [[a]]
t)
```