    --------------------------------------------------------------------------------
    --  See end of this file for licence information.
    --------------------------------------------------------------------------------
    -- |
    --  Module      :  Proof
    --  Copyright   :  (c) 2003, Graham Klyne, 2009 Vasili I Galchin, 2011 Douglas Burke
    --  License     :  GPL V2
    --
    --  Maintainer  :  Douglas Burke
    --  Stability   :  experimental
    --  Portability :  H98
    --
    --  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 Swish.Rule (Expression(..), Formula(..), Rule(..))
    import Swish.Rule (showsFormula, showsFormulae)
    import Swish.Ruleset (Ruleset(..))

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

    import qualified Data.Set as S

    ------------------------------------------------------------
    --  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
        { stepRule :: Rule ex           -- ^ Inference rule used
        , stepAnt  :: [Formula ex]      -- ^ Antecedents of inference rule
        , stepCon  :: Formula ex        -- ^ Named consequence of inference rule
        } deriving 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
        { proofContext :: [Ruleset ex]  -- ^ Proof context:  list of rulesets,
                                        --   each of which provides a number of
                                        --   axioms and rules.
        , proofInput   :: Formula ex    -- ^ Given expression
        , proofResult  :: Formula ex    -- ^ Result expression
        , 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 = concatMap rsAxioms . proofContext

    -- |Return a list of rules from all the rulesets in a proof
    proofRules :: Proof a -> [Rule a]
    proofRules = concatMap rsRules . proofContext

    -- |Return list of axioms actually referenced by a proof
    proofAxiomsUsed :: Proof ex -> [Formula ex]
    proofAxiomsUsed proof = foldl' union [] $ map stepAxioms (proofChain proof)
        where
            stepAxioms st = stepAnt st `intersect` proofAxioms 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 pr =
        checkProof1 (proofRules pr) initExpr (proofChain pr) goalExpr
        where
            initExpr = formExpr (proofInput pr) : map formExpr (proofAxioms pr)
            goalExpr = formExpr $ proofResult pr

    checkProof1 ::
        (Expression ex, Ord ex)
        => [Rule ex] -> [ex] -> [Step ex] -> ex -> Bool
    checkProof1 _     prev []       res = res `elem` prev
    checkProof1 rules prev (st:steps) res =
        checkStep rules prev st &&
        checkProof1 rules (formExpr (stepCon st):prev) steps 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 ::
      (Expression ex, Ord ex)
      => [Rule ex]   -- ^ rules
      -> [ex]        -- ^ antecedants
      -> Step ex     -- ^ the step to validate
      -> Bool        -- ^ @True@ if the step is valid

    checkStep rules prev step = isNothing $ explainStep rules prev 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 pr =
        explainProof1 (proofRules pr) initExpr (proofChain pr) goalExpr
        where
            initExpr = formExpr (proofInput pr) : map formExpr (proofAxioms pr)
            goalExpr = formExpr $ proofResult pr

    explainProof1 ::
        (Expression ex, Ord ex)
        => [Rule ex] -> [ex] -> [Step ex] -> ex -> Maybe String
    explainProof1 _     prev []       res   =
        if res `elem` prev then Nothing else Just "Result not demonstrated"
    explainProof1 rules prev (st:steps) res =
        case explainStep rules prev st  of
            Nothing -> explainProof1 rules (formExpr (stepCon st):prev) steps res
            Just ex -> Just ("Invalid step: "++show (formName $ stepCon st)++": "++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 ::
      (Expression ex, Ord ex)
      => [Rule ex]  -- ^ rules
      -> [ex]       -- ^ previous
      -> Step ex    -- ^ step
      -> Maybe String -- ^ @Nothing@ if step is okay, otherwise a string indicating the error
    explainStep rules prev step =
            if null errors then Nothing else Just $ intercalate ", " errors
        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
            --  Tests for step to be valid
            errors = catMaybes
                -- Rule name is one of supplied rules, and
                [ require (ruleName srul `elem` map ruleName rules)
                          ("rule "++show (ruleName srul)++" not present")
                -- Antecedent expressions are all previously accepted expressions
                , require (S.fromList sant `S.isSubsetOf` S.fromList prev) -- (sant `subset` prev)
                          "antecedent not axiom or previous result"
                -- Inference rule yields consequence from antecedents
                , require (checkInference srul sant scon)
                          "rule does not deduce consequence from antecedents"
                ]
            require b s = if b then Nothing else Just 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 newline proof =
        if null axioms then shProof else shAxioms . shProof
        where
            axioms = proofAxiomsUsed proof
            shAxioms =
                showString    ("Axioms:" ++ newline) .
                showsFormulae newline (proofAxiomsUsed proof) newline
            shProof =
                showString    ("Input:" ++ newline) .
                showsFormula  newline (proofInput  proof) .
                showString    (newline ++ "Proof:" ++ newline) .
                showsSteps    newline (proofChain  proof)

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

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

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

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

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

    --------------------------------------------------------------------------------
    --
    --  Copyright (c) 2003, Graham Klyne, 2009 Vasili I Galchin, 2011 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
    --
    --------------------------------------------------------------------------------