1.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Thu Oct 20 10:23:38 2022 +0200
1.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Thu Oct 20 10:47:52 2022 +0200
1.3 @@ -181,9 +181,7 @@
1.4 else
1.5 case LItool.check_leaf "next " ctxt eval (get_subst ist) t of
1.6 (Program.Expr s, _) => Term_Val s (*TODO?: include set_found here and drop those after call*)
1.7 - | (Program.Tac prog_tac, form_arg) =>
1.8 - (tracing ("### scan_dn fall-through, prog_tac = " ^ quote (UnparseC.term prog_tac) ^ " |");
1.9 -check_tac cc ist (prog_tac, form_arg))
1.10 + | (Program.Tac prog_tac, form_arg) => check_tac cc ist (prog_tac, form_arg)
1.11
1.12 fun go_scan_up (pcc as (sc, _)) (ist as {path, act_arg, found_accept, ...}) =
1.13 if path = [R] (*root of the program body*) then
2.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Thu Oct 20 10:23:38 2022 +0200
2.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Thu Oct 20 10:47:52 2022 +0200
2.3 @@ -1532,6 +1532,7 @@
2.4 ============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*)
2.5 DEconstrCalcTree 1;
2.6
2.7 +(*POSTPONE CORRECTION AT END OF TRANSITION TO Isabelle/PIDE/Isac (~ Cas_Cmd ?)
2.8 "--------- UC errpat add-fraction, fillpat by input --------------";
2.9 "--------- UC errpat add-fraction, fillpat by input --------------";
2.10 "--------- UC errpat add-fraction, fillpat by input --------------";
2.11 @@ -1548,6 +1549,7 @@
2.12 --- but in BridgeLog Java <=> SML:
2.13 <CALCMESSAGE> error pattern #addition-of-fractions# </CALCMESSAGE>*)
2.14 DEconstrCalcTree 1;
2.15 +-----------------------------------------------------------------------------------------------*)
2.16
2.17 "--------- UC errpat, fillpat step to Rewrite --------------------";
2.18 "--------- UC errpat, fillpat step to Rewrite --------------------";
3.1 --- a/test/Tools/isac/Test_Isac.thy Thu Oct 20 10:23:38 2022 +0200
3.2 +++ b/test/Tools/isac/Test_Isac.thy Thu Oct 20 10:47:52 2022 +0200
3.3 @@ -317,1638 +317,6 @@
3.4
3.5 section \<open>further tests additional to src/.. files\<close>
3.6 ML_file "BridgeLibisabelle/use-cases.sml"
3.7 -ML \<open>
3.8 -\<close> ML \<open>
3.9 -\<close> ML \<open>
3.10 -(* Title: tests the interface of isac's SML-kernel in accordance to
3.11 - java-tests/isac.bridge.
3.12 - Author: Walther Neuper
3.13 - (c) copyright due to lincense terms.
3.14 -
3.15 -Tests the interface of isac's SML-kernel in accordance to java-tests/isac.bridge.
3.16 -Some tests are outcommented since "eliminate ThmC.numerals_to_Free";
3.17 -these are considered irrelevant for Isabelle/Isac.
3.18 -
3.19 -WN050707 ... if true, the test ist marked with a \label referring
3.20 -to the same UC in isac-docu.tex as the JUnit testcase.
3.21 -WN120210?not ME: added some labels, which are not among the above,
3.22 -repaired lost \label (s).
3.23 -
3.24 -theory Test_Some imports Isac.Build_Thydata begin
3.25 -ML {* KEStore_Elems.set_ref_thy @{theory};
3.26 - fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*) *}
3.27 -ML_file "Frontend/use-cases.sml"
3.28 -*)
3.29 -
3.30 -"--------------------------------------------------------";
3.31 -"table of contents --------------------------------------";
3.32 -"--------------------------------------------------------";
3.33 -"within struct ------------------------------------------";
3.34 -"--------------------------------------------------------";
3.35 -"--------- encode ^ -> ^^ ------------------------------";
3.36 -"--------------------------------------------------------";
3.37 -"exported from struct -----------------------------------";
3.38 -"--------------------------------------------------------";
3.39 -(*"--------- empty rootpbl --------------------------------";*)
3.40 -"--------- solve_linear as rootpbl FE -------------------";
3.41 -"--------- inspect the CalcTree @{context} No.1 with Iterator No.2 -";
3.42 -"--------- miniscript with mini-subpbl ------------------";
3.43 -"--------- mini-subpbl AUTOCALCULATE Steps 1 ------------";
3.44 -"--------- solve_linear as rootpbl AUTO CompleteCalc ----";
3.45 -"--------- solve_linear as rootpbl AUTO CompleteHead/Eval ";
3.46 -"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
3.47 -"--------- mini-subpbl AUTO CompleteCalcHead ------------";
3.48 -"--------- solve_linear as rootpbl AUTO CompleteModel ---";
3.49 -"--------- setContext..Thy ------------------------------";
3.50 -"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
3.51 -"--------- rat-eq + subpbl: no_met, NO solution dropped - WITH fun me IN test/../solve.sml";
3.52 -"--------- tryMatchProblem, tryRefineProblem ------------";
3.53 -"--------- modifyCalcHead, resetCalcHead, modelProblem --";
3.54 -"--------- maximum-example, UC: Modeling an example -----";
3.55 -"--------- solve_linear from pbl-hierarchy --------------";
3.56 -"--------- solve_linear as in an algebra system (CAS)----";
3.57 -"--------- interSteps: on 'miniscript with mini-subpbl' -";
3.58 -"--------- getTactic, fetchApplicableTactics ------------";
3.59 -"--------- getAssumptions, getAccumulatedAsms -----------";
3.60 -"--------- arbitrary combinations of steps --------------";
3.61 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
3.62 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
3.63 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
3.64 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
3.65 -"--------- replaceFormula {SOL:MAN:FOR:replace} right----";
3.66 -"--------- replaceFormula {SOL:MAN:FOR:replace} other----";
3.67 -"--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
3.68 -"--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
3.69 -"--------- UC errpat chain-rule-diff-both, fillpat by input ------";
3.70 -"--------- UC errpat add-fraction, fillpat by input --------------";
3.71 -"--------- UC errpat, fillpat step to Rewrite --------------------";
3.72 -"--------- UC errpat, fillpat step to Rewrite_Set ----------------";
3.73 -"--------------------------------------------------------";
3.74 -
3.75 -"within struct ---------------------------------------------------";
3.76 -"within struct ---------------------------------------------------";
3.77 -"within struct ---------------------------------------------------";
3.78 -(*==================================================================
3.79 -
3.80 -==================================================================*)
3.81 -"exported from struct --------------------------------------------";
3.82 -"exported from struct --------------------------------------------";
3.83 -"exported from struct --------------------------------------------";
3.84 -
3.85 -
3.86 -(*------------ set at startup of the Kernel ----------------------*)
3.87 -States.reset (); (*resets all state information in Kernel *)
3.88 -(*----------------------------------------------------------------*)
3.89 -
3.90 -(*---------------------------------------------------- postpone to Outer_Syntax..Example -----
3.91 -"--------- empty rootpbl --------------------------------";
3.92 -"--------- empty rootpbl --------------------------------";
3.93 -"--------- empty rootpbl --------------------------------";
3.94 - CalcTree @{context} [([], ("", [], []))];
3.95 - Iterator 1;
3.96 - moveActiveRoot 1;
3.97 - refFormula 1 (States.get_pos 1 1);
3.98 -(*WN.040222: stoert das sehr, dass ThyC.id_empty etc. statt leer kommt ???*)
3.99 -DEconstrCalcTree 1;
3.100 ------------------------------------------------------- postpone to Outer_Syntax..Example -----*)
3.101 -
3.102 -"--------- solve_linear as rootpbl FE -------------------";
3.103 -"--------- solve_linear as rootpbl FE -------------------";
3.104 -"--------- solve_linear as rootpbl FE -------------------";
3.105 -States.reset ();
3.106 -
3.107 - CalcTree @{context} (*start of calculation, return No.1*)
3.108 - [(["equality (1+- 1*2+x=(0::real))", "solveFor x", "solutions L"],
3.109 - ("Test",
3.110 - ["LINEAR", "univariate", "equation", "test"],
3.111 - ["Test", "solve_linear"]))];
3.112 - Iterator 1; (*create an active Iterator on CalcTree @{context} No.1*)
3.113 -
3.114 - moveActiveRoot 1;(*sets the CalcIterator No.1 at the root of CalcTree @{context} No.1*);
3.115 - refFormula 1 (States.get_pos 1 1) (*gets CalcHead; model is still empty*);
3.116 -
3.117 -
3.118 -(*1*) fetchProposedTactic 1 (*by using Iterator No.1*);
3.119 - setNextTactic 1 (Model_Problem); (*by using Iterator No.1*)
3.120 - autoCalculate 1 (Steps 1);
3.121 - refFormula 1 (States.get_pos 1 1) (*model contains descriptions for all items*);
3.122 - autoCalculate 1 (Steps 1);
3.123 -(*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
3.124 -(*2*) fetchProposedTactic 1;
3.125 - setNextTactic 1 (Add_Given "equality (1 + - 1 * 2 + x = 0)");
3.126 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1); (*equality added*);
3.127 -
3.128 -(*3*) fetchProposedTactic 1;
3.129 - setNextTactic 1 (Add_Given "solveFor x");
3.130 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.131 -
3.132 -(*4*) fetchProposedTactic 1;
3.133 - setNextTactic 1 (Add_Find "solutions L");
3.134 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.135 -
3.136 -(*5*) fetchProposedTactic 1;
3.137 - setNextTactic 1 (Specify_Theory "Test");
3.138 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.139 -*-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
3.140 -
3.141 -(*6*) fetchProposedTactic 1;
3.142 - setNextTactic 1 (Specify_Problem ["LINEAR", "univariate", "equation", "test"]);
3.143 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.144 -(*-------------------------------------------------------------------------*)
3.145 -(*7*) fetchProposedTactic 1;
3.146 - val (ptp as (pt,p), tacis) = States.get_calc 1; States.get_pos 1 1;
3.147 -
3.148 - setNextTactic 1 (Specify_Method ["Test", "solve_linear"]);
3.149 - val (ptp as (pt,p), tacis) = States.get_calc 1; States.get_pos 1 1;
3.150 -
3.151 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.152 - val (ptp as (pt,p), tacis) = States.get_calc 1; States.get_pos 1 1;
3.153 -
3.154 -(*-------------------------------------------------------------------------*)
3.155 -(*8*) fetchProposedTactic 1;
3.156 - val (ptp as (pt,p), tacis) = States.get_calc 1; States.get_pos 1 1;
3.157 -
3.158 -(*8*) setNextTactic 1 (Apply_Method ["Test", "solve_linear"]);
3.159 - (*ERROR.110620 <SETNEXTTACTIC>..<MESSAGE> end-of-calculation*)
3.160 - val (ptp as (pt,p), tacis) = States.get_calc 1; States.get_pos 1 1;
3.161 - SpecificationC.is_complete ptp;
3.162 - References.are_complete ptp;
3.163 -
3.164 -(*8*) autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1); (*<---------------------- orig. test code*)
3.165 -
3.166 - val (ptp as (pt,p), tacis) = States.get_calc 1; States.get_pos 1 1; (*<---------------------- orig. test code*)
3.167 -(*+isa=REP*) if p = ([1], Frm) andalso UnparseC.term (get_obj g_form pt [1]) = "1 + - 1 * 2 + x = 0"
3.168 -andalso Istate.string_of (get_istate_LI pt p)
3.169 - = "Pstate ([\"\n(e_e, 1 + - 1 * 2 + x = 0)\", \"\n(v_v, x)\"], [], empty, NONE, \n??.empty, ORundef, false, true)"
3.170 -then () else error "refFormula = 1 + - 1 * 2 + x = 0 changed";
3.171 -(*-------------------------------------------------------------------------*)
3.172 -
3.173 -(*9*) fetchProposedTactic 1; (*<----------------------------------------------------- orig. test code*)
3.174 -(*+\\------------------------------------------ isa == REP -----------------------------------//* )
3.175 -(*+//========================================== isa <> REP (1) ===============================\\*)
3.176 -(*9*) setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "isolate_bdv")); ( *<------- orig. test code*)
3.177 -
3.178 -"~~~~~ fun setNextTactic , args:"; val (cI, tac) = (1, (Rewrite_Set_Inst (["(''bdv'',x)"], "isolate_bdv")));
3.179 - val ((pt'''''_', _), _) = States.get_calc cI
3.180 - val ip'''''_' = States.get_pos cI 1;
3.181 -
3.182 - val xxxxx_x(*"ok", (tacis, _, _)*) = (*case*) Step.by_tactic tac (pt'''''_', ip'''''_') (*of*);
3.183 -(*+isa+REP*)val ("ok", ( [ (Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv"),
3.184 - Rewrite_Set_Inst' _, (pos', (istate, ctxt))) ] , _, cstate)) = xxxxx_x;
3.185 -
3.186 -(*//******************* Step.by_tactic returns tac_ + istate + cstate *****************************\\*)
3.187 -Step.by_tactic : Tactic.input -> state -> string * (State_Steps.T * pos' list * state);
3.188 -if Istate.string_of istate
3.189 - = "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)"
3.190 -then () else error "from Step.by_tactic return --- changed 1";
3.191 -
3.192 -if Istate.string_of (get_istate_LI (fst cstate) (snd cstate))
3.193 - = "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)"
3.194 -then () else error "from Step.by_tactic return --- changed 2";
3.195 -(*\\******************* Step.by_tactic returns tac_ + istate + cstate *****************************//*)
3.196 -
3.197 -"~~~~~ fun Step.by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt'''''_', ip'''''_'));
3.198 - val Applicable.Yes m = (*case*) Step.check tac (pt, p) (*of*);
3.199 - (*if*) Tactic.for_specify' m; (*false*)
3.200 -
3.201 -Step_Solve.by_tactic m (pt, p);
3.202 -"~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, p));
3.203 - (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p); (*else*)
3.204 - val thy' = get_obj g_domID pt (par_pblobj pt p);
3.205 - val (is, sc) = LItool.resume_prog (p,p_) pt;
3.206 - val Safe_Step (istate, _, tac) =
3.207 - (*case*) LI.locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*);
3.208 -
3.209 -(*+*)Safe_Step: Istate.T * Proof.context * Tactic.T -> input_tactic_result;
3.210 -(********************* locate_input_tactic returns cstate * istate * Proof.context *************)
3.211 -(*+*)if Istate.string_of istate
3.212 -(*+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)"
3.213 -then case m of Rewrite_Set_Inst' _ => ()
3.214 -else error "from locate_input_tactic return --- changed";
3.215 -
3.216 -val ("ok", (tacis'''''_', _, _)) = xxxxx_x;
3.217 -"~~~~~ from TOPLEVEL to states return:"; States.upd_calc cI ((pt'''''_', ip'''''_'), tacis'''''_');
3.218 -(*\\=========================================== isa <> REP (1) ===============================//*)
3.219 -(*//=========================================== isa <> REP (2) ===============================\\*)
3.220 -(*9* ) autoCalculate 1 (Steps 1); (*<-------------------------------------------------- orig. test code*)
3.221 -( *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>*)
3.222 -
3.223 -"~~~~~ fun autoCalculate , args:"; val (cI, auto) = (1, (Steps 1));
3.224 - val pold = States.get_pos cI 1;
3.225 - val xxx = (States.get_calc cI);
3.226 -(*isa*) val (**)xxxx(**) (**) = (**)
3.227 - (*case*) Math_Engine.autocalc [] pold (xxx) auto (*of*);
3.228 -"~~~~~ fun autocalc , args:"; val (c, ip, cs, (Solve.Steps s)) = ([], pold, (xxx), auto);
3.229 - (*if*) s <= 1; (*then*)
3.230 - (*val (str, (_, c', ptp)) =*)
3.231 -
3.232 -Step.do_next ip cs;
3.233 -"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt,p), tacis)) = (ip, cs);
3.234 -
3.235 -(*+isa==REP*)val [(Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv"),
3.236 - Rewrite_Set_Inst' _, (pos', (istate, ctxt)))] = tacis;
3.237 -(*+*)if pos' = ([1], Res) andalso Istate.string_of istate
3.238 - = "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)"
3.239 -then () else error "init. step 1 + - 1 * 2 + x = 0 changed";
3.240 -
3.241 - val pIopt = get_pblID (pt,ip);
3.242 - (*if*) ip = ([], Pos.Res);(*else*)
3.243 - val (_::_) = (*case*) tacis (*of*);
3.244 -(*isa==REP*) (*if*) ip = p;(*then*)
3.245 - (*val (pt',c',p') =*) Solve_Step.s_add_general tacis (pt,[],p);
3.246 -(*//------------------------------------- final test -----------------------------------------\\*)
3.247 -val ("ok", [], ptp as (pt, p)) = xxxx;
3.248 -
3.249 -if Istate.string_of (get_istate_LI pt p) (* <> <> <> <> \<up> \<up> \<up> \<up> ^*)
3.250 -(*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)"
3.251 -then () else error "REP autoCalculate on (e_e, 1 + - 1 * 2 + x = 0) changed"
3.252 -
3.253 -"~~~~~ from TOPLEVEL to states return:"; States.upd_calc cI (ptp, []); States.upd_ipos cI 1 p;
3.254 -(*\\=========================================== isa <> REP (2) ===============================//*)
3.255 -
3.256 -(*10*) fetchProposedTactic 1;
3.257 - setNextTactic 1 (Rewrite_Set "Test_simplify");
3.258 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.259 -
3.260 -(*11*) fetchProposedTactic 1;
3.261 - setNextTactic 1 (Check_Postcond ["LINEAR", "univariate", "equation", "test"]);
3.262 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.263 -
3.264 -(*======= final test ==================================================*)
3.265 - val ((pt,_),_) = States.get_calc 1;
3.266 - val ip = States.get_pos 1 1;
3.267 -
3.268 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, ip);
3.269 - (*exception just above means: 'ModSpec' has been returned: error anyway*)
3.270 - if ip = ([], Res) andalso UnparseC.term f = "[x = 1]" then () else
3.271 - error "FE-Kernel-interface.sml: diff.behav. in solve_linear as rootpbl";
3.272 -
3.273 -
3.274 -"--------- inspect the CalcTree @{context} No.1 with Iterator No.2 -";
3.275 -"--------- inspect the CalcTree @{context} No.1 with Iterator No.2 -";
3.276 -"--------- inspect the CalcTree @{context} No.1 with Iterator No.2 -";
3.277 -(*WN041118: inspection shifted to Iterator No.1, because others need pos'*)
3.278 -(*-------- WN190723: doesnt work since changeset 59474 21d4d2868b83
3.279 - moveActiveRoot 1;
3.280 - refFormula 1 ([],Pbl); getTactic 1 ([],Pbl);(*Error*)
3.281 - moveActiveDown 1;
3.282 - refFormula 1 ([1],Frm); getTactic 1 ([1],Frm);(*Error*)
3.283 - moveActiveDown 1 ;
3.284 - refFormula 1 ([1],Res); getTactic 1 ([1],Res);(*OK*)
3.285 - (*getAssumption 1 ([1],Res); TODO.WN041217*)
3.286 - moveActiveDown 1 ; refFormula 1 ([2],Res);
3.287 - moveActiveCalcHead 1; refFormula 1 ([],Pbl);
3.288 - moveActiveDown 1;
3.289 - moveActiveDown 1;
3.290 - moveActiveDown 1;
3.291 - if States.get_pos 1 1 = ([2], Res) then () else
3.292 - error "FE-interface.sml: diff.behav. in a inspect 1 with Iterator 2";
3.293 - moveActiveDown 1; refFormula 1 ([], Res);
3.294 - if States.get_pos 1 1 = ([], Res) then () else
3.295 - error "FE-interface.sml: diff.behav. in b inspect 1 with Iterator 2";
3.296 - moveActiveCalcHead 1; refFormula 1 ([],Pbl);
3.297 -DEconstrCalcTree 1;
3.298 -------------------------------------------------------------------------------------------------*)
3.299 -
3.300 -"--------- miniscript with mini-subpbl ------------------";
3.301 -"--------- miniscript with mini-subpbl ------------------";
3.302 -"--------- miniscript with mini-subpbl ------------------";
3.303 -(*WN120210?not ME:\label{SOLVE:MANUAL:TACTIC:enter} UC 30.3.2.1 p.175 !!!!!NOT IMPL IN FE*)
3.304 -"=== this sequence of fun-calls resembles fun me ===";
3.305 - CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
3.306 - ("Test", ["sqroot-test", "univariate", "equation", "test"],
3.307 - ["Test", "squ-equ-test-subpbl1"]))];
3.308 - Iterator 1;
3.309 -
3.310 - moveActiveRoot 1;
3.311 - refFormula 1 (States.get_pos 1 1);
3.312 - fetchProposedTactic 1;
3.313 - setNextTactic 1 (Model_Problem);
3.314 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*gets ModSpec;model is still empty*)
3.315 -
3.316 - fetchProposedTactic 1; (*<SYSERROR><CALCID>1</CALCID><ERROR>error in kernel 3</ERROR></SYSERROR>* )
3.317 - setNextTactic 1 (Add_Given "equality (x + 1 = 2)");
3.318 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.319 -
3.320 - fetchProposedTactic 1;
3.321 - setNextTactic 1 (Add_Given "solveFor x");
3.322 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.323 -
3.324 - fetchProposedTactic 1;
3.325 - setNextTactic 1 (Add_Find "solutions L");
3.326 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.327 -
3.328 - fetchProposedTactic 1;
3.329 - setNextTactic 1 (Specify_Theory "Test");
3.330 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.331 -
3.332 - fetchProposedTactic 1;
3.333 - setNextTactic 1 (Specify_Problem
3.334 - ["sqroot-test", "univariate", "equation", "test"]);
3.335 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.336 -"1-----------------------------------------------------------------";
3.337 -
3.338 - fetchProposedTactic 1;
3.339 - setNextTactic 1 (Specify_Method ["Test", "squ-equ-test-subpbl1"]);
3.340 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.341 -
3.342 - fetchProposedTactic 1;
3.343 - setNextTactic 1 (Apply_Method ["Test", "squ-equ-test-subpbl1"]);
3.344 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.345 -
3.346 - fetchProposedTactic 1;
3.347 - setNextTactic 1 (Rewrite_Set "norm_equation");
3.348 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.349 -
3.350 - fetchProposedTactic 1;
3.351 - setNextTactic 1 (Rewrite_Set "Test_simplify");
3.352 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.353 -
3.354 - fetchProposedTactic 1;(*----------------Subproblem--------------------*);
3.355 - setNextTactic 1 (Subproblem ("Test",
3.356 - ["LINEAR", "univariate", "equation", "test"]));
3.357 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.358 -
3.359 - fetchProposedTactic 1;
3.360 - setNextTactic 1 (Model_Problem );
3.361 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.362 -
3.363 - fetchProposedTactic 1;
3.364 - setNextTactic 1 (Add_Given "equality (- 1 + x = 0)");
3.365 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.366 -
3.367 - fetchProposedTactic 1;
3.368 - setNextTactic 1 (Add_Given "solveFor x");
3.369 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.370 -
3.371 - fetchProposedTactic 1;
3.372 - setNextTactic 1 (Add_Find "solutions x_i");
3.373 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.374 -
3.375 - fetchProposedTactic 1;
3.376 - setNextTactic 1 (Specify_Theory "Test");
3.377 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.378 -
3.379 - fetchProposedTactic 1;
3.380 - setNextTactic 1 (Specify_Problem ["LINEAR", "univariate", "equation", "test"]);
3.381 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.382 -"2-----------------------------------------------------------------";
3.383 -
3.384 - fetchProposedTactic 1;
3.385 - setNextTactic 1 (Specify_Method ["Test", "solve_linear"]);
3.386 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.387 -
3.388 - fetchProposedTactic 1;
3.389 - setNextTactic 1 (Apply_Method ["Test", "solve_linear"]);
3.390 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.391 -
3.392 - fetchProposedTactic 1;
3.393 - setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "isolate_bdv"));
3.394 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.395 -
3.396 - fetchProposedTactic 1;
3.397 - setNextTactic 1 (Rewrite_Set "Test_simplify");
3.398 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.399 -
3.400 - fetchProposedTactic 1;
3.401 - setNextTactic 1 (Check_Postcond ["LINEAR", "univariate", "equation", "test"]);
3.402 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.403 -
3.404 - fetchProposedTactic 1;
3.405 - setNextTactic 1 (Check_elementwise "Assumptions");
3.406 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.407 -
3.408 - val xml = fetchProposedTactic 1;
3.409 - setNextTactic 1 (Check_Postcond
3.410 - ["sqroot-test", "univariate", "equation", "test"]);
3.411 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.412 -
3.413 - val ((pt,_),_) = States.get_calc 1;
3.414 - val str = pr_ctree pr_short pt;
3.415 - writeln str;
3.416 - val ip = States.get_pos 1 1;
3.417 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, ip);
3.418 - (*exception just above means: 'ModSpec' has been returned: error anyway*)
3.419 - if UnparseC.term f = "[x = 1]" then () else
3.420 - error "FE-interface.sml: diff.behav. in miniscript with mini-subpb";
3.421 -(**)-------------------------------------------------------------------------------------------*)
3.422 - DEconstrCalcTree 1;
3.423 -
3.424 -"--------- mini-subpbl AUTOCALCULATE Steps 1 -------------";
3.425 -"--------- mini-subpbl AUTOCALCULATE Steps 1 -------------";
3.426 -"--------- mini-subpbl AUTOCALCULATE Steps 1 -------------";
3.427 -(*WN120210?not ME:\label{SOLVE:AUTO:one} UC 30.3.3.2 p.176*)
3.428 - CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
3.429 - ("Test", ["sqroot-test", "univariate", "equation", "test"],
3.430 - ["Test", "squ-equ-test-subpbl1"]))];
3.431 - Iterator 1;
3.432 - moveActiveRoot 1;
3.433 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.434 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.435 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.436 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.437 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.438 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.439 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.440 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.441 - (*here the solve-phase starts*)
3.442 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.443 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.444 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.445 - (*------------------------------------*)
3.446 -(* (*default_print_depth 13*) States.get_calc 1;
3.447 - *)
3.448 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.449 - (*calc-head of subproblem*)
3.450 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.451 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.452 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.453 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.454 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.455 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.456 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.457 - (*solve-phase of the subproblem*)
3.458 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.459 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.460 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.461 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.462 - (*finish subproblem*)
3.463 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.464 - (*finish problem*)
3.465 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.466 -
3.467 - (*this checks the test for correctness..*)
3.468 - val ((pt,_),_) = States.get_calc 1;
3.469 - val p = States.get_pos 1 1;
3.470 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
3.471 - if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
3.472 - error "FE-interface.sml: diff.behav. in miniscript with mini-subpb";
3.473 - DEconstrCalcTree 1;
3.474 -
3.475 -
3.476 -"--------- solve_linear as rootpbl AUTO CompleteCalc ----";
3.477 -"--------- solve_linear as rootpbl AUTO CompleteCalc ----";
3.478 -"--------- solve_linear as rootpbl AUTO CompleteCalc ----";
3.479 -(*WN120210?not ME:\label{SPECIFY:START:auto} UC 30.2.4.2 p.174*)
3.480 - CalcTree @{context}
3.481 - [(["equality (1+- 1*2+x=(0::real))", "solveFor x", "solutions L"],
3.482 - ("Test",
3.483 - ["LINEAR", "univariate", "equation", "test"],
3.484 - ["Test", "solve_linear"]))];
3.485 - Iterator 1;
3.486 - moveActiveRoot 1;
3.487 -getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 999 false;
3.488 -
3.489 - autoCalculate 1 CompleteCalc;
3.490 - val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
3.491 - getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
3.492 -
3.493 - val ((pt,_),_) = States.get_calc 1;
3.494 - val p = States.get_pos 1 1;
3.495 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
3.496 - if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
3.497 - error "FE-interface.sml: diff.behav. in solve_linear/rt AUTOCALCULATE ";
3.498 -DEconstrCalcTree 1;
3.499 -
3.500 -"--------- solve_linear as rootpbl AUTO CompleteHead/Eval ";
3.501 -"--------- solve_linear as rootpbl AUTO CompleteHead/Eval ";
3.502 -"--------- solve_linear as rootpbl AUTO CompleteHead/Eval ";
3.503 -(* ERROR: error in kernel ?? *)
3.504 - CalcTree @{context}
3.505 - [(["equality (1+- 1*2+x=(0::real))", "solveFor x", "solutions L"],
3.506 - ("Test",
3.507 - ["LINEAR", "univariate", "equation", "test"],
3.508 - ["Test", "solve_linear"]))];
3.509 - Iterator 1;
3.510 - moveActiveRoot 1;
3.511 -
3.512 - autoCalculate 1 CompleteCalcHead;
3.513 - refFormula 1 (States.get_pos 1 1);
3.514 - val ((pt,p),_) = States.get_calc 1;
3.515 -
3.516 - autoCalculate 1 CompleteCalc;
3.517 - val ((pt,p),_) = States.get_calc 1;
3.518 - if p=([], Res) then () else
3.519 - error "FE-interface.sml: diff.behav. in solve_linear AUTOC Head/Eval ";
3.520 -DEconstrCalcTree 1;
3.521 -
3.522 -"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
3.523 -"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
3.524 -"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
3.525 -(*WN120210?not ME:\label{SPECIFY:START:auto} UC 30.2.4.2 p.174*)
3.526 - CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
3.527 - ("Test", ["sqroot-test", "univariate", "equation", "test"],
3.528 - ["Test", "squ-equ-test-subpbl1"]))];
3.529 - Iterator 1;
3.530 - moveActiveRoot 1;
3.531 - autoCalculate 1 CompleteCalc;
3.532 - val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
3.533 -(*
3.534 -getTactic 1 ([1],Frm);
3.535 -getTactic 1 ([1],Res);
3.536 -initContext 1 Ptool.Thy_ ([1],Res);
3.537 -*)
3.538 - (*... returns calcChangedEvent with*)
3.539 - val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
3.540 - getFormulaeFromTo 1 unc gen 0 (*only result*) false;
3.541 - getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
3.542 - getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
3.543 -
3.544 - val ((pt,_),_) = States.get_calc 1;
3.545 - val p = States.get_pos 1 1;
3.546 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
3.547 - if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
3.548 - error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
3.549 - DEconstrCalcTree 1;
3.550 -
3.551 -"--------- mini-subpbl AUTO CompleteCalcHead ------------";
3.552 -"--------- mini-subpbl AUTO CompleteCalcHead ------------";
3.553 -"--------- mini-subpbl AUTO CompleteCalcHead ------------";
3.554 - CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
3.555 - ("Test", ["sqroot-test", "univariate", "equation", "test"],
3.556 - ["Test", "squ-equ-test-subpbl1"]))];
3.557 - Iterator 1;
3.558 - moveActiveRoot 1;
3.559 - autoCalculate 1 CompleteCalcHead;
3.560 -
3.561 -val ((Nd (PblObj {fmz = (fm, ("Test", pblID, metID)), loc = (SOME (env, ctxt1), NONE),
3.562 - meth, probl,
3.563 - spec = ("Test", ["sqroot-test", "univariate", "equation", "test"],
3.564 - ["Test", "squ-equ-test-subpbl1"]),
3.565 - branch = TransitiveB, ostate = Incomplete (*!?\<forall>*), ...}, []),
3.566 - ([], Met)), []) = States.get_calc 1;
3.567 -if length meth = 3 andalso length probl = 3 (*just some items tested*) then ()
3.568 -else error "--- mini-subpbl AUTO CompleteCalcHead ---";
3.569 -DEconstrCalcTree 1;
3.570 -
3.571 -"--------- solve_linear as rootpbl AUTO CompleteModel ---";
3.572 -"--------- solve_linear as rootpbl AUTO CompleteModel ---";
3.573 -"--------- solve_linear as rootpbl AUTO CompleteModel ---";
3.574 -States.reset ();
3.575 - CalcTree @{context}
3.576 - [(["equality (1+- 1*2+x=(0::real))", "solveFor x", "solutions L"],
3.577 - ("Test",
3.578 - ["LINEAR", "univariate", "equation", "test"],
3.579 - ["Test", "solve_linear"]))];
3.580 - Iterator 1;
3.581 - moveActiveRoot 1;
3.582 - autoCalculate 1 CompleteModel;
3.583 - refFormula 1 (States.get_pos 1 1);
3.584 -
3.585 -setProblem 1 ["LINEAR", "univariate", "equation", "test"];
3.586 -val pos = States.get_pos 1 1;
3.587 -(*setContext 1 pos (Ptool.kestoreID2guh Ptool.Pbl_["LINEAR", "univariate", "equation", "test"]);*)
3.588 - refFormula 1 (States.get_pos 1 1);
3.589 -
3.590 -setMethod 1 ["Test", "solve_linear"];
3.591 -(*setContext 1 pos (Ptool.kestoreID2guh Ptool.Met_ ["Test", "solve_linear"]);*)
3.592 - refFormula 1 (States.get_pos 1 1);
3.593 - val ((pt,_),_) = States.get_calc 1;
3.594 - if get_obj g_spec pt [] = (ThyC.id_empty,
3.595 - ["LINEAR", "univariate", "equation", "test"],
3.596 - ["Test", "solve_linear"]) then ()
3.597 - else error "FE-interface.sml: diff.behav. in setProblem, setMethod";
3.598 -
3.599 - autoCalculate 1 CompleteCalcHead;
3.600 - refFormula 1 (States.get_pos 1 1);
3.601 - autoCalculate 1 CompleteCalc;
3.602 - moveActiveDown 1;
3.603 - moveActiveDown 1;
3.604 - moveActiveDown 1;
3.605 - refFormula 1 (States.get_pos 1 1);
3.606 - val ((pt,_),_) = States.get_calc 1;
3.607 - val p = States.get_pos 1 1;
3.608 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
3.609 - if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
3.610 - error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
3.611 - DEconstrCalcTree 1;
3.612 -
3.613 -"--------- setContext..Thy ------------------------------";
3.614 -"--------- setContext..Thy ------------------------------";
3.615 -"--------- setContext..Thy ------------------------------";
3.616 -States.reset ();
3.617 - CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
3.618 - ("Test", ["sqroot-test", "univariate", "equation", "test"],
3.619 - ["Test", "squ-equ-test-subpbl1"]))];
3.620 - Iterator 1; moveActiveRoot 1;
3.621 - autoCalculate 1 CompleteCalcHead;
3.622 - autoCalculate 1 (Steps 1);
3.623 - val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt; (*2 lines, OK*)
3.624 - (*
3.625 - setNextTactic 1 (Rewrite_Set "Test_simplify"); (*--> "thy_isac_Test-rls-Test_simplify"*)
3.626 - autoCalculate 1 (Steps 1);
3.627 - val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
3.628 - *)
3.629 -"----- \<up> ^^ and vvvvv do the same -----";
3.630 -(*setContext 1 p "thy_isac_Test-rls-Test_simplify";*)
3.631 - val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt; (*2 lines, OK*)
3.632 -
3.633 - autoCalculate 1 (Steps 1);
3.634 -(*setContext 1 p "thy_isac_Test-rls-Test_simplify";*)
3.635 - val (((pt,_),_), p) = (States.get_calc 1, States.get_pos 1 1);
3.636 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
3.637 - if p = ([1], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "x + 1 + - 1 * 2 = 0"
3.638 - then () else error "--- setContext..Thy --- autoCalculate 1 (Steps 1) #1";
3.639 -
3.640 - autoCalculate 1 CompleteCalc;
3.641 - val (((pt,_),_), p) = (States.get_calc 1, States.get_pos 1 1);
3.642 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
3.643 -
3.644 - if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then ()
3.645 - else error "--- setContext..Thy --- autoCalculate CompleteCalc";
3.646 - DEconstrCalcTree 1;
3.647 -
3.648 -"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
3.649 -"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
3.650 -"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
3.651 -States.reset ();
3.652 - CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
3.653 - ("Test", ["sqroot-test", "univariate", "equation", "test"],
3.654 - ["Test", "squ-equ-test-subpbl1"]))];
3.655 - Iterator 1; moveActiveRoot 1;
3.656 - autoCalculate 1 CompleteToSubpbl;
3.657 - refFormula 1 (States.get_pos 1 1); (*<ISA> - 1 + x = 0 </ISA>*);
3.658 - val ((pt,_),_) = States.get_calc 1;
3.659 - val str = pr_ctree pr_short pt;
3.660 - writeln str;
3.661 - if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + - 1 * 2 = 0\n"
3.662 - then () else
3.663 - error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl- 1";
3.664 -
3.665 - autoCalculate 1 (Steps 1); (*proceeds only, if NOT 1 step before subplb*)
3.666 - autoCalculate 1 CompleteToSubpbl;
3.667 - val ((pt,_),_) = States.get_calc 1;
3.668 - val str = pr_ctree pr_short pt;
3.669 - writeln str;
3.670 - autoCalculate 1 CompleteCalc; (*das geht ohnehin !*);
3.671 - val ((pt,_),_) = States.get_calc 1;
3.672 - val p = States.get_pos 1 1;
3.673 -
3.674 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
3.675 - if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
3.676 - error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl 1";
3.677 - DEconstrCalcTree 1;
3.678 -
3.679 -"--------- rat-eq + subpbl: no_met, NO solution dropped -";
3.680 -"--------- rat-eq + subpbl: no_met, NO solution dropped -";
3.681 -"--------- rat-eq + subpbl: no_met, NO solution dropped -";
3.682 -"--------- rat-eq + subpbl: no_met, NO solution dropped - see LI: '--- simpl.rat.term, '..";
3.683 -(*--- THIS IS RE-USED WITH fun me IN test/../MathEngine/solve.sml -------------------
3.684 - ---- rat-eq + subpbl: set_found in check_tac1 ----*)
3.685 - CalcTree @{context}
3.686 - [(["equality ((5*x)/(x - 2) - x/(x+2)=(4::real))", "solveFor x", "solutions L"],
3.687 - ((** )"RatEq"( **)"PolyEq"(*required for "make_ratpoly_in"*),
3.688 - ["univariate", "equation"], ["no_met"]))];
3.689 - Iterator 1;
3.690 - moveActiveRoot 1;
3.691 - fetchProposedTactic 1;
3.692 -
3.693 - setNextTactic 1 (Model_Problem);
3.694 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
3.695 -
3.696 - setNextTactic 1 (Specify_Theory "RatEq");
3.697 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
3.698 - setNextTactic 1 (Specify_Problem ["rational", "univariate", "equation"]);
3.699 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
3.700 - setNextTactic 1 (Specify_Method ["RatEq", "solve_rat_equation"]);
3.701 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
3.702 - setNextTactic 1 (Apply_Method ["RatEq", "solve_rat_equation"]);
3.703 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
3.704 - setNextTactic 1 (Rewrite_Set "RatEq_simplify");
3.705 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
3.706 - setNextTactic 1 (Rewrite_Set "norm_Rational");
3.707 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
3.708 - setNextTactic 1 (Rewrite_Set "RatEq_eliminate");
3.709 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
3.710 - (* __________ for "12 * x + 4 * x \<up> 2 = 4 * (-4 + x \<up> 2)"*)
3.711 - setNextTactic 1 (Subproblem ("PolyEq", ["normalise", "polynomial",
3.712 - "univariate", "equation"]));
3.713 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
3.714 - setNextTactic 1 (Model_Problem );
3.715 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
3.716 - setNextTactic 1 (Specify_Theory "PolyEq");
3.717 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
3.718 - setNextTactic 1 (Specify_Problem ["normalise", "polynomial",
3.719 - "univariate", "equation"]);
3.720 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
3.721 - setNextTactic 1 (Specify_Method ["PolyEq", "normalise_poly"]);
3.722 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
3.723 - setNextTactic 1 (Apply_Method ["PolyEq", "normalise_poly"]);
3.724 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
3.725 - setNextTactic 1 (Rewrite ("all_left", @{thm all_left}));
3.726 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
3.727 - setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "make_ratpoly_in"));
3.728 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
3.729 - (* __________ for "16 + 12 * x = 0"*)
3.730 - setNextTactic 1 (Subproblem ("PolyEq",
3.731 - ["degree_1", "polynomial", "univariate", "equation"]));
3.732 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
3.733 - setNextTactic 1 (Model_Problem );
3.734 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
3.735 - setNextTactic 1 (Specify_Theory "PolyEq");
3.736 - (*------------- some trials in the problem-hierarchy ---------------*)
3.737 - setNextTactic 1 (Specify_Problem ["LINEAR", "univariate", "equation"]);
3.738 - autoCalculate 1 (Steps 1); fetchProposedTactic 1; (*<ERROR> helpless </ERROR> !!!*)
3.739 - setNextTactic 1 (Refine_Problem ["univariate", "equation"]);
3.740 - (*------------------------------------------------------------------*)
3.741 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
3.742 - setNextTactic 1 (Specify_Method ["PolyEq", "solve_d1_polyeq_equation"]);
3.743 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
3.744 - setNextTactic 1 (Apply_Method ["PolyEq", "solve_d1_polyeq_equation"]);
3.745 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
3.746 - setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "d1_polyeq_simplify"));
3.747 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
3.748 - setNextTactic 1 (Rewrite_Set "polyeq_simplify");
3.749 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
3.750 - setNextTactic 1 Or_to_List;
3.751 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
3.752 - setNextTactic 1 (Check_elementwise "Assumptions");
3.753 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
3.754 - setNextTactic 1 (Check_Postcond ["degree_1", "polynomial",
3.755 - "univariate", "equation"]);
3.756 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
3.757 - setNextTactic 1 (Check_Postcond ["normalise", "polynomial",
3.758 - "univariate", "equation"]);
3.759 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
3.760 - setNextTactic 1 (Check_Postcond ["rational", "univariate", "equation"]);
3.761 - val (ptp,_) = States.get_calc 1;
3.762 - val (Form t,_,_) = ME_Misc.pt_extract ptp;
3.763 - if States.get_pos 1 1 = ([], Res) andalso UnparseC.term t = "[x = -4 / 3]" then ()
3.764 - else writeln "FE-inteface.sml: diff.behav. in rat-eq + subpbl: no_met, NO ..";
3.765 - DEconstrCalcTree 1;
3.766 -
3.767 -
3.768 -\<close> ML \<open>
3.769 -"--------- tryMatchProblem, tryRefineProblem ------------";
3.770 -"--------- tryMatchProblem, tryRefineProblem ------------";
3.771 -"--------- tryMatchProblem, tryRefineProblem ------------";
3.772 -(*{\bf\UC{Having \isac{} Refine the Problem
3.773 - * Automatically}\label{SPECIFY:refine-auto}\\} test match and refine with
3.774 - * x \<up>2 + 4*x + 5 = 2
3.775 -see isac.bridge.TestSpecify#testMatchRefine*)
3.776 -States.reset ();
3.777 - CalcTree @{context}
3.778 - [(["equality (x \<up> 2 + 4*x + 5 = (2::real))", "solveFor x", "solutions L"],
3.779 - ("Isac_Knowledge",
3.780 - ["univariate", "equation"],
3.781 - ["no_met"]))];
3.782 - Iterator 1;
3.783 - moveActiveRoot 1;
3.784 -
3.785 - fetchProposedTactic 1;
3.786 - setNextTactic 1 (Model_Problem );
3.787 - (*..this tactic should be done 'tacitly', too !*)
3.788 -
3.789 -(*
3.790 -autoCalculate 1 CompleteCalcHead;
3.791 -checkContext 1 ([],Pbl) "pbl_equ_univ";
3.792 -checkContext 1 ([],Pbl) (Ptool.kestoreID2guh Ptool.Pbl_ ["univariate", "equation"]);
3.793 -*)
3.794 -
3.795 - autoCalculate 1 (Steps 1);
3.796 -
3.797 - fetchProposedTactic 1;
3.798 - setNextTactic 1 (Add_Given "equality (x \<up> 2 + 4 * x + 5 = (2::real))");
3.799 - autoCalculate 1 (Steps 1);
3.800 -
3.801 - "--------- we go into the ProblemBrowser (_NO_ pblID selected) -";
3.802 -(*initContext 1 Ptool.Pbl_ ([],Pbl);*)
3.803 -(* this would break if a calculation would be inserted before: CALCID...
3.804 - and pattern matching is not available in *.java.
3.805 -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"
3.806 -then () else error "--- tryMatchProblem, tryRefineProblem: initContext 1 Ptool.Pbl_ ([],Pbl); CHANGED";
3.807 -*)
3.808 -(*initContext 1 Ptool.Met_ ([],Pbl);*)
3.809 -(*<SYSERROR><CALCID>1</CALCID><ERROR>error in kernel 33</ERROR></SYSERROR>*)
3.810 -
3.811 - "--------- this match will show some incomplete items: ---------";
3.812 -
3.813 -(*checkContext 1 ([],Pbl) (Ptool.kestoreID2guh Ptool.Pbl_ ["univariate", "equation"]);
3.814 -checkContext 1 ([],Pbl) (Ptool.kestoreID2guh Ptool.Met_ ["LinEq", "solve_lineq_equation"]);*)
3.815 -
3.816 -
3.817 - fetchProposedTactic 1;
3.818 - setNextTactic 1 (Add_Given "solveFor x"); autoCalculate 1 (Steps 1);
3.819 -
3.820 - fetchProposedTactic 1;
3.821 - setNextTactic 1 (Add_Find "solutions L"); autoCalculate 1 (Steps 1);
3.822 -
3.823 - "--------- this is a matching model (all items correct): -------";
3.824 -(*checkContext 1 ([],Pbl) (Ptool.kestoreID2guh Ptool.Pbl_ ["univariate", "equation"]);*)
3.825 - "--------- this is a NOT matching model (some 'false': ---------";
3.826 -(*checkContext 1 ([],Pbl)(Ptool.kestoreID2guh Ptool.Pbl_ ["LINEAR", "univariate", "equation"]);*)
3.827 -
3.828 - "--------- find out a matching problem: ------------------------";
3.829 - "--------- find out a matching problem (FAILING: no new pbl) ---";
3.830 - refineProblem 1 ([],Pbl)(Ptool.pblID2guh @{context} ["LINEAR", "univariate", "equation"]);
3.831 -
3.832 - "--------- find out a matching problem (SUCCESSFUL) ------------";
3.833 - refineProblem 1 ([],Pbl) (Ptool.pblID2guh @{context} ["univariate", "equation"]);
3.834 -
3.835 - "--------- tryMatch, tryRefine did not change the calculation -";
3.836 - "--------- this is done by <TRANSFER> on the pbl-browser: ------";
3.837 - setNextTactic 1 (Specify_Problem ["normalise", "polynomial",
3.838 - "univariate", "equation"]);
3.839 - autoCalculate 1 (Steps 1);
3.840 -(*WN050904 fetchProposedTactic again --> Specify_Problem ["normalise",...
3.841 - and Specify_Theory skipped in comparison to below --- \<up> -inserted *)
3.842 -(*------------vvv-inserted-----------------------------------------------*)
3.843 - fetchProposedTactic 1;
3.844 -(*/-----ERROR INTRODUCED BY CHILD OF 33913fe24685 --------------------------------------------\* )
3.845 - setNextTactic 1 (Specify_Problem ["normalise", "polynomial",
3.846 - "univariate", "equation"]);
3.847 - autoCalculate 1 (Steps 1);
3.848 -
3.849 -(*and Specify_Theory skipped by fetchProposedTactic ?!?*)
3.850 -
3.851 - fetchProposedTactic 1;
3.852 - setNextTactic 1 (Specify_Method ["PolyEq", "normalise_poly"]);
3.853 - autoCalculate 1 (Steps 1);
3.854 -
3.855 - fetchProposedTactic 1;
3.856 - setNextTactic 1 (Apply_Method ["PolyEq", "normalise_poly"]);
3.857 -
3.858 - autoCalculate 1 CompleteCalc;
3.859 -
3.860 - val ((pt,_),_) = States.get_calc 1;
3.861 - Test_Tool.show_pt pt;
3.862 - val p = States.get_pos 1 1;
3.863 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
3.864 - if UnparseC.term f = "[x = - 1, x = -3]" andalso p = ([], Res) then () else
3.865 - error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
3.866 -
3.867 -(*------------ \<up> -inserted-----------------------------------------------*)
3.868 -(*WN050904 the fetchProposedTactic's below may not have worked like that
3.869 - before, too, because there was no check*)
3.870 - fetchProposedTactic 1;
3.871 - setNextTactic 1 (Specify_Theory "PolyEq");
3.872 - autoCalculate 1 (Steps 1);
3.873 -
3.874 - fetchProposedTactic 1;
3.875 - setNextTactic 1 (Specify_Method ["PolyEq", "normalise_poly"]);
3.876 - autoCalculate 1 (Steps 1);
3.877 -
3.878 - fetchProposedTactic 1;
3.879 - "--------- now the calc-header is ready for enter 'solving' ----";
3.880 - autoCalculate 1 CompleteCalc;
3.881 -
3.882 - val ((pt,_),_) = States.get_calc 1;
3.883 - rootthy pt;
3.884 - Test_Tool.show_pt pt;
3.885 - val p = States.get_pos 1 1;
3.886 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
3.887 - if UnparseC.term f = "[x = - 1, x = -3]" andalso p = ([], Res) then () else
3.888 - error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
3.889 - DEconstrCalcTree 1;
3.890 -( *\-----ERROR INTRODUCED BY CHILD OF 33913fe24685 --------------------------------------------/*)
3.891 -
3.892 -"--------- modifyCalcHead, resetCalcHead, modelProblem --";
3.893 -"--------- modifyCalcHead, resetCalcHead, modelProblem --";
3.894 -"--------- modifyCalcHead, resetCalcHead, modelProblem --";
3.895 -States.reset ();
3.896 - CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
3.897 - ("Test", ["sqroot-test", "univariate", "equation", "test"],
3.898 - ["Test", "squ-equ-test-subpbl1"]))];
3.899 - Iterator 1;
3.900 - moveActiveRoot 1;
3.901 -
3.902 - modifyCalcHead 1 (([],Pbl),(*the position from refFormula*)
3.903 - "solve (x+1=2, x)",(*the headline*)
3.904 - [P_Spec.Given ["equality (x+1=(2::real))", "solveFor x"],
3.905 - P_Spec.Find ["solutions L"](*,P_Spec.Relate []*)],
3.906 - Pbl,
3.907 - ("Test",
3.908 - ["sqroot-test", "univariate", "equation", "test"],
3.909 - ["Test", "squ-equ-test-subpbl1"]));
3.910 -
3.911 -val ((Nd (PblObj {fmz = (fm, tpm),
3.912 - loc = (SOME scrst_ctxt, NONE),
3.913 - ctxt,
3.914 - meth,
3.915 - spec = (thy,
3.916 - ["sqroot-test", "univariate", "equation", "test"],
3.917 - ["Test", "squ-equ-test-subpbl1"]),
3.918 - probl,
3.919 - branch = TransitiveB,
3.920 - origin,
3.921 - ostate = Incomplete,
3.922 - result},
3.923 - []),
3.924 - ([], Pbl)),
3.925 - []) = States.get_calc 1;
3.926 -(*WN110622: is the same as in 2002, but shouldn't be probl = [3 items?]*)
3.927 -if length meth = 0 andalso length probl = 0 (*just some items tested*) then ()
3.928 -else error "--- modifyCalcHead, resetCalcHead, modelProblem 1 --";
3.929 -
3.930 -resetCalcHead 1;
3.931 -modelProblem 1;
3.932 -
3.933 -States.get_calc 1;
3.934 -val ((Nd (PblObj {fmz = (fm, tpm),
3.935 - loc = (SOME scrst_ctxt, NONE),
3.936 - ctxt,
3.937 - meth,
3.938 - spec = ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]),
3.939 - probl,
3.940 - branch = TransitiveB,
3.941 - origin,
3.942 - ostate = Incomplete,
3.943 - result},
3.944 - []),
3.945 - ([], Pbl)),
3.946 - []) = States.get_calc 1;
3.947 -if length meth = 3 andalso length probl = 3 (*just some items tested*) then ()
3.948 -else error "--- modifyCalcHead, resetCalcHead, modelProblem 2 --";
3.949 -
3.950 -"--------- maximum-example, UC: Modeling an example -----";
3.951 -"--------- maximum-example, UC: Modeling an example -----";
3.952 -"--------- maximum-example, UC: Modeling an example -----";
3.953 -(* {\bf\UC{Editing the Model}\label{SPECIFY:enter}\label{SPECIFY:check}\\}
3.954 -see isac.bridge.TestModel#testEditItems
3.955 -*)
3.956 - val elems = ["fixedValues [r=Arbfix]", "maximum A", "valuesFor [a,b]",
3.957 - "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
3.958 - "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
3.959 - "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]",
3.960 - (* \<up> these are the elements for the root-problem (in variants)*)
3.961 - (*vvv these are elements required for subproblems*)
3.962 - "boundVariable a", "boundVariable b", "boundVariable alpha",
3.963 - "interval {x::real. 0 <= x & x <= 2*r}",
3.964 - "interval {x::real. 0 <= x & x <= 2*r}",
3.965 - "interval {x::real. 0 <= x & x <= pi}",
3.966 - "errorBound (eps=(0::real))"]
3.967 - (*specifying is not interesting for this example*)
3.968 - val spec = ("Diff_App", ["maximum_of", "function"],
3.969 - ["Diff_App", "max_by_calculus"]);
3.970 - (*the empty model with descriptions for user-guidance by Model_Problem*)
3.971 - val empty_model = [P_Spec.Given ["fixedValues []"],
3.972 - P_Spec.Find ["maximum", "valuesFor"],
3.973 - P_Spec.Relate ["relations []"]];
3.974 - DEconstrCalcTree 1;
3.975 -
3.976 -"#################################################################";
3.977 -States.reset ();
3.978 - CalcTree @{context} [(elems, spec)];
3.979 - Iterator 1;
3.980 - moveActiveRoot 1;
3.981 - refFormula 1 (States.get_pos 1 1);
3.982 - (*this gives a completely empty model*)
3.983 -
3.984 - fetchProposedTactic 1;
3.985 -(*fill the CalcHead with Descriptions...*)
3.986 - setNextTactic 1 (Model_Problem );
3.987 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.988 -
3.989 - (*user input is !!!!!EITHER!!!!! _some_ (at least one) items of the model
3.990 - !!!!!OR!!!!! _one_ part of the specification !!!!!!!!!!!!!*)
3.991 - (*input of two items, 'fixedValues [r=Arbfix]' and 'maximum b'...*)
3.992 - modifyCalcHead 1 (([],Pbl) (*position, from previous refFormula*),
3.993 - "Problem (Diff_App.thy, [maximum_of, function])",
3.994 - (*the head-form \<up> is not used for input here*)
3.995 - [P_Spec.Given ["fixedValues [r=Arbfix]"(*new input*)],
3.996 - P_Spec.Find ["maximum b"(*new input*), "valuesFor"],
3.997 - P_Spec.Relate ["relations"]],
3.998 - (*input (Arbfix will dissappear soon)*)
3.999 - Pbl (*belongsto*),
3.1000 - References.empty (*no input to the specification*));
3.1001 -
3.1002 - (*the user does not know, what 'superfluous' for 'maximum b' may mean
3.1003 - and asks what to do next*)
3.1004 - fetchProposedTactic 1;
3.1005 - (*the student follows the advice*)
3.1006 - setNextTactic 1 (Add_Find "maximum A"); (*FIXME.17.11.03: does not yet work*)
3.1007 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
3.1008 -
3.1009 - (*this input completes the model*)
3.1010 - modifyCalcHead 1 (([],Pbl), "not used here",
3.1011 - [P_Spec.Given ["fixedValues [r=Arbfix]"],
3.1012 - P_Spec.Find ["maximum A", "valuesFor [a,b]"(*new input*)],
3.1013 - P_Spec.Relate ["relations [A=a*b, \
3.1014 - \(a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]"]], Pbl, References.empty);
3.1015 -
3.1016 - (*specification is not interesting and should be skipped by the dialogguide;
3.1017 - !!!!!!!!!!!!!!!!!!!! input of ONE part at a time !!!!!!!!!!!!!!!!!!!!!!*)
3.1018 - modifyCalcHead 1 (([],Pbl), "not used here",
3.1019 - [P_Spec.Given ["fixedValues [r=Arbfix]"],
3.1020 - P_Spec.Find ["maximum A", "valuesFor [a,b]"(*new input*)],
3.1021 - P_Spec.Relate ["relations [A=a*b, \
3.1022 - \(a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]"]], Pbl,
3.1023 - ("Diff_App", Problem.id_empty, MethodC.id_empty));
3.1024 - modifyCalcHead 1 (([],Pbl), "not used here",
3.1025 - [P_Spec.Given ["fixedValues [r=Arbfix]"],
3.1026 - P_Spec.Find ["maximum A", "valuesFor [a,b]"(*new input*)],
3.1027 - P_Spec.Relate ["relations [A=a*b, \
3.1028 - \(a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]"]], Pbl,
3.1029 - ("Diff_App", ["maximum_of", "function"],
3.1030 - MethodC.id_empty));
3.1031 - modifyCalcHead 1 (([],Pbl), "not used here",
3.1032 - [P_Spec.Given ["fixedValues [r=Arbfix]"],
3.1033 - P_Spec.Find ["maximum A", "valuesFor [a,b]"(*new input*)],
3.1034 - P_Spec.Relate ["relations [A=a*b, \
3.1035 - \(a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]"]], Pbl,
3.1036 - ("Diff_App", ["maximum_of", "function"],
3.1037 - ["Diff_App", "max_by_calculus"]));
3.1038 - (*this final calcHead now has STATUS 'complete' !*)
3.1039 - DEconstrCalcTree 1;
3.1040 -
3.1041 -(*POSTPONE CORRECTION AT END OF TRANSITION TO Isabelle/PIDE/Isac (~ Cas_Cmd)
3.1042 -"--------- solve_linear from pbl-hierarchy --------------";
3.1043 -"--------- solve_linear from pbl-hierarchy --------------";
3.1044 -"--------- solve_linear from pbl-hierarchy --------------";
3.1045 -States.reset ();
3.1046 - val (fmz, sp) = ([], ("", ["LINEAR", "univariate", "equation", "test"], []));
3.1047 - CalcTree @{context} [(fmz, sp)];
3.1048 - Iterator 1; moveActiveRoot 1;
3.1049 - refFormula 1 (States.get_pos 1 1);
3.1050 - modifyCalcHead 1 (([],Pbl),"solve (1+- 1*2+x=(0::real))",
3.1051 - [P_Spec.Given ["equality (1+- 1*2+x=(0::real))", "solveFor x"],
3.1052 - P_Spec.Find ["solutions L"]],
3.1053 - Pbl,
3.1054 - ("Test", ["LINEAR", "univariate", "equation", "test"],
3.1055 - ["Test", "solve_linear"]));
3.1056 - autoCalculate 1 CompleteCalc;
3.1057 - refFormula 1 (States.get_pos 1 1);
3.1058 - val ((pt,_),_) = States.get_calc 1;
3.1059 - val p = States.get_pos 1 1;
3.1060 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
3.1061 - if UnparseC.term f = "[x = 1]" andalso p = ([], Res) andalso map UnparseC.term asms = [] then ()
3.1062 - else error "FE-interface.sml: diff.behav. in from pbl -hierarchy 1";
3.1063 - DEconstrCalcTree 1;
3.1064 -
3.1065 -"--------- solve_linear as in an algebra system (CAS)----";
3.1066 -"--------- solve_linear as in an algebra system (CAS)----";
3.1067 -"--------- solve_linear as in an algebra system (CAS)----";
3.1068 -(*WN120210?not ME:\label{UC:cas-input} UC 30.1.2.5 p.168*)
3.1069 -States.reset ();
3.1070 - val (fmz, sp) = ([], ("", [], []));
3.1071 - CalcTree @{context} [(fmz, sp)];
3.1072 - Iterator 1; moveActiveRoot 1;
3.1073 - modifyCalcHead 1 (([],Pbl),"solveTest (1+- 1*2+x=0,x)", [], Pbl, ("", [], []));
3.1074 - autoCalculate 1 CompleteCalc;
3.1075 - refFormula 1 (States.get_pos 1 1);
3.1076 - val ((pt,_),_) = States.get_calc 1;
3.1077 - val p = States.get_pos 1 1;
3.1078 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
3.1079 - if UnparseC.term f = "[x = 1]" andalso p = ([], Res) andalso map UnparseC.term asms = [] then ()
3.1080 - else error "FE-interface.sml: diff.behav. in from pbl -hierarchy 2";
3.1081 -DEconstrCalcTree 1;
3.1082 -*)
3.1083 -
3.1084 -"--------- interSteps: on 'miniscript with mini-subpbl' -";
3.1085 -"--------- interSteps: on 'miniscript with mini-subpbl' -";
3.1086 -"--------- interSteps: on 'miniscript with mini-subpbl' -";
3.1087 - CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
3.1088 - ("Test", ["sqroot-test", "univariate", "equation", "test"],
3.1089 - ["Test", "squ-equ-test-subpbl1"]))];
3.1090 - Iterator 1;
3.1091 - moveActiveRoot 1;
3.1092 - autoCalculate 1 CompleteCalc;
3.1093 - val ((pt,_),_) = States.get_calc 1;
3.1094 - Test_Tool.show_pt pt;
3.1095 -
3.1096 - (*UC\label{UC:inter-steps} UC 30.3.5.5 p.178*)
3.1097 - interSteps 1 ([2],Res);
3.1098 - val ((pt,_),_) = States.get_calc 1; Test_Tool.show_pt pt (*new ([2,1],Frm)..([2,6],Res)*);
3.1099 - val (unc, del, gen) = (([1],Res),([1],Res),([2,6],Res));
3.1100 - getFormulaeFromTo 1 unc gen 1 false;
3.1101 -
3.1102 - (*UC\label{UC:inter-steps} UC 30.3.5.5 p.178*)
3.1103 - interSteps 1 ([3,2],Res);
3.1104 - val ((pt,_),_) = States.get_calc 1; Test_Tool.show_pt pt (*new ([3,2,1],Frm)..([3,2,2],Res)*);
3.1105 - val (unc, del, gen) = (([3,1],Res),([3,1],Res),([3,2,2],Res));
3.1106 - getFormulaeFromTo 1 unc gen 1 false;
3.1107 -
3.1108 - (*UC\label{UC:inter-steps} UC 30.3.5.5 p.178*)
3.1109 - interSteps 1 ([3],Res) (*no new steps in subproblems*);
3.1110 - val (unc, del, gen) = (([3],Pbl),([3],Pbl),([3,2],Res));
3.1111 - getFormulaeFromTo 1 unc gen 1 false;
3.1112 -
3.1113 - (*UC\label{UC:inter-steps} UC 30.3.5.5 p.178*)
3.1114 - interSteps 1 ([],Res) (*no new steps in subproblems*);
3.1115 - val (unc, del, gen) = (([],Pbl),([],Pbl),([4],Res));
3.1116 - getFormulaeFromTo 1 unc gen 1 false;
3.1117 -DEconstrCalcTree 1;
3.1118 -
3.1119 -"--------- getTactic, fetchApplicableTactics ------------";
3.1120 -"--------- getTactic, fetchApplicableTactics ------------";
3.1121 -"--------- getTactic, fetchApplicableTactics ------------";
3.1122 -(* compare test/../script.sml
3.1123 -"----------- fun from_prog ---------------------------------------";
3.1124 -*)
3.1125 - CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
3.1126 - ("Test", ["sqroot-test", "univariate", "equation", "test"],
3.1127 - ["Test", "squ-equ-test-subpbl1"]))];
3.1128 - Iterator 1; moveActiveRoot 1;
3.1129 - autoCalculate 1 CompleteCalc;
3.1130 - val ((pt,_),_) = States.get_calc 1;
3.1131 - Test_Tool.show_pt pt;
3.1132 -
3.1133 - (*UC\label{SOLVE:HIDE:getTactic} \label{SOLVE:AUTO:tactic} UC 30.3.3.1 p.176
3.1134 -WN120210 not impl. in FE*)
3.1135 - getTactic 1 ([],Pbl);
3.1136 - getTactic 1 ([1],Res);
3.1137 - getTactic 1 ([3],Pbl);
3.1138 - getTactic 1 ([3,1],Frm);
3.1139 - getTactic 1 ([3],Res);
3.1140 - getTactic 1 ([],Res);
3.1141 -
3.1142 -(*UC\label{SOLVE:MANUAL:TACTIC:listall} UC 30.3.2.2 p.175*)
3.1143 - fetchApplicableTactics 1 99999 ([],Pbl);
3.1144 - fetchApplicableTactics 1 99999 ([1],Res);
3.1145 - fetchApplicableTactics 1 99999 ([3],Pbl);
3.1146 - fetchApplicableTactics 1 99999 ([3,1],Res);
3.1147 - fetchApplicableTactics 1 99999 ([3],Res);
3.1148 - fetchApplicableTactics 1 99999 ([],Res);
3.1149 -DEconstrCalcTree 1;
3.1150 -
3.1151 -(*SINCE eliminate ThmC.numerals_to_Free: loops ---------------------------------------------\\* )
3.1152 -"--------- getAssumptions, getAccumulatedAsms -----------";
3.1153 -"--------- getAssumptions, getAccumulatedAsms -----------";
3.1154 -"--------- getAssumptions, getAccumulatedAsms -----------";
3.1155 -States.reset ();
3.1156 -CalcTree @{context}
3.1157 -[(["equality (x/(x \<up> 2 - 6*x+9) - 1/(x \<up> 2 - 3*x) =1/x)",
3.1158 - "solveFor x", "solutions L"],
3.1159 - ("RatEq",["univariate", "equation"],["no_met"]))];
3.1160 -Iterator 1; moveActiveRoot 1;
3.1161 -autoCalculate 1 CompleteCalc;
3.1162 -val ((pt,_),_) = States.get_calc 1;
3.1163 -val p = States.get_pos 1 1;
3.1164 -val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
3.1165 -(*============ inhibit exn WN120316 compare 2002-- 2011 ===========================
3.1166 -if map UnparseC.term asms =
3.1167 - ["True |\n~ lhs ((3 + - 1 * x + x \<up> 2) * x =\n" ^
3.1168 - " 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3)) is_poly_in x", "-6 * x + 5 * x \<up>\<up> 2 = 0",
3.1169 - "lhs (-6 * x + 5 * x \<up> 2 = 0) is_poly_in x",
3.1170 - "lhs (-6 * x + 5 * x \<up>\<up> 2 = 0) has_degree_in x = 2",
3.1171 - "9 * x + -6 * x \<up> 2 + x \<up> 3 ~= 0"]
3.1172 -andalso UnparseC.term f = "[-6 * x + 5 * x \<up> 2 = 0]" andalso p = ([], Res) then ()
3.1173 -else error "TODO compare 2002-- 2011"; (*...data during test --- x / (x \<up> 2 - 6 * x + 9) - 1...*)
3.1174 -============ inhibit exn WN120316 compare 2002-- 2011 ===========================*)
3.1175 -
3.1176 -if p = ([], Res) andalso UnparseC.term f = "[x = 6 / 5]"
3.1177 -andalso map UnparseC.term asms = []
3.1178 -then () else error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b [x = 6 / 5]";
3.1179 -
3.1180 -(*UC\label{SOLVE:HELP:assumptions} UC 30.3.5.1 p.178*)
3.1181 -getAssumptions 1 ([3], Res);
3.1182 -getAssumptions 1 ([5], Res);
3.1183 -(*UC\label{SOLVE:HELP:assumptions-origin} UC 30.3.5.2 p.178
3.1184 - WN0502 still without positions*)
3.1185 -getAccumulatedAsms 1 ([3], Res);
3.1186 -getAccumulatedAsms 1 ([5], Res);
3.1187 -DEconstrCalcTree 1;
3.1188 -( *SINCE eliminate ThmC.numerals_to_Free: loops ---------------------------------------------//*)
3.1189 -
3.1190 -\<close> ML \<open>
3.1191 -"--------- arbitrary combinations of steps --------------";
3.1192 -"--------- arbitrary combinations of steps --------------";
3.1193 -"--------- arbitrary combinations of steps --------------";
3.1194 - CalcTree @{context} (*start of calculation, return No.1*)
3.1195 - [(["equality (1+- 1*2+x=(0::real))", "solveFor x", "solutions L"],
3.1196 - ("Test",
3.1197 - ["LINEAR", "univariate", "equation", "test"],
3.1198 - ["Test", "solve_linear"]))];
3.1199 - Iterator 1; moveActiveRoot 1;
3.1200 -
3.1201 - fetchProposedTactic 1;
3.1202 - (*ERROR States.get_calc 1 not existent*)
3.1203 - setNextTactic 1 (Model_Problem );
3.1204 - autoCalculate 1 (Steps 1);
3.1205 - fetchProposedTactic 1;
3.1206 - fetchProposedTactic 1;
3.1207 -
3.1208 - setNextTactic 1 (Add_Find "solutions L");
3.1209 - setNextTactic 1 (Add_Find "solutions L");
3.1210 -
3.1211 - autoCalculate 1 (Steps 1);
3.1212 - autoCalculate 1 (Steps 1);
3.1213 -
3.1214 - setNextTactic 1 (Specify_Theory "Test");
3.1215 - fetchProposedTactic 1;
3.1216 - autoCalculate 1 (Steps 1);
3.1217 -
3.1218 - autoCalculate 1 (Steps 1);
3.1219 - autoCalculate 1 (Steps 1);
3.1220 - autoCalculate 1 (Steps 1);
3.1221 - autoCalculate 1 (Steps 1);
3.1222 -(*------------------------- end calc-head*)
3.1223 -
3.1224 - fetchProposedTactic 1;
3.1225 - setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "isolate_bdv"));
3.1226 - autoCalculate 1 (Steps 1);
3.1227 -
3.1228 - setNextTactic 1 (Rewrite_Set "Test_simplify");
3.1229 - fetchProposedTactic 1;
3.1230 - autoCalculate 1 (Steps 1);
3.1231 -
3.1232 - autoCalculate 1 CompleteCalc;
3.1233 - val ((pt,_),_) = States.get_calc 1;
3.1234 - val p = States.get_pos 1 1;
3.1235 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
3.1236 - if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
3.1237 - error "FE-interface.sml: diff.behav. in combinations of steps";
3.1238 -DEconstrCalcTree 1;
3.1239 -
3.1240 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right"; (*UC 30.3.2.4 p.175*)
3.1241 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
3.1242 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
3.1243 -States.reset ();
3.1244 - CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
3.1245 - ("Test", ["sqroot-test", "univariate", "equation", "test"],
3.1246 - ["Test", "squ-equ-test-subpbl1"]))];
3.1247 - Iterator 1;
3.1248 - moveActiveRoot 1;
3.1249 - autoCalculate 1 CompleteCalcHead;
3.1250 - autoCalculate 1 (Steps 1);
3.1251 - autoCalculate 1 (Steps 1);
3.1252 - appendFormula 1 "- 1 + x = 0" (*|> Future.join*);
3.1253 - (*... returns calcChangedEvent with*)
3.1254 - val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res));
3.1255 - getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
3.1256 -
3.1257 - val ((pt,_),_) = States.get_calc 1;
3.1258 - val p = States.get_pos 1 1;
3.1259 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
3.1260 - if UnparseC.term f = "- 1 + x = 0" andalso p = ([2], Res) then () else
3.1261 - error "FE-interface.sml: diff.behav. in FORMULA:enter} right";
3.1262 -DEconstrCalcTree 1;
3.1263 -
3.1264 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other"; (*UC 30.3.2.4 p.175*)
3.1265 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
3.1266 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
3.1267 - CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
3.1268 - ("Test", ["sqroot-test", "univariate", "equation", "test"],
3.1269 - ["Test", "squ-equ-test-subpbl1"]))];
3.1270 - Iterator 1;
3.1271 - moveActiveRoot 1;
3.1272 - autoCalculate 1 CompleteCalcHead;
3.1273 - autoCalculate 1 (Steps 1);
3.1274 - autoCalculate 1 (Steps 1);
3.1275 - appendFormula 1 "x - 1 = 0" (*|> Future.join*);
3.1276 - val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res));
3.1277 - getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
3.1278 - (*11 elements !!!*)
3.1279 -
3.1280 - val ((pt,_),_) = States.get_calc 1;
3.1281 - val p = States.get_pos 1 1;
3.1282 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
3.1283 - if UnparseC.term f = "x - 1 = 0" andalso p = ([2], Res) then () else
3.1284 - error "FE-interface.sml: diff.behav. in FORMULA:enter} other";
3.1285 -DEconstrCalcTree 1;
3.1286 -
3.1287 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2"; (*UC 30.3.2.4 p.175*)
3.1288 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
3.1289 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
3.1290 - CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
3.1291 - ("Test", ["sqroot-test", "univariate", "equation", "test"],
3.1292 - ["Test", "squ-equ-test-subpbl1"]))];
3.1293 - Iterator 1;
3.1294 - moveActiveRoot 1;
3.1295 - autoCalculate 1 CompleteCalcHead;
3.1296 - autoCalculate 1 (Steps 1);
3.1297 - autoCalculate 1 (Steps 1);
3.1298 - appendFormula 1 "x = 1" (*|> Future.join*);
3.1299 - (*... returns calcChangedEvent with*)
3.1300 - val (unc, del, gen) = (([1],Res), ([1],Res), ([3,2],Res));
3.1301 - getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
3.1302 - (*6 elements !!!*)
3.1303 -
3.1304 - val ((pt,_),_) = States.get_calc 1;
3.1305 - val p = States.get_pos 1 1;
3.1306 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
3.1307 - if UnparseC.term f = "x = 1" andalso p = ([3,2], Res) then () else
3.1308 - error "FE-interface.sml: diff.behav. in FORMULA:enter} oth 2";
3.1309 -DEconstrCalcTree 1;
3.1310 -
3.1311 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok"; (*UC 30.3.2.4 p.175*)
3.1312 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
3.1313 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
3.1314 - CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
3.1315 - ("Test", ["sqroot-test", "univariate", "equation", "test"],
3.1316 - ["Test", "squ-equ-test-subpbl1"]))];
3.1317 - Iterator 1;
3.1318 - moveActiveRoot 1;
3.1319 - autoCalculate 1 CompleteCalcHead;
3.1320 - autoCalculate 1 (Steps 1);
3.1321 - autoCalculate 1 (Steps 1);
3.1322 - appendFormula 1 "x - 4711 = 0" (*|> Future.join*);
3.1323 - (*... returns <ERROR> no derivation found </ERROR>*)
3.1324 -
3.1325 - val ((pt,_),_) = States.get_calc 1;
3.1326 - val p = States.get_pos 1 1;
3.1327 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
3.1328 - if UnparseC.term f = "x + 1 + - 1 * 2 = 0" andalso p = ([1], Res) then () else
3.1329 - error "FE-interface.sml: diff.behav. in FORMULA:enter} NOTok";
3.1330 -DEconstrCalcTree 1;
3.1331 -
3.1332 -"--------- replaceFormula {SOL:MAN:FOR:replace} right----"; (*UC 30.3.2.5 p.176*)
3.1333 -"--------- replaceFormula {SOL:MAN:FOR:replace} right----";
3.1334 -"--------- replaceFormula {SOL:MAN:FOR:replace} right----";
3.1335 -(*\label{SOLVE:MANUAL:FORMULA:replace}*)
3.1336 - CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
3.1337 - ("Test", ["sqroot-test", "univariate", "equation", "test"],
3.1338 - ["Test", "squ-equ-test-subpbl1"]))];
3.1339 - Iterator 1;
3.1340 - moveActiveRoot 1;
3.1341 - autoCalculate 1 CompleteCalc;
3.1342 - moveActiveFormula 1 ([2],Res);
3.1343 - replaceFormula 1 "- 1 + x = 0" (*i.e. repeats input*);
3.1344 - (*... returns <ERROR> formula not changed </ERROR>*)
3.1345 -
3.1346 - val ((pt,_),_) = States.get_calc 1;
3.1347 - val p = States.get_pos 1 1;
3.1348 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
3.1349 - if UnparseC.term f = "- 1 + x = 0" andalso p = ([2], Res) then () else
3.1350 - error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
3.1351 - if map fst3 (ME_Misc.get_interval ([2],Res) ([],Res) 9999 pt) =
3.1352 - [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
3.1353 - ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else
3.1354 - error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2";
3.1355 -
3.1356 -(*WN050211 replaceFormula didn't work on second ctree: thus now tested...*)
3.1357 - CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
3.1358 - ("Test", ["sqroot-test", "univariate", "equation", "test"],
3.1359 - ["Test", "squ-equ-test-subpbl1"]))];
3.1360 - Iterator 2; (*! ! ! 1 CalcTree @{context} inbetween States.reset (); *)
3.1361 - moveActiveRoot 2;
3.1362 - autoCalculate 2 CompleteCalc;
3.1363 - moveActiveFormula 2 ([2],Res);
3.1364 - replaceFormula 2 "- 1 + x = 0" (*i.e. repeats input*);
3.1365 - (*... returns <ERROR> formula not changed </ERROR>*)
3.1366 -
3.1367 - val ((pt,_),_) = States.get_calc 2;
3.1368 - val p = States.get_pos 2 1;
3.1369 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
3.1370 - if UnparseC.term f = "- 1 + x = 0" andalso p = ([2], Res) then () else
3.1371 - error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
3.1372 - if map fst3 (ME_Misc.get_interval ([2],Res) ([],Res) 9999 pt) =
3.1373 - [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
3.1374 - ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else
3.1375 - error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2b";
3.1376 -DEconstrCalcTree 1;
3.1377 -
3.1378 -"--------- replaceFormula {SOL:MAN:FOR:replace} other----"; (*UC 30.3.2.5 p.176*)
3.1379 -"--------- replaceFormula {SOL:MAN:FOR:replace} other----";
3.1380 -"--------- replaceFormula {SOL:MAN:FOR:replace} other----";
3.1381 -(*\label{SOLVE:MANUAL:FORMULA:replace}*)
3.1382 - CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
3.1383 - ("Test", ["sqroot-test", "univariate", "equation", "test"],
3.1384 - ["Test", "squ-equ-test-subpbl1"]))];
3.1385 - Iterator 1;
3.1386 - moveActiveRoot 1;
3.1387 - autoCalculate 1 CompleteCalc;
3.1388 - moveActiveFormula 1 ([2],Res); (*there is "- 1 + x = 0"*)
3.1389 - replaceFormula 1 "x - 1 = 0"; (*<-------------------------------------*)
3.1390 - (*... returns calcChangedEvent with*)
3.1391 - val (unc, del, gen) = (([1],Res), ([4],Res), ([2],Res));
3.1392 - getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
3.1393 -
3.1394 - val ((pt,_),_) = States.get_calc 1;
3.1395 - Test_Tool.show_pt pt;
3.1396 - val p = States.get_pos 1 1;
3.1397 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
3.1398 - if UnparseC.term f = "x - 1 = 0" andalso p = ([2], Res) then () else
3.1399 - error "FE-interface.sml: diff.behav. in FORMULA:replace} other 1";
3.1400 -(* for getting the list in whole length ...
3.1401 -(*default_print_depth 99*) map fst3 (ME_Misc.get_interval ([1],Res) ([],Res) 9999 pt); (*default_print_depth 3*)
3.1402 - *)
3.1403 - if map fst3 (ME_Misc.get_interval ([1],Res) ([],Res) 9999 pt) =
3.1404 - [([1], Res), ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
3.1405 - ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2, 7], Res),
3.1406 - ([2, 8], Res), ([2, 9], Res), ([2], Res)] then () else
3.1407 - error "FE-interface.sml: diff.behav. in FORMULA:replace} other 2";
3.1408 -DEconstrCalcTree 1;
3.1409 -
3.1410 -"--------- replaceFormula {SOL:MAN:FOR:replace} other 2--"; (*UC 30.3.2.5 p.176*)
3.1411 -"--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
3.1412 -"--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
3.1413 -(*\label{SOLVE:MANUAL:FORMULA:replace}*)
3.1414 - CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
3.1415 - ("Test", ["sqroot-test", "univariate", "equation", "test"],
3.1416 - ["Test", "squ-equ-test-subpbl1"]))];
3.1417 - Iterator 1;
3.1418 - moveActiveRoot 1;
3.1419 - autoCalculate 1 CompleteCalc;
3.1420 - moveActiveFormula 1 ([2],Res); (*there is "- 1 + x = 0"*)
3.1421 - replaceFormula 1 "x = 1"; (*<-------------------------------------*)
3.1422 - (*... returns calcChangedEvent with ...*)
3.1423 - val (unc, del, gen) = (([1],Res), ([4],Res), ([3,2],Res));
3.1424 - getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
3.1425 - (*9 elements !!!*)
3.1426 -
3.1427 - val ((pt,_),_) = States.get_calc 1;
3.1428 - Test_Tool.show_pt pt; (*error: ...ME_Misc.get_interval drops ([3,2],Res) ...*)
3.1429 - val (t,_) = get_obj g_result pt [3,2]; UnparseC.term t;
3.1430 - if map fst3 (ME_Misc.get_interval ([1],Res) ([],Res) 9999 pt) =
3.1431 - [([1], Res), ([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res),
3.1432 - ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
3.1433 - ([3,2],Res)] then () else
3.1434 - error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 1";
3.1435 -
3.1436 - val p = States.get_pos 1 1;
3.1437 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
3.1438 - if UnparseC.term f = "x = 1" andalso p = ([3,2], Res) then () else
3.1439 - error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 2";
3.1440 -DEconstrCalcTree 1;
3.1441 -
3.1442 -\<close> ML \<open>
3.1443 -"--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----"; (*UC 30.3.2.5 p.176*)
3.1444 -"--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
3.1445 -"--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
3.1446 -(*\label{SOLVE:MANUAL:FORMULA:replace}*)
3.1447 - CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
3.1448 - ("Test", ["sqroot-test", "univariate", "equation", "test"],
3.1449 - ["Test", "squ-equ-test-subpbl1"]))];
3.1450 - Iterator 1;
3.1451 - moveActiveRoot 1;
3.1452 - autoCalculate 1 CompleteCalc;
3.1453 - moveActiveFormula 1 ([2],Res); (*there is "- 1 + x = 0"*)
3.1454 - replaceFormula 1 "x - 4711 = 0";
3.1455 - (*... returns <ERROR> no derivation found </ERROR>*)
3.1456 -
3.1457 - val ((pt,_),_) = States.get_calc 1;
3.1458 - Test_Tool.show_pt pt;
3.1459 - val p = States.get_pos 1 1;
3.1460 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
3.1461 - if UnparseC.term f = "- 1 + x = 0" andalso p = ([2], Res) then () else
3.1462 - error "FE-interface.sml: diff.behav. in FORMULA:replace} NOTok";
3.1463 - DEconstrCalcTree 1;
3.1464 -
3.1465 -"--------- UC errpat chain-rule-diff-both, fillpat by input ------";
3.1466 -"--------- UC errpat chain-rule-diff-both, fillpat by input ------";
3.1467 -"--------- UC errpat chain-rule-diff-both, fillpat by input ------";
3.1468 -CalcTree @{context}
3.1469 -[(["functionTerm (x \<up> 2 + sin (x \<up> 4))", "differentiateFor x", "derivative f_f'"],
3.1470 - ("Isac_Knowledge", ["derivative_of", "function"], ["diff", "differentiate_on_R"]))];
3.1471 -Iterator 1;
3.1472 -moveActiveRoot 1;
3.1473 -autoCalculate 1 CompleteCalcHead;
3.1474 -autoCalculate 1 (Steps 1);
3.1475 -autoCalculate 1 (Steps 1);(*([1], Res), d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))*)
3.1476 -appendFormula 1 "d_d x (x \<up> 2) + cos (4 * x \<up> 3)" (*|> Future.join*); (*<<<<<<<=========================*)
3.1477 -(* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),
3.1478 - would recognize "cos (4 * x \<up> (4 - 1)) + 2 * x" as well.
3.1479 - results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>
3.1480 - instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)
3.1481 - val ((pt,pos), _) = States.get_calc 1;
3.1482 - val p = States.get_pos 1 1;
3.1483 - val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
3.1484 -
3.1485 - if p = ([1], Res) andalso UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))"
3.1486 - then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"],
3.1487 - ("diff_sum", thm)) => () | _ => error "embed fun fill_form changed 0"
3.1488 - | _ => error "embed fun fill_form changed 1"
3.1489 -else error "embed fun fill_form changed 2";
3.1490 -
3.1491 -(*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ====================
3.1492 -findFillpatterns 1 "chain-rule-diff-both"; (*<<<<<<<=================================*)
3.1493 -(*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x \<up> 2) + d_d x (sin (x \<up> 4)) =
3.1494 - d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *)
3.1495 - val ((pt,pos),_) = States.get_calc 1;
3.1496 - val p = States.get_pos 1 1;
3.1497 -
3.1498 - val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
3.1499 - if p = ([1], Res) andalso UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" andalso
3.1500 - get_obj g_tac pt (fst p) = Rewrite_Inst (["(''bdv'', x)"], ("diff_sum", "Diff.diff_sum"(*?!?*)))
3.1501 - then ()
3.1502 - else error "embed fun fill_form changed 2";
3.1503 -
3.1504 -(* if we assume, that the fill-patterns are ordered such that the 1st has large gaps
3.1505 - and the last has no gaps, then the number of fill-patterns would suffice
3.1506 - for the DialogGuide to select appropriately. *)
3.1507 -requestFillformula 1 ("chain-rule-diff-both", "fill-both-args");(*<<<<<<<============*)
3.1508 - (*<AUTOCALC> ([1], Res) ([2], Res) ([2], Res) </AUTOCALC>*)
3.1509 - val ((pt,pos),_) = States.get_calc 1;
3.1510 - val p = States.get_pos 1 1;
3.1511 - val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
3.1512 - if p = ([1], Res) andalso existpt [2] pt andalso
3.1513 - UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up>\<up> 4))" andalso
3.1514 - get_obj g_tac pt (fst p) = Rewrite_Inst (["(''bdv'', x)"], ("diff_sum", "Diff.diff_sum"))
3.1515 - then () else error "embed fun fill_form changed 3";
3.1516 -
3.1517 -inputFillFormula 1 "d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x (x \<up> 4)";(*<<<<<<<=====*)
3.1518 - val ((pt, _),_) = States.get_calc 1;
3.1519 - val p = States.get_pos 1 1;
3.1520 - val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
3.1521 - if p = ([2], Res) andalso
3.1522 - UnparseC.term f = "d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x (x \<up> 4)" andalso
3.1523 - get_obj g_tac pt (fst p) = Rewrite_Inst (["(''bdv'', x)"], ("diff_sin_chain", ""))
3.1524 - then () else error "inputFillFormula changed 11";
3.1525 -
3.1526 -autoCalculate 1 CompleteCalc;
3.1527 -
3.1528 -"~~~~~ final check: the input formula is inserted as it would have been correct from beginning";
3.1529 -val ((pt, _),_) = States.get_calc 1;
3.1530 -val p = States.get_pos 1 1;
3.1531 -val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
3.1532 -if p = ([], Res) andalso UnparseC.term f = "2 * x + cos (x \<up> 4) * 4 * x \<up> 3"
3.1533 -then () else error "inputFillFormula changed 12";
3.1534 -Test_Tool.show_pt pt;
3.1535 -(*[
3.1536 -(([], Frm), Diff (x \<up> 2 + sin (x \<up> 4), x)),
3.1537 -(([1], Frm), d_d x (x \<up> 2 + sin (x \<up> 4))),
3.1538 -(([1], Res), d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))),
3.1539 -(([2], Res), d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x (x \<up> 4)), (*<<<<<<<=====*)
3.1540 -(([3], Res), d_d x (x \<up> 2) + cos (x \<up> 4) * (4 * x \<up> (4 - 1))),
3.1541 -(([4], Res), 2 * x \<up> (2 - 1) + cos (x \<up> 4) * (4 * x \<up> (4 - 1))),
3.1542 -(([5], Res), 2 * x + cos (x \<up> 4) * 4 * x \<up> 3),
3.1543 -(([], Res), 2 * x + cos (x \<up> 4) * 4 * x \<up> 3)] *)
3.1544 -============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*)
3.1545 -DEconstrCalcTree 1;
3.1546 -
3.1547 -\<close> ML \<open>
3.1548 -(*POSTPONE CORRECTION AT END OF TRANSITION TO Isabelle/PIDE/Isac (~ Cas_Cmd ?)
3.1549 -"--------- UC errpat add-fraction, fillpat by input --------------";
3.1550 -"--------- UC errpat add-fraction, fillpat by input --------------";
3.1551 -"--------- UC errpat add-fraction, fillpat by input --------------";
3.1552 -(*cp from BridgeLog Java <=> SML*)
3.1553 -CalcTree @{context} [([], References.empty)];
3.1554 -Iterator 1;
3.1555 -moveActiveRoot 1;
3.1556 -moveActiveFormula 1 ([],Pbl);
3.1557 -replaceFormula 1 "Simplify (5 * x / (4 * y) + 3 * x / (4 * y))";
3.1558 -autoCalculate 1 CompleteCalcHead;
3.1559 -autoCalculate 1 (Steps 1);
3.1560 -appendFormula 1 "8 * x / (8 * y)" (*|> Future.join*);
3.1561 -(*<CALCMESSAGE> no derivation found </CALCMESSAGE>
3.1562 ---- but in BridgeLog Java <=> SML:
3.1563 -<CALCMESSAGE> error pattern #addition-of-fractions# </CALCMESSAGE>*)
3.1564 -DEconstrCalcTree 1;
3.1565 ------------------------------------------------------------------------------------------------*)
3.1566 -
3.1567 -\<close> ML \<open>
3.1568 -"--------- UC errpat, fillpat step to Rewrite --------------------";
3.1569 -"--------- UC errpat, fillpat step to Rewrite --------------------";
3.1570 -"--------- UC errpat, fillpat step to Rewrite --------------------";
3.1571 -(*TODO*)
3.1572 -CalcTree @{context}
3.1573 -[(["functionTerm ((x \<up> 2) \<up> 3 + sin (x \<up> 4))",
3.1574 - "differentiateFor x", "derivative f_f'"],
3.1575 - ("Isac_Knowledge", ["derivative_of", "function"],
3.1576 - ["diff", "differentiate_on_R"]))]; (*<<<======= EP is directly in script*)
3.1577 -Iterator 1;
3.1578 -moveActiveRoot 1;
3.1579 -autoCalculate 1 CompleteCalc;
3.1580 -val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
3.1581 -DEconstrCalcTree 1;
3.1582 -
3.1583 -\<close> ML \<open>
3.1584 -"--------- UC errpat, fillpat step to Rewrite_Set ----------------";
3.1585 -"--------- UC errpat, fillpat step to Rewrite_Set ----------------";
3.1586 -"--------- UC errpat, fillpat step to Rewrite_Set ----------------";
3.1587 -CalcTree @{context}
3.1588 -[(["functionTerm ((x \<up> 2) \<up> 3 + sin (x \<up> 4))",
3.1589 - "differentiateFor x", "derivative f_f'"],
3.1590 - ("Isac_Knowledge", ["derivative_of", "function"],
3.1591 - ["diff", "after_simplification"]))]; (*<<<======= EP is in a ruleset*)
3.1592 -Iterator 1;
3.1593 -moveActiveRoot 1;
3.1594 -autoCalculate 1 CompleteCalcHead;
3.1595 -autoCalculate 1 (Steps 1); fetchProposedTactic 1;
3.1596 -autoCalculate 1 (Steps 1); fetchProposedTactic 1;
3.1597 -(*
3.1598 -<NEXTTAC>
3.1599 - <CALCID> 1 </CALCID>
3.1600 - <TACTICERRORPATTERNS>
3.1601 - <STRINGLIST>
3.1602 - <STRING> chain-rule-diff-both </STRING>
3.1603 - <STRING> cancel </STRING>
3.1604 - </STRINGLIST>
3.1605 - <REWRITESETINSTTACTIC name="Rewrite_Set_Inst">
3.1606 - <RULESET> norm_diff </RULESET>
3.1607 - <SUBSTITUTION>
3.1608 - <PAIR>
3.1609 - <VARIABLE>
3.1610 - <MATHML>
3.1611 - <ISA> bdv </ISA>
3.1612 - </MATHML>
3.1613 - </VARIABLE>
3.1614 - <VALUE>
3.1615 - <MATHML>
3.1616 - <ISA> x </ISA>
3.1617 - </MATHML>
3.1618 - </VALUE>
3.1619 - </PAIR>
3.1620 - </SUBSTITUTION>
3.1621 - </REWRITESETINSTTACTIC>
3.1622 - </TACTICERRORPATTERNS>
3.1623 -</NEXTTAC>
3.1624 -
3.1625 -
3.1626 -(*WN1208 postponed due to efforts required for stepToErrorPatterns (NEW rewrite_set_)*)
3.1627 -stepToErrorPatterns 1; (*--> calcChanged, rule immediately calls... *)
3.1628 -stepOnErrorPatterns 1; (*--> calcChanged, rule calls getTactic and displays it *)
3.1629 -(* then --- UC errpat, fillpat by input ---*)
3.1630 -*)
3.1631 -autoCalculate 1 CompleteCalc;
3.1632 -val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
3.1633 -(*WN1208 postponed due to efforts required for stepToErrorPatterns (NEW rewrite_set_)*)
3.1634 -DEconstrCalcTree 1;
3.1635 -
3.1636 -\<close> ML \<open>
3.1637 -\<close> ML \<open>
3.1638 -\<close>
3.1639
3.1640 ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
3.1641 ML \<open>"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";\<close>