1.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Sun Oct 23 16:08:27 2022 +0200
1.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Sun Oct 23 17:21:04 2022 +0200
1.3 @@ -256,7 +256,7 @@
1.4 val ((pt,_),_) = States.get_calc 1;
1.5 val ip = States.get_pos 1 1;
1.6
1.7 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, ip);
1.8 + val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, ip);
1.9 (*exception just above means: 'ModSpec' has been returned: error anyway*)
1.10 if ip = ([], Res) andalso UnparseC.term f = "[x = 1]" then () else
1.11 error "FE-Kernel-interface.sml: diff.behav. in solve_linear as rootpbl";
1.12 @@ -458,7 +458,7 @@
1.13 (*this checks the test for correctness..*)
1.14 val ((pt,_),_) = States.get_calc 1;
1.15 val p = States.get_pos 1 1;
1.16 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.17 + val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
1.18 if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
1.19 error "FE-interface.sml: diff.behav. in miniscript with mini-subpb";
1.20 DEconstrCalcTree 1;
1.21 @@ -483,7 +483,7 @@
1.22
1.23 val ((pt,_),_) = States.get_calc 1;
1.24 val p = States.get_pos 1 1;
1.25 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.26 + val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
1.27 if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
1.28 error "FE-interface.sml: diff.behav. in solve_linear/rt AUTOCALCULATE ";
1.29 DEconstrCalcTree 1;
1.30 @@ -534,7 +534,7 @@
1.31
1.32 val ((pt,_),_) = States.get_calc 1;
1.33 val p = States.get_pos 1 1;
1.34 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.35 + val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
1.36 if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
1.37 error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
1.38 DEconstrCalcTree 1;
1.39 @@ -596,7 +596,7 @@
1.40 refFormula 1 (States.get_pos 1 1);
1.41 val ((pt,_),_) = States.get_calc 1;
1.42 val p = States.get_pos 1 1;
1.43 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.44 + val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
1.45 if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
1.46 error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
1.47 DEconstrCalcTree 1;
1.48 @@ -624,13 +624,13 @@
1.49 autoCalculate 1 (Steps 1);
1.50 (*setContext 1 p "thy_isac_Test-rls-Test_simplify";*)
1.51 val (((pt,_),_), p) = (States.get_calc 1, States.get_pos 1 1);
1.52 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.53 + val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
1.54 if p = ([1], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "x + 1 + - 1 * 2 = 0"
1.55 then () else error "--- setContext..Thy --- autoCalculate 1 (Steps 1) #1";
1.56
1.57 autoCalculate 1 CompleteCalc;
1.58 val (((pt,_),_), p) = (States.get_calc 1, States.get_pos 1 1);
1.59 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.60 + val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
1.61
1.62 if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then ()
1.63 else error "--- setContext..Thy --- autoCalculate CompleteCalc";
1.64 @@ -662,7 +662,7 @@
1.65 val ((pt,_),_) = States.get_calc 1;
1.66 val p = States.get_pos 1 1;
1.67
1.68 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.69 + val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
1.70 if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
1.71 error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl 1";
1.72 DEconstrCalcTree 1;
1.73 @@ -750,7 +750,7 @@
1.74 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.75 setNextTactic 1 (Check_Postcond ["rational", "univariate", "equation"]);
1.76 val (ptp,_) = States.get_calc 1;
1.77 - val (Form t,_,_) = ME_Misc.pt_extract ptp;
1.78 + val (Form t,_,_) = ME_Misc.pt_extract ctxt ptp;
1.79 if States.get_pos 1 1 = ([], Res) andalso UnparseC.term t = "[x = -4 / 3]" then ()
1.80 else writeln "FE-inteface.sml: diff.behav. in rat-eq + subpbl: no_met, NO ..";
1.81 DEconstrCalcTree 1;
1.82 @@ -850,7 +850,7 @@
1.83 val ((pt,_),_) = States.get_calc 1;
1.84 Test_Tool.show_pt pt;
1.85 val p = States.get_pos 1 1;
1.86 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.87 + val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
1.88 if UnparseC.term f = "[x = - 1, x = -3]" andalso p = ([], Res) then () else
1.89 error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
1.90
1.91 @@ -873,7 +873,7 @@
1.92 rootthy pt;
1.93 Test_Tool.show_pt pt;
1.94 val p = States.get_pos 1 1;
1.95 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.96 + val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
1.97 if UnparseC.term f = "[x = - 1, x = -3]" andalso p = ([], Res) then () else
1.98 error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
1.99 DEconstrCalcTree 1;
1.100 @@ -1047,7 +1047,7 @@
1.101 refFormula 1 (States.get_pos 1 1);
1.102 val ((pt,_),_) = States.get_calc 1;
1.103 val p = States.get_pos 1 1;
1.104 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.105 + val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
1.106 if UnparseC.term f = "[x = 1]" andalso p = ([], Res) andalso map UnparseC.term asms = [] then ()
1.107 else error "FE-interface.sml: diff.behav. in from pbl -hierarchy 1";
1.108 DEconstrCalcTree 1;
1.109 @@ -1065,7 +1065,7 @@
1.110 refFormula 1 (States.get_pos 1 1);
1.111 val ((pt,_),_) = States.get_calc 1;
1.112 val p = States.get_pos 1 1;
1.113 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.114 + val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
1.115 if UnparseC.term f = "[x = 1]" andalso p = ([], Res) andalso map UnparseC.term asms = [] then ()
1.116 else error "FE-interface.sml: diff.behav. in from pbl -hierarchy 2";
1.117 DEconstrCalcTree 1;
1.118 @@ -1151,7 +1151,7 @@
1.119 autoCalculate 1 CompleteCalc;
1.120 val ((pt,_),_) = States.get_calc 1;
1.121 val p = States.get_pos 1 1;
1.122 -val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.123 +val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
1.124 (*============ inhibit exn WN120316 compare 2002-- 2011 ===========================
1.125 if map UnparseC.term asms =
1.126 ["True |\n~ lhs ((3 + - 1 * x + x \<up> 2) * x =\n" ^
1.127 @@ -1221,7 +1221,7 @@
1.128 autoCalculate 1 CompleteCalc;
1.129 val ((pt,_),_) = States.get_calc 1;
1.130 val p = States.get_pos 1 1;
1.131 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.132 + val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
1.133 if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
1.134 error "FE-interface.sml: diff.behav. in combinations of steps";
1.135 DEconstrCalcTree 1;
1.136 @@ -1245,7 +1245,7 @@
1.137
1.138 val ((pt,_),_) = States.get_calc 1;
1.139 val p = States.get_pos 1 1;
1.140 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.141 + val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
1.142 if UnparseC.term f = "- 1 + x = 0" andalso p = ([2], Res) then () else
1.143 error "FE-interface.sml: diff.behav. in FORMULA:enter} right";
1.144 DEconstrCalcTree 1;
1.145 @@ -1268,7 +1268,7 @@
1.146
1.147 val ((pt,_),_) = States.get_calc 1;
1.148 val p = States.get_pos 1 1;
1.149 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.150 + val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
1.151 if UnparseC.term f = "x - 1 = 0" andalso p = ([2], Res) then () else
1.152 error "FE-interface.sml: diff.behav. in FORMULA:enter} other";
1.153 DEconstrCalcTree 1;
1.154 @@ -1292,7 +1292,7 @@
1.155
1.156 val ((pt,_),_) = States.get_calc 1;
1.157 val p = States.get_pos 1 1;
1.158 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.159 + val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
1.160 if UnparseC.term f = "x = 1" andalso p = ([3,2], Res) then () else
1.161 error "FE-interface.sml: diff.behav. in FORMULA:enter} oth 2";
1.162 DEconstrCalcTree 1;
1.163 @@ -1313,7 +1313,7 @@
1.164
1.165 val ((pt,_),_) = States.get_calc 1;
1.166 val p = States.get_pos 1 1;
1.167 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.168 + val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
1.169 if UnparseC.term f = "x + 1 + - 1 * 2 = 0" andalso p = ([1], Res) then () else
1.170 error "FE-interface.sml: diff.behav. in FORMULA:enter} NOTok";
1.171 DEconstrCalcTree 1;
1.172 @@ -1334,10 +1334,10 @@
1.173
1.174 val ((pt,_),_) = States.get_calc 1;
1.175 val p = States.get_pos 1 1;
1.176 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.177 + val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
1.178 if UnparseC.term f = "- 1 + x = 0" andalso p = ([2], Res) then () else
1.179 error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
1.180 - if map fst3 (ME_Misc.get_interval ([2],Res) ([],Res) 9999 pt) =
1.181 + if map fst3 (ME_Misc.get_interval ctxt ([2],Res) ([],Res) 9999 pt) =
1.182 [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
1.183 ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else
1.184 error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2";
1.185 @@ -1355,10 +1355,10 @@
1.186
1.187 val ((pt,_),_) = States.get_calc 2;
1.188 val p = States.get_pos 2 1;
1.189 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.190 + val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
1.191 if UnparseC.term f = "- 1 + x = 0" andalso p = ([2], Res) then () else
1.192 error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
1.193 - if map fst3 (ME_Misc.get_interval ([2],Res) ([],Res) 9999 pt) =
1.194 + if map fst3 (ME_Misc.get_interval ctxt ([2],Res) ([],Res) 9999 pt) =
1.195 [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
1.196 ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else
1.197 error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2b";
1.198 @@ -1383,13 +1383,13 @@
1.199 val ((pt,_),_) = States.get_calc 1;
1.200 Test_Tool.show_pt pt;
1.201 val p = States.get_pos 1 1;
1.202 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.203 + val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
1.204 if UnparseC.term f = "x - 1 = 0" andalso p = ([2], Res) then () else
1.205 error "FE-interface.sml: diff.behav. in FORMULA:replace} other 1";
1.206 (* for getting the list in whole length ...
1.207 -(*default_print_depth 99*) map fst3 (ME_Misc.get_interval ([1],Res) ([],Res) 9999 pt); (*default_print_depth 3*)
1.208 +(*default_print_depth 99*) map fst3 (ME_Misc.get_interval ctxt ([1],Res) ([],Res) 9999 pt); (*default_print_depth 3*)
1.209 *)
1.210 - if map fst3 (ME_Misc.get_interval ([1],Res) ([],Res) 9999 pt) =
1.211 + if map fst3 (ME_Misc.get_interval ctxt ([1],Res) ([],Res) 9999 pt) =
1.212 [([1], Res), ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
1.213 ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2, 7], Res),
1.214 ([2, 8], Res), ([2, 9], Res), ([2], Res)] then () else
1.215 @@ -1416,14 +1416,14 @@
1.216 val ((pt,_),_) = States.get_calc 1;
1.217 Test_Tool.show_pt pt; (*error: ...ME_Misc.get_interval drops ([3,2],Res) ...*)
1.218 val (t,_) = get_obj g_result pt [3,2]; UnparseC.term t;
1.219 - if map fst3 (ME_Misc.get_interval ([1],Res) ([],Res) 9999 pt) =
1.220 + if map fst3 (ME_Misc.get_interval ctxt ([1],Res) ([],Res) 9999 pt) =
1.221 [([1], Res), ([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res),
1.222 ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
1.223 ([3,2],Res)] then () else
1.224 error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 1";
1.225
1.226 val p = States.get_pos 1 1;
1.227 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.228 + val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
1.229 if UnparseC.term f = "x = 1" andalso p = ([3,2], Res) then () else
1.230 error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 2";
1.231 DEconstrCalcTree 1;
1.232 @@ -1445,7 +1445,7 @@
1.233 val ((pt,_),_) = States.get_calc 1;
1.234 Test_Tool.show_pt pt;
1.235 val p = States.get_pos 1 1;
1.236 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.237 + val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
1.238 if UnparseC.term f = "- 1 + x = 0" andalso p = ([2], Res) then () else
1.239 error "FE-interface.sml: diff.behav. in FORMULA:replace} NOTok";
1.240 DEconstrCalcTree 1;
1.241 @@ -1468,7 +1468,7 @@
1.242 instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)
1.243 val ((pt,pos), _) = States.get_calc 1;
1.244 val p = States.get_pos 1 1;
1.245 - val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
1.246 + val (Form f, _, asms) = ME_Misc.pt_extract ctxt (pt, p);
1.247
1.248 if p = ([1], Res) andalso UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))"
1.249 then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"],
1.250 @@ -1483,7 +1483,7 @@
1.251 val ((pt,pos),_) = States.get_calc 1;
1.252 val p = States.get_pos 1 1;
1.253
1.254 - val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
1.255 + val (Form f, _, asms) = ME_Misc.pt_extract ctxt (pt, p);
1.256 if p = ([1], Res) andalso UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" andalso
1.257 get_obj g_tac pt (fst p) = Rewrite_Inst (["(''bdv'', x)"], ("diff_sum", "Diff.diff_sum"(*?!?*)))
1.258 then ()
1.259 @@ -1496,7 +1496,7 @@
1.260 (*<AUTOCALC> ([1], Res) ([2], Res) ([2], Res) </AUTOCALC>*)
1.261 val ((pt,pos),_) = States.get_calc 1;
1.262 val p = States.get_pos 1 1;
1.263 - val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
1.264 + val (Form f, _, asms) = ME_Misc.pt_extract ctxt (pt, p);
1.265 if p = ([1], Res) andalso existpt [2] pt andalso
1.266 UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up>\<up> 4))" andalso
1.267 get_obj g_tac pt (fst p) = Rewrite_Inst (["(''bdv'', x)"], ("diff_sum", "Diff.diff_sum"))
1.268 @@ -1505,7 +1505,7 @@
1.269 inputFillFormula 1 "d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x (x \<up> 4)";(*<<<<<<<=====*)
1.270 val ((pt, _),_) = States.get_calc 1;
1.271 val p = States.get_pos 1 1;
1.272 - val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
1.273 + val (Form f, _, asms) = ME_Misc.pt_extract ctxt (pt, p);
1.274 if p = ([2], Res) andalso
1.275 UnparseC.term f = "d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x (x \<up> 4)" andalso
1.276 get_obj g_tac pt (fst p) = Rewrite_Inst (["(''bdv'', x)"], ("diff_sin_chain", ""))
1.277 @@ -1516,7 +1516,7 @@
1.278 "~~~~~ final check: the input formula is inserted as it would have been correct from beginning";
1.279 val ((pt, _),_) = States.get_calc 1;
1.280 val p = States.get_pos 1 1;
1.281 -val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
1.282 +val (Form f, _, asms) = ME_Misc.pt_extract ctxt (pt, p);
1.283 if p = ([], Res) andalso UnparseC.term f = "2 * x + cos (x \<up> 4) * 4 * x \<up> 3"
1.284 then () else error "inputFillFormula changed 12";
1.285 Test_Tool.show_pt pt;