neuper@42279
|
1 |
(* Title: tests for Interpret/mathengine.sml
|
neuper@42279
|
2 |
Author: Walther Neuper 2000, 2006
|
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 ----------------------------------";
|
neuper@55412
|
16 |
"---------- mini-subpbl isac-java 3992e3bd1948: initial <NEXT> ---------------";
|
neuper@41982
|
17 |
"----------- fun step: Apply_Method without init_form ---";
|
neuper@38065
|
18 |
"----------- fun step -----------------------------------";
|
neuper@38065
|
19 |
"----------- fun autocalc -------------------------------";
|
s1210629013@55446
|
20 |
"----------- fun autoCalculate' --------------------------";
|
neuper@42067
|
21 |
"----------- fun autoCalculate..CompleteCalc ------------";
|
t@42225
|
22 |
"----------- search for Or_to_List ----------------------";
|
neuper@42279
|
23 |
"----------- check thy in CalcTreeTEST ------------------";
|
neuper@38065
|
24 |
"--------------------------------------------------------";
|
neuper@38065
|
25 |
"--------------------------------------------------------";
|
neuper@38065
|
26 |
"--------------------------------------------------------";
|
neuper@37906
|
27 |
|
neuper@41940
|
28 |
"----------- change to parse ctxt -----------------------";
|
neuper@41940
|
29 |
"----------- change to parse ctxt -----------------------";
|
neuper@41940
|
30 |
"----------- change to parse ctxt -----------------------";
|
neuper@41940
|
31 |
"===== start calculation: from problem description (fmz) to origin";
|
neuper@41940
|
32 |
val fmz = ["realTestGiven (((1+2)*4/3)^^^2)","realTestFind s"];
|
neuper@41940
|
33 |
val (thyID, pblID, metID) =
|
neuper@41940
|
34 |
("Test", ["calculate", "test"], ["Test", "test_calculate"]);
|
neuper@41940
|
35 |
val (p,_,_,nxt,_,pt) = CalcTreeTEST [(fmz, (thyID, pblID, metID))];
|
neuper@41940
|
36 |
"----- ";
|
neuper@41940
|
37 |
(* call sequence: CalcTreeTEST
|
neuper@41940
|
38 |
> nxt_specify_init_calc
|
neuper@41940
|
39 |
> prep_ori
|
neuper@41940
|
40 |
*)
|
neuper@41940
|
41 |
val (thy, pbt) = (Thy_Info.get_theory thyID, (#ppc o get_pbt) pblID);
|
neuper@41940
|
42 |
"----- in prep_ori";
|
neuper@48761
|
43 |
val ctxt = Proof_Context.init_global thy;
|
neuper@41940
|
44 |
|
bonzai@41952
|
45 |
val ctopts = map (parseNEW ctxt) fmz;
|
bonzai@41952
|
46 |
val dts = map (split_dts o the) ctopts;
|
neuper@41940
|
47 |
(*split_dts:
|
neuper@41940
|
48 |
(term * term list) list
|
neuper@41940
|
49 |
formulas: e.g. ((1+2)*4/3)^^^2
|
neuper@41940
|
50 |
description: e.g. realTestGiven
|
neuper@41940
|
51 |
*)
|
neuper@41940
|
52 |
prep_ori;
|
neuper@41940
|
53 |
(* FROM
|
neuper@41940
|
54 |
val it = fn:
|
neuper@41940
|
55 |
string list -> theory -> (string * (term * 'a)) list -> ori list
|
neuper@41940
|
56 |
TO
|
neuper@41940
|
57 |
val it = fn:
|
neuper@41940
|
58 |
string list -> theory -> (string * (term * 'a)) list -> (ori list * ctxt)
|
neuper@41940
|
59 |
AND
|
neuper@41940
|
60 |
FROM val oris = prep_ori...
|
neuper@41940
|
61 |
TO val (oris, _) = prep_ori...
|
neuper@41940
|
62 |
*)
|
neuper@41940
|
63 |
"----- insert ctxt in ptree";
|
neuper@41940
|
64 |
(* datatype ppobj
|
neuper@41940
|
65 |
FROM loc : istate option * istate option,
|
neuper@41940
|
66 |
TO loc : (istate * ctxt) option * (istate * ctxt) option,
|
neuper@41940
|
67 |
e.g.
|
neuper@41940
|
68 |
FROM val pt = Nd (PblObj
|
neuper@41940
|
69 |
{.., loc = (SOME (ScrState ([], [], NONE, Const ("empty", "'a"), Sundef, false)),
|
neuper@41940
|
70 |
NONE),
|
neuper@41940
|
71 |
TO val pt = Nd (PblObj
|
neuper@41940
|
72 |
{.., loc =
|
neuper@41940
|
73 |
((SOME (ScrState ([], [], NONE, Const ("empty", "'a"), Sundef, false)), ctxt),
|
neuper@41940
|
74 |
NONE),
|
neuper@41940
|
75 |
*)
|
neuper@41940
|
76 |
|
neuper@41940
|
77 |
"===== interactive specification: from origin to specification (probl)";
|
neuper@41940
|
78 |
val (p,_,_,nxt,_,pt) = me nxt p [1] pt;
|
neuper@41940
|
79 |
(*nxt =("Add_Given", Model_Problem)*)
|
neuper@41940
|
80 |
val (p,_,_,nxt,_,pt) = me nxt p [1] pt;
|
neuper@41940
|
81 |
(*nxt = ("Add_Find",Add_Find "realTestFind s") : string * tac*)
|
neuper@41940
|
82 |
"----- ";
|
neuper@41940
|
83 |
(* call sequence: me Model_Problem
|
neuper@41940
|
84 |
> me ("Add_Given", Add_Given "realTestGiven (((1 + 2) * 4 / 3) ^^^ 2)")
|
neuper@41940
|
85 |
> locatetac tac
|
neuper@41940
|
86 |
> loc_specify_
|
neuper@41940
|
87 |
> specify GET ctxt (stored in ctree)
|
neuper@41940
|
88 |
> specify_additem
|
neuper@41940
|
89 |
> appl_add
|
neuper@41940
|
90 |
|
neuper@41940
|
91 |
*)
|
neuper@41940
|
92 |
"----- in appl_add";
|
neuper@41940
|
93 |
(* FROM appl_add thy
|
neuper@41940
|
94 |
TO appl_add ctxt
|
neuper@41940
|
95 |
FROM parse thy str
|
neuper@41940
|
96 |
TO parseNEW ctxt str
|
neuper@41940
|
97 |
*)
|
neuper@41940
|
98 |
val (p,_,_,nxt,_,pt) = me nxt p [1] pt;
|
neuper@41940
|
99 |
(*nxt = ("Specify_Theory",Specify_Theory "Test") : string * tac*)
|
neuper@41940
|
100 |
val (p,_,_,nxt,_,pt) = me nxt p [1] pt;
|
neuper@41940
|
101 |
(*nxt = ("Specify_Problem",Specify_Problem ["calculate","test"])*)
|
neuper@41940
|
102 |
|
neuper@41940
|
103 |
"===== end specify: from specification (probl) to guard (method)";
|
neuper@41940
|
104 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@41940
|
105 |
(*nxt = ("Specify_Method",Specify_Method ("Test","test_calculate"))*)
|
neuper@41940
|
106 |
|
neuper@41940
|
107 |
"===== start interpretation: from guard to environment";
|
neuper@41940
|
108 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@41940
|
109 |
(*nxt = ("Apply_Method",Apply_Method ("Test","test_calculate"))*)
|
neuper@41940
|
110 |
"----- ";
|
neuper@41940
|
111 |
(* call sequence: me ("Apply_Method",...
|
neuper@41940
|
112 |
> locatetac
|
neuper@41940
|
113 |
> loc_solve_
|
neuper@41940
|
114 |
> solve ("Apply_Method",...
|
neuper@41940
|
115 |
*)
|
neuper@41940
|
116 |
val ((_,tac), ptp) = (nxt, (pt, p));
|
neuper@41940
|
117 |
locatetac tac (pt,p);
|
neuper@41940
|
118 |
val (mI, m) = mk_tac'_ tac;
|
neuper@41940
|
119 |
val Appl m = applicable_in p pt m;
|
neuper@41940
|
120 |
member op = specsteps mI;
|
neuper@41940
|
121 |
loc_solve_ (mI,m) ptp;
|
neuper@41940
|
122 |
val (m, (pt, pos)) = ((mI,m), ptp);
|
neuper@41940
|
123 |
solve m (pt, pos);
|
bonzai@41949
|
124 |
val ((_, m as Apply_Method' (mI, _, _, _)), (pt, (pos as (p,_)))) =
|
neuper@41940
|
125 |
(m, (pt, pos));
|
neuper@41940
|
126 |
val {srls,...} = get_met mI;
|
neuper@41940
|
127 |
val PblObj{meth=itms,...} = get_obj I pt p;
|
neuper@41940
|
128 |
val thy' = get_obj g_domID pt p;
|
neuper@41940
|
129 |
val thy = assoc_thy thy';
|
bonzai@41949
|
130 |
val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
|
neuper@41940
|
131 |
|
neuper@41940
|
132 |
"----- go on in the calculation";
|
neuper@41940
|
133 |
val (p,_,f,nxt,_,pt) = me nxt pos [1] pt;
|
neuper@41940
|
134 |
(*nxt = ("Calculate",Calculate "PLUS")*)
|
neuper@41940
|
135 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@41940
|
136 |
(*nxt = ("Calculate",Calculate "TIMES")*)
|
neuper@41940
|
137 |
|
neuper@41940
|
138 |
"===== input a formula to be derived from previous istate";
|
neuper@41940
|
139 |
"----- appendFormula TODO: first repair error";
|
neuper@41940
|
140 |
val cs = ((pt,p),[]);
|
neuper@41940
|
141 |
val ("ok", cs' as (_,_,(pt,p))) = step p cs;
|
neuper@41943
|
142 |
val ifo = (* encode "4^^^2" \<longrightarrow>*) "4^2";
|
neuper@41940
|
143 |
(*
|
neuper@41943
|
144 |
val ("no derivation found", (_,_,(pt, p))) = inform cs' ((*encode*) ifo);
|
neuper@41940
|
145 |
here ^^^^^^^^^^^^^^^^^^^^^ should be "ok"
|
neuper@41940
|
146 |
*)
|
neuper@41940
|
147 |
|
neuper@41940
|
148 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@41940
|
149 |
(*nxt = ("Calculate",Calculate "DIVIDE")*)
|
neuper@41940
|
150 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@41940
|
151 |
(*nxt = ("Calculate",Calculate "POWER")*)
|
neuper@41940
|
152 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@41940
|
153 |
(*nxt = ("Check_Postcond",Check_Postcond ["calculate","test"])*)
|
neuper@41940
|
154 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@41940
|
155 |
(*nxt = ("End_Proof'",End_Proof')*)
|
neuper@41940
|
156 |
if f = Form' (FormKF (~1,EdUndef,0,Nundef,"16")) then ()
|
neuper@41940
|
157 |
else error "calculate.sml: script test_calculate changed behaviour";
|
neuper@41940
|
158 |
|
neuper@41940
|
159 |
"===== tactic Subproblem: from environment to origin";
|
neuper@41940
|
160 |
"----- TODO";
|
neuper@41940
|
161 |
|
neuper@37906
|
162 |
|
neuper@38065
|
163 |
"----------- debugging setContext..pbl_ -----------------";
|
neuper@38065
|
164 |
"----------- debugging setContext..pbl_ -----------------";
|
neuper@38065
|
165 |
"----------- debugging setContext..pbl_ -----------------";
|
s1210629013@55445
|
166 |
reset_states ();
|
neuper@41970
|
167 |
CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
|
neuper@41970
|
168 |
("Test", ["sqroot-test","univariate","equation","test"],
|
neuper@37906
|
169 |
["Test","squ-equ-test-subpbl1"]))];
|
neuper@37906
|
170 |
Iterator 1;
|
neuper@37906
|
171 |
moveActiveRoot 1; modelProblem 1;
|
neuper@37906
|
172 |
|
neuper@37906
|
173 |
val pos as (p,_) = ([],Pbl);
|
neuper@37906
|
174 |
val guh = "pbl_equ_univ";
|
neuper@37906
|
175 |
checkContext 1 pos guh;
|
neuper@37906
|
176 |
val ((pt,_),_) = get_calc 1;
|
neuper@37906
|
177 |
val pp = par_pblobj pt p;
|
neuper@37906
|
178 |
val keID = guh2kestoreID guh;
|
neuper@37906
|
179 |
case context_pbl keID pt pp of (true,["univariate", "equation"],_,_,_)=>()
|
neuper@38031
|
180 |
| _ => error "mathengine.sml: context_pbl .. pbl_equ_univ checked";
|
neuper@37906
|
181 |
|
neuper@37906
|
182 |
case get_obj g_spec pt p of (_, ["e_pblID"], _) => ()
|
neuper@38031
|
183 |
| _ => error "mathengine.sml: context_pbl .. pbl still empty";
|
neuper@37906
|
184 |
setContext 1 pos guh;
|
neuper@37906
|
185 |
val ((pt,_),_) = get_calc 1;
|
neuper@37906
|
186 |
case get_obj g_spec pt p of (_, ["univariate", "equation"], _) => ()
|
neuper@38031
|
187 |
| _ => error "mathengine.sml: context_pbl .. pbl set";
|
neuper@37906
|
188 |
|
neuper@37906
|
189 |
|
neuper@37906
|
190 |
setContext 1 pos "met_eq_lin";
|
neuper@37906
|
191 |
val ((pt,_),_) = get_calc 1;
|
neuper@37906
|
192 |
case get_obj g_spec pt p of (_, _, ["LinEq", "solve_lineq_equation"]) => ()
|
neuper@38031
|
193 |
| _ => error "mathengine.sml: context_pbl .. pbl set";
|
neuper@37906
|
194 |
|
neuper@37906
|
195 |
|
neuper@38065
|
196 |
"----------- tryrefine ----------------------------------";
|
neuper@38065
|
197 |
"----------- tryrefine ----------------------------------";
|
neuper@38065
|
198 |
"----------- tryrefine ----------------------------------";
|
s1210629013@55445
|
199 |
reset_states ();
|
neuper@37906
|
200 |
CalcTree [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
|
neuper@37906
|
201 |
"solveFor x", "solutions L"],
|
neuper@38058
|
202 |
("RatEq",["univariate","equation"],["no_met"]))];
|
neuper@37906
|
203 |
Iterator 1;
|
s1210629013@55446
|
204 |
moveActiveRoot 1; autoCalculate' 1 CompleteCalc;
|
neuper@37906
|
205 |
|
neuper@37906
|
206 |
refineProblem 1 ([1],Res) "pbl_equ_univ"
|
neuper@37906
|
207 |
(*gives "pbl_equ_univ_rat" correct*);
|
neuper@37906
|
208 |
|
neuper@55279
|
209 |
refineProblem 1 ([1],Res) (pblID2guh ["LINEAR","univariate","equation"])
|
neuper@38065
|
210 |
(*gives "pbl_equ_univ_lin" incorrect*);
|
neuper@38065
|
211 |
|
neuper@55412
|
212 |
"---------- mini-subpbl isac-java 3992e3bd1948: initial <NEXT> ---------------";
|
neuper@55412
|
213 |
"---------- mini-subpbl isac-java 3992e3bd1948: initial <NEXT> ---------------";
|
neuper@55412
|
214 |
"---------- mini-subpbl isac-java 3992e3bd1948: initial <NEXT> ---------------";
|
s1210629013@55445
|
215 |
reset_states ();
|
neuper@55412
|
216 |
(*this is the exact sequence of input provided by isac-java 3992e3bd1948;
|
neuper@55412
|
217 |
Surrounding ML { * ... * } are omitted.
|
neuper@55412
|
218 |
The multiple calls suggest to replicate the CalcTree in the Dialogue.
|
neuper@55412
|
219 |
*)
|
neuper@55412
|
220 |
CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
|
neuper@55412
|
221 |
("Test",["sqroot-test","univariate","equation","test"],["Test","squ-equ-test-subpbl1"]))];
|
neuper@55412
|
222 |
Iterator 1;
|
neuper@55412
|
223 |
moveActiveRoot 1;
|
neuper@55412
|
224 |
getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 0 false;
|
neuper@55412
|
225 |
getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 0 false;
|
s1210629013@55446
|
226 |
(*completeCalcHead*)autoCalculate' 1 CompleteCalcHead;
|
neuper@55412
|
227 |
(*completeCalcHead*)getActiveFormula 1 ;
|
neuper@55412
|
228 |
(*completeCalcHead*)refFormula 1 ([],Met);
|
neuper@55412
|
229 |
refFormula 1 ([],Pbl);
|
neuper@55412
|
230 |
(*<REFFORMULA> <CALCID> 1 </CALCID> <CALCHEAD status = "correct"> *)
|
neuper@55473
|
231 |
fetchProposedTactic 1;
|
neuper@55473
|
232 |
(*-> <STRINGLISTTACTIC name="Apply_Method">
|
neuper@55473
|
233 |
<STRINGLIST>
|
neuper@55473
|
234 |
<STRING> Test </STRING>
|
neuper@55473
|
235 |
<STRING> squ-equ-test-subpbl1 </STRING>
|
neuper@55473
|
236 |
WAS PREVIOUSLY: <SYSERROR> <CALCID> 1 </CALCID> <ERROR> error in kernel </ERROR></SYSERROR>*)
|
neuper@55412
|
237 |
"~~~~~ fun fetchProposedTactic, args:"; val (cI) = (1);
|
neuper@55412
|
238 |
val ("ok", (tacis, _, _)) = step (get_pos cI 1) (get_calc cI)
|
neuper@55412
|
239 |
val _= upd_tacis cI tacis
|
neuper@55412
|
240 |
val (tac,_,_) = last_elem tacis;
|
neuper@55412
|
241 |
(*fetchproposedtacticOK2xml cI tac (fetchErrorpatterns tac);
|
neuper@55415
|
242 |
fetchErrorpatterns tac
|
neuper@55473
|
243 |
WAS PREVIOUSLY ERROR: app_py: not found: ["IsacKnowledge","KEStore","Rulesets","e_rls"]*)
|
neuper@55415
|
244 |
"~~~~~ fun fetchErrorpatterns, args:"; val (tac) = (tac);
|
neuper@55415
|
245 |
val rlsID = "e_rls"
|
neuper@55415
|
246 |
val (part, thyID) = thy_containing_rls "Build_Thydata" rlsID;
|
neuper@55458
|
247 |
if part = "IsacScripts" andalso thyID = "KEStore" then ()
|
neuper@55415
|
248 |
else error "fetchErrorpatterns .. e_rls changed";
|
neuper@55473
|
249 |
val Hrls {thy_rls = (_, rls), ...} = get_the [part, thyID, "Rulesets", rlsID];
|
neuper@55473
|
250 |
(* WAS PREVIOUSLY ERROR app_py: not found: ["IsacKnowledge","KEStore","Rulesets","e_rls"]*)
|
neuper@55473
|
251 |
case rls of
|
neuper@55473
|
252 |
Rls {id = "e_rls", ...} => ()
|
neuper@55473
|
253 |
| _ => error "thy_containing_rls changed for e_rls"
|
neuper@38065
|
254 |
|
neuper@41982
|
255 |
"----------- fun step: Apply_Method without init_form ---";
|
neuper@41982
|
256 |
"----------- fun step: Apply_Method without init_form ---";
|
neuper@41982
|
257 |
"----------- fun step: Apply_Method without init_form ---";
|
neuper@41982
|
258 |
val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
|
neuper@41982
|
259 |
val (dI',pI',mI') =
|
neuper@41982
|
260 |
("Test", ["sqroot-test","univariate","equation","test"],
|
neuper@41982
|
261 |
["Test","squ-equ-test-subpbl1"]);
|
neuper@41982
|
262 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@41982
|
263 |
"~~~~~ fun me, args:"; val (_,tac) = nxt;
|
neuper@41982
|
264 |
val ("ok", (_, _, (pt, p))) = locatetac tac (pt,p);
|
neuper@41982
|
265 |
"~~~~~ fun step, args:"; val (ip as (_,p_), ptp as (pt,p), tacis) = (p, (pt, e_pos'), []);
|
neuper@41982
|
266 |
val pIopt = get_pblID (pt,ip);
|
neuper@41982
|
267 |
ip = ([],Res) (*false*);
|
neuper@41982
|
268 |
val SOME pI = pIopt;
|
neuper@55412
|
269 |
member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p));
|
neuper@41982
|
270 |
(*^^^^^^^^: Apply_Method without init_form*)
|
neuper@38065
|
271 |
|
neuper@38065
|
272 |
"----------- fun step -----------------------------------";
|
neuper@38065
|
273 |
"----------- fun step -----------------------------------";
|
neuper@38065
|
274 |
"----------- fun step -----------------------------------";
|
neuper@38065
|
275 |
val p = e_pos'; val c = [];
|
neuper@38065
|
276 |
val (p,_,f,nxt,_,pt) =
|
neuper@38065
|
277 |
CalcTreeTEST
|
neuper@38065
|
278 |
[(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"],
|
neuper@38065
|
279 |
("Integrate", ["integrate","function"], ["diff","integration"]))];
|
neuper@38065
|
280 |
"----- step 1: returns tac = Model_Problem ---";
|
neuper@38065
|
281 |
val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
|
neuper@38065
|
282 |
"----- step 2: returns tac = ---";
|
neuper@38065
|
283 |
val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
|
neuper@38065
|
284 |
"----- step 3: returns tac = ---";
|
neuper@38065
|
285 |
val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
|
neuper@38065
|
286 |
"----- step 4: returns tac = ---";
|
neuper@38065
|
287 |
val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
|
neuper@38065
|
288 |
"----- step 5: returns tac = ---";
|
neuper@38065
|
289 |
|
neuper@48895
|
290 |
(*========== inhibit exn AK110718 ==============================================
|
neuper@38066
|
291 |
2002 stops here as well: TODO review actual arguments:
|
neuper@38065
|
292 |
val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
|
neuper@38065
|
293 |
"----- step 6: returns tac = ---";
|
neuper@38065
|
294 |
val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
|
neuper@38065
|
295 |
"----- step 7: returns tac = ---";
|
neuper@38065
|
296 |
val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
|
neuper@38065
|
297 |
"----- step 8: returns tac = ---";
|
neuper@38065
|
298 |
val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
|
neuper@48895
|
299 |
========== inhibit exn AK110718 ==============================================*)
|
neuper@38065
|
300 |
|
neuper@38065
|
301 |
|
neuper@38065
|
302 |
"----------- fun autocalc -------------------------------";
|
neuper@38065
|
303 |
"----------- fun autocalc -------------------------------";
|
neuper@38065
|
304 |
"----------- fun autocalc -------------------------------";
|
neuper@38065
|
305 |
val p = e_pos'; val c = [];
|
neuper@38065
|
306 |
val (p,_,f,nxt,_,pt) =
|
neuper@38065
|
307 |
CalcTreeTEST
|
neuper@38065
|
308 |
[(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"],
|
neuper@38065
|
309 |
("Integrate",["integrate","function"], ["diff","integration"]))];
|
neuper@38066
|
310 |
(*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
|
neuper@38066
|
311 |
modeling is skipped FIXME
|
neuper@38066
|
312 |
*-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
|
neuper@38065
|
313 |
tracing "----- step 1 ---";
|
neuper@38065
|
314 |
val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
|
neuper@38065
|
315 |
tracing "----- step 2 ---";
|
neuper@38065
|
316 |
val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
|
neuper@38065
|
317 |
tracing "----- step 3 ---";
|
neuper@38065
|
318 |
val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
|
neuper@38065
|
319 |
tracing "----- step 4 ---";
|
neuper@38065
|
320 |
val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
|
neuper@38065
|
321 |
tracing "----- step 5 ---";
|
neuper@38065
|
322 |
val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
|
neuper@38065
|
323 |
tracing "----- step 6 ---";
|
neuper@38065
|
324 |
val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
|
neuper@38065
|
325 |
tracing "----- step 7 ---";
|
neuper@38065
|
326 |
val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
|
neuper@38065
|
327 |
tracing "----- step 8 ---";
|
neuper@38065
|
328 |
val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
|
neuper@48895
|
329 |
(*========== inhibit exn AK110718 ==============================================
|
neuper@42067
|
330 |
WN110628: Integration does not work, see Knowledge/integrate.sml
|
neuper@42067
|
331 |
|
neuper@41929
|
332 |
if str = "end-of-calculation" andalso
|
neuper@41929
|
333 |
term2str (get_obj g_res pt (fst p)) = "c + x + 1 / 3 * x ^^^ 3" then ()
|
neuper@38065
|
334 |
else error "mathengine.sml -- fun autocalc -- end";
|
neuper@48895
|
335 |
========== inhibit exn AK110718 ==============================================*)
|
neuper@38065
|
336 |
|
neuper@38065
|
337 |
|
s1210629013@55446
|
338 |
"----------- fun autoCalculate' -----------------------------------";
|
s1210629013@55446
|
339 |
"----------- fun autoCalculate' -----------------------------------";
|
s1210629013@55446
|
340 |
"----------- fun autoCalculate' -----------------------------------";
|
s1210629013@55445
|
341 |
reset_states ();
|
neuper@38065
|
342 |
CalcTree (*ATTENTION: encode_fmz ... unlike CalcTreeTEST*)
|
neuper@38065
|
343 |
[(["functionTerm (x^2 + 1)", "integrateBy x", "antiDerivative FF"],
|
neuper@38065
|
344 |
("Integrate", ["integrate", "function"], ["diff", "integration"]))];
|
neuper@38065
|
345 |
Iterator 1;
|
neuper@38065
|
346 |
moveActiveRoot 1;
|
neuper@38066
|
347 |
(*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
|
neuper@38066
|
348 |
modeling is skipped FIXME
|
neuper@38066
|
349 |
see test/../interface -- solve_linear as rootpbl FE -- for OTHER expl:
|
neuper@38066
|
350 |
setNextTactic 1 (Add_Given "equality (1 + -1 * 2 + x = 0)");
|
s1210629013@55446
|
351 |
autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1); (*equality added*);
|
neuper@38066
|
352 |
|
neuper@38066
|
353 |
fetchProposedTactic 1;
|
neuper@38066
|
354 |
setNextTactic 1 (Add_Given "solveFor x");
|
s1210629013@55446
|
355 |
autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
|
neuper@38066
|
356 |
|
neuper@38066
|
357 |
fetchProposedTactic 1;
|
neuper@38066
|
358 |
setNextTactic 1 (Add_Find "solutions L");
|
s1210629013@55446
|
359 |
autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
|
neuper@38066
|
360 |
|
neuper@38066
|
361 |
fetchProposedTactic 1;
|
neuper@38066
|
362 |
setNextTactic 1 (Specify_Theory "Test");
|
s1210629013@55446
|
363 |
autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
|
neuper@38066
|
364 |
*-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
|
s1210629013@55446
|
365 |
autoCalculate' 1 (Step 1);
|
neuper@38065
|
366 |
"----- step 1 ---";
|
s1210629013@55446
|
367 |
autoCalculate' 1 (Step 1);
|
neuper@38065
|
368 |
"----- step 2 ---";
|
s1210629013@55446
|
369 |
autoCalculate' 1 (Step 1);
|
neuper@38065
|
370 |
"----- step 3 ---";
|
s1210629013@55446
|
371 |
autoCalculate' 1 (Step 1);
|
neuper@38065
|
372 |
"----- step 4 ---";
|
s1210629013@55446
|
373 |
autoCalculate' 1 (Step 1);
|
neuper@38065
|
374 |
"----- step 5 ---";
|
s1210629013@55446
|
375 |
autoCalculate' 1 (Step 1);
|
neuper@38065
|
376 |
"----- step 6 ---";
|
s1210629013@55446
|
377 |
autoCalculate' 1 (Step 1);
|
neuper@38065
|
378 |
"----- step 7 ---";
|
s1210629013@55446
|
379 |
autoCalculate' 1 (Step 1);
|
neuper@38065
|
380 |
"----- step 8 ---";
|
s1210629013@55446
|
381 |
autoCalculate' 1 (Step 1);
|
neuper@38065
|
382 |
val (ptp as (_, p), _) = get_calc 1;
|
neuper@38065
|
383 |
val (Form t,_,_) = pt_extract ptp;
|
akargl@42108
|
384 |
|
neuper@38065
|
385 |
if term2str t = "c + x + 1 / 3 * x ^^^ 3" andalso p = ([], Res) then ()
|
s1210629013@55446
|
386 |
else error "mathengine.sml -- fun autoCalculate' -- end";
|
neuper@38065
|
387 |
|
neuper@42067
|
388 |
"----------- fun autoCalculate..CompleteCalc ------------";
|
neuper@42067
|
389 |
"----------- fun autoCalculate..CompleteCalc ------------";
|
neuper@42067
|
390 |
"----------- fun autoCalculate..CompleteCalc ------------";
|
s1210629013@55445
|
391 |
reset_states ();
|
neuper@42067
|
392 |
CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
|
neuper@42067
|
393 |
("Test", ["sqroot-test","univariate","equation","test"],
|
neuper@42067
|
394 |
["Test","squ-equ-test-subpbl1"]))];
|
neuper@42067
|
395 |
Iterator 1;
|
neuper@42103
|
396 |
moveActiveRoot 1;
|
s1210629013@55446
|
397 |
(*autoCalculate' 1 CompleteCalc; (*WAS <SYSERROR>..<ERROR> error in kernel </ERROR>*)*)
|
neuper@42103
|
398 |
"~~~~~ fun autoCalculate, args:"; val (cI, auto) = (1, CompleteCalc);
|
neuper@42103
|
399 |
val pold = get_pos cI 1;
|
neuper@42103
|
400 |
(*autocalc [] pold (get_calc cI) auto; (*WAS Type unification failed
|
neuper@42103
|
401 |
Type error in application: incompatible operand type
|
neuper@42103
|
402 |
Operator: solveFor :: real \<Rightarrow> una
|
neuper@42103
|
403 |
Operand: x :: 'a *)*)
|
neuper@42103
|
404 |
"~~~~~ fun autocalc, args:"; val (c, (pos as (_,p_)), ((pt,_), _), auto)
|
neuper@42103
|
405 |
= ([] : pos' list, pold, (get_calc cI), auto);
|
neuper@42103
|
406 |
autoord auto > 3 andalso just_created (pt, pos); (*true*)
|
neuper@42103
|
407 |
val ptp = all_modspec (pt, pos);
|
neuper@42103
|
408 |
"TODO all_modspec: preconds for rootpbl";
|
neuper@42103
|
409 |
(*all_solve auto c ptp; (*WAS Type unification failed...*)*)
|
neuper@42103
|
410 |
"~~~~~ and all_solve, args:"; val (auto, c, (ptp as (pt, pos as (p,_)))) =
|
neuper@42103
|
411 |
(auto, c, ptp);
|
neuper@42103
|
412 |
val (_,_,mI) = get_obj g_spec pt p
|
neuper@42103
|
413 |
val ctxt = get_ctxt pt pos
|
neuper@42103
|
414 |
val (ttt, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate, ctxt)) (e_istate, ctxt) ptp;
|
neuper@42103
|
415 |
(* complete_solve auto (c @ c') ptp; (*WAS Type unification failed...*) pos = ([], Met)*)
|
neuper@42103
|
416 |
"~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)))) =
|
neuper@42103
|
417 |
(auto, (c @ c'), ptp);
|
neuper@42103
|
418 |
p = ([], Res) (*false p = ([1], Frm)*);
|
neuper@42103
|
419 |
member op = [Pbl,Met] p_ (*false*);
|
neuper@42103
|
420 |
val (ttt, c', ptp') = nxt_solve_ ptp; (*ttt = Rewrite_Set "norm_equation"*)
|
neuper@42103
|
421 |
(* complete_solve auto (c @ c') ptp'; (*WAS Type unification failed...*) pos = ([], Met)*)
|
neuper@42103
|
422 |
"~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)))) =
|
neuper@42103
|
423 |
(auto, (c @ c'), ptp');
|
neuper@42103
|
424 |
p = ([], Res) (*false p = ([1], Res)*);
|
neuper@42103
|
425 |
member op = [Pbl,Met] p_ (*false*);
|
neuper@42103
|
426 |
val (ttt, c', ptp') = nxt_solve_ ptp; (*ttt = Rewrite_Set "Test_simplify"*)
|
neuper@42103
|
427 |
(* complete_solve auto (c @ c') ptp'; (*WAS Type unification failed...*) pos = ([], Met)*)
|
neuper@42103
|
428 |
"~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)))) =
|
neuper@42103
|
429 |
(auto, (c @ c'), ptp');
|
neuper@42103
|
430 |
p = ([], Res) (*false p = ([2], Res)*);
|
neuper@42103
|
431 |
member op = [Pbl,Met] p_ (*false*);
|
neuper@42103
|
432 |
val ((Subproblem _, tac_, (_, is))::_, c', ptp') = nxt_solve_ ptp;
|
neuper@42103
|
433 |
autoord auto < 5 (*false*);
|
neuper@42103
|
434 |
(* val ptp = all_modspec ptp' (*WAS Type unification failed...*)*)
|
neuper@42103
|
435 |
"~~~~~ fun all_modspec, args:"; val (pt, pos as (p,_)) = (ptp');
|
neuper@42103
|
436 |
val (PblObj {fmz = (fmz_, _), origin = (pors, spec as (dI,pI,mI), hdl), ...}) = get_obj I pt p;
|
neuper@42103
|
437 |
val thy = assoc_thy dI;
|
neuper@42103
|
438 |
val {ppc, ...} = get_met mI;
|
neuper@42103
|
439 |
(* val (mors, ctxt) = prep_ori fmz_ thy ppc; WAS Type unification failed because
|
neuper@48761
|
440 |
val ctxt' = dI |> Thy_Info.get_theory |> Proof_Context.init_global;
|
neuper@42103
|
441 |
(parseNEW ctxt' "x" |> the |> type_of) = TFree ("'a",[]);
|
neuper@42103
|
442 |
^^^^^ *)
|
neuper@42103
|
443 |
(*vvv from: | assod pt _ (Subproblem'...*)
|
neuper@42103
|
444 |
val (fmz_, vals) = oris2fmz_vals pors;
|
neuper@42103
|
445 |
(**)
|
neuper@48761
|
446 |
val ctxt = dI |> Thy_Info.get_theory |> Proof_Context.init_global
|
neuper@42103
|
447 |
|> declare_constraints' vals
|
neuper@42103
|
448 |
(**)
|
neuper@42103
|
449 |
(*^^^ from: | assod pt _ (Subproblem'...*)
|
neuper@42103
|
450 |
val [(1, [1], "#Given", dsc_eq, [equality]),
|
neuper@42103
|
451 |
(2, [1], "#Given", dsc_solvefor, [xxx]),
|
neuper@42103
|
452 |
(3, [1], "#Find", dsc_solutions, [x_i])] = pors;
|
neuper@42103
|
453 |
if term2str xxx = "x" andalso type_of xxx = HOLogic.realT then ()
|
neuper@42103
|
454 |
else error "autoCalculate..CompleteCalc: SubProblem broken 1";
|
neuper@42103
|
455 |
val pt = update_pblppc pt p (map (ori2Coritm ppc) pors);
|
neuper@42103
|
456 |
val pt = update_metppc pt p (map (ori2Coritm ppc) pors);
|
neuper@42103
|
457 |
val pt = update_spec pt p (dI,pI,mI);
|
neuper@42103
|
458 |
val pt = update_ctxt pt p ctxt;
|
neuper@42103
|
459 |
"~~~~~ return to complete_solve, args:"; val (ptp) = (pt, (p,Met));
|
neuper@42103
|
460 |
val (msg, c, (pt, p)) = complete_solve auto (c @ c') ptp;
|
neuper@42103
|
461 |
if msg = "end-of-calculation" andalso c = [] andalso p = ([], Res) then ()
|
neuper@42103
|
462 |
else error "autoCalculate..CompleteCalc: final result";
|
neuper@42103
|
463 |
if terms2strs (get_assumptions_ pt p) =
|
neuper@42105
|
464 |
["matches (?a = ?b) (-1 + x = 0)", (*precond of submet*)
|
neuper@42104
|
465 |
"x = 1", (*result of subpbl and rootpbl*)
|
neuper@42104
|
466 |
"precond_rootmet x"] (*precond of rootmet*)
|
neuper@42103
|
467 |
then () else error "autoCalculate..CompleteCalc: ctxt at final result";
|
neuper@42067
|
468 |
|
akargl@42108
|
469 |
|
neuper@42394
|
470 |
"--------- search for Or_to_List ------------------------";
|
neuper@42394
|
471 |
"--------- search for Or_to_List ------------------------";
|
t@42225
|
472 |
"--------- search for Or_to_List ------------------------";
|
t@42225
|
473 |
val fmz = ["equality (x^^^2 + 4*x + 5 = (2::real))", "solveFor x","solutions L"];
|
t@42225
|
474 |
val (dI',pI',mI') = ("Isac", ["univariate","equation"], ["no_met"])
|
t@42225
|
475 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
t@42225
|
476 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
477 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
478 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
479 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
480 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
481 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
482 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
483 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
484 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
485 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Subproblem"*)
|
t@42225
|
486 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
487 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
488 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
489 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
490 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
491 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
492 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
493 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
494 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
495 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
496 |
"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), (_:NEW(*remove*)), (pt:ptree)) =
|
t@42225
|
497 |
(nxt, p, [], pt);
|
t@42225
|
498 |
val ("ok", (_, _, ptp)) = locatetac tac (pt,p)
|
t@42225
|
499 |
val (pt, p) = ptp;
|
t@42225
|
500 |
"~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =
|
t@42225
|
501 |
(p, ((pt, e_pos'),[]));
|
t@42225
|
502 |
val pIopt = get_pblID (pt,ip);
|
t@42225
|
503 |
ip = ([],Res); (*false*)
|
t@42225
|
504 |
ip = p; (*false*)
|
t@42225
|
505 |
member op = [Pbl,Met] p_; (*false*)
|
t@42225
|
506 |
"~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p,p_))) = (pt,ip);
|
t@42225
|
507 |
e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)
|
t@42225
|
508 |
val thy' = get_obj g_domID pt (par_pblobj pt p);
|
t@42225
|
509 |
val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
|
t@42225
|
510 |
val (tac_,is,(t,_)) = next_tac (thy',srls) (pt,pos) sc is; (*WAS Empty_Tac_: tac_*)
|
t@42225
|
511 |
case tac_ of Or_to_List' _ => ()
|
t@42225
|
512 |
| _ => error "Or_to_List broken ?"
|
akargl@42108
|
513 |
|
neuper@42394
|
514 |
|
neuper@42279
|
515 |
"----------- check thy in CalcTreeTEST ------------------";
|
neuper@42279
|
516 |
"----------- check thy in CalcTreeTEST ------------------";
|
neuper@42279
|
517 |
"----------- check thy in CalcTreeTEST ------------------";
|
neuper@42279
|
518 |
"WN1109 with Inverse_Z_Transform.thy when starting tests with CalcTreeTEST \n" ^
|
neuper@42279
|
519 |
"we got the message: ME_Isa: thy 'Build_Inverse_Z_Transform' not in system \n" ^
|
neuper@42279
|
520 |
"Below there are the steps which found out the reason: \n" ^
|
neuper@42279
|
521 |
"store_pbt mistakenly stored that theory.";
|
neuper@48761
|
522 |
val ctxt = Proof_Context.init_global @{theory Isac};
|
neuper@42279
|
523 |
val SOME t = parseNEW ctxt "filterExpression (X = 3 / (z - 1/4 + -1/8 * (1/(z::real))))";
|
neuper@42279
|
524 |
val SOME t = parseNEW ctxt "stepResponse (x[n::real]::bool)";
|
akargl@42108
|
525 |
|
neuper@42279
|
526 |
val fmz = ["filterExpression (X = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
|
neuper@42279
|
527 |
"stepResponse (x[n::real]::bool)"];
|
neuper@42405
|
528 |
val (dI,pI,mI) = ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
|
neuper@42405
|
529 |
["SignalProcessing","Z_Transform","Inverse"]);
|
neuper@42279
|
530 |
|
neuper@42279
|
531 |
val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))];
|
neuper@42279
|
532 |
(*WAS ME_Isa: thy 'Build_Inverse_Z_Transform' not in system*)
|
neuper@42279
|
533 |
|
neuper@42279
|
534 |
"~~~~~ T fun CalcTreeTEST, args:"; val [(fmz, sp):fmz] = [(fmz, (dI,pI,mI))];
|
neuper@42279
|
535 |
"~~~~~ fun nxt_specify_init_calc, args:"; val (fmz, (dI, pI, mI)) = (fmz, sp);
|
neuper@42279
|
536 |
val thy = assoc_thy dI;
|
neuper@42279
|
537 |
mI = ["no_met"]; (*false*)
|
neuper@42279
|
538 |
val (pI, (pors, pctxt), mI) = (pI, get_pbt pI |> #ppc |> prep_ori fmz thy, mI)
|
neuper@42279
|
539 |
val {cas, ppc, thy=thy',...} = get_pbt pI; (*take dI from _refined_ pbl*)
|
neuper@42279
|
540 |
"tracing bottom up"; Context.theory_name thy' = "Build_Inverse_Z_Transform"; (*WAS true*)
|
neuper@42279
|
541 |
val dI = theory2theory' (maxthy thy thy');
|
neuper@42279
|
542 |
"tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*)
|
neuper@42279
|
543 |
cas = NONE; (*true*)
|
neuper@42279
|
544 |
val hdl = pblterm dI pI;
|
neuper@42279
|
545 |
val (pt, _) = cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI))
|
neuper@42279
|
546 |
(pors, (dI, pI, mI), hdl)
|
neuper@42279
|
547 |
val pt = update_ctxt pt [] pctxt;
|
neuper@42279
|
548 |
|
neuper@42279
|
549 |
"~~~~~ fun nxt_specif, args:"; val ((tac as Model_Problem), (pt, pos as (p,p_))) = (Model_Problem, (pt, ([], Pbl)));
|
neuper@42279
|
550 |
val PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} = get_obj I pt p;
|
neuper@42279
|
551 |
"tracing bottom up"; #1(ospec) = "Build_Inverse_Z_Transform"; (*WAS true*)
|
neuper@42279
|
552 |
|
neuper@42279
|
553 |
"~~~~~ fun some_spec, args:"; val ((odI, opI, omI), (dI, pI, mI)) = (ospec, spec);
|
neuper@42279
|
554 |
dI = e_domID; (*true*)
|
neuper@42279
|
555 |
odI = "Build_Inverse_Z_Transform"; (*true*)
|
neuper@42279
|
556 |
dI = "e_domID"; (*true*)
|
neuper@42279
|
557 |
"~~~~~ after fun some_spec:";
|
neuper@42279
|
558 |
val (dI, pI, mI) = some_spec ospec spec;
|
neuper@42279
|
559 |
"tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*)
|
neuper@42279
|
560 |
val thy = assoc_thy dI; (*caused ME_Isa: thy 'Build_Inverse_Z_Transform' not in system*)
|
neuper@42279
|
561 |
|