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