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;