neuper@37906
|
1 |
(* translate formulae from Isabelle-string format to xml-format.
|
neuper@37906
|
2 |
TODO implement MathML
|
neuper@37906
|
3 |
author: Walther Neuper 030701
|
neuper@37906
|
4 |
(c) isac-team 2003
|
neuper@37906
|
5 |
*)
|
neuper@37906
|
6 |
|
neuper@37906
|
7 |
(*.decode Isabelle-strings to the format as seen by the user (1)
|
neuper@37906
|
8 |
EXCEPT xml-coding issues (2).
|
neuper@37906
|
9 |
(2) have a _reverse_ method
|
neuper@37906
|
10 |
'isac.util.parser.FormalizationDigest.decodeEntities'
|
neuper@37906
|
11 |
called within Formula#toSMLString in java
|
neuper@37906
|
12 |
|
neuper@37947
|
13 |
ad(1) decode "^^^" ---> "^"; see Knowledge/Atools.thy;
|
neuper@37906
|
14 |
ad(2) decode "<" ---> "<", decode ">" ---> ">"
|
neuper@37906
|
15 |
decode "&" ---> "&"
|
wneuper@59260
|
16 |
called for term2xml; + see "fun encode" below*)
|
wneuper@59416
|
17 |
fun decode (str: Rule.cterm') =
|
neuper@37906
|
18 |
let fun dec [] = []
|
neuper@37906
|
19 |
| dec ("^"::"^"::"^"::cs) = "^"::(dec cs)
|
neuper@37906
|
20 |
| dec ("&"::cs) = "&"::"a"::"m"::"p"::";"::(dec cs)
|
neuper@37906
|
21 |
| dec ("<"::cs) = "&"::"l"::"t"::";"::(dec cs)
|
neuper@37906
|
22 |
| dec (">"::cs) = "&"::"g"::"t"::";"::(dec cs)
|
neuper@37906
|
23 |
| dec (c::cs) = c::(dec cs)
|
wneuper@59416
|
24 |
in (implode o dec o Symbol.explode) str: Rule.cterm' end;
|
wneuper@59177
|
25 |
|
wneuper@59177
|
26 |
fun dop_leading _ [] = []
|
wneuper@59177
|
27 |
| dop_leading c (c' :: cs) =
|
wneuper@59177
|
28 |
if c = c' then dop_leading c cs else (c' :: cs)
|
wneuper@59177
|
29 |
fun rm_doublets _ singled [] = singled
|
wneuper@59177
|
30 |
| rm_doublets c singled (c' :: cs) =
|
wneuper@59177
|
31 |
if c = c'
|
wneuper@59177
|
32 |
then
|
wneuper@59177
|
33 |
let val cs' = dop_leading "^" cs
|
wneuper@59177
|
34 |
in rm_doublets c (singled @ [c']) cs' end
|
wneuper@59177
|
35 |
else rm_doublets c (singled @ [c']) cs
|
wneuper@59416
|
36 |
fun encode (str : Rule.cterm') =
|
wneuper@59154
|
37 |
let fun enc [] = []
|
wneuper@59154
|
38 |
| enc ("^" :: cs) = "^" :: "^" :: "^" :: (enc cs)
|
wneuper@59154
|
39 |
| enc (c :: cs) = c :: (enc cs)
|
wneuper@59177
|
40 |
in str |> Symbol.explode |> rm_doublets "^" [] |> enc |> implode end;
|
neuper@37906
|
41 |
|
wneuper@59154
|
42 |
val indentation = 2;
|
wneuper@59154
|
43 |
|
walther@59612
|
44 |
(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
|
wneuper@59154
|
45 |
local
|
wneuper@59154
|
46 |
fun indent i = fold (curry op ^) (replicate i ". ") ""
|
wneuper@59154
|
47 |
in
|
wneuper@59224
|
48 |
(* proper <> is translated to html; however, () creates readable output.. *)
|
wneuper@59154
|
49 |
fun xmlstr i (XML.Text str) = indent i ^ str ^ "\n"
|
wneuper@59224
|
50 |
| xmlstr i (XML.Elem (("TERM", []), [xt])) =
|
wneuper@59224
|
51 |
indent i ^ "(" ^ "TERM" ^ ")" ^ "\n" ^
|
wneuper@59469
|
52 |
indent (i + 1) ^ (xt |> Codec.decode Codec.term |> Codec.the_success |> Rule.term2str) ^ "\n" ^
|
wneuper@59224
|
53 |
indent i ^ "(/" ^ "TERM" ^ ")" ^ "\n"
|
wneuper@59154
|
54 |
| xmlstr i (XML.Elem ((str, []), trees)) =
|
wneuper@59163
|
55 |
indent i ^ "(" ^ str ^ ")" ^ "\n" ^
|
wneuper@59154
|
56 |
List.foldr op ^ "" (map (xmlstr (i + 1)) trees) ^
|
wneuper@59163
|
57 |
indent i ^ "(/" ^ str ^ ")" ^ "\n"
|
wneuper@59158
|
58 |
| xmlstr i (XML.Elem ((str, [(flag, value)]), trees)) =
|
wneuper@59163
|
59 |
indent i ^ "(" ^ str ^ " " ^ flag ^ "=" ^ value ^ ")" ^ "\n" ^
|
wneuper@59154
|
60 |
List.foldr op ^ "" (map (xmlstr (i + 1)) trees) ^
|
wneuper@59163
|
61 |
indent i ^ "(/" ^ str ^ ")" ^ "\n"
|
wneuper@59154
|
62 |
| xmlstr _ (XML.Elem ((_, (_ :: _)), _)) =
|
wneuper@59154
|
63 |
error "xmlstr: TODO review attribute \"status\" etc";
|
wneuper@59154
|
64 |
end
|
walther@59612
|
65 |
( *\\---------------------------------- rm libisabelle ---------------------------------------//*)
|
neuper@37906
|
66 |
|
neuper@37906
|
67 |
fun strs2xml strs = foldl (op ^) ("", strs);
|
neuper@38031
|
68 |
(* writeln (strs2xml ["<XXX> xxx </XXX>\n","<YYY> yyy </YYY>\n"]);
|
neuper@37906
|
69 |
<XXX> xxx </XXX>
|
neuper@37906
|
70 |
<YYY> yyy </YYY>*)
|
neuper@37906
|
71 |
|
neuper@37906
|
72 |
val indentation = 2;
|
neuper@37906
|
73 |
val i = indentation;
|
neuper@37906
|
74 |
|
neuper@37947
|
75 |
(*WN071016 checked that _all_ Frontend/interface.sml uses this*)
|
neuper@37906
|
76 |
fun term2xml j t =
|
neuper@37906
|
77 |
indt (j+i) ^ "<MATHML>\n" ^
|
wneuper@59416
|
78 |
indt (j+2*i) ^ "<ISA> " ^ (decode o Rule.term2str) t ^ " </ISA>\n" ^
|
neuper@37906
|
79 |
indt (j+i) ^ "</MATHML>";
|
neuper@37906
|
80 |
(*val t = str2term "equality e_";
|
neuper@38031
|
81 |
writeln (term2xml 8 t);
|
neuper@37906
|
82 |
<MATHML>
|
neuper@37906
|
83 |
<ISA> equality e_ </ISA>
|
neuper@37906
|
84 |
<MATHML> *)
|
walther@59612
|
85 |
(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
|
wneuper@59127
|
86 |
fun xml_of_term t =
|
wneuper@59127
|
87 |
XML.Elem (("MATHML", []),
|
wneuper@59416
|
88 |
[XML.Elem (("ISA", []), [XML.Text ((decode o Rule.term2str) t)])])
|
wneuper@59127
|
89 |
fun xml_of_terms ts = map xml_of_term ts
|
wneuper@59154
|
90 |
fun xml_to_term
|
wneuper@59221
|
91 |
((XML.Elem (("MATHML", []), [
|
wneuper@59389
|
92 |
XML.Elem (("ISA", []), [XML.Text str])]))) = str |> encode |> TermC.str2term
|
wneuper@59154
|
93 |
| xml_to_term xx = raise ERROR ("xml_to_term wrong arg: " ^ xmlstr 0 xx)
|
wneuper@59221
|
94 |
fun xml_to_term_NEW
|
wneuper@59221
|
95 |
((XML.Elem (("FORMULA", []), [
|
wneuper@59389
|
96 |
XML.Elem (("ISA", []), [XML.Text str])]))) = str |> encode |> TermC.str2term
|
wneuper@59221
|
97 |
| xml_to_term_NEW xx = raise ERROR ("xml_to_term_NEW wrong arg: " ^ xmlstr 0 xx)
|
wneuper@59154
|
98 |
fun xml_to_terms ts = map xml_to_term ts
|
wneuper@59221
|
99 |
fun xml_to_terms_NEW ts = map xml_to_term_NEW ts
|
wneuper@59211
|
100 |
|
wneuper@59211
|
101 |
(* intermediate replacements while introducing transfer of terms by libisabelle *)
|
wneuper@59458
|
102 |
fun xml_of_term_NEW (t : term) =
|
wneuper@59222
|
103 |
XML.Elem (("FORMULA", []), [
|
wneuper@59469
|
104 |
XML.Elem (("ISA", []), [XML.Text ((decode o Rule.term2str) t)]),
|
wneuper@59469
|
105 |
XML.Elem (("TERM", []), [Codec.encode Codec.term t])])
|
wneuper@59221
|
106 |
(* unused: formulas come as strings from frontend and are parsed by Isabelle *)
|
wneuper@59221
|
107 |
fun xml_to_term_UNUSED
|
wneuper@59221
|
108 |
((XML.Elem (("FORMULA", []), [
|
wneuper@59211
|
109 |
XML.Elem (("ISA", []), [XML.Text _]),
|
wneuper@59469
|
110 |
XML.Elem (("TERM", []), [xt])]))) = xt |> Codec.decode Codec.term |> Codec.the_success
|
wneuper@59221
|
111 |
| xml_to_term_UNUSED xx = raise ERROR ("xml_to_term_NEW wrong arg: " ^ xmlstr 0 xx)
|
walther@59612
|
112 |
( *\\---------------------------------- rm libisabelle ---------------------------------------//*)
|
neuper@37906
|
113 |
|
neuper@37906
|
114 |
(*version for TextIO*)
|
neuper@37906
|
115 |
fun terms2xml j [] = ""
|
neuper@37906
|
116 |
| terms2xml j (t::ts) = term2xml j t ^ terms2xml j ts;
|
neuper@38031
|
117 |
(*version for writeln: extra \n*)
|
neuper@37906
|
118 |
fun terms2xml' j [] = ""
|
neuper@37906
|
119 |
| terms2xml' j [t] = term2xml j t
|
neuper@37906
|
120 |
| terms2xml' j (t::ts) = term2xml j t ^"\n"^ terms2xml' j ts;
|
neuper@37906
|
121 |
|
neuper@37906
|
122 |
(*WN060513 'cterm' means the Isabelle-type*)
|
neuper@37906
|
123 |
fun cterm2xml j ct =
|
neuper@37906
|
124 |
indt (j+i) ^ "<MATHML>\n" ^
|
neuper@37906
|
125 |
indt (j+2*i) ^ "<ISA> " ^ ct ^ " </ISA>\n" ^
|
neuper@37906
|
126 |
indt (j+i) ^ "</MATHML>\n";
|
walther@59612
|
127 |
(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
|
wneuper@59127
|
128 |
fun xml_of_cterm ct =
|
wneuper@59127
|
129 |
XML.Elem (("MATHML", []),
|
wneuper@59127
|
130 |
[XML.Elem (("ISA", []), [XML.Text ct])])
|
wneuper@59155
|
131 |
fun xml_to_cterm
|
wneuper@59155
|
132 |
(XML.Elem (("MATHML", []),
|
wneuper@59155
|
133 |
[XML.Elem (("ISA", []), [XML.Text ct])])) = ct
|
wneuper@59155
|
134 |
| xml_to_cterm x = raise ERROR ("xml_to_cterm wrong arg: " ^ xmlstr 0 x)
|
walther@59612
|
135 |
( *\\---------------------------------- rm libisabelle ---------------------------------------//*)
|
wneuper@59127
|
136 |
|
neuper@37906
|
137 |
(*version for TextIO*)
|
neuper@37906
|
138 |
fun cterms2xml j [] = ""
|
neuper@37906
|
139 |
| cterms2xml j (t::ts) = cterm2xml j t ^ cterms2xml j ts;
|
neuper@38031
|
140 |
(*version for writeln: extra \n*)
|
neuper@37906
|
141 |
fun cterms2xml' j [] = ""
|
neuper@37906
|
142 |
| cterms2xml' j (t::ts) = cterm2xml j t ^"\n"^ cterms2xml j ts;
|
neuper@37906
|
143 |
|
neuper@38031
|
144 |
(* writeln(cterms2xml 5 ["cterm1", "cterm2"]);
|
neuper@37906
|
145 |
<MATHML>
|
neuper@37906
|
146 |
<ISA> cterm1 </ISA>
|
neuper@37906
|
147 |
</MATHML>
|
neuper@37906
|
148 |
<MATHML>
|
neuper@37906
|
149 |
<ISA> cterm2 </ISA>
|
neuper@37906
|
150 |
</MATHML>
|
neuper@37906
|
151 |
*) |