{-# LANGUAGE CPP #-}
{-# LANGUAGE OverloadedStrings #-}

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

--------------------------------------------------------------------------------
--  See end of this file for licence information.
--------------------------------------------------------------------------------
-- |
--  Module      :  Rule
--  Copyright   :  (c) 2003, Graham Klyne, 2009 Vasili I Galchin, 2011, 2012, 2022 Douglas Burke
--  License     :  GPL V2
--
--  Maintainer  :  Douglas Burke
--  Stability   :  experimental
--  Portability :  CPP, DerivingStrategies, OverloadedStrings
--
--  This module defines a framework for defining inference rules
--  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.
--
--------------------------------------------------------------------------------

module Swish.Rule
       ( Expression(..), Formula(..), Rule(..), RuleMap
       , nullScope, nullSN, nullFormula, nullRule
       , fwdCheckInference, bwdCheckInference
       , showsFormula, showsFormulae, showsWidth
       )
       where

import Swish.Namespace (Namespace, ScopedName)
import Swish.Namespace (makeNamespace, makeNSScopedName)
import Swish.QName (LName)

import Data.Maybe (fromJust)
import Data.String.ShowLines (ShowLines(..))

import Network.URI (URI, parseURI)

import qualified Data.Map as M

------------------------------------------------------------
--  Expressions
------------------------------------------------------------

-- |Expression is a type class for values over which proofs
--  may be constructed.
class (Eq ex) => Expression ex where
    -- |Is expression true in all interpretations?
    --  If so, then its truth is assumed without justification.
    isValid :: ex -> Bool

------------------------------------------------------------
--  Formula:  a named expression
------------------------------------------------------------

-- | A Formula is a named expression.
data Formula ex = Formula
    { forall ex. Formula ex -> ScopedName
formName :: ScopedName        -- ^ Name used for formula in proof chain
    , forall ex. Formula ex -> ex
formExpr :: ex                -- ^ Named formula value
    } deriving
#if (__GLASGOW_HASKELL__ >= 802)
    stock
#endif
    Int -> Formula ex -> ShowS
[Formula ex] -> ShowS
Formula ex -> String
(Int -> Formula ex -> ShowS)
-> (Formula ex -> String)
-> ([Formula ex] -> ShowS)
-> Show (Formula ex)
forall ex. Show ex => Int -> Formula ex -> ShowS
forall ex. Show ex => [Formula ex] -> ShowS
forall ex. Show ex => Formula ex -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall ex. Show ex => Int -> Formula ex -> ShowS
showsPrec :: Int -> Formula ex -> ShowS
$cshow :: forall ex. Show ex => Formula ex -> String
show :: Formula ex -> String
$cshowList :: forall ex. Show ex => [Formula ex] -> ShowS
showList :: [Formula ex] -> ShowS
Show

-- |Define equality of formulae as equality of formula names
instance Eq (Formula ex) where
    Formula ex
f1 == :: Formula ex -> Formula ex -> Bool
== Formula ex
f2 = Formula ex -> ScopedName
forall ex. Formula ex -> ScopedName
formName Formula ex
f1 ScopedName -> ScopedName -> Bool
forall a. Eq a => a -> a -> Bool
== Formula ex -> ScopedName
forall ex. Formula ex -> ScopedName
formName Formula ex
f2

-- |Define ordering of formulae based on formula names
instance Ord (Formula ex) where
    Formula ex
f1 <= :: Formula ex -> Formula ex -> Bool
<= Formula ex
f2 = Formula ex -> ScopedName
forall ex. Formula ex -> ScopedName
formName Formula ex
f1 ScopedName -> ScopedName -> Bool
forall a. Ord a => a -> a -> Bool
<= Formula ex -> ScopedName
forall ex. Formula ex -> ScopedName
formName Formula ex
f2

-- | The namespace @http:\/\/id.ninebynine.org\/2003\/Ruleset\/null@ with the prefix @null:@.
nullScope :: Namespace
nullScope :: Namespace
nullScope = Maybe Text -> URI -> Namespace
makeNamespace (Text -> Maybe Text
forall a. a -> Maybe a
Just Text
"null") URI
nullScopeURI

-- | Create a scoped name with the null namespace.
nullSN :: 
  LName -- ^ local name.
  -> ScopedName
nullSN :: LName -> ScopedName
nullSN = Namespace -> LName -> ScopedName
makeNSScopedName Namespace
nullScope

tU :: String -> URI
tU :: String -> URI
tU = Maybe URI -> URI
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe URI -> URI) -> (String -> Maybe URI) -> String -> URI
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Maybe URI
parseURI

nullScopeURI :: URI
nullScopeURI :: URI
nullScopeURI = String -> URI
tU String
"http://id.ninebynine.org/2003/Ruleset/null"

-- | The null formula.
nullFormula :: Formula ex
nullFormula :: forall ex. Formula ex
nullFormula = Formula
    { formName :: ScopedName
formName = Namespace -> LName -> ScopedName
makeNSScopedName Namespace
nullScope LName
"nullFormula"
    , formExpr :: ex
formExpr = String -> ex
forall a. HasCallStack => String -> a
error String
"Null formula"
    }

-- testf1 = Formula "f1" ('f',1)
-- testf2 = Formula "f2" ('f',2)

-- |Return a displayable form of a list of labelled formulae
showsFormulae :: 
  (ShowLines ex) 
  => String        -- ^ newline
  -> [Formula ex]  -- ^ the formulae to show
  -> String        -- ^ text to be placed after the formulae
  -> ShowS
showsFormulae :: forall ex.
ShowLines ex =>
String -> [Formula ex] -> String -> ShowS
showsFormulae String
_       []     String
_     = ShowS
forall a. a -> a
id
showsFormulae String
newline [Formula ex
f]    String
after = String -> Formula ex -> ShowS
forall ex. ShowLines ex => String -> Formula ex -> ShowS
showsFormula  String
newline Formula ex
f ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                                     String -> ShowS
showString    String
after
showsFormulae String
newline (Formula ex
f:[Formula ex]
fs) String
after = String -> Formula ex -> ShowS
forall ex. ShowLines ex => String -> Formula ex -> ShowS
showsFormula  String
newline Formula ex
f 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 -> [Formula ex] -> String -> ShowS
forall ex.
ShowLines ex =>
String -> [Formula ex] -> String -> ShowS
showsFormulae String
newline [Formula ex]
fs String
after

-- |Create a displayable form of a labelled formula
showsFormula :: 
  (ShowLines ex) 
  => String      -- ^ newline
  -> Formula ex  -- ^ formula
  -> ShowS
showsFormula :: forall ex. ShowLines ex => String -> Formula ex -> ShowS
showsFormula String
newline Formula ex
f =
    Int -> String -> ShowS
showsWidth Int
16 (String
"[" 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
f) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"] ") ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    String -> ex -> ShowS
forall sh. ShowLines sh => String -> sh -> ShowS
showls (String
newline String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
16 Char
' ') (Formula ex -> ex
forall ex. Formula ex -> ex
formExpr Formula ex
f)

