intermed. ctxt integration - assumptions now in context
1 (* solve an example by interpreting a method's script
2 (c) Walther Neuper 1999
8 fun safe (ScrState (_,_,_,_,s,_)) = s
9 | safe (RrlsState _) = Safe;
12 type tac'_ = mstID * tac; (*DG <-> ME*)
13 val e_tac'_ = ("Empty_Tac", Empty_Tac):tac'_;
15 fun mk_tac'_ m = case m of
16 Init_Proof (ppc, spec) => ("Init_Proof", Init_Proof (ppc, spec ))
17 | Model_Problem => ("Model_Problem", Model_Problem)
18 | Refine_Tacitly pblID => ("Refine_Tacitly", Refine_Tacitly pblID)
19 | Refine_Problem pblID => ("Refine_Problem", Refine_Problem pblID)
20 | Add_Given cterm' => ("Add_Given", Add_Given cterm')
21 | Del_Given cterm' => ("Del_Given", Del_Given cterm')
22 | Add_Find cterm' => ("Add_Find", Add_Find cterm')
23 | Del_Find cterm' => ("Del_Find", Del_Find cterm')
24 | Add_Relation cterm' => ("Add_Relation", Add_Relation cterm')
25 | Del_Relation cterm' => ("Del_Relation", Del_Relation cterm')
27 | Specify_Theory domID => ("Specify_Theory", Specify_Theory domID)
28 | Specify_Problem pblID => ("Specify_Problem", Specify_Problem pblID)
29 | Specify_Method metID => ("Specify_Method", Specify_Method metID)
30 | Apply_Method metID => ("Apply_Method", Apply_Method metID)
31 | Check_Postcond pblID => ("Check_Postcond", Check_Postcond pblID)
32 | Free_Solve => ("Free_Solve",Free_Solve)
34 | Rewrite_Inst (subs, thm') => ("Rewrite_Inst", Rewrite_Inst (subs, thm'))
35 | Rewrite thm' => ("Rewrite", Rewrite thm')
36 | Rewrite_Asm thm' => ("Rewrite_Asm", Rewrite_Asm thm')
37 | Rewrite_Set_Inst (subs, rls')
38 => ("Rewrite_Set_Inst", Rewrite_Set_Inst (subs, rls'))
39 | Rewrite_Set rls' => ("Rewrite_Set", Rewrite_Set rls')
40 | End_Ruleset => ("End_Ruleset", End_Ruleset)
42 | End_Detail => ("End_Detail", End_Detail)
43 | Detail_Set rls' => ("Detail_Set", Detail_Set rls')
44 | Detail_Set_Inst (s, rls') => ("Detail_Set_Inst", Detail_Set_Inst (s, rls'))
46 | Calculate op_ => ("Calculate", Calculate op_)
47 | Substitute sube => ("Substitute", Substitute sube)
48 | Apply_Assumption cts' => ("Apply_Assumption", Apply_Assumption cts')
50 | Take cterm' => ("Take", Take cterm')
51 | Take_Inst cterm' => ("Take_Inst", Take_Inst cterm')
52 | Group (con, ints) => ("Group", Group (con, ints))
53 | Subproblem (domID, pblID) => ("Subproblem", Subproblem (domID, pblID))
55 | Subproblem_Full(spec,cts')=> ("Subproblem_Full", Subproblem_Full(spec,cts'))
57 | End_Subproblem => ("End_Subproblem",End_Subproblem)
58 | CAScmd cterm' => ("CAScmd", CAScmd cterm')
60 | Split_And => ("Split_And", Split_And)
61 | Conclude_And => ("Conclude_And", Conclude_And)
62 | Split_Or => ("Split_Or", Split_Or)
63 | Conclude_Or => ("Conclude_Or", Conclude_Or)
64 | Begin_Trans => ("Begin_Trans", Begin_Trans)
65 | End_Trans => ("End_Trans", End_Trans)
66 | Begin_Sequ => ("Begin_Sequ", Begin_Sequ)
67 | End_Sequ => ("End_Sequ", Begin_Sequ)
68 | Split_Intersect => ("Split_Intersect", Split_Intersect)
69 | End_Intersect => ("End_Intersect", End_Intersect)
70 | Check_elementwise cterm' => ("Check_elementwise", Check_elementwise cterm')
71 | Or_to_List => ("Or_to_List", Or_to_List)
72 | Collect_Trues => ("Collect_Results", Collect_Trues)
74 | Empty_Tac => ("Empty_Tac",Empty_Tac)
75 | Tac string => ("Tac",Tac string)
76 | User => ("User",User)
77 | End_Proof' => ("End_Proof'",End_Proof');
80 val empty_tac'_ = (mk_tac'_ Empty_Tac):tac'_;
82 fun mk_tac ((_,m):tac'_) = m;
83 fun mk_mstID ((mI,_):tac'_) = mI;
85 fun tac'_2str ((ID,ms):tac'_) = ID ^ (tac2str ms);
86 (* TODO: tac2str, tac'_2str NOT tested *)
90 type squ = ptree; (* TODO: safe etc. *)
92 (*13.9.02--------------
93 type ctr = (loc * pos) list;
94 val ops = [("PLUS","Groups.plus_class.plus"),("MINUS","Groups.minus_class.minus"),("TIMES","Groups.times_class.times"),
95 ("cancel","cancel"),("pow","pow"),("sqrt","sqrt")];
97 @{term "PLUS"}; (*Free ("PLUS", "'a") : term*)
98 @{term "plus"}; (*Const ("Groups.plus_class.plus", "'a => 'a => 'a")*)
99 @{term "MINUS"}; (*Free ("MINUS", "'a")*)
100 @{term "minus"}; (*Const ("Groups.minus_class.minus", "'a => 'a => 'a")*)
101 @{term "TIMES"}; (*Free ("TIMES", "'a")*)
102 @{term "times"}; (*Const ("Groups.times_class.times", "'a => 'a => 'a")*)
103 @{term "CANCEL"}; (*Free ("CANCEL", "'a")*)
104 @{term "cancel"}; (*Free ("cancel", "'a")*)
105 @{term "POWER"}; (*Free ("POWER", "'a")*)
106 @{term "pow"}; (*Free ("pow", "'a")*)
107 @{term "SQRT"}; (*Free ("SQRT", "'a")*)
108 @{term "sqrt"}; (*Const ("NthRoot.sqrt", "RealDef.real => RealDef.real")*)
111 case assoc (ops, op_) of
112 SOME op' => op' | NONE => error ("op_intern: no op= "^op_);
113 -----------------------*)
117 (* use"ME/solve.sml";
120 val ttt = (term_of o the o (parse thy))"Substitute [(bdv,x)] g";
121 val ttt = (term_of o the o (parse thy))"Rewrite thmid True g";
123 Const ("Script.Rewrite'_Inst",_) $ sub $ Free (thm',_) $ Const (pa,_) $ f'
128 val specsteps = ["Init_Proof","Refine_Tacitly","Refine_Problem",
129 "Model_Problem",(*"Match_Problem",*)
130 "Add_Given","Del_Given","Add_Find","Del_Find",
131 "Add_Relation","Del_Relation",
132 "Specify_Theory","Specify_Problem","Specify_Method"];
134 "-----------------------------------------------------------------------";
137 fun step2taci ((tac_, _, pt, p, _):step) = (*FIXXME.040312: redesign step*)
138 (tac_2tac tac_, tac_, (p, get_loc pt p)):taci;
141 (*FIXME.WN050821 compare solve ... nxt_solv*)
142 (* val ("Apply_Method",Apply_Method' (mI,_))=(mI,m);
143 val (("Apply_Method",Apply_Method' (mI,_,_)),pt, pos as (p,_))=(m,pt, pos);
145 fun solve ("Apply_Method", m as Apply_Method' (mI, _, _, _))
146 (pt:ptree, (pos as (p,_))) =
147 let val {srls,...} = get_met mI;
148 val PblObj{meth=itms,...} = get_obj I pt p;
149 val thy' = get_obj g_domID pt p;
150 val thy = assoc_thy thy';
151 val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
152 val ini = init_form thy sc env;
156 SOME t => (* val SOME t = ini;
158 let val (pos,c,_,pt) =
159 generate1 thy (Apply_Method' (mI, SOME t, is, ctxt))
160 (is, ctxt) (lev_on p, Frm)(*implicit Take*) pt;
161 in ("ok",([(Apply_Method mI, Apply_Method' (mI, SOME t, is, ctxt),
162 ((lev_on p, Frm), (is, ctxt)))], c, (pt,pos)):calcstate')
164 | NONE => (*execute the first tac in the Script, compare solve m*)
165 let val (m', (is', ctxt'), _) = next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);
166 val d = e_rls (*FIXME: get simplifier from domID*);
168 case locate_gen (thy',srls) m' (pt,(p, Res))(sc,d) (is', ctxt') of
169 Steps (is'', ss as (m'',f',pt',p',c')::_) =>
170 (* val Steps (is'', ss as (m'',f',pt',p',c')::_) =
171 locate_gen (thy',srls) m' (pt,(p,Res)) (sc,d) is';
173 ("ok", (map step2taci ss, c', (pt',p')))
175 let val (p,ps,f,pt) =
176 generate_hard (assoc_thy "Isac") m (p,Frm) pt;
177 in ("not-found-in-script",
178 ([(tac_2tac m, m, (pos, (is, ctxt)))], ps, (pt,p))) end
179 (*just-before------------------------------------------------------
180 ("ok",([(Apply_Method mI,Apply_Method'(mI,NONE,e_istate),
182 [], (update_env pt (fst pos) (SOME is),pos)))
183 -----------------------------------------------------------------*)
187 | solve ("Free_Solve", Free_Solve') (pt,po as (p,_)) =
188 let (*val _=tracing"###solve Free_Solve";*)
189 val p' = lev_dn_ (p,Res);
190 val pt = update_metID pt (par_pblobj pt p) e_metID;
191 in ("ok", ((*(p',Uistate,Empty_Tac_), EmptyMout, Empty_Tac, Unsafe,*)
192 [(Empty_Tac, Empty_Tac_, (po, (Uistate, e_ctxt)))], [], (pt,p'))) end
194 (* val (("Check_Postcond",Check_Postcond' (pI,_)), (pt,(pos as (p,p_)))) =
197 | solve ("Check_Postcond",Check_Postcond' (pI,_)) (pt,(pos as (p,p_))) =
198 let (*val _=tracing"###solve Check_Postcond";*)
199 val pp = par_pblobj pt p
200 val asm = (case get_obj g_tac pt p of
201 Check_elementwise _ => (*collects and instantiates asms*)
202 (snd o (get_obj g_result pt)) p
203 | _ => get_assumptions_ pt (p,p_))
204 handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*)
205 val metID = get_obj g_metID pt pp;
206 val {srls=srls,scr=sc,...} = get_met metID;
207 val loc as (ScrState (E,l,a,_,_,b), ctxt) = get_loc pt (p,p_);
208 (*val _= tracing("### solve Check_postc, subpbl pos= "^(pos'2str (p,p_)));
209 val _= tracing("### solve Check_postc, is= "^(istate2str is));*)
210 val thy' = get_obj g_domID pt pp;
211 val thy = assoc_thy thy';
212 val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc loc;
213 (*val _= tracing("### solve Check_postc, scval= "^(term2str scval));*)
216 let val is = ScrState (E,l,a,scval,scsaf,b)
217 val tac_ = Check_Postcond'(pI,(scval, map term2str asm))
218 val (pos,ps,f,pt) = generate1 thy tac_ (is, ctxt) (pp,Res) pt;
219 in ("ok", ((*(([],Res),is,End_Proof''), f, End_Proof', scsaf,*)
220 [(Check_Postcond pI, tac_, ((pp,Res),(is, ctxt)))], ps,(pt,pos))) end
223 (*resume script of parpbl, transfer value of subpbl-script*)
224 val ppp = par_pblobj pt (lev_up p);
225 val thy' = get_obj g_domID pt ppp;
226 val thy = assoc_thy thy';
227 val metID = get_obj g_metID pt ppp;
228 val sc = (#scr o get_met) metID;
229 val (ScrState (E,l,a,_,_,b), ctxt) = get_loc pt (pp(*!/p/*),Frm);
230 (*val _=tracing("### solve Check_postc, parpbl pos= "^(pos'2str(pp,Frm)));
231 val _=tracing("### solve Check_postc, is(pt)= "^(istate2str is));
232 val _=tracing("### solve Check_postc, is'= "^
233 (istate2str (E,l,a,scval,scsaf,b)));*)
234 val ((p,p_),ps,f,pt) =
235 generate1 thy (Check_Postcond' (pI, (scval, map term2str asm)))
236 (ScrState (E,l,a,scval,scsaf,b), ctxt) (pp,Res) pt;
237 (*val _=tracing("### solve Check_postc, is(pt')= "^
238 (istate2str (get_istate pt ([3],Res))));
239 val (nx,is',_) = next_tac (thy',srls) (pt,(p,p_)) sc
240 (ScrState (E,l,a,scval,scsaf,b));*)
241 in ("ok",(*((pp,Res),is',nx), f, tac_2tac nx, scsaf,*)
242 ([(Check_Postcond pI, Check_Postcond'(pI,(scval, map term2str asm)),
243 ((pp,Res), (ScrState (E,l,a,scval,scsaf,b), ctxt)))],ps,(pt,(p,p_))))
247 ("ok",([(Check_Postcond pI,Check_Postcond'(pI, (scval, map term2str asm))),
248 ((pp,Res),(ScrState (E,l,a,scval,scsaf,b)))], (pt,(p,p_))));
249 val (_,(pt',p')) = cs';
250 (tracing o istate2str) (get_istate pt' p');
251 (term2str o fst) (get_obj g_result pt' (fst p'));
254 (* tracing(istate2str(get_istate pt (p,p_)));
256 | solve (_,End_Proof'') (pt, (p,p_)) =
258 ((*(([],Res),Uistate,Empty_Tac_), EmptyMout, Empty_Tac, Safe,*)
259 [(Empty_Tac,Empty_Tac_,(([],Res),(Uistate, e_ctxt)))],[],(pt,(p,p_))))
261 (*-----------vvvvvvvvvvv could be done by generate1 ?!?*)
262 | solve (_,End_Detail' t) (pt,(p,p_)) =
263 let val pr as (p',_) = (lev_up p, Res)
264 val pp = par_pblobj pt p
265 val r = (fst o (get_obj g_result pt)) p'
266 (*Rewrite_Set* done at Detail_Set*: this result is already in ptree*)
267 val thy' = get_obj g_domID pt pp
268 val (srls, is, sc) = from_pblobj' thy' pr pt
269 val (tac_,is',_) = next_tac (thy',srls) (pt,pr) sc is
270 in ("ok", ((*((pp,Frm(*???*)),is,tac_),
271 Form' (FormKF (~1, EdUndef, length p', Nundef, term2str r)),
272 tac_2tac tac_, Sundef,*)
273 [(End_Detail, End_Detail' t ,
274 ((p,p_), get_loc pt (p,p_)))], [], (pt,pr))) end
276 | solve (mI,m) (pt, po as (p,p_)) =
277 (* val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
279 if e_metID = get_obj g_metID pt (par_pblobj pt p)(*29.8.02:
280 could be detail, too !!*)
281 then let val ((p,p_),ps,f,pt) =
282 generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p)))
283 m (e_istate, e_ctxt) (p,p_) pt;
284 in ("no-method-specified", (*Free_Solve*)
285 ((*((p,p_),Uistate,Empty_Tac_),f, Empty_Tac, Unsafe,*)
286 [(Empty_Tac,Empty_Tac_, ((p,p_),(Uistate, e_ctxt)))], ps, (pt,(p,p_)))) end
289 val thy' = get_obj g_domID pt (par_pblobj pt p);
290 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
291 (*val _= tracing("### solve, before locate_gen p="^(pos'2str(p,p_)));*)
292 val d = e_rls; (*FIXME: canon.simplifier for domain is missing
293 8.01: generate from domID?*)
294 in case locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is of
295 Steps (is', ss as (m',f',pt',p',c')::_) =>
296 (* val Steps (is', ss as (m',f',pt',p',c')::_) =
297 locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is;
299 let (*val _= tracing("### solve, after locate_gen: is= ")
300 val _= tracing(istate2str is')*)
302 case p' of (*change from solve to model subpbl*)
303 (_,Pbl) => nxt_model_pbl m' (pt',p')
304 | _ => fst3 (next_tac (thy',srls) (pt',p') sc is');*)
305 (*27.8.02:next_tac may change to other branches in pt FIXXXXME*)
306 in ("ok", ((*(p',is',nxt_), f', tac_2tac nxt_, safe is',*)
307 map step2taci ss, c', (pt',p'))) end
309 let val (p,ps,f,pt) =
310 generate_hard (assoc_thy "Isac") m (p,p_) pt;
311 in ("not-found-in-script",
312 ((*(p,Uistate,Empty_Tac_),f, Empty_Tac, Unsafe,*)
313 [(tac_2tac m, m, (po,is))], ps, (pt,p))) end
317 (*FIXME.WN050821 compare solve ... nxt_solv*)
318 (* nxt_solv (Apply_Method' vvv FIXME: get args in applicable_in *)
319 fun nxt_solv (Apply_Method' (mI,_,_,_)) _ (pt:ptree, pos as (p,_)) =
320 (* val ((Apply_Method' (mI,_,_)), _, (pt:ptree, pos as (p,_))) =
321 ((Apply_Method' (mI, NONE, e_istate)), e_istate, ptp);
323 let val {srls,ppc,...} = get_met mI;
324 val PblObj{meth=itms,origin=(oris,_,_),probl,...} = get_obj I pt p;
325 val itms = if itms <> [] then itms
326 else complete_metitms oris probl [] ppc
327 val thy' = get_obj g_domID pt p;
328 val thy = assoc_thy thy';
329 val (is as ScrState (env,_,_,_,_,_), ctxt, scr) = init_scrstate thy itms mI;
330 val ini = init_form thy scr env;
333 SOME t => (* val SOME t = ini;
335 let val pos = ((lev_on o lev_dn) p, Frm)
336 val tac_ = Apply_Method' (mI, SOME t, is, ctxt);
337 val (pos,c,_,pt) = (*implicit Take*)
338 generate1 thy tac_ (is, ctxt) pos pt
339 (*val _= ("### nxt_solv Apply_Method, pos= "^pos'2str (lev_on p,Frm));*)
340 in ([(Apply_Method mI, tac_, (pos, (is, ctxt)))], c, (pt, pos)):calcstate' end
342 let val pt = update_env pt (fst pos) (SOME (is, ctxt))
343 val (tacis, c, ptp) = nxt_solve_ (pt, pos)
345 [(Apply_Method mI, Apply_Method' (mI, NONE, e_istate, e_ctxt), (pos, (is, ctxt)))],
348 (* val ("Check_Postcond",Check_Postcond' (pI,_)) = (mI,m);
349 val (Check_Postcond' (pI,_), _, (pt, pos as (p,p_))) =
352 (*TODO.WN050913 remove unnecessary code below*)
353 | nxt_solv (Check_Postcond' (pI,_)) _ (pt, pos as (p,p_)) =
354 let (*val _=tracing"###solve Check_Postcond";*)
355 val pp = par_pblobj pt p
356 val asm = (case get_obj g_tac pt p of
357 Check_elementwise _ => (*collects and instantiates asms*)
358 (snd o (get_obj g_result pt)) p
359 | _ => get_assumptions_ pt (p,p_))
360 handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*)
361 val metID = get_obj g_metID pt pp;
362 val {srls=srls,scr=sc,...} = get_met metID;
363 val loc as (ScrState (E,l,a,_,_,b), ctxt) = get_loc pt (p,p_);
364 (*val _= tracing("### solve Check_postc, subpbl pos= "^(pos'2str (p,p_)));
365 val _= tracing("### solve Check_postc, is= "^(istate2str is));*)
366 val thy' = get_obj g_domID pt pp;
367 val thy = assoc_thy thy';
368 val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc loc;
369 (*val _= tracing("### solve Check_postc, scval= "^(term2str scval));*)
371 let val is = ScrState (E,l,a,scval,scsaf,b)
372 val tac_ = Check_Postcond'(pI,(scval, map term2str asm))
373 (*val _= tracing"### nxt_solv2 Apply_Method: stored is =";
374 val _= tracing(istate2str is);*)
375 val ((p,p_),ps,f,pt) =
376 generate1 thy tac_ (is, ctxt) (pp,Res) pt;
377 in ([(Check_Postcond pI, tac_, ((pp,Res), (is, ctxt)))],ps,(pt, (p,p_))) end
380 (*resume script of parpbl, transfer value of subpbl-script*)
381 val ppp = par_pblobj pt (lev_up p);
382 val thy' = get_obj g_domID pt ppp;
383 val thy = assoc_thy thy';
384 val metID = get_obj g_metID pt ppp;
385 val {scr,...} = get_met metID;
386 val (ScrState (E,l,a,_,_,b), ctxt) = get_loc pt (pp(*!/p/*),Frm)
387 val tac_ = Check_Postcond' (pI, (scval, map term2str asm))
388 val is = ScrState (E,l,a,scval,scsaf,b)
389 (*val _= tracing"### nxt_solv3 Apply_Method: stored is =";
390 val _= tracing(istate2str is);*)
391 val ((p,p_),ps,f,pt) = generate1 thy tac_ (is, ctxt) (pp, Res) pt;
392 (*val (nx,is',_) = next_tac (thy',srls) (pt,(p,p_)) scr is;WN050913*)
393 in ([(Check_Postcond pI, tac_, ((pp, Res), (is, ctxt)))], ps, (pt, (p,p_))) end
395 (* tracing(istate2str(get_istate pt (p,p_)));
398 (*.start interpreter and do one rewrite.*)
399 (* val (_,Detail_Set'(thy',rls,t)) = (mI,m); val p = (p,p_);
400 solve ("",Detail_Set'(thy', rls, t)) p pt;
401 | nxt_solv (Detail_Set'(thy', rls, t)) _ (pt, p) = **********
402 ---> Frontend/sml.sml
404 | nxt_solv (End_Detail' t) _ (pt, (p,p_)) = **********
405 let val pr as (p',_) = (lev_up p, Res)
406 val pp = par_pblobj pt p
407 val r = (fst o (get_obj g_result pt)) p'
408 (*Rewrite_Set* done at Detail_Set*: this result is already in ptree*)
409 val thy' = get_obj g_domID pt pp
410 val (srls, is, sc) = from_pblobj' thy' pr pt
411 val (tac_,is',_) = next_tac (thy',srls) (pt,pr) sc is
412 in (pr, ((pp,Frm(*???*)),is,tac_),
413 Form' (FormKF (~1, EdUndef, length p', Nundef, term2str r)),
414 tac_2tac tac_, Sundef, pt) end
416 | nxt_solv (End_Proof'') _ ptp = ([], [], ptp)
418 | nxt_solv tac_ is (pt, pos as (p,p_)) =
419 (* val (pt, pos as (p,p_)) = ptp;
421 let val pos = case pos of
422 (p, Met) => ((lev_on o lev_dn) p, Frm)(*begin script*)
423 | (p, Res) => (lev_on p,Res) (*somewhere in script*)
424 | _ => pos (*somewhere in script*)
425 (*val _= tracing"### nxt_solv4 Apply_Method: stored is =";
426 val _= tracing(istate2str is);*)
427 val (pos',c,_,pt) = generate1 (assoc_thy "Isac") tac_ is pos pt;
428 in ([(tac_2tac tac_, tac_, (pos,is))], c, (pt, pos')) end
431 (*(p,p_), (([],Res),Uistate,Empty_Tac_), EmptyMout, Empty_Tac, Safe, pt*)
434 (*.find the next tac from the script, nxt_solv will update the ptree.*)
435 (* val (ptp as (pt,pos as (p,p_))) = ptp';
436 val (ptp as (pt, pos as (p,p_))) = ptp'';
437 val (ptp as (pt, pos as (p,p_))) = ptp;
438 val (ptp as (pt, pos as (p,p_))) = (pt,ip);
439 val (ptp as (pt, pos as (p,p_))) = (pt, pos);
441 and nxt_solve_ (ptp as (pt, pos as (p,p_))) =
442 if e_metID = get_obj g_metID pt (par_pblobj pt p)
443 then ([], [], (pt,(p,p_))):calcstate'
444 else let val thy' = get_obj g_domID pt (par_pblobj pt p);
445 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
446 val (tac_,is,(t,_)) = next_tac (thy',srls) (pt,pos) sc is;
447 (*TODO here ^^^ return finished/helpless/ok !*)
448 (* val (tac_',is',(t',_)) = next_tac (thy',srls) (pt,pos) sc is;
451 End_Detail' _ => ([(End_Detail,
452 End_Detail' (t,[(*FIXME.040215*)]),
453 (pos, is))], [], (pt, pos))
454 | _ => nxt_solv tac_ is ptp end;
456 (*.says how may steps of a calculation should be done by "fun autocalc".*)
457 (*TODO.WN0512 redesign togehter with autocalc ?*)
459 Step of int (*1 do #int steps; may stop in model/specify:
460 IS VERY INEFFICIENT IN MODEL/SPECIY*)
461 | CompleteModel (*2 complete modeling
462 if model complete, finish specifying + start solving*)
463 | CompleteCalcHead (*3 complete model/specify in one go + start solving*)
464 | CompleteToSubpbl (*4 stop at the next begin of a subproblem,
465 if none, complete the actual (sub)problem*)
466 | CompleteSubpbl (*5 complete the actual (sub)problem (incl.ev.subproblems)*)
467 | CompleteCalc; (*6 complete the calculation as a whole*)
468 fun autoord (Step _ ) = 1
469 | autoord CompleteModel = 2
470 | autoord CompleteCalcHead = 3
471 | autoord CompleteToSubpbl = 4
472 | autoord CompleteSubpbl = 5
473 | autoord CompleteCalc = 6;
475 (* val (auto, c, (ptp as (_, p))) = (auto, (c@c'), ptp);
477 fun complete_solve auto c (ptp as (_, p): ptree * pos') =
478 if p = ([], Res) then ("end-of-calculation", [], ptp) else
479 case nxt_solve_ ptp of
480 ((Subproblem _, tac_, (_, is))::_, c', ptp') =>
481 (* val ptp' = ptp''';
483 if autoord auto < 5 then ("ok", c@c', ptp)
484 else let val ptp = all_modspec ptp';
485 val (_, c'', ptp) = all_solve auto (c@c') ptp;
486 in complete_solve auto (c@c'@c'') ptp end
487 | ((Check_Postcond _, tac_, (_, is))::_, c', ptp' as (_, p')) =>
488 if autoord auto < 6 orelse p' = ([],Res) then ("ok", c@c', ptp')
489 else complete_solve auto (c@c') ptp'
490 | ((End_Detail, _, _)::_, c', ptp') =>
491 if autoord auto < 6 then ("ok", c@c', ptp')
492 else complete_solve auto (c@c') ptp'
493 | (_, c', ptp') => complete_solve auto (c@c') ptp'
494 (* val (tacis, c', ptp') = nxt_solve_ ptp;
495 val (tacis, c', ptp'') = nxt_solve_ ptp';
496 val (tacis, c', ptp''') = nxt_solve_ ptp'';
497 val (tacis, c', ptp'''') = nxt_solve_ ptp''';
498 val (tacis, c', ptp''''') = nxt_solve_ ptp'''';
500 and all_solve auto c (ptp as (pt, (p,_)): ptree * pos') =
501 (* val (ptp as (pt, (p,_))) = ptp;
502 val (ptp as (pt, (p,_))) = ptp';
503 val (ptp as (pt, (p,_))) = (pt, pos);
505 let val (_,_,mI) = get_obj g_spec pt p;
506 val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt))
507 (e_istate, e_ctxt) ptp;
508 in complete_solve auto (c@c') ptp end;
509 (*@@@ vvv @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
510 fun complete_solve auto c (ptp as (_, p as (_,p_)): ptree * pos') =
511 if p = ([], Res) then ("end-of-calculation", [], ptp) else
512 if member op = [Pbl,Met] p_
513 then let val ptp = all_modspec ptp
514 val (_, c', ptp) = all_solve auto c ptp
515 in complete_solve auto (c@c') ptp end
516 else case nxt_solve_ ptp of
517 ((Subproblem _, tac_, (_, is))::_, c', ptp') =>
518 if autoord auto < 5 then ("ok", c@c', ptp)
519 else let val ptp = all_modspec ptp'
520 val (_, c'', ptp) = all_solve auto (c@c') ptp
521 in complete_solve auto (c@c'@c'') ptp end
522 | ((Check_Postcond _, tac_, (_, is))::_, c', ptp' as (_, p')) =>
523 if autoord auto < 6 orelse p' = ([],Res) then ("ok", c@c', ptp')
524 else complete_solve auto (c@c') ptp'
525 | ((End_Detail, _, _)::_, c', ptp') =>
526 if autoord auto < 6 then ("ok", c@c', ptp')
527 else complete_solve auto (c@c') ptp'
528 | (_, c', ptp') => complete_solve auto (c@c') ptp'
529 and all_solve auto c (ptp as (pt, (p,_)): ptree * pos') =
530 let val (_,_,mI) = get_obj g_spec pt p
531 val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt))
532 (e_istate, e_ctxt) ptp
533 in complete_solve auto (c@c') ptp end;
535 (*.aux.fun for detailrls with Rrls, reverse rewriting.*)
536 (* val (nds, t, ((rule, (t', asm)) :: rts)) = ([], t, rul_terms);
538 fun rul_terms_2nds nds t [] = nds
539 | rul_terms_2nds nds t ((rule, res as (t', _)) :: rts) =
540 (append_atomic [] (e_istate, e_ctxt) t (rule2tac [] rule) res Complete EmptyPtree) ::
541 (rul_terms_2nds nds t' rts);
544 (*. detail steps done internally by Rewrite_Set*
545 into ctree by use of a script .*)
546 (* val (pt, (p,p_)) = (pt, pos);
548 fun detailrls pt ((p,p_):pos') =
549 let val t = get_obj g_form pt p
550 val tac = get_obj g_tac pt p
551 val rls = (assoc_rls o rls_of) tac
553 (* val Rrls {scr = Rfuns {init_state,...},...} = rls;
555 Rrls {scr = Rfuns {init_state,...},...} =>
556 let val (_,_,_,rul_terms) = init_state t
557 val newnds = rul_terms_2nds [] t rul_terms
558 val pt''' = ins_chn newnds pt p
559 in ("detailrls", pt''', (p @ [length newnds], Res):pos') end
561 let val is = init_istate tac t
562 (*TODO.WN060602 ScrState (["(t_, Problem (Isac,[equation,univar]))"]
563 is wrong for simpl, but working ?!? *)
564 val tac_ = Apply_Method' (e_metID(*WN0402: see generate1 !?!*),
566 val pos' = ((lev_on o lev_dn) p, Frm)
567 val thy = assoc_thy "Isac"
568 val (_,_,_,pt') = (*implicit Take*)generate1 thy tac_ (is, e_ctxt) pos' pt
569 val (_,_,(pt'',_)) = complete_solve CompleteSubpbl [] (pt',pos')
570 val newnds = children (get_nd pt'' p)
571 val pt''' = ins_chn newnds pt p
572 (*complete_solve cuts branches after*)
573 in ("detailrls", pt'''(*, get_formress [] ((lev_on o lev_dn) p)cn*),
574 (p @ [length newnds], Res):pos') end
579 (* val(mI,m)=m;val ppp=p;(*!!!*)val(p,p_)=pos;val(_,pt,_)=ppp(*!!!*);
580 get_form ((mI,m):tac'_) ((p,p_):pos') ppp;
582 fun get_form ((mI,m):tac'_) ((p,p_):pos') pt =
583 case applicable_in (p,p_) pt m of
584 Notappl e => Error' (Error_ e)
586 (* val Appl m=applicable_in (p,p_) pt m;
588 if member op = specsteps mI
589 then let val (_,_,f,_,_,_) = specify m (p,p_) [] pt
591 else let val (*_,_,f,_,_,_*)_ = solve (mI,m) (pt,(p,p_))
592 in (*f*) EmptyMout end;