(* translate formulae from Isabelle-string format to xml-format.

   TODO implement MathML

   author: Walther Neuper 030701

   (c) isac-team 2003

*)

(*.decode Isabelle-strings to the format as seen by the user (1)

   EXCEPT xml-coding issues (2).

   (2) have a _reverse_ method 

   'isac.util.parser.FormalizationDigest.decodeEntities' 

   called within Formula#toSMLString in java

   ad(1) decode "^^^" ---> "^"; see Knowledge/Atools.thy;

   ad(2) decode "<" ---> "&lt;", decode ">" ---> "&gt;"

         decode "&" ---> "&"

   called for term2xml; + see "fun encode" below*)

fun decode (str: TermC.as_string) = 

    let fun dec [] = []

	  | dec ("^"::"^"::"^"::cs) = "^"::(dec cs)

	  | dec ("&"::cs) = "&"::"a"::"m"::"p"::";"::(dec cs)

	  | dec ("<"::cs) = "&"::"l"::"t"::";"::(dec cs)

	  | dec (">"::cs) = "&"::"g"::"t"::";"::(dec cs)

	  | dec (c::cs) = c::(dec cs)

    in (implode o dec o Symbol.explode) str: TermC.as_string end;

fun dop_leading _ [] = []

  | dop_leading c (c' :: cs) =

    if c = c' then dop_leading c cs else (c' :: cs)