------------------------------------------------------------
--  Rule
------------------------------------------------------------

-- |Rule is a data type for inference rules that can be used
--  to construct a step in a proof.
data Rule ex = Rule
    {
      -- |Name of rule, for use when displaying a proof
      forall ex. Rule ex -> ScopedName
ruleName :: ScopedName,
      
      -- |Forward application of a rule, takes a list of
      --  expressions and returns a list (possibly empty)
      --  of forward applications of the rule to combinations
      --  of the antecedent expressions.
      --  Note that all of the results returned can be assumed to
      --  be (simultaneously) true, given the antecedents provided.
      forall ex. Rule ex -> [ex] -> [ex]
fwdApply :: [ex] -> [ex],
      
      -- |Backward application of a rule, takes an expression
      --  and returns a list of alternative antecedents, each of
      --  which is a list of expressions that jointly yield the
      --  given consequence through application of the inference
      --  rule.  An empty list is returned if no antecedents
      --  will allow the consequence to be inferred.
      forall ex. Rule ex -> ex -> [[ex]]
bwdApply :: ex -> [[ex]],
      
      -- |Inference check.  Takes a list of antecedent expressions
      --  and a consequent expression, returning True if the
      --  consequence can be obtained from the antecedents by
      --  application of the rule.  When the antecedents and
      --  consequent are both given, this is generally more efficient
      --  that using either forward or backward chaining.
      --  Also, a particular rule may not fully support either
      --  forward or backward chaining, but all rules are required
      --  to fully support this function.
      --
      --  A default implementation based on forward chaining is
      --  given below.
      forall ex. Rule ex -> [ex] -> ex -> Bool
checkInference :: [ex] -> ex -> Bool 
    }

