(*.export theory-data to xml

   author: Walther Neuper 0601

   (c) isac-team

   FIXME.WN0602: re-engineer this file for analogy to pbl-met-hierarchy

   as follows:

   # 'fun collect_thydata': unit -> string list * thydata list

                                    ^^^^^^^^^^^ hierarchy-key

   # 'fun thys2file': from this ^^^ datastructure (^^^^^^^^^^^ for free!)

   # map 'fun store_pbt' (NEW!) over ^^^ into 'thy_data ptyp'

   # from 'thy_data ptyp' create 'thy_hierarchy'

use"xmlsrc/thy-hierarchy.sml";

use"thy-hierarchy.sml";

.*)

(**.collect data and build intermediate structure for hierarchy:

    theorems, rulesets and Calc's, (TODO rew_ord's etc) defined in isac 

    and Isabelle-thms used in rulesets;

    this code binds ref-var's and must be after IsacKnowledge .**)

(*.collect all theorems defined in in a theory and insert the guh.*)

fun makeHthm (part:string, thyID:thyID) (thmID:thmID, thm:term) =

    let val theID = [part, thyID, "Theorems"] @ [strip_thy thmID] : theID

    in (theID, Hthm {guh = theID2guh theID, coursedesign = [], 

		     mathauthors = ["isac-team"], thm = thm})

    end;

