# HG changeset patch # User Walther Neuper # Date 1343659268 -7200 # Node ID 429980a4c4720bdd045dfa1c15aa97f46d7f9d22 # Parent 36ac220da82e5f8dbd2a714fabac89c87869e8ef findFillpatterns: repaired signature now matches the method IToCalc#findFillpatterns, which now returns the patterns directly without involving CalcMessage. diff -r 36ac220da82e -r 429980a4c472 src/Tools/isac/Frontend/interface.sml --- a/src/Tools/isac/Frontend/interface.sml Sun Jul 29 16:29:04 2012 +0200 +++ b/src/Tools/isac/Frontend/interface.sml Mon Jul 30 16:41:08 2012 +0200 @@ -782,10 +782,7 @@ val ((pt, _), _) = get_calc cI val pos = get_pos cI 1; val fillpats = find_fillpatterns (pt, pos) errpatID - val args = "fill patterns " ^ - ((map ((apsnd term2str) o quad2pair) fillpats) |> map pair2str_ |> strs2str_) - (* the format for the message's arguments is waiting for generalisation of CalcMessage *) - in calcMessage2xml cI ("fill patterns " ^ args) end; + in findFillpatterns2xml cI (map #1 fillpats) end; (* given a fillpatID propose a fillform to the learner on the worksheet; the "ctree" is extended with fillpat and "ostate Inconsistent", diff -r 36ac220da82e -r 429980a4c472 src/Tools/isac/xmlsrc/interface-xml.sml --- a/src/Tools/isac/xmlsrc/interface-xml.sml Sun Jul 29 16:29:04 2012 +0200 +++ b/src/Tools/isac/xmlsrc/interface-xml.sml Mon Jul 30 16:41:08 2012 +0200 @@ -12,10 +12,7 @@ "@@@@@begin@@@@@\n "^string_of_int uI # omit the distinctions APPENDFORMULA, REPLACEFORMULA, ... WN071004 these 2 simplifications are begun with CALCMESSAGE - - use"xmlsrc/interface-xml.sml"; - use"interface-xml.sml"; - *) +*) type iterID = int; type calcID = int; @@ -260,16 +257,14 @@ "\n" ^ "@@@@@end@@@@@"); -fun fetchproposedtacticOK2xml (*uI:userID*) (cI:calcID) tac = +fun fetchproposedtacticOK2xml (cI:calcID) tac = writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^ "\n" ^ " "^string_of_int cI^" \n"^ tac2xml i tac^ -(* ^(strs2xml o (map (tac2xml i))) tacs^*) "\n" ^ "@@@@@end@@@@@"); -(* fetchproposedtactic2xml 11 22 (Rewrite ("rmult_commute","?m *?n =?n *?m")); - *) + fun fetchproposedtacticERROR2xml (*uI:userID*) (cI:calcID) e = writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^ "\n" ^ @@ -340,8 +335,16 @@ contthy2xml i contthy ^ "\n" ^ "@@@@@end@@@@@"); - (* fun contextthyNO2xml guh = writeln (datatypes.contextthyNO2xml 0 guh); *) + +fun findFillpatterns2xml (cI:calcID) pattIDs = + writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^ + "\n" ^ + " "^string_of_int cI^" \n" ^ + id2xml 3 pattIDs ^ + "\n" ^ + "@@@@@end@@@@@"); + diff -r 36ac220da82e -r 429980a4c472 test/Tools/isac/Frontend/interface.sml --- a/test/Tools/isac/Frontend/interface.sml Sun Jul 29 16:29:04 2012 +0200 +++ b/test/Tools/isac/Frontend/interface.sml Mon Jul 30 16:41:08 2012 +0200 @@ -49,8 +49,8 @@ "--------- replaceFormula {SOL:MAN:FOR:replace} other 2--"; "--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----"; "--------- UC errpat, fillpat by input ---------------------------"; -"--------- UC errpat, fillpat step to at Rewrite -----------------"; -"--------- UC errpat, fillpat step to at Rewrite_Set -------------"; +"--------- UC errpat, fillpat step to Rewrite --------------------"; +"--------- UC errpat, fillpat step to Rewrite_Set ----------------"; "--------------------------------------------------------"; "within struct ---------------------------------------------------"; @@ -1341,9 +1341,8 @@ error "FE-interface.sml: diff.behav. in FORMULA:replace} NOTok"; DEconstrCalcTree 1; -"--------- UC errpat, fillpat ------------------------------------"; -"--------- UC errpat, fillpat ------------------------------------"; -"--------- UC errpat, fillpat ------------------------------------"; +"--------- UC errpat, fillpat by input ---------------------------"; +"--------- UC errpat, fillpat by input ---------------------------"; "--------- UC errpat, fillpat by input ---------------------------"; states := []; CalcTree @@ -1420,9 +1419,9 @@ (([5], Res), 2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3), (([], Res), 2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3)] *) -"--------- UC errpat, fillpat step to at Rewrite -----------------"; -"--------- UC errpat, fillpat step to at Rewrite -----------------"; -"--------- UC errpat, fillpat step to at Rewrite -----------------"; +"--------- UC errpat, fillpat step to Rewrite --------------------"; +"--------- UC errpat, fillpat step to Rewrite --------------------"; +"--------- UC errpat, fillpat step to Rewrite --------------------"; (*TODO*) states:=[]; CalcTree @@ -1435,9 +1434,9 @@ autoCalculate 1 CompleteCalc; val ((pt,p),_) = get_calc 1; show_pt pt; -"--------- UC errpat, fillpat step to at Rewrite_Set -------------"; -"--------- UC errpat, fillpat step to at Rewrite_Set -------------"; -"--------- UC errpat, fillpat step to at Rewrite_Set -------------"; +"--------- UC errpat, fillpat step to Rewrite_Set ----------------"; +"--------- UC errpat, fillpat step to Rewrite_Set ----------------"; +"--------- UC errpat, fillpat step to Rewrite_Set ----------------"; (*TODO*) states:=[]; CalcTree diff -r 36ac220da82e -r 429980a4c472 test/Tools/isac/Interpret/generate.sml --- a/test/Tools/isac/Interpret/generate.sml Sun Jul 29 16:29:04 2012 +0200 +++ b/test/Tools/isac/Interpret/generate.sml Mon Jul 30 16:41:08 2012 +0200 @@ -78,8 +78,9 @@ if p = ([2], Res) andalso get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", "")) andalso term2str f = - "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos ?_dummy_2 * d_d x ?_dummy_3" + "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos ?u * d_d x ?_dummy_2" + (*WAS with old findFillpatterns: + "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos ?_dummy_2 * d_d x ?_dummy_3"*) then () else error ""; show_pt pt; (*ATTENTION: omits the last step, if pt is incomplete, ([2], Res) EXISTS !*) - diff -r 36ac220da82e -r 429980a4c472 test/Tools/isac/Interpret/inform.sml --- a/test/Tools/isac/Interpret/inform.sml Sun Jul 29 16:29:04 2012 +0200 +++ b/test/Tools/isac/Interpret/inform.sml Mon Jul 30 16:41:08 2012 +0200 @@ -1016,9 +1016,10 @@ "~~~~~ to findFillpatterns return val:"; val (fillpats) = (map (get_fillpats (subs_opt, subst) f_curr errpatID) errpatthms |> flat) (*only from "hd errpatthms"*); +"vvv--- dropped this code WN120730"; val msg = "fill patterns " ^ ((map ((apsnd term2str) o quad2pair) fillpats) |> map pair2str_ |> strs2str_); -if msg = +msg = "fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" ^ " =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1" ^ "#fill-both-args#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" ^ @@ -1027,8 +1028,13 @@ " =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * ?_dummy_1 x (x ^^^ 4)" ^ "#fill-inner-deriv#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" ^ " =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * ?_dummy_1" ^ - "#fill-all#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) = d_d x (x ^^^ 2) + ?_dummy_1#" -then () else error "find_fillpatterns changed 4"; + "#fill-all#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) = d_d x (x ^^^ 2) + ?_dummy_1#"; +"^^^--- dropped this code WN120730"; + +if (map #1 fillpats) = + ["fill-d_d-arg", "fill-both-args", "fill-d_d", "fill-inner-deriv", "fill-all"] +then () else error "find_fillpatterns changed 4b"; + "--------- build fun is_exactly_equal, inputFillFormula ----------"; "--------- build fun is_exactly_equal, inputFillFormula ----------"; diff -r 36ac220da82e -r 429980a4c472 test/Tools/isac/Test_Some.thy --- a/test/Tools/isac/Test_Some.thy Sun Jul 29 16:29:04 2012 +0200 +++ b/test/Tools/isac/Test_Some.thy Mon Jul 30 16:41:08 2012 +0200 @@ -1,7 +1,7 @@ theory Test_Some imports Isac begin -use"../../../test/Tools/isac/Knowledge/diff.sml" +use"../../../test/Tools/isac/Interpret/generate.sml" ML {* val thy = @{theory "Isac"}; @@ -12,75 +12,30 @@ ML {* *} ML {* (*==================*) -@{thm times_divide_times_eq} (* "?x / ?y * (?z / ?w) = ?x * ?z / (?y * ?w)" *); -@{thm rat_mult} (* "?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)" *); *} ML {* *} - -find_theorems "(_ / _) * (_ / _)= _" - ML {* -val fillpats = [ - ("fill-cancel-right-num", - parse_patt @{theory Rational} "(?a * ?b) / (?c * ?b) = _ / ?c", "cancel"), - ("fill-cancel-right-den", - parse_patt @{theory Rational} "(?a * ?b) / (?c * ?b) = ?b / _", "cancel"), - - - - ("fill-mult-den", - parse_patt @{theory Rational} "(?a * ?b) / (?a * ?c) = ?b / _", "cancel")]: fillpat list; +*} +ML {* (*==================*) *} -text {* -insert_fillpats @{theory Rational} "IsacKnowledge" ("diff_sin_chain", @{thm diff_sin_chain}) fillpats; +ML {* +*} +ML {* +*} +ML {* *} ML {* *} ML {* (*==================*) *} ML {* -@{thm frac_eq_eq}; -@{thm nonzero_divide_eq_eq}; -@{thm right_inverse_eq}; - -@{thm divide_cancel_left}; -@{thm divide_cancel_right}; -@{thm divide_eq_eq_number_of}; -@{thm divide_eq_eq_number_of1}; -@{thm divide_eq_0_iff}; -@{thm divide_eq_1_iff}; -@{thm divide_eq_eq}; -@{thm divide_eq_eq_1}; -@{thm one_divide_eq_0_iff}; *} ML {* *} ML {* -states:=[]; -CalcTree -[(["Term ((5*b + 25)/(a^2 - b^2) * (a - b)/(5*b))", "normalform N"], - ("Rational",["rational","simplification"], ["simplification","of_rationals"]))]; -Iterator 1; -moveActiveRoot 1; -autoCalculate 1 CompleteCalc; -val ((pt,p),_) = get_calc 1; show_pt pt; - -*} -ML {* -states:=[]; -CalcTree -[(["Term (8 / (4 / 2))", "normalform N"], - ("Rational",["rational","simplification"], ["simplification","of_rationals"]))]; -Iterator 1; -moveActiveRoot 1; -autoCalculate 1 CompleteCalc; -val ((pt,p),_) = get_calc 1; show_pt pt; - -*} -ML {* *} ML {* (*==================*) "~~~~~ fun , args:"; val () = (); diff -r 36ac220da82e -r 429980a4c472 test/Tools/isac/xmlsrc/interface-xml.sml --- a/test/Tools/isac/xmlsrc/interface-xml.sml Sun Jul 29 16:29:04 2012 +0200 +++ b/test/Tools/isac/xmlsrc/interface-xml.sml Mon Jul 30 16:41:08 2012 +0200 @@ -2,3 +2,53 @@ Author: Walther Neuper 110320 (c) copyright due to lincense terms. *) + +"-----------------------------------------------------------------"; +"table of contents -----------------------------------------------"; +"-----------------------------------------------------------------"; +"----------- fun fetchproposedtacticOK2xml -----------------------"; +"----------- fun findFillpatterns2xml ----------------------------"; +"-----------------------------------------------------------------"; +"-----------------------------------------------------------------"; +"-----------------------------------------------------------------"; + + +"----------- fun fetchproposedtacticOK2xml -----------------------"; +"----------- fun fetchproposedtacticOK2xml -----------------------"; +"----------- fun fetchproposedtacticOK2xml -----------------------"; +fetchproposedtacticOK2xml 11 (Rewrite ("rmult_commute", "?m *?n =?n *?m")); +(* +@@@@@begin@@@@@ + 11 + + 11 + + + rmult_commute + + + ?m * ?n = ?n * ?m + + + + + +@@@@@end@@@@@ +*) + +"----------- fun findFillpatterns2xml ----------------------------"; +"----------- fun findFillpatterns2xml ----------------------------"; +"----------- fun findFillpatterns2xml ----------------------------"; +findFillpatterns2xml 11 ["fill-d_d-arg","fill-both-args"] +(* +@@@@@begin@@@@@ + 11 + + 11 + + fill-d_d-arg + fill-both-args + + +@@@@@end@@@@@ +*)