1 (* Title: the calctree, which holds a calculation |
|
2 Author: Walther Neuper 1999 |
|
3 (c) due to copyright terms |
|
4 |
|
5 Definitions required for Ctree, renamed later appropriately |
|
6 -------------------------vvvvv + I_Model.T-TEST are the only difference to |
|
7 BASIC_CALC_TREE |
|
8 *) |
|
9 |
|
10 signature BASIC_CALC_TREE_POS = |
|
11 sig |
|
12 (**** signature ****) |
|
13 (** the basic datatype **) |
|
14 type state |
|
15 val e_state: state |
|
16 |
|
17 type con |
|
18 eqtype cellID |
|
19 |
|
20 datatype branch = AndB | CollectB | IntersectB | MapB | NoBranch | OrB | SequenceB | TransitiveB |
|
21 datatype ostate = Complete | Incomplete | Inconsistent |
|
22 type specify_data |
|
23 type solve_data |
|
24 datatype ppobj = PblObj of specify_data | PrfObj of solve_data |
|
25 datatype ctree = EmptyPtree | Nd of ppobj * ctree list |
|
26 |
|
27 val rep_solve_data: ppobj -> solve_data |
|
28 val rep_specify_data: ppobj -> specify_data |
|
29 |
|
30 (** basic functions **) |
|
31 val e_ctree : ctree (* TODO: replace by EmptyPtree*) |
|
32 val existpt' : Pos.pos' -> ctree -> bool |
|
33 val is_interpos : Pos.pos' -> bool |
|
34 val lev_pred' : ctree -> Pos.pos' -> Pos.pos' |
|
35 val ins_chn : ctree list -> ctree -> Pos.pos -> ctree |
|
36 val children : ctree -> ctree list |
|
37 val get_nd : ctree -> Pos.pos -> ctree |
|
38 val just_created_ : ppobj -> bool |
|
39 val just_created : state -> bool |
|
40 val e_origin : Model_Def.o_model * References_Def.T * term |
|
41 |
|
42 val is_pblobj : ppobj -> bool |
|
43 val is_pblobj' : ctree -> Pos.pos -> bool |
|
44 val is_pblnd : ctree -> bool |
|
45 |
|
46 val g_spec : ppobj -> References_Def.T |
|
47 val g_loc : ppobj -> (Istate_Def.T * Proof.context) option * (Istate_Def.T * Proof.context) option |
|
48 val g_form : ppobj -> term |
|
49 val g_pbl : ppobj -> Model_Def.i_model_POS |
|
50 val g_met : ppobj -> Model_Def.i_model_POS |
|
51 val g_metID : ppobj -> MethodC.id |
|
52 val g_result : ppobj -> Celem.result |
|
53 val g_tac : ppobj -> Tactic.input |
|
54 val g_domID : ppobj -> ThyC.id |
|
55 |
|
56 val g_origin : ppobj -> Model_Def.o_model * References_Def.T * term |
|
57 val get_loc : ctree -> Pos.pos' -> Istate_Def.T * Proof.context |
|
58 val get_istate_LI : ctree -> Pos.pos' -> Istate_Def.T |
|
59 val get_ctxt_LI: ctree -> Pos.pos' -> Proof.context |
|
60 val get_ctxt : ctree -> Pos.pos' -> Proof.context (*DEPRECATED*) |
|
61 val get_obj : (ppobj -> 'a) -> ctree -> Pos.pos -> 'a |
|
62 val get_curr_formula : state -> term |
|
63 val get_assumptions : ctree -> Pos.pos' -> term list |
|
64 |
|
65 val new_val : term -> Istate_Def.T -> Istate_Def.T |
|
66 |
|
67 type cid = cellID list |
|
68 datatype ptform = Form of term | ModSpec of Specification_Def.T |
|
69 val get_somespec' : References_Def.T -> References_Def.T -> References_Def.T |
|
70 exception PTREE of string; |
|
71 |
|
72 val root_thy : ctree -> theory |
|
73 (* ---- made visible ONLY for structure CTaccess : CALC_TREE_ACCESS --------------------------- *) |
|
74 val appl_obj : (ppobj -> ppobj) -> ctree -> Pos.pos -> ctree |
|
75 val existpt : Pos.pos -> ctree -> bool |
|
76 val cut_tree : ctree -> Pos.pos * 'a -> ctree * Pos.pos' list |
|
77 val insert_pt : ppobj -> ctree -> int list -> ctree |
|
78 (* ---- made visible ONLY for structure CTnavi : CALC_TREE_NAVIGATION ------------------------- *) |
|
79 val g_branch : ppobj -> branch |
|
80 val g_form' : ctree -> term |
|
81 val g_ostate : ppobj -> ostate |
|
82 val g_ostate' : ctree -> ostate |
|
83 val g_res : ppobj -> term |
|
84 val g_res' : ctree -> term |
|
85 (*/---- duplicates in CTnavi, reconsider structs ----------------------------------------------- |
|
86 val lev_dn : CTbasic.Pos.pos -> Pos.pos (* duplicate in ctree-navi.sml *) |
|
87 val par_pblobj : CTbasic.ctree -> Pos.pos -> Pos.pos (* duplicate in ctree-navi.sml *) |
|
88 ---- duplicates in CTnavi, reconsider structs ----------------------------------------------/*) |
|
89 (*from isac_test for Minisubpbl*) |
|
90 val pr_ctree: Proof.context -> (Proof.context -> int list -> ppobj -> string) -> ctree -> string |
|
91 val pr_short: Proof.context -> Pos.pos -> ppobj -> string |
|
92 |
|
93 \<^isac_test>\<open> |
|
94 val g_ctxt : ppobj -> Proof.context |
|
95 val g_fmz : ppobj -> Model_Def.form_T |
|
96 val get_allp : Pos.pos' list -> Pos.pos * (int list * Pos.pos_) -> ctree -> Pos.pos' list |
|
97 val get_allps : (Pos.pos * Pos.pos_) list -> Pos.posel list -> ctree list -> Pos.pos' list |
|
98 val get_allpos' : Pos.pos * Pos.posel -> ctree -> Pos.pos' list |
|
99 val get_allpos's : Pos.pos * Pos.posel -> ctree list -> (Pos.pos * Pos.pos_) list |
|
100 val cut_bottom : Pos.pos * Pos.posel -> ctree -> (ctree * Pos.pos' list) * bool |
|
101 val cut_level : Pos.pos' list -> Pos.pos -> ctree -> int list * Pos.pos_ -> ctree * Pos.pos' list |
|
102 val cut_level__ : Pos.pos' list -> Pos.pos -> ctree -> int list * Pos.pos_ -> ctree * Pos.pos' list |
|
103 val get_trace : ctree -> int list -> int list -> int list list |
|
104 val branch2str : branch -> string |
|
105 \<close> |
|
106 end |
|
107 |
|
108 (**) |
|
109 structure CTbasic_POS(**): BASIC_CALC_TREE_POS(**) = |
|
110 struct |
|
111 (**) |
|
112 open Pos |
|
113 |
|
114 (**** Ctree ****) |
|
115 |
|
116 (*** general types* **) |
|
117 |
|
118 datatype branch = |
|
119 NoBranch | AndB | OrB |
|
120 | TransitiveB (* FIXXXME.0308: set branch from met in Apply_Method |
|
121 FIXXXME.0402: -"- in Begin_Trans'*) |
|
122 | SequenceB | IntersectB | CollectB | MapB; |
|
123 |
|
124 \<^isac_test>\<open> |
|
125 fun branch2str NoBranch = "NoBranch" |
|
126 | branch2str AndB = "AndB" |
|
127 | branch2str OrB = "OrB" |
|
128 | branch2str TransitiveB = "TransitiveB" |
|
129 | branch2str SequenceB = "SequenceB" |
|
130 | branch2str IntersectB = "IntersectB" |
|
131 | branch2str CollectB = "CollectB" |
|
132 | branch2str MapB = "MapB"; |
|
133 \<close> |
|
134 |
|
135 datatype ostate = |
|
136 Incomplete | Complete | Inconsistent (* WN041020 latter still unused *); |
|
137 \<^isac_test>\<open> |
|
138 fun ostate2str Incomplete = "Incomplete" |
|
139 | ostate2str Complete = "Complete" |
|
140 | ostate2str Inconsistent = "Inconsistent"; |
|
141 \<close> |
|
142 |
|
143 type cellID = int; |
|
144 type cid = cellID list; |
|
145 |
|
146 |
|
147 type iist = Istate_Def.T option * Istate_Def.T option; |
|
148 (*val e_iist = (empty, empty); --- sinnlos f"ur NICHT-equality-type*) |
|
149 |
|
150 |
|
151 fun new_val v (Istate_Def.Pstate pst) = |
|
152 (Istate_Def.Pstate (Istate_Def.set_act v pst)) |
|
153 | new_val _ _ = raise ERROR "new_val: only for Pstate"; |
|
154 |
|
155 datatype con = land | lor; |
|
156 |
|
157 (* executed tactics (tac_s) with local environment etc.; |
|
158 used for continuing eval script + for generate *) |
|
159 type ets = |
|
160 (TermC.path *(* of tactic in program, tactic (weakly) associated with tac_ *) |
|
161 (Tactic.T * (* (for generate) *) |
|
162 Env.T * (* with 'tactic=result' as rule, tactic ev. _not_ ready for 'parallel let' *) |
|
163 Env.T * (* with results of (ready) tacs *) |
|
164 term * (* itr_arg of tactic, for upd. env at Repeat, Try *) |
|
165 term * (* result value of the tac *) |
|
166 Celem.safe)) |
|
167 list; |
|
168 |
|
169 type envp =(*9.5.03: unused, delete with field in ctree.PblObj FIXXXME*) |
|
170 (int * term list) list * (* assoc-list: args of met*) |
|
171 (int * Rule_Set.T) list * (* assoc-list: tacs already done ///15.9.00*) |
|
172 (int * ets) list * (* assoc-list: tacs etc. already done*) |
|
173 (string * pos) list; (* asms * from where*) |
|
174 |
|
175 |
|
176 (*** type Ctree ***) |
|
177 |
|
178 type specify_data = |
|
179 {fmz : Model_Def.form_T, (* for uniformity also created/used for/by Subproblem *) |
|
180 origin: (Model_Def.o_model) *(* = O_Model.T for efficiently checking input to I_Model *) |
|
181 References_Def.T * (* updated by Refine_Tacitly *) |
|
182 term, (* headline of calc-head, as calculated initially(!) *) |
|
183 spec : References_Def.T, (* explicitly input *) |
|
184 probl : Model_Def.i_model_POS,(* = I_Model.T for interactive input to a Problem *) |
|
185 meth : Model_Def.i_model_POS,(* = I_Model.T for interactive input to a MethodC *) |
|
186 ctxt : Proof.context, (* used while specifying this (Sub-)Problem and MethodC *) |
|
187 loc : (Istate_Def.T * Proof.context) option (* like in PrfObj, calling this SubProblem *) |
|
188 * (Istate_Def.T * Proof.context) option, (* like in PrfObj, finishing the SubProblem *) |
|
189 branch: branch, (* like PrfObj *) |
|
190 result: Celem.result, (* like PrfObj *) |
|
191 ostate: ostate}; (* like PrfObj *) |
|
192 type solve_data = (* TODO: arrange according to signature *) |
|
193 {form : term, (* where tactic is applied to *) |
|
194 tac : Tactic.input, (* tactic as presented to users *) |
|
195 loc : (Istate_Def.T * (* program interpreter state *) |
|
196 Proof.context) (* context for provers, type inference *) |
|
197 option * (* both for interpreter location on Frm, Pbl, Met *) |
|
198 (Istate_Def.T * (* script interpreter state *) |
|
199 Proof.context) (* context for provers, type inference *) |
|
200 option, (* both for interpreter location on Res, (NONE,NONE) == empty *) |
|
201 branch: branch, (* only rudimentary *) |
|
202 result: Celem.result, (* result and assumptions *) |
|
203 ostate: ostate} (* Complete <=> result is OK *) |
|
204 |
|
205 datatype ppobj = |
|
206 PblObj of specify_data (* data serving a whole specification-phase *) |
|
207 | PrfObj of solve_data; (* data for a proof step triggered by a tactic *) |
|
208 |
|
209 (* this tree contains isac's calculations; |
|
210 the tree's structure has been copied from an early version of Theorema(c); |
|
211 it has the disadvantage, that there is no space |
|
212 for the first tactic in a script generating the first formula at (p,Frm); |
|
213 this trouble has been covered by 'implicit_take' and 'Take' so far, |
|
214 but it is crucial if the first tactic in a script is eg. 'Subproblem'; |
|
215 see 'type tac', Apply_Method. |
|
216 *) |
|
217 datatype ctree = |
|
218 EmptyPtree |
|
219 | Nd of ppobj * (ctree list); |
|
220 val e_ctree = EmptyPtree; |
|
221 type state = ctree * pos' |
|
222 val e_state = (EmptyPtree , e_pos') |
|
223 |
|
224 fun rep_solve_data (PrfObj solve_data) = solve_data |
|
225 | rep_solve_data _ = raise ERROR "rep_solve_data ONLY for solve_data" |
|
226 fun rep_specify_data (PblObj specify_data) = specify_data |
|
227 | rep_specify_data _ = raise ERROR "rep_solve_data ONLY for solve_data" |
|
228 |
|
229 |
|
230 (*** minimal set of functions on Ctree* **) |
|
231 |
|
232 fun is_pblobj (PblObj _) = true |
|
233 | is_pblobj _ = false; |
|
234 |
|
235 exception PTREE of string; |
|
236 fun nth _ [] = raise PTREE "nth _ []" |
|
237 | nth 1 (x :: _) = x |
|
238 | nth n (_ :: xs) = nth (n - 1) xs; |
|
239 (*> nth 2 [11,22,33]; -->> val it = 22 : int*) |
|
240 |
|
241 |
|
242 (** convert ctree to a string **) |
|
243 |
|
244 (* convert a pos from list to string *) |
|
245 fun pr_pos ps = (space_implode "." (map string_of_int ps)) ^ ". "; |
|
246 (* show hd origin or form only *) |
|
247 (**) |
|
248 fun pr_short _ p (PblObj _) = pr_pos p ^ " ----- pblobj -----\n" |
|
249 | pr_short ctxt p (PrfObj {form = form, ...}) = pr_pos p ^ UnparseC.term ctxt form ^ "\n"; |
|
250 fun pr_ctree ctxt f pt = |
|
251 let |
|
252 fun pr_pt _ _ EmptyPtree = "" |
|
253 | pr_pt pfn ps (Nd (b, [])) = pfn ps b |
|
254 | pr_pt pfn ps (Nd (b, ts)) = pfn ps b ^ prts pfn ps 1 ts |
|
255 and prts _ _ _ [] = "" |
|
256 | prts pfn ps p (t :: ts) = (pr_pt pfn (ps @ [p]) t)^ |
|
257 (prts pfn ps (p + 1) ts) |
|
258 in pr_pt (f ctxt) [] pt end; |
|
259 |
|
260 |
|
261 |
|
262 (** access the branches of ctree **) |
|
263 |
|
264 fun repl [] _ _ = raise PTREE "repl [] _ _" |
|
265 | repl (_ :: ls) 1 e = e :: ls |
|
266 | repl (l :: ls) n e = l :: (repl ls (n-1) e); |
|
267 fun repl_app ls n e = |
|
268 let |
|
269 val lim = 1 + length ls |
|
270 in |
|
271 if n > lim |
|
272 then raise PTREE "repl_app: n > lim" |
|
273 else if n = lim |
|
274 then ls @ [e] |
|
275 else repl ls n e end; |
|
276 |
|
277 (* get from obj at pos by f : ppobj -> 'a *) |
|
278 fun get_obj _ EmptyPtree _ = raise PTREE "get_obj f EmptyPtree" |
|
279 | get_obj f (Nd (b, _)) [] = f b |
|
280 | get_obj f (Nd (_, bs)) (p :: ps) = |
|
281 case \<^try>\<open> get_obj f (nth p bs) ps \<close> of |
|
282 SOME obj => obj |
|
283 | NONE => raise PTREE ("get_obj: pos = " ^ ints2str' (p :: ps) ^ " does not exist"); |
|
284 fun get_nd EmptyPtree _ = raise PTREE "get_nd EmptyPtree" |
|
285 | get_nd n [] = n |
|
286 | get_nd (Nd (_, nds)) (pos as p :: ps) = |
|
287 case \<^try>\<open> get_nd (nth p nds) ps \<close> of |
|
288 SOME nd => nd |
|
289 | NONE => raise PTREE ("get_nd: not existent pos = " ^ ints2str' pos); |
|
290 |
|
291 (* for use by get_obj *) |
|
292 fun g_form (PrfObj {form = f,...}) = f |
|
293 | g_form (PblObj {origin= (_,_,f),...}) = f; |
|
294 fun g_form' (Nd (PrfObj {form = f, ...}, _)) = f |
|
295 | g_form' (Nd (PblObj {origin= (_, _, f),...}, _)) = f |
|
296 | g_form' _ = raise ERROR "g_form': uncovered fun def."; |
|
297 (* | g_form _ = raise PTREE "g_form not for PblObj";*) |
|
298 fun g_origin (PblObj {origin = ori, ...}) = ori |
|
299 | g_origin _ = raise PTREE "g_origin not for PrfObj"; |
|
300 \<^isac_test>\<open> |
|
301 fun g_fmz (PblObj {fmz = f, ...}) = f |
|
302 | g_fmz _ = raise PTREE "g_fmz not for PrfObj"; |
|
303 \<close> |
|
304 fun g_spec (PblObj {spec = s, ...}) = s |
|
305 | g_spec _ = raise PTREE "g_spec not for PrfObj"; |
|
306 fun g_pbl (PblObj {probl = p, ...}) = p |
|
307 | g_pbl _ = raise PTREE "g_pbl not for PrfObj"; |
|
308 fun g_met (PblObj {meth = p, ...}) = p |
|
309 | g_met _ = raise PTREE "g_met not for PrfObj"; |
|
310 fun g_domID (PblObj {spec = (d, _, _), ...}) = d |
|
311 | g_domID _ = raise PTREE "g_metID not for PrfObj"; |
|
312 fun g_metID (PblObj {spec = (_, _, m), ...}) = m |
|
313 | g_metID _ = raise PTREE "g_metID not for PrfObj"; |
|
314 fun g_ctxt (PblObj {ctxt, ...}) = ctxt |
|
315 | g_ctxt _ = raise PTREE "g_ctxt not for PrfObj"; |
|
316 fun g_loc (PblObj {loc = l, ...}) = l |
|
317 | g_loc (PrfObj {loc = l, ...}) = l; |
|
318 fun g_branch (PblObj {branch = b, ...}) = b |
|
319 | g_branch (PrfObj {branch = b, ...}) = b; |
|
320 fun g_tac (PblObj {spec = (_, _, m),...}) = Tactic.Apply_Method m |
|
321 | g_tac (PrfObj {tac = m, ...}) = m; |
|
322 fun g_result (PblObj {result = r, ...}) = r |
|
323 | g_result (PrfObj {result = r, ...}) = r; |
|
324 fun g_res (PblObj {result = (r, _) ,...}) = r |
|
325 | g_res (PrfObj {result = (r, _),...}) = r; |
|
326 fun g_res' (Nd (PblObj {result = (r, _), ...}, _)) = r |
|
327 | g_res' (Nd (PrfObj {result = (r, _),...}, _)) = r |
|
328 | g_res' _ = raise PTREE "g_res': uncovered fun def."; |
|
329 fun g_ostate (PblObj {ostate = r, ...}) = r |
|
330 | g_ostate (PrfObj {ostate = r, ...}) = r; |
|
331 fun g_ostate' (Nd (PblObj {ostate = r, ...}, _)) = r |
|
332 | g_ostate' (Nd (PrfObj {ostate = r, ...}, _)) = r |
|
333 | g_ostate' _ = raise PTREE "g_ostate': uncovered fun def."; |
|
334 |
|
335 (* get the formula preceeding the current position in a calculation *) |
|
336 fun get_curr_formula (pt, (p, p_)) = |
|
337 case p_ of |
|
338 Frm => get_obj g_form pt p |
|
339 | Res => (fst o (get_obj g_result pt)) p |
|
340 | _ => #3 (get_obj g_origin pt p); (* the headline*) |
|
341 |
|
342 (* in CalcTree/Subproblem an 'just_created_' model is created; |
|
343 this is filled to 'untouched' by Model/Refine_Problem *) |
|
344 fun just_created_ (PblObj {meth, probl, spec, ...}) = |
|
345 null meth andalso null probl andalso spec = References_Def.empty |
|
346 | just_created_ _ = raise PTREE "g_ostate': uncovered fun def."; |
|
347 val e_origin = ([], References_Def.empty, TermC.empty); |
|
348 |
|
349 fun just_created (pt, (p, _)) = |
|
350 let val ppobj = get_obj I pt p |
|
351 in is_pblobj ppobj andalso just_created_ ppobj end; |
|
352 |
|
353 (* does the pos in the ctree exist ? *) |
|
354 fun existpt pos pt = can (get_obj I pt) pos; |
|
355 (* does the pos' in the ctree exist, ie. extra check for result in the node *) |
|
356 fun existpt' (p, p_) pt = |
|
357 if can (get_obj I pt) p |
|
358 then case p_ of |
|
359 Res => get_obj g_ostate pt p = Complete |
|
360 | _ => true |
|
361 else false; |
|
362 |
|
363 (* is this position appropriate for calculating intermediate steps? *) |
|
364 fun is_interpos (_, Res) = true |
|
365 | is_interpos _ = false; |
|
366 |
|
367 (* get the children of a node in ctree *) |
|
368 fun children (Nd (PblObj _, cn)) = cn |
|
369 | children (Nd (PrfObj _, cn)) = cn |
|
370 | children _ = raise ERROR "children: uncovered fun def."; |
|
371 |
|
372 (*/--------------- duplicates in ctree-navi.sml: required also here below ---------------\*) |
|
373 \<^isac_test>\<open> |
|
374 fun lev_up [] = raise PTREE "lev_up []" |
|
375 | lev_up p = (drop_last p):pos; |
|
376 (* find the position of the next parent which is a PblObj in ctree *) |
|
377 fun par_pblobj _ [] = [] |
|
378 | par_pblobj pt p = |
|
379 let |
|
380 fun par _ [] = [] |
|
381 | par pt p = |
|
382 if is_pblobj (get_obj I pt p) |
|
383 then p |
|
384 else par pt (lev_up p) |
|
385 in par pt (lev_up p) end; |
|
386 \<close> |
|
387 (*\--------------- duplicates in ctree-navi.sml: required also here below ---------------/*) |
|
388 |
|
389 (* insert obj b into ctree at pos, ev.overwriting this pos *) |
|
390 fun insert_pt b EmptyPtree [] = Nd (b, []) |
|
391 | insert_pt _ EmptyPtree _ = raise PTREE "insert_pt b Empty _" |
|
392 | insert_pt b _ [] = Nd (b, []) |
|
393 | insert_pt b (Nd (b', bs)) (p :: []) = Nd (b', repl_app bs p (Nd (b, []))) |
|
394 | insert_pt b (Nd (b', bs)) (p :: ps) = Nd (b', repl_app bs p (insert_pt b (nth p bs) ps)); |
|
395 |
|
396 (* insert children to a node without children. compare: fun insert_pt *) |
|
397 fun ins_chn _ EmptyPtree _ = raise PTREE "ins_chn: EmptyPtree" |
|
398 | ins_chn _ (Nd _) [] = raise PTREE "ins_chn: pos = []" |
|
399 | ins_chn ns (Nd (b, bs)) (p :: []) = |
|
400 if p > length bs |
|
401 then raise PTREE "ins_chn: pos not existent" |
|
402 else |
|
403 let |
|
404 val (b', bs') = case nth p bs of |
|
405 Nd (b', bs') => (b', bs') |
|
406 | _ => raise ERROR "ins_chn: uncovered case nth" |
|
407 in |
|
408 if null bs' |
|
409 then Nd (b, repl_app bs p (Nd (b', ns))) |
|
410 else raise PTREE "ins_chn: pos mustNOT be overwritten" |
|
411 end |
|
412 | ins_chn ns (Nd (b, bs)) (p::ps) = Nd (b, repl_app bs p (ins_chn ns (nth p bs) ps)); |
|
413 |
|
414 (* apply f to obj at pos, f: ppobj -> ppobj *) |
|
415 fun appl_to_node f (Nd (b, bs)) = Nd (f b, bs) |
|
416 | appl_to_node _ _ = raise ERROR "appl_to_node: uncovered fun def."; |
|
417 fun appl_obj _ EmptyPtree [] = EmptyPtree |
|
418 | appl_obj _ EmptyPtree _ = raise PTREE "appl_obj f Empty _" |
|
419 | appl_obj f (Nd (b, bs)) [] = Nd (f b, bs) |
|
420 | appl_obj f (Nd (b, bs)) (p :: []) = Nd (b, repl_app bs p (((appl_to_node f) o (nth p)) bs)) |
|
421 | appl_obj f (Nd (b, bs)) (p :: ps) = Nd (b, repl_app bs p (appl_obj f (nth p bs) (ps:pos))); |
|
422 |
|
423 datatype ptform = Form of term | ModSpec of Specification_Def.T; |
|
424 |
|
425 \<^isac_test>\<open> |
|
426 fun test_trans (PrfObj {branch, ...}) = true andalso branch = TransitiveB |
|
427 | test_trans (PblObj {branch, ...}) = true andalso branch = TransitiveB; |
|
428 \<close> |
|
429 |
|
430 fun is_pblobj' pt p = |
|
431 let val ppobj = get_obj I pt p |
|
432 in is_pblobj ppobj end; |
|
433 |
|
434 fun del_res (PblObj {fmz, origin, spec, probl, meth, ctxt, loc = (l1, _), branch, ...}) = |
|
435 PblObj {fmz = fmz, origin = origin, spec = spec, probl = probl, meth = meth, |
|
436 ctxt = ctxt, loc= (l1, NONE), branch = branch, |
|
437 result = (TermC.empty, []), ostate = Incomplete} |
|
438 | del_res (PrfObj {form, tac, loc= (l1, _), branch, ...}) = |
|
439 PrfObj {form = form, tac = tac, loc = (l1, NONE), branch = branch, |
|
440 result = (TermC.empty, []), ostate = Incomplete}; |
|
441 |
|
442 |
|
443 fun get_loc EmptyPtree _ = (Istate_Def.empty, ContextC.empty) |
|
444 | get_loc pt (p, Res) = |
|
445 (case get_obj g_loc pt p of |
|
446 (SOME ist_ctxt, NONE) => ist_ctxt |
|
447 | (NONE , NONE) => (Istate_Def.empty, ContextC.empty) |
|
448 | (_ , SOME ist_ctxt) => ist_ctxt) |
|
449 | get_loc pt (p, _) = |
|
450 (case get_obj g_loc pt p of |
|
451 (NONE , SOME ist_ctxt) => ist_ctxt (* 020813 too liberal? *) |
|
452 | (NONE , NONE) => (Istate_Def.empty, ContextC.empty) |
|
453 | (SOME ist_ctxt, _) => ist_ctxt); |
|
454 fun get_istate_LI pt p = get_loc pt p |> #1; |
|
455 fun get_ctxt_LI pt p = get_loc pt p |> #2; |
|
456 fun get_ctxt pt (pos as (p, p_)) = |
|
457 if member op = [Frm, Res] p_ |
|
458 then get_loc pt pos |> #2 (*for program interpretation rely on fun get_loc*) |
|
459 else (*p = Pbl: for specify phase take ctxt from PblObj *) |
|
460 if (p |> get_obj g_origin pt |> LibraryC.fst3) = [] (*CAS-command ? *) |
|
461 then (Know_Store.get_via_last_thy "Isac_Knowledge"(*CAS-command unknown*)) |> Defs.global_context |> fst |
|
462 else get_obj g_ctxt pt p |
|
463 |
|
464 fun get_assumptions pt p = get_ctxt pt p |> ContextC.get_assumptions; |
|
465 |
|
466 fun get_somespec' (dI, pI, mI) (dI', pI', mI') = |
|
467 let |
|
468 val domID = if dI = ThyC.id_empty then dI' else dI |
|
469 val pblID = if pI = Problem.id_empty then pI' else pI |
|
470 val metID = if mI = MethodC.id_empty then mI' else mI |
|
471 in (domID, pblID, metID) end; |
|
472 |
|
473 (**.development for extracting an 'interval' from ptree.**) |
|
474 |
|
475 \<^isac_test>\<open> |
|
476 (*WN0510 version stopped in favour of get_interval with !!!move_dn, getFormulaeFromTo |
|
477 actually used (inefficient) version with move_dn: see modspec.sml*) |
|
478 local |
|
479 |
|
480 fun hdp [] = 1 | hdp [0] = 1 | hdp x = hd x;(*start with first*) |
|
481 fun hdq [] = 99999 | hdq [0] = 99999 | hdq x = hd x;(*take until last*) |
|
482 fun tlp [] = [0] | tlp [_] = [0] | tlp x = tl x; |
|
483 fun tlq [] = [99999] | tlq [_] = [99999] | tlq x = tl x; |
|
484 |
|
485 fun getnd i (b,p) q (Nd (_, nds)) = |
|
486 (if i <= 0 then [[b]] else []) @ |
|
487 (getnds (i-1) true (b@[hdp p], tlp p) (tlq q) |
|
488 (take_fromto (hdp p) (hdq q) nds)) |
|
489 | getnd _ _ _ _ = raise ERROR "getnd: uncovered case in fun.def." |
|
490 and getnds _ _ _ _ [] = [] (*no children*) |
|
491 | getnds i _ (b,p) q [nd] = (getnd i (b,p) q nd) (*l+r-margin*) |
|
492 |
|
493 | getnds i true (b,p) q [n1, n2] = (*l-margin, r-margin*) |
|
494 (getnd i ( b, p ) [99999] n1) @ |
|
495 (getnd ~99999 (lev_on b,[0]) q n2) |
|
496 |
|
497 | getnds i _ (b, _) q [n1, n2] = (*intern, r-margin*) |
|
498 (getnd i ( b,[0]) [99999] n1) @ |
|
499 (getnd ~99999 (lev_on b,[0]) q n2) |
|
500 |
|
501 | getnds i true (b,p) q (nd::(nds as _::_)) = (*l-margin, intern*) |
|
502 (getnd i ( b, p ) [99999] nd) @ |
|
503 (getnds ~99999 false (lev_on b,[0]) q nds) |
|
504 |
|
505 | getnds i _ (b, _) q (nd::(nds as _::_)) = (*intern, ...*) |
|
506 (getnd i ( b,[0]) [99999] nd) @ |
|
507 (getnds ~99999 false (lev_on b,[0]) q nds); |
|
508 in |
|
509 (*get an 'interval from to' from a ptree as 'intervals f t' of respective nodes |
|
510 where 'from' are pos, i.e. a key as int list, 'f' an int (to,t analoguous) |
|
511 (1) the 'f' are given |
|
512 (1a) by 'from' if 'f' = the respective element of 'from' (left margin) |
|
513 (1b) -inifinity, if 'f' > the respective element of 'from' (internal node) |
|
514 (2) the 't' ar given |
|
515 (2a) by 'to' if 't' = the respective element of 'to' (right margin) |
|
516 (2b) inifinity, if 't' < the respective element of 'to (internal node)' |
|
517 the 'f' and 't' are set by hdp,... *) |
|
518 fun get_trace pt p q = |
|
519 (flat o (getnds ((length p) -1) true ([hdp p], tlp p) (tlq q))) |
|
520 (take_fromto (hdp p) (hdq q) (children pt)); |
|
521 end; |
|
522 |
|
523 (*extract a formula or model from ctree for itms2itemppc or model2xml*) |
|
524 fun preconds2str bts = |
|
525 (strs2str o (map (linefeed o pair2str o |
|
526 (apsnd (UnparseC.term @{context})) o |
|
527 (apfst bool2str)))) bts; |
|
528 |
|
529 fun ocalhd2str (b, p, hdf, itms, prec, spec) = |
|
530 "(" ^ bool2str b ^ ", " ^ pos_2str p ^ ", " ^ UnparseC.term @{context} hdf ^ |
|
531 ", " ^ "\<forall>itms2str itms\<forall>" (*Model_Def.itms2str_ (ThyC.id_to_ctxt "Isac_Knowledge") itms*) ^ |
|
532 ", " ^ preconds2str prec ^ ", \n" ^ References_Def.to_string spec ^ " )"; |
|
533 \<close> |
|
534 |
|
535 |
|
536 fun is_pblnd (Nd (ppobj, _)) = is_pblobj ppobj |
|
537 | is_pblnd _ = raise ERROR "is_pblnd: uncovered fun def."; |
|
538 |
|
539 |
|
540 (* determine the previous pos' on the same level |
|
541 WN0502 made for interSteps; _only_ works for branch TransitiveB WN120517 compare lev_back *) |
|
542 fun lev_pred' _ ([], Res) = ([], Pbl) |
|
543 | lev_pred' pt (p, Res) = |
|
544 let val (p', last) = split_last p |
|
545 in |
|
546 if last = 1 |
|
547 then if (is_pblobj o (get_obj I pt)) p then (p, Pbl) else (p, Frm) |
|
548 else if get_obj g_res pt (p' @ [last - 1]) = get_obj g_form pt p |
|
549 then (p' @ [last - 1], Res) (* TransitiveB *) |
|
550 else if (is_pblobj o (get_obj I pt)) p then (p,Pbl) else (p, Frm) |
|
551 end |
|
552 | lev_pred' _ _ = raise ERROR ""; |
|
553 |
|
554 |
|
555 (**.insert into ctree and cut branches accordingly.**) |
|
556 |
|
557 \<^isac_test>\<open> |
|
558 (* get all positions of certain intervals on the ctree. |
|
559 old VERSION without move_dn; kept for occasional redesign |
|
560 get all pos's to be cut in a ctree |
|
561 below a pos or from a ctree list after i-th element (NO level_up) *) |
|
562 fun get_allpos' (_, _) EmptyPtree = [] |
|
563 | get_allpos' (p, 1) (Nd (b, bs)) = (* p is pos of Nd *) |
|
564 if g_ostate b = Incomplete |
|
565 then (p, Frm) :: (get_allpos's (p, 1) bs) |
|
566 else (p, Frm) :: (get_allpos's (p, 1) bs) @ [(p, Res)] |
|
567 | get_allpos' (p, _) (Nd (b, bs)) = (* p is pos of Nd *) |
|
568 if length bs > 0 orelse is_pblobj b |
|
569 then if g_ostate b = Incomplete |
|
570 then [(p,Frm)] @ (get_allpos's (p, 1) bs) |
|
571 else [(p,Frm)] @ (get_allpos's (p, 1) bs) @ [(p, Res)] |
|
572 else if g_ostate b = Incomplete then [] else [(p, Res)] |
|
573 and get_allpos's _ [] = [] |
|
574 | get_allpos's (p, i) (pt :: pts) = (* p is pos of parent-Nd *) |
|
575 (get_allpos' (p @ [i], i) pt) @ (get_allpos's (p, i + 1) pts); |
|
576 |
|
577 (*WN050106 like cut_level, but deletes exactly 1 node *) |
|
578 fun cut_level__ _ _ EmptyPtree _ =raise PTREE "cut_level__ Empty _" (* for tests ONLY *) |
|
579 | cut_level__ _ _ (Nd ( _, _)) ([], _) = raise PTREE "cut_level__ _ []" |
|
580 | cut_level__ cuts P (Nd (b, bs)) (p :: [], p_) = |
|
581 if test_trans b |
|
582 then |
|
583 (Nd (b, drop_nth [] (p:Pos.posel, bs)), |
|
584 cuts @ (if p_ = Frm then [(P @ [p], Res)] else []) @ |
|
585 (get_allpos's (P, p + 1) (drop_nth [] (p, bs)))) |
|
586 else (Nd (b, bs), cuts) |
|
587 | cut_level__ cuts P (Nd (b, bs)) ((p :: ps), p_) = |
|
588 let |
|
589 val (bs', cuts') = cut_level__ cuts P (nth p bs) (ps, p_) |
|
590 in (Nd (b, repl_app bs p bs'), cuts @ cuts') end; |
|
591 |
|
592 fun cut_level _ _ EmptyPtree _ = raise PTREE "cut_level EmptyPtree _" |
|
593 | cut_level _ _ (Nd ( _, _)) ([],_) = raise PTREE "cut_level _ []" |
|
594 | cut_level cuts P (Nd (b, bs)) (p :: [], p_) = |
|
595 if test_trans b |
|
596 then |
|
597 (Nd (b, take (p:Pos.posel, bs)), |
|
598 cuts @ |
|
599 (if p_ = Frm andalso (*#*) g_ostate b = Complete then [(P@[p],Res)] else ([]:pos' list)) @ |
|
600 (get_allpos's (P, p+1) (takerest (p, bs)))) |
|
601 else (Nd (b, bs), cuts) |
|
602 | cut_level cuts P (Nd (b, bs)) ((p :: ps), p_) = |
|
603 let |
|
604 val (bs', cuts') = cut_level cuts P (nth p bs) (ps, p_) |
|
605 in (Nd (b, repl_app bs p bs'), cuts @ cuts') end; |
|
606 |
|
607 |
|
608 (*old version before WN050219, overwritten below*) |
|
609 fun cut_tree _ ([], _) = raise PTREE "cut_tree _ ([],_)" |
|
610 | cut_tree pt (pos as ([_], _)) = |
|
611 let |
|
612 val (pt', cuts) = cut_level [] [] pt pos |
|
613 in |
|
614 (pt', cuts @ (if get_obj g_ostate pt [] = Incomplete then [] else [([], Res)])) |
|
615 end |
|
616 | cut_tree pt (p,p_) = |
|
617 let |
|
618 fun cutfn pt cuts (p, p_) = |
|
619 let |
|
620 val (pt', cuts') = cut_level [] (lev_up p) pt (p,p_) |
|
621 in |
|
622 if length cuts' > 0 andalso length p > 1 |
|
623 then cutfn pt' (cuts @ cuts') (lev_up p, Frm(*-->(p,Res)*)) |
|
624 else (pt', cuts @ cuts') |
|
625 end |
|
626 val (pt', cuts) = cutfn pt [] (p, p_) |
|
627 in |
|
628 (pt', cuts @ (if get_obj g_ostate pt [] = Incomplete then [] else [([], Res)])) |
|
629 end; |
|
630 \<close> |
|
631 |
|
632 local |
|
633 fun move_dn _ (Nd (_, ns)) ([],p_) = (* root problem *) |
|
634 (case p_ of |
|
635 Res => raise PTREE "move_dn: end of calculation" |
|
636 | _ => |
|
637 if null ns (* go down from Pbl + Met *) |
|
638 then raise PTREE "move_dn: solve problem not started" |
|
639 else ([1], Frm)) |
|
640 | move_dn P (Nd (_, ns)) (p :: (ps as (_ :: _)), p_) = (* iterate to end of pos *) |
|
641 if p > length ns |
|
642 then raise PTREE "move_dn: pos not existent 2" |
|
643 else move_dn (P @ [p]) (nth p ns) (ps, p_) |
|
644 | move_dn P (Nd (c, ns)) ([p], p_) = (* act on last element of pos *) |
|
645 if p > length ns |
|
646 then raise PTREE "move_dn: pos not existent 3" |
|
647 else |
|
648 (case p_ of |
|
649 Res => |
|
650 if p = length ns (* last Res on this level: go a level up *) |
|
651 then if g_ostate c = Complete |
|
652 then (P, Res) |
|
653 else raise PTREE (ints2str' P ^ " not complete 1") |
|
654 else (* go to the next Nd on this level, or down into the next Nd *) |
|
655 if is_pblnd (nth (p + 1) ns) then (P@[p + 1], Pbl) |
|
656 else if g_res' (nth p ns) = g_form' (nth (p + 1) ns) |
|
657 then if (null o children o (nth (p + 1))) ns |
|
658 then (* take the Res if Complete *) |
|
659 if g_ostate' (nth (p + 1) ns) = Complete |
|
660 then (P@[p + 1], Res) |
|
661 else raise PTREE (ints2str' (P@[p + 1]) ^ " not complete 2") |
|
662 else (P@[p + 1, 1], Frm) (* go down into the next PrfObj *) |
|
663 else (P@[p + 1], Frm) (* take Frm: exists if the Nd exists *) |
|
664 | Frm => (*go down or to the Res of this Nd*) |
|
665 if (null o children o (nth p)) ns |
|
666 then if g_ostate' (nth p ns) = Complete then (P @ [p], Res) |
|
667 else raise PTREE (ints2str' (P @ [p])^" not complete 3") |
|
668 else (P @ [p, 1], Frm) |
|
669 | _ => (* is Pbl or Met *) |
|
670 if (null o children o (nth p)) ns |
|
671 then raise PTREE "move_dn:solve subproblem not startd" |
|
672 else (P @ [p, 1], |
|
673 if (is_pblnd o hd o children o (nth p)) ns |
|
674 then Pbl else Frm)) |
|
675 | move_dn _ _ _ = raise ERROR ""; |
|
676 in |
|
677 (* get all positions in a ctree until ([],Res) or ostate=Incomplete |
|
678 val get_allp = fn : |
|
679 pos' list -> : accumulated, start with [] |
|
680 pos -> : the offset for subtrees wrt the root |
|
681 ctree -> : (sub)tree |
|
682 pos' : initialization (the last pos' before ...) |
|
683 -> pos' list : of positions in this (sub) tree (relative to the root) |
|
684 *) |
|
685 fun get_allp cuts (P, pos) pt = |
|
686 (let |
|
687 val nxt = move_dn [] pt pos (*exn if Incomplete reached*) |
|
688 in |
|
689 if nxt <> ([], Res) |
|
690 then get_allp (cuts @ [nxt]) (P, nxt) pt |
|
691 else map (apfst (curry op @ P)) (cuts @ [nxt]) |
|
692 end) |
|
693 handle PTREE _ => (map (apfst (curry op@ P)) cuts); |
|
694 end |
|
695 |
|
696 (* the pts are assumed to be on the same level *) |
|
697 fun get_allps cuts _ [] = cuts |
|
698 | get_allps cuts P (pt :: pts) = |
|
699 let |
|
700 val below = get_allp [] (P, ([], Frm)) pt |
|
701 val levfrm = |
|
702 if is_pblnd pt |
|
703 then (P, Pbl) :: below |
|
704 else if last_elem P = 1 |
|
705 then (P, Frm) :: below |
|
706 else (*Trans*) below |
|
707 val levres = levfrm @ (if null below then [(P, Res)] else []) |
|
708 in |
|
709 get_allps (cuts @ levres) (lev_on P) pts |
|
710 end; |
|
711 |
|
712 (** these 2 funs decide on how far cut_tree goes **) |
|
713 (* shall the nodes _after_ the pos to be inserted at be deleted? |
|
714 shall cutting be continued on the higher level(s)? the Nd regarded will NOT be changed *) |
|
715 fun test_trans (PrfObj {branch, ...}) = (branch = TransitiveB orelse branch = NoBranch) |
|
716 | test_trans (PblObj {branch, ...}) = (branch = TransitiveB orelse branch = NoBranch); |
|
717 |
|
718 (* cut_bottom new sml603..608 |
|
719 cut the level at the bottom of the pos (used by cappend_...) |
|
720 and handle the parent in order to avoid extra case for root |
|
721 fn: ctree -> : the _whole_ ctree for cut_levup |
|
722 pos * Pos.posel -> : the pos after split_last |
|
723 ctree -> : the parent of the Nd to be cut |
|
724 return |
|
725 (ctree * : the updated ctree |
|
726 pos' list) * : the pos's cut |
|
727 bool : cutting shall be continued on the higher level(s) |
|
728 *) |
|
729 fun cut_bottom _ (pt' as Nd (b, [])) = ((pt', []), test_trans b) |
|
730 | cut_bottom (P, p) (Nd (b, bs)) = |
|
731 let (*divide level into 3 parts...*) |
|
732 val keep = take (p - 1, bs) |
|
733 val pt' = case nth p bs of |
|
734 pt' as Nd _ => pt' |
|
735 | _ => raise ERROR "cut_bottom: uncovered case nth p bs" |
|
736 (*^^^^^_here_ will be 'insert_pt'ed by 'append_..'*) |
|
737 val (tail, _) = (takerest (p, bs), if null (takerest (p, bs)) then 0 else p + 1) |
|
738 val (children, cuts) = |
|
739 if test_trans b |
|
740 then |
|
741 (keep, (if is_pblnd pt' then [(P @ [p], Pbl)] else []) |
|
742 @ (get_allp [] (P @ [p], (P, Frm)) pt') |
|
743 @ (get_allps [] (P @ [p + 1]) tail)) |
|
744 else (keep @ [(*'insert_pt'ed by 'append_..'*)] @ tail, |
|
745 get_allp [] (P @ [p], (P, Frm)) pt') |
|
746 val (pt'', cuts) = |
|
747 if test_trans b |
|
748 then (Nd (del_res b, children), cuts @ (if g_ostate b = Incomplete then [] else [(P, Res)])) |
|
749 else (Nd (b, children), cuts) |
|
750 in ((pt'', cuts), test_trans b) end |
|
751 | cut_bottom _ _ = raise ERROR "cut_bottom: uncovered fun def."; |
|
752 |
|
753 |
|
754 (* go all levels from the bottom of 'pos' up to the root, |
|
755 on each level compose the children of a node and accumulate the cut Nds |
|
756 args |
|
757 pos' list -> : for accumulation |
|
758 bool -> : cutting shall be continued on the higher level(s) |
|
759 ctree -> : the whole ctree for 'get_nd pt P' on each level |
|
760 ctree -> : the Nd from the lower level for insertion at path |
|
761 pos * Pos.posel -> : pos=path split for convenience |
|
762 ctree -> : Nd the children of are under consideration on this call |
|
763 returns : |
|
764 ctree * pos' list : the updated parent-Nd and the pos's of the Nds cut |
|
765 *) |
|
766 fun cut_levup (cuts:pos' list) clevup pt pt' (P:pos, p:Pos.posel) (Nd (b, bs)) = |
|
767 let (*divide level into 3 parts...*) |
|
768 val keep = take (p - 1, bs) |
|
769 (*val pt' comes as argument from below*) |
|
770 val (tail, _) = |
|
771 (takerest (p, bs), if null (takerest (p, bs)) then 0 else p + 1) |
|
772 val (children, cuts') = |
|
773 if clevup |
|
774 then (keep @ [pt'], get_allps [] (P @ [p+1]) tail) |
|
775 else (keep @ [pt'] @ tail, []) |
|
776 val clevup' = if clevup then test_trans b else false |
|
777 (*the first Nd with false stops cutting on all levels above*) |
|
778 val (pt'', cuts') = |
|
779 if clevup' |
|
780 then (Nd (del_res b, children), cuts' @ (if g_ostate b = Incomplete then [] else [(P, Res)])) |
|
781 else (Nd (b, children), cuts') |
|
782 in |
|
783 if null P |
|
784 then (pt'', cuts @ cuts') |
|
785 else |
|
786 let val (P, p) = split_last P |
|
787 in cut_levup (cuts @ cuts') clevup' pt pt'' (P, p) (get_nd pt P) end |
|
788 end |
|
789 | cut_levup _ _ _ _ _ _ = raise ERROR "cut_levup: uncovered fun def."; |
|
790 |
|
791 (* cut nodes after and below an inserted node in the ctree; |
|
792 the cuts range is limited by the predicate 'fun cutlevup' *) |
|
793 fun cut_tree pt (pos, _) = |
|
794 if not (existpt pos pt) |
|
795 then (pt, []) (*appending a formula never cuts anything*) |
|
796 else |
|
797 let |
|
798 val (P, p) = split_last pos |
|
799 val ((pt', cuts), clevup) = cut_bottom (P, p) (get_nd pt P) |
|
800 (* pt' is the updated parent of the Nd to cappend_..*) |
|
801 in |
|
802 if null P |
|
803 then (pt', cuts) |
|
804 else |
|
805 let val (P, p) = split_last P |
|
806 in cut_levup cuts clevup pt pt' (P, p) (get_nd pt P) end |
|
807 end; |
|
808 |
|
809 (* get the theory explicitly just for the rootpbl; |
|
810 thus use this function _after_ finishing specification *) |
|
811 fun root_thy (Nd (PblObj {spec = (thyID, _, _), ctxt, ...}, _)) = ThyC.get_theory ctxt thyID |
|
812 | root_thy _ = raise ERROR "root_thy: uncovered fun def."; |
|
813 |
|
814 (**) |
|
815 end; |
|
816 (**) |
|