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

--------------------------------------------------------------------------------
--  See end of this file for licence information.
--------------------------------------------------------------------------------
-- |
--  Module      :  ProofContext
--  Copyright   :  (c) 2003, Graham Klyne, 2009 Vasili I Galchin, 2011, 2012, 2014 Douglas Burke
--  License     :  GPL V2
--
--  Maintainer  :  Douglas Burke
--  Stability   :  experimental
--  Portability :  CPP, OverloadedStrings
--
--  This module contains proof-context declarations based on
--  the RDF, RDFS, and RDF datatyping semantics specifications.
--  These definitions consist of namespaces (for identification
--  in proofs), axioms and inference rules.
--
--------------------------------------------------------------------------------

module Swish.RDF.ProofContext ( rulesetRDF
                              , rulesetRDFS
                              , rulesetRDFD) where

import Swish.Datatype (typeMkCanonicalForm)
import Swish.Namespace (Namespace, makeNSScopedName)
import Swish.QName (LName)
import Swish.Ruleset (makeRuleset)
import Swish.VarBinding (VarBindingModify(..))
import Swish.VarBinding (applyVarBinding, addVarBinding, makeVarFilterModify, varFilterDisjunction)

import Swish.RDF.BuiltIn.Datatypes (findRDFDatatype)

import Swish.RDF.Proof (makeRdfSubgraphEntailmentRule
                       , makeRdfSimpleEntailmentRule )

import Swish.RDF.Ruleset
    ( RDFFormula, RDFRule, RDFRuleset
    , makeRDFFormula
    , makeN3ClosureRule
    , makeN3ClosureSimpleRule
    , makeN3ClosureModifyRule
    , makeN3ClosureAllocatorRule
    , makeNodeAllocTo )

import Swish.RDF.VarBinding
    ( RDFVarBinding
    , RDFVarBindingModify
    , RDFVarBindingFilter
    , rdfVarBindingUriRef, rdfVarBindingBlank
    , rdfVarBindingLiteral
    , rdfVarBindingUntypedLiteral
    , rdfVarBindingXMLLiteral, rdfVarBindingDatatyped
    , rdfVarBindingMemberProp
    )

import Swish.RDF.Graph (RDFLabel(..), isUri)

import Swish.RDF.Vocabulary
    ( namespaceRDFD
    , scopeRDF
    , scopeRDFS
    , scopeRDFD
    )

#if (!defined(__GLASGOW_HASKELL__)) || (__GLASGOW_HASKELL__ < 710)
import Data.Monoid (Monoid(..))
#endif

import qualified Data.Text.Lazy.Builder as B

------------------------------------------------------------
--  Define query binding filter auxiliaries
------------------------------------------------------------

makeFormula :: Namespace -> LName -> B.Builder -> RDFFormula
makeFormula = makeRDFFormula

requireAny :: [RDFVarBindingFilter] -> RDFVarBindingFilter
requireAny = varFilterDisjunction

isLiteralV :: String -> RDFVarBindingFilter
isLiteralV = rdfVarBindingLiteral . Var

isUntypedLitV :: String -> RDFVarBindingFilter
isUntypedLitV = rdfVarBindingUntypedLiteral . Var

isXMLLitV :: String -> RDFVarBindingFilter
isXMLLitV = rdfVarBindingXMLLiteral . Var

isUriRefV :: String -> RDFVarBindingFilter
isUriRefV = rdfVarBindingUriRef . Var

isBlankV :: String -> RDFVarBindingFilter
isBlankV = rdfVarBindingBlank . Var

isDatatypedV :: String -> String -> RDFVarBindingFilter
isDatatypedV d l = rdfVarBindingDatatyped (Var d) (Var l)

isMemberPropV :: String -> RDFVarBindingFilter
isMemberPropV = rdfVarBindingMemberProp . Var

allocateTo :: String -> String -> [RDFLabel] -> RDFVarBindingModify
allocateTo bv av = makeNodeAllocTo (Var bv) (Var av)

--  Create new binding for datatype
valueSame :: String -> String -> String -> String -> RDFVarBindingModify
valueSame val1 typ1 val2 typ2 =
    sameDatatypedValue (Var val1) (Var typ1) (Var val2) (Var typ2)

--  Variable binding modifier to create new binding to a canonical
--  form of a datatyped literal.
sameDatatypedValue ::
    RDFLabel -> RDFLabel -> RDFLabel -> RDFLabel -> RDFVarBindingModify
