1.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Sat Feb 08 12:41:27 2020 +0100
1.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Sat Feb 08 14:44:24 2020 +0100
1.3 @@ -21,13 +21,17 @@
1.4 val locate_input_tactic: Program.T -> Calc.T -> Istate.T -> Proof.context
1.5 -> Tactic.T -> input_tactic_result
1.6
1.7 -(*TODO input_term_result = Found_Step of Calc.T | Not_Derivable *)
1.8 +(*NEW*)datatype input_term_result = Found_Step of Calc.T | Not_Derivable (**)
1.9 +(*old
1.10 datatype input_term_result =
1.11 Found_Step of Calc.T * Istate.T * Proof.context
1.12 - | Not_Derivable of Chead.calcstate' (*of message: contains errpatt!*)
1.13 -(*TODO locate_input_term: Calc.T -> term -> input_term_result *)
1.14 + | Not_Derivable of Chead.calcstate'
1.15 +*)
1.16 +(*NEW*)val locate_input_term: Calc.T -> term -> input_term_result (**)
1.17 +(*old
1.18 val locate_input_term: Program.T -> Calc.T -> Istate.T -> Proof.context -> term
1.19 -> input_term_result
1.20 +*)
1.21
1.22 (* must reside here:
1.23 find_next_step calls do_next and is called by by_tactic;
1.24 @@ -504,9 +508,7 @@
1.25
1.26 (*** locate an input formula in the program ***)
1.27
1.28 -datatype input_term_result =
1.29 - Found_Step of Calc.T * Istate.T * Proof.context
1.30 - | Not_Derivable of Chead.calcstate'
1.31 +datatype input_term_result = Found_Step of Calc.T | Not_Derivable
1.32
1.33 fun by_tactic (Tactic.Apply_Method' (mI, _, _, _)) (_, ctxt) (pt, pos as (p, _)) =
1.34 let
1.35 @@ -652,17 +654,17 @@
1.36 ALTERNATIVE: check_error_patterns _within_ compare_step: seems too expensive
1.37 *)
1.38 (* vvvv vvvvvv vvvv NEW args for compare_step *)
1.39 -fun locate_input_term (Rule.Prog _) ((pt, pos) : Calc.T) (_ : Istate.T) (_ : Proof.context) tm =
1.40 +fun locate_input_term (pt, pos) tm =
1.41 let
1.42 val pos_pred = Pos.lev_back' pos (*f_pred ---"step pos cs"---> f_succ in appendFormula*)
1.43 val _(*f_pred*) = Ctree.get_curr_formula (pt, pos_pred)
1.44 in
1.45 case compare_step ([], [], (pt, pos_pred)) tm of
1.46 - ("no derivation found", calcstate') => Not_Derivable calcstate'
1.47 + ("no derivation found", calcstate') => Not_Derivable
1.48 | ("ok", (_, _, cstate as (pt', pos'))) =>
1.49 - Found_Step (cstate, get_istate pt' pos', get_ctxt pt' pos')
1.50 + Found_Step cstate
1.51 | _ => raise ERROR "compare_step: uncovered case"
1.52 end
1.53 - | locate_input_term _ _ _ _ _ = raise ERROR "locate_input_term: uncovered case"
1.54 + | locate_input_term _ _ = raise ERROR "locate_input_term: uncovered case"
1.55
1.56 (**)end(**)
2.1 --- a/src/Tools/isac/MathEngine/solve.sml Sat Feb 08 12:41:27 2020 +0100
2.2 +++ b/src/Tools/isac/MathEngine/solve.sml Sat Feb 08 14:44:24 2020 +0100
2.3 @@ -132,7 +132,7 @@
2.4
2.5 fun inform (next_cs as (_, _, (pt, pos as (p, _))): Chead.calcstate') istr =
2.6 case TermC.parse (Celem.assoc_thy "Isac_Knowledge") istr of
2.7 - NONE => ("syntax error in '" ^ istr ^ "'", Chead.e_calcstate' (*TODO: previous cs'*))
2.8 + NONE => ("syntax error in '" ^ istr ^ "'", Chead.e_calcstate')
2.9 | SOME f_in =>
2.10 let
2.11 val f_in = Thm.term_of f_in
2.12 @@ -146,16 +146,18 @@
2.13 case Inform.cas_input f_in of
2.14 SOME (pt, _) => ("ok", ([], [], (pt, (p, Pos.Met))))
2.15 | NONE => (*/-------------------------------------- NEW fun locate_input_term------*)
2.16 +(*old
2.17 let
2.18 val (_, _, metID) = get_obj g_spec pt (par_pblobj pt p)
2.19 val {scr = prog, ...} = Specify.get_met metID
2.20 val istate = get_istate pt pos
2.21 val ctxt = get_ctxt pt pos
2.22 in
2.23 - case LI.locate_input_term prog (pt, pos) istate ctxt f_in of
2.24 - LI.Found_Step (cstate, _(*istate*), _(*ctxt*)) =>
2.25 +*)
2.26 + case LI.locate_input_term (pt, pos) f_in of
2.27 + LI.Found_Step cstate =>
2.28 ("ok" , ([], [], cstate (* already contains istate, ctxt *)))
2.29 - | LI.Not_Derivable calcstate' =>
2.30 + | LI.Not_Derivable =>
2.31 let
2.32 val pp = Ctree.par_pblobj pt p
2.33 val (errpats, nrls, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of
2.34 @@ -164,10 +166,12 @@
2.35 val {env, ...} = Ctree.get_istate pt pos |> Istate.the_pstate
2.36 in
2.37 case Inform.check_error_patterns (f_pred, f_in) (prog, env) (errpats, nrls) of
2.38 - SOME errpatID => ("error pattern #" ^ errpatID ^ "#", calcstate')
2.39 - | NONE => ("no derivation found", calcstate')
2.40 + SOME errpatID => ("error pattern #" ^ errpatID ^ "#", Chead.e_calcstate')
2.41 + | NONE => ("no derivation found", Chead.e_calcstate')
2.42 end
2.43 +(*old
2.44 end
2.45 +*)
2.46 end
2.47
2.48 end
2.49 \ No newline at end of file
3.1 --- a/test/Tools/isac/Interpret/inform.sml Sat Feb 08 12:41:27 2020 +0100
3.2 +++ b/test/Tools/isac/Interpret/inform.sml Sat Feb 08 14:44:24 2020 +0100
3.3 @@ -1024,12 +1024,13 @@
3.4 val f_pred = Ctree.get_curr_formula (pt, pos_pred);
3.5 (*if*) f_pred = f_in; (*else*)
3.6 val NONE = (*case*) Inform.cas_input f_in (*of*);
3.7 - (*NEW*)val (_, _, metID) = get_obj g_spec pt (par_pblobj pt p)
3.8 - (*NEW*)val {scr = prog, ...} = Specify.get_met metID
3.9 - (*NEW*)val istate = get_istate pt pos
3.10 - (*NEW*)val ctxt = get_ctxt pt pos
3.11 - val LI.Not_Derivable calcstate' =
3.12 - (*case*) LI.locate_input_term prog (pt, pos) istate ctxt f_in (*of*);
3.13 + (*old* )val (_, _, metID) = get_obj g_spec pt (par_pblobj pt p)
3.14 + (*old*)val {scr = prog, ...} = Specify.get_met metID
3.15 + (*old*)val istate = get_istate pt pos
3.16 + (*old*)val ctxt = get_ctxt pt pos
3.17 + ( *old*)
3.18 + val LI.Not_Derivable =
3.19 + (*case*) LI.locate_input_term (pt, pos) f_in (*of*);
3.20 val pp = Ctree.par_pblobj pt p
3.21 val (errpats, nrls, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of
3.22 {errpats, nrls, scr = Rule.Prog prog, ...} => (errpats, nrls, prog)
4.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Sat Feb 08 12:41:27 2020 +0100
4.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Sat Feb 08 14:44:24 2020 +0100
4.3 @@ -495,6 +495,154 @@
4.4 "----------- re-build: fun locate_input_term ---------------------------------------------------";
4.5 "----------- re-build: fun locate_input_term ---------------------------------------------------";
4.6 "----------- re-build: fun locate_input_term ---------------------------------------------------";
4.7 +(*cp from inform.sml
4.8 + ----------- appendFormula: on Res + late deriv ------------------------------------------------*)
4.9 +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
4.10 +val (dI',pI',mI') = ("Test", ["sqroot-test","univariate","equation","test"],
4.11 + ["Test","squ-equ-test-subpbl1"]);
4.12 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
4.13 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.14 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.15 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.16 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.17 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.18 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.19 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["Test", "squ-equ-test-subpbl1"]*);
4.20
4.21 +(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Rewrite_Set "norm_equation"*)
4.22 +(*+*)if f2str f = "x + 1 = 2" then () else error "locate_input_term at ([1], Frm) CHANGED";
4.23
4.24 +(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Rewrite_Set "Test_simplify"*)
4.25 +(*+*)if f2str f = "x + 1 + -1 * 2 = 0" then () else error "locate_input_term at ([1], Frm) CHANGED";
4.26
4.27 +show_pt_tac pt; (*[
4.28 +([], Frm), solve (x + 1 = 2, x)
4.29 +. . . . . . . . . . Apply_Method ["Test","squ-equ-test-subpbl1"],
4.30 +([1], Frm), x + 1 = 2
4.31 +. . . . . . . . . . Rewrite_Set "norm_equation",
4.32 +([1], Res), x + 1 + -1 * 2 = 0 ///Check_Postcond..ERROR*)
4.33 +
4.34 +(*//---------- appendFormula 1 "x = 1" \<longrightarrow> Solve.inform \<longrightarrow> LI.locate_input_term ----------\\*)
4.35 +"~~~~~ fun appendFormula , args:"; val ((*cI, *) ifo: Rule.cterm') = ((**) "x = 1");
4.36 + val cs = (*get_calc cI*) ((pt, p), [(*nxt, nxt_, (pos, (ist, ctxt))*)])
4.37 + val pos = (*get_pos cI 1*) p
4.38 +
4.39 +(*+*)val ptp''''' = (pt, p);
4.40 +(*+*)if snd ptp''''' = ([1], Res) then () else error "old_cs changed";
4.41 +(*+*)show_pt_tac pt; (*[
4.42 +(*+*)([], Frm), solve (x + 1 = 2, x)
4.43 +(*+*). . . . . . . . . . Apply_Method ["Test","squ-equ-test-subpbl1"],
4.44 +(*+*)([1], Frm), x + 1 = 2
4.45 +(*+*). . . . . . . . . . Rewrite_Set "norm_equation",
4.46 +(*+*)([1], Res), x + 1 + -1 * 2 = 0 ///Check_Postcond*)
4.47 +
4.48 + val ("ok", cs') =
4.49 + (*case*) Step.do_next pos cs (*of*);
4.50 +
4.51 +val ("ok", (_(*use in DG !!!*), [], ptp''''' as (pt''''', p'''''))) = (*case*)
4.52 + Solve.inform cs' (encode ifo) (*of*);
4.53 +"~~~~~ fun inform , args:"; val ((next_cs as (_, _, (pt, pos as (p, _))): Chead.calcstate'), istr)
4.54 + = (cs', (encode ifo));
4.55 + val SOME f_in =
4.56 + (*case*) TermC.parse (Celem.assoc_thy "Isac_Knowledge") istr (*of*);
4.57 + val f_in = Thm.term_of f_in
4.58 + val pos_pred = lev_back(*'*) pos
4.59 + val f_pred = Ctree.get_curr_formula (pt, pos_pred);
4.60 + val f_succ = Ctree.get_curr_formula (pt, pos);
4.61 + (*if*) f_succ = f_in (*else*);
4.62 + val NONE =
4.63 + (*case*) Inform.cas_input f_in (*of*);
4.64 +
4.65 +(*old* ) val (_, _, metID) = get_obj g_spec pt (par_pblobj pt p)
4.66 +(*old*) val {scr = prog, ...} = Specify.get_met metID
4.67 +(*old*) val istate = get_istate pt pos
4.68 +(*old*) val ctxt = get_ctxt pt pos
4.69 + val LI.Found_Step (cstate'''''_', _(*istate*), _(*ctxt*)) = (*case*)
4.70 + LI.locate_input_term prog (pt, pos) istate ctxt f_in (*of*);
4.71 +"~~~~~ fun locate_input_term , args:"; val ((Rule.Prog _), ((pt, pos) : Calc.T), (_ : Istate.T), (_ : Proof.context), tm)
4.72 + = (prog, (pt, pos), istate, ctxt, f_in);
4.73 +( *old*)
4.74 +
4.75 +(*NEW*) LI.locate_input_term (pt, pos) f_in (*of*);
4.76 +"~~~~~ fun locate_input_term , args:"; val ((pt, pos), tm) = ((pt, pos), f_in);
4.77 + val pos_pred = Pos.lev_back' pos (*f_pred ---"step pos cs"---> f_succ in appendFormula*)
4.78 +
4.79 + val ("ok", (_, _, cstate as (pt', pos'))) =
4.80 + (*case*) compare_step ([], [], (pt, pos_pred)) tm (*of*);
4.81 +
4.82 +(*old* )
4.83 + Found_Step (cstate, get_istate pt' pos', get_ctxt pt' pos') (*return from locate_input_term*);
4.84 +( *old*)
4.85 +(*NEW*) Found_Step cstate (*return from locate_input_term*);
4.86 + (*LI.Found_Step ( *)cstate(*, _(*istate*), _(*ctxt*))( *return from locate_input_term*);
4.87 +"~~~~~ from fun locate_input_term\<longrightarrow>fun inform, return:"; val ("ok", (_(*use in DG !!!*), c, ptp as (_, p)))
4.88 + = (("ok" , ([], [], cstate (* already contains istate, ctxt *))));
4.89 +
4.90 + ("ok", ((*_ use in DG !!!,*) c, ptp(* as (_*), p))(*)*)(*return from inform*);
4.91 +"~~~~~ from fun inform\<longrightarrow>(fun appendFormula)!toplevel, return:"; val ("ok", (_(*use in DG !!!*), [], ptp''''' as (pt''''', p''''')))
4.92 + = ("ok", ([], [], ptp));
4.93 +
4.94 +(*fun me requires nxt...*)
4.95 + Step.do_next p''''' (ptp''''', []);
4.96 + val ("ok", ([(nxt'''''_' as Check_Postcond ["LINEAR", "univariate", "equation", "test"], _, _)], _,
4.97 + (pt'''''_', p'''''_'))) = Step.do_next p''''' (ptp''''', [])
4.98 +(*\\---------- appendFormula 1 "x = 1" \<longrightarrow> Solve.inform \<longrightarrow> LI.locate_input_term ----------//*)
4.99 +
4.100 +(*//----- REPLACED BY appendFormula 1 "x = 1" \<longrightarrow> Solve.inform \<longrightarrow> LI.locate_input_term -----\\* )
4.101 + (*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
4.102 + (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)
4.103 + (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (-1 + x = 0)"*)
4.104 + (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor x"*)
4.105 + (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions x_i"*)
4.106 + (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Test"*)
4.107 + (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)
4.108 + (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["Test", "solve_linear"]*)
4.109 + (*[3], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
4.110 + (*[3, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)
4.111 + (*[3, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
4.112 + (*[3, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)
4.113 +( *\\----- REPLACED BY appendFormula 1 "x = 1" \<longrightarrow> Solve.inform \<longrightarrow> LI.locate_input_term -----//*)
4.114 +
4.115 + (*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt'''''_' p'''''_' [] pt'''''_'; (*nxt = Check_elementwise "Assumptions"*)
4.116 + (*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)
4.117 + (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*)
4.118 +
4.119 +(*/--- final test ---------------------------------------------------------------------------\\*)
4.120 +if p = ([], Res) andalso f2str f = "[x = 1]" andalso pr_ctree pr_short pt =
4.121 + ". ----- pblobj -----\n" ^
4.122 + "1. x + 1 = 2\n" ^
4.123 + "2. x + 1 + -1 * 2 = 0\n" ^
4.124 + "3. ----- pblobj -----\n" ^
4.125 + "3.1. -1 + x = 0\n" ^
4.126 + "3.2. x = 0 + -1 * -1\n" ^
4.127 + "3.2.1. x = 0 + -1 * -1\n" ^
4.128 + "3.2.2. x = 0 + 1\n" (*ATTENTION: see complete Calc below*)
4.129 +then case nxt of End_Proof' => () | _ => error "re-build: fun locate_input_term CHANGED 1"
4.130 +else error "re-build: fun locate_input_term CHANGED 2";
4.131 +
4.132 +show_pt_tac pt; (*[
4.133 +([], Frm), solve (x + 1 = 2, x)
4.134 +. . . . . . . . . . Apply_Method ["Test","squ-equ-test-subpbl1"],
4.135 +([1], Frm), x + 1 = 2
4.136 +. . . . . . . . . . Rewrite_Set "norm_equation",
4.137 +([1], Res), x + 1 + -1 * 2 = 0
4.138 +. . . . . . . . . . Rewrite_Set "Test_simplify",
4.139 +([2], Res), -1 + x = 0
4.140 +. . . . . . . . . . Subproblem (Test, ["LINEAR","univariate","equation","test"]),
4.141 +([3], Pbl), solve (-1 + x = 0, x)
4.142 +. . . . . . . . . . Apply_Method ["Test","solve_linear"],
4.143 +([3,1], Frm), -1 + x = 0
4.144 +. . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', x)], "isolate_bdv"),
4.145 +([3,1], Res), x = 0 + -1 * -1
4.146 +. . . . . . . . . . Derive Test_simplify,
4.147 +([3,2,1], Frm), x = 0 + -1 * -1
4.148 +. . . . . . . . . . Rewrite ("#: -1 * -1 = 1", "-1 * -1 = 1"),
4.149 +([3,2,1], Res), x = 0 + 1
4.150 +. . . . . . . . . . Rewrite ("radd_0", "0 + ?k = ?k"),
4.151 +([3,2,2], Res), x = 1
4.152 +. . . . . . . . . . tac2str not impl. for ?!,
4.153 +([3,2], Res), x = 1
4.154 +. . . . . . . . . . Check_Postcond ["LINEAR","univariate","equation","test"],
4.155 +([3], Res), [x = 1]
4.156 +. . . . . . . . . . Check_Postcond ["sqroot-test","univariate","equation","test"],
4.157 +([], Res), [x = 1]]*)
5.1 --- a/test/Tools/isac/Test_Some.thy Sat Feb 08 12:41:27 2020 +0100
5.2 +++ b/test/Tools/isac/Test_Some.thy Sat Feb 08 14:44:24 2020 +0100
5.3 @@ -80,175 +80,6 @@
5.4 \<close> ML \<open>
5.5 \<close>
5.6
5.7 -section \<open>==========--- re-build: fun locate_input_term ---> test/../lucas-interpreter.sml ==\<close>
5.8 -ML \<open>
5.9 -"----------- re-build: fun locate_input_term ---------------------------------------------------";
5.10 -"----------- re-build: fun locate_input_term ---------------------------------------------------";
5.11 -"----------- re-build: fun locate_input_term ---------------------------------------------------";
5.12 -(*cp from inform.sml
5.13 - ----------- appendFormula: on Res + late deriv ------------------------------------------------*)
5.14 -val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
5.15 -val (dI',pI',mI') = ("Test", ["sqroot-test","univariate","equation","test"],
5.16 - ["Test","squ-equ-test-subpbl1"]);
5.17 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
5.18 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.19 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.20 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.21 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.22 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.23 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.24 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["Test", "squ-equ-test-subpbl1"]*);
5.25 -
5.26 -(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Rewrite_Set "norm_equation"*)
5.27 -(*+*)if f2str f = "x + 1 = 2" then () else error "locate_input_term at ([1], Frm) CHANGED";
5.28 -
5.29 -(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Rewrite_Set "Test_simplify"*)
5.30 -(*+*)if f2str f = "x + 1 + -1 * 2 = 0" then () else error "locate_input_term at ([1], Frm) CHANGED";
5.31 -
5.32 -show_pt_tac pt; (*[
5.33 -([], Frm), solve (x + 1 = 2, x)
5.34 -. . . . . . . . . . Apply_Method ["Test","squ-equ-test-subpbl1"],
5.35 -([1], Frm), x + 1 = 2
5.36 -. . . . . . . . . . Rewrite_Set "norm_equation",
5.37 -([1], Res), x + 1 + -1 * 2 = 0 ///Check_Postcond..ERROR*)
5.38 -
5.39 -(*//---------- appendFormula 1 "x = 1" \<longrightarrow> Solve.inform \<longrightarrow> LI.locate_input_term ----------\\*)
5.40 -\<close> ML \<open>
5.41 -"~~~~~ fun appendFormula , args:"; val ((*cI, *) ifo: Rule.cterm') = ((**) "x = 1");
5.42 -\<close> ML \<open>
5.43 - val cs = (*get_calc cI*) ((pt, p), [(*nxt, nxt_, (pos, (ist, ctxt))*)])
5.44 - val pos = (*get_pos cI 1*) p
5.45 -\<close> ML \<open>
5.46 - val ("ok", cs') =
5.47 - (*case*) Step.do_next pos cs (*of*);
5.48 -\<close> ML \<open>
5.49 -(*+*) inform: calcstate' -> string -> string * calcstate';
5.50 -\<close> ML \<open>
5.51 -val ("ok", (_(*use in DG !!!*), [], ptp''''' as (pt''''', p'''''))) = (*case*)
5.52 - Solve.inform cs' (encode ifo) (*of*);
5.53 -\<close> ML \<open>
5.54 -"~~~~~ fun inform , args:"; val ((next_cs as (_, _, (pt, pos as (p, _))): Chead.calcstate'), istr)
5.55 - = (cs', (encode ifo));
5.56 -\<close> ML \<open>
5.57 - val SOME f_in =
5.58 - (*case*) TermC.parse (Celem.assoc_thy "Isac_Knowledge") istr (*of*);
5.59 -\<close> ML \<open>
5.60 - val f_in = Thm.term_of f_in
5.61 - val pos_pred = lev_back(*'*) pos
5.62 - val f_pred = Ctree.get_curr_formula (pt, pos_pred);
5.63 - val f_succ = Ctree.get_curr_formula (pt, pos);
5.64 -\<close> ML \<open>
5.65 - (*if*) f_succ = f_in (*else*);
5.66 -\<close> ML \<open>
5.67 - val NONE =
5.68 - (*case*) Inform.cas_input f_in (*of*);
5.69 -\<close> ML \<open>
5.70 -(*old* ) val (_, _, metID) = get_obj g_spec pt (par_pblobj pt p)
5.71 -(*old*) val {scr = prog, ...} = Specify.get_met metID
5.72 -(*old*) val istate = get_istate pt pos
5.73 -(*old*) val ctxt = get_ctxt pt pos
5.74 -( *old*)
5.75 -\<close> text \<open>(*old*)
5.76 - val LI.Found_Step (cstate'''''_', _(*istate*), _(*ctxt*)) = (*case*)
5.77 - LI.locate_input_term prog (pt, pos) istate ctxt f_in (*of*);
5.78 -\<close> text \<open>(*old*)
5.79 -"~~~~~ fun locate_input_term , args:"; val ((Rule.Prog _), ((pt, pos) : Calc.T), (_ : Istate.T), (_ : Proof.context), tm)
5.80 - = (prog, (pt, pos), istate, ctxt, f_in);
5.81 -\<close> text \<open>(*NEW*)
5.82 - LI.locate_input_term prog (pt, pos) f_in (*of*);
5.83 -\<close> ML \<open>(*NEW*)
5.84 -"~~~~~ fun locate_input_term , args:"; val ((pt, pos), tm) = ((pt, pos), f_in);
5.85 -\<close> ML \<open>
5.86 - val pos_pred = Pos.lev_back' pos (*f_pred ---"step pos cs"---> f_succ in appendFormula*)
5.87 -\<close> ML \<open>
5.88 - val ("ok", (_, _, cstate as (pt', pos'))) =
5.89 - (*case*) compare_step ([], [], (pt, pos_pred)) tm (*of*);
5.90 -\<close> ML \<open>(*old*)
5.91 - Found_Step (cstate, get_istate pt' pos', get_ctxt pt' pos') (*return from locate_input_term*);
5.92 -\<close> text \<open>(*NEW*)
5.93 - Found_Step cstate (*return from locate_input_term*);
5.94 -\<close> ML \<open>
5.95 - (*LI.Found_Step ( *)cstate(*, _(*istate*), _(*ctxt*))( *return from locate_input_term*);
5.96 -\<close> ML \<open>
5.97 -"~~~~~ from fun locate_input_term\<longrightarrow>fun inform, return:"; val ("ok", (_(*use in DG !!!*), c, ptp as (_, p)))
5.98 - = (("ok" , ([], [], cstate (* already contains istate, ctxt *))));
5.99 -\<close> ML \<open>
5.100 - ("ok", ((*_ use in DG !!!,*) c, ptp(* as (_*), p))(*)*)(*return from inform*);
5.101 -\<close> ML \<open>
5.102 -"~~~~~ from fun inform\<longrightarrow>(fun appendFormula)!toplevel, return:"; val ("ok", (_(*use in DG !!!*), [], ptp''''' as (pt''''', p''''')))
5.103 - = ("ok", ([], [], ptp));
5.104 -\<close> ML \<open>
5.105 -(*fun me requires nxt...*)
5.106 -\<close> ML \<open>
5.107 - Step.do_next p''''' (ptp''''', [])
5.108 -\<close> ML \<open>
5.109 - val ("ok", ([(nxt'''''_' as Check_Postcond ["LINEAR", "univariate", "equation", "test"], _, _)], _,
5.110 - (pt'''''_', p'''''_'))) = Step.do_next p''''' (ptp''''', [])
5.111 -\<close> ML \<open>
5.112 -(*\\---------- appendFormula 1 "x = 1" \<longrightarrow> Solve.inform \<longrightarrow> LI.locate_input_term ----------//*)
5.113 -\<close> ML \<open>
5.114 -(*//----- REPLACED BY appendFormula 1 "x = 1" \<longrightarrow> Solve.inform \<longrightarrow> LI.locate_input_term -----\\* )
5.115 - (*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
5.116 - (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)
5.117 - (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (-1 + x = 0)"*)
5.118 - (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor x"*)
5.119 - (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions x_i"*)
5.120 - (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Test"*)
5.121 - (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)
5.122 - (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["Test", "solve_linear"]*)
5.123 - (*[3], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
5.124 - (*[3, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)
5.125 - (*[3, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
5.126 - (*[3, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)
5.127 -( *\\----- REPLACED BY appendFormula 1 "x = 1" \<longrightarrow> Solve.inform \<longrightarrow> LI.locate_input_term -----//*)
5.128 -\<close> ML \<open>
5.129 - (*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt'''''_' p'''''_' [] pt'''''_'; (*nxt = Check_elementwise "Assumptions"*)
5.130 - (*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)
5.131 - (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*)
5.132 -\<close> ML \<open>
5.133 -(*/--- final test ---------------------------------------------------------------------------\\*)
5.134 -if p = ([], Res) andalso f2str f = "[x = 1]" andalso pr_ctree pr_short pt =
5.135 - ". ----- pblobj -----\n" ^
5.136 - "1. x + 1 = 2\n" ^
5.137 - "2. x + 1 + -1 * 2 = 0\n" ^
5.138 - "3. ----- pblobj -----\n" ^
5.139 - "3.1. -1 + x = 0\n" ^
5.140 - "3.2. x = 0 + -1 * -1\n" ^
5.141 - "3.2.1. x = 0 + -1 * -1\n" ^
5.142 - "3.2.2. x = 0 + 1\n" (*ATTENTION: see complete Calc below*)
5.143 -then case nxt of End_Proof' => () | _ => error "re-build: fun locate_input_term CHANGED 1"
5.144 -else error "re-build: fun locate_input_term CHANGED 2";
5.145 -\<close> ML \<open>
5.146 -show_pt_tac pt; (*[
5.147 -([], Frm), solve (x + 1 = 2, x)
5.148 -. . . . . . . . . . Apply_Method ["Test","squ-equ-test-subpbl1"],
5.149 -([1], Frm), x + 1 = 2
5.150 -. . . . . . . . . . Rewrite_Set "norm_equation",
5.151 -([1], Res), x + 1 + -1 * 2 = 0
5.152 -. . . . . . . . . . Rewrite_Set "Test_simplify",
5.153 -([2], Res), -1 + x = 0
5.154 -. . . . . . . . . . Subproblem (Test, ["LINEAR","univariate","equation","test"]),
5.155 -([3], Pbl), solve (-1 + x = 0, x)
5.156 -. . . . . . . . . . Apply_Method ["Test","solve_linear"],
5.157 -([3,1], Frm), -1 + x = 0
5.158 -. . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', x)], "isolate_bdv"),
5.159 -([3,1], Res), x = 0 + -1 * -1
5.160 -. . . . . . . . . . Derive Test_simplify,
5.161 -([3,2,1], Frm), x = 0 + -1 * -1
5.162 -. . . . . . . . . . Rewrite ("#: -1 * -1 = 1", "-1 * -1 = 1"),
5.163 -([3,2,1], Res), x = 0 + 1
5.164 -. . . . . . . . . . Rewrite ("radd_0", "0 + ?k = ?k"),
5.165 -([3,2,2], Res), x = 1
5.166 -. . . . . . . . . . tac2str not impl. for ?!,
5.167 -([3,2], Res), x = 1
5.168 -. . . . . . . . . . Check_Postcond ["LINEAR","univariate","equation","test"],
5.169 -([3], Res), [x = 1]
5.170 -. . . . . . . . . . Check_Postcond ["sqroot-test","univariate","equation","test"],
5.171 -([], Res), [x = 1]]*)
5.172 -
5.173 -\<close> ML \<open>
5.174 -\<close>
5.175 -
5.176 section \<open>===================================================================================\<close>
5.177 ML \<open>
5.178 \<close> ML \<open>