flams_ontology/
rdf.rs

1pub use oxrdf::{
2    BlankNode, GraphName, GraphNameRef, Literal, LiteralRef, NamedNode, NamedNodeRef, Quad,
3    QuadRef, Subject, SubjectRef, Term as RDFTerm, TermRef as RDFTermRef, Triple, TripleRef,
4    Variable,
5};
6
7#[macro_export]
8macro_rules! triple {
9    (<($sub:expr)> $($tt:tt)*) => {
10        triple!(@PRED $crate::rdf::Subject::NamedNode($sub); $($tt)*)
11    };
12
13    (($sub:expr)! $($tt:tt)*) => {
14        triple!(@PRED $crate::rdf::Subject::BlankNode($sub); $($tt)*)
15    };
16
17    (@PRED $sub:expr; : $($tt:tt)*) => {
18        triple!(@OBJ $sub;$crate::rdf::ontologies::rdf::TYPE.into_owned(); $($tt)*)
19    };
20    (@PRED $sub:expr;ulo:$pred:ident $($tt:tt)*) => {
21        triple!(@OBJ $sub;$crate::rdf::ontologies::ulo2::$pred.into_owned(); $($tt)*)
22    };
23    (@PRED $sub:expr;dc:$pred:ident $($tt:tt)*) => {
24        triple!(@OBJ $sub;$crate::rdf::ontologies::dc::$pred.into_owned(); $($tt)*)
25    };
26    (@PRED $sub:expr;rdfs:$pred:ident $($tt:tt)*) => {
27        triple!(@OBJ $sub;$crate::rdf::ontologies::rdfs::$pred.into_owned(); $($tt)*)
28    };
29
30    (@OBJ $sub:expr;$pred:expr; = ($obj:expr) $($tt:tt)*) => {
31        triple!(@MAYBEQUAD $sub;$pred;$crate::rdf::RDFTerm::Literal(
32            $crate::rdf::Literal::new_simple_literal($obj)
33        ); $($tt)*)
34    };
35    (@OBJ $sub:expr;$pred:expr; ulo:$obj:ident $($tt:tt)*) => {
36        triple!(@MAYBEQUAD $sub;$pred;$crate::rdf::RDFTerm::NamedNode($crate::rdf::ontologies::ulo2::$obj.into_owned()); $($tt)*)
37    };
38    (@OBJ $sub:expr;$pred:expr; <($obj:expr)> $($tt:tt)*) => {
39        triple!(@MAYBEQUAD $sub;$pred;$crate::rdf::RDFTerm::NamedNode($obj); $($tt)*)
40    };
41    (@OBJ $sub:expr;$pred:expr; ($obj:expr)! $($tt:tt)*) => {
42        triple!(@MAYBEQUAD $sub;$pred;$crate::rdf::RDFTerm::BlankNode($obj); $($tt)*)
43    };
44
45    (@MAYBEQUAD $sub:expr;$pred:expr;$obj:expr;) => {
46        $crate::rdf::Triple {
47            subject: $sub,
48            predicate: $pred,
49            object: $obj
50        }
51    }
52}
53
54#[macro_export]
55macro_rules! rdft {
56    (> ($sub:expr) : $tp:ident) => {
57        rdft!(($crate::rdf::NamedNode::new($sub).unwrap()) : $tp)
58    };
59    (($sub:expr) : $tp:ident) => {
60        rdft!(@TRIPLE $sub; $crate::rdf::ontologies::rdf::TYPE.into_owned(); $crate::rdf::ontologies::ulo2::$tp.into_owned())
61    };
62    (($sub:expr) : ($tp:expr)) => {
63        rdft!(@TRIPLE $sub; $crate::rdf::ontologies::rdf::TYPE.into_owned(); $tp)
64    };
65    (>($sub:expr) : $tp:ident Q) => {
66        rdft!(($crate::rdf::NamedNode::new($sub).unwrap()) : $tp Q)
67    };
68    (($sub:expr) : $tp:ident Q) => {
69        rdft!(@QUAD $sub; $crate::rdf::ontologies::rdf::TYPE.into_owned(); $crate::rdf::ontologies::ulo2::$tp.into_owned())
70    };
71    (>($sub:expr) : $tp:ident IN $graph:expr) => {
72        rdft!(($crate::rdf::NamedNode::new($sub).unwrap()) : $tp IN $graph)
73    };
74    (($sub:expr) : >($tp:expr) IN $graph:expr) => {
75        rdft!(@QUAD_IN $sub; $crate::rdf::ontologies::rdf::TYPE.into_owned(); $tp; $graph)
76    };
77    (($sub:expr) : $tp:ident IN $graph:expr) => {
78        rdft!(@QUAD_IN $sub; $crate::rdf::ontologies::rdf::TYPE.into_owned(); $crate::rdf::ontologies::ulo2::$tp.into_owned(); $graph)
79    };
80    (($sub:expr) !($tp:expr) ($obj:expr) IN $graph:expr) => {
81        rdft!(@QUAD_IN $sub; $tp.into_owned(); $obj; $graph)
82    };
83    (($sub:expr) !($tp:expr) ($obj:expr)) => {
84        rdft!(@TRIPLE $sub; $tp.into_owned(); $obj)
85    };
86
87    (>($sub:expr) $tp:ident >($obj:expr) Q) => {
88        rdft!(($crate::rdf::NamedNode::new($sub).unwrap()) $tp ($crate::rdf::NamedNode::new($obj).unwrap()) Q)
89    };
90    (($sub:expr) $tp:ident >($obj:expr) Q) => {
91        rdft!(($sub) $tp ($crate::rdf::NamedNode::new($obj).unwrap()) Q)
92    };
93    (>($sub:expr) $tp:ident ($obj:expr) Q) => {
94        rdft!(($crate::rdf::NamedNode::new($sub).unwrap()) $tp ($obj) Q)
95    };
96    (($sub:expr) $tp:ident ($obj:expr) Q) => {
97        rdft!(@QUAD $sub; $crate::rdf::ontologies::ulo2::$tp.into_owned(); $obj)
98    };
99    (($sub:expr) $tp:ident ($obj:expr) IN $graph:expr) => {
100        rdft!(@QUAD_IN $sub; $crate::rdf::ontologies::ulo2::$tp.into_owned(); $obj; $graph)
101    };
102    (($sub:expr) $tp:ident >>($obj:expr) IN $graph:expr) => {
103        rdft!(@QUAD_IN $sub; $crate::rdf::ontologies::ulo2::$tp.into_owned(); >>$obj; $graph)
104    };
105    (($sub:expr) $tp:ident >>($obj:expr)) => {
106        rdft!(@TRIPLE $sub; $crate::rdf::ontologies::ulo2::$tp.into_owned(); >>$obj)
107    };
108    (>>($sub:expr) $tp:ident ($obj:expr) IN $graph:expr) => {
109        rdft!(@QUAD_IN >>$sub; $crate::rdf::ontologies::ulo2::$tp.into_owned(); $obj; $graph)
110    };
111    (>>($sub:expr) $tp:ident ($obj:expr)) => {
112        rdft!(@TRIPLE >>$sub; $crate::rdf::ontologies::ulo2::$tp.into_owned(); $obj)
113    };
114    (>($sub:expr) $tp:ident >($obj:expr)) => {
115        rdft!(($crate::rdf::NamedNode::new($sub).unwrap()) $tp ($crate::rdf::NamedNode::new($obj).unwrap()))
116    };
117    (($sub:expr) $tp:ident >($obj:expr)) => {
118        rdft!(($sub) $tp ($crate::rdf::NamedNode::new($obj).unwrap()))
119    };
120    (>($sub:expr) $tp:ident ($obj:expr)) => {
121        rdft!(($crate::rdf::NamedNode::new($sub).unwrap()) $tp ($obj))
122    };
123    (($sub:expr) $tp:ident ($obj:expr)) => {
124        rdft!(@TRIPLE $sub; $crate::rdf::ontologies::ulo2::$tp.into_owned(); $obj)
125    };
126    (($sub:expr) ($tp:expr) = ($obj:expr) IN $graph:expr) => {
127        $crate::rdf::Quad {
128            subject: $crate::rdf::Subject::NamedNode($sub),
129            predicate: $tp.into(),
130            object: $crate::rdf::Term::Literal(
131                $crate::rdf::Literal::new_simple_literal($obj)
132            ),
133            graph_name: $crate::rdf::GraphName::NamedNode($graph)
134        }
135    };
136
137    (@TRIPLE >>$sub:expr; $pred:expr; $obj:expr) => {
138        $crate::rdf::Triple {
139            subject: $sub,
140            predicate: $pred,
141            object: $crate::rdf::Term::NamedNode($obj)
142        }
143    };
144    (@TRIPLE $sub:expr; $pred:expr; >>$obj:expr) => {
145        $crate::rdf::Triple {
146            subject: $crate::rdf::Subject::NamedNode($sub),
147            predicate: $pred,
148            object: $obj
149        }
150    };
151    (@TRIPLE $sub:expr; $pred:expr; $obj:expr) => {
152        $crate::rdf::Triple {
153            subject: $crate::rdf::Subject::NamedNode($sub),
154            predicate: $pred,
155            object: $crate::rdf::Term::NamedNode($obj)
156        }
157    };
158    (@QUAD $sub:expr; $pred:expr; $obj:expr) => {
159        $crate::rdf::Quad {
160            subject: $crate::rdf::Subject::NamedNode($sub),
161            predicate: $pred,
162            object: $crate::rdf::Term::NamedNode($obj),
163            graph_name: $crate::rdf::GraphName::DefaultGraph
164        }
165    };
166    (@QUAD_IN $sub:expr; $pred:expr; >>$obj:expr; $graph:expr) => {
167        $crate::rdf::Quad {
168            subject: $crate::rdf::Subject::NamedNode($sub),
169            predicate: $pred,
170            object: $obj,
171            graph_name: $crate::rdf::GraphName::NamedNode($graph)
172        }
173    };
174    (@QUAD_IN >>$sub:expr; $pred:expr; $obj:expr; $graph:expr) => {
175        $crate::rdf::Quad {
176            subject: $sub,
177            predicate: $pred,
178            object: $crate::rdf::Term::NamedNode($obj),
179            graph_name: $crate::rdf::GraphName::NamedNode($graph)
180        }
181    };
182    (@QUAD_IN $sub:expr; $pred:expr; $obj:expr; $graph:expr) => {
183        $crate::rdf::Quad {
184            subject: $crate::rdf::Subject::NamedNode($sub),
185            predicate: $pred,
186            object: $crate::rdf::Term::NamedNode($obj),
187            graph_name: $crate::rdf::GraphName::NamedNode($graph)
188        }
189    };
190}
191
192pub mod ontologies {
193    /*! # RDF Ontology Summary
194     *
195     * #### [`Document`](crate::narration::documents::Document) `D`
196     * | struct | field | triple |
197     * | -----  | ----- | ------ |
198     * |   |    | `D` [`<rdf:#type>`](rdf::TYPE) [`<ulo:#document>`](ulo2::DOCUMENT) |
199     * |   | language `l` | `D` [`<dc:#language>`](dc::LANGUAGE) `l` |
200     * |   | in archive `A`  | `A` [`<ulo:#contains>`](ulo2::CONTAINS) `D` |
201     * | [`DocumentReference`](crate::narration::DocumentElement::DocumentReference) | [`.target`](crate::narration::DocumentElement::DocumentReference::target)`=D2` | `D` [`<dc:#hasPart>`](dc::HAS_PART) `D2` |
202     * | [`UseModule`](crate::narration::DocumentElement::UseModule) | `(M)` | `D` [`<dc:#requires>`](dc::REQUIRES) `M` |
203     * | [`Paragraph`](crate::narration::paragraphs::LogicalParagraph) |   | `D` [`<ulo:#contains>`](ulo2::CONTAINS) `P` |
204     * |   | `P`[`.kind`](crate::narration::paragraphs::LogicalParagraph::kind)`=`[`Definition`](crate::narration::paragraphs::ParagraphKind::Definition) | `P` [`<rdf:#type>`](rdf::TYPE) [`<ulo:#definition>`](ulo2::DEFINITION) |
205     * |   | `P`[`.kind`](crate::narration::paragraphs::LogicalParagraph::kind)`=`[`Assertion`](crate::narration::paragraphs::ParagraphKind::Assertion) | `P` [`<rdf:#type>`](rdf::TYPE) [`<ulo:#proposition>`](ulo2::PROPOSITION) |
206     * |   | `P`[`.kind`](crate::narration::paragraphs::LogicalParagraph::kind)`=`[`Paragraph`](crate::narration::paragraphs::ParagraphKind::Paragraph) | `P` [`<rdf:#type>`](rdf::TYPE) [`<ulo:#para>`](ulo2::PARA) |
207     * |   | `P`[`.kind`](crate::narration::paragraphs::LogicalParagraph::kind)`=`[`Example`](crate::narration::paragraphs::ParagraphKind::Example) | `P` [`<rdf:#type>`](rdf::TYPE) [`<ulo:#example>`](ulo2::EXAMPLE) |
208     * |   | is [`Example`](crate::narration::paragraphs::ParagraphKind::Example) and `_`[`.fors`](crate::narration::paragraphs::LogicalParagraph::fors)`.contains(S)`  | `P` [`<ulo:#example-for>`](ulo2::EXAMPLE_FOR) `S` |
209     * |   | [`is_definition_like`](crate::narration::paragraphs::ParagraphKind::is_definition_like) and  `_`[`.fors`](crate::narration::paragraphs::LogicalParagraph::fors)`.contains(S)`  | `P` [`<ulo:#defines>`](ulo2::DEFINES) `S` |
210     * | [`Problem`](crate::narration::problems::Problem) `E` |   | `D` [`<ulo:#contains>`](ulo2::CONTAINS) `E` |
211     * |   | [`.sub_problem`](crate::narration::problems::Problem::sub_problem)`==false`   | `E` [`<rdf:#type>`](rdf::TYPE) [`<ulo:#problem>`](ulo2::PROBLEM) |
212     * |   | [`.sub_problem`](crate::narration::problems::Problem::sub_problem)`==true`   | `E` [`<rdf:#type>`](rdf::TYPE) [`<ulo:#subproblem>`](ulo2::SUBPROBLEM) |
213     * |   | `_`[`.preconditions`](crate::narration::problems::Problem::preconditions)`.contains(d,S)`  | `E` [`<ulo:#precondition>`](ulo2::PRECONDITION) `<BLANK>` |
214     * |   |    | `<BLANK>` [`<ulo:#cognitive-dimension>`](ulo2::COGDIM) `d`, where `d=`[`<ulo:#cs-remember>`](ulo2::REMEMBER)⏐[`<ulo:#cs-understand>`](ulo2::UNDERSTAND)⏐[`<ulo:#cs-apply>`](ulo2::APPLY)⏐[`<ulo:#cs-analyze>`](ulo2::ANALYZE)⏐[`<ulo:#cs-evaluate>`](ulo2::EVALUATE)⏐[`<ulo:#cs-create>`](ulo2::CREATE) |
215     * |   |    | `<BLANK>` [`<ulo:#po-symbol>`](ulo2::POSYMBOL) `S` |
216     * |   | `_`[`.objectives`](crate::narration::problems::Problem::objectives)`.contains(d,S)`  | `E` [`<ulo:#objective>`](ulo2::OBJECTIVE) `<BLANK>` |
217     * |   |    | `<BLANK>` [`<ulo:#cognitive-dimension>`](ulo2::COGDIM) `d`, where `d=`[`<ulo:#cs-remember>`](ulo2::REMEMBER)⏐[`<ulo:#cs-understand>`](ulo2::UNDERSTAND)⏐[`<ulo:#cs-apply>`](ulo2::APPLY)⏐[`<ulo:#cs-analyze>`](ulo2::ANALYZE)⏐[`<ulo:#cs-evaluate>`](ulo2::EVALUATE)⏐[`<ulo:#cs-create>`](ulo2::CREATE) |
218     * |   |    | `<BLANK>` [`<ulo:#po-symbol>`](ulo2::POSYMBOL) `S` |
219     *
220     * #### [`Module`](crate::content::modules::Module) `M`
221     * | struct | field | triple |
222     * | -----  | ----- | ------ |
223     * |   |    | `D` [`<ulo:#contains>`](ulo2::CONTAINS) `M` |
224     * |   |    | `M` [`<rdf:#type>`](rdf::TYPE) [`<ulo:#theory>`](ulo2::THEORY) |
225     * | [`Import`](crate::content::declarations::OpenDeclaration::Import) | `(M2)` | `M` [`<ulo:#imports>`](ulo2::IMPORTS) `M2` |
226     * | [`NestedModule`](crate::content::declarations::OpenDeclaration::NestedModule) | `(M2)` | `D` [`<ulo:#contains>`](ulo2::CONTAINS) `M2` |
227     * |   |    | `M` [`<ulo:#contains>`](ulo2::CONTAINS) `M2` |
228     * |   |    | `M2` [`<rdf:#type>`](rdf::TYPE) [`<ulo:#theory>`](ulo2::THEORY) |
229     * | [`MathStructure`](crate::content::declarations::OpenDeclaration::MathStructure) | `(S)` | `M` [`<ulo:#contains>`](ulo2::CONTAINS) `S` |
230     * |   |    | `S` [`<rdf:#type>`](rdf::TYPE) [`<ulo:#structure>`](ulo2::STRUCTURE) |
231     * |   | [`Import`](crate::content::declarations::OpenDeclaration::Import)(`S2`)   | `S` [`<ulo:#extends>`](ulo2::EXTENDS) `S2` |
232     * | [`Morphism`](crate::content::declarations::OpenDeclaration::Morphism) | `(F)` | `M` [`<ulo:#contains>`](ulo2::CONTAINS) `F` |
233     * |   |    | `F` [`<rdf:#type>`](rdf::TYPE) [`<ulo:#morphism>`](ulo2::MORPHISM) |
234     * |   | [`.domain`](crate::content::declarations::morphisms::Morphism)`=M2`   | `F` [`<rdfs:#domain>`](rdfs::DOMAIN) `M2` |
235     *
236     *
237     *
238     * # Some Example Queries
239     *
240     * #### Unused files in `ARCHIVE`:
241     * All elements contained in the archive that are neither inputrefed elsewhere
242     * nor (transitively) contain an element that is required or imported (=> is a module)
243     * by another document:
244     * ```sparql
245     * SELECT DISTINCT ?f WHERE {
246     *   <ARCHIVE> ulo:contains ?f .
247     *   MINUS { ?d dc:hasPart ?f }
248     *   MINUS {
249     *     ?f ulo:contains+ ?m.
250     *     ?d (dc:requires|ulo:imports) ?m.
251     *   }
252     * }
253     * ```
254     *
255     * #### All referenced symbols in `DOCUMENT`:
256     * All symbols referenced in an element that is transitively contained or inputrefed in
257     * the document:
258     * ```sparql
259     * SELECT DISTINCT ?s WHERE {
260     *   <DOCUMENT> (ulo:contains|dc:hasPart)* ?p.
261     *   ?p ulo:crossrefs ?s.
262     * }
263     * ```
264     *
265     * #### All symbols defined in a `DOCUMENT`:
266     * All symbols defined by a paragraph `p` that is transitively contained or inputrefed in
267     * the document:
268     * ```sparql
269     * SELECT DISTINCT ?s WHERE {
270     *   <DOCUMENT> (ulo:contains|dc:hasPart)* ?p.
271     *   ?p ulo:defines ?s.
272     * }
273     * ```
274     *
275     * #### All "prerequisite" concepts in a `DOCUMENT`:
276     * All symbols references in the document that are not also defined in it:
277     * ```sparql
278     * SELECT DISTINCT ?s WHERE {
279     *   <DOCUMENT> (ulo:contains|dc:hasPart)* ?p.
280     *   ?p ulo:crossrefs ?s.
281     *   MINUS {
282     *     <DOCUMENT> (ulo:contains|dc:hasPart)* ?p.
283     *     ?p ulo:defines ?s.
284     *   }
285     * }
286     * ```
287     *
288     *
289     */
290
291    /*
292
293     use crate::content::declarations::OpenDeclaration::Symbol;
294     use crate::narration::problems::Problem;
295     use crate::narration::paragraphs::ParagraphKind::Definition;
296     use crate::content::declarations::morphisms::Morphism;
297
298    section:
299
300
301    symdecl:
302    #[cfg(feature="rdf")]
303    if E::RDF {
304        if let Some(m) = extractor.get_content_iri() {
305            let iri = uri.to_iri();
306            extractor.add_triples([
307                triple!(<(iri.clone())> : ulo:DECLARATION),
308                triple!(<(m)> ulo:DECLARES <(iri)>),
309            ]);
310        }
311    }
312
313    vardecl:
314    #[cfg(feature="rdf")]
315    if E::RDF {
316        let iri = uri.to_iri();
317        extractor.add_triples([
318            triple!(<(iri.clone())> : ulo:VARIABLE),
319            triple!(<(extractor.get_document_iri())> ulo:DECLARES <(iri)>),
320        ]);
321    }
322
323    notation:
324    #[cfg(feature="rdf")]
325    if E::RDF {
326        let iri = uri.to_iri();
327        extractor.add_triples([
328            triple!(<(iri.clone())> : ulo:NOTATION),
329            triple!(<(iri.clone())> ulo:NOTATION_FOR <(symbol.to_iri())>),
330            triple!(<(extractor.get_document_iri())> ulo:DECLARES <(iri)>),
331        ]);
332    }
333
334    symref:
335    #[cfg(feature="rdf")]
336    if E::RDF {
337        let iri = extractor.get_document_iri();
338        extractor.add_triples([
339            triple!(<(iri)> ulo:CROSSREFS <(uri.to_iri())>)
340        ]);
341    }
342
343    varref:
344    #[cfg(feature="rdf")]
345    if E::RDF {
346        let iri = extractor.get_document_iri();
347        extractor.add_triples([
348            triple!(<(iri)> ulo:CROSSREFS <(uri.to_iri())>)
349        ]);
350    }
351
352
353
354
355
356     */
357
358    pub mod rdf {
359        pub use oxrdf::vocab::rdf::*;
360    }
361    pub mod rdfs {
362        pub use oxrdf::vocab::rdfs::*;
363    }
364    pub mod xsd {
365        pub use oxrdf::vocab::xsd::*;
366    }
367    macro_rules! count {
368        () => (0usize);
369        ( $e:expr; $($n:expr;)* ) => (1usize + count!($($n;)*));
370    }
371
372    macro_rules! dict {
373        ($name:ident = $uri:literal: $(
374            $(+ $i:ident = $l:literal)?
375            $(DATAPROP $di:ident = $dl:literal $(<: $( $($dsup:ident)::*  ),* )? $(: $($dtp:ident)::* )? $(@ $dcl:literal)? )?
376            $(OBJPROP $oi:ident = $ol:literal $(<: $( $($osup:ident)::*  ),* )? $(( $dom:ident => $range:ident ))? $(- $inv:ident)? $(! $disj:ident)? $(@ $ocl:literal)? )?
377            $(CLASS $ci:ident = $cl:literal $(<: $( $($csup:ident)::*  ),* )? $(= $left:ident u $right:ident)? $(@ $ccl:literal)? )?
378            $({
379              $($subj_n:ident)::*
380              <$($pred_n:ident)::*>
381              $(<$($obj_n:ident)::*>)?
382              $(S $obj_str:literal)?
383            })?
384        ;)*) => {
385            dict!{@old $name = $uri;
386                $($($i = $l,)?)* $($($di = $dl,)?)* $($($oi = $ol,)?)* $($($ci = $cl,)?)*;
387                $(
388                    $( // dict!(@triple $($subj_n)::*;$($pred_n)::*; $(NAME $($obj_n)::*)? $(STRING $obj_str)? );
389                          SubjectRef::NamedNode($($subj_n)::*),
390                          $($pred_n)::*,
391                          $(RDFTermRef::NamedNode($($obj_n)::*))?
392                          $(RDFTermRef::Literal(LiteralRef::new_simple_literal($obj_str)))?
393                    ;)?
394                    $(  //dict!(@tp $ci;super::owl::DATATYPE_PROPERTY);
395                        SubjectRef::NamedNode($di),
396                        super::rdf::TYPE,
397                        RDFTermRef::NamedNode(super::owl::DATATYPE_PROPERTY);
398                        $(//dict!(@comment $di;$dcl);
399                            SubjectRef::NamedNode($di),
400                            super::rdfs::COMMENT,
401                            RDFTermRef::Literal(LiteralRef::new_simple_literal($dcl));
402                        )?
403                        $(
404                            SubjectRef::NamedNode($di),
405                            super::rdfs::RANGE,
406                            RDFTermRef::NamedNode($($dtp)::*);
407                        )?
408                        $($(//dict!(@subprop $oi;$($osup)::*);
409                            SubjectRef::NamedNode($di),
410                            super::rdfs::SUB_PROPERTY_OF,
411                            RDFTermRef::NamedNode($($dsup)::*);
412                        )*)?
413                    )?
414                    $(  //dict!(@tp $ci;super::owl::OBJECT_PROPERTY);
415                        SubjectRef::NamedNode($oi),
416                        super::rdf::TYPE,
417                        RDFTermRef::NamedNode(super::owl::OBJECT_PROPERTY);
418                        $(//dict!(@comment $oi;$ocl);
419                            SubjectRef::NamedNode($oi),
420                            super::rdfs::COMMENT,
421                            RDFTermRef::Literal(LiteralRef::new_simple_literal($ocl));
422                        )?
423                        $(
424                            SubjectRef::NamedNode($oi),
425                            super::rdfs::DOMAIN,
426                            RDFTermRef::NamedNode($dom);
427                            SubjectRef::NamedNode($oi),
428                            super::rdfs::RANGE,
429                            RDFTermRef::NamedNode($range);
430                        )?
431                        $(
432                            SubjectRef::NamedNode($oi),
433                            super::owl::INVERSE_OF,
434                            RDFTermRef::NamedNode($inv);
435                        )?
436                        $(
437                            SubjectRef::NamedNode($oi),
438                            super::owl::DISJOINT_WITH,
439                            RDFTermRef::NamedNode($disj);
440                        )?
441                        $($(//dict!(@subprop $oi;$($osup)::*);
442                            SubjectRef::NamedNode($oi),
443                            super::rdfs::SUB_PROPERTY_OF,
444                            RDFTermRef::NamedNode($($osup)::*);
445                        )*)?
446                    )?
447                    $(  //dict!(@tp $ci;super::owl::CLASS);
448                        SubjectRef::NamedNode($ci),
449                        super::rdf::TYPE,
450                        RDFTermRef::NamedNode(super::owl::CLASS);
451                        $(//dict!(@comment $ci;$ccl);
452                            SubjectRef::NamedNode($ci),
453                            super::rdfs::COMMENT,
454                            RDFTermRef::Literal(LiteralRef::new_simple_literal($ccl));
455                        )?
456                        $(
457                            SubjectRef::NamedNode($left),
458                            super::owl::DISJOINT_WITH,
459                            RDFTermRef::NamedNode($right);
460                            SubjectRef::NamedNode($left),
461                            super::owl::COMPLEMENT_OF,
462                            RDFTermRef::NamedNode($right);
463                        )?
464                        $($(//dict!(@subclass $ci;$($csup)::*);
465                            SubjectRef::NamedNode($ci),
466                            super::rdfs::SUB_CLASS_OF,
467                            RDFTermRef::NamedNode($($csup)::*);
468                        )*)?
469                    )?
470                )*
471            }
472        };
473        (@triple $($subj:ident)::*;$($pred:ident)::*;$(NAME $($obj_n:ident)::*)? $(STRING $obj_str:literal)? ) => {dict!(@quad
474              SubjectRef::NamedNode($($subj)::*);
475              $($pred_n)::*;
476              $(TermRef::NamedNode($($obj_n)::*))?
477              $(TermRef::Literal(LiteralRef::new_simple_literal($obj_str)))?
478        )};
479        (@tp $i:ident;$($tp:ident)::*) => {dict!(@quad
480            SubjectRef::NamedNode($i);
481            super::rdfs::SUB_CLASS_OF;
482            TermRef::NamedNode($($tp)::*)
483        )};
484        (@subprop $i:ident;$($sup:ident)::*) => {dict!(@quad
485            SubjectRef::NamedNode($i);
486            super::rdfs::SUB_PROPERTY_OF;
487            TermRef::NamedNode($($sup)::*)
488        )};
489        (@subclass $i:ident;$($sup:ident)::*) => {dict!(@quad
490            SubjectRef::NamedNode($i);
491            super::rdfs::SUB_CLASS_OF;
492            TermRef::NamedNode($($sup)::*)
493        )};
494        (@class $i:ident;) => {dict!(@quad
495            SubjectRef::NamedNode($ci);
496            super::rdf::TYPE;
497            TermRef::NamedNode(super::owl::CLASS)
498        )};
499        (@comment $i:ident;$c:literal;) => {dict!(@quad
500            SubjectRef::NamedNode($i);
501            super::rdfs::COMMENT;
502            TermRef::Literal(LiteralRef::new_simple_literal($c))
503        )};
504        (@quad $sub:expr;$pred:expr;$obj:expr) => {
505            QuadRef{ subject:$sub,predicate:$pred,object:$obj,graph_name:GraphNameRef::NamedNode(NS) }
506        };
507        (@final $name:ident = $uri:literal;
508            $($i:ident = $l:literal,)*;
509            $($($quad:tt)*;)*
510        ) => {
511            pub mod $name {
512                #![doc=concat!("`",$uri,"`")]
513                use super::super::terms::*;
514                #[doc=concat!("`",$uri,"`")]
515                pub const NS : NamedNodeRef = NamedNodeRef::new_unchecked($uri);
516                $(
517                    #[doc=concat!("`",$uri,"#",$l,"`")]
518                    pub const $i : NamedNodeRef = NamedNodeRef::new_unchecked(concat!($uri,"#",$l));
519                )*
520
521                pub static QUADS :&[QuadRef;count!($( $($quad)*; )*)] = &[$( $($quad)* ),*];
522            }
523        };
524        (@old $name:ident = $uri:literal;
525            $($i:ident = $l:literal,)*;
526            $($sub:expr,$pred:expr,$obj:expr;)*
527        ) => {
528            pub mod $name {
529                #![doc=concat!("`",$uri,"`")]
530                use super::super::*;
531                #[doc=concat!("`",$uri,"`")]
532                pub const NS : NamedNodeRef = NamedNodeRef::new_unchecked($uri);
533                $(
534                    #[doc=concat!("`",$uri,"#",$l,"`")]
535                    pub const $i : NamedNodeRef = NamedNodeRef::new_unchecked(concat!($uri,"#",$l));
536                )*
537
538                pub static QUADS :&[QuadRef;count!($($sub;)*)] = &[$(QuadRef{
539                    subject:$sub,predicate:$pred,object:$obj,graph_name:GraphNameRef::NamedNode(NS)
540                }),*];
541            }
542        }
543    }
544
545    dict! { dc = "http://purl.org/dc/elements/1.1":
546        + RIGHTS = "rights";
547        + LANGUAGE = "language";
548        + HAS_PART = "hasPart";
549        + REQUIRES = "requires";
550    }
551
552    dict! { owl = "http://www.w3.org/2002/07/owl":
553        + OBJECT_PROPERTY = "ObjectProperty";
554        + DATATYPE_PROPERTY = "DatatypeProperty";
555        + CLASS = "Class";
556        + DISJOINT_WITH = "disjointWith";
557        + DISJOINT_UNION_OF = "disjointUnionOf";
558        + COMPLEMENT_OF = "complementOf";
559        + INVERSE_OF = "inverseOf";
560        + SYMMETRIC_PROPERTY = "SymmetricProperty";
561        + ASYMMETRIC_PROPERTY = "AsymmetricProperty";
562        + TRANSITIVE_PROPERTY = "TransitiveProperty";
563        + THING = "Thing";
564        + FUNCTIONAL_PROPERTY = "FunctionalProperty";
565    }
566
567    dict! { ulo2 = "http://mathhub.info/ulo":
568        { NS <super::dc::RIGHTS> S "This ontology is licensed under the CC-BY-SA license."};
569        DATAPROP ORGANIZATIONAL = "organizational";
570
571
572        CLASS PHYSICAL = "physical" @ "An organizational unit for the physical organization of \
573            mathematical knowledge into documents or document collections.";
574        CLASS FILE = "file" <: PHYSICAL @ "A document in a file system.";
575        CLASS DOCUMENT = "document" <: PHYSICAL @ "A document; typically corresponding to a file.";
576        CLASS FOLDER = "folder" <: PHYSICAL @ "A grouping of files and other folder, i.e. above the document level.";
577        CLASS LIBRARY = "library" <: PHYSICAL @ "A grouping of mathematical documents. Usually in the \
578            form of a repository.";
579        CLASS LIBRARY_GROUP = "library-group" <: PHYSICAL @ "A group of libraries, usually on a \
580            repository server like GitHub.";
581        CLASS PARA = "para" <: PHYSICAL @ "A document paragraph with mathematical meaning.";
582        CLASS PHRASE = "phrase" <: PHYSICAL @ "Phrasal structures in mathematical texts and formulae, \
583            these include symbols, declarations, and quantifications.";
584        CLASS SECTION = "section" <: PHYSICAL @ "A physical grouping inside a document. These can be nested.";
585        CLASS DEFINITION = "definition" <: PARA @ "A logical paragraph that defines a new concept.";
586        CLASS EXAMPLE = "example" <: PARA @ "A logical paragraph that introduces a mathematical example.";
587        CLASS PROOF = "proof" <: PARA @ "A logical paragraph that serves as a justification of a proposition.";
588        CLASS SUBPROOF = "subproof" <: PARA @ "A logical paragraph that serves as a justification of an\
589         intermediate proposition within a proof.";
590        CLASS PROPOSITION = "proposition" <: PARA @ "A statement of a mathematical object or some relation between some." ;
591        CLASS PROBLEM = "problem" <: PARA @ "A logical paragraph posing an exercise/question/problem for the reader.";
592        CLASS SUBPROBLEM = "subproblem" <: PARA @ "A logical paragraph posing a subproblem in some problem/question/problem for the reader.";
593
594
595        // -----------------------------------------------------------------------------
596
597        CLASS LOGICAL = "logical" = PRIMITIVE u LOGICAL @ "A logical classification of mathematical \
598            knowledge items.";
599        CLASS PRIMITIVE = "primitive" <: LOGICAL @ "This knowledge item does not have a definition in \
600            terms of (more) primitive items." ;
601        CLASS DERIVED = "derived" <: LOGICAL;
602        CLASS THEORY = "theory" <: LOGICAL @ "A semantically meaningful block of declarations that can \
603            be referred to globally. Examples include MMT theories, Mizar articles, Isabelle locales \
604            and Coq sections.";
605        CLASS STRUCTURE = "structure" <: LOGICAL @ "A semantically meaningful block of declarations that can \
606            be instantiated by providing definientia for all (undefined) declarations.";
607        CLASS MORPHISM = "morphism" <: LOGICAL @ "A semantically meaningful block of declarations that map \
608            map declarations in the domain to expressions over the containing module";
609        CLASS DECLARATION = "declaration" <: LOGICAL @ "Declarations are named objects. They can also \
610            have a type and a definiens.";
611        CLASS VARIABLE = "variable" <: LOGICAL @ "A local variable with optional type and definiens";
612        CLASS NOTATION = "notation" <: LOGICAL @ "A way of representing (an application of) a symbol\
613            for parsing or presentation.";
614        CLASS STATEMENT = "statement" <: DECLARATION = AXIOM u THEOREM @ "Statements are declarations of \
615            objects that can in principle have proofs.";
616        CLASS AXIOM = "axiom" <: STATEMENT @ "Logically (using the Curry-Howard isomorphism), an axiom \
617            is a primitive statement, i.e. a declaration without a definiens.";
618        CLASS THEOREM = "theorem" <: STATEMENT @ "Logically (using the Curry-Howard isomorphism), a \
619            theorem is a derived statement, i.e. a declaration with a definiens (this is the proof of \
620            the theorem given in the type)";
621        CLASS FUNCTION_DECL = "function-declaration" <: DECLARATION, FUNCTION;
622        CLASS FUNCTION = "function" <: LOGICAL @ "Functions that construct objects, possibly from other \
623            objects, for example in first-order logic the successor function.";
624        CLASS TYPE_DECL = "type-declaration" <: DECLARATION, TYPE;
625        CLASS TYPE = "type" <: LOGICAL @ "Types divide their universe into named subsets.";
626        CLASS UNIVERSE_DECL = "universe-declaration" <: DECLARATION, UNIVERSE;
627        CLASS UNIVERSE = "universe" <: LOGICAL @ "A universe, used e.g. in strong logics like Coq.";
628        CLASS PREDICATE = "predicate" <: FUNCTION @ "A predicate is a mathematical object that \
629            evaluates to true/false when applied to enough arguments.";
630        CLASS RULE = "rule" <: STATEMENT @  "Rules are statements that can be used for computation, \
631            e.g. theorems that can be used for simplification.";
632
633        OBJPROP IMPORTS = "imports" (LOGICAL => LOGICAL);
634        { IMPORTS <super::rdf::TYPE> <super::owl::TRANSITIVE_PROPERTY>};
635
636        // -----------------------------------------------------------------------------
637
638        OBJPROP CONTAINS = "contains" (PHYSICAL => PHYSICAL);
639        OBJPROP DECLARES = "declares" (LOGICAL => LOGICAL);
640
641        OBJPROP SPECIFIES = "specifies" (PHYSICAL => LOGICAL) -SPECIFIED_IN @ "The physical organizational \
642            item S specifies a knowledge item O, i.e. S is represented in O.";
643        OBJPROP SPECIFIED_IN = "specified-in" (LOGICAL => PHYSICAL) -SPECIFIES;
644        OBJPROP CROSSREFS = "crossrefs";
645        OBJPROP ALIGNED_WITH = "aligned-with" <: CROSSREFS;
646        { ALIGNED_WITH <super::rdf::TYPE> <super::owl::SYMMETRIC_PROPERTY>};
647        OBJPROP ALTERNATIVE_FOR = "alternative-for" <: CROSSREFS;
648        OBJPROP INSPIRED_BY = "inspired-by" <: CROSSREFS;
649        OBJPROP SAME_AS = "same-as" <: CROSSREFS;
650        { SAME_AS <super::rdf::TYPE> <super::owl::SYMMETRIC_PROPERTY>};
651        OBJPROP SEE_ALSO = "see-also" <: CROSSREFS;
652        OBJPROP SIMILAR_TO = "similar-to" <: CROSSREFS;
653        { SIMILAR_TO <super::rdf::TYPE> <super::owl::SYMMETRIC_PROPERTY>};
654
655        OBJPROP INTER_STATEMENT = "inter-statement";
656        OBJPROP CONSTRUCTS = "constructs" <: INTER_STATEMENT @ "S is a constructor for an inductive type or predicate O";
657        OBJPROP EXTENDS = "extends" <: INTER_STATEMENT @ "S is a conservative extension of O";
658
659        OBJPROP EXAMPLE_FOR = "example-for" <: INTER_STATEMENT !COUNTER_EXAMPLE_FOR;
660        OBJPROP COUNTER_EXAMPLE_FOR = "counter-example-for" <: INTER_STATEMENT !EXAMPLE_FOR;
661        OBJPROP DEFINES = "defines" <: INTER_STATEMENT (DEFINITION => FUNCTION) @ "A definition defines various objects.";
662
663        OBJPROP GENERATED_BY = "generated-by" <: INTER_STATEMENT (FUNCTION => FUNCTION);
664        OBJPROP INDUCTIVE_ON = "inductive-on" <: INTER_STATEMENT;
665        OBJPROP JUSTIFIES = "justifies" <: INTER_STATEMENT;
666        { JUSTIFIES <super::rdfs::DOMAIN> <PROOF>};
667        OBJPROP NOTATION_FOR = "notation-for" <: INTER_STATEMENT;
668        { NOTATION_FOR <super::rdfs::DOMAIN> <NOTATION>};
669
670        OBJPROP PRECONDITION = "precondition";
671        OBJPROP OBJECTIVE = "objective";
672
673        OBJPROP COGDIM = "cognitive-dimension";
674        OBJPROP POSYMBOL = "po-symbol";
675
676        // -----------------------------------------------------------------------------
677
678        OBJPROP NYMS = "nyms";
679        OBJPROP ANTONYM = "antonym" <: NYMS;
680        OBJPROP HYPONYM = "hyponym" <: NYMS;
681        OBJPROP HYPERNYM = "hypernym" <: NYMS -HYPONYM;
682
683        // -----------------------------------------------------------------------------
684
685        OBJPROP FORMALIZES = "formalizes";
686        OBJPROP USES = "uses" (STATEMENT => FUNCTION);
687        { USES <super::rdfs::RANGE> <TYPE>};
688        { USES <super::rdf::TYPE> <super::owl::TRANSITIVE_PROPERTY>};
689
690        OBJPROP INSTANCE_OF = "instance-of" @ "S is an instance of O iff it is a model of O, iniherits \
691            from O, interprets O, etc.";
692
693        OBJPROP SUPERSEDED_BY = "superseded-by" @ "S (a deprecated knowledge item) is superseded by another.";
694        { SUPERSEDED_BY <super::rdf::TYPE> <super::owl::TRANSITIVE_PROPERTY>};
695
696        // -----------------------------------------------------------------------------
697
698        DATAPROP SIZE_PROPERTIES = "size-properties";
699        { SIZE_PROPERTIES <super::rdfs::DOMAIN> <super::owl::THING>};
700        { SIZE_PROPERTIES <super::rdf::TYPE> <super::owl::FUNCTIONAL_PROPERTY>};
701
702        DATAPROP AUTOMATICALLY_PROVED = "automatically-proved" <: ORGANIZATIONAL : super::xsd::STRING
703            @ "S is automatically proven by a theorem prover, O is an explanatory string.";
704        DATAPROP CHECK_TIME = "check-time" <: SIZE_PROPERTIES : super::xsd::DAY_TIME_DURATION
705            @ "time it took to check the declaration that introduced the subject.";
706        { CHECK_TIME <super::rdfs::DOMAIN> <FUNCTION>};
707        { CHECK_TIME <super::rdfs::DOMAIN> <TYPE>};
708        DATAPROP DEPRECATED = "deprecated" <: ORGANIZATIONAL : super::xsd::STRING
709            @ "S is deprecated (do not use any longer), O is an explanatory string.";
710        DATAPROP LAST_CHECKED_AT = "last-checked-at" <: SIZE_PROPERTIES : super::xsd::DATE_TIME_STAMP
711            @ "The time stamp of when the subject was last checked.";
712        { LAST_CHECKED_AT <super::rdfs::DOMAIN> <FUNCTION>};
713        { LAST_CHECKED_AT <super::rdfs::DOMAIN> <TYPE>};
714        DATAPROP SOURCEREF = "sourceref" : super::xsd::ANY_URI @ "The URI of the physical \
715            location (e.g. file/URI, line, column) of the source code that introduced the subject.";
716
717        + REMEMBER = "cd-remember";
718        + UNDERSTAND = "cd-understand";
719        + APPLY = "cd-apply";
720        + ANALYZE = "cd-analyze";
721        + EVALUATE = "cd-evaluate";
722        + CREATE = "cd-create";
723    }
724}
flams_ontology/rdf.rs

flams_ontology/
rdf.rs
