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 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
() <- forall a. String -> a -> a
mtrace (String
fun forall a. [a] -> [a] -> [a]
++ String
": " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
args) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ()
b
ret <- m b
mret
() <- forall a. String -> a -> a
mtrace (String
fun forall a. [a] -> [a] -> [a]
++ String
" returns: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show b
ret) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ()
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 forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Bool
null 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 = forall a. P a -> [a]
runP 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 = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Goal -> Goal -> Goal
(:->) Goal
a (forall a b. (a -> b) -> [a] -> [b]
map 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 (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Proof -> Proof -> Proof
Apply Proof
p (forall a b. (a -> b) -> [a] -> [b]
map (Symbol -> Proof
Var forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall a. Eq a => a -> a -> Bool
== Symbol
s' then [(Symbol, Symbol)] -> Proof -> P Proof
copy [] Proof
b else forall (m :: * -> *) a. Monad m => a -> m a
return Proof
t
sub (Lam Symbol
s Proof
t) = 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) = 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 = 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) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Symbol -> Proof
Var forall a b. (a -> b) -> a -> b
$ forall b a. b -> (a -> b) -> Maybe a -> b
maybe Symbol
s forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ 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"
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Symbol -> Proof -> Proof
Lam Symbol
s') forall a b. (a -> b) -> a -> b
$ [(Symbol, Symbol)] -> Proof -> P Proof
copy ((Symbol
s, Symbol
s')forall a. a -> [a] -> [a]
:[(Symbol, Symbol)]
r) Proof
t
copy [(Symbol, Symbol)]
r (Apply Proof
t1 Proof
t2) = 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 = 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 = 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) (forall a b. (a -> b) -> [a] -> [b]
map Symbol -> Proof
Var [Symbol]
xs))) [Symbol]
xs
where xs :: [Symbol]
xs = [ String -> Symbol
Symbol (String
"x_" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i) | Int
i <- [Int
0 .. Int
nforall 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 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 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 forall a b. (a -> b) -> a -> b
$ Proof -> Proof -> Proof
Apply Proof
cdf forall a b. (a -> b) -> a -> b
$ Symbol -> Proof -> Proof
Lam Symbol
x forall a b. (a -> b) -> a -> b
$ Proof -> Proof -> Proof
Apply ([ConsDesc] -> Proof
Ccases []) 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 forall a b. (a -> b) -> a -> b
$ Proof -> Proof -> Proof
Apply Proof
cdf forall a b. (a -> b) -> a -> b
$ Symbol -> Proof -> Proof
Lam Symbol
c 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 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' forall a. a -> [a] -> [a]
: [Proof]
as)
spine (Lam Symbol
s Proof
e) [] = 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 forall a. Ord a => a -> a -> Bool
<= 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
aforall 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) | forall (t :: * -> *) a. Foldable t => t a -> Int
length [Proof]
as forall a. Ord a => a -> a -> Bool
>= Int
n = Proof -> [Proof] -> P Proof
spine (Proof -> Proof -> Proof
Apply ([Proof]
asforall a. [a] -> Int -> a
!!Int
i) Proof
x) (forall a. Int -> [a] -> [a]
drop Int
n [Proof]
as)
where n :: Int
n = forall (t :: * -> *) a. Foldable t => t a -> Int
length [ConsDesc]
cds
spine Proof
f [Proof]
as = forall (m :: * -> *) a. Monad m => a -> m a
return 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 = forall (m :: * -> *) a. Monad m => a -> m a
return
<*> :: forall a 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 = forall a. (PS -> [(PS, a)]) -> P a
P 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 = forall a. (PS -> [(PS, a)]) -> P a
P 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 <- 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) = forall a. (PS -> [(PS, a)]) -> P a
P 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 = forall (m :: * -> *) a. MonadPlus m => m a
mzero
<|> :: forall 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 = forall a. (PS -> [(PS, a)]) -> P a
P 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 = forall a. (PS -> [(PS, a)]) -> P a
P forall a b. (a -> b) -> a -> b
$ \ PS
s -> PS -> [(PS, a)]
fxs PS
s 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 = forall a. (PS -> [(PS, a)]) -> P a
P forall a b. (a -> b) -> a -> b
$ \ (PS Integer
i) -> [(Integer -> PS
PS (Integer
iforall a. Num a => a -> a -> a
+Integer
1), Integer
i)]
none :: P a
none :: forall a. P a
none = forall (m :: * -> *) a. MonadPlus m => m a
mzero
many :: [a] -> P a
many :: forall a. [a] -> P a
many [a]
xs = forall a. (PS -> [(PS, a)]) -> P a
P forall a b. (a -> b) -> a -> b
$ \ PS
s -> forall a b. [a] -> [b] -> [(a, b)]
zip (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) = forall a. (PS -> [(PS, a)]) -> P a
P forall a b. (a -> b) -> a -> b
$ \ PS
s -> 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) = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd (PS -> [(PS, a)]
m PS
startPS)
data AtomF = AtomF Term Symbol
deriving (AtomF -> AtomF -> Bool
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) = forall a. Show a => a -> String
show Proof
p forall a. [a] -> [a] -> [a]
++ String
":" forall a. [a] -> [a] -> [a]
++ 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 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 forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` AtomFs
as then AtomFs
as else AtomF
a forall a. a -> [a] -> [a]
: AtomFs
as
data AtomImp = AtomImp Symbol Antecedents
deriving (Int -> AtomImp -> ShowS
AtomImps -> ShowS
AtomImp -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: AtomImps -> ShowS
$cshowList :: AtomImps -> ShowS
show :: AtomImp -> String
$cshow :: AtomImp -> String
showsPrec :: Int -> AtomImp -> ShowS
$cshowsPrec :: Int -> AtomImp -> ShowS
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 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 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 forall a. Ord a => a -> a -> Ordering
compare Symbol
a Symbol
a' of
Ordering
GT -> AtomImp
atomImp forall a. a -> [a] -> [a]
: AtomImps -> AtomImp -> AtomImps
insert AtomImps
atomImps AtomImp
ai
Ordering
EQ -> Symbol -> Antecedents -> AtomImp
AtomImp Symbol
a (Antecedents
bs forall a. [a] -> [a] -> [a]
++ Antecedents
bs') forall a. a -> [a] -> [a]
: AtomImps
atomImps
Ordering
LT -> AtomImp
ai forall a. a -> [a] -> [a]
: AtomImps
aatomImps
data NestImp = NestImp Term Formula Formula Formula
deriving (NestImp -> NestImp -> Bool
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) = forall a. Show a => a -> String
show 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 forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` NestImps
ns then NestImps
ns else NestImp
n 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 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 forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Goal]
bs Bool -> Bool -> Bool
|| Goal
false forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Goal]
bs
nice_for NestImp
_ = Bool
False
(NestImps
good, NestImps
ok) = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition NestImp -> Bool
good_for NestImps
nestImps
(NestImps
nice, NestImps
bad) = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition NestImp -> Bool
nice_for NestImps
ok
in NestImps
good forall a. [a] -> [a] -> [a]
++ NestImps
nice forall a. [a] -> [a] -> [a]
++ NestImps
bad
newSym :: String -> P Symbol
newSym :: String -> P Symbol
newSym String
pre = do
Integer
i <- P Integer
nextInt
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ String -> Symbol
Symbol forall a b. (a -> b) -> a -> b
$ String
pre forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
i
select :: [a] -> P (a, [a])
select :: forall a. [a] -> P (a, [a])
select [a]
zs = forall a. [a] -> P a
many [ forall {a} {a}. (Eq a, Num a) => a -> [a] -> (a, [a])
del Int
n [a]
zs | Int
n <- [Int
0 .. forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
zs 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
nforall a. Num a => a -> a -> a
-a
1) [a]
xs in (a
y, a
xforall a. a -> [a] -> [a]
:[a]
ys)
del a
_ [a]
_ = forall a. HasCallStack => String -> a
error String
"select"
data Antecedent = A Term Formula deriving (Int -> Antecedent -> ShowS
Antecedents -> ShowS
Antecedent -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: Antecedents -> ShowS
$cshowList :: Antecedents -> ShowS
show :: Antecedent -> String
$cshow :: Antecedent -> String
showsPrec :: Int -> Antecedent -> ShowS
$cshowsPrec :: Int -> Antecedent -> ShowS
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 =
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) 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 =
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) forall a b. (a -> b) -> a -> b
$
if Goal
f forall a. Eq a => a -> a -> Bool
== Goal
g
then
if Bool
more
then forall (m :: * -> *) a. Monad m => a -> m a
return Proof
p 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 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] 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 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a b. a -> b -> a
const (String -> P Symbol
newSym String
"v")) [Goal]
bs
Proof
gp <- Antecedents -> Goal -> P Proof
redant0 (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 forall a. [a] -> [a] -> [a]
++ Antecedents
l) Goal
g
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Proof -> [Proof] -> Proof
applys (Int -> Proof
Csplit (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Goal]
bs)) [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 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a b. a -> b -> a
const (String -> P Symbol
newSym String
"d")) [(ConsDesc, Goal)]
ds
[Proof]
ps <- 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) (forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
vs [(ConsDesc, Goal)]
ds)
if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(ConsDesc, Goal)]
ds Bool -> Bool -> Bool
&& Goal
g forall a. Eq a => a -> a -> Bool
== [(ConsDesc, Goal)] -> Goal
Disj []
then forall (m :: * -> *) a. Monad m => a -> m a
return Proof
p
else forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Proof -> [Proof] -> Proof
applys ([ConsDesc] -> Proof
Ccases (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(ConsDesc, Goal)]
ds)) (Proof
p forall a. a -> [a] -> [a]
: 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 =
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) 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 = 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 (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 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a b. a -> b -> a
const (String -> P Symbol
newSym String
"d")) [(ConsDesc, Goal)]
ds
Proof
gp <- Antecedents -> Goal -> P Proof
redant0 (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 forall a. [a] -> [a] -> [a]
++ Antecedents
l) Goal
g
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 (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 =
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) 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 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) 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 =
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) 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 <- forall a. Bool -> P a -> P a
cutSearch Bool
more forall a b. (a -> b) -> a -> b
$ 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
forall a. String -> a -> a
mtrace String
"redantimpatom: LLL" 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
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus`
(forall a. String -> a -> a
mtrace String
"redantimpatom: RRR" 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 =
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) 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) =
(forall a. Bool -> P a -> P a
cutSearch Bool
more forall a b. (a -> b) -> a -> b
$ forall a. [a] -> P a
many (Symbol -> AtomFs -> [Proof]
findAtoms Symbol
s AtomFs
atoms))
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 forall a. P a
none)
redsucc' (Conj [Goal]
cs) = do
[Proof]
ps <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Goal -> P Proof
redsucc [Goal]
cs
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Proof -> [Proof] -> Proof
applys (Int -> Proof
Ctuple (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) forall a b. (a -> b) -> a -> b
$ Goal
d Goal -> Goal -> Goal
:-> Goal
v | (Int
i, (ConsDesc
cd, Goal
d)) <- 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
forall (m :: * -> *) a. Monad m => a -> m a
return 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 =
forall a b (m :: * -> *).
(Show a, Show b, Monad m) =>
String -> a -> m b -> m b
wrapM String
"redsucc_choice" Goal
g 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) <-
forall a. String -> a -> a
mtrace (String
"redsucc_choice: order=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show NestImps
ordImps) forall a b. (a -> b) -> a -> b
$
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) 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 = 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 = 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) = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Symbol -> Goal -> Bool
posin3 Symbol
g) (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(ConsDesc, Goal)]
as)
posin3 Symbol
g (Conj [Goal]
as) = 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 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 = forall a. P a -> P a
atMostOne P a
p
cutSearch Bool
True P a
p = P a
p