--
-- Copyright (c) 2005, 2008 Lennart Augustsson
-- See LICENSE for licensing details.
--
-- Intuitionistic theorem prover
-- Written by Roy Dyckhoff, Summer 1991
-- Modified to use the LWB syntax  Summer 1997
-- and simplified in various ways...
--
-- Translated to Haskell by Lennart Augustsson December 2005
--
-- Incorporates the Vorob'ev-Hudelmaier etc calculus (I call it LJT)
-- See RD's paper in JSL 1992:
-- "Contraction-free calculi for intuitionistic logic"
--
-- Torkel Franzen (at SICS) gave me good ideas about how to write this
-- properly, taking account of first-argument indexing,
-- and I learnt a trick or two from Neil Tennant's "Autologic" book.

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 :: 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
-- wrap :: (Show a, Show b) => String -> a -> b -> b
-- wrap fun args ret = mtrace (fun ++ ": " ++ show args) $
--                     let o = show ret in seq o $
--                     mtrace (fun ++ " returns: " ++ o) ret
wrapM :: (Show a, Show b, Monad m) => String -> a -> m b -> m b
wrapM :: 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 :: Formula -> Bool
provable Formula
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, Formula)] -> Formula -> [Proof]
prove Bool
False [] Formula
a

prove :: MoreSolutions -> [(Symbol, Formula)] -> Formula -> [Proof]
prove :: Bool -> [(Symbol, Formula)] -> Formula -> [Proof]
prove Bool
more [(Symbol, Formula)]
env Formula
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, Formula)] -> Formula -> P Proof
redtop Bool
more [(Symbol, Formula)]
env Formula
a

redtop :: MoreSolutions -> [(Symbol, Formula)] -> Formula -> P Proof
redtop :: Bool -> [(Symbol, Formula)] -> Formula -> P Proof
redtop Bool
more [(Symbol, Formula)]
ifs Formula
a = do
  let form :: Formula
form = (Formula -> Formula -> Formula) -> Formula -> [Formula] -> Formula
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Formula -> Formula -> Formula
(:->) Formula
a (((Symbol, Formula) -> Formula) -> [(Symbol, Formula)] -> [Formula]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol, Formula) -> Formula
forall a b. (a, b) -> b
snd [(Symbol, Formula)]
ifs)
  Proof
p <- Bool
-> Antecedents
-> AtomImps
-> NestImps
-> AtomFs
-> Formula
-> P Proof
redant Bool
more [] [] [] [] Formula
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, Formula) -> Proof) -> [(Symbol, Formula)] -> [Proof]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol -> Proof
Var (Symbol -> Proof)
-> ((Symbol, Formula) -> Symbol) -> (Symbol, Formula) -> Proof
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, Formula) -> Symbol
forall a b. (a, b) -> a
fst) [(Symbol, Formula)]
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

------------------------------

-- XXX The symbols used in the functions below must not clash
-- XXX with any symbols from newSym.

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"

-- ((c->d)->false) -> ((c->false)->false, d->false)
-- p : (c->d)->false)
-- replace p1 and p2 with the components of the pair
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

------------------------------

-- More simplifications:
--  split where no variables used can be removed
--  either with equal RHS can me merged.

-- Compute the normal form
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


------------------------------
----- Our Proof monad, P, a monad with state and multiple results

-- Note, this is the non-standard way to combine state with multiple
-- results.  But this is much better for backtracking.
newtype P a = P { P a -> PS -> [(PS, a)]
unP :: PS -> [(PS, a)] }

instance Applicative P where
  pure :: a -> P a
