author | wenzelm |
Fri, 27 Mar 2020 22:01:27 +0100 | |
changeset 71601 | 97ccf48c2f0c |
parent 69983 | 4ce5ce3a612b |
child 75393 | 87ebf5a50283 |
permissions | -rw-r--r-- |
69807 | 1 |
/* Title: Pure/General/rdf.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Support for RDF/XML representation, see also: |
|
5 |
- https://www.w3.org/RDF |
|
6 |
- https://www.w3.org/TR/rdf-primer |
|
7 |
*/ |
|
8 |
||
9 |
package isabelle |
|
10 |
||
11 |
||
12 |
object RDF |
|
13 |
{ |
|
14 |
/* document */ |
|
15 |
||
16 |
val rdf: XML.Namespace = XML.Namespace("rdf", "http://www.w3.org/1999/02/22-rdf-syntax-ns#") |
|
69916
3235ecdcd884
more meta data from "dcterms" (superset of "dc");
wenzelm
parents:
69902
diff
changeset
|
17 |
val dcterms: XML.Namespace = XML.Namespace("dcterms", "http://purl.org/dc/terms/") |
69807 | 18 |
|
69916
3235ecdcd884
more meta data from "dcterms" (superset of "dc");
wenzelm
parents:
69902
diff
changeset
|
19 |
val default_namespaces: List[XML.Namespace] = List(rdf, dcterms) |
69807 | 20 |
|
21 |
def document(body: XML.Body, |
|
22 |
namespaces: List[XML.Namespace] = default_namespaces, |
|
23 |
attributes: XML.Attributes = Nil): XML.Elem = |
|
24 |
{ |
|
25 |
XML.Elem(Markup(rdf("RDF"), namespaces.map(_.attribute) ::: attributes), body) |
|
26 |
} |
|
27 |
||
28 |
||
29 |
/* multiple triples vs. compact description */ |
|
30 |
||
69902
9c697c7ad8d6
URIs should normally be "rdf:resource", not string body;
wenzelm
parents:
69900
diff
changeset
|
31 |
sealed case class Triple( |
9c697c7ad8d6
URIs should normally be "rdf:resource", not string body;
wenzelm
parents:
69900
diff
changeset
|
32 |
subject: String, predicate: String, `object`: XML.Body = Nil, resource: String = "") |
69807 | 33 |
{ |
69902
9c697c7ad8d6
URIs should normally be "rdf:resource", not string body;
wenzelm
parents:
69900
diff
changeset
|
34 |
require(`object`.isEmpty || resource.isEmpty) |
9c697c7ad8d6
URIs should normally be "rdf:resource", not string body;
wenzelm
parents:
69900
diff
changeset
|
35 |
|
9c697c7ad8d6
URIs should normally be "rdf:resource", not string body;
wenzelm
parents:
69900
diff
changeset
|
36 |
def property: XML.Elem = |
9c697c7ad8d6
URIs should normally be "rdf:resource", not string body;
wenzelm
parents:
69900
diff
changeset
|
37 |
if (resource.nonEmpty) XML.elem(Markup(predicate, List("rdf:resource" -> resource))) |
9c697c7ad8d6
URIs should normally be "rdf:resource", not string body;
wenzelm
parents:
69900
diff
changeset
|
38 |
else XML.elem(predicate, `object`) |
69807 | 39 |
} |
40 |
||
41 |
def triples(args: List[Triple]): XML.Body = |
|
69870
0af6b4a5a7d9
afford redundant whitespace for improved readability;
wenzelm
parents:
69868
diff
changeset
|
42 |
XML.newline :: |
0af6b4a5a7d9
afford redundant whitespace for improved readability;
wenzelm
parents:
69868
diff
changeset
|
43 |
args.zipWithIndex.groupBy({ case (t, _) => t.subject }).iterator.map(_._2). |
0af6b4a5a7d9
afford redundant whitespace for improved readability;
wenzelm
parents:
69868
diff
changeset
|
44 |
toList.sortBy(ps => ps.head._2).flatMap(ps => |
0af6b4a5a7d9
afford redundant whitespace for improved readability;
wenzelm
parents:
69868
diff
changeset
|
45 |
List( |
0af6b4a5a7d9
afford redundant whitespace for improved readability;
wenzelm
parents:
69868
diff
changeset
|
46 |
description(ps.head._1.subject, |
0af6b4a5a7d9
afford redundant whitespace for improved readability;
wenzelm
parents:
69868
diff
changeset
|
47 |
XML.newline :: ps.flatMap({ case (t, _) => List(t.property, XML.newline) })), |
0af6b4a5a7d9
afford redundant whitespace for improved readability;
wenzelm
parents:
69868
diff
changeset
|
48 |
XML.newline)) |
69807 | 49 |
|
50 |
def description(subject: String, body: XML.Body, attributes: XML.Attributes = Nil): XML.Elem = |
|
51 |
XML.Elem(Markup(rdf("Description"), (rdf("about"), subject) :: attributes), body) |
|
69808 | 52 |
|
53 |
||
54 |
/* collections */ |
|
55 |
||
56 |
def collection(kind: String, items: List[XML.Body]): XML.Elem = |
|
57 |
XML.elem(kind, items.map(item => XML.elem(rdf("li"), item))) |
|
58 |
||
59 |
def bag(items: List[XML.Body]): XML.Elem = collection(rdf("Bag"), items) |
|
60 |
def seq(items: List[XML.Body]): XML.Elem = collection(rdf("Seq"), items) |
|
61 |
def alt(items: List[XML.Body]): XML.Elem = collection(rdf("Alt"), items) |
|
69809 | 62 |
|
63 |
||
64 |
/* datatypes */ |
|
65 |
||
66 |
// see https://www.w3.org/TR/rdf11-concepts/#section-Datatypes |
|
67 |
// see https://www.w3.org/TR/xmlschema-2/#built-in-datatypes |
|
68 |
||
69 |
def string(x: String): XML.Body = if (x.isEmpty) Nil else List(XML.Text(x)) |
|
70 |
def bool(x: Boolean): XML.Body = string(x.toString) |
|
71 |
def int(x: Int): XML.Body = string(Value.Int(x)) |
|
72 |
def long(x: Long): XML.Body = string(Value.Long(x)) |
|
73 |
def double(x: Double): XML.Body = string(Value.Double(x)) |
|
74 |
def seconds(x: Time): XML.Body = double(x.seconds) |
|
69982 | 75 |
|
76 |
val date_format: Date.Format = Date.Format("uuuu-MM-dd'T'HH:mm:ss.SSSxxx") |
|
77 |
def date_time_stamp(x: Date): XML.Body = string(date_format(x)) |
|
69858 | 78 |
|
79 |
||
80 |
/* predicates */ |
|
81 |
||
82 |
object Property // binary relation with plain value |
|
83 |
{ |
|
69983
4ce5ce3a612b
more robust: avoid NPE due to odd problems with object initialization;
wenzelm
parents:
69982
diff
changeset
|
84 |
def title: String = dcterms("title") |
4ce5ce3a612b
more robust: avoid NPE due to odd problems with object initialization;
wenzelm
parents:
69982
diff
changeset
|
85 |
def creator: String = dcterms("creator") |
4ce5ce3a612b
more robust: avoid NPE due to odd problems with object initialization;
wenzelm
parents:
69982
diff
changeset
|
86 |
def contributor: String = dcterms("contributor") |
4ce5ce3a612b
more robust: avoid NPE due to odd problems with object initialization;
wenzelm
parents:
69982
diff
changeset
|
87 |
def date: String = dcterms("date") |
4ce5ce3a612b
more robust: avoid NPE due to odd problems with object initialization;
wenzelm
parents:
69982
diff
changeset
|
88 |
def license: String = dcterms("license") |
4ce5ce3a612b
more robust: avoid NPE due to odd problems with object initialization;
wenzelm
parents:
69982
diff
changeset
|
89 |
def description: String = dcterms("description") |
69858 | 90 |
} |
69900 | 91 |
|
69983
4ce5ce3a612b
more robust: avoid NPE due to odd problems with object initialization;
wenzelm
parents:
69982
diff
changeset
|
92 |
private lazy val meta_data_table = |
69900 | 93 |
Map( |
94 |
Markup.META_TITLE -> Property.title, |
|
95 |
Markup.META_CREATOR -> Property.creator, |
|
96 |
Markup.META_CONTRIBUTOR -> Property.contributor, |
|
97 |
Markup.META_DATE -> Property.date, |
|
69982 | 98 |
Markup.META_LICENSE -> Property.license, |
99 |
Markup.META_DESCRIPTION -> Property.description) |
|
69900 | 100 |
|
101 |
def meta_data(props: Properties.T): Properties.T = |
|
102 |
props.flatMap({ case (a, b) => meta_data_table.get(a).map((_, b)) }) |
|
69807 | 103 |
} |