{- |
Module      :  ./Propositional/Fold.hs
Description :  folding function for propositional formulas
Copyright   :  (c) Christian Maeder, DFKI GmbH 2009
License     :  GPLv2 or higher, see LICENSE.txt

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)