1.1 --- a/test/Tools/isac/Test_Isac.thy Wed Oct 19 15:39:15 2022 +0200
1.2 +++ b/test/Tools/isac/Test_Isac.thy Thu Oct 20 10:23:38 2022 +0200
1.3 @@ -91,7 +91,7 @@
1.4 ML \<open>
1.5 open Kernel;
1.6 open Math_Engine;
1.7 - open Test_Code; CalcTreeTEST;
1.8 + open Test_Code; Test_Code.init_calc @{context};
1.9 open LItool; arguments_from_model;
1.10 open Sub_Problem;
1.11 open Fetch_Tacs;
1.12 @@ -320,6 +320,1632 @@
1.13 ML \<open>
1.14 \<close> ML \<open>
1.15 \<close> ML \<open>
1.16 +(* Title: tests the interface of isac's SML-kernel in accordance to
1.17 + java-tests/isac.bridge.
1.18 + Author: Walther Neuper
1.19 + (c) copyright due to lincense terms.
1.20 +
1.21 +Tests the interface of isac's SML-kernel in accordance to java-tests/isac.bridge.
1.22 +Some tests are outcommented since "eliminate ThmC.numerals_to_Free";
1.23 +these are considered irrelevant for Isabelle/Isac.
1.24 +
1.25 +WN050707 ... if true, the test ist marked with a \label referring
1.26 +to the same UC in isac-docu.tex as the JUnit testcase.
1.27 +WN120210?not ME: added some labels, which are not among the above,
1.28 +repaired lost \label (s).
1.29 +
1.30 +theory Test_Some imports Isac.Build_Thydata begin
1.31 +ML {* KEStore_Elems.set_ref_thy @{theory};
1.32 + fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*) *}
1.33 +ML_file "Frontend/use-cases.sml"
1.34 +*)
1.35 +
1.36 +"--------------------------------------------------------";
1.37 +"table of contents --------------------------------------";
1.38 +"--------------------------------------------------------";
1.39 +"within struct ------------------------------------------";
1.40 +"--------------------------------------------------------";
1.41 +"--------- encode ^ -> ^^ ------------------------------";
1.42 +"--------------------------------------------------------";
1.43 +"exported from struct -----------------------------------";
1.44 +"--------------------------------------------------------";
1.45 +(*"--------- empty rootpbl --------------------------------";*)
1.46 +"--------- solve_linear as rootpbl FE -------------------";
1.47 +"--------- inspect the CalcTree @{context} No.1 with Iterator No.2 -";
1.48 +"--------- miniscript with mini-subpbl ------------------";
1.49 +"--------- mini-subpbl AUTOCALCULATE Steps 1 ------------";
1.50 +"--------- solve_linear as rootpbl AUTO CompleteCalc ----";
1.51 +"--------- solve_linear as rootpbl AUTO CompleteHead/Eval ";
1.52 +"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
1.53 +"--------- mini-subpbl AUTO CompleteCalcHead ------------";
1.54 +"--------- solve_linear as rootpbl AUTO CompleteModel ---";
1.55 +"--------- setContext..Thy ------------------------------";
1.56 +"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
1.57 +"--------- rat-eq + subpbl: no_met, NO solution dropped - WITH fun me IN test/../solve.sml";
1.58 +"--------- tryMatchProblem, tryRefineProblem ------------";
1.59 +"--------- modifyCalcHead, resetCalcHead, modelProblem --";
1.60 +"--------- maximum-example, UC: Modeling an example -----";
1.61 +"--------- solve_linear from pbl-hierarchy --------------";
1.62 +"--------- solve_linear as in an algebra system (CAS)----";
1.63 +"--------- interSteps: on 'miniscript with mini-subpbl' -";
1.64 +"--------- getTactic, fetchApplicableTactics ------------";
1.65 +"--------- getAssumptions, getAccumulatedAsms -----------";
1.66 +"--------- arbitrary combinations of steps --------------";
1.67 +"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
1.68 +"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
1.69 +"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
1.70 +"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
1.71 +"--------- replaceFormula {SOL:MAN:FOR:replace} right----";
1.72 +"--------- replaceFormula {SOL:MAN:FOR:replace} other----";
1.73 +"--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
1.74 +"--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
1.75 +"--------- UC errpat chain-rule-diff-both, fillpat by input ------";
1.76 +"--------- UC errpat add-fraction, fillpat by input --------------";
1.77 +"--------- UC errpat, fillpat step to Rewrite --------------------";
1.78 +"--------- UC errpat, fillpat step to Rewrite_Set ----------------";
1.79 +"--------------------------------------------------------";
1.80 +
1.81 +"within struct ---------------------------------------------------";
1.82 +"within struct ---------------------------------------------------";
1.83 +"within struct ---------------------------------------------------";
1.84 +(*==================================================================
1.85 +
1.86 +==================================================================*)
1.87 +"exported from struct --------------------------------------------";
1.88 +"exported from struct --------------------------------------------";
1.89 +"exported from struct --------------------------------------------";
1.90 +
1.91 +
1.92 +(*------------ set at startup of the Kernel ----------------------*)
1.93 +States.reset (); (*resets all state information in Kernel *)
1.94 +(*----------------------------------------------------------------*)
1.95 +
1.96 +(*---------------------------------------------------- postpone to Outer_Syntax..Example -----
1.97 +"--------- empty rootpbl --------------------------------";
1.98 +"--------- empty rootpbl --------------------------------";
1.99 +"--------- empty rootpbl --------------------------------";
1.100 + CalcTree @{context} [([], ("", [], []))];
1.101 + Iterator 1;
1.102 + moveActiveRoot 1;
1.103 + refFormula 1 (States.get_pos 1 1);
1.104 +(*WN.040222: stoert das sehr, dass ThyC.id_empty etc. statt leer kommt ???*)
1.105 +DEconstrCalcTree 1;
1.106 +------------------------------------------------------ postpone to Outer_Syntax..Example -----*)
1.107 +
1.108 +"--------- solve_linear as rootpbl FE -------------------";
1.109 +"--------- solve_linear as rootpbl FE -------------------";
1.110 +"--------- solve_linear as rootpbl FE -------------------";
1.111 +States.reset ();
1.112 +
1.113 + CalcTree @{context} (*start of calculation, return No.1*)
1.114 + [(["equality (1+- 1*2+x=(0::real))", "solveFor x", "solutions L"],
1.115 + ("Test",
1.116 + ["LINEAR", "univariate", "equation", "test"],
1.117 + ["Test", "solve_linear"]))];
1.118 + Iterator 1; (*create an active Iterator on CalcTree @{context} No.1*)
1.119 +
1.120 + moveActiveRoot 1;(*sets the CalcIterator No.1 at the root of CalcTree @{context} No.1*);
1.121 + refFormula 1 (States.get_pos 1 1) (*gets CalcHead; model is still empty*);
1.122 +
1.123 +
1.124 +(*1*) fetchProposedTactic 1 (*by using Iterator No.1*);
1.125 + setNextTactic 1 (Model_Problem); (*by using Iterator No.1*)
1.126 + autoCalculate 1 (Steps 1);
1.127 + refFormula 1 (States.get_pos 1 1) (*model contains descriptions for all items*);
1.128 + autoCalculate 1 (Steps 1);
1.129 +(*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
1.130 +(*2*) fetchProposedTactic 1;
1.131 + setNextTactic 1 (Add_Given "equality (1 + - 1 * 2 + x = 0)");
1.132 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1); (*equality added*);
1.133 +
1.134 +(*3*) fetchProposedTactic 1;
1.135 + setNextTactic 1 (Add_Given "solveFor x");
1.136 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.137 +
1.138 +(*4*) fetchProposedTactic 1;
1.139 + setNextTactic 1 (Add_Find "solutions L");
1.140 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.141 +
1.142 +(*5*) fetchProposedTactic 1;
1.143 + setNextTactic 1 (Specify_Theory "Test");
1.144 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.145 +*-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
1.146 +
1.147 +(*6*) fetchProposedTactic 1;
1.148 + setNextTactic 1 (Specify_Problem ["LINEAR", "univariate", "equation", "test"]);
1.149 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.150 +(*-------------------------------------------------------------------------*)
1.151 +(*7*) fetchProposedTactic 1;
1.152 + val (ptp as (pt,p), tacis) = States.get_calc 1; States.get_pos 1 1;
1.153 +
1.154 + setNextTactic 1 (Specify_Method ["Test", "solve_linear"]);
1.155 + val (ptp as (pt,p), tacis) = States.get_calc 1; States.get_pos 1 1;
1.156 +
1.157 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.158 + val (ptp as (pt,p), tacis) = States.get_calc 1; States.get_pos 1 1;
1.159 +
1.160 +(*-------------------------------------------------------------------------*)
1.161 +(*8*) fetchProposedTactic 1;
1.162 + val (ptp as (pt,p), tacis) = States.get_calc 1; States.get_pos 1 1;
1.163 +
1.164 +(*8*) setNextTactic 1 (Apply_Method ["Test", "solve_linear"]);
1.165 + (*ERROR.110620 <SETNEXTTACTIC>..<MESSAGE> end-of-calculation*)
1.166 + val (ptp as (pt,p), tacis) = States.get_calc 1; States.get_pos 1 1;
1.167 + SpecificationC.is_complete ptp;
1.168 + References.are_complete ptp;
1.169 +
1.170 +(*8*) autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1); (*<---------------------- orig. test code*)
1.171 +
1.172 + val (ptp as (pt,p), tacis) = States.get_calc 1; States.get_pos 1 1; (*<---------------------- orig. test code*)
1.173 +(*+isa=REP*) if p = ([1], Frm) andalso UnparseC.term (get_obj g_form pt [1]) = "1 + - 1 * 2 + x = 0"
1.174 +andalso Istate.string_of (get_istate_LI pt p)
1.175 + = "Pstate ([\"\n(e_e, 1 + - 1 * 2 + x = 0)\", \"\n(v_v, x)\"], [], empty, NONE, \n??.empty, ORundef, false, true)"
1.176 +then () else error "refFormula = 1 + - 1 * 2 + x = 0 changed";
1.177 +(*-------------------------------------------------------------------------*)
1.178 +
1.179 +(*9*) fetchProposedTactic 1; (*<----------------------------------------------------- orig. test code*)
1.180 +(*+\\------------------------------------------ isa == REP -----------------------------------//* )
1.181 +(*+//========================================== isa <> REP (1) ===============================\\*)
1.182 +(*9*) setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "isolate_bdv")); ( *<------- orig. test code*)
1.183 +
1.184 +"~~~~~ fun setNextTactic , args:"; val (cI, tac) = (1, (Rewrite_Set_Inst (["(''bdv'',x)"], "isolate_bdv")));
1.185 + val ((pt'''''_', _), _) = States.get_calc cI
1.186 + val ip'''''_' = States.get_pos cI 1;
1.187 +
1.188 + val xxxxx_x(*"ok", (tacis, _, _)*) = (*case*) Step.by_tactic tac (pt'''''_', ip'''''_') (*of*);
1.189 +(*+isa+REP*)val ("ok", ( [ (Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv"),
1.190 + Rewrite_Set_Inst' _, (pos', (istate, ctxt))) ] , _, cstate)) = xxxxx_x;
1.191 +
1.192 +(*//******************* Step.by_tactic returns tac_ + istate + cstate *****************************\\*)
1.193 +Step.by_tactic : Tactic.input -> state -> string * (State_Steps.T * pos' list * state);
1.194 +if Istate.string_of istate
1.195 + = "Pstate ([\"\n(e_e, 1 + - 1 * 2 + x = 0)\", \"\n(v_v, x)\"], [R, L, R, L, R, L, R], empty, SOME e_e, \nx = 0 + - 1 * (1 + - 1 * 2), ORundef, true, true)"
1.196 +then () else error "from Step.by_tactic return --- changed 1";
1.197 +
1.198 +if Istate.string_of (get_istate_LI (fst cstate) (snd cstate))
1.199 + = "Pstate ([\"\n(e_e, 1 + - 1 * 2 + x = 0)\", \"\n(v_v, x)\"], [R, L, R, L, R, L, R], empty, SOME e_e, \nx = 0 + - 1 * (1 + - 1 * 2), ORundef, true, true)"
1.200 +then () else error "from Step.by_tactic return --- changed 2";
1.201 +(*\\******************* Step.by_tactic returns tac_ + istate + cstate *****************************//*)
1.202 +
1.203 +"~~~~~ fun Step.by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt'''''_', ip'''''_'));
1.204 + val Applicable.Yes m = (*case*) Step.check tac (pt, p) (*of*);
1.205 + (*if*) Tactic.for_specify' m; (*false*)
1.206 +
1.207 +Step_Solve.by_tactic m (pt, p);
1.208 +"~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, p));
1.209 + (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p); (*else*)
1.210 + val thy' = get_obj g_domID pt (par_pblobj pt p);
1.211 + val (is, sc) = LItool.resume_prog (p,p_) pt;
1.212 + val Safe_Step (istate, _, tac) =
1.213 + (*case*) LI.locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*);
1.214 +
1.215 +(*+*)Safe_Step: Istate.T * Proof.context * Tactic.T -> input_tactic_result;
1.216 +(********************* locate_input_tactic returns cstate * istate * Proof.context *************)
1.217 +(*+*)if Istate.string_of istate
1.218 +(*+isa*) = "Pstate ([\"\n(e_e, 1 + - 1 * 2 + x = 0)\", \"\n(v_v, x)\"], [R, L, R, L, R, L, R], empty, SOME e_e, \nx = 0 + - 1 * (1 + - 1 * 2), ORundef, true, true)"
1.219 +then case m of Rewrite_Set_Inst' _ => ()
1.220 +else error "from locate_input_tactic return --- changed";
1.221 +
1.222 +val ("ok", (tacis'''''_', _, _)) = xxxxx_x;
1.223 +"~~~~~ from TOPLEVEL to states return:"; States.upd_calc cI ((pt'''''_', ip'''''_'), tacis'''''_');
1.224 +(*\\=========================================== isa <> REP (1) ===============================//*)
1.225 +(*//=========================================== isa <> REP (2) ===============================\\*)
1.226 +(*9* ) autoCalculate 1 (Steps 1); (*<-------------------------------------------------- orig. test code*)
1.227 +( *isa: <AUTOCALC><CALCID>1</CALCID><CALCCHANGED><UNCHANGED><INTLIST><INT>1</INT></INTLIST><POS>Frm</POS></UNCHANGED><DELETED><INTLIST><INT>1</INT></INTLIST><POS>Frm</POS></DELETED><GENERATED><INTLIST><INT>1</INT></INTLIST><POS>Res</POS></GENERATED></CALCCHANGED></AUTOCALC>*)
1.228 +
1.229 +"~~~~~ fun autoCalculate , args:"; val (cI, auto) = (1, (Steps 1));
1.230 + val pold = States.get_pos cI 1;
1.231 + val xxx = (States.get_calc cI);
1.232 +(*isa*) val (**)xxxx(**) (**) = (**)
1.233 + (*case*) Math_Engine.autocalc [] pold (xxx) auto (*of*);
1.234 +"~~~~~ fun autocalc , args:"; val (c, ip, cs, (Solve.Steps s)) = ([], pold, (xxx), auto);
1.235 + (*if*) s <= 1; (*then*)
1.236 + (*val (str, (_, c', ptp)) =*)
1.237 +
1.238 +Step.do_next ip cs;
1.239 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt,p), tacis)) = (ip, cs);
1.240 +
1.241 +(*+isa==REP*)val [(Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv"),
1.242 + Rewrite_Set_Inst' _, (pos', (istate, ctxt)))] = tacis;
1.243 +(*+*)if pos' = ([1], Res) andalso Istate.string_of istate
1.244 + = "Pstate ([\"\n(e_e, 1 + - 1 * 2 + x = 0)\", \"\n(v_v, x)\"], [R, L, R, L, R, L, R], empty, SOME e_e, \nx = 0 + - 1 * (1 + - 1 * 2), ORundef, true, true)"
1.245 +then () else error "init. step 1 + - 1 * 2 + x = 0 changed";
1.246 +
1.247 + val pIopt = get_pblID (pt,ip);
1.248 + (*if*) ip = ([], Pos.Res);(*else*)
1.249 + val (_::_) = (*case*) tacis (*of*);
1.250 +(*isa==REP*) (*if*) ip = p;(*then*)
1.251 + (*val (pt',c',p') =*) Solve_Step.s_add_general tacis (pt,[],p);
1.252 +(*//------------------------------------- final test -----------------------------------------\\*)
1.253 +val ("ok", [], ptp as (pt, p)) = xxxx;
1.254 +
1.255 +if Istate.string_of (get_istate_LI pt p) (* <> <> <> <> \<up> \<up> \<up> \<up> ^*)
1.256 +(*REP*) = "Pstate ([\"\n(e_e, 1 + - 1 * 2 + x = 0)\", \"\n(v_v, x)\"], [R, L, R, L, R, L, R], empty, SOME e_e, \nx = 0 + - 1 * (1 + - 1 * 2), ORundef, true, true)"
1.257 +then () else error "REP autoCalculate on (e_e, 1 + - 1 * 2 + x = 0) changed"
1.258 +
1.259 +"~~~~~ from TOPLEVEL to states return:"; States.upd_calc cI (ptp, []); States.upd_ipos cI 1 p;
1.260 +(*\\=========================================== isa <> REP (2) ===============================//*)
1.261 +
1.262 +(*10*) fetchProposedTactic 1;
1.263 + setNextTactic 1 (Rewrite_Set "Test_simplify");
1.264 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.265 +
1.266 +(*11*) fetchProposedTactic 1;
1.267 + setNextTactic 1 (Check_Postcond ["LINEAR", "univariate", "equation", "test"]);
1.268 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.269 +
1.270 +(*======= final test ==================================================*)
1.271 + val ((pt,_),_) = States.get_calc 1;
1.272 + val ip = States.get_pos 1 1;
1.273 +
1.274 + val (Form f, tac, asms) = ME_Misc.pt_extract (pt, ip);
1.275 + (*exception just above means: 'ModSpec' has been returned: error anyway*)
1.276 + if ip = ([], Res) andalso UnparseC.term f = "[x = 1]" then () else
1.277 + error "FE-Kernel-interface.sml: diff.behav. in solve_linear as rootpbl";
1.278 +
1.279 +
1.280 +"--------- inspect the CalcTree @{context} No.1 with Iterator No.2 -";
1.281 +"--------- inspect the CalcTree @{context} No.1 with Iterator No.2 -";
1.282 +"--------- inspect the CalcTree @{context} No.1 with Iterator No.2 -";
1.283 +(*WN041118: inspection shifted to Iterator No.1, because others need pos'*)
1.284 +(*-------- WN190723: doesnt work since changeset 59474 21d4d2868b83
1.285 + moveActiveRoot 1;
1.286 + refFormula 1 ([],Pbl); getTactic 1 ([],Pbl);(*Error*)
1.287 + moveActiveDown 1;
1.288 + refFormula 1 ([1],Frm); getTactic 1 ([1],Frm);(*Error*)
1.289 + moveActiveDown 1 ;
1.290 + refFormula 1 ([1],Res); getTactic 1 ([1],Res);(*OK*)
1.291 + (*getAssumption 1 ([1],Res); TODO.WN041217*)
1.292 + moveActiveDown 1 ; refFormula 1 ([2],Res);
1.293 + moveActiveCalcHead 1; refFormula 1 ([],Pbl);
1.294 + moveActiveDown 1;
1.295 + moveActiveDown 1;
1.296 + moveActiveDown 1;
1.297 + if States.get_pos 1 1 = ([2], Res) then () else
1.298 + error "FE-interface.sml: diff.behav. in a inspect 1 with Iterator 2";
1.299 + moveActiveDown 1; refFormula 1 ([], Res);
1.300 + if States.get_pos 1 1 = ([], Res) then () else
1.301 + error "FE-interface.sml: diff.behav. in b inspect 1 with Iterator 2";
1.302 + moveActiveCalcHead 1; refFormula 1 ([],Pbl);
1.303 +DEconstrCalcTree 1;
1.304 +------------------------------------------------------------------------------------------------*)
1.305 +
1.306 +"--------- miniscript with mini-subpbl ------------------";
1.307 +"--------- miniscript with mini-subpbl ------------------";
1.308 +"--------- miniscript with mini-subpbl ------------------";
1.309 +(*WN120210?not ME:\label{SOLVE:MANUAL:TACTIC:enter} UC 30.3.2.1 p.175 !!!!!NOT IMPL IN FE*)
1.310 +"=== this sequence of fun-calls resembles fun me ===";
1.311 + CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.312 + ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.313 + ["Test", "squ-equ-test-subpbl1"]))];
1.314 + Iterator 1;
1.315 +
1.316 + moveActiveRoot 1;
1.317 + refFormula 1 (States.get_pos 1 1);
1.318 + fetchProposedTactic 1;
1.319 + setNextTactic 1 (Model_Problem);
1.320 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*gets ModSpec;model is still empty*)
1.321 +
1.322 + fetchProposedTactic 1; (*<SYSERROR><CALCID>1</CALCID><ERROR>error in kernel 3</ERROR></SYSERROR>* )
1.323 + setNextTactic 1 (Add_Given "equality (x + 1 = 2)");
1.324 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.325 +
1.326 + fetchProposedTactic 1;
1.327 + setNextTactic 1 (Add_Given "solveFor x");
1.328 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.329 +
1.330 + fetchProposedTactic 1;
1.331 + setNextTactic 1 (Add_Find "solutions L");
1.332 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.333 +
1.334 + fetchProposedTactic 1;
1.335 + setNextTactic 1 (Specify_Theory "Test");
1.336 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.337 +
1.338 + fetchProposedTactic 1;
1.339 + setNextTactic 1 (Specify_Problem
1.340 + ["sqroot-test", "univariate", "equation", "test"]);
1.341 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.342 +"1-----------------------------------------------------------------";
1.343 +
1.344 + fetchProposedTactic 1;
1.345 + setNextTactic 1 (Specify_Method ["Test", "squ-equ-test-subpbl1"]);
1.346 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.347 +
1.348 + fetchProposedTactic 1;
1.349 + setNextTactic 1 (Apply_Method ["Test", "squ-equ-test-subpbl1"]);
1.350 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.351 +
1.352 + fetchProposedTactic 1;
1.353 + setNextTactic 1 (Rewrite_Set "norm_equation");
1.354 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.355 +
1.356 + fetchProposedTactic 1;
1.357 + setNextTactic 1 (Rewrite_Set "Test_simplify");
1.358 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.359 +
1.360 + fetchProposedTactic 1;(*----------------Subproblem--------------------*);
1.361 + setNextTactic 1 (Subproblem ("Test",
1.362 + ["LINEAR", "univariate", "equation", "test"]));
1.363 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.364 +
1.365 + fetchProposedTactic 1;
1.366 + setNextTactic 1 (Model_Problem );
1.367 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.368 +
1.369 + fetchProposedTactic 1;
1.370 + setNextTactic 1 (Add_Given "equality (- 1 + x = 0)");
1.371 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.372 +
1.373 + fetchProposedTactic 1;
1.374 + setNextTactic 1 (Add_Given "solveFor x");
1.375 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.376 +
1.377 + fetchProposedTactic 1;
1.378 + setNextTactic 1 (Add_Find "solutions x_i");
1.379 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.380 +
1.381 + fetchProposedTactic 1;
1.382 + setNextTactic 1 (Specify_Theory "Test");
1.383 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.384 +
1.385 + fetchProposedTactic 1;
1.386 + setNextTactic 1 (Specify_Problem ["LINEAR", "univariate", "equation", "test"]);
1.387 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.388 +"2-----------------------------------------------------------------";
1.389 +
1.390 + fetchProposedTactic 1;
1.391 + setNextTactic 1 (Specify_Method ["Test", "solve_linear"]);
1.392 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.393 +
1.394 + fetchProposedTactic 1;
1.395 + setNextTactic 1 (Apply_Method ["Test", "solve_linear"]);
1.396 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.397 +
1.398 + fetchProposedTactic 1;
1.399 + setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "isolate_bdv"));
1.400 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.401 +
1.402 + fetchProposedTactic 1;
1.403 + setNextTactic 1 (Rewrite_Set "Test_simplify");
1.404 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.405 +
1.406 + fetchProposedTactic 1;
1.407 + setNextTactic 1 (Check_Postcond ["LINEAR", "univariate", "equation", "test"]);
1.408 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.409 +
1.410 + fetchProposedTactic 1;
1.411 + setNextTactic 1 (Check_elementwise "Assumptions");
1.412 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.413 +
1.414 + val xml = fetchProposedTactic 1;
1.415 + setNextTactic 1 (Check_Postcond
1.416 + ["sqroot-test", "univariate", "equation", "test"]);
1.417 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.418 +
1.419 + val ((pt,_),_) = States.get_calc 1;
1.420 + val str = pr_ctree pr_short pt;
1.421 + writeln str;
1.422 + val ip = States.get_pos 1 1;
1.423 + val (Form f, tac, asms) = ME_Misc.pt_extract (pt, ip);
1.424 + (*exception just above means: 'ModSpec' has been returned: error anyway*)
1.425 + if UnparseC.term f = "[x = 1]" then () else
1.426 + error "FE-interface.sml: diff.behav. in miniscript with mini-subpb";
1.427 +(**)-------------------------------------------------------------------------------------------*)
1.428 + DEconstrCalcTree 1;
1.429 +
1.430 +"--------- mini-subpbl AUTOCALCULATE Steps 1 -------------";
1.431 +"--------- mini-subpbl AUTOCALCULATE Steps 1 -------------";
1.432 +"--------- mini-subpbl AUTOCALCULATE Steps 1 -------------";
1.433 +(*WN120210?not ME:\label{SOLVE:AUTO:one} UC 30.3.3.2 p.176*)
1.434 + CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.435 + ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.436 + ["Test", "squ-equ-test-subpbl1"]))];
1.437 + Iterator 1;
1.438 + moveActiveRoot 1;
1.439 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.440 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.441 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.442 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.443 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.444 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.445 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.446 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.447 + (*here the solve-phase starts*)
1.448 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.449 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.450 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.451 + (*------------------------------------*)
1.452 +(* (*default_print_depth 13*) States.get_calc 1;
1.453 + *)
1.454 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.455 + (*calc-head of subproblem*)
1.456 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.457 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.458 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.459 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.460 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.461 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.462 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.463 + (*solve-phase of the subproblem*)
1.464 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.465 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.466 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.467 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.468 + (*finish subproblem*)
1.469 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.470 + (*finish problem*)
1.471 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.472 +
1.473 + (*this checks the test for correctness..*)
1.474 + val ((pt,_),_) = States.get_calc 1;
1.475 + val p = States.get_pos 1 1;
1.476 + val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.477 + if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
1.478 + error "FE-interface.sml: diff.behav. in miniscript with mini-subpb";
1.479 + DEconstrCalcTree 1;
1.480 +
1.481 +
1.482 +"--------- solve_linear as rootpbl AUTO CompleteCalc ----";
1.483 +"--------- solve_linear as rootpbl AUTO CompleteCalc ----";
1.484 +"--------- solve_linear as rootpbl AUTO CompleteCalc ----";
1.485 +(*WN120210?not ME:\label{SPECIFY:START:auto} UC 30.2.4.2 p.174*)
1.486 + CalcTree @{context}
1.487 + [(["equality (1+- 1*2+x=(0::real))", "solveFor x", "solutions L"],
1.488 + ("Test",
1.489 + ["LINEAR", "univariate", "equation", "test"],
1.490 + ["Test", "solve_linear"]))];
1.491 + Iterator 1;
1.492 + moveActiveRoot 1;
1.493 +getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 999 false;
1.494 +
1.495 + autoCalculate 1 CompleteCalc;
1.496 + val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
1.497 + getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
1.498 +
1.499 + val ((pt,_),_) = States.get_calc 1;
1.500 + val p = States.get_pos 1 1;
1.501 + val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.502 + if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
1.503 + error "FE-interface.sml: diff.behav. in solve_linear/rt AUTOCALCULATE ";
1.504 +DEconstrCalcTree 1;
1.505 +
1.506 +"--------- solve_linear as rootpbl AUTO CompleteHead/Eval ";
1.507 +"--------- solve_linear as rootpbl AUTO CompleteHead/Eval ";
1.508 +"--------- solve_linear as rootpbl AUTO CompleteHead/Eval ";
1.509 +(* ERROR: error in kernel ?? *)
1.510 + CalcTree @{context}
1.511 + [(["equality (1+- 1*2+x=(0::real))", "solveFor x", "solutions L"],
1.512 + ("Test",
1.513 + ["LINEAR", "univariate", "equation", "test"],
1.514 + ["Test", "solve_linear"]))];
1.515 + Iterator 1;
1.516 + moveActiveRoot 1;
1.517 +
1.518 + autoCalculate 1 CompleteCalcHead;
1.519 + refFormula 1 (States.get_pos 1 1);
1.520 + val ((pt,p),_) = States.get_calc 1;
1.521 +
1.522 + autoCalculate 1 CompleteCalc;
1.523 + val ((pt,p),_) = States.get_calc 1;
1.524 + if p=([], Res) then () else
1.525 + error "FE-interface.sml: diff.behav. in solve_linear AUTOC Head/Eval ";
1.526 +DEconstrCalcTree 1;
1.527 +
1.528 +"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
1.529 +"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
1.530 +"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
1.531 +(*WN120210?not ME:\label{SPECIFY:START:auto} UC 30.2.4.2 p.174*)
1.532 + CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.533 + ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.534 + ["Test", "squ-equ-test-subpbl1"]))];
1.535 + Iterator 1;
1.536 + moveActiveRoot 1;
1.537 + autoCalculate 1 CompleteCalc;
1.538 + val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
1.539 +(*
1.540 +getTactic 1 ([1],Frm);
1.541 +getTactic 1 ([1],Res);
1.542 +initContext 1 Ptool.Thy_ ([1],Res);
1.543 +*)
1.544 + (*... returns calcChangedEvent with*)
1.545 + val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
1.546 + getFormulaeFromTo 1 unc gen 0 (*only result*) false;
1.547 + getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
1.548 + getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1.549 +
1.550 + val ((pt,_),_) = States.get_calc 1;
1.551 + val p = States.get_pos 1 1;
1.552 + val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.553 + if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
1.554 + error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
1.555 + DEconstrCalcTree 1;
1.556 +
1.557 +"--------- mini-subpbl AUTO CompleteCalcHead ------------";
1.558 +"--------- mini-subpbl AUTO CompleteCalcHead ------------";
1.559 +"--------- mini-subpbl AUTO CompleteCalcHead ------------";
1.560 + CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.561 + ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.562 + ["Test", "squ-equ-test-subpbl1"]))];
1.563 + Iterator 1;
1.564 + moveActiveRoot 1;
1.565 + autoCalculate 1 CompleteCalcHead;
1.566 +
1.567 +val ((Nd (PblObj {fmz = (fm, ("Test", pblID, metID)), loc = (SOME (env, ctxt1), NONE),
1.568 + meth, probl,
1.569 + spec = ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.570 + ["Test", "squ-equ-test-subpbl1"]),
1.571 + branch = TransitiveB, ostate = Incomplete (*!?\<forall>*), ...}, []),
1.572 + ([], Met)), []) = States.get_calc 1;
1.573 +if length meth = 3 andalso length probl = 3 (*just some items tested*) then ()
1.574 +else error "--- mini-subpbl AUTO CompleteCalcHead ---";
1.575 +DEconstrCalcTree 1;
1.576 +
1.577 +"--------- solve_linear as rootpbl AUTO CompleteModel ---";
1.578 +"--------- solve_linear as rootpbl AUTO CompleteModel ---";
1.579 +"--------- solve_linear as rootpbl AUTO CompleteModel ---";
1.580 +States.reset ();
1.581 + CalcTree @{context}
1.582 + [(["equality (1+- 1*2+x=(0::real))", "solveFor x", "solutions L"],
1.583 + ("Test",
1.584 + ["LINEAR", "univariate", "equation", "test"],
1.585 + ["Test", "solve_linear"]))];
1.586 + Iterator 1;
1.587 + moveActiveRoot 1;
1.588 + autoCalculate 1 CompleteModel;
1.589 + refFormula 1 (States.get_pos 1 1);
1.590 +
1.591 +setProblem 1 ["LINEAR", "univariate", "equation", "test"];
1.592 +val pos = States.get_pos 1 1;
1.593 +(*setContext 1 pos (Ptool.kestoreID2guh Ptool.Pbl_["LINEAR", "univariate", "equation", "test"]);*)
1.594 + refFormula 1 (States.get_pos 1 1);
1.595 +
1.596 +setMethod 1 ["Test", "solve_linear"];
1.597 +(*setContext 1 pos (Ptool.kestoreID2guh Ptool.Met_ ["Test", "solve_linear"]);*)
1.598 + refFormula 1 (States.get_pos 1 1);
1.599 + val ((pt,_),_) = States.get_calc 1;
1.600 + if get_obj g_spec pt [] = (ThyC.id_empty,
1.601 + ["LINEAR", "univariate", "equation", "test"],
1.602 + ["Test", "solve_linear"]) then ()
1.603 + else error "FE-interface.sml: diff.behav. in setProblem, setMethod";
1.604 +
1.605 + autoCalculate 1 CompleteCalcHead;
1.606 + refFormula 1 (States.get_pos 1 1);
1.607 + autoCalculate 1 CompleteCalc;
1.608 + moveActiveDown 1;
1.609 + moveActiveDown 1;
1.610 + moveActiveDown 1;
1.611 + refFormula 1 (States.get_pos 1 1);
1.612 + val ((pt,_),_) = States.get_calc 1;
1.613 + val p = States.get_pos 1 1;
1.614 + val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.615 + if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
1.616 + error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
1.617 + DEconstrCalcTree 1;
1.618 +
1.619 +"--------- setContext..Thy ------------------------------";
1.620 +"--------- setContext..Thy ------------------------------";
1.621 +"--------- setContext..Thy ------------------------------";
1.622 +States.reset ();
1.623 + CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.624 + ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.625 + ["Test", "squ-equ-test-subpbl1"]))];
1.626 + Iterator 1; moveActiveRoot 1;
1.627 + autoCalculate 1 CompleteCalcHead;
1.628 + autoCalculate 1 (Steps 1);
1.629 + val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt; (*2 lines, OK*)
1.630 + (*
1.631 + setNextTactic 1 (Rewrite_Set "Test_simplify"); (*--> "thy_isac_Test-rls-Test_simplify"*)
1.632 + autoCalculate 1 (Steps 1);
1.633 + val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
1.634 + *)
1.635 +"----- \<up> ^^ and vvvvv do the same -----";
1.636 +(*setContext 1 p "thy_isac_Test-rls-Test_simplify";*)
1.637 + val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt; (*2 lines, OK*)
1.638 +
1.639 + autoCalculate 1 (Steps 1);
1.640 +(*setContext 1 p "thy_isac_Test-rls-Test_simplify";*)
1.641 + val (((pt,_),_), p) = (States.get_calc 1, States.get_pos 1 1);
1.642 + val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.643 + if p = ([1], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "x + 1 + - 1 * 2 = 0"
1.644 + then () else error "--- setContext..Thy --- autoCalculate 1 (Steps 1) #1";
1.645 +
1.646 + autoCalculate 1 CompleteCalc;
1.647 + val (((pt,_),_), p) = (States.get_calc 1, States.get_pos 1 1);
1.648 + val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.649 +
1.650 + if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then ()
1.651 + else error "--- setContext..Thy --- autoCalculate CompleteCalc";
1.652 + DEconstrCalcTree 1;
1.653 +
1.654 +"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
1.655 +"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
1.656 +"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
1.657 +States.reset ();
1.658 + CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.659 + ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.660 + ["Test", "squ-equ-test-subpbl1"]))];
1.661 + Iterator 1; moveActiveRoot 1;
1.662 + autoCalculate 1 CompleteToSubpbl;
1.663 + refFormula 1 (States.get_pos 1 1); (*<ISA> - 1 + x = 0 </ISA>*);
1.664 + val ((pt,_),_) = States.get_calc 1;
1.665 + val str = pr_ctree pr_short pt;
1.666 + writeln str;
1.667 + if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + - 1 * 2 = 0\n"
1.668 + then () else
1.669 + error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl- 1";
1.670 +
1.671 + autoCalculate 1 (Steps 1); (*proceeds only, if NOT 1 step before subplb*)
1.672 + autoCalculate 1 CompleteToSubpbl;
1.673 + val ((pt,_),_) = States.get_calc 1;
1.674 + val str = pr_ctree pr_short pt;
1.675 + writeln str;
1.676 + autoCalculate 1 CompleteCalc; (*das geht ohnehin !*);
1.677 + val ((pt,_),_) = States.get_calc 1;
1.678 + val p = States.get_pos 1 1;
1.679 +
1.680 + val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.681 + if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
1.682 + error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl 1";
1.683 + DEconstrCalcTree 1;
1.684 +
1.685 +"--------- rat-eq + subpbl: no_met, NO solution dropped -";
1.686 +"--------- rat-eq + subpbl: no_met, NO solution dropped -";
1.687 +"--------- rat-eq + subpbl: no_met, NO solution dropped -";
1.688 +"--------- rat-eq + subpbl: no_met, NO solution dropped - see LI: '--- simpl.rat.term, '..";
1.689 +(*--- THIS IS RE-USED WITH fun me IN test/../MathEngine/solve.sml -------------------
1.690 + ---- rat-eq + subpbl: set_found in check_tac1 ----*)
1.691 + CalcTree @{context}
1.692 + [(["equality ((5*x)/(x - 2) - x/(x+2)=(4::real))", "solveFor x", "solutions L"],
1.693 + ((** )"RatEq"( **)"PolyEq"(*required for "make_ratpoly_in"*),
1.694 + ["univariate", "equation"], ["no_met"]))];
1.695 + Iterator 1;
1.696 + moveActiveRoot 1;
1.697 + fetchProposedTactic 1;
1.698 +
1.699 + setNextTactic 1 (Model_Problem);
1.700 + autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.701 +
1.702 + setNextTactic 1 (Specify_Theory "RatEq");
1.703 + autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.704 + setNextTactic 1 (Specify_Problem ["rational", "univariate", "equation"]);
1.705 + autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.706 + setNextTactic 1 (Specify_Method ["RatEq", "solve_rat_equation"]);
1.707 + autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.708 + setNextTactic 1 (Apply_Method ["RatEq", "solve_rat_equation"]);
1.709 + autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.710 + setNextTactic 1 (Rewrite_Set "RatEq_simplify");
1.711 + autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.712 + setNextTactic 1 (Rewrite_Set "norm_Rational");
1.713 + autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.714 + setNextTactic 1 (Rewrite_Set "RatEq_eliminate");
1.715 + autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.716 + (* __________ for "12 * x + 4 * x \<up> 2 = 4 * (-4 + x \<up> 2)"*)
1.717 + setNextTactic 1 (Subproblem ("PolyEq", ["normalise", "polynomial",
1.718 + "univariate", "equation"]));
1.719 + autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.720 + setNextTactic 1 (Model_Problem );
1.721 + autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.722 + setNextTactic 1 (Specify_Theory "PolyEq");
1.723 + autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.724 + setNextTactic 1 (Specify_Problem ["normalise", "polynomial",
1.725 + "univariate", "equation"]);
1.726 + autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.727 + setNextTactic 1 (Specify_Method ["PolyEq", "normalise_poly"]);
1.728 + autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.729 + setNextTactic 1 (Apply_Method ["PolyEq", "normalise_poly"]);
1.730 + autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.731 + setNextTactic 1 (Rewrite ("all_left", @{thm all_left}));
1.732 + autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.733 + setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "make_ratpoly_in"));
1.734 + autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.735 + (* __________ for "16 + 12 * x = 0"*)
1.736 + setNextTactic 1 (Subproblem ("PolyEq",
1.737 + ["degree_1", "polynomial", "univariate", "equation"]));
1.738 + autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.739 + setNextTactic 1 (Model_Problem );
1.740 + autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.741 + setNextTactic 1 (Specify_Theory "PolyEq");
1.742 + (*------------- some trials in the problem-hierarchy ---------------*)
1.743 + setNextTactic 1 (Specify_Problem ["LINEAR", "univariate", "equation"]);
1.744 + autoCalculate 1 (Steps 1); fetchProposedTactic 1; (*<ERROR> helpless </ERROR> !!!*)
1.745 + setNextTactic 1 (Refine_Problem ["univariate", "equation"]);
1.746 + (*------------------------------------------------------------------*)
1.747 + autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.748 + setNextTactic 1 (Specify_Method ["PolyEq", "solve_d1_polyeq_equation"]);
1.749 + autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.750 + setNextTactic 1 (Apply_Method ["PolyEq", "solve_d1_polyeq_equation"]);
1.751 + autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.752 + setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "d1_polyeq_simplify"));
1.753 + autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.754 + setNextTactic 1 (Rewrite_Set "polyeq_simplify");
1.755 + autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.756 + setNextTactic 1 Or_to_List;
1.757 + autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.758 + setNextTactic 1 (Check_elementwise "Assumptions");
1.759 + autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.760 + setNextTactic 1 (Check_Postcond ["degree_1", "polynomial",
1.761 + "univariate", "equation"]);
1.762 + autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.763 + setNextTactic 1 (Check_Postcond ["normalise", "polynomial",
1.764 + "univariate", "equation"]);
1.765 + autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.766 + setNextTactic 1 (Check_Postcond ["rational", "univariate", "equation"]);
1.767 + val (ptp,_) = States.get_calc 1;
1.768 + val (Form t,_,_) = ME_Misc.pt_extract ptp;
1.769 + if States.get_pos 1 1 = ([], Res) andalso UnparseC.term t = "[x = -4 / 3]" then ()
1.770 + else writeln "FE-inteface.sml: diff.behav. in rat-eq + subpbl: no_met, NO ..";
1.771 + DEconstrCalcTree 1;
1.772 +
1.773 +
1.774 +\<close> ML \<open>
1.775 +"--------- tryMatchProblem, tryRefineProblem ------------";
1.776 +"--------- tryMatchProblem, tryRefineProblem ------------";
1.777 +"--------- tryMatchProblem, tryRefineProblem ------------";
1.778 +(*{\bf\UC{Having \isac{} Refine the Problem
1.779 + * Automatically}\label{SPECIFY:refine-auto}\\} test match and refine with
1.780 + * x \<up>2 + 4*x + 5 = 2
1.781 +see isac.bridge.TestSpecify#testMatchRefine*)
1.782 +States.reset ();
1.783 + CalcTree @{context}
1.784 + [(["equality (x \<up> 2 + 4*x + 5 = (2::real))", "solveFor x", "solutions L"],
1.785 + ("Isac_Knowledge",
1.786 + ["univariate", "equation"],
1.787 + ["no_met"]))];
1.788 + Iterator 1;
1.789 + moveActiveRoot 1;
1.790 +
1.791 + fetchProposedTactic 1;
1.792 + setNextTactic 1 (Model_Problem );
1.793 + (*..this tactic should be done 'tacitly', too !*)
1.794 +
1.795 +(*
1.796 +autoCalculate 1 CompleteCalcHead;
1.797 +checkContext 1 ([],Pbl) "pbl_equ_univ";
1.798 +checkContext 1 ([],Pbl) (Ptool.kestoreID2guh Ptool.Pbl_ ["univariate", "equation"]);
1.799 +*)
1.800 +
1.801 + autoCalculate 1 (Steps 1);
1.802 +
1.803 + fetchProposedTactic 1;
1.804 + setNextTactic 1 (Add_Given "equality (x \<up> 2 + 4 * x + 5 = (2::real))");
1.805 + autoCalculate 1 (Steps 1);
1.806 +
1.807 + "--------- we go into the ProblemBrowser (_NO_ pblID selected) -";
1.808 +(*initContext 1 Ptool.Pbl_ ([],Pbl);*)
1.809 +(* this would break if a calculation would be inserted before: CALCID...
1.810 + and pattern matching is not available in *.java.
1.811 +if cut_xml xml = "(CONTEXTPBL)\n. (CALCID)\n. . 1\n. (/CALCID)\n. (CONTEXTDATA)\n. . (GUH)\n. . . pbl_equ_univ\n. . (/GUH)\n. . (STATUS)\n. . . correct\n. . (/STATUS)\n. . (HEAD)\n. . . (MATHML)\n. . . . (ISA)\n. . . . . solve (x ^ 2 + 4 * x + 5 = 2, x)\n. . . . (/ISA)\n. . . (/MATHML)\n. . (/HEAD)\n. . (MODEL)\n. . . (GIVEN)\n. . . . (ITEM status=correct)\n. . . . . (MATHML)\n. . . . . . (ISA)\n. . . . . . . equality (x ^ 2 + 4 * x + 5 = 2)\n. . . . . . (/ISA)\n. . . . . (/MATHML)\n. . . . (/ITEM)\n. . . . (ITEM status=correct)\n. . . . . (MATHML)\n. . . . . . (ISA)\n. . . . . . . solveFor x\n. . . . . . (/ISA)\n. . . . . (/MATHML)\n. . . . (/ITEM)\n. . . (/GIVEN)\n. . . (WHERE)\n. . . . (ITEM status=correct)\n. . . . . (MATHML)\n. . . . . . (ISA)\n. . . . . . . TermC.matches (?a = ?b) (x \<up> ^ 2 + 4 * x + 5 = 2)\n. . . . . . (/ISA)\n. . . . . (/MATHML)\n. . . . (/ITEM)\n. . . (/WHERE)\n. . . (FIND)\n. . . . (ITEM status=correct)\n. . . . . (MATHML)\n. . . . . . (ISA)\n. . . . . . . solutions L\n. . . . . . (/ISA)\n. . . . . (/MATHML)\n. . . . (/ITEM)\n. . . (/FI"
1.812 +then () else error "--- tryMatchProblem, tryRefineProblem: initContext 1 Ptool.Pbl_ ([],Pbl); CHANGED";
1.813 +*)
1.814 +(*initContext 1 Ptool.Met_ ([],Pbl);*)
1.815 +(*<SYSERROR><CALCID>1</CALCID><ERROR>error in kernel 33</ERROR></SYSERROR>*)
1.816 +
1.817 + "--------- this match will show some incomplete items: ---------";
1.818 +
1.819 +(*checkContext 1 ([],Pbl) (Ptool.kestoreID2guh Ptool.Pbl_ ["univariate", "equation"]);
1.820 +checkContext 1 ([],Pbl) (Ptool.kestoreID2guh Ptool.Met_ ["LinEq", "solve_lineq_equation"]);*)
1.821 +
1.822 +
1.823 + fetchProposedTactic 1;
1.824 + setNextTactic 1 (Add_Given "solveFor x"); autoCalculate 1 (Steps 1);
1.825 +
1.826 + fetchProposedTactic 1;
1.827 + setNextTactic 1 (Add_Find "solutions L"); autoCalculate 1 (Steps 1);
1.828 +
1.829 + "--------- this is a matching model (all items correct): -------";
1.830 +(*checkContext 1 ([],Pbl) (Ptool.kestoreID2guh Ptool.Pbl_ ["univariate", "equation"]);*)
1.831 + "--------- this is a NOT matching model (some 'false': ---------";
1.832 +(*checkContext 1 ([],Pbl)(Ptool.kestoreID2guh Ptool.Pbl_ ["LINEAR", "univariate", "equation"]);*)
1.833 +
1.834 + "--------- find out a matching problem: ------------------------";
1.835 + "--------- find out a matching problem (FAILING: no new pbl) ---";
1.836 + refineProblem 1 ([],Pbl)(Ptool.pblID2guh @{context} ["LINEAR", "univariate", "equation"]);
1.837 +
1.838 + "--------- find out a matching problem (SUCCESSFUL) ------------";
1.839 + refineProblem 1 ([],Pbl) (Ptool.pblID2guh @{context} ["univariate", "equation"]);
1.840 +
1.841 + "--------- tryMatch, tryRefine did not change the calculation -";
1.842 + "--------- this is done by <TRANSFER> on the pbl-browser: ------";
1.843 + setNextTactic 1 (Specify_Problem ["normalise", "polynomial",
1.844 + "univariate", "equation"]);
1.845 + autoCalculate 1 (Steps 1);
1.846 +(*WN050904 fetchProposedTactic again --> Specify_Problem ["normalise",...
1.847 + and Specify_Theory skipped in comparison to below --- \<up> -inserted *)
1.848 +(*------------vvv-inserted-----------------------------------------------*)
1.849 + fetchProposedTactic 1;
1.850 +(*/-----ERROR INTRODUCED BY CHILD OF 33913fe24685 --------------------------------------------\* )
1.851 + setNextTactic 1 (Specify_Problem ["normalise", "polynomial",
1.852 + "univariate", "equation"]);
1.853 + autoCalculate 1 (Steps 1);
1.854 +
1.855 +(*and Specify_Theory skipped by fetchProposedTactic ?!?*)
1.856 +
1.857 + fetchProposedTactic 1;
1.858 + setNextTactic 1 (Specify_Method ["PolyEq", "normalise_poly"]);
1.859 + autoCalculate 1 (Steps 1);
1.860 +
1.861 + fetchProposedTactic 1;
1.862 + setNextTactic 1 (Apply_Method ["PolyEq", "normalise_poly"]);
1.863 +
1.864 + autoCalculate 1 CompleteCalc;
1.865 +
1.866 + val ((pt,_),_) = States.get_calc 1;
1.867 + Test_Tool.show_pt pt;
1.868 + val p = States.get_pos 1 1;
1.869 + val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.870 + if UnparseC.term f = "[x = - 1, x = -3]" andalso p = ([], Res) then () else
1.871 + error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
1.872 +
1.873 +(*------------ \<up> -inserted-----------------------------------------------*)
1.874 +(*WN050904 the fetchProposedTactic's below may not have worked like that
1.875 + before, too, because there was no check*)
1.876 + fetchProposedTactic 1;
1.877 + setNextTactic 1 (Specify_Theory "PolyEq");
1.878 + autoCalculate 1 (Steps 1);
1.879 +
1.880 + fetchProposedTactic 1;
1.881 + setNextTactic 1 (Specify_Method ["PolyEq", "normalise_poly"]);
1.882 + autoCalculate 1 (Steps 1);
1.883 +
1.884 + fetchProposedTactic 1;
1.885 + "--------- now the calc-header is ready for enter 'solving' ----";
1.886 + autoCalculate 1 CompleteCalc;
1.887 +
1.888 + val ((pt,_),_) = States.get_calc 1;
1.889 + rootthy pt;
1.890 + Test_Tool.show_pt pt;
1.891 + val p = States.get_pos 1 1;
1.892 + val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.893 + if UnparseC.term f = "[x = - 1, x = -3]" andalso p = ([], Res) then () else
1.894 + error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
1.895 + DEconstrCalcTree 1;
1.896 +( *\-----ERROR INTRODUCED BY CHILD OF 33913fe24685 --------------------------------------------/*)
1.897 +
1.898 +"--------- modifyCalcHead, resetCalcHead, modelProblem --";
1.899 +"--------- modifyCalcHead, resetCalcHead, modelProblem --";
1.900 +"--------- modifyCalcHead, resetCalcHead, modelProblem --";
1.901 +States.reset ();
1.902 + CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.903 + ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.904 + ["Test", "squ-equ-test-subpbl1"]))];
1.905 + Iterator 1;
1.906 + moveActiveRoot 1;
1.907 +
1.908 + modifyCalcHead 1 (([],Pbl),(*the position from refFormula*)
1.909 + "solve (x+1=2, x)",(*the headline*)
1.910 + [P_Spec.Given ["equality (x+1=(2::real))", "solveFor x"],
1.911 + P_Spec.Find ["solutions L"](*,P_Spec.Relate []*)],
1.912 + Pbl,
1.913 + ("Test",
1.914 + ["sqroot-test", "univariate", "equation", "test"],
1.915 + ["Test", "squ-equ-test-subpbl1"]));
1.916 +
1.917 +val ((Nd (PblObj {fmz = (fm, tpm),
1.918 + loc = (SOME scrst_ctxt, NONE),
1.919 + ctxt,
1.920 + meth,
1.921 + spec = (thy,
1.922 + ["sqroot-test", "univariate", "equation", "test"],
1.923 + ["Test", "squ-equ-test-subpbl1"]),
1.924 + probl,
1.925 + branch = TransitiveB,
1.926 + origin,
1.927 + ostate = Incomplete,
1.928 + result},
1.929 + []),
1.930 + ([], Pbl)),
1.931 + []) = States.get_calc 1;
1.932 +(*WN110622: is the same as in 2002, but shouldn't be probl = [3 items?]*)
1.933 +if length meth = 0 andalso length probl = 0 (*just some items tested*) then ()
1.934 +else error "--- modifyCalcHead, resetCalcHead, modelProblem 1 --";
1.935 +
1.936 +resetCalcHead 1;
1.937 +modelProblem 1;
1.938 +
1.939 +States.get_calc 1;
1.940 +val ((Nd (PblObj {fmz = (fm, tpm),
1.941 + loc = (SOME scrst_ctxt, NONE),
1.942 + ctxt,
1.943 + meth,
1.944 + spec = ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]),
1.945 + probl,
1.946 + branch = TransitiveB,
1.947 + origin,
1.948 + ostate = Incomplete,
1.949 + result},
1.950 + []),
1.951 + ([], Pbl)),
1.952 + []) = States.get_calc 1;
1.953 +if length meth = 3 andalso length probl = 3 (*just some items tested*) then ()
1.954 +else error "--- modifyCalcHead, resetCalcHead, modelProblem 2 --";
1.955 +
1.956 +"--------- maximum-example, UC: Modeling an example -----";
1.957 +"--------- maximum-example, UC: Modeling an example -----";
1.958 +"--------- maximum-example, UC: Modeling an example -----";
1.959 +(* {\bf\UC{Editing the Model}\label{SPECIFY:enter}\label{SPECIFY:check}\\}
1.960 +see isac.bridge.TestModel#testEditItems
1.961 +*)
1.962 + val elems = ["fixedValues [r=Arbfix]", "maximum A", "valuesFor [a,b]",
1.963 + "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
1.964 + "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
1.965 + "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]",
1.966 + (* \<up> these are the elements for the root-problem (in variants)*)
1.967 + (*vvv these are elements required for subproblems*)
1.968 + "boundVariable a", "boundVariable b", "boundVariable alpha",
1.969 + "interval {x::real. 0 <= x & x <= 2*r}",
1.970 + "interval {x::real. 0 <= x & x <= 2*r}",
1.971 + "interval {x::real. 0 <= x & x <= pi}",
1.972 + "errorBound (eps=(0::real))"]
1.973 + (*specifying is not interesting for this example*)
1.974 + val spec = ("Diff_App", ["maximum_of", "function"],
1.975 + ["Diff_App", "max_by_calculus"]);
1.976 + (*the empty model with descriptions for user-guidance by Model_Problem*)
1.977 + val empty_model = [P_Spec.Given ["fixedValues []"],
1.978 + P_Spec.Find ["maximum", "valuesFor"],
1.979 + P_Spec.Relate ["relations []"]];
1.980 + DEconstrCalcTree 1;
1.981 +
1.982 +"#################################################################";
1.983 +States.reset ();
1.984 + CalcTree @{context} [(elems, spec)];
1.985 + Iterator 1;
1.986 + moveActiveRoot 1;
1.987 + refFormula 1 (States.get_pos 1 1);
1.988 + (*this gives a completely empty model*)
1.989 +
1.990 + fetchProposedTactic 1;
1.991 +(*fill the CalcHead with Descriptions...*)
1.992 + setNextTactic 1 (Model_Problem );
1.993 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.994 +
1.995 + (*user input is !!!!!EITHER!!!!! _some_ (at least one) items of the model
1.996 + !!!!!OR!!!!! _one_ part of the specification !!!!!!!!!!!!!*)
1.997 + (*input of two items, 'fixedValues [r=Arbfix]' and 'maximum b'...*)
1.998 + modifyCalcHead 1 (([],Pbl) (*position, from previous refFormula*),
1.999 + "Problem (Diff_App.thy, [maximum_of, function])",
1.1000 + (*the head-form \<up> is not used for input here*)
1.1001 + [P_Spec.Given ["fixedValues [r=Arbfix]"(*new input*)],
1.1002 + P_Spec.Find ["maximum b"(*new input*), "valuesFor"],
1.1003 + P_Spec.Relate ["relations"]],
1.1004 + (*input (Arbfix will dissappear soon)*)
1.1005 + Pbl (*belongsto*),
1.1006 + References.empty (*no input to the specification*));
1.1007 +
1.1008 + (*the user does not know, what 'superfluous' for 'maximum b' may mean
1.1009 + and asks what to do next*)
1.1010 + fetchProposedTactic 1;
1.1011 + (*the student follows the advice*)
1.1012 + setNextTactic 1 (Add_Find "maximum A"); (*FIXME.17.11.03: does not yet work*)
1.1013 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.1014 +
1.1015 + (*this input completes the model*)
1.1016 + modifyCalcHead 1 (([],Pbl), "not used here",
1.1017 + [P_Spec.Given ["fixedValues [r=Arbfix]"],
1.1018 + P_Spec.Find ["maximum A", "valuesFor [a,b]"(*new input*)],
1.1019 + P_Spec.Relate ["relations [A=a*b, \
1.1020 + \(a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]"]], Pbl, References.empty);
1.1021 +
1.1022 + (*specification is not interesting and should be skipped by the dialogguide;
1.1023 + !!!!!!!!!!!!!!!!!!!! input of ONE part at a time !!!!!!!!!!!!!!!!!!!!!!*)
1.1024 + modifyCalcHead 1 (([],Pbl), "not used here",
1.1025 + [P_Spec.Given ["fixedValues [r=Arbfix]"],
1.1026 + P_Spec.Find ["maximum A", "valuesFor [a,b]"(*new input*)],
1.1027 + P_Spec.Relate ["relations [A=a*b, \
1.1028 + \(a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]"]], Pbl,
1.1029 + ("Diff_App", Problem.id_empty, MethodC.id_empty));
1.1030 + modifyCalcHead 1 (([],Pbl), "not used here",
1.1031 + [P_Spec.Given ["fixedValues [r=Arbfix]"],
1.1032 + P_Spec.Find ["maximum A", "valuesFor [a,b]"(*new input*)],
1.1033 + P_Spec.Relate ["relations [A=a*b, \
1.1034 + \(a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]"]], Pbl,
1.1035 + ("Diff_App", ["maximum_of", "function"],
1.1036 + MethodC.id_empty));
1.1037 + modifyCalcHead 1 (([],Pbl), "not used here",
1.1038 + [P_Spec.Given ["fixedValues [r=Arbfix]"],
1.1039 + P_Spec.Find ["maximum A", "valuesFor [a,b]"(*new input*)],
1.1040 + P_Spec.Relate ["relations [A=a*b, \
1.1041 + \(a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]"]], Pbl,
1.1042 + ("Diff_App", ["maximum_of", "function"],
1.1043 + ["Diff_App", "max_by_calculus"]));
1.1044 + (*this final calcHead now has STATUS 'complete' !*)
1.1045 + DEconstrCalcTree 1;
1.1046 +
1.1047 +(*POSTPONE CORRECTION AT END OF TRANSITION TO Isabelle/PIDE/Isac (~ Cas_Cmd)
1.1048 +"--------- solve_linear from pbl-hierarchy --------------";
1.1049 +"--------- solve_linear from pbl-hierarchy --------------";
1.1050 +"--------- solve_linear from pbl-hierarchy --------------";
1.1051 +States.reset ();
1.1052 + val (fmz, sp) = ([], ("", ["LINEAR", "univariate", "equation", "test"], []));
1.1053 + CalcTree @{context} [(fmz, sp)];
1.1054 + Iterator 1; moveActiveRoot 1;
1.1055 + refFormula 1 (States.get_pos 1 1);
1.1056 + modifyCalcHead 1 (([],Pbl),"solve (1+- 1*2+x=(0::real))",
1.1057 + [P_Spec.Given ["equality (1+- 1*2+x=(0::real))", "solveFor x"],
1.1058 + P_Spec.Find ["solutions L"]],
1.1059 + Pbl,
1.1060 + ("Test", ["LINEAR", "univariate", "equation", "test"],
1.1061 + ["Test", "solve_linear"]));
1.1062 + autoCalculate 1 CompleteCalc;
1.1063 + refFormula 1 (States.get_pos 1 1);
1.1064 + val ((pt,_),_) = States.get_calc 1;
1.1065 + val p = States.get_pos 1 1;
1.1066 + val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.1067 + if UnparseC.term f = "[x = 1]" andalso p = ([], Res) andalso map UnparseC.term asms = [] then ()
1.1068 + else error "FE-interface.sml: diff.behav. in from pbl -hierarchy 1";
1.1069 + DEconstrCalcTree 1;
1.1070 +
1.1071 +"--------- solve_linear as in an algebra system (CAS)----";
1.1072 +"--------- solve_linear as in an algebra system (CAS)----";
1.1073 +"--------- solve_linear as in an algebra system (CAS)----";
1.1074 +(*WN120210?not ME:\label{UC:cas-input} UC 30.1.2.5 p.168*)
1.1075 +States.reset ();
1.1076 + val (fmz, sp) = ([], ("", [], []));
1.1077 + CalcTree @{context} [(fmz, sp)];
1.1078 + Iterator 1; moveActiveRoot 1;
1.1079 + modifyCalcHead 1 (([],Pbl),"solveTest (1+- 1*2+x=0,x)", [], Pbl, ("", [], []));
1.1080 + autoCalculate 1 CompleteCalc;
1.1081 + refFormula 1 (States.get_pos 1 1);
1.1082 + val ((pt,_),_) = States.get_calc 1;
1.1083 + val p = States.get_pos 1 1;
1.1084 + val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.1085 + if UnparseC.term f = "[x = 1]" andalso p = ([], Res) andalso map UnparseC.term asms = [] then ()
1.1086 + else error "FE-interface.sml: diff.behav. in from pbl -hierarchy 2";
1.1087 +DEconstrCalcTree 1;
1.1088 +*)
1.1089 +
1.1090 +"--------- interSteps: on 'miniscript with mini-subpbl' -";
1.1091 +"--------- interSteps: on 'miniscript with mini-subpbl' -";
1.1092 +"--------- interSteps: on 'miniscript with mini-subpbl' -";
1.1093 + CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.1094 + ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.1095 + ["Test", "squ-equ-test-subpbl1"]))];
1.1096 + Iterator 1;
1.1097 + moveActiveRoot 1;
1.1098 + autoCalculate 1 CompleteCalc;
1.1099 + val ((pt,_),_) = States.get_calc 1;
1.1100 + Test_Tool.show_pt pt;
1.1101 +
1.1102 + (*UC\label{UC:inter-steps} UC 30.3.5.5 p.178*)
1.1103 + interSteps 1 ([2],Res);
1.1104 + val ((pt,_),_) = States.get_calc 1; Test_Tool.show_pt pt (*new ([2,1],Frm)..([2,6],Res)*);
1.1105 + val (unc, del, gen) = (([1],Res),([1],Res),([2,6],Res));
1.1106 + getFormulaeFromTo 1 unc gen 1 false;
1.1107 +
1.1108 + (*UC\label{UC:inter-steps} UC 30.3.5.5 p.178*)
1.1109 + interSteps 1 ([3,2],Res);
1.1110 + val ((pt,_),_) = States.get_calc 1; Test_Tool.show_pt pt (*new ([3,2,1],Frm)..([3,2,2],Res)*);
1.1111 + val (unc, del, gen) = (([3,1],Res),([3,1],Res),([3,2,2],Res));
1.1112 + getFormulaeFromTo 1 unc gen 1 false;
1.1113 +
1.1114 + (*UC\label{UC:inter-steps} UC 30.3.5.5 p.178*)
1.1115 + interSteps 1 ([3],Res) (*no new steps in subproblems*);
1.1116 + val (unc, del, gen) = (([3],Pbl),([3],Pbl),([3,2],Res));
1.1117 + getFormulaeFromTo 1 unc gen 1 false;
1.1118 +
1.1119 + (*UC\label{UC:inter-steps} UC 30.3.5.5 p.178*)
1.1120 + interSteps 1 ([],Res) (*no new steps in subproblems*);
1.1121 + val (unc, del, gen) = (([],Pbl),([],Pbl),([4],Res));
1.1122 + getFormulaeFromTo 1 unc gen 1 false;
1.1123 +DEconstrCalcTree 1;
1.1124 +
1.1125 +"--------- getTactic, fetchApplicableTactics ------------";
1.1126 +"--------- getTactic, fetchApplicableTactics ------------";
1.1127 +"--------- getTactic, fetchApplicableTactics ------------";
1.1128 +(* compare test/../script.sml
1.1129 +"----------- fun from_prog ---------------------------------------";
1.1130 +*)
1.1131 + CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.1132 + ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.1133 + ["Test", "squ-equ-test-subpbl1"]))];
1.1134 + Iterator 1; moveActiveRoot 1;
1.1135 + autoCalculate 1 CompleteCalc;
1.1136 + val ((pt,_),_) = States.get_calc 1;
1.1137 + Test_Tool.show_pt pt;
1.1138 +
1.1139 + (*UC\label{SOLVE:HIDE:getTactic} \label{SOLVE:AUTO:tactic} UC 30.3.3.1 p.176
1.1140 +WN120210 not impl. in FE*)
1.1141 + getTactic 1 ([],Pbl);
1.1142 + getTactic 1 ([1],Res);
1.1143 + getTactic 1 ([3],Pbl);
1.1144 + getTactic 1 ([3,1],Frm);
1.1145 + getTactic 1 ([3],Res);
1.1146 + getTactic 1 ([],Res);
1.1147 +
1.1148 +(*UC\label{SOLVE:MANUAL:TACTIC:listall} UC 30.3.2.2 p.175*)
1.1149 + fetchApplicableTactics 1 99999 ([],Pbl);
1.1150 + fetchApplicableTactics 1 99999 ([1],Res);
1.1151 + fetchApplicableTactics 1 99999 ([3],Pbl);
1.1152 + fetchApplicableTactics 1 99999 ([3,1],Res);
1.1153 + fetchApplicableTactics 1 99999 ([3],Res);
1.1154 + fetchApplicableTactics 1 99999 ([],Res);
1.1155 +DEconstrCalcTree 1;
1.1156 +
1.1157 +(*SINCE eliminate ThmC.numerals_to_Free: loops ---------------------------------------------\\* )
1.1158 +"--------- getAssumptions, getAccumulatedAsms -----------";
1.1159 +"--------- getAssumptions, getAccumulatedAsms -----------";
1.1160 +"--------- getAssumptions, getAccumulatedAsms -----------";
1.1161 +States.reset ();
1.1162 +CalcTree @{context}
1.1163 +[(["equality (x/(x \<up> 2 - 6*x+9) - 1/(x \<up> 2 - 3*x) =1/x)",
1.1164 + "solveFor x", "solutions L"],
1.1165 + ("RatEq",["univariate", "equation"],["no_met"]))];
1.1166 +Iterator 1; moveActiveRoot 1;
1.1167 +autoCalculate 1 CompleteCalc;
1.1168 +val ((pt,_),_) = States.get_calc 1;
1.1169 +val p = States.get_pos 1 1;
1.1170 +val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.1171 +(*============ inhibit exn WN120316 compare 2002-- 2011 ===========================
1.1172 +if map UnparseC.term asms =
1.1173 + ["True |\n~ lhs ((3 + - 1 * x + x \<up> 2) * x =\n" ^
1.1174 + " 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3)) is_poly_in x", "-6 * x + 5 * x \<up>\<up> 2 = 0",
1.1175 + "lhs (-6 * x + 5 * x \<up> 2 = 0) is_poly_in x",
1.1176 + "lhs (-6 * x + 5 * x \<up>\<up> 2 = 0) has_degree_in x = 2",
1.1177 + "9 * x + -6 * x \<up> 2 + x \<up> 3 ~= 0"]
1.1178 +andalso UnparseC.term f = "[-6 * x + 5 * x \<up> 2 = 0]" andalso p = ([], Res) then ()
1.1179 +else error "TODO compare 2002-- 2011"; (*...data during test --- x / (x \<up> 2 - 6 * x + 9) - 1...*)
1.1180 +============ inhibit exn WN120316 compare 2002-- 2011 ===========================*)
1.1181 +
1.1182 +if p = ([], Res) andalso UnparseC.term f = "[x = 6 / 5]"
1.1183 +andalso map UnparseC.term asms = []
1.1184 +then () else error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b [x = 6 / 5]";
1.1185 +
1.1186 +(*UC\label{SOLVE:HELP:assumptions} UC 30.3.5.1 p.178*)
1.1187 +getAssumptions 1 ([3], Res);
1.1188 +getAssumptions 1 ([5], Res);
1.1189 +(*UC\label{SOLVE:HELP:assumptions-origin} UC 30.3.5.2 p.178
1.1190 + WN0502 still without positions*)
1.1191 +getAccumulatedAsms 1 ([3], Res);
1.1192 +getAccumulatedAsms 1 ([5], Res);
1.1193 +DEconstrCalcTree 1;
1.1194 +( *SINCE eliminate ThmC.numerals_to_Free: loops ---------------------------------------------//*)
1.1195 +
1.1196 +\<close> ML \<open>
1.1197 +"--------- arbitrary combinations of steps --------------";
1.1198 +"--------- arbitrary combinations of steps --------------";
1.1199 +"--------- arbitrary combinations of steps --------------";
1.1200 + CalcTree @{context} (*start of calculation, return No.1*)
1.1201 + [(["equality (1+- 1*2+x=(0::real))", "solveFor x", "solutions L"],
1.1202 + ("Test",
1.1203 + ["LINEAR", "univariate", "equation", "test"],
1.1204 + ["Test", "solve_linear"]))];
1.1205 + Iterator 1; moveActiveRoot 1;
1.1206 +
1.1207 + fetchProposedTactic 1;
1.1208 + (*ERROR States.get_calc 1 not existent*)
1.1209 + setNextTactic 1 (Model_Problem );
1.1210 + autoCalculate 1 (Steps 1);
1.1211 + fetchProposedTactic 1;
1.1212 + fetchProposedTactic 1;
1.1213 +
1.1214 + setNextTactic 1 (Add_Find "solutions L");
1.1215 + setNextTactic 1 (Add_Find "solutions L");
1.1216 +
1.1217 + autoCalculate 1 (Steps 1);
1.1218 + autoCalculate 1 (Steps 1);
1.1219 +
1.1220 + setNextTactic 1 (Specify_Theory "Test");
1.1221 + fetchProposedTactic 1;
1.1222 + autoCalculate 1 (Steps 1);
1.1223 +
1.1224 + autoCalculate 1 (Steps 1);
1.1225 + autoCalculate 1 (Steps 1);
1.1226 + autoCalculate 1 (Steps 1);
1.1227 + autoCalculate 1 (Steps 1);
1.1228 +(*------------------------- end calc-head*)
1.1229 +
1.1230 + fetchProposedTactic 1;
1.1231 + setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "isolate_bdv"));
1.1232 + autoCalculate 1 (Steps 1);
1.1233 +
1.1234 + setNextTactic 1 (Rewrite_Set "Test_simplify");
1.1235 + fetchProposedTactic 1;
1.1236 + autoCalculate 1 (Steps 1);
1.1237 +
1.1238 + autoCalculate 1 CompleteCalc;
1.1239 + val ((pt,_),_) = States.get_calc 1;
1.1240 + val p = States.get_pos 1 1;
1.1241 + val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.1242 + if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
1.1243 + error "FE-interface.sml: diff.behav. in combinations of steps";
1.1244 +DEconstrCalcTree 1;
1.1245 +
1.1246 +"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right"; (*UC 30.3.2.4 p.175*)
1.1247 +"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
1.1248 +"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
1.1249 +States.reset ();
1.1250 + CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.1251 + ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.1252 + ["Test", "squ-equ-test-subpbl1"]))];
1.1253 + Iterator 1;
1.1254 + moveActiveRoot 1;
1.1255 + autoCalculate 1 CompleteCalcHead;
1.1256 + autoCalculate 1 (Steps 1);
1.1257 + autoCalculate 1 (Steps 1);
1.1258 + appendFormula 1 "- 1 + x = 0" (*|> Future.join*);
1.1259 + (*... returns calcChangedEvent with*)
1.1260 + val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res));
1.1261 + getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1.1262 +
1.1263 + val ((pt,_),_) = States.get_calc 1;
1.1264 + val p = States.get_pos 1 1;
1.1265 + val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.1266 + if UnparseC.term f = "- 1 + x = 0" andalso p = ([2], Res) then () else
1.1267 + error "FE-interface.sml: diff.behav. in FORMULA:enter} right";
1.1268 +DEconstrCalcTree 1;
1.1269 +
1.1270 +"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other"; (*UC 30.3.2.4 p.175*)
1.1271 +"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
1.1272 +"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
1.1273 + CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.1274 + ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.1275 + ["Test", "squ-equ-test-subpbl1"]))];
1.1276 + Iterator 1;
1.1277 + moveActiveRoot 1;
1.1278 + autoCalculate 1 CompleteCalcHead;
1.1279 + autoCalculate 1 (Steps 1);
1.1280 + autoCalculate 1 (Steps 1);
1.1281 + appendFormula 1 "x - 1 = 0" (*|> Future.join*);
1.1282 + val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res));
1.1283 + getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1.1284 + (*11 elements !!!*)
1.1285 +
1.1286 + val ((pt,_),_) = States.get_calc 1;
1.1287 + val p = States.get_pos 1 1;
1.1288 + val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.1289 + if UnparseC.term f = "x - 1 = 0" andalso p = ([2], Res) then () else
1.1290 + error "FE-interface.sml: diff.behav. in FORMULA:enter} other";
1.1291 +DEconstrCalcTree 1;
1.1292 +
1.1293 +"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2"; (*UC 30.3.2.4 p.175*)
1.1294 +"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
1.1295 +"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
1.1296 + CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.1297 + ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.1298 + ["Test", "squ-equ-test-subpbl1"]))];
1.1299 + Iterator 1;
1.1300 + moveActiveRoot 1;
1.1301 + autoCalculate 1 CompleteCalcHead;
1.1302 + autoCalculate 1 (Steps 1);
1.1303 + autoCalculate 1 (Steps 1);
1.1304 + appendFormula 1 "x = 1" (*|> Future.join*);
1.1305 + (*... returns calcChangedEvent with*)
1.1306 + val (unc, del, gen) = (([1],Res), ([1],Res), ([3,2],Res));
1.1307 + getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1.1308 + (*6 elements !!!*)
1.1309 +
1.1310 + val ((pt,_),_) = States.get_calc 1;
1.1311 + val p = States.get_pos 1 1;
1.1312 + val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.1313 + if UnparseC.term f = "x = 1" andalso p = ([3,2], Res) then () else
1.1314 + error "FE-interface.sml: diff.behav. in FORMULA:enter} oth 2";
1.1315 +DEconstrCalcTree 1;
1.1316 +
1.1317 +"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok"; (*UC 30.3.2.4 p.175*)
1.1318 +"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
1.1319 +"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
1.1320 + CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.1321 + ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.1322 + ["Test", "squ-equ-test-subpbl1"]))];
1.1323 + Iterator 1;
1.1324 + moveActiveRoot 1;
1.1325 + autoCalculate 1 CompleteCalcHead;
1.1326 + autoCalculate 1 (Steps 1);
1.1327 + autoCalculate 1 (Steps 1);
1.1328 + appendFormula 1 "x - 4711 = 0" (*|> Future.join*);
1.1329 + (*... returns <ERROR> no derivation found </ERROR>*)
1.1330 +
1.1331 + val ((pt,_),_) = States.get_calc 1;
1.1332 + val p = States.get_pos 1 1;
1.1333 + val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.1334 + if UnparseC.term f = "x + 1 + - 1 * 2 = 0" andalso p = ([1], Res) then () else
1.1335 + error "FE-interface.sml: diff.behav. in FORMULA:enter} NOTok";
1.1336 +DEconstrCalcTree 1;
1.1337 +
1.1338 +"--------- replaceFormula {SOL:MAN:FOR:replace} right----"; (*UC 30.3.2.5 p.176*)
1.1339 +"--------- replaceFormula {SOL:MAN:FOR:replace} right----";
1.1340 +"--------- replaceFormula {SOL:MAN:FOR:replace} right----";
1.1341 +(*\label{SOLVE:MANUAL:FORMULA:replace}*)
1.1342 + CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.1343 + ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.1344 + ["Test", "squ-equ-test-subpbl1"]))];
1.1345 + Iterator 1;
1.1346 + moveActiveRoot 1;
1.1347 + autoCalculate 1 CompleteCalc;
1.1348 + moveActiveFormula 1 ([2],Res);
1.1349 + replaceFormula 1 "- 1 + x = 0" (*i.e. repeats input*);
1.1350 + (*... returns <ERROR> formula not changed </ERROR>*)
1.1351 +
1.1352 + val ((pt,_),_) = States.get_calc 1;
1.1353 + val p = States.get_pos 1 1;
1.1354 + val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.1355 + if UnparseC.term f = "- 1 + x = 0" andalso p = ([2], Res) then () else
1.1356 + error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
1.1357 + if map fst3 (ME_Misc.get_interval ([2],Res) ([],Res) 9999 pt) =
1.1358 + [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
1.1359 + ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else
1.1360 + error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2";
1.1361 +
1.1362 +(*WN050211 replaceFormula didn't work on second ctree: thus now tested...*)
1.1363 + CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.1364 + ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.1365 + ["Test", "squ-equ-test-subpbl1"]))];
1.1366 + Iterator 2; (*! ! ! 1 CalcTree @{context} inbetween States.reset (); *)
1.1367 + moveActiveRoot 2;
1.1368 + autoCalculate 2 CompleteCalc;
1.1369 + moveActiveFormula 2 ([2],Res);
1.1370 + replaceFormula 2 "- 1 + x = 0" (*i.e. repeats input*);
1.1371 + (*... returns <ERROR> formula not changed </ERROR>*)
1.1372 +
1.1373 + val ((pt,_),_) = States.get_calc 2;
1.1374 + val p = States.get_pos 2 1;
1.1375 + val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.1376 + if UnparseC.term f = "- 1 + x = 0" andalso p = ([2], Res) then () else
1.1377 + error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
1.1378 + if map fst3 (ME_Misc.get_interval ([2],Res) ([],Res) 9999 pt) =
1.1379 + [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
1.1380 + ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else
1.1381 + error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2b";
1.1382 +DEconstrCalcTree 1;
1.1383 +
1.1384 +"--------- replaceFormula {SOL:MAN:FOR:replace} other----"; (*UC 30.3.2.5 p.176*)
1.1385 +"--------- replaceFormula {SOL:MAN:FOR:replace} other----";
1.1386 +"--------- replaceFormula {SOL:MAN:FOR:replace} other----";
1.1387 +(*\label{SOLVE:MANUAL:FORMULA:replace}*)
1.1388 + CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.1389 + ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.1390 + ["Test", "squ-equ-test-subpbl1"]))];
1.1391 + Iterator 1;
1.1392 + moveActiveRoot 1;
1.1393 + autoCalculate 1 CompleteCalc;
1.1394 + moveActiveFormula 1 ([2],Res); (*there is "- 1 + x = 0"*)
1.1395 + replaceFormula 1 "x - 1 = 0"; (*<-------------------------------------*)
1.1396 + (*... returns calcChangedEvent with*)
1.1397 + val (unc, del, gen) = (([1],Res), ([4],Res), ([2],Res));
1.1398 + getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1.1399 +
1.1400 + val ((pt,_),_) = States.get_calc 1;
1.1401 + Test_Tool.show_pt pt;
1.1402 + val p = States.get_pos 1 1;
1.1403 + val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.1404 + if UnparseC.term f = "x - 1 = 0" andalso p = ([2], Res) then () else
1.1405 + error "FE-interface.sml: diff.behav. in FORMULA:replace} other 1";
1.1406 +(* for getting the list in whole length ...
1.1407 +(*default_print_depth 99*) map fst3 (ME_Misc.get_interval ([1],Res) ([],Res) 9999 pt); (*default_print_depth 3*)
1.1408 + *)
1.1409 + if map fst3 (ME_Misc.get_interval ([1],Res) ([],Res) 9999 pt) =
1.1410 + [([1], Res), ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
1.1411 + ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2, 7], Res),
1.1412 + ([2, 8], Res), ([2, 9], Res), ([2], Res)] then () else
1.1413 + error "FE-interface.sml: diff.behav. in FORMULA:replace} other 2";
1.1414 +DEconstrCalcTree 1;
1.1415 +
1.1416 +"--------- replaceFormula {SOL:MAN:FOR:replace} other 2--"; (*UC 30.3.2.5 p.176*)
1.1417 +"--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
1.1418 +"--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
1.1419 +(*\label{SOLVE:MANUAL:FORMULA:replace}*)
1.1420 + CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.1421 + ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.1422 + ["Test", "squ-equ-test-subpbl1"]))];
1.1423 + Iterator 1;
1.1424 + moveActiveRoot 1;
1.1425 + autoCalculate 1 CompleteCalc;
1.1426 + moveActiveFormula 1 ([2],Res); (*there is "- 1 + x = 0"*)
1.1427 + replaceFormula 1 "x = 1"; (*<-------------------------------------*)
1.1428 + (*... returns calcChangedEvent with ...*)
1.1429 + val (unc, del, gen) = (([1],Res), ([4],Res), ([3,2],Res));
1.1430 + getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1.1431 + (*9 elements !!!*)
1.1432 +
1.1433 + val ((pt,_),_) = States.get_calc 1;
1.1434 + Test_Tool.show_pt pt; (*error: ...ME_Misc.get_interval drops ([3,2],Res) ...*)
1.1435 + val (t,_) = get_obj g_result pt [3,2]; UnparseC.term t;
1.1436 + if map fst3 (ME_Misc.get_interval ([1],Res) ([],Res) 9999 pt) =
1.1437 + [([1], Res), ([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res),
1.1438 + ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
1.1439 + ([3,2],Res)] then () else
1.1440 + error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 1";
1.1441 +
1.1442 + val p = States.get_pos 1 1;
1.1443 + val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.1444 + if UnparseC.term f = "x = 1" andalso p = ([3,2], Res) then () else
1.1445 + error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 2";
1.1446 +DEconstrCalcTree 1;
1.1447 +
1.1448 +\<close> ML \<open>
1.1449 +"--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----"; (*UC 30.3.2.5 p.176*)
1.1450 +"--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
1.1451 +"--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
1.1452 +(*\label{SOLVE:MANUAL:FORMULA:replace}*)
1.1453 + CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.1454 + ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.1455 + ["Test", "squ-equ-test-subpbl1"]))];
1.1456 + Iterator 1;
1.1457 + moveActiveRoot 1;
1.1458 + autoCalculate 1 CompleteCalc;
1.1459 + moveActiveFormula 1 ([2],Res); (*there is "- 1 + x = 0"*)
1.1460 + replaceFormula 1 "x - 4711 = 0";
1.1461 + (*... returns <ERROR> no derivation found </ERROR>*)
1.1462 +
1.1463 + val ((pt,_),_) = States.get_calc 1;
1.1464 + Test_Tool.show_pt pt;
1.1465 + val p = States.get_pos 1 1;
1.1466 + val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.1467 + if UnparseC.term f = "- 1 + x = 0" andalso p = ([2], Res) then () else
1.1468 + error "FE-interface.sml: diff.behav. in FORMULA:replace} NOTok";
1.1469 + DEconstrCalcTree 1;
1.1470 +
1.1471 +"--------- UC errpat chain-rule-diff-both, fillpat by input ------";
1.1472 +"--------- UC errpat chain-rule-diff-both, fillpat by input ------";
1.1473 +"--------- UC errpat chain-rule-diff-both, fillpat by input ------";
1.1474 +CalcTree @{context}
1.1475 +[(["functionTerm (x \<up> 2 + sin (x \<up> 4))", "differentiateFor x", "derivative f_f'"],
1.1476 + ("Isac_Knowledge", ["derivative_of", "function"], ["diff", "differentiate_on_R"]))];
1.1477 +Iterator 1;
1.1478 +moveActiveRoot 1;
1.1479 +autoCalculate 1 CompleteCalcHead;
1.1480 +autoCalculate 1 (Steps 1);
1.1481 +autoCalculate 1 (Steps 1);(*([1], Res), d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))*)
1.1482 +appendFormula 1 "d_d x (x \<up> 2) + cos (4 * x \<up> 3)" (*|> Future.join*); (*<<<<<<<=========================*)
1.1483 +(* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),
1.1484 + would recognize "cos (4 * x \<up> (4 - 1)) + 2 * x" as well.
1.1485 + results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>
1.1486 + instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)
1.1487 + val ((pt,pos), _) = States.get_calc 1;
1.1488 + val p = States.get_pos 1 1;
1.1489 + val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
1.1490 +
1.1491 + if p = ([1], Res) andalso UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))"
1.1492 + then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"],
1.1493 + ("diff_sum", thm)) => () | _ => error "embed fun fill_form changed 0"
1.1494 + | _ => error "embed fun fill_form changed 1"
1.1495 +else error "embed fun fill_form changed 2";
1.1496 +
1.1497 +(*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ====================
1.1498 +findFillpatterns 1 "chain-rule-diff-both"; (*<<<<<<<=================================*)
1.1499 +(*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x \<up> 2) + d_d x (sin (x \<up> 4)) =
1.1500 + d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *)
1.1501 + val ((pt,pos),_) = States.get_calc 1;
1.1502 + val p = States.get_pos 1 1;
1.1503 +
1.1504 + val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
1.1505 + if p = ([1], Res) andalso UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" andalso
1.1506 + get_obj g_tac pt (fst p) = Rewrite_Inst (["(''bdv'', x)"], ("diff_sum", "Diff.diff_sum"(*?!?*)))
1.1507 + then ()
1.1508 + else error "embed fun fill_form changed 2";
1.1509 +
1.1510 +(* if we assume, that the fill-patterns are ordered such that the 1st has large gaps
1.1511 + and the last has no gaps, then the number of fill-patterns would suffice
1.1512 + for the DialogGuide to select appropriately. *)
1.1513 +requestFillformula 1 ("chain-rule-diff-both", "fill-both-args");(*<<<<<<<============*)
1.1514 + (*<AUTOCALC> ([1], Res) ([2], Res) ([2], Res) </AUTOCALC>*)
1.1515 + val ((pt,pos),_) = States.get_calc 1;
1.1516 + val p = States.get_pos 1 1;
1.1517 + val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
1.1518 + if p = ([1], Res) andalso existpt [2] pt andalso
1.1519 + UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up>\<up> 4))" andalso
1.1520 + get_obj g_tac pt (fst p) = Rewrite_Inst (["(''bdv'', x)"], ("diff_sum", "Diff.diff_sum"))
1.1521 + then () else error "embed fun fill_form changed 3";
1.1522 +
1.1523 +inputFillFormula 1 "d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x (x \<up> 4)";(*<<<<<<<=====*)
1.1524 + val ((pt, _),_) = States.get_calc 1;
1.1525 + val p = States.get_pos 1 1;
1.1526 + val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
1.1527 + if p = ([2], Res) andalso
1.1528 + UnparseC.term f = "d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x (x \<up> 4)" andalso
1.1529 + get_obj g_tac pt (fst p) = Rewrite_Inst (["(''bdv'', x)"], ("diff_sin_chain", ""))
1.1530 + then () else error "inputFillFormula changed 11";
1.1531 +
1.1532 +autoCalculate 1 CompleteCalc;
1.1533 +
1.1534 +"~~~~~ final check: the input formula is inserted as it would have been correct from beginning";
1.1535 +val ((pt, _),_) = States.get_calc 1;
1.1536 +val p = States.get_pos 1 1;
1.1537 +val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
1.1538 +if p = ([], Res) andalso UnparseC.term f = "2 * x + cos (x \<up> 4) * 4 * x \<up> 3"
1.1539 +then () else error "inputFillFormula changed 12";
1.1540 +Test_Tool.show_pt pt;
1.1541 +(*[
1.1542 +(([], Frm), Diff (x \<up> 2 + sin (x \<up> 4), x)),
1.1543 +(([1], Frm), d_d x (x \<up> 2 + sin (x \<up> 4))),
1.1544 +(([1], Res), d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))),
1.1545 +(([2], Res), d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x (x \<up> 4)), (*<<<<<<<=====*)
1.1546 +(([3], Res), d_d x (x \<up> 2) + cos (x \<up> 4) * (4 * x \<up> (4 - 1))),
1.1547 +(([4], Res), 2 * x \<up> (2 - 1) + cos (x \<up> 4) * (4 * x \<up> (4 - 1))),
1.1548 +(([5], Res), 2 * x + cos (x \<up> 4) * 4 * x \<up> 3),
1.1549 +(([], Res), 2 * x + cos (x \<up> 4) * 4 * x \<up> 3)] *)
1.1550 +============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*)
1.1551 +DEconstrCalcTree 1;
1.1552 +
1.1553 +\<close> ML \<open>
1.1554 +(*POSTPONE CORRECTION AT END OF TRANSITION TO Isabelle/PIDE/Isac (~ Cas_Cmd ?)
1.1555 +"--------- UC errpat add-fraction, fillpat by input --------------";
1.1556 +"--------- UC errpat add-fraction, fillpat by input --------------";
1.1557 +"--------- UC errpat add-fraction, fillpat by input --------------";
1.1558 +(*cp from BridgeLog Java <=> SML*)
1.1559 +CalcTree @{context} [([], References.empty)];
1.1560 +Iterator 1;
1.1561 +moveActiveRoot 1;
1.1562 +moveActiveFormula 1 ([],Pbl);
1.1563 +replaceFormula 1 "Simplify (5 * x / (4 * y) + 3 * x / (4 * y))";
1.1564 +autoCalculate 1 CompleteCalcHead;
1.1565 +autoCalculate 1 (Steps 1);
1.1566 +appendFormula 1 "8 * x / (8 * y)" (*|> Future.join*);
1.1567 +(*<CALCMESSAGE> no derivation found </CALCMESSAGE>
1.1568 +--- but in BridgeLog Java <=> SML:
1.1569 +<CALCMESSAGE> error pattern #addition-of-fractions# </CALCMESSAGE>*)
1.1570 +DEconstrCalcTree 1;
1.1571 +-----------------------------------------------------------------------------------------------*)
1.1572 +
1.1573 +\<close> ML \<open>
1.1574 +"--------- UC errpat, fillpat step to Rewrite --------------------";
1.1575 +"--------- UC errpat, fillpat step to Rewrite --------------------";
1.1576 +"--------- UC errpat, fillpat step to Rewrite --------------------";
1.1577 +(*TODO*)
1.1578 +CalcTree @{context}
1.1579 +[(["functionTerm ((x \<up> 2) \<up> 3 + sin (x \<up> 4))",
1.1580 + "differentiateFor x", "derivative f_f'"],
1.1581 + ("Isac_Knowledge", ["derivative_of", "function"],
1.1582 + ["diff", "differentiate_on_R"]))]; (*<<<======= EP is directly in script*)
1.1583 +Iterator 1;
1.1584 +moveActiveRoot 1;
1.1585 +autoCalculate 1 CompleteCalc;
1.1586 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
1.1587 +DEconstrCalcTree 1;
1.1588 +
1.1589 +\<close> ML \<open>
1.1590 +"--------- UC errpat, fillpat step to Rewrite_Set ----------------";
1.1591 +"--------- UC errpat, fillpat step to Rewrite_Set ----------------";
1.1592 +"--------- UC errpat, fillpat step to Rewrite_Set ----------------";
1.1593 +CalcTree @{context}
1.1594 +[(["functionTerm ((x \<up> 2) \<up> 3 + sin (x \<up> 4))",
1.1595 + "differentiateFor x", "derivative f_f'"],
1.1596 + ("Isac_Knowledge", ["derivative_of", "function"],
1.1597 + ["diff", "after_simplification"]))]; (*<<<======= EP is in a ruleset*)
1.1598 +Iterator 1;
1.1599 +moveActiveRoot 1;
1.1600 +autoCalculate 1 CompleteCalcHead;
1.1601 +autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.1602 +autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.1603 +(*
1.1604 +<NEXTTAC>
1.1605 + <CALCID> 1 </CALCID>
1.1606 + <TACTICERRORPATTERNS>
1.1607 + <STRINGLIST>
1.1608 + <STRING> chain-rule-diff-both </STRING>
1.1609 + <STRING> cancel </STRING>
1.1610 + </STRINGLIST>
1.1611 + <REWRITESETINSTTACTIC name="Rewrite_Set_Inst">
1.1612 + <RULESET> norm_diff </RULESET>
1.1613 + <SUBSTITUTION>
1.1614 + <PAIR>
1.1615 + <VARIABLE>
1.1616 + <MATHML>
1.1617 + <ISA> bdv </ISA>
1.1618 + </MATHML>
1.1619 + </VARIABLE>
1.1620 + <VALUE>
1.1621 + <MATHML>
1.1622 + <ISA> x </ISA>
1.1623 + </MATHML>
1.1624 + </VALUE>
1.1625 + </PAIR>
1.1626 + </SUBSTITUTION>
1.1627 + </REWRITESETINSTTACTIC>
1.1628 + </TACTICERRORPATTERNS>
1.1629 +</NEXTTAC>
1.1630 +
1.1631 +
1.1632 +(*WN1208 postponed due to efforts required for stepToErrorPatterns (NEW rewrite_set_)*)
1.1633 +stepToErrorPatterns 1; (*--> calcChanged, rule immediately calls... *)
1.1634 +stepOnErrorPatterns 1; (*--> calcChanged, rule calls getTactic and displays it *)
1.1635 +(* then --- UC errpat, fillpat by input ---*)
1.1636 +*)
1.1637 +autoCalculate 1 CompleteCalc;
1.1638 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
1.1639 +(*WN1208 postponed due to efforts required for stepToErrorPatterns (NEW rewrite_set_)*)
1.1640 +DEconstrCalcTree 1;
1.1641 +
1.1642 \<close> ML \<open>
1.1643 \<close> ML \<open>
1.1644 \<close>