{-# 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 :: Namespace -> LName -> Builder -> RDFFormula
makeFormula = Namespace -> LName -> Builder -> RDFFormula
makeRDFFormula

requireAny :: [RDFVarBindingFilter] -> RDFVarBindingFilter
requireAny :: [RDFVarBindingFilter] -> RDFVarBindingFilter
requireAny = [RDFVarBindingFilter] -> RDFVarBindingFilter
forall a b. Eq a => [VarBindingFilter a b] -> VarBindingFilter a b
varFilterDisjunction

isLiteralV :: String -> RDFVarBindingFilter
isLiteralV :: String -> RDFVarBindingFilter
isLiteralV = RDFLabel -> RDFVarBindingFilter
rdfVarBindingLiteral (RDFLabel -> RDFVarBindingFilter)
-> (String -> RDFLabel) -> String -> RDFVarBindingFilter
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> RDFLabel
Var

isUntypedLitV :: String -> RDFVarBindingFilter
isUntypedLitV :: String -> RDFVarBindingFilter
isUntypedLitV = RDFLabel -> RDFVarBindingFilter
rdfVarBindingUntypedLiteral (RDFLabel -> RDFVarBindingFilter)
-> (String -> RDFLabel) -> String -> RDFVarBindingFilter
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> RDFLabel
Var

isXMLLitV :: String -> RDFVarBindingFilter
isXMLLitV :: String -> RDFVarBindingFilter
isXMLLitV = RDFLabel -> RDFVarBindingFilter
rdfVarBindingXMLLiteral (RDFLabel -> RDFVarBindingFilter)
-> (String -> RDFLabel) -> String -> RDFVarBindingFilter
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> RDFLabel
Var

isUriRefV :: String -> RDFVarBindingFilter
isUriRefV :: String -> RDFVarBindingFilter
isUriRefV = RDFLabel -> RDFVarBindingFilter
rdfVarBindingUriRef (RDFLabel -> RDFVarBindingFilter)
-> (String -> RDFLabel) -> String -> RDFVarBindingFilter
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> RDFLabel
Var

isBlankV :: String -> RDFVarBindingFilter
isBlankV :: String -> RDFVarBindingFilter
isBlankV = RDFLabel -> RDFVarBindingFilter
rdfVarBindingBlank (RDFLabel -> RDFVarBindingFilter)
-> (String -> RDFLabel) -> String -> RDFVarBindingFilter
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> RDFLabel
Var

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

isMemberPropV :: String -> RDFVarBindingFilter
isMemberPropV :: String -> RDFVarBindingFilter
isMemberPropV = RDFLabel -> RDFVarBindingFilter
rdfVarBindingMemberProp (RDFLabel -> RDFVarBindingFilter)
-> (String -> RDFLabel) -> String -> RDFVarBindingFilter
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> RDFLabel
Var

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

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

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

sameDatatypedValueApplyAll ::
    RDFLabel -> RDFLabel -> RDFLabel -> RDFLabel
    -> [RDFVarBinding]
    -> [RDFVarBinding]
sameDatatypedValueApplyAll :: RDFLabel
-> RDFLabel
-> RDFLabel
-> RDFLabel
-> [VarBinding RDFLabel RDFLabel]
-> [VarBinding RDFLabel RDFLabel]
sameDatatypedValueApplyAll RDFLabel
val1 RDFLabel
typ1 RDFLabel
val2 RDFLabel
typ2 =
    (VarBinding RDFLabel RDFLabel -> [VarBinding RDFLabel RDFLabel])
-> [VarBinding RDFLabel RDFLabel] -> [VarBinding RDFLabel RDFLabel]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (RDFLabel
-> RDFLabel
-> RDFLabel
-> RDFLabel
-> VarBinding RDFLabel RDFLabel
-> [VarBinding RDFLabel RDFLabel]
sameDatatypedValueApply RDFLabel
val1 RDFLabel
typ1 RDFLabel
val2 RDFLabel
typ2) 

--  Auxiliary function that handles variable binding updates
--  for sameDatatypedValue
sameDatatypedValueApply ::
    RDFLabel -> RDFLabel -> RDFLabel -> RDFLabel
    -> RDFVarBinding
    -> [RDFVarBinding]
sameDatatypedValueApply :: RDFLabel
-> RDFLabel
-> RDFLabel
-> RDFLabel
-> VarBinding RDFLabel RDFLabel
-> [VarBinding RDFLabel RDFLabel]
sameDatatypedValueApply RDFLabel
val1 RDFLabel
typ1 RDFLabel
val2 RDFLabel
typ2 VarBinding RDFLabel RDFLabel
vbind =
    [VarBinding RDFLabel RDFLabel]
result
    where
        v1 :: RDFLabel
v1    = VarBinding RDFLabel RDFLabel -> RDFLabel -> RDFLabel
forall a. VarBinding a a -> a -> a
applyVarBinding VarBinding RDFLabel RDFLabel
vbind RDFLabel
val1
        t1 :: RDFLabel
t1    = VarBinding RDFLabel RDFLabel -> RDFLabel -> RDFLabel
forall a. VarBinding a a -> a -> a
applyVarBinding VarBinding RDFLabel RDFLabel
vbind RDFLabel
typ1
        t2 :: RDFLabel
t2    = VarBinding RDFLabel RDFLabel -> RDFLabel -> RDFLabel
forall a. VarBinding a a -> a -> a
applyVarBinding VarBinding RDFLabel RDFLabel
vbind RDFLabel
typ2
        sametype :: Maybe RDFLabel
sametype = RDFLabel -> RDFLabel -> RDFLabel -> Maybe RDFLabel
getCanonical RDFLabel
v1 RDFLabel
t1 RDFLabel
t2
        result :: [VarBinding RDFLabel RDFLabel]
result   =
            if RDFLabel -> Bool
isUri RDFLabel
t1 Bool -> Bool -> Bool
&& RDFLabel -> Bool
isUri RDFLabel
t2 then
                if RDFLabel
t1 RDFLabel -> RDFLabel -> Bool
forall a. Eq a => a -> a -> Bool
== RDFLabel
t2 then
                    case Maybe RDFLabel
sametype of
                      Just RDFLabel
st -> [RDFLabel
-> RDFLabel
-> VarBinding RDFLabel RDFLabel
-> VarBinding RDFLabel RDFLabel
forall a b.
(Ord a, Ord b) =>
a -> b -> VarBinding a b -> VarBinding a b
addVarBinding RDFLabel
val2 RDFLabel
st VarBinding RDFLabel RDFLabel
vbind]
                      Maybe RDFLabel
_ -> []
                else
                    String -> [VarBinding RDFLabel RDFLabel]
forall a. HasCallStack => String -> a
error String
"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 :: RDFLabel -> RDFLabel -> RDFLabel -> Maybe RDFLabel
getCanonical (TypedLit Text
v ScopedName
dt) (Res ScopedName
dqn1) (Res ScopedName
dqn2) =
    if ScopedName
dt ScopedName -> ScopedName -> Bool
forall a. Eq a => a -> a -> Bool
== ScopedName
dqn1
    then case ScopedName -> Maybe RDFDatatype
findRDFDatatype ScopedName
dqn1 of
           Just RDFDatatype
dt1 -> (Text -> ScopedName -> RDFLabel) -> ScopedName -> Text -> RDFLabel
forall a b c. (a -> b -> c) -> b -> a -> c
flip Text -> ScopedName -> RDFLabel
TypedLit ScopedName
dqn2 (Text -> RDFLabel) -> Maybe Text -> Maybe RDFLabel
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` RDFDatatype -> Text -> Maybe Text
forall ex lb vn. Datatype ex lb vn -> Text -> Maybe Text
typeMkCanonicalForm RDFDatatype
dt1 Text
v
           Maybe RDFDatatype
_ -> Maybe RDFLabel
forall a. Maybe a
Nothing

    else Maybe RDFLabel
forall a. Maybe a
Nothing

getCanonical RDFLabel
_                RDFLabel
_          RDFLabel
_  = Maybe RDFLabel
forall a. Maybe a
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 :: RDFFormula
rdfa1 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDF LName
"a1" Builder
"rdf:type      rdf:type rdf:Property ."

rdfa2 :: RDFFormula
rdfa2 :: RDFFormula
rdfa2 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDF LName
"a2" Builder
"rdf:subject   rdf:type rdf:Property ."

rdfa3 :: RDFFormula
rdfa3 :: RDFFormula
rdfa3 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDF LName
"a3" Builder
"rdf:predicate rdf:type rdf:Property ."

rdfa4 :: RDFFormula
rdfa4 :: RDFFormula
rdfa4 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDF LName
"a4" Builder
"rdf:object    rdf:type rdf:Property ."

rdfa5 :: RDFFormula
rdfa5 :: RDFFormula
rdfa5 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDF LName
"a5" Builder
"rdf:first     rdf:type rdf:Property ."

rdfa6 :: RDFFormula
rdfa6 :: RDFFormula
rdfa6 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDF LName
"a6" Builder
"rdf:rest      rdf:type rdf:Property ."

rdfa7 :: RDFFormula
rdfa7 :: RDFFormula
rdfa7 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDF LName
"a7" Builder
"rdf:value     rdf:type rdf:Property ."

rdfa8 :: RDFFormula
rdfa8 :: RDFFormula
rdfa8 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDF LName
"a8" Builder
"rdf:nil       rdf:type rdf:List ."

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

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

--  RDF subgraph entailment (from RDF semantics document section 2)
--
rdfsub :: RDFRule 
rdfsub :: RDFRule
rdfsub = ScopedName -> RDFRule
makeRdfSubgraphEntailmentRule (Namespace -> LName -> ScopedName
makeNSScopedName Namespace
scopeRDF LName
"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 :: RDFRule
rdfse = ScopedName -> RDFRule
makeRdfSimpleEntailmentRule (Namespace -> LName -> ScopedName
makeNSScopedName Namespace
scopeRDF LName
"se")

--  RDF bnode-for-literal assignments (from RDF semantics document section 7.1)
--
rdflg :: RDFRule
rdflg :: RDFRule
rdflg = Namespace
-> LName
-> Builder
-> Builder
-> RDFVarBindingModify
-> ([RDFLabel] -> RDFVarBindingModify)
-> RDFRule
makeN3ClosureAllocatorRule Namespace
scopeRDF LName
"lg"
            Builder
"?x  ?a ?l . "
            Builder
"?x  ?a ?b . ?b rdf:_allocatedTo ?l ."
            (RDFVarBindingFilter -> RDFVarBindingModify
forall a b. VarBindingFilter a b -> VarBindingModify a b
makeVarFilterModify (RDFVarBindingFilter -> RDFVarBindingModify)
-> RDFVarBindingFilter -> RDFVarBindingModify
forall a b. (a -> b) -> a -> b
$ String -> RDFVarBindingFilter
isLiteralV String
"l")
            (String -> String -> [RDFLabel] -> RDFVarBindingModify
allocateTo String
"b" String
"l")

--  RDF bnode-for-literal back-tracking (from RDF semantics document section 7.1)
--
rdfgl :: RDFRule
rdfgl :: RDFRule
rdfgl = Namespace -> LName -> Builder -> Builder -> RDFRule
makeN3ClosureSimpleRule Namespace
scopeRDF LName
"gl"
            Builder
"?x  ?a ?l . ?b rdf:_allocatedTo ?l . "
            Builder
"?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 :: RDFRule
rdfr1 = Namespace -> LName -> Builder -> Builder -> RDFRule
makeN3ClosureSimpleRule Namespace
scopeRDF LName
"r1"
            Builder
"?x ?a ?y ."
            Builder
"?a rdf:type rdf:Property ."

rdfr2 :: RDFRule
rdfr2 :: RDFRule
rdfr2 = Namespace
-> LName -> Builder -> Builder -> RDFVarBindingModify -> RDFRule
makeN3ClosureRule Namespace
scopeRDF LName
"r2"
            Builder
"?x  ?a ?b . ?b rdf:_allocatedTo ?l . "
            Builder
"?b rdf:type rdf:XMLLiteral ."
            (RDFVarBindingFilter -> RDFVarBindingModify
forall a b. VarBindingFilter a b -> VarBindingModify a b
makeVarFilterModify (RDFVarBindingFilter -> RDFVarBindingModify)
-> RDFVarBindingFilter -> RDFVarBindingModify
forall a b. (a -> b) -> a -> b
$ String -> RDFVarBindingFilter
isXMLLitV String
"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 :: RDFRule
rdfcp1 = Namespace
-> LName -> Builder -> Builder -> RDFVarBindingModify -> RDFRule
makeN3ClosureRule Namespace
scopeRDF LName
"cp1"
            Builder
"?x  ?c ?y . "
            Builder
"?c rdf:type rdf:Property ."
            (RDFVarBindingFilter -> RDFVarBindingModify
forall a b. VarBindingFilter a b -> VarBindingModify a b
makeVarFilterModify (RDFVarBindingFilter -> RDFVarBindingModify)
-> RDFVarBindingFilter -> RDFVarBindingModify
forall a b. (a -> b) -> a -> b
$ String -> RDFVarBindingFilter
isMemberPropV String
"c")

rdfcp2 :: RDFRule
rdfcp2 :: RDFRule
rdfcp2 = Namespace
-> LName -> Builder -> Builder -> RDFVarBindingModify -> RDFRule
makeN3ClosureRule Namespace
scopeRDF LName
"cp2"
            Builder
"?c  ?p ?y . "
            Builder
"?c rdf:type rdf:Property ."
            (RDFVarBindingFilter -> RDFVarBindingModify
forall a b. VarBindingFilter a b -> VarBindingModify a b
makeVarFilterModify (RDFVarBindingFilter -> RDFVarBindingModify)
-> RDFVarBindingFilter -> RDFVarBindingModify
forall a b. (a -> b) -> a -> b
$ String -> RDFVarBindingFilter
isMemberPropV String
"c")

rdfcp3 :: RDFRule
rdfcp3 :: RDFRule
rdfcp3 = Namespace
-> LName -> Builder -> Builder -> RDFVarBindingModify -> RDFRule
makeN3ClosureRule Namespace
scopeRDF LName
"cp3"
            Builder
"?x  ?p ?c . "
            Builder
"?c rdf:type rdf:Property ."
            (RDFVarBindingFilter -> RDFVarBindingModify
forall a b. VarBindingFilter a b -> VarBindingModify a b
makeVarFilterModify (RDFVarBindingFilter -> RDFVarBindingModify)
-> RDFVarBindingFilter -> RDFVarBindingModify
forall a b. (a -> b) -> a -> b
$ String -> RDFVarBindingFilter
isMemberPropV String
"c")

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

-- | Ruleset for RDF inference.

rulesetRDF :: RDFRuleset
rulesetRDF :: RDFRuleset
rulesetRDF = Namespace -> [RDFFormula] -> [RDFRule] -> RDFRuleset
forall ex. Namespace -> [Formula ex] -> [Rule ex] -> Ruleset ex
makeRuleset Namespace
scopeRDF [RDFFormula]
axiomsRDF [RDFRule]
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 :: RDFFormula
rdfsa01 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDFS LName
"a01"
    Builder
"rdf:type           rdfs:domain rdfs:Resource ."

rdfsa02 :: RDFFormula
rdfsa02 :: RDFFormula
rdfsa02 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDFS LName
"a02"
    Builder
"rdf:type           rdfs:range  rdfs:Class ."

rdfsa03 :: RDFFormula
rdfsa03 :: RDFFormula
rdfsa03 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDFS LName
"a03"
    Builder
"rdfs:domain        rdfs:domain rdf:Property ."

rdfsa04 :: RDFFormula
rdfsa04 :: RDFFormula
rdfsa04 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDFS LName
"a04"
    Builder
"rdfs:domain        rdfs:range  rdfs:Class ."

rdfsa05 :: RDFFormula
rdfsa05 :: RDFFormula
rdfsa05 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDFS LName
"a05"
    Builder
"rdfs:range         rdfs:domain rdf:Property ."

rdfsa06 :: RDFFormula
rdfsa06 :: RDFFormula
rdfsa06 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDFS LName
"a06"
    Builder
"rdfs:range         rdfs:range  rdfs:Class ."

rdfsa07 :: RDFFormula
rdfsa07 :: RDFFormula
rdfsa07 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDFS LName
"a07"
    Builder
"rdfs:subPropertyOf rdfs:domain rdf:Property ."

rdfsa08 :: RDFFormula
rdfsa08 :: RDFFormula
rdfsa08 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDFS LName
"a08"
    Builder
"rdfs:subPropertyOf rdfs:range  rdf:Property ."

rdfsa09 :: RDFFormula
rdfsa09 :: RDFFormula
rdfsa09 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDFS LName
"a09"
    Builder
"rdfs:subClassOf    rdfs:domain rdfs:Class ."

rdfsa10 :: RDFFormula
rdfsa10 :: RDFFormula
rdfsa10 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDFS LName
"a10"
    Builder
"rdfs:subClassOf    rdfs:range  rdfs:Class ."

rdfsa11 :: RDFFormula
rdfsa11 :: RDFFormula
rdfsa11 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDFS LName
"a11"
    Builder
"rdf:subject        rdfs:domain rdf:Statement ."

rdfsa12 :: RDFFormula
rdfsa12 :: RDFFormula
rdfsa12 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDFS LName
"a12"
    Builder
"rdf:subject        rdfs:range  rdfs:Resource ."

rdfsa13 :: RDFFormula
rdfsa13 :: RDFFormula
rdfsa13 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDFS LName
"a13"
    Builder
"rdf:predicate      rdfs:domain rdf:Statement ."

rdfsa14 :: RDFFormula
rdfsa14 :: RDFFormula
rdfsa14 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDFS LName
"a14"
    Builder
"rdf:predicate      rdfs:range  rdfs:Resource ."

rdfsa15 :: RDFFormula
rdfsa15 :: RDFFormula
rdfsa15 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDFS LName
"a15"
    Builder
"rdf:object         rdfs:domain rdf:Statement ."

rdfsa16 :: RDFFormula
rdfsa16 :: RDFFormula
rdfsa16 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDFS LName
"a16"
    Builder
"rdf:object         rdfs:range  rdfs:Resource ."

rdfsa17 :: RDFFormula
rdfsa17 :: RDFFormula
rdfsa17 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDFS LName
"a17"
    Builder
"rdfs:member        rdfs:domain rdfs:Resource ."

rdfsa18 :: RDFFormula
rdfsa18 :: RDFFormula
rdfsa18 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDFS LName
"a18"
    Builder
"rdfs:member        rdfs:range  rdfs:Resource ."

rdfsa19 :: RDFFormula
rdfsa19 :: RDFFormula
rdfsa19 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDFS LName
"a19"
    Builder
"rdf:first          rdfs:domain rdf:List ."

rdfsa20 :: RDFFormula
rdfsa20 :: RDFFormula
rdfsa20 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDFS LName
"a20"
    Builder
"rdf:first          rdfs:range  rdfs:Resource ."

rdfsa21 :: RDFFormula
rdfsa21 :: RDFFormula
rdfsa21 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDFS LName
"a21"
    Builder
"rdf:rest           rdfs:domain rdf:List ."

rdfsa22 :: RDFFormula
rdfsa22 :: RDFFormula
rdfsa22 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDFS LName
"a22"
    Builder
"rdf:rest           rdfs:range  rdf:List ."

rdfsa23 :: RDFFormula
rdfsa23 :: RDFFormula
rdfsa23 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDFS LName
"a23"
    Builder
"rdfs:seeAlso       rdfs:domain rdfs:Resource ."

rdfsa24 :: RDFFormula
rdfsa24 :: RDFFormula
rdfsa24 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDFS LName
"a24"
    Builder
"rdfs:seeAlso       rdfs:range  rdfs:Resource ."

rdfsa25 :: RDFFormula
rdfsa25 :: RDFFormula
rdfsa25 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDFS LName
"a25"
    Builder
"rdfs:isDefinedBy   rdfs:domain rdfs:Resource ."

rdfsa26 :: RDFFormula
rdfsa26 :: RDFFormula
rdfsa26 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDFS LName
"a26"
    Builder
"rdfs:isDefinedBy   rdfs:range  rdfs:Resource ."

rdfsa27 :: RDFFormula
rdfsa27 :: RDFFormula
rdfsa27 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDFS LName
"a27"
    Builder
"rdfs:isDefinedBy   rdfs:subPropertyOf rdfs:seeAlso ."

rdfsa28 :: RDFFormula
rdfsa28 :: RDFFormula
rdfsa28 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDFS LName
"a28"
    Builder
"rdfs:comment       rdfs:domain rdfs:Resource ."

rdfsa29 :: RDFFormula
rdfsa29 :: RDFFormula
rdfsa29 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDFS LName
"a29"
    Builder
"rdfs:comment       rdfs:range  rdfs:Literal ."

rdfsa30 :: RDFFormula
rdfsa30 :: RDFFormula
rdfsa30 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDFS LName
"a30"
    Builder
"rdfs:label         rdfs:domain rdfs:Resource ."

rdfsa31 :: RDFFormula
rdfsa31 :: RDFFormula
rdfsa31 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDFS LName
"a31"
    Builder
"rdfs:label         rdfs:range  rdfs:Literal ."

rdfsa32 :: RDFFormula
rdfsa32 :: RDFFormula
rdfsa32 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDFS LName
"a32"
    Builder
"rdf:value          rdfs:domain rdfs:Resource ."

rdfsa33 :: RDFFormula
rdfsa33 :: RDFFormula
rdfsa33 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDFS LName
"a33"
    Builder
"rdf:value          rdfs:range  rdfs:Resource ."

rdfsa34 :: RDFFormula
rdfsa34 :: RDFFormula
rdfsa34 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDFS LName
"a34"
    Builder
"rdf:Alt            rdfs:subClassOf    rdfs:Container ."

rdfsa35 :: RDFFormula
rdfsa35 :: RDFFormula
rdfsa35 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDFS LName
"a35"
    Builder
"rdf:Bag            rdfs:subClassOf    rdfs:Container ."

rdfsa36 :: RDFFormula
rdfsa36 :: RDFFormula
rdfsa36 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDFS LName
"a36"
    Builder
"rdf:Seq            rdfs:subClassOf    rdfs:Container ."

rdfsa37 :: RDFFormula
rdfsa37 :: RDFFormula
rdfsa37 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDFS LName
"a37"
    Builder
"rdfs:ContainerMembershipProperty rdfs:subClassOf rdf:Property ."

rdfsa38 :: RDFFormula
rdfsa38 :: RDFFormula
rdfsa38 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDFS LName
"a38"
    Builder
"rdf:XMLLiteral     rdf:type           rdfs:Datatype ."

rdfsa39 :: RDFFormula
rdfsa39 :: RDFFormula
rdfsa39 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDFS LName
"a39"
    Builder
"rdf:XMLLiteral     rdfs:subClassOf    rdfs:Literal ."

rdfsa40 :: RDFFormula
rdfsa40 :: RDFFormula
rdfsa40 = Namespace -> LName -> Builder -> RDFFormula
makeFormula Namespace
scopeRDFS LName
"a40"
    Builder
"rdfs:Datatype      rdfs:subClassOf    rdfs:Class ."

axiomsRDFS :: [RDFFormula]
axiomsRDFS :: [RDFFormula]
axiomsRDFS =
    [          RDFFormula
rdfsa01, RDFFormula
rdfsa02, RDFFormula
rdfsa03, RDFFormula
rdfsa04
    , RDFFormula
rdfsa05, RDFFormula
rdfsa06, RDFFormula
rdfsa07, RDFFormula
rdfsa08, RDFFormula
rdfsa09
    , RDFFormula
rdfsa10, RDFFormula
rdfsa11, RDFFormula
rdfsa12, RDFFormula
rdfsa13, RDFFormula
rdfsa14
    , RDFFormula
rdfsa15, RDFFormula
rdfsa16, RDFFormula
rdfsa17, RDFFormula
rdfsa18, RDFFormula
rdfsa19
    , RDFFormula
rdfsa20, RDFFormula
rdfsa21, RDFFormula
rdfsa22, RDFFormula
rdfsa23, RDFFormula
rdfsa24
    , RDFFormula
rdfsa25, RDFFormula
rdfsa26, RDFFormula
rdfsa27, RDFFormula
rdfsa28, RDFFormula
rdfsa29
    , RDFFormula
rdfsa30, RDFFormula
rdfsa31, RDFFormula
rdfsa32, RDFFormula
rdfsa33, RDFFormula
rdfsa34
    , RDFFormula
rdfsa35, RDFFormula
rdfsa36, RDFFormula
rdfsa37, RDFFormula
rdfsa38, RDFFormula
rdfsa39
    , RDFFormula
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 :: RDFRule
rdfsr1 = Namespace
-> LName -> Builder -> Builder -> RDFVarBindingModify -> RDFRule
makeN3ClosureRule Namespace
scopeRDFS LName
"r1"
            Builder
"?x  ?a ?b . ?b rdf:_allocatedTo ?l . "
            Builder
"?b rdf:type rdfs:Literal ."
            (RDFVarBindingFilter -> RDFVarBindingModify
forall a b. VarBindingFilter a b -> VarBindingModify a b
makeVarFilterModify (RDFVarBindingFilter -> RDFVarBindingModify)
-> RDFVarBindingFilter -> RDFVarBindingModify
forall a b. (a -> b) -> a -> b
$ String -> RDFVarBindingFilter
isUntypedLitV String
"l" )

rdfsr2 :: RDFRule
rdfsr2 :: RDFRule
rdfsr2 = Namespace -> LName -> Builder -> Builder -> RDFRule
makeN3ClosureSimpleRule Namespace
scopeRDFS LName
"r2"
            Builder
"?x ?a ?y . ?a rdfs:domain ?z ."
            Builder
"?x rdf:type ?z ."

rdfsr3 :: RDFRule
rdfsr3 :: RDFRule
rdfsr3 = Namespace
-> LName -> Builder -> Builder -> RDFVarBindingModify -> RDFRule
makeN3ClosureRule Namespace
scopeRDFS LName
"r3"
            Builder
"?u ?a ?v . ?a rdfs:range ?z ."
            Builder
"?v rdf:type ?z ."
            (RDFVarBindingFilter -> RDFVarBindingModify
forall a b. VarBindingFilter a b -> VarBindingModify a b
makeVarFilterModify (RDFVarBindingFilter -> RDFVarBindingModify)
-> RDFVarBindingFilter -> RDFVarBindingModify
forall a b. (a -> b) -> a -> b
$ [RDFVarBindingFilter] -> RDFVarBindingFilter
requireAny [String -> RDFVarBindingFilter
isUriRefV String
"v",String -> RDFVarBindingFilter
isBlankV String
"v"])

rdfsr4a :: RDFRule
rdfsr4a :: RDFRule
rdfsr4a = Namespace -> LName -> Builder -> Builder -> RDFRule
makeN3ClosureSimpleRule Namespace
scopeRDFS LName
"r4a"
            Builder
"?x ?a ?y ."
            Builder
"?x rdf:type rdfs:Resource ."

rdfsr4b :: RDFRule
rdfsr4b :: RDFRule
rdfsr4b = Namespace
-> LName -> Builder -> Builder -> RDFVarBindingModify -> RDFRule
makeN3ClosureRule Namespace
scopeRDFS LName
"r4b"
            Builder
"?x ?a ?u ."
            Builder
"?u rdf:type rdfs:Resource ."
            (RDFVarBindingFilter -> RDFVarBindingModify
forall a b. VarBindingFilter a b -> VarBindingModify a b
makeVarFilterModify (RDFVarBindingFilter -> RDFVarBindingModify)
-> RDFVarBindingFilter -> RDFVarBindingModify
forall a b. (a -> b) -> a -> b
$ [RDFVarBindingFilter] -> RDFVarBindingFilter
requireAny [String -> RDFVarBindingFilter
isUriRefV String
"u",String -> RDFVarBindingFilter
isBlankV String
"u"])

rdfsr5 :: RDFRule
rdfsr5 :: RDFRule
rdfsr5  = Namespace -> LName -> Builder -> Builder -> RDFRule
makeN3ClosureSimpleRule Namespace
scopeRDFS LName
"r5"
            Builder
"?a rdfs:subPropertyOf ?b . ?b rdfs:subPropertyOf ?c ."
            Builder
"?a rdfs:subPropertyOf ?c ."

rdfsr6 :: RDFRule
rdfsr6 :: RDFRule
rdfsr6  = Namespace -> LName -> Builder -> Builder -> RDFRule
makeN3ClosureSimpleRule Namespace
scopeRDFS LName
"r6"
            Builder
"?x rdf:type rdf:Property ."
            Builder
"?x rdfs:subPropertyOf ?x ."

rdfsr7 :: RDFRule
rdfsr7 :: RDFRule
rdfsr7  = Namespace -> LName -> Builder -> Builder -> RDFRule
makeN3ClosureSimpleRule Namespace
scopeRDFS LName
"r7"
            Builder
"?x ?a ?y . ?a rdfs:subPropertyOf ?b ."
            Builder
"?x ?b ?y ."

rdfsr8 :: RDFRule
rdfsr8 :: RDFRule
rdfsr8  = Namespace -> LName -> Builder -> Builder -> RDFRule
makeN3ClosureSimpleRule Namespace
scopeRDFS LName
"r8"
            Builder
"?x rdf:type rdfs:Class ."
            Builder
"?x rdfs:subClassOf rdfs:Resource ."

rdfsr9 :: RDFRule
rdfsr9 :: RDFRule
rdfsr9  = Namespace -> LName -> Builder -> Builder -> RDFRule
makeN3ClosureSimpleRule Namespace
scopeRDFS LName
"r9"
            Builder
"?x rdfs:subClassOf ?y . ?a rdf:type ?x ."
            Builder
"?a rdf:type ?y ."

rdfsr10 :: RDFRule
rdfsr10 :: RDFRule
rdfsr10 = Namespace -> LName -> Builder -> Builder -> RDFRule
makeN3ClosureSimpleRule Namespace
scopeRDFS LName
"r10"
            Builder
"?x rdf:type rdfs:Class ."
            Builder
"?x rdfs:subClassOf ?x ."

rdfsr11 :: RDFRule
rdfsr11 :: RDFRule
rdfsr11 = Namespace -> LName -> Builder -> Builder -> RDFRule
makeN3ClosureSimpleRule Namespace
scopeRDFS LName
"r11"
            Builder
"?x rdfs:subClassOf ?y . ?y rdfs:subClassOf ?z ."
            Builder
"?x rdfs:subClassOf ?z ."

rdfsr12 :: RDFRule
rdfsr12 :: RDFRule
rdfsr12 = Namespace -> LName -> Builder -> Builder -> RDFRule
makeN3ClosureSimpleRule Namespace
scopeRDFS LName
"r12"
            Builder
"?x rdf:type rdfs:ContainerMembershipProperty ."
            Builder
"?x rdfs:subPropertyOf rdfs:member ."

rdfsr13 :: RDFRule
rdfsr13 :: RDFRule
rdfsr13 = Namespace -> LName -> Builder -> Builder -> RDFRule
makeN3ClosureSimpleRule Namespace
scopeRDFS LName
"r13"
            Builder
"?x rdf:type rdfs:Datatype ."
            Builder
"?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 :: RDFRule
rdfscp11 = Namespace
-> LName -> Builder -> Builder -> RDFVarBindingModify -> RDFRule
makeN3ClosureRule Namespace
scopeRDFS LName
"cp11"
            Builder
"?x  ?c ?y . "
            Builder
"?c rdf:type rdfs:ContainerMembershipProperty ."
            (RDFVarBindingFilter -> RDFVarBindingModify
forall a b. VarBindingFilter a b -> VarBindingModify a b
makeVarFilterModify (RDFVarBindingFilter -> RDFVarBindingModify)
-> RDFVarBindingFilter -> RDFVarBindingModify
forall a b. (a -> b) -> a -> b
$ String -> RDFVarBindingFilter
isMemberPropV String
"c")

rdfscp12 :: RDFRule
rdfscp12 :: RDFRule
rdfscp12 = Namespace
-> LName -> Builder -> Builder -> RDFVarBindingModify -> RDFRule
makeN3ClosureRule Namespace
scopeRDFS LName
"cp12"
            Builder
"?c  ?p ?y . "
            Builder
"?c rdf:type rdfs:ContainerMembershipProperty ."
            (RDFVarBindingFilter -> RDFVarBindingModify
forall a b. VarBindingFilter a b -> VarBindingModify a b
makeVarFilterModify (RDFVarBindingFilter -> RDFVarBindingModify)
-> RDFVarBindingFilter -> RDFVarBindingModify
forall a b. (a -> b) -> a -> b
$ String -> RDFVarBindingFilter
isMemberPropV String
"c")

rdfscp13 :: RDFRule
rdfscp13 :: RDFRule
rdfscp13 = Namespace
-> LName -> Builder -> Builder -> RDFVarBindingModify -> RDFRule
makeN3ClosureRule Namespace
scopeRDFS LName
"cp13"
            Builder
"?x  ?p ?c . "
            Builder
"?c rdf:type rdfs:ContainerMembershipProperty ."
            (RDFVarBindingFilter -> RDFVarBindingModify
forall a b. VarBindingFilter a b -> VarBindingModify a b
makeVarFilterModify (RDFVarBindingFilter -> RDFVarBindingModify)
-> RDFVarBindingFilter -> RDFVarBindingModify
forall a b. (a -> b) -> a -> b
$ String -> RDFVarBindingFilter
isMemberPropV String
"c")

rdfscp21 :: RDFRule
rdfscp21 :: RDFRule
rdfscp21 = Namespace
-> LName -> Builder -> Builder -> RDFVarBindingModify -> RDFRule
makeN3ClosureRule Namespace
scopeRDFS LName
"cp21"
            Builder
"?x  ?c ?y . "
            Builder
"?c rdfs:domain rdfs:Resource ."
            (RDFVarBindingFilter -> RDFVarBindingModify
forall a b. VarBindingFilter a b -> VarBindingModify a b
makeVarFilterModify (RDFVarBindingFilter -> RDFVarBindingModify)
-> RDFVarBindingFilter -> RDFVarBindingModify
forall a b. (a -> b) -> a -> b
$ String -> RDFVarBindingFilter
isMemberPropV String
"c")

rdfscp22 :: RDFRule
rdfscp22 :: RDFRule
rdfscp22 = Namespace
-> LName -> Builder -> Builder -> RDFVarBindingModify -> RDFRule
makeN3ClosureRule Namespace
scopeRDFS LName
"cp22"
            Builder
"?c  ?p ?y . "
            Builder
"?c rdfs:domain rdfs:Resource ."
            (RDFVarBindingFilter -> RDFVarBindingModify
forall a b. VarBindingFilter a b -> VarBindingModify a b
makeVarFilterModify (RDFVarBindingFilter -> RDFVarBindingModify)
-> RDFVarBindingFilter -> RDFVarBindingModify
forall a b. (a -> b) -> a -> b
$ String -> RDFVarBindingFilter
isMemberPropV String
"c")

rdfscp23 :: RDFRule
rdfscp23 :: RDFRule
rdfscp23 = Namespace
-> LName -> Builder -> Builder -> RDFVarBindingModify -> RDFRule
makeN3ClosureRule Namespace
scopeRDFS LName
"cp23"
            Builder
"?x  ?p ?c . "
            Builder
"?c rdfs:domain rdfs:Resource ."
            (RDFVarBindingFilter -> RDFVarBindingModify
forall a b. VarBindingFilter a b -> VarBindingModify a b
makeVarFilterModify (RDFVarBindingFilter -> RDFVarBindingModify)
-> RDFVarBindingFilter -> RDFVarBindingModify
forall a b. (a -> b) -> a -> b
$ String -> RDFVarBindingFilter
isMemberPropV String
"c")

rdfscp31 :: RDFRule
rdfscp31 :: RDFRule
rdfscp31 = Namespace
-> LName -> Builder -> Builder -> RDFVarBindingModify -> RDFRule
makeN3ClosureRule Namespace
scopeRDFS LName
"cp31"
            Builder
"?x  ?c ?y . "
            Builder
"?c rdfs:range rdfs:Resource ."
            (RDFVarBindingFilter -> RDFVarBindingModify
forall a b. VarBindingFilter a b -> VarBindingModify a b
makeVarFilterModify (RDFVarBindingFilter -> RDFVarBindingModify)
-> RDFVarBindingFilter -> RDFVarBindingModify
forall a b. (a -> b) -> a -> b
$ String -> RDFVarBindingFilter
isMemberPropV String
"c")

rdfscp32 :: RDFRule
rdfscp32 :: RDFRule
rdfscp32 = Namespace
-> LName -> Builder -> Builder -> RDFVarBindingModify -> RDFRule
makeN3ClosureRule Namespace
scopeRDFS LName
"cp32"
            Builder
"?c  ?p ?y . "
            Builder
"?c rdfs:range rdfs:Resource ."
            (RDFVarBindingFilter -> RDFVarBindingModify
forall a b. VarBindingFilter a b -> VarBindingModify a b
makeVarFilterModify (RDFVarBindingFilter -> RDFVarBindingModify)
-> RDFVarBindingFilter -> RDFVarBindingModify
forall a b. (a -> b) -> a -> b
$ String -> RDFVarBindingFilter
isMemberPropV String
"c")

rdfscp33 :: RDFRule
rdfscp33 :: RDFRule
rdfscp33 = Namespace
-> LName -> Builder -> Builder -> RDFVarBindingModify -> RDFRule
makeN3ClosureRule Namespace
scopeRDFS LName
"cp33"
            Builder
"?x  ?p ?c . "
            Builder
"?c rdfs:range rdfs:Resource ."
            (RDFVarBindingFilter -> RDFVarBindingModify
forall a b. VarBindingFilter a b -> VarBindingModify a b
makeVarFilterModify (RDFVarBindingFilter -> RDFVarBindingModify)
-> RDFVarBindingFilter -> RDFVarBindingModify
forall a b. (a -> b) -> a -> b
$ String -> RDFVarBindingFilter
isMemberPropV String
"c")

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

-- | Ruleset for RDFS inference.

rulesetRDFS :: RDFRuleset
rulesetRDFS :: RDFRuleset
rulesetRDFS = Namespace -> [RDFFormula] -> [RDFRule] -> RDFRuleset
forall ex. Namespace -> [Formula ex] -> [Rule ex] -> Ruleset ex
makeRuleset Namespace
scopeRDFS [RDFFormula]
axiomsRDFS [RDFRule]
rulesRDFS

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

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

axiomsRDFD :: [RDFFormula]
axiomsRDFD :: [RDFFormula]
axiomsRDFD =
    [
    ]

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

--  RDFD closure rules from semantics document, section 7.4

--  Infer type of datatyped literal
--
rdfdr1 :: RDFRule
rdfdr1 :: RDFRule
rdfdr1 = Namespace
-> LName -> Builder -> Builder -> RDFVarBindingModify -> RDFRule
makeN3ClosureRule Namespace
scopeRDFD LName
"r1"
            Builder
"?d rdf:type rdfs:Datatype . ?a ?p ?l . ?b rdf:_allocatedTo ?l . "
            Builder
"?b rdf:type ?d ."
            (RDFVarBindingFilter -> RDFVarBindingModify
forall a b. VarBindingFilter a b -> VarBindingModify a b
makeVarFilterModify (RDFVarBindingFilter -> RDFVarBindingModify)
-> RDFVarBindingFilter -> RDFVarBindingModify
forall a b. (a -> b) -> a -> b
$ String -> String -> RDFVarBindingFilter
isDatatypedV String
"d" String
"l")

--  Equivalent literals with same datatype:
--  (generate canonical form, or operate in proof mode only)
--
rdfdr2 :: RDFRule
rdfdr2 :: RDFRule
rdfdr2 = Namespace
-> LName -> Builder -> Builder -> RDFVarBindingModify -> RDFRule
makeN3ClosureRule Namespace
scopeRDFD LName
"r2"
            Builder
"?d rdf:type rdfs:Datatype . ?a ?p ?s ."
            Builder
"?a ?p ?t ."
            (String -> String -> String -> String -> RDFVarBindingModify
valueSame String
"s" String
"d" String
"t" String
"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 :: RDFRule
rdfdr3 = Namespace
-> LName
-> Builder
-> Builder
-> RDFVarBindingModify
-> RDFVarBindingModify
-> RDFRule
makeN3ClosureModifyRule Namespace
scopeRDFD LName
"r3"
            ( Builder
"?d rdf:type rdfs:Datatype . ?e rdf:type rdfs:Datatype . " Builder -> Builder -> Builder
forall a. Monoid a => a -> a -> a
`mappend`
              Builder
"?a ?p ?s ." )
            Builder
"?a ?p ?t ."
            (RDFVarBindingFilter -> RDFVarBindingModify
forall a b. VarBindingFilter a b -> VarBindingModify a b
makeVarFilterModify (RDFVarBindingFilter -> RDFVarBindingModify)
-> RDFVarBindingFilter -> RDFVarBindingModify
forall a b. (a -> b) -> a -> b
$ String -> String -> RDFVarBindingFilter
isDatatypedV String
"s" String
"d")
            (String -> String -> String -> String -> RDFVarBindingModify
valueSame String
"s" String
"d" String
"t" String
"e")

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

-- | Ruleset for RDFD (datatyping) inference.
--
rulesetRDFD :: RDFRuleset
rulesetRDFD :: RDFRuleset
rulesetRDFD = Namespace -> [RDFFormula] -> [RDFRule] -> RDFRuleset
forall ex. Namespace -> [Formula ex] -> [Rule ex] -> Ruleset ex
makeRuleset Namespace
scopeRDFD [RDFFormula]
axiomsRDFD [RDFRule]
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
--
--------------------------------------------------------------------------------