lucin: unify fun.ids. for locate_input_tactic
1.1 --- a/src/Tools/isac/CalcElements/contextC.sml Thu Dec 19 16:53:52 2019 +0100
1.2 +++ b/src/Tools/isac/CalcElements/contextC.sml Thu Dec 19 17:37:25 2019 +0100
1.3 @@ -35,7 +35,7 @@
1.4 * Tactic.Apply_Method
1.5 * initialises ctxt (declare_constraints' + insert_assumptions pres) by init_pstate
1.6 * in solve for root problem
1.7 - * in begin_end_prog for subproblem
1.8 + * in by_tactic for subproblem
1.9 * Tactic.Rewrite* create assumptions; respective insert_assumptions is done by associate
1.10 * associate..Subproblem' returns ctxt ONLY with declare_constraints',
1.11 with insert_assumptions wait for Tactic.Apply_Method
1.12 @@ -49,7 +49,7 @@
1.13 * locate_input_formula: follows sig. of find_next_tactic
1.14 * changing from one method to another (in find_next_tactic only):
1.15 * from method to sub-program: just add new preconditions of the guard
1.16 - * locate_input_tactic: init_pstate by begin_end_prog
1.17 + * locate_input_tactic: init_pstate by by_tactic
1.18 * find_next_tactic:
1.19 * from_subpbl_to_caller
1.20 * finishing a method:
1.21 @@ -93,13 +93,13 @@
1.22 declare_constraints'
1.23
1.24 all_solve
1.25 - begin_end_prog (Tactic.Apply_Method'
1.26 + by_tactic (Tactic.Apply_Method'
1.27 init_pstate
1.28 declare_constraints'
1.29 insert_assumptions
1.30
1.31 nxt_specify_
1.32 - begin_end_prog (Tactic.Apply_Method'
1.33 + by_tactic (Tactic.Apply_Method'
1.34 init_pstate
1.35 declare_constraints'
1.36 insert_assumptions
1.37 @@ -132,7 +132,7 @@
1.38 compare_step
1.39 all_modspec
1.40 declare_constraints'
1.41 - begin_end_prog (Tactic.Apply_Method'
1.42 + by_tactic (Tactic.Apply_Method'
1.43 init_pstate
1.44 declare_constraints'
1.45 insert_assumptions
2.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Thu Dec 19 16:53:52 2019 +0100
2.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Thu Dec 19 17:37:25 2019 +0100
2.3 @@ -27,10 +27,10 @@
2.4 -> input_formula_result
2.5
2.6 (* must reside here:
2.7 - find_next_tactic calls do_solve_step and is called by begin_end_prog;
2.8 - begin_end_prog and do_solve_step are mutually recursive via begin_end_prog Apply_Method'
2.9 + find_next_tactic calls do_solve_step and is called by by_tactic;
2.10 + by_tactic and do_solve_step are mutually recursive via by_tactic Apply_Method'
2.11 *)
2.12 - val begin_end_prog: Tactic.T -> Istate.T * Proof.context -> Ctree.state -> Chead.calcstate'
2.13 + val by_tactic: Tactic.T -> Istate.T * Proof.context -> Ctree.state -> Chead.calcstate'
2.14 val do_solve_step: Ctree.state -> Chead.calcstate'
2.15
2.16 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
2.17 @@ -502,13 +502,13 @@
2.18 Found_Step of Ctree.state * Istate.T * Proof.context
2.19 | Not_Derivable of Chead.calcstate'
2.20
2.21 -(* FIXME.WN050821 compare fun solve ... fun begin_end_prog *)
2.22 -fun begin_end_prog (Tactic.Apply_Method' (mI, _, _, _)) (_, ctxt) (pt, pos as (p, _)) =
2.23 +(* FIXME.WN050821 compare fun solve ... fun by_tactic *)
2.24 +fun by_tactic (Tactic.Apply_Method' (mI, _, _, _)) (_, ctxt) (pt, pos as (p, _)) =
2.25 let
2.26 val {ppc, ...} = Specify.get_met mI;
2.27 val (itms, oris, probl) = case get_obj I pt p of
2.28 PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
2.29 - | _ => error "begin_end_prog Apply_Method': uncovered case get_obj"
2.30 + | _ => error "by_tactic Apply_Method': uncovered case get_obj"
2.31 val itms = if itms <> [] then itms else Chead.complete_metitms oris probl [] ppc
2.32 val thy' = get_obj g_domID pt p;
2.33 val thy = Celem.assoc_thy thy';
2.34 @@ -516,7 +516,7 @@
2.35 val itms = Specify.hack_until_review_Specify_1 mI itms
2.36 val (is, env, ctxt, scr) = case Lucin.init_pstate srls ctxt itms mI of
2.37 (is as Istate.Pstate {env, ...}, ctxt, scr) => (is, env, ctxt, scr)
2.38 - | _ => error "begin_end_prog Apply_Method': uncovered case init_pstate"
2.39 + | _ => error "by_tactic Apply_Method': uncovered case init_pstate"
2.40 val ini = Lucin.init_form thy scr env;
2.41 in
2.42 case ini of
2.43 @@ -536,12 +536,12 @@
2.44 Tactic.Apply_Method' (mI, NONE, Istate.e_istate, ctxt), (pos, (is, ctxt)))], c, ptp)
2.45 end
2.46 end
2.47 - | begin_end_prog (Tactic.Check_Postcond' (pI, (prog_res, _))) _ (pt, (p, p_)) =
2.48 + | by_tactic (Tactic.Check_Postcond' (pI, (prog_res, _))) _ (pt, (p, p_)) =
2.49 let
2.50 val pp = par_pblobj pt p
2.51 val thy = Celem.assoc_thy (get_obj g_domID pt pp);
2.52 val (pst, ctxt) = case get_loc pt (p, p_) of (Istate.Pstate pst, ctxt) => (pst, ctxt)
2.53 - | _ => error "begin_end_prog Check_Postcond': uncovered case get_loc"
2.54 + | _ => error "by_tactic Check_Postcond': uncovered case get_loc"
2.55 val asm = (case get_obj g_tac pt p of (*collects and instantiates asms*)
2.56 Tactic.Check_elementwise _ => (snd o (get_obj g_result pt)) p
2.57 | _ => get_assumptions_ pt (p, p_))
2.58 @@ -559,14 +559,14 @@
2.59
2.60 val (pst', ctxt') = case get_loc pt (pp, Frm) of
2.61 (Istate.Pstate pst', ctxt') => (pst', ctxt')
2.62 - | _ => error "begin_end_prog Check_Postcond' script of parpbl: uncovered case get_loc"
2.63 + | _ => error "by_tactic Check_Postcond' script of parpbl: uncovered case get_loc"
2.64 val ctxt'' = ContextC.from_subpbl_to_caller ctxt prog_res ctxt'
2.65 val is = Istate.Pstate (pst' |> Istate.set_act prog_res |> Istate.set_appy Istate.Skip_)
2.66 val ((p, p_), ps, _, pt) = Generate.generate1 thy tac (is, ctxt'') (pp, Res) pt;
2.67 in ([(Tactic.Check_Postcond pI, tac, ((pp, Res), (is, ctxt'')))], ps, (pt, (p, p_))) end
2.68 end
2.69 - | begin_end_prog (Tactic.End_Proof'') _ ptp = ([], [], ptp)
2.70 - | begin_end_prog tac_ is (pt, pos) =
2.71 + | by_tactic (Tactic.End_Proof'') _ ptp = ([], [], ptp)
2.72 + | by_tactic tac_ is (pt, pos) =
2.73 let
2.74 val pos = case pos of
2.75 (p, Met) => ((lev_on o lev_dn) p, Frm) (* begin program *)
2.76 @@ -576,7 +576,7 @@
2.77 in
2.78 ([(Tactic.input_from_T tac_, tac_, (pos, is))], c, (pt, pos'))
2.79 end
2.80 -(*find_next_tactic from program, begin_end_prog will update the ctree*)
2.81 +(*find_next_tactic from program, by_tactic will update the ctree*)
2.82 and do_solve_step (ptp as (pt, pos as (p, p_))) =
2.83 if Celem.e_metID = get_obj g_metID pt (par_pblobj pt p)
2.84 then ([], [], (pt, (p, p_)))
2.85 @@ -587,13 +587,13 @@
2.86 in
2.87 case find_next_tactic sc (pt, pos) ist ctxt of
2.88 Next_Step (ist, ctxt, tac) =>
2.89 - begin_end_prog tac (ist, Tactic.insert_assumptions tac ctxt) ptp
2.90 + by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp
2.91 | End_Program (ist, tac) =>
2.92 (case tac of
2.93 Tactic.End_Detail' res =>
2.94 ([(Tactic.End_Detail,
2.95 Tactic.End_Detail' res, (pos, (ist, ctxt)))], [], ptp)
2.96 - | _ => begin_end_prog tac (ist, ctxt) ptp)
2.97 + | _ => by_tactic tac (ist, ctxt) ptp)
2.98 | Helpless => Chead.e_calcstate'
2.99 end;
2.100
2.101 @@ -635,7 +635,7 @@
2.102 val ptp as (pt, (p,_)) = Chead.all_modspec ptp (*<--------------------*)
2.103 val mI = Ctree.get_obj Ctree.g_metID pt p
2.104 in
2.105 - begin_end_prog (Tactic.Apply_Method' (mI, NONE, Istate.e_istate, ContextC.e_ctxt)) (Istate.e_istate, ContextC.e_ctxt) ptp
2.106 + by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.e_istate, ContextC.e_ctxt)) (Istate.e_istate, ContextC.e_ctxt) ptp
2.107 end
2.108 | _ => cs';
2.109 in compare_step (tacis, c @ c' @ c'', ptp) ifo end
3.1 --- a/src/Tools/isac/Interpret/step-solve.sml Thu Dec 19 16:53:52 2019 +0100
3.2 +++ b/src/Tools/isac/Interpret/step-solve.sml Thu Dec 19 17:37:25 2019 +0100
3.3 @@ -1,11 +1,11 @@
3.4 -(* Title: Interpret/step-solve-2.sml
3.5 +(* Title: Interpret/step-by_tactic-2.sml
3.6 Author: Walther Neuper 2019
3.7 (c) due to copyright terms
3.8 *)
3.9
3.10 signature STEP_SOLVE =
3.11 sig
3.12 - val solve : Tactic.T -> Ctree.state -> string * Chead.calcstate'
3.13 + val by_tactic : Tactic.T -> Ctree.state -> string * Chead.calcstate'
3.14
3.15 end
3.16
3.17 @@ -16,20 +16,20 @@
3.18 open Ctree;
3.19 open Pos
3.20
3.21 -(*FIXME.WN050821 compare solve ... begin_end_prog:
3.22 - WN190811: solve ("Apply_Method",.. used by root-pbl + by locate_input_tactic !!!
3.23 +(*FIXME.WN050821 compare by_tactic ... by_tactic:
3.24 + WN190811: by_tactic ("Apply_Method",.. used by root-pbl + by locate_input_tactic !!!
3.25 *)
3.26 -fun solve (m as Tactic.Apply_Method' (mI, _, _, ctxt)) (pt, (pos as (p, _))) =
3.27 +fun by_tactic (m as Tactic.Apply_Method' (mI, _, _, ctxt)) (pt, (pos as (p, _))) =
3.28 let
3.29 val itms = case get_obj I pt p of
3.30 PblObj {meth=itms, ...} => itms
3.31 - | _ => error "solve Apply_Method: uncovered case get_obj"
3.32 + | _ => error "Step_Solve.by_tactic Apply_Method: uncovered case get_obj"
3.33 val thy' = get_obj g_domID pt p;
3.34 val thy = Celem.assoc_thy thy';
3.35 val srls = Lucin.get_simplifier (pt, pos)
3.36 val (is, env, ctxt, sc) = case Lucin.init_pstate srls ctxt itms mI of
3.37 (is as Istate.Pstate {env, ...}, ctxt, sc) => (is, env, ctxt, sc)
3.38 - | _ => error "solve Apply_Method: uncovered case init_pstate"
3.39 + | _ => error "Step_Solve.by_tactic Apply_Method: uncovered case init_pstate"
3.40 val ini = Lucin.init_form thy sc env;
3.41 val p = lev_dn p;
3.42 in
3.43 @@ -46,7 +46,7 @@
3.44 val (m', is', ctxt') =
3.45 case LucinNEW.find_next_tactic sc (pt, (p, Res)) is ctxt of
3.46 LucinNEW.Next_Step (ist, ctxt, tac) => (tac, ist, ctxt)
3.47 - | _ => raise ERROR ("solve Apply_Method " ^ strs2str' mI)
3.48 + | _ => raise ERROR ("Step_Solve.by_tactic Apply_Method " ^ strs2str' mI)
3.49 in
3.50 case LucinNEW.locate_input_tactic sc (pt, (p, Res)) is' ctxt' m' of
3.51 LucinNEW.Safe_Step (istate, ctxt, tac) =>
3.52 @@ -68,38 +68,38 @@
3.53 end
3.54 end
3.55 end
3.56 - | solve (Tactic.Free_Solve') (pt, po as (p, _)) =
3.57 + | by_tactic (Tactic.Free_Solve') (pt, po as (p, _)) =
3.58 let
3.59 val p' = lev_dn_ (p, Res);
3.60 val pt = update_metID pt (par_pblobj pt p) Celem.e_metID;
3.61 in
3.62 ("ok", ([(Tactic.Empty_Tac, Tactic.Empty_Tac_, (po, (Istate.Uistate, ContextC.e_ctxt)))], [], (pt,p')))
3.63 end
3.64 - | solve (Tactic.Check_Postcond' (pI, _)) (ptp as (pt, (p, p_))) =
3.65 + | by_tactic (Tactic.Check_Postcond' (pI, _)) (ptp as (pt, (p, p_))) =
3.66 let
3.67 val pp = par_pblobj pt p
3.68 val {scr, ...} = Specify.get_met (get_obj g_metID pt pp);
3.69 val (pst, ctxt) = case get_loc pt (p, p_) of (Istate.Pstate pst, ctxt) => (pst, ctxt)
3.70 - | _ => error "solve Check_Postcond: uncovered case get_loc"
3.71 + | _ => error "Step_Solve.by_tactic Check_Postcond: uncovered case get_loc"
3.72 val prog_res =
3.73 case LucinNEW.find_next_tactic scr (pt, (p, p_)) (Istate.Pstate pst) ctxt of
3.74 LucinNEW.Next_Step (_, _, Tactic.Check_elementwise' (_, _, (prog_res, _))) => prog_res
3.75 | LucinNEW.End_Program (_, Tactic.Check_Postcond' (_, (prog_res, _))) => prog_res
3.76 - | _ => raise ERROR ("solve Check_Postcond " ^ strs2str' pI)
3.77 + | _ => raise ERROR ("Step_Solve.by_tactic Check_Postcond " ^ strs2str' pI)
3.78 in (*for Applicable.applicable_in not yet available -----------vvvvv*)
3.79 - ("ok", LucinNEW.begin_end_prog (Tactic.Check_Postcond' (pI, (prog_res, [(*fill.later*)])))
3.80 + ("ok", LucinNEW.by_tactic (Tactic.Check_Postcond' (pI, (prog_res, [(*fill.later*)])))
3.81 (Istate.e_istate, ContextC.e_ctxt) ptp)
3.82 end
3.83 - | solve (Tactic.End_Proof'') (pt, (p, p_)) =
3.84 + | by_tactic (Tactic.End_Proof'') (pt, (p, p_)) =
3.85 ("end-proof", ([(Tactic.Empty_Tac, Tactic.Empty_Tac_, (([], Res), (Istate.Uistate, ContextC.e_ctxt)))], [], (pt, (p, p_))))
3.86 - | solve (Tactic.End_Detail' t) (pt, (p, p_)) = (* could be done by generate1 ?!? *)
3.87 + | by_tactic (Tactic.End_Detail' t) (pt, (p, p_)) = (* could be done by generate1 ?!? *)
3.88 let (*Rewrite_Set* done at Detail_Set*: this result is already in ctree*)
3.89 val pr = (lev_up p, Res)
3.90 in
3.91 ("ok", ([(Tactic.End_Detail, Tactic.End_Detail' t , ((p, p_), get_loc pt (p, p_)))], [], (pt, pr)))
3.92 end
3.93 - (* ======== general case as fall htrough ======== *)
3.94 - | solve m (pt, po as (p, p_)) =
3.95 + (* ======== general case as fall through ======== *)
3.96 + | by_tactic m (pt, po as (p, p_)) =
3.97 if Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*29.8.02: could be detail, too !!*)
3.98 then
3.99 let
3.100 @@ -120,7 +120,7 @@
3.101 val p' =
3.102 case p_ of Frm => p
3.103 | Res => lev_on p
3.104 - | _ => error ("solve: call by " ^ pos'2str (p, p_));
3.105 + | _ => error ("Step_Solve.by_tactic: call by " ^ pos'2str (p, p_));
3.106 val (p'', _, _,pt') =
3.107 Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") tac
3.108 (* DEL.^^^^^ ContextC.insert_assumptions asms' ctxt 2nd, fst in Lucin.associate *)
3.109 @@ -134,7 +134,7 @@
3.110 val p' =
3.111 case p_ of Frm => p
3.112 | Res => lev_on p
3.113 - | _ => error ("solve: call by " ^ pos'2str (p, p_));
3.114 + | _ => error ("Step_Solve.by_tactic: call by " ^ pos'2str (p, p_));
3.115 val (p'', _, _,pt') =
3.116 Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") tac
3.117 (* DEL.^^^^^ ContextC.insert_assumptions asms' ctxt 2nd, fst in Lucin.associate *)
4.1 --- a/src/Tools/isac/MathEngBasic/position.sml Thu Dec 19 16:53:52 2019 +0100
4.2 +++ b/src/Tools/isac/MathEngBasic/position.sml Thu Dec 19 17:37:25 2019 +0100
4.3 @@ -60,7 +60,7 @@
4.4 exceptions: Begin/End_Trans
4.5 # thus generate(1) called in
4.6 .# scan_dn1, locate_input_tactic
4.7 -.# begin_end_prog (tac_ -cases); general case:
4.8 +.# by_tactic (tac_ -cases); general case:
4.9 val pos' = case pos' of (p,Res) => (lev_on p',Res) | _ => pos'
4.10 # WN050220, S(604):
4.11 generate1...(Rewrite(f,..,res))..(pos, pos_)
5.1 --- a/src/Tools/isac/MathEngine/mathengine-stateless.sml Thu Dec 19 16:53:52 2019 +0100
5.2 +++ b/src/Tools/isac/MathEngine/mathengine-stateless.sml Thu Dec 19 17:37:25 2019 +0100
5.3 @@ -71,7 +71,7 @@
5.4 (* TODO push return-value cs' into solve and rename solve->loc_solve?_? *)
5.5 fun loc_solve_ m (pt, pos) =
5.6 let
5.7 - val (msg, cs') = Step_Solve.solve m (pt, pos);
5.8 + val (msg, cs') = Step_Solve.by_tactic m (pt, pos);
5.9 in
5.10 case msg of "ok" => Updated cs' | msg => ERror msg
5.11 end
5.12 @@ -83,26 +83,22 @@
5.13 (* locate a tactic in a program and apply it if possible;
5.14 report of tacs' applicability in tacis; pt is dropped in setNextTactic*)
5.15 fun locatetac _ (ptp as (_, ([], Pos.Res))) = ("end-of-calculation", ([], [], ptp))
5.16 - | locatetac tac (ptp as (pt, p)) =
5.17 - let
5.18 - val (mI, m) = Solve.mk_tac'_ tac;
5.19 - in
5.20 - case Applicable.applicable_in p pt m of
5.21 - Applicable.Notappl _ => ("not-applicable", ([],[], ptp): Chead.calcstate')
5.22 - | Applicable.Appl m =>
5.23 - let
5.24 - val x = if Tactic.for_specify' m
5.25 - then loc_specify_ m ptp else loc_solve_ m ptp
5.26 - in
5.27 - case x of
5.28 - ERror _ => ("failure", ([], [], ptp))
5.29 - (*FIXXXXXME: loc_specify_, loc_solve_ TOGETHER with dropping meOLD+detail.sml*)
5.30 - | UNsafe cs' => ("unsafe-ok", cs')
5.31 - | Updated (cs' as (_, _, (_, p'))) => (*ev.SEVER.tacs like Begin_Trans*)
5.32 - (if p' = ([], Pos.Res) then "end-of-calculation" else "ok", cs')
5.33 - (*for SEVER.tacs user to ask ? *)
5.34 - end
5.35 - end
5.36 + | locatetac m (ptp as (pt, p)) =
5.37 + case Applicable.applicable_in p pt m of
5.38 + Applicable.Notappl _ => ("not-applicable", ([],[], ptp): Chead.calcstate')
5.39 + | Applicable.Appl m =>
5.40 + let
5.41 + val x = if Tactic.for_specify' m
5.42 + then loc_specify_ m ptp else loc_solve_ m ptp
5.43 + in
5.44 + case x of
5.45 + ERror _ => ("failure", ([], [], ptp))
5.46 + (*FIXXXXXME: loc_specify_, loc_solve_ TOGETHER with dropping meOLD+detail.sml*)
5.47 + | UNsafe cs' => ("unsafe-ok", cs')
5.48 + | Updated (cs' as (_, _, (_, p'))) => (*ev.SEVER.tacs like Begin_Trans*)
5.49 + (if p' = ([], Pos.Res) then "end-of-calculation" else "ok", cs')
5.50 + (*for SEVER.tacs user to ask ? *)
5.51 + end
5.52
5.53 (* iterated by nxt_me; there (the resulting) ptp dropped
5.54 may call nxt_solve Apply_Method --- thus evaluated here after solve.sml *)
5.55 @@ -133,7 +129,7 @@
5.56 in
5.57 case tac of
5.58 Tactic.Apply_Method mI =>
5.59 - LucinNEW.begin_end_prog (Tactic.Apply_Method' (mI, NONE, Istate.e_istate, ContextC.e_ctxt)) ist_ctxt ptp
5.60 + LucinNEW.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.e_istate, ContextC.e_ctxt)) ist_ctxt ptp
5.61 | _ => Chead.nxt_specif tac ptp
5.62 end
5.63 end
6.1 --- a/src/Tools/isac/MathEngine/solve.sml Thu Dec 19 16:53:52 2019 +0100
6.2 +++ b/src/Tools/isac/MathEngine/solve.sml Thu Dec 19 17:37:25 2019 +0100
6.3 @@ -111,7 +111,7 @@
6.4 "Add_Given", "Del_Given", "Add_Find", "Del_Find", "Add_Relation", "Del_Relation",
6.5 "Specify_Theory", "Specify_Problem", "Specify_Method"];
6.6
6.7 -(*FIXME.WN050821 compare solve ... begin_end_prog:
6.8 +(*FIXME.WN050821 compare solve ... by_tactic:
6.9 WN190811: solve ("Apply_Method",.. used by root-pbl + by locate_input_tactic !!!
6.10 *)
6.11 (*-------------------------------------------------------------------
6.12 @@ -183,7 +183,7 @@
6.13 | LucinNEW.End_Program (_, Tactic.Check_Postcond' (_, (prog_res, _))) => prog_res
6.14 | _ => raise ERROR ("solve Check_Postcond " ^ strs2str' pI)
6.15 in (*for Applicable.applicable_in not yet available -----------vvvvv*)
6.16 - ("ok", LucinNEW.begin_end_prog (Tactic.Check_Postcond' (pI, (prog_res, [(*fill.later*)])))
6.17 + ("ok", LucinNEW.by_tactic (Tactic.Check_Postcond' (pI, (prog_res, [(*fill.later*)])))
6.18 (Istate.e_istate, ContextC.e_ctxt) ptp)
6.19 end
6.20 | solve (_, Tactic.End_Proof'') (pt, (p, p_)) =
6.21 @@ -302,7 +302,7 @@
6.22 let
6.23 val (_, _, mI) = get_obj g_spec pt p
6.24 val ctxt = get_ctxt pt pos
6.25 - val (_, c', ptp) = LucinNEW.begin_end_prog (Tactic.Apply_Method' (mI, NONE, Istate.e_istate, ctxt)) (Istate.e_istate, ctxt) ptp
6.26 + val (_, c', ptp) = LucinNEW.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.e_istate, ctxt)) (Istate.e_istate, ctxt) ptp
6.27 in
6.28 complete_solve auto (c @ c') ptp
6.29 end;
7.1 --- a/src/Tools/isac/Specify/calchead.sml Thu Dec 19 16:53:52 2019 +0100
7.2 +++ b/src/Tools/isac/Specify/calchead.sml Thu Dec 19 17:37:25 2019 +0100
7.3 @@ -1025,7 +1025,7 @@
7.4 (for ev. finding several more tacs due to hide) *)
7.5 (* FIXXXME: unify ... fun nxt_specif = nxt_spec + applicable_in + specify !! *)
7.6 (* WN.24.10.03 ~~~~~~~~~~~~~~ -> tac -> tac_ -> -"- as arg *)
7.7 -(* WN.24.10.03 fun begin_end_prog = ...................................?? *)
7.8 +(* WN.24.10.03 fun by_tactic = ...................................?? *)
7.9 fun nxt_specif (tac as Tactic.Model_Problem) (pt, pos as (p, _)) =
7.10 let
7.11 val (oris, ospec, probl, spec, ctxt) = case get_obj I pt p of
8.1 --- a/src/Tools/isac/TODO.thy Thu Dec 19 16:53:52 2019 +0100
8.2 +++ b/src/Tools/isac/TODO.thy Thu Dec 19 17:37:25 2019 +0100
8.3 @@ -94,7 +94,7 @@
8.4 inserts all data into Tactic.T available -- not all are at time of call!
8.5 \item Step_Solve.add <-- Generate.generate1
8.6 \item Step_Solve.by_tactic : Tactic.input -> Ctree.state -> ...
8.7 - ^^^^LucinNEW.begin_end_prog
8.8 + ^^^^LucinNEW.by_tactic
8.9 \item Step_Solve.by_formula : term -> Ctree.state -> ...
8.10 \item Step_Solve.find_next : Ctree.state -> ...
8.11 ^^^^LucinNEW.do_solve_step
8.12 @@ -121,7 +121,7 @@
8.13 \end{itemize}
8.14 \item xxx
8.15 \item xxx
8.16 - \item decompose do_solve_step, begin_end_prog: mutual recursion only avoids multiple generate1
8.17 + \item decompose do_solve_step, by_tactic: mutual recursion only avoids multiple generate1
8.18 ! ^^^ in find_next_tactic --- ? ? ? in locate_input_tactic ?
8.19 \item xxx
8.20 \item Generate.generate1 thy is redundant: is the same during pbl, thus lookup spec
8.21 @@ -353,11 +353,11 @@
8.22 \item xxx
8.23 \end{itemize}
8.24 \<close>
8.25 -subsection \<open>solve, loc_solve_, begin_end_prog, do_solve_step, ...\<close>
8.26 +subsection \<open>solve, loc_solve_, by_tactic, do_solve_step, ...\<close>
8.27 text \<open>
8.28 unify to calcstate, calcstate', ?Ctree.state?
8.29 \begin{itemize}
8.30 - \item begin_end_prog Check_Postcond' needs NO 2.find_next_tactic
8.31 + \item by_tactic Check_Postcond' needs NO 2.find_next_tactic
8.32 solve Check_Postcond' needs, because NO prog_result in Tactic.input
8.33 and applicable_in cannot get it.
8.34 \item xxx
9.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Thu Dec 19 16:53:52 2019 +0100
9.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Thu Dec 19 17:37:25 2019 +0100
9.3 @@ -197,7 +197,7 @@
9.4 (*val Updated (cs' as (_, _, (_, p'))) =*) loc_solve_ m ptp;
9.5 "~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = (m, ptp);
9.6
9.7 -"~~~~~ fun solve , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, pos));
9.8 +"~~~~~ fun Step_Solve.by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, pos));
9.9 (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p); (*else*)
9.10 val thy' = get_obj g_domID pt (par_pblobj pt p);
9.11 val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
10.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Thu Dec 19 16:53:52 2019 +0100
10.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Thu Dec 19 17:37:25 2019 +0100
10.3 @@ -41,7 +41,7 @@
10.4 member op = specsteps mI (*false*);
10.5 "~~~~~ fun loc_solve_ , args:"; val (m, (pt,pos)) = (m, ptp);
10.6
10.7 -"~~~~~ fun solve , args:"; val (m as Apply_Method' (mI, _, _, ctxt), (pt, (pos as (p,_))))
10.8 +"~~~~~ fun Step_Solve.by_tactic , args:"; val (m as Apply_Method' (mI, _, _, ctxt), (pt, (pos as (p,_))))
10.9 = (m, (pt, pos));
10.10 val {srls, ...} = get_met mI;
10.11 val itms = case get_obj I pt p of
10.12 @@ -116,8 +116,8 @@
10.13 (** )val (***)xxxxx(***) ( *Updated (cs' as (_, _, (_, p'))) =( **) loc_solve_ m ptp;
10.14 "~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = (m, ptp);
10.15
10.16 - (** )val (***)xxxxx_x(***) ( *(msg, cs') =( **) Step_Solve.solve m (pt, pos);
10.17 -"~~~~~ fun solve , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, pos));
10.18 + (** )val (***)xxxxx_x(***) ( *(msg, cs') =( **) Step_Solve.by_tactic m (pt, pos);
10.19 +"~~~~~ fun Step_Solve.by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, pos));
10.20 (*+*)val (pt'''''_', (p'''''_', p_'''''_')) = (pt, (p, p_));
10.21 (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p); (*else*)
10.22 val thy' = get_obj g_domID pt (par_pblobj pt p);
10.23 @@ -165,10 +165,10 @@
10.24 (*if*) LibraryC.assoc (*then*);
10.25
10.26 Safe_Step (Istate.Pstate ist, ctxt, tac') (*return value*);
10.27 -"~~~~~ from locate_input_tactic to fun solve return:"; val Safe_Step (istate, ctxt, tac)
10.28 +"~~~~~ from locate_input_tactic to fun Step_Solve.by_tactic return:"; val Safe_Step (istate, ctxt, tac)
10.29 = (*xxxxx_xx*)(**)Safe_Step (Istate.Pstate ist, ctxt, tac')(**);
10.30
10.31 -(*+*)val (pt, po as (p, p_)) = (pt'''''_', (p'''''_', p_'''''_')); (* from begin of solve *)
10.32 +(*+*)val (pt, po as (p, p_)) = (pt'''''_', (p'''''_', p_'''''_')); (* from begin of by_tactic *)
10.33 val (p'', _, _,pt') =
10.34 Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") tac
10.35 (* DEL.^^^^^ ContextC.insert_assumptions asms' ctxt 2nd, fst in Lucin.associate *)
10.36 @@ -177,7 +177,7 @@
10.37
10.38 ("ok", ([(Tactic.input_from_T tac, tac, (p'', (istate, ctxt)))],
10.39 [(*ctree NOT cut*)], (pt', p''))) (*return value*);
10.40 -"~~~~~ from solve to loc_solve_ return:"; val ((msg, cs' : calcstate'))
10.41 +"~~~~~ from Step_Solve.by_tactic to loc_solve_ return:"; val ((msg, cs' : calcstate'))
10.42 = ("ok", ([(Tactic.input_from_T tac, tac, (p'', (istate, ctxt)) )], [(*ctree NOT cut*)], (pt', p'')));
10.43
10.44 "~~~~~ from loc_solve_ to locatetac return:"; val (Updated (cs' as (_, _, (_, p'))))
10.45 @@ -279,9 +279,9 @@
10.46
10.47 loc_solve_ m ptp;
10.48 "~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = (m, ptp);
10.49 - solve m (pt, pos);
10.50 + Step_Solve.by_tactic m (pt, pos);
10.51 (* ======== general case ======== *)
10.52 -"~~~~~ fun solve , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, pos));
10.53 +"~~~~~ fun Step_Solve.by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, pos));
10.54 (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
10.55 val thy' = get_obj g_domID pt (par_pblobj pt p);
10.56 val (_, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
10.57 @@ -411,16 +411,13 @@
10.58 (*NEW* ) case find_next_tactic sc (pt, pos) ist ctxt of
10.59 (*NEW*) Next_Step (ist, ctxt, tac) =>
10.60 ( *NEW*)
10.61 - begin_end_prog tac (ist, Tactic.insert_assumptions tac ctxt) ptp;
10.62 -(*NEW* ) | End_Program (ist, tac) => begin_end_prog tac (ist, ctxt) ptp
10.63 + LucinNEW.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp;
10.64 +(*NEW* ) | End_Program (ist, tac) => LucinNEW.by_tactic tac (ist, ctxt) ptp
10.65 (*NEW*) | Helpless => Chead.e_calcstate'
10.66 ( *NEW*)
10.67
10.68 (*+*)val Rewrite_Set' ("Test", false, Rls {id = "Test_simplify", ...}, _, _) = tac;
10.69
10.70 -(*OLD skip* ) val _ = (*case*) tac_'''''_' (*of*);
10.71 -(*OLD skip*)begin_end_prog tac_'''''_' is'''''_' ptp'''''_' (*return value*);
10.72 -( *OLD*)
10.73 "~~~~~ fun begin_end_prog , args:"; val (tac_, is, (pt, pos))
10.74 (*skip* )= (tac_'''''_', is, ptp);( *skip*)
10.75 (*use*) = (tac, (ist, Tactic.insert_assumptions tac ctxt), ptp) (*use*)
10.76 @@ -432,8 +429,6 @@
10.77
10.78 ([(Tactic.input_from_T tac_, tac_, (pos, is))], c, (pt, pos')) (*return from do_solve_step*);
10.79 "~~~~~ from and do_solve_step\<longrightarrow>fun step , return:";
10.80 -(*OLD skip* )val (tac_'''''_')
10.81 -(*OLD skip*) = (begin_end_prog tac_'''''_' is ptp);( **)
10.82 (*use*)val cs =
10.83 (*use*)([(Tactic.input_from_T tac_, tac_, (pos, is))], c, (pt, pos'));
10.84 (*use*)
11.1 --- a/test/Tools/isac/Interpret/script.sml Thu Dec 19 16:53:52 2019 +0100
11.2 +++ b/test/Tools/isac/Interpret/script.sml Thu Dec 19 17:37:25 2019 +0100
11.3 @@ -68,11 +68,11 @@
11.4 (mI,m); (*string * tac*)
11.5 ptp (*ctree * pos'*);
11.6 "~~~~~ fun loc_solve_, args:"; val (m ,(pt,pos)) = (m, ptp);
11.7 -(*val (msg, cs') = solve m (pt, pos);
11.8 +(*val (msg, cs') = Step_Solve.by_tactic m (pt, pos);
11.9 (*Argument: m : string * tac Reason: Can't unify tac_ with tac (Different type constructors)*)*)
11.10 m;
11.11 (pt, pos);
11.12 -"~~~~~ fun solve, args:"; val (m, (pt, po as (p,p_))) = (m, (pt, pos));
11.13 +"~~~~~ fun Step_Solve.by_tactic , args:"; val (m, (pt, po as (p,p_))) = (m, (pt, pos));
11.14 (*solve has still p_!!!!!!!!!!!!!!!!!!!!!!!!!*)
11.15
11.16 e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)
11.17 @@ -112,7 +112,8 @@
11.18 val Appl m = applicable_in p pt m;
11.19 member op = specsteps mI; (*false*)
11.20 "~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = (m, ptp);
11.21 -"~~~~~ fun solve , args:"; val (Apply_Method' (mI,_,_,ctxt), pos as (p,_)) = (m, pos);
11.22 +"~~~~~ fun Step_Solve.by_tactic , args:"; val (Apply_Method' (mI,_,_,ctxt), pos as (p,_))
11.23 + = (m, pos);
11.24 val {srls, ...} = get_met mI;
11.25 val PblObj {meth=itms, ...} = get_obj I pt p;
11.26 val thy' = get_obj g_domID pt p;
12.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
12.2 +++ b/test/Tools/isac/Interpret/step-solve.sml Thu Dec 19 17:37:25 2019 +0100
12.3 @@ -0,0 +1,17 @@
12.4 +(* Title: "Interpret/step-solve.sml"
12.5 + Author: Walther Neuper
12.6 + (c) due to copyright terms
12.7 +*)
12.8 +
12.9 +"-----------------------------------------------------------------------------------------------";
12.10 +"table of contents -----------------------------------------------------------------------------";
12.11 +"-----------------------------------------------------------------------------------------------";
12.12 +"-----------------------------------------------------------------------------------------------";
12.13 +"----------- TODO ------------------------------------------------------------------------------";
12.14 +"-----------------------------------------------------------------------------------------------";
12.15 +"-----------------------------------------------------------------------------------------------";
12.16 +"-----------------------------------------------------------------------------------------------";
12.17 +
12.18 +"----------- TODO ------------------------------------------------------------------------------";
12.19 +"----------- TODO ------------------------------------------------------------------------------";
12.20 +"----------- TODO ------------------------------------------------------------------------------";
13.1 --- a/test/Tools/isac/Knowledge/biegelinie-4.sml Thu Dec 19 16:53:52 2019 +0100
13.2 +++ b/test/Tools/isac/Knowledge/biegelinie-4.sml Thu Dec 19 17:37:25 2019 +0100
13.3 @@ -150,19 +150,19 @@
13.4 loc_solve_ (mI,m) ptp;
13.5 "~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = (m, ptp);
13.6
13.7 -Solve.solve m (pt, pos);
13.8 -"~~~~~ fun solve , args:"; val (m as Tactic.Apply_Method' (mI, _, _, ctxt)), (pt, (pos as (p, _)))) =
13.9 - (m, (pt, pos));
13.10 + Step_Solve.by_tactic m (pt, pos);
13.11 +"~~~~~ fun Step_Solve.by_tactic , args:"; val (m as Tactic.Apply_Method' (mI, _, _, ctxt)), (pt, (pos as (p, _))))
13.12 + = (m, (pt, pos));
13.13 val {srls, ...} = Specify.get_met mI;
13.14 val itms = case get_obj I pt p of
13.15 PblObj {meth=itms, ...} => itms
13.16 - | _ => error "solve Apply_Method: uncovered case get_obj"
13.17 + | _ => error "Step_Solve.by_tactic Apply_Method: uncovered case get_obj"
13.18 val thy' = get_obj g_domID pt p;
13.19 val thy = Celem.assoc_thy thy';
13.20 val srls = Lucin.get_simplifier (pt, pos)
13.21 val (is, env, ctxt, sc) = case Lucin.init_pstate srls ctxt itms mI of
13.22 (is as Istate.Pstate ist, ctxt, sc) => (is, get_env ist, ctxt, sc)
13.23 - | _ => error "solve Apply_Method: uncovered case init_pstate"
13.24 + | _ => error "Step_Solve.by_tactic Apply_Method: uncovered case init_pstate"
13.25 val ini = Lucin.init_form thy sc env;
13.26 val p = lev_dn p;
13.27 val NONE = (*case*) ini (*of*);
14.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Thu Dec 19 16:53:52 2019 +0100
14.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Thu Dec 19 17:37:25 2019 +0100
14.3 @@ -203,7 +203,7 @@
14.4 "~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = (m, ptp);
14.5 (*solve m (pt, pos);
14.6 WAS: not-found-in-script: NotLocatable from Term_Val1 (Const ("List...*)
14.7 -"~~~~~ fun solve, args:"; val (m, (pt, po as (p,p_))) = (m, (pt, pos));
14.8 +"~~~~~ fun Step_Solve.by_tactic , args:"; val (m, (pt, po as (p,p_))) = (m, (pt, pos));
14.9 e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*);
14.10 val thy' = get_obj g_domID pt (par_pblobj pt p);
14.11 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
15.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Thu Dec 19 16:53:52 2019 +0100
15.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Thu Dec 19 17:37:25 2019 +0100
15.3 @@ -287,7 +287,7 @@
15.4 (auto, c, ptp);
15.5 val (_,_,mI) = get_obj g_spec pt p
15.6 val ctxt = get_ctxt pt pos
15.7 - val (ttt, c', ptp) = begin_end_prog (Apply_Method' (mI, NONE, e_istate, ctxt)) (e_istate, ctxt) ptp;
15.8 + val (ttt, c', ptp) = LucinNEW.by_tactic (Apply_Method' (mI, NONE, e_istate, ctxt)) (e_istate, ctxt) ptp;
15.9 (* complete_solve auto (c @ c') ptp; (*WAS Type unification failed...*) pos = ([], Met)*)
15.10 "~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)))) =
15.11 (auto, (c @ c'), ptp);
16.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Thu Dec 19 16:53:52 2019 +0100
16.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Thu Dec 19 17:37:25 2019 +0100
16.3 @@ -51,7 +51,7 @@
16.4 val Appl m = applicable_in p pt m; (*m = Apply_Method'..*)
16.5 member op = specsteps mI; (*false*)
16.6 "~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos) ) = (m, ptp);
16.7 -"~~~~~ fun solve , args:"; val (Apply_Method' (mI,_,_,_), pos as (p,_)) = (m, pos);
16.8 +"~~~~~ fun Step_Solve.by_tactic , args:"; val (Apply_Method' (mI,_,_,_), pos as (p,_)) = (m, pos);
16.9 val PblObj {meth, ctxt, ...} = get_obj I pt p;
16.10 val thy' = get_obj g_domID pt p;
16.11 val thy = assoc_thy thy';
16.12 @@ -99,7 +99,7 @@
16.13 val pres = Stool.check_preconds (Proof_Context.theory_of ctxt) prls pre itms |> map snd;
16.14 val ctxt = ctxt |> ContextC.insert_assumptions pres;
16.15
16.16 -"~~~~~ continue solve";
16.17 +"~~~~~ continue Step_Solve.by_tactic";
16.18 val ini = init_form thy sc'''' env'''';
16.19 val p = lev_dn p;
16.20 val SOME t = ini;
17.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Thu Dec 19 16:53:52 2019 +0100
17.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Thu Dec 19 17:37:25 2019 +0100
17.3 @@ -41,9 +41,9 @@
17.4
17.5 loc_solve_ m ptp ; (* scan_dn1: call by ([3], Pbl)*)
17.6 "~~~~~ fun loc_solve_, args:"; val (m, (pt, pos)) = (m, ptp);
17.7 - solve m (pt, pos); (* scan_dn1: call by ([3], Pbl)*)
17.8 + Step_Solve.by_tactic m (pt, pos); (* scan_dn1: call by ([3], Pbl)*)
17.9 (* ======== general tactic as fall through ======== *)
17.10 -"~~~~~ fun solve , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, pos));
17.11 +"~~~~~ fun Step_Solve.by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, pos));
17.12 (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (* = else*);
17.13 val thy' = get_obj g_domID pt (par_pblobj pt p);
17.14 val (_, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
18.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml Thu Dec 19 16:53:52 2019 +0100
18.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml Thu Dec 19 17:37:25 2019 +0100
18.3 @@ -47,7 +47,7 @@
18.4
18.5 val Apply_Method mI = (*case*) tac (*of*);
18.6 (*+*)val (_, _, (pt'''', p'''')) =
18.7 - begin_end_prog (Tactic.Apply_Method' (mI, NONE, Istate.e_istate, ContextC.e_ctxt)) ist_ctxt ptp;
18.8 + LucinNEW.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.e_istate, ContextC.e_ctxt)) ist_ctxt ptp;
18.9 "~~~~~ fun begin_end_prog , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (ist, ctxt), (pt, pos as (p, _)))
18.10 = ((Tactic.Apply_Method' (mI, NONE, Istate.e_istate, ContextC.e_ctxt)), ist_ctxt, ptp);
18.11 val {ppc, ...} = Specify.get_met mI;
19.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Thu Dec 19 16:53:52 2019 +0100
19.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Thu Dec 19 17:37:25 2019 +0100
19.3 @@ -31,8 +31,9 @@
19.4 member op = specsteps mI; (*false*)
19.5 (*val Updated (cs' as (_,_,(_,p'))) = loc_solve_ (mI,m) ptp;*)
19.6 "~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = (m, ptp);
19.7 -(*val (msg, cs') = solve m (pt, pos);*)
19.8 -"~~~~~ fun solve , args:"; val (m, (pt, po as (p,p_))) = (m, (pt, pos));
19.9 +(*val (msg, cs') =*)
19.10 + Step_Solve.by_tactic m (pt, pos);
19.11 +"~~~~~ fun Step_Solve.by_tactic , args:"; val (m, (pt, po as (p,p_))) = (m, (pt, pos));
19.12 e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*);
19.13 val thy' = get_obj g_domID pt (par_pblobj pt p);
19.14 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
20.1 --- a/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Thu Dec 19 16:53:52 2019 +0100
20.2 +++ b/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Thu Dec 19 17:37:25 2019 +0100
20.3 @@ -47,24 +47,24 @@
20.4 loc_solve_ m ptp;
20.5 "~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos) ) = (m, ptp);
20.6
20.7 - solve m (pt, pos);
20.8 -"~~~~~ fun solve , args:"; val (m as Tactic.Apply_Method' (mI, _, _, ctxt), (pt, (pos as (p, _))))
20.9 + Step_Solve.by_tactic m (pt, pos);
20.10 +"~~~~~ fun Step_Solve.by_tactic , args:"; val (m as Tactic.Apply_Method' (mI, _, _, ctxt), (pt, (pos as (p, _))))
20.11 = (m, (pt, pos));
20.12 val itms = case get_obj I pt p of
20.13 PblObj {meth=itms, ...} => itms
20.14 - | _ => error "solve Apply_Method: uncovered case get_obj"
20.15 + | _ => error "Step_Solve.by_tactic Apply_Method: uncovered case get_obj"
20.16 val thy' = get_obj g_domID pt p;
20.17 val thy = Celem.assoc_thy thy';
20.18 val srls = Lucin.get_simplifier (pt, pos)
20.19 val (is, env, ctxt, sc) = case Lucin.init_pstate srls ctxt itms mI of
20.20 (is as Istate.Pstate {env, ...}, ctxt, sc) => (is, env, ctxt, sc)
20.21 - | _ => error "solve Apply_Method: uncovered case init_pstate"
20.22 + | _ => error "Step_Solve.by_tactic Apply_Method: uncovered case init_pstate"
20.23
20.24 (*+*)val (pt, p) = case locatetac tac (pt, pos) of
20.25 ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
20.26 (*+*)val SOME t = parseNEW (get_ctxt pt p) "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
20.27
20.28 -"~~~~~ from solve to..to me return"; val (pt, p) = (pt'''', p'''');
20.29 +"~~~~~ from Step_Solve.by_tactic to..to me return"; val (pt, p) = (pt'''', p'''');
20.30
20.31 val ("ok", ([(Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv"), _, (_, (Pstate _, _)))], _, _)) = (*case*)
20.32 step p ((pt, e_pos'), []) (*of*);
21.1 --- a/test/Tools/isac/Test_Isac_Short.thy Thu Dec 19 16:53:52 2019 +0100
21.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Thu Dec 19 17:37:25 2019 +0100
21.3 @@ -210,9 +210,10 @@
21.4 ML_file "Interpret/script.sml"
21.5 ML_file "Interpret/inform.sml"
21.6 ML_file "Interpret/lucas-interpreter.sml"
21.7 + ML_file "Interpret/step-solve.sml"
21.8 +
21.9 ML_file "MathEngine/solve.sml"
21.10 ML_file "MathEngine/mathengine-stateless.sml" (*!part. WN130804: +check Interpret/me.sml*)
21.11 -
21.12 ML_file "MathEngine/messages.sml"
21.13 ML_file "MathEngine/states.sml"
21.14
22.1 --- a/test/Tools/isac/Test_Some.thy Thu Dec 19 16:53:52 2019 +0100
22.2 +++ b/test/Tools/isac/Test_Some.thy Thu Dec 19 17:37:25 2019 +0100
22.3 @@ -220,9 +220,9 @@
22.4 \<close> ML \<open>
22.5 "~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = ((mI, m), ptp);
22.6 \<close> ML \<open>
22.7 - Solve.solve m (pt, pos);
22.8 + Step_Solve.by_tactic m (pt, pos);
22.9 \<close> ML \<open>
22.10 -"~~~~~ fun solve , args:"; val (Tactic.Check_Postcond' (pI, _)), (pt, (p, p_)))
22.11 +"~~~~~ fun Step_Solve.by_tactic , args:"; val (Tactic.Check_Postcond' (pI, _)), (pt, (p, p_)))
22.12 = (m, (pt, pos));
22.13 \<close> ML \<open>
22.14 \<close> ML \<open>