143 |
143 |
144 |
144 |
145 (**.construct scr-env from scr(created automatically) and Rewrite_Set.**) |
145 (**.construct scr-env from scr(created automatically) and Rewrite_Set.**) |
146 |
146 |
147 fun one_scr_arg (Const _ $ arg $ _) = arg |
147 fun one_scr_arg (Const _ $ arg $ _) = arg |
148 | one_scr_arg t = raise error ("one_scr_arg: called by "^(term2str t)); |
148 | one_scr_arg t = error ("one_scr_arg: called by "^(term2str t)); |
149 fun two_scr_arg (Const _ $ a1 $ a2 $ _) = (a1, a2) |
149 fun two_scr_arg (Const _ $ a1 $ a2 $ _) = (a1, a2) |
150 | two_scr_arg t = raise error ("two_scr_arg: called by "^(term2str t)); |
150 | two_scr_arg t = error ("two_scr_arg: called by "^(term2str t)); |
151 |
151 |
152 |
152 |
153 (**.generate calc from a script.**) |
153 (**.generate calc from a script.**) |
154 |
154 |
155 (*.instantiate a stactic or scriptexpr, and ev. attach (curried) argument |
155 (*.instantiate a stactic or scriptexpr, and ev. attach (curried) argument |
165 (b) not curried: then the values of the initialization are not used |
165 (b) not curried: then the values of the initialization are not used |
166 .*) |
166 .*) |
167 datatype stacexpr = STac of term | Expr of term |
167 datatype stacexpr = STac of term | Expr of term |
168 fun rep_stacexpr (STac t ) = t |
168 fun rep_stacexpr (STac t ) = t |
169 | rep_stacexpr (Expr t) = |
169 | rep_stacexpr (Expr t) = |
170 raise error ("rep_stacexpr called with t= "^(term2str t)); |
170 error ("rep_stacexpr called with t= "^(term2str t)); |
171 |
171 |
172 type env = (term * term) list; |
172 type env = (term * term) list; |
173 |
173 |
174 (*update environment; t <> empty if coming from listexpr*) |
174 (*update environment; t <> empty if coming from listexpr*) |
175 fun upd_env (env:env) (v,t) = |
175 fun upd_env (env:env) (v,t) = |
298 fun is_calc (Const ("Script.Calculate",_) $ _) = true |
298 fun is_calc (Const ("Script.Calculate",_) $ _) = true |
299 | is_calc (Const ("Script.Calculate",_) $ _ $ _) = true |
299 | is_calc (Const ("Script.Calculate",_) $ _ $ _) = true |
300 | is_calc _ = false; |
300 | is_calc _ = false; |
301 fun op_of_calc (Const ("Script.Calculate",_) $ Free (op_,_)) = op_ |
301 fun op_of_calc (Const ("Script.Calculate",_) $ Free (op_,_)) = op_ |
302 | 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); |
303 | op_of_calc t = error ("op_of_calc called with"^term2str t); |
304 (* |
304 (* |
305 val Script sc = (#scr o rep_rls) Test_simplify; |
305 val Script sc = (#scr o rep_rls) Test_simplify; |
306 val stacs = stacpbls sc; |
306 val stacs = stacpbls sc; |
307 |
307 |
308 val calcs = filter is_calc stacs; |
308 val calcs = filter is_calc stacs; |
438 | contain_bdv (Calc _ ::rs) = contain_bdv rs |
438 | contain_bdv (Calc _ ::rs) = contain_bdv rs |
439 | contain_bdv (Cal1 _ ::rs) = contain_bdv rs |
439 | contain_bdv (Cal1 _ ::rs) = contain_bdv rs |
440 | contain_bdv (Rls_ rls ::rs) = |
440 | contain_bdv (Rls_ rls ::rs) = |
441 contain_bdv (get_rules rls) orelse contain_bdv rs |
441 contain_bdv (get_rules rls) orelse contain_bdv rs |
442 | contain_bdv (r::_) = |
442 | contain_bdv (r::_) = |
443 raise error ("contain_bdv called with ["^(id_rule r)^",...]"); |
443 error ("contain_bdv called with ["^(id_rule r)^",...]"); |
444 |
444 |
445 fun rules2scr_Rls calc rules = (*WN100816 t_ -> t_t like "Script Stepwise..*) |
445 fun rules2scr_Rls calc rules = (*WN100816 t_ -> t_t like "Script Stepwise..*) |
446 if contain_bdv rules |
446 if contain_bdv rules |
447 then ScrStep_inst $ Term $ Bdv $ |
447 then ScrStep_inst $ Term $ Bdv $ |
448 (Repeat $ (((@@ o (map (rule2stac_inst calc))) rules) $ e_term)) |
448 (Repeat $ (((@@ o (map (rule2stac_inst calc))) rules) $ e_term)) |
459 |
459 |
460 (*.prepare the input for an rls for use: |
460 (*.prepare the input for an rls for use: |
461 # generate a script for stepwise execution of the rls |
461 # generate a script for stepwise execution of the rls |
462 # filter the operators for Calc out of the script |
462 # filter the operators for Calc out of the script |
463 !!!use this function in ruleset' := !!! .*) |
463 !!!use this function in ruleset' := !!! .*) |
464 fun prep_rls Erls = raise error "prep_rls not impl. for Erls" |
464 fun prep_rls Erls = error "prep_rls not impl. for Erls" |
465 | prep_rls (Rls {id,preconds,rew_ord,erls,srls,calc,rules,...}) = |
465 | prep_rls (Rls {id,preconds,rew_ord,erls,srls,calc,rules,...}) = |
466 let val sc = (rules2scr_Rls (!calclist') rules) |
466 let val sc = (rules2scr_Rls (!calclist') rules) |
467 in Rls {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls, |
467 in Rls {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls, |
468 srls=srls, |
468 srls=srls, |
469 calc = (*FIXXXME.040207 use also for met*) |
469 calc = (*FIXXXME.040207 use also for met*) |
480 calc = ((map (curry assoc1 (!calclist'))) o (map op_of_calc) o |
480 calc = ((map (curry assoc1 (!calclist'))) o (map op_of_calc) o |
481 (filter is_calc) o stacpbls) sc, |
481 (filter is_calc) o stacpbls) sc, |
482 rules=rules, |
482 rules=rules, |
483 scr = Script sc} end |
483 scr = Script sc} end |
484 | prep_rls (Rrls {id,...}) = |
484 | prep_rls (Rrls {id,...}) = |
485 raise error ("prep_rls not required for Rrls \""^id^"\""); |
485 error ("prep_rls not required for Rrls \""^id^"\""); |
486 (* |
486 (* |
487 val Script sc = (#scr o rep_rls o prep_rls) isolate_root; |
487 val Script sc = (#scr o rep_rls o prep_rls) isolate_root; |
488 (tracing o term2str) sc; |
488 (tracing o term2str) sc; |
489 val Script sc = (#scr o rep_rls o prep_rls) isolate_bdv; |
489 val Script sc = (#scr o rep_rls o prep_rls) isolate_bdv; |
490 (tracing o term2str) sc; |
490 (tracing o term2str) sc; |