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