|
1 (* The _functional_ mathematics engine, ie. without a state. |
|
2 Input and output are Isabelle's formulae as strings. |
|
3 authors: Walther Neuper 2000 |
|
4 (c) due to copyright terms |
|
5 |
|
6 use"mathengine.sml"; |
|
7 *) |
|
8 |
|
9 signature MATHENGINE = |
|
10 sig |
|
11 type nxt_ |
|
12 (* datatype nxt_ = HElpless | Nexts of CalcHead.calcstate *) |
|
13 type NEW |
|
14 type lOc_ |
|
15 (*datatype |
|
16 lOc_ = |
|
17 ERror of string |
|
18 | UNsafe of CalcHead.calcstate' |
|
19 | Updated of CalcHead.calcstate' *) |
|
20 |
|
21 val CalcTreeTEST : |
|
22 fmz list -> |
|
23 pos' * NEW * mout * (string * tac) * safe * ptree |
|
24 |
|
25 val TESTg_form : ptree * (int list * pos_) -> mout |
|
26 val autocalc : |
|
27 pos' list -> |
|
28 pos' -> |
|
29 (ptree * pos') * taci list -> |
|
30 auto -> string * pos' list * (ptree * pos') |
|
31 val detailstep : ptree -> pos' -> string * ptree * pos' |
|
32 (* val e_tac_ : tac_ *) |
|
33 val f2str : mout -> cterm' |
|
34 (* val get_pblID : ptree * pos' -> pblID option *) |
|
35 val initmatch : ptree -> pos' -> ptform |
|
36 (* val loc_solve_ : |
|
37 string * tac_ -> ptree * (int list * pos_) -> lOc_ *) |
|
38 (* val loc_specify_ : tac_ -> ptree * pos' -> lOc_ *) |
|
39 val locatetac : (*tests only*) |
|
40 tac -> |
|
41 ptree * (posel list * pos_) -> |
|
42 string * (taci list * pos' list * (ptree * (posel list * pos_))) |
|
43 val me : |
|
44 tac'_ -> |
|
45 pos' -> |
|
46 NEW -> |
|
47 ptree -> pos' * NEW * mout * tac'_ * safe * ptree |
|
48 |
|
49 val nxt_specify_ : ptree * (int list * pos_) -> calcstate'(*tests only*) |
|
50 val set_method : metID -> ptree * pos' -> ptree * ocalhd |
|
51 val set_problem : pblID -> ptree * pos' -> ptree * ocalhd |
|
52 val set_theory : thyID -> ptree * pos' -> ptree * ocalhd |
|
53 val step : pos' -> calcstate -> string * calcstate' |
|
54 val trymatch : pblID -> ptree -> pos' -> ptform |
|
55 val tryrefine : pblID -> ptree -> pos' -> ptform |
|
56 end |
|
57 |
|
58 |
|
59 |
|
60 (*------------------------------------------------------------------(**) |
|
61 structure MathEngine : MATHENGINE = |
|
62 struct |
|
63 (**)------------------------------------------------------------------*) |
|
64 |
|
65 fun get_pblID (pt, (p,_):pos') = |
|
66 let val p' = par_pblobj pt p |
|
67 val (_,pI,_) = get_obj g_spec pt p' |
|
68 val (_,(_,oI,_),_) = get_obj g_origin pt p' |
|
69 in if pI <> e_pblID then SOME pI |
|
70 else if oI <> e_pblID then SOME oI |
|
71 else NONE end; |
|
72 (*fun get_pblID (pt, (p,_):pos') = |
|
73 ((snd3 o (get_obj g_spec pt)) (par_pblobj pt p));*) |
|
74 |
|
75 |
|
76 (*--vvv--dummies for test*) |
|
77 val e_tac_ = Tac_ (Pure.thy,"","",""); |
|
78 datatype lOc_ = |
|
79 ERror of string (*after loc_specify, loc_solve*) |
|
80 | UNsafe of calcstate' (*after loc_specify, loc_solve*) |
|
81 | Updated of calcstate'; (*after loc_specify, loc_solve*) |
|
82 fun loc_specify_ m (pt,pos) = |
|
83 (* val pos = ip; |
|
84 *) |
|
85 let val (p,_,f,_,s,pt) = specify m pos [] pt; |
|
86 (* val (_,_,_,_,_,pt')= specify m pos [] pt; |
|
87 *) |
|
88 in case f of |
|
89 (Error' (Error_ e)) => ERror e |
|
90 | _ => Updated ([], [], (pt,p)) end; |
|
91 |
|
92 (*. TODO push return-value cs' into solve and rename solve->loc_solve?_? .*) |
|
93 (* val (m, pos) = ((mI,m), ip); |
|
94 val (m,(pt,pos) ) = ((mI,m), ptp); |
|
95 *) |
|
96 fun loc_solve_ m (pt,pos) = |
|
97 let val (msg, cs') = solve m (pt, pos); |
|
98 (* val (tacis,dels,(pt',p')) = cs'; |
|
99 (writeln o istate2str) (get_istate pt' p'); |
|
100 (term2str o fst) (get_obj g_result pt' (fst p')); |
|
101 *) |
|
102 in case msg of |
|
103 "ok" => Updated cs' |
|
104 | msg => ERror msg |
|
105 end; |
|
106 |
|
107 datatype nxt_ = |
|
108 HElpless (**) |
|
109 | Nexts of calcstate; (**) |
|
110 |
|
111 (*. locate a tactic in a script and apply it if possible .*) |
|
112 (*report applicability of tac in tacis; pt is dropped in setNextTactic*) |
|
113 fun locatetac _ (ptp as (_,([],Res))) = ("end-of-calculation", ([], [], ptp)) |
|
114 (* val ptp as (pt, p) = (pt, p); |
|
115 val ptp as (pt, p) = (pt, ip); |
|
116 *) |
|
117 | locatetac tac (ptp as (pt, p)) = |
|
118 let val (mI,m) = mk_tac'_ tac; |
|
119 in case applicable_in p pt m of |
|
120 Notappl e => ("not-applicable", ([],[], ptp):calcstate') |
|
121 | Appl m => |
|
122 (* val Appl m = applicable_in p pt m; |
|
123 *) |
|
124 let val x = if member op = specsteps mI |
|
125 then loc_specify_ m ptp else loc_solve_ (mI,m) ptp |
|
126 in case x of |
|
127 ERror e => ("failure", ([], [], ptp)) |
|
128 (*FIXXXXXME: loc_specify_, loc_solve_ TOGETHER with dropping meOLD+detail.sml*) |
|
129 | UNsafe cs' => ("unsafe-ok", cs') |
|
130 | Updated (cs' as (_,_,(_,p'))) => |
|
131 (*ev.SEVER.tacs like Begin_Trans*) |
|
132 (if p' = ([],Res) then "end-of-calculation" else "ok", |
|
133 cs')(*for -"- user to ask ? *) |
|
134 end |
|
135 end; |
|
136 |
|
137 |
|
138 (*------------------------------------------------------------------ |
|
139 fun init_detail ptp = e_calcstate;(*15.8.03.MISSING-->solve.sml!?*) |
|
140 (*----------------------------------------------------from solve.sml*) |
|
141 | nxt_solv (Detail_Set'(thy', rls, t)) (pt, p) = |
|
142 let (*val rls = the (assoc(!ruleset',rls')) |
|
143 handle _ => raise error ("solve: '"^rls'^"' not known");*) |
|
144 val thy = assoc_thy thy'; |
|
145 val (srls, sc, is) = |
|
146 case rls of |
|
147 Rrls {scr=sc as Rfuns {init_state=ii,...},...} => |
|
148 (e_rls, sc, RrlsState (ii t)) |
|
149 | Rls {srls=srls,scr=sc as Script s,...} => |
|
150 (srls, sc, ScrState ([(one_scr_arg s,t)], [], |
|
151 NONE, e_term, Sundef, true)); |
|
152 val pt = update_tac pt (fst p) (Detail_Set (id_rls rls)); |
|
153 val (p,cid,_,pt) = generate1 thy (Begin_Trans' t) is p pt; |
|
154 val nx = (tac_2tac o fst3) (next_tac (thy',srls) (pt,p) sc is); |
|
155 val aopt = applicable_in p pt nx; |
|
156 in case aopt of |
|
157 Notappl s => raise error ("solve Detail_Set: "^s) |
|
158 (* val Appl m = aopt; |
|
159 *) |
|
160 | Appl m => solve ("discardFIXME",m) p pt end |
|
161 ------------------------------------------------------------------*) |
|
162 |
|
163 |
|
164 (*iterated by nxt_me; there (the resulting) ptp dropped |
|
165 may call nxt_solve Apply_Method --- thus evaluated here after solve.sml*) |
|
166 (* val (ptp as (pt, pos as (p,p_))) = ptp; |
|
167 val (ptp as (pt, pos as (p,p_))) = (pt,ip); |
|
168 *) |
|
169 fun nxt_specify_ (ptp as (pt, pos as (p,p_))) = |
|
170 let val pblobj as (PblObj{meth,origin=origin as (oris,(dI',pI',mI'),_), |
|
171 probl,spec=(dI,pI,mI),...}) = get_obj I pt p; |
|
172 in if just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin |
|
173 then case mI' of |
|
174 ["no_met"] => nxt_specif (Refine_Tacitly pI') (pt, (p, Pbl)) |
|
175 | _ => nxt_specif Model_Problem (pt, (p,Pbl)) |
|
176 else let val cpI = if pI = e_pblID then pI' else pI; |
|
177 val cmI = if mI = e_metID then mI' else mI; |
|
178 val {ppc,prls,where_,...} = get_pbt cpI; |
|
179 val pre = check_preconds "thy 100820" prls where_ probl; |
|
180 val pb = foldl and_ (true, map fst pre); |
|
181 (*FIXME.WN0308: ~~~~~: just check true in itms of pbl/met?*) |
|
182 val (_,tac) = |
|
183 nxt_spec p_ pb oris (dI',pI',mI') (probl, meth) |
|
184 (ppc, (#ppc o get_met) cmI) (dI, pI, mI); |
|
185 in case tac of |
|
186 Apply_Method mI => |
|
187 (* val Apply_Method mI = tac; |
|
188 *) |
|
189 nxt_solv (Apply_Method' (mI, NONE, e_istate)) e_istate ptp |
|
190 | _ => nxt_specif tac ptp end |
|
191 end; |
|
192 |
|
193 |
|
194 (*.specify a new method; |
|
195 WN0512 impl.incomplete, see 'nxt_specif (Specify_Method ' .*) |
|
196 fun set_method (mI:metID) ptp = |
|
197 let val ([(_, Specify_Method' (_, _, mits), _)], [], (pt, pos as (p,_))) = |
|
198 nxt_specif (Specify_Method mI) ptp |
|
199 val pre = [] (*...from Specify_Method'*) |
|
200 val complete = true (*...from Specify_Method'*) |
|
201 (*from Specify_Method' ? vvv, vvv ?*) |
|
202 val PblObj {origin = (_,_,hdf), spec,...} = get_obj I pt p |
|
203 in (pt, (complete, Met, hdf, mits, pre, spec):ocalhd) end; |
|
204 |
|
205 (* val ([(_, Specify_Method' (_, _, mits), _)], [],_) = |
|
206 nxt_specif (Specify_Method mI) ptp; |
|
207 *) |
|
208 |
|
209 (*.specify a new problem; |
|
210 WN0512 impl.incomplete, see 'nxt_specif (Specify_Problem ' .*) |
|
211 (* val (pI, ptp) = (pI, (pt, ip)); |
|
212 *) |
|
213 fun set_problem pI (ptp: ptree * pos') = |
|
214 let val ([(_, Specify_Problem' (_, (complete, (pits, pre))),_)], |
|
215 _, (pt, pos as (p,_))) = nxt_specif (Specify_Problem pI) ptp |
|
216 (*from Specify_Problem' ? vvv, vvv ?*) |
|
217 val PblObj {origin = (_,_,hdf), spec,...} = get_obj I pt p |
|
218 in (pt, (complete, Pbl, hdf, pits, pre, spec):ocalhd) end; |
|
219 |
|
220 fun set_theory (tI:thyID) (ptp: ptree * pos') = |
|
221 let val ([(_, Specify_Problem' (_, (complete, (pits, pre))),_)], |
|
222 _, (pt, pos as (p,_))) = nxt_specif (Specify_Theory tI) ptp |
|
223 (*from Specify_Theory' ? vvv, vvv ?*) |
|
224 val PblObj {origin = (_,_,hdf), spec,...} = get_obj I pt p |
|
225 in (pt, (complete, Pbl, hdf, pits, pre, spec):ocalhd) end; |
|
226 |
|
227 (*.does a step forward; returns tactic used, ctree updated. |
|
228 TODO.WN0512 redesign after specify-phase became more separated from solve-phase |
|
229 arg ip: |
|
230 calcstate |
|
231 .*) |
|
232 (* val (ip as (_,p_), (ptp as (pt,p), tacis)) = (get_pos 1 1, get_calc 1); |
|
233 val (ip as (_,p_), (ptp as (pt,p), tacis)) = (pos, cs); |
|
234 val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'),[])); |
|
235 val (ip as (_,p_), (ptp as (pt,p), tacis)) = (ip,cs); |
|
236 *) |
|
237 fun step ((ip as (_,p_)):pos') ((ptp as (pt,p), tacis):calcstate) = |
|
238 let val pIopt = get_pblID (pt,ip); |
|
239 in if (*p = ([],Res) orelse*) ip = ([],Res) |
|
240 then ("end-of-calculation",(tacis, [], ptp):calcstate') else |
|
241 case tacis of |
|
242 (_::_) => |
|
243 (* val((tac,_,_)::_) = tacis; |
|
244 *) |
|
245 if ip = p (*the request is done where ptp waits for*) |
|
246 then let val (pt',c',p') = generate tacis (pt,[],p) |
|
247 in ("ok", (tacis, c', (pt', p'))) end |
|
248 else (case (if member op = [Pbl,Met] p_ |
|
249 then nxt_specify_ (pt,ip) else nxt_solve_ (pt,ip)) |
|
250 handle _ => ([],[],ptp)(*e.g.by Add_Given "equality///"*) |
|
251 of cs as ([],_,_) => ("helpless", cs) |
|
252 | cs => ("ok", cs)) |
|
253 (* val [] = tacis; |
|
254 *) |
|
255 | _ => (case pIopt of |
|
256 NONE => ("no-fmz-spec", ([], [], ptp)) |
|
257 | SOME pI => |
|
258 (* val SOME pI = pIopt; |
|
259 val cs=(if member op = [Pbl,Met] p_ andalso is_none(get_obj g_env pt (fst p)) |
|
260 then nxt_specify_ (pt,ip) else nxt_solve_ (pt,ip)) |
|
261 handle _ => ([], ptp); |
|
262 *) |
|
263 (case (if member op = [Pbl,Met] p_ |
|
264 andalso is_none (get_obj g_env pt (fst p)) |
|
265 (*^^^^^^^^: Apply_Method without init_form*) |
|
266 then nxt_specify_ (pt,ip) else nxt_solve_ (pt,ip) ) |
|
267 handle _ => ([],[],ptp)(*e.g.by Add_Giv"equality/"*) |
|
268 of cs as ([],_,_) =>("helpless", cs)(*FIXXMEdel.handle*) |
|
269 | cs => ("ok", cs))) |
|
270 end; |
|
271 |
|
272 (* (nxt_solve_ (pt,ip)) handle e => print_exn e ; |
|
273 |
|
274 *) |
|
275 |
|
276 |
|
277 |
|
278 |
|
279 (*.does several steps within one calculation as given by "type auto"; |
|
280 the steps may arbitrarily go into and leave different phases, |
|
281 i.e. specify-phase and solve-phase.*) |
|
282 (*TODO.WN0512 ? redesign after the phases have been more separated |
|
283 at the fron-end in 05: |
|
284 eg. CompleteCalcHead could be done by a separate fun !!!*) |
|
285 (* val (ip, cs as (ptp as (pt,p),tacis)) = (get_pos cI 1, get_calc cI); |
|
286 val (ip, cs as (ptp as (pt,p),tacis)) = (pold, get_calc cI); |
|
287 val (c, ip, cs as (ptp as (_,p),tacis), Step s) = |
|
288 ([]:pos' list, pold, get_calc cI, auto); |
|
289 *) |
|
290 fun autocalc c ip (cs as (ptp as (_,p),tacis)) (Step s) = |
|
291 if s <= 1 |
|
292 then let val (str, (_, c', ptp)) = step ip cs;(*1*) |
|
293 (*at least does 1 step, ev.1 too much*) |
|
294 in (str, c@c', ptp) end |
|
295 else let val (str, (_, c', ptp as (_, p))) = step ip cs; |
|
296 in if str = "ok" |
|
297 then autocalc (c@c') p (ptp,[]) (Step (s-1)) |
|
298 else (str, c@c', ptp) end |
|
299 (*handles autoord <= 3, autoord > 3 handled by all_/complete_solve*) |
|
300 | autocalc c (pos as (_,p_)) ((pt,_), _(*tacis would help 1x in solve*))auto= |
|
301 (* val (c:pos' list, (pos as (_,p_)),((pt,_),_),auto) = |
|
302 ([], pold, get_calc cI, auto); |
|
303 *) |
|
304 if autoord auto > 3 andalso just_created (pt, pos) |
|
305 then let val ptp = all_modspec (pt, pos); |
|
306 in all_solve auto c ptp end |
|
307 else |
|
308 if member op = [Pbl, Met] p_ |
|
309 then if not (is_complete_mod (pt, pos)) |
|
310 then let val ptp = complete_mod (pt, pos) |
|
311 in if autoord auto < 3 then ("ok", c, ptp) |
|
312 else |
|
313 if not (is_complete_spec ptp) |
|
314 then let val ptp = complete_spec ptp |
|
315 in if autoord auto = 3 then ("ok", c, ptp) |
|
316 else all_solve auto c ptp |
|
317 end |
|
318 else if autoord auto = 3 then ("ok", c, ptp) |
|
319 else all_solve auto c ptp |
|
320 end |
|
321 else |
|
322 if not (is_complete_spec (pt,pos)) |
|
323 then let val ptp = complete_spec (pt, pos) |
|
324 in if autoord auto = 3 then ("ok", c, ptp) |
|
325 else all_solve auto c ptp |
|
326 end |
|
327 else if autoord auto = 3 then ("ok", c, (pt, pos)) |
|
328 else all_solve auto c (pt, pos) |
|
329 else complete_solve auto c (pt, pos); |
|
330 (* val pbl = get_obj g_pbl (fst ptp) []; |
|
331 val (oris,_,_) = get_obj g_origin (fst ptp) []; |
|
332 *) |
|
333 |
|
334 |
|
335 |
|
336 |
|
337 |
|
338 (*.initialiye matching; before 'tryMatch' get the pblID to match with: |
|
339 if no pbl has been specified, take the init from origin.*) |
|
340 (*fun initmatch pt (pos as (p,_):pos') = |
|
341 let val PblObj {probl,origin=(os,(_,pI,_),_),spec=(dI',pI',mI'),...} = |
|
342 get_obj I pt p |
|
343 val pblID = if pI' = e_pblID |
|
344 then (*TODO.WN051125 (#init o get_pbt) pI <<<*) |
|
345 takelast (2, pI) (*FIXME.WN051125 a hack, impl.^^^*) |
|
346 else pI' |
|
347 val spec = (dI',pblID,mI') |
|
348 val {ppc,where_,prls,...} = get_pbt pblID |
|
349 val (model_ok, (pbl, pre)) = |
|
350 match_itms_oris (assoc_thy "Isac.thy") probl (ppc,where_,prls) os |
|
351 in ModSpec (ocalhd_complete pbl pre spec, |
|
352 Pbl, e_term, pbl, pre, spec) end;*) |
|
353 fun initcontext_pbl pt (pos as (p,_):pos') = |
|
354 let val PblObj {probl,origin=(os,(_,pI,_),hdl),spec=(dI',pI',mI'),...} = |
|
355 get_obj I pt p |
|
356 val pblID = if pI' = e_pblID |
|
357 then (*TODO.WN051125 (#init o get_pbt) pI <<<*) |
|
358 takelast (2, pI) (*FIXME.WN051125 a hack, impl.^^^*) |
|
359 else pI' |
|
360 val {ppc,where_,prls,...} = get_pbt pblID |
|
361 val (model_ok, (pbl, pre)) = |
|
362 match_itms_oris (assoc_thy "Isac.thy") probl (ppc,where_,prls) os |
|
363 in (model_ok, pblID, hdl, pbl, pre) end; |
|
364 |
|
365 fun initcontext_met pt (pos as (p,_):pos') = |
|
366 let val PblObj {meth,origin=(os,(_,_,mI), _),spec=(_, _, mI'),...} = |
|
367 get_obj I pt p |
|
368 val metID = if mI' = e_metID |
|
369 then (*TODO.WN051125 (#init o get_pbt) pI <<<*) |
|
370 takelast (2, mI) (*FIXME.WN051125 a hack, impl.^^^*) |
|
371 else mI' |
|
372 val {ppc,pre,prls,scr,...} = get_met metID |
|
373 val (model_ok, (pbl, pre)) = |
|
374 match_itms_oris (assoc_thy "Isac.thy") meth (ppc,pre,prls) os |
|
375 in (model_ok, metID, scr, pbl, pre) end; |
|
376 |
|
377 (*.match the model of a problem at pos p |
|
378 with the model-pattern of the problem with pblID*) |
|
379 fun context_pbl pI pt (p:pos) = |
|
380 let val PblObj {probl,origin=(os,_,hdl),...} = get_obj I pt p |
|
381 val {ppc,where_,prls,...} = get_pbt pI |
|
382 val (model_ok, (pbl, pre)) = |
|
383 match_itms_oris (assoc_thy "Isac.thy") probl (ppc,where_,prls) os |
|
384 in (model_ok, pI, hdl, pbl, pre) end; |
|
385 |
|
386 fun context_met mI pt (p:pos) = |
|
387 let val PblObj {meth,origin=(os,_,hdl),...} = get_obj I pt p |
|
388 val {ppc,pre,prls,scr,...} = get_met mI |
|
389 val (model_ok, (pbl, pre)) = |
|
390 match_itms_oris (assoc_thy "Isac.thy") meth (ppc,pre,prls) os |
|
391 in (model_ok, mI, scr, pbl, pre) end |
|
392 |
|
393 |
|
394 (* val (pI, pt, pos as (p,_)) = (pblID, pt, p); |
|
395 *) |
|
396 fun tryrefine pI pt (pos as (p,_):pos') = |
|
397 let val PblObj {probl,origin=(os,_,hdl),...} = get_obj I pt p |
|
398 in case refine_pbl (assoc_thy "Isac.thy") pI probl of |
|
399 NONE => (*copy from context_pbl*) |
|
400 let val {ppc,where_,prls,...} = get_pbt pI |
|
401 val (_, (pbl, pre)) = match_itms_oris (assoc_thy "Isac.thy") |
|
402 probl (ppc,where_,prls) os |
|
403 in (false, pI, hdl, pbl, pre) end |
|
404 | SOME (pI, (pbl, pre)) => |
|
405 (true, pI, hdl, pbl, pre) |
|
406 end; |
|
407 |
|
408 (* val (pt, (pos as (p,p_):pos')) = (pt, ip); |
|
409 *) |
|
410 fun detailstep pt (pos as (p,p_):pos') = |
|
411 let val nd = get_nd pt p |
|
412 val cn = children nd |
|
413 in if null cn |
|
414 then if (is_rewset o (get_obj g_tac nd)) [(*root of nd*)] |
|
415 then detailrls pt pos |
|
416 else ("no-Rewrite_Set...", EmptyPtree, e_pos') |
|
417 else ("donesteps", pt(*, get_formress [] ((lev_on o lev_dn) p) cn*), |
|
418 (p @ [length (children (get_nd pt p))], Res) ) |
|
419 end; |
|
420 |
|
421 |
|
422 |
|
423 (***. for mathematics authoring on sml-toplevel; no XML .***) |
|
424 |
|
425 type NEW = int list; |
|
426 (* val sp = (dI',pI',mI'); |
|
427 *) |
|
428 |
|
429 (*15.8.03 for me with loc_specify/solve, nxt_specify/solve |
|
430 delete as soon as TESTg_form -> _mout_ dropped*) |
|
431 fun TESTg_form ptp = |
|
432 (* val ptp = (pt,p); |
|
433 *) |
|
434 let val (form,_,_) = pt_extract ptp |
|
435 in case form of |
|
436 Form t => Form' (FormKF (~1,EdUndef,0,Nundef,term2str t)) |
|
437 | ModSpec (_,p_, head, gfr, pre, _) => |
|
438 Form' (PpcKF (0,EdUndef,0,Nundef, |
|
439 (case p_ of Pbl => Problem[] | Met => Method[], |
|
440 itms2itemppc (assoc_thy"Isac.thy") gfr pre))) |
|
441 end; |
|
442 |
|
443 (*.create a calc-tree; for use within sml: thus ^^^ NOT decoded to ^; |
|
444 compare "fun CalcTree" which DOES decode.*) |
|
445 fun CalcTreeTEST [(fmz, sp):fmz] = |
|
446 (* val [(fmz, sp):fmz] = [(fmz, (dI',pI',mI'))]; |
|
447 val [(fmz, sp):fmz] = [([], ("e_domID", ["e_pblID"], ["e_metID"]))]; |
|
448 *) |
|
449 let val cs as ((pt,p), tacis) = nxt_specify_init_calc (fmz, sp) |
|
450 val tac = case tacis of [] => Empty_Tac | _ => (#1 o hd) tacis |
|
451 val f = TESTg_form (pt,p) |
|
452 in (p, []:NEW, f, (tac2IDstr tac, tac), Sundef, pt) end; |
|
453 |
|
454 (*for tests > 15.8.03 after separation setnexttactic / nextTac: |
|
455 external view: me should be used by math-authors as done so far |
|
456 internal view: loc_specify/solve, nxt_specify/solve used |
|
457 i.e. same as in setnexttactic / nextTac*) |
|
458 (*ENDE TESTPHASE 08/10.03: |
|
459 NEW loeschen, eigene Version von locatetac, step |
|
460 meNEW, CalcTreeTEST: tac'_ -replace-> tac, remove [](cid) *) |
|
461 |
|
462 (* val ((_,tac), p, _, pt) = (nxt, p, c, pt); |
|
463 *) |
|
464 fun me ((_,tac):tac'_) (p:pos') (_:NEW(*remove*)) (pt:ptree) = |
|
465 let val (pt, p) = |
|
466 (* val (msg, (tacis, pos's, (pt',p'))) = locatetac tac (pt,p); |
|
467 p = ([1, 9], Res); |
|
468 (writeln o istate2str) (get_istate pt p); |
|
469 *) |
|
470 (*locatetac is here for testing by me; step would suffice in me*) |
|
471 case locatetac tac (pt,p) of |
|
472 ("ok", (_, _, ptp)) => ptp |
|
473 | ("unsafe-ok", (_, _, ptp)) => ptp |
|
474 | ("not-applicable",_) => (pt, p) |
|
475 | ("end-of-calculation", (_, _, ptp)) => ptp |
|
476 | ("failure",_) => raise error "sys-error"; |
|
477 val (_, ts) = |
|
478 (* val (eee, (ts, _, (pt'',_))) = step p ((pt, e_pos'),[]); |
|
479 *) |
|
480 (case step p ((pt, e_pos'),[]) of |
|
481 ("ok", (ts as (tac,_,_)::_, _, _)) => ("",ts) |
|
482 | ("helpless",_) => ("helpless: cannot propose tac", []) |
|
483 | ("no-fmz-spec",_) => raise error "no-fmz-spec" |
|
484 | ("end-of-calculation", (ts, _, _)) => ("",ts)) |
|
485 handle _ => raise error "sys-error"; |
|
486 val tac = case ts of tacis as (_::_) => |
|
487 (* val tacis as (_::_) = ts; |
|
488 *) |
|
489 let val (tac,_,_) = last_elem tacis |
|
490 in tac end |
|
491 | _ => if p = ([],Res) then End_Proof' |
|
492 else Empty_Tac; |
|
493 (*form output comes from locatetac*) |
|
494 in(p:pos',[]:NEW, TESTg_form (pt, p), |
|
495 (tac2IDstr tac, tac):tac'_, Sundef, pt) end; |
|
496 |
|
497 (*for quick test-print-out, until 'type inout' is removed*) |
|
498 fun f2str (Form' (FormKF (_, _, _, _, cterm'))) = cterm'; |
|
499 |
|
500 |
|
501 |
|
502 (*------------------------------------------------------------------(**) |
|
503 end |
|
504 open MathEngine; |
|
505 (**)------------------------------------------------------------------*) |
|
506 |