2011-->2012: ...
modules ProgLang .. Frontend compile
thms renamed:
real_mult_assos --> mult_assoc
real_mult_commute --> mult_commute
1 (* use"ME/generate.sml";
5 (*.initialize istate for Detail_Set.*)
6 fun init_istate (Rewrite_Set rls) t =
7 (* val (Rewrite_Set rls) = (get_obj g_tac pt p);
10 Rrls {scr=sc as Rfuns {init_state=ii,...},...} => (RrlsState (ii t))
11 (* val Rrls {scr=sc as Rfuns {init_state=ii,...},...} = assoc_rls rls;
13 | Rls {scr=EmptyScr,...} =>
14 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
15 ^"use prep_rls for storing rule-sets !")
16 | Rls {scr = Prog s,...} =>
17 (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true))
18 | Seq {scr=EmptyScr,...} =>
19 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
20 ^"use prep_rls for storing rule-sets !")
21 | Seq {srls=srls,scr = Prog s,...} =>
22 (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true)))
23 (* val ((Rewrite_Set_Inst (subs, rls)), t) = ((get_obj g_tac pt p), t);
25 | init_istate (Rewrite_Set_Inst (subs, rls)) t =
26 let val (_, v)::_ = subs2subst (assoc_thy "Isac") subs
27 (*...we suppose the substitution of only _one_ bound variable*)
28 in case assoc_rls rls of
29 Rls {scr=EmptyScr,...} =>
30 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
31 ^"use prep_rls for storing rule-sets !")
32 | Rls {scr = Prog s,...} =>
33 let val (form, bdv) = two_scr_arg s
34 in (ScrState ([(form, t), (bdv, v)],[], NONE, e_term, Sundef,true))
36 | Seq {scr=EmptyScr,...} =>
37 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
38 ^"use prep_rls for storing rule-sets !")
39 | Seq {scr = Prog s,...} =>
40 let val (form, bdv) = two_scr_arg s
41 in (ScrState ([(form, t), (bdv, v)],[], NONE, e_term, Sundef,true))
46 (*.a taci holds alle information required to build a node in the calc-tree;
47 a taci is assumed to be used efficiently such that the calc-tree
48 resulting from applying a taci need not be stored separately;
49 see "type calcstate".*)
50 (*TODO.WN0504 redesign ??? or redesign generate ?? see "fun generate"
51 TODO.WN0512 ? redesign this _list_:
52 # only used for [Apply_Method + (Take or Subproblem)], i.e. for initacs
53 # the latter problem may be resolved automatically if "fun autocalc" is
54 not any more used for the specify-phase and for changing the phases*)
56 (tac * (*for comparison with input tac*)
57 tac_ * (*for ptree generation*)
58 (pos' * (*after applying tac_, for ptree generation*)
59 (istate * Proof.context))); (*after applying tac_, for ptree generation*)
60 val e_taci = (Empty_Tac, Empty_Tac_, (e_pos', (e_istate, e_ctxt))): taci;
61 (* val (tac, tac_, (pos', istate))::_ = tacis';
63 fun taci2str ((tac, tac_, (pos', (istate, _))):taci) =
64 "( "^tac2str tac^", "^tac_2str tac_^", ( "^pos'2str pos'
65 ^", "^istate2str istate^" ))";
66 fun tacis2str tacis = (strs2str o (map (linefeed o taci2str))) tacis;
68 datatype pblmet = (*%^%*)
70 | Problem of pblID (*%^%*)
71 | Method of metID; (*%^%*)
72 fun pblmet2str (Problem pblID) = "Problem "^(strs2str pblID)(*%^%*)
73 | pblmet2str (Method metID) = "Method "^(metID2str metID);(*%^%*)
74 (*%^%*) (*26.6. moved to sequent.sml: fun ~~~~~~~~~; was here below*)
77 (* copy from 03.60.usecases.sml 15.11.99 *)
79 Accept | NotAccept | Example
80 | YourTurn | MyTurn (* internal use only 7.6.02 java-sml*)
82 | DontKnow (*| HowComes | WhatFor 7.6.02 java-sml*)
83 | Undo (*| Back | Forward 7.6.02 java-sml*)
84 | EndProof | EndSession
85 | ActivePlus | ActiveMinus | SpeedPlus | SpeedMinus
86 (*Stepwidth...7.6.02 java-sml*)
87 | Auto | NotAuto | Details;
88 (* for test-print-outs *)
89 fun user_cmd2str Accept ="Accept"
90 | user_cmd2str NotAccept ="NotAccept"
91 | user_cmd2str Example ="Example"
92 | user_cmd2str MyTurn ="MyTurn"
93 | user_cmd2str YourTurn ="YourTurn"
94 | user_cmd2str Rules ="Rules"
95 (*| user_cmd2str HowComes ="HowComes"*)
96 | user_cmd2str DontKnow ="DontKnow"
97 (*| user_cmd2str WhatFor ="WhatFor"
98 | user_cmd2str Back ="Back"*)
99 | user_cmd2str Undo ="Undo"
100 (*| user_cmd2str Forward ="Forward"*)
101 | user_cmd2str EndProof ="EndProof"
102 | user_cmd2str EndSession ="EndSession"
103 | user_cmd2str ActivePlus = "ActivePlus"
104 | user_cmd2str ActiveMinus = "ActiveMinus"
105 | user_cmd2str SpeedPlus = "SpeedPlus"
106 | user_cmd2str SpeedMinus = "SpeedMinus"
107 | user_cmd2str Auto = "Auto"
108 | user_cmd2str NotAuto = "NotAuto"
109 | user_cmd2str Details = "Details";
113 (*3.5.00: TODO: foppFK eliminated in interface FE-KE !!!*)
114 datatype foppFK = (* in DG cases div 2 *)
115 EmptyFoppFK (*DG internal*)
117 | PpcFK of cterm' ppc;
118 fun foppFK2str (FormFK ct') ="FormFK "^ct'
119 | foppFK2str (PpcFK ppc) ="PpcFK "^(ppc2str ppc)
120 | foppFK2str EmptyFoppFK ="EmptyFoppFK";
123 datatype nest = Open | Closed | Nundef;
124 fun nest2str Open = "Open"
125 | nest2str Closed = "Closed"
126 | nest2str Nundef = "Nundef";
129 datatype edit = EdUndef | Write | Protect;
130 (* bridge --> kernel *)
131 (* bridge <-> kernel *)
132 (* needed in dialog.sml *) (* bridge <-- kernel *)
133 fun edit2str EdUndef = "EdUndef"
134 | edit2str Write = "Write"
135 | edit2str Protect = "Protect";
138 datatype inout = (*FIXME.WN1105 drop this: was required for proto0 with dialog in sml*)
139 New_User | End_User (*<->*)
140 | New_Proof | End_Proof (*<->*)
141 | Command of user_cmd (*-->*)
142 | Request of string | Message of string (*<--*)
143 | Error_ of string | System of string (*<--*)
144 | FoPpcFK of foppFK (*-->*)
145 | FormKF of cellID * edit * indent * nest * cterm' (*<--*)
146 | PpcKF of cellID * edit * indent * nest * (pblmet * item ppc) (*<--*)
147 | RuleFK of tac (*-->*)
148 | RuleKF of edit * tac (*<--*)
149 | RefinedKF of (pblID * ((itm list) * ((bool * term) list))) (*<--*)
150 | Select of tac list (*<--*)
151 | RefineKF of match list (*<--*)
152 | Speed of int (*<--*)
153 | Active of int (*<--*)
154 | Domain of domID; (*<--*)
156 fun inout2str End_Proof = "End_Proof"
157 | inout2str (Command user_cmd) = "Command "^(user_cmd2str user_cmd)
158 | inout2str (Request s) = "Request "^s
159 | inout2str (Message s) = "Message "^s
160 | inout2str (Error_ s) = "Error_ "^s
161 | inout2str (System s) = "System "^s
162 | inout2str (FoPpcFK foppFK) = "FoPpcFK "^(foppFK2str foppFK)
163 | inout2str (FormKF (cellID, edit, indent, nest, ct')) =
164 "FormKF ("^(string_of_int cellID)^","
165 ^(edit2str edit)^","^(string_of_int indent)^","
166 ^(nest2str nest)^",("
168 | inout2str (PpcKF (cellID, edit, indent, nest, (pm,itemppc))) =
169 "PpcKF ("^(string_of_int cellID)^","
170 ^(edit2str edit)^","^(string_of_int indent)^","
171 ^(nest2str nest)^",("
172 ^(pblmet2str pm)^","^(itemppc2str itemppc)^"))"
173 | inout2str (RuleKF (edit,tac)) = "RuleKF "^
174 pair2str(edit2str edit,tac2str tac)
175 | inout2str (RuleFK tac) = "RuleFK "^(tac2str tac)
176 | inout2str (Select tacs)=
177 "Select "^((strs2str' o (map tac2str)) tacs)
178 | inout2str (RefineKF ms) = "RefineKF "^(matchs2str ms)
179 | inout2str (Speed i) = "Speed "^(string_of_int i)
180 | inout2str (Active i) = "Active "^(string_of_int i)
181 | inout2str (Domain dI) = "Domain "^dI;
182 fun inouts2str ios = (strs2str' o (map inout2str)) ios;
185 Form' of inout (* packing cterm' | cterm' ppc *)
186 | Problems of inout (* passes specify (and solve) *)
190 fun mout2str (Form' inout) ="Form' "^(inout2str inout)
191 | mout2str (Error' inout) ="Error' "^(inout2str inout)
192 | mout2str (EmptyMout ) ="EmptyMout";
194 (*fun Form'2str (Form' )*)
200 (* init pbl with ...,dsc,empty | [] *)
203 fun pbt2itm (f, (d, t)) =
204 ((0, [], false, f, Inc ((d, []), (e_term, []))) : itm);
205 in map pbt2itm pbt end;
206 (*take formal parameters from pbt, for transfer from pbl/met-hierarchy*)
209 fun pbt2itm (f,(d,t)) =
210 ((0,[],false,f,Inc((d,[t]),(e_term,[]))):itm);
211 in map pbt2itm pbt end;
214 (*generate 1 ppobj in ptree*)
215 (*TODO.WN0501: take calcstate as an argument (see embed_derive etc.)?specify?*)
216 fun generate1 thy (Add_Given' (_, itmlist)) _ (pos as (p,p_)) pt =
217 (pos:pos',[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet, itms2itemppc thy [][]))),
219 Pbl => update_pbl pt p itmlist
220 | Met => update_met pt p itmlist)
221 (*WN110515 probably declare_constraints with input item (without dsc) --
222 -- important when specifying without formalisation*)
223 | generate1 thy (Add_Find' (_, itmlist)) _ (pos as (p,p_)) pt =
224 (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
226 Pbl => update_pbl pt p itmlist
227 | Met => update_met pt p itmlist)
228 (*WN110515 probably declare_constraints with input item (without dsc)*)
229 | generate1 thy (Add_Relation' (_, itmlist)) _ (pos as (p,p_)) pt =
230 (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
232 Pbl => update_pbl pt p itmlist
233 | Met => update_met pt p itmlist)
235 | generate1 thy (Specify_Theory' domID) _ (pos as (p,_)) pt =
236 (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
237 update_domID pt p domID)
239 | generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) _
241 let val pt = update_pbl pt p itms
242 val pt = update_pblID pt p pI
244 Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
247 | generate1 thy (Specify_Method' (mID, oris, itms)) _
249 let val pt = update_oris pt p oris
250 val pt = update_met pt p itms
251 val pt = update_metID pt p mID
253 Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
256 | generate1 thy (Model_Problem' (_, itms, met)) _ (pos as (p,_)) pt =
258 val pt = update_pbl pt p itms
259 val pt = update_met pt p met
260 in (pos,[],Form'(PpcKF(0,EdUndef,0,Nundef, (Upblmet, itms2itemppc thy [] []))), pt)
263 | generate1 thy (Refine_Tacitly' (pI,pIre,domID,metID,pbl))
264 _ (pos as (p,_)) pt =
265 let val pt = update_pbl pt p pbl
266 val pt = update_orispec pt p (domID,pIre,metID)
268 Form'(PpcKF(0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
271 | generate1 thy (Refine_Problem' (pI,_)) _ (pos as (p,_)) pt =
272 let val (dI,_,mI) = get_obj g_spec pt p
273 val pt = update_spec pt p (dI, pI, mI)
275 Form'(PpcKF(0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),pt)
278 | generate1 thy (Apply_Method' (_,topt, is, ctxt)) _ (pos as (p,p_)) pt =
279 ((*tracing("###generate1 Apply_Method': pos = "^pos'2str (p,p_));
280 tracing("###generate1 Apply_Method': topt= "^termopt2str topt);
281 tracing("###generate1 Apply_Method': is = "^istate2str is);*)
284 let val (pt,c) = cappend_form pt p (is, ctxt) t
285 (*val _= tracing("###generate1 Apply_Method: after cappend")*)
286 in (pos,c, EmptyMout,pt)
289 (pos,[],EmptyMout,update_env pt p (SOME (is, ctxt))))
290 (* val (thy, (Take' t), l, (p,p_), pt) =
291 ((assoc_thy "Isac"), tac_, is, pos, pt);
293 | generate1 thy (Take' t) l (p,p_) pt = (* val (Take' t) = m; *)
294 let (*val _=tracing("### generate1: Take' pos="^pos'2str (p,p_));*)
295 val p = let val (ps,p') = split_last p(*no connex to prev.ppobj*)
296 in if p'=0 then ps@[1] else p end;
297 val (pt,c) = cappend_form pt p l t;
299 Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str t)), pt) end
301 (* val (l, (p,p_)) = (RrlsState is, p);
303 val (thy, Begin_Trans' t, l, (p,Frm), pt) =
304 (assoc_thy "Isac", tac_, is, p, pt);
306 | generate1 thy (Begin_Trans' t) l (p,Frm) pt =
307 let (* print_depth 99;
308 map fst (get_interval ([],Pbl) ([],Res) 9999 pt);print_depth 3;
310 val (pt,c) = cappend_form pt p l t
312 map fst (get_interval ([],Pbl) ([],Res) 9999 pt);print_depth 3;
314 val pt = update_branch pt p TransitiveB (*040312*)
315 (*replace the old PrfOjb ~~~~~*)
316 val p = (lev_on o lev_dn(*starts with [...,0]*)) p;
317 val (pt,c') = cappend_form pt p l t(*FIXME.0402 same istate ???*);
318 in ((p,Frm), c @ c', Form' (FormKF (~1,EdUndef,(length p), Nundef,
319 term2str t)), pt) end
321 (* val (thy, Begin_Trans' t, l, (p,Res), pt) =
322 (assoc_thy "Isac", tac_, is, p, pt);
324 | generate1 thy (Begin_Trans' t) l (p ,Res) pt =
325 (*append after existing PrfObj _________*)
326 generate1 thy (Begin_Trans' t) l (lev_on p,Frm) pt
328 | generate1 thy (End_Trans' tasm) l (p,p_) pt =
331 val (pt,c) = append_result pt p' l tasm Complete;
332 in ((p',Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str t)), pt) end
334 | generate1 thy (Rewrite_Inst' (_,_,_,_,subs',thm',f,(f', asm))) (is, ctxt) (p,p_) pt =
336 val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
337 (Rewrite_Inst (subst2subs subs',thm')) (f',asm) Complete;
338 val pt = update_branch pt p TransitiveB
339 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end
341 | generate1 thy (Rewrite' (thy',ord',rls',pa,thm',f,(f',asm))) (is, ctxt) (p,p_) pt =
343 val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
344 (Rewrite thm') (f',asm) Complete
345 val pt = update_branch pt p TransitiveB
346 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end
348 | generate1 thy (Rewrite_Asm' all) l p pt = generate1 thy (Rewrite' all) l p pt
350 | generate1 thy (Rewrite_Set_Inst' (_,_,subs',rls',f,(f',asm))) (is, ctxt) (p,p_) pt =
352 val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
353 (Rewrite_Set_Inst (subst2subs subs',id_rls rls')) (f',asm) Complete
354 val pt = update_branch pt p TransitiveB
355 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end
357 | generate1 thy (Detail_Set_Inst' (_,_,subs,rls,f,(f',asm))) (is, ctxt) (p,p_) pt =
359 val ctxt' = insert_assumptions asm ctxt
360 val (pt,c) = cappend_form pt p (is, ctxt') f
361 val pt = update_branch pt p TransitiveB
363 val is = init_istate (Rewrite_Set_Inst (subst2subs subs, id_rls rls)) f
364 val tac_ = Apply_Method' (e_metID, SOME t, is, ctxt')
365 val pos' = ((lev_on o lev_dn) p, Frm)
366 in (*implicit Take*) generate1 thy tac_ (is, ctxt') pos' pt end
368 | generate1 thy (Rewrite_Set' (_,_,rls',f,(f',asm))) (is, ctxt) (p,p_) pt =
370 val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
371 (Rewrite_Set (id_rls rls')) (f',asm) Complete
372 val pt = update_branch pt p TransitiveB
373 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end
375 | generate1 thy (Detail_Set' (_,_,rls,f,(f',asm))) (is, ctxt) (p,p_) pt =
377 val ctxt' = insert_assumptions asm ctxt
378 val (pt,c) = cappend_form pt p (is, ctxt') f
379 val pt = update_branch pt p TransitiveB
381 val is = init_istate (Rewrite_Set (id_rls rls)) f
382 val tac_ = Apply_Method' (e_metID, SOME t, is, ctxt')
383 val pos' = ((lev_on o lev_dn) p, Frm)
384 in (*implicit Take*) generate1 thy tac_ (is, ctxt') pos' pt end
386 | generate1 thy (Check_Postcond' (pI, (scval, asm))) l (p,p_) pt =
387 let val (pt,c) = append_result pt p l (scval, asm) Complete
388 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str scval)), pt) end
390 | generate1 thy (Calculate' (thy',op_,f,(f',thm'))) l (p,p_) pt =
391 let val (pt,c) = cappend_atomic pt p l f (Calculate op_) (f',[]) Complete;
392 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end
394 | generate1 thy (Check_elementwise' (consts,pred,(f',asm))) l (p,p_) pt =
396 val (pt,c) = cappend_atomic pt p l consts (Check_elementwise pred) (f',asm) Complete;
397 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end
399 | generate1 thy (Or_to_List' (ors,list)) l (p,p_) pt =
400 let val (pt,c) = cappend_atomic pt p l ors Or_to_List (list,[]) Complete;
401 in ((p,Res), c, Form' (FormKF(~1,EdUndef,(length p), Nundef, term2str list)), pt) end
403 | generate1 thy (Substitute' (_, _, subte, t, t')) l (p,p_) pt =
406 cappend_atomic pt p l t (Substitute (subte2sube subte)) (t',[]) Complete;
407 in ((p,Res), c, Form' (FormKF(~1,EdUndef,(length p), Nundef, term2str t')), pt)
410 | generate1 thy (Tac_ (_,f,id,f')) l (p,p_) pt =
413 cappend_atomic pt p l (str2term f) (Tac id) (str2term f',[]) Complete;
414 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f')), pt)end
416 | generate1 thy (Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, ctxt, f)) l (p,p_) pt =
419 cappend_problem pt p l (fmz_, (domID, pblID, metID)) (oris, (domID, pblID, metID), hdl);
420 val pt = update_ctxt pt p ctxt
421 val f = Syntax.string_of_term (thy2ctxt thy) f;
422 in ((p,Pbl), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f)), pt) end
424 | generate1 thy m' _ _ _ =
425 error ("generate1: not impl.for "^(tac_2str m'));
427 fun generate_inconsistent_rew (subs_opt, thm') f' (is, ctxt) (pos as (p,_)) pt =
429 val f = get_curr_formula (pt, pos);
430 val pos' as (p', _) = (lev_on p, Res);
433 NONE => cappend_atomic pt p' (is, insert_assumptions [] ctxt) f
434 (Rewrite thm') (f', []) Inconsistent
435 | SOME subs => cappend_atomic pt p' (is, insert_assumptions [] ctxt) f
436 (Rewrite_Inst (subs, thm')) (f', []) Inconsistent
437 val pt = update_branch pt p' TransitiveB;
440 fun generate_hard thy m' (p,p_) pt =
444 Frm => p | Res => lev_on p
445 | _ => error ("generate_hard: call by " ^ pos'2str (p,p_));
446 in generate1 thy m' (e_istate, e_ctxt) (p,p_) pt end;
448 (*tacis are in reverse order from nxt_solve_/specify_: last = fst to insert*)
449 fun generate ([]: taci list) ptp = ptp
450 | generate tacis (pt, c, _:pos'(*!dropped!WN0504redesign generate/tacis?*))=
452 val (tacis', (_, tac_, (p, is))) = split_last tacis
453 val (p',c',_,pt') = generate1 (assoc_thy "Isac") tac_ is p pt
454 in generate tacis' (pt', c@c', p') end;
456 (*. a '_deriv'ation is constructed during 'reverse rewring' by an Rrls *
457 * of for connecting a user-input formula with the current calc-state. *
458 *# It is somewhat incompatible with the rest of the math-engine: *
459 * (1) it is not created by a script *
460 * (2) thus there cannot be another user-input within a derivation *
461 *# It suffers particularily from the not-well-foundedness of the math-engine*
462 * (1) FIXME other branchtyptes than Transitive will change 'embed_deriv' *
463 * (2) FIXME and eventually 'compare_step' (ie. the script interpreter) *
464 * (3) FIXME and eventually 'lev_back' *
465 *# SOME improvements are evident FIXME.040215 '_deriv'ation: *
466 * (1) FIXME nest Rls_ in 'make_deriv' *
467 * (2) FIXME do the not-reversed part in 'make_deriv' by scripts -- thus *
468 * user-input will become possible in this part of a derivation *
469 * (3) FIXME do (2) only if a derivation has been found -- for efficiency, *
470 * while a non-derivable inform requires to step until End_Proof' *
471 * (4) FIXME find criteria on when _not_ to step until End_Proof' *
474 (*.update pos in tacis for embedding by generate.*)
477 fun insert_pos _ [] = []
478 | insert_pos (p:pos) (((tac,tac_,(_, ist))::tacis):taci list) =
479 ((tac,tac_,((p, Res), ist)):taci)
480 ::((insert_pos (lev_on p) tacis):taci list);
482 fun res_from_taci (_, Rewrite'(_,_,_,_,_,_,(res, asm)), _) = (res, asm)
483 | res_from_taci (_, Rewrite_Set'(_,_,_,_,(res, asm)), _) = (res, asm)
484 | res_from_taci (_, tac_, _) =
485 error ("res_from_taci: called with" ^ tac_2str tac_);
487 (*.embed the tacis created by a '_deriv'ation; sys.form <> input.form
488 tacis are in order, thus are reverted for generate.*)
489 (* val (tacis, (pt, pos as (p, Frm))) = (tacis', ptp);
491 fun embed_deriv (tacis:taci list) (pt, pos as (p, Frm):pos') =
492 (*inform at Frm: replace the whole PrfObj by a Transitive-ProfObj FIXME?0402
493 and transfer the istate (from _after_ compare_deriv) from Frm to Res*)
494 let val (res, asm) = (res_from_taci o last_elem) tacis
495 val (SOME (ist, ctxt),_) = get_obj g_loc pt p
496 val form = get_obj g_form pt p
497 (*val p = lev_on p; ---------------only difference to (..,Res) below*)
498 val tacis = (Begin_Trans, Begin_Trans' form, (pos, (Uistate, ctxt)))
499 ::(insert_pos ((lev_on o lev_dn) p) tacis)
500 @ [(End_Trans, End_Trans' (res, asm),
501 (pos_plus (length tacis) (lev_dn p, Res),
502 (new_val res ist, ctxt)))]
503 val {nrls,...} = get_met (get_obj g_metID pt (par_pblobj pt p))
504 val (pt, c, pos as (p,_)) = generate (rev tacis) (pt, [], (p, Res))
505 val pt = update_tac pt p (Derive (id_rls nrls))
506 (*FIXME.040216 struct.ctree*)
507 val pt = update_branch pt p TransitiveB
508 in (c, (pt, pos:pos')) end
510 (* val (tacis, (pt, (p, Res))) = (tacis', ptp);
512 | embed_deriv tacis (pt, (p, Res)) =
513 (*inform at Res: append a Transitive-PrfObj FIXME?0402 other branch-types ?
514 and transfer the istate (from _after_ compare_deriv) from Res to new Res*)
515 let val (res, asm) = (res_from_taci o last_elem) tacis
516 val (_, SOME (ist, ctxt)) = get_obj g_loc pt p
517 val (f,a) = get_obj g_result pt p
518 val p = lev_on p(*---------------only difference to (..,Frm) above*);
519 val tacis = (Begin_Trans, Begin_Trans' f, ((p, Frm), (Uistate, ctxt)))
520 ::(insert_pos ((lev_on o lev_dn) p) tacis)
521 @ [(End_Trans, End_Trans' (res, asm),
522 (pos_plus (length tacis) (lev_dn p, Res),
523 (new_val res ist, ctxt)))];
524 val {nrls,...} = get_met (get_obj g_metID pt (par_pblobj pt p))
525 val (pt, c, pos as (p,_)) = generate (rev tacis) (pt, [], (p, Res))
526 val pt = update_tac pt p (Derive (id_rls nrls))
527 (*FIXME.040216 struct.ctree*)
528 val pt = update_branch pt p TransitiveB
529 in (c, (pt, pos)) end;