neuper@37906
|
1 |
(* use"../ME/ctree.sml";
|
neuper@37906
|
2 |
use"ME/ctree.sml";
|
neuper@37906
|
3 |
use"ctree.sml";
|
neuper@37906
|
4 |
W.N.26.10.99
|
neuper@37906
|
5 |
|
neuper@37906
|
6 |
writeln (pr_ptree pr_short pt);
|
neuper@37906
|
7 |
|
neuper@37906
|
8 |
val Nd ( _, ns) = pt;
|
neuper@37906
|
9 |
|
neuper@37906
|
10 |
*)
|
neuper@37906
|
11 |
|
neuper@37906
|
12 |
(*structure Ptree (**): PTREE (**) = ###### outcommented ######*)
|
neuper@37906
|
13 |
signature PTREE =
|
neuper@37906
|
14 |
sig
|
neuper@37906
|
15 |
type ptree
|
neuper@37906
|
16 |
type envp
|
neuper@37906
|
17 |
val e_ptree : ptree
|
neuper@37906
|
18 |
exception PTREE of string
|
neuper@37906
|
19 |
type branch
|
neuper@37906
|
20 |
type ostate
|
neuper@37906
|
21 |
type cellID
|
neuper@37906
|
22 |
type cid
|
neuper@37906
|
23 |
type posel
|
neuper@37906
|
24 |
type pos
|
neuper@37906
|
25 |
type pos'
|
neuper@37906
|
26 |
type loc
|
neuper@37906
|
27 |
type domID
|
neuper@37906
|
28 |
type pblID
|
neuper@37906
|
29 |
type metID
|
neuper@37906
|
30 |
type spec
|
neuper@37906
|
31 |
type 'a ppc
|
neuper@37906
|
32 |
type con
|
neuper@37906
|
33 |
type subs
|
neuper@37906
|
34 |
type subst
|
neuper@37906
|
35 |
type env
|
neuper@37906
|
36 |
type ets
|
neuper@37906
|
37 |
val ets2str : ets -> string
|
neuper@37906
|
38 |
type item
|
neuper@37906
|
39 |
type tac
|
neuper@37906
|
40 |
type tac_
|
neuper@37906
|
41 |
val tac_2str : tac_ -> string
|
neuper@37906
|
42 |
type safe
|
neuper@37906
|
43 |
val safe2str : safe -> string
|
neuper@37906
|
44 |
|
neuper@37906
|
45 |
type meth
|
neuper@37906
|
46 |
val cappend_atomic : ptree -> pos -> loc -> cterm' -> tac
|
neuper@37906
|
47 |
-> cterm' -> ostate -> cid -> ptree * posel list * cid
|
neuper@37906
|
48 |
val cappend_form : ptree
|
neuper@37906
|
49 |
-> pos -> loc -> cterm' -> cid -> ptree * pos * cid
|
neuper@37906
|
50 |
val cappend_parent : ptree -> pos -> loc -> cterm' -> tac
|
neuper@37906
|
51 |
-> branch -> cid -> ptree * int list * cid
|
neuper@37906
|
52 |
val cappend_problem : ptree -> posel list(*FIXME*) -> loc
|
neuper@37906
|
53 |
-> cterm' list * spec -> cid -> ptree * int list * cellID list
|
neuper@37906
|
54 |
val append_result : ptree -> pos -> cterm' -> ostate -> ptree * pos
|
neuper@37906
|
55 |
|
neuper@37906
|
56 |
type ppobj
|
neuper@37906
|
57 |
val g_branch : ppobj -> branch
|
neuper@37906
|
58 |
val g_cell : ppobj -> cid
|
neuper@37906
|
59 |
val g_args : ppobj -> (int * (term list)) list (*args of scr*)
|
neuper@37906
|
60 |
val g_form : ppobj -> cterm'
|
neuper@37906
|
61 |
val g_loc : ppobj -> loc
|
neuper@37906
|
62 |
val g_met : ppobj -> meth
|
neuper@37906
|
63 |
val g_domID : ppobj -> domID
|
neuper@37906
|
64 |
val g_metID : ppobj -> metID
|
neuper@37906
|
65 |
val g_model : ppobj -> cterm' ppc
|
neuper@37906
|
66 |
val g_tac : ppobj -> tac
|
neuper@37906
|
67 |
val g_origin : ppobj -> cterm' list * spec
|
neuper@37906
|
68 |
val g_ostate : ppobj -> ostate
|
neuper@37906
|
69 |
val g_pbl : ppobj -> pblID * item ppc
|
neuper@37906
|
70 |
val g_result : ppobj -> cterm'
|
neuper@37906
|
71 |
val g_spec : ppobj -> spec
|
neuper@37906
|
72 |
(* val get_all : (ppobj -> 'a) -> ptree -> 'a list
|
neuper@37906
|
73 |
val get_alls : (ppobj -> 'a) -> ptree list -> 'a list *)
|
neuper@37906
|
74 |
val get_obj : (ppobj -> 'a) -> ptree -> pos -> 'a
|
neuper@37906
|
75 |
val gpt_cell : ptree -> cid
|
neuper@37906
|
76 |
val par_pblobj : ptree -> pos -> pos
|
neuper@37906
|
77 |
val pre_pos : pos -> pos
|
neuper@37906
|
78 |
val lev_dn : int list -> int list
|
neuper@37906
|
79 |
val lev_on : pos -> posel list
|
neuper@37906
|
80 |
val lev_pred : pos -> pos
|
neuper@37906
|
81 |
val lev_up : pos -> pos
|
neuper@37906
|
82 |
(* val pr_cell : pos -> ppobj -> string
|
neuper@37906
|
83 |
val pr_pos : int list -> string *)
|
neuper@37906
|
84 |
val pr_ptree : (pos -> ppobj -> string) -> ptree -> string
|
neuper@37906
|
85 |
val pr_short : pos -> ppobj -> string
|
neuper@37906
|
86 |
(* val repl : 'a list -> int -> 'a -> 'a list
|
neuper@37906
|
87 |
val repl_app : 'a list -> int -> 'a -> 'a list
|
neuper@37906
|
88 |
val repl_branch : branch -> ppobj -> ppobj
|
neuper@37906
|
89 |
val repl_domID : domID -> ppobj -> ppobj
|
neuper@37906
|
90 |
val repl_form : cterm' -> ppobj -> ppobj
|
neuper@37906
|
91 |
val repl_met : item ppc -> ppobj -> ppobj
|
neuper@37906
|
92 |
val repl_metID : metID -> ppobj -> ppobj
|
neuper@37906
|
93 |
val repl_model : cterm' list -> ppobj -> ppobj
|
neuper@37906
|
94 |
val repl_tac : tac -> ppobj -> ppobj
|
neuper@37906
|
95 |
val repl_pbl : item ppc -> ppobj -> ppobj
|
neuper@37906
|
96 |
val repl_pblID : pblID -> ppobj -> ppobj
|
neuper@37906
|
97 |
val repl_result : cterm' -> ostate -> ppobj -> ppobj
|
neuper@37906
|
98 |
val repl_spec : spec -> ppobj -> ppobj
|
neuper@37906
|
99 |
val repl_subs : (string * string) list -> ppobj -> ppobj *)
|
neuper@37906
|
100 |
val rootthy : ptree -> domID
|
neuper@37906
|
101 |
(* val test_trans : ppobj -> bool
|
neuper@37906
|
102 |
val uni__asm : (string * pos) list -> ppobj -> ppobj
|
neuper@37906
|
103 |
val uni__cid : cellID list -> ppobj -> ppobj *)
|
neuper@37906
|
104 |
val union_asm : ptree -> pos -> (string * pos) list -> ptree
|
neuper@37906
|
105 |
val union_cid : ptree -> pos -> cellID list -> ptree
|
neuper@37906
|
106 |
val update_branch : ptree -> pos -> branch -> ptree
|
neuper@37906
|
107 |
val update_domID : ptree -> pos -> domID -> ptree
|
neuper@37906
|
108 |
val update_met : ptree -> pos -> meth -> ptree
|
neuper@37906
|
109 |
val update_metppc : ptree -> pos -> item ppc -> ptree
|
neuper@37906
|
110 |
val update_metID : ptree -> pos -> metID -> ptree
|
neuper@37906
|
111 |
val update_tac : ptree -> pos -> tac -> ptree
|
neuper@37906
|
112 |
val update_pbl : ptree -> pos -> pblID * item ppc -> ptree
|
neuper@37906
|
113 |
val update_pblppc : ptree -> pos -> item ppc -> ptree
|
neuper@37906
|
114 |
val update_pblID : ptree -> pos -> pblID -> ptree
|
neuper@37906
|
115 |
val update_spec : ptree -> pos -> spec -> ptree
|
neuper@37906
|
116 |
val update_subs : ptree -> pos -> (string * string) list -> ptree
|
neuper@37906
|
117 |
|
neuper@37906
|
118 |
val rep_pblobj : ppobj
|
neuper@37906
|
119 |
-> {branch:branch, cell:cid, env:envp, loc:loc, meth:meth, model:cterm' ppc,
|
neuper@37906
|
120 |
origin:cterm' list * spec, ostate:ostate, probl:pblID * item ppc,
|
neuper@37906
|
121 |
result:cterm', spec:spec}
|
neuper@37906
|
122 |
val rep_prfobj : ppobj
|
neuper@37906
|
123 |
-> {branch:branch, cell:cid, form:cterm', loc:loc, tac:tac,
|
neuper@37906
|
124 |
ostate:ostate, result:cterm'}
|
neuper@37906
|
125 |
end
|
neuper@37906
|
126 |
|
neuper@37906
|
127 |
(* --------------
|
neuper@37906
|
128 |
structure Ptree (**): PTREE (**) =
|
neuper@37906
|
129 |
struct
|
neuper@37906
|
130 |
-------------- *)
|
neuper@37906
|
131 |
|
neuper@37906
|
132 |
type env = (term * term) list;
|
neuper@37906
|
133 |
|
neuper@37906
|
134 |
|
neuper@37906
|
135 |
datatype branch =
|
neuper@37906
|
136 |
NoBranch | AndB | OrB
|
neuper@37906
|
137 |
| TransitiveB (* FIXXXME.8.03: set branch from met in Apply_Method
|
neuper@37906
|
138 |
FIXXXME.0402: -"- in Begin_Trans'*)
|
neuper@37906
|
139 |
| SequenceB | IntersectB | CollectB | MapB;
|
neuper@37906
|
140 |
fun branch2str NoBranch = "NoBranch"
|
neuper@37906
|
141 |
| branch2str AndB = "AndB"
|
neuper@37906
|
142 |
| branch2str OrB = "OrB"
|
neuper@37906
|
143 |
| branch2str TransitiveB = "TransitiveB"
|
neuper@37906
|
144 |
| branch2str SequenceB = "SequenceB"
|
neuper@37906
|
145 |
| branch2str IntersectB = "IntersectB"
|
neuper@37906
|
146 |
| branch2str CollectB = "CollectB"
|
neuper@37906
|
147 |
| branch2str MapB = "MapB";
|
neuper@37906
|
148 |
|
neuper@37906
|
149 |
datatype ostate =
|
neuper@37906
|
150 |
Incomplete | Complete | Inconsistent(*WN041020 latter unused*);
|
neuper@37906
|
151 |
fun ostate2str Incomplete = "Incomplete"
|
neuper@37906
|
152 |
| ostate2str Complete = "Complete"
|
neuper@37906
|
153 |
| ostate2str Inconsistent = "Inconsistent";
|
neuper@37906
|
154 |
|
neuper@37906
|
155 |
type cellID = int;
|
neuper@37906
|
156 |
type cid = cellID list;
|
neuper@37906
|
157 |
|
neuper@37906
|
158 |
type posel = int; (* roundabout for (some of) nice signatures *)
|
neuper@37906
|
159 |
type pos = posel list;
|
neuper@37906
|
160 |
val pos2str = ints2str';
|
neuper@37906
|
161 |
datatype pos_ =
|
neuper@37906
|
162 |
Pbl (*PblObj-position: problem-type*)
|
neuper@37906
|
163 |
| Met (*PblObj-position: method*)
|
neuper@37906
|
164 |
| Frm (*PblObj-position: -> Pbl in ME (not by moveDown !)
|
neuper@37906
|
165 |
| PrfObj-position: formula*)
|
neuper@37906
|
166 |
| Res (*PblObj | PrfObj-position: result*)
|
neuper@37906
|
167 |
| Und; (*undefined*)
|
neuper@37906
|
168 |
fun pos_2str Pbl = "Pbl"
|
neuper@37906
|
169 |
| pos_2str Met = "Met"
|
neuper@37906
|
170 |
| pos_2str Frm = "Frm"
|
neuper@37906
|
171 |
| pos_2str Res = "Res"
|
neuper@37906
|
172 |
| pos_2str Und = "Und";
|
neuper@37906
|
173 |
|
neuper@37906
|
174 |
type pos' = pos * pos_;
|
neuper@37906
|
175 |
(*WN.12.03 remembering interator (pos * pos_) for ptree
|
neuper@37906
|
176 |
pos : lev_on, lev_dn, lev_up,
|
neuper@37906
|
177 |
lev_onFrm, lev_dnRes (..see solve Apply_Method !)
|
neuper@37906
|
178 |
pos_:
|
neuper@37906
|
179 |
# generate1 sets pos_ if possible ...?WN0502?NOT...
|
neuper@37906
|
180 |
# generate1 does NOT set pos, because certain nodes can be lev_on OR lev_dn
|
neuper@37906
|
181 |
exceptions: Begin/End_Trans
|
neuper@37906
|
182 |
# thus generate(1) called in
|
neuper@37906
|
183 |
.# assy, locate_gen
|
neuper@37906
|
184 |
.# nxt_solv (tac_ -cases); general case:
|
neuper@37906
|
185 |
val pos' = case pos' of (p,Res) => (lev_on p',Res) | _ => pos'
|
neuper@37906
|
186 |
# WN050220, S(604):
|
neuper@37906
|
187 |
generate1...(Rewrite(f,..,res))..(pos, pos_)
|
neuper@37906
|
188 |
cappend_atomic.................pos ////// gets f+res always!!!
|
neuper@37906
|
189 |
cut_tree....................pos, pos_
|
neuper@37906
|
190 |
*)
|
neuper@37906
|
191 |
fun pos'2str (p,p_) = pair2str (ints2str' p, pos_2str p_);
|
neuper@37906
|
192 |
fun pos's2str ps = (strs2str' o (map pos'2str)) ps;
|
neuper@37906
|
193 |
val e_pos' = ([],Und):pos';
|
neuper@37906
|
194 |
|
neuper@37906
|
195 |
fun res2str (t, ts) = pair2str (term2str t, terms2str ts);
|
neuper@37906
|
196 |
fun asm2str (t, p:pos) = pair2str (term2str t, ints2str' p);
|
neuper@37906
|
197 |
fun asms2str asms = (strs2str' o (map asm2str)) asms;
|
neuper@37906
|
198 |
|
neuper@37906
|
199 |
|
neuper@37906
|
200 |
|
neuper@37906
|
201 |
(*26.4.02: never used after introduction of scripts !!!
|
neuper@37906
|
202 |
type loc = loc_ * (* + interpreter-state *)
|
neuper@37906
|
203 |
(loc_ * rls') (* -"- for script of the ruleset*)
|
neuper@37906
|
204 |
option;
|
neuper@37906
|
205 |
val e_loc = ([],None):loc;
|
neuper@37906
|
206 |
val ee_loc = (e_loc,e_loc);*)
|
neuper@37906
|
207 |
|
neuper@37906
|
208 |
|
neuper@37906
|
209 |
datatype safe = Sundef | Safe | Unsafe | Helpless;
|
neuper@37906
|
210 |
fun safe2str Sundef = "Sundef"
|
neuper@37906
|
211 |
| safe2str Safe = "Safe"
|
neuper@37906
|
212 |
| safe2str Unsafe = "Unsafe"
|
neuper@37906
|
213 |
| safe2str Helpless = "Helpless";
|
neuper@37906
|
214 |
|
neuper@37906
|
215 |
type subs = cterm' list; (*16.11.00 for FE-KE*)
|
neuper@37906
|
216 |
val e_subs = ["(bdv, x)"];
|
neuper@37906
|
217 |
|
neuper@37906
|
218 |
(*._sub_stitution as strings of _e_qualities.*)
|
neuper@37906
|
219 |
type sube = cterm' list;
|
neuper@37906
|
220 |
val e_sube = []:cterm' list;
|
neuper@37906
|
221 |
fun sube2str s = strs2str s;
|
neuper@37906
|
222 |
|
neuper@37906
|
223 |
(*._sub_stitution as _t_erms of _e_qualities.*)
|
neuper@37906
|
224 |
type subte = term list;
|
neuper@37906
|
225 |
val e_subte = []:term list;
|
neuper@37906
|
226 |
fun subte2str ss = terms2str ss;
|
neuper@37906
|
227 |
|
neuper@37906
|
228 |
fun subte2sube ss = map term2str ss;
|
neuper@37906
|
229 |
|
neuper@37906
|
230 |
(*fun subst2str' thy' (s:subst) =
|
neuper@37906
|
231 |
(strs2str o
|
neuper@37906
|
232 |
(map (pair2str o
|
neuper@37906
|
233 |
(apsnd (Sign.string_of_term (sign_of (assoc_thy thy')))) o
|
neuper@37906
|
234 |
(apfst (Sign.string_of_term (sign_of (assoc_thy thy'))))))) s;*)
|
neuper@37906
|
235 |
fun subst2subs s = map (pair2str o
|
neuper@37925
|
236 |
(apfst (Syntax.string_of_term (ctxt_Isac""))) o
|
neuper@37925
|
237 |
(apsnd (Syntax.string_of_term (ctxt_Isac"")))) s;
|
neuper@37925
|
238 |
fun subst2subs' s = map ((apfst (Syntax.string_of_term (ctxt_Isac""))) o
|
neuper@37925
|
239 |
(apsnd (Syntax.string_of_term (ctxt_Isac"")))) s;
|
neuper@37906
|
240 |
fun subs2subst thy s = map (isapair2pair o term_of o the o (parse thy)) s;
|
neuper@37906
|
241 |
(*> subs2subst thy ["(bdv,x)","(err,#0)"];
|
neuper@37906
|
242 |
val it =
|
neuper@37906
|
243 |
[(Free ("bdv","RealDef.real"),Free ("x","RealDef.real")),
|
neuper@37906
|
244 |
(Free ("err","RealDef.real"),Free ("#0","RealDef.real"))]
|
neuper@37906
|
245 |
: (term * term) list*)
|
neuper@37906
|
246 |
(*["bdv=x","err=0"] ---> [(bdv,x), (err,0)]*)
|
neuper@37906
|
247 |
fun sube2subst thy s = map (dest_equals' o term_of o the o (parse thy)) s;
|
neuper@37906
|
248 |
(* val ts = sube2subst thy ["bdv=x","err=0"];
|
neuper@37906
|
249 |
subst2str' ts;
|
neuper@37906
|
250 |
*)
|
neuper@37906
|
251 |
fun sube2subte ss = map str2term ss;
|
neuper@37906
|
252 |
|
neuper@37906
|
253 |
|
neuper@37906
|
254 |
fun isasub2subst isasub = ((map isapair2pair) o isalist2list) isasub;
|
neuper@37906
|
255 |
|
neuper@37906
|
256 |
|
neuper@37906
|
257 |
type scrstate = (*state for script interpreter*)
|
neuper@37906
|
258 |
env(*stack*) (*used to instantiate tac for checking assod
|
neuper@37906
|
259 |
12.03.noticed: e_ not updated during execution ?!?*)
|
neuper@37906
|
260 |
* loc_ (*location of tac in script*)
|
neuper@37906
|
261 |
* term option(*argument of curried functions*)
|
neuper@37906
|
262 |
* term (*value obtained by tac executed
|
neuper@37906
|
263 |
updated also after a derivation by 'new_val'*)
|
neuper@37906
|
264 |
* safe (*estimation of how result will be obtained*)
|
neuper@37906
|
265 |
* bool; (*true = strongly .., false = weakly associated:
|
neuper@37906
|
266 |
only used during ass_dn/up*)
|
neuper@37925
|
267 |
val e_scrstate = ([],[],NONE,e_term,Sundef,false):scrstate;
|
neuper@37906
|
268 |
|
neuper@37906
|
269 |
|
neuper@37906
|
270 |
(*21.8.02 ---> definitions.sml for datatype scr
|
neuper@37906
|
271 |
type rrlsstate = (*state for reverse rewriting*)
|
neuper@37906
|
272 |
(term * (*the current formula*)
|
neuper@37906
|
273 |
rule list (*of reverse rewrite set (#1#)*)
|
neuper@37906
|
274 |
list * (*may be serveral, eg. in norm_rational*)
|
neuper@37906
|
275 |
(rule * (*Thm (+ Thm generated from Calc) resulting in ...*)
|
neuper@37906
|
276 |
(term * (*... rewrite with ...*)
|
neuper@37906
|
277 |
term list)) (*... assumptions*)
|
neuper@37906
|
278 |
list); (*derivation from given term to normalform
|
neuper@37906
|
279 |
in reverse order with sym_thm;
|
neuper@37906
|
280 |
(#1#) could be extracted from here #1*) --------*)
|
neuper@37906
|
281 |
|
neuper@37906
|
282 |
datatype istate = (*interpreter state*)
|
neuper@37906
|
283 |
Uistate (*undefined in modspec, in '_deriv'ation*)
|
neuper@37906
|
284 |
| ScrState of scrstate (*for script interpreter*)
|
neuper@37906
|
285 |
| RrlsState of rrlsstate; (*for reverse rewriting*)
|
neuper@37925
|
286 |
val e_istate = (ScrState ([],[],NONE,e_term,Sundef,false)):istate;
|
neuper@37906
|
287 |
|
neuper@37906
|
288 |
type iist = istate option * istate option;
|
neuper@37906
|
289 |
(*val e_iist = (e_istate, e_istate); --- sinnlos f"ur NICHT-equality-type*)
|
neuper@37906
|
290 |
|
neuper@37906
|
291 |
|
neuper@37906
|
292 |
fun rta2str (r,(t,a)) = "\n("^(rule2str r)^",("^(term2str t)^", "^
|
neuper@37906
|
293 |
(terms2str a)^"))";
|
neuper@37906
|
294 |
fun istate2str Uistate = "Uistate"
|
neuper@37906
|
295 |
| istate2str (ScrState (e,l,to,t,s,b):istate) =
|
neuper@37906
|
296 |
"ScrState ("^ subst2str e ^",\n "^
|
neuper@37906
|
297 |
loc_2str l ^", "^ termopt2str to ^",\n "^
|
neuper@37906
|
298 |
term2str t ^", "^ safe2str s ^", "^ bool2str b ^")"
|
neuper@37906
|
299 |
| istate2str (RrlsState (t,t1,rss,rtas)) =
|
neuper@37906
|
300 |
"RrlsState ("^(term2str t)^", "^(term2str t1)^", "^
|
neuper@37906
|
301 |
((strs2str o (map (strs2str o (map rule2str)))) rss)^", "^
|
neuper@37906
|
302 |
((strs2str o (map rta2str)) rtas)^")";
|
neuper@37925
|
303 |
fun istates2str (NONE, NONE) = "(#NONE, #NONE)"
|
neuper@37925
|
304 |
| istates2str (NONE, SOME ist) = "(#NONE,\n#SOME "^istate2str ist^")"
|
neuper@37925
|
305 |
| istates2str (SOME ist, NONE) = "(#SOME "^istate2str ist^",\n #NONE)"
|
neuper@37925
|
306 |
| istates2str (SOME i1, SOME i2) = "(#SOME "^istate2str i1^",\n #SOME "^
|
neuper@37906
|
307 |
istate2str i2^")";
|
neuper@37906
|
308 |
|
neuper@37906
|
309 |
fun new_val v (ScrState (env, loc_, topt, _, safe, bool)) =
|
neuper@37906
|
310 |
(ScrState (env, loc_, topt, v, safe, bool))
|
neuper@37906
|
311 |
| new_val _ _ = raise error "new_val: only for ScrState";
|
neuper@37906
|
312 |
|
neuper@37906
|
313 |
datatype con = land | lor;
|
neuper@37906
|
314 |
|
neuper@37906
|
315 |
|
neuper@37906
|
316 |
type spec =
|
neuper@37906
|
317 |
domID * (*WN.12.03: is replaced by thy from get_met ?FIXME? in:
|
neuper@37906
|
318 |
specify (Init_Proof..), nxt_specify_init_calc,
|
neuper@37906
|
319 |
assod (.SubProblem...), stac2tac (.SubProblem...)*)
|
neuper@37906
|
320 |
pblID *
|
neuper@37906
|
321 |
metID;
|
neuper@37906
|
322 |
fun spec2str ((dom,pbl,met)(*:spec*)) =
|
neuper@37906
|
323 |
"(" ^ (quote dom) ^ ", " ^ (strs2str pbl) ^
|
neuper@37906
|
324 |
", " ^ (strs2str met) ^ ")";
|
neuper@37906
|
325 |
(*> spec2str empty_spec;
|
neuper@37906
|
326 |
val it = "(\"\", [], (\"\", \"\"))" : string *)
|
neuper@37906
|
327 |
val empty_spec = (e_domID,e_pblID,e_metID):spec;
|
neuper@37906
|
328 |
val e_spec = empty_spec;
|
neuper@37906
|
329 |
|
neuper@37906
|
330 |
|
neuper@37906
|
331 |
|
neuper@37906
|
332 |
(*.tactics propagate the construction of the calc-tree;
|
neuper@37906
|
333 |
there are
|
neuper@37906
|
334 |
(a) 'specsteps' for the specify-phase, and others for the solve-phase
|
neuper@37906
|
335 |
(b) those of the solve-phase are 'initac's and others;
|
neuper@37906
|
336 |
initacs start with a formula different from the preceding formula.
|
neuper@37906
|
337 |
see 'type tac_' for the internal representation of tactics.*)
|
neuper@37906
|
338 |
datatype tac =
|
neuper@37906
|
339 |
Init_Proof of ((cterm' list) * spec)
|
neuper@37906
|
340 |
(*'specsteps'...*)
|
neuper@37906
|
341 |
| Model_Problem
|
neuper@37906
|
342 |
| Refine_Problem of pblID | Refine_Tacitly of pblID
|
neuper@37906
|
343 |
|
neuper@37906
|
344 |
| Add_Given of cterm' | Del_Given of cterm'
|
neuper@37906
|
345 |
| Add_Find of cterm' | Del_Find of cterm'
|
neuper@37906
|
346 |
| Add_Relation of cterm' | Del_Relation of cterm'
|
neuper@37906
|
347 |
|
neuper@37906
|
348 |
| Specify_Theory of domID | Specify_Problem of pblID
|
neuper@37906
|
349 |
| Specify_Method of metID
|
neuper@37906
|
350 |
(*...'specsteps'*)
|
neuper@37906
|
351 |
| Apply_Method of metID
|
neuper@37906
|
352 |
(*.creates an 'istate' in PblObj.env; in case of 'init_form'
|
neuper@37906
|
353 |
creates a formula at ((lev_on o lev_dn) p, Frm) and in this ppobj.'loc'
|
neuper@37925
|
354 |
'SOME istate' (at fst of 'loc').
|
neuper@37906
|
355 |
As each step (in the solve-phase) has a resulting formula (at the front-end)
|
neuper@37906
|
356 |
Apply_Method also does the 1st step in the script (an 'initac') if there
|
neuper@37906
|
357 |
is no 'init_form' .*)
|
neuper@37906
|
358 |
| Check_Postcond of pblID
|
neuper@37906
|
359 |
| Free_Solve
|
neuper@37906
|
360 |
|
neuper@37906
|
361 |
| Rewrite_Inst of ( subs * thm') | Rewrite of thm'
|
neuper@37906
|
362 |
| Rewrite_Asm of thm'
|
neuper@37906
|
363 |
| Rewrite_Set_Inst of ( subs * rls') | Rewrite_Set of rls'
|
neuper@37906
|
364 |
| Detail_Set_Inst of ( subs * rls') | Detail_Set of rls'
|
neuper@37906
|
365 |
| End_Detail (*end of script from next_tac,
|
neuper@37906
|
366 |
in solve: switches back to parent script WN0509 drop!*)
|
neuper@37906
|
367 |
| Derive of rls' (*an input formula using rls WN0509 drop!*)
|
neuper@37906
|
368 |
| Calculate of string (* plus | minus | times | cancel | pow | sqrt *)
|
neuper@37906
|
369 |
| End_Ruleset
|
neuper@37906
|
370 |
| Substitute of sube | Apply_Assumption of cterm' list
|
neuper@37906
|
371 |
|
neuper@37906
|
372 |
| Take of cterm' (*an 'initac'*)
|
neuper@37906
|
373 |
| Take_Inst of cterm'
|
neuper@37906
|
374 |
| Group of (con * int list )
|
neuper@37906
|
375 |
| Subproblem of (domID * pblID) (*an 'initac'*)
|
neuper@37906
|
376 |
| CAScmd of cterm' (*6.6.02 URD: Function formula; WN0509 drop!*)
|
neuper@37906
|
377 |
| End_Subproblem (*WN0509 drop!*)
|
neuper@37906
|
378 |
|
neuper@37906
|
379 |
| Split_And | Conclude_And
|
neuper@37906
|
380 |
| Split_Or | Conclude_Or
|
neuper@37906
|
381 |
| Begin_Trans | End_Trans
|
neuper@37906
|
382 |
| Begin_Sequ | End_Sequ(* substitute root.env *)
|
neuper@37906
|
383 |
| Split_Intersect | End_Intersect
|
neuper@37906
|
384 |
| Check_elementwise of cterm' | Collect_Trues
|
neuper@37906
|
385 |
| Or_to_List
|
neuper@37906
|
386 |
|
neuper@37906
|
387 |
| Empty_Tac (*TODO.11.6.03 ... of string: could carry msg of (Notappl msg)
|
neuper@37906
|
388 |
in 'helpless'*)
|
neuper@37906
|
389 |
| Tac of string(* eg.'repeat'*WN0509 drop!*)
|
neuper@37906
|
390 |
| User (*internal, for ets*WN0509 drop!*)
|
neuper@37906
|
391 |
| End_Proof';(* inout*)
|
neuper@37906
|
392 |
|
neuper@37906
|
393 |
(* tac2str /--> library.sml: needed in dialog.sml for 'separable *)
|
neuper@37906
|
394 |
fun tac2str (ma:tac) = case ma of
|
neuper@37906
|
395 |
Init_Proof (ppc, spec) =>
|
neuper@37906
|
396 |
"Init_Proof "^(pair2str (strs2str ppc, spec2str spec))
|
neuper@37906
|
397 |
| Model_Problem => "Model_Problem "
|
neuper@37906
|
398 |
| Refine_Tacitly pblID => "Refine_Tacitly "^(strs2str pblID)
|
neuper@37906
|
399 |
| Refine_Problem pblID => "Refine_Problem "^(strs2str pblID)
|
neuper@37906
|
400 |
| Add_Given cterm' => "Add_Given "^cterm'
|
neuper@37906
|
401 |
| Del_Given cterm' => "Del_Given "^cterm'
|
neuper@37906
|
402 |
| Add_Find cterm' => "Add_Find "^cterm'
|
neuper@37906
|
403 |
| Del_Find cterm' => "Del_Find "^cterm'
|
neuper@37906
|
404 |
| Add_Relation cterm' => "Add_Relation "^cterm'
|
neuper@37906
|
405 |
| Del_Relation cterm' => "Del_Relation "^cterm'
|
neuper@37906
|
406 |
|
neuper@37906
|
407 |
| Specify_Theory domID => "Specify_Theory "^(quote domID )
|
neuper@37906
|
408 |
| Specify_Problem pblID => "Specify_Problem "^(strs2str pblID )
|
neuper@37906
|
409 |
| Specify_Method metID => "Specify_Method "^(strs2str metID)
|
neuper@37906
|
410 |
| Apply_Method metID => "Apply_Method "^(strs2str metID)
|
neuper@37906
|
411 |
| Check_Postcond pblID => "Check_Postcond "^(strs2str pblID)
|
neuper@37906
|
412 |
| Free_Solve => "Free_Solve"
|
neuper@37906
|
413 |
|
neuper@37906
|
414 |
| Rewrite_Inst (subs,thm')=>
|
neuper@37906
|
415 |
"Rewrite_Inst "^(pair2str (subs2str subs, spair2str thm'))
|
neuper@37906
|
416 |
| Rewrite thm' => "Rewrite "^(spair2str thm')
|
neuper@37906
|
417 |
| Rewrite_Asm thm' => "Rewrite_Asm "^(spair2str thm')
|
neuper@37906
|
418 |
| Rewrite_Set_Inst (subs, rls) =>
|
neuper@37906
|
419 |
"Rewrite_Set_Inst "^(pair2str (subs2str subs, quote rls))
|
neuper@37906
|
420 |
| Rewrite_Set rls => "Rewrite_Set "^(quote rls )
|
neuper@37906
|
421 |
| Detail_Set rls => "Detail_Set "^(quote rls )
|
neuper@37906
|
422 |
| Detail_Set_Inst (subs, rls) =>
|
neuper@37906
|
423 |
"Detail_Set_Inst "^(pair2str (subs2str subs, quote rls))
|
neuper@37906
|
424 |
| End_Detail => "End_Detail"
|
neuper@37906
|
425 |
| Derive rls' => "Derive "^rls'
|
neuper@37906
|
426 |
| Calculate op_ => "Calculate "^op_
|
neuper@37906
|
427 |
| Substitute sube => "Substitute "^sube2str sube
|
neuper@37906
|
428 |
| Apply_Assumption ct's => "Apply_Assumption "^(strs2str ct's)
|
neuper@37906
|
429 |
|
neuper@37906
|
430 |
| Take cterm' => "Take "^(quote cterm' )
|
neuper@37906
|
431 |
| Take_Inst cterm' => "Take_Inst "^(quote cterm' )
|
neuper@37906
|
432 |
| Group (con, ints) =>
|
neuper@37906
|
433 |
"Group "^(pair2str (con2str con, ints2str ints))
|
neuper@37906
|
434 |
| Subproblem (domID, pblID) =>
|
neuper@37906
|
435 |
"Subproblem "^(pair2str (domID, strs2str pblID))
|
neuper@37906
|
436 |
(*| Subproblem_Full (spec, cts') =>
|
neuper@37906
|
437 |
"Subproblem_Full "^(pair2str (spec2str spec, strs2str cts'))*)
|
neuper@37906
|
438 |
| End_Subproblem => "End_Subproblem"
|
neuper@37906
|
439 |
| CAScmd cterm' => "CAScmd "^(quote cterm')
|
neuper@37906
|
440 |
|
neuper@37906
|
441 |
| Check_elementwise cterm'=> "Check_elementwise "^(quote cterm')
|
neuper@37906
|
442 |
| Or_to_List => "Or_to_List "
|
neuper@37906
|
443 |
| Collect_Trues => "Collect_Trues"
|
neuper@37906
|
444 |
|
neuper@37906
|
445 |
| Empty_Tac => "Empty_Tac"
|
neuper@37906
|
446 |
| Tac string => "Tac "^string
|
neuper@37906
|
447 |
| User => "User"
|
neuper@37906
|
448 |
| End_Proof' => "tac End_Proof'"
|
neuper@37906
|
449 |
| _ => "tac2str not impl. for ?!";
|
neuper@37906
|
450 |
|
neuper@37906
|
451 |
fun is_rewset (Rewrite_Set_Inst _) = true
|
neuper@37906
|
452 |
| is_rewset (Rewrite_Set _) = true
|
neuper@37906
|
453 |
| is_rewset _ = false;
|
neuper@37906
|
454 |
fun is_rewtac (Rewrite _) = true
|
neuper@37906
|
455 |
| is_rewtac (Rewrite_Inst _) = true
|
neuper@37906
|
456 |
| is_rewtac (Rewrite_Asm _) = true
|
neuper@37906
|
457 |
| is_rewtac tac = is_rewset tac;
|
neuper@37906
|
458 |
|
neuper@37906
|
459 |
fun tac2IDstr (ma:tac) = case ma of
|
neuper@37906
|
460 |
Model_Problem => "Model_Problem"
|
neuper@37906
|
461 |
| Refine_Tacitly pblID => "Refine_Tacitly"
|
neuper@37906
|
462 |
| Refine_Problem pblID => "Refine_Problem"
|
neuper@37906
|
463 |
| Add_Given cterm' => "Add_Given"
|
neuper@37906
|
464 |
| Del_Given cterm' => "Del_Given"
|
neuper@37906
|
465 |
| Add_Find cterm' => "Add_Find"
|
neuper@37906
|
466 |
| Del_Find cterm' => "Del_Find"
|
neuper@37906
|
467 |
| Add_Relation cterm' => "Add_Relation"
|
neuper@37906
|
468 |
| Del_Relation cterm' => "Del_Relation"
|
neuper@37906
|
469 |
|
neuper@37906
|
470 |
| Specify_Theory domID => "Specify_Theory"
|
neuper@37906
|
471 |
| Specify_Problem pblID => "Specify_Problem"
|
neuper@37906
|
472 |
| Specify_Method metID => "Specify_Method"
|
neuper@37906
|
473 |
| Apply_Method metID => "Apply_Method"
|
neuper@37906
|
474 |
| Check_Postcond pblID => "Check_Postcond"
|
neuper@37906
|
475 |
| Free_Solve => "Free_Solve"
|
neuper@37906
|
476 |
|
neuper@37906
|
477 |
| Rewrite_Inst (subs,thm')=> "Rewrite_Inst"
|
neuper@37906
|
478 |
| Rewrite thm' => "Rewrite"
|
neuper@37906
|
479 |
| Rewrite_Asm thm' => "Rewrite_Asm"
|
neuper@37906
|
480 |
| Rewrite_Set_Inst (subs, rls) => "Rewrite_Set_Inst"
|
neuper@37906
|
481 |
| Rewrite_Set rls => "Rewrite_Set"
|
neuper@37906
|
482 |
| Detail_Set rls => "Detail_Set"
|
neuper@37906
|
483 |
| Detail_Set_Inst (subs, rls) => "Detail_Set_Inst"
|
neuper@37906
|
484 |
| Derive rls' => "Derive "
|
neuper@37906
|
485 |
| Calculate op_ => "Calculate "
|
neuper@37906
|
486 |
| Substitute subs => "Substitute"
|
neuper@37906
|
487 |
| Apply_Assumption ct's => "Apply_Assumption"
|
neuper@37906
|
488 |
|
neuper@37906
|
489 |
| Take cterm' => "Take"
|
neuper@37906
|
490 |
| Take_Inst cterm' => "Take_Inst"
|
neuper@37906
|
491 |
| Group (con, ints) => "Group"
|
neuper@37906
|
492 |
| Subproblem (domID, pblID) => "Subproblem"
|
neuper@37906
|
493 |
| End_Subproblem => "End_Subproblem"
|
neuper@37906
|
494 |
| CAScmd cterm' => "CAScmd"
|
neuper@37906
|
495 |
|
neuper@37906
|
496 |
| Check_elementwise cterm'=> "Check_elementwise"
|
neuper@37906
|
497 |
| Or_to_List => "Or_to_List "
|
neuper@37906
|
498 |
| Collect_Trues => "Collect_Trues"
|
neuper@37906
|
499 |
|
neuper@37906
|
500 |
| Empty_Tac => "Empty_Tac"
|
neuper@37906
|
501 |
| Tac string => "Tac "
|
neuper@37906
|
502 |
| User => "User"
|
neuper@37906
|
503 |
| End_Proof' => "End_Proof'"
|
neuper@37906
|
504 |
| _ => "tac2str not impl. for ?!";
|
neuper@37906
|
505 |
|
neuper@37906
|
506 |
fun rls_of (Rewrite_Set_Inst (_, rls)) = rls
|
neuper@37906
|
507 |
| rls_of (Rewrite_Set rls) = rls
|
neuper@37906
|
508 |
| rls_of tac = raise error ("rls_of: called with tac '"^tac2IDstr tac^"'");
|
neuper@37906
|
509 |
|
neuper@37906
|
510 |
fun thm_of_rew (Rewrite_Inst (subs,(thmID,_))) =
|
neuper@37925
|
511 |
(thmID, SOME ((subs2subst (assoc_thy "Isac.thy") subs):subst))
|
neuper@37925
|
512 |
| thm_of_rew (Rewrite (thmID,_)) = (thmID, NONE)
|
neuper@37925
|
513 |
| thm_of_rew (Rewrite_Asm (thmID,_)) = (thmID, NONE);
|
neuper@37906
|
514 |
|
neuper@37906
|
515 |
fun rls_of_rewset (Rewrite_Set_Inst (subs,rls)) =
|
neuper@37925
|
516 |
(rls, SOME ((subs2subst (assoc_thy "Isac.thy") subs):subst))
|
neuper@37925
|
517 |
| rls_of_rewset (Rewrite_Set rls) = (rls, NONE)
|
neuper@37925
|
518 |
| rls_of_rewset (Detail_Set rls) = (rls, NONE)
|
neuper@37906
|
519 |
| rls_of_rewset (Detail_Set_Inst (subs, rls)) =
|
neuper@37925
|
520 |
(rls, SOME ((subs2subst (assoc_thy "Isac.thy") subs):subst));
|
neuper@37906
|
521 |
|
neuper@37906
|
522 |
fun rule2tac _ (Calc (opID, thm)) = Calculate (calID2calcID opID)
|
neuper@37906
|
523 |
| rule2tac [] (Thm (thmID, thm)) = Rewrite (thmID, string_of_thmI thm)
|
neuper@37906
|
524 |
| rule2tac subst (Thm (thmID, thm)) =
|
neuper@37906
|
525 |
Rewrite_Inst (subst2subs subst, (thmID, string_of_thmI thm))
|
neuper@37906
|
526 |
| rule2tac [] (Rls_ rls) = Rewrite_Set (id_rls rls)
|
neuper@37906
|
527 |
| rule2tac subst (Rls_ rls) =
|
neuper@37906
|
528 |
Rewrite_Set_Inst (subst2subs subst, (id_rls rls))
|
neuper@37906
|
529 |
| rule2tac _ rule =
|
neuper@37906
|
530 |
raise error ("rule2tac: called with '" ^ rule2str rule ^ "'");
|
neuper@37906
|
531 |
|
neuper@37906
|
532 |
type fmz_ = cterm' list;
|
neuper@37906
|
533 |
|
neuper@37906
|
534 |
(*.a formalization of an example containing data
|
neuper@37906
|
535 |
sufficient for mechanically finding the solution for the example.*)
|
neuper@37906
|
536 |
(*FIXME.WN051014: dont store fmz = (_,spec) in the PblObj,
|
neuper@37906
|
537 |
this is done in origin*)
|
neuper@37906
|
538 |
type fmz = fmz_ * spec;
|
neuper@37906
|
539 |
val e_fmz = ([],e_spec);
|
neuper@37906
|
540 |
|
neuper@37906
|
541 |
(*tac_ is made from tac in applicable_in,
|
neuper@37906
|
542 |
and carries all data necessary for generate;*)
|
neuper@37906
|
543 |
datatype tac_ =
|
neuper@37906
|
544 |
(* datatype tac = *)
|
neuper@37906
|
545 |
Init_Proof' of ((cterm' list) * spec)
|
neuper@37906
|
546 |
(* ori list !: code specify -> applicable*)
|
neuper@37906
|
547 |
| Model_Problem' of pblID *
|
neuper@37906
|
548 |
itm list * (*the 'untouched' pbl*)
|
neuper@37906
|
549 |
itm list (*the casually completed met*)
|
neuper@37906
|
550 |
| Refine_Tacitly' of pblID * (*input*)
|
neuper@37906
|
551 |
pblID * (*the refined from applicable_in*)
|
neuper@37906
|
552 |
domID * (*from new pbt?! filled in specify*)
|
neuper@37906
|
553 |
metID * (*from new pbt?! filled in specify*)
|
neuper@37906
|
554 |
itm list (*drop ! 9.03: remains [] for
|
neuper@37906
|
555 |
Model_Problem recognizing its activation*)
|
neuper@37906
|
556 |
| Refine_Problem' of (pblID * (itm list * (bool * Term.term) list))
|
neuper@37906
|
557 |
(*FIXME?040215 drop: done automatically in init_proof + Subproblem'*)
|
neuper@37906
|
558 |
| Add_Given' of cterm' *
|
neuper@37906
|
559 |
itm list (*updated with input in fun specify_additem*)
|
neuper@37906
|
560 |
| Add_Find' of cterm' *
|
neuper@37906
|
561 |
itm list (*updated with input in fun specify_additem*)
|
neuper@37906
|
562 |
| Add_Relation' of cterm' *
|
neuper@37906
|
563 |
itm list (*updated with input in fun specify_additem*)
|
neuper@37906
|
564 |
| Del_Given' of cterm' | Del_Find' of cterm' | Del_Relation' of cterm'
|
neuper@37906
|
565 |
(*4.00.: all.. term: in applicable_in ..? Syn ?only for FormFK?*)
|
neuper@37906
|
566 |
|
neuper@37906
|
567 |
| Specify_Theory' of domID
|
neuper@37906
|
568 |
| Specify_Problem' of (pblID * (* *)
|
neuper@37906
|
569 |
(bool * (* matches *)
|
neuper@37906
|
570 |
(itm list * (* ppc *)
|
neuper@37906
|
571 |
(bool * term) list))) (* preconditions *)
|
neuper@37906
|
572 |
| Specify_Method' of metID *
|
neuper@37906
|
573 |
ori list * (*repl. "#undef"*)
|
neuper@37906
|
574 |
itm list (*... updated from pbl to met*)
|
neuper@37906
|
575 |
| Apply_Method' of metID *
|
neuper@37906
|
576 |
(term option) * (*init_form*)
|
neuper@37906
|
577 |
istate
|
neuper@37906
|
578 |
| Check_Postcond' of
|
neuper@37906
|
579 |
pblID *
|
neuper@37906
|
580 |
(term * (*returnvalue of script in solve*)
|
neuper@37906
|
581 |
cterm' list)(*collect by get_assumptions_ in applicable_in, except if
|
neuper@37906
|
582 |
butlast tac is Check_elementwise: take only these asms*)
|
neuper@37906
|
583 |
| Free_Solve'
|
neuper@37906
|
584 |
|
neuper@37906
|
585 |
| Rewrite_Inst' of theory' * rew_ord' * rls
|
neuper@37906
|
586 |
* bool * subst * thm' * term * (term * term list)
|
neuper@37906
|
587 |
| Rewrite' of theory' * rew_ord' * rls * bool * thm' *
|
neuper@37906
|
588 |
term * (term * term list)
|
neuper@37906
|
589 |
| Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm' *
|
neuper@37906
|
590 |
term * (term * term list)
|
neuper@37906
|
591 |
| Rewrite_Set_Inst' of theory' * bool * subst * rls *
|
neuper@37906
|
592 |
term * (term * term list)
|
neuper@37906
|
593 |
| Detail_Set_Inst' of theory' * bool * subst * rls *
|
neuper@37906
|
594 |
term * (term * term list)
|
neuper@37906
|
595 |
| Rewrite_Set' of theory' * bool * rls * term * (term * term list)
|
neuper@37906
|
596 |
| Detail_Set' of theory' * bool * rls * term * (term * term list)
|
neuper@37906
|
597 |
| End_Detail' of (term * (term list)) (*see End_Trans'*)
|
neuper@37906
|
598 |
| End_Ruleset' of term
|
neuper@37906
|
599 |
| Derive' of rls
|
neuper@37906
|
600 |
| Calculate' of theory' * string * term * (term * thm')
|
neuper@37906
|
601 |
(*WN.29.4.03 asm?: * term list??*)
|
neuper@37906
|
602 |
| Substitute' of subte (*the 'substitution': terms of type bool*)
|
neuper@37906
|
603 |
* term (*to be substituted in*)
|
neuper@37906
|
604 |
* term (*resulting from the substitution*)
|
neuper@37906
|
605 |
| Apply_Assumption' of term list * term
|
neuper@37906
|
606 |
|
neuper@37906
|
607 |
| Take' of term | Take_Inst' of term
|
neuper@37906
|
608 |
| Group' of (con * int list * term)
|
neuper@37906
|
609 |
| Subproblem' of (spec *
|
neuper@37906
|
610 |
(ori list) * (*filled in assod Subproblem'*)
|
neuper@37906
|
611 |
term * (*-"-, headline of calc-head *)
|
neuper@37906
|
612 |
fmz_ *
|
neuper@37906
|
613 |
term) (*Subproblem(dom,pbl)*)
|
neuper@37906
|
614 |
| CAScmd' of term
|
neuper@37906
|
615 |
| End_Subproblem' of term (*???*)
|
neuper@37906
|
616 |
| Split_And' of term | Conclude_And' of term
|
neuper@37906
|
617 |
| Split_Or' of term | Conclude_Or' of term
|
neuper@37906
|
618 |
| Begin_Trans' of term | End_Trans' of (term * (term list))
|
neuper@37906
|
619 |
| Begin_Sequ' | End_Sequ'(* substitute root.env*)
|
neuper@37906
|
620 |
| Split_Intersect' of term | End_Intersect' of term
|
neuper@37906
|
621 |
| Check_elementwise' of (*special case:*)
|
neuper@37906
|
622 |
term * (*(1)the current formula: [x=1,x=...]*)
|
neuper@37906
|
623 |
string * (*(2)the pred from Check_elementwise *)
|
neuper@37906
|
624 |
(term * (*(3)composed from (1) and (2): {x. pred}*)
|
neuper@37906
|
625 |
term list) (*20.5.03 assumptions*)
|
neuper@37906
|
626 |
|
neuper@37906
|
627 |
| Or_to_List' of term * term (* (a | b, [a,b]) *)
|
neuper@37906
|
628 |
| Collect_Trues' of term
|
neuper@37906
|
629 |
|
neuper@37906
|
630 |
| Empty_Tac_ | Tac_ of (*for dummies*)
|
neuper@37906
|
631 |
theory *
|
neuper@37906
|
632 |
string * (*form*)
|
neuper@37906
|
633 |
string * (*in Tac*)
|
neuper@37906
|
634 |
string (*result of Tac".."*)
|
neuper@37906
|
635 |
| User' (*internal for ets*) | End_Proof'';(*End_Proof:inout*)
|
neuper@37906
|
636 |
|
neuper@37906
|
637 |
fun tac_2str ma = case ma of
|
neuper@37906
|
638 |
Init_Proof' (ppc, spec) =>
|
neuper@37906
|
639 |
"Init_Proof' "^(pair2str (strs2str ppc, spec2str spec))
|
neuper@37906
|
640 |
| Model_Problem' (pblID,_,_) => "Model_Problem' "^(strs2str pblID )
|
neuper@37906
|
641 |
| Refine_Tacitly'(p,prefin,domID,metID,itms)=>
|
neuper@37906
|
642 |
"Refine_Tacitly' ("
|
neuper@37906
|
643 |
^(strs2str p)^", "^(strs2str prefin)^", "
|
neuper@37906
|
644 |
^domID^", "^(strs2str metID)^", pbl-itms)"
|
neuper@37906
|
645 |
| Refine_Problem' ms => "Refine_Problem' ("^(*matchs2str ms*)"..."^")"
|
neuper@37906
|
646 |
(*| Match_Problem' (pI, (ok, (itms, pre))) =>
|
neuper@37906
|
647 |
"Match_Problem' "^(spair2str (strs2str pI,
|
neuper@37906
|
648 |
spair2str (bool2str ok,
|
neuper@37924
|
649 |
spair2str ("itms2str_ itms",
|
neuper@37906
|
650 |
"items2str pre"))))*)
|
neuper@37906
|
651 |
| Add_Given' cterm' => "Add_Given' "(*^cterm'*)
|
neuper@37906
|
652 |
| Del_Given' cterm' => "Del_Given' "(*^cterm'*)
|
neuper@37906
|
653 |
| Add_Find' cterm' => "Add_Find' "(*^cterm'*)
|
neuper@37906
|
654 |
| Del_Find' cterm' => "Del_Find' "(*^cterm'*)
|
neuper@37906
|
655 |
| Add_Relation' cterm' => "Add_Relation' "(*^cterm'*)
|
neuper@37906
|
656 |
| Del_Relation' cterm' => "Del_Relation' "(*^cterm'*)
|
neuper@37906
|
657 |
|
neuper@37906
|
658 |
| Specify_Theory' domID => "Specify_Theory' "^(quote domID )
|
neuper@37906
|
659 |
| Specify_Problem' (pI, (ok, (itms, pre))) =>
|
neuper@37906
|
660 |
"Specify_Problem' "^(spair2str (strs2str pI,
|
neuper@37906
|
661 |
spair2str (bool2str ok,
|
neuper@37924
|
662 |
spair2str ("itms2str_ itms",
|
neuper@37906
|
663 |
"items2str pre"))))
|
neuper@37906
|
664 |
| Specify_Method' (pI,oris,itms) =>
|
neuper@37906
|
665 |
"Specify_Method' ("^metID2str pI^", "^oris2str oris^", )"
|
neuper@37906
|
666 |
|
neuper@37906
|
667 |
| Apply_Method' (metID,_,_) => "Apply_Method' "^(strs2str metID)
|
neuper@37906
|
668 |
| Check_Postcond' (pblID,(scval,asm)) =>
|
neuper@37906
|
669 |
"Check_Postcond' "^(spair2str(strs2str pblID,
|
neuper@37906
|
670 |
spair2str (term2str scval, strs2str asm)))
|
neuper@37906
|
671 |
|
neuper@37906
|
672 |
| Free_Solve' => "Free_Solve'"
|
neuper@37906
|
673 |
|
neuper@37906
|
674 |
| Rewrite_Inst' (*subs,thm'*) _ =>
|
neuper@37906
|
675 |
"Rewrite_Inst' "(*^(pair2str (subs2str subs, spair2str thm'))*)
|
neuper@37906
|
676 |
| Rewrite' thm' => "Rewrite' "(*^(spair2str thm')*)
|
neuper@37906
|
677 |
| Rewrite_Asm' thm' => "Rewrite_Asm' "(*^(spair2str thm')*)
|
neuper@37906
|
678 |
| Rewrite_Set_Inst' (*subs,thm'*) _ =>
|
neuper@37906
|
679 |
"Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*)
|
neuper@37906
|
680 |
| Rewrite_Set'(thy',pasm,rls',f,(f',asm))
|
neuper@37906
|
681 |
=> "Rewrite_Set' ("^thy'^","^(bool2str pasm)^","^(id_rls rls')^","
|
neuper@37925
|
682 |
^(Syntax.string_of_term (ctxt_Isac"") f)^",("^(Syntax.string_of_term (ctxt_Isac"") f')
|
neuper@37925
|
683 |
^","^((strs2str o (map (Syntax.string_of_term (ctxt_Isac"")))) asm)^"))"
|
neuper@37906
|
684 |
|
neuper@37906
|
685 |
| End_Detail' _ => "End_Detail' xxx"
|
neuper@37906
|
686 |
| Detail_Set' _ => "Detail_Set' xxx"
|
neuper@37906
|
687 |
| Detail_Set_Inst' _ => "Detail_Set_Inst' xxx"
|
neuper@37906
|
688 |
|
neuper@37906
|
689 |
| Derive' rls => "Derive' "^id_rls rls
|
neuper@37906
|
690 |
| Calculate' _ => "Calculate' "
|
neuper@37906
|
691 |
| Substitute' subs => "Substitute' "(*^(subs2str subs)*)
|
neuper@37906
|
692 |
| Apply_Assumption' ct's => "Apply_Assumption' "(*^(strs2str ct's)*)
|
neuper@37906
|
693 |
|
neuper@37906
|
694 |
| Take' cterm' => "Take' "(*^(quote cterm' )*)
|
neuper@37906
|
695 |
| Take_Inst' cterm' => "Take_Inst' "(*^(quote cterm' )*)
|
neuper@37906
|
696 |
| Group' (con, ints, _) =>
|
neuper@37906
|
697 |
"Group' "^(pair2str (con2str con, ints2str ints))
|
neuper@37906
|
698 |
| Subproblem' (spec, oris, _,_,pbl_form) =>
|
neuper@37906
|
699 |
"Subproblem' "(*^(pair2str (domID, strs2str ,...))*)
|
neuper@37906
|
700 |
| End_Subproblem' _ => "End_Subproblem'"
|
neuper@37906
|
701 |
| CAScmd' cterm' => "CAScmd' "(*^(quote cterm')*)
|
neuper@37906
|
702 |
|
neuper@37906
|
703 |
| Empty_Tac_ => "Empty_Tac_"
|
neuper@37906
|
704 |
| User' => "User'"
|
neuper@37906
|
705 |
| Tac_ (_,form,id,result) => "Tac_ (thy,"^form^","^id^","^result^")"
|
neuper@37906
|
706 |
| _ => "tac_2str not impl. for arg";
|
neuper@37906
|
707 |
|
neuper@37906
|
708 |
(*'executed tactics' (tac_s) with local environment etc.;
|
neuper@37906
|
709 |
used for continuing eval script + for generate*)
|
neuper@37906
|
710 |
type ets =
|
neuper@37906
|
711 |
(loc_ * (* of tactic in scr, tactic (weakly) associated with tac_*)
|
neuper@37906
|
712 |
(tac_ * (* (for generate) *)
|
neuper@37906
|
713 |
env * (* with 'tactic=result' as a rule, tactic ev. _not_ ready:
|
neuper@37906
|
714 |
for handling 'parallel let'*)
|
neuper@37906
|
715 |
env * (* with results of (ready) tacs *)
|
neuper@37906
|
716 |
term * (* itr_arg of tactic, for upd. env at Repeat, Try*)
|
neuper@37906
|
717 |
term * (* result value of the tac *)
|
neuper@37906
|
718 |
safe))
|
neuper@37906
|
719 |
list;
|
neuper@37906
|
720 |
val Ets = []:ets;
|
neuper@37906
|
721 |
|
neuper@37906
|
722 |
|
neuper@37906
|
723 |
fun ets2s (l,(m,eno,env,iar,res,s)) =
|
neuper@37906
|
724 |
"\n("^(loc_2str l)^",("^(tac_2str m)^
|
neuper@37906
|
725 |
",\n ens= "^(subst2str eno)^
|
neuper@37906
|
726 |
",\n env= "^(subst2str env)^
|
neuper@37925
|
727 |
",\n iar= "^(Syntax.string_of_term (ctxt_Isac"") iar)^
|
neuper@37925
|
728 |
",\n res= "^(Syntax.string_of_term (ctxt_Isac"") res)^
|
neuper@37906
|
729 |
",\n "^(safe2str s)^"))";
|
neuper@37906
|
730 |
fun ets2str (ets:ets) = (strs2str o (map ets2s)) ets;
|
neuper@37906
|
731 |
|
neuper@37906
|
732 |
|
neuper@37906
|
733 |
type envp =(*9.5.03: unused, delete with field in ptree.PblObj FIXXXME*)
|
neuper@37906
|
734 |
(int * term list) list * (*assoc-list: args of met*)
|
neuper@37906
|
735 |
(int * rls) list * (*assoc-list: tacs already done ///15.9.00*)
|
neuper@37906
|
736 |
(int * ets) list * (*assoc-list: tacs etc. already done*)
|
neuper@37906
|
737 |
(string * pos) list; (*asms * from where*)
|
neuper@37906
|
738 |
val empty_envp = ([],[],[],[]):envp;
|
neuper@37906
|
739 |
|
neuper@37906
|
740 |
datatype ppobj =
|
neuper@37906
|
741 |
PrfObj of {cell : lrd option, (*where in form tac has been applied*)
|
neuper@37906
|
742 |
(*^^^FIXME.WN0607 rename this field*)
|
neuper@37906
|
743 |
form : term,
|
neuper@37906
|
744 |
tac : tac, (* also in istate*)
|
neuper@37906
|
745 |
loc : istate option * istate option, (*for form, result
|
neuper@37925
|
746 |
13.8.02: (NONE,NONE) <==> e_istate ! see update_loc, get_loc*)
|
neuper@37906
|
747 |
branch: branch,
|
neuper@37906
|
748 |
result: term * term list,
|
neuper@37906
|
749 |
ostate: ostate} (*Complete <=> result is OK*)
|
neuper@37906
|
750 |
| PblObj of {cell : lrd option,(*unused: meaningful only for some _Prf_Obj*)
|
neuper@37906
|
751 |
fmz : fmz, (*from init:FIXME never use this spec;-drop*)
|
neuper@37906
|
752 |
origin: (ori list) * (*representation from fmz+pbt
|
neuper@37906
|
753 |
for efficiently adding items in probl, meth*)
|
neuper@37906
|
754 |
spec * (*updated by Refine_Tacitly*)
|
neuper@37906
|
755 |
term, (*headline of calc-head, as calculated
|
neuper@37906
|
756 |
initially(!)*)
|
neuper@37906
|
757 |
(*# the origin of a root-pbl is created from fmz
|
neuper@37906
|
758 |
(thus providing help for input to the user),
|
neuper@37906
|
759 |
# the origin of a sub-pbl is created from the argument
|
neuper@37906
|
760 |
-list of a script-tac 'SubProblem (spec) [arg-list]'
|
neuper@37906
|
761 |
by 'match_ags'*)
|
neuper@37906
|
762 |
spec : spec, (*explicitly input*)
|
neuper@37906
|
763 |
probl : itm list, (*itms explicitly input*)
|
neuper@37906
|
764 |
meth : itm list, (*itms automatically added to copy of probl
|
neuper@37906
|
765 |
TODO: input like to 'probl'*)
|
neuper@37906
|
766 |
env : istate option,(*for problem with initac in script*)
|
neuper@37906
|
767 |
loc : istate option * istate option, (*for pbl+met * result*)
|
neuper@37906
|
768 |
branch: branch,
|
neuper@37906
|
769 |
result: term * term list,
|
neuper@37906
|
770 |
ostate: ostate}; (*Complete <=> result is _proven_ OK*)
|
neuper@37906
|
771 |
|
neuper@37906
|
772 |
(*.this tree contains isac's calculations; TODO.WN03 rename to ctree;
|
neuper@37906
|
773 |
the structure has been copied from an early version of Theorema(c);
|
neuper@37906
|
774 |
it has the disadvantage, that there is no space
|
neuper@37906
|
775 |
for the first tactic in a script generating the first formula at (p,Frm);
|
neuper@37906
|
776 |
this trouble has been covered by 'init_form' and 'Take' so far,
|
neuper@37906
|
777 |
but it is crucial if the first tactic in a script is eg. 'Subproblem';
|
neuper@37906
|
778 |
see 'type tac ', Apply_Method.
|
neuper@37906
|
779 |
.*)
|
neuper@37906
|
780 |
datatype ptree =
|
neuper@37906
|
781 |
EmptyPtree
|
neuper@37906
|
782 |
| Nd of ppobj * (ptree list);
|
neuper@37906
|
783 |
val e_ptree = EmptyPtree;
|
neuper@37906
|
784 |
|
neuper@37906
|
785 |
fun rep_prfobj (PrfObj {cell,form,tac,loc,branch,result,ostate}) =
|
neuper@37906
|
786 |
{cell=cell,form=form,tac=tac,loc=loc,branch=branch,result=result,ostate=ostate};
|
neuper@37906
|
787 |
fun rep_pblobj (PblObj {cell,origin,fmz,spec,probl,meth,env,
|
neuper@37906
|
788 |
loc,branch,result,ostate}) =
|
neuper@37906
|
789 |
{cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,meth=meth,
|
neuper@37906
|
790 |
env=env,loc=loc,branch=branch,result=result,ostate=ostate};
|
neuper@37906
|
791 |
fun is_prfobj (PrfObj _) = true
|
neuper@37906
|
792 |
| is_prfobj _ =false;
|
neuper@37906
|
793 |
(*val is_prfobj' = get_obj is_prfobj; *)
|
neuper@37906
|
794 |
fun is_pblobj (PblObj _) = true
|
neuper@37906
|
795 |
| is_pblobj _ = false;
|
neuper@37906
|
796 |
(*val is_pblobj' = get_obj is_pblobj; 'Error: unbound constructor get_obj'*)
|
neuper@37906
|
797 |
|
neuper@37906
|
798 |
|
neuper@37906
|
799 |
exception PTREE of string;
|
neuper@37906
|
800 |
fun nth _ [] = raise PTREE "nth _ []"
|
neuper@37906
|
801 |
| nth 1 (x::xs) = x
|
neuper@37906
|
802 |
| nth n (x::xs) = nth (n-1) xs;
|
neuper@37906
|
803 |
(*> nth 2 [11,22,33]; -->> val it = 22 : int*)
|
neuper@37906
|
804 |
|
neuper@37906
|
805 |
fun lev_up ([]:pos) = raise PTREE "lev_up []"
|
neuper@37906
|
806 |
| lev_up p = (drop_last p):pos;
|
neuper@37906
|
807 |
fun lev_on ([]:pos) = raise PTREE "lev_on []"
|
neuper@37906
|
808 |
| lev_on pos =
|
neuper@37906
|
809 |
let val len = length pos
|
neuper@37906
|
810 |
in (drop_last pos) @ [(nth len pos)+1] end;
|
neuper@37906
|
811 |
fun lev_onFrm ((p,_):pos') = (lev_on p,Frm):pos'
|
neuper@37906
|
812 |
| lev_onFrm p = raise PTREE ("*** lev_onFrm: pos'="^(pos'2str p));
|
neuper@37906
|
813 |
(*040216: for inform --> embed_deriv: remains on same level*)
|
neuper@37906
|
814 |
fun lev_back (([],_):pos') = raise PTREE "lev_on_back: called by ([],_)"
|
neuper@37906
|
815 |
| lev_back (p,_) =
|
neuper@37906
|
816 |
if last_elem p <= 1 then (p, Frm):pos'
|
neuper@37906
|
817 |
else ((drop_last p) @ [(nth (length p) p) - 1], Res);
|
neuper@37906
|
818 |
(*.increase pos by n within a level.*)
|
neuper@37906
|
819 |
fun pos_plus 0 pos = pos
|
neuper@37906
|
820 |
| pos_plus n ((p,Frm):pos') = pos_plus (n-1) (p, Res)
|
neuper@37906
|
821 |
| pos_plus n ((p, _):pos') = pos_plus (n-1) (lev_on p, Res);
|
neuper@37906
|
822 |
|
neuper@37906
|
823 |
|
neuper@37906
|
824 |
|
neuper@37906
|
825 |
fun lev_pred ([]:pos) = raise PTREE "lev_pred []"
|
neuper@37906
|
826 |
| lev_pred (pos:pos) =
|
neuper@37906
|
827 |
let val len = length pos
|
neuper@37906
|
828 |
in ((drop_last pos) @ [(nth len pos)-1]):pos end;
|
neuper@37906
|
829 |
(*lev_pred [1,2,3];
|
neuper@37906
|
830 |
val it = [1,2,2] : pos
|
neuper@37906
|
831 |
> lev_pred [1];
|
neuper@37906
|
832 |
val it = [0] : pos *)
|
neuper@37906
|
833 |
|
neuper@37906
|
834 |
fun lev_dn p = p @ [0];
|
neuper@37906
|
835 |
(*> (lev_dn o lev_on) [1,2,3];
|
neuper@37906
|
836 |
val it = [1,2,4,0] : pos *)
|
neuper@37906
|
837 |
(*fun lev_dn' ((p,p_):pos') = (lev_dn p, Frm):pos'; WN.3.12.03: never used*)
|
neuper@37906
|
838 |
fun lev_dnRes ((p,_):pos') = (lev_dn p, Res):pos';
|
neuper@37906
|
839 |
|
neuper@37906
|
840 |
(*4.4.00*)
|
neuper@37906
|
841 |
fun lev_up_ ((p,Res):pos') = (lev_up p,Res):pos'
|
neuper@37906
|
842 |
| lev_up_ p' = raise error ("lev_up_: called for "^(pos'2str p'));
|
neuper@37906
|
843 |
fun lev_dn_ ((p,_):pos') = (lev_dn p,Res):pos'
|
neuper@37906
|
844 |
fun ind ((p,_):pos') = length p; (*WN050108 deprecated in favour of lev_of*)
|
neuper@37906
|
845 |
fun lev_of ((p,_):pos') = length p;
|
neuper@37906
|
846 |
|
neuper@37906
|
847 |
|
neuper@37906
|
848 |
(** convert ptree to a string **)
|
neuper@37906
|
849 |
|
neuper@37906
|
850 |
(* convert a pos from list to string *)
|
neuper@37906
|
851 |
fun pr_pos ps = (space_implode "." (map string_of_int ps))^". ";
|
neuper@37906
|
852 |
(* show hd origin or form only *)
|
neuper@37906
|
853 |
fun pr_short (p:pos) (PblObj {origin = (ori,_,_),...}) =
|
neuper@37906
|
854 |
((pr_pos p) ^ " ----- pblobj -----\n")
|
neuper@37925
|
855 |
(* ((((Syntax.string_of_term (ctxt_Isac"")) o #4 o hd) ori)^" "^
|
neuper@37925
|
856 |
(((Syntax.string_of_term (ctxt_Isac"")) o hd(*!?!*) o #5 o hd) ori))^
|
neuper@37906
|
857 |
"\n") *)
|
neuper@37906
|
858 |
| pr_short p (PrfObj {form = form,...}) =
|
neuper@37906
|
859 |
((pr_pos p) ^ (term2str form) ^ "\n");
|
neuper@37906
|
860 |
(*
|
neuper@37906
|
861 |
fun pr_cell (p:pos) (PblObj {cell = c, origin = (ori,_,_),...}) =
|
neuper@37906
|
862 |
((ints2str c) ^" "^
|
neuper@37925
|
863 |
((((Syntax.string_of_term (ctxt_Isac"")) o #4 o hd) ori)^" "^
|
neuper@37925
|
864 |
(((Syntax.string_of_term (ctxt_Isac"")) o hd(*!?!*) o #5 o hd) ori))^
|
neuper@37906
|
865 |
"\n")
|
neuper@37906
|
866 |
| pr_cell p (PrfObj {cell = c, form = form,...}) =
|
neuper@37906
|
867 |
((ints2str c) ^" "^ (term2str form) ^ "\n");
|
neuper@37906
|
868 |
*)
|
neuper@37906
|
869 |
|
neuper@37906
|
870 |
(* convert ptree *)
|
neuper@37906
|
871 |
fun pr_ptree f pt =
|
neuper@37906
|
872 |
let
|
neuper@37906
|
873 |
fun pr_pt pfn _ EmptyPtree = ""
|
neuper@37906
|
874 |
| pr_pt pfn ps (Nd (b, [])) = pfn ps b
|
neuper@37906
|
875 |
| pr_pt pfn ps (Nd (b, ts)) = (pfn ps b)^
|
neuper@37906
|
876 |
(prts pfn (ps:pos) 1 ts)
|
neuper@37906
|
877 |
and prts pfn ps p [] = ""
|
neuper@37906
|
878 |
| prts pfn ps p (t::ts) = (pr_pt pfn (ps @ [p]) t)^
|
neuper@37906
|
879 |
(prts pfn ps (p+1) ts)
|
neuper@37906
|
880 |
in pr_pt f [] pt end;
|
neuper@37906
|
881 |
(*
|
neuper@37906
|
882 |
> fun prfn ps b = (pr_pos ps)^" "^b(*TODO*)^"\n";
|
neuper@37906
|
883 |
> val pt = ref EmptyPtree;
|
neuper@37906
|
884 |
> pt:=Nd("root",
|
neuper@37906
|
885 |
[Nd("xx1",[]),
|
neuper@37906
|
886 |
Nd("xx2",
|
neuper@37906
|
887 |
[Nd("xx2.1.",[]),
|
neuper@37906
|
888 |
Nd("xx2.2.",[])]),
|
neuper@37906
|
889 |
Nd("xx3",[])]);
|
neuper@37906
|
890 |
> writeln (pr_ptree prfn (!pt));
|
neuper@37906
|
891 |
*)
|
neuper@37906
|
892 |
|
neuper@37906
|
893 |
|
neuper@37906
|
894 |
(** access the branches of ptree **)
|
neuper@37906
|
895 |
|
neuper@37906
|
896 |
fun ins_nth 1 e l = e::l
|
neuper@37906
|
897 |
| ins_nth n e [] = raise PTREE "ins_nth n e []"
|
neuper@37906
|
898 |
| ins_nth n e (l::ls) = l::(ins_nth (n-1) e ls);
|
neuper@37906
|
899 |
fun repl [] _ _ = raise PTREE "repl [] _ _"
|
neuper@37906
|
900 |
| repl (l::ls) 1 e = e::ls
|
neuper@37906
|
901 |
| repl (l::ls) n e = l::(repl ls (n-1) e);
|
neuper@37906
|
902 |
fun repl_app ls n e =
|
neuper@37906
|
903 |
let val lim = 1 + length ls
|
neuper@37906
|
904 |
in if n > lim then raise PTREE "repl_app: n > lim"
|
neuper@37906
|
905 |
else if n = lim then ls @ [e]
|
neuper@37906
|
906 |
else repl ls n e end;
|
neuper@37906
|
907 |
(*
|
neuper@37906
|
908 |
> repl [1,2,3] 2 22222;
|
neuper@37906
|
909 |
val it = [1,22222,3] : int list
|
neuper@37906
|
910 |
> repl_app [1,2,3,4] 5 5555;
|
neuper@37906
|
911 |
val it = [1,2,3,4,5555] : int list
|
neuper@37906
|
912 |
> repl_app [1,2,3] 2 22222;
|
neuper@37906
|
913 |
val it = [1,22222,3] : int list
|
neuper@37906
|
914 |
> repl_app [1] 2 22222 ;
|
neuper@37906
|
915 |
val it = [1,22222] : int list
|
neuper@37906
|
916 |
*)
|
neuper@37906
|
917 |
|
neuper@37906
|
918 |
|
neuper@37906
|
919 |
(*.get from obj at pos by f : ppobj -> 'a.*)
|
neuper@37906
|
920 |
fun get_obj f EmptyPtree (_:pos) = raise PTREE "get_obj f EmptyPtree"
|
neuper@37906
|
921 |
| get_obj f (Nd (b, _)) [] = f b
|
neuper@37906
|
922 |
| get_obj f (Nd (b, bs)) (p::ps) =
|
neuper@37906
|
923 |
(* val (f, Nd (b, bs), (p::ps)) = (I, pt, p);
|
neuper@37906
|
924 |
*)
|
neuper@37906
|
925 |
let val _ = (nth p bs) handle _ => raise PTREE ("get_obj: pos = "^
|
neuper@37906
|
926 |
(ints2str' (p::ps))^" does not exist");
|
neuper@37906
|
927 |
in (get_obj f (nth p bs) (ps:pos))
|
neuper@37906
|
928 |
(*before WN050419: 'wrong type..' raised also if pos doesn't exist*)
|
neuper@37906
|
929 |
handle _ => raise PTREE (*"get_obj: at pos = "^
|
neuper@37906
|
930 |
(ints2str' (p::ps))^" wrong type of ppobj"*)
|
neuper@37906
|
931 |
("get_obj: pos = "^
|
neuper@37906
|
932 |
(ints2str' (p::ps))^" does not exist")
|
neuper@37906
|
933 |
end;
|
neuper@37906
|
934 |
fun get_nd EmptyPtree _ = raise PTREE "get_nd EmptyPtree"
|
neuper@37906
|
935 |
| get_nd n [] = n
|
neuper@37906
|
936 |
| get_nd (Nd (_,nds)) (pos as p::(ps:pos)) = (get_nd (nth p nds) ps)
|
neuper@37906
|
937 |
handle _ => raise PTREE ("get_nd: not existent pos = "^(ints2str' pos));
|
neuper@37906
|
938 |
|
neuper@37906
|
939 |
|
neuper@37906
|
940 |
(* for use by get_obj *)
|
neuper@37925
|
941 |
fun g_cell (PblObj {cell = c,...}) = NONE
|
neuper@37906
|
942 |
| g_cell (PrfObj {cell = c,...}) = c;(*WN0607 hack for quick introduction of lrd + rewrite-at (thms, calcs)*)
|
neuper@37906
|
943 |
fun g_form (PrfObj {form = f,...}) = f
|
neuper@37906
|
944 |
| g_form (PblObj {origin=(_,_,f),...}) = f;
|
neuper@37906
|
945 |
fun g_form' (Nd (PrfObj {form = f,...}, _)) = f
|
neuper@37906
|
946 |
| g_form' (Nd (PblObj {origin=(_,_,f),...}, _)) = f;
|
neuper@37906
|
947 |
(* | g_form _ = raise PTREE "g_form not for PblObj";*)
|
neuper@37906
|
948 |
fun g_origin (PblObj {origin = ori,...}) = ori
|
neuper@37906
|
949 |
| g_origin _ = raise PTREE "g_origin not for PrfObj";
|
neuper@37906
|
950 |
fun g_fmz (PblObj {fmz = f,...}) = f
|
neuper@37906
|
951 |
| g_fmz _ = raise PTREE "g_fmz not for PrfObj";
|
neuper@37906
|
952 |
fun g_spec (PblObj {spec = s,...}) = s
|
neuper@37906
|
953 |
| g_spec _ = raise PTREE "g_spec not for PrfObj";
|
neuper@37906
|
954 |
fun g_pbl (PblObj {probl = p,...}) = p
|
neuper@37906
|
955 |
| g_pbl _ = raise PTREE "g_pbl not for PrfObj";
|
neuper@37906
|
956 |
fun g_met (PblObj {meth = p,...}) = p
|
neuper@37906
|
957 |
| g_met _ = raise PTREE "g_met not for PrfObj";
|
neuper@37906
|
958 |
fun g_domID (PblObj {spec = (d,_,_),...}) = d
|
neuper@37906
|
959 |
| g_domID _ = raise PTREE "g_metID not for PrfObj";
|
neuper@37906
|
960 |
fun g_metID (PblObj {spec = (_,_,m),...}) = m
|
neuper@37906
|
961 |
| g_metID _ = raise PTREE "g_metID not for PrfObj";
|
neuper@37906
|
962 |
fun g_env (PblObj {env,...}) = env
|
neuper@37906
|
963 |
| g_env _ = raise PTREE "g_env not for PrfObj";
|
neuper@37906
|
964 |
fun g_loc (PblObj {loc = l,...}) = l
|
neuper@37906
|
965 |
| g_loc (PrfObj {loc = l,...}) = l;
|
neuper@37906
|
966 |
fun g_branch (PblObj {branch = b,...}) = b
|
neuper@37906
|
967 |
| g_branch (PrfObj {branch = b,...}) = b;
|
neuper@37906
|
968 |
fun g_tac (PblObj {spec = (d,p,m),...}) = Apply_Method m
|
neuper@37906
|
969 |
| g_tac (PrfObj {tac = m,...}) = m;
|
neuper@37906
|
970 |
fun g_result (PblObj {result = r,...}) = r
|
neuper@37906
|
971 |
| g_result (PrfObj {result = r,...}) = r;
|
neuper@37906
|
972 |
fun g_res (PblObj {result = (r,_),...}) = r
|
neuper@37906
|
973 |
| g_res (PrfObj {result = (r,_),...}) = r;
|
neuper@37906
|
974 |
fun g_res' (Nd (PblObj {result = (r,_),...}, _)) = r
|
neuper@37906
|
975 |
| g_res' (Nd (PrfObj {result = (r,_),...}, _)) = r;
|
neuper@37906
|
976 |
fun g_ostate (PblObj {ostate = r,...}) = r
|
neuper@37906
|
977 |
| g_ostate (PrfObj {ostate = r,...}) = r;
|
neuper@37906
|
978 |
fun g_ostate' (Nd (PblObj {ostate = r,...}, _)) = r
|
neuper@37906
|
979 |
| g_ostate' (Nd (PrfObj {ostate = r,...}, _)) = r;
|
neuper@37906
|
980 |
|
neuper@37925
|
981 |
fun gpt_cell (Nd (PblObj {cell = c,...},_)) = NONE
|
neuper@37906
|
982 |
| gpt_cell (Nd (PrfObj {cell = c,...},_)) = c;
|
neuper@37906
|
983 |
|
neuper@37906
|
984 |
(*in CalcTree/Subproblem an 'just_created_' model is created;
|
neuper@37906
|
985 |
this is filled to 'untouched' by Model/Refine_Problem*)
|
neuper@37906
|
986 |
fun just_created_ (PblObj {meth, probl, spec, ...}) =
|
neuper@37906
|
987 |
null meth andalso null probl andalso spec = e_spec;
|
neuper@37906
|
988 |
val e_origin = ([],e_spec,e_term): (ori list) * spec * term;
|
neuper@37906
|
989 |
|
neuper@37906
|
990 |
fun just_created (pt,(p,_):pos') =
|
neuper@37906
|
991 |
let val ppobj = get_obj I pt p
|
neuper@37906
|
992 |
in is_pblobj ppobj andalso just_created_ ppobj end;
|
neuper@37906
|
993 |
|
neuper@37906
|
994 |
(*.does the pos in the ctree exist ?.*)
|
neuper@37906
|
995 |
fun existpt pos pt = can (get_obj I pt) pos;
|
neuper@37906
|
996 |
(*.does the pos' in the ctree exist, ie. extra check for result in the node.*)
|
neuper@37906
|
997 |
fun existpt' ((p,p_):pos') pt =
|
neuper@37906
|
998 |
if can (get_obj I pt) p
|
neuper@37906
|
999 |
then case p_ of
|
neuper@37906
|
1000 |
Res => get_obj g_ostate pt p = Complete
|
neuper@37906
|
1001 |
| _ => true
|
neuper@37906
|
1002 |
else false;
|
neuper@37906
|
1003 |
|
neuper@37906
|
1004 |
(*.is this position appropriate for calculating intermediate steps?.*)
|
neuper@37906
|
1005 |
fun is_interpos ((_, Res):pos') = true
|
neuper@37906
|
1006 |
| is_interpos _ = false;
|
neuper@37906
|
1007 |
|
neuper@37906
|
1008 |
fun last_onlev pt pos = not (existpt (lev_on pos) pt);
|
neuper@37906
|
1009 |
|
neuper@37906
|
1010 |
|
neuper@37906
|
1011 |
(*.find the position of the next parent which is a PblObj in ptree.*)
|
neuper@37906
|
1012 |
fun par_pblobj pt ([]:pos) = ([]:pos)
|
neuper@37906
|
1013 |
| par_pblobj pt p =
|
neuper@37906
|
1014 |
let fun par pt [] = []
|
neuper@37906
|
1015 |
| par pt p = if is_pblobj (get_obj I pt p) then p
|
neuper@37906
|
1016 |
else par pt (lev_up p)
|
neuper@37906
|
1017 |
in par pt (lev_up p) end;
|
neuper@37906
|
1018 |
(* lev_up for hard_gen operating with pos = [...,0] *)
|
neuper@37906
|
1019 |
|
neuper@37906
|
1020 |
(*.find the position and the children of the next parent which is a PblObj.*)
|
neuper@37906
|
1021 |
fun par_children (Nd (PblObj _, children)) ([]:pos) = (children, []:pos)
|
neuper@37906
|
1022 |
| par_children (pt as Nd (PblObj _, children)) p =
|
neuper@37906
|
1023 |
let fun par [] = (children, [])
|
neuper@37906
|
1024 |
| par p = let val Nd (obj, children) = get_nd pt p
|
neuper@37906
|
1025 |
in if is_pblobj obj then (children, p) else par (lev_up p)
|
neuper@37906
|
1026 |
end;
|
neuper@37906
|
1027 |
in par (lev_up p) end;
|
neuper@37906
|
1028 |
|
neuper@37906
|
1029 |
(*.get the children of a node in ptree.*)
|
neuper@37906
|
1030 |
fun children (Nd (PblObj _, cn)) = cn
|
neuper@37906
|
1031 |
| children (Nd (PrfObj _, cn)) = cn;
|
neuper@37906
|
1032 |
|
neuper@37906
|
1033 |
|
neuper@37906
|
1034 |
(*.find the next parent, which is either a PblObj (return true)
|
neuper@37906
|
1035 |
or a PrfObj with tac = Detail_Set (return false).*)
|
neuper@37906
|
1036 |
(*FIXME.3.4.03:re-organize par_pbl_det after rls' --> rls*)
|
neuper@37906
|
1037 |
fun par_pbl_det pt ([]:pos) = (true, []:pos, Erls)
|
neuper@37906
|
1038 |
| par_pbl_det pt p =
|
neuper@37906
|
1039 |
let fun par pt [] = (true, [], Erls)
|
neuper@37906
|
1040 |
| par pt p = if is_pblobj (get_obj I pt p) then (true, p, Erls)
|
neuper@37906
|
1041 |
else case get_obj g_tac pt p of
|
neuper@37906
|
1042 |
(*Detail_Set rls' => (false, p, assoc_rls rls')
|
neuper@37906
|
1043 |
(*^^^--- before 040206 after ---vvv*)
|
neuper@37906
|
1044 |
|*)Rewrite_Set rls' => (false, p, assoc_rls rls')
|
neuper@37906
|
1045 |
| Rewrite_Set_Inst (_, rls') =>
|
neuper@37906
|
1046 |
(false, p, assoc_rls rls')
|
neuper@37906
|
1047 |
| _ => par pt (lev_up p)
|
neuper@37906
|
1048 |
in par pt (lev_up p) end;
|
neuper@37906
|
1049 |
|
neuper@37906
|
1050 |
|
neuper@37906
|
1051 |
|
neuper@37906
|
1052 |
|
neuper@37906
|
1053 |
(*.get from the whole ptree by f : ppobj -> 'a.*)
|
neuper@37906
|
1054 |
fun get_all f EmptyPtree = []
|
neuper@37906
|
1055 |
| get_all f (Nd (b, [])) = [f b]
|
neuper@37906
|
1056 |
| get_all f (Nd (b, bs)) = [f b] @ (get_alls f bs)
|
neuper@37906
|
1057 |
and get_alls f [] = []
|
neuper@37906
|
1058 |
| get_alls f pts = flat (map (get_all f) pts);
|
neuper@37906
|
1059 |
|
neuper@37906
|
1060 |
|
neuper@37906
|
1061 |
(*.insert obj b into ptree at pos, ev.overwriting this pos.*)
|
neuper@37906
|
1062 |
fun insert b EmptyPtree ([]:pos) = Nd (b, [])
|
neuper@37906
|
1063 |
| insert b EmptyPtree _ = raise PTREE "insert b Empty _"
|
neuper@37906
|
1064 |
| insert b (Nd ( _, _)) [] = raise PTREE "insert b _ []"
|
neuper@37906
|
1065 |
| insert b (Nd (b', bs)) (p::[]) =
|
neuper@37906
|
1066 |
Nd (b', repl_app bs p (Nd (b,[])))
|
neuper@37906
|
1067 |
| insert b (Nd (b', bs)) (p::ps) =
|
neuper@37906
|
1068 |
Nd (b', repl_app bs p (insert b (nth p bs) ps));
|
neuper@37906
|
1069 |
(*
|
neuper@37906
|
1070 |
> type ppobj = string;
|
neuper@37906
|
1071 |
> writeln (pr_ptree prfn (!pt));
|
neuper@37906
|
1072 |
val pt = ref Empty;
|
neuper@37906
|
1073 |
pt:= insert ("root":ppobj) EmptyPtree [];
|
neuper@37906
|
1074 |
pt:= insert ("xx1":ppobj) (!pt) [1];
|
neuper@37906
|
1075 |
pt:= insert ("xx2":ppobj) (!pt) [2];
|
neuper@37906
|
1076 |
pt:= insert ("xx3":ppobj) (!pt) [3];
|
neuper@37906
|
1077 |
pt:= insert ("xx2.1":ppobj) (!pt) [2,1];
|
neuper@37906
|
1078 |
pt:= insert ("xx2.2":ppobj) (!pt) [2,2];
|
neuper@37906
|
1079 |
pt:= insert ("xx2.1.1":ppobj) (!pt) [2,1,1];
|
neuper@37906
|
1080 |
pt:= insert ("xx2.1.2":ppobj) (!pt) [2,1,2];
|
neuper@37906
|
1081 |
pt:= insert ("xx2.1.3":ppobj) (!pt) [2,1,3];
|
neuper@37906
|
1082 |
*)
|
neuper@37906
|
1083 |
|
neuper@37906
|
1084 |
(*.insert children to a node without children.*)
|
neuper@37906
|
1085 |
(*compare: fun insert*)
|
neuper@37906
|
1086 |
fun ins_chn _ EmptyPtree (_:pos) = raise PTREE "ins_chn: EmptyPtree"
|
neuper@37906
|
1087 |
| ins_chn ns (Nd _) [] = raise PTREE "ins_chn: pos = []"
|
neuper@37906
|
1088 |
| ins_chn ns (Nd (b, bs)) (p::[]) =
|
neuper@37906
|
1089 |
if p > length bs then raise PTREE "ins_chn: pos not existent"
|
neuper@37906
|
1090 |
else let val Nd (b', bs') = nth p bs
|
neuper@37906
|
1091 |
in if null bs' then Nd (b, repl_app bs p (Nd (b', ns)))
|
neuper@37906
|
1092 |
else raise PTREE "ins_chn: pos mustNOT be overwritten" end
|
neuper@37906
|
1093 |
| ins_chn ns (Nd (b, bs)) (p::ps) =
|
neuper@37906
|
1094 |
Nd (b, repl_app bs p (ins_chn ns (nth p bs) ps));
|
neuper@37906
|
1095 |
|
neuper@37906
|
1096 |
(* print_depth 11;ins_chn;print_depth 3; ###insert#########################*);
|
neuper@37906
|
1097 |
|
neuper@37906
|
1098 |
|
neuper@37906
|
1099 |
(** apply f to obj at pos, f: ppobj -> ppobj **)
|
neuper@37906
|
1100 |
|
neuper@37906
|
1101 |
fun appl_to_node f (Nd (b,bs)) = Nd (f b, bs);
|
neuper@37906
|
1102 |
fun appl_obj f EmptyPtree [] = EmptyPtree
|
neuper@37906
|
1103 |
| appl_obj f EmptyPtree _ = raise PTREE "appl_obj f Empty _"
|
neuper@37906
|
1104 |
| appl_obj f (Nd (b, bs)) [] = Nd (f b, bs)
|
neuper@37906
|
1105 |
| appl_obj f (Nd (b, bs)) (p::[]) =
|
neuper@37906
|
1106 |
Nd (b, repl_app bs p (((appl_to_node f) o (nth p)) bs))
|
neuper@37906
|
1107 |
| appl_obj f (Nd (b, bs)) (p::ps) =
|
neuper@37906
|
1108 |
Nd (b, repl_app bs p (appl_obj f (nth p bs) (ps:pos)));
|
neuper@37906
|
1109 |
|
neuper@37906
|
1110 |
(* for use by appl_obj *)
|
neuper@37906
|
1111 |
fun repl_form f (PrfObj {cell=c,form= _,tac=tac,loc=loc,
|
neuper@37906
|
1112 |
branch=branch,result=result,ostate=ostate}) =
|
neuper@37906
|
1113 |
PrfObj {cell=c,form= f,tac=tac,loc=loc,
|
neuper@37906
|
1114 |
branch=branch,result=result,ostate=ostate}
|
neuper@37906
|
1115 |
| repl_form _ _ = raise PTREE "repl_form takes no PblObj";
|
neuper@37906
|
1116 |
fun repl_pbl x (PblObj {cell=cell,origin=origin,fmz=fmz,
|
neuper@37906
|
1117 |
spec=spec,probl=_,meth=meth,env=env,loc=loc,
|
neuper@37906
|
1118 |
branch=branch,result=result,ostate=ostate}) =
|
neuper@37906
|
1119 |
PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl= x,
|
neuper@37906
|
1120 |
meth=meth,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
|
neuper@37906
|
1121 |
| repl_pbl _ _ = raise PTREE "repl_pbl takes no PrfObj";
|
neuper@37906
|
1122 |
fun repl_met x (PblObj {cell=cell,origin=origin,fmz=fmz,
|
neuper@37906
|
1123 |
spec=spec,probl=probl,meth=_,env=env,loc=loc,
|
neuper@37906
|
1124 |
branch=branch,result=result,ostate=ostate}) =
|
neuper@37906
|
1125 |
PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,
|
neuper@37906
|
1126 |
meth= x,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
|
neuper@37906
|
1127 |
| repl_met _ _ = raise PTREE "repl_pbl takes no PrfObj";
|
neuper@37906
|
1128 |
|
neuper@37906
|
1129 |
fun repl_spec x (PblObj {cell=cell,origin=origin,fmz=fmz,
|
neuper@37906
|
1130 |
spec= _,probl=probl,meth=meth,env=env,loc=loc,
|
neuper@37906
|
1131 |
branch=branch,result=result,ostate=ostate}) =
|
neuper@37906
|
1132 |
PblObj {cell=cell,origin=origin,fmz=fmz,spec= x,probl=probl,
|
neuper@37906
|
1133 |
meth=meth,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
|
neuper@37906
|
1134 |
| repl_spec _ _ = raise PTREE "repl_domID takes no PrfObj";
|
neuper@37906
|
1135 |
fun repl_domID x (PblObj {cell=cell,origin=origin,fmz=fmz,
|
neuper@37906
|
1136 |
spec=(_,p,m),probl=probl,meth=meth,env=env,loc=loc,
|
neuper@37906
|
1137 |
branch=branch,result=result,ostate=ostate}) =
|
neuper@37906
|
1138 |
PblObj {cell=cell,origin=origin,fmz=fmz,spec=(x,p,m),probl=probl,
|
neuper@37906
|
1139 |
meth=meth,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
|
neuper@37906
|
1140 |
| repl_domID _ _ = raise PTREE "repl_domID takes no PrfObj";
|
neuper@37906
|
1141 |
fun repl_pblID x (PblObj {cell=cell,origin=origin,fmz=fmz,
|
neuper@37906
|
1142 |
spec=(d,_,m),probl=probl,meth=meth,env=env,loc=loc,
|
neuper@37906
|
1143 |
branch=branch,result=result,ostate=ostate}) =
|
neuper@37906
|
1144 |
PblObj {cell=cell,origin=origin,fmz=fmz,spec=(d,x,m),probl=probl,
|
neuper@37906
|
1145 |
meth=meth,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
|
neuper@37906
|
1146 |
| repl_pblID _ _ = raise PTREE "repl_pblID takes no PrfObj";
|
neuper@37906
|
1147 |
fun repl_metID x (PblObj {cell=cell,origin=origin,fmz=fmz,
|
neuper@37906
|
1148 |
spec=(d,p,_),probl=probl,meth=meth,env=env,loc=loc,
|
neuper@37906
|
1149 |
branch=branch,result=result,ostate=ostate}) =
|
neuper@37906
|
1150 |
PblObj {cell=cell,origin=origin,fmz=fmz,spec=(d,p,x),probl=probl,
|
neuper@37906
|
1151 |
meth=meth,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
|
neuper@37906
|
1152 |
| repl_metID _ _ = raise PTREE "repl_metID takes no PrfObj";
|
neuper@37906
|
1153 |
|
neuper@37906
|
1154 |
fun repl_result l f' s (PrfObj {cell=cell,form=form,tac=tac,loc=_,
|
neuper@37906
|
1155 |
branch=branch,result = _ ,ostate = _}) =
|
neuper@37906
|
1156 |
PrfObj {cell=cell,form=form,tac=tac,loc= l,
|
neuper@37906
|
1157 |
branch=branch,result = f',ostate = s}
|
neuper@37906
|
1158 |
| repl_result l f' s (PblObj {cell=cell,origin=origin,fmz=fmz,
|
neuper@37906
|
1159 |
spec=spec,probl=probl,meth=meth,env=env,loc=_,
|
neuper@37906
|
1160 |
branch=branch,result= _ ,ostate= _}) =
|
neuper@37906
|
1161 |
PblObj {cell=cell,origin=origin,fmz=fmz,
|
neuper@37906
|
1162 |
spec=spec,probl=probl,meth=meth,env=env,loc= l,
|
neuper@37906
|
1163 |
branch=branch,result= f',ostate= s};
|
neuper@37906
|
1164 |
|
neuper@37906
|
1165 |
fun repl_tac x (PrfObj {cell=cell,form=form,tac= _,loc=loc,
|
neuper@37906
|
1166 |
branch=branch,result=result,ostate=ostate}) =
|
neuper@37906
|
1167 |
PrfObj {cell=cell,form=form,tac= x,loc=loc,
|
neuper@37906
|
1168 |
branch=branch,result=result,ostate=ostate}
|
neuper@37906
|
1169 |
| repl_tac _ _ = raise PTREE "repl_tac takes no PblObj";
|
neuper@37906
|
1170 |
|
neuper@37906
|
1171 |
fun repl_branch b (PblObj {cell=cell,origin=origin,fmz=fmz,
|
neuper@37906
|
1172 |
spec=spec,probl=probl,meth=meth,env=env,loc=loc,
|
neuper@37906
|
1173 |
branch= _,result=result,ostate=ostate}) =
|
neuper@37906
|
1174 |
PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,
|
neuper@37906
|
1175 |
meth=meth,env=env,loc=loc,branch= b,result=result,ostate=ostate}
|
neuper@37906
|
1176 |
| repl_branch b (PrfObj {cell=cell,form=form,tac=tac,loc=loc,
|
neuper@37906
|
1177 |
branch= _,result=result,ostate=ostate}) =
|
neuper@37906
|
1178 |
PrfObj {cell=cell,form=form,tac=tac,loc=loc,
|
neuper@37906
|
1179 |
branch= b,result=result,ostate=ostate};
|
neuper@37906
|
1180 |
|
neuper@37906
|
1181 |
fun repl_env e
|
neuper@37906
|
1182 |
(PblObj {cell=cell,origin=origin,fmz=fmz,
|
neuper@37906
|
1183 |
spec=spec,probl=probl,meth=meth,env=_,loc=loc,
|
neuper@37906
|
1184 |
branch=branch,result=result,ostate=ostate}) =
|
neuper@37906
|
1185 |
PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,
|
neuper@37906
|
1186 |
meth=meth,env=e,loc=loc,branch=branch,
|
neuper@37906
|
1187 |
result=result,ostate=ostate}
|
neuper@37906
|
1188 |
| repl_env _ _ = raise PTREE "repl_ets takes no PrfObj";
|
neuper@37906
|
1189 |
|
neuper@37906
|
1190 |
fun repl_oris oris
|
neuper@37906
|
1191 |
(PblObj {cell=cell,origin=(_,spe,hdf),fmz=fmz,
|
neuper@37906
|
1192 |
spec=spec,probl=probl,meth=meth,env=env,loc=loc,
|
neuper@37906
|
1193 |
branch=branch,result=result,ostate=ostate}) =
|
neuper@37906
|
1194 |
PblObj{cell=cell,origin=(oris,spe,hdf),fmz=fmz,spec=spec,probl=probl,
|
neuper@37906
|
1195 |
meth=meth,env=env,loc=loc,branch=branch,
|
neuper@37906
|
1196 |
result=result,ostate=ostate}
|
neuper@37906
|
1197 |
| repl_oris _ _ = raise PTREE "repl_oris takes no PrfObj";
|
neuper@37906
|
1198 |
fun repl_orispec spe
|
neuper@37906
|
1199 |
(PblObj {cell=cell,origin=(oris,_,hdf),fmz=fmz,
|
neuper@37906
|
1200 |
spec=spec,probl=probl,meth=meth,env=env,loc=loc,
|
neuper@37906
|
1201 |
branch=branch,result=result,ostate=ostate}) =
|
neuper@37906
|
1202 |
PblObj{cell=cell,origin=(oris,spe,hdf),fmz=fmz,spec=spec,probl=probl,
|
neuper@37906
|
1203 |
meth=meth,env=env,loc=loc,branch=branch,
|
neuper@37906
|
1204 |
result=result,ostate=ostate}
|
neuper@37906
|
1205 |
| repl_orispec _ _ = raise PTREE "repl_orispec takes no PrfObj";
|
neuper@37906
|
1206 |
|
neuper@37906
|
1207 |
fun repl_loc l (PblObj {cell=cell,origin=origin,fmz=fmz,
|
neuper@37906
|
1208 |
spec=spec,probl=probl,meth=meth,env=env,loc=_,
|
neuper@37906
|
1209 |
branch=branch,result=result,ostate=ostate}) =
|
neuper@37906
|
1210 |
PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,
|
neuper@37906
|
1211 |
meth=meth,env=env,loc=l,branch=branch,result=result,ostate=ostate}
|
neuper@37906
|
1212 |
| repl_loc l (PrfObj {cell=cell,form=form,tac=tac,loc=_,
|
neuper@37906
|
1213 |
branch=branch,result=result,ostate=ostate}) =
|
neuper@37906
|
1214 |
PrfObj {cell=cell,form=form,tac=tac,loc= l,
|
neuper@37906
|
1215 |
branch=branch,result=result,ostate=ostate};
|
neuper@37906
|
1216 |
(*
|
neuper@37906
|
1217 |
fun uni__cid cell'
|
neuper@37906
|
1218 |
(PblObj {cell=cell,origin=origin,fmz=fmz,
|
neuper@37906
|
1219 |
spec=spec,probl=probl,meth=meth,env=env,loc=loc,
|
neuper@37906
|
1220 |
branch=branch,result=result,ostate=ostate}) =
|
neuper@37906
|
1221 |
PblObj {cell=cell union cell',origin=origin,fmz=fmz,spec=spec,probl=probl,
|
neuper@37906
|
1222 |
meth=meth,env=env,loc=loc,branch=branch,
|
neuper@37906
|
1223 |
result=result,ostate=ostate}
|
neuper@37906
|
1224 |
| uni__cid cell'
|
neuper@37906
|
1225 |
(PrfObj {cell=cell,form=form,tac=tac,loc=loc,
|
neuper@37906
|
1226 |
branch=branch,result=result,ostate=ostate}) =
|
neuper@37906
|
1227 |
PrfObj {cell=cell union cell',form=form,tac=tac,loc=loc,
|
neuper@37906
|
1228 |
branch=branch,result=result,ostate=ostate};
|
neuper@37906
|
1229 |
*)
|
neuper@37906
|
1230 |
|
neuper@37906
|
1231 |
(*WN050219 put here for interpreting code for cut_tree below...*)
|
neuper@37906
|
1232 |
type ocalhd =
|
neuper@37906
|
1233 |
bool * (*ALL itms+preconds true*)
|
neuper@37906
|
1234 |
pos_ * (*model belongs to Problem | Method*)
|
neuper@37906
|
1235 |
term * (*header: Problem... or Cas
|
neuper@37906
|
1236 |
FIXXXME.12.03: item! for marking syntaxerrors*)
|
neuper@37906
|
1237 |
itm list * (*model: given, find, relate*)
|
neuper@37906
|
1238 |
((bool * term) list) *(*model: preconds*)
|
neuper@37906
|
1239 |
spec; (*specification*)
|
neuper@37906
|
1240 |
val e_ocalhd = (false, Und, e_term, [e_itm], [(false, e_term)], e_spec);
|
neuper@37906
|
1241 |
|
neuper@37906
|
1242 |
datatype ptform =
|
neuper@37906
|
1243 |
Form of term
|
neuper@37906
|
1244 |
| ModSpec of ocalhd;
|
neuper@37906
|
1245 |
val e_ptform = Form e_term;
|
neuper@37906
|
1246 |
val e_ptform' = ModSpec e_ocalhd;
|
neuper@37906
|
1247 |
|
neuper@37906
|
1248 |
|
neuper@37906
|
1249 |
|
neuper@37906
|
1250 |
(*.applies (snd f) to the branches at a pos if ((fst f) b),
|
neuper@37906
|
1251 |
f : (ppobj -> bool) * (int -> ptree list -> ptree list).*)
|
neuper@37906
|
1252 |
|
neuper@37906
|
1253 |
fun appl_branch f EmptyPtree [] = (EmptyPtree, false)
|
neuper@37906
|
1254 |
| appl_branch f EmptyPtree _ = raise PTREE "appl_branch f Empty _"
|
neuper@37906
|
1255 |
| appl_branch f (Nd ( _, _)) [] = raise PTREE "appl_branch f _ []"
|
neuper@37906
|
1256 |
| appl_branch f (Nd (b, bs)) (p::[]) =
|
neuper@37906
|
1257 |
if (fst f) b then (Nd (b, (snd f) (p:posel) bs), true)
|
neuper@37906
|
1258 |
else (Nd (b, bs), false)
|
neuper@37906
|
1259 |
| appl_branch f (Nd (b, bs)) (p::ps) =
|
neuper@37906
|
1260 |
let val (b',bool) = appl_branch f (nth p bs) ps
|
neuper@37906
|
1261 |
in (Nd (b, repl_app bs p b'), bool) end;
|
neuper@37906
|
1262 |
|
neuper@37906
|
1263 |
(* for cut_level; appl_branch(deprecated) *)
|
neuper@37906
|
1264 |
fun test_trans (PrfObj{branch = Transitive,...}) = true
|
neuper@37906
|
1265 |
| test_trans (PblObj{branch = Transitive,...}) = true
|
neuper@37906
|
1266 |
| test_trans _ = false;
|
neuper@37906
|
1267 |
|
neuper@37906
|
1268 |
fun is_pblobj' pt (p:pos) =
|
neuper@37906
|
1269 |
let val ppobj = get_obj I pt p
|
neuper@37906
|
1270 |
in is_pblobj ppobj end;
|
neuper@37906
|
1271 |
|
neuper@37906
|
1272 |
|
neuper@37906
|
1273 |
fun delete_result pt (p:pos) =
|
neuper@37925
|
1274 |
(appl_obj (repl_result (fst (get_obj g_loc pt p), NONE)
|
neuper@37906
|
1275 |
(e_term,[]) Incomplete) pt p);
|
neuper@37906
|
1276 |
|
neuper@37906
|
1277 |
fun del_res (PblObj {cell, fmz, origin, spec, probl, meth,
|
neuper@37906
|
1278 |
env, loc=(l1,_), branch, result, ostate}) =
|
neuper@37906
|
1279 |
PblObj {cell=cell,fmz=fmz,origin=origin,spec=spec,probl=probl,meth=meth,
|
neuper@37925
|
1280 |
env=env, loc=(l1,NONE), branch=branch, result=(e_term,[]),
|
neuper@37906
|
1281 |
ostate=Incomplete}
|
neuper@37906
|
1282 |
|
neuper@37906
|
1283 |
| del_res (PrfObj {cell, form, tac, loc=(l1,_), branch, result, ostate}) =
|
neuper@37925
|
1284 |
PrfObj {cell=cell,form=form,tac=tac, loc=(l1,NONE), branch=branch,
|
neuper@37906
|
1285 |
result=(e_term,[]), ostate=Incomplete};
|
neuper@37906
|
1286 |
|
neuper@37906
|
1287 |
|
neuper@37906
|
1288 |
(*
|
neuper@37906
|
1289 |
fun update_fmz pt pos x = appl_obj (repl_fmz x) pt pos;
|
neuper@37906
|
1290 |
1.00 not used anymore*)
|
neuper@37906
|
1291 |
|
neuper@37906
|
1292 |
(*FIXME.WN.12.03: update_X X pos pt -> pt could be chained by o (efficiency?)*)
|
neuper@37906
|
1293 |
fun update_env pt pos x = appl_obj (repl_env x) pt pos;
|
neuper@37906
|
1294 |
fun update_domID pt pos x = appl_obj (repl_domID x) pt pos;
|
neuper@37906
|
1295 |
fun update_pblID pt pos x = appl_obj (repl_pblID x) pt pos;
|
neuper@37906
|
1296 |
fun update_metID pt pos x = appl_obj (repl_metID x) pt pos;
|
neuper@37906
|
1297 |
fun update_spec pt pos x = appl_obj (repl_spec x) pt pos;
|
neuper@37906
|
1298 |
|
neuper@37906
|
1299 |
fun update_pbl pt pos x = appl_obj (repl_pbl x) pt pos;
|
neuper@37906
|
1300 |
fun update_pblppc pt pos x = appl_obj (repl_pbl x) pt pos;
|
neuper@37906
|
1301 |
|
neuper@37906
|
1302 |
fun update_met pt pos x = appl_obj (repl_met x) pt pos;
|
neuper@37906
|
1303 |
(*1.09.01 ----
|
neuper@37906
|
1304 |
fun update_metppc pt pos x =
|
neuper@37906
|
1305 |
let val {rew_ord'=od,rls'=rs,asm_thm=at,asm_rls=ar,...} =
|
neuper@37906
|
1306 |
get_obj g_met pt pos
|
neuper@37906
|
1307 |
in appl_obj (repl_met
|
neuper@37906
|
1308 |
{rew_ord'=od,rls'=rs,asm_thm=at,asm_rls=ar,ppc=x})
|
neuper@37906
|
1309 |
pt pos end;*)
|
neuper@37906
|
1310 |
fun update_metppc pt pos x = appl_obj (repl_met x) pt pos;
|
neuper@37906
|
1311 |
|
neuper@37906
|
1312 |
(*fun union_cid pt pos x = appl_obj (uni__cid x) pt pos;*)
|
neuper@37906
|
1313 |
|
neuper@37906
|
1314 |
fun update_branch pt pos x = appl_obj (repl_branch x) pt pos;
|
neuper@37906
|
1315 |
fun update_tac pt pos x = appl_obj (repl_tac x) pt pos;
|
neuper@37906
|
1316 |
|
neuper@37906
|
1317 |
fun update_oris pt pos x = appl_obj (repl_oris x) pt pos;
|
neuper@37906
|
1318 |
fun update_orispec pt pos x = appl_obj (repl_orispec x) pt pos;
|
neuper@37906
|
1319 |
|
neuper@37906
|
1320 |
(*done by append_* !! 3.5.02; ununsed WN050305 thus outcommented
|
neuper@37925
|
1321 |
fun update_loc pt (p,_) (ScrState ([],[],NONE,
|
neuper@37906
|
1322 |
Const ("empty",_),Sundef,false)) =
|
neuper@37925
|
1323 |
appl_obj (repl_loc (NONE,NONE)) pt p
|
neuper@37906
|
1324 |
| update_loc pt (p,Res) x =
|
neuper@37906
|
1325 |
let val (lform,_) = get_obj g_loc pt p
|
neuper@37925
|
1326 |
in appl_obj (repl_loc (lform,SOME x)) pt p end
|
neuper@37906
|
1327 |
|
neuper@37906
|
1328 |
| update_loc pt (p,_) x =
|
neuper@37906
|
1329 |
let val (_,lres) = get_obj g_loc pt p
|
neuper@37925
|
1330 |
in appl_obj (repl_loc (SOME x,lres)) pt p end;-------------*)
|
neuper@37906
|
1331 |
|
neuper@37906
|
1332 |
(*WN050305 for handling cut_tree in cappend_atomic -- TODO redesign !*)
|
neuper@37906
|
1333 |
fun update_loc' pt p iss = appl_obj (repl_loc iss) pt p;
|
neuper@37906
|
1334 |
|
neuper@37906
|
1335 |
(*13.8.02---------------------------
|
neuper@37925
|
1336 |
fun get_loc EmptyPtree _ = NONE
|
neuper@37906
|
1337 |
| get_loc pt (p,Res) =
|
neuper@37906
|
1338 |
let val (lfrm,lres) = get_obj g_loc pt p
|
neuper@37906
|
1339 |
in if lres = e_istate then lfrm else lres end
|
neuper@37906
|
1340 |
| get_loc pt (p,_) =
|
neuper@37906
|
1341 |
let val (lfrm,lres) = get_obj g_loc pt p
|
neuper@37906
|
1342 |
in if lfrm = e_istate then lres else lfrm end; 5.10.00: too liberal ?*)
|
neuper@37906
|
1343 |
(*13.8.02: options, because istate is no equalitype any more*)
|
neuper@37906
|
1344 |
fun get_loc EmptyPtree _ = e_istate
|
neuper@37906
|
1345 |
| get_loc pt (p,Res) =
|
neuper@37906
|
1346 |
(case get_obj g_loc pt p of
|
neuper@37925
|
1347 |
(SOME i, NONE) => i
|
neuper@37925
|
1348 |
| (NONE , NONE) => e_istate
|
neuper@37925
|
1349 |
| (_ , SOME i) => i)
|
neuper@37906
|
1350 |
| get_loc pt (p,_) =
|
neuper@37906
|
1351 |
(case get_obj g_loc pt p of
|
neuper@37925
|
1352 |
(NONE , SOME i) => i (*13.8.02 just copied from ^^^: too liberal ?*)
|
neuper@37925
|
1353 |
| (NONE , NONE) => e_istate
|
neuper@37925
|
1354 |
| (SOME i, _) => i);
|
neuper@37906
|
1355 |
val get_istate = get_loc; (*3.5.02*)
|
neuper@37906
|
1356 |
|
neuper@37906
|
1357 |
(*.collect the assumptions within a problem up to a certain position.*)
|
neuper@37906
|
1358 |
type asms = (term * pos) list;(*WN0502 should be (pos' * term) list
|
neuper@37906
|
1359 |
...........===^===*)
|
neuper@37906
|
1360 |
|
neuper@37906
|
1361 |
fun get_asm (b:pos, p:pos) (Nd (PblObj {result=(_,asm),...},_)) =
|
neuper@37906
|
1362 |
((*writeln ("### get_asm PblObj:(b,p)= "^
|
neuper@37906
|
1363 |
(pair2str(ints2str b, ints2str p)));*)
|
neuper@37906
|
1364 |
(map (rpair b) asm):asms)
|
neuper@37906
|
1365 |
| get_asm (b, p) (Nd (PrfObj {result=(_,asm),...}, [])) =
|
neuper@37906
|
1366 |
((*writeln ("### get_asm PrfObj []:(b,p)= "^
|
neuper@37906
|
1367 |
(pair2str(ints2str b, ints2str p)));*)
|
neuper@37906
|
1368 |
(map (rpair b) asm))
|
neuper@37906
|
1369 |
| get_asm (b, p:pos) (Nd (PrfObj _, nds)) =
|
neuper@37906
|
1370 |
let (*val _= writeln ("### get_asm PrfObj nds:(b,p)= "^
|
neuper@37906
|
1371 |
(pair2str(ints2str b, ints2str p)));*)
|
neuper@37906
|
1372 |
val levdn =
|
neuper@37906
|
1373 |
if p <> [] then (b @ [hd p]:pos, tl p:pos)
|
neuper@37906
|
1374 |
else (b @ [1], [99999]) (*_deeper_ nesting is always _before_ p*)
|
neuper@37906
|
1375 |
in gets_asm levdn 1 nds end
|
neuper@37906
|
1376 |
and gets_asm _ _ [] = []
|
neuper@37906
|
1377 |
| gets_asm (b, p' as p::ps) i (nd::nds) =
|
neuper@37906
|
1378 |
if p < i then []
|
neuper@37906
|
1379 |
else ((*writeln ("### gets_asm: (b,p')= "^(pair2str(ints2str b,
|
neuper@37906
|
1380 |
ints2str p')));*)
|
neuper@37906
|
1381 |
(get_asm (b @ [i], ps) nd) @ (gets_asm (b, p') (i + 1) nds));
|
neuper@37906
|
1382 |
|
neuper@37906
|
1383 |
fun get_assumptions_ (Nd (PblObj {result=(r,asm),...}, cn)) (([], _):pos') =
|
neuper@37906
|
1384 |
if r = e_term then gets_asm ([], [99999]) 1 cn
|
neuper@37906
|
1385 |
else map (rpair []) asm
|
neuper@37906
|
1386 |
| get_assumptions_ pt (p,p_) =
|
neuper@37906
|
1387 |
let val (cn, base) = par_children pt p
|
neuper@37906
|
1388 |
val offset = drop (length base, p)
|
neuper@37906
|
1389 |
val base' = replicate (length base) 1
|
neuper@37906
|
1390 |
val offset' = case p_ of
|
neuper@37906
|
1391 |
Frm => let val (qs,q) = split_last offset
|
neuper@37906
|
1392 |
in qs @ [q - 1] end
|
neuper@37906
|
1393 |
| _ => offset
|
neuper@37906
|
1394 |
(*val _= writeln ("... get_assumptions: (b,o)= "^
|
neuper@37906
|
1395 |
(pair2str(ints2str base',ints2str offset)))*)
|
neuper@37906
|
1396 |
in gets_asm (base', offset) 1 cn end;
|
neuper@37906
|
1397 |
|
neuper@37906
|
1398 |
|
neuper@37906
|
1399 |
(*---------
|
neuper@37906
|
1400 |
end
|
neuper@37906
|
1401 |
|
neuper@37906
|
1402 |
open Ptree;
|
neuper@37906
|
1403 |
----------*)
|
neuper@37906
|
1404 |
|
neuper@37906
|
1405 |
(*pos of the formula on FE relative to the current pos,
|
neuper@37906
|
1406 |
which is the next writepos*)
|
neuper@37906
|
1407 |
fun pre_pos ([]:pos) = []:pos
|
neuper@37906
|
1408 |
| pre_pos pp =
|
neuper@37906
|
1409 |
let val (ps,p) = split_last pp
|
neuper@37906
|
1410 |
in case p of 1 => ps | n => ps @ [n-1] end;
|
neuper@37906
|
1411 |
|
neuper@37906
|
1412 |
(*WN.20.5.03 ... but not used*)
|
neuper@37906
|
1413 |
fun posless [] (_::_) = true
|
neuper@37906
|
1414 |
| posless (_::_) [] = false
|
neuper@37906
|
1415 |
| posless (p::ps) (q::qs) = if p = q then posless ps qs else p < q;
|
neuper@37906
|
1416 |
(* posless [2,3,4] [3,4,5];
|
neuper@37906
|
1417 |
true
|
neuper@37906
|
1418 |
> posless [2,3,4] [1,2,3];
|
neuper@37906
|
1419 |
false
|
neuper@37906
|
1420 |
> posless [2,3] [2,3,4];
|
neuper@37906
|
1421 |
true
|
neuper@37906
|
1422 |
> posless [2,3,4] [2,3];
|
neuper@37906
|
1423 |
false
|
neuper@37906
|
1424 |
> posless [6] [6,5,2];
|
neuper@37906
|
1425 |
true
|
neuper@37906
|
1426 |
+++ see Isabelle/../library.ML*)
|
neuper@37906
|
1427 |
|
neuper@37906
|
1428 |
|
neuper@37906
|
1429 |
(**.development for extracting an 'interval' from ptree.**)
|
neuper@37906
|
1430 |
|
neuper@37906
|
1431 |
(*version 1 stopped 8.03 in favour of get_interval with !!!move_dn
|
neuper@37906
|
1432 |
actually used (inefficient) version with move_dn: see modspec.sml*)
|
neuper@37906
|
1433 |
local
|
neuper@37906
|
1434 |
|
neuper@37906
|
1435 |
fun hdp [] = 1 | hdp [0] = 1 | hdp x = hd x;(*start with first*)
|
neuper@37906
|
1436 |
fun hdq [] = 99999 | hdq [0] = 99999 | hdq x = hd x;(*take until last*)
|
neuper@37906
|
1437 |
fun tlp [] = [0] | tlp [_] = [0] | tlp x = tl x;
|
neuper@37906
|
1438 |
fun tlq [] = [99999] | tlq [_] = [99999] | tlq x = tl x;
|
neuper@37906
|
1439 |
|
neuper@37906
|
1440 |
fun getnd i (b,p) q (Nd (po, nds)) =
|
neuper@37906
|
1441 |
(if i <= 0 then [[b]] else []) @
|
neuper@37906
|
1442 |
(getnds (i-1) true (b@[hdp p], tlp p) (tlq q)
|
neuper@37906
|
1443 |
(take_fromto (hdp p) (hdq q) nds))
|
neuper@37906
|
1444 |
|
neuper@37906
|
1445 |
and getnds _ _ _ _ [] = [] (*no children*)
|
neuper@37906
|
1446 |
| getnds i _ (b,p) q [nd] = (getnd i (b,p) q nd) (*l+r-margin*)
|
neuper@37906
|
1447 |
|
neuper@37906
|
1448 |
| getnds i true (b,p) q [n1, n2] = (*l-margin, r-margin*)
|
neuper@37906
|
1449 |
(getnd i ( b, p ) [99999] n1) @
|
neuper@37906
|
1450 |
(getnd ~99999 (lev_on b,[0]) q n2)
|
neuper@37906
|
1451 |
|
neuper@37906
|
1452 |
| getnds i _ (b,p) q [n1, n2] = (*intern, r-margin*)
|
neuper@37906
|
1453 |
(getnd i ( b,[0]) [99999] n1) @
|
neuper@37906
|
1454 |
(getnd ~99999 (lev_on b,[0]) q n2)
|
neuper@37906
|
1455 |
|
neuper@37906
|
1456 |
| getnds i true (b,p) q (nd::(nds as _::_)) = (*l-margin, intern*)
|
neuper@37906
|
1457 |
(getnd i ( b, p ) [99999] nd) @
|
neuper@37906
|
1458 |
(getnds ~99999 false (lev_on b,[0]) q nds)
|
neuper@37906
|
1459 |
|
neuper@37906
|
1460 |
| getnds i _ (b,p) q (nd::(nds as _::_)) = (*intern, ...*)
|
neuper@37906
|
1461 |
(getnd i ( b,[0]) [99999] nd) @
|
neuper@37906
|
1462 |
(getnds ~99999 false (lev_on b,[0]) q nds);
|
neuper@37906
|
1463 |
in
|
neuper@37906
|
1464 |
(*get an 'interval from to' from a ptree as 'intervals f t' of respective nodes
|
neuper@37906
|
1465 |
where 'from' are pos, i.e. a key as int list, 'f' an int (to,t analoguous)
|
neuper@37906
|
1466 |
(1) the 'f' are given
|
neuper@37906
|
1467 |
(1a) by 'from' if 'f' = the respective element of 'from' (left margin)
|
neuper@37906
|
1468 |
(1b) -inifinity, if 'f' > the respective element of 'from' (internal node)
|
neuper@37906
|
1469 |
(2) the 't' ar given
|
neuper@37906
|
1470 |
(2a) by 'to' if 't' = the respective element of 'to' (right margin)
|
neuper@37906
|
1471 |
(2b) inifinity, if 't' < the respective element of 'to (internal node)'
|
neuper@37906
|
1472 |
the 'f' and 't' are set by hdp,... *)
|
neuper@37906
|
1473 |
fun get_trace pt p q =
|
neuper@37906
|
1474 |
(flat o (getnds ((length p) -1) true ([hdp p], tlp p) (tlq q)))
|
neuper@37906
|
1475 |
(take_fromto (hdp p) (hdq q) (children pt));
|
neuper@37906
|
1476 |
end;
|
neuper@37906
|
1477 |
(*WN0510 stoppde this development;
|
neuper@37906
|
1478 |
actually used (inefficient) version with move_dn: getFormulaeFromTo*)
|
neuper@37906
|
1479 |
|
neuper@37906
|
1480 |
|
neuper@37906
|
1481 |
|
neuper@37906
|
1482 |
|
neuper@37906
|
1483 |
fun get_somespec ((dI,pI,mI):spec) ((dI',pI',mI'):spec) =
|
neuper@37906
|
1484 |
let val domID = if dI = e_domID
|
neuper@37906
|
1485 |
then if dI' = e_domID
|
neuper@37906
|
1486 |
then raise error"pt_extract: no domID in probl,origin"
|
neuper@37906
|
1487 |
else dI'
|
neuper@37906
|
1488 |
else dI
|
neuper@37906
|
1489 |
val pblID = if pI = e_pblID
|
neuper@37906
|
1490 |
then if pI' = e_pblID
|
neuper@37906
|
1491 |
then raise error"pt_extract: no pblID in probl,origin"
|
neuper@37906
|
1492 |
else pI'
|
neuper@37906
|
1493 |
else pI
|
neuper@37906
|
1494 |
val metID = if mI = e_metID
|
neuper@37906
|
1495 |
then if pI' = e_metID
|
neuper@37906
|
1496 |
then raise error"pt_extract: no metID in probl,origin"
|
neuper@37906
|
1497 |
else mI'
|
neuper@37906
|
1498 |
else mI
|
neuper@37906
|
1499 |
in (domID, pblID, metID):spec end;
|
neuper@37906
|
1500 |
fun get_somespec' ((dI,pI,mI):spec) ((dI',pI',mI'):spec) =
|
neuper@37906
|
1501 |
let val domID = if dI = e_domID then dI' else dI
|
neuper@37906
|
1502 |
val pblID = if pI = e_pblID then pI' else pI
|
neuper@37906
|
1503 |
val metID = if mI = e_metID then mI' else mI
|
neuper@37906
|
1504 |
in (domID, pblID, metID):spec end;
|
neuper@37906
|
1505 |
|
neuper@37906
|
1506 |
(*extract a formula or model from ptree for itms2itemppc or model2xml*)
|
neuper@37906
|
1507 |
fun preconds2str bts =
|
neuper@37906
|
1508 |
(strs2str o (map (linefeed o pair2str o
|
neuper@37906
|
1509 |
(apsnd term2str) o
|
neuper@37906
|
1510 |
(apfst bool2str)))) bts;
|
neuper@37906
|
1511 |
fun ocalhd2str ((b, p, hdf, itms, prec, spec):ocalhd) =
|
neuper@37906
|
1512 |
"("^bool2str b^", "^pos_2str p^", "^term2str hdf^
|
neuper@37925
|
1513 |
", "^itms2str_ (thy2ctxt "Isac") itms^
|
neuper@37906
|
1514 |
", "^preconds2str prec^", \n"^spec2str spec^" )";
|
neuper@37906
|
1515 |
|
neuper@37906
|
1516 |
|
neuper@37906
|
1517 |
|
neuper@37906
|
1518 |
fun is_pblnd (Nd (ppobj, _)) = is_pblobj ppobj;
|
neuper@37906
|
1519 |
|
neuper@37906
|
1520 |
|
neuper@37906
|
1521 |
(**.functions for the 'ptree iterator' as seen from the FE-Kernel interface.**)
|
neuper@37906
|
1522 |
|
neuper@37906
|
1523 |
(*move one step down into existing nodes of ptree; regard TransitiveB
|
neuper@37906
|
1524 |
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~##################
|
neuper@37906
|
1525 |
fun move_dn _ (Nd (c, ns)) ([],p_) = (*root problem*)
|
neuper@37906
|
1526 |
(* val (Nd (c, ns), ([],p_)) = (pt, get_pos cI uI);
|
neuper@37906
|
1527 |
*)
|
neuper@37906
|
1528 |
if is_pblobj c
|
neuper@37906
|
1529 |
then case p_ of (*Frm => ([], Pbl) 1.12.03
|
neuper@37906
|
1530 |
|*) Res => raise PTREE "move_dn: end of calculation"
|
neuper@37906
|
1531 |
| _ => if null ns (*go down from Pbl + Met*)
|
neuper@37906
|
1532 |
then raise PTREE "move_dn: solve problem not started"
|
neuper@37906
|
1533 |
else ([1], Frm)
|
neuper@37906
|
1534 |
else (case p_ of Res => raise PTREE "move_dn: end of (sub-)tree"
|
neuper@37906
|
1535 |
| _ => if null ns
|
neuper@37906
|
1536 |
then raise PTREE "move_dn: pos not existent 1"
|
neuper@37906
|
1537 |
else ([1], Frm))
|
neuper@37906
|
1538 |
|
neuper@37906
|
1539 |
(*iterate towards end of pos*)
|
neuper@37906
|
1540 |
(* val (P,(Nd (_, ns)),(p::(ps as (_::_)),p_)) = ([]:pos, pt, get_pos cI uI);
|
neuper@37906
|
1541 |
val (P,(Nd (_, ns)),(p::(ps as (_::_)),p_)) = ((P@[p]),(nth p ns),(ps, p_));
|
neuper@37906
|
1542 |
*)
|
neuper@37906
|
1543 |
| move_dn P (Nd (_, ns)) (p::(ps as (_::_)),p_) =
|
neuper@37906
|
1544 |
if p > length ns then raise PTREE "move_dn: pos not existent 2"
|
neuper@37906
|
1545 |
else move_dn ((P@[p]): pos) (nth p ns) (ps, p_)
|
neuper@37906
|
1546 |
(* val (P, (Nd (c, ns)), ([p], p_)) = ((P@[p]), (nth p ns), (ps, p_));
|
neuper@37906
|
1547 |
val (P, (Nd (c, ns)), ([p], p_)) = ([],pt,get_pos cI uI);
|
neuper@37906
|
1548 |
*)
|
neuper@37906
|
1549 |
| move_dn P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*)
|
neuper@37906
|
1550 |
if p > length ns then raise PTREE "move_dn: pos not existent 3"
|
neuper@37906
|
1551 |
else if is_pblnd (nth p ns) then
|
neuper@37906
|
1552 |
((*writeln("### move_dn: is_pblnd (nth p ns), P= "^ints2str' P^", \n"^
|
neuper@37906
|
1553 |
"length ns= "^((string_of_int o length) ns)^
|
neuper@37906
|
1554 |
", p= "^string_of_int p^", p_= "^pos_2str p_);*)
|
neuper@37906
|
1555 |
case p_ of Res => if p = length ns
|
neuper@37906
|
1556 |
then if g_ostate c = Complete then (P, Res)
|
neuper@37906
|
1557 |
else raise PTREE (ints2str' P^" not complete")
|
neuper@37906
|
1558 |
(*FIXME here handle not-sequent-branches*)
|
neuper@37906
|
1559 |
else if g_branch c = TransitiveB
|
neuper@37906
|
1560 |
andalso (not o is_pblnd o (nth (p+1))) ns
|
neuper@37906
|
1561 |
then (P@[p+1], Res)
|
neuper@37906
|
1562 |
else (P@[p+1], if is_pblnd (nth (p+1) ns)
|
neuper@37906
|
1563 |
then Pbl else Frm)
|
neuper@37906
|
1564 |
| _ => if (null o children o (nth p)) ns (*go down from Pbl*)
|
neuper@37906
|
1565 |
then raise PTREE "move_dn: solve subproblem not started"
|
neuper@37906
|
1566 |
else (P @ [p, 1],
|
neuper@37906
|
1567 |
if (is_pblnd o hd o children o (nth p)) ns
|
neuper@37906
|
1568 |
then Pbl else Frm)
|
neuper@37906
|
1569 |
)
|
neuper@37906
|
1570 |
(* val (P, Nd (c, ns), ([p], p_)) = ([], pt, ([1], Frm));
|
neuper@37906
|
1571 |
*)
|
neuper@37906
|
1572 |
else case p_ of Frm => if (null o children o (nth p)) ns
|
neuper@37906
|
1573 |
(*then if g_ostate c = Complete then (P@[p],Res)*)
|
neuper@37906
|
1574 |
then if g_ostate' (nth p ns) = Complete
|
neuper@37906
|
1575 |
then (P@[p],Res)
|
neuper@37906
|
1576 |
else raise PTREE "move_dn: pos not existent 4"
|
neuper@37906
|
1577 |
else (P @ [p, 1], (*go down*)
|
neuper@37906
|
1578 |
if (is_pblnd o hd o children o (nth p)) ns
|
neuper@37906
|
1579 |
then Pbl else Frm)
|
neuper@37906
|
1580 |
| Res => if p = length ns
|
neuper@37906
|
1581 |
then
|
neuper@37906
|
1582 |
if g_ostate c = Complete then (P, Res)
|
neuper@37906
|
1583 |
else raise PTREE (ints2str' P^" not complete")
|
neuper@37906
|
1584 |
else
|
neuper@37906
|
1585 |
if g_branch c = TransitiveB
|
neuper@37906
|
1586 |
andalso (not o is_pblnd o (nth (p+1))) ns
|
neuper@37906
|
1587 |
then if (null o children o (nth (p+1))) ns
|
neuper@37906
|
1588 |
then (P@[p+1], Res)
|
neuper@37906
|
1589 |
else (P@[p+1,1], Frm)(*040221*)
|
neuper@37906
|
1590 |
else (P@[p+1], if is_pblnd (nth (p+1) ns)
|
neuper@37906
|
1591 |
then Pbl else Frm);
|
neuper@37906
|
1592 |
*)
|
neuper@37906
|
1593 |
(*.move one step down into existing nodes of ptree; skip Res = Frm.nxt;
|
neuper@37906
|
1594 |
move_dn at the end of the calc-tree raises PTREE.*)
|
neuper@37906
|
1595 |
fun move_dn _ (Nd (c, ns)) ([],p_) = (*root problem*)
|
neuper@37906
|
1596 |
(case p_ of
|
neuper@37906
|
1597 |
Res => raise PTREE "move_dn: end of calculation"
|
neuper@37906
|
1598 |
| _ => if null ns (*go down from Pbl + Met*)
|
neuper@37906
|
1599 |
then raise PTREE "move_dn: solve problem not started"
|
neuper@37906
|
1600 |
else ([1], Frm))
|
neuper@37906
|
1601 |
| move_dn P (Nd (_, ns)) (p::(ps as (_::_)),p_) =(*iterate to end of pos*)
|
neuper@37906
|
1602 |
if p > length ns then raise PTREE "move_dn: pos not existent 2"
|
neuper@37906
|
1603 |
else move_dn ((P@[p]): pos) (nth p ns) (ps, p_)
|
neuper@37906
|
1604 |
|
neuper@37906
|
1605 |
| move_dn P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*)
|
neuper@37906
|
1606 |
if p > length ns then raise PTREE "move_dn: pos not existent 3"
|
neuper@37906
|
1607 |
else case p_ of
|
neuper@37906
|
1608 |
Res =>
|
neuper@37906
|
1609 |
if p = length ns (*last Res on this level: go a level up*)
|
neuper@37906
|
1610 |
then if g_ostate c = Complete then (P, Res)
|
neuper@37906
|
1611 |
else raise PTREE (ints2str' P^" not complete 1")
|
neuper@37906
|
1612 |
else (*go to the next Nd on this level, or down into the next Nd*)
|
neuper@37906
|
1613 |
if is_pblnd (nth (p+1) ns) then (P@[p+1], Pbl)
|
neuper@37906
|
1614 |
else
|
neuper@37906
|
1615 |
if g_res' (nth p ns) = g_form' (nth (p+1) ns)
|
neuper@37906
|
1616 |
then if (null o children o (nth (p+1))) ns
|
neuper@37906
|
1617 |
then (*take the Res if Complete*)
|
neuper@37906
|
1618 |
if g_ostate' (nth (p+1) ns) = Complete
|
neuper@37906
|
1619 |
then (P@[p+1], Res)
|
neuper@37906
|
1620 |
else raise PTREE (ints2str' (P@[p+1])^
|
neuper@37906
|
1621 |
" not complete 2")
|
neuper@37906
|
1622 |
else (P@[p+1,1], Frm)(*go down into the next PrfObj*)
|
neuper@37906
|
1623 |
else (P@[p+1], Frm)(*take Frm: exists if the Nd exists*)
|
neuper@37906
|
1624 |
| Frm => (*go down or to the Res of this Nd*)
|
neuper@37906
|
1625 |
if (null o children o (nth p)) ns
|
neuper@37906
|
1626 |
then if g_ostate' (nth p ns) = Complete then (P @ [p], Res)
|
neuper@37906
|
1627 |
else raise PTREE (ints2str' (P @ [p])^" not complete 3")
|
neuper@37906
|
1628 |
else (P @ [p, 1], Frm)
|
neuper@37906
|
1629 |
| _ => (*is Pbl or Met*)
|
neuper@37906
|
1630 |
if (null o children o (nth p)) ns
|
neuper@37906
|
1631 |
then raise PTREE "move_dn:solve subproblem not startd"
|
neuper@37906
|
1632 |
else (P @ [p, 1],
|
neuper@37906
|
1633 |
if (is_pblnd o hd o children o (nth p)) ns
|
neuper@37906
|
1634 |
then Pbl else Frm);
|
neuper@37906
|
1635 |
|
neuper@37906
|
1636 |
|
neuper@37906
|
1637 |
(*.go one level down into ptree.*)
|
neuper@37906
|
1638 |
fun movelevel_dn [] (Nd (c, ns)) ([],p_) = (*root problem*)
|
neuper@37906
|
1639 |
if is_pblobj c
|
neuper@37906
|
1640 |
then if null ns
|
neuper@37906
|
1641 |
then raise PTREE "solve problem not started"
|
neuper@37906
|
1642 |
else ([1], if (is_pblnd o hd) ns then Pbl else Frm)
|
neuper@37906
|
1643 |
else raise PTREE "pos not existent 1"
|
neuper@37906
|
1644 |
|
neuper@37906
|
1645 |
(*iterate towards end of pos*)
|
neuper@37906
|
1646 |
| movelevel_dn P (Nd (_, ns)) (p::(ps as (_::_)),p_) =
|
neuper@37906
|
1647 |
if p > length ns then raise PTREE "pos not existent 2"
|
neuper@37906
|
1648 |
else movelevel_dn (P@[p]) (nth p ns) (ps, p_)
|
neuper@37906
|
1649 |
|
neuper@37906
|
1650 |
| movelevel_dn P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*)
|
neuper@37906
|
1651 |
if p > length ns then raise PTREE "pos not existent 3" else
|
neuper@37906
|
1652 |
case p_ of Res =>
|
neuper@37906
|
1653 |
if p = length ns
|
neuper@37906
|
1654 |
then raise PTREE "no children"
|
neuper@37906
|
1655 |
else
|
neuper@37906
|
1656 |
if g_branch c = TransitiveB
|
neuper@37906
|
1657 |
then if (null o children o (nth (p+1))) ns
|
neuper@37906
|
1658 |
then raise PTREE "no children"
|
neuper@37906
|
1659 |
else (P @ [p+1, 1],
|
neuper@37906
|
1660 |
if (is_pblnd o hd o children o (nth (p+1))) ns
|
neuper@37906
|
1661 |
then Pbl else Frm)
|
neuper@37906
|
1662 |
else if (null o children o (nth p)) ns
|
neuper@37906
|
1663 |
then raise PTREE "no children"
|
neuper@37906
|
1664 |
else (P @ [p, 1], if (is_pblnd o hd o children o (nth p)) ns
|
neuper@37906
|
1665 |
then Pbl else Frm)
|
neuper@37906
|
1666 |
| _ => if (null o children o (nth p)) ns
|
neuper@37906
|
1667 |
then raise PTREE "no children"
|
neuper@37906
|
1668 |
else (P @ [p, 1], (*go down*)
|
neuper@37906
|
1669 |
if (is_pblnd o hd o children o (nth p)) ns
|
neuper@37906
|
1670 |
then Pbl else Frm);
|
neuper@37906
|
1671 |
|
neuper@37906
|
1672 |
|
neuper@37906
|
1673 |
|
neuper@37906
|
1674 |
(*.go to the previous position in ptree; regard TransitiveB.*)
|
neuper@37906
|
1675 |
fun move_up _ (Nd (c, ns)) (([],p_):pos') = (*root problem*)
|
neuper@37906
|
1676 |
if is_pblobj c
|
neuper@37906
|
1677 |
then case p_ of Res => if null ns then ([], Pbl) (*Res -> Pbl (not Met)!*)
|
neuper@37906
|
1678 |
else ([length ns], Res)
|
neuper@37906
|
1679 |
| _ => raise PTREE "begin of calculation"
|
neuper@37906
|
1680 |
else raise PTREE "pos not existent"
|
neuper@37906
|
1681 |
|
neuper@37906
|
1682 |
| move_up P (Nd (_, ns)) (p::(ps as (_::_)),p_) = (*iterate to end of pos*)
|
neuper@37906
|
1683 |
if p > length ns then raise PTREE "pos not existent"
|
neuper@37906
|
1684 |
else move_up (P@[p]) (nth p ns) (ps,p_)
|
neuper@37906
|
1685 |
|
neuper@37906
|
1686 |
| move_up P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*)
|
neuper@37906
|
1687 |
if p > length ns then raise PTREE "pos not existent"
|
neuper@37906
|
1688 |
else if is_pblnd (nth p ns) then
|
neuper@37906
|
1689 |
case p_ of Res =>
|
neuper@37906
|
1690 |
let val nc = (length o children o (nth p)) ns
|
neuper@37906
|
1691 |
in if nc = 0 then (P@[p], Pbl) (*Res -> Pbl (not Met)!*)
|
neuper@37906
|
1692 |
else (P @ [p, nc], Res) end (*go down*)
|
neuper@37906
|
1693 |
| _ => if p = 1 then (P, Pbl) else (P@[p-1], Res)
|
neuper@37906
|
1694 |
else case p_ of Frm => if p <> 1 then (P, Frm)
|
neuper@37906
|
1695 |
else if is_pblobj c then (P, Pbl) else (P, Frm)
|
neuper@37906
|
1696 |
| Res =>
|
neuper@37906
|
1697 |
let val nc = (length o children o (nth p)) ns
|
neuper@37906
|
1698 |
in if nc = 0 (*cannot go down*)
|
neuper@37906
|
1699 |
then if g_branch c = TransitiveB andalso p <> 1
|
neuper@37906
|
1700 |
then (P@[p-1], Res) else (P@[p], Frm)
|
neuper@37906
|
1701 |
else (P @ [p, nc], Res) end; (*go down*)
|
neuper@37906
|
1702 |
|
neuper@37906
|
1703 |
|
neuper@37906
|
1704 |
|
neuper@37906
|
1705 |
(*.go one level up in ptree; sets the position on Frm.*)
|
neuper@37906
|
1706 |
fun movelevel_up _ (Nd (c, ns)) (([],p_):pos') = (*root problem*)
|
neuper@37906
|
1707 |
raise PTREE "pos not existent"
|
neuper@37906
|
1708 |
|
neuper@37906
|
1709 |
(*iterate towards end of pos*)
|
neuper@37906
|
1710 |
| movelevel_up P (Nd (_, ns)) (p::(ps as (_::_)),p_) =
|
neuper@37906
|
1711 |
if p > length ns then raise PTREE "pos not existent"
|
neuper@37906
|
1712 |
else movelevel_up (P@[p]) (nth p ns) (ps,p_)
|
neuper@37906
|
1713 |
|
neuper@37906
|
1714 |
| movelevel_up P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*)
|
neuper@37906
|
1715 |
if p > length ns then raise PTREE "pos not existent"
|
neuper@37906
|
1716 |
else if is_pblobj c then (P, Pbl) else (P, Frm);
|
neuper@37906
|
1717 |
|
neuper@37906
|
1718 |
|
neuper@37906
|
1719 |
(*.go to the next calc-head up in the calc-tree.*)
|
neuper@37906
|
1720 |
fun movecalchd_up pt ((p, Res):pos') =
|
neuper@37906
|
1721 |
(par_pblobj pt p, Pbl):pos'
|
neuper@37906
|
1722 |
| movecalchd_up pt (p, _) =
|
neuper@37906
|
1723 |
if is_pblobj (get_obj I pt p)
|
neuper@37906
|
1724 |
then (p, Pbl) else (par_pblobj pt p, Pbl);
|
neuper@37906
|
1725 |
|
neuper@37906
|
1726 |
(*.determine the previous pos' on the same level.*)
|
neuper@37906
|
1727 |
(*WN0502 made for interSteps; _only_ works for branch TransitiveB*)
|
neuper@37906
|
1728 |
fun lev_pred' pt (pos:pos' as ([],Res)) = ([],Pbl):pos'
|
neuper@37906
|
1729 |
| lev_pred' pt (pos:pos' as (p, Res)) =
|
neuper@37906
|
1730 |
let val (p', last) = split_last p
|
neuper@37906
|
1731 |
in if last = 1
|
neuper@37906
|
1732 |
then if (is_pblobj o (get_obj I pt)) p then (p,Pbl) else (p, Frm)
|
neuper@37906
|
1733 |
else if get_obj g_res pt (p' @ [last - 1]) = get_obj g_form pt p
|
neuper@37906
|
1734 |
then (p' @ [last - 1], Res) (*TransitiveB*)
|
neuper@37906
|
1735 |
else if (is_pblobj o (get_obj I pt)) p then (p,Pbl) else (p, Frm)
|
neuper@37906
|
1736 |
end;
|
neuper@37906
|
1737 |
|
neuper@37906
|
1738 |
(*.determine the next pos' on the same level.*)
|
neuper@37906
|
1739 |
fun lev_on' pt (([],Pbl):pos') = ([],Res):pos'
|
neuper@37906
|
1740 |
| lev_on' pt (p, Res) =
|
neuper@37906
|
1741 |
if get_obj g_res pt p = get_obj g_form pt (lev_on p)(*TransitiveB*)
|
neuper@37906
|
1742 |
then if existpt' (lev_on p, Res) pt then (lev_on p, Res)
|
neuper@37906
|
1743 |
else raise error ("lev_on': (p, Res) -> (p, Res) not existent, \
|
neuper@37906
|
1744 |
\p = "^ints2str' (lev_on p))
|
neuper@37906
|
1745 |
else (lev_on p, Frm)
|
neuper@37906
|
1746 |
| lev_on' pt (p, _) =
|
neuper@37906
|
1747 |
if existpt' (p, Res) pt then (p, Res)
|
neuper@37906
|
1748 |
else raise error ("lev_on': (p, Frm) -> (p, Res) not existent, \
|
neuper@37906
|
1749 |
\p = "^ints2str' p);
|
neuper@37906
|
1750 |
|
neuper@37906
|
1751 |
fun exist_lev_on' pt p = (lev_on' pt p; true) handle _ => false;
|
neuper@37906
|
1752 |
|
neuper@37906
|
1753 |
(*.is the pos' at the last element of a calulation _AND_ can be continued.*)
|
neuper@37906
|
1754 |
(* val (pt, pos as (p,p_)) = (pt, ([1],Frm));
|
neuper@37906
|
1755 |
*)
|
neuper@37906
|
1756 |
fun is_curr_endof_calc pt (([],Res) : pos') = false
|
neuper@37906
|
1757 |
| is_curr_endof_calc pt (pos as (p,_)) =
|
neuper@37906
|
1758 |
not (exist_lev_on' pt pos)
|
neuper@37906
|
1759 |
andalso get_obj g_ostate pt (lev_up p) = Incomplete;
|
neuper@37906
|
1760 |
|
neuper@37906
|
1761 |
|
neuper@37906
|
1762 |
(**.insert into ctree and cut branches accordingly.**)
|
neuper@37906
|
1763 |
|
neuper@37906
|
1764 |
(*.get all positions of certain intervals on the ctree.*)
|
neuper@37906
|
1765 |
(*OLD VERSION without move_dn; kept for occasional redesign
|
neuper@37906
|
1766 |
get all pos's to be cut in a ptree
|
neuper@37906
|
1767 |
below a pos or from a ptree list after i-th element (NO level_up).*)
|
neuper@37906
|
1768 |
fun get_allpos' (_:pos, _:posel) EmptyPtree = ([]:pos' list)
|
neuper@37906
|
1769 |
| get_allpos' (p, 1) (Nd (b, bs)) = (*p is pos of Nd*)
|
neuper@37906
|
1770 |
if g_ostate b = Incomplete
|
neuper@37906
|
1771 |
then ((*writeln("get_allpos' (p, 1) Incomplete: p="^ints2str' p);*)
|
neuper@37906
|
1772 |
[(p,Frm)] @ (get_allpos's (p, 1) bs)
|
neuper@37906
|
1773 |
)
|
neuper@37906
|
1774 |
else ((*writeln("get_allpos' (p, 1) else: p="^ints2str' p);*)
|
neuper@37906
|
1775 |
[(p,Frm)] @ (get_allpos's (p, 1) bs) @ [(p,Res)]
|
neuper@37906
|
1776 |
)
|
neuper@37906
|
1777 |
(*WN041020 here we assume what is presented on the worksheet ?!*)
|
neuper@37906
|
1778 |
| get_allpos' (p, i) (Nd (b, bs)) = (*p is pos of Nd*)
|
neuper@37906
|
1779 |
if length bs > 0 orelse is_pblobj b
|
neuper@37906
|
1780 |
then if g_ostate b = Incomplete
|
neuper@37906
|
1781 |
then [(p,Frm)] @ (get_allpos's (p, 1) bs)
|
neuper@37906
|
1782 |
else [(p,Frm)] @ (get_allpos's (p, 1) bs) @ [(p,Res)]
|
neuper@37906
|
1783 |
else
|
neuper@37906
|
1784 |
if g_ostate b = Incomplete
|
neuper@37906
|
1785 |
then []
|
neuper@37906
|
1786 |
else [(p,Res)]
|
neuper@37906
|
1787 |
(*WN041020 here we assume what is presented on the worksheet ?!*)
|
neuper@37906
|
1788 |
and get_allpos's _ [] = []
|
neuper@37906
|
1789 |
| get_allpos's (p, i) (pt::pts) = (*p is pos of parent-Nd*)
|
neuper@37906
|
1790 |
(get_allpos' (p@[i], i) pt) @ (get_allpos's (p, i+1) pts);
|
neuper@37906
|
1791 |
|
neuper@37906
|
1792 |
(*.get all positions of certain intervals on the ctree.*)
|
neuper@37906
|
1793 |
(*NEW version WN050225*)
|
neuper@37906
|
1794 |
|
neuper@37906
|
1795 |
|
neuper@37906
|
1796 |
(*.cut branches.*)
|
neuper@37906
|
1797 |
(*before WN041019......
|
neuper@37906
|
1798 |
val cut_branch = (test_trans, curry take):
|
neuper@37906
|
1799 |
(ppobj -> bool) * (int -> ptree list -> ptree list);
|
neuper@37906
|
1800 |
.. formlery used for ...
|
neuper@37906
|
1801 |
fun cut_tree''' _ [] = EmptyPtree
|
neuper@37906
|
1802 |
| cut_tree''' pt pos =
|
neuper@37906
|
1803 |
let val (pt',cut) = appl_branch cut_branch pt pos
|
neuper@37906
|
1804 |
in if cut andalso length pos > 1 then cut_tree''' pt' (lev_up pos)
|
neuper@37906
|
1805 |
else pt' end;
|
neuper@37906
|
1806 |
*)
|
neuper@37906
|
1807 |
(*OLD version before WN050225*)
|
neuper@37906
|
1808 |
(*WN050106 like cut_level, but deletes exactly 1 node --- for tests ONLY*)
|
neuper@37906
|
1809 |
fun cut_level_'_ (_:pos' list) (_:pos) EmptyPtree (_:pos') =
|
neuper@37906
|
1810 |
raise PTREE "cut_level_'_ Empty _"
|
neuper@37906
|
1811 |
| cut_level_'_ _ _ (Nd ( _, _)) ([],_) = raise PTREE "cut_level_'_ _ []"
|
neuper@37906
|
1812 |
| cut_level_'_ cuts P (Nd (b, bs)) (p::[],p_) =
|
neuper@37906
|
1813 |
if test_trans b
|
neuper@37906
|
1814 |
then (Nd (b, drop_nth [] (p:posel, bs)),
|
neuper@37906
|
1815 |
(* ~~~~~~~~~~~*)
|
neuper@37906
|
1816 |
cuts @
|
neuper@37906
|
1817 |
(if p_ = Frm then [(P@[p],Res)] else ([]:pos' list)) @
|
neuper@37906
|
1818 |
(*WN041020 here we assume what is presented on the worksheet ?!*)
|
neuper@37906
|
1819 |
(get_allpos's (P, p+1) (drop_nth [] (p, bs))))
|
neuper@37906
|
1820 |
(* ~~~~~~~~~~~*)
|
neuper@37906
|
1821 |
else (Nd (b, bs), cuts)
|
neuper@37906
|
1822 |
| cut_level_'_ cuts P (Nd (b, bs)) ((p::ps),p_) =
|
neuper@37906
|
1823 |
let val (bs',cuts') = cut_level_'_ cuts P (nth p bs) (ps, p_)
|
neuper@37906
|
1824 |
in (Nd (b, repl_app bs p bs'), cuts @ cuts') end;
|
neuper@37906
|
1825 |
|
neuper@37906
|
1826 |
(*before WN050219*)
|
neuper@37906
|
1827 |
fun cut_level (_:pos' list) (_:pos) EmptyPtree (_:pos') =
|
neuper@37906
|
1828 |
raise PTREE "cut_level EmptyPtree _"
|
neuper@37906
|
1829 |
| cut_level _ _ (Nd ( _, _)) ([],_) = raise PTREE "cut_level _ []"
|
neuper@37906
|
1830 |
|
neuper@37906
|
1831 |
| cut_level cuts P (Nd (b, bs)) (p::[],p_) =
|
neuper@37906
|
1832 |
if test_trans b
|
neuper@37906
|
1833 |
then (Nd (b, take (p:posel, bs)),
|
neuper@37906
|
1834 |
cuts @
|
neuper@37906
|
1835 |
(if p_ = Frm andalso (*#*) g_ostate b = Complete
|
neuper@37906
|
1836 |
then [(P@[p],Res)] else ([]:pos' list)) @
|
neuper@37906
|
1837 |
(*WN041020 here we assume what is presented on the worksheet ?!*)
|
neuper@37906
|
1838 |
(get_allpos's (P, p+1) (takerest (p, bs))))
|
neuper@37906
|
1839 |
else (Nd (b, bs), cuts)
|
neuper@37906
|
1840 |
|
neuper@37906
|
1841 |
| cut_level cuts P (Nd (b, bs)) ((p::ps),p_) =
|
neuper@37906
|
1842 |
let val (bs',cuts') = cut_level cuts P (nth p bs) (ps, p_)
|
neuper@37906
|
1843 |
in (Nd (b, repl_app bs p bs'), cuts @ cuts') end;
|
neuper@37906
|
1844 |
|
neuper@37906
|
1845 |
(*OLD version before WN050219, overwritten below*)
|
neuper@37906
|
1846 |
fun cut_tree _ (([],_):pos') = raise PTREE "cut_tree _ ([],_)"
|
neuper@37906
|
1847 |
| cut_tree pt (pos as ([p],_)) =
|
neuper@37906
|
1848 |
let val (pt', cuts) = cut_level ([]:pos' list) [] pt pos
|
neuper@37906
|
1849 |
in (pt', cuts @ (if get_obj g_ostate pt [] = Incomplete
|
neuper@37906
|
1850 |
then [] else [([],Res)])) end
|
neuper@37906
|
1851 |
| cut_tree pt (p,p_) =
|
neuper@37906
|
1852 |
let
|
neuper@37906
|
1853 |
fun cutfn pt cuts (p,p_) =
|
neuper@37906
|
1854 |
let val (pt', cuts') = cut_level [] (lev_up p) pt (p,p_)
|
neuper@37906
|
1855 |
val cuts'' = if get_obj g_ostate pt (lev_up p) = Incomplete
|
neuper@37906
|
1856 |
then [] else [(lev_up p, Res)]
|
neuper@37906
|
1857 |
in if length cuts' > 0 andalso length p > 1
|
neuper@37906
|
1858 |
then cutfn pt' (cuts @ cuts') (lev_up p, Frm(*-->(p,Res)*))
|
neuper@37906
|
1859 |
else (pt',cuts @ cuts') end
|
neuper@37906
|
1860 |
val (pt', cuts) = cutfn pt [] (p,p_)
|
neuper@37906
|
1861 |
in (pt', cuts @ (if get_obj g_ostate pt [] = Incomplete
|
neuper@37906
|
1862 |
then [] else [([], Res)])) end;
|
neuper@37906
|
1863 |
|
neuper@37906
|
1864 |
|
neuper@37906
|
1865 |
(*########/ inserted from ctreeNEW.sml \#################################**)
|
neuper@37906
|
1866 |
|
neuper@37906
|
1867 |
(*.get all positions in a ptree until ([],Res) or ostate=Incomplete
|
neuper@37906
|
1868 |
val get_allp = fn :
|
neuper@37906
|
1869 |
pos' list -> : accumulated, start with []
|
neuper@37906
|
1870 |
pos -> : the offset for subtrees wrt the root
|
neuper@37906
|
1871 |
ptree -> : (sub)tree
|
neuper@37906
|
1872 |
pos' : initialization (the last pos' before ...)
|
neuper@37906
|
1873 |
-> pos' list : of positions in this (sub) tree (relative to the root)
|
neuper@37906
|
1874 |
.*)
|
neuper@37906
|
1875 |
(* val (cuts, P, pt, pos) = ([], [3], get_nd pt [3], ([], Frm):pos');
|
neuper@37906
|
1876 |
val (cuts, P, pt, pos) = ([], [2], get_nd pt [2], ([], Frm):pos');
|
neuper@37906
|
1877 |
length (children pt);
|
neuper@37906
|
1878 |
*)
|
neuper@37906
|
1879 |
fun get_allp (cuts:pos' list) (P:pos, pos:pos') pt =
|
neuper@37906
|
1880 |
(let val nxt = move_dn [] pt pos (*exn if Incomplete reached*)
|
neuper@37906
|
1881 |
in if nxt <> ([],Res)
|
neuper@37906
|
1882 |
then get_allp (cuts @ [nxt]) (P, nxt) pt
|
neuper@37906
|
1883 |
else (map (apfst (curry op@ P)) (cuts @ [nxt])): pos' list
|
neuper@37906
|
1884 |
end) handle PTREE _ => (map (apfst (curry op@ P)) cuts);
|
neuper@37906
|
1885 |
|
neuper@37906
|
1886 |
|
neuper@37906
|
1887 |
(*the pts are assumed to be on the same level*)
|
neuper@37906
|
1888 |
fun get_allps (cuts: pos' list) (P:pos) [] = cuts
|
neuper@37906
|
1889 |
| get_allps cuts P (pt::pts) =
|
neuper@37906
|
1890 |
let val below = get_allp [] (P, ([], Frm)) pt
|
neuper@37906
|
1891 |
val levfrm =
|
neuper@37906
|
1892 |
if is_pblnd pt
|
neuper@37906
|
1893 |
then (P, Pbl)::below
|
neuper@37906
|
1894 |
else if last_elem P = 1
|
neuper@37906
|
1895 |
then (P, Frm)::below
|
neuper@37906
|
1896 |
else (*Trans*) below
|
neuper@37906
|
1897 |
val levres = levfrm @ (if null below then [(P, Res)] else [])
|
neuper@37906
|
1898 |
in get_allps (cuts @ levres) (lev_on P) pts end;
|
neuper@37906
|
1899 |
|
neuper@37906
|
1900 |
|
neuper@37906
|
1901 |
(**.these 2 funs decide on how far cut_tree goes.**)
|
neuper@37906
|
1902 |
(*.shall the nodes _after_ the pos to be inserted at be deleted?.*)
|
neuper@37906
|
1903 |
fun test_trans (PrfObj{branch = Transitive,...}) = true
|
neuper@37906
|
1904 |
| test_trans (PrfObj{branch = NoBranch,...}) = true
|
neuper@37906
|
1905 |
| test_trans (PblObj{branch = Transitive,...}) = true
|
neuper@37906
|
1906 |
| test_trans (PblObj{branch = NoBranch,...}) = true
|
neuper@37906
|
1907 |
| test_trans _ = false;
|
neuper@37906
|
1908 |
(*.shall cutting be continued on the higher level(s)?
|
neuper@37906
|
1909 |
the Nd regarded will NOT be changed.*)
|
neuper@37906
|
1910 |
fun cutlevup (PblObj _) = false (*for tests of LK0502*)
|
neuper@37906
|
1911 |
| cutlevup _ = true;
|
neuper@37906
|
1912 |
val cutlevup = test_trans;(*WN060727 after summerterm tests.LK0502 withdrawn*)
|
neuper@37906
|
1913 |
|
neuper@37906
|
1914 |
(*cut_bottom new sml603..608
|
neuper@37906
|
1915 |
cut the level at the bottom of the pos (used by cappend_...)
|
neuper@37906
|
1916 |
and handle the parent in order to avoid extra case for root
|
neuper@37906
|
1917 |
fn: ptree -> : the _whole_ ptree for cut_levup
|
neuper@37906
|
1918 |
pos * posel -> : the pos after split_last
|
neuper@37906
|
1919 |
ptree -> : the parent of the Nd to be cut
|
neuper@37906
|
1920 |
return
|
neuper@37906
|
1921 |
(ptree * : the updated ptree
|
neuper@37906
|
1922 |
pos' list) * : the pos's cut
|
neuper@37906
|
1923 |
bool : cutting shall be continued on the higher level(s)
|
neuper@37906
|
1924 |
*)
|
neuper@37906
|
1925 |
fun cut_bottom _ (pt' as Nd (b, [])) = ((pt', []), cutlevup b)
|
neuper@37906
|
1926 |
| cut_bottom (P:pos, p:posel) (Nd (b, bs)) =
|
neuper@37906
|
1927 |
let (*divide level into 3 parts...*)
|
neuper@37906
|
1928 |
val keep = take (p - 1, bs)
|
neuper@37906
|
1929 |
val pt' as Nd (_,bs') = nth p bs
|
neuper@37906
|
1930 |
(*^^^^^_here_ will be 'insert'ed by 'append_..'*)
|
neuper@37906
|
1931 |
val (tail, tp) = (takerest (p, bs),
|
neuper@37906
|
1932 |
if null (takerest (p, bs)) then 0 else p + 1)
|
neuper@37906
|
1933 |
val (children, cuts) =
|
neuper@37906
|
1934 |
if test_trans b
|
neuper@37906
|
1935 |
then (keep,
|
neuper@37906
|
1936 |
(if is_pblnd pt' then [(P @ [p], Pbl)] else [])
|
neuper@37906
|
1937 |
@ (get_allp [] (P @ [p], (P, Frm)) pt')
|
neuper@37906
|
1938 |
@ (get_allps [] (P @ [p+1]) tail))
|
neuper@37906
|
1939 |
else (keep @ [(*'insert'ed by 'append_..'*)] @ tail,
|
neuper@37906
|
1940 |
get_allp [] (P @ [p], (P, Frm)) pt')
|
neuper@37906
|
1941 |
val (pt'', cuts) =
|
neuper@37906
|
1942 |
if cutlevup b
|
neuper@37906
|
1943 |
then (Nd (del_res b, children),
|
neuper@37906
|
1944 |
cuts @ (if g_ostate b = Incomplete then [] else [(P,Res)]))
|
neuper@37906
|
1945 |
else (Nd (b, children), cuts)
|
neuper@37906
|
1946 |
(*val _= writeln("####cut_bottom (P, p)="^pos2str (P @ [p])^
|
neuper@37906
|
1947 |
", Nd=.............................................")
|
neuper@37906
|
1948 |
val _= show_pt pt''
|
neuper@37906
|
1949 |
val _= writeln("####cut_bottom form='"^
|
neuper@37906
|
1950 |
term2str (get_obj g_form pt'' []))
|
neuper@37906
|
1951 |
val _= writeln("####cut_bottom cuts#="^string_of_int (length cuts)^
|
neuper@37906
|
1952 |
", cuts="^pos's2str cuts)*)
|
neuper@37906
|
1953 |
in ((pt'', cuts:pos' list), cutlevup b) end;
|
neuper@37906
|
1954 |
|
neuper@37906
|
1955 |
|
neuper@37906
|
1956 |
(*.go all levels from the bottom of 'pos' up to the root,
|
neuper@37906
|
1957 |
on each level compose the children of a node and accumulate the cut Nds
|
neuper@37906
|
1958 |
args
|
neuper@37906
|
1959 |
pos' list -> : for accumulation
|
neuper@37906
|
1960 |
bool -> : cutting shall be continued on the higher level(s)
|
neuper@37906
|
1961 |
ptree -> : the whole ptree for 'get_nd pt P' on each level
|
neuper@37906
|
1962 |
ptree -> : the Nd from the lower level for insertion at path
|
neuper@37906
|
1963 |
pos * posel -> : pos=path split for convenience
|
neuper@37906
|
1964 |
ptree -> : Nd the children of are under consideration on this call
|
neuper@37906
|
1965 |
returns :
|
neuper@37906
|
1966 |
ptree * pos' list : the updated parent-Nd and the pos's of the Nds cut
|
neuper@37906
|
1967 |
.*)
|
neuper@37906
|
1968 |
fun cut_levup (cuts:pos' list) clevup pt pt' (P:pos, p:posel) (Nd (b, bs)) =
|
neuper@37906
|
1969 |
let (*divide level into 3 parts...*)
|
neuper@37906
|
1970 |
val keep = take (p - 1, bs)
|
neuper@37906
|
1971 |
(*val pt' comes as argument from below*)
|
neuper@37906
|
1972 |
val (tail, tp) = (takerest (p, bs),
|
neuper@37906
|
1973 |
if null (takerest (p, bs)) then 0 else p + 1)
|
neuper@37906
|
1974 |
val (children, cuts') =
|
neuper@37906
|
1975 |
if clevup
|
neuper@37906
|
1976 |
then (keep @ [pt'], get_allps [] (P @ [p+1]) tail)
|
neuper@37906
|
1977 |
else (keep @ [pt'] @ tail, [])
|
neuper@37906
|
1978 |
val clevup' = if clevup then cutlevup b else false
|
neuper@37906
|
1979 |
(*the first Nd with false stops cutting on all levels above*)
|
neuper@37906
|
1980 |
val (pt'', cuts') =
|
neuper@37906
|
1981 |
if clevup'
|
neuper@37906
|
1982 |
then (Nd (del_res b, children),
|
neuper@37906
|
1983 |
cuts' @ (if g_ostate b = Incomplete then [] else [(P,Res)]))
|
neuper@37906
|
1984 |
else (Nd (b, children), cuts')
|
neuper@37906
|
1985 |
(*val _= writeln("#####cut_levup clevup= "^bool2str clevup)
|
neuper@37906
|
1986 |
val _= writeln("#####cut_levup cutlevup b= "^bool2str (cutlevup b))
|
neuper@37906
|
1987 |
val _= writeln("#####cut_levup (P, p)="^pos2str (P @ [p])^
|
neuper@37906
|
1988 |
", Nd=.............................................")
|
neuper@37906
|
1989 |
val _= show_pt pt''
|
neuper@37906
|
1990 |
val _= writeln("#####cut_levup form='"^
|
neuper@37906
|
1991 |
term2str (get_obj g_form pt'' []))
|
neuper@37906
|
1992 |
val _= writeln("#####cut_levup cuts#="^string_of_int (length cuts)^
|
neuper@37906
|
1993 |
", cuts="^pos's2str cuts)*)
|
neuper@37906
|
1994 |
in if null P then (pt'', (cuts @ cuts'):pos' list)
|
neuper@37906
|
1995 |
else let val (P, p) = split_last P
|
neuper@37906
|
1996 |
in cut_levup (cuts @ cuts') clevup' pt pt'' (P, p) (get_nd pt P)
|
neuper@37906
|
1997 |
end
|
neuper@37906
|
1998 |
end;
|
neuper@37906
|
1999 |
|
neuper@37906
|
2000 |
(*.cut nodes after and below an inserted node in the ctree;
|
neuper@37906
|
2001 |
the cuts range is limited by the predicate 'fun cutlevup'.*)
|
neuper@37906
|
2002 |
fun cut_tree pt (pos,_) =
|
neuper@37906
|
2003 |
if not (existpt pos pt)
|
neuper@37906
|
2004 |
then (pt,[]) (*appending a formula never cuts anything*)
|
neuper@37906
|
2005 |
else let val (P, p) = split_last pos
|
neuper@37906
|
2006 |
val ((pt', cuts), clevup) = cut_bottom (P, p) (get_nd pt P)
|
neuper@37906
|
2007 |
(* pt' is the updated parent of the Nd to cappend_..*)
|
neuper@37906
|
2008 |
in if null P then (pt', cuts)
|
neuper@37906
|
2009 |
else let val (P, p) = split_last P
|
neuper@37906
|
2010 |
in cut_levup cuts clevup pt pt' (P, p) (get_nd pt P)
|
neuper@37906
|
2011 |
end
|
neuper@37906
|
2012 |
end;
|
neuper@37906
|
2013 |
|
neuper@37906
|
2014 |
fun append_atomic p l f r f' s pt =
|
neuper@37906
|
2015 |
let (**val _= writeln("#@append_atomic: pos ="^pos2str p)**)
|
neuper@37906
|
2016 |
val (iss, f) = if existpt p pt andalso get_obj g_tac pt p=Empty_Tac
|
neuper@37906
|
2017 |
then (*after Take*)
|
neuper@37925
|
2018 |
((fst (get_obj g_loc pt p), SOME l),
|
neuper@37906
|
2019 |
get_obj g_form pt p)
|
neuper@37925
|
2020 |
else ((NONE, SOME l), f)
|
neuper@37925
|
2021 |
in insert (PrfObj {cell = NONE,
|
neuper@37906
|
2022 |
form = f,
|
neuper@37906
|
2023 |
tac = r,
|
neuper@37906
|
2024 |
loc = iss,
|
neuper@37906
|
2025 |
branch= NoBranch,
|
neuper@37906
|
2026 |
result= f',
|
neuper@37906
|
2027 |
ostate= s}) pt p end;
|
neuper@37906
|
2028 |
|
neuper@37906
|
2029 |
|
neuper@37906
|
2030 |
(*20.8.02: cappend_* FIXXXXME cut branches below cannot be decided here:
|
neuper@37906
|
2031 |
detail - generate - cappend: inserted, not appended !!!
|
neuper@37906
|
2032 |
|
neuper@37906
|
2033 |
cut decided in applicable_in !?!
|
neuper@37906
|
2034 |
*)
|
neuper@37906
|
2035 |
fun cappend_atomic pt p loc f r f' s =
|
neuper@37906
|
2036 |
(* val (pt, p, loc, f, r, f', s) =
|
neuper@37906
|
2037 |
(pt,p,l,f,Rewrite_Set_Inst (subst2subs subs',id_rls rls'),
|
neuper@37906
|
2038 |
(f',asm),Complete);
|
neuper@37906
|
2039 |
*)
|
neuper@37906
|
2040 |
((*writeln("##@cappend_atomic: pos ="^pos2str p);*)
|
neuper@37906
|
2041 |
apfst (append_atomic p loc f r f' s) (cut_tree pt (p,Frm))
|
neuper@37906
|
2042 |
);
|
neuper@37906
|
2043 |
(*TODO.WN050305 redesign the handling of istates*)
|
neuper@37906
|
2044 |
fun cappend_atomic pt p ist_res f r f' s =
|
neuper@37906
|
2045 |
if existpt p pt andalso get_obj g_tac pt p=Empty_Tac
|
neuper@37906
|
2046 |
then (*after Take: transfer Frm and respective istate*)
|
neuper@37906
|
2047 |
let val (ist_form, f) = (get_loc pt (p,Frm),
|
neuper@37906
|
2048 |
get_obj g_form pt p)
|
neuper@37906
|
2049 |
val (pt, cs) = cut_tree pt (p,Frm)
|
neuper@37906
|
2050 |
val pt = append_atomic p e_istate f r f' s pt
|
neuper@37925
|
2051 |
val pt = update_loc' pt p (SOME ist_form, SOME ist_res)
|
neuper@37906
|
2052 |
in (pt, cs) end
|
neuper@37906
|
2053 |
else apfst (append_atomic p ist_res f r f' s) (cut_tree pt (p,Frm));
|
neuper@37906
|
2054 |
|
neuper@37906
|
2055 |
|
neuper@37906
|
2056 |
(* called by Take *)
|
neuper@37906
|
2057 |
fun append_form p l f pt =
|
neuper@37906
|
2058 |
((*writeln("##@append_form: pos ="^pos2str p);*)
|
neuper@37925
|
2059 |
insert (PrfObj {cell = NONE,
|
neuper@37906
|
2060 |
form = (*if existpt p pt
|
neuper@37906
|
2061 |
andalso get_obj g_tac pt p = Empty_Tac
|
neuper@37906
|
2062 |
(*distinction from 'old' (+complete!) pobjs*)
|
neuper@37906
|
2063 |
then get_obj g_form pt p else*) f,
|
neuper@37906
|
2064 |
tac = Empty_Tac,
|
neuper@37925
|
2065 |
loc = (SOME l, NONE),
|
neuper@37906
|
2066 |
branch= NoBranch,
|
neuper@37906
|
2067 |
result= (e_term,[]),
|
neuper@37906
|
2068 |
ostate= Incomplete}) pt p
|
neuper@37906
|
2069 |
);
|
neuper@37906
|
2070 |
(* val (p,loc,f) = ([1], e_istate, str2term "x + 1 = 2");
|
neuper@37906
|
2071 |
val (p,loc,f) = (fst p, e_istate, str2term "-1 + x = 0");
|
neuper@37906
|
2072 |
*)
|
neuper@37906
|
2073 |
fun cappend_form pt p loc f =
|
neuper@37906
|
2074 |
((*writeln("##@cappend_form: pos ="^pos2str p);*)
|
neuper@37906
|
2075 |
apfst (append_form p loc f) (cut_tree pt (p,Frm))
|
neuper@37906
|
2076 |
);
|
neuper@37906
|
2077 |
fun cappend_form pt p loc f =
|
neuper@37906
|
2078 |
let (*val _= writeln("##@cappend_form: pos ="^pos2str p)
|
neuper@37906
|
2079 |
val _= writeln("##@cappend_form before cut_tree: loc ="^istate2str loc)*)
|
neuper@37906
|
2080 |
val (pt', cs) = cut_tree pt (p,Frm)
|
neuper@37906
|
2081 |
val pt'' = append_form p loc f pt'
|
neuper@37906
|
2082 |
(*val _= writeln("##@cappend_form after append: loc ="^
|
neuper@37906
|
2083 |
istates2str (get_obj g_loc pt'' p))*)
|
neuper@37906
|
2084 |
in (pt'', cs) end;
|
neuper@37906
|
2085 |
|
neuper@37906
|
2086 |
|
neuper@37906
|
2087 |
|
neuper@37906
|
2088 |
fun append_result pt p l f s =
|
neuper@37906
|
2089 |
((*writeln("##@append_result: pos ="^pos2str p);*)
|
neuper@37906
|
2090 |
(appl_obj (repl_result (fst (get_obj g_loc pt p),
|
neuper@37925
|
2091 |
SOME l) f s) pt p, [])
|
neuper@37906
|
2092 |
);
|
neuper@37906
|
2093 |
|
neuper@37906
|
2094 |
|
neuper@37906
|
2095 |
(*WN041022 deprecated, still for kbtest/diffapp.sml, /systest/root-equ.sml*)
|
neuper@37906
|
2096 |
fun append_parent p l f r b pt =
|
neuper@37906
|
2097 |
let (*val _= writeln("###append_parent: pos ="^pos2str p);*)
|
neuper@37906
|
2098 |
val (ll,f) = if existpt p pt andalso get_obj g_tac pt p=Empty_Tac
|
neuper@37925
|
2099 |
then ((fst (get_obj g_loc pt p), SOME l),
|
neuper@37906
|
2100 |
get_obj g_form pt p)
|
neuper@37925
|
2101 |
else ((SOME l, NONE), f)
|
neuper@37906
|
2102 |
in insert (PrfObj
|
neuper@37925
|
2103 |
{cell = NONE,
|
neuper@37906
|
2104 |
form = f,
|
neuper@37906
|
2105 |
tac = r,
|
neuper@37906
|
2106 |
loc = ll,
|
neuper@37906
|
2107 |
branch= b,
|
neuper@37906
|
2108 |
result= (e_term,[]),
|
neuper@37906
|
2109 |
ostate= Incomplete}) pt p end;
|
neuper@37906
|
2110 |
fun cappend_parent pt p loc f r b =
|
neuper@37906
|
2111 |
((*writeln("###cappend_parent: pos ="^pos2str p);*)
|
neuper@37906
|
2112 |
apfst (append_parent p loc f r b) (cut_tree pt (p,Und))
|
neuper@37906
|
2113 |
);
|
neuper@37906
|
2114 |
|
neuper@37906
|
2115 |
|
neuper@37906
|
2116 |
fun append_problem [] l fmz (strs,spec,hdf) _ =
|
neuper@37906
|
2117 |
((*writeln("###append_problem: pos = []");*)
|
neuper@37906
|
2118 |
(Nd (PblObj
|
neuper@37925
|
2119 |
{cell = NONE,
|
neuper@37906
|
2120 |
origin= (strs,spec,hdf),
|
neuper@37906
|
2121 |
fmz = fmz,
|
neuper@37906
|
2122 |
spec = empty_spec,
|
neuper@37906
|
2123 |
probl = []:itm list,
|
neuper@37906
|
2124 |
meth = []:itm list,
|
neuper@37925
|
2125 |
env = NONE,
|
neuper@37925
|
2126 |
loc = (SOME l, NONE),
|
neuper@37906
|
2127 |
branch= TransitiveB,(*FIXXXXXME.27.8.03: for equations only*)
|
neuper@37906
|
2128 |
result= (e_term,[]),
|
neuper@37906
|
2129 |
ostate= Incomplete},[]))
|
neuper@37906
|
2130 |
)
|
neuper@37906
|
2131 |
| append_problem p l fmz (strs,spec,hdf) pt =
|
neuper@37906
|
2132 |
((*writeln("###append_problem: pos ="^pos2str p);*)
|
neuper@37906
|
2133 |
insert (PblObj
|
neuper@37925
|
2134 |
{cell = NONE,
|
neuper@37906
|
2135 |
origin= (strs,spec,hdf),
|
neuper@37906
|
2136 |
fmz = fmz,
|
neuper@37906
|
2137 |
spec = empty_spec,
|
neuper@37906
|
2138 |
probl = []:itm list,
|
neuper@37906
|
2139 |
meth = []:itm list,
|
neuper@37925
|
2140 |
env = NONE,
|
neuper@37925
|
2141 |
loc = (SOME l, NONE),
|
neuper@37906
|
2142 |
branch= TransitiveB,
|
neuper@37906
|
2143 |
result= (e_term,[]),
|
neuper@37906
|
2144 |
ostate= Incomplete}) pt p
|
neuper@37906
|
2145 |
);
|
neuper@37906
|
2146 |
fun cappend_problem _ [] loc fmz ori =
|
neuper@37906
|
2147 |
((*writeln("###cappend_problem: pos = []");*)
|
neuper@37906
|
2148 |
(append_problem [] loc fmz ori EmptyPtree,[])
|
neuper@37906
|
2149 |
)
|
neuper@37906
|
2150 |
| cappend_problem pt p loc fmz ori =
|
neuper@37906
|
2151 |
((*writeln("###cappend_problem: pos ="^pos2str p);*)
|
neuper@37906
|
2152 |
apfst (append_problem p (loc:istate) fmz ori) (cut_tree pt (p,Frm))
|
neuper@37906
|
2153 |
);
|
neuper@37906
|
2154 |
|
neuper@37906
|
2155 |
(*.get the theory explicitly specified for the rootpbl;
|
neuper@37906
|
2156 |
thus use this function _after_ finishing specification.*)
|
neuper@37906
|
2157 |
fun rootthy (Nd (PblObj {spec=(thyID, _, _),...}, _)) = assoc_thy thyID
|
neuper@37906
|
2158 |
| rootthy _ = raise error "rootthy";
|
neuper@37906
|
2159 |
|