sameDatatypedValue val1 typ1 val2 typ2 = VarBindingModify
        { vbmName   = makeNSScopedName namespaceRDFD "sameValue"
        , vbmApply  = sameDatatypedValueApplyAll val1 typ1 val2 typ2
        , vbmVocab  = [val1,typ1,val2,typ2]
        , vbmUsage  = [[val2]]
        }

sameDatatypedValueApplyAll ::
    RDFLabel -> RDFLabel -> RDFLabel -> RDFLabel
    -> [RDFVarBinding]
    -> [RDFVarBinding]
sameDatatypedValueApplyAll val1 typ1 val2 typ2 =
    concatMap (sameDatatypedValueApply val1 typ1 val2 typ2)

--  Auxiliary function that handles variable binding updates
--  for sameDatatypedValue
sameDatatypedValueApply ::
    RDFLabel -> RDFLabel -> RDFLabel -> RDFLabel
    -> RDFVarBinding
    -> [RDFVarBinding]
sameDatatypedValueApply val1 typ1 val2 typ2 vbind =
    result
    where
        v1    = applyVarBinding vbind val1
        t1    = applyVarBinding vbind typ1
        t2    = applyVarBinding vbind typ2
        sametype = getCanonical v1 t1 t2
        result   =
            if isUri t1 && isUri t2 then
                if t1 == t2 then
                    case sametype of
                      Just st -> [addVarBinding val2 st vbind]
                      _ -> []
                else
                    error "subtype conversions not yet defined"
            else
                []

{-
getCanonical :: RDFLabel -> RDFLabel -> RDFLabel -> Maybe RDFLabel
getCanonical v1 t1 t2 =
    if isDatatyped dqn1 v1 && isJust mdt1 then
        liftM mkLit $ typeMkCanonicalForm dt1 (getLiteralText v1)
    else
        Nothing
    where
        dqn1  = getRes t1
        dqn2  = getRes t2
        mdt1  = findRDFDatatype dqn1
        dt1   = fromJust mdt1
        mkLit = flip Lit (Just dqn2)

        getRes (Res dqnam) = dqnam
        getRes x = error $ "Expected a Resource, sent " ++ show x -- for -Wall
-}

getCanonical :: RDFLabel -> RDFLabel -> RDFLabel -> Maybe RDFLabel
getCanonical (TypedLit v dt) (Res dqn1) (Res dqn2) =
    if dt == dqn1
    then case findRDFDatatype dqn1 of
           Just dt1 -> flip TypedLit dqn2 `fmap` typeMkCanonicalForm dt1 v
           _ -> Nothing

    else Nothing

getCanonical _                _          _  = Nothing



{- -- Test data
qnamint = ScopedName namespaceXSD "integer"
xsdint  = Res qnamint
lab010  = Lit "010" (Just qnamint)
can010  = getCanonical lab010 xsdint xsdint
nsex    = Namespace "ex" "http://example.org/"
resexp  = Res (ScopedName nsex "p")
resexs  = Res (ScopedName nsex "s")

vara = Var "a"
varb = Var "b"
varc = Var "c"
vard = Var "d"
varp = Var "p"
vars = Var "s"
vart = Var "t"

vb1  = makeVarBinding [(vara,lab010),(varb,xsdint),(vard,xsdint)]
vb2  = sameDatatypedValueApply vara varb varc vard vb1
vb3  = vbmApply (sameDatatypedValue vara varb varc vard) [vb1]
vb3t = vb3 == vb2
vb4  = vbmApply (valueSame "a" "b" "c" "d") [vb1]
vb4t = vb4 == vb2
vb5  = vbmApply (valueSame "a" "b" "c" "b") [vb1]
vb5t = vb5 == vb2

vb6  = makeVarBinding [(vars,lab010),(varp,resexp),(vara,resexs),(vard,xsdint)]
vb7  = vbmApply (valueSame "s" "d" "t" "d") [vb6]
vb8  = makeVarBinding [(vars,lab010),(varp,resexp),(vara,resexs),(vard,xsdint)
                      ,(vart,fromJust can010)]
vb8t = vb7 == [vb8]
-- -}

------------------------------------------------------------
--  Common definitions
------------------------------------------------------------

------------------------------------------------------------
--  Define RDF axioms
------------------------------------------------------------

-- scopeRDF  = Namespace "rs-rdf"  "http://id.ninebynine.org/2003/Ruleset/rdf#"

