{-# 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
--
--------------------------------------------------------------------------------