{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wall #-}
module Data.Logic.ATP.Resolution
( match_atoms
, match_atoms_eq
, resolution1
, resolution2
, resolution3
, presolution
, davis_putnam_example_formula
, testResolution
) where
import Control.Monad.State (execStateT, get, StateT)
import Data.List as List (map)
import Data.Logic.ATP.Apply (HasApply(TermOf), JustApply, pApp, zipApplys)
import Data.Logic.ATP.Equate (HasEquate, zipEquates)
import Data.Logic.ATP.FOL (generalize, IsFirstOrder, lsubst, var)
import Data.Logic.ATP.Formulas (IsFormula(AtomOf))
import Data.Logic.ATP.Lib (allpairs, allsubsets, allnonemptysubsets, apply, defined,
Failing(..), failing, (|->), setAll, setAny, settryfind)
import Data.Logic.ATP.Lit ((.~.), IsLiteral, JustLiteral, LFormula, positive, zipLiterals')
import Data.Logic.ATP.Pretty (assertEqual', Pretty, prettyShow)
import Data.Logic.ATP.Prop ((.|.), (.&.), (.=>.), (.<=>.), list_conj, PFormula, simpcnf, trivial)
import Data.Logic.ATP.Quantified (exists, for_all, IsQuantified(VarOf))
import Data.Logic.ATP.Parser (fof)
import Data.Logic.ATP.Skolem (askolemize, Formula, Function(Skolem), HasSkolem(SVarOf), pnf,
runSkolem, simpdnf', SkAtom, skolemize, SkolemT, specialize, SkTerm)
import Data.Logic.ATP.Term (fApp, foldTerm, IsTerm(FunOf, TVarOf), prefix, V, vt)
import Data.Logic.ATP.Unif (solve, Unify(UTermOf), unify_literals)
import Data.Map.Strict as Map
import Data.Maybe (fromMaybe)
import Data.Set as Set
import Data.String (fromString)
import Test.HUnit
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
"Barber's paradox: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Formula -> String
forall a. Pretty a => a -> String
prettyShow Formula
barb String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" (p. 181)")
(Set (Set Formula) -> String
forall a. Pretty a => a -> String
prettyShow Set (Set Formula)
expected)
(Set (Set (LFormula (FOL Predicate SkTerm))) -> String
forall a. Pretty a => a -> String
prettyShow Set (Set (LFormula (FOL Predicate SkTerm)))
input)
where shaves :: [SkTerm] -> Formula
shaves = 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)
"shaves" :: [SkTerm] -> Formula
[SkTerm
b, SkTerm
x] = [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"b", TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"x"] :: [SkTerm]
fx :: [SkTerm] -> SkTerm
fx = FunOf SkTerm -> [SkTerm] -> SkTerm
forall term. IsTerm term => FunOf term -> [term] -> term
fApp (V -> Int -> Function
Skolem V
"x" Int
1) :: [SkTerm] -> SkTerm
barb :: Formula
barb = VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists V
VarOf Formula
"b" (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"x" ([SkTerm] -> Formula
shaves [SkTerm
b, SkTerm
x] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. Formula -> Formula
forall formula. IsLiteral formula => formula -> formula
(.~.)([SkTerm] -> Formula
shaves [SkTerm
x, SkTerm
x]))) :: Formula
input :: Set (Set (LFormula SkAtom))
input :: Set (Set (LFormula (FOL Predicate SkTerm)))
input = (AtomOf (PFormula (FOL Predicate SkTerm))
-> AtomOf (LFormula (FOL Predicate SkTerm)))
-> PFormula (FOL Predicate SkTerm)
-> Set (Set (LFormula (FOL Predicate SkTerm)))
forall pf lit.
(JustPropositional pf, JustLiteral lit, Ord lit) =>
(AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
simpcnf AtomOf (PFormula (FOL Predicate SkTerm))
-> AtomOf (LFormula (FOL Predicate SkTerm))
FOL Predicate SkTerm -> FOL Predicate SkTerm
forall a. a -> a
id (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 -> Formula
forall formula. IsLiteral formula => formula -> formula
(.~.)Formula
barb)) :: PFormula SkAtom)
expected :: Set (Set Formula)
expected :: Set (Set Formula)
expected = [Set Formula] -> Set (Set Formula)
forall a. Ord a => [a] -> Set a
Set.fromList [[Formula] -> Set Formula
forall a. Ord a => [a] -> Set a
Set.fromList [[SkTerm] -> Formula
shaves [SkTerm
b, [SkTerm] -> SkTerm
fx [SkTerm
b]], Formula -> Formula
forall formula. IsLiteral formula => formula -> formula
(.~.)([SkTerm] -> Formula
shaves [[SkTerm] -> SkTerm
fx [SkTerm
b],[SkTerm] -> SkTerm
fx [SkTerm
b]])],
[Formula] -> Set Formula
forall a. Ord a => [a] -> Set a
Set.fromList [[SkTerm] -> Formula
shaves [[SkTerm] -> SkTerm
fx [SkTerm
b],[SkTerm] -> SkTerm
fx [SkTerm
b]], Formula -> Formula
forall formula. IsLiteral formula => formula -> formula
(.~.)([SkTerm] -> Formula
shaves [SkTerm
b, [SkTerm] -> SkTerm
fx [SkTerm
b]])]]
mgu :: forall lit atom term v.
(JustLiteral lit, HasApply atom, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), IsTerm term,
atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
Set lit -> StateT (Map v term) Failing (Map v term)
mgu :: forall lit atom term v.
(JustLiteral lit, HasApply atom, Unify Failing (atom, atom),
term ~ UTermOf (atom, atom), IsTerm term, atom ~ AtomOf lit,
term ~ TermOf atom, v ~ TVarOf term) =>
Set lit -> StateT (Map v term) Failing (Map v term)
mgu Set lit
l =
case Set lit -> Maybe (lit, Set lit)
forall a. Set a -> Maybe (a, Set a)
Set.minView Set lit
l of
Just (lit
a, Set lit
rest) ->
case Set lit -> Maybe (lit, Set lit)
forall a. Set a -> Maybe (a, Set a)
Set.minView Set lit
rest of
Just (lit
b, Set lit
_) -> lit -> lit -> StateT (Map v term) Failing ()
forall lit1 lit2 atom1 atom2 v term (m :: * -> *).
(IsLiteral lit1, HasApply atom1, atom1 ~ AtomOf lit1,
term ~ TermOf atom1, JustLiteral lit2, HasApply atom2,
atom2 ~ AtomOf lit2, term ~ TermOf atom2, Unify m (atom1, atom2),
term ~ UTermOf (atom1, atom2), v ~ TVarOf term, MonadFail m) =>
lit1 -> lit2 -> StateT (Map v term) m ()
unify_literals lit
a lit
b StateT (Map v term) Failing ()
-> StateT (Map v term) Failing (Map v term)
-> StateT (Map v term) Failing (Map v term)
forall a b.
StateT (Map v term) Failing a
-> StateT (Map v term) Failing b -> StateT (Map v term) Failing b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Set lit -> StateT (Map v term) Failing (Map v term)
forall lit atom term v.
(JustLiteral lit, HasApply atom, Unify Failing (atom, atom),
term ~ UTermOf (atom, atom), IsTerm term, atom ~ AtomOf lit,
term ~ TermOf atom, v ~ TVarOf term) =>
Set lit -> StateT (Map v term) Failing (Map v term)
mgu Set lit
rest
Maybe (lit, Set lit)
_ -> Map v term -> Map v term
forall term v.
(IsTerm term, v ~ TVarOf term) =>
Map v term -> Map v term
solve (Map v term -> Map v term)
-> StateT (Map v term) Failing (Map v term)
-> StateT (Map v term) Failing (Map v term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT (Map v term) Failing (Map v term)
forall s (m :: * -> *). MonadState s m => m s
get
Maybe (lit, Set lit)
_ -> Map v term -> Map v term
forall term v.
(IsTerm term, v ~ TVarOf term) =>
Map v term -> Map v term
solve (Map v term -> Map v term)
-> StateT (Map v term) Failing (Map v term)
-> StateT (Map v term) Failing (Map v term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT (Map v term) Failing (Map v term)
forall s (m :: * -> *). MonadState s m => m s
get
unifiable :: forall lit term atom v.
(JustLiteral lit, IsTerm term, HasApply atom, Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
lit -> lit -> Bool
unifiable :: forall lit term atom v.
(JustLiteral lit, IsTerm term, HasApply atom,
Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
lit -> lit -> Bool
unifiable lit
p lit
q = ([String] -> Bool)
-> (Map v term -> Bool) -> Failing (Map v term) -> Bool
forall b a. ([String] -> b) -> (a -> b) -> Failing a -> b
failing (Bool -> [String] -> Bool
forall a b. a -> b -> a
const Bool
False) (Bool -> Map v term -> Bool
forall a b. a -> b -> a
const Bool
True) (StateT (Map v term) Failing ()
-> Map v term -> Failing (Map v term)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT (lit -> lit -> StateT (Map v term) Failing ()
forall lit1 lit2 atom1 atom2 v term (m :: * -> *).
(IsLiteral lit1, HasApply atom1, atom1 ~ AtomOf lit1,
term ~ TermOf atom1, JustLiteral lit2, HasApply atom2,
atom2 ~ AtomOf lit2, term ~ TermOf atom2, Unify m (atom1, atom2),
term ~ UTermOf (atom1, atom2), v ~ TVarOf term, MonadFail m) =>
lit1 -> lit2 -> StateT (Map v term) m ()
unify_literals lit
p lit
q) Map v term
forall k a. Map k a
Map.empty :: Failing (Map v term))
rename :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term,
atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
(v -> v) -> Set lit -> Set lit
rename :: forall lit atom term v.
(JustLiteral lit, Ord lit, HasApply atom, IsTerm term,
atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
(v -> v) -> Set lit -> Set lit
rename v -> v
pfx Set lit
cls =
(lit -> lit) -> Set lit -> Set lit
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Map v term -> lit -> lit
forall lit atom term v.
(JustLiteral lit, HasApply atom, IsTerm term, atom ~ AtomOf lit,
term ~ TermOf atom, v ~ TVarOf term) =>
Map v term -> lit -> lit
lsubst ([(v, term)] -> Map v term
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList (Set (v, term) -> [(v, term)]
forall a. Set a -> [a]
Set.toList ((v -> (v, term)) -> Set v -> Set (v, term)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\v
v -> (v
v, (TVarOf term -> term
forall term. IsTerm term => TVarOf term -> term
vt (v -> v
pfx v
v)))) Set v
fvs)))) Set lit
cls
where
fvs :: Set v
fvs = (Set v -> Set v -> Set v) -> Set v -> Set (Set v) -> Set v
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold Set v -> Set v -> Set v
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set v
forall a. Set a
Set.empty ((lit -> Set v) -> Set lit -> Set (Set v)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map lit -> Set v
forall formula atom term v.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula,
term ~ TermOf atom, v ~ TVarOf term) =>
formula -> Set v
var Set lit
cls)
resolvents :: (JustLiteral lit, Ord lit, HasApply atom, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), IsTerm term,
atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
Set lit -> Set lit -> lit -> Set lit -> Set lit
resolvents :: forall lit atom term v.
(JustLiteral lit, Ord lit, HasApply atom,
Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
IsTerm term, atom ~ AtomOf lit, term ~ TermOf atom,
v ~ TVarOf term) =>
Set lit -> Set lit -> lit -> Set lit -> Set lit
resolvents Set lit
cl1 Set lit
cl2 lit
p Set lit
acc =
if Set lit -> Bool
forall a. Set a -> Bool
Set.null Set lit
ps2 then Set lit
acc else ((Set lit, Set lit) -> Set lit -> Set lit)
-> Set lit -> Set (Set lit, Set lit) -> Set lit
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (Set lit, Set lit) -> Set lit -> Set lit
doPair Set lit
acc Set (Set lit, Set lit)
pairs
where
doPair :: (Set lit, Set lit) -> Set lit -> Set lit
doPair (Set lit
s1,Set lit
s2) Set lit
sof =
case StateT
(Map v (UTermOf (atom, atom)))
Failing
(Map v (UTermOf (atom, atom)))
-> Map v (UTermOf (atom, atom))
-> Failing (Map v (UTermOf (atom, atom)))
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT (Set lit
-> StateT
(Map v (UTermOf (atom, atom)))
Failing
(Map v (UTermOf (atom, atom)))
forall lit atom term v.
(JustLiteral lit, HasApply atom, Unify Failing (atom, atom),
term ~ UTermOf (atom, atom), IsTerm term, atom ~ AtomOf lit,
term ~ TermOf atom, v ~ TVarOf term) =>
Set lit -> StateT (Map v term) Failing (Map v term)
mgu (Set lit -> Set lit -> Set lit
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set lit
s1 ((lit -> lit) -> Set lit -> Set lit
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map lit -> lit
forall formula. IsLiteral formula => formula -> formula
(.~.) Set lit
s2))) Map v (UTermOf (atom, atom))
forall k a. Map k a
Map.empty of
Success Map v (UTermOf (atom, atom))
mp -> Set lit -> Set lit -> Set lit
forall a. Ord a => Set a -> Set a -> Set a
Set.union ((lit -> lit) -> Set lit -> Set lit
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Map v (UTermOf (atom, atom)) -> lit -> lit
forall lit atom term v.
(JustLiteral lit, HasApply atom, IsTerm term, atom ~ AtomOf lit,
term ~ TermOf atom, v ~ TVarOf term) =>
Map v term -> lit -> lit
lsubst Map v (UTermOf (atom, atom))
mp) (Set lit -> Set lit -> Set lit
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Set lit -> Set lit -> Set lit
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set lit
cl1 Set lit
s1) (Set lit -> Set lit -> Set lit
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set lit
cl2 Set lit
s2))) Set lit
sof
Failure [String]
_ -> Set lit
sof
pairs :: Set (Set lit, Set lit)
pairs = (Set lit -> Set lit -> (Set lit, Set lit))
-> Set (Set lit) -> Set (Set lit) -> Set (Set lit, Set lit)
forall a b c (set :: * -> *).
(SetLike set, Ord c) =>
(a -> b -> c) -> set a -> set b -> set c
allpairs (,) ((Set lit -> Set lit) -> Set (Set lit) -> Set (Set lit)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (lit -> Set lit -> Set lit
forall a. Ord a => a -> Set a -> Set a
Set.insert lit
p) (Set lit -> Set (Set lit)
forall a. Ord a => Set a -> Set (Set a)
allsubsets Set lit
ps1)) (Set lit -> Set (Set lit)
forall a. Ord a => Set a -> Set (Set a)
allnonemptysubsets Set lit
ps2)
ps1 :: Set lit
ps1 = (lit -> Bool) -> Set lit -> Set lit
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\ lit
q -> lit
q lit -> lit -> Bool
forall a. Eq a => a -> a -> Bool
/= lit
p Bool -> Bool -> Bool
&& lit -> lit -> Bool
forall lit term atom v.
(JustLiteral lit, IsTerm term, HasApply atom,
Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
lit -> lit -> Bool
unifiable lit
p lit
q) Set lit
cl1
ps2 :: Set lit
ps2 = (lit -> Bool) -> Set lit -> Set lit
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (lit -> lit -> Bool
forall lit term atom v.
(JustLiteral lit, IsTerm term, HasApply atom,
Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
lit -> lit -> Bool
unifiable (lit -> lit
forall formula. IsLiteral formula => formula -> formula
(.~.) lit
p)) Set lit
cl2
resolve_clauses :: (JustLiteral lit, Ord lit, HasApply atom, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), IsTerm term,
atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
Set lit -> Set lit -> Set lit
resolve_clauses :: forall lit atom term v.
(JustLiteral lit, Ord lit, HasApply atom,
Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
IsTerm term, atom ~ AtomOf lit, term ~ TermOf atom,
v ~ TVarOf term) =>
Set lit -> Set lit -> Set lit
resolve_clauses Set lit
cls1 Set lit
cls2 =
let cls1' :: Set lit
cls1' = (v -> v) -> Set lit -> Set lit
forall lit atom term v.
(JustLiteral lit, Ord lit, HasApply atom, IsTerm term,
atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
(v -> v) -> Set lit -> Set lit
rename (String -> v -> v
forall v. IsVariable v => String -> v -> v
prefix String
"x") Set lit
cls1
cls2' :: Set lit
cls2' = (v -> v) -> Set lit -> Set lit
forall lit atom term v.
(JustLiteral lit, Ord lit, HasApply atom, IsTerm term,
atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
(v -> v) -> Set lit -> Set lit
rename (String -> v -> v
forall v. IsVariable v => String -> v -> v
prefix String
"y") Set lit
cls2 in
(lit -> Set lit -> Set lit) -> Set lit -> Set lit -> Set lit
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (Set lit -> Set lit -> lit -> Set lit -> Set lit
forall lit atom term v.
(JustLiteral lit, Ord lit, HasApply atom,
Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
IsTerm term, atom ~ AtomOf lit, term ~ TermOf atom,
v ~ TVarOf term) =>
Set lit -> Set lit -> lit -> Set lit -> Set lit
resolvents Set lit
cls1' Set lit
cls2') Set lit
forall a. Set a
Set.empty Set lit
cls1'
resloop1 :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term, Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
Set (Set lit) -> Set (Set lit) -> Failing Bool
resloop1 :: forall lit atom term v.
(JustLiteral lit, Ord lit, HasApply atom, IsTerm term,
Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
Set (Set lit) -> Set (Set lit) -> Failing Bool
resloop1 Set (Set lit)
used Set (Set lit)
unused =
Failing Bool
-> ((Set lit, Set (Set lit)) -> Failing Bool)
-> Maybe (Set lit, Set (Set lit))
-> Failing Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ([String] -> Failing Bool
forall a. [String] -> Failing a
Failure [String
"No proof found"]) (Set lit, Set (Set lit)) -> Failing Bool
step (Set (Set lit) -> Maybe (Set lit, Set (Set lit))
forall a. Set a -> Maybe (a, Set a)
Set.minView Set (Set lit)
unused)
where
step :: (Set lit, Set (Set lit)) -> Failing Bool
step (Set lit
cl, Set (Set lit)
ros) =
if Set lit -> Set (Set lit) -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Set lit
forall a. Set a
Set.empty Set (Set lit)
news then Bool -> Failing Bool
forall a. a -> Failing a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True else Set (Set lit) -> Set (Set lit) -> Failing Bool
forall lit atom term v.
(JustLiteral lit, Ord lit, HasApply atom, IsTerm term,
Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
Set (Set lit) -> Set (Set lit) -> Failing Bool
resloop1 Set (Set lit)
used' (Set (Set lit) -> Set (Set lit) -> Set (Set lit)
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set (Set lit)
ros Set (Set lit)
news)
where
used' :: Set (Set lit)
used' = Set lit -> Set (Set lit) -> Set (Set lit)
forall a. Ord a => a -> Set a -> Set a
Set.insert Set lit
cl Set (Set lit)
used
news :: Set (Set lit)
news = (Set lit -> Set (Set lit) -> Set (Set lit))
-> Set (Set lit) -> Set (Set lit) -> Set (Set lit)
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold Set lit -> Set (Set lit) -> Set (Set lit)
forall a. Ord a => a -> Set a -> Set a
Set.insert Set (Set lit)
forall a. Set a
Set.empty ( (Set lit -> Set lit) -> Set (Set lit) -> Set (Set lit)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Set lit -> Set lit -> Set lit
forall lit atom term v.
(JustLiteral lit, Ord lit, HasApply atom,
Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
IsTerm term, atom ~ AtomOf lit, term ~ TermOf atom,
v ~ TVarOf term) =>
Set lit -> Set lit -> Set lit
resolve_clauses Set lit
cl) Set (Set lit)
used')
pure_resolution1 :: forall fof atom term v.
(atom ~ AtomOf fof, term ~ TermOf atom, v ~ TVarOf term,
IsFirstOrder fof,
Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
Ord fof, Pretty fof
) => fof -> Failing Bool
pure_resolution1 :: forall fof atom term v.
(atom ~ AtomOf fof, term ~ TermOf atom, v ~ TVarOf term,
IsFirstOrder fof, Unify Failing (atom, atom),
term ~ UTermOf (atom, atom), Ord fof, Pretty fof) =>
fof -> Failing Bool
pure_resolution1 fof
fm = Set (Set (LFormula atom))
-> Set (Set (LFormula atom)) -> Failing Bool
forall lit atom term v.
(JustLiteral lit, Ord lit, HasApply atom, IsTerm term,
Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
Set (Set lit) -> Set (Set lit) -> Failing Bool
resloop1 Set (Set (LFormula atom))
forall a. Set a
Set.empty ((AtomOf (PFormula atom) -> AtomOf (LFormula atom))
-> PFormula atom -> Set (Set (LFormula atom))
forall pf lit.
(JustPropositional pf, JustLiteral lit, Ord lit) =>
(AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
simpcnf atom -> atom
AtomOf (PFormula atom) -> AtomOf (LFormula atom)
forall a. a -> a
id ((AtomOf fof -> AtomOf (PFormula atom)) -> fof -> PFormula atom
forall fof pf.
(IsQuantified fof, JustPropositional pf) =>
(AtomOf fof -> AtomOf pf) -> fof -> pf
specialize atom -> atom
AtomOf fof -> AtomOf (PFormula atom)
forall a. a -> a
id (fof -> fof
forall formula. IsFirstOrder formula => formula -> formula
pnf fof
fm) :: PFormula atom) :: Set (Set (LFormula atom)))
resolution1 :: forall m fof atom term v function.
(IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Ord fof, HasSkolem function, Monad m,
atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) =>
fof -> SkolemT m function (Set (Failing Bool))
resolution1 :: forall (m :: * -> *) fof atom term v function.
(IsFirstOrder fof, Unify Failing (atom, atom),
term ~ UTermOf (atom, atom), Ord fof, HasSkolem function, Monad m,
atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term,
v ~ TVarOf term, v ~ SVarOf function) =>
fof -> SkolemT m function (Set (Failing Bool))
resolution1 fof
fm = fof -> SkolemT m function fof
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 (fof -> fof
forall formula. IsLiteral formula => formula -> formula
(.~.)(fof -> fof
forall formula. IsFirstOrder formula => formula -> formula
generalize fof
fm)) SkolemT m function fof
-> (fof -> StateT (SkolemState function) m (Set (Failing Bool)))
-> StateT (SkolemState function) m (Set (Failing Bool))
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
>>= Set (Failing Bool)
-> StateT (SkolemState function) m (Set (Failing Bool))
forall a. a -> StateT (SkolemState function) m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Set (Failing Bool)
-> StateT (SkolemState function) m (Set (Failing Bool)))
-> (fof -> Set (Failing Bool))
-> fof
-> StateT (SkolemState function) m (Set (Failing Bool))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set fof -> Failing Bool) -> Set (Set fof) -> Set (Failing Bool)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (fof -> Failing Bool
forall fof atom term v.
(atom ~ AtomOf fof, term ~ TermOf atom, v ~ TVarOf term,
IsFirstOrder fof, Unify Failing (atom, atom),
term ~ UTermOf (atom, atom), Ord fof, Pretty fof) =>
fof -> Failing Bool
pure_resolution1 (fof -> Failing Bool)
-> (Set fof -> fof) -> Set fof -> Failing Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set fof -> fof
forall (t :: * -> *) formula.
(Foldable t, IsFormula formula, IsPropositional formula) =>
t formula -> formula
list_conj) (Set (Set fof) -> Set (Failing Bool))
-> (fof -> Set (Set fof)) -> fof -> Set (Failing Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (fof -> Set (Set fof)
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 -> Set (Set fof))
davis_putnam_example_formula :: Formula
davis_putnam_example_formula :: Formula
davis_putnam_example_formula = [fof| ∃ x y. (∀ z. ((F(x,y)⇒F(y,z)∧F(z,z))∧(F(x,y)∧G(x,y)⇒G(x,z)∧G(z,z)))) |]
test02 :: Test
test02 :: Test
test02 =
Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> Set (Failing Bool) -> Set (Failing Bool) -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"Davis-Putnam example 1" Set (Failing Bool)
expected (SkolemT Identity Function (Set (Failing Bool))
-> Set (Failing Bool)
forall function a.
IsFunction function =>
SkolemT Identity function a -> a
runSkolem (Formula -> SkolemT Identity Function (Set (Failing Bool))
forall (m :: * -> *) fof atom term v function.
(IsFirstOrder fof, Unify Failing (atom, atom),
term ~ UTermOf (atom, atom), Ord fof, HasSkolem function, Monad m,
atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term,
v ~ TVarOf term, v ~ SVarOf function) =>
fof -> SkolemT m function (Set (Failing Bool))
resolution1 Formula
davis_putnam_example_formula))
where
expected :: Set (Failing Bool)
expected = Failing Bool -> Set (Failing Bool)
forall a. a -> Set a
Set.singleton (Bool -> Failing Bool
forall a. a -> Failing a
Success Bool
True)
class Match a v term where
match :: Map v term -> a -> Failing (Map v term)
match_terms :: forall term v. (IsTerm term, v ~ TVarOf term) => Map v term -> [(term, term)] -> Failing (Map v term)
match_terms :: forall term v.
(IsTerm term, v ~ TVarOf term) =>
Map v term -> [(term, term)] -> Failing (Map v term)
match_terms Map v term
env [] = Map v term -> Failing (Map v term)
forall a. a -> Failing a
Success Map v term
env
match_terms Map v term
env ((term
p, term
q) : [(term, term)]
oth) =
(TVarOf term -> Failing (Map v term))
-> (FunOf term -> [term] -> Failing (Map v term))
-> term
-> Failing (Map v term)
forall term r.
IsTerm term =>
(TVarOf term -> r) -> (FunOf term -> [term] -> r) -> term -> r
forall r.
(TVarOf term -> r) -> (FunOf term -> [term] -> r) -> term -> r
foldTerm v -> Failing (Map v term)
TVarOf term -> Failing (Map v term)
vr FunOf term -> [term] -> Failing (Map v term)
fn term
p
where
vr :: v -> Failing (Map v term)
vr v
x | Bool -> Bool
not (Map v term -> v -> Bool
forall t a. Ord t => Map t a -> t -> Bool
defined Map v term
env v
x) = Map v term -> [(term, term)] -> Failing (Map v term)
forall term v.
(IsTerm term, v ~ TVarOf term) =>
Map v term -> [(term, term)] -> Failing (Map v term)
match_terms ((v
x v -> term -> Map v term -> Map v term
forall k a. Ord k => k -> a -> Map k a -> Map k a
|-> term
q) Map v term
env) [(term, term)]
oth
| Map v term -> v -> Maybe term
forall k a. Ord k => Map k a -> k -> Maybe a
apply Map v term
env v
x Maybe term -> Maybe term -> Bool
forall a. Eq a => a -> a -> Bool
== term -> Maybe term
forall a. a -> Maybe a
Just term
q = Map v term -> [(term, term)] -> Failing (Map v term)
forall term v.
(IsTerm term, v ~ TVarOf term) =>
Map v term -> [(term, term)] -> Failing (Map v term)
match_terms Map v term
env [(term, term)]
oth
| Bool
otherwise = String -> Failing (Map v term)
forall a. String -> Failing a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"match_terms"
fn :: FunOf term -> [term] -> Failing (Map v term)
fn FunOf term
f [term]
fa =
(TVarOf term -> Failing (Map v term))
-> (FunOf term -> [term] -> Failing (Map v term))
-> term
-> Failing (Map v term)
forall term r.
IsTerm term =>
(TVarOf term -> r) -> (FunOf term -> [term] -> r) -> term -> r
forall r.
(TVarOf term -> r) -> (FunOf term -> [term] -> r) -> term -> r
foldTerm v -> Failing (Map v term)
TVarOf term -> Failing (Map v term)
forall {m :: * -> *} {p} {a}. MonadFail m => p -> m a
vr' FunOf term -> [term] -> Failing (Map v term)
fn' term
q
where
fn' :: FunOf term -> [term] -> Failing (Map v term)
fn' FunOf term
g [term]
ga | FunOf term
f FunOf term -> FunOf term -> Bool
forall a. Eq a => a -> a -> Bool
== FunOf term
g Bool -> Bool -> Bool
&& [term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [term]
fa Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [term]
ga = Map v term -> [(term, term)] -> Failing (Map v term)
forall term v.
(IsTerm term, v ~ TVarOf term) =>
Map v term -> [(term, term)] -> Failing (Map v term)
match_terms Map v term
env ([term] -> [term] -> [(term, term)]
forall a b. [a] -> [b] -> [(a, b)]
zip [term]
fa [term]
ga [(term, term)] -> [(term, term)] -> [(term, term)]
forall a. [a] -> [a] -> [a]
++ [(term, term)]
oth)
fn' FunOf term
_ [term]
_ = String -> Failing (Map v term)
forall a. String -> Failing a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"match_terms"
vr' :: p -> m a
vr' p
_ = String -> m a
forall a. String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"match_terms"
match_atoms :: (JustApply atom, IsTerm term, term ~ TermOf atom, v ~ TVarOf term) =>
Map v term -> (atom, atom) -> Failing (Map v term)
match_atoms :: forall atom term v.
(JustApply atom, IsTerm term, term ~ TermOf atom,
v ~ TVarOf term) =>
Map v term -> (atom, atom) -> Failing (Map v term)
match_atoms Map v term
env (atom
a1, atom
a2) =
Failing (Map v term)
-> (Failing (Map v term) -> Failing (Map v term))
-> Maybe (Failing (Map v term))
-> Failing (Map v term)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ([String] -> Failing (Map v term)
forall a. [String] -> Failing a
Failure [String
"match_atoms"]) Failing (Map v term) -> Failing (Map v term)
forall a. a -> a
id ((PredOf atom -> [(term, term)] -> Maybe (Failing (Map v term)))
-> atom -> atom -> Maybe (Failing (Map v term))
forall atom1 term predicate atom2 r.
(JustApply atom1, term ~ TermOf atom1, predicate ~ PredOf atom1,
JustApply atom2, term ~ TermOf atom2, predicate ~ PredOf atom2) =>
(predicate -> [(term, term)] -> Maybe r)
-> atom1 -> atom2 -> Maybe r
zipApplys (\PredOf atom
_ [(term, term)]
pairs -> Failing (Map v term) -> Maybe (Failing (Map v term))
forall a. a -> Maybe a
Just (Map v term -> [(term, term)] -> Failing (Map v term)
forall term v.
(IsTerm term, v ~ TVarOf term) =>
Map v term -> [(term, term)] -> Failing (Map v term)
match_terms Map v term
env [(term, term)]
pairs)) atom
a1 atom
a2)
match_atoms_eq :: (HasEquate atom, IsTerm term, term ~ TermOf atom, v ~ TVarOf term) =>
Map v term -> (atom, atom) -> Failing (Map v term)
match_atoms_eq :: forall atom term v.
(HasEquate atom, IsTerm term, term ~ TermOf atom,
v ~ TVarOf term) =>
Map v term -> (atom, atom) -> Failing (Map v term)
match_atoms_eq Map v term
env (atom
a1, atom
a2) =
Failing (Map v term)
-> (Failing (Map v term) -> Failing (Map v term))
-> Maybe (Failing (Map v term))
-> Failing (Map v term)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ([String] -> Failing (Map v term)
forall a. [String] -> Failing a
Failure [String
"match_atoms_eq"]) Failing (Map v term) -> Failing (Map v term)
forall a. a -> a
id ((TermOf atom
-> TermOf atom
-> TermOf atom
-> TermOf atom
-> Maybe (Failing (Map v term)))
-> (PredOf atom
-> [(TermOf atom, TermOf atom)] -> Maybe (Failing (Map v term)))
-> atom
-> atom
-> Maybe (Failing (Map v term))
forall atom1 atom2 r.
(HasEquate atom1, HasEquate atom2, PredOf atom1 ~ PredOf atom2) =>
(TermOf atom1
-> TermOf atom1 -> TermOf atom2 -> TermOf atom2 -> Maybe r)
-> (PredOf atom1 -> [(TermOf atom1, TermOf atom2)] -> Maybe r)
-> atom1
-> atom2
-> Maybe r
zipEquates (\TermOf atom
l1 TermOf atom
r1 TermOf atom
l2 TermOf atom
r2 -> Failing (Map v term) -> Maybe (Failing (Map v term))
forall a. a -> Maybe a
Just (Map v term -> [(term, term)] -> Failing (Map v term)
forall term v.
(IsTerm term, v ~ TVarOf term) =>
Map v term -> [(term, term)] -> Failing (Map v term)
match_terms Map v term
env [(term
TermOf atom
l1, term
TermOf atom
l2), (term
TermOf atom
r1, term
TermOf atom
r2)]))
(\PredOf atom
_ [(TermOf atom, TermOf atom)]
pairs -> Failing (Map v term) -> Maybe (Failing (Map v term))
forall a. a -> Maybe a
Just (Map v term -> [(term, term)] -> Failing (Map v term)
forall term v.
(IsTerm term, v ~ TVarOf term) =>
Map v term -> [(term, term)] -> Failing (Map v term)
match_terms Map v term
env [(term, term)]
[(TermOf atom, TermOf atom)]
pairs)) atom
a1 atom
a2)
match_literals :: forall lit atom term v.
(IsLiteral lit, HasApply atom, IsTerm term, Match (atom, atom) v term,
atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
Map v term -> lit -> lit -> Failing (Map v term)
match_literals :: forall lit atom term v.
(IsLiteral lit, HasApply atom, IsTerm term,
Match (atom, atom) v term, atom ~ AtomOf lit, term ~ TermOf atom,
v ~ TVarOf term) =>
Map v term -> lit -> lit -> Failing (Map v term)
match_literals Map v term
env lit
t1 lit
t2 =
Failing (Map v term)
-> Maybe (Failing (Map v term)) -> Failing (Map v term)
forall a. a -> Maybe a -> a
fromMaybe (String -> Failing (Map v term)
forall a. String -> Failing a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"match_literals") ((lit -> lit -> Maybe (Failing (Map v term)))
-> (lit -> lit -> Maybe (Failing (Map v term)))
-> (Bool -> Bool -> Maybe (Failing (Map v term)))
-> (AtomOf lit -> AtomOf lit -> Maybe (Failing (Map v term)))
-> lit
-> lit
-> Maybe (Failing (Map v term))
forall lit1 lit2 r.
(IsLiteral lit1, IsLiteral lit2) =>
(lit1 -> lit2 -> Maybe r)
-> (lit1 -> lit2 -> Maybe r)
-> (Bool -> Bool -> Maybe r)
-> (AtomOf lit1 -> AtomOf lit2 -> Maybe r)
-> lit1
-> lit2
-> Maybe r
zipLiterals' lit -> lit -> Maybe (Failing (Map v term))
forall {p} {p} {a}. p -> p -> Maybe a
ho lit -> lit -> Maybe (Failing (Map v term))
ne Bool -> Bool -> Maybe (Failing (Map v term))
tf atom -> atom -> Maybe (Failing (Map v term))
AtomOf lit -> AtomOf lit -> Maybe (Failing (Map v term))
at lit
t1 lit
t2)
where
ho :: p -> p -> Maybe a
ho p
_ p
_ = Maybe a
forall a. Maybe a
Nothing
ne :: lit -> lit -> Maybe (Failing (Map v term))
ne lit
p lit
q = Failing (Map v term) -> Maybe (Failing (Map v term))
forall a. a -> Maybe a
Just (Failing (Map v term) -> Maybe (Failing (Map v term)))
-> Failing (Map v term) -> Maybe (Failing (Map v term))
forall a b. (a -> b) -> a -> b
$ Map v term -> lit -> lit -> Failing (Map v term)
forall lit atom term v.
(IsLiteral lit, HasApply atom, IsTerm term,
Match (atom, atom) v term, atom ~ AtomOf lit, term ~ TermOf atom,
v ~ TVarOf term) =>
Map v term -> lit -> lit -> Failing (Map v term)
match_literals Map v term
env lit
p lit
q
tf :: Bool -> Bool -> Maybe (Failing (Map v term))
tf Bool
a Bool
b = if Bool
a Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
b then Failing (Map v term) -> Maybe (Failing (Map v term))
forall a. a -> Maybe a
Just (Map v term -> Failing (Map v term)
forall a. a -> Failing a
Success Map v term
env) else Maybe (Failing (Map v term))
forall a. Maybe a
Nothing
at :: atom -> atom -> Maybe (Failing (Map v term))
at atom
a1 atom
a2 = Failing (Map v term) -> Maybe (Failing (Map v term))
forall a. a -> Maybe a
Just (Map v term -> (atom, atom) -> Failing (Map v term)
forall a v term.
Match a v term =>
Map v term -> a -> Failing (Map v term)
match Map v term
env (atom
a1, atom
a2))
resolution2 :: forall fof atom term v function m.
(IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof,
atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) =>
fof -> SkolemT m function (Set (Failing Bool))
resolution2 :: forall fof atom term v function (m :: * -> *).
(IsFirstOrder fof, Unify Failing (atom, atom),
term ~ UTermOf (atom, atom), Match (atom, atom) v term,
HasSkolem function, Monad m, Ord fof, atom ~ AtomOf fof,
term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term,
v ~ SVarOf function) =>
fof -> SkolemT m function (Set (Failing Bool))
resolution2 fof
fm = fof -> SkolemT m function fof
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 (fof -> fof
forall formula. IsLiteral formula => formula -> formula
(.~.) (fof -> fof
forall formula. IsFirstOrder formula => formula -> formula
generalize fof
fm)) SkolemT m function fof
-> (fof -> StateT (SkolemState function) m (Set (Failing Bool)))
-> StateT (SkolemState function) m (Set (Failing Bool))
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
>>= Set (Failing Bool)
-> StateT (SkolemState function) m (Set (Failing Bool))
forall a. a -> StateT (SkolemState function) m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Set (Failing Bool)
-> StateT (SkolemState function) m (Set (Failing Bool)))
-> (fof -> Set (Failing Bool))
-> fof
-> StateT (SkolemState function) m (Set (Failing Bool))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set fof -> Failing Bool) -> Set (Set fof) -> Set (Failing Bool)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (fof -> Failing Bool
forall fof atom term v.
(IsFirstOrder fof, Ord fof, Pretty fof, HasApply atom, IsTerm term,
Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
Match (atom, atom) v term, atom ~ AtomOf fof, term ~ TermOf atom,
v ~ TVarOf term) =>
fof -> Failing Bool
pure_resolution2 (fof -> Failing Bool)
-> (Set fof -> fof) -> Set fof -> Failing Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set fof -> fof
forall (t :: * -> *) formula.
(Foldable t, IsFormula formula, IsPropositional formula) =>
t formula -> formula
list_conj) (Set (Set fof) -> Set (Failing Bool))
-> (fof -> Set (Set fof)) -> fof -> Set (Failing Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (fof -> Set (Set fof)
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 -> Set (Set fof))
pure_resolution2 :: forall fof atom term v.
(IsFirstOrder fof, Ord fof, Pretty fof,
HasApply atom, IsTerm term,
Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term,
atom ~ AtomOf fof, term ~ TermOf atom, v ~ TVarOf term) =>
fof -> Failing Bool
pure_resolution2 :: forall fof atom term v.
(IsFirstOrder fof, Ord fof, Pretty fof, HasApply atom, IsTerm term,
Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
Match (atom, atom) v term, atom ~ AtomOf fof, term ~ TermOf atom,
v ~ TVarOf term) =>
fof -> Failing Bool
pure_resolution2 fof
fm = Set (Set (LFormula atom))
-> Set (Set (LFormula atom)) -> Failing Bool
forall lit atom term v.
(JustLiteral lit, Ord lit, HasApply atom, IsTerm term,
Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
Match (atom, atom) v term, atom ~ AtomOf lit, term ~ TermOf atom,
v ~ TVarOf term) =>
Set (Set lit) -> Set (Set lit) -> Failing Bool
resloop2 Set (Set (LFormula atom))
forall a. Set a
Set.empty ((AtomOf (PFormula atom) -> AtomOf (LFormula atom))
-> PFormula atom -> Set (Set (LFormula atom))
forall pf lit.
(JustPropositional pf, JustLiteral lit, Ord lit) =>
(AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
simpcnf atom -> atom
AtomOf (PFormula atom) -> AtomOf (LFormula atom)
forall a. a -> a
id ((AtomOf fof -> AtomOf (PFormula atom)) -> fof -> PFormula atom
forall fof pf.
(IsQuantified fof, JustPropositional pf) =>
(AtomOf fof -> AtomOf pf) -> fof -> pf
specialize atom -> atom
AtomOf fof -> AtomOf (PFormula atom)
forall a. a -> a
id (fof -> fof
forall formula. IsFirstOrder formula => formula -> formula
pnf fof
fm) :: PFormula atom) :: Set (Set (LFormula atom)))
resloop2 :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term,
Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term,
atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
Set (Set lit) -> Set (Set lit) -> Failing Bool
resloop2 :: forall lit atom term v.
(JustLiteral lit, Ord lit, HasApply atom, IsTerm term,
Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
Match (atom, atom) v term, atom ~ AtomOf lit, term ~ TermOf atom,
v ~ TVarOf term) =>
Set (Set lit) -> Set (Set lit) -> Failing Bool
resloop2 Set (Set lit)
used Set (Set lit)
unused =
case Set (Set lit) -> Maybe (Set lit, Set (Set lit))
forall a. Set a -> Maybe (a, Set a)
Set.minView Set (Set lit)
unused of
Maybe (Set lit, Set (Set lit))
Nothing -> [String] -> Failing Bool
forall a. [String] -> Failing a
Failure [String
"No proof found"]
Just (Set lit
cl, Set (Set lit)
ros) ->
let used' :: Set (Set lit)
used' = Set lit -> Set (Set lit) -> Set (Set lit)
forall a. Ord a => a -> Set a -> Set a
Set.insert Set lit
cl Set (Set lit)
used in
let news :: Set (Set lit)
news = (Set lit -> Set lit) -> Set (Set lit) -> Set (Set lit)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Set lit -> Set lit -> Set lit
forall lit atom term v.
(JustLiteral lit, Ord lit, HasApply atom,
Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
IsTerm term, atom ~ AtomOf lit, term ~ TermOf atom,
v ~ TVarOf term) =>
Set lit -> Set lit -> Set lit
resolve_clauses Set lit
cl) Set (Set lit)
used' in
if Set lit -> Set (Set lit) -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Set lit
forall a. Set a
Set.empty Set (Set lit)
news then Bool -> Failing Bool
forall a. a -> Failing a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True else Set (Set lit) -> Set (Set lit) -> Failing Bool
forall lit atom term v.
(JustLiteral lit, Ord lit, HasApply atom, IsTerm term,
Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
Match (atom, atom) v term, atom ~ AtomOf lit, term ~ TermOf atom,
v ~ TVarOf term) =>
Set (Set lit) -> Set (Set lit) -> Failing Bool
resloop2 Set (Set lit)
used' ((Set lit -> Set (Set lit) -> Set (Set lit))
-> Set (Set lit) -> Set (Set lit) -> Set (Set lit)
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (Set lit -> Set lit -> Set (Set lit) -> Set (Set lit)
forall atom lit term v.
(atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term,
IsLiteral lit, Ord lit, HasApply atom, Match (atom, atom) v term,
IsTerm term) =>
Set lit -> Set lit -> Set (Set lit) -> Set (Set lit)
incorporate Set lit
cl) Set (Set lit)
ros Set (Set lit)
news)
incorporate :: (atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term,
IsLiteral lit, Ord lit,
HasApply atom, Match (atom, atom) v term,
IsTerm term) =>
Set lit
-> Set lit
-> Set (Set lit)
-> Set (Set lit)
incorporate :: forall atom lit term v.
(atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term,
IsLiteral lit, Ord lit, HasApply atom, Match (atom, atom) v term,
IsTerm term) =>
Set lit -> Set lit -> Set (Set lit) -> Set (Set lit)
incorporate Set lit
gcl Set lit
cl Set (Set lit)
unused =
if Set lit -> Bool
forall lit. (Ord lit, IsLiteral lit) => Set lit -> Bool
trivial Set lit
cl Bool -> Bool -> Bool
|| (Set lit -> Bool) -> Set (Set lit) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
setAny (\ Set lit
c -> Set lit -> Set lit -> Bool
forall lit atom term v.
(IsLiteral lit, HasApply atom, IsTerm term,
Match (atom, atom) v term, atom ~ AtomOf lit, term ~ TermOf atom,
v ~ TVarOf term) =>
Set lit -> Set lit -> Bool
subsumes_clause Set lit
c Set lit
cl) (Set lit -> Set (Set lit) -> Set (Set lit)
forall a. Ord a => a -> Set a -> Set a
Set.insert Set lit
gcl Set (Set lit)
unused)
then Set (Set lit)
unused
else Set lit -> Set (Set lit) -> Set (Set lit)
forall atom lit term v.
(atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term,
IsLiteral lit, Ord lit, IsTerm term, HasApply atom,
Match (atom, atom) v term) =>
Set lit -> Set (Set lit) -> Set (Set lit)
replace Set lit
cl Set (Set lit)
unused
replace :: (atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term,
IsLiteral lit, Ord lit,
IsTerm term,
HasApply atom, Match (atom, atom) v term) =>
Set lit
-> Set (Set lit)
-> Set (Set lit)
replace :: forall atom lit term v.
(atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term,
IsLiteral lit, Ord lit, IsTerm term, HasApply atom,
Match (atom, atom) v term) =>
Set lit -> Set (Set lit) -> Set (Set lit)
replace Set lit
cl Set (Set lit)
st =
case Set (Set lit) -> Maybe (Set lit, Set (Set lit))
forall a. Set a -> Maybe (a, Set a)
Set.minView Set (Set lit)
st of
Maybe (Set lit, Set (Set lit))
Nothing -> Set lit -> Set (Set lit)
forall a. a -> Set a
Set.singleton Set lit
cl
Just (Set lit
c, Set (Set lit)
st') -> if Set lit -> Set lit -> Bool
forall lit atom term v.
(IsLiteral lit, HasApply atom, IsTerm term,
Match (atom, atom) v term, atom ~ AtomOf lit, term ~ TermOf atom,
v ~ TVarOf term) =>
Set lit -> Set lit -> Bool
subsumes_clause Set lit
cl Set lit
c
then Set lit -> Set (Set lit) -> Set (Set lit)
forall a. Ord a => a -> Set a -> Set a
Set.insert Set lit
cl Set (Set lit)
st'
else Set lit -> Set (Set lit) -> Set (Set lit)
forall a. Ord a => a -> Set a -> Set a
Set.insert Set lit
c (Set lit -> Set (Set lit) -> Set (Set lit)
forall atom lit term v.
(atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term,
IsLiteral lit, Ord lit, IsTerm term, HasApply atom,
Match (atom, atom) v term) =>
Set lit -> Set (Set lit) -> Set (Set lit)
replace Set lit
cl Set (Set lit)
st')
subsumes_clause :: (IsLiteral lit, HasApply atom, IsTerm term, Match (atom, atom) v term,
atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
Set lit -> Set lit -> Bool
subsumes_clause :: forall lit atom term v.
(IsLiteral lit, HasApply atom, IsTerm term,
Match (atom, atom) v term, atom ~ AtomOf lit, term ~ TermOf atom,
v ~ TVarOf term) =>
Set lit -> Set lit -> Bool
subsumes_clause Set lit
cls1 Set lit
cls2 =
([String] -> Bool)
-> (Map v term -> Bool) -> Failing (Map v term) -> Bool
forall b a. ([String] -> b) -> (a -> b) -> Failing a -> b
failing (Bool -> [String] -> Bool
forall a b. a -> b -> a
const Bool
False) (Bool -> Map v term -> Bool
forall a b. a -> b -> a
const Bool
True) (Map v term -> Set lit -> Failing (Map v term)
subsume Map v term
forall k a. Map k a
Map.empty Set lit
cls1)
where
subsume :: Map v term -> Set lit -> Failing (Map v term)
subsume Map v term
env Set lit
cls =
case Set lit -> Maybe (lit, Set lit)
forall a. Set a -> Maybe (a, Set a)
Set.minView Set lit
cls of
Maybe (lit, Set lit)
Nothing -> Map v term -> Failing (Map v term)
forall a. a -> Failing a
Success Map v term
env
Just (lit
l1, Set lit
clt) -> (lit -> Failing (Map v term)) -> Set lit -> Failing (Map v term)
forall t a. (t -> Failing a) -> Set t -> Failing a
settryfind (\ lit
l2 -> case (Map v term -> lit -> lit -> Failing (Map v term)
forall lit atom term v.
(IsLiteral lit, HasApply atom, IsTerm term,
Match (atom, atom) v term, atom ~ AtomOf lit, term ~ TermOf atom,
v ~ TVarOf term) =>
Map v term -> lit -> lit -> Failing (Map v term)
match_literals Map v term
env lit
l1 lit
l2) of
Success Map v term
env' -> Map v term -> Set lit -> Failing (Map v term)
subsume Map v term
env' Set lit
clt
Failure [String]
msgs -> [String] -> Failing (Map v term)
forall a. [String] -> Failing a
Failure [String]
msgs) Set lit
cls2
test03 :: Test
test03 :: Test
test03 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> Set (Failing Bool) -> Set (Failing Bool) -> Assertion
forall a.
(?loc::CallStack, Eq a, Pretty a) =>
String -> a -> a -> Assertion
assertEqual' String
"Davis-Putnam example 2" Set (Failing Bool)
expected (SkolemT Identity Function (Set (Failing Bool))
-> Set (Failing Bool)
forall function a.
IsFunction function =>
SkolemT Identity function a -> a
runSkolem (Formula -> SkolemT Identity Function (Set (Failing Bool))
forall fof atom term v function (m :: * -> *).
(IsFirstOrder fof, Unify Failing (atom, atom),
term ~ UTermOf (atom, atom), Match (atom, atom) v term,
HasSkolem function, Monad m, Ord fof, atom ~ AtomOf fof,
term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term,
v ~ SVarOf function) =>
fof -> SkolemT m function (Set (Failing Bool))
resolution2 Formula
davis_putnam_example_formula))
where
expected :: Set (Failing Bool)
expected = Failing Bool -> Set (Failing Bool)
forall a. a -> Set a
Set.singleton (Bool -> Failing Bool
forall a. a -> Failing a
Success Bool
True)
presolution :: forall fof atom term v function m.
(IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof, Pretty fof,
atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) =>
fof -> SkolemT m function (Set (Failing Bool))
presolution :: forall fof atom term v function (m :: * -> *).
(IsFirstOrder fof, Unify Failing (atom, atom),
term ~ UTermOf (atom, atom), Match (atom, atom) v term,
HasSkolem function, Monad m, Ord fof, Pretty fof,
atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term,
v ~ VarOf fof, v ~ SVarOf function) =>
fof -> SkolemT m function (Set (Failing Bool))
presolution fof
fm =
fof -> SkolemT m function fof
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 (fof -> fof
forall formula. IsLiteral formula => formula -> formula
(.~.) (fof -> fof
forall formula. IsFirstOrder formula => formula -> formula
generalize fof
fm)) SkolemT m function fof
-> (fof -> StateT (SkolemState function) m (Set (Failing Bool)))
-> StateT (SkolemState function) m (Set (Failing Bool))
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
>>= Set (Failing Bool)
-> StateT (SkolemState function) m (Set (Failing Bool))
forall a. a -> StateT (SkolemState function) m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Set (Failing Bool)
-> StateT (SkolemState function) m (Set (Failing Bool)))
-> (fof -> Set (Failing Bool))
-> fof
-> StateT (SkolemState function) m (Set (Failing Bool))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set fof -> Failing Bool) -> Set (Set fof) -> Set (Failing Bool)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (fof -> Failing Bool
forall fof atom term v.
(IsFirstOrder fof, Unify Failing (atom, atom),
term ~ UTermOf (atom, atom), Match (atom, atom) v term, Ord fof,
Pretty fof, atom ~ AtomOf fof, term ~ TermOf atom, v ~ VarOf fof,
v ~ TVarOf term) =>
fof -> Failing Bool
pure_presolution (fof -> Failing Bool)
-> (Set fof -> fof) -> Set fof -> Failing Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set fof -> fof
forall (t :: * -> *) formula.
(Foldable t, IsFormula formula, IsPropositional formula) =>
t formula -> formula
list_conj) (Set (Set fof) -> Set (Failing Bool))
-> (fof -> Set (Set fof)) -> fof -> Set (Failing Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (fof -> Set (Set fof)
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 -> Set (Set fof))
pure_presolution :: forall fof atom term v.
(IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, Ord fof, Pretty fof,
atom ~ AtomOf fof, term ~ TermOf atom, v ~ VarOf fof, v ~ TVarOf term) =>
fof -> Failing Bool
pure_presolution :: forall fof atom term v.
(IsFirstOrder fof, Unify Failing (atom, atom),
term ~ UTermOf (atom, atom), Match (atom, atom) v term, Ord fof,
Pretty fof, atom ~ AtomOf fof, term ~ TermOf atom, v ~ VarOf fof,
v ~ TVarOf term) =>
fof -> Failing Bool
pure_presolution fof
fm = Set (Set (LFormula atom))
-> Set (Set (LFormula atom)) -> Failing Bool
forall lit atom term v.
(JustLiteral lit, Ord lit, HasApply atom, IsTerm term,
Match (atom, atom) v term, Unify Failing (atom, atom),
term ~ UTermOf (atom, atom), atom ~ AtomOf lit, term ~ TermOf atom,
v ~ TVarOf term) =>
Set (Set lit) -> Set (Set lit) -> Failing Bool
presloop Set (Set (LFormula atom))
forall a. Set a
Set.empty ((AtomOf (PFormula atom) -> AtomOf (LFormula atom))
-> PFormula atom -> Set (Set (LFormula atom))
forall pf lit.
(JustPropositional pf, JustLiteral lit, Ord lit) =>
(AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
simpcnf atom -> atom
AtomOf (PFormula atom) -> AtomOf (LFormula atom)
forall a. a -> a
id ((AtomOf fof -> AtomOf (PFormula atom)) -> fof -> PFormula atom
forall fof pf.
(IsQuantified fof, JustPropositional pf) =>
(AtomOf fof -> AtomOf pf) -> fof -> pf
specialize atom -> atom
AtomOf fof -> AtomOf (PFormula atom)
forall a. a -> a
id (fof -> fof
forall formula. IsFirstOrder formula => formula -> formula
pnf fof
fm :: fof) :: PFormula atom) :: Set (Set (LFormula atom)))
presloop :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term,
Match (atom, atom) v term, Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
Set (Set lit) -> Set (Set lit) -> Failing Bool
presloop :: forall lit atom term v.
(JustLiteral lit, Ord lit, HasApply atom, IsTerm term,
Match (atom, atom) v term, Unify Failing (atom, atom),
term ~ UTermOf (atom, atom), atom ~ AtomOf lit, term ~ TermOf atom,
v ~ TVarOf term) =>
Set (Set lit) -> Set (Set lit) -> Failing Bool
presloop Set (Set lit)
used Set (Set lit)
unused =
case Set (Set lit) -> Maybe (Set lit, Set (Set lit))
forall a. Set a -> Maybe (a, Set a)
Set.minView Set (Set lit)
unused of
Maybe (Set lit, Set (Set lit))
Nothing -> [String] -> Failing Bool
forall a. [String] -> Failing a
Failure [String
"No proof found"]
Just (Set lit
cl, Set (Set lit)
ros) ->
let used' :: Set (Set lit)
used' = Set lit -> Set (Set lit) -> Set (Set lit)
forall a. Ord a => a -> Set a -> Set a
Set.insert Set lit
cl Set (Set lit)
used in
let news :: Set (Set lit)
news = (Set lit -> Set lit) -> Set (Set lit) -> Set (Set lit)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Set lit -> Set lit -> Set lit
forall lit atom term v.
(JustLiteral lit, Ord lit, HasApply atom, IsTerm term,
Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
Set lit -> Set lit -> Set lit
presolve_clauses Set lit
cl) Set (Set lit)
used' in
if Set lit -> Set (Set lit) -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Set lit
forall a. Set a
Set.empty Set (Set lit)
news
then Bool -> Failing Bool
forall a. a -> Failing a
Success Bool
True
else Set (Set lit) -> Set (Set lit) -> Failing Bool
forall lit atom term v.
(JustLiteral lit, Ord lit, HasApply atom, IsTerm term,
Match (atom, atom) v term, Unify Failing (atom, atom),
term ~ UTermOf (atom, atom), atom ~ AtomOf lit, term ~ TermOf atom,
v ~ TVarOf term) =>
Set (Set lit) -> Set (Set lit) -> Failing Bool
presloop Set (Set lit)
used' ((Set lit -> Set (Set lit) -> Set (Set lit))
-> Set (Set lit) -> Set (Set lit) -> Set (Set lit)
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (Set lit -> Set lit -> Set (Set lit) -> Set (Set lit)
forall atom lit term v.
(atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term,
IsLiteral lit, Ord lit, HasApply atom, Match (atom, atom) v term,
IsTerm term) =>
Set lit -> Set lit -> Set (Set lit) -> Set (Set lit)
incorporate Set lit
cl) Set (Set lit)
ros Set (Set lit)
news)
presolve_clauses :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term, Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
Set lit -> Set lit -> Set lit
presolve_clauses :: forall lit atom term v.
(JustLiteral lit, Ord lit, HasApply atom, IsTerm term,
Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
Set lit -> Set lit -> Set lit
presolve_clauses Set lit
cls1 Set lit
cls2 =
if (lit -> Bool) -> Set lit -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
setAll lit -> Bool
forall formula. IsLiteral formula => formula -> Bool
positive Set lit
cls1 Bool -> Bool -> Bool
|| (lit -> Bool) -> Set lit -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
setAll lit -> Bool
forall formula. IsLiteral formula => formula -> Bool
positive Set lit
cls2
then Set lit -> Set lit -> Set lit
forall lit atom term v.
(JustLiteral lit, Ord lit, HasApply atom,
Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
IsTerm term, atom ~ AtomOf lit, term ~ TermOf atom,
v ~ TVarOf term) =>
Set lit -> Set lit -> Set lit
resolve_clauses Set lit
cls1 Set lit
cls2
else Set lit
forall a. Set a
Set.empty
resolution3 :: forall fof atom term v function m.
(IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof,
atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) =>
fof -> SkolemT m function (Set (Failing Bool))
resolution3 :: forall fof atom term v function (m :: * -> *).
(IsFirstOrder fof, Unify Failing (atom, atom),
term ~ UTermOf (atom, atom), Match (atom, atom) v term,
HasSkolem function, Monad m, Ord fof, atom ~ AtomOf fof,
term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof,
v ~ SVarOf function) =>
fof -> SkolemT m function (Set (Failing Bool))
resolution3 fof
fm =
fof -> SkolemT m function fof
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 (fof -> fof
forall formula. IsLiteral formula => formula -> formula
(.~.)(fof -> fof
forall formula. IsFirstOrder formula => formula -> formula
generalize fof
fm)) SkolemT m function fof
-> (fof -> StateT (SkolemState function) m (Set (Failing Bool)))
-> StateT (SkolemState function) m (Set (Failing Bool))
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
>>= Set (Failing Bool)
-> StateT (SkolemState function) m (Set (Failing Bool))
forall a. a -> StateT (SkolemState function) m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Set (Failing Bool)
-> StateT (SkolemState function) m (Set (Failing Bool)))
-> (fof -> Set (Failing Bool))
-> fof
-> StateT (SkolemState function) m (Set (Failing Bool))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set fof -> Failing Bool) -> Set (Set fof) -> Set (Failing Bool)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (fof -> Failing Bool
forall fof atom term v.
(atom ~ AtomOf fof, term ~ TermOf atom, v ~ VarOf fof,
v ~ TVarOf term, IsFirstOrder fof, Unify Failing (atom, atom),
term ~ UTermOf (atom, atom), Match (atom, atom) v term, Ord fof,
Pretty fof) =>
fof -> Failing Bool
pure_resolution3 (fof -> Failing Bool)
-> (Set fof -> fof) -> Set fof -> Failing Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set fof -> fof
forall (t :: * -> *) formula.
(Foldable t, IsFormula formula, IsPropositional formula) =>
t formula -> formula
list_conj) (Set (Set fof) -> Set (Failing Bool))
-> (fof -> Set (Set fof)) -> fof -> Set (Failing Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (fof -> Set (Set fof)
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 -> Set (Set fof))
pure_resolution3 :: forall fof atom term v.
(atom ~ AtomOf fof, term ~ TermOf atom, v ~ VarOf fof, v ~ TVarOf term,
IsFirstOrder fof,
Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
Match (atom, atom) v term,
Ord fof, Pretty fof) => fof -> Failing Bool
pure_resolution3 :: forall fof atom term v.
(atom ~ AtomOf fof, term ~ TermOf atom, v ~ VarOf fof,
v ~ TVarOf term, IsFirstOrder fof, Unify Failing (atom, atom),
term ~ UTermOf (atom, atom), Match (atom, atom) v term, Ord fof,
Pretty fof) =>
fof -> Failing Bool
pure_resolution3 fof
fm =
(Set (Set (LFormula atom))
-> Set (Set (LFormula atom)) -> Failing Bool)
-> (Set (Set (LFormula atom)), Set (Set (LFormula atom)))
-> Failing Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Set (Set (LFormula atom))
-> Set (Set (LFormula atom)) -> Failing Bool
forall lit atom term v.
(JustLiteral lit, Ord lit, HasApply atom, IsTerm term,
Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
Match (atom, atom) v term, atom ~ AtomOf lit, term ~ TermOf atom,
v ~ TVarOf term) =>
Set (Set lit) -> Set (Set lit) -> Failing Bool
resloop2 ((Set (LFormula atom) -> Bool)
-> Set (Set (LFormula atom))
-> (Set (Set (LFormula atom)), Set (Set (LFormula atom)))
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.partition ((LFormula atom -> Bool) -> Set (LFormula atom) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
setAny LFormula atom -> Bool
forall formula. IsLiteral formula => formula -> Bool
positive) ((AtomOf (PFormula atom) -> AtomOf (LFormula atom))
-> PFormula atom -> Set (Set (LFormula atom))
forall pf lit.
(JustPropositional pf, JustLiteral lit, Ord lit) =>
(AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
simpcnf atom -> atom
AtomOf (PFormula atom) -> AtomOf (LFormula atom)
forall a. a -> a
id ((AtomOf fof -> AtomOf (PFormula atom)) -> fof -> PFormula atom
forall fof pf.
(IsQuantified fof, JustPropositional pf) =>
(AtomOf fof -> AtomOf pf) -> fof -> pf
specialize atom -> atom
AtomOf fof -> AtomOf (PFormula atom)
forall a. a -> a
id (fof -> fof
forall formula. IsFirstOrder formula => formula -> formula
pnf fof
fm) :: PFormula atom) :: Set (Set (LFormula atom))))
instance Match (SkAtom, SkAtom) V SkTerm where
match :: Map V SkTerm
-> (FOL Predicate SkTerm, FOL Predicate SkTerm)
-> Failing (Map V SkTerm)
match = Map V SkTerm
-> (FOL Predicate SkTerm, FOL Predicate SkTerm)
-> Failing (Map V SkTerm)
forall atom term v.
(HasEquate atom, IsTerm term, term ~ TermOf atom,
v ~ TVarOf term) =>
Map v term -> (atom, atom) -> Failing (Map v term)
match_atoms_eq
gilmore_1 :: Test
gilmore_1 :: Test
gilmore_1 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> Set (Failing Bool) -> Set (Failing Bool) -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"Gilmore 1" Set (Failing Bool)
expected (SkolemT Identity Function (Set (Failing Bool))
-> Set (Failing Bool)
forall function a.
IsFunction function =>
SkolemT Identity function a -> a
runSkolem (Formula -> SkolemT Identity Function (Set (Failing Bool))
forall fof atom term v function (m :: * -> *).
(IsFirstOrder fof, Unify Failing (atom, atom),
term ~ UTermOf (atom, atom), Match (atom, atom) v term,
HasSkolem function, Monad m, Ord fof, atom ~ AtomOf fof,
term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof,
v ~ SVarOf function) =>
fof -> SkolemT m function (Set (Failing Bool))
resolution3 Formula
fm))
where
expected :: Set (Failing Bool)
expected = Failing Bool -> Set (Failing Bool)
forall a. a -> Set a
Set.singleton (Bool -> Failing Bool
forall a. a -> Failing a
Success Bool
True)
fm :: Formula
fm :: Formula
fm = VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists V
VarOf Formula
"x" (Formula -> Formula) -> (Formula -> Formula) -> Formula -> 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 V
VarOf Formula
"y" (Formula -> Formula) -> (Formula -> Formula) -> Formula -> 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 V
VarOf Formula
"z" (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$
(([TermOf (AtomOf Formula)] -> Formula
f[SkTerm
TermOf (AtomOf Formula)
y] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. [TermOf (AtomOf Formula)] -> Formula
g[SkTerm
TermOf (AtomOf Formula)
y]) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. [TermOf (AtomOf Formula)] -> Formula
f[SkTerm
TermOf (AtomOf Formula)
x]) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&.
(([TermOf (AtomOf Formula)] -> Formula
f[SkTerm
TermOf (AtomOf Formula)
y] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. [TermOf (AtomOf Formula)] -> Formula
h[SkTerm
TermOf (AtomOf Formula)
y]) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. [TermOf (AtomOf Formula)] -> Formula
g[SkTerm
TermOf (AtomOf Formula)
x]) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&.
((([TermOf (AtomOf Formula)] -> Formula
f[SkTerm
TermOf (AtomOf Formula)
y] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. [TermOf (AtomOf Formula)] -> Formula
g[SkTerm
TermOf (AtomOf Formula)
y]) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. [TermOf (AtomOf Formula)] -> Formula
h[SkTerm
TermOf (AtomOf Formula)
y]) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. [TermOf (AtomOf Formula)] -> Formula
h[SkTerm
TermOf (AtomOf Formula)
x])
Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. [TermOf (AtomOf Formula)] -> Formula
f[SkTerm
TermOf (AtomOf Formula)
z] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. [TermOf (AtomOf Formula)] -> Formula
g[SkTerm
TermOf (AtomOf Formula)
z] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. [TermOf (AtomOf Formula)] -> Formula
h[SkTerm
TermOf (AtomOf Formula)
z]
[SkTerm
x, SkTerm
y, SkTerm
z] = [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", TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"z"] :: [SkTerm]
[[TermOf (AtomOf Formula)] -> Formula
f, [TermOf (AtomOf Formula)] -> Formula
g, [TermOf (AtomOf Formula)] -> Formula
h] = [PredOf (AtomOf Formula) -> [TermOf (AtomOf Formula)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp PredOf (AtomOf Formula)
"F", PredOf (AtomOf Formula) -> [TermOf (AtomOf Formula)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp PredOf (AtomOf Formula)
"G", PredOf (AtomOf Formula) -> [TermOf (AtomOf Formula)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp PredOf (AtomOf Formula)
"H"]
p1 :: Test
p1 :: Test
p1 =
let [Formula
p, Formula
q] = [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 (String -> Predicate
forall a. IsString a => String -> a
fromString String
"p") [], 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 (String -> Predicate
forall a. IsString a => String -> a
fromString String
"q") []] :: [Formula] in
Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> Set (Failing Bool) -> Set (Failing Bool) -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"p1" Set (Failing Bool)
forall a. Set a
Set.empty (SkolemT Identity Function (Set (Failing Bool))
-> Set (Failing Bool)
forall function a.
IsFunction function =>
SkolemT Identity function a -> a
runSkolem (Formula -> SkolemT Identity Function (Set (Failing Bool))
forall fof atom term v function (m :: * -> *).
(IsFirstOrder fof, Unify Failing (atom, atom),
term ~ UTermOf (atom, atom), Match (atom, atom) v term,
HasSkolem function, Monad m, Ord fof, Pretty fof,
atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term,
v ~ VarOf fof, v ~ SVarOf function) =>
fof -> SkolemT m function (Set (Failing Bool))
presolution ((Formula
p Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. Formula
q Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. Formula -> Formula
forall formula. IsLiteral formula => formula -> formula
(.~.)Formula
q Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. Formula -> Formula
forall formula. IsLiteral formula => formula -> formula
(.~.)Formula
p) :: Formula)))
los :: Test
los :: Test
los =
let [SkTerm
x, SkTerm
y, SkTerm
z] = (V -> SkTerm) -> [V] -> [SkTerm]
forall a b. (a -> b) -> [a] -> [b]
List.map (TVarOf SkTerm -> SkTerm
V -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt :: V -> SkTerm) [V
"x", V
"y", V
"z"]
[[SkTerm] -> Formula
p, [SkTerm] -> Formula
q] = (Predicate -> [SkTerm] -> Formula)
-> [Predicate] -> [[SkTerm] -> Formula]
forall a b. (a -> b) -> [a] -> [b]
List.map Predicate -> [SkTerm] -> 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
"P", Predicate
"Q"] :: [[SkTerm] -> Formula]
fm :: Formula
fm = (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"x" (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"y" (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"z" (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ [SkTerm] -> Formula
p[SkTerm
x,SkTerm
y] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. [SkTerm] -> Formula
p[SkTerm
y,SkTerm
z] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. [SkTerm] -> Formula
p[SkTerm
x,SkTerm
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
"x" (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"y" (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"z" (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ [SkTerm] -> Formula
q[SkTerm
x,SkTerm
y] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. [SkTerm] -> Formula
q[SkTerm
y,SkTerm
z] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. [SkTerm] -> Formula
q[SkTerm
x,SkTerm
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
"x" (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"y" (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ [SkTerm] -> Formula
q[SkTerm
x,SkTerm
y] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. [SkTerm] -> Formula
q[SkTerm
y,SkTerm
x]) 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
"x" (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"y" (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ [SkTerm] -> Formula
p[SkTerm
x,SkTerm
y] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. [SkTerm] -> Formula
q[SkTerm
x,SkTerm
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
"x" (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"y" (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ [SkTerm] -> Formula
p[SkTerm
x,SkTerm
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
"x" (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"y" (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ [SkTerm] -> Formula
q[SkTerm
x,SkTerm
y]) :: Formula
result :: Set (Failing Bool)
result = SkolemT Identity Function (Set (Failing Bool))
-> Set (Failing Bool)
forall function a.
IsFunction function =>
SkolemT Identity function a -> a
runSkolem (Formula -> SkolemT Identity Function (Set (Failing Bool))
forall fof atom term v function (m :: * -> *).
(IsFirstOrder fof, Unify Failing (atom, atom),
term ~ UTermOf (atom, atom), Match (atom, atom) v term,
HasSkolem function, Monad m, Ord fof, Pretty fof,
atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term,
v ~ VarOf fof, v ~ SVarOf function) =>
fof -> SkolemT m function (Set (Failing Bool))
presolution Formula
fm)
expected :: Set (Failing Bool)
expected = Failing Bool -> Set (Failing Bool)
forall a. a -> Set a
Set.singleton (Bool -> Failing Bool
forall a. a -> Failing a
Success Bool
True) in
Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> Set (Failing Bool) -> Set (Failing Bool) -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"los (p. 198)" Set (Failing Bool)
expected Set (Failing Bool)
result
testResolution :: Test
testResolution :: Test
testResolution = String -> Test -> Test
TestLabel String
"Resolution" ([Test] -> Test
TestList [Test
test01, Test
test02, Test
test03, Test
gilmore_1, Test
p1, Test
los])