1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/xmlsrc/thy-hierarchy.sml Thu Aug 12 11:02:32 2010 +0200
1.3 @@ -0,0 +1,361 @@
1.4 +(*.export theory-data to xml
1.5 + author: Walther Neuper 0601
1.6 + (c) isac-team
1.7 +
1.8 + FIXME.WN0602: re-engineer this file for analogy to pbl-met-hierarchy
1.9 + as follows:
1.10 + # 'fun collect_thydata': unit -> string list * thydata list
1.11 + ^^^^^^^^^^^ hierarchy-key
1.12 + # 'fun thys2file': from this ^^^ datastructure (^^^^^^^^^^^ for free!)
1.13 + # map 'fun store_pbt' (NEW!) over ^^^ into 'thy_data ptyp'
1.14 + # from 'thy_data ptyp' create 'thy_hierarchy'
1.15 +
1.16 +use"xmlsrc/thy-hierarchy.sml";
1.17 +use"thy-hierarchy.sml";
1.18 +.*)
1.19 +
1.20 +
1.21 +(**.collect data and build intermediate structure for hierarchy:
1.22 + theorems, rulesets and Calc's, (TODO rew_ord's etc) defined in isac
1.23 + and Isabelle-thms used in rulesets;
1.24 + this code binds ref-var's and must be after IsacKnowledge .**)
1.25 +
1.26 +(*.collect all theorems defined in in a theory and insert the guh.*)
1.27 +fun makeHthm (part:string, thyID:thyID) (thmID:thmID, thm:thm) =
1.28 + let val theID = [part, thyID, "Theorems"] @ [strip_thy thmID] : theID
1.29 + in (theID, Hthm {guh = theID2guh theID, coursedesign = [],
1.30 + mathauthors = ["isac-team"], thm = thm})
1.31 + end;
1.32 +fun makeHrls (part:string) (rls':rls', thy_rls as (thyID, rls): thyID * rls) =
1.33 + let val theID = [part, thyID,"Rulesets"] @ [rls'] : theID
1.34 + in (theID, Hrls {guh = theID2guh theID, coursedesign=[],
1.35 + mathauthors=["isac-team"], thy_rls = thy_rls})
1.36 + end;
1.37 +fun makeHcal (part:string, thyID:thyID) (calID, cal) =
1.38 + let val theID = [part, thyID,"Operations"] @ [calID] : theID
1.39 + in (theID, Hcal {guh = theID2guh theID, coursedesign=[],
1.40 + mathauthors=["isac-team"], calc = cal})
1.41 + end;
1.42 +fun makeHord (part:string, thyID:thyID) (ordID, ord) =
1.43 + let val theID = [part, thyID,"TODO-Orders"] @ [ordID] : theID
1.44 + in (theID, Hord {guh = theID2guh theID, coursedesign=[],
1.45 + mathauthors=["isac-team"], ord = ord})
1.46 + end;
1.47 +
1.48 +
1.49 +fun collect_thms' (part, thy') =
1.50 + let val thy = assoc_thy (thyID2theory' thy')
1.51 + in map (makeHthm (part, thy')) (thms_of thy) end;
1.52 +
1.53 +(*.collect all rulesets defined in in a theory and insert the guh.*)
1.54 +fun collect_rlss (part, thy') =
1.55 + let val rlss = filter ((curry op= thy') o
1.56 + ((#1 o #2):(rls' * (theory' * rls)) -> theory'))
1.57 + (!ruleset')
1.58 + in map (makeHrls part) rlss end;
1.59 +
1.60 +(*.collect all calcs defined in in a theory.*)
1.61 +fun collect_cals (part, thy') =
1.62 + let val cals = [] (*FIXXXXXXXXXXME.WN060713 add thyID: (thyID, cal)*)
1.63 + in map (makeHcal (part, thy')) cals end;
1.64 +
1.65 +
1.66 +(*.collect all rew_ord's defined in in a theory.*)
1.67 +fun collect_ords (part, thy') =
1.68 + let val thy = assoc_thy (thyID2theory' thy')
1.69 + in [(*TODO.WN060120 rew_ord, Calc*)]:(theID * thydata) list end;
1.70 +
1.71 +(*.collect all data for a thy TODO.WN060120 rew_ord, Calc.*)
1.72 +(* val thy' = nth 1 scri_thys;
1.73 + *)
1.74 +fun collect_thy part(*IsacScripts|IsacKnowledge*) (thy': theory') =
1.75 + ((collect_thms' (part, thy')) @ (collect_rlss (part, thy')) @
1.76 + (collect_cals (part, thy')) @ (collect_ords (part, thy')))
1.77 + : (theID * thydata) list;
1.78 +
1.79 +(*.collect theorems defined in Isabelle (before Isac is evaluated above).*)
1.80 +fun collect_isab isa (thyID, (thmID, thm)) =
1.81 + let val theID = [isa, thyID, "Theorems", thmID]
1.82 + in (theID:theID, Hthm {guh = theID2guh theID,
1.83 + mathauthors = ["Isabelle team, TU Munich"],
1.84 + coursedesign = [],
1.85 + thm = thm}) end;
1.86 +
1.87 +val isabelle_page = (["Isabelle"] : theID,
1.88 + Html {guh = theID2guh ["Isabelle"],
1.89 + html = "",
1.90 + mathauthors = ["Isabelle team, TU Munich"],
1.91 + coursedesign = []});
1.92 +
1.93 +(*.create a list with all thydata=thyelements=the;
1.94 + this list is used by 'fun the_hier' to create the hierarchy .*)
1.95 +fun collect_thydata () =
1.96 + let val isab_thms = map rearrange_inv (!isab_thm_thy)
1.97 + val scri_thys = (map (get_thy o #1) (!script_thys))
1.98 + \\ ["e_domID"]
1.99 + val isac_thys = (map (get_thy o #1)
1.100 + (!theory')) \\ scri_thys \\ ["e_domID"]
1.101 + in [isabelle_page] @
1.102 + (map (collect_isab "Isabelle") isab_thms) @
1.103 + ((flat o (map (collect_thy "IsacScripts"))) scri_thys) @
1.104 + ((flat o (map (collect_thy "IsacKnowledge"))) isac_thys)
1.105 + : (theID * thydata) list
1.106 + end;
1.107 +
1.108 +fun show_thes () = (writeln o format_pblIDl o (scan [])) (!thehier);
1.109 +
1.110 +
1.111 +
1.112 +(***.create the xml-format for the hierarchy.***)
1.113 +
1.114 +(**.make a hierarchy from (theID * thydata) list created by 'fun collect_thy';
1.115 + use the same mechanism as for pbl_hierarchy and met_hierarchy;
1.116 + but check, if a thydata is already there (for auto-gen. Isabelle).**)
1.117 +
1.118 +(*.for preserving elements created by 'fun store_thy'.*)
1.119 +fun exist_the (theID:theID) (thy_hie:thehier) =
1.120 + let fun node theID ids (Ptyp (id,_,ns)) =
1.121 + if theID = ids @ [id] then true
1.122 + else nodes theID (ids @ [id]) ns
1.123 + and nodes _ _ [] = false
1.124 + | nodes theID ids (n::ns) = if node theID ids n then true
1.125 + else nodes theID ids ns
1.126 + in nodes theID [] thy_hie end;
1.127 +
1.128 +(*.insrt requires a parent; see 'fun fill_parents'.*)
1.129 +fun can_insert (theID:theID) (thy_hie:thehier) =
1.130 + (insrt theID e_thydata theID thy_hie; true)
1.131 + handle _ => false;
1.132 +
1.133 +(*.cut 'theID', the ID of theory elements from tail to head
1.134 + until insertion into the hierarchy of theory elements 'th' is possible
1.135 + (the hierarchy requires the parentnode to exist for insertion).*)
1.136 +fun cut_theID th ([]:theID) =
1.137 + raise error "could not insert into thy-hierarchy"
1.138 + | cut_theID th theID =
1.139 + if can_insert theID th
1.140 + then theID else cut_theID th (drop_last theID);
1.141 +
1.142 +(*.insert empty parents 'Html' into the hierarchy of theory elements 'th'
1.143 + until the actual node can be inserted with key 'theID'.*)
1.144 +(* val (th, cutID, theID) = (th, theID, theID);
1.145 + val (th, cutID, theID) = (th', cutID_, theID);
1.146 + *)
1.147 +fun fill_parents th cutID theID =
1.148 + let val cutID' = cut_theID th cutID
1.149 + in if cutID' = theID
1.150 + then th
1.151 + else let val th' = insrt cutID' (Html {guh=theID2guh theID,
1.152 + coursedesign=["isac team 2006"],
1.153 + mathauthors=[],
1.154 + html=""}) cutID' th
1.155 + val cutID_ = cutID' @ [nth ((length cutID') + 1) theID]
1.156 + in fill_parents th' cutID_ theID end
1.157 + end;
1.158 +
1.159 +(*.create the hierarchy from a list (generated automatically);
1.160 + thus, missing parents of list-elems are inserted
1.161 + (causing msgs '*** insert: not found');
1.162 + elemes already store_*d in some *.ML are NOT overwritten.*)
1.163 +fun the_hier th ([]: (theID * thydata) list) = th
1.164 +(* val (th, (theID, thydata)::ths) = (!thehier, collect_thydata ());
1.165 + *)
1.166 + | the_hier th ((theID, thydata)::ths) =
1.167 + if can_insert theID th
1.168 + then let val th' = if exist_the theID th
1.169 + then (writeln ("*** insert: preserved "^strs2str theID);
1.170 + th)
1.171 + else insrt theID thydata theID th
1.172 + in the_hier th' ths end
1.173 + else let val th' = fill_parents th theID theID (*..*** insert: not found*)
1.174 + val th' = insrt theID thydata theID th'
1.175 + in the_hier th' ths end;
1.176 +
1.177 +
1.178 +(*these files shall contain 'invisible' html
1.179 +val thydatafilename = "thy_datafile.xml"; (*for "Theorems"|...*)
1.180 +fun partfilename str = "thy_" ^ str ^ ".xml"; (*for "Isabelle"|...*)*)
1.181 +
1.182 +(*.create an xml-hierarchy where the filname is created from the guh.*)
1.183 +(*ad DTD: a NODE contains an ID and zero or more NODEs*)
1.184 +fun hierarchy_guh h =
1.185 + let val i = indentation
1.186 + val j = indentation
1.187 + fun node i p theID (Ptyp (id,_,ns)) =
1.188 + let val p' = lev_on p
1.189 + val theID' = theID @ [id]
1.190 + in (indt i) ^ "<NODE>\n" ^
1.191 + (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^
1.192 + (indt (i+j)) ^ "<NO> " (*on this level*) ^
1.193 + (string_of_int o last_elem) p' ^ " </NO>\n" ^
1.194 + (indt (i+j)) ^ "<CONTENTREF> " ^ theID2guh theID' ^
1.195 + " </CONTENTREF>\n" ^
1.196 + (nodes (i+j) (lev_dn p') theID' ns) ^
1.197 + (indt i) ^ "</NODE>\n"
1.198 + end
1.199 + and nodes _ _ _ [] = ""
1.200 + | nodes i p theID (n::ns) = (node i p theID n)
1.201 + ^ (nodes i (lev_on p) theID ns);
1.202 + in nodes j [0] [] h end;
1.203 +
1.204 +fun thy_hierarchy2file (path:path) =
1.205 + str2file (path ^ "thy_hierarchy.xml")
1.206 + ("<NODE>\n" ^
1.207 + " <ID> theory hierarchy </ID>\n" ^
1.208 + " <NO> 1 </NO>\n" ^
1.209 + " <CONTENTREF> thy_ROOT </CONTENTREF>\n" ^
1.210 + (hierarchy_guh (!thehier)) ^
1.211 + "</NODE>");
1.212 +
1.213 +
1.214 +(**.create the xml-files for the theory-data from the hierarchy.**)
1.215 +
1.216 +val i = indentation;
1.217 +(*.analoguous to 'fun met2xml'.*)
1.218 +fun thydata2xml (theID:theID, Html {guh, coursedesign, mathauthors, html}) =
1.219 + "<HTMLDATA>\n" ^
1.220 + indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
1.221 + id2xml i theID ^
1.222 + indt i ^ "<EXPLANATIONS> " ^ html ^ "</EXPLANATIONS>\n" ^
1.223 + authors2xml i "MATHAUTHORS" mathauthors ^
1.224 + authors2xml i "COURSEDESIGNS" coursedesign ^
1.225 + "</HTMLDATA>\n" : xml
1.226 + | thydata2xml (theID:theID, Hthm {guh, coursedesign, mathauthors, thm}) =
1.227 + "<THEOREMDATA>\n" ^
1.228 + indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
1.229 + id2xml i theID ^
1.230 + thm''2xml i thm ^
1.231 + indt i ^ "<PROOF>\n" ^
1.232 + extref2xml (i+i) "Proof of the theorem"
1.233 + ("http://www.ist.tugraz.at/projects/isac/www/\
1.234 + \kbase/thy/browser_info/HOL/HOL-Real/Isac/" ^
1.235 + nth 2 theID ^ ".html") ^
1.236 + indt i ^ "</PROOF>\n" ^
1.237 + indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
1.238 + authors2xml i "MATHAUTHORS" mathauthors ^
1.239 + authors2xml i "COURSEDESIGNS" coursedesign ^
1.240 + "</THEOREMDATA>\n"
1.241 +(* val (theID:theID, Hrls {guh, coursedesign, mathauthors, thy_rls}) =
1.242 + (theID, thydata);
1.243 + *)
1.244 + | thydata2xml (theID, Hrls {guh, coursedesign, mathauthors, thy_rls}) =
1.245 + "<RULESETDATA>\n" ^
1.246 + indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
1.247 + id2xml i theID ^
1.248 + rls2xml i thy_rls ^
1.249 + indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
1.250 + authors2xml i "MATHAUTHORS" mathauthors ^
1.251 + authors2xml i "COURSEDESIGNS" coursedesign ^
1.252 + "</RULESETDATA>\n"
1.253 +(* val (theID:theID, Hcal {guh, coursedesign, mathauthors, calc}) =
1.254 + (theID, rlsdata);
1.255 + *)
1.256 + | thydata2xml (theID, Hcal {guh, coursedesign, mathauthors, calc}) =
1.257 + "<RULESETDATA>\n" ^
1.258 + indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
1.259 + id2xml i theID ^
1.260 + calc2xml i (theID2thyID theID, calc) ^
1.261 + indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
1.262 + authors2xml i "MATHAUTHORS" mathauthors ^
1.263 + authors2xml i "COURSEDESIGNS" coursedesign ^
1.264 + "</RULESETDATA>\n"
1.265 + | thydata2xml (theID, _) =
1.266 + raise error ("thydata2xml: not implemented for "^ strs2str' theID);
1.267 +
1.268 +(*.analoguous to 'fun met2file'.*)
1.269 +fun thydata2file (xmldata:path) (pos:pos) (theID:theID) thydata =
1.270 + (writeln ("### thes2file: id = " ^ strs2str theID);
1.271 + str2file (xmldata ^ theID2filename theID)
1.272 + (thydata2xml (theID:theID, thydata)));
1.273 +
1.274 +(*.analoguous to 'fun node'; here we scan ??????????.*)
1.275 +(* val (pa, ids, po, wfn, (Ptyp (id,[n],ns))) =
1.276 + (pa, ids, po, wfn, n);
1.277 + *)
1.278 +fun thenode (pa:path) ids po wfn (Ptyp (id,[n],ns)) =
1.279 + let val po' = lev_on po
1.280 + in wfn pa po' (ids@[id]) n;
1.281 + thenodes pa (ids@[id]) ((lev_dn po'):pos) wfn ns end
1.282 +(* val (pa, ids, po, wfn, (n::ns)) =
1.283 + (path, []:string list, [0], thydata2file, (!thehier));
1.284 + *)
1.285 +and thenodes _ _ _ _ [] = ()
1.286 + | thenodes pa ids po wfn (n::ns) = (thenode pa ids po wfn n;
1.287 + thenodes pa ids (lev_on po) wfn ns);
1.288 +
1.289 +(*..analoguous to 'fun mets2file'*)
1.290 +fun thes2file (p : path) =
1.291 + thenodes p [] [0] thydata2file (!thehier);
1.292 +
1.293 +
1.294 +(***.store a single theory element in the hierarchy.***)
1.295 +
1.296 +(*.for mathauthors only, other html is added to xml exported from here.*)
1.297 +(* val (theID, mathauthors) =
1.298 + (["IsacKnowledge", theory2thyID Biegelinie.thy, "Theorems"],
1.299 + ["Walther Neuper 2005 supported by a grant from NMI Austria"]);
1.300 + *)
1.301 +fun store_isa (theID : theID) (mathauthors : authors) =
1.302 + let val guh = case theID of
1.303 + [part] => part2guh theID
1.304 + | [part, thyID, thypart] => thypart2guh theID
1.305 + val theID = guh2theID guh
1.306 + val the = Html {guh = guh,
1.307 + coursedesign = [],
1.308 + mathauthors = mathauthors,
1.309 + html = ""}
1.310 + in (*needs no (!check_guhs_unique) because guh is generated automatically*)
1.311 + thehier := insrt theID the theID (!thehier) end;
1.312 +
1.313 +fun store_thy thy (mathauthors : authors) =
1.314 + let val guh = thy2guh ["IsacKnowledge", theory2thyID thy]
1.315 + val theID = guh2theID guh
1.316 + val the = Html {guh = guh,
1.317 + coursedesign = [],
1.318 + mathauthors = mathauthors,
1.319 + html = ""}
1.320 + in (*needs no (!check_guhs_unique) because guh is generated automatically*)
1.321 + thehier := insrt theID the theID (!thehier) end;
1.322 +
1.323 +fun store_thm thy (thmID : thmID, thm) (mathauthors : authors) =
1.324 + let val guh = thm2guh ("IsacKnowledge", theory2thyID thy) thmID
1.325 + val theID = guh2theID guh
1.326 + val the = Hthm {guh = guh,
1.327 + coursedesign = [], (*done at xml exported from here*)
1.328 + mathauthors=mathauthors,
1.329 + thm = thm}
1.330 + in (*needs no (!check_guhs_unique) because guh is generated automatically*)
1.331 + thehier := insrt theID the theID (!thehier) end;
1.332 +
1.333 +fun store_rls thy rls (mathauthors : authors) =
1.334 + let val guh = rls2guh ("IsacKnowledge", theory2thyID thy)
1.335 + ((#id o rep_rls) rls)
1.336 + val theID = guh2theID guh
1.337 + val the = Hrls {guh = guh,
1.338 + coursedesign = [],
1.339 + mathauthors = mathauthors,
1.340 + thy_rls=(theory2thyID thy, rls)}
1.341 + in (*needs no (!check_guhs_unique) because guh is generated automatically*)
1.342 + thehier := insrt theID the theID (!thehier) end;
1.343 +
1.344 +fun store_cal thy cal (mathauthors : authors) =
1.345 + let val guh = cal2guh ("IsacKnowledge", theory2thyID thy)
1.346 + ("TODO store_cal")
1.347 + val theID = guh2theID guh
1.348 + val the = Hcal {guh = guh,
1.349 + coursedesign = [],
1.350 + mathauthors = mathauthors,
1.351 + calc = cal}
1.352 + in (*needs no (!check_guhs_unique) because guh is generated automatically*)
1.353 + thehier := insrt theID the theID (!thehier) end;
1.354 +
1.355 +fun store_ord thy ord (mathauthors : authors) =
1.356 + let val guh = ord2guh ("IsacKnowledge", theory2thyID thy)
1.357 + ("TODO store_ord")
1.358 + val theID = guh2theID guh
1.359 + val the = Hord {guh = guh,
1.360 + coursedesign = [],
1.361 + mathauthors = mathauthors,
1.362 + ord = ord}
1.363 + in (*needs no (!check_guhs_unique) because guh is generated automatically*)
1.364 + thehier := insrt theID the theID (!thehier) end;