pure  = a -> P a
forall (m :: * -> *) a. Monad m => a -> m a
return
  <*> :: 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 :: 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 >>= :: 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 :: (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 :: P a
empty = P a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  <|> :: 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 :: 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 :: 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

-- The state, just an integer for generating new variables
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 :: P a
none = P a
forall (m :: * -> *) a. MonadPlus m => m a
mzero

many :: [a] -> P a
many :: [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 :: 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 :: 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)


------------------------------
----- Atomic formulae

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' ]

--removeAtom :: Symbol -> AtomFs -> AtomFs
--removeAtom s atoms = [ a | a@(AtomF _ s') <- atoms, s /= 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

------------------------------
----- Implications of one atom

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)
extract :: AtomImps -> Symbol -> (Antecedents, AtomImps)
extract 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

------------------------------
----- Nested implications, (a -> b) -> c

data NestImp = NestImp Term Formula Formula Formula -- NestImp a b c represents (a :-> b) :-> c
             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
_ Formula
a Formula
b Formula
c) = Formula -> String
forall a. Show a => a -> String
show (Formula -> String) -> Formula -> String
forall a b. (a -> b) -> a -> b
$ (Formula
a Formula -> Formula -> Formula
:-> Formula
b) Formula -> Formula -> Formula
:-> Formula
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

------------------------------
----- Ordering of nested implications
heuristics :: Bool
heuristics :: Bool
heuristics = Bool
True

order :: NestImps -> Formula -> AtomImps -> NestImps
order :: NestImps -> Formula -> AtomImps -> NestImps
order NestImps
nestImps Formula
g AtomImps
atomImps =
  if Bool
heuristics
     then NestImps
nestImps
     else let good_for :: NestImp -> Bool
good_for (NestImp Proof
_ Formula
_ Formula
_ (Disj [])) = Bool
True
              good_for (NestImp Proof
_ Formula
_ Formula
_ Formula
g')        = Formula
g Formula -> Formula -> Bool
forall a. Eq a => a -> a -> Bool
== Formula
g'
              nice_for :: NestImp -> Bool
nice_for (NestImp Proof
_ Formula
_ Formula
_ (PVar Symbol
s)) =
                case AtomImps -> Symbol -> (Antecedents, AtomImps)
extract AtomImps
atomImps Symbol
s of
                  (Antecedents
bs', AtomImps
_) -> let bs :: [Formula]
bs = [ Formula
b | A Proof
_ Formula
b <- Antecedents
bs'] in Formula
g Formula -> [Formula] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Formula]
bs Bool -> Bool -> Bool
|| Formula
false Formula -> [Formula] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Formula]
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

------------------------------
----- Generate a new unique variable
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

------------------------------
----- Generate all ways to select one element of a list
select :: [a] -> P (a, [a])
select :: [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

--
-- This is the main loop of the proof search.
--
-- The redant functions reduce antecedents and the redsucc
-- function reduces the goal (succedent).
--
-- The antecedents are kept in four groups: Antecedents, AtomImps, NestImps, AtomFs
--   Antecedents contains as yet unclassified antecedents; the redant functions
--     go through them one by one and reduces and classifies them.
--   AtomImps contains implications of the form (a -> b), where `a' is an atom.
--     To speed up the processing it is stored as a map from the `a' to all the
--     formulae it implies.
--   NestImps contains implications of the form ((b -> c) -> d)
--   AtomFs contains atomic formulae.
--
-- There is also a proof object associated with each antecedent.
--
redant :: MoreSolutions -> Antecedents -> AtomImps -> NestImps -> AtomFs -> Goal -> P Proof
redant :: Bool
-> Antecedents
-> AtomImps
-> NestImps
-> AtomFs
-> Formula
-> P Proof
redant Bool
more Antecedents
antes AtomImps
atomImps NestImps
nestImps AtomFs
atoms Formula
goal =
  String
-> (Antecedents, AtomImps, NestImps, AtomFs, Formula)
-> 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, Formula
goal) (P Proof -> P Proof) -> P Proof -> P Proof
forall a b. (a -> b) -> a -> b
$
    case Antecedents
antes of
      [] -> Formula -> P Proof
redsucc Formula
goal
      Antecedent
a:Antecedents
l -> Antecedent -> Antecedents -> Formula -> P Proof
redant1 Antecedent
a Antecedents
l Formula
goal
  where redant0 :: Antecedents -> Formula -> P Proof
redant0 Antecedents
l Formula
g = Bool
-> Antecedents
-> AtomImps
-> NestImps
-> AtomFs
-> Formula
-> P Proof
redant Bool
more Antecedents
l AtomImps
atomImps NestImps
nestImps AtomFs
atoms Formula
g
        redant1 :: Antecedent -> Antecedents -> Goal -> P Proof
        redant1 :: Antecedent -> Antecedents -> Formula -> P Proof
redant1 a :: Antecedent
a@(A Proof
p Formula
f) Antecedents
l Formula
g =
          String
-> ((Antecedent, Antecedents), AtomImps, NestImps, AtomFs, Formula)
-> 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, Formula
g) (P Proof -> P Proof) -> P Proof -> P Proof
forall a b. (a -> b) -> a -> b
$
          if Formula
