diff -r 5100a9c3abf8 -r 875b6efa7ced src/Pure/isac/xmlsrc/thy-hierarchy.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/isac/xmlsrc/thy-hierarchy.sml Wed Jul 21 13:53:39 2010 +0200 @@ -0,0 +1,361 @@ +(*.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:thm) = + 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')) (thms_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 = (map (get_thy o #1) (!script_thys)) + \\ ["e_domID"] + val isac_thys = (map (get_thy o #1) + (!theory')) \\ scri_thys \\ ["e_domID"] + 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) = + raise 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) ^ "\n" ^ + (indt (i+j)) ^ " " ^ id ^ " \n" ^ + (indt (i+j)) ^ " " (*on this level*) ^ + (string_of_int o last_elem) p' ^ " \n" ^ + (indt (i+j)) ^ " " ^ theID2guh theID' ^ + " \n" ^ + (nodes (i+j) (lev_dn p') theID' ns) ^ + (indt i) ^ "\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") + ("\n" ^ + " theory hierarchy \n" ^ + " 1 \n" ^ + " thy_ROOT \n" ^ + (hierarchy_guh (!thehier)) ^ + ""); + + +(**.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}) = + "\n" ^ + indt i ^ " "^ guh ^" \n" ^ + id2xml i theID ^ + indt i ^ " " ^ html ^ "\n" ^ + authors2xml i "MATHAUTHORS" mathauthors ^ + authors2xml i "COURSEDESIGNS" coursedesign ^ + "\n" : xml + | thydata2xml (theID:theID, Hthm {guh, coursedesign, mathauthors, thm}) = + "\n" ^ + indt i ^ " "^ guh ^" \n" ^ + id2xml i theID ^ + thm''2xml i thm ^ + indt i ^ "\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 ^ "\n" ^ + indt i ^ " \n" ^ + authors2xml i "MATHAUTHORS" mathauthors ^ + authors2xml i "COURSEDESIGNS" coursedesign ^ + "\n" +(* val (theID:theID, Hrls {guh, coursedesign, mathauthors, thy_rls}) = + (theID, thydata); + *) + | thydata2xml (theID, Hrls {guh, coursedesign, mathauthors, thy_rls}) = + "\n" ^ + indt i ^ " "^ guh ^" \n" ^ + id2xml i theID ^ + rls2xml i thy_rls ^ + indt i ^ " \n" ^ + authors2xml i "MATHAUTHORS" mathauthors ^ + authors2xml i "COURSEDESIGNS" coursedesign ^ + "\n" +(* val (theID:theID, Hcal {guh, coursedesign, mathauthors, calc}) = + (theID, rlsdata); + *) + | thydata2xml (theID, Hcal {guh, coursedesign, mathauthors, calc}) = + "\n" ^ + indt i ^ " "^ guh ^" \n" ^ + id2xml i theID ^ + calc2xml i (theID2thyID theID, calc) ^ + indt i ^ " \n" ^ + authors2xml i "MATHAUTHORS" mathauthors ^ + authors2xml i "COURSEDESIGNS" coursedesign ^ + "\n" + | thydata2xml (theID, _) = + raise 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;