1.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml Tue Feb 11 10:59:18 2020 +0100
1.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml Tue Feb 11 11:58:45 2020 +0100
1.3 @@ -125,14 +125,14 @@
1.4 val ((pt, _), _) = get_calc cI (* retrieve calcstate from states *)
1.5 val ip = get_pos cI 1 (* retrieve position from states *)
1.6 in
1.7 - case Math_Engine.locatetac tac (pt, ip) of
1.8 + case Step.by_tactic tac (pt, ip) of
1.9 ("ok", (tacis, _, _)) => (* update calcstate in states *)
1.10 (upd_calc cI ((pt, ip), tacis); setnexttactic2xml cI "ok")
1.11 | ("unsafe-ok", (tacis, _, _)) =>
1.12 (upd_calc cI ((pt, ip), tacis); setnexttactic2xml cI "unsafe-ok")
1.13 | ("not-applicable", _) => setnexttactic2xml cI "not-applicable"
1.14 | ("end-of-calculation", _) => setnexttactic2xml cI "end-of-calculation"
1.15 - | (msg, _) => sysERROR2xml cI ("setNextTactic: locatetac returns " ^ msg)
1.16 + | (msg, _) => sysERROR2xml cI ("setNextTactic: Step.by_tactic returns " ^ msg)
1.17 end;
1.18
1.19 (*. apply a tactic at a position and update the calc-tree if applicable .*)
1.20 @@ -142,7 +142,7 @@
1.21 val ((pt, _), _) = get_calc cI
1.22 val p = get_pos cI 1
1.23 in
1.24 - case Math_Engine.locatetac tac (pt, ip) of
1.25 + case Step.by_tactic tac (pt, ip) of
1.26 ("ok", (_, c, ptp as (_, p'))) =>
1.27 (upd_calc cI (ptp, []);
1.28 upd_ipos cI 1 p';
1.29 @@ -155,7 +155,7 @@
1.30 (upd_calc cI (ptp, []);
1.31 upd_ipos cI 1 p';
1.32 autocalculateOK2xml cI p (if null c then p' else last_elem c) p')
1.33 - | (str, _) => autocalculateERROR2xml cI ("applyTactic: locatetac returns " ^ str)
1.34 + | (str, _) => autocalculateERROR2xml cI ("applyTactic: Step.by_tactic returns " ^ str)
1.35 end;
1.36
1.37 fun fetchProposedTactic cI =
1.38 @@ -334,7 +334,7 @@
1.39 val subs = Rtools.subs_from is "dummy" guh
1.40 val tac = Rtools.guh2rewtac guh subs
1.41 in
1.42 - case Math_Engine.locatetac tac (pt, ip) of (*='fun setNextTactic'+step*)
1.43 + case Step.by_tactic tac (pt, ip) of (*='fun setNextTactic'+step*)
1.44 ("ok", (tacis, c, ptp as (_, p))) =>
1.45 (upd_calc cI ((pt, p), []);
1.46 autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)
1.47 @@ -701,7 +701,7 @@
1.48 ("ok", tac) =>
1.49 let
1.50 in (* cp from applyTactic *)
1.51 - case Math_Engine.locatetac tac (pt, pos) of
1.52 + case Step.by_tactic tac (pt, pos) of
1.53 ("ok", (_, c, ptp as (_,p'))) =>
1.54 (upd_calc cI (ptp, []);
1.55 upd_ipos cI 1 p';
2.1 --- a/src/Tools/isac/MathEngine/mathengine-stateless.sml Tue Feb 11 10:59:18 2020 +0100
2.2 +++ b/src/Tools/isac/MathEngine/mathengine-stateless.sml Tue Feb 11 11:58:45 2020 +0100
2.3 @@ -12,8 +12,6 @@
2.4 Ctree.pos' * NEW * Generate.mout * Tactic.input * Telem.safe * Ctree.ctree
2.5 val autocalc : Ctree.pos' list -> Ctree.pos' -> (Calc.T) * Generate.taci list ->
2.6 Solve.auto -> string * Ctree.pos' list * (Calc.T)
2.7 - val locatetac :
2.8 - Tactic.input -> Calc.T -> string * (Generate.taci list * Ctree.pos' list * (Calc.T))
2.9 val detailstep : Ctree.ctree -> Ctree.pos' -> string * Ctree.ctree * Ctree.pos'
2.10
2.11 val initcontext_met : Ctree.ctree -> Ctree.pos' -> bool * string list * Program.T * Model.itm list * (bool * term) list
2.12 @@ -29,9 +27,6 @@
2.13 val f2str : Generate.mout -> Rule.cterm'
2.14 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
2.15 type nxt_
2.16 - datatype lOc_ = ERror of string | UNsafe of Chead.calcstate' | Updated of Chead.calcstate'
2.17 - val loc_solve_ : Tactic.T -> Ctree.ctree * Ctree.pos' -> lOc_
2.18 - val loc_specify_ : Tactic.T -> Calc.T -> lOc_
2.19 val TESTg_form : Calc.T -> Generate.mout
2.20 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
2.21
2.22 @@ -44,49 +39,10 @@
2.23 struct
2.24 (**)
2.25
2.26 -datatype lOc_ =
2.27 - ERror of string (*after loc_specify, loc_solve*)
2.28 -| UNsafe of Chead.calcstate' (*after loc_specify, loc_solve*)
2.29 -| Updated of Chead.calcstate' (*after loc_specify, loc_solve*)
2.30 -
2.31 -fun loc_specify_ m (pt, pos) =
2.32 - let
2.33 - val (p, _, f, _, _, pt) = Chead.specify m pos [] pt;
2.34 - in
2.35 - case f of (Generate.Error' e) => ERror e | _ => Updated ([], [], (pt,p))
2.36 - end
2.37 -
2.38 -fun loc_solve_ m (pt, pos) =
2.39 - let
2.40 - val (msg, cs') = Step_Solve.by_tactic m (pt, pos);
2.41 - in
2.42 - case msg of "ok" => Updated cs' | msg => ERror msg
2.43 - end
2.44 -
2.45 datatype nxt_ =
2.46 HElpless (**)
2.47 | Nexts of Chead.calcstate (**)
2.48
2.49 -(* locate a tactic in a program and apply it if possible;
2.50 - report of tacs' applicability in tacis; pt is dropped in setNextTactic*)
2.51 -fun locatetac _ (ptp as (_, ([], Pos.Res))) = ("end-of-calculation", ([], [], ptp))
2.52 - | locatetac m (ptp as (pt, p)) =
2.53 - case Applicable.applicable_in p pt m of
2.54 - Applicable.Notappl _ => ("not-applicable", ([],[], ptp): Chead.calcstate')
2.55 - | Applicable.Appl m =>
2.56 - let
2.57 - val x = if Tactic.for_specify' m
2.58 - then loc_specify_ m ptp else loc_solve_ m ptp
2.59 - in
2.60 - case x of
2.61 - ERror _ => ("failure", ([], [], ptp))
2.62 - (*FIXXXXXME: loc_specify_, loc_solve_ TOGETHER with dropping meOLD+detail.sml*)
2.63 - | UNsafe cs' => ("unsafe-ok", cs')
2.64 - | Updated (cs' as (_, _, (_, p'))) => (*ev.SEVER.tacs like Begin_Trans*)
2.65 - (if p' = ([], Pos.Res) then "end-of-calculation" else "ok", cs')
2.66 - (*for SEVER.tacs user to ask ? *)
2.67 - end
2.68 -
2.69 (* specify a new method; WN0512 impl.incomplete, see 'nxt_specif (Specify_Method ' *)
2.70 fun set_method mI ptp =
2.71 let
2.72 @@ -310,21 +266,21 @@
2.73 internal view: loc_specify/solve, nxt_specify/solve used
2.74 i.e. same as in setnexttactic / nextTac*)
2.75 (*ENDE TESTPHASE 08/10.03:
2.76 - NEW loeschen, eigene Version von locatetac, do_next
2.77 + NEW loeschen, eigene Version von Step.by_tactic, do_next
2.78 meNEW, CalcTreeTEST: tac'_ -replace-> tac, remove [](cid) *)
2.79
2.80 fun me (*(Empty_Tac) p _ _ = raise ERROR ("me: Empty_Tac at " ^ pos'2str p)
2.81 | me*) tac p _(*NEW remove*) pt =
2.82 let
2.83 val (pt, p) =
2.84 - (*locatetac is here for testing by me; do_next would suffice in me*)
2.85 - case locatetac tac (pt, p) of
2.86 + (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
2.87 + case Step.by_tactic tac (pt, p) of
2.88 ("ok", (_, _, ptp)) => ptp
2.89 | ("unsafe-ok", (_, _, ptp)) => ptp
2.90 | ("not-applicable",_) => (pt, p)
2.91 | ("end-of-calculation", (_, _, ptp)) => ptp
2.92 | ("failure", _) => error "sys-error"
2.93 - | _ => error "me: uncovered case locatetac"
2.94 + | _ => error "me: uncovered case Step.by_tactic"
2.95 val (_, ts) =
2.96 (*step's correct ctree is not tested in me, but in autocalc*)
2.97 (case Step.do_next p ((pt, Pos.e_pos'), []) of
2.98 @@ -338,7 +294,7 @@
2.99 tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
2.100 | _ => if p = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
2.101 in
2.102 - (p, [] : NEW, TESTg_form (pt, p) (* form output comes from locatetac *),
2.103 + (p, [] : NEW, TESTg_form (pt, p) (* form output comes from Step.by_tactic *),
2.104 tac, Telem.Sundef, pt)
2.105 end
2.106
3.1 --- a/src/Tools/isac/MathEngine/step.sml Tue Feb 11 10:59:18 2020 +0100
3.2 +++ b/src/Tools/isac/MathEngine/step.sml Tue Feb 11 11:58:45 2020 +0100
3.3 @@ -13,7 +13,8 @@
3.4 *)
3.5 signature STEP =
3.6 sig
3.7 - val (*see TODO below*) do_next: Ctree.pos' -> Chead.calcstate -> string * Chead.calcstate'
3.8 + val do_next: Ctree.pos' -> Chead.calcstate -> string * Chead.calcstate'
3.9 + val by_tactic: Tactic.input -> Calc.T -> string * Chead.calcstate'
3.10 (*
3.11 val by_tactic = Step_Solve.by_tactic
3.12 = Step_Specify.by_tactic ? depending on PIDE, see TODO.thy
3.13 @@ -26,6 +27,10 @@
3.14 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
3.15 val specify_do_next: Calc.T -> string * Chead.calcstate'
3.16 val switch_specify_solve: Pos.pos_ -> Calc.T -> string * Chead.calcstate'
3.17 +
3.18 + datatype lOc_ = ERror of string | UNsafe of Chead.calcstate' | Updated of Chead.calcstate'
3.19 + val loc_solve_ : Tactic.T -> Calc.T -> lOc_
3.20 + val loc_specify_ : Tactic.T -> Calc.T -> lOc_
3.21 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
3.22 end
3.23
3.24 @@ -34,6 +39,8 @@
3.25 struct
3.26 (**)
3.27
3.28 +(** do a next step **)
3.29 +
3.30 fun specify_do_next (ptp as (pt, (p, p_))) =
3.31 let
3.32 val (_, (p_', tac)) = SpecifyNEW.find_next_step ptp
3.33 @@ -76,8 +83,45 @@
3.34 switch_specify_solve p_ (pt, ip)
3.35 | _ => case pIopt of
3.36 NONE => ("no-fmz-spec", ([], [], ptp))
3.37 - | SOME _ => (*vvvvvv: Apply_Method without init_form*)
3.38 - switch_specify_solve p_ (pt, ip)
3.39 + | SOME _ => switch_specify_solve p_ (pt, ip)
3.40 end
3.41
3.42 +(** locate an input tactic **)
3.43 +
3.44 +datatype lOc_ = ERror of string | UNsafe of Chead.calcstate' | Updated of Chead.calcstate'
3.45 +(* loc_specify_ : Tactic.T -> Calc.T -> lOc_*)
3.46 +fun loc_specify_ m (pt, pos) =
3.47 + let
3.48 + val (p, _, f, _, _, pt) = Chead.specify m pos [] pt;
3.49 + in
3.50 + case f of (Generate.Error' e) => ERror e | _ => Updated ([], [], (pt,p))
3.51 + end
3.52 +(* loc_solve_ : Tactic.T -> Calc.T -> lOc_*)
3.53 +fun loc_solve_ m (pt, pos) =
3.54 + let
3.55 + val (msg, cs') = Step_Solve.by_tactic m (pt, pos); (*..sig.OK*)
3.56 + in
3.57 + case msg of "ok" => Updated cs' | msg => ERror msg
3.58 + end
3.59 +
3.60 +(* locate a tactic in a program and apply it if possible;
3.61 + report of tacs' applicability in tacis; pt is dropped in setNextTactic*)
3.62 +fun by_tactic _ (ptp as (_, ([], Pos.Res))) = ("end-of-calculation", ([], [], ptp))
3.63 + | by_tactic m (ptp as (pt, p)) =
3.64 + case Applicable.applicable_in p pt m of
3.65 + Applicable.Notappl _ => ("not-applicable", ([],[], ptp): Chead.calcstate')
3.66 + | Applicable.Appl m =>
3.67 + let
3.68 + val x = if Tactic.for_specify' m
3.69 + then loc_specify_ m ptp else loc_solve_ m ptp
3.70 + in
3.71 + case x of
3.72 + ERror _ => ("failure", ([], [], ptp))
3.73 + (*FIXXXXXME: loc_specify_, loc_solve_ TOGETHER with dropping meOLD+detail.sml*)
3.74 + | UNsafe cs' => ("unsafe-ok", cs')
3.75 + | Updated (cs' as (_, _, (_, p'))) => (*ev.SEVER.tacs like Begin_Trans*)
3.76 + (if p' = ([], Pos.Res) then "end-of-calculation" else "ok", cs')
3.77 + (*for SEVER.tacs user to ask ? *)
3.78 + end
3.79 +
3.80 (**)end(**)
4.1 --- a/src/Tools/isac/TODO.thy Tue Feb 11 10:59:18 2020 +0100
4.2 +++ b/src/Tools/isac/TODO.thy Tue Feb 11 11:58:45 2020 +0100
4.3 @@ -288,7 +288,7 @@
4.4 \begin{itemize}
4.5 \item Step_Specify.check <-- Applicable.applicable_in
4.6 \item Step_Specify.add <-- Generate.generate1
4.7 - \item Step_Specify.do_next :
4.8 + \item Step_Specify.do_next : DONE
4.9 \item Step_Specify.by_tactic :
4.10 \item Step_Specify.by_/// = Step_Specify.by_tactic ? depending on PIDE
4.11 \end{itemize}
5.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Tue Feb 11 10:59:18 2020 +0100
5.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Tue Feb 11 11:58:45 2020 +0100
5.3 @@ -174,22 +174,22 @@
5.4 val ((pt'''''_', _), _) = get_calc cI
5.5 val ip'''''_' = get_pos cI 1;
5.6
5.7 - val xxxxx_x(*"ok", (tacis, _, _)*) = (*case*) Math_Engine.locatetac tac (pt'''''_', ip'''''_') (*of*);
5.8 + val xxxxx_x(*"ok", (tacis, _, _)*) = (*case*) Step.by_tactic tac (pt'''''_', ip'''''_') (*of*);
5.9 (*+isa+REP*)val ("ok", ( [ (Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv"),
5.10 Rewrite_Set_Inst' _, (pos', (istate, ctxt))) ] , _, cstate)) = xxxxx_x;
5.11
5.12 -(*//******************* locatetac returns tac_ + istate + cstate *****************************\\*)
5.13 -locatetac : Tactic.input -> state -> string * (taci list * pos' list * state);
5.14 +(*//******************* Step.by_tactic returns tac_ + istate + cstate *****************************\\*)
5.15 +Step.by_tactic : Tactic.input -> state -> string * (taci list * pos' list * state);
5.16 if istate2str istate
5.17 = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], e_rls, SOME e_e, \nx = 0 + -1 * (1 + -1 * 2), ORundef, true, true)"
5.18 -then () else error "from locatetac return --- changed 1";
5.19 +then () else error "from Step.by_tactic return --- changed 1";
5.20
5.21 if istate2str (get_istate (fst cstate) (snd cstate))
5.22 = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], e_rls, SOME e_e, \nx = 0 + -1 * (1 + -1 * 2), ORundef, true, true)"
5.23 -then () else error "from locatetac return --- changed 2";
5.24 -(*\\******************* locatetac returns tac_ + istate + cstate *****************************//*)
5.25 +then () else error "from Step.by_tactic return --- changed 2";
5.26 +(*\\******************* Step.by_tactic returns tac_ + istate + cstate *****************************//*)
5.27
5.28 -"~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt'''''_', ip'''''_'));
5.29 +"~~~~~ fun Step.by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt'''''_', ip'''''_'));
5.30 val Applicable.Appl m = (*case*) Applicable.applicable_in p pt tac (*of*);
5.31 (*if*) Tactic.for_specify' m; (*false*)
5.32
6.1 --- a/test/Tools/isac/Interpret/inform.sml Tue Feb 11 10:59:18 2020 +0100
6.2 +++ b/test/Tools/isac/Interpret/inform.sml Tue Feb 11 11:58:45 2020 +0100
6.3 @@ -1218,7 +1218,7 @@
6.4 val Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) = rew;
6.5
6.6 "~~~~~ to inputFillFormula return val:"; val ("ok", tac) = ("ok", tac);
6.7 - val ("ok", (_, c, ptp as (_,p'))) = locatetac tac (pt, pos);
6.8 + val ("ok", (_, c, ptp as (_,p'))) = Step.by_tactic tac (pt, pos);
6.9 upd_calc cI (ptp, []);
6.10 upd_ipos cI 1 p';
6.11 autocalculateOK2xml cI pos (if null c then p' else last_elem c) p';
7.1 --- a/test/Tools/isac/Interpret/li-tool.sml Tue Feb 11 10:59:18 2020 +0100
7.2 +++ b/test/Tools/isac/Interpret/li-tool.sml Tue Feb 11 11:58:45 2020 +0100
7.3 @@ -54,11 +54,11 @@
7.4 "~~~~~ fun applyTactic, args:"; val ((cI:calcID), ip, tac) = (1, p, (hd appltacs));
7.5 val ((pt, _), _) = get_calc cI;
7.6 val p = get_pos cI 1;
7.7 -locatetac;
7.8 -locatetac tac;
7.9 +Step.by_tactic;
7.10 +Step.by_tactic tac;
7.11
7.12 -(*locatetac tac (pt, ip); (*WAS scan_dn1: call by ([3], Pbl)*)*)
7.13 -"~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, ip));
7.14 +(*Step.by_tactic tac (pt, ip); (*WAS scan_dn1: call by ([3], Pbl)*)*)
7.15 +"~~~~~ fun Step.by_tactic, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, ip));
7.16 val Appl m = applicable_in p pt tac ; (*Appl*)
7.17 (*if*) Tactic.for_specify' m; (*false*)
7.18 (*loc_solve_ (mI,m) ptp; (*Argument: (mI, m) : string * tac Reason: Can't unify tac_ with tac*)*)
7.19 @@ -106,7 +106,7 @@
7.20 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.21 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.22 "~~~~~ fun me, args:"; val tac = nxt;
7.23 -"~~~~~ fun locatetac, args:"; val ptp as (pt, p) = (pt, p);
7.24 +"~~~~~ fun Step.by_tactic, args:"; val ptp as (pt, p) = (pt, p);
7.25 val Appl m = applicable_in p pt tac;
7.26 (*if*) Tactic.for_specify' m; (*false*)
7.27 "~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = (m, ptp);
8.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Tue Feb 11 10:59:18 2020 +0100
8.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Tue Feb 11 11:58:45 2020 +0100
8.3 @@ -36,7 +36,7 @@
8.4 "----- step 8: returns nxt = Rewrite_Set_Inst ([\"(''bdv'', x)\"],\"integration\")";
8.5
8.6 "~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
8.7 -"~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
8.8 +"~~~~~ fun Step.by_tactic, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
8.9 val Appl m = applicable_in p pt tac;
8.10 (*if*) Tactic.for_specify' m; (*false*)
8.11 "~~~~~ fun loc_solve_ , args:"; val (m, (pt,pos)) = (m, ptp);
8.12 @@ -107,8 +107,8 @@
8.13
8.14 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt);
8.15
8.16 - (** )val (***)xxxx(***) ( *("ok", (_, _, (pt, p))) =( **) (*case*) locatetac tac (pt,p) (*of*);
8.17 -"~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
8.18 + (** )val (***)xxxx(***) ( *("ok", (_, _, (pt, p))) =( **) (*case*) Step.by_tactic tac (pt,p) (*of*);
8.19 +"~~~~~ fun Step.by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
8.20 val Applicable.Appl m = (*case*) Applicable.applicable_in p pt tac (*of*);
8.21 (*if*) Tactic.for_specify' m; (*false*)
8.22
8.23 @@ -179,11 +179,11 @@
8.24 "~~~~~ from Step_Solve.by_tactic to loc_solve_ return:"; val ((msg, cs' : calcstate'))
8.25 = ("ok", ([(Tactic.input_from_T tac, tac, (p'', (istate, ctxt)) )], [(*ctree NOT cut*)], (pt', p'')));
8.26
8.27 -"~~~~~ from loc_solve_ to locatetac return:"; val (Updated (cs' as (_, _, (_, p'))))
8.28 +"~~~~~ from loc_solve_ to Step.by_tactic return:"; val (Updated (cs' as (_, _, (_, p'))))
8.29 = (*** )xxxxx( ***) (Updated (cs'));
8.30 (*if*) p' = ([], Pos.Res); (*else*)
8.31 ("ok", cs');
8.32 -"~~~~~ from locatetac to me return:"; val (("ok", (_, _, (pt, p)))) = (*** )xxxx( ***) ("ok", cs');
8.33 +"~~~~~ from Step.by_tactic to me return:"; val (("ok", (_, _, (pt, p)))) = (*** )xxxx( ***) ("ok", cs');
8.34 val (_, ts) =
8.35 (case Step.do_next p ((pt, Pos.e_pos'), []) of
8.36 ("ok", (ts as (_, _, _) :: _, _, _)) => ("", ts)
8.37 @@ -260,18 +260,18 @@
8.38 ["Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",
8.39 "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")"]
8.40 then () else error "sel_appl_atomic_tacs ([1], Res) CHANGED";
8.41 -(*[2], Res*)val ("ok", (_, _, ptp as (pt, p))) = locatetac (hd (sel_appl_atomic_tacs pt p)) (pt, p);
8.42 +(*[2], Res*)val ("ok", (_, _, ptp as (pt, p))) = Step.by_tactic (hd (sel_appl_atomic_tacs pt p)) (pt, p);
8.43
8.44 (*+*)if map tac2str (sel_appl_atomic_tacs pt p) =
8.45 ["Rewrite (\"tausche_minus\", \"\<lbrakk>?b ist_monom; ?a kleiner ?b\<rbrakk>\n\<Longrightarrow> ?b - ?a = - ?a + ?b\")", "Rewrite (\"tausche_plus_minus\", \"?b kleiner ?c \<Longrightarrow> ?a + ?c - ?b = ?a - ?b + ?c\")",
8.46 "Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",
8.47 "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")", "Calculate MINUS"]
8.48 then () else error "sel_appl_atomic_tacs ([1], Res) CHANGED";
8.49 -(* = ([3], Res)*)val ("ok", (_, _, ptp as (pt, p))) = locatetac (hd (sel_appl_atomic_tacs pt p)) (pt, p);
8.50 +(* = ([3], Res)*)val ("ok", (_, _, ptp as (pt, p))) = Step.by_tactic (hd (sel_appl_atomic_tacs pt p)) (pt, p);
8.51
8.52 (*//----------------- exception PTREE "get_obj f EmptyPtree" raised --------------------------\\*)
8.53 -(** )val ("ok", (_, _, ptp as (pt, p))) =( **) locatetac (hd (sel_appl_atomic_tacs pt p)) (pt, p);
8.54 -"~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (hd (sel_appl_atomic_tacs pt p), (pt, p));
8.55 +(** )val ("ok", (_, _, ptp as (pt, p))) =( **) Step.by_tactic (hd (sel_appl_atomic_tacs pt p)) (pt, p);
8.56 +"~~~~~ fun Step.by_tactic , args:"; val (tac, (ptp as (pt, p))) = (hd (sel_appl_atomic_tacs pt p), (pt, p));
8.57 val Applicable.Appl m = (*case*) Applicable.applicable_in p pt tac (*of*);
8.58 (*if*) Tactic.for_specify' m; (*false*)
8.59
9.1 --- a/test/Tools/isac/Knowledge/biegelinie-4.sml Tue Feb 11 10:59:18 2020 +0100
9.2 +++ b/test/Tools/isac/Knowledge/biegelinie-4.sml Tue Feb 11 11:58:45 2020 +0100
9.3 @@ -126,14 +126,14 @@
9.4
9.5 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
9.6 val (pt''', p''') =
9.7 - (*locatetac is here for testing by me; Step.do_next would suffice in me*)
9.8 - case locatetac tac (pt,p) of
9.9 + (*Step.by_tactic is here for testing by me; Step.do_next would suffice in me*)
9.10 + case Step.by_tactic tac (pt,p) of
9.11 ("ok", (_, _, ptp)) => ptp
9.12 ;
9.13 (*+*)p = ([], Met);
9.14 (*+*)p''' = ([1], Pbl);
9.15 (*+*)val PblObj {meth, probl, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt''' (fst p''');
9.16 -(*+*)(*MISSING after locatetac:*)
9.17 +(*+*)(*MISSING after Step.by_tactic:*)
9.18 (*+*)writeln (oris2str oris); (*[
9.19 (1, ["1"], #Given,Streckenlast, ["q_0"]),
9.20 (2, ["1"], #Given,FunktionsVariable, ["x"]),
9.21 @@ -142,7 +142,7 @@
9.22 Biegelinie
9.23 AbleitungBiegelinie
9.24 *)
9.25 -"~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
9.26 +"~~~~~ fun Step.by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
9.27 val Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
9.28 (*if*) member op = Solve.specsteps mI = false; (*else*)
9.29
9.30 @@ -219,11 +219,11 @@
9.31
9.32 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt''''', p''''', c, pt''''');
9.33 (* val (pt, p) = *)
9.34 - (*locatetac is here for testing by me; Step.do_next would suffice in me*)
9.35 - case locatetac tac (pt,p) of
9.36 + (*Step.by_tactic is here for testing by me; Step.do_next would suffice in me*)
9.37 + case Step.by_tactic tac (pt,p) of
9.38 ("ok", (_, _, ptp)) => ptp
9.39 ;
9.40 -"~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
9.41 +"~~~~~ fun Step.by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
9.42 val Applicable.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
9.43 (*if*) member op = Solve.specsteps mI = true; (*then*)
9.44
10.1 --- a/test/Tools/isac/Knowledge/partial_fractions.sml Tue Feb 11 10:59:18 2020 +0100
10.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml Tue Feb 11 11:58:45 2020 +0100
10.3 @@ -40,7 +40,7 @@
10.4 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Rewrite (ruleZY, Inverse_Z_Transform.ruleZY) --> X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))";
10.5 val (p''',_,f,nxt''',_,pt''') = me nxt p [] pt; "nxt = Rewrite_Set norm_Rational --> X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))";
10.6 "~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, [], pt);
10.7 -val ("ok", (_, _, ptp)) = locatetac tac (pt,p)
10.8 +val ("ok", (_, _, ptp)) = Step.by_tactic tac (pt,p)
10.9 val (pt, p) = ptp;
10.10 "~~~~~ fun Step.do_next, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =
10.11 (p, ((pt, e_pos'),[]));
10.12 @@ -59,7 +59,7 @@
10.13 "----------- why not nxt = Model_Problem here ? ---------";
10.14 val (p,_,f,nxt,_,pt) = me nxt''' p''' [] pt''';
10.15 "~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
10.16 -val ("ok", (_, _, ptp)) = locatetac tac (pt,p);
10.17 +val ("ok", (_, _, ptp)) = Step.by_tactic tac (pt,p);
10.18 val (pt, p) = ptp;
10.19 "~~~~~ fun Step.do_next, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =
10.20 (p, ((pt, e_pos'),[]));
11.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Tue Feb 11 10:59:18 2020 +0100
11.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Tue Feb 11 11:58:45 2020 +0100
11.3 @@ -183,7 +183,7 @@
11.4 (*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2] TODO sqrt*)
11.5 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*)
11.6 "~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, [], pt);
11.7 -"~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
11.8 +"~~~~~ fun Step.by_tactic, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
11.9 val Appl m = applicable_in p pt tac;
11.10 val Check_elementwise' (trm1, str, (trm2, trms)) = m;
11.11 term2str trm1 = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]";
12.1 --- a/test/Tools/isac/Knowledge/rateq.sml Tue Feb 11 10:59:18 2020 +0100
12.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Tue Feb 11 11:58:45 2020 +0100
12.3 @@ -93,8 +93,8 @@
12.4 f2str f = "[x = 1 / 5]";
12.5 case nxt of ("Check_elementwise", Check_elementwise "Assumptions") => () | _ => ((*not checked before*));
12.6 "~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
12.7 -val (pt, p) = case locatetac tac (pt,p) of
12.8 -("ok", (_, _, ptp)) => ptp | _ => error "--- solve (1/x = 5.. locatetac";
12.9 +val (pt, p) = case Step.by_tactic tac (pt,p) of
12.10 +("ok", (_, _, ptp)) => ptp | _ => error "--- solve (1/x = 5.. Step.by_tactic";
12.11 "~~~~~ fun Step.do_next, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
12.12 val pIopt = get_pblID (pt,ip); (*= SOME ["rational", "univariate", "equation"]
12.13 1-1 associated to metID ["RatEq", "solve_rat_equation"]*)
12.14 @@ -277,7 +277,7 @@
12.15 *)
12.16 val (pt''', p''') = (pt, p);
12.17 "~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
12.18 - val (pt, p) = case locatetac tac (pt,p) of
12.19 + val (pt, p) = case Step.by_tactic tac (pt,p) of
12.20 ("ok", (_, _, ptp)) => ptp | _ => error "error in test setup";
12.21 "~~~~~ Step.do_next, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =
12.22 (p, ((pt, e_pos'),[]));
13.1 --- a/test/Tools/isac/Knowledge/rootrateq.sml Tue Feb 11 10:59:18 2020 +0100
13.2 +++ b/test/Tools/isac/Knowledge/rootrateq.sml Tue Feb 11 11:58:45 2020 +0100
13.3 @@ -101,7 +101,7 @@
13.4 (*... which works; thus error must be in script interpretation*)
13.5
13.6 "~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
13.7 -val (pt, p) = case locatetac tac (pt,p) of
13.8 +val (pt, p) = case Step.by_tactic tac (pt,p) of
13.9 ("ok", (_, _, ptp)) => ptp;
13.10 "~~~~~ fun Step.do_next, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
13.11 val pIopt = get_pblID (pt,ip);
13.12 @@ -312,14 +312,14 @@
13.13 (*val (p,_,f,nxt,_,pt) =*) me nxt p c pt;
13.14 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
13.15 val (pt, p) =
13.16 - (*locatetac is here for testing by me; do_next would suffice in me*)
13.17 - case locatetac tac (pt, p) of
13.18 + (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
13.19 + case Step.by_tactic tac (pt, p) of
13.20 ("ok", (_, _, ptp)) => ptp
13.21 | ("unsafe-ok", (_, _, ptp)) => ptp
13.22 | ("not-applicable",_) => (pt, p)
13.23 | ("end-of-calculation", (_, _, ptp)) => ptp
13.24 | ("failure", _) => error "sys-error"
13.25 - | _ => error "me: uncovered case locatetac"
13.26 + | _ => error "me: uncovered case Step.by_tactic"
13.27
13.28 (*case*)
13.29 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
14.1 --- a/test/Tools/isac/MathEngBasic/ctree-navi.sml Tue Feb 11 10:59:18 2020 +0100
14.2 +++ b/test/Tools/isac/MathEngBasic/ctree-navi.sml Tue Feb 11 11:58:45 2020 +0100
14.3 @@ -47,8 +47,8 @@
14.4 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Subproblem",*)
14.5 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Model_Problem",*)
14.6 "~~~~~ fun me, args:"; val (tac) = nxt;
14.7 -val (pt, p) = case locatetac tac (pt,p) of
14.8 - ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
14.9 +val (pt, p) = case Step.by_tactic tac (pt,p) of
14.10 + ("ok", (_, _, ptp)) => ptp | _ => error "script.sml Step.by_tactic";
14.11 "~~~~~ fun Step.do_next, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
14.12 val pIopt = get_pblID (pt,ip);
14.13 tacis; (*= []*)
15.1 --- a/test/Tools/isac/MathEngBasic/mstools.sml Tue Feb 11 10:59:18 2020 +0100
15.2 +++ b/test/Tools/isac/MathEngBasic/mstools.sml Tue Feb 11 11:58:45 2020 +0100
15.3 @@ -47,8 +47,8 @@
15.4 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Subproblem",*)
15.5 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Model_Problem",*)
15.6 "~~~~~ fun me, args:"; val (tac) = nxt;
15.7 -val (pt, p) = case locatetac tac (pt,p) of
15.8 - ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
15.9 +val (pt, p) = case Step.by_tactic tac (pt,p) of
15.10 + ("ok", (_, _, ptp)) => ptp | _ => error "script.sml Step.by_tactic";
15.11 "~~~~~ fun Step.do_next, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
15.12 val pIopt = get_pblID (pt,ip);
15.13 tacis; (*= []*)
16.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Tue Feb 11 10:59:18 2020 +0100
16.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Tue Feb 11 11:58:45 2020 +0100
16.3 @@ -137,7 +137,7 @@
16.4 ["Test","squ-equ-test-subpbl1"]);
16.5 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
16.6 "~~~~~ fun me, args:"; val tac = nxt;
16.7 -val ("ok", (_, _, (pt, p))) = locatetac tac (pt,p);
16.8 +val ("ok", (_, _, (pt, p))) = Step.by_tactic tac (pt,p);
16.9 "~~~~~ fun Step.do_next, args:"; val (ip as (_,p_), ptp as (pt,p), tacis) = (p, (pt, e_pos'), []);
16.10 val pIopt = get_pblID (pt,ip);
16.11 ip = ([],Res) (*false*);
16.12 @@ -353,7 +353,7 @@
16.13 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
16.14 "~~~~~ fun me, args:"; val (tac, (p:pos'), (_:NEW(*remove*)), (pt:ctree)) =
16.15 (nxt, p, [], pt);
16.16 -val ("ok", (_, _, ptp)) = locatetac tac (pt,p)
16.17 +val ("ok", (_, _, ptp)) = Step.by_tactic tac (pt,p)
16.18 val (pt, p) = ptp;
16.19 "~~~~~ fun Step.do_next, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =
16.20 (p, ((pt, e_pos'),[]));
17.1 --- a/test/Tools/isac/MathEngine/solve.sml Tue Feb 11 10:59:18 2020 +0100
17.2 +++ b/test/Tools/isac/MathEngine/solve.sml Tue Feb 11 11:58:45 2020 +0100
17.3 @@ -110,7 +110,7 @@
17.4
17.5 (*//------------------ begin step into 2 ----------------------------------------------------\\*)
17.6 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt'''''_', p'''''_', [], pt'''''_');
17.7 - val ("ok", (_, _, (pt, p))) = (*case*) locatetac tac (pt, p) (*of*);
17.8 + val ("ok", (_, _, (pt, p))) = (*case*) Step.by_tactic tac (pt, p) (*of*);
17.9
17.10 (*+*)if (get_istate pt p |> istate2str)
17.11 (*+*) = "Pstate ([\"\n(e_e, 16 + 12 * x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,L,R,R], e_rls, SOME e_e, \nx = -1 * 16 / 12, ORundef, true, true)"
17.12 @@ -124,10 +124,10 @@
17.13 tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
17.14 | _ => if p = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
17.15
17.16 - (p, [] : NEW, TESTg_form (pt, p) (* form output comes from locatetac *),
17.17 + (p, [] : NEW, TESTg_form (pt, p) (* form output comes from Step.by_tactic *),
17.18 tac, Telem.Sundef, pt); (*return from me*)
17.19 "~~~~~ from fun me\<longrightarrow>toplevel, return:"; val (p'''''_',_,f,nxt'''''_',_,pt'''''_')
17.20 - = (p, [] : NEW, TESTg_form (pt, p) (* form output comes from locatetac *),
17.21 + = (p, [] : NEW, TESTg_form (pt, p) (* form output comes from Step.by_tactic *),
17.22 tac, Telem.Sundef, pt);
17.23
17.24 (*+*)if (get_istate pt'''''_' p'''''_' |> istate2str)
18.1 --- a/test/Tools/isac/Minisubpbl/150-add-given.sml Tue Feb 11 10:59:18 2020 +0100
18.2 +++ b/test/Tools/isac/Minisubpbl/150-add-given.sml Tue Feb 11 11:58:45 2020 +0100
18.3 @@ -14,7 +14,7 @@
18.4 "~~~~~ fun me, args:"; val (tac, (p:pos'), (_:NEW), (pt:ctree)) = (nxt, p, [], pt);
18.5 val (pt, p) =
18.6 (*ERROR nxt_add: types or dsc DO NOT MATCH BETWEEN fmz --- pbt ... see 100-init-rootpbl.sml*)
18.7 - case locatetac tac (pt,p) of
18.8 + case Step.by_tactic tac (pt,p) of
18.9 ("ok", (_, _, ptp)) => ptp;
18.10 (* val (_, ts) =
18.11 (case Step.do_next p ((pt, e_pos'),[]) of
19.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Tue Feb 11 10:59:18 2020 +0100
19.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Tue Feb 11 11:58:45 2020 +0100
19.3 @@ -23,8 +23,8 @@
19.4 val (p, f, nxt, pt) = (p'''',f'''',nxt'''',pt'''');
19.5 "~~~~~ fun me, args:"; val tac = nxt;
19.6 val (pt, p) =
19.7 - (*locatetac is here for testing by me; Step.do_next would suffice in me*)
19.8 - case locatetac tac (pt,p) of
19.9 + (*Step.by_tactic is here for testing by me; Step.do_next would suffice in me*)
19.10 + case Step.by_tactic tac (pt,p) of
19.11 ("ok", (_, _, ptp)) => ptp | _ => error "CHANGED --- Minisubplb/200-start-method 1"
19.12 (* Step.do_next p ((pt, e_pos'),[]) ..ERROR = ("helpless",*)
19.13 "~~~~~ fun Step.do_next, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =
19.14 @@ -45,8 +45,8 @@
19.15 2.ERROR WAS: *** stac2tac_ TODO: no match for (Rewrite_Set ''norm_equation'') (x + 1 = 2)*)
19.16 "~~~~~ we continue with (@2) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~";
19.17 "~~~~~ fun me, args:"; val tac = nxt;
19.18 -val ("ok", (_, _, (pt''''',p'''''))) = locatetac tac (pt,p);
19.19 -"~~~~~ fun locatetac, args:"; val ptp as (pt, p) = (pt, p);
19.20 +val ("ok", (_, _, (pt''''',p'''''))) = Step.by_tactic tac (pt,p);
19.21 +"~~~~~ fun Step.by_tactic, args:"; val ptp as (pt, p) = (pt, p);
19.22 val Appl m = applicable_in p pt tac; (*m = Apply_Method'..*)
19.23 (*if*) Tactic.for_specify' m; (*false*)
19.24 "~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos) ) = (m, ptp);
19.25 @@ -116,7 +116,7 @@
19.26 if type_of unknown = TFree ("'a", ["Groups.plus"]) then ()
19.27 else error "x+1=2 after start root-pbl wrong type-inference for unknown";
19.28
19.29 -"~~~~~ continue me (@3) after locatetac";
19.30 +"~~~~~ continue me (@3) after Step.by_tactic";
19.31 val (pt, p) = (pt''''',p''''');
19.32 "~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~";
19.33 "~~~~~ fun Step.do_next, args:"; val ((ip as (_, p_)), (ptp as (pt,p), tacis)) = (p, ((pt, Pos.e_pos'),[]));
20.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Tue Feb 11 10:59:18 2020 +0100
20.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Tue Feb 11 11:58:45 2020 +0100
20.3 @@ -33,8 +33,8 @@
20.4 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt'''', p'''', [], pt'''');
20.5
20.6 (*ERROR WAS: scan_dn1: call by ([3], Pbl)*)
20.7 -val ("ok", (_, _, ptp''''')) = (*case*) locatetac tac (pt,p) (*of*);
20.8 -"~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
20.9 +val ("ok", (_, _, ptp''''')) = (*case*) Step.by_tactic tac (pt,p) (*of*);
20.10 +"~~~~~ fun Step.by_tactic, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
20.11 val Applicable.Appl m = (*case*) Applicable.applicable_in p pt tac (*of*);
20.12 (*if*) Tactic.for_specify' m; (*false*)
20.13
20.14 @@ -87,7 +87,7 @@
20.15
20.16 (*+*)if Rule.id_rls rls = HOLogic.dest_string rls_ then () else error "Prog_Tac.associate changed";
20.17
20.18 -"~~~~~ continue me[1] after locatetac";
20.19 +"~~~~~ continue me[1] after Step.by_tactic";
20.20 val (pt, p) = ptp''''';
20.21 (* isabisac17: val ("helpless", _) = (*case*) Step.do_next p ((pt, Pos.e_pos'),[]) (*of*)*)
20.22 "~~~~~ fun step, args:"; val ((ip as (_, p_)), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'),[]));
20.23 @@ -132,8 +132,8 @@
20.24 (**)val (p,_,f,nxt,_,pt) = me nxt'''_' p'''_' [] pt'''_';(**)
20.25 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt'''_', p'''_', [], pt'''_');
20.26 val (pt, p) =
20.27 - (*locatetac is here for testing by me; step would suffice in me*)
20.28 - case locatetac tac (pt, p) of
20.29 + (*Step.by_tactic is here for testing by me; step would suffice in me*)
20.30 + case Step.by_tactic tac (pt, p) of
20.31 ("ok", (_, _, ptp)) => ptp
20.32 | ("unsafe-ok", (_, _, ptp)) => ptp
20.33 | ("not-applicable",_) => (pt, p)
21.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Tue Feb 11 10:59:18 2020 +0100
21.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Tue Feb 11 11:58:45 2020 +0100
21.3 @@ -25,7 +25,7 @@
21.4 1 relevant for updating ctxt *)
21.5 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt''', p''', [], pt''');
21.6
21.7 -"~~~~~ fun locatetac , args:"; val (tac, ptp as (pt, p)) = (tac, (pt''',p'''));
21.8 +"~~~~~ fun Step.by_tactic , args:"; val (tac, ptp as (pt, p)) = (tac, (pt''',p'''));
21.9 val Appl m = applicable_in p pt tac;
21.10 (*if*) Tactic.for_specify' m; (*false*)
21.11 (*val Updated (cs' as (_,_,(_,p'))) = loc_solve_ (mI,m) ptp;*)
22.1 --- a/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Tue Feb 11 10:59:18 2020 +0100
22.2 +++ b/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Tue Feb 11 11:58:45 2020 +0100
22.3 @@ -38,8 +38,8 @@
22.4 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt''', p''', [], pt''');
22.5 val ("ok", (_, _, (pt'''', p''''))) = (*case*)
22.6
22.7 - locatetac tac (pt, p) (*of*);
22.8 -"~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
22.9 + Step.by_tactic tac (pt, p) (*of*);
22.10 +"~~~~~ fun Step.by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
22.11 val Appl m = (*case*) applicable_in p pt tac (*of*);
22.12 (*if*) Tactic.for_specify' m; (*false*)
22.13
22.14 @@ -59,8 +59,8 @@
22.15 (is as Istate.Pstate {env, ...}, ctxt, sc) => (is, env, ctxt, sc)
22.16 | _ => error "Step_Solve.by_tactic Apply_Method: uncovered case init_pstate"
22.17
22.18 -(*+*)val (pt, p) = case locatetac tac (pt, pos) of
22.19 - ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
22.20 +(*+*)val (pt, p) = case Step.by_tactic tac (pt, pos) of
22.21 + ("ok", (_, _, ptp)) => ptp | _ => error "script.sml Step.by_tactic";
22.22 (*+*)val SOME t = parseNEW (get_ctxt pt p) "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
22.23
22.24 "~~~~~ from Step_Solve.by_tactic to..to me return"; val (pt, p) = (pt'''', p'''');
23.1 --- a/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Tue Feb 11 10:59:18 2020 +0100
23.2 +++ b/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Tue Feb 11 11:58:45 2020 +0100
23.3 @@ -34,8 +34,8 @@
23.4 val (pt''''', p''''') = (pt, p);
23.5
23.6 "~~~~~ fun me , args:"; val tac = nxt;
23.7 -val (pt, p) = case locatetac tac (pt,p) of
23.8 - ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
23.9 +val (pt, p) = case Step.by_tactic tac (pt,p) of
23.10 + ("ok", (_, _, ptp)) => ptp | _ => error "script.sml Step.by_tactic";
23.11 val (pt'''', p'''') = (pt, p);
23.12 "~~~~~ fun do_next , args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
23.13 val pIopt = get_pblID (pt,ip); (*= SOME ["sqroot-test", "univariate", ...]*)
24.1 --- a/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Tue Feb 11 10:59:18 2020 +0100
24.2 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Tue Feb 11 11:58:45 2020 +0100
24.3 @@ -45,8 +45,8 @@
24.4
24.5 val (pt'''', p'''') = (pt, p);
24.6 "~~~~~ fun me, args:"; val tac = nxt;
24.7 -val (pt, p) = case locatetac tac (pt,p) of
24.8 -("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
24.9 +val (pt, p) = case Step.by_tactic tac (pt,p) of
24.10 +("ok", (_, _, ptp)) => ptp | _ => error "script.sml Step.by_tactic";
24.11 show_pt pt; (*...(([3], Res), [x = 1])]... back in root, OK *)
24.12 "~~~~~ fun do_next, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
24.13 val pIopt = get_pblID (pt,ip); (*= SOME ["sqroot-test", "univariate", ...]*)
25.1 --- a/test/Tools/isac/Test_Isac_Short.thy Tue Feb 11 10:59:18 2020 +0100
25.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Tue Feb 11 11:58:45 2020 +0100
25.3 @@ -286,6 +286,14 @@
25.4 ML \<open>
25.5 \<close> ML \<open>
25.6 \<close> ML \<open>
25.7 +\<close> ML \<open>
25.8 +\<close> ML \<open>
25.9 +\<close> ML \<open>
25.10 +\<close> ML \<open>
25.11 +\<close> ML \<open>
25.12 +\<close> ML \<open>
25.13 +\<close> ML \<open>
25.14 +\<close> ML \<open>
25.15 \<close>
25.16
25.17 section \<open>history of tests\<close>
26.1 --- a/test/Tools/isac/Test_Some.thy Tue Feb 11 10:59:18 2020 +0100
26.2 +++ b/test/Tools/isac/Test_Some.thy Tue Feb 11 11:58:45 2020 +0100
26.3 @@ -202,13 +202,13 @@
26.4 \<close> ML \<open>
26.5 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [1], pt);
26.6 \<close> ML \<open>
26.7 - val ("ok", (_, _, ptp''''')) = (*case*) locatetac tac (pt, p) (*of*);
26.8 + val ("ok", (_, _, ptp''''')) = (*case*) Step.by_tactic tac (pt, p) (*of*);
26.9 \<close> ML \<open>
26.10 val ctxt = get_ctxt (fst ptp''''') (snd ptp''''');
26.11 terms2str (get_assumptions ctxt)
26.12 = "[\"lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2\",\"lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x\",\"x = 0\",\"x = 6 / 5\"]"
26.13 \<close> ML \<open>
26.14 -"~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
26.15 +"~~~~~ fun Step.by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
26.16 \<close> ML \<open>
26.17 val Applicable.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
26.18 \<close> ML \<open>