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