--------------------------------------------------------------------------------
--  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.RDF.Proof
    ( Proof(..), Step(..)
    , checkProof, explainProof, checkStep, showProof, showsProof, showsFormula )
where

import Swish.RDF.Ruleset (Ruleset(..))

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

import Swish.Utils.ShowM (ShowM(..))

import Swish.Utils.ListHelpers (subset)

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

------------------------------------------------------------
--  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) => 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) => [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) 
  => [Rule ex]   -- ^ rules
  -> [ex]        -- ^ a ntecedants
  -> 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) => 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) => [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) 
  => [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 (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 :: 
  (ShowM 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 :: 
  (ShowM 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 :: (ShowM 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 :: (ShowM 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
--
--------------------------------------------------------------------------------