--  RDF axioms (from RDF semantics document, section 3.1)
--
--  (See also, container property rules below)
--
rdfa1 :: RDFFormula
rdfa1 = makeFormula scopeRDF "a1" "rdf:type      rdf:type rdf:Property ."

rdfa2 :: RDFFormula
rdfa2 = makeFormula scopeRDF "a2" "rdf:subject   rdf:type rdf:Property ."

rdfa3 :: RDFFormula
rdfa3 = makeFormula scopeRDF "a3" "rdf:predicate rdf:type rdf:Property ."

rdfa4 :: RDFFormula
rdfa4 = makeFormula scopeRDF "a4" "rdf:object    rdf:type rdf:Property ."

rdfa5 :: RDFFormula
rdfa5 = makeFormula scopeRDF "a5" "rdf:first     rdf:type rdf:Property ."

rdfa6 :: RDFFormula
rdfa6 = makeFormula scopeRDF "a6" "rdf:rest      rdf:type rdf:Property ."

rdfa7 :: RDFFormula
rdfa7 = makeFormula scopeRDF "a7" "rdf:value     rdf:type rdf:Property ."

rdfa8 :: RDFFormula
rdfa8 = makeFormula scopeRDF "a8" "rdf:nil       rdf:type rdf:List ."

axiomsRDF :: [RDFFormula]
axiomsRDF =
    [ rdfa1,  rdfa2,  rdfa3,  rdfa4,  rdfa5
    , rdfa6,  rdfa7,  rdfa8
    ]

------------------------------------------------------------
--  Define RDF rules
------------------------------------------------------------

--  RDF subgraph entailment (from RDF semantics document section 2)
--
rdfsub :: RDFRule
rdfsub = makeRdfSubgraphEntailmentRule (makeNSScopedName scopeRDF "sub")

--  RDF simple entailment (from RDF semantics document section 7.1)
--  (Note: rules se1 and se2 are combined here, because the scope of
--  the "allocatedTo" modifier is the application of a single rule.)
--
rdfse :: RDFRule
rdfse = makeRdfSimpleEntailmentRule (makeNSScopedName scopeRDF "se")

--  RDF bnode-for-literal assignments (from RDF semantics document section 7.1)
--
rdflg :: RDFRule
rdflg = makeN3ClosureAllocatorRule scopeRDF "lg"
            "?x  ?a ?l . "
            "?x  ?a ?b . ?b rdf:_allocatedTo ?l ."
            (makeVarFilterModify $ isLiteralV "l")
            (allocateTo "b" "l")

--  RDF bnode-for-literal back-tracking (from RDF semantics document section 7.1)
--
rdfgl :: RDFRule
rdfgl = makeN3ClosureSimpleRule scopeRDF "gl"
            "?x  ?a ?l . ?b rdf:_allocatedTo ?l . "
            "?x  ?a ?b ."

--  RDF entailment rules (from RDF semantics document section 7.2)
--
--  (Note, statements with property rdf:_allocatedTo are introduced to
--  track bnodes introduced according to rule rdflf [presumably this
--  is actually rdflg?])
--
rdfr1 :: RDFRule
rdfr1 = makeN3ClosureSimpleRule scopeRDF "r1"
            "?x ?a ?y ."
            "?a rdf:type rdf:Property ."

rdfr2 :: RDFRule
rdfr2 = makeN3ClosureRule scopeRDF "r2"
            "?x  ?a ?b . ?b rdf:_allocatedTo ?l . "
            "?b rdf:type rdf:XMLLiteral ."
            (makeVarFilterModify $ isXMLLitV "l")

--  Container property axioms (from RDF semantics document section 3.1)
--
--  (Using here an inference rule with a filter in place of an axiom schema)
--
--  This is a restricted form of the given axioms, in that the axioms
--  are asserted only for container membership terms that appear in
--  the graph.
--
--  (This may be very inefficient for forward chaining when dealing with
--  large graphs:  may need to look at query logic to see if the search for
--  container membership properties can be optimized.  This may call for a
--  custom inference rule.)
--
rdfcp1 :: RDFRule
rdfcp1 = makeN3ClosureRule scopeRDF "cp1"
            "?x  ?c ?y . "
            "?c rdf:type rdf:Property ."
            (makeVarFilterModify $ isMemberPropV "c")

