1.1 --- a/TODO.md Sun Aug 21 16:20:48 2022 +0200
1.2 +++ b/TODO.md Mon Aug 22 11:26:20 2022 +0200
1.3 @@ -51,20 +51,15 @@
1.4 - the trial with <fun is_empty> in Calculation.thy makes the question more precise:
1.5 better hack parsers or better work on ML_Syntax?
1.6
1.7 +* ?How accomplish two user-requirements by Outer_Syntax.command \<^command_keyword>\<open>Example\<close>
1.8 + (1) start a Calculation with a CAS_Cmd
1.9 + (2) start an Example from scratch, i.e. with (Formalize.empty, References.empty)
1.10 + Proposals for a solution are in test/../Test_VSCode_Example.thy
1.11 + subsubsection ‹Start Example with a CAS_Cmd›
1.12 +
1.13
1.14 ***** priority of WN items is top down, most urgent/simple on top
1.15
1.16 -* WN: rewriting with ctxt not complete (cause errors hard to indentify later)
1.17 - - Solve_Step.check ..Rewrite_Inst, Substitute, etc: push ctxt through Interpret/*
1.18 - a step in a calculation
1.19 - initialises ctxt from specified thy -> pushes ctxt through whole calculation
1.20 - val pp = Ctree.par_pblobj pt p; -> val ctxt = Ctree.get_loc pt pos |> snd
1.21 - val thy' = Ctree.get_obj Ctree.g_domID pt pp;->
1.22 - val thy = ThyC.get_theory thy'; -> val thy = Proof_Context.theory_of ctxt
1.23 - val ctxt = Proof_Context.init_global thy; -> val thy' = Context.theory_name thy
1.24 - cp code to test/*
1.25 - - Derive.steps: note HACK, new code still outcommented
1.26 -
1.27 * WN: eliminate SPARK; as an example replaced by Outer_Syntax.command..problem
1.28
1.29 * WN: Step_Specify.initialisePIDE: remove hdl in return-value, replace Step_Specify.nxt_specify_init_calc
2.1 --- a/src/Tools/isac/TODO.thy Sun Aug 21 16:20:48 2022 +0200
2.2 +++ b/src/Tools/isac/TODO.thy Mon Aug 22 11:26:20 2022 +0200
2.3 @@ -683,7 +683,7 @@
2.4
2.5 src/../InsSort.thy
2.6 srls = Rule_Set.empty, calc = [], rules = [
2.7 - Rule.Thm ("xfoldr_Nil",(*num_str*) @{thm xfoldr_Nil} (* foldr ?f [] = id *)),
2.8 + Rule.Thm ("xfoldr_Nil",(*num_str*) @ {thm xfoldr_Nil} (* foldr ?f [] = id *)),
2.9 *)
2.10 \item xxx
2.11 \item xxx
3.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Sun Aug 21 16:20:48 2022 +0200
3.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Mon Aug 22 11:26:20 2022 +0200
3.3 @@ -555,16 +555,6 @@
3.4 val NONE =
3.5 (*case*) CAS_Cmd.input f_in (*of*);
3.6
3.7 -(*old* ) val (_, _, metID) = get_obj g_spec pt (par_pblobj pt p)
3.8 -(*old*) val {scr = prog, ...} = MethodC.from_store metID
3.9 -(*old*) val istate = get_istate_LI pt pos
3.10 -(*old*) val ctxt = get_ctxt pt pos
3.11 - val LI.Found_Step (cstate'''''_', _(*istate*), _(*ctxt*)) = (*case*)
3.12 - LI.locate_input_term prog (pt, pos) istate ctxt f_in (*of*);
3.13 -"~~~~~ fun locate_input_term , args:"; val ((Rule.Prog _), ((pt, pos) : Calc.T), (_ : Istate.T), (_ : Proof.context), tm)
3.14 - = (prog, (pt, pos), istate, ctxt, f_in);
3.15 -( *old*)
3.16 -
3.17 (*NEW*) LI.locate_input_term (pt, pos) f_in (*of*);
3.18 "~~~~~ fun locate_input_term , args:"; val ((pt, pos), tm) = ((pt, pos), f_in);
3.19 val pos_pred = Pos.lev_back' pos (*f_pred ---"step pos cs"---> f_succ in appendFormula*)
3.20 @@ -576,7 +566,7 @@
3.21 Found_Step (cstate, get_istate_LI pt' pos', get_ctxt pt' pos') (*return from locate_input_term*);
3.22 ( *old*)
3.23 (*NEW*) Found_Step cstate (*return from locate_input_term*);
3.24 - (*LI.Found_Step ( *)cstate(*, _(*istate*), _(*ctxt*))( *return from locate_input_term*);
3.25 + (*LI.Found_Step ( *)cstate(*, _(*istate*), _)( *return from locate_input_term*);
3.26 "~~~~~ from fun locate_input_term\<longrightarrow>fun Step_Solve.by_term, return:"; val ("ok", (_(*use in DG !!!*), c, ptp as (_, p)))
3.27 = (("ok" , ([], [], cstate (* already contains istate, ctxt *))));
3.28
4.1 --- a/test/Tools/isac/Knowledge/simplify.sml Sun Aug 21 16:20:48 2022 +0200
4.2 +++ b/test/Tools/isac/Knowledge/simplify.sml Mon Aug 22 11:26:20 2022 +0200
4.3 @@ -16,7 +16,8 @@
4.4 val thy = @{theory "Simplify"};
4.5
4.6 (*
4.7 - This test is postponed, because respective user-requirements are not clarified.
4.8 + This test is postponed within Isabelle/PIDE/isac development,
4.9 + because respective user-requirements are not clarified.
4.10 See test/../cas-command.sml --- start Calculation with CAS_Cmd ---
4.11 and test/../Test_VSCode_Example.thy subsubsection \<open>Start Example with a CAS_Cmd\<close>
4.12 "----------- CAS-command Simplify -----------------------";
5.1 --- a/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Sun Aug 21 16:20:48 2022 +0200
5.2 +++ b/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Mon Aug 22 11:26:20 2022 +0200
5.3 @@ -79,4 +79,4 @@
5.4 case nxt of Model_Problem => ()
5.5 | _ => error "minisubpbl: CalcTreeTEST has no nxt = Model_Problem";
5.6
5.7 -(*ctxt*)Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Isac_Knowledge"*)
5.8 +Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Isac_Knowledge"*)
6.1 --- a/test/Tools/isac/Minisubpbl/150-add-given.sml Sun Aug 21 16:20:48 2022 +0200
6.2 +++ b/test/Tools/isac/Minisubpbl/150-add-given.sml Mon Aug 22 11:26:20 2022 +0200
6.3 @@ -66,4 +66,4 @@
6.4 case nxt of (Add_Given "solveFor x") => ()
6.5 | _ => error "minisubpbl: Add_Given is broken in root-problem";
6.6
6.7 -(*ctxt*)Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)
6.8 +Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)
7.1 --- a/test/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml Sun Aug 21 16:20:48 2022 +0200
7.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml Mon Aug 22 11:26:20 2022 +0200
7.3 @@ -95,4 +95,4 @@
7.4 | _ => error "Minisubplb/200-start-method-NEXT_STEP.sml CHANGED 1"
7.5 else error "Minisubplb/200-start-method-NEXT_STEP.sml CHANGED 2"
7.6
7.7 -(*ctxt*)Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)
7.8 +Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)
8.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml Sun Aug 21 16:20:48 2022 +0200
8.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml Mon Aug 22 11:26:20 2022 +0200
8.3 @@ -59,5 +59,5 @@
8.4 ) else error "Apply_Method [Test, squ-equ-test-subpbl1] changed p")
8.5 | _ => error "Apply_Method [Test, squ-equ-test-subpbl1] changed tac";
8.6
8.7 -(*ctxt*)Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)
8.8 +Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)
8.9
9.1 --- a/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Sun Aug 21 16:20:48 2022 +0200
9.2 +++ b/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Mon Aug 22 11:26:20 2022 +0200
9.3 @@ -73,7 +73,7 @@
9.4 val thy' = get_obj g_domID pt (par_pblobj pt p);
9.5 val (is, sc) = resume_prog thy' (p,p_) pt;
9.6
9.7 -"~~~~~ fun find_next_step , args:"; val ((thy, _), (ptp as (pt, (p, _))), sc, (Istate.Pstate ist, _(*ctxt*)))
9.8 +"~~~~~ fun find_next_step , args:"; val ((thy, _), (ptp as (pt, (p, _))), sc, (Istate.Pstate ist, _))
9.9 = ((thy',srls), (pt,pos), sc, is);
9.10
9.11 (*+*)val SOME t = parseNEW (get_ctxt pt pos) "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
9.12 @@ -85,4 +85,4 @@
9.13 Tactic.input_to_string nxt = "Rewrite_Set_Inst ([(''bdv'', x)], \"isolate_bdv\")"
9.14 then () else error "Minisubpbl/400-start-meth-subpbl changed";
9.15
9.16 -(*ctxt*)Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)
9.17 +Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)
10.1 --- a/test/Tools/isac/Minisubpbl/450-Rewrite_Set_Inst.sml Sun Aug 21 16:20:48 2022 +0200
10.2 +++ b/test/Tools/isac/Minisubpbl/450-Rewrite_Set_Inst.sml Mon Aug 22 11:26:20 2022 +0200
10.3 @@ -33,4 +33,4 @@
10.4 case nxt of (Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")) => ()
10.5 | _ => error "Rewrite_Set_Inst changed";
10.6
10.7 -(*ctxt*)Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)
10.8 +Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)
11.1 --- a/test/Tools/isac/Minisubpbl/470-Check_elementwise-NEXT_STEP.sml Sun Aug 21 16:20:48 2022 +0200
11.2 +++ b/test/Tools/isac/Minisubpbl/470-Check_elementwise-NEXT_STEP.sml Mon Aug 22 11:26:20 2022 +0200
11.3 @@ -98,4 +98,4 @@
11.4 (*+*) map UnparseC.term asm = []
11.5 (*+*)then () else error "Minisubpbl/470-Check_elementwise-NEXT_STEP.sml CHANGED";
11.6
11.7 -(*ctxt*)Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)
11.8 +Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)
12.1 --- a/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Sun Aug 21 16:20:48 2022 +0200
12.2 +++ b/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Mon Aug 22 11:26:20 2022 +0200
12.3 @@ -86,5 +86,5 @@
12.4 case nxt of ( Check_Postcond ["LINEAR", "univariate", "equation", "test"]) => ()
12.5 | _ => error "450-nxt-Check_Postcond broken";
12.6
12.7 -(*ctxt*)Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)
12.8 +Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)
12.9
13.1 --- a/test/Tools/isac/Minisubpbl/500-met-sub-to-root.sml Sun Aug 21 16:20:48 2022 +0200
13.2 +++ b/test/Tools/isac/Minisubpbl/500-met-sub-to-root.sml Mon Aug 22 11:26:20 2022 +0200
13.3 @@ -40,4 +40,4 @@
13.4 case nxt of (Check_elementwise "Assumptions") => ()
13.5 | _ => error "Check_elementwise changed; after switch sub-->root-method";
13.6
13.7 -(*ctxt*)Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)
13.8 +Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)
14.1 --- a/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Sun Aug 21 16:20:48 2022 +0200
14.2 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Mon Aug 22 11:26:20 2022 +0200
14.3 @@ -97,4 +97,4 @@
14.4 case nxt of (Check_elementwise "Assumptions") => ()
14.5 | _ => error "Check_elementwise changed; after switch sub-->root-method";
14.6
14.7 -(*ctxt*)Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)
14.8 +Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)
15.1 --- a/test/Tools/isac/Minisubpbl/600-postcond.sml Sun Aug 21 16:20:48 2022 +0200
15.2 +++ b/test/Tools/isac/Minisubpbl/600-postcond.sml Mon Aug 22 11:26:20 2022 +0200
15.3 @@ -37,5 +37,5 @@
15.4 | _ => error "calculation not finished correctly 1"
15.5 else error "calculation not finished correctly 2";
15.6
15.7 -(*ctxt*)Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)
15.8 +Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)
15.9
16.1 --- a/test/Tools/isac/Minisubpbl/700-interSteps.sml Sun Aug 21 16:20:48 2022 +0200
16.2 +++ b/test/Tools/isac/Minisubpbl/700-interSteps.sml Mon Aug 22 11:26:20 2022 +0200
16.3 @@ -172,5 +172,5 @@
16.4 (*". [x = 1]" only shown by Test_Tool.show_pt*)
16.5 then () else error "intermediate steps CHANGED";
16.6
16.7 -(*ctxt*)Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)
16.8 +Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)
16.9
17.1 --- a/test/Tools/isac/Minisubpbl/710-interSteps-short.sml Sun Aug 21 16:20:48 2022 +0200
17.2 +++ b/test/Tools/isac/Minisubpbl/710-interSteps-short.sml Mon Aug 22 11:26:20 2022 +0200
17.3 @@ -79,4 +79,4 @@
17.4 (*". [x = 1]" only by Test_Tool.show_pt_tac*)
17.5 then () else error "intermediate steps CHANGED";
17.6
17.7 -(*ctxt*)Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)
17.8 +Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)
18.1 --- a/test/Tools/isac/Minisubpbl/790-complete-NEXT_STEP.sml Sun Aug 21 16:20:48 2022 +0200
18.2 +++ b/test/Tools/isac/Minisubpbl/790-complete-NEXT_STEP.sml Mon Aug 22 11:26:20 2022 +0200
18.3 @@ -59,5 +59,5 @@
18.4 | _ => error "Minisubpbl/790-complete-NEXT_STEP.sml, WRONG RESULT CHANGED 2"
18.5 else error "Minisubpbl/790-complete-NEXT_STEP.sml, WRONG RESULT CHANGED 1";
18.6
18.7 -(*ctxt*)Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)
18.8 +Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)
18.9
19.1 --- a/test/Tools/isac/Minisubpbl/790-complete.sml Sun Aug 21 16:20:48 2022 +0200
19.2 +++ b/test/Tools/isac/Minisubpbl/790-complete.sml Mon Aug 22 11:26:20 2022 +0200
19.3 @@ -46,4 +46,4 @@
19.4 then case nxt of End_Proof' => () | _ => error "re-build: fun locate_input_tactic changed 1"
19.5 else error "re-build: fun locate_input_tactic changed";
19.6
19.7 -(*ctxt*)Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)
19.8 +Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)
20.1 --- a/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml Sun Aug 21 16:20:48 2022 +0200
20.2 +++ b/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml Mon Aug 22 11:26:20 2022 +0200
20.3 @@ -191,5 +191,5 @@
20.4 . . . . . . . . . . Check_Postcond ["sqroot-test", "univariate", "equation", "test"]]
20.5 *)
20.6
20.7 -(*ctxt*)Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)
20.8 +Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)
20.9
21.1 --- a/test/Tools/isac/Specify/cas-command.sml Sun Aug 21 16:20:48 2022 +0200
21.2 +++ b/test/Tools/isac/Specify/cas-command.sml Mon Aug 22 11:26:20 2022 +0200
21.3 @@ -15,3 +15,19 @@
21.4 "----------- start Calculation with CAS_Cmd ----------------------------------------------------";
21.5 "----------- start Calculation with CAS_Cmd ----------------------------------------------------";
21.6 "----------- start Calculation with CAS_Cmd ----------------------------------------------------";
21.7 +val fmz = [];
21.8 +val (dI',pI',mI') = References.empty;
21.9 +
21.10 + CalcTreeTEST [(fmz, (dI',pI',mI'))];
21.11 +"~~~~~ fun CalcTreeTEST, args:"; val [(fmz, sp): Formalise.T] = [(fmz, (dI',pI',mI'))];
21.12 +"~~~~~ fun nxt_specify_init_calc , args:"; val (fmz : Formalise.model, (dI, pI, mI) : References.T) = (fmz, sp);
21.13 + val thy = ThyC.get_theory dI;
21.14 + (*if*) mI = ["no_met"]; (*else*)
21.15 +(*+*)dI = "empty_thy_id";
21.16 +(*+*)pI = ["empty_probl_id"];
21.17 +(*+*)mI = ["empty_meth_id"];
21.18 +(*+* )
21.19 + ORGINALLY DONE IN test/../simplify.sml BY replaceFormula 1 "Simplify (2*a + 3*a)"
21.20 + after creation of the root Ctree.PblObj.
21.21 + REDESIGN NEEDED FOR Outer_Syntax.command \<^command_keyword>\<open>Example\<close>
21.22 +( **)
22.1 --- a/test/Tools/isac/Test_Isac_Short.thy Sun Aug 21 16:20:48 2022 +0200
22.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Mon Aug 22 11:26:20 2022 +0200
22.3 @@ -251,723 +251,6 @@
22.4 ML_file "Interpret/error-pattern.sml"
22.5 ML_file "Interpret/li-tool.sml"
22.6 ML_file "Interpret/lucas-interpreter.sml"
22.7 -ML \<open>
22.8 -\<close> ML \<open>
22.9 -\<close> ML \<open>
22.10 -(* Title: "Interpret/lucas-interpreter.sml"
22.11 - Author: Walther Neuper
22.12 - (c) due to copyright terms
22.13 -*)
22.14 -
22.15 -"-----------------------------------------------------------------------------------------------";
22.16 -"table of contents -----------------------------------------------------------------------------";
22.17 -"-----------------------------------------------------------------------------------------------";
22.18 -"----------- Take as 1st stac in program -------------------------------------------------------";
22.19 -"----------- re-build: fun locate_input_tactic -------------------------------------------------";
22.20 -"----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------";
22.21 -"----------- re-build: fun find_next_step, mini ------------------------------------------------";
22.22 -"----------- re-build: fun locate_input_term ---------------------------------------------------";
22.23 -"-----------------------------------------------------------------------------------------------";
22.24 -"-----------------------------------------------------------------------------------------------";
22.25 -"-----------------------------------------------------------------------------------------------";
22.26 -
22.27 -"----------- Take as 1st stac in program -------------------------------------------------------";
22.28 -"----------- Take as 1st stac in program -------------------------------------------------------";
22.29 -"----------- Take as 1st stac in program -------------------------------------------------------";
22.30 -"compare --- Apply_Method with initial Take by Step.do_next --- in test/../step-solve ----------";
22.31 -val p = e_pos'; val c = [];
22.32 -val (p,_,f,nxt,_,pt) =
22.33 - CalcTreeTEST
22.34 - [(["functionTerm (x \<up> 2 + 1)", "integrateBy x", "antiDerivative FF"],
22.35 - ("Integrate", ["integrate", "function"], ["diff", "integration"]))];
22.36 -val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Tac ", ...) --> Add_Given...*)
22.37 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
22.38 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
22.39 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
22.40 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
22.41 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
22.42 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
22.43 -case nxt of (Apply_Method ["diff", "integration"]) => ()
22.44 - | _ => error "integrate.sml -- me method [diff,integration] -- spec";
22.45 -"----- step 8: returns nxt = Rewrite_Set_Inst ([\"(''bdv'', x)\"],\"integration\")";
22.46 -
22.47 -"~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
22.48 -"~~~~~ fun Step.by_tactic, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
22.49 -val Applicable.Yes m = Step.check tac (pt, p);
22.50 - (*if*) Tactic.for_specify' m; (*false*)
22.51 -"~~~~~ fun loc_solve_ , args:"; val (m, (pt,pos)) = (m, ptp);
22.52 -
22.53 -"~~~~~ fun Step_Solve.by_tactic , args:"; val (m as Apply_Method' (mI, _, _, ctxt), (pt, (pos as (p,_))))
22.54 - = (m, (pt, pos));
22.55 - val {srls, ...} = MethodC.from_store mI;
22.56 - val itms = case get_obj I pt p of
22.57 - PblObj {meth=itms, ...} => itms
22.58 - | _ => error "solve Apply_Method: uncovered case get_obj"
22.59 - val thy' = get_obj g_domID pt p;
22.60 - val thy = ThyC.get_theory thy';
22.61 - val srls = LItool.get_simplifier (pt, pos)
22.62 - val (is, env, ctxt, sc) = case LItool.init_pstate srls ctxt itms mI of
22.63 - (is as Istate.Pstate {env, ...}, ctxt, sc) => (is, env, ctxt, sc)
22.64 - | _ => error "solve Apply_Method: uncovered case init_pstate";
22.65 -(*+*)pstate2str (the_pstate is) = "([\"\n(f_f, x \<up> 2 + 1)\",\"\n(v_v, x)\"], [], empty, NONE, \n??.empty, ORundef, false, true)";
22.66 - val ini = LItool.implicit_take sc env;
22.67 - val p = lev_dn p;
22.68 -
22.69 - val NONE = (*case*) ini (*of*);
22.70 - val Next_Step (is', ctxt', m') =
22.71 - LI.find_next_step sc (pt, (p, Res)) is ctxt;
22.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)";
22.73 - val Safe_Step (_, _, Take' _) = (*case*)
22.74 - locate_input_tactic sc (pt, (p, Res)) is' ctxt' m' (*of*);
22.75 -"~~~~~ fun locate_input_tactic , args:"; val ((Prog prog), cstate, istate, ctxt, tac)
22.76 - = (sc, (pt, (p, Res)), is', ctxt', m');
22.77 -
22.78 - (*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
22.79 -"~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
22.80 - = ((prog, (cstate, ctxt, tac)), istate);
22.81 - (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);
22.82 -
22.83 - val Accept_Tac1 (_, _, Take' _) =
22.84 - scan_dn1 cctt (ist |> set_path [R] |> set_or ORundef) (Program.body_of prog);
22.85 -"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const (\<^const_name>\<open>Let\<close>, _) $ e $ (Abs (id, T, b))))
22.86 - = (cctt, (ist |> set_path [R] |> set_or ORundef), (Program.body_of prog));
22.87 -
22.88 -(*+*) if UnparseC.term e = "Take (Integral f_f D v_v)" then () else error "scan_dn1 Integral changed";
22.89 -
22.90 - (*case*)
22.91 - scan_dn1 xxx (ist |> path_down [L, R]) e (*of*);
22.92 - (*======= end of scanning tacticals, a leaf =======*)
22.93 -"~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {eval, or, ...}), t)
22.94 - = (xxx, (ist |> path_down [L, R]), e);
22.95 -val (Program.Tac stac, a') = check_leaf "locate" ctxt eval (get_subst ist) t;
22.96 -
22.97 -
22.98 -
22.99 -"----------- re-build: fun locate_input_tactic -------------------------------------------------";
22.100 -"----------- re-build: fun locate_input_tactic -------------------------------------------------";
22.101 -"----------- re-build: fun locate_input_tactic -------------------------------------------------";
22.102 -val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
22.103 -val (dI',pI',mI') = ("Test", ["sqroot-test", "univariate", "equation", "test"],
22.104 - ["Test", "squ-equ-test-subpbl1"]);
22.105 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
22.106 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.107 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.108 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.109 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.110 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.111 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.112 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = (_, Apply_Method ["Test", "squ-equ-test-subpbl1"])*);
22.113 -(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Rewrite_Set", Rewrite_Set "norm_equation")*)
22.114 -
22.115 -(*//------------------ begin step into ------------------------------------------------------\\*)
22.116 -(*[1], Res*)val (p'''''_''',_,f,nxt'''''_''',_,pt'''''_''') = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
22.117 -
22.118 -"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt);
22.119 -
22.120 - (** )val (***)xxxx(***) ( *("ok", (_, _, (pt, p))) =( **) (*case*)
22.121 - Step.by_tactic tac (pt,p) (*of*);
22.122 -"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
22.123 - val Applicable.Yes m = (*case*) Solve_Step.check tac (pt, p) (*of*);
22.124 - (*if*) Tactic.for_specify' m; (*false*)
22.125 -
22.126 - (** )val (***)xxxxx_x(***) ( *(msg, cs') =( **)
22.127 -Step_Solve.by_tactic m ptp;
22.128 -"~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, ptp);
22.129 -(*+*)val (pt'''''_', (p'''''_', p_'''''_')) = (pt, (p, p_));
22.130 - (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p); (*else*)
22.131 - val thy' = get_obj g_domID pt (par_pblobj pt p);
22.132 - val (is, sc) = LItool.resume_prog thy' (p,p_) pt;
22.133 -
22.134 - locate_input_tactic sc (pt, po) (fst is) (snd is) m;
22.135 -"~~~~~ fun locate_input_tactic , args:"; val (Prog prog, cstate, istate, ctxt, tac)
22.136 - = (sc, (pt, po), (fst is), (snd is), m);
22.137 - val srls = get_simplifier cstate;
22.138 -
22.139 - (** )val Accept_Tac1 ((is as (_,_,_,_,_,strong_ass), ctxt, ss as((tac', _, ctree, pos', _) :: _))) =( **)
22.140 - (*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
22.141 -"~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
22.142 - = ((prog, (cstate, ctxt, tac)), istate);
22.143 - (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);
22.144 -
22.145 - (** )val xxxxx_xx = ( **)
22.146 - scan_dn1 cctt (ist |> set_path [R] |> set_or ORundef) (Program.body_of prog);
22.147 -"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const (\<^const_name>\<open>Let\<close>, _) $ e $ (Abs (id, T, b))))
22.148 - = (cctt, (ist |> set_path [R] |> set_or ORundef), (Program.body_of prog));
22.149 -
22.150 - (*case*) scan_dn1 xxx (ist |> path_down [L, R]) e (*of*);
22.151 -"~~~~~ fun scan_dn1 , args:"; val ((xxx as (cstate, _, _)), ist, (Const (\<^const_name>\<open>Chain\<close>(*1*), _) $ e1 $ e2 $ a))
22.152 - = (xxx, (ist |> path_down [L, R]), e);
22.153 -
22.154 - (*case*) scan_dn1 xxx (ist |> path_down_form ([L, L, R], a)) e1 (*of*);
22.155 -"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const (\<^const_name>\<open>Try\<close>(*2*), _) $ e))
22.156 - = (xxx, (ist |> path_down_form ([L, L, R], a)), e1);
22.157 -
22.158 - (*case*) scan_dn1 xxx (ist |> path_down [R]) e (*of*);
22.159 - (*======= end of scanning tacticals, a leaf =======*)
22.160 -"~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t)
22.161 - = (xxx, (ist |> path_down [R]), e);
22.162 - val (Program.Tac stac, a') =
22.163 - (*case*) check_leaf "locate" ctxt eval (get_subst ist) t (*of*);
22.164 - val LItool.Associated (m, v', ctxt) =
22.165 - (*case*) associate pt ctxt (m, stac) (*of*);
22.166 -
22.167 - Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m) (*return value*);
22.168 -"~~~~~ from scan_dn1 to scan_to_tactic1 return val:"; val (xxxxx_xx)
22.169 - = (Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m));
22.170 -
22.171 -"~~~~~ from scan_to_tactic1 to fun locate_input_tactic return val:"; val Accept_Tac1 ((ist as {assoc, ...}), ctxt, tac')
22.172 - = (Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m));
22.173 - (*if*) LibraryC.assoc (*then*);
22.174 -
22.175 - Safe_Step (Istate.Pstate ist, ctxt, tac') (*return value*);
22.176 -"~~~~~ from locate_input_tactic to fun Step_Solve.by_tactic return:"; val Safe_Step (istate, ctxt, tac)
22.177 - = (*xxxxx_xx*)(**)Safe_Step (Istate.Pstate ist, ctxt, tac')(**);
22.178 -
22.179 -(*+*)val (pt, po as (p, p_)) = (pt'''''_', (p'''''_', p_'''''_')); (* from begin of by_tactic *)
22.180 - val (p'', _, _,pt') =
22.181 - Step.add tac (istate, ctxt) (pt, (lev_on p, Pbl));
22.182 - (*in*)
22.183 -
22.184 - ("ok", ([(Tactic.input_from_T tac, tac, (p'', (istate, ctxt)))],
22.185 - [(*ctree NOT cut*)], (pt', p''))) (*return value*);
22.186 -"~~~~~ from Step_Solve.by_tactic \<longrightarrow> Step.by_tactic return:"; val ((msg, cs' : Calc.state_post))
22.187 - = ("ok", ([(Tactic.input_from_T tac, tac, (p'', (istate, ctxt)) )],
22.188 - [(*ctree NOT cut*)], (pt', p'')));
22.189 -
22.190 -"~~~~~ from Step.by_tactic to me return:"; val (("ok", (_, _, (pt, p)))) = (*** )xxxx( ***) ("ok", cs');
22.191 - val (_, ts) =
22.192 - (case Step.do_next p ((pt, Pos.e_pos'), []) of
22.193 - ("ok", (ts as (_, _, _) :: _, _, _)) => ("", ts)
22.194 - | ("helpless", _) => ("helpless: cannot propose tac", [])
22.195 - | ("no-fmz-spec", _) => error "no-fmz-spec"
22.196 - | ("end-of-calculation", (ts, _, _)) => ("", ts)
22.197 - | _ => error "me: uncovered case")
22.198 - handle ERROR msg => raise ERROR msg
22.199 - val tac =
22.200 - case ts of
22.201 - tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
22.202 - | _ => if p = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
22.203 -
22.204 - (p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Celem.Sundef, pt);
22.205 -"~~~~~ from me to TOOPLEVEL return:"; val (p,_,f,nxt,_,pt)
22.206 - = (*** )xxx( ***) (p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Celem.Sundef, pt);
22.207 -
22.208 -(*//--------------------- check results from modified me ----------------------------------\\*)
22.209 -if p = ([2], Res) andalso
22.210 - pr_ctree pr_short pt = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 = 2\n"
22.211 -then
22.212 - (case nxt of ("Rewrite_Set", Rewrite_Set "Test_simplify") => ()
22.213 - | _ => error "")
22.214 -else error "check results from modified me CHANGED";
22.215 -(*\\--------------------- check results from modified me ----------------------------------//*)
22.216 -
22.217 -"~~~~~ from me to TOPLEVEL return:"; val (p,_,f,nxt,_,pt) = (*** )xxx( ***) (**)(p, 000, f, nxt, 000, pt)(**);
22.218 -(*\\------------------ end step into --------------------------------------------------------//*)
22.219 -
22.220 -(*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt'''''_''' p'''''_''' [] pt'''''_'''; (*nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
22.221 -(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)
22.222 -(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (- 1 + x = 0)"*)
22.223 -(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor x"*)
22.224 -(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions x_i"*)
22.225 -(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Test"*)
22.226 -(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)
22.227 -(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["Test", "solve_linear"]*)
22.228 -(*[3], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
22.229 -(*[3, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)
22.230 -(*[3, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
22.231 -(*[3, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)
22.232 -(*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_elementwise "Assumptions"*)
22.233 -(*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)
22.234 -(*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*)
22.235 -
22.236 -(*/--------------------- final test ----------------------------------\\*)
22.237 -if p = ([], Res) andalso f2str f = "[x = 1]" andalso pr_ctree pr_short pt =
22.238 - ". ----- pblobj -----\n" ^
22.239 - "1. x + 1 = 2\n" ^
22.240 - "2. x + 1 + - 1 * 2 = 0\n" ^
22.241 - "3. ----- pblobj -----\n" ^
22.242 - "3.1. - 1 + x = 0\n" ^
22.243 - "3.2. x = 0 + - 1 * - 1\n" ^
22.244 - "4. [x = 1]\n"
22.245 -then case nxt of End_Proof' => () | _ => error "re-build: fun locate_input_tactic changed 1"
22.246 -else error "re-build: fun locate_input_tactic changed 2";
22.247 -
22.248 -
22.249 -"----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------";
22.250 -"----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------";
22.251 -"----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------";
22.252 -(*cp from -- try fun applyTactics ------- *)
22.253 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",
22.254 - "normalform N"],
22.255 - ("PolyMinus",["plus_minus", "polynom", "vereinfachen"],
22.256 - ["simplification", "for_polynomials", "with_minus"]))];
22.257 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.258 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.259 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.260 -(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "ordne_alphabetisch"*)
22.261 -
22.262 -(*+*)val Test_Out.FormKF "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12" = f
22.263 -
22.264 -(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "fasse_zusammen"*)
22.265 -
22.266 -(*+*)if map Tactic.input_to_string (specific_from_prog pt p) =
22.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\")",
22.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\")",
22.269 -(*this is new since ThmC.numerals_to_Free.-----\\*)
22.270 - "Calculate PLUS"]
22.271 - then () else error "specific_from_prog ([1], Res) 1 CHANGED";
22.272 -(*[2], Res*)val ("ok", (_, _, ptp as (pt, p))) = Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);
22.273 -
22.274 -(*+*)if map Tactic.input_to_string (specific_from_prog pt p) = [
22.275 - "Rewrite (\"tausche_minus\", \"\<lbrakk>?b ist_monom; ?a kleiner ?b\<rbrakk>\n\<Longrightarrow> ?b - ?a = - ?a + ?b\")",
22.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\")",
22.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\")",
22.278 - (*this is new since ThmC.numerals_to_Free.-----\\*)
22.279 - "Calculate PLUS",
22.280 - (*this is new since ThmC.numerals_to_Free.-----//*)
22.281 - "Calculate MINUS"]
22.282 - then () else error "specific_from_prog ([1], Res) 2 CHANGED";
22.283 -(* = ([3], Res)*)val ("ok", (_, _, ptp as (pt, p))) = Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);
22.284 -
22.285 -(*//----------------- exception PTREE "get_obj f EmptyPtree" raised --------------------------\\*)
22.286 -(**)val ("ok", ([(Rewrite ("tausche_minus", _), _, _)], _, _)) = (*isa*)
22.287 - Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);
22.288 -"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (hd (specific_from_prog pt p), (pt, p));
22.289 - val Applicable.Yes m = (*case*) Solve_Step.check tac (pt, p) (*of*);
22.290 - (*if*) Tactic.for_specify' m; (*false*)
22.291 -
22.292 -(**) val ("ok", ([(Rewrite ("tausche_minus", _), _, _)], _, _)) = (*isa*)
22.293 -Step_Solve.by_tactic m (pt, p);
22.294 -"~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, p));
22.295 - (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
22.296 - val thy' = get_obj g_domID pt (par_pblobj pt p);
22.297 - val (is, sc) = LItool.resume_prog thy' (p,p_) pt;
22.298 -
22.299 - (*case*) locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*);
22.300 -"~~~~~ fun locate_input_tactic , args:"; val ((Rule.Prog prog), (cstate as (pt, (*?*)pos(*?*))), istate, ctxt, tac)
22.301 - = (sc, (pt, po), (fst is), (snd is), m);
22.302 - val srls = LItool.get_simplifier cstate (*TODO: shift into Istate.T*);
22.303 -
22.304 - (*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
22.305 -"~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
22.306 - = ((prog, (cstate, ctxt, tac)), istate);
22.307 - (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*else*);
22.308 -
22.309 - go_scan_up1 (prog, cctt) ist;
22.310 -"~~~~~ fun go_scan_up1 , args:"; val ((pcct as (prog, _)), (ist as {path, ...}))
22.311 - = ((prog, cctt), ist);
22.312 - (*if*) 1 < length path (*then*);
22.313 -
22.314 - scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog);
22.315 -"~~~~~ and scan_up1 , args:"; val (pcct, ist, (Const (\<^const_name>\<open>Try\<close>(*2*), _) $ _))
22.316 - = (pcct, (ist |> path_up), (TermC.sub_at (path_up' path) prog));
22.317 -
22.318 - go_scan_up1 pcct ist;
22.319 -"~~~~~ and go_scan_up1 , args:"; val ((pcct as (prog, _)), (ist as {path, ...}))
22.320 - = (pcct, ist);
22.321 - (*if*) 1 < length path (*then*);
22.322 -
22.323 - scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog);
22.324 -"~~~~~ and scan_up1 , args:"; val ((pcct as (prog, cct as (cstate, _, _))), ist,
22.325 - (Const (\<^const_name>\<open>Chain\<close>(*3*), _) $ _ ))
22.326 - = (pcct, (ist |> path_up), (TermC.sub_at (path_up' path) prog));
22.327 - val e2 = check_Seq_up ist prog
22.328 -;
22.329 - (*case*) scan_dn1 cct (ist |> path_up_down [R] |> set_or ORundef) e2 (*of*);
22.330 -"~~~~~ fun scan_dn1 , args:"; val (yyy, ist, (Const (\<^const_name>\<open>Chain\<close>(*2*), _) $ e1 $ e2))
22.331 - = (cct, (ist |> path_up_down [R] |> set_or ORundef), e2);
22.332 -
22.333 - (*case*) scan_dn1 cct (ist |> path_down [L, R]) e1 (*of*);
22.334 -"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const (\<^const_name>\<open>Try\<close>(*2*), _) $ e))
22.335 - = (cct, (ist |> path_down [L, R]), e1);
22.336 -
22.337 -\<close> ML \<open>
22.338 - (*case*) scan_dn1 cct (ist |> path_down [R]) e (*of*);
22.339 - (*======= end of scanning tacticals, a leaf =======*)
22.340 -"~~~~~ fun scan_dn1 , args:"; val ((cct as (_, ctxt, _)), (ist as {eval, ...}), t)
22.341 - = (cct, (ist |> path_down [R]), e);
22.342 - (*if*) Tactical.contained_in t (*else*);
22.343 - val (Program.Tac prog_tac, form_arg) = (*case*)
22.344 - LItool.check_leaf "locate" ctxt eval (get_subst ist) t (*of*);
22.345 -
22.346 - check_tac1 cct ist (prog_tac, form_arg);
22.347 -"~~~~~ fun check_tac1 , args:"; val (((pt, p), ctxt, tac), (ist as {act_arg, or, ...}), (prog_tac, form_arg)) =
22.348 - (cct, ist, (prog_tac, form_arg));
22.349 -val LItool.Not_Associated = (*case*)
22.350 - LItool.associate pt ctxt (tac, prog_tac) (*of*);
22.351 - val _(*ORundef*) = (*case*) or (*of*);
22.352 -
22.353 -(*+*)Solve_Step.check (LItool.tac_from_prog pt (ThyC.get_theory "Isac_Knowledge") prog_tac) (pt, p);
22.354 -
22.355 - val Applicable.Yes m' =
22.356 - (*case*) Solve_Step.check (LItool.tac_from_prog pt (ThyC.get_theory "Isac_Knowledge") prog_tac) (pt, p) (*of*);
22.357 -
22.358 - Reject_Tac1 (ist |> set_subst_false (form_arg, Tactic.result m'), ctxt, tac)
22.359 - (*return from check_tac1*);
22.360 -"~~~~~ from fun check_tac1 \<longrightarrow>fun scan_dn1 \<longrightarrow>fun scan_dn1 \<longrightarrow>fun locate_input_tactic , return:"; val (Reject_Tac1 _) =
22.361 - (Reject_Tac1 (ist |> set_subst_false (form_arg, Tactic.result m'), ctxt, tac));
22.362 -
22.363 -val Test_Out.FormKF "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g" = f;
22.364 -val ([3], Res) = p;
22.365 -
22.366 -
22.367 -\<close> ML \<open>
22.368 -"----------- re-build: fun find_next_step, mini ------------------------------------------------";
22.369 -"----------- re-build: fun find_next_step, mini ------------------------------------------------";
22.370 -"----------- re-build: fun find_next_step, mini ------------------------------------------------";
22.371 -val fmz = ["Term (a + a ::real)", "normalform n_n"];
22.372 -val (dI',pI',mI') = ("Poly",["polynomial", "simplification"],["simplification", "for_polynomials"]);
22.373 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
22.374 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Model_Problem*)
22.375 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Specify_Theory "Poly"*)
22.376 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Specify_Problem ["polynomial", "simplification"]*)
22.377 -(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Method ["simplification", "for_polynomials"]*)
22.378 -(*1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Apply_Method ["simplification", "for_polynomials"]*)
22.379 -(*[1], Res*)val (_, ([(tac'''''_', _, _)], _, (pt'''''_', p'''''_'))) =
22.380 -
22.381 - Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set "norm_Poly"*)
22.382 -(*//------------------ go into 1 ------------------------------------------------------------\\*)
22.383 -"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
22.384 - = (p, ((pt, e_pos'), []));
22.385 - val pIopt = Ctree.get_pblID (pt, ip);
22.386 - (*if*) ip = ([], Res) (*else*);
22.387 - val _ = (*case*) tacis (*of*);
22.388 - val SOME _ = (*case*) pIopt (*of*);
22.389 - (*if*) member op = [Pos.Pbl, Pos.Met] p_ (*else*);
22.390 -
22.391 -val ("ok", ([(Rewrite_Set "norm_Poly", _, _)], _, (_, ([1], Res)))) =
22.392 -Step_Solve.do_next (pt, ip);
22.393 -"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
22.394 - (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
22.395 - val thy' = get_obj g_domID pt (par_pblobj pt p);
22.396 - val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
22.397 -
22.398 -val Next_Step (_, _, Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _)) =
22.399 - LI.find_next_step sc (pt, pos) ist ctxt (*of*);
22.400 -"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), (Pstate ist), ctxt)
22.401 - = (sc, (pt, pos), ist, ctxt);
22.402 -
22.403 -val Accept_Tac (Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _), _, _) =
22.404 - (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
22.405 -"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))
22.406 - = ((prog, (ptp, ctxt)), (Pstate ist));
22.407 - (*if*) path = [] (*then*);
22.408 -
22.409 -val Accept_Tac (Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _), _, _) =
22.410 - scan_dn cc (trans_scan_dn ist) (Program.body_of prog);
22.411 -"~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t)
22.412 - = (cc, (trans_scan_dn ist), (Program.body_of prog));
22.413 - (*if*) Tactical.contained_in t (*else*);
22.414 - val (Program.Tac prog_tac, form_arg) = (*case*) LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
22.415 -
22.416 -val Accept_Tac (Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _), _, _) =
22.417 - check_tac cc ist (prog_tac, form_arg) (*return from xxx*);
22.418 -"~~~~~ from fun scan_dn\<longrightarrow>fun scan_to_tactic\<longrightarrow>fun find_next_step, return:"; val (Accept_Tac (tac, ist, ctxt))
22.419 - = (check_tac cc ist (prog_tac, form_arg));
22.420 -
22.421 - Next_Step (Pstate ist, Tactic.insert_assumptions tac ctxt, tac) (*return from find_next_step*);
22.422 -"~~~~~ from fun find_next_step\<longrightarrow>and do_next\<longrightarrow>fun zzz, return:"; val (Next_Step (ist, ctxt, tac))
22.423 - = (Next_Step (Pstate ist, Tactic.insert_assumptions tac ctxt, tac));
22.424 -
22.425 - LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp (*return from and do_next*);
22.426 -"~~~~~ from and do_next\<longrightarrow>fun do_next\<longrightarrow>toplevel, return:"; val (_, ([(tac''''', _, _)], _, (pt''''', p''''')))
22.427 - = (LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp);
22.428 -(*\\------------------ end of go into 1 -----------------------------------------------------//*)
22.429 -
22.430 -(*[], Res*)val (_, ([(tac''''', _, _)], _, (pt''''', p'''''))) =
22.431 -
22.432 - Step.do_next p'''''_' ((pt'''''_', Pos.e_pos'), []);(* Check_Postcond ["polynomial", "simplification"]*)
22.433 -(*//------------------ go into 2 ------------------------------------------------------------\\*)
22.434 -"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
22.435 - = (p''''', ((pt''''', e_pos'), []));
22.436 - val pIopt = Ctree.get_pblID (pt, ip);
22.437 - (*if*) ip = ([], Res) (*else*);
22.438 - val _ = (*case*) tacis (*of*);
22.439 - val SOME _ = (*case*) pIopt (*of*);
22.440 - (*if*) member op = [Pos.Pbl, Pos.Met] p_ (*else*);
22.441 -
22.442 -val ("ok", ([(Check_Postcond ["polynomial", "simplification"], _, _)], _, (_, ([], Res)))) =
22.443 -Step_Solve.do_next (pt, ip);
22.444 -"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
22.445 - (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
22.446 - val thy' = get_obj g_domID pt (par_pblobj pt p);
22.447 - val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
22.448 -
22.449 - (** )val End_Program (ist, tac) =
22.450 - ( *case*) LI.find_next_step sc (pt, pos) ist ctxt (*of*);
22.451 -"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), (Pstate ist), ctxt)
22.452 - = (sc, (pt, pos), ist, ctxt);
22.453 -
22.454 -(* val Term_Val (Const (\<^const_name>\<open>times\<close>, _) $ Free ("2", _) $ Free ("a", _))*)
22.455 - (** )val Term_Val prog_result =
22.456 - ( *case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
22.457 -"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))
22.458 - = ((prog, (ptp, ctxt)), (Pstate ist));
22.459 - (*if*) path = [] (*else*);
22.460 -
22.461 - go_scan_up (prog, cc) (trans_scan_up ist |> set_found);
22.462 -"~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...}))
22.463 - = ((prog, cc), (trans_scan_up ist(*|> set_found !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *)));
22.464 - (*if*) path = [R] (*then*);
22.465 - (*if*) found_accept = true (*then*);
22.466 -
22.467 - Term_Val act_arg (*return from go_scan_up*);
22.468 -"~~~~~ from fun go_scan_up\<longrightarrow>fun scan_to_tactic, return:"; val (Term_Val prog_result) = (Term_Val act_arg);
22.469 -
22.470 - Term_Val prog_result (*return from scan_to_tactic*);
22.471 -"~~~~~ from fun scan_to_tactic\<longrightarrow>fun find_next_step, return:"; val (Term_Val prog_result) = (Term_Val prog_result);
22.472 - val (true, p', _) = (*case*) parent_node pt p (*of*);
22.473 - val (_, pblID, _) = get_obj g_spec pt p';
22.474 -
22.475 - End_Program (Pstate ist, Tactic.Check_Postcond' (pblID, prog_result))
22.476 - (*return from find_next_step*);
22.477 -"~~~~~ from fun find_next_step\<longrightarrow>and do_next\<longrightarrow>fun zzz, return:"; val (End_Program (ist, tac))
22.478 - = (End_Program (Pstate ist, Tactic.Check_Postcond' (pblID,prog_result)));
22.479 - val _ = (*case*) tac (*of*);
22.480 -
22.481 -val ("ok", ([(Check_Postcond ["polynomial", "simplification"], _, _)], _, (_, ([], Res))))
22.482 - = LI.by_tactic tac (ist, ctxt) ptp (*return from and do_next*);
22.483 -"~~~~~ from and do_next\<longrightarrow>top level, return:"; val (_, ([(tac''''', _, _)], _, (pt''''', p''''')))
22.484 - = (LI.by_tactic tac (ist, ctxt) ptp);
22.485 -(*\\------------------ end of go into 2 -----------------------------------------------------//*)
22.486 -
22.487 -(*[], Und*)val (msg, ([], _, (pt, p))) = Step.do_next p''''' ((pt''''', Pos.e_pos'), []);(**)
22.488 -
22.489 -Test_Tool.show_pt_tac pt; (*[
22.490 -([], Frm), Simplify (a + a)
22.491 -. . . . . . . . . . Apply_Method ["simplification", "for_polynomials"],
22.492 -([1], Frm), a + a
22.493 -. . . . . . . . . . Rewrite_Set "norm_Poly",
22.494 -([1], Res), 2 * a
22.495 -. . . . . . . . . . Check_Postcond ["polynomial", "simplification"],
22.496 -([], Res), 2 * a]*)
22.497 -
22.498 -(*/--- final test ---------------------------------------------------------------------------\\*)
22.499 -val (res, asm) = (get_obj g_result pt (fst p));
22.500 -if UnparseC.term res = "2 * a" andalso map UnparseC.term asm = []
22.501 -andalso p = ([], Und) andalso msg = "end-of-calculation"
22.502 -andalso pr_ctree pr_short pt = ". ----- pblobj -----\n1. a + a\n"
22.503 -then
22.504 - case tac''''' of Check_Postcond ["polynomial", "simplification"] => ()
22.505 - | _ => error "re-build: fun find_next_step, mini 1"
22.506 -else error "re-build: fun find_next_step, mini 2"
22.507 -
22.508 -
22.509 -"----------- re-build: fun locate_input_term ---------------------------------------------------";
22.510 -"----------- re-build: fun locate_input_term ---------------------------------------------------";
22.511 -"----------- re-build: fun locate_input_term ---------------------------------------------------";
22.512 -(*cp from inform.sml
22.513 - ----------- appendFormula: on Res + late deriv ------------------------------------------------*)
22.514 -val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
22.515 -val (dI',pI',mI') = ("Test", ["sqroot-test", "univariate", "equation", "test"],
22.516 - ["Test", "squ-equ-test-subpbl1"]);
22.517 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
22.518 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.519 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.520 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.521 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.522 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.523 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.524 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["Test", "squ-equ-test-subpbl1"]*);
22.525 -
22.526 -(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Rewrite_Set "norm_equation"*)
22.527 -(*+*)if f2str f = "x + 1 = 2" then () else error "locate_input_term at ([1], Frm) CHANGED";
22.528 -
22.529 -(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Rewrite_Set "Test_simplify"*)
22.530 -(*+*)if f2str f = "x + 1 + - 1 * 2 = 0" then () else error "locate_input_term at ([1], Frm) CHANGED";
22.531 -
22.532 -Test_Tool.show_pt_tac pt; (*[
22.533 -([], Frm), solve (x + 1 = 2, x)
22.534 -. . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
22.535 -([1], Frm), x + 1 = 2
22.536 -. . . . . . . . . . Rewrite_Set "norm_equation",
22.537 -([1], Res), x + 1 + - 1 * 2 = 0 ///Check_Postcond..ERROR*)
22.538 -
22.539 -\<close> ML \<open>
22.540 -(*//---------- appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term ----------\\*)
22.541 -"~~~~~ fun appendFormula , args:"; val ((*cI, *) ifo: TermC.as_string) = ((**) "x = 1");
22.542 - val cs = (*get_calc cI*) ((pt, p), [(*nxt, nxt_, (pos, (ist, ctxt))*)])
22.543 - val pos = (*get_pos cI 1*) p
22.544 -
22.545 -(*+*)val ptp''''' = (pt, p);
22.546 -(*+*)if snd ptp''''' = ([1], Res) then () else error "old_cs changed";
22.547 -(*+*)Test_Tool.show_pt_tac pt; (*[
22.548 -(*+*)([], Frm), solve (x + 1 = 2, x)
22.549 -(*+*). . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
22.550 -(*+*)([1], Frm), x + 1 = 2
22.551 -(*+*). . . . . . . . . . Rewrite_Set "norm_equation",
22.552 -(*+*)([1], Res), x + 1 + - 1 * 2 = 0 ///Check_Postcond*)
22.553 -
22.554 - val ("ok", cs' as (_, _, ptp')) =
22.555 - (*case*) Step.do_next pos cs (*of*);
22.556 -
22.557 -\<close> ML \<open>
22.558 -val ("ok", (_(*use in DG !!!*), [], ptp''''' as (pt''''', p'''''))) = (*case*)
22.559 -Step_Solve.by_term ptp' (encode ifo) (*of*);
22.560 -\<close> ML \<open>
22.561 -"~~~~~ fun by_term , args:"; val ((pt, pos as (p, _)), istr)
22.562 - = (ptp', (encode ifo));
22.563 -\<close> ML \<open>
22.564 - val SOME f_in =
22.565 - (*case*) TermC.parseNEW (get_ctxt pt pos) istr (*of*);
22.566 - val pos_pred = lev_back(*'*) pos
22.567 - val f_pred = Ctree.get_curr_formula (pt, pos_pred);
22.568 - val f_succ = Ctree.get_curr_formula (pt, pos);
22.569 - (*if*) f_succ = f_in (*else*);
22.570 - val NONE =
22.571 - (*case*) CAS_Cmd.input f_in (*of*);
22.572 -
22.573 -\<close> ML \<open>
22.574 -(*NEW*) LI.locate_input_term (pt, pos) f_in (*of*);
22.575 -\<close> ML \<open>
22.576 -"~~~~~ fun locate_input_term , args:"; val ((pt, pos), tm) = ((pt, pos), f_in);
22.577 - val pos_pred = Pos.lev_back' pos (*f_pred ---"step pos cs"---> f_succ in appendFormula*)
22.578 -
22.579 - \<close> ML \<open>
22.580 - val ("ok", (_, _, cstate as (pt', pos'))) =
22.581 - (*case*) compare_step ([], [], (pt, pos_pred)) tm (*of*);
22.582 -\<close> ML \<open>
22.583 -"~~~~~ fun compare_step , args:"; val ((tacis, c, ptp as (pt, pos as (p, _))), ifo) =
22.584 - (([], [], (pt, pos_pred)), tm);
22.585 - val fo = Calc.current_formula ptp
22.586 - val {nrls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
22.587 - val {rew_ord, erls, rules, ...} = Rule_Set.rep nrls
22.588 -\<close> ML \<open>
22.589 -(*+*)Proof_Context.theory_of (Ctree.get_ctxt pt pos) (*Isac.Test OK!*)
22.590 -\<close> ML \<open>
22.591 - val (found, der) = Derive.steps (Ctree.get_ctxt pt pos) rew_ord erls rules fo ifo; (*<---------------*)
22.592 -\<close> ML \<open>
22.593 - (*if*) found (*else*);
22.594 - (*if*) pos = ([], Pos.Res) (*else*);
22.595 -\<close> ML \<open>
22.596 - val msg_cs' as (_, (tacis, c', ptp)) = LI.do_next ptp; (*<---------------------*)
22.597 -\<close> ML \<open>
22.598 - (*case*) tacis (*of \<longrightarrow> [(Rewrite_Set "Test_simplify",...*) :State_Steps.T;
22.599 -\<close> ML \<open>
22.600 -
22.601 -(*+*) val ((input, tac, (pos, (ist, ctxt))) :: _) = tacis;
22.602 -(*+*) input (*= Tactic.Rewrite_Set "Test_simplify"*);
22.603 -(*+*) tac;
22.604 -(*+*) pos = ([2], Res);
22.605 -(*+*) ist;
22.606 -(*+*) Proof_Context.theory_of ctxt (*.., Isac.Test*);
22.607 -
22.608 -\<close> ML \<open>
22.609 - (*in*) compare_step (tacis, c @ c' (*@ c'' =c'BECAUSE OF | _ => msg_cs'*), ptp) ifo (*end*)
22.610 -\<close> ML \<open>
22.611 -"~~~~~ fun compare_step , args:"; val ((tacis, c, ptp as (pt, pos as (p, _))), ifo) =
22.612 - (([], [], (pt, pos_pred)), tm);
22.613 - val fo = Calc.current_formula ptp
22.614 - val {nrls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
22.615 - val {rew_ord, erls, rules, ...} = Rule_Set.rep nrls
22.616 -\<close> ML \<open>
22.617 - val (found, der) = Derive.steps (Ctree.get_ctxt pt pos) rew_ord erls rules fo ifo; (*<---------------*)
22.618 -\<close> ML \<open>
22.619 - (*if*) found (*else*);
22.620 - (*if*) pos = ([], Pos.Res) (*else*);
22.621 -\<close> ML \<open>
22.622 - val msg_cs' as (_, (tacis, c', ptp)) = LI.do_next ptp; (*<---------------------*)
22.623 -\<close> ML \<open>
22.624 -
22.625 -(*+*) val ((input, tac, (pos, (ist, ctxt))) :: _) = tacis;
22.626 -(*+*) input (*= Tactic.Rewrite_Set "Test_simplify"*);
22.627 -\<close> ML \<open>
22.628 -(*+*) tac;
22.629 -(*+*) pos = ([2], Res);
22.630 -(*+*) ist;
22.631 -(*+*) Proof_Context.theory_of ctxt (*.., Isac.Test*);
22.632 -
22.633 -\<close> ML \<open>
22.634 -\<close> ML \<open>
22.635 -\<close> ML \<open>
22.636 -Tactic.Apply_Method': MethodC.id * term option * Istate.T * Proof.context -> Tactic.T
22.637 -\<close> ML \<open>
22.638 -\<close> ML \<open>
22.639 -\<close> ML \<open>
22.640 -\<close> ML \<open>
22.641 -\<close> ML \<open>
22.642 -\<close> ML \<open>
22.643 -\<close> ML \<open>
22.644 -
22.645 -\<close> ML \<open> (*----- original..*)
22.646 -(*NEW*) Found_Step cstate (*return from locate_input_term*);
22.647 - (*LI.Found_Step ( *)cstate(*, _(*istate*), _(*ctxt*))( *return from locate_input_term*);
22.648 -"~~~~~ from fun locate_input_term\<longrightarrow>fun Step_Solve.by_term, return:"; val ("ok", (_(*use in DG !!!*), c, ptp as (_, p)))
22.649 - = (("ok" , ([], [], cstate (* already contains istate, ctxt *))));
22.650 -
22.651 - ("ok", ((*_ use in DG !!!,*) c, ptp(* as (_*), p))(*)*)(*return from Step_Solve.by_term*);
22.652 -"~~~~~ from fun Step_Solve.by_term\<longrightarrow>(fun appendFormula)!toplevel, return:"; val ("ok", (_(*use in DG !!!*), [], ptp''''' as (pt''''', p''''')))
22.653 - = ("ok", ([], [], ptp));
22.654 -
22.655 -\<close> ML \<open>
22.656 -(*fun me requires nxt...*)
22.657 - Step.do_next p''''' (ptp''''', []);
22.658 - val ("ok", ([(nxt'''''_' as Check_Postcond ["LINEAR", "univariate", "equation", "test"], _, _)], _,
22.659 - (pt'''''_', p'''''_'))) = Step.do_next p''''' (ptp''''', [])
22.660 -(*\\---------- appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term ----------//*)
22.661 -
22.662 -(*//----- REPLACED BY appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term -----\\* )
22.663 - (*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
22.664 - (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)
22.665 - (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (- 1 + x = 0)"*)
22.666 - (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor x"*)
22.667 - (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions x_i"*)
22.668 - (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Test"*)
22.669 - (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)
22.670 - (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["Test", "solve_linear"]*)
22.671 - (*[3], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
22.672 - (*[3, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)
22.673 - (*[3, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
22.674 - (*[3, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)
22.675 -( *\\----- REPLACED BY appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term -----//*)
22.676 -
22.677 - (*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt'''''_' p'''''_' [] pt'''''_'; (*nxt = Check_elementwise "Assumptions"*)
22.678 - (*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)
22.679 - (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*)
22.680 -
22.681 -\<close> ML \<open>
22.682 -(*/--- final test ---------------------------------------------------------------------------\\*)
22.683 -if p = ([], Res) andalso f2str f = "[x = 1]" andalso pr_ctree pr_short pt =
22.684 - ". ----- pblobj -----\n" ^
22.685 - "1. x + 1 = 2\n" ^
22.686 - "2. x + 1 + - 1 * 2 = 0\n" ^
22.687 - "3. ----- pblobj -----\n" ^
22.688 - "3.1. - 1 + x = 0\n" ^
22.689 - "3.2. x = 0 + - 1 * - 1\n" ^
22.690 - "3.2.1. x = 0 + - 1 * - 1\n" ^
22.691 - "3.2.2. x = 0 + 1\n" (*ATTENTION: see complete Calc below*)
22.692 -then case nxt of End_Proof' => () | _ => error "re-build: fun locate_input_term CHANGED 1"
22.693 -else error "re-build: fun locate_input_term CHANGED 2";
22.694 -
22.695 -Test_Tool.show_pt_tac pt; (*[
22.696 -([], Frm), solve (x + 1 = 2, x)
22.697 -. . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
22.698 -([1], Frm), x + 1 = 2
22.699 -. . . . . . . . . . Rewrite_Set "norm_equation",
22.700 -([1], Res), x + 1 + - 1 * 2 = 0
22.701 -. . . . . . . . . . Rewrite_Set "Test_simplify",
22.702 -([2], Res), - 1 + x = 0
22.703 -. . . . . . . . . . Subproblem (Test, ["LINEAR", "univariate", "equation", "test"]),
22.704 -([3], Pbl), solve (- 1 + x = 0, x)
22.705 -. . . . . . . . . . Apply_Method ["Test", "solve_linear"],
22.706 -([3,1], Frm), - 1 + x = 0
22.707 -. . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', x)], "isolate_bdv"),
22.708 -([3,1], Res), x = 0 + - 1 * - 1
22.709 -. . . . . . . . . . Derive Test_simplify,
22.710 -([3,2,1], Frm), x = 0 + - 1 * - 1
22.711 -. . . . . . . . . . Rewrite ("#: - 1 * - 1 = 1", "- 1 * - 1 = 1"),
22.712 -([3,2,1], Res), x = 0 + 1
22.713 -. . . . . . . . . . Rewrite ("radd_0", "0 + ?k = ?k"),
22.714 -([3,2,2], Res), x = 1
22.715 -. . . . . . . . . . Tactic.input_to_string not impl. for ?!,
22.716 -([3,2], Res), x = 1
22.717 -. . . . . . . . . . Check_Postcond ["LINEAR", "univariate", "equation", "test"],
22.718 -([3], Res), [x = 1]
22.719 -. . . . . . . . . . Check_Postcond ["sqroot-test", "univariate", "equation", "test"],
22.720 -([], Res), [x = 1]]*)
22.721 -\<close> ML \<open>
22.722 -\<close> ML \<open>
22.723 -\<close>
22.724 ML_file "Interpret/step-solve.sml"
22.725
22.726 ML_file "MathEngine/me-misc.sml"
22.727 @@ -991,12 +274,6 @@
22.728 ML_file "Knowledge/delete.sml"
22.729 ML_file "Knowledge/descript.sml"
22.730 ML_file "Knowledge/simplify.sml"
22.731 -ML \<open>
22.732 -\<close> ML \<open>
22.733 -\<close> ML \<open>
22.734 -\<close> ML \<open>
22.735 -\<close> ML \<open>
22.736 -\<close>
22.737 ML_file "Knowledge/poly-1.sml"
22.738 (*ML_file "Knowledge/poly-2.sml" Test_Isac_Short*)
22.739 ML_file "Knowledge/gcd_poly_ml.sml"
23.1 --- a/test/Tools/isac/Test_Some.thy Sun Aug 21 16:20:48 2022 +0200
23.2 +++ b/test/Tools/isac/Test_Some.thy Mon Aug 22 11:26:20 2022 +0200
23.3 @@ -108,716 +108,10 @@
23.4 \<close> ML \<open>
23.5 \<close>
23.6
23.7 -section \<open>===== "Specify/cas-command.sml" ==================================================\<close>
23.8 +section \<open>===================================================================================\<close>
23.9 ML \<open>
23.10 \<close> ML \<open>
23.11 \<close> ML \<open>
23.12 -"----------- start Calculation with CAS_Cmd ----------------------------------------------------";
23.13 -"----------- start Calculation with CAS_Cmd ----------------------------------------------------";
23.14 -"----------- start Calculation with CAS_Cmd ----------------------------------------------------";
23.15 -\<close> ML \<open>
23.16 -val fmz = [];
23.17 -val (dI',pI',mI') = References.empty;
23.18 -\<close> ML \<open>
23.19 -CalcTreeTEST [(fmz, (dI',pI',mI'))]
23.20 -\<close> ML \<open>
23.21 -"~~~~~ fun CalcTreeTEST, args:"; val [(fmz, sp): Formalise.T] = [(fmz, (dI',pI',mI'))];
23.22 -"~~~~~ fun nxt_specify_init_calc , args:"; val (fmz : Formalise.model, (dI, pI, mI) : References.T) = (fmz, sp);
23.23 - val thy = ThyC.get_theory dI;
23.24 -\<close> ML \<open>
23.25 - (*if*) mI = ["no_met"]; (*else*)
23.26 -\<close> ML \<open>
23.27 -dI = "empty_thy_id";
23.28 -\<close> ML \<open>
23.29 -pI = ["empty_probl_id"];
23.30 -\<close> ML \<open>
23.31 -mI = ["empty_meth_id"];
23.32 -\<close> ML \<open>
23.33 -\<close> ML \<open>
23.34 -\<close> ML \<open>
23.35 -\<close> ML \<open>
23.36 -\<close> text \<open>
23.37 -replaceFormula 1 "Simplify (2*a + 3*a)";
23.38 -\<close> ML \<open>
23.39 -\<close> ML \<open>
23.40 -\<close> ML \<open>
23.41 -\<close>
23.42 -
23.43 -section \<open>===== "Interpret/lucas-interpreter.sml" ==========================================\<close>
23.44 -ML \<open>
23.45 -\<close> ML \<open>
23.46 -\<close> ML \<open>
23.47 -(* Title: "Interpret/lucas-interpreter.sml"
23.48 - Author: Walther Neuper
23.49 - (c) due to copyright terms
23.50 -*)
23.51 -
23.52 -"-----------------------------------------------------------------------------------------------";
23.53 -"table of contents -----------------------------------------------------------------------------";
23.54 -"-----------------------------------------------------------------------------------------------";
23.55 -"----------- Take as 1st stac in program -------------------------------------------------------";
23.56 -"----------- re-build: fun locate_input_tactic -------------------------------------------------";
23.57 -"----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------";
23.58 -"----------- re-build: fun find_next_step, mini ------------------------------------------------";
23.59 -"----------- re-build: fun locate_input_term ---------------------------------------------------";
23.60 -"-----------------------------------------------------------------------------------------------";
23.61 -"-----------------------------------------------------------------------------------------------";
23.62 -"-----------------------------------------------------------------------------------------------";
23.63 -
23.64 -"----------- Take as 1st stac in program -------------------------------------------------------";
23.65 -"----------- Take as 1st stac in program -------------------------------------------------------";
23.66 -"----------- Take as 1st stac in program -------------------------------------------------------";
23.67 -"compare --- Apply_Method with initial Take by Step.do_next --- in test/../step-solve ----------";
23.68 -val p = e_pos'; val c = [];
23.69 -val (p,_,f,nxt,_,pt) =
23.70 - CalcTreeTEST
23.71 - [(["functionTerm (x \<up> 2 + 1)", "integrateBy x", "antiDerivative FF"],
23.72 - ("Integrate", ["integrate", "function"], ["diff", "integration"]))];
23.73 -val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Tac ", ...) --> Add_Given...*)
23.74 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
23.75 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
23.76 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
23.77 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
23.78 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
23.79 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
23.80 -case nxt of (Apply_Method ["diff", "integration"]) => ()
23.81 - | _ => error "integrate.sml -- me method [diff,integration] -- spec";
23.82 -"----- step 8: returns nxt = Rewrite_Set_Inst ([\"(''bdv'', x)\"],\"integration\")";
23.83 -
23.84 -"~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
23.85 -"~~~~~ fun Step.by_tactic, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
23.86 -val Applicable.Yes m = Step.check tac (pt, p);
23.87 - (*if*) Tactic.for_specify' m; (*false*)
23.88 -"~~~~~ fun loc_solve_ , args:"; val (m, (pt,pos)) = (m, ptp);
23.89 -
23.90 -"~~~~~ fun Step_Solve.by_tactic , args:"; val (m as Apply_Method' (mI, _, _, ctxt), (pt, (pos as (p,_))))
23.91 - = (m, (pt, pos));
23.92 - val {srls, ...} = MethodC.from_store mI;
23.93 - val itms = case get_obj I pt p of
23.94 - PblObj {meth=itms, ...} => itms
23.95 - | _ => error "solve Apply_Method: uncovered case get_obj"
23.96 - val thy' = get_obj g_domID pt p;
23.97 - val thy = ThyC.get_theory thy';
23.98 - val srls = LItool.get_simplifier (pt, pos)
23.99 - val (is, env, ctxt, sc) = case LItool.init_pstate srls ctxt itms mI of
23.100 - (is as Istate.Pstate {env, ...}, ctxt, sc) => (is, env, ctxt, sc)
23.101 - | _ => error "solve Apply_Method: uncovered case init_pstate";
23.102 -(*+*)pstate2str (the_pstate is) = "([\"\n(f_f, x \<up> 2 + 1)\",\"\n(v_v, x)\"], [], empty, NONE, \n??.empty, ORundef, false, true)";
23.103 - val ini = LItool.implicit_take sc env;
23.104 - val p = lev_dn p;
23.105 -
23.106 - val NONE = (*case*) ini (*of*);
23.107 - val Next_Step (is', ctxt', m') =
23.108 - LI.find_next_step sc (pt, (p, Res)) is ctxt;
23.109 -(*+*)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)";
23.110 - val Safe_Step (_, _, Take' _) = (*case*)
23.111 - locate_input_tactic sc (pt, (p, Res)) is' ctxt' m' (*of*);
23.112 -"~~~~~ fun locate_input_tactic , args:"; val ((Prog prog), cstate, istate, ctxt, tac)
23.113 - = (sc, (pt, (p, Res)), is', ctxt', m');
23.114 -
23.115 - (*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
23.116 -"~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
23.117 - = ((prog, (cstate, ctxt, tac)), istate);
23.118 - (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);
23.119 -
23.120 - val Accept_Tac1 (_, _, Take' _) =
23.121 - scan_dn1 cctt (ist |> set_path [R] |> set_or ORundef) (Program.body_of prog);
23.122 -"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const (\<^const_name>\<open>Let\<close>, _) $ e $ (Abs (id, T, b))))
23.123 - = (cctt, (ist |> set_path [R] |> set_or ORundef), (Program.body_of prog));
23.124 -
23.125 -(*+*) if UnparseC.term e = "Take (Integral f_f D v_v)" then () else error "scan_dn1 Integral changed";
23.126 -
23.127 - (*case*)
23.128 - scan_dn1 xxx (ist |> path_down [L, R]) e (*of*);
23.129 - (*======= end of scanning tacticals, a leaf =======*)
23.130 -"~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {eval, or, ...}), t)
23.131 - = (xxx, (ist |> path_down [L, R]), e);
23.132 -val (Program.Tac stac, a') = check_leaf "locate" ctxt eval (get_subst ist) t;
23.133 -
23.134 -
23.135 -
23.136 -"----------- re-build: fun locate_input_tactic -------------------------------------------------";
23.137 -"----------- re-build: fun locate_input_tactic -------------------------------------------------";
23.138 -"----------- re-build: fun locate_input_tactic -------------------------------------------------";
23.139 -val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
23.140 -val (dI',pI',mI') = ("Test", ["sqroot-test", "univariate", "equation", "test"],
23.141 - ["Test", "squ-equ-test-subpbl1"]);
23.142 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
23.143 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
23.144 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
23.145 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
23.146 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
23.147 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
23.148 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
23.149 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = (_, Apply_Method ["Test", "squ-equ-test-subpbl1"])*);
23.150 -(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Rewrite_Set", Rewrite_Set "norm_equation")*)
23.151 -
23.152 -(*//------------------ begin step into ------------------------------------------------------\\*)
23.153 -(*[1], Res*)val (p'''''_''',_,f,nxt'''''_''',_,pt'''''_''') = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
23.154 -
23.155 -"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt);
23.156 -
23.157 - (** )val (***)xxxx(***) ( *("ok", (_, _, (pt, p))) =( **) (*case*)
23.158 - Step.by_tactic tac (pt,p) (*of*);
23.159 -"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
23.160 - val Applicable.Yes m = (*case*) Solve_Step.check tac (pt, p) (*of*);
23.161 - (*if*) Tactic.for_specify' m; (*false*)
23.162 -
23.163 - (** )val (***)xxxxx_x(***) ( *(msg, cs') =( **)
23.164 -Step_Solve.by_tactic m ptp;
23.165 -"~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, ptp);
23.166 -(*+*)val (pt'''''_', (p'''''_', p_'''''_')) = (pt, (p, p_));
23.167 - (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p); (*else*)
23.168 - val thy' = get_obj g_domID pt (par_pblobj pt p);
23.169 - val (is, sc) = LItool.resume_prog thy' (p,p_) pt;
23.170 -
23.171 - locate_input_tactic sc (pt, po) (fst is) (snd is) m;
23.172 -"~~~~~ fun locate_input_tactic , args:"; val (Prog prog, cstate, istate, ctxt, tac)
23.173 - = (sc, (pt, po), (fst is), (snd is), m);
23.174 - val srls = get_simplifier cstate;
23.175 -
23.176 - (** )val Accept_Tac1 ((is as (_,_,_,_,_,strong_ass), ctxt, ss as((tac', _, ctree, pos', _) :: _))) =( **)
23.177 - (*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
23.178 -"~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
23.179 - = ((prog, (cstate, ctxt, tac)), istate);
23.180 - (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);
23.181 -
23.182 - (** )val xxxxx_xx = ( **)
23.183 - scan_dn1 cctt (ist |> set_path [R] |> set_or ORundef) (Program.body_of prog);
23.184 -"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const (\<^const_name>\<open>Let\<close>, _) $ e $ (Abs (id, T, b))))
23.185 - = (cctt, (ist |> set_path [R] |> set_or ORundef), (Program.body_of prog));
23.186 -
23.187 - (*case*) scan_dn1 xxx (ist |> path_down [L, R]) e (*of*);
23.188 -"~~~~~ fun scan_dn1 , args:"; val ((xxx as (cstate, _, _)), ist, (Const (\<^const_name>\<open>Chain\<close>(*1*), _) $ e1 $ e2 $ a))
23.189 - = (xxx, (ist |> path_down [L, R]), e);
23.190 -
23.191 - (*case*) scan_dn1 xxx (ist |> path_down_form ([L, L, R], a)) e1 (*of*);
23.192 -"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const (\<^const_name>\<open>Try\<close>(*2*), _) $ e))
23.193 - = (xxx, (ist |> path_down_form ([L, L, R], a)), e1);
23.194 -
23.195 - (*case*) scan_dn1 xxx (ist |> path_down [R]) e (*of*);
23.196 - (*======= end of scanning tacticals, a leaf =======*)
23.197 -"~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t)
23.198 - = (xxx, (ist |> path_down [R]), e);
23.199 - val (Program.Tac stac, a') =
23.200 - (*case*) check_leaf "locate" ctxt eval (get_subst ist) t (*of*);
23.201 - val LItool.Associated (m, v', ctxt) =
23.202 - (*case*) associate pt ctxt (m, stac) (*of*);
23.203 -
23.204 - Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m) (*return value*);
23.205 -"~~~~~ from scan_dn1 to scan_to_tactic1 return val:"; val (xxxxx_xx)
23.206 - = (Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m));
23.207 -
23.208 -"~~~~~ from scan_to_tactic1 to fun locate_input_tactic return val:"; val Accept_Tac1 ((ist as {assoc, ...}), ctxt, tac')
23.209 - = (Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m));
23.210 - (*if*) LibraryC.assoc (*then*);
23.211 -
23.212 - Safe_Step (Istate.Pstate ist, ctxt, tac') (*return value*);
23.213 -"~~~~~ from locate_input_tactic to fun Step_Solve.by_tactic return:"; val Safe_Step (istate, ctxt, tac)
23.214 - = (*xxxxx_xx*)(**)Safe_Step (Istate.Pstate ist, ctxt, tac')(**);
23.215 -
23.216 -(*+*)val (pt, po as (p, p_)) = (pt'''''_', (p'''''_', p_'''''_')); (* from begin of by_tactic *)
23.217 - val (p'', _, _,pt') =
23.218 - Step.add tac (istate, ctxt) (pt, (lev_on p, Pbl));
23.219 - (*in*)
23.220 -
23.221 - ("ok", ([(Tactic.input_from_T tac, tac, (p'', (istate, ctxt)))],
23.222 - [(*ctree NOT cut*)], (pt', p''))) (*return value*);
23.223 -"~~~~~ from Step_Solve.by_tactic \<longrightarrow> Step.by_tactic return:"; val ((msg, cs' : Calc.state_post))
23.224 - = ("ok", ([(Tactic.input_from_T tac, tac, (p'', (istate, ctxt)) )],
23.225 - [(*ctree NOT cut*)], (pt', p'')));
23.226 -
23.227 -"~~~~~ from Step.by_tactic to me return:"; val (("ok", (_, _, (pt, p)))) = (*** )xxxx( ***) ("ok", cs');
23.228 - val (_, ts) =
23.229 - (case Step.do_next p ((pt, Pos.e_pos'), []) of
23.230 - ("ok", (ts as (_, _, _) :: _, _, _)) => ("", ts)
23.231 - | ("helpless", _) => ("helpless: cannot propose tac", [])
23.232 - | ("no-fmz-spec", _) => error "no-fmz-spec"
23.233 - | ("end-of-calculation", (ts, _, _)) => ("", ts)
23.234 - | _ => error "me: uncovered case")
23.235 - handle ERROR msg => raise ERROR msg
23.236 - val tac =
23.237 - case ts of
23.238 - tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
23.239 - | _ => if p = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
23.240 -
23.241 - (p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Celem.Sundef, pt);
23.242 -"~~~~~ from me to TOOPLEVEL return:"; val (p,_,f,nxt,_,pt)
23.243 - = (*** )xxx( ***) (p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Celem.Sundef, pt);
23.244 -
23.245 -(*//--------------------- check results from modified me ----------------------------------\\*)
23.246 -if p = ([2], Res) andalso
23.247 - pr_ctree pr_short pt = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 = 2\n"
23.248 -then
23.249 - (case nxt of ("Rewrite_Set", Rewrite_Set "Test_simplify") => ()
23.250 - | _ => error "")
23.251 -else error "check results from modified me CHANGED";
23.252 -(*\\--------------------- check results from modified me ----------------------------------//*)
23.253 -
23.254 -"~~~~~ from me to TOPLEVEL return:"; val (p,_,f,nxt,_,pt) = (*** )xxx( ***) (**)(p, 000, f, nxt, 000, pt)(**);
23.255 -(*\\------------------ end step into --------------------------------------------------------//*)
23.256 -
23.257 -(*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt'''''_''' p'''''_''' [] pt'''''_'''; (*nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
23.258 -(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)
23.259 -(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (- 1 + x = 0)"*)
23.260 -(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor x"*)
23.261 -(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions x_i"*)
23.262 -(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Test"*)
23.263 -(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)
23.264 -(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["Test", "solve_linear"]*)
23.265 -(*[3], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
23.266 -(*[3, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)
23.267 -(*[3, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
23.268 -(*[3, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)
23.269 -(*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_elementwise "Assumptions"*)
23.270 -(*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)
23.271 -(*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*)
23.272 -
23.273 -(*/--------------------- final test ----------------------------------\\*)
23.274 -if p = ([], Res) andalso f2str f = "[x = 1]" andalso pr_ctree pr_short pt =
23.275 - ". ----- pblobj -----\n" ^
23.276 - "1. x + 1 = 2\n" ^
23.277 - "2. x + 1 + - 1 * 2 = 0\n" ^
23.278 - "3. ----- pblobj -----\n" ^
23.279 - "3.1. - 1 + x = 0\n" ^
23.280 - "3.2. x = 0 + - 1 * - 1\n" ^
23.281 - "4. [x = 1]\n"
23.282 -then case nxt of End_Proof' => () | _ => error "re-build: fun locate_input_tactic changed 1"
23.283 -else error "re-build: fun locate_input_tactic changed 2";
23.284 -
23.285 -
23.286 -"----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------";
23.287 -"----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------";
23.288 -"----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------";
23.289 -(*cp from -- try fun applyTactics ------- *)
23.290 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",
23.291 - "normalform N"],
23.292 - ("PolyMinus",["plus_minus", "polynom", "vereinfachen"],
23.293 - ["simplification", "for_polynomials", "with_minus"]))];
23.294 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
23.295 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
23.296 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
23.297 -(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "ordne_alphabetisch"*)
23.298 -
23.299 -(*+*)val Test_Out.FormKF "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12" = f
23.300 -
23.301 -(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "fasse_zusammen"*)
23.302 -
23.303 -(*+*)if map Tactic.input_to_string (specific_from_prog pt p) =
23.304 - ["Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_num; ?m is_num\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",
23.305 - "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_num; ?m is_num\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")",
23.306 -(*this is new since ThmC.numerals_to_Free.-----\\*)
23.307 - "Calculate PLUS"]
23.308 - then () else error "specific_from_prog ([1], Res) 1 CHANGED";
23.309 -(*[2], Res*)val ("ok", (_, _, ptp as (pt, p))) = Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);
23.310 -
23.311 -(*+*)if map Tactic.input_to_string (specific_from_prog pt p) = [
23.312 - "Rewrite (\"tausche_minus\", \"\<lbrakk>?b ist_monom; ?a kleiner ?b\<rbrakk>\n\<Longrightarrow> ?b - ?a = - ?a + ?b\")",
23.313 - "Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_num; ?m is_num\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",
23.314 - "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_num; ?m is_num\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")",
23.315 - (*this is new since ThmC.numerals_to_Free.-----\\*)
23.316 - "Calculate PLUS",
23.317 - (*this is new since ThmC.numerals_to_Free.-----//*)
23.318 - "Calculate MINUS"]
23.319 - then () else error "specific_from_prog ([1], Res) 2 CHANGED";
23.320 -(* = ([3], Res)*)val ("ok", (_, _, ptp as (pt, p))) = Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);
23.321 -
23.322 -(*//----------------- exception PTREE "get_obj f EmptyPtree" raised --------------------------\\*)
23.323 -(**)val ("ok", ([(Rewrite ("tausche_minus", _), _, _)], _, _)) = (*isa*)
23.324 - Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);
23.325 -"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (hd (specific_from_prog pt p), (pt, p));
23.326 - val Applicable.Yes m = (*case*) Solve_Step.check tac (pt, p) (*of*);
23.327 - (*if*) Tactic.for_specify' m; (*false*)
23.328 -
23.329 -(**) val ("ok", ([(Rewrite ("tausche_minus", _), _, _)], _, _)) = (*isa*)
23.330 -Step_Solve.by_tactic m (pt, p);
23.331 -"~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, p));
23.332 - (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
23.333 - val thy' = get_obj g_domID pt (par_pblobj pt p);
23.334 - val (is, sc) = LItool.resume_prog thy' (p,p_) pt;
23.335 -
23.336 - (*case*) locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*);
23.337 -"~~~~~ fun locate_input_tactic , args:"; val ((Rule.Prog prog), (cstate as (pt, (*?*)pos(*?*))), istate, ctxt, tac)
23.338 - = (sc, (pt, po), (fst is), (snd is), m);
23.339 - val srls = LItool.get_simplifier cstate (*TODO: shift into Istate.T*);
23.340 -
23.341 - (*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
23.342 -"~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
23.343 - = ((prog, (cstate, ctxt, tac)), istate);
23.344 - (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*else*);
23.345 -
23.346 - go_scan_up1 (prog, cctt) ist;
23.347 -"~~~~~ fun go_scan_up1 , args:"; val ((pcct as (prog, _)), (ist as {path, ...}))
23.348 - = ((prog, cctt), ist);
23.349 - (*if*) 1 < length path (*then*);
23.350 -
23.351 -\<close> ML \<open>
23.352 - scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog);
23.353 -"~~~~~ and scan_up1 , args:"; val (pcct, ist, (Const (\<^const_name>\<open>Try\<close>(*2*), _) $ _))
23.354 - = (pcct, (ist |> path_up), (TermC.sub_at (path_up' path) prog));
23.355 -
23.356 - go_scan_up1 pcct ist;
23.357 -"~~~~~ and go_scan_up1 , args:"; val ((pcct as (prog, _)), (ist as {path, ...}))
23.358 - = (pcct, ist);
23.359 - (*if*) 1 < length path (*then*);
23.360 -
23.361 - scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog);
23.362 -"~~~~~ and scan_up1 , args:"; val ((pcct as (prog, cct as (cstate, _, _))), ist,
23.363 - (Const (\<^const_name>\<open>Chain\<close>(*3*), _) $ _ ))
23.364 - = (pcct, (ist |> path_up), (TermC.sub_at (path_up' path) prog));
23.365 - val e2 = check_Seq_up ist prog
23.366 -;
23.367 - (*case*) scan_dn1 cct (ist |> path_up_down [R] |> set_or ORundef) e2 (*of*);
23.368 -"~~~~~ fun scan_dn1 , args:"; val (yyy, ist, (Const (\<^const_name>\<open>Chain\<close>(*2*), _) $ e1 $ e2))
23.369 - = (cct, (ist |> path_up_down [R] |> set_or ORundef), e2);
23.370 -
23.371 - (*case*) scan_dn1 cct (ist |> path_down [L, R]) e1 (*of*);
23.372 -"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const (\<^const_name>\<open>Try\<close>(*2*), _) $ e))
23.373 - = (cct, (ist |> path_down [L, R]), e1);
23.374 -
23.375 - (*case*) scan_dn1 cct (ist |> path_down [R]) e (*of*);
23.376 - (*======= end of scanning tacticals, a leaf =======*)
23.377 -"~~~~~ fun scan_dn1 , args:"; val ((cct as (_, ctxt, _)), (ist as {eval, ...}), t)
23.378 - = (cct, (ist |> path_down [R]), e);
23.379 - (*if*) Tactical.contained_in t (*else*);
23.380 - val (Program.Tac prog_tac, form_arg) = (*case*)
23.381 - LItool.check_leaf "locate" ctxt eval (get_subst ist) t (*of*);
23.382 -
23.383 - check_tac1 cct ist (prog_tac, form_arg);
23.384 -"~~~~~ fun check_tac1 , args:"; val (((pt, p), ctxt, tac), (ist as {act_arg, or, ...}), (prog_tac, form_arg)) =
23.385 - (cct, ist, (prog_tac, form_arg));
23.386 -val LItool.Not_Associated = (*case*)
23.387 - LItool.associate pt ctxt (tac, prog_tac) (*of*);
23.388 - val _(*ORundef*) = (*case*) or (*of*);
23.389 -
23.390 -(*+*)Solve_Step.check (LItool.tac_from_prog pt (ThyC.get_theory "Isac_Knowledge") prog_tac) (pt, p);
23.391 -
23.392 - val Applicable.Yes m' =
23.393 - (*case*) Solve_Step.check (LItool.tac_from_prog pt (ThyC.get_theory "Isac_Knowledge") prog_tac) (pt, p) (*of*);
23.394 -
23.395 - Reject_Tac1 (ist |> set_subst_false (form_arg, Tactic.result m'), ctxt, tac)
23.396 - (*return from check_tac1*);
23.397 -"~~~~~ from fun check_tac1 \<longrightarrow>fun scan_dn1 \<longrightarrow>fun scan_dn1 \<longrightarrow>fun locate_input_tactic , return:"; val (Reject_Tac1 _) =
23.398 - (Reject_Tac1 (ist |> set_subst_false (form_arg, Tactic.result m'), ctxt, tac));
23.399 -
23.400 -val Test_Out.FormKF "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g" = f;
23.401 -val ([3], Res) = p;
23.402 -
23.403 -
23.404 -"----------- re-build: fun find_next_step, mini ------------------------------------------------";
23.405 -"----------- re-build: fun find_next_step, mini ------------------------------------------------";
23.406 -"----------- re-build: fun find_next_step, mini ------------------------------------------------";
23.407 -val fmz = ["Term (a + a ::real)", "normalform n_n"];
23.408 -val (dI',pI',mI') = ("Poly",["polynomial", "simplification"],["simplification", "for_polynomials"]);
23.409 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
23.410 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Model_Problem*)
23.411 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Specify_Theory "Poly"*)
23.412 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Specify_Problem ["polynomial", "simplification"]*)
23.413 -(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Method ["simplification", "for_polynomials"]*)
23.414 -(*1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Apply_Method ["simplification", "for_polynomials"]*)
23.415 -(*[1], Res*)val (_, ([(tac'''''_', _, _)], _, (pt'''''_', p'''''_'))) =
23.416 -
23.417 - Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set "norm_Poly"*)
23.418 -(*//------------------ go into 1 ------------------------------------------------------------\\*)
23.419 -"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
23.420 - = (p, ((pt, e_pos'), []));
23.421 - val pIopt = Ctree.get_pblID (pt, ip);
23.422 - (*if*) ip = ([], Res) (*else*);
23.423 - val _ = (*case*) tacis (*of*);
23.424 - val SOME _ = (*case*) pIopt (*of*);
23.425 - (*if*) member op = [Pos.Pbl, Pos.Met] p_ (*else*);
23.426 -
23.427 -val ("ok", ([(Rewrite_Set "norm_Poly", _, _)], _, (_, ([1], Res)))) =
23.428 -Step_Solve.do_next (pt, ip);
23.429 -"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
23.430 - (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
23.431 - val thy' = get_obj g_domID pt (par_pblobj pt p);
23.432 - val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
23.433 -
23.434 -val Next_Step (_, _, Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _)) =
23.435 - LI.find_next_step sc (pt, pos) ist ctxt (*of*);
23.436 -"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), (Pstate ist), ctxt)
23.437 - = (sc, (pt, pos), ist, ctxt);
23.438 -
23.439 -val Accept_Tac (Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _), _, _) =
23.440 - (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
23.441 -"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))
23.442 - = ((prog, (ptp, ctxt)), (Pstate ist));
23.443 - (*if*) path = [] (*then*);
23.444 -
23.445 -val Accept_Tac (Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _), _, _) =
23.446 - scan_dn cc (trans_scan_dn ist) (Program.body_of prog);
23.447 -"~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t)
23.448 - = (cc, (trans_scan_dn ist), (Program.body_of prog));
23.449 - (*if*) Tactical.contained_in t (*else*);
23.450 - val (Program.Tac prog_tac, form_arg) = (*case*) LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
23.451 -
23.452 -val Accept_Tac (Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _), _, _) =
23.453 - check_tac cc ist (prog_tac, form_arg) (*return from xxx*);
23.454 -"~~~~~ from fun scan_dn\<longrightarrow>fun scan_to_tactic\<longrightarrow>fun find_next_step, return:"; val (Accept_Tac (tac, ist, ctxt))
23.455 - = (check_tac cc ist (prog_tac, form_arg));
23.456 -
23.457 - Next_Step (Pstate ist, Tactic.insert_assumptions tac ctxt, tac) (*return from find_next_step*);
23.458 -"~~~~~ from fun find_next_step\<longrightarrow>and do_next\<longrightarrow>fun zzz, return:"; val (Next_Step (ist, ctxt, tac))
23.459 - = (Next_Step (Pstate ist, Tactic.insert_assumptions tac ctxt, tac));
23.460 -
23.461 - LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp (*return from and do_next*);
23.462 -"~~~~~ from and do_next\<longrightarrow>fun do_next\<longrightarrow>toplevel, return:"; val (_, ([(tac''''', _, _)], _, (pt''''', p''''')))
23.463 - = (LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp);
23.464 -(*\\------------------ end of go into 1 -----------------------------------------------------//*)
23.465 -
23.466 -(*[], Res*)val (_, ([(tac''''', _, _)], _, (pt''''', p'''''))) =
23.467 -
23.468 - Step.do_next p'''''_' ((pt'''''_', Pos.e_pos'), []);(* Check_Postcond ["polynomial", "simplification"]*)
23.469 -(*//------------------ go into 2 ------------------------------------------------------------\\*)
23.470 -"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
23.471 - = (p''''', ((pt''''', e_pos'), []));
23.472 - val pIopt = Ctree.get_pblID (pt, ip);
23.473 - (*if*) ip = ([], Res) (*else*);
23.474 - val _ = (*case*) tacis (*of*);
23.475 - val SOME _ = (*case*) pIopt (*of*);
23.476 - (*if*) member op = [Pos.Pbl, Pos.Met] p_ (*else*);
23.477 -
23.478 -val ("ok", ([(Check_Postcond ["polynomial", "simplification"], _, _)], _, (_, ([], Res)))) =
23.479 -Step_Solve.do_next (pt, ip);
23.480 -"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
23.481 - (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
23.482 - val thy' = get_obj g_domID pt (par_pblobj pt p);
23.483 - val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
23.484 -
23.485 - (** )val End_Program (ist, tac) =
23.486 - ( *case*) LI.find_next_step sc (pt, pos) ist ctxt (*of*);
23.487 -"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), (Pstate ist), ctxt)
23.488 - = (sc, (pt, pos), ist, ctxt);
23.489 -
23.490 -(* val Term_Val (Const (\<^const_name>\<open>times\<close>, _) $ Free ("2", _) $ Free ("a", _))*)
23.491 - (** )val Term_Val prog_result =
23.492 - ( *case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
23.493 -"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))
23.494 - = ((prog, (ptp, ctxt)), (Pstate ist));
23.495 - (*if*) path = [] (*else*);
23.496 -
23.497 - go_scan_up (prog, cc) (trans_scan_up ist |> set_found);
23.498 -"~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...}))
23.499 - = ((prog, cc), (trans_scan_up ist(*|> set_found !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *)));
23.500 - (*if*) path = [R] (*then*);
23.501 - (*if*) found_accept = true (*then*);
23.502 -
23.503 - Term_Val act_arg (*return from go_scan_up*);
23.504 -"~~~~~ from fun go_scan_up\<longrightarrow>fun scan_to_tactic, return:"; val (Term_Val prog_result) = (Term_Val act_arg);
23.505 -
23.506 - Term_Val prog_result (*return from scan_to_tactic*);
23.507 -"~~~~~ from fun scan_to_tactic\<longrightarrow>fun find_next_step, return:"; val (Term_Val prog_result) = (Term_Val prog_result);
23.508 - val (true, p', _) = (*case*) parent_node pt p (*of*);
23.509 - val (_, pblID, _) = get_obj g_spec pt p';
23.510 -
23.511 - End_Program (Pstate ist, Tactic.Check_Postcond' (pblID, prog_result))
23.512 - (*return from find_next_step*);
23.513 -"~~~~~ from fun find_next_step\<longrightarrow>and do_next\<longrightarrow>fun zzz, return:"; val (End_Program (ist, tac))
23.514 - = (End_Program (Pstate ist, Tactic.Check_Postcond' (pblID,prog_result)));
23.515 - val _ = (*case*) tac (*of*);
23.516 -
23.517 -val ("ok", ([(Check_Postcond ["polynomial", "simplification"], _, _)], _, (_, ([], Res))))
23.518 - = LI.by_tactic tac (ist, ctxt) ptp (*return from and do_next*);
23.519 -"~~~~~ from and do_next\<longrightarrow>top level, return:"; val (_, ([(tac''''', _, _)], _, (pt''''', p''''')))
23.520 - = (LI.by_tactic tac (ist, ctxt) ptp);
23.521 -(*\\------------------ end of go into 2 -----------------------------------------------------//*)
23.522 -
23.523 -(*[], Und*)val (msg, ([], _, (pt, p))) = Step.do_next p''''' ((pt''''', Pos.e_pos'), []);(**)
23.524 -
23.525 -Test_Tool.show_pt_tac pt; (*[
23.526 -([], Frm), Simplify (a + a)
23.527 -. . . . . . . . . . Apply_Method ["simplification", "for_polynomials"],
23.528 -([1], Frm), a + a
23.529 -. . . . . . . . . . Rewrite_Set "norm_Poly",
23.530 -([1], Res), 2 * a
23.531 -. . . . . . . . . . Check_Postcond ["polynomial", "simplification"],
23.532 -([], Res), 2 * a]*)
23.533 -
23.534 -(*/--- final test ---------------------------------------------------------------------------\\*)
23.535 -val (res, asm) = (get_obj g_result pt (fst p));
23.536 -\<close> ML \<open>
23.537 -if UnparseC.term res = "2 * a" andalso map UnparseC.term asm = []
23.538 -andalso p = ([], Und) andalso msg = "end-of-calculation"
23.539 -andalso pr_ctree pr_short pt = ". ----- pblobj -----\n1. a + a\n"
23.540 -then
23.541 - case tac''''' of Check_Postcond ["polynomial", "simplification"] => ()
23.542 - | _ => error "re-build: fun find_next_step, mini 1"
23.543 -else error "re-build: fun find_next_step, mini 2"
23.544 -
23.545 -
23.546 -\<close> ML \<open>
23.547 -"----------- re-build: fun locate_input_term ---------------------------------------------------";
23.548 -"----------- re-build: fun locate_input_term ---------------------------------------------------";
23.549 -"----------- re-build: fun locate_input_term ---------------------------------------------------";
23.550 -(*cp from inform.sml
23.551 - ----------- appendFormula: on Res + late deriv ------------------------------------------------*)
23.552 -val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
23.553 -val (dI',pI',mI') = ("Test", ["sqroot-test", "univariate", "equation", "test"],
23.554 - ["Test", "squ-equ-test-subpbl1"]);
23.555 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
23.556 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
23.557 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
23.558 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
23.559 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
23.560 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
23.561 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
23.562 -\<close> ML \<open>
23.563 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["Test", "squ-equ-test-subpbl1"]*);
23.564 -
23.565 -(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Rewrite_Set "norm_equation"*)
23.566 -(*+*)if f2str f = "x + 1 = 2" then () else error "locate_input_term at ([1], Frm) CHANGED";
23.567 -
23.568 -(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Rewrite_Set "Test_simplify"*)
23.569 -(*+*)if f2str f = "x + 1 + - 1 * 2 = 0" then () else error "locate_input_term at ([1], Frm) CHANGED";
23.570 -
23.571 -Test_Tool.show_pt_tac pt; (*[
23.572 -([], Frm), solve (x + 1 = 2, x)
23.573 -. . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
23.574 -([1], Frm), x + 1 = 2
23.575 -. . . . . . . . . . Rewrite_Set "norm_equation",
23.576 -([1], Res), x + 1 + - 1 * 2 = 0 ///Check_Postcond..ERROR*)
23.577 -
23.578 -(*//---------- appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term ----------\\*)
23.579 -"~~~~~ fun appendFormula , args:"; val ((*cI, *) ifo: TermC.as_string) = ((**) "x = 1");
23.580 - val cs = (*get_calc cI*) ((pt, p), [(*nxt, nxt_, (pos, (ist, ctxt))*)])
23.581 - val pos = (*get_pos cI 1*) p
23.582 -
23.583 -\<close> ML \<open>
23.584 -(*+*)val ptp''''' = (pt, p);
23.585 -(*+*)if snd ptp''''' = ([1], Res) then () else error "old_cs changed";
23.586 -(*+*)Test_Tool.show_pt_tac pt; (*[
23.587 -(*+*)([], Frm), solve (x + 1 = 2, x)
23.588 -(*+*). . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
23.589 -(*+*)([1], Frm), x + 1 = 2
23.590 -(*+*). . . . . . . . . . Rewrite_Set "norm_equation",
23.591 -(*+*)([1], Res), x + 1 + - 1 * 2 = 0 ///Check_Postcond*)
23.592 -
23.593 - val ("ok", cs' as (_, _, ptp')) =
23.594 - (*case*) Step.do_next pos cs (*of*);
23.595 -
23.596 -\<close> ML \<open>
23.597 -val (pt, p) = ptp'
23.598 -\<close> ML \<open>
23.599 -Proof_Context.theory_of (Ctree.get_ctxt pt p) (*= Isac.Test*)
23.600 -\<close> ML \<open>
23.601 -ifo = "x = 1"
23.602 -\<close> ML \<open>
23.603 -(*+*)Step_Solve.by_term ptp' (encode ifo)
23.604 -(*Inner syntax error
23.605 -Failed to parse term*)
23.606 -\<close> ML \<open>
23.607 -val ("ok", (_(*use in DG !!!*), [], ptp''''' as (pt''''', p'''''))) = (*case*)
23.608 - Step_Solve.by_term ptp' (encode ifo) (*of*);
23.609 -"~~~~~ fun Step_Solve.by_term , args:"; val ((pt, pos as (p, _)), istr)
23.610 - = (ptp', (encode ifo));
23.611 -\<close> ML \<open>
23.612 - val SOME f_in =
23.613 - (*case*) TermC.parseNEW (get_ctxt pt pos) istr (*of*);
23.614 - val pos_pred = lev_back(*'*) pos
23.615 - val f_pred = Ctree.get_curr_formula (pt, pos_pred);
23.616 - val f_succ = Ctree.get_curr_formula (pt, pos);
23.617 - (*if*) f_succ = f_in (*else*);
23.618 - val NONE =
23.619 - (*case*) CAS_Cmd.input f_in (*of*);
23.620 -
23.621 -(*old* ) val (_, _, metID) = get_obj g_spec pt (par_pblobj pt p)
23.622 -(*old*) val {scr = prog, ...} = MethodC.from_store metID
23.623 -(*old*) val istate = get_istate_LI pt pos
23.624 -(*old*) val ctxt = get_ctxt pt pos
23.625 - val LI.Found_Step (cstate'''''_', _(*istate*), _(*ctxt*)) = (*case*)
23.626 - LI.locate_input_term prog (pt, pos) istate ctxt f_in (*of*);
23.627 -"~~~~~ fun locate_input_term , args:"; val ((Rule.Prog _), ((pt, pos) : Calc.T), (_ : Istate.T), (_ : Proof.context), tm)
23.628 - = (prog, (pt, pos), istate, ctxt, f_in);
23.629 -( *old*)
23.630 -
23.631 -\<close> ML \<open>
23.632 -(*NEW*) LI.locate_input_term (pt, pos) f_in (*of*);
23.633 -"~~~~~ fun locate_input_term , args:"; val ((pt, pos), tm) = ((pt, pos), f_in);
23.634 - val pos_pred = Pos.lev_back' pos (*f_pred ---"step pos cs"---> f_succ in appendFormula*)
23.635 -
23.636 - val ("ok", (_, _, cstate as (pt', pos'))) =
23.637 - (*case*) compare_step ([], [], (pt, pos_pred)) tm (*of*);
23.638 -
23.639 -(*old* )
23.640 - Found_Step (cstate, get_istate_LI pt' pos', get_ctxt pt' pos') (*return from locate_input_term*);
23.641 -( *old*)
23.642 -(*NEW*) Found_Step cstate (*return from locate_input_term*);
23.643 - (*LI.Found_Step ( *)cstate(*, _(*istate*), _(*ctxt*))( *return from locate_input_term*);
23.644 -"~~~~~ from fun locate_input_term\<longrightarrow>fun Step_Solve.by_term, return:"; val ("ok", (_(*use in DG !!!*), c, ptp as (_, p)))
23.645 - = (("ok" , ([], [], cstate (* already contains istate, ctxt *))));
23.646 -
23.647 - ("ok", ((*_ use in DG !!!,*) c, ptp(* as (_*), p))(*)*)(*return from Step_Solve.by_term*);
23.648 -"~~~~~ from fun Step_Solve.by_term\<longrightarrow>(fun appendFormula)!toplevel, return:"; val ("ok", (_(*use in DG !!!*), [], ptp''''' as (pt''''', p''''')))
23.649 - = ("ok", ([], [], ptp));
23.650 -
23.651 -(*fun me requires nxt...*)
23.652 - Step.do_next p''''' (ptp''''', []);
23.653 - val ("ok", ([(nxt'''''_' as Check_Postcond ["LINEAR", "univariate", "equation", "test"], _, _)], _,
23.654 - (pt'''''_', p'''''_'))) = Step.do_next p''''' (ptp''''', [])
23.655 -(*\\---------- appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term ----------//*)
23.656 -
23.657 -(*//----- REPLACED BY appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term -----\\* )
23.658 - (*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
23.659 - (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)
23.660 - (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (- 1 + x = 0)"*)
23.661 - (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor x"*)
23.662 - (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions x_i"*)
23.663 - (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Test"*)
23.664 - (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)
23.665 - (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["Test", "solve_linear"]*)
23.666 - (*[3], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
23.667 - (*[3, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)
23.668 - (*[3, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
23.669 - (*[3, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)
23.670 -( *\\----- REPLACED BY appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term -----//*)
23.671 -
23.672 - (*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt'''''_' p'''''_' [] pt'''''_'; (*nxt = Check_elementwise "Assumptions"*)
23.673 - (*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)
23.674 - (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*)
23.675 -
23.676 -\<close> ML \<open>
23.677 -(*/--- final test ---------------------------------------------------------------------------\\*)
23.678 -if p = ([], Res) andalso f2str f = "[x = 1]" andalso pr_ctree pr_short pt =
23.679 - ". ----- pblobj -----\n" ^
23.680 - "1. x + 1 = 2\n" ^
23.681 - "2. x + 1 + - 1 * 2 = 0\n" ^
23.682 - "3. ----- pblobj -----\n" ^
23.683 - "3.1. - 1 + x = 0\n" ^
23.684 - "3.2. x = 0 + - 1 * - 1\n" ^
23.685 - "3.2.1. x = 0 + - 1 * - 1\n" ^
23.686 - "3.2.2. x = 0 + 1\n" (*ATTENTION: see complete Calc below*)
23.687 -then case nxt of End_Proof' => () | _ => error "re-build: fun locate_input_term CHANGED 1"
23.688 -else error "re-build: fun locate_input_term CHANGED 2";
23.689 -
23.690 -Test_Tool.show_pt_tac pt; (*[
23.691 -([], Frm), solve (x + 1 = 2, x)
23.692 -. . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
23.693 -([1], Frm), x + 1 = 2
23.694 -. . . . . . . . . . Rewrite_Set "norm_equation",
23.695 -([1], Res), x + 1 + - 1 * 2 = 0
23.696 -. . . . . . . . . . Rewrite_Set "Test_simplify",
23.697 -([2], Res), - 1 + x = 0
23.698 -. . . . . . . . . . Subproblem (Test, ["LINEAR", "univariate", "equation", "test"]),
23.699 -([3], Pbl), solve (- 1 + x = 0, x)
23.700 -. . . . . . . . . . Apply_Method ["Test", "solve_linear"],
23.701 -([3,1], Frm), - 1 + x = 0
23.702 -. . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', x)], "isolate_bdv"),
23.703 -([3,1], Res), x = 0 + - 1 * - 1
23.704 -. . . . . . . . . . Derive Test_simplify,
23.705 -([3,2,1], Frm), x = 0 + - 1 * - 1
23.706 -. . . . . . . . . . Rewrite ("#: - 1 * - 1 = 1", "- 1 * - 1 = 1"),
23.707 -([3,2,1], Res), x = 0 + 1
23.708 -. . . . . . . . . . Rewrite ("radd_0", "0 + ?k = ?k"),
23.709 -([3,2,2], Res), x = 1
23.710 -. . . . . . . . . . Tactic.input_to_string not impl. for ?!,
23.711 -([3,2], Res), x = 1
23.712 -. . . . . . . . . . Check_Postcond ["LINEAR", "univariate", "equation", "test"],
23.713 -([3], Res), [x = 1]
23.714 -. . . . . . . . . . Check_Postcond ["sqroot-test", "univariate", "equation", "test"],
23.715 -([], Res), [x = 1]]*)
23.716 -\<close> ML \<open>
23.717 -\<close> ML \<open>
23.718 \<close> ML \<open>
23.719 \<close>
23.720