1 (* solve an example by interpreting a method's script
2 (c) Walther Neuper 1999
4 use"~/proto2/isac/src/sml/ME/solve.sml";
7 fun safe (ScrState (_,_,_,_,s,_)) = s
8 | safe (RrlsState _) = Safe;
11 type tac'_ = mstID * tac; (*DG <-> ME*)
12 val e_tac'_ = ("Empty_Tac", Empty_Tac):tac'_;
14 fun mk_tac'_ m = case m of
15 Init_Proof (ppc, spec) => ("Init_Proof", Init_Proof (ppc, spec ))
16 | Model_Problem pblID => ("Model_Problem", Model_Problem pblID)
17 | Refine_Tacitly pblID => ("Refine_Tacitly", Refine_Tacitly pblID)
18 | Refine_Problem pblID => ("Refine_Problem", Refine_Problem pblID)
19 | Add_Given cterm' => ("Add_Given", Add_Given cterm')
20 | Del_Given cterm' => ("Del_Given", Del_Given cterm')
21 | Add_Find cterm' => ("Add_Find", Add_Find cterm')
22 | Del_Find cterm' => ("Del_Find", Del_Find cterm')
23 | Add_Relation cterm' => ("Add_Relation", Add_Relation cterm')
24 | Del_Relation cterm' => ("Del_Relation", Del_Relation cterm')
26 | Specify_Theory domID => ("Specify_Theory", Specify_Theory domID)
27 | Specify_Problem pblID => ("Specify_Problem", Specify_Problem pblID)
28 | Specify_Method metID => ("Specify_Method", Specify_Method metID)
29 | Apply_Method metID => ("Apply_Method", Apply_Method metID)
30 | Check_Postcond pblID => ("Check_Postcond", Check_Postcond pblID)
31 | Free_Solve => ("Free_Solve",Free_Solve)
33 | Rewrite_Inst (subs, thm') => ("Rewrite_Inst", Rewrite_Inst (subs, thm'))
34 | Rewrite thm' => ("Rewrite", Rewrite thm')
35 | Rewrite_Asm thm' => ("Rewrite_Asm", Rewrite_Asm thm')
36 | Rewrite_Set_Inst (subs, rls')
37 => ("Rewrite_Set_Inst", Rewrite_Set_Inst (subs, rls'))
38 | Rewrite_Set rls' => ("Rewrite_Set", Rewrite_Set rls')
39 | End_Ruleset => ("End_Ruleset", End_Ruleset)
41 | End_Detail => ("End_Detail", End_Detail)
42 | Detail_Set rls' => ("Detail_Set", Detail_Set rls')
43 | Detail_Set_Inst (s, rls') => ("Detail_Set_Inst", Detail_Set_Inst (s, rls'))
45 | Calculate op_ => ("Calculate", Calculate op_)
46 | Substitute sube => ("Substitute", Substitute sube)
47 | Apply_Assumption cts' => ("Apply_Assumption", Apply_Assumption cts')
49 | Take cterm' => ("Take", Take cterm')
50 | Take_Inst cterm' => ("Take_Inst", Take_Inst cterm')
51 | Group (con, ints) => ("Group", Group (con, ints))
52 | Subproblem (domID, pblID) => ("Subproblem", Subproblem (domID, pblID))
54 | Subproblem_Full(spec,cts')=> ("Subproblem_Full", Subproblem_Full(spec,cts'))
56 | End_Subproblem => ("End_Subproblem",End_Subproblem)
57 | CAScmd cterm' => ("CAScmd", CAScmd cterm')
59 | Split_And => ("Split_And", Split_And)
60 | Conclude_And => ("Conclude_And", Conclude_And)
61 | Split_Or => ("Split_Or", Split_Or)
62 | Conclude_Or => ("Conclude_Or", Conclude_Or)
63 | Begin_Trans => ("Begin_Trans", Begin_Trans)
64 | End_Trans => ("End_Trans", End_Trans)
65 | Begin_Sequ => ("Begin_Sequ", Begin_Sequ)
66 | End_Sequ => ("End_Sequ", Begin_Sequ)
67 | Split_Intersect => ("Split_Intersect", Split_Intersect)
68 | End_Intersect => ("End_Intersect", End_Intersect)
69 | Check_elementwise cterm' => ("Check_elementwise", Check_elementwise cterm')
70 | Or_to_List => ("Or_to_List", Or_to_List)
71 | Collect_Trues => ("Collect_Results", Collect_Trues)
73 | Empty_Tac => ("Empty_Tac",Empty_Tac)
74 | Tac string => ("Tac",Tac string)
75 | User => ("User",User)
76 | End_Proof' => ("End_Proof'",End_Proof');
79 val empty_tac'_ = (mk_tac'_ Empty_Tac):tac'_;
81 fun mk_tac ((_,m):tac'_) = m;
82 fun mk_mstID ((mI,_):tac'_) = mI;
84 fun tac'_2str ((ID,ms):tac'_) = ID ^ (tac2str ms);
85 (* TODO: tac2str, tac'_2str NOT tested *)
89 type squ = ptree; (* TODO: safe etc. *)
91 (*13.9.02--------------
92 type ctr = (loc * pos) list;
93 val ops = [("plus","op +"),("minus","op -"),("times","op *"),
94 ("cancel","cancel"),("pow","pow"),("sqrt","sqrt")];
96 case assoc (ops,op_) of
97 Some op' => op' | None => raise error ("op_intern: no op= "^op_);
98 -----------------------*)
102 (* use"ME/solve.sml";
105 val ttt = (term_of o the o (parse thy))"Substitute [(bdv,x)] g";
106 val ttt = (term_of o the o (parse thy))"Rewrite thmid True g";
108 Const ("Script.Rewrite'_Inst",_) $ sub $ Free (thm',_) $ Const (pa,_) $ f'
113 val specsteps = ["Init_Proof","Refine_Tacitly","Refine_Problem",
114 "Model_Problem",(*"Match_Problem",*)
115 "Add_Given","Del_Given","Add_Find","Del_Find",
116 "Add_Relation","Del_Relation",
117 "Specify_Theory","Specify_Problem","Specify_Method"];
119 "-----------------------------------------------------------------------";
122 fun step2taci ((tac_, _, pt, p, _):step) = (*FIXXME.040312: redesign step*)
123 (tac_2tac tac_, tac_, (p, get_istate pt p)):taci;
126 (*FIXME.WN050821 compare solve ... nxt_solv*)
127 (* val ("Apply_Method",Apply_Method' (mI,_))=(mI,m);
128 val (("Apply_Method",Apply_Method' (mI,_,_)),pt, pos as (p,_))=(m,pt, pos);
130 fun solve ("Apply_Method", m as Apply_Method' (mI, _, _))
131 (pt:ptree, (pos as (p,_))) =
132 let val {srls,...} = get_met mI;
133 val PblObj{meth=itms,...} = get_obj I pt p;
134 val thy' = get_obj g_domID pt p;
135 val thy = assoc_thy thy';
136 val (is as ScrState (env,_,_,_,_,_), sc) = init_scrstate thy itms mI;
137 val ini = init_form thy sc env;
141 Some t => (* val Some t = ini;
143 let val (pos,c,_,pt) =
144 generate1 thy (Apply_Method' (mI, Some t, is))
145 is (lev_on p, Frm)(*implicit Take*) pt;
146 in ("ok",([(Apply_Method mI, Apply_Method' (mI, Some t, is),
147 ((lev_on p, Frm), is))], c, (pt,pos)):calcstate')
149 | None => (*execute the first tac in the Script, compare solve m*)
150 let val (m', is', _) = next_tac (thy', srls) (pt, (p, Res)) sc is;
151 val d = e_rls (*FIXME: get simplifier from domID*);
153 case locate_gen (thy',srls) m' (pt,(p, Res))(sc,d) is' of
154 Steps (is'', ss as (m'',f',pt',p',c')::_) =>
155 (* val Steps (is'', ss as (m'',f',pt',p',c')::_) =
156 locate_gen (thy',srls) m' (pt,(p,Res)) (sc,d) is';
158 ("ok", (map step2taci ss, c', (pt',p')))
160 let val (p,ps,f,pt) =
161 generate_hard (assoc_thy "Isac.thy") m (p,Frm) pt;
162 in ("not-found-in-script",
163 ([(tac_2tac m, m, (pos, is))], ps, (pt,p))) end
164 (*just-before------------------------------------------------------
165 ("ok",([(Apply_Method mI,Apply_Method'(mI,None,e_istate),
167 [], (update_env pt (fst pos) (Some is),pos)))
168 -----------------------------------------------------------------*)
172 | solve ("Free_Solve", Free_Solve') (pt,po as (p,_)) =
173 let (*val _=writeln"###solve Free_Solve";*)
174 val p' = lev_dn_ (p,Res);
175 val pt = update_metID pt (par_pblobj pt p) e_metID;
176 in ("ok", ((*(p',Uistate,Empty_Tac_), EmptyMout, Empty_Tac, Unsafe,*)
177 [(Empty_Tac, Empty_Tac_, (po, Uistate))], [], (pt,p'))) end
179 (* val (("Check_Postcond",Check_Postcond' (pI,_)), (pt,(pos as (p,p_)))) =
182 | solve ("Check_Postcond",Check_Postcond' (pI,_)) (pt,(pos as (p,p_))) =
183 let (*val _=writeln"###solve Check_Postcond";*)
184 val pp = par_pblobj pt p
185 val asm = (case get_obj g_tac pt p of
186 Check_elementwise _ => (*collects and instantiates asms*)
187 (snd o (get_obj g_result pt)) p
188 | _ => ((map fst) o (get_assumptions_ pt)) (p,p_))
189 handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*)
190 val metID = get_obj g_metID pt pp;
191 val {srls=srls,scr=sc,...} = get_met metID;
192 val is as ScrState (E,l,a,_,_,b) = get_istate pt (p,p_);
193 (*val _= writeln("### solve Check_postc, subpbl pos= "^(pos'2str (p,p_)));
194 val _= writeln("### solve Check_postc, is= "^(istate2str is));*)
195 val thy' = get_obj g_domID pt pp;
196 val thy = assoc_thy thy';
197 val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc is;
198 (*val _= writeln("### solve Check_postc, scval= "^(term2str scval));*)
201 let val is = ScrState (E,l,a,scval,scsaf,b)
202 val tac_ = Check_Postcond'(pI,(scval, map term2str asm))
203 val (pos,ps,f,pt) = generate1 thy tac_ is (pp,Res) pt;
204 in ("ok", ((*(([],Res),is,End_Proof''), f, End_Proof', scsaf,*)
205 [(Check_Postcond pI, tac_, ((pp,Res),is))], ps,(pt,pos))) end
208 (*resume script of parpbl, transfer value of subpbl-script*)
209 val ppp = par_pblobj pt (lev_up p);
210 val thy' = get_obj g_domID pt ppp;
211 val thy = assoc_thy thy';
212 val metID = get_obj g_metID pt ppp;
213 val sc = (#scr o get_met) metID;
214 val is as ScrState (E,l,a,_,_,b) = get_istate pt (pp(*!/p/*),Frm);
215 (*val _=writeln("### solve Check_postc, parpbl pos= "^(pos'2str(pp,Frm)));
216 val _=writeln("### solve Check_postc, is(pt)= "^(istate2str is));
217 val _=writeln("### solve Check_postc, is'= "^
218 (istate2str (E,l,a,scval,scsaf,b)));*)
219 val ((p,p_),ps,f,pt) =
220 generate1 thy (Check_Postcond' (pI, (scval, map term2str asm)))
221 (ScrState (E,l,a,scval,scsaf,b)) (pp,Res) pt;
222 (*val _=writeln("### solve Check_postc, is(pt')= "^
223 (istate2str (get_istate pt ([3],Res))));
224 val (nx,is',_) = next_tac (thy',srls) (pt,(p,p_)) sc
225 (ScrState (E,l,a,scval,scsaf,b));*)
226 in ("ok",(*((pp,Res),is',nx), f, tac_2tac nx, scsaf,*)
227 ([(Check_Postcond pI, Check_Postcond'(pI,(scval, map term2str asm)),
228 ((pp,Res), ScrState (E,l,a,scval,scsaf,b)))],ps,(pt,(p,p_))))
232 ("ok",([(Check_Postcond pI,Check_Postcond'(pI, (scval, map term2str asm))),
233 ((pp,Res),(ScrState (E,l,a,scval,scsaf,b)))], (pt,(p,p_))));
234 val (_,(pt',p')) = cs';
235 (writeln o istate2str) (get_istate pt' p');
236 (term2str o fst) (get_obj g_result pt' (fst p'));
239 (* writeln(istate2str(get_istate pt (p,p_)));
241 | solve (_,End_Proof'') (pt, (p,p_)) =
243 ((*(([],Res),Uistate,Empty_Tac_), EmptyMout, Empty_Tac, Safe,*)
244 [(Empty_Tac,Empty_Tac_,(([],Res),Uistate))],[],(pt,(p,p_))))
246 (*-----------vvvvvvvvvvv could be done by generate1 ?!?*)
247 | solve (_,End_Detail' t) (pt,(p,p_)) =
248 let val pr as (p',_) = (lev_up p, Res)
249 val pp = par_pblobj pt p
250 val r = (fst o (get_obj g_result pt)) p'
251 (*Rewrite_Set* done at Detail_Set*: this result is already in ptree*)
252 val thy' = get_obj g_domID pt pp
253 val (srls, is, sc) = from_pblobj' thy' pr pt
254 val (tac_,is',_) = next_tac (thy',srls) (pt,pr) sc is
255 in ("ok", ((*((pp,Frm(*???*)),is,tac_),
256 Form' (FormKF (~1, EdUndef, length p', Nundef, term2str r)),
257 tac_2tac tac_, Sundef,*)
258 [(End_Detail, End_Detail' t ,
259 ((p,p_), get_istate pt (p,p_)))], [], (pt,pr))) end
261 | solve (mI,m) (pt, po as (p,p_)) =
262 (* val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
264 if e_metID = get_obj g_metID pt (par_pblobj pt p)(*29.8.02:
265 could be detail, too !!*)
266 then let val ((p,p_),ps,f,pt) =
267 generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p)))
268 m e_istate (p,p_) pt;
269 in ("no-method-specified", (*Free_Solve*)
270 ((*((p,p_),Uistate,Empty_Tac_),f, Empty_Tac, Unsafe,*)
271 [(Empty_Tac,Empty_Tac_, ((p,p_),Uistate))], ps, (pt,(p,p_)))) end
274 val thy' = get_obj g_domID pt (par_pblobj pt p);
275 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
276 (*val _= writeln("### solve, before locate_gen p="^(pos'2str(p,p_)));*)
277 val d = e_rls; (*FIXME: canon.simplifier for domain is missing
278 8.01: generate from domID?*)
279 in case locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is of
280 Steps (is', ss as (m',f',pt',p',c')::_) =>
281 (* val Steps (is', ss as (m',f',pt',p',c')::_) =
282 locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is;
284 let (*val _= writeln("### solve, after locate_gen: is= ")
285 val _= writeln(istate2str is')*)
287 case p' of (*change from solve to model subpbl*)
288 (_,Pbl) => nxt_model_pbl m' (pt',p')
289 | _ => fst3 (next_tac (thy',srls) (pt',p') sc is');*)
290 (*27.8.02:next_tac may change to other branches in pt FIXXXXME*)
291 in ("ok", ((*(p',is',nxt_), f', tac_2tac nxt_, safe is',*)
292 map step2taci ss, c', (pt',p'))) end
294 let val (p,ps,f,pt) =
295 generate_hard (assoc_thy "Isac.thy") m (p,p_) pt;
296 in ("not-found-in-script",
297 ((*(p,Uistate,Empty_Tac_),f, Empty_Tac, Unsafe,*)
298 [(tac_2tac m, m, (po,is))], ps, (pt,p))) end
303 (*FIXME.WN050821 compare solve ... nxt_solv*)
304 (* nxt_solv (Apply_Method' vvv FIXME: get args in applicable_in *)
305 (*fun nxt_solv (Apply_Method' (mI,_,_)) _ (pt:ptree, pos as (p,_)) =
306 (* val ((Apply_Method' (mI,_,_)), _, (pt:ptree, pos as (p,_))) =
307 ((Apply_Method' (mI, None, e_istate)), e_istate, ptp);
309 let val {srls,ppc,...} = get_met mI;
310 val PblObj{meth=itms,origin=(oris,_,_),probl,...} = get_obj I pt p;
311 val itms = if itms <> [] then itms
312 else complete_metitms oris probl [] ppc
313 val thy' = get_obj g_domID pt p;
314 val thy = assoc_thy thy';
315 val (is as ScrState (env,_,_,_,_,_), scr) = init_scrstate thy itms mI;
316 val ini = init_form thy scr env;
320 Some t => (* val Some t = ini;
322 let val tac_ = Apply_Method' (mI, Some t, is);
323 val (pos,c,_,pt) = (*implicit Take*)
324 generate1 thy tac_ is (lev_on p,Frm) pt
325 (*val _= ("### nxt_solv Apply_Method, pos= "^pos'2str (lev_on p,Frm));*)
326 in ([(Apply_Method mI, tac_, ((lev_on p, Frm), is))],
327 c, (pt, pos)):calcstate' end
329 ([(Apply_Method mI, Apply_Method' (mI, None, e_istate), (pos, is))], [],
330 (update_env pt (fst pos) (Some is), pos))
334 (*FIXME.WN050821 compare solve ... nxt_solv*)
335 (* nxt_solv (Apply_Method' vvv FIXME: get args in applicable_in *)
336 fun nxt_solv (Apply_Method' (mI,_,_)) _ (pt:ptree, pos as (p,_)) =
337 (* val ((Apply_Method' (mI,_,_)), _, (pt:ptree, pos as (p,_))) =
338 ((Apply_Method' (mI, None, e_istate)), e_istate, ptp);
340 let val {srls,ppc,...} = get_met mI;
341 val PblObj{meth=itms,origin=(oris,_,_),probl,...} = get_obj I pt p;
342 val itms = if itms <> [] then itms
343 else complete_metitms oris probl [] ppc
344 val thy' = get_obj g_domID pt p;
345 val thy = assoc_thy thy';
346 val (is as ScrState (env,_,_,_,_,_), scr) = init_scrstate thy itms mI;
347 val ini = init_form thy scr env;
351 Some t => (* val Some t = ini;
353 let val pos = (lev_on p, Frm)
354 val tac_ = Apply_Method' (mI, Some t, is);
355 val (pos,c,_,pt) = (*implicit Take*)
356 generate1 thy tac_ is pos pt
357 (*val _= ("### nxt_solv Apply_Method, pos= "^pos'2str (lev_on p,Frm));*)
358 in ([(Apply_Method mI, tac_, (pos, is))],
359 c, (pt, pos)):calcstate' end
361 ([(Apply_Method mI, Apply_Method' (mI, None, e_istate), (pos, is))], [],
362 (update_env pt (fst pos) (Some is), pos))
365 (* val ("Check_Postcond",Check_Postcond' (pI,_)) = (mI,m);
366 val (Check_Postcond' (pI,_), _, (pt, pos as (p,p_))) =
369 (*TODO.WN050913 remove unnecessary code below*)
370 | nxt_solv (Check_Postcond' (pI,_)) _ (pt, pos as (p,p_)) =
371 let (*val _=writeln"###solve Check_Postcond";*)
372 val pp = par_pblobj pt p
373 val asm = (case get_obj g_tac pt p of
374 Check_elementwise _ => (*collects and instantiates asms*)
375 (snd o (get_obj g_result pt)) p
376 | _ => ((map fst) o (get_assumptions_ pt)) (p,p_))
377 handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*)
378 val metID = get_obj g_metID pt pp;
379 val {srls=srls,scr=sc,...} = get_met metID;
380 val is as ScrState (E,l,a,_,_,b) = get_istate pt (p,p_);
381 (*val _= writeln("### solve Check_postc, subpbl pos= "^(pos'2str (p,p_)));
382 val _= writeln("### solve Check_postc, is= "^(istate2str is));*)
383 val thy' = get_obj g_domID pt pp;
384 val thy = assoc_thy thy';
385 val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc is;
386 (*val _= writeln("### solve Check_postc, scval= "^(term2str scval));*)
388 let val is = ScrState (E,l,a,scval,scsaf,b)
389 val tac_ = Check_Postcond'(pI,(scval, map term2str asm))
390 (*val _= writeln"### nxt_solv2 Apply_Method: stored is =";
391 val _= writeln(istate2str is);*)
392 val ((p,p_),ps,f,pt) =
393 generate1 thy tac_ is (pp,Res) pt;
394 in ([(Check_Postcond pI, tac_, ((pp,Res), is))],ps,(pt, (p,p_))) end
397 (*resume script of parpbl, transfer value of subpbl-script*)
398 val ppp = par_pblobj pt (lev_up p);
399 val thy' = get_obj g_domID pt ppp;
400 val thy = assoc_thy thy';
401 val metID = get_obj g_metID pt ppp;
402 val {scr,...} = get_met metID;
403 val is as ScrState (E,l,a,_,_,b) = get_istate pt (pp(*!/p/*),Frm)
404 val tac_ = Check_Postcond' (pI, (scval, map term2str asm))
405 val is = ScrState (E,l,a,scval,scsaf,b)
406 (*val _= writeln"### nxt_solv3 Apply_Method: stored is =";
407 val _= writeln(istate2str is);*)
408 val ((p,p_),ps,f,pt) = generate1 thy tac_ is (pp, Res) pt;
409 (*val (nx,is',_) = next_tac (thy',srls) (pt,(p,p_)) scr is;WN050913*)
410 in ([(Check_Postcond pI, tac_, ((pp, Res), is))], ps, (pt, (p,p_))) end
412 (* writeln(istate2str(get_istate pt (p,p_)));
415 (*.start interpreter and do one rewrite.*)
416 (* val (_,Detail_Set'(thy',rls,t)) = (mI,m); val p = (p,p_);
417 solve ("",Detail_Set'(thy', rls, t)) p pt;
418 | nxt_solv (Detail_Set'(thy', rls, t)) _ (pt, p) = **********
419 ---> FE-interface/sml.sml
421 | nxt_solv (End_Detail' t) _ (pt, (p,p_)) = **********
422 let val pr as (p',_) = (lev_up p, Res)
423 val pp = par_pblobj pt p
424 val r = (fst o (get_obj g_result pt)) p'
425 (*Rewrite_Set* done at Detail_Set*: this result is already in ptree*)
426 val thy' = get_obj g_domID pt pp
427 val (srls, is, sc) = from_pblobj' thy' pr pt
428 val (tac_,is',_) = next_tac (thy',srls) (pt,pr) sc is
429 in (pr, ((pp,Frm(*???*)),is,tac_),
430 Form' (FormKF (~1, EdUndef, length p', Nundef, term2str r)),
431 tac_2tac tac_, Sundef, pt) end
433 | nxt_solv (End_Proof'') _ ptp = ([], [], ptp)
435 | nxt_solv tac_ is (pt, pos as (p,p_)) =
436 (* val (pt, pos as (p,p_)) = ptp;
438 let val pos = case pos of (p,Res) => (lev_on p,Res) | _ => pos
439 (*val _= writeln"### nxt_solv4 Apply_Method: stored is =";
440 val _= writeln(istate2str is);*)
441 val (pos',c,_,pt) = generate1 (assoc_thy "Isac.thy") tac_ is pos pt;
442 in ([(tac_2tac tac_, tac_, (pos,is))], c, (pt, pos')) end;
445 (*(p,p_), (([],Res),Uistate,Empty_Tac_), EmptyMout, Empty_Tac, Safe, pt*)
448 (*.find the next tac from the script, nxt_solv will update the ptree.*)
449 fun nxt_solve_ (ptp as (pt, pos as (p,p_))) =
450 (* val (pt,pos as (p,p_)) = ptp;
451 val (pt,pos as (p,p_)) = ptp';
452 val (pt,pos as (p,p_)) = ptp'';
453 val (ptp as (pt, pos as (p,p_))) = (pt,ip);
455 if e_metID = get_obj g_metID pt (par_pblobj pt p)
456 then ([], [], (pt,(p,p_))):calcstate'
457 else let val thy' = get_obj g_domID pt (par_pblobj pt p);
458 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
459 val (tac_,is,(t,_)) = next_tac (thy',srls) (pt,pos) sc is;
460 (*TODO here ^^^ return finished/helpless/ok !*)
461 (* val (tac_',is',_) = next_tac (thy',srls) (pt,pos) sc is;
464 End_Detail' _ => ([(End_Detail,
465 End_Detail' (t,[(*FIXME.040215*)]),
466 (pos, is))], [], (pt, pos))
467 | _ => nxt_solv tac_ is ptp end;
470 Step of int (*1 do #int steps; may stop in model/specify:
471 IS VERY INEFFICIENT IN MODEL/SPECIY*)
472 | CompleteModel (*2 complete modeling
473 if model complete, finish specifying + start solving*)
474 | CompleteCalcHead (*3 complete model/specify in one go + start solving*)
475 | CompleteToSubpbl (*4 stop at the next begin of a subproblem,
476 if none, complete the actual (sub)problem*)
477 | CompleteSubpbl (*5 complete the actual (sub)problem (incl.ev.subproblems)*)
478 | CompleteCalc; (*6 complete the calculation as a whole*)
479 fun autoord (Step _ ) = 1
480 | autoord CompleteModel = 2
481 | autoord CompleteCalcHead = 3
482 | autoord CompleteToSubpbl = 4
483 | autoord CompleteSubpbl = 5
484 | autoord CompleteCalc = 6;
485 (* val ptp as (_, p) = ptp;
486 val ptp as (_, p) = (pt, pos); val auto = CompleteSubpbl;
487 val (auto, ptp as (_, p)) = (CompleteSubpbl, (pt', pos'));
489 val (c, (ptp as (_, p))) = ((c@c'), ptp);
491 fun complete_solve auto c (ptp as (_, p): ptree * pos') =
492 if p = ([], Res) then ("end-of-calculation", [], ptp) else
493 case nxt_solve_ ptp of
494 ((Subproblem _, tac_, (_, is))::_, c', ptp') =>
495 (* val ptp' = ptp''';
497 if autoord auto < 5 then ("ok", c@c', ptp)
498 else let val ptp = all_modspec ptp';
499 val (_, c'', ptp) = all_solve auto (c@c') ptp;
500 in complete_solve auto (c@c'@c'') ptp end
501 | ((Check_Postcond _, tac_, (_, is))::_, c', ptp' as (_, p')) =>
502 if autoord auto < 6 orelse p' = ([],Res) then ("ok", c@c', ptp')
503 else complete_solve auto (c@c') ptp'
504 | ((End_Detail, _, _)::_, c', ptp') =>
505 if autoord auto < 6 then ("ok", c@c', ptp')
506 else complete_solve auto (c@c') ptp'
507 | (_, c', ptp') => complete_solve auto (c@c') ptp'
508 (* val (tacis, c', ptp') = nxt_solve_ ptp;
509 val (tacis, c', ptp'') = nxt_solve_ ptp';
510 val (tacis, c', ptp''') = nxt_solve_ ptp'';
511 val (tacis, c', ptp'''') = nxt_solve_ ptp''';
512 val (tacis, c', ptp''''') = nxt_solve_ ptp'''';
514 and all_solve auto c (ptp as (pt, (p,_)): ptree * pos') =
515 (* val (ptp as (pt, (p,_))) = ptp;
516 val (ptp as (pt, (p,_))) = ptp';
517 val (ptp as (pt, (p,_))) = (pt, pos);
519 let val (_,_,mI) = get_obj g_spec pt p;
520 val (_, c', ptp) = nxt_solv (Apply_Method' (mI, None, e_istate))
522 in complete_solve auto (c@c') ptp end;
525 (*. detail steps done internally by Rewrite_Set*
526 into ctree by use of a script .*)
529 fun detailrls pt ((p,p_):pos') =
530 let val t = get_obj g_form pt p
531 val is = init_istate (get_obj g_tac pt p)
532 val tac_ = Apply_Method' (e_metID(*WN.0402: see generate1 !?!*),
534 val pos' = ((lev_on o lev_dn) p, Frm);
535 val (_,_,_,pt') = (*implicit Take*) generate1 thy tac_ is pos' pt;
536 val (_, _, (pt'',_)) = complete_solve CompleteSubpbl [] (pt', pos');
537 val newnds =children (get_nd pt'' p)
538 val pt''' = ins_chn newnds pt p (*complete_solve cuts branches after*)
539 (*val nd = get_nd pt p; val cn = children nd;*)
540 in ("detailrls", pt'''(*, get_formress [] ((lev_on o lev_dn) p) cn*),
541 (p @ [length newnds], Res):pos') end;
545 (* val(mI,m)=m;val ppp=p;(*!!!*)val(p,p_)=pos;val(_,pt,_)=ppp(*!!!*);
546 get_form ((mI,m):tac'_) ((p,p_):pos') ppp;
548 fun get_form ((mI,m):tac'_) ((p,p_):pos') pt =
549 case applicable_in (p,p_) pt m of
550 Notappl e => Error' (Error_ e)
552 (* val Appl m=applicable_in (p,p_) pt m;
555 then let val (_,_,f,_,_,_) = specify m (p,p_) [] pt
557 else let val (*_,_,f,_,_,_*)_ = solve (mI,m) (pt,(p,p_))
558 in (*f*) EmptyMout end;