{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Logic.ATP.FOL
( IsFirstOrder
, Interp
, holds
, holdsQuantified
, holdsAtom
, termval
, var
, fv, fva, fvt
, generalize
, subst, substq, asubst, tsubst, lsubst
, bool_interp
, mod_interp
, ApFormula, EqFormula
, testFOL
) where
import Data.Logic.ATP.Apply (ApAtom, HasApply(PredOf, TermOf, overterms, onterms), Predicate)
import Data.Logic.ATP.Equate ((.=.), EqAtom, foldEquate, HasEquate)
import Data.Logic.ATP.Formulas (fromBool, IsFormula(..))
import Data.Logic.ATP.Lib (setAny, tryApplyD, undefine, (|->))
import Data.Logic.ATP.Lit ((.~.), foldLiteral, JustLiteral)
import Data.Logic.ATP.Pretty (prettyShow)
import Data.Logic.ATP.Prop (BinOp(..), IsPropositional((.&.), (.|.), (.=>.), (.<=>.)))
import Data.Logic.ATP.Quantified (exists, foldQuantified, for_all, IsQuantified(VarOf), Quant((:!:), (:?:)), QFormula)
import Data.Logic.ATP.Term (FName, foldTerm, IsTerm(FunOf, TVarOf, vt, fApp), V, variant)
import Data.Map.Strict as Map (empty, fromList, insert, lookup, Map)
import Data.Maybe (fromMaybe)
import Data.Set as Set (difference, empty, fold, fromList, member, Set, singleton, union, unions)
import Data.String (IsString(fromString))
import Prelude hiding (pred)
import Test.HUnit
class (IsQuantified formula,
HasApply (AtomOf formula),
IsTerm (TermOf (AtomOf formula)),
VarOf formula ~ TVarOf (TermOf (AtomOf formula)))
=> IsFirstOrder formula
type ApFormula = QFormula V ApAtom
instance IsFirstOrder ApFormula
type EqFormula = QFormula V EqAtom
instance IsFirstOrder EqFormula
data Interp function predicate d
= Interp { forall function predicate d. Interp function predicate d -> [d]
domain :: [d]
, forall function predicate d.
Interp function predicate d -> function -> [d] -> d
funcApply :: function -> [d] -> d
, forall function predicate d.
Interp function predicate d -> predicate -> [d] -> Bool
predApply :: predicate -> [d] -> Bool
, forall function predicate d.
Interp function predicate d -> d -> d -> Bool
eqApply :: d -> d -> Bool }
class FiniteInterpretation a function predicate v dom where
holds :: Interp function predicate dom -> Map v dom -> a -> Bool
holdsQuantified :: forall formula function predicate dom.
(IsQuantified formula,
FiniteInterpretation (AtomOf formula) function predicate (VarOf formula) dom,
FiniteInterpretation formula function predicate (VarOf formula) dom) =>
Interp function predicate dom -> Map (VarOf formula) dom -> formula -> Bool
holdsQuantified :: forall formula function predicate dom.
(IsQuantified formula,
FiniteInterpretation
(AtomOf formula) function predicate (VarOf formula) dom,
FiniteInterpretation
formula function predicate (VarOf formula) dom) =>
Interp function predicate dom
-> Map (VarOf formula) dom -> formula -> Bool
holdsQuantified Interp function predicate dom
m Map (VarOf formula) dom
v formula
fm =
(Quant -> VarOf formula -> formula -> Bool)
-> (formula -> BinOp -> formula -> Bool)
-> (formula -> Bool)
-> (Bool -> Bool)
-> (AtomOf formula -> Bool)
-> formula
-> Bool
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 -> Bool
qu formula -> BinOp -> formula -> Bool
co formula -> Bool
ne Bool -> Bool
forall {p}. p -> p
tf AtomOf formula -> Bool
at formula
fm
where
qu :: Quant -> VarOf formula -> formula -> Bool
qu Quant
(:!:) VarOf formula
x formula
p = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((dom -> Bool) -> [dom] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (\dom
a -> Interp function predicate dom
-> Map (VarOf formula) dom -> formula -> Bool
forall a function predicate v dom.
FiniteInterpretation a function predicate v dom =>
Interp function predicate dom -> Map v dom -> a -> Bool
holds Interp function predicate dom
m (VarOf formula
-> dom -> Map (VarOf formula) dom -> Map (VarOf formula) dom
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert VarOf formula
x dom
a Map (VarOf formula) dom
v) formula
p) (Interp function predicate dom -> [dom]
forall function predicate d. Interp function predicate d -> [d]
domain Interp function predicate dom
m))
qu Quant
(:?:) VarOf formula
x formula
p = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or ((dom -> Bool) -> [dom] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (\dom
a -> Interp function predicate dom
-> Map (VarOf formula) dom -> formula -> Bool
forall a function predicate v dom.
FiniteInterpretation a function predicate v dom =>
Interp function predicate dom -> Map v dom -> a -> Bool
holds Interp function predicate dom
m (VarOf formula
-> dom -> Map (VarOf formula) dom -> Map (VarOf formula) dom
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert VarOf formula
x dom
a Map (VarOf formula) dom
v) formula
p) (Interp function predicate dom -> [dom]
forall function predicate d. Interp function predicate d -> [d]
domain Interp function predicate dom
m))
ne :: formula -> Bool
ne formula
p = Bool -> Bool
not (Interp function predicate dom
-> Map (VarOf formula) dom -> formula -> Bool
forall a function predicate v dom.
FiniteInterpretation a function predicate v dom =>
Interp function predicate dom -> Map v dom -> a -> Bool
holds Interp function predicate dom
m Map (VarOf formula) dom
v formula
p)
co :: formula -> BinOp -> formula -> Bool
co formula
p BinOp
(:&:) formula
q = (Interp function predicate dom
-> Map (VarOf formula) dom -> formula -> Bool
forall a function predicate v dom.
FiniteInterpretation a function predicate v dom =>
Interp function predicate dom -> Map v dom -> a -> Bool
holds Interp function predicate dom
m Map (VarOf formula) dom
v formula
p) Bool -> Bool -> Bool
&& (Interp function predicate dom
-> Map (VarOf formula) dom -> formula -> Bool
forall a function predicate v dom.
FiniteInterpretation a function predicate v dom =>
Interp function predicate dom -> Map v dom -> a -> Bool
holds Interp function predicate dom
m Map (VarOf formula) dom
v formula
q)
co formula
p BinOp
(:|:) formula
q = (Interp function predicate dom
-> Map (VarOf formula) dom -> formula -> Bool
forall a function predicate v dom.
FiniteInterpretation a function predicate v dom =>
Interp function predicate dom -> Map v dom -> a -> Bool
holds Interp function predicate dom
m Map (VarOf formula) dom
v formula
p) Bool -> Bool -> Bool
|| (Interp function predicate dom
-> Map (VarOf formula) dom -> formula -> Bool
forall a function predicate v dom.
FiniteInterpretation a function predicate v dom =>
Interp function predicate dom -> Map v dom -> a -> Bool
holds Interp function predicate dom
m Map (VarOf formula) dom
v formula
q)
co formula
p BinOp
(:=>:) formula
q = Bool -> Bool
not (Interp function predicate dom
-> Map (VarOf formula) dom -> formula -> Bool
forall a function predicate v dom.
FiniteInterpretation a function predicate v dom =>
Interp function predicate dom -> Map v dom -> a -> Bool
holds Interp function predicate dom
m Map (VarOf formula) dom
v formula
p) Bool -> Bool -> Bool
|| (Interp function predicate dom
-> Map (VarOf formula) dom -> formula -> Bool
forall a function predicate v dom.
FiniteInterpretation a function predicate v dom =>
Interp function predicate dom -> Map v dom -> a -> Bool
holds Interp function predicate dom
m Map (VarOf formula) dom
v formula
q)
co formula
p BinOp
(:<=>:) formula
q = (Interp function predicate dom
-> Map (VarOf formula) dom -> formula -> Bool
forall a function predicate v dom.
FiniteInterpretation a function predicate v dom =>
Interp function predicate dom -> Map v dom -> a -> Bool
holds Interp function predicate dom
m Map (VarOf formula) dom
v formula
p) Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== (Interp function predicate dom
-> Map (VarOf formula) dom -> formula -> Bool
forall a function predicate v dom.
FiniteInterpretation a function predicate v dom =>
Interp function predicate dom -> Map v dom -> a -> Bool
holds Interp function predicate dom
m Map (VarOf formula) dom
v formula
q)
tf :: p -> p
tf p
x = p
x
at :: AtomOf formula -> Bool
at = (Interp function predicate dom
-> Map (VarOf formula) dom -> AtomOf formula -> Bool
forall a function predicate v dom.
FiniteInterpretation a function predicate v dom =>
Interp function predicate dom -> Map v dom -> a -> Bool
holds Interp function predicate dom
m Map (VarOf formula) dom
v :: AtomOf formula -> Bool)
holdsAtom :: (HasEquate atom, IsTerm term, Eq dom,
term ~ TermOf atom, v ~ TVarOf term, function ~ FunOf term, predicate ~ PredOf atom) =>
Interp function predicate dom -> Map v dom -> atom -> Bool
holdsAtom :: forall atom term dom v function predicate.
(HasEquate atom, IsTerm term, Eq dom, term ~ TermOf atom,
v ~ TVarOf term, function ~ FunOf term, predicate ~ PredOf atom) =>
Interp function predicate dom -> Map v dom -> atom -> Bool
holdsAtom Interp function predicate dom
m Map v dom
v atom
at = (TermOf atom -> TermOf atom -> Bool)
-> (PredOf atom -> [TermOf atom] -> Bool) -> atom -> Bool
forall atom r.
HasEquate atom =>
(TermOf atom -> TermOf atom -> r)
-> (PredOf atom -> [TermOf atom] -> r) -> atom -> r
forall r.
(TermOf atom -> TermOf atom -> r)
-> (PredOf atom -> [TermOf atom] -> r) -> atom -> r
foldEquate (\TermOf atom
t1 TermOf atom
t2 -> Interp function predicate dom -> dom -> dom -> Bool
forall function predicate d.
Interp function predicate d -> d -> d -> Bool
eqApply Interp function predicate dom
m (Interp function predicate dom -> Map v dom -> term -> dom
forall term v function predicate r.
(IsTerm term, v ~ TVarOf term, function ~ FunOf term) =>
Interp function predicate r -> Map v r -> term -> r
termval Interp function predicate dom
m Map v dom
v term
TermOf atom
t1) (Interp function predicate dom -> Map v dom -> term -> dom
forall term v function predicate r.
(IsTerm term, v ~ TVarOf term, function ~ FunOf term) =>
Interp function predicate r -> Map v r -> term -> r
termval Interp function predicate dom
m Map v dom
v term
TermOf atom
t2))
(\PredOf atom
r [TermOf atom]
args -> Interp function predicate dom -> predicate -> [dom] -> Bool
forall function predicate d.
Interp function predicate d -> predicate -> [d] -> Bool
predApply Interp function predicate dom
m predicate
PredOf atom
r ((term -> dom) -> [term] -> [dom]
forall a b. (a -> b) -> [a] -> [b]
map (Interp function predicate dom -> Map v dom -> term -> dom
forall term v function predicate r.
(IsTerm term, v ~ TVarOf term, function ~ FunOf term) =>
Interp function predicate r -> Map v r -> term -> r
termval Interp function predicate dom
m Map v dom
v) [term]
[TermOf atom]
args)) atom
at
termval :: (IsTerm term, v ~ TVarOf term, function ~ FunOf term) => Interp function predicate r -> Map v r -> term -> r
termval :: forall term v function predicate r.
(IsTerm term, v ~ TVarOf term, function ~ FunOf term) =>
Interp function predicate r -> Map v r -> term -> r
termval Interp function predicate r
m Map v r
v term
tm =
(TVarOf term -> r) -> (FunOf term -> [term] -> r) -> term -> r
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 (\TVarOf term
x -> r -> Maybe r -> r
forall a. a -> Maybe a -> a
fromMaybe ([Char] -> r
forall a. HasCallStack => [Char] -> a
error ([Char]
"Undefined variable: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ v -> [Char]
forall a. Show a => a -> [Char]
show v
TVarOf term
x)) (v -> Map v r -> Maybe r
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup v
TVarOf term
x Map v r
v))
(\FunOf term
f [term]
args -> Interp function predicate r -> function -> [r] -> r
forall function predicate d.
Interp function predicate d -> function -> [d] -> d
funcApply Interp function predicate r
m function
FunOf term
f ((term -> r) -> [term] -> [r]
forall a b. (a -> b) -> [a] -> [b]
map (Interp function predicate r -> Map v r -> term -> r
forall term v function predicate r.
(IsTerm term, v ~ TVarOf term, function ~ FunOf term) =>
Interp function predicate r -> Map v r -> term -> r
termval Interp function predicate r
m Map v r
v) [term]
args)) term
tm
bool_interp :: Interp FName Predicate Bool
bool_interp :: Interp FName Predicate Bool
bool_interp =
[Bool]
-> (FName -> [Bool] -> Bool)
-> (Predicate -> [Bool] -> Bool)
-> (Bool -> Bool -> Bool)
-> Interp FName Predicate Bool
forall function predicate d.
[d]
-> (function -> [d] -> d)
-> (predicate -> [d] -> Bool)
-> (d -> d -> Bool)
-> Interp function predicate d
Interp [Bool
False, Bool
True] FName -> [Bool] -> Bool
forall {a}. (Eq a, IsString a, Show a) => a -> [Bool] -> Bool
func Predicate -> [Bool] -> Bool
forall {a} {p} {a}. Show a => a -> p -> a
pred Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
(==)
where
func :: a -> [Bool] -> Bool
func a
f [] | a
f a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== [Char] -> a
forall a. IsString a => [Char] -> a
fromString [Char]
"False" = Bool
False
func a
f [] | a
f a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== [Char] -> a
forall a. IsString a => [Char] -> a
fromString [Char]
"True" = Bool
True
func a
f [Bool
x,Bool
y] | a
f a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== [Char] -> a
forall a. IsString a => [Char] -> a
fromString [Char]
"+" = Bool
x Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
/= Bool
y
func a
f [Bool
x,Bool
y] | a
f a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== [Char] -> a
forall a. IsString a => [Char] -> a
fromString [Char]
"*" = Bool
x Bool -> Bool -> Bool
&& Bool
y
func a
f [Bool]
_ = [Char] -> Bool
forall a. HasCallStack => [Char] -> a
error ([Char]
"bool_interp - uninterpreted function: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
f)
pred :: a -> p -> a
pred a
p p
_ = [Char] -> a
forall a. HasCallStack => [Char] -> a
error ([Char]
"bool_interp - uninterpreted predicate: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
p)
mod_interp :: Int -> Interp FName Predicate Int
mod_interp :: Int -> Interp FName Predicate Int
mod_interp Int
n =
[Int]
-> (FName -> [Int] -> Int)
-> (Predicate -> [Int] -> Bool)
-> (Int -> Int -> Bool)
-> Interp FName Predicate Int
forall function predicate d.
[d]
-> (function -> [d] -> d)
-> (predicate -> [d] -> Bool)
-> (d -> d -> Bool)
-> Interp function predicate d
Interp [Int
0..(Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)] FName -> [Int] -> Int
func Predicate -> [Int] -> Bool
forall {a} {p} {a}. Show a => a -> p -> a
pred Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
(==)
where
func :: FName -> [Int] -> Int
func FName
f [] | FName
f FName -> FName -> Bool
forall a. Eq a => a -> a -> Bool
== [Char] -> FName
forall a. IsString a => [Char] -> a
fromString [Char]
"0" = Int
0
func FName
f [] | FName
f FName -> FName -> Bool
forall a. Eq a => a -> a -> Bool
== [Char] -> FName
forall a. IsString a => [Char] -> a
fromString [Char]
"1" = Int
1 Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
n
func FName
f [Int
x,Int
y] | FName
f FName -> FName -> Bool
forall a. Eq a => a -> a -> Bool
== [Char] -> FName
forall a. IsString a => [Char] -> a
fromString [Char]
"+" = (Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
y) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
n
func FName
f [Int
x,Int
y] | FName
f FName -> FName -> Bool
forall a. Eq a => a -> a -> Bool
== [Char] -> FName
forall a. IsString a => [Char] -> a
fromString [Char]
"*" = (Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
y) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
n
func FName
f [Int]
_ = [Char] -> Int
forall a. HasCallStack => [Char] -> a
error ([Char]
"mod_interp - uninterpreted function: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ FName -> [Char]
forall a. Show a => a -> [Char]
show FName
f)
pred :: a -> p -> a
pred a
p p
_ = [Char] -> a
forall a. HasCallStack => [Char] -> a
error ([Char]
"mod_interp - uninterpreted predicate: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
p)
instance Eq dom => FiniteInterpretation EqFormula FName Predicate V dom where holds :: Interp FName Predicate dom -> Map V dom -> EqFormula -> Bool
holds = Interp FName Predicate dom -> Map V dom -> EqFormula -> Bool
Interp FName Predicate dom
-> Map (VarOf EqFormula) dom -> EqFormula -> Bool
forall formula function predicate dom.
(IsQuantified formula,
FiniteInterpretation
(AtomOf formula) function predicate (VarOf formula) dom,
FiniteInterpretation
formula function predicate (VarOf formula) dom) =>
Interp function predicate dom
-> Map (VarOf formula) dom -> formula -> Bool
holdsQuantified
instance Eq dom => FiniteInterpretation EqAtom FName Predicate V dom where holds :: Interp FName Predicate dom
-> Map V dom -> FOL Predicate FTerm -> Bool
holds = Interp FName Predicate dom
-> Map V dom -> FOL Predicate FTerm -> Bool
forall atom term dom v function predicate.
(HasEquate atom, IsTerm term, Eq dom, term ~ TermOf atom,
v ~ TVarOf term, function ~ FunOf term, predicate ~ PredOf atom) =>
Interp function predicate dom -> Map v dom -> atom -> Bool
holdsAtom
test01 :: Test
test01 :: Test
test01 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ [Char] -> Bool -> Bool -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
[Char] -> a -> a -> Assertion
assertEqual [Char]
"holds bool test (p. 126)" Bool
expected Bool
input
where input :: Bool
input = Interp FName Predicate Bool -> Map V Bool -> EqFormula -> Bool
forall a function predicate v dom.
FiniteInterpretation a function predicate v dom =>
Interp function predicate dom -> Map v dom -> a -> Bool
holds Interp FName Predicate Bool
bool_interp (Map V Bool
forall k a. Map k a
Map.empty :: Map V Bool) (VarOf EqFormula -> EqFormula -> EqFormula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf EqFormula
"x" ((TVarOf FTerm -> FTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf FTerm
V
"x") TermOf (FOL Predicate FTerm)
-> TermOf (FOL Predicate FTerm) -> EqFormula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. (FunOf FTerm -> [FTerm] -> FTerm
forall term. IsTerm term => FunOf term -> [term] -> term
fApp FunOf FTerm
FName
"False" []) EqFormula -> EqFormula -> EqFormula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. (TVarOf FTerm -> FTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf FTerm
V
"x") TermOf (FOL Predicate FTerm)
-> TermOf (FOL Predicate FTerm) -> EqFormula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. (FunOf FTerm -> [FTerm] -> FTerm
forall term. IsTerm term => FunOf term -> [term] -> term
fApp FunOf FTerm
FName
"True" [])) :: EqFormula)
expected :: Bool
expected = Bool
True
test02 :: Test
test02 :: Test
test02 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ [Char] -> Bool -> Bool -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
[Char] -> a -> a -> Assertion
assertEqual [Char]
"holds mod test 1 (p. 126)" Bool
expected Bool
input
where input :: Bool
input = Interp FName Predicate Int -> Map V Int -> EqFormula -> Bool
forall a function predicate v dom.
FiniteInterpretation a function predicate v dom =>
Interp function predicate dom -> Map v dom -> a -> Bool
holds (Int -> Interp FName Predicate Int
mod_interp Int
2) (Map V Int
forall k a. Map k a
Map.empty :: Map V Int) (VarOf EqFormula -> EqFormula -> EqFormula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf EqFormula
"x" (TVarOf FTerm -> FTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf FTerm
V
"x" TermOf (FOL Predicate FTerm)
-> TermOf (FOL Predicate FTerm) -> EqFormula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. (FunOf FTerm -> [FTerm] -> FTerm
forall term. IsTerm term => FunOf term -> [term] -> term
fApp FunOf FTerm
FName
"0" []) EqFormula -> EqFormula -> EqFormula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. TVarOf FTerm -> FTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf FTerm
V
"x" TermOf (FOL Predicate FTerm)
-> TermOf (FOL Predicate FTerm) -> EqFormula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. (FunOf FTerm -> [FTerm] -> FTerm
forall term. IsTerm term => FunOf term -> [term] -> term
fApp FunOf FTerm
FName
"1" [])) :: EqFormula)
expected :: Bool
expected = Bool
True
test03 :: Test
test03 :: Test
test03 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ [Char] -> Bool -> Bool -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
[Char] -> a -> a -> Assertion
assertEqual [Char]
"holds mod test 2 (p. 126)" Bool
expected Bool
input
where input :: Bool
input = Interp FName Predicate Int -> Map V Int -> EqFormula -> Bool
forall a function predicate v dom.
FiniteInterpretation a function predicate v dom =>
Interp function predicate dom -> Map v dom -> a -> Bool
holds (Int -> Interp FName Predicate Int
mod_interp Int
3) (Map V Int
forall k a. Map k a
Map.empty :: Map V Int) (VarOf EqFormula -> EqFormula -> EqFormula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf EqFormula
"x" (TVarOf FTerm -> FTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf FTerm
V
"x" TermOf (FOL Predicate FTerm)
-> TermOf (FOL Predicate FTerm) -> EqFormula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. FunOf FTerm -> [FTerm] -> FTerm
forall term. IsTerm term => FunOf term -> [term] -> term
fApp FunOf FTerm
FName
"0" [] EqFormula -> EqFormula -> EqFormula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. TVarOf FTerm -> FTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf FTerm
V
"x" TermOf (FOL Predicate FTerm)
-> TermOf (FOL Predicate FTerm) -> EqFormula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. FunOf FTerm -> [FTerm] -> FTerm
forall term. IsTerm term => FunOf term -> [term] -> term
fApp FunOf FTerm
FName
"1" []) :: EqFormula)
expected :: Bool
expected = Bool
False
test04 :: Test
test04 :: Test
test04 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ [Char] -> [Int] -> [Int] -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
[Char] -> a -> a -> Assertion
assertEqual [Char]
"holds mod test 3 (p. 126)" [Int]
expected [Int]
input
where input :: [Int]
input = (Int -> Bool) -> [Int] -> [Int]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ Int
n -> Interp FName Predicate Int -> Map V Int -> EqFormula -> Bool
forall a function predicate v dom.
FiniteInterpretation a function predicate v dom =>
Interp function predicate dom -> Map v dom -> a -> Bool
holds (Int -> Interp FName Predicate Int
mod_interp Int
n) (Map V Int
forall k a. Map k a
Map.empty :: Map V Int) EqFormula
fm) [Int
1..Int
45]
where fm :: EqFormula
fm = VarOf EqFormula -> EqFormula -> EqFormula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf EqFormula
"x" (EqFormula -> EqFormula
forall formula. IsLiteral formula => formula -> formula
(.~.) (TVarOf FTerm -> FTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf FTerm
V
"x" TermOf (FOL Predicate FTerm)
-> TermOf (FOL Predicate FTerm) -> EqFormula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. FunOf FTerm -> [FTerm] -> FTerm
forall term. IsTerm term => FunOf term -> [term] -> term
fApp FunOf FTerm
FName
"0" []) EqFormula -> EqFormula -> EqFormula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. VarOf EqFormula -> EqFormula -> EqFormula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists V
VarOf EqFormula
"y" (FunOf FTerm -> [FTerm] -> FTerm
forall term. IsTerm term => FunOf term -> [term] -> term
fApp FunOf FTerm
FName
"*" [TVarOf FTerm -> FTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf FTerm
V
"x", TVarOf FTerm -> FTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf FTerm
V
"y"] TermOf (FOL Predicate FTerm)
-> TermOf (FOL Predicate FTerm) -> EqFormula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. FunOf FTerm -> [FTerm] -> FTerm
forall term. IsTerm term => FunOf term -> [term] -> term
fApp FunOf FTerm
FName
"1" [])) :: EqFormula
expected :: [Int]
expected = [Int
1,Int
2,Int
3,Int
5,Int
7,Int
11,Int
13,Int
17,Int
19,Int
23,Int
29,Int
31,Int
37,Int
41,Int
43]
test05 :: Test
test05 :: Test
test05 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ [Char] -> Bool -> Bool -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
[Char] -> a -> a -> Assertion
assertEqual [Char]
"holds mod test 4 (p. 129)" Bool
expected Bool
input
where input :: Bool
input = Interp FName Predicate Int -> Map V Int -> EqFormula -> Bool
forall a function predicate v dom.
FiniteInterpretation a function predicate v dom =>
Interp function predicate dom -> Map v dom -> a -> Bool
holds (Int -> Interp FName Predicate Int
mod_interp Int
3) (Map V Int
forall k a. Map k a
Map.empty :: Map V Int) ((VarOf EqFormula -> EqFormula -> EqFormula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf EqFormula
"x" (TVarOf FTerm -> FTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf FTerm
V
"x" TermOf (FOL Predicate FTerm)
-> TermOf (FOL Predicate FTerm) -> EqFormula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. FunOf FTerm -> [FTerm] -> FTerm
forall term. IsTerm term => FunOf term -> [term] -> term
fApp FunOf FTerm
FName
"0" [])) EqFormula -> EqFormula -> EqFormula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. FunOf FTerm -> [FTerm] -> FTerm
forall term. IsTerm term => FunOf term -> [term] -> term
fApp FunOf FTerm
FName
"1" [] TermOf (FOL Predicate FTerm)
-> TermOf (FOL Predicate FTerm) -> EqFormula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. FunOf FTerm -> [FTerm] -> FTerm
forall term. IsTerm term => FunOf term -> [term] -> term
fApp FunOf FTerm
FName
"0" [] :: EqFormula)
expected :: Bool
expected = Bool
True
test06 :: Test
test06 :: Test
test06 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ [Char] -> Bool -> Bool -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
[Char] -> a -> a -> Assertion
assertEqual [Char]
"holds mod test 5 (p. 129)" Bool
expected Bool
input
where input :: Bool
input = Interp FName Predicate Int -> Map V Int -> EqFormula -> Bool
forall a function predicate v dom.
FiniteInterpretation a function predicate v dom =>
Interp function predicate dom -> Map v dom -> a -> Bool
holds (Int -> Interp FName Predicate Int
mod_interp Int
3) (Map V Int
forall k a. Map k a
Map.empty :: Map V Int) (VarOf EqFormula -> EqFormula -> EqFormula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf EqFormula
"x" (TVarOf FTerm -> FTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf FTerm
V
"x" TermOf (FOL Predicate FTerm)
-> TermOf (FOL Predicate FTerm) -> EqFormula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. FunOf FTerm -> [FTerm] -> FTerm
forall term. IsTerm term => FunOf term -> [term] -> term
fApp FunOf FTerm
FName
"0" [] EqFormula -> EqFormula -> EqFormula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. FunOf FTerm -> [FTerm] -> FTerm
forall term. IsTerm term => FunOf term -> [term] -> term
fApp FunOf FTerm
FName
"1" [] TermOf (FOL Predicate FTerm)
-> TermOf (FOL Predicate FTerm) -> EqFormula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. FunOf FTerm -> [FTerm] -> FTerm
forall term. IsTerm term => FunOf term -> [term] -> term
fApp FunOf FTerm
FName
"0" []) :: EqFormula)
expected :: Bool
expected = Bool
False
fv :: (IsFirstOrder formula, v ~ VarOf formula) => formula -> Set v
fv :: forall formula v.
(IsFirstOrder formula, v ~ VarOf formula) =>
formula -> Set v
fv formula
fm =
(Quant -> VarOf formula -> formula -> Set v)
-> (formula -> BinOp -> formula -> Set v)
-> (formula -> Set v)
-> (Bool -> Set v)
-> (AtomOf formula -> Set v)
-> formula
-> Set v
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 -> Set v
Quant -> VarOf formula -> formula -> Set (VarOf formula)
forall {formula} {p}.
IsFirstOrder formula =>
p -> VarOf formula -> formula -> Set (VarOf formula)
qu formula -> BinOp -> formula -> Set v
formula -> BinOp -> formula -> Set (VarOf formula)
forall {formula} {formula} {p}.
(TVarOf (TermOf (AtomOf formula))
~ TVarOf (TermOf (AtomOf formula)),
VarOf formula ~ TVarOf (TermOf (AtomOf formula)),
IsFirstOrder formula, IsFirstOrder formula) =>
formula -> p -> formula -> Set (VarOf formula)
co formula -> Set v
formula -> Set (VarOf formula)
forall {formula}.
IsFirstOrder formula =>
formula -> Set (VarOf formula)
ne Bool -> Set v
forall {p} {a}. p -> Set a
tf AtomOf formula -> Set v
AtomOf formula -> Set (TVarOf (TermOf (AtomOf formula)))
at formula
fm
where
qu :: p -> VarOf formula -> formula -> Set (VarOf formula)
qu p
_ VarOf formula
x formula
p = Set (VarOf formula) -> Set (VarOf formula) -> Set (VarOf formula)
forall a. Ord a => Set a -> Set a -> Set a
difference (formula -> Set (VarOf formula)
forall formula v.
(IsFirstOrder formula, v ~ VarOf formula) =>
formula -> Set v
fv formula
p) (VarOf formula -> Set (VarOf formula)
forall a. a -> Set a
singleton VarOf formula
x)
ne :: formula -> Set (VarOf formula)
ne formula
p = formula -> Set (VarOf formula)
forall formula v.
(IsFirstOrder formula, v ~ VarOf formula) =>
formula -> Set v
fv formula
p
co :: formula -> p -> formula -> Set (VarOf formula)
co formula
p p
_ formula
q = Set (VarOf formula) -> Set (VarOf formula) -> Set (VarOf formula)
forall a. Ord a => Set a -> Set a -> Set a
union (formula -> Set (VarOf formula)
forall formula v.
(IsFirstOrder formula, v ~ VarOf formula) =>
formula -> Set v
fv formula
p) (formula -> Set (VarOf formula)
forall formula v.
(IsFirstOrder formula, v ~ VarOf formula) =>
formula -> Set v
fv formula
q)
tf :: p -> Set a
tf p
_ = Set a
forall a. Set a
Set.empty
at :: AtomOf formula -> Set (TVarOf (TermOf (AtomOf formula)))
at = AtomOf formula -> Set (TVarOf (TermOf (AtomOf formula)))
forall atom term v.
(HasApply atom, IsTerm term, term ~ TermOf atom,
v ~ TVarOf term) =>
atom -> Set v
fva
var :: (IsFormula formula, HasApply atom,
atom ~ AtomOf formula, term ~ TermOf atom, v ~ TVarOf term) =>
formula -> Set v
var :: forall formula atom term v.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula,
term ~ TermOf atom, v ~ TVarOf term) =>
formula -> Set v
var formula
fm = (AtomOf formula -> Set v -> Set v) -> formula -> Set v -> Set v
forall formula r.
IsFormula formula =>
(AtomOf formula -> r -> r) -> formula -> r -> r
forall r. (AtomOf formula -> r -> r) -> formula -> r -> r
overatoms (\AtomOf formula
a Set v
s -> Set v -> Set v -> Set v
forall a. Ord a => Set a -> Set a -> Set a
Set.union (atom -> Set v
forall atom term v.
(HasApply atom, IsTerm term, term ~ TermOf atom,
v ~ TVarOf term) =>
atom -> Set v
fva atom
AtomOf formula
a) Set v
s) formula
fm Set v
forall a. Monoid a => a
mempty
fva :: (HasApply atom, IsTerm term, term ~ TermOf atom, v ~ TVarOf term) => atom -> Set v
fva :: forall atom term v.
(HasApply atom, IsTerm term, term ~ TermOf atom,
v ~ TVarOf term) =>
atom -> Set v
fva = (TermOf atom -> Set v -> Set v) -> Set v -> atom -> Set v
forall atom r.
HasApply atom =>
(TermOf atom -> r -> r) -> r -> atom -> r
forall r. (TermOf atom -> r -> r) -> r -> atom -> r
overterms (\TermOf atom
t Set v
s -> Set v -> Set v -> Set v
forall a. Ord a => Set a -> Set a -> Set a
Set.union (term -> Set v
forall term v. (IsTerm term, v ~ TVarOf term) => term -> Set v
fvt term
TermOf atom
t) Set v
s) Set v
forall a. Monoid a => a
mempty
fvt :: (IsTerm term, v ~ TVarOf term) => term -> Set v
fvt :: forall term v. (IsTerm term, v ~ TVarOf term) => term -> Set v
fvt term
tm = (TVarOf term -> Set v)
-> (FunOf term -> [term] -> Set v) -> term -> Set v
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 -> Set v
TVarOf term -> Set v
forall a. a -> Set a
singleton (\FunOf term
_ [term]
args -> [Set v] -> Set v
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
unions ((term -> Set v) -> [term] -> [Set v]
forall a b. (a -> b) -> [a] -> [b]
map term -> Set v
forall term v. (IsTerm term, v ~ TVarOf term) => term -> Set v
fvt [term]
args)) term
tm
generalize :: IsFirstOrder formula => formula -> formula
generalize :: forall formula. IsFirstOrder formula => formula -> formula
generalize formula
fm = (TVarOf (TermOf (AtomOf formula)) -> formula -> formula)
-> formula -> Set (TVarOf (TermOf (AtomOf formula))) -> formula
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold TVarOf (TermOf (AtomOf formula)) -> formula -> formula
VarOf formula -> formula -> formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all formula
fm (formula -> Set (TVarOf (TermOf (AtomOf formula)))
forall formula v.
(IsFirstOrder formula, v ~ VarOf formula) =>
formula -> Set v
fv formula
fm)
test07 :: Test
test07 :: Test
test07 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ [Char] -> V -> V -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
[Char] -> a -> a -> Assertion
assertEqual [Char]
"variant 1 (p. 133)" V
expected V
input
where input :: V
input = V -> Set V -> V
forall v. IsVariable v => v -> Set v -> v
variant V
"x" ([V] -> Set V
forall a. Ord a => [a] -> Set a
Set.fromList [V
"y", V
"z"]) :: V
expected :: V
expected = V
"x"
test08 :: Test
test08 :: Test
test08 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ [Char] -> V -> V -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
[Char] -> a -> a -> Assertion
assertEqual [Char]
"variant 2 (p. 133)" V
expected V
input
where input :: V
input = V -> Set V -> V
forall v. IsVariable v => v -> Set v -> v
variant V
"x" ([V] -> Set V
forall a. Ord a => [a] -> Set a
Set.fromList [V
"x", V
"y"]) :: V
expected :: V
expected = V
"x'"
test09 :: Test
test09 :: Test
test09 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ [Char] -> V -> V -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
[Char] -> a -> a -> Assertion
assertEqual [Char]
"variant 3 (p. 133)" V
expected V
input
where input :: V
input = V -> Set V -> V
forall v. IsVariable v => v -> Set v -> v
variant V
"x" ([V] -> Set V
forall a. Ord a => [a] -> Set a
Set.fromList [V
"x", V
"x'"]) :: V
expected :: V
expected = V
"x''"
subst :: (IsFirstOrder formula, term ~ TermOf (AtomOf formula), v ~ VarOf formula) => Map v term -> formula -> formula
subst :: forall formula term v.
(IsFirstOrder formula, term ~ TermOf (AtomOf formula),
v ~ VarOf formula) =>
Map v term -> formula -> formula
subst Map v term
subfn 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 -> v -> formula -> formula
Quant -> VarOf formula -> formula -> formula
qu formula -> BinOp -> formula -> formula
co formula -> formula
ne Bool -> formula
forall {formula}. IsFormula formula => Bool -> formula
tf AtomOf formula -> formula
at formula
fm
where
qu :: Quant -> v -> formula -> formula
qu Quant
(:!:) v
x formula
p = Map v term -> (v -> formula -> formula) -> v -> formula -> formula
forall formula v term.
(IsFirstOrder formula, v ~ VarOf formula,
term ~ TermOf (AtomOf formula)) =>
Map v term -> (v -> formula -> formula) -> v -> formula -> formula
substq Map v term
subfn v -> formula -> formula
VarOf formula -> formula -> formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all v
x formula
p
qu Quant
(:?:) v
x formula
p = Map v term -> (v -> formula -> formula) -> v -> formula -> formula
forall formula v term.
(IsFirstOrder formula, v ~ VarOf formula,
term ~ TermOf (AtomOf formula)) =>
Map v term -> (v -> formula -> formula) -> v -> formula -> formula
substq Map v term
subfn v -> formula -> formula
VarOf formula -> formula -> formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists v
x formula
p
ne :: formula -> formula
ne formula
p = formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) (Map v term -> formula -> formula
forall formula term v.
(IsFirstOrder formula, term ~ TermOf (AtomOf formula),
v ~ VarOf formula) =>
Map v term -> formula -> formula
subst Map v term
subfn formula
p)
co :: formula -> BinOp -> formula -> formula
co formula
p BinOp
(:&:) formula
q = (Map v term -> formula -> formula
forall formula term v.
(IsFirstOrder formula, term ~ TermOf (AtomOf formula),
v ~ VarOf formula) =>
Map v term -> formula -> formula
subst Map v term
subfn formula
p) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (Map v term -> formula -> formula
forall formula term v.
(IsFirstOrder formula, term ~ TermOf (AtomOf formula),
v ~ VarOf formula) =>
Map v term -> formula -> formula
subst Map v term
subfn formula
q)
co formula
p BinOp
(:|:) formula
q = (Map v term -> formula -> formula
forall formula term v.
(IsFirstOrder formula, term ~ TermOf (AtomOf formula),
v ~ VarOf formula) =>
Map v term -> formula -> formula
subst Map v term
subfn formula
p) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. (Map v term -> formula -> formula
forall formula term v.
(IsFirstOrder formula, term ~ TermOf (AtomOf formula),
v ~ VarOf formula) =>
Map v term -> formula -> formula
subst Map v term
subfn formula
q)
co formula
p BinOp
(:=>:) formula
q = (Map v term -> formula -> formula
forall formula term v.
(IsFirstOrder formula, term ~ TermOf (AtomOf formula),
v ~ VarOf formula) =>
Map v term -> formula -> formula
subst Map v term
subfn formula
p) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. (Map v term -> formula -> formula
forall formula term v.
(IsFirstOrder formula, term ~ TermOf (AtomOf formula),
v ~ VarOf formula) =>
Map v term -> formula -> formula
subst Map v term
subfn formula
q)
co formula
p BinOp
(:<=>:) formula
q = (Map v term -> formula -> formula
forall formula term v.
(IsFirstOrder formula, term ~ TermOf (AtomOf formula),
v ~ VarOf formula) =>
Map v term -> formula -> formula
subst Map v term
subfn formula
p) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. (Map v term -> formula -> formula
forall formula term v.
(IsFirstOrder formula, term ~ TermOf (AtomOf formula),
v ~ VarOf formula) =>
Map v term -> formula -> formula
subst Map v term
subfn formula
q)
tf :: Bool -> formula
tf Bool
False = formula
forall formula. IsFormula formula => formula
false
tf Bool
True = formula
forall formula. IsFormula formula => formula
true
at :: AtomOf formula -> formula
at = AtomOf formula -> formula
forall formula. IsFormula formula => AtomOf formula -> formula
atomic (AtomOf formula -> formula)
-> (AtomOf formula -> AtomOf formula) -> AtomOf formula -> formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map v term -> AtomOf formula -> AtomOf formula
forall atom term v.
(HasApply atom, IsTerm term, term ~ TermOf atom,
v ~ TVarOf term) =>
Map v term -> atom -> atom
asubst Map v term
subfn
tsubst :: (IsTerm term, v ~ TVarOf term) => Map v term -> term -> term
tsubst :: forall term v.
(IsTerm term, v ~ TVarOf term) =>
Map v term -> term -> term
tsubst Map v term
sfn term
tm =
(TVarOf term -> term)
-> (FunOf term -> [term] -> term) -> term -> 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 (\TVarOf term
x -> term -> Maybe term -> term
forall a. a -> Maybe a -> a
fromMaybe term
tm (v -> Map v term -> Maybe term
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup v
TVarOf term
x Map v term
sfn))
(\FunOf term
f [term]
args -> FunOf term -> [term] -> term
forall term. IsTerm term => FunOf term -> [term] -> term
fApp FunOf term
f ((term -> term) -> [term] -> [term]
forall a b. (a -> b) -> [a] -> [b]
map (Map v term -> term -> term
forall term v.
(IsTerm term, v ~ TVarOf term) =>
Map v term -> term -> term
tsubst Map v term
sfn) [term]
args))
term
tm
lsubst :: (JustLiteral lit, HasApply atom, IsTerm term,
atom ~ AtomOf lit,
term ~ TermOf atom,
v ~ TVarOf term) =>
Map v term -> lit -> lit
lsubst :: 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 term
subfn lit
fm =
(lit -> lit) -> (Bool -> lit) -> (AtomOf lit -> lit) -> lit -> lit
forall lit r.
JustLiteral lit =>
(lit -> r) -> (Bool -> r) -> (AtomOf lit -> r) -> lit -> r
foldLiteral lit -> lit
ne Bool -> lit
forall {formula}. IsFormula formula => Bool -> formula
fromBool atom -> lit
AtomOf lit -> lit
at lit
fm
where
ne :: lit -> lit
ne lit
p = lit -> lit
forall formula. IsLiteral formula => formula -> formula
(.~.) (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 Map v term
subfn lit
p)
at :: atom -> lit
at = atom -> lit
AtomOf lit -> lit
forall formula. IsFormula formula => AtomOf formula -> formula
atomic (atom -> lit) -> (atom -> atom) -> atom -> lit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map v term -> atom -> atom
forall atom term v.
(HasApply atom, IsTerm term, term ~ TermOf atom,
v ~ TVarOf term) =>
Map v term -> atom -> atom
asubst Map v term
subfn
asubst :: (HasApply atom, IsTerm term, term ~ TermOf atom, v ~ TVarOf term) => Map v term -> atom -> atom
asubst :: forall atom term v.
(HasApply atom, IsTerm term, term ~ TermOf atom,
v ~ TVarOf term) =>
Map v term -> atom -> atom
asubst Map v term
sfn atom
a = (TermOf atom -> TermOf atom) -> atom -> atom
forall atom.
HasApply atom =>
(TermOf atom -> TermOf atom) -> atom -> atom
onterms (Map v term -> term -> term
forall term v.
(IsTerm term, v ~ TVarOf term) =>
Map v term -> term -> term
tsubst Map v term
sfn) atom
a
substq :: (IsFirstOrder formula, v ~ VarOf formula, term ~ TermOf (AtomOf formula)) =>
Map v term -> (v -> formula -> formula) -> v -> formula -> formula
substq :: forall formula v term.
(IsFirstOrder formula, v ~ VarOf formula,
term ~ TermOf (AtomOf formula)) =>
Map v term -> (v -> formula -> formula) -> v -> formula -> formula
substq Map v term
subfn v -> formula -> formula
qu v
x formula
p =
let x' :: v
x' = if (v -> Bool) -> Set v -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
setAny (\v
y -> v -> Set v -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member v
x (term -> Set v
forall term v. (IsTerm term, v ~ TVarOf term) => term -> Set v
fvt(Map v term -> v -> term -> term
forall k a. Ord k => Map k a -> k -> a -> a
tryApplyD Map v term
subfn v
y (TVarOf term -> term
forall term. IsTerm term => TVarOf term -> term
vt v
TVarOf term
y))))
(Set v -> Set v -> Set v
forall a. Ord a => Set a -> Set a -> Set a
difference (formula -> Set v
forall formula v.
(IsFirstOrder formula, v ~ VarOf formula) =>
formula -> Set v
fv formula
p) (v -> Set v
forall a. a -> Set a
singleton v
x))
then 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 (Map v term -> formula -> formula
forall formula term v.
(IsFirstOrder formula, term ~ TermOf (AtomOf formula),
v ~ VarOf formula) =>
Map v term -> formula -> formula
subst (v -> Map v term -> Map v term
forall k a. Ord k => k -> Map k a -> Map k a
undefine v
x Map v term
subfn) formula
p)) else v
x in
v -> formula -> formula
qu v
x' (Map v term -> formula -> formula
forall formula term v.
(IsFirstOrder formula, term ~ TermOf (AtomOf formula),
v ~ VarOf formula) =>
Map v term -> formula -> formula
subst ((v
x v -> term -> Map v term -> Map v term
forall k a. Ord k => k -> a -> Map k a -> Map k a
|-> TVarOf term -> term
forall term. IsTerm term => TVarOf term -> term
vt v
TVarOf term
x') Map v term
subfn) formula
p)
test10 :: Test
test10 :: Test
test10 =
let [FTerm
x, FTerm
x', FTerm
y] = [TVarOf FTerm -> FTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf FTerm
"x", TVarOf FTerm -> FTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf FTerm
"x'", TVarOf FTerm -> FTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf FTerm
"y"]
fm :: EqFormula
fm = VarOf EqFormula -> EqFormula -> EqFormula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf EqFormula
"x" ((FTerm
TermOf (FOL Predicate FTerm)
x TermOf (FOL Predicate FTerm)
-> TermOf (FOL Predicate FTerm) -> EqFormula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. FTerm
TermOf (FOL Predicate FTerm)
y)) :: EqFormula
expected :: EqFormula
expected = VarOf EqFormula -> EqFormula -> EqFormula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf EqFormula
"x'" (FTerm
TermOf (FOL Predicate FTerm)
x' TermOf (FOL Predicate FTerm)
-> TermOf (FOL Predicate FTerm) -> EqFormula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. FTerm
TermOf (FOL Predicate FTerm)
x) :: EqFormula in
Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ [Char] -> EqFormula -> EqFormula -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
[Char] -> a -> a -> Assertion
assertEqual ([Char]
"subst (\"y\" |=> Var \"x\") " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ EqFormula -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow EqFormula
fm [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" (p. 134)")
EqFormula
expected
(Map V FTerm -> EqFormula -> EqFormula
forall formula term v.
(IsFirstOrder formula, term ~ TermOf (AtomOf formula),
v ~ VarOf formula) =>
Map v term -> formula -> formula
subst ([(V, FTerm)] -> Map V FTerm
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(V
"y", FTerm
x)]) EqFormula
fm)
test11 :: Test
test11 :: Test
test11 =
let [FTerm
x, FTerm
x', FTerm
x'', FTerm
y] = [TVarOf FTerm -> FTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf FTerm
"x", TVarOf FTerm -> FTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf FTerm
"x'", TVarOf FTerm -> FTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf FTerm
"x''", TVarOf FTerm -> FTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf FTerm
"y"]
fm :: EqFormula
fm = (VarOf EqFormula -> EqFormula -> EqFormula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf EqFormula
"x" (VarOf EqFormula -> EqFormula -> EqFormula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf EqFormula
"x'" ((FTerm
TermOf (FOL Predicate FTerm)
x TermOf (FOL Predicate FTerm)
-> TermOf (FOL Predicate FTerm) -> EqFormula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. FTerm
TermOf (FOL Predicate FTerm)
y) EqFormula -> EqFormula -> EqFormula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. (FTerm
TermOf (FOL Predicate FTerm)
x TermOf (FOL Predicate FTerm)
-> TermOf (FOL Predicate FTerm) -> EqFormula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. FTerm
TermOf (FOL Predicate FTerm)
x')))) :: EqFormula
expected :: EqFormula
expected = VarOf EqFormula -> EqFormula -> EqFormula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf EqFormula
"x'" (VarOf EqFormula -> EqFormula -> EqFormula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf EqFormula
"x''" ((FTerm
TermOf (FOL Predicate FTerm)
x' TermOf (FOL Predicate FTerm)
-> TermOf (FOL Predicate FTerm) -> EqFormula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. FTerm
TermOf (FOL Predicate FTerm)
x) EqFormula -> EqFormula -> EqFormula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. ((FTerm
TermOf (FOL Predicate FTerm)
x' TermOf (FOL Predicate FTerm)
-> TermOf (FOL Predicate FTerm) -> EqFormula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. FTerm
TermOf (FOL Predicate FTerm)
x'')))) :: EqFormula in
Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ [Char] -> EqFormula -> EqFormula -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
[Char] -> a -> a -> Assertion
assertEqual ([Char]
"subst (\"y\" |=> Var \"x\") " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ EqFormula -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow EqFormula
fm [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" (p. 134)")
EqFormula
expected
(Map V FTerm -> EqFormula -> EqFormula
forall formula term v.
(IsFirstOrder formula, term ~ TermOf (AtomOf formula),
v ~ VarOf formula) =>
Map v term -> formula -> formula
subst ([(V, FTerm)] -> Map V FTerm
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(V
"y", FTerm
x)]) EqFormula
fm)
testFOL :: Test
testFOL :: Test
testFOL = [Char] -> Test -> Test
TestLabel [Char]
"FOL" ([Test] -> Test
TestList [Test
test01, Test
test02, Test
test03, Test
test04,
Test
test05, Test
test06, Test
test07, Test
test08, Test
test09,
Test
test10, Test
test11])