446 | contain_bdv (Rls_ rls ::rs) = |
446 | contain_bdv (Rls_ rls ::rs) = |
447 contain_bdv (get_rules rls) orelse contain_bdv rs |
447 contain_bdv (get_rules rls) orelse contain_bdv rs |
448 | contain_bdv (r::_) = |
448 | contain_bdv (r::_) = |
449 error ("contain_bdv called with ["^(id_rule r)^",...]"); |
449 error ("contain_bdv called with ["^(id_rule r)^",...]"); |
450 |
450 |
451 (* get a substitution for "bdv*" from the current program and environment*) |
|
452 fun get_bdv_subst prog env = |
|
453 let |
|
454 fun scan (Const _) = NONE |
|
455 | scan (Free _) = NONE |
|
456 | scan (Var _) = NONE |
|
457 | scan (Bound _) = NONE |
|
458 | scan (t as Const ("List.list.Cons", _) $ |
|
459 (Const ("Product_Type.Pair", _) $ Free (str, _) $ _) $ _) = |
|
460 if is_bdv_subst t then SOME t else NONE |
|
461 | scan (Abs (_, _, body)) = scan body |
|
462 | scan (t1 $ t2) = |
|
463 case scan t1 of |
|
464 NONE => scan t2 |
|
465 | SOME subst => SOME subst |
|
466 in |
|
467 case scan prog of |
|
468 NONE => []: subst |
|
469 | SOME subs => |
|
470 (subs |> subst_atomic env |> isalist2list |> map isapair2pair) |
|
471 (*"[(bdv,v_v)]": term |
|
472 |> "[(bdv,x)]": term |> ["(bdv,x)"]: term list |
|
473 |> [("bdv","x")]: (term * term) list*) |
|
474 end; |
|
475 |
|
476 fun rules2scr_Rls calc rules = (*WN100816 t_ -> t_t like "Script Stepwise..*) |
451 fun rules2scr_Rls calc rules = (*WN100816 t_ -> t_t like "Script Stepwise..*) |
477 if contain_bdv rules |
452 if contain_bdv rules |
478 then ScrStep_inst $ Term $ Bdv $ |
453 then ScrStep_inst $ Term $ Bdv $ |
479 (Repeat $ (((@@ o (map (rule2stac_inst calc))) rules) $ e_term)) |
454 (Repeat $ (((@@ o (map (rule2stac_inst calc))) rules) $ e_term)) |
480 else ScrStep $ Term $ |
455 else ScrStep $ Term $ |