fun makeHrls (part:string) (rls':rls', thy_rls as (thyID, rls): thyID * rls) =

    let val theID = [part, thyID,"Rulesets"] @ [rls'] : theID

    in (theID, Hrls {guh = theID2guh theID, coursedesign=[], 

		     mathauthors=["isac-team"], thy_rls = thy_rls})

    end;

fun makeHcal (part:string, thyID:thyID) (calID, cal) =

    let val theID = [part, thyID,"Operations"] @ [calID] : theID

    in (theID, Hcal {guh = theID2guh theID, coursedesign=[], 

		     mathauthors=["isac-team"], calc = cal})

    end;

fun makeHord (part:string, thyID:thyID) (ordID, ord) =

    let val theID = [part, thyID,"TODO-Orders"] @ [ordID] : theID

    in (theID, Hord  {guh = theID2guh theID, coursedesign=[], 

		      mathauthors=["isac-team"], ord = ord})

    end;

fun collect_thms' (part, thy') =

    let val thy = assoc_thy (thyID2theory' thy')

    in map (makeHthm (part, thy')) (Theory.axioms_of thy) end;

(*.collect all rulesets defined in in a theory and insert the guh.*)

fun collect_rlss (part, thy') = 

    let val rlss = filter ((curry op= thy') o 

			   ((#1 o #2):(rls' * (theory' * rls)) -> theory')) 

			  (!ruleset')

    in map (makeHrls part) rlss end;

(*.collect all calcs defined in in a theory.*)

fun collect_cals (part, thy') =

    let val cals = [] (*FIXXXXXXXXXXME.WN060713 add thyID: (thyID, cal)*)

    in map (makeHcal (part, thy')) cals end;

(*.collect all rew_ord's defined in in a theory.*)

fun collect_ords (part, thy') =

    let val thy = assoc_thy (thyID2theory' thy')

    in [(*TODO.WN060120 rew_ord, Calc*)]:(theID * thydata) list end;

(*.collect all data for a thy TODO.WN060120 rew_ord, Calc.*)

(* val thy' = nth 1 scri_thys;

   *)

fun collect_thy part(*IsacScripts|IsacKnowledge*) (thy': theory') =

    ((collect_thms' (part, thy')) @ (collect_rlss (part, thy')) @ 

     (collect_cals (part, thy')) @ (collect_ords (part, thy')))

    : (theID * thydata) list;

(*.collect theorems defined in Isabelle (before Isac is evaluated above).*)

fun collect_isab isa (thyID, (thmID, thm)) =

    let val theID = [isa, thyID, "Theorems", thmID]

    in (theID:theID, Hthm {guh = theID2guh theID, 

		     mathauthors = ["Isabelle team, TU Munich"],

		     coursedesign = [],

		     thm = thm}) end;

val isabelle_page = (["Isabelle"] : theID,

		     Html {guh = theID2guh ["Isabelle"],

			   html = "",

			   mathauthors = ["Isabelle team, TU Munich"],

			   coursedesign = []});

(*.create a list with all thydata=thyelements=the;

   this list is used by 'fun the_hier' to create the hierarchy .*)

fun collect_thydata () =

    let val isab_thms = map rearrange_inv (!isab_thm_thy)

	val scri_thys = 

            subtract op = ["e_domID"] (map (get_thy o #1) (!script_thys))

	val isac_thys = 

            subtract op = ["e_domID"] 

            (subtract op = scri_thys (map (get_thy o #1) (!theory')))

    in [isabelle_page] @

       (map (collect_isab "Isabelle") isab_thms) @

       ((flat o (map (collect_thy "IsacScripts"))) scri_thys) @

       ((flat o (map (collect_thy "IsacKnowledge"))) isac_thys)

	 : (theID * thydata) list

    end; 

fun show_thes () = (writeln o format_pblIDl o (scan [])) (!thehier);

(***.create the xml-format for the hierarchy.***)

(**.make a hierarchy from (theID * thydata) list created by 'fun collect_thy';

    use the same mechanism as for pbl_hierarchy and met_hierarchy;

    but check, if a thydata is already there (for auto-gen. Isabelle).**)

(*.for preserving elements created by 'fun store_thy'.*)

fun exist_the (theID:theID) (thy_hie:thehier) =

    let fun node theID ids (Ptyp (id,_,ns)) =

	    if theID = ids @ [id] then true

	    else nodes theID (ids @ [id]) ns

	and nodes _ _ [] = false

	  | nodes theID ids (n::ns) = if node theID ids n then true

				      else  nodes theID ids ns

    in nodes theID [] thy_hie end;

(*.insrt requires a parent; see 'fun fill_parents'.*)

fun can_insert (theID:theID) (thy_hie:thehier) = 

    (insrt theID e_thydata theID thy_hie; true)

    handle _ => false;

(*.cut 'theID', the ID of theory elements from tail to head

   until insertion into the hierarchy of theory elements 'th' is possible

   (the hierarchy requires the parentnode to exist for insertion).*)

fun cut_theID th ([]:theID) = 

    error "could not insert into thy-hierarchy"

  | cut_theID th theID  = 

    if can_insert theID th

    then theID else cut_theID th (drop_last theID);

(*.insert empty parents 'Html' into the hierarchy of theory elements 'th'

   until the actual node can be inserted with key 'theID'.*)

(* val (th, cutID, theID) = (th, theID, theID);

   val (th, cutID, theID) = (th', cutID_, theID);

   *)

fun fill_parents th cutID theID =

    let val cutID' = cut_theID th cutID

    in if cutID' = theID

       then th

       else let val th' = insrt cutID' (Html {guh=theID2guh theID,

					      coursedesign=["isac team 2006"],

					      mathauthors=[],

					      html=""}) cutID' th

		val cutID_ = cutID' @ [nth ((length cutID') + 1) theID]

	    in fill_parents th' cutID_ theID end

    end;

(*.create the hierarchy from a list (generated automatically);

   thus, missing parents of list-elems are inserted 

   (causing msgs '*** insert: not found');

   elemes already store_*d in some *.ML are NOT overwritten.*)

fun the_hier th ([]: (theID * thydata) list) = th

(* val (th, (theID, thydata)::ths) = (!thehier, collect_thydata ());

   *)

  | the_hier th ((theID, thydata)::ths) =

    if can_insert theID th 

    then let val th' = if exist_the theID th

		       then (writeln ("*** insert: preserved "^strs2str theID);

			     th)

		       else insrt theID thydata theID th

	 in the_hier th' ths end

    else let val th' = fill_parents th theID theID (*..*** insert: not found*)

	     val th' = insrt theID thydata theID th'

	 in the_hier th' ths end;

(*these files shall contain 'invisible' html

val thydatafilename = "thy_datafile.xml"; (*for "Theorems"|...*)

fun partfilename str = "thy_" ^ str ^ ".xml"; (*for "Isabelle"|...*)*)

(*.create an xml-hierarchy where the filname is created from the guh.*)

(*ad DTD: a NODE contains an ID and zero or more NODEs*)

fun hierarchy_guh h =

    let val i = indentation

	val j = indentation

	fun node i p theID (Ptyp (id,_,ns)) = 

	    let val p' = lev_on p

		val theID' = theID @ [id]

	    in (indt i) ^ "<NODE>\n" ^ 

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

	       (indt (i+j)) ^ "<NO> " (*on this level*) ^ 

	       (string_of_int o last_elem) p' ^ " </NO>\n" ^ 

	       (indt (i+j)) ^ "<CONTENTREF> " ^ theID2guh theID' ^

	       " </CONTENTREF>\n" ^

	       (nodes (i+j) (lev_dn p') theID' ns) ^ 

	       (indt i) ^ "</NODE>\n"

	    end

	and nodes _ _ _ [] = ""

	  | nodes i p theID (n::ns) = (node i p theID n) 

				      ^ (nodes i (lev_on p) theID ns);

    in nodes j [0] [] h end;

fun thy_hierarchy2file (path:path) = 

    str2file (path ^ "thy_hierarchy.xml") 

	     ("<NODE>\n" ^

	      "  <ID> theory hierarchy </ID>\n" ^

	      "  <NO> 1 </NO>\n" ^

	      "  <CONTENTREF> thy_ROOT </CONTENTREF>\n" ^

	     (hierarchy_guh (!thehier)) ^

	     "</NODE>");

(**.create the xml-files for the theory-data from the hierarchy.**)

val i = indentation;

(*.analoguous to 'fun met2xml'.*)

fun thydata2xml (theID:theID, Html {guh, coursedesign, mathauthors, html}) =

    "<HTMLDATA>\n" ^

    indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^

    id2xml i theID ^

    indt i ^ "<EXPLANATIONS> " ^ html ^ "</EXPLANATIONS>\n" ^

    authors2xml i "MATHAUTHORS" mathauthors ^

    authors2xml i "COURSEDESIGNS" coursedesign ^

    "</HTMLDATA>\n" : xml

  | thydata2xml (theID:theID, Hthm {guh, coursedesign, mathauthors, thm}) =

    "<THEOREMDATA>\n" ^

    indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^

    id2xml i theID ^

    term2xml i thm ^

    indt i ^ "<PROOF>\n" ^

    extref2xml (i+i) "Proof of the theorem" 

	       ("http://www.ist.tugraz.at/projects/isac/www/\

		\kbase/thy/browser_info/HOL/HOL-Real/Isac/" ^

		nth 2 theID ^ ".html") ^

    indt i ^  "</PROOF>\n" ^

    indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^

    authors2xml i "MATHAUTHORS" mathauthors ^

    authors2xml i "COURSEDESIGNS" coursedesign ^

    "</THEOREMDATA>\n"

(* val (theID:theID, Hrls {guh, coursedesign, mathauthors, thy_rls}) = 

       (theID, thydata);

   *)

  | thydata2xml (theID, Hrls {guh, coursedesign, mathauthors, thy_rls}) =

    "<RULESETDATA>\n" ^

    indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^

    id2xml i theID ^

    rls2xml i thy_rls ^

    indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^

    authors2xml i "MATHAUTHORS" mathauthors ^

    authors2xml i "COURSEDESIGNS" coursedesign ^

    "</RULESETDATA>\n"

(* val (theID:theID, Hcal {guh, coursedesign, mathauthors, calc}) = 

       (theID, rlsdata);

   *)

  | thydata2xml (theID, Hcal {guh, coursedesign, mathauthors, calc}) =

    "<RULESETDATA>\n" ^

    indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^

    id2xml i theID ^

    calc2xml i (theID2thyID theID, calc) ^

    indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^

    authors2xml i "MATHAUTHORS" mathauthors ^

    authors2xml i "COURSEDESIGNS" coursedesign ^

    "</RULESETDATA>\n"

  | thydata2xml (theID, _) =

    error ("thydata2xml: not implemented for "^ strs2str' theID);

(*.analoguous to 'fun met2file'.*)

fun thydata2file (xmldata:path) (pos:pos) (theID:theID) thydata =

    (writeln ("### thes2file: id = " ^ strs2str theID);

     str2file (xmldata ^ theID2filename theID)

	     (thydata2xml (theID:theID, thydata)));

(*.analoguous to 'fun node'; here we scan ??????????.*)

(* val (pa, ids, po, wfn, (Ptyp (id,[n],ns))) =

       (pa, ids, po, wfn,  n);

   *)

fun thenode (pa:path) ids po wfn (Ptyp (id,[n],ns)) = 

    let val po' = lev_on po

    in wfn pa po' (ids@[id]) n;

    thenodes pa (ids@[id]) ((lev_dn po'):pos) wfn ns end

(* val (pa,   ids,            po,  wfn,            (n::ns)) =

       (path, []:string list, [0], thydata2file, (!thehier));

   *)

and thenodes _ _ _ _ [] = ()

  | thenodes pa ids po wfn (n::ns) = (thenode pa ids po wfn n;

				 thenodes pa ids (lev_on po) wfn ns);

(*..analoguous to 'fun mets2file'*)

fun thes2file (p : path) = 

    thenodes p [] [0] thydata2file (!thehier);

(***.store a single theory element in the hierarchy.***)

(*.for mathauthors only, other html is added to xml exported from here.*)

(* val (theID, mathauthors) = 

       (["IsacKnowledge", theory2thyID Biegelinie.thy, "Theorems"],

	["Walther Neuper 2005 supported by a grant from NMI Austria"]);

   *)

fun store_isa (theID : theID) (mathauthors : authors) =

    let val guh = case theID of

		      [part] => part2guh theID

		    | [part, thyID, thypart] => thypart2guh theID

	val theID = guh2theID guh

	val the = Html {guh = guh, 

			coursedesign = [], 

			mathauthors = mathauthors,

			html = ""}

    in (*needs no (!check_guhs_unique) because guh is generated automatically*)

	thehier := insrt theID the theID (!thehier) end;

fun store_thy thy (mathauthors : authors) =

    let val guh = thy2guh ["IsacKnowledge", theory2thyID thy]

	val theID = guh2theID guh

	val the = Html {guh = guh, 

			coursedesign = [], 

			mathauthors = mathauthors,

			html = ""}

    in (*needs no (!check_guhs_unique) because guh is generated automatically*)

	thehier := insrt theID the theID (!thehier) end;

fun store_thm thy (thmID : thmID, thm) (mathauthors : authors) =

    let val guh = thm2guh ("IsacKnowledge", theory2thyID thy) thmID

	val theID = guh2theID guh

	val the = Hthm {guh = guh, 

			coursedesign = [], (*done at xml exported from here*)

			mathauthors=mathauthors,

			thm = thm}

    in (*needs no (!check_guhs_unique) because guh is generated automatically*)

	thehier := insrt theID the theID (!thehier) end;

fun store_rls thy rls (mathauthors : authors) =

    let val guh = rls2guh ("IsacKnowledge", theory2thyID thy) 

			  ((#id o rep_rls)  rls)

	val theID = guh2theID guh

	val the = Hrls {guh = guh,

			coursedesign = [], 

			mathauthors = mathauthors,

			thy_rls=(theory2thyID thy, rls)}

    in (*needs no (!check_guhs_unique) because guh is generated automatically*)

	thehier := insrt theID the theID (!thehier) end;

fun store_cal thy cal (mathauthors : authors) =

    let val guh = cal2guh ("IsacKnowledge", theory2thyID thy)

			  ("TODO store_cal")

	val theID = guh2theID guh

	val the = Hcal {guh = guh,

			coursedesign = [],

			mathauthors = mathauthors,

			calc = cal}

    in (*needs no (!check_guhs_unique) because guh is generated automatically*)

	thehier := insrt theID the theID (!thehier) end;

fun store_ord thy ord (mathauthors : authors) =

    let val guh = ord2guh ("IsacKnowledge", theory2thyID thy)

			  ("TODO store_ord")

	val theID = guh2theID guh

	val the = Hord {guh = guh,

			coursedesign = [],

			mathauthors = mathauthors,

			ord = ord}

    in (*needs no (!check_guhs_unique) because guh is generated automatically*)

	thehier := insrt theID the theID (!thehier) end;