-- | Prenex and Skolem normal forms.
--
-- Copyright (c) 2003-2007, John Harrison. (See "LICENSE.txt" for details.)

{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}

module Data.Logic.ATP.Skolem
    (
    -- * Class of Skolem functions
      HasSkolem(SVarOf, toSkolem, foldSkolem, variantSkolem)
    , showSkolem
    , prettySkolem
    -- * Skolem monad
    , SkolemM
    , runSkolem
    , SkolemT
    , runSkolemT
    -- * Skolemization procedure
    , simplify
    , nnf
    , pnf
    , skolems
    , askolemize
    , skolemize
    , specialize
    -- * Normalization
    , simpdnf'
    , simpcnf'
    -- * Instances
    , Function(Fn, Skolem)
    , Formula, SkTerm, SkAtom
    -- * Tests
    , testSkolem
    ) where

import Control.Monad.Identity (Identity, runIdentity)
import Control.Monad.State (runStateT, StateT, get, modify)
import Data.Data (Data)
import Data.List as List (map)
import Data.Logic.ATP.Apply (functions, HasApply(TermOf, PredOf), pApp, Predicate)
import Data.Logic.ATP.Equate (FOL)
import Data.Logic.ATP.FOL (fv, IsFirstOrder, subst)
import Data.Logic.ATP.Formulas (IsFormula(AtomOf), false, true, atomic)
import Data.Logic.ATP.Lib (setAny, distrib)
import Data.Logic.ATP.Lit ((.~.), negate)
import Data.Logic.ATP.Pretty (brackets, Doc, Pretty(pPrint), prettyShow, text)
import Data.Logic.ATP.Prop ((.&.), (.|.), (.=>.), (.<=>.), BinOp((:&:), (:|:), (:=>:), (:<=>:)),
                            convertToPropositional, foldPropositional', JustPropositional, PFormula, psimplify1, trivial)
import Data.Logic.ATP.Quantified (exists, for_all, IsQuantified(VarOf, foldQuantified),
                                  QFormula, quant, Quant((:?:), (:!:)))
import Data.Logic.ATP.Term (fApp, IsFunction, IsTerm(TVarOf, FunOf), IsVariable, Term, V, variant, vt)
import Data.Map.Strict as Map (singleton)
import Data.Monoid ((<>))
import Data.Set as Set (empty, filter, insert, isProperSubsetOf, map, member, notMember, Set, singleton, toAscList, union)
import Data.String (IsString(fromString))
import Data.Typeable (Typeable)
import Prelude hiding (negate)
import Test.HUnit

-- | Class of functions that include embedded Skolem functions
--
-- A Skolem function is created to eliminate an an existentially
-- quantified variable.  The idea is that if we have a predicate
-- @P[x,y,z]@, and @z@ is existentially quantified, then @P@ is only
-- satisfiable if there *exists* at least one @z@ that causes @P@ to
-- be true.  Therefore, we envision a function @sKz[x,y]@ whose value
-- is one of the z's that cause @P@ to be satisfied (if there are any;
-- if the formula is satisfiable there must be.)  Because we are
-- trying to determine if there is a satisfying triple @x, y, z@, the
-- Skolem function @sKz@ will have to be a function of @x@ and @y@, so
-- we make these parameters.  Now, if @P[x,y,z]@ is satisfiable, there
-- will be a function sKz which can be substituted in such that
-- @P[x,y,sKz[x,y]]@ is also satisfiable.  Thus, using this mechanism
-- we can eliminate all the formula's existential quantifiers and some
-- of its variables.
class (IsFunction function, IsVariable (SVarOf function)) => HasSkolem function where
    type SVarOf function
    toSkolem :: SVarOf function -> Int -> function
    -- ^ Create a skolem function with a variant number that differs
    -- from all the members of the set.
    foldSkolem :: (function -> r) -> (SVarOf function -> Int -> r) -> function -> r
    variantSkolem :: function -> Set function -> function
    -- ^ Return a function based on f but different from any set
    -- element.  The result may be f itself if f is not a member of
    -- the set.

-- fromSkolem :: HasSkolem function v => function -> Maybe v
-- fromSkolem = foldSkolem (const Nothing) Just

showSkolem :: (HasSkolem function, IsVariable (SVarOf function)) => function -> String
showSkolem :: forall function.
(HasSkolem function, IsVariable (SVarOf function)) =>
function -> String
showSkolem = (function -> String)
-> (SVarOf function -> Int -> String) -> function -> String
forall function r.
HasSkolem function =>
(function -> r) -> (SVarOf function -> Int -> r) -> function -> r
forall r.
(function -> r) -> (SVarOf function -> Int -> r) -> function -> r
foldSkolem (String -> String
forall a. Show a => a -> String
show (String -> String) -> (function -> String) -> function -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. function -> String
forall a. Pretty a => a -> String
prettyShow) (\SVarOf function
v Int
n -> String
"(toSkolem " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SVarOf function -> String
forall a. Show a => a -> String
show SVarOf function
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")")

prettySkolem :: HasSkolem function => (function -> Doc) -> function -> Doc
prettySkolem :: forall function.
HasSkolem function =>
(function -> Doc) -> function -> Doc
prettySkolem function -> Doc
prettyFunction =
    (function -> Doc)
-> (SVarOf function -> Int -> Doc) -> function -> Doc
forall function r.
HasSkolem function =>
(function -> r) -> (SVarOf function -> Int -> r) -> function -> r
forall r.
(function -> r) -> (SVarOf function -> Int -> r) -> function -> r
foldSkolem function -> Doc
prettyFunction (\SVarOf function
v Int
n -> String -> Doc
text String
"sK" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
brackets (SVarOf function -> Doc
forall a. Pretty a => a -> Doc
pPrint SVarOf function
v Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 then Doc
forall a. Monoid a => a
mempty else (String -> Doc
text String
"." Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
forall a. Pretty a => a -> Doc
pPrint (Int -> String
forall a. Show a => a -> String
show Int
n))))

-- | State monad for generating Skolem functions and constants.
type SkolemT m function = StateT (SkolemState function) m
type SkolemM function = StateT (SkolemState function) Identity

-- | The state associated with the Skolem monad.
data SkolemState function
    = SkolemState
      { forall function. SkolemState function -> Set function
skolemSet :: Set function
        -- ^ The set of allocated skolem functions
      , forall function. SkolemState function -> [String]
univQuant :: [String]
        -- ^ The variables which are universally quantified in the
        -- current scope, in the order they were encountered.  During
        -- Skolemization these are the parameters passed to the Skolem
        -- function.
      }

-- | Run a computation in a stacked invocation of the Skolem monad.
runSkolemT :: (Monad m, IsFunction function) => SkolemT m function a -> m a
runSkolemT :: forall (m :: * -> *) function a.
(Monad m, IsFunction function) =>
SkolemT m function a -> m a
runSkolemT SkolemT m function a
action = (SkolemT m function a
-> SkolemState function -> m (a, SkolemState function)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT SkolemT m function a
action) SkolemState function
forall function. IsFunction function => SkolemState function
newSkolemState m (a, SkolemState function)
-> ((a, SkolemState function) -> m a) -> m a
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> m a)
-> ((a, SkolemState function) -> a)
-> (a, SkolemState function)
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, SkolemState function) -> a
forall a b. (a, b) -> a
fst
    where
      newSkolemState :: IsFunction function => SkolemState function
      newSkolemState :: forall function. IsFunction function => SkolemState function
newSkolemState
          = SkolemState
            { skolemSet :: Set function
skolemSet = Set function
forall a. Monoid a => a
mempty
            , univQuant :: [String]
univQuant = []
            }

-- | Run a pure computation in the Skolem monad.
runSkolem :: IsFunction function => SkolemT Identity function a -> a
runSkolem :: forall function a.
IsFunction function =>
SkolemT Identity function a -> a
runSkolem = Identity a -> a
forall a. Identity a -> a
runIdentity (Identity a -> a)
-> (SkolemT Identity function a -> Identity a)
-> SkolemT Identity function a
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SkolemT Identity function a -> Identity a
forall (m :: * -> *) function a.
(Monad m, IsFunction function) =>
SkolemT m function a -> m a
runSkolemT

-- -------------------------------------------------------------------------
-- Simplification, normal forms, and the skolemization procedure
-- -------------------------------------------------------------------------

-- | Routine simplification. Like "psimplify" but with quantifier clauses.
simplify :: IsFirstOrder formula => formula -> formula
simplify :: forall formula. IsFirstOrder formula => formula -> formula
simplify formula
fm =
    (Quant -> VarOf formula -> formula -> formula)
-> (formula -> BinOp -> formula -> formula)
-> (formula -> formula)
-> (Bool -> formula)
-> (AtomOf formula -> formula)
-> formula
-> formula
forall formula r.
IsQuantified formula =>
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
forall r.
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
foldQuantified Quant -> VarOf formula -> formula -> formula
forall {formula}.
IsFirstOrder formula =>
Quant -> VarOf formula -> formula -> formula
qu formula -> BinOp -> formula -> formula
forall {formula}.
IsFirstOrder formula =>
formula -> BinOp -> formula -> formula
co formula -> formula
forall formula. IsFirstOrder formula => formula -> formula
ne (\Bool
_ -> formula
fm) (\AtomOf formula
_ -> formula
fm) formula
fm
    where
      qu :: Quant -> VarOf formula -> formula -> formula
qu Quant
(:!:) VarOf formula
x formula
p = formula -> formula
forall formula. IsFirstOrder formula => formula -> formula
simplify1 (VarOf formula -> formula -> formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all VarOf formula
x (formula -> formula
forall formula. IsFirstOrder formula => formula -> formula
simplify formula
p))
      qu Quant
(:?:) VarOf formula
x formula
p = formula -> formula
forall formula. IsFirstOrder formula => formula -> formula
simplify1 (VarOf formula -> formula -> formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists VarOf formula
x (formula -> formula
forall formula. IsFirstOrder formula => formula -> formula
simplify formula
p))
      ne :: formula -> formula
ne formula
p = formula -> formula
forall formula. IsFirstOrder formula => formula -> formula
simplify1 (formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) (formula -> formula
forall formula. IsFirstOrder formula => formula -> formula
simplify formula
p))
      co :: formula -> BinOp -> formula -> formula
co formula
p BinOp
(:&:) formula
q = formula -> formula
forall formula. IsFirstOrder formula => formula -> formula
simplify1 (formula -> formula
forall formula. IsFirstOrder formula => formula -> formula
simplify formula
p formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. formula -> formula
forall formula. IsFirstOrder formula => formula -> formula
simplify formula
q)
      co formula
