wneuper/isa: comparison test/Tools/isac/Frontend/use-cases.sml

equal deleted inserted replaced

-:7d3dbc1171ff
+:f0bb15a046ae
 "exported from struct --------------------------------------------";
 "exported from struct --------------------------------------------";
 (*------------ set at startup of the Kernel ----------------------*)
-reset_states ();  (*resets all state information in Kernel           *)
+reset_states ();  (*resets all state information in Kernel        *)
 (*----------------------------------------------------------------*)
 "--------- empty rootpbl --------------------------------";
 "--------- empty rootpbl --------------------------------";
 "--------- empty rootpbl --------------------------------";
 "--------- miniscript with mini-subpbl ------------------";
 "--------- miniscript with mini-subpbl ------------------";
 "--------- miniscript with mini-subpbl ------------------";
 (*WN120210?not ME:\label{SOLVE:MANUAL:TACTIC:enter} UC 30.3.2.1 p.175 !!!!!NOT IMPL IN FE*)
 "=== this sequence of fun-calls resembles fun me ===";
-reset_states (); (*start of calculation, return No.1*)
 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
 ("Test", ["sqroot-test","univariate","equation","test"],
 ["Test","squ-equ-test-subpbl1"]))];
 Iterator 1;
 val ((pt,_),_) = get_calc 1;
 val p = get_pos 1 1;
 val (Form f, tac, asms) = pt_extract (pt, p);
 if term2str f = "[x = 1]" andalso p = ([], Res) then () else
 error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
 DEconstrCalcTree 1;
 "--------- mini-subpbl AUTO CompleteCalcHead ------------";
 "--------- mini-subpbl AUTO CompleteCalcHead ------------";
 "--------- mini-subpbl AUTO CompleteCalcHead ------------";
 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
 val ((pt,_),_) = get_calc 1;
 val p = get_pos 1 1;
 val (Form f, tac, asms) = pt_extract (pt, p);
 if term2str f = "[x = 1]" andalso p = ([], Res) then () else
 error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
 DEconstrCalcTree 1;
 "--------- setContext..Thy ------------------------------";
 "--------- setContext..Thy ------------------------------";
 "--------- setContext..Thy ------------------------------";
-reset_states ();
 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
 ("Test", ["sqroot-test","univariate","equation","test"],
 ["Test","squ-equ-test-subpbl1"]))];
 Iterator 1; moveActiveRoot 1;
 autoCalculate 1 CompleteCalcHead;
 val p = get_pos 1 1;
 val (Form f, tac, asms) = pt_extract (pt, p);
 if term2str f = "[x = 1]" andalso p = ([], Res) then () else
 error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl 1";
 DEconstrCalcTree 1;
 "--------- rat-eq + subpbl: no_met, NO solution dropped -";
 "--------- rat-eq + subpbl: no_met, NO solution dropped -";
 "--------- rat-eq + subpbl: no_met, NO solution dropped -";
 CalcTree
 autoCalculate 1 (Step 1); fetchProposedTactic 1;
 setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
 autoCalculate 1 (Step 1); fetchProposedTactic 1;
 setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);
 autoCalculate 1 (Step 1); fetchProposedTactic 1;
