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