159 (*8*) autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); (*<---------------------- orig. test code*) |
159 (*8*) autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); (*<---------------------- orig. test code*) |
160 |
160 |
161 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1; (*<---------------------- orig. test code*) |
161 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1; (*<---------------------- orig. test code*) |
162 (*+isa=REP*) if p = ([1], Frm) andalso term2str (get_obj g_form pt [1]) = "1 + -1 * 2 + x = 0" |
162 (*+isa=REP*) if p = ([1], Frm) andalso term2str (get_obj g_form pt [1]) = "1 + -1 * 2 + x = 0" |
163 andalso istate2str (get_istate pt p) |
163 andalso istate2str (get_istate pt p) |
164 = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"],\n [], NONE,\n ??.empty, AppUndef_, true)" |
164 = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [], e_rls, NONE, \n??.empty, AppUndef_, true)" |
165 then () else error "refFormula = 1 + -1 * 2 + x = 0 changed"; |
165 then () else error "refFormula = 1 + -1 * 2 + x = 0 changed"; |
166 (*-------------------------------------------------------------------------*) |
166 (*-------------------------------------------------------------------------*) |
167 |
167 |
168 (*9*) fetchProposedTactic 1; (*<----------------------------------------------------- orig. test code*) |
168 (*9*) fetchProposedTactic 1; (*<----------------------------------------------------- orig. test code*) |
169 (*+\\------------------------------------------ isa == REP -----------------------------------//* ) |
169 (*+\\------------------------------------------ isa == REP -----------------------------------//* ) |
179 Rewrite_Set_Inst' _, (pos', (istate, ctxt))) ] , _, cstate)) = xxxxx_x; |
179 Rewrite_Set_Inst' _, (pos', (istate, ctxt))) ] , _, cstate)) = xxxxx_x; |
180 |
180 |
181 (*//******************* locatetac returns tac_ + istate + cstate *****************************\\*) |
181 (*//******************* locatetac returns tac_ + istate + cstate *****************************\\*) |
182 locatetac : Tactic.input -> state -> string * (taci list * pos' list * state); |
182 locatetac : Tactic.input -> state -> string * (taci list * pos' list * state); |
183 if istate2str istate |
183 if istate2str istate |
184 = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"],\n [R,L,R,L,R,L,R], (SOME e_e),\n x = 0 + -1 * (1 + -1 * 2), AppUndef_, true)" |
184 = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], e_rls, SOMEe_e, \nx = 0 + -1 * (1 + -1 * 2), AppUndef_, true)" |
185 then () else error "from locatetac return --- changed 1"; |
185 then () else error "from locatetac return --- changed 1"; |
186 |
186 |
187 if istate2str (get_istate (fst cstate) (snd cstate)) |
187 if istate2str (get_istate (fst cstate) (snd cstate)) |
188 = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"],\n [R,L,R,L,R,L,R], (SOME e_e),\n x = 0 + -1 * (1 + -1 * 2), AppUndef_, true)" |
188 = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], e_rls, SOMEe_e, \nx = 0 + -1 * (1 + -1 * 2), AppUndef_, true)" |
189 then () else error "from locatetac return --- changed 2"; |
189 then () else error "from locatetac return --- changed 2"; |
190 (*\\******************* locatetac returns tac_ + istate + cstate *****************************//*) |
190 (*\\******************* locatetac returns tac_ + istate + cstate *****************************//*) |
191 |
191 |
192 "~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt'''''_', ip'''''_')); |
192 "~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt'''''_', ip'''''_')); |
193 val (mI, m) = Solve.mk_tac'_ tac; |
193 val (mI, m) = Solve.mk_tac'_ tac; |
205 (*case*) LucinNEW.locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*); |
205 (*case*) LucinNEW.locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*); |
206 |
206 |
207 (*+*)Safe_Step: Istate.T * Proof.context * T -> input_tactic_result; |
207 (*+*)Safe_Step: Istate.T * Proof.context * T -> input_tactic_result; |
208 (********************* locate_input_tactic returns cstate * istate * Proof.context *************) |
208 (********************* locate_input_tactic returns cstate * istate * Proof.context *************) |
209 (*+*)if istate2str istate |
209 (*+*)if istate2str istate |
210 (*+isa*) = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"],\n [R,L,R,L,R,L,R], (SOME e_e),\n x = 0 + -1 * (1 + -1 * 2), AppUndef_, true)"(**) |
210 (*+isa*) = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], e_rls, SOMEe_e, \nx = 0 + -1 * (1 + -1 * 2), AppUndef_, true)" |
211 then case m of Rewrite_Set_Inst' _ => () |
211 then case m of Rewrite_Set_Inst' _ => () |
212 else error "from locate_input_tactic return --- changed"; |
212 else error "from locate_input_tactic return --- changed"; |
213 |
213 |
214 val ("ok", (tacis'''''_', _, _)) = xxxxx_x; |
214 val ("ok", (tacis'''''_', _, _)) = xxxxx_x; |
215 "~~~~~ from TOPLEVEL to states return:"; upd_calc cI ((pt'''''_', ip'''''_'), tacis'''''_'); |
215 "~~~~~ from TOPLEVEL to states return:"; upd_calc cI ((pt'''''_', ip'''''_'), tacis'''''_'); |
230 "~~~~~ fun step , args:"; val ((ip as (_, p_)), (ptp as (pt,p), tacis)) = (ip, cs); |
230 "~~~~~ fun step , args:"; val ((ip as (_, p_)), (ptp as (pt,p), tacis)) = (ip, cs); |
231 |
231 |
232 (*+isa==REP*)val [(Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv"), |
232 (*+isa==REP*)val [(Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv"), |
233 Rewrite_Set_Inst' _, (pos', (istate, ctxt)))] = tacis; |
233 Rewrite_Set_Inst' _, (pos', (istate, ctxt)))] = tacis; |
234 (*+*)if pos' = ([1], Res) andalso istate2str istate |
234 (*+*)if pos' = ([1], Res) andalso istate2str istate |
235 = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"],\n [R,L,R,L,R,L,R], (SOME e_e),\n x = 0 + -1 * (1 + -1 * 2), AppUndef_, true)" |
235 = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], e_rls, SOMEe_e, \nx = 0 + -1 * (1 + -1 * 2), AppUndef_, true)" |
236 then () else error "init. step 1 + -1 * 2 + x = 0 changed"; |
236 then () else error "init. step 1 + -1 * 2 + x = 0 changed"; |
237 |
237 |
238 val pIopt = get_pblID (pt,ip); |
238 val pIopt = get_pblID (pt,ip); |
239 (*if*) ip = ([], Ctree.Res);(*else*) |
239 (*if*) ip = ([], Ctree.Res);(*else*) |
240 val (_::_) = (*case*) tacis (*of*); |
240 val (_::_) = (*case*) tacis (*of*); |
242 (*val (pt',c',p') =*) Generate.generate tacis (pt,[],p); |
242 (*val (pt',c',p') =*) Generate.generate tacis (pt,[],p); |
243 (*//------------------------------------- final test -----------------------------------------\\*) |
243 (*//------------------------------------- final test -----------------------------------------\\*) |
244 val ("ok", [], ptp as (pt, p)) = xxxx; |
244 val ("ok", [], ptp as (pt, p)) = xxxx; |
245 |
245 |
246 if istate2str (get_istate pt p) (* <> <> <> <> ^^^^^^^^^^^^^*) |
246 if istate2str (get_istate pt p) (* <> <> <> <> ^^^^^^^^^^^^^*) |
247 (*REP*) = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"],\n [R,L,R,L,R,L,R], (SOME e_e),\n x = 0 + -1 * (1 + -1 * 2), AppUndef_, true)" |
247 (*REP*) = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], e_rls, SOMEe_e, \nx = 0 + -1 * (1 + -1 * 2), AppUndef_, true)" |
248 then () else error "REP autoCalculate on (e_e, 1 + -1 * 2 + x = 0) changed" |
248 then () else error "REP autoCalculate on (e_e, 1 + -1 * 2 + x = 0) changed" |
249 |
249 |
250 "~~~~~ from TOPLEVEL to states return:"; upd_calc cI (ptp, []); upd_ipos cI 1 p; |
250 "~~~~~ from TOPLEVEL to states return:"; upd_calc cI (ptp, []); upd_ipos cI 1 p; |
251 (*\\=========================================== isa <> REP (2) ===============================//*) |
251 (*\\=========================================== isa <> REP (2) ===============================//*) |
252 |
252 |