p BinOp
(:|:) formula
q = formula -> formula
forall formula. IsFirstOrder formula => formula -> formula
simplify1 (formula -> formula
forall formula. IsFirstOrder formula => formula -> formula
simplify formula
p formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. formula -> formula
forall formula. IsFirstOrder formula => formula -> formula
simplify formula
q)
      co formula
p BinOp
(:=>:) formula
q = formula -> formula
forall formula. IsFirstOrder formula => formula -> formula
simplify1 (formula -> formula
forall formula. IsFirstOrder formula => formula -> formula
simplify formula
p formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. formula -> formula
forall formula. IsFirstOrder formula => formula -> formula
simplify formula
q)
      co formula
p BinOp
(:<=>:) formula
q = formula -> formula
forall formula. IsFirstOrder formula => formula -> formula
simplify1 (formula -> formula
forall formula. IsFirstOrder formula => formula -> formula
simplify formula
p formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. formula -> formula
forall formula. IsFirstOrder formula => formula -> formula
simplify formula
q)

simplify1 :: IsFirstOrder formula => formula -> formula
simplify1 :: forall formula. IsFirstOrder formula => formula -> formula
simplify1 formula
fm =
    (Quant -> VarOf formula -> formula -> formula)
-> (formula -> BinOp -> formula -> formula)
-> (formula -> formula)
-> (Bool -> formula)
-> (AtomOf formula -> formula)
-> formula
-> formula
forall formula r.
IsQuantified formula =>
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
forall r.
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
foldQuantified Quant -> TVarOf (TermOf (AtomOf formula)) -> formula -> formula
Quant -> VarOf formula -> formula -> formula
qu (\formula
_ BinOp
_ formula
_ -> formula -> formula
forall formula. IsPropositional formula => formula -> formula
psimplify1 formula
fm) (\formula
_ -> formula -> formula
forall formula. IsPropositional formula => formula -> formula
psimplify1 formula
fm) (\Bool
_ -> formula -> formula
forall formula. IsPropositional formula => formula -> formula
psimplify1 formula
fm) (\AtomOf formula
_ -> formula -> formula
forall formula. IsPropositional formula => formula -> formula
psimplify1 formula
fm) formula
fm
    where
      qu :: Quant -> TVarOf (TermOf (AtomOf formula)) -> formula -> formula
qu Quant
_ TVarOf (TermOf (AtomOf formula))
x formula
p = if TVarOf (TermOf (AtomOf formula))
-> Set (TVarOf (TermOf (AtomOf formula))) -> Bool
forall a. Ord a => a -> Set a -> Bool
member TVarOf (TermOf (AtomOf formula))
x (formula -> Set (TVarOf (TermOf (AtomOf formula)))
forall formula v.
(IsFirstOrder formula, v ~ VarOf formula) =>
formula -> Set v
fv formula
p) then formula
fm else formula
p

-- Example.
test01 :: Test
test01 :: Test
test01 = 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
"simplify (p. 140) " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Formula -> String
forall a. Pretty a => a -> String
prettyShow Formula
fm) String
expected String
input
    where input :: String
input = Formula -> String
forall a. Pretty a => a -> String
prettyShow (Formula -> Formula
forall formula. IsFirstOrder formula => formula -> formula
simplify Formula
fm)
          expected :: String
expected = Formula -> String
forall a. Pretty a => a -> String
prettyShow ((VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"x" (PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
"P" [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"x"])) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. (PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
"Q" []) :: Formula)
          fm :: Formula
          fm :: Formula
fm = (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"x" (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"y" (PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
"P" [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"x"] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. (PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
"P" [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"y"] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. Formula
forall formula. IsFormula formula => formula
false)))) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists V
VarOf Formula
"z" (PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
"Q" [])

-- | Negation normal form for first order formulas
nnf :: IsFirstOrder formula => formula -> formula
nnf :: forall formula. IsFirstOrder formula => formula -> formula
nnf = formula -> formula
forall formula. IsQuantified formula => formula -> formula
nnf1 (formula -> formula) -> (formula -> formula) -> formula -> formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. formula -> formula
forall formula. IsFirstOrder formula => formula -> formula
simplify

nnf1 :: IsQuantified formula => formula -> formula
nnf1 :: forall formula. IsQuantified formula => formula -> formula
nnf1 formula
fm =
    (Quant -> VarOf formula -> formula -> formula)
-> (formula -> BinOp -> formula -> formula)
-> (formula -> formula)
-> (Bool -> formula)
-> (AtomOf formula -> formula)
-> formula
-> formula
forall formula r.
IsQuantified formula =>
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
forall r.
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
foldQuantified Quant -> VarOf formula -> formula -> formula
forall {formula}.
IsQuantified formula =>
Quant -> VarOf formula -> formula -> formula
qu formula -> BinOp -> formula -> formula
forall {formula}.
IsQuantified formula =>
formula -> BinOp -> formula -> formula
co formula -> formula
ne (\Bool
_ -> formula
fm) (\AtomOf formula
_ -> formula
fm) formula
fm
    where
      qu :: Quant -> VarOf formula -> formula -> formula
qu Quant
(:!:) VarOf formula
x formula
p = Quant -> VarOf formula -> formula -> formula
forall {formula}.
IsQuantified formula =>
Quant -> VarOf formula -> formula -> formula
quant Quant
(:!:) VarOf formula
x (formula -> formula
forall formula. IsQuantified formula => formula -> formula
nnf1 formula
p)
      qu Quant
(:?:) VarOf formula
x formula
p = Quant -> VarOf formula -> formula -> formula
forall {formula}.
IsQuantified formula =>
Quant -> VarOf formula -> formula -> formula
quant Quant
(:?:) VarOf formula
x (formula -> formula
forall formula. IsQuantified formula => formula -> formula
nnf1 formula
p)
      ne :: formula -> formula
ne formula
p = (Quant -> VarOf formula -> formula -> formula)
-> (formula -> BinOp -> formula -> formula)
-> (formula -> formula)
-> (Bool -> formula)
-> (AtomOf formula -> formula)
-> formula
-> formula
forall formula r.
IsQuantified formula =>
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
forall r.
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
foldQuantified Quant -> VarOf formula -> formula -> formula
forall {formula}.
IsQuantified formula =>
Quant -> VarOf formula -> formula -> formula
quNot formula -> BinOp -> formula -> formula
forall {formula}.
IsQuantified formula =>
formula -> BinOp -> formula -> formula
coNot formula -> formula
forall formula. IsQuantified formula => formula -> formula
neNot (\Bool
_ -> formula
fm) (\AtomOf formula
_ -> formula
fm) formula
p
      co :: formula -> BinOp -> formula -> formula
co formula
p BinOp
(:&:) formula
q = formula -> formula
forall formula. IsQuantified formula => formula -> formula
nnf1 formula
p formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. formula -> formula
forall formula. IsQuantified formula => formula -> formula
nnf1 formula
q
      co formula
p BinOp
(:|:) formula
q = formula -> formula
forall formula. IsQuantified formula => formula -> formula
nnf1 formula
p formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. formula -> formula
forall formula. IsQuantified formula => formula -> formula
nnf1 formula
q
      co formula
p BinOp
(:=>:) formula
q = formula -> formula
forall formula. IsQuantified formula => formula -> formula
nnf1 (formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) formula
p) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. formula -> formula
forall formula. IsQuantified formula => formula -> formula
nnf1 formula
q
      co formula
p BinOp
(:<=>:) formula
q = (formula -> formula
forall formula. IsQuantified formula => formula -> formula
nnf1 formula
p formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. formula -> formula
forall formula. IsQuantified formula => formula -> formula
nnf1 formula
q) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. (formula -> formula
forall formula. IsQuantified formula => formula -> formula
nnf1 (formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) formula
p) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. formula -> formula
forall formula. IsQuantified formula => formula -> formula
nnf1 (formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) formula
q))
      quNot :: Quant -> VarOf formula -> formula -> formula
quNot Quant
(:!:) VarOf formula
x formula
p = Quant -> VarOf formula -> formula -> formula
forall {formula}.
IsQuantified formula =>
Quant -> VarOf formula -> formula -> formula
quant Quant
(:?:) VarOf formula
x (formula -> formula
forall formula. IsQuantified formula => formula -> formula
nnf1 (formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) formula
p))
      quNot Quant
(:?:) VarOf formula
x formula
p = Quant -> VarOf formula -> formula -> formula
forall {formula}.
IsQuantified formula =>
Quant -> VarOf formula -> formula -> formula
quant Quant
(:!:) VarOf formula
x (formula -> formula
forall formula. IsQuantified formula => formula -> formula
nnf1 (formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) formula
p))
      neNot :: formula -> formula
neNot formula
p = formula -> formula
forall formula. IsQuantified formula => formula -> formula
nnf1 formula
p
      coNot :: formula -> BinOp -> formula -> formula
coNot formula
p BinOp
(:&:) formula
q = formula -> formula
forall formula. IsQuantified formula => formula -> formula
nnf1 (formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) formula
p) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. formula -> formula
forall formula. IsQuantified formula => formula -> formula
nnf1 (formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) formula
q)
      coNot formula
p BinOp
(:|:) formula
q = formula -> formula
forall formula. IsQuantified formula => formula -> formula
nnf1 (formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) formula
p) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. formula -> formula
forall formula. IsQuantified formula => formula -> formula
nnf1 (formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) formula
q)
      coNot formula
p BinOp
(:=>:) formula
q = formula -> formula
forall formula. IsQuantified formula => formula -> formula
nnf1 formula
p formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. formula -> formula
forall formula. IsQuantified formula => formula -> formula
nnf1 (formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) formula
q)
      coNot formula
p BinOp
(:<=>:) formula
q = (formula -> formula
forall formula. IsQuantified formula => formula -> formula
nnf1 formula
p formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. formula -> formula
forall formula. IsQuantified formula => formula -> formula
nnf1 (formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) formula
q)) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. (formula -> formula
forall formula. IsQuantified formula => formula -> formula
nnf1 (formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) formula
p) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. formula -> formula
forall formula. IsQuantified formula => formula -> formula
nnf1 formula
q)

-- Example of NNF function in action.
test02 :: Test
test02 :: Test
test02 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> Formula -> Formula -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"nnf (p. 140)" Formula
expected Formula
input
    where p :: Predicate
p = Predicate
"P"
          q :: Predicate
q = Predicate
"Q"
          input :: Formula
input = Formula -> Formula
forall formula. IsFirstOrder formula => formula -> formula
nnf Formula
fm
          expected :: Formula
