1.1 --- a/src/sml/KI-interface.sml Thu Aug 14 08:15:41 2003 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,8 +0,0 @@
1.4 -(* interface to knowledge interpreter
1.5 - use"KI-interface.sml";
1.6 - *)
1.7 -
1.8 -(*
1.9 -fun applytac uI cI pos tac =
1.10 - let val ((pt,p), tacs) = get_calc uI cI
1.11 -*)
1.12 \ No newline at end of file
2.1 --- a/src/sml/ME/generate.sml Thu Aug 14 08:15:41 2003 +0200
2.2 +++ b/src/sml/ME/generate.sml Fri Aug 15 12:23:47 2003 +0200
2.3 @@ -120,11 +120,12 @@
2.4 | inout2str (Domain dI) = "Domain "^dI;
2.5 fun inouts2str ios = (strs2str' o (map inout2str)) ios;
2.6
2.7 -datatype mout = (* DG<--ME *)
2.8 +datatype mout =
2.9 Form' of inout (* packing cterm' | cterm' ppc *)
2.10 | Problems of inout (* passes specify (and solve) *)
2.11 | Error' of inout
2.12 | EmptyMout;
2.13 +
2.14 fun mout2str (Form' inout) ="Form' "^(inout2str inout)
2.15 | mout2str (Error' inout) ="Error' "^(inout2str inout)
2.16 | mout2str (EmptyMout ) ="EmptyMout";
3.1 --- a/src/sml/ME/sequent.sml Thu Aug 14 08:15:41 2003 +0200
3.2 +++ b/src/sml/ME/sequent.sml Fri Aug 15 12:23:47 2003 +0200
3.3 @@ -384,6 +384,55 @@
3.4 | _ => "tac2str not impl. for ?!";
3.5
3.6
3.7 +fun tac2IDstr (ma:tac) = case ma of
3.8 + Model_Problem _ => "Model_Problem"
3.9 + | Refine_Tacitly pblID => "Refine_Tacitly"
3.10 + | Refine_Problem pblID => "Refine_Problem"
3.11 + | Add_Given cterm' => "Add_Given"
3.12 + | Del_Given cterm' => "Del_Given"
3.13 + | Add_Find cterm' => "Add_Find"
3.14 + | Del_Find cterm' => "Del_Find"
3.15 + | Add_Relation cterm' => "Add_Relation"
3.16 + | Del_Relation cterm' => "Del_Relation"
3.17 +
3.18 + | Specify_Domain domID => "Specify_Domain"
3.19 + | Specify_Problem pblID => "Specify_Problem"
3.20 + | Specify_Method metID => "Specify_Method"
3.21 + | Apply_Method metID => "Apply_Method"
3.22 + | Check_Postcond pblID => "Check_Postcond"
3.23 + | Free_Solve => "Free_Solve"
3.24 +
3.25 + | Rewrite_Inst (subs,thm')=> "Rewrite_Inst"
3.26 + | Rewrite thm' => "Rewrite"
3.27 + | Rewrite_Asm thm' => "Rewrite_Asm"
3.28 + | Rewrite_Set_Inst (subs, rls) => "Rewrite_Set_Inst"
3.29 + | Rewrite_Set rls => "Rewrite_Set"
3.30 + | Detail => "Detail"
3.31 + | End_Detail => "End_Detail"
3.32 + | Detail_Set rls => "Detail_Set"
3.33 + | Detail_Set_Inst (subs, rls) => "Detail_Set_Inst"
3.34 + | Calculate op_ => "Calculate "
3.35 + | Substitute subs => "Substitute"
3.36 + | Apply_Assumption ct's => "Apply_Assumption"
3.37 +
3.38 + | Take cterm' => "Take"
3.39 + | Take_Inst cterm' => "Take_Inst"
3.40 + | Group (con, ints) => "Group"
3.41 + | Subproblem (domID, pblID) => "Subproblem"
3.42 + | End_Subproblem => "End_Subproblem"
3.43 + | CAScmd cterm' => "CAScmd"
3.44 +
3.45 + | Check_elementwise cterm'=> "Check_elementwise"
3.46 + | Or_to_List => "Or_to_List "
3.47 + | Collect_Trues => "Collect_Trues"
3.48 +
3.49 + | Empty_Tac => "Empty_Tac"
3.50 + | Tac string => "Tac "
3.51 + | User => "User"
3.52 + | End_Proof' => "End_Proof'"
3.53 + | _ => "tac2str not impl. for ?!";
3.54 +
3.55 +
3.56
3.57
3.58 (*tac_ is made from tac in applicable_in,
4.1 --- a/src/sml/ME/solve.sml Thu Aug 14 08:15:41 2003 +0200
4.2 +++ b/src/sml/ME/solve.sml Fri Aug 15 12:23:47 2003 +0200
4.3 @@ -193,7 +193,7 @@
4.4 else
4.5 let
4.6 (*resume script of parpbl, transfer value of subpbl-script*)
4.7 - val ppp = par_pblobj pt ((**)lev_up(**) p);
4.8 + val ppp = par_pblobj pt (lev_up p);
4.9 val thy' = get_obj g_domID pt ppp;
4.10 val thy = assoc_thy thy';
4.11 val metID = get_obj g_metID pt ppp;
5.1 --- a/src/sml/ROOT.ML Thu Aug 14 08:15:41 2003 +0200
5.2 +++ b/src/sml/ROOT.ML Fri Aug 15 12:23:47 2003 +0200
5.3 @@ -100,19 +100,25 @@
5.4 use"solve.sml";
5.5 cd "..";
5.6 "******* build ME complete *******";
5.7 +use"states";
5.8 cd "xmlsrc";
5.9 use"mathml.sml";
5.10 - use"pbl_met.sml";
5.11 + use"pbl-met-hierarchy.sml";
5.12 + use"interface-xml.sml";
5.13 cd "..";
5.14 -use"states";
5.15 -use"KI-interface.sml";
5.16 -
5.17 +cd"FE-interface";
5.18 + use"messages.sml";
5.19 + use"interface.sml";
5.20 + cd "..";
5.21 +(*-----------------vvv-delete!*)
5.22 use"DG-ME-states.sml";
5.23 cd "DG";
5.24 use"dialog.sml";
5.25 cd "..";
5.26 +use"stdin-out.sml";
5.27 +(*-----------------^^^-delete!*)
5.28 +
5.29 use"print_exn_G.sml";
5.30 -use"stdin-out.sml";
5.31 "******* build ME & DG complete *******";
5.32
5.33 cd "IsacKnowledge";
6.1 --- a/src/sml/states.sml Thu Aug 14 08:15:41 2003 +0200
6.2 +++ b/src/sml/states.sml Fri Aug 15 12:23:47 2003 +0200
6.3 @@ -2,9 +2,12 @@
6.4 use"states.sml";
6.5 *)
6.6
6.7 -type hide_detail = (string list * (*pblID or metID*)
6.8 - string list * (*for tacs*)
6.9 - bool) (*inherit to children*)
6.10 +type hide_detail = (pblID *
6.11 + string list * (*hide: tacs + "MODEL","SPEC","APPLY",
6.12 + detail: rls
6.13 + tacs (as strings)
6.14 + must _not_ be contained in this list*)
6.15 + bool) (*inherit to children in pbl-herarchy*)
6.16 list;
6.17 type hide = hide_detail;
6.18 type detail = hide_detail;
6.19 @@ -26,47 +29,124 @@
6.20 is_child_of ["root","univar","equation"] ["linear","univar","equation"];
6.21 val it = false : bool
6.22 *)
6.23 -(*. search all pbls if there is some tactic to hide .*)
6.24 -fun is_hiddet pblID tac ([]:hide_detail) = false
6.25 - | is_hiddet pblID tac ((pblID', tacs, inherit)::pts) =
6.26 +
6.27 +(*.what tactics have to be hidden (in model/specify these may be several).*)
6.28 +datatype hid =
6.29 + Show (**)
6.30 + | Hundef (**)
6.31 + | Htac (*a tactic has to be hidden*)
6.32 + | Hmodel (*the model of the (sub)problem has to be hidden*)
6.33 + | Hspecify (*the specification of the (sub)problem has to be hidden*)
6.34 + | Happly; (*solving the (sub)problem has to be hidden*)
6.35 +
6.36 +(*. search all pbls if there is some tactic or model/spec/calc to hide .*)
6.37 +fun is_hid pblID arg [] = Show
6.38 + | is_hid pblID arg ((pblID', strs, inherit)::pts) =
6.39 + let fun is_mem arg =
6.40 + if arg mem strs then Htac
6.41 + else if arg mem ["Add_Given","Add_Find","Add_Relation"]
6.42 + andalso "MODEL" mem strs then Hmodel
6.43 + else if arg mem ["Specify_Domain","Specify_Problem",
6.44 + "Specify_Method"]
6.45 + andalso "SPEC" mem strs then Hspecify
6.46 + else if "APPLY" mem strs then Htac
6.47 + else Hundef
6.48 + in if inherit then
6.49 + if is_child_of (pblID:pblID) pblID'
6.50 + then case is_mem arg of Hundef => is_hid pblID arg (pts:hide)
6.51 + | hid => hid
6.52 + else is_hid pblID arg pts
6.53 + else if pblID = pblID'
6.54 + then case is_mem arg of Hundef => is_hid pblID arg (pts:hide)
6.55 + | hid => hid
6.56 + else is_hid pblID arg pts
6.57 + end;
6.58 +(*val hide = [([],["Refine_Tacitly"],true),
6.59 + (["univar","equation"],["Apply_Method","Model_Problem","SPEC"],
6.60 + false)]
6.61 + :hide;
6.62 +is_hid [] "Rewrite" hide;
6.63 +val it = Show
6.64 +is_hid ["any","problem"] "Refine_Tacitly" hide;
6.65 +val it = Htac
6.66 +is_hid ["root","univar","equation"] "Apply_Method" hide;
6.67 +val it = Show
6.68 +is_hid ["univar","equation"] "Apply_Method" hide;
6.69 +val it = Htac
6.70 +is_hid ["univar","equation"] "Specify_Problem" hide;
6.71 +val it = Hspecify
6.72 +*)
6.73 +
6.74 +fun is_hide pblID (tac as (Subproblem (_,pI))) (det:detail) =
6.75 + is_hid pblID "SELF" det
6.76 + | is_hide pblID (tac as (Rewrite (thmID,_))) det =
6.77 + is_hid pblID thmID det
6.78 + | is_hide pblID (tac as (Rewrite_Inst (_,(thmID,_)))) det =
6.79 + is_hid pblID thmID det
6.80 + | is_hide pblID (tac as (Rewrite_Set rls)) det =
6.81 + is_hid pblID rls det
6.82 + | is_hide pblID (tac as (Rewrite_Set_Inst (_,rls))) det =
6.83 + is_hid pblID rls det
6.84 + | is_hide pblID tac det = is_hid pblID (tac2IDstr tac) det;
6.85 +(*val hide = [([],["Refine_Tacitly"],true),
6.86 + (["univar","equation"],["Apply_Method","Model_Problem",
6.87 + "SPEC","SELF"],
6.88 + false)]
6.89 + :hide;
6.90 +is_hide [] (Rewrite ("","")) hide;
6.91 +val it = Show
6.92 +is_hide ["any","problem"] (Refine_Tacitly []) hide;
6.93 +val it = Htac
6.94 +is_hide ["root","univar","equation"] (Apply_Method []) hide;
6.95 +val it = Show
6.96 +is_hide ["univar","equation"] (Apply_Method []) hide;
6.97 +val it = Htac
6.98 +is_hide ["univar","equation"] (Specify_Problem []) hide;
6.99 +val it = Hspecify
6.100 +is_hide ["univar","equation"] (Subproblem (e_domID,["univar","equation"]))hide;
6.101 +val it = Htac
6.102 +is_hide ["equation"] (Subproblem (e_domID,["univar","equation"]))hide;
6.103 +val it = Show
6.104 +*)
6.105 +
6.106 +
6.107 +(*. search all pbls in detail if there is some rls' to be detailed .*)
6.108 +fun is_det pblID arg [] = false
6.109 + | is_det pblID arg ((pblID', rlss, inherit)::pts) =
6.110 if inherit then
6.111 - if is_child_of pblID pblID'
6.112 - then if tac mem tacs
6.113 - then true
6.114 - else is_hiddet pblID tac pts
6.115 - else is_hiddet pblID tac pts
6.116 - else if pblID = pblID'
6.117 - then if tac mem tacs
6.118 - then true
6.119 - else is_hiddet pblID tac pts
6.120 - else is_hiddet pblID tac pts;
6.121 -(*
6.122 -val hide = [([],["Refine_Tacitly"],true),
6.123 - (["univar","equation"],["Apply_Method","Model_Problem"],false)]
6.124 - :hide;
6.125 -is_hiddet [] "Rewrite" hide;
6.126 -val it = false : bool
6.127 -is_hiddet ["any","problem"] "Refine_Tacitly" hide;
6.128 -val it = true : bool
6.129 -is_hiddet ["root","univar","equation"] "Apply_Method" hide;
6.130 -val it = false : bool
6.131 -is_hiddet ["univar","equation"] "Apply_Method" hide;
6.132 -val it = true : bool
6.133 -*)
6.134 + if is_child_of (pblID:pblID) pblID'
6.135 + then if arg mem rlss then true
6.136 + else is_det pblID arg (pts:detail)
6.137 + else is_det pblID arg pts
6.138 + else if pblID = pblID'
6.139 + then if arg mem rlss then true
6.140 + else is_det pblID arg (pts:detail)
6.141 + else is_det pblID arg pts;
6.142 +
6.143 +(*fun is_detail pblID (tac as (Subproblem (_,pI))) (det:detail) =
6.144 + is_det pblID "SELF" det*)
6.145 +fun is_detail pblID (tac as (Rewrite_Set rls)) det =
6.146 + is_det pblID rls det
6.147 + | is_detail pblID (tac as (Rewrite_Set_Inst (_,rls))) det =
6.148 + is_det pblID rls det
6.149 + | is_detail _ _ _ = false;
6.150 +
6.151
6.152 type userID = int;
6.153 type calcID = int;
6.154
6.155 type calcstate =
6.156 - ((ptree * pos') * (*the current calc-state*)
6.157 + ((ptree * pos') * (*the current calc-state
6.158 + in applytac: the result from tacs
6.159 + in nexttac: ???*)
6.160 ((tac * (*for comparison with input tac*)
6.161 - tac_) (*for ptree generation*)
6.162 + tac_ * (*for ptree generation*)
6.163 + istate) (*for ptree generation*)
6.164 list)); (*ev. several hidden steps; in REVERSE order*)
6.165 -val e_calcstate = ((EmptyPtree, e_pos'),[]):calcstate;
6.166 +val e_calcstate = ((EmptyPtree, e_pos'),
6.167 + []: (tac * tac_ * istate) list):calcstate;
6.168 type state = calcstate * (hide * detail);
6.169 -val e_state = (((EmptyPtree, e_pos'),
6.170 - []:(tac * tac_) list),
6.171 - ([]:hide,[]:detail)):state;
6.172 +val e_state = (e_calcstate, ([]:hide,[]:detail)):state;
6.173 val states = ref ([]:(userID * (calcID * state) list) list);
6.174 (*
6.175 states:= ([(3,[(1,e_state),
6.176 @@ -112,7 +192,7 @@
6.177 " " ^ (string_of_int pI) ^ " not existent");
6.178 (*
6.179 > get_cal 3 1 (!states);
6.180 -val it = EmptyPtree : ptree
6.181 +val it = (((EmptyPtree,(#,#)),[]),([],[])) : state
6.182 *)
6.183 fun get_state (uI:userID) (pI:calcID) = get_cal uI pI (!states);
6.184 fun get_calc (uI:userID) (pI:calcID) = (fst o (get_cal uI pI)) (!states);
6.185 @@ -138,11 +218,8 @@
6.186 > states:= del_assoc2 4 41 (!states);
6.187 > !states;
6.188 val it = [(3,[(#,#),(#,#),(#,#)]),(4,[(#,#)]),(1,[(#,#)])] : states
6.189 -> states:= del_assoc2 4 41 (!states);
6.190 -> !states;
6.191 -val it = [(3,[(#,#),(#,#),(#,#)]),(4,[(#,#)]),(1,[(#,#)])] : states
6.192
6.193 -> states:= del_user 3;
6.194 +> del_user 3;
6.195 > !states;
6.196 val it = [(4,[(#,#)]),(1,[(#,#)])] : states
6.197 *)
6.198 @@ -200,44 +277,51 @@
6.199 (states:= del_assoc (!states, uI));
6.200
6.201 (* -------------- test all exported funs --------------
6.202 +Compiler.Control.Print.printDepth:=8;
6.203 +states:=[];
6.204 +add_user (); add_user (); !states;
6.205 +ML> val it = 1 : userID
6.206 +ML> val it = 2 : userID
6.207 +ML> val it = [(1,[]),(2,[])]
6.208
6.209 -> states:=[];
6.210 -> add_user (); add_user (); !states;
6.211 -val it = 1 : userID
6.212 -val it = 2 : userID
6.213 -val it = [(1,[]),(2,[])]
6.214 -> add_calc 1 e_state; add_calc 1 e_state; !states;
6.215 -val it = 1 : calcID
6.216 -val it = 2 : calcID
6.217 -val it =
6.218 +val (hide,detail) = ([(["pI"],["tac"],true)]:hide,
6.219 + [(["pI"],["tac"],true)]:detail);
6.220 +add_calc 1 e_state;
6.221 +add_calc 1 (e_calcstate,(hide,detail)); !states;
6.222 +ML> val it = 1 : calcID
6.223 +ML> val it = 2 : calcID
6.224 +ML> val it =
6.225 [(1,
6.226 [(1,(((EmptyPtree,(#,#)),[]),([],[]))),
6.227 - (2,(((EmptyPtree,(#,#)),[]),([],[])))]),(2,[])]
6.228 -> val (pt,p) = (EmptyPtree,e_pos');
6.229 -> val (pt,_) = cappend_problem pt p Uistate ([],e_spec);
6.230 -> upd_calc 1 2 ((pt,p),[]); !states;
6.231 -val it =
6.232 - [(1,[(1,(((EmptyPtree,(#,#)),[]),([],[]))),(2,(((Nd #,(#,#)),[]),([],[])))]),
6.233 - (2,[])]
6.234 -> get_state 1 1; get_state 1 2;
6.235 -val it = (((EmptyPtree,([],Und)),[]),([],[])) : state
6.236 -val it =
6.237 + (2,(((EmptyPtree,(#,#)),[]),([(#,#,#)],[(#,#,#)])))]),(2,[])]
6.238 +
6.239 +val (pt,(p,p_)) = (EmptyPtree,e_pos');
6.240 +val (pt,_) = cappend_problem pt p Uistate ([],e_spec);
6.241 +upd_calc 1 2 ((pt,(p,p_)),[]); !states;
6.242 +ML> val it =
6.243 + [(1,
6.244 + [(1,(((EmptyPtree,(#,#)),[]),([],[]))),
6.245 + (2,(((Nd #,(#,#)),[]),([(#,#,#)],[(#,#,#)])))]),(2,[])]
6.246 +(* ~~~~~~~~~~~~~~~~~~~~ unchanged !!!*)
6.247 +
6.248 +get_state 1 1; get_state 1 2;
6.249 +ML> val it = (((EmptyPtree,([],Und)),[]),([],[])) : state
6.250 +ML> val it =
6.251 (((Nd
6.252 (PblObj
6.253 {branch=NoBranch,cell=[],env=(#,#,#,#),loc=(#,#),meth=[],
6.254 model={Find=#,Given=#,Relate=#,Where=#,With=#},origin=(#,#),
6.255 ostate=Incomplete,probl=[],result=(#,#),spec=(#,#,#)},[]),([],Und)),
6.256 - []),([],[]))
6.257 -> del_calc 2 1; !states;
6.258 -val it =
6.259 - [(1,[(1,(((EmptyPtree,(#,#)),[]),([],[]))),(2,(((Nd #,(#,#)),[]),([],[])))]),
6.260 - (2,[])]
6.261 -> del_calc 1 2; !states;
6.262 -val it = [(1,[(1,(((EmptyPtree,(#,#)),[]),([],[])))]),(2,[])]
6.263 -> del_user 1; !states;
6.264 -val it = [(2,[])]
6.265 -> add_user (); add_user (); !states;
6.266 -val it = 1 : userID
6.267 -val it = 3 : userID
6.268 -val it = [(2,[]),(1,[]),(3,[])]
6.269 + []),([(["pI"],["tac"],true)],[(["pI"],["tac"],true)])) : state
6.270 +
6.271 +del_calc 2 1 (*non existent - NO msg!*); del_calc 1 2; !states;
6.272 +ML> val it = [(1,[(1,(((EmptyPtree,(#,#)),[]),([],[])))]),(2,[])]
6.273 +
6.274 +del_user 1; !states;
6.275 +ML> val it = [(2,[])]
6.276 +
6.277 +add_user (); add_user (); !states;
6.278 +ML> val it = 1 : userID
6.279 +ML> val it = 3 : userID
6.280 +ML> val it = [(2,[]),(1,[]),(3,[])]
6.281 *)
6.282 \ No newline at end of file
7.1 --- a/src/sml/systest/script.sml Thu Aug 14 08:15:41 2003 +0200
7.2 +++ b/src/sml/systest/script.sml Fri Aug 15 12:23:47 2003 +0200
7.3 @@ -69,7 +69,7 @@
7.4 val ags = map (term_of o the o (parse DiffApp.thy))
7.5 ["A::real", "alpha::real",
7.6 "[A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]"];
7.7 -val ll = []:loc_;
7.8 +val ll = [](*:loc_*);
7.9 (* problem with exn PTREE + eval_to -------------------------
7.10 "-------------- subproblem with empty formalizaton -------";
7.11 val (mI1,m1) =
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/src/sml/xmlsrc/interface-xml.sml Fri Aug 15 12:23:47 2003 +0200
8.3 @@ -0,0 +1,62 @@
8.4 +(* use"xmlsrc/interface-xml.sml";;
8.5 + *)
8.6 +
8.7 +val i = indentation;
8.8 +
8.9 +(*. applytac .*)
8.10 +fun applytacOK2xml (uI:userID) (cI:calcID) =
8.11 + writeln ("@@@@@begin@@@@@\n "^string_of_int uI^" \n\
8.12 + \<APPLYTAC>\n\
8.13 + \ <USERID> "^string_of_int uI^" </USERID>\n\
8.14 + \ <CALCID> "^string_of_int cI^" </CALCID>\n\
8.15 + \ <SYS> calc-tree successfully updated </SYS>\n\
8.16 + \</APPLYTAC>\n\
8.17 + \@@@@@end@@@@@");
8.18 +fun applytacERROR2xml (uI:userID) (cI:calcID) e =
8.19 + writeln ("@@@@@begin@@@@@\n "^string_of_int uI^" \n\
8.20 + \<APPLYTAC>\n\
8.21 + \ <USERID> "^string_of_int uI^" </USERID>\n\
8.22 + \ <CALCID> "^string_of_int cI^" </CALCID>\n\
8.23 + \ <MESSAGE> "^e^" </MESSAGE>\n\
8.24 + \</APPLYTAC>");
8.25 +
8.26 +(*. nexttac .*)
8.27 +fun thmstr2xml j str = ((((term2xml j) o str2term) str)^"\n"):xml;
8.28 +
8.29 +fun thm'2xml j ((ID, form):thm') =
8.30 + (indt j ^"<THEOREM>\n"^
8.31 + indt (j+i) ^"<ID> "^ID^" </ID>\n"^
8.32 + indt (j+i) ^"<FORMULA>\n"^
8.33 + thmstr2xml (j+i) form^
8.34 + indt (j+i) ^"</FORMULA>\n"^
8.35 + indt j ^"</THEOREM>\n"):xml;
8.36 +
8.37 +fun tac2xml j (Rewrite thm') =
8.38 + (indt j ^"<TACTIC>\n"^
8.39 + indt (j+i) ^"<REWRITE>\n"^
8.40 + thm'2xml (j+2*i) thm'^
8.41 + indt (j+i) ^"</REWRITE>\n"^
8.42 + indt j ^"</TACTIC>\n"):xml
8.43 + | tac2xml j tac = raise error ("tac2xml: not impl. for "^tac2str tac);
8.44 +
8.45 +fun nexttacOK2xml (uI:userID) (cI:calcID) tac =
8.46 + writeln ("@@@@@begin@@@@@\n "^string_of_int uI^" \n\
8.47 + \<NEXTTAC>\n\
8.48 + \ <USERID> "^string_of_int uI^" </USERID>\n\
8.49 + \ <CALCID> "^string_of_int cI^" </CALCID>\n"^
8.50 + tac2xml i tac^
8.51 +(* ^(strs2xml o (map (tac2xml i))) tacs^*)
8.52 + "</NEXTTAC>\n\
8.53 + \@@@@@end@@@@@");
8.54 +(* nexttacOK2xml 11 22 (Rewrite ("rmult_commute", "?m * ?n = ?n * ?m"));
8.55 + *)
8.56 +
8.57 +
8.58 +
8.59 +fun nexttacERROR2xml (uI:userID) (cI:calcID) =
8.60 + writeln ("@@@@@begin@@@@@\n "^string_of_int uI^" \n\
8.61 + \<NEXTTAC>\n\
8.62 + \ <USERID> "^string_of_int uI^" </USERID>\n\
8.63 + \ <CALCID> "^string_of_int cI^" </CALCID>\n\
8.64 + \ <MESSAGE> 2020 </MESSAGE>\n\
8.65 + \</NEXTTAC>");
9.1 --- a/src/sml/xmlsrc/mathml.sml Thu Aug 14 08:15:41 2003 +0200
9.2 +++ b/src/sml/xmlsrc/mathml.sml Fri Aug 15 12:23:47 2003 +0200
9.3 @@ -2,13 +2,19 @@
9.4
9.5 *)
9.6
9.7 +type xml = string;
9.8 +fun strs2xml strs = foldl (op ^) ("", strs);
9.9 +(* writeln (strs2xml ["<XXX> xxx </XXX>\n","<YYY> yyy </YYY>\n"]);
9.10 +<XXX> xxx </XXX>
9.11 +<YYY> yyy </YYY>*)
9.12 +
9.13 val indentation = 2;
9.14 val i = indentation;
9.15
9.16 fun term2xml j t =
9.17 indt (j+i) ^ "<MATHML>\n" ^
9.18 indt (j+2*i) ^ "<ISA> " ^ term2str t ^ " </ISA>\n" ^
9.19 - indt (j+i) ^ "</MATHML>\n";
9.20 + indt (j+i) ^ "</MATHML>";
9.21 (*val t = str2term "equality e_";
9.22 writeln (term2xml 8 t);
9.23 <MATHML>
10.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
10.2 +++ b/src/sml/xmlsrc/pbl-met-hierarchy.sml Fri Aug 15 12:23:47 2003 +0200
10.3 @@ -0,0 +1,147 @@
10.4 +(* use"pbl_met.sml";
10.5 + use"xmlsrc/pbl-met-hierarchy.sml";
10.6 + use"../xmlsrc/pbl-met-hierarchy.sml";
10.7 + *)
10.8 +
10.9 +type path = string;
10.10 +type filename = string;
10.11 +
10.12 +fun str2file (fnm:filename) (str:string) =
10.13 + let val file = TextIO.openOut fnm
10.14 + in (TextIO.output (file, str);
10.15 + TextIO.flushOut file;
10.16 + TextIO.closeOut file) end;
10.17 +fun pos2filename [] = raise error "pos2filename called with []"
10.18 + | pos2filename [i] = "_" ^ string_of_int i ^ ".xml"
10.19 + | pos2filename (i::is) = "_" ^ string_of_int i ^ pos2filename is;
10.20 +(* pos2filename [1,22,3];
10.21 +val it = "_1_22_3.xml" : string
10.22 +*)
10.23 +fun id2filename [] = raise error "id2filename called with []"
10.24 + | id2filename [s] = s ^ ".xml"
10.25 + | id2filename (s::ss) = s ^ "_" ^ id2filename ss;
10.26 +(* id2filename ["linear","univariate","equation"];
10.27 +val it = "linear_univariate_equation.xml" : string
10.28 +*)
10.29 +fun id2xml i ids =
10.30 + let fun id2x _ [] = ""
10.31 + | id2x i (s::ss) = (indt i) ^ "<ID> " ^ s ^ " </ID>\n" ^
10.32 + (id2x i ss)
10.33 + in (indt i) ^ "<KEY>\n" ^
10.34 + (id2x (i + indentation) ids) ^
10.35 + (indt i) ^ "</KEY>\n" end;
10.36 +(* writeln(id2xml 8 ["linear","univariate","equation"]);
10.37 + <KEY>
10.38 + <ID>linear</ID>
10.39 + <ID>univariate</ID>
10.40 + <ID>equation</ID>
10.41 + </KEY>*)
10.42 +
10.43 +
10.44 +
10.45 +(*ad DTD: a NODE contains an ID and zero or more NODEs*)
10.46 +fun hierarchy pm(*"pbl" | "met"*) h =
10.47 + let val j = indentation
10.48 + fun nd i p (Ptyp (id,_,ns)) =
10.49 + let val p' = lev_on p
10.50 + in
10.51 + (indt i) ^ "<NODE>\n" ^
10.52 + (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^
10.53 + (indt (i+j)) ^
10.54 + "<CONTENTREF> " ^ pm ^ pos2filename p' ^
10.55 + " </CONTENTREF>\n" ^
10.56 + (nds (i+j) (lev_dn p') ns) ^
10.57 + (indt i) ^ "</NODE>\n"
10.58 + end
10.59 + and nds _ _ [] = ""
10.60 + | nds i p (n::ns) = (nd i p n) ^ (nds i (lev_on p) ns);
10.61 + in nds 0 [0] h end;
10.62 +(* (writeln o hierarchy) (!ptyps);
10.63 + *)
10.64 +
10.65 +fun pbl_hierarchy2file (path:path) =
10.66 + str2file (path ^ "pbl_hierarchy.xml") (hierarchy "pbl" (!ptyps));
10.67 +fun met_hierarchy2file (path:path) =
10.68 + str2file (path ^ "met_hierarchy.xml") (hierarchy "met" (!mets));
10.69 +(* pbl_hierarchy2file "../xml/pbl/";
10.70 + met_hierarchy2file "../xml/met/";
10.71 + *)
10.72 +
10.73 +
10.74 +val i = indentation;
10.75 +
10.76 +fun filtermodel str =
10.77 + let fun filt [] = []
10.78 + | filt ((s, (t1, t2)) :: ps) =
10.79 + if str = s then (t1 $ t2) :: filt ps else filt ps
10.80 + in filt end;
10.81 +
10.82 +fun model2xml j p where_ =
10.83 + (case filtermodel "#Given" p of
10.84 + [] => (indt j) ^ "<GIVEN> </GIVEN>\n"
10.85 + | gis => (indt j) ^ "<GIVEN>\n" ^ terms2xml j gis ^
10.86 + (indt j) ^ "</GIVEN>\n")
10.87 + ^
10.88 + (case where_ of
10.89 + [] => (indt j) ^ "<WHERE> </WHERE>\n"
10.90 + | whs => (indt j) ^ "<WHERE>\n" ^ terms2xml j whs ^
10.91 + (indt j) ^ "</WHERE>\n")
10.92 + ^
10.93 + (case filtermodel "#Find" p of
10.94 + [] => (indt j) ^ "<FIND> </FIND>\n"
10.95 + | fis => (indt j) ^ "<FIND>\n" ^ terms2xml j fis ^
10.96 + (indt j) ^ "</FIND>\n")
10.97 + ^
10.98 + (case filtermodel "#Relate" p of
10.99 + [] => (indt j) ^ "<RELATE> </RELATE>\n"
10.100 + | res => (indt j) ^ "<RELATE>\n" ^ terms2xml j res ^
10.101 + (indt j) ^ "</RELATE>\n");
10.102 +
10.103 +fun pbl2xml (id:pblRD) ({cas,met,ppc,prls,thy,where_}:pbt) =
10.104 + "<NODECONTENT>\n"
10.105 + ^
10.106 + (((id2xml i) o rev) id)
10.107 + ^
10.108 + model2xml i ppc where_
10.109 + ^
10.110 + (indt i) ^ "<THEORY> " ^ theory2theory' thy ^ " </THEORY>\n"
10.111 + ^
10.112 + (case met of [] => (indt i) ^ "<METHODS> </METHODS>\n"
10.113 + | _ => (indt i) ^ "<METHODS>\n" ^
10.114 + foldl op^ ("", map (id2xml (i+i)) met) ^
10.115 + (indt i) ^ "</METHODS>\n")
10.116 + ^
10.117 + (case cas of None => (indt i) ^ "<CAS> </CAS>\n"
10.118 + | Some t => (indt i) ^ "<CAS>\n" ^ term2xml i t ^ "\n" ^
10.119 + (indt i) ^ "</CAS>\n")
10.120 + ^
10.121 + (indt i) ^ "<EVAL_PRECOND> " ^ (#id o rep_rls) prls ^ " </EVAL_PRECOND>\n"
10.122 + ^
10.123 + "</NODECONTENT>";
10.124 +fun met2xml (id:metID) m =
10.125 + "<NODECONTENT>\n" ^
10.126 + (id2xml i) id ^
10.127 + indt i ^ "met2xml not impl.\n" ^
10.128 + "</NODECONTENT>";
10.129 +
10.130 +fun pbl2file path (pos:pos) id pbl =
10.131 + (writeln ("### pbl2file: id = " ^ strs2str id);
10.132 + ((str2file (path ^ "pbl" ^ pos2filename pos)) o (pbl2xml id)) pbl
10.133 + );
10.134 +fun met2file path (pos:pos) id met =
10.135 + ((str2file (path ^ "met" ^ pos2filename pos)) o (met2xml id)) met;
10.136 +
10.137 +fun nd (pa:path) ids po wfn (Ptyp (id,[n],ns)) =
10.138 + let val po' = lev_on po
10.139 + in wfn pa po' (ids@[id]) n;
10.140 + nds pa (ids@[id]) ((lev_dn po'):pos) wfn ns end
10.141 +and nds _ _ _ _ [] = ()
10.142 + | nds pa ids po wfn (n::ns) = (nd pa ids po wfn n;
10.143 + nds pa ids (lev_on po) wfn ns);
10.144 +
10.145 +
10.146 +fun pbls2file (p:path) = nds p [] [0] pbl2file (!ptyps);
10.147 +fun mets2file (p:path) = nds p [] [0] met2file (!mets);
10.148 +(* pbls2file "../xml/pbl/";
10.149 + mets2file "../xml/met/";
10.150 + *)
10.151 \ No newline at end of file
11.1 --- a/src/sml/xmlsrc/pbl_met.sml Thu Aug 14 08:15:41 2003 +0200
11.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
11.3 @@ -1,147 +0,0 @@
11.4 -(* use"pbl_met.sml";
11.5 - use"xmlsrc/pbl_met.sml";
11.6 - use"../xmlsrc/pbl_met.sml";
11.7 - *)
11.8 -
11.9 -type path = string;
11.10 -type filename = string;
11.11 -
11.12 -fun str2file (fnm:filename) (str:string) =
11.13 - let val file = TextIO.openOut fnm
11.14 - in (TextIO.output (file, str);
11.15 - TextIO.flushOut file;
11.16 - TextIO.closeOut file) end;
11.17 -fun pos2filename [] = raise error "pos2filename called with []"
11.18 - | pos2filename [i] = "_" ^ string_of_int i ^ ".xml"
11.19 - | pos2filename (i::is) = "_" ^ string_of_int i ^ pos2filename is;
11.20 -(* pos2filename [1,22,3];
11.21 -val it = "_1_22_3.xml" : string
11.22 -*)
11.23 -fun id2filename [] = raise error "id2filename called with []"
11.24 - | id2filename [s] = s ^ ".xml"
11.25 - | id2filename (s::ss) = s ^ "_" ^ id2filename ss;
11.26 -(* id2filename ["linear","univariate","equation"];
11.27 -val it = "linear_univariate_equation.xml" : string
11.28 -*)
11.29 -fun id2xml i ids =
11.30 - let fun id2x _ [] = ""
11.31 - | id2x i (s::ss) = (indt i) ^ "<ID> " ^ s ^ " </ID>\n" ^
11.32 - (id2x i ss)
11.33 - in (indt i) ^ "<KEY>\n" ^
11.34 - (id2x (i + indentation) ids) ^
11.35 - (indt i) ^ "</KEY>\n" end;
11.36 -(* writeln(id2xml 8 ["linear","univariate","equation"]);
11.37 - <KEY>
11.38 - <ID>linear</ID>
11.39 - <ID>univariate</ID>
11.40 - <ID>equation</ID>
11.41 - </KEY>*)
11.42 -
11.43 -
11.44 -
11.45 -(*ad DTD: a NODE contains an ID and zero or more NODEs*)
11.46 -fun hierarchy pm(*"pbl" | "met"*) h =
11.47 - let val j = indentation
11.48 - fun nd i p (Ptyp (id,_,ns)) =
11.49 - let val p' = lev_on p
11.50 - in
11.51 - (indt i) ^ "<NODE>\n" ^
11.52 - (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^
11.53 - (indt (i+j)) ^
11.54 - "<CONTENTREF> " ^ pm ^ pos2filename p' ^
11.55 - " </CONTENTREF>\n" ^
11.56 - (nds (i+j) (lev_dn p') ns) ^
11.57 - (indt i) ^ "</NODE>\n"
11.58 - end
11.59 - and nds _ _ [] = ""
11.60 - | nds i p (n::ns) = (nd i p n) ^ (nds i (lev_on p) ns);
11.61 - in nds 0 [0] h end;
11.62 -(* (writeln o hierarchy) (!ptyps);
11.63 - *)
11.64 -
11.65 -fun pbl_hierarchy2file (path:path) =
11.66 - str2file (path ^ "pbl_hierarchy.xml") (hierarchy "pbl" (!ptyps));
11.67 -fun met_hierarchy2file (path:path) =
11.68 - str2file (path ^ "met_hierarchy.xml") (hierarchy "met" (!mets));
11.69 -(* pbl_hierarchy2file "../xml/pbl/";
11.70 - met_hierarchy2file "../xml/met/";
11.71 - *)
11.72 -
11.73 -
11.74 -val i = indentation;
11.75 -
11.76 -fun filterppc str =
11.77 - let fun filt [] = []
11.78 - | filt ((s, (t1, t2)) :: ps) =
11.79 - if str = s then (t1 $ t2) :: filt ps else filt ps
11.80 - in filt end;
11.81 -
11.82 -fun ppc2xml j p where_ =
11.83 - (case filterppc "#Given" p of
11.84 - [] => (indt j) ^ "<GIVEN> </GIVEN>\n"
11.85 - | gis => (indt j) ^ "<GIVEN>\n" ^ terms2xml j gis ^
11.86 - (indt j) ^ "</GIVEN>\n")
11.87 - ^
11.88 - (case where_ of
11.89 - [] => (indt j) ^ "<WHERE> </WHERE>\n"
11.90 - | whs => (indt j) ^ "<WHERE>\n" ^ terms2xml j whs ^
11.91 - (indt j) ^ "</WHERE>\n")
11.92 - ^
11.93 - (case filterppc "#Find" p of
11.94 - [] => (indt j) ^ "<FIND> </FIND>\n"
11.95 - | fis => (indt j) ^ "<FIND>\n" ^ terms2xml j fis ^
11.96 - (indt j) ^ "</FIND>\n")
11.97 - ^
11.98 - (case filterppc "#Relate" p of
11.99 - [] => (indt j) ^ "<RELATE> </RELATE>\n"
11.100 - | res => (indt j) ^ "<RELATE>\n" ^ terms2xml j res ^
11.101 - (indt j) ^ "</RELATE>\n");
11.102 -
11.103 -fun pbl2xml (id:pblRD) ({cas,met,ppc,prls,thy,where_}:pbt) =
11.104 - "<NODECONTENT>\n"
11.105 - ^
11.106 - (((id2xml i) o rev) id)
11.107 - ^
11.108 - ppc2xml i ppc where_
11.109 - ^
11.110 - (indt i) ^ "<THEORY> " ^ theory2theory' thy ^ " </THEORY>\n"
11.111 - ^
11.112 - (case met of [] => (indt i) ^ "<METHODS> </METHODS>\n"
11.113 - | _ => (indt i) ^ "<METHODS>\n" ^
11.114 - foldl op^ ("", map (id2xml (i+i)) met) ^
11.115 - (indt i) ^ "</METHODS>\n")
11.116 - ^
11.117 - (case cas of None => (indt i) ^ "<CAS> </CAS>\n"
11.118 - | Some t => (indt i) ^ "<CAS>\n" ^ term2xml i t ^ "\n" ^
11.119 - (indt i) ^ "</CAS>\n")
11.120 - ^
11.121 - (indt i) ^ "<EVAL_PRECOND> " ^ (#id o rep_rls) prls ^ " </EVAL_PRECOND>\n"
11.122 - ^
11.123 - "</NODECONTENT>";
11.124 -fun met2xml (id:metID) m =
11.125 - "<NODECONTENT>\n" ^
11.126 - (id2xml i) id ^
11.127 - indt i ^ "met2xml not impl.\n" ^
11.128 - "</NODECONTENT>";
11.129 -
11.130 -fun pbl2file path (pos:pos) id pbl =
11.131 - (writeln ("### pbl2file: id = " ^ strs2str id);
11.132 - ((str2file (path ^ "pbl" ^ pos2filename pos)) o (pbl2xml id)) pbl
11.133 - );
11.134 -fun met2file path (pos:pos) id met =
11.135 - ((str2file (path ^ "met" ^ pos2filename pos)) o (met2xml id)) met;
11.136 -
11.137 -fun nd (pa:path) ids po wfn (Ptyp (id,[n],ns)) =
11.138 - let val po' = lev_on po
11.139 - in wfn pa po' (ids@[id]) n;
11.140 - nds pa (ids@[id]) ((lev_dn po'):pos) wfn ns end
11.141 -and nds _ _ _ _ [] = ()
11.142 - | nds pa ids po wfn (n::ns) = (nd pa ids po wfn n;
11.143 - nds pa ids (lev_on po) wfn ns);
11.144 -
11.145 -
11.146 -fun pbls2file (p:path) = nds p [] [0] pbl2file (!ptyps);
11.147 -fun mets2file (p:path) = nds p [] [0] met2file (!mets);
11.148 -(* pbls2file "../xml/pbl/";
11.149 - mets2file "../xml/met/";
11.150 - *)
11.151 \ No newline at end of file