1.1 --- a/test/Tools/isac/Knowledge/diff.sml Tue May 19 12:33:35 2020 +0200
1.2 +++ b/test/Tools/isac/Knowledge/diff.sml Wed May 20 12:52:09 2020 +0200
1.3 @@ -39,11 +39,11 @@
1.4 val chkpbt = ((map (the o (parse thy))) o P_Model.to_list) pbt;
1.5
1.6 val org = ["functionTerm (d_d x (x ^^^ 2 + 3 * x + 4))",
1.7 - "differentiateFor x","derivative f_f'"];
1.8 + "differentiateFor x", "derivative f_f'"];
1.9 val chkorg = map (the o (parse thy)) org;
1.10
1.11 -Problem.from_store ["derivative_of","function"];
1.12 -Method.from_store ["diff","differentiate_on_R"];
1.13 +Problem.from_store ["derivative_of", "function"];
1.14 +Method.from_store ["diff", "differentiate_on_R"];
1.15
1.16 "----------- for correction of diff_const ---------------";
1.17 "----------- for correction of diff_const ---------------";
1.18 @@ -111,10 +111,10 @@
1.19 "----------- differentiate: me (*+ tacs input*) ---------";
1.20 "----------- differentiate: me (*+ tacs input*) ---------";
1.21 val fmz = ["functionTerm (x ^^^ 2 + 3 * x + 4)",
1.22 - "differentiateFor x","derivative f_f'"];
1.23 + "differentiateFor x", "derivative f_f'"];
1.24 val (dI',pI',mI') =
1.25 - ("Diff",["derivative_of","function"],
1.26 - ["diff","diff_simpl"]);
1.27 + ("Diff",["derivative_of", "function"],
1.28 + ["diff", "diff_simpl"]);
1.29 val p = e_pos'; val c = [];
1.30 "--- s1 ---";
1.31 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.32 @@ -142,10 +142,10 @@
1.33 (*val nxt = ("Apply_Method",Apply_Method mI');*)
1.34 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.35 "--- 1 ---";
1.36 -(*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(''bdv'',x)"],("diff_sum","")));*)
1.37 +(*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(''bdv'',x)"],("diff_sum", "")));*)
1.38 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.39 "--- 2 ---";
1.40 -(*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(''bdv'',x)"],("diff_sum","")));*)
1.41 +(*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(''bdv'',x)"],("diff_sum", "")));*)
1.42 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.43 (*val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.44 val (p,_,f,nxt,_,pt) = me nxt p c pt;*)
1.45 @@ -154,7 +154,7 @@
1.46 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.47 (*val (p,_,f,nxt,_,pt) = me nxt p c pt;*)
1.48 "--- 4 ---";
1.49 -(*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(''bdv'',x)"],("diff_pow","")));*)
1.50 +(*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(''bdv'',x)"],("diff_pow", "")));*)
1.51 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.52 (*val (p,_,f,nxt,_,pt) = me nxt p c pt;*)
1.53 "--- 5 ---";
1.54 @@ -162,7 +162,7 @@
1.55 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.56 (*val (p,_,f,nxt,_,pt) = me nxt p c pt;*)
1.57 "--- 6 ---";
1.58 -(*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(''bdv'',x)"],("diff_var","")));*)
1.59 +(*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(''bdv'',x)"],("diff_var", "")));*)
1.60 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.61 if f2str f = "2 * x ^^^ (2 - 1) + 3 * 1 + 0" then ()
1.62 else error "diff.sml: diff.behav. in d_d x ^^^ 2 + 3 * x + 4";
1.63 @@ -170,7 +170,7 @@
1.64 (*val nxt = ("Rewrite_Set",Rewrite_Set "make_polynomial");*)
1.65 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.66 "--- 8 ---";
1.67 -(*val nxt = ("Check_Postcond",Check_Postcond ("Diff","differentiate_on_R"));*)
1.68 +(*val nxt = ("Check_Postcond",Check_Postcond ("Diff", "differentiate_on_R"));*)
1.69 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.70 "--- 9 ---";
1.71 (*val nxt = ("End_Proof'",End_Proof');*)
1.72 @@ -186,10 +186,10 @@
1.73 "----------- 1.5.02 me from script ----------------------";
1.74 (*exp_Diff_No-1.xml*)
1.75 val fmz = ["functionTerm (x ^^^ 2 + 3 * x + 4)",
1.76 - "differentiateFor x","derivative f_f'"];
1.77 + "differentiateFor x", "derivative f_f'"];
1.78 val (dI',pI',mI') =
1.79 - ("Diff",["derivative_of","function"],
1.80 - ["diff","diff_simpl"]);
1.81 + ("Diff",["derivative_of", "function"],
1.82 + ["diff", "diff_simpl"]);
1.83 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.84 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.85 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.86 @@ -198,7 +198,7 @@
1.87 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.88 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.89 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.90 -(*nxt = ("Apply_Method",Apply_Method ("Diff","differentiate_on_R*)
1.91 +(*nxt = ("Apply_Method",Apply_Method ("Diff", "differentiate_on_R*)
1.92 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.93
1.94 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.95 @@ -303,8 +303,8 @@
1.96 [(["functionTerm (x^2 + x+ 1/x + 2/x^2)",
1.97 (*"functionTerm ((x^3)^5)",*)
1.98 "differentiateFor x", "derivative f_f'"],
1.99 - ("Isac_Knowledge", ["derivative_of","function"],
1.100 - ["diff","differentiate_on_R"]))];
1.101 + ("Isac_Knowledge", ["derivative_of", "function"],
1.102 + ["diff", "differentiate_on_R"]))];
1.103 Iterator 1;
1.104 moveActiveRoot 1;
1.105 autoCalculate 1 CompleteCalc;
1.106 @@ -318,8 +318,8 @@
1.107 CalcTree
1.108 [(["functionTerm (x^3 * x^5)",
1.109 "differentiateFor x", "derivative f_f'"],
1.110 - ("Isac_Knowledge", ["derivative_of","function"],
1.111 - ["diff","differentiate_on_R"]))];
1.112 + ("Isac_Knowledge", ["derivative_of", "function"],
1.113 + ["diff", "differentiate_on_R"]))];
1.114 Iterator 1;
1.115 moveActiveRoot 1;
1.116 autoCalculate 1 CompleteCalc;
1.117 @@ -339,8 +339,8 @@
1.118 CalcTree
1.119 [(["functionTerm (x^3 * x^5)",
1.120 "differentiateFor x", "derivative f_f'"],
1.121 - ("Isac_Knowledge", ["derivative_of","function"],
1.122 - ["diff","after_simplification"]))];
1.123 + ("Isac_Knowledge", ["derivative_of", "function"],
1.124 + ["diff", "after_simplification"]))];
1.125 Iterator 1;
1.126 moveActiveRoot 1;
1.127 (* Rewrite.trace_on := true;
1.128 @@ -359,8 +359,8 @@
1.129 CalcTree
1.130 [(["functionTerm ((x^3)^5)",
1.131 "differentiateFor x", "derivative f_f'"],
1.132 - ("Isac_Knowledge", ["derivative_of","function"],
1.133 - ["diff","after_simplification"]))];
1.134 + ("Isac_Knowledge", ["derivative_of", "function"],
1.135 + ["diff", "after_simplification"]))];
1.136 Iterator 1;
1.137 moveActiveRoot 1;
1.138 autoCalculate 1 CompleteCalc;
1.139 @@ -374,8 +374,8 @@
1.140 reset_states ();
1.141 CalcTree
1.142 [(["functionEq (A = s * (a - (s::real)))", "differentiateFor s", "derivativeEq f_f'"],
1.143 - ("Isac_Knowledge", ["named","derivative_of","function"],
1.144 - ["diff","differentiate_equality"]))];
1.145 + ("Isac_Knowledge", ["named", "derivative_of", "function"],
1.146 + ["diff", "differentiate_equality"]))];
1.147 Iterator 1;
1.148 moveActiveRoot 1;
1.149 autoCalculate 1 CompleteCalc;
1.150 @@ -401,8 +401,8 @@
1.151 CalcTree
1.152 [(["functionTerm (x^2 + x + 1)",
1.153 "differentiateFor x", "derivative f_f'"],
1.154 - ("Isac_Knowledge", ["derivative_of","function"],
1.155 - ["diff","differentiate_on_R"]))];
1.156 + ("Isac_Knowledge", ["derivative_of", "function"],
1.157 + ["diff", "differentiate_on_R"]))];
1.158 Iterator 1;
1.159 moveActiveRoot 1;
1.160 autoCalculate 1 CompleteCalcHead;