--------------------------------------------------------------------------------
--  See end of this file for licence information.
--------------------------------------------------------------------------------
-- |
--  Module      :  Ruleset
--  Copyright   :  (c) 2003, Graham Klyne, 2009 Vasili I Galchin, 2011, 2012 Douglas Burke
--  License     :  GPL V2
--
--  Maintainer  :  Douglas Burke
--  Stability   :  experimental
--  Portability :  H98
--
--  This module defines a ruleset data type, used to collect information
--  about a ruleset that may contribute torwards inferences in RDF;
--  e.g. RDF and RDFS are rulesets.
--
--  A 'Ruleset' consists of a namespace, a collection of axioms, and
--  a collection of rules.
--
--------------------------------------------------------------------------------

module Swish.Ruleset
    ( Ruleset(..), RulesetMap
    , makeRuleset, getRulesetNamespace, getRulesetAxioms, getRulesetRules
    , getRulesetAxiom, getRulesetRule
    , getContextAxiom, getMaybeContextAxiom
    , getContextRule,  getMaybeContextRule
    )
where

import Swish.Namespace (Namespace, ScopedName)
import Swish.Rule (Formula(..), Rule(..))

{-
Used for the Show instance of Ruleset, which was
used for debugging but has been removed as not
really needed by the general user.

import Swish.Utils.ShowM (ShowM(..))
import Data.List (intercalate)
-}

import Data.Maybe (fromMaybe, listToMaybe, mapMaybe)

import qualified Data.Map as M

-- | A Rule set.

data Ruleset ex = Ruleset
    { forall ex. Ruleset ex -> Namespace
rsNamespace :: Namespace    -- ^ Namespace.
    , forall ex. Ruleset ex -> [Formula ex]
rsAxioms    :: [Formula ex] -- ^ Axioms.
    , forall ex. Ruleset ex -> [Rule ex]
rsRules     :: [Rule ex]    -- ^ Rules.
    }

{-

Used for debugging.

instance (ShowM ex) => Show (Ruleset ex) where
  show (Ruleset ns axs rls) = 
    intercalate "\n" 
    [ "Ruleset: " ++ show ns
    , "Axioms:" ]
    ++ (showsFormulae "\n" axs 
       (intercalate "\n" ("Rules:" : map show rls))) ""
-}

-- | Ruleset comparisons are based only on their namespace components.
instance Eq (Ruleset ex) where
    Ruleset ex
r1 == :: Ruleset ex -> Ruleset ex -> Bool
== Ruleset ex
r2 = Ruleset ex -> Namespace
forall ex. Ruleset ex -> Namespace
rsNamespace Ruleset ex
r1 Namespace -> Namespace -> Bool
forall a. Eq a => a -> a -> Bool
== Ruleset ex -> Namespace
forall ex. Ruleset ex -> Namespace
rsNamespace Ruleset ex
r2

-- | A set of Rulesets labelled by their Namespace.
type RulesetMap ex = M.Map Namespace (Ruleset ex)

-- | Create a ruleset.
makeRuleset :: Namespace -> [Formula ex] -> [Rule ex] -> Ruleset ex
makeRuleset :: forall ex. Namespace -> [Formula ex] -> [Rule ex] -> Ruleset ex
makeRuleset Namespace
nsp [Formula ex]
fms [Rule ex]
rls = Ruleset
    { rsNamespace :: Namespace
rsNamespace = Namespace
nsp
    , rsAxioms :: [Formula ex]
rsAxioms    = [Formula ex]
fms
    , rsRules :: [Rule ex]
rsRules     = [Rule ex]
rls
    }

-- | Extract the namespace of a ruleset.
getRulesetNamespace :: Ruleset ex -> Namespace
getRulesetNamespace :: forall ex. Ruleset ex -> Namespace
getRulesetNamespace = Ruleset ex -> Namespace
forall ex. Ruleset ex -> Namespace
rsNamespace

-- | Extract the axioms from a ruleset.
getRulesetAxioms :: Ruleset ex -> [Formula ex]
getRulesetAxioms :: forall ex. Ruleset ex -> [Formula ex]
getRulesetAxioms = Ruleset ex -> [Formula ex]
forall ex. Ruleset ex -> [Formula ex]
rsAxioms

-- | Extract the rules from a ruleset.
getRulesetRules :: Ruleset ex -> [Rule ex]
getRulesetRules :: forall ex. Ruleset ex -> [Rule ex]
getRulesetRules = Ruleset ex -> [Rule ex]
forall ex. Ruleset ex -> [Rule ex]
rsRules

-- | Find a named axiom in a ruleset.
getRulesetAxiom :: ScopedName -> Ruleset ex -> Maybe (Formula ex)
getRulesetAxiom :: forall ex. ScopedName -> Ruleset ex -> Maybe (Formula ex)
getRulesetAxiom ScopedName
nam Ruleset ex
rset =
    ScopedName -> Map ScopedName (Formula ex) -> Maybe (Formula ex)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup ScopedName
nam (Map ScopedName (Formula ex) -> Maybe (Formula ex))
-> Map ScopedName (Formula ex) -> Maybe (Formula ex)
forall a b. (a -> b) -> a -> b
$ [(ScopedName, Formula ex)] -> Map ScopedName (Formula ex)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(ScopedName, Formula ex)] -> Map ScopedName (Formula ex))
-> [(ScopedName, Formula ex)] -> Map ScopedName (Formula ex)
forall a b. (a -> b) -> a -> b
$ (Formula ex -> (ScopedName, Formula ex))
-> [Formula ex] -> [(ScopedName, Formula ex)]
forall a b. (a -> b) -> [a] -> [b]
map (\Formula ex
f -> (Formula ex -> ScopedName
forall ex. Formula ex -> ScopedName
formName Formula ex
f, Formula ex
f)) (Ruleset ex -> [Formula ex]
forall ex. Ruleset ex -> [Formula ex]
rsAxioms Ruleset ex
rset)

