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