|
1 (* solve an example by interpreting a method's script |
|
2 (c) Walther Neuper 1999 |
|
3 |
|
4 use"ME/solve.sml"; |
|
5 use"solve.sml"; |
|
6 *) |
|
7 |
|
8 fun safe (ScrState (_,_,_,_,s,_)) = s |
|
9 | safe (RrlsState _) = Safe; |
|
10 |
|
11 type mstID = string; |
|
12 type tac'_ = mstID * tac; (*DG <-> ME*) |
|
13 val e_tac'_ = ("Empty_Tac", Empty_Tac):tac'_; |
|
14 |
|
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') |
|
26 |
|
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) |
|
33 |
|
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) |
|
41 |
|
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')) |
|
45 |
|
46 | Calculate op_ => ("Calculate", Calculate op_) |
|
47 | Substitute sube => ("Substitute", Substitute sube) |
|
48 | Apply_Assumption cts' => ("Apply_Assumption", Apply_Assumption cts') |
|
49 |
|
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)) |
|
54 (* |
|
55 | Subproblem_Full(spec,cts')=> ("Subproblem_Full", Subproblem_Full(spec,cts')) |
|
56 *) |
|
57 | End_Subproblem => ("End_Subproblem",End_Subproblem) |
|
58 | CAScmd cterm' => ("CAScmd", CAScmd cterm') |
|
59 |
|
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) |
|
73 |
|
74 | Empty_Tac => ("Empty_Tac",Empty_Tac) |
|
75 | Tac string => ("Tac",Tac string) |
|
76 | User => ("User",User) |
|
77 | End_Proof' => ("End_Proof'",End_Proof'); |
|
78 |
|
79 (*Detail*) |
|
80 val empty_tac'_ = (mk_tac'_ Empty_Tac):tac'_; |
|
81 |
|
82 fun mk_tac ((_,m):tac'_) = m; |
|
83 fun mk_mstID ((mI,_):tac'_) = mI; |
|
84 |
|
85 fun tac'_2str ((ID,ms):tac'_) = ID ^ (tac2str ms); |
|
86 (* TODO: tac2str, tac'_2str NOT tested *) |
|
87 |
|
88 |
|
89 |
|
90 type squ = ptree; (* TODO: safe etc. *) |
|
91 |
|
92 (*13.9.02-------------- |
|
93 type ctr = (loc * pos) list; |
|
94 val ops = [("PLUS","op +"),("minus","op -"),("TIMES","op *"), |
|
95 ("cancel","cancel"),("pow","pow"),("sqrt","sqrt")]; |
|
96 fun op_intern op_ = |
|
97 case assoc (ops,op_) of |
|
98 SOME op' => op' | NONE => raise error ("op_intern: no op= "^op_); |
|
99 -----------------------*) |
|
100 |
|
101 |
|
102 |
|
103 (* use"ME/solve.sml"; |
|
104 use"solve.sml"; |
|
105 |
|
106 val ttt = (term_of o the o (parse thy))"Substitute [(bdv,x)] g"; |
|
107 val ttt = (term_of o the o (parse thy))"Rewrite thmid True g"; |
|
108 |
|
109 Const ("Script.Rewrite'_Inst",_) $ sub $ Free (thm',_) $ Const (pa,_) $ f' |
|
110 *) |
|
111 |
|
112 |
|
113 |
|
114 val specsteps = ["Init_Proof","Refine_Tacitly","Refine_Problem", |
|
115 "Model_Problem",(*"Match_Problem",*) |
|
116 "Add_Given","Del_Given","Add_Find","Del_Find", |
|
117 "Add_Relation","Del_Relation", |
|
118 "Specify_Theory","Specify_Problem","Specify_Method"]; |
|
119 |
|
120 "-----------------------------------------------------------------------"; |
|
121 |
|
122 |
|
123 fun step2taci ((tac_, _, pt, p, _):step) = (*FIXXME.040312: redesign step*) |
|
124 (tac_2tac tac_, tac_, (p, get_istate pt p)):taci; |
|
125 |
|
126 |
|
127 (*FIXME.WN050821 compare solve ... nxt_solv*) |
|
128 (* val ("Apply_Method",Apply_Method' (mI,_))=(mI,m); |
|
129 val (("Apply_Method",Apply_Method' (mI,_,_)),pt, pos as (p,_))=(m,pt, pos); |
|
130 *) |
|
131 fun solve ("Apply_Method", m as Apply_Method' (mI, _, _)) |
|
132 (pt:ptree, (pos as (p,_))) = |
|
133 let val {srls,...} = get_met mI; |
|
134 val PblObj{meth=itms,...} = get_obj I pt p; |
|
135 val thy' = get_obj g_domID pt p; |
|
136 val thy = assoc_thy thy'; |
|
137 val (is as ScrState (env,_,_,_,_,_), sc) = init_scrstate thy itms mI; |
|
138 val ini = init_form thy sc env; |
|
139 val p = lev_dn p; |
|
140 in |
|
141 case ini of |
|
142 SOME t => (* val SOME t = ini; |
|
143 *) |
|
144 let val (pos,c,_,pt) = |
|
145 generate1 thy (Apply_Method' (mI, SOME t, is)) |
|
146 is (lev_on p, Frm)(*implicit Take*) pt; |
|
147 in ("ok",([(Apply_Method mI, Apply_Method' (mI, SOME t, is), |
|
148 ((lev_on p, Frm), is))], c, (pt,pos)):calcstate') |
|
149 end |
|
150 | NONE => (*execute the first tac in the Script, compare solve m*) |
|
151 let val (m', is', _) = next_tac (thy', srls) (pt, (p, Res)) sc is; |
|
152 val d = e_rls (*FIXME: get simplifier from domID*); |
|
153 in |
|
154 case locate_gen (thy',srls) m' (pt,(p, Res))(sc,d) is' of |
|
155 Steps (is'', ss as (m'',f',pt',p',c')::_) => |
|
156 (* val Steps (is'', ss as (m'',f',pt',p',c')::_) = |
|
157 locate_gen (thy',srls) m' (pt,(p,Res)) (sc,d) is'; |
|
158 *) |
|
159 ("ok", (map step2taci ss, c', (pt',p'))) |
|
160 | NotLocatable => |
|
161 let val (p,ps,f,pt) = |
|
162 generate_hard (assoc_thy "Isac.thy") m (p,Frm) pt; |
|
163 in ("not-found-in-script", |
|
164 ([(tac_2tac m, m, (pos, is))], ps, (pt,p))) end |
|
165 (*just-before------------------------------------------------------ |
|
166 ("ok",([(Apply_Method mI,Apply_Method'(mI,NONE,e_istate), |
|
167 (pos, is))], |
|
168 [], (update_env pt (fst pos) (SOME is),pos))) |
|
169 -----------------------------------------------------------------*) |
|
170 end |
|
171 end |
|
172 |
|
173 | solve ("Free_Solve", Free_Solve') (pt,po as (p,_)) = |
|
174 let (*val _=writeln"###solve Free_Solve";*) |
|
175 val p' = lev_dn_ (p,Res); |
|
176 val pt = update_metID pt (par_pblobj pt p) e_metID; |
|
177 in ("ok", ((*(p',Uistate,Empty_Tac_), EmptyMout, Empty_Tac, Unsafe,*) |
|
178 [(Empty_Tac, Empty_Tac_, (po, Uistate))], [], (pt,p'))) end |
|
179 |
|
180 (* val (("Check_Postcond",Check_Postcond' (pI,_)), (pt,(pos as (p,p_)))) = |
|
181 ( m, (pt, pos)); |
|
182 *) |
|
183 | solve ("Check_Postcond",Check_Postcond' (pI,_)) (pt,(pos as (p,p_))) = |
|
184 let (*val _=writeln"###solve Check_Postcond";*) |
|
185 val pp = par_pblobj pt p |
|
186 val asm = (case get_obj g_tac pt p of |
|
187 Check_elementwise _ => (*collects and instantiates asms*) |
|
188 (snd o (get_obj g_result pt)) p |
|
189 | _ => ((map fst) o (get_assumptions_ pt)) (p,p_)) |
|
190 handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*) |
|
191 val metID = get_obj g_metID pt pp; |
|
192 val {srls=srls,scr=sc,...} = get_met metID; |
|
193 val is as ScrState (E,l,a,_,_,b) = get_istate pt (p,p_); |
|
194 (*val _= writeln("### solve Check_postc, subpbl pos= "^(pos'2str (p,p_))); |
|
195 val _= writeln("### solve Check_postc, is= "^(istate2str is));*) |
|
196 val thy' = get_obj g_domID pt pp; |
|
197 val thy = assoc_thy thy'; |
|
198 val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc is; |
|
199 (*val _= writeln("### solve Check_postc, scval= "^(term2str scval));*) |
|
200 |
|
201 in if pp = [] then |
|
202 let val is = ScrState (E,l,a,scval,scsaf,b) |
|
203 val tac_ = Check_Postcond'(pI,(scval, map term2str asm)) |
|
204 val (pos,ps,f,pt) = generate1 thy tac_ is (pp,Res) pt; |
|
205 in ("ok", ((*(([],Res),is,End_Proof''), f, End_Proof', scsaf,*) |
|
206 [(Check_Postcond pI, tac_, ((pp,Res),is))], ps,(pt,pos))) end |
|
207 else |
|
208 let |
|
209 (*resume script of parpbl, transfer value of subpbl-script*) |
|
210 val ppp = par_pblobj pt (lev_up p); |
|
211 val thy' = get_obj g_domID pt ppp; |
|
212 val thy = assoc_thy thy'; |
|
213 val metID = get_obj g_metID pt ppp; |
|
214 val sc = (#scr o get_met) metID; |
|
215 val is as ScrState (E,l,a,_,_,b) = get_istate pt (pp(*!/p/*),Frm); |
|
216 (*val _=writeln("### solve Check_postc, parpbl pos= "^(pos'2str(pp,Frm))); |
|
217 val _=writeln("### solve Check_postc, is(pt)= "^(istate2str is)); |
|
218 val _=writeln("### solve Check_postc, is'= "^ |
|
219 (istate2str (E,l,a,scval,scsaf,b)));*) |
|
220 val ((p,p_),ps,f,pt) = |
|
221 generate1 thy (Check_Postcond' (pI, (scval, map term2str asm))) |
|
222 (ScrState (E,l,a,scval,scsaf,b)) (pp,Res) pt; |
|
223 (*val _=writeln("### solve Check_postc, is(pt')= "^ |
|
224 (istate2str (get_istate pt ([3],Res)))); |
|
225 val (nx,is',_) = next_tac (thy',srls) (pt,(p,p_)) sc |
|
226 (ScrState (E,l,a,scval,scsaf,b));*) |
|
227 in ("ok",(*((pp,Res),is',nx), f, tac_2tac nx, scsaf,*) |
|
228 ([(Check_Postcond pI, Check_Postcond'(pI,(scval, map term2str asm)), |
|
229 ((pp,Res), ScrState (E,l,a,scval,scsaf,b)))],ps,(pt,(p,p_)))) |
|
230 end |
|
231 end |
|
232 (* val (msg, cs') = |
|
233 ("ok",([(Check_Postcond pI,Check_Postcond'(pI, (scval, map term2str asm))), |
|
234 ((pp,Res),(ScrState (E,l,a,scval,scsaf,b)))], (pt,(p,p_)))); |
|
235 val (_,(pt',p')) = cs'; |
|
236 (writeln o istate2str) (get_istate pt' p'); |
|
237 (term2str o fst) (get_obj g_result pt' (fst p')); |
|
238 *) |
|
239 |
|
240 (* writeln(istate2str(get_istate pt (p,p_))); |
|
241 *) |
|
242 | solve (_,End_Proof'') (pt, (p,p_)) = |
|
243 ("end-proof", |
|
244 ((*(([],Res),Uistate,Empty_Tac_), EmptyMout, Empty_Tac, Safe,*) |
|
245 [(Empty_Tac,Empty_Tac_,(([],Res),Uistate))],[],(pt,(p,p_)))) |
|
246 |
|
247 (*-----------vvvvvvvvvvv could be done by generate1 ?!?*) |
|
248 | solve (_,End_Detail' t) (pt,(p,p_)) = |
|
249 let val pr as (p',_) = (lev_up p, Res) |
|
250 val pp = par_pblobj pt p |
|
251 val r = (fst o (get_obj g_result pt)) p' |
|
252 (*Rewrite_Set* done at Detail_Set*: this result is already in ptree*) |
|
253 val thy' = get_obj g_domID pt pp |
|
254 val (srls, is, sc) = from_pblobj' thy' pr pt |
|
255 val (tac_,is',_) = next_tac (thy',srls) (pt,pr) sc is |
|
256 in ("ok", ((*((pp,Frm(*???*)),is,tac_), |
|
257 Form' (FormKF (~1, EdUndef, length p', Nundef, term2str r)), |
|
258 tac_2tac tac_, Sundef,*) |
|
259 [(End_Detail, End_Detail' t , |
|
260 ((p,p_), get_istate pt (p,p_)))], [], (pt,pr))) end |
|
261 |
|
262 | solve (mI,m) (pt, po as (p,p_)) = |
|
263 (* val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos)); |
|
264 *) |
|
265 if e_metID = get_obj g_metID pt (par_pblobj pt p)(*29.8.02: |
|
266 could be detail, too !!*) |
|
267 then let val ((p,p_),ps,f,pt) = |
|
268 generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p))) |
|
269 m e_istate (p,p_) pt; |
|
270 in ("no-method-specified", (*Free_Solve*) |
|
271 ((*((p,p_),Uistate,Empty_Tac_),f, Empty_Tac, Unsafe,*) |
|
272 [(Empty_Tac,Empty_Tac_, ((p,p_),Uistate))], ps, (pt,(p,p_)))) end |
|
273 else |
|
274 let |
|
275 val thy' = get_obj g_domID pt (par_pblobj pt p); |
|
276 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; |
|
277 (*val _= writeln("### solve, before locate_gen p="^(pos'2str(p,p_)));*) |
|
278 val d = e_rls; (*FIXME: canon.simplifier for domain is missing |
|
279 8.01: generate from domID?*) |
|
280 in case locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is of |
|
281 Steps (is', ss as (m',f',pt',p',c')::_) => |
|
282 (* val Steps (is', ss as (m',f',pt',p',c')::_) = |
|
283 locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is; |
|
284 *) |
|
285 let (*val _= writeln("### solve, after locate_gen: is= ") |
|
286 val _= writeln(istate2str is')*) |
|
287 (*val nxt_ = |
|
288 case p' of (*change from solve to model subpbl*) |
|
289 (_,Pbl) => nxt_model_pbl m' (pt',p') |
|
290 | _ => fst3 (next_tac (thy',srls) (pt',p') sc is');*) |
|
291 (*27.8.02:next_tac may change to other branches in pt FIXXXXME*) |
|
292 in ("ok", ((*(p',is',nxt_), f', tac_2tac nxt_, safe is',*) |
|
293 map step2taci ss, c', (pt',p'))) end |
|
294 | NotLocatable => |
|
295 let val (p,ps,f,pt) = |
|
296 generate_hard (assoc_thy "Isac.thy") m (p,p_) pt; |
|
297 in ("not-found-in-script", |
|
298 ((*(p,Uistate,Empty_Tac_),f, Empty_Tac, Unsafe,*) |
|
299 [(tac_2tac m, m, (po,is))], ps, (pt,p))) end |
|
300 end; |
|
301 |
|
302 |
|
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); |
|
308 *) |
|
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; |
|
317 in |
|
318 case ini of |
|
319 SOME t => (* val SOME t = ini; |
|
320 *) |
|
321 let val pos = ((lev_on o lev_dn) p, Frm) |
|
322 val tac_ = Apply_Method' (mI, SOME t, is); |
|
323 val (pos,c,_,pt) = (*implicit Take*) |
|
324 generate1 thy tac_ is pos pt |
|
325 (*val _= ("### nxt_solv Apply_Method, pos= "^pos'2str (lev_on p,Frm));*) |
|
326 in ([(Apply_Method mI, tac_, (pos, is))], c, (pt, pos)):calcstate' end |
|
327 | NONE => |
|
328 let val pt = update_env pt (fst pos) (SOME is) |
|
329 val (tacis, c, ptp) = nxt_solve_ (pt, pos) |
|
330 in (tacis @ |
|
331 [(Apply_Method mI, Apply_Method' (mI, NONE, e_istate), (pos, is))], |
|
332 c, ptp) end |
|
333 end |
|
334 (* val ("Check_Postcond",Check_Postcond' (pI,_)) = (mI,m); |
|
335 val (Check_Postcond' (pI,_), _, (pt, pos as (p,p_))) = |
|
336 (tac_, is, ptp); |
|
337 *) |
|
338 (*TODO.WN050913 remove unnecessary code below*) |
|
339 | nxt_solv (Check_Postcond' (pI,_)) _ (pt, pos as (p,p_)) = |
|
340 let (*val _=writeln"###solve Check_Postcond";*) |
|
341 val pp = par_pblobj pt p |
|
342 val asm = (case get_obj g_tac pt p of |
|
343 Check_elementwise _ => (*collects and instantiates asms*) |
|
344 (snd o (get_obj g_result pt)) p |
|
345 | _ => ((map fst) o (get_assumptions_ pt)) (p,p_)) |
|
346 handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*) |
|
347 val metID = get_obj g_metID pt pp; |
|
348 val {srls=srls,scr=sc,...} = get_met metID; |
|
349 val is as ScrState (E,l,a,_,_,b) = get_istate pt (p,p_); |
|
350 (*val _= writeln("### solve Check_postc, subpbl pos= "^(pos'2str (p,p_))); |
|
351 val _= writeln("### solve Check_postc, is= "^(istate2str is));*) |
|
352 val thy' = get_obj g_domID pt pp; |
|
353 val thy = assoc_thy thy'; |
|
354 val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc is; |
|
355 (*val _= writeln("### solve Check_postc, scval= "^(term2str scval));*) |
|
356 in if pp = [] then |
|
357 let val is = ScrState (E,l,a,scval,scsaf,b) |
|
358 val tac_ = Check_Postcond'(pI,(scval, map term2str asm)) |
|
359 (*val _= writeln"### nxt_solv2 Apply_Method: stored is ="; |
|
360 val _= writeln(istate2str is);*) |
|
361 val ((p,p_),ps,f,pt) = |
|
362 generate1 thy tac_ is (pp,Res) pt; |
|
363 in ([(Check_Postcond pI, tac_, ((pp,Res), is))],ps,(pt, (p,p_))) end |
|
364 else |
|
365 let |
|
366 (*resume script of parpbl, transfer value of subpbl-script*) |
|
367 val ppp = par_pblobj pt (lev_up p); |
|
368 val thy' = get_obj g_domID pt ppp; |
|
369 val thy = assoc_thy thy'; |
|
370 val metID = get_obj g_metID pt ppp; |
|
371 val {scr,...} = get_met metID; |
|
372 val is as ScrState (E,l,a,_,_,b) = get_istate pt (pp(*!/p/*),Frm) |
|
373 val tac_ = Check_Postcond' (pI, (scval, map term2str asm)) |
|
374 val is = ScrState (E,l,a,scval,scsaf,b) |
|
375 (*val _= writeln"### nxt_solv3 Apply_Method: stored is ="; |
|
376 val _= writeln(istate2str is);*) |
|
377 val ((p,p_),ps,f,pt) = generate1 thy tac_ is (pp, Res) pt; |
|
378 (*val (nx,is',_) = next_tac (thy',srls) (pt,(p,p_)) scr is;WN050913*) |
|
379 in ([(Check_Postcond pI, tac_, ((pp, Res), is))], ps, (pt, (p,p_))) end |
|
380 end |
|
381 (* writeln(istate2str(get_istate pt (p,p_))); |
|
382 *) |
|
383 |
|
384 (*.start interpreter and do one rewrite.*) |
|
385 (* val (_,Detail_Set'(thy',rls,t)) = (mI,m); val p = (p,p_); |
|
386 solve ("",Detail_Set'(thy', rls, t)) p pt; |
|
387 | nxt_solv (Detail_Set'(thy', rls, t)) _ (pt, p) = ********** |
|
388 ---> Frontend/sml.sml |
|
389 |
|
390 | nxt_solv (End_Detail' t) _ (pt, (p,p_)) = ********** |
|
391 let val pr as (p',_) = (lev_up p, Res) |
|
392 val pp = par_pblobj pt p |
|
393 val r = (fst o (get_obj g_result pt)) p' |
|
394 (*Rewrite_Set* done at Detail_Set*: this result is already in ptree*) |
|
395 val thy' = get_obj g_domID pt pp |
|
396 val (srls, is, sc) = from_pblobj' thy' pr pt |
|
397 val (tac_,is',_) = next_tac (thy',srls) (pt,pr) sc is |
|
398 in (pr, ((pp,Frm(*???*)),is,tac_), |
|
399 Form' (FormKF (~1, EdUndef, length p', Nundef, term2str r)), |
|
400 tac_2tac tac_, Sundef, pt) end |
|
401 *) |
|
402 | nxt_solv (End_Proof'') _ ptp = ([], [], ptp) |
|
403 |
|
404 | nxt_solv tac_ is (pt, pos as (p,p_)) = |
|
405 (* val (pt, pos as (p,p_)) = ptp; |
|
406 *) |
|
407 let val pos = case pos of |
|
408 (p, Met) => ((lev_on o lev_dn) p, Frm)(*begin script*) |
|
409 | (p, Res) => (lev_on p,Res) (*somewhere in script*) |
|
410 | _ => pos (*somewhere in script*) |
|
411 (*val _= writeln"### nxt_solv4 Apply_Method: stored is ="; |
|
412 val _= writeln(istate2str is);*) |
|
413 val (pos',c,_,pt) = generate1 (assoc_thy "Isac.thy") tac_ is pos pt; |
|
414 in ([(tac_2tac tac_, tac_, (pos,is))], c, (pt, pos')) end |
|
415 |
|
416 |
|
417 (*(p,p_), (([],Res),Uistate,Empty_Tac_), EmptyMout, Empty_Tac, Safe, pt*) |
|
418 |
|
419 |
|
420 (*.find the next tac from the script, nxt_solv will update the ptree.*) |
|
421 (* val (ptp as (pt,pos as (p,p_))) = ptp'; |
|
422 val (ptp as (pt, pos as (p,p_))) = ptp''; |
|
423 val (ptp as (pt, pos as (p,p_))) = ptp; |
|
424 val (ptp as (pt, pos as (p,p_))) = (pt,ip); |
|
425 val (ptp as (pt, pos as (p,p_))) = (pt, pos); |
|
426 *) |
|
427 and nxt_solve_ (ptp as (pt, pos as (p,p_))) = |
|
428 if e_metID = get_obj g_metID pt (par_pblobj pt p) |
|
429 then ([], [], (pt,(p,p_))):calcstate' |
|
430 else let val thy' = get_obj g_domID pt (par_pblobj pt p); |
|
431 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; |
|
432 val (tac_,is,(t,_)) = next_tac (thy',srls) (pt,pos) sc is; |
|
433 (*TODO here ^^^ return finished/helpless/ok !*) |
|
434 (* val (tac_',is',(t',_)) = next_tac (thy',srls) (pt,pos) sc is; |
|
435 *) |
|
436 in case tac_ of |
|
437 End_Detail' _ => ([(End_Detail, |
|
438 End_Detail' (t,[(*FIXME.040215*)]), |
|
439 (pos, is))], [], (pt, pos)) |
|
440 | _ => nxt_solv tac_ is ptp end; |
|
441 |
|
442 (*.says how may steps of a calculation should be done by "fun autocalc".*) |
|
443 (*TODO.WN0512 redesign togehter with autocalc ?*) |
|
444 datatype auto = |
|
445 Step of int (*1 do #int steps; may stop in model/specify: |
|
446 IS VERY INEFFICIENT IN MODEL/SPECIY*) |
|
447 | CompleteModel (*2 complete modeling |
|
448 if model complete, finish specifying + start solving*) |
|
449 | CompleteCalcHead (*3 complete model/specify in one go + start solving*) |
|
450 | CompleteToSubpbl (*4 stop at the next begin of a subproblem, |
|
451 if none, complete the actual (sub)problem*) |
|
452 | CompleteSubpbl (*5 complete the actual (sub)problem (incl.ev.subproblems)*) |
|
453 | CompleteCalc; (*6 complete the calculation as a whole*) |
|
454 fun autoord (Step _ ) = 1 |
|
455 | autoord CompleteModel = 2 |
|
456 | autoord CompleteCalcHead = 3 |
|
457 | autoord CompleteToSubpbl = 4 |
|
458 | autoord CompleteSubpbl = 5 |
|
459 | autoord CompleteCalc = 6; |
|
460 |
|
461 (* val (auto, c, (ptp as (_, p))) = (auto, (c@c'), ptp); |
|
462 *) |
|
463 fun complete_solve auto c (ptp as (_, p): ptree * pos') = |
|
464 if p = ([], Res) then ("end-of-calculation", [], ptp) else |
|
465 case nxt_solve_ ptp of |
|
466 ((Subproblem _, tac_, (_, is))::_, c', ptp') => |
|
467 (* val ptp' = ptp'''; |
|
468 *) |
|
469 if autoord auto < 5 then ("ok", c@c', ptp) |
|
470 else let val ptp = all_modspec ptp'; |
|
471 val (_, c'', ptp) = all_solve auto (c@c') ptp; |
|
472 in complete_solve auto (c@c'@c'') ptp end |
|
473 | ((Check_Postcond _, tac_, (_, is))::_, c', ptp' as (_, p')) => |
|
474 if autoord auto < 6 orelse p' = ([],Res) then ("ok", c@c', ptp') |
|
475 else complete_solve auto (c@c') ptp' |
|
476 | ((End_Detail, _, _)::_, c', ptp') => |
|
477 if autoord auto < 6 then ("ok", c@c', ptp') |
|
478 else complete_solve auto (c@c') ptp' |
|
479 | (_, c', ptp') => complete_solve auto (c@c') ptp' |
|
480 (* val (tacis, c', ptp') = nxt_solve_ ptp; |
|
481 val (tacis, c', ptp'') = nxt_solve_ ptp'; |
|
482 val (tacis, c', ptp''') = nxt_solve_ ptp''; |
|
483 val (tacis, c', ptp'''') = nxt_solve_ ptp'''; |
|
484 val (tacis, c', ptp''''') = nxt_solve_ ptp''''; |
|
485 *) |
|
486 and all_solve auto c (ptp as (pt, (p,_)): ptree * pos') = |
|
487 (* val (ptp as (pt, (p,_))) = ptp; |
|
488 val (ptp as (pt, (p,_))) = ptp'; |
|
489 val (ptp as (pt, (p,_))) = (pt, pos); |
|
490 *) |
|
491 let val (_,_,mI) = get_obj g_spec pt p; |
|
492 val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate)) |
|
493 e_istate ptp; |
|
494 in complete_solve auto (c@c') ptp end; |
|
495 (*@@@ vvv @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*) |
|
496 fun complete_solve auto c (ptp as (_, p as (_,p_)): ptree * pos') = |
|
497 if p = ([], Res) then ("end-of-calculation", [], ptp) else |
|
498 if member op = [Pbl,Met] p_ |
|
499 then let val ptp = all_modspec ptp |
|
500 val (_, c', ptp) = all_solve auto c ptp |
|
501 in complete_solve auto (c@c') ptp end |
|
502 else case nxt_solve_ ptp of |
|
503 ((Subproblem _, tac_, (_, is))::_, c', ptp') => |
|
504 if autoord auto < 5 then ("ok", c@c', ptp) |
|
505 else let val ptp = all_modspec ptp' |
|
506 val (_, c'', ptp) = all_solve auto (c@c') ptp |
|
507 in complete_solve auto (c@c'@c'') ptp end |
|
508 | ((Check_Postcond _, tac_, (_, is))::_, c', ptp' as (_, p')) => |
|
509 if autoord auto < 6 orelse p' = ([],Res) then ("ok", c@c', ptp') |
|
510 else complete_solve auto (c@c') ptp' |
|
511 | ((End_Detail, _, _)::_, c', ptp') => |
|
512 if autoord auto < 6 then ("ok", c@c', ptp') |
|
513 else complete_solve auto (c@c') ptp' |
|
514 | (_, c', ptp') => complete_solve auto (c@c') ptp' |
|
515 and all_solve auto c (ptp as (pt, (p,_)): ptree * pos') = |
|
516 let val (_,_,mI) = get_obj g_spec pt p |
|
517 val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate)) |
|
518 e_istate ptp |
|
519 in complete_solve auto (c@c') ptp end; |
|
520 |
|
521 (*.aux.fun for detailrls with Rrls, reverse rewriting.*) |
|
522 (* val (nds, t, ((rule, (t', asm)) :: rts)) = ([], t, rul_terms); |
|
523 *) |
|
524 fun rul_terms_2nds nds t [] = nds |
|
525 | rul_terms_2nds nds t ((rule, res as (t', _)) :: rts) = |
|
526 (append_atomic [] e_istate t (rule2tac [] rule) res Complete EmptyPtree) :: |
|
527 (rul_terms_2nds nds t' rts); |
|
528 |
|
529 |
|
530 (*. detail steps done internally by Rewrite_Set* |
|
531 into ctree by use of a script .*) |
|
532 (* val (pt, (p,p_)) = (pt, pos); |
|
533 *) |
|
534 fun detailrls pt ((p,p_):pos') = |
|
535 let val t = get_obj g_form pt p |
|
536 val tac = get_obj g_tac pt p |
|
537 val rls = (assoc_rls o rls_of) tac |
|
538 in case rls of |
|
539 (* val Rrls {scr = Rfuns {init_state,...},...} = rls; |
|
540 *) |
|
541 Rrls {scr = Rfuns {init_state,...},...} => |
|
542 let val (_,_,_,rul_terms) = init_state t |
|
543 val newnds = rul_terms_2nds [] t rul_terms |
|
544 val pt''' = ins_chn newnds pt p |
|
545 in ("detailrls", pt''', (p @ [length newnds], Res):pos') end |
|
546 | _ => |
|
547 let val is = init_istate tac t |
|
548 (*TODO.WN060602 ScrState (["(t_, Problem (Isac,[equation,univar]))"] |
|
549 is wrong for simpl, but working ?!? *) |
|
550 val tac_ = Apply_Method' (e_metID(*WN0402: see generate1 !?!*), |
|
551 SOME t, is) |
|
552 val pos' = ((lev_on o lev_dn) p, Frm) |
|
553 val thy = assoc_thy "Isac.thy" |
|
554 val (_,_,_,pt') = (*implicit Take*)generate1 thy tac_ is pos' pt |
|
555 val (_,_,(pt'',_)) = complete_solve CompleteSubpbl [] (pt',pos') |
|
556 val newnds = children (get_nd pt'' p) |
|
557 val pt''' = ins_chn newnds pt p |
|
558 (*complete_solve cuts branches after*) |
|
559 in ("detailrls", pt'''(*, get_formress [] ((lev_on o lev_dn) p)cn*), |
|
560 (p @ [length newnds], Res):pos') end |
|
561 end; |
|
562 |
|
563 |
|
564 |
|
565 (* val(mI,m)=m;val ppp=p;(*!!!*)val(p,p_)=pos;val(_,pt,_)=ppp(*!!!*); |
|
566 get_form ((mI,m):tac'_) ((p,p_):pos') ppp; |
|
567 *) |
|
568 fun get_form ((mI,m):tac'_) ((p,p_):pos') pt = |
|
569 case applicable_in (p,p_) pt m of |
|
570 Notappl e => Error' (Error_ e) |
|
571 | Appl m => |
|
572 (* val Appl m=applicable_in (p,p_) pt m; |
|
573 *) |
|
574 if member op = specsteps mI |
|
575 then let val (_,_,f,_,_,_) = specify m (p,p_) [] pt |
|
576 in f end |
|
577 else let val (*_,_,f,_,_,_*)_ = solve (mI,m) (pt,(p,p_)) |
|
578 in (*f*) EmptyMout end; |
|
579 |