rdfcp2 :: RDFRule
rdfcp2 = makeN3ClosureRule scopeRDF "cp2"
            "?c  ?p ?y . "
            "?c rdf:type rdf:Property ."
            (makeVarFilterModify $ isMemberPropV "c")

rdfcp3 :: RDFRule
rdfcp3 = makeN3ClosureRule scopeRDF "cp3"
            "?x  ?p ?c . "
            "?c rdf:type rdf:Property ."
            (makeVarFilterModify $ isMemberPropV "c")

--  Collect RDF rules
--
rulesRDF :: [RDFRule]
rulesRDF =
    [ rdfsub,     rdfse
    , rdflg,      rdfgl
    , rdfr1,      rdfr2
    , rdfcp1,     rdfcp2,     rdfcp3
    ]

-- | Ruleset for RDF inference.

rulesetRDF :: RDFRuleset
rulesetRDF = makeRuleset scopeRDF axiomsRDF rulesRDF

------------------------------------------------------------
--  Define RDFS axioms
------------------------------------------------------------

-- scopeRDFS = Namespace "rdfs" "http://id.ninebynine.org/2003/Ruleset/rdfs#"

--  RDFS axioms (from RDF semantics document, section 4.1)
--
--  (See also, container property rules below)
--

rdfsa01 :: RDFFormula
rdfsa01 = makeFormula scopeRDFS "a01"
    "rdf:type           rdfs:domain rdfs:Resource ."

rdfsa02 :: RDFFormula
rdfsa02 = makeFormula scopeRDFS "a02"
    "rdf:type           rdfs:range  rdfs:Class ."

rdfsa03 :: RDFFormula
rdfsa03 = makeFormula scopeRDFS "a03"
    "rdfs:domain        rdfs:domain rdf:Property ."

rdfsa04 :: RDFFormula
rdfsa04 = makeFormula scopeRDFS "a04"
    "rdfs:domain        rdfs:range  rdfs:Class ."

rdfsa05 :: RDFFormula
rdfsa05 = makeFormula scopeRDFS "a05"
    "rdfs:range         rdfs:domain rdf:Property ."

rdfsa06 :: RDFFormula
rdfsa06 = makeFormula scopeRDFS "a06"
    "rdfs:range         rdfs:range  rdfs:Class ."

rdfsa07 :: RDFFormula
rdfsa07 = makeFormula scopeRDFS "a07"
    "rdfs:subPropertyOf rdfs:domain rdf:Property ."

rdfsa08 :: RDFFormula
rdfsa08 = makeFormula scopeRDFS "a08"
    "rdfs:subPropertyOf rdfs:range  rdf:Property ."

rdfsa09 :: RDFFormula
rdfsa09 = makeFormula scopeRDFS "a09"
    "rdfs:subClassOf    rdfs:domain rdfs:Class ."

rdfsa10 :: RDFFormula
rdfsa10 = makeFormula scopeRDFS "a10"
    "rdfs:subClassOf    rdfs:range  rdfs:Class ."

rdfsa11 :: RDFFormula
rdfsa11 = makeFormula scopeRDFS "a11"
    "rdf:subject        rdfs:domain rdf:Statement ."

rdfsa12 :: RDFFormula
rdfsa12 = makeFormula scopeRDFS "a12"
    "rdf:subject        rdfs:range  rdfs:Resource ."

rdfsa13 :: RDFFormula
rdfsa13 = makeFormula scopeRDFS "a13"
    "rdf:predicate      rdfs:domain rdf:Statement ."

rdfsa14 :: RDFFormula
rdfsa14 = makeFormula scopeRDFS "a14"
    "rdf:predicate      rdfs:range  rdfs:Resource ."

rdfsa15 :: RDFFormula
rdfsa15 = makeFormula scopeRDFS "a15"
    "rdf:object         rdfs:domain rdf:Statement ."

rdfsa16 :: RDFFormula
rdfsa16 = makeFormula scopeRDFS "a16"
    "rdf:object         rdfs:range  rdfs:Resource ."

rdfsa17 :: RDFFormula
rdfsa17 = makeFormula scopeRDFS "a17"
    "rdfs:member        rdfs:domain rdfs:Resource ."

rdfsa18 :: RDFFormula
rdfsa18 = makeFormula scopeRDFS "a18"
    "rdfs:member        rdfs:range  rdfs:Resource ."

rdfsa19 :: RDFFormula
rdfsa19 = makeFormula scopeRDFS "a19"
    "rdf:first          rdfs:domain rdf:List ."