-- | Find a named rule in a ruleset. 
getRulesetRule :: ScopedName -> Ruleset ex -> Maybe (Rule ex)
getRulesetRule :: forall ex. ScopedName -> Ruleset ex -> Maybe (Rule ex)
getRulesetRule ScopedName
nam Ruleset ex
rset =
    ScopedName -> Map ScopedName (Rule ex) -> Maybe (Rule ex)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup ScopedName
nam (Map ScopedName (Rule ex) -> Maybe (Rule ex))
-> Map ScopedName (Rule ex) -> Maybe (Rule ex)
forall a b. (a -> b) -> a -> b
$ [(ScopedName, Rule ex)] -> Map ScopedName (Rule ex)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(ScopedName, Rule ex)] -> Map ScopedName (Rule ex))
-> [(ScopedName, Rule ex)] -> Map ScopedName (Rule ex)
forall a b. (a -> b) -> a -> b
$ (Rule ex -> (ScopedName, Rule ex))
-> [Rule ex] -> [(ScopedName, Rule ex)]
forall a b. (a -> b) -> [a] -> [b]
map (\Rule ex
r -> (Rule ex -> ScopedName
forall ex. Rule ex -> ScopedName
ruleName Rule ex
r, Rule ex
r)) (Ruleset ex -> [Rule ex]
forall ex. Ruleset ex -> [Rule ex]
rsRules Ruleset ex
rset)

-- | Find a named axiom in a proof context.
getContextAxiom :: 
  ScopedName -- ^ Name of axiom.
  -> Formula ex -- ^ Default axiom (used if named component does not exist).
  -> [Ruleset ex] -- ^ Rulesets to search.
  -> Formula ex
getContextAxiom :: forall ex. ScopedName -> Formula ex -> [Ruleset ex] -> Formula ex
getContextAxiom ScopedName
nam Formula ex
def [Ruleset ex]
rsets = Formula ex -> Maybe (Formula ex) -> Formula ex
forall a. a -> Maybe a -> a
fromMaybe Formula ex
def (ScopedName -> [Ruleset ex] -> Maybe (Formula ex)
forall ex. ScopedName -> [Ruleset ex] -> Maybe (Formula ex)
getMaybeContextAxiom ScopedName
nam [Ruleset ex]
rsets)

-- | Find a named axiom in a proof context.
getMaybeContextAxiom ::
  ScopedName -- ^ Name of axiom.
  -> [Ruleset ex] -- ^ Rulesets to search.
  -> Maybe (Formula ex)
getMaybeContextAxiom :: forall ex. ScopedName -> [Ruleset ex] -> Maybe (Formula ex)
getMaybeContextAxiom ScopedName
nam [Ruleset ex]
rsets =
    [Formula ex] -> Maybe (Formula ex)
forall a. [a] -> Maybe a
listToMaybe ([Formula ex] -> Maybe (Formula ex))
-> [Formula ex] -> Maybe (Formula ex)
forall a b. (a -> b) -> a -> b
$ (Ruleset ex -> Maybe (Formula ex)) -> [Ruleset ex] -> [Formula ex]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (ScopedName -> Ruleset ex -> Maybe (Formula ex)
forall ex. ScopedName -> Ruleset ex -> Maybe (Formula ex)
getRulesetAxiom ScopedName
nam) [Ruleset ex]
rsets

-- | Find a named rule in a proof context.
getContextRule :: 
  ScopedName -- ^ Name of rule.
  -> Rule ex -- ^ Default rule (used if named component does not exist).
  -> [Ruleset ex] -- ^ Rulesets to search.
  -> Rule ex
getContextRule :: forall ex. ScopedName -> Rule ex -> [Ruleset ex] -> Rule ex
getContextRule ScopedName
nam Rule ex
def [Ruleset ex]
rsets = Rule ex -> Maybe (Rule ex) -> Rule ex
forall a. a -> Maybe a -> a
fromMaybe Rule ex
def (ScopedName -> [Ruleset ex] -> Maybe (Rule ex)
forall ex. ScopedName -> [Ruleset ex] -> Maybe (Rule ex)
getMaybeContextRule ScopedName
nam [Ruleset ex]
rsets)

-- | Find a named rule in a proof context.
getMaybeContextRule :: 
  ScopedName -- ^ Name of rule.
  -> [Ruleset ex] -- ^ Rulesets to search.
  -> Maybe (Rule ex)
getMaybeContextRule :: forall ex. ScopedName -> [Ruleset ex] -> Maybe (Rule ex)
getMaybeContextRule ScopedName
nam [Ruleset ex]
rsets =
    [Rule ex] -> Maybe (Rule ex)
forall a. [a] -> Maybe a
listToMaybe ([Rule ex] -> Maybe (Rule ex)) -> [Rule ex] -> Maybe (Rule ex)
forall a b. (a -> b) -> a -> b
$ (Ruleset ex -> Maybe (Rule ex)) -> [Ruleset ex] -> [Rule ex]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (ScopedName -> Ruleset ex -> Maybe (Rule ex)
forall ex. ScopedName -> Ruleset ex -> Maybe (Rule ex)
getRulesetRule ScopedName
nam) [Ruleset ex]
rsets

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