f Formula -> Formula -> Bool
forall a. Eq a => a -> a -> Bool
== Formula
g
             then -- The goal is the antecedent, we're done.
               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 -> Formula -> P Proof
redant1' Antecedent
a Antecedents
l Formula
g
                  else Proof -> P Proof
forall (m :: * -> *) a. Monad m => a -> m a
return Proof
p
             else Antecedent -> Antecedents -> Formula -> P Proof
redant1' Antecedent
a Antecedents
l Formula
g

        -- Reduce the first antecedent
        redant1' :: Antecedent -> Antecedents -> Goal -> P Proof
        redant1' :: Antecedent -> Antecedents -> Formula -> P Proof
redant1' (A Proof
p (PVar Symbol
s)) Antecedents
l Formula
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
-> Formula
-> P Proof
redant Bool
more ([Proof -> Formula -> Antecedent
A (Proof -> Proof -> Proof
Apply Proof
f Proof
p) Formula
b | A Proof
f Formula
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) Formula
g
        redant1' (A Proof
p (Conj [Formula]
bs)) Antecedents
l Formula
g = do
          [Symbol]
vs <- (Formula -> P Symbol) -> [Formula] -> P [Symbol]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (P Symbol -> Formula -> P Symbol
forall a b. a -> b -> a
const (String -> P Symbol
newSym String
"v")) [Formula]
bs
          Proof
gp <- Antecedents -> Formula -> P Proof
redant0 ((Symbol -> Formula -> Antecedent)
-> [Symbol] -> [Formula] -> Antecedents
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ Symbol
v Formula
a -> Proof -> Formula -> Antecedent
A (Symbol -> Proof
Var Symbol
v) Formula
a) [Symbol]
vs [Formula]
bs Antecedents -> Antecedents -> Antecedents
forall a. [a] -> [a] -> [a]
++ Antecedents
l) Formula
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 ([Formula] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Formula]
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, Formula)]
ds)) Antecedents
l Formula
g = do
          [Symbol]
vs <- ((ConsDesc, Formula) -> P Symbol)
-> [(ConsDesc, Formula)] -> P [Symbol]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (P Symbol -> (ConsDesc, Formula) -> P Symbol
forall a b. a -> b -> a
const (String -> P Symbol
newSym String
"d")) [(ConsDesc, Formula)]
ds
          [Proof]