rdfsa20 :: RDFFormula
rdfsa20 = makeFormula scopeRDFS "a20"
    "rdf:first          rdfs:range  rdfs:Resource ."

rdfsa21 :: RDFFormula
rdfsa21 = makeFormula scopeRDFS "a21"
    "rdf:rest           rdfs:domain rdf:List ."

rdfsa22 :: RDFFormula
rdfsa22 = makeFormula scopeRDFS "a22"
    "rdf:rest           rdfs:range  rdf:List ."

rdfsa23 :: RDFFormula
rdfsa23 = makeFormula scopeRDFS "a23"
    "rdfs:seeAlso       rdfs:domain rdfs:Resource ."

rdfsa24 :: RDFFormula
rdfsa24 = makeFormula scopeRDFS "a24"
    "rdfs:seeAlso       rdfs:range  rdfs:Resource ."

rdfsa25 :: RDFFormula
rdfsa25 = makeFormula scopeRDFS "a25"
    "rdfs:isDefinedBy   rdfs:domain rdfs:Resource ."

rdfsa26 :: RDFFormula
rdfsa26 = makeFormula scopeRDFS "a26"
    "rdfs:isDefinedBy   rdfs:range  rdfs:Resource ."

rdfsa27 :: RDFFormula
rdfsa27 = makeFormula scopeRDFS "a27"
    "rdfs:isDefinedBy   rdfs:subPropertyOf rdfs:seeAlso ."

rdfsa28 :: RDFFormula
rdfsa28 = makeFormula scopeRDFS "a28"
    "rdfs:comment       rdfs:domain rdfs:Resource ."

rdfsa29 :: RDFFormula
rdfsa29 = makeFormula scopeRDFS "a29"
    "rdfs:comment       rdfs:range  rdfs:Literal ."

rdfsa30 :: RDFFormula
rdfsa30 = makeFormula scopeRDFS "a30"
    "rdfs:label         rdfs:domain rdfs:Resource ."

rdfsa31 :: RDFFormula
rdfsa31 = makeFormula scopeRDFS "a31"
    "rdfs:label         rdfs:range  rdfs:Literal ."

rdfsa32 :: RDFFormula
rdfsa32 = makeFormula scopeRDFS "a32"
    "rdf:value          rdfs:domain rdfs:Resource ."

rdfsa33 :: RDFFormula
rdfsa33 = makeFormula scopeRDFS "a33"
    "rdf:value          rdfs:range  rdfs:Resource ."

rdfsa34 :: RDFFormula
rdfsa34 = makeFormula scopeRDFS "a34"
    "rdf:Alt            rdfs:subClassOf    rdfs:Container ."

rdfsa35 :: RDFFormula
rdfsa35 = makeFormula scopeRDFS "a35"
    "rdf:Bag            rdfs:subClassOf    rdfs:Container ."

rdfsa36 :: RDFFormula
rdfsa36 = makeFormula scopeRDFS "a36"
    "rdf:Seq            rdfs:subClassOf    rdfs:Container ."

rdfsa37 :: RDFFormula
rdfsa37 = makeFormula scopeRDFS "a37"
    "rdfs:ContainerMembershipProperty rdfs:subClassOf rdf:Property ."

rdfsa38 :: RDFFormula
rdfsa38 = makeFormula scopeRDFS "a38"
    "rdf:XMLLiteral     rdf:type           rdfs:Datatype ."

rdfsa39 :: RDFFormula
rdfsa39 = makeFormula scopeRDFS "a39"
    "rdf:XMLLiteral     rdfs:subClassOf    rdfs:Literal ."

rdfsa40 :: RDFFormula
rdfsa40 = makeFormula scopeRDFS "a40"
    "rdfs:Datatype      rdfs:subClassOf    rdfs:Class ."

axiomsRDFS :: [RDFFormula]
axiomsRDFS =
    [          rdfsa01, rdfsa02, rdfsa03, rdfsa04
    , rdfsa05, rdfsa06, rdfsa07, rdfsa08, rdfsa09
    , rdfsa10, rdfsa11, rdfsa12, rdfsa13, rdfsa14
    , rdfsa15, rdfsa16, rdfsa17, rdfsa18, rdfsa19
    , rdfsa20, rdfsa21, rdfsa22, rdfsa23, rdfsa24
    , rdfsa25, rdfsa26, rdfsa27, rdfsa28, rdfsa29
    , rdfsa30, rdfsa31, rdfsa32, rdfsa33, rdfsa34
    , rdfsa35, rdfsa36, rdfsa37, rdfsa38, rdfsa39
    , rdfsa40
    ]

