60 (**) |
60 (**) |
61 |
61 |
62 open Celem |
62 open Celem |
63 |
63 |
64 datatype asap = (* arg. of scan_dn1 _only_ for distinction w.r.t. Or *) |
64 datatype asap = (* arg. of scan_dn1 _only_ for distinction w.r.t. Or *) |
65 Aundef (* undefined: set only by (topmost) Or *) |
65 ORundef (* undefined: set only by (topmost) Or *) |
66 | AssOnly (* do not execute applicable Prog_Tac - there could be an associated |
66 | AssOnly (* do not execute applicable Prog_Tac - there could be an associated |
67 in parallel Or-branch *) |
67 in parallel Or-branch *) |
68 | AssGen; (* no Ass(Weak) found within Or, thus continue scan |
68 | AssGen; (* no Ass(Weak) found within Or, thus continue scan |
69 search for _applicable_ stacs, execute and generate pt *) |
69 search for _applicable_ stacs, execute and generate pt *) |
70 (*this constructions doesnt allow arbitrary nesting of Or !!! *) |
70 (*this constructions doesnt allow arbitrary nesting of Or !!! *) |
71 fun asap2str Aundef = "Aundef" |
71 fun asap2str ORundef = "ORundef" |
72 | asap2str AssOnly = "AssOnly" |
72 | asap2str AssOnly = "AssOnly" |
73 | asap2str AssGen = "AssGen" |
73 | asap2str AssGen = "AssGen" |
74 |
74 |
75 datatype appy_ = (* as argument in scan_up2, go_scan_up2, from scan_dn2 *) |
75 datatype appy_ = (* as argument in scan_up2, go_scan_up2, from scan_dn2 *) |
76 (*Ackn_Tac2 is only (final) returnvalue, not argument during search *) |
76 (*Accept_Tac2 is only (final) returnvalue, not argument during search *) |
77 AppUndef_ |
77 AppUndef_ |
78 | Napp_ (* ev. detects 'script is not appropriate for this example' *) |
78 | Napp_ (* ev. detects 'script is not appropriate for this example' *) |
79 | Skip_; (* detects 'script successfully finished' |
79 | Skip_; (* detects 'script successfully finished' |
80 also used as init-value for resuming; this works, |
80 also used as init-value for resuming; this works, |
81 because 'nxt_up Or e1' treats as Ackn_Tac2 *) |
81 because 'nxt_up Or e1' treats as Accept_Tac2 *) |
82 fun appy_2str AppUndef_ = "AppUndef_" |
82 fun appy_2str AppUndef_ = "AppUndef_" |
83 | appy_2str Napp_ = "Napp_" |
83 | appy_2str Napp_ = "Napp_" |
84 | appy_2str Skip_ = "Skip_" |
84 | appy_2str Skip_ = "Skip_" |
85 |
85 |
86 type pstate = |
86 type pstate = |
92 or: asap, (* flag for scanning tactical "Or" *) |
92 or: asap, (* flag for scanning tactical "Or" *) |
93 finish: appy_, (* flag set after execution of a tactic *) |
93 finish: appy_, (* flag set after execution of a tactic *) |
94 assoc: bool} (* is the tactic associated to input *) |
94 assoc: bool} (* is the tactic associated to input *) |
95 val e_scrstate = |
95 val e_scrstate = |
96 {env = [], path = [], eval = Rule.e_rls, form_arg = NONE, act_arg = Rule.e_term, |
96 {env = [], path = [], eval = Rule.e_rls, form_arg = NONE, act_arg = Rule.e_term, |
97 or = Aundef, finish = AppUndef_, assoc = false} |
97 or = ORundef, finish = AppUndef_, assoc = false} |
98 fun topt2str NONE = "NONE" |
98 fun topt2str NONE = "NONE" |
99 | topt2str (SOME t) = "SOME" ^ Rule.term2str t; |
99 | topt2str (SOME t) = "SOME" ^ Rule.term2str t; |
100 fun scrstate2str {env, path, eval, form_arg, act_arg, or, finish, assoc} = (* for tests only *) |
100 fun scrstate2str {env, path, eval, form_arg, act_arg, or, finish, assoc} = (* for tests only *) |
101 "(" ^ Env.env2str env ^ ", " ^ Celem.path2str path ^ ", " ^ Rule.id_rls eval ^ ", " ^ |
101 "(" ^ Env.env2str env ^ ", " ^ Celem.path2str path ^ ", " ^ Rule.id_rls eval ^ ", " ^ |
102 topt2str form_arg ^ ", \n" ^ Rule.term2str act_arg ^ ", " ^ asap2str or ^ ", " ^ |
102 topt2str form_arg ^ ", \n" ^ Rule.term2str act_arg ^ ", " ^ asap2str or ^ ", " ^ |
186 fun set_subst_false (form_arg, act_arg) {env, path, eval, or, finish, ...} = |
186 fun set_subst_false (form_arg, act_arg) {env, path, eval, or, finish, ...} = |
187 {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg, |
187 {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg, |
188 or = or, finish = finish, assoc = false} |
188 or = or, finish = finish, assoc = false} |
189 fun set_subst_reset (form_arg, act_arg) {env, path, eval, ...} = (*compare NEW OLD usage*) |
189 fun set_subst_reset (form_arg, act_arg) {env, path, eval, ...} = (*compare NEW OLD usage*) |
190 {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg, |
190 {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg, |
191 or = Aundef, finish = AppUndef_, assoc = false} |
191 or = ORundef, finish = AppUndef_, assoc = false} |
192 |
192 |
193 fun set_env env {path, eval, form_arg, act_arg, or, finish, assoc, ...} = |
193 fun set_env env {path, eval, form_arg, act_arg, or, finish, assoc, ...} = |
194 {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg, |
194 {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg, |
195 or = or, finish = finish, assoc = assoc} |
195 or = or, finish = finish, assoc = assoc} |
196 fun set_env_true env {path, eval, form_arg, act_arg, or, finish, ...} = |
196 fun set_env_true env {path, eval, form_arg, act_arg, or, finish, ...} = |