follow up 6a: eliminate Thy_Info.get_theory for Minisubplb/100-init-rootpbl.sml
1.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml Sun Oct 23 16:08:27 2022 +0200
1.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml Sun Oct 23 17:21:04 2022 +0200
1.3 @@ -181,8 +181,9 @@
1.4 fun getTactic cI (p:pos') =
1.5 case \<^try>\<open>
1.6 let
1.7 - val ((pt, _), _) = States.get_calc cI
1.8 - val (_, tac, _) = ME_Misc.pt_extract (pt, p)
1.9 + val ((pt, p), _) = States.get_calc cI
1.10 + val ctxt = Ctree.get_ctxt_LI pt p
1.11 + val (_, tac, _) = ME_Misc.pt_extract ctxt (pt, p)
1.12 in
1.13 case tac of
1.14 SOME ta => gettacticOK2xml cI ta
1.15 @@ -212,8 +213,9 @@
1.16 fun getAssumptions cI (p:pos') =
1.17 case \<^try>\<open>
1.18 let
1.19 - val ((pt, _), _) = States.get_calc cI
1.20 - val (_, _, asms) = ME_Misc.pt_extract (pt, p)
1.21 + val ((pt, p), _) = States.get_calc cI
1.22 + val ctxt = Ctree.get_ctxt_LI pt p
1.23 + val (_, _, asms) = ME_Misc.pt_extract ctxt (pt, p)
1.24 in getasmsOK2xml cI asms end
1.25 \<close> of
1.26 SOME xml => xml
1.27 @@ -233,8 +235,9 @@
1.28 fun refFormula cI (p: pos') = (*WN0501 rename to "fun getElement" !*)
1.29 case \<^try>\<open>
1.30 let
1.31 - val ((pt, _), _) = States.get_calc cI
1.32 - val (form, _, _) = ME_Misc.pt_extract (pt, p)
1.33 + val ((pt, p), _) = States.get_calc cI
1.34 + val ctxt = Ctree.get_ctxt_LI pt p
1.35 + val (form, _, _) = ME_Misc.pt_extract ctxt (pt, p)
1.36 in refformulaOK2xml cI p form end
1.37 \<close> of
1.38 SOME xml => xml
1.39 @@ -247,9 +250,10 @@
1.40 fun getFormulaeFromTo cI (([], Pbl) : pos') (to as ([], Pbl) : pos') _ false =
1.41 (case \<^try>\<open>
1.42 let
1.43 - val ((pt,_),_) = States.get_calc cI
1.44 + val ((pt, p), _) = States.get_calc cI
1.45 + val ctxt = Ctree.get_ctxt_LI pt p
1.46 val headline =
1.47 - case ME_Misc.pt_extract (pt, to) of
1.48 + case ME_Misc.pt_extract ctxt (pt, to) of
1.49 (ModSpec (_, _, headline, _, _, _), _, _) => headline
1.50 | _ => raise ERROR "getFormulaeFromTo: uncovered case of ME_Misc.pt_extract"
1.51 in getintervalOK cI [(to, headline, NONE)] end
1.52 @@ -268,11 +272,12 @@
1.53 "from=([],Res) .. goes beyond result")
1.54 | _ =>
1.55 let
1.56 - val ((pt,_),_) = States.get_calc cI
1.57 + val ((pt, p), _) = States.get_calc cI
1.58 + val ctxt = Ctree.get_ctxt_LI pt p
1.59 val f = move_dn [] pt from
1.60 fun max (a,b) = if a < b then b else a
1.61 val lev = max (level, max (lev_of from, lev_of to)) (*... must reach margins *)
1.62 - in getintervalOK cI (ME_Misc.get_interval f to lev pt) end)
1.63 + in getintervalOK cI (ME_Misc.get_interval ctxt f to lev pt) end)
1.64 \<close> of
1.65 SOME xml => xml
1.66 | NONE => sysERROR2xml cI "error in getFormulaeFromTo")
2.1 --- a/src/Tools/isac/Build_Isac.thy Sun Oct 23 16:08:27 2022 +0200
2.2 +++ b/src/Tools/isac/Build_Isac.thy Sun Oct 23 17:21:04 2022 +0200
2.3 @@ -168,6 +168,7 @@
2.4 \<close> ML \<open>
2.5 \<close> ML \<open>
2.6 \<close>
2.7 +(*----------------------- exclude in TEST_BASE ----------------------------------------(**)
2.8 subsection \<open>basic functionality on simple example first -- cp for first tests\<close>
2.9 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/000-comments.sml"
2.10 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/100-init-rootpbl.sml"
2.11 @@ -190,6 +191,7 @@
2.12 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/790-complete-NEXT_STEP.sml"
2.13 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/790-complete.sml"
2.14 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/800-append-on-Frm.sml"
2.15 +(**)----------------------- exclude in TEST_BASE ----------------------------------------*)
2.16
2.17
2.18 text \<open>
3.1 --- a/test/Tools/isac/BaseDefinitions/contextC.sml Sun Oct 23 16:08:27 2022 +0200
3.2 +++ b/test/Tools/isac/BaseDefinitions/contextC.sml Sun Oct 23 17:21:04 2022 +0200
3.3 @@ -299,7 +299,7 @@
3.4 | _ => if p = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
3.5
3.6 "~~~~~ from fun me \<longrightarrow>toplevel , return:"; val (p''''',_,f,nxt''''',_,pt''''')
3.7 - = (p, [] : NEW, TESTg_form (pt, p) (* form output comes from Step.by_tactic *),
3.8 + = (p, [] : NEW, TESTg_form ctxt (pt, p) (* form output comes from Step.by_tactic *),
3.9 tac, Celem.Sundef, pt);
3.10 (*\--------- step into 2. Check_Postcond -----------------------------------------------------/*)
3.11
4.1 --- a/test/Tools/isac/BridgeLibisabelle/interface.sml Sun Oct 23 16:08:27 2022 +0200
4.2 +++ b/test/Tools/isac/BridgeLibisabelle/interface.sml Sun Oct 23 17:21:04 2022 +0200
4.3 @@ -93,9 +93,9 @@
4.4 ############################################################################*)
4.5
4.6 writeln(pr_ctree pr_short pt);
4.7 -writeln(Test_Tool.posterms2str (ME_Misc.get_interval ([],Frm) ([],Res) 99999 pt));
4.8 +writeln(Test_Tool.posterms2str (ME_Misc.get_interval ctxt ([],Frm) ([],Res) 99999 pt));
4.9
4.10 -case map fst3 (ME_Misc.get_interval ([],Frm) ([],Res) 99999 pt) of
4.11 +case map fst3 (ME_Misc.get_interval ctxt ([],Frm) ([],Res) 99999 pt) of
4.12 [([], Frm),
4.13 ([1], Frm),
4.14 ([1, 1], Frm),
4.15 @@ -124,7 +124,7 @@
4.16 ([5], Res),
4.17 ([], Res)] => ()
4.18 | _ => error "diff.behav.in ctree.sml: ME_Misc.get_interval lev 1f";
4.19 -case map fst3 (ME_Misc.get_interval ([],Frm) ([],Res) 1 pt) of
4.20 +case map fst3 (ME_Misc.get_interval ctxt ([],Frm) ([],Res) 1 pt) of
4.21 [([], Frm),
4.22 ([1], Frm),
4.23 ([1], Res),
4.24 @@ -135,12 +135,12 @@
4.25 ([5], Res),
4.26 ([], Res)] => ()
4.27 | _ => error "diff.behav.in ctree.sml: ME_Misc.get_interval lev 1f";
4.28 -case map fst3 (ME_Misc.get_interval ([],Frm) ([],Res) 0 pt) of
4.29 +case map fst3 (ME_Misc.get_interval ctxt ([],Frm) ([],Res) 0 pt) of
4.30 [([], Frm),
4.31 ([], Res)] => ()
4.32 | _ => error "diff.behav.in ctree.sml: ME_Misc.get_interval lev 1f";
4.33
4.34 -case map fst3 (ME_Misc.get_interval ([1,3],Res) ([4,1,1],Frm) 99999 pt) of
4.35 +case map fst3 (ME_Misc.get_interval ctxt ([1,3],Res) ([4,1,1],Frm) 99999 pt) of
4.36 [([1, 3], Res),
4.37 ([1, 4], Res),
4.38 ([1], Res),
4.39 @@ -152,7 +152,7 @@
4.40 | _ => error "diff.behav.in ctree.sml: ME_Misc.get_interval lev 1a";
4.41
4.42 (*this pos' is not generated bu move_dn:......vvv: goes to end of calc*)
4.43 -case map fst3 (ME_Misc.get_interval ([2],Res) ([4,3,2],Frm) 99999 pt) of
4.44 +case map fst3 (ME_Misc.get_interval ctxt ([2],Res) ([4,3,2],Frm) 99999 pt) of
4.45 [([2], Res),
4.46 ([3], Res),
4.47 ([4], Pbl),
4.48 @@ -173,7 +173,7 @@
4.49 ([5], Res), (*this is beyond 'to'*)
4.50 ([], Res)] => () (*this is beyond 'to'*)
4.51 | _ => error "diff.behav.in ctree.sml: ME_Misc.get_interval lev 1b";
4.52 -case map fst3 (ME_Misc.get_interval ([1,4],Res) ([4,3,1],Frm) 99999 pt) of
4.53 +case map fst3 (ME_Misc.get_interval ctxt ([1,4],Res) ([4,3,1],Frm) 99999 pt) of
4.54 [([1, 4], Res),
4.55 ([1], Res),
4.56 ([2], Res),
4.57 @@ -187,7 +187,7 @@
4.58 ([4, 3], Pbl),
4.59 ([4, 3, 1], Frm)] => ()
4.60 | _ => error "diff.behav.in ctree.sml: ME_Misc.get_interval lev 1c";
4.61 -case map fst3 (ME_Misc.get_interval ([4,2],Res) ([5],Res) 99999 pt) of
4.62 +case map fst3 (ME_Misc.get_interval ctxt ([4,2],Res) ([5],Res) 99999 pt) of
4.63 [([4, 2], Res),
4.64 ([4, 3], Pbl),
4.65 ([4, 3, 1], Frm),
4.66 @@ -200,7 +200,7 @@
4.67 ([4], Res),
4.68 ([5], Res)]=>()
4.69 | _ => error "diff.behav.in ctree.sml: ME_Misc.get_interval lev 1d";
4.70 -case map fst3 (ME_Misc.get_interval ([],Frm) ([4,3,2],Res) 99999 pt) of
4.71 +case map fst3 (ME_Misc.get_interval ctxt ([],Frm) ([4,3,2],Res) 99999 pt) of
4.72 [([], Frm),
4.73 ([1], Frm),
4.74 ([1, 1], Frm),
4.75 @@ -222,7 +222,7 @@
4.76 ([4, 3, 1], Res),
4.77 ([4, 3, 2], Res)] => ()
4.78 | _ => error "diff.behav.in ctree.sml: ME_Misc.get_interval lev 1e";
4.79 -case map fst3 (ME_Misc.get_interval ([4,3],Frm) ([4,3],Res) 99999 pt) of
4.80 +case map fst3 (ME_Misc.get_interval ctxt ([4,3],Frm) ([4,3],Res) 99999 pt) of
4.81 [([4, 3], Frm),
4.82 ([4, 3, 1], Frm),
4.83 ([4, 3, 1], Res),
5.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Sun Oct 23 16:08:27 2022 +0200
5.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Sun Oct 23 17:21:04 2022 +0200
5.3 @@ -256,7 +256,7 @@
5.4 val ((pt,_),_) = States.get_calc 1;
5.5 val ip = States.get_pos 1 1;
5.6
5.7 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, ip);
5.8 + val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, ip);
5.9 (*exception just above means: 'ModSpec' has been returned: error anyway*)
5.10 if ip = ([], Res) andalso UnparseC.term f = "[x = 1]" then () else
5.11 error "FE-Kernel-interface.sml: diff.behav. in solve_linear as rootpbl";
5.12 @@ -458,7 +458,7 @@
5.13 (*this checks the test for correctness..*)
5.14 val ((pt,_),_) = States.get_calc 1;
5.15 val p = States.get_pos 1 1;
5.16 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
5.17 + val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
5.18 if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
5.19 error "FE-interface.sml: diff.behav. in miniscript with mini-subpb";
5.20 DEconstrCalcTree 1;
5.21 @@ -483,7 +483,7 @@
5.22
5.23 val ((pt,_),_) = States.get_calc 1;
5.24 val p = States.get_pos 1 1;
5.25 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
5.26 + val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
5.27 if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
5.28 error "FE-interface.sml: diff.behav. in solve_linear/rt AUTOCALCULATE ";
5.29 DEconstrCalcTree 1;
5.30 @@ -534,7 +534,7 @@
5.31
5.32 val ((pt,_),_) = States.get_calc 1;
5.33 val p = States.get_pos 1 1;
5.34 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
5.35 + val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
5.36 if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
5.37 error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
5.38 DEconstrCalcTree 1;
5.39 @@ -596,7 +596,7 @@
5.40 refFormula 1 (States.get_pos 1 1);
5.41 val ((pt,_),_) = States.get_calc 1;
5.42 val p = States.get_pos 1 1;
5.43 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
5.44 + val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
5.45 if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
5.46 error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
5.47 DEconstrCalcTree 1;
5.48 @@ -624,13 +624,13 @@
5.49 autoCalculate 1 (Steps 1);
5.50 (*setContext 1 p "thy_isac_Test-rls-Test_simplify";*)
5.51 val (((pt,_),_), p) = (States.get_calc 1, States.get_pos 1 1);
5.52 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
5.53 + val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
5.54 if p = ([1], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "x + 1 + - 1 * 2 = 0"
5.55 then () else error "--- setContext..Thy --- autoCalculate 1 (Steps 1) #1";
5.56
5.57 autoCalculate 1 CompleteCalc;
5.58 val (((pt,_),_), p) = (States.get_calc 1, States.get_pos 1 1);
5.59 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
5.60 + val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
5.61
5.62 if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then ()
5.63 else error "--- setContext..Thy --- autoCalculate CompleteCalc";
5.64 @@ -662,7 +662,7 @@
5.65 val ((pt,_),_) = States.get_calc 1;
5.66 val p = States.get_pos 1 1;
5.67
5.68 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
5.69 + val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
5.70 if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
5.71 error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl 1";
5.72 DEconstrCalcTree 1;
5.73 @@ -750,7 +750,7 @@
5.74 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
5.75 setNextTactic 1 (Check_Postcond ["rational", "univariate", "equation"]);
5.76 val (ptp,_) = States.get_calc 1;
5.77 - val (Form t,_,_) = ME_Misc.pt_extract ptp;
5.78 + val (Form t,_,_) = ME_Misc.pt_extract ctxt ptp;
5.79 if States.get_pos 1 1 = ([], Res) andalso UnparseC.term t = "[x = -4 / 3]" then ()
5.80 else writeln "FE-inteface.sml: diff.behav. in rat-eq + subpbl: no_met, NO ..";
5.81 DEconstrCalcTree 1;
5.82 @@ -850,7 +850,7 @@
5.83 val ((pt,_),_) = States.get_calc 1;
5.84 Test_Tool.show_pt pt;
5.85 val p = States.get_pos 1 1;
5.86 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
5.87 + val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
5.88 if UnparseC.term f = "[x = - 1, x = -3]" andalso p = ([], Res) then () else
5.89 error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
5.90
5.91 @@ -873,7 +873,7 @@
5.92 rootthy pt;
5.93 Test_Tool.show_pt pt;
5.94 val p = States.get_pos 1 1;
5.95 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
5.96 + val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
5.97 if UnparseC.term f = "[x = - 1, x = -3]" andalso p = ([], Res) then () else
5.98 error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
5.99 DEconstrCalcTree 1;
5.100 @@ -1047,7 +1047,7 @@
5.101 refFormula 1 (States.get_pos 1 1);
5.102 val ((pt,_),_) = States.get_calc 1;
5.103 val p = States.get_pos 1 1;
5.104 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
5.105 + val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
5.106 if UnparseC.term f = "[x = 1]" andalso p = ([], Res) andalso map UnparseC.term asms = [] then ()
5.107 else error "FE-interface.sml: diff.behav. in from pbl -hierarchy 1";
5.108 DEconstrCalcTree 1;
5.109 @@ -1065,7 +1065,7 @@
5.110 refFormula 1 (States.get_pos 1 1);
5.111 val ((pt,_),_) = States.get_calc 1;
5.112 val p = States.get_pos 1 1;
5.113 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
5.114 + val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
5.115 if UnparseC.term f = "[x = 1]" andalso p = ([], Res) andalso map UnparseC.term asms = [] then ()
5.116 else error "FE-interface.sml: diff.behav. in from pbl -hierarchy 2";
5.117 DEconstrCalcTree 1;
5.118 @@ -1151,7 +1151,7 @@
5.119 autoCalculate 1 CompleteCalc;
5.120 val ((pt,_),_) = States.get_calc 1;
5.121 val p = States.get_pos 1 1;
5.122 -val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
5.123 +val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
5.124 (*============ inhibit exn WN120316 compare 2002-- 2011 ===========================
5.125 if map UnparseC.term asms =
5.126 ["True |\n~ lhs ((3 + - 1 * x + x \<up> 2) * x =\n" ^
5.127 @@ -1221,7 +1221,7 @@
5.128 autoCalculate 1 CompleteCalc;
5.129 val ((pt,_),_) = States.get_calc 1;
5.130 val p = States.get_pos 1 1;
5.131 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
5.132 + val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
5.133 if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
5.134 error "FE-interface.sml: diff.behav. in combinations of steps";
5.135 DEconstrCalcTree 1;
5.136 @@ -1245,7 +1245,7 @@
5.137
5.138 val ((pt,_),_) = States.get_calc 1;
5.139 val p = States.get_pos 1 1;
5.140 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
5.141 + val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
5.142 if UnparseC.term f = "- 1 + x = 0" andalso p = ([2], Res) then () else
5.143 error "FE-interface.sml: diff.behav. in FORMULA:enter} right";
5.144 DEconstrCalcTree 1;
5.145 @@ -1268,7 +1268,7 @@
5.146
5.147 val ((pt,_),_) = States.get_calc 1;
5.148 val p = States.get_pos 1 1;
5.149 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
5.150 + val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
5.151 if UnparseC.term f = "x - 1 = 0" andalso p = ([2], Res) then () else
5.152 error "FE-interface.sml: diff.behav. in FORMULA:enter} other";
5.153 DEconstrCalcTree 1;
5.154 @@ -1292,7 +1292,7 @@
5.155
5.156 val ((pt,_),_) = States.get_calc 1;
5.157 val p = States.get_pos 1 1;
5.158 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
5.159 + val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
5.160 if UnparseC.term f = "x = 1" andalso p = ([3,2], Res) then () else
5.161 error "FE-interface.sml: diff.behav. in FORMULA:enter} oth 2";
5.162 DEconstrCalcTree 1;
5.163 @@ -1313,7 +1313,7 @@
5.164
5.165 val ((pt,_),_) = States.get_calc 1;
5.166 val p = States.get_pos 1 1;
5.167 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
5.168 + val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
5.169 if UnparseC.term f = "x + 1 + - 1 * 2 = 0" andalso p = ([1], Res) then () else
5.170 error "FE-interface.sml: diff.behav. in FORMULA:enter} NOTok";
5.171 DEconstrCalcTree 1;
5.172 @@ -1334,10 +1334,10 @@
5.173
5.174 val ((pt,_),_) = States.get_calc 1;
5.175 val p = States.get_pos 1 1;
5.176 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
5.177 + val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
5.178 if UnparseC.term f = "- 1 + x = 0" andalso p = ([2], Res) then () else
5.179 error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
5.180 - if map fst3 (ME_Misc.get_interval ([2],Res) ([],Res) 9999 pt) =
5.181 + if map fst3 (ME_Misc.get_interval ctxt ([2],Res) ([],Res) 9999 pt) =
5.182 [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
5.183 ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else
5.184 error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2";
5.185 @@ -1355,10 +1355,10 @@
5.186
5.187 val ((pt,_),_) = States.get_calc 2;
5.188 val p = States.get_pos 2 1;
5.189 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
5.190 + val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
5.191 if UnparseC.term f = "- 1 + x = 0" andalso p = ([2], Res) then () else
5.192 error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
5.193 - if map fst3 (ME_Misc.get_interval ([2],Res) ([],Res) 9999 pt) =
5.194 + if map fst3 (ME_Misc.get_interval ctxt ([2],Res) ([],Res) 9999 pt) =
5.195 [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
5.196 ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else
5.197 error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2b";
5.198 @@ -1383,13 +1383,13 @@
5.199 val ((pt,_),_) = States.get_calc 1;
5.200 Test_Tool.show_pt pt;
5.201 val p = States.get_pos 1 1;
5.202 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
5.203 + val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
5.204 if UnparseC.term f = "x - 1 = 0" andalso p = ([2], Res) then () else
5.205 error "FE-interface.sml: diff.behav. in FORMULA:replace} other 1";
5.206 (* for getting the list in whole length ...
5.207 -(*default_print_depth 99*) map fst3 (ME_Misc.get_interval ([1],Res) ([],Res) 9999 pt); (*default_print_depth 3*)
5.208 +(*default_print_depth 99*) map fst3 (ME_Misc.get_interval ctxt ([1],Res) ([],Res) 9999 pt); (*default_print_depth 3*)
5.209 *)
5.210 - if map fst3 (ME_Misc.get_interval ([1],Res) ([],Res) 9999 pt) =
5.211 + if map fst3 (ME_Misc.get_interval ctxt ([1],Res) ([],Res) 9999 pt) =
5.212 [([1], Res), ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
5.213 ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2, 7], Res),
5.214 ([2, 8], Res), ([2, 9], Res), ([2], Res)] then () else
5.215 @@ -1416,14 +1416,14 @@
5.216 val ((pt,_),_) = States.get_calc 1;
5.217 Test_Tool.show_pt pt; (*error: ...ME_Misc.get_interval drops ([3,2],Res) ...*)
5.218 val (t,_) = get_obj g_result pt [3,2]; UnparseC.term t;
5.219 - if map fst3 (ME_Misc.get_interval ([1],Res) ([],Res) 9999 pt) =
5.220 + if map fst3 (ME_Misc.get_interval ctxt ([1],Res) ([],Res) 9999 pt) =
5.221 [([1], Res), ([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res),
5.222 ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
5.223 ([3,2],Res)] then () else
5.224 error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 1";
5.225
5.226 val p = States.get_pos 1 1;
5.227 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
5.228 + val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
5.229 if UnparseC.term f = "x = 1" andalso p = ([3,2], Res) then () else
5.230 error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 2";
5.231 DEconstrCalcTree 1;
5.232 @@ -1445,7 +1445,7 @@
5.233 val ((pt,_),_) = States.get_calc 1;
5.234 Test_Tool.show_pt pt;
5.235 val p = States.get_pos 1 1;
5.236 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
5.237 + val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
5.238 if UnparseC.term f = "- 1 + x = 0" andalso p = ([2], Res) then () else
5.239 error "FE-interface.sml: diff.behav. in FORMULA:replace} NOTok";
5.240 DEconstrCalcTree 1;
5.241 @@ -1468,7 +1468,7 @@
5.242 instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)
5.243 val ((pt,pos), _) = States.get_calc 1;
5.244 val p = States.get_pos 1 1;
5.245 - val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
5.246 + val (Form f, _, asms) = ME_Misc.pt_extract ctxt (pt, p);
5.247
5.248 if p = ([1], Res) andalso UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))"
5.249 then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"],
5.250 @@ -1483,7 +1483,7 @@
5.251 val ((pt,pos),_) = States.get_calc 1;
5.252 val p = States.get_pos 1 1;
5.253
5.254 - val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
5.255 + val (Form f, _, asms) = ME_Misc.pt_extract ctxt (pt, p);
5.256 if p = ([1], Res) andalso UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" andalso
5.257 get_obj g_tac pt (fst p) = Rewrite_Inst (["(''bdv'', x)"], ("diff_sum", "Diff.diff_sum"(*?!?*)))
5.258 then ()
5.259 @@ -1496,7 +1496,7 @@
5.260 (*<AUTOCALC> ([1], Res) ([2], Res) ([2], Res) </AUTOCALC>*)
5.261 val ((pt,pos),_) = States.get_calc 1;
5.262 val p = States.get_pos 1 1;
5.263 - val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
5.264 + val (Form f, _, asms) = ME_Misc.pt_extract ctxt (pt, p);
5.265 if p = ([1], Res) andalso existpt [2] pt andalso
5.266 UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up>\<up> 4))" andalso
5.267 get_obj g_tac pt (fst p) = Rewrite_Inst (["(''bdv'', x)"], ("diff_sum", "Diff.diff_sum"))
5.268 @@ -1505,7 +1505,7 @@
5.269 inputFillFormula 1 "d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x (x \<up> 4)";(*<<<<<<<=====*)
5.270 val ((pt, _),_) = States.get_calc 1;
5.271 val p = States.get_pos 1 1;
5.272 - val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
5.273 + val (Form f, _, asms) = ME_Misc.pt_extract ctxt (pt, p);
5.274 if p = ([2], Res) andalso
5.275 UnparseC.term f = "d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x (x \<up> 4)" andalso
5.276 get_obj g_tac pt (fst p) = Rewrite_Inst (["(''bdv'', x)"], ("diff_sin_chain", ""))
5.277 @@ -1516,7 +1516,7 @@
5.278 "~~~~~ final check: the input formula is inserted as it would have been correct from beginning";
5.279 val ((pt, _),_) = States.get_calc 1;
5.280 val p = States.get_pos 1 1;
5.281 -val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
5.282 +val (Form f, _, asms) = ME_Misc.pt_extract ctxt (pt, p);
5.283 if p = ([], Res) andalso UnparseC.term f = "2 * x + cos (x \<up> 4) * 4 * x \<up> 3"
5.284 then () else error "inputFillFormula changed 12";
5.285 Test_Tool.show_pt pt;
6.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Sun Oct 23 16:08:27 2022 +0200
6.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Sun Oct 23 17:21:04 2022 +0200
6.3 @@ -740,7 +740,7 @@
6.4 (*7>*)fetchProposedTactic 1 (*--> Apply_Method*);
6.5 autoCalculate 1 (Steps 1);
6.6 val ((pt,p),_) = States.get_calc 1;
6.7 -val Form res = (#1 o ME_Misc.pt_extract) (pt, p);
6.8 +val Form res = (#1 o (ME_Misc.pt_extract ctxt)) (pt, p);
6.9 if UnparseC.term res = "d_d x (x \<up> 2 + x + 1)" then ()
6.10 else error "diff.sml Diff (x \<up> 2 + x + 1, x) from exp";
6.11 DEconstrCalcTree 1;
6.12 @@ -1173,7 +1173,7 @@
6.13 instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)
6.14 val ((pt,pos), _) = States.get_calc 1;
6.15 val p = States.get_pos 1 1;
6.16 - val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
6.17 + val (Form f, _, asms) = ME_Misc.pt_extract ctxt (pt, p);
6.18
6.19 if p = ([1], Res) andalso UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" then
6.20 case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"],
6.21 @@ -1189,7 +1189,7 @@
6.22 val ((pt,pos),_) = States.get_calc 1;
6.23 val p = States.get_pos 1 1;
6.24
6.25 - val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
6.26 + val (Form f, _, asms) = ME_Misc.pt_extract ctxt (pt, p);
6.27 if p = ([1], Res) andalso UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" then
6.28 case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"],
6.29 ("diff_sum", thm)) =>
6.30 @@ -1202,7 +1202,7 @@
6.31 (*<AUTOCALC> ([1], Res) ([2], Res) ([2], Res) </AUTOCALC>*)
6.32 val ((pt,pos),_) = States.get_calc 1;
6.33 val p = States.get_pos 1 1;
6.34 - val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
6.35 + val (Form f, _, asms) = ME_Misc.pt_extract ctxt (pt, p);
6.36 if p = ([1], Res) andalso existpt [2] pt
6.37 andalso UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))"
6.38 then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"],
6.39 @@ -1241,7 +1241,7 @@
6.40 "~~~~~ final check:";
6.41 val ((pt, _),_) = States.get_calc 1;
6.42 val p = States.get_pos 1 1;
6.43 -val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
6.44 +val (Form f, _, asms) = ME_Misc.pt_extract ctxt (pt, p);
6.45 if p = ([2], Res) andalso UnparseC.term f = "d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x (x \<up> 4)"
6.46 then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"],
6.47 ("diff_sin_chain", thm)) =>
7.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Sun Oct 23 16:08:27 2022 +0200
7.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Sun Oct 23 17:21:04 2022 +0200
7.3 @@ -282,9 +282,9 @@
7.4 tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
7.5 | _ => if p = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
7.6
7.7 - (p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Celem.Sundef, pt);
7.8 + (p, [] : NEW, TESTg_form ctxt (pt, p), (Tactic.tac2IDstr tac, tac), Celem.Sundef, pt);
7.9 "~~~~~ from me to TOOPLEVEL return:"; val (p,_,f,nxt,_,pt)
7.10 - = (*** )xxx( ***) (p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Celem.Sundef, pt);
7.11 + = (*** )xxx( ***) (p, [] : NEW, TESTg_form ctxt (pt, p), (Tactic.tac2IDstr tac, tac), Celem.Sundef, pt);
7.12
7.13 (*//--------------------- check results from modified me ----------------------------------\\*)
7.14 if p = ([2], Res) andalso
8.1 --- a/test/Tools/isac/Knowledge/inssort.sml Sun Oct 23 16:08:27 2022 +0200
8.2 +++ b/test/Tools/isac/Knowledge/inssort.sml Sun Oct 23 17:21:04 2022 +0200
8.3 @@ -176,5 +176,5 @@
8.4 val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
8.5
8.6 if p = ([], Res)andalso UnparseC.term (get_obj g_res pt (fst p)) = "{|| 1, 2, 3 ||}"
8.7 -andalso length (ME_Misc.get_interval ([], Pbl) ([], Res) 1 pt) = 23 then ()
8.8 +andalso length (ME_Misc.get_interval ctxt ([], Pbl) ([], Res) 1 pt) = 23 then ()
8.9 else error "met_Prog_sort_ins_steps CHANGED"
9.1 --- a/test/Tools/isac/Knowledge/integrate.sml Sun Oct 23 16:08:27 2022 +0200
9.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Sun Oct 23 17:21:04 2022 +0200
9.3 @@ -414,7 +414,7 @@
9.4 moveActiveRoot 1;
9.5 autoCalculate 1 CompleteCalc;
9.6 val ((pt,p),_) = States.get_calc 1; @{make_string} p; Test_Tool.show_pt pt;
9.7 -val (Form t,_,_) = ME_Misc.pt_extract (pt, p);
9.8 +val (Form t,_,_) = ME_Misc.pt_extract ctxt (pt, p);
9.9 if UnparseC.term t = "c + x + 1 / 3 * x \<up> 3" then ()
9.10 else error "integrate.sml -- interSteps [diff,integration] -- result";
9.11
10.1 --- a/test/Tools/isac/Knowledge/rational-2.sml Sun Oct 23 16:08:27 2022 +0200
10.2 +++ b/test/Tools/isac/Knowledge/rational-2.sml Sun Oct 23 17:21:04 2022 +0200
10.3 @@ -1549,7 +1549,7 @@
10.4
10.5 val p = ([2,1,9],Res);
10.6 getTactic 1 p;
10.7 -val (_, tac, _) = ME_Misc.pt_extract (pt, p);
10.8 +val (_, tac, _) = ME_Misc.pt_extract ctxt (pt, p);
10.9 case tac of SOME (Rewrite ("sym_distrib_left", _)) => ()
10.10 | _ => error "rational.sml: getTactic, sym_real_plus_binom_times1";
10.11
11.1 --- a/test/Tools/isac/Knowledge/simplify.sml Sun Oct 23 16:08:27 2022 +0200
11.2 +++ b/test/Tools/isac/Knowledge/simplify.sml Sun Oct 23 17:21:04 2022 +0200
11.3 @@ -48,7 +48,7 @@
11.4 val ((pt,p),_) = States.get_calc 1;
11.5 Test_Tool.show_pt pt; (*[
11.6 (([], Frm), Simplify (14 * x * y / (x * y)))] *)
11.7 -ME_Misc.pt_extract (pt, p); (*determines SOME (Apply_Method ["simplification", "of_rationals"])*)
11.8 +ME_Misc.pt_extract ctxt (pt, p); (*determines SOME (Apply_Method ["simplification", "of_rationals"])*)
11.9
11.10 (*/------------------- step into autoCalculate 1 (Steps 1) \<longrightarrow> Apply_Method ----------------\*)
11.11 "~~~~~ fun autoCalculate , args:"; val (cI, auto) = (1, Steps 1);
11.12 @@ -146,7 +146,7 @@
11.13 (([1,3], Res), 14),
11.14 (([1], Res), 14),
11.15 (([], Res), 14)] *)
11.16 -val Form res = (#1 o ME_Misc.pt_extract) (pt, ([],Res));
11.17 +val Form res = (#1 o (ME_Misc.pt_extract ctxt)) (pt, ([],Res));
11.18
11.19 if p = ([], Res) andalso UnparseC.term res = "14" then ()
11.20 else error "simplify.sml: append inform with final result changed";
12.1 --- a/test/Tools/isac/MathEngBasic/ctree.sml Sun Oct 23 16:08:27 2022 +0200
12.2 +++ b/test/Tools/isac/MathEngBasic/ctree.sml Sun Oct 23 17:21:04 2022 +0200
12.3 @@ -229,7 +229,7 @@
12.4 error "ctree.sml: diff:behav. in cut_level 1ab";
12.5 ============ inhibit exn AK110726 ==============================================*)
12.6 (*============ inhibit exn AK110726 ==============================================
12.7 -if map fst3 (ME_Misc.get_interval ([],Frm) ([],Res) 9999 pt') =
12.8 +if map fst3 (ME_Misc.get_interval ctxt ([],Frm) ([],Res) 9999 pt') =
12.9 [([], Frm),
12.10 ([1], Frm),
12.11 ([1], Res),
12.12 @@ -300,7 +300,7 @@
12.13 if res = TermC.empty (*WN050219 done by cut_tree*) then () else
12.14 error "ctree.sml: diff:behav. in cut_tree 1ac";
12.15
12.16 -if map fst3 (ME_Misc.get_interval ([],Frm) ([],Res) 9999 pt') =
12.17 +if map fst3 (ME_Misc.get_interval ctxt ([],Frm) ([],Res) 9999 pt') =
12.18 [([], Frm),
12.19 ([1], Frm),
12.20 ([1], Res)] then () else
12.21 @@ -373,7 +373,7 @@
12.22 Test_Tool.show_pt pt;
12.23 Test_Tool.show_pt pt';
12.24 (*default_print_depth 99;*)cuts;(*default_print_depth 3;*)
12.25 -(*default_print_depth 99;*)map fst3 (ME_Misc.get_interval ([],Frm) ([],Res) 9999 pt');(*default_print_depth 3;*)
12.26 +(*default_print_depth 99;*)map fst3 (ME_Misc.get_interval ctxt ([],Frm) ([],Res) 9999 pt');(*default_print_depth 3;*)
12.27 ####################################################################*)
12.28
12.29
12.30 @@ -886,7 +886,7 @@
12.31 "-------------- ME_Misc.pt_extract form, tac, asm<>[] --------------------";
12.32 "-------------- ME_Misc.pt_extract form, tac, asm<>[] --------------------";
12.33 "-------------- ME_Misc.pt_extract form, tac, asm<>[] --------------------";
12.34 -val (Form form, SOME tac, asm) = ME_Misc.pt_extract (pt, ([3], Res));
12.35 +val (Form form, SOME tac, asm) = ME_Misc.pt_extract ctxt (pt, ([3], Res));
12.36 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
12.37 ("(3 + - 1 * x + x \<up> 2) * x = 1 * (9 * x + - 6 * x \<up> 2 + x \<up> 3)",
12.38 Subproblem
12.39 @@ -924,68 +924,68 @@
12.40 "-------------- ME_Misc.pt_extract form, tac, asm ------------------------";
12.41 "-------------- ME_Misc.pt_extract form, tac, asm ------------------------";
12.42 "-------------- ME_Misc.pt_extract form, tac, asm ------------------------";
12.43 -val (ModSpec (_,_,form,_,_,_), SOME tac, asm) = ME_Misc.pt_extract (pt, ([], Frm));
12.44 +val (ModSpec (_,_,form,_,_,_), SOME tac, asm) = ME_Misc.pt_extract ctxt (pt, ([], Frm));
12.45 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
12.46 ("solve (x + 1 = 2, x)",
12.47 Apply_Method ["Test", "squ-equ-test-subpbl1"],
12.48 []) => ()
12.49 - | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract ([], Pbl)";
12.50 + | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract ctxt ([], Pbl)";
12.51
12.52 -val (Form form, SOME tac, asm) = ME_Misc.pt_extract (pt, ([1], Frm));
12.53 +val (Form form, SOME tac, asm) = ME_Misc.pt_extract ctxt (pt, ([1], Frm));
12.54 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
12.55 ("x + 1 = 2", Rewrite_Set "norm_equation", []) => ()
12.56 - | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract ([1], Frm)";
12.57 + | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract ctxt ([1], Frm)";
12.58
12.59 -val (Form form, SOME tac, asm) = ME_Misc.pt_extract (pt, ([1], Res));
12.60 +val (Form form, SOME tac, asm) = ME_Misc.pt_extract ctxt (pt, ([1], Res));
12.61 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
12.62 ("x + 1 + - 1 * 2 = 0", Rewrite_Set "Test_simplify", []) => ()
12.63 - | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract ([1], Res)";
12.64 + | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract ctxt ([1], Res)";
12.65
12.66 -val (Form form, SOME tac, asm) = ME_Misc.pt_extract (pt, ([2], Res));
12.67 +val (Form form, SOME tac, asm) = ME_Misc.pt_extract ctxt (pt, ([2], Res));
12.68 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
12.69 ("- 1 + x = 0",
12.70 Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),
12.71 []) => ()
12.72 - | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract ([2], Res)";
12.73 + | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract ctxt ([2], Res)";
12.74
12.75 -val (ModSpec (_,_,form,_,_,_), SOME tac, asm) = ME_Misc.pt_extract (pt, ([3], Pbl));
12.76 +val (ModSpec (_,_,form,_,_,_), SOME tac, asm) = ME_Misc.pt_extract ctxt (pt, ([3], Pbl));
12.77 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
12.78 ("solve (- 1 + x = 0, x)", Apply_Method ["Test", "solve_linear"], []) => ()
12.79 - | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract ([3], Pbl)";
12.80 + | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract ctxt ([3], Pbl)";
12.81
12.82 -val (Form form, SOME tac, asm) = ME_Misc.pt_extract (pt, ([3,1], Frm));
12.83 +val (Form form, SOME tac, asm) = ME_Misc.pt_extract ctxt (pt, ([3,1], Frm));
12.84 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
12.85 ("- 1 + x = 0", Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv"), []) => ()
12.86 - | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract ([3,1], Frm)";
12.87 + | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract ctxt ([3,1], Frm)";
12.88
12.89 -val (Form form, SOME tac, asm) = ME_Misc.pt_extract (pt, ([3,1], Res));
12.90 +val (Form form, SOME tac, asm) = ME_Misc.pt_extract ctxt (pt, ([3,1], Res));
12.91 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
12.92 ("x = 0 + - 1 * - 1", Rewrite_Set "Test_simplify", []) => ()
12.93 - | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract ([3,1], Res)";
12.94 + | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract ctxt ([3,1], Res)";
12.95
12.96 -val (Form form, SOME tac, asm) = ME_Misc.pt_extract (pt, ([3,2], Res));
12.97 +val (Form form, SOME tac, asm) = ME_Misc.pt_extract ctxt (pt, ([3,2], Res));
12.98 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
12.99 ("x = 1", Check_Postcond ["LINEAR", "univariate", "equation", "test"],
12.100 []) => ()
12.101 - | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract ([3,2], Res)";
12.102 + | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract ctxt ([3,2], Res)";
12.103
12.104 (*========== inhibit exn AK110719 ==============================================
12.105 -val (Form form, SOME tac, asm) = ME_Misc.pt_extract (pt, ([3], Res));
12.106 +val (Form form, SOME tac, asm) = ME_Misc.pt_extract ctxt (pt, ([3], Res));
12.107 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
12.108 ("[x = 1]", Check_elementwise "Assumptions", []) => ()
12.109 - | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract ([3], Res)";
12.110 + | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract ctxt ([3], Res)";
12.111
12.112 -val (Form form, SOME tac, asm) = ME_Misc.pt_extract (pt, ([4], Res));
12.113 +val (Form form, SOME tac, asm) = ME_Misc.pt_extract ctxt (pt, ([4], Res));
12.114 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
12.115 ("[x = 1]",
12.116 Check_Postcond ["sqroot-test", "univariate", "equation", "test"],
12.117 []) => ()
12.118 - | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract ([4], Res)";
12.119 + | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract ctxt ([4], Res)";
12.120
12.121 -val (Form form, tac, asm) = ME_Misc.pt_extract (pt, ([], Res));
12.122 +val (Form form, tac, asm) = ME_Misc.pt_extract ctxt (pt, ([], Res));
12.123 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
12.124 ("[x = 1]", NONE, []) => ()
12.125 - | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract ([], Res)";
12.126 + | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract ctxt ([], Res)";
12.127 ========== inhibit exn AK110719 ==============================================*)
12.128
12.129 "=====new ctree 6 minisubpbl intersteps ==========================";
13.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Sun Oct 23 16:08:27 2022 +0200
13.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Sun Oct 23 17:21:04 2022 +0200
13.3 @@ -117,7 +117,7 @@
13.4 Step_Specify.nxt_specify_init_calc ctxt (fmz, sp);
13.5 "~~~~~ fun nxt_specify_init_calc , args:"; val (fmz, (dI, pI, mI)) = (fmz, sp);
13.6 (*val (_, hdl, (dI, pI, mI), pors, pctxt) =*)
13.7 - initialise (fmz, (dI, pI, mI));
13.8 + initialise ctxt (fmz, (dI, pI, mI));
13.9 "~~~~~ fun initialise , args:"; val (fmz, (dI, pI, mI)) = (fmz, (dI, pI, mI));
13.10 val thy = ThyC.get_theory dI
13.11 val ctxt = Proof_Context.init_global thy;
14.1 --- a/test/Tools/isac/MathEngine/me-misc.sml Sun Oct 23 16:08:27 2022 +0200
14.2 +++ b/test/Tools/isac/MathEngine/me-misc.sml Sun Oct 23 17:21:04 2022 +0200
14.3 @@ -27,15 +27,15 @@
14.4 val (unc, del, gen) = (([1],Res), ([4],Res), ([3,2],Res));
14.5 val ((pt,_),_) = States.get_calc 1;
14.6
14.7 -(*default_print_depth 99*)map fst3 (ME_Misc.get_interval ([],Pbl) ([],Res) 9999 pt);(*default_print_depth 3*)
14.8 -if map fst3 (ME_Misc.get_interval ([],Pbl) ([],Res) 9999 pt) =
14.9 +(*default_print_depth 99*)map fst3 (ME_Misc.get_interval ctxt ([],Pbl) ([],Res) 9999 pt);(*default_print_depth 3*)
14.10 +if map fst3 (ME_Misc.get_interval ctxt ([],Pbl) ([],Res) 9999 pt) =
14.11 [([], Pbl), ([1], Frm),([1], Res), ([2], Res), ([3], Pbl), ([3, 1], Frm),
14.12 ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
14.13 ([3, 2], Res)] then () else
14.14 error "calchead.sml: diff.behav. ME_Misc.get_interval after replace} other 2 a";
14.15
14.16 -(*default_print_depth 99*)map fst3 (ME_Misc.get_interval ([3, 2, 1], Res) ([],Res) 9999 pt); (*default_print_depth 3*)
14.17 -if map fst3 (ME_Misc.get_interval ([3, 2, 1], Res) ([],Res) 9999 pt) =
14.18 +(*default_print_depth 99*)map fst3 (ME_Misc.get_interval ctxt ([3, 2, 1], Res) ([],Res) 9999 pt); (*default_print_depth 3*)
14.19 +if map fst3 (ME_Misc.get_interval ctxt ([3, 2, 1], Res) ([],Res) 9999 pt) =
14.20 [([3, 2, 1], Res), ([3, 2, 2], Res), ([3, 2], Res)] then () else
14.21 error "modspec.sml: diff.behav. ME_Misc.get_interval after replace} other 2 b";
14.22
15.1 --- a/test/Tools/isac/MathEngine/solve.sml Sun Oct 23 16:08:27 2022 +0200
15.2 +++ b/test/Tools/isac/MathEngine/solve.sml Sun Oct 23 17:21:04 2022 +0200
15.3 @@ -52,7 +52,7 @@
15.4
15.5 getTactic 1 ([6,1,1], Frm); (*WN130909 <ERROR> syserror in getTactic </ERROR>*)
15.6 val ((pt,_),_) = States.get_calc 1; Test_Tool.show_pt pt;
15.7 -val (Form form, SOME tac, asm) = ME_Misc.pt_extract (pt, ([6], Res));
15.8 +val (Form form, SOME tac, asm) = ME_Misc.pt_extract ctxt (pt, ([6], Res));
15.9 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
15.10 ("1 / 2", Check_Postcond ["rational", "simplification"], []) => ()
15.11 | _ => error "solve.sml: interSteps on norm_Rational 2";
16.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Sun Oct 23 16:08:27 2022 +0200
16.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Sun Oct 23 17:21:04 2022 +0200
16.3 @@ -84,7 +84,7 @@
16.4 val tacis as (_::_) = (*case*) ts (*of*);
16.5 val (tac, _, _) = last_elem tacis;
16.6
16.7 - (p, [] : NEW, TESTg_form (pt'''''_', p'''''_'), tac, Celem.Sundef, pt) (*return from me*);
16.8 + (p, [] : NEW, TESTg_form ctxt (pt'''''_', p'''''_'), tac, Celem.Sundef, pt) (*return from me*);
16.9 (*\------------------- end step into 1 -----------------------------------------------------/*)
16.10
16.11 (*/------------------- begin step into 2 ---------------------------------------------------\*)
17.1 --- a/test/Tools/isac/ProgLang/auto_prog.sml Sun Oct 23 16:08:27 2022 +0200
17.2 +++ b/test/Tools/isac/ProgLang/auto_prog.sml Sun Oct 23 17:21:04 2022 +0200
17.3 @@ -200,7 +200,7 @@
17.4 \ ((Rewrite_Set norm_Rational) t_)"
17.5 val (Form form, SOME tac, asm) = ME_Misc.pt_extract (pt, ([1], Res));
17.6 *)
17.7 -val (Form form, SOME tac, asm) = ME_Misc.pt_extract (pt, ([2], Res));
17.8 +val (Form form, SOME tac, asm) = ME_Misc.pt_extract ctxt (pt, ([2], Res));
17.9 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
17.10 ("a", Check_Postcond ["polynomial", "simplification"], []) => ()
17.11 | _ => error "scrtools.sml: auto-generated norm_Rational doesnt work";
18.1 --- a/test/Tools/isac/Specify/o-model.sml Sun Oct 23 16:08:27 2022 +0200
18.2 +++ b/test/Tools/isac/Specify/o-model.sml Sun Oct 23 17:21:04 2022 +0200
18.3 @@ -29,13 +29,14 @@
18.4 val f_spec = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]);
18.5 (*[], Pbl*)val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(f_model, f_spec)]; (*\<rightarrow>Model_Problem*)
18.6
18.7 -"~~~~~ fun Test_Code.init_calc @{context} , args:"; val [(fmz, sp)] = [(f_model, f_spec)];
18.8 +"~~~~~ fun Test_Code.init_calc @{context} , args:"; val (ctxt, [(fmz, sp)])
18.9 + = (@{context}, [(f_model, f_spec)]);
18.10
18.11 (* val ((pt, p), tacis) =*)
18.12 Step_Specify.nxt_specify_init_calc ctxt (fmz, sp);
18.13 "~~~~~ fun nxt_specify_init_calc , args:"; val (fmz, (dI, pI, mI)) = (fmz, sp);
18.14 (*val (_, hdl, (dI, pI, mI), pors, pctxt) = *)
18.15 - Step_Specify.initialise (fmz, (dI, pI, mI));
18.16 + Step_Specify.initialise ctxt(fmz, (dI, pI, mI));
18.17 "~~~~~ fun initialise , args:"; val (fmz, (dI, pI, mI)) = (fmz, sp);
18.18 val thy = ThyC.get_theory dI
18.19 val ctxt = Proof_Context.init_global thy;
19.1 --- a/test/Tools/isac/Specify/refine.sml Sun Oct 23 16:08:27 2022 +0200
19.2 +++ b/test/Tools/isac/Specify/refine.sml Sun Oct 23 17:21:04 2022 +0200
19.3 @@ -528,7 +528,7 @@
19.4
19.5 val ((pt, _), _) = States.get_calc 1;
19.6 val p = States.get_pos 1 1;
19.7 -val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
19.8 +val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
19.9 if UnparseC.term f = "[x = 6 / 5]" then () else error "equation for timing CHANGED"
19.10
19.11 "----------- refine ad-hoc equation for timing: with/out adapt_to_type -------------------------";
20.1 --- a/test/Tools/isac/Specify/step-specify.sml Sun Oct 23 16:08:27 2022 +0200
20.2 +++ b/test/Tools/isac/Specify/step-specify.sml Sun Oct 23 17:21:04 2022 +0200
20.3 @@ -91,7 +91,7 @@
20.4
20.5 val (ptp as (_, p), _) = States.get_calc 1;
20.6
20.7 -val (Form t,_,_) = ME_Misc.pt_extract ptp;
20.8 +val (Form t,_,_) = ME_Misc.pt_extract ctxt ptp;
20.9
20.10 if UnparseC.term t = "c + x + 1 / 3 * x \<up> 3" andalso p = ([], Res) then ()
20.11 else error "mathengine.sml -- fun autoCalculate -- end";
21.1 --- a/test/Tools/isac/Test_Theory.thy Sun Oct 23 16:08:27 2022 +0200
21.2 +++ b/test/Tools/isac/Test_Theory.thy Sun Oct 23 17:21:04 2022 +0200
21.3 @@ -77,107 +77,6 @@
21.4 ML \<open>
21.5 \<close> ML \<open>
21.6 \<close> ML \<open>
21.7 -(* Title: 100-init-rootpbl.sml
21.8 - Author: Walther Neuper 1105
21.9 - (c) copyright due to lincense terms.
21.10 -*)
21.11 -
21.12 -"----------- Minisubplb/100-init-rootpbl.sml ---------------------";
21.13 -"----------- Minisubplb/100-init-rootpbl.sml ---------------------";
21.14 -"----------- Minisubplb/100-init-rootpbl.sml ---------------------";
21.15 -\<close> ML \<open>
21.16 -val (_(*example text*),
21.17 - (model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" ::
21.18 - "Extremum (A = 2 * u * v - u \<up> 2)" ::
21.19 - "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
21.20 - "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
21.21 - "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" ::
21.22 - "FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" ::
21.23 - "Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::
21.24 - "ErrorBound (\<epsilon> = (0::real))" :: []),
21.25 - refs as ("Diff_App",
21.26 - ["univariate_calculus", "Optimisation"],
21.27 - ["Optimisation", "by_univariate_calculus"])))
21.28 - = Store.get (KEStore_Elems.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"]
21.29 -\<close> ML \<open>
21.30 - Test_Code.init_calc @{context} [(model, refs)];
21.31 -\<close> ML \<open>
21.32 -"~~~~~ fun init_calc , args:"; val (ctxt, [(model, refs as (thy_id, _, _))])
21.33 - = (@{context}, [(model, refs)]);
21.34 - val ctxt = thy_id |> ThyC.get_theory_PIDE ctxt |> Proof_Context.init_global
21.35 - val ((pt''', p'''), tacis''') = (* keep for continuation *)
21.36 -
21.37 -Step_Specify.nxt_specify_init_calc ctxt (model, refs);
21.38 -"~~~~~ fun nxt_specify_init_calc , args:"; val (ctxt, (model, (dI, pI, mI))) = (ctxt, (model, refs));
21.39 -
21.40 -Step_Specify.initialise ctxt (model, refs);
21.41 -"~~~~~ fun initialise , args:"; val (ctxt, (fmz, (dI, pI, mI))) = (ctxt, (model, refs));
21.42 - val thy = ThyC.get_theory_PIDE ctxt dI
21.43 - val ctxt = Proof_Context.init_global thy (* ctxt restricted to Formalise *)
21.44 - val (pI, (pors, pctxt), mI) =
21.45 - if mI = ["no_met"]
21.46 - then raise error "else not covered by test"
21.47 - else
21.48 - let
21.49 - val pors = Problem.from_store ctxt pI |> #ppc |> O_Model.init thy fmz; (*..TermC.parseNEW'*)
21.50 - val pctxt = ContextC.initialise' thy fmz; (*..DUPLICATE ermC.parseNEW'*)
21.51 - in (pI, (pors, pctxt), mI) end;
21.52 -
21.53 -(*-------------------- stop step into Step_Specify.nxt_specify_init_calc ---------------------*)
21.54 -"~~~~~ continue fun init_calc , args:"; val ((pt, p), tacis)
21.55 - = ((pt''', p'''), tacis''');
21.56 - val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis;
21.57 -
21.58 - Test_Code.TESTg_form ctxt (pt,p);
21.59 -"~~~~~ fun TESTg_form , args:"; val (ctxt, ptp) = (ctxt, (pt,p));
21.60 - val (form, _, _) = ME_Misc.pt_extract ctxt ptp;
21.61 -val Ctree.ModSpec (_, p_, _, gfr, pre, _) =
21.62 - (*case*) form (*of*);
21.63 -val Pos.Pbl =
21.64 - (*case*) p_ (*of*);
21.65 - Test_Out.Problem [];
21.66 - Test_Out.MethodC [];
21.67 -
21.68 -(*val return =*)
21.69 - Test_Out.PpcKF (Test_Out.Problem [],
21.70 - P_Model.from (Proof_Context.theory_of ctxt) gfr pre);
21.71 -"~~~~~ fun from , args:"; val (thy, itms, pre) = ((Proof_Context.theory_of ctxt), gfr, pre);
21.72 -
21.73 -(*//------------------ inserted hidden code ------------------------------------------------\\*)
21.74 -fun item_from_feedback (_: theory) (I_Model.Cor ((d, ts), _)) = P_Model.Correct (UnparseC.term (Input_Descript.join (d, ts)))
21.75 - | item_from_feedback _ (I_Model.Syn c) = P_Model.SyntaxE c
21.76 - | item_from_feedback _ (I_Model.Typ c) = P_Model.TypeE c
21.77 - | item_from_feedback _ (I_Model.Inc ((d, ts), _)) = P_Model.Incompl (UnparseC.term (Input_Descript.join (d, ts)))
21.78 - | item_from_feedback _ (I_Model.Sup (d, ts)) = P_Model.Superfl (UnparseC.term (Input_Descript.join (d, ts)))
21.79 - | item_from_feedback _ (I_Model.Mis (d, pid)) = P_Model.Missing (UnparseC.term d ^ " " ^ UnparseC.term pid)
21.80 - | item_from_feedback _ _ = raise ERROR "item_from_feedback: uncovered definition"
21.81 -fun add_sel_ppc (_: theory) sel {Given = gi, Where = wh, Find = fi, With = wi, Relate = re} x =
21.82 - case sel of
21.83 - "#Given" => {Given = gi @ [x], Where = wh, Find = fi, With = wi,Relate = re}
21.84 - | "#Where" => {Given = gi, Where = wh @ [x], Find = fi, With = wi, Relate = re}
21.85 - | "#Find" => {Given = gi, Where = wh, Find = fi @ [x], With = wi, Relate = re}
21.86 - | "#Relate"=> {Given = gi, Where = wh, Find = fi, With = wi, Relate = re @ [x]}
21.87 - | "#undef" => {Given = gi @ [x], Where = wh, Find = fi, With = wi, Relate = re} (*ori2itmSup*)
21.88 - | _ => raise ERROR ("add_sel_ppc tried to select by \"" ^ sel ^ "\"")
21.89 -fun add_where {Given = gi, Where = _, Find = fi, With = wi, Relate = re} wh =
21.90 - {Given = gi, Where = wh, Find= fi ,With = wi, Relate = re}
21.91 -fun boolterm2item ctxt (true, term) = P_Model.Correct (UnparseC.term_in_ctxt ctxt term)
21.92 - | boolterm2item ctxt(false, term) = P_Model.False (UnparseC.term_in_ctxt ctxt term);
21.93 -(*\\------------------ inserted hidden code ------------------------------------------------//*)
21.94 -
21.95 - fun coll ppc [] = ppc
21.96 - | coll ppc ((_, _, _, field, itm_)::itms) =
21.97 - coll (add_sel_ppc thy field ppc (item_from_feedback thy itm_)) itms;
21.98 - val gfr = coll P_Model.empty itms;
21.99 -
21.100 -(*val return =*)
21.101 - add_where gfr (map (boolterm2item (Proof_Context.init_global thy)) pre);
21.102 -"~~~~~ fun add_where , args:"; val ({Given = gi, Where = _, Find = fi, With = wi, Relate = re}, wh)
21.103 - = (gfr, (map
21.104 - (boolterm2item ctxt) pre));
21.105 -"~~~~~ fun boolterm2item , args:"; val () = ();
21.106 -(*\\------------------ step into nxt_specify_init_calc -------------------------------------//*)
21.107 -
21.108 \<close> ML \<open>
21.109 \<close> ML \<open>
21.110 \<close> ML \<open>