(*.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"], fillpats = [], 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') (*SWITCH KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")*)

     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 (thmDeriv, thm) =

     let val theID =

       [isa, thyID_of_derivation_name thmDeriv, "Theorems", thmID_of_derivation_name thmDeriv]

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

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

 		     coursedesign = [],

 		     fillpats = [],

 		     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 () =

   [isabelle_page] @

   (map (collect_isab "Isabelle") (! isab_thm_thy)) @ 

   ((flat o (map (collect_thy "IsacScripts"))) (map Context.theory_name (! progthys))) @

   ((flat o (map (collect_thy "IsacKnowledge"))) (map Context.theory_name (! knowthys))): 

 (theID * thydata) list; 

 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'.*)

 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

   | 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, fillpats(*TODO?*), 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"

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

       "<RULESETDATA>\n" ^

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

       id2xml i theID ^

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

       authors2xml i "MATHAUTHORS" mathauthors ^

     authors2xml i "COURSEDESIGNS" coursedesign ^

       "</RULESETDATA>\n"

   | 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' *)

 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

 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 part (thmID : thmID, thm) (mathauthors : authors) =

   let

     val guh = thm2guh (part, theory2thyID thy) thmID

     val theID = guh2theID guh

     val the = Hthm {guh = guh, 

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

 			mathauthors = mathauthors,

 			fillpats = [],

 			thm = thm}

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

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

 (*WN120512 DESIGN TODO: build thehier already in respective theories*)

 fun insert_fillpats thy part (thmID : thmID, thm) fillpats =

   let

     val guh = thm2guh (part, theory2thyID thy) thmID

     val theID = guh2theID guh

     val Hthm {guh, coursedesign, mathauthors, thm, ...} = get_the theID

     val the = Hthm {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors,

       fillpats = fillpats, thm = thm}

   in 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)}

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

 	in 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;

 fun update_hthm (Hthm {guh, coursedesign, mathauthors, thm, ...}) fillpats' =

   Hthm {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors,

     fillpats = fillpats', thm = thm}

   | update_hthm _ _ = raise ERROR "wrong data";

 (* for interface for dialog-authoring *)

 fun update_hrls (Hrls {guh, coursedesign, mathauthors, thy_rls = (thyID, rls)}) errpatIDs =

   let

     val rls' = 

       case rls of

         Rls {id, preconds, rew_ord, erls, srls, calc, rules, scr, ...} =>

           Rls {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,

             calc = calc, rules = rules, scr = scr, errpatts = errpatIDs}

       | Seq {id, preconds, rew_ord, erls, srls, calc, rules, scr, ...} =>

             Seq {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,

               calc = calc, rules = rules, scr = scr, errpatts = errpatIDs}

       | Rrls {id, prepat, rew_ord, erls, calc, scr, ...} =>

             Rrls {id = id, prepat = prepat, rew_ord = rew_ord, erls = erls, calc = calc,

               scr = scr, errpatts = errpatIDs}

       | Erls => Erls

   in

     Hrls {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors,

       thy_rls = (thyID, rls')}

   end

   | update_hrls _ _ = raise ERROR "wrong data";

 (* interface for dialog-authoring: call in Buld_Thydata.thy only ! *)

 fun insert_fillpats theID fillpats =

   let

     val hthm = get_the theID

     val hthm' = update_hthm hthm fillpats

       handle ERROR _ => error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")

   in thehier := insrt theID hthm' theID (! thehier) end;

 fun insert_errpatIDs theID errpatIDs =

   let

     val hrls = get_the theID

     val hrls' = update_hrls hrls errpatIDs

       handle ERROR _ => error ("insert_errpatIDs: " ^ strs2str theID ^ "must address a rule-set")

   in thehier := insrt theID hrls' theID (! thehier) end;