expected = VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists V
VarOf Formula
"x" (Formula -> Formula
forall formula. IsLiteral formula => formula -> formula
(.~.)(PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
p [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"x"])) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                     ((VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists V
VarOf Formula
"y" (PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
q [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"y"]) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists V
VarOf Formula
"z" ((PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
p [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"z"]) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
q [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"z"]))) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                      (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"y" (Formula -> Formula
forall formula. IsLiteral formula => formula -> formula
(.~.)(PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
q [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"y"])) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&.
                       VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"z" ((Formula -> Formula
forall formula. IsLiteral formula => formula -> formula
(.~.)(PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
p [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"z"])) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. (Formula -> Formula
forall formula. IsLiteral formula => formula -> formula
(.~.)(PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
q [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"z"])))) :: Formula)
          fm :: Formula
          fm :: Formula
fm = (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"x" (PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
p [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"x"])) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. ((VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists V
VarOf Formula
"y" (PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
q [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"y"])) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists V
VarOf Formula
"z" (PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
p [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"z"] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
q [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"z"]))

-- | Prenex normal form.
pnf :: IsFirstOrder formula => formula -> formula
pnf :: forall formula. IsFirstOrder formula => formula -> formula
pnf = formula -> formula
forall formula. IsFirstOrder formula => formula -> formula
prenex (formula -> formula) -> (formula -> formula) -> formula -> formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. formula -> formula
forall formula. IsFirstOrder formula => formula -> formula
nnf (formula -> formula) -> (formula -> formula) -> formula -> formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. formula -> formula
forall formula. IsFirstOrder formula => formula -> formula
simplify

prenex :: IsFirstOrder formula => formula -> formula
prenex :: forall formula. IsFirstOrder formula => formula -> formula
prenex formula
fm =
    (Quant -> VarOf formula -> formula -> formula)
-> (formula -> BinOp -> formula -> formula)
-> (formula -> formula)
-> (Bool -> formula)
-> (AtomOf formula -> formula)
-> formula
-> formula
forall formula r.
IsQuantified formula =>
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
forall r.
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
foldQuantified Quant -> VarOf formula -> formula -> formula
forall {formula}.
IsFirstOrder formula =>
Quant -> VarOf formula -> formula -> formula
qu formula -> BinOp -> formula -> formula
co (\ formula
_ -> formula
fm) (\ Bool
_ -> formula
fm) (\ AtomOf formula
_ -> formula
fm) formula
fm
    where
      qu :: Quant -> VarOf formula -> formula -> formula
qu Quant
op VarOf formula
x formula
p = Quant -> VarOf formula -> formula -> formula
forall {formula}.
IsQuantified formula =>
Quant -> VarOf formula -> formula -> formula
quant Quant
op VarOf formula
x (formula -> formula
forall formula. IsFirstOrder formula => formula -> formula
prenex formula
p)
      co :: formula -> BinOp -> formula -> formula
co formula
l BinOp
(:&:) formula
r = formula -> formula
forall formula. IsFirstOrder formula => formula -> formula
pullquants (formula -> formula
forall formula. IsFirstOrder formula => formula -> formula
prenex formula
l formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. formula -> formula
forall formula. IsFirstOrder formula => formula -> formula
prenex formula
r)
      co formula
l BinOp
(:|:) formula
r = formula -> formula
forall formula. IsFirstOrder formula => formula -> formula
pullquants (formula -> formula
forall formula. IsFirstOrder formula => formula -> formula
prenex formula
l formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. formula -> formula
forall formula. IsFirstOrder formula => formula -> formula
prenex formula
r)
      co formula
_ BinOp
_ formula
_ = formula
fm

pullquants :: IsFirstOrder formula => formula -> formula
pullquants :: forall formula. IsFirstOrder formula => formula -> formula
pullquants formula
fm =
    (Quant -> VarOf formula -> formula -> formula)
-> (formula -> BinOp -> formula -> formula)
-> (formula -> formula)
-> (Bool -> formula)
-> (AtomOf formula -> formula)
-> formula
-> formula
forall formula r.
IsQuantified formula =>
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
forall r.
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
foldQuantified (\Quant
_ VarOf formula
_ formula
_ -> formula
fm) formula -> BinOp -> formula -> formula
pullQuantsCombine (\formula
_ -> formula
fm) (\Bool
_ -> formula
fm) (\AtomOf formula
_ -> formula
fm) formula
fm
    where
      pullQuantsCombine :: formula -> BinOp -> formula -> formula