------------------------------------------------------------
--  Define RDFS rules
------------------------------------------------------------

{-
rdfr2 = makeN3ClosureRule scopeRDF "r2"
            "?x  ?a ?b . ?b rdf:_allocatedTo ?l . "
            "?b rdf:type rdf:XMLLiteral ."
            (makeVarFilterModify $ isXMLLit "?l")
-}

--  RDFS entailment rules (from RDF semantics document section 7.2)
--
--  (Note, statements with property rdf:_allocatedTo are introduced to
--  track bnodes introduced according to rule rdflf [presumably this
--  is actually rdflg?])
--
rdfsr1 :: RDFRule
rdfsr1 = makeN3ClosureRule scopeRDFS "r1"
            "?x  ?a ?b . ?b rdf:_allocatedTo ?l . "
            "?b rdf:type rdfs:Literal ."
            (makeVarFilterModify $ isUntypedLitV "l" )

rdfsr2 :: RDFRule
rdfsr2 = makeN3ClosureSimpleRule scopeRDFS "r2"
            "?x ?a ?y . ?a rdfs:domain ?z ."
            "?x rdf:type ?z ."

rdfsr3 :: RDFRule
rdfsr3 = makeN3ClosureRule scopeRDFS "r3"
            "?u ?a ?v . ?a rdfs:range ?z ."
            "?v rdf:type ?z ."
            (makeVarFilterModify $ requireAny [isUriRefV "v",isBlankV "v"])

rdfsr4a :: RDFRule
rdfsr4a = makeN3ClosureSimpleRule scopeRDFS "r4a"
            "?x ?a ?y ."
            "?x rdf:type rdfs:Resource ."

rdfsr4b :: RDFRule
rdfsr4b = makeN3ClosureRule scopeRDFS "r4b"
            "?x ?a ?u ."
            "?u rdf:type rdfs:Resource ."
            (makeVarFilterModify $ requireAny [isUriRefV "u",isBlankV "u"])

rdfsr5 :: RDFRule
rdfsr5  = makeN3ClosureSimpleRule scopeRDFS "r5"
            "?a rdfs:subPropertyOf ?b . ?b rdfs:subPropertyOf ?c ."
            "?a rdfs:subPropertyOf ?c ."

rdfsr6 :: RDFRule
rdfsr6  = makeN3ClosureSimpleRule scopeRDFS "r6"
            "?x rdf:type rdf:Property ."
            "?x rdfs:subPropertyOf ?x ."

rdfsr7 :: RDFRule
rdfsr7  = makeN3ClosureSimpleRule scopeRDFS "r7"
            "?x ?a ?y . ?a rdfs:subPropertyOf ?b ."
            "?x ?b ?y ."

rdfsr8 :: RDFRule
rdfsr8  = makeN3ClosureSimpleRule scopeRDFS "r8"
            "?x rdf:type rdfs:Class ."
            "?x rdfs:subClassOf rdfs:Resource ."

rdfsr9 :: RDFRule
rdfsr9  = makeN3ClosureSimpleRule scopeRDFS "r9"
            "?x rdfs:subClassOf ?y . ?a rdf:type ?x ."
            "?a rdf:type ?y ."

rdfsr10 :: RDFRule
rdfsr10 = makeN3ClosureSimpleRule scopeRDFS "r10"
            "?x rdf:type rdfs:Class ."
            "?x rdfs:subClassOf ?x ."

rdfsr11 :: RDFRule
rdfsr11 = makeN3ClosureSimpleRule scopeRDFS "r11"
            "?x rdfs:subClassOf ?y . ?y rdfs:subClassOf ?z ."
            "?x rdfs:subClassOf ?z ."

rdfsr12 :: RDFRule
rdfsr12 = makeN3ClosureSimpleRule scopeRDFS "r12"
            "?x rdf:type rdfs:ContainerMembershipProperty ."
            "?x rdfs:subPropertyOf rdfs:member ."

rdfsr13 :: RDFRule
rdfsr13 = makeN3ClosureSimpleRule scopeRDFS "r13"
            "?x rdf:type rdfs:Datatype ."
            "?x rdfs:subClassOf rdfs:Literal ."

