1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/BridgeLibisabelle/mathml.sml Wed Aug 28 11:21:26 2019 +0200
1.3 @@ -0,0 +1,145 @@
1.4 +(* translate formulae from Isabelle-string format to xml-format.
1.5 + TODO implement MathML
1.6 + author: Walther Neuper 030701
1.7 + (c) isac-team 2003
1.8 +*)
1.9 +
1.10 +(*.decode Isabelle-strings to the format as seen by the user (1)
1.11 + EXCEPT xml-coding issues (2).
1.12 + (2) have a _reverse_ method
1.13 + 'isac.util.parser.FormalizationDigest.decodeEntities'
1.14 + called within Formula#toSMLString in java
1.15 +
1.16 + ad(1) decode "^^^" ---> "^"; see Knowledge/Atools.thy;
1.17 + ad(2) decode "<" ---> "<", decode ">" ---> ">"
1.18 + decode "&" ---> "&"
1.19 + called for term2xml; + see "fun encode" below*)
1.20 +fun decode (str: Rule.cterm') =
1.21 + let fun dec [] = []
1.22 + | dec ("^"::"^"::"^"::cs) = "^"::(dec cs)
1.23 + | dec ("&"::cs) = "&"::"a"::"m"::"p"::";"::(dec cs)
1.24 + | dec ("<"::cs) = "&"::"l"::"t"::";"::(dec cs)
1.25 + | dec (">"::cs) = "&"::"g"::"t"::";"::(dec cs)
1.26 + | dec (c::cs) = c::(dec cs)
1.27 + in (implode o dec o Symbol.explode) str: Rule.cterm' end;
1.28 +
1.29 +fun dop_leading _ [] = []
1.30 + | dop_leading c (c' :: cs) =
1.31 + if c = c' then dop_leading c cs else (c' :: cs)
1.32 +fun rm_doublets _ singled [] = singled
1.33 + | rm_doublets c singled (c' :: cs) =
1.34 + if c = c'
1.35 + then
1.36 + let val cs' = dop_leading "^" cs
1.37 + in rm_doublets c (singled @ [c']) cs' end
1.38 + else rm_doublets c (singled @ [c']) cs
1.39 +fun encode (str : Rule.cterm') =
1.40 + let fun enc [] = []
1.41 + | enc ("^" :: cs) = "^" :: "^" :: "^" :: (enc cs)
1.42 + | enc (c :: cs) = c :: (enc cs)
1.43 + in str |> Symbol.explode |> rm_doublets "^" [] |> enc |> implode end;
1.44 +
1.45 +val indentation = 2;
1.46 +
1.47 +local
1.48 +fun indent i = fold (curry op ^) (replicate i ". ") ""
1.49 +in
1.50 +(* proper <> is translated to html; however, () creates readable output.. *)
1.51 +fun xmlstr i (XML.Text str) = indent i ^ str ^ "\n"
1.52 + | xmlstr i (XML.Elem (("TERM", []), [xt])) =
1.53 + indent i ^ "(" ^ "TERM" ^ ")" ^ "\n" ^
1.54 + indent (i + 1) ^ (xt |> Codec.decode Codec.term |> Codec.the_success |> Rule.term2str) ^ "\n" ^
1.55 + indent i ^ "(/" ^ "TERM" ^ ")" ^ "\n"
1.56 + | xmlstr i (XML.Elem ((str, []), trees)) =
1.57 + indent i ^ "(" ^ str ^ ")" ^ "\n" ^
1.58 + List.foldr op ^ "" (map (xmlstr (i + 1)) trees) ^
1.59 + indent i ^ "(/" ^ str ^ ")" ^ "\n"
1.60 + | xmlstr i (XML.Elem ((str, [(flag, value)]), trees)) =
1.61 + indent i ^ "(" ^ str ^ " " ^ flag ^ "=" ^ value ^ ")" ^ "\n" ^
1.62 + List.foldr op ^ "" (map (xmlstr (i + 1)) trees) ^
1.63 + indent i ^ "(/" ^ str ^ ")" ^ "\n"
1.64 + | xmlstr _ (XML.Elem ((_, (_ :: _)), _)) =
1.65 + error "xmlstr: TODO review attribute \"status\" etc";
1.66 +end
1.67 +
1.68 +fun strs2xml strs = foldl (op ^) ("", strs);
1.69 +(* writeln (strs2xml ["<XXX> xxx </XXX>\n","<YYY> yyy </YYY>\n"]);
1.70 +<XXX> xxx </XXX>
1.71 +<YYY> yyy </YYY>*)
1.72 +
1.73 +val indentation = 2;
1.74 +val i = indentation;
1.75 +
1.76 +(*WN071016 checked that _all_ Frontend/interface.sml uses this*)
1.77 +fun term2xml j t =
1.78 + indt (j+i) ^ "<MATHML>\n" ^
1.79 + indt (j+2*i) ^ "<ISA> " ^ (decode o Rule.term2str) t ^ " </ISA>\n" ^
1.80 + indt (j+i) ^ "</MATHML>";
1.81 +(*val t = str2term "equality e_";
1.82 + writeln (term2xml 8 t);
1.83 + <MATHML>
1.84 + <ISA> equality e_ </ISA>
1.85 + <MATHML> *)
1.86 +fun xml_of_term t =
1.87 + XML.Elem (("MATHML", []),
1.88 + [XML.Elem (("ISA", []), [XML.Text ((decode o Rule.term2str) t)])])
1.89 +fun xml_of_terms ts = map xml_of_term ts
1.90 +fun xml_to_term
1.91 + ((XML.Elem (("MATHML", []), [
1.92 + XML.Elem (("ISA", []), [XML.Text str])]))) = str |> encode |> TermC.str2term
1.93 + | xml_to_term xx = raise ERROR ("xml_to_term wrong arg: " ^ xmlstr 0 xx)
1.94 +fun xml_to_term_NEW
1.95 + ((XML.Elem (("FORMULA", []), [
1.96 + XML.Elem (("ISA", []), [XML.Text str])]))) = str |> encode |> TermC.str2term
1.97 + | xml_to_term_NEW xx = raise ERROR ("xml_to_term_NEW wrong arg: " ^ xmlstr 0 xx)
1.98 +fun xml_to_terms ts = map xml_to_term ts
1.99 +fun xml_to_terms_NEW ts = map xml_to_term_NEW ts
1.100 +
1.101 +(* intermediate replacements while introducing transfer of terms by libisabelle *)
1.102 +fun xml_of_term_NEW (t : term) =
1.103 + XML.Elem (("FORMULA", []), [
1.104 + XML.Elem (("ISA", []), [XML.Text ((decode o Rule.term2str) t)]),
1.105 + XML.Elem (("TERM", []), [Codec.encode Codec.term t])])
1.106 +(* unused: formulas come as strings from frontend and are parsed by Isabelle *)
1.107 +fun xml_to_term_UNUSED
1.108 + ((XML.Elem (("FORMULA", []), [
1.109 + XML.Elem (("ISA", []), [XML.Text _]),
1.110 + XML.Elem (("TERM", []), [xt])]))) = xt |> Codec.decode Codec.term |> Codec.the_success
1.111 + | xml_to_term_UNUSED xx = raise ERROR ("xml_to_term_NEW wrong arg: " ^ xmlstr 0 xx)
1.112 +
1.113 +(*version for TextIO*)
1.114 +fun terms2xml j [] = ""
1.115 + | terms2xml j (t::ts) = term2xml j t ^ terms2xml j ts;
1.116 +(*version for writeln: extra \n*)
1.117 +fun terms2xml' j [] = ""
1.118 + | terms2xml' j [t] = term2xml j t
1.119 + | terms2xml' j (t::ts) = term2xml j t ^"\n"^ terms2xml' j ts;
1.120 +
1.121 +(*WN060513 'cterm' means the Isabelle-type*)
1.122 +fun cterm2xml j ct =
1.123 + indt (j+i) ^ "<MATHML>\n" ^
1.124 + indt (j+2*i) ^ "<ISA> " ^ ct ^ " </ISA>\n" ^
1.125 + indt (j+i) ^ "</MATHML>\n";
1.126 +fun xml_of_cterm ct =
1.127 + XML.Elem (("MATHML", []),
1.128 + [XML.Elem (("ISA", []), [XML.Text ct])])
1.129 +fun xml_to_cterm
1.130 + (XML.Elem (("MATHML", []),
1.131 + [XML.Elem (("ISA", []), [XML.Text ct])])) = ct
1.132 + | xml_to_cterm x = raise ERROR ("xml_to_cterm wrong arg: " ^ xmlstr 0 x)
1.133 +
1.134 +(*version for TextIO*)
1.135 +fun cterms2xml j [] = ""
1.136 + | cterms2xml j (t::ts) = cterm2xml j t ^ cterms2xml j ts;
1.137 +(*version for writeln: extra \n*)
1.138 +fun cterms2xml' j [] = ""
1.139 + | cterms2xml' j (t::ts) = cterm2xml j t ^"\n"^ cterms2xml j ts;
1.140 +
1.141 +(* writeln(cterms2xml 5 ["cterm1", "cterm2"]);
1.142 + <MATHML>
1.143 + <ISA> cterm1 </ISA>
1.144 + </MATHML>
1.145 + <MATHML>
1.146 + <ISA> cterm2 </ISA>
1.147 + </MATHML>
1.148 +*)
1.149 \ No newline at end of file