1.1 --- a/src/Tools/isac/Interpret/step-solve.sml Sun Jan 08 10:30:58 2023 +0100
1.2 +++ b/src/Tools/isac/Interpret/step-solve.sml Sun Jan 08 12:33:27 2023 +0100
1.3 @@ -36,45 +36,46 @@
1.4 ("ok", ([(Tactic.End_Detail, Tactic.End_Detail' t , ((p, p_), get_loc pt (p, p_)))], [], (pt, pr)))
1.5 end
1.6 | by_tactic m (pt, po as (p, p_)) =
1.7 - if MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*29.8.02: could be detail, too !!*)
1.8 - then
1.9 - let
1.10 - val ctxt = get_ctxt pt po
1.11 - val ((p, p_), ps, _, pt) = Solve_Step.add_general m (Istate.empty, ctxt) (pt, (p, p_))
1.12 - in ("no-method-specified", (*Free_Solve*)
1.13 - ([(Tactic.Empty_Tac, Tactic.Empty_Tac_, ((p, p_), (Istate.Uistate, ctxt)))], ps, (pt, (p, p_))))
1.14 - end
1.15 - else
1.16 - let
1.17 - val (is, sc) = LItool.resume_prog (p,p_) pt;
1.18 - in
1.19 - case LI.locate_input_tactic sc (pt, po) (fst is) (snd is) m of
1.20 - LI.Safe_Step (istate, ctxt, tac) =>
1.21 - let
1.22 - val p' = next_in_prog po
1.23 - val (p'', _, _,pt') = Solve_Step.add_general tac (istate, ctxt) (pt, (p', p_))
1.24 - in
1.25 - ("ok", ([(Tactic.input_from_T ctxt tac, tac, (p'', (istate, ctxt)))],
1.26 - [(*Ctree NOT cut*)], (pt', p'')))
1.27 + let
1.28 + val ctxt = get_ctxt pt po
1.29 + val thy = Proof_Context.theory_of ctxt
1.30 + in
1.31 + if MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*29.8.02: could be detail, too !!*)
1.32 + then
1.33 + let val ((p, p_), ps, _, pt) = Solve_Step.add_general m (Istate.empty, ctxt) (pt, (p, p_))
1.34 + in ("no-method-specified", (*Free_Solve*)
1.35 + ([(Tactic.Empty_Tac, Tactic.Empty_Tac_, ((p, p_), (Istate.Uistate, ctxt)))], ps, (pt, (p, p_))))
1.36 + end
1.37 + else
1.38 + let val (is, sc) = LItool.resume_prog (p,p_) pt;
1.39 + in
1.40 + case LI.locate_input_tactic sc (pt, po) (fst is) (snd is) m of
1.41 + LI.Safe_Step (istate, ctxt, tac) =>
1.42 + let
1.43 + val p' = next_in_prog po
1.44 + val (p'', _, _,pt') = Solve_Step.add_general tac (istate, ctxt) (pt, (p', p_))
1.45 + in
1.46 + ("ok", ([(Tactic.input_from_T ctxt tac, tac, (p'', (istate, ctxt)))],
1.47 + [(*Ctree NOT cut*)], (pt', p'')))
1.48 + end
1.49 + | LI.Unsafe_Step (istate, ctxt, tac) =>
1.50 + let
1.51 + val p' =
1.52 + case p_ of Frm => p
1.53 + | Res => lev_on p
1.54 + | _ => raise ERROR ("Step_Solve.by_tactic: call by " ^ pos'2str (p, p_));
1.55 + val (p'', _, _,pt') = Solve_Step.add_general tac (istate, ctxt) (pt, (p', p_));
1.56 + in
1.57 + ("ok", ([(Tactic.input_from_T ctxt tac, tac, (p'', (istate, ctxt)))],
1.58 + [(*Ctree NOT cut*)], (pt', p'')))
1.59 + end
1.60 + | _ => (* NotLocatable *)
1.61 + let val (p,ps, _, pt) = Solve_Step.add_hard thy m (p, p_) pt;
1.62 + in
1.63 + ("not-found-in-program", ([(Tactic.input_from_T ContextC.empty m, m, (po, is))], ps, (pt, p)))
1.64 end
1.65 - | LI.Unsafe_Step (istate, ctxt, tac) =>
1.66 - let
1.67 - val p' =
1.68 - case p_ of Frm => p
1.69 - | Res => lev_on p
1.70 - | _ => raise ERROR ("Step_Solve.by_tactic: call by " ^ pos'2str (p, p_));
1.71 - val (p'', _, _,pt') = Solve_Step.add_general tac (istate, ctxt) (pt, (p', p_));
1.72 - in
1.73 - ("ok", ([(Tactic.input_from_T ctxt tac, tac, (p'', (istate, ctxt)))],
1.74 - [(*Ctree NOT cut*)], (pt', p'')))
1.75 - end
1.76 - | _ => (* NotLocatable *)
1.77 - let
1.78 - val (p,ps, _, pt) = Solve_Step.add_hard (ThyC.get_theory "Isac_Knowledge") m (p, p_) pt;
1.79 - in
1.80 - ("not-found-in-program", ([(Tactic.input_from_T ContextC.empty m, m, (po, is))], ps, (pt, p)))
1.81 - end
1.82 - end;
1.83 + end
1.84 + end;
1.85
1.86 val do_next = LI.do_next
1.87
2.1 --- a/src/Tools/isac/MathEngine/fetch-tactics.sml Sun Jan 08 10:30:58 2023 +0100
2.2 +++ b/src/Tools/isac/MathEngine/fetch-tactics.sml Sun Jan 08 12:33:27 2023 +0100
2.3 @@ -27,12 +27,11 @@
2.4 else
2.5 let
2.6 val pp = par_pblobj pt p;
2.7 - val thy' = get_obj g_domID pt pp;
2.8 - val thy = ThyC.get_theory thy';
2.9 val ctxt = Ctree.get_ctxt pt pos
2.10 - val metID = get_obj g_metID pt pp;
2.11 - val metID' = if metID = MethodC.id_empty then (thd3 o snd3) (get_obj g_origin pt pp) else metID
2.12 - val (sc, prog_rls) = (case MethodC.from_store ctxt metID' of
2.13 + val met_id = get_obj g_metID pt pp;
2.14 + val met_id_ori = (thd3 o snd3) (get_obj g_origin pt pp)
2.15 + val met_id' = if met_id = MethodC.id_empty then met_id_ori else met_id
2.16 + val (sc, prog_rls) = (case MethodC.from_store ctxt met_id' of
2.17 {program = Rule.Prog sc, prog_rls, ...} => (sc, prog_rls) | _ => raise ERROR "from_prog 1")
2.18 val subst = get_istate_LI pt (p, p_) |> Istate.the_pstate |> Istate.get_subst
2.19 val ctxt = get_ctxt pt (p, p_)
2.20 @@ -51,8 +50,6 @@
2.21 let
2.22 val pp = par_pblobj pt p
2.23 val ctxt = Ctree.get_loc pt pos |> snd
2.24 - val thy = Ctree.get_loc pt pos |> snd |> Proof_Context.theory_of
2.25 -
2.26 val metID = get_obj g_metID pt pp
2.27 val metID' =
2.28 if metID = MethodC.id_empty