ps <- ((Symbol, (ConsDesc, Formula)) -> P Proof)
-> [(Symbol, (ConsDesc, Formula))] -> P [Proof]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ (Symbol
v, (ConsDesc
_, Formula
d)) -> Antecedent -> Antecedents -> Formula -> P Proof
redant1 (Proof -> Formula -> Antecedent
A (Symbol -> Proof
Var Symbol
v) Formula
d) Antecedents
l Formula
g) ([Symbol]
-> [(ConsDesc, Formula)] -> [(Symbol, (ConsDesc, Formula))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
vs [(ConsDesc, Formula)]
ds)
          if [(ConsDesc, Formula)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(ConsDesc, Formula)]
ds Bool -> Bool -> Bool
&& Formula
g Formula -> Formula -> Bool
forall a. Eq a => a -> a -> Bool
== [(ConsDesc, Formula)] -> Formula
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, Formula) -> ConsDesc)
-> [(ConsDesc, Formula)] -> [ConsDesc]
forall a b. (a -> b) -> [a] -> [b]
map (ConsDesc, Formula) -> ConsDesc
forall a b. (a, b) -> a
fst [(ConsDesc, Formula)]
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 (Formula
a :-> Formula
b)) Antecedents
l Formula
g = Proof -> Formula -> Formula -> Antecedents -> Formula -> P Proof
redantimp Proof
p Formula
a Formula
b Antecedents
l Formula
g

        redantimp :: Term -> Formula -> Formula -> Antecedents -> Goal -> P Proof
        redantimp :: Proof -> Formula -> Formula -> Antecedents -> Formula -> P Proof
redantimp Proof
t Formula
c Formula
d Antecedents
a Formula
g =
          String
-> (Formula, Formula, Antecedents, Formula) -> P Proof -> P Proof
forall a b (m :: * -> *).
(Show a, Show b, Monad m) =>
String -> a -> m b -> m b
wrapM String
"redantimp" (Formula
c,Formula
d,Antecedents
a,Formula
g) (P Proof -> P Proof) -> P Proof -> P Proof
forall a b. (a -> b) -> a -> b
$
          Proof -> Formula -> Formula -> Antecedents -> Formula -> P Proof
redantimp' Proof
t Formula
c Formula
d Antecedents
a Formula
g

        -- Reduce an implication antecedent
        redantimp' :: Term -> Formula -> Formula -> Antecedents -> Goal -> P Proof
        -- p : PVar s -> b
        redantimp' :: Proof -> Formula -> Formula -> Antecedents -> Formula -> P Proof
redantimp' Proof
p (PVar Symbol
s) Formula
b Antecedents
l Formula
g = Proof -> Symbol -> Formula -> Antecedents -> Formula -> P Proof
redantimpatom Proof
p Symbol
s Formula
b Antecedents
l Formula
g
        -- p : (c & d) -> b
        redantimp' Proof
p (Conj [Formula]
cs) Formula
b Antecedents
l Formula
g = do
          Symbol
x <- String -> P Symbol
newSym String
"x"
          let imp :: Formula
imp = (Formula -> Formula -> Formula) -> Formula -> [Formula] -> Formula
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Formula -> Formula -> Formula
(:->) Formula
b [Formula]
cs
          Proof
gp <- Antecedent -> Antecedents -> Formula -> P Proof
redant1 (Proof -> Formula -> Antecedent
A (Symbol -> Proof
Var Symbol
x) Formula
imp) Antecedents
l Formula
g
          Proof -> Symbol -> Proof -> P Proof
subst (Int -> Proof -> Proof
curryt ([Formula] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Formula]
cs) Proof
p) Symbol
x Proof
gp
        -- p : (c | d) -> b
        redantimp' Proof
p (Disj [(ConsDesc, Formula)]
ds) Formula
b Antecedents
l Formula
g = do
          [Symbol]
vs <- ((ConsDesc, Formula) -> P Symbol)
-> [(ConsDesc, Formula)] -> P [Symbol]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (P Symbol -> (ConsDesc, Formula) -> P Symbol
forall a b. a -> b -> a
const (String -> P Symbol
newSym String
"d")) [(ConsDesc, Formula)]
ds
          Proof
