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

author	Walther Neuper <wneuper@ist.tugraz.at>
	Thu, 22 Dec 2016 11:36:20 +0100
changeset 59279	255c853ea2f0
parent 59254	0d84c462dd7e
child 59283	96c2da5217f8
permissions	-rw-r--r--