author | wenzelm |
Mon, 25 Mar 2019 16:45:08 +0100 | |
changeset 69980 | f2e3adfd916f |
parent 69916 | 3235ecdcd884 |
child 69982 | f150253cb201 |
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) |
|
75 |
def date_time_stamp(x: Date): XML.Body = string(Date.Format("uuuu-MM-dd'T'HH:mm:ss.SSSxxx")(x)) |
|
69858 | 76 |
|
77 |
||
78 |
/* predicates */ |
|
79 |
||
80 |
object Property // binary relation with plain value |
|
81 |
{ |
|
69916
3235ecdcd884
more meta data from "dcterms" (superset of "dc");
wenzelm
parents:
69902
diff
changeset
|
82 |
val title: String = dcterms("title") |
3235ecdcd884
more meta data from "dcterms" (superset of "dc");
wenzelm
parents:
69902
diff
changeset
|
83 |
val creator: String = dcterms("creator") |
3235ecdcd884
more meta data from "dcterms" (superset of "dc");
wenzelm
parents:
69902
diff
changeset
|
84 |
val contributor: String = dcterms("contributor") |
3235ecdcd884
more meta data from "dcterms" (superset of "dc");
wenzelm
parents:
69902
diff
changeset
|
85 |
val date: String = dcterms("date") |
3235ecdcd884
more meta data from "dcterms" (superset of "dc");
wenzelm
parents:
69902
diff
changeset
|
86 |
val description: String = dcterms("description") |
3235ecdcd884
more meta data from "dcterms" (superset of "dc");
wenzelm
parents:
69902
diff
changeset
|
87 |
val license: String = dcterms("license") |
69858 | 88 |
} |
69900 | 89 |
|
90 |
private val meta_data_table = |
|
91 |
Map( |
|
92 |
Markup.META_TITLE -> Property.title, |
|
93 |
Markup.META_CREATOR -> Property.creator, |
|
94 |
Markup.META_CONTRIBUTOR -> Property.contributor, |
|
95 |
Markup.META_DATE -> Property.date, |
|
69916
3235ecdcd884
more meta data from "dcterms" (superset of "dc");
wenzelm
parents:
69902
diff
changeset
|
96 |
Markup.META_DESCRIPTION -> Property.description, |
3235ecdcd884
more meta data from "dcterms" (superset of "dc");
wenzelm
parents:
69902
diff
changeset
|
97 |
Markup.META_LICENSE -> Property.license) |
69900 | 98 |
|
99 |
def meta_data(props: Properties.T): Properties.T = |
|
100 |
props.flatMap({ case (a, b) => meta_data_table.get(a).map((_, b)) }) |
|
69807 | 101 |
} |