1 (* Title: Interpret/step-solve.sml
2 Author: Walther Neuper 2019
3 (c) due to copyright terms
8 val do_next: Calc.T -> string * Calc.state_post
9 val by_tactic : Tactic.T -> Calc.T -> string * Calc.state_post
10 val by_term : Calc.T -> string -> string * Calc.state_post (*TODO: string * Calc.T*)
14 structure Step_Solve(**): STEP_SOLVE(**) =
20 fun by_tactic (tac as Tactic.Apply_Method' _) (ptp as (pt, p)) =
21 LI.by_tactic tac (get_istate_LI pt p, get_ctxt_LI pt p) ptp
22 | by_tactic (tac as Tactic.Check_Postcond' _) (ptp as (pt, p)) =
23 LI.by_tactic tac (get_istate_LI pt p, get_ctxt_LI pt p) ptp
24 | by_tactic (Tactic.Free_Solve') (pt, po as (p, _)) =
26 val p' = lev_dn_ (p, Res);
27 val pt = update_metID pt (par_pblobj pt p) MethodC.id_empty;
29 ("ok", ([(Tactic.Empty_Tac, Tactic.Empty_Tac_, (po, (Istate.Uistate, ContextC.empty)))], [], (pt,p')))
31 | by_tactic (Tactic.End_Proof'') ptp = ("end-proof", ([], [], ptp))
32 | by_tactic (Tactic.End_Detail' t) (pt, (p, p_)) = (* could be done by generate1 ?!? *)
33 let (*Rewrite_Set* done at Detail_Set*: this result is already in ctree*)
34 val pr = (lev_up p, Res)
36 ("ok", ([(Tactic.End_Detail, Tactic.End_Detail' t , ((p, p_), get_loc pt (p, p_)))], [], (pt, pr)))
38 | by_tactic m (pt, po as (p, p_)) =
39 if MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*29.8.02: could be detail, too !!*)
42 val ctxt = get_ctxt pt po
43 val ((p, p_), ps, _, pt) = Solve_Step.add_general m (Istate.empty, ctxt) (pt, (p, p_))
44 in ("no-method-specified", (*Free_Solve*)
45 ([(Tactic.Empty_Tac, Tactic.Empty_Tac_, ((p, p_), (Istate.Uistate, ctxt)))], ps, (pt, (p, p_))))
49 val thy' = get_obj g_domID pt (par_pblobj pt p);
50 val (is, sc) = LItool.resume_prog thy' (p,p_) pt;
52 case LI.locate_input_tactic sc (pt, po) (fst is) (snd is) m of
53 LI.Safe_Step (istate, ctxt, tac) =>
55 val p' = next_in_prog po
56 val (p'', _, _,pt') = Solve_Step.add_general tac (istate, ctxt) (pt, (p', p_))
58 ("ok", ([(Tactic.input_from_T tac, tac, (p'', (istate, ctxt)))],
59 [(*Ctree NOT cut*)], (pt', p'')))
61 | LI.Unsafe_Step (istate, ctxt, tac) =>
66 | _ => raise ERROR ("Step_Solve.by_tactic: call by " ^ pos'2str (p, p_));
67 val (p'', _, _,pt') = Solve_Step.add_general tac (istate, ctxt) (pt, (p', p_));
69 ("ok", ([(Tactic.input_from_T tac, tac, (p'', (istate, ctxt)))],
70 [(*Ctree NOT cut*)], (pt', p'')))
72 | _ => (* NotLocatable *)
74 val (p,ps, _, pt) = Solve_Step.add_hard (ThyC.get_theory "Isac_Knowledge") m (p, p_) pt;
76 ("not-found-in-program", ([(Tactic.input_from_T m, m, (po, is))], ps, (pt, p)))
80 val do_next = LI.do_next
84 Locate a step in a program, which has been determined by input of a term.
85 Special case: if the term is a CAS-command, then create a calchead, and do 1 step.
86 If "no derivation found" then Error_Pattern.check_for.
87 (Error_Pattern.check_for *within* compare_step seems too expensive)
89 (*fun by_term (next_cs as (_, _, (pt, pos as (p, _))): Calc.state_post) istr =*)
90 fun by_term (pt, pos as (p, _)) istr =
91 case TermC.parseNEW (get_ctxt pt pos) istr of
92 NONE => ("syntax error in '" ^ istr ^ "'", Calc.state_empty_post)
95 val pos_pred = lev_back(*'*) pos
96 val f_pred = Ctree.get_curr_formula (pt, pos_pred);
97 val f_succ = Ctree.get_curr_formula (pt, pos);
100 then ("same-formula", ([], [], (pt, pos))) (* ctree not cut with replaceFormula *)
102 case CAS_Cmd.input f_in of
103 SOME (pt, _) => ("ok", ([], [], (pt, (p, Pos.Met))))
105 case LI.locate_input_term (pt, pos) f_in of
106 LI.Found_Step cstate =>
107 ("ok" , ([], [], cstate (* already contains istate, ctxt *)))
108 | LI.Not_Derivable =>
110 val pp = Ctree.par_pblobj pt p
111 val (errpats, nrls, prog) = case MethodC.from_store (Ctree.get_obj Ctree.g_metID pt pp) of
112 {errpats, nrls, scr = Rule.Prog prog, ...} => (errpats, nrls, prog)
113 | _ => raise ERROR "inform: uncovered case of get_met"
114 val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
116 case Error_Pattern.check_for (f_pred, f_in) (prog, env) (errpats, nrls) of
117 SOME errpatID => ("error pattern #" ^ errpatID ^ "#", Calc.state_empty_post)
118 | NONE => ("no derivation found", Calc.state_empty_post)