1.1 --- a/src/Tools/isac/Build_Isac.thy Tue Mar 31 15:43:33 2020 +0200
1.2 +++ b/src/Tools/isac/Build_Isac.thy Wed Apr 01 10:24:13 2020 +0200
1.3 @@ -148,7 +148,7 @@
1.4 calcelems.sml:val depth = Unsynchronized.ref 99999;
1.5 calcelems.sml:val lim_rewrite = Unsynchronized.ref 99999;
1.6 calcelems.sml:val lim_deriv = Unsynchronized.ref 100;
1.7 - Interpret/script.sml:val trace_script = Unsynchronized.ref false;
1.8 + Interpret/script.sml:val trace_LI = Unsynchronized.ref false;
1.9 KEEP FOR EASIER DEVELOPMENT
1.10 calcelems.sml:val check_guhs_unique = Unsynchronized.ref true;
1.11 KEEP FOR DEMOS
2.1 --- a/src/Tools/isac/Interpret/li-tool.sml Tue Mar 31 15:43:33 2020 +0200
2.2 +++ b/src/Tools/isac/Interpret/li-tool.sml Wed Apr 01 10:24:13 2020 +0200
2.3 @@ -1,6 +1,8 @@
2.4 -(* Title: interpreter for scripts
2.5 +(* Title: Interpret/li-tool.sml
2.6 Author: Walther Neuper 2000
2.7 (c) due to copyright terms
2.8 +
2.9 +Tools for Lucas_Interpreter
2.10 *)
2.11
2.12 signature LUCAS_INTERPRETER_TOOL =
2.13 @@ -9,18 +11,17 @@
2.14 Associated of Tactic.T * term * Proof.context
2.15 | Ass_Weak of Tactic.T * term * Proof.context
2.16 | Not_Associated;
2.17 - val associate: Ctree.ctree -> Proof.context -> (Tactic.T * term) -> ass
2.18 + val associate: Ctree.ctree -> Proof.context -> (Tactic.T * term (*..Prog_Tac*)) -> ass
2.19
2.20 - val init_form : 'a -> Program.T -> (term * term) list -> term option
2.21 + val implicit_take : 'a -> Program.T -> (term * term) list -> term option
2.22 val init_pstate : Rule.rls -> Proof.context -> Model.itm list -> Celem.metID ->
2.23 Istate.T * Proof.context * Program.T
2.24
2.25 val get_simplifier : Calc.T -> Rule.rls
2.26 -(*vvv initialise : Rule.theory'(*?!?*) -> Calc.T -> (Istate.T * Proof.context) * Program.T*)
2.27 - val resume_prog : Rule.theory' -> Ctree.pos' -> Ctree.ctree ->
2.28 + val resume_prog : Rule.theory' (*..for lookup in KEStore*) -> Ctree.pos' -> Ctree.ctree ->
2.29 (Istate.T * Proof.context) * Program.T
2.30
2.31 - val tac_from_prog : Ctree.ctree -> theory -> term -> Tactic.input
2.32 + val tac_from_prog : Ctree.ctree -> theory (*..for lookup in KEStore*) -> term -> Tactic.input
2.33 val check_leaf : string -> Proof.context -> Rule.rls -> (Env.T * (term option * term)) -> term ->
2.34 Program.leaf * term option
2.35 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
2.36 @@ -31,7 +32,7 @@
2.37 end
2.38
2.39 (* traces the leaves (ie. non-tactical nodes) of Prog found by find_next_step, see "and scr" *)
2.40 -val trace_script = Unsynchronized.ref false; (* TODO: how are traces done in Isabelle? *)
2.41 +val trace_LI = Unsynchronized.ref false; (* TODO: how are traces done in Isabelle? *)
2.42
2.43 (**)
2.44 structure LItool(**): LUCAS_INTERPRETER_TOOL(**) =
2.45 @@ -42,11 +43,11 @@
2.46
2.47 (* determine the first tactic in case of a program with one argument (like simplification)
2.48 and without an initial Tactic.Take *)
2.49 -fun init_form thy (Rule.Prog prog) env =
2.50 +fun implicit_take thy (Rule.Prog prog) env =
2.51 (case Prog_Tac.get_first thy prog of
2.52 NONE => NONE
2.53 | SOME prog_tac => SOME (subst_atomic env prog_tac))
2.54 - | init_form _ _ _ = error "init_form: no match";
2.55 + | implicit_take _ _ _ = error "implicit_take: no match";
2.56
2.57 type dsc = typ; (* <-> nam..unknow in Descript.thy *)
2.58
2.59 @@ -102,29 +103,15 @@
2.60
2.61 datatype ass =
2.62 Associated of
2.63 - Tactic.T (* SubProblem gets args instantiated in associate *)
2.64 - * term (* for itr_arg, result in ets *)
2.65 - * Proof.context (* separate from Tactic.T like in locate_input_tactic *)
2.66 + Tactic.T (* Subproblem' gets args instantiated in associate *)
2.67 + * term (* resulting from application of Tactic.T *)
2.68 + * Proof.context (* updated by assumptioons from Rewrite* *)
2.69 | Ass_Weak of Tactic.T * term * Proof.context
2.70 | Not_Associated;
2.71
2.72 -(* check if tac_ is associated with stac.
2.73 - Note: this is the only fun in "fun locate_input_tactic", which handles tactics individually.
2.74 - Additional tasks:
2.75 - (1) to "Subproblem'" add "pors, hdl, fmz_, ctxt, f" TODO: ctxt <-?-> sig locate_input_tac
2.76 - (2) check if term t (the result has been calculated from) in tac_
2.77 - has been changed (see "datatype tac_"); if yes, recalculate result
2.78 - TODO.WN120106 recalculate impl.only for Substitute'
2.79 -args
2.80 - pt : ctree for pushing the thy specified in rootpbl into subpbls
2.81 - d : unused (planned for data for comparison)
2.82 - tac_ : from user (via applicable_in); to be compared with ...
2.83 - stac : found in program
2.84 -returns
2.85 - Associated : associated: e.g. thmID in stac = thmID in m
2.86 - +++ arg in stac = arg in m
2.87 - Ass_Weak: weakly ass.:e.g. thmID in stac = thmID in m, //arg//
2.88 - Not_Associated : e.g. thmID in stac/=/thmID in m (not =)
2.89 +(*
2.90 + associate is the ONLY code within by_tactic, which handles Tactic.T individually;
2.91 + thus it does ContextC.insert_assumptions in case of Rewrite*.
2.92 *)
2.93 fun associate _ ctxt (m as Tactic.Rewrite_Inst'
2.94 (_, _, _, _, _, thm'' as (thmID, _), f, (f', asms')), stac) =
2.95 @@ -253,7 +240,7 @@
2.96 else Not_Associated
2.97 | _ => raise ERROR ("associate: uncovered case"))
2.98 | associate _ _ (m, _) =
2.99 - (if (!trace_script)
2.100 + (if (!trace_LI)
2.101 then tracing("@@@ the 'tac_' proposed to apply does NOT match the leaf found in the script:\n"
2.102 ^ "@@@ tac_ = " ^ Tactic.string_of m)
2.103 else ();
2.104 @@ -302,7 +289,7 @@
2.105 "formals: " ^ Rule.terms2str formals ^ "\n" ^
2.106 "actuals: " ^ Rule.terms2str actuals
2.107 fun trace_init metID =
2.108 - if (!trace_script)
2.109 + if (!trace_LI)
2.110 then tracing("@@@ program " ^ strs2str metID)
2.111 else ();
2.112 in
2.113 @@ -365,8 +352,19 @@
2.114 Rule.Prog (Auto_Prog.gen (Celem.assoc_thy thy) (get_last_formula (pt, (p, p_))) rls'))
2.115 end
2.116
2.117 -(* handle a leaf at the end of recursive descent; a leaf is either a Prog_Tac or a Prog_Expr.
2.118 - TODO: what is a' ??? *)
2.119 +(*
2.120 + handle a leaf at the end of recursive descent; a leaf is either a Prog_Tac or a Prog_Expr.
2.121 + snd of return value is the formal arguments in case of currying.
2.122 +*)
2.123 +fun trace_msg_1 call t stac =
2.124 + if (! trace_LI) then
2.125 + tracing ("@@@ " ^ call ^ " leaf '" ^ Rule.term2str t ^ "' ---> Tac '" ^ Rule.term2str stac ^ "'")
2.126 + else ();
2.127 +fun trace_msg_2 call t lexpr' =
2.128 + if (! trace_LI) then
2.129 + tracing("@@@ " ^ call ^ " leaf '" ^ Rule.term2str t ^ "' ---> Expr '" ^ Rule.term2str lexpr' ^ "'")
2.130 + else ();
2.131 +
2.132 fun check_leaf call ctxt srls (E, (a, v)) t =
2.133 case Prog_Tac.eval_leaf E a v t of
2.134 (Program.Tac stac, a') =>
2.135 @@ -374,20 +372,14 @@
2.136 Rewrite.eval_prog_expr (Proof_Context.theory_of ctxt) srls
2.137 (subst_atomic (Env.update_opt E (a, v)) stac)
2.138 in
2.139 - (if (! trace_script)
2.140 - then tracing ("@@@ " ^ call ^ " leaf '" ^ Rule.term2str t ^ "' ---> Tac '" ^ Rule.term2str stac ^ "'")
2.141 - else ();
2.142 - (Program.Tac stac', a'))
2.143 + (trace_msg_1 call t stac; (Program.Tac stac', a'))
2.144 end
2.145 | (Program.Expr lexpr, a') =>
2.146 let val lexpr' =
2.147 Rewrite.eval_prog_expr (Proof_Context.theory_of ctxt) srls
2.148 (subst_atomic (Env.update_opt E (a, v)) lexpr)
2.149 in
2.150 - (if (! trace_script)
2.151 - then tracing("@@@ " ^ call ^ " leaf '" ^ Rule.term2str t ^ "' ---> Expr '" ^ Rule.term2str lexpr' ^ "'")
2.152 - else ();
2.153 - (Program.Expr lexpr', a'))
2.154 + (trace_msg_2 call t lexpr'; (Program.Expr lexpr', a'))
2.155 end;
2.156
2.157 (**)end(**)
3.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Tue Mar 31 15:43:33 2020 +0200
3.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Apr 01 10:24:13 2020 +0200
3.3 @@ -491,7 +491,7 @@
3.4 then Safe_Step (Pstate ist, ctxt, tac')
3.5 else Unsafe_Step (Pstate ist, ctxt, tac')
3.6 | Reject_Tac1 _ => Not_Locatable (Tactic.string_of tac ^ " not locatable")
3.7 - | err => raise ERROR ("not-found-in-script: NotLocatable from " ^ @{make_string} err))
3.8 + | err => raise ERROR ("not-found-in-program: NotLocatable from " ^ @{make_string} err))
3.9 | locate_input_tactic _ _ _ _ _ = raise ERROR "locate_input_tactic: uncovered case in definition"
3.10
3.11
3.12 @@ -511,7 +511,7 @@
3.13 val (is, env, ctxt, prog) = case LItool.init_pstate srls ctxt itms mI of
3.14 (is as Pstate {env, ...}, ctxt, scr) => (is, env, ctxt, scr)
3.15 | _ => error "LI.by_tactic Apply_Method': uncovered case init_pstate"
3.16 - val ini = LItool.init_form (Celem.assoc_thy (get_obj g_domID pt p)) prog env;
3.17 + val ini = LItool.implicit_take (Celem.assoc_thy (get_obj g_domID pt p)) prog env;
3.18 val pos = start_new_level pos
3.19 in
3.20 case ini of
4.1 --- a/src/Tools/isac/Interpret/step-solve.sml Tue Mar 31 15:43:33 2020 +0200
4.2 +++ b/src/Tools/isac/Interpret/step-solve.sml Wed Apr 01 10:24:13 2020 +0200
4.3 @@ -76,7 +76,7 @@
4.4 let
4.5 val (p,ps, _, pt) = Generate.generate_hard (Celem.assoc_thy "Isac_Knowledge") m (p, p_) pt;
4.6 in
4.7 - ("not-found-in-script", ([(Tactic.input_from_T m, m, (po, is))], ps, (pt, p)))
4.8 + ("not-found-in-program", ([(Tactic.input_from_T m, m, (po, is))], ps, (pt, p)))
4.9 end
4.10 end;
4.11
5.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml Tue Mar 31 15:43:33 2020 +0200
5.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml Wed Apr 01 10:24:13 2020 +0200
5.3 @@ -225,7 +225,7 @@
5.4 the tree's structure has been copied from an early version of Theorema(c);
5.5 it has the disadvantage, that there is no space
5.6 for the first tactic in a script generating the first formula at (p,Frm);
5.7 - this trouble has been covered by 'init_form' and 'Take' so far,
5.8 + this trouble has been covered by 'implicit_take' and 'Take' so far,
5.9 but it is crucial if the first tactic in a script is eg. 'Subproblem';
5.10 see 'type tac', Apply_Method.
5.11 *)
6.1 --- a/src/Tools/isac/MathEngBasic/tactic-def.sml Tue Mar 31 15:43:33 2020 +0200
6.2 +++ b/src/Tools/isac/MathEngBasic/tactic-def.sml Wed Apr 01 10:24:13 2020 +0200
6.3 @@ -126,11 +126,11 @@
6.4 Add_Find of Rule.cterm' | Add_Given of Rule.cterm' | Add_Relation of Rule.cterm'
6.5 | Apply_Assumption of Rule.cterm' list
6.6 | Apply_Method of Celem.metID
6.7 - (* creates an "istate" in PblObj.env; in case of "init_form"
6.8 + (* creates an "istate" in PblObj.env; in case of "implicit_take"
6.9 creates a formula at ((lev_on o lev_dn) p, Frm) and in this "ppobj.loc"
6.10 a "SOME istate" at fst of "loc".
6.11 As each step (in the solve-phase) has a resulting formula (at the front-end)
6.12 - Apply_Method also does the 1st step in the script (an "initac") if there is no "init_form" *)
6.13 + Apply_Method also does the 1st step in the script (an "initac") if there is no "implicit_take" *)
6.14 (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
6.15 | Begin_Sequ | Begin_Trans
6.16 | Split_And | Split_Or | Split_Intersect
7.1 --- a/src/Tools/isac/ProgLang/Prog_Tac.thy Tue Mar 31 15:43:33 2020 +0200
7.2 +++ b/src/Tools/isac/ProgLang/Prog_Tac.thy Wed Apr 01 10:24:13 2020 +0200
7.3 @@ -79,7 +79,7 @@
7.4 m |> HOLogic.dest_list |> map HOLogic.dest_string) : Celem.spec
7.5 | dest_spec t = raise TERM ("dest_spec: called with ", [t])
7.6
7.7 -(* get argument of first Prog_Tac in a progam for init_form *)
7.8 +(* get argument of first Prog_Tac in a progam for implicit_take *)
7.9 fun get_first thy (_ $ body) =
7.10 let
7.11 (* entries occur twice, for form curried by #> or non-curried *)
8.1 --- a/src/Tools/isac/TODO.thy Tue Mar 31 15:43:33 2020 +0200
8.2 +++ b/src/Tools/isac/TODO.thy Wed Apr 01 10:24:13 2020 +0200
8.3 @@ -48,17 +48,9 @@
8.4 \item xxx
8.5 \item xxx
8.6 \item in check_leaf SEPARATE tracing
8.7 - collect all trace_script --> Trace_LI
8.8 - trace_script: replace ' by " in writeln
8.9 + collect all trace_LI --> Trace_LI
8.10 + trace_LI: replace ' by " in writeln
8.11 \item xxx
8.12 - \item renamings
8.13 - \begin{itemize}
8.14 - \item xxx
8.15 - \item xxx
8.16 - \item rename field scr in meth
8.17 - \item xxx
8.18 - \item xxx
8.19 - \end{itemize}
8.20 \item xxx
8.21 \item relocations + renamings
8.22 \begin{itemize}
8.23 @@ -138,8 +130,10 @@
8.24 \item TermC.list2isalist: typ -> term list -> term .. should NOT requires typ
8.25 \item get_ctxt_LI should replace get_ctxt
8.26 \item ALL CODE: rename spec(ification) --> know(ledge), in Specification: Relation -> Knowledge
8.27 - \item rename Base_Tool.thy <--- Base_Tools
8.28 - \item adopt naming conventions in Knowledge: EqSystem --> Equation_System, etc
8.29 + \item rename Base_Tool.thy <--- Base_Tools
8.30 + \item adopt naming conventions in Knowledge: EqSystem --> Equation_System, etc
8.31 + \item rename field scr in meth
8.32 + \item xxx
8.33 \item xxx
8.34 \item xxx
8.35 \item cleanup fun me:
8.36 @@ -255,7 +249,7 @@
8.37 \item automatically extrac rls from program-code
8.38 ? take ["SignalProcessing", "Z_Transform", "Inverse_sub"] as an example ?
8.39 \item xxx
8.40 - \item finish output of trace_script with Check_Postcond (useful for SubProblem)
8.41 + \item finish output of trace_LI with Check_Postcond (useful for SubProblem)
8.42 \item xxx
8.43 \item xxx
8.44 \item xxx
9.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Tue Mar 31 15:43:33 2020 +0200
9.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Wed Apr 01 10:24:13 2020 +0200
9.3 @@ -1243,7 +1243,7 @@
9.4
9.5 ML \<open>
9.6 trace_rewrite := false; (*true*)
9.7 - trace_script := false; (*true*)
9.8 + trace_LI := false; (*true*)
9.9 print_depth 9;
9.10
9.11 val fmz =
9.12 @@ -1492,7 +1492,7 @@
9.13 \<close>
9.14
9.15 ML \<open>
9.16 -trace_script := true;
9.17 +trace_LI := true;
9.18 \<close>
9.19 ML \<open>
9.20 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
10.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Tue Mar 31 15:43:33 2020 +0200
10.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Wed Apr 01 10:24:13 2020 +0200
10.3 @@ -26,7 +26,7 @@
10.4 "--------- locate_input_term [rational,simplification] ----------------------";
10.5 "--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
10.6 "--------- Take as 1st tac, start from exp -----------------------";
10.7 -"--------- init_form, start with <NEW> (CAS input) ---------------";
10.8 +"--------- implicit_take, start with <NEW> (CAS input) ---------------";
10.9 "--------- build fun check_err_patt ------------------------------";
10.10 "--------- build fun check_err_patt ?bdv -------------------------";
10.11 "--------- build fun Error_Pattern.check_for ------------------------";
10.12 @@ -732,9 +732,9 @@
10.13 else error "diff.sml Diff (x^2 + x + 1, x) from exp";
10.14 DEconstrCalcTree 1;
10.15
10.16 -"--------- init_form, start with <NEW> (CAS input) ---------------";
10.17 -"--------- init_form, start with <NEW> (CAS input) ---------------";
10.18 -"--------- init_form, start with <NEW> (CAS input) ---------------";
10.19 +"--------- implicit_take, start with <NEW> (CAS input) ---------------";
10.20 +"--------- implicit_take, start with <NEW> (CAS input) ---------------";
10.21 +"--------- implicit_take, start with <NEW> (CAS input) ---------------";
10.22 reset_states ();
10.23 CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
10.24 (*[[from sml: > @@@@@begin@@@@@
11.1 --- a/test/Tools/isac/Interpret/li-tool.sml Tue Mar 31 15:43:33 2020 +0200
11.2 +++ b/test/Tools/isac/Interpret/li-tool.sml Wed Apr 01 10:24:13 2020 +0200
11.3 @@ -6,7 +6,7 @@
11.4 "table of contents -----------------------------------------------";
11.5 "-----------------------------------------------------------------";
11.6 "----------- fun specific_from_prog ----------------------------";
11.7 -"----------- fun init_form, fun get_first -------------------------";
11.8 +"----------- fun implicit_take, fun get_first -------------------------";
11.9 "----------- fun from_prog ---------------------------------------";
11.10 "----------- fun specific_from_prog ----------------------------";
11.11 "----------- fun de_esc_underscore -------------------------------";
11.12 @@ -44,8 +44,8 @@
11.13 else error "script.sml fun specific_from_prog diff.behav. 2"
11.14 | _ => error "script.sml fun specific_from_prog diff.behav. 1";
11.15
11.16 -trace_script := true;
11.17 -trace_script := false;
11.18 +trace_LI := true;
11.19 +trace_LI := false;
11.20 applyTactic 1 p (hd appltacs);
11.21 val ((pt, p), _) = get_calc 1; show_pt pt;
11.22 val appltacs = specific_from_prog pt p;
11.23 @@ -88,9 +88,9 @@
11.24 autoCalculate 1 CompleteCalc; (* ONE ERROR *)
11.25 ==============================^^^^^^^^^^^^^*)
11.26
11.27 -"----------- fun init_form, fun get_first -------------------------";
11.28 -"----------- fun init_form, fun get_first -------------------------";
11.29 -"----------- fun init_form, fun get_first -------------------------";
11.30 +"----------- fun implicit_take, fun get_first -------------------------";
11.31 +"----------- fun implicit_take, fun get_first -------------------------";
11.32 +"----------- fun implicit_take, fun get_first -------------------------";
11.33 val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
11.34 val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"],
11.35 ["Test","squ-equ-test-subpbl1"]);
11.36 @@ -115,8 +115,8 @@
11.37 val thy = assoc_thy thy';
11.38 val srls = LItool.get_simplifier (pt, pos)
11.39 val (is as Pstate {env, ...}, ctxt, sc) = init_pstate srls ctxt itms mI;
11.40 -val ini = init_form thy sc env;
11.41 -"----- fun init_form, args:"; val (Prog sc) = sc;
11.42 +val ini = implicit_take thy sc env;
11.43 +"----- fun implicit_take, args:"; val (Prog sc) = sc;
11.44 "----- fun get_first, args:"; val (y, h $ body) = (thy, sc);
11.45 case get_first thy sc of SOME (Free ("e_e", _)) => ()
11.46 | _ => error "script: Const (?, ?) in script (as term) changed";;
12.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Tue Mar 31 15:43:33 2020 +0200
12.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Wed Apr 01 10:24:13 2020 +0200
12.3 @@ -54,7 +54,7 @@
12.4 (is as Istate.Pstate {env, ...}, ctxt, sc) => (is, env, ctxt, sc)
12.5 | _ => error "solve Apply_Method: uncovered case init_pstate";
12.6 (*+*)pstate2str (the_pstate is) = "([\"\n(f_f, x ^^^ 2 + 1)\",\"\n(v_v, x)\"], [], e_rls, NONE, \n??.empty, ORundef, false, true)";
12.7 - val ini = LItool.init_form thy sc env;
12.8 + val ini = LItool.implicit_take thy sc env;
12.9 val p = lev_dn p;
12.10
12.11 val NONE = (*case*) ini (*of*);
13.1 --- a/test/Tools/isac/Knowledge/biegelinie-4.sml Tue Mar 31 15:43:33 2020 +0200
13.2 +++ b/test/Tools/isac/Knowledge/biegelinie-4.sml Wed Apr 01 10:24:13 2020 +0200
13.3 @@ -162,7 +162,7 @@
13.4 val (is, env, ctxt, sc) = case LItool.init_pstate srls ctxt itms mI of
13.5 (is as Istate.Pstate ist, ctxt, sc) => (is, get_env ist, ctxt, sc)
13.6 | _ => error "Step_Solve.by_tactic Apply_Method: uncovered case init_pstate"
13.7 - val ini = LItool.init_form thy sc env;
13.8 + val ini = LItool.implicit_take thy sc env;
13.9 val p = lev_dn p;
13.10 val NONE = (*case*) ini (*of*);
13.11 val (m', (is', ctxt'), _) = LI.find_next_step sc (pt, (p, Res)) is ctxt;
14.1 --- a/test/Tools/isac/Knowledge/diff.sml Tue Mar 31 15:43:33 2020 +0200
14.2 +++ b/test/Tools/isac/Knowledge/diff.sml Wed Apr 01 10:24:13 2020 +0200
14.3 @@ -327,7 +327,7 @@
14.4 moveActiveRoot 1;
14.5 autoCalculate 1 CompleteCalc;
14.6 (* trace_rewrite := true;
14.7 - trace_script := false;
14.8 + trace_LI := false;
14.9 *)
14.10 val ((pt,p),_) = get_calc 1; show_pt pt;
14.11
14.12 @@ -347,11 +347,11 @@
14.13 Iterator 1;
14.14 moveActiveRoot 1;
14.15 (* trace_rewrite := true;
14.16 - trace_script := true;
14.17 + trace_LI := true;
14.18 *)
14.19 autoCalculate 1 CompleteCalc;
14.20 (* trace_rewrite := false;
14.21 - trace_script := false;
14.22 + trace_LI := false;
14.23 *)
14.24 val ((pt,p),_) = get_calc 1; show_pt pt;
14.25 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "8 * x ^^^ 7"
15.1 --- a/test/Tools/isac/Knowledge/diffapp.sml Tue Mar 31 15:43:33 2020 +0200
15.2 +++ b/test/Tools/isac/Knowledge/diffapp.sml Wed Apr 01 10:24:13 2020 +0200
15.3 @@ -303,7 +303,7 @@
15.4 val (p,_,f,nxt,_,pt) = me nxt p c pt;
15.5 === inhibit exn 110722=============================================================*)
15.6
15.7 -(*since 0508 Apply_Method does the 1st step, if NONE init_form -------------
15.8 +(*since 0508 Apply_Method does the 1st step, if NONE implicit_take -------------
15.9 (*val nxt = ("Subproblem",Subproblem ("DiffApp",["make","function"]))*)
15.10 val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => print_exn_G e;
15.11 (*val nxt = ("Refine_Tacitly",Refine_Tacitly ["make","function"])*)
16.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Tue Mar 31 15:43:33 2020 +0200
16.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Wed Apr 01 10:24:13 2020 +0200
16.3 @@ -653,7 +653,7 @@
16.4 ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))];
16.5 moveActiveRoot 1;
16.6 (*
16.7 -trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
16.8 +trace_LI := true; autoCalculate 1 CompleteCalc; trace_LI := false;
16.9 ##7.27## ordered substs
16.10 c_4 c_2
16.11 c c_2 c_3 c_4 c c_2 1->2: c
16.12 @@ -698,7 +698,7 @@
16.13 ["Biegelinien", "AusMomentenlinie"]))];
16.14 (*
16.15 moveActiveRoot 1;
16.16 -trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
16.17 +trace_LI := true; autoCalculate 1 CompleteCalc; trace_LI := false;
16.18 *)
16.19
16.20 "------- Bsp 7.69";
16.21 @@ -709,7 +709,7 @@
16.22 ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))];
16.23 moveActiveRoot 1;
16.24 (*
16.25 -trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
16.26 +trace_LI := true; autoCalculate 1 CompleteCalc; trace_LI := false;
16.27 ##7.69## ordered subst 2x2
16.28 c_4 c_3
16.29 c c_2 c_3 c_4 c c_2 c_3 1:c_3 -> 2:c c_2 2: c c_2
16.30 @@ -729,7 +729,7 @@
16.31 ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"] ))];
16.32 moveActiveRoot 1;
16.33 (*
16.34 -trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
16.35 +trace_LI := true; autoCalculate 1 CompleteCalc; trace_LI := false;
16.36 ##7.70## |subst
16.37 c |
16.38 c c_2 |1:c -> 2:c_2
16.39 @@ -846,7 +846,7 @@
16.40 ["IntegrierenUndKonstanteBestimmen2"] ))];
16.41 moveActiveRoot 1;
16.42 (*
16.43 -trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
16.44 +trace_LI := true; autoCalculate 1 CompleteCalc; trace_LI := false;
16.45 ##7.71## |ordered |subst.singles (recurs) |2x2 |diagonal
16.46 c c_2 |c c_2 |1' |1': c c_2 |
16.47 c_4 | c_3 |2:c_3 -> 4' :c c_2 c_4 | |
16.48 @@ -868,7 +868,7 @@
16.49 ["Biegelinien", "AusMomentenlinie"]))];
16.50 moveActiveRoot 1;
16.51 (*
16.52 -trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
16.53 +trace_LI := true; autoCalculate 1 CompleteCalc; trace_LI := false;
16.54 *)
16.55
16.56 "------- Bsp 7.72b";
16.57 @@ -881,7 +881,7 @@
16.58 ["IntegrierenUndKonstanteBestimmen2"] ))];
16.59 moveActiveRoot 1;
16.60 (*
16.61 -trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
16.62 +trace_LI := true; autoCalculate 1 CompleteCalc; trace_LI := false;
16.63 ##7.72b## |ord. |subst.singles |ord.triang.
16.64 c_2 | | |c_2
16.65 c c_2 | |1:c_2 -> 2':c |c_2 c
16.66 @@ -902,7 +902,7 @@
16.67 ["Biegelinien", "AusMomentenlinie"]))];
16.68 moveActiveRoot 1;
16.69 (*
16.70 -trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
16.71 +trace_LI := true; autoCalculate 1 CompleteCalc; trace_LI := false;
16.72 *)
16.73
16.74 "----------- 4x4 systems from Biegelinie -------------------------";
17.1 --- a/test/Tools/isac/Knowledge/partial_fractions.sml Tue Mar 31 15:43:33 2020 +0200
17.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml Wed Apr 01 10:24:13 2020 +0200
17.3 @@ -70,7 +70,7 @@
17.4 member op = [Pbl,Met] p_; " = false";
17.5 (* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ leads into
17.6 Step_Solve.do_next, which is definitely WRONG (should be nxt_specify_ for FIND_ADD).
17.7 -This ERROR seems to be introduced together with ctxt, concerns Apply_Method without init_form.
17.8 +This ERROR seems to be introduced together with ctxt, concerns Apply_Method without implicit_take.
17.9 See TODO.txt
17.10 *)
17.11
17.12 @@ -426,7 +426,7 @@
17.13 exception Empty raised (line 429 of "library.ML") TODO during lucin: *)
17.14
17.15 (*
17.16 -trace_script := true;
17.17 +trace_LI := true;
17.18
17.19 @@@ program ["simplification","of_rationals","to_partial_fraction"]
17.20 @@@ istate ["
18.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Tue Mar 31 15:43:33 2020 +0200
18.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Wed Apr 01 10:24:13 2020 +0200
18.3 @@ -198,17 +198,17 @@
18.4 (*TODO simplify assumptions (sqrt!) and check ERROR in has_degree_in*);
18.5 (*if*) Tactic.for_specify' m; (*false*)
18.6 (*loc_solve_ (mI,m) ptp;
18.7 - WAS: not-found-in-script: NotLocatable from Term_Val1 (Const ("List...*)
18.8 + WAS: not-found-in-program: NotLocatable from Term_Val1 (Const ("List...*)
18.9 "~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = (m, ptp);
18.10 (*solve m (pt, pos);
18.11 - WAS: not-found-in-script: NotLocatable from Term_Val1 (Const ("List...*)
18.12 + WAS: not-found-in-program: NotLocatable from Term_Val1 (Const ("List...*)
18.13 "~~~~~ fun Step_Solve.by_tactic , args:"; val (m, (pt, po as (p,p_))) = (m, (pt, pos));
18.14 e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*);
18.15 val thy' = get_obj g_domID pt (par_pblobj pt p);
18.16 val (is, sc) = resume_prog thy' (p,p_) pt;
18.17 val d = e_rls;
18.18 (*locate_input_tactic (thy',srls) m (pt,(p,p_)) (sc,d) is;
18.19 - WAS: not-found-in-script: NotLocatable from Term_Val1 (Const ("List...*)
18.20 + WAS: not-found-in-program: NotLocatable from Term_Val1 (Const ("List...*)
18.21 "~~~~~ fun locate_input_tactic, args:"; val () = ();
18.22 (*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* )
18.23 l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*false*);
19.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Tue Mar 31 15:43:33 2020 +0200
19.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Wed Apr 01 10:24:13 2020 +0200
19.3 @@ -98,7 +98,7 @@
19.4 val ctxt = ctxt |> ContextC.insert_assumptions pres;
19.5
19.6 "~~~~~ continue Step_Solve.by_tactic";
19.7 -val ini = init_form thy sc'''' env'''';
19.8 +val ini = implicit_take thy sc'''' env'''';
19.9 val p = lev_dn p;
19.10 val SOME t = ini;
19.11 val (pos,c,_,pt) =
20.1 --- a/test/Tools/isac/Test_Isac.thy Tue Mar 31 15:43:33 2020 +0200
20.2 +++ b/test/Tools/isac/Test_Isac.thy Wed Apr 01 10:24:13 2020 +0200
20.3 @@ -521,7 +521,7 @@
20.4 --------------------------------------------------------------------------------
20.5 WN111013.TODO: lots of cleanup/removal in test/../Test.thy
20.6 --------------------------------------------------------------------------------
20.7 - WN111013.TODO: remove concept around "fun init_form", lots of troubles with
20.8 + WN111013.TODO: remove concept around "fun implicit_take", lots of troubles with
20.9 this special case (see) --- why not nxt = Model_Problem here ? ---
20.10 --------------------------------------------------------------------------------
20.11 WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat, see test/
21.1 --- a/test/Tools/isac/Test_Isac_Short.thy Tue Mar 31 15:43:33 2020 +0200
21.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Wed Apr 01 10:24:13 2020 +0200
21.3 @@ -521,7 +521,7 @@
21.4 --------------------------------------------------------------------------------
21.5 WN111013.TODO: lots of cleanup/removal in test/../Test.thy
21.6 --------------------------------------------------------------------------------
21.7 - WN111013.TODO: remove concept around "fun init_form", lots of troubles with
21.8 + WN111013.TODO: remove concept around "fun implicit_take", lots of troubles with
21.9 this special case (see) --- why not nxt = Model_Problem here ? ---
21.10 --------------------------------------------------------------------------------
21.11 WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat, see test/