module Djinn.LJT (
module Djinn.LJTFormula,
provable,
prove,
Proof,
MoreSolutions
) where
import Control.Applicative (Applicative, Alternative, pure, (<*>), empty, (<|>))
import Control.Monad
import Data.List (partition)
import Debug.Trace
import Djinn.LJTFormula
mtrace :: String -> a -> a
mtrace :: forall a. String -> a -> a
mtrace String
m a
x = if Bool
debug then String -> a -> a
forall a. String -> a -> a
trace String
m a
x else a
x
wrapM :: (Show a, Show b, Monad m) => String -> a -> m b -> m b
wrapM :: forall a b (m :: * -> *).
(Show a, Show b, Monad m) =>
String -> a -> m b -> m b
wrapM String
fun a
args m b
mret = do
() <- String -> m () -> m ()
forall a. String -> a -> a
mtrace (String
fun String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
args) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
b
ret <- m b
mret
() <- String -> m () -> m ()
forall a. String -> a -> a
mtrace (String
fun String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" returns: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ b -> String
forall a. Show a => a -> String
show b
ret) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
b -> m b
forall (m :: * -> *) a. Monad m => a -> m a
return b
ret
debug :: Bool
debug :: Bool
debug = Bool
False
type MoreSolutions = Bool
provable :: Formula -> Bool
provable :: Goal -> Bool
provable Goal
a = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Proof] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Proof] -> Bool) -> [Proof] -> Bool
forall a b. (a -> b) -> a -> b
$ Bool -> [(Symbol, Goal)] -> Goal -> [Proof]
prove Bool
False [] Goal
a
prove :: MoreSolutions -> [(Symbol, Formula)] -> Formula -> [Proof]
prove :: Bool -> [(Symbol, Goal)] -> Goal -> [Proof]
prove Bool
more [(Symbol, Goal)]
env Goal
a = P Proof -> [Proof]
forall a. P a -> [a]
runP (P Proof -> [Proof]) -> P Proof -> [Proof]
forall a b. (a -> b) -> a -> b
$ Bool -> [(Symbol, Goal)] -> Goal -> P Proof
redtop Bool
more [(Symbol, Goal)]
env Goal
a
redtop :: MoreSolutions -> [(Symbol, Formula)] -> Formula -> P Proof
redtop :: Bool -> [(Symbol, Goal)] -> Goal -> P Proof
redtop Bool
more [(Symbol, Goal)]
ifs Goal
a = do
let form :: Goal
form = (Goal -> Goal -> Goal) -> Goal -> [Goal] -> Goal
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Goal -> Goal -> Goal
(:->) Goal
a (((Symbol, Goal) -> Goal) -> [(Symbol, Goal)] -> [Goal]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol, Goal) -> Goal
forall a b. (a, b) -> b
snd [(Symbol, Goal)]
ifs)
Proof
p <- Bool
-> Antecedents -> AtomImps -> NestImps -> AtomFs -> Goal -> P Proof
redant Bool
more [] [] [] [] Goal
form
Proof -> P Proof
nf ((Proof -> Proof -> Proof) -> Proof -> [Proof] -> Proof
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Proof -> Proof -> Proof
Apply Proof
p (((Symbol, Goal) -> Proof) -> [(Symbol, Goal)] -> [Proof]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol -> Proof
Var (Symbol -> Proof)
-> ((Symbol, Goal) -> Symbol) -> (Symbol, Goal) -> Proof
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, Goal) -> Symbol
forall a b. (a, b) -> a
fst) [(Symbol, Goal)]
ifs))
type Proof = Term
subst :: Term -> Symbol -> Term -> P Term
subst :: Proof -> Symbol -> Proof -> P Proof
subst Proof
b Symbol
x Proof
term = Proof -> P Proof
sub Proof
term
where sub :: Proof -> P Proof
sub t :: Proof
t@(Var Symbol
s') = if Symbol
x Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
s' then [(Symbol, Symbol)] -> Proof -> P Proof
copy [] Proof
b else Proof -> P Proof
forall (m :: * -> *) a. Monad m => a -> m a
return Proof
t
sub (Lam Symbol
s Proof
t) = (Proof -> Proof) -> P Proof -> P Proof
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Symbol -> Proof -> Proof
Lam Symbol
s) (Proof -> P Proof
sub Proof
t)
sub (Apply Proof
t1 Proof
t2) = (Proof -> Proof -> Proof) -> P Proof -> P Proof -> P Proof
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Proof -> Proof -> Proof
Apply (Proof -> P Proof
sub Proof
t1) (Proof -> P Proof
sub Proof
t2)
sub Proof
t = Proof -> P Proof
forall (m :: * -> *) a. Monad m => a -> m a
return Proof
t
copy :: [(Symbol, Symbol)] -> Term -> P Term
copy :: [(Symbol, Symbol)] -> Proof -> P Proof
copy [(Symbol, Symbol)]
r (Var Symbol
s) = Proof -> P Proof
forall (m :: * -> *) a. Monad m => a -> m a
return (Proof -> P Proof) -> Proof -> P Proof
forall a b. (a -> b) -> a -> b
$ Symbol -> Proof
Var (Symbol -> Proof) -> Symbol -> Proof
forall a b. (a -> b) -> a -> b
$ Symbol -> (Symbol -> Symbol) -> Maybe Symbol -> Symbol
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Symbol
s Symbol -> Symbol
forall a. a -> a
id (Maybe Symbol -> Symbol) -> Maybe Symbol -> Symbol
forall a b. (a -> b) -> a -> b
$ Symbol -> [(Symbol, Symbol)] -> Maybe Symbol
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Symbol
s [(Symbol, Symbol)]
r
copy [(Symbol, Symbol)]
r (Lam Symbol
s Proof
t) = do
Symbol
s' <- String -> P Symbol
newSym String
"c"
(Proof -> Proof) -> P Proof -> P Proof
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Symbol -> Proof -> Proof
Lam Symbol
s') (P Proof -> P Proof) -> P Proof -> P Proof
forall a b. (a -> b) -> a -> b
$ [(Symbol, Symbol)] -> Proof -> P Proof
copy ((Symbol
s, Symbol
s')(Symbol, Symbol) -> [(Symbol, Symbol)] -> [(Symbol, Symbol)]
forall a. a -> [a] -> [a]
:[(Symbol, Symbol)]
r) Proof
t
copy [(Symbol, Symbol)]
r (Apply Proof
t1 Proof
t2) = (Proof -> Proof -> Proof) -> P Proof -> P Proof -> P Proof
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Proof -> Proof -> Proof
Apply ([(Symbol, Symbol)] -> Proof -> P Proof
copy [(Symbol, Symbol)]
r Proof
t1) ([(Symbol, Symbol)] -> Proof -> P Proof
copy [(Symbol, Symbol)]
r Proof
t2)
copy [(Symbol, Symbol)]
_r Proof
t = Proof -> P Proof
forall (m :: * -> *) a. Monad m => a -> m a
return Proof
t
applyAtom :: Term -> Term -> Term
applyAtom :: Proof -> Proof -> Proof
applyAtom Proof
f Proof
a = Proof -> Proof -> Proof
Apply Proof
f Proof
a
curryt :: Int -> Term -> Term
curryt :: Int -> Proof -> Proof
curryt Int
n Proof
p = (Symbol -> Proof -> Proof) -> Proof -> [Symbol] -> Proof
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Symbol -> Proof -> Proof
Lam (Proof -> Proof -> Proof
Apply Proof
p (Proof -> [Proof] -> Proof
applys (Int -> Proof
Ctuple Int
n) ((Symbol -> Proof) -> [Symbol] -> [Proof]
forall a b. (a -> b) -> [a] -> [b]
map Symbol -> Proof
Var [Symbol]
xs))) [Symbol]
xs
where xs :: [Symbol]
xs = [ String -> Symbol
Symbol (String
"x_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i) | Int
i <- [Int
0 .. Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1] ]
inj :: ConsDesc -> Int -> Term -> Term
inj :: ConsDesc -> Int -> Proof -> Proof
inj ConsDesc
cd Int
i Proof
p = Symbol -> Proof -> Proof
Lam Symbol
x (Proof -> Proof) -> Proof -> Proof
forall a b. (a -> b) -> a -> b
$ Proof -> Proof -> Proof
Apply Proof
p (Proof -> Proof -> Proof
Apply (ConsDesc -> Int -> Proof
Cinj ConsDesc
cd Int
i) (Symbol -> Proof
Var Symbol
x))
where x :: Symbol
x = String -> Symbol
Symbol String
"x"
applyImp :: Term -> Term -> Term
applyImp :: Proof -> Proof -> Proof
applyImp Proof
p Proof
q = Proof -> Proof -> Proof
Apply Proof
p (Proof -> Proof -> Proof
Apply Proof
q (Symbol -> Proof -> Proof
Lam Symbol
y (Proof -> Proof) -> Proof -> Proof
forall a b. (a -> b) -> a -> b
$ Proof -> Proof -> Proof
Apply Proof
p (Symbol -> Proof -> Proof
Lam Symbol
x (Symbol -> Proof
Var Symbol
y))))
where x :: Symbol
x = String -> Symbol
Symbol String
"x"
y :: Symbol
y = String -> Symbol
Symbol String
"y"
cImpDImpFalse :: Symbol -> Symbol -> Term -> Term -> P Term
cImpDImpFalse :: Symbol -> Symbol -> Proof -> Proof -> P Proof
cImpDImpFalse Symbol
p1 Symbol
p2 Proof
cdf Proof
gp = do
let p1b :: Proof
p1b = Symbol -> Proof -> Proof
Lam Symbol
cf (Proof -> Proof) -> Proof -> Proof
forall a b. (a -> b) -> a -> b
$ Proof -> Proof -> Proof
Apply Proof
cdf (Proof -> Proof) -> Proof -> Proof
forall a b. (a -> b) -> a -> b
$ Symbol -> Proof -> Proof
Lam Symbol
x (Proof -> Proof) -> Proof -> Proof
forall a b. (a -> b) -> a -> b
$ Proof -> Proof -> Proof
Apply ([ConsDesc] -> Proof
Ccases []) (Proof -> Proof) -> Proof -> Proof
forall a b. (a -> b) -> a -> b
$ Proof -> Proof -> Proof
Apply (Symbol -> Proof
Var Symbol
cf) (Symbol -> Proof
Var Symbol
x)
p2b :: Proof
p2b = Symbol -> Proof -> Proof
Lam Symbol
d (Proof -> Proof) -> Proof -> Proof
forall a b. (a -> b) -> a -> b
$ Proof -> Proof -> Proof
Apply Proof
cdf (Proof -> Proof) -> Proof -> Proof
forall a b. (a -> b) -> a -> b
$ Symbol -> Proof -> Proof
Lam Symbol
c (Proof -> Proof) -> Proof -> Proof
forall a b. (a -> b) -> a -> b
$ Symbol -> Proof
Var Symbol
d
cf :: Symbol
cf = String -> Symbol
Symbol String
"cf"
x :: Symbol
x = String -> Symbol
Symbol String
"x"
d :: Symbol
d = String -> Symbol
Symbol String
"d"
c :: Symbol
c = String -> Symbol
Symbol String
"c"
Proof -> Symbol -> Proof -> P Proof
subst Proof
p1b Symbol
p1 Proof
gp P Proof -> (Proof -> P Proof) -> P Proof
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof -> Symbol -> Proof -> P Proof
subst Proof
p2b Symbol
p2
nf :: Term -> P Term
nf :: Proof -> P Proof
nf Proof
ee = Proof -> [Proof] -> P Proof
spine Proof
ee []
where spine :: Proof -> [Proof] -> P Proof
spine (Apply Proof
f Proof
a) [Proof]
as = do Proof
a' <- Proof -> P Proof
nf Proof
a; Proof -> [Proof] -> P Proof
spine Proof
f (Proof
a' Proof -> [Proof] -> [Proof]
forall a. a -> [a] -> [a]
: [Proof]
as)
spine (Lam Symbol
s Proof
e) [] = (Proof -> Proof) -> P Proof -> P Proof
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Symbol -> Proof -> Proof
Lam Symbol
s) (Proof -> P Proof
nf Proof
e)
spine (Lam Symbol
s Proof
e) (Proof
a : [Proof]
as) = do Proof
e' <- Proof -> Symbol -> Proof -> P Proof
subst Proof
a Symbol
s Proof
e; Proof -> [Proof] -> P Proof
spine Proof
e' [Proof]
as
spine (Csplit Int
n) (Proof
b : Proof
tup : [Proof]
args) | Bool
istup Bool -> Bool -> Bool
&& Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= [Proof] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Proof]
xs = Proof -> [Proof] -> P Proof
spine (Proof -> [Proof] -> Proof
applys Proof
b [Proof]
xs) [Proof]
args
where (Bool
istup, [Proof]
xs) = Proof -> (Bool, [Proof])
getTup Proof
tup
getTup :: Proof -> (Bool, [Proof])
getTup (Ctuple Int
_) = (Bool
True, [])
getTup (Apply Proof
f Proof
a) = let (Bool
tf, [Proof]
as) = Proof -> (Bool, [Proof])
getTup Proof
f in (Bool
tf, Proof
aProof -> [Proof] -> [Proof]
forall a. a -> [a] -> [a]
:[Proof]
as)
getTup Proof
_ = (Bool
False, [])
spine (Ccases []) (e :: Proof
e@(Apply (Ccases []) Proof
_) : [Proof]
as) = Proof -> [Proof] -> P Proof
spine Proof
e [Proof]
as
spine (Ccases [ConsDesc]
cds) (Apply (Cinj ConsDesc
_ Int
i) Proof
x : [Proof]
as) | [Proof] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Proof]
as Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
n = Proof -> [Proof] -> P Proof
spine (Proof -> Proof -> Proof
Apply ([Proof]
as[Proof] -> Int -> Proof
forall a. [a] -> Int -> a
!!Int
i) Proof
x) (Int -> [Proof] -> [Proof]
forall a. Int -> [a] -> [a]
drop Int
n [Proof]
as)
where n :: Int
n = [ConsDesc] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ConsDesc]
cds
spine Proof
f [Proof]
as = Proof -> P Proof
forall (m :: * -> *) a. Monad m => a -> m a
return (Proof -> P Proof) -> Proof -> P Proof
forall a b. (a -> b) -> a -> b
$ Proof -> [Proof] -> Proof
applys Proof
f [Proof]
as
newtype P a = P { forall a. P a -> PS -> [(PS, a)]
unP :: PS -> [(PS, a)] }
instance Applicative P where
pure :: forall a. a -> P a
pure = a -> P a
forall (m :: * -> *) a. Monad m => a -> m a
return
<*> :: forall a b. P (a -> b) -> P a -> P b
(<*>) = P (a -> b) -> P a -> P b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap
instance Monad P where
return :: forall a. a -> P a
return a
x = (PS -> [(PS, a)]) -> P a
forall a. (PS -> [(PS, a)]) -> P a
P ((PS -> [(PS, a)]) -> P a) -> (PS -> [(PS, a)]) -> P a
forall a b. (a -> b) -> a -> b
$ \ PS
s -> [(PS
s, a
x)]
P PS -> [(PS, a)]
m >>= :: forall a b. P a -> (a -> P b) -> P b
>>= a -> P b
f = (PS -> [(PS, b)]) -> P b
forall a. (PS -> [(PS, a)]) -> P a
P ((PS -> [(PS, b)]) -> P b) -> (PS -> [(PS, b)]) -> P b
forall a b. (a -> b) -> a -> b
$ \ PS
s -> [ (PS, b)
y | (PS
s',a
x) <- PS -> [(PS, a)]
m PS
s, (PS, b)
y <- P b -> PS -> [(PS, b)]
forall a. P a -> PS -> [(PS, a)]
unP (a -> P b
f a
x) PS
s' ]
instance Functor P where
fmap :: forall a b. (a -> b) -> P a -> P b
fmap a -> b
f (P PS -> [(PS, a)]
m) = (PS -> [(PS, b)]) -> P b
forall a. (PS -> [(PS, a)]) -> P a
P ((PS -> [(PS, b)]) -> P b) -> (PS -> [(PS, b)]) -> P b
forall a b. (a -> b) -> a -> b
$ \ PS
s -> [ (PS
s', a -> b
f a
x) | (PS
s', a
x) <- PS -> [(PS, a)]
m PS
s ]
instance Alternative P where
empty :: forall a. P a
empty = P a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
<|> :: forall a. P a -> P a -> P a
(<|>) = P a -> P a -> P a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus
instance MonadPlus P where
mzero :: forall a. P a
mzero = (PS -> [(PS, a)]) -> P a
forall a. (PS -> [(PS, a)]) -> P a
P ((PS -> [(PS, a)]) -> P a) -> (PS -> [(PS, a)]) -> P a
forall a b. (a -> b) -> a -> b
$ \ PS
_s -> []
P PS -> [(PS, a)]
fxs mplus :: forall a. P a -> P a -> P a
`mplus` P PS -> [(PS, a)]
fys = (PS -> [(PS, a)]) -> P a
forall a. (PS -> [(PS, a)]) -> P a
P ((PS -> [(PS, a)]) -> P a) -> (PS -> [(PS, a)]) -> P a
forall a b. (a -> b) -> a -> b
$ \ PS
s -> PS -> [(PS, a)]
fxs PS
s [(PS, a)] -> [(PS, a)] -> [(PS, a)]
forall a. [a] -> [a] -> [a]
++ PS -> [(PS, a)]
fys PS
s
data PS = PS !Integer
startPS :: PS
startPS :: PS
startPS = Integer -> PS
PS Integer
1
nextInt :: P Integer
nextInt :: P Integer
nextInt = (PS -> [(PS, Integer)]) -> P Integer
forall a. (PS -> [(PS, a)]) -> P a
P ((PS -> [(PS, Integer)]) -> P Integer)
-> (PS -> [(PS, Integer)]) -> P Integer
forall a b. (a -> b) -> a -> b
$ \ (PS Integer
i) -> [(Integer -> PS
PS (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1), Integer
i)]
none :: P a
none :: forall a. P a
none = P a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
many :: [a] -> P a
many :: forall a. [a] -> P a
many [a]
xs = (PS -> [(PS, a)]) -> P a
forall a. (PS -> [(PS, a)]) -> P a
P ((PS -> [(PS, a)]) -> P a) -> (PS -> [(PS, a)]) -> P a
forall a b. (a -> b) -> a -> b
$ \ PS
s -> [PS] -> [a] -> [(PS, a)]
forall a b. [a] -> [b] -> [(a, b)]
zip (PS -> [PS]
forall a. a -> [a]
repeat PS
s) [a]
xs
atMostOne :: P a -> P a
atMostOne :: forall a. P a -> P a
atMostOne (P PS -> [(PS, a)]
f) = (PS -> [(PS, a)]) -> P a
forall a. (PS -> [(PS, a)]) -> P a
P ((PS -> [(PS, a)]) -> P a) -> (PS -> [(PS, a)]) -> P a
forall a b. (a -> b) -> a -> b
$ \ PS
s -> Int -> [(PS, a)] -> [(PS, a)]
forall a. Int -> [a] -> [a]
take Int
1 (PS -> [(PS, a)]
f PS
s)
runP :: P a -> [a]
runP :: forall a. P a -> [a]
runP (P PS -> [(PS, a)]
m) = ((PS, a) -> a) -> [(PS, a)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (PS, a) -> a
forall a b. (a, b) -> b
snd (PS -> [(PS, a)]
m PS
startPS)
data AtomF = AtomF Term Symbol
deriving (AtomF -> AtomF -> Bool
(AtomF -> AtomF -> Bool) -> (AtomF -> AtomF -> Bool) -> Eq AtomF
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: AtomF -> AtomF -> Bool
$c/= :: AtomF -> AtomF -> Bool
== :: AtomF -> AtomF -> Bool
$c== :: AtomF -> AtomF -> Bool
Eq)
instance Show AtomF where
show :: AtomF -> String
show (AtomF Proof
p Symbol
s) = Proof -> String
forall a. Show a => a -> String
show Proof
p String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
":" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Symbol -> String
forall a. Show a => a -> String
show Symbol
s
type AtomFs = [AtomF]
findAtoms :: Symbol -> AtomFs -> [Term]
findAtoms :: Symbol -> AtomFs -> [Proof]
findAtoms Symbol
s AtomFs
atoms = [ Proof
p | AtomF Proof
p Symbol
s' <- AtomFs
atoms, Symbol
s Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
s' ]
addAtom :: AtomF -> AtomFs -> AtomFs
addAtom :: AtomF -> AtomFs -> AtomFs
addAtom AtomF
a AtomFs
as = if AtomF
a AtomF -> AtomFs -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` AtomFs
as then AtomFs
as else AtomF
a AtomF -> AtomFs -> AtomFs
forall a. a -> [a] -> [a]
: AtomFs
as
data AtomImp = AtomImp Symbol Antecedents
deriving (Int -> AtomImp -> String -> String
AtomImps -> String -> String
AtomImp -> String
(Int -> AtomImp -> String -> String)
-> (AtomImp -> String)
-> (AtomImps -> String -> String)
-> Show AtomImp
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: AtomImps -> String -> String
$cshowList :: AtomImps -> String -> String
show :: AtomImp -> String
$cshow :: AtomImp -> String
showsPrec :: Int -> AtomImp -> String -> String
$cshowsPrec :: Int -> AtomImp -> String -> String
Show)
type AtomImps = [AtomImp]
extract :: AtomImps -> Symbol -> ([Antecedent], AtomImps)
aatomImps :: AtomImps
aatomImps@(atomImp :: AtomImp
atomImp@(AtomImp Symbol
a' Antecedents
bs) : AtomImps
atomImps) Symbol
a =
case Symbol -> Symbol -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Symbol
a Symbol
a' of
Ordering
GT -> let (Antecedents
rbs, AtomImps
restImps) = AtomImps -> Symbol -> (Antecedents, AtomImps)
extract AtomImps
atomImps Symbol
a in (Antecedents
rbs, AtomImp
atomImp AtomImp -> AtomImps -> AtomImps
forall a. a -> [a] -> [a]
: AtomImps
restImps)
Ordering
EQ -> (Antecedents
bs, AtomImps
atomImps)
Ordering
LT -> ([], AtomImps
aatomImps)
extract AtomImps
_ Symbol
_ = ([], [])
insert :: AtomImps -> AtomImp -> AtomImps
insert :: AtomImps -> AtomImp -> AtomImps
insert [] AtomImp
ai = [ AtomImp
ai ]
insert aatomImps :: AtomImps
aatomImps@(atomImp :: AtomImp
atomImp@(AtomImp Symbol
a' Antecedents
bs') : AtomImps
atomImps) ai :: AtomImp
ai@(AtomImp Symbol
a Antecedents
bs) =
case Symbol -> Symbol -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Symbol
a Symbol
a' of
Ordering
GT -> AtomImp
atomImp AtomImp -> AtomImps -> AtomImps
forall a. a -> [a] -> [a]
: AtomImps -> AtomImp -> AtomImps
insert AtomImps
atomImps AtomImp
ai
Ordering
EQ -> Symbol -> Antecedents -> AtomImp
AtomImp Symbol
a (Antecedents
bs Antecedents -> Antecedents -> Antecedents
forall a. [a] -> [a] -> [a]
++ Antecedents
bs') AtomImp -> AtomImps -> AtomImps
forall a. a -> [a] -> [a]
: AtomImps
atomImps
Ordering
LT -> AtomImp
ai AtomImp -> AtomImps -> AtomImps
forall a. a -> [a] -> [a]
: AtomImps
aatomImps
data NestImp = NestImp Term Formula Formula Formula
deriving (NestImp -> NestImp -> Bool
(NestImp -> NestImp -> Bool)
-> (NestImp -> NestImp -> Bool) -> Eq NestImp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: NestImp -> NestImp -> Bool
$c/= :: NestImp -> NestImp -> Bool
== :: NestImp -> NestImp -> Bool
$c== :: NestImp -> NestImp -> Bool
Eq)
instance Show NestImp where
show :: NestImp -> String
show (NestImp Proof
_ Goal
a Goal
b Goal
c) = Goal -> String
forall a. Show a => a -> String
show (Goal -> String) -> Goal -> String
forall a b. (a -> b) -> a -> b
$ (Goal
a Goal -> Goal -> Goal
:-> Goal
b) Goal -> Goal -> Goal
:-> Goal
c
type NestImps = [NestImp]
addNestImp :: NestImp -> NestImps -> NestImps
addNestImp :: NestImp -> NestImps -> NestImps
addNestImp NestImp
n NestImps
ns = if NestImp
n NestImp -> NestImps -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` NestImps
ns then NestImps
ns else NestImp
n NestImp -> NestImps -> NestImps
forall a. a -> [a] -> [a]
: NestImps
ns
heuristics :: Bool
heuristics :: Bool
heuristics = Bool
True
order :: NestImps -> Formula -> AtomImps -> NestImps
order :: NestImps -> Goal -> AtomImps -> NestImps
order NestImps
nestImps Goal
g AtomImps
atomImps =
if Bool
heuristics
then NestImps
nestImps
else let good_for :: NestImp -> Bool
good_for (NestImp Proof
_ Goal
_ Goal
_ (Disj [])) = Bool
True
good_for (NestImp Proof
_ Goal
_ Goal
_ Goal
g') = Goal
g Goal -> Goal -> Bool
forall a. Eq a => a -> a -> Bool
== Goal
g'
nice_for :: NestImp -> Bool
nice_for (NestImp Proof
_ Goal
_ Goal
_ (PVar Symbol
s)) =
case AtomImps -> Symbol -> (Antecedents, AtomImps)
extract AtomImps
atomImps Symbol
s of
(Antecedents
bs', AtomImps
_) -> let bs :: [Goal]
bs = [ Goal
b | A Proof
_ Goal
b <- Antecedents
bs'] in Goal
g Goal -> [Goal] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Goal]
bs Bool -> Bool -> Bool
|| Goal
false Goal -> [Goal] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Goal]
bs
nice_for NestImp
_ = Bool
False
(NestImps
good, NestImps
ok) = (NestImp -> Bool) -> NestImps -> (NestImps, NestImps)
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition NestImp -> Bool
good_for NestImps
nestImps
(NestImps
nice, NestImps
bad) = (NestImp -> Bool) -> NestImps -> (NestImps, NestImps)
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition NestImp -> Bool
nice_for NestImps
ok
in NestImps
good NestImps -> NestImps -> NestImps
forall a. [a] -> [a] -> [a]
++ NestImps
nice NestImps -> NestImps -> NestImps
forall a. [a] -> [a] -> [a]
++ NestImps
bad
newSym :: String -> P Symbol
newSym :: String -> P Symbol
newSym String
pre = do
Integer
i <- P Integer
nextInt
Symbol -> P Symbol
forall (m :: * -> *) a. Monad m => a -> m a
return (Symbol -> P Symbol) -> Symbol -> P Symbol
forall a b. (a -> b) -> a -> b
$ String -> Symbol
Symbol (String -> Symbol) -> String -> Symbol
forall a b. (a -> b) -> a -> b
$ String
pre String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
i
select :: [a] -> P (a, [a])
select :: forall a. [a] -> P (a, [a])
select [a]
zs = [(a, [a])] -> P (a, [a])
forall a. [a] -> P a
many [ Int -> [a] -> (a, [a])
forall {a} {a}. (Eq a, Num a) => a -> [a] -> (a, [a])
del Int
n [a]
zs | Int
n <- [Int
0 .. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
zs Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1] ]
where del :: a -> [a] -> (a, [a])
del a
0 (a
x:[a]
xs) = (a
x, [a]
xs)
del a
n (a
x:[a]
xs) = let (a
y,[a]
ys) = a -> [a] -> (a, [a])
del (a
na -> a -> a
forall a. Num a => a -> a -> a
-a
1) [a]
xs in (a
y, a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
ys)
del a
_ [a]
_ = String -> (a, [a])
forall a. HasCallStack => String -> a
error String
"select"
data Antecedent = A Term Formula deriving (Int -> Antecedent -> String -> String
Antecedents -> String -> String
Antecedent -> String
(Int -> Antecedent -> String -> String)
-> (Antecedent -> String)
-> (Antecedents -> String -> String)
-> Show Antecedent
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: Antecedents -> String -> String
$cshowList :: Antecedents -> String -> String
show :: Antecedent -> String
$cshow :: Antecedent -> String
showsPrec :: Int -> Antecedent -> String -> String
$cshowsPrec :: Int -> Antecedent -> String -> String
Show)
type Antecedents = [Antecedent]
type Goal = Formula
redant :: MoreSolutions -> Antecedents -> AtomImps -> NestImps -> AtomFs -> Goal -> P Proof
redant :: Bool
-> Antecedents -> AtomImps -> NestImps -> AtomFs -> Goal -> P Proof
redant Bool
more Antecedents
antes AtomImps
atomImps NestImps
nestImps AtomFs
atoms Goal
goal =
String
-> (Antecedents, AtomImps, NestImps, AtomFs, Goal)
-> P Proof
-> P Proof
forall a b (m :: * -> *).
(Show a, Show b, Monad m) =>
String -> a -> m b -> m b
wrapM String
"redant" (Antecedents
antes, AtomImps
atomImps, NestImps
nestImps, AtomFs
atoms, Goal
goal) (P Proof -> P Proof) -> P Proof -> P Proof
forall a b. (a -> b) -> a -> b
$
case Antecedents
antes of
[] -> Goal -> P Proof
redsucc Goal
goal
Antecedent
a:Antecedents
l -> Antecedent -> Antecedents -> Goal -> P Proof
redant1 Antecedent
a Antecedents
l Goal
goal
where redant0 :: Antecedents -> Goal -> P Proof
redant0 Antecedents
l Goal
g = Bool
-> Antecedents -> AtomImps -> NestImps -> AtomFs -> Goal -> P Proof
redant Bool
more Antecedents
l AtomImps
atomImps NestImps
nestImps AtomFs
atoms Goal
g
redant1 :: Antecedent -> Antecedents -> Goal -> P Proof
redant1 :: Antecedent -> Antecedents -> Goal -> P Proof
redant1 a :: Antecedent
a@(A Proof
p Goal
f) Antecedents
l Goal
g =
String
-> ((Antecedent, Antecedents), AtomImps, NestImps, AtomFs, Goal)
-> P Proof
-> P Proof
forall a b (m :: * -> *).
(Show a, Show b, Monad m) =>
String -> a -> m b -> m b
wrapM String
"redant1" ((Antecedent
a, Antecedents
l), AtomImps
atomImps, NestImps
nestImps, AtomFs
atoms, Goal
g) (P Proof -> P Proof) -> P Proof -> P Proof
forall a b. (a -> b) -> a -> b
$
if Goal
f Goal -> Goal -> Bool
forall a. Eq a => a -> a -> Bool
== Goal
g
then
if Bool
more
then Proof -> P Proof
forall (m :: * -> *) a. Monad m => a -> m a
return Proof
p P Proof -> P Proof -> P Proof
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Antecedent -> Antecedents -> Goal -> P Proof
redant1' Antecedent
a Antecedents
l Goal
g
else Proof -> P Proof
forall (m :: * -> *) a. Monad m => a -> m a
return Proof
p
else Antecedent -> Antecedents -> Goal -> P Proof
redant1' Antecedent
a Antecedents
l Goal
g
redant1' :: Antecedent -> Antecedents -> Goal -> P Proof
redant1' :: Antecedent -> Antecedents -> Goal -> P Proof
redant1' (A Proof
p (PVar Symbol
s)) Antecedents
l Goal
g =
let af :: AtomF
af = Proof -> Symbol -> AtomF
AtomF Proof
p Symbol
s
(Antecedents
bs, AtomImps
restAtomImps) = AtomImps -> Symbol -> (Antecedents, AtomImps)
extract AtomImps
atomImps Symbol
s
in Bool
-> Antecedents -> AtomImps -> NestImps -> AtomFs -> Goal -> P Proof
redant Bool
more ([Proof -> Goal -> Antecedent
A (Proof -> Proof -> Proof
Apply Proof
f Proof
p) Goal
b | A Proof
f Goal
b <- Antecedents
bs] Antecedents -> Antecedents -> Antecedents
forall a. [a] -> [a] -> [a]
++ Antecedents
l) AtomImps
restAtomImps NestImps
nestImps (AtomF -> AtomFs -> AtomFs
addAtom AtomF
af AtomFs
atoms) Goal
g
redant1' (A Proof
p (Conj [Goal]
bs)) Antecedents
l Goal
g = do
[Symbol]
vs <- (Goal -> P Symbol) -> [Goal] -> P [Symbol]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (P Symbol -> Goal -> P Symbol
forall a b. a -> b -> a
const (String -> P Symbol
newSym String
"v")) [Goal]
bs
Proof
gp <- Antecedents -> Goal -> P Proof
redant0 ((Symbol -> Goal -> Antecedent) -> [Symbol] -> [Goal] -> Antecedents
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ Symbol
v Goal
a -> Proof -> Goal -> Antecedent
A (Symbol -> Proof
Var Symbol
v) Goal
a) [Symbol]
vs [Goal]
bs Antecedents -> Antecedents -> Antecedents
forall a. [a] -> [a] -> [a]
++ Antecedents
l) Goal
g
Proof -> P Proof
forall (m :: * -> *) a. Monad m => a -> m a
return (Proof -> P Proof) -> Proof -> P Proof
forall a b. (a -> b) -> a -> b
$ Proof -> [Proof] -> Proof
applys (Int -> Proof
Csplit ([Goal] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Goal]
bs)) [(Symbol -> Proof -> Proof) -> Proof -> [Symbol] -> Proof
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Symbol -> Proof -> Proof
Lam Proof
gp [Symbol]
vs, Proof
p]
redant1' (A Proof
p (Disj [(ConsDesc, Goal)]
ds)) Antecedents
l Goal
g = do
[Symbol]
vs <- ((ConsDesc, Goal) -> P Symbol) -> [(ConsDesc, Goal)] -> P [Symbol]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (P Symbol -> (ConsDesc, Goal) -> P Symbol
forall a b. a -> b -> a
const (String -> P Symbol
newSym String
"d")) [(ConsDesc, Goal)]
ds
[Proof]
ps <- ((Symbol, (ConsDesc, Goal)) -> P Proof)
-> [(Symbol, (ConsDesc, Goal))] -> P [Proof]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ (Symbol
v, (ConsDesc
_, Goal
d)) -> Antecedent -> Antecedents -> Goal -> P Proof
redant1 (Proof -> Goal -> Antecedent
A (Symbol -> Proof
Var Symbol
v) Goal
d) Antecedents
l Goal
g) ([Symbol] -> [(ConsDesc, Goal)] -> [(Symbol, (ConsDesc, Goal))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
vs [(ConsDesc, Goal)]
ds)
if [(ConsDesc, Goal)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(ConsDesc, Goal)]
ds Bool -> Bool -> Bool
&& Goal
g Goal -> Goal -> Bool
forall a. Eq a => a -> a -> Bool
== [(ConsDesc, Goal)] -> Goal
Disj []
then Proof -> P Proof
forall (m :: * -> *) a. Monad m => a -> m a
return Proof
p
else Proof -> P Proof
forall (m :: * -> *) a. Monad m => a -> m a
return (Proof -> P Proof) -> Proof -> P Proof
forall a b. (a -> b) -> a -> b
$ Proof -> [Proof] -> Proof
applys ([ConsDesc] -> Proof
Ccases (((ConsDesc, Goal) -> ConsDesc) -> [(ConsDesc, Goal)] -> [ConsDesc]
forall a b. (a -> b) -> [a] -> [b]
map (ConsDesc, Goal) -> ConsDesc
forall a b. (a, b) -> a
fst [(ConsDesc, Goal)]
ds)) (Proof
p Proof -> [Proof] -> [Proof]
forall a. a -> [a] -> [a]
: (Symbol -> Proof -> Proof) -> [Symbol] -> [Proof] -> [Proof]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Symbol -> Proof -> Proof
Lam [Symbol]
vs [Proof]
ps)
redant1' (A Proof
p (Goal
a :-> Goal
b)) Antecedents
l Goal
g = Proof -> Goal -> Goal -> Antecedents -> Goal -> P Proof
redantimp Proof
p Goal
a Goal
b Antecedents
l Goal
g
redantimp :: Term -> Formula -> Formula -> Antecedents -> Goal -> P Proof
redantimp :: Proof -> Goal -> Goal -> Antecedents -> Goal -> P Proof
redantimp Proof
t Goal
c Goal
d Antecedents
a Goal
g =
String -> (Goal, Goal, Antecedents, Goal) -> P Proof -> P Proof
forall a b (m :: * -> *).
(Show a, Show b, Monad m) =>
String -> a -> m b -> m b
wrapM String
"redantimp" (Goal
c,Goal
d,Antecedents
a,Goal
g) (P Proof -> P Proof) -> P Proof -> P Proof
forall a b. (a -> b) -> a -> b
$
Proof -> Goal -> Goal -> Antecedents -> Goal -> P Proof
redantimp' Proof
t Goal
c Goal
d Antecedents
a Goal
g
redantimp' :: Term -> Formula -> Formula -> Antecedents -> Goal -> P Proof
redantimp' :: Proof -> Goal -> Goal -> Antecedents -> Goal -> P Proof
redantimp' Proof
p (PVar Symbol
s) Goal
b Antecedents
l Goal
g = Proof -> Symbol -> Goal -> Antecedents -> Goal -> P Proof
redantimpatom Proof
p Symbol
s Goal
b Antecedents
l Goal
g
redantimp' Proof
p (Conj [Goal]
cs) Goal
b Antecedents
l Goal
g = do
Symbol
x <- String -> P Symbol
newSym String
"x"
let imp :: Goal
imp = (Goal -> Goal -> Goal) -> Goal -> [Goal] -> Goal
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Goal -> Goal -> Goal
(:->) Goal
b [Goal]
cs
Proof
gp <- Antecedent -> Antecedents -> Goal -> P Proof
redant1 (Proof -> Goal -> Antecedent
A (Symbol -> Proof
Var Symbol
x) Goal
imp) Antecedents
l Goal
g
Proof -> Symbol -> Proof -> P Proof
subst (Int -> Proof -> Proof
curryt ([Goal] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Goal]
cs) Proof
p) Symbol
x Proof
gp
redantimp' Proof
p (Disj [(ConsDesc, Goal)]
ds) Goal
b Antecedents
l Goal
g = do
[Symbol]
vs <- ((ConsDesc, Goal) -> P Symbol) -> [(ConsDesc, Goal)] -> P [Symbol]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (P Symbol -> (ConsDesc, Goal) -> P Symbol
forall a b. a -> b -> a
const (String -> P Symbol
newSym String
"d")) [(ConsDesc, Goal)]
ds
Proof
gp <- Antecedents -> Goal -> P Proof
redant0 ((Symbol -> (ConsDesc, Goal) -> Antecedent)
-> [Symbol] -> [(ConsDesc, Goal)] -> Antecedents
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ Symbol
v (ConsDesc
_, Goal
d) -> Proof -> Goal -> Antecedent
A (Symbol -> Proof
Var Symbol
v) (Goal
d Goal -> Goal -> Goal
:-> Goal
b)) [Symbol]
vs [(ConsDesc, Goal)]
ds Antecedents -> Antecedents -> Antecedents
forall a. [a] -> [a] -> [a]
++ Antecedents
l) Goal
g
(Proof -> (Int, Symbol, (ConsDesc, Goal)) -> P Proof)
-> Proof -> [(Int, Symbol, (ConsDesc, Goal))] -> P Proof
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ Proof
r (Int
i, Symbol
v, (ConsDesc
cd, Goal
_)) -> Proof -> Symbol -> Proof -> P Proof
subst (ConsDesc -> Int -> Proof -> Proof
inj ConsDesc
cd Int
i Proof
p) Symbol
v Proof
r) Proof
gp ([Int]
-> [Symbol]
-> [(ConsDesc, Goal)]
-> [(Int, Symbol, (ConsDesc, Goal))]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Int
0..] [Symbol]
vs [(ConsDesc, Goal)]
ds)
redantimp' Proof
p (Goal
c :-> Goal
d) Goal
b Antecedents
l Goal
g = Proof -> Goal -> Goal -> Goal -> Antecedents -> Goal -> P Proof
redantimpimp Proof
p Goal
c Goal
d Goal
b Antecedents
l Goal
g
redantimpimp :: Term -> Formula -> Formula -> Formula -> Antecedents -> Goal -> P Proof
redantimpimp :: Proof -> Goal -> Goal -> Goal -> Antecedents -> Goal -> P Proof
redantimpimp Proof
f Goal
b Goal
c Goal
d Antecedents
a Goal
g =
String
-> (Goal, Goal, Goal, Antecedents, Goal) -> P Proof -> P Proof
forall a b (m :: * -> *).
(Show a, Show b, Monad m) =>
String -> a -> m b -> m b
wrapM String
"redantimpimp" (Goal
b,Goal
c,Goal
d,Antecedents
a,Goal
g) (P Proof -> P Proof) -> P Proof -> P Proof
forall a b. (a -> b) -> a -> b
$
Proof -> Goal -> Goal -> Goal -> Antecedents -> Goal -> P Proof
redantimpimp' Proof
f Goal
b Goal
c Goal
d Antecedents
a Goal
g
redantimpimp' :: Term -> Formula -> Formula -> Formula -> Antecedents -> Goal -> P Proof
redantimpimp' :: Proof -> Goal -> Goal -> Goal -> Antecedents -> Goal -> P Proof
redantimpimp' Proof
p Goal
c Goal
d (Disj []) Antecedents
l Goal
g | Goal
d Goal -> Goal -> Bool
forall a. Eq a => a -> a -> Bool
/= Goal
false = do
Symbol
x <- String -> P Symbol
newSym String
"x"
Symbol
y <- String -> P Symbol
newSym String
"y"
Proof
gp <- Proof -> Goal -> Goal -> Goal -> Antecedents -> Goal -> P Proof
redantimpimp (Symbol -> Proof
Var Symbol
x) Goal
c Goal
false Goal
false (Proof -> Goal -> Antecedent
A (Symbol -> Proof
Var Symbol
y) (Goal
d Goal -> Goal -> Goal
:-> Goal
false) Antecedent -> Antecedents -> Antecedents
forall a. a -> [a] -> [a]
: Antecedents
l) Goal
g
Symbol -> Symbol -> Proof -> Proof -> P Proof
cImpDImpFalse Symbol
x Symbol
y Proof
p Proof
gp
redantimpimp' Proof
p Goal
c Goal
d Goal
b Antecedents
l Goal
g = Bool
-> Antecedents -> AtomImps -> NestImps -> AtomFs -> Goal -> P Proof
redant Bool
more Antecedents
l AtomImps
atomImps (NestImp -> NestImps -> NestImps
addNestImp (Proof -> Goal -> Goal -> Goal -> NestImp
NestImp Proof
p Goal
c Goal
d Goal
b) NestImps
nestImps) AtomFs
atoms Goal
g
redantimpatom :: Term -> Symbol -> Formula -> Antecedents -> Goal -> P Proof
redantimpatom :: Proof -> Symbol -> Goal -> Antecedents -> Goal -> P Proof
redantimpatom Proof
p Symbol
s Goal
b Antecedents
l Goal
g =
String -> (Symbol, Goal, Antecedents, Goal) -> P Proof -> P Proof
forall a b (m :: * -> *).
(Show a, Show b, Monad m) =>
String -> a -> m b -> m b
wrapM String
"redantimpatom" (Symbol
s,Goal
b,Antecedents
l,Goal
g) (P Proof -> P Proof) -> P Proof -> P Proof
forall a b. (a -> b) -> a -> b
$
Proof -> Symbol -> Goal -> Antecedents -> Goal -> P Proof
redantimpatom' Proof
p Symbol
s Goal
b Antecedents
l Goal
g
redantimpatom' :: Term -> Symbol -> Formula -> Antecedents -> Goal -> P Proof
redantimpatom' :: Proof -> Symbol -> Goal -> Antecedents -> Goal -> P Proof
redantimpatom' Proof
p Symbol
s Goal
b Antecedents
l Goal
g =
do Proof
a <- Bool -> P Proof -> P Proof
forall a. Bool -> P a -> P a
cutSearch Bool
more (P Proof -> P Proof) -> P Proof -> P Proof
forall a b. (a -> b) -> a -> b
$ [Proof] -> P Proof
forall a. [a] -> P a
many (Symbol -> AtomFs -> [Proof]
findAtoms Symbol
s AtomFs
atoms)
Symbol
x <- String -> P Symbol
newSym String
"x"
Proof
gp <- Antecedent -> Antecedents -> Goal -> P Proof
redant1 (Proof -> Goal -> Antecedent
A (Symbol -> Proof
Var Symbol
x) Goal
b) Antecedents
l Goal
g
String -> P Proof -> P Proof
forall a. String -> a -> a
mtrace String
"redantimpatom: LLL" (P Proof -> P Proof) -> P Proof -> P Proof
forall a b. (a -> b) -> a -> b
$ Proof -> Symbol -> Proof -> P Proof
subst (Proof -> Proof -> Proof
applyAtom Proof
p Proof
a) Symbol
x Proof
gp
P Proof -> P Proof -> P Proof
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus`
(String -> P Proof -> P Proof
forall a. String -> a -> a
mtrace String
"redantimpatom: RRR" (P Proof -> P Proof) -> P Proof -> P Proof
forall a b. (a -> b) -> a -> b
$
Bool
-> Antecedents -> AtomImps -> NestImps -> AtomFs -> Goal -> P Proof
redant Bool
more Antecedents
l (AtomImps -> AtomImp -> AtomImps
insert AtomImps
atomImps (Symbol -> Antecedents -> AtomImp
AtomImp Symbol
s [Proof -> Goal -> Antecedent
A Proof
p Goal
b])) NestImps
nestImps AtomFs
atoms Goal
g)
redsucc :: Goal -> P Proof
redsucc :: Goal -> P Proof
redsucc Goal
g =
String -> (Goal, AtomImps, NestImps, AtomFs) -> P Proof -> P Proof
forall a b (m :: * -> *).
(Show a, Show b, Monad m) =>
String -> a -> m b -> m b
wrapM String
"redsucc" (Goal
g, AtomImps
atomImps, NestImps
nestImps, AtomFs
atoms) (P Proof -> P Proof) -> P Proof -> P Proof
forall a b. (a -> b) -> a -> b
$
Goal -> P Proof
redsucc' Goal
g
redsucc' :: Goal -> P Proof
redsucc' :: Goal -> P Proof
redsucc' a :: Goal
a@(PVar Symbol
s) =
(Bool -> P Proof -> P Proof
forall a. Bool -> P a -> P a
cutSearch Bool
more (P Proof -> P Proof) -> P Proof -> P Proof
forall a b. (a -> b) -> a -> b
$ [Proof] -> P Proof
forall a. [a] -> P a
many (Symbol -> AtomFs -> [Proof]
findAtoms Symbol
s AtomFs
atoms))
P Proof -> P Proof -> P Proof
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus`
(if Symbol -> AtomImps -> NestImps -> Bool
posin Symbol
s AtomImps
atomImps NestImps
nestImps then Goal -> P Proof
redsucc_choice Goal
a else P Proof
forall a. P a
none)
redsucc' (Conj [Goal]
cs) = do
[Proof]
ps <- (Goal -> P Proof) -> [Goal] -> P [Proof]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Goal -> P Proof
redsucc [Goal]
cs
Proof -> P Proof
forall (m :: * -> *) a. Monad m => a -> m a
return (Proof -> P Proof) -> Proof -> P Proof
forall a b. (a -> b) -> a -> b
$ Proof -> [Proof] -> Proof
applys (Int -> Proof
Ctuple ([Goal] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Goal]
cs)) [Proof]
ps
redsucc' (Disj [(ConsDesc, Goal)]
ds) = do
Symbol
s1 <- String -> P Symbol
newSym String
"_"
let v :: Goal
v = Symbol -> Goal
PVar Symbol
s1
Antecedents -> Goal -> P Proof
redant0 [ Proof -> Goal -> Antecedent
A (ConsDesc -> Int -> Proof
Cinj ConsDesc
cd Int
i) (Goal -> Antecedent) -> Goal -> Antecedent
forall a b. (a -> b) -> a -> b
$ Goal
d Goal -> Goal -> Goal
:-> Goal
v | (Int
i, (ConsDesc
cd, Goal
d)) <- [Int] -> [(ConsDesc, Goal)] -> [(Int, (ConsDesc, Goal))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [(ConsDesc, Goal)]
ds ] Goal
v
redsucc' (Goal
a :-> Goal
b) = do
Symbol
s <- String -> P Symbol
newSym String
"x"
Proof
p <- Antecedent -> Antecedents -> Goal -> P Proof
redant1 (Proof -> Goal -> Antecedent
A (Symbol -> Proof
Var Symbol
s) Goal
a) [] Goal
b
Proof -> P Proof
forall (m :: * -> *) a. Monad m => a -> m a
return (Proof -> P Proof) -> Proof -> P Proof
forall a b. (a -> b) -> a -> b
$ Symbol -> Proof -> Proof
Lam Symbol
s Proof
p
redsucc_choice :: Goal -> P Proof
redsucc_choice :: Goal -> P Proof
redsucc_choice Goal
g =
String -> Goal -> P Proof -> P Proof
forall a b (m :: * -> *).
(Show a, Show b, Monad m) =>
String -> a -> m b -> m b
wrapM String
"redsucc_choice" Goal
g (P Proof -> P Proof) -> P Proof -> P Proof
forall a b. (a -> b) -> a -> b
$
Goal -> P Proof
redsucc_choice' Goal
g
redsucc_choice' :: Goal -> P Proof
redsucc_choice' :: Goal -> P Proof
redsucc_choice' Goal
g = do
let ordImps :: NestImps
ordImps = NestImps -> Goal -> AtomImps -> NestImps
order NestImps
nestImps Goal
g AtomImps
atomImps
(NestImp Proof
p Goal
c Goal
d Goal
b, NestImps
restImps) <-
String -> P (NestImp, NestImps) -> P (NestImp, NestImps)
forall a. String -> a -> a
mtrace (String
"redsucc_choice: order=" String -> String -> String
forall a. [a] -> [a] -> [a]
++ NestImps -> String
forall a. Show a => a -> String
show NestImps
ordImps) (P (NestImp, NestImps) -> P (NestImp, NestImps))
-> P (NestImp, NestImps) -> P (NestImp, NestImps)
forall a b. (a -> b) -> a -> b
$
NestImps -> P (NestImp, NestImps)
forall a. [a] -> P (a, [a])
select NestImps
ordImps
Symbol
x <- String -> P Symbol
newSym String
"x"
Symbol
z <- String -> P Symbol
newSym String
"z"
Proof
qz <- Bool
-> Antecedents -> AtomImps -> NestImps -> AtomFs -> Goal -> P Proof
redant Bool
more [Proof -> Goal -> Antecedent
A (Symbol -> Proof
Var Symbol
z) (Goal -> Antecedent) -> Goal -> Antecedent
forall a b. (a -> b) -> a -> b
$ Goal
d Goal -> Goal -> Goal
:-> Goal
b] AtomImps
atomImps NestImps
restImps AtomFs
atoms (Goal
c Goal -> Goal -> Goal
:-> Goal
d)
Proof
gp <- Bool
-> Antecedents -> AtomImps -> NestImps -> AtomFs -> Goal -> P Proof
redant Bool
more [Proof -> Goal -> Antecedent
A (Symbol -> Proof
Var Symbol
x) Goal
b] AtomImps
atomImps NestImps
restImps AtomFs
atoms Goal
g
Proof -> Symbol -> Proof -> P Proof
subst (Proof -> Proof -> Proof
applyImp Proof
p (Symbol -> Proof -> Proof
Lam Symbol
z Proof
qz)) Symbol
x Proof
gp
posin :: Symbol -> AtomImps -> NestImps -> Bool
posin :: Symbol -> AtomImps -> NestImps -> Bool
posin Symbol
g AtomImps
atomImps NestImps
nestImps = Symbol -> AtomImps -> Bool
posin1 Symbol
g AtomImps
atomImps Bool -> Bool -> Bool
|| Symbol -> [Goal] -> Bool
posin2 Symbol
g [ (Goal
a Goal -> Goal -> Goal
:-> Goal
b) Goal -> Goal -> Goal
:-> Goal
c | NestImp Proof
_ Goal
a Goal
b Goal
c <- NestImps
nestImps ]
posin1 :: Symbol -> AtomImps -> Bool
posin1 :: Symbol -> AtomImps -> Bool
posin1 Symbol
g AtomImps
atomImps = (AtomImp -> Bool) -> AtomImps -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\ (AtomImp Symbol
_ Antecedents
bs) -> Symbol -> [Goal] -> Bool
posin2 Symbol
g [ Goal
b | A Proof
_ Goal
b <- Antecedents
bs]) AtomImps
atomImps
posin2 :: Symbol -> [Formula] -> Bool
posin2 :: Symbol -> [Goal] -> Bool
posin2 Symbol
g [Goal]
bs = (Goal -> Bool) -> [Goal] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Symbol -> Goal -> Bool
posin3 Symbol
g) [Goal]
bs
posin3 :: Symbol -> Formula -> Bool
posin3 :: Symbol -> Goal -> Bool
posin3 Symbol
g (Disj [(ConsDesc, Goal)]
as) = (Goal -> Bool) -> [Goal] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Symbol -> Goal -> Bool
posin3 Symbol
g) (((ConsDesc, Goal) -> Goal) -> [(ConsDesc, Goal)] -> [Goal]
forall a b. (a -> b) -> [a] -> [b]
map (ConsDesc, Goal) -> Goal
forall a b. (a, b) -> b
snd [(ConsDesc, Goal)]
as)
posin3 Symbol
g (Conj [Goal]
as) = (Goal -> Bool) -> [Goal] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Symbol -> Goal -> Bool
posin3 Symbol
g) [Goal]
as
posin3 Symbol
g (Goal
_ :-> Goal
b) = Symbol -> Goal -> Bool
posin3 Symbol
g Goal
b
posin3 Symbol
s (PVar Symbol
s') = Symbol
s Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
s'
cutSearch :: MoreSolutions -> P a -> P a
cutSearch :: forall a. Bool -> P a -> P a
cutSearch Bool
False P a
p = P a -> P a
forall a. P a -> P a
atMostOne P a
p
cutSearch Bool
True P a
p = P a
p