1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/xmlsrc/pbl-met-hierarchy.sml Thu Aug 12 11:02:32 2010 +0200
1.3 @@ -0,0 +1,329 @@
1.4 +(* export problem-data and method-data to xml
1.5 + author: Walther Neuper
1.6 + (c) isac-team
1.7 +
1.8 +use"xmlsrc/pbl-met-hierarchy.sml";
1.9 +use"pbl-met-hierarchy.sml";
1.10 +*)
1.11 +
1.12 +fun str2file (fnm:filename) (str:string) =
1.13 + let val file = TextIO.openOut fnm
1.14 + in (TextIO.output (file, str);
1.15 + TextIO.flushOut file;
1.16 + TextIO.closeOut file) end;
1.17 +fun pos2filename [] = raise error "pos2filename called with []"
1.18 + | pos2filename [i] = "_" ^ string_of_int i ^ ".xml"
1.19 + | pos2filename (i::is) = "_" ^ string_of_int i ^ pos2filename is;
1.20 +(* pos2filename [1,22,3];
1.21 +val it = "_1_22_3.xml" : string
1.22 +*)
1.23 +fun id2filename [] = raise error "id2filename called with []"
1.24 + | id2filename [s] = s ^ ".xml"
1.25 + | id2filename (s::ss) = s ^ "_" ^ id2filename ss;
1.26 +(* id2filename ["linear","univariate","equation"];
1.27 +val it = "linear_univariate_equation.xml" : string
1.28 +*)
1.29 +
1.30 +
1.31 +
1.32 +(*ad DTD: a NODE contains an ID and zero or more NODEs*)
1.33 +(*old version with pos2filename*)
1.34 +fun hierarchy pm(*"pbl" | "met"*) h =
1.35 + let val j = indentation
1.36 + fun nd i p (Ptyp (id,_,ns)) =
1.37 + let val p' = lev_on p
1.38 + in (indt i) ^ "<NODE>\n" ^
1.39 + (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^
1.40 + (indt (i+j)) ^ "<NO> " (*on this level*) ^
1.41 + (string_of_int o last_elem) p' ^ " </NO>\n" ^
1.42 + (indt (i+j)) ^ "<CONTENTREF> " ^ pm ^ pos2filename p' ^
1.43 + " </CONTENTREF>\n" ^
1.44 + (nds (i+j) (lev_dn p') ns) ^
1.45 + (indt i) ^ "</NODE>\n"
1.46 + end
1.47 + and nds _ _ [] = ""
1.48 + | nds i p (n::ns) = (nd i p n) ^ (nds i (lev_on p) ns);
1.49 + in nds j [0] h end;
1.50 +(*.create a hierarchy with references to the guh's.*)
1.51 +fun hierarchy_pbl h =
1.52 + let val j = indentation
1.53 + fun nd i p (Ptyp (id,[n as {guh,...} : pbt],ns)) =
1.54 + let val p' = lev_on p
1.55 + in (indt i) ^ "<NODE>\n" ^
1.56 + (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^
1.57 + (indt (i+j)) ^ "<NO> " (*on this level*) ^
1.58 + (string_of_int o last_elem) p' ^ " </NO>\n" ^
1.59 + (indt (i+j)) ^ "<CONTENTREF> " ^ guh ^
1.60 + " </CONTENTREF>\n" ^
1.61 + (nds (i+j) (lev_dn p') ns) ^
1.62 + (indt i) ^ "</NODE>\n"
1.63 + end
1.64 + and nds _ _ [] = ""
1.65 + | nds i p (n::ns) = (nd i p n) ^ (nds i (lev_on p) ns);
1.66 + in nds j [0] h : xml end;
1.67 +fun hierarchy_met h =
1.68 + let val j = indentation
1.69 + fun nd i p (Ptyp (id,[n as {guh,...} : met],ns)) =
1.70 + let val p' = lev_on p
1.71 + in (indt i) ^ "<NODE>\n" ^
1.72 + (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^
1.73 + (indt (i+j)) ^ "<NO> " (*on this level*) ^
1.74 + (string_of_int o last_elem) p' ^ " </NO>\n" ^
1.75 + (indt (i+j)) ^ "<CONTENTREF> " ^ guh ^
1.76 + " </CONTENTREF>\n" ^
1.77 + (nds (i+j) (lev_dn p') ns) ^
1.78 + (indt i) ^ "</NODE>\n"
1.79 + end
1.80 + and nds _ _ [] = ""
1.81 + | nds i p (n::ns) = (nd i p n) ^ (nds i (lev_on p) ns);
1.82 + in nds j [0] h : xml end;
1.83 +(* (writeln o hierarchy_pbl) (!ptyps);
1.84 + *)
1.85 +
1.86 +fun pbl_hierarchy2file (path:path) =
1.87 + str2file (path ^ "pbl_hierarchy.xml")
1.88 + ("<NODE>\n" ^
1.89 + " <ID> problem hierarchy </ID>\n" ^
1.90 + " <NO> 1 </NO>\n" ^
1.91 + " <CONTENTREF> pbl_ROOT </CONTENTREF>\n" ^
1.92 + (hierarchy_pbl (!ptyps)) ^
1.93 + "</NODE>");
1.94 +
1.95 +fun met_hierarchy2file (path:path) =
1.96 + str2file (path ^ "met_hierarchy.xml")
1.97 + ("<NODE>\n" ^
1.98 + " <ID> method hierarchy </ID>\n" ^
1.99 + " <NO> 1 </NO>\n" ^
1.100 + " <CONTENTREF> met_ROOT </CONTENTREF>\n" ^
1.101 + (hierarchy_met (!mets)) ^
1.102 + "</NODE>");
1.103 +
1.104 +
1.105 +
1.106 +(**.create the xml-files for the pbls, mets from the hierarchy.**)
1.107 +
1.108 +val i = indentation;
1.109 +
1.110 +fun pbl2term thy (pblRD:pblRD) =
1.111 + str2term ("Problem (" ^
1.112 + (get_thy o theory2domID) thy ^ "_, " ^
1.113 + (strs2str' o rev) pblRD ^ ")");
1.114 +(* term2str (pbl2term Isac.thy ["equations","univariate","normalize"]);
1.115 +val it = "Problem (Isac, [normalize, univariate, equations])" : string
1.116 +*)
1.117 +
1.118 +
1.119 +(*.format a problem in xml for presentation on the problem browser;
1.120 + new version with <KESTOREREF>s -- not used because linking
1.121 + requires elements (rls, calc, ...) to be reorganized.*)
1.122 +(*######## ATTENTION: THIS IS not THE ACTUAL VERSION ################*)
1.123 +fun pbl2xml (id:(*pblRD*)pblID) ({guh,mathauthors,init,cas,met,ppc,prls,
1.124 + thy,where_}:pbt) =
1.125 + let val thy' = theory2theory' thy
1.126 + val prls' = (#id o rep_rls) prls
1.127 + in "<NODECONTENT>\n" ^
1.128 + indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
1.129 + (((id2xml i)(* o rev*)) id) ^
1.130 + indt i ^ "<META> </META>\n" ^
1.131 + (*--------------- begin display ------------------------------*)
1.132 + indt i ^ "<HEADLINE>\n" ^
1.133 + (case cas of None => term2xml i (pbl2term thy id)
1.134 + | Some t => term2xml i t) ^ "\n" ^
1.135 + indt i ^ "</HEADLINE>\n" ^
1.136 + (*--------------- hline --------------------------------------*)
1.137 + pattern2xml i ppc where_ ^
1.138 + (*--------------- hline --------------------------------------*)
1.139 + indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n"
1.140 + (*--------------- end display --------------------------------*)
1.141 + ^
1.142 + indt i ^ "<THEORY>\n" ^
1.143 + theref2xml (i+i) thy' "Theorems" "" ^
1.144 + indt i ^ "</THEORY>\n" ^
1.145 + (case met of [] => (indt i) ^ "<METHODS> </METHODS>\n"
1.146 + | _ => (indt i) ^ "<METHODS>\n" ^
1.147 + foldl op^ ("", map (keref2xml (i+i) Met_) met) ^
1.148 + (indt i) ^ "</METHODS>\n") ^
1.149 + indt i ^ "<EVALPRECOND>\n" ^
1.150 + theref2xml (i+i) (snd (thy_containing_rls thy' prls')) "Rulesets" prls'^
1.151 + indt i ^ "</EVALPRECOND>\n" ^
1.152 + authors2xml i "MATHAUTHORS" mathauthors ^
1.153 + authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^
1.154 + "</NODECONTENT>" : xml
1.155 + end;
1.156 +
1.157 +(*.format a problem in xml for presentation on the problem browser;
1.158 + old version with 'dead' strings for rls, calc, ....*)
1.159 +(*
1.160 +val pblID = ["linear","univariate","equation"];
1.161 +val pblID = ["degree_4","polynomial","univariate","equation"];
1.162 +val pblID = rev ["tool","find_values"];
1.163 +val (id, {guh,mathauthors,init,cas,met,ppc,prls,thy,where_}:pbt) =
1.164 + (pblID, get_pbt pblID);
1.165 + *)
1.166 +fun pbl2xml (id:(*pblRD*)pblID) ({guh,mathauthors,init,cas,met,ppc,prls,
1.167 + thy,where_}:pbt) =
1.168 + "<NODECONTENT>\n" ^
1.169 + indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
1.170 + (((id2xml i)(* o rev*)) id) ^
1.171 + indt i ^ "<META> </META>\n" ^
1.172 + (*--------------- begin display ------------------------------*)
1.173 + indt i ^ "<HEADLINE>\n" ^
1.174 + (case cas of None => term2xml i (pbl2term thy id)
1.175 + | Some t => term2xml i t) ^ "\n" ^
1.176 + indt i ^ "</HEADLINE>\n" ^
1.177 + (*--------------- hline --------------------------------------*)
1.178 + pattern2xml i ppc where_ ^
1.179 + (*--------------- hline --------------------------------------*)
1.180 + indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n"
1.181 + (*--------------- end display --------------------------------*)
1.182 + ^
1.183 + indt i ^ "<THEORY>\n" ^
1.184 + theref2xml (i+i) (theory2theory' thy) "Theorems" "" ^
1.185 + indt i ^ "</THEORY>\n" ^
1.186 + (case met of [] => (indt i) ^ "<METHODS> </METHODS>\n"
1.187 + | _ => (indt i) ^ "<METHODS>\n" ^
1.188 + foldl op^ ("", map (keref2xml (i+i) Met_) met) ^
1.189 + (indt i) ^ "</METHODS>\n") ^
1.190 + indt i ^ "<EVALPRECOND> " ^ (#id o rep_rls)
1.191 + prls ^ " </EVALPRECOND>\n" ^
1.192 + authors2xml i "MATHAUTHORS" mathauthors ^
1.193 + authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^
1.194 + "</NODECONTENT>" : xml;
1.195 +(*
1.196 +val pblID = ["linear","univariate","equation"];
1.197 +val pblID = ["degree_4","polynomial","univariate","equation"];
1.198 +writeln (pbl2xml pblID (get_pbt pblID));
1.199 +*)
1.200 +
1.201 +(*replace by 'fun calc2xml' as developed for thy in 0607*)
1.202 +fun calc2xmlOLD j ((scr_op, (isa_op, _)):calc) =
1.203 + indt i ^ "<CALCULATE> (" ^ scr_op ^ ", (" ^ isa_op ^ ")) </CALCULATE>\n";
1.204 +fun calcs2xmlOLD j [] = ("":xml) (*TODO replace with 'strs2xml'*)
1.205 + | calcs2xmlOLD j (r::rs) = calc2xmlOLD j r ^ calcs2xmlOLD j rs;
1.206 +
1.207 +(* val (id, {guh,mathauthors,init,ppc,pre,scr,calc,
1.208 + crls,erls,nrls,prls,srls,rew_ord'}) =
1.209 + (["Test", "solve_linear"],
1.210 + get_met ["Test", "solve_linear"]);
1.211 + *)
1.212 +
1.213 +(*.format a method in xml for presentation on the method browser;
1.214 + new version with <KESTOREREF>s -- not used because linking
1.215 + requires elements (rls, calc, ...) to be reorganized.*)
1.216 +(*######## ATTENTION: THIS IS not THE ACTUAL VERSION ################*)
1.217 +fun met2xml (id:metID) ({guh,mathauthors,init,ppc,pre,scr,calc,
1.218 + crls,erls,nrls,prls,srls,rew_ord'}:met) =
1.219 + let val thy' = "Isac.thy" (*FIXME.WN0607 get thy from met ?!?*)
1.220 + val crls' = (#id o rep_rls) crls
1.221 + val erls' = (#id o rep_rls) erls
1.222 + val nrls' = (#id o rep_rls) nrls
1.223 + val prls' = (#id o rep_rls) prls
1.224 + val srls' = (#id o rep_rls) srls
1.225 + in "<NODECONTENT>\n" ^
1.226 + indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
1.227 + id2xml i id ^
1.228 + indt i ^ "<META> </META>\n" ^
1.229 + scr2xml i scr ^
1.230 + pattern2xml i ppc pre ^
1.231 + indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
1.232 + indt i ^ "<EVALPRECOND>\n" ^
1.233 + theref2xml (i+i) (snd (thy_containing_rls thy' prls')) "Rulesets" prls'^
1.234 + indt i ^ "</EVALPRECOND>\n" ^
1.235 + indt i ^ "<EVALCOND>\n" ^
1.236 + theref2xml (i+i) (snd (thy_containing_rls thy' erls')) "Rulesets" erls'^
1.237 + indt i ^ "</EVALCOND>\n" ^
1.238 + indt i ^ "<EVALLISTEXPR>\n"^
1.239 + theref2xml (i+i) (snd (thy_containing_rls thy' srls')) "Rulesets" srls'^
1.240 + indt i ^ "</EVALLISTEXPR>\n" ^
1.241 + indt i ^ "<CHECKELEMENTWISE>\n" ^
1.242 + theref2xml (i+i) (snd (thy_containing_rls thy' crls')) "Rulesets" crls'^
1.243 + indt i ^ "</CHECKELEMENTWISE>\n" ^
1.244 + indt i ^ "<NORMALFORM>\n" ^
1.245 + theref2xml (i+i) (snd (thy_containing_rls thy' nrls')) "Rulesets" nrls'^
1.246 + indt i ^ "</NORMALFORM>\n" ^
1.247 + indt i ^ "<REWORDER> " ^ rew_ord' ^ " </REWORDER>\n" ^
1.248 + calcs2xmlOLD i calc ^
1.249 + authors2xml i "MATHAUTHORS" mathauthors ^
1.250 + authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^
1.251 + "</NODECONTENT>" : xml
1.252 + end;
1.253 +(*.format a method in xml for presentation on the method browser;
1.254 + old version with 'dead' strings for rls, calc, ....*)
1.255 +fun met2xml (id:metID) ({guh,mathauthors,init,ppc,pre,scr,calc,
1.256 + crls,erls,nrls,prls,srls,rew_ord'}:met) =
1.257 + "<NODECONTENT>\n" ^
1.258 + indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
1.259 + id2xml i id ^
1.260 + indt i ^ "<META> </META>\n" ^
1.261 + scr2xml i scr ^
1.262 + pattern2xml i ppc pre ^
1.263 + indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
1.264 + indt i ^ "<EVALPRECOND> " ^ (#id o rep_rls) prls ^ " </EVALPRECOND>\n" ^
1.265 + indt i ^ "<EVALCOND> " ^ (#id o rep_rls) erls ^ " </EVALCOND>\n" ^
1.266 + indt i ^ "<EVALLISTEXPR> "^ (#id o rep_rls) srls ^ " </EVALLISTEXPR>\n" ^
1.267 + indt i ^ "<CHECKELEMENTWISE> " ^ (#id o rep_rls)
1.268 + crls ^ " </CHECKELEMENTWISE>\n" ^
1.269 + indt i ^ "<NORMALFORM> " ^ (#id o rep_rls) nrls ^ " </NORMALFORM>\n" ^
1.270 + indt i ^ "<REWORDER> " ^ rew_ord' ^ " </REWORDER>\n" ^
1.271 + calcs2xmlOLD i calc ^
1.272 + authors2xml i "MATHAUTHORS" mathauthors ^
1.273 + authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^
1.274 + "</NODECONTENT>" : xml;
1.275 +
1.276 +(* writeln (met2xml ["Test", "solve_linear"]
1.277 + (get_met ["Test", "solve_linear"]));
1.278 + *)
1.279 +
1.280 +(**. write pbls from hierarchy to files.**)
1.281 +
1.282 +(*.write the files using an int-key (pos') as filename.*)
1.283 +fun pbl2file (path:path) (pos:pos) (id:metID) (pbl as {guh,...}) =
1.284 + (writeln ("### pbl2file: id = " ^ strs2str id);
1.285 + ((str2file (path ^ pos2filename pos)) o (pbl2xml id)) pbl
1.286 + );
1.287 +
1.288 +(*.write the files using the guh as filename.*)
1.289 +(* *)
1.290 +fun pbl2file (path:path) (pos:pos) (id:metID) (pbl as {guh,...}) =
1.291 + (writeln ("### pbl2file: id = " ^ strs2str id ^ ", pos = " ^ pos2str pos);
1.292 + ((str2file (path ^ guh2filename guh)) o (pbl2xml id)) pbl
1.293 + );
1.294 +
1.295 +(**. write mets from hierarchy to files.**)
1.296 +
1.297 +(*.write the files using an int-key (pos') as filename.*)
1.298 +fun met2file (path:path) (pos:pos) (id:metID) met =
1.299 + (writeln ("### met2file: id = " ^ strs2str id);
1.300 + ((str2file (path ^ "met" ^ pos2filename pos)) o (met2xml id)) met);
1.301 +
1.302 +(*.write the files using the guh as filename.*)
1.303 +fun met2file (path:path) (pos:pos) (id:metID) (met as {guh,...}) =
1.304 + (writeln ("### met2file: id = " ^ strs2str id);
1.305 + ((str2file (path ^ guh2filename guh)) o (met2xml id)) met);
1.306 +
1.307 +
1.308 +(*.scan the mtree Ptyp and and print the nodes using wfn.*)
1.309 +fun node (pa:path) ids po wfn (Ptyp (id,[n],ns)) =
1.310 + let val po' = lev_on po
1.311 + in wfn pa po' (ids@[id]) n;
1.312 + nodes pa (ids@[id]) ((lev_dn po'):pos) wfn ns end
1.313 +and nodes _ _ _ _ [] = ()
1.314 + | nodes pa ids po wfn (n::ns) = (node pa ids po wfn n;
1.315 + nodes pa ids (lev_on po) wfn ns);
1.316 +
1.317 +
1.318 +fun pbls2file (p:path) = nodes p [] [0] pbl2file (!ptyps);
1.319 +fun mets2file (p:path) = nodes p [] [0] met2file (!mets);
1.320 +(*
1.321 +val path = "/home/neuper/proto2/isac/xmldata/";
1.322 +val path = "/home/neuper/tmp/";
1.323 +
1.324 +pbl_hierarchy2file (path ^ "pbl/");
1.325 +pbls2file (path ^ "pbl/");
1.326 +
1.327 +met_hierarchy2file (path ^ "met/");
1.328 +mets2file (path ^ "met/");
1.329 +
1.330 +thy_hierarchy2file (path ^ "thy/");
1.331 +thes2file (path ^ "thy/");
1.332 +*)
1.333 \ No newline at end of file