fun rm_doublets _ singled [] = singled

  | rm_doublets c singled (c' :: cs) =

    if c = c'

    then 

      let val cs' = dop_leading "^" cs

      in rm_doublets c (singled @ [c']) cs' end

    else rm_doublets c (singled @ [c']) cs

fun encode (str : TermC.as_string) =

    let fun enc [] = []

	  | enc ("^" :: cs) = "^" :: "^" :: "^" :: (enc cs)

	  | enc (c :: cs) = c :: (enc cs)

    in str |> Symbol.explode |> rm_doublets "^" [] |>  enc |>  implode end;

val indentation = 2;

(* proper <> is translated to html; however, () creates readable output.. *)

fun xmlstr i (XML.Text str) = indent i ^ str ^ "\n"

  | xmlstr i (XML.Elem (("TERM", []), [xt])) = 

    indent i ^ "(" ^ "TERM" ^ ")" ^ "\n" ^

    indent (i + 1) ^

(*//---------------------------------- rm libisabelle ---------------------------------------\\* )

      (xt |> Codec.decode Codec.term |> Codec.the_success |> UnparseC.term)

( *------------------------------------ rm libisabelle -----------------------------------------*)

      "rm libisabelle: xt NOT DECODED"

(*\\---------------------------------- rm libisabelle ---------------------------------------//*)

      ^ "\n" ^

    indent i ^ "(/" ^ "TERM" ^ ")" ^ "\n"

  | xmlstr i (XML.Elem ((str, []), trees)) = 

    indent i ^ "(" ^ str ^ ")" ^ "\n" ^

      List.foldr op ^ "" (map (xmlstr (i + 1)) trees) ^

    indent i ^ "(/" ^ str ^ ")" ^ "\n"

  | xmlstr i (XML.Elem ((str, [(flag, value)]), trees)) = 

    indent i ^ "(" ^ str ^ " " ^ flag ^ "=" ^ value  ^ ")" ^ "\n" ^

      List.foldr op ^ "" (map (xmlstr (i + 1)) trees) ^

    indent i ^ "(/" ^ str ^ ")" ^ "\n"

  | xmlstr _ (XML.Elem ((_, (_ :: _)), _)) = 

    error "xmlstr: TODO review attribute \"status\" etc";

fun strs2xml strs = foldl (op ^) ("", strs); 

(* writeln (strs2xml ["<XXX> xxx </XXX>\n","<YYY> yyy </YYY>\n"]);

<XXX> xxx </XXX>

<YYY> yyy </YYY>*)

val indentation = 2;

val i = indentation;

(*WN071016 checked that _all_ Frontend/interface.sml uses this*)

fun term2xml j t = 

    indt (j+i) ^ "<MATHML>\n" ^ 

    indt (j+2*i) ^ "<ISA> " ^ (decode o UnparseC.term) t ^ " </ISA>\n" ^

    indt (j+i) ^ "</MATHML>";

(*val t = str2term "equality e_";

  writeln (term2xml 8 t);

          <MATHML>

            <ISA> equality e_ </ISA>

          <MATHML> *)

fun xml_of_term t =

  XML.Elem (("MATHML", []),

    [XML.Elem (("ISA", []), [XML.Text ((decode o UnparseC.term) t)])])

fun xml_of_terms ts = map xml_of_term ts

fun xml_to_term 

    ((XML.Elem (("MATHML", []), [

        XML.Elem (("ISA", []), [XML.Text str])]))) = str |> encode |> TermC.str2term

  | xml_to_term xx = raise ERROR ("xml_to_term wrong arg: " ^ xmlstr 0 xx)

fun xml_to_term_NEW 

    ((XML.Elem (("FORMULA", []), [

        XML.Elem (("ISA", []), [XML.Text str])]))) = str |> encode |> TermC.str2term

  | xml_to_term_NEW xx = raise ERROR ("xml_to_term_NEW wrong arg: " ^ xmlstr 0 xx)

fun xml_to_terms ts = map xml_to_term ts

fun xml_to_terms_NEW ts = map xml_to_term_NEW ts

(* intermediate replacements while introducing transfer of terms by libisabelle *)

fun xml_of_term_NEW (t : term) =

  XML.Elem (("FORMULA", []), [

    XML.Elem (("ISA", []), [XML.Text ((decode o UnparseC.term) t)]),

(*//---------------------------------- rm libisabelle ---------------------------------------\\* )

    XML.Elem (("TERM", []), [Codec.encode Codec.term t])

( *------------------------------------ rm libisabelle -----------------------------------------*)

    XML.Text ("(TERM)\n " ^ UnparseC.term t  ^ "\n(/TERM)")

(*\\---------------------------------- rm libisabelle ---------------------------------------//*)

    ])

(* unused: formulas come as strings from frontend and are parsed by Isabelle *)

fun xml_to_term_UNUSED

  ((XML.Elem (("FORMULA", []), [

      XML.Elem (("ISA", []), [XML.Text _]),

    XML.Elem (("TERM", []), [xt])]))) =

(*//---------------------------------- rm libisabelle ---------------------------------------\\* )

      xt |> Codec.decode Codec.term |> Codec.the_success

( *------------------------------------ rm libisabelle -----------------------------------------*)

      Const ("rm libisabelle: xt NOT DECODED", HOLogic.realT)

(*\\---------------------------------- rm libisabelle ---------------------------------------//*)

  | xml_to_term_UNUSED xx = raise ERROR ("xml_to_term_NEW wrong arg: " ^ xmlstr 0 xx)

(*version for TextIO*)                                                         

fun terms2xml j [] = ""

  | terms2xml j (t::ts) = term2xml j t ^ terms2xml j ts;

(*version for writeln: extra \n*)

fun terms2xml' j [] = ""

  | terms2xml' j [t] = term2xml j t

  | terms2xml' j (t::ts) = term2xml j t ^"\n"^ terms2xml' j ts;

(*WN060513 'cterm' means the Isabelle-type*)

fun cterm2xml j ct = 

    indt (j+i) ^ "<MATHML>\n" ^ 

    indt (j+2*i) ^ "<ISA> " ^ ct ^ " </ISA>\n" ^

    indt (j+i) ^ "</MATHML>\n";

fun xml_of_cterm ct = 

  XML.Elem (("MATHML", []),

    [XML.Elem (("ISA", []), [XML.Text ct])])

fun xml_to_cterm

    (XML.Elem (("MATHML", []),

      [XML.Elem (("ISA", []), [XML.Text ct])])) = ct

  | xml_to_cterm x = raise ERROR ("xml_to_cterm wrong arg: " ^ xmlstr 0 x)

(*version for TextIO*)                                                         

fun cterms2xml j [] = ""

  | cterms2xml j (t::ts) = cterm2xml j t ^ cterms2xml j ts;

(*version for writeln: extra \n*)

fun cterms2xml' j [] = ""

  | cterms2xml' j (t::ts) = cterm2xml j t ^"\n"^ cterms2xml j ts;

(* writeln(cterms2xml 5 ["cterm1", "cterm2"]);

       <MATHML>

         <ISA> cterm1 </ISA>

       </MATHML>

       <MATHML>

         <ISA> cterm2 </ISA>

       </MATHML>

*)