pullQuantsCombine formula
l BinOp
op formula
r =
          case (formula -> Maybe (Quant, VarOf formula, formula)
getQuant formula
l, BinOp
op, formula -> Maybe (Quant, VarOf formula, formula)
getQuant formula
r) of
            (Just (Quant
(:!:), TVarOf (TermOf (AtomOf formula))
vl, formula
l'), BinOp
(:&:), Just (Quant
(:!:), TVarOf (TermOf (AtomOf formula))
vr, formula
r')) -> (Bool, Bool)
-> formula
-> (TVarOf (TermOf (AtomOf formula)) -> formula -> formula)
-> (formula -> formula -> formula)
-> TVarOf (TermOf (AtomOf formula))
-> TVarOf (TermOf (AtomOf formula))
-> formula
-> formula
-> formula
forall formula v.
(IsFirstOrder formula, v ~ VarOf formula) =>
(Bool, Bool)
-> formula
-> (v -> formula -> formula)
-> (formula -> formula -> formula)
-> v
-> v
-> formula
-> formula
-> formula
pullq (Bool
True,  Bool
True)  formula
fm TVarOf (TermOf (AtomOf formula)) -> formula -> formula
VarOf formula -> formula -> formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(.&.) TVarOf (TermOf (AtomOf formula))
vl TVarOf (TermOf (AtomOf formula))
vr formula
l' formula
r'
            (Just (Quant
(:?:), TVarOf (TermOf (AtomOf formula))
vl, formula
l'), BinOp
(:|:), Just (Quant
(:?:), TVarOf (TermOf (AtomOf formula))
vr, formula
r')) -> (Bool, Bool)
-> formula
-> (TVarOf (TermOf (AtomOf formula)) -> formula -> formula)
-> (formula -> formula -> formula)
-> TVarOf (TermOf (AtomOf formula))
-> TVarOf (TermOf (AtomOf formula))
-> formula
-> formula
-> formula
forall formula v.
(IsFirstOrder formula, v ~ VarOf formula) =>
(Bool, Bool)
-> formula
-> (v -> formula -> formula)
-> (formula -> formula -> formula)
-> v
-> v
-> formula
-> formula
-> formula
pullq (Bool
True,  Bool
True)  formula
fm TVarOf (TermOf (AtomOf formula)) -> formula -> formula
VarOf formula -> formula -> formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists  formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(.|.) TVarOf (TermOf (AtomOf formula))
vl TVarOf (TermOf (AtomOf formula))
vr formula
l' formula
r'
            (Just (Quant
(:!:), TVarOf (TermOf (AtomOf formula))
vl, formula
l'), BinOp
(:&:), Maybe (Quant, TVarOf (TermOf (AtomOf formula)), formula)
_)                    -> (Bool, Bool)
-> formula
-> (TVarOf (TermOf (AtomOf formula)) -> formula -> formula)
-> (formula -> formula -> formula)
-> TVarOf (TermOf (AtomOf formula))
-> TVarOf (TermOf (AtomOf formula))
-> formula
-> formula
-> formula
forall formula v.
(IsFirstOrder formula, v ~ VarOf formula) =>
(Bool, Bool)
-> formula
-> (v -> formula -> formula)
-> (formula -> formula -> formula)
-> v
-> v
-> formula
-> formula
-> formula
pullq (Bool
True,  Bool
False) formula
fm TVarOf (TermOf (AtomOf formula)) -> formula -> formula
VarOf formula -> formula -> formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(.&.) TVarOf (TermOf (AtomOf formula))
vl TVarOf (TermOf (AtomOf formula))
vl formula
l' formula
r
            (Maybe (Quant, TVarOf (TermOf (AtomOf formula)), formula)
_,                    BinOp
(:&:), Just (Quant
(:!:), TVarOf (TermOf (AtomOf formula))
vr, formula
r')) -> (Bool, Bool)
-> formula
-> (TVarOf (TermOf (AtomOf formula)) -> formula -> formula)
-> (formula -> formula -> formula)
-> TVarOf (TermOf (AtomOf formula))
-> TVarOf (TermOf (AtomOf formula))
-> formula
-> formula
-> formula
forall formula v.
(IsFirstOrder formula, v ~ VarOf formula) =>
(Bool, Bool)
-> formula
-> (v -> formula -> formula)
-> (formula -> formula -> formula)
-> v
-> v
-> formula
-> formula
-> formula
pullq (Bool
False, Bool
True)  formula
fm TVarOf (TermOf (AtomOf formula)) -> formula -> formula
VarOf formula -> formula -> formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(.&.) TVarOf (TermOf (AtomOf formula))
vr TVarOf (TermOf (AtomOf formula))
vr formula
l  formula
r'
            (Just (Quant
(:!:), TVarOf (TermOf (AtomOf formula))
vl, formula
l'), BinOp
(:|:), Maybe (Quant, TVarOf (TermOf (AtomOf formula)), formula)
_)                    -> (Bool, Bool)
-> formula
-> (TVarOf (TermOf (AtomOf formula)) -> formula -> formula)
-> (formula -> formula -> formula)
-> TVarOf (TermOf (AtomOf formula))
-> TVarOf (TermOf (AtomOf formula))
-> formula
-> formula
-> formula
forall formula v.
(IsFirstOrder formula, v ~ VarOf formula) =>
(Bool, Bool)
-> formula
-> (v -> formula -> formula)
-> (formula -> formula -> formula)
-> v
-> v
-> formula
-> formula
-> formula
pullq (Bool
True,  Bool
False) formula
fm TVarOf (TermOf (AtomOf formula)) -> formula -> formula
VarOf formula -> formula -> formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(.|.) TVarOf (TermOf (AtomOf formula))
vl TVarOf (TermOf (AtomOf formula))
vl formula
l' formula
r
            (Maybe (Quant, TVarOf (TermOf (AtomOf formula)), formula)
_,                    BinOp
(:|:), Just (Quant
(:!:), TVarOf (TermOf (AtomOf formula))
vr, formula
r')) -> (Bool, Bool)
-> formula
-> (TVarOf (TermOf (AtomOf formula)) -> formula -> formula)
-> (formula -> formula -> formula)
-> TVarOf (TermOf (AtomOf formula))
-> TVarOf (TermOf (AtomOf formula))
-> formula
-> formula
-> formula
forall formula v.
(IsFirstOrder formula, v ~ VarOf formula) =>
(Bool, Bool)
-> formula
-> (v -> formula -> formula)
-> (formula -> formula -> formula)
-> v
-> v
-> formula
-> formula
-> formula
pullq (Bool
False, Bool
True)  formula
fm TVarOf (TermOf (AtomOf formula)) -> formula -> formula
VarOf formula -> formula -> formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(.|.) TVarOf (TermOf (AtomOf formula))
vr TVarOf (TermOf (AtomOf formula))
vr formula
l  formula
r'
            (Just (Quant
(:?:), TVarOf (TermOf (AtomOf formula))
vl, formula
l'), BinOp
(:&:), Maybe (Quant, TVarOf (TermOf (AtomOf formula)), formula)
_)                    -> (Bool, Bool)
-> formula
-> (TVarOf (TermOf (AtomOf formula)) -> formula -> formula)
-> (formula -> formula -> formula)
-> TVarOf (TermOf (AtomOf formula))
-> TVarOf (TermOf (AtomOf formula))
-> formula
-> formula
-> formula
forall formula v.
(IsFirstOrder formula, v ~ VarOf formula) =>
(Bool, Bool)
-> formula
-> (v -> formula -> formula)
-> (formula -> formula -> formula)
-> v
-> v
-> formula
-> formula
-> formula
pullq (Bool
True,  Bool
False) formula
fm TVarOf (TermOf (AtomOf formula)) -> formula -> formula
VarOf formula -> formula -> formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists  formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(.&.) TVarOf (TermOf (AtomOf formula))
vl TVarOf (TermOf (AtomOf formula))
vl formula
l' formula
r
            (Maybe (Quant, TVarOf (TermOf (AtomOf formula)), formula)
_,                    BinOp
(:&:), Just (Quant
(:?:), TVarOf (TermOf (AtomOf formula))
vr, formula
r')) -> (Bool, Bool)
-> formula
-> (TVarOf (TermOf (AtomOf formula)) -> formula -> formula)
-> (formula -> formula -> formula)
-> TVarOf (TermOf (AtomOf formula))
-> TVarOf (TermOf (AtomOf formula))
-> formula
-> formula
-> formula
forall formula v.
(IsFirstOrder formula, v ~ VarOf formula) =>
(Bool, Bool)
-> formula
-> (v -> formula -> formula)
-> (formula -> formula -> formula)
-> v
-> v
-> formula
-> formula
-> formula
pullq (Bool
False, Bool
True)  formula
fm TVarOf (TermOf (AtomOf formula)) -> formula -> formula
VarOf formula -> formula -> formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists  formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(.&.) TVarOf (TermOf (AtomOf formula))
vr TVarOf (TermOf (AtomOf formula))
vr formula
l  formula
r'
            (Just (Quant
(:?:), TVarOf (TermOf (AtomOf formula))
vl, formula
l'), BinOp
(:|:), Maybe (Quant, TVarOf (TermOf (AtomOf formula)), formula)
_)                    -> (Bool, Bool)
-> formula
-> (TVarOf (TermOf (AtomOf formula)) -> formula -> formula)
-> (formula -> formula -> formula)
-> TVarOf (TermOf (AtomOf formula))
-> TVarOf (TermOf (AtomOf formula))
-> formula
-> formula
-> formula
forall formula v.
(IsFirstOrder formula, v ~ VarOf formula) =>
(Bool, Bool)
-> formula
-> (v -> formula -> formula)
-> (formula -> formula -> formula)
-> v
-> v
-> formula
-> formula
-> formula
pullq (Bool
True,  Bool
False) formula
fm TVarOf (TermOf (AtomOf formula)) -> formula -> formula
VarOf formula -> formula -> formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists  formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(.|.) TVarOf (TermOf (AtomOf formula))
vl TVarOf (TermOf (AtomOf formula))
vl formula
l' formula
r
            (Maybe (Quant, TVarOf (TermOf (AtomOf formula)), formula)
_,                    BinOp
(:|:), Just (Quant
(:?:), TVarOf (TermOf (AtomOf formula))
vr, formula
r')) -> (Bool, Bool)
-> formula
-> (TVarOf (TermOf (AtomOf formula)) -> formula -> formula)
-> (formula -> formula -> formula)
-> TVarOf (TermOf (AtomOf formula))
-> TVarOf (TermOf (AtomOf formula))
-> formula
-> formula
-> formula
forall formula v.
(IsFirstOrder formula, v ~ VarOf formula) =>
(Bool, Bool)
-> formula
-> (v -> formula -> formula)
-> (formula -> formula -> formula)
-> v
-> v
-> formula
-> formula
-> formula
pullq (Bool
False, Bool
True)  formula
fm TVarOf (TermOf (AtomOf formula)) -> formula -> formula
VarOf formula -> formula -> formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists  formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(.|.) TVarOf (TermOf (AtomOf formula))
vr TVarOf (TermOf (AtomOf formula))
vr formula
l  formula
r'
            (Maybe (Quant, TVarOf (TermOf (AtomOf formula)), formula), BinOp,
 Maybe (Quant, TVarOf (TermOf (AtomOf formula)), formula))
_                                                   -> formula
fm
      getQuant :: formula -> Maybe (Quant, VarOf formula, formula)
getQuant = (Quant
 -> VarOf formula
 -> formula
 -> Maybe (Quant, VarOf formula, formula))
-> (formula
    -> BinOp -> formula -> Maybe (Quant, VarOf formula, formula))
-> (formula -> Maybe (Quant, VarOf formula, formula))
-> (Bool -> Maybe (Quant, VarOf formula, formula))
-> (AtomOf formula -> Maybe (Quant, VarOf formula, formula))
-> formula
-> Maybe (Quant, VarOf formula, formula)
forall formula r.
IsQuantified formula =>
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
forall r.
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
foldQuantified (\ Quant
op VarOf formula
v formula
f -> (Quant, VarOf formula, formula)
-> Maybe (Quant, VarOf formula, formula)
forall a. a -> Maybe a
Just (Quant
op, VarOf formula
v, formula
f)) (\ formula
_ BinOp
_ formula
_ -> Maybe (Quant, VarOf formula, formula)
forall a. Maybe a
Nothing) (\ formula
_ -> Maybe (Quant, VarOf formula, formula)
forall a. Maybe a
Nothing) (\ Bool
_ -> Maybe (Quant, VarOf formula, formula)
forall a. Maybe a
Nothing) (\ AtomOf formula
_ -> Maybe (Quant, VarOf formula, formula)
forall a. Maybe a
Nothing)

pullq :: (IsFirstOrder formula, v ~ VarOf formula) =>
         (Bool, Bool)
      -> formula
      -> (v -> formula -> formula)
      -> (formula -> formula -> formula)
      -> v
      -> v
      -> formula
      -> formula
      -> formula
pullq :: forall formula v.
(IsFirstOrder formula, v ~ VarOf formula) =>
(Bool, Bool)
-> formula
-> (v -> formula -> formula)
-> (formula -> formula -> formula)
-> v
-> v
-> formula
-> formula
-> formula
pullq (Bool
l,Bool
r) formula
fm v -> formula -> formula
qu formula -> formula -> formula
op v
x v
y formula
p formula
q =
  let z :: v
z = v -> Set v -> v
forall v. IsVariable v => v -> Set v -> v
variant v
x (formula -> Set v
forall formula v.
(IsFirstOrder formula, v ~ VarOf formula) =>
formula -> Set v
fv formula
fm) in
  let p' :: formula
p' = if Bool
l then Map v (TermOf (AtomOf formula)) -> formula -> formula
forall formula term v.
(IsFirstOrder formula, term ~ TermOf (AtomOf formula),
 v ~ VarOf formula) =>
Map v term -> formula -> formula
subst (v -> TermOf (AtomOf formula) -> Map v (TermOf (AtomOf formula))
forall k a. k -> a -> Map k a
Map.singleton v
x (TVarOf (TermOf (AtomOf formula)) -> TermOf (AtomOf formula)
forall term. IsTerm term => TVarOf term -> term
vt v
TVarOf (TermOf (AtomOf formula))
z)) formula
p else formula
p
      q' :: formula
q' = if Bool
r then Map v (TermOf (AtomOf formula)) -> formula -> formula
forall formula term v.
(IsFirstOrder formula, term ~ TermOf (AtomOf formula),
 v ~ VarOf formula) =>
Map v term -> formula -> formula
subst (v -> TermOf (AtomOf formula) -> Map v (TermOf (AtomOf formula))
forall k a. k -> a -> Map k a
Map.singleton v
y (TVarOf (TermOf (AtomOf formula)) -> TermOf (AtomOf formula)
forall term. IsTerm term => TVarOf term -> term
vt v
TVarOf (TermOf (AtomOf formula))
z)) formula
q else formula
q in
  v -> formula -> formula
qu v
z (formula -> formula
forall formula. IsFirstOrder formula => formula -> formula
pullquants (formula -> formula -> formula
op formula
p' formula
q'))

-- Example.

test03 :: Test
test03 :: Test
test03 = 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
"pnf (p. 144)" (Formula -> String
forall a. Pretty a => a -> String
prettyShow Formula
expected) (Formula -> String
forall a. Pretty a => a -> String
prettyShow Formula
input)
    where p :: Predicate
p = Predicate
"P"
          q :: Predicate
q = Predicate
"Q"
          r :: Predicate
r = Predicate
"R"
          input :: Formula
input = Formula -> Formula
forall formula. IsFirstOrder formula => formula -> formula
pnf Formula
fm
          expected :: Formula
expected = VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists V
VarOf Formula
"x" (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"z"
                                 (((Formula -> Formula
forall formula. IsLiteral formula => formula -> formula
(.~.)(PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
p [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"x"])) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (Formula -> Formula
forall formula. IsLiteral formula => formula -> formula
(.~.)(PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
r [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"y"]))) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                                  ((PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
q [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"x"]) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                                   ((Formula -> Formula
forall formula. IsLiteral formula => formula -> formula
(.~.)(PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
p [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"z"])) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                                    (Formula -> Formula
forall formula. IsLiteral formula => formula -> formula
(.~.)(PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
q [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"z"])))))) :: Formula
          fm :: Formula
          fm :: Formula
fm = (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"x" (PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
p [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"x"]) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. (PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
r [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"y"])) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>.
               VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists V
VarOf Formula
"y" (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists V
VarOf Formula
"z" ((PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
q [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"y"]) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. (Formula -> Formula
forall formula. IsLiteral formula => formula -> formula
(.~.)(VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists V
VarOf Formula
"z" (PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
p [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"z"] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
q [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"z"])))))

-- | Extract the skolem functions from a formula.
skolems :: (IsFormula formula, HasSkolem function, HasApply atom, Ord function,
            atom ~ AtomOf formula,
            term ~ TermOf atom,
            function ~ FunOf term {-,
            v ~ TVarOf term,
            v ~ SVarOf function-}) => formula -> Set function
skolems :: forall formula function atom term.
(IsFormula formula, HasSkolem function, HasApply atom,
 Ord function, atom ~ AtomOf formula, term ~ TermOf atom,
 function ~ FunOf term) =>
formula -> Set function
skolems = (function -> Bool) -> Set function -> Set function
forall a. (a -> Bool) -> Set a -> Set a
Set.filter ((function -> Bool)
-> (SVarOf function -> Int -> Bool) -> function -> Bool
forall function r.
HasSkolem function =>
(function -> r) -> (SVarOf function -> Int -> r) -> function -> r
forall r.
(function -> r) -> (SVarOf function -> Int -> r) -> function -> r
foldSkolem (Bool -> function -> Bool
forall a b. a -> b -> a
const Bool
False) (\SVarOf function
_ Int
_ -> Bool
True)) (Set function -> Set function)
-> (formula -> Set function) -> formula -> Set function
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((function, Int) -> function)
-> Set (function, Int) -> Set function
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (function, Int) -> function
forall a b. (a, b) -> a
fst (Set (function, Int) -> Set function)
-> (formula -> Set (function, Int)) -> formula -> Set function
forall b c a. (b -> c) -> (a -> b) -> a -> c
. formula -> Set (function, Int)
forall formula atom function term.
(IsFormula formula, HasApply atom, Ord function,
 atom ~ AtomOf formula, term ~ TermOf atom,
 function ~ FunOf term) =>
formula -> Set (function, Int)
functions

-- | Core Skolemization function.
--
-- Skolemize the formula by removing the existential quantifiers and
-- replacing the variables they quantify with skolem functions (and
-- constants, which are functions of zero variables.)  The Skolem
-- functions are new functions (obtained from the SkolemT monad) which
-- are applied to the list of variables which are universally
-- quantified in the context where the existential quantifier
-- appeared.
skolem :: (IsFirstOrder formula, HasSkolem function, Monad m,
           atom ~ AtomOf formula,
           term ~ TermOf atom,
           function ~ FunOf term,
           VarOf formula ~ SVarOf function {-,
           predicate ~ PredOf atom-}) =>
          formula -> SkolemT m function formula
skolem :: forall formula function (m :: * -> *) atom term.
(IsFirstOrder formula, HasSkolem function, Monad m,
 atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
 VarOf formula ~ SVarOf function) =>
formula -> SkolemT m function formula
skolem formula
fm =
    (Quant -> VarOf formula -> formula -> SkolemT m function formula)
-> (formula -> BinOp -> formula -> SkolemT m function formula)
-> (formula -> SkolemT m function formula)
-> (Bool -> SkolemT m function formula)
-> (AtomOf formula -> SkolemT m function formula)
-> formula
-> SkolemT m function formula
forall formula r.
IsQuantified formula =>
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
forall r.
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
foldQuantified Quant -> TVarOf term -> formula -> SkolemT m function formula
Quant -> VarOf formula -> formula -> SkolemT m function formula
qu formula -> BinOp -> formula -> SkolemT m function formula
co formula -> SkolemT m function formula
ne Bool -> SkolemT m function formula
forall {m :: * -> *} {a}. (Monad m, IsFormula a) => Bool -> m a
tf (formula -> SkolemT m function formula
forall a. a -> StateT (SkolemState function) m a
forall (m :: * -> *) a. Monad m => a -> m a
return (formula -> SkolemT m function formula)
-> (atom -> formula) -> atom -> SkolemT m function formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. atom -> formula
AtomOf formula -> formula
forall formula. IsFormula formula => AtomOf formula -> formula
atomic) formula
fm
    where
      qu :: Quant -> TVarOf term -> formula -> SkolemT m function formula
qu Quant
(:?:) TVarOf term
y formula
p =
          do function
sk <- TVarOf term -> SkolemT m function function
forall (m :: * -> *) function v.
(Monad m, HasSkolem function, v ~ SVarOf function) =>
v -> SkolemT m function function
newSkolem TVarOf term
y
             let xs :: Set (TVarOf term)
xs = formula -> Set (TVarOf term)
forall formula v.
(IsFirstOrder formula, v ~ VarOf formula) =>
formula -> Set v
fv formula
fm
             let fx :: term
fx = FunOf term -> [term] -> term
forall term. IsTerm term => FunOf term -> [term] -> term
fApp function
FunOf term
sk ((TVarOf term -> term) -> [TVarOf term] -> [term]
forall a b. (a -> b) -> [a] -> [b]
List.map TVarOf term -> term
forall term. IsTerm term => TVarOf term -> term
vt (Set (TVarOf term) -> [TVarOf term]
forall a. Set a -> [a]
Set.toAscList Set (TVarOf term)
xs))
             formula -> SkolemT m function formula
forall formula function (m :: * -> *) atom term.
(IsFirstOrder formula, HasSkolem function, Monad m,
 atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
 VarOf formula ~ SVarOf function) =>
formula -> SkolemT m function formula
skolem (Map (TVarOf term) term -> formula -> formula
forall formula term v.
(IsFirstOrder formula, term ~ TermOf (AtomOf formula),
 v ~ VarOf formula) =>
Map v term -> formula -> formula
subst (TVarOf term -> term -> Map (TVarOf term) term
forall k a. k -> a -> Map k a
Map.singleton TVarOf term
y term
fx) formula
p)
      qu Quant
(:!:) TVarOf term
x formula
p = formula -> SkolemT m function formula
forall formula function (m :: * -> *) atom term.
(IsFirstOrder formula, HasSkolem function, Monad m,
 atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
 VarOf formula ~ SVarOf function) =>
formula -> SkolemT m function formula
skolem formula
p SkolemT m function formula
-> (formula -> SkolemT m function formula)
-> SkolemT m function formula
forall a b.
StateT (SkolemState function) m a
-> (a -> StateT (SkolemState function) m b)
-> StateT (SkolemState function) m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= formula -> SkolemT m function formula
forall a. a -> StateT (SkolemState function) m a
forall (m :: * -> *) a. Monad m => a -> m a
return (formula -> SkolemT m function formula)
-> (formula -> formula) -> formula -> SkolemT m function formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarOf formula -> formula -> formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all TVarOf term
VarOf formula
x
      co :: formula -> BinOp -> formula -> SkolemT m function formula
co formula
l BinOp
(:&:) formula
r = (formula -> formula -> formula)
-> formula -> formula -> SkolemT m function formula
forall formula function (m :: * -> *) atom term.
(IsFirstOrder formula, HasSkolem function, Monad m,
 atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
 VarOf formula ~ SVarOf function) =>
(formula -> formula -> formula)
-> formula -> formula -> SkolemT m function formula
skolem2 formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(.&.) formula
l formula
r
      co formula
l BinOp
(:|:) formula
r = (formula -> formula -> formula)
-> formula -> formula -> SkolemT m function formula
forall formula function (m :: * -> *) atom term.
(IsFirstOrder formula, HasSkolem function, Monad m,
 atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
 VarOf formula ~ SVarOf function) =>
(formula -> formula -> formula)
-> formula -> formula -> SkolemT m function formula
skolem2 formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
(.|.) formula
l formula
r
      co formula
_ BinOp
_ formula
_ = formula -> SkolemT m function formula
forall a. a -> StateT (SkolemState function) m a
forall (m :: * -> *) a. Monad m => a -> m a
return formula
fm
      ne :: formula -> SkolemT m function formula
ne formula
_ = formula -> SkolemT m function formula
forall a. a -> StateT (SkolemState function) m a
forall (m :: * -> *) a. Monad m => a -> m a
return formula
fm
      tf :: Bool -> m a
tf Bool
True = a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
forall formula. IsFormula formula => formula
true
      tf Bool
False = a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
forall formula. IsFormula formula => formula
false

newSkolem :: (Monad m, HasSkolem function, v ~ SVarOf function) => v -> SkolemT m function function
newSkolem :: forall (m :: * -> *) function v.
(Monad m, HasSkolem function, v ~ SVarOf function) =>
v -> SkolemT m function function
newSkolem v
v = do
  function
f <- function -> Set function -> function
forall function.
HasSkolem function =>
function -> Set function -> function
variantSkolem (SVarOf function -> Int -> function
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem v
SVarOf function
v Int
1) (Set function -> function)
-> (SkolemState function -> Set function)
-> SkolemState function
-> function
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SkolemState function -> Set function
forall function. SkolemState function -> Set function
skolemSet (SkolemState function -> function)
-> StateT (SkolemState function) m (SkolemState function)
-> SkolemT m function function
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT (SkolemState function) m (SkolemState function)
forall s (m :: * -> *). MonadState s m => m s
get
  (SkolemState function -> SkolemState function)
-> StateT (SkolemState function) m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\SkolemState function
s -> SkolemState function
s {skolemSet = Set.insert f (skolemSet s)})
  function -> SkolemT m function function
forall a. a -> StateT (SkolemState function) m a
forall (m :: * -> *) a. Monad m => a -> m a
return function
f

skolem2 :: (IsFirstOrder formula, HasSkolem function, Monad m,
            atom ~ AtomOf formula,
            term ~ TermOf atom,
            function ~ FunOf term,
            VarOf formula ~ SVarOf function) =>
           (formula -> formula -> formula) -> formula -> formula -> SkolemT m function formula
skolem2 :: forall formula function (m :: * -> *) atom term.
(IsFirstOrder formula, HasSkolem function, Monad m,
 atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
 VarOf formula ~ SVarOf function) =>
(formula -> formula -> formula)
-> formula -> formula -> SkolemT m function formula
skolem2 formula -> formula -> formula
cons formula
p formula
q =
    formula -> SkolemT m function formula
forall formula function (m :: * -> *) atom term.
(IsFirstOrder formula, HasSkolem function, Monad m,
 atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
 VarOf formula ~ SVarOf function) =>
formula -> SkolemT m function formula
skolem formula
p SkolemT m function formula
-> (formula -> SkolemT m function formula)
-> SkolemT m function formula
forall a b.
StateT (SkolemState function) m a
-> (a -> StateT (SkolemState function) m b)
-> StateT (SkolemState function) m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ formula
p' ->
    formula -> SkolemT m function formula
forall formula function (m :: * -> *) atom term.
(IsFirstOrder formula, HasSkolem function, Monad m,
 atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
 VarOf formula ~ SVarOf function) =>
formula -> SkolemT m function formula
skolem formula
q SkolemT m function formula
-> (formula -> SkolemT m function formula)
-> SkolemT m function formula
forall a b.
StateT (SkolemState function) m a
-> (a -> StateT (SkolemState function) m b)
-> StateT (SkolemState function) m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ formula
q' ->
    formula -> SkolemT m function formula
forall a. a -> StateT (SkolemState function) m a
forall (m :: * -> *) a. Monad m => a -> m a
return (formula -> formula -> formula
cons formula
p' formula
q')

-- | Overall Skolemization function.
askolemize :: (IsFirstOrder formula, HasSkolem function, Monad m,
               atom ~ AtomOf formula,
               term ~ TermOf atom,
               function ~ FunOf term,
               VarOf formula ~ SVarOf function) =>
              formula -> SkolemT m function formula
askolemize :: forall formula function (m :: * -> *) atom term.
(IsFirstOrder formula, HasSkolem function, Monad m,
 atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
 VarOf formula ~ SVarOf function) =>
formula -> SkolemT m function formula
askolemize = formula -> SkolemT m function formula
forall formula function (m :: * -> *) atom term.
(IsFirstOrder formula, HasSkolem function, Monad m,
 atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
 VarOf formula ~ SVarOf function) =>
formula -> SkolemT m function formula
skolem (formula -> SkolemT m function formula)
-> (formula -> formula) -> formula -> SkolemT m function formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. formula -> formula
forall formula. IsFirstOrder formula => formula -> formula
nnf (formula -> formula) -> (formula -> formula) -> formula -> formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. formula -> formula
forall formula. IsFirstOrder formula => formula -> formula
simplify

-- | Remove the leading universal quantifiers.  After a call to pnf
-- this will be all the universal quantifiers, and the skolemization
-- will have already turned all the existential quantifiers into
-- skolem functions.  For this reason we can safely convert to any
-- instance of IsPropositional.
specialize :: (IsQuantified fof, JustPropositional pf) => (AtomOf fof -> AtomOf pf) -> fof -> pf
specialize :: forall fof pf.
(IsQuantified fof, JustPropositional pf) =>
(AtomOf fof -> AtomOf pf) -> fof -> pf
specialize AtomOf fof -> AtomOf pf
ca fof
fm =
    (fof -> pf) -> (AtomOf fof -> AtomOf pf) -> fof -> pf
forall formula pf.
(IsPropositional formula, JustPropositional pf) =>
(formula -> pf) -> (AtomOf formula -> AtomOf pf) -> formula -> pf
convertToPropositional (String -> fof -> pf
forall a. HasCallStack => String -> a
error String
"specialize failure") AtomOf fof -> AtomOf pf
ca (fof -> fof
specialize' fof
fm)
    where
      specialize' :: fof -> fof
specialize' fof
p = (Quant -> VarOf fof -> fof -> fof)
-> (fof -> BinOp -> fof -> fof)
-> (fof -> fof)
-> (Bool -> fof)
-> (AtomOf fof -> fof)
-> fof
-> fof
forall formula r.
IsQuantified formula =>
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
forall r.
(Quant -> VarOf fof -> fof -> r)
-> (fof -> BinOp -> fof -> r)
-> (fof -> r)
-> (Bool -> r)
-> (AtomOf fof -> r)
-> fof
-> r
foldQuantified Quant -> VarOf fof -> fof -> fof
qu (\fof
_ BinOp
_ fof
_ -> fof
p) (\fof
_ -> fof
p) (\Bool
_ -> fof
p) (\AtomOf fof
_ -> fof
p) fof
p
      qu :: Quant -> VarOf fof -> fof -> fof
qu Quant
(:!:) VarOf fof
_ fof
p = fof -> fof
specialize' fof
p
      qu Quant
_ VarOf fof
_ fof
_ = fof
fm

-- | Skolemize and then specialize.  Because we know all quantifiers
-- are gone we can convert to any instance of IsPropositional.
skolemize :: (IsFirstOrder formula, JustPropositional pf, HasSkolem function, Monad m,
              atom ~ AtomOf formula,
              term ~ TermOf atom,
              function ~ FunOf term,
              VarOf formula ~ SVarOf function) =>
             (AtomOf formula -> AtomOf pf) -> formula -> StateT (SkolemState function) m pf
skolemize :: forall formula pf function (m :: * -> *) atom term.
(IsFirstOrder formula, JustPropositional pf, HasSkolem function,
 Monad m, atom ~ AtomOf formula, term ~ TermOf atom,
 function ~ FunOf term, VarOf formula ~ SVarOf function) =>
(AtomOf formula -> AtomOf pf)
-> formula -> StateT (SkolemState function) m pf
skolemize AtomOf formula -> AtomOf pf
ca formula
fm = ((AtomOf formula -> AtomOf pf) -> formula -> pf
forall fof pf.
(IsQuantified fof, JustPropositional pf) =>
(AtomOf fof -> AtomOf pf) -> fof -> pf
specialize AtomOf formula -> AtomOf pf
ca (formula -> pf) -> (formula -> formula) -> formula -> pf
forall b c a. (b -> c) -> (a -> b) -> a -> c
. formula -> formula
forall formula. IsFirstOrder formula => formula -> formula
pnf) (formula -> pf)
-> StateT (SkolemState function) m formula
-> StateT (SkolemState function) m pf
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> formula -> StateT (SkolemState function) m formula
forall formula function (m :: * -> *) atom term.
(IsFirstOrder formula, HasSkolem function, Monad m,
 atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
 VarOf formula ~ SVarOf function) =>
formula -> SkolemT m function formula
askolemize formula
fm

-- | A function type that is an instance of HasSkolem
data Function
    = Fn String
    | Skolem V Int
    deriving (Function -> Function -> Bool
(Function -> Function -> Bool)
-> (Function -> Function -> Bool) -> Eq Function
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Function -> Function -> Bool
== :: Function -> Function -> Bool
$c/= :: Function -> Function -> Bool
/= :: Function -> Function -> Bool
Eq, Eq Function
Eq Function =>
(Function -> Function -> Ordering)
-> (Function -> Function -> Bool)
-> (Function -> Function -> Bool)
-> (Function -> Function -> Bool)
-> (Function -> Function -> Bool)
-> (Function -> Function -> Function)
-> (Function -> Function -> Function)
-> Ord Function
Function -> Function -> Bool
Function -> Function -> Ordering
Function -> Function -> Function
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 :: Function -> Function -> Ordering
compare :: Function -> Function -> Ordering
$c< :: Function -> Function -> Bool
< :: Function -> Function -> Bool
$c<= :: Function -> Function -> Bool
<= :: Function -> Function -> Bool
$c> :: Function -> Function -> Bool
> :: Function -> Function -> Bool
$c>= :: Function -> Function -> Bool
>= :: Function -> Function -> Bool
$cmax :: Function -> Function -> Function
max :: Function -> Function -> Function
$cmin :: Function -> Function -> Function
min :: Function -> Function -> Function
Ord, Typeable Function
Typeable Function =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Function -> c Function)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Function)
-> (Function -> Constr)
-> (Function -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Function))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Function))
-> ((forall b. Data b => b -> b) -> Function -> Function)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Function -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Function -> r)
-> (forall u. (forall d. Data d => d -> u) -> Function -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Function -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Function -> m Function)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Function -> m Function)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Function -> m Function)
-> Data Function
Function -> Constr
Function -> DataType
(forall b. Data b => b -> b) -> Function -> Function
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) -> Function -> u
forall u. (forall d. Data d => d -> u) -> Function -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Function -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Function -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Function -> m Function
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Function -> m Function
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Function
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Function -> c Function
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Function)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Function)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Function -> c Function
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Function -> c Function
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Function
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Function
$ctoConstr :: Function -> Constr
toConstr :: Function -> Constr
$cdataTypeOf :: Function -> DataType
dataTypeOf :: Function -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Function)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Function)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Function)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Function)
$cgmapT :: (forall b. Data b => b -> b) -> Function -> Function
gmapT :: (forall b. Data b => b -> b) -> Function -> Function
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Function -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Function -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Function -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Function -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Function -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Function -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Function -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Function -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Function -> m Function
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Function -> m Function
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Function -> m Function
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Function -> m Function
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Function -> m Function
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Function -> m Function
Data, Typeable, ReadPrec [Function]
ReadPrec Function
Int -> ReadS Function
ReadS [Function]
(Int -> ReadS Function)
-> ReadS [Function]
-> ReadPrec Function
-> ReadPrec [Function]
-> Read Function
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS Function
readsPrec :: Int -> ReadS Function
$creadList :: ReadS [Function]
readList :: ReadS [Function]
$creadPrec :: ReadPrec Function
readPrec :: ReadPrec Function
$creadListPrec :: ReadPrec [Function]
readListPrec :: ReadPrec [Function]
Read)

instance IsFunction Function

instance IsString Function where
    fromString :: String -> Function
fromString = String -> Function
Fn

instance Show Function where
    show :: Function -> String
show = Function -> String
forall function.
(HasSkolem function, IsVariable (SVarOf function)) =>
function -> String
showSkolem

instance Pretty Function where
    pPrint :: Function -> Doc
pPrint = (Function -> Doc) -> Function -> Doc
forall function.
HasSkolem function =>
(function -> Doc) -> function -> Doc
prettySkolem (\(Fn String
s) -> String -> Doc
text String
s)

instance HasSkolem Function where
    type SVarOf Function = V
    toSkolem :: SVarOf Function -> Int -> Function
toSkolem = V -> Int -> Function
SVarOf Function -> Int -> Function
Skolem
    foldSkolem :: forall r.
(Function -> r) -> (SVarOf Function -> Int -> r) -> Function -> r
foldSkolem Function -> r
_ SVarOf Function -> Int -> r
sk (Skolem V
v Int
n) = SVarOf Function -> Int -> r
sk V
SVarOf Function
v Int
n
    foldSkolem Function -> r
other SVarOf Function -> Int -> r
_ Function
f = Function -> r
other Function
f
    variantSkolem :: Function -> Set Function -> Function
variantSkolem Function
f Set Function
fns | Function -> Set Function -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.notMember Function
f Set Function
fns = Function
f
    variantSkolem (Fn String
s) Set Function
fns = Function -> Set Function -> Function
forall function.
HasSkolem function =>
function -> Set function -> function
variantSkolem (String -> Function
forall a. IsString a => String -> a
fromString (String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'")) Set Function
fns
    variantSkolem (Skolem V
v Int
n) Set Function
fns = Function -> Set Function -> Function
forall function.
HasSkolem function =>
function -> Set function -> function
variantSkolem (V -> Int -> Function
Skolem V
v (Int -> Int
forall a. Enum a => a -> a
succ Int
n)) Set Function
fns

-- | A first order logic formula type with an equality predicate and skolem functions.
type Formula = QFormula V SkAtom
type SkAtom = FOL Predicate SkTerm
type SkTerm = Term Function V

instance IsFirstOrder Formula

test04 :: Test
test04 :: Test
test04 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String
-> PFormula (FOL Predicate SkTerm)
-> PFormula (FOL Predicate SkTerm)
-> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"skolemize 1 (p. 150)" PFormula (FOL Predicate SkTerm)
expected PFormula (FOL Predicate SkTerm)
input
    where input :: PFormula (FOL Predicate SkTerm)
input = SkolemT Identity Function (PFormula (FOL Predicate SkTerm))
-> PFormula (FOL Predicate SkTerm)
forall function a.
IsFunction function =>
SkolemT Identity function a -> a
runSkolem ((AtomOf Formula -> AtomOf (PFormula (FOL Predicate SkTerm)))
-> Formula
-> SkolemT Identity Function (PFormula (FOL Predicate SkTerm))
forall formula pf function (m :: * -> *) atom term.
(IsFirstOrder formula, JustPropositional pf, HasSkolem function,
 Monad m, atom ~ AtomOf formula, term ~ TermOf atom,
 function ~ FunOf term, VarOf formula ~ SVarOf function) =>
(AtomOf formula -> AtomOf pf)
-> formula -> StateT (SkolemState function) m pf
skolemize AtomOf Formula -> AtomOf (PFormula (FOL Predicate SkTerm))
FOL Predicate SkTerm -> FOL Predicate SkTerm
forall a. a -> a
id Formula
fm) :: PFormula SkAtom
          fm :: Formula
          fm :: Formula
fm = VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists V
VarOf Formula
"y" (PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp (Predicate
PredOf (FOL Predicate SkTerm)
"<") [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"x", TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"y"] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>.
                           VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"u" (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists V
VarOf Formula
"v" (PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp (Predicate
PredOf (FOL Predicate SkTerm)
"<") [FunOf SkTerm -> [SkTerm] -> SkTerm
forall term. IsTerm term => FunOf term -> [term] -> term
fApp FunOf SkTerm
Function
"*" [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"x", TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"u"],  FunOf SkTerm -> [SkTerm] -> SkTerm
forall term. IsTerm term => FunOf term -> [term] -> term
fApp FunOf SkTerm
Function
"*" [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"y", TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"v"]])))
          expected :: PFormula (FOL Predicate SkTerm)
expected = (PFormula (FOL Predicate SkTerm) -> PFormula (FOL Predicate SkTerm)
forall formula. IsLiteral formula => formula -> formula
(.~.)(PredOf (AtomOf (PFormula (FOL Predicate SkTerm)))
-> [TermOf (AtomOf (PFormula (FOL Predicate SkTerm)))]
-> PFormula (FOL Predicate SkTerm)
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp (PredOf (AtomOf (PFormula (FOL Predicate SkTerm)))
"<") [TVarOf (TermOf (AtomOf (PFormula (FOL Predicate SkTerm))))
-> TermOf (AtomOf (PFormula (FOL Predicate SkTerm)))
forall term. IsTerm term => TVarOf term -> term
vt TVarOf (TermOf (AtomOf (PFormula (FOL Predicate SkTerm))))
"x",FunOf (TermOf (AtomOf (PFormula (FOL Predicate SkTerm))))
-> [TermOf (AtomOf (PFormula (FOL Predicate SkTerm)))]
-> TermOf (AtomOf (PFormula (FOL Predicate SkTerm)))
forall term. IsTerm term => FunOf term -> [term] -> term
fApp (V -> Int -> Function
Skolem V
"y" Int
1) [TVarOf (TermOf (AtomOf (PFormula (FOL Predicate SkTerm))))
-> TermOf (AtomOf (PFormula (FOL Predicate SkTerm)))
forall term. IsTerm term => TVarOf term -> term
vt TVarOf (TermOf (AtomOf (PFormula (FOL Predicate SkTerm))))
"x"]])) PFormula (FOL Predicate SkTerm)
-> PFormula (FOL Predicate SkTerm)
-> PFormula (FOL Predicate SkTerm)
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                     (PredOf (AtomOf (PFormula (FOL Predicate SkTerm)))
-> [TermOf (AtomOf (PFormula (FOL Predicate SkTerm)))]
-> PFormula (FOL Predicate SkTerm)
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp (PredOf (AtomOf (PFormula (FOL Predicate SkTerm)))
"<") [FunOf (TermOf (AtomOf (PFormula (FOL Predicate SkTerm))))
-> [TermOf (AtomOf (PFormula (FOL Predicate SkTerm)))]
-> TermOf (AtomOf (PFormula (FOL Predicate SkTerm)))
forall term. IsTerm term => FunOf term -> [term] -> term
fApp FunOf (TermOf (AtomOf (PFormula (FOL Predicate SkTerm))))
Function
"*" [TVarOf (TermOf (AtomOf (PFormula (FOL Predicate SkTerm))))
-> TermOf (AtomOf (PFormula (FOL Predicate SkTerm)))
forall term. IsTerm term => TVarOf term -> term
vt TVarOf (TermOf (AtomOf (PFormula (FOL Predicate SkTerm))))
"x",TVarOf (TermOf (AtomOf (PFormula (FOL Predicate SkTerm))))
-> TermOf (AtomOf (PFormula (FOL Predicate SkTerm)))
forall term. IsTerm term => TVarOf term -> term
vt TVarOf (TermOf (AtomOf (PFormula (FOL Predicate SkTerm))))
"u"],FunOf (TermOf (AtomOf (PFormula (FOL Predicate SkTerm))))
-> [TermOf (AtomOf (PFormula (FOL Predicate SkTerm)))]
-> TermOf (AtomOf (PFormula (FOL Predicate SkTerm)))
forall term. IsTerm term => FunOf term -> [term] -> term
fApp FunOf (TermOf (AtomOf (PFormula (FOL Predicate SkTerm))))
Function
"*" [FunOf (TermOf (AtomOf (PFormula (FOL Predicate SkTerm))))
-> [TermOf (AtomOf (PFormula (FOL Predicate SkTerm)))]
-> TermOf (AtomOf (PFormula (FOL Predicate SkTerm)))
forall term. IsTerm term => FunOf term -> [term] -> term
fApp (V -> Int -> Function
Skolem V
"y" Int
1) [TVarOf (TermOf (AtomOf (PFormula (FOL Predicate SkTerm))))
-> TermOf (AtomOf (PFormula (FOL Predicate SkTerm)))
forall term. IsTerm term => TVarOf term -> term
vt TVarOf (TermOf (AtomOf (PFormula (FOL Predicate SkTerm))))
"x"],FunOf (TermOf (AtomOf (PFormula (FOL Predicate SkTerm))))
-> [TermOf (AtomOf (PFormula (FOL Predicate SkTerm)))]
-> TermOf (AtomOf (PFormula (FOL Predicate SkTerm)))
forall term. IsTerm term => FunOf term -> [term] -> term
fApp (V -> Int -> Function
Skolem V
"v" Int
1) [TVarOf (TermOf (AtomOf (PFormula (FOL Predicate SkTerm))))
-> TermOf (AtomOf (PFormula (FOL Predicate SkTerm)))
forall term. IsTerm term => TVarOf term -> term
vt TVarOf (TermOf (AtomOf (PFormula (FOL Predicate SkTerm))))
"u",TVarOf (TermOf (AtomOf (PFormula (FOL Predicate SkTerm))))
-> TermOf (AtomOf (PFormula (FOL Predicate SkTerm)))
forall term. IsTerm term => TVarOf term -> term
vt TVarOf (TermOf (AtomOf (PFormula (FOL Predicate SkTerm))))
"x"]]])

test05 :: Test
test05 :: Test
test05 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String
-> PFormula (FOL Predicate SkTerm)
-> PFormula (FOL Predicate SkTerm)
-> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"skolemize 2 (p. 150)" PFormula (FOL Predicate SkTerm)
expected PFormula (FOL Predicate SkTerm)
input
    where p :: Predicate
p = Predicate
"P"
          q :: Predicate
q = Predicate
"Q"
          input :: PFormula (FOL Predicate SkTerm)
input = SkolemT Identity Function (PFormula (FOL Predicate SkTerm))
-> PFormula (FOL Predicate SkTerm)
forall function a.
IsFunction function =>
SkolemT Identity function a -> a
runSkolem ((AtomOf Formula -> AtomOf (PFormula (FOL Predicate SkTerm)))
-> Formula
-> SkolemT Identity Function (PFormula (FOL Predicate SkTerm))
forall formula pf function (m :: * -> *) atom term.
(IsFirstOrder formula, JustPropositional pf, HasSkolem function,
 Monad m, atom ~ AtomOf formula, term ~ TermOf atom,
 function ~ FunOf term, VarOf formula ~ SVarOf function) =>
(AtomOf formula -> AtomOf pf)
-> formula -> StateT (SkolemState function) m pf
skolemize AtomOf Formula -> AtomOf (PFormula (FOL Predicate SkTerm))
FOL Predicate SkTerm -> FOL Predicate SkTerm
forall a. a -> a
id Formula
fm) :: PFormula SkAtom
          fm :: Formula
          fm :: Formula
fm = VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"x" ((PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
p [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"x"]) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>.
                            (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists V
VarOf Formula
"y" (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists V
VarOf Formula
"z" ((PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
q [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"y"]) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                                                     (Formula -> Formula
forall formula. IsLiteral formula => formula -> formula
(.~.)(VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists V
VarOf Formula
"z" ((PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
p [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"z"]) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
q [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"z"]))))))))
          expected :: PFormula (FOL Predicate SkTerm)
expected = (PFormula (FOL Predicate SkTerm) -> PFormula (FOL Predicate SkTerm)
forall formula. IsLiteral formula => formula -> formula
(.~.)(PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)]
-> PFormula (FOL Predicate SkTerm)
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
p [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"x"])) PFormula (FOL Predicate SkTerm)
-> PFormula (FOL Predicate SkTerm)
-> PFormula (FOL Predicate SkTerm)
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                     ((PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)]
-> PFormula (FOL Predicate SkTerm)
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
q [FunOf SkTerm -> [SkTerm] -> SkTerm
forall term. IsTerm term => FunOf term -> [term] -> term
fApp (V -> Int -> Function
Skolem V
"y" Int
1) []]) PFormula (FOL Predicate SkTerm)
-> PFormula (FOL Predicate SkTerm)
-> PFormula (FOL Predicate SkTerm)
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                      ((PFormula (FOL Predicate SkTerm) -> PFormula (FOL Predicate SkTerm)
forall formula. IsLiteral formula => formula -> formula
(.~.)(PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)]
-> PFormula (FOL Predicate SkTerm)
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
p [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"z"])) PFormula (FOL Predicate SkTerm)
-> PFormula (FOL Predicate SkTerm)
-> PFormula (FOL Predicate SkTerm)
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                       (PFormula (FOL Predicate SkTerm) -> PFormula (FOL Predicate SkTerm)
forall formula. IsLiteral formula => formula -> formula
(.~.)(PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)]
-> PFormula (FOL Predicate SkTerm)
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
q [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"z"]))))