gp <- Antecedents -> Formula -> P Proof
redant0 ((Symbol -> (ConsDesc, Formula) -> Antecedent)
-> [Symbol] -> [(ConsDesc, Formula)] -> Antecedents
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ Symbol
v (ConsDesc
_, Formula
d) -> Proof -> Formula -> Antecedent
A (Symbol -> Proof
Var Symbol
v) (Formula
d Formula -> Formula -> Formula
:-> Formula
b)) [Symbol]
vs [(ConsDesc, Formula)]
ds Antecedents -> Antecedents -> Antecedents
forall a. [a] -> [a] -> [a]
++ Antecedents
l) Formula
g
          (Proof -> (Int, Symbol, (ConsDesc, Formula)) -> P Proof)
-> Proof -> [(Int, Symbol, (ConsDesc, Formula))] -> 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, Formula
_)) -> 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, Formula)]
-> [(Int, Symbol, (ConsDesc, Formula))]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Int
0..] [Symbol]
vs [(ConsDesc, Formula)]
ds)
        -- p : (c -> d) -> b
        redantimp' Proof
p (Formula
c :-> Formula
d) Formula
b Antecedents
l Formula
g = Proof
-> Formula
-> Formula
-> Formula
-> Antecedents
-> Formula
-> P Proof
redantimpimp Proof
p Formula
c Formula
d Formula
b Antecedents
l Formula
g

        redantimpimp :: Term -> Formula -> Formula -> Formula -> Antecedents -> Goal -> P Proof
        redantimpimp :: Proof
-> Formula
-> Formula
-> Formula
-> Antecedents
-> Formula
-> P Proof
redantimpimp Proof
f Formula
b Formula
c Formula
d Antecedents
a Formula
g =
          String
-> (Formula, Formula, Formula, Antecedents, Formula)
-> P Proof
-> P Proof
forall a b (m :: * -> *).
(Show a, Show b, Monad m) =>
String -> a -> m b -> m b
wrapM String
"redantimpimp" (Formula
b,Formula
c,Formula
d,Antecedents
a,Formula
g) (P Proof -> P Proof) -> P Proof -> P Proof
forall a b. (a -> b) -> a -> b
$
          Proof
-> Formula
-> Formula
-> Formula
-> Antecedents
-> Formula
-> P Proof
redantimpimp' Proof
f Formula
b Formula
c Formula
d Antecedents
a Formula
g

        -- Reduce a double implication antecedent
        redantimpimp' :: Term -> Formula -> Formula -> Formula -> Antecedents -> Goal -> P Proof
        -- next clause exploits ~(C->D) <=> (~~C & ~D)
        -- which isn't helpful when D = false
        redantimpimp' :: Proof
-> Formula
-> Formula
-> Formula
-> Antecedents
-> Formula
-> P Proof
redantimpimp' Proof
p Formula
c Formula
d (Disj []) Antecedents
l Formula
g | Formula
d Formula -> Formula -> Bool
forall a. Eq a => a -> a -> Bool
/= Formula
false = do
          Symbol
x <- String -> P Symbol
newSym String
"x"
          Symbol
y <- String -> P Symbol
newSym String
"y"
          Proof
gp <- Proof
-> Formula
-> Formula
-> Formula
-> Antecedents
-> Formula
-> P Proof
redantimpimp (Symbol -> Proof
Var Symbol
x) Formula
c Formula
false Formula
false (Proof -> Formula -> Antecedent
A (Symbol -> Proof
Var Symbol
y) (Formula
d Formula -> Formula -> Formula
:-> Formula
false) Antecedent -> Antecedents -> Antecedents
forall a. a -> [a] -> [a]
: Antecedents
l) Formula
g
          Symbol -> Symbol -> Proof -> Proof -> P Proof
cImpDImpFalse Symbol
x Symbol
y Proof
p Proof
gp
        -- p : (c -> d) -> b
        redantimpimp' Proof
