    {-# LANGUAGE CPP #-}

    #if (__GLASGOW_HASKELL__ >= 802)
    {-# LANGUAGE DerivingStrategies #-}
    #endif

    --------------------------------------------------------------------------------
    --  See end of this file for licence information.
    --------------------------------------------------------------------------------
    -- |
    --  Module      :  Proof
    --  Copyright   :  (c) 2003, Graham Klyne, 2009 Vasili I Galchin,
    --                 2011, 2016, 2022, 2024 Douglas Burke
    --  License     :  GPL V2
    --
    --  Maintainer  :  Douglas Burke
    --  Stability   :  experimental
    --  Portability :  CPP, DerivingStrategies
    --
    --  This module defines a framework for constructing proofs
    --  over some expression form.  It is intended to be used
    --  with RDF graphs, but the structures aim to be quite
    --  generic with respect to the expression forms allowed.
    --
    --  It does not define any proof-finding strategy.
    --
    --------------------------------------------------------------------------------

    module Swish.Proof
        ( Proof(..), Step(..)
        , checkProof, explainProof, checkStep, showProof, showsProof, showsFormula )
    where

    import qualified Data.Set as S

    import Data.Foldable(Foldable(..))
    import Data.List (union, intersect, intercalate)
    import Data.Maybe (catMaybes, isNothing)
    import Data.String.ShowLines (ShowLines(..))

    -- Avoid messages added in GHC 9.10 about foldl' import from Data.List
    -- being redundant.
    import Prelude hiding (Foldable(..))

    import Swish.Rule (Expression(..), Formula(..), Rule(..))
    import Swish.Rule (showsFormula, showsFormulae)
    import Swish.Ruleset (Ruleset(..))

    ------------------------------------------------------------
    --  Proof framework
    ------------------------------------------------------------

    -- |Step in proof chain
    --
    --  The display name for a proof step comes from the display name of its
    --  consequence formula.
    data Step ex = Step
        { forall ex. Step ex -> Rule ex
    stepRule :: Rule ex           -- ^ Inference rule used
        , forall ex. Step ex -> [Formula ex]
    stepAnt  :: [Formula ex]      -- ^ Antecedents of inference rule
        , forall ex. Step ex -> Formula ex
    stepCon  :: Formula ex        -- ^ Named consequence of inference rule
        } deriving
    #if (__GLASGOW_HASKELL__ >= 802)
        stock
    #endif
        Int -> Step ex -> ShowS
    [Step ex] -> ShowS
    Step ex -> String
    (Int -> Step ex -> ShowS)
    -> (Step ex -> String) -> ([Step ex] -> ShowS) -> Show (Step ex)
    forall ex. Show ex => Int -> Step ex -> ShowS
    forall ex. Show ex => [Step ex] -> ShowS
    forall ex. Show ex => Step ex -> String
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall ex. Show ex => Int -> Step ex -> ShowS
    showsPrec :: Int -> Step ex -> ShowS
    $cshow :: forall ex. Show ex => Step ex -> String
    show :: Step ex -> String
    $cshowList :: forall ex. Show ex => [Step ex] -> ShowS
    showList :: [Step ex] -> ShowS
    Show

    -- |Proof is a structure that presents a chain of rule applications
    --  that yield a result expression from a given expression
    data Proof ex = Proof
        { forall ex. Proof ex -> [Ruleset ex]
    proofContext :: [Ruleset ex]  -- ^ Proof context:  list of rulesets,
                                        --   each of which provides a number of
                                        --   axioms and rules.
        , forall ex. Proof ex -> Formula ex
    proofInput   :: Formula ex    -- ^ Given expression
        , forall ex. Proof ex -> Formula ex
    proofResult  :: Formula ex    -- ^ Result expression
        , forall ex. Proof ex -> [Step ex]
    proofChain   :: [Step ex]     -- ^ Chain of inference rule applications
                                        --   progressing from input to result
        }

    -- |Return a list of axioms from all the rulesets in a proof
    proofAxioms :: Proof a -> [Formula a]
    proofAxioms :: forall a. Proof a -> [Formula a]
    proofAxioms = (Ruleset a -> [Formula a]) -> [Ruleset a] -> [Formula a]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap Ruleset a -> [Formula a]
    forall ex. Ruleset ex -> [Formula ex]
    rsAxioms ([Ruleset a] -> [Formula a])
    -> (Proof a -> [Ruleset a]) -> Proof a -> [Formula a]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Proof a -> [Ruleset a]
    forall ex. Proof ex -> [Ruleset ex]
    proofContext

    -- |Return a list of rules from all the rulesets in a proof
    proofRules :: Proof a -> [Rule a]
    proofRules :: forall a. Proof a -> [Rule a]
    proofRules = (Ruleset a -> [Rule a]) -> [Ruleset a] -> [Rule a]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap Ruleset a -> [Rule a]
    forall ex. Ruleset ex -> [Rule ex]
    rsRules ([Ruleset a] -> [Rule a])
    -> (Proof a -> [Ruleset a]) -> Proof a -> [Rule a]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Proof a -> [Ruleset a]
    forall ex. Proof ex -> [Ruleset ex]
    proofContext

    -- |Return list of axioms actually referenced by a proof
    proofAxiomsUsed :: Proof ex -> [Formula ex]
    proofAxiomsUsed :: forall a. Proof a -> [Formula a]
    proofAxiomsUsed Proof ex
    proof = ([Formula ex] -> [Formula ex] -> [Formula ex])
    -> [Formula ex] -> [[Formula ex]] -> [Formula ex]
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl' [Formula ex] -> [Formula ex] -> [Formula ex]
    forall a. Eq a => [a] -> [a] -> [a]
    union [] ([[Formula ex]] -> [Formula ex]) -> [[Formula ex]] -> [Formula ex]
    forall a b. (a -> b) -> a -> b
    $ (Step ex -> [Formula ex]) -> [Step ex] -> [[Formula ex]]
    forall a b. (a -> b) -> [a] -> [b]
    map Step ex -> [Formula ex]
    stepAxioms (Proof ex -> [Step ex]
    forall ex. Proof ex -> [Step ex]
    proofChain Proof ex
    proof)
        where
            stepAxioms :: Step ex -> [Formula ex]
    stepAxioms Step ex
    st = Step ex -> [Formula ex]
    forall ex. Step ex -> [Formula ex]
    stepAnt Step ex
    st [Formula ex] -> [Formula ex] -> [Formula ex]
    forall a. Eq a => [a] -> [a] -> [a]
    `intersect` Proof ex -> [Formula ex]
    forall a. Proof a -> [Formula a]
    proofAxioms Proof ex
    proof

    -- |Check consistency of given proof.
    --  The supplied rules and axioms are assumed to be correct.
    checkProof ::
        (Expression ex, Ord ex)
        => Proof ex -> Bool
    checkProof :: forall ex. (Expression ex, Ord ex) => Proof ex -> Bool
    checkProof Proof ex
    pr =
        [Rule ex] -> [ex] -> [Step ex] -> ex -> Bool
    forall ex.
    (Expression ex, Ord ex) =>
    [Rule ex] -> [ex] -> [Step ex] -> ex -> Bool
    checkProof1 (Proof ex -> [Rule ex]
    forall a. Proof a -> [Rule a]
    proofRules Proof ex
    pr) [ex]
    initExpr (Proof ex -> [Step ex]
    forall ex. Proof ex -> [Step ex]
    proofChain Proof ex
    pr) ex
    goalExpr
        where
            initExpr :: [ex]
    initExpr = Formula ex -> ex
    forall ex. Formula ex -> ex
    formExpr (Proof ex -> Formula ex
    forall ex. Proof ex -> Formula ex
    proofInput Proof ex
    pr) ex -> [ex] -> [ex]
    forall a. a -> [a] -> [a]
    : (Formula ex -> ex) -> [Formula ex] -> [ex]
    forall a b. (a -> b) -> [a] -> [b]
    map Formula ex -> ex
    forall ex. Formula ex -> ex
    formExpr (Proof ex -> [Formula ex]
    forall a. Proof a -> [Formula a]
    proofAxioms Proof ex
    pr)
            goalExpr :: ex
    goalExpr = Formula ex -> ex
    forall ex. Formula ex -> ex
    formExpr (Formula ex -> ex) -> Formula ex -> ex
    forall a b. (a -> b) -> a -> b
    $ Proof ex -> Formula ex
    forall ex. Proof ex -> Formula ex
    proofResult Proof ex
    pr

    checkProof1 ::
        (Expression ex, Ord ex)
        => [Rule ex] -> [ex] -> [Step ex] -> ex -> Bool
    checkProof1 :: forall ex.
    (Expression ex, Ord ex) =>
    [Rule ex] -> [ex] -> [Step ex] -> ex -> Bool
    checkProof1 [Rule ex]
    _     [ex]
    prev []       ex
    res = ex
    res ex -> [ex] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [ex]
    prev
    checkProof1 [Rule ex]
    rules [ex]
    prev (Step ex
    st:[Step ex]
    steps) ex
    res =
        [Rule ex] -> [ex] -> Step ex -> Bool
    forall ex. Ord ex => [Rule ex] -> [ex] -> Step ex -> Bool
    checkStep [Rule ex]
    rules [ex]
    prev Step ex
    st Bool -> Bool -> Bool
    &&
        [Rule ex] -> [ex] -> [Step ex] -> ex -> Bool
    forall ex.
    (Expression ex, Ord ex) =>
    [Rule ex] -> [ex] -> [Step ex] -> ex -> Bool
    checkProof1 [Rule ex]
    rules (Formula ex -> ex
    forall ex. Formula ex -> ex
    formExpr (Step ex -> Formula ex
    forall ex. Step ex -> Formula ex
    stepCon Step ex
    st)ex -> [ex] -> [ex]
    forall a. a -> [a] -> [a]
    :[ex]
    prev) [Step ex]
    steps ex
    res

    -- | A proof step is valid if rule is in list of rules
    --  and the antecedents are sufficient to obtain the conclusion
    --  and the antecedents are in the list of formulae already proven.
    --
    --  Note:  this function depends on the ruleName of any rule being
    --  unique among all rules.  In particular the name of the step rule
    --  being in correspondence with the name of one of the indicated
    --  valid rules of inference.
    checkStep ::
      Ord ex
      => [Rule ex]   -- ^ rules
      -> [ex]        -- ^ antecedants
      -> Step ex     -- ^ the step to validate
      -> Bool        -- ^ @True@ if the step is valid

    checkStep :: forall ex. Ord ex => [Rule ex] -> [ex] -> Step ex -> Bool
    checkStep [Rule ex]
    rules [ex]
    prev Step ex
    step = Maybe String -> Bool
    forall a. Maybe a -> Bool
    isNothing (Maybe String -> Bool) -> Maybe String -> Bool
    forall a b. (a -> b) -> a -> b
    $ [Rule ex] -> [ex] -> Step ex -> Maybe String
    forall ex. Ord ex => [Rule ex] -> [ex] -> Step ex -> Maybe String
    explainStep [Rule ex]
    rules [ex]
    prev Step ex
    step

    {-

    Is the following an optimisation of the above?

    checkStep rules prev step =
        -- Rule name is one of supplied rules, and
        (ruleName srul `elem` map ruleName rules) &&
        -- Antecedent expressions are all previously accepted expressions
        (sant `subset` prev)   &&
        -- Inference rule yields concequence from antecendents
        checkInference srul sant scon
        where
            --  Rule from proof step:
            srul = stepRule step
            --  Antecedent expressions from proof step:
            sant = map formExpr $ stepAnt step
            --  Consequentent expression from proof step:
            scon = formExpr $ stepCon step
    -}

    {-
        (formExpr (stepCon step) `elem` sfwd)
        -- (or $ map (`subset` sant) sbwd)
        where
            --  Rule from proof step:
            srul = stepRule step
            --  Antecedent expressions from proof step:
            sant = map formExpr $ stepAnt step
            --  Forward chaining from antecedents of proof step
            scon = map formExpr $ stepCon step
            --  Forward chaining from antecedents of proof step

            sfwd = fwdApply srul sant
            --  Backward chaining from consequent of proof step
            --  (Does not work because of introduction of existentials)
            sbwd = bwdApply srul (formExpr $ stepCon step)
    -}

    -- |Check proof. If there is an error then return information
    -- about the failing step.
    explainProof ::
        (Expression ex, Ord ex) => Proof ex -> Maybe String
    explainProof :: forall ex. (Expression ex, Ord ex) => Proof ex -> Maybe String
    explainProof Proof ex
    pr =
        [Rule ex] -> [ex] -> [Step ex] -> ex -> Maybe String
    forall ex.
    (Expression ex, Ord ex) =>
    [Rule ex] -> [ex] -> [Step ex] -> ex -> Maybe String
    explainProof1 (Proof ex -> [Rule ex]
    forall a. Proof a -> [Rule a]
    proofRules Proof ex
    pr) [ex]
    initExpr (Proof ex -> [Step ex]
    forall ex. Proof ex -> [Step ex]
    proofChain Proof ex
    pr) ex
    goalExpr
        where
            initExpr :: [ex]
    initExpr = Formula ex -> ex
    forall ex. Formula ex -> ex
    formExpr (Proof ex -> Formula ex
    forall ex. Proof ex -> Formula ex
    proofInput Proof ex
    pr) ex -> [ex] -> [ex]
    forall a. a -> [a] -> [a]
    : (Formula ex -> ex) -> [Formula ex] -> [ex]
    forall a b. (a -> b) -> [a] -> [b]
    map Formula ex -> ex
    forall ex. Formula ex -> ex
    formExpr (Proof ex -> [Formula ex]
    forall a. Proof a -> [Formula a]
    proofAxioms Proof ex
    pr)
            goalExpr :: ex
    goalExpr = Formula ex -> ex
    forall ex. Formula ex -> ex
    formExpr (Formula ex -> ex) -> Formula ex -> ex
    forall a b. (a -> b) -> a -> b
    $ Proof ex -> Formula ex
    forall ex. Proof ex -> Formula ex
    proofResult Proof ex
    pr

    explainProof1 ::
        (Expression ex, Ord ex)
        => [Rule ex] -> [ex] -> [Step ex] -> ex -> Maybe String
    explainProof1 :: forall ex.
    (Expression ex, Ord ex) =>
    [Rule ex] -> [ex] -> [Step ex] -> ex -> Maybe String
    explainProof1 [Rule ex]
    _     [ex]
    prev []       ex
    res   =
        if ex
    res ex -> [ex] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [ex]
    prev then Maybe String
    forall a. Maybe a
    Nothing else String -> Maybe String
    forall a. a -> Maybe a
    Just String
    "Result not demonstrated"
    explainProof1 [Rule ex]
    rules [ex]
    prev (Step ex
    st:[Step ex]
    steps) ex
    res =
        case [Rule ex] -> [ex] -> Step ex -> Maybe String
    forall ex. Ord ex => [Rule ex] -> [ex] -> Step ex -> Maybe String
    explainStep [Rule ex]
    rules [ex]
    prev Step ex
    st  of
            Maybe String
    Nothing -> [Rule ex] -> [ex] -> [Step ex] -> ex -> Maybe String
    forall ex.
    (Expression ex, Ord ex) =>
    [Rule ex] -> [ex] -> [Step ex] -> ex -> Maybe String
    explainProof1 [Rule ex]
    rules (Formula ex -> ex
    forall ex. Formula ex -> ex
    formExpr (Step ex -> Formula ex
    forall ex. Step ex -> Formula ex
    stepCon Step ex
    st)ex -> [ex] -> [ex]
    forall a. a -> [a] -> [a]
    :[ex]
    prev) [Step ex]
    steps ex
    res
            Just String
    ex -> String -> Maybe String
    forall a. a -> Maybe a
    Just (String
    "Invalid step: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ScopedName -> String
    forall a. Show a => a -> String
    show (Formula ex -> ScopedName
    forall ex. Formula ex -> ScopedName
    formName (Formula ex -> ScopedName) -> Formula ex -> ScopedName
    forall a b. (a -> b) -> a -> b
    $ Step ex -> Formula ex
    forall ex. Step ex -> Formula ex
    stepCon Step ex
    st) String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ": " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ex)

    -- | A proof step is valid if rule is in list of rules
    --  and the antecedents are sufficient to obtain the conclusion
    --  and the antecedents are in the list of formulae already proven.
    --
    --  Note:  this function depends on the ruleName of any rule being
    --  unique among all rules.  In particular the name of the step rule
    --  being in correspondence with the name of one of the indicated
    --  valid rules of inference.
    --
    explainStep ::
      Ord ex
      => [Rule ex]  -- ^ rules
      -> [ex]       -- ^ previous
      -> Step ex    -- ^ step
      -> Maybe String -- ^ @Nothing@ if step is okay, otherwise a string indicating the error
    explainStep :: forall ex. Ord ex => [Rule ex] -> [ex] -> Step ex -> Maybe String
    explainStep [Rule ex]
    rules [ex]
    prev Step ex
    step =
            if [String] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [String]
    errors then Maybe String
    forall a. Maybe a
    Nothing else String -> Maybe String
    forall a. a -> Maybe a
    Just (String -> Maybe String) -> String -> Maybe String
    forall a b. (a -> b) -> a -> b
    $ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    ", " [String]
    errors
        where
            --  Rule from proof step:
            srul :: Rule ex
    srul = Step ex -> Rule ex
    forall ex. Step ex -> Rule ex
    stepRule Step ex
    step
            --  Antecedent expressions from proof step:
            sant :: [ex]
    sant = (Formula ex -> ex) -> [Formula ex] -> [ex]
    forall a b. (a -> b) -> [a] -> [b]
    map Formula ex -> ex
    forall ex. Formula ex -> ex
    formExpr ([Formula ex] -> [ex]) -> [Formula ex] -> [ex]
    forall a b. (a -> b) -> a -> b
    $ Step ex -> [Formula ex]
    forall ex. Step ex -> [Formula ex]
    stepAnt Step ex
    step
            --  Consequentent expression from proof step:
            scon :: ex
    scon = Formula ex -> ex
    forall ex. Formula ex -> ex
    formExpr (Formula ex -> ex) -> Formula ex -> ex
    forall a b. (a -> b) -> a -> b
    $ Step ex -> Formula ex
    forall ex. Step ex -> Formula ex
    stepCon Step ex
    step
            --  Tests for step to be valid
            errors :: [String]
    errors = [Maybe String] -> [String]
    forall a. [Maybe a] -> [a]
    catMaybes
                -- Rule name is one of supplied rules, and
                [ Bool -> String -> Maybe String
    forall {a}. Bool -> a -> Maybe a
    require (Rule ex -> ScopedName
    forall ex. Rule ex -> ScopedName
    ruleName Rule ex
    srul ScopedName -> [ScopedName] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` (Rule ex -> ScopedName) -> [Rule ex] -> [ScopedName]
    forall a b. (a -> b) -> [a] -> [b]
    map Rule ex -> ScopedName
    forall ex. Rule ex -> ScopedName
    ruleName [Rule ex]
    rules)
                          (String
    "rule " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ScopedName -> String
    forall a. Show a => a -> String
    show (Rule ex -> ScopedName
    forall ex. Rule ex -> ScopedName
    ruleName Rule ex
    srul) String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " not present")
                -- Antecedent expressions are all previously accepted expressions
                , Bool -> String -> Maybe String
    forall {a}. Bool -> a -> Maybe a
    require ([ex] -> Set ex
    forall a. Ord a => [a] -> Set a
    S.fromList [ex]
    sant Set ex -> Set ex -> Bool
    forall a. Ord a => Set a -> Set a -> Bool
    `S.isSubsetOf` [ex] -> Set ex
    forall a. Ord a => [a] -> Set a
    S.fromList [ex]
    prev) -- (sant `subset` prev)
                          String
    "antecedent not axiom or previous result"
                -- Inference rule yields consequence from antecedents
                , Bool -> String -> Maybe String
    forall {a}. Bool -> a -> Maybe a
    require (Rule ex -> [ex] -> ex -> Bool
    forall ex. Rule ex -> [ex] -> ex -> Bool
    checkInference Rule ex
    srul [ex]
    sant ex
    scon)
                          String
    "rule does not deduce consequence from antecedents"
                ]
            require :: Bool -> a -> Maybe a
    require Bool
    b a
    s = if Bool
    b then Maybe a
    forall a. Maybe a
    Nothing else a -> Maybe a
    forall a. a -> Maybe a
    Just a
    s

    -- |Create a displayable form of a proof, returned as a `ShowS` value.
    --
    --  This function is intended to allow the calling function some control
    --  of multiline displays by providing:
    --
    --  (1) the first line of the proof is not preceded by any text, so
    --      it may be appended to some preceding text on the same line,
    --
    --  (2) the supplied newline string is used to separate lines of the
    --      formatted text, and may include any desired indentation, and
    --
    --  (3) no newline is output following the final line of text.
    showsProof ::
      (ShowLines ex)
      => String    -- ^ newline string
      -> Proof ex
      -> ShowS
    showsProof :: forall ex. ShowLines ex => String -> Proof ex -> ShowS
    showsProof String
    newline Proof ex
    proof =
        if [Formula ex] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Formula ex]
    axioms then ShowS
    shProof else ShowS
    shAxioms ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ShowS
    shProof
        where
            axioms :: [Formula ex]
    axioms = Proof ex -> [Formula ex]
    forall a. Proof a -> [Formula a]
    proofAxiomsUsed Proof ex
    proof
            shAxioms :: ShowS
    shAxioms =
                String -> ShowS
    showString    (String
    "Axioms:" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    newline) ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .
                String -> [Formula ex] -> String -> ShowS
    forall ex.
    ShowLines ex =>
    String -> [Formula ex] -> String -> ShowS
    showsFormulae String
    newline (Proof ex -> [Formula ex]
    forall a. Proof a -> [Formula a]
    proofAxiomsUsed Proof ex
    proof) String
    newline
            shProof :: ShowS
    shProof =
                String -> ShowS
    showString    (String
    "Input:" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    newline) ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .
                String -> Formula ex -> ShowS
    forall ex. ShowLines ex => String -> Formula ex -> ShowS
    showsFormula  String
    newline (Proof ex -> Formula ex
    forall ex. Proof ex -> Formula ex
    proofInput  Proof ex
    proof) ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .
                String -> ShowS
    showString    (String
    newline String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    "Proof:" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    newline) ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .
                String -> [Step ex] -> ShowS
    forall ex. ShowLines ex => String -> [Step ex] -> ShowS
    showsSteps    String
    newline (Proof ex -> [Step ex]
    forall ex. Proof ex -> [Step ex]
    proofChain  Proof ex
    proof)

    -- |Returns a simple string representation of a proof.
    showProof ::
      (ShowLines ex)
      => String    -- ^ newline string
      -> Proof ex
      -> String
    showProof :: forall ex. ShowLines ex => String -> Proof ex -> String
    showProof String
    newline Proof ex
    proof = String -> Proof ex -> ShowS
    forall ex. ShowLines ex => String -> Proof ex -> ShowS
    showsProof String
    newline Proof ex
    proof String
    ""

    -- |Create a displayable form of a list of labelled proof steps
    showsSteps :: (ShowLines ex) => String -> [Step ex] -> ShowS
    showsSteps :: forall ex. ShowLines ex => String -> [Step ex] -> ShowS
    showsSteps String
    _       []     = ShowS
    forall a. a -> a
    id
    showsSteps String
    newline [Step ex
    s]    = String -> Step ex -> ShowS
    forall ex. ShowLines ex => String -> Step ex -> ShowS
    showsStep  String
    newline Step ex
    s
    showsSteps String
    newline (Step ex
    s:[Step ex]
    ss) = String -> Step ex -> ShowS
    forall ex. ShowLines ex => String -> Step ex -> ShowS
    showsStep  String
    newline Step ex
    s ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .
                                String -> ShowS
    showString String
    newline ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .
                                String -> [Step ex] -> ShowS
    forall ex. ShowLines ex => String -> [Step ex] -> ShowS
    showsSteps String
    newline [Step ex]
    ss

    -- |Create a displayable form of a labelled proof step.
    showsStep :: (ShowLines ex) => String -> Step ex -> ShowS
    showsStep :: forall ex. ShowLines ex => String -> Step ex -> ShowS
    showsStep String
    newline Step ex
    s = String -> Formula ex -> ShowS
    forall ex. ShowLines ex => String -> Formula ex -> ShowS
    showsFormula String
    newline (Step ex -> Formula ex
    forall ex. Step ex -> Formula ex
    stepCon Step ex
    s) ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .
                          String -> ShowS
    showString String
    newline ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .
                          String -> ShowS
    showString (String
    "  (by [" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    rulename String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    "] from " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    antnames String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ")")
        where
            rulename :: String
    rulename = ScopedName -> String
    forall a. Show a => a -> String
    show (ScopedName -> String)
    -> (Rule ex -> ScopedName) -> Rule ex -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Rule ex -> ScopedName
    forall ex. Rule ex -> ScopedName
    ruleName (Rule ex -> String) -> Rule ex -> String
    forall a b. (a -> b) -> a -> b
    $ Step ex -> Rule ex
    forall ex. Step ex -> Rule ex
    stepRule Step ex
    s
            antnames :: String
    antnames = [String] -> String
    showNames ([String] -> String) -> [String] -> String
    forall a b. (a -> b) -> a -> b
    $ (Formula ex -> String) -> [Formula ex] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (ScopedName -> String
    forall a. Show a => a -> String
    show (ScopedName -> String)
    -> (Formula ex -> ScopedName) -> Formula ex -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Formula ex -> ScopedName
    forall ex. Formula ex -> ScopedName
    formName) (Step ex -> [Formula ex]
    forall ex. Step ex -> [Formula ex]
    stepAnt Step ex
    s)

    -- |Return a string containing a list of names.
    showNames :: [String] -> String
    showNames :: [String] -> String
    showNames []      = String
    "<nothing>"
    showNames [String
    n]     = ShowS
    showName String
    n
    showNames [String
    n1,String
    n2] = ShowS
    showName String
    n1 String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " and " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    showName String
    n2
    showNames (String
    n1:[String]
    ns) = ShowS
    showName String
    n1 String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ", " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    showNames [String]
    ns

    -- |Return a string representing a single name.
    showName :: String -> String
    showName :: ShowS
    showName String
    n = String
    "[" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    n String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    "]"

    --------------------------------------------------------------------------------
    --
    --  Copyright (c) 2003, Graham Klyne, 2009 Vasili I Galchin, 2011, 2016, 2022 Douglas Burke
    --  All rights reserved.
    --
    --  This file is part of Swish.
    --
    --  Swish is free software; you can redistribute it and/or modify
    --  it under the terms of the GNU General Public License as published by
    --  the Free Software Foundation; either version 2 of the License, or
    --  (at your option) any later version.
    --
    --  Swish is distributed in the hope that it will be useful,
    --  but WITHOUT ANY WARRANTY; without even the implied warranty of
    --  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
    --  GNU General Public License for more details.
    --
    --  You should have received a copy of the GNU General Public License
    --  along with Swish; if not, write to:
    --    The Free Software Foundation, Inc.,
    --    59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
    --
    --------------------------------------------------------------------------------