{-# 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 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 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
    { 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
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
showList :: [Step ex] -> ShowS
$cshowList :: forall ex. Show ex => [Step ex] -> ShowS
show :: Step ex -> String
$cshow :: forall ex. Show ex => Step ex -> String
showsPrec :: Int -> Step ex -> ShowS
$cshowsPrec :: forall ex. Show ex => Int -> 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 = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall ex. Ruleset ex -> [Formula ex]
rsAxioms forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall ex. Ruleset ex -> [Rule ex]
rsRules forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' forall a. Eq a => [a] -> [a] -> [a]
union [] forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Step ex -> [Formula ex]
stepAxioms (forall ex. Proof ex -> [Step ex]
proofChain Proof ex
proof)
    where
        stepAxioms :: Step ex -> [Formula ex]
stepAxioms Step ex
st = forall ex. Step ex -> [Formula ex]
stepAnt Step ex
st forall a. Eq a => [a] -> [a] -> [a]
`intersect` 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 =
    forall ex.
(Expression ex, Ord ex) =>
[Rule ex] -> [ex] -> [Step ex] -> ex -> Bool
checkProof1 (forall a. Proof a -> [Rule a]
proofRules Proof ex
pr) [ex]
initExpr (forall ex. Proof ex -> [Step ex]
proofChain Proof ex
pr) ex
goalExpr
    where
        initExpr :: [ex]
initExpr = forall ex. Formula ex -> ex
formExpr (forall ex. Proof ex -> Formula ex
proofInput Proof ex
pr) forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map forall ex. Formula ex -> ex
formExpr (forall a. Proof a -> [Formula a]
proofAxioms Proof ex
pr)
        goalExpr :: ex
goalExpr = forall ex. Formula ex -> ex
formExpr forall a b. (a -> b) -> a -> b
$ 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 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 =
    forall ex. Ord ex => [Rule ex] -> [ex] -> Step ex -> Bool
checkStep [Rule ex]
rules [ex]
prev Step ex
st Bool -> Bool -> Bool
&&
    forall ex.
(Expression ex, Ord ex) =>
[Rule ex] -> [ex] -> [Step ex] -> ex -> Bool
checkProof1 [Rule ex]
rules (forall ex. Formula ex -> ex
formExpr (forall ex. Step ex -> Formula ex
stepCon Step ex
st)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 = forall a. Maybe a -> Bool
isNothing forall a b. (a -> b) -> a -> b
$ 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 =
    forall ex.
(Expression ex, Ord ex) =>
[Rule ex] -> [ex] -> [Step ex] -> ex -> Maybe String
explainProof1 (forall a. Proof a -> [Rule a]
proofRules Proof ex
pr) [ex]
initExpr (forall ex. Proof ex -> [Step ex]
proofChain Proof ex
pr) ex
goalExpr
    where
        initExpr :: [ex]
initExpr = forall ex. Formula ex -> ex
formExpr (forall ex. Proof ex -> Formula ex
proofInput Proof ex
pr) forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map forall ex. Formula ex -> ex
formExpr (forall a. Proof a -> [Formula a]
proofAxioms Proof ex
pr)
        goalExpr :: ex
goalExpr = forall ex. Formula ex -> ex
formExpr forall a b. (a -> b) -> a -> b
$ 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 forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [ex]
prev then forall a. Maybe a
Nothing else 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 forall ex. Ord ex => [Rule ex] -> [ex] -> Step ex -> Maybe String
explainStep [Rule ex]
rules [ex]
prev Step ex
st  of
        Maybe String
Nothing -> forall ex.
(Expression ex, Ord ex) =>
[Rule ex] -> [ex] -> [Step ex] -> ex -> Maybe String
explainProof1 [Rule ex]
rules (forall ex. Formula ex -> ex
formExpr (forall ex. Step ex -> Formula ex
stepCon Step ex
st)forall a. a -> [a] -> [a]
:[ex]
prev) [Step ex]
steps ex
res
        Just String
ex -> forall a. a -> Maybe a
Just (String
"Invalid step: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall ex. Formula ex -> ScopedName
formName forall a b. (a -> b) -> a -> b
$ forall ex. Step ex -> Formula ex
stepCon Step ex
st) forall a. [a] -> [a] -> [a]
++ String
": " 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 forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
errors then forall a. Maybe a
Nothing else forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [[a]] -> [a]
intercalate String
", " [String]
errors
    where
        --  Rule from proof step:
        srul :: Rule ex
srul = forall ex. Step ex -> Rule ex
stepRule Step ex
step
        --  Antecedent expressions from proof step:
        sant :: [ex]
sant = forall a b. (a -> b) -> [a] -> [b]
map forall ex. Formula ex -> ex
formExpr forall a b. (a -> b) -> a -> b
$ forall ex. Step ex -> [Formula ex]
stepAnt Step ex
step
        --  Consequentent expression from proof step:
        scon :: ex
scon = forall ex. Formula ex -> ex
formExpr forall a b. (a -> b) -> a -> b
$ forall ex. Step ex -> Formula ex
stepCon Step ex
step
        --  Tests for step to be valid
        errors :: [String]
errors = forall a. [Maybe a] -> [a]
catMaybes
            -- Rule name is one of supplied rules, and
            [ forall {a}. Bool -> a -> Maybe a
require (forall ex. Rule ex -> ScopedName
ruleName Rule ex
srul forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` forall a b. (a -> b) -> [a] -> [b]
map forall ex. Rule ex -> ScopedName
ruleName [Rule ex]
rules)
                      (String
"rule " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall ex. Rule ex -> ScopedName
ruleName Rule ex
srul) forall a. [a] -> [a] -> [a]
++ String
" not present")
            -- Antecedent expressions are all previously accepted expressions
            , forall {a}. Bool -> a -> Maybe a
require (forall a. Ord a => [a] -> Set a
S.fromList [ex]
sant forall a. Ord a => Set a -> Set a -> Bool
`S.isSubsetOf` 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
            , forall {a}. Bool -> a -> Maybe a
require (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 forall a. Maybe a
Nothing else 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 forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Formula ex]
axioms then ShowS
shProof else ShowS
shAxioms forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
shProof
    where
        axioms :: [Formula ex]
axioms = forall a. Proof a -> [Formula a]
proofAxiomsUsed Proof ex
proof
        shAxioms :: ShowS
shAxioms =
            String -> ShowS
showString    (String
"Axioms:" forall a. [a] -> [a] -> [a]
++ String
newline) forall b c a. (b -> c) -> (a -> b) -> a -> c
.
            forall ex.
ShowLines ex =>
String -> [Formula ex] -> String -> ShowS
showsFormulae String
newline (forall a. Proof a -> [Formula a]
proofAxiomsUsed Proof ex
proof) String
newline
        shProof :: ShowS
shProof =
            String -> ShowS
showString    (String
"Input:" forall a. [a] -> [a] -> [a]
++ String
newline) forall b c a. (b -> c) -> (a -> b) -> a -> c
.
            forall ex. ShowLines ex => String -> Formula ex -> ShowS
showsFormula  String
newline (forall ex. Proof ex -> Formula ex
proofInput  Proof ex
proof) forall b c a. (b -> c) -> (a -> b) -> a -> c
.
            String -> ShowS
showString    (String
newline forall a. [a] -> [a] -> [a]
++ String
"Proof:" forall a. [a] -> [a] -> [a]
++ String
newline) forall b c a. (b -> c) -> (a -> b) -> a -> c
.
            forall ex. ShowLines ex => String -> [Step ex] -> ShowS
showsSteps    String
newline (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 = 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
_       []     = forall a. a -> a
id
showsSteps String
newline [Step ex
s]    = forall ex. ShowLines ex => String -> Step ex -> ShowS
showsStep  String
newline Step ex
s
showsSteps String
newline (Step ex
s:[Step ex]
ss) = forall ex. ShowLines ex => String -> Step ex -> ShowS
showsStep  String
newline Step ex
s forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                            String -> ShowS
showString String
newline forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                            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 = forall ex. ShowLines ex => String -> Formula ex -> ShowS
showsFormula String
newline (forall ex. Step ex -> Formula ex
stepCon Step ex
s) forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                      String -> ShowS
showString String
newline forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                      String -> ShowS
showString (String
"  (by [" forall a. [a] -> [a] -> [a]
++ String
rulename forall a. [a] -> [a] -> [a]
++ String
"] from " forall a. [a] -> [a] -> [a]
++ String
antnames forall a. [a] -> [a] -> [a]
++ String
")")
    where
        rulename :: String
rulename = forall a. Show a => a -> String
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ex. Rule ex -> ScopedName
ruleName forall a b. (a -> b) -> a -> b
$ forall ex. Step ex -> Rule ex
stepRule Step ex
s
        antnames :: String
antnames = [String] -> String
showNames forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a. Show a => a -> String
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ex. Formula ex -> ScopedName
formName) (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 forall a. [a] -> [a] -> [a]
++ String
" and " forall a. [a] -> [a] -> [a]
++ ShowS
showName String
n2
showNames (String
n1:[String]
ns) = ShowS
showName String
n1 forall a. [a] -> [a] -> [a]
++ String
", " 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
"[" forall a. [a] -> [a] -> [a]
++ String
n 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
--
--------------------------------------------------------------------------------