1.1 --- a/src/Tools/isac/Interpret/derive.sml Tue Aug 16 15:53:20 2022 +0200
1.2 +++ b/src/Tools/isac/Interpret/derive.sml Sun Aug 21 11:22:04 2022 +0200
1.3 @@ -121,8 +121,8 @@
1.4 fun derivat ([]:(term * Rule.rule * (term * term list)) list) = TermC.empty
1.5 | derivat dt = (#1 o #3 o last_elem) dt
1.6 fun equal (_, _, (t1, _)) (_, _, (t2, _)) = t1 = t2
1.7 - val fod = do_one (** )ctxt( *HACK*)(Proof_Context.init_global (ThyC.Isac()))(*ctxt*) erls rules (snd rew_ord) NONE fo
1.8 - val ifod = do_one (** )ctxt( *HACK*)(Proof_Context.init_global (ThyC.Isac()))(*ctxt*) erls rules (snd rew_ord) NONE ifo
1.9 + val fod = do_one (**)ctxt(*HACK* )(Proof_Context.init_global (ThyC.Isac()))( *ctxt*) erls rules (snd rew_ord) NONE fo
1.10 + val ifod = do_one (**)ctxt(*HACK* )(Proof_Context.init_global (ThyC.Isac()))( *ctxt*) erls rules (snd rew_ord) NONE ifo
1.11 in
1.12 case (fod, ifod) of
1.13 ([], []) => if fo = ifo then (true, []) else (false, [])
2.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Tue Aug 16 15:53:20 2022 +0200
2.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Sun Aug 21 11:22:04 2022 +0200
2.3 @@ -630,15 +630,20 @@
2.4 then ("no derivation found", (tacis, c, ptp): Calc.state_post)
2.5 else
2.6 let
2.7 - val msg_cs' as (_, (tacis, c', ptp)) = do_next ptp; (*<---------------------*)
2.8 + val msg_cs' as (_, (tacis, c', ptp)) = (*LI.*)do_next ptp; (*<---------------------*)
2.9 val (_, (tacis, c'', ptp)) = case tacis of
2.10 ((Tactic.Subproblem _, _, _) :: _) =>
2.11 let
2.12 - val ptp as (pt, (p, _)) = Specify.do_all ptp (*<--------------------*)
2.13 - val mI = Ctree.get_obj Ctree.g_metID pt p
2.14 + val ptp as (pt, pos as (p, _)) = Specify.do_all ptp (*<--------------------*)
2.15 + val mI = Ctree.get_obj Ctree.g_metID pt p
2.16 +(*ctxt*)val (ist, ctxt) = (Istate.empty, Ctree.get_ctxt pt pos)(*ctxt*)
2.17 in
2.18 +(*ctxt* )
2.19 by_tactic (Tactic.Apply_Method' (mI, NONE, empty, ContextC.empty))
2.20 (empty, ContextC.empty) ptp
2.21 +( *ctxt*)
2.22 + by_tactic (Tactic.Apply_Method' (mI, NONE, ist, ctxt)) (ist, ctxt) ptp
2.23 +(*ctxt*)
2.24 end
2.25 | _ => msg_cs';
2.26 in compare_step (tacis, c @ c' @ c'', ptp) ifo end
3.1 --- a/src/Tools/isac/Interpret/solve-step.sml Tue Aug 16 15:53:20 2022 +0200
3.2 +++ b/src/Tools/isac/Interpret/solve-step.sml Sun Aug 21 11:22:04 2022 +0200
3.3 @@ -150,15 +150,15 @@
3.4 | check (Tactic.Rewrite_Inst (subs, thm)) (cs as (pt, pos as (p, _))) =
3.5 let
3.6 val pp = Ctree.par_pblobj pt p;
3.7 -(*ctxt*)
3.8 +(*ctxt* )
3.9 val thy' = Ctree.get_obj Ctree.g_domID pt pp;
3.10 val thy = ThyC.get_theory thy';
3.11 val ctxt = Proof_Context.init_global thy;
3.12 -(*ctxt* )
3.13 +( *ctxt*)
3.14 val ctxt = Ctree.get_loc pt pos |> snd
3.15 val thy = Proof_Context.theory_of ctxt
3.16 val thy' = Context.theory_name thy
3.17 -( *ctxt*)
3.18 +(*ctxt*)
3.19 val {rew_ord' = ro', erls = erls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt pp);
3.20 val f = Calc.current_formula cs;
3.21 val subst = Subst.T_from_input ctxt subs; (*TODO: input requires parse _: _ -> _ option*)
3.22 @@ -170,14 +170,14 @@
3.23 end
3.24 | check (Tactic.Rewrite_Set rls) (cs as (pt, pos as (p, _))) =
3.25 let
3.26 -(*ctxt*)
3.27 +(*ctxt* )
3.28 val pp = Ctree.par_pblobj pt p;
3.29 val thy' = Ctree.get_obj Ctree.g_domID pt pp;
3.30 -(*ctxt* )
3.31 +( *ctxt*)
3.32 val ctxt = Ctree.get_loc pt pos |> snd
3.33 val thy = Proof_Context.theory_of ctxt
3.34 val thy' = Context.theory_name thy
3.35 -( *ctxt*)
3.36 +(*ctxt*)
3.37 val f = Calc.current_formula cs;
3.38 in
3.39 case Rewrite.rewrite_set_ (ThyC.id_to_ctxt thy') false (assoc_rls rls) f of
3.40 @@ -187,16 +187,16 @@
3.41 end
3.42 | check (Tactic.Rewrite_Set_Inst (subs, rls)) (cs as (pt, pos as (p, _))) =
3.43 let
3.44 -(*ctxt*)
3.45 +(*ctxt* )
3.46 val pp = Ctree.par_pblobj pt p;
3.47 val thy' = Ctree.get_obj Ctree.g_domID pt pp;
3.48 val thy = ThyC.get_theory thy';
3.49 val ctxt = Proof_Context.init_global thy;
3.50 -(*ctxt* )
3.51 +( *ctxt*)
3.52 val ctxt = Ctree.get_loc pt pos |> snd
3.53 val thy = Proof_Context.theory_of ctxt
3.54 val thy' = Context.theory_name thy
3.55 -( *ctxt*)
3.56 +(*ctxt*)
3.57 val f = Calc.current_formula cs;
3.58 val subst = Subst.T_from_input ctxt subs; (*TODO: input requires parse _: _ -> _ option*)
3.59 in
3.60 @@ -211,14 +211,14 @@
3.61 | check (Tactic.Substitute sube) (cs as (pt, pos as (p, _))) =
3.62 let
3.63 val pp = Ctree.par_pblobj pt p
3.64 -(*ctxt*)
3.65 +(*ctxt* )
3.66 val thy = ThyC.get_theory (Ctree.get_obj Ctree.g_domID pt pp)
3.67 val ctxt = Proof_Context.init_global thy;
3.68 -(*ctxt* )
3.69 +( *ctxt*)
3.70 val ctxt = Ctree.get_loc pt pos |> snd
3.71 val thy = Proof_Context.theory_of ctxt
3.72 val thy' = Context.theory_name thy
3.73 -( *ctxt*)
3.74 +(*ctxt*)
3.75 val f = Calc.current_formula cs;
3.76 val {rew_ord', erls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt pp)
3.77 val subte = Subst.input_to_terms sube (*TODO: input requires parse _: _ -> _ option*)
3.78 @@ -237,17 +237,17 @@
3.79 SOME (f', _) => Applicable.Yes (Tactic.Substitute' (ro, erls, subte, f, f'))
3.80 | NONE => Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable")
3.81 end
3.82 - | check (Tactic.Tac id) (cs as (pt, (p, _))) =
3.83 + | check (Tactic.Tac id) (cs as (pt, pos as (p, _))) =
3.84 let
3.85 -(*ctxt*)
3.86 +(*ctxt* )
3.87 val pp = Ctree.par_pblobj pt p;
3.88 val thy' = Ctree.get_obj Ctree.g_domID pt pp;
3.89 val thy = ThyC.get_theory thy';
3.90 -(*ctxt* )
3.91 +( *ctxt*)
3.92 val ctxt = Ctree.get_loc pt pos |> snd
3.93 val thy = Proof_Context.theory_of ctxt
3.94 val thy' = Context.theory_name thy
3.95 -( *ctxt*)
3.96 +(*ctxt*)
3.97 val f = Calc.current_formula cs;
3.98 in
3.99 Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, UnparseC.term f))
4.1 --- a/src/Tools/isac/MathEngBasic/state-steps.sml Tue Aug 16 15:53:20 2022 +0200
4.2 +++ b/src/Tools/isac/MathEngBasic/state-steps.sml Sun Aug 21 11:22:04 2022 +0200
4.3 @@ -34,7 +34,7 @@
4.4 type single =
4.5 (Tactic.input * (* for comparison with input tac *)
4.6 Tactic.T * (* for ctree generation *)
4.7 - (Pos.pos' * (* after applying tac_, for ctree generation *)
4.8 + (Pos.pos' * (* after applying tac_, for ctree generation *)
4.9 (Istate_Def.T * Proof.context))) (* after applying tac_, for ctree generation *)
4.10 val single_empty = (Tactic.Empty_Tac, Tactic.Empty_Tac_, (Pos.e_pos', (Istate_Def.empty, ContextC.empty))): single
4.11 fun taci2str ((tac, tac_, (pos', (istate, _))):single) =
5.1 --- a/test/Tools/isac/Test_Isac_Short.thy Tue Aug 16 15:53:20 2022 +0200
5.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Sun Aug 21 11:22:04 2022 +0200
5.3 @@ -251,6 +251,723 @@
5.4 ML_file "Interpret/error-pattern.sml"
5.5 ML_file "Interpret/li-tool.sml"
5.6 ML_file "Interpret/lucas-interpreter.sml"
5.7 +ML \<open>
5.8 +\<close> ML \<open>
5.9 +\<close> ML \<open>
5.10 +(* Title: "Interpret/lucas-interpreter.sml"
5.11 + Author: Walther Neuper
5.12 + (c) due to copyright terms
5.13 +*)
5.14 +
5.15 +"-----------------------------------------------------------------------------------------------";
5.16 +"table of contents -----------------------------------------------------------------------------";
5.17 +"-----------------------------------------------------------------------------------------------";
5.18 +"----------- Take as 1st stac in program -------------------------------------------------------";
5.19 +"----------- re-build: fun locate_input_tactic -------------------------------------------------";
5.20 +"----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------";
5.21 +"----------- re-build: fun find_next_step, mini ------------------------------------------------";
5.22 +"----------- re-build: fun locate_input_term ---------------------------------------------------";
5.23 +"-----------------------------------------------------------------------------------------------";
5.24 +"-----------------------------------------------------------------------------------------------";
5.25 +"-----------------------------------------------------------------------------------------------";
5.26 +
5.27 +"----------- Take as 1st stac in program -------------------------------------------------------";
5.28 +"----------- Take as 1st stac in program -------------------------------------------------------";
5.29 +"----------- Take as 1st stac in program -------------------------------------------------------";
5.30 +"compare --- Apply_Method with initial Take by Step.do_next --- in test/../step-solve ----------";
5.31 +val p = e_pos'; val c = [];
5.32 +val (p,_,f,nxt,_,pt) =
5.33 + CalcTreeTEST
5.34 + [(["functionTerm (x \<up> 2 + 1)", "integrateBy x", "antiDerivative FF"],
5.35 + ("Integrate", ["integrate", "function"], ["diff", "integration"]))];
5.36 +val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Tac ", ...) --> Add_Given...*)
5.37 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.38 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.39 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.40 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.41 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.42 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.43 +case nxt of (Apply_Method ["diff", "integration"]) => ()
5.44 + | _ => error "integrate.sml -- me method [diff,integration] -- spec";
5.45 +"----- step 8: returns nxt = Rewrite_Set_Inst ([\"(''bdv'', x)\"],\"integration\")";
5.46 +
5.47 +"~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
5.48 +"~~~~~ fun Step.by_tactic, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
5.49 +val Applicable.Yes m = Step.check tac (pt, p);
5.50 + (*if*) Tactic.for_specify' m; (*false*)
5.51 +"~~~~~ fun loc_solve_ , args:"; val (m, (pt,pos)) = (m, ptp);
5.52 +
5.53 +"~~~~~ fun Step_Solve.by_tactic , args:"; val (m as Apply_Method' (mI, _, _, ctxt), (pt, (pos as (p,_))))
5.54 + = (m, (pt, pos));
5.55 + val {srls, ...} = MethodC.from_store mI;
5.56 + val itms = case get_obj I pt p of
5.57 + PblObj {meth=itms, ...} => itms
5.58 + | _ => error "solve Apply_Method: uncovered case get_obj"
5.59 + val thy' = get_obj g_domID pt p;
5.60 + val thy = ThyC.get_theory thy';
5.61 + val srls = LItool.get_simplifier (pt, pos)
5.62 + val (is, env, ctxt, sc) = case LItool.init_pstate srls ctxt itms mI of
5.63 + (is as Istate.Pstate {env, ...}, ctxt, sc) => (is, env, ctxt, sc)
5.64 + | _ => error "solve Apply_Method: uncovered case init_pstate";
5.65 +(*+*)pstate2str (the_pstate is) = "([\"\n(f_f, x \<up> 2 + 1)\",\"\n(v_v, x)\"], [], empty, NONE, \n??.empty, ORundef, false, true)";
5.66 + val ini = LItool.implicit_take sc env;
5.67 + val p = lev_dn p;
5.68 +
5.69 + val NONE = (*case*) ini (*of*);
5.70 + val Next_Step (is', ctxt', m') =
5.71 + LI.find_next_step sc (pt, (p, Res)) is ctxt;
5.72 +(*+*)pstate2str (the_pstate is') = "([\"\n(f_f, x \<up> 2 + 1)\",\"\n(v_v, x)\"], [R,L,R], empty, NONE, \nIntegral x \<up> 2 + 1 D x, ORundef, false, false)";
5.73 + val Safe_Step (_, _, Take' _) = (*case*)
5.74 + locate_input_tactic sc (pt, (p, Res)) is' ctxt' m' (*of*);
5.75 +"~~~~~ fun locate_input_tactic , args:"; val ((Prog prog), cstate, istate, ctxt, tac)
5.76 + = (sc, (pt, (p, Res)), is', ctxt', m');
5.77 +
5.78 + (*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
5.79 +"~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
5.80 + = ((prog, (cstate, ctxt, tac)), istate);
5.81 + (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);
5.82 +
5.83 + val Accept_Tac1 (_, _, Take' _) =
5.84 + scan_dn1 cctt (ist |> set_path [R] |> set_or ORundef) (Program.body_of prog);
5.85 +"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const (\<^const_name>\<open>Let\<close>, _) $ e $ (Abs (id, T, b))))
5.86 + = (cctt, (ist |> set_path [R] |> set_or ORundef), (Program.body_of prog));
5.87 +
5.88 +(*+*) if UnparseC.term e = "Take (Integral f_f D v_v)" then () else error "scan_dn1 Integral changed";
5.89 +
5.90 + (*case*)
5.91 + scan_dn1 xxx (ist |> path_down [L, R]) e (*of*);
5.92 + (*======= end of scanning tacticals, a leaf =======*)
5.93 +"~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {eval, or, ...}), t)
5.94 + = (xxx, (ist |> path_down [L, R]), e);
5.95 +val (Program.Tac stac, a') = check_leaf "locate" ctxt eval (get_subst ist) t;
5.96 +
5.97 +
5.98 +
5.99 +"----------- re-build: fun locate_input_tactic -------------------------------------------------";
5.100 +"----------- re-build: fun locate_input_tactic -------------------------------------------------";
5.101 +"----------- re-build: fun locate_input_tactic -------------------------------------------------";
5.102 +val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
5.103 +val (dI',pI',mI') = ("Test", ["sqroot-test", "univariate", "equation", "test"],
5.104 + ["Test", "squ-equ-test-subpbl1"]);
5.105 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
5.106 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.107 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.108 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.109 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.110 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.111 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.112 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = (_, Apply_Method ["Test", "squ-equ-test-subpbl1"])*);
5.113 +(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Rewrite_Set", Rewrite_Set "norm_equation")*)
5.114 +
5.115 +(*//------------------ begin step into ------------------------------------------------------\\*)
5.116 +(*[1], Res*)val (p'''''_''',_,f,nxt'''''_''',_,pt'''''_''') = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
5.117 +
5.118 +"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt);
5.119 +
5.120 + (** )val (***)xxxx(***) ( *("ok", (_, _, (pt, p))) =( **) (*case*)
5.121 + Step.by_tactic tac (pt,p) (*of*);
5.122 +"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
5.123 + val Applicable.Yes m = (*case*) Solve_Step.check tac (pt, p) (*of*);
5.124 + (*if*) Tactic.for_specify' m; (*false*)
5.125 +
5.126 + (** )val (***)xxxxx_x(***) ( *(msg, cs') =( **)
5.127 +Step_Solve.by_tactic m ptp;
5.128 +"~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, ptp);
5.129 +(*+*)val (pt'''''_', (p'''''_', p_'''''_')) = (pt, (p, p_));
5.130 + (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p); (*else*)
5.131 + val thy' = get_obj g_domID pt (par_pblobj pt p);
5.132 + val (is, sc) = LItool.resume_prog thy' (p,p_) pt;
5.133 +
5.134 + locate_input_tactic sc (pt, po) (fst is) (snd is) m;
5.135 +"~~~~~ fun locate_input_tactic , args:"; val (Prog prog, cstate, istate, ctxt, tac)
5.136 + = (sc, (pt, po), (fst is), (snd is), m);
5.137 + val srls = get_simplifier cstate;
5.138 +
5.139 + (** )val Accept_Tac1 ((is as (_,_,_,_,_,strong_ass), ctxt, ss as((tac', _, ctree, pos', _) :: _))) =( **)
5.140 + (*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
5.141 +"~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
5.142 + = ((prog, (cstate, ctxt, tac)), istate);
5.143 + (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);
5.144 +
5.145 + (** )val xxxxx_xx = ( **)
5.146 + scan_dn1 cctt (ist |> set_path [R] |> set_or ORundef) (Program.body_of prog);
5.147 +"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const (\<^const_name>\<open>Let\<close>, _) $ e $ (Abs (id, T, b))))
5.148 + = (cctt, (ist |> set_path [R] |> set_or ORundef), (Program.body_of prog));
5.149 +
5.150 + (*case*) scan_dn1 xxx (ist |> path_down [L, R]) e (*of*);
5.151 +"~~~~~ fun scan_dn1 , args:"; val ((xxx as (cstate, _, _)), ist, (Const (\<^const_name>\<open>Chain\<close>(*1*), _) $ e1 $ e2 $ a))
5.152 + = (xxx, (ist |> path_down [L, R]), e);
5.153 +
5.154 + (*case*) scan_dn1 xxx (ist |> path_down_form ([L, L, R], a)) e1 (*of*);
5.155 +"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const (\<^const_name>\<open>Try\<close>(*2*), _) $ e))
5.156 + = (xxx, (ist |> path_down_form ([L, L, R], a)), e1);
5.157 +
5.158 + (*case*) scan_dn1 xxx (ist |> path_down [R]) e (*of*);
5.159 + (*======= end of scanning tacticals, a leaf =======*)
5.160 +"~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t)
5.161 + = (xxx, (ist |> path_down [R]), e);
5.162 + val (Program.Tac stac, a') =
5.163 + (*case*) check_leaf "locate" ctxt eval (get_subst ist) t (*of*);
5.164 + val LItool.Associated (m, v', ctxt) =
5.165 + (*case*) associate pt ctxt (m, stac) (*of*);
5.166 +
5.167 + Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m) (*return value*);
5.168 +"~~~~~ from scan_dn1 to scan_to_tactic1 return val:"; val (xxxxx_xx)
5.169 + = (Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m));
5.170 +
5.171 +"~~~~~ from scan_to_tactic1 to fun locate_input_tactic return val:"; val Accept_Tac1 ((ist as {assoc, ...}), ctxt, tac')
5.172 + = (Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m));
5.173 + (*if*) LibraryC.assoc (*then*);
5.174 +
5.175 + Safe_Step (Istate.Pstate ist, ctxt, tac') (*return value*);
5.176 +"~~~~~ from locate_input_tactic to fun Step_Solve.by_tactic return:"; val Safe_Step (istate, ctxt, tac)
5.177 + = (*xxxxx_xx*)(**)Safe_Step (Istate.Pstate ist, ctxt, tac')(**);
5.178 +
5.179 +(*+*)val (pt, po as (p, p_)) = (pt'''''_', (p'''''_', p_'''''_')); (* from begin of by_tactic *)
5.180 + val (p'', _, _,pt') =
5.181 + Step.add tac (istate, ctxt) (pt, (lev_on p, Pbl));
5.182 + (*in*)
5.183 +
5.184 + ("ok", ([(Tactic.input_from_T tac, tac, (p'', (istate, ctxt)))],
5.185 + [(*ctree NOT cut*)], (pt', p''))) (*return value*);
5.186 +"~~~~~ from Step_Solve.by_tactic \<longrightarrow> Step.by_tactic return:"; val ((msg, cs' : Calc.state_post))
5.187 + = ("ok", ([(Tactic.input_from_T tac, tac, (p'', (istate, ctxt)) )],
5.188 + [(*ctree NOT cut*)], (pt', p'')));
5.189 +
5.190 +"~~~~~ from Step.by_tactic to me return:"; val (("ok", (_, _, (pt, p)))) = (*** )xxxx( ***) ("ok", cs');
5.191 + val (_, ts) =
5.192 + (case Step.do_next p ((pt, Pos.e_pos'), []) of
5.193 + ("ok", (ts as (_, _, _) :: _, _, _)) => ("", ts)
5.194 + | ("helpless", _) => ("helpless: cannot propose tac", [])
5.195 + | ("no-fmz-spec", _) => error "no-fmz-spec"
5.196 + | ("end-of-calculation", (ts, _, _)) => ("", ts)
5.197 + | _ => error "me: uncovered case")
5.198 + handle ERROR msg => raise ERROR msg
5.199 + val tac =
5.200 + case ts of
5.201 + tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
5.202 + | _ => if p = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
5.203 +
5.204 + (p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Celem.Sundef, pt);
5.205 +"~~~~~ from me to TOOPLEVEL return:"; val (p,_,f,nxt,_,pt)
5.206 + = (*** )xxx( ***) (p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Celem.Sundef, pt);
5.207 +
5.208 +(*//--------------------- check results from modified me ----------------------------------\\*)
5.209 +if p = ([2], Res) andalso
5.210 + pr_ctree pr_short pt = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 = 2\n"
5.211 +then
5.212 + (case nxt of ("Rewrite_Set", Rewrite_Set "Test_simplify") => ()
5.213 + | _ => error "")
5.214 +else error "check results from modified me CHANGED";
5.215 +(*\\--------------------- check results from modified me ----------------------------------//*)
5.216 +
5.217 +"~~~~~ from me to TOPLEVEL return:"; val (p,_,f,nxt,_,pt) = (*** )xxx( ***) (**)(p, 000, f, nxt, 000, pt)(**);
5.218 +(*\\------------------ end step into --------------------------------------------------------//*)
5.219 +
5.220 +(*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt'''''_''' p'''''_''' [] pt'''''_'''; (*nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
5.221 +(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)
5.222 +(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (- 1 + x = 0)"*)
5.223 +(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor x"*)
5.224 +(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions x_i"*)
5.225 +(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Test"*)
5.226 +(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)
5.227 +(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["Test", "solve_linear"]*)
5.228 +(*[3], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
5.229 +(*[3, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)
5.230 +(*[3, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
5.231 +(*[3, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)
5.232 +(*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_elementwise "Assumptions"*)
5.233 +(*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)
5.234 +(*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*)
5.235 +
5.236 +(*/--------------------- final test ----------------------------------\\*)
5.237 +if p = ([], Res) andalso f2str f = "[x = 1]" andalso pr_ctree pr_short pt =
5.238 + ". ----- pblobj -----\n" ^
5.239 + "1. x + 1 = 2\n" ^
5.240 + "2. x + 1 + - 1 * 2 = 0\n" ^
5.241 + "3. ----- pblobj -----\n" ^
5.242 + "3.1. - 1 + x = 0\n" ^
5.243 + "3.2. x = 0 + - 1 * - 1\n" ^
5.244 + "4. [x = 1]\n"
5.245 +then case nxt of End_Proof' => () | _ => error "re-build: fun locate_input_tactic changed 1"
5.246 +else error "re-build: fun locate_input_tactic changed 2";
5.247 +
5.248 +
5.249 +"----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------";
5.250 +"----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------";
5.251 +"----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------";
5.252 +(*cp from -- try fun applyTactics ------- *)
5.253 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",
5.254 + "normalform N"],
5.255 + ("PolyMinus",["plus_minus", "polynom", "vereinfachen"],
5.256 + ["simplification", "for_polynomials", "with_minus"]))];
5.257 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.258 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.259 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.260 +(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "ordne_alphabetisch"*)
5.261 +
5.262 +(*+*)val Test_Out.FormKF "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12" = f
5.263 +
5.264 +(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "fasse_zusammen"*)
5.265 +
5.266 +(*+*)if map Tactic.input_to_string (specific_from_prog pt p) =
5.267 + ["Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_num; ?m is_num\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",
5.268 + "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_num; ?m is_num\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")",
5.269 +(*this is new since ThmC.numerals_to_Free.-----\\*)
5.270 + "Calculate PLUS"]
5.271 + then () else error "specific_from_prog ([1], Res) 1 CHANGED";
5.272 +(*[2], Res*)val ("ok", (_, _, ptp as (pt, p))) = Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);
5.273 +
5.274 +(*+*)if map Tactic.input_to_string (specific_from_prog pt p) = [
5.275 + "Rewrite (\"tausche_minus\", \"\<lbrakk>?b ist_monom; ?a kleiner ?b\<rbrakk>\n\<Longrightarrow> ?b - ?a = - ?a + ?b\")",
5.276 + "Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_num; ?m is_num\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",
5.277 + "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_num; ?m is_num\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")",
5.278 + (*this is new since ThmC.numerals_to_Free.-----\\*)
5.279 + "Calculate PLUS",
5.280 + (*this is new since ThmC.numerals_to_Free.-----//*)
5.281 + "Calculate MINUS"]
5.282 + then () else error "specific_from_prog ([1], Res) 2 CHANGED";
5.283 +(* = ([3], Res)*)val ("ok", (_, _, ptp as (pt, p))) = Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);
5.284 +
5.285 +(*//----------------- exception PTREE "get_obj f EmptyPtree" raised --------------------------\\*)
5.286 +(**)val ("ok", ([(Rewrite ("tausche_minus", _), _, _)], _, _)) = (*isa*)
5.287 + Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);
5.288 +"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (hd (specific_from_prog pt p), (pt, p));
5.289 + val Applicable.Yes m = (*case*) Solve_Step.check tac (pt, p) (*of*);
5.290 + (*if*) Tactic.for_specify' m; (*false*)
5.291 +
5.292 +(**) val ("ok", ([(Rewrite ("tausche_minus", _), _, _)], _, _)) = (*isa*)
5.293 +Step_Solve.by_tactic m (pt, p);
5.294 +"~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, p));
5.295 + (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
5.296 + val thy' = get_obj g_domID pt (par_pblobj pt p);
5.297 + val (is, sc) = LItool.resume_prog thy' (p,p_) pt;
5.298 +
5.299 + (*case*) locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*);
5.300 +"~~~~~ fun locate_input_tactic , args:"; val ((Rule.Prog prog), (cstate as (pt, (*?*)pos(*?*))), istate, ctxt, tac)
5.301 + = (sc, (pt, po), (fst is), (snd is), m);
5.302 + val srls = LItool.get_simplifier cstate (*TODO: shift into Istate.T*);
5.303 +
5.304 + (*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
5.305 +"~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
5.306 + = ((prog, (cstate, ctxt, tac)), istate);
5.307 + (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*else*);
5.308 +
5.309 + go_scan_up1 (prog, cctt) ist;
5.310 +"~~~~~ fun go_scan_up1 , args:"; val ((pcct as (prog, _)), (ist as {path, ...}))
5.311 + = ((prog, cctt), ist);
5.312 + (*if*) 1 < length path (*then*);
5.313 +
5.314 + scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog);
5.315 +"~~~~~ and scan_up1 , args:"; val (pcct, ist, (Const (\<^const_name>\<open>Try\<close>(*2*), _) $ _))
5.316 + = (pcct, (ist |> path_up), (TermC.sub_at (path_up' path) prog));
5.317 +
5.318 + go_scan_up1 pcct ist;
5.319 +"~~~~~ and go_scan_up1 , args:"; val ((pcct as (prog, _)), (ist as {path, ...}))
5.320 + = (pcct, ist);
5.321 + (*if*) 1 < length path (*then*);
5.322 +
5.323 + scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog);
5.324 +"~~~~~ and scan_up1 , args:"; val ((pcct as (prog, cct as (cstate, _, _))), ist,
5.325 + (Const (\<^const_name>\<open>Chain\<close>(*3*), _) $ _ ))
5.326 + = (pcct, (ist |> path_up), (TermC.sub_at (path_up' path) prog));
5.327 + val e2 = check_Seq_up ist prog
5.328 +;
5.329 + (*case*) scan_dn1 cct (ist |> path_up_down [R] |> set_or ORundef) e2 (*of*);
5.330 +"~~~~~ fun scan_dn1 , args:"; val (yyy, ist, (Const (\<^const_name>\<open>Chain\<close>(*2*), _) $ e1 $ e2))
5.331 + = (cct, (ist |> path_up_down [R] |> set_or ORundef), e2);
5.332 +
5.333 + (*case*) scan_dn1 cct (ist |> path_down [L, R]) e1 (*of*);
5.334 +"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const (\<^const_name>\<open>Try\<close>(*2*), _) $ e))
5.335 + = (cct, (ist |> path_down [L, R]), e1);
5.336 +
5.337 +\<close> ML \<open>
5.338 + (*case*) scan_dn1 cct (ist |> path_down [R]) e (*of*);
5.339 + (*======= end of scanning tacticals, a leaf =======*)
5.340 +"~~~~~ fun scan_dn1 , args:"; val ((cct as (_, ctxt, _)), (ist as {eval, ...}), t)
5.341 + = (cct, (ist |> path_down [R]), e);
5.342 + (*if*) Tactical.contained_in t (*else*);
5.343 + val (Program.Tac prog_tac, form_arg) = (*case*)
5.344 + LItool.check_leaf "locate" ctxt eval (get_subst ist) t (*of*);
5.345 +
5.346 + check_tac1 cct ist (prog_tac, form_arg);
5.347 +"~~~~~ fun check_tac1 , args:"; val (((pt, p), ctxt, tac), (ist as {act_arg, or, ...}), (prog_tac, form_arg)) =
5.348 + (cct, ist, (prog_tac, form_arg));
5.349 +val LItool.Not_Associated = (*case*)
5.350 + LItool.associate pt ctxt (tac, prog_tac) (*of*);
5.351 + val _(*ORundef*) = (*case*) or (*of*);
5.352 +
5.353 +(*+*)Solve_Step.check (LItool.tac_from_prog pt (ThyC.get_theory "Isac_Knowledge") prog_tac) (pt, p);
5.354 +
5.355 + val Applicable.Yes m' =
5.356 + (*case*) Solve_Step.check (LItool.tac_from_prog pt (ThyC.get_theory "Isac_Knowledge") prog_tac) (pt, p) (*of*);
5.357 +
5.358 + Reject_Tac1 (ist |> set_subst_false (form_arg, Tactic.result m'), ctxt, tac)
5.359 + (*return from check_tac1*);
5.360 +"~~~~~ from fun check_tac1 \<longrightarrow>fun scan_dn1 \<longrightarrow>fun scan_dn1 \<longrightarrow>fun locate_input_tactic , return:"; val (Reject_Tac1 _) =
5.361 + (Reject_Tac1 (ist |> set_subst_false (form_arg, Tactic.result m'), ctxt, tac));
5.362 +
5.363 +val Test_Out.FormKF "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g" = f;
5.364 +val ([3], Res) = p;
5.365 +
5.366 +
5.367 +\<close> ML \<open>
5.368 +"----------- re-build: fun find_next_step, mini ------------------------------------------------";
5.369 +"----------- re-build: fun find_next_step, mini ------------------------------------------------";
5.370 +"----------- re-build: fun find_next_step, mini ------------------------------------------------";
5.371 +val fmz = ["Term (a + a ::real)", "normalform n_n"];
5.372 +val (dI',pI',mI') = ("Poly",["polynomial", "simplification"],["simplification", "for_polynomials"]);
5.373 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
5.374 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Model_Problem*)
5.375 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Specify_Theory "Poly"*)
5.376 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Specify_Problem ["polynomial", "simplification"]*)
5.377 +(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Method ["simplification", "for_polynomials"]*)
5.378 +(*1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Apply_Method ["simplification", "for_polynomials"]*)
5.379 +(*[1], Res*)val (_, ([(tac'''''_', _, _)], _, (pt'''''_', p'''''_'))) =
5.380 +
5.381 + Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set "norm_Poly"*)
5.382 +(*//------------------ go into 1 ------------------------------------------------------------\\*)
5.383 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
5.384 + = (p, ((pt, e_pos'), []));
5.385 + val pIopt = Ctree.get_pblID (pt, ip);
5.386 + (*if*) ip = ([], Res) (*else*);
5.387 + val _ = (*case*) tacis (*of*);
5.388 + val SOME _ = (*case*) pIopt (*of*);
5.389 + (*if*) member op = [Pos.Pbl, Pos.Met] p_ (*else*);
5.390 +
5.391 +val ("ok", ([(Rewrite_Set "norm_Poly", _, _)], _, (_, ([1], Res)))) =
5.392 +Step_Solve.do_next (pt, ip);
5.393 +"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
5.394 + (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
5.395 + val thy' = get_obj g_domID pt (par_pblobj pt p);
5.396 + val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
5.397 +
5.398 +val Next_Step (_, _, Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _)) =
5.399 + LI.find_next_step sc (pt, pos) ist ctxt (*of*);
5.400 +"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), (Pstate ist), ctxt)
5.401 + = (sc, (pt, pos), ist, ctxt);
5.402 +
5.403 +val Accept_Tac (Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _), _, _) =
5.404 + (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
5.405 +"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))
5.406 + = ((prog, (ptp, ctxt)), (Pstate ist));
5.407 + (*if*) path = [] (*then*);
5.408 +
5.409 +val Accept_Tac (Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _), _, _) =
5.410 + scan_dn cc (trans_scan_dn ist) (Program.body_of prog);
5.411 +"~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t)
5.412 + = (cc, (trans_scan_dn ist), (Program.body_of prog));
5.413 + (*if*) Tactical.contained_in t (*else*);
5.414 + val (Program.Tac prog_tac, form_arg) = (*case*) LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
5.415 +
5.416 +val Accept_Tac (Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _), _, _) =
5.417 + check_tac cc ist (prog_tac, form_arg) (*return from xxx*);
5.418 +"~~~~~ from fun scan_dn\<longrightarrow>fun scan_to_tactic\<longrightarrow>fun find_next_step, return:"; val (Accept_Tac (tac, ist, ctxt))
5.419 + = (check_tac cc ist (prog_tac, form_arg));
5.420 +
5.421 + Next_Step (Pstate ist, Tactic.insert_assumptions tac ctxt, tac) (*return from find_next_step*);
5.422 +"~~~~~ from fun find_next_step\<longrightarrow>and do_next\<longrightarrow>fun zzz, return:"; val (Next_Step (ist, ctxt, tac))
5.423 + = (Next_Step (Pstate ist, Tactic.insert_assumptions tac ctxt, tac));
5.424 +
5.425 + LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp (*return from and do_next*);
5.426 +"~~~~~ from and do_next\<longrightarrow>fun do_next\<longrightarrow>toplevel, return:"; val (_, ([(tac''''', _, _)], _, (pt''''', p''''')))
5.427 + = (LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp);
5.428 +(*\\------------------ end of go into 1 -----------------------------------------------------//*)
5.429 +
5.430 +(*[], Res*)val (_, ([(tac''''', _, _)], _, (pt''''', p'''''))) =
5.431 +
5.432 + Step.do_next p'''''_' ((pt'''''_', Pos.e_pos'), []);(* Check_Postcond ["polynomial", "simplification"]*)
5.433 +(*//------------------ go into 2 ------------------------------------------------------------\\*)
5.434 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
5.435 + = (p''''', ((pt''''', e_pos'), []));
5.436 + val pIopt = Ctree.get_pblID (pt, ip);
5.437 + (*if*) ip = ([], Res) (*else*);
5.438 + val _ = (*case*) tacis (*of*);
5.439 + val SOME _ = (*case*) pIopt (*of*);
5.440 + (*if*) member op = [Pos.Pbl, Pos.Met] p_ (*else*);
5.441 +
5.442 +val ("ok", ([(Check_Postcond ["polynomial", "simplification"], _, _)], _, (_, ([], Res)))) =
5.443 +Step_Solve.do_next (pt, ip);
5.444 +"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
5.445 + (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
5.446 + val thy' = get_obj g_domID pt (par_pblobj pt p);
5.447 + val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
5.448 +
5.449 + (** )val End_Program (ist, tac) =
5.450 + ( *case*) LI.find_next_step sc (pt, pos) ist ctxt (*of*);
5.451 +"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), (Pstate ist), ctxt)
5.452 + = (sc, (pt, pos), ist, ctxt);
5.453 +
5.454 +(* val Term_Val (Const (\<^const_name>\<open>times\<close>, _) $ Free ("2", _) $ Free ("a", _))*)
5.455 + (** )val Term_Val prog_result =
5.456 + ( *case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
5.457 +"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))
5.458 + = ((prog, (ptp, ctxt)), (Pstate ist));
5.459 + (*if*) path = [] (*else*);
5.460 +
5.461 + go_scan_up (prog, cc) (trans_scan_up ist |> set_found);
5.462 +"~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...}))
5.463 + = ((prog, cc), (trans_scan_up ist(*|> set_found !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *)));
5.464 + (*if*) path = [R] (*then*);
5.465 + (*if*) found_accept = true (*then*);
5.466 +
5.467 + Term_Val act_arg (*return from go_scan_up*);
5.468 +"~~~~~ from fun go_scan_up\<longrightarrow>fun scan_to_tactic, return:"; val (Term_Val prog_result) = (Term_Val act_arg);
5.469 +
5.470 + Term_Val prog_result (*return from scan_to_tactic*);
5.471 +"~~~~~ from fun scan_to_tactic\<longrightarrow>fun find_next_step, return:"; val (Term_Val prog_result) = (Term_Val prog_result);
5.472 + val (true, p', _) = (*case*) parent_node pt p (*of*);
5.473 + val (_, pblID, _) = get_obj g_spec pt p';
5.474 +
5.475 + End_Program (Pstate ist, Tactic.Check_Postcond' (pblID, prog_result))
5.476 + (*return from find_next_step*);
5.477 +"~~~~~ from fun find_next_step\<longrightarrow>and do_next\<longrightarrow>fun zzz, return:"; val (End_Program (ist, tac))
5.478 + = (End_Program (Pstate ist, Tactic.Check_Postcond' (pblID,prog_result)));
5.479 + val _ = (*case*) tac (*of*);
5.480 +
5.481 +val ("ok", ([(Check_Postcond ["polynomial", "simplification"], _, _)], _, (_, ([], Res))))
5.482 + = LI.by_tactic tac (ist, ctxt) ptp (*return from and do_next*);
5.483 +"~~~~~ from and do_next\<longrightarrow>top level, return:"; val (_, ([(tac''''', _, _)], _, (pt''''', p''''')))
5.484 + = (LI.by_tactic tac (ist, ctxt) ptp);
5.485 +(*\\------------------ end of go into 2 -----------------------------------------------------//*)
5.486 +
5.487 +(*[], Und*)val (msg, ([], _, (pt, p))) = Step.do_next p''''' ((pt''''', Pos.e_pos'), []);(**)
5.488 +
5.489 +Test_Tool.show_pt_tac pt; (*[
5.490 +([], Frm), Simplify (a + a)
5.491 +. . . . . . . . . . Apply_Method ["simplification", "for_polynomials"],
5.492 +([1], Frm), a + a
5.493 +. . . . . . . . . . Rewrite_Set "norm_Poly",
5.494 +([1], Res), 2 * a
5.495 +. . . . . . . . . . Check_Postcond ["polynomial", "simplification"],
5.496 +([], Res), 2 * a]*)
5.497 +
5.498 +(*/--- final test ---------------------------------------------------------------------------\\*)
5.499 +val (res, asm) = (get_obj g_result pt (fst p));
5.500 +if UnparseC.term res = "2 * a" andalso map UnparseC.term asm = []
5.501 +andalso p = ([], Und) andalso msg = "end-of-calculation"
5.502 +andalso pr_ctree pr_short pt = ". ----- pblobj -----\n1. a + a\n"
5.503 +then
5.504 + case tac''''' of Check_Postcond ["polynomial", "simplification"] => ()
5.505 + | _ => error "re-build: fun find_next_step, mini 1"
5.506 +else error "re-build: fun find_next_step, mini 2"
5.507 +
5.508 +
5.509 +"----------- re-build: fun locate_input_term ---------------------------------------------------";
5.510 +"----------- re-build: fun locate_input_term ---------------------------------------------------";
5.511 +"----------- re-build: fun locate_input_term ---------------------------------------------------";
5.512 +(*cp from inform.sml
5.513 + ----------- appendFormula: on Res + late deriv ------------------------------------------------*)
5.514 +val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
5.515 +val (dI',pI',mI') = ("Test", ["sqroot-test", "univariate", "equation", "test"],
5.516 + ["Test", "squ-equ-test-subpbl1"]);
5.517 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
5.518 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.519 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.520 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.521 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.522 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.523 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.524 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["Test", "squ-equ-test-subpbl1"]*);
5.525 +
5.526 +(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Rewrite_Set "norm_equation"*)
5.527 +(*+*)if f2str f = "x + 1 = 2" then () else error "locate_input_term at ([1], Frm) CHANGED";
5.528 +
5.529 +(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Rewrite_Set "Test_simplify"*)
5.530 +(*+*)if f2str f = "x + 1 + - 1 * 2 = 0" then () else error "locate_input_term at ([1], Frm) CHANGED";
5.531 +
5.532 +Test_Tool.show_pt_tac pt; (*[
5.533 +([], Frm), solve (x + 1 = 2, x)
5.534 +. . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
5.535 +([1], Frm), x + 1 = 2
5.536 +. . . . . . . . . . Rewrite_Set "norm_equation",
5.537 +([1], Res), x + 1 + - 1 * 2 = 0 ///Check_Postcond..ERROR*)
5.538 +
5.539 +\<close> ML \<open>
5.540 +(*//---------- appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term ----------\\*)
5.541 +"~~~~~ fun appendFormula , args:"; val ((*cI, *) ifo: TermC.as_string) = ((**) "x = 1");
5.542 + val cs = (*get_calc cI*) ((pt, p), [(*nxt, nxt_, (pos, (ist, ctxt))*)])
5.543 + val pos = (*get_pos cI 1*) p
5.544 +
5.545 +(*+*)val ptp''''' = (pt, p);
5.546 +(*+*)if snd ptp''''' = ([1], Res) then () else error "old_cs changed";
5.547 +(*+*)Test_Tool.show_pt_tac pt; (*[
5.548 +(*+*)([], Frm), solve (x + 1 = 2, x)
5.549 +(*+*). . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
5.550 +(*+*)([1], Frm), x + 1 = 2
5.551 +(*+*). . . . . . . . . . Rewrite_Set "norm_equation",
5.552 +(*+*)([1], Res), x + 1 + - 1 * 2 = 0 ///Check_Postcond*)
5.553 +
5.554 + val ("ok", cs' as (_, _, ptp')) =
5.555 + (*case*) Step.do_next pos cs (*of*);
5.556 +
5.557 +\<close> ML \<open>
5.558 +val ("ok", (_(*use in DG !!!*), [], ptp''''' as (pt''''', p'''''))) = (*case*)
5.559 +Step_Solve.by_term ptp' (encode ifo) (*of*);
5.560 +\<close> ML \<open>
5.561 +"~~~~~ fun by_term , args:"; val ((pt, pos as (p, _)), istr)
5.562 + = (ptp', (encode ifo));
5.563 +\<close> ML \<open>
5.564 + val SOME f_in =
5.565 + (*case*) TermC.parseNEW (get_ctxt pt pos) istr (*of*);
5.566 + val pos_pred = lev_back(*'*) pos
5.567 + val f_pred = Ctree.get_curr_formula (pt, pos_pred);
5.568 + val f_succ = Ctree.get_curr_formula (pt, pos);
5.569 + (*if*) f_succ = f_in (*else*);
5.570 + val NONE =
5.571 + (*case*) CAS_Cmd.input f_in (*of*);
5.572 +
5.573 +\<close> ML \<open>
5.574 +(*NEW*) LI.locate_input_term (pt, pos) f_in (*of*);
5.575 +\<close> ML \<open>
5.576 +"~~~~~ fun locate_input_term , args:"; val ((pt, pos), tm) = ((pt, pos), f_in);
5.577 + val pos_pred = Pos.lev_back' pos (*f_pred ---"step pos cs"---> f_succ in appendFormula*)
5.578 +
5.579 + \<close> ML \<open>
5.580 + val ("ok", (_, _, cstate as (pt', pos'))) =
5.581 + (*case*) compare_step ([], [], (pt, pos_pred)) tm (*of*);
5.582 +\<close> ML \<open>
5.583 +"~~~~~ fun compare_step , args:"; val ((tacis, c, ptp as (pt, pos as (p, _))), ifo) =
5.584 + (([], [], (pt, pos_pred)), tm);
5.585 + val fo = Calc.current_formula ptp
5.586 + val {nrls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
5.587 + val {rew_ord, erls, rules, ...} = Rule_Set.rep nrls
5.588 +\<close> ML \<open>
5.589 +(*+*)Proof_Context.theory_of (Ctree.get_ctxt pt pos) (*Isac.Test OK!*)
5.590 +\<close> ML \<open>
5.591 + val (found, der) = Derive.steps (Ctree.get_ctxt pt pos) rew_ord erls rules fo ifo; (*<---------------*)
5.592 +\<close> ML \<open>
5.593 + (*if*) found (*else*);
5.594 + (*if*) pos = ([], Pos.Res) (*else*);
5.595 +\<close> ML \<open>
5.596 + val msg_cs' as (_, (tacis, c', ptp)) = LI.do_next ptp; (*<---------------------*)
5.597 +\<close> ML \<open>
5.598 + (*case*) tacis (*of \<longrightarrow> [(Rewrite_Set "Test_simplify",...*) :State_Steps.T;
5.599 +\<close> ML \<open>
5.600 +
5.601 +(*+*) val ((input, tac, (pos, (ist, ctxt))) :: _) = tacis;
5.602 +(*+*) input (*= Tactic.Rewrite_Set "Test_simplify"*);
5.603 +(*+*) tac;
5.604 +(*+*) pos = ([2], Res);
5.605 +(*+*) ist;
5.606 +(*+*) Proof_Context.theory_of ctxt (*.., Isac.Test*);
5.607 +
5.608 +\<close> ML \<open>
5.609 + (*in*) compare_step (tacis, c @ c' (*@ c'' =c'BECAUSE OF | _ => msg_cs'*), ptp) ifo (*end*)
5.610 +\<close> ML \<open>
5.611 +"~~~~~ fun compare_step , args:"; val ((tacis, c, ptp as (pt, pos as (p, _))), ifo) =
5.612 + (([], [], (pt, pos_pred)), tm);
5.613 + val fo = Calc.current_formula ptp
5.614 + val {nrls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
5.615 + val {rew_ord, erls, rules, ...} = Rule_Set.rep nrls
5.616 +\<close> ML \<open>
5.617 + val (found, der) = Derive.steps (Ctree.get_ctxt pt pos) rew_ord erls rules fo ifo; (*<---------------*)
5.618 +\<close> ML \<open>
5.619 + (*if*) found (*else*);
5.620 + (*if*) pos = ([], Pos.Res) (*else*);
5.621 +\<close> ML \<open>
5.622 + val msg_cs' as (_, (tacis, c', ptp)) = LI.do_next ptp; (*<---------------------*)
5.623 +\<close> ML \<open>
5.624 +
5.625 +(*+*) val ((input, tac, (pos, (ist, ctxt))) :: _) = tacis;
5.626 +(*+*) input (*= Tactic.Rewrite_Set "Test_simplify"*);
5.627 +\<close> ML \<open>
5.628 +(*+*) tac;
5.629 +(*+*) pos = ([2], Res);
5.630 +(*+*) ist;
5.631 +(*+*) Proof_Context.theory_of ctxt (*.., Isac.Test*);
5.632 +
5.633 +\<close> ML \<open>
5.634 +\<close> ML \<open>
5.635 +\<close> ML \<open>
5.636 +Tactic.Apply_Method': MethodC.id * term option * Istate.T * Proof.context -> Tactic.T
5.637 +\<close> ML \<open>
5.638 +\<close> ML \<open>
5.639 +\<close> ML \<open>
5.640 +\<close> ML \<open>
5.641 +\<close> ML \<open>
5.642 +\<close> ML \<open>
5.643 +\<close> ML \<open>
5.644 +
5.645 +\<close> ML \<open> (*----- original..*)
5.646 +(*NEW*) Found_Step cstate (*return from locate_input_term*);
5.647 + (*LI.Found_Step ( *)cstate(*, _(*istate*), _(*ctxt*))( *return from locate_input_term*);
5.648 +"~~~~~ from fun locate_input_term\<longrightarrow>fun Step_Solve.by_term, return:"; val ("ok", (_(*use in DG !!!*), c, ptp as (_, p)))
5.649 + = (("ok" , ([], [], cstate (* already contains istate, ctxt *))));
5.650 +
5.651 + ("ok", ((*_ use in DG !!!,*) c, ptp(* as (_*), p))(*)*)(*return from Step_Solve.by_term*);
5.652 +"~~~~~ from fun Step_Solve.by_term\<longrightarrow>(fun appendFormula)!toplevel, return:"; val ("ok", (_(*use in DG !!!*), [], ptp''''' as (pt''''', p''''')))
5.653 + = ("ok", ([], [], ptp));
5.654 +
5.655 +\<close> ML \<open>
5.656 +(*fun me requires nxt...*)
5.657 + Step.do_next p''''' (ptp''''', []);
5.658 + val ("ok", ([(nxt'''''_' as Check_Postcond ["LINEAR", "univariate", "equation", "test"], _, _)], _,
5.659 + (pt'''''_', p'''''_'))) = Step.do_next p''''' (ptp''''', [])
5.660 +(*\\---------- appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term ----------//*)
5.661 +
5.662 +(*//----- REPLACED BY appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term -----\\* )
5.663 + (*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
5.664 + (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)
5.665 + (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (- 1 + x = 0)"*)
5.666 + (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor x"*)
5.667 + (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions x_i"*)
5.668 + (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Test"*)
5.669 + (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)
5.670 + (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["Test", "solve_linear"]*)
5.671 + (*[3], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
5.672 + (*[3, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)
5.673 + (*[3, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
5.674 + (*[3, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)
5.675 +( *\\----- REPLACED BY appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term -----//*)
5.676 +
5.677 + (*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt'''''_' p'''''_' [] pt'''''_'; (*nxt = Check_elementwise "Assumptions"*)
5.678 + (*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)
5.679 + (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*)
5.680 +
5.681 +\<close> ML \<open>
5.682 +(*/--- final test ---------------------------------------------------------------------------\\*)
5.683 +if p = ([], Res) andalso f2str f = "[x = 1]" andalso pr_ctree pr_short pt =
5.684 + ". ----- pblobj -----\n" ^
5.685 + "1. x + 1 = 2\n" ^
5.686 + "2. x + 1 + - 1 * 2 = 0\n" ^
5.687 + "3. ----- pblobj -----\n" ^
5.688 + "3.1. - 1 + x = 0\n" ^
5.689 + "3.2. x = 0 + - 1 * - 1\n" ^
5.690 + "3.2.1. x = 0 + - 1 * - 1\n" ^
5.691 + "3.2.2. x = 0 + 1\n" (*ATTENTION: see complete Calc below*)
5.692 +then case nxt of End_Proof' => () | _ => error "re-build: fun locate_input_term CHANGED 1"
5.693 +else error "re-build: fun locate_input_term CHANGED 2";
5.694 +
5.695 +Test_Tool.show_pt_tac pt; (*[
5.696 +([], Frm), solve (x + 1 = 2, x)
5.697 +. . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
5.698 +([1], Frm), x + 1 = 2
5.699 +. . . . . . . . . . Rewrite_Set "norm_equation",
5.700 +([1], Res), x + 1 + - 1 * 2 = 0
5.701 +. . . . . . . . . . Rewrite_Set "Test_simplify",
5.702 +([2], Res), - 1 + x = 0
5.703 +. . . . . . . . . . Subproblem (Test, ["LINEAR", "univariate", "equation", "test"]),
5.704 +([3], Pbl), solve (- 1 + x = 0, x)
5.705 +. . . . . . . . . . Apply_Method ["Test", "solve_linear"],
5.706 +([3,1], Frm), - 1 + x = 0
5.707 +. . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', x)], "isolate_bdv"),
5.708 +([3,1], Res), x = 0 + - 1 * - 1
5.709 +. . . . . . . . . . Derive Test_simplify,
5.710 +([3,2,1], Frm), x = 0 + - 1 * - 1
5.711 +. . . . . . . . . . Rewrite ("#: - 1 * - 1 = 1", "- 1 * - 1 = 1"),
5.712 +([3,2,1], Res), x = 0 + 1
5.713 +. . . . . . . . . . Rewrite ("radd_0", "0 + ?k = ?k"),
5.714 +([3,2,2], Res), x = 1
5.715 +. . . . . . . . . . Tactic.input_to_string not impl. for ?!,
5.716 +([3,2], Res), x = 1
5.717 +. . . . . . . . . . Check_Postcond ["LINEAR", "univariate", "equation", "test"],
5.718 +([3], Res), [x = 1]
5.719 +. . . . . . . . . . Check_Postcond ["sqroot-test", "univariate", "equation", "test"],
5.720 +([], Res), [x = 1]]*)
5.721 +\<close> ML \<open>
5.722 +\<close> ML \<open>
5.723 +\<close>
5.724 ML_file "Interpret/step-solve.sml"
5.725
5.726 ML_file "MathEngine/me-misc.sml"
5.727 @@ -274,6 +991,12 @@
5.728 ML_file "Knowledge/delete.sml"
5.729 ML_file "Knowledge/descript.sml"
5.730 ML_file "Knowledge/simplify.sml"
5.731 +ML \<open>
5.732 +\<close> ML \<open>
5.733 +\<close> ML \<open>
5.734 +\<close> ML \<open>
5.735 +\<close> ML \<open>
5.736 +\<close>
5.737 ML_file "Knowledge/poly-1.sml"
5.738 (*ML_file "Knowledge/poly-2.sml" Test_Isac_Short*)
5.739 ML_file "Knowledge/gcd_poly_ml.sml"
6.1 --- a/test/Tools/isac/Test_Some.thy Tue Aug 16 15:53:20 2022 +0200
6.2 +++ b/test/Tools/isac/Test_Some.thy Sun Aug 21 11:22:04 2022 +0200
6.3 @@ -112,6 +112,677 @@
6.4 ML \<open>
6.5 \<close> ML \<open>
6.6 \<close> ML \<open>
6.7 +(* Title: "Interpret/lucas-interpreter.sml"
6.8 + Author: Walther Neuper
6.9 + (c) due to copyright terms
6.10 +*)
6.11 +
6.12 +"-----------------------------------------------------------------------------------------------";
6.13 +"table of contents -----------------------------------------------------------------------------";
6.14 +"-----------------------------------------------------------------------------------------------";
6.15 +"----------- Take as 1st stac in program -------------------------------------------------------";
6.16 +"----------- re-build: fun locate_input_tactic -------------------------------------------------";
6.17 +"----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------";
6.18 +"----------- re-build: fun find_next_step, mini ------------------------------------------------";
6.19 +"----------- re-build: fun locate_input_term ---------------------------------------------------";
6.20 +"-----------------------------------------------------------------------------------------------";
6.21 +"-----------------------------------------------------------------------------------------------";
6.22 +"-----------------------------------------------------------------------------------------------";
6.23 +
6.24 +"----------- Take as 1st stac in program -------------------------------------------------------";
6.25 +"----------- Take as 1st stac in program -------------------------------------------------------";
6.26 +"----------- Take as 1st stac in program -------------------------------------------------------";
6.27 +"compare --- Apply_Method with initial Take by Step.do_next --- in test/../step-solve ----------";
6.28 +val p = e_pos'; val c = [];
6.29 +val (p,_,f,nxt,_,pt) =
6.30 + CalcTreeTEST
6.31 + [(["functionTerm (x \<up> 2 + 1)", "integrateBy x", "antiDerivative FF"],
6.32 + ("Integrate", ["integrate", "function"], ["diff", "integration"]))];
6.33 +val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Tac ", ...) --> Add_Given...*)
6.34 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.35 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.36 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.37 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.38 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.39 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.40 +case nxt of (Apply_Method ["diff", "integration"]) => ()
6.41 + | _ => error "integrate.sml -- me method [diff,integration] -- spec";
6.42 +"----- step 8: returns nxt = Rewrite_Set_Inst ([\"(''bdv'', x)\"],\"integration\")";
6.43 +
6.44 +"~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
6.45 +"~~~~~ fun Step.by_tactic, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
6.46 +val Applicable.Yes m = Step.check tac (pt, p);
6.47 + (*if*) Tactic.for_specify' m; (*false*)
6.48 +"~~~~~ fun loc_solve_ , args:"; val (m, (pt,pos)) = (m, ptp);
6.49 +
6.50 +"~~~~~ fun Step_Solve.by_tactic , args:"; val (m as Apply_Method' (mI, _, _, ctxt), (pt, (pos as (p,_))))
6.51 + = (m, (pt, pos));
6.52 + val {srls, ...} = MethodC.from_store mI;
6.53 + val itms = case get_obj I pt p of
6.54 + PblObj {meth=itms, ...} => itms
6.55 + | _ => error "solve Apply_Method: uncovered case get_obj"
6.56 + val thy' = get_obj g_domID pt p;
6.57 + val thy = ThyC.get_theory thy';
6.58 + val srls = LItool.get_simplifier (pt, pos)
6.59 + val (is, env, ctxt, sc) = case LItool.init_pstate srls ctxt itms mI of
6.60 + (is as Istate.Pstate {env, ...}, ctxt, sc) => (is, env, ctxt, sc)
6.61 + | _ => error "solve Apply_Method: uncovered case init_pstate";
6.62 +(*+*)pstate2str (the_pstate is) = "([\"\n(f_f, x \<up> 2 + 1)\",\"\n(v_v, x)\"], [], empty, NONE, \n??.empty, ORundef, false, true)";
6.63 + val ini = LItool.implicit_take sc env;
6.64 + val p = lev_dn p;
6.65 +
6.66 + val NONE = (*case*) ini (*of*);
6.67 + val Next_Step (is', ctxt', m') =
6.68 + LI.find_next_step sc (pt, (p, Res)) is ctxt;
6.69 +(*+*)pstate2str (the_pstate is') = "([\"\n(f_f, x \<up> 2 + 1)\",\"\n(v_v, x)\"], [R,L,R], empty, NONE, \nIntegral x \<up> 2 + 1 D x, ORundef, false, false)";
6.70 + val Safe_Step (_, _, Take' _) = (*case*)
6.71 + locate_input_tactic sc (pt, (p, Res)) is' ctxt' m' (*of*);
6.72 +"~~~~~ fun locate_input_tactic , args:"; val ((Prog prog), cstate, istate, ctxt, tac)
6.73 + = (sc, (pt, (p, Res)), is', ctxt', m');
6.74 +
6.75 + (*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
6.76 +"~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
6.77 + = ((prog, (cstate, ctxt, tac)), istate);
6.78 + (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);
6.79 +
6.80 + val Accept_Tac1 (_, _, Take' _) =
6.81 + scan_dn1 cctt (ist |> set_path [R] |> set_or ORundef) (Program.body_of prog);
6.82 +"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const (\<^const_name>\<open>Let\<close>, _) $ e $ (Abs (id, T, b))))
6.83 + = (cctt, (ist |> set_path [R] |> set_or ORundef), (Program.body_of prog));
6.84 +
6.85 +(*+*) if UnparseC.term e = "Take (Integral f_f D v_v)" then () else error "scan_dn1 Integral changed";
6.86 +
6.87 + (*case*)
6.88 + scan_dn1 xxx (ist |> path_down [L, R]) e (*of*);
6.89 + (*======= end of scanning tacticals, a leaf =======*)
6.90 +"~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {eval, or, ...}), t)
6.91 + = (xxx, (ist |> path_down [L, R]), e);
6.92 +val (Program.Tac stac, a') = check_leaf "locate" ctxt eval (get_subst ist) t;
6.93 +
6.94 +
6.95 +
6.96 +"----------- re-build: fun locate_input_tactic -------------------------------------------------";
6.97 +"----------- re-build: fun locate_input_tactic -------------------------------------------------";
6.98 +"----------- re-build: fun locate_input_tactic -------------------------------------------------";
6.99 +val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
6.100 +val (dI',pI',mI') = ("Test", ["sqroot-test", "univariate", "equation", "test"],
6.101 + ["Test", "squ-equ-test-subpbl1"]);
6.102 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.103 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.104 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.105 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.106 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.107 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.108 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.109 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = (_, Apply_Method ["Test", "squ-equ-test-subpbl1"])*);
6.110 +(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Rewrite_Set", Rewrite_Set "norm_equation")*)
6.111 +
6.112 +(*//------------------ begin step into ------------------------------------------------------\\*)
6.113 +(*[1], Res*)val (p'''''_''',_,f,nxt'''''_''',_,pt'''''_''') = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
6.114 +
6.115 +"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt);
6.116 +
6.117 + (** )val (***)xxxx(***) ( *("ok", (_, _, (pt, p))) =( **) (*case*)
6.118 + Step.by_tactic tac (pt,p) (*of*);
6.119 +"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
6.120 + val Applicable.Yes m = (*case*) Solve_Step.check tac (pt, p) (*of*);
6.121 + (*if*) Tactic.for_specify' m; (*false*)
6.122 +
6.123 + (** )val (***)xxxxx_x(***) ( *(msg, cs') =( **)
6.124 +Step_Solve.by_tactic m ptp;
6.125 +"~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, ptp);
6.126 +(*+*)val (pt'''''_', (p'''''_', p_'''''_')) = (pt, (p, p_));
6.127 + (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p); (*else*)
6.128 + val thy' = get_obj g_domID pt (par_pblobj pt p);
6.129 + val (is, sc) = LItool.resume_prog thy' (p,p_) pt;
6.130 +
6.131 + locate_input_tactic sc (pt, po) (fst is) (snd is) m;
6.132 +"~~~~~ fun locate_input_tactic , args:"; val (Prog prog, cstate, istate, ctxt, tac)
6.133 + = (sc, (pt, po), (fst is), (snd is), m);
6.134 + val srls = get_simplifier cstate;
6.135 +
6.136 + (** )val Accept_Tac1 ((is as (_,_,_,_,_,strong_ass), ctxt, ss as((tac', _, ctree, pos', _) :: _))) =( **)
6.137 + (*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
6.138 +"~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
6.139 + = ((prog, (cstate, ctxt, tac)), istate);
6.140 + (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);
6.141 +
6.142 + (** )val xxxxx_xx = ( **)
6.143 + scan_dn1 cctt (ist |> set_path [R] |> set_or ORundef) (Program.body_of prog);
6.144 +"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const (\<^const_name>\<open>Let\<close>, _) $ e $ (Abs (id, T, b))))
6.145 + = (cctt, (ist |> set_path [R] |> set_or ORundef), (Program.body_of prog));
6.146 +
6.147 + (*case*) scan_dn1 xxx (ist |> path_down [L, R]) e (*of*);
6.148 +"~~~~~ fun scan_dn1 , args:"; val ((xxx as (cstate, _, _)), ist, (Const (\<^const_name>\<open>Chain\<close>(*1*), _) $ e1 $ e2 $ a))
6.149 + = (xxx, (ist |> path_down [L, R]), e);
6.150 +
6.151 + (*case*) scan_dn1 xxx (ist |> path_down_form ([L, L, R], a)) e1 (*of*);
6.152 +"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const (\<^const_name>\<open>Try\<close>(*2*), _) $ e))
6.153 + = (xxx, (ist |> path_down_form ([L, L, R], a)), e1);
6.154 +
6.155 + (*case*) scan_dn1 xxx (ist |> path_down [R]) e (*of*);
6.156 + (*======= end of scanning tacticals, a leaf =======*)
6.157 +"~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t)
6.158 + = (xxx, (ist |> path_down [R]), e);
6.159 + val (Program.Tac stac, a') =
6.160 + (*case*) check_leaf "locate" ctxt eval (get_subst ist) t (*of*);
6.161 + val LItool.Associated (m, v', ctxt) =
6.162 + (*case*) associate pt ctxt (m, stac) (*of*);
6.163 +
6.164 + Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m) (*return value*);
6.165 +"~~~~~ from scan_dn1 to scan_to_tactic1 return val:"; val (xxxxx_xx)
6.166 + = (Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m));
6.167 +
6.168 +"~~~~~ from scan_to_tactic1 to fun locate_input_tactic return val:"; val Accept_Tac1 ((ist as {assoc, ...}), ctxt, tac')
6.169 + = (Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m));
6.170 + (*if*) LibraryC.assoc (*then*);
6.171 +
6.172 + Safe_Step (Istate.Pstate ist, ctxt, tac') (*return value*);
6.173 +"~~~~~ from locate_input_tactic to fun Step_Solve.by_tactic return:"; val Safe_Step (istate, ctxt, tac)
6.174 + = (*xxxxx_xx*)(**)Safe_Step (Istate.Pstate ist, ctxt, tac')(**);
6.175 +
6.176 +(*+*)val (pt, po as (p, p_)) = (pt'''''_', (p'''''_', p_'''''_')); (* from begin of by_tactic *)
6.177 + val (p'', _, _,pt') =
6.178 + Step.add tac (istate, ctxt) (pt, (lev_on p, Pbl));
6.179 + (*in*)
6.180 +
6.181 + ("ok", ([(Tactic.input_from_T tac, tac, (p'', (istate, ctxt)))],
6.182 + [(*ctree NOT cut*)], (pt', p''))) (*return value*);
6.183 +"~~~~~ from Step_Solve.by_tactic \<longrightarrow> Step.by_tactic return:"; val ((msg, cs' : Calc.state_post))
6.184 + = ("ok", ([(Tactic.input_from_T tac, tac, (p'', (istate, ctxt)) )],
6.185 + [(*ctree NOT cut*)], (pt', p'')));
6.186 +
6.187 +"~~~~~ from Step.by_tactic to me return:"; val (("ok", (_, _, (pt, p)))) = (*** )xxxx( ***) ("ok", cs');
6.188 + val (_, ts) =
6.189 + (case Step.do_next p ((pt, Pos.e_pos'), []) of
6.190 + ("ok", (ts as (_, _, _) :: _, _, _)) => ("", ts)
6.191 + | ("helpless", _) => ("helpless: cannot propose tac", [])
6.192 + | ("no-fmz-spec", _) => error "no-fmz-spec"
6.193 + | ("end-of-calculation", (ts, _, _)) => ("", ts)
6.194 + | _ => error "me: uncovered case")
6.195 + handle ERROR msg => raise ERROR msg
6.196 + val tac =
6.197 + case ts of
6.198 + tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
6.199 + | _ => if p = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
6.200 +
6.201 + (p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Celem.Sundef, pt);
6.202 +"~~~~~ from me to TOOPLEVEL return:"; val (p,_,f,nxt,_,pt)
6.203 + = (*** )xxx( ***) (p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Celem.Sundef, pt);
6.204 +
6.205 +(*//--------------------- check results from modified me ----------------------------------\\*)
6.206 +if p = ([2], Res) andalso
6.207 + pr_ctree pr_short pt = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 = 2\n"
6.208 +then
6.209 + (case nxt of ("Rewrite_Set", Rewrite_Set "Test_simplify") => ()
6.210 + | _ => error "")
6.211 +else error "check results from modified me CHANGED";
6.212 +(*\\--------------------- check results from modified me ----------------------------------//*)
6.213 +
6.214 +"~~~~~ from me to TOPLEVEL return:"; val (p,_,f,nxt,_,pt) = (*** )xxx( ***) (**)(p, 000, f, nxt, 000, pt)(**);
6.215 +(*\\------------------ end step into --------------------------------------------------------//*)
6.216 +
6.217 +(*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt'''''_''' p'''''_''' [] pt'''''_'''; (*nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
6.218 +(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)
6.219 +(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (- 1 + x = 0)"*)
6.220 +(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor x"*)
6.221 +(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions x_i"*)
6.222 +(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Test"*)
6.223 +(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)
6.224 +(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["Test", "solve_linear"]*)
6.225 +(*[3], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
6.226 +(*[3, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)
6.227 +(*[3, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
6.228 +(*[3, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)
6.229 +(*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_elementwise "Assumptions"*)
6.230 +(*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)
6.231 +(*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*)
6.232 +
6.233 +(*/--------------------- final test ----------------------------------\\*)
6.234 +if p = ([], Res) andalso f2str f = "[x = 1]" andalso pr_ctree pr_short pt =
6.235 + ". ----- pblobj -----\n" ^
6.236 + "1. x + 1 = 2\n" ^
6.237 + "2. x + 1 + - 1 * 2 = 0\n" ^
6.238 + "3. ----- pblobj -----\n" ^
6.239 + "3.1. - 1 + x = 0\n" ^
6.240 + "3.2. x = 0 + - 1 * - 1\n" ^
6.241 + "4. [x = 1]\n"
6.242 +then case nxt of End_Proof' => () | _ => error "re-build: fun locate_input_tactic changed 1"
6.243 +else error "re-build: fun locate_input_tactic changed 2";
6.244 +
6.245 +
6.246 +"----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------";
6.247 +"----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------";
6.248 +"----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------";
6.249 +(*cp from -- try fun applyTactics ------- *)
6.250 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",
6.251 + "normalform N"],
6.252 + ("PolyMinus",["plus_minus", "polynom", "vereinfachen"],
6.253 + ["simplification", "for_polynomials", "with_minus"]))];
6.254 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.255 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.256 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.257 +(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "ordne_alphabetisch"*)
6.258 +
6.259 +(*+*)val Test_Out.FormKF "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12" = f
6.260 +
6.261 +(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "fasse_zusammen"*)
6.262 +
6.263 +(*+*)if map Tactic.input_to_string (specific_from_prog pt p) =
6.264 + ["Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_num; ?m is_num\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",
6.265 + "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_num; ?m is_num\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")",
6.266 +(*this is new since ThmC.numerals_to_Free.-----\\*)
6.267 + "Calculate PLUS"]
6.268 + then () else error "specific_from_prog ([1], Res) 1 CHANGED";
6.269 +(*[2], Res*)val ("ok", (_, _, ptp as (pt, p))) = Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);
6.270 +
6.271 +(*+*)if map Tactic.input_to_string (specific_from_prog pt p) = [
6.272 + "Rewrite (\"tausche_minus\", \"\<lbrakk>?b ist_monom; ?a kleiner ?b\<rbrakk>\n\<Longrightarrow> ?b - ?a = - ?a + ?b\")",
6.273 + "Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_num; ?m is_num\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",
6.274 + "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_num; ?m is_num\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")",
6.275 + (*this is new since ThmC.numerals_to_Free.-----\\*)
6.276 + "Calculate PLUS",
6.277 + (*this is new since ThmC.numerals_to_Free.-----//*)
6.278 + "Calculate MINUS"]
6.279 + then () else error "specific_from_prog ([1], Res) 2 CHANGED";
6.280 +(* = ([3], Res)*)val ("ok", (_, _, ptp as (pt, p))) = Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);
6.281 +
6.282 +(*//----------------- exception PTREE "get_obj f EmptyPtree" raised --------------------------\\*)
6.283 +(**)val ("ok", ([(Rewrite ("tausche_minus", _), _, _)], _, _)) = (*isa*)
6.284 + Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);
6.285 +"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (hd (specific_from_prog pt p), (pt, p));
6.286 + val Applicable.Yes m = (*case*) Solve_Step.check tac (pt, p) (*of*);
6.287 + (*if*) Tactic.for_specify' m; (*false*)
6.288 +
6.289 +(**) val ("ok", ([(Rewrite ("tausche_minus", _), _, _)], _, _)) = (*isa*)
6.290 +Step_Solve.by_tactic m (pt, p);
6.291 +"~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, p));
6.292 + (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
6.293 + val thy' = get_obj g_domID pt (par_pblobj pt p);
6.294 + val (is, sc) = LItool.resume_prog thy' (p,p_) pt;
6.295 +
6.296 + (*case*) locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*);
6.297 +"~~~~~ fun locate_input_tactic , args:"; val ((Rule.Prog prog), (cstate as (pt, (*?*)pos(*?*))), istate, ctxt, tac)
6.298 + = (sc, (pt, po), (fst is), (snd is), m);
6.299 + val srls = LItool.get_simplifier cstate (*TODO: shift into Istate.T*);
6.300 +
6.301 + (*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
6.302 +"~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
6.303 + = ((prog, (cstate, ctxt, tac)), istate);
6.304 + (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*else*);
6.305 +
6.306 + go_scan_up1 (prog, cctt) ist;
6.307 +"~~~~~ fun go_scan_up1 , args:"; val ((pcct as (prog, _)), (ist as {path, ...}))
6.308 + = ((prog, cctt), ist);
6.309 + (*if*) 1 < length path (*then*);
6.310 +
6.311 +\<close> ML \<open>
6.312 + scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog);
6.313 +"~~~~~ and scan_up1 , args:"; val (pcct, ist, (Const (\<^const_name>\<open>Try\<close>(*2*), _) $ _))
6.314 + = (pcct, (ist |> path_up), (TermC.sub_at (path_up' path) prog));
6.315 +
6.316 + go_scan_up1 pcct ist;
6.317 +"~~~~~ and go_scan_up1 , args:"; val ((pcct as (prog, _)), (ist as {path, ...}))
6.318 + = (pcct, ist);
6.319 + (*if*) 1 < length path (*then*);
6.320 +
6.321 + scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog);
6.322 +"~~~~~ and scan_up1 , args:"; val ((pcct as (prog, cct as (cstate, _, _))), ist,
6.323 + (Const (\<^const_name>\<open>Chain\<close>(*3*), _) $ _ ))
6.324 + = (pcct, (ist |> path_up), (TermC.sub_at (path_up' path) prog));
6.325 + val e2 = check_Seq_up ist prog
6.326 +;
6.327 + (*case*) scan_dn1 cct (ist |> path_up_down [R] |> set_or ORundef) e2 (*of*);
6.328 +"~~~~~ fun scan_dn1 , args:"; val (yyy, ist, (Const (\<^const_name>\<open>Chain\<close>(*2*), _) $ e1 $ e2))
6.329 + = (cct, (ist |> path_up_down [R] |> set_or ORundef), e2);
6.330 +
6.331 + (*case*) scan_dn1 cct (ist |> path_down [L, R]) e1 (*of*);
6.332 +"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const (\<^const_name>\<open>Try\<close>(*2*), _) $ e))
6.333 + = (cct, (ist |> path_down [L, R]), e1);
6.334 +
6.335 + (*case*) scan_dn1 cct (ist |> path_down [R]) e (*of*);
6.336 + (*======= end of scanning tacticals, a leaf =======*)
6.337 +"~~~~~ fun scan_dn1 , args:"; val ((cct as (_, ctxt, _)), (ist as {eval, ...}), t)
6.338 + = (cct, (ist |> path_down [R]), e);
6.339 + (*if*) Tactical.contained_in t (*else*);
6.340 + val (Program.Tac prog_tac, form_arg) = (*case*)
6.341 + LItool.check_leaf "locate" ctxt eval (get_subst ist) t (*of*);
6.342 +
6.343 + check_tac1 cct ist (prog_tac, form_arg);
6.344 +"~~~~~ fun check_tac1 , args:"; val (((pt, p), ctxt, tac), (ist as {act_arg, or, ...}), (prog_tac, form_arg)) =
6.345 + (cct, ist, (prog_tac, form_arg));
6.346 +val LItool.Not_Associated = (*case*)
6.347 + LItool.associate pt ctxt (tac, prog_tac) (*of*);
6.348 + val _(*ORundef*) = (*case*) or (*of*);
6.349 +
6.350 +(*+*)Solve_Step.check (LItool.tac_from_prog pt (ThyC.get_theory "Isac_Knowledge") prog_tac) (pt, p);
6.351 +
6.352 + val Applicable.Yes m' =
6.353 + (*case*) Solve_Step.check (LItool.tac_from_prog pt (ThyC.get_theory "Isac_Knowledge") prog_tac) (pt, p) (*of*);
6.354 +
6.355 + Reject_Tac1 (ist |> set_subst_false (form_arg, Tactic.result m'), ctxt, tac)
6.356 + (*return from check_tac1*);
6.357 +"~~~~~ from fun check_tac1 \<longrightarrow>fun scan_dn1 \<longrightarrow>fun scan_dn1 \<longrightarrow>fun locate_input_tactic , return:"; val (Reject_Tac1 _) =
6.358 + (Reject_Tac1 (ist |> set_subst_false (form_arg, Tactic.result m'), ctxt, tac));
6.359 +
6.360 +val Test_Out.FormKF "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g" = f;
6.361 +val ([3], Res) = p;
6.362 +
6.363 +
6.364 +"----------- re-build: fun find_next_step, mini ------------------------------------------------";
6.365 +"----------- re-build: fun find_next_step, mini ------------------------------------------------";
6.366 +"----------- re-build: fun find_next_step, mini ------------------------------------------------";
6.367 +val fmz = ["Term (a + a ::real)", "normalform n_n"];
6.368 +val (dI',pI',mI') = ("Poly",["polynomial", "simplification"],["simplification", "for_polynomials"]);
6.369 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.370 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Model_Problem*)
6.371 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Specify_Theory "Poly"*)
6.372 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Specify_Problem ["polynomial", "simplification"]*)
6.373 +(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Method ["simplification", "for_polynomials"]*)
6.374 +(*1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Apply_Method ["simplification", "for_polynomials"]*)
6.375 +(*[1], Res*)val (_, ([(tac'''''_', _, _)], _, (pt'''''_', p'''''_'))) =
6.376 +
6.377 + Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set "norm_Poly"*)
6.378 +(*//------------------ go into 1 ------------------------------------------------------------\\*)
6.379 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
6.380 + = (p, ((pt, e_pos'), []));
6.381 + val pIopt = Ctree.get_pblID (pt, ip);
6.382 + (*if*) ip = ([], Res) (*else*);
6.383 + val _ = (*case*) tacis (*of*);
6.384 + val SOME _ = (*case*) pIopt (*of*);
6.385 + (*if*) member op = [Pos.Pbl, Pos.Met] p_ (*else*);
6.386 +
6.387 +val ("ok", ([(Rewrite_Set "norm_Poly", _, _)], _, (_, ([1], Res)))) =
6.388 +Step_Solve.do_next (pt, ip);
6.389 +"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
6.390 + (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
6.391 + val thy' = get_obj g_domID pt (par_pblobj pt p);
6.392 + val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
6.393 +
6.394 +val Next_Step (_, _, Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _)) =
6.395 + LI.find_next_step sc (pt, pos) ist ctxt (*of*);
6.396 +"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), (Pstate ist), ctxt)
6.397 + = (sc, (pt, pos), ist, ctxt);
6.398 +
6.399 +val Accept_Tac (Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _), _, _) =
6.400 + (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
6.401 +"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))
6.402 + = ((prog, (ptp, ctxt)), (Pstate ist));
6.403 + (*if*) path = [] (*then*);
6.404 +
6.405 +val Accept_Tac (Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _), _, _) =
6.406 + scan_dn cc (trans_scan_dn ist) (Program.body_of prog);
6.407 +"~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t)
6.408 + = (cc, (trans_scan_dn ist), (Program.body_of prog));
6.409 + (*if*) Tactical.contained_in t (*else*);
6.410 + val (Program.Tac prog_tac, form_arg) = (*case*) LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
6.411 +
6.412 +val Accept_Tac (Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _), _, _) =
6.413 + check_tac cc ist (prog_tac, form_arg) (*return from xxx*);
6.414 +"~~~~~ from fun scan_dn\<longrightarrow>fun scan_to_tactic\<longrightarrow>fun find_next_step, return:"; val (Accept_Tac (tac, ist, ctxt))
6.415 + = (check_tac cc ist (prog_tac, form_arg));
6.416 +
6.417 + Next_Step (Pstate ist, Tactic.insert_assumptions tac ctxt, tac) (*return from find_next_step*);
6.418 +"~~~~~ from fun find_next_step\<longrightarrow>and do_next\<longrightarrow>fun zzz, return:"; val (Next_Step (ist, ctxt, tac))
6.419 + = (Next_Step (Pstate ist, Tactic.insert_assumptions tac ctxt, tac));
6.420 +
6.421 + LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp (*return from and do_next*);
6.422 +"~~~~~ from and do_next\<longrightarrow>fun do_next\<longrightarrow>toplevel, return:"; val (_, ([(tac''''', _, _)], _, (pt''''', p''''')))
6.423 + = (LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp);
6.424 +(*\\------------------ end of go into 1 -----------------------------------------------------//*)
6.425 +
6.426 +(*[], Res*)val (_, ([(tac''''', _, _)], _, (pt''''', p'''''))) =
6.427 +
6.428 + Step.do_next p'''''_' ((pt'''''_', Pos.e_pos'), []);(* Check_Postcond ["polynomial", "simplification"]*)
6.429 +(*//------------------ go into 2 ------------------------------------------------------------\\*)
6.430 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
6.431 + = (p''''', ((pt''''', e_pos'), []));
6.432 + val pIopt = Ctree.get_pblID (pt, ip);
6.433 + (*if*) ip = ([], Res) (*else*);
6.434 + val _ = (*case*) tacis (*of*);
6.435 + val SOME _ = (*case*) pIopt (*of*);
6.436 + (*if*) member op = [Pos.Pbl, Pos.Met] p_ (*else*);
6.437 +
6.438 +val ("ok", ([(Check_Postcond ["polynomial", "simplification"], _, _)], _, (_, ([], Res)))) =
6.439 +Step_Solve.do_next (pt, ip);
6.440 +"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
6.441 + (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
6.442 + val thy' = get_obj g_domID pt (par_pblobj pt p);
6.443 + val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
6.444 +
6.445 + (** )val End_Program (ist, tac) =
6.446 + ( *case*) LI.find_next_step sc (pt, pos) ist ctxt (*of*);
6.447 +"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), (Pstate ist), ctxt)
6.448 + = (sc, (pt, pos), ist, ctxt);
6.449 +
6.450 +(* val Term_Val (Const (\<^const_name>\<open>times\<close>, _) $ Free ("2", _) $ Free ("a", _))*)
6.451 + (** )val Term_Val prog_result =
6.452 + ( *case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
6.453 +"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))
6.454 + = ((prog, (ptp, ctxt)), (Pstate ist));
6.455 + (*if*) path = [] (*else*);
6.456 +
6.457 + go_scan_up (prog, cc) (trans_scan_up ist |> set_found);
6.458 +"~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...}))
6.459 + = ((prog, cc), (trans_scan_up ist(*|> set_found !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *)));
6.460 + (*if*) path = [R] (*then*);
6.461 + (*if*) found_accept = true (*then*);
6.462 +
6.463 + Term_Val act_arg (*return from go_scan_up*);
6.464 +"~~~~~ from fun go_scan_up\<longrightarrow>fun scan_to_tactic, return:"; val (Term_Val prog_result) = (Term_Val act_arg);
6.465 +
6.466 + Term_Val prog_result (*return from scan_to_tactic*);
6.467 +"~~~~~ from fun scan_to_tactic\<longrightarrow>fun find_next_step, return:"; val (Term_Val prog_result) = (Term_Val prog_result);
6.468 + val (true, p', _) = (*case*) parent_node pt p (*of*);
6.469 + val (_, pblID, _) = get_obj g_spec pt p';
6.470 +
6.471 + End_Program (Pstate ist, Tactic.Check_Postcond' (pblID, prog_result))
6.472 + (*return from find_next_step*);
6.473 +"~~~~~ from fun find_next_step\<longrightarrow>and do_next\<longrightarrow>fun zzz, return:"; val (End_Program (ist, tac))
6.474 + = (End_Program (Pstate ist, Tactic.Check_Postcond' (pblID,prog_result)));
6.475 + val _ = (*case*) tac (*of*);
6.476 +
6.477 +val ("ok", ([(Check_Postcond ["polynomial", "simplification"], _, _)], _, (_, ([], Res))))
6.478 + = LI.by_tactic tac (ist, ctxt) ptp (*return from and do_next*);
6.479 +"~~~~~ from and do_next\<longrightarrow>top level, return:"; val (_, ([(tac''''', _, _)], _, (pt''''', p''''')))
6.480 + = (LI.by_tactic tac (ist, ctxt) ptp);
6.481 +(*\\------------------ end of go into 2 -----------------------------------------------------//*)
6.482 +
6.483 +(*[], Und*)val (msg, ([], _, (pt, p))) = Step.do_next p''''' ((pt''''', Pos.e_pos'), []);(**)
6.484 +
6.485 +Test_Tool.show_pt_tac pt; (*[
6.486 +([], Frm), Simplify (a + a)
6.487 +. . . . . . . . . . Apply_Method ["simplification", "for_polynomials"],
6.488 +([1], Frm), a + a
6.489 +. . . . . . . . . . Rewrite_Set "norm_Poly",
6.490 +([1], Res), 2 * a
6.491 +. . . . . . . . . . Check_Postcond ["polynomial", "simplification"],
6.492 +([], Res), 2 * a]*)
6.493 +
6.494 +(*/--- final test ---------------------------------------------------------------------------\\*)
6.495 +val (res, asm) = (get_obj g_result pt (fst p));
6.496 +\<close> ML \<open>
6.497 +if UnparseC.term res = "2 * a" andalso map UnparseC.term asm = []
6.498 +andalso p = ([], Und) andalso msg = "end-of-calculation"
6.499 +andalso pr_ctree pr_short pt = ". ----- pblobj -----\n1. a + a\n"
6.500 +then
6.501 + case tac''''' of Check_Postcond ["polynomial", "simplification"] => ()
6.502 + | _ => error "re-build: fun find_next_step, mini 1"
6.503 +else error "re-build: fun find_next_step, mini 2"
6.504 +
6.505 +
6.506 +\<close> ML \<open>
6.507 +"----------- re-build: fun locate_input_term ---------------------------------------------------";
6.508 +"----------- re-build: fun locate_input_term ---------------------------------------------------";
6.509 +"----------- re-build: fun locate_input_term ---------------------------------------------------";
6.510 +(*cp from inform.sml
6.511 + ----------- appendFormula: on Res + late deriv ------------------------------------------------*)
6.512 +val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
6.513 +val (dI',pI',mI') = ("Test", ["sqroot-test", "univariate", "equation", "test"],
6.514 + ["Test", "squ-equ-test-subpbl1"]);
6.515 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.516 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.517 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.518 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.519 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.520 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.521 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.522 +\<close> ML \<open>
6.523 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["Test", "squ-equ-test-subpbl1"]*);
6.524 +
6.525 +(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Rewrite_Set "norm_equation"*)
6.526 +(*+*)if f2str f = "x + 1 = 2" then () else error "locate_input_term at ([1], Frm) CHANGED";
6.527 +
6.528 +(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Rewrite_Set "Test_simplify"*)
6.529 +(*+*)if f2str f = "x + 1 + - 1 * 2 = 0" then () else error "locate_input_term at ([1], Frm) CHANGED";
6.530 +
6.531 +Test_Tool.show_pt_tac pt; (*[
6.532 +([], Frm), solve (x + 1 = 2, x)
6.533 +. . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
6.534 +([1], Frm), x + 1 = 2
6.535 +. . . . . . . . . . Rewrite_Set "norm_equation",
6.536 +([1], Res), x + 1 + - 1 * 2 = 0 ///Check_Postcond..ERROR*)
6.537 +
6.538 +(*//---------- appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term ----------\\*)
6.539 +"~~~~~ fun appendFormula , args:"; val ((*cI, *) ifo: TermC.as_string) = ((**) "x = 1");
6.540 + val cs = (*get_calc cI*) ((pt, p), [(*nxt, nxt_, (pos, (ist, ctxt))*)])
6.541 + val pos = (*get_pos cI 1*) p
6.542 +
6.543 +\<close> ML \<open>
6.544 +(*+*)val ptp''''' = (pt, p);
6.545 +(*+*)if snd ptp''''' = ([1], Res) then () else error "old_cs changed";
6.546 +(*+*)Test_Tool.show_pt_tac pt; (*[
6.547 +(*+*)([], Frm), solve (x + 1 = 2, x)
6.548 +(*+*). . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
6.549 +(*+*)([1], Frm), x + 1 = 2
6.550 +(*+*). . . . . . . . . . Rewrite_Set "norm_equation",
6.551 +(*+*)([1], Res), x + 1 + - 1 * 2 = 0 ///Check_Postcond*)
6.552 +
6.553 + val ("ok", cs' as (_, _, ptp')) =
6.554 + (*case*) Step.do_next pos cs (*of*);
6.555 +
6.556 +\<close> ML \<open>
6.557 +val (pt, p) = ptp'
6.558 +\<close> ML \<open>
6.559 +Proof_Context.theory_of (Ctree.get_ctxt pt p) (*= Isac.Test*)
6.560 +\<close> ML \<open>
6.561 +ifo = "x = 1"
6.562 +\<close> ML \<open>
6.563 +(*+*)Step_Solve.by_term ptp' (encode ifo)
6.564 +(*Inner syntax error
6.565 +Failed to parse term*)
6.566 +\<close> ML \<open>
6.567 +val ("ok", (_(*use in DG !!!*), [], ptp''''' as (pt''''', p'''''))) = (*case*)
6.568 + Step_Solve.by_term ptp' (encode ifo) (*of*);
6.569 +"~~~~~ fun Step_Solve.by_term , args:"; val ((pt, pos as (p, _)), istr)
6.570 + = (ptp', (encode ifo));
6.571 +\<close> ML \<open>
6.572 + val SOME f_in =
6.573 + (*case*) TermC.parseNEW (get_ctxt pt pos) istr (*of*);
6.574 + val pos_pred = lev_back(*'*) pos
6.575 + val f_pred = Ctree.get_curr_formula (pt, pos_pred);
6.576 + val f_succ = Ctree.get_curr_formula (pt, pos);
6.577 + (*if*) f_succ = f_in (*else*);
6.578 + val NONE =
6.579 + (*case*) CAS_Cmd.input f_in (*of*);
6.580 +
6.581 +(*old* ) val (_, _, metID) = get_obj g_spec pt (par_pblobj pt p)
6.582 +(*old*) val {scr = prog, ...} = MethodC.from_store metID
6.583 +(*old*) val istate = get_istate_LI pt pos
6.584 +(*old*) val ctxt = get_ctxt pt pos
6.585 + val LI.Found_Step (cstate'''''_', _(*istate*), _(*ctxt*)) = (*case*)
6.586 + LI.locate_input_term prog (pt, pos) istate ctxt f_in (*of*);
6.587 +"~~~~~ fun locate_input_term , args:"; val ((Rule.Prog _), ((pt, pos) : Calc.T), (_ : Istate.T), (_ : Proof.context), tm)
6.588 + = (prog, (pt, pos), istate, ctxt, f_in);
6.589 +( *old*)
6.590 +
6.591 +\<close> ML \<open>
6.592 +(*NEW*) LI.locate_input_term (pt, pos) f_in (*of*);
6.593 +"~~~~~ fun locate_input_term , args:"; val ((pt, pos), tm) = ((pt, pos), f_in);
6.594 + val pos_pred = Pos.lev_back' pos (*f_pred ---"step pos cs"---> f_succ in appendFormula*)
6.595 +
6.596 + val ("ok", (_, _, cstate as (pt', pos'))) =
6.597 + (*case*) compare_step ([], [], (pt, pos_pred)) tm (*of*);
6.598 +
6.599 +(*old* )
6.600 + Found_Step (cstate, get_istate_LI pt' pos', get_ctxt pt' pos') (*return from locate_input_term*);
6.601 +( *old*)
6.602 +(*NEW*) Found_Step cstate (*return from locate_input_term*);
6.603 + (*LI.Found_Step ( *)cstate(*, _(*istate*), _(*ctxt*))( *return from locate_input_term*);
6.604 +"~~~~~ from fun locate_input_term\<longrightarrow>fun Step_Solve.by_term, return:"; val ("ok", (_(*use in DG !!!*), c, ptp as (_, p)))
6.605 + = (("ok" , ([], [], cstate (* already contains istate, ctxt *))));
6.606 +
6.607 + ("ok", ((*_ use in DG !!!,*) c, ptp(* as (_*), p))(*)*)(*return from Step_Solve.by_term*);
6.608 +"~~~~~ from fun Step_Solve.by_term\<longrightarrow>(fun appendFormula)!toplevel, return:"; val ("ok", (_(*use in DG !!!*), [], ptp''''' as (pt''''', p''''')))
6.609 + = ("ok", ([], [], ptp));
6.610 +
6.611 +(*fun me requires nxt...*)
6.612 + Step.do_next p''''' (ptp''''', []);
6.613 + val ("ok", ([(nxt'''''_' as Check_Postcond ["LINEAR", "univariate", "equation", "test"], _, _)], _,
6.614 + (pt'''''_', p'''''_'))) = Step.do_next p''''' (ptp''''', [])
6.615 +(*\\---------- appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term ----------//*)
6.616 +
6.617 +(*//----- REPLACED BY appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term -----\\* )
6.618 + (*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
6.619 + (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)
6.620 + (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (- 1 + x = 0)"*)
6.621 + (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor x"*)
6.622 + (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions x_i"*)
6.623 + (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Test"*)
6.624 + (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)
6.625 + (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["Test", "solve_linear"]*)
6.626 + (*[3], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
6.627 + (*[3, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)
6.628 + (*[3, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
6.629 + (*[3, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)
6.630 +( *\\----- REPLACED BY appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term -----//*)
6.631 +
6.632 + (*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt'''''_' p'''''_' [] pt'''''_'; (*nxt = Check_elementwise "Assumptions"*)
6.633 + (*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)
6.634 + (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*)
6.635 +
6.636 +\<close> ML \<open>
6.637 +(*/--- final test ---------------------------------------------------------------------------\\*)
6.638 +if p = ([], Res) andalso f2str f = "[x = 1]" andalso pr_ctree pr_short pt =
6.639 + ". ----- pblobj -----\n" ^
6.640 + "1. x + 1 = 2\n" ^
6.641 + "2. x + 1 + - 1 * 2 = 0\n" ^
6.642 + "3. ----- pblobj -----\n" ^
6.643 + "3.1. - 1 + x = 0\n" ^
6.644 + "3.2. x = 0 + - 1 * - 1\n" ^
6.645 + "3.2.1. x = 0 + - 1 * - 1\n" ^
6.646 + "3.2.2. x = 0 + 1\n" (*ATTENTION: see complete Calc below*)
6.647 +then case nxt of End_Proof' => () | _ => error "re-build: fun locate_input_term CHANGED 1"
6.648 +else error "re-build: fun locate_input_term CHANGED 2";
6.649 +
6.650 +Test_Tool.show_pt_tac pt; (*[
6.651 +([], Frm), solve (x + 1 = 2, x)
6.652 +. . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
6.653 +([1], Frm), x + 1 = 2
6.654 +. . . . . . . . . . Rewrite_Set "norm_equation",
6.655 +([1], Res), x + 1 + - 1 * 2 = 0
6.656 +. . . . . . . . . . Rewrite_Set "Test_simplify",
6.657 +([2], Res), - 1 + x = 0
6.658 +. . . . . . . . . . Subproblem (Test, ["LINEAR", "univariate", "equation", "test"]),
6.659 +([3], Pbl), solve (- 1 + x = 0, x)
6.660 +. . . . . . . . . . Apply_Method ["Test", "solve_linear"],
6.661 +([3,1], Frm), - 1 + x = 0
6.662 +. . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', x)], "isolate_bdv"),
6.663 +([3,1], Res), x = 0 + - 1 * - 1
6.664 +. . . . . . . . . . Derive Test_simplify,
6.665 +([3,2,1], Frm), x = 0 + - 1 * - 1
6.666 +. . . . . . . . . . Rewrite ("#: - 1 * - 1 = 1", "- 1 * - 1 = 1"),
6.667 +([3,2,1], Res), x = 0 + 1
6.668 +. . . . . . . . . . Rewrite ("radd_0", "0 + ?k = ?k"),
6.669 +([3,2,2], Res), x = 1
6.670 +. . . . . . . . . . Tactic.input_to_string not impl. for ?!,
6.671 +([3,2], Res), x = 1
6.672 +. . . . . . . . . . Check_Postcond ["LINEAR", "univariate", "equation", "test"],
6.673 +([3], Res), [x = 1]
6.674 +. . . . . . . . . . Check_Postcond ["sqroot-test", "univariate", "equation", "test"],
6.675 +([], Res), [x = 1]]*)
6.676 +\<close> ML \<open>
6.677 +\<close> ML \<open>
6.678 \<close> ML \<open>
6.679 \<close>
6.680