-setNextTactic 1 (Rewrite ("all_left", Thm.prop_of @{thm all_left}));
+setNextTactic 1 (Rewrite ("all_left", @{thm all_left}));
 autoCalculate 1 (Step 1); fetchProposedTactic 1;
 setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "make_ratpoly_in"));
 autoCalculate 1 (Step 1); fetchProposedTactic 1;
 (*               __________ for "16 + 12 * x = 0"*)
 setNextTactic 1 (Subproblem ("PolyEq",
 setNextTactic 1 (Check_Postcond ["rational","univariate","equation"]);
 val (ptp,_) = get_calc 1;
 val (Form t,_,_) = pt_extract ptp;
 if get_pos 1 1 = ([], Res) andalso term2str t = "[x = -4 / 3]" then ()
 else writeln "FE-inteface.sml: diff.behav. in rat-eq + subpbl: no_met, NO ..";
 DEconstrCalcTree 1;
 "--------- tryMatchProblem, tryRefineProblem ------------";
 "--------- tryMatchProblem, tryRefineProblem ------------";
 "--------- tryMatchProblem, tryRefineProblem ------------";
 (*{\bf\UC{Having \isac{} Refine the Problem
 show_pt pt;
 val p = get_pos 1 1;
 val (Form f, tac, asms) = pt_extract (pt, p);
 if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else
 error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
+DEconstrCalcTree 1;
-DEconstrCalcTree 1;
 "--------- modifyCalcHead, resetCalcHead, modelProblem --";
 "--------- modifyCalcHead, resetCalcHead, modelProblem --";
 "--------- modifyCalcHead, resetCalcHead, modelProblem --";
 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
 DEconstrCalcTree 1;
 "--------- UC errpat chain-rule-diff-both, fillpat by input ------";
 "--------- UC errpat chain-rule-diff-both, fillpat by input ------";
 "--------- UC errpat chain-rule-diff-both, fillpat by input ------";
-reset_states ();
 CalcTree
 [(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
 ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
 Iterator 1;
 moveActiveRoot 1;
 instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)
 val ((pt,pos), _) = get_calc 1;
 val p = get_pos 1 1;
 val (Form f, _, asms) = pt_extract (pt, p);
-if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
+if p = ([2], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"
-get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"],
+then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(bdv, x)"],
-("diff_sum", str2term "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v"))
+("diff_sum", thm)) => () | _ => error "embed fun get_fillform changed 0"
-then () else error "embed fun get_fillform changed 1";
+| _ => error "embed fun get_fillform changed 1"
+else error "embed fun get_fillform changed 2";
+============ inhibit exn WN161019 TODO ========================================================*)
 (*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ====================
 findFillpatterns 1 "chain-rule-diff-both"; (*<<<<<<<=================================*)
 (*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =
 d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *)
 (([3], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * (4 * x ^^^ (4 - 1))),
 (([4], Res), 2 * x ^^^ (2 - 1) + cos (x ^^^ 4) * (4 * x ^^^ (4 - 1))),
 (([5], Res), 2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3),
 (([], Res), 2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3)] *)
 ============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*)
+DEconstrCalcTree 1;
 "--------- UC errpat add-fraction, fillpat by input --------------";
 "--------- UC errpat add-fraction, fillpat by input --------------";
 "--------- UC errpat add-fraction, fillpat by input --------------";
 (*cp from BridgeLog Java <=> SML*)
-reset_states ();
+=CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
-CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
 Iterator 1;
 moveActiveRoot 1;
 moveActiveFormula 1 ([],Pbl);
 replaceFormula 1 "Simplify (5 * x / (4 * y) + 3 * x / (4 * y))";
 autoCalculate 1 CompleteCalcHead;
 autoCalculate 1 (Step 1);
 appendFormula 1 "8 * x / (8 * y)" (*|> Future.join*);
 (*<CALCMESSAGE> no derivation found </CALCMESSAGE>
 --- but in BridgeLog Java <=> SML:
 <CALCMESSAGE> error pattern #addition-of-fractions# </CALCMESSAGE>*)
+DEconstrCalcTree 1;
 "--------- UC errpat, fillpat step to Rewrite --------------------";
 "--------- UC errpat, fillpat step to Rewrite --------------------";
 "--------- UC errpat, fillpat step to Rewrite --------------------";
 (*TODO*)
-reset_states ();
+=CalcTree
-CalcTree
 [(["functionTerm ((x ^ 2) ^ 3 + sin (x ^ 4))",
 "differentiateFor x", "derivative f_f'"],
 ("Isac", ["derivative_of","function"],
 ["diff","differentiate_on_R"]))]; (*<<<======= EP is directly in script*)
 Iterator 1;
 moveActiveRoot 1;
 autoCalculate 1 CompleteCalc;
 val ((pt,p),_) = get_calc 1; show_pt pt;
+DEconstrCalcTree 1;
 "--------- UC errpat, fillpat step to Rewrite_Set ----------------";
 "--------- UC errpat, fillpat step to Rewrite_Set ----------------";
 "--------- UC errpat, fillpat step to Rewrite_Set ----------------";
-reset_states ();
 CalcTree
 [(["functionTerm ((x ^ 2) ^ 3 + sin (x ^ 4))",
 "differentiateFor x", "derivative f_f'"],
 ("Isac", ["derivative_of","function"],
 ["diff","after_simplification"]))]; (*<<<======= EP is in a ruleset*)
 (* then --- UC errpat, fillpat by input ---*)
 *)
 autoCalculate 1 CompleteCalc;
 val ((pt,p),_) = get_calc 1; show_pt pt;
 (*WN1208 postponed due to efforts required for stepToErrorPatterns (NEW rewrite_set_)*)
+DEconstrCalcTree 1;

changeset 59253	f0bb15a046ae
parent 59252	7d3dbc1171ff
child 59254	0d84c462dd7e