1.1 --- a/test/Tools/isac/Frontend/use-cases.sml Tue Oct 18 12:05:03 2016 +0200
1.2 +++ b/test/Tools/isac/Frontend/use-cases.sml Thu Oct 20 10:26:29 2016 +0200
1.3 @@ -81,7 +81,7 @@
1.4
1.5
1.6 (*------------ set at startup of the Kernel ----------------------*)
1.7 -reset_states (); (*resets all state information in Kernel *)
1.8 +reset_states (); (*resets all state information in Kernel *)
1.9 (*----------------------------------------------------------------*)
1.10
1.11 "--------- empty rootpbl --------------------------------";
1.12 @@ -207,7 +207,6 @@
1.13 "--------- miniscript with mini-subpbl ------------------";
1.14 (*WN120210?not ME:\label{SOLVE:MANUAL:TACTIC:enter} UC 30.3.2.1 p.175 !!!!!NOT IMPL IN FE*)
1.15 "=== this sequence of fun-calls resembles fun me ===";
1.16 - reset_states (); (*start of calculation, return No.1*)
1.17 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.18 ("Test", ["sqroot-test","univariate","equation","test"],
1.19 ["Test","squ-equ-test-subpbl1"]))];
1.20 @@ -451,7 +450,7 @@
1.21 val (Form f, tac, asms) = pt_extract (pt, p);
1.22 if term2str f = "[x = 1]" andalso p = ([], Res) then () else
1.23 error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
1.24 -DEconstrCalcTree 1;
1.25 + DEconstrCalcTree 1;
1.26
1.27 "--------- mini-subpbl AUTO CompleteCalcHead ------------";
1.28 "--------- mini-subpbl AUTO CompleteCalcHead ------------";
1.29 @@ -512,12 +511,11 @@
1.30 val (Form f, tac, asms) = pt_extract (pt, p);
1.31 if term2str f = "[x = 1]" andalso p = ([], Res) then () else
1.32 error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
1.33 -DEconstrCalcTree 1;
1.34 + DEconstrCalcTree 1;
1.35
1.36 "--------- setContext..Thy ------------------------------";
1.37 "--------- setContext..Thy ------------------------------";
1.38 "--------- setContext..Thy ------------------------------";
1.39 - reset_states ();
1.40 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.41 ("Test", ["sqroot-test","univariate","equation","test"],
1.42 ["Test","squ-equ-test-subpbl1"]))];
1.43 @@ -577,7 +575,7 @@
1.44 val (Form f, tac, asms) = pt_extract (pt, p);
1.45 if term2str f = "[x = 1]" andalso p = ([], Res) then () else
1.46 error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl 1";
1.47 -DEconstrCalcTree 1;
1.48 + DEconstrCalcTree 1;
1.49
1.50 "--------- rat-eq + subpbl: no_met, NO solution dropped -";
1.51 "--------- rat-eq + subpbl: no_met, NO solution dropped -";
1.52 @@ -621,7 +619,7 @@
1.53 autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.54 setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);
1.55 autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.56 - setNextTactic 1 (Rewrite ("all_left", Thm.prop_of @{thm all_left}));
1.57 + setNextTactic 1 (Rewrite ("all_left", @{thm all_left}));
1.58 autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.59 setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "make_ratpoly_in"));
1.60 autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.61 @@ -661,7 +659,7 @@
1.62 val (Form t,_,_) = pt_extract ptp;
1.63 if get_pos 1 1 = ([], Res) andalso term2str t = "[x = -4 / 3]" then ()
1.64 else writeln "FE-inteface.sml: diff.behav. in rat-eq + subpbl: no_met, NO ..";
1.65 -DEconstrCalcTree 1;
1.66 + DEconstrCalcTree 1;
1.67
1.68 "--------- tryMatchProblem, tryRefineProblem ------------";
1.69 "--------- tryMatchProblem, tryRefineProblem ------------";
1.70 @@ -781,8 +779,7 @@
1.71 val (Form f, tac, asms) = pt_extract (pt, p);
1.72 if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else
1.73 error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
1.74 -
1.75 -DEconstrCalcTree 1;
1.76 + DEconstrCalcTree 1;
1.77
1.78 "--------- modifyCalcHead, resetCalcHead, modelProblem --";
1.79 "--------- modifyCalcHead, resetCalcHead, modelProblem --";
1.80 @@ -1356,7 +1353,6 @@
1.81 "--------- UC errpat chain-rule-diff-both, fillpat by input ------";
1.82 "--------- UC errpat chain-rule-diff-both, fillpat by input ------";
1.83 "--------- UC errpat chain-rule-diff-both, fillpat by input ------";
1.84 -reset_states ();
1.85 CalcTree
1.86 [(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
1.87 ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
1.88 @@ -1374,10 +1370,12 @@
1.89 val p = get_pos 1 1;
1.90 val (Form f, _, asms) = pt_extract (pt, p);
1.91
1.92 - if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
1.93 - get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"],
1.94 - ("diff_sum", str2term "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v"))
1.95 - then () else error "embed fun get_fillform changed 1";
1.96 + if p = ([2], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"
1.97 + then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(bdv, x)"],
1.98 + ("diff_sum", thm)) => () | _ => error "embed fun get_fillform changed 0"
1.99 + | _ => error "embed fun get_fillform changed 1"
1.100 +else error "embed fun get_fillform changed 2";
1.101 +============ inhibit exn WN161019 TODO ========================================================*)
1.102
1.103 (*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ====================
1.104 findFillpatterns 1 "chain-rule-diff-both"; (*<<<<<<<=================================*)
1.105 @@ -1433,13 +1431,13 @@
1.106 (([5], Res), 2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3),
1.107 (([], Res), 2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3)] *)
1.108 ============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*)
1.109 +DEconstrCalcTree 1;
1.110
1.111 "--------- UC errpat add-fraction, fillpat by input --------------";
1.112 "--------- UC errpat add-fraction, fillpat by input --------------";
1.113 "--------- UC errpat add-fraction, fillpat by input --------------";
1.114 (*cp from BridgeLog Java <=> SML*)
1.115 -reset_states ();
1.116 -CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
1.117 +=CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
1.118 Iterator 1;
1.119 moveActiveRoot 1;
1.120 moveActiveFormula 1 ([],Pbl);
1.121 @@ -1450,13 +1448,13 @@
1.122 (*<CALCMESSAGE> no derivation found </CALCMESSAGE>
1.123 --- but in BridgeLog Java <=> SML:
1.124 <CALCMESSAGE> error pattern #addition-of-fractions# </CALCMESSAGE>*)
1.125 +DEconstrCalcTree 1;
1.126
1.127 "--------- UC errpat, fillpat step to Rewrite --------------------";
1.128 "--------- UC errpat, fillpat step to Rewrite --------------------";
1.129 "--------- UC errpat, fillpat step to Rewrite --------------------";
1.130 (*TODO*)
1.131 -reset_states ();
1.132 -CalcTree
1.133 +=CalcTree
1.134 [(["functionTerm ((x ^ 2) ^ 3 + sin (x ^ 4))",
1.135 "differentiateFor x", "derivative f_f'"],
1.136 ("Isac", ["derivative_of","function"],
1.137 @@ -1465,11 +1463,11 @@
1.138 moveActiveRoot 1;
1.139 autoCalculate 1 CompleteCalc;
1.140 val ((pt,p),_) = get_calc 1; show_pt pt;
1.141 +DEconstrCalcTree 1;
1.142
1.143 "--------- UC errpat, fillpat step to Rewrite_Set ----------------";
1.144 "--------- UC errpat, fillpat step to Rewrite_Set ----------------";
1.145 "--------- UC errpat, fillpat step to Rewrite_Set ----------------";
1.146 -reset_states ();
1.147 CalcTree
1.148 [(["functionTerm ((x ^ 2) ^ 3 + sin (x ^ 4))",
1.149 "differentiateFor x", "derivative f_f'"],
1.150 @@ -1517,4 +1515,5 @@
1.151 autoCalculate 1 CompleteCalc;
1.152 val ((pt,p),_) = get_calc 1; show_pt pt;
1.153 (*WN1208 postponed due to efforts required for stepToErrorPatterns (NEW rewrite_set_)*)
1.154 +DEconstrCalcTree 1;
1.155