-- | Versions of the normal form functions that leave quantifiers in place.
simpdnf' :: (IsFirstOrder fof, Ord fof,
             atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term,
             v ~ VarOf fof, v ~ TVarOf term) =>
            fof -> Set (Set fof)
simpdnf' :: forall fof atom term function v.
(IsFirstOrder fof, Ord fof, atom ~ AtomOf fof, term ~ TermOf atom,
 function ~ FunOf term, v ~ VarOf fof, v ~ TVarOf term) =>
fof -> Set (Set fof)
simpdnf' fof
fm =
    (Quant -> VarOf fof -> fof -> Set (Set fof))
-> (fof -> BinOp -> fof -> Set (Set fof))
-> (fof -> Set (Set fof))
-> (Bool -> Set (Set fof))
-> (AtomOf fof -> Set (Set fof))
-> fof
-> Set (Set fof)
forall formula r.
IsQuantified formula =>
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
forall r.
(Quant -> VarOf fof -> fof -> r)
-> (fof -> BinOp -> fof -> r)
-> (fof -> r)
-> (Bool -> r)
-> (AtomOf fof -> r)
-> fof
-> r
foldQuantified (\Quant
_ VarOf fof
_ fof
_ -> Set (Set fof)
go) (\fof
_ BinOp
_ fof
_ -> Set (Set fof)
go) (\fof
_ -> Set (Set fof)
go) Bool -> Set (Set fof)
forall {a}. Bool -> Set (Set a)
tf (\AtomOf fof
_ -> Set (Set fof)
go) fof
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
Set.singleton Set a
forall a. Set a
Set.empty
      go :: Set (Set fof)
