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