181 _, (pt, pos as (p,_))) = nxt_specif (Specify_Theory tI) ptp |
181 _, (pt, pos as (p,_))) = nxt_specif (Specify_Theory tI) ptp |
182 (*from Specify_Theory' ? vvv, vvv ?*) |
182 (*from Specify_Theory' ? vvv, vvv ?*) |
183 val PblObj {origin = (_,_,hdf), spec,...} = get_obj I pt p |
183 val PblObj {origin = (_,_,hdf), spec,...} = get_obj I pt p |
184 in (pt, (complete, Pbl, hdf, pits, pre, spec):ocalhd) end; |
184 in (pt, (complete, Pbl, hdf, pits, pre, spec):ocalhd) end; |
185 |
185 |
186 (*.does a step forward; returns tactic used, ctree updated. |
186 (* does a step forward; returns tactic used, ctree updated. |
187 TODO.WN0512 redesign after specify-phase became more separated from solve-phase |
187 TODO.WN0512 redesign after specify-phase became more separated from solve-phase *) |
188 arg ip: |
|
189 calcstate |
|
190 .*) |
|
191 (* val (ip as (_,p_), (ptp as (pt,p), tacis)) = (get_pos 1 1, get_calc 1); |
|
192 val (ip as (_,p_), (ptp as (pt,p), tacis)) = (pos, cs); |
|
193 val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'),[])); |
|
194 val (ip as (_,p_), (ptp as (pt,p), tacis)) = (ip,cs); |
|
195 *) |
|
196 fun step ((ip as (_,p_)):pos') ((ptp as (pt,p), tacis):calcstate) = |
188 fun step ((ip as (_,p_)):pos') ((ptp as (pt,p), tacis):calcstate) = |
197 let val pIopt = get_pblID (pt,ip); |
189 let val pIopt = get_pblID (pt,ip); |
198 in |
190 in |
199 if (*p = ([],Res) orelse*) ip = ([],Res) |
191 if (*p = ([],Res) orelse*) ip = ([],Res) |
200 then ("end-of-calculation",(tacis, [], ptp):calcstate') |
192 then ("end-of-calculation",(tacis, [], ptp):calcstate') |
221 handle _ => ([],[],ptp)(*e.g.by Add_Giv"equality///"*) of |
213 handle _ => ([],[],ptp)(*e.g.by Add_Giv"equality///"*) of |
222 cs as ([],_,_) =>("helpless", cs)(*FIXXMEdel.handle*) |
214 cs as ([],_,_) =>("helpless", cs)(*FIXXMEdel.handle*) |
223 | cs => ("ok", cs))) |
215 | cs => ("ok", cs))) |
224 end; |
216 end; |
225 |
217 |
226 (* (nxt_solve_ (pt,ip)) handle e => print_exn e ; |
|
227 |
|
228 *) |
|
229 |
|
230 |
|
231 |
|
232 |
|
233 (*.does several steps within one calculation as given by "type auto"; |
218 (*.does several steps within one calculation as given by "type auto"; |
234 the steps may arbitrarily go into and leave different phases, |
219 the steps may arbitrarily go into and leave different phases, |
235 i.e. specify-phase and solve-phase.*) |
220 i.e. specify-phase and solve-phase.*) |
236 (*TODO.WN0512 ? redesign after the phases have been more separated |
221 (*TODO.WN0512 ? redesign after the phases have been more separated |
237 at the fron-end in 05: |
222 at the fron-end in 05: |
238 eg. CompleteCalcHead could be done by a separate fun !!!*) |
223 eg. CompleteCalcHead could be done by a separate fun !!!*) |
239 (* val (ip, cs as (ptp as (pt,p),tacis)) = (get_pos cI 1, get_calc cI); |
|
240 val (ip, cs as (ptp as (pt,p),tacis)) = (pold, get_calc cI); |
|
241 val (c, ip, cs as (ptp as (_,p),tacis), Step s) = |
|
242 ([]:pos' list, pold, get_calc cI, auto); |
|
243 *) |
|
244 fun autocalc c ip (cs as (ptp as (_,p),tacis)) (Step s) = |
224 fun autocalc c ip (cs as (ptp as (_,p),tacis)) (Step s) = |
245 if s <= 1 |
225 if s <= 1 |
246 then let val (str, (_, c', ptp)) = step ip cs;(*1*) |
226 then let val (str, (_, c', ptp)) = step ip cs;(*1*) |
247 (*at least does 1 step, ev.1 too much*) |
227 (*at least does 1 step, ev.1 too much*) |
248 in (str, c@c', ptp) end |
228 in (str, c@c', ptp) end |
411 i.e. same as in setnexttactic / nextTac*) |
391 i.e. same as in setnexttactic / nextTac*) |
412 (*ENDE TESTPHASE 08/10.03: |
392 (*ENDE TESTPHASE 08/10.03: |
413 NEW loeschen, eigene Version von locatetac, step |
393 NEW loeschen, eigene Version von locatetac, step |
414 meNEW, CalcTreeTEST: tac'_ -replace-> tac, remove [](cid) *) |
394 meNEW, CalcTreeTEST: tac'_ -replace-> tac, remove [](cid) *) |
415 |
395 |
416 (* val ((_,tac), p, _, pt) = (nxt, p, c, pt); |
|
417 *) |
|
418 fun me ((_,tac):tac'_) (p:pos') (_:NEW(*remove*)) (pt:ptree) = |
396 fun me ((_,tac):tac'_) (p:pos') (_:NEW(*remove*)) (pt:ptree) = |
419 let |
397 let |
420 val (pt, p) = |
398 val (pt, p) = |
421 (*locatetac is here for testing by me; step would suffice in me*) |
399 (*locatetac is here for testing by me; step would suffice in me*) |
422 case locatetac tac (pt,p) of |
400 case locatetac tac (pt,p) of |