go = let djs :: Set (Set fof)
djs = (Set fof -> Bool) -> Set (Set fof) -> Set (Set fof)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Bool -> Bool
not (Bool -> Bool) -> (Set fof -> Bool) -> Set fof -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set fof -> Bool
forall lit. (Ord lit, IsLiteral lit) => Set lit -> Bool
trivial) (fof -> Set (Set fof)
forall fof. (IsQuantified fof, Ord fof) => fof -> Set (Set fof)
purednf' (fof -> fof
forall formula. IsFirstOrder formula => formula -> formula
nnf fof
fm)) in
           (Set fof -> Bool) -> Set (Set fof) -> Set (Set fof)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\Set fof
d -> Bool -> Bool
not ((Set fof -> Bool) -> Set (Set fof) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
setAny (\Set fof
d' -> Set fof -> Set fof -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isProperSubsetOf Set fof
d' Set fof
d) Set (Set fof)
djs)) Set (Set fof)
djs

purednf' :: (IsQuantified fof, Ord fof) => fof -> Set (Set fof)
purednf' :: forall fof. (IsQuantified fof, Ord fof) => fof -> Set (Set fof)
purednf' fof
fm =
    {-t4 $-}
    (fof -> Set (Set fof))
-> (fof -> BinOp -> fof -> Set (Set fof))
-> (fof -> Set (Set fof))
-> (Bool -> Set (Set fof))
-> (AtomOf fof -> Set (Set fof))
-> fof
-> Set (Set fof)
forall formula r.
IsPropositional formula =>
(formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
forall r.
(fof -> r)
-> (fof -> BinOp -> fof -> r)
-> (fof -> r)
-> (Bool -> r)
-> (AtomOf fof -> r)
-> fof
-> r
foldPropositional' fof -> Set (Set fof)
ho fof -> BinOp -> fof -> Set (Set fof)
co (\fof
_ -> fof -> Set (Set fof)
forall {a}. a -> Set (Set a)
lf fof
fm) (\Bool
_ -> fof -> Set (Set fof)
forall {a}. a -> Set (Set a)
lf fof
fm) (\AtomOf fof
_ -> fof -> Set (Set fof)
forall {a}. a -> Set (Set a)
lf fof
fm) ({-t3-} fof
fm)
    where
      lf :: a -> Set (Set a)
lf = Set a -> Set (Set a)
forall a. a -> Set a
Set.singleton (Set a -> Set (Set a)) -> (a -> Set a) -> a -> Set (Set a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Set a
forall a. a -> Set a
Set.singleton
      ho :: fof -> Set (Set fof)
ho fof
_ = fof -> Set (Set fof)
forall {a}. a -> Set (Set a)
lf fof
fm
      co :: fof -> BinOp -> fof -> Set (Set fof)
co fof
p BinOp
(:&:) fof
q = Set (Set fof) -> Set (Set fof) -> Set (Set fof)
forall a. Ord a => Set (Set a) -> Set (Set a) -> Set (Set a)
distrib (fof -> Set (Set fof)
forall fof. (IsQuantified fof, Ord fof) => fof -> Set (Set fof)
purednf' fof
p) (fof -> Set (Set fof)
forall fof. (IsQuantified fof, Ord fof) => fof -> Set (Set fof)
purednf' fof
q)
      co fof
p BinOp
(:|:) fof
q = Set (Set fof) -> Set (Set fof) -> Set (Set fof)
forall a. Ord a => Set a -> Set a -> Set a
union (fof -> Set (Set fof)
forall fof. (IsQuantified fof, Ord fof) => fof -> Set (Set fof)
purednf' fof
p) (fof -> Set (Set fof)
forall fof. (IsQuantified fof, Ord fof) => fof -> Set (Set fof)
purednf' fof
q)
      co fof
_ BinOp
_ fof
_ = fof -> Set (Set fof)
forall {a}. a -> Set (Set a)
lf fof
fm
      -- t3 x = trace ("purednf' (" ++ prettyShow x) x
      -- t4 x = trace ("purednf' (" ++ prettyShow fm ++ ") -> " ++ prettyShow x) x

simpcnf' :: (atom ~ AtomOf fof, term ~ TermOf atom, predicate ~ PredOf atom, v ~ VarOf fof, v ~ TVarOf term, function ~ FunOf term,
             IsFirstOrder fof, Ord fof) => fof -> Set (Set fof)
simpcnf' :: forall atom fof term predicate v function.
(atom ~ AtomOf fof, term ~ TermOf atom, predicate ~ PredOf atom,
 v ~ VarOf fof, v ~ TVarOf term, function ~ FunOf term,
 IsFirstOrder fof, Ord fof) =>
fof -> Set (Set fof)
simpcnf' fof
fm =
    (Quant -> VarOf fof -> fof -> Set (Set fof))
-> (fof -> BinOp -> fof -> Set (Set fof))
-> (fof -> Set (Set fof))
-> (Bool -> Set (Set fof))
-> (AtomOf fof -> Set (Set fof))
-> fof
-> Set (Set fof)
forall formula r.
IsQuantified formula =>
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
forall r.
(Quant -> VarOf fof -> fof -> r)
-> (fof -> BinOp -> fof -> r)
-> (fof -> r)
-> (Bool -> r)
-> (AtomOf fof -> r)
-> fof
-> r
foldQuantified (\Quant
_ VarOf fof
_ fof
_ -> Set (Set fof)
go) (\fof
_ BinOp
_ fof
_ -> Set (Set fof)
go) (\fof
_ -> Set (Set fof)
go) Bool -> Set (Set fof)
forall {a}. Bool -> Set (Set a)
tf (\AtomOf fof
_ -> Set (Set fof)
go) fof
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
Set.singleton Set a
forall a. Set a
Set.empty
      go :: Set (Set fof)
go = let cjs :: Set (Set fof)
cjs = (Set fof -> Bool) -> Set (Set fof) -> Set (Set fof)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Bool -> Bool
not (Bool -> Bool) -> (Set fof -> Bool) -> Set fof -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set fof -> Bool
forall lit. (Ord lit, IsLiteral lit) => Set lit -> Bool
trivial) (fof -> Set (Set fof)
forall atom fof term predicate v function.
(atom ~ AtomOf fof, term ~ TermOf atom, predicate ~ PredOf atom,
 v ~ VarOf fof, v ~ TVarOf term, function ~ FunOf term,
 IsFirstOrder fof, Ord fof) =>
fof -> Set (Set fof)
purecnf' fof
fm) in
           (Set fof -> Bool) -> Set (Set fof) -> Set (Set fof)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\Set fof
