17 val update_pblppc : CTbasic.ctree -> CTbasic.pos -> Model.itm list -> CTbasic.ctree (* =^^^= ? *) |
17 val update_pblppc : CTbasic.ctree -> CTbasic.pos -> Model.itm list -> CTbasic.ctree (* =^^^= ? *) |
18 val update_pblID : CTbasic.ctree -> CTbasic.pos -> Celem.pblID -> CTbasic.ctree |
18 val update_pblID : CTbasic.ctree -> CTbasic.pos -> Celem.pblID -> CTbasic.ctree |
19 val update_oris : CTbasic.ctree -> CTbasic.pos -> Model.ori list -> CTbasic.ctree |
19 val update_oris : CTbasic.ctree -> CTbasic.pos -> Model.ori list -> CTbasic.ctree |
20 val update_orispec : CTbasic.ctree -> CTbasic.pos -> Celem.spec -> CTbasic.ctree |
20 val update_orispec : CTbasic.ctree -> CTbasic.pos -> Celem.spec -> CTbasic.ctree |
21 val update_spec : CTbasic.ctree -> CTbasic.pos -> Celem.spec -> CTbasic.ctree |
21 val update_spec : CTbasic.ctree -> CTbasic.pos -> Celem.spec -> CTbasic.ctree |
22 val update_tac : CTbasic.ctree -> CTbasic.pos -> Tactic.input -> CTbasic.ctree |
22 val update_tac : CTbasic.ctree -> CTbasic.pos -> Tactic_Def.input -> CTbasic.ctree |
23 |
23 |
24 val upd_istate_ctxt : CTbasic.state -> Istate_Def.T * Proof.context -> CTbasic.ctree |
24 val upd_istate_ctxt : CTbasic.state -> Istate_Def.T * Proof.context -> CTbasic.ctree |
25 val upd_istate : CTbasic.state -> Istate_Def.T -> CTbasic.ctree |
25 val upd_istate : CTbasic.state -> Istate_Def.T -> CTbasic.ctree |
26 val upd_ctxt : CTbasic.state ->Proof.context -> CTbasic.ctree |
26 val upd_ctxt : CTbasic.state ->Proof.context -> CTbasic.ctree |
27 |
27 |
30 val cappend_problem : CTbasic.ctree -> CTbasic.pos -> Istate_Def.T * Proof.context -> |
30 val cappend_problem : CTbasic.ctree -> CTbasic.pos -> Istate_Def.T * Proof.context -> |
31 Selem.fmz -> Model.ori list * Celem.spec * term -> CTbasic.ctree * CTbasic.pos' list |
31 Selem.fmz -> Model.ori list * Celem.spec * term -> CTbasic.ctree * CTbasic.pos' list |
32 val append_result : CTbasic.ctree -> CTbasic.pos -> Istate_Def.T * Proof.context -> |
32 val append_result : CTbasic.ctree -> CTbasic.pos -> Istate_Def.T * Proof.context -> |
33 Selem.result -> CTbasic.ostate -> CTbasic.ctree * 'a list |
33 Selem.result -> CTbasic.ostate -> CTbasic.ctree * 'a list |
34 val append_atomic : (* for solve.sml *) |
34 val append_atomic : (* for solve.sml *) |
35 CTbasic.pos -> Istate_Def.T * Proof.context -> term -> Tactic.input -> Selem.result -> |
35 CTbasic.pos -> Istate_Def.T * Proof.context -> term -> Tactic_Def.input -> Selem.result -> |
36 CTbasic.ostate -> CTbasic.ctree -> CTbasic.ctree |
36 CTbasic.ostate -> CTbasic.ctree -> CTbasic.ctree |
37 val cappend_atomic : CTbasic.ctree -> CTbasic.pos -> Istate_Def.T * Proof.context -> term -> |
37 val cappend_atomic : CTbasic.ctree -> CTbasic.pos -> Istate_Def.T * Proof.context -> term -> |
38 Tactic.input -> Selem.result -> CTbasic.ostate -> CTbasic.ctree * CTbasic.pos' list |
38 Tactic_Def.input -> Selem.result -> CTbasic.ostate -> CTbasic.ctree * CTbasic.pos' list |
39 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) |
39 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) |
40 val cappend_parent : CTbasic.ctree -> int list -> Istate_Def.T * Proof.context -> term -> |
40 val cappend_parent : CTbasic.ctree -> int list -> Istate_Def.T * Proof.context -> term -> |
41 Tactic.input -> CTbasic.branch -> CTbasic.ctree * CTbasic.pos' list |
41 Tactic_Def.input -> CTbasic.branch -> CTbasic.ctree * CTbasic.pos' list |
42 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) |
42 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) |
43 val update_loc' : CTbasic.ctree -> CTbasic.pos -> |
43 val update_loc' : CTbasic.ctree -> CTbasic.pos -> |
44 (Istate_Def.T * Proof.context) option * (Istate_Def.T * Proof.context) option -> CTbasic.ctree |
44 (Istate_Def.T * Proof.context) option * (Istate_Def.T * Proof.context) option -> CTbasic.ctree |
45 val append_problem : int list -> Istate_Def.T * Proof.context -> Selem.fmz -> |
45 val append_problem : int list -> Istate_Def.T * Proof.context -> Selem.fmz -> |
46 Model.ori list * Celem.spec * term -> CTbasic.ctree -> CTbasic.ctree |
46 Model.ori list * Celem.spec * term -> CTbasic.ctree -> CTbasic.ctree |
206 | SOME (istate, _) => update_loc' pt p (SOME (istate, ctxt), for_result) |
206 | SOME (istate, _) => update_loc' pt p (SOME (istate, ctxt), for_result) |
207 end |
207 end |
208 |
208 |
209 (* called by Take *) |
209 (* called by Take *) |
210 fun append_form p l f pt = |
210 fun append_form p l f pt = |
211 insert_pt (PrfObj {cell = NONE, form = f, tac = Tactic.Empty_Tac, loc = (SOME l, NONE), |
211 insert_pt (PrfObj {cell = NONE, form = f, tac = Tactic_Def.Empty_Tac, loc = (SOME l, NONE), |
212 branch = NoBranch, result = (Rule.e_term, []), ostate = Incomplete}) pt p; |
212 branch = NoBranch, result = (Rule.e_term, []), ostate = Incomplete}) pt p; |
213 fun cappend_form pt p loc f = |
213 fun cappend_form pt p loc f = |
214 let |
214 let |
215 val (pt', cs) = cut_tree pt (p, Frm) |
215 val (pt', cs) = cut_tree pt (p, Frm) |
216 val pt'' = append_form p loc f pt' |
216 val pt'' = append_form p loc f pt' |
230 |
230 |
231 (*WN041022 deprecated, still for kbtest/diffapp.sml, /systest/root-equ.sml*) |
231 (*WN041022 deprecated, still for kbtest/diffapp.sml, /systest/root-equ.sml*) |
232 fun append_parent p l f r b pt = |
232 fun append_parent p l f r b pt = |
233 let |
233 let |
234 val (ll, f) = |
234 val (ll, f) = |
235 if existpt p pt andalso Tactic.is_empty_tac (get_obj g_tac pt p) |
235 if existpt p pt andalso Tactic_Def.is_empty_tac (get_obj g_tac pt p) |
236 then ((fst (get_obj g_loc pt p), SOME l), get_obj g_form pt p) |
236 then ((fst (get_obj g_loc pt p), SOME l), get_obj g_form pt p) |
237 else ((SOME l, NONE), f) |
237 else ((SOME l, NONE), f) |
238 in insert_pt (PrfObj {cell = NONE, form = f, tac = r, loc = ll, |
238 in insert_pt (PrfObj {cell = NONE, form = f, tac = r, loc = ll, |
239 branch = b, result = (Rule.e_term, []), ostate= Incomplete}) pt p |
239 branch = b, result = (Rule.e_term, []), ostate= Incomplete}) pt p |
240 end; |
240 end; |
242 apfst (append_parent p loc f r b) (cut_tree pt (p, Und)); |
242 apfst (append_parent p loc f r b) (cut_tree pt (p, Und)); |
243 |
243 |
244 fun append_atomic p l f r f' s pt = |
244 fun append_atomic p l f r f' s pt = |
245 let |
245 let |
246 val (iss, f) = |
246 val (iss, f) = |
247 if existpt p pt andalso Tactic.is_empty_tac (get_obj g_tac pt p) |
247 if existpt p pt andalso Tactic_Def.is_empty_tac (get_obj g_tac pt p) |
248 then (*after Take*) ((fst (get_obj g_loc pt p), SOME l), get_obj g_form pt p) |
248 then (*after Take*) ((fst (get_obj g_loc pt p), SOME l), get_obj g_form pt p) |
249 else ((NONE, SOME l), f) |
249 else ((NONE, SOME l), f) |
250 in |
250 in |
251 insert_pt (PrfObj {cell = NONE, form = f, tac = r, loc = iss, branch = NoBranch, |
251 insert_pt (PrfObj {cell = NONE, form = f, tac = r, loc = iss, branch = NoBranch, |
252 result = f', ostate = s}) pt p |
252 result = f', ostate = s}) pt p |
255 (* 20.8.02: cappend_* FIXXXXME cut branches below cannot be decided here: |
255 (* 20.8.02: cappend_* FIXXXXME cut branches below cannot be decided here: |
256 detail - generate - cappend: inserted, not appended !!! |
256 detail - generate - cappend: inserted, not appended !!! |
257 cut decided in applicable_in !?! |
257 cut decided in applicable_in !?! |
258 *) |
258 *) |
259 fun cappend_atomic pt p ist_res f r f' s = |
259 fun cappend_atomic pt p ist_res f r f' s = |
260 if existpt p pt andalso Tactic.is_empty_tac (get_obj g_tac pt p) |
260 if existpt p pt andalso Tactic_Def.is_empty_tac (get_obj g_tac pt p) |
261 then (*after Take: transfer Frm and respective istate*) |
261 then (*after Take: transfer Frm and respective istate*) |
262 let |
262 let |
263 val (ist_form, f) = |
263 val (ist_form, f) = |
264 (get_loc pt (p,Frm), get_obj g_form pt p) |
264 (get_loc pt (p,Frm), get_obj g_form pt p) |
265 val (pt, cs) = cut_tree pt (p,Frm) |
265 val (pt, cs) = cut_tree pt (p,Frm) |