{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TypeFamilies #-}

-- |
-- Module      : AutoProof.Internal.Proof.Types
-- Copyright   : (c) Artem Mavrin, 2021
-- License     : BSD3
-- Maintainer  : artemvmavrin@gmail.com
-- Stability   : experimental
-- Portability : POSIX
--
-- Defines the 'Proof' type.
module AutoProof.Internal.Proof.Types
  ( Proof
      ( Axiom,
        FalseElim,
        TrueIntr,
        NotElim,
        NotIntr,
        ImpElim,
        ImpIntr,
        OrElim,
        OrIntrL,
        OrIntrR,
        AndElimL,
        AndElimR,
        AndIntr,
        IffElimL,
        IffElimR,
        IffIntr
      ),
    prettyProof,
  )
where

import AutoProof.Internal.AST
  ( AST (Root, children, height, metadata, root),
    ASTMetadata,
    atomicASTConstructor,
    binaryRootedASTConstructor,
    ternaryRootedASTConstructor,
    unaryRootedASTConstructor,
  )
import AutoProof.Internal.Judgement (Judgement)
import AutoProof.Internal.Utils.PrettyPrintable (PrettyPrintable (pretty))
import AutoProof.Internal.Utils.PrettyPrintable.Symbols
  ( andElimLS,
    andElimRS,
    andIntrS,
    axiomS,
    branchS,
    cornerS,
    falseElimS,
    iffElimLS,
    iffElimRS,
    iffIntrS,
    impElimS,
    impIntrS,
    notElimS,
    notIntrS,
    orElimS,
    orIntrLS,
    orIntrRS,
    trueIntrS,
    vertS,
  )

-- | A proof tree for propositional logic.
data Proof a
  = Axiom_ !ASTMetadata (Judgement a)
  | FalseElim_ !ASTMetadata (Judgement a) (Proof a)
  | TrueIntr_ !ASTMetadata (Judgement a)
  | NotElim_ !ASTMetadata (Judgement a) !(Proof a) !(Proof a)
  | NotIntr_ !ASTMetadata (Judgement a) !(Proof a)
  | ImpElim_ !ASTMetadata (Judgement a) !(Proof a) !(Proof a)
  | ImpIntr_ !ASTMetadata (Judgement a) !(Proof a)
  | OrElim_ !ASTMetadata (Judgement a) !(Proof a) !(Proof a) !(Proof a)
  | OrIntrL_ !ASTMetadata (Judgement a) !(Proof a)
  | OrIntrR_ !ASTMetadata (Judgement a) !(Proof a)
  | AndElimL_ !ASTMetadata (Judgement a) !(Proof a)
  | AndElimR_ !ASTMetadata (Judgement a) !(Proof a)
  | AndIntr_ !ASTMetadata (Judgement a) !(Proof a) !(Proof a)
  | IffElimL_ !ASTMetadata (Judgement a) !(Proof a)
  | IffElimR_ !ASTMetadata (Judgement a) !(Proof a)
  | IffIntr_ !ASTMetadata (Judgement a) !(Proof a) !(Proof a)

instance AST (Proof a) where
  type Root (Proof a) = Judgement a

  root :: Proof a -> Root (Proof a)
root (Axiom j :: Judgement a
j) = Root (Proof a)
Judgement a
j
  root (FalseElim j :: Judgement a
j _) = Root (Proof a)
Judgement a
j
  root (TrueIntr j :: Judgement a
j) = Root (Proof a)
Judgement a
j
  root (NotElim j :: Judgement a
j _ _) = Root (Proof a)
Judgement a
j
  root (NotIntr j :: Judgement a
j _) = Root (Proof a)
Judgement a
j
  root (ImpElim j :: Judgement a
j _ _) = Root (Proof a)
Judgement a
j
  root (ImpIntr j :: Judgement a
j _) = Root (Proof a)
Judgement a
j
  root (OrElim j :: Judgement a
j _ _ _) = Root (Proof a)
Judgement a
j
  root (OrIntrL j :: Judgement a
j _) = Root (Proof a)
Judgement a
j
  root (OrIntrR j :: Judgement a
j _) = Root (Proof a)
Judgement a
j
  root (AndElimL j :: Judgement a
j _) = Root (Proof a)
Judgement a
j
  root (AndElimR j :: Judgement a
j _) = Root (Proof a)
Judgement a
j
  root (AndIntr j :: Judgement a
j _ _) = Root (Proof a)
Judgement a
j
  root (IffElimL j :: Judgement a
j _) = Root (Proof a)
Judgement a
j
  root (IffElimR j :: Judgement a
j _) = Root (Proof a)
Judgement a
j
  root (IffIntr j :: Judgement a
j _ _) = Root (Proof a)
Judgement a
j

  children :: Proof a -> [Proof a]
children (Axiom _) = []
  children (FalseElim _ p :: Proof a
p) = [Proof a
p]
  children (TrueIntr _) = []
  children (NotElim _ p :: Proof a
p q :: Proof a
q) = [Proof a
p, Proof a
q]
  children (NotIntr _ p :: Proof a
p) = [Proof a
p]
  children (ImpElim _ p :: Proof a
p q :: Proof a
q) = [Proof a
p, Proof a
q]
  children (ImpIntr _ p :: Proof a
p) = [Proof a
p]
  children (OrElim _ p :: Proof a
p q :: Proof a
q r :: Proof a
r) = [Proof a
p, Proof a
q, Proof a
r]
  children (OrIntrL _ p :: Proof a
p) = [Proof a
p]
  children (OrIntrR _ p :: Proof a
p) = [Proof a
p]
  children (AndElimL _ p :: Proof a
p) = [Proof a
p]
  children (AndElimR _ p :: Proof a
p) = [Proof a
p]
  children (AndIntr _ p :: Proof a
p q :: Proof a
q) = [Proof a
p, Proof a
q]
  children (IffElimL _ p :: Proof a
p) = [Proof a
p]
  children (IffElimR _ p :: Proof a
p) = [Proof a
p]
  children (IffIntr _ p :: Proof a
p q :: Proof a
q) = [Proof a
p, Proof a
q]

  metadata :: Proof a -> ASTMetadata
metadata (Axiom_ m :: ASTMetadata
m _) = ASTMetadata
m
  metadata (FalseElim_ m :: ASTMetadata
m _ _) = ASTMetadata
m
  metadata (TrueIntr_ m :: ASTMetadata
m _) = ASTMetadata
m
  metadata (NotElim_ m :: ASTMetadata
m _ _ _) = ASTMetadata
m
  metadata (NotIntr_ m :: ASTMetadata
m _ _) = ASTMetadata
m
  metadata (ImpElim_ m :: ASTMetadata
m _ _ _) = ASTMetadata
m
  metadata (ImpIntr_ m :: ASTMetadata
m _ _) = ASTMetadata
m
  metadata (OrElim_ m :: ASTMetadata
m _ _ _ _) = ASTMetadata
m
  metadata (OrIntrL_ m :: ASTMetadata
m _ _) = ASTMetadata
m
  metadata (OrIntrR_ m :: ASTMetadata
m _ _) = ASTMetadata
m
  metadata (AndElimL_ m :: ASTMetadata
m _ _) = ASTMetadata
m
  metadata (AndElimR_ m :: ASTMetadata
m _ _) = ASTMetadata
m
  metadata (AndIntr_ m :: ASTMetadata
m _ _ _) = ASTMetadata
m
  metadata (IffElimL_ m :: ASTMetadata
m _ _) = ASTMetadata
m
  metadata (IffElimR_ m :: ASTMetadata
m _ _) = ASTMetadata
m
  metadata (IffIntr_ m :: ASTMetadata
m _ _ _) = ASTMetadata
m

-- Smart constructors and pattern matching synonyms

-- | An axiom @('Axiom' (g 'AutoProof.Judgement.|-' a))@ represents the
-- inference of the judgement \(g \vdash a\), where \(a \in g\):
--
-- \[
--   \frac{}{
--     g \vdash a
--   }
--   \, (\text{Axiom})
-- \]
pattern Axiom :: Judgement a -> Proof a
pattern $bAxiom :: Judgement a -> Proof a
$mAxiom :: forall r a. Proof a -> (Judgement a -> r) -> (Void# -> r) -> r
Axiom a <-
  Axiom_ _ a
  where
    Axiom = (ASTMetadata -> Judgement a -> Proof a) -> Judgement a -> Proof a
forall a t. (ASTMetadata -> a -> t) -> a -> t
atomicASTConstructor ASTMetadata -> Judgement a -> Proof a
forall a. ASTMetadata -> Judgement a -> Proof a
Axiom_

-- | Falsity elimination (principle of explosion).
-- @('FalseElim' (g 'AutoProof.Judgement.|-' a) p)@ represents the inference of
-- the judgement \(g \vdash a\) given a proof \(p\) of \(g \vdash \bot\):
--
-- \[
--   \frac{
--     \displaystyle\frac{
--       p
--     }{
--       g \vdash \bot
--     }
--   }{
--     g \vdash a
--   }
--   \, ({\bot}\text{E})
-- \]
pattern FalseElim :: Judgement a -> Proof a -> Proof a
pattern $bFalseElim :: Judgement a -> Proof a -> Proof a
$mFalseElim :: forall r a.
Proof a -> (Judgement a -> Proof a -> r) -> (Void# -> r) -> r
FalseElim j p <-
  FalseElim_ _ j p
  where
    FalseElim = (ASTMetadata -> Judgement a -> Proof a -> Proof a)
-> Judgement a -> Proof a -> Proof a
forall t a. AST t => (ASTMetadata -> a -> t -> t) -> a -> t -> t
unaryRootedASTConstructor ASTMetadata -> Judgement a -> Proof a -> Proof a
forall a. ASTMetadata -> Judgement a -> Proof a -> Proof a
FalseElim_

-- | Truth introduction.
-- @('TrueIntr' (g 'AutoProof.Judgement.|-' 'AutoProof.Formula.Lit' 'True'))@
-- represents the vacuous inference of the judgement \(g \vdash \top\):
--
-- \[
--   \frac{}{
--     g \vdash \top
--   }
--   \, (\top\text{I})
-- \]
pattern TrueIntr :: Judgement a -> Proof a
pattern $bTrueIntr :: Judgement a -> Proof a
$mTrueIntr :: forall r a. Proof a -> (Judgement a -> r) -> (Void# -> r) -> r
TrueIntr j <-
  TrueIntr_ _ j
  where
    TrueIntr = (ASTMetadata -> Judgement a -> Proof a) -> Judgement a -> Proof a
forall a t. (ASTMetadata -> a -> t) -> a -> t
atomicASTConstructor ASTMetadata -> Judgement a -> Proof a
forall a. ASTMetadata -> Judgement a -> Proof a
TrueIntr_

-- | Negation elimination.
-- @('NotElim' (g 'AutoProof.Judgement.|-' 'AutoProof.Formula.Lit' 'False') p q)@
-- represents the inference of the judgement \(g \vdash \bot\) given a proof
-- \(p\) of \(g_1 \vdash \lnot a\) and a proof \(q\) of \(g_2 \vdash a\), where
-- \(g = g_1 \cup g_2\):
--
-- \[
--   \frac{
--     \displaystyle\frac{
--       p
--     }{
--       g_1 \vdash \lnot a
--     }
--     \qquad
--     \displaystyle\frac{
--       q
--     }{
--       g_2 \vdash a
--     }
--   }{
--     g \vdash \bot
--   }
--   \, ({\lnot}\text{E})
-- \]
pattern NotElim :: Judgement a -> Proof a -> Proof a -> Proof a
pattern $bNotElim :: Judgement a -> Proof a -> Proof a -> Proof a
$mNotElim :: forall r a.
Proof a
-> (Judgement a -> Proof a -> Proof a -> r) -> (Void# -> r) -> r
NotElim j p q <-
  NotElim_ _ j p q
  where
    NotElim = (ASTMetadata -> Judgement a -> Proof a -> Proof a -> Proof a)
-> Judgement a -> Proof a -> Proof a -> Proof a
forall t a.
AST t =>
(ASTMetadata -> a -> t -> t -> t) -> a -> t -> t -> t
binaryRootedASTConstructor ASTMetadata -> Judgement a -> Proof a -> Proof a -> Proof a
forall a.
ASTMetadata -> Judgement a -> Proof a -> Proof a -> Proof a
NotElim_

-- | Negation introduction.
-- @('NotIntr' (g 'AutoProof.Judgement.|-' ('AutoProof.Formula.Not' a)) p)@
-- represents the inference of the judgement \(g \vdash \lnot a\) given a proof
-- \(p\) of \(g, a \vdash \bot\):
--
-- \[
--   \frac{
--     \displaystyle\frac{
--       p
--     }{
--       g, a \vdash \bot
--     }
--   }{
--     g \vdash \lnot a
--   }
--   \, ({\lnot}\text{I})
-- \]
pattern NotIntr :: Judgement a -> Proof a -> Proof a
pattern $bNotIntr :: Judgement a -> Proof a -> Proof a
$mNotIntr :: forall r a.
Proof a -> (Judgement a -> Proof a -> r) -> (Void# -> r) -> r
NotIntr j p <-
  NotIntr_ _ j p
  where
    NotIntr = (ASTMetadata -> Judgement a -> Proof a -> Proof a)
-> Judgement a -> Proof a -> Proof a
forall t a. AST t => (ASTMetadata -> a -> t -> t) -> a -> t -> t
unaryRootedASTConstructor ASTMetadata -> Judgement a -> Proof a -> Proof a
forall a. ASTMetadata -> Judgement a -> Proof a -> Proof a
NotIntr_

-- | Implication elimination (/modus ponens/).
-- @('ImpElim' (g 'AutoProof.Judgement.|-' b) p q)@ represents the inference of
-- the judgement \(g \vdash b\) given a proof \(p\) of
-- \(g_1 \vdash a \rightarrow b\) and a proof \(q\) of \(g_2 \vdash a\), where
-- \(g = g_1 \cup g_2\):
--
-- \[
--   \frac{
--     \displaystyle\frac{
--       p
--     }{
--       g_1 \vdash a \rightarrow b
--     }
--     \qquad
--     \displaystyle\frac{
--       q
--     }{
--       g_2 \vdash a
--     }
--   }{
--     g \vdash b
--   }
--   \, ({\rightarrow}\text{E})
-- \]
pattern ImpElim :: Judgement a -> Proof a -> Proof a -> Proof a
pattern $bImpElim :: Judgement a -> Proof a -> Proof a -> Proof a
$mImpElim :: forall r a.
Proof a
-> (Judgement a -> Proof a -> Proof a -> r) -> (Void# -> r) -> r
ImpElim j p q <-
  ImpElim_ _ j p q
  where
    ImpElim = (ASTMetadata -> Judgement a -> Proof a -> Proof a -> Proof a)
-> Judgement a -> Proof a -> Proof a -> Proof a
forall t a.
AST t =>
(ASTMetadata -> a -> t -> t -> t) -> a -> t -> t -> t
binaryRootedASTConstructor ASTMetadata -> Judgement a -> Proof a -> Proof a -> Proof a
forall a.
ASTMetadata -> Judgement a -> Proof a -> Proof a -> Proof a
ImpElim_

-- | Implication introduction.
-- @('ImpIntr' (g 'AutoProof.Judgement.|-' ('AutoProof.Formula.Imp' a b) p)@
-- represents the inference of the judgement \(g \vdash a \rightarrow b\) given
-- a proof \(p\) of \(g, a \vdash b\):
--
-- \[
--   \frac{
--     \displaystyle\frac{
--       p
--     }{
--       g, a \vdash b
--     }
--   }{
--     g \vdash a \rightarrow b
--   }
--   \, ({\rightarrow}\text{I})
-- \]
pattern ImpIntr :: Judgement a -> Proof a -> Proof a
pattern $bImpIntr :: Judgement a -> Proof a -> Proof a
$mImpIntr :: forall r a.
Proof a -> (Judgement a -> Proof a -> r) -> (Void# -> r) -> r
ImpIntr j p <-
  ImpIntr_ _ j p
  where
    ImpIntr = (ASTMetadata -> Judgement a -> Proof a -> Proof a)
-> Judgement a -> Proof a -> Proof a
forall t a. AST t => (ASTMetadata -> a -> t -> t) -> a -> t -> t
unaryRootedASTConstructor ASTMetadata -> Judgement a -> Proof a -> Proof a
forall a. ASTMetadata -> Judgement a -> Proof a -> Proof a
ImpIntr_

-- | Disjunction elimination.
-- @('OrElim' (g 'AutoProof.Judgement.|-' c) p q r)@ represents the inference of
-- the judgement \(g \vdash c\) given proofs \(p\) of \(g_1 \vdash a \lor b\),
-- \(q\) of \(g_2, a \vdash c\), and \(r\) of \(g_3, b \vdash c\), where
-- \(g = g_1 \cup g_2 \cup g_3\):
--
-- \[
--   \frac{
--     \displaystyle\frac{
--       p
--     }{
--       g_1 \vdash a \lor b
--     }
--     \qquad
--     \displaystyle\frac{
--       q
--     }{
--       g_2, a \vdash c
--     }
--     \qquad
--     \displaystyle\frac{
--       r
--     }{
--       g_3, b \vdash c
--     }
--   }{
--     g \vdash c
--   }
--   \, ({\lor}\text{E})
-- \]
pattern OrElim :: Judgement a -> Proof a -> Proof a -> Proof a -> Proof a
pattern $bOrElim :: Judgement a -> Proof a -> Proof a -> Proof a -> Proof a
$mOrElim :: forall r a.
Proof a
-> (Judgement a -> Proof a -> Proof a -> Proof a -> r)
-> (Void# -> r)
-> r
OrElim j p q r <-
  OrElim_ _ j p q r
  where
    OrElim = (ASTMetadata
 -> Judgement a -> Proof a -> Proof a -> Proof a -> Proof a)
-> Judgement a -> Proof a -> Proof a -> Proof a -> Proof a
forall t a.
AST t =>
(ASTMetadata -> a -> t -> t -> t -> t) -> a -> t -> t -> t -> t
ternaryRootedASTConstructor ASTMetadata
-> Judgement a -> Proof a -> Proof a -> Proof a -> Proof a
forall a.
ASTMetadata
-> Judgement a -> Proof a -> Proof a -> Proof a -> Proof a
OrElim_

-- | Left disjunction introduction.
-- @('OrIntrL' (g 'AutoProof.Judgement.|-' ('AutoProof.Formula.Or' a b)) p)@
-- represents the inference of the judgement \(g \vdash a \lor b\) given a proof
-- \(p\) of \(g \vdash a\):
--
-- \[
--   \frac{
--     \displaystyle\frac{
--       p
--     }{
--       g \vdash a
--     }
--   }{
--     g \vdash a \lor b
--   }
--   \, ({\lor}\text{IL})
-- \]
pattern OrIntrL :: Judgement a -> Proof a -> Proof a
pattern $bOrIntrL :: Judgement a -> Proof a -> Proof a
$mOrIntrL :: forall r a.
Proof a -> (Judgement a -> Proof a -> r) -> (Void# -> r) -> r
OrIntrL j p <-
  OrIntrL_ _ j p
  where
    OrIntrL = (ASTMetadata -> Judgement a -> Proof a -> Proof a)
-> Judgement a -> Proof a -> Proof a
forall t a. AST t => (ASTMetadata -> a -> t -> t) -> a -> t -> t
unaryRootedASTConstructor ASTMetadata -> Judgement a -> Proof a -> Proof a
forall a. ASTMetadata -> Judgement a -> Proof a -> Proof a
OrIntrL_

-- | Right disjunction introduction.
-- @('OrIntrR' (g 'AutoProof.Judgement.|-' ('AutoProof.Formula.Or' a b)) p)@
-- represents the inference of the judgement \(g \vdash a \lor b\) given a proof
-- \(p\) of \(g \vdash b\):
--
-- \[
--   \frac{
--     \displaystyle\frac{
--       p
--     }{
--       g \vdash b
--     }
--   }{
--     g \vdash a \lor b
--   }
--   \, ({\lor}\text{IR})
-- \]
pattern OrIntrR :: Judgement a -> Proof a -> Proof a
pattern $bOrIntrR :: Judgement a -> Proof a -> Proof a
$mOrIntrR :: forall r a.
Proof a -> (Judgement a -> Proof a -> r) -> (Void# -> r) -> r
OrIntrR j p <-
  OrIntrR_ _ j p
  where
    OrIntrR = (ASTMetadata -> Judgement a -> Proof a -> Proof a)
-> Judgement a -> Proof a -> Proof a
forall t a. AST t => (ASTMetadata -> a -> t -> t) -> a -> t -> t
unaryRootedASTConstructor ASTMetadata -> Judgement a -> Proof a -> Proof a
forall a. ASTMetadata -> Judgement a -> Proof a -> Proof a
OrIntrR_

-- | Left conjunction elimination.
-- @('AndElimL' (g 'AutoProof.Judgement.|-' a) p)@ represents the inference of
-- the judgement \(g \vdash a\) given a proof \(p\) of \(g \vdash a \land b\):
--
-- \[
--   \frac{
--     \displaystyle\frac{
--       p
--     }{
--       g \vdash a \land b
--     }
--   }{
--     g \vdash a
--   }
--   \, ({\land}\text{EL})
-- \]
pattern AndElimL :: Judgement a -> Proof a -> Proof a
pattern $bAndElimL :: Judgement a -> Proof a -> Proof a
$mAndElimL :: forall r a.
Proof a -> (Judgement a -> Proof a -> r) -> (Void# -> r) -> r
AndElimL j p <-
  AndElimL_ _ j p
  where
    AndElimL = (ASTMetadata -> Judgement a -> Proof a -> Proof a)
-> Judgement a -> Proof a -> Proof a
forall t a. AST t => (ASTMetadata -> a -> t -> t) -> a -> t -> t
unaryRootedASTConstructor ASTMetadata -> Judgement a -> Proof a -> Proof a
forall a. ASTMetadata -> Judgement a -> Proof a -> Proof a
AndElimL_

-- | Right conjunction elimination.
-- @('AndElimR' (g 'AutoProof.Judgement.|-' b) p)@ represents the inference of
-- the judgement \(g \vdash b\) given a proof \(p\) of \(g \vdash a \land b\):
--
-- \[
--   \frac{
--     \displaystyle\frac{
--       p
--     }{
--       g \vdash a \land b
--     }
--   }{
--     g \vdash b
--   }
--   \, ({\land}\text{ER})
-- \]
pattern AndElimR :: Judgement a -> Proof a -> Proof a
pattern $bAndElimR :: Judgement a -> Proof a -> Proof a
$mAndElimR :: forall r a.
Proof a -> (Judgement a -> Proof a -> r) -> (Void# -> r) -> r
AndElimR j p <-
  AndElimR_ _ j p
  where
    AndElimR = (ASTMetadata -> Judgement a -> Proof a -> Proof a)
-> Judgement a -> Proof a -> Proof a
forall t a. AST t => (ASTMetadata -> a -> t -> t) -> a -> t -> t
unaryRootedASTConstructor ASTMetadata -> Judgement a -> Proof a -> Proof a
forall a. ASTMetadata -> Judgement a -> Proof a -> Proof a
AndElimR_

-- | Conjunction introduction.
-- @('AndIntr' (g 'AutoProof.Judgement.|-' ('AutoProof.Formula.And' a b)) p)@
-- represents the inference of the judgement \(g \vdash a \land b\) given a
-- proof \(p\) of \(g_1 \vdash a\) and a proof \(q\) of \(g_2 \vdash b\), where
-- \(g = g_1 \cup g_2\):
--
-- \[
--   \frac{
--     \displaystyle\frac{
--       p
--     }{
--       g_1 \vdash a
--     }
--     \qquad
--     \displaystyle\frac{
--       q
--     }{
--       g_2 \vdash b
--     }
--   }{
--     g \vdash a \land b
--   }
--   \, ({\land}\text{I})
-- \]
pattern AndIntr :: Judgement a -> Proof a -> Proof a -> Proof a
pattern $bAndIntr :: Judgement a -> Proof a -> Proof a -> Proof a
$mAndIntr :: forall r a.
Proof a
-> (Judgement a -> Proof a -> Proof a -> r) -> (Void# -> r) -> r
AndIntr j p q <-
  AndIntr_ _ j p q
  where
    AndIntr = (ASTMetadata -> Judgement a -> Proof a -> Proof a -> Proof a)
-> Judgement a -> Proof a -> Proof a -> Proof a
forall t a.
AST t =>
(ASTMetadata -> a -> t -> t -> t) -> a -> t -> t -> t
binaryRootedASTConstructor ASTMetadata -> Judgement a -> Proof a -> Proof a -> Proof a
forall a.
ASTMetadata -> Judgement a -> Proof a -> Proof a -> Proof a
AndIntr_

-- | Left equivalence elimination.
-- @('IffElimL' (g 'AutoProof.Judgement.|-' ('AutoProof.Formula.Imp' a b)) p)@
-- represents the inference of the judgement \(g \vdash a \rightarrow b\) given
-- a proof \(p\) of \(g \vdash a \leftrightarrow b\):
--
-- \[
--   \frac{
--     \displaystyle\frac{
--       p
--     }{
--       g \vdash a \leftrightarrow b
--     }
--   }{
--     g \vdash a \rightarrow b
--   }
--   \, ({\leftrightarrow}\text{EL})
-- \]
pattern IffElimL :: Judgement a -> Proof a -> Proof a
pattern $bIffElimL :: Judgement a -> Proof a -> Proof a
$mIffElimL :: forall r a.
Proof a -> (Judgement a -> Proof a -> r) -> (Void# -> r) -> r
IffElimL j p <-
  IffElimL_ _ j p
  where
    IffElimL = (ASTMetadata -> Judgement a -> Proof a -> Proof a)
-> Judgement a -> Proof a -> Proof a
forall t a. AST t => (ASTMetadata -> a -> t -> t) -> a -> t -> t
unaryRootedASTConstructor ASTMetadata -> Judgement a -> Proof a -> Proof a
forall a. ASTMetadata -> Judgement a -> Proof a -> Proof a
IffElimL_

-- | Right equivalence elimination.
-- @('IffElimR' (g 'AutoProof.Judgement.|-' ('AutoProof.Formula.Imp' b a)) p)@
-- represents the inference of the judgement \(g \vdash b \rightarrow a\) given
-- a proof \(p\) of \(g \vdash a \leftrightarrow b\):
--
-- \[
--   \frac{
--     \displaystyle\frac{
--       p
--     }{
--       g \vdash a \leftrightarrow b
--     }
--   }{
--     g \vdash b \rightarrow a
--   }
--   \, ({\leftrightarrow}\text{ER})
-- \]
pattern IffElimR :: Judgement a -> Proof a -> Proof a
pattern $bIffElimR :: Judgement a -> Proof a -> Proof a
$mIffElimR :: forall r a.
Proof a -> (Judgement a -> Proof a -> r) -> (Void# -> r) -> r
IffElimR j p <-
  IffElimR_ _ j p
  where
    IffElimR = (ASTMetadata -> Judgement a -> Proof a -> Proof a)
-> Judgement a -> Proof a -> Proof a
forall t a. AST t => (ASTMetadata -> a -> t -> t) -> a -> t -> t
unaryRootedASTConstructor ASTMetadata -> Judgement a -> Proof a -> Proof a
forall a. ASTMetadata -> Judgement a -> Proof a -> Proof a
IffElimR_

-- | Equivalence introduction.
-- @('IffIntr' (g 'AutoProof.Judgement.|-' ('AutoProof.Formula.Iff' a b)) p)@
-- represents the inference of the judgement \(g \vdash a \leftrightarrow b\)
-- given a proof \(p\) of \(g_1 \vdash a \rightarrow b\) and a proof \(q\) of
-- \(g_2 \vdash b \rightarrow a\), where \(g = g_1 \cup g_2\):
--
-- \[
--   \frac{
--     \displaystyle\frac{
--       p
--     }{
--       g_1 \vdash a \rightarrow b
--     }
--     \qquad
--     \displaystyle\frac{
--       q
--     }{
--       g_2 \vdash b \rightarrow a
--     }
--   }{
--     g \vdash a \leftrightarrow b
--   }
--   \, ({\leftrightarrow}\text{I})
-- \]
pattern IffIntr :: Judgement a -> Proof a -> Proof a -> Proof a
pattern $bIffIntr :: Judgement a -> Proof a -> Proof a -> Proof a
$mIffIntr :: forall r a.
Proof a
-> (Judgement a -> Proof a -> Proof a -> r) -> (Void# -> r) -> r
IffIntr j p q <-
  IffIntr_ _ j p q
  where
    IffIntr = (ASTMetadata -> Judgement a -> Proof a -> Proof a -> Proof a)
-> Judgement a -> Proof a -> Proof a -> Proof a
forall t a.
AST t =>
(ASTMetadata -> a -> t -> t -> t) -> a -> t -> t -> t
binaryRootedASTConstructor ASTMetadata -> Judgement a -> Proof a -> Proof a -> Proof a
forall a.
ASTMetadata -> Judgement a -> Proof a -> Proof a -> Proof a
IffIntr_

{-# COMPLETE
  Axiom,
  FalseElim,
  TrueIntr,
  NotElim,
  NotIntr,
  ImpElim,
  ImpIntr,
  OrElim,
  OrIntrL,
  OrIntrR,
  AndElimL,
  AndElimR,
  AndIntr,
  IffElimL,
  IffElimR,
  IffIntr
  #-}

-- Instance declarations

instance Eq a => Eq (Proof a) where
  (Axiom j :: Judgement a
j) == :: Proof a -> Proof a -> Bool
== (Axiom j' :: Judgement a
j') = Judgement a
j Judgement a -> Judgement a -> Bool
forall a. Eq a => a -> a -> Bool
== Judgement a
j'
  (FalseElim j :: Judgement a
j p :: Proof a
p) == (FalseElim j' :: Judgement a
j' p' :: Proof a
p') = Judgement a
j Judgement a -> Judgement a -> Bool
forall a. Eq a => a -> a -> Bool
== Judgement a
j' Bool -> Bool -> Bool
&& Proof a
p Proof a -> Proof a -> Bool
forall a. Eq a => a -> a -> Bool
== Proof a
p'
  (TrueIntr j :: Judgement a
j) == (TrueIntr j' :: Judgement a
j') = Judgement a
j Judgement a -> Judgement a -> Bool
forall a. Eq a => a -> a -> Bool
== Judgement a
j'
  (NotElim j :: Judgement a
j p :: Proof a
p q :: Proof a
q) == (NotElim j' :: Judgement a
j' p' :: Proof a
p' q' :: Proof a
q') = Judgement a
j Judgement a -> Judgement a -> Bool
forall a. Eq a => a -> a -> Bool
== Judgement a
j' Bool -> Bool -> Bool
&& Proof a
p Proof a -> Proof a -> Bool
forall a. Eq a => a -> a -> Bool
== Proof a
p' Bool -> Bool -> Bool
&& Proof a
q Proof a -> Proof a -> Bool
forall a. Eq a => a -> a -> Bool
== Proof a
q'
  (NotIntr j :: Judgement a
j p :: Proof a
p) == (NotIntr j' :: Judgement a
j' p' :: Proof a
p') = Judgement a
j Judgement a -> Judgement a -> Bool
forall a. Eq a => a -> a -> Bool
== Judgement a
j' Bool -> Bool -> Bool
&& Proof a
p Proof a -> Proof a -> Bool
forall a. Eq a => a -> a -> Bool
== Proof a
p'
  (ImpElim j :: Judgement a
j p :: Proof a
p q :: Proof a
q) == (ImpElim j' :: Judgement a
j' p' :: Proof a
p' q' :: Proof a
q') = Judgement a
j Judgement a -> Judgement a -> Bool
forall a. Eq a => a -> a -> Bool
== Judgement a
j' Bool -> Bool -> Bool
&& Proof a
p Proof a -> Proof a -> Bool
forall a. Eq a => a -> a -> Bool
== Proof a
p' Bool -> Bool -> Bool
&& Proof a
q Proof a -> Proof a -> Bool
forall a. Eq a => a -> a -> Bool
== Proof a
q'
  (ImpIntr j :: Judgement a
j p :: Proof a
p) == (ImpIntr j' :: Judgement a
j' p' :: Proof a
p') = Judgement a
j Judgement a -> Judgement a -> Bool
forall a. Eq a => a -> a -> Bool
== Judgement a
j' Bool -> Bool -> Bool
&& Proof a
p Proof a -> Proof a -> Bool
forall a. Eq a => a -> a -> Bool
== Proof a
p'
  (OrElim j :: Judgement a
j p :: Proof a
p q :: Proof a
q r :: Proof a
r) == (OrElim j' :: Judgement a
j' p' :: Proof a
p' q' :: Proof a
q' r' :: Proof a
r') = Judgement a
j Judgement a -> Judgement a -> Bool
forall a. Eq a => a -> a -> Bool
== Judgement a
j' Bool -> Bool -> Bool
&& Proof a
p Proof a -> Proof a -> Bool
forall a. Eq a => a -> a -> Bool
== Proof a
p' Bool -> Bool -> Bool
&& Proof a
q Proof a -> Proof a -> Bool
forall a. Eq a => a -> a -> Bool
== Proof a
q' Bool -> Bool -> Bool
&& Proof a
r Proof a -> Proof a -> Bool
forall a. Eq a => a -> a -> Bool
== Proof a
r'
  (OrIntrL j :: Judgement a
j p :: Proof a
p) == (OrIntrL j' :: Judgement a
j' p' :: Proof a
p') = Judgement a
j Judgement a -> Judgement a -> Bool
forall a. Eq a => a -> a -> Bool
== Judgement a
j' Bool -> Bool -> Bool
&& Proof a
p Proof a -> Proof a -> Bool
forall a. Eq a => a -> a -> Bool
== Proof a
p'
  (OrIntrR j :: Judgement a
j p :: Proof a
p) == (OrIntrR j' :: Judgement a
j' p' :: Proof a
p') = Judgement a
j Judgement a -> Judgement a -> Bool
forall a. Eq a => a -> a -> Bool
== Judgement a
j' Bool -> Bool -> Bool
&& Proof a
p Proof a -> Proof a -> Bool
forall a. Eq a => a -> a -> Bool
== Proof a
p'
  (AndElimL j :: Judgement a
j p :: Proof a
p) == (AndElimL j' :: Judgement a
j' p' :: Proof a
p') = Judgement a
j Judgement a -> Judgement a -> Bool
forall a. Eq a => a -> a -> Bool
== Judgement a
j' Bool -> Bool -> Bool
&& Proof a
p Proof a -> Proof a -> Bool
forall a. Eq a => a -> a -> Bool
== Proof a
p'
  (AndElimR j :: Judgement a
j p :: Proof a
p) == (AndElimR j' :: Judgement a
j' p' :: Proof a
p') = Judgement a
j Judgement a -> Judgement a -> Bool
forall a. Eq a => a -> a -> Bool
== Judgement a
j' Bool -> Bool -> Bool
&& Proof a
p Proof a -> Proof a -> Bool
forall a. Eq a => a -> a -> Bool
== Proof a
p'
  (AndIntr j :: Judgement a
j p :: Proof a
p q :: Proof a
q) == (AndIntr j' :: Judgement a
j' p' :: Proof a
p' q' :: Proof a
q') = Judgement a
j Judgement a -> Judgement a -> Bool
forall a. Eq a => a -> a -> Bool
== Judgement a
j' Bool -> Bool -> Bool
&& Proof a
p Proof a -> Proof a -> Bool
forall a. Eq a => a -> a -> Bool
== Proof a
p' Bool -> Bool -> Bool
&& Proof a
q Proof a -> Proof a -> Bool
forall a. Eq a => a -> a -> Bool
== Proof a
q'
  (IffElimL j :: Judgement a
j p :: Proof a
p) == (IffElimL j' :: Judgement a
j' p' :: Proof a
p') = Judgement a
j Judgement a -> Judgement a -> Bool
forall a. Eq a => a -> a -> Bool
== Judgement a
j' Bool -> Bool -> Bool
&& Proof a
p Proof a -> Proof a -> Bool
forall a. Eq a => a -> a -> Bool
== Proof a
p'
  (IffElimR j :: Judgement a
j p :: Proof a
p) == (IffElimR j' :: Judgement a
j' p' :: Proof a
p') = Judgement a
j Judgement a -> Judgement a -> Bool
forall a. Eq a => a -> a -> Bool
== Judgement a
j' Bool -> Bool -> Bool
&& Proof a
p Proof a -> Proof a -> Bool
forall a. Eq a => a -> a -> Bool
== Proof a
p'
  (IffIntr j :: Judgement a
j p :: Proof a
p q :: Proof a
q) == (IffIntr j' :: Judgement a
j' p' :: Proof a
p' q' :: Proof a
q') = Judgement a
j Judgement a -> Judgement a -> Bool
forall a. Eq a => a -> a -> Bool
== Judgement a
j' Bool -> Bool -> Bool
&& Proof a
p Proof a -> Proof a -> Bool
forall a. Eq a => a -> a -> Bool
== Proof a
p' Bool -> Bool -> Bool
&& Proof a
q Proof a -> Proof a -> Bool
forall a. Eq a => a -> a -> Bool
== Proof a
q'
  _ == _ = Bool
False

instance Ord a => Ord (Proof a) where
  compare :: Proof a -> Proof a -> Ordering
compare p :: Proof a
p p' :: Proof a
p' = case Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Proof a -> Int
forall t. AST t => t -> Int
height Proof a
p) (Proof a -> Int
forall t. AST t => t -> Int
height Proof a
p') of
    EQ -> case Proof a
p of
      Axiom j :: Judgement a
j -> case Proof a
p' of
        Axiom j' :: Judgement a
j' -> Judgement a -> Judgement a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Judgement a
j Judgement a
j'
        _ -> Ordering
LT
      FalseElim j :: Judgement a
j q :: Proof a
q -> case Proof a
p' of
        Axiom {} -> Ordering
GT
        FalseElim j' :: Judgement a
j' q' :: Proof a
q' -> Judgement a -> Proof a -> Judgement a -> Proof a -> Ordering
forall a a. (Ord a, Ord a) => a -> a -> a -> a -> Ordering
compareUnary Judgement a
j Proof a
q Judgement a
j' Proof a
q'
        _ -> Ordering
LT
      TrueIntr j :: Judgement a
j -> case Proof a
p' of
        Axiom {} -> Ordering
GT
        FalseElim {} -> Ordering
GT
        TrueIntr j' :: Judgement a
j' -> Judgement a -> Judgement a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Judgement a
j Judgement a
j'
        _ -> Ordering
LT
      NotElim j :: Judgement a
j q :: Proof a
q r :: Proof a
r -> case Proof a
p' of
        Axiom {} -> Ordering
GT
        FalseElim {} -> Ordering
GT
        TrueIntr {} -> Ordering
GT
        NotElim j' :: Judgement a
j' q' :: Proof a
q' r' :: Proof a
r' -> Judgement a
-> Proof a
-> Proof a
-> Judgement a
-> Proof a
-> Proof a
-> Ordering
forall a a a.
(Ord a, Ord a, Ord a) =>
a -> a -> a -> a -> a -> a -> Ordering
compareBinary Judgement a
j Proof a
q Proof a
r Judgement a
j' Proof a
q' Proof a
r'
        _ -> Ordering
LT
      NotIntr j :: Judgement a
j q :: Proof a
q -> case Proof a
p' of
        Axiom {} -> Ordering
GT
        FalseElim {} -> Ordering
GT
        TrueIntr {} -> Ordering
GT
        NotElim {} -> Ordering
GT
        NotIntr j' :: Judgement a
j' q' :: Proof a
q' -> Judgement a -> Proof a -> Judgement a -> Proof a -> Ordering
forall a a. (Ord a, Ord a) => a -> a -> a -> a -> Ordering
compareUnary Judgement a
j Proof a
q Judgement a
j' Proof a
q'
        _ -> Ordering
LT
      ImpElim j :: Judgement a
j q :: Proof a
q r :: Proof a
r -> case Proof a
p' of
        Axiom {} -> Ordering
GT
        FalseElim {} -> Ordering
GT
        TrueIntr {} -> Ordering
GT
        NotElim {} -> Ordering
GT
        NotIntr {} -> Ordering
GT
        ImpElim j' :: Judgement a
j' q' :: Proof a
q' r' :: Proof a
r' -> Judgement a
-> Proof a
-> Proof a
-> Judgement a
-> Proof a
-> Proof a
-> Ordering
forall a a a.
(Ord a, Ord a, Ord a) =>
a -> a -> a -> a -> a -> a -> Ordering
compareBinary Judgement a
j Proof a
q Proof a
r Judgement a
j' Proof a
q' Proof a
r'
        _ -> Ordering
LT
      ImpIntr j :: Judgement a
j q :: Proof a
q -> case Proof a
p' of
        Axiom {} -> Ordering
GT
        FalseElim {} -> Ordering
GT
        TrueIntr {} -> Ordering
GT
        NotElim {} -> Ordering
GT
        NotIntr {} -> Ordering
GT
        ImpElim {} -> Ordering
GT
        ImpIntr j' :: Judgement a
j' q' :: Proof a
q' -> Judgement a -> Proof a -> Judgement a -> Proof a -> Ordering
forall a a. (Ord a, Ord a) => a -> a -> a -> a -> Ordering
compareUnary Judgement a
j Proof a
q Judgement a
j' Proof a
q'
        _ -> Ordering
LT
      OrElim j :: Judgement a
j q :: Proof a
q r :: Proof a
r s :: Proof a
s -> case Proof a
p' of
        Axiom {} -> Ordering
GT
        FalseElim {} -> Ordering
GT
        TrueIntr {} -> Ordering
GT
        NotElim {} -> Ordering
GT
        NotIntr {} -> Ordering
GT
        ImpElim {} -> Ordering
GT
        ImpIntr {} -> Ordering
GT
        OrElim j' :: Judgement a
j' q' :: Proof a
q' r' :: Proof a
r' s' :: Proof a
s' -> Judgement a
-> Proof a
-> Proof a
-> Proof a
-> Judgement a
-> Proof a
-> Proof a
-> Proof a
-> Ordering
forall a a a a.
(Ord a, Ord a, Ord a, Ord a) =>
a -> a -> a -> a -> a -> a -> a -> a -> Ordering
compareTernary Judgement a
j Proof a
q Proof a
r Proof a
s Judgement a
j' Proof a
q' Proof a
r' Proof a
s'
        _ -> Ordering
LT
      OrIntrL j :: Judgement a
j q :: Proof a
q -> case Proof a
p' of
        Axiom {} -> Ordering
GT
        FalseElim {} -> Ordering
GT
        TrueIntr {} -> Ordering
GT
        NotElim {} -> Ordering
GT
        NotIntr {} -> Ordering
GT
        ImpElim {} -> Ordering
GT
        ImpIntr {} -> Ordering
GT
        OrElim {} -> Ordering
GT
        OrIntrL j' :: Judgement a
j' q' :: Proof a
q' -> Judgement a -> Proof a -> Judgement a -> Proof a -> Ordering
forall a a. (Ord a, Ord a) => a -> a -> a -> a -> Ordering
compareUnary Judgement a
j Proof a
q Judgement a
j' Proof a
q'
        _ -> Ordering
LT
      OrIntrR j :: Judgement a
j q :: Proof a
q -> case Proof a
p' of
        Axiom {} -> Ordering
GT
        FalseElim {} -> Ordering
GT
        TrueIntr {} -> Ordering
GT
        NotElim {} -> Ordering
GT
        NotIntr {} -> Ordering
GT
        ImpElim {} -> Ordering
GT
        ImpIntr {} -> Ordering
GT
        OrElim {} -> Ordering
GT
        OrIntrL {} -> Ordering
GT
        OrIntrR j' :: Judgement a
j' q' :: Proof a
q' -> Judgement a -> Proof a -> Judgement a -> Proof a -> Ordering
forall a a. (Ord a, Ord a) => a -> a -> a -> a -> Ordering
compareUnary Judgement a
j Proof a
q Judgement a
j' Proof a
q'
        _ -> Ordering
LT
      AndElimL j :: Judgement a
j q :: Proof a
q -> case Proof a
p' of
        Axiom {} -> Ordering
GT
        FalseElim {} -> Ordering
GT
        TrueIntr {} -> Ordering
GT
        NotElim {} -> Ordering
GT
        NotIntr {} -> Ordering
GT
        ImpElim {} -> Ordering
GT
        ImpIntr {} -> Ordering
GT
        OrElim {} -> Ordering
GT
        OrIntrL {} -> Ordering
GT
        OrIntrR {} -> Ordering
GT
        AndElimL j' :: Judgement a
j' q' :: Proof a
q' -> Judgement a -> Proof a -> Judgement a -> Proof a -> Ordering
forall a a. (Ord a, Ord a) => a -> a -> a -> a -> Ordering
compareUnary Judgement a
j Proof a
q Judgement a
j' Proof a
q'
        _ -> Ordering
LT
      AndElimR j :: Judgement a
j q :: Proof a
q -> case Proof a
p' of
        Axiom {} -> Ordering
GT
        FalseElim {} -> Ordering
GT
        TrueIntr {} -> Ordering
GT
        NotElim {} -> Ordering
GT
        NotIntr {} -> Ordering
GT
        ImpElim {} -> Ordering
GT
        ImpIntr {} -> Ordering
GT
        OrElim {} -> Ordering
GT
        OrIntrL {} -> Ordering
GT
        OrIntrR {} -> Ordering
GT
        AndElimL {} -> Ordering
GT
        AndElimR j' :: Judgement a
j' q' :: Proof a
q' -> Judgement a -> Proof a -> Judgement a -> Proof a -> Ordering
forall a a. (Ord a, Ord a) => a -> a -> a -> a -> Ordering
compareUnary Judgement a
j Proof a
q Judgement a
j' Proof a
q'
        _ -> Ordering
LT
      AndIntr j :: Judgement a
j q :: Proof a
q r :: Proof a
r -> case Proof a
p' of
        Axiom {} -> Ordering
GT
        FalseElim {} -> Ordering
GT
        TrueIntr {} -> Ordering
GT
        NotElim {} -> Ordering
GT
        NotIntr {} -> Ordering
GT
        ImpElim {} -> Ordering
GT
        ImpIntr {} -> Ordering
GT
        OrElim {} -> Ordering
GT
        OrIntrL {} -> Ordering
GT
        OrIntrR {} -> Ordering
GT
        AndElimL {} -> Ordering
GT
        AndElimR {} -> Ordering
GT
        AndIntr j' :: Judgement a
j' q' :: Proof a
q' r' :: Proof a
r' -> Judgement a
-> Proof a
-> Proof a
-> Judgement a
-> Proof a
-> Proof a
-> Ordering
forall a a a.
(Ord a, Ord a, Ord a) =>
a -> a -> a -> a -> a -> a -> Ordering
compareBinary Judgement a
j Proof a
q Proof a
r Judgement a
j' Proof a
q' Proof a
r'
        _ -> Ordering
LT
      IffElimL j :: Judgement a
j q :: Proof a
q -> case Proof a
p' of
        Axiom {} -> Ordering
GT
        FalseElim {} -> Ordering
GT
        TrueIntr {} -> Ordering
GT
        NotElim {} -> Ordering
GT
        NotIntr {} -> Ordering
GT
        ImpElim {} -> Ordering
GT
        ImpIntr {} -> Ordering
GT
        OrElim {} -> Ordering
GT
        OrIntrL {} -> Ordering
GT
        OrIntrR {} -> Ordering
GT
        AndElimL {} -> Ordering
GT
        AndElimR {} -> Ordering
GT
        AndIntr {} -> Ordering
GT
        IffElimL j' :: Judgement a
j' q' :: Proof a
q' -> Judgement a -> Proof a -> Judgement a -> Proof a -> Ordering
forall a a. (Ord a, Ord a) => a -> a -> a -> a -> Ordering
compareUnary Judgement a
j Proof a
q Judgement a
j' Proof a
q'
        _ -> Ordering
LT
      IffElimR j :: Judgement a
j q :: Proof a
q -> case Proof a
p' of
        Axiom {} -> Ordering
GT
        FalseElim {} -> Ordering
GT
        TrueIntr {} -> Ordering
GT
        NotElim {} -> Ordering
GT
        NotIntr {} -> Ordering
GT
        ImpElim {} -> Ordering
GT
        ImpIntr {} -> Ordering
GT
        OrElim {} -> Ordering
GT
        OrIntrL {} -> Ordering
GT
        OrIntrR {} -> Ordering
GT
        AndElimL {} -> Ordering
GT
        AndElimR {} -> Ordering
GT
        AndIntr {} -> Ordering
GT
        IffElimL {} -> Ordering
GT
        IffElimR j' :: Judgement a
j' q' :: Proof a
q' -> Judgement a -> Proof a -> Judgement a -> Proof a -> Ordering
forall a a. (Ord a, Ord a) => a -> a -> a -> a -> Ordering
compareUnary Judgement a
j Proof a
q Judgement a
j' Proof a
q'
        _ -> Ordering
LT
      IffIntr j :: Judgement a
j q :: Proof a
q r :: Proof a
r -> case Proof a
p' of
        Axiom {} -> Ordering
GT
        FalseElim {} -> Ordering
GT
        TrueIntr {} -> Ordering
GT
        NotElim {} -> Ordering
GT
        NotIntr {} -> Ordering
GT
        ImpElim {} -> Ordering
GT
        ImpIntr {} -> Ordering
GT
        OrElim {} -> Ordering
GT
        OrIntrL {} -> Ordering
GT
        OrIntrR {} -> Ordering
GT
        AndElimL {} -> Ordering
GT
        AndElimR {} -> Ordering
GT
        AndIntr {} -> Ordering
GT
        IffElimL {} -> Ordering
GT
        IffElimR {} -> Ordering
GT
        IffIntr j' :: Judgement a
j' q' :: Proof a
q' r' :: Proof a
r' -> Judgement a
-> Proof a
-> Proof a
-> Judgement a
-> Proof a
-> Proof a
-> Ordering
forall a a a.
(Ord a, Ord a, Ord a) =>
a -> a -> a -> a -> a -> a -> Ordering
compareBinary Judgement a
j Proof a
q Proof a
r Judgement a
j' Proof a
q' Proof a
r'
    x :: Ordering
x -> Ordering
x
    where
      compareUnary :: a -> a -> a -> a -> Ordering
compareUnary j :: a
j q :: a
q j' :: a
j' q' :: a
q' = case a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
j a
j' of
        EQ -> a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
q a
q'
        x :: Ordering
x -> Ordering
x
      compareBinary :: a -> a -> a -> a -> a -> a -> Ordering
compareBinary j :: a
j q :: a
q r :: a
r j' :: a
j' q' :: a
q' r' :: a
r' = case a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
j a
j' of
        EQ -> case a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
q a
q' of
          EQ -> a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
r a
r'
          y :: Ordering
y -> Ordering
y
        x :: Ordering
x -> Ordering
x
      compareTernary :: a -> a -> a -> a -> a -> a -> a -> a -> Ordering
compareTernary j :: a
j q :: a
q r :: a
r s :: a
s j' :: a
j' q' :: a
q' r' :: a
r' s' :: a
s' = case a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
j a
j' of
        EQ -> case a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
q a
q' of
          EQ -> case a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
r a
r' of
            EQ -> a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
s a
s'
            z :: Ordering
z -> Ordering
z
          y :: Ordering
y -> Ordering
y
        x :: Ordering
x -> Ordering
x

instance Show a => Show (Proof a) where
  showsPrec :: Int -> Proof a -> ShowS
showsPrec d :: Int
d = Bool -> Proof a -> ShowS
f (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
appPrec)
    where
      appPrec :: Int
appPrec = 10

      f :: Bool -> Proof a -> ShowS
f b :: Bool
b a :: Proof a
a = Bool -> ShowS -> ShowS
showParen Bool
b (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Proof a -> ShowS
g Proof a
a

      g :: Proof a -> ShowS
g (Axiom j :: Judgement a
j) = String -> Judgement a -> ShowS
showsNullary "Axiom " Judgement a
j
      g (FalseElim j :: Judgement a
j p :: Proof a
p) = String -> Judgement a -> Proof a -> ShowS
showsUnary "FalseElim " Judgement a
j Proof a
p
      g (TrueIntr j :: Judgement a
j) = String -> Judgement a -> ShowS
showsNullary "TrueIntr " Judgement a
j
      g (NotElim j :: Judgement a
j p :: Proof a
p q :: Proof a
q) = String -> Judgement a -> Proof a -> Proof a -> ShowS
showsBinary "NotElim " Judgement a
j Proof a
p Proof a
q
      g (NotIntr j :: Judgement a
j p :: Proof a
p) = String -> Judgement a -> Proof a -> ShowS
showsUnary "NotIntr " Judgement a
j Proof a
p
      g (ImpElim j :: Judgement a
j p :: Proof a
p q :: Proof a
q) = String -> Judgement a -> Proof a -> Proof a -> ShowS
showsBinary "ImpElim " Judgement a
j Proof a
p Proof a
q
      g (ImpIntr j :: Judgement a
j p :: Proof a
p) = String -> Judgement a -> Proof a -> ShowS
showsUnary "ImpIntr " Judgement a
j Proof a
p
      g (OrElim j :: Judgement a
j p :: Proof a
p q :: Proof a
q r :: Proof a
r) = String -> Judgement a -> Proof a -> Proof a -> Proof a -> ShowS
showsTernary "OrElim " Judgement a
j Proof a
p Proof a
q Proof a
r
      g (OrIntrL j :: Judgement a
j p :: Proof a
p) = String -> Judgement a -> Proof a -> ShowS
showsUnary "OrIntrL " Judgement a
j Proof a
p
      g (OrIntrR j :: Judgement a
j p :: Proof a
p) = String -> Judgement a -> Proof a -> ShowS
showsUnary "OrIntrR " Judgement a
j Proof a
p
      g (AndElimL j :: Judgement a
j p :: Proof a
p) = String -> Judgement a -> Proof a -> ShowS
showsUnary "AndElimL " Judgement a
j Proof a
p
      g (AndElimR j :: Judgement a
j p :: Proof a
p) = String -> Judgement a -> Proof a -> ShowS
showsUnary "AndElimR " Judgement a
j Proof a
p
      g (AndIntr j :: Judgement a
j p :: Proof a
p q :: Proof a
q) = String -> Judgement a -> Proof a -> Proof a -> ShowS
showsBinary "AndIntr " Judgement a
j Proof a
p Proof a
q
      g (IffElimL j :: Judgement a
j p :: Proof a
p) = String -> Judgement a -> Proof a -> ShowS
showsUnary "IffElimL " Judgement a
j Proof a
p
      g (IffElimR j :: Judgement a
j p :: Proof a
p) = String -> Judgement a -> Proof a -> ShowS
showsUnary "IffElimR " Judgement a
j Proof a
p
      g (IffIntr j :: Judgement a
j p :: Proof a
p q :: Proof a
q) = String -> Judgement a -> Proof a -> Proof a -> ShowS
showsBinary "IffIntr " Judgement a
j Proof a
p Proof a
q

      showsNullary :: String -> Judgement a -> ShowS
showsNullary c :: String
c j :: Judgement a
j = String -> ShowS
showString String
c ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Judgement a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec (Int
appPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) Judgement a
j

      showsUnary :: String -> Judgement a -> Proof a -> ShowS
showsUnary c :: String
c j :: Judgement a
j p :: Proof a
p =
        String -> ShowS
showString String
c ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Judgement a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec (Int
appPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) Judgement a
j
          ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString " "
          ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Proof a -> ShowS
f Bool
True Proof a
p

      showsBinary :: String -> Judgement a -> Proof a -> Proof a -> ShowS
showsBinary c :: String
c j :: Judgement a
j p :: Proof a
p q :: Proof a
q =
        String -> ShowS
showString String
c ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Judgement a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec (Int
appPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) Judgement a
j
          ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString " "
          ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Proof a -> ShowS
f Bool
True Proof a
p
          ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString " "
          ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Proof a -> ShowS
f Bool
True Proof a
q

      showsTernary :: String -> Judgement a -> Proof a -> Proof a -> Proof a -> ShowS
showsTernary c :: String
c j :: Judgement a
j p :: Proof a
p q :: Proof a
q r :: Proof a
r =
        String -> ShowS
showString String
c ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Judgement a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec (Int
appPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) Judgement a
j
          ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString " "
          ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Proof a -> ShowS
f Bool
True Proof a
p
          ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString " "
          ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Proof a -> ShowS
f Bool
True Proof a
q
          ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString " "
          ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Proof a -> ShowS
f Bool
True Proof a
r

instance (Ord a, Read a) => Read (Proof a) where
  readsPrec :: Int -> ReadS (Proof a)
readsPrec d :: Int
d = Bool -> ReadS (Proof a)
f (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
appPrec)
    where
      appPrec :: Int
appPrec = 10

      f :: Bool -> ReadS (Proof a)
f b :: Bool
b s :: String
s = (ReadS (Proof a) -> [(Proof a, String)])
-> [ReadS (Proof a)] -> [(Proof a, String)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((ReadS (Proof a) -> ReadS (Proof a)
forall a b. (a -> b) -> a -> b
$ String
s) (ReadS (Proof a) -> [(Proof a, String)])
-> (ReadS (Proof a) -> ReadS (Proof a))
-> ReadS (Proof a)
-> [(Proof a, String)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> ReadS (Proof a) -> ReadS (Proof a)
forall a. Bool -> ReadS a -> ReadS a
readParen Bool
b) [ReadS (Proof a)]
readers
      readers :: [ReadS (Proof a)]
readers =
        [ ReadS (Proof a)
readAxiom,
          ReadS (Proof a)
readFalseElim,
          ReadS (Proof a)
readTrueIntr,
          ReadS (Proof a)
readNotElim,
          ReadS (Proof a)
readNotIntr,
          ReadS (Proof a)
readImpElim,
          ReadS (Proof a)
readImpIntr,
          ReadS (Proof a)
readOrElim,
          ReadS (Proof a)
readOrIntrL,
          ReadS (Proof a)
readOrIntrR,
          ReadS (Proof a)
readAndElimL,
          ReadS (Proof a)
readAndElimR,
          ReadS (Proof a)
readAndIntr,
          ReadS (Proof a)
readIffElimL,
          ReadS (Proof a)
readIffElimR,
          ReadS (Proof a)
readIffIntr
        ]
      readAxiom :: ReadS (Proof a)
readAxiom = (Judgement a -> Proof a) -> String -> ReadS (Proof a)
parseNullary Judgement a -> Proof a
forall a. Judgement a -> Proof a
Axiom "Axiom"
      readFalseElim :: ReadS (Proof a)
readFalseElim = (Judgement a -> Proof a -> Proof a) -> String -> ReadS (Proof a)
parseUnary Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
FalseElim "FalseElim"
      readTrueIntr :: ReadS (Proof a)
readTrueIntr = (Judgement a -> Proof a) -> String -> ReadS (Proof a)
parseNullary Judgement a -> Proof a
forall a. Judgement a -> Proof a
TrueIntr "TrueIntr"
      readNotElim :: ReadS (Proof a)
readNotElim = (Judgement a -> Proof a -> Proof a -> Proof a)
-> String -> ReadS (Proof a)
parseBinary Judgement a -> Proof a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a -> Proof a
NotElim "NotElim"
      readNotIntr :: ReadS (Proof a)
readNotIntr = (Judgement a -> Proof a -> Proof a) -> String -> ReadS (Proof a)
parseUnary Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
NotIntr "NotIntr"
      readImpElim :: ReadS (Proof a)
readImpElim = (Judgement a -> Proof a -> Proof a -> Proof a)
-> String -> ReadS (Proof a)
parseBinary Judgement a -> Proof a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a -> Proof a
ImpElim "ImpElim"
      readImpIntr :: ReadS (Proof a)
readImpIntr = (Judgement a -> Proof a -> Proof a) -> String -> ReadS (Proof a)
parseUnary Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
ImpIntr "ImpIntr"
      readOrElim :: ReadS (Proof a)
readOrElim = (Judgement a -> Proof a -> Proof a -> Proof a -> Proof a)
-> String -> ReadS (Proof a)
parseTernary Judgement a -> Proof a -> Proof a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a -> Proof a -> Proof a
OrElim "OrElim"
      readOrIntrL :: ReadS (Proof a)
readOrIntrL = (Judgement a -> Proof a -> Proof a) -> String -> ReadS (Proof a)
parseUnary Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
OrIntrL "OrIntrL"
      readOrIntrR :: ReadS (Proof a)
readOrIntrR = (Judgement a -> Proof a -> Proof a) -> String -> ReadS (Proof a)
parseUnary Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
OrIntrR "OrIntrR"
      readAndElimL :: ReadS (Proof a)
readAndElimL = (Judgement a -> Proof a -> Proof a) -> String -> ReadS (Proof a)
parseUnary Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
AndElimL "AndElimL"
      readAndElimR :: ReadS (Proof a)
readAndElimR = (Judgement a -> Proof a -> Proof a) -> String -> ReadS (Proof a)
parseUnary Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
AndElimR "AndElimR"
      readAndIntr :: ReadS (Proof a)
readAndIntr = (Judgement a -> Proof a -> Proof a -> Proof a)
-> String -> ReadS (Proof a)
parseBinary Judgement a -> Proof a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a -> Proof a
AndIntr "AndIntr"
      readIffElimL :: ReadS (Proof a)
readIffElimL = (Judgement a -> Proof a -> Proof a) -> String -> ReadS (Proof a)
parseUnary Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
IffElimL "IffElimL"
      readIffElimR :: ReadS (Proof a)
readIffElimR = (Judgement a -> Proof a -> Proof a) -> String -> ReadS (Proof a)
parseUnary Judgement a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a
IffElimR "IffElimR"
      readIffIntr :: ReadS (Proof a)
readIffIntr = (Judgement a -> Proof a -> Proof a -> Proof a)
-> String -> ReadS (Proof a)
parseBinary Judgement a -> Proof a -> Proof a -> Proof a
forall a. Judgement a -> Proof a -> Proof a -> Proof a
IffIntr "IffIntr"

      parseNullary :: (Judgement a -> Proof a) -> String -> ReadS (Proof a)
parseNullary c :: Judgement a -> Proof a
c n :: String
n s :: String
s =
        [ (Judgement a -> Proof a
c Judgement a
j, String
u)
          | (n' :: String
n', t :: String
t) <- ReadS String
lex String
s,
            String
n String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
n',
            (j :: Judgement a
j, u :: String
u) <- Int -> ReadS (Judgement a)
forall a. Read a => Int -> ReadS a
readsPrec (Int
appPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) String
t
        ]
      parseUnary :: (Judgement a -> Proof a -> Proof a) -> String -> ReadS (Proof a)
parseUnary c :: Judgement a -> Proof a -> Proof a
c n :: String
n s :: String
s =
        [ (Judgement a -> Proof a -> Proof a
c Judgement a
j Proof a
p, String
v)
          | (n' :: String
n', t :: String
t) <- ReadS String
lex String
s,
            String
n String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
n',
            (j :: Judgement a
j, u :: String
u) <- Int -> ReadS (Judgement a)
forall a. Read a => Int -> ReadS a
readsPrec (Int
appPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) String
t,
            (p :: Proof a
p, v :: String
v) <- Bool -> ReadS (Proof a)
f Bool
True String
u
        ]
      parseBinary :: (Judgement a -> Proof a -> Proof a -> Proof a)
-> String -> ReadS (Proof a)
parseBinary c :: Judgement a -> Proof a -> Proof a -> Proof a
c n :: String
n s :: String
s =
        [ (Judgement a -> Proof a -> Proof a -> Proof a
c Judgement a
j Proof a
p Proof a
q, String
w)
          | (n' :: String
n', t :: String
t) <- ReadS String
lex String
s,
            String
n String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
n',
            (j :: Judgement a
j, u :: String
u) <- Int -> ReadS (Judgement a)
forall a. Read a => Int -> ReadS a
readsPrec (Int
appPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) String
t,
            (p :: Proof a
p, v :: String
v) <- Bool -> ReadS (Proof a)
f Bool
True String
u,
            (q :: Proof a
q, w :: String
w) <- Bool -> ReadS (Proof a)
f Bool
True String
v
        ]
      parseTernary :: (Judgement a -> Proof a -> Proof a -> Proof a -> Proof a)
-> String -> ReadS (Proof a)
parseTernary c :: Judgement a -> Proof a -> Proof a -> Proof a -> Proof a
c n :: String
n s :: String
s =
        [ (Judgement a -> Proof a -> Proof a -> Proof a -> Proof a
c Judgement a
j Proof a
p Proof a
q Proof a
r, String
x)
          | (n' :: String
n', t :: String
t) <- ReadS String
lex String
s,
            String
n String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
n',
            (j :: Judgement a
j, u :: String
u) <- Int -> ReadS (Judgement a)
forall a. Read a => Int -> ReadS a
readsPrec (Int
appPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) String
t,
            (p :: Proof a
p, v :: String
v) <- Bool -> ReadS (Proof a)
f Bool
True String
u,
            (q :: Proof a
q, w :: String
w) <- Bool -> ReadS (Proof a)
f Bool
True String
v,
            (r :: Proof a
r, x :: String
x) <- Bool -> ReadS (Proof a)
f Bool
True String
w
        ]

instance PrettyPrintable a => PrettyPrintable (Proof a) where
  -- Adapted from drawTree in Data.Tree from the containers package
  pretty :: Proof a -> String
pretty = [String] -> String
unlines ([String] -> String) -> (Proof a -> [String]) -> Proof a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> [String]
forall a. [a] -> [a]
reverse ([String] -> [String])
-> (Proof a -> [String]) -> Proof a -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proof a -> [String]
forall a. PrettyPrintable a => Proof a -> [String]
draw
    where
      draw :: Proof a -> [String]
draw p :: Proof a
p = Proof a -> String
forall a. PrettyPrintable a => Proof a -> String
line Proof a
p String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [Proof a] -> [String]
drawPremises ([Proof a] -> [Proof a]
forall a. [a] -> [a]
reverse (Proof a -> [Proof a]
forall t. AST t => t -> [t]
children Proof a
p))

      line :: Proof a -> String
line p :: Proof a
p = Proof a -> String
forall a. Proof a -> String
rule Proof a
p String -> ShowS
forall a. [a] -> [a] -> [a]
++ " " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Judgement a -> String
forall a. PrettyPrintable a => a -> String
pretty (Proof a -> Root (Proof a)
forall t. AST t => t -> Root t
root Proof a
p)

      drawPremises :: [Proof a] -> [String]
drawPremises [] = []
      drawPremises [q :: Proof a
q] =
        String
vertS String -> [String] -> [String]
forall a. a -> [a] -> [a]
: String -> String -> [String] -> [String]
forall a. [a] -> [a] -> [[a]] -> [[a]]
shift String
cornerS "    " (Proof a -> [String]
draw Proof a
q)
      drawPremises (q :: Proof a
q : qs :: [Proof a]
qs) =
        String
vertS String -> [String] -> [String]
forall a. a -> [a] -> [a]
: String -> String -> [String] -> [String]
forall a. [a] -> [a] -> [[a]] -> [[a]]
shift String
branchS (String
vertS String -> ShowS
forall a. [a] -> [a] -> [a]
++ "   ") (Proof a -> [String]
draw Proof a
q) [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [Proof a] -> [String]
drawPremises [Proof a]
qs

      shift :: [a] -> [a] -> [[a]] -> [[a]]
shift first :: [a]
first other :: [a]
other = ([a] -> [a] -> [a]) -> [[a]] -> [[a]] -> [[a]]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
(++) ([a]
first [a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
: [a] -> [[a]]
forall a. a -> [a]
repeat [a]
other)

      rule :: Proof a -> String
rule Axiom {} = String
axiomS
      rule FalseElim {} = String
falseElimS
      rule TrueIntr {} = String
trueIntrS
      rule NotElim {} = String
notElimS
      rule NotIntr {} = String
notIntrS
      rule ImpElim {} = String
impElimS
      rule ImpIntr {} = String
impIntrS
      rule OrElim {} = String
orElimS
      rule OrIntrL {} = String
orIntrLS
      rule OrIntrR {} = String
orIntrRS
      rule AndElimL {} = String
andElimLS
      rule AndElimR {} = String
andElimRS
      rule AndIntr {} = String
andIntrS
      rule IffElimL {} = String
iffElimLS
      rule IffElimR {} = String
iffElimRS
      rule IffIntr {} = String
iffIntrS

-- | Get a pretty-printed representation of a proof.
prettyProof :: PrettyPrintable a => Proof a -> String
prettyProof :: Proof a -> String
prettyProof = Proof a -> String
forall a. PrettyPrintable a => a -> String
pretty