author | wenzelm |
Tue, 05 Mar 2019 11:52:20 +0100 | |
changeset 69862 | db622ada496d |
parent 69858 | 3d0f27273aa1 |
child 69867 | 3fd9298dd200 |
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 |
||
69809 | 12 |
import java.net.URI |
13 |
||
14 |
||
69807 | 15 |
object RDF |
16 |
{ |
|
17 |
/* document */ |
|
18 |
||
19 |
val rdf: XML.Namespace = XML.Namespace("rdf", "http://www.w3.org/1999/02/22-rdf-syntax-ns#") |
|
20 |
val dc: XML.Namespace = XML.Namespace("dc", "http://purl.org/dc/elements/1.1/") |
|
21 |
||
22 |
val default_namespaces: List[XML.Namespace] = List(rdf, dc) |
|
23 |
||
24 |
def document(body: XML.Body, |
|
25 |
namespaces: List[XML.Namespace] = default_namespaces, |
|
26 |
attributes: XML.Attributes = Nil): XML.Elem = |
|
27 |
{ |
|
28 |
XML.Elem(Markup(rdf("RDF"), namespaces.map(_.attribute) ::: attributes), body) |
|
29 |
} |
|
30 |
||
31 |
||
32 |
/* multiple triples vs. compact description */ |
|
33 |
||
34 |
sealed case class Triple(subject: String, predicate: String, `object`: XML.Body) |
|
35 |
{ |
|
36 |
def property: XML.Elem = XML.elem(predicate, `object`) |
|
37 |
} |
|
38 |
||
39 |
def triples(args: List[Triple]): XML.Body = |
|
40 |
args.groupBy(_.subject).toList.map( |
|
69862
db622ada496d
afford redundant whitespace for improved readability;
wenzelm
parents:
69858
diff
changeset
|
41 |
{ case (subject, ts) => |
db622ada496d
afford redundant whitespace for improved readability;
wenzelm
parents:
69858
diff
changeset
|
42 |
val nl = XML.Text("\n") |
db622ada496d
afford redundant whitespace for improved readability;
wenzelm
parents:
69858
diff
changeset
|
43 |
val body = nl :: ts.flatMap(t => List(t.property, nl)) |
db622ada496d
afford redundant whitespace for improved readability;
wenzelm
parents:
69858
diff
changeset
|
44 |
description(subject, body) |
db622ada496d
afford redundant whitespace for improved readability;
wenzelm
parents:
69858
diff
changeset
|
45 |
}) |
69807 | 46 |
|
47 |
def description(subject: String, body: XML.Body, attributes: XML.Attributes = Nil): XML.Elem = |
|
48 |
XML.Elem(Markup(rdf("Description"), (rdf("about"), subject) :: attributes), body) |
|
69808 | 49 |
|
50 |
||
51 |
/* collections */ |
|
52 |
||
53 |
def collection(kind: String, items: List[XML.Body]): XML.Elem = |
|
54 |
XML.elem(kind, items.map(item => XML.elem(rdf("li"), item))) |
|
55 |
||
56 |
def bag(items: List[XML.Body]): XML.Elem = collection(rdf("Bag"), items) |
|
57 |
def seq(items: List[XML.Body]): XML.Elem = collection(rdf("Seq"), items) |
|
58 |
def alt(items: List[XML.Body]): XML.Elem = collection(rdf("Alt"), items) |
|
69809 | 59 |
|
60 |
||
61 |
/* datatypes */ |
|
62 |
||
63 |
// see https://www.w3.org/TR/rdf11-concepts/#section-Datatypes |
|
64 |
// see https://www.w3.org/TR/xmlschema-2/#built-in-datatypes |
|
65 |
||
66 |
def string(x: String): XML.Body = if (x.isEmpty) Nil else List(XML.Text(x)) |
|
67 |
def uri(x: URI): XML.Body = string(x.toString) |
|
68 |
def bool(x: Boolean): XML.Body = string(x.toString) |
|
69 |
def int(x: Int): XML.Body = string(Value.Int(x)) |
|
70 |
def long(x: Long): XML.Body = string(Value.Long(x)) |
|
71 |
def double(x: Double): XML.Body = string(Value.Double(x)) |
|
72 |
def seconds(x: Time): XML.Body = double(x.seconds) |
|
73 |
def date_time_stamp(x: Date): XML.Body = string(Date.Format("uuuu-MM-dd'T'HH:mm:ss.SSSxxx")(x)) |
|
69858 | 74 |
|
75 |
||
76 |
/* predicates */ |
|
77 |
||
78 |
object Property // binary relation with plain value |
|
79 |
{ |
|
80 |
val title: String = dc("title") |
|
81 |
val creator: String = dc("creator") |
|
82 |
val contributor: String = dc("contributor") |
|
83 |
val date: String = dc("date") |
|
84 |
val description: String = dc("description") |
|
85 |
} |
|
69807 | 86 |
} |