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

author	Mathias Lehnfeld <s1210629013@students.fh-hagenberg.at>
	Fri, 13 Jun 2014 12:42:15 +0200
changeset 55446	42c45d1241d7
parent 55445	33b0f6db720c
child 55480	1738bef7d5d3
permissions	-rw-r--r--