1 (* Title: the calctree, which holds a calculation
2 Author: Walther Neuper 1999
3 (c) due to copyright terms
7 sig (* vvv--- *.sml require these typs incrementally, with these exception -----------------vvv *)
9 type fmz_ = cterm' list
10 type fmz = fmz_ * spec;
11 val e_fmz : fmz_ * spec (* for datatypes.sml *)
14 datatype istate = RrlsState of rrlsstate | ScrState of scrstate | Uistate
15 val istate2str : istate -> string
19 val sube2str : cterm' list -> string
21 val sube2subst : theory -> cterm' list -> (term * term) list
22 val sube2subte : cterm' list -> term list
23 val subs2subst : theory -> cterm' list -> (term * term) list
24 val subst2sube : (term * term) list -> cterm' list (* for datatypes.sml *)
25 val subst2subs : (term * term) list -> cterm' list
26 val subst2subs' : (term * term) list -> (string * string) list
27 val subte2sube : term list -> cterm' list
30 datatype tac_ = (* TODO.WN161219: replace *every* cterm' by term *)
31 Add_Find' of cterm' * itm list | Add_Given' of cterm' * itm list | Add_Relation' of cterm' * itm list
32 | Apply_Assumption' of term list * term
33 | Apply_Method' of metID * term option * istate * Proof.context
34 (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
35 | Begin_Sequ' | Begin_Trans' of term
36 | Split_And' of term | Split_Or' of term | Split_Intersect' of term
37 | Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
38 | End_Sequ' | End_Trans' of result
39 | End_Ruleset' of term | End_Subproblem' of term | End_Intersect' of term | End_Proof''
40 (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
42 | Calculate' of theory' * string * term * (term * thm')
43 | Check_Postcond' of pblID * result
44 | Check_elementwise' of term * cterm' * result
45 | Del_Find' of cterm' | Del_Given' of cterm' | Del_Relation' of cterm'
48 | Detail_Set' of theory' * bool * rls * term * result
49 | Detail_Set_Inst' of theory' * bool * subst * rls * term * result
50 | End_Detail' of result
55 | Init_Proof' of cterm' list * spec
56 | Model_Problem' of pblID * itm list * itm list
57 | Or_to_List' of term * term
58 | Refine_Problem' of pblID * (itm list * (bool * term) list)
59 | Refine_Tacitly' of pblID * pblID * domID * metID * itm list
61 | Rewrite' of theory' * rew_ord' * rls * bool * thm'' * term * result
62 | Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm'' * term * result
63 | Rewrite_Inst' of theory' * rew_ord' * rls * bool * subst * thm'' * term * result
64 | Rewrite_Set' of theory' * bool * rls * term * result
65 | Rewrite_Set_Inst' of theory' * bool * subst * rls * term * result
67 | Specify_Method' of metID * ori list * itm list
68 | Specify_Problem' of pblID * (bool * (itm list * (bool * term) list))
69 | Specify_Theory' of domID
70 | Subproblem' of spec * ori list * term * fmz_ * Proof.context * term
71 | Substitute' of rew_ord_ * rls * subte * term * term
72 | Tac_ of theory * string * string * string
73 | Take' of term | Take_Inst' of term
75 Add_Find of cterm' | Add_Given of cterm' | Add_Relation of cterm'
76 | Apply_Assumption of cterm' list
77 | Apply_Method of metID
79 | Begin_Sequ | Begin_Trans
80 | Split_And | Split_Or | Split_Intersect
81 | Conclude_And | Conclude_Or | Collect_Trues
82 | End_Sequ | End_Trans
83 | End_Ruleset | End_Subproblem | End_Intersect | End_Proof'
87 | Check_Postcond of pblID
88 | Check_elementwise of cterm'
89 | Del_Find of cterm' | Del_Given of cterm' | Del_Relation of cterm'
93 | Detail_Set_Inst of subs * rls'
98 | Group of con * int list
100 | Init_Proof of cterm' list * spec
103 | Refine_Problem of pblID
104 | Refine_Tacitly of pblID
107 | Rewrite_Asm of thm''
108 | Rewrite_Inst of subs * thm''
109 | Rewrite_Set of rls'
110 | Rewrite_Set_Inst of subs * rls'
112 | Specify_Method of metID
113 | Specify_Problem of pblID
114 | Specify_Theory of domID
115 | Subproblem of domID * pblID
119 | Take of cterm' | Take_Inst of cterm'
120 val tac2str : tac -> string
121 val rls_of : tac -> rls' (* for solve.sml *)
122 val tac2IDstr : tac -> string
123 val is_rewset : tac -> bool (* for mathengine.sml *)
124 val is_rewtac : tac -> bool (* for interface.sml *)
127 type pos = posel list
128 val pos2str : int list -> string (* for datatypes.sml *)
129 datatype pos_ = Frm | Met | Pbl | Res | Und
130 val pos_2str : pos_ -> string
132 val pos'2str : pos' -> string
133 val str2pos_ : string -> pos_ (* for datatypes.sml *)
136 (* for generate.sml ?!? ca.*)
137 datatype safe = Helpless | Safe | Sundef | Unsafe
138 val tac_2str : tac_ -> string
141 datatype branch = AndB | CollectB | IntersectB | MapB | NoBranch | OrB | SequenceB | TransitiveB
142 datatype ostate = Complete | Incomplete | Inconsistent
147 loc: (istate * Proof.context) option * (istate * Proof.context) option,
152 origin: ori list * spec * term,
157 env: (istate * Proof.context) option}
161 loc: (istate * Proof.context) option * (istate * Proof.context) option,
167 val lev_on : pos -> pos
168 val lev_dn : pos -> pos
169 val lev_dn_ : pos' -> pos'
170 val lev_up : pos -> pos
171 val lev_of : pos' -> int
172 val pos_plus : int -> pos' -> pos'
173 val lev_back' : pos' -> pos' (* for inform.sml *)
175 datatype ctree = EmptyPtree | Nd of ppobj * ctree list
176 val e_ctree : ctree (* TODO: replace by EmptyPtree*)
177 val existpt' : pos' -> ctree -> bool (* for interface.sml *)
178 val exist_lev_on' : ctree -> pos' -> bool (* for interface.sml *)
179 val is_interpos : pos' -> bool (* for interface.sml *)
180 val lev_on' : ctree -> pos' -> pos' (* for interface.sml *)
181 val lev_pred' : ctree -> pos' -> pos' (* for interface.sml *)
182 val move_up : pos -> ctree -> pos' -> pos' (* for interface.sml *)
183 val movelevel_dn : pos -> ctree -> pos' -> pos' (* for interface.sml *)
184 val movelevel_up : pos -> ctree -> pos' -> pos' (* for interface.sml *)
185 val movecalchd_up : ctree -> pos' -> pos' (* for interface.sml *)
186 val par_pblobj : ctree -> pos -> pos
187 val ins_chn : ctree list -> ctree -> pos -> ctree (* for solve.sml *)
188 val children : ctree -> ctree list (* for solve.sml *)
189 val get_nd : ctree -> pos -> ctree (* for solve.sml *)
190 val just_created_ : ppobj -> bool (* for mathengine.sml *)
191 val just_created : ctree * pos' -> bool (* for mathengine.sml *)
192 val is_curr_endof_calc : ctree -> pos' -> bool (* for interface.sml *)
193 val e_origin : ori list * spec * term (* for mathengine.sml *)
195 val move_dn : pos -> ctree -> pos' -> pos'
196 val is_pblobj : ppobj -> bool
197 val is_pblobj' : ctree -> pos -> bool
198 val is_pblnd : ctree -> bool
199 val last_onlev : ctree -> pos -> bool
201 val g_spec : ppobj -> spec
202 val g_loc : ppobj -> (istate * Proof.context) option * (istate * Proof.context) option
203 val g_form : ppobj -> term
204 val g_pbl : ppobj -> itm list
205 val g_met : ppobj -> itm list
206 val g_metID : ppobj -> metID
207 val g_result : ppobj -> result
208 val g_tac : ppobj -> tac
209 val g_domID : ppobj -> domID (* for appl.sml TODO: replace by thyID *)
210 val g_env : ppobj -> (istate * Proof.context) option (* for appl.sml *)
212 val g_origin : ppobj -> ori list * spec * term (* for script.sml *)
213 val get_loc : ctree -> pos' -> istate * Proof.context (* for script.sml *)
214 val get_istate : ctree -> pos' -> istate (* for script.sml *)
215 val get_ctxt : ctree -> pos' -> Proof.context
216 val get_obj : (ppobj -> 'a) -> ctree -> pos -> 'a
217 val get_curr_formula : ctree * pos' -> term
218 val get_assumptions_ : ctree -> pos' -> term list (* for appl.sml *)
220 val append_result : ctree -> pos -> istate * Proof.context -> result ->
221 ostate -> ctree * 'a list
222 val append_atomic : (* for solve.sml *)
223 pos -> istate * Proof.context -> term -> tac -> result -> ostate -> ctree -> ctree
224 val cappend_atomic : ctree -> pos -> istate * Proof.context -> term -> tac -> result ->
225 ostate -> ctree * pos' list
226 val cappend_form : ctree -> pos -> istate * Proof.context -> term -> ctree * pos' list
227 val cappend_problem : ctree -> pos -> istate * Proof.context -> fmz ->
228 ori list * spec * term -> ctree * pos' list
230 val update_branch : ctree -> pos -> branch -> ctree
231 val update_ctxt : ctree -> pos -> Proof.context -> ctree
232 val update_env : ctree -> pos -> (istate * Proof.context) option -> ctree
233 val update_oris : ctree -> pos -> ori list -> ctree
234 val update_orispec : ctree -> pos -> spec -> ctree
235 val update_pbl : ctree -> pos -> itm list -> ctree
236 val update_pblppc : ctree -> pos -> itm list -> ctree (* =vvv= ? *)
237 val update_pblID : ctree -> pos -> pblID -> ctree (* =^^^= ? *)
238 val update_met : ctree -> pos -> itm list -> ctree (* =vvv= ? *)
239 val update_metppc : ctree -> pos -> itm list -> ctree (* =^^^= ? *)
240 val update_metID : ctree -> pos -> metID -> ctree
241 val update_domID : ctree -> pos -> domID -> ctree
242 val update_spec : ctree -> pos -> spec -> ctree
243 val update_tac : ctree -> pos -> tac -> ctree
245 val e_ctxt : Proof.context
246 val is_e_ctxt : Proof.context -> bool (* for appl.sml *)
247 val new_val : term -> istate -> istate
248 (* for calchead.sml *)
249 type cid = cellID list
250 type ocalhd = bool * pos_ * term * itm list * (bool * term) list * spec
251 datatype ptform = Form of term | ModSpec of ocalhd
252 val get_somespec' : spec -> spec -> spec
253 exception PTREE of string;
255 val par_pbl_det : ctree -> pos -> bool * pos * rls
256 (* for rewtools.sml *)
257 val rule2tac : theory -> (term * term) list -> rule -> tac
258 val eq_tac : tac * tac -> bool
260 val rootthy : ctree -> theory
261 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
262 val update_loc' : ctree -> pos -> (istate * Proof.context) option * (istate * Proof.context) option -> ctree
263 val append_problem : int list -> istate * Proof.context -> fmz -> ori list * spec * term -> ctree -> ctree
264 val g_res : ppobj -> term
265 val pr_ctree : (pos -> ppobj -> string) -> ctree -> string
266 val pr_short : pos -> ppobj -> string
267 val existpt : pos -> ctree -> bool
268 val is_empty_tac : tac -> bool
269 val e_subs : string list
270 val e_sube : cterm' list
271 val g_branch : ppobj -> branch
272 val g_ctxt : ppobj -> Proof.context
273 val g_fmz : ppobj -> fmz
274 val get_allp : pos' list -> pos * (int list * pos_) -> ctree -> pos' list
275 val get_allps : (pos * pos_) list -> posel list -> ctree list -> pos' list
276 val get_allpos' : pos * posel -> ctree -> pos' list
277 val get_allpos's : pos * posel -> ctree list -> (pos * pos_) list
278 val cut_bottom : pos * posel -> ctree -> (ctree * pos' list) * bool
279 val cut_tree : ctree -> pos * 'a -> ctree * pos' list
280 val cut_level : pos' list -> pos -> ctree -> int list * pos_ -> ctree * pos' list
281 val cut_level_'_ : pos' list -> pos -> ctree -> int list * pos_ -> ctree * pos' list
282 val get_trace : ctree -> int list -> int list -> int list list
283 val subte2subst : term list -> (term * term) list
284 val branch2str : branch -> string
285 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
290 val Ets : ets exception PTREE of string
292 pos -> istate * Proof.context -> term -> tac -> term * term list -> ostate -> ctree -> ctree
293 val append_form : int list -> istate * Proof.context -> term -> ctree -> ctree
294 val append_parent : pos -> istate * Proof.context -> term -> tac -> branch -> ctree -> ctree
295 val append_problem : int list -> istate * Proof.context -> fmz -> ori list * spec * term -> ctree -> ctree
296 val append_result : ctree -> pos -> istate * Proof.context -> term * term list -> ostate -> ctree * 'a list
297 val appl_branch : (ppobj -> bool) * (posel -> ctree list -> ctree list) -> ctree -> int list -> ctree * bool
298 val appl_obj : (ppobj -> ppobj) -> ctree -> pos -> ctree
299 val appl_to_node : (ppobj -> ppobj) -> ctree -> ctree
300 datatype branch = AndB | CollectB | IntersectB | MapB | NoBranch | OrB | SequenceB | TransitiveB
301 val branch2str : branch -> string
303 ctree -> pos -> istate * Proof.context -> term -> tac -> term * term list -> ostate -> ctree * pos' list
304 val cappend_form : ctree -> pos -> istate * Proof.context -> term -> ctree * pos' list
305 val cappend_parent : ctree -> pos -> istate * Proof.context -> term -> tac -> branch -> ctree * pos' list
306 val cappend_problem :
307 ctree -> int list -> istate * Proof.context -> fmz -> ori list * spec * term -> ctree * pos' list
309 val children : ctree -> ctree list
310 type cid = cellID list
311 datatype con = land | lor
312 val cut_bottom : pos * posel -> ctree -> (ctree * pos' list) * bool
313 val cut_level : pos' list -> pos -> ctree -> int list * pos_ -> ctree * pos' list
314 val cut_level_'_ : pos' list -> pos -> ctree -> int list * pos_ -> ctree * pos' list
315 val cut_levup : pos' list -> bool -> ctree -> ctree -> posel list * posel -> ctree -> ctree * pos' list
316 val cut_tree : ctree -> pos * 'a -> ctree * pos' list
317 val cutlevup : ppobj -> bool
318 val del_res : ppobj -> ppobj
319 val delete_result : ctree -> pos -> ctree
320 val e_ctxt : Proof.context
321 val e_fmz : 'a list * spec
322 val e_ocalhd : bool * pos_ * term * itm list * (bool * term) list * spec
323 val e_origin : ori list * spec * term
324 val e_ptform : ptform
325 val e_ptform' : ptform
327 val e_scrstate : scrstate
328 val e_sube : cterm' list
329 val e_subs : string list
330 val e_subte : term list
331 val empty_envp : envp type env = (term * term) list
332 type envp = (int * term list) list * (int * rls) list * (int * ets) list * (string * pos) list
333 val eq_tac : tac * tac -> bool type ets = (loc_ * (tac_ * env * env * term * term * safe)) list
334 val ets2s : loc_ * (tac_ * subst * subst * term * term * safe) -> string
335 val ets2str : ets -> string
336 val exist_lev_on' : ctree -> pos' -> bool
337 val existpt : pos -> ctree -> bool
338 val existpt' : pos' -> ctree -> bool
339 type fmz = fmz_ * spec
340 type fmz_ = cterm' list
341 val g_branch : ppobj -> branch
342 val g_cell : ppobj -> lrd option
343 val g_ctxt : ppobj -> Proof.context
344 val g_domID : ppobj -> domID
345 val g_env : ppobj -> (istate * Proof.context) option
346 val g_fmz : ppobj -> fmz
347 val g_form : ppobj -> term
348 val g_form' : ctree -> term
349 val g_loc : ppobj -> (istate * Proof.context) option * (istate * Proof.context) option
350 val g_met : ppobj -> itm list
351 val g_metID : ppobj -> metID
352 val g_origin : ppobj -> ori list * spec * term
353 val g_ostate : ppobj -> ostate
354 val g_ostate' : ctree -> ostate
355 val g_pbl : ppobj -> itm list
356 val g_res : ppobj -> term
357 val g_res' : ctree -> term
358 val g_result : ppobj -> term * term list
359 val g_spec : ppobj -> spec
360 val g_tac : ppobj -> tac
361 val get_all : (ppobj -> 'a) -> ctree -> 'a list
362 val get_allp : pos' list -> pos * (int list * pos_) -> ctree -> pos' list
363 val get_allpos' : pos * posel -> ctree -> pos' list
364 val get_allpos's : pos * posel -> ctree list -> (pos * pos_) list
365 val get_allps : (pos * pos_) list -> posel list -> ctree list -> pos' list
366 val get_alls : (ppobj -> 'a) -> ctree list -> 'a list
367 val get_assumptions_ : ctree -> pos * pos_ -> term list
368 val get_ctxt : ctree -> pos * pos_ -> Proof.context
369 val get_curr_formula : ctree * (pos * pos_) -> term
370 val get_istate : ctree -> pos * pos_ -> istate
371 val get_loc : ctree -> pos * pos_ -> istate * Proof.context
372 val get_nd : ctree -> pos -> ctree
373 val get_obj : (ppobj -> 'a) -> ctree -> pos -> 'a
374 val get_somespec : spec -> spec -> spec
375 val get_somespec' : spec -> spec -> spec
376 val get_trace : ctree -> int list -> int list -> int list list
377 val gpt_cell : ctree -> lrd option
378 type iist = istate option * istate option
379 val ind : pos' -> int
380 val ins_chn : ctree list -> ctree -> int list -> ctree
381 val ins_nth : int -> 'a -> 'a list -> 'a list
382 val insert_pt : ppobj -> ctree -> int list -> ctree
383 val is_curr_endof_calc : ctree -> pos' -> bool
384 val is_e_ctxt : Proof.context -> bool
385 val is_empty_tac : tac -> bool
386 val is_interpos : pos' -> bool
387 val is_pblnd : ctree -> bool
388 val is_pblobj : ppobj -> bool
389 val is_pblobj' : ctree -> pos -> bool
390 val is_prfobj : ppobj -> bool
391 val is_rewset : tac -> bool
392 val is_rewtac : tac -> bool
393 val isasub2subst : term -> (term * term) list
394 datatype istate = RrlsState of rrlsstate | ScrState of scrstate | Uistate
395 val istate2str : istate -> string
396 val istates2str : istate option * istate option -> string
397 val just_created : ctree * pos' -> bool
398 val just_created_ : ppobj -> bool
399 val last_onlev : ctree -> pos -> bool
400 val lev_back' : pos' -> pos'
401 val lev_dn : posel list -> posel list
402 val lev_dnRes : pos' -> pos'
403 val lev_dn_ : pos' -> pos'
404 val lev_of : pos' -> int
405 val lev_on : pos -> posel list
406 val lev_on' : ctree -> pos' -> pos'
407 val lev_onFrm : pos' -> pos'
408 val lev_pred : pos -> pos
409 val lev_pred' : ctree -> pos' -> pos'
410 val lev_up : pos -> pos
411 val lev_up_ : pos' -> pos'
412 val move_dn : pos -> ctree -> int list * pos_ -> int list * pos_
413 val move_up : int list -> ctree -> int list * pos_ -> int list * pos_
414 val movecalchd_up : ctree -> pos' -> pos'
415 val movelevel_dn : int list -> ctree -> int list * pos_ -> int list * pos_
416 val movelevel_up : int list -> ctree -> int list * pos_ -> int list * pos_
417 val new_val : term -> istate -> istate
418 val nth : int -> 'a list -> 'a
419 type ocalhd = bool * pos_ * term * itm list * (bool * term) list * spec
420 val ocalhd2str : ocalhd -> string
421 datatype ostate = Complete | Incomplete | Inconsistent
422 val ostate2str : ostate -> string
423 val par_children : ctree -> pos -> ctree list * pos
424 val par_pbl_det : ctree -> pos -> bool * pos * rls
425 val par_pblobj : ctree -> pos -> pos
426 type pos = posel list
427 type pos' = pos * pos_
428 val pos's2str : (int list * pos_) list -> string
429 val pos2str : int list -> string
430 datatype pos_ = Frm | Met | Pbl | Res | Und
431 val pos_2str : pos_ -> string
432 val pos_plus : int -> pos * pos_ -> pos'
434 val posless : int list -> int list -> bool
440 env: (istate * Proof.context) option,
442 loc: (istate * Proof.context) option * (istate * Proof.context) option,
444 origin: ori list * spec * term, ostate: ostate, probl: itm list, result: term * term list, spec: spec}
449 loc: (istate * Proof.context) option * (istate * Proof.context) option,
450 ostate: ostate, result: term * term list, tac: tac}
451 val pr_pos : int list -> string
452 val pr_ctree : (pos -> ppobj -> string) -> ctree -> string
453 val pr_short : pos -> ppobj -> string
454 val pre_pos : pos -> pos
455 val preconds2str : (bool * term) list -> string
456 datatype ptform = Form of term | ModSpec of ocalhd
457 datatype ctree = EmptyPtree | Nd of ppobj * ctree list
463 env: (istate * Proof.context) option,
465 loc: (istate * Proof.context) option * (istate * Proof.context) option,
467 origin: ori list * spec * term, ostate: ostate, probl: itm list, result: term * term list, spec: spec}
473 loc: (istate * Proof.context) option * (istate * Proof.context) option,
474 ostate: ostate, result: term * term list, tac: tac}
475 val repl : 'a list -> int -> 'a -> 'a list
476 val repl_app : 'a list -> int -> 'a -> 'a list
477 val repl_branch : branch -> ppobj -> ppobj
478 val repl_ctxt : Proof.context -> ppobj -> ppobj
479 val repl_domID : domID -> ppobj -> ppobj
480 val repl_env : (istate * Proof.context) option -> ppobj -> ppobj
481 val repl_form : term -> ppobj -> ppobj
482 val repl_loc : (istate * Proof.context) option * (istate * Proof.context) option -> ppobj -> ppobj
483 val repl_met : itm list -> ppobj -> ppobj
484 val repl_metID : metID -> ppobj -> ppobj
485 val repl_oris : ori list -> ppobj -> ppobj
486 val repl_orispec : spec -> ppobj -> ppobj
487 val repl_pbl : itm list -> ppobj -> ppobj
488 val repl_pblID : pblID -> ppobj -> ppobj
490 (istate * Proof.context) option * (istate * Proof.context) option ->
491 term * term list -> ostate -> ppobj -> ppobj
492 val repl_spec : spec -> ppobj -> ppobj
493 val repl_tac : tac -> ppobj -> ppobj
494 val res2str : term * term list -> string
495 val rls_of : tac -> rls'
496 val rls_of_rewset : tac -> rls' * subst option
497 val rootthy : ctree -> theory
498 val rta2str : rule * (term * term list) -> string
499 val rule2tac : theory -> (term * term) list -> rule -> tac
500 val safe2str : safe -> string
501 type scrstate = env * loc_ * term option * term * safe * bool
502 val scrstate2str : subst * loc_ * term option * term * safe * bool -> string
503 val str2pos_ : string -> pos_
504 type sube = cterm' list
505 val sube2str : string list -> string
506 val sube2subst : theory -> string list -> (term * term) list
507 val sube2subte : string list -> term list
508 type subs = cterm' list
509 val subs2subst : theory -> string list -> (term * term) list
510 val subst2sube : (term * term) list -> string list
511 val subst2subs : (term * term) list -> string list
512 val subst2subs' : (term * term) list -> (string * string) list
513 type subte = term list
514 val subte2str : term list -> string
515 val subte2sube : term list -> string list
516 val subte2subst : term list -> (term * term) list
518 = Add_Find of cterm' | Add_Given of cterm' | Add_Relation of cterm' | Apply_Assumption of cterm' list
519 | Apply_Method of metID | Begin_Sequ | Begin_Trans | CAScmd of cterm' | Calculate of string
520 | Check_Postcond of pblID | Check_elementwise of cterm' | Collect_Trues | Conclude_And | Conclude_Or
521 | Del_Find of cterm' | Del_Given of cterm' | Del_Relation of cterm' | Derive of rls' | Detail_Set of rls'
522 | Detail_Set_Inst of subs * rls' | Empty_Tac | End_Detail | End_Intersect | End_Proof' | End_Ruleset
523 | End_Sequ | End_Subproblem | End_Trans | Free_Solve | Group of con * int list
524 | Init_Proof of cterm' list * spec | Model_Problem | Or_to_List | Refine_Problem of pblID
525 | Refine_Tacitly of pblID | Rewrite of thm'' | Rewrite_Asm of thm'' | Rewrite_Inst of subs * thm''
526 | Rewrite_Set of rls' | Rewrite_Set_Inst of subs * rls' | Specify_Method of metID
527 | Specify_Problem of pblID | Specify_Theory of domID | Split_And | Split_Intersect | Split_Or
528 | Subproblem of domID * pblID | Substitute of sube | Tac of string | Take of cterm' | Take_Inst of cterm'
529 val tac2IDstr : tac -> string
531 = Add_Find' of cterm' * itm list | Add_Given' of cterm' * itm list | Add_Relation' of cterm' * itm list
532 | Apply_Assumption' of term list * term | Apply_Method' of metID * term option * istate * Proof.context
533 | Begin_Sequ' | Begin_Trans' of term | CAScmd' of term
534 | Calculate' of theory' * string * term * (term * thm') | Check_Postcond' of pblID * (term * term list)
535 | Check_elementwise' of term * string * (term * term list) | Collect_Trues' of term
536 | Conclude_And' of term | Conclude_Or' of term | Del_Find' of cterm' | Del_Given' of cterm'
537 | Del_Relation' of cterm' | Derive' of rls
538 | Detail_Set' of theory' * bool * rls * term * (term * term list)
539 | Detail_Set_Inst' of theory' * bool * subst * rls * term * (term * term list) | Empty_Tac_
540 | End_Detail' of term * term list | End_Intersect' of term | End_Proof'' | End_Ruleset' of term
541 | End_Sequ' | End_Subproblem' of term | End_Trans' of term * term list | Free_Solve'
542 | Group' of con * int list * term | Init_Proof' of cterm' list * spec
543 | Model_Problem' of pblID * itm list * itm list | Or_to_List' of term * term
544 | Refine_Problem' of pblID * (itm list * (bool * term) list)
545 | Refine_Tacitly' of pblID * pblID * domID * metID * itm list
546 | Rewrite' of theory' * rew_ord' * rls * bool * thm'' * term * (term * term list)
547 | Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm'' * term * (term * term list)
548 | Rewrite_Inst' of theory' * rew_ord' * rls * bool * subst * thm'' * term * (term * term list)
549 | Rewrite_Set' of theory' * bool * rls * term * (term * term list)
550 | Rewrite_Set_Inst' of theory' * bool * subst * rls * term * (term * term list)
551 | Specify_Method' of metID * ori list * itm list
552 | Specify_Problem' of pblID * (bool * (itm list * (bool * term) list)) | Specify_Theory' of domID
553 | Split_And' of term | Split_Intersect' of term | Split_Or' of term
554 | Subproblem' of spec * ori list * term * fmz_ * Proof.context * term
555 | Substitute' of rew_ord_ * rls * subte * term * term | Tac_ of theory * string * string * string
556 | Take' of term | Take_Inst' of term
557 val tac_2str : tac_ -> string
558 val test_trans : ppobj -> bool
559 val thm_of_rew : tac -> thmID * subst option
560 val topt2str : term option -> string
561 val update_branch : ctree -> pos -> branch -> ctree
562 val update_ctxt : ctree -> pos -> Proof.context -> ctree
563 val update_domID : ctree -> pos -> domID -> ctree
564 val update_env : ctree -> pos -> (istate * Proof.context) option -> ctree
565 val update_loc' : ctree -> pos -> (istate * Proof.context) option * (istate * Proof.context) option -> ctree
566 val update_met : ctree -> pos -> itm list -> ctree
567 val update_metID : ctree -> pos -> metID -> ctree
568 val update_metppc : ctree -> pos -> itm list -> ctree
569 val update_oris : ctree -> pos -> ori list -> ctree
570 val update_orispec : ctree -> pos -> spec -> ctree
571 val update_pbl : ctree -> pos -> itm list -> ctree
572 val update_pblID : ctree -> pos -> pblID -> ctree
573 val update_pblppc : ctree -> pos -> itm list -> ctree
574 val update_spec : ctree -> pos -> spec -> ctree
575 val update_tac : ctree -> pos -> tac -> ctree end
579 structure Ctree(**): CALC_TREEE(**) =
582 type result = term * term list
583 type env = (term * term) list;
586 NoBranch | AndB | OrB
587 | TransitiveB (* FIXXXME.0308: set branch from met in Apply_Method
588 FIXXXME.0402: -"- in Begin_Trans'*)
589 | SequenceB | IntersectB | CollectB | MapB;
591 fun branch2str NoBranch = "NoBranch" (* for tests only *)
592 | branch2str AndB = "AndB"
593 | branch2str OrB = "OrB"
594 | branch2str TransitiveB = "TransitiveB"
595 | branch2str SequenceB = "SequenceB"
596 | branch2str IntersectB = "IntersectB"
597 | branch2str CollectB = "CollectB"
598 | branch2str MapB = "MapB";
601 Incomplete | Complete | Inconsistent (* WN041020 latter still unused *);
602 fun ostate2str Incomplete = "Incomplete" (* for tests only *)
603 | ostate2str Complete = "Complete"
604 | ostate2str Inconsistent = "Inconsistent";
607 type cid = cellID list;
609 type posel = int; (* for readability in funs accessing Ctree *)
611 val pos2str = ints2str';
613 Pbl (* PblObj-position: problem-type *)
614 | Met (* PblObj-position: method *)
615 | Frm (* PblObj-position: -> Pbl in ME (not by moveDown !)
616 | PrfObj-position: formula *)
617 | Res (* PblObj | PrfObj-position: result *)
618 | Und; (* undefined*)
619 fun pos_2str Pbl = "Pbl"
620 | pos_2str Met = "Met"
621 | pos_2str Frm = "Frm"
622 | pos_2str Res = "Res"
623 | pos_2str Und = "Und";
624 fun str2pos_ "Pbl" = Pbl
625 | str2pos_ "Met" = Met
626 | str2pos_ "Frm" = Frm
627 | str2pos_ "Res" = Res
628 | str2pos_ "Und" = Und
629 | str2pos_ str = error ("str2pos_: wrong argument = " ^ str)
631 type pos' = pos * pos_;
632 (*WN0312 remembering interator (pos * pos_) for ctree
633 pos : lev_on, lev_dn, lev_up,
634 lev_onFrm, lev_dnRes (..see solve Apply_Method !)
636 # generate1 sets pos_ if possible ...?WN0502?NOT...
637 # generate1 does NOT set pos, because certain nodes can be lev_on OR lev_dn
638 exceptions: Begin/End_Trans
639 # thus generate(1) called in
641 .# nxt_solv (tac_ -cases); general case:
642 val pos' = case pos' of (p,Res) => (lev_on p',Res) | _ => pos'
644 generate1...(Rewrite(f,..,res))..(pos, pos_)
645 cappend_atomic.................pos ////// gets f+res always!!!
646 cut_tree....................pos, pos_
648 fun pos'2str (p, p_) = pair2str (ints2str' p, pos_2str p_);
649 fun pos's2str ps = (strs2str' o (map pos'2str)) ps; (* for tests only *)
650 val e_pos' = ([], Und);
652 fun res2str (t, ts) = pair2str (term2str t, terms2str ts);
656 (*26.4.02: never used after introduction of scripts !!!
657 type loc = loc_ * (* + interpreter-state *)
658 (loc_ * rls') (* -"- for script of the ruleset*)
660 val e_loc = ([],NONE):loc;
661 val ee_loc = (e_loc,e_loc);*)
664 datatype safe = Sundef | Safe | Unsafe | Helpless;
665 fun safe2str Sundef = "Sundef"
666 | safe2str Safe = "Safe"
667 | safe2str Unsafe = "Unsafe"
668 | safe2str Helpless = "Helpless";
670 type subs = cterm' list; (*16.11.00 for FE-KE*)
671 val e_subs = ["(bdv, x)"];
673 (* argument type of tac Rewrite_Inst *)
674 type sube = cterm' list;
675 val e_sube = []: cterm' list;
676 fun sube2str s = strs2str s;
678 (*._sub_stitution as _t_erms of _e_qualities.*)
679 type subte = term list;
680 val e_subte = []: term list;
681 fun subte2str ss = terms2str ss;
683 val subte2sube = map term2str;
684 val subst2subs = map (pair2str o (apfst term2str) o (apsnd term2str));
685 fun subst2sube subst = map term2str (map HOLogic.mk_eq subst)
686 val subst2subs' = map ((apfst term2str) o (apsnd term2str));
687 fun subs2subst thy s = map (isapair2pair o (parse_patt thy)) s;
688 fun sube2subst thy s = map (dest_equals' o (parse_patt thy)) s;
689 val sube2subte = map str2term;
690 val subte2subst = map HOLogic.dest_eq;
692 fun isasub2subst isasub = ((map isapair2pair) o isalist2list) isasub;
694 type scrstate = (*state for script interpreter*)
695 env(*stack*) (*used to instantiate tac for checking assod
696 12.03.noticed: e_ not updated during execution ?!?*)
697 * loc_ (*location of tac in script*)
698 * term option(*argument of curried functions*)
699 * term (*value obtained by tac executed
700 updated also after a derivation by 'new_val'*)
701 * safe (*estimation of how result will be obtained*)
702 * bool; (*true = strongly .., false = weakly associated:
703 only used during ass_dn/up*)
704 val e_scrstate = ([],[],NONE,e_term,Sundef,false): scrstate;
705 fun topt2str NONE = "NONE"
706 | topt2str (SOME t) = "SOME" ^ term2str t;
707 fun scrstate2str (env, loc_, topt, t, safe, bool) =
708 "(" ^ env2str env ^ ", " ^ loc_2str loc_ ^ ", " ^ topt2str topt ^ ", \n" ^
709 term2str t ^ ", " ^ safe2str safe ^ ", " ^ bool2str bool ^ ")";
711 (* for handling type istate see fun from_pblobj_or_detail', +? *)
712 datatype istate = (*interpreter state*)
713 Uistate (*undefined in modspec, in '_deriv'ation*)
714 | ScrState of scrstate (*for script interpreter*)
715 | RrlsState of rrlsstate; (*for reverse rewriting*)
716 val e_istate = (ScrState ([],[],NONE,e_term,Sundef,false));
717 val e_ctxt = Proof_Context.init_global @{theory "Pure"};
719 (* ATTENTION: does _not_ recognise Variable.declare_constraints, etc...*)
720 fun is_e_ctxt ctxt = Theory.eq_thy (Proof_Context.theory_of ctxt, @{theory "Pure"});
722 type iist = istate option * istate option;
723 (*val e_iist = (e_istate, e_istate); --- sinnlos f"ur NICHT-equality-type*)
726 fun rta2str (r,(t,a)) = "\n("^(rule2str r)^",("^(term2str t)^", "^
728 fun istate2str Uistate = "Uistate"
729 | istate2str (ScrState (e, l, to, t, s, b)) =
730 "ScrState ("^ subst2str e ^",\n "^
731 loc_2str l ^", "^ termopt2str to ^",\n "^
732 term2str t ^", "^ safe2str s ^", "^ bool2str b ^")"
733 | istate2str (RrlsState (t,t1,rss,rtas)) =
734 "RrlsState ("^(term2str t)^", "^(term2str t1)^", "^
735 ((strs2str o (map (strs2str o (map rule2str)))) rss)^", "^
736 ((strs2str o (map rta2str)) rtas)^")";
737 fun istates2str (NONE, NONE) = "(#NONE, #NONE)"
738 | istates2str (NONE, SOME ist) = "(#NONE,\n#SOME "^istate2str ist^")"
739 | istates2str (SOME ist, NONE) = "(#SOME "^istate2str ist^",\n #NONE)"
740 | istates2str (SOME i1, SOME i2) = "(#SOME "^istate2str i1^",\n #SOME "^
743 fun new_val v (ScrState (env, loc_, topt, _, safe, bool)) =
744 (ScrState (env, loc_, topt, v, safe, bool))
745 | new_val _ _ = error "new_val: only for ScrState";
747 datatype con = land | lor;
751 (*.tactics propagate the construction of the calc-tree;
753 (a) 'specsteps' for the specify-phase, and others for the solve-phase
754 (b) those of the solve-phase are 'initac's and others;
755 initacs start with a formula different from the preceding formula.
756 see 'type tac_' for the internal representation of tactics.*)
757 datatype tac = (* TODO: arrange according to signature *)
758 Init_Proof of ((cterm' list) * spec)
761 | Refine_Problem of pblID | Refine_Tacitly of pblID
763 | Add_Given of cterm' | Del_Given of cterm'
764 | Add_Find of cterm' | Del_Find of cterm'
765 | Add_Relation of cterm' | Del_Relation of cterm'
767 | Specify_Theory of domID | Specify_Problem of pblID
768 | Specify_Method of metID
770 | Apply_Method of metID
771 (*.creates an 'istate' in PblObj.env; in case of 'init_form'
772 creates a formula at ((lev_on o lev_dn) p, Frm) and in this ppobj.'loc'
773 'SOME istate' (at fst of 'loc').
774 As each step (in the solve-phase) has a resulting formula (at the front-end)
775 Apply_Method also does the 1st step in the script (an 'initac') if there
776 is no 'init_form' .*)
777 | Check_Postcond of pblID
780 (* rewrite-tactics can transport a (thmID, thm) to and (!) from the java-front-end
781 because there all the thms are present with both (thmID, thm)
782 (where user-views can show both or only one of (thmID, thm)),
783 and thm is created from ThmID by assoc_thm'' when entering isabisac *)
784 | Rewrite_Inst of ( subs * thm'') | Rewrite of thm'' | Rewrite_Asm of thm''
785 | Rewrite_Set_Inst of ( subs * rls') | Rewrite_Set of rls'
786 | Detail_Set_Inst of ( subs * rls') | Detail_Set of rls'
787 | End_Detail (*end of script from next_tac,
788 in solve: switches back to parent script WN0509 drop!*)
789 | Derive of rls' (*an input formula using rls WN0509 drop!*)
790 | Calculate of string (* plus | minus | times | cancel | pow | sqrt *)
792 | Substitute of sube | Apply_Assumption of cterm' list
794 | Take of cterm' (*an 'initac'*)
795 | Take_Inst of cterm'
796 | Group of (con * int list )
797 | Subproblem of (domID * pblID) (*an 'initac'*)
798 | CAScmd of cterm' (*6.6.02 URD: Function formula; WN0509 drop!*)
799 | End_Subproblem (*WN0509 drop!*)
801 | Split_And | Conclude_And
802 | Split_Or | Conclude_Or
803 | Begin_Trans | End_Trans
804 | Begin_Sequ | End_Sequ(* substitute root.env *)
805 | Split_Intersect | End_Intersect
806 | Check_elementwise of cterm' | Collect_Trues
807 | Or_to_List (*WN120315 ~ @{thm d2_prescind1},2,3,4 in PolyEq.thy *)
809 | Empty_Tac (* TODO.11.6.03 ... of string: could carry msg of (Notappl msg)
811 | Tac of string (* eg.'repeat'*WN0509 drop! (ab)used to report syntaxerror *)
812 | End_Proof'; (* inout *)
814 (* tac2str /--> library.sml: needed in dialog.sml for 'separable *)
815 fun tac2str ma = case ma of
816 Init_Proof (ppc, spec) =>
817 "Init_Proof "^(pair2str (strs2str ppc, spec2str spec))
818 | Model_Problem => "Model_Problem "
819 | Refine_Tacitly pblID => "Refine_Tacitly "^(strs2str pblID)
820 | Refine_Problem pblID => "Refine_Problem "^(strs2str pblID)
821 | Add_Given cterm' => "Add_Given "^cterm'
822 | Del_Given cterm' => "Del_Given "^cterm'
823 | Add_Find cterm' => "Add_Find "^cterm'
824 | Del_Find cterm' => "Del_Find "^cterm'
825 | Add_Relation cterm' => "Add_Relation "^cterm'
826 | Del_Relation cterm' => "Del_Relation "^cterm'
828 | Specify_Theory domID => "Specify_Theory "^(quote domID )
829 | Specify_Problem pblID => "Specify_Problem "^(strs2str pblID )
830 | Specify_Method metID => "Specify_Method "^(strs2str metID)
831 | Apply_Method metID => "Apply_Method "^(strs2str metID)
832 | Check_Postcond pblID => "Check_Postcond "^(strs2str pblID)
833 | Free_Solve => "Free_Solve"
835 | Rewrite_Inst (subs, (id, thm)) =>
836 "Rewrite_Inst " ^ (pair2str (subs2str subs, spair2str (id, thm |> Thm.prop_of |> term2str)))
837 | Rewrite (id, thm) => "Rewrite " ^ spair2str (id, thm |> Thm.prop_of |> term2str)
838 | Rewrite_Asm (id, thm) => "Rewrite_Asm " ^ spair2str (id, thm |> Thm.prop_of |> term2str)
839 | Rewrite_Set_Inst (subs, rls) =>
840 "Rewrite_Set_Inst "^(pair2str (subs2str subs, quote rls))
841 | Rewrite_Set rls => "Rewrite_Set "^(quote rls )
842 | Detail_Set rls => "Detail_Set "^(quote rls )
843 | Detail_Set_Inst (subs, rls) =>
844 "Detail_Set_Inst "^(pair2str (subs2str subs, quote rls))
845 | End_Detail => "End_Detail"
846 | Derive rls' => "Derive "^rls'
847 | Calculate op_ => "Calculate "^op_
848 | Substitute sube => "Substitute "^sube2str sube
849 | Apply_Assumption ct's => "Apply_Assumption "^(strs2str ct's)
851 | Take cterm' => "Take "^(quote cterm' )
852 | Take_Inst cterm' => "Take_Inst "^(quote cterm' )
853 | Group (con, ints) =>
854 "Group "^(pair2str (con2str con, ints2str ints))
855 | Subproblem (domID, pblID) =>
856 "Subproblem "^(pair2str (domID, strs2str pblID))
857 (*| Subproblem_Full (spec, cts') =>
858 "Subproblem_Full "^(pair2str (spec2str spec, strs2str cts'))*)
859 | End_Subproblem => "End_Subproblem"
860 | CAScmd cterm' => "CAScmd "^(quote cterm')
862 | Check_elementwise cterm'=> "Check_elementwise "^(quote cterm')
863 | Or_to_List => "Or_to_List "
864 | Collect_Trues => "Collect_Trues"
866 | Empty_Tac => "Empty_Tac"
867 | Tac string => "Tac "^string
868 | End_Proof' => "tac End_Proof'"
869 | _ => "tac2str not impl. for ?!";
871 fun is_empty_tac tac = case tac of Empty_Tac => true | _ => false
873 fun eq_tac (Rewrite (id1, _), Rewrite (id2, _)) = id1 = id2
874 | eq_tac (Rewrite_Inst (_, (id1, _)), Rewrite_Inst (_, (id2, _))) = id1 = id2
875 | eq_tac (Rewrite_Set id1, Rewrite_Set id2) = id1 = id2
876 | eq_tac (Rewrite_Set_Inst (_, id1), Rewrite_Set_Inst (_, id2)) = id1 = id2
877 | eq_tac (Calculate id1, Calculate id2) = id1 = id2
880 fun is_rewset (Rewrite_Set_Inst _) = true
881 | is_rewset (Rewrite_Set _) = true
882 | is_rewset _ = false;
883 fun is_rewtac (Rewrite _) = true
884 | is_rewtac (Rewrite_Inst _) = true
885 | is_rewtac (Rewrite_Asm _) = true
886 | is_rewtac tac = is_rewset tac;
888 fun tac2IDstr ma = case ma of
889 Model_Problem => "Model_Problem"
890 | Refine_Tacitly pblID => "Refine_Tacitly"
891 | Refine_Problem pblID => "Refine_Problem"
892 | Add_Given cterm' => "Add_Given"
893 | Del_Given cterm' => "Del_Given"
894 | Add_Find cterm' => "Add_Find"
895 | Del_Find cterm' => "Del_Find"
896 | Add_Relation cterm' => "Add_Relation"
897 | Del_Relation cterm' => "Del_Relation"
899 | Specify_Theory domID => "Specify_Theory"
900 | Specify_Problem pblID => "Specify_Problem"
901 | Specify_Method metID => "Specify_Method"
902 | Apply_Method metID => "Apply_Method"
903 | Check_Postcond pblID => "Check_Postcond"
904 | Free_Solve => "Free_Solve"
906 | Rewrite_Inst (subs,thm')=> "Rewrite_Inst"
907 | Rewrite thm' => "Rewrite"
908 | Rewrite_Asm thm' => "Rewrite_Asm"
909 | Rewrite_Set_Inst (subs, rls) => "Rewrite_Set_Inst"
910 | Rewrite_Set rls => "Rewrite_Set"
911 | Detail_Set rls => "Detail_Set"
912 | Detail_Set_Inst (subs, rls) => "Detail_Set_Inst"
913 | Derive rls' => "Derive "
914 | Calculate op_ => "Calculate "
915 | Substitute subs => "Substitute"
916 | Apply_Assumption ct's => "Apply_Assumption"
918 | Take cterm' => "Take"
919 | Take_Inst cterm' => "Take_Inst"
920 | Group (con, ints) => "Group"
921 | Subproblem (domID, pblID) => "Subproblem"
922 | End_Subproblem => "End_Subproblem"
923 | CAScmd cterm' => "CAScmd"
925 | Check_elementwise cterm'=> "Check_elementwise"
926 | Or_to_List => "Or_to_List "
927 | Collect_Trues => "Collect_Trues"
929 | Empty_Tac => "Empty_Tac"
930 | Tac string => "Tac "
931 | End_Proof' => "End_Proof'"
932 | _ => "tac2str not impl. for ?!";
934 fun rls_of (Rewrite_Set_Inst (_, rls)) = rls
935 | rls_of (Rewrite_Set rls) = rls
936 | rls_of tac = error ("rls_of: called with tac '"^tac2IDstr tac^"'");
938 fun thm_of_rew (Rewrite_Inst (subs,(thmID,_))) =
939 (thmID, SOME ((subs2subst (assoc_thy "Isac") subs)))
940 | thm_of_rew (Rewrite (thmID,_)) = (thmID, NONE)
941 | thm_of_rew (Rewrite_Asm (thmID,_)) = (thmID, NONE);
943 fun rls_of_rewset (Rewrite_Set_Inst (subs,rls)) =
944 (rls, SOME ((subs2subst (assoc_thy "Isac") subs)))
945 | rls_of_rewset (Rewrite_Set rls) = (rls, NONE)
946 | rls_of_rewset (Detail_Set rls) = (rls, NONE)
947 | rls_of_rewset (Detail_Set_Inst (subs, rls)) =
948 (rls, SOME ((subs2subst (assoc_thy "Isac") subs)));
950 fun rule2tac thy _ (Calc (opID, thm)) = Calculate (assoc_calc thy opID)
951 | rule2tac _ [] (Thm thm'') = Rewrite thm''
952 | rule2tac _ subst (Thm thm'') =
953 Rewrite_Inst (subst2subs subst, thm'')
954 | rule2tac _ [] (Rls_ rls) = Rewrite_Set (id_rls rls)
955 | rule2tac _ subst (Rls_ rls) =
956 Rewrite_Set_Inst (subst2subs subst, (id_rls rls))
957 | rule2tac _ _ rule =
958 error ("rule2tac: called with '" ^ rule2str rule ^ "'");
960 type fmz_ = cterm' list;
962 (*.a formalization of an example containing data
963 sufficient for mechanically finding the solution for the example.*)
964 (*FIXME.WN051014: dont store fmz = (_,spec) in the PblObj,
965 this is done in origin*)
966 type fmz = fmz_ * spec;
967 val e_fmz = ([],e_spec);
969 (* tac_ contains results from check in 'fun applicable_in'.
970 This is useful for costly results, e.g. from rewriting;
971 however, these results might be changed by Scripts like
972 " eq = (Rewrite_Set ansatz_rls False) eql;" ^
973 " eq = drop_questionmarks eq;" ^
974 " eq = (Rewrite_Set equival_trans False) eq;" ^
975 WN120106 TODO ANALOGOUSLY TO Substitute':
976 So tac_ contains the term t the result was calculated from
977 in order to compare t with t' possibly changed by "Expr "
978 and re-calculate result if t<>t'*)
979 datatype tac_ = (* TODO: arrange according to signature *)
980 Init_Proof' of ((cterm' list) * spec)
983 itm list * (*the 'untouched' pbl*)
984 itm list (*the casually completed met*)
987 pblID * (*the refined from applicable_in*)
988 domID * (*from new pbt?! filled in specify*)
989 metID * (*from new pbt?! filled in specify*)
990 itm list (*drop ! 9.03: remains [] for
991 Model_Problem recognizing its activation*)
992 | Refine_Problem' of (pblID * (itm list * (bool * Term.term) list))
993 (*FIXME?040215 drop: done automatically in init_proof + Subproblem'*)
996 itm list (*updated with input in fun specify_additem*)
997 | Add_Find' of cterm' * itm list (* see Add_Given' *)
998 | Add_Relation' of cterm' * itm list (* see Add_Given' *)
999 | Del_Given' of cterm' | Del_Find' of cterm' | Del_Relation' of cterm'
1000 (*4.00.: all.. term: in applicable_in ..? Syn ?only for FormFK?*)
1001 | Specify_Theory' of domID
1002 | Specify_Problem' of
1004 (bool * (* matches *)
1005 (itm list * (* ppc *)
1006 (bool * term) list))) (* preconditions *)
1007 | Specify_Method' of
1009 ori list * (*repl. "#undef"*)
1010 itm list (*... updated from pbl to met*)
1013 (term option) * (*init_form*)
1014 istate * Proof.context
1015 | Check_Postcond' of
1017 (term * (*returnvalue of script in solve*)
1018 term list) (*collect by get_assumptions_ in applicable_in, except if
1019 butlast tac is Check_elementwise: take only these asms*)
1021 (* context_thy would be simpler if instead thm' woudl be thm *)
1022 | Rewrite_Inst' of theory' * rew_ord' * rls * bool * subst * thm'' * term * (term * term list)
1023 | Rewrite' of theory' * rew_ord' * rls * bool * thm'' * term * result
1024 | Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm'' * term * result
1025 | Rewrite_Set_Inst' of theory' * bool * subst * rls * term * result
1026 | Detail_Set_Inst' of theory' * bool * subst * rls * term * result
1027 | Rewrite_Set' of theory' * bool * rls * term * result
1028 | Detail_Set' of theory' * bool * rls * term * result
1029 | End_Detail' of (term * (term list)) (*see End_Trans'*)
1030 | End_Ruleset' of term
1032 | Calculate' of theory' * string * term * (term * thm')
1034 rew_ord_ * (*for re-calculation *)
1035 rls * (*for re-calculation *)
1036 subte * (*the 'substitution': terms of type bool*)
1037 term * (*to be substituted in *)
1038 term (*resulting from the substitution *)
1039 | Apply_Assumption' of term list * term
1041 | Take_Inst' of term
1044 (ori list) * (* filled in assod Subproblem' *)
1045 term * (*-"-, headline of calc-head *)
1047 Proof.context *(* transported from assod to generate1 *)
1048 term) (* Subproblem(dom,pbl) OR cascmd*)
1050 | End_Subproblem' of term (*???*)
1051 | Split_And' of term | Conclude_And' of term
1052 | Split_Or' of term | Conclude_Or' of term
1053 | Begin_Trans' of term | End_Trans' of (term * (term list))
1054 | Begin_Sequ' | End_Sequ'(* substitute root.env*)
1055 | Split_Intersect' of term | End_Intersect' of term
1056 | Check_elementwise' of (*special case:*)
1057 term * (*(1)the current formula: [x=1,x=...]*)
1058 string * (*(2)the pred from Check_elementwise *)
1059 (term * (*(3)composed from (1) and (2): {x. pred}*)
1060 term list) (*20.5.03 assumptions*)
1061 | Or_to_List' of term * term (* (a | b, [a,b]) *)
1062 | Collect_Trues' of term
1064 | Tac_ of (*for dummies*)
1068 string (*result of Tac".."*)
1069 | End_Proof'';(*End_Proof:inout*)
1071 fun tac_2str ma = case ma of
1072 Init_Proof' (ppc, spec) =>
1073 "Init_Proof' "^(pair2str (strs2str ppc, spec2str spec))
1074 | Model_Problem' (pblID,_,_) => "Model_Problem' "^(strs2str pblID )
1075 | Refine_Tacitly'(p,prefin,domID,metID,itms)=>
1077 ^(strs2str p)^", "^(strs2str prefin)^", "
1078 ^domID^", "^(strs2str metID)^", pbl-itms)"
1079 | Refine_Problem' ms => "Refine_Problem' ("^(*matchs2str ms*)"..."^")"
1080 (*| Match_Problem' (pI, (ok, (itms, pre))) =>
1081 "Match_Problem' "^(spair2str (strs2str pI,
1082 spair2str (bool2str ok,
1083 spair2str ("itms2str_ itms",
1084 "items2str pre"))))*)
1085 | Add_Given' cterm' => "Add_Given' "(*^cterm'*)
1086 | Del_Given' cterm' => "Del_Given' "(*^cterm'*)
1087 | Add_Find' cterm' => "Add_Find' "(*^cterm'*)
1088 | Del_Find' cterm' => "Del_Find' "(*^cterm'*)
1089 | Add_Relation' cterm' => "Add_Relation' "(*^cterm'*)
1090 | Del_Relation' cterm' => "Del_Relation' "(*^cterm'*)
1092 | Specify_Theory' domID => "Specify_Theory' "^(quote domID )
1093 | Specify_Problem' (pI, (ok, (itms, pre))) =>
1094 "Specify_Problem' "^(spair2str (strs2str pI,
1095 spair2str (bool2str ok,
1096 spair2str ("itms2str_ itms",
1098 | Specify_Method' (pI,oris,itms) =>
1099 "Specify_Method' ("^metID2str pI^", "^oris2str oris^", )"
1101 | Apply_Method' (metID,_,_,_) => "Apply_Method' "^(strs2str metID)
1102 | Check_Postcond' (pblID,(scval,asm)) =>
1103 "Check_Postcond' " ^
1104 (spair2str (strs2str pblID, spair2str (term2str scval, terms2str asm)))
1106 | Free_Solve' => "Free_Solve'"
1108 | Rewrite_Inst' (*subs,thm'*) _ =>
1109 "Rewrite_Inst' "(*^(pair2str (subs2str subs, spair2str thm'))*)
1110 | Rewrite' thm' => "Rewrite' "(*^(spair2str thm')*)
1111 | Rewrite_Asm' thm' => "Rewrite_Asm' "(*^(spair2str thm')*)
1112 | Rewrite_Set_Inst' (*subs,thm'*) _ =>
1113 "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*)
1114 | Rewrite_Set' (thy', pasm, rls', f, (f', asm)) =>
1115 "Rewrite_Set' (" ^ thy' ^ "," ^ bool2str pasm ^ "," ^ id_rls rls' ^ "," ^
1116 term2str f ^ ",(" ^ term2str f' ^ "," ^ terms2str asm ^ "))"
1117 | End_Detail' _ => "End_Detail' xxx"
1118 | Detail_Set' _ => "Detail_Set' xxx"
1119 | Detail_Set_Inst' _ => "Detail_Set_Inst' xxx"
1121 | Derive' rls => "Derive' "^id_rls rls
1122 | Calculate' _ => "Calculate' "
1123 | Substitute' _ => "Substitute' "(*^(subs2str subs)*)
1124 | Apply_Assumption' ct's => "Apply_Assumption' "(*^(strs2str ct's)*)
1126 | Take' cterm' => "Take' "(*^(quote cterm' )*)
1127 | Take_Inst' cterm' => "Take_Inst' "(*^(quote cterm' )*)
1128 | Subproblem' (spec, oris, _, _, _, pbl_form) =>
1129 "Subproblem' "(*^(pair2str (domID, strs2str ,...))*)
1130 | End_Subproblem' _ => "End_Subproblem'"
1131 | CAScmd' cterm' => "CAScmd' "(*^(quote cterm')*)
1133 | Empty_Tac_ => "Empty_Tac_"
1134 | Tac_ (_,form,id,result) => "Tac_ (thy,"^form^","^id^","^result^")"
1135 | _ => "tac_2str not impl. for arg";
1137 (*'executed tactics' (tac_s) with local environment etc.;
1138 used for continuing eval script + for generate*)
1140 (loc_ * (* of tactic in scr, tactic (weakly) associated with tac_*)
1141 (tac_ * (* (for generate) *)
1142 env * (* with 'tactic=result' as a rule, tactic ev. _not_ ready:
1143 for handling 'parallel let'*)
1144 env * (* with results of (ready) tacs *)
1145 term * (* itr_arg of tactic, for upd. env at Repeat, Try*)
1146 term * (* result value of the tac *)
1152 fun ets2s (l,(m,eno,env,iar,res,s)) =
1153 "\n(" ^ loc_2str l ^ ",(" ^ tac_2str m ^
1154 ",\n ens= " ^ subst2str eno ^
1155 ",\n env= " ^ subst2str env ^
1156 ",\n iar= " ^ term2str iar ^
1157 ",\n res= " ^ term2str res ^
1158 ",\n " ^ safe2str s ^ "))";
1159 fun ets2str (ets: ets) = (strs2str o (map ets2s)) ets;
1162 type envp =(*9.5.03: unused, delete with field in ctree.PblObj FIXXXME*)
1163 (int * term list) list * (*assoc-list: args of met*)
1164 (int * rls) list * (*assoc-list: tacs already done ///15.9.00*)
1165 (int * ets) list * (*assoc-list: tacs etc. already done*)
1166 (string * pos) list; (*asms * from where*)
1167 val empty_envp = ([], [], [], []): envp;
1169 datatype ppobj = (* TODO: arrange according to signature *)
1171 {cell : lrd option, (* where in form tac has been applied *)
1172 (*^^^FIXME.WN0607 rename this field*)
1173 form : term, (* where tac is applied to *)
1174 tac : tac, (* also in istate *)
1175 loc : (istate * (* script interpreter state *)
1176 Proof.context) (* context for provers, type inference *)
1177 option * (* both for interpreter location on Frm, Pbl, Met *)
1178 (istate * (* script interpreter state *)
1179 Proof.context) (* context for provers, type inference *)
1180 option, (* both for interpreter location on Res *)
1181 (*(NONE,NONE) <==> e_istate ! see update_loc, get_loc*)
1182 branch: branch, (* only rudimentary *)
1183 result: result, (* result and assumptions *)
1184 ostate: ostate} (* Complete <=> result is OK *)
1186 {cell : lrd option, (* unused: meaningful only for some _Prf_Obj *)
1187 fmz : fmz, (* from init:FIXME never use this spec;-drop *)
1188 origin: (ori list) * (* representation from fmz+pbt
1189 for efficiently adding items in probl, meth *)
1190 spec * (* updated by Refine_Tacitly *)
1191 term, (* headline of calc-head, as calculated initially(!)*)
1192 spec : spec, (* explicitly input *)
1193 probl : itm list, (* itms explicitly input *)
1194 meth : itm list, (* itms automatically added to copy of probl *)
1195 ctxt : Proof.context, (* WN110513 introduced to avoid [*] [**]*)
1196 env : (istate * Proof.context) option,
1197 (* istate only for initac in script
1198 context for specify phase on this node NO..
1199 ..NO: this conflicts with init_form/initac: see Apply_Method without init_form *)
1200 loc : (istate * Proof.context) option * (istate * (* like PrfObj *)
1201 Proof.context) option, (* for spec-phase [*], NO..
1202 ..NO: raises errors not tracable on WN110513 [**]*)
1203 branch: branch, (* like PrfObj *)
1204 result: result, (* like PrfObj *)
1205 ostate: ostate}; (* like PrfObj *)
1207 (*.this tree contains isac's calculations; TODO.WN03 rename to ctree;
1208 the structure has been copied from an early version of Theorema(c);
1209 it has the disadvantage, that there is no space
1210 for the first tactic in a script generating the first formula at (p,Frm);
1211 this trouble has been covered by 'init_form' and 'Take' so far,
1212 but it is crucial if the first tactic in a script is eg. 'Subproblem';
1213 see 'type tac ', Apply_Method.
1217 | Nd of ppobj * (ctree list);
1218 val e_ctree = EmptyPtree;
1219 type state = ctree * pos
1221 fun rep_prfobj (PrfObj {cell,form,tac,loc,branch,result,ostate}) =
1222 {cell=cell,form=form,tac=tac,loc=loc,branch=branch,result=result,ostate=ostate};
1223 fun rep_pblobj (PblObj {cell,origin,fmz,spec,probl,meth,ctxt,
1224 env,loc,branch,result,ostate}) =
1225 {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,meth=meth,ctxt=ctxt,
1226 env=env,loc=loc,branch=branch,result=result,ostate=ostate};
1227 fun is_prfobj (PrfObj _) = true
1228 | is_prfobj _ =false;
1229 (*val is_prfobj' = get_obj is_prfobj; *)
1230 fun is_pblobj (PblObj _) = true
1231 | is_pblobj _ = false;
1232 (*val is_pblobj' = get_obj is_pblobj; 'Error: unbound constructor get_obj'*)
1235 exception PTREE of string;
1236 fun nth _ [] = raise PTREE "nth _ []"
1238 | nth n (x::xs) = nth (n-1) xs;
1239 (*> nth 2 [11,22,33]; -->> val it = 22 : int*)
1241 fun lev_up [] = raise PTREE "lev_up []"
1242 | lev_up p = (drop_last p):pos;
1243 fun lev_on [] = raise PTREE "lev_on []"
1245 let val len = length pos
1246 in (drop_last pos) @ [(nth len pos)+1] end;
1247 fun lev_onFrm (p,_) = (lev_on p,Frm):pos'
1248 | lev_onFrm p = raise PTREE ("*** lev_onFrm: pos'="^(pos'2str p));
1249 (*040216: for inform --> embed_deriv: remains on same level TODO.WN120517 compare lev_pred*)
1250 fun lev_back' ([],_) = raise PTREE "lev_back': called by ([],_)"
1252 if last_elem p <= 1 then (p, Frm):pos'
1253 else ((drop_last p) @ [(nth (length p) p) - 1], Res);
1254 (*.increase pos by n within a level.*)
1255 fun pos_plus 0 pos = pos
1256 | pos_plus n (p,Frm) = pos_plus (n-1) (p, Res)
1257 | pos_plus n (p, _) = pos_plus (n-1) (lev_on p, Res);
1259 fun lev_pred [] = raise PTREE "lev_pred []"
1261 let val len = length pos
1262 in ((drop_last pos) @ [(nth len pos)-1]) end;
1264 val it = [1,2,2] : pos
1266 val it = [0] : pos *)
1268 fun lev_dn p = p @ [0];
1269 (*> (lev_dn o lev_on) [1,2,3];
1270 val it = [1,2,4,0] : pos *)
1271 (*fun lev_dn' ((p,p_):pos') = (lev_dn p, Frm):pos'; WN.3.12.03: never used*)
1272 fun lev_dnRes (p,_) = (lev_dn p, Res);
1275 fun lev_up_ (p,Res) = (lev_up p,Res):pos'
1276 | lev_up_ p' = error ("lev_up_: called for "^(pos'2str p'));
1277 fun lev_dn_ (p, _) = (lev_dn p, Res)
1278 fun ind (p,_) = length p; (*WN050108 deprecated in favour of lev_of*)
1279 fun lev_of (p,_) = length p;
1282 (** convert ctree to a string **)
1284 (* convert a pos from list to string *)
1285 fun pr_pos ps = (space_implode "." (map string_of_int ps))^". ";
1286 (* show hd origin or form only *)
1287 fun pr_short p (PblObj {origin = (ori,_,_),...}) =
1288 ((pr_pos p) ^ " ----- pblobj -----\n")
1289 (* ((((Syntax.string_of_term (thy2ctxt' "Isac")) o #4 o hd) ori)^" "^
1290 (((Syntax.string_of_term (thy2ctxt' "Isac")) o hd(*!?!*) o #5 o hd) ori))^
1292 | pr_short p (PrfObj {form = form,...}) =
1293 ((pr_pos p) ^ (term2str form) ^ "\n");
1295 fun pr_cell (p:pos) (PblObj {cell = c, origin = (ori,_,_),...}) =
1297 ((((Syntax.string_of_term (thy2ctxt' "Isac")) o #4 o hd) ori)^" "^
1298 (((Syntax.string_of_term (thy2ctxt' "Isac")) o hd(*!?!*) o #5 o hd) ori))^
1300 | pr_cell p (PrfObj {cell = c, form = form,...}) =
1301 ((ints2str c) ^" "^ (term2str form) ^ "\n");
1307 fun pr_pt pfn _ EmptyPtree = ""
1308 | pr_pt pfn ps (Nd (b, [])) = pfn ps b
1309 | pr_pt pfn ps (Nd (b, ts)) = (pfn ps b)^
1311 and prts pfn ps p [] = ""
1312 | prts pfn ps p (t::ts) = (pr_pt pfn (ps @ [p]) t)^
1313 (prts pfn ps (p+1) ts)
1314 in pr_pt f [] pt end;
1316 > fun prfn ps b = (pr_pos ps)^" "^b(*TODO*)^"\n";
1317 (*val pt = Unsynchronized.ref EmptyPtree;*)
1324 > tracing (pr_ctree prfn (!pt));
1328 (** access the branches of ctree **)
1330 fun ins_nth 1 e l = e::l
1331 | ins_nth n e [] = raise PTREE "ins_nth n e []"
1332 | ins_nth n e (l::ls) = l::(ins_nth (n-1) e ls);
1333 fun repl [] _ _ = raise PTREE "repl [] _ _"
1334 | repl (l::ls) 1 e = e::ls
1335 | repl (l::ls) n e = l::(repl ls (n-1) e);
1336 fun repl_app ls n e =
1337 let val lim = 1 + length ls
1338 in if n > lim then raise PTREE "repl_app: n > lim"
1339 else if n = lim then ls @ [e]
1340 else repl ls n e end;
1342 > repl [1,2,3] 2 22222;
1343 val it = [1,22222,3] : int list
1344 > repl_app [1,2,3,4] 5 5555;
1345 val it = [1,2,3,4,5555] : int list
1346 > repl_app [1,2,3] 2 22222;
1347 val it = [1,22222,3] : int list
1348 > repl_app [1] 2 22222 ;
1349 val it = [1,22222] : int list
1353 (*.get from obj at pos by f : ppobj -> 'a.*)
1354 fun get_obj f EmptyPtree _ = raise PTREE "get_obj f EmptyPtree"
1355 | get_obj f (Nd (b, _)) [] = f b
1356 | get_obj f (Nd (b, bs)) (p::ps) =
1357 (* val (f, Nd (b, bs), (p::ps)) = (I, pt, p);
1359 let val _ = (nth p bs) handle _ => raise PTREE ("get_obj: pos = "^
1360 (ints2str' (p::ps))^" does not exist");
1361 in (get_obj f (nth p bs) ps)
1362 (*before WN050419: 'wrong type..' raised also if pos doesn't exist*)
1363 handle _ => raise PTREE (*"get_obj: at pos = "^
1364 (ints2str' (p::ps))^" wrong type of ppobj"*)
1366 (ints2str' (p::ps))^" does not exist")
1368 fun get_nd EmptyPtree _ = raise PTREE "get_nd EmptyPtree"
1370 | get_nd (Nd (_,nds)) (pos as p :: ps) = (get_nd (nth p nds) ps)
1371 handle _ => raise PTREE ("get_nd: not existent pos = "^(ints2str' pos));
1373 (* for use by get_obj *)
1374 fun g_cell (PblObj {cell = c,...}) = NONE
1375 | g_cell (PrfObj {cell = c,...}) = c;(*WN0607 hack for quick introduction of lrd + rewrite-at (thms, calcs)*)
1376 fun g_form (PrfObj {form = f,...}) = f
1377 | g_form (PblObj {origin=(_,_,f),...}) = f;
1378 fun g_form' (Nd (PrfObj {form = f,...}, _)) = f
1379 | g_form' (Nd (PblObj {origin=(_,_,f),...}, _)) = f;
1380 (* | g_form _ = raise PTREE "g_form not for PblObj";*)
1381 fun g_origin (PblObj {origin = ori,...}) = ori
1382 | g_origin _ = raise PTREE "g_origin not for PrfObj";
1383 fun g_fmz (PblObj {fmz = f,...}) = f
1384 | g_fmz _ = raise PTREE "g_fmz not for PrfObj";
1385 fun g_spec (PblObj {spec = s,...}) = s
1386 | g_spec _ = raise PTREE "g_spec not for PrfObj";
1387 fun g_pbl (PblObj {probl = p,...}) = p
1388 | g_pbl _ = raise PTREE "g_pbl not for PrfObj";
1389 fun g_met (PblObj {meth = p,...}) = p
1390 | g_met _ = raise PTREE "g_met not for PrfObj";
1391 fun g_domID (PblObj {spec = (d,_,_),...}) = d
1392 | g_domID _ = raise PTREE "g_metID not for PrfObj";
1393 fun g_metID (PblObj {spec = (_,_,m),...}) = m
1394 | g_metID _ = raise PTREE "g_metID not for PrfObj";
1395 fun g_ctxt (PblObj {ctxt, ...}) = ctxt
1396 | g_ctxt _ = raise PTREE "g_ctxt not for PrfObj";
1397 fun g_env (PblObj {env,...}) = env
1398 | g_env _ = raise PTREE "g_env not for PrfObj";
1399 fun g_loc (PblObj {loc = l,...}) = l
1400 | g_loc (PrfObj {loc = l,...}) = l;
1401 fun g_branch (PblObj {branch = b,...}) = b
1402 | g_branch (PrfObj {branch = b,...}) = b;
1403 fun g_tac (PblObj {spec = (d,p,m),...}) = Apply_Method m
1404 | g_tac (PrfObj {tac = m,...}) = m;
1405 fun g_result (PblObj {result = r,...}) = r
1406 | g_result (PrfObj {result = r,...}) = r;
1407 fun g_res (PblObj {result = (r,_),...}) = r
1408 | g_res (PrfObj {result = (r,_),...}) = r;
1409 fun g_res' (Nd (PblObj {result = (r,_),...}, _)) = r
1410 | g_res' (Nd (PrfObj {result = (r,_),...}, _)) = r;
1411 fun g_ostate (PblObj {ostate = r,...}) = r
1412 | g_ostate (PrfObj {ostate = r,...}) = r;
1413 fun g_ostate' (Nd (PblObj {ostate = r,...}, _)) = r
1414 | g_ostate' (Nd (PrfObj {ostate = r,...}, _)) = r;
1416 fun gpt_cell (Nd (PblObj {cell = c,...},_)) = NONE
1417 | gpt_cell (Nd (PrfObj {cell = c,...},_)) = c;
1419 (* get the formula preceeding the current position in a calculation *)
1420 fun get_curr_formula (pt, pos as (p, p_)) =
1422 Frm => get_obj g_form pt p
1423 | Res => (fst o (get_obj g_result pt)) p
1424 | _ => #3 (get_obj g_origin pt p);
1426 (*in CalcTree/Subproblem an 'just_created_' model is created;
1427 this is filled to 'untouched' by Model/Refine_Problem*)
1428 fun just_created_ (PblObj {meth, probl, spec, ...}) =
1429 null meth andalso null probl andalso spec = e_spec;
1430 val e_origin = ([],e_spec,e_term);
1432 fun just_created (pt, (p, _)) =
1433 let val ppobj = get_obj I pt p
1434 in is_pblobj ppobj andalso just_created_ ppobj end;
1436 (*.does the pos in the ctree exist ?.*)
1437 fun existpt pos pt = can (get_obj I pt) pos;
1438 (*.does the pos' in the ctree exist, ie. extra check for result in the node.*)
1439 fun existpt' (p,p_) pt =
1440 if can (get_obj I pt) p
1442 Res => get_obj g_ostate pt p = Complete
1446 (*.is this position appropriate for calculating intermediate steps?.*)
1447 fun is_interpos (_, Res) = true
1448 | is_interpos _ = false;
1450 fun last_onlev pt pos = not (existpt (lev_on pos) pt);
1453 (*.find the position of the next parent which is a PblObj in ctree.*)
1454 fun par_pblobj pt [] = []
1456 let fun par pt [] = []
1457 | par pt p = if is_pblobj (get_obj I pt p) then p
1458 else par pt (lev_up p)
1459 in par pt (lev_up p) end;
1460 (* lev_up for hard_gen operating with pos = [...,0] *)
1462 (*.find the position and the children of the next parent which is a PblObj.*)
1463 fun par_children (Nd (PblObj _, children)) [] = (children, [])
1464 | par_children (pt as Nd (PblObj _, children)) p =
1465 let fun par [] = (children, [])
1466 | par p = let val Nd (obj, children) = get_nd pt p
1467 in if is_pblobj obj then (children, p) else par (lev_up p)
1469 in par (lev_up p) end;
1471 (*.get the children of a node in ctree.*)
1472 fun children (Nd (PblObj _, cn)) = cn
1473 | children (Nd (PrfObj _, cn)) = cn;
1476 (*.find the next parent, which is either a PblObj (return true)
1477 or a PrfObj with tac = Detail_Set (return false).*)
1478 (*FIXME.3.4.03:re-organize par_pbl_det after rls' --> rls*)
1479 fun par_pbl_det pt [] = (true, [], Erls)
1480 | par_pbl_det pt p =
1481 let fun par pt [] = (true, [], Erls)
1482 | par pt p = if is_pblobj (get_obj I pt p) then (true, p, Erls)
1483 else case get_obj g_tac pt p of
1484 (*Detail_Set rls' => (false, p, assoc_rls rls')
1485 (*^^^--- before 040206 after ---vvv*)
1486 |*)Rewrite_Set rls' => (false, p, assoc_rls rls')
1487 | Rewrite_Set_Inst (_, rls') =>
1488 (false, p, assoc_rls rls')
1489 | _ => par pt (lev_up p)
1490 in par pt (lev_up p) end;
1495 (*.get from the whole ctree by f : ppobj -> 'a.*)
1496 fun get_all f EmptyPtree = []
1497 | get_all f (Nd (b, [])) = [f b]
1498 | get_all f (Nd (b, bs)) = [f b] @ (get_alls f bs)
1499 and get_alls f [] = []
1500 | get_alls f pts = flat (map (get_all f) pts);
1503 (*.insert obj b into ctree at pos, ev.overwriting this pos.
1504 covers library.ML TODO.WN110315 rename*)
1505 fun insert_pt b EmptyPtree [] = Nd (b, [])
1506 | insert_pt b EmptyPtree _ = raise PTREE "insert_pt b Empty _"
1507 | insert_pt b (Nd ( _, _)) [] = raise PTREE "insert_pt b _ []"
1508 | insert_pt b (Nd (b', bs)) (p::[]) =
1509 Nd (b', repl_app bs p (Nd (b,[])))
1510 | insert_pt b (Nd (b', bs)) (p::ps) =
1511 Nd (b', repl_app bs p (insert_pt b (nth p bs) ps));
1513 > type ppobj = string;
1514 > tracing (pr_ctree prfn (!pt));
1515 (*val pt = Unsynchronized.ref Empty;*)
1516 pt:= insert_pt ("root'":ppobj) EmptyPtree [];
1517 pt:= insert_pt ("xx1":ppobj) (!pt) [1];
1518 pt:= insert_pt ("xx2":ppobj) (!pt) [2];
1519 pt:= insert_pt ("xx3":ppobj) (!pt) [3];
1520 pt:= insert_pt ("xx2.1":ppobj) (!pt) [2,1];
1521 pt:= insert_pt ("xx2.2":ppobj) (!pt) [2,2];
1522 pt:= insert_pt ("xx2.1.1":ppobj) (!pt) [2,1,1];
1523 pt:= insert_pt ("xx2.1.2":ppobj) (!pt) [2,1,2];
1524 pt:= insert_pt ("xx2.1.3":ppobj) (!pt) [2,1,3];
1527 (*.insert children to a node without children.*)
1528 (*compare: fun insert_pt*)
1529 fun ins_chn _ EmptyPtree _ = raise PTREE "ins_chn: EmptyPtree"
1530 | ins_chn ns (Nd _) [] = raise PTREE "ins_chn: pos = []"
1531 | ins_chn ns (Nd (b, bs)) (p::[]) =
1532 if p > length bs then raise PTREE "ins_chn: pos not existent"
1533 else let val Nd (b', bs') = nth p bs
1534 in if null bs' then Nd (b, repl_app bs p (Nd (b', ns)))
1535 else raise PTREE "ins_chn: pos mustNOT be overwritten" end
1536 | ins_chn ns (Nd (b, bs)) (p::ps) =
1537 Nd (b, repl_app bs p (ins_chn ns (nth p bs) ps));
1539 (* print_depth 11;ins_chn;print_depth 3; ###insert_pt#########################*);
1542 (** apply f to obj at pos, f: ppobj -> ppobj **)
1544 fun appl_to_node f (Nd (b,bs)) = Nd (f b, bs);
1545 fun appl_obj f EmptyPtree [] = EmptyPtree
1546 | appl_obj f EmptyPtree _ = raise PTREE "appl_obj f Empty _"
1547 | appl_obj f (Nd (b, bs)) [] = Nd (f b, bs)
1548 | appl_obj f (Nd (b, bs)) (p::[]) =
1549 Nd (b, repl_app bs p (((appl_to_node f) o (nth p)) bs))
1550 | appl_obj f (Nd (b, bs)) (p::ps) =
1551 Nd (b, repl_app bs p (appl_obj f (nth p bs) (ps:pos)));
1553 (* for use by appl_obj *)
1554 fun repl_form f (PrfObj {cell=c,form= _,tac=tac,loc=loc,
1555 branch=branch,result=result,ostate=ostate}) =
1556 PrfObj {cell=c,form= f,tac=tac,loc=loc,
1557 branch=branch,result=result,ostate=ostate}
1558 | repl_form _ _ = raise PTREE "repl_form takes no PblObj";
1559 fun repl_pbl x (PblObj {cell=cell,origin=origin,fmz=fmz,
1560 spec=spec,probl=_,meth=meth,ctxt=ctxt,env=env,loc=loc,
1561 branch=branch,result=result,ostate=ostate}) =
1562 PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl= x,
1563 meth=meth,ctxt=ctxt,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
1564 | repl_pbl _ _ = raise PTREE "repl_pbl takes no PrfObj";
1565 fun repl_met x (PblObj {cell=cell,origin=origin,fmz=fmz,
1566 spec=spec,probl=probl,meth=_,ctxt=ctxt,env=env,loc=loc,
1567 branch=branch,result=result,ostate=ostate}) =
1568 PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,
1569 meth= x,ctxt=ctxt,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
1570 | repl_met _ _ = raise PTREE "repl_pbl takes no PrfObj";
1572 fun repl_spec x (PblObj {cell=cell,origin=origin,fmz=fmz,
1573 spec= _,probl=probl,meth=meth,ctxt=ctxt,env=env,loc=loc,
1574 branch=branch,result=result,ostate=ostate}) =
1575 PblObj {cell=cell,origin=origin,fmz=fmz,spec= x,probl=probl,
1576 meth=meth,ctxt=ctxt,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
1577 | repl_spec _ _ = raise PTREE "repl_domID takes no PrfObj";
1578 fun repl_domID x (PblObj {cell=cell,origin=origin,fmz=fmz,
1579 spec=(_,p,m),probl=probl,meth=meth,ctxt=ctxt,env=env,loc=loc,
1580 branch=branch,result=result,ostate=ostate}) =
1581 PblObj {cell=cell,origin=origin,fmz=fmz,spec=(x,p,m),probl=probl,
1582 meth=meth,ctxt=ctxt,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
1583 | repl_domID _ _ = raise PTREE "repl_domID takes no PrfObj";
1584 fun repl_pblID x (PblObj {cell=cell,origin=origin,fmz=fmz,
1585 spec=(d,_,m),probl=probl,meth=meth,ctxt=ctxt,env=env,loc=loc,
1586 branch=branch,result=result,ostate=ostate}) =
1587 PblObj {cell=cell,origin=origin,fmz=fmz,spec=(d,x,m),probl=probl,
1588 meth=meth,ctxt=ctxt,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
1589 | repl_pblID _ _ = raise PTREE "repl_pblID takes no PrfObj";
1590 fun repl_metID x (PblObj {cell=cell,origin=origin,fmz=fmz,
1591 spec=(d,p,_),probl=probl,meth=meth,ctxt=ctxt,env=env,loc=loc,
1592 branch=branch,result=result,ostate=ostate}) =
1593 PblObj {cell=cell,origin=origin,fmz=fmz,spec=(d,p,x),probl=probl,
1594 meth=meth,ctxt=ctxt,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
1595 | repl_metID _ _ = raise PTREE "repl_metID takes no PrfObj";
1597 fun repl_result l f' s (PrfObj {cell=cell,form=form,tac=tac,loc=_,
1598 branch=branch,result = _ ,ostate = _}) =
1599 PrfObj {cell=cell,form=form,tac=tac,loc= l,
1600 branch=branch,result = f',ostate = s}
1601 | repl_result l f' s (PblObj {cell=cell,origin=origin,fmz=fmz,
1602 spec=spec,probl=probl,meth=meth,ctxt=ctxt,env=env,loc=_,
1603 branch=branch,result= _ ,ostate= _}) =
1604 PblObj {cell=cell,origin=origin,fmz=fmz,
1605 spec=spec,probl=probl,meth=meth,ctxt=ctxt,env=env,loc= l,
1606 branch=branch,result= f',ostate= s};
1608 fun repl_tac x (PrfObj {cell=cell,form=form,tac= _,loc=loc,
1609 branch=branch,result=result,ostate=ostate}) =
1610 PrfObj {cell=cell,form=form,tac= x,loc=loc,
1611 branch=branch,result=result,ostate=ostate}
1612 | repl_tac _ _ = raise PTREE "repl_tac takes no PblObj";
1614 fun repl_branch b (PblObj {cell=cell,origin=origin,fmz=fmz,
1615 spec=spec,probl=probl,meth=meth,ctxt=ctxt,env=env,loc=loc,
1616 branch= _,result=result,ostate=ostate}) =
1617 PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,
1618 meth=meth,ctxt=ctxt,env=env,loc=loc,branch= b,result=result,ostate=ostate}
1619 | repl_branch b (PrfObj {cell=cell,form=form,tac=tac,loc=loc,
1620 branch= _,result=result,ostate=ostate}) =
1621 PrfObj {cell=cell,form=form,tac=tac,loc=loc,
1622 branch= b,result=result,ostate=ostate};
1625 (PblObj {cell, origin, fmz, spec, probl, meth,
1626 ctxt=_, env, loc, branch, result, ostate}) =
1627 PblObj {cell=cell, origin=origin, fmz=fmz, spec=spec, probl=probl, meth=meth,
1628 ctxt=x, env=env, loc=loc, branch=branch, result=result, ostate=ostate}
1629 | repl_ctxt _ _ = raise PTREE "repl_env takes no PrfObj";
1632 (PblObj {cell=cell, origin=origin, fmz=fmz, spec=spec, probl=probl, meth=meth,
1633 ctxt=ctxt, env=_, loc=loc, branch=branch, result=result, ostate=ostate}) =
1634 PblObj {cell=cell, origin=origin, fmz=fmz, spec=spec, probl=probl, meth=meth,
1635 ctxt=ctxt, env=e, loc=loc, branch=branch, result=result, ostate=ostate}
1636 | repl_env _ _ = raise PTREE "repl_env takes no PrfObj";
1639 (PblObj {cell=cell,origin=(_,spe,hdf),fmz=fmz,
1640 spec=spec,probl=probl,meth=meth,ctxt=ctxt,env=env,loc=loc,
1641 branch=branch,result=result,ostate=ostate}) =
1642 PblObj{cell=cell,origin=(oris,spe,hdf),fmz=fmz,spec=spec,probl=probl,
1643 meth=meth,ctxt=ctxt,env=env,loc=loc,branch=branch,
1644 result=result,ostate=ostate}
1645 | repl_oris _ _ = raise PTREE "repl_oris takes no PrfObj";
1646 fun repl_orispec spe
1647 (PblObj {cell=cell,origin=(oris,_,hdf),fmz=fmz,
1648 spec=spec,probl=probl,meth=meth,ctxt=ctxt,env=env,loc=loc,
1649 branch=branch,result=result,ostate=ostate}) =
1650 PblObj{cell=cell,origin=(oris,spe,hdf),fmz=fmz,spec=spec,probl=probl,
1651 meth=meth,ctxt=ctxt,env=env,loc=loc,branch=branch,
1652 result=result,ostate=ostate}
1653 | repl_orispec _ _ = raise PTREE "repl_orispec takes no PrfObj";
1655 fun repl_loc l (PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,meth=meth,
1656 ctxt=ctxt,env=env,loc=_,branch=branch,result=result,ostate=ostate}) =
1657 PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,meth=meth,
1658 ctxt=ctxt,env=env,loc=l,branch=branch,result=result,ostate=ostate}
1659 | repl_loc l (PrfObj {cell=cell,form=form,tac=tac,
1660 loc=_,branch=branch,result=result,ostate=ostate}) =
1661 PrfObj {cell=cell,form=form,tac=tac,
1662 loc= l,branch=branch,result=result,ostate=ostate};
1664 (*WN050219 put here for interpreting code for cut_tree below...*)
1666 bool * (*ALL itms+preconds true*)
1667 pos_ * (*model belongs to Problem | Method*)
1668 term * (*header: Problem... or Cas
1669 FIXXXME.12.03: item! for marking syntaxerrors*)
1670 itm list * (*model: given, find, relate*)
1671 ((bool * term) list) *(*model: preconds*)
1672 spec; (*specification*)
1673 val e_ocalhd = (false, Und, e_term, [e_itm], [(false, e_term)], e_spec);
1675 datatype ptform = Form of term | ModSpec of ocalhd;
1676 val e_ptform = Form e_term;
1677 val e_ptform' = ModSpec e_ocalhd;
1679 (*.applies (snd f) to the branches at a pos if ((fst f) b),
1680 f : (ppobj -> bool) * (int -> ctree list -> ctree list).*)
1682 fun appl_branch f EmptyPtree [] = (EmptyPtree, false)
1683 | appl_branch f EmptyPtree _ = raise PTREE "appl_branch f Empty _"
1684 | appl_branch f (Nd ( _, _)) [] = raise PTREE "appl_branch f _ []"
1685 | appl_branch f (Nd (b, bs)) (p::[]) =
1686 if (fst f) b then (Nd (b, (snd f) p bs), true)
1687 else (Nd (b, bs), false)
1688 | appl_branch f (Nd (b, bs)) (p::ps) =
1689 let val (b',bool) = appl_branch f (nth p bs) ps
1690 in (Nd (b, repl_app bs p b'), bool) end;
1692 (* for cut_level; appl_branch(deprecated) *)
1693 fun test_trans (PrfObj{branch = Transitive,...}) = true
1694 | test_trans (PblObj{branch = Transitive,...}) = true
1695 | test_trans _ = false;
1697 fun is_pblobj' pt p =
1698 let val ppobj = get_obj I pt p
1699 in is_pblobj ppobj end;
1701 fun delete_result pt p =
1702 (appl_obj (repl_result (fst (get_obj g_loc pt p), NONE)
1703 (e_term,[]) Incomplete) pt p);
1705 fun del_res (PblObj {cell, fmz, origin, spec, probl, meth,
1706 ctxt, env, loc=(l1,_), branch, result, ostate}) =
1707 PblObj {cell=cell,fmz=fmz,origin=origin,spec=spec,probl=probl,meth=meth,
1708 ctxt=ctxt,env=env, loc=(l1,NONE), branch=branch, result=(e_term,[]),
1711 | del_res (PrfObj {cell, form, tac, loc=(l1,_), branch, result, ostate}) =
1712 PrfObj {cell=cell,form=form,tac=tac, loc=(l1,NONE), branch=branch,
1713 result=(e_term,[]), ostate=Incomplete};
1715 (*FIXME.WN0312 update_X X pos pt -> pt could be chained by o (efficiency?)*)
1716 (*fun update_fmz pt pos x = appl_obj (repl_fmz x) pt pos; WN01xx *)
1717 fun update_ctxt pt pos x = appl_obj (repl_ctxt x) pt pos; (*for use on PblObj,
1718 otherwise use fun generate1; compare fun get_ctxt*)
1719 fun update_env pt pos x = appl_obj (repl_env x) pt pos;
1720 fun update_domID pt pos x = appl_obj (repl_domID x) pt pos;
1721 fun update_pblID pt pos x = appl_obj (repl_pblID x) pt pos;
1722 fun update_metID pt pos x = appl_obj (repl_metID x) pt pos;
1723 fun update_spec pt pos x = appl_obj (repl_spec x) pt pos;
1724 fun update_pbl pt pos x = appl_obj (repl_pbl x) pt pos;
1725 fun update_pblppc pt pos x = appl_obj (repl_pbl x) pt pos;
1726 fun update_met pt pos x = appl_obj (repl_met x) pt pos;
1727 fun update_metppc pt pos x = appl_obj (repl_met x) pt pos;
1728 fun update_branch pt pos x = appl_obj (repl_branch x) pt pos;
1729 fun update_tac pt pos x = appl_obj (repl_tac x) pt pos;
1730 fun update_oris pt pos x = appl_obj (repl_oris x) pt pos;
1731 fun update_orispec pt pos x = appl_obj (repl_orispec x) pt pos;
1733 (*WN050305 for handling cut_tree in cappend_atomic + for testing*)
1734 fun update_loc' pt pos x = appl_obj (repl_loc x) pt pos;
1736 (*13.8.02: options, because istate is no equalitype any more*)
1737 fun get_loc EmptyPtree _ = (e_istate, e_ctxt)
1738 | get_loc pt (p,Res) =
1739 (case get_obj g_loc pt p of
1741 | (NONE , NONE) => (e_istate, e_ctxt)
1742 | (_ , SOME i) => i)
1743 | get_loc pt (p,_) =
1744 (case get_obj g_loc pt p of
1745 (NONE , SOME i) => i (*13.8.02 just copied from ^^^: too liberal ?*)
1746 | (NONE , NONE) => (e_istate, e_ctxt)
1747 | (SOME i, _) => i);
1748 fun get_istate pt p = get_loc pt p |> #1;
1749 fun get_ctxt pt (pos as (p, p_)) =
1750 if member op = [Frm, Res] p_
1751 then get_loc pt pos |> #2 (*for script interpretation rely on fun get_loc*)
1752 else get_obj g_ctxt pt p (*for specify phase take ctx from PblObj*)
1754 fun get_assumptions_ pt p = get_ctxt pt p |> get_assumptions;
1756 (*pos of the formula on FE relative to the current pos,
1757 which is the next writepos*)
1760 let val (ps,p) = split_last pp
1761 in case p of 1 => ps | n => ps @ [n-1] end;
1763 (*WN.20.5.03 ... but not used*)
1764 fun posless [] (_::_) = true
1765 | posless (_::_) [] = false
1766 | posless (p::ps) (q::qs) = if p = q then posless ps qs else p < q;
1767 (* posless [2,3,4] [3,4,5];
1769 > posless [2,3,4] [1,2,3];
1771 > posless [2,3] [2,3,4];
1773 > posless [2,3,4] [2,3];
1775 > posless [6] [6,5,2];
1777 +++ see Isabelle/../library.ML*)
1780 (**.development for extracting an 'interval' from ctree.**)
1782 (*WN0510 version stopped in favour of get_interval with !!!move_dn, getFormulaeFromTo
1783 actually used (inefficient) version with move_dn: see modspec.sml*)
1786 fun hdp [] = 1 | hdp [0] = 1 | hdp x = hd x;(*start with first*)
1787 fun hdq [] = 99999 | hdq [0] = 99999 | hdq x = hd x;(*take until last*)
1788 fun tlp [] = [0] | tlp [_] = [0] | tlp x = tl x;
1789 fun tlq [] = [99999] | tlq [_] = [99999] | tlq x = tl x;
1791 fun getnd i (b,p) q (Nd (po, nds)) =
1792 (if i <= 0 then [[b]] else []) @
1793 (getnds (i-1) true (b@[hdp p], tlp p) (tlq q)
1794 (take_fromto (hdp p) (hdq q) nds))
1796 and getnds _ _ _ _ [] = [] (*no children*)
1797 | getnds i _ (b,p) q [nd] = (getnd i (b,p) q nd) (*l+r-margin*)
1799 | getnds i true (b,p) q [n1, n2] = (*l-margin, r-margin*)
1800 (getnd i ( b, p ) [99999] n1) @
1801 (getnd ~99999 (lev_on b,[0]) q n2)
1803 | getnds i _ (b,p) q [n1, n2] = (*intern, r-margin*)
1804 (getnd i ( b,[0]) [99999] n1) @
1805 (getnd ~99999 (lev_on b,[0]) q n2)
1807 | getnds i true (b,p) q (nd::(nds as _::_)) = (*l-margin, intern*)
1808 (getnd i ( b, p ) [99999] nd) @
1809 (getnds ~99999 false (lev_on b,[0]) q nds)
1811 | getnds i _ (b,p) q (nd::(nds as _::_)) = (*intern, ...*)
1812 (getnd i ( b,[0]) [99999] nd) @
1813 (getnds ~99999 false (lev_on b,[0]) q nds);
1815 (*get an 'interval from to' from a ctree as 'intervals f t' of respective nodes
1816 where 'from' are pos, i.e. a key as int list, 'f' an int (to,t analoguous)
1817 (1) the 'f' are given
1818 (1a) by 'from' if 'f' = the respective element of 'from' (left margin)
1819 (1b) -inifinity, if 'f' > the respective element of 'from' (internal node)
1820 (2) the 't' ar given
1821 (2a) by 'to' if 't' = the respective element of 'to' (right margin)
1822 (2b) inifinity, if 't' < the respective element of 'to (internal node)'
1823 the 'f' and 't' are set by hdp,... *)
1824 fun get_trace pt p q =
1825 (flat o (getnds ((length p) -1) true ([hdp p], tlp p) (tlq q)))
1826 (take_fromto (hdp p) (hdq q) (children pt));
1829 fun get_somespec (dI,pI,mI) (dI',pI',mI') =
1830 let val domID = if dI = e_domID
1831 then if dI' = e_domID
1832 then error"pt_extract: no domID in probl,origin"
1835 val pblID = if pI = e_pblID
1836 then if pI' = e_pblID
1837 then error"pt_extract: no pblID in probl,origin"
1840 val metID = if mI = e_metID
1841 then if pI' = e_metID
1842 then error"pt_extract: no metID in probl,origin"
1845 in (domID, pblID, metID) end;
1846 fun get_somespec' (dI,pI,mI) (dI',pI',mI') =
1847 let val domID = if dI = e_domID then dI' else dI
1848 val pblID = if pI = e_pblID then pI' else pI
1849 val metID = if mI = e_metID then mI' else mI
1850 in (domID, pblID, metID) end;
1852 (*extract a formula or model from ctree for itms2itemppc or model2xml*)
1853 fun preconds2str bts =
1854 (strs2str o (map (linefeed o pair2str o
1856 (apfst bool2str)))) bts;
1857 fun ocalhd2str (b, p, hdf, itms, prec, spec) =
1858 "("^bool2str b^", "^pos_2str p^", "^term2str hdf^
1859 ", "^itms2str_ (thy2ctxt' "Isac") itms^
1860 ", "^preconds2str prec^", \n"^spec2str spec^" )";
1864 fun is_pblnd (Nd (ppobj, _)) = is_pblobj ppobj;
1867 (**.functions for the 'ctree iterator' as seen from the FE-Kernel interface.**)
1869 (*move one step down into existing nodes of ctree; regard TransitiveB
1870 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~##################
1871 fun move_dn _ (Nd (c, ns)) ([],p_) = (*root problem*)
1872 (* val (Nd (c, ns), ([],p_)) = (pt, get_pos cI uI);
1875 then case p_ of (*Frm => ([], Pbl) 1.12.03
1876 |*) Res => raise PTREE "move_dn: end of calculation"
1877 | _ => if null ns (*go down from Pbl + Met*)
1878 then raise PTREE "move_dn: solve problem not started"
1880 else (case p_ of Res => raise PTREE "move_dn: end of (sub-)tree"
1882 then raise PTREE "move_dn: pos not existent 1"
1885 (*iterate towards end of pos*)
1886 (* val (P,(Nd (_, ns)),(p::(ps as (_::_)),p_)) = ([]:pos, pt, get_pos cI uI);
1887 val (P,(Nd (_, ns)),(p::(ps as (_::_)),p_)) = ((P@[p]),(nth p ns),(ps, p_));
1889 | move_dn P (Nd (_, ns)) (p::(ps as (_::_)),p_) =
1890 if p > length ns then raise PTREE "move_dn: pos not existent 2"
1891 else move_dn ((P@[p]): pos) (nth p ns) (ps, p_)
1892 (* val (P, (Nd (c, ns)), ([p], p_)) = ((P@[p]), (nth p ns), (ps, p_));
1893 val (P, (Nd (c, ns)), ([p], p_)) = ([],pt,get_pos cI uI);
1895 | move_dn P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*)
1896 if p > length ns then raise PTREE "move_dn: pos not existent 3"
1897 else if is_pblnd (nth p ns) then
1898 ((*tracing("### move_dn: is_pblnd (nth p ns), P= "^ints2str' P^", \n"^
1899 "length ns= "^((string_of_int o length) ns)^
1900 ", p= "^string_of_int p^", p_= "^pos_2str p_);*)
1901 case p_ of Res => if p = length ns
1902 then if g_ostate c = Complete then (P, Res)
1903 else raise PTREE (ints2str' P^" not complete")
1904 (*FIXME here handle not-sequent-branches*)
1905 else if g_branch c = TransitiveB
1906 andalso (not o is_pblnd o (nth (p+1))) ns
1908 else (P@[p+1], if is_pblnd (nth (p+1) ns)
1910 | _ => if (null o children o (nth p)) ns (*go down from Pbl*)
1911 then raise PTREE "move_dn: solve subproblem not started"
1913 if (is_pblnd o hd o children o (nth p)) ns
1916 (* val (P, Nd (c, ns), ([p], p_)) = ([], pt, ([1], Frm));
1918 else case p_ of Frm => if (null o children o (nth p)) ns
1919 (*then if g_ostate c = Complete then (P@[p],Res)*)
1920 then if g_ostate' (nth p ns) = Complete
1922 else raise PTREE "move_dn: pos not existent 4"
1923 else (P @ [p, 1], (*go down*)
1924 if (is_pblnd o hd o children o (nth p)) ns
1926 | Res => if p = length ns
1928 if g_ostate c = Complete then (P, Res)
1929 else raise PTREE (ints2str' P^" not complete")
1931 if g_branch c = TransitiveB
1932 andalso (not o is_pblnd o (nth (p+1))) ns
1933 then if (null o children o (nth (p+1))) ns
1935 else (P@[p+1,1], Frm)(*040221*)
1936 else (P@[p+1], if is_pblnd (nth (p+1) ns)
1939 (*.move one step down into existing nodes of ctree; skip Res = Frm.nxt;
1940 move_dn at the end of the calc-tree raises PTREE.*)
1941 fun move_dn _ (Nd (c, ns)) ([],p_) = (*root problem*)
1943 Res => raise PTREE "move_dn: end of calculation"
1944 | _ => if null ns (*go down from Pbl + Met*)
1945 then raise PTREE "move_dn: solve problem not started"
1947 | move_dn P (Nd (_, ns)) (p::(ps as (_::_)),p_) =(*iterate to end of pos*)
1948 if p > length ns then raise PTREE "move_dn: pos not existent 2"
1949 else move_dn (P@[p]) (nth p ns) (ps, p_)
1951 | move_dn P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*)
1952 if p > length ns then raise PTREE "move_dn: pos not existent 3"
1955 if p = length ns (*last Res on this level: go a level up*)
1956 then if g_ostate c = Complete then (P, Res)
1957 else raise PTREE (ints2str' P^" not complete 1")
1958 else (*go to the next Nd on this level, or down into the next Nd*)
1959 if is_pblnd (nth (p+1) ns) then (P@[p+1], Pbl)
1961 if g_res' (nth p ns) = g_form' (nth (p+1) ns)
1962 then if (null o children o (nth (p+1))) ns
1963 then (*take the Res if Complete*)
1964 if g_ostate' (nth (p+1) ns) = Complete
1966 else raise PTREE (ints2str' (P@[p+1])^
1968 else (P@[p+1,1], Frm)(*go down into the next PrfObj*)
1969 else (P@[p+1], Frm)(*take Frm: exists if the Nd exists*)
1970 | Frm => (*go down or to the Res of this Nd*)
1971 if (null o children o (nth p)) ns
1972 then if g_ostate' (nth p ns) = Complete then (P @ [p], Res)
1973 else raise PTREE (ints2str' (P @ [p])^" not complete 3")
1974 else (P @ [p, 1], Frm)
1975 | _ => (*is Pbl or Met*)
1976 if (null o children o (nth p)) ns
1977 then raise PTREE "move_dn:solve subproblem not startd"
1979 if (is_pblnd o hd o children o (nth p)) ns
1983 (*.go one level down into ctree.*)
1984 fun movelevel_dn [] (Nd (c, ns)) ([],p_) = (*root problem*)
1987 then raise PTREE "solve problem not started"
1988 else ([1], if (is_pblnd o hd) ns then Pbl else Frm)
1989 else raise PTREE "pos not existent 1"
1991 (*iterate towards end of pos*)
1992 | movelevel_dn P (Nd (_, ns)) (p::(ps as (_::_)),p_) =
1993 if p > length ns then raise PTREE "pos not existent 2"
1994 else movelevel_dn (P@[p]) (nth p ns) (ps, p_)
1996 | movelevel_dn P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*)
1997 if p > length ns then raise PTREE "pos not existent 3" else
2000 then raise PTREE "no children"
2002 if g_branch c = TransitiveB
2003 then if (null o children o (nth (p+1))) ns
2004 then raise PTREE "no children"
2006 if (is_pblnd o hd o children o (nth (p+1))) ns
2008 else if (null o children o (nth p)) ns
2009 then raise PTREE "no children"
2010 else (P @ [p, 1], if (is_pblnd o hd o children o (nth p)) ns
2012 | _ => if (null o children o (nth p)) ns
2013 then raise PTREE "no children"
2014 else (P @ [p, 1], (*go down*)
2015 if (is_pblnd o hd o children o (nth p)) ns
2020 (*.go to the previous position in ctree; regard TransitiveB.*)
2021 fun move_up _ (Nd (c, ns)) ([],p_) = (*root problem*)
2023 then case p_ of Res => if null ns then ([], Pbl) (*Res -> Pbl (not Met)!*)
2024 else ([length ns], Res)
2025 | _ => raise PTREE "begin of calculation"
2026 else raise PTREE "pos not existent"
2028 | move_up P (Nd (_, ns)) (p::(ps as (_::_)),p_) = (*iterate to end of pos*)
2029 if p > length ns then raise PTREE "pos not existent"
2030 else move_up (P@[p]) (nth p ns) (ps,p_)
2032 | move_up P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*)
2033 if p > length ns then raise PTREE "pos not existent"
2034 else if is_pblnd (nth p ns) then
2036 let val nc = (length o children o (nth p)) ns
2037 in if nc = 0 then (P@[p], Pbl) (*Res -> Pbl (not Met)!*)
2038 else (P @ [p, nc], Res) end (*go down*)
2039 | _ => if p = 1 then (P, Pbl) else (P@[p-1], Res)
2040 else case p_ of Frm => if p <> 1 then (P, Frm)
2041 else if is_pblobj c then (P, Pbl) else (P, Frm)
2043 let val nc = (length o children o (nth p)) ns
2044 in if nc = 0 (*cannot go down*)
2045 then if g_branch c = TransitiveB andalso p <> 1
2046 then (P@[p-1], Res) else (P@[p], Frm)
2047 else (P @ [p, nc], Res) end; (*go down*)
2051 (*.go one level up in ctree; sets the position on Frm.*)
2052 fun movelevel_up _ (Nd (c, ns)) (([],p_):pos') = (*root problem*)
2053 raise PTREE "pos not existent"
2055 (*iterate towards end of pos*)
2056 | movelevel_up P (Nd (_, ns)) (p::(ps as (_::_)),p_) =
2057 if p > length ns then raise PTREE "pos not existent"
2058 else movelevel_up (P@[p]) (nth p ns) (ps,p_)
2060 | movelevel_up P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*)
2061 if p > length ns then raise PTREE "pos not existent"
2062 else if is_pblobj c then (P, Pbl) else (P, Frm);
2065 (*.go to the next calc-head up in the calc-tree.*)
2066 fun movecalchd_up pt ((p, Res):pos') =
2067 (par_pblobj pt p, Pbl):pos'
2068 | movecalchd_up pt (p, _) =
2069 if is_pblobj (get_obj I pt p)
2070 then (p, Pbl) else (par_pblobj pt p, Pbl);
2072 (*.determine the previous pos' on the same level.*)
2073 (*WN0502 made for interSteps; _only_ works for branch TransitiveB WN120517 compare lev_back*)
2074 fun lev_pred' pt (pos:pos' as ([],Res)) = ([],Pbl):pos'
2075 | lev_pred' pt (pos:pos' as (p, Res)) =
2076 let val (p', last) = split_last p
2078 then if (is_pblobj o (get_obj I pt)) p then (p,Pbl) else (p, Frm)
2079 else if get_obj g_res pt (p' @ [last - 1]) = get_obj g_form pt p
2080 then (p' @ [last - 1], Res) (*TransitiveB*)
2081 else if (is_pblobj o (get_obj I pt)) p then (p,Pbl) else (p, Frm)
2085 (*.determine the next pos' on the same level.*)
2086 fun lev_on' pt (([],Pbl):pos') = ([],Res):pos'
2087 | lev_on' pt (p, Res) =
2088 if get_obj g_res pt p = get_obj g_form pt (lev_on p)(*TransitiveB*)
2089 then if existpt' (lev_on p, Res) pt then (lev_on p, Res)
2090 else error ("lev_on': (p, Res) -> (p, Res) not existent, \
2091 \p = "^ints2str' (lev_on p))
2092 else (lev_on p, Frm)
2093 | lev_on' pt (p, _) =
2094 if existpt' (p, Res) pt then (p, Res)
2095 else error ("lev_on': (p, Frm) -> (p, Res) not existent, \
2096 \p = "^ints2str' p);
2098 fun exist_lev_on' pt p = (lev_on' pt p; true) handle _ => false;
2100 (*.is the pos' at the last element of a calulation _AND_ can be continued.*)
2101 (* val (pt, pos as (p,p_)) = (pt, ([1],Frm));
2103 fun is_curr_endof_calc pt (([],Res) : pos') = false
2104 | is_curr_endof_calc pt (pos as (p,_)) =
2105 not (exist_lev_on' pt pos)
2106 andalso get_obj g_ostate pt (lev_up p) = Incomplete;
2109 (**.insert into ctree and cut branches accordingly.**)
2111 (*.get all positions of certain intervals on the ctree.*)
2112 (*OLD VERSION without move_dn; kept for occasional redesign
2113 get all pos's to be cut in a ctree
2114 below a pos or from a ctree list after i-th element (NO level_up).*)
2115 fun get_allpos' (_:pos, _:posel) EmptyPtree = ([]:pos' list)
2116 | get_allpos' (p, 1) (Nd (b, bs)) = (*p is pos of Nd*)
2117 if g_ostate b = Incomplete
2118 then ((*tracing("get_allpos' (p, 1) Incomplete: p="^ints2str' p);*)
2119 [(p,Frm)] @ (get_allpos's (p, 1) bs)
2121 else ((*tracing("get_allpos' (p, 1) else: p="^ints2str' p);*)
2122 [(p,Frm)] @ (get_allpos's (p, 1) bs) @ [(p,Res)]
2124 (*WN041020 here we assume what is presented on the worksheet ?!*)
2125 | get_allpos' (p, i) (Nd (b, bs)) = (*p is pos of Nd*)
2126 if length bs > 0 orelse is_pblobj b
2127 then if g_ostate b = Incomplete
2128 then [(p,Frm)] @ (get_allpos's (p, 1) bs)
2129 else [(p,Frm)] @ (get_allpos's (p, 1) bs) @ [(p,Res)]
2131 if g_ostate b = Incomplete
2134 (*WN041020 here we assume what is presented on the worksheet ?!*)
2135 and get_allpos's _ [] = []
2136 | get_allpos's (p, i) (pt::pts) = (*p is pos of parent-Nd*)
2137 (get_allpos' (p@[i], i) pt) @ (get_allpos's (p, i+1) pts);
2139 (*.get all positions of certain intervals on the ctree.*)
2140 (*NEW version WN050225*)
2144 (*before WN041019......
2145 val cut_branch = (test_trans, curry take):
2146 (ppobj -> bool) * (int -> ctree list -> ctree list);
2147 .. formlery used for ...
2148 fun cut_tree''' _ [] = EmptyPtree
2149 | cut_tree''' pt pos =
2150 let val (pt',cut) = appl_branch cut_branch pt pos
2151 in if cut andalso length pos > 1 then cut_tree''' pt' (lev_up pos)
2154 (*OLD version before WN050225*)
2155 (*WN050106 like cut_level, but deletes exactly 1 node --- for tests ONLY*)
2156 fun cut_level_'_ (_:pos' list) (_:pos) EmptyPtree (_:pos') =
2157 raise PTREE "cut_level_'_ Empty _"
2158 | cut_level_'_ _ _ (Nd ( _, _)) ([],_) = raise PTREE "cut_level_'_ _ []"
2159 | cut_level_'_ cuts P (Nd (b, bs)) (p::[],p_) =
2161 then (Nd (b, drop_nth [] (p:posel, bs)),
2164 (if p_ = Frm then [(P@[p],Res)] else ([]:pos' list)) @
2165 (*WN041020 here we assume what is presented on the worksheet ?!*)
2166 (get_allpos's (P, p+1) (drop_nth [] (p, bs))))
2168 else (Nd (b, bs), cuts)
2169 | cut_level_'_ cuts P (Nd (b, bs)) ((p::ps),p_) =
2170 let val (bs',cuts') = cut_level_'_ cuts P (nth p bs) (ps, p_)
2171 in (Nd (b, repl_app bs p bs'), cuts @ cuts') end;
2174 fun cut_level (_:pos' list) (_:pos) EmptyPtree (_:pos') =
2175 raise PTREE "cut_level EmptyPtree _"
2176 | cut_level _ _ (Nd ( _, _)) ([],_) = raise PTREE "cut_level _ []"
2178 | cut_level cuts P (Nd (b, bs)) (p::[],p_) =
2180 then (Nd (b, take (p:posel, bs)),
2182 (if p_ = Frm andalso (*#*) g_ostate b = Complete
2183 then [(P@[p],Res)] else ([]:pos' list)) @
2184 (*WN041020 here we assume what is presented on the worksheet ?!*)
2185 (get_allpos's (P, p+1) (takerest (p, bs))))
2186 else (Nd (b, bs), cuts)
2188 | cut_level cuts P (Nd (b, bs)) ((p::ps),p_) =
2189 let val (bs',cuts') = cut_level cuts P (nth p bs) (ps, p_)
2190 in (Nd (b, repl_app bs p bs'), cuts @ cuts') end;
2192 (*OLD version before WN050219, overwritten below*)
2193 fun cut_tree _ (([],_):pos') = raise PTREE "cut_tree _ ([],_)"
2194 | cut_tree pt (pos as ([p],_)) =
2195 let val (pt', cuts) = cut_level ([]:pos' list) [] pt pos
2196 in (pt', cuts @ (if get_obj g_ostate pt [] = Incomplete
2197 then [] else [([],Res)])) end
2198 | cut_tree pt (p,p_) =
2200 fun cutfn pt cuts (p,p_) =
2201 let val (pt', cuts') = cut_level [] (lev_up p) pt (p,p_)
2202 val cuts'' = if get_obj g_ostate pt (lev_up p) = Incomplete
2203 then [] else [(lev_up p, Res)]
2204 in if length cuts' > 0 andalso length p > 1
2205 then cutfn pt' (cuts @ cuts') (lev_up p, Frm(*-->(p,Res)*))
2206 else (pt',cuts @ cuts') end
2207 val (pt', cuts) = cutfn pt [] (p,p_)
2208 in (pt', cuts @ (if get_obj g_ostate pt [] = Incomplete
2209 then [] else [([], Res)])) end;
2212 (*########/ inserted from ctreeNEW.sml \#################################**)
2214 (*.get all positions in a ctree until ([],Res) or ostate=Incomplete
2216 pos' list -> : accumulated, start with []
2217 pos -> : the offset for subtrees wrt the root
2218 ctree -> : (sub)tree
2219 pos' : initialization (the last pos' before ...)
2220 -> pos' list : of positions in this (sub) tree (relative to the root)
2222 (* val (cuts, P, pt, pos) = ([], [3], get_nd pt [3], ([], Frm):pos');
2223 val (cuts, P, pt, pos) = ([], [2], get_nd pt [2], ([], Frm):pos');
2224 length (children pt);
2226 fun get_allp (cuts:pos' list) (P:pos, pos:pos') pt =
2227 (let val nxt = move_dn [] pt pos (*exn if Incomplete reached*)
2228 in if nxt <> ([],Res)
2229 then get_allp (cuts @ [nxt]) (P, nxt) pt
2230 else (map (apfst (curry op@ P)) (cuts @ [nxt])): pos' list
2231 end) handle PTREE _ => (map (apfst (curry op@ P)) cuts);
2234 (*the pts are assumed to be on the same level*)
2235 fun get_allps (cuts: pos' list) (P:pos) [] = cuts
2236 | get_allps cuts P (pt::pts) =
2237 let val below = get_allp [] (P, ([], Frm)) pt
2240 then (P, Pbl)::below
2241 else if last_elem P = 1
2242 then (P, Frm)::below
2243 else (*Trans*) below
2244 val levres = levfrm @ (if null below then [(P, Res)] else [])
2245 in get_allps (cuts @ levres) (lev_on P) pts end;
2248 (**.these 2 funs decide on how far cut_tree goes.**)
2249 (*.shall the nodes _after_ the pos to be inserted at be deleted?.*)
2250 fun test_trans (PrfObj{branch = Transitive,...}) = true
2251 | test_trans (PrfObj{branch = NoBranch,...}) = true
2252 | test_trans (PblObj{branch = Transitive,...}) = true
2253 | test_trans (PblObj{branch = NoBranch,...}) = true
2254 | test_trans _ = false;
2255 (*.shall cutting be continued on the higher level(s)?
2256 the Nd regarded will NOT be changed.*)
2257 fun cutlevup (PblObj _) = false (*for tests of LK0502*)
2258 | cutlevup _ = true;
2259 val cutlevup = test_trans;(*WN060727 after summerterm tests.LK0502 withdrawn*)
2261 (*cut_bottom new sml603..608
2262 cut the level at the bottom of the pos (used by cappend_...)
2263 and handle the parent in order to avoid extra case for root
2264 fn: ctree -> : the _whole_ ctree for cut_levup
2265 pos * posel -> : the pos after split_last
2266 ctree -> : the parent of the Nd to be cut
2268 (ctree * : the updated ctree
2269 pos' list) * : the pos's cut
2270 bool : cutting shall be continued on the higher level(s)
2272 fun cut_bottom _ (pt' as Nd (b, [])) = ((pt', []), cutlevup b)
2273 | cut_bottom (P:pos, p:posel) (Nd (b, bs)) =
2274 let (*divide level into 3 parts...*)
2275 val keep = take (p - 1, bs)
2276 val pt' as Nd (_,bs') = nth p bs
2277 (*^^^^^_here_ will be 'insert_pt'ed by 'append_..'*)
2278 val (tail, tp) = (takerest (p, bs),
2279 if null (takerest (p, bs)) then 0 else p + 1)
2280 val (children, cuts) =
2283 (if is_pblnd pt' then [(P @ [p], Pbl)] else [])
2284 @ (get_allp [] (P @ [p], (P, Frm)) pt')
2285 @ (get_allps [] (P @ [p+1]) tail))
2286 else (keep @ [(*'insert_pt'ed by 'append_..'*)] @ tail,
2287 get_allp [] (P @ [p], (P, Frm)) pt')
2290 then (Nd (del_res b, children),
2291 cuts @ (if g_ostate b = Incomplete then [] else [(P,Res)]))
2292 else (Nd (b, children), cuts)
2293 (*val _= tracing("####cut_bottom (P, p)="^pos2str (P @ [p])^
2294 ", Nd=.............................................")
2296 val _= tracing("####cut_bottom form='"^
2297 term2str (get_obj g_form pt'' []))
2298 val _= tracing("####cut_bottom cuts#="^string_of_int (length cuts)^
2299 ", cuts="^pos's2str cuts)*)
2300 in ((pt'', cuts:pos' list), cutlevup b) end;
2303 (*.go all levels from the bottom of 'pos' up to the root,
2304 on each level compose the children of a node and accumulate the cut Nds
2306 pos' list -> : for accumulation
2307 bool -> : cutting shall be continued on the higher level(s)
2308 ctree -> : the whole ctree for 'get_nd pt P' on each level
2309 ctree -> : the Nd from the lower level for insertion at path
2310 pos * posel -> : pos=path split for convenience
2311 ctree -> : Nd the children of are under consideration on this call
2313 ctree * pos' list : the updated parent-Nd and the pos's of the Nds cut
2315 fun cut_levup (cuts:pos' list) clevup pt pt' (P:pos, p:posel) (Nd (b, bs)) =
2316 let (*divide level into 3 parts...*)
2317 val keep = take (p - 1, bs)
2318 (*val pt' comes as argument from below*)
2319 val (tail, tp) = (takerest (p, bs),
2320 if null (takerest (p, bs)) then 0 else p + 1)
2321 val (children, cuts') =
2323 then (keep @ [pt'], get_allps [] (P @ [p+1]) tail)
2324 else (keep @ [pt'] @ tail, [])
2325 val clevup' = if clevup then cutlevup b else false
2326 (*the first Nd with false stops cutting on all levels above*)
2329 then (Nd (del_res b, children),
2330 cuts' @ (if g_ostate b = Incomplete then [] else [(P,Res)]))
2331 else (Nd (b, children), cuts')
2332 (*val _= tracing("#####cut_levup clevup= "^bool2str clevup)
2333 val _= tracing("#####cut_levup cutlevup b= "^bool2str (cutlevup b))
2334 val _= tracing("#####cut_levup (P, p)="^pos2str (P @ [p])^
2335 ", Nd=.............................................")
2337 val _= tracing("#####cut_levup form='"^
2338 term2str (get_obj g_form pt'' []))
2339 val _= tracing("#####cut_levup cuts#="^string_of_int (length cuts)^
2340 ", cuts="^pos's2str cuts)*)
2341 in if null P then (pt'', (cuts @ cuts'):pos' list)
2342 else let val (P, p) = split_last P
2343 in cut_levup (cuts @ cuts') clevup' pt pt'' (P, p) (get_nd pt P)
2347 (*.cut nodes after and below an inserted node in the ctree;
2348 the cuts range is limited by the predicate 'fun cutlevup'.*)
2349 fun cut_tree pt (pos,_) =
2350 if not (existpt pos pt)
2351 then (pt,[]) (*appending a formula never cuts anything*)
2352 else let val (P, p) = split_last pos
2353 val ((pt', cuts), clevup) = cut_bottom (P, p) (get_nd pt P)
2354 (* pt' is the updated parent of the Nd to cappend_..*)
2355 in if null P then (pt', cuts)
2356 else let val (P, p) = split_last P
2357 in cut_levup cuts clevup pt pt' (P, p) (get_nd pt P)
2361 fun append_atomic p l f r f' s pt =
2362 let (**val _= tracing("#@append_atomic: pos ="^pos2str p)**)
2363 val (iss, f) = if existpt p pt andalso is_empty_tac (get_obj g_tac pt p)
2365 ((fst (get_obj g_loc pt p), SOME l),
2366 get_obj g_form pt p)
2367 else ((NONE, SOME l), f)
2368 in insert_pt (PrfObj {cell = NONE,
2374 ostate= s}) pt p end;
2377 (*20.8.02: cappend_* FIXXXXME cut branches below cannot be decided here:
2378 detail - generate - cappend: inserted, not appended !!!
2380 cut decided in applicable_in !?!
2382 fun cappend_atomic pt p loc f r f' s =
2383 (* val (pt, p, loc, f, r, f', s) =
2384 (pt,p,l,f,Rewrite_Set_Inst (subst2subs subs',id_rls rls'),
2387 ((*tracing("##@cappend_atomic: pos ="^pos2str p);*)
2388 apfst (append_atomic p loc f r f' s) (cut_tree pt (p,Frm))
2390 (*TODO.WN050305 redesign the handling of istates*)
2391 fun cappend_atomic pt p ist_res f r f' s =
2392 if existpt p pt andalso is_empty_tac (get_obj g_tac pt p)
2393 then (*after Take: transfer Frm and respective istate*)
2396 (get_loc pt (p,Frm), get_obj g_form pt p)
2397 val (pt, cs) = cut_tree pt (p,Frm)
2398 val pt = append_atomic p (e_istate, e_ctxt) f r f' s pt
2399 val pt = update_loc' pt p (SOME ist_form, SOME ist_res)
2401 else apfst (append_atomic p ist_res f r f' s) (cut_tree pt (p,Frm));
2403 (* called by Take *)
2404 fun append_form p l f pt =
2405 ((*tracing("##@append_form: pos ="^pos2str p);*)
2406 insert_pt (PrfObj {cell = NONE,
2407 form = (*if existpt p pt
2408 andalso get_obj g_tac pt p = Empty_Tac
2409 (*distinction from 'old' (+complete!) pobjs*)
2410 then get_obj g_form pt p else*) f,
2412 loc = (SOME l, NONE),
2414 result= (e_term,[]),
2415 ostate= Incomplete}) pt p
2417 (* val (p,loc,f) = ([1], e_istate, str2term "x + 1 = 2");
2418 val (p,loc,f) = (fst p, e_istate, str2term "-1 + x = 0");
2420 fun cappend_form pt p loc f =
2421 ((*tracing("##@cappend_form: pos ="^pos2str p);*)
2422 apfst (append_form p loc f) (cut_tree pt (p,Frm))
2424 fun cappend_form pt p loc f =
2425 let (*val _= tracing("##@cappend_form: pos ="^pos2str p)
2426 val _= tracing("##@cappend_form before cut_tree: loc ="^istate2str loc)*)
2427 val (pt', cs) = cut_tree pt (p,Frm)
2428 val pt'' = append_form p loc f pt'
2429 (*val _= tracing("##@cappend_form after append: loc ="^
2430 istates2str (get_obj g_loc pt'' p))*)
2435 fun append_result pt p l f s =
2436 (appl_obj (repl_result (fst (get_obj g_loc pt p), SOME l) f s) pt p, []);
2439 (*WN041022 deprecated, still for kbtest/diffapp.sml, /systest/root-equ.sml*)
2440 fun append_parent p l f r b pt =
2441 let (*val _= tracing("###append_parent: pos ="^pos2str p);*)
2442 val (ll,f) = if existpt p pt andalso is_empty_tac (get_obj g_tac pt p)
2443 then ((fst (get_obj g_loc pt p), SOME l),
2444 get_obj g_form pt p)
2445 else ((SOME l, NONE), f)
2446 in insert_pt (PrfObj
2452 result= (e_term,[]),
2453 ostate= Incomplete}) pt p end;
2454 fun cappend_parent pt p loc f r b =
2455 ((*tracing("###cappend_parent: pos ="^pos2str p);*)
2456 apfst (append_parent p loc f r b) (cut_tree pt (p,Und))
2460 fun append_problem [] l fmz (strs,spec,hdf) _ =
2461 ((*tracing("###append_problem: pos = []");*)
2464 origin= (strs,spec,hdf),
2467 probl = []:itm list,
2471 loc = (SOME l, NONE),
2472 branch= TransitiveB,(*FIXXXXXME.27.8.03: for equations only*)
2473 result= (e_term,[]),
2474 ostate= Incomplete},[]))
2476 | append_problem p l fmz (strs,spec,hdf) pt =
2477 ((*tracing("###append_problem: pos ="^pos2str p);*)
2480 origin= (strs,spec,hdf),
2483 probl = []:itm list,
2487 loc = (SOME l, NONE),
2488 branch= TransitiveB,
2489 result= (e_term,[]),
2490 ostate= Incomplete}) pt p
2492 fun cappend_problem _ [] loc fmz ori =
2493 ((*tracing("###cappend_problem: pos = []");*)
2494 (append_problem [] loc fmz ori EmptyPtree,[])
2496 | cappend_problem pt p loc fmz ori =
2497 ((*tracing("###cappend_problem: pos ="^pos2str p);*)
2498 apfst (append_problem p (loc:(istate * Proof.context)) fmz ori) (cut_tree pt (p,Frm))
2501 (*.get the theory explicitly specified for the rootpbl;
2502 thus use this function _after_ finishing specification.*)
2503 fun rootthy (Nd (PblObj {spec=(thyID, _, _), ...}, _)) = assoc_thy thyID
2504 | rootthy _ = error "rootthy";
2509 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
2511 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
2513 (* policy for "open" structures:
2514 --------------------------------
2515 The above "open Ctree" creates an unclear situation with structures, in particular in test/.
2516 This is work in progress, but urges to make policy explicit:
2518 (1) All structures are closed with a signature; this for prepares re-arrangement of structures.
2519 (2) Some structures are pervasive (e.g. Ctree) such, that an "open" ensures readability locally.
2520 (3) test/ is preceeded by "open" for all structures, in order to ease copy&paste from scr/ to test/
2522 ad (1) Presently this point is under construction.
2523 ad (2) Such local "open" are kept to a minimum (with the goal to reach Isabelle's state).
2524 ad (3) See https://intra.ist.tugraz.at/hg/isa/file/2ba35efb07b7/test/Tools/isac/Test_Isac.thy#l70