diff -r 5100a9c3abf8 -r 875b6efa7ced src/Pure/isac/xmlsrc/datatypes.sml
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/isac/xmlsrc/datatypes.sml Wed Jul 21 13:53:39 2010 +0200
@@ -0,0 +1,843 @@
+(* 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 =
+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) ^ " " ^ s ^ " \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) ^ " " ^ s ^ " \n" ^
+ (id2x j ss)
+ in (indt j) ^ "\n" ^
+ (id2x (j + indentation) ids) ^
+ (indt j) ^ "\n" end;
+(* writeln(id2xml 8 ["linear","univariate","equation"]);
+
+ linear
+ univariate
+ equation
+ *)
+
+fun ints2xml j ids =
+ let fun int2x _ [] = ""
+ | int2x j (s::ss) = (indt j) ^" "^ string_of_int s ^" \n"^
+ (int2x j ss)
+ in (indt j) ^ "\n" ^
+ (int2x (j + i) ids) ^
+ (indt j) ^ "\n" end;
+(* writeln(ints2xml 3 [1,2,3]);
+ *)
+
+
+(** isac datatypes **)
+
+fun pos_2xml j pos_ =
+ (indt j) ^ " " ^ pos_2str 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_ *)
+ indt j ^ "\n"^
+ term2xml j term ^"\n"^
+ indt j ^ "\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 ^ "\n" ^
+ pos'2xml (j+i) ("POSITION", p) ^
+ indt (j+i) ^ "\n"^
+ term2xml (j+i) term ^"\n"^
+ indt (j+i) ^ "\n"^
+ indt j ^ "\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 ^ "\n" ^
+ indt (j+i) ^ " " ^ scrop ^ "\n" ^
+ indt (j+i) ^ " " ^ cal2guh ("IsacKnowledge",
+ thyID) scrop ^ " \n" ^
+ indt j ^ "\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 ^ "\n" ^
+ indt (j+i) ^ "\n" ^ scrop ^ "\n" ^
+ indt (j+i) ^ "\n" ^ cal2guh ("IsacKnowledge",
+ thyID) scrop ^ "\n" ^
+ indt (j+i) ^ "\n" ^ rewop ^ "\n" ^
+ indt j ^ "\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 =
+ raise 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 ^ "\n" ^
+ indt (j+i) ^ " Theorem \n" ^
+ indt (j+i) ^ " " ^ thmID ^ " \n" ^
+ indt (j+i) ^ " " ^ thm2guh (thy_containing_thm thyID thmID)
+ thmID ^ " \n" ^
+ indt j ^ "\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 ^ "\n" ^
+ indt (j+i) ^ " " ^ termop ^ " \n" ^
+ indt (j+i) ^ " " ^ cal2guh (thy_containing_cal thyID termop)
+ termop ^ " \n" ^
+ indt j ^ "\n"
+*)
+ | rule2xml j thyID (Cal1 (termop, _)) = ""
+ | rule2xml j thyID (Rls_ rls) =
+ let val rls' = (#id o rep_rls) rls
+ in indt j ^ "\n" ^
+ indt (j+i) ^ " Ruleset \n" ^
+ indt (j+i) ^ " " ^ rls' ^ " \n" ^
+ indt (j+i) ^ " " ^ rls2guh (thy_containing_rls thyID rls')
+ rls' ^ " \n" ^
+ indt j ^ "\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) ^ " \n"
+(* val gis = filterpbl "#Given" p;
+ *)
+ | gis => (indt j) ^ "\n" ^ terms2xml' j gis ^
+ (indt j) ^ "\n")
+ ^
+ (case where_ of
+ [] => (indt j) ^ " \n"
+ | whs => (indt j) ^ "\n" ^ terms2xml' j whs ^
+ (indt j) ^ "\n")
+ ^
+ (case filterpbl "#Find" p of
+ [] => (indt j) ^ " \n"
+ | fis => (indt j) ^ "\n" ^ terms2xml' j fis ^
+ (indt j) ^ "\n")
+ ^
+ (case filterpbl "#Relate" p of
+ [] => (indt j) ^ " \n"
+ | res => (indt j) ^ "\n" ^ terms2xml' j res ^
+ (indt j) ^ "\n");
+(*
+writeln(pattern2xml 3 ((#ppc o get_pbt)
+ ["squareroot","univariate","equation","test"]) []);
+ *)
+
+(*see itm_2item*)
+fun itm_2xml j (Cor (dts,_))=
+ (indt j ^"- \n"^
+ term2xml (j) (comp_dts' dts)^"\n"^
+ indt j ^"
\n"):xml
+ | itm_2xml j (Syn c) =
+ indt j ^"- \n"^
+ indt (j) ^c^
+ indt j ^"
\n"
+ | itm_2xml j (Typ c) =
+ indt j ^"- \n"^
+ indt (j) ^c^
+ indt j ^"
\n"
+ (*type item also has 'False of cterm' set in preconds2xml WN 050618*)
+ | itm_2xml j (Inc (dts,_)) =
+ indt j ^"- \n"^
+ term2xml (j) (comp_dts' dts)^"\n"^
+ indt j ^"
\n"
+ | itm_2xml j (Sup dts) =
+ indt j ^"- \n"^
+ term2xml (j) (comp_dts' dts)^"\n"^
+ indt j ^"
\n"
+ | itm_2xml j (Mis (d,pid)) =
+ indt j ^"- \n"^
+ term2xml (j) (d $ pid)^"\n"^
+ indt j ^"
\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 ^"- \n"^
+ term2xml (j) term^"\n"^
+ indt j ^"
\n"):xml
+ | precond2xml j (false, term) =
+ indt j ^"- \n"^
+ term2xml (j+i) term^"\n"^
+ indt j ^"
\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 ^"\n"^
+ (case filter (eq4 "#Given") itms of
+ [] => (indt (j+i)) ^ " \n"
+ | gis => (indt (j+i)) ^ "\n" ^ itms2xml (j+2*i) gis ^
+ (indt (j+i)) ^ "\n")
+ ^
+ (case where_ of
+ [] => (indt (j+i)) ^ " \n"
+ | whs => (indt (j+i)) ^ "\n" ^ preconds2xml (j+2*i) whs ^
+ (indt (j+i)) ^ "\n")
+ ^
+ (case filter (eq4 "#Find") itms of
+ [] => (indt (j+i)) ^ " \n"
+ | fis => (indt (j+i)) ^ "\n" ^ itms2xml (j+2*i) fis ^
+ (indt (j+i)) ^ "\n")
+ ^
+ (case filter (eq4 "#Relate") itms of
+ [] => (indt (j+i)) ^ " \n"
+ | res => (indt (j+i)) ^ "\n" ^ itms2xml (j+2*i) res ^
+ (indt (j+i)) ^ "\n")^
+ indt j ^"\n"):xml
+ end;
+(* writeln(model2xml 3 itms []);
+ *)
+
+fun spec2xml j ((dI,pI,mI):spec) =
+ (indt j ^"\n"^
+ indt (j+i) ^" "^ dI ^" \n"^
+ indt (j+i) ^"\n"^
+ id2xml (j+2*i) pI ^
+ indt (j+i) ^"\n"^
+ indt (j+i) ^"\n"^
+ id2xml (j+2*i) mI ^
+ indt (j+i) ^"\n"^
+ indt j ^"\n"):xml;
+
+fun modspec2xml j ((b, p_, head, gfr, pre, spec): ocalhd) =
+ (indt j ^"\n"^
+ indt (j+i) ^"\n"^
+ term2xml (j+i) head^"\n"^
+ indt (j+i) ^"\n"^
+ model2xml (j+i) gfr pre ^
+ indt (j+i) ^" "^(case p_ of Pbl => "Pbl"
+ | Met => "Met"
+ | _ => "Und")^" \n"^
+ spec2xml (j+i) spec ^
+ indt j ^"\n"):xml;
+(* writeln (modspec2xml 2 e_ocalhd);
+ *)
+fun pos'calchead2xml j (p:pos', (b, p_, head, gfr, pre, spec): ocalhd) =
+ (indt j ^"\n"^
+ pos'2xml (j+i) ("POSITION", p) ^
+ indt (j+i) ^"\n"^
+ term2xml (j+i) head^"\n"^
+ indt (j+i) ^"\n"^
+ model2xml (j+i) gfr pre ^
+ indt (j+i) ^" "^(case p_ of Pbl => "Pbl"
+ | Met => "Met"
+ | _ => "Und")^" \n"^
+ spec2xml (j+i) spec ^
+ indt j ^"\n"):xml;
+
+fun sub2xml j (id, value) =
+ (indt j ^"\n"^
+ indt j ^" \n"^
+ term2xml (j+i) id ^ "\n" ^
+ indt j ^" \n" ^
+ indt j ^" \n"^
+ term2xml (j+i) value ^ "\n" ^
+ indt j ^" \n" ^
+ indt j ^"\n"):xml;
+fun subs2xml j (subs:subs) =
+ (indt j ^"\n"^
+ foldl op^ ("", map (sub2xml (j+i))
+ (subs2subst (assoc_thy "Isac.thy") subs)) ^
+ indt j ^"\n"):xml;
+(* val subs = [(str2term "bdv", str2term "x")];
+ val subs = ["(bdv, x)"];
+ writeln(subs2xml 0 subs);
+ *)
+fun subst2xml j (subst:subst) =
+ (indt j ^"\n"^
+ foldl op^ ("", map (sub2xml (j+i)) subst) ^
+ indt j ^"\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 ^"\n"^
+ indt (j+i) ^" "^ID^" \n"^
+ indt (j+i) ^"\n"^
+ thmstr2xml (j+i) form^
+ indt (j+i) ^"\n"^
+ indt j ^"\n"):xml;
+
+(*WN060627 scope of thy's not considered ?!?*)
+fun thm''2xml j (thm:thm) =
+ indt j ^"\n"^
+ indt (j+i) ^" "^ (strip_thy o Thm.name_of_thm) thm ^" \n"^
+ term2xml j ((#prop o rep_thm) thm) ^ "\n" ^
+ indt j ^"\n":xml;
+
+
+fun scr2xml j EmptyScr =
+ indt j ^"\n" : xml
+ | scr2xml j (Script term) =
+ if term = e_term
+ then indt j ^"\n"
+ else indt j ^"\n"
+ | scr2xml j (Rfuns _) =
+ indt j ^" reverse rewrite functions \n";
+
+fun prepa12xml j (terms, term) =
+ indt j ^"\n"^
+ indt (j+i) ^"\n"^
+ terms2xml (j+2*i) terms ^
+ indt (j+i) ^"\n"^
+ indt (j+i) ^"\n"^
+ term2xml (j+2*i) term ^
+ indt (j+i) ^"\n"^
+ indt j ^"\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 ^"\n"^
+ indt (j+i) ^" "^ id ^" \n"^
+ indt (j+i) ^" "^ seqrls ^" \n"^
+ indt (j+i) ^"\n" ^
+ rules2xml (j+2*i) thyID rules ^
+ indt (j+i) ^"\n" ^
+ indt (j+i) ^" " ^
+ terms2xml' (j+2*i) preconds ^
+ indt (j+i) ^"\n" ^
+ indt (j+i) ^"\n" ^
+ indt (j+2*i) ^ " " ^ ord ^ " \n" ^
+(*WN060714 thy_isac_*-ord-*.xml not yet generated ................
+ indt (j+2*i) ^ " " ^ ord2guh ("IsacKnowledge",
+ thyID) ord ^ " \n" ^
+..................................................................*)
+ indt (j+i) ^"\n" ^
+ indt (j+i) ^"\n" ^
+ indt (j+2*i) ^ " Ruleset \n" ^
+ indt (j+2*i) ^ " " ^ id_rls erls ^ " \n" ^
+ indt (j+2*i) ^ " " ^ rls2guh ("IsacKnowledge", thyID)
+ (id_rls erls) ^ " \n" ^
+ indt (j+i) ^"\n" ^
+ indt (j+i) ^"\n" ^
+ indt (j+2*i) ^ " Ruleset \n" ^
+ indt (j+2*i) ^ " " ^ id_rls erls ^ " \n" ^
+ indt (j+2*i) ^ " " ^ rls2guh ("IsacKnowledge", thyID)
+ (id_rls srls) ^ " \n" ^
+ indt (j+i) ^"\n" ^
+ calcrefs2xml (j+i) (thyID, calc) ^
+ scr2xml (j+i) scr ^
+ indt j ^"\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 ^"\n"^
+ indt (j+i) ^" "^ id ^" \n"^
+ indt (j+i) ^" Rrls \n"^
+ prepat2xml (j+i) prepat ^
+ indt (j+i) ^" " ^
+ indt (j+2*i) ^ " Rewrite order \n" ^
+ indt (j+2*i) ^ " " ^ ord ^ " \n" ^
+(*WN060714 thy_isac_*-ord-*.xml not yet generated ................
+ indt (j+2*i) ^ " " ^ ord2guh ("IsacKnowledge",
+ thyID) ord ^ " \n" ^
+.................................................................*)
+ indt (j+i) ^"\n" ^
+ indt (j+i) ^" " ^
+ indt (j+2*i) ^ " Ruleset \n" ^
+ indt (j+2*i) ^ " " ^ id_rls erls ^ " \n" ^
+ indt (j+2*i) ^ " " ^ rls2guh ("IsacKnowledge", thyID)
+ (id_rls erls) ^ " \n" ^
+ indt (j+i) ^"\n" ^
+ calcrefs2xml (j+i) (thyID, calc) ^
+ indt (j+i) ^"\n"^
+ indt j ^"\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 ^"\n"^
+ indt (j+i) ^" "^ dI ^" \n"^
+ indt (j+i) ^"\n"^
+ id2xml (j+2*i) pI^
+ indt (j+i) ^"\n"^
+ indt j ^"\n"):xml
+ | tac2xml j Model_Problem =
+ (indt j ^""^
+ indt j ^"\n"):xml
+ | tac2xml j (Refine_Tacitly pI) =
+ (indt j ^"\n"^
+ id2xml (j+i) pI^
+ indt j ^"\n"):xml
+
+ | tac2xml j (Add_Given ct) =
+ (indt j ^"\n"^
+ cterm2xml (j+i) ct^
+ indt j ^"\n"):xml
+ | tac2xml j (Add_Find ct) =
+ (indt j ^"\n"^
+ cterm2xml (j+i) ct^
+ indt j ^"\n"):xml
+ | tac2xml j (Add_Relation ct) =
+ (indt j ^"\n"^
+ cterm2xml (j+i) ct^
+ indt j ^"\n"):xml
+
+ | tac2xml j (Specify_Theory ct) =
+ (indt j ^"\n"^
+ cterm2xml (j+i) ct^(*WN060513 Specify_Theory = fn : domID -> tac
+and domID is a string, not a cterm *)
+ indt j ^"\n"):xml
+ | tac2xml j (Specify_Problem ct) =
+ (indt j ^"\n"^
+ id2xml (j+i) ct^
+ indt j ^"\n"):xml
+ | tac2xml j (Specify_Method ct) =
+ (indt j ^"\n"^
+ id2xml (j+i) ct^
+ indt j ^"\n"):xml
+ | tac2xml j (Apply_Method mI) =
+ (indt j ^"\n"^
+ id2xml (j+i) mI^
+ indt j ^"\n"):xml
+
+ | tac2xml j (Take ct) =
+ (indt j ^"\n"^
+ cterm2xml (j+i) ct^
+ indt j ^"\n"):xml
+ | tac2xml j (Calculate opstr) =
+ (indt j ^"\n"^
+ cterm2xml (j+i) opstr^(*WN060513 Calculate = fn : string -> tac
+ 'string', _NOT_ 'cterm' ..flaw from RG*)
+ indt j ^"\n"):xml
+(* val (j, Rewrite thm') = (i, tac);
+ *)
+ | tac2xml j (Rewrite thm') =
+ (indt j ^"\n"^
+ thm'2xml (j+i) thm'^
+ indt j ^"\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 ^"\n"^
+ subs2xml (j+i) subs^
+ thm'2xml (j+i) thm'^
+ indt j ^"\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 ^"\n"^
+ indt (j+i) ^" "^ rls' ^" \n"^
+ indt j ^"\n"):xml
+ | tac2xml j (Rewrite_Set_Inst (subs, rls')) =
+ (indt j ^"\n"^
+ indt (j+i) ^" "^ rls' ^" \n"^
+ subs2xml (j+i) subs^
+ indt j ^"\n"):xml
+
+ | tac2xml j (Or_to_List) =
+ (indt j ^" \
+ \\n"):xml
+ | tac2xml j (Check_elementwise ct) =
+ (indt j ^"\n"^
+ cterm2xml (j+i) ct ^ "\n"^
+ indt j ^"\n"):xml
+ (*WN0605 quick and dirty: cterms is _NOT_ a stringlist like pblID...*)
+ | tac2xml j (Substitute cterms) =
+ (indt j ^"\n"^
+ (*cterms2xml (j+i) cterms^ ....should be WN060514: TODO TERMLISTTACTIC?*)
+ id2xml (j+i) cterms^
+ indt j ^"\n"):xml
+ | tac2xml j (Check_Postcond pI) =
+ (indt j ^"\n"^
+ id2xml (j+i) pI^
+ indt j ^"\n"):xml
+
+ | tac2xml j tac = raise 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 ^"\n"^
+ pos'2xml (j+i) ("POSITION", p) ^
+ indt (j+i) ^"\n"^
+ term2xml (j+i) f^"\n"^
+ indt (j+i) ^"\n"^
+ indt j ^"\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 (assoc_thy "Script.thy")))
+ ("Problem (" ^ e_domID ^ "," ^ strs2str' e_pblID ^ ")");
+
+(*WN051224 minimal adaption to exporting Formulae _only_ by getFormulaeFromTo*)
+fun posterm2xml j (p:pos', t) =
+ indt j ^"\n"^
+ pos'2xml (j+i) ("POSITION", p) ^
+ indt (j+i) ^"\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) ^"\n"^
+ indt j ^"\n";
+
+fun posterms2xml j [] = ("":xml)
+ | posterms2xml j (r::rs) = posterm2xml j r ^ posterms2xml j rs;
+
+fun asm_val2xml j (asm, vl) =
+ indt j ^ "\n" ^
+ indt (j+i) ^ "\n" ^
+ term2xml (j+i) asm ^ "\n" ^
+ indt (j+i) ^ "\n" ^
+ indt (j+i) ^ "\n" ^
+ term2xml (j+i) vl ^ "\n" ^
+ indt (j+i) ^ "\n" ^
+ indt j ^ "\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 ^ "\n" ^
+ indt (j+i) ^ " " ^ typ' ^ " \n" ^
+ indt (j+i) ^ " " ^ xstring ^ " \n" ^
+ indt (j+i) ^ " " ^ guh ^ " \n" ^
+ indt j ^ "\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 ^ "\n" ^
+ indt (j+i) ^ " " ^ ketype2str' typ ^ "\n" ^
+ indt (j+i) ^ " " ^ id ^ " \n" ^
+ indt (j+i) ^ " " ^ guh ^ " \n" ^
+ indt j ^ "\n" : xml
+ end;
+
+(*url to a source external to isac*)
+fun extref2xml j linktext url =
+ indt j ^ "\n" ^
+ indt (j+i) ^ " " ^ linktext ^ " \n" ^
+ indt (j+i) ^ " " ^ url ^ " \n" ^
+ indt j ^ "\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 =
+ raise error "contthy2xml called with EContThy"
+ | contthy2xml j (ContThm {thyID, thm, applto, applat, reword,
+ asms,lhs, rhs, result, resasms, asmrls}) =
+ indt j ^ " " ^ thm ^ " \n" ^
+ indt j ^ "\n" ^
+ term2xml j applto ^ "\n" ^
+ indt j ^ "\n" ^
+ indt j ^ "\n" ^
+ term2xml j applat ^ "\n" ^
+ indt j ^ "\n" ^
+ indt j ^ "\n" ^ (*should be a theref2xml*)
+ indt (j+i) ^" " ^ reword ^ " \n" ^
+ indt j ^ "\n" ^
+ indt j ^ "\n" ^
+ asm_vals2xml (j+i) asms ^
+ indt j ^ "\n" ^
+ indt j ^ "\n" ^
+ term2xml j (fst lhs) ^ "\n" ^
+ indt j ^ "\n" ^
+ indt j ^ "\n" ^
+ term2xml j (snd lhs) ^ "\n" ^
+ indt j ^ "\n" ^
+ indt j ^ "\n" ^
+ term2xml j (fst rhs) ^ "\n" ^
+ indt j ^ "\n" ^
+ indt j ^ "\n" ^
+ term2xml j (snd rhs) ^ "\n" ^
+ indt j ^ "\n" ^
+ indt j ^ "\n" ^
+ term2xml j result ^ "\n" ^
+ indt j ^ "\n" ^
+ indt j ^ "\n" ^
+ terms2xml' j resasms ^
+ indt j ^ "\n" ^
+ indt j ^ "\n" ^
+ theref2xml j thyID "Rulesets" asmrls ^
+ indt j ^ "\n"
+
+ | contthy2xml j (ContThmInst{thyID, thm, bdvs, thminst, applto, applat,
+ reword, asms, lhs, rhs, result, resasms,
+ asmrls}) =
+ indt j ^ " " ^ thm ^ " \n" ^
+ indt j ^ "\n" ^ (*should be an environment = substitution*)
+ indt (j+i) ^ "\n" ^
+ indt (j+2*i) ^ " " ^ subst2str' bdvs ^ " \n" ^
+ indt (j+i) ^ "\n" ^
+ indt j ^ "\n" ^
+ indt j ^ "\n" ^
+ term2xml j thminst ^ "\n" ^
+ indt j ^ "\n" ^
+ indt j ^ "\n" ^
+ term2xml j applto ^ "\n" ^
+ indt j ^ "\n" ^
+ indt j ^ "\n" ^
+ term2xml j applat ^ "\n" ^
+ indt j ^ "\n" ^
+ indt j ^ "\n" ^ (*should be a theref2xml*)
+ indt (j+i) ^" " ^ reword ^ " \n" ^
+ indt j ^ "\n" ^
+ indt j ^ "\n" ^
+ asm_vals2xml (j+i) asms ^
+ indt j ^ "\n" ^
+ indt j ^ "\n" ^
+ term2xml j (fst lhs) ^ "\n" ^
+ indt j ^ "\n" ^
+ indt j ^ "\n" ^
+ term2xml j (snd lhs) ^ "\n" ^
+ indt j ^ "\n" ^
+ indt j ^ "\n" ^
+ term2xml j (fst rhs) ^ "\n" ^
+ indt j ^ "\n" ^
+ indt j ^ "\n" ^
+ term2xml j (snd rhs) ^ "\n" ^
+ indt j ^ "\n" ^
+ indt j ^ "\n" ^
+ term2xml j result ^ "\n" ^
+ indt j ^ "\n" ^
+ indt j ^ "\n" ^
+ terms2xml' j resasms ^
+ indt j ^ "\n" ^
+ indt j ^ "\n" ^
+ theref2xml j thyID "Rulesets" asmrls ^
+ indt j ^ "\n"
+
+ | contthy2xml j (ContRls {thyID, rls, applto, result, asms}) =
+ indt j ^ " " ^ rls ^ " \n" ^
+ indt j ^ "\n" ^
+ term2xml j applto ^ "\n" ^
+ indt j ^ "\n" ^
+ indt j ^ "\n" ^
+ term2xml j result ^ "\n" ^
+ indt j ^ "\n" ^
+ indt j ^ "\n" ^
+ terms2xml' j asms ^
+ indt j ^ "\n"
+
+ | contthy2xml j (ContRlsInst {thyID, rls, bdvs, applto, result, asms}) =
+ indt j ^ " " ^ rls ^ " \n" ^
+ indt j ^ "\n" ^ (*should be an environment = substitution*)
+ indt (j+i) ^ "\n" ^
+ indt (j+2*i) ^ " " ^ subst2str' bdvs ^ " \n" ^
+ indt (j+i) ^ "\n" ^
+ indt j ^ "\n" ^
+ indt j ^ "\n" ^
+ term2xml j applto ^ "\n" ^
+ indt j ^ "\n" ^
+ indt j ^ "\n" ^
+ term2xml j result ^ "\n" ^
+ indt j ^ "\n" ^
+ indt j ^ "\n" ^
+ terms2xml' j asms ^
+ indt j ^ "\n"
+
+ | contthy2xml j (ContNOrew {thyID, thm_rls, applto}) =
+ indt j ^ " " ^ thm_rls ^ " \n" ^
+ indt j ^ "\n" ^
+ term2xml j applto ^ "\n" ^
+ indt j ^ "\n"
+
+ | contthy2xml j (ContNOrewInst{thyID, thm_rls, bdvs, thminst, applto}) =
+ indt j ^ " " ^ thm_rls ^ " \n" ^
+ indt j ^ "\n" ^ (*should be an environment = substitution*)
+ indt (j+i) ^ "\n" ^
+ indt (j+2*i) ^ " " ^ subst2str' bdvs ^ " \n" ^
+ indt (j+i) ^ "\n" ^
+ indt j ^ "\n" ^
+ indt j ^ "\n" ^
+ term2xml j thminst ^ "\n" ^
+ indt j ^ "\n" ^
+ indt j ^ "\n" ^
+ term2xml j applto ^ "\n" ^
+ indt j ^ "\n" : xml;
+
+
+(*------------------------------------------------------------------*)
+end
+open datatypes;
+(*------------------------------------------------------------------*)