|
1 (* tools which depend on Script.thy and thus are not in term_G.sml |
|
2 (c) Walther Neuper 2000 |
|
3 |
|
4 use"Scripts/scrtools.sml"; |
|
5 use"scrtools.sml"; |
|
6 *) |
|
7 |
|
8 |
|
9 fun is_reall_dsc |
|
10 (Const(_,Type("fun",[Type("List.list", |
|
11 [Type ("real",[])]),_]))) = true |
|
12 | is_reall_dsc |
|
13 (Const(_,Type("fun",[Type("List.list", |
|
14 [Type ("real",[])]),_])) $ t) = true |
|
15 | is_reall_dsc _ = false; |
|
16 fun is_booll_dsc |
|
17 (Const(_,Type("fun",[Type("List.list", |
|
18 [Type ("bool",[])]),_]))) = true |
|
19 | is_booll_dsc |
|
20 (Const(_,Type("fun",[Type("List.list", |
|
21 [Type ("bool",[])]),_])) $ t) = true |
|
22 | is_booll_dsc _ = false; |
|
23 (* |
|
24 > val t = (term_of o the o (parse thy)) "relations"; |
|
25 > atomtyp (type_of t); |
|
26 *** Type (fun,[ |
|
27 *** Type (List.list,[ |
|
28 *** Type (bool,[]) |
|
29 *** ] |
|
30 *** Type (Tools.una,[]) |
|
31 *** ] |
|
32 > is_booll_dsc t; |
|
33 val it = true : bool |
|
34 > is_reall_dsc t; |
|
35 val it = false : bool |
|
36 *) |
|
37 |
|
38 fun is_list_dsc (Const(_,Type("fun",[Type("List.list",_),_]))) = true |
|
39 | is_list_dsc (Const(_,Type("fun",[Type("List.list",_),_])) $ t) = true |
|
40 (*WN:8.5.03: ??? ~~~~ ???*) |
|
41 | is_list_dsc _ = false; |
|
42 (* |
|
43 > val t = str2term "someList"; |
|
44 > is_list_dsc t; |
|
45 val it = true : bool |
|
46 |
|
47 > val t = (term_of o the o (parse thy)) |
|
48 "additional_relations [a=b,c=(d::real)]"; |
|
49 > is_list_dsc t; |
|
50 val it = true : bool |
|
51 > is_list_dsc (head_of t); |
|
52 val it = true : bool |
|
53 |
|
54 > val t = (term_of o the o (parse thy))"max_relation (A=#2*a*b-a^^^#2)"; |
|
55 > is_list_dsc t; |
|
56 val it = false : bool |
|
57 > is_list_dsc (head_of t); |
|
58 val it = false : bool |
|
59 > val t = (term_of o the o (parse thy)) "testdscforlist"; |
|
60 > is_list_dsc (head_of t); |
|
61 val it = true : bool |
|
62 *) |
|
63 |
|
64 |
|
65 fun is_unl (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) = true |
|
66 | is_unl _ = false; |
|
67 (* |
|
68 > val t = str2term "someList"; is_unl t; |
|
69 val it = true : bool |
|
70 > val t = (term_of o the o (parse thy)) "maximum"; |
|
71 > is_unl t; |
|
72 val it = false : bool |
|
73 *) |
|
74 |
|
75 fun is_dsc (Const(_,Type("fun",[_,Type("Tools.nam",_)]))) = true |
|
76 | is_dsc (Const(_,Type("fun",[_,Type("Tools.una",_)]))) = true |
|
77 | is_dsc (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) = true |
|
78 | is_dsc (Const(_,Type("fun",[_,Type("Tools.str",_)]))) = true |
|
79 | is_dsc (Const(_,Type("fun",[_,Type("Tools.toreal",_)]))) = true |
|
80 | is_dsc (Const(_,Type("fun",[_,Type("Tools.toreall",_)])))= true |
|
81 | is_dsc (Const(_,Type("fun",[_,Type("Tools.tobooll",_)])))= true |
|
82 | is_dsc (Const(_,Type("fun",[_,Type("Tools.unknow",_)])))= true |
|
83 | is_dsc (Const(_,Type("fun",[_,Type("Tools.cpy",_)])))= true |
|
84 | is_dsc _ = false; |
|
85 fun is_dsc term = |
|
86 (case (range_type o type_of) term of |
|
87 Type("Tools.nam",_) => true |
|
88 | Type("Tools.una",_) => true |
|
89 | Type("Tools.unl",_) => true |
|
90 | Type("Tools.str",_) => true |
|
91 | Type("Tools.toreal",_) => true |
|
92 | Type("Tools.toreall",_) => true |
|
93 | Type("Tools.tobooll",_) => true |
|
94 | Type("Tools.unknow",_) => true |
|
95 | Type("Tools.cpy",_) => true |
|
96 | _ => false) |
|
97 handle Match => false; |
|
98 |
|
99 |
|
100 (* |
|
101 val t as t1 $ t2 = str2term "antiDerivativeName M_b"; |
|
102 val Const (_, Type ("fun", [Type ("fun", _), Type ("Tools.una",[])])) $ _ = t; |
|
103 is_dsc t1; |
|
104 |
|
105 > val t = (term_of o the o (parse thy)) "maximum"; |
|
106 > is_dsc t; |
|
107 val it = true : bool |
|
108 > val t = (term_of o the o (parse thy)) "testdscforlist"; |
|
109 > is_dsc t; |
|
110 val it = true : bool |
|
111 |
|
112 > val t = (head_of o term_of o the o (parse thy)) "maximum A"; |
|
113 > is_dsc t; |
|
114 val it = true : bool |
|
115 > val t = (head_of o term_of o the o (parse thy)) |
|
116 "fixedValues [R=(R::real)]"; |
|
117 > is_dsc t; |
|
118 val it = true : bool |
|
119 *) |
|
120 |
|
121 |
|
122 (*make the term 'Subproblem (domID, pblID)' to a formula for frontend; |
|
123 needs to be here after def. Subproblem in Script.thy*) |
|
124 val t as (subpbl_t $ (pair_t $ Free (domID,_) $ pblID)) = |
|
125 (term_of o the o (parse Script.thy)) |
|
126 "Subproblem (Isac,[equation,univar])"; |
|
127 val t as (pbl_t $ _) = |
|
128 (term_of o the o (parse Script.thy)) |
|
129 "Problem (Isac,[equation,univar])"; |
|
130 val Free (_, ID_type) = (term_of o the o (parse Script.thy)) "x::ID"; |
|
131 |
|
132 |
|
133 fun subpbl domID pblID = |
|
134 subpbl_t $ (pair_t $ Free (domID,ID_type) $ |
|
135 (((list2isalist ID_type) o (map (mk_free ID_type))) pblID)); |
|
136 (*> subpbl "Isac" ["equation","univar"] = t; |
|
137 val it = true : bool *) |
|
138 |
|
139 |
|
140 fun pblterm (domID:domID) (pblID:pblID) = |
|
141 pbl_t $ (pair_t $ Free (domID,ID_type) $ |
|
142 (((list2isalist ID_type) o (map (mk_free ID_type))) pblID)); |
|
143 |
|
144 |
|
145 (**.construct scr-env from scr(created automatically) and Rewrite_Set.**) |
|
146 |
|
147 fun one_scr_arg (Const _ $ arg $ _) = arg |
|
148 | one_scr_arg t = raise error ("one_scr_arg: called by "^(term2str t)); |
|
149 fun two_scr_arg (Const _ $ a1 $ a2 $ _) = (a1, a2) |
|
150 | two_scr_arg t = raise error ("two_scr_arg: called by "^(term2str t)); |
|
151 |
|
152 |
|
153 (**.generate calc from a script.**) |
|
154 |
|
155 (*.instantiate a stactic or scriptexpr, and ev. attach (curried) argument |
|
156 args: |
|
157 E environment |
|
158 v current value, is attached to curried stactics |
|
159 stac stactic to be instantiated |
|
160 precond: |
|
161 not (a = None) /\ (v = e_term) /\ (stac curried, i.e. without last arg.) |
|
162 this ........................ is the initialization for assy with l=[], |
|
163 but the 1st stac is |
|
164 (a) curried: then (a = Some _), or |
|
165 (b) not curried: then the values of the initialization are not used |
|
166 .*) |
|
167 datatype stacexpr = STac of term | Expr of term |
|
168 fun rep_stacexpr (STac t ) = t |
|
169 | rep_stacexpr (Expr t) = |
|
170 raise error ("rep_stacexpr called with t= "^(term2str t)); |
|
171 |
|
172 type env = (term * term) list; |
|
173 |
|
174 (*update environment; t <> empty if coming from listexpr*) |
|
175 fun upd_env (env:env) (v,t) = |
|
176 let val env' = if t = e_term then env else overwrite (env,(v,t)); |
|
177 (*val _= writeln("### upd_env: = "^(subst2str env'));*) |
|
178 in env' end; |
|
179 |
|
180 (*.substitute the scripts environment in a leaf of the scripts parse-tree |
|
181 and attach the curried argument of a tactic, if any. |
|
182 a leaf is either a tactic or an 'exp' in 'let v = expr' |
|
183 where 'exp' does not contain a tactic. |
|
184 CAUTION: (1) currying with @@ requires 2 patterns for each tactic |
|
185 (2) the non-curried version must return None for a |
|
186 (3) non-matching patterns become an Expr by fall-through. |
|
187 WN060906 quick and dirty fix: due to (2) a is returned, too.*) |
|
188 fun subst_stacexpr E a v (t as (Const ("Script.Rewrite",_) $ _ $ _ $ _ ))= |
|
189 (None, STac (subst_atomic E t)) |
|
190 |
|
191 | subst_stacexpr E a v (t as (Const ("Script.Rewrite",_) $ _ $ _ ))= |
|
192 (a, (*in these cases we hope, that a = Some _*) |
|
193 STac (case a of Some a' => (subst_atomic E (t $ a')) |
|
194 | None => ((subst_atomic E t) $ v))) |
|
195 |
|
196 | subst_stacexpr E a v |
|
197 (t as (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ $ _ )) = |
|
198 (None, STac (subst_atomic E t)) |
|
199 |
|
200 | subst_stacexpr E a v (t as (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _))= |
|
201 (a, STac (case a of Some a' => subst_atomic E (t $ a') |
|
202 | None => ((subst_atomic E t) $ v))) |
|
203 |
|
204 | subst_stacexpr E a v (t as (Const ("Script.Rewrite'_Set",_) $ _ $ _ $ _ ))= |
|
205 (None, STac (subst_atomic E t)) |
|
206 |
|
207 | subst_stacexpr E a v (t as (Const ("Script.Rewrite'_Set",_) $ _ $ _ )) = |
|
208 (a, STac (case a of Some a' => subst_atomic E (t $ a') |
|
209 | None => ((subst_atomic E t) $ v))) |
|
210 |
|
211 | subst_stacexpr E a v |
|
212 (t as (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ $ _ )) = |
|
213 (None, STac (subst_atomic E t)) |
|
214 |
|
215 | subst_stacexpr E a v |
|
216 (t as (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ )) = |
|
217 (a, STac (case a of Some a' => subst_atomic E (t $ a') |
|
218 | None => ((subst_atomic E t) $ v))) |
|
219 |
|
220 | subst_stacexpr E a v (t as (Const ("Script.Calculate",_) $ _ $ _ )) = |
|
221 (None, STac (subst_atomic E t)) |
|
222 |
|
223 | subst_stacexpr E a v (t as (Const ("Script.Calculate",_) $ _ )) = |
|
224 (a, STac (case a of Some a' => subst_atomic E (t $ a') |
|
225 | None => ((subst_atomic E t) $ v))) |
|
226 |
|
227 | subst_stacexpr E a v |
|
228 (t as (Const("Script.Check'_elementwise",_) $ _ $ _ )) = |
|
229 (None, STac (subst_atomic E t)) |
|
230 |
|
231 | subst_stacexpr E a v (t as (Const("Script.Check'_elementwise",_) $ _ )) = |
|
232 (a, STac (case a of Some a' => subst_atomic E (t $ a') |
|
233 | None => ((subst_atomic E t) $ v))) |
|
234 |
|
235 | subst_stacexpr E a v (t as (Const("Script.Or'_to'_List",_) $ _ )) = |
|
236 (None, STac (subst_atomic E t)) |
|
237 |
|
238 | subst_stacexpr E a v (t as (Const("Script.Or'_to'_List",_))) = (*t $ v*) |
|
239 (a, STac (case a of Some a' => subst_atomic E (t $ a') |
|
240 | None => ((subst_atomic E t) $ v))) |
|
241 |
|
242 | subst_stacexpr E a v (t as (Const ("Script.SubProblem",_) $ _ $ _ )) = |
|
243 (None, STac (subst_atomic E t)) |
|
244 |
|
245 | subst_stacexpr E a v (t as (Const ("Script.Take",_) $ _ )) = |
|
246 (None, STac (subst_atomic E t)) |
|
247 |
|
248 | subst_stacexpr E a v (t as (Const ("Script.Substitute",_) $ _ $ _ )) = |
|
249 (None, STac (subst_atomic E t)) |
|
250 |
|
251 | subst_stacexpr E a v (t as (Const ("Script.Substitute",_) $ _ )) = |
|
252 (a, STac (case a of Some a' => subst_atomic E (t $ a') |
|
253 | None => ((subst_atomic E t) $ v))) |
|
254 |
|
255 (*now all tactics are matched out and this leaf must be without a tactic*) |
|
256 | subst_stacexpr E a v t = |
|
257 (a, Expr (subst_atomic (case a of Some a => upd_env E (a,v) |
|
258 | None => E) t)); |
|
259 (*> val t = str2term "SubProblem(Test_, [linear, univariate, equation, test], [Test, solve_linear]) [bool_ e_, real_ v_]"; |
|
260 > subst_stacexpr [] None e_term t;*) |
|
261 |
|
262 |
|
263 fun stacpbls (h $ body) = |
|
264 let |
|
265 fun scan ts (Const ("Let",_) $ e $ (Abs (v,T,b))) = |
|
266 (scan ts e) @ (scan ts b) |
|
267 | scan ts (Const ("If",_) $ c $ e1 $ e2) = (scan ts e1) @ (scan ts e2) |
|
268 | scan ts (Const ("Script.While",_) $ c $ e $ _) = scan ts e |
|
269 | scan ts (Const ("Script.While",_) $ c $ e) = scan ts e |
|
270 | scan ts (Const ("Script.Repeat",_) $ e $ _) = scan ts e |
|
271 | scan ts (Const ("Script.Repeat",_) $ e) = scan ts e |
|
272 | scan ts (Const ("Script.Try",_) $ e $ _) = scan ts e |
|
273 | scan ts (Const ("Script.Try",_) $ e) = scan ts e |
|
274 | scan ts (Const ("Script.Or",_) $e1 $ e2 $ _) = |
|
275 (scan ts e1) @ (scan ts e2) |
|
276 | scan ts (Const ("Script.Or",_) $e1 $ e2) = |
|
277 (scan ts e1) @ (scan ts e2) |
|
278 | scan ts (Const ("Script.Seq",_) $e1 $ e2 $ _) = |
|
279 (scan ts e1) @ (scan ts e2) |
|
280 | scan ts (Const ("Script.Seq",_) $e1 $ e2) = |
|
281 (scan ts e1) @ (scan ts e2) |
|
282 | scan ts t = case subst_stacexpr [] None e_term t of |
|
283 (_, STac _) => [t] | (_, Expr _) => [] |
|
284 in (distinct o (scan [])) body end; |
|
285 (*sc = Solve_root_equation ... |
|
286 > val ts = stacpbls sc; |
|
287 > writeln (terms2str thy ts); |
|
288 ["Rewrite square_equation_left True e_", |
|
289 "Rewrite_Set SqRoot_simplify False e_", |
|
290 "Rewrite_Set rearrange_assoc False e_", |
|
291 "Rewrite_Set isolate_root False e_", |
|
292 "Rewrite_Set norm_equation False e_", |
|
293 "Rewrite_Set_Inst [(bdv, v_)] isolate_bdv False e_"] |
|
294 *) |
|
295 |
|
296 |
|
297 |
|
298 fun is_calc (Const ("Script.Calculate",_) $ _) = true |
|
299 | is_calc (Const ("Script.Calculate",_) $ _ $ _) = true |
|
300 | is_calc _ = false; |
|
301 fun op_of_calc (Const ("Script.Calculate",_) $ Free (op_,_)) = op_ |
|
302 | op_of_calc (Const ("Script.Calculate",_) $ Free (op_,_) $ _) = op_ |
|
303 | op_of_calc t = raise error ("op_of_calc called with"^term2str t); |
|
304 |
|
305 (*###################################################################### |
|
306 |
|
307 val Script sc = (#scr o rep_rls) Test_simplify; |
|
308 val stacs = stacpbls sc; |
|
309 |
|
310 val calcs = filter is_calc stacs; |
|
311 val ids = map op_of_calc calcs; |
|
312 map (curry assoc1 (!calclist')) ids; |
|
313 |
|
314 (((map (curry assoc1 (!calclist'))) o (map op_of_calc) o |
|
315 (filter is_calc) o stacpbls) sc):calc list; |
|
316 |
|
317 ######################################################################*) |
|
318 |
|
319 (**.for automatic creation of scripts from rls.**) |
|
320 |
|
321 val ScrStep $ _ $ _ = (*'z not affected by parse: 'a --> real*) |
|
322 ((inst_abs thy) o term_of o the o (parse thy)) |
|
323 "Script Stepwise (t_::'z) =\ |
|
324 \(Repeat\ |
|
325 \ ((Try (Repeat (Rewrite real_diff_minus False))) @@ \ |
|
326 \ (Try (Repeat (Rewrite real_add_commute False))) @@ \ |
|
327 \ (Try (Repeat (Rewrite real_mult_commute False)))) \ |
|
328 \ t_)"; |
|
329 (*WN060605 script-arg (t_::'z) and "Free (t_, 'a)" at end of body |
|
330 are inconsistent !!!*) |
|
331 val ScrStep_inst $ Term $ Bdv $ _=(*'z not affected by parse: 'a --> real*) |
|
332 ((inst_abs thy) o term_of o the o (parse thy)) |
|
333 "Script Stepwise_inst (t_::'z) (v_::real) =\ |
|
334 \(Repeat\ |
|
335 \ ((Try (Repeat (Rewrite_Inst [(bdv,v_)] real_diff_minus False))) @@ \ |
|
336 \ (Try (Repeat (Rewrite_Inst [(bdv,v_)] real_add_commute False))) @@\ |
|
337 \ (Try (Repeat (Rewrite_Inst [(bdv,v_)] real_mult_commute False)))) \ |
|
338 \ t_)"; |
|
339 val Repeat $ _ = |
|
340 ((inst_abs thy) o term_of o the o (parseN thy)) |
|
341 "Repeat (Rewrite real_diff_minus False t_)"; |
|
342 val Try $ _ = |
|
343 ((inst_abs thy) o term_of o the o (parseN thy)) |
|
344 "Try (Rewrite real_diff_minus False t_)"; |
|
345 val Cal $ _ = |
|
346 ((inst_abs thy) o term_of o the o (parseN thy)) |
|
347 "Calculate plus"; |
|
348 val Rew $ (Free (_,IDtype)) $ _ $ t_ = |
|
349 ((inst_abs thy) o term_of o the o (parseN thy)) |
|
350 "Rewrite real_diff_minus False t_"; |
|
351 val Rew_Inst $ Subs $ _ $ _ = |
|
352 ((inst_abs thy) o term_of o the o (parseN thy)) |
|
353 "Rewrite_Inst [(bdv,v_)] real_diff_minus False"; |
|
354 val Rew_Set $ _ $ _ = |
|
355 ((inst_abs thy) o term_of o the o (parseN thy)) |
|
356 "Rewrite_Set real_diff_minus False"; |
|
357 val Rew_Set_Inst $ _ $ _ $ _ = |
|
358 ((inst_abs thy) o term_of o the o (parseN thy)) |
|
359 "Rewrite_Set_Inst [(bdv,v_)] real_diff_minus False"; |
|
360 val SEq $ _ $ _ $ _ = |
|
361 ((inst_abs thy) o term_of o the o (parseN thy)) |
|
362 " ((Try (Repeat (Rewrite real_diff_minus False))) @@ \ |
|
363 \ (Try (Repeat (Rewrite real_add_commute False))) @@ \ |
|
364 \ (Try (Repeat (Rewrite real_mult_commute False)))) t_"; |
|
365 |
|
366 fun rule2stac _ (Thm (thmID, _)) = |
|
367 Try $ (Repeat $ (Rew $ Free (thmID, IDtype) $ HOLogic.false_const)) |
|
368 | rule2stac calc (Calc (c, _)) = |
|
369 Try $ (Repeat $ (Cal $ Free (assoc_calc (calc ,c), IDtype))) |
|
370 | rule2stac _ (Rls_ rls) = |
|
371 Try $ (Rew_Set $ Free (id_rls rls, IDtype) $ HOLogic.false_const); |
|
372 (*val t = rule2stac [] (Thm ("real_diff_minus", num_str real_diff_minus)); |
|
373 atomt t; term2str t; |
|
374 val t = rule2stac calclist (Calc ("op +", eval_binop "#add_")); |
|
375 atomt t; term2str t; |
|
376 val t = rule2stac [] (Rls_ rearrange_assoc); |
|
377 atomt t; term2str t; |
|
378 *) |
|
379 fun rule2stac_inst _ (Thm (thmID, _)) = |
|
380 Try $ (Repeat $ (Rew_Inst $ Subs $ Free (thmID, IDtype) $ |
|
381 HOLogic.false_const)) |
|
382 | rule2stac_inst calc (Calc (c, _)) = |
|
383 Try $ (Repeat $ (Cal $ Free (assoc_calc (calc ,c), IDtype))) |
|
384 | rule2stac_inst _ (Rls_ rls) = |
|
385 Try $ (Rew_Set_Inst $ Subs $ Free (id_rls rls, IDtype) $ |
|
386 HOLogic.false_const); |
|
387 (*val t = rule2stac_inst [] (Thm ("real_diff_minus", num_str real_diff_minus)); |
|
388 atomt t; term2str t; |
|
389 val t = rule2stac_inst calclist (Calc ("op +", eval_binop "#add_")); |
|
390 atomt t; term2str t; |
|
391 val t = rule2stac_inst [] (Rls_ rearrange_assoc); |
|
392 atomt t; term2str t; |
|
393 *) |
|
394 |
|
395 (*for appropriate nesting take stacs in _reverse_ order*) |
|
396 fun @@@ sts [s] = SEq $ s $ sts |
|
397 | @@@ sts (s::ss) = @@@ (SEq $ s $ sts) ss; |
|
398 fun @@ [stac] = stac |
|
399 | @@ [s1, s2] = SEq $ s1 $ s2 (*---------vvv--*) |
|
400 | @@ stacs = |
|
401 let val s3::s2::ss = rev stacs |
|
402 in @@@ (SEq $ s2 $ s3) ss end; |
|
403 (* |
|
404 val rules = (#rules o rep_rls) isolate_root; |
|
405 val rs = map (rule2stac calclist) rules; |
|
406 val tt = @@ rs; |
|
407 atomt tt; writeln (term2str tt); |
|
408 *) |
|
409 |
|
410 val contains_bdv = (not o null o (filter is_bdv) o ids2str o #prop o rep_thm); |
|
411 |
|
412 (*.does a rule contain a 'bdv'; descend recursively into Rls_.*) |
|
413 fun contain_bdv [] = false |
|
414 | contain_bdv (Thm (_, thm)::rs) = |
|
415 if (not o contains_bdv) thm |
|
416 then contain_bdv rs |
|
417 else true |
|
418 | contain_bdv (Calc _ ::rs) = contain_bdv rs |
|
419 | contain_bdv (Rls_ rls ::rs) = |
|
420 contain_bdv (get_rules rls) orelse contain_bdv rs |
|
421 | contain_bdv (r::_) = |
|
422 raise error ("contain_bdv called with ["^(id_rule r)^",...]"); |
|
423 |
|
424 |
|
425 fun rules2scr_Rls calc rules = |
|
426 if contain_bdv rules |
|
427 then ScrStep_inst $ Term $ Bdv $ |
|
428 (Repeat $ (((@@ o (map (rule2stac_inst calc))) rules) $ t_)) |
|
429 else ScrStep $ Term $ |
|
430 (Repeat $ (((@@ o (map (rule2stac calc))) rules) $ t_)); |
|
431 fun rules2scr_Seq calc rules = |
|
432 if contain_bdv rules |
|
433 then ScrStep_inst $ Term $ Bdv $ |
|
434 (((@@ o (map (rule2stac_inst calc))) rules) $ t_) |
|
435 else ScrStep $ Term $ |
|
436 (((@@ o (map (rule2stac calc))) rules) $ t_); |
|
437 |
|
438 (*.prepare the input for an rls for use: |
|
439 # generate a script for stepwise execution of the rls |
|
440 # filter the operators for Calc out of the script |
|
441 !!!use this function in ruleset' := !!! .*) |
|
442 fun prep_rls Erls = raise error "prep_rls not impl. for Erls" |
|
443 | prep_rls (Rls {id,preconds,rew_ord,erls,srls,calc,rules,...}) = |
|
444 let val sc = (rules2scr_Rls (!calclist') rules) |
|
445 in Rls {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls, |
|
446 srls=srls, |
|
447 calc = (*FIXXXME.040207 use also for met*) |
|
448 ((map (curry assoc1 (!calclist'))) o (map op_of_calc) o |
|
449 (filter is_calc) o stacpbls) sc, |
|
450 rules=rules, |
|
451 scr = Script sc} end |
|
452 | prep_rls (Seq {id,preconds,rew_ord,erls,srls,calc,rules,...}) = |
|
453 let val sc = (rules2scr_Seq (!calclist') rules) |
|
454 in Seq {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls, |
|
455 srls=srls, |
|
456 calc = ((map (curry assoc1 (!calclist'))) o (map op_of_calc) o |
|
457 (filter is_calc) o stacpbls) sc, |
|
458 rules=rules, |
|
459 scr = Script sc} end |
|
460 | prep_rls (Rrls {id,...}) = |
|
461 raise error ("prep_rls not required for Rrls \""^id^"\""); |
|
462 (* |
|
463 val Script sc = (#scr o rep_rls o prep_rls) isolate_root; |
|
464 (writeln o term2str) sc; |
|
465 val Script sc = (#scr o rep_rls o prep_rls) isolate_bdv; |
|
466 (writeln o term2str) sc; |
|
467 *) |
|
468 |