p Formula
c Formula
d Formula
b Antecedents
l Formula
g = Bool
-> Antecedents
-> AtomImps
-> NestImps
-> AtomFs
-> Formula
-> P Proof
redant Bool
more Antecedents
l AtomImps
atomImps (NestImp -> NestImps -> NestImps
addNestImp (Proof -> Formula -> Formula -> Formula -> NestImp
NestImp Proof
p Formula
c Formula
d Formula
b) NestImps
nestImps) AtomFs
atoms Formula
g

        -- Reduce an atomic implication
        redantimpatom :: Term -> Symbol -> Formula -> Antecedents -> Goal -> P Proof
        redantimpatom :: Proof -> Symbol -> Formula -> Antecedents -> Formula -> P Proof
redantimpatom Proof
p Symbol
s Formula
b Antecedents
l Formula
g =
          String
-> (Symbol, Formula, Antecedents, Formula) -> 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,Formula
b,Antecedents
l,Formula
g) (P Proof -> P Proof) -> P Proof -> P Proof
forall a b. (a -> b) -> a -> b
$
          Proof -> Symbol -> Formula -> Antecedents -> Formula -> P Proof
redantimpatom' Proof
p Symbol
s Formula
b Antecedents
l Formula
g

        redantimpatom' :: Term -> Symbol -> Formula -> Antecedents -> Goal -> P Proof
        redantimpatom' :: Proof -> Symbol -> Formula -> Antecedents -> Formula -> P Proof
redantimpatom' Proof
p Symbol
s Formula
b Antecedents
l Formula
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 -> Formula -> P Proof
redant1 (Proof -> Formula -> Antecedent
A (Symbol -> Proof
Var Symbol
x) Formula
b) Antecedents
l Formula
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
-> Formula
-> P Proof
redant Bool
more Antecedents
l (AtomImps -> AtomImp -> AtomImps
insert AtomImps
atomImps (Symbol -> Antecedents -> AtomImp
AtomImp Symbol
s [Proof -> Formula -> Antecedent
A Proof
p Formula
b])) NestImps
nestImps AtomFs
atoms Formula
g)

        -- Reduce the goal, with all antecedents already being classified
        redsucc :: Goal -> P Proof
        redsucc :: Formula -> P Proof
redsucc Formula
g =
          String
-> (Formula, 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" (Formula
g, AtomImps
atomImps, NestImps
nestImps, AtomFs
atoms) (P Proof -> P Proof) -> P Proof -> P Proof
forall a b. (a -> b) -> a -> b
$
          Formula -> P Proof
redsucc' Formula
g

        redsucc' :: Goal -> P Proof
        redsucc' :: Formula -> P Proof
