test/Tools/isac/Interpret/error-pattern.sml
changeset 59983 f1fdb213717b
parent 59982 56654afad89f
child 59988 9a6aa40d1962
     1.1 --- a/test/Tools/isac/Interpret/error-pattern.sml	Thu May 14 16:58:33 2020 +0200
     1.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml	Fri May 15 11:46:43 2020 +0200
     1.3 @@ -480,7 +480,7 @@
     1.4  
     1.5    Compare tests "CAS-command" in test/../inssort.sml etc.
     1.6    ---------------------------------------------------------------------------------------------
     1.7 -show_pt pt;
     1.8 +Test_Tool.show_pt pt;
     1.9  val nxt = (Apply_Method ["Test","squ-equ-test-subpbl1"]);
    1.10  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.11  if p = ([1], Frm) andalso f2str f = "x + 1 = 2" then ()
    1.12 @@ -498,7 +498,7 @@
    1.13  replaceFormula 1 "solve(x+1=2,x)";
    1.14  autoCalculate 1 CompleteCalc;
    1.15  val ((pt,p),_) = get_calc 1;
    1.16 -show_pt pt;
    1.17 +Test_Tool.show_pt pt;
    1.18  if p = ([], Res) then ()
    1.19  else error "inform.sml: diff.behav. CAScmd ([],Pbl) FE-interface";
    1.20  DEconstrCalcTree 1;
    1.21 @@ -516,7 +516,7 @@
    1.22  (*
    1.23  autoCalculate 1 CompleteCalc;
    1.24  val ((pt, p), _) = get_calc 1;
    1.25 -show_pt pt;
    1.26 +Test_Tool.show_pt pt;
    1.27  [
    1.28  (([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
    1.29  (([1], Frm), a * x / (b * x) + c * x / (d * x) + e / f),
    1.30 @@ -531,7 +531,7 @@
    1.31  autoCalculate 1 (Steps 1);
    1.32  autoCalculate 1 (Steps 1);
    1.33  val ((pt, p), _) = get_calc 1;
    1.34 -(*show_pt pt;
    1.35 +(*Test_Tool.show_pt pt;
    1.36  [
    1.37  (([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
    1.38  (([1], Frm), a * x / (b * x) + c * x / (d * x) + e / f),
    1.39 @@ -540,7 +540,7 @@
    1.40  "--- (1) input an arbitrary next formula";
    1.41  appendFormula 1 "((a * d) + (c * b)) / (b * d) + e / f" (*|> Future.join*);
    1.42  val ((pt, p), _) = get_calc 1;
    1.43 -(*show_pt pt;
    1.44 +(*Test_Tool.show_pt pt;
    1.45  [
    1.46  (([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
    1.47  (([1], Frm), a * x / (b * x) + c * x / (d * x) + e / f),
    1.48 @@ -558,7 +558,7 @@
    1.49  (* generate a preview:
    1.50  autoCalculate 1 (Steps 1);
    1.51  val ((pt, p), _) = get_calc 1;
    1.52 -show_pt pt;
    1.53 +Test_Tool.show_pt pt;
    1.54  [
    1.55  (([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
    1.56  (([1], Frm), a * x / (b * x) + c * x / (d * x) + e / f),
    1.57 @@ -571,7 +571,7 @@
    1.58  *)
    1.59  appendFormula 1 "(b * d * e + b * c * f + a * d * f) / (b * d * f)" (*|> Future.join*);
    1.60  val ((pt, p), _) = get_calc 1;
    1.61 -(*show_pt pt;
    1.62 +(*Test_Tool.show_pt pt;
    1.63  [
    1.64  (([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
    1.65  (([1], Frm), a * x / (b * x) + c * x / (d * x) + e / f),
    1.66 @@ -588,7 +588,7 @@
    1.67  "--- (3) input the exact final result";
    1.68  appendFormula 1 "(b * d * e + b * c * f + a * d * f) / (b * d * f)" (*|> Future.join*);
    1.69  val ((pt, p), _) = get_calc 1;
    1.70 -(*show_pt pt;
    1.71 +(*Test_Tool.show_pt pt;
    1.72  [
    1.73  (([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
    1.74  (([1], Frm), a * x / (b * x) + c * x / (d * x) + e / f),
    1.75 @@ -614,7 +614,7 @@
    1.76  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.77                      "[]" (*..found broken in child of 33913fe24685, error covered by  CAS-command *)
    1.78  then () else error "inform [rational,simplification] changed at end";
    1.79 -(*show_pt pt;
    1.80 +(*Test_Tool.show_pt pt;
    1.81  [
    1.82  (([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
    1.83  (([1], Frm), a * x / (b * x) + c * x / (d * x) + e / f),
    1.84 @@ -692,8 +692,8 @@
    1.85  (*WN081028 fixed <ERROR> helpless </ERROR> by inform returning ...(.,Met)*)
    1.86  autoCalculate 1 CompleteCalc;
    1.87  val ((pt,p),_) = get_calc 1;
    1.88 -val Form res = (#1 o pt_extract) (pt, ([],Res));
    1.89 -show_pt pt;
    1.90 +val Form res = (#1 o ME_Misc.pt_extract) (pt, ([],Res));
    1.91 +Test_Tool.show_pt pt;
    1.92  if p = ([], Res) andalso UnparseC.term res = "1 + 2 * x" then ()
    1.93  else error "diff.sml behav.changed for Diff (x^2 + x + 1, x)";
    1.94  DEconstrCalcTree 1;
    1.95 @@ -734,7 +734,7 @@
    1.96  (*7>*)fetchProposedTactic 1 (*--> Apply_Method*);
    1.97  autoCalculate 1 (Steps 1);
    1.98  val ((pt,p),_) = get_calc 1;
    1.99 -val Form res = (#1 o pt_extract) (pt, p);
   1.100 +val Form res = (#1 o ME_Misc.pt_extract) (pt, p);
   1.101  if UnparseC.term res = "d_d x (x ^^^ 2 + x + 1)" then ()
   1.102  else error "diff.sml Diff (x^2 + x + 1, x) from exp";
   1.103  DEconstrCalcTree 1;
   1.104 @@ -1165,7 +1165,7 @@
   1.105    instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)
   1.106    val ((pt,pos), _) = get_calc 1;
   1.107    val p = get_pos 1 1;
   1.108 -  val (Form f, _, asms) = pt_extract (pt, p);
   1.109 +  val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
   1.110  
   1.111    if p = ([1], Res) andalso UnparseC.term f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" then
   1.112      case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"], 
   1.113 @@ -1181,7 +1181,7 @@
   1.114    val ((pt,pos),_) = get_calc 1;
   1.115    val p = get_pos 1 1;
   1.116  
   1.117 -  val (Form f, _, asms) = pt_extract (pt, p);
   1.118 +  val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
   1.119    if p = ([1], Res) andalso UnparseC.term f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" then
   1.120      case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"], 
   1.121        ("diff_sum", thm)) =>
   1.122 @@ -1194,7 +1194,7 @@
   1.123    (*<AUTOCALC> ([1], Res) ([2], Res) ([2], Res) </AUTOCALC>*)
   1.124    val ((pt,pos),_) = get_calc 1;
   1.125    val p = get_pos 1 1;
   1.126 -  val (Form f, _, asms) = pt_extract (pt, p);
   1.127 +  val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
   1.128    if p = ([1], Res) andalso existpt [2] pt
   1.129      andalso UnparseC.term f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"
   1.130    then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"], 
   1.131 @@ -1233,7 +1233,7 @@
   1.132  "~~~~~ final check:";
   1.133  val ((pt, _),_) = get_calc 1;
   1.134  val p = get_pos 1 1;
   1.135 -val (Form f, _, asms) = pt_extract (pt, p);
   1.136 +val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
   1.137    if p = ([2], Res) andalso UnparseC.term f = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)"
   1.138    then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"], 
   1.139        ("diff_sin_chain", thm)) =>
   1.140 @@ -1250,8 +1250,8 @@
   1.141     ...vvv
   1.142     *)
   1.143  (* val (dI, oris, ppc, pbt, (selct::ss))=
   1.144 -       (#1 (some_spec ospec spec), oris, []:I_Model.T,
   1.145 -	((#ppc o Problem.from_store) (#2 (some_spec ospec spec))),(imodel2fstr imodel));
   1.146 +       (#1 (References.select ospec spec), oris, []:I_Model.T,
   1.147 +	((#ppc o Problem.from_store) (#2 (References.select ospec spec))),(imodel2fstr imodel));
   1.148     val iii = appl_adds dI oris ppc pbt (selct::ss); 
   1.149     tracing(I_Model.to_string thy iii);
   1.150