1 (* use"ME/generate.sml";
4 (*.initialize istate for Detail_Set.*)
5 fun init_istate (Rewrite_Set rls) =
7 Rrls {scr=sc as Rfuns {init_state=ii,...},...} => (RrlsState (ii t))
8 | Rls {scr=Script s,...} =>
9 (* val Rls {scr=Script s,...} = assoc_rls rls;
11 (ScrState ([(one_scr_arg s, t)], [], None, e_term, Sundef, true))
12 | Seq {srls=srls,scr=Script s,...} =>
13 (ScrState ([(one_scr_arg s, t)], [], None, e_term, Sundef, true)))
14 | init_istate (Rewrite_Set_Inst (subs, rls)) =
15 let val (_, v)::_ = subs2subst (assoc_thy "Isac.thy") subs
16 in case assoc_rls rls of
17 Rls {scr=Script s,...} =>
18 let val (a1, a2) = two_scr_arg s
19 in (ScrState ([(a1, v), (a2, t)],[], None, e_term, Sundef,true)) end
20 | Seq {scr=Script s,...} =>
21 let val (a1, a2) = two_scr_arg s
22 in (ScrState ([(a1, v), (a2, t)],[], None, e_term, Sundef,true)) end
26 (tac * (*for comparison with input tac*)
27 tac_ * (*for ptree generation*)
28 (pos' * (*after applying tac_, for ptree generation*)
29 istate)); (*after applying tac_, for ptree generation*)
30 val e_taci = (Empty_Tac, Empty_Tac_, (e_pos', e_istate)): taci;
31 (* val (tac, tac_, (pos', istate))::_ = tacis';
33 fun taci2str ((tac, tac_, (pos', istate)):taci) =
34 "( "^tac2str tac^", "^tac_2str tac_^", ( "^pos'2str pos'
35 ^", "^istate2str istate^" ))";
36 fun tacis2str tacis = (strs2str o (map (linefeed o taci2str))) tacis;
38 datatype pblmet = (*%^%*)
40 | Problem of pblID (*%^%*)
41 | Method of metID; (*%^%*)
42 fun pblmet2str (Problem pblID) = "Problem "^(strs2str pblID)(*%^%*)
43 | pblmet2str (Method metID) = "Method "^(metID2str metID);(*%^%*)
44 (*%^%*) (*26.6. moved to sequent.sml: fun ~~~~~~~~~; was here below*)
47 (* copy from 03.60.usecases.sml 15.11.99 *)
49 Accept | NotAccept | Example
50 | YourTurn | MyTurn (* internal use only 7.6.02 java-sml*)
52 | DontKnow (*| HowComes | WhatFor 7.6.02 java-sml*)
53 | Undo (*| Back | Forward 7.6.02 java-sml*)
54 | EndProof | EndSession
55 | ActivePlus | ActiveMinus | SpeedPlus | SpeedMinus
56 (*Stepwidth...7.6.02 java-sml*)
57 | Auto | NotAuto | Details;
58 (* for test-print-outs *)
59 fun user_cmd2str Accept ="Accept"
60 | user_cmd2str NotAccept ="NotAccept"
61 | user_cmd2str Example ="Example"
62 | user_cmd2str MyTurn ="MyTurn"
63 | user_cmd2str YourTurn ="YourTurn"
64 | user_cmd2str Rules ="Rules"
65 (*| user_cmd2str HowComes ="HowComes"*)
66 | user_cmd2str DontKnow ="DontKnow"
67 (*| user_cmd2str WhatFor ="WhatFor"
68 | user_cmd2str Back ="Back"*)
69 | user_cmd2str Undo ="Undo"
70 (*| user_cmd2str Forward ="Forward"*)
71 | user_cmd2str EndProof ="EndProof"
72 | user_cmd2str EndSession ="EndSession"
73 | user_cmd2str ActivePlus = "ActivePlus"
74 | user_cmd2str ActiveMinus = "ActiveMinus"
75 | user_cmd2str SpeedPlus = "SpeedPlus"
76 | user_cmd2str SpeedMinus = "SpeedMinus"
77 | user_cmd2str Auto = "Auto"
78 | user_cmd2str NotAuto = "NotAuto"
79 | user_cmd2str Details = "Details";
83 (*3.5.00: TODO: foppFK eliminated in interface FE-KE !!!*)
84 datatype foppFK = (* in DG cases div 2 *)
85 EmptyFoppFK (*DG internal*)
87 | PpcFK of cterm' ppc;
88 fun foppFK2str (FormFK ct') ="FormFK "^ct'
89 | foppFK2str (PpcFK ppc) ="PpcFK "^(ppc2str ppc)
90 | foppFK2str EmptyFoppFK ="EmptyFoppFK";
93 datatype nest = Open | Closed | Nundef;
94 fun nest2str Open = "Open"
95 | nest2str Closed = "Closed"
96 | nest2str Nundef = "Nundef";
99 datatype edit = EdUndef | Write | Protect;
100 (* bridge --> kernel *)
101 (* bridge <-> kernel *)
102 (* needed in dialog.sml *) (* bridge <-- kernel *)
103 fun edit2str EdUndef = "EdUndef"
104 | edit2str Write = "Write"
105 | edit2str Protect = "Protect";
109 New_User | End_User (*<->*)
110 | New_Proof | End_Proof (*<->*)
111 | Command of user_cmd (*-->*)
112 | Request of string | Message of string (*<--*)
113 | Error_ of string | System of string (*<--*)
114 | FoPpcFK of foppFK (*-->*)
115 | FormKF of cellID * edit * indent * nest * cterm' (*<--*)
116 | PpcKF of cellID * edit * indent * nest * (pblmet * item ppc) (*<--*)
117 | RuleFK of tac (*-->*)
118 | RuleKF of edit * tac (*<--*)
119 | RefinedKF of (pblID * ((itm list) * ((bool * term) list))) (*<--*)
120 | Select of tac list (*<--*)
121 | RefineKF of match list (*<--*)
122 | Speed of int (*<--*)
123 | Active of int (*<--*)
124 | Domain of domID; (*<--*)
126 fun inout2str End_Proof = "End_Proof"
127 | inout2str (Command user_cmd) = "Command "^(user_cmd2str user_cmd)
128 | inout2str (Request s) = "Request "^s
129 | inout2str (Message s) = "Message "^s
130 | inout2str (Error_ s) = "Error_ "^s
131 | inout2str (System s) = "System "^s
132 | inout2str (FoPpcFK foppFK) = "FoPpcFK "^(foppFK2str foppFK)
133 | inout2str (FormKF (cellID, edit, indent, nest, ct')) =
134 "FormKF ("^(string_of_int cellID)^","
135 ^(edit2str edit)^","^(string_of_int indent)^","
136 ^(nest2str nest)^",("
138 | inout2str (PpcKF (cellID, edit, indent, nest, (pm,itemppc))) =
139 "PpcKF ("^(string_of_int cellID)^","
140 ^(edit2str edit)^","^(string_of_int indent)^","
141 ^(nest2str nest)^",("
142 ^(pblmet2str pm)^","^(itemppc2str itemppc)^"))"
143 | inout2str (RuleKF (edit,tac)) = "RuleKF "^
144 pair2str(edit2str edit,tac2str tac)
145 | inout2str (RuleFK tac) = "RuleFK "^(tac2str tac)
146 | inout2str (Select tacs)=
147 "Select "^((strs2str' o (map tac2str)) tacs)
148 | inout2str (RefineKF ms) = "RefineKF "^(matchs2str ms)
149 | inout2str (Speed i) = "Speed "^(string_of_int i)
150 | inout2str (Active i) = "Active "^(string_of_int i)
151 | inout2str (Domain dI) = "Domain "^dI;
152 fun inouts2str ios = (strs2str' o (map inout2str)) ios;
155 Form' of inout (* packing cterm' | cterm' ppc *)
156 | Problems of inout (* passes specify (and solve) *)
160 fun mout2str (Form' inout) ="Form' "^(inout2str inout)
161 | mout2str (Error' inout) ="Error' "^(inout2str inout)
162 | mout2str (EmptyMout ) ="EmptyMout";
164 (*fun Form'2str (Form' )*)
170 (* init pbl with ...,dsc,empty | [] *)
173 fun pbt2itm (f,(d,t)) =
174 ((0,[],false,f,Inc((d,[]),(e_term,[]))):itm);
175 in map pbt2itm pbt end;
176 (*take formal parameters from pbt, for transfer from pbl/met-hierarchy*)
179 fun pbt2itm (f,(d,t)) =
180 ((0,[],false,f,Inc((d,[t]),(e_term,[]))):itm);
181 in map pbt2itm pbt end;
184 (*generate 1 ppobj in ptree*)
185 fun generate1 thy (Add_Given' (_, itmlist)) Uistate (pos as (p,p_)) pt =
186 (pos:pos',[],Form' (PpcKF (0,EdUndef,0,Nundef,
187 (Upblmet,itms2itemppc thy [][]))),
188 case p_ of Pbl => update_pbl pt p itmlist
189 | Met => update_met pt p itmlist)
190 | generate1 thy (Add_Find' (_, itmlist)) Uistate (pos as (p,p_)) pt =
191 (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
192 case p_ of Pbl => update_pbl pt p itmlist
193 | Met => update_met pt p itmlist)
194 | generate1 thy (Add_Relation' (_, itmlist)) Uistate (pos as (p,p_)) pt =
195 (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
196 case p_ of Pbl => update_pbl pt p itmlist
197 | Met => update_met pt p itmlist)
199 | generate1 thy (Specify_Theory' domID) Uistate (pos as (p,_)) pt =
200 (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
201 update_domID pt p domID)
203 | generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) Uistate
205 let val pt = update_pbl pt p itms
206 val pt = update_pblID pt p pI
208 Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
211 | generate1 thy (Specify_Method' (mID, oris, itms)) Uistate
213 let val pt = update_oris pt p oris
214 val pt = update_met pt p itms
215 val pt = update_metID pt p mID
217 Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
220 | generate1 thy (Model_Problem' (_, itms)) Uistate (pos as (p,_)) pt =
221 (* val (itms,pos as (p,_)) = (pbl, pos);
223 let val pt = update_pbl pt p itms
224 in (pos,[],Form'(PpcKF(0,EdUndef,0,Nundef,
225 (Upblmet,itms2itemppc thy [][]))), pt) end
227 | generate1 thy (Refine_Tacitly' (pI,pIre,domID,metID,pbl))
228 Uistate (pos as (p,_)) pt =
229 let val pt = update_pbl pt p pbl
230 val pt = update_orispec pt p (domID,pIre,metID)
232 Form'(PpcKF(0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
235 | generate1 thy (Refine_Problem' (pI,_)) Uistate (pos as (p,_)) pt =
236 let val (dI,_,mI) = get_obj g_spec pt p
237 val pt = update_spec pt p (dI, pI, mI)
239 Form'(PpcKF(0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),pt)
242 | generate1 thy (Apply_Method' (_,topt, is)) _ (pos as (p,p_)) pt =
243 (writeln("###generate1 Apply_Method': pos= "^pos'2str (p,p_));
246 let val (pt,_) = cappend_form pt p is t
247 in (pos,[(*WN0502: pblnd generated without children*)], EmptyMout,pt)
250 (pos,[],EmptyMout,update_env pt p (Some is)))
252 | generate1 thy (Take' t) l (p,p_) pt = (* val (Take' t) = m; *)
253 let val p = let val (ps,p') = split_last p(*no connex to prev.ppobj*)
254 in if p'=0 then ps@[1] else p end;
255 val (pt,c) = cappend_form pt p l t;
257 Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str t)), pt) end
259 (* val (l, (p,p_)) = (RrlsState is, p);
261 | generate1 thy (Begin_Trans' t) l (p,Frm) pt =
262 let val (pt,c) = cappend_form pt p l t
263 val pt = update_branch pt p TransitiveB (*040312*)
264 (*replace the old PrfOjb ~~~~~*)
265 val p = (lev_on o lev_dn(*starts with [...,0]*)) p;
266 val (pt,c) = cappend_form pt p l t;(*FIXME.0402 same istate ???*)
267 in ((p,Frm), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str t)),
270 | generate1 thy (Begin_Trans' t) l (p ,Res) pt =
271 (*append after existing PrfObj _________*)
272 generate1 thy (Begin_Trans' t) l (lev_on p,Frm) pt
274 | generate1 thy (End_Trans' tasm) l (p,p_) pt =
275 let val p' = lev_up p
276 val (pt,c) = append_result pt p' l tasm Complete;
277 in ((p',Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str t)),
280 | generate1 thy (Rewrite_Inst' (_,_,_,_,subs',thm',f,(f',asm))) l (p,p_) pt =
281 let val _= writeln("###generate1 Rewrite_Inst': pos= "^pos'2str (p,p_));
282 val (pt,c) = cappend_atomic pt p l f
283 (Rewrite_Inst (subst2subs subs',thm')) (f',asm) Complete;
284 val pt = update_branch pt p TransitiveB (*040312*)
285 (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm);9.6.03??*)
286 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')),
289 | generate1 thy (Rewrite' (thy',ord',rls',pa,thm',f,(f',asm))) l (p,p_) pt =
290 let val _= writeln("###generate1 Rewrite': pos= "^pos'2str (p,p_))
291 val (pt,c) = cappend_atomic pt p l f (Rewrite thm') (f',asm) Complete
292 val pt = update_branch pt p TransitiveB (*040312*)
293 (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm);9.6.03??*)
294 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')),
297 | generate1 thy (Rewrite_Asm' all) l p pt =
298 generate1 thy (Rewrite' all) l p pt
300 | generate1 thy (Rewrite_Set_Inst' (_,_,subs',rls',f,(f',asm))) l (p,p_) pt =
301 (* val (thy, Rewrite_Set_Inst' (_,_,subs',rls',f,(f',asm)), l, (p,p_), pt) =
302 (assoc_thy "Isac.thy", tac_, is, pos, pt);
304 let val _= writeln("###generate1 Rewrite_Set_Inst': pos= "^pos'2str (p,p_))
305 val (pt,c) = cappend_atomic pt p l f
306 (Rewrite_Set_Inst (subst2subs subs',id_rls rls')) (f',asm) Complete
307 val pt = update_branch pt p TransitiveB (*040312*)
308 (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm');9.6.03??*)
309 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')),
312 | generate1 thy (Detail_Set_Inst' (_,_,subs,rls,f,(f',asm))) l (p,p_) pt =
313 let val (pt,c) = cappend_form pt p l f
314 val pt = update_branch pt p TransitiveB (*040312*)
316 val is = init_istate (Rewrite_Set_Inst (subst2subs subs, id_rls rls))
317 val tac_ = Apply_Method' (e_metID, Some t, is)
318 val pos' = ((lev_on o lev_dn) p, Frm)
319 in (*implicit Take*) generate1 thy tac_ is pos' pt end
321 | generate1 thy (Rewrite_Set' (_,_,rls',f,(f',asm))) l (p,p_) pt =
322 let val _= writeln("###generate1 Rewrite_Set': pos= "^pos'2str (p,p_))
323 val (pt,c) = cappend_atomic pt p l f
324 (Rewrite_Set (id_rls rls')) (f',asm) Complete
325 val pt = update_branch pt p TransitiveB (*040312*)
326 (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm');9.6.03??*)
327 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')),
330 | generate1 thy (Detail_Set' (_,_,rls,f,(f',asm))) l (p,p_) pt =
331 let val (pt,c) = cappend_form pt p l f
332 val pt = update_branch pt p TransitiveB (*040312*)
334 val is = init_istate (Rewrite_Set (id_rls rls))
335 val tac_ = Apply_Method' (e_metID, Some t, is)
336 val pos' = ((lev_on o lev_dn) p, Frm)
337 in (*implicit Take*) generate1 thy tac_ is pos' pt end
339 | generate1 thy (Check_Postcond' (pI,(scval,asm))) l (p,p_) pt =
340 let val _= writeln("###generate1 Check_Postcond': pos= "^pos'2str (p,p_))
341 (*val (l',_) = get_obj g_loc pt p..don't overwrite with l from subpbl*)
342 val (pt,c) = append_result pt p l (scval,map str2term asm) Complete
343 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p),
344 Nundef, term2str scval)), pt) end
346 | generate1 thy (Calculate' (thy',op_,f,(f',thm'))) l (p,p_) pt =
347 let val (pt,c) = cappend_atomic pt p l f (Calculate op_) (f',[]) Complete;
348 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')),
351 | generate1 thy (Check_elementwise' (consts,pred,(f',asm))) l (p,p_) pt =
352 let val _=writeln("###generate1 Check_elementwise': pos= "^pos'2str (p,p_))
353 val (pt,c) = cappend_atomic pt p l consts
354 (Check_elementwise pred) (f',asm) Complete;
355 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')),
358 | generate1 thy (Or_to_List' (ors,list)) l (p,p_) pt =
359 let val (pt,c) = cappend_atomic pt p l ors
360 Or_to_List (list,[]) Complete;
361 in ((p,Res), c, Form' (FormKF(~1,EdUndef,(length p), Nundef, term2str list)),
364 | generate1 thy (Tac_ (_,f,id,f')) l (p,p_) pt =
365 let val (pt,c) = cappend_atomic pt p l (str2term f)
366 (Tac id) (str2term f',[]) Complete;
367 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f')), pt)end
369 | generate1 thy (Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, f))
371 let val _=writeln("###generate1 Subproblem': pos= "^pos'2str (p,p_))
372 val (pt,c) = cappend_problem pt p l (fmz_, (domID, pblID, metID))
373 (oris, (domID, pblID, metID), hdl);
374 (*val pbl = init_pbl ((#ppc o get_pbt) pblID);
375 val pt = update_pblppc pt p pbl;--------4.9.03->Model_Problem*)
376 (*val _= writeln("### generate1: is([3],Frm)= "^
377 (istate2str (get_istate pt ([3],Frm))));*)
378 val f = Sign.string_of_term (sign_of thy) f;
379 in ((p,Pbl), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f)), pt) end
381 | generate1 thy m' _ _ _ =
382 raise error ("generate1: not impl.for "^(tac_2str m'))
386 fun generate_hard thy m' (p,p_) pt =
388 val p = case p_ of Frm => p | Res => lev_on p
389 | _ => raise error ("generate_hard: call by "^(pos'2str (p,p_)));
390 in generate1 thy m' e_istate (p,p_) pt end;
392 (*tacis are in reverse order from nxt_solve_/specify_: last = hd*)
393 fun generate ([]: taci list) ptp =
394 (writeln("### generate END-------------------------------");
396 (* val (tacis, (pt, _)) = (tacis, ptp);
398 | generate tacis (pt, c, _:pos'(*!!dropped!!*)) =
399 let val (tacis', (_, tac_, (p, is))) = split_last tacis
400 val (p',c',_,pt') = generate1 (assoc_thy "Isac.thy") tac_ is p pt
401 in generate tacis' (pt', c@c', p') end;
405 (*. a '_deriv'ation is constructed during 'reverse rewring' by an Rrls *
406 * of for connecting a user-input formula with the current calc-state. *
407 *# It is somewhat incompatible with the rest of the math-engine: *
408 * (1) it is not created by a script *
409 * (2) thus there cannot be another user-input within a derivation *
410 *# It suffers particularily from the not-well-foundedness of the math-engine*
411 * (1) FIXME other branchtyptes than Transitive will change 'embed_deriv' *
412 * (2) FIXME and eventually 'compare_step' (ie. the script interpreter) *
413 * (3) FIXME and eventually 'lev_back' *
414 *# Some improvements are evident FIXME.040215 '_deriv'ation: *
415 * (1) FIXME nest Rls_ in 'make_deriv' *
416 * (2) FIXME do the not-reversed part in 'make_deriv' by scripts -- thus *
417 * user-input will become possible in this part of a derivation *
418 * (3) FIXME do (2) only if a derivation has been found -- for efficiency, *
419 * while a non-derivable inform requires to step until End_Proof' *
420 * (4) FIXME find criteria on when _not_ to step until End_Proof' *
423 (*.update pos in tacis for embedding by generate.*)
426 fun insert_pos _ [] = []
427 | insert_pos (p:pos) (((tac,tac_,(_, ist))::tacis):taci list) =
428 ((tac,tac_,((p, Res), ist)):taci)
429 ::((insert_pos (lev_on p) tacis):taci list);
431 (*.embed the tacis created by a '_deriv'ation;
432 tacis are in order, thus are reverted for generate.*)
433 (* val (tacis, (pt, pos as (p, Frm))) = (tacis', ptp);
435 fun embed_deriv (*[] ptp = ptp ...sys.form = input.form... excluded in inform
436 | embed_deriv *)tacis (pt, pos as (p, Frm)) =
437 (*inform at Frm: replace the whole PrfObj by a Transitive-ProfObj FIXME?0402
438 and transfer the istate (from _after_ compare_deriv) from Frm to Res*)
439 let val (_, Rewrite'(_,_,_,_,_,_,(res, asm)), _) = last_elem tacis
440 val (Some ist,_) = get_obj g_loc pt p
441 val form = get_obj g_form pt p
442 (*val p = lev_on p; ---------------only difference*)
443 val tacis = (Begin_Trans, Begin_Trans' form, (pos, Uistate))
444 ::(insert_pos ((lev_on o lev_dn) p) tacis)
445 @ [(End_Trans, End_Trans' (res, asm),
446 (pos_plus (length tacis) (lev_dn p, Res),
448 val {nrls,...} = get_met (get_obj g_metID pt (par_pblobj pt p))
449 val (pt, c, pos as (p,_)) = generate (rev tacis) (pt, [], (p, Res))
450 val pt = update_tac pt p (Derive (id_rls nrls))
451 (*FIXME.040216 struct.ctree*)
452 val pt = update_branch pt p TransitiveB
453 in (c, (pt, pos)) end
455 (* val (tacis, (pt, pos as (p, Res))) = (tacis', ptp);
457 | embed_deriv tacis (pt, (p, Res)) =
458 (*inform at Res: append a Transitive-ProfObj FIXME?0402 other branch-types ?
459 and transfer the istate (from _after_ compare_deriv) from Res to new Res*)
460 let val (_, Rewrite'(_,_,_,_,_,_,(res, asm)), _) = last_elem tacis;
461 val (_, Some ist) = get_obj g_loc pt p
462 val (f,a) = get_obj g_result pt p
463 val p = lev_on p;(*---------------only difference*)
464 val tacis = (Begin_Trans, Begin_Trans' f, ((p, Frm), Uistate))
465 ::(insert_pos ((lev_on o lev_dn) p) tacis)
466 @ [(End_Trans, End_Trans' (res, asm),
467 (pos_plus (length tacis) (lev_dn p, Res),
469 val {nrls,...} = get_met (get_obj g_metID pt (par_pblobj pt p))
470 val (pt, c, pos as (p,_)) = generate (rev tacis) (pt, [], (p, Res))
471 val pt = update_tac pt p (Derive (id_rls nrls))
472 (*FIXME.040216 struct.ctree*)
473 val pt = update_branch pt p TransitiveB
474 in (c, (pt, pos)) end;
476 val (_, Some ist) = get_obj g_loc pt p
477 val (f,a) = get_obj g_result pt p