173 | scan_dn (cc as (_, ctxt)) (ist as {eval, ...}) (Const (\<^const_name>\<open>Tactical.If\<close>(*1*), _) $ c $ e1 $ e2) = |
173 | scan_dn (cc as (_, ctxt)) (ist as {eval, ...}) (Const (\<^const_name>\<open>Tactical.If\<close>(*1*), _) $ c $ e1 $ e2) = |
174 if Rewrite.eval_true_ ctxt eval (subst_atomic (Env.update_opt' (get_subst ist)) c) |
174 if Rewrite.eval_true_ ctxt eval (subst_atomic (Env.update_opt' (get_subst ist)) c) |
175 then scan_dn cc (ist |> path_down [L, R]) e1 |
175 then scan_dn cc (ist |> path_down [L, R]) e1 |
176 else scan_dn cc (ist |> path_down [R]) e2 |
176 else scan_dn cc (ist |> path_down [R]) e2 |
177 |
177 |
178 | scan_dn (cc as (_, ctxt)) (ist as {eval, ...}) t = |
178 | scan_dn (cc as (_, ctxt)) (ist as {eval, ...}) t (*fall-through*) = |
179 if Tactical.contained_in t |
179 if Tactical.contained_in t |
180 then raise TERM ("scan_dn expects Prog_Tac or Prog_Expr", [t]) |
180 then raise TERM ("scan_dn expects Prog_Tac or Prog_Expr", [t]) |
181 else |
181 else |
182 case LItool.check_leaf "next " ctxt eval (get_subst ist) t of |
182 case LItool.check_leaf "next " ctxt eval (get_subst ist) t of |
183 (Program.Expr s, _) => Term_Val s (*TODO?: include set_found here and drop those after call*) |
183 (Program.Expr s, _) => Term_Val s (*TODO?: include set_found here and drop those after call*) |
184 | (Program.Tac prog_tac, form_arg) => |
184 | (Program.Tac prog_tac, form_arg) => |
185 check_tac cc ist (prog_tac, form_arg) |
185 (tracing ("### scan_dn fall-through, prog_tac = " ^ quote (UnparseC.term prog_tac) ^ " |"); |
186 |
186 check_tac cc ist (prog_tac, form_arg)) |
|
187 |
187 fun go_scan_up (pcc as (sc, _)) (ist as {path, act_arg, found_accept, ...}) = |
188 fun go_scan_up (pcc as (sc, _)) (ist as {path, act_arg, found_accept, ...}) = |
188 if path = [R] (*root of the program body*) then |
189 if path = [R] (*root of the program body*) then |
189 if found_accept then |
190 if found_accept then |
190 Term_Val act_arg |
191 Term_Val act_arg |
191 else raise ERROR "LItool.find_next_step without result" |
192 else raise ERROR "LItool.find_next_step without result" |