1.1 --- a/src/Tools/isac/CalcElements/contextC.sml Wed Dec 18 11:02:32 2019 +0100
1.2 +++ b/src/Tools/isac/CalcElements/contextC.sml Wed Dec 18 11:31:31 2019 +0100
1.3 @@ -40,17 +40,17 @@
1.4 * associate..Subproblem' returns ctxt ONLY with declare_constraints',
1.5 with insert_assumptions wait for Tactic.Apply_Method
1.6 * storing ctxt is done after return form locate_input_tactic
1.7 - * determine_next_tactic:
1.8 + * find_next_tactic:
1.9 * TODO initialises ctxt by TODO
1.10 * Tactic.Rewrite* create assumptions; respective insert_assumptions TODO
1.11 *
1.12 *
1.13 *
1.14 - * locate_input_formula: follows sig. of determine_next_tactic
1.15 - * changing from one method to another (in determine_next_tactic only):
1.16 + * locate_input_formula: follows sig. of find_next_tactic
1.17 + * changing from one method to another (in find_next_tactic only):
1.18 * from method to sub-program: just add new preconditions of the guard
1.19 * locate_input_tactic: init_pstate by begin_end_prog
1.20 - * determine_next_tactic:
1.21 + * find_next_tactic:
1.22 * from_subpbl_to_caller
1.23 * finishing a method:
1.24 * Tactic.Check_Postcond' uses ctxt for proving the post-condition (not yet implemented)
1.25 @@ -119,7 +119,7 @@
1.26 insert_assumptions
1.27 ? generate1 (look in test with "from ... to..))
1.28
1.29 -determine_next_tactic
1.30 +find_next_tactic
1.31 scan_to_tactic2
1.32 scan_dn2 ..leaf
1.33 stac2tac_
1.34 @@ -128,7 +128,7 @@
1.35 insert_assumptions
1.36 ? generate1 (look in test with "from ... to..))
1.37
1.38 -locate_input_formula uses determine_next_tactic
1.39 +locate_input_formula uses find_next_tactic
1.40 compare_step
1.41 all_modspec
1.42 declare_constraints'
2.1 --- a/src/Tools/isac/CalcElements/rule.sml Wed Dec 18 11:02:32 2019 +0100
2.2 +++ b/src/Tools/isac/CalcElements/rule.sml Wed Dec 18 11:31:31 2019 +0100
2.3 @@ -244,7 +244,7 @@
2.4 | Rfuns of (* for Rrls, usage see rational.sml ----- reverse rewrite ----- *)
2.5 {init_state : (* initialise for reverse rewriting by the Interpreter *)
2.6 term -> (* for this the rrlsstate is initialised: *)
2.7 - term * (* the current formula: goes locate_input_tactic -> determine_next_tactic via istate *)
2.8 + term * (* the current formula: goes locate_input_tactic -> find_next_tactic via istate *)
2.9 term * (* the final formula *)
2.10 rule list (* of reverse rewrite set (#1#) *)
2.11 list * (* may be serveral, eg. in norm_rational *)
3.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Dec 18 11:02:32 2019 +0100
3.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Dec 18 11:31:31 2019 +0100
3.3 @@ -13,7 +13,7 @@
3.4
3.5 datatype next_tactic_result = Next_Step of Istate.T * Proof.context * Tactic.T
3.6 | Helpless | End_Program of Istate.T * Tactic.T
3.7 - val determine_next_tactic: Rule.program -> Ctree.state -> Istate.T -> Proof.context
3.8 + val find_next_tactic: Rule.program -> Ctree.state -> Istate.T -> Proof.context
3.9 -> next_tactic_result
3.10
3.11 (*datatype input_formula_result = FStep of calcstate' | Not_Derivable *)
3.12 @@ -273,7 +273,7 @@
3.13 | scan_up1 _ _ t = error ("scan_up1 not impl for t= " ^ Rule.term2str t)
3.14
3.15 fun scan_to_tactic1 (prog, (cctt as ((_, p), _, _))) (Istate.Pstate (ist as {path, ...})) =
3.16 - if path = [] orelse Pos.at_first_tactic(*RM prog path RM WITH determine_next_tactic IN solve*)p
3.17 + if path = [] orelse Pos.at_first_tactic(*RM prog path RM WITH find_next_tactic IN solve*)p
3.18 then scan_dn1 cctt (ist |> set_path [R] |> set_or ORundef) (Program.body_of prog)
3.19 else go_scan_up1 (prog, cctt) ist
3.20 | scan_to_tactic1 _ _ = raise ERROR "scan_to_tactic1: uncovered pattern in fun.def"
3.21 @@ -307,7 +307,7 @@
3.22 term; (* value of Prog_Expr, for updating environment *)
3.23
3.24 (*
3.25 - scan_dn2, go_scan_up2, scan_up2 scan for determine_next_tactic.
3.26 + scan_dn2, go_scan_up2, scan_up2 scan for find_next_tactic.
3.27 (1) scan_dn2 is recursive descent;
3.28 (2) go_scan_up2 goes to the parent node and calls (3);
3.29 (3) scan_up2 resumes according to the interpreter-state.
3.30 @@ -473,7 +473,7 @@
3.31 | scan_to_tactic2 _ _ = raise ERROR "scan_to_tactic2: uncovered pattern";
3.32
3.33 (* decide for the next applicable Prog_Tac *)
3.34 -fun determine_next_tactic (Rule.Prog prog) (ptp as(pt, (p, _))) (Istate.Pstate ist) ctxt =
3.35 +fun find_next_tactic (Rule.Prog prog) (ptp as(pt, (p, _))) (Istate.Pstate ist) ctxt =
3.36 (case scan_to_tactic2 (prog, (ptp, ctxt)) (Istate.Pstate ist) of
3.37 (*
3.38 Term_Val2 v => (*program finished*)
3.39 @@ -505,8 +505,8 @@
3.40 (*NEW*) | _ => End_Program (Istate.Pstate ist, Tactic.End_Detail' (Rule.e_term,[])))
3.41 (*NEW*)| Reject_Tac2 => Helpless)
3.42 (*NEW*)
3.43 - | determine_next_tactic _ _ is _ =
3.44 - raise ERROR ("determine_next_tactic: not impl for " ^ Istate.istate2str is);
3.45 + | find_next_tactic _ _ is _ =
3.46 + raise ERROR ("find_next_tactic: not impl for " ^ Istate.istate2str is);
3.47
3.48
3.49 (*** locate an input formula in the program ***)
3.50 @@ -594,7 +594,7 @@
3.51 in
3.52 ([(Tactic.input_from_T tac_, tac_, (pos, is))], c, (pt, pos'))
3.53 end
3.54 -(*determine_next_tactic from program, begin_end_prog will update the ctree*)
3.55 +(*find_next_tactic from program, begin_end_prog will update the ctree*)
3.56 and do_solve_step (ptp as (pt, pos as (p, p_))) = (* WN1907: ?only for Begin_/End_Detail' DEL!!!*)
3.57 if Celem.e_metID = get_obj g_metID pt (par_pblobj pt p)
3.58 then ([], [], (pt, (p, p_)))
3.59 @@ -602,10 +602,10 @@
3.60 let
3.61 val thy' = get_obj g_domID pt (par_pblobj pt p);
3.62 val (_, (ist, ctxt), sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
3.63 -(*OLD* ) val (tac_, is, (t, _)) = determine_next_tactic sc (pt, pos) ist ctxt;
3.64 +(*OLD* ) val (tac_, is, (t, _)) = find_next_tactic sc (pt, pos) ist ctxt;
3.65 ( *OLD*)
3.66 (*NE*)in
3.67 -(*NEW*) case determine_next_tactic sc (pt, pos) ist ctxt of
3.68 +(*NEW*) case find_next_tactic sc (pt, pos) ist ctxt of
3.69 (*NEW*) Next_Step (ist, ctxt, tac) =>
3.70 (*NEW*) begin_end_prog tac (ist, Tactic.insert_assumptions tac ctxt) ptp
3.71 (*NEW*) | End_Program (ist, tac) =>
4.1 --- a/src/Tools/isac/Interpret/script.sml Wed Dec 18 11:02:32 2019 +0100
4.2 +++ b/src/Tools/isac/Interpret/script.sml Wed Dec 18 11:31:31 2019 +0100
4.3 @@ -43,7 +43,7 @@
4.4
4.5 end
4.6
4.7 -(* traces the leaves (ie. non-tactical nodes) of Prog found by determine_next_tactic, see "and scr" *)
4.8 +(* traces the leaves (ie. non-tactical nodes) of Prog found by find_next_tactic, see "and scr" *)
4.9 val trace_script = Unsynchronized.ref false; (* TODO: how are traces done in Isabelle? *)
4.10
4.11 (**)
5.1 --- a/src/Tools/isac/MathEngine/solve.sml Wed Dec 18 11:02:32 2019 +0100
5.2 +++ b/src/Tools/isac/MathEngine/solve.sml Wed Dec 18 11:31:31 2019 +0100
5.3 @@ -138,10 +138,10 @@
5.4 | NONE =>
5.5 let
5.6 (*OLD* ) val (m', (is', ctxt'), _) = (* re-design: should not be necessary *)
5.7 -(*OLD*) LucinNEW.determine_next_tactic sc (pt, (p, Res)) is ctxt;
5.8 +(*OLD*) LucinNEW.find_next_tactic sc (pt, (p, Res)) is ctxt;
5.9 ( *OLD*)
5.10 (*NEW*) val (m', is', ctxt') =
5.11 -(*NEW*) case LucinNEW.determine_next_tactic sc (pt, (p, Res)) is ctxt of
5.12 +(*NEW*) case LucinNEW.find_next_tactic sc (pt, (p, Res)) is ctxt of
5.13 (*NEW*) LucinNEW.Next_Step (ist, ctxt, tac) => (tac, ist, ctxt)
5.14 (*NEW*) | _ => raise ERROR ("solve Apply_Method " ^ strs2str' mI)
5.15 (*NEW*)
5.16 @@ -189,11 +189,11 @@
5.17 val thy' = get_obj g_domID pt pp;
5.18 val thy = Celem.assoc_thy thy';
5.19 (*OLD* )(*TODO?: required for 1 step in caller ??? vvvvvvvvvvvvvvvvvvvvv; dropped in begin_end_prog*)
5.20 -(*OLD*)val (_, _, (scval, _(*scsaf*))) = LucinNEW.determine_next_tactic (sc) (pt, (p, p_)) (Istate.Pstate pst) ctxt;
5.21 +(*OLD*)val (_, _, (scval, _(*scsaf*))) = LucinNEW.find_next_tactic (sc) (pt, (p, p_)) (Istate.Pstate pst) ctxt;
5.22 ( *OLD*)
5.23 (*NEW*)(* Tactic.input has NO prog_result, applicable_in canNOT get it*)
5.24 (*NEW*)val scval =
5.25 -(*NEW*) case LucinNEW.determine_next_tactic (sc) (pt, (p, p_)) (Istate.Pstate pst) ctxt of
5.26 +(*NEW*) case LucinNEW.find_next_tactic (sc) (pt, (p, p_)) (Istate.Pstate pst) ctxt of
5.27 (*NEW*) LucinNEW.Next_Step (_, _, Tactic.Check_elementwise' (_, _, (scval, _))) => scval
5.28 (*NEW*) | LucinNEW.End_Program (_, Tactic.Check_Postcond' (_, (scval, _))) => scval
5.29 (*NEW*) | _ => raise ERROR ("solve Check_Postcond " ^ strs2str' pI)
6.1 --- a/src/Tools/isac/Specify/appl.sml Wed Dec 18 11:02:32 2019 +0100
6.2 +++ b/src/Tools/isac/Specify/appl.sml Wed Dec 18 11:31:31 2019 +0100
6.3 @@ -122,7 +122,7 @@
6.4 | Notappl of string (* tactic is NOT applicable *)
6.5
6.6 (* applicability of a tacic wrt. a calc-state (ctree, pos').
6.7 - additionally used by determine_next_tactic.
6.8 + additionally used by find_next_tactic.
6.9 tests for applicability are so expensive, that results (rewrites!)
6.10 are kept in the return-value of 'type tac_' *)
6.11 fun applicable_in _ _ (Tactic.Init_Proof (ct', spec)) = Appl (Tactic.Init_Proof' (ct', spec))
7.1 --- a/src/Tools/isac/TODO.thy Wed Dec 18 11:02:32 2019 +0100
7.2 +++ b/src/Tools/isac/TODO.thy Wed Dec 18 11:31:31 2019 +0100
7.3 @@ -78,23 +78,37 @@
7.4 \item xxx
7.5 \item re-organise code for Interpret
7.6 \begin{itemize}
7.7 - \item Step*
7.8 + \item Step*:
7.9 + datatype step_result = Step of Ctree.state | Step_Failed of msg (*TODO: exn hierarchy*)
7.10 + ! not other returns, because lucin already does Step_Solve.add, so all is in Ctree.state.
7.11 \begin{itemize}
7.12 - \item Step_Specify: Specify/step-specify.sml in analogy to Interpret/...
7.13 + \item Step_Specify in Specify/step-specify.sml in analogy to Interpret/... TODO
7.14 \begin{itemize}
7.15 - \item Applicable.applicable_in --> Step_Specify.applicable
7.16 - \item Generate.generate1 --> Step_Specify.add
7.17 - \item xxx
7.18 + \item Step_Specify.check <-- Applicable.applicable_in
7.19 + \item Step_Specify.add <-- Generate.generate1
7.20 + \item Step_Specify.by_tactic : Tactic.input -> Ctree.state -> step_result
7.21 + \item Step_Specify.by_formula: ?term? -> Ctree.state -> step_result
7.22 + \item Step_Specify.find_next : Ctree.state -> step_result
7.23 \end{itemize}
7.24 - \item Step_Solve: Interpret/step-solve ? is there recurs.-vvvvvvvvvvvvv?
7.25 + \item Step_Solve in Interpret/step-solve.sml
7.26 \begin{itemize}
7.27 - \item Step_Solve.do <-- LucinNEW,do_solve_step
7.28 - ATTENTION: several uses of ---------------^^^^^^^^^^^^^ + recurs.! for Step_Solve.add
7.29 - \item Step_Solve.end_program <--? LucinNEW,begin_end_prog NOT separate ----------^^^^^^^
7.30 - \item Step_Solve.begin_program <-? LucinNEW,do_solve_step Apply_Method: ever used???
7.31 + \item Step_Solve.check <-- Applicable.applicable_in
7.32 + \item Step_Solve.add <-- Generate.generate1
7.33 + \item Step_Solve.by_tactic : Tactic.input -> Ctree.state -> step_result
7.34 + ^^^^LucinNEW,begin_end_prog
7.35 + \item Step_Solve.by_formula : term -> Ctree.state -> step_result
7.36 + \item Step_Solve.find_next : Ctree.state -> step_result
7.37 + ^^^^LucinNEW,do_solve_step; Apply_Method ever used???
7.38 \end{itemize}
7.39 - \item MathEngine/step.sml: Step.do calls Step_Solve.do | Step_Specify.do
7.40 - i.e. shift respective and other code from solve.sml to step.sml
7.41 + \item Step in MathEngine/step.sml
7.42 + \begin{itemize}
7.43 + \item Step.check : Step_Specify.check | Step_Solve.check depending on pos'
7.44 + \item Step.add : Step_Specify.add | Step_Solve.add depending on pos'
7.45 + \item Step.by_tactic : Step_Specify.by_tactic | Step_Solve.by_tactic depending on pos'
7.46 + \item Step.by_formula: Step_Specify.by_formula | Step_Solve.by_formula depending on pos'
7.47 + \item Step.find_next : Step_Specify.find_next | Step_Solve.find_next depending on pos'
7.48 + \end{itemize}
7.49 + \end{itemize}
7.50 \item xxx
7.51 \item MathEngBasic/calculation.sml
7.52 \begin{itemize}
7.53 @@ -108,7 +122,7 @@
7.54 \item xxx
7.55 \item xxx
7.56 \item decompose do_solve_step, begin_end_prog: mutual recursion only avoids multiple generate1
7.57 - ! ^^^ in determine_next_tactic --- ? ? ? in locate_input_tactic ?
7.58 + ! ^^^ in find_next_tactic --- ? ? ? in locate_input_tactic ?
7.59 \item xxx
7.60 \item Generate.generate1 thy is redundant: is the same during pbl, thus lookup spec
7.61 \item xxx
7.62 @@ -223,14 +237,14 @@
7.63 \item xxx
7.64 \end{itemize}
7.65 \item concentrate "insert_assumptions" for locate_input_tactic in "associate", ?OR? Tactic.insert_assumptions
7.66 - DONE for determine_next_tactic by Tactic.insert_assumptions m' ctxt
7.67 + DONE for find_next_tactic by Tactic.insert_assumptions m' ctxt
7.68 \begin{itemize}
7.69 \item rm from "generate1" ("Detail_Set_Inst'", Tactic.Detail_Set' ?)
7.70 \item shift from "applicable_in..Apply_Method" to ? ? ? (is ONLY use-case in appl.sml))
7.71 \item ?"insert_assumptions" necessary in "init_pstate" ?+++? in "applicable_in" ?+++? "associate"
7.72 \item xxx
7.73 \item xxx
7.74 - \item DO DELETIONS AFTER analogous concentrations in determine_next_tactic
7.75 + \item DO DELETIONS AFTER analogous concentrations in find_next_tactic
7.76 \end{itemize}
7.77 \item xxx
7.78 \item ? what is the difference headline <--> cascmd in
7.79 @@ -312,7 +326,7 @@
7.80 Note: replacement of Istate.safe by Istate.appy_ didn't care much about Telem.safe.
7.81 If Telem.safe is kept, consider merge with CTbasic.ostate
7.82 \item xxx
7.83 - \item remove determine_next_tactic from solve Apply_Method';
7.84 + \item remove find_next_tactic from solve Apply_Method';
7.85 this enforces Pos.at_first_tactic, which should be dropped, too.
7.86 \item xxx
7.87 \item xxx
7.88 @@ -361,7 +375,7 @@
7.89 text \<open>
7.90 unify to calcstate, calcstate', ?Ctree.state?
7.91 \begin{itemize}
7.92 - \item begin_end_prog Check_Postcond' needs NO 2.determine_next_tactic
7.93 + \item begin_end_prog Check_Postcond' needs NO 2.find_next_tactic
7.94 solve Check_Postcond' needs, because NO prog_result in Tactic.input
7.95 and applicable_in cannot get it.
7.96 \item xxx
8.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Wed Dec 18 11:02:32 2019 +0100
8.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Wed Dec 18 11:31:31 2019 +0100
8.3 @@ -9,7 +9,7 @@
8.4 "----------- Take as 1st stac in program -------------------------------------------------------";
8.5 "----------- re-build: fun locate_input_tactic -------------------------------------------------";
8.6 "----------- fun locate_input_tactic Helpless, but applicable ----------------------------------";
8.7 -"----------- re-build: fun determine_next_tactic -----------------------------------------------";
8.8 +"----------- re-build: fun find_next_tactic ----------------------------------------------------";
8.9 "----------- re-build: fun locate_input_formula ------------------------------------------------";
8.10 "-----------------------------------------------------------------------------------------------";
8.11 "-----------------------------------------------------------------------------------------------";
8.12 @@ -59,7 +59,7 @@
8.13
8.14 val NONE = (*case*) ini (*of*);
8.15 val Next_Step (is', ctxt', m') =
8.16 - LucinNEW.determine_next_tactic sc (pt, (p, Res)) is ctxt;
8.17 + LucinNEW.find_next_tactic sc (pt, (p, Res)) is ctxt;
8.18 (*+*)scrstate2str (the_pstate is') = "([\"\n(f_f, x ^^^ 2 + 1)\",\"\n(v_v, x)\"], [R,L,R], e_rls, NONE, \nIntegral x ^^^ 2 + 1 D x, ORundef, AppUndef_, false)";
8.19 val Safe_Step (_, _, Take' _) = (*case*)
8.20 locate_input_tactic sc (pt, (p, Res)) is' ctxt' m' (*of*);
8.21 @@ -351,9 +351,9 @@
8.22 then () else error "locate_input_tactic Helpless, but applicable CHANGED";
8.23
8.24
8.25 -"----------- re-build: fun determine_next_tactic -----------------------------------------------";
8.26 -"----------- re-build: fun determine_next_tactic -----------------------------------------------";
8.27 -"----------- re-build: fun determine_next_tactic -----------------------------------------------";
8.28 +"----------- re-build: fun find_next_tactic -----------------------------------------------";
8.29 +"----------- re-build: fun find_next_tactic -----------------------------------------------";
8.30 +"----------- re-build: fun find_next_tactic -----------------------------------------------";
8.31 (*//--------- exception Size raised (line 171 of "./basis/LibrarySupport.sml") ---------------\\
8.32 THIS CODE WORKS IN Test.Some.thy
8.33 ------------------------------------
8.34 @@ -389,8 +389,8 @@
8.35 val (_, (ist, ctxt), sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
8.36
8.37 (*NEW*) val Next_Step (_, _, Rewrite_Set' (_, _, Rls {id = "Test_simplify", ...}, _, _)) = (*case*)
8.38 -(*NEW*) determine_next_tactic sc (pt, pos) ist ctxt (*of*);
8.39 -"~~~~~ fun determine_next_tactic , args:"; val (Rule.Prog prog, ptp as (pt, (p, _)), Istate.Pstate ist, ctxt)
8.40 +(*NEW*) find_next_tactic sc (pt, pos) ist ctxt (*of*);
8.41 +"~~~~~ fun find_next_tactic , args:"; val (Rule.Prog prog, ptp as (pt, (p, _)), Istate.Pstate ist, ctxt)
8.42 = (sc, (pt, pos), ist, ctxt);
8.43 (*OLD* ) val Accept_Tac2 (m', ist as {act_arg, ...}, ctxt) =
8.44 (*OLD*) (*case*) scan_to_tactic2 (prog, (ptp, ctxt)) (Istate.Pstate ist) (*of*);
8.45 @@ -406,9 +406,9 @@
8.46 ( *OLD*)
8.47 (*NEW*) Next_Step (Istate.Pstate ist, Tactic.insert_assumptions tac ctxt, tac) (*return value*);
8.48 (*NEW*)
8.49 -"~~~~~ from fun determine_next_tactic\<longrightarrow>and do_solve_step , return:"; val (Next_Step (ist, ctxt, tac))
8.50 +"~~~~~ from fun find_next_tactic\<longrightarrow>and do_solve_step , return:"; val (Next_Step (ist, ctxt, tac))
8.51 = (Next_Step (Istate.Pstate ist, Tactic.insert_assumptions tac ctxt, tac));
8.52 -(*NEW* ) case determine_next_tactic sc (pt, pos) ist ctxt of
8.53 +(*NEW* ) case find_next_tactic sc (pt, pos) ist ctxt of
8.54 (*NEW*) Next_Step (ist, ctxt, tac) =>
8.55 ( *NEW*)
8.56 begin_end_prog tac (ist, Tactic.insert_assumptions tac ctxt) ptp;
8.57 @@ -461,14 +461,14 @@
8.58 val (res, asm) = (get_obj g_result pt (fst p));
8.59
8.60 if term2str res = "[x = 1]" andalso terms2str asm = "[\"precond_rootmet 1\"]"
8.61 -then () else error "re-build: fun determine_next_tactic CHANGED 1";
8.62 +then () else error "re-build: fun find_next_tactic CHANGED 1";
8.63
8.64 if p = ([], Und) (*.. should be ([], Res) *)
8.65 then
8.66 case get_obj g_tac pt (fst p) of
8.67 Apply_Method ["Test", "squ-equ-test-subpbl1"] => ((*ok, further tactics are level down*))
8.68 - | _ => error "re-build: fun determine_next_tactic CHANGED 3"
8.69 -else error "re-build: fun determine_next_tactic CHANGED 2";
8.70 + | _ => error "re-build: fun find_next_tactic CHANGED 3"
8.71 +else error "re-build: fun find_next_tactic CHANGED 2";
8.72 \\--------- exception Size raised (line 171 of "./basis/LibrarySupport.sml") ---------------//*)
8.73
8.74
9.1 --- a/test/Tools/isac/Knowledge/biegelinie-4.sml Wed Dec 18 11:02:32 2019 +0100
9.2 +++ b/test/Tools/isac/Knowledge/biegelinie-4.sml Wed Dec 18 11:31:31 2019 +0100
9.3 @@ -166,7 +166,7 @@
9.4 val ini = Lucin.init_form thy sc env;
9.5 val p = lev_dn p;
9.6 val NONE = (*case*) ini (*of*);
9.7 - val (m', (is', ctxt'), _) = determine_next_tactic sc (pt, (p, Res)) is ctxt;
9.8 + val (m', (is', ctxt'), _) = find_next_tactic sc (pt, (p, Res)) is ctxt;
9.9 val d = Rule.e_rls (*FIXME: get simplifier from domID*);
9.10 val Safe_Step ((pt', p'), _, _, _) = (*case*) locate_input_tactic sc (pt,(p, Res)) is' ctxt' m' (*of*);
9.11 Safe_Step : state * Istate.T * Proof.context * Tactic.T -> input_tactic_result;
10.1 --- a/test/Tools/isac/Knowledge/rateq.sml Wed Dec 18 11:02:32 2019 +0100
10.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Wed Dec 18 11:31:31 2019 +0100
10.3 @@ -103,7 +103,7 @@
10.4 "~~~~~ fun do_solve_step, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
10.5 val thy' = get_obj g_domID pt (par_pblobj pt p);
10.6 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)
10.7 -"~~~~~ fun determine_next_tactic, args:"; val () = ();
10.8 +"~~~~~ fun find_next_tactic, args:"; val () = ();
10.9 (*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* )
10.10 "~~~~~ fun go_scan_up2, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) =
10.11 (thy, ptp, sc, E, l, Skip_, a, v);
10.12 @@ -289,7 +289,7 @@
10.13 e_metID = get_obj g_metID pt (par_pblobj pt p); (* = false*)
10.14 val thy' = get_obj g_domID pt (par_pblobj pt p);
10.15 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
10.16 -"~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'),
10.17 +"~~~~~ fun find_next_tactic, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'),
10.18 (sc as Prog (h $ body)), (Pstate (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
10.19 (*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* )
10.20 l = []; (* = false*)
10.21 @@ -316,7 +316,7 @@
10.22 go_scan_up2 thy ptp scr E l ay a v;
10.23 scan_up2 thy ptp (Prog sc) E up ay (go up sc) a v;
10.24 go_scan_up2 thy ptp sc E l Skip_ a v;
10.25 -determine_next_tactic sc (pt,pos) is (*is as (ist, ctxt) ---> ist ctxt*);
10.26 +find_next_tactic sc (pt,pos) is (*is as (ist, ctxt) ---> ist ctxt*);
10.27 do_solve_step (pt,ip);
10.28 step p ((pt, e_pos'),[]);
10.29 *)
11.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Wed Dec 18 11:02:32 2019 +0100
11.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Wed Dec 18 11:31:31 2019 +0100
11.3 @@ -383,7 +383,7 @@
11.4 e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)
11.5 val thy' = get_obj g_domID pt (par_pblobj pt p);
11.6 val (srls, (ist, ctxt), sc) = from_pblobj_or_detail' thy' (p,p_) pt;
11.7 -val Next_Step (istate, ctxt, tac) = determine_next_tactic sc (pt,pos) ist ctxt; (*WAS Empty_Tac_: tac_*)
11.8 +val Next_Step (istate, ctxt, tac) = find_next_tactic sc (pt,pos) ist ctxt; (*WAS Empty_Tac_: tac_*)
11.9 case tac of Or_to_List' _ => ()
11.10 | _ => error "Or_to_List broken ?"
11.11
11.12 @@ -487,15 +487,15 @@
11.13 e_metID = get_obj g_metID pt (par_pblobj pt p) = false;
11.14 val thy' = get_obj g_domID pt (par_pblobj pt p);
11.15 val (srls, (ist, ctxt), sc) = from_pblobj_or_detail' thy' (p,p_) pt;
11.16 - val Next_Step (is, ctxt, tac_) = determine_next_tactic sc (pt,pos) ist ctxt;
11.17 + val Next_Step (is, ctxt, tac_) = find_next_tactic sc (pt,pos) ist ctxt;
11.18 (*tac_ = Rewrite' (..., ("rnorm_equation_add", "Test.rnorm_equation_add"), ...) !!!!!!!!!!!!!!!!*)
11.19
11.20 (*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* )
11.21 -"~~~~~ fun determine_next_tactic , args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'),
11.22 +"~~~~~ fun find_next_tactic , args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'),
11.23 (sc as Prog (h $ body)), (Pstate (ist as (E,l,rls,a,v,s,b)), ctxt)) = ((thy',srls), (pt,pos), sc, is);
11.24 l = [] = false;
11.25 go_scan_up2 thy ptp sc ist Skip_ (*--> Accept_Tac2 (Rewrite' (.., (.., "Test.rnorm_equation_add"), ...)
11.26 - BUT WE FIND IN THE CODE ABOVE IN determine_next_tactic:*)
11.27 + BUT WE FIND IN THE CODE ABOVE IN find_next_tactic:*)
11.28 ;
11.29 (*----------------------------------------------------------------------------------------------*)
11.30 if string_of_thmI @{thm rnorm_equation_add} = "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a + - 1 * ?b = 0)"
12.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Wed Dec 18 11:02:32 2019 +0100
12.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Wed Dec 18 11:31:31 2019 +0100
12.3 @@ -130,7 +130,7 @@
12.4 Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (* = false*);
12.5 val thy' = get_obj g_domID pt (par_pblobj pt p);
12.6 val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
12.7 -"~~~~~ fun determine_next_tactic , args:"; val ((ptp as(pt, (p, _))), (Rule.Prog prog), (Istate.Pstate ist, ctxt))
12.8 +"~~~~~ fun find_next_tactic , args:"; val ((ptp as(pt, (p, _))), (Rule.Prog prog), (Istate.Pstate ist, ctxt))
12.9 = ((pt, pos), sc, is);
12.10 (*case*) scan_to_tactic2 (prog, (ptp, ctxt)) (Istate.Pstate ist) (*of*);
12.11 "~~~~~ fun scan_to_tactic2 , args:"; val ((prog, cc), (Istate.Pstate (ist as {path, ...})))
13.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Wed Dec 18 11:02:32 2019 +0100
13.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Wed Dec 18 11:31:31 2019 +0100
13.3 @@ -104,8 +104,8 @@
13.4 val (_, (ist, ctxt), sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
13.5
13.6 val Next_Step (_, _, _) =
13.7 - (*case*) determine_next_tactic sc (pt, pos) ist ctxt (*of*);
13.8 -"~~~~~ fun determine_next_tactic , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), Istate.Pstate ist, ctxt)
13.9 + (*case*) find_next_tactic sc (pt, pos) ist ctxt (*of*);
13.10 +"~~~~~ fun find_next_tactic , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), Istate.Pstate ist, ctxt)
13.11 = (sc, (pt, pos), ist, ctxt);
13.12
13.13 val Accept_Tac2 (Rewrite_Set' _, _, _) = (*case*)
13.14 @@ -158,8 +158,8 @@
13.15 val (srls, (ist, ctxt), sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
13.16
13.17 val Next_Step (_, _, _) =
13.18 - (*case*) determine_next_tactic sc (pt, pos) ist ctxt (*of*);
13.19 -"~~~~~ fun determine_next_tactic , args:"; val (Rule.Prog prog, (ptp as(pt, (p, _))), Istate.Pstate ist, ctxt)
13.20 + (*case*) find_next_tactic sc (pt, pos) ist ctxt (*of*);
13.21 +"~~~~~ fun find_next_tactic , args:"; val (Rule.Prog prog, (ptp as(pt, (p, _))), Istate.Pstate ist, ctxt)
13.22 = (sc, (pt, pos), ist, ctxt);
13.23
13.24 val Accept_Tac2 (_, _, _) = (*case*)
14.1 --- a/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Wed Dec 18 11:02:32 2019 +0100
14.2 +++ b/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Wed Dec 18 11:31:31 2019 +0100
14.3 @@ -77,7 +77,7 @@
14.4 val thy' = get_obj g_domID pt (par_pblobj pt p);
14.5 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
14.6
14.7 -"~~~~~ fun determine_next_tactic , args:"; val ((thy, _), (ptp as (pt, (p, _))), sc, (Istate.Pstate ist, _(*ctxt*)))
14.8 +"~~~~~ fun find_next_tactic , args:"; val ((thy, _), (ptp as (pt, (p, _))), sc, (Istate.Pstate ist, _(*ctxt*)))
14.9 = ((thy',srls), (pt,pos), sc, is);
14.10
14.11 (*+*)val SOME t = parseNEW (get_ctxt pt pos) "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
15.1 --- a/test/Tools/isac/Minisubpbl/470-Check_elementwise-NEXT_STEP.sml Wed Dec 18 11:02:32 2019 +0100
15.2 +++ b/test/Tools/isac/Minisubpbl/470-Check_elementwise-NEXT_STEP.sml Wed Dec 18 11:31:31 2019 +0100
15.3 @@ -56,8 +56,8 @@
15.4 val thy' = get_obj g_domID pt (par_pblobj pt p);
15.5 val (srls, (ist, ctxt), sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
15.6
15.7 - determine_next_tactic sc (pt, pos) ist ctxt;
15.8 -"~~~~~ fun determine_next_tactic , args:"; val (Rule.Prog prog, (ptp as(pt, (p, _))), Istate.Pstate ist, ctxt)
15.9 + find_next_tactic sc (pt, pos) ist ctxt;
15.10 +"~~~~~ fun find_next_tactic , args:"; val (Rule.Prog prog, (ptp as(pt, (p, _))), Istate.Pstate ist, ctxt)
15.11 = (sc, (pt, pos), ist, ctxt);
15.12
15.13 (*case*) scan_to_tactic2 (prog, (ptp, ctxt)) (Istate.Pstate ist) (*of*);
16.1 --- a/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Wed Dec 18 11:02:32 2019 +0100
16.2 +++ b/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Wed Dec 18 11:31:31 2019 +0100
16.3 @@ -47,7 +47,7 @@
16.4 e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)
16.5 val thy' = get_obj g_domID pt (par_pblobj pt p);
16.6 val (srls, (ist, ctxt), sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)
16.7 -val End_Program (ist, tac) = determine_next_tactic sc (pt,pos) ist ctxt;
16.8 +val End_Program (ist, tac) = find_next_tactic sc (pt,pos) ist ctxt;
16.9
16.10 (*+*);tac; (* = Check_Postcond' *)
16.11
17.1 --- a/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Wed Dec 18 11:02:32 2019 +0100
17.2 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Wed Dec 18 11:31:31 2019 +0100
17.3 @@ -58,8 +58,8 @@
17.4 val (srls, (ist, ctxt), sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
17.5
17.6 val Next_Step (_, _, Check_elementwise' _) =
17.7 - (*case*) determine_next_tactic sc (pt, pos) ist ctxt (*of*);
17.8 -"~~~~~ fun determine_next_tactic , args:"; val ((Rule.Prog prog), (ptp as (pt, (p, _))), Istate.Pstate ist, ctxt)
17.9 + (*case*) find_next_tactic sc (pt, pos) ist ctxt (*of*);
17.10 +"~~~~~ fun find_next_tactic , args:"; val ((Rule.Prog prog), (ptp as (pt, (p, _))), Istate.Pstate ist, ctxt)
17.11 = (sc, (pt, pos), ist, ctxt);
17.12
17.13 (*case*)
18.1 --- a/test/Tools/isac/Minisubpbl/790-complete-NEXT_STEP.sml Wed Dec 18 11:02:32 2019 +0100
18.2 +++ b/test/Tools/isac/Minisubpbl/790-complete-NEXT_STEP.sml Wed Dec 18 11:31:31 2019 +0100
18.3 @@ -49,7 +49,7 @@
18.4 val (res, asm) = (get_obj g_result pt (fst p));
18.5
18.6 if term2str res = "[x = 1]" andalso terms2str asm = "[\"precond_rootmet 1\"]"
18.7 -then () else error "Minisubpbl/790-complete-NEXT_STEP.sml, determine_next_tactic CHANGED";
18.8 +then () else error "Minisubpbl/790-complete-NEXT_STEP.sml, find_next_tactic CHANGED";
18.9
18.10 if p = ([], Und)
18.11 then
19.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml Wed Dec 18 11:02:32 2019 +0100
19.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Wed Dec 18 11:31:31 2019 +0100
19.3 @@ -565,7 +565,7 @@
19.4 val Steps [(m',f',pt',p',c',s')] =
19.5 locate_input_tactic thy' m (pt,(p,p_)) (sc,d) is;
19.6 val is' = get_istate pt' p';
19.7 - determine_next_tactic thy' sc (pt'(*'*),p') is' (*as (ist, ctxt) ---> ist ctxt*);
19.8 + find_next_tactic thy' sc (pt'(*'*),p') is' (*as (ist, ctxt) ---> ist ctxt*);
19.9
19.10
19.11