wneuper/isa: test/Tools/isac/Frontend/use-cases.sml@7d3dbc1171ff (annotated)

neuper@52113	1	(* Title: tests the interface of isac's SML-kernel in accordance to
neuper@52113	2	java-tests/isac.bridge.
neuper@52113	3	Author: Walther Neuper
neuper@52113	4	(c) copyright due to lincense terms.
neuper@52113	5
neuper@52113	6	WN050707 ... if true, the test ist marked with a \label referring
neuper@52113	7	to the same UC in isac-docu.tex as the JUnit testcase.
neuper@52113	8	WN120210?not ME: added some labels, which are not among the above,
neuper@52113	9	repaired lost \label (s).
wneuper@59127	10
wneuper@59127	11	theory Test_Some imports Build_Thydata begin
wneuper@59127	12	ML {* KEStore_Elems.set_ref_thy @{theory};
wneuper@59127	13	fun autoCalculate' cI auto = autoCalculate cI auto (\|> Future.join) *}
wneuper@59127	14	ML_file "Frontend/use-cases.sml"
neuper@52113	15	*)
neuper@52113	16
neuper@52113	17	"--------------------------------------------------------";
neuper@52113	18	"table of contents --------------------------------------";
neuper@52113	19	"--------------------------------------------------------";
neuper@52113	20	"within struct ------------------------------------------";
neuper@52113	21	"--------------------------------------------------------";
neuper@52113	22	"--------- encode ^ -> ^^^ ------------------------------";
neuper@52113	23	"--------------------------------------------------------";
neuper@52113	24	"exported from struct -----------------------------------";
neuper@52113	25	"--------------------------------------------------------";
neuper@52113	26	"--------- empty rootpbl --------------------------------";
neuper@52113	27	"--------- solve_linear as rootpbl FE -------------------";
neuper@52113	28	"--------- inspect the CalcTree No.1 with Iterator No.2 -";
neuper@52113	29	"--------- miniscript with mini-subpbl ------------------";
neuper@52113	30	"--------- mini-subpbl AUTOCALCULATE Step 1 -------------";
neuper@52113	31	"--------- solve_linear as rootpbl AUTO CompleteCalc ----";
neuper@52113	32	"--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
neuper@52113	33	"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
neuper@52113	34	"--------- mini-subpbl AUTO CompleteCalcHead ------------";
neuper@52113	35	"--------- solve_linear as rootpbl AUTO CompleteModel ---";
neuper@52113	36	"--------- setContext..Thy ------------------------------";
neuper@52113	37	"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
neuper@52113	38	"--------- rat-eq + subpbl: no_met, NO solution dropped -";
neuper@52113	39	"--------- tryMatchProblem, tryRefineProblem ------------";
neuper@52113	40	"--------- modifyCalcHead, resetCalcHead, modelProblem --";
neuper@52113	41	"--------- maximum-example, UC: Modeling an example -----";
neuper@52113	42	"--------- solve_linear from pbl-hierarchy --------------";
neuper@52113	43	"--------- solve_linear as in an algebra system (CAS)----";
neuper@52113	44	"--------- interSteps: on 'miniscript with mini-subpbl' -";
neuper@52113	45	"--------- getTactic, fetchApplicableTactics ------------";
neuper@52113	46	"--------- getAssumptions, getAccumulatedAsms -----------";
neuper@52113	47	"--------- arbitrary combinations of steps --------------";
neuper@52113	48	"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
neuper@52113	49	"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
neuper@52113	50	"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
neuper@52113	51	"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
neuper@52113	52	"--------- replaceFormula {SOL:MAN:FOR:replace} right----";
neuper@52113	53	"--------- replaceFormula {SOL:MAN:FOR:replace} other----";
neuper@52113	54	"--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
neuper@52113	55	"--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
neuper@52113	56	"--------- UC errpat chain-rule-diff-both, fillpat by input ------";
neuper@52113	57	"--------- UC errpat add-fraction, fillpat by input --------------";
neuper@52113	58	"--------- UC errpat, fillpat step to Rewrite --------------------";
neuper@52113	59	"--------- UC errpat, fillpat step to Rewrite_Set ----------------";
neuper@52113	60	"--------------------------------------------------------";
neuper@52113	61
neuper@52113	62	"within struct ---------------------------------------------------";
neuper@52113	63	"within struct ---------------------------------------------------";
neuper@52113	64	"within struct ---------------------------------------------------";
neuper@52113	65	(*==================================================================
neuper@52113	66
neuper@52113	67
neuper@52113	68	"--------- encode ^ -> ^^^ ------------------------------";
neuper@52113	69	"--------- encode ^ -> ^^^ ------------------------------";
neuper@52113	70	"--------- encode ^ -> ^^^ ------------------------------";
neuper@52113	71	if encode "a^2+b^2=c^2" = "a^^^2+b^^^2=c^^^2" then ()
neuper@52113	72	else error "interface.sml: diff.behav. in encode ^ -> ^^^ ";
neuper@52113	73
neuper@52113	74	if (decode o encode) "a^2+b^2=c^2" = "a^2+b^2=c^2" then ()
neuper@52113	75	else error "interface.sml: diff.behav. in de/encode ^ <-> ^^^ ";
neuper@52113	76
neuper@52113	77	==================================================================*)
neuper@52113	78	"exported from struct --------------------------------------------";
neuper@52113	79	"exported from struct --------------------------------------------";
neuper@52113	80	"exported from struct --------------------------------------------";
neuper@52113	81
neuper@52113	82
neuper@52113	83	(------------ set at startup of the Kernel ----------------------)
s1210629013@55445	84	reset_states (); (resets all state information in Kernel )
neuper@52113	85	(----------------------------------------------------------------)
neuper@52113	86
neuper@52113	87	"--------- empty rootpbl --------------------------------";
neuper@52113	88	"--------- empty rootpbl --------------------------------";
neuper@52113	89	"--------- empty rootpbl --------------------------------";
neuper@52113	90	CalcTree [([], ("", [], []))];
neuper@52113	91	Iterator 1;
neuper@52113	92	moveActiveRoot 1;
neuper@52113	93	refFormula 1 (get_pos 1 1);
neuper@52113	94	(WN.040222: stoert das sehr, dass e_domID etc. statt leer kommt ???)
neuper@52113	95	DEconstrCalcTree 1;
neuper@52113	96
neuper@52113	97	"--------- solve_linear as rootpbl FE -------------------";
neuper@52113	98	"--------- solve_linear as rootpbl FE -------------------";
neuper@52113	99	"--------- solve_linear as rootpbl FE -------------------";
neuper@52113	100	CalcTree (start of calculation, return No.1)
neuper@52113	101	[(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
neuper@52113	102	("Test",
neuper@55279	103	["LINEAR","univariate","equation","test"],
neuper@52113	104	["Test","solve_linear"]))];
neuper@52113	105	Iterator 1; (create an active Iterator on CalcTree No.1)
neuper@52113	106
neuper@52113	107	moveActiveRoot 1;(sets the CalcIterator No.1 at the root of CalcTree No.1);
neuper@52113	108	refFormula 1 (get_pos 1 1) (gets CalcHead; model is still empty);
neuper@52113	109
neuper@52113	110
neuper@52113	111	fetchProposedTactic 1 (by using Iterator No.1);
neuper@52113	112	setNextTactic 1 (Model_Problem); (by using Iterator No.1)
wneuper@59248	113	autoCalculate 1 (Step 1);
neuper@52113	114	refFormula 1 (get_pos 1 1) (model contains descriptions for all items);
wneuper@59248	115	autoCalculate 1 (Step 1);
neuper@52113	116	(-----since Model_Problem + complete_mod_ in case cas of SOME-----
neuper@52113	117	fetchProposedTactic 1;
neuper@52113	118	setNextTactic 1 (Add_Given "equality (1 + -1 * 2 + x = 0)");
wneuper@59248	119	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); (equality added);
neuper@52113	120
neuper@52113	121	fetchProposedTactic 1;
neuper@52113	122	setNextTactic 1 (Add_Given "solveFor x");
wneuper@59248	123	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@52113	124
neuper@52113	125	fetchProposedTactic 1;
neuper@52113	126	setNextTactic 1 (Add_Find "solutions L");
wneuper@59248	127	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@52113	128
neuper@52113	129	fetchProposedTactic 1;
neuper@52113	130	setNextTactic 1 (Specify_Theory "Test");
wneuper@59248	131	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@52113	132	-----since Model_Problem + complete_mod_ in case cas of SOME-----)
neuper@52113	133
neuper@52113	134	fetchProposedTactic 1;
neuper@55279	135	setNextTactic 1 (Specify_Problem ["LINEAR","univariate","equation","test"]);
wneuper@59248	136	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@52113	137	(-------------------------------------------------------------------------)
neuper@52113	138	fetchProposedTactic 1;
neuper@52113	139	val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
neuper@52113	140
neuper@52113	141	setNextTactic 1 (Specify_Method ["Test","solve_linear"]);
neuper@52113	142	val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
neuper@52113	143
wneuper@59248	144	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@52113	145	val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
neuper@52113	146
neuper@52113	147	(-------------------------------------------------------------------------)
neuper@52113	148	fetchProposedTactic 1;
neuper@52113	149	val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
neuper@52113	150
neuper@52113	151	setNextTactic 1 (Apply_Method ["Test","solve_linear"]);
neuper@52113	152	(ERROR.110620 <SETNEXTTACTIC>..<MESSAGE> end-of-calculation)
neuper@52113	153	val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
neuper@52113	154	is_complete_mod ptp;
neuper@52113	155	is_complete_spec ptp;
neuper@52113	156
wneuper@59248	157	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@52113	158	val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
neuper@52113	159	(term2str (get_obj g_form pt [1]);)
neuper@52113	160	(-------------------------------------------------------------------------)
neuper@52113	161
neuper@52113	162	fetchProposedTactic 1;
neuper@52113	163	setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
wneuper@59248	164	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@52113	165
neuper@52113	166	fetchProposedTactic 1;
neuper@52113	167	setNextTactic 1 (Rewrite_Set "Test_simplify");
wneuper@59248	168	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@52113	169
neuper@52113	170	fetchProposedTactic 1;
neuper@55279	171	setNextTactic 1 (Check_Postcond ["LINEAR","univariate","equation","test"]);
wneuper@59248	172	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@52113	173
neuper@52113	174	val ((pt,_),_) = get_calc 1;
neuper@52113	175	val ip = get_pos 1 1;
neuper@52113	176	val (Form f, tac, asms) = pt_extract (pt, ip);
neuper@52113	177	(exception just above means: 'ModSpec' has been returned: error anyway)
neuper@52113	178	if term2str f = "[x = 1]" then () else
neuper@52113	179	error "FE-Kernel-interface.sml: diff.behav. in solve_linear as rootpbl";
neuper@52113	180
neuper@52113	181	"--------- inspect the CalcTree No.1 with Iterator No.2 -";
neuper@52113	182	"--------- inspect the CalcTree No.1 with Iterator No.2 -";
neuper@52113	183	"--------- inspect the CalcTree No.1 with Iterator No.2 -";
neuper@52113	184	(WN041118: inspection shifted to Iterator No.1, because others need pos')
neuper@52113	185	moveActiveRoot 1;
neuper@52113	186	refFormula 1 ([],Pbl); getTactic 1 ([],Pbl);(Error)
neuper@52113	187	moveActiveDown 1;
neuper@52113	188	refFormula 1 ([1],Frm); getTactic 1 ([1],Frm);(Error)
neuper@52113	189	moveActiveDown 1 ;
neuper@52113	190	refFormula 1 ([1],Res); getTactic 1 ([1],Res);(OK)
neuper@52113	191	(getAssumption 1 ([1],Res); TODO.WN041217)
neuper@52113	192	moveActiveDown 1 ; refFormula 1 ([2],Res);
neuper@52113	193	moveActiveCalcHead 1; refFormula 1 ([],Pbl);
neuper@52113	194	moveActiveDown 1;
neuper@52113	195	moveActiveDown 1;
neuper@52113	196	moveActiveDown 1;
neuper@52113	197	if get_pos 1 1 = ([2], Res) then () else
neuper@52113	198	error "FE-interface.sml: diff.behav. in a inspect 1 with Iterator 2";
neuper@52113	199	moveActiveDown 1; refFormula 1 ([], Res);
neuper@52113	200	if get_pos 1 1 = ([], Res) then () else
neuper@52113	201	error "FE-interface.sml: diff.behav. in b inspect 1 with Iterator 2";
neuper@52113	202	moveActiveCalcHead 1; refFormula 1 ([],Pbl);
neuper@52113	203	DEconstrCalcTree 1;
neuper@52113	204
neuper@52113	205	"--------- miniscript with mini-subpbl ------------------";
neuper@52113	206	"--------- miniscript with mini-subpbl ------------------";
neuper@52113	207	"--------- miniscript with mini-subpbl ------------------";
neuper@52113	208	(WN120210?not ME:\label{SOLVE:MANUAL:TACTIC:enter} UC 30.3.2.1 p.175 !!!!!NOT IMPL IN FE)
neuper@52113	209	"=== this sequence of fun-calls resembles fun me ===";
s1210629013@55445	210	reset_states (); (start of calculation, return No.1)
neuper@52113	211	CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
neuper@52113	212	("Test", ["sqroot-test","univariate","equation","test"],
neuper@52113	213	["Test","squ-equ-test-subpbl1"]))];
neuper@52113	214	Iterator 1;
neuper@52113	215
neuper@52113	216	moveActiveRoot 1;
neuper@52113	217	refFormula 1 (get_pos 1 1);
neuper@52113	218	fetchProposedTactic 1;
neuper@52113	219	setNextTactic 1 (Model_Problem);
wneuper@59248	220	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(gets ModSpec;model is still empty)
neuper@52113	221
neuper@52113	222	fetchProposedTactic 1;
neuper@52113	223	setNextTactic 1 (Add_Given "equality (x + 1 = 2)");
wneuper@59248	224	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@52113	225
neuper@52113	226	fetchProposedTactic 1;
neuper@52113	227	setNextTactic 1 (Add_Given "solveFor x");
wneuper@59248	228	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@52113	229
neuper@52113	230	fetchProposedTactic 1;
neuper@52113	231	setNextTactic 1 (Add_Find "solutions L");
wneuper@59248	232	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@52113	233
neuper@52113	234	fetchProposedTactic 1;
neuper@52113	235	setNextTactic 1 (Specify_Theory "Test");
wneuper@59248	236	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@52113	237
neuper@52113	238	fetchProposedTactic 1;
neuper@52113	239	setNextTactic 1 (Specify_Problem
neuper@52113	240	["sqroot-test","univariate","equation","test"]);
wneuper@59248	241	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@52113	242	"1-----------------------------------------------------------------";
neuper@52113	243
neuper@52113	244	fetchProposedTactic 1;
neuper@52113	245	setNextTactic 1 (Specify_Method ["Test","squ-equ-test-subpbl1"]);
wneuper@59248	246	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@52113	247
neuper@52113	248	fetchProposedTactic 1;
neuper@52113	249	setNextTactic 1 (Apply_Method ["Test","squ-equ-test-subpbl1"]);
wneuper@59248	250	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@52113	251
neuper@52113	252	fetchProposedTactic 1;
neuper@52113	253	setNextTactic 1 (Rewrite_Set "norm_equation");
wneuper@59248	254	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@52113	255
neuper@52113	256	fetchProposedTactic 1;
neuper@52113	257	setNextTactic 1 (Rewrite_Set "Test_simplify");
wneuper@59248	258	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@52113	259
neuper@52113	260	fetchProposedTactic 1;(----------------Subproblem--------------------);
neuper@52113	261	setNextTactic 1 (Subproblem ("Test",
neuper@55279	262	["LINEAR","univariate","equation","test"]));
wneuper@59248	263	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@52113	264
neuper@52113	265	fetchProposedTactic 1;
neuper@52113	266	setNextTactic 1 (Model_Problem );
wneuper@59248	267	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@52113	268
neuper@52113	269	fetchProposedTactic 1;
neuper@52113	270	setNextTactic 1 (Add_Given "equality (-1 + x = 0)");
wneuper@59248	271	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@52113	272
neuper@52113	273	fetchProposedTactic 1;
neuper@52113	274	setNextTactic 1 (Add_Given "solveFor x");
wneuper@59248	275	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@52113	276
neuper@52113	277	fetchProposedTactic 1;
neuper@52113	278	setNextTactic 1 (Add_Find "solutions x_i");
wneuper@59248	279	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@52113	280
neuper@52113	281	fetchProposedTactic 1;
neuper@52113	282	setNextTactic 1 (Specify_Theory "Test");
wneuper@59248	283	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@52113	284
neuper@52113	285	fetchProposedTactic 1;
neuper@55279	286	setNextTactic 1 (Specify_Problem ["LINEAR","univariate","equation","test"]);
wneuper@59248	287	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@52113	288	"2-----------------------------------------------------------------";
neuper@52113	289
neuper@52113	290	fetchProposedTactic 1;
neuper@52113	291	setNextTactic 1 (Specify_Method ["Test","solve_linear"]);
wneuper@59248	292	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@52113	293
neuper@52113	294	fetchProposedTactic 1;
neuper@52113	295	setNextTactic 1 (Apply_Method ["Test","solve_linear"]);
wneuper@59248	296	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@52113	297
neuper@52113	298	fetchProposedTactic 1;
neuper@52113	299	setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
wneuper@59248	300	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@52113	301
neuper@52113	302	fetchProposedTactic 1;
neuper@52113	303	setNextTactic 1 (Rewrite_Set "Test_simplify");
wneuper@59248	304	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@52113	305
neuper@52113	306	fetchProposedTactic 1;
neuper@55279	307	setNextTactic 1 (Check_Postcond ["LINEAR","univariate","equation","test"]);
wneuper@59248	308	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@52113	309
neuper@52113	310	fetchProposedTactic 1;
neuper@52113	311	setNextTactic 1 (Check_elementwise "Assumptions");
wneuper@59248	312	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@52113	313
neuper@52113	314	val xml = fetchProposedTactic 1;
neuper@52113	315	setNextTactic 1 (Check_Postcond
neuper@52113	316	["sqroot-test","univariate","equation","test"]);
wneuper@59248	317	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@52113	318
neuper@52113	319	val ((pt,_),_) = get_calc 1;
neuper@52113	320	val str = pr_ptree pr_short pt;
neuper@52113	321	writeln str;
neuper@52113	322	val ip = get_pos 1 1;
neuper@52113	323	val (Form f, tac, asms) = pt_extract (pt, ip);
neuper@52113	324	(exception just above means: 'ModSpec' has been returned: error anyway)
neuper@52113	325	if term2str f = "[x = 1]" then () else
neuper@52113	326	error "FE-interface.sml: diff.behav. in miniscript with mini-subpb";
neuper@52113	327	DEconstrCalcTree 1;
neuper@52113	328
neuper@52113	329	"--------- mini-subpbl AUTOCALCULATE Step 1 -------------";
neuper@52113	330	"--------- mini-subpbl AUTOCALCULATE Step 1 -------------";
neuper@52113	331	"--------- mini-subpbl AUTOCALCULATE Step 1 -------------";
neuper@52113	332	(WN120210?not ME:\label{SOLVE:AUTO:one} UC 30.3.3.2 p.176)
neuper@52113	333	CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
neuper@52113	334	("Test", ["sqroot-test","univariate","equation","test"],
neuper@52113	335	["Test","squ-equ-test-subpbl1"]))];
neuper@52113	336	Iterator 1;
neuper@52113	337	moveActiveRoot 1;
wneuper@59248	338	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
wneuper@59248	339	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
wneuper@59248	340	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
wneuper@59248	341	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
wneuper@59248	342	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
wneuper@59248	343	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
wneuper@59248	344	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
wneuper@59248	345	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@52113	346	(here the solve-phase starts)
wneuper@59248	347	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
wneuper@59248	348	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
wneuper@59248	349	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@52113	350	(------------------------------------)
wneuper@59111	351	(* default_print_depth 13; get_calc 1;
neuper@52113	352	*)
wneuper@59248	353	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@52113	354	(calc-head of subproblem)
wneuper@59248	355	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
wneuper@59248	356	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
wneuper@59248	357	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
wneuper@59248	358	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
wneuper@59248	359	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
wneuper@59248	360	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
wneuper@59248	361	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@52113	362	(solve-phase of the subproblem)
wneuper@59248	363	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
wneuper@59248	364	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
wneuper@59248	365	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
wneuper@59248	366	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@52113	367	(finish subproblem)
wneuper@59248	368	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@52113	369	(finish problem)
wneuper@59248	370	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@52113	371
neuper@52113	372	(this checks the test for correctness..)
neuper@52113	373	val ((pt,_),_) = get_calc 1;
neuper@52113	374	val p = get_pos 1 1;
neuper@52113	375	val (Form f, tac, asms) = pt_extract (pt, p);
neuper@52113	376	if term2str f = "[x = 1]" andalso p = ([], Res) then () else
neuper@52113	377	error "FE-interface.sml: diff.behav. in miniscript with mini-subpb";
neuper@52113	378	DEconstrCalcTree 1;
neuper@52113	379
neuper@52113	380
neuper@52113	381	"--------- solve_linear as rootpbl AUTO CompleteCalc ----";
neuper@52113	382	"--------- solve_linear as rootpbl AUTO CompleteCalc ----";
neuper@52113	383	"--------- solve_linear as rootpbl AUTO CompleteCalc ----";
neuper@52113	384	(WN120210?not ME:\label{SPECIFY:START:auto} UC 30.2.4.2 p.174)
neuper@52113	385	CalcTree
neuper@52113	386	[(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
neuper@52113	387	("Test",
neuper@55279	388	["LINEAR","univariate","equation","test"],
neuper@52113	389	["Test","solve_linear"]))];
neuper@52113	390	Iterator 1;
neuper@52113	391	moveActiveRoot 1;
neuper@52113	392	getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 999 false;
neuper@52113	393
wneuper@59248	394	autoCalculate 1 CompleteCalc;
neuper@52113	395	val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
neuper@52113	396	getFormulaeFromTo 1 unc gen 1 (only level 1) false;
neuper@52113	397
neuper@52113	398	val ((pt,_),_) = get_calc 1;
neuper@52113	399	val p = get_pos 1 1;
neuper@52113	400	val (Form f, tac, asms) = pt_extract (pt, p);
neuper@52113	401	if term2str f = "[x = 1]" andalso p = ([], Res) then () else
neuper@52113	402	error "FE-interface.sml: diff.behav. in solve_linear/rt AUTOCALCULATE ";
neuper@52113	403	DEconstrCalcTree 1;
neuper@52113	404
neuper@52113	405	"--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
neuper@52113	406	"--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
neuper@52113	407	"--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
neuper@52113	408	(* ERROR: error in kernel ?? *)
neuper@52113	409	CalcTree
neuper@52113	410	[(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
neuper@52113	411	("Test",
neuper@55279	412	["LINEAR","univariate","equation","test"],
neuper@52113	413	["Test","solve_linear"]))];
neuper@52113	414	Iterator 1;
neuper@52113	415	moveActiveRoot 1;
neuper@52113	416
wneuper@59248	417	autoCalculate 1 CompleteCalcHead;
neuper@52113	418	refFormula 1 (get_pos 1 1);
neuper@52113	419	val ((pt,p),_) = get_calc 1;
neuper@52113	420
wneuper@59248	421	autoCalculate 1 CompleteCalc;
neuper@52113	422	val ((pt,p),_) = get_calc 1;
neuper@52113	423	if p=([], Res) then () else
neuper@52113	424	error "FE-interface.sml: diff.behav. in solve_linear AUTOC Head/Calc ";
neuper@52113	425	DEconstrCalcTree 1;
neuper@52113	426
neuper@52113	427	"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
neuper@52113	428	"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
neuper@52113	429	"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
neuper@52113	430	(WN120210?not ME:\label{SPECIFY:START:auto} UC 30.2.4.2 p.174)
neuper@52113	431	CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
neuper@52113	432	("Test", ["sqroot-test","univariate","equation","test"],
neuper@52113	433	["Test","squ-equ-test-subpbl1"]))];
neuper@52113	434	Iterator 1;
neuper@52113	435	moveActiveRoot 1;
wneuper@59248	436	autoCalculate 1 CompleteCalc;
neuper@52113	437	val ((pt,p),_) = get_calc 1; show_pt pt;
neuper@52113	438	(*
neuper@52113	439	getTactic 1 ([1],Frm);
neuper@52113	440	getTactic 1 ([1],Res);
neuper@52113	441	initContext 1 Thy_ ([1],Res);
neuper@52113	442	*)
neuper@52113	443	(... returns calcChangedEvent with)
neuper@52113	444	val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
neuper@52113	445	getFormulaeFromTo 1 unc gen 0 (only result) false;
neuper@52113	446	getFormulaeFromTo 1 unc gen 1 (only level 1) false;
neuper@52113	447	getFormulaeFromTo 1 unc gen 99999 (all levels) false;
neuper@52113	448
neuper@52113	449	val ((pt,_),_) = get_calc 1;
neuper@52113	450	val p = get_pos 1 1;
neuper@52113	451	val (Form f, tac, asms) = pt_extract (pt, p);
neuper@52113	452	if term2str f = "[x = 1]" andalso p = ([], Res) then () else
neuper@52113	453	error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
neuper@52113	454	DEconstrCalcTree 1;
neuper@52113	455
neuper@52113	456	"--------- mini-subpbl AUTO CompleteCalcHead ------------";
neuper@52113	457	"--------- mini-subpbl AUTO CompleteCalcHead ------------";
neuper@52113	458	"--------- mini-subpbl AUTO CompleteCalcHead ------------";
neuper@52113	459	CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
neuper@52113	460	("Test", ["sqroot-test","univariate","equation","test"],
neuper@52113	461	["Test","squ-equ-test-subpbl1"]))];
neuper@52113	462	Iterator 1;
neuper@52113	463	moveActiveRoot 1;
wneuper@59248	464	autoCalculate 1 CompleteCalcHead;
neuper@52113	465
neuper@52113	466	val ((Nd (PblObj {env = NONE, fmz = (fm, ("Test", pblID, metID)), loc = (SOME (env, ctxt1), NONE),
neuper@52113	467	cell = NONE, ctxt = ctxt2, meth,
neuper@52113	468	spec = ("Test", ["sqroot-test", "univariate", "equation", "test"],
neuper@52113	469	["Test", "squ-equ-test-subpbl1"]),
neuper@52113	470	probl, branch = TransitiveB, origin, ostate = Incomplete, result}, []),
neuper@52113	471	([], Met)), []) = get_calc 1;
neuper@52113	472	if length meth = 3 andalso length probl = 3 (just some items tested) then ()
neuper@52113	473	else error "--- mini-subpbl AUTO CompleteCalcHead ---";
neuper@52113	474	DEconstrCalcTree 1;
neuper@52113	475
neuper@52113	476	"--------- solve_linear as rootpbl AUTO CompleteModel ---";
neuper@52113	477	"--------- solve_linear as rootpbl AUTO CompleteModel ---";
neuper@52113	478	"--------- solve_linear as rootpbl AUTO CompleteModel ---";
neuper@52113	479	CalcTree
neuper@52113	480	[(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
neuper@52113	481	("Test",
neuper@55279	482	["LINEAR","univariate","equation","test"],
neuper@52113	483	["Test","solve_linear"]))];
neuper@52113	484	Iterator 1;
neuper@52113	485	moveActiveRoot 1;
wneuper@59248	486	autoCalculate 1 CompleteModel;
neuper@52113	487	refFormula 1 (get_pos 1 1);
neuper@52113	488
neuper@55279	489	setProblem 1 ["LINEAR","univariate","equation","test"];
neuper@52113	490	val pos = get_pos 1 1;
neuper@55279	491	setContext 1 pos (kestoreID2guh Pbl_["LINEAR","univariate","equation","test"]);
neuper@52113	492	refFormula 1 (get_pos 1 1);
neuper@52113	493
neuper@52113	494	setMethod 1 ["Test","solve_linear"];
neuper@52113	495	setContext 1 pos (kestoreID2guh Met_ ["Test","solve_linear"]);
neuper@52113	496	refFormula 1 (get_pos 1 1);
neuper@52113	497	val ((pt,_),_) = get_calc 1;
neuper@52113	498	if get_obj g_spec pt [] = ("e_domID",
neuper@55279	499	["LINEAR", "univariate","equation","test"],
neuper@52113	500	["Test","solve_linear"]) then ()
neuper@52113	501	else error "FE-interface.sml: diff.behav. in setProblem, setMethod";
neuper@52113	502
wneuper@59248	503	autoCalculate 1 CompleteCalcHead;
neuper@52113	504	refFormula 1 (get_pos 1 1);
wneuper@59248	505	autoCalculate 1 CompleteCalc;
neuper@52113	506	moveActiveDown 1;
neuper@52113	507	moveActiveDown 1;
neuper@52113	508	moveActiveDown 1;
neuper@52113	509	refFormula 1 (get_pos 1 1);
neuper@52113	510	val ((pt,_),_) = get_calc 1;
neuper@52113	511	val p = get_pos 1 1;
neuper@52113	512	val (Form f, tac, asms) = pt_extract (pt, p);
neuper@52113	513	if term2str f = "[x = 1]" andalso p = ([], Res) then () else
neuper@52113	514	error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
neuper@52113	515	DEconstrCalcTree 1;
neuper@52113	516
neuper@52113	517	"--------- setContext..Thy ------------------------------";
neuper@52113	518	"--------- setContext..Thy ------------------------------";
neuper@52113	519	"--------- setContext..Thy ------------------------------";
s1210629013@55445	520	reset_states ();
neuper@52113	521	CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
neuper@52113	522	("Test", ["sqroot-test","univariate","equation","test"],
neuper@52113	523	["Test","squ-equ-test-subpbl1"]))];
neuper@52113	524	Iterator 1; moveActiveRoot 1;
wneuper@59248	525	autoCalculate 1 CompleteCalcHead;
wneuper@59248	526	autoCalculate 1 (Step 1);
neuper@52113	527	val ((pt,p),_) = get_calc 1; show_pt pt; (2 lines, OK)
neuper@52113	528	(*
neuper@52113	529	setNextTactic 1 (Rewrite_Set "Test_simplify"); (--> "thy_isac_Test-rls-Test_simplify")
wneuper@59248	530	autoCalculate 1 (Step 1);
neuper@52113	531	val ((pt,p),_) = get_calc 1; show_pt pt;
neuper@52113	532	*)
neuper@52113	533	"-----^^^^^ and vvvvv do the same -----";
neuper@52113	534	setContext 1 p "thy_isac_Test-rls-Test_simplify";
neuper@52113	535	val ((pt,p),_) = get_calc 1; show_pt pt; (2 lines, OK)
neuper@52113	536
wneuper@59248	537	autoCalculate 1 (Step 1);
neuper@52113	538	setContext 1 p "thy_isac_Test-rls-Test_simplify";
neuper@52113	539	val (((pt,_),_), p) = (get_calc 1, get_pos 1 1);
neuper@52113	540	val (Form f, tac, asms) = pt_extract (pt, p);
neuper@52113	541	if p = ([1], Res) andalso term2str (get_obj g_res pt (fst p)) = "x + 1 + -1 * 2 = 0"
wneuper@59248	542	then () else error "--- setContext..Thy --- autoCalculate 1 (Step 1) #1";
neuper@52113	543
wneuper@59248	544	autoCalculate 1 CompleteCalc;
neuper@52113	545	val (((pt,_),_), p) = (get_calc 1, get_pos 1 1);
neuper@52113	546	val (Form f, tac, asms) = pt_extract (pt, p);
neuper@52113	547
neuper@52113	548	if term2str f = "[x = 1]" andalso p = ([], Res) then ()
wneuper@59248	549	else error "--- setContext..Thy --- autoCalculate CompleteCalc";
neuper@52113	550	DEconstrCalcTree 1;
neuper@52113	551
neuper@52113	552	"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
neuper@52113	553	"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
neuper@52113	554	"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
neuper@52113	555	CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
neuper@52113	556	("Test", ["sqroot-test","univariate","equation","test"],
neuper@52113	557	["Test","squ-equ-test-subpbl1"]))];
neuper@52113	558	Iterator 1; moveActiveRoot 1;
wneuper@59248	559	autoCalculate 1 CompleteToSubpbl;
neuper@52113	560	refFormula 1 (get_pos 1 1); (<ISA> -1 + x = 0 </ISA>);
neuper@52113	561	val ((pt,_),_) = get_calc 1;
neuper@52113	562	val str = pr_ptree pr_short pt;
neuper@52113	563	writeln str;
neuper@52113	564	if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n"
neuper@52113	565	then () else
neuper@52113	566	error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl-1";
neuper@52113	567
wneuper@59248	568	autoCalculate 1 (Step 1); (proceeds only, of NOT 1 step before subplb)
wneuper@59248	569	autoCalculate 1 CompleteToSubpbl;
neuper@52113	570	val ((pt,_),_) = get_calc 1;
neuper@52113	571	val str = pr_ptree pr_short pt;
neuper@52113	572	writeln str;
wneuper@59248	573	autoCalculate 1 CompleteCalc; (das geht ohnehin !);
neuper@52113	574	val ((pt,_),_) = get_calc 1;
neuper@52113	575	val p = get_pos 1 1;
neuper@52113	576
neuper@52113	577	val (Form f, tac, asms) = pt_extract (pt, p);
neuper@52113	578	if term2str f = "[x = 1]" andalso p = ([], Res) then () else
neuper@52113	579	error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl 1";
neuper@52113	580	DEconstrCalcTree 1;
neuper@52113	581
neuper@52113	582	"--------- rat-eq + subpbl: no_met, NO solution dropped -";
neuper@52113	583	"--------- rat-eq + subpbl: no_met, NO solution dropped -";
neuper@52113	584	"--------- rat-eq + subpbl: no_met, NO solution dropped -";
neuper@52113	585	CalcTree
neuper@52113	586	[(["equality ((5*x)/(x - 2) - x/(x+2)=(4::real))", "solveFor x","solutions L"],
neuper@52113	587	("RatEq", ["univariate","equation"], ["no_met"]))];
neuper@52113	588	Iterator 1;
neuper@52113	589	moveActiveRoot 1;
neuper@52113	590	fetchProposedTactic 1;
neuper@52113	591
neuper@52113	592	setNextTactic 1 (Model_Problem);
wneuper@59248	593	autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@52113	594
neuper@52113	595	setNextTactic 1 (Specify_Theory "RatEq");
wneuper@59248	596	autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@52113	597	setNextTactic 1 (Specify_Problem ["rational","univariate","equation"]);
wneuper@59248	598	autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@52113	599	setNextTactic 1 (Specify_Method ["RatEq","solve_rat_equation"]);
wneuper@59248	600	autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@52113	601	setNextTactic 1 (Apply_Method ["RatEq","solve_rat_equation"]);
wneuper@59248	602	autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@52113	603	setNextTactic 1 (Rewrite_Set "RatEq_simplify");
wneuper@59248	604	autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@52113	605	setNextTactic 1 (Rewrite_Set "norm_Rational");
wneuper@59248	606	autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@52113	607	setNextTactic 1 (Rewrite_Set "RatEq_eliminate");
wneuper@59248	608	autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@52113	609	(* __________ for "12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2)"*)
neuper@52113	610	setNextTactic 1 (Subproblem ("PolyEq", ["normalize","polynomial",
neuper@52113	611	"univariate","equation"]));
wneuper@59248	612	autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@52113	613	setNextTactic 1 (Model_Problem );
wneuper@59248	614	autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@52113	615	setNextTactic 1 (Specify_Theory "PolyEq");
wneuper@59248	616	autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@52113	617	setNextTactic 1 (Specify_Problem ["normalize","polynomial",
neuper@52113	618	"univariate","equation"]);
wneuper@59248	619	autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@52113	620	setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
wneuper@59248	621	autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@52113	622	setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);
wneuper@59248	623	autoCalculate 1 (Step 1); fetchProposedTactic 1;
wneuper@59252	624	setNextTactic 1 (Rewrite ("all_left", Thm.prop_of @{thm all_left}));
wneuper@59248	625	autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@52113	626	setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "make_ratpoly_in"));
wneuper@59248	627	autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@52113	628	(* __________ for "16 + 12 * x = 0"*)
neuper@52113	629	setNextTactic 1 (Subproblem ("PolyEq",
neuper@52113	630	["degree_1","polynomial","univariate","equation"]));
wneuper@59248	631	autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@52113	632	setNextTactic 1 (Model_Problem );
wneuper@59248	633	autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@52113	634	setNextTactic 1 (Specify_Theory "PolyEq");
neuper@52113	635	(------------- some trials in the problem-hierarchy ---------------)
neuper@55279	636	setNextTactic 1 (Specify_Problem ["LINEAR","univariate","equation"]);
wneuper@59248	637	autoCalculate 1 (Step 1); fetchProposedTactic 1; (<ERROR> helpless </ERROR> !!!)
neuper@52113	638	setNextTactic 1 (Refine_Problem ["univariate","equation"]);
neuper@52113	639	(------------------------------------------------------------------)
wneuper@59248	640	autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@52113	641	setNextTactic 1 (Specify_Method ["PolyEq","solve_d1_polyeq_equation"]);
wneuper@59248	642	autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@52113	643	setNextTactic 1 (Apply_Method ["PolyEq","solve_d1_polyeq_equation"]);
wneuper@59248	644	autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@52113	645	setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "d1_polyeq_simplify"));
wneuper@59248	646	autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@52113	647	setNextTactic 1 (Rewrite_Set "polyeq_simplify");
wneuper@59248	648	autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@52113	649	setNextTactic 1 Or_to_List;
wneuper@59248	650	autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@52113	651	setNextTactic 1 (Check_elementwise "Assumptions");
wneuper@59248	652	autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@52113	653	setNextTactic 1 (Check_Postcond ["degree_1","polynomial",
neuper@52113	654	"univariate","equation"]);
wneuper@59248	655	autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@52113	656	setNextTactic 1 (Check_Postcond ["normalize","polynomial",
neuper@52113	657	"univariate","equation"]);
wneuper@59248	658	autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@52113	659	setNextTactic 1 (Check_Postcond ["rational","univariate","equation"]);
neuper@52113	660	val (ptp,_) = get_calc 1;
neuper@52113	661	val (Form t,_,_) = pt_extract ptp;
neuper@52113	662	if get_pos 1 1 = ([], Res) andalso term2str t = "[x = -4 / 3]" then ()
neuper@52113	663	else writeln "FE-inteface.sml: diff.behav. in rat-eq + subpbl: no_met, NO ..";
neuper@52113	664	DEconstrCalcTree 1;
neuper@52113	665
neuper@52113	666	"--------- tryMatchProblem, tryRefineProblem ------------";
neuper@52113	667	"--------- tryMatchProblem, tryRefineProblem ------------";
neuper@52113	668	"--------- tryMatchProblem, tryRefineProblem ------------";
neuper@52113	669	(*{\bf\UC{Having \isac{} Refine the Problem
neuper@52113	670	* Automatically}\label{SPECIFY:refine-auto}\\} test match and refine with
neuper@52113	671	* x^^^2 + 4*x + 5 = 2
neuper@52113	672	see isac.bridge.TestSpecify#testMatchRefine*)
neuper@52113	673	CalcTree
neuper@52113	674	[(["equality (x^2 + 4*x + 5 = (2::real))", "solveFor x","solutions L"],
neuper@52113	675	("Isac",
neuper@52113	676	["univariate","equation"],
neuper@52113	677	["no_met"]))];
neuper@52113	678	Iterator 1;
neuper@52113	679	moveActiveRoot 1;
neuper@52113	680
neuper@52113	681	fetchProposedTactic 1;
neuper@52113	682	setNextTactic 1 (Model_Problem );
neuper@52113	683	(..this tactic should be done 'tacitly', too !)
neuper@52113	684
neuper@52113	685	(*
wneuper@59248	686	autoCalculate 1 CompleteCalcHead;
neuper@52113	687	checkContext 1 ([],Pbl) "pbl_equ_univ";
neuper@52113	688	checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
neuper@52113	689	*)
neuper@52113	690
wneuper@59248	691	autoCalculate 1 (Step 1);
neuper@52113	692
neuper@52113	693	fetchProposedTactic 1;
neuper@52113	694	setNextTactic 1 (Add_Given "equality (x ^^^ 2 + 4 * x + 5 = (2::real))");
wneuper@59248	695	autoCalculate 1 (Step 1);
neuper@52113	696
neuper@52113	697	"--------- we go into the ProblemBrowser (_NO_ pblID selected) -";
neuper@52113	698	initContext 1 Pbl_ ([],Pbl);
wneuper@59173	699	(* this would break if a calculation would be inserted before: CALCID...
wneuper@59173	700	and pattern matching is not available in *.java.
wneuper@59173	701	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. . . . . . . matches (?a = ?b) (x ^ 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"
wneuper@59173	702	then () else error "--- tryMatchProblem, tryRefineProblem: initContext 1 Pbl_ ([],Pbl); CHANGED";
wneuper@59173	703	*)
neuper@52113	704	initContext 1 Met_ ([],Pbl);
wneuper@59173	705	(<SYSERROR><CALCID>1</CALCID><ERROR>error in kernel 33</ERROR></SYSERROR>)
neuper@52113	706
neuper@52113	707	"--------- this match will show some incomplete items: ---------";
neuper@52113	708
neuper@52113	709	checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
neuper@52113	710	checkContext 1 ([],Pbl) (kestoreID2guh Met_ ["LinEq", "solve_lineq_equation"]);
neuper@52113	711
neuper@52113	712
neuper@52113	713	fetchProposedTactic 1;
wneuper@59248	714	setNextTactic 1 (Add_Given "solveFor x"); autoCalculate 1 (Step 1);
neuper@52113	715
neuper@52113	716	fetchProposedTactic 1;
wneuper@59248	717	setNextTactic 1 (Add_Find "solutions L"); autoCalculate 1 (Step 1);
neuper@52113	718
neuper@52113	719	"--------- this is a matching model (all items correct): -------";
neuper@52113	720	checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
neuper@52113	721	"--------- this is a NOT matching model (some 'false': ---------";
neuper@55279	722	checkContext 1 ([],Pbl)(kestoreID2guh Pbl_ ["LINEAR","univariate","equation"]);
neuper@52113	723
neuper@52113	724	"--------- find out a matching problem: ------------------------";
neuper@52113	725	"--------- find out a matching problem (FAILING: no new pbl) ---";
neuper@55279	726	refineProblem 1([],Pbl)(pblID2guh ["LINEAR","univariate","equation"]);
neuper@52113	727
neuper@52113	728	"--------- find out a matching problem (SUCCESSFUL) ------------";
neuper@52113	729	refineProblem 1 ([],Pbl) (pblID2guh ["univariate","equation"]);
neuper@52113	730
neuper@52113	731	"--------- tryMatch, tryRefine did not change the calculation -";
neuper@52113	732	"--------- this is done by <TRANSFER> on the pbl-browser: ------";
neuper@52113	733	setNextTactic 1 (Specify_Problem ["normalize","polynomial",
neuper@52113	734	"univariate","equation"]);
wneuper@59248	735	autoCalculate 1 (Step 1);
neuper@52113	736	(*WN050904 fetchProposedTactic again --> Specify_Problem ["normalize",...
neuper@52113	737	and Specify_Theory skipped in comparison to below ---^^^-inserted *)
neuper@52113	738	(------------vvv-inserted-----------------------------------------------)
neuper@52113	739	fetchProposedTactic 1;
neuper@52113	740	setNextTactic 1 (Specify_Problem ["normalize","polynomial",
neuper@52113	741	"univariate","equation"]);
wneuper@59248	742	autoCalculate 1 (Step 1);
neuper@52113	743
neuper@52113	744	(and Specify_Theory skipped by fetchProposedTactic ?!?)
neuper@52113	745
neuper@52113	746	fetchProposedTactic 1;
neuper@52113	747	setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
wneuper@59248	748	autoCalculate 1 (Step 1);
neuper@52113	749
neuper@52113	750	fetchProposedTactic 1;
neuper@52113	751	setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);
neuper@52113	752
wneuper@59248	753	autoCalculate 1 CompleteCalc;
neuper@52113	754
neuper@52113	755	val ((pt,_),_) = get_calc 1;
neuper@52113	756	show_pt pt;
neuper@52113	757	val p = get_pos 1 1;
neuper@52113	758	val (Form f, tac, asms) = pt_extract (pt, p);
neuper@52113	759	if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else
neuper@52113	760	error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
neuper@52113	761
neuper@52113	762	(------------^^^-inserted-----------------------------------------------)
neuper@52113	763	(*WN050904 the fetchProposedTactic's below may not have worked like that
neuper@52113	764	before, too, because there was no check*)
neuper@52113	765	fetchProposedTactic 1;
neuper@52113	766	setNextTactic 1 (Specify_Theory "PolyEq");
wneuper@59248	767	autoCalculate 1 (Step 1);
neuper@52113	768
neuper@52113	769	fetchProposedTactic 1;
neuper@52113	770	setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
wneuper@59248	771	autoCalculate 1 (Step 1);
neuper@52113	772
neuper@52113	773	fetchProposedTactic 1;
neuper@52113	774	"--------- now the calc-header is ready for enter 'solving' ----";
wneuper@59248	775	autoCalculate 1 CompleteCalc;
neuper@52113	776
neuper@52113	777	val ((pt,_),_) = get_calc 1;
neuper@52113	778	rootthy pt;
neuper@52113	779	show_pt pt;
neuper@52113	780	val p = get_pos 1 1;
neuper@52113	781	val (Form f, tac, asms) = pt_extract (pt, p);
neuper@52113	782	if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else
neuper@52113	783	error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
neuper@52113	784
neuper@52113	785	DEconstrCalcTree 1;
neuper@52113	786
neuper@52113	787	"--------- modifyCalcHead, resetCalcHead, modelProblem --";
neuper@52113	788	"--------- modifyCalcHead, resetCalcHead, modelProblem --";
neuper@52113	789	"--------- modifyCalcHead, resetCalcHead, modelProblem --";
neuper@52113	790	CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
neuper@52113	791	("Test", ["sqroot-test","univariate","equation","test"],
neuper@52113	792	["Test","squ-equ-test-subpbl1"]))];
neuper@52113	793	Iterator 1;
neuper@52113	794	moveActiveRoot 1;
neuper@52113	795
neuper@52113	796	modifyCalcHead 1 (([],Pbl),(the position from refFormula)
neuper@52113	797	"solve (x+1=2, x)",(the headline)
neuper@52113	798	[Given ["equality (x+1=(2::real))", "solveFor x"],
neuper@52113	799	Find ["solutions L"](,Relate [])],
neuper@52113	800	Pbl,
neuper@52113	801	("Test",
neuper@52113	802	["sqroot-test","univariate","equation","test"],
neuper@52113	803	["Test","squ-equ-test-subpbl1"]));
neuper@52113	804
neuper@52113	805	val ((Nd (PblObj {env = NONE,
neuper@52113	806	fmz = (fm, tpm),
neuper@52113	807	loc = (SOME scrst_ctxt, NONE),
neuper@52113	808	ctxt,
neuper@52113	809	cell = NONE,
neuper@52113	810	meth,
neuper@52113	811	spec = (thy,
neuper@52113	812	["sqroot-test", "univariate", "equation", "test"],
neuper@52113	813	["Test", "squ-equ-test-subpbl1"]),
neuper@52113	814	probl,
neuper@52113	815	branch = TransitiveB,
neuper@52113	816	origin,
neuper@52113	817	ostate = Incomplete,
neuper@52113	818	result},
neuper@52113	819	[]),
neuper@52113	820	([], Pbl)),
neuper@52113	821	[]) = get_calc 1;
neuper@52113	822	(WN110622: is the same as in 2002, but shouldn't be probl = [3 items?])
neuper@52113	823	if length meth = 0 andalso length probl = 0 (just some items tested) then ()
neuper@52113	824	else error "--- modifyCalcHead, resetCalcHead, modelProblem 1 --";
neuper@52113	825
neuper@52113	826	resetCalcHead 1;
neuper@52113	827	modelProblem 1;
neuper@52113	828
neuper@52113	829	get_calc 1;
neuper@52113	830	val ((Nd (PblObj {env = NONE,
neuper@52113	831	fmz = (fm, tpm),
neuper@52113	832	loc = (SOME scrst_ctxt, NONE),
neuper@52113	833	ctxt,
neuper@52113	834	cell = NONE,
neuper@52113	835	meth,
neuper@52113	836	spec = ("e_domID", ["e_pblID"], ["e_metID"]),
neuper@52113	837	probl,
neuper@52113	838	branch = TransitiveB,
neuper@52113	839	origin,
neuper@52113	840	ostate = Incomplete,
neuper@52113	841	result},
neuper@52113	842	[]),
neuper@52113	843	([], Pbl)),
neuper@52113	844	[]) = get_calc 1;
neuper@52113	845	if length meth = 3 andalso length probl = 3 (just some items tested) then ()
neuper@52113	846	else error "--- modifyCalcHead, resetCalcHead, modelProblem 2 --";
neuper@52113	847
neuper@52113	848	"--------- maximum-example, UC: Modeling an example -----";
neuper@52113	849	"--------- maximum-example, UC: Modeling an example -----";
neuper@52113	850	"--------- maximum-example, UC: Modeling an example -----";
neuper@52113	851	(* {\bf\UC{Editing the Model}\label{SPECIFY:enter}\label{SPECIFY:check}\\}
neuper@52113	852	see isac.bridge.TestModel#testEditItems
neuper@52113	853	*)
neuper@52113	854	val elems = ["fixedValues [r=Arbfix]","maximum A","valuesFor [a,b]",
neuper@52113	855	"relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]",
neuper@52113	856	"relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]",
neuper@52113	857	"relations [A=ab, a/2=rsin alpha, b/2=r*cos alpha]",
neuper@52113	858	(^^^ these are the elements for the root-problem (in variants))
neuper@52113	859	(vvv these are elements required for subproblems)
neuper@52113	860	"boundVariable a","boundVariable b","boundVariable alpha",
neuper@52113	861	"interval {x::real. 0 <= x & x <= 2*r}",
neuper@52113	862	"interval {x::real. 0 <= x & x <= 2*r}",
neuper@52113	863	"interval {x::real. 0 <= x & x <= pi}",
neuper@52113	864	"errorBound (eps=(0::real))"]
neuper@52113	865	(specifying is not interesting for this example)
neuper@52113	866	val spec = ("DiffApp", ["maximum_of","function"],
neuper@52113	867	["DiffApp","max_by_calculus"]);
neuper@52113	868	(the empty model with descriptions for user-guidance by Model_Problem)
neuper@52113	869	val empty_model = [Given ["fixedValues []"],
neuper@52113	870	Find ["maximum", "valuesFor"],
neuper@52113	871	Relate ["relations []"]];
neuper@52113	872	DEconstrCalcTree 1;
neuper@52113	873
neuper@52113	874	"#################################################################";
neuper@52113	875
neuper@52113	876	CalcTree [(elems, spec)];
neuper@52113	877	Iterator 1;
neuper@52113	878	moveActiveRoot 1;
neuper@52113	879	refFormula 1 (get_pos 1 1);
neuper@52113	880	(this gives a completely empty model)
neuper@52113	881
neuper@52113	882	fetchProposedTactic 1;
neuper@52113	883	(fill the CalcHead with Descriptions...)
neuper@52113	884	setNextTactic 1 (Model_Problem );
wneuper@59248	885	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@52113	886
neuper@52113	887	(*user input is !!!!!EITHER!!!!! _some_ (at least one) items of the model
neuper@52113	888	!!!!!OR!!!!! _one_ part of the specification !!!!!!!!!!!!!*)
neuper@52113	889	(input of two items, 'fixedValues [r=Arbfix]' and 'maximum b'...)
neuper@52113	890	modifyCalcHead 1 (([],Pbl) (position, from previous refFormula),
neuper@52113	891	"Problem (DiffApp.thy, [maximum_of, function])",
neuper@52113	892	(the head-form ^^^ is not used for input here)
neuper@52113	893	[Given ["fixedValues [r=Arbfix]"(new input)],
neuper@52113	894	Find ["maximum b"(new input), "valuesFor"],
neuper@52113	895	Relate ["relations"]],
neuper@52113	896	(input (Arbfix will dissappear soon))
neuper@52113	897	Pbl (belongsto),
neuper@52113	898	e_spec (no input to the specification));
neuper@52113	899
neuper@52113	900	(*the user does not know, what 'superfluous' for 'maximum b' may mean
neuper@52113	901	and asks what to do next*)
neuper@52113	902	fetchProposedTactic 1;
neuper@52113	903	(the student follows the advice)
neuper@52113	904	setNextTactic 1 (Add_Find "maximum A"); (FIXME.17.11.03: does not yet work)
wneuper@59248	905	autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@52113	906
neuper@52113	907	(this input completes the model)
neuper@52113	908	modifyCalcHead 1 (([],Pbl), "not used here",
neuper@52113	909	[Given ["fixedValues [r=Arbfix]"],
neuper@52113	910	Find ["maximum A", "valuesFor [a,b]"(new input)],
neuper@52113	911	Relate ["relations [A=a*b, \
neuper@52113	912	\(a/2)^2 + (b/2)^2 = r^2]"]], Pbl, e_spec);
neuper@52113	913
neuper@52113	914	(*specification is not interesting and should be skipped by the dialogguide;
neuper@52113	915	!!!!!!!!!!!!!!!!!!!! input of ONE part at a time !!!!!!!!!!!!!!!!!!!!!!*)
neuper@52113	916	modifyCalcHead 1 (([],Pbl), "not used here",
neuper@52113	917	[Given ["fixedValues [r=Arbfix]"],
neuper@52113	918	Find ["maximum A", "valuesFor [a,b]"(new input)],
neuper@52113	919	Relate ["relations [A=a*b, \
neuper@52113	920	\(a/2)^2 + (b/2)^2 = r^2]"]], Pbl,
neuper@52113	921	("DiffApp", ["e_pblID"], ["e_metID"]));
neuper@52113	922	modifyCalcHead 1 (([],Pbl), "not used here",
neuper@52113	923	[Given ["fixedValues [r=Arbfix]"],
neuper@52113	924	Find ["maximum A", "valuesFor [a,b]"(new input)],
neuper@52113	925	Relate ["relations [A=a*b, \
neuper@52113	926	\(a/2)^2 + (b/2)^2 = r^2]"]], Pbl,
neuper@52113	927	("DiffApp", ["maximum_of","function"],
neuper@52113	928	["e_metID"]));
neuper@52113	929	modifyCalcHead 1 (([],Pbl), "not used here",
neuper@52113	930	[Given ["fixedValues [r=Arbfix]"],
neuper@52113	931	Find ["maximum A", "valuesFor [a,b]"(new input)],
neuper@52113	932	Relate ["relations [A=a*b, \
neuper@52113	933	\(a/2)^2 + (b/2)^2 = r^2]"]], Pbl,
neuper@52113	934	("DiffApp", ["maximum_of","function"],
neuper@52113	935	["DiffApp","max_by_calculus"]));
neuper@52113	936	(this final calcHead now has STATUS 'complete' !)
neuper@52113	937	DEconstrCalcTree 1;
neuper@52113	938
neuper@52113	939	"--------- solve_linear from pbl-hierarchy --------------";
neuper@52113	940	"--------- solve_linear from pbl-hierarchy --------------";
neuper@52113	941	"--------- solve_linear from pbl-hierarchy --------------";
neuper@55279	942	val (fmz, sp) = ([], ("", ["LINEAR","univariate","equation","test"], []));
neuper@52113	943	CalcTree [(fmz, sp)];
neuper@52113	944	Iterator 1; moveActiveRoot 1;
neuper@52113	945	refFormula 1 (get_pos 1 1);
neuper@52113	946	modifyCalcHead 1 (([],Pbl),"solve (1+-1*2+x=(0::real))",
neuper@52113	947	[Given ["equality (1+-1*2+x=(0::real))", "solveFor x"],
neuper@52113	948	Find ["solutions L"]],
neuper@52113	949	Pbl,
neuper@55279	950	("Test", ["LINEAR","univariate","equation","test"],
neuper@52113	951	["Test","solve_linear"]));
wneuper@59248	952	autoCalculate 1 CompleteCalc;
neuper@52113	953	refFormula 1 (get_pos 1 1);
neuper@52113	954	val ((pt,_),_) = get_calc 1;
neuper@52113	955	val p = get_pos 1 1;
neuper@52113	956	val (Form f, tac, asms) = pt_extract (pt, p);
neuper@52113	957	if term2str f = "[x = 1]" andalso p = ([], Res)
neuper@52113	958	andalso terms2str asms = "[\"matches (?a = ?b) (1 + -1 * 2 + x = 0)\"]" then ()
neuper@52113	959	else error "FE-interface.sml: diff.behav. in from pbl -hierarchy";
neuper@52113	960	DEconstrCalcTree 1;
neuper@52113	961
neuper@52113	962	"--------- solve_linear as in an algebra system (CAS)----";
neuper@52113	963	"--------- solve_linear as in an algebra system (CAS)----";
neuper@52113	964	"--------- solve_linear as in an algebra system (CAS)----";
neuper@52113	965	(WN120210?not ME:\label{UC:cas-input} UC 30.1.2.5 p.168)
neuper@52113	966	val (fmz, sp) = ([], ("", [], []));
neuper@52113	967	CalcTree [(fmz, sp)];
neuper@52113	968	Iterator 1; moveActiveRoot 1;
neuper@52113	969	modifyCalcHead 1 (([],Pbl),"solveTest (1+-1*2+x=0,x)", [], Pbl, ("", [], []));
wneuper@59248	970	autoCalculate 1 CompleteCalc;
neuper@52113	971	refFormula 1 (get_pos 1 1);
neuper@52113	972	val ((pt,_),_) = get_calc 1;
neuper@52113	973	val p = get_pos 1 1;
neuper@52113	974	val (Form f, tac, asms) = pt_extract (pt, p);
neuper@52113	975	if term2str f = "[x = 1]" andalso p = ([], Res)
neuper@52113	976	andalso terms2str asms = "[\"matches (?a = ?b) (1 + -1 * 2 + x = 0)\"]" then ()
neuper@52113	977	else error "FE-interface.sml: diff.behav. in from pbl -hierarchy";
neuper@52113	978	DEconstrCalcTree 1;
neuper@52113	979
neuper@52113	980	"--------- interSteps: on 'miniscript with mini-subpbl' -";
neuper@52113	981	"--------- interSteps: on 'miniscript with mini-subpbl' -";
neuper@52113	982	"--------- interSteps: on 'miniscript with mini-subpbl' -";
neuper@52113	983	CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
neuper@52113	984	("Test", ["sqroot-test","univariate","equation","test"],
neuper@52113	985	["Test","squ-equ-test-subpbl1"]))];
neuper@52113	986	Iterator 1;
neuper@52113	987	moveActiveRoot 1;
wneuper@59248	988	autoCalculate 1 CompleteCalc;
neuper@52113	989	val ((pt,_),_) = get_calc 1;
neuper@52113	990	show_pt pt;
neuper@52113	991
neuper@52113	992	(UC\label{UC:inter-steps} UC 30.3.5.5 p.178)
neuper@52113	993	interSteps 1 ([2],Res);
neuper@52113	994	val ((pt,_),_) = get_calc 1; show_pt pt (new ([2,1],Frm)..([2,6],Res));
neuper@52113	995	val (unc, del, gen) = (([1],Res),([1],Res),([2,6],Res));
neuper@52113	996	getFormulaeFromTo 1 unc gen 1 false;
neuper@52113	997
neuper@52113	998	(UC\label{UC:inter-steps} UC 30.3.5.5 p.178)
neuper@52113	999	interSteps 1 ([3,2],Res);
neuper@52113	1000	val ((pt,_),_) = get_calc 1; show_pt pt (new ([3,2,1],Frm)..([3,2,2],Res));
neuper@52113	1001	val (unc, del, gen) = (([3,1],Res),([3,1],Res),([3,2,2],Res));
neuper@52113	1002	getFormulaeFromTo 1 unc gen 1 false;
neuper@52113	1003
neuper@52113	1004	(UC\label{UC:inter-steps} UC 30.3.5.5 p.178)
neuper@52113	1005	interSteps 1 ([3],Res) (no new steps in subproblems);
neuper@52113	1006	val (unc, del, gen) = (([3],Pbl),([3],Pbl),([3,2],Res));
neuper@52113	1007	getFormulaeFromTo 1 unc gen 1 false;
neuper@52113	1008
neuper@52113	1009	(UC\label{UC:inter-steps} UC 30.3.5.5 p.178)
neuper@52113	1010	interSteps 1 ([],Res) (no new steps in subproblems);
neuper@52113	1011	val (unc, del, gen) = (([],Pbl),([],Pbl),([4],Res));
neuper@52113	1012	getFormulaeFromTo 1 unc gen 1 false;
neuper@52113	1013	DEconstrCalcTree 1;
neuper@52113	1014
neuper@52113	1015	"--------- getTactic, fetchApplicableTactics ------------";
neuper@52113	1016	"--------- getTactic, fetchApplicableTactics ------------";
neuper@52113	1017	"--------- getTactic, fetchApplicableTactics ------------";
neuper@52113	1018	(* compare test/../script.sml
neuper@52113	1019	"----------- fun sel_rules ---------------------------------------";
neuper@52113	1020	*)
neuper@52113	1021	CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
neuper@52113	1022	("Test", ["sqroot-test","univariate","equation","test"],
neuper@52113	1023	["Test","squ-equ-test-subpbl1"]))];
neuper@52113	1024	Iterator 1; moveActiveRoot 1;
wneuper@59248	1025	autoCalculate 1 CompleteCalc;
neuper@52113	1026	val ((pt,_),_) = get_calc 1;
neuper@52113	1027	show_pt pt;
neuper@52113	1028
neuper@52113	1029	(*UC\label{SOLVE:HIDE:getTactic} \label{SOLVE:AUTO:tactic} UC 30.3.3.1 p.176
neuper@52113	1030	WN120210 not impl. in FE*)
neuper@52113	1031	getTactic 1 ([],Pbl);
neuper@52113	1032	getTactic 1 ([1],Res);
neuper@52113	1033	getTactic 1 ([3],Pbl);
neuper@52113	1034	getTactic 1 ([3,1],Frm);
neuper@52113	1035	getTactic 1 ([3],Res);
neuper@52113	1036	getTactic 1 ([],Res);
neuper@52113	1037
neuper@52113	1038	(UC\label{SOLVE:MANUAL:TACTIC:listall} UC 30.3.2.2 p.175)
neuper@52113	1039	fetchApplicableTactics 1 99999 ([],Pbl);
neuper@52113	1040	fetchApplicableTactics 1 99999 ([1],Res);
neuper@52113	1041	fetchApplicableTactics 1 99999 ([3],Pbl);
neuper@52113	1042	fetchApplicableTactics 1 99999 ([3,1],Res);
neuper@52113	1043	fetchApplicableTactics 1 99999 ([3],Res);
neuper@52113	1044	fetchApplicableTactics 1 99999 ([],Res);
neuper@52113	1045	DEconstrCalcTree 1;
neuper@52113	1046
neuper@52113	1047	"--------- getAssumptions, getAccumulatedAsms -----------";
neuper@52113	1048	"--------- getAssumptions, getAccumulatedAsms -----------";
neuper@52113	1049	"--------- getAssumptions, getAccumulatedAsms -----------";
neuper@52113	1050	CalcTree
neuper@52113	1051	[(["equality (x/(x^2 - 6x+9) - 1/(x^2 - 3x) =1/x)",
neuper@52113	1052	"solveFor x","solutions L"],
neuper@52113	1053	("RatEq",["univariate","equation"],["no_met"]))];
neuper@52113	1054	Iterator 1; moveActiveRoot 1;
wneuper@59248	1055	autoCalculate 1 CompleteCalc;
neuper@52113	1056	val ((pt,_),_) = get_calc 1;
neuper@52113	1057	val p = get_pos 1 1;
neuper@52113	1058	val (Form f, tac, asms) = pt_extract (pt, p);
neuper@52113	1059	(*============ inhibit exn WN120316 compare 2002--2011 ===========================
neuper@52113	1060	if map term2str asms =
neuper@52113	1061	["True \|\n~ lhs ((3 + -1 * x + x ^^^ 2) * x =\n" ^
neuper@52113	1062	" 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x", "-6 * x + 5 * x ^^^ 2 = 0",
neuper@52113	1063	"lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x",
neuper@52113	1064	"lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2",
neuper@52113	1065	"9 * x + -6 * x ^^^ 2 + x ^^^ 3 ~= 0"]
neuper@52113	1066	andalso term2str f = "[-6 * x + 5 * x ^^^ 2 = 0]" andalso p = ([], Res) then ()
neuper@52113	1067	else error "TODO compare 2002--2011"; (...data during test --- x / (x ^ 2 - 6 x + 9) - 1...*)
neuper@52113	1068	============ inhibit exn WN120316 compare 2002--2011 ===========================*)
neuper@52113	1069	if p = ([], Res) andalso term2str f = "[]" (see WN120317.TODO dropped rateq)
neuper@52113	1070	andalso asms = [] (STRANGE!, compare test --- x / (x ^ 2 - 6 x + 9) - 1 / (x ^ 2 ...*)
neuper@52113	1071	then () else error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b [x = 6 / 5]";
neuper@52113	1072
neuper@52113	1073	(UC\label{SOLVE:HELP:assumptions} UC 30.3.5.1 p.178)
neuper@52113	1074	getAssumptions 1 ([3], Res);
neuper@52113	1075	getAssumptions 1 ([5], Res);
neuper@52113	1076	(*UC\label{SOLVE:HELP:assumptions-origin} UC 30.3.5.2 p.178
neuper@52113	1077	WN0502 still without positions*)
neuper@52113	1078	getAccumulatedAsms 1 ([3], Res);
neuper@52113	1079	getAccumulatedAsms 1 ([5], Res);
neuper@52113	1080	DEconstrCalcTree 1;
neuper@52113	1081
neuper@52113	1082	"--------- arbitrary combinations of steps --------------";
neuper@52113	1083	"--------- arbitrary combinations of steps --------------";
neuper@52113	1084	"--------- arbitrary combinations of steps --------------";
neuper@52113	1085	CalcTree (start of calculation, return No.1)
neuper@52113	1086	[(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
neuper@52113	1087	("Test",
neuper@55279	1088	["LINEAR","univariate","equation","test"],
neuper@52113	1089	["Test","solve_linear"]))];
neuper@52113	1090	Iterator 1; moveActiveRoot 1;
neuper@52113	1091
neuper@52113	1092	fetchProposedTactic 1;
neuper@52113	1093	(ERROR get_calc 1 not existent)
neuper@52113	1094	setNextTactic 1 (Model_Problem );
wneuper@59248	1095	autoCalculate 1 (Step 1);
neuper@52113	1096	fetchProposedTactic 1;
neuper@52113	1097	fetchProposedTactic 1;
neuper@52113	1098
neuper@52113	1099	setNextTactic 1 (Add_Find "solutions L");
neuper@52113	1100	setNextTactic 1 (Add_Find "solutions L");
neuper@52113	1101
wneuper@59248	1102	autoCalculate 1 (Step 1);
wneuper@59248	1103	autoCalculate 1 (Step 1);
neuper@52113	1104
neuper@52113	1105	setNextTactic 1 (Specify_Theory "Test");
neuper@52113	1106	fetchProposedTactic 1;
wneuper@59248	1107	autoCalculate 1 (Step 1);
neuper@52113	1108
wneuper@59248	1109	autoCalculate 1 (Step 1);
wneuper@59248	1110	autoCalculate 1 (Step 1);
wneuper@59248	1111	autoCalculate 1 (Step 1);
wneuper@59248	1112	autoCalculate 1 (Step 1);
neuper@52113	1113	(------------------------- end calc-head)
neuper@52113	1114
neuper@52113	1115	fetchProposedTactic 1;
neuper@52113	1116	setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
wneuper@59248	1117	autoCalculate 1 (Step 1);
neuper@52113	1118
neuper@52113	1119	setNextTactic 1 (Rewrite_Set "Test_simplify");
neuper@52113	1120	fetchProposedTactic 1;
wneuper@59248	1121	autoCalculate 1 (Step 1);
neuper@52113	1122
wneuper@59248	1123	autoCalculate 1 CompleteCalc;
neuper@52113	1124	val ((pt,_),_) = get_calc 1;
neuper@52113	1125	val p = get_pos 1 1;
neuper@52113	1126	val (Form f, tac, asms) = pt_extract (pt, p);
neuper@52113	1127	if term2str f = "[x = 1]" andalso p = ([], Res) then () else
neuper@52113	1128	error "FE-interface.sml: diff.behav. in combinations of steps";
neuper@52113	1129	DEconstrCalcTree 1;
neuper@52113	1130
neuper@52113	1131	"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right"; (UC 30.3.2.4 p.175)
neuper@52113	1132	"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
neuper@52113	1133	"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
neuper@52113	1134	CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
neuper@52113	1135	("Test", ["sqroot-test","univariate","equation","test"],
neuper@52113	1136	["Test","squ-equ-test-subpbl1"]))];
neuper@52113	1137	Iterator 1;
neuper@52113	1138	moveActiveRoot 1;
wneuper@59248	1139	autoCalculate 1 CompleteCalcHead;
wneuper@59248	1140	autoCalculate 1 (Step 1);
wneuper@59248	1141	autoCalculate 1 (Step 1);
wneuper@59123	1142	appendFormula 1 "-1 + x = 0" (\|> Future.join);
neuper@52113	1143	(... returns calcChangedEvent with)
neuper@52113	1144	val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res));
neuper@52113	1145	getFormulaeFromTo 1 unc gen 99999 (all levels) false;
neuper@52113	1146
neuper@52113	1147	val ((pt,_),_) = get_calc 1;
neuper@52113	1148	val p = get_pos 1 1;
neuper@52113	1149	val (Form f, tac, asms) = pt_extract (pt, p);
neuper@52113	1150	if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
neuper@52113	1151	error "FE-interface.sml: diff.behav. in FORMULA:enter} right";
neuper@52113	1152	DEconstrCalcTree 1;
neuper@52113	1153
neuper@52113	1154	"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other"; (UC 30.3.2.4 p.175)
neuper@52113	1155	"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
neuper@52113	1156	"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
neuper@52113	1157	CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
neuper@52113	1158	("Test", ["sqroot-test","univariate","equation","test"],
neuper@52113	1159	["Test","squ-equ-test-subpbl1"]))];
neuper@52113	1160	Iterator 1;
neuper@52113	1161	moveActiveRoot 1;
wneuper@59248	1162	autoCalculate 1 CompleteCalcHead;
wneuper@59248	1163	autoCalculate 1 (Step 1);
wneuper@59248	1164	autoCalculate 1 (Step 1);
wneuper@59123	1165	appendFormula 1 "x - 1 = 0" (\|> Future.join);
neuper@52113	1166	val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res));
neuper@52113	1167	getFormulaeFromTo 1 unc gen 99999 (all levels) false;
neuper@52113	1168	(11 elements !!!)
neuper@52113	1169
neuper@52113	1170	val ((pt,_),_) = get_calc 1;
neuper@52113	1171	val p = get_pos 1 1;
neuper@52113	1172	val (Form f, tac, asms) = pt_extract (pt, p);
neuper@52113	1173	if term2str f = "x - 1 = 0" andalso p = ([2], Res) then () else
neuper@52113	1174	error "FE-interface.sml: diff.behav. in FORMULA:enter} other";
neuper@52113	1175	DEconstrCalcTree 1;
neuper@52113	1176
neuper@52113	1177	"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2"; (UC 30.3.2.4 p.175)
neuper@52113	1178	"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
neuper@52113	1179	"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
neuper@52113	1180	CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
neuper@52113	1181	("Test", ["sqroot-test","univariate","equation","test"],
neuper@52113	1182	["Test","squ-equ-test-subpbl1"]))];
neuper@52113	1183	Iterator 1;
neuper@52113	1184	moveActiveRoot 1;
wneuper@59248	1185	autoCalculate 1 CompleteCalcHead;
wneuper@59248	1186	autoCalculate 1 (Step 1);
wneuper@59248	1187	autoCalculate 1 (Step 1);
wneuper@59123	1188	appendFormula 1 "x = 1" (\|> Future.join);
neuper@52113	1189	(... returns calcChangedEvent with)
neuper@52113	1190	val (unc, del, gen) = (([1],Res), ([1],Res), ([3,2],Res));
neuper@52113	1191	getFormulaeFromTo 1 unc gen 99999 (all levels) false;
neuper@52113	1192	(6 elements !!!)
neuper@52113	1193
neuper@52113	1194	val ((pt,_),_) = get_calc 1;
neuper@52113	1195	val p = get_pos 1 1;
neuper@52113	1196	val (Form f, tac, asms) = pt_extract (pt, p);
neuper@52113	1197	if term2str f = "x = 1" andalso p = ([3,2], Res) then () else
neuper@52113	1198	error "FE-interface.sml: diff.behav. in FORMULA:enter} oth 2";
neuper@52113	1199	DEconstrCalcTree 1;
neuper@52113	1200
neuper@52113	1201	"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok"; (UC 30.3.2.4 p.175)
neuper@52113	1202	"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
neuper@52113	1203	"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
neuper@52113	1204	CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
neuper@52113	1205	("Test", ["sqroot-test","univariate","equation","test"],
neuper@52113	1206	["Test","squ-equ-test-subpbl1"]))];
neuper@52113	1207	Iterator 1;
neuper@52113	1208	moveActiveRoot 1;
wneuper@59248	1209	autoCalculate 1 CompleteCalcHead;
wneuper@59248	1210	autoCalculate 1 (Step 1);
wneuper@59248	1211	autoCalculate 1 (Step 1);
wneuper@59123	1212	appendFormula 1 "x - 4711 = 0" (\|> Future.join);
neuper@52113	1213	(... returns <ERROR> no derivation found </ERROR>)
neuper@52113	1214
neuper@52113	1215	val ((pt,_),_) = get_calc 1;
neuper@52113	1216	val p = get_pos 1 1;
neuper@52113	1217	val (Form f, tac, asms) = pt_extract (pt, p);
neuper@52113	1218	if term2str f = "x + 1 + -1 * 2 = 0" andalso p = ([1], Res) then () else
neuper@52113	1219	error "FE-interface.sml: diff.behav. in FORMULA:enter} NOTok";
neuper@52113	1220	DEconstrCalcTree 1;
neuper@52113	1221
neuper@52113	1222	"--------- replaceFormula {SOL:MAN:FOR:replace} right----"; (UC 30.3.2.5 p.176)
neuper@52113	1223	"--------- replaceFormula {SOL:MAN:FOR:replace} right----";
neuper@52113	1224	"--------- replaceFormula {SOL:MAN:FOR:replace} right----";
neuper@52113	1225	(\label{SOLVE:MANUAL:FORMULA:replace})
neuper@52113	1226	CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
neuper@52113	1227	("Test", ["sqroot-test","univariate","equation","test"],
neuper@52113	1228	["Test","squ-equ-test-subpbl1"]))];
neuper@52113	1229	Iterator 1;
neuper@52113	1230	moveActiveRoot 1;
wneuper@59248	1231	autoCalculate 1 CompleteCalc;
neuper@52113	1232	moveActiveFormula 1 ([2],Res);
neuper@52113	1233	replaceFormula 1 "-1 + x = 0" (i.e. repeats input);
neuper@52113	1234	(... returns <ERROR> formula not changed </ERROR>)
neuper@52113	1235
neuper@52113	1236	val ((pt,_),_) = get_calc 1;
neuper@52113	1237	val p = get_pos 1 1;
neuper@52113	1238	val (Form f, tac, asms) = pt_extract (pt, p);
neuper@52113	1239	if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
neuper@52113	1240	error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
neuper@52113	1241	if map fst (get_interval ([2],Res) ([],Res) 9999 pt) =
neuper@52113	1242	[([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
neuper@52113	1243	([3], Res), ([4], Res), ([], Res)] then () (nothing deleted!) else
neuper@52113	1244	error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2";
neuper@52113	1245
neuper@52113	1246	(WN050211 replaceFormula didn't work on second ctree: thus now tested...)
neuper@52113	1247	CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
neuper@52113	1248	("Test", ["sqroot-test","univariate","equation","test"],
neuper@52113	1249	["Test","squ-equ-test-subpbl1"]))];
neuper@52113	1250	Iterator 2;
neuper@52113	1251	moveActiveRoot 2;
wneuper@59248	1252	autoCalculate 2 CompleteCalc;
neuper@52113	1253	moveActiveFormula 2 ([2],Res);
neuper@52113	1254	replaceFormula 2 "-1 + x = 0" (i.e. repeats input);
neuper@52113	1255	(... returns <ERROR> formula not changed </ERROR>)
neuper@52113	1256
neuper@52113	1257	val ((pt,_),_) = get_calc 2;
neuper@52113	1258	val p = get_pos 2 1;
neuper@52113	1259	val (Form f, tac, asms) = pt_extract (pt, p);
neuper@52113	1260	if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
neuper@52113	1261	error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
neuper@52113	1262	if map fst (get_interval ([2],Res) ([],Res) 9999 pt) =
neuper@52113	1263	[([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
neuper@52113	1264	([3], Res), ([4], Res), ([], Res)] then () (nothing deleted!) else
neuper@52113	1265	error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2b";
neuper@52113	1266	DEconstrCalcTree 1;
neuper@52113	1267
neuper@52113	1268	"--------- replaceFormula {SOL:MAN:FOR:replace} other----"; (UC 30.3.2.5 p.176)
neuper@52113	1269	"--------- replaceFormula {SOL:MAN:FOR:replace} other----";
neuper@52113	1270	"--------- replaceFormula {SOL:MAN:FOR:replace} other----";
neuper@52113	1271	(\label{SOLVE:MANUAL:FORMULA:replace})
neuper@52113	1272	CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
neuper@52113	1273	("Test", ["sqroot-test","univariate","equation","test"],
neuper@52113	1274	["Test","squ-equ-test-subpbl1"]))];
neuper@52113	1275	Iterator 1;
neuper@52113	1276	moveActiveRoot 1;
wneuper@59248	1277	autoCalculate 1 CompleteCalc;
neuper@52113	1278	moveActiveFormula 1 ([2],Res); (there is "-1 + x = 0")
neuper@52113	1279	replaceFormula 1 "x - 1 = 0"; (<-------------------------------------)
neuper@52113	1280	(... returns calcChangedEvent with)
neuper@52113	1281	val (unc, del, gen) = (([1],Res), ([4],Res), ([2],Res));
neuper@52113	1282	getFormulaeFromTo 1 unc gen 99999 (all levels) false;
neuper@52113	1283
neuper@52113	1284	val ((pt,_),_) = get_calc 1;
neuper@52113	1285	show_pt pt;
neuper@52113	1286	val p = get_pos 1 1;
neuper@52113	1287	val (Form f, tac, asms) = pt_extract (pt, p);
neuper@52113	1288	if term2str f = "x - 1 = 0" andalso p = ([2], Res) then () else
neuper@52113	1289	error "FE-interface.sml: diff.behav. in FORMULA:replace} other 1";
neuper@52113	1290	(* for getting the list in whole length ...
wneuper@59111	1291	default_print_depth 99;map fst (get_interval ([1],Res) ([],Res) 9999 pt);default_print_depth 3;
neuper@52113	1292	*)
neuper@52113	1293	if map fst (get_interval ([1],Res) ([],Res) 9999 pt) =
neuper@52113	1294	[([1], Res), ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
neuper@52113	1295	([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2, 7], Res),
neuper@52113	1296	([2, 8], Res), ([2, 9], Res), ([2], Res)
neuper@52113	1297	(*WN060727 {cutlevup->test_trans} removed: ,
neuper@52113	1298	([], Res)(dropped, if test_trans doesnt stop at PblNd)*)] then () else
neuper@52113	1299	error "FE-interface.sml: diff.behav. in FORMULA:replace} other 2";
neuper@52113	1300	DEconstrCalcTree 1;
neuper@52113	1301
neuper@52113	1302	"--------- replaceFormula {SOL:MAN:FOR:replace} other 2--"; (UC 30.3.2.5 p.176)
neuper@52113	1303	"--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
neuper@52113	1304	"--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
neuper@52113	1305	(\label{SOLVE:MANUAL:FORMULA:replace})
neuper@52113	1306	CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
neuper@52113	1307	("Test", ["sqroot-test","univariate","equation","test"],
neuper@52113	1308	["Test","squ-equ-test-subpbl1"]))];
neuper@52113	1309	Iterator 1;
neuper@52113	1310	moveActiveRoot 1;
wneuper@59248	1311	autoCalculate 1 CompleteCalc;
neuper@52113	1312	moveActiveFormula 1 ([2],Res); (there is "-1 + x = 0")
neuper@52113	1313	replaceFormula 1 "x = 1"; (<-------------------------------------)
neuper@52113	1314	(... returns calcChangedEvent with ...)
neuper@52113	1315	val (unc, del, gen) = (([1],Res), ([4],Res), ([3,2],Res));
neuper@52113	1316	getFormulaeFromTo 1 unc gen 99999 (all levels) false;
neuper@52113	1317	(9 elements !!!)
neuper@52113	1318
neuper@52113	1319	val ((pt,_),_) = get_calc 1;
neuper@52113	1320	show_pt pt; (error: ...get_interval drops ([3,2],Res) ...)
neuper@52113	1321	val (t,_) = get_obj g_result pt [3,2]; term2str t;
neuper@52113	1322	if map fst (get_interval ([1],Res) ([],Res) 9999 pt) =
neuper@52113	1323	[([1], Res), ([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res),
neuper@52113	1324	([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
neuper@52113	1325	([3,2],Res)] then () else
neuper@52113	1326	error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 1";
neuper@52113	1327
neuper@52113	1328	val p = get_pos 1 1;
neuper@52113	1329	val (Form f, tac, asms) = pt_extract (pt, p);
neuper@52113	1330	if term2str f = "x = 1" andalso p = ([3,2], Res) then () else
neuper@52113	1331	error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 2";
neuper@52113	1332	DEconstrCalcTree 1;
neuper@52113	1333
neuper@52113	1334	"--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----"; (UC 30.3.2.5 p.176)
neuper@52113	1335	"--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
neuper@52113	1336	"--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
neuper@52113	1337	(\label{SOLVE:MANUAL:FORMULA:replace})
neuper@52113	1338	CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
neuper@52113	1339	("Test", ["sqroot-test","univariate","equation","test"],
neuper@52113	1340	["Test","squ-equ-test-subpbl1"]))];
neuper@52113	1341	Iterator 1;
neuper@52113	1342	moveActiveRoot 1;
wneuper@59248	1343	autoCalculate 1 CompleteCalc;
neuper@52113	1344	moveActiveFormula 1 ([2],Res); (there is "-1 + x = 0")
neuper@52113	1345	replaceFormula 1 "x - 4711 = 0";
neuper@52113	1346	(... returns <ERROR> no derivation found </ERROR>)
neuper@52113	1347
neuper@52113	1348	val ((pt,_),_) = get_calc 1;
neuper@52113	1349	show_pt pt;
neuper@52113	1350	val p = get_pos 1 1;
neuper@52113	1351	val (Form f, tac, asms) = pt_extract (pt, p);
neuper@52113	1352	if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
neuper@52113	1353	error "FE-interface.sml: diff.behav. in FORMULA:replace} NOTok";
neuper@52113	1354	DEconstrCalcTree 1;
neuper@52113	1355
neuper@52113	1356	"--------- UC errpat chain-rule-diff-both, fillpat by input ------";
neuper@52113	1357	"--------- UC errpat chain-rule-diff-both, fillpat by input ------";
neuper@52113	1358	"--------- UC errpat chain-rule-diff-both, fillpat by input ------";
s1210629013@55445	1359	reset_states ();
neuper@52113	1360	CalcTree
neuper@52113	1361	[(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
neuper@52113	1362	("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
neuper@52113	1363	Iterator 1;
neuper@52113	1364	moveActiveRoot 1;
wneuper@59248	1365	autoCalculate 1 CompleteCalcHead;
wneuper@59248	1366	autoCalculate 1 (Step 1);
wneuper@59248	1367	autoCalculate 1 (Step 1);(([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)))
wneuper@59123	1368	appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)" (\|> Future.join); (<<<<<<<=========================)
neuper@52113	1369	(* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),
neuper@52113	1370	would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well.
neuper@52113	1371	results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>
neuper@52113	1372	instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)
neuper@52113	1373	val ((pt,pos), _) = get_calc 1;
neuper@52113	1374	val p = get_pos 1 1;
neuper@52113	1375	val (Form f, _, asms) = pt_extract (pt, p);
neuper@52113	1376
neuper@52113	1377	if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
wneuper@59252	1378	get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"],
wneuper@59252	1379	("diff_sum", str2term "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v"))
neuper@52113	1380	then () else error "embed fun get_fillform changed 1";
neuper@52113	1381
neuper@52113	1382	(*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ====================
neuper@52113	1383	findFillpatterns 1 "chain-rule-diff-both"; (<<<<<<<=================================)
neuper@52113	1384	(*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =
neuper@52113	1385	d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *)
neuper@52113	1386	val ((pt,pos),_) = get_calc 1;
neuper@52113	1387	val p = get_pos 1 1;
neuper@52113	1388
neuper@52113	1389	val (Form f, _, asms) = pt_extract (pt, p);
neuper@52113	1390	if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
neuper@52113	1391	get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sum", "Diff.diff_sum"(?!?)))
neuper@52113	1392	then ()
neuper@52113	1393	else error "embed fun get_fillform changed 2";
neuper@52113	1394
neuper@52113	1395	(* if we assume, that the fill-patterns are ordered such that the 1st has large gaps
neuper@52113	1396	and the last has no gaps, then the number of fill-patterns would suffice
neuper@52113	1397	for the DialogGuide to select appropriately. *)
neuper@52113	1398	requestFillformula 1 ("chain-rule-diff-both", "fill-both-args");(<<<<<<<============)
neuper@52113	1399	(<AUTOCALC> ([1], Res) ([2], Res) ([2], Res) </AUTOCALC>)
neuper@52113	1400	val ((pt,pos),_) = get_calc 1;
neuper@52113	1401	val p = get_pos 1 1;
neuper@52113	1402	val (Form f, _, asms) = pt_extract (pt, p);
neuper@52113	1403	if p = ([1], Res) andalso existpt [2] pt andalso
neuper@52113	1404	term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
neuper@52113	1405	get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sum", "Diff.diff_sum"))
neuper@52113	1406	then () else error "embed fun get_fillform changed 3";
neuper@52113	1407
neuper@52113	1408	inputFillFormula 1 "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)";(<<<<<<<=====)
neuper@52113	1409	val ((pt, _),_) = get_calc 1;
neuper@52113	1410	val p = get_pos 1 1;
neuper@52113	1411	val (Form f, _, asms) = pt_extract (pt, p);
neuper@52113	1412	if p = ([2], Res) andalso
neuper@52113	1413	term2str f = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)" andalso
neuper@52113	1414	get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", ""))
neuper@52113	1415	then () else error "inputFillFormula changed 11";
neuper@52113	1416
wneuper@59248	1417	autoCalculate 1 CompleteCalc;
neuper@52113	1418
neuper@52113	1419	"~~~~~ final check: the input formula is inserted as it would have been correct from beginning";
neuper@52113	1420	val ((pt, _),_) = get_calc 1;
neuper@52113	1421	val p = get_pos 1 1;
neuper@52113	1422	val (Form f, _, asms) = pt_extract (pt, p);
neuper@52113	1423	if p = ([], Res) andalso term2str f = "2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3"
neuper@52113	1424	then () else error "inputFillFormula changed 12";
neuper@52113	1425	show_pt pt;
neuper@52113	1426	(*[
neuper@52113	1427	(([], Frm), Diff (x ^^^ 2 + sin (x ^^^ 4), x)),
neuper@52113	1428	(([1], Frm), d_d x (x ^^^ 2 + sin (x ^^^ 4))),
neuper@52113	1429	(([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))),
neuper@52113	1430	(([2], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)), (<<<<<<<=====)
neuper@52113	1431	(([3], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * (4 * x ^^^ (4 - 1))),
neuper@52113	1432	(([4], Res), 2 * x ^^^ (2 - 1) + cos (x ^^^ 4) * (4 * x ^^^ (4 - 1))),
neuper@52113	1433	(([5], Res), 2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3),
neuper@52113	1434	(([], Res), 2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3)] *)
neuper@52113	1435	============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*)
neuper@52113	1436
neuper@52113	1437	"--------- UC errpat add-fraction, fillpat by input --------------";
neuper@52113	1438	"--------- UC errpat add-fraction, fillpat by input --------------";
neuper@52113	1439	"--------- UC errpat add-fraction, fillpat by input --------------";
neuper@52113	1440	(cp from BridgeLog Java <=> SML)
s1210629013@55445	1441	reset_states ();
neuper@52113	1442	CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
neuper@52113	1443	Iterator 1;
neuper@52113	1444	moveActiveRoot 1;
neuper@52113	1445	moveActiveFormula 1 ([],Pbl);
neuper@52113	1446	replaceFormula 1 "Simplify (5 * x / (4 * y) + 3 * x / (4 * y))";
wneuper@59248	1447	autoCalculate 1 CompleteCalcHead;
wneuper@59248	1448	autoCalculate 1 (Step 1);
wneuper@59123	1449	appendFormula 1 "8 * x / (8 * y)" (\|> Future.join);
neuper@52113	1450	(*<CALCMESSAGE> no derivation found </CALCMESSAGE>
neuper@52113	1451	--- but in BridgeLog Java <=> SML:
neuper@52113	1452	<CALCMESSAGE> error pattern #addition-of-fractions# </CALCMESSAGE>*)
neuper@52113	1453
neuper@52113	1454	"--------- UC errpat, fillpat step to Rewrite --------------------";
neuper@52113	1455	"--------- UC errpat, fillpat step to Rewrite --------------------";
neuper@52113	1456	"--------- UC errpat, fillpat step to Rewrite --------------------";
neuper@52113	1457	(TODO)
s1210629013@55445	1458	reset_states ();
neuper@52113	1459	CalcTree
neuper@52113	1460	[(["functionTerm ((x ^ 2) ^ 3 + sin (x ^ 4))",
neuper@52113	1461	"differentiateFor x", "derivative f_f'"],
neuper@52113	1462	("Isac", ["derivative_of","function"],
neuper@52113	1463	["diff","differentiate_on_R"]))]; (<<<======= EP is directly in script)
neuper@52113	1464	Iterator 1;
neuper@52113	1465	moveActiveRoot 1;
wneuper@59248	1466	autoCalculate 1 CompleteCalc;
neuper@52113	1467	val ((pt,p),_) = get_calc 1; show_pt pt;
neuper@52113	1468
neuper@52113	1469	"--------- UC errpat, fillpat step to Rewrite_Set ----------------";
neuper@52113	1470	"--------- UC errpat, fillpat step to Rewrite_Set ----------------";
neuper@52113	1471	"--------- UC errpat, fillpat step to Rewrite_Set ----------------";
s1210629013@55445	1472	reset_states ();
neuper@52113	1473	CalcTree
neuper@52113	1474	[(["functionTerm ((x ^ 2) ^ 3 + sin (x ^ 4))",
neuper@52113	1475	"differentiateFor x", "derivative f_f'"],
neuper@52113	1476	("Isac", ["derivative_of","function"],
neuper@52113	1477	["diff","after_simplification"]))]; (<<<======= EP is in a ruleset)
neuper@52113	1478	Iterator 1;
neuper@52113	1479	moveActiveRoot 1;
wneuper@59248	1480	autoCalculate 1 CompleteCalcHead;
wneuper@59248	1481	autoCalculate 1 (Step 1); fetchProposedTactic 1;
wneuper@59248	1482	autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@52113	1483	(*
neuper@52113	1484	<NEXTTAC>
neuper@52113	1485	<CALCID> 1 </CALCID>
neuper@52113	1486	<TACTICERRORPATTERNS>
neuper@52113	1487	<STRINGLIST>
neuper@52113	1488	<STRING> chain-rule-diff-both </STRING>
neuper@52113	1489	<STRING> cancel </STRING>
neuper@52113	1490	</STRINGLIST>
neuper@52113	1491	<REWRITESETINSTTACTIC name="Rewrite_Set_Inst">
neuper@52113	1492	<RULESET> norm_diff </RULESET>
neuper@52113	1493	<SUBSTITUTION>
neuper@52113	1494	<PAIR>
neuper@52113	1495	<VARIABLE>
neuper@52113	1496	<MATHML>
neuper@52113	1497	<ISA> bdv </ISA>
neuper@52113	1498	</MATHML>
neuper@52113	1499	</VARIABLE>
neuper@52113	1500	<VALUE>
neuper@52113	1501	<MATHML>
neuper@52113	1502	<ISA> x </ISA>
neuper@52113	1503	</MATHML>
neuper@52113	1504	</VALUE>
neuper@52113	1505	</PAIR>
neuper@52113	1506	</SUBSTITUTION>
neuper@52113	1507	</REWRITESETINSTTACTIC>
neuper@52113	1508	</TACTICERRORPATTERNS>
neuper@52113	1509	</NEXTTAC>
neuper@52113	1510
neuper@52113	1511
neuper@52113	1512	(WN1208 postponed due to efforts required for stepToErrorPatterns (NEW rewrite_set_))
neuper@52113	1513	stepToErrorPatterns 1; (--> calcChanged, rule immediately calls... )
neuper@52113	1514	stepOnErrorPatterns 1; (--> calcChanged, rule calls getTactic and displays it )
neuper@52113	1515	(* then --- UC errpat, fillpat by input ---*)
neuper@52113	1516	*)
wneuper@59248	1517	autoCalculate 1 CompleteCalc;
neuper@52113	1518	val ((pt,p),_) = get_calc 1; show_pt pt;
neuper@52113	1519	(WN1208 postponed due to efforts required for stepToErrorPatterns (NEW rewrite_set_))
neuper@52113	1520

author	Walther Neuper <wneuper@ist.tugraz.at>
	Tue, 18 Oct 2016 12:05:03 +0200
changeset 59252	7d3dbc1171ff
parent 59248	5eba5e6d5266
child 59253	f0bb15a046ae
permissions	-rw-r--r--