walther@59820
|
1 |
(* Title: tests for MathEngine/mathengine-stateless.sml
|
walther@59820
|
2 |
Author: Walther Neuper 2000, 2006, 2020
|
neuper@37906
|
3 |
(c) due to copyright terms
|
neuper@55460
|
4 |
|
neuper@55460
|
5 |
theory Test_Some imports Build_Thydata begin
|
neuper@55460
|
6 |
ML {* KEStore_Elems.set_ref_thy @{theory};
|
neuper@55460
|
7 |
fun autoCalculate' cI auto = autoCalculate cI auto |> Future.join *}
|
neuper@55460
|
8 |
ML_file "~~/test/Tools/isac/Interpret/mathengine.sml"
|
neuper@37906
|
9 |
*)
|
neuper@38065
|
10 |
"--------------------------------------------------------";
|
neuper@38065
|
11 |
"table of contents --------------------------------------";
|
neuper@38065
|
12 |
"--------------------------------------------------------";
|
neuper@41940
|
13 |
"----------- change to parse ctxt -----------------------";
|
neuper@38065
|
14 |
"----------- debugging setContext..pbl_ -----------------";
|
neuper@38065
|
15 |
"----------- tryrefine ----------------------------------";
|
t@42225
|
16 |
"----------- search for Or_to_List ----------------------";
|
neuper@42279
|
17 |
"----------- check thy in CalcTreeTEST ------------------";
|
walther@59875
|
18 |
"----------- identified error in fun getTactic, ThmC.string_of_thm ---------------";
|
neuper@55486
|
19 |
"----------- improved fun getTactic for interSteps and numeral calculations --";
|
neuper@38065
|
20 |
"--------------------------------------------------------";
|
neuper@38065
|
21 |
"--------------------------------------------------------";
|
neuper@38065
|
22 |
"--------------------------------------------------------";
|
neuper@37906
|
23 |
|
neuper@41940
|
24 |
"----------- change to parse ctxt -----------------------";
|
neuper@41940
|
25 |
"----------- change to parse ctxt -----------------------";
|
neuper@41940
|
26 |
"----------- change to parse ctxt -----------------------";
|
neuper@41940
|
27 |
"===== start calculation: from problem description (fmz) to origin";
|
neuper@41940
|
28 |
val fmz = ["realTestGiven (((1+2)*4/3)^^^2)","realTestFind s"];
|
neuper@41940
|
29 |
val (thyID, pblID, metID) =
|
neuper@41940
|
30 |
("Test", ["calculate", "test"], ["Test", "test_calculate"]);
|
walther@59679
|
31 |
(*======= Isabelle2013-2 --> Isabelle2014: unclear, why this test ever run =====================*)
|
neuper@37906
|
32 |
|
neuper@38065
|
33 |
"----------- debugging setContext..pbl_ -----------------";
|
neuper@38065
|
34 |
"----------- debugging setContext..pbl_ -----------------";
|
neuper@38065
|
35 |
"----------- debugging setContext..pbl_ -----------------";
|
s1210629013@55445
|
36 |
reset_states ();
|
neuper@41970
|
37 |
CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
|
neuper@41970
|
38 |
("Test", ["sqroot-test","univariate","equation","test"],
|
neuper@37906
|
39 |
["Test","squ-equ-test-subpbl1"]))];
|
neuper@37906
|
40 |
Iterator 1;
|
neuper@37906
|
41 |
moveActiveRoot 1; modelProblem 1;
|
neuper@37906
|
42 |
|
neuper@37906
|
43 |
val pos as (p,_) = ([],Pbl);
|
neuper@37906
|
44 |
val guh = "pbl_equ_univ";
|
neuper@37906
|
45 |
checkContext 1 pos guh;
|
neuper@37906
|
46 |
val ((pt,_),_) = get_calc 1;
|
neuper@37906
|
47 |
val pp = par_pblobj pt p;
|
neuper@37906
|
48 |
val keID = guh2kestoreID guh;
|
wneuper@59529
|
49 |
case context_pbl keID pt pp of (true,["univariate","equation"],_,_,_)=>()
|
neuper@38031
|
50 |
| _ => error "mathengine.sml: context_pbl .. pbl_equ_univ checked";
|
neuper@37906
|
51 |
|
walther@59903
|
52 |
case get_obj g_spec pt p of (_, ["empty_probl_id"], _) => ()
|
neuper@38031
|
53 |
| _ => error "mathengine.sml: context_pbl .. pbl still empty";
|
neuper@37906
|
54 |
setContext 1 pos guh;
|
neuper@37906
|
55 |
val ((pt,_),_) = get_calc 1;
|
wneuper@59529
|
56 |
case get_obj g_spec pt p of (_, ["univariate","equation"], _) => ()
|
neuper@38031
|
57 |
| _ => error "mathengine.sml: context_pbl .. pbl set";
|
neuper@37906
|
58 |
|
neuper@37906
|
59 |
|
neuper@37906
|
60 |
setContext 1 pos "met_eq_lin";
|
neuper@37906
|
61 |
val ((pt,_),_) = get_calc 1;
|
neuper@37906
|
62 |
case get_obj g_spec pt p of (_, _, ["LinEq", "solve_lineq_equation"]) => ()
|
neuper@38031
|
63 |
| _ => error "mathengine.sml: context_pbl .. pbl set";
|
neuper@37906
|
64 |
|
neuper@37906
|
65 |
|
neuper@38065
|
66 |
"----------- tryrefine ----------------------------------";
|
neuper@38065
|
67 |
"----------- tryrefine ----------------------------------";
|
neuper@38065
|
68 |
"----------- tryrefine ----------------------------------";
|
s1210629013@55445
|
69 |
reset_states ();
|
neuper@37906
|
70 |
CalcTree [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
|
neuper@37906
|
71 |
"solveFor x", "solutions L"],
|
neuper@38058
|
72 |
("RatEq",["univariate","equation"],["no_met"]))];
|
neuper@37906
|
73 |
Iterator 1;
|
wneuper@59248
|
74 |
moveActiveRoot 1; autoCalculate 1 CompleteCalc;
|
neuper@37906
|
75 |
|
neuper@37906
|
76 |
refineProblem 1 ([1],Res) "pbl_equ_univ"
|
neuper@37906
|
77 |
(*gives "pbl_equ_univ_rat" correct*);
|
neuper@37906
|
78 |
|
neuper@55279
|
79 |
refineProblem 1 ([1],Res) (pblID2guh ["LINEAR","univariate","equation"])
|
neuper@38065
|
80 |
(*gives "pbl_equ_univ_lin" incorrect*);
|
neuper@38065
|
81 |
|
neuper@42394
|
82 |
"--------- search for Or_to_List ------------------------";
|
neuper@42394
|
83 |
"--------- search for Or_to_List ------------------------";
|
t@42225
|
84 |
"--------- search for Or_to_List ------------------------";
|
t@42225
|
85 |
val fmz = ["equality (x^^^2 + 4*x + 5 = (2::real))", "solveFor x","solutions L"];
|
wneuper@59592
|
86 |
val (dI',pI',mI') = ("Isac_Knowledge", ["univariate","equation"], ["no_met"])
|
t@42225
|
87 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
t@42225
|
88 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
89 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
90 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
91 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
92 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
93 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
94 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
95 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
96 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
97 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Subproblem"*)
|
t@42225
|
98 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
99 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
100 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
101 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
102 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
103 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
104 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
105 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
106 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
107 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59749
|
108 |
"~~~~~ fun me, args:"; val (tac, (p:pos'), (_:NEW(*remove*)), (pt:ctree)) =
|
t@42225
|
109 |
(nxt, p, [], pt);
|
walther@59804
|
110 |
val ("ok", (_, _, ptp)) = Step.by_tactic tac (pt,p)
|
t@42225
|
111 |
val (pt, p) = ptp;
|
walther@59765
|
112 |
"~~~~~ fun Step.do_next, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =
|
t@42225
|
113 |
(p, ((pt, e_pos'),[]));
|
t@42225
|
114 |
val pIopt = get_pblID (pt,ip);
|
t@42225
|
115 |
ip = ([],Res); (*false*)
|
t@42225
|
116 |
ip = p; (*false*)
|
walther@59914
|
117 |
Library.member op = [Pbl,Met] p_; (*false*)
|
walther@59760
|
118 |
"~~~~~ fun do_next, args:"; val (ptp as (pt, pos as (p,p_))) = (pt,ip);
|
walther@59903
|
119 |
Method.id_empty = get_obj g_metID pt (par_pblobj pt p); (*false*)
|
t@42225
|
120 |
val thy' = get_obj g_domID pt (par_pblobj pt p);
|
walther@59831
|
121 |
val ((ist, ctxt), sc) = resume_prog thy' (p,p_) pt;
|
walther@59841
|
122 |
|
walther@59791
|
123 |
val Next_Step (istate, ctxt, tac) = LI.find_next_step sc (pt,pos) ist ctxt; (*WAS Empty_Tac_: tac_*)
|
walther@59734
|
124 |
case tac of Or_to_List' _ => ()
|
t@42225
|
125 |
| _ => error "Or_to_List broken ?"
|
akargl@42108
|
126 |
|
neuper@42394
|
127 |
|
neuper@42279
|
128 |
"----------- check thy in CalcTreeTEST ------------------";
|
neuper@42279
|
129 |
"----------- check thy in CalcTreeTEST ------------------";
|
neuper@42279
|
130 |
"----------- check thy in CalcTreeTEST ------------------";
|
neuper@42279
|
131 |
"WN1109 with Inverse_Z_Transform.thy when starting tests with CalcTreeTEST \n" ^
|
neuper@42279
|
132 |
"we got the message: ME_Isa: thy 'Build_Inverse_Z_Transform' not in system \n" ^
|
neuper@42279
|
133 |
"Below there are the steps which found out the reason: \n" ^
|
neuper@42279
|
134 |
"store_pbt mistakenly stored that theory.";
|
wneuper@59592
|
135 |
val ctxt = Proof_Context.init_global @{theory Isac_Knowledge};
|
neuper@42279
|
136 |
val SOME t = parseNEW ctxt "filterExpression (X = 3 / (z - 1/4 + -1/8 * (1/(z::real))))";
|
neuper@42279
|
137 |
val SOME t = parseNEW ctxt "stepResponse (x[n::real]::bool)";
|
akargl@42108
|
138 |
|
wneuper@59550
|
139 |
val fmz = ["filterExpression (X = 3 / (z - 1/4 + -1/8 * (1/(z::real))))", "boundVariable z",
|
neuper@42279
|
140 |
"stepResponse (x[n::real]::bool)"];
|
wneuper@59592
|
141 |
val (dI,pI,mI) = ("Isac_Knowledge", ["Inverse", "Z_Transform", "SignalProcessing"],
|
neuper@42405
|
142 |
["SignalProcessing","Z_Transform","Inverse"]);
|
neuper@42279
|
143 |
|
neuper@42279
|
144 |
val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))];
|
neuper@42279
|
145 |
(*WAS ME_Isa: thy 'Build_Inverse_Z_Transform' not in system*)
|
neuper@42279
|
146 |
|
walther@59941
|
147 |
"~~~~~ T fun CalcTreeTEST, args:"; val [(fmz, sp):Formalise.T] = [(fmz, (dI,pI,mI))];
|
neuper@42279
|
148 |
"~~~~~ fun nxt_specify_init_calc, args:"; val (fmz, (dI, pI, mI)) = (fmz, sp);
|
walther@59881
|
149 |
val thy = ThyC.get_theory dI;
|
neuper@42279
|
150 |
mI = ["no_met"]; (*false*)
|
walther@59947
|
151 |
val (pI, (pors, pctxt), mI) = (pI, get_pbt pI |> #ppc |> O_Model.prep_ori fmz thy, mI)
|
neuper@42279
|
152 |
val {cas, ppc, thy=thy',...} = get_pbt pI; (*take dI from _refined_ pbl*)
|
neuper@42279
|
153 |
"tracing bottom up"; Context.theory_name thy' = "Build_Inverse_Z_Transform"; (*WAS true*)
|
walther@59918
|
154 |
val dI = Context.theory_name (ThyC.parent_of thy thy');
|
neuper@42279
|
155 |
"tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*)
|
neuper@42279
|
156 |
cas = NONE; (*true*)
|
neuper@42279
|
157 |
val hdl = pblterm dI pI;
|
walther@59846
|
158 |
val (pt, _) = cappend_problem e_ctree [] (Istate.empty, pctxt) (fmz, (dI, pI, mI))
|
walther@59846
|
159 |
(pors, (dI, pI, mI), hdl, ContextC.empty)
|
walther@59821
|
160 |
;
|
walther@59806
|
161 |
"~~~~~ fun Step_Specify.by_tactic_input, args:"; val ((tac as Model_Problem), (pt, pos as (p,p_))) = (Model_Problem, (pt, ([], Pbl)));
|
neuper@42279
|
162 |
val PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} = get_obj I pt p;
|
neuper@42279
|
163 |
"tracing bottom up"; #1(ospec) = "Build_Inverse_Z_Transform"; (*WAS true*)
|
neuper@42279
|
164 |
|
neuper@42279
|
165 |
"~~~~~ fun some_spec, args:"; val ((odI, opI, omI), (dI, pI, mI)) = (ospec, spec);
|
walther@59879
|
166 |
dI = ThyC.id_empty; (*true*)
|
neuper@42279
|
167 |
odI = "Build_Inverse_Z_Transform"; (*true*)
|
walther@59903
|
168 |
dI = "empty_thy_id"; (*true*)
|
neuper@42279
|
169 |
"~~~~~ after fun some_spec:";
|
neuper@42279
|
170 |
val (dI, pI, mI) = some_spec ospec spec;
|
neuper@42279
|
171 |
"tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*)
|
walther@59881
|
172 |
val thy = ThyC.get_theory dI; (*caused ME_Isa: thy 'Build_Inverse_Z_Transform' not in system*)
|
neuper@42279
|
173 |
|
walther@59875
|
174 |
"----------- identified error in fun getTactic, ThmC.string_of_thm ---------------";
|
walther@59875
|
175 |
"----------- identified error in fun getTactic, ThmC.string_of_thm ---------------";
|
walther@59875
|
176 |
"----------- identified error in fun getTactic, ThmC.string_of_thm ---------------";
|
neuper@55482
|
177 |
reset_states ();
|
neuper@55482
|
178 |
CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
|
neuper@55482
|
179 |
("Test",["sqroot-test","univariate","equation","test"],["Test","squ-equ-test-subpbl1"]))];
|
neuper@55482
|
180 |
moveActiveRoot 1;
|
wneuper@59248
|
181 |
autoCalculate 1 CompleteCalcHead;
|
walther@59747
|
182 |
autoCalculate 1 (Steps 1);
|
walther@59747
|
183 |
autoCalculate 1 (Steps 1);
|
walther@59747
|
184 |
autoCalculate 1 (Steps 1);
|
neuper@55482
|
185 |
getTactic 1 ([1],Frm); (*<RULESET> norm_equation </RULESET>*)
|
neuper@55482
|
186 |
interSteps 1 ([1],Res);
|
neuper@55482
|
187 |
"~~~~~ fun interSteps, args:"; val (cI, ip) = (1, ([1],Res));
|
neuper@55482
|
188 |
val ((pt,p), tacis) = get_calc cI;
|
neuper@55482
|
189 |
(not o is_interpos) ip = false;
|
neuper@55482
|
190 |
val ip' = lev_pred' pt ip;
|
walther@59833
|
191 |
"~~~~~ fun go, args:"; val (pt, (pos as (p,p_):pos')) = (pt, ip);
|
neuper@55482
|
192 |
(* ^^^^^^^^^ not in test/../ *)
|
neuper@55482
|
193 |
val nd = get_nd pt p
|
neuper@55482
|
194 |
val cn = children nd;
|
neuper@55482
|
195 |
null cn = false;
|
neuper@55482
|
196 |
(is_rewset o (get_obj g_tac nd)) [(*root of nd*)] = true;
|
neuper@55482
|
197 |
"~~~~~ fun detailrls, args:"; val (pt, (pos as (p,p_):pos')) = (pt, pos);
|
neuper@55482
|
198 |
(* ^^^^^^^^^ only once in test/../solve.sml*)
|
neuper@55482
|
199 |
val t = get_obj g_form pt p
|
neuper@55482
|
200 |
val tac = get_obj g_tac pt p
|
neuper@55482
|
201 |
val rls = (assoc_rls o rls_of) tac
|
neuper@55482
|
202 |
val ctxt = get_ctxt pt pos
|
walther@59851
|
203 |
(*rls = Rule_Set.Repeat {calc = [], erls = ...*)
|
walther@59935
|
204 |
val is = Istate.init_detail tac t
|
wneuper@59583
|
205 |
(*TODO.WN060602 Pstate (["(t_, Problem (Isac,[equation,univar]))"]
|
neuper@55482
|
206 |
is wrong for simpl, but working ?!? *)
|
walther@59932
|
207 |
val tac_ = Apply_Method' (Method.id_empty(*WN0402: see Step.add !?!*), SOME t, is, ctxt)
|
neuper@55482
|
208 |
val pos' = ((lev_on o lev_dn) p, Frm)
|
walther@59881
|
209 |
val thy = ThyC.get_theory "Isac_Knowledge"
|
walther@59932
|
210 |
val (_,_,_,pt') = (*implicit Take*)Step.add tac_ (is, ctxt) (pt, pos');
|
neuper@55482
|
211 |
(*val (_,_,(pt'',_)) = *)complete_solve CompleteSubpbl [] (pt',pos');
|
neuper@55482
|
212 |
(* ^^^^^^^^^^^^^^ in test/../mathengine.sml*)
|
neuper@55482
|
213 |
(* in pt'': tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
|
neuper@55482
|
214 |
^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
|
walther@59672
|
215 |
"~~~~~ fun complete_solve , args:"; val (auto, c, (ptp as (_, p as (_,p_)): ctree * pos')) =
|
neuper@55482
|
216 |
(CompleteSubpbl, [], (pt',pos'));
|
neuper@55482
|
217 |
p = ([], Res) = false;
|
walther@59914
|
218 |
Library.member op = [Pbl,Met] p_ = false;
|
walther@59762
|
219 |
val (_, (_, c', ptp')) = Step_Solve.do_next ptp;
|
neuper@55482
|
220 |
(* in pt': tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
|
neuper@55482
|
221 |
^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
|
walther@59760
|
222 |
"~~~~~ fun do_next , args:"; val ((ptp as (pt, pos as (p,p_)))) = (ptp);
|
walther@59903
|
223 |
Method.id_empty = get_obj g_metID pt (par_pblobj pt p) = false;
|
neuper@55482
|
224 |
val thy' = get_obj g_domID pt (par_pblobj pt p);
|
walther@59831
|
225 |
val ((ist, ctxt), sc) = resume_prog thy' (p,p_) pt;
|
walther@59791
|
226 |
val Next_Step (is, ctxt, tac_) = LI.find_next_step sc (pt,pos) ist ctxt;
|
neuper@55482
|
227 |
(*tac_ = Rewrite' (..., ("rnorm_equation_add", "Test.rnorm_equation_add"), ...) !!!!!!!!!!!!!!!!*)
|
walther@59680
|
228 |
|
walther@59680
|
229 |
(*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* )
|
walther@59772
|
230 |
"~~~~~ fun find_next_step , args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'),
|
walther@59676
|
231 |
(sc as Prog (h $ body)), (Pstate (ist as (E,l,rls,a,v,s,b)), ctxt)) = ((thy',srls), (pt,pos), sc, is);
|
neuper@55482
|
232 |
l = [] = false;
|
walther@59784
|
233 |
go_scan_up thy ptp sc ist true (*--> Accept_Tac (Rewrite' (.., (.., "Test.rnorm_equation_add"), ...)
|
walther@59772
|
234 |
BUT WE FIND IN THE CODE ABOVE IN find_next_step:*)
|
neuper@55482
|
235 |
;
|
neuper@55482
|
236 |
(*----------------------------------------------------------------------------------------------*)
|
walther@59875
|
237 |
if ThmC.string_of_thm @{thm rnorm_equation_add} = "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a + - 1 * ?b = 0)"
|
walther@59875
|
238 |
then () else error "ThmC.string_of_thm changed";
|
walther@59875
|
239 |
if ThmC.string_of_thm @{thm rnorm_equation_add} = "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a + - 1 * ?b = 0)"
|
neuper@55482
|
240 |
then () else error "string_of_thm changed";
|
neuper@55482
|
241 |
(*----------------------------------------------------------------------------------------------*)
|
neuper@55482
|
242 |
;
|
neuper@55482
|
243 |
(*SEARCH FOR THE ERROR WENT DOWN TO THE END OF THIS TEST, AND THEN UP TO HERE AGAIN*)
|
wneuper@59562
|
244 |
"~~~~~ fun begin_end_prog, args:"; val (tac_, is, (pt, pos as (p,p_))) = (tac_, is, ptp);
|
neuper@55482
|
245 |
val pos =
|
neuper@55482
|
246 |
case pos of
|
neuper@55482
|
247 |
(p, Met) => ((lev_on o lev_dn) p, Frm)(*begin script*)
|
neuper@55482
|
248 |
| (p, Res) => (lev_on p,Res) (*somewhere in script*)
|
neuper@55482
|
249 |
| _ => pos;
|
walther@59932
|
250 |
Step.add tac_ is pos pt;
|
neuper@55482
|
251 |
(* tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
|
neuper@55482
|
252 |
^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
|
walther@59932
|
253 |
"~~~~~ fun add, args:"; val (thy, (Rewrite' (thy',ord',rls',pa,thm',f,(f',asm))),
|
walther@59881
|
254 |
(is, ctxt), (p,p_), pt) = ((ThyC.get_theory "Isac_Knowledge"), tac_, is, pos, pt);
|
walther@59728
|
255 |
val (pt,c) = cappend_atomic pt p (is, ContextC.insert_assumptions asm ctxt) f
|
wneuper@59253
|
256 |
(Rewrite thm') (f',asm) Complete;
|
neuper@55482
|
257 |
(* in pt: tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
|
neuper@55482
|
258 |
^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
|
neuper@55482
|
259 |
"~~~~~ fun cappend_atomic, args:"; val (pt, p, ist_res, f, r, f', s) =
|
walther@59728
|
260 |
(pt, p, (is, ContextC.insert_assumptions asm ctxt), f, (Rewrite thm'), (f',asm), Complete);
|
walther@59844
|
261 |
existpt p pt andalso Tactic.is_empty (get_obj g_tac pt p) = false;
|
neuper@55482
|
262 |
apfst (append_atomic p ist_res f r f' s) (cut_tree pt (p,Frm));
|
neuper@55482
|
263 |
apfst : ('a -> 'b) -> 'a * 'c -> 'b * 'c;
|
wneuper@59279
|
264 |
(append_atomic p ist_res f r f' s) : ctree -> ctree;
|
neuper@55482
|
265 |
;
|
neuper@55482
|
266 |
(* HERE THE ERROR OCCURED IN THE FIRST APPROACH
|
neuper@55482
|
267 |
getTactic 1 ([1,1],Frm); <ERROR> syserror in getTactic </ERROR> <<<<<=========================*)
|
neuper@55482
|
268 |
"~~~~~ fun getTactic, args:"; val (cI, (p:pos')) = (1, ([1,1],Frm));
|
neuper@55482
|
269 |
val ((pt,_),_) = get_calc cI
|
neuper@55482
|
270 |
val (form, tac, asms) = pt_extract (pt, p)
|
neuper@55482
|
271 |
val SOME ta = tac;
|
neuper@55482
|
272 |
"~~~~~ fun gettacticOK2xml, args:"; val ((cI:calcID), tac) = (cI, ta);
|
wneuper@59262
|
273 |
val i = 2;
|
neuper@55482
|
274 |
"~~~~~ fun tac2xml, args:"; val (j, (Rewrite thm')) = (i, tac);
|
wneuper@59252
|
275 |
"~~~~~ fun thm'2xml, args:"; val (j, ((ID, form) : thm'')) = ((j+i), thm');
|
neuper@55482
|
276 |
ID = "rnorm_equation_add";
|
neuper@55482
|
277 |
@{thm rnorm_equation_add};
|
walther@59868
|
278 |
(UnparseC.term o Thm.prop_of) form = "~ ?b =!= 0 ==> (?a = ?b) = (?a + -1 * ?b = 0)"
|
neuper@55482
|
279 |
(*?!? should be "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a + -1 * ?b = 0)"*)
|
neuper@55482
|
280 |
(*thmstr2xml (j+i) form;
|
neuper@55482
|
281 |
ERROR Undeclared constant: "Test.rnorm_equation_add" ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
|
neuper@55482
|
282 |
;
|
neuper@55482
|
283 |
show_pt pt;
|
neuper@55482
|
284 |
(*[
|
neuper@55482
|
285 |
(([], Frm), solve (x + 1 = 2, x)),
|
neuper@55482
|
286 |
(([1], Frm), x + 1 = 2),
|
neuper@55482
|
287 |
(([1,1], Frm), x + 1 = 2),
|
neuper@55482
|
288 |
(([1,1], Res), x + 1 + -1 * 2 = 0),
|
neuper@55482
|
289 |
(([1], Res), x + 1 + -1 * 2 = 0),
|
neuper@55482
|
290 |
(([2], Res), -1 + x = 0)]
|
neuper@55482
|
291 |
|
neuper@55482
|
292 |
pt; --> tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")*)
|
walther@59679
|
293 |
( *----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------//*)
|
neuper@55482
|
294 |
|
neuper@55486
|
295 |
"----------- improved fun getTactic for interSteps and numeral calculations --";
|
neuper@55486
|
296 |
"----------- improved fun getTactic for interSteps and numeral calculations --";
|
neuper@55486
|
297 |
"----------- improved fun getTactic for interSteps and numeral calculations --";
|
neuper@55486
|
298 |
reset_states (); val cI = 1;
|
neuper@55486
|
299 |
CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
|
neuper@55486
|
300 |
("Test",["sqroot-test","univariate","equation","test"],["Test","squ-equ-test-subpbl1"]))];
|
neuper@55486
|
301 |
moveActiveRoot 1;
|
wneuper@59248
|
302 |
autoCalculate 1 CompleteCalcHead;
|
walther@59747
|
303 |
autoCalculate 1 (Steps 1);
|
neuper@55486
|
304 |
|
neuper@55486
|
305 |
val cs = get_calc cI (* we improve from the calcstate here [*] *);
|
neuper@55486
|
306 |
val pos as (_,p_) = get_pos cI 1 (* we improve from the calcstate here [*] *);
|
neuper@55486
|
307 |
|
wneuper@59123
|
308 |
appendFormula 1 "x + 4 + -3 = 2" (*|> Future.join*);
|
neuper@55486
|
309 |
interSteps 1 ([1],Res); (* already done by appendFormula, now showed to frontend *)
|
neuper@55486
|
310 |
getTactic 1 ([1,1], Res);
|
neuper@55486
|
311 |
(*<ID> sym_#add_Float ((~3,0), (0,0)) __ ((4,0), (0,0)) </ID> <<<<<================== to improve
|
neuper@55486
|
312 |
<ISA> 1 + x = -3 + (4 + x) </ISA>*)
|
neuper@55486
|
313 |
|
neuper@55486
|
314 |
val ((pt''',p'''), tacis''') = get_calc cI;
|
neuper@55486
|
315 |
show_pt pt'''
|
neuper@55486
|
316 |
(*[
|
neuper@55486
|
317 |
(([], Frm), solve (x + 1 = 2, x)),
|
neuper@55486
|
318 |
(([1], Frm), x + 1 = 2),
|
neuper@55486
|
319 |
(([1,1], Frm), x + 1 = 2),
|
neuper@55486
|
320 |
(([1,1], Res), 1 + x = 2),
|
neuper@55486
|
321 |
(([1,2], Res), -3 + (4 + x) = 2),
|
neuper@55486
|
322 |
(([1,3], Res), -3 + (x + 4) = 2),
|
neuper@55486
|
323 |
(([1,4], Res), x + 4 + -3 = 2),
|
neuper@55486
|
324 |
(([1], Res), x + 4 + -3 = 2)]*)
|
neuper@55486
|
325 |
;
|
neuper@55486
|
326 |
"~~~~~ fun appendFormula', args:"; val (cI, ifo) = (1, "x + 4 + -3 = 2");
|
neuper@55486
|
327 |
(* val cs = get_calc cI (* we improve from the calcstate here [*] *);
|
neuper@55486
|
328 |
val pos as (_,p_) = get_pos cI 1 (* we improve from the calcstate here [*] *);*)
|
walther@59798
|
329 |
val ("ok", cs' as (_, _, ptp')) = Step.do_next pos cs;
|
walther@59798
|
330 |
(*val ("ok", (_, c, ptp as (_,p))) = *)Step_Solve.by_term ptp' (encode ifo);
|
walther@59797
|
331 |
"~~~~~ fun Step_Solve.by_term , args:"; val (cs as (_, _, ptp as (pt, pos as (p, p_))), istr) =
|
neuper@55486
|
332 |
(cs', (encode ifo));
|
walther@59881
|
333 |
val SOME f_in = parse (ThyC.get_theory "Isac_Knowledge") istr
|
wneuper@59188
|
334 |
val f_in = Thm.term_of f_in
|
neuper@55486
|
335 |
val f_succ = get_curr_formula (pt, pos);
|
neuper@55486
|
336 |
f_succ = f_in = false;
|
neuper@55486
|
337 |
val NONE = cas_input f_in
|
neuper@55486
|
338 |
val pos_pred = lev_back' pos
|
neuper@55486
|
339 |
(* f_pred ---"step pos cs"---> f_succ in appendFormula *)
|
neuper@55486
|
340 |
val f_pred = get_curr_formula (pt, pos_pred);
|
neuper@55486
|
341 |
(*val msg_calcstate' = *)compare_step ([], [], (pt, pos_pred)) f_in (*<<=====*);
|
neuper@55486
|
342 |
"~~~~~ fun compare_step, args:"; val (((tacis, c, ptp as (pt, pos as (p,p_)))), ifo) =
|
neuper@55486
|
343 |
(([], [], (pt, pos_pred)), f_in);
|
neuper@55486
|
344 |
val fo =
|
neuper@55486
|
345 |
case p_ of
|
neuper@55486
|
346 |
Frm => get_obj g_form pt p
|
neuper@55486
|
347 |
| Res => (fst o (get_obj g_result pt)) p
|
walther@59861
|
348 |
| _ => TermC.empty (*on PblObj is fo <> ifo*);
|
neuper@55486
|
349 |
val {nrls, ...} = get_met (get_obj g_metID pt (par_pblobj pt p))
|
walther@59852
|
350 |
val {rew_ord, erls, rules, ...} = Rule_Set.rep nrls;
|
walther@59907
|
351 |
(*val (found, der) = *)Derive.steps rew_ord erls rules fo ifo; (*<---------------*)
|
walther@59906
|
352 |
"~~~~~ fun .concat_deriv, args:"; val (rew_ord, erls, rules, fo, ifo) =
|
neuper@55486
|
353 |
(rew_ord, erls, rules, fo, ifo);
|
walther@59861
|
354 |
fun derivat ([]:(term * rule * (term * term list)) list) = TermC.empty
|
neuper@55486
|
355 |
| derivat dt = (#1 o #3 o last_elem) dt
|
neuper@55486
|
356 |
fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1=t2
|
walther@59907
|
357 |
(*val fod = *)Derive.do_one (Isac"") erls rules (snd rew_ord) NONE fo;
|
walther@59907
|
358 |
(*val ifod = *)Derive.do_one (Isac"") erls rules (snd rew_ord) NONE ifo;
|
neuper@55486
|
359 |
|