--  These are valid only under an extensional strengthening of RDFS,
--  discussed in section 7.3.1 of the RDF semantics specification:

{-
rdfsrext1 :: RDFRule
rdfsrext1 = makeN3ClosureSimpleRule scopeRDFS "ext1"
            "?x rdfs:domain ?y . ?y rdfs:subClassOf ?z ."
            "?x rdfs:domain ?z ."

rdfsrext2 :: RDFRule
rdfsrext2 = makeN3ClosureSimpleRule scopeRDFS "ext2"
            "?x rdfs:range ?y . ?y rdfs:subClassOf ?z ."
            "?x rdfs:range ?z ."

rdfsrext3 :: RDFRule
rdfsrext3 = makeN3ClosureSimpleRule scopeRDFS "ext3"
            "?x rdfs:domain ?y . ?z rdfs:subPropertyOf ?x ."
            "?z rdfs:domain ?y ."

rdfsrext4 :: RDFRule
rdfsrext4 = makeN3ClosureSimpleRule scopeRDFS "ext4"
            "?x rdfs:range ?y . ?z rdfs:subPropertyOf ?x ."
            "?z rdfs:range ?y ."

rdfsrext5 :: RDFRule
rdfsrext5 = makeN3ClosureSimpleRule scopeRDFS "ext5"
            "rdf:type rdfs:subPropertyOf ?z . ?z rdfs:domain ?y ."
            "rdfs:Resource rdfs:subClassOf ?y ."

rdfsrext6 :: RDFRule
rdfsrext6 = makeN3ClosureSimpleRule scopeRDFS "rext6"
            "rdfs:subClassOf rdfs:subPropertyOf ?z . ?z rdfs:domain ?y ."
            "rdfs:Class rdfs:subClassOf ?y ."

rdfsrext7 :: RDFRule
rdfsrext7 = makeN3ClosureSimpleRule scopeRDFS "rext7"
            "rdfs:subPropertyOf rdfs:subPropertyOf ?z . ?z rdfs:domain ?y ."
            "rdfs:Property rdfs:subClassOf ?y ."

rdfsrext8 :: RDFRule
rdfsrext8 = makeN3ClosureSimpleRule scopeRDFS "rext8"
            "rdfs:subClassOf rdfs:subPropertyOf ?z . ?z rdfs:range ?y ."
            "rdfs:Class rdfs:subClassOf ?y ."

rdfsrext9 :: RDFRule
rdfsrext9 = makeN3ClosureSimpleRule scopeRDFS "rext9"
            "rdfs:subPropertyOf rdfs:subPropertyOf ?z . ?z rdfs:range ?y ."
            "rdfs:Property rdfs:subClassOf ?y ."

-}

--  Container property axioms (from RDF semantics document section 4.1)
--
--  (Using here an inference rule with a filter in place of an axiom schema)
--
--  This is a restricted form of the given axioms, in that the axioms
--  are asserted only for container membership terms that appear in
--  the graph.
--
--  (This may be very inefficient for forward chaining when dealing with
--  large graphs:  may need to look at query logic to see if the search for
--  container membership properties can be optimized.  This may call for a
--  custom inference rule.)
--
rdfscp11 :: RDFRule
rdfscp11 = makeN3ClosureRule scopeRDFS "cp11"
            "?x  ?c ?y . "
            "?c rdf:type rdfs:ContainerMembershipProperty ."
            (makeVarFilterModify $ isMemberPropV "c")

rdfscp12 :: RDFRule
rdfscp12 = makeN3ClosureRule scopeRDFS "cp12"
            "?c  ?p ?y . "
            "?c rdf:type rdfs:ContainerMembershipProperty ."
            (makeVarFilterModify $ isMemberPropV "c")

rdfscp13 :: RDFRule
rdfscp13 = makeN3ClosureRule scopeRDFS "cp13"
            "?x  ?p ?c . "
            "?c rdf:type rdfs:ContainerMembershipProperty ."
            (makeVarFilterModify $ isMemberPropV "c")

rdfscp21 :: RDFRule
rdfscp21 = makeN3ClosureRule scopeRDFS "cp21"
            "?x  ?c ?y . "
            "?c rdfs:domain rdfs:Resource ."
            (makeVarFilterModify $ isMemberPropV "c")

rdfscp22 :: RDFRule
rdfscp22 = makeN3ClosureRule scopeRDFS "cp22"
            "?c  ?p ?y . "
            "?c rdfs:domain rdfs:Resource ."
            (makeVarFilterModify $ isMemberPropV "c")