redsucc' a :: Formula
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`
            -- The posin check is an optimization.  It gets a little slower without the test.
            (if Symbol -> AtomImps -> NestImps -> Bool
posin Symbol
s AtomImps
atomImps NestImps
nestImps then Formula -> P Proof
redsucc_choice Formula
a else P Proof
forall a. P a
none)
        redsucc' (Conj [Formula]
cs) = do
          [Proof]
ps <- (Formula -> P Proof) -> [Formula] -> P [Proof]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Formula -> P Proof
redsucc [Formula]
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 ([Formula] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Formula]
cs)) [Proof]
ps
        -- next clause deals with succedent (A v B) by pushing the
        -- non-determinism into the treatment of implication on the left
        redsucc' (Disj [(ConsDesc, Formula)]
ds) = do
          Symbol
s1 <- String -> P Symbol
newSym String
"_"
          let v :: Formula
v = Symbol -> Formula
PVar Symbol
s1
          Antecedents -> Formula -> P Proof
redant0 [ Proof -> Formula -> Antecedent
A (ConsDesc -> Int -> Proof
Cinj ConsDesc
cd Int
i) (Formula -> Antecedent) -> Formula -> Antecedent
forall a b. (a -> b) -> a -> b
$ Formula
d Formula -> Formula -> Formula
:-> Formula
v | (Int
i, (ConsDesc
cd, Formula
d)) <- [Int] -> [(ConsDesc, Formula)] -> [(Int, (ConsDesc, Formula))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [(ConsDesc, Formula)]
ds ] Formula
v
        redsucc' (Formula
a :-> Formula
b) = do
          Symbol
s <- String -> P Symbol
newSym String
"x"
          Proof
p <- Antecedent -> Antecedents -> Formula -> P Proof
redant1 (Proof -> Formula -> Antecedent
A (Symbol -> Proof
Var Symbol
s) Formula
a) [] Formula
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

        -- Now we have the hard part; maybe lots of formulae
        -- of form (C->D)->B  in nestImps to choose from!
        -- Which one to take first? We use the order heuristic.
        redsucc_choice :: Goal -> P Proof
        redsucc_choice :: Formula -> P Proof
redsucc_choice Formula
g =
          String -> Formula -> P Proof -> P Proof
forall a b (m :: * -> *).
(Show a, Show b, Monad m) =>
String -> a -> m b -> m b
wrapM String
"redsucc_choice" Formula
g (P Proof -> P Proof) -> P Proof -> P Proof
forall a b. (a -> b) -> a -> b
$
          Formula -> P Proof
redsucc_choice' Formula
g

        redsucc_choice' :: Goal -> P Proof
        redsucc_choice' :: Formula -> P Proof
redsucc_choice' Formula
g = do
          let ordImps :: NestImps
ordImps = NestImps -> Formula -> AtomImps -> NestImps
order NestImps
nestImps Formula
g AtomImps
atomImps
          (NestImp Proof
p Formula
c Formula
d Formula
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
-> Formula
-> P Proof
redant Bool
more [Proof -> Formula -> Antecedent
A (Symbol -> Proof
Var Symbol
z) (Formula -> Antecedent) -> Formula -> Antecedent
forall a b. (a -> b) -> a -> b
$ Formula
d Formula -> Formula -> Formula
:-> Formula
b] AtomImps
atomImps NestImps
restImps AtomFs
atoms (Formula
c Formula -> Formula -> Formula
:-> Formula
d)
          Proof
gp <- Bool
-> Antecedents
-> AtomImps
-> NestImps
-> AtomFs
-> Formula
-> P Proof
redant Bool
more [Proof -> Formula -> Antecedent
A (Symbol -> Proof
Var Symbol
x) Formula
b] AtomImps
atomImps NestImps
restImps AtomFs
atoms Formula
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 -> [Formula] -> Bool
posin2 Symbol
g [ (Formula
a Formula -> Formula -> Formula
:-> Formula
b) Formula -> Formula -> Formula
:-> Formula
c | NestImp Proof
_ Formula
a Formula
b Formula
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 -> [Formula] -> Bool
posin2 Symbol
g [ Formula
b | A Proof
_ Formula
b <- Antecedents
bs]) AtomImps
atomImps

posin2 :: Symbol -> [Formula] -> Bool
posin2 :: Symbol -> [Formula] -> Bool
posin2 Symbol
g [Formula]
bs = (Formula -> Bool) -> [Formula] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Symbol -> Formula -> Bool
posin3 Symbol
g) [Formula]
bs

posin3 :: Symbol -> Formula -> Bool
posin3 :: Symbol -> Formula -> Bool
posin3 Symbol
g (Disj [(ConsDesc, Formula)]
as) = (Formula -> Bool) -> [Formula] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Symbol -> Formula -> Bool
posin3 Symbol
g) (((ConsDesc, Formula) -> Formula)
-> [(ConsDesc, Formula)] -> [Formula]
forall a b. (a -> b) -> [a] -> [b]
map (ConsDesc, Formula) -> Formula
forall a b. (a, b) -> b
snd [(ConsDesc, Formula)]
as)
posin3 Symbol
g (Conj [Formula]
as) = (Formula -> Bool) -> [Formula] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Symbol -> Formula -> Bool
posin3 Symbol
g) [Formula]
as
posin3 Symbol
g (Formula
_ :-> Formula
b) = Symbol -> Formula -> Bool
posin3 Symbol
g Formula
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 :: 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

---------------------------