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