1.1 --- a/src/Tools/isac/Frontend/interface.sml Sun Jul 29 16:29:04 2012 +0200
1.2 +++ b/src/Tools/isac/Frontend/interface.sml Mon Jul 30 16:41:08 2012 +0200
1.3 @@ -782,10 +782,7 @@
1.4 val ((pt, _), _) = get_calc cI
1.5 val pos = get_pos cI 1;
1.6 val fillpats = find_fillpatterns (pt, pos) errpatID
1.7 - val args = "fill patterns " ^
1.8 - ((map ((apsnd term2str) o quad2pair) fillpats) |> map pair2str_ |> strs2str_)
1.9 - (* the format for the message's arguments is waiting for generalisation of CalcMessage *)
1.10 - in calcMessage2xml cI ("fill patterns " ^ args) end;
1.11 + in findFillpatterns2xml cI (map #1 fillpats) end;
1.12
1.13 (* given a fillpatID propose a fillform to the learner on the worksheet;
1.14 the "ctree" is extended with fillpat and "ostate Inconsistent",
2.1 --- a/src/Tools/isac/xmlsrc/interface-xml.sml Sun Jul 29 16:29:04 2012 +0200
2.2 +++ b/src/Tools/isac/xmlsrc/interface-xml.sml Mon Jul 30 16:41:08 2012 +0200
2.3 @@ -12,10 +12,7 @@
2.4 "@@@@@begin@@@@@\n "^string_of_int uI
2.5 # omit the distinctions APPENDFORMULA, REPLACEFORMULA, ...
2.6 WN071004 these 2 simplifications are begun with CALCMESSAGE
2.7 -
2.8 - use"xmlsrc/interface-xml.sml";
2.9 - use"interface-xml.sml";
2.10 - *)
2.11 +*)
2.12
2.13 type iterID = int;
2.14 type calcID = int;
2.15 @@ -260,16 +257,14 @@
2.16 "</SETNEXTTACTIC>\n" ^
2.17 "@@@@@end@@@@@");
2.18
2.19 -fun fetchproposedtacticOK2xml (*uI:userID*) (cI:calcID) tac =
2.20 +fun fetchproposedtacticOK2xml (cI:calcID) tac =
2.21 writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
2.22 "<NEXTTAC>\n" ^
2.23 " <CALCID> "^string_of_int cI^" </CALCID>\n"^
2.24 tac2xml i tac^
2.25 -(* ^(strs2xml o (map (tac2xml i))) tacs^*)
2.26 "</NEXTTAC>\n" ^
2.27 "@@@@@end@@@@@");
2.28 -(* fetchproposedtactic2xml 11 22 (Rewrite ("rmult_commute","?m *?n =?n *?m"));
2.29 - *)
2.30 +
2.31 fun fetchproposedtacticERROR2xml (*uI:userID*) (cI:calcID) e =
2.32 writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
2.33 "<NEXTTAC>\n" ^
2.34 @@ -340,8 +335,16 @@
2.35 contthy2xml i contthy ^
2.36 "</CONTEXTTHY>\n" ^
2.37 "@@@@@end@@@@@");
2.38 -
2.39 (*
2.40 fun contextthyNO2xml guh =
2.41 writeln (datatypes.contextthyNO2xml 0 guh);
2.42 *)
2.43 +
2.44 +fun findFillpatterns2xml (cI:calcID) pattIDs =
2.45 + writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
2.46 + "<FINDFILLPATTERNS>\n" ^
2.47 + " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
2.48 + id2xml 3 pattIDs ^
2.49 + "</FINDFILLPATTERNS>\n" ^
2.50 + "@@@@@end@@@@@");
2.51 +
3.1 --- a/test/Tools/isac/Frontend/interface.sml Sun Jul 29 16:29:04 2012 +0200
3.2 +++ b/test/Tools/isac/Frontend/interface.sml Mon Jul 30 16:41:08 2012 +0200
3.3 @@ -49,8 +49,8 @@
3.4 "--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
3.5 "--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
3.6 "--------- UC errpat, fillpat by input ---------------------------";
3.7 -"--------- UC errpat, fillpat step to at Rewrite -----------------";
3.8 -"--------- UC errpat, fillpat step to at Rewrite_Set -------------";
3.9 +"--------- UC errpat, fillpat step to Rewrite --------------------";
3.10 +"--------- UC errpat, fillpat step to Rewrite_Set ----------------";
3.11 "--------------------------------------------------------";
3.12
3.13 "within struct ---------------------------------------------------";
3.14 @@ -1341,9 +1341,8 @@
3.15 error "FE-interface.sml: diff.behav. in FORMULA:replace} NOTok";
3.16 DEconstrCalcTree 1;
3.17
3.18 -"--------- UC errpat, fillpat ------------------------------------";
3.19 -"--------- UC errpat, fillpat ------------------------------------";
3.20 -"--------- UC errpat, fillpat ------------------------------------";
3.21 +"--------- UC errpat, fillpat by input ---------------------------";
3.22 +"--------- UC errpat, fillpat by input ---------------------------";
3.23 "--------- UC errpat, fillpat by input ---------------------------";
3.24 states := [];
3.25 CalcTree
3.26 @@ -1420,9 +1419,9 @@
3.27 (([5], Res), 2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3),
3.28 (([], Res), 2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3)] *)
3.29
3.30 -"--------- UC errpat, fillpat step to at Rewrite -----------------";
3.31 -"--------- UC errpat, fillpat step to at Rewrite -----------------";
3.32 -"--------- UC errpat, fillpat step to at Rewrite -----------------";
3.33 +"--------- UC errpat, fillpat step to Rewrite --------------------";
3.34 +"--------- UC errpat, fillpat step to Rewrite --------------------";
3.35 +"--------- UC errpat, fillpat step to Rewrite --------------------";
3.36 (*TODO*)
3.37 states:=[];
3.38 CalcTree
3.39 @@ -1435,9 +1434,9 @@
3.40 autoCalculate 1 CompleteCalc;
3.41 val ((pt,p),_) = get_calc 1; show_pt pt;
3.42
3.43 -"--------- UC errpat, fillpat step to at Rewrite_Set -------------";
3.44 -"--------- UC errpat, fillpat step to at Rewrite_Set -------------";
3.45 -"--------- UC errpat, fillpat step to at Rewrite_Set -------------";
3.46 +"--------- UC errpat, fillpat step to Rewrite_Set ----------------";
3.47 +"--------- UC errpat, fillpat step to Rewrite_Set ----------------";
3.48 +"--------- UC errpat, fillpat step to Rewrite_Set ----------------";
3.49 (*TODO*)
3.50 states:=[];
3.51 CalcTree
4.1 --- a/test/Tools/isac/Interpret/generate.sml Sun Jul 29 16:29:04 2012 +0200
4.2 +++ b/test/Tools/isac/Interpret/generate.sml Mon Jul 30 16:41:08 2012 +0200
4.3 @@ -78,8 +78,9 @@
4.4 if p = ([2], Res) andalso
4.5 get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", "")) andalso
4.6 term2str f =
4.7 - "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos ?_dummy_2 * d_d x ?_dummy_3"
4.8 + "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos ?u * d_d x ?_dummy_2"
4.9 + (*WAS with old findFillpatterns:
4.10 + "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos ?_dummy_2 * d_d x ?_dummy_3"*)
4.11 then () else error "";
4.12
4.13 show_pt pt; (*ATTENTION: omits the last step, if pt is incomplete, ([2], Res) EXISTS !*)
4.14 -
5.1 --- a/test/Tools/isac/Interpret/inform.sml Sun Jul 29 16:29:04 2012 +0200
5.2 +++ b/test/Tools/isac/Interpret/inform.sml Mon Jul 30 16:41:08 2012 +0200
5.3 @@ -1016,9 +1016,10 @@
5.4 "~~~~~ to findFillpatterns return val:"; val (fillpats) =
5.5 (map (get_fillpats (subs_opt, subst) f_curr errpatID) errpatthms |> flat) (*only from "hd errpatthms"*);
5.6
5.7 +"vvv--- dropped this code WN120730";
5.8 val msg = "fill patterns " ^
5.9 ((map ((apsnd term2str) o quad2pair) fillpats) |> map pair2str_ |> strs2str_);
5.10 -if msg =
5.11 +msg =
5.12 "fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" ^
5.13 " =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1" ^
5.14 "#fill-both-args#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" ^
5.15 @@ -1027,8 +1028,13 @@
5.16 " =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * ?_dummy_1 x (x ^^^ 4)" ^
5.17 "#fill-inner-deriv#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" ^
5.18 " =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * ?_dummy_1" ^
5.19 - "#fill-all#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) = d_d x (x ^^^ 2) + ?_dummy_1#"
5.20 -then () else error "find_fillpatterns changed 4";
5.21 + "#fill-all#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) = d_d x (x ^^^ 2) + ?_dummy_1#";
5.22 +"^^^--- dropped this code WN120730";
5.23 +
5.24 +if (map #1 fillpats) =
5.25 + ["fill-d_d-arg", "fill-both-args", "fill-d_d", "fill-inner-deriv", "fill-all"]
5.26 +then () else error "find_fillpatterns changed 4b";
5.27 +
5.28
5.29 "--------- build fun is_exactly_equal, inputFillFormula ----------";
5.30 "--------- build fun is_exactly_equal, inputFillFormula ----------";
6.1 --- a/test/Tools/isac/Test_Some.thy Sun Jul 29 16:29:04 2012 +0200
6.2 +++ b/test/Tools/isac/Test_Some.thy Mon Jul 30 16:41:08 2012 +0200
6.3 @@ -1,7 +1,7 @@
6.4
6.5 theory Test_Some imports Isac begin
6.6
6.7 -use"../../../test/Tools/isac/Knowledge/diff.sml"
6.8 +use"../../../test/Tools/isac/Interpret/generate.sml"
6.9
6.10 ML {*
6.11 val thy = @{theory "Isac"};
6.12 @@ -12,75 +12,30 @@
6.13 ML {*
6.14 *}
6.15 ML {* (*==================*)
6.16 -@{thm times_divide_times_eq} (* "?x / ?y * (?z / ?w) = ?x * ?z / (?y * ?w)" *);
6.17 -@{thm rat_mult} (* "?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)" *);
6.18
6.19 *}
6.20 ML {*
6.21 *}
6.22 -
6.23 -find_theorems "(_ / _) * (_ / _)= _"
6.24 -
6.25 ML {*
6.26 -val fillpats = [
6.27 - ("fill-cancel-right-num",
6.28 - parse_patt @{theory Rational} "(?a * ?b) / (?c * ?b) = _ / ?c", "cancel"),
6.29 - ("fill-cancel-right-den",
6.30 - parse_patt @{theory Rational} "(?a * ?b) / (?c * ?b) = ?b / _", "cancel"),
6.31 -
6.32 -
6.33 -
6.34 - ("fill-mult-den",
6.35 - parse_patt @{theory Rational} "(?a * ?b) / (?a * ?c) = ?b / _", "cancel")]: fillpat list;
6.36 +*}
6.37 +ML {* (*==================*)
6.38
6.39 *}
6.40 -text {*
6.41 -insert_fillpats @{theory Rational} "IsacKnowledge" ("diff_sin_chain", @{thm diff_sin_chain}) fillpats;
6.42 +ML {*
6.43 +*}
6.44 +ML {*
6.45 +*}
6.46 +ML {*
6.47 *}
6.48 ML {*
6.49 *}
6.50 ML {* (*==================*)
6.51 *}
6.52 ML {*
6.53 -@{thm frac_eq_eq};
6.54 -@{thm nonzero_divide_eq_eq};
6.55 -@{thm right_inverse_eq};
6.56 -
6.57 -@{thm divide_cancel_left};
6.58 -@{thm divide_cancel_right};
6.59 -@{thm divide_eq_eq_number_of};
6.60 -@{thm divide_eq_eq_number_of1};
6.61 -@{thm divide_eq_0_iff};
6.62 -@{thm divide_eq_1_iff};
6.63 -@{thm divide_eq_eq};
6.64 -@{thm divide_eq_eq_1};
6.65 -@{thm one_divide_eq_0_iff};
6.66 *}
6.67 ML {*
6.68 *}
6.69 ML {*
6.70 -states:=[];
6.71 -CalcTree
6.72 -[(["Term ((5*b + 25)/(a^2 - b^2) * (a - b)/(5*b))", "normalform N"],
6.73 - ("Rational",["rational","simplification"], ["simplification","of_rationals"]))];
6.74 -Iterator 1;
6.75 -moveActiveRoot 1;
6.76 -autoCalculate 1 CompleteCalc;
6.77 -val ((pt,p),_) = get_calc 1; show_pt pt;
6.78 -
6.79 -*}
6.80 -ML {*
6.81 -states:=[];
6.82 -CalcTree
6.83 -[(["Term (8 / (4 / 2))", "normalform N"],
6.84 - ("Rational",["rational","simplification"], ["simplification","of_rationals"]))];
6.85 -Iterator 1;
6.86 -moveActiveRoot 1;
6.87 -autoCalculate 1 CompleteCalc;
6.88 -val ((pt,p),_) = get_calc 1; show_pt pt;
6.89 -
6.90 -*}
6.91 -ML {*
6.92 *}
6.93 ML {* (*==================*)
6.94 "~~~~~ fun , args:"; val () = ();
7.1 --- a/test/Tools/isac/xmlsrc/interface-xml.sml Sun Jul 29 16:29:04 2012 +0200
7.2 +++ b/test/Tools/isac/xmlsrc/interface-xml.sml Mon Jul 30 16:41:08 2012 +0200
7.3 @@ -2,3 +2,53 @@
7.4 Author: Walther Neuper 110320
7.5 (c) copyright due to lincense terms.
7.6 *)
7.7 +
7.8 +"-----------------------------------------------------------------";
7.9 +"table of contents -----------------------------------------------";
7.10 +"-----------------------------------------------------------------";
7.11 +"----------- fun fetchproposedtacticOK2xml -----------------------";
7.12 +"----------- fun findFillpatterns2xml ----------------------------";
7.13 +"-----------------------------------------------------------------";
7.14 +"-----------------------------------------------------------------";
7.15 +"-----------------------------------------------------------------";
7.16 +
7.17 +
7.18 +"----------- fun fetchproposedtacticOK2xml -----------------------";
7.19 +"----------- fun fetchproposedtacticOK2xml -----------------------";
7.20 +"----------- fun fetchproposedtacticOK2xml -----------------------";
7.21 +fetchproposedtacticOK2xml 11 (Rewrite ("rmult_commute", "?m *?n =?n *?m"));
7.22 +(*
7.23 +@@@@@begin@@@@@
7.24 + 11
7.25 +<NEXTTAC>
7.26 + <CALCID> 11 </CALCID>
7.27 + <REWRITETACTIC name="Rewrite">
7.28 + <THEOREM>
7.29 + <ID> rmult_commute </ID>
7.30 + <FORMULA>
7.31 + <MATHML>
7.32 + <ISA> ?m * ?n = ?n * ?m </ISA>
7.33 + </MATHML>
7.34 + </FORMULA>
7.35 + </THEOREM>
7.36 + </REWRITETACTIC>
7.37 +</NEXTTAC>
7.38 +@@@@@end@@@@@
7.39 +*)
7.40 +
7.41 +"----------- fun findFillpatterns2xml ----------------------------";
7.42 +"----------- fun findFillpatterns2xml ----------------------------";
7.43 +"----------- fun findFillpatterns2xml ----------------------------";
7.44 +findFillpatterns2xml 11 ["fill-d_d-arg","fill-both-args"]
7.45 +(*
7.46 +@@@@@begin@@@@@
7.47 + 11
7.48 +<FINDFILLPATTERNS>
7.49 + <CALCID> 11 </CALCID>
7.50 + <STRINGLIST>
7.51 + <STRING> fill-d_d-arg </STRING>
7.52 + <STRING> fill-both-args </STRING>
7.53 + </STRINGLIST>
7.54 +</FINDFILLPATTERNS>
7.55 +@@@@@end@@@@@
7.56 +*)