1.1 --- a/src/Tools/isac/Interpret/script.sml Wed Jul 20 13:05:48 2011 +0200
1.2 +++ b/src/Tools/isac/Interpret/script.sml Wed Jul 20 14:55:29 2011 +0200
1.3 @@ -1015,41 +1015,35 @@
1.4 )
1.5 end);
1.6
1.7 -fun ass_up (ys as (y,s,Script sc,d)) (is as (E,l,a,v,S,b),ss)
1.8 - (Const ("HOL.Let",_) $ _) =
1.9 - let (*val _= tracing("### ass_up1 Let$e: is=")
1.10 - val _= tracing(istate2str (ScrState is))*)
1.11 - val l = drop_last l; (*comes from e, goes to Abs*)
1.12 - val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go l sc;
1.13 - val i = mk_Free (i, T);
1.14 - val E = upd_env E (i, v);
1.15 - (*val _=tracing("### ass_up2 Let$e: E="^(subst2str E));*)
1.16 - in case assy (((y,s),d),Aundef) ((E, l@[R,D], a,v,S,b),ss) body of
1.17 - Assoc iss => Assoc iss
1.18 - | NasApp iss => astep_up ys iss
1.19 - | NasNap (v, E) => astep_up ys ((E,l,a,v,S,b),ss) end
1.20 +fun ass_up (ys as (y,s,Script sc,d)) (is as (E,l,a,v,S,b),ss) (Const ("HOL.Let",_) $ _) =
1.21 + let
1.22 + (*val _= tracing("### ass_up1 Let$e: is=")
1.23 + val _= tracing(istate2str (ScrState is))*)
1.24 + val l = drop_last l; (*comes from e, goes to Abs*)
1.25 + val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go l sc;
1.26 + val i = mk_Free (i, T);
1.27 + val E = upd_env E (i, v);
1.28 + (*val _=tracing("### ass_up2 Let$e: E="^(subst2str E));*)
1.29 + in case assy (((y,s),d),Aundef) ((E, l@[R,D], a,v,S,b),ss) body of
1.30 + Assoc iss => Assoc iss
1.31 + | NasApp iss => astep_up ys iss
1.32 + | NasNap (v, E) => astep_up ys ((E,l,a,v,S,b),ss) end
1.33
1.34 | ass_up ys (iss as (is,_)) (Abs (_,_,_)) =
1.35 - ((*tracing("### ass_up Abs: is=");
1.36 - tracing(istate2str (ScrState is));*)
1.37 - astep_up ys iss) (*TODO 5.9.00: env ?*)
1.38 + ((*tracing("### ass_up Abs: is=");
1.39 + tracing(istate2str (ScrState is));*)
1.40 + astep_up ys iss) (*TODO 5.9.00: env ?*)
1.41
1.42 | ass_up ys (iss as (is,_)) (Const ("HOL.Let",_) $ e $ (Abs (i,T,b)))=
1.43 - ((*tracing("### ass_up Let $ e $ Abs: is=");
1.44 - tracing(istate2str (ScrState is));*)
1.45 - astep_up ys iss) (*TODO 5.9.00: env ?*)
1.46 + ((*tracing("### ass_up Let $ e $ Abs: is=");
1.47 + tracing(istate2str (ScrState is));*)
1.48 + astep_up ys iss) (*TODO 5.9.00: env ?*)
1.49
1.50 - (* val (ysa, iss, (Const ("Script.Seq",_) $ _ $ _ $ _)) =
1.51 - (ys, ((E,up,a,v,S,b),ss), (go up sc));
1.52 - *)
1.53 | ass_up ysa iss (Const ("Script.Seq",_) $ _ $ _ $ _) =
1.54 - astep_up ysa iss (*all has been done in (*2*) below*)
1.55 + astep_up ysa iss (*all has been done in (*2*) below*)
1.56
1.57 | ass_up ysa iss (Const ("Script.Seq",_) $ _ $ _) =
1.58 - (* val (ysa, iss, (Const ("Script.Seq",_) $ _ $ _)) =
1.59 - (ys, ((E,up,a,v,S,b),ss), (go up sc));
1.60 - *)
1.61 - astep_up ysa iss (*2*: comes from e2*)
1.62 + astep_up ysa iss (*2*: comes from e2*)
1.63
1.64 | ass_up (ysa as (y,s,Script sc,d)) (is as (E,l,a,v,S,b),ss)
1.65 (Const ("Script.Seq",_) $ _ ) = (*2*: comes from e1, goes to e2*)
2.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Wed Jul 20 13:05:48 2011 +0200
2.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Wed Jul 20 14:55:29 2011 +0200
2.3 @@ -1103,7 +1103,7 @@
2.4 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
2.5 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
2.6 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
2.7 - " in Check_elementwise L_LL {(v_v::real). Assumptions} )"
2.8 + " in Check_elementwise L_L {(v_v::real). Assumptions} )"
2.9 ));
2.10 *}
2.11 ML{*
3.1 --- a/test/Tools/isac/Frontend/interface.sml Wed Jul 20 13:05:48 2011 +0200
3.2 +++ b/test/Tools/isac/Frontend/interface.sml Wed Jul 20 14:55:29 2011 +0200
3.3 @@ -581,20 +581,219 @@
3.4 states:=[];
3.5 CalcTree
3.6 [(["equality ((5*x)/(x - 2) - x/(x+2)=(4::real))", "solveFor x","solutions L"],
3.7 - ("RatEq",
3.8 + ("RatEq", ["univariate","equation"], ["no_met"]))];
3.9 + Iterator 1;
3.10 + moveActiveRoot 1;
3.11 + fetchProposedTactic 1;
3.12
3.13 - val (Form f, tac, asms) = pt_extract (pt, p);
3.14 - if term2str f = "[x = 1]" andalso p = ([], Res) then () else
3.15 - error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl 1";
3.16 + setNextTactic 1 (Model_Problem);
3.17 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.18
3.19 + setNextTactic 1 (Specify_Theory "RatEq");
3.20 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.21 + setNextTactic 1 (Specify_Problem ["rational","univariate","equation"]);
3.22 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.23 + setNextTactic 1 (Specify_Method ["RatEq","solve_rat_equation"]);
3.24 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.25 + setNextTactic 1 (Apply_Method ["RatEq","solve_rat_equation"]);
3.26 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.27 + setNextTactic 1 (Rewrite_Set "RatEq_simplify");
3.28 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.29 + setNextTactic 1 (Rewrite_Set "norm_Rational");
3.30 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.31 + setNextTactic 1 (Rewrite_Set "RatEq_eliminate");
3.32 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.33 + (* __________ for "12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2)"*)
3.34 + setNextTactic 1 (Subproblem ("PolyEq", ["normalize","polynomial",
3.35 + "univariate","equation"]));
3.36 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.37 + setNextTactic 1 (Model_Problem );
3.38 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.39 + setNextTactic 1 (Specify_Theory "PolyEq");
3.40 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.41 + setNextTactic 1 (Specify_Problem ["normalize","polynomial",
3.42 + "univariate","equation"]);
3.43 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.44 + setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
3.45 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.46 + setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);
3.47 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.48 + setNextTactic 1 (Rewrite ("all_left",""));
3.49 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.50 + setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "make_ratpoly_in"));
3.51 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.52 + (* __________ for "16 + 12 * x = 0"*)
3.53 + setNextTactic 1 (Subproblem ("PolyEq",
3.54 + ["degree_1","polynomial","univariate","equation"]));
3.55 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.56 + setNextTactic 1 (Model_Problem );
3.57 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.58 + setNextTactic 1 (Specify_Theory "PolyEq");
3.59 + (*------------- some trials in the problem-hierarchy ---------------*)
3.60 + setNextTactic 1 (Specify_Problem ["linear","univariate","equation"]);
3.61 + autoCalculate 1 (Step 1); fetchProposedTactic 1; (*<ERROR> helpless </ERROR> !!!*)
3.62 + setNextTactic 1 (Refine_Problem ["univariate","equation"]);
3.63 + (*------------------------------------------------------------------*)
3.64 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.65 + setNextTactic 1 (Specify_Method ["PolyEq","solve_d1_polyeq_equation"]);
3.66 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.67 + setNextTactic 1 (Apply_Method ["PolyEq","solve_d1_polyeq_equation"]);
3.68 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.69 + setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "d1_polyeq_simplify"));
3.70 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.71 + setNextTactic 1 (Rewrite_Set "polyeq_simplify");
3.72 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.73 + (*==================================================================*)
3.74 + setNextTactic 1 Or_to_List;
3.75 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.76 +(* setNextTactic 1 (Check_elementwise "Assumptions");
3.77 + WAS: exception Match raised (line 1218 of ".../script.sml")*)
3.78 +"~~~~~ fun setNextTactic, args:"; val ((cI:calcID), tac) = (1, (Check_elementwise "Assumptions"));
3.79 +val ((pt, _), _) = get_calc cI;
3.80 +val ip = get_pos cI 1;
3.81 +(*locatetac tac (pt, ip) WAS: exception Match raised (line 1218 of ".../script.sml")*)
3.82 +"~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, ip));
3.83 +val (mI,m) = mk_tac'_ tac;
3.84 +val Appl m = applicable_in p pt m;
3.85 +member op = specsteps mI (*false*);
3.86 +(* loc_solve_ (mI,m) ptp WAS: exception Match raised (line 1218 of ".../script.sml")*)
3.87 +"~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = ((mI,m), ptp);
3.88 +(*solve m (pt, pos); WAS: exception Match raised (line 1218 of ".../script.sml")*)
3.89 +"~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
3.90 +e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*);
3.91 + val thy' = get_obj g_domID pt (par_pblobj pt p);
3.92 + val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
3.93 + val d = e_rls;
3.94 +(*locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is;
3.95 + WAS: exception Match raised (line 1218 of "isabisac/src/Tools/isac/Interpret/script.sml"*)
3.96 +"~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ptree * pos'),
3.97 + (scr as Script (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) =
3.98 + ((thy',srls), m ,(pt,(p,p_)) ,(sc,d) ,is); (* locate_gen 2nd pattern *)
3.99 +val thy = assoc_thy thy';
3.100 +l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*false*);
3.101 +(*WAS val NasApp _ =(astep_up (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) )
3.102 + ... Assoc ... is correct*)
3.103 +"~~~~~ and astep_up, args:"; val ((ys as (_,_,Script sc,_)), ((E,l,a,v,S,b),ss)) =
3.104 + ((thy',srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]));
3.105 +1 < length l (*true*);
3.106 +val up = drop_last l;
3.107 + term2str (go up sc);
3.108 + (go up sc);
3.109 +(*WAS val NasNap _ = ass_up ys ((E,up,a,v,S,b),ss) (go up sc)
3.110 + ... ???? ... is correct*)
3.111 +"~~~~~ fun ass_up, args:"; val ((ys as (y,s,Script sc,d)), (is as (E,l,a,v,S,b),ss),
3.112 + (Const ("HOL.Let",_) $ _)) = (ys, ((E,up,a,v,S,b),ss), (go up sc));
3.113 + val l = drop_last l; (*comes from e, goes to Abs*)
3.114 + val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go l sc;
3.115 + val i = mk_Free (i, T);
3.116 + val E = upd_env E (i, v);
3.117 +(*Type error ...: Can't unify _a to pos * pos_ (Incompatible types)*)
3.118 +val [(tac_, mout, ptree, pos', xxx)] = ss;
3.119 +val ss = [(tac_, mout, ptree, pos', []:(pos * pos_) list)];
3.120 +(*WAS val NasApp iss = assy (((y,s),d),Aundef) ((E, l@[R,D], a,v,S,b),ss) body
3.121 + ... Assoc ... is correct*)
3.122 +"~~~~~ fun assy, args:"; val ((((thy',sr),d),ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) =
3.123 + ((((y,s),d),Aundef), ((E, l@[R,D], a,v,S,b),ss), body);
3.124 +val (a', STac stac) = handle_leaf "locate" thy' sr E a v t
3.125 + val ctxt = get_ctxt pt (p,p_)
3.126 + val p' = lev_on p : pos;
3.127 +(* WAS val NotAss = assod pt d m stac
3.128 + ... Ass ... is correct*)
3.129 +"~~~~~ fun assod, args:"; val (pt, _, (m as Check_elementwise' (consts,_,(consts_chkd,_))),
3.130 + (Const ("Script.Check'_elementwise",_) $ consts' $ _)) = (pt, d, m, stac);
3.131 +consts = consts' (*WAS false*);
3.132 +(*========== inhibit exn 110719 ================================================
3.133 +========== inhibit exn 110719 =============================================*)
3.134 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.135 + setNextTactic 1 (Check_Postcond ["degree_1","polynomial",
3.136 + "univariate","equation"]);
3.137 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.138 + setNextTactic 1 (Check_Postcond ["normalize","polynomial",
3.139 + "univariate","equation"]);
3.140 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.141
3.142 -"--------- rat-eq + subpbl: no_met, NO solution dropped -";
3.143 -"--------- rat-eq + subpbl: no_met, NO solution dropped -";
3.144 -"--------- rat-eq + subpbl: no_met, NO solution dropped -";
3.145 - states:=[];
3.146 +(*** exception TYPE raised (line 460 of "old_goals.ML"):
3.147 +*** Type error in application: Incompatible operand type
3.148 +***
3.149 +*** Operator: equality :: bool => una
3.150 +*** Operand: [((x * 3) = -4)] :: bool list
3.151 +***
3.152 +*** bool => una
3.153 +*** bool list
3.154 +*** equality
3.155 +*** [x * 3 = -4]*)
3.156 +
3.157 +(*========== inhibit exn 110719 ================================================
3.158 + setNextTactic 1 (Check_elementwise "Assumptions");
3.159 +============ inhibit exn 110719 ==============================================*)
3.160 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.161 + setNextTactic 1 (Check_Postcond ["rational","univariate","equation"]);
3.162 + val (ptp,_) = get_calc 1;
3.163 + val (Form t,_,_) = pt_extract ptp;
3.164 + if get_pos 1 1 = ([], Res) andalso term2str t = "[x = -4 / 3]" then ()
3.165 + else writeln "FE-inteface.sml: diff.behav. in rat-eq + subpbl: no_met, NO ..";
3.166 +
3.167 +
3.168 +"--------- tryMatchProblem, tryRefineProblem ------------";
3.169 +"--------- tryMatchProblem, tryRefineProblem ------------";
3.170 +"--------- tryMatchProblem, tryRefineProblem ------------";
3.171 +(*{\bf\UC{Having \isac{} Refine the Problem
3.172 + * Automatically}\label{SPECIFY:refine-auto}\\} test match and refine with
3.173 + * x^^^2 + 4*x + 5 = 2
3.174 +see isac.bridge.TestSpecify#testMatchRefine*)
3.175 + DEconstrCalcTree 1;
3.176 CalcTree
3.177 - [(["equality ((5*x)/(x - 2) - x/(x+2)=(4::real))", "solveFor x","solutions L"],
3.178 - ("RatEq", ["univariate","equation"], ["no_met"]))];
3.179 + [(["equality (x^2 + 4*x + 5 = (2::real))", "solveFor x","solutions L"],
3.180 + ("Isac",
3.181 + ["univariate","equation"],
3.182 + ["no_met"]))];
3.183 + Iterator 1;
3.184 + moveActiveRoot 1;
3.185 +
3.186 + fetchProposedTactic 1;
3.187 + setNextTactic 1 (Model_Problem );
3.188 + (*..this tactic should be done 'tacitly', too !*)
3.189 +
3.190 +(*
3.191 +autoCalculate 1 CompleteCalcHead;
3.192 +checkContext 1 ([],Pbl) "pbl_equ_univ";
3.193 +checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
3.194 +*)
3.195 +
3.196 + autoCalculate 1 (Step 1);
3.197 +
3.198 + fetchProposedTactic 1;
3.199 + setNextTactic 1 (Add_Given "equality (x ^^^ 2 + 4 * x + 5 = (2::real))");
3.200 + autoCalculate 1 (Step 1);
3.201 +
3.202 + "--------- we go into the ProblemBrowser (_NO_ pblID selected) -";
3.203 +initContext 1 Pbl_ ([],Pbl);
3.204 +initContext 1 Met_ ([],Pbl);
3.205 +
3.206 + "--------- this match will show some incomplete items: ---------";
3.207 +checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
3.208 +checkContext 1 ([],Pbl) (kestoreID2guh Met_ ["LinEq", "solve_lineq_equation"]);
3.209 +
3.210 +
3.211 + fetchProposedTactic 1;
3.212 + setNextTactic 1 (Add_Given "solveFor x"); autoCalculate 1 (Step 1);
3.213 +
3.214 + fetchProposedTactic 1;
3.215 + setNextTactic 1 (Add_Find "solutions L"); autoCalculate 1 (Step 1);
3.216 +
3.217 + "--------- this is a matching model (all items correct): -------";
3.218 +checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
3.219 + "--------- this is a NOT matching model (some 'false': ---------";
3.220 +checkContext 1 ([],Pbl)(kestoreID2guh Pbl_["linear","univariate","equation"]);
3.221 +
3.222 + "--------- find out a matching problem: ------------------------";
3.223 + "--------- find out a matching problem (FAILING: no new pbl) ---";
3.224 + refineProblem 1([],Pbl)(pblID2guh ["linear","univariate","equation"]);
3.225 +
3.226 + "--------- find out a matching problem (SUCCESSFUL) ------------";
3.227 + refineProblem 1 ([],Pbl) (pblID2guh ["univariate","equation"]);
3.228 +
3.229 + "--------- tryMatch, tryRefine di [univariate,equation], [no_met]))]";
3.230 Iterator 1;
3.231 moveActiveRoot 1;
3.232 fetchProposedTactic 1;
3.233 @@ -727,211 +926,8 @@
3.234 *** equality
3.235 *** [x * 3 = -4]*)
3.236
3.237 + setNextTactic 1 (Check_elementwise "Assumptions");
3.238 (*========== inhibit exn 110719 ================================================
3.239 - setNextTactic 1 (Check_elementwise "Assumptions");
3.240 -============ inhibit exn 110719 ==============================================*)
3.241 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.242 - setNextTactic 1 (Check_Postcond ["rational","univariate","equation"]);
3.243 - val (ptp,_) = get_calc 1;
3.244 - val (Form t,_,_) = pt_extract ptp;
3.245 - if get_pos 1 1 = ([], Res) andalso term2str t = "[x = -4 / 3]" then ()
3.246 - else writeln "FE-inteface.sml: diff.behav. in rat-eq + subpbl: no_met, NO ..";
3.247 -
3.248 -
3.249 -"--------- tryMatchProblem, tryRefineProblem ------------";
3.250 -"--------- tryMatchProblem, tryRefineProblem ------------";
3.251 -"--------- tryMatchProblem, tryRefineProblem ------------";
3.252 -(*{\bf\UC{Having \isac{} Refine the Problem
3.253 - * Automatically}\label{SPECIFY:refine-auto}\\} test match and refine with
3.254 - * x^^^2 + 4*x + 5 = 2
3.255 -see isac.bridge.TestSpecify#testMatchRefine*)
3.256 - DEconstrCalcTree 1;
3.257 - CalcTree
3.258 - [(["equality (x^2 + 4*x + 5 = (2::real))", "solveFor x","solutions L"],
3.259 - ("Isac",
3.260 - ["univariate","equation"],
3.261 - ["no_met"]))];
3.262 - Iterator 1;
3.263 - moveActiveRoot 1;
3.264 -
3.265 - fetchProposedTactic 1;
3.266 - setNextTactic 1 (Model_Problem );
3.267 - (*..this tactic should be done 'tacitly', too !*)
3.268 -
3.269 -(*
3.270 -autoCalculate 1 CompleteCalcHead;
3.271 -checkContext 1 ([],Pbl) "pbl_equ_univ";
3.272 -checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
3.273 -*)
3.274 -
3.275 - autoCalculate 1 (Step 1);
3.276 -
3.277 - fetchProposedTactic 1;
3.278 - setNextTactic 1 (Add_Given "equality (x ^^^ 2 + 4 * x + 5 = (2::real))");
3.279 - autoCalculate 1 (Step 1);
3.280 -
3.281 - "--------- we go into the ProblemBrowser (_NO_ pblID selected) -";
3.282 -initContext 1 Pbl_ ([],Pbl);
3.283 -initContext 1 Met_ ([],Pbl);
3.284 -
3.285 - "--------- this match will show some incomplete items: ---------";
3.286 -checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
3.287 -checkContext 1 ([],Pbl) (kestoreID2guh Met_ ["LinEq", "solve_lineq_equation"]);
3.288 -
3.289 -
3.290 - fetchProposedTactic 1;
3.291 - setNextTactic 1 (Add_Given "solveFor x"); autoCalculate 1 (Step 1);
3.292 -
3.293 - fetchProposedTactic 1;
3.294 - setNextTactic 1 (Add_Find "solutions L"); autoCalculate 1 (Step 1);
3.295 -
3.296 - "--------- this is a matching model (all items correct): -------";
3.297 -checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
3.298 - "--------- this is a NOT matching model (some 'false': ---------";
3.299 -checkContext 1 ([],Pbl)(kestoreID2guh Pbl_["linear","univariate","equation"]);
3.300 -
3.301 - "--------- find out a matching problem: ------------------------";
3.302 - "--------- find out a matching problem (FAILING: no new pbl) ---";
3.303 - refineProblem 1([],Pbl)(pblID2guh ["linear","univariate","equation"]);
3.304 -
3.305 - "--------- find out a matching problem (SUCCESSFUL) ------------";
3.306 - refineProblem 1 ([],Pbl) (pblID2guh ["univariate","equation"]);
3.307 -
3.308 - "--------- tryMatch, tryRefine di ["univariate","equation"], ["no_met"]))];
3.309 - Iterator 1;
3.310 - moveActiveRoot 1;
3.311 - fetchProposedTactic 1;
3.312 -
3.313 -(*ERROR: setNextTactic 1 produces "get_calc 1 not existent"*)
3.314 - setNextTactic 1 (Model_Problem );
3.315 -autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.316 -
3.317 -(*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
3.318 - setNextTactic 1 (Add_Given "equality (5 * x / (x - 2) - x / (x + 2) = 4)");
3.319 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.320 - setNextTactic 1 (Add_Given "solveFor x");
3.321 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.322 - setNextTactic 1 (Add_Find "solutions L");
3.323 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.324 -*-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
3.325 - setNextTactic 1 (Specify_Theory "RatEq");
3.326 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.327 - setNextTactic 1 (Specify_Problem ["rational","univariate","equation"]);
3.328 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.329 - setNextTactic 1 (Specify_Method ["RatEq","solve_rat_equation"]);
3.330 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.331 - setNextTactic 1 (Apply_Method ["RatEq","solve_rat_equation"]);
3.332 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.333 - setNextTactic 1 (Rewrite_Set "RatEq_simplify");
3.334 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.335 - setNextTactic 1 (Rewrite_Set "norm_Rational");
3.336 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.337 - setNextTactic 1 (Rewrite_Set "RatEq_eliminate");
3.338 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.339 - (* __________ for "12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2)"*)
3.340 - setNextTactic 1 (Subproblem ("PolyEq", ["normalize","polynomial",
3.341 - "univariate","equation"]));
3.342 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.343 - setNextTactic 1 (Model_Problem );
3.344 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.345 -(*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
3.346 - setNextTactic 1 (Add_Given
3.347 - "equality (12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2))");
3.348 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.349 - setNextTactic 1 (Add_Given "solveFor x");
3.350 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.351 - setNextTactic 1 (Add_Find "solutions x_i");
3.352 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.353 -*-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
3.354 - setNextTactic 1 (Specify_Theory "PolyEq");
3.355 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.356 - setNextTactic 1 (Specify_Problem ["normalize","polynomial",
3.357 - "univariate","equation"]);
3.358 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.359 - setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
3.360 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.361 - setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);
3.362 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.363 - setNextTactic 1 (Rewrite ("all_left",""));
3.364 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.365 - setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "make_ratpoly_in"));
3.366 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.367 - (* __________ for "16 + 12 * x = 0"*)
3.368 - setNextTactic 1 (Subproblem ("PolyEq",
3.369 - ["degree_1","polynomial","univariate","equation"]));
3.370 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.371 - setNextTactic 1 (Model_Problem );
3.372 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.373 -(*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
3.374 - setNextTactic 1 (Add_Given
3.375 - "equality (16 + 12 * x = 0)");
3.376 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.377 - setNextTactic 1 (Add_Given "solveFor x");
3.378 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.379 - setNextTactic 1 (Add_Find "solutions x_i");
3.380 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.381 -*-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
3.382 - setNextTactic 1 (Specify_Theory "PolyEq");
3.383 - (*------------- some trials in the problem-hierarchy ---------------*)
3.384 - setNextTactic 1 (Specify_Problem ["linear","univariate","equation"]);
3.385 - autoCalculate 1 (Step 1); fetchProposedTactic 1; (*<ERROR> helpless </ERROR> !!!*)
3.386 - setNextTactic 1 (Refine_Problem ["univariate","equation"]);
3.387 - (*------------------------------------------------------------------*)
3.388 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.389 - setNextTactic 1 (Specify_Method ["PolyEq","solve_d1_polyeq_equation"]);
3.390 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.391 - setNextTactic 1 (Apply_Method ["PolyEq","solve_d1_polyeq_equation"]);
3.392 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.393 - setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "d1_polyeq_simplify"));
3.394 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.395 - setNextTactic 1 (Rewrite_Set "polyeq_simplify");
3.396 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.397 - (*==================================================================*)
3.398 - setNextTactic 1 Or_to_List;
3.399 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.400 -(* setNextTactic 1 (Check_elementwise "Assumptions");
3.401 - WAS: exception Match raised (line 1218 of ".../script.sml")*)
3.402 -"~~~~~ fun setNextTactic, args:"; val ((cI:calcID), tac) = (1, (Check_elementwise "Assumptions"));
3.403 -val ((pt, _), _) = get_calc cI;
3.404 -val ip = get_pos cI 1;
3.405 -(*locatetac tac (pt, ip) WAS: exception Match raised (line 1218 of ".../script.sml")*)
3.406 -"~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, ip));
3.407 -val (mI,m) = mk_tac'_ tac;
3.408 -val Appl m = applicable_in p pt m;
3.409 -member op = specsteps mI (*false*);
3.410 -(* loc_solve_ (mI,m) ptp WAS: exception Match raised (line 1218 of ".../script.sml")*)
3.411 -"~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = ((mI,m), ptp);
3.412 -(*solve m (pt, pos); WAS: exception Match raised (line 1218 of ".../script.sml")*)
3.413 -"~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
3.414 -e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*);
3.415 - val thy' = get_obj g_domID pt (par_pblobj pt p);
3.416 - val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
3.417 - val d = e_rls;
3.418 -(*locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is;
3.419 - WAS: exception Match raised (line 1218 of ".../script.sml"*)
3.420 -(*========== inhibit exn 110719 ================================================
3.421 -========== inhibit exn 110719 XXX=============================================*)
3.422 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.423 - setNextTactic 1 (Check_Postcond ["degree_1","polynomial",
3.424 - "univariate","equation"]);
3.425 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.426 - setNextTactic 1 (Check_Postcond ["normalize","polynomial",
3.427 - "univariate","equation"]);
3.428 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.429 -
3.430 -(*** exception TYPE raised (line 460 of "old_goals.ML"):
3.431 -*** Type error in application: Incompatible operand type
3.432 -***
3.433 -*** Operator: equality :: bool => una
3.434 -*** Operand: [((x * 3) = -4)] :: bool list
3.435 -***
3.436 -*** bool => una
3.437 -*** bool list
3.438 -*** equality
3.439 -*** [x * 3 = -4]*)
3.440 -
3.441 -(*========== inhibit exn 110719 ================================================
3.442 - setNextTactic 1 (Check_elementwise "Assumptions");
3.443 ============ inhibit exn 110719 ==============================================*)
3.444 autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.445 setNextTactic 1 (Check_Postcond ["rational","univariate","equation"]);
4.1 --- a/test/Tools/isac/Test_Some.thy Wed Jul 20 13:05:48 2011 +0200
4.2 +++ b/test/Tools/isac/Test_Some.thy Wed Jul 20 14:55:29 2011 +0200
4.3 @@ -7,177 +7,13 @@
4.4
4.5 ML{* writeln "**** run the test ***************************************" *}
4.6
4.7 -use"../../../test/Tools/isac/Frontend/interface.sml"
4.8 +use"../../../test/Tools/isac/Frontend/interface.sml"
4.9
4.10 ML{*
4.11
4.12
4.13 -"--------- rat-eq + subpbl: no_met, NO solution dropped -";
4.14 - states:=[];
4.15 - CalcTree
4.16 - [(["equality ((5*x)/(x - 2) - x/(x+2)=(4::real))", "solveFor x","solutions L"],
4.17 - ("RatEq", ["univariate","equation"], ["no_met"]))];
4.18 - Iterator 1;
4.19 - moveActiveRoot 1;
4.20 - fetchProposedTactic 1;
4.21 -
4.22 -(*ERROR: setNextTactic 1 produces "get_calc 1 not existent"*)
4.23 - setNextTactic 1 (Model_Problem );
4.24 -autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.25 -
4.26 -(*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
4.27 - setNextTactic 1 (Add_Given "equality (5 * x / (x - 2) - x / (x + 2) = 4)");
4.28 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.29 - setNextTactic 1 (Add_Given "solveFor x");
4.30 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.31 - setNextTactic 1 (Add_Find "solutions L");
4.32 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.33 -*-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
4.34 - setNextTactic 1 (Specify_Theory "RatEq");
4.35 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.36 - setNextTactic 1 (Specify_Problem ["rational","univariate","equation"]);
4.37 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.38 - setNextTactic 1 (Specify_Method ["RatEq","solve_rat_equation"]);
4.39 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.40 - setNextTactic 1 (Apply_Method ["RatEq","solve_rat_equation"]);
4.41 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.42 - setNextTactic 1 (Rewrite_Set "RatEq_simplify");
4.43 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.44 - setNextTactic 1 (Rewrite_Set "norm_Rational");
4.45 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.46 - setNextTactic 1 (Rewrite_Set "RatEq_eliminate");
4.47 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.48 - (* __________ for "12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2)"*)
4.49 - setNextTactic 1 (Subproblem ("PolyEq", ["normalize","polynomial",
4.50 - "univariate","equation"]));
4.51 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.52 - setNextTactic 1 (Model_Problem );
4.53 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.54 -(*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
4.55 - setNextTactic 1 (Add_Given
4.56 - "equality (12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2))");
4.57 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.58 - setNextTactic 1 (Add_Given "solveFor x");
4.59 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.60 - setNextTactic 1 (Add_Find "solutions x_i");
4.61 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.62 -*-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
4.63 - setNextTactic 1 (Specify_Theory "PolyEq");
4.64 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.65 - setNextTactic 1 (Specify_Problem ["normalize","polynomial",
4.66 - "univariate","equation"]);
4.67 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.68 - setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
4.69 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.70 - setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);
4.71 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.72 - setNextTactic 1 (Rewrite ("all_left",""));
4.73 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.74 - setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "make_ratpoly_in"));
4.75 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.76 - (* __________ for "16 + 12 * x = 0"*)
4.77 - setNextTactic 1 (Subproblem ("PolyEq",
4.78 - ["degree_1","polynomial","univariate","equation"]));
4.79 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.80 - setNextTactic 1 (Model_Problem );
4.81 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.82 -(*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
4.83 - setNextTactic 1 (Add_Given
4.84 - "equality (16 + 12 * x = 0)");
4.85 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.86 - setNextTactic 1 (Add_Given "solveFor x");
4.87 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.88 - setNextTactic 1 (Add_Find "solutions x_i");
4.89 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.90 -*-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
4.91 - setNextTactic 1 (Specify_Theory "PolyEq");
4.92 - (*------------- some trials in the problem-hierarchy ---------------*)
4.93 - setNextTactic 1 (Specify_Problem ["linear","univariate","equation"]);
4.94 - autoCalculate 1 (Step 1); fetchProposedTactic 1; (*<ERROR> helpless </ERROR> !!!*)
4.95 - setNextTactic 1 (Refine_Problem ["univariate","equation"]);
4.96 - (*------------------------------------------------------------------*)
4.97 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.98 - setNextTactic 1 (Specify_Method ["PolyEq","solve_d1_polyeq_equation"]);
4.99 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.100 - setNextTactic 1 (Apply_Method ["PolyEq","solve_d1_polyeq_equation"]);
4.101 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.102 - setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "d1_polyeq_simplify"));
4.103 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.104 - setNextTactic 1 (Rewrite_Set "polyeq_simplify");
4.105 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.106 - (*==================================================================*)
4.107 - setNextTactic 1 Or_to_List;
4.108 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.109 -(* setNextTactic 1 (Check_elementwise "Assumptions");
4.110 - WAS: exception Match raised (line 1218 of ".../script.sml")*)
4.111 -"~~~~~ fun setNextTactic, args:"; val ((cI:calcID), tac) = (1, (Check_elementwise "Assumptions"));
4.112 -val ((pt, _), _) = get_calc cI;
4.113 -val ip = get_pos cI 1;
4.114 -(*locatetac tac (pt, ip) WAS: exception Match raised (line 1218 of ".../script.sml")*)
4.115 -"~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, ip));
4.116 -val (mI,m) = mk_tac'_ tac;
4.117 -val Appl m = applicable_in p pt m;
4.118 -member op = specsteps mI (*false*);
4.119 -(* loc_solve_ (mI,m) ptp WAS: exception Match raised (line 1218 of ".../script.sml")*)
4.120 -"~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = ((mI,m), ptp);
4.121 -(*solve m (pt, pos); WAS: exception Match raised (line 1218 of ".../script.sml")*)
4.122 -"~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
4.123 -e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*);
4.124 - val thy' = get_obj g_domID pt (par_pblobj pt p);
4.125 - val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
4.126 - val d = e_rls;
4.127 *}
4.128 ML{*
4.129 -(*locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is;
4.130 - WAS: exception Match raised (line 1218 of "isabisac/src/Tools/isac/Interpret/script.sml"*)
4.131 -"~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ptree * pos'),
4.132 - (scr as Script (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) =
4.133 - ((thy',srls), m ,(pt,(p,p_)) ,(sc,d) ,is); (* locate_gen 2nd pattern *)
4.134 -val thy = assoc_thy thy';
4.135 -
4.136 -*}
4.137 -ML{*
4.138 -*}
4.139 -ML{*
4.140 -(*case (astep_up (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) )
4.141 - of
4.142 - (Assoc (iss as (is as (_,_,_,_,_,bb), ss as ((m',f',pt',p',c')::_))))
4.143 - =>
4.144 - "nix";*)
4.145 -(*ERROR:
4.146 - Value identifier (c') has not been referenced.
4.147 - Value identifier (p') has not been referenced.
4.148 - Value identifier (pt') has not been referenced.
4.149 - Value identifier (f') has not been referenced.
4.150 - Value identifier (m') has not been referenced.
4.151 - Value identifier (ss) has not been referenced.
4.152 - Value identifier (bb) has not been referenced.
4.153 - Value identifier (is) has not been referenced.
4.154 - Value identifier (iss) has not been referenced.
4.155 - Matches are not exhaustive.
4.156 - exception Match raised*)
4.157 -*}
4.158 -ML{*
4.159 -(*case (astep_up (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) )
4.160 - of
4.161 - (Assoc (iss as (is as (_,_,_,_,_,bb), ss as ((m',f',pt',p',c')::_))))
4.162 - => (iss,is,bb,ss,m',f',pt',p',c');*)
4.163 -(*ERROR:
4.164 - Matches are not exhaustive.
4.165 - exception Match raised*)
4.166 -*}
4.167 -ML{*
4.168 -*}
4.169 -ML{*
4.170 -*}
4.171 -ML{*
4.172 -(*========== inhibit exn 110719 ================================================
4.173 -========== inhibit exn 110719 XXX=============================================*)
4.174 -
4.175 -
4.176 -*}
4.177 -ML{*
4.178 -
4.179 *}
4.180 ML{*
4.181 *}