-- |Define equality of rules as equality of the rule names.
instance Eq (Rule ex) where
    Rule ex
r1 == :: Rule ex -> Rule ex -> Bool
== Rule ex
r2 = Rule ex -> ScopedName
forall ex. Rule ex -> ScopedName
ruleName Rule ex
r1 ScopedName -> ScopedName -> Bool
forall a. Eq a => a -> a -> Bool
== Rule ex -> ScopedName
forall ex. Rule ex -> ScopedName
ruleName Rule ex
r2

-- |Define ordering of rules based on the rule names.
instance Ord (Rule ex) where
    Rule ex
r1 <= :: Rule ex -> Rule ex -> Bool
<= Rule ex
r2 = Rule ex -> ScopedName
forall ex. Rule ex -> ScopedName
ruleName Rule ex
r1 ScopedName -> ScopedName -> Bool
forall a. Ord a => a -> a -> Bool
<= Rule ex -> ScopedName
forall ex. Rule ex -> ScopedName
ruleName Rule ex
r2

instance Show (Rule ex) where
    show :: Rule ex -> String
show Rule ex
rl = 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
rl)

-- | A set of rules labelled with their name.
type RuleMap ex = M.Map ScopedName (Rule ex)

-- | Checks that consequence is a result of
-- applying the rule to the antecedants.
fwdCheckInference :: 
  (Eq ex) 
  => Rule ex   -- ^ rule
  -> [ex]      -- ^ antecedants
  -> ex        -- ^ consequence
  -> Bool
fwdCheckInference :: forall ex. Eq ex => Rule ex -> [ex] -> ex -> Bool
fwdCheckInference Rule ex
rule [ex]
ante ex
cons =
    ex
cons ex -> [ex] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Rule ex -> [ex] -> [ex]
forall ex. Rule ex -> [ex] -> [ex]
fwdApply Rule ex
rule [ex]
ante

-- | Checks that the antecedants are all required
-- to create the consequence using the given rule.
bwdCheckInference ::
  (Eq ex) 
  => Rule ex   -- ^ rule
  -> [ex]      -- ^ antecedants
  -> ex        -- ^ consequence
  -> Bool
bwdCheckInference :: forall ex. Eq ex => Rule ex -> [ex] -> ex -> Bool
bwdCheckInference Rule ex
rule [ex]
ante ex
cons = ([ex] -> Bool) -> [[ex]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any [ex] -> Bool
checkAnts (Rule ex -> ex -> [[ex]]
forall ex. Rule ex -> ex -> [[ex]]
bwdApply Rule ex
rule ex
cons)
    where
        checkAnts :: [ex] -> Bool
checkAnts = (ex -> Bool) -> [ex] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (ex -> [ex] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [ex]
ante)

-- | The null rule.
nullRule :: Rule ex
nullRule :: forall ex. Rule ex
nullRule = Rule
    { ruleName :: ScopedName
ruleName = Namespace -> LName -> ScopedName
makeNSScopedName Namespace
nullScope LName
"nullRule"
    , fwdApply :: [ex] -> [ex]
fwdApply = [ex] -> [ex] -> [ex]
forall a b. a -> b -> a
const []
    , bwdApply :: ex -> [[ex]]
bwdApply = [[ex]] -> ex -> [[ex]]
forall a b. a -> b -> a
const []
    , checkInference :: [ex] -> ex -> Bool
checkInference = \ [ex]
_ ex
_ -> Bool
False
    }

------------------------------------------------------------
--  Shows formatting support functions
-----------------------------------------------------------

-- |Show a string left justified in a field of at least the specified
--  number of characters width.
showsWidth :: Int -> String -> ShowS
showsWidth :: Int -> String -> ShowS
showsWidth Int
wid String
str String
more = String
str String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
pad Char
' ' String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
more
    where
        pad :: Int
pad = Int
wid Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
str


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