1 (* use"ME/generate.sml"; |
|
2 use"generate.sml"; |
|
3 *) |
|
4 |
|
5 (*.initialize istate for Detail_Set.*) |
|
6 (* |
|
7 fun init_istate (Rewrite_Set rls) = |
|
8 (* val (Rewrite_Set rls) = (get_obj g_tac pt p); |
|
9 *) |
|
10 (case assoc_rls rls of |
|
11 Rrls {scr=sc as Rfuns {init_state=ii,...},...} => (RrlsState (ii t)) |
|
12 (* val Rrls {scr=sc as Rfuns {init_state=ii,...},...} = assoc_rls rls; |
|
13 *) |
|
14 | Rls {scr=EmptyScr,...} => |
|
15 raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." |
|
16 ^"use prep_rls for storing rule-sets !") |
|
17 | Rls {scr=Script s,...} => |
|
18 (* val Rls {scr=Script s,...} = assoc_rls rls; |
|
19 *) |
|
20 (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true)) |
|
21 | Seq {scr=EmptyScr,...} => |
|
22 raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." |
|
23 ^"use prep_rls for storing rule-sets !") |
|
24 | Seq {srls=srls,scr=Script s,...} => |
|
25 (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true))) |
|
26 | init_istate (Rewrite_Set_Inst (subs, rls)) = |
|
27 (* val (Rewrite_Set_Inst (subs, rls)) = (get_obj g_tac pt p); |
|
28 *) |
|
29 let val (_, v)::_ = subs2subst (assoc_thy "Isac.thy") subs |
|
30 in case assoc_rls rls of |
|
31 Rls {scr=EmptyScr,...} => |
|
32 raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." |
|
33 ^"use prep_rls for storing rule-sets !") |
|
34 | Rls {scr=Script s,...} => |
|
35 let val (a1, a2) = two_scr_arg s |
|
36 in (ScrState ([(a1, v), (a2, t)],[], NONE, e_term, Sundef,true)) end |
|
37 | Seq {scr=EmptyScr,...} => |
|
38 raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." |
|
39 ^"use prep_rls for storing rule-sets !") |
|
40 (* val Seq {scr=Script s,...} = assoc_rls rls; |
|
41 *) |
|
42 | Seq {scr=Script s,...} => |
|
43 let val (a1, a2) = two_scr_arg s |
|
44 in (ScrState ([(a1, v), (a2, t)],[], NONE, e_term, Sundef,true)) end |
|
45 end; |
|
46 *) |
|
47 (*~~~~~~~~~~~~~~~~~~~~~~copy for dev. until del.~~~~~~~~~~~~~~~~~~~~~~~~~*) |
|
48 fun init_istate (Rewrite_Set rls) t = |
|
49 (* val (Rewrite_Set rls) = (get_obj g_tac pt p); |
|
50 *) |
|
51 (case assoc_rls rls of |
|
52 Rrls {scr=sc as Rfuns {init_state=ii,...},...} => (RrlsState (ii t)) |
|
53 (* val Rrls {scr=sc as Rfuns {init_state=ii,...},...} = assoc_rls rls; |
|
54 *) |
|
55 | Rls {scr=EmptyScr,...} => |
|
56 raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." |
|
57 ^"use prep_rls for storing rule-sets !") |
|
58 | Rls {scr=Script s,...} => |
|
59 (* val Rls {scr=Script s,...} = assoc_rls rls; |
|
60 *) |
|
61 (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true)) |
|
62 | Seq {scr=EmptyScr,...} => |
|
63 raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." |
|
64 ^"use prep_rls for storing rule-sets !") |
|
65 | Seq {srls=srls,scr=Script s,...} => |
|
66 (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true))) |
|
67 (* val ((Rewrite_Set_Inst (subs, rls)), t) = ((get_obj g_tac pt p), t); |
|
68 *) |
|
69 | init_istate (Rewrite_Set_Inst (subs, rls)) t = |
|
70 let val (_, v)::_ = subs2subst (assoc_thy "Isac.thy") subs |
|
71 (*...we suppose the substitution of only _one_ bound variable*) |
|
72 in case assoc_rls rls of |
|
73 Rls {scr=EmptyScr,...} => |
|
74 raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." |
|
75 ^"use prep_rls for storing rule-sets !") |
|
76 | Rls {scr=Script s,...} => |
|
77 let val (form, bdv) = two_scr_arg s |
|
78 in (ScrState ([(form, t), (bdv, v)],[], NONE, e_term, Sundef,true)) |
|
79 end |
|
80 | Seq {scr=EmptyScr,...} => |
|
81 raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." |
|
82 ^"use prep_rls for storing rule-sets !") |
|
83 (* val Seq {scr=Script s,...} = assoc_rls rls; |
|
84 *) |
|
85 | Seq {scr=Script s,...} => |
|
86 let val (form, bdv) = two_scr_arg s |
|
87 in (ScrState ([(form, t), (bdv, v)],[], NONE, e_term, Sundef,true)) |
|
88 end |
|
89 end; |
|
90 |
|
91 |
|
92 (*.a taci holds alle information required to build a node in the calc-tree; |
|
93 a taci is assumed to be used efficiently such that the calc-tree |
|
94 resulting from applying a taci need not be stored separately; |
|
95 see "type calcstate".*) |
|
96 (*TODO.WN0504 redesign ??? or redesign generate ?? see "fun generate" |
|
97 TODO.WN0512 ? redesign this _list_: |
|
98 # only used for [Apply_Method + (Take or Subproblem)], i.e. for initacs |
|
99 # the latter problem may be resolved automatically if "fun autocalc" is |
|
100 not any more used for the specify-phase and for changing the phases*) |
|
101 type taci = |
|
102 (tac * (*for comparison with input tac*) |
|
103 tac_ * (*for ptree generation*) |
|
104 (pos' * (*after applying tac_, for ptree generation*) |
|
105 istate)); (*after applying tac_, for ptree generation*) |
|
106 val e_taci = (Empty_Tac, Empty_Tac_, (e_pos', e_istate)): taci; |
|
107 (* val (tac, tac_, (pos', istate))::_ = tacis'; |
|
108 *) |
|
109 fun taci2str ((tac, tac_, (pos', istate)):taci) = |
|
110 "( "^tac2str tac^", "^tac_2str tac_^", ( "^pos'2str pos' |
|
111 ^", "^istate2str istate^" ))"; |
|
112 fun tacis2str tacis = (strs2str o (map (linefeed o taci2str))) tacis; |
|
113 |
|
114 datatype pblmet = (*%^%*) |
|
115 Upblmet (*undefined*) |
|
116 | Problem of pblID (*%^%*) |
|
117 | Method of metID; (*%^%*) |
|
118 fun pblmet2str (Problem pblID) = "Problem "^(strs2str pblID)(*%^%*) |
|
119 | pblmet2str (Method metID) = "Method "^(metID2str metID);(*%^%*) |
|
120 (*%^%*) (*26.6. moved to sequent.sml: fun ~~~~~~~~~; was here below*) |
|
121 |
|
122 |
|
123 (* copy from 03.60.usecases.sml 15.11.99 *) |
|
124 datatype user_cmd = |
|
125 Accept | NotAccept | Example |
|
126 | YourTurn | MyTurn (* internal use only 7.6.02 java-sml*) |
|
127 | Rules |
|
128 | DontKnow (*| HowComes | WhatFor 7.6.02 java-sml*) |
|
129 | Undo (*| Back | Forward 7.6.02 java-sml*) |
|
130 | EndProof | EndSession |
|
131 | ActivePlus | ActiveMinus | SpeedPlus | SpeedMinus |
|
132 (*Stepwidth...7.6.02 java-sml*) |
|
133 | Auto | NotAuto | Details; |
|
134 (* for test-print-outs *) |
|
135 fun user_cmd2str Accept ="Accept" |
|
136 | user_cmd2str NotAccept ="NotAccept" |
|
137 | user_cmd2str Example ="Example" |
|
138 | user_cmd2str MyTurn ="MyTurn" |
|
139 | user_cmd2str YourTurn ="YourTurn" |
|
140 | user_cmd2str Rules ="Rules" |
|
141 (*| user_cmd2str HowComes ="HowComes"*) |
|
142 | user_cmd2str DontKnow ="DontKnow" |
|
143 (*| user_cmd2str WhatFor ="WhatFor" |
|
144 | user_cmd2str Back ="Back"*) |
|
145 | user_cmd2str Undo ="Undo" |
|
146 (*| user_cmd2str Forward ="Forward"*) |
|
147 | user_cmd2str EndProof ="EndProof" |
|
148 | user_cmd2str EndSession ="EndSession" |
|
149 | user_cmd2str ActivePlus = "ActivePlus" |
|
150 | user_cmd2str ActiveMinus = "ActiveMinus" |
|
151 | user_cmd2str SpeedPlus = "SpeedPlus" |
|
152 | user_cmd2str SpeedMinus = "SpeedMinus" |
|
153 | user_cmd2str Auto = "Auto" |
|
154 | user_cmd2str NotAuto = "NotAuto" |
|
155 | user_cmd2str Details = "Details"; |
|
156 |
|
157 |
|
158 |
|
159 (*3.5.00: TODO: foppFK eliminated in interface FE-KE !!!*) |
|
160 datatype foppFK = (* in DG cases div 2 *) |
|
161 EmptyFoppFK (*DG internal*) |
|
162 | FormFK of cterm' |
|
163 | PpcFK of cterm' ppc; |
|
164 fun foppFK2str (FormFK ct') ="FormFK "^ct' |
|
165 | foppFK2str (PpcFK ppc) ="PpcFK "^(ppc2str ppc) |
|
166 | foppFK2str EmptyFoppFK ="EmptyFoppFK"; |
|
167 |
|
168 |
|
169 datatype nest = Open | Closed | Nundef; |
|
170 fun nest2str Open = "Open" |
|
171 | nest2str Closed = "Closed" |
|
172 | nest2str Nundef = "Nundef"; |
|
173 |
|
174 type indent = int; |
|
175 datatype edit = EdUndef | Write | Protect; |
|
176 (* bridge --> kernel *) |
|
177 (* bridge <-> kernel *) |
|
178 (* needed in dialog.sml *) (* bridge <-- kernel *) |
|
179 fun edit2str EdUndef = "EdUndef" |
|
180 | edit2str Write = "Write" |
|
181 | edit2str Protect = "Protect"; |
|
182 |
|
183 |
|
184 datatype inout = |
|
185 New_User | End_User (*<->*) |
|
186 | New_Proof | End_Proof (*<->*) |
|
187 | Command of user_cmd (*-->*) |
|
188 | Request of string | Message of string (*<--*) |
|
189 | Error_ of string | System of string (*<--*) |
|
190 | FoPpcFK of foppFK (*-->*) |
|
191 | FormKF of cellID * edit * indent * nest * cterm' (*<--*) |
|
192 | PpcKF of cellID * edit * indent * nest * (pblmet * item ppc) (*<--*) |
|
193 | RuleFK of tac (*-->*) |
|
194 | RuleKF of edit * tac (*<--*) |
|
195 | RefinedKF of (pblID * ((itm list) * ((bool * term) list))) (*<--*) |
|
196 | Select of tac list (*<--*) |
|
197 | RefineKF of match list (*<--*) |
|
198 | Speed of int (*<--*) |
|
199 | Active of int (*<--*) |
|
200 | Domain of domID; (*<--*) |
|
201 |
|
202 fun inout2str End_Proof = "End_Proof" |
|
203 | inout2str (Command user_cmd) = "Command "^(user_cmd2str user_cmd) |
|
204 | inout2str (Request s) = "Request "^s |
|
205 | inout2str (Message s) = "Message "^s |
|
206 | inout2str (Error_ s) = "Error_ "^s |
|
207 | inout2str (System s) = "System "^s |
|
208 | inout2str (FoPpcFK foppFK) = "FoPpcFK "^(foppFK2str foppFK) |
|
209 | inout2str (FormKF (cellID, edit, indent, nest, ct')) = |
|
210 "FormKF ("^(string_of_int cellID)^"," |
|
211 ^(edit2str edit)^","^(string_of_int indent)^"," |
|
212 ^(nest2str nest)^",(" |
|
213 ^ct' ^")" |
|
214 | inout2str (PpcKF (cellID, edit, indent, nest, (pm,itemppc))) = |
|
215 "PpcKF ("^(string_of_int cellID)^"," |
|
216 ^(edit2str edit)^","^(string_of_int indent)^"," |
|
217 ^(nest2str nest)^",(" |
|
218 ^(pblmet2str pm)^","^(itemppc2str itemppc)^"))" |
|
219 | inout2str (RuleKF (edit,tac)) = "RuleKF "^ |
|
220 pair2str(edit2str edit,tac2str tac) |
|
221 | inout2str (RuleFK tac) = "RuleFK "^(tac2str tac) |
|
222 | inout2str (Select tacs)= |
|
223 "Select "^((strs2str' o (map tac2str)) tacs) |
|
224 | inout2str (RefineKF ms) = "RefineKF "^(matchs2str ms) |
|
225 | inout2str (Speed i) = "Speed "^(string_of_int i) |
|
226 | inout2str (Active i) = "Active "^(string_of_int i) |
|
227 | inout2str (Domain dI) = "Domain "^dI; |
|
228 fun inouts2str ios = (strs2str' o (map inout2str)) ios; |
|
229 |
|
230 datatype mout = |
|
231 Form' of inout (* packing cterm' | cterm' ppc *) |
|
232 | Problems of inout (* passes specify (and solve) *) |
|
233 | Error' of inout |
|
234 | EmptyMout; |
|
235 |
|
236 fun mout2str (Form' inout) ="Form' "^(inout2str inout) |
|
237 | mout2str (Error' inout) ="Error' "^(inout2str inout) |
|
238 | mout2str (EmptyMout ) ="EmptyMout"; |
|
239 |
|
240 (*fun Form'2str (Form' )*) |
|
241 |
|
242 |
|
243 |
|
244 |
|
245 |
|
246 (* init pbl with ...,dsc,empty | [] *) |
|
247 fun init_pbl pbt = |
|
248 let |
|
249 fun pbt2itm (f,(d,t)) = |
|
250 ((0,[],false,f,Inc((d,[]),(e_term,[]))):itm); |
|
251 in map pbt2itm pbt end; |
|
252 (*take formal parameters from pbt, for transfer from pbl/met-hierarchy*) |
|
253 fun init_pbl' pbt = |
|
254 let |
|
255 fun pbt2itm (f,(d,t)) = |
|
256 ((0,[],false,f,Inc((d,[t]),(e_term,[]))):itm); |
|
257 in map pbt2itm pbt end; |
|
258 |
|
259 |
|
260 (*generate 1 ppobj in ptree*) |
|
261 (*TODO.WN0501: take calcstate as an argument (see embed_derive etc.)?specify?*) |
|
262 fun generate1 thy (Add_Given' (_, itmlist)) Uistate (pos as (p,p_)) pt = |
|
263 (pos:pos',[],Form' (PpcKF (0,EdUndef,0,Nundef, |
|
264 (Upblmet,itms2itemppc thy [][]))), |
|
265 case p_ of Pbl => update_pbl pt p itmlist |
|
266 | Met => update_met pt p itmlist) |
|
267 | generate1 thy (Add_Find' (_, itmlist)) Uistate (pos as (p,p_)) pt = |
|
268 (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))), |
|
269 case p_ of Pbl => update_pbl pt p itmlist |
|
270 | Met => update_met pt p itmlist) |
|
271 | generate1 thy (Add_Relation' (_, itmlist)) Uistate (pos as (p,p_)) pt = |
|
272 (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))), |
|
273 case p_ of Pbl => update_pbl pt p itmlist |
|
274 | Met => update_met pt p itmlist) |
|
275 |
|
276 | generate1 thy (Specify_Theory' domID) Uistate (pos as (p,_)) pt = |
|
277 (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))), |
|
278 update_domID pt p domID) |
|
279 |
|
280 | generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) Uistate |
|
281 (pos as (p,_)) pt = |
|
282 let val pt = update_pbl pt p itms |
|
283 val pt = update_pblID pt p pI |
|
284 in ((p,Pbl),[], |
|
285 Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))), |
|
286 pt) end |
|
287 |
|
288 | generate1 thy (Specify_Method' (mID, oris, itms)) Uistate |
|
289 (pos as (p,_)) pt = |
|
290 let val pt = update_oris pt p oris |
|
291 val pt = update_met pt p itms |
|
292 val pt = update_metID pt p mID |
|
293 in ((p,Met),[], |
|
294 Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))), |
|
295 pt) end |
|
296 |
|
297 | generate1 thy (Model_Problem' (_, itms, met)) Uistate (pos as (p,_)) pt = |
|
298 (* val (itms,pos as (p,_)) = (pbl, pos); |
|
299 *) |
|
300 let val pt = update_pbl pt p itms |
|
301 val pt = update_met pt p met |
|
302 in (pos,[],Form'(PpcKF(0,EdUndef,0,Nundef, |
|
303 (Upblmet,itms2itemppc thy [][]))), pt) end |
|
304 |
|
305 | generate1 thy (Refine_Tacitly' (pI,pIre,domID,metID,pbl)) |
|
306 Uistate (pos as (p,_)) pt = |
|
307 let val pt = update_pbl pt p pbl |
|
308 val pt = update_orispec pt p (domID,pIre,metID) |
|
309 in (pos,[], |
|
310 Form'(PpcKF(0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))), |
|
311 pt) end |
|
312 |
|
313 | generate1 thy (Refine_Problem' (pI,_)) Uistate (pos as (p,_)) pt = |
|
314 let val (dI,_,mI) = get_obj g_spec pt p |
|
315 val pt = update_spec pt p (dI, pI, mI) |
|
316 in (pos,[], |
|
317 Form'(PpcKF(0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),pt) |
|
318 end |
|
319 |
|
320 | generate1 thy (Apply_Method' (_,topt, is)) _ (pos as (p,p_)) pt = |
|
321 ((*writeln("###generate1 Apply_Method': pos = "^pos'2str (p,p_)); |
|
322 writeln("###generate1 Apply_Method': topt= "^termopt2str topt); |
|
323 writeln("###generate1 Apply_Method': is = "^istate2str is);*) |
|
324 case topt of |
|
325 SOME t => |
|
326 let val (pt,c) = cappend_form pt p is t |
|
327 (*val _= writeln("###generate1 Apply_Method: after cappend")*) |
|
328 in (pos,c, EmptyMout,pt) |
|
329 end |
|
330 | NONE => |
|
331 (pos,[],EmptyMout,update_env pt p (SOME is))) |
|
332 (* val (thy, (Take' t), l, (p,p_), pt) = |
|
333 ((assoc_thy "Isac.thy"), tac_, is, pos, pt); |
|
334 *) |
|
335 | generate1 thy (Take' t) l (p,p_) pt = (* val (Take' t) = m; *) |
|
336 let (*val _=writeln("### generate1: Take' pos="^pos'2str (p,p_));*) |
|
337 val p = let val (ps,p') = split_last p(*no connex to prev.ppobj*) |
|
338 in if p'=0 then ps@[1] else p end; |
|
339 val (pt,c) = cappend_form pt p l t; |
|
340 in ((p,Frm):pos', c, |
|
341 Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str t)), pt) end |
|
342 |
|
343 (* val (l, (p,p_)) = (RrlsState is, p); |
|
344 |
|
345 val (thy, Begin_Trans' t, l, (p,Frm), pt) = |
|
346 (assoc_thy "Isac.thy", tac_, is, p, pt); |
|
347 *) |
|
348 | generate1 thy (Begin_Trans' t) l (p,Frm) pt = |
|
349 let (* print_depth 99; |
|
350 map fst (get_interval ([],Pbl) ([],Res) 9999 pt);print_depth 3; |
|
351 *) |
|
352 val (pt,c) = cappend_form pt p l t |
|
353 (* print_depth 99; |
|
354 map fst (get_interval ([],Pbl) ([],Res) 9999 pt);print_depth 3; |
|
355 *) |
|
356 val pt = update_branch pt p TransitiveB (*040312*) |
|
357 (*replace the old PrfOjb ~~~~~*) |
|
358 val p = (lev_on o lev_dn(*starts with [...,0]*)) p; |
|
359 val (pt,c') = cappend_form pt p l t(*FIXME.0402 same istate ???*); |
|
360 in ((p,Frm), c @ c', Form' (FormKF (~1,EdUndef,(length p), Nundef, |
|
361 term2str t)), pt) end |
|
362 |
|
363 (* val (thy, Begin_Trans' t, l, (p,Res), pt) = |
|
364 (assoc_thy "Isac.thy", tac_, is, p, pt); |
|
365 *) |
|
366 | generate1 thy (Begin_Trans' t) l (p ,Res) pt = |
|
367 (*append after existing PrfObj _________*) |
|
368 generate1 thy (Begin_Trans' t) l (lev_on p,Frm) pt |
|
369 |
|
370 | generate1 thy (End_Trans' tasm) l (p,p_) pt = |
|
371 let val p' = lev_up p |
|
372 val (pt,c) = append_result pt p' l tasm Complete; |
|
373 in ((p',Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str t)), |
|
374 pt) end |
|
375 |
|
376 | generate1 thy (Rewrite_Inst' (_,_,_,_,subs',thm',f,(f',asm))) l (p,p_) pt = |
|
377 let (*val _= writeln("###generate1 Rewrite_Inst': pos= "^pos'2str (p,p_));*) |
|
378 val (pt,c) = cappend_atomic pt p l f |
|
379 (Rewrite_Inst (subst2subs subs',thm')) (f',asm) Complete; |
|
380 val pt = update_branch pt p TransitiveB (*040312*) |
|
381 (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm);9.6.03??*) |
|
382 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), |
|
383 pt) end |
|
384 |
|
385 | generate1 thy (Rewrite' (thy',ord',rls',pa,thm',f,(f',asm))) l (p,p_) pt = |
|
386 let (*val _= writeln("###generate1 Rewrite': pos= "^pos'2str (p,p_))*) |
|
387 val (pt,c) = cappend_atomic pt p l f (Rewrite thm') (f',asm) Complete |
|
388 val pt = update_branch pt p TransitiveB (*040312*) |
|
389 (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm);9.6.03??*) |
|
390 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), |
|
391 pt)end |
|
392 |
|
393 | generate1 thy (Rewrite_Asm' all) l p pt = |
|
394 generate1 thy (Rewrite' all) l p pt |
|
395 |
|
396 | generate1 thy (Rewrite_Set_Inst' (_,_,subs',rls',f,(f',asm))) l (p,p_) pt = |
|
397 (* val (thy, Rewrite_Set_Inst' (_,_,subs',rls',f,(f',asm)), l, (p,p_), pt) = |
|
398 (assoc_thy "Isac.thy", tac_, is, pos, pt); |
|
399 *) |
|
400 let (*val _=writeln("###generate1 Rewrite_Set_Inst': pos= "^pos'2str(p,p_))*) |
|
401 val (pt,c) = cappend_atomic pt p l f |
|
402 (Rewrite_Set_Inst (subst2subs subs',id_rls rls')) (f',asm) Complete |
|
403 val pt = update_branch pt p TransitiveB (*040312*) |
|
404 (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm');9.6.03??*) |
|
405 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), |
|
406 pt) end |
|
407 |
|
408 | generate1 thy (Detail_Set_Inst' (_,_,subs,rls,f,(f',asm))) l (p,p_) pt = |
|
409 let val (pt,c) = cappend_form pt p l f |
|
410 val pt = update_branch pt p TransitiveB (*040312*) |
|
411 |
|
412 val is = init_istate (Rewrite_Set_Inst (subst2subs subs, id_rls rls)) f |
|
413 val tac_ = Apply_Method' (e_metID, SOME t, is) |
|
414 val pos' = ((lev_on o lev_dn) p, Frm) |
|
415 in (*implicit Take*) generate1 thy tac_ is pos' pt end |
|
416 |
|
417 | generate1 thy (Rewrite_Set' (_,_,rls',f,(f',asm))) l (p,p_) pt = |
|
418 let (*val _= writeln("###generate1 Rewrite_Set': pos= "^pos'2str (p,p_))*) |
|
419 val (pt,c) = cappend_atomic pt p l f |
|
420 (Rewrite_Set (id_rls rls')) (f',asm) Complete |
|
421 val pt = update_branch pt p TransitiveB (*040312*) |
|
422 (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm');9.6.03??*) |
|
423 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), |
|
424 pt) end |
|
425 |
|
426 | generate1 thy (Detail_Set' (_,_,rls,f,(f',asm))) l (p,p_) pt = |
|
427 let val (pt,c) = cappend_form pt p l f |
|
428 val pt = update_branch pt p TransitiveB (*040312*) |
|
429 |
|
430 val is = init_istate (Rewrite_Set (id_rls rls)) f |
|
431 val tac_ = Apply_Method' (e_metID, SOME t, is) |
|
432 val pos' = ((lev_on o lev_dn) p, Frm) |
|
433 in (*implicit Take*) generate1 thy tac_ is pos' pt end |
|
434 |
|
435 | generate1 thy (Check_Postcond' (pI,(scval,asm))) l (p,p_) pt = |
|
436 let (*val _=writeln("###generate1 Check_Postcond': pos= "^pos'2str(p,p_))*) |
|
437 (*val (l',_) = get_obj g_loc pt p..don't overwrite with l from subpbl*) |
|
438 val (pt,c) = append_result pt p l (scval,map str2term asm) Complete |
|
439 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), |
|
440 Nundef, term2str scval)), pt) end |
|
441 |
|
442 | generate1 thy (Calculate' (thy',op_,f,(f',thm'))) l (p,p_) pt = |
|
443 let val (pt,c) = cappend_atomic pt p l f (Calculate op_) (f',[]) Complete; |
|
444 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), |
|
445 pt) end |
|
446 |
|
447 | generate1 thy (Check_elementwise' (consts,pred,(f',asm))) l (p,p_) pt = |
|
448 let(*val _=writeln("###generate1 Check_elementwise': p= "^pos'2str(p,p_))*) |
|
449 val (pt,c) = cappend_atomic pt p l consts |
|
450 (Check_elementwise pred) (f',asm) Complete; |
|
451 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), |
|
452 pt) end |
|
453 |
|
454 | generate1 thy (Or_to_List' (ors,list)) l (p,p_) pt = |
|
455 let val (pt,c) = cappend_atomic pt p l ors |
|
456 Or_to_List (list,[]) Complete; |
|
457 in ((p,Res), c, Form' (FormKF(~1,EdUndef,(length p), Nundef, term2str list)), |
|
458 pt) end |
|
459 |
|
460 | generate1 thy (Substitute' (subte, t, t')) l (p,p_) pt = |
|
461 let val (pt,c) = cappend_atomic pt p l t (Substitute (subte2sube subte)) |
|
462 (t',[]) Complete; |
|
463 in ((p,Res), c, Form' (FormKF(~1,EdUndef,(length p), Nundef, |
|
464 term2str t')), pt) |
|
465 end |
|
466 |
|
467 | generate1 thy (Tac_ (_,f,id,f')) l (p,p_) pt = |
|
468 let val (pt,c) = cappend_atomic pt p l (str2term f) |
|
469 (Tac id) (str2term f',[]) Complete; |
|
470 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f')), pt)end |
|
471 |
|
472 | generate1 thy (Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, f)) |
|
473 l (p,p_) pt = |
|
474 let (*val _=writeln("###generate1 Subproblem': pos= "^pos'2str (p,p_))*) |
|
475 val (pt,c) = cappend_problem pt p l (fmz_, (domID, pblID, metID)) |
|
476 (oris, (domID, pblID, metID), hdl); |
|
477 (*val pbl = init_pbl ((#ppc o get_pbt) pblID); |
|
478 val pt = update_pblppc pt p pbl;--------4.9.03->Model_Problem*) |
|
479 (*val _= writeln("### generate1: is([3],Frm)= "^ |
|
480 (istate2str (get_istate pt ([3],Frm))));*) |
|
481 val f = Syntax.string_of_term (thy2ctxt thy) f; |
|
482 in ((p,Pbl), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f)), pt) end |
|
483 |
|
484 | generate1 thy m' _ _ _ = |
|
485 raise error ("generate1: not impl.for "^(tac_2str m')) |
|
486 ; |
|
487 |
|
488 |
|
489 fun generate_hard thy m' (p,p_) pt = |
|
490 let |
|
491 val p = case p_ of Frm => p | Res => lev_on p |
|
492 | _ => raise error ("generate_hard: call by "^(pos'2str (p,p_))); |
|
493 in generate1 thy m' e_istate (p,p_) pt end; |
|
494 |
|
495 |
|
496 |
|
497 (*tacis are in reverse order from nxt_solve_/specify_: last = fst to insert*) |
|
498 (* val (tacis, (pt, _)) = (tacis, ptp); |
|
499 |
|
500 val (tacis, (pt, c, _)) = (rev tacis, (pt, [], (p, Res))); |
|
501 *) |
|
502 fun generate ([]: taci list) ptp = ptp |
|
503 | generate tacis (pt, c, _:pos'(*!dropped!WN0504redesign generate/tacis?*))= |
|
504 let val (tacis', (_, tac_, (p, is))) = split_last tacis |
|
505 (* for recursion ... |
|
506 (tacis', (_, tac_, (p, is))) = split_last tacis'; |
|
507 *) |
|
508 val (p',c',_,pt') = generate1 (assoc_thy "Isac.thy") tac_ is p pt |
|
509 in generate tacis' (pt', c@c', p') end; |
|
510 |
|
511 |
|
512 |
|
513 (*. a '_deriv'ation is constructed during 'reverse rewring' by an Rrls * |
|
514 * of for connecting a user-input formula with the current calc-state. * |
|
515 *# It is somewhat incompatible with the rest of the math-engine: * |
|
516 * (1) it is not created by a script * |
|
517 * (2) thus there cannot be another user-input within a derivation * |
|
518 *# It suffers particularily from the not-well-foundedness of the math-engine* |
|
519 * (1) FIXME other branchtyptes than Transitive will change 'embed_deriv' * |
|
520 * (2) FIXME and eventually 'compare_step' (ie. the script interpreter) * |
|
521 * (3) FIXME and eventually 'lev_back' * |
|
522 *# SOME improvements are evident FIXME.040215 '_deriv'ation: * |
|
523 * (1) FIXME nest Rls_ in 'make_deriv' * |
|
524 * (2) FIXME do the not-reversed part in 'make_deriv' by scripts -- thus * |
|
525 * user-input will become possible in this part of a derivation * |
|
526 * (3) FIXME do (2) only if a derivation has been found -- for efficiency, * |
|
527 * while a non-derivable inform requires to step until End_Proof' * |
|
528 * (4) FIXME find criteria on when _not_ to step until End_Proof' * |
|
529 * (5) FIXME |
|
530 .*) |
|
531 (*.update pos in tacis for embedding by generate.*) |
|
532 (* val |
|
533 *) |
|
534 fun insert_pos _ [] = [] |
|
535 | insert_pos (p:pos) (((tac,tac_,(_, ist))::tacis):taci list) = |
|
536 ((tac,tac_,((p, Res), ist)):taci) |
|
537 ::((insert_pos (lev_on p) tacis):taci list); |
|
538 |
|
539 fun res_from_taci (_, Rewrite'(_,_,_,_,_,_,(res, asm)), _) = (res, asm) |
|
540 | res_from_taci (_, Rewrite_Set'(_,_,_,_,(res, asm)), _) = (res, asm) |
|
541 | res_from_taci (_, tac_, _) = |
|
542 raise error ("res_from_taci: called with" ^ tac_2str tac_); |
|
543 |
|
544 (*.embed the tacis created by a '_deriv'ation; sys.form <> input.form |
|
545 tacis are in order, thus are reverted for generate.*) |
|
546 (* val (tacis, (pt, pos as (p, Frm))) = (tacis', ptp); |
|
547 *) |
|
548 fun embed_deriv (tacis:taci list) (pt, pos as (p, Frm):pos') = |
|
549 (*inform at Frm: replace the whole PrfObj by a Transitive-ProfObj FIXME?0402 |
|
550 and transfer the istate (from _after_ compare_deriv) from Frm to Res*) |
|
551 let val (res, asm) = (res_from_taci o last_elem) tacis |
|
552 val (SOME ist,_) = get_obj g_loc pt p |
|
553 val form = get_obj g_form pt p |
|
554 (*val p = lev_on p; ---------------only difference to (..,Res) below*) |
|
555 val tacis = (Begin_Trans, Begin_Trans' form, (pos, Uistate)) |
|
556 ::(insert_pos ((lev_on o lev_dn) p) tacis) |
|
557 @ [(End_Trans, End_Trans' (res, asm), |
|
558 (pos_plus (length tacis) (lev_dn p, Res), |
|
559 new_val res ist))] |
|
560 val {nrls,...} = get_met (get_obj g_metID pt (par_pblobj pt p)) |
|
561 val (pt, c, pos as (p,_)) = generate (rev tacis) (pt, [], (p, Res)) |
|
562 val pt = update_tac pt p (Derive (id_rls nrls)) |
|
563 (*FIXME.040216 struct.ctree*) |
|
564 val pt = update_branch pt p TransitiveB |
|
565 in (c, (pt, pos:pos')) end |
|
566 |
|
567 (* val (tacis, (pt, (p, Res))) = (tacis', ptp); |
|
568 *) |
|
569 | embed_deriv tacis (pt, (p, Res)) = |
|
570 (*inform at Res: append a Transitive-PrfObj FIXME?0402 other branch-types ? |
|
571 and transfer the istate (from _after_ compare_deriv) from Res to new Res*) |
|
572 let val (res, asm) = (res_from_taci o last_elem) tacis |
|
573 val (_, SOME ist) = get_obj g_loc pt p |
|
574 val (f,a) = get_obj g_result pt p |
|
575 val p = lev_on p(*---------------only difference to (..,Frm) above*); |
|
576 val tacis = (Begin_Trans, Begin_Trans' f, ((p, Frm), Uistate)) |
|
577 ::(insert_pos ((lev_on o lev_dn) p) tacis) |
|
578 @ [(End_Trans, End_Trans' (res, asm), |
|
579 (pos_plus (length tacis) (lev_dn p, Res), |
|
580 new_val res ist))]; |
|
581 val {nrls,...} = get_met (get_obj g_metID pt (par_pblobj pt p)) |
|
582 val (pt, c, pos as (p,_)) = generate (rev tacis) (pt, [], (p, Res)) |
|
583 val pt = update_tac pt p (Derive (id_rls nrls)) |
|
584 (*FIXME.040216 struct.ctree*) |
|
585 val pt = update_branch pt p TransitiveB |
|
586 in (c, (pt, pos)) end; |
|