rdfscp23 :: RDFRule
rdfscp23 = makeN3ClosureRule scopeRDFS "cp23"
            "?x  ?p ?c . "
            "?c rdfs:domain rdfs:Resource ."
            (makeVarFilterModify $ isMemberPropV "c")

rdfscp31 :: RDFRule
rdfscp31 = makeN3ClosureRule scopeRDFS "cp31"
            "?x  ?c ?y . "
            "?c rdfs:range rdfs:Resource ."
            (makeVarFilterModify $ isMemberPropV "c")

rdfscp32 :: RDFRule
rdfscp32 = makeN3ClosureRule scopeRDFS "cp32"
            "?c  ?p ?y . "
            "?c rdfs:range rdfs:Resource ."
            (makeVarFilterModify $ isMemberPropV "c")

rdfscp33 :: RDFRule
rdfscp33 = makeN3ClosureRule scopeRDFS "cp33"
            "?x  ?p ?c . "
            "?c rdfs:range rdfs:Resource ."
            (makeVarFilterModify $ isMemberPropV "c")

--  Collect RDFS rules
--
rulesRDFS :: [RDFRule]
rulesRDFS =
    [ rdfsr1,    rdfsr2,    rdfsr3,    rdfsr4a,   rdfsr4b
    , rdfsr5,    rdfsr6,    rdfsr7,    rdfsr8,    rdfsr9
    , rdfsr10,   rdfsr11,   rdfsr12,   rdfsr13
    , rdfscp11,   rdfscp12,   rdfscp13
    , rdfscp21,   rdfscp22,   rdfscp23
    , rdfscp31,   rdfscp32,   rdfscp33
    ]

-- | Ruleset for RDFS inference.

rulesetRDFS :: RDFRuleset
rulesetRDFS = makeRuleset scopeRDFS axiomsRDFS rulesRDFS

------------------------------------------------------------
--  Define RDFD (datatyping) axioms
------------------------------------------------------------

-- scopeRDFD = Namespace "rdfd" "http://id.ninebynine.org/2003/Ruleset/rdfd#"

axiomsRDFD :: [RDFFormula]
axiomsRDFD =
    [
    ]

------------------------------------------------------------
--  Define RDFD (datatyping) axioms
------------------------------------------------------------

--  RDFD closure rules from semantics document, section 7.4

--  Infer type of datatyped literal
--
rdfdr1 :: RDFRule
rdfdr1 = makeN3ClosureRule scopeRDFD "r1"
            "?d rdf:type rdfs:Datatype . ?a ?p ?l . ?b rdf:_allocatedTo ?l . "
            "?b rdf:type ?d ."
            (makeVarFilterModify $ isDatatypedV "d" "l")

--  Equivalent literals with same datatype:
--  (generate canonical form, or operate in proof mode only)
--
rdfdr2 :: RDFRule
rdfdr2 = makeN3ClosureRule scopeRDFD "r2"
            "?d rdf:type rdfs:Datatype . ?a ?p ?s ."
            "?a ?p ?t ."
            (valueSame "s" "d" "t" "d")

{- Note that valueSame does datatype check.  Otherwise use:
rdfdr2 = makeN3ClosureModifyRule scopeRDFD "r2"
            "?d rdf:type rdfs:Datatype . ?a ?p ?s ."
            "?a ?p ?t ."
            (makeVarFilterModify $ isDatatypedV "d" "s")
            (valueSame "s" "d" "t" "d")
-}

--  Equivalent literals with different datatypes:
--  (generate canonical form, or operate in proof mode only)
--
rdfdr3 :: RDFRule
rdfdr3 = makeN3ClosureModifyRule scopeRDFD "r3"
            ( "?d rdf:type rdfs:Datatype . ?e rdf:type rdfs:Datatype . " `mappend`
              "?a ?p ?s ." )
            "?a ?p ?t ."
            (makeVarFilterModify $ isDatatypedV "s" "d")
            (valueSame "s" "d" "t" "e")

--  Collect RDFD rules
--
rulesRDFD :: [RDFRule]
rulesRDFD =
    [ rdfdr1, rdfdr2, rdfdr3
    ]

-- | Ruleset for RDFD (datatyping) inference.
--
rulesetRDFD :: RDFRuleset
rulesetRDFD = makeRuleset scopeRDFD axiomsRDFD rulesRDFD

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