1.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Tue Jan 31 11:23:16 2023 +0100
1.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Tue Jan 31 12:29:42 2023 +0100
1.3 @@ -49,9 +49,9 @@
1.4 "--------- appendFormula: on Res + equ_nrls ----------------------";
1.5 "--------- appendFormula: on Res + equ_nrls ----------------------";
1.6 val Prog sc = (#program o MethodC.from_store ctxt) ["Test", "squ-equ-test-subpbl1"];
1.7 - (writeln o UnparseC.term) sc;
1.8 + (writeln o UnparseC.term_in_ctxt @{context}) sc;
1.9 val Prog sc = (#program o MethodC.from_store ctxt) ["Test", "solve_linear"];
1.10 - (writeln o UnparseC.term) sc;
1.11 + (writeln o UnparseC.term_in_ctxt @{context}) sc;
1.12
1.13 States.reset ();
1.14 CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.15 @@ -89,7 +89,7 @@
1.16 moveDown 1 ([2,4],Res); refFormula 1 ([2,5],Res);
1.17 moveDown 1 ([2,5],Res); refFormula 1 ([2,6],Res);
1.18 val ((pt,_),_) = States.get_calc 1;
1.19 - if "- 2 * 1 + (1 + x) = 0" = UnparseC.term (fst (get_obj g_result pt [2,6])) then()
1.20 + if "- 2 * 1 + (1 + x) = 0" = UnparseC.term_in_ctxt @{context} (fst (get_obj g_result pt [2,6])) then()
1.21 else error "inform.sml: diff.behav.appendFormula: on Res + equ 2";
1.22
1.23 fetchProposedTactic 1; (*takes Iterator 1 _1_*)
1.24 @@ -102,7 +102,7 @@
1.25
1.26 autoCalculate 1 CompleteCalc;
1.27 val ((pt,_),_) = States.get_calc 1;
1.28 - if "[x = 1]" = UnparseC.term (fst (get_obj g_result pt [])) then ()
1.29 + if "[x = 1]" = UnparseC.term_in_ctxt @{context} (fst (get_obj g_result pt [])) then ()
1.30 else error "inform.sml: diff.behav.appendFormula: on Res + equ 4";
1.31 (* autoCalculate 1 CompleteCalc;
1.32 val ((pt,p),_) = States.get_calc 1;
1.33 @@ -157,7 +157,7 @@
1.34 moveDown 1 ([1,4],Res); refFormula 1 ([1,5],Res);
1.35 moveDown 1 ([1,5],Res); refFormula 1 ([1,6],Res);
1.36 val ((pt,_),_) = States.get_calc 1;
1.37 - if "2 + - 1 + x = 2" = UnparseC.term (fst (get_obj g_result pt [1,6])) then()
1.38 + if "2 + - 1 + x = 2" = UnparseC.term_in_ctxt @{context} (fst (get_obj g_result pt [1,6])) then()
1.39 else error "inform.sml: diff.behav.appendFormula: on Frm + equ 1";
1.40
1.41 fetchProposedTactic 1; (*takes Iterator 1 _1_*)
1.42 @@ -166,7 +166,7 @@
1.43 | _ => error "inform.sml: diff.behav.appendFormula: on Frm + equ 2";
1.44 autoCalculate 1 CompleteCalc;
1.45 val ((pt,_),_) = States.get_calc 1;
1.46 - if "[x = 1]" = UnparseC.term (fst (get_obj g_result pt [])) then ()
1.47 + if "[x = 1]" = UnparseC.term_in_ctxt @{context} (fst (get_obj g_result pt [])) then ()
1.48 else error "inform.sml: diff.behav.appendFormula: on Frm + equ 3";
1.49 DEconstrCalcTree 1;
1.50
1.51 @@ -196,7 +196,7 @@
1.52 | _ => error "inform.sml: diff.behav.appendFormula: Res + NOder 2";
1.53 autoCalculate 1 CompleteCalc;
1.54 val ((pt,_),_) = States.get_calc 1;
1.55 - if "[x = 1]" = UnparseC.term (fst (get_obj g_result pt [])) then ()
1.56 + if "[x = 1]" = UnparseC.term_in_ctxt @{context} (fst (get_obj g_result pt [])) then ()
1.57 else error "inform.sml: diff.behav.appendFormula: on Frm + equ 3";
1.58 DEconstrCalcTree 1;
1.59
1.60 @@ -229,7 +229,7 @@
1.61 | _ => error "inform.sml: diff.behav.appendFormula: Res + late d 2";
1.62 autoCalculate 1 CompleteCalc;
1.63 val ((pt,_),_) = States.get_calc 1;
1.64 - if "[x = 1]" = UnparseC.term (fst (get_obj g_result pt [])) then ()
1.65 + if "[x = 1]" = UnparseC.term_in_ctxt @{context} (fst (get_obj g_result pt [])) then ()
1.66 else error "inform.sml: diff.behav.appendFormula: Res + late d 3";
1.67 DEconstrCalcTree 1;
1.68
1.69 @@ -252,7 +252,7 @@
1.70 else error "inform.sml: diff.behav.appendFormula: Res + latEE 1";
1.71 autoCalculate 1 CompleteCalc;
1.72 val ((pt,p),_) = States.get_calc 1;
1.73 - if "[x = 3 + - 2 * 1]" = UnparseC.term (fst (get_obj g_result pt [])) then ()
1.74 + if "[x = 3 + - 2 * 1]" = UnparseC.term_in_ctxt @{context} (fst (get_obj g_result pt [])) then ()
1.75 (* ~~~~~~~~~~ simplify as last step in any script ?!*)
1.76 else error "inform.sml: diff.behav.appendFormula: Res + latEE 2";
1.77 DEconstrCalcTree 1;
1.78 @@ -299,7 +299,7 @@
1.79
1.80 autoCalculate 1 CompleteCalc;
1.81 val ((pt,pos as (p,_)),_) = States.get_calc 1;
1.82 - if pos = ([],Res) andalso "[x = 1]" = (UnparseC.term o fst) (get_obj g_result pt p) then()
1.83 + if pos = ([],Res) andalso "[x = 1]" = (UnparseC.term_in_ctxt @{context} o fst) (get_obj g_result pt p) then()
1.84 else error "inform.sml: diff.behav.replaceFormula: on Res + = 2";
1.85 DEconstrCalcTree 1;
1.86
1.87 @@ -323,7 +323,7 @@
1.88 else error "inform.sml: diff.behav.replaceFormula: on Res 1 + = 1";
1.89 autoCalculate 1 CompleteCalc;
1.90 val ((pt,pos as (p,_)),_) = States.get_calc 1;
1.91 - if pos = ([],Res) andalso "[x = 1]" = (UnparseC.term o fst)(get_obj g_result pt p) then()
1.92 + if pos = ([],Res) andalso "[x = 1]" = (UnparseC.term_in_ctxt @{context} o fst)(get_obj g_result pt p) then()
1.93 else error "inform.sml: diff.behav.replaceFormula: on Res + = 2";
1.94 DEconstrCalcTree 1;
1.95
1.96 @@ -346,7 +346,7 @@
1.97 else error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 1";
1.98 autoCalculate 1 CompleteCalc;
1.99 val ((pt,pos as (p,_)),_) = States.get_calc 1;
1.100 - if pos = ([],Res) andalso "[x = 1]" = (UnparseC.term o fst)(get_obj g_result pt p) then()
1.101 + if pos = ([],Res) andalso "[x = 1]" = (UnparseC.term_in_ctxt @{context} o fst)(get_obj g_result pt p) then()
1.102 else error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 2";
1.103 DEconstrCalcTree 1;
1.104
1.105 @@ -615,7 +615,7 @@
1.106 autoCalculate 1 CompleteCalc;
1.107 val ((pt, p), _) = States.get_calc 1;
1.108 val (t, asm) = get_obj g_result pt [];
1.109 -if UnparseC.term t = "(a * d * f + b * c * f + b * d * e) / (b * d * f)" andalso
1.110 +if UnparseC.term_in_ctxt @{context} t = "(a * d * f + b * c * f + b * d * e) / (b * d * f)" andalso
1.111 UnparseC.terms asm =(*"[\"b * d * f \<noteq> 0\",\"d \<noteq> 0\",\"b \<noteq> 0\",\"a * x / (b * x) + c * x / (d * x) + e / f is_ratpolyexp\"]"*)
1.112 "[]" (*..found broken in child of 33913fe24685, error covered by CAS-command *)
1.113 then () else error "inform [rational,simplification] changed at end";
1.114 @@ -701,7 +701,7 @@
1.115 val Form res = (#1 o ME_Misc.pt_extract) (pt, ([],Res));
1.116 Test_Tool.show_pt pt;
1.117
1.118 -if p = ([], Res) andalso UnparseC.term res = "1 + 2 * x" then ()
1.119 +if p = ([], Res) andalso UnparseC.term_in_ctxt @{context} res = "1 + 2 * x" then ()
1.120 else error "diff.sml behav.changed for Diff (x \<up> 2 + x + 1, x)";
1.121 DEconstrCalcTree 1;
1.122 -----------------------------------------------------------------------------------------------*)
1.123 @@ -743,7 +743,7 @@
1.124 autoCalculate 1 (Steps 1);
1.125 val ((pt,p),_) = States.get_calc 1;
1.126 val Form res = (#1 o (ME_Misc.pt_extract ctxt)) (pt, p);
1.127 -if UnparseC.term res = "d_d x (x \<up> 2 + x + 1)" then ()
1.128 +if UnparseC.term_in_ctxt @{context} res = "d_d x (x \<up> 2 + x + 1)" then ()
1.129 else error "diff.sml Diff (x \<up> 2 + x + 1, x) from exp";
1.130 DEconstrCalcTree 1;
1.131
1.132 @@ -958,7 +958,7 @@
1.133 val subst = [(ParseC.parse_test @{context} "bdv", ParseC.parse_test @{context} "x")]: subst;
1.134 val t = ParseC.parse_test @{context} "d_d x (x \<up> 2 + sin (x \<up> 4))";
1.135 val SOME (t, _) = rewrite_set_inst_ ctxt false subst norm_diff t;
1.136 -if UnparseC.term t = "2 * x + cos (x \<up> 4) * 4 * x \<up> 3" then ()
1.137 +if UnparseC.term_in_ctxt @{context} t = "2 * x + cos (x \<up> 4) * 4 * x \<up> 3" then ()
1.138 else error "build fun check_for' ?bdv changed 1";
1.139
1.140 val rls = norm_diff
1.141 @@ -967,19 +967,19 @@
1.142
1.143 val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern TermC.matches in res*)
1.144 rew_sub ctxt 1 subst Rewrite_Ord.function_empty Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
1.145 -if UnparseC.term res' = "2 * x + cos (d_d x (x \<up> 4))" andalso rewritten then ()
1.146 +if UnparseC.term_in_ctxt @{context} res' = "2 * x + cos (d_d x (x \<up> 4))" andalso rewritten then ()
1.147 else error "build fun check_for' ?bdv changed 2";
1.148
1.149 val norm_res = case rewrite_set_inst_ ctxt false subst rls res' of
1.150 NONE => res'
1.151 | SOME (norm_res, _) => norm_res;
1.152 -if UnparseC.term norm_res = "2 * x + cos (4 * x \<up> 3)" then ()
1.153 +if UnparseC.term_in_ctxt @{context} norm_res = "2 * x + cos (4 * x \<up> 3)" then ()
1.154 else error "build fun check_for' ?bdv changed 3";
1.155
1.156 val norm_inf = case rewrite_set_inst_ ctxt false subst rls inf of
1.157 NONE => inf
1.158 | SOME (norm_inf, _) => norm_inf;
1.159 -if UnparseC.term norm_inf = "2 * x + cos (4 * x \<up> 3)" then ()
1.160 +if UnparseC.term_in_ctxt @{context} norm_inf = "2 * x + cos (4 * x \<up> 3)" then ()
1.161 else error "build fun check_for' ?bdv changed 4";
1.162
1.163 res' = inf;
1.164 @@ -1058,8 +1058,8 @@
1.165
1.166 val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
1.167 ;
1.168 -(*+*)if UnparseC.term f_pred = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" andalso
1.169 -(*+*) UnparseC.term f_in = "d_d x (x \<up> 2) + cos (4 * x \<up> 3)"
1.170 +(*+*)if UnparseC.term_in_ctxt @{context} f_pred = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" andalso
1.171 +(*+*) UnparseC.term_in_ctxt @{context} f_in = "d_d x (x \<up> 2) + cos (4 * x \<up> 3)"
1.172 (*+*)then () else error "inform with (positive) Error_Pattern.check_for broken 2";
1.173
1.174 val SOME "chain-rule-diff-both" = (*case*) Error_Pattern.check_for ctxt (f_pred, f_in) (prog, env) (errpats, rew_rls) (*of*);
1.175 @@ -1160,7 +1160,7 @@
1.176 (* final test ... ----------------------------------------------------------------------------*)
1.177 (*+*)if length return_fill_from_store = 5 then
1.178 (*+*) case return_fill_from_store of
1.179 -(*+*) ("fill-d_d-arg", tm, thm, subsopt) :: _ => if UnparseC.term tm =
1.180 +(*+*) ("fill-d_d-arg", tm, thm, subsopt) :: _ => if UnparseC.term_in_ctxt @{context} tm =
1.181 (*+*) "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4)) =\nd_d x (x \<up> 2) + cos (x \<up> 4) * d_d x ?_dummy_1"
1.182 (*+*) then () else error "find_fill_patterns changed 2a"
1.183 (*+*) | _ => error "find_fill_patterns changed 2b"
1.184 @@ -1235,10 +1235,10 @@
1.185 val p = States.get_pos 1 1;
1.186 val (Form f, _, asms) = ME_Misc.pt_extract ctxt (pt, p);
1.187
1.188 - if p = ([1], Res) andalso UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" then
1.189 + if p = ([1], Res) andalso UnparseC.term_in_ctxt @{context} f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" then
1.190 case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"],
1.191 ("diff_sum", thm)) =>
1.192 - if (UnparseC.term o Thm.prop_of) thm = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" then ()
1.193 + if (UnparseC.term_in_ctxt @{context} o Thm.prop_of) thm = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" then ()
1.194 else error "embed fun fill_form changed 11"
1.195 | _ => error "embed fun fill_form changed 12"
1.196 else error "embed fun fill_form changed 13";
1.197 @@ -1250,10 +1250,10 @@
1.198 val p = States.get_pos 1 1;
1.199
1.200 val (Form f, _, asms) = ME_Misc.pt_extract ctxt (pt, p);
1.201 - if p = ([1], Res) andalso UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" then
1.202 + if p = ([1], Res) andalso UnparseC.term_in_ctxt @{context} f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" then
1.203 case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"],
1.204 ("diff_sum", thm)) =>
1.205 - if (UnparseC.term o Thm.prop_of) thm = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" then ()
1.206 + if (UnparseC.term_in_ctxt @{context} o Thm.prop_of) thm = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" then ()
1.207 else error "embed fun fill_form changed 21"
1.208 | _ => error "embed fun fill_form changed 22"
1.209 else error "embed fun fill_form changed 23";
1.210 @@ -1264,10 +1264,10 @@
1.211 val p = States.get_pos 1 1;
1.212 val (Form f, _, asms) = ME_Misc.pt_extract ctxt (pt, p);
1.213 if p = ([1], Res) andalso existpt [2] pt
1.214 - andalso UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))"
1.215 + andalso UnparseC.term_in_ctxt @{context} f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))"
1.216 then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"],
1.217 ("diff_sum", thm)) =>
1.218 - if (UnparseC.term o Thm.prop_of) thm = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" then ()
1.219 + if (UnparseC.term_in_ctxt @{context} o Thm.prop_of) thm = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" then ()
1.220 else error "embed fun fill_form changed 31"
1.221 | _ => error "embed fun fill_form changed 32"
1.222 else error "embed fun fill_form changed 33";
1.223 @@ -1287,7 +1287,7 @@
1.224 val p' = lev_on p;
1.225 val tac = get_obj g_tac pt p';
1.226 val Rewrite_Inst ([bbb as "(''bdv'', x)"], ("diff_sin_chain", ttt)) = tac;
1.227 -if (UnparseC.term o Thm.prop_of) ttt = "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u" then ()
1.228 +if (UnparseC.term_in_ctxt @{context} o Thm.prop_of) ttt = "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u" then ()
1.229 else error "inputFillFormula changed 10";
1.230 val Applicable.Yes rew = Step.check tac (pt, pos);
1.231 val Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) = rew;
1.232 @@ -1302,10 +1302,10 @@
1.233 val ((pt, _),_) = States.get_calc 1;
1.234 val p = States.get_pos 1 1;
1.235 val (Form f, _, asms) = ME_Misc.pt_extract ctxt (pt, p);
1.236 - if p = ([2], Res) andalso UnparseC.term f = "d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x (x \<up> 4)"
1.237 + if p = ([2], Res) andalso UnparseC.term_in_ctxt @{context} f = "d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x (x \<up> 4)"
1.238 then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"],
1.239 ("diff_sin_chain", thm)) =>
1.240 - if (UnparseC.term o Thm.prop_of) thm = "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u" then ()
1.241 + if (UnparseC.term_in_ctxt @{context} o Thm.prop_of) thm = "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u" then ()
1.242 else error "inputFillFormula changed 111"
1.243 | _ => error "inputFillFormula changed 112"
1.244 else error "inputFillFormula changed 113";