c -> Bool -> Bool
not ((Set fof -> Bool) -> Set (Set fof) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
setAny (\Set fof
c' -> Set fof -> Set fof -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isProperSubsetOf Set fof
c' Set fof
c) Set (Set fof)
cjs)) Set (Set fof)
cjs

purecnf' :: (atom ~ AtomOf fof, term ~ TermOf atom, predicate ~ PredOf atom, v ~ VarOf fof, v ~ TVarOf term, function ~ FunOf term,
             IsFirstOrder fof, Ord fof) => fof -> Set (Set fof)
purecnf' :: forall atom fof term predicate v function.
(atom ~ AtomOf fof, term ~ TermOf atom, predicate ~ PredOf atom,
 v ~ VarOf fof, v ~ TVarOf term, function ~ FunOf term,
 IsFirstOrder fof, Ord fof) =>
fof -> Set (Set fof)
purecnf' fof
fm = (Set fof -> Set fof) -> Set (Set fof) -> Set (Set fof)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ((fof -> fof) -> Set fof -> Set fof
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map fof -> fof
forall formula. IsLiteral formula => formula -> formula
negate) (fof -> Set (Set fof)
forall fof. (IsQuantified fof, Ord fof) => fof -> Set (Set fof)
purednf' (fof -> fof
forall formula. IsFirstOrder formula => formula -> formula
nnf (fof -> fof
forall formula. IsLiteral formula => formula -> formula
(.~.) fof
fm)))

testSkolem :: Test
testSkolem :: Test
testSkolem = String -> Test -> Test
TestLabel String
"Skolem" ([Test] -> Test
TestList [Test
test01, Test
test02, Test
test03, Test
test04, Test
test05])