1.1 --- a/test/Tools/isac/Test_Some.thy Wed Jul 20 13:05:48 2011 +0200
1.2 +++ b/test/Tools/isac/Test_Some.thy Wed Jul 20 14:55:29 2011 +0200
1.3 @@ -7,177 +7,13 @@
1.4
1.5 ML{* writeln "**** run the test ***************************************" *}
1.6
1.7 -use"../../../test/Tools/isac/Frontend/interface.sml"
1.8 +use"../../../test/Tools/isac/Frontend/interface.sml"
1.9
1.10 ML{*
1.11
1.12
1.13 -"--------- rat-eq + subpbl: no_met, NO solution dropped -";
1.14 - states:=[];
1.15 - CalcTree
1.16 - [(["equality ((5*x)/(x - 2) - x/(x+2)=(4::real))", "solveFor x","solutions L"],
1.17 - ("RatEq", ["univariate","equation"], ["no_met"]))];
1.18 - Iterator 1;
1.19 - moveActiveRoot 1;
1.20 - fetchProposedTactic 1;
1.21 -
1.22 -(*ERROR: setNextTactic 1 produces "get_calc 1 not existent"*)
1.23 - setNextTactic 1 (Model_Problem );
1.24 -autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.25 -
1.26 -(*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
1.27 - setNextTactic 1 (Add_Given "equality (5 * x / (x - 2) - x / (x + 2) = 4)");
1.28 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.29 - setNextTactic 1 (Add_Given "solveFor x");
1.30 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.31 - setNextTactic 1 (Add_Find "solutions L");
1.32 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.33 -*-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
1.34 - setNextTactic 1 (Specify_Theory "RatEq");
1.35 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.36 - setNextTactic 1 (Specify_Problem ["rational","univariate","equation"]);
1.37 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.38 - setNextTactic 1 (Specify_Method ["RatEq","solve_rat_equation"]);
1.39 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.40 - setNextTactic 1 (Apply_Method ["RatEq","solve_rat_equation"]);
1.41 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.42 - setNextTactic 1 (Rewrite_Set "RatEq_simplify");
1.43 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.44 - setNextTactic 1 (Rewrite_Set "norm_Rational");
1.45 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.46 - setNextTactic 1 (Rewrite_Set "RatEq_eliminate");
1.47 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.48 - (* __________ for "12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2)"*)
1.49 - setNextTactic 1 (Subproblem ("PolyEq", ["normalize","polynomial",
1.50 - "univariate","equation"]));
1.51 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.52 - setNextTactic 1 (Model_Problem );
1.53 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.54 -(*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
1.55 - setNextTactic 1 (Add_Given
1.56 - "equality (12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2))");
1.57 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.58 - setNextTactic 1 (Add_Given "solveFor x");
1.59 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.60 - setNextTactic 1 (Add_Find "solutions x_i");
1.61 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.62 -*-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
1.63 - setNextTactic 1 (Specify_Theory "PolyEq");
1.64 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.65 - setNextTactic 1 (Specify_Problem ["normalize","polynomial",
1.66 - "univariate","equation"]);
1.67 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.68 - setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
1.69 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.70 - setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);
1.71 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.72 - setNextTactic 1 (Rewrite ("all_left",""));
1.73 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.74 - setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "make_ratpoly_in"));
1.75 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.76 - (* __________ for "16 + 12 * x = 0"*)
1.77 - setNextTactic 1 (Subproblem ("PolyEq",
1.78 - ["degree_1","polynomial","univariate","equation"]));
1.79 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.80 - setNextTactic 1 (Model_Problem );
1.81 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.82 -(*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
1.83 - setNextTactic 1 (Add_Given
1.84 - "equality (16 + 12 * x = 0)");
1.85 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.86 - setNextTactic 1 (Add_Given "solveFor x");
1.87 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.88 - setNextTactic 1 (Add_Find "solutions x_i");
1.89 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.90 -*-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
1.91 - setNextTactic 1 (Specify_Theory "PolyEq");
1.92 - (*------------- some trials in the problem-hierarchy ---------------*)
1.93 - setNextTactic 1 (Specify_Problem ["linear","univariate","equation"]);
1.94 - autoCalculate 1 (Step 1); fetchProposedTactic 1; (*<ERROR> helpless </ERROR> !!!*)
1.95 - setNextTactic 1 (Refine_Problem ["univariate","equation"]);
1.96 - (*------------------------------------------------------------------*)
1.97 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.98 - setNextTactic 1 (Specify_Method ["PolyEq","solve_d1_polyeq_equation"]);
1.99 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.100 - setNextTactic 1 (Apply_Method ["PolyEq","solve_d1_polyeq_equation"]);
1.101 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.102 - setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "d1_polyeq_simplify"));
1.103 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.104 - setNextTactic 1 (Rewrite_Set "polyeq_simplify");
1.105 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.106 - (*==================================================================*)
1.107 - setNextTactic 1 Or_to_List;
1.108 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.109 -(* setNextTactic 1 (Check_elementwise "Assumptions");
1.110 - WAS: exception Match raised (line 1218 of ".../script.sml")*)
1.111 -"~~~~~ fun setNextTactic, args:"; val ((cI:calcID), tac) = (1, (Check_elementwise "Assumptions"));
1.112 -val ((pt, _), _) = get_calc cI;
1.113 -val ip = get_pos cI 1;
1.114 -(*locatetac tac (pt, ip) WAS: exception Match raised (line 1218 of ".../script.sml")*)
1.115 -"~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, ip));
1.116 -val (mI,m) = mk_tac'_ tac;
1.117 -val Appl m = applicable_in p pt m;
1.118 -member op = specsteps mI (*false*);
1.119 -(* loc_solve_ (mI,m) ptp WAS: exception Match raised (line 1218 of ".../script.sml")*)
1.120 -"~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = ((mI,m), ptp);
1.121 -(*solve m (pt, pos); WAS: exception Match raised (line 1218 of ".../script.sml")*)
1.122 -"~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
1.123 -e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*);
1.124 - val thy' = get_obj g_domID pt (par_pblobj pt p);
1.125 - val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
1.126 - val d = e_rls;
1.127 *}
1.128 ML{*
1.129 -(*locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is;
1.130 - WAS: exception Match raised (line 1218 of "isabisac/src/Tools/isac/Interpret/script.sml"*)
1.131 -"~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ptree * pos'),
1.132 - (scr as Script (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) =
1.133 - ((thy',srls), m ,(pt,(p,p_)) ,(sc,d) ,is); (* locate_gen 2nd pattern *)
1.134 -val thy = assoc_thy thy';
1.135 -
1.136 -*}
1.137 -ML{*
1.138 -*}
1.139 -ML{*
1.140 -(*case (astep_up (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) )
1.141 - of
1.142 - (Assoc (iss as (is as (_,_,_,_,_,bb), ss as ((m',f',pt',p',c')::_))))
1.143 - =>
1.144 - "nix";*)
1.145 -(*ERROR:
1.146 - Value identifier (c') has not been referenced.
1.147 - Value identifier (p') has not been referenced.
1.148 - Value identifier (pt') has not been referenced.
1.149 - Value identifier (f') has not been referenced.
1.150 - Value identifier (m') has not been referenced.
1.151 - Value identifier (ss) has not been referenced.
1.152 - Value identifier (bb) has not been referenced.
1.153 - Value identifier (is) has not been referenced.
1.154 - Value identifier (iss) has not been referenced.
1.155 - Matches are not exhaustive.
1.156 - exception Match raised*)
1.157 -*}
1.158 -ML{*
1.159 -(*case (astep_up (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) )
1.160 - of
1.161 - (Assoc (iss as (is as (_,_,_,_,_,bb), ss as ((m',f',pt',p',c')::_))))
1.162 - => (iss,is,bb,ss,m',f',pt',p',c');*)
1.163 -(*ERROR:
1.164 - Matches are not exhaustive.
1.165 - exception Match raised*)
1.166 -*}
1.167 -ML{*
1.168 -*}
1.169 -ML{*
1.170 -*}
1.171 -ML{*
1.172 -(*========== inhibit exn 110719 ================================================
1.173 -========== inhibit exn 110719 XXX=============================================*)
1.174 -
1.175 -
1.176 -*}
1.177 -ML{*
1.178 -
1.179 *}
1.180 ML{*
1.181 *}