intermed. ctxt ..: x+1=2 now goes until Check_elementwise
1 (* use"ME/generate.sml";
5 (*.initialize istate for Detail_Set.*)
7 fun init_istate (Rewrite_Set rls) =
8 (* val (Rewrite_Set rls) = (get_obj g_tac pt p);
10 (case assoc_rls rls of
11 Rrls {scr=sc as Rfuns {init_state=ii,...},...} => (RrlsState (ii t))
12 (* val Rrls {scr=sc as Rfuns {init_state=ii,...},...} = assoc_rls rls;
14 | Rls {scr=EmptyScr,...} =>
15 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
16 ^"use prep_rls for storing rule-sets !")
17 | Rls {scr=Script s,...} =>
18 (* val Rls {scr=Script s,...} = assoc_rls rls;
20 (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true))
21 | Seq {scr=EmptyScr,...} =>
22 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
23 ^"use prep_rls for storing rule-sets !")
24 | Seq {srls=srls,scr=Script s,...} =>
25 (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true)))
26 | init_istate (Rewrite_Set_Inst (subs, rls)) =
27 (* val (Rewrite_Set_Inst (subs, rls)) = (get_obj g_tac pt p);
29 let val (_, v)::_ = subs2subst (assoc_thy "Isac") subs
30 in case assoc_rls rls of
31 Rls {scr=EmptyScr,...} =>
32 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
33 ^"use prep_rls for storing rule-sets !")
34 | Rls {scr=Script s,...} =>
35 let val (a1, a2) = two_scr_arg s
36 in (ScrState ([(a1, v), (a2, t)],[], NONE, e_term, Sundef,true)) end
37 | Seq {scr=EmptyScr,...} =>
38 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
39 ^"use prep_rls for storing rule-sets !")
40 (* val Seq {scr=Script s,...} = assoc_rls rls;
42 | Seq {scr=Script s,...} =>
43 let val (a1, a2) = two_scr_arg s
44 in (ScrState ([(a1, v), (a2, t)],[], NONE, e_term, Sundef,true)) end
47 (*~~~~~~~~~~~~~~~~~~~~~~copy for dev. until del.~~~~~~~~~~~~~~~~~~~~~~~~~*)
48 fun init_istate (Rewrite_Set rls) t =
49 (* val (Rewrite_Set rls) = (get_obj g_tac pt p);
51 (case assoc_rls rls of
52 Rrls {scr=sc as Rfuns {init_state=ii,...},...} => (RrlsState (ii t))
53 (* val Rrls {scr=sc as Rfuns {init_state=ii,...},...} = assoc_rls rls;
55 | Rls {scr=EmptyScr,...} =>
56 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
57 ^"use prep_rls for storing rule-sets !")
58 | Rls {scr=Script s,...} =>
59 (* val Rls {scr=Script s,...} = assoc_rls rls;
61 (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true))
62 | Seq {scr=EmptyScr,...} =>
63 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
64 ^"use prep_rls for storing rule-sets !")
65 | Seq {srls=srls,scr=Script s,...} =>
66 (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true)))
67 (* val ((Rewrite_Set_Inst (subs, rls)), t) = ((get_obj g_tac pt p), t);
69 | init_istate (Rewrite_Set_Inst (subs, rls)) t =
70 let val (_, v)::_ = subs2subst (assoc_thy "Isac") subs
71 (*...we suppose the substitution of only _one_ bound variable*)
72 in case assoc_rls rls of
73 Rls {scr=EmptyScr,...} =>
74 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
75 ^"use prep_rls for storing rule-sets !")
76 | Rls {scr=Script s,...} =>
77 let val (form, bdv) = two_scr_arg s
78 in (ScrState ([(form, t), (bdv, v)],[], NONE, e_term, Sundef,true))
80 | Seq {scr=EmptyScr,...} =>
81 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
82 ^"use prep_rls for storing rule-sets !")
83 (* val Seq {scr=Script s,...} = assoc_rls rls;
85 | Seq {scr=Script s,...} =>
86 let val (form, bdv) = two_scr_arg s
87 in (ScrState ([(form, t), (bdv, v)],[], NONE, e_term, Sundef,true))
92 (*.a taci holds alle information required to build a node in the calc-tree;
93 a taci is assumed to be used efficiently such that the calc-tree
94 resulting from applying a taci need not be stored separately;
95 see "type calcstate".*)
96 (*TODO.WN0504 redesign ??? or redesign generate ?? see "fun generate"
97 TODO.WN0512 ? redesign this _list_:
98 # only used for [Apply_Method + (Take or Subproblem)], i.e. for initacs
99 # the latter problem may be resolved automatically if "fun autocalc" is
100 not any more used for the specify-phase and for changing the phases*)
102 (tac * (*for comparison with input tac*)
103 tac_ * (*for ptree generation*)
104 (pos' * (*after applying tac_, for ptree generation*)
105 (istate * Proof.context))); (*after applying tac_, for ptree generation*)
106 val e_taci = (Empty_Tac, Empty_Tac_, (e_pos', (e_istate, e_ctxt))): taci;
107 (* val (tac, tac_, (pos', istate))::_ = tacis';
109 fun taci2str ((tac, tac_, (pos', (istate, _))):taci) =
110 "( "^tac2str tac^", "^tac_2str tac_^", ( "^pos'2str pos'
111 ^", "^istate2str istate^" ))";
112 fun tacis2str tacis = (strs2str o (map (linefeed o taci2str))) tacis;
114 datatype pblmet = (*%^%*)
115 Upblmet (*undefined*)
116 | Problem of pblID (*%^%*)
117 | Method of metID; (*%^%*)
118 fun pblmet2str (Problem pblID) = "Problem "^(strs2str pblID)(*%^%*)
119 | pblmet2str (Method metID) = "Method "^(metID2str metID);(*%^%*)
120 (*%^%*) (*26.6. moved to sequent.sml: fun ~~~~~~~~~; was here below*)
123 (* copy from 03.60.usecases.sml 15.11.99 *)
125 Accept | NotAccept | Example
126 | YourTurn | MyTurn (* internal use only 7.6.02 java-sml*)
128 | DontKnow (*| HowComes | WhatFor 7.6.02 java-sml*)
129 | Undo (*| Back | Forward 7.6.02 java-sml*)
130 | EndProof | EndSession
131 | ActivePlus | ActiveMinus | SpeedPlus | SpeedMinus
132 (*Stepwidth...7.6.02 java-sml*)
133 | Auto | NotAuto | Details;
134 (* for test-print-outs *)
135 fun user_cmd2str Accept ="Accept"
136 | user_cmd2str NotAccept ="NotAccept"
137 | user_cmd2str Example ="Example"
138 | user_cmd2str MyTurn ="MyTurn"
139 | user_cmd2str YourTurn ="YourTurn"
140 | user_cmd2str Rules ="Rules"
141 (*| user_cmd2str HowComes ="HowComes"*)
142 | user_cmd2str DontKnow ="DontKnow"
143 (*| user_cmd2str WhatFor ="WhatFor"
144 | user_cmd2str Back ="Back"*)
145 | user_cmd2str Undo ="Undo"
146 (*| user_cmd2str Forward ="Forward"*)
147 | user_cmd2str EndProof ="EndProof"
148 | user_cmd2str EndSession ="EndSession"
149 | user_cmd2str ActivePlus = "ActivePlus"
150 | user_cmd2str ActiveMinus = "ActiveMinus"
151 | user_cmd2str SpeedPlus = "SpeedPlus"
152 | user_cmd2str SpeedMinus = "SpeedMinus"
153 | user_cmd2str Auto = "Auto"
154 | user_cmd2str NotAuto = "NotAuto"
155 | user_cmd2str Details = "Details";
159 (*3.5.00: TODO: foppFK eliminated in interface FE-KE !!!*)
160 datatype foppFK = (* in DG cases div 2 *)
161 EmptyFoppFK (*DG internal*)
163 | PpcFK of cterm' ppc;
164 fun foppFK2str (FormFK ct') ="FormFK "^ct'
165 | foppFK2str (PpcFK ppc) ="PpcFK "^(ppc2str ppc)
166 | foppFK2str EmptyFoppFK ="EmptyFoppFK";
169 datatype nest = Open | Closed | Nundef;
170 fun nest2str Open = "Open"
171 | nest2str Closed = "Closed"
172 | nest2str Nundef = "Nundef";
175 datatype edit = EdUndef | Write | Protect;
176 (* bridge --> kernel *)
177 (* bridge <-> kernel *)
178 (* needed in dialog.sml *) (* bridge <-- kernel *)
179 fun edit2str EdUndef = "EdUndef"
180 | edit2str Write = "Write"
181 | edit2str Protect = "Protect";
185 New_User | End_User (*<->*)
186 | New_Proof | End_Proof (*<->*)
187 | Command of user_cmd (*-->*)
188 | Request of string | Message of string (*<--*)
189 | Error_ of string | System of string (*<--*)
190 | FoPpcFK of foppFK (*-->*)
191 | FormKF of cellID * edit * indent * nest * cterm' (*<--*)
192 | PpcKF of cellID * edit * indent * nest * (pblmet * item ppc) (*<--*)
193 | RuleFK of tac (*-->*)
194 | RuleKF of edit * tac (*<--*)
195 | RefinedKF of (pblID * ((itm list) * ((bool * term) list))) (*<--*)
196 | Select of tac list (*<--*)
197 | RefineKF of match list (*<--*)
198 | Speed of int (*<--*)
199 | Active of int (*<--*)
200 | Domain of domID; (*<--*)
202 fun inout2str End_Proof = "End_Proof"
203 | inout2str (Command user_cmd) = "Command "^(user_cmd2str user_cmd)
204 | inout2str (Request s) = "Request "^s
205 | inout2str (Message s) = "Message "^s
206 | inout2str (Error_ s) = "Error_ "^s
207 | inout2str (System s) = "System "^s
208 | inout2str (FoPpcFK foppFK) = "FoPpcFK "^(foppFK2str foppFK)
209 | inout2str (FormKF (cellID, edit, indent, nest, ct')) =
210 "FormKF ("^(string_of_int cellID)^","
211 ^(edit2str edit)^","^(string_of_int indent)^","
212 ^(nest2str nest)^",("
214 | inout2str (PpcKF (cellID, edit, indent, nest, (pm,itemppc))) =
215 "PpcKF ("^(string_of_int cellID)^","
216 ^(edit2str edit)^","^(string_of_int indent)^","
217 ^(nest2str nest)^",("
218 ^(pblmet2str pm)^","^(itemppc2str itemppc)^"))"
219 | inout2str (RuleKF (edit,tac)) = "RuleKF "^
220 pair2str(edit2str edit,tac2str tac)
221 | inout2str (RuleFK tac) = "RuleFK "^(tac2str tac)
222 | inout2str (Select tacs)=
223 "Select "^((strs2str' o (map tac2str)) tacs)
224 | inout2str (RefineKF ms) = "RefineKF "^(matchs2str ms)
225 | inout2str (Speed i) = "Speed "^(string_of_int i)
226 | inout2str (Active i) = "Active "^(string_of_int i)
227 | inout2str (Domain dI) = "Domain "^dI;
228 fun inouts2str ios = (strs2str' o (map inout2str)) ios;
231 Form' of inout (* packing cterm' | cterm' ppc *)
232 | Problems of inout (* passes specify (and solve) *)
236 fun mout2str (Form' inout) ="Form' "^(inout2str inout)
237 | mout2str (Error' inout) ="Error' "^(inout2str inout)
238 | mout2str (EmptyMout ) ="EmptyMout";
240 (*fun Form'2str (Form' )*)
246 (* init pbl with ...,dsc,empty | [] *)
249 fun pbt2itm (f, (d, t)) =
250 ((0, [], false, f, Inc ((d, []), (e_term, []))) : itm);
251 in map pbt2itm pbt end;
252 (*take formal parameters from pbt, for transfer from pbl/met-hierarchy*)
255 fun pbt2itm (f,(d,t)) =
256 ((0,[],false,f,Inc((d,[t]),(e_term,[]))):itm);
257 in map pbt2itm pbt end;
260 (*generate 1 ppobj in ptree*)
261 (*TODO.WN0501: take calcstate as an argument (see embed_derive etc.)?specify?*)
262 fun generate1 thy (Add_Given' (_, itmlist)) _ (pos as (p,p_)) pt =
263 (pos:pos',[],Form' (PpcKF (0,EdUndef,0,Nundef,
264 (Upblmet,itms2itemppc thy [][]))),
265 case p_ of Pbl => update_pbl pt p itmlist
266 | Met => update_met pt p itmlist)
267 | generate1 thy (Add_Find' (_, itmlist)) _ (pos as (p,p_)) pt =
268 (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
269 case p_ of Pbl => update_pbl pt p itmlist
270 | Met => update_met pt p itmlist)
271 | generate1 thy (Add_Relation' (_, itmlist)) _ (pos as (p,p_)) pt =
272 (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
273 case p_ of Pbl => update_pbl pt p itmlist
274 | Met => update_met pt p itmlist)
276 | generate1 thy (Specify_Theory' domID) _ (pos as (p,_)) pt =
277 (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
278 update_domID pt p domID)
280 | generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) _
282 let val pt = update_pbl pt p itms
283 val pt = update_pblID pt p pI
285 Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
288 | generate1 thy (Specify_Method' (mID, oris, itms)) _
290 let val pt = update_oris pt p oris
291 val pt = update_met pt p itms
292 val pt = update_metID pt p mID
294 Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
297 | generate1 thy (Model_Problem' (_, itms, met)) _ (pos as (p,_)) pt =
299 val pt = update_pbl pt p itms
300 val pt = update_met pt p met
301 in (pos,[],Form'(PpcKF(0,EdUndef,0,Nundef, (Upblmet, itms2itemppc thy [] []))), pt)
304 | generate1 thy (Refine_Tacitly' (pI,pIre,domID,metID,pbl))
305 _ (pos as (p,_)) pt =
306 let val pt = update_pbl pt p pbl
307 val pt = update_orispec pt p (domID,pIre,metID)
309 Form'(PpcKF(0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
312 | generate1 thy (Refine_Problem' (pI,_)) _ (pos as (p,_)) pt =
313 let val (dI,_,mI) = get_obj g_spec pt p
314 val pt = update_spec pt p (dI, pI, mI)
316 Form'(PpcKF(0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),pt)
319 | generate1 thy (Apply_Method' (_,topt, is, ctxt)) _ (pos as (p,p_)) pt =
320 ((*tracing("###generate1 Apply_Method': pos = "^pos'2str (p,p_));
321 tracing("###generate1 Apply_Method': topt= "^termopt2str topt);
322 tracing("###generate1 Apply_Method': is = "^istate2str is);*)
325 let val (pt,c) = cappend_form pt p (is, ctxt) t
326 (*val _= tracing("###generate1 Apply_Method: after cappend")*)
327 in (pos,c, EmptyMout,pt)
330 (pos,[],EmptyMout,update_env pt p (SOME (is, ctxt))))
331 (* val (thy, (Take' t), l, (p,p_), pt) =
332 ((assoc_thy "Isac"), tac_, is, pos, pt);
334 | generate1 thy (Take' t) l (p,p_) pt = (* val (Take' t) = m; *)
335 let (*val _=tracing("### generate1: Take' pos="^pos'2str (p,p_));*)
336 val p = let val (ps,p') = split_last p(*no connex to prev.ppobj*)
337 in if p'=0 then ps@[1] else p end;
338 val (pt,c) = cappend_form pt p l t;
340 Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str t)), pt) end
342 (* val (l, (p,p_)) = (RrlsState is, p);
344 val (thy, Begin_Trans' t, l, (p,Frm), pt) =
345 (assoc_thy "Isac", tac_, is, p, pt);
347 | generate1 thy (Begin_Trans' t) l (p,Frm) pt =
348 let (* print_depth 99;
349 map fst (get_interval ([],Pbl) ([],Res) 9999 pt);print_depth 3;
351 val (pt,c) = cappend_form pt p l t
353 map fst (get_interval ([],Pbl) ([],Res) 9999 pt);print_depth 3;
355 val pt = update_branch pt p TransitiveB (*040312*)
356 (*replace the old PrfOjb ~~~~~*)
357 val p = (lev_on o lev_dn(*starts with [...,0]*)) p;
358 val (pt,c') = cappend_form pt p l t(*FIXME.0402 same istate ???*);
359 in ((p,Frm), c @ c', Form' (FormKF (~1,EdUndef,(length p), Nundef,
360 term2str t)), pt) end
362 (* val (thy, Begin_Trans' t, l, (p,Res), pt) =
363 (assoc_thy "Isac", tac_, is, p, pt);
365 | generate1 thy (Begin_Trans' t) l (p ,Res) pt =
366 (*append after existing PrfObj _________*)
367 generate1 thy (Begin_Trans' t) l (lev_on p,Frm) pt
369 | generate1 thy (End_Trans' tasm) l (p,p_) pt =
370 let val p' = lev_up p
371 val (pt,c) = append_result pt p' l tasm Complete;
372 in ((p',Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str t)),
375 | generate1 thy (Rewrite_Inst' (_,_,_,_,subs',thm',f,(f',asm))) (is, ctxt)
377 let (*val _= tracing("###generate1 Rewrite_Inst': pos= "^pos'2str (p,p_));*)
378 val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
379 (Rewrite_Inst (subst2subs subs',thm')) (f',asm) Complete;
380 val pt = update_branch pt p TransitiveB (*040312*)
381 (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm);9.6.03??*)
382 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')),
385 | generate1 thy (Rewrite' (thy',ord',rls',pa,thm',f,(f',asm))) (is, ctxt)
387 let (*val _= tracing("###generate1 Rewrite': pos= "^pos'2str (p,p_))*)
388 val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
389 (Rewrite thm') (f',asm) Complete
390 val pt = update_branch pt p TransitiveB (*040312*)
391 (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm);9.6.03??*)
392 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')),
395 | generate1 thy (Rewrite_Asm' all) l p pt =
396 generate1 thy (Rewrite' all) l p pt
398 | generate1 thy (Rewrite_Set_Inst' (_,_,subs',rls',f,(f',asm))) (is, ctxt)
400 (* val (thy, Rewrite_Set_Inst' (_,_,subs',rls',f,(f',asm)), l, (p,p_), pt) =
401 (assoc_thy "Isac", tac_, is, pos, pt);
403 let (*val _=tracing("###generate1 Rewrite_Set_Inst': pos= "^pos'2str(p,p_))*)
404 val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
405 (Rewrite_Set_Inst (subst2subs subs',id_rls rls')) (f',asm) Complete
406 val pt = update_branch pt p TransitiveB (*040312*)
407 (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm');9.6.03??*)
408 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')),
411 | generate1 thy (Detail_Set_Inst' (_,_,subs,rls,f,(f',asm))) (is, ctxt) (p,p_)
413 let val ctxt' = insert_assumptions asm ctxt
414 val (pt,c) = cappend_form pt p (is, ctxt') f
415 val pt = update_branch pt p TransitiveB (*040312*)
416 val is = init_istate (Rewrite_Set_Inst (subst2subs subs, id_rls rls)) f
417 val tac_ = Apply_Method' (e_metID, SOME t, is, ctxt')
418 val pos' = ((lev_on o lev_dn) p, Frm)
419 in (*implicit Take*) generate1 thy tac_ (is, ctxt') pos' pt end
421 | generate1 thy (Rewrite_Set' (_,_,rls',f,(f',asm))) (is, ctxt) (p,p_) pt =
422 let (*val _= tracing("###generate1 Rewrite_Set': pos= "^pos'2str (p,p_))*)
423 val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
424 (Rewrite_Set (id_rls rls')) (f',asm) Complete
425 val pt = update_branch pt p TransitiveB (*040312*)
426 (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm');9.6.03??*)
427 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')),
430 | generate1 thy (Detail_Set' (_,_,rls,f,(f',asm))) (is, ctxt) (p,p_) pt =
431 let val (pt,c) = cappend_form pt p (is, ctxt) f
432 val pt = update_branch pt p TransitiveB (*040312*)
434 val is = init_istate (Rewrite_Set (id_rls rls)) f
435 val tac_ = Apply_Method' (e_metID, SOME t, is, ctxt)
436 val pos' = ((lev_on o lev_dn) p, Frm)
437 in (*implicit Take*) generate1 thy tac_ (is, ctxt) pos' pt end
439 | generate1 thy (Check_Postcond' (pI,(scval,asm))) l (p,p_) pt =
440 let (*val _=tracing("###generate1 Check_Postcond': pos= "^pos'2str(p,p_))*)
441 (*val (l',_) = get_obj g_loc pt p..don't overwrite with l from subpbl*)
442 val (pt,c) = append_result pt p l (scval,map str2term asm) Complete
443 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p),
444 Nundef, term2str scval)), pt) end
446 | generate1 thy (Calculate' (thy',op_,f,(f',thm'))) l (p,p_) pt =
447 let val (pt,c) = cappend_atomic pt p l f (Calculate op_) (f',[]) Complete;
448 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')),
451 | generate1 thy (Check_elementwise' (consts,pred,(f',asm))) l (p,p_) pt =
452 let(*val _=tracing("###generate1 Check_elementwise': p= "^pos'2str(p,p_))*)
453 val (pt,c) = cappend_atomic pt p l consts
454 (Check_elementwise pred) (f',asm) Complete;
455 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')),
458 | generate1 thy (Or_to_List' (ors,list)) l (p,p_) pt =
459 let val (pt,c) = cappend_atomic pt p l ors
460 Or_to_List (list,[]) Complete;
461 in ((p,Res), c, Form' (FormKF(~1,EdUndef,(length p), Nundef, term2str list)),
464 | generate1 thy (Substitute' (subte, t, t')) l (p,p_) pt =
467 cappend_atomic pt p l t (Substitute (subte2sube subte)) (t',[]) Complete;
468 in ((p,Res), c, Form' (FormKF(~1,EdUndef,(length p), Nundef, term2str t')), pt)
471 | generate1 thy (Tac_ (_,f,id,f')) l (p,p_) pt =
474 cappend_atomic pt p l (str2term f) (Tac id) (str2term f',[]) Complete;
475 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f')), pt)end
477 | generate1 thy (Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, ctxt, f))
479 let (*val _=tracing("###generate1 Subproblem': pos= "^pos'2str (p,p_))*)
481 cappend_problem pt p l (fmz_, (domID, pblID, metID)) (oris, (domID, pblID, metID), hdl);
482 val pt = update_ctxt pt p ctxt (*FIXME.WN110511*)
483 val f = Syntax.string_of_term (thy2ctxt thy) f;
484 in ((p,Pbl), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f)), pt) end
486 | generate1 thy m' _ _ _ =
487 error ("generate1: not impl.for "^(tac_2str m'))
491 fun generate_hard thy m' (p,p_) pt =
493 val p = case p_ of Frm => p | Res => lev_on p
494 | _ => error ("generate_hard: call by "^(pos'2str (p,p_)));
495 in generate1 thy m' (e_istate, e_ctxt) (p,p_) pt end;
499 (*tacis are in reverse order from nxt_solve_/specify_: last = fst to insert*)
500 (* val (tacis, (pt, _)) = (tacis, ptp);
502 val (tacis, (pt, c, _)) = (rev tacis, (pt, [], (p, Res)));
504 fun generate ([]: taci list) ptp = ptp
505 | generate tacis (pt, c, _:pos'(*!dropped!WN0504redesign generate/tacis?*))=
506 let val (tacis', (_, tac_, (p, is))) = split_last tacis
508 (tacis', (_, tac_, (p, is))) = split_last tacis';
510 val (p',c',_,pt') = generate1 (assoc_thy "Isac") tac_ is p pt
511 in generate tacis' (pt', c@c', p') end;
515 (*. a '_deriv'ation is constructed during 'reverse rewring' by an Rrls *
516 * of for connecting a user-input formula with the current calc-state. *
517 *# It is somewhat incompatible with the rest of the math-engine: *
518 * (1) it is not created by a script *
519 * (2) thus there cannot be another user-input within a derivation *
520 *# It suffers particularily from the not-well-foundedness of the math-engine*
521 * (1) FIXME other branchtyptes than Transitive will change 'embed_deriv' *
522 * (2) FIXME and eventually 'compare_step' (ie. the script interpreter) *
523 * (3) FIXME and eventually 'lev_back' *
524 *# SOME improvements are evident FIXME.040215 '_deriv'ation: *
525 * (1) FIXME nest Rls_ in 'make_deriv' *
526 * (2) FIXME do the not-reversed part in 'make_deriv' by scripts -- thus *
527 * user-input will become possible in this part of a derivation *
528 * (3) FIXME do (2) only if a derivation has been found -- for efficiency, *
529 * while a non-derivable inform requires to step until End_Proof' *
530 * (4) FIXME find criteria on when _not_ to step until End_Proof' *
533 (*.update pos in tacis for embedding by generate.*)
536 fun insert_pos _ [] = []
537 | insert_pos (p:pos) (((tac,tac_,(_, ist))::tacis):taci list) =
538 ((tac,tac_,((p, Res), ist)):taci)
539 ::((insert_pos (lev_on p) tacis):taci list);
541 fun res_from_taci (_, Rewrite'(_,_,_,_,_,_,(res, asm)), _) = (res, asm)
542 | res_from_taci (_, Rewrite_Set'(_,_,_,_,(res, asm)), _) = (res, asm)
543 | res_from_taci (_, tac_, _) =
544 error ("res_from_taci: called with" ^ tac_2str tac_);
546 (*.embed the tacis created by a '_deriv'ation; sys.form <> input.form
547 tacis are in order, thus are reverted for generate.*)
548 (* val (tacis, (pt, pos as (p, Frm))) = (tacis', ptp);
550 fun embed_deriv (tacis:taci list) (pt, pos as (p, Frm):pos') =
551 (*inform at Frm: replace the whole PrfObj by a Transitive-ProfObj FIXME?0402
552 and transfer the istate (from _after_ compare_deriv) from Frm to Res*)
553 let val (res, asm) = (res_from_taci o last_elem) tacis
554 val (SOME (ist, ctxt),_) = get_obj g_loc pt p
555 val form = get_obj g_form pt p
556 (*val p = lev_on p; ---------------only difference to (..,Res) below*)
557 val tacis = (Begin_Trans, Begin_Trans' form, (pos, (Uistate, ctxt)))
558 ::(insert_pos ((lev_on o lev_dn) p) tacis)
559 @ [(End_Trans, End_Trans' (res, asm),
560 (pos_plus (length tacis) (lev_dn p, Res),
561 (new_val res ist, ctxt)))]
562 val {nrls,...} = get_met (get_obj g_metID pt (par_pblobj pt p))
563 val (pt, c, pos as (p,_)) = generate (rev tacis) (pt, [], (p, Res))
564 val pt = update_tac pt p (Derive (id_rls nrls))
565 (*FIXME.040216 struct.ctree*)
566 val pt = update_branch pt p TransitiveB
567 in (c, (pt, pos:pos')) end
569 (* val (tacis, (pt, (p, Res))) = (tacis', ptp);
571 | embed_deriv tacis (pt, (p, Res)) =
572 (*inform at Res: append a Transitive-PrfObj FIXME?0402 other branch-types ?
573 and transfer the istate (from _after_ compare_deriv) from Res to new Res*)
574 let val (res, asm) = (res_from_taci o last_elem) tacis
575 val (_, SOME (ist, ctxt)) = get_obj g_loc pt p
576 val (f,a) = get_obj g_result pt p
577 val p = lev_on p(*---------------only difference to (..,Frm) above*);
578 val tacis = (Begin_Trans, Begin_Trans' f, ((p, Frm), (Uistate, ctxt)))
579 ::(insert_pos ((lev_on o lev_dn) p) tacis)
580 @ [(End_Trans, End_Trans' (res, asm),
581 (pos_plus (length tacis) (lev_dn p, Res),
582 (new_val res ist, ctxt)))];
583 val {nrls,...} = get_met (get_obj g_metID pt (par_pblobj pt p))
584 val (pt, c, pos as (p,_)) = generate (rev tacis) (pt, [], (p, Res))
585 val pt = update_tac pt p (Derive (id_rls nrls))
586 (*FIXME.040216 struct.ctree*)
587 val pt = update_branch pt p TransitiveB
588 in (c, (pt, pos)) end;