(* convert sml-datatypes to xml

   authors: Walther Neuper 2003

   (c) due to copyright terms

use"xmlsrc/datatypes.sml";

use"datatypes.sml";

*)

signature DATATYPES =

  sig

    val authors2xml : int -> string -> string list -> xml

    val calc2xml : int -> thyID * calc -> xml

    val calcrefs2xml : int -> thyID * calc list -> xml

    val contthy2xml : int -> contthy -> xml

    val extref2xml : int -> string -> string -> xml

    val filterpbl :

       ''a -> (''a * (Term.term * Term.term)) list -> Term.term list

    val formula2xml : int -> Term.term -> xml

    val formulae2xml : int -> Term.term list -> xml

    val i : int

    val id2xml : int -> string list -> string

    val ints2xml : int -> int list -> string

    val itm_2xml : int -> SpecifyTools.itm_ -> xml

    val itms2xml :

       int ->

       (int * SpecifyTools.vats * bool * string * SpecifyTools.itm_) list ->

       string

    val keref2xml : int -> ketype -> kestoreID -> xml

    val model2xml :

       int -> SpecifyTools.itm list -> (bool * Term.term) list -> xml

    val modspec2xml : int -> ocalhd -> xml

    val pattern2xml :

       int ->

       (string * (Term.term * Term.term)) list -> Term.term list -> string

    val pos'2xml : int -> string * (int list * pos_) -> string

    val pos'calchead2xml : int -> pos' * ocalhd -> xml

    val pos_2xml : int -> pos_ -> string

    val posform2xml : int -> pos' * Term.term -> xml

    val posformhead2xml : int -> pos' * ptform -> string

    val posformheads2xml : int -> (pos' * ptform) list -> xml

    val posforms2xml : int -> (pos' * Term.term) list -> xml

    val posterms2xml : int -> (pos' * term) list -> xml

    val precond2xml : int -> bool * Term.term -> xml

    val preconds2xml : int -> (bool * Term.term) list -> xml

    val rls2xml : int -> thyID * rls -> xml

    val rule2xml : int -> guh -> rule -> xml

    val rules2xml : int -> guh -> rule list -> xml

    val scr2xml : int -> scr -> xml

    val spec2xml : int -> spec -> xml

    val sub2xml : int -> Term.term * Term.term -> xml

    val subs2xml : int -> subs -> xml

    val subst2xml : int -> subst -> xml

    val tac2xml : int -> tac -> xml

    val tacs2xml : int -> tac list -> xml

    val theref2xml : int -> thyID -> string -> xstring -> string

    val thm'2xml : int -> thm' -> xml

    val thm''2xml : int -> thm -> xml

    val thmstr2xml : int -> string -> xml

  end

(*------------------------------------------------------------------*)

structure datatypes:DATATYPES =

(*structure datatypes =*)

struct

(*------------------------------------------------------------------*)

val i = indentation;

(** general types: lists,  **)

(*.handles string list like 'fun id2xml'.*)

fun authors2xml j str auts = 

    let fun autx _ [] = ""

	  | autx j (s::ss) = (indt j) ^ "<STRING> " ^ s ^ " </STRING>\n" ^ 

			     (autx j ss)

    in indt j ^ "<"^str^">\n" ^

       autx (j + i) auts ^ 

       indt j ^ "</"^str^">\n" : xml

    end;

(* writeln(authors2xml 2 "MATHAUTHORS" []);

   writeln(authors2xml 2 "MATHAUTHORS" 

		       ["isac-team 2001", "Richard Lang 2003"]);

   *)

fun id2xml j ids =

    let fun id2x _ [] = ""

	  | id2x j (s::ss) = (indt j) ^ "<STRING> " ^ s ^ " </STRING>\n" ^ 

			     (id2x j ss)

    in (indt j) ^ "<STRINGLIST>\n" ^ 

       (id2x (j + indentation) ids) ^ 

       (indt j) ^ "</STRINGLIST>\n" end;

(* writeln(id2xml 8 ["linear","univariate","equation"]);

        <STRINGLIST>

          <STRING>linear</STRING>

          <STRING>univariate</STRING>

          <STRING>equation</STRING>

        </STRINGLIST>*)

fun ints2xml j ids =

    let fun int2x _ [] = ""

	  | int2x j (s::ss) = (indt j) ^"<INT> "^ string_of_int s ^" </INT>\n"^

			     (int2x j ss)

    in (indt j) ^ "<INTLIST>\n" ^ 

       (int2x (j + i) ids) ^ 

       (indt j) ^ "</INTLIST>\n" end;

(* writeln(ints2xml 3 [1,2,3]);

   *)

(** isac datatypes **)

fun pos_2xml j pos_ =

    (indt j) ^ "<POS> " ^  pos_2str pos_ ^ " </POS>\n";

(*.due to specialties of isac/util/parser/XMLParseDigest.java

   pos' requires different tags.*)

fun pos'2xml j (tag, (pos, pos_)) =

    indt     (j) ^ "<" ^ tag ^ ">\n" ^ 

    ints2xml (j+i) pos ^ 

    pos_2xml (j+i) pos_ ^ 

    indt     (j) ^ "</" ^ tag ^ ">\n";

(* writeln(pos'2xml 3 ("POSITION", ([1,2,3], Pbl)));

   *)

fun formula2xml j term = (*TODO.WN050211: use for _all_ <FORMULA>*)

    indt j ^ "<FORMULA>\n"^

    term2xml j term ^"\n"^

    indt j ^ "</FORMULA>\n" : xml;

(* writeln(formula2xml 6 (str2term "1+1=2"));

   *)

fun formulae2xml j [] = ("":xml)

  | formulae2xml j (r::rs) = formula2xml j r ^ formulae2xml j rs;

(* writeln(formulae2xml 6 [str2term "1+1=2", str2term "1+1+1=3"]);

   *)

(*WN0502 @see ME/ctree: type asms: illdesigned, thus not used*)

fun posform2xml j (p:pos', term) =

    indt j ^     "<POSFORM>\n" ^

    pos'2xml (j+i) ("POSITION", p) ^

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

    term2xml (j+i) term ^"\n"^

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

    indt j ^     "</POSFORM>\n" : xml;

(* writeln(posform2xml 6 (([1,2],Frm), str2term "1+1=2"));

   *)

fun posforms2xml j [] = ("":xml)

  | posforms2xml j (r::rs) = posform2xml j r ^ posforms2xml j rs;

(* writeln(posforms2xml 6 [(([1],Res), str2term "1+1=2"),(([2],Res), str2term "1+1+1=3")]);

   *)

fun calcref2xml j (thyID:thyID, (scrop, (rewop, _)):calc) =

    indt j ^ "<CALCREF>\n" ^

    indt (j+i) ^ "<STRING> " ^ scrop ^ "</STRING>\n" ^

    indt (j+i) ^ "<GUH> " ^ cal2guh ("IsacKnowledge", 

				      thyID) scrop  ^ " </GUH>\n" ^

    indt j ^ "</CALCREF>\n" : xml;

fun calcrefs2xml _ (_,[]) = "":xml

  | calcrefs2xml j (thyID, cal::cs) = 

    calcref2xml j (thyID, cal) ^ calcrefs2xml j (thyID, cs);

fun calc2xml j (thyID:thyID, (scrop, (rewop, _)):calc) =

    indt j ^ "<CALC>\n" ^

    indt (j+i) ^ "<STRING>\n" ^ scrop ^ "</STRING>\n" ^

    indt (j+i) ^ "<GUH>\n" ^ cal2guh ("IsacKnowledge", 

				      thyID) scrop  ^ "</GUH>\n" ^

    indt (j+i) ^ "<TERMOP>\n" ^ rewop ^ "</TERMOP>\n" ^

    indt j ^ "</CALC>\n" : xml;

(*.for creating a href for a rule within an rls's rule list;

   the guh points to the thy of definition of the rule, NOT of use in rls.*)

fun rule2xml j (thyID:thyID) Erule =

    error "rule2xml called with 'Erule'"

(* val (j, thyID, Thm (thmID, thm)) = (j+i, thyID, nth 1 rules);

   val (j, thyID, Thm (thmID, thm)) = (j, thyID,r);

   *)

  | rule2xml j thyID (Thm (thmID, thm)) =

    indt j ^ "<RULE>\n" ^

    indt (j+i) ^ "<TAG> Theorem </TAG>\n" ^

    indt (j+i) ^ "<STRING> " ^ thmID ^ " </STRING>\n" ^

    indt (j+i) ^ "<GUH> " ^ thm2guh (thy_containing_thm thyID thmID) 

				    thmID ^ " </GUH>\n" ^

    indt j ^ "</RULE>\n" : xml

(* val (j, thyID, Calc (termop, _)) = (j+i, thyID, nth 42 rules);

   val (j, thyID, Calc (termop, _)) = (j+i, thyID, nth 43 rules);

   *)

  | rule2xml j thyID (Calc (termop, _)) = ""

(*FIXXXXXXXME.WN060714 in rls make Calc : calc -> rule [add scriptop!]

  see smltest/../datatypes.sml !

    indt j ^ "<RULE>\n" ^

    indt (j+i) ^ "<STRING> " ^ termop ^ " </STRING>\n" ^

    indt (j+i) ^ "<GUH> " ^ cal2guh (thy_containing_cal thyID termop) 

				    termop ^ " </GUH>\n" ^

    indt j ^ "</RULE>\n"

*)

  | rule2xml j thyID (Cal1 (termop, _)) = ""

  | rule2xml j thyID (Rls_ rls) =

    let val rls' = (#id o rep_rls) rls

    in indt j ^ "<RULE>\n" ^

       indt (j+i) ^ "<TAG> Ruleset </TAG>\n" ^

       indt (j+i) ^ "<STRING> " ^ rls' ^ " </STRING>\n" ^

       indt (j+i) ^ "<GUH> " ^ rls2guh (thy_containing_rls thyID rls') 

				       rls' ^ " </GUH>\n" ^

       indt j ^ "</RULE>\n"

    end;

(* val (j, thyID, r::rs) = (2, "Test", rules);

   *)

fun rules2xml j thyID [] = ("":xml)

  | rules2xml j thyID (r::rs) = rule2xml j thyID r ^ rules2xml j thyID rs;

fun filterpbl str =

  let fun filt [] = []

        | filt ((s, (t1, t2)) :: ps) = 

	  if str = s then (t1 $ t2) :: filt ps else filt ps

  in filt end;

(*FIXME.WN040831 model2xml <--?--> pattern2xml*)

(*WN.25.8.03: pattern2xml different output with TextIO | writeln !!!

  the version below is for TextIO: terms2xml makes \n !*)

(* val (j, p, where_) = (i, ppc, where_);

   *)

fun pattern2xml j p where_ =

    (case filterpbl "#Given" p of

	[] =>  (indt j) ^ "<GIVEN>  </GIVEN>\n"

(* val gis = filterpbl "#Given" p;

   *)

      | gis => (indt j) ^ "<GIVEN>\n" ^ terms2xml' j gis ^

	       (indt j) ^ "</GIVEN>\n")

    ^ 

    (case where_ of

	 [] =>  (indt j) ^ "<WHERE>  </WHERE>\n"

       | whs => (indt j) ^ "<WHERE>\n" ^ terms2xml' j whs ^

		(indt j) ^ "</WHERE>\n")

    ^ 

    (case filterpbl "#Find" p of

	 [] =>  (indt j) ^ "<FIND>  </FIND>\n"

       | fis => (indt j) ^ "<FIND>\n" ^ terms2xml' j fis ^

		(indt j) ^ "</FIND>\n")

    ^ 

    (case filterpbl "#Relate" p of

	 [] =>  (indt j) ^ "<RELATE>  </RELATE>\n"

       | res => (indt j) ^ "<RELATE>\n" ^ terms2xml' j res ^

		(indt j) ^ "</RELATE>\n");

(*

writeln(pattern2xml 3 ((#ppc o get_pbt)

			 ["squareroot","univariate","equation","test"]) []);

  *)

(*see itm_2item*)

fun itm_2xml j (Cor (dts,_))= 

    (indt j ^"<ITEM status=\"correct\">\n"^    

    term2xml (j) (comp_dts' dts)^"\n"^    

    indt j ^"</ITEM>\n"):xml

  | itm_2xml j (Syn c) =

    indt j ^"<ITEM status=\"syntaxerror\">\n"^    

    indt (j) ^c^    

    indt j ^"</ITEM>\n"

  | itm_2xml j (Typ c) =

    indt j ^"<ITEM status=\"typeerror\">\n"^    

    indt (j) ^c^    

    indt j ^"</ITEM>\n"

  (*type item also has 'False of cterm' set in preconds2xml WN 050618*)

  | itm_2xml j (Inc (dts,_)) = 

    indt j ^"<ITEM status=\"incomplete\">\n"^    

    term2xml (j) (comp_dts' dts)^"\n"^    

    indt j ^"</ITEM>\n"

  | itm_2xml j (Sup dts) = 

    indt j ^"<ITEM status=\"superfluous\">\n"^    

    term2xml (j) (comp_dts' dts)^"\n"^    

    indt j ^"</ITEM>\n"

  | itm_2xml j (Mis (d,pid)) =

    indt j ^"<ITEM status=\"missing\">\n"^    

    term2xml (j) (d $ pid)^"\n"^    

    indt j ^"</ITEM>\n";

(*see terms2xml' fpr \n*)

fun itms2xml _ [] = ""

  | itms2xml j [(_,_,_,_,itm_)] = itm_2xml j itm_

  | itms2xml j (((_,_,_,_,itm_):itm)::itms) =

    itm_2xml j itm_ ^ itms2xml j itms;

fun precond2xml j (true, term) =

    (indt j ^"<ITEM status=\"correct\">\n"^

    term2xml (j) term^"\n"^

    indt j ^"</ITEM>\n"):xml

  | precond2xml j (false, term) =

    indt j ^"<ITEM status=\"false\">\n"^

    term2xml (j+i) term^"\n"^

    indt j ^"</ITEM>\n";

fun preconds2xml _ [] = ("":xml)

  | preconds2xml j (p::ps) = precond2xml j p ^ preconds2xml j ps;

(*FIXME.WN040831 model2xml <--?--> pattern2xml*)

fun model2xml j (itms:itm list) where_ =

    let fun eq4 str (_,_,_,field,_) = str = field

    in  (indt j ^"<MODEL>\n"^

	(case filter (eq4 "#Given") itms of

	     [] =>  (indt (j+i)) ^ "<GIVEN>  </GIVEN>\n"

	   | gis => (indt (j+i)) ^ "<GIVEN>\n" ^ itms2xml (j+2*i) gis ^

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

	^

	(case where_ of

	     [] =>  (indt (j+i)) ^ "<WHERE>  </WHERE>\n"

	   | whs => (indt (j+i)) ^ "<WHERE>\n" ^ preconds2xml (j+2*i) whs ^

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

	^

	(case filter (eq4 "#Find") itms of

	     [] =>  (indt (j+i)) ^ "<FIND>  </FIND>\n"

	   | fis => (indt (j+i)) ^ "<FIND>\n" ^ itms2xml (j+2*i) fis ^

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

	^

	(case filter (eq4 "#Relate") itms of

	     [] =>  (indt (j+i)) ^ "<RELATE>  </RELATE>\n"

	   | res => (indt (j+i)) ^ "<RELATE>\n" ^ itms2xml (j+2*i) res ^

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

	    indt j ^"</MODEL>\n"):xml

    end;

(* writeln(model2xml 3 itms []);

   *)

fun spec2xml j ((dI,pI,mI):spec) =

    (indt j ^"<SPECIFICATION>\n"^

    indt (j+i) ^"<THEORYID> "^ dI ^" </THEORYID>\n"^

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

    id2xml (j+2*i) pI ^

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

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

    id2xml (j+2*i) mI ^

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

    indt j ^"</SPECIFICATION>\n"):xml;

fun modspec2xml j ((b, p_, head, gfr, pre, spec): ocalhd) =

    (indt j ^"<CALCHEAD status = "^

     quote (if b then "correct" else "incorrect")^">\n"^

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

     term2xml (j+i) head^"\n"^

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

     model2xml (j+i) gfr pre ^

     indt (j+i) ^"<BELONGSTO> "^(case p_ of Pbl => "Pbl"

					  | Met => "Met"

					  | _ => "Und")^" </BELONGSTO>\n"^

     spec2xml (j+i) spec ^

     indt j ^"</CALCHEAD>\n"):xml;

(* writeln (modspec2xml 2 e_ocalhd);

   *)

fun pos'calchead2xml j (p:pos', (b, p_, head, gfr, pre, spec): ocalhd) =

    (indt j ^"<CALCHEAD status = "^

     quote (if b then "correct" else "incorrect")^">\n"^

     pos'2xml (j+i) ("POSITION", p) ^

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

     term2xml (j+i) head^"\n"^

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

     model2xml (j+i) gfr pre ^

     indt (j+i) ^"<BELONGSTO> "^(case p_ of Pbl => "Pbl"

					  | Met => "Met"

					  | _ => "Und")^" </BELONGSTO>\n"^

     spec2xml (j+i) spec ^

     indt j ^"</CALCHEAD>\n"):xml;

fun sub2xml j (id, value) =

    (indt j ^"<PAIR>\n"^

     indt j ^"  <VARIABLE>\n"^

     term2xml (j+i) id ^ "\n" ^

     indt j ^"  </VARIABLE>\n" ^

     indt j ^"  <VALUE>\n"^

     term2xml (j+i) value ^ "\n" ^

     indt j ^"  </VALUE>\n" ^

     indt j ^"</PAIR>\n"):xml;

fun subs2xml j (subs:subs) =

    (indt j ^"<SUBSTITUTION>\n"^

     foldl op^ ("", map (sub2xml (j+i))

			(subs2subst (assoc_thy "Isac.thy") subs)) ^

     indt j ^"</SUBSTITUTION>\n"):xml;

(* val subs = [(str2term "bdv", str2term "x")];

   val subs = ["(bdv, x)"];

   writeln(subs2xml 0 subs);

   *)

fun subst2xml j (subst:subst) =

    (indt j ^"<SUBSTITUTION>\n"^

     foldl op^ ("", map (sub2xml (j+i)) subst) ^

     indt j ^"</SUBSTITUTION>\n"):xml;

(* val subst = [(str2term "bdv", str2term "x")];

   writeln(subst2xml 0 subst);

   *)

(* val (j, str) = ((j+i), form);

   *)

fun thmstr2xml j str = ((((term2xml j) o str2term) str)^"\n"):xml;

(* val (j, ((ID, form):thm')) = ((j+i), thm');

   *)

fun thm'2xml j ((ID, form):thm') =

    (indt j ^"<THEOREM>\n"^

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

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

    thmstr2xml (j+i) form^

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

    indt j ^"</THEOREM>\n"):xml;

(*WN060627 scope of thy's not considered ?!?*)

fun thm''2xml j (thm:thm) =

    indt j ^"<THEOREM>\n"^

    indt (j+i) ^"<ID> "^ (strip_thy o Thm.get_name_hint) thm ^" </ID>\n"^

    term2xml j ((#prop o rep_thm) thm) ^ "\n" ^

    indt j ^"</THEOREM>\n":xml;

fun scr2xml j EmptyScr =

    indt j ^"<SCRIPT>  </SCRIPT>\n" : xml

  | scr2xml j (Script term) =

    if term = e_term 

    then indt j ^"<SCRIPT>  </SCRIPT>\n"

    else indt j ^"<SCRIPT>\n"^ 

	 term2xml j (inst_abs (assoc_thy "Isac.thy") term) ^ "\n" ^

	 indt j ^"</SCRIPT>\n"

  | scr2xml j (Rfuns _) =

    indt j ^"<REVERSREWRITE> reverse rewrite functions </REVERSREWRITE>\n";

fun prepa12xml j (terms, term) =

    indt j ^"<PREPAT>\n"^

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

    terms2xml (j+2*i) terms ^

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

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

    term2xml (j+2*i) term ^

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

    indt j ^"</PREPAT>\n" : xml;

fun prepat2xml j [] = ""

  | prepat2xml j (p::ps) = prepa12xml j p ^ prepat2xml j ps : xml;

(* val (j, (thyID, seqrls, {id, preconds, rew_ord=(ord,_), erls,

			    srls, calc, rules, scr})) = 

	   (j, (thyID, "Seq", data));

   *)

fun rls2xm j (thyID, seqrls, {id, preconds, rew_ord=(ord,_), erls,

		      srls, calc, rules, scr}) =

    indt j ^"<RULESET>\n"^

    indt (j+i) ^"<ID> "^ id ^" </ID>\n"^

    indt (j+i) ^"<TYPE> "^ seqrls ^" </TYPE>\n"^

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

    rules2xml (j+2*i) thyID rules ^

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

    indt (j+i) ^"<PRECONDS> " ^

    terms2xml' (j+2*i) preconds ^

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

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

    indt (j+2*i) ^ "<STRING> " ^ ord ^ " </STRING>\n" ^

(*WN060714 thy_isac_*-ord-*.xml not yet generated ................

    indt (j+2*i) ^ "<GUH> " ^ ord2guh ("IsacKnowledge", 

				      thyID) ord ^ " </GUH>\n" ^

..................................................................*)

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

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

    indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^

    indt (j+2*i) ^ "<STRING> " ^ id_rls erls ^ " </STRING>\n" ^

    indt (j+2*i) ^ "<GUH> " ^ rls2guh ("IsacKnowledge", thyID) 

				     (id_rls erls) ^ " </GUH>\n" ^

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

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

    indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^

    indt (j+2*i) ^ "<STRING> " ^ id_rls erls ^ " </STRING>\n" ^

    indt (j+2*i) ^ "<GUH> " ^ rls2guh ("IsacKnowledge", thyID) 

				     (id_rls srls) ^ " </GUH>\n" ^

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

    calcrefs2xml (j+i) (thyID, calc) ^

    scr2xml (j+i) scr ^

    indt j ^"</RULESET>\n" : xml;

fun rls2xml j (thyID, Erls) = rls2xml j (thyID, e_rls)

(* rls2xml j (thyID, Rls {id=id, preconds=preconds, rew_ord=(ord,e_rew_ord), 

			  erls=erls,srls=srls,calc=calc,rules=rules,scr=scr});

   val (j, (thyID, Rls {id, preconds, rew_ord=(ord,_), erls,

			srls, calc, rules, scr})) = (i, thy_rls);

   val (j, (thyID, Seq data)) = (i, thy_rls);

   *)

  | rls2xml j (thyID, Rls data) = rls2xm j (thyID, "Rls", data)

(* val (j, (thyID, Seq data)) = (i, thy_rls);

   *)

  | rls2xml j (thyID, Seq data) = rls2xm j (thyID, "Seq", data)

  | rls2xml j (thyID, Rrls {id, prepat, rew_ord=(ord,_), erls, calc, scr}) = 

    indt j ^"<RULESET>\n"^

    indt (j+i) ^"<ID> "^ id ^" </ID>\n"^

    indt (j+i) ^"<TYPE> Rrls </TYPE>\n"^

    prepat2xml (j+i) prepat ^

    indt (j+i) ^"<ORDER> " ^

    indt (j+2*i) ^ "<TAG> Rewrite order </TAG>\n" ^

    indt (j+2*i) ^ "<STRING> " ^ ord ^ " </STRING>\n" ^

(*WN060714 thy_isac_*-ord-*.xml not yet generated ................

    indt (j+2*i) ^ "<GUH> " ^ ord2guh ("IsacKnowledge", 

				      thyID) ord ^ " </GUH>\n" ^

.................................................................*)

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

    indt (j+i) ^"<ERLS> " ^

    indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^

    indt (j+2*i) ^ "<STRING> " ^ id_rls erls ^ " </STRING>\n" ^

    indt (j+2*i) ^ "<GUH> " ^ rls2guh ("IsacKnowledge", thyID) 

				     (id_rls erls) ^ " </GUH>\n" ^

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

    calcrefs2xml (j+i) (thyID, calc) ^

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

    scr2xml (j+2*i) scr ^

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

    indt j ^"</RULESET>\n" : xml;

(*.convert a tactic into xml-format

   ATTENTION: WN060513 detected faulty 'cterm2xml's with 'string's as args.*)

fun tac2xml j (Subproblem (dI, pI)) =

    (indt j ^"<SUBPROBLEMTACTIC name=\"Subproblem\">\n"^

    indt (j+i) ^"<THEORY> "^ dI ^" </THEORY>\n"^

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

    id2xml (j+2*i) pI^

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

    indt j ^"</SUBPROBLEMTACTIC>\n"):xml

  | tac2xml j Model_Problem =

    (indt j ^"<STRINGLISTTACTIC name=\"Model_Problem\">"^

    indt j ^"</STRINGLISTTACTIC>\n"):xml

  | tac2xml j (Refine_Tacitly pI) =

    (indt j ^"<STRINGLISTTACTIC name=\"Refine_Tacitly\">\n"^

    id2xml (j+i) pI^

    indt j ^"</STRINGLISTTACTIC>\n"):xml

  | tac2xml j (Add_Given ct) =

    (indt j ^"<SIMPLETACTIC name=\"Add_Given\">\n"^

    cterm2xml (j+i) ct^

    indt j ^"</SIMPLETACTIC>\n"):xml

  | tac2xml j (Add_Find ct) =

    (indt j ^"<SIMPLETACTIC name=\"Add_Find\">\n"^

    cterm2xml (j+i) ct^

    indt j ^"</SIMPLETACTIC>\n"):xml

  | tac2xml j (Add_Relation ct) =

    (indt j ^"<SIMPLETACTIC name=\"Add_Relation\">\n"^

    cterm2xml (j+i) ct^

    indt j ^"</SIMPLETACTIC>\n"):xml

  | tac2xml j (Specify_Theory ct) =

    (indt j ^"<SIMPLETACTIC name=\"Specify_Theory\">\n"^

    cterm2xml (j+i) ct^(*WN060513 Specify_Theory = fn : domID -> tac

and domID is a string, not a cterm *)

    indt j ^"</SIMPLETACTIC>\n"):xml

  | tac2xml j (Specify_Problem ct) =

    (indt j ^"<STRINGLISTTACTIC name=\"Specify_Problem\">\n"^

    id2xml (j+i) ct^

    indt j ^"</STRINGLISTTACTIC>\n"):xml

  | tac2xml j (Specify_Method ct) =

    (indt j ^"<STRINGLISTTACTIC name=\"Specify_Method\">\n"^

    id2xml (j+i) ct^

    indt j ^"</STRINGLISTTACTIC>\n"):xml

  | tac2xml j (Apply_Method mI) =

    (indt j ^"<STRINGLISTTACTIC name=\"Apply_Method\">\n"^

    id2xml (j+i) mI^

    indt j ^"</STRINGLISTTACTIC>\n"):xml

  | tac2xml j (Take ct) =

    (indt j ^"<SIMPLETACTIC name=\"Take\">\n"^

    cterm2xml (j+i) ct^

    indt j ^"</SIMPLETACTIC>\n"):xml

  | tac2xml j (Calculate opstr) =

    (indt j ^"<SIMPLETACTIC name=\"Calculate\">\n"^

    cterm2xml (j+i) opstr^(*WN060513 Calculate = fn : string -> tac

			'string', _NOT_ 'cterm' ..flaw from RG*)

    indt j ^"</SIMPLETACTIC>\n"):xml

(* val (j, Rewrite thm') = (i, tac);

   *)

  | tac2xml j (Rewrite thm') =

    (indt j ^"<REWRITETACTIC name=\"Rewrite\">\n"^

    thm'2xml (j+i) thm'^

    indt j ^"</REWRITETACTIC>\n"):xml

(* writeln (tac2xml 2 (Rewrite ("all_left",

				"~ ?b =!= 0 ==> (?a = ?b) = (?a - ?b = 0)")));

   val (j, (Rewrite_Inst (subs, thm'))) = (i, tac);

   *)

  | tac2xml j (Rewrite_Inst (subs, thm')) =

    (indt j ^"<REWRITEINSTTACTIC name=\"Rewrite_Inst\">\n"^

    subs2xml (j+i) subs^

    thm'2xml (j+i) thm'^

    indt j ^"</REWRITEINSTTACTIC>\n"):xml

(* writeln (tac2xml 2 (Rewrite_Inst

			   (["(bdv,x)"],

			    ("all_left",

			     "~ ?b =!= 0 ==> (?a = ?b) = (?a - ?b = 0)"))));

   *)

  | tac2xml j (Rewrite_Set rls') =

    (indt j ^"<REWRITESETTACTIC name=\"Rewrite_Set\">\n"^

    indt (j+i) ^"<RULESET> "^ rls' ^" </RULESET>\n"^

    indt j ^"</REWRITESETTACTIC>\n"):xml

  | tac2xml j (Rewrite_Set_Inst (subs, rls')) =

    (indt j ^"<REWRITESETINSTTACTIC name=\"Rewrite_Set_Inst\">\n"^

    indt (j+i) ^"<RULESET> "^ rls' ^" </RULESET>\n"^

    subs2xml (j+i) subs^

    indt j ^"</REWRITESETINSTTACTIC>\n"):xml

  | tac2xml j (Or_to_List) =

    (indt j ^"<STRINGLISTTACTIC name=\"Or_to_List\"> </STRINGLISTTACTIC>\n"):xml

  | tac2xml j (Check_elementwise ct) =

    (indt j ^"<SIMPLETACTIC name=\"Check_elementwise\">\n"^

    cterm2xml (j+i) ct ^ "\n"^

    indt j ^"</SIMPLETACTIC>\n"):xml

  (*WN0605 quick and dirty: cterms is _NOT_ a stringlist like pblID...*)

  | tac2xml j (Substitute cterms) =

    (indt j ^"<STRINGLISTTACTIC name=\"Substitute\">\n"^

    (*cterms2xml (j+i) cterms^  ....should be WN060514: TODO TERMLISTTACTIC?*)

    id2xml (j+i) cterms^

    indt j ^"</STRINGLISTTACTIC>\n"):xml

  | tac2xml j (Check_Postcond pI) =

    (indt j ^"<STRINGLISTTACTIC name=\"Check_Postcond\">\n"^

    id2xml (j+i) pI^

    indt j ^"</STRINGLISTTACTIC>\n"):xml

  | tac2xml j tac = error ("tac2xml: not impl. for "^tac2str tac);

fun tacs2xml j [] = "":xml

  | tacs2xml j (t::ts) = tac2xml j t ^ tacs2xml j ts;

fun posformhead2xml j (p:pos', Form f) =

    indt j ^"<CALCFORMULA>\n"^

    pos'2xml (j+i) ("POSITION", p) ^

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

    term2xml (j+i) f^"\n"^

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

    indt j ^"</CALCFORMULA>\n"

  | posformhead2xml j (p, ModSpec c) =

    pos'calchead2xml (j) (p, c);

fun posformheads2xml j [] = ("":xml)

  | posformheads2xml j (r::rs) = posformhead2xml j r ^ posformheads2xml j rs;

val e_pblterm = (term_of o the o (parse (theory "Script"))) 

		    ("Problem (" ^ e_domID ^ "," ^ strs2str' e_pblID ^ ")");

(*WN051224 minimal adaption to exporting Formulae _only_ by getFormulaeFromTo*)

fun posterm2xml j (p:pos', t) =

    indt j ^"<CALCFORMULA>\n"^

    pos'2xml (j+i) ("POSITION", p) ^

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

    (if t = e_pblterm (*headline in pbl is e_ <- _root_pbl for CAS-command*)

     then cterm2xml (j+i) "________________________________________________" 

     else term2xml (j+i) t)^"\n" ^

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

    indt j ^"</CALCFORMULA>\n";

fun posterms2xml j [] = ("":xml)

  | posterms2xml j (r::rs) = posterm2xml j r ^ posterms2xml j rs;

fun  asm_val2xml j (asm, vl) = 

    indt j ^ "<ASMEVALUATED>\n" ^

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

    term2xml (j+i) asm ^ "\n" ^

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

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

    term2xml (j+i) vl ^ "\n" ^

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

    indt j ^ "</ASMEVALUATED>\n" : xml;

fun asm_vals2xml j [] = ("":xml)

  | asm_vals2xml j (asm_val::avs) = asm_val2xml j asm_val ^

				    asm_vals2xml j avs;

(*.a reference to an element in the theory hierarchy; 

   compare 'fun keref2xml'.*)

(* val (j, thyID, typ, xstring) = 

       (i+i, snd (thy_containing_rls thy' prls'), "Rulesets", prls');

   *)

fun theref2xml j (thyID:thyID) typ (xstring:xstring) =

    let val guh = theID2guh ["IsacKnowledge", thyID, typ, xstring]

	val typ' = (implode o (drop_last_n 1) o explode) typ

    in indt j ^ "<KESTOREREF>\n" ^

       indt (j+i) ^ "<TAG> " ^ typ' ^ " </TAG>\n" ^

       indt (j+i) ^ "<ID> " ^ xstring ^ " </ID>\n" ^

       indt (j+i) ^ "<GUH> " ^ guh ^ " </GUH>\n" ^

       indt j ^ "</KESTOREREF>\n" : xml

    end;

(*.a reference to an element in the kestore EXCEPT theory hierarchy; 

   compare 'fun theref2xml'.*)

(* val (j, typ, kestoreID) = (i+i, Met_, hd met);

   *)

fun keref2xml j typ (kestoreID:kestoreID) =

    let val id = strs2str' kestoreID

	val guh = kestoreID2guh typ kestoreID

    in indt j ^ "<KESTOREREF>\n" ^

       indt (j+i) ^ "<TAG> " ^ ketype2str' typ ^ "</TAG>\n" ^

       indt (j+i) ^ "<ID> " ^ id ^ " </ID>\n" ^

       indt (j+i) ^ "<GUH> " ^ guh ^ " </GUH>\n" ^

       indt j ^ "</KESTOREREF>\n" : xml

    end;

(*url to a source external to isac*)

fun extref2xml j linktext url =

    indt j ^ "<EXTREF>\n" ^

    indt (j+i) ^ "<TEXT> " ^ linktext ^ " </TEXT>\n" ^

    indt (j+i) ^ "<URL> " ^ url ^ " </URL>\n" ^

    indt j ^ "</EXTREF>\n" : xml;

(* val (ContThmInst{thyID, thm, bdvs, thminst, applto, applat, reword,

		    asms, lhs, rhs, result, resasms, asmrls}) =

       (context_thy (pt,pos) tac);

writeln (contthy2xml 2 (context_thy (pt,pos) tac));

   *)

fun contthy2xml j EContThy =

    error "contthy2xml called with EContThy"

  | contthy2xml j (ContThm {thyID, thm, applto, applat, reword, 

				 asms,lhs, rhs, result, resasms, asmrls}) =

    indt j ^ "<GUH> " ^ thm ^ " </GUH>\n" ^

    indt j ^ "<APPLTO>\n" ^

    term2xml j applto ^ "\n" ^

    indt j ^ "</APPLTO>\n" ^

    indt j ^ "<APPLAT>\n" ^

    term2xml j applat ^ "\n" ^

    indt j ^ "</APPLAT>\n" ^

    indt j ^ "<ORDER>\n" ^ (*should be a theref2xml*)

    indt (j+i) ^"<ID> " ^ reword ^ " </ID>\n" ^

    indt j ^ "</ORDER>\n" ^

    indt j ^ "<ASMSEVAL>\n" ^

    asm_vals2xml (j+i) asms ^

    indt j ^ "</ASMSEVAL>\n" ^

    indt j ^ "<LHS>\n" ^

    term2xml j (fst lhs) ^ "\n" ^

    indt j ^ "</LHS>\n" ^

    indt j ^ "<LHSINST>\n" ^

    term2xml j (snd lhs) ^ "\n" ^

    indt j ^ "</LHSINST>\n" ^

    indt j ^ "<RHS>\n" ^

    term2xml j (fst rhs) ^ "\n" ^

    indt j ^ "</RHS>\n" ^

    indt j ^ "<RHSINST>\n" ^

    term2xml j (snd rhs) ^ "\n" ^

    indt j ^ "</RHSINST>\n" ^

    indt j ^ "<RESULT>\n" ^

    term2xml j result ^ "\n" ^

    indt j ^ "</RESULT>\n" ^

    indt j ^ "<ASSUMPTIONS>\n" ^

    terms2xml' j resasms ^

    indt j ^ "</ASSUMPTIONS>\n" ^

    indt j ^ "<EVALRLS>\n" ^

    theref2xml j thyID "Rulesets" asmrls ^

    indt j ^ "</EVALRLS>\n"

  | contthy2xml j (ContThmInst{thyID, thm, bdvs, thminst, applto, applat, 

				    reword, asms, lhs, rhs, result, resasms, 

				    asmrls}) =

    indt j ^ "<GUH> " ^ thm ^ " </GUH>\n" ^

    indt j ^ "<SUBSLIST>\n" ^ (*should be an environment = substitution*)

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

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

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

    indt j ^ "</SUBSLIST>\n" ^

    indt j ^ "<INSTANTIATED>\n" ^

    term2xml j thminst ^ "\n" ^

    indt j ^ "</INSTANTIATED>\n" ^

    indt j ^ "<APPLTO>\n" ^

    term2xml j applto ^ "\n" ^

    indt j ^ "</APPLTO>\n" ^

    indt j ^ "<APPLAT>\n" ^

    term2xml j applat ^ "\n" ^

    indt j ^ "</APPLAT>\n" ^

    indt j ^ "<ORDER>\n" ^ (*should be a theref2xml*)

    indt (j+i) ^"<ID> " ^ reword ^ " </ID>\n" ^

    indt j ^ "</ORDER>\n" ^

    indt j ^ "<ASMSEVAL>\n" ^

    asm_vals2xml (j+i) asms ^

    indt j ^ "</ASMSEVAL>\n" ^

    indt j ^ "<LHS>\n" ^

    term2xml j (fst lhs) ^ "\n" ^

    indt j ^ "</LHS>\n" ^

    indt j ^ "<LHSINST>\n" ^

    term2xml j (snd lhs) ^ "\n" ^

    indt j ^ "</LHSINST>\n" ^

    indt j ^ "<RHS>\n" ^

    term2xml j (fst rhs) ^ "\n" ^

    indt j ^ "</RHS>\n" ^

    indt j ^ "<RHSINST>\n" ^

    term2xml j (snd rhs) ^ "\n" ^

    indt j ^ "</RHSINST>\n" ^

    indt j ^ "<RESULT>\n" ^

    term2xml j result ^ "\n" ^

    indt j ^ "</RESULT>\n" ^

    indt j ^ "<ASSUMPTOIONS>\n" ^

    terms2xml' j resasms ^

    indt j ^ "</ASSUMPTOIONS>\n" ^

    indt j ^ "<EVALRLS>\n" ^

    theref2xml j thyID "Rulesets" asmrls ^

    indt j ^ "</EVALRLS>\n"

  | contthy2xml j (ContRls {thyID, rls, applto, result, asms}) =

    indt j ^ "<GUH> " ^ rls ^ " </GUH>\n" ^

    indt j ^ "<APPLTO>\n" ^

    term2xml j applto ^ "\n" ^

    indt j ^ "</APPLTO>\n" ^

    indt j ^ "<RESULT>\n" ^

    term2xml j result ^ "\n" ^

    indt j ^ "</RESULT>\n" ^

    indt j ^ "<ASSUMPTOIONS>\n" ^

    terms2xml' j asms ^

    indt j ^ "</ASSUMPTOIONS>\n"

  | contthy2xml j (ContRlsInst {thyID, rls, bdvs, applto, result, asms}) =

    indt j ^ "<GUH> " ^ rls ^ " </GUH>\n" ^

    indt j ^ "<SUBSLIST>\n" ^ (*should be an environment = substitution*)

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

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

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

    indt j ^ "</SUBSLIST>\n" ^

    indt j ^ "<APPLTO>\n" ^

    term2xml j applto ^ "\n" ^

    indt j ^ "</APPLTO>\n" ^

    indt j ^ "<RESULT>\n" ^

    term2xml j result ^ "\n" ^

    indt j ^ "</RESULT>\n" ^

    indt j ^ "<ASSUMPTOIONS>\n" ^

    terms2xml' j asms ^

    indt j ^ "</ASSUMPTOIONS>\n"

  | contthy2xml j (ContNOrew {thyID, thm_rls, applto}) =

    indt j ^ "<GUH> " ^ thm_rls ^ " </GUH>\n" ^

    indt j ^ "<APPLTO>\n" ^

    term2xml j applto ^ "\n" ^

    indt j ^ "</APPLTO>\n"

  | contthy2xml j (ContNOrewInst{thyID, thm_rls, bdvs, thminst, applto}) =

    indt j ^ "<GUH> " ^ thm_rls ^ " </GUH>\n" ^

    indt j ^ "<SUBSLIST>\n" ^ (*should be an environment = substitution*)

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

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

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

    indt j ^ "</SUBSLIST>\n" ^

    indt j ^ "<INSTANTIATED>\n" ^

    term2xml j thminst ^ "\n" ^

    indt j ^ "</INSTANTIATED>\n" ^

    indt j ^ "<APPLTO>\n" ^

    term2xml j applto ^ "\n" ^

    indt j ^ "</APPLTO>\n" : xml;

(*------------------------------------------------------------------*)

end

open datatypes;

(*------------------------------------------------------------------*)