    --
    -- 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 m :: String
    m x :: 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 fun :: String
    fun args :: a
    args mret :: 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
    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]
    ++ " 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 a :: 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 more :: Bool
    more env :: [(Symbol, Formula)]
    env a :: 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 more :: Bool
    more ifs :: [(Symbol, Formula)]
    ifs a :: 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 b :: Proof
    b x :: Symbol
    x term :: Proof
    term = Proof -> P Proof
    sub Proof
    term
      where sub :: Proof -> P Proof
    sub t :: Proof
    t@(Var s' :: 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 s :: Symbol
    s t :: 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 t1 :: Proof
    t1 t2 :: 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 t :: 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 r :: [(Symbol, Symbol)]
    r (Var s :: 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 r :: [(Symbol, Symbol)]
    r (Lam s :: Symbol
    s t :: Proof
    t)     = do
        Symbol
    s' <- String -> P Symbol
    newSym "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 r :: [(Symbol, Symbol)]
    r (Apply t1 :: Proof
    t1 t2 :: 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 _r :: [(Symbol, Symbol)]
    _r t :: 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 f :: Proof
    f a :: Proof
    a = Proof -> Proof -> Proof
    Apply Proof
    f Proof
    a

    curryt :: Int -> Term -> Term
    curryt :: Int -> Proof -> Proof
    curryt n :: Int
    n p :: 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 ("x_" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    i) | Int
    i <- [0 .. Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -1] ]

    inj :: ConsDesc -> Int -> Term -> Term
    inj :: ConsDesc -> Int -> Proof -> Proof
    inj cd :: ConsDesc
    cd i :: Int
    i p :: 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 "x"

    applyImp :: Term -> Term -> Term
    applyImp :: Proof -> Proof -> Proof
    applyImp p :: Proof
    p q :: 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 "x"
            y :: Symbol
    y = String -> Symbol
    Symbol "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 p1 :: Symbol
    p1 p2 :: Symbol
    p2 cdf :: Proof
    cdf gp :: 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 "cf"
          x :: Symbol
    x = String -> Symbol
    Symbol "x"
          d :: Symbol
    d = String -> Symbol
    Symbol "d"
          c :: Symbol
    c = String -> Symbol
    Symbol "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 ee :: Proof
    ee = Proof -> [Proof] -> P Proof
    spine Proof
    ee []
      where spine :: Proof -> [Proof] -> P Proof
    spine (Apply f :: Proof
    f a :: Proof
    a) as :: [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 s :: Symbol
    s e :: 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 s :: Symbol
    s e :: Proof
    e) (a :: Proof
    a : as :: [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 n :: Int
    n) (b :: Proof
    b : tup :: Proof
    tup : args :: [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 (istup :: Bool
    istup, xs :: [Proof]
    xs) = Proof -> (Bool, [Proof])
    getTup Proof
    tup
                    getTup :: Proof -> (Bool, [Proof])
    getTup (Ctuple _)  = (Bool
    True, [])
                    getTup (Apply f :: Proof
    f a :: Proof
    a) = let (tf :: Bool
    tf, as :: [Proof]
    as) = Proof -> (Bool, [Proof])
    getTup Proof
    f in (Bool
    tf, Proof
    aProof -> [Proof] -> [Proof]
    forall a. a -> [a] -> [a]
    :[Proof]
    as)
                    getTup _ = (Bool
    False, [])
            spine (Ccases []) (e :: Proof
    e@(Apply (Ccases []) _) : as :: [Proof]
    as) = Proof -> [Proof] -> P Proof
    spine Proof
    e [Proof]
    as
            spine (Ccases cds :: [ConsDesc]
    cds) (Apply (Cinj _ i :: Int
    i) x :: Proof
    x : as :: [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 f :: Proof
    f as :: [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 x :: 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
    $ \ s :: PS
    s -> [(PS
    s, a
    x)]
      P m :: PS -> [(PS, a)]
    m >>= :: P a -> (a -> P b) -> P b
    >>= f :: 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
    $ \ s :: PS
    s -> [ (PS, b)
    y | (s' :: PS
    s',x :: 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 f :: a -> b
    f (P m :: 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
    $ \ s :: PS
    s -> [ (PS
    s', a -> b
    f a
    x) | (s' :: PS
    s', x :: 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
    $ \ _s :: PS
    _s -> []
      P fxs :: PS -> [(PS, a)]
    fxs mplus :: P a -> P a -> P a
    `mplus` P fys :: 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
    $ \ s :: 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 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 i :: Integer
    i) -> [(Integer -> PS
    PS (Integer
    iInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    +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 xs :: [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
    $ \ s :: 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 f :: 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
    $ \ s :: PS
    s -> Int -> [(PS, a)] -> [(PS, a)]
    forall a. Int -> [a] -> [a]
    take 1 (PS -> [(PS, a)]
    f PS
    s)

    runP :: P a -> [a]
    runP :: P a -> [a]
    runP (P m :: 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 p :: Proof
    p s :: Symbol
    s) = Proof -> String
    forall a. Show a => a -> String
    show Proof
    p String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ":" 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 s :: Symbol
    s atoms :: AtomFs
    atoms = [ Proof
    p | AtomF p :: Proof
    p s' :: 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 a :: AtomF
    a as :: 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 a' :: Symbol
    a' bs :: Antecedents
    bs) : atomImps :: AtomImps
    atomImps) a :: Symbol
    a =
      case Symbol -> Symbol -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare Symbol
    a Symbol
    a' of
        GT -> let (rbs :: Antecedents
    rbs, restImps :: 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)
        EQ -> (Antecedents
    bs, AtomImps
    atomImps)
        LT -> ([], AtomImps
    aatomImps)
    extract _ _ = ([], [])

    insert :: AtomImps -> AtomImp -> AtomImps
    insert :: AtomImps -> AtomImp -> AtomImps
    insert [] ai :: AtomImp
    ai = [ AtomImp
    ai ]
    insert aatomImps :: AtomImps
    aatomImps@(atomImp :: AtomImp
    atomImp@(AtomImp a' :: Symbol
    a' bs' :: Antecedents
    bs') : atomImps :: AtomImps
    atomImps) ai :: AtomImp
    ai@(AtomImp a :: Symbol
    a bs :: Antecedents
    bs) =
      case Symbol -> Symbol -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare Symbol
    a Symbol
    a' of
        GT -> AtomImp
    atomImp AtomImp -> AtomImps -> AtomImps
    forall a. a -> [a] -> [a]
    : AtomImps -> AtomImp -> AtomImps
    insert AtomImps
    atomImps AtomImp
    ai
        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
        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 _ a :: Formula
    a b :: Formula
    b c :: 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 n :: NestImp
    n ns :: 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
    nestImps g :: Formula
    g atomImps :: AtomImps
    atomImps =
      if Bool
    heuristics
         then NestImps
    nestImps
         else let good_for :: NestImp -> Bool
    good_for (NestImp _ _ _ (Disj [])) = Bool
    True
                  good_for (NestImp _ _ _ g' :: Formula
    g')        = Formula
    g Formula -> Formula -> Bool
    forall a. Eq a => a -> a -> Bool
    == Formula
    g'
                  nice_for :: NestImp -> Bool
    nice_for (NestImp _ _ _ (PVar s :: Symbol
    s)) =
                    case AtomImps -> Symbol -> (Antecedents, AtomImps)
    extract AtomImps
    atomImps Symbol
    s of
                      (bs' :: Antecedents
    bs', _) -> let bs :: [Formula]
    bs = [ Formula
    b | A _ b :: 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 _ = Bool
    False
                  (good :: NestImps
    good, ok :: NestImps
    ok) = (NestImp -> Bool) -> NestImps -> (NestImps, NestImps)
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    partition NestImp -> Bool
    good_for NestImps
    nestImps
                  (nice :: NestImps
    nice, bad :: 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 pre :: 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 zs :: [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 <- [0 .. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [a]
    zs Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1] ]
      where del :: a -> [a] -> (a, [a])
    del 0 (x :: a
    x:xs :: [a]
    xs) = (a
    x, [a]
    xs)
            del n :: a
    n (x :: a
    x:xs :: [a]
    xs) = let (y :: a
    y,ys :: [a]
    ys) = a -> [a] -> (a, [a])
    del (a
    na -> a -> a
    forall a. Num a => a -> a -> a
    -1) [a]
    xs in (a
    y, a
    xa -> [a] -> [a]
    forall a. a -> [a] -> [a]
    :[a]
    ys)
            del _ _ = String -> (a, [a])
    forall a. HasCallStack => String -> a
    error "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 more :: Bool
    more antes :: Antecedents
    antes atomImps :: AtomImps
    atomImps nestImps :: NestImps
    nestImps atoms :: AtomFs
    atoms goal :: 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 "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
          a :: Antecedent
    a:l :: Antecedents
    l -> Antecedent -> Antecedents -> Formula -> P Proof
    redant1 Antecedent
    a Antecedents
    l Formula
    goal
      where redant0 :: Antecedents -> Formula -> P Proof
    redant0 l :: Antecedents
    l g :: 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 p :: Proof
    p f :: Formula
    f) l :: Antecedents
    l g :: 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 "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 p :: Proof
    p (PVar s :: Symbol
    s)) l :: Antecedents
    l g :: Formula
    g =
              let af :: AtomF
    af = Proof -> Symbol -> AtomF
    AtomF Proof
    p Symbol
    s
                  (bs :: Antecedents
    bs, restAtomImps :: 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 f :: Proof
    f b :: 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 p :: Proof
    p (Conj bs :: [Formula]
    bs)) l :: Antecedents
    l g :: 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 "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 (\ v :: Symbol
    v a :: 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 p :: Proof
    p (Disj ds :: [(ConsDesc, Formula)]
    ds)) l :: Antecedents
    l g :: 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 "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 (\ (v :: Symbol
    v, (_, d :: 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 p :: Proof
    p (a :: Formula
    a :-> b :: Formula
    b)) l :: Antecedents
    l g :: 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 t :: Proof
    t c :: Formula
    c d :: Formula
    d a :: Antecedents
    a g :: 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 "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' p :: Proof
    p (PVar s :: Symbol
    s) b :: Formula
    b l :: Antecedents
    l g :: 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' p :: Proof
    p (Conj cs :: [Formula]
    cs) b :: Formula
    b l :: Antecedents
    l g :: Formula
    g = do
              Symbol
    x <- String -> P Symbol
    newSym "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' p :: Proof
    p (Disj ds :: [(ConsDesc, Formula)]
    ds) b :: Formula
    b l :: Antecedents
    l g :: 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 "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 (\ v :: Symbol
    v (_, d :: 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 (\ r :: Proof
    r (i :: Int
    i, v :: Symbol
    v, (cd :: ConsDesc
    cd, _)) -> 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 [0..] [Symbol]
    vs [(ConsDesc, Formula)]
    ds)
            -- p : (c -> d) -> b
            redantimp' p :: Proof
    p (c :: Formula
    c :-> d :: Formula
    d) b :: Formula
    b l :: Antecedents
    l g :: 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 f :: Proof
    f b :: Formula
    b c :: Formula
    c d :: Formula
    d a :: Antecedents
    a g :: 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 "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' p :: Proof
    p c :: Formula
    c d :: Formula
    d (Disj []) l :: Antecedents
    l g :: Formula
    g | Formula
    d Formula -> Formula -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Formula
    false = do
              Symbol
    x <- String -> P Symbol
    newSym "x"
              Symbol
    y <- String -> P Symbol
    newSym "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' p :: Proof
    p c :: Formula
    c d :: Formula
    d b :: Formula
    b l :: Antecedents
    l g :: 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 p :: Proof
    p s :: Symbol
    s b :: Formula
    b l :: Antecedents
    l g :: 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 "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' p :: Proof
    p s :: Symbol
    s b :: Formula
    b l :: Antecedents
    l g :: 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 "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 "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 "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 g :: 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 "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 s :: 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 cs :: [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 ds :: [(ConsDesc, Formula)]
    ds) = do
              Symbol
    s1 <- String -> P Symbol
    newSym "_"
              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 | (i :: Int
    i, (cd :: ConsDesc
    cd, d :: Formula
    d)) <- [Int] -> [(ConsDesc, Formula)] -> [(Int, (ConsDesc, Formula))]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [0..] [(ConsDesc, Formula)]
    ds ] Formula
    v
            redsucc' (a :: Formula
    a :-> b :: Formula
    b) = do
              Symbol
    s <- String -> P Symbol
    newSym "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 g :: 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 "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' g :: Formula
    g = do
              let ordImps :: NestImps
    ordImps = NestImps -> Formula -> AtomImps -> NestImps
    order NestImps
    nestImps Formula
    g AtomImps
    atomImps
              (NestImp p :: Proof
    p c :: Formula
    c d :: Formula
    d b :: Formula
    b, restImps :: NestImps
    restImps) <-
                  String -> P (NestImp, NestImps) -> P (NestImp, NestImps)
    forall a. String -> a -> a
    mtrace ("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 "x"
              Symbol
    z <- String -> P Symbol
    newSym "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 g :: Symbol
    g atomImps :: AtomImps
    atomImps nestImps :: 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 _ a :: Formula
    a b :: Formula
    b c :: Formula
    c <- NestImps
    nestImps ]

    posin1 :: Symbol -> AtomImps -> Bool
    posin1 :: Symbol -> AtomImps -> Bool
    posin1 g :: Symbol
    g atomImps :: AtomImps
    atomImps = (AtomImp -> Bool) -> AtomImps -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any (\ (AtomImp _ bs :: Antecedents
    bs) -> Symbol -> [Formula] -> Bool
    posin2 Symbol
    g [ Formula
    b | A _ b :: Formula
    b <- Antecedents
    bs]) AtomImps
    atomImps

    posin2 :: Symbol -> [Formula] -> Bool
    posin2 :: Symbol -> [Formula] -> Bool
    posin2 g :: Symbol
    g bs :: [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 g :: Symbol
    g (Disj as :: [(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 g :: Symbol
    g (Conj as :: [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 g :: Symbol
    g (_ :-> b :: Formula
    b) = Symbol -> Formula -> Bool
    posin3 Symbol
    g Formula
    b
    posin3 s :: Symbol
    s (PVar s' :: 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 False p :: P a
    p = P a -> P a
    forall a. P a -> P a
    atMostOne P a
    p
    cutSearch True p :: P a
    p = P a
    p

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