-------------------------------------------------------------------------------- -- See end of this file for licence information. -------------------------------------------------------------------------------- -- | -- Module : RDFProofContextTest -- Copyright : (c) 2003, Graham Klyne, 2009 Vasili I Galchin, 2011 Douglas Burke -- License : GPL V2 -- -- Maintainer : Douglas Burke -- Stability : experimental -- Portability : H98 -- -- This module contains RDF proof-checking test cases based on the RDF -- semantics specifications, as capured in module RDFProofContext. -- -------------------------------------------------------------------------------- module Main where import Swish.RDF.BuiltInMap ( rdfRulesetMap, allRulesets ) import Swish.RDF.RDFProofContext ( rulesetRDF , rulesetRDFS , rulesetRDFD ) import Swish.RDF.RDFProof ( RDFProof, RDFProofStep , makeRDFProof, makeRDFProofStep ) import Swish.RDF.RDFRuleset ( RDFFormula, RDFRule, RDFRuleset , nullRDFFormula , makeRDFFormula ) import Swish.RDF.RDFGraph ( RDFGraph ) import Swish.RDF.RDFGraphShowM() import Swish.RDF.Proof ( Step(..) , checkProof, checkStep , explainProof) import Swish.RDF.Ruleset ( getContextAxiom, getContextRule ) import Swish.RDF.Rule ( Formula(..), Rule(..) , nullFormula, nullRule ) import Swish.Utils.Namespace ( Namespace(..), ScopedName(..) ) import Swish.Utils.LookupMap ( mapFindMaybe ) import Swish.RDF.Vocabulary ( namespaceRDF , namespaceRDFS , namespaceRDFD , namespaceXSD , namespaceXsdType , scopeRDF , scopeRDFS , scopeRDFD ) import Test.HUnit ( Test(TestCase,TestList) , assertBool, assertEqual , runTestTT ) import Data.Maybe ( isJust, isNothing, fromJust, fromMaybe ) -- misc helpers test :: String -> Bool -> Test test lab tst = TestCase $ assertBool lab tst testEq :: (Eq a, Show a) => String -> a -> a -> Test testEq lab e a = TestCase $ assertEqual lab e a testJe :: (Eq a, Show a) => String -> a -> Maybe a -> Test testJe lab e a = TestList [ TestCase $ assertBool lab (isJust a) , TestCase $ assertEqual lab e (fromJust a) ] testJl :: (Eq a, Show a) => String -> Int -> Maybe [a] -> Test testJl lab e a = TestList [ TestCase $ assertBool lab (isJust a) , TestCase $ assertEqual lab e (length (fromJust a)) ] testNo :: (Eq a, Show a) => String -> [[a]] -> Test testNo lab a = TestCase $ assertBool lab (null a) testGr :: String -> RDFGraph -> [RDFGraph] -> Test testGr lab eg a = TestCase $ assertBool lab (eg `elem` a) -- testProof "rdfProof01" True rdfProof01 testProof :: String -> Bool -> RDFProof -> Test testProof lab valid proof = TestList [ TestCase $ assertEqual lab valid (checkProof proof) , TestCase $ assertBool (lab++": "++ex) (valid == (isNothing $ expl)) ] where expl = explainProof proof ex = fromMaybe "(Proof OK)" expl -- testProofStep "rdfStep01" True [rules] [antes] rdfStep01 testProofStep :: String -> Bool -> [RDFRule] -> [RDFGraph] -> Step RDFGraph -> Test testProofStep lab valid rules antes step = TestCase $ assertEqual lab valid (checkStep rules antes step) -- Various support methods makeFormula :: Namespace -> String -> String -> RDFFormula makeFormula scope local gr = makeRDFFormula scope local (prefix++gr) getRule :: String -> RDFRule getRule nam = getContextRule (makeSName nam) nullRule $ rdfdContext++[rulesetXsdInt,rulesetXsdStr] getAxiom :: String -> RDFFormula getAxiom nam = getContextAxiom (makeSName nam) nullRDFFormula rdfdContext makeSName :: String -> ScopedName makeSName nam = ScopedName ns loc where (pre,_:loc) = break (==':') nam ns = case pre of "rs_rdf" -> scopeRDF "rs_rdfs" -> scopeRDFS "rs_rdfd" -> scopeRDFD "xsd_integer" -> (namespaceXsdType "integer") "xsd_string" -> (namespaceXsdType "string") _ -> error ("makeSName: Unrecognized prefix in rule name: "++nam) -- Common definitions prefix :: String prefix = "@prefix rdf: <" ++ nsURI namespaceRDF ++ "> . \n" ++ "@prefix rdfs: <" ++ nsURI namespaceRDFS ++ "> . \n" ++ "@prefix rdfd: <" ++ nsURI namespaceRDFD ++ "> . \n" ++ "@prefix xsd: <" ++ nsURI namespaceXSD ++ "> . \n" ++ "@prefix ex: . \n" ++ " \n" scopeex :: Namespace scopeex = Namespace "ex" "http://id.ninebynine.org/wip/2003/RDFProofCheck#" rdfContext, rdfsContext, rdfdContext, xsdintContext, xsdstrContext :: [RDFRuleset] rdfContext = [ rulesetRDF ] rdfsContext = [ rulesetRDF, rulesetRDFS ] rdfdContext = [ rulesetRDF, rulesetRDFS, rulesetRDFD ] xsdintContext = [ rulesetRDF, rulesetRDFS, rulesetRDFD, rulesetXsdInt ] xsdstrContext = [ rulesetRDF, rulesetRDFS, rulesetRDFD, rulesetXsdStr ] rulesetXsdInt, rulesetXsdStr :: RDFRuleset rulesetXsdInt = fromJust $ mapFindMaybe (namespaceXsdType "integer") rdfRulesetMap rulesetXsdStr = fromJust $ mapFindMaybe (namespaceXsdType "string") rdfRulesetMap ------------------------ -- RDF/S rule tests ------------------------ -- -- These tests aim to exercise the specific closure rule constructs -- that are used by the RDF/S rules. They have been prepared as a -- regression test for a refactoring of the variable binding -- filtering and modification logic. -- Simple rule test - forward and backward chaining -- -- rdfr1 = "?x ?a ?y ." => "?a rdf:type rdf:Property ." -- rdfr1 :: RDFRule rdfr1 = getRule "rs_rdf:r1" ant01, con01, bwd01 :: RDFGraph ant01 = formExpr $ makeFormula scopeex "ant01" $ "ex:s ex:p1 ex:o1 ; ex:p2 ex:o2 ." con01 = formExpr $ makeFormula scopeex "con01" $ "ex:p1 rdf:type rdf:Property ." ++ "ex:p2 rdf:type rdf:Property ." bwd01 = formExpr $ makeFormula scopeex "bwd01a" $ "_:s1 ex:p1 _:o1 . " ++ "_:s2 ex:p2 _:o2 . " -- Simple rule test - no match forward or backward -- -- rdfsr2 = "?x ?a ?y . ?a rdfs:domain ?z ." => "?x rdf:type ?z ." -- rdfsr2 :: RDFRule rdfsr2 = getRule "rs_rdfs:r2" ant02, con02 :: RDFGraph ant02 = formExpr $ makeFormula scopeex "ant02" $ "ex:s ex:p1 ex:o1 . ex:p2 rdfs:domain ex:d2 ." con02 = formExpr $ makeFormula scopeex "con02" $ "ex:s ex:p1 ex:o1 . ex:p2 rdfs:domain ex:d2 ." -- Rule with literal test and "allocateTo": -- match forward, but not backward -- -- This is a two-part rule: (a) apply rdflg, (b) apply rdfr2 -- -- rdflg = "?x ?a ?l . " => "?x ?a ?b . ?b rdf:_allocatedTo ?l ." -- where: -- (isLiteral "?l") -- (allocateTo "?b" "?l") -- -- rdfr2 = "?x ?a ?l . ?b rdf:_allocatedTo ?l . " -- => "?b rdf:type rdf:XMLLiteral ." -- where: -- (isXMLLit "?l") -- rdflg, rdfr2 :: RDFRule rdflg = getRule "rs_rdf:lg" rdfr2 = getRule "rs_rdf:r2" ant03, con03lg, con03r2 :: RDFGraph ant03 = formExpr $ makeFormula scopeex "ant03" $ "ex:s ex:p1 \"lit1\"^^rdf:XMLLiteral ; " ++ " ex:p2a \"lit2\"^^rdf:XMLLiteral ; " ++ " ex:p2b \"lit2\"^^rdf:XMLLiteral ." con03lg = formExpr $ makeFormula scopeex "con03" $ "ex:s ex:p1 _:l1 ; ex:p2a _:l2; ex:p2b _:l2 ." ++ "_:l1 rdf:_allocatedTo \"lit1\"^^rdf:XMLLiteral ." ++ "_:l2 rdf:_allocatedTo \"lit2\"^^rdf:XMLLiteral ." con03r2 = formExpr $ makeFormula scopeex "con03" $ "_:l1 rdf:type rdf:XMLLiteral ." ++ "_:l2 rdf:type rdf:XMLLiteral ." -- Rule with member property test, match forwards and backwards -- rdfcp1 = "?x ?c ?y . " => "?c rdf:type rdf:Property ." -- where: -- (isMemberProp "?c") -- rdfcp :: RDFRule rdfcp = getRule "rs_rdf:cp1" ant04, con04, bwd04 :: RDFGraph ant04 = formExpr $ makeFormula scopeex "ant04" $ "ex:s rdf:_123 ex:o1 ; " ++ " rdf:_2 ex:o2 . " con04 = formExpr $ makeFormula scopeex "con04" $ "rdf:_123 rdf:type rdf:Property ." ++ "rdf:_2 rdf:type rdf:Property ." bwd04 = formExpr $ makeFormula scopeex "bwd04a" $ "_:s1 rdf:_123 _:o1 . " ++ "_:s2 rdf:_2 _:o2 . " -- Rule with disjunction test, match forwards and backwards -- -- rdfsr3 = "?x ?a ?u . ?a rdfs:range ?z ." => "?u rdf:type ?z ." -- where: -- (requireAny [isUriRef "?u",isBlank "?u"]) -- rdfsr3 :: RDFRule rdfsr3 = getRule "rs_rdfs:r3" ant05, con05, bwd05 :: RDFGraph ant05 = formExpr $ makeFormula scopeex "ant05" $ "ex:s ex:p1 ex:o1 ; " ++ " ex:p2 _:o2 . " ++ "ex:p1 rdfs:range ex:pr1 . " ++ "ex:p2 rdfs:range ex:pr2 . " con05 = formExpr $ makeFormula scopeex "con05" $ "ex:o1 rdf:type ex:pr1 ." ++ "_:o2 rdf:type ex:pr2 ." bwd05 = formExpr $ makeFormula scopeex "bwd05a" $ "_:s1 _:p1 ex:o1 . " ++ "_:s2 _:p2 _:o2 . " ++ "_:p1 rdfs:range ex:pr1 . " ++ "_:p2 rdfs:range ex:pr2 . " -- Rule with disjunction test, fail forwards -- -- rdfsr3 = "?x ?a ?u . ?a rdfs:range ?z ." => "?u rdf:type ?z ." -- where: -- (requireAny [isUriRef "?u",isBlank "?u"]) -- ant06, con06, bwd06, chk06 :: RDFGraph ant06 = formExpr $ makeFormula scopeex "ant06" $ "ex:s ex:p1 \"lit1\" . " ++ "ex:p1 rdfs:range ex:pr1 . " con06 = formExpr $ makeFormula scopeex "con06" $ "_:o1 rdf:type ex:pr1 ." bwd06 = formExpr $ makeFormula scopeex "bwd06a" $ "_:s1 _:p1 _:o1 . " ++ "_:p1 rdfs:range ex:pr1 . " chk06 = formExpr $ makeFormula scopeex "bwd06a" $ "_:s1 _:p1 \"lit1\" . " ++ "_:p1 rdfs:range ex:pr1 . " -- Collected rule tests testRules :: Test testRules = TestList [ testEq "testRule01a" "rs_rdf:r1" (show $ ruleName rdfr1) , testEq "testRule01b" [con01] (fwdApply rdfr1 [ant01]) , testEq "testRule01c" [[bwd01]] (bwdApply rdfr1 con01) , test "testRule01d" (checkInference rdfr1 [ant01] con01) , test "testRule01e" (checkInference rdfr1 [bwd01] con01) , testEq "testRule02a" "rs_rdfs:r2" (show $ ruleName rdfsr2) , testEq "testRule02b" [] (fwdApply rdfsr2 [ant02]) , testEq "testRule02c" [] (bwdApply rdfsr2 con02) , testEq "testRule02d" False (checkInference rdfsr2 [ant02] con02) , testEq "testRule03a" "rs_rdf:lg" (show $ ruleName rdflg) , testEq "testRule03b" "rs_rdf:r2" (show $ ruleName rdfr2) , testEq "testRule03c" [con03lg] (fwdApply rdflg [ant03]) , testEq "testRule03d" [] (bwdApply rdflg con03lg) , test "testRule03e" (checkInference rdflg [ant03] con03lg) , testEq "testRule03f" [con03r2] (fwdApply rdfr2 [con03lg]) , testEq "testRule03g" [] (bwdApply rdfr2 con03r2) , test "testRule03h" (checkInference rdfr2 [con03lg] con03r2) , testEq "testRule04a" "rs_rdf:cp1" (show $ ruleName rdfcp) , testEq "testRule04b" [con04] (fwdApply rdfcp [ant04]) , testEq "testRule04c" [[bwd04]] (bwdApply rdfcp con04) , test "testRule04d" (checkInference rdfcp [ant04] con04) , test "testRule01e" (checkInference rdfcp [bwd04] con04) , testEq "testRule05a" "rs_rdfs:r3" (show $ ruleName rdfsr3) , testEq "testRule05b" [con05] (fwdApply rdfsr3 [ant05]) , testEq "testRule05c" [[bwd05]] (bwdApply rdfsr3 con05) , test "testRule05d" (checkInference rdfsr3 [ant05] con05) , test "testRule01e" (checkInference rdfsr3 [bwd05] con05) , testEq "testRule06a" "rs_rdfs:r3" (show $ ruleName rdfsr3) , testEq "testRule06b" [] (fwdApply rdfsr3 [ant06]) , testEq "testRule06c" [[bwd06]] (bwdApply rdfsr3 con06) , testEq "testRule06d" False (checkInference rdfsr3 [ant06] con06) , testEq "testRule06e" True (checkInference rdfsr3 [bwd06] con06) , testEq "testRule06e" False (checkInference rdfsr3 [chk06] con06) ] ------------------------ -- Complete proof tests ------------------------ -- -- These are a few tests of complete RDF proof chains based on the -- RDF semantic rules. -- RDF entailment proof checks rdfBase01, rdfGoal01 :: RDFFormula rdfBase01 = makeFormula scopeex "rdfBase01" "ex:s ex:p ex:o ." rdfGoal01 = makeFormula scopeex "rdfGoal01" "ex:p rdf:type rdf:Property ." rdfStep01a :: RDFProofStep rdfStep01a = makeRDFProofStep (getRule "rs_rdf:r1") [rdfBase01] rdfGoal01 rdfProof01 :: RDFProof rdfProof01 = makeRDFProof rdfsContext rdfBase01 rdfGoal01 [ rdfStep01a ] rdfBase02, rdfCon02a, rdfGoal02 :: RDFFormula rdfBase02 = makeFormula scopeex "rdfBase02" $ "ex:s ex:p \"l1\"^^rdf:XMLLiteral ." rdfCon02a = makeFormula scopeex "rdfStep02a" $ "ex:s ex:p _:lll . " ++ "_:lll rdf:_allocatedTo \"l1\"^^rdf:XMLLiteral . " rdfGoal02 = makeFormula scopeex "rdfGoal02" $ "_:lll rdf:type rdf:XMLLiteral . " rdfStep02a, rdfStep02b :: RDFProofStep rdfStep02a = makeRDFProofStep (getRule "rs_rdf:lg") [rdfBase02] rdfCon02a rdfStep02b = makeRDFProofStep (getRule "rs_rdf:r2") [rdfCon02a] rdfGoal02 rdfProof02 :: RDFProof rdfProof02 = makeRDFProof rdfsContext rdfBase02 rdfGoal02 [ rdfStep02a, rdfStep02b ] rdfBase03, rdfCon03a, rdfGoal03 :: RDFFormula rdfBase03 = makeFormula scopeex "rdfBase03" $ "ex:s ex:p ex:o ." rdfCon03a = makeFormula scopeex "rdfStep03a" $ "ex:s ex:p _:lll . " ++ "_:lll rdf:_allocatedTo \"l1\"^^rdf:XMLLiteral . " rdfGoal03 = makeFormula scopeex "rdfGoal03" $ "_:lll rdf:type rdf:XMLLiteral . " rdfStep03a, rdfStep03b :: RDFProofStep rdfStep03a = makeRDFProofStep (getRule "rs_rdf:lg") [rdfBase03] rdfCon03a rdfStep03b = makeRDFProofStep (getRule "rs_rdf:r2") [rdfCon03a] rdfGoal03 rdfProof03 :: RDFProof rdfProof03 = makeRDFProof rdfsContext rdfBase03 rdfGoal03 [ rdfStep03a, rdfStep03b ] rdfBase04, rdfGoal04 :: RDFFormula rdfBase04 = makeFormula scopeex "rdfBase04" "ex:s ex:p ex:o ." rdfGoal04 = makeFormula scopeex "rdfGoal04" "_:s ex:p _:o ." rdfStep04a :: RDFProofStep rdfStep04a = makeRDFProofStep (getRule "rs_rdf:se") [rdfBase04] rdfGoal04 rdfProof04 :: RDFProof rdfProof04 = makeRDFProof rdfsContext rdfBase04 rdfGoal04 [ rdfStep04a ] rdfBase05 :: RDFFormula rdfBase05 = makeFormula scopeex "rdfBase05" $ "ex:s ex:p rdf:nil ." rdfStep05a :: RDFProofStep rdfStep05a = makeRDFProofStep (getRule "rs_rdf:r1") [rdfBase05] rdfCons05a rdfCons05a :: RDFFormula rdfCons05a = makeFormula scopeex "rdfCons05a" $ "ex:p rdf:type rdf:Property ." rdfStep05b :: RDFProofStep rdfStep05b = makeRDFProofStep (getRule "rs_rdf:se") [rdfBase05,rdfCons05a,(getAxiom "rs_rdf:a8")] rdfGoal05 rdfGoal05 :: RDFFormula rdfGoal05 = makeFormula scopeex "rdfGoal05" $ "ex:s _:p _:n ." ++ "_:p rdf:type rdf:Property ." ++ "_:n rdf:type rdf:List ." rdfProof05 :: RDFProof rdfProof05 = makeRDFProof rdfsContext rdfBase05 rdfGoal05 [ rdfStep05a, rdfStep05b ] -- Swap rdfProof05 proof steps: rdfProof06 :: RDFProof rdfProof06 = makeRDFProof rdfsContext rdfBase05 rdfGoal05 [ rdfStep05b, rdfStep05a ] -- Proof using rdfsr1 and rdfsub -- -- ex:s1 ex:p1 "lll" -- ex:s2 ex:p2 "lll" -- => -- ex:s1 ex:p1 _:l -- ex:s2 ex:p2 _:l -- _:l rdf:type rdfs:Literal rdfBase07 :: RDFFormula rdfBase07 = makeFormula scopeex "rdfBase07" $ "ex:s1 ex:p1 \"lll\" ." ++ "ex:s2 ex:p2 \"lll\" ." ++ "ex:s3 ex:p3 \"mmm\" ." rdfStep07a :: RDFProofStep rdfStep07a = makeRDFProofStep (getRule "rs_rdf:lg") [rdfBase07] rdfCons07a rdfCons07a :: RDFFormula rdfCons07a = makeFormula scopeex "rdfCons07a" $ "ex:s1 ex:p1 _:l ." ++ "ex:s2 ex:p2 _:l ." ++ "_:l rdf:_allocatedTo \"lll\" ." ++ "ex:s3 ex:p3 _:m ." ++ "_:m rdf:_allocatedTo \"mmm\" ." rdfStep07b :: RDFProofStep rdfStep07b = makeRDFProofStep (getRule "rs_rdfs:r1") [rdfCons07a] rdfCons07b rdfCons07b :: RDFFormula rdfCons07b = makeFormula scopeex "rdfCons07a" $ "_:l rdf:type rdfs:Literal ." ++ "_:m rdf:type rdfs:Literal ." rdfStep07c :: RDFProofStep rdfStep07c = makeRDFProofStep (getRule "rs_rdf:sub") [rdfCons07a,rdfCons07b] rdfGoal07 rdfGoal07 :: RDFFormula rdfGoal07 = makeFormula scopeex "rdfGoal07" $ "ex:s1 ex:p1 _:l ." ++ "ex:s2 ex:p2 _:l ." ++ "_:l rdf:type rdfs:Literal ." rdfProof07 :: RDFProof rdfProof07 = makeRDFProof rdfsContext rdfBase07 rdfGoal07 [ rdfStep07a, rdfStep07b, rdfStep07c ] -- Proof of: -- rdf:_123 rdfs:supPropertyOf rdfs:member rdfBase08 :: RDFFormula rdfBase08 = makeFormula scopeex "rdfBase08" $ "ex:s1 rdf:_123 ex:o ." rdfStep08a :: RDFProofStep rdfStep08a = makeRDFProofStep (getRule "rs_rdfs:cp1") [rdfBase08] rdfCons08a rdfCons08a :: RDFFormula rdfCons08a = makeFormula scopeex "rdfCons08a" $ "rdf:_123 rdf:type rdfs:ContainerMembershipProperty ." rdfStep08b :: RDFProofStep rdfStep08b = makeRDFProofStep (getRule "rs_rdfs:r12") [rdfCons08a] rdfGoal08 rdfGoal08 :: RDFFormula rdfGoal08 = makeFormula scopeex "rdfCons08b" $ "rdf:_123 rdfs:subPropertyOf rdfs:member ." rdfProof08 :: RDFProof rdfProof08 = makeRDFProof rdfsContext rdfBase08 rdfGoal08 [ rdfStep08a, rdfStep08b ] -- Proof of: -- ex:s ex:p "010"^^xsd:Integer . -- => -- ex:s ex:p "10"^^xsd:Integer . -- ex:s ex:p _:b -- _:b rdf:type xsd:integer . rdfAxiomIntDt :: RDFFormula rdfAxiomIntDt = getContextAxiom (ScopedName (namespaceXsdType "integer") "dt") nullFormula allRulesets rdfAxiom09 :: Test rdfAxiom09 = testEq "rdfAxiom09" "xsd_integer:dt" $ show (formName rdfAxiomIntDt) rdfBase09 :: RDFFormula rdfBase09 = makeFormula scopeex "rdfBase09" $ "ex:s ex:p \"010\"^^xsd:integer ." rdfStep09a :: RDFProofStep rdfStep09a = makeRDFProofStep (getRule "rs_rdfd:r2") [rdfAxiomIntDt,rdfBase09] rdfCons09a rdfCons09a :: RDFFormula rdfCons09a = makeFormula scopeex "rdfCons09a" $ "ex:s ex:p \"10\"^^xsd:integer ." rdfStep09b :: RDFProofStep rdfStep09b = makeRDFProofStep (getRule "rs_rdf:lg") [rdfCons09a] rdfCons09b rdfCons09b :: RDFFormula rdfCons09b = makeFormula scopeex "rdfCons09b" $ "ex:s ex:p _:l ." ++ "_:l rdf:_allocatedTo \"10\"^^xsd:integer ." rdfStep09c :: RDFProofStep rdfStep09c = makeRDFProofStep (getRule "rs_rdfd:r1") [rdfAxiomIntDt,rdfCons09a,rdfCons09b] rdfCons09c rdfCons09c :: RDFFormula rdfCons09c = makeFormula scopeex "rdfCons09c" $ "_:l rdf:type xsd:integer ." rdfStep09d :: RDFProofStep rdfStep09d = makeRDFProofStep (getRule "rs_rdf:sub") [rdfCons09a,rdfCons09b,rdfCons09c] rdfGoal09 rdfGoal09 :: RDFFormula rdfGoal09 = makeFormula scopeex "rdfGoal09" $ "ex:s ex:p \"10\"^^xsd:integer ." ++ "_:l rdf:_allocatedTo \"10\"^^xsd:integer ." ++ "_:l rdf:type xsd:integer ." rdfProof09 :: RDFProof rdfProof09 = makeRDFProof xsdintContext rdfBase09 rdfGoal09 [ rdfStep09a, rdfStep09b, rdfStep09c, rdfStep09d ] {- test data p09t1 = fwdApply (getRule "rs_rdfd:r2") [(formExpr rdfAxiomIntDt),(formExpr rdfBase09)] p09sh = putStrLn ("\n"++showProof "\n" rdfProof09++"\n") -} -- Proof of: -- ex:s ex:p "abc" . -- ex:s ex:p "def"^^xsd:string . -- => -- ex:s ex:p "abc"^^xsd:string . -- ex:s ex:p "def" . -- xsd:string rdf:type rdfs:Datatype . rdfAxiomStrDt :: RDFFormula rdfAxiomStrDt = getContextAxiom (ScopedName (namespaceXsdType "string") "dt") nullFormula allRulesets rdfAxiom10 :: Test rdfAxiom10 = testEq "rdfAxiom10" "xsd_string:dt" $ show (formName rdfAxiomStrDt) rdfRule10 :: Test rdfRule10 = testEq "rdfRule10" "xsd_string:ls" $ show (ruleName (getRule "xsd_string:ls")) rdfBase10 :: RDFFormula rdfBase10 = makeFormula scopeex "rdfBase10" $ "ex:s ex:p \"abc\" . " ++ "ex:s ex:p \"def\"^^xsd:string . " rdfStep10a :: RDFProofStep rdfStep10a = makeRDFProofStep (getRule "xsd_string:ls") [rdfBase10] rdfCons10a rdfCons10a :: RDFFormula rdfCons10a = makeFormula scopeex "rdfCons10a" $ "ex:s ex:p \"abc\"^^xsd:string . " rdfStep10b :: RDFProofStep rdfStep10b = makeRDFProofStep (getRule "xsd_string:sl") [rdfBase10] rdfCons10b rdfCons10b :: RDFFormula rdfCons10b = makeFormula scopeex "rdfCons10b" $ "ex:s ex:p \"def\" . " rdfStep10c :: RDFProofStep rdfStep10c = makeRDFProofStep (getRule "rs_rdf:sub") [rdfCons10a,rdfCons10b,rdfAxiomStrDt] rdfGoal10 rdfGoal10 :: RDFFormula rdfGoal10 = makeFormula scopeex "rdfGoal10" $ "ex:s ex:p \"abc\"^^xsd:string . " ++ "ex:s ex:p \"def\" . " ++ "xsd:string rdf:type rdfs:Datatype . " rdfProof10 :: RDFProof rdfProof10 = makeRDFProof xsdstrContext rdfBase10 rdfGoal10 [ rdfStep10a, rdfStep10b, rdfStep10c ] testRdf :: Test testRdf = TestList [ testProofStep "rdfStep01a" True [(getRule "rs_rdf:r1")] [formExpr rdfBase01] rdfStep01a , testProof "rdfProof01" True rdfProof01 -- Really should have support for scoped bnodes , testProof "rdfProof02" True rdfProof02 , testProof "rdfProof03" False rdfProof03 , testProof "rdfProof04" True rdfProof04 , testProof "rdfProof05" True rdfProof05 , testProof "rdfProof06" False rdfProof06 , testProof "rdfProof07" True rdfProof07 , testProof "rdfProof08" True rdfProof08 , rdfAxiom09 , testProof "rdfProof09" True rdfProof09 , rdfAxiom10, rdfRule10 , testProof "rdfProof10" True rdfProof10 {- , TestCase $ putStrLn ("\n"++showProof "\n" rdfProof01) , TestCase $ putStrLn ("\n"++showProof "\n" rdfProof05) -} ] ------------------------------------------------------------ -- Full test suite, main program, -- and useful expressions for interactive use ------------------------------------------------------------ allTests :: Test allTests = TestList [ testRules , testRdf ] main :: IO () main = runTestTT allTests >> return () {- runTestFile t = do h <- openFile "a.tmp" WriteMode runTestText (putTextToHandle h False) t hClose h tf = runTestFile tt = runTestTT p10 = runTestTT $ TestList [ rdfAxiom10 , rdfRule10 , testProof "rdfProof10" True rdfProof10 ] -} -------------------------------------------------------------------------------- -- -- Copyright (c) 2003, Graham Klyne, 2009 Vasili I Galchin, 2011 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 -- --------------------------------------------------------------------------------