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