48 Rule.Rrls {scr = Rule.Rfuns {init_state = ii, ...}, ...} => Selem.RrlsState (ii t) |
48 Rule.Rrls {scr = Rule.Rfuns {init_state = ii, ...}, ...} => Selem.RrlsState (ii t) |
49 | Rule.Rls {scr = Rule.EmptyScr, ...} => |
49 | Rule.Rls {scr = Rule.EmptyScr, ...} => |
50 error ("interSteps>..>init_istate: \"" ^ rls ^ "\" has EmptyScr." ^ |
50 error ("interSteps>..>init_istate: \"" ^ rls ^ "\" has EmptyScr." ^ |
51 "use prep_rls' for storing rule-sets !") |
51 "use prep_rls' for storing rule-sets !") |
52 | Rule.Rls {scr = Rule.Prog s, ...} => |
52 | Rule.Rls {scr = Rule.Prog s, ...} => |
53 (Selem.ScrState ([(LTool.one_scr_arg s, t)], [], NONE, Rule.e_term, Selem.Sundef, true)) |
53 (Selem.ScrState ([(hd (LTool.formal_args s), t)], [], NONE, Rule.e_term, Selem.Sundef, true)) |
54 | Rule.Seq {scr = Rule.EmptyScr,...} => |
54 | Rule.Seq {scr = Rule.EmptyScr,...} => |
55 error ("interSteps>..>init_istate: \"" ^ rls ^ "\" has EmptyScr." ^ |
55 error ("interSteps>..>init_istate: \"" ^ rls ^ "\" has EmptyScr." ^ |
56 " Use prep_rls' for storing rule-sets !") |
56 " Use prep_rls' for storing rule-sets !") |
57 | Rule.Seq {scr = Rule.Prog s,...} => |
57 | Rule.Seq {scr = Rule.Prog s,...} => |
58 (writeln ("### init_istate: rls = \"" ^ "rls" ^ "\", Prog = \"" ^ Rule.term2str s ^ "\""); |
58 (writeln ("### init_istate: rls = \"" ^ "rls" ^ "\", Prog = \"" ^ Rule.term2str s ^ "\""); |
59 (Selem.ScrState ([(LTool.one_scr_arg s, t)], [], NONE, Rule.e_term, Selem.Sundef, true)) |
59 (Selem.ScrState ([(hd (LTool.formal_args s), t)], [], NONE, Rule.e_term, Selem.Sundef, true)) |
60 ) |
60 ) |
61 | _ => error "init_istate Rewrite_Set: uncovered case assoc_rls") |
61 | _ => error "init_istate Rewrite_Set: uncovered case assoc_rls") |
62 | init_istate (Tac.Rewrite_Set_Inst (subs, rls)) t = |
62 | init_istate (Tac.Rewrite_Set_Inst (subs, rls)) t = |
63 let |
63 let |
64 val v = case Selem.subs2subst (Celem.assoc_thy "Isac") subs of |
64 val v = case Selem.subs2subst (Celem.assoc_thy "Isac") subs of |
68 in case assoc_rls rls of |
68 in case assoc_rls rls of |
69 Rule.Rls {scr = Rule.EmptyScr, ...} => |
69 Rule.Rls {scr = Rule.EmptyScr, ...} => |
70 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." ^ |
70 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." ^ |
71 "use prep_rls' for storing rule-sets !") |
71 "use prep_rls' for storing rule-sets !") |
72 | Rule.Rls {scr = Rule.Prog s, ...} => |
72 | Rule.Rls {scr = Rule.Prog s, ...} => |
73 let val (form, bdv) = LTool.two_scr_arg s |
73 let val env = (LTool.formal_args s) ~~ [t, v] |
74 in (Selem.ScrState ([(form, t), (bdv, v)], [], NONE, Rule.e_term, Selem.Sundef,true)) |
74 in (Selem.ScrState (env, [], NONE, Rule.e_term, Selem.Sundef,true)) |
75 end |
75 end |
76 | Rule.Seq {scr = Rule.EmptyScr, ...} => |
76 | Rule.Seq {scr = Rule.EmptyScr, ...} => |
77 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." ^ |
77 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." ^ |
78 "use prep_rls' for storing rule-sets !") |
78 "use prep_rls' for storing rule-sets !") |
79 | Rule.Seq {scr = Rule.Prog s,...} => |
79 | Rule.Seq {scr = Rule.Prog s,...} => |
80 let val (form, bdv) = LTool.two_scr_arg s |
80 let val env = (LTool.formal_args s) ~~ [t, v] |
81 in (Selem.ScrState ([(form, t), (bdv, v)],[], NONE, Rule.e_term, Selem.Sundef,true)) |
81 in (Selem.ScrState (env,[], NONE, Rule.e_term, Selem.Sundef,true)) |
82 end |
82 end |
83 | _ => error "init_istate Rewrite_Set_Inst: uncovered case assoc_rls" |
83 | _ => error "init_istate Rewrite_Set_Inst: uncovered case assoc_rls" |
84 end |
84 end |
85 | init_istate tac _ = error ("init_istate: uncovered definition for " ^ Tac.tac2str tac) |
85 | init_istate tac _ = error ("init_istate: uncovered definition for " ^ Tac.tac2str tac) |
86 |
86 |