forked from linkeddata/swap
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathvalc.n3
151 lines (109 loc) · 5.31 KB
/
valc.n3
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
# Test whether a schema mentions the classes used in this data
# This involves searching in files for statements being present or absent.
@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#> .
@prefix s: <http://www.w3.org/2000/01/rdf-schema#> .
# @prefix dpo: <http://www.daml.org/2001/03/daml+oil#> .
@prefix log: <http://www.w3.org/2000/10/swap/log#> .
@prefix os: <http://www.w3.org/2000/10/swap/os#> .
@prefix : <validate.n3#>. # Local stuff
@prefix val: <validate.n3#>. # Local stuff
# Usage: TARGET=myfile.n3 cwm check.n3 -think -purge
#
# Output should not incldue any error messages.
#
this log:forAll :c, :d, :o, :p, :s, :S, :s1, :x, :y, :F, :G, :H.
# Some internal terms we will be using in this document:
:usedAsClassIn a rdf:Property;
s:comment "This term is used as a Class in the given document.";
a log:Chaff. # Internal use only, may be purged.
:within a rdf:Property;
s:comment "relationship between a subforumula and the document it was found in";
a log:Chaff. # Internal use only, may be purged.
:targetDocument a s:Class;
s:comment "Documents which this run is checking for schema validity";
a log:Chaff. # Internal use only, may be purged.
:schema a rdf:Property;
s:comment "The schema for a Class is the document which defines it.".
:ERROR_NO_SCHEMA_OR_CLASS_NOT_DECLARED a rdf:Property;
s:comment """The document used this as a predicate and there is no
schema which declares it as a Property""".
:ERROR_CLASS_NOT_DECLARED a rdf:Property.
# Target formulae are the top level formula we are pointed at,
# and any subformulae.
{ :d log:uri [is os:environ of "TARGET"] } log:implies { :d a :targetDocument }.
{ :d a :targetDocument. :d log:semantics :F } log:implies { :F :within :d }.
# Define subforumulae which are within the target documents:
{ :d a :targetDocument.
:F :within :d.
:F log:includes { :s :p :o}.
:s log:rawType log:Formula } log:implies { :s :within :d } .
{ :d a :targetDocument.
:F :within :d.
:F log:includes { :s :p :o}.
:o log:rawType log:Formula } log:implies { :o :within :d } .
# Anything used as a predicate in any target formula should be checked.
# We don't bother bout the pseudoproperties log:forSome and log:forAll.
{ :d a :targetDocument.
:F :within :d.
:F log:includes { :s a :c}.
:c log:rawType log:Other. # Ignore lists
} log:implies { :c :usedAsClassIn :d } .
# Let's see what happens when we dereference a class:
{ :d a :targetDocument.
:c :usedAsClassIn :d.
:c log:semanticsOrError :x } log:implies { :c :classSemanticsOrError :x }.
{ :d a :targetDocument.
:c :usedAsClassIn :d.
:c :classSemanticsOrError :x.
:x log:rawType log:Literal } log:implies { :d :ERROR_IN_SCHEMA_ACCESS_FOR_CLASS :c.
:c :CLASS_HAS_SCHEMA_ACCESS_ERROR :x }.
{ :c :classSemanticsOrError :x.
:x log:rawType log:Formula } log:implies { :c :semanticsOK :x }.
# The RDFS spec implies the following algorithm for the definitive schema corresponding
# to a Property :p. (From Ralph Swick, whiteboard conversation)
# This is the equivalent for a Class :c
# Maybe we should simplify it to the schema being the result of dereferencing the Class?
# I think the counterexample is the dublin core, but it may not work anyway.
# Actually, the dublic core uses a redirect!!! We need to be aware of the
# existence of redirects like that @@
{ :d a :targetDocument.
:c :usedAsClassIn :d.
:c :semanticsOK [log:includes { :c s:isDefinedBy :s }] } log:implies {:c :schema :s}.
# We actually need the formula the schema parses to:
{ :c :schema [ :semanticsOK :F ] } log:implies { :c :classSchemaFormula :F }.
# Alternatively, the schema can just be the document we pick up
# directly This is much simpler!
#
{ :c :usedAsClassIn :d .
:d a :targetDocument.
:c :semanticsOK :F.
:F log:includes { :c a s:Class } } log:implies { :c :classSchemaFormula :F.
:c a :classDeclaredInDirectSchema }.
# If there is no indirect schema pointer or direct declaration found, then we flag a problem
{ :d a :targetDocument.
:d log:semantics :G. # These 2 lines and one below suppress error messages
:G log:notEqualTo :F. # about undeclared locals in the same file.
:c :usedAsClassIn :d.
:c :semanticsOK :F.
:F log:notIncludes { :c s:isDefinedBy [] }. # No indirect Schema
:F log:notIncludes { :c a s:Class }. # Not a direct schema
} log:implies { :d :ERROR_DEREF_DOC_DOES_NOT_DECLARE_CLASS :c }.
# It is an error, we say, for something to be used as a Property but
# not *explicitly* declared as such in the schema:
{:c :classSchemaFormula :F.
:F log:notIncludes { :c a s:Class }}log:implies { :d :ERROR_CLASS_NOT_DECLARED :c } .
# (b)when the document is combined with the above, no condradiction
# can be found from anything being (eg) member of disjoint sets.
#
# @@ to come.
################################################################### Clean up
{:d a :targetDocument. :F :within :d } log:implies { :F a log:Chaff }. # Clear our formulae
log:Chaff is rdf:type of
rdf:type, # Seriously ...
s:comment,
log:forAll,
log:implies, # Clear out rules on -purge
:within, :classSchemaFormula, :schema, :classSemanticsOrError, :semanticsOK,
# :targetDocument,
:usedAsPropertyIn.
#ends