author | wenzelm |
Sat, 07 Aug 2010 21:03:06 +0200 | |
changeset 38228 | ada3ab6b9085 |
parent 33392 | 73c8987dc9f0 |
permissions | -rw-r--r-- |
20658 | 1 |
(* Title: Pure/Tools/xml_syntax.ML |
2 |
Author: Stefan Berghofer, TU Muenchen |
|
3 |
||
4 |
Input and output of types, terms, and proofs in XML format. |
|
5 |
See isabelle.xsd for a description of the syntax. |
|
6 |
*) |
|
7 |
||
8 |
signature XML_SYNTAX = |
|
9 |
sig |
|
10 |
val xml_of_type: typ -> XML.tree |
|
11 |
val xml_of_term: term -> XML.tree |
|
12 |
val xml_of_proof: Proofterm.proof -> XML.tree |
|
21645
4af699cdfe47
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
20658
diff
changeset
|
13 |
val write_to_file: Path.T -> string -> XML.tree -> unit |
20658 | 14 |
exception XML of string * XML.tree |
15 |
val type_of_xml: XML.tree -> typ |
|
16 |
val term_of_xml: XML.tree -> term |
|
17 |
val proof_of_xml: XML.tree -> Proofterm.proof |
|
18 |
end; |
|
19 |
||
33392 | 20 |
structure XML_Syntax : XML_SYNTAX = |
20658 | 21 |
struct |
22 |
||
23 |
(**** XML output ****) |
|
24 |
||
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
25 |
fun xml_of_class name = XML.Elem (("class", [("name", name)]), []); |
20658 | 26 |
|
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
27 |
fun xml_of_type (TVar ((s, i), S)) = |
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
28 |
XML.Elem (("TVar", ("name", s) :: (if i=0 then [] else [("index", string_of_int i)])), |
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
29 |
map xml_of_class S) |
20658 | 30 |
| xml_of_type (TFree (s, S)) = |
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
31 |
XML.Elem (("TFree", [("name", s)]), map xml_of_class S) |
20658 | 32 |
| xml_of_type (Type (s, Ts)) = |
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
33 |
XML.Elem (("Type", [("name", s)]), map xml_of_type Ts); |
20658 | 34 |
|
35 |
fun xml_of_term (Bound i) = |
|
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
36 |
XML.Elem (("Bound", [("index", string_of_int i)]), []) |
20658 | 37 |
| xml_of_term (Free (s, T)) = |
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
38 |
XML.Elem (("Free", [("name", s)]), [xml_of_type T]) |
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
39 |
| xml_of_term (Var ((s, i), T)) = |
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
40 |
XML.Elem (("Var", ("name", s) :: (if i=0 then [] else [("index", string_of_int i)])), |
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
41 |
[xml_of_type T]) |
20658 | 42 |
| xml_of_term (Const (s, T)) = |
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
43 |
XML.Elem (("Const", [("name", s)]), [xml_of_type T]) |
20658 | 44 |
| xml_of_term (t $ u) = |
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
45 |
XML.Elem (("App", []), [xml_of_term t, xml_of_term u]) |
20658 | 46 |
| xml_of_term (Abs (s, T, t)) = |
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
47 |
XML.Elem (("Abs", [("vname", s)]), [xml_of_type T, xml_of_term t]); |
20658 | 48 |
|
49 |
fun xml_of_opttypes NONE = [] |
|
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
50 |
| xml_of_opttypes (SOME Ts) = [XML.Elem (("types", []), map xml_of_type Ts)]; |
20658 | 51 |
|
52 |
(* FIXME: the t argument of PThm and PAxm is actually redundant, since *) |
|
53 |
(* it can be looked up in the theorem database. Thus, it could be *) |
|
54 |
(* omitted from the xml representation. *) |
|
55 |
||
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
56 |
(* FIXME not exhaustive *) |
20658 | 57 |
fun xml_of_proof (PBound i) = |
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
58 |
XML.Elem (("PBound", [("index", string_of_int i)]), []) |
20658 | 59 |
| xml_of_proof (Abst (s, optT, prf)) = |
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
60 |
XML.Elem (("Abst", [("vname", s)]), |
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
61 |
(case optT of NONE => [] | SOME T => [xml_of_type T]) @ [xml_of_proof prf]) |
20658 | 62 |
| xml_of_proof (AbsP (s, optt, prf)) = |
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
63 |
XML.Elem (("AbsP", [("vname", s)]), |
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
64 |
(case optt of NONE => [] | SOME t => [xml_of_term t]) @ [xml_of_proof prf]) |
20658 | 65 |
| xml_of_proof (prf % optt) = |
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
66 |
XML.Elem (("Appt", []), |
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
67 |
xml_of_proof prf :: (case optt of NONE => [] | SOME t => [xml_of_term t])) |
20658 | 68 |
| xml_of_proof (prf %% prf') = |
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
69 |
XML.Elem (("AppP", []), [xml_of_proof prf, xml_of_proof prf']) |
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
70 |
| xml_of_proof (Hyp t) = XML.Elem (("Hyp", []), [xml_of_term t]) |
28811 | 71 |
| xml_of_proof (PThm (_, ((s, t, optTs), _))) = |
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
72 |
XML.Elem (("PThm", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs) |
20658 | 73 |
| xml_of_proof (PAxm (s, t, optTs)) = |
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
74 |
XML.Elem (("PAxm", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs) |
20658 | 75 |
| xml_of_proof (Oracle (s, t, optTs)) = |
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
76 |
XML.Elem (("Oracle", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs) |
28811 | 77 |
| xml_of_proof MinProof = |
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
78 |
XML.Elem (("MinProof", []), []); |
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
79 |
|
20658 | 80 |
|
81 |
(* useful for checking the output against a schema file *) |
|
82 |
||
21645
4af699cdfe47
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
20658
diff
changeset
|
83 |
fun write_to_file path elname x = |
4af699cdfe47
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
20658
diff
changeset
|
84 |
File.write path |
20658 | 85 |
("<?xml version=\"1.0\" encoding=\"UTF-8\"?>\n" ^ |
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
86 |
XML.string_of (XML.Elem ((elname, |
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
87 |
[("xmlns:xsi", "http://www.w3.org/2001/XMLSchema-instance"), |
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
88 |
("xsi:noNamespaceSchemaLocation", "isabelle.xsd")]), |
20658 | 89 |
[x]))); |
90 |
||
91 |
||
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
92 |
|
20658 | 93 |
(**** XML input ****) |
94 |
||
95 |
exception XML of string * XML.tree; |
|
96 |
||
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
97 |
fun class_of_xml (XML.Elem (("class", [("name", name)]), [])) = name |
20658 | 98 |
| class_of_xml tree = raise XML ("class_of_xml: bad tree", tree); |
99 |
||
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
100 |
fun index_of_string s tree idx = |
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
101 |
(case Int.fromString idx of |
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
102 |
NONE => raise XML (s ^ ": bad index", tree) |
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
103 |
| SOME i => i); |
20658 | 104 |
|
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
105 |
fun type_of_xml (tree as XML.Elem (("TVar", atts), classes)) = TVar |
28017 | 106 |
((case Properties.get atts "name" of |
20658 | 107 |
NONE => raise XML ("type_of_xml: name of TVar missing", tree) |
108 |
| SOME name => name, |
|
109 |
the_default 0 (Option.map (index_of_string "type_of_xml" tree) |
|
28017 | 110 |
(Properties.get atts "index"))), |
20658 | 111 |
map class_of_xml classes) |
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
112 |
| type_of_xml (XML.Elem (("TFree", [("name", s)]), classes)) = |
20658 | 113 |
TFree (s, map class_of_xml classes) |
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
114 |
| type_of_xml (XML.Elem (("Type", [("name", s)]), types)) = |
20658 | 115 |
Type (s, map type_of_xml types) |
116 |
| type_of_xml tree = raise XML ("type_of_xml: bad tree", tree); |
|
117 |
||
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
118 |
fun term_of_xml (tree as XML.Elem (("Bound", [("index", idx)]), [])) = |
20658 | 119 |
Bound (index_of_string "bad variable index" tree idx) |
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
120 |
| term_of_xml (XML.Elem (("Free", [("name", s)]), [typ])) = |
20658 | 121 |
Free (s, type_of_xml typ) |
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
122 |
| term_of_xml (tree as XML.Elem (("Var", atts), [typ])) = Var |
28017 | 123 |
((case Properties.get atts "name" of |
20658 | 124 |
NONE => raise XML ("type_of_xml: name of Var missing", tree) |
125 |
| SOME name => name, |
|
126 |
the_default 0 (Option.map (index_of_string "term_of_xml" tree) |
|
28017 | 127 |
(Properties.get atts "index"))), |
20658 | 128 |
type_of_xml typ) |
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
129 |
| term_of_xml (XML.Elem (("Const", [("name", s)]), [typ])) = |
20658 | 130 |
Const (s, type_of_xml typ) |
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
131 |
| term_of_xml (XML.Elem (("App", []), [term, term'])) = |
20658 | 132 |
term_of_xml term $ term_of_xml term' |
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
133 |
| term_of_xml (XML.Elem (("Abs", [("vname", s)]), [typ, term])) = |
20658 | 134 |
Abs (s, type_of_xml typ, term_of_xml term) |
135 |
| term_of_xml tree = raise XML ("term_of_xml: bad tree", tree); |
|
136 |
||
137 |
fun opttypes_of_xml [] = NONE |
|
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
138 |
| opttypes_of_xml [XML.Elem (("types", []), types)] = |
20658 | 139 |
SOME (map type_of_xml types) |
140 |
| opttypes_of_xml (tree :: _) = raise XML ("opttypes_of_xml: bad tree", tree); |
|
141 |
||
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
142 |
fun proof_of_xml (tree as XML.Elem (("PBound", [("index", idx)]), [])) = |
20658 | 143 |
PBound (index_of_string "proof_of_xml" tree idx) |
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
144 |
| proof_of_xml (XML.Elem (("Abst", [("vname", s)]), [proof])) = |
20658 | 145 |
Abst (s, NONE, proof_of_xml proof) |
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
146 |
| proof_of_xml (XML.Elem (("Abst", [("vname", s)]), [typ, proof])) = |
20658 | 147 |
Abst (s, SOME (type_of_xml typ), proof_of_xml proof) |
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
148 |
| proof_of_xml (XML.Elem (("AbsP", [("vname", s)]), [proof])) = |
20658 | 149 |
AbsP (s, NONE, proof_of_xml proof) |
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
150 |
| proof_of_xml (XML.Elem (("AbsP", [("vname", s)]), [term, proof])) = |
20658 | 151 |
AbsP (s, SOME (term_of_xml term), proof_of_xml proof) |
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
152 |
| proof_of_xml (XML.Elem (("Appt", []), [proof])) = |
20658 | 153 |
proof_of_xml proof % NONE |
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
154 |
| proof_of_xml (XML.Elem (("Appt", []), [proof, term])) = |
20658 | 155 |
proof_of_xml proof % SOME (term_of_xml term) |
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
156 |
| proof_of_xml (XML.Elem (("AppP", []), [proof, proof'])) = |
20658 | 157 |
proof_of_xml proof %% proof_of_xml proof' |
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
158 |
| proof_of_xml (XML.Elem (("Hyp", []), [term])) = |
23831
64e6e5c738a1
Added clause for hypotheses to proof_of_xml function.
berghofe
parents:
21645
diff
changeset
|
159 |
Hyp (term_of_xml term) |
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
160 |
| proof_of_xml (XML.Elem (("PThm", [("name", s)]), term :: opttypes)) = |
28811 | 161 |
(* FIXME? *) |
162 |
PThm (serial (), ((s, term_of_xml term, opttypes_of_xml opttypes), |
|
30718 | 163 |
Future.value (Proofterm.approximate_proof_body MinProof))) |
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
164 |
| proof_of_xml (XML.Elem (("PAxm", [("name", s)]), term :: opttypes)) = |
20658 | 165 |
PAxm (s, term_of_xml term, opttypes_of_xml opttypes) |
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
166 |
| proof_of_xml (XML.Elem (("Oracle", [("name", s)]), term :: opttypes)) = |
20658 | 167 |
Oracle (s, term_of_xml term, opttypes_of_xml opttypes) |
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
33392
diff
changeset
|
168 |
| proof_of_xml (XML.Elem (("MinProof", _), _)) = MinProof |
20658 | 169 |
| proof_of_xml tree = raise XML ("proof_of_xml: bad tree", tree); |
170 |
||
171 |
end; |