1 (* Title: generate specific entries into Ctree
3 (c) due to copyright terms
6 signature GENERATE_CALC_TREE =
8 (* vvv request into signature is incremental with *.sml *)
9 (* for calchead.sml --------------------------------------------------------------- vvv *)
12 datatype pblmet = Method of Celem.metID | Problem of Celem.pblID | Upblmet
16 | FormKF of Celem.cterm'
17 | PpcKF of pblmet * Model.item Model.ppc
18 | RefinedKF of Celem.pblID * (Model.itm list * (bool * term) list)
19 val generate1 : theory -> Tac.tac_ -> Selem.istate * Proof.context ->
20 Ctree.pos' -> Ctree.ctree -> Ctree.pos' * Ctree.pos' list * mout * Ctree.ctree (* for calchead.sml------------- ^^^ *)
21 val init_istate : Tac.tac -> term -> Selem.istate (* for solve.sml *)
22 val init_pbl : (string * (term * 'a)) list -> Model.itm list
23 val init_pbl' : (string * (term * term)) list -> Model.itm list
24 val embed_deriv : taci list -> Ctree.state -> Ctree.pos' list * (Ctree.state) (* for inform.sml *)
25 val generate_hard : (* for solve.sml *)
26 theory -> Tac.tac_ -> Ctree.pos' -> Ctree.ctree -> Ctree.pos' * Ctree.pos' list * mout * Ctree.ctree
27 val generate : (Tac.tac * Tac.tac_ * (Ctree.pos' * (Selem.istate * Proof.context))) list ->
28 Ctree.ctree * Ctree.pos' list * Ctree.pos' -> Ctree.ctree * Ctree.pos' list * Ctree.pos' (* for mathengine.sml *)
29 val generate_inconsistent_rew : Selem.subs option * Celem.thm'' -> term -> Selem.istate * Proof.context ->
30 Ctree.pos' -> Ctree.ctree -> Ctree.state (* for interface.sml *)
31 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
32 val tacis2str : taci list -> string
33 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
35 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
37 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
41 structure Generate(**): GENERATE_CALC_TREE(**) =
45 (* initialize istate for Detail_Set *)
46 fun init_istate (Tac.Rewrite_Set rls) t =
47 (case assoc_rls rls of
48 Celem.Rrls {scr = Celem.Rfuns {init_state = ii, ...}, ...} => Selem.RrlsState (ii t)
49 | Celem.Rls {scr = EmptyScr, ...} =>
50 error ("interSteps>..>init_istate: \"" ^ rls ^ "\" has EmptyScr." ^
51 "use prep_rls' for storing rule-sets !")
52 | Celem.Rls {scr = Celem.Prog s, ...} => (Selem.ScrState ([(LTool.one_scr_arg s, t)], [], NONE, Celem.e_term, Selem.Sundef, true))
53 | Celem.Seq {scr=EmptyScr,...} =>
54 error ("interSteps>..>init_istate: \"" ^ rls ^ "\" has EmptyScr." ^
55 "use prep_rls' for storing rule-sets !")
56 | Celem.Seq {scr = Celem.Prog s,...} => (Selem.ScrState ([(LTool.one_scr_arg s, t)], [], NONE, Celem.e_term, Selem.Sundef, true))
57 | _ => error "init_istate Rewrite_Set: uncovered case assoc_rls")
58 | init_istate (Tac.Rewrite_Set_Inst (subs, rls)) t =
60 val v = case Selem.subs2subst (Celem.assoc_thy "Isac") subs of
62 | _ => error "init_istate: uncovered case "
63 (*...we suppose the substitution of only _one_ bound variable*)
64 in case assoc_rls rls of
65 Celem.Rls {scr = EmptyScr, ...} =>
66 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." ^
67 "use prep_rls' for storing rule-sets !")
68 | Celem.Rls {scr = Celem.Prog s, ...} =>
69 let val (form, bdv) = LTool.two_scr_arg s
70 in (Selem.ScrState ([(form, t), (bdv, v)], [], NONE, Celem.e_term, Selem.Sundef,true))
72 | Celem.Seq {scr = EmptyScr, ...} =>
73 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." ^
74 "use prep_rls' for storing rule-sets !")
75 | Celem.Seq {scr = Celem.Prog s,...} =>
76 let val (form, bdv) = LTool.two_scr_arg s
77 in (Selem.ScrState ([(form, t), (bdv, v)],[], NONE, Celem.e_term, Selem.Sundef,true))
79 | _ => error "init_istate Rewrite_Set_Inst: uncovered case assoc_rls"
81 | init_istate tac _ = error ("init_istate: uncovered definition for " ^ Tac.tac2str tac)
83 (* a taci holds alle information required to build a node in the calc-tree;
84 a taci is assumed to be used efficiently such that the calc-tree
85 resulting from applying a taci need not be stored separately;
86 see "type calcstate" *)
87 (*TODO.WN0504 redesign ??? or redesign generate ?? see "fun generate"
88 TODO.WN0512 ? redesign this _list_:
89 # only used for [Apply_Method + (Take or Subproblem)], i.e. for initacs
90 # the latter problem may be resolved automatically if "fun autocalc" is
91 not any more used for the specify-phase and for changing the phases*)
93 (Tac.tac * (* for comparison with input tac *)
94 Tac.tac_ * (* for ctree generation *)
95 (pos' * (* after applying tac_, for ctree generation *)
96 (Selem.istate * Proof.context))) (* after applying tac_, for ctree generation *)
97 val e_taci = (Tac.Empty_Tac, Tac.Empty_Tac_, (e_pos', (Selem.e_istate, Selem.e_ctxt))): taci
98 fun taci2str ((tac, tac_, (pos', (istate, _))):taci) =
99 "( " ^ Tac.tac2str tac ^ ", " ^ Tac.tac_2str tac_ ^ ", ( " ^ pos'2str pos' ^ ", " ^
100 Selem.istate2str istate ^ " ))"
101 fun tacis2str tacis = (strs2str o (map (Celem.linefeed o taci2str))) tacis
103 datatype pblmet = (*%^%*)
104 Upblmet (*undefined*)
105 | Problem of Celem.pblID (*%^%*)
106 | Method of Celem.metID; (*%^%*)
107 fun pblmet2str (Problem pblID) = "Problem " ^ strs2str pblID (*%^%*)
108 | pblmet2str (Method metID) = "Method " ^ Celem.metID2str metID (*%^%*)
109 | pblmet2str x = error ("pblmet2str: uncovered definition " ^ pblmet2str x)
111 (*3.5.00: TODO: foppFK eliminated in interface FE-KE !!!*)
112 datatype foppFK = (* in DG cases div 2 *)
113 EmptyFoppFK (*DG internal*)
114 | FormFK of Celem.cterm'
115 | PpcFK of Celem.cterm' Model.ppc
116 fun foppFK2str (FormFK ct') ="FormFK " ^ ct'
117 | foppFK2str (PpcFK ppc) ="PpcFK " ^ Model.ppc2str ppc
118 | foppFK2str EmptyFoppFK ="EmptyFoppFK"
120 datatype nest = Open | Closed | Nundef;
121 fun nest2str Open = "Open"
122 | nest2str Closed = "Closed"
123 | nest2str Nundef = "Nundef"
126 datatype edit = EdUndef | Write | Protect;
127 (* bridge --> kernel *)
128 (* bridge <-> kernel *)
129 (* needed in dialog.sml *) (* bridge <-- kernel *)
130 fun edit2str EdUndef = "EdUndef"
131 | edit2str Write = "Write"
132 | edit2str Protect = "Protect";
134 datatype inout = (*FIXME.WN1105 drop this: was required for proto0 with dialog in sml*)
135 Error_ of string (*<--*)
136 | FormKF of cellID * edit * indent * nest * Celem.cterm' (*<--*)
137 | PpcKF of cellID * edit * indent * nest * (pblmet * Model.item Model.ppc) (*<--*)
138 | RefineKF of Stool.match list (*<--*)
139 | RefinedKF of (Celem.pblID * ((Model.itm list) * ((bool * term) list))) (*<--*)
142 datatype mout = EmptyMout | Error' of inout | Form' of inout | Problems of inout
145 FormKF of Celem.cterm'
146 | PpcKF of (pblmet * Model.item Model.ppc)
147 | RefinedKF of Celem.pblID * (Model.itm list * (bool * term) list)
151 fun mout2str (FormKF cterm') = "FormKF " ^ cterm'
152 | mout2str (PpcKF (pm, itemppc)) = "PpcKF (" ^ pblmet2str pm ^ "," ^ Model.itemppc2str itemppc ^ ")"
153 | mout2str (RefinedKF (_, _)) = "mout2str: RefinedKF not impl."
154 | mout2str (Error' str) = "Error' " ^ str
155 | mout2str (EmptyMout ) = "EmptyMout"
157 (* init pbl with ...,dsc,empty | [] *)
160 fun pbt2itm (f, (d, _)) = (0, [], false, f, Model.Inc ((d, []), (Celem.e_term, [])))
161 in map pbt2itm pbt end
163 (* take formal parameters from pbt, for transfer from pbl/met-hierarchy *)
166 fun pbt2itm (f, (d, t)) = (0, [], false, f, Model.Inc((d, [t]), (Celem.e_term, [])))
167 in map pbt2itm pbt end
169 (*generate 1 ppobj in ctree*)
170 (*TODO.WN0501: take calcstate as an argument (see embed_derive etc.)?specify?*)
171 fun generate1 thy (Tac.Add_Given' (_, itmlist)) _ (pos as (p, p_)) pt =
172 (pos: pos', [], PpcKF (Upblmet, Specify.itms2itemppc thy [][]),
174 Pbl => update_pbl pt p itmlist
175 | Met => update_met pt p itmlist
176 | _ => error ("uncovered case " ^ pos_2str p_))
177 (* WN110515 probably declare_constraints with input item (without dsc) --
178 -- important when specifying without formalisation *)
179 | generate1 thy (Tac.Add_Find' (_, itmlist)) _ (pos as (p, p_)) pt =
180 (pos, [], (PpcKF (Upblmet, Specify.itms2itemppc thy [] [])),
182 Pbl => update_pbl pt p itmlist
183 | Met => update_met pt p itmlist
184 | _ => error ("uncovered case " ^ pos_2str p_))
185 (*WN110515 probably declare_constraints with input item (without dsc)*)
186 | generate1 thy (Tac.Add_Relation' (_, itmlist)) _ (pos as (p, p_)) pt =
187 (pos, [], PpcKF (Upblmet, Specify.itms2itemppc thy [] []),
189 Pbl => update_pbl pt p itmlist
190 | Met => update_met pt p itmlist
191 | _ => error ("uncovered case " ^ pos_2str p_))
192 | generate1 thy (Tac.Specify_Theory' domID) _ (pos as (p,_)) pt =
193 (pos, [] , PpcKF (Upblmet, Specify.itms2itemppc thy [] []),
194 update_domID pt p domID)
195 | generate1 thy (Tac.Specify_Problem' (pI, (_, (itms, _)))) _ (p, _) pt =
197 val pt = update_pbl pt p itms
198 val pt = update_pblID pt p pI
200 ((p, Pbl), [], PpcKF (Upblmet, Specify.itms2itemppc thy [] []), pt)
202 | generate1 thy (Tac.Specify_Method' (mID, oris, itms)) _ (p, _) pt =
204 val pt = update_oris pt p oris
205 val pt = update_met pt p itms
206 val pt = update_metID pt p mID
208 ((p, Met), [], PpcKF (Upblmet, Specify.itms2itemppc thy [] []), pt)
210 | generate1 thy (Tac.Model_Problem' (_, itms, met)) _ (pos as (p,_)) pt =
212 val pt = update_pbl pt p itms
213 val pt = update_met pt p met
215 (pos, [], PpcKF (Upblmet, Specify.itms2itemppc thy [] []), pt)
217 | generate1 thy (Tac.Refine_Tacitly' (_, pIre, domID, metID, pbl)) _ (pos as (p, _)) pt =
219 val pt = update_pbl pt p pbl
220 val pt = update_orispec pt p (domID, pIre, metID)
222 (pos, [], PpcKF (Upblmet, Specify.itms2itemppc thy [] []), pt)
224 | generate1 thy (Tac.Refine_Problem' (pI, _)) _ (pos as (p, _)) pt =
226 val (dI, _, mI) = get_obj g_spec pt p
227 val pt = update_spec pt p (dI, pI, mI)
229 (pos, [], PpcKF (Upblmet, Specify.itms2itemppc thy [] []), pt)
231 | generate1 _ (Tac.Apply_Method' (_, topt, is, ctxt)) _ (pos as (p, _)) pt =
234 let val (pt, c) = cappend_form pt p (is, ctxt) t
235 in (pos, c, EmptyMout, pt) end
236 | NONE => (pos, [], EmptyMout, update_env pt p (SOME (is, ctxt))))
237 | generate1 _ (Tac.Take' t) l (p, _) pt = (* val (Take' t) = m; *)
240 let val (ps, p') = split_last p (* no connex to prev.ppobj *)
241 in if p' = 0 then ps @ [1] else p end
242 val (pt, c) = cappend_form pt p l t
244 ((p, Frm): pos', c, FormKF (Celem.term2str t), pt)
246 | generate1 _ (Tac.Begin_Trans' t) l (p, Frm) pt =
248 val (pt, c) = cappend_form pt p l t
249 val pt = update_branch pt p TransitiveB (*040312*)
250 (* replace the old PrfOjb ~~~~~ *)
251 val p = (lev_on o lev_dn (* starts with [...,0] *)) p
252 val (pt, c') = cappend_form pt p l t (*FIXME.0402 same istate ???*)
254 ((p, Frm), c @ c', FormKF (Celem.term2str t), pt)
256 | generate1 thy (Tac.Begin_Trans' t) l (p, Res) pt =
257 (*append after existing PrfObj vvvvvvvvvvvvv*)
258 generate1 thy (Tac.Begin_Trans' t) l (lev_on p, Frm) pt
259 | generate1 _ (Tac.End_Trans' tasm) l (p, _) pt =
262 val (pt, c) = append_result pt p' l tasm Complete
264 ((p', Res), c, FormKF "DUMMY" (*term2str t ..ERROR (t) has not been declared*), pt)
266 | generate1 _ (Tac.Rewrite_Inst' (_, _, _, _, subs', thm', f, (f', asm))) (is, ctxt) (p, _) pt =
268 val (pt, c) = cappend_atomic pt p (is, Stool.insert_assumptions asm ctxt) f
269 (Tac.Rewrite_Inst (Selem.subst2subs subs', thm')) (f',asm) Complete;
270 val pt = update_branch pt p TransitiveB
272 ((p, Res), c, FormKF (Celem.term2str f'), pt)
274 | generate1 _ (Tac.Rewrite' (_, _, _, _, thm', f, (f', asm))) (is, ctxt) (p, _) pt =
276 val (pt, c) = cappend_atomic pt p (is, Stool.insert_assumptions asm ctxt) f
277 (Tac.Rewrite thm') (f', asm) Complete
278 val pt = update_branch pt p TransitiveB
280 ((p, Res), c, FormKF (Celem.term2str f'), pt)
282 | generate1 thy (Tac.Rewrite_Asm' all) l p pt = generate1 thy (Tac.Rewrite' all) l p pt
283 | generate1 _ (Tac.Rewrite_Set_Inst' (_, _, subs', rls', f, (f', asm))) (is, ctxt) (p, _) pt =
285 val (pt, c) = cappend_atomic pt p (is, Stool.insert_assumptions asm ctxt) f
286 (Tac.Rewrite_Set_Inst (Selem.subst2subs subs', Celem.id_rls rls')) (f', asm) Complete
287 val pt = update_branch pt p TransitiveB
289 ((p, Res), c, FormKF (Celem.term2str f'), pt)
291 | generate1 thy (Tac.Detail_Set_Inst' (_, _, subs, rls, f, (_, asm))) (is, ctxt) (p, _) pt =
293 val ctxt' = Stool.insert_assumptions asm ctxt
294 val (pt, _) = cappend_form pt p (is, ctxt') f
295 val pt = update_branch pt p TransitiveB
296 val is = init_istate (Tac.Rewrite_Set_Inst (Selem.subst2subs subs, Celem.id_rls rls)) f
297 val tac_ = Tac.Apply_Method' (Celem.e_metID, SOME Celem.e_term (*t ..has not been declared*), is, ctxt')
298 val pos' = ((lev_on o lev_dn) p, Frm)
300 generate1 thy tac_ (is, ctxt') pos' pt (*implicit Take*)
302 | generate1 _ (Tac.Rewrite_Set' (_, _, rls', f, (f', asm))) (is, ctxt) (p, _) pt =
304 val (pt, c) = cappend_atomic pt p (is, Stool.insert_assumptions asm ctxt) f
305 (Tac.Rewrite_Set (Celem.id_rls rls')) (f',asm) Complete
306 val pt = update_branch pt p TransitiveB
308 ((p, Res), c, FormKF (Celem.term2str f'), pt)
310 | generate1 thy (Tac.Detail_Set' (_, _, rls, f, (_, asm))) (is, ctxt) (p, _) pt =
312 val ctxt' = Stool.insert_assumptions asm ctxt
313 val (pt, _) = cappend_form pt p (is, ctxt') f
314 val pt = update_branch pt p TransitiveB
315 val is = init_istate (Tac.Rewrite_Set (Celem.id_rls rls)) f
316 val tac_ = Tac.Apply_Method' (Celem.e_metID, SOME Celem.e_term (*t ..has not been declared*), is, ctxt')
317 val pos' = ((lev_on o lev_dn) p, Frm)
319 generate1 thy tac_ (is, ctxt') pos' pt (*implicit Take*)
321 | generate1 _ (Tac.Check_Postcond' (_, (scval, asm))) l (p, _) pt =
323 val (pt, c) = append_result pt p l (scval, asm) Complete
325 ((p, Res), c, FormKF (Celem.term2str scval), pt)
327 | generate1 _ (Tac.Calculate' (_, op_, f, (f', _))) l (p, _) pt =
329 val (pt,c) = cappend_atomic pt p l f (Tac.Calculate op_) (f', []) Complete
331 ((p, Res), c, FormKF (Celem.term2str f'), pt)
333 | generate1 _ (Tac.Check_elementwise' (consts, pred, (f', asm))) l (p, _) pt =
335 val (pt,c) = cappend_atomic pt p l consts (Tac.Check_elementwise pred) (f', asm) Complete
337 ((p, Res), c, FormKF (Celem.term2str f'), pt)
339 | generate1 _ (Tac.Or_to_List' (ors, list)) l (p, _) pt =
341 val (pt,c) = cappend_atomic pt p l ors Tac.Or_to_List (list, []) Complete
343 ((p, Res), c, FormKF (Celem.term2str list), pt)
345 | generate1 _ (Tac.Substitute' (_, _, subte, t, t')) l (p, _) pt =
348 cappend_atomic pt p l t (Tac.Substitute (Selem.subte2sube subte)) (t',[]) Complete
349 in ((p, Res), c, FormKF (Celem.term2str t'), pt)
351 | generate1 _ (Tac.Tac_ (_, f, id, f')) l (p, _) pt =
353 val (pt, c) = cappend_atomic pt p l (TermC.str2term f) (Tac.Tac id) (TermC.str2term f', []) Complete
355 ((p,Res), c, FormKF f', pt)
357 | generate1 thy (Tac.Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, ctxt, f)) l (p, _) pt =
359 val (pt, c) = cappend_problem pt p l (fmz_, (domID, pblID, metID)) (oris, (domID, pblID, metID), hdl)
360 val pt = update_ctxt pt p ctxt
361 val f = Syntax.string_of_term (Celem.thy2ctxt thy) f
363 ((p, Pbl), c, FormKF f, pt)
365 | generate1 _ m' _ _ _ = error ("generate1: not impl.for " ^ Tac.tac_2str m')
367 fun generate_inconsistent_rew (subs_opt, thm') f' (is, ctxt) (pos as (p,_)) pt =
369 val f = get_curr_formula (pt, pos)
370 val pos' as (p', _) = (lev_on p, Res)
371 val (pt, _) = case subs_opt of
372 NONE => cappend_atomic pt p' (is, Stool.insert_assumptions [] ctxt) f
373 (Tac.Rewrite thm') (f', []) Inconsistent
374 | SOME subs => cappend_atomic pt p' (is, Stool.insert_assumptions [] ctxt) f
375 (Tac.Rewrite_Inst (subs, thm')) (f', []) Inconsistent
376 val pt = update_branch pt p' TransitiveB
379 fun generate_hard thy m' (p,p_) pt =
382 Frm => p | Res => lev_on p
383 | _ => error ("generate_hard: call by " ^ pos'2str (p,p_))
384 in generate1 thy m' (Selem.e_istate, Selem.e_ctxt) (p,p_) pt end
386 (* tacis are in reverse order from nxt_solve_/specify_: last = fst to insert *)
387 fun generate ([]: taci list) ptp = ptp
388 | generate tacis (pt, c, _: pos'(*!dropped!WN0504redesign generate/tacis?*))=
390 val (tacis', (_, tac_, (p, is))) = split_last tacis
391 val (p',c',_,pt') = generate1 (Celem.assoc_thy "Isac") tac_ is p pt
393 generate tacis' (pt', c@c', p')
396 (* update pos in tacis for embedding by generate *)
397 fun insert_pos (_: pos) [] = []
398 | insert_pos (p: pos) (((tac, tac_, (_, ist)): taci) :: tacis) =
399 ((tac, tac_, ((p, Res), ist)): taci) :: (insert_pos (lev_on p) tacis)
401 fun res_from_taci (_, Tac.Rewrite' (_, _, _, _, _, _,(res, asm)), _) = (res, asm)
402 | res_from_taci (_, Tac.Rewrite_Set' (_, _, _, _, (res, asm)), _) = (res, asm)
403 | res_from_taci (_, tac_, _) = error ("res_from_taci: called with" ^ Tac.tac_2str tac_)
405 (* embed the tacis created by a '_deriv'ation; sys.form <> input.form
406 tacis are in order, thus are reverted for generate *)
407 fun embed_deriv (tacis: taci list) (pt, pos as (p, Frm): pos') =
408 (*inform at Frm: replace the whole PrfObj by a Transitive-ProfObj FIXME?0402
409 and transfer the istate (from _after_ compare_deriv) from Frm to Res*)
411 val (res, asm) = (res_from_taci o last_elem) tacis
412 val (ist, ctxt) = case get_obj g_loc pt p of
413 (SOME (ist, ctxt), _) => (ist, ctxt)
414 | (NONE, _) => error "embed_deriv Frm: uncovered case get_obj"
415 val form = get_obj g_form pt p
416 (*val p = lev_on p; ---------------only difference to (..,Res) below*)
417 val tacis = (Tac.Begin_Trans, Tac.Begin_Trans' form, (pos, (Selem.Uistate, ctxt))) ::
418 (insert_pos ((lev_on o lev_dn) p) tacis) @ [(Tac.End_Trans, Tac.End_Trans' (res, asm),
419 (pos_plus (length tacis) (lev_dn p, Res), (new_val res ist, ctxt)))]
420 val {nrls, ...} = Specify.get_met (get_obj g_metID pt (par_pblobj pt p))
421 val (pt, c, pos as (p, _)) = generate (rev tacis) (pt, [], (p, Res))
422 val pt = update_tac pt p (Tac.Derive (Celem.id_rls nrls))
423 val pt = update_branch pt p TransitiveB
424 in (c, (pt, pos: pos')) end
425 | embed_deriv tacis (pt, (p, Res)) =
426 (*inform at Res: append a Transitive-PrfObj FIXME?0402 other branch-types ?
427 and transfer the istate (from _after_ compare_deriv) from Res to new Res*)
428 let val (res, asm) = (res_from_taci o last_elem) tacis
429 val (ist, ctxt) = case get_obj g_loc pt p of
430 (_, SOME (ist, ctxt)) => (ist, ctxt)
431 | (_, NONE) => error "embed_deriv Frm: uncovered case get_obj"
432 val (f, _) = get_obj g_result pt p
433 val p = lev_on p(*---------------only difference to (..,Frm) above*);
434 val tacis = (Tac.Begin_Trans, Tac.Begin_Trans' f, ((p, Frm), (Selem.Uistate, ctxt))) ::
435 (insert_pos ((lev_on o lev_dn) p) tacis) @ [(Tac.End_Trans, Tac.End_Trans' (res, asm),
436 (pos_plus (length tacis) (lev_dn p, Res), (new_val res ist, ctxt)))];
437 val {nrls, ...} = Specify.get_met (get_obj g_metID pt (par_pblobj pt p))
438 val (pt, c, pos as (p, _)) = generate (rev tacis) (pt, [], (p, Res))
439 val pt = update_tac pt p (Tac.Derive (Celem.id_rls nrls))
440 val pt = update_branch pt p TransitiveB
441 in (c, (pt, pos)) end
442 | embed_deriv _ _ = error "embed_deriv: uncovered definition"