1.1 --- a/src/Tools/isac/xmlsrc/pbl-met-hierarchy.sml Tue Mar 13 15:04:27 2018 +0100
1.2 +++ b/src/Tools/isac/xmlsrc/pbl-met-hierarchy.sml Thu Mar 15 10:17:44 2018 +0100
1.3 @@ -3,13 +3,13 @@
1.4 (c) isac-team
1.5 *)
1.6
1.7 -fun file2str (path : path) (fnm : filename) =
1.8 +fun file2str (path : Celem.path) (fnm : Celem.filename) =
1.9 let
1.10 val file = TextIO.openIn (path ^ fnm)
1.11 val str = TextIO.inputAll file
1.12 in TextIO.closeIn file; str end
1.13
1.14 -fun str2file (fnm : filename) (str : string) =
1.15 +fun str2file (fnm : Celem.filename) (str : string) =
1.16 let val file = TextIO.openOut fnm
1.17 in
1.18 TextIO.output (file, str);
1.19 @@ -33,7 +33,7 @@
1.20 (*old version with pos2filename*)
1.21 fun hierarchy pm(*"pbl" | "met"*) h =
1.22 let val j = indentation
1.23 - fun nd i p (Ptyp (id,_,ns)) =
1.24 + fun nd i p (Celem.Ptyp (id,_,ns)) =
1.25 let val p' = Ctree.lev_on p
1.26 in (indt i) ^ "<NODE>\n" ^
1.27 (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^
1.28 @@ -50,7 +50,7 @@
1.29 (*.create a hierarchy with references to the guh's.*)
1.30 fun hierarchy_pbl h =
1.31 let val j = indentation
1.32 - fun nd i p (Ptyp (id,[n as {guh,...} : pbt],ns)) =
1.33 + fun nd i p (Celem.Ptyp (id,[n as {guh,...} : Celem.pbt],ns)) =
1.34 let val p' = Ctree.lev_on p
1.35 in (indt i) ^ "<NODE>\n" ^
1.36 (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^
1.37 @@ -63,10 +63,10 @@
1.38 end
1.39 and nds _ _ [] = ""
1.40 | nds i p (n::ns) = (nd i p n) ^ (nds i (Ctree.lev_on p) ns);
1.41 - in nds j [0] h : xml end;
1.42 + in nds j [0] h : Celem.xml end;
1.43 fun hierarchy_met h =
1.44 let val j = indentation
1.45 - fun nd i p (Ptyp (id,[n as {guh,...} : met],ns)) =
1.46 + fun nd i p (Celem.Ptyp (id,[n as {guh,...} : Celem.met],ns)) =
1.47 let val p' = Ctree.lev_on p
1.48 in (indt i) ^ "<NODE>\n" ^
1.49 (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^
1.50 @@ -79,11 +79,11 @@
1.51 end
1.52 and nds _ _ [] = ""
1.53 | nds i p (n::ns) = (nd i p n) ^ (nds i (Ctree.lev_on p) ns);
1.54 - in nds j [0] h : xml end;
1.55 + in nds j [0] h : Celem.xml end;
1.56 (* (writeln o hierarchy_pbl) (!ptyps);
1.57 *)
1.58
1.59 -fun pbl_hierarchy2file (path:path) =
1.60 +fun pbl_hierarchy2file (path : Celem.path) =
1.61 str2file (path ^ "pbl_hierarchy.xml")
1.62 ("<NODE>\n" ^
1.63 " <ID> problem hierarchy </ID>\n" ^
1.64 @@ -92,7 +92,7 @@
1.65 (hierarchy_pbl (get_ptyps ())) ^
1.66 "</NODE>");
1.67
1.68 -fun met_hierarchy2file (path:path) =
1.69 +fun met_hierarchy2file (path : Celem.path) =
1.70 str2file (path ^ "met_hierarchy.xml")
1.71 ("<NODE>\n" ^
1.72 " <ID> method hierarchy </ID>\n" ^
1.73 @@ -108,17 +108,17 @@
1.74 requires elements (rls, calc, ...) to be reorganized.*)
1.75 (*######## ATTENTION: THIS IS not THE ACTUAL VERSION ################*)
1.76 fun pbl2term thy (pblRD: Specify.pblRD) = (*WN120405.TODO.txt*)
1.77 - TermC.str2term ("Problem (" ^ (get_thy o theory2domID) thy ^ "', " ^ (strs2str' o rev) pblRD ^ ")");
1.78 + TermC.str2term ("Problem (" ^ (get_thy o Celem.theory2domID) thy ^ "', " ^ (strs2str' o rev) pblRD ^ ")");
1.79 (* term2str (pbl2term (Thy_Info_get_theory "Isac") ["equations","univariate","normalise"]);
1.80 val it = "Problem (Isac, [normalise, univariate, equations])" : string
1.81 *)
1.82 val i = indentation;
1.83
1.84 (* new version with <KESTOREREF>s -- not used *)
1.85 -fun pbl2xml (id:(*pblRD*)pblID) ({guh,mathauthors,init,cas,met,ppc,prls,
1.86 - thy,where_}:pbt) =
1.87 - let val thy' = theory2theory' thy
1.88 - val prls' = (#id o rep_rls) prls
1.89 +fun pbl2xml (id:(*pblRD*)Celem.pblID) ({guh,mathauthors,init,cas,met,ppc,prls,
1.90 + thy,where_}:Celem.pbt) =
1.91 + let val thy' = Celem.theory2theory' thy
1.92 + val prls' = (#id o Celem.rep_rls) prls
1.93 in "<NODECONTENT>\n" ^
1.94 indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
1.95 (((id2xml i)(* o rev*)) id) ^
1.96 @@ -139,18 +139,18 @@
1.97 indt i ^ "</THEORY>\n" ^
1.98 (case met of [] => (indt i) ^ "<METHODS> </METHODS>\n"
1.99 | _ => (indt i) ^ "<METHODS>\n" ^
1.100 - foldl op^ ("", map (keref2xml (i+i) Met_) met) ^
1.101 + foldl op ^ ("", map (keref2xml (i+i) Celem.Met_) met) ^
1.102 (indt i) ^ "</METHODS>\n") ^
1.103 indt i ^ "<EVALPRECOND>\n" ^
1.104 theref2xml (i+i) (snd (Rtools.thy_containing_rls thy' prls')) "Rulesets" prls'^
1.105 indt i ^ "</EVALPRECOND>\n" ^
1.106 authors2xml i "MATHAUTHORS" mathauthors ^
1.107 authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^
1.108 - "</NODECONTENT>" : xml
1.109 + "</NODECONTENT>" : Celem.xml
1.110 end;
1.111 (* old version with 'dead' strings for rls, calc, ....* *)
1.112 -fun pbl2xml (id:(*pblRD*)pblID) ({guh,mathauthors,init,cas,met,ppc,prls,
1.113 - thy,where_}:pbt) =
1.114 +fun pbl2xml (id:(*pblRD*)Celem.pblID) ({guh,mathauthors,init,cas,met,ppc,prls,
1.115 + thy,where_}:Celem.pbt) =
1.116 "<NODECONTENT>\n" ^
1.117 indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
1.118 (((id2xml i)(* o rev*)) id) ^
1.119 @@ -167,21 +167,21 @@
1.120 (*--------------- end display --------------------------------*)
1.121 ^
1.122 indt i ^ "<THEORY>\n" ^
1.123 - theref2xml (i+i) (theory2theory' thy) "Theorems" "" ^
1.124 + theref2xml (i+i) (Celem.theory2theory' thy) "Theorems" "" ^
1.125 indt i ^ "</THEORY>\n" ^
1.126 (case met of [] => (indt i) ^ "<METHODS> </METHODS>\n"
1.127 | _ => (indt i) ^ "<METHODS>\n" ^
1.128 - foldl op^ ("", map (keref2xml (i+i) Met_) met) ^
1.129 + foldl op^ ("", map (keref2xml (i+i) Celem.Met_) met) ^
1.130 (indt i) ^ "</METHODS>\n") ^
1.131 - indt i ^ "<EVALPRECOND> " ^ (#id o rep_rls)
1.132 + indt i ^ "<EVALPRECOND> " ^ (#id o Celem.rep_rls)
1.133 prls ^ " </EVALPRECOND>\n" ^
1.134 authors2xml i "MATHAUTHORS" mathauthors ^
1.135 authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^
1.136 - "</NODECONTENT>" : xml;
1.137 + "</NODECONTENT>" : Celem.xml;
1.138
1.139
1.140 (**. write pbls from hierarchy to files.**)
1.141 -fun pbl2file (path:path) (pos: Ctree.pos) (id:metID) (pbl as {guh,...}) =
1.142 +fun pbl2file (path: Celem.path) (pos: Ctree.pos) (id:Celem.metID) (pbl as {guh,...}) =
1.143 (writeln ("### pbl2file: id = " ^ strs2str id ^ ", pos = " ^ Ctree.pos2str pos);
1.144 ((str2file (path ^ Rtools.guh2filename guh)) o (pbl2xml id)) pbl
1.145 );
1.146 @@ -191,14 +191,14 @@
1.147 new version with <KESTOREREF>s -- not used because linking
1.148 requires elements (rls, calc, ...) to be reorganized.*)
1.149 (*######## ATTENTION: THIS IS not THE ACTUAL VERSION ################*)
1.150 -fun met2xml (id:metID) ({guh,mathauthors,init,ppc,pre,scr,calc,
1.151 - crls,erls,errpats,nrls,prls,srls,rew_ord'}:met) =
1.152 +fun met2xml (id: Celem.metID) ({guh,mathauthors,init,ppc,pre,scr,calc,
1.153 + crls,erls,errpats,nrls,prls,srls,rew_ord'}: Celem.met) =
1.154 let val thy' = "Isac" (*FIXME.WN0607 get thy from met ?!?*)
1.155 - val crls' = (#id o rep_rls) crls
1.156 - val erls' = (#id o rep_rls) erls
1.157 - val nrls' = (#id o rep_rls) nrls
1.158 - val prls' = (#id o rep_rls) prls
1.159 - val srls' = (#id o rep_rls) srls
1.160 + val crls' = (#id o Celem.rep_rls) crls
1.161 + val erls' = (#id o Celem.rep_rls) erls
1.162 + val nrls' = (#id o Celem.rep_rls) nrls
1.163 + val prls' = (#id o Celem.rep_rls) prls
1.164 + val srls' = (#id o Celem.rep_rls) srls
1.165 in "<NODECONTENT>\n" ^
1.166 indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
1.167 id2xml i id ^
1.168 @@ -225,12 +225,12 @@
1.169 calcs2xmlOLD i calc ^
1.170 authors2xml i "MATHAUTHORS" mathauthors ^
1.171 authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^
1.172 - "</NODECONTENT>" : xml
1.173 + "</NODECONTENT>" : Celem.xml
1.174 end;
1.175 (*.format a method in xml for presentation on the method browser;
1.176 old version with 'dead' strings for rls, calc, ....*)
1.177 -fun met2xml (id:metID) ({guh,mathauthors,init,ppc,pre,scr,calc,
1.178 - crls,erls,errpats,nrls,prls,srls,rew_ord'}:met) =
1.179 +fun met2xml (id: Celem.metID) ({guh,mathauthors,init,ppc,pre,scr,calc,
1.180 + crls,erls,errpats,nrls,prls,srls,rew_ord'}: Celem.met) =
1.181 "<NODECONTENT>\n" ^
1.182 indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
1.183 id2xml i id ^
1.184 @@ -238,33 +238,33 @@
1.185 scr2xml i scr ^
1.186 pattern2xml i ppc pre ^
1.187 indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
1.188 - indt i ^ "<EVALPRECOND> " ^ (#id o rep_rls) prls ^ " </EVALPRECOND>\n" ^
1.189 - indt i ^ "<EVALCOND> " ^ (#id o rep_rls) erls ^ " </EVALCOND>\n" ^
1.190 - indt i ^ "<EVALLISTEXPR> "^ (#id o rep_rls) srls ^ " </EVALLISTEXPR>\n" ^
1.191 - indt i ^ "<CHECKELEMENTWISE> " ^ (#id o rep_rls)
1.192 + indt i ^ "<EVALPRECOND> " ^ (#id o Celem.rep_rls) prls ^ " </EVALPRECOND>\n" ^
1.193 + indt i ^ "<EVALCOND> " ^ (#id o Celem.rep_rls) erls ^ " </EVALCOND>\n" ^
1.194 + indt i ^ "<EVALLISTEXPR> "^ (#id o Celem.rep_rls) srls ^ " </EVALLISTEXPR>\n" ^
1.195 + indt i ^ "<CHECKELEMENTWISE> " ^ (#id o Celem.rep_rls)
1.196 crls ^ " </CHECKELEMENTWISE>\n" ^
1.197 - indt i ^ "<NORMALFORM> " ^ (#id o rep_rls) nrls ^ " </NORMALFORM>\n" ^
1.198 + indt i ^ "<NORMALFORM> " ^ (#id o Celem.rep_rls) nrls ^ " </NORMALFORM>\n" ^
1.199 indt i ^ "<REWORDER> " ^ rew_ord' ^ " </REWORDER>\n" ^
1.200 calcs2xmlOLD i calc ^
1.201 authors2xml i "MATHAUTHORS" mathauthors ^
1.202 authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^
1.203 - "</NODECONTENT>" : xml;
1.204 + "</NODECONTENT>" : Celem.xml;
1.205 (* writeln (met2xml ["Test", "solve_linear"]
1.206 (get_met ["Test", "solve_linear"]));
1.207 *)
1.208
1.209 (*.write the files using an int-key (pos') as filename.*)
1.210 -fun met2file (path:path) (pos: Ctree.pos) (id:metID) met =
1.211 +fun met2file (path: Celem.path) (pos: Ctree.pos) (id: Celem.metID) met =
1.212 (writeln ("### met2file: id = " ^ strs2str id);
1.213 ((str2file (path ^ "met" ^ pos2filename pos)) o (met2xml id)) met);
1.214
1.215 (*.write the files using the guh as filename.*)
1.216 -fun met2file (path:path) (pos: Ctree.pos) (id:metID) (met as {guh,...}) =
1.217 +fun met2file (path: Celem.path) (pos: Ctree.pos) (id: Celem.metID) (met as {guh,...}) =
1.218 (writeln ("### met2file: id = " ^ strs2str id);
1.219 ((str2file (path ^ Rtools.guh2filename guh)) o (met2xml id)) met);
1.220
1.221 (*.scan the mtree Ptyp and print the nodes using wfn.*)
1.222 -fun node (pa:path) ids po wfn (Ptyp (id,[n],ns)) =
1.223 +fun node (pa: Celem.path) ids po wfn (Celem.Ptyp (id,[n],ns)) =
1.224 let val po' = Ctree.lev_on po
1.225 in
1.226 wfn pa po' (ids@[id]) n;
1.227 @@ -274,8 +274,8 @@
1.228 | nodes pa ids po wfn (n::ns) =
1.229 (node pa ids po wfn n; nodes pa ids (Ctree.lev_on po) wfn ns);
1.230
1.231 -fun pbls2file (p:path) = nodes p [] [0] pbl2file (get_ptyps ());
1.232 -fun mets2file (p:path) = nodes p [] [0] met2file (get_mets ());
1.233 +fun pbls2file (p: Celem.path) = nodes p [] [0] pbl2file (get_ptyps ());
1.234 +fun mets2file (p: Celem.path) = nodes p [] [0] met2file (get_mets ());
1.235 (*
1.236 val path = "/home/neuper/proto2/isac/xmldata/";
1.237 val path = "/home/neuper/tmp/";
1.238 @@ -291,11 +291,11 @@
1.239 *)
1.240
1.241 fun update_metdata
1.242 - ({guh, mathauthors, init, rew_ord', erls, srls, prls, crls, nrls, calc, ppc, pre, scr, ...}: met)
1.243 + ({guh, mathauthors, init, rew_ord', erls, srls, prls, crls, nrls, calc, ppc, pre, scr, ...}: Celem.met)
1.244 errpats' =
1.245 {guh = guh, mathauthors = mathauthors, init = init, rew_ord' = rew_ord', erls = erls,
1.246 srls = srls, prls = prls, crls = crls, nrls = nrls, calc = calc,
1.247 - ppc = ppc, pre = pre, scr = scr, errpats = errpats'}: met
1.248 + ppc = ppc, pre = pre, scr = scr, errpats = errpats'}: Celem.met
1.249
1.250 (* interface for dialog-authoring: call in Buld_Thydata.thy only ! *)
1.251 fun update_metpair thy metID errpats = let