1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy Wed Dec 21 18:48:23 2022 +0100
1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy Thu Dec 22 10:27:12 2022 +0100
1.3 @@ -89,7 +89,7 @@
1.4 val insert_fillpats: (Thy_Write.theID * Error_Pattern_Def.fill_in list) list -> theory -> theory
1.5 val get_ref_last_thy: unit -> theory
1.6 val set_ref_last_thy: theory -> unit
1.7 - val get_via_last_thy: ThyC.id -> theory (* only used for Subproblem retrieving respective thy *)
1.8 + val get_via_last_thy: ThyC.id -> theory (*only used for (Sub-)problem retrieving respective thy*)
1.9 end;
1.10
1.11 structure Know_Store(**): KNOW_STORE(**) =
2.1 --- a/src/Tools/isac/BaseDefinitions/rule.sml Wed Dec 21 18:48:23 2022 +0100
2.2 +++ b/src/Tools/isac/BaseDefinitions/rule.sml Thu Dec 22 10:27:12 2022 +0100
2.3 @@ -58,7 +58,15 @@
2.4 fun distinct' rs = distinct equal rs
2.5
2.6 fun to_string Rule_Def.Erule = "Erule"
2.7 - | to_string (Rule_Def.Thm (str, thm)) = "Thm (\"" ^ str ^ "\", " ^ ThmC_Def.string_of_thm thm ^ ")"
2.8 + | to_string (Rule_Def.Thm (str, thm)) =
2.9 +(** )
2.10 + let
2.11 + val thy = Know_Store.get_ref_last_thy () ! ! !Know_Store defined later ! ! !
2.12 + in
2.13 +( **)
2.14 + "Thm (\"" ^ str ^ "\", " ^ ThmC_Def.string_of_thm thm ^ ")"
2.15 +(** )end( **)
2.16 +
2.17 | to_string (Rule_Def.Eval (str, _)) = "Eval (\"" ^ str ^ "\",fn)"
2.18 | to_string (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)"
2.19 | to_string (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ set_id rls ^ "\")";
3.1 --- a/src/Tools/isac/BaseDefinitions/unparseC.sml Wed Dec 21 18:48:23 2022 +0100
3.2 +++ b/src/Tools/isac/BaseDefinitions/unparseC.sml Thu Dec 22 10:27:12 2022 +0100
3.3 @@ -19,7 +19,6 @@
3.4 (*val term_opt: Proof.context -> term option -> term_as_string *)
3.5 val term_opt: term option -> term_as_string
3.6
3.7 -(*val terms: Proof.context -> term list -> term_as_string*)
3.8 val terms: term list -> term_as_string
3.9 (*replace by ^^^*)
3.10 val terms_in_ctxt: Proof.context -> term list -> term_as_string
4.1 --- a/src/Tools/isac/Build_Isac.thy Wed Dec 21 18:48:23 2022 +0100
4.2 +++ b/src/Tools/isac/Build_Isac.thy Thu Dec 22 10:27:12 2022 +0100
4.3 @@ -190,19 +190,264 @@
4.4 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/600-postcond.sml"
4.5 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/700-interSteps.sml"
4.6 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/710-interSteps-short.sml"
4.7 + ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/790-complete-NEXT_STEP.sml"
4.8 + ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/790-complete.sml"
4.9 (** )
4.10 - ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/790-complete-NEXT_STEP.sml"
4.11 + ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/800-append-on-Frm.sml"
4.12 ( **)
4.13 ML \<open>
4.14 \<close> ML \<open>
4.15 \<close> ML \<open>
4.16 +(* Title: "Minisubpbl/800-append-on-Frm.sml"
4.17 + Author: Walther Neuper
4.18 + (c) copyright due to lincense terms.
4.19 +*)
4.20 +
4.21 +"----------- Minisubpbl/800-append-on-Frm.sml ------------------------------------------------";
4.22 +"----------- Minisubpbl/800-append-on-Frm.sml ------------------------------------------------";
4.23 +"----------- Minisubpbl/800-append-on-Frm.sml ------------------------------------------------";
4.24 +(*cp from -- appendFormula: on Frm + equ_nrls --- in Interpret.inform.sml --------------------*)
4.25 +val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
4.26 +val (dI',pI',mI') =
4.27 + ("Test", ["sqroot-test", "univariate", "equation", "test"],
4.28 + ["Test", "squ-equ-test-subpbl1"]);
4.29 + (*[], Pbl*)val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];(*Model_Problem*)
4.30 + (*autoCalculate 1 CompleteCalcHead;*)
4.31 + (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Add_Given "equality (x + 1 = 2)"*)
4.32 + (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Add_Given "solveFor x"*)
4.33 + (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Add_Find "solutions L"*)
4.34 + (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Specify_Theory "Test"*)
4.35 + (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Specify_Problem ["sqroot-test", "univariate", "equation", "test"]*)
4.36 + (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Specify_Method ["Test", "squ-equ-test-subpbl1"]*)
4.37 + (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Apply_Method ["Test", "squ-equ-test-subpbl1"])*);
4.38 +
4.39 +\<close> ML \<open>
4.40 + (*autoCalculate 1 (Steps 1);*)
4.41 + (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Rewrite_Set", Rewrite_Set "norm_equation")*)
4.42 +
4.43 +(*+*)Test_Tool.show_pt_tac pt; (*isa==REP [
4.44 +([], Frm), solve (x + 1 = 2, x)
4.45 +. . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
4.46 +([1], Frm), x + 1 = 2
4.47 +. . . . . . . . . . Empty_Tac] *)
4.48 +
4.49 + (*appendFormula 1 "2+ - 1 + x = 2";*)
4.50 +"~~~~~ fun appendFormula , args:"; val (ifo) = ("2+ - 1 + x = 2");
4.51 + val cs = (*States.get_calc cI*) ((pt, p), []) (*..continue fun me*)
4.52 + val pos = (*States.get_pos cI 1*) p (*..continue fun me*)
4.53 +
4.54 + val ("ok", cs' as (_, _, ptp''''')) = (*case*)
4.55 + Step.do_next pos cs (*of*);
4.56 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (pos, cs);
4.57 + val pIopt = Ctree.get_pblID (pt, ip);
4.58 + (*if*) ip = ([], Pos.Res) (*else*);
4.59 + val _ = (*case*) tacis (*of*);
4.60 + val SOME _ = (*case*) pIopt (*of*);
4.61 +
4.62 + Step.switch_specify_solve p_ (pt, ip);
4.63 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
4.64 + (*if*) member op = [Pos.Pbl, Pos.Met] state_pos (*else*);
4.65 +
4.66 + LI.do_next (pt, input_pos);
4.67 +"~~~~~ and do_next , args:"; val ((ptp as (pt, pos as (p, p_)))) = (pt, input_pos);
4.68 + (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
4.69 + val thy' = get_obj g_domID pt (par_pblobj pt p);
4.70 + val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
4.71 +
4.72 +\<close> ML \<open>
4.73 +val Next_Step (ist, ctxt, tac) = (*case*) (**..Ctree NOT updated yet**)
4.74 + LI.find_next_step sc (pt, pos) ist ctxt (*of*);
4.75 +
4.76 +(*+*)val ("ok", ([(Rewrite_Set "norm_equation", _, (([1], Frm), _))], _, _)) =
4.77 + LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp;
4.78 +"~~~~~ fun by_tactic , args:"; val (tac_, is, (pt, pos)) = (tac, (ist, Tactic.insert_assumptions tac ctxt), ptp);
4.79 + val pos = next_in_prog' pos;
4.80 +
4.81 + (** )val (pos', c, _, pt) =( **)
4.82 + Step.add tac_ is (pt, pos);
4.83 +"~~~~~ fun add , args:"; val ((Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))), (is, ctxt), (pt, (p, _)))
4.84 + = (tac_, is, (pt, pos));
4.85 +(*+*)pos = ([1], Frm);
4.86 +
4.87 + (** )val (pt, c) =( **)
4.88 + cappend_atomic pt p (is, ContextC.insert_assumptions asm ctxt) f
4.89 + (Tactic.Rewrite_Set (Rule_Set.id rls')) (f',asm) Complete;
4.90 +"~~~~~ fun cappend_atomic , args:"; val (pt, p: pos, ic_res, f, r, f', s)
4.91 + = (pt, p, (is, ContextC.insert_assumptions asm ctxt), f,
4.92 + (Tactic.Rewrite_Set (Rule_Set.id rls')), (f',asm), Complete);
4.93 + (*if*) existpt p pt andalso Tactic.is_empty (get_obj g_tac pt p) (*then*);
4.94 + val (ic_form, f) = (get_loc pt (p, Frm), get_obj g_form pt p)
4.95 + val (pt, cs) = cut_tree(*!*)pt (p, Frm);
4.96 + (** )val pt = ( **)
4.97 + append_atomic p (SOME ic_form, ic_res) f r f' s pt;
4.98 +"~~~~~ fun append_atomic , args:"; val (p, (ic_form, ic_res), f, r, f', s, pt)
4.99 + = (p, (SOME ic_form, ic_res), f, r, f', s, pt);
4.100 + (*if*) existpt p pt andalso Tactic.is_empty (get_obj g_tac pt p) (*else*);
4.101 + val (iss, f) =
4.102 + ((ic_form, SOME ic_res), f); (*return from if*)
4.103 +
4.104 +\<close> ML \<open>
4.105 + insert_pt (PrfObj {form = f, tac = r, loc = iss, branch = NoBranch,
4.106 + result = f', ostate = s}) pt p (*return from append_atomic*);
4.107 +"~~~~~ from fun append_atomic \<longrightarrow>fun cappend_atomic , return:"; val (pt)
4.108 + = (insert_pt (PrfObj {form = f, tac = r, loc = iss, branch = NoBranch,
4.109 + result = f', ostate = s}) pt p);
4.110 +
4.111 +\<close> text \<open>
4.112 +(*/--------------------- step into Deriv.embed -----------------------------------------------\*)
4.113 + val ("ok", ([], _, ptp''''' as (_, ([1], Res)))) =
4.114 + (*case*)
4.115 +\<close> text \<open>
4.116 +Step_Solve.by_term ptp (encode ifo) (*of*);
4.117 +\<close> ML \<open>
4.118 +"~~~~~ fun by_term , args:"; val ((pt, pos as (p, _)), istr) = (ptp, (encode ifo));
4.119 + val SOME f_in =(*case*) TermC.parseNEW (get_ctxt pt pos) istr (*of*);
4.120 + val pos_pred = lev_back(*'*) pos
4.121 + val f_pred = Ctree.get_curr_formula (pt, pos_pred);
4.122 + val f_succ = Ctree.get_curr_formula (pt, pos);
4.123 + (*if*) f_succ = f_in (*else*);
4.124 + val NONE =(*case*) CAS_Cmd.input f_in (*of*);
4.125 +
4.126 +\<close> text \<open>
4.127 + (*case*)
4.128 + LI.locate_input_term (pt, pos) f_in (*of*);
4.129 +\<close> ML \<open>
4.130 +"~~~~~ fun locate_input_term , args:"; val ((pt, pos), tm) = ((pt, pos), f_in);
4.131 + val pos_pred = Pos.lev_back' pos (*f_pred ---"step pos cs"---> f_succ in appendFormula*)
4.132 + val _(*f_pred*) = Ctree.get_curr_formula (pt, pos_pred);
4.133 +
4.134 +\<close> text \<open>
4.135 + (*case*) compare_step ([], [], (pt, pos_pred)) tm (*of*);
4.136 +\<close> ML \<open>
4.137 +"~~~~~ fun compare_step , args:"; val ((tacis, c, ptp as (pt, pos as (p, _))), ifo) = (([], [], (pt, pos_pred)), tm);
4.138 + val fo = Calc.current_formula ptp
4.139 + val {rew_rls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
4.140 + val {rew_ord, asm_rls, rules, ...} = Rule_Set.rep rew_rls
4.141 +
4.142 +\<close> text \<open>
4.143 + val (found, der) =
4.144 + Derive.steps ctxt rew_ord asm_rls rules fo ifo; (*<---------------*)
4.145 +\<close> ML \<open> (*//----------- step into Derive.steps ----------------------------------------------\\*)
4.146 +(*//------------------ step into Derive.steps ----------------------------------------------\\*)
4.147 +"~~~~~ fun steps , args:"; val (ctxt, rew_ord, asm_rls, rules, fo, ifo) =
4.148 + (ctxt, rew_ord, asm_rls, rules, fo, ifo);
4.149 +\<close> ML \<open>
4.150 + fun derivat ([]:(term * Rule.rule * (term * term list)) list) = TermC.empty
4.151 + | derivat dt = (#1 o #3 o last_elem) dt
4.152 + fun equal (_, _, (t1, _)) (_, _, (t2, _)) = t1 = t2
4.153 + val fod = Derive.do_one ctxt asm_rls rules (snd rew_ord) NONE fo
4.154 + val ifod = Derive.do_one ctxt asm_rls rules (snd rew_ord) NONE ifo
4.155 +\<close> ML \<open>
4.156 +val (fod, ifod) =
4.157 + (*case*) (fod, ifod) (*of*);
4.158 +\<close> ML \<open>
4.159 + (*if*) derivat fod = derivat ifod (*common normal form found*) (*then*);
4.160 +\<close> ML \<open>
4.161 + val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod)
4.162 +\<close> ML \<open>
4.163 +(*/--- local to steps ---\*)
4.164 +fun rev_deriv' (t, r, (t', a)) = (t', ThmC.make_sym_rule r, (t, a));
4.165 +(*\--- local to steps ---/*)
4.166 +\<close> text \<open>
4.167 +val return = (true, fod' @ (map rev_deriv' rifod'))
4.168 +\<close> ML \<open>
4.169 +\<close> ML \<open>
4.170 +\<close> ML \<open>
4.171 +\<close> ML \<open>
4.172 +\<close> ML \<open>
4.173 +\<close> ML \<open>
4.174 +\<close> ML \<open>
4.175 +(*keep for continuing compare_step*)
4.176 +\<close> ML \<open> (*------------- continuing Derive.steps -----------------------------------------------*)
4.177 +(*-------------------- continuing Derive.steps -----------------------------------------------*)
4.178 +(*kept for continuing compare_step*)
4.179 +(*-------------------- stop step into Derive.steps -------------------------------------------*)
4.180 +\<close> ML \<open> (*------------- stop step into Derive.steps -------------------------------------------*)
4.181 +(*\\------------------ step into Derive.steps ----------------------------------------------//*)
4.182 +\<close> text \<open> (*\\----------- step into Derive.steps ----------------------------------------------//*)
4.183 + (*if*) found (*then*);
4.184 + val tacis' = map (State_Steps.make_single rew_ord asm_rls) der;
4.185 +
4.186 + val (c', ptp) =
4.187 + Derive.embed tacis' ptp;
4.188 +"~~~~~ fun embed , args:"; val (tacis, (pt, pos as (p, Res))) = (tacis', ptp);
4.189 + val (res, asm) = (State_Steps.result o last_elem) tacis
4.190 + val (ist, ctxt) = case Ctree.get_obj Ctree.g_loc pt p of
4.191 + (_, SOME (ist, ctxt)) => (ist, ctxt)
4.192 + | (_, NONE) => error "Derive.embed Frm: uncovered case get_obj"
4.193 + val (f, _) = Ctree.get_obj Ctree.g_result pt p
4.194 + val p = Pos.lev_on p(*---------------only difference to (..,Frm) above*);
4.195 + val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' f, ((p, Pos.Frm), (Istate_Def.Uistate, ctxt))) ::
4.196 + (State_Steps.insert_pos ((Pos.lev_on o Pos.lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm),
4.197 + (Pos.pos_plus (length tacis) (Pos.lev_dn p, Pos.Res), (Ctree.new_val res ist, ctxt)))];
4.198 + val {rew_rls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
4.199 + val (pt, c, pos as (p, _)) =
4.200 +
4.201 +Solve_Step.s_add_general (rev tacis) (pt, [], (p, Res));
4.202 +"~~~~~ fun s_add_general , args:"; val (tacis, (pt, c, _)) = ((rev tacis), (pt, [], (p, Res)));
4.203 +(*+*)length tacis = 8;
4.204 +(*+*)if State_Steps.to_string ctxt tacis = "[\"\n" ^
4.205 + "( End_Trans, End_Trans' xxx, ( ([2, 6], Res), Pstate ([\"\n(e_e, x + 1 = 2)\", \"\n" ^
4.206 + "(v_v, x)\"], [], empty, NONE, \n2 + - 1 + x = 2, ORundef, false, true) ))\", \"\n" ^
4.207 + "( Rewrite (\"sym_radd_commute\", \"?n + ?m = ?m + ?n\"), Rewrite' , ( ([2, 6], Res), Uistate ))\", \"\n" ^
4.208 + "( Rewrite (\"sym_radd_commute\", \"?n + ?m = ?m + ?n\"), Rewrite' , ( ([2, 5], Res), Uistate ))\", \"\n" ^
4.209 + "( Rewrite (\"sym_radd_left_commute\", \"?y + (?x + ?z) = ?x + (?y + ?z)\"), Rewrite' , ( ([2, 4], Res), Uistate ))\", \"\n" ^
4.210 + "( Rewrite (\"sym_radd_commute\", \"?n + ?m = ?m + ?n\"), Rewrite' , ( ([2, 3], Res), Uistate ))\", \"\n" ^
4.211 + "( Rewrite (\"#: 1 + x = - 1 + (2 + x)\", \"1 + x = - 1 + (2 + x)\"), Rewrite' , ( ([2, 2], Res), Uistate ))\", \"\n" ^
4.212 + "( Rewrite (\"radd_commute\", \"?m + ?n = ?n + ?m\"), Rewrite' , ( ([2, 1], Res), Uistate ))\", \"\n" ^
4.213 + "( Begin_Trans, Begin_Trans' xxx, ( ([2], Frm), Uistate ))\"]"
4.214 +(*+*)then () else error "Derive.embed CHANGED";
4.215 +
4.216 + val (tacis', (_, tac_, (p, is))) = split_last tacis
4.217 +
4.218 +(*+*)val Begin_Trans' _ = tac_;
4.219 +
4.220 + val (p',c',_,pt') = Specify_Step.add tac_ is (pt, p)
4.221 +(*-------------------- stop step into -------------------------------------------------------*)
4.222 +(*\------------------- end step into -------------------------------------------------------/*)
4.223 +
4.224 +(*/--------------------- final test ----------------------------------------------------------\*)
4.225 +val (SOME (Uistate, ctxt_frm), SOME (ist_res, ctxt_res)) = get_obj g_loc (fst ptp''''') (fst (snd ptp'''''))
4.226 +;
4.227 +if
4.228 + (ctxt_frm |> ContextC.get_assumptions |> UnparseC.terms_in_ctxt ctxt) = "[\"precond_rootmet x\"]"
4.229 + andalso
4.230 + (ctxt_res |> ContextC.get_assumptions |> UnparseC.terms_in_ctxt ctxt) = "[\"precond_rootmet x\"]"
4.231 + andalso
4.232 + Istate.string_of ist_res =
4.233 + "Pstate ([\"\n(e_e, x + 1 = 2)\", \"\n(v_v, x)\"], [], empty, NONE, \n2 + - 1 + x = 2, ORundef, false, true)"
4.234 +then () else error "/800-append-on-Frm.sml CHANGED";
4.235 +
4.236 +Test_Tool.show_pt_tac (fst ptp''''');(*[
4.237 +([], Frm), solve (x + 1 = 2, x)
4.238 +. . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
4.239 +([1], Frm), x + 1 = 2
4.240 +. . . . . . . . . . Derive Test_simplify,
4.241 +([1,1], Frm), x + 1 = 2
4.242 +. . . . . . . . . . Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
4.243 +([1,1], Res), 1 + x = 2
4.244 +. . . . . . . . . . Rewrite ("#: 1 + x = - 1 + (2 + x)", "1 + x = - 1 + (2 + x)"),
4.245 +([1,2], Res), - 1 + (2 + x) = 2
4.246 +. . . . . . . . . . Rewrite ("sym_radd_commute", "?n + ?m = ?m + ?n"),
4.247 +([1,3], Res), - 1 + (x + 2) = 2
4.248 +. . . . . . . . . . Rewrite ("sym_radd_left_commute", "?y + (?x + ?z) = ?x + (?y + ?z)"),
4.249 +([1,4], Res), x + (- 1 + 2) = 2
4.250 +. . . . . . . . . . Rewrite ("sym_radd_commute", "?n + ?m = ?m + ?n"),
4.251 +([1,5], Res), x + (2 + - 1) = 2
4.252 +. . . . . . . . . . Rewrite ("sym_radd_commute", "?n + ?m = ?m + ?n"),
4.253 +([1,6], Res), 2 + - 1 + x = 2
4.254 +. . . . . . . . . . Tactic.input_to_string not impl. for ?!,
4.255 +([1], Res), 2 + - 1 + x = 2
4.256 +. . . . . . . . . . Check_Postcond ["sqroot-test", "univariate", "equation", "test"]]
4.257 +*)
4.258 +
4.259 +Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)
4.260 +
4.261
4.262 \<close> ML \<open>
4.263 \<close> ML \<open>
4.264 \<close>
4.265 (*/------- outcomment in order to intermediately check with Test_Isac.thy ------------\(**)
4.266 - ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/790-complete.sml"
4.267 - ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/800-append-on-Frm.sml"
4.268 (**)\----- outcomment in order to intermediately check with Test_Isac.thy --------------/*)
4.269
4.270
5.1 --- a/src/Tools/isac/Interpret/derive.sml Wed Dec 21 18:48:23 2022 +0100
5.2 +++ b/src/Tools/isac/Interpret/derive.sml Thu Dec 22 10:27:12 2022 +0100
5.3 @@ -62,7 +62,7 @@
5.4
5.5
5.6 fun do_one ctxt asm_rls rs ro goal tt =
5.7 - let
5.8 + let
5.9 datatype switch = Appl | Noap (* TODO: unify with version in Rewrite *)
5.10 fun rew_once _ rts t Noap [] =
5.11 (case goal of NONE => rts | SOME _ =>
6.1 --- a/test/Tools/isac/Minisubpbl/790-complete-NEXT_STEP.sml Wed Dec 21 18:48:23 2022 +0100
6.2 +++ b/test/Tools/isac/Minisubpbl/790-complete-NEXT_STEP.sml Thu Dec 22 10:27:12 2022 +0100
6.3 @@ -48,7 +48,7 @@
6.4 (*/--------------------- final test ----------------------------------\\*)
6.5 val (res, asm) = (get_obj g_result pt (fst p));
6.6
6.7 -if UnparseC.term res = "[x = 1]" andalso
6.8 +if UnparseC.term_in_ctxt @{context} res = "[x = 1]" andalso
6.9 map UnparseC.term asm = [] (* assumptions have gone to the ctxt *)
6.10 then () else error "Minisubpbl/790-complete-NEXT_STEP.sml, find_next_step CHANGED";
6.11
7.1 --- a/test/Tools/isac/Test_Isac.thy Wed Dec 21 18:48:23 2022 +0100
7.2 +++ b/test/Tools/isac/Test_Isac.thy Thu Dec 22 10:27:12 2022 +0100
7.3 @@ -145,7 +145,7 @@
7.4 "~~~~~ continue fun xxx"; val () = ();
7.5 (*if*) (*then*); (*else*); (*case*) (*of*); (*return value*); (*in*) (*end*);
7.6 "xx"
7.7 -^ "xxx" (*+*) (*+++*) (*keep for continuing XXXXX*) (*isa*) (*isa2*) (**)
7.8 +^ "xxx" (*+*) (*+++*) (*keep for continuing YYYYY*) (*isa*) (*isa2*) (**)
7.9 \<close> ML \<open> (*//----------- adhoc inserted n ----------------------------------------------------\\*)
7.10 (*//----------------- adhoc inserted n ----------------------------------------------------\\*)
7.11 (*\\------------------ adhoc inserted n ----------------------------------------------------//*)
7.12 @@ -153,7 +153,7 @@
7.13
7.14 \<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*)
7.15 (*//------------------ step into XXXXX -----------------------------------------------------\\*)
7.16 -(*keep for continuing XXXXX*)
7.17 +(*keep for continuing YYYYY*)
7.18 \<close> ML \<open> (*------------- continuing XXXXX ------------------------------------------------------*)
7.19 (*-------------------- continuing XXXXX ------------------------------------------------------*)
7.20 (*kept for continuing XXXXX*)
8.1 --- a/test/Tools/isac/Test_Isac_Short.thy Wed Dec 21 18:48:23 2022 +0100
8.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Thu Dec 22 10:27:12 2022 +0100
8.3 @@ -145,7 +145,7 @@
8.4 "~~~~~ continue fun xxx"; val () = ();
8.5 (*if*) (*then*); (*else*); (*case*) (*of*); (*return value*); (*in*) (*end*);
8.6 "xx"
8.7 -^ "xxx" (*+*) (*+++*) (*keep for continuing XXXXX*) (*isa*) (*isa2*) (**)
8.8 +^ "xxx" (*+*) (*+++*) (*keep for continuing YYYYY*) (*isa*) (*isa2*) (**)
8.9 \<close> ML \<open> (*//----------- adhoc inserted n ----------------------------------------------------\\*)
8.10 (*//----------------- adhoc inserted n ----------------------------------------------------\\*)
8.11 (*\\------------------ adhoc inserted n ----------------------------------------------------//*)
8.12 @@ -153,7 +153,7 @@
8.13
8.14 \<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*)
8.15 (*//------------------ step into XXXXX -----------------------------------------------------\\*)
8.16 -(*keep for continuing XXXXX*)
8.17 +(*keep for continuing YYYYY*)
8.18 \<close> ML \<open> (*------------- continuing XXXXX ------------------------------------------------------*)
8.19 (*-------------------- continuing XXXXX ------------------------------------------------------*)
8.20 (*kept for continuing XXXXX*)
9.1 --- a/test/Tools/isac/Test_Some.thy Wed Dec 21 18:48:23 2022 +0100
9.2 +++ b/test/Tools/isac/Test_Some.thy Thu Dec 22 10:27:12 2022 +0100
9.3 @@ -60,7 +60,7 @@
9.4 "~~~~~ continue fun xxx"; val () = ();
9.5 (*if*) (*then*); (*else*); (*case*) (*of*); (*return value*); (*in*) (*end*);
9.6 "xx"
9.7 -^ "xxx" (*+*) (*+++*) (*keep for continuing XXXXX*) (*isa*) (*isa2*) (**)
9.8 +^ "xxx" (*+*) (*+++*) (*keep for continuing YYYYY*) (*isa*) (*isa2*) (**)
9.9 \<close> ML \<open> (*//----------- adhoc inserted n ----------------------------------------------------\\*)
9.10 (*//----------------- adhoc inserted n ----------------------------------------------------\\*)
9.11 (*\\------------------ adhoc inserted n ----------------------------------------------------//*)
9.12 @@ -68,7 +68,7 @@
9.13
9.14 \<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*)
9.15 (*//------------------ step into XXXXX -----------------------------------------------------\\*)
9.16 -(*keep for continuing XXXXX*)
9.17 +(*keep for continuing YYYYY*)
9.18 \<close> ML \<open> (*------------- continuing XXXXX ------------------------------------------------------*)
9.19 (*-------------------- continuing XXXXX ------------------------------------------------------*)
9.20 (*kept for continuing XXXXX*)
9.21 @@ -142,7 +142,7 @@
9.22 "~~~~~ continue fun xxx"; val () = ();
9.23 (*if*) (*then*); (*else*); (*case*) (*of*); (*return value*); (*in*) (*end*);
9.24 "xx"
9.25 -^ "xxx" (*+*) (*+++*) (*keep for continuing XXXXX*) (*isa*) (*isa2*) (**)
9.26 +^ "xxx" (*+*) (*+++*) (*keep for continuing YYYYY*) (*isa*) (*isa2*) (**)
9.27 \<close> ML \<open> (*//----------- adhoc inserted n ----------------------------------------------------\\*)
9.28 (*//----------------- adhoc inserted n ----------------------------------------------------\\*)
9.29 (*\\------------------ adhoc inserted n ----------------------------------------------------//*)
9.30 @@ -150,7 +150,7 @@
9.31
9.32 \<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*)
9.33 (*//------------------ step into XXXXX -----------------------------------------------------\\*)
9.34 -(*keep for continuing XXXXX*)
9.35 +(*keep for continuing YYYYY*)
9.36 \<close> ML \<open> (*------------- continuing XXXXX ------------------------------------------------------*)
9.37 (*-------------------- continuing XXXXX ------------------------------------------------------*)
9.38 (*kept for continuing XXXXX*)
10.1 --- a/test/Tools/isac/Test_Theory.thy Wed Dec 21 18:48:23 2022 +0100
10.2 +++ b/test/Tools/isac/Test_Theory.thy Thu Dec 22 10:27:12 2022 +0100
10.3 @@ -13,7 +13,7 @@
10.4 "~~~~~ continue fun xxx"; val () = ();
10.5 (*if*) (*then*); (*else*); (*case*) (*of*); (*return value*); (*in*) (*end*);
10.6 "xx"
10.7 -^ "xxx" (*+*) (*+++*) (*keep for continuing XXXXX*) (*isa*) (*isa2*) (**)
10.8 +^ "xxx" (*+*) (*+++*) (*keep for continuing YYYYY*) (*isa*) (*isa2*) (**)
10.9 \<close> ML \<open> (*//----------- adhoc inserted n ----------------------------------------------------\\*)
10.10 (*//------------------ adhoc inserted n ----------------------------------------------------\\*)
10.11 (*\\------------------ adhoc inserted n ----------------------------------------------------//*)
10.12 @@ -21,10 +21,10 @@
10.13
10.14 \<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*)
10.15 (*//------------------ step into XXXXX -----------------------------------------------------\\*)
10.16 -(*keep for continuing XXXXX*)
10.17 +(*keep for continuing YYYYY*)
10.18 \<close> ML \<open> (*------------- continuing XXXXX ------------------------------------------------------*)
10.19 (*-------------------- continuing XXXXX ------------------------------------------------------*)
10.20 -(*kept for continuing XXXXX*)
10.21 +(*kept for continuing YYYYY*)
10.22 (*-------------------- stop step into XXXXX --------------------------------------------------*)
10.23 \<close> ML \<open> (*------------- stop step into XXXXX --------------------------------------------------*)
10.24 (*\\------------------ step into XXXXX -----------------------------------------------------//*)
10.25 @@ -116,7 +116,7 @@
10.26 "~~~~~ continue fun xxx"; val () = ();
10.27 (*if*) (*then*); (*else*); (*case*) (*of*); (*return value*); (*in*) (*end*);
10.28 "xx"
10.29 -^ "xxx" (*+*) (*+++*) (*keep for continuing XXXXX*) (*isa*) (*isa2*) (**)
10.30 +^ "xxx" (*+*) (*+++*) (*keep for continuing YYYYY*) (*isa*) (*isa2*) (**)
10.31 \<close> ML \<open> (*//----------- adhoc inserted n ----------------------------------------------------\\*)
10.32 (*//----------------- adhoc inserted n ----------------------------------------------------\\*)
10.33 (*\\------------------ adhoc inserted n ----------------------------------------------------//*)
10.34 @@ -124,7 +124,7 @@
10.35
10.36 \<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*)
10.37 (*//------------------ step into XXXXX -----------------------------------------------------\\*)
10.38 -(*keep for continuing XXXXX*)
10.39 +(*keep for continuing YYYYY*)
10.40 \<close> ML \<open> (*------------- continuing XXXXX ------------------------------------------------------*)
10.41 (*-------------------- continuing XXXXX ------------------------------------------------------*)
10.42 (*kept for continuing XXXXX*)