1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
|
{-# LANGUAGE OverloadedStrings #-}
--------------------------------------------------------------------------------
-- See end of this file for licence information.
--------------------------------------------------------------------------------
-- |
-- Module : RDFProofContextTest
-- Copyright : (c) 2003, Graham Klyne, 2009 Vasili I Galchin, 2011, 2012, 2013 Douglas Burke
-- License : GPL V2
--
-- Maintainer : Douglas Burke
-- Stability : experimental
-- Portability : OverloadedStrings
--
-- This module contains RDF proof-checking test cases based on the RDF
-- semantics specifications, as capured in module RDFProofContext.
--
--------------------------------------------------------------------------------
module Main where
import qualified Data.Map as M
import qualified Data.Text as T
import qualified Data.Text.Lazy.Builder as B
import qualified Test.Framework as TF
import Swish.Namespace (Namespace, makeNamespace, ScopedName, makeNSScopedName, namespaceToBuilder)
import Swish.QName (LName, newLName)
import Swish.Proof (Step(..), checkProof, checkStep, explainProof)
import Swish.Rule (Formula(..), Rule(..), nullFormula, nullRule)
import Swish.Ruleset (getContextAxiom, getContextRule)
import Swish.RDF.BuiltIn (rdfRulesetMap, allRulesets)
import Swish.RDF.ProofContext (rulesetRDF, rulesetRDFS, rulesetRDFD)
import Swish.RDF.Proof (RDFProof, RDFProofStep, makeRDFProof, makeRDFProofStep )
import Swish.RDF.Ruleset
( RDFFormula, RDFRule, RDFRuleset
, nullRDFFormula
, makeRDFFormula )
import Swish.RDF.Graph (RDFGraph)
-- import Swish.RDF.GraphShowLines ()
import Swish.RDF.Vocabulary
( namespaceRDF
, namespaceRDFS
, namespaceRDFD
, namespaceXSD
, namespaceXsdType
, scopeRDF
, scopeRDFS
, scopeRDFD
)
import Data.Maybe (isNothing, fromJust, fromMaybe)
import Data.Monoid (Monoid(..))
import Network.URI (URI, parseURI)
import Test.HUnit
( Test(TestCase,TestList)
, assertBool, assertEqual )
import TestHelpers ( conv, test
, testEq
, testElem
)
-- misc helpers
testGr :: String -> RDFGraph -> [RDFGraph] -> Test
testGr = testElem
-- 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 -> LName -> B.Builder -> RDFFormula
makeFormula scope local gr =
makeRDFFormula scope local (prefix `mappend` 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 = makeNSScopedName ns (fromJust (newLName (T.pack 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
toURI :: String -> URI
toURI = fromJust . parseURI
toNS :: Maybe T.Text -> String -> Namespace
toNS p = makeNamespace p . toURI
mkPrefix :: Namespace -> B.Builder
mkPrefix = namespaceToBuilder
prefix :: B.Builder
prefix =
mconcat
[ mkPrefix namespaceRDF
, mkPrefix namespaceRDFS
, mkPrefix namespaceRDFD
, mkPrefix namespaceXSD
-- TODO: should the following use scopeex instead?
, mkPrefix $ toNS (Just "ex") "http://example.org/"
]
scopeex :: Namespace
scopeex = toNS (Just "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 $ M.lookup (namespaceXsdType "integer") rdfRulesetMap
rulesetXsdStr = fromJust $ M.lookup (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 ." `mappend`
"ex:p2 rdf:type rdf:Property ."
bwd01 = formExpr $ makeFormula scopeex "bwd01a" $
"_:s1 ex:p1 _:o1 . " `mappend`
"_: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 ; " `mappend`
" ex:p2a \"lit2\"^^rdf:XMLLiteral ; " `mappend`
" ex:p2b \"lit2\"^^rdf:XMLLiteral ."
con03lg = formExpr $ makeFormula scopeex "con03" $
"ex:s ex:p1 _:l1 ; ex:p2a _:l2; ex:p2b _:l2 ." `mappend`
"_:l1 rdf:_allocatedTo \"lit1\"^^rdf:XMLLiteral ." `mappend`
"_:l2 rdf:_allocatedTo \"lit2\"^^rdf:XMLLiteral ."
con03r2 = formExpr $ makeFormula scopeex "con03" $
"_:l1 rdf:type rdf:XMLLiteral ." `mappend`
"_: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 ; " `mappend`
" rdf:_2 ex:o2 . "
con04 = formExpr $ makeFormula scopeex "con04" $
"rdf:_123 rdf:type rdf:Property ." `mappend`
"rdf:_2 rdf:type rdf:Property ."
bwd04 = formExpr $ makeFormula scopeex "bwd04a" $
"_:s1 rdf:_123 _:o1 . " `mappend`
"_: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 ; " `mappend`
" ex:p2 _:o2 . " `mappend`
"ex:p1 rdfs:range ex:pr1 . " `mappend`
"ex:p2 rdfs:range ex:pr2 . "
con05 = formExpr $ makeFormula scopeex "con05" $
"ex:o1 rdf:type ex:pr1 ." `mappend`
"_:o2 rdf:type ex:pr2 ."
bwd05 = formExpr $ makeFormula scopeex "bwd05a" $
"_:s1 _:p1 ex:o1 . " `mappend`
"_:s2 _:p2 _:o2 . " `mappend`
"_:p1 rdfs:range ex:pr1 . " `mappend`
"_: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\" . " `mappend`
"ex:p1 rdfs:range ex:pr1 . "
con06 = formExpr $ makeFormula scopeex "con06"
"_:o1 rdf:type ex:pr1 ."
bwd06 = formExpr $ makeFormula scopeex "bwd06a" $
"_:s1 _:p1 _:o1 . " `mappend`
"_:p1 rdfs:range ex:pr1 . "
chk06 = formExpr $ makeFormula scopeex "bwd06a" $
"_:s1 _:p1 \"lit1\" . " `mappend`
"_: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 . " `mappend`
"_: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 . " `mappend`
"_: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 ." `mappend`
"_:p rdf:type rdf:Property ." `mappend`
"_: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\" ." `mappend`
"ex:s2 ex:p2 \"lll\" ." `mappend`
"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 ." `mappend`
"ex:s2 ex:p2 _:l ." `mappend`
"_:l rdf:_allocatedTo \"lll\" ." `mappend`
"ex:s3 ex:p3 _:m ." `mappend`
"_: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 ." `mappend`
"_: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 ." `mappend`
"ex:s2 ex:p2 _:l ." `mappend`
"_: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:cp11") [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
(makeNSScopedName (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 ." `mappend`
"_: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 ." `mappend`
"_:l rdf:_allocatedTo \"10\"^^xsd:integer ." `mappend`
"_: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
(makeNSScopedName (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\" . " `mappend`
"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 . " `mappend`
"ex:s ex:p \"def\" . " `mappend`
"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 :: [TF.Test]
allTests =
[ conv "rules" testRules
, conv "rdf" testRdf
]
main :: IO ()
main = TF.defaultMain allTests
--------------------------------------------------------------------------------
--
-- Copyright (c) 2003, Graham Klyne, 2009 Vasili I Galchin,
-- 2011, 2012, 2013 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
--
--------------------------------------------------------------------------------
|
