1.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml Tue May 19 12:33:35 2020 +0200
1.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Wed May 20 12:52:09 2020 +0200
1.3 @@ -39,7 +39,7 @@
1.4 " _________________ rewrite _________________ ";
1.5 val thy' = "Test";
1.6 val ct = "sqrt(9+4*x)=sqrt x + sqrt(-3+x)";
1.7 -val thm = ("square_equation_left","");
1.8 +val thm = ("square_equation_left", "");
1.9 val SOME (ct,asm) = rewrite thy' "tless_true" "tval_rls" true thm ct;
1.10 (*"9 + 4 * x = (sqrt x + sqrt (-3 + x)) ^^^ 2"*)
1.11 val rls = ("Test_simplify");
1.12 @@ -55,7 +55,7 @@
1.13 val rls = ("Test_simplify");
1.14 val (ct,_) = the (rewrite_set thy' false rls ct);
1.15 (*"sqrt (x ^^^ 2 + -3 * x) = 6 + x"*)
1.16 -val thm = ("square_equation_left","");
1.17 +val thm = ("square_equation_left", "");
1.18 val (ct,asm') = the (rewrite thy' "tless_true" "tval_rls" true thm ct);
1.19 val asm = asm union asm';
1.20 (*"x ^^^ 2 + -3 * x = (6 + x) ^^^ 2"*)
1.21 @@ -70,7 +70,7 @@
1.22 (*"-36 + -15 * x = 0"*)
1.23 val rls = ("isolate_bdv");
1.24 val (ct,_) = the (rewrite_set_inst thy' false
1.25 - [("bdv","x::real")] rls ct);
1.26 + [("bdv", "x::real")] rls ct);
1.27 (*"x = (0 + -1 * -36) // -15"*)
1.28 val rls = ("Test_simplify");
1.29 val (ct,_) = the (rewrite_set thy' false rls ct);
1.30 @@ -80,8 +80,8 @@
1.31 val ct = "x = (-12) / 5" : TermC.as_string
1.32 > asm;
1.33 val it =
1.34 - ["(+0) <= sqrt x + sqrt ((-3) + x) ","(+0) <= 9 + 4 * x",
1.35 - "(+0) <= (-3) * x + x ^^^ 2","(+0) <= 6 + x"] : TermC.as_string list
1.36 + ["(+0) <= sqrt x + sqrt ((-3) + x) ", "(+0) <= 9 + 4 * x",
1.37 + "(+0) <= (-3) * x + x ^^^ 2", "(+0) <= 6 + x"] : TermC.as_string list
1.38 *)
1.39
1.40
1.41 @@ -97,7 +97,7 @@
1.42 " -------------- model, specify ------------ ";
1.43 " --- subproblem 1: linear-equation --- ";
1.44 val origin = ["equation (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
1.45 - "bound_variable x","error_bound 0"(*,
1.46 + "bound_variable x", "error_bound 0"(*,
1.47 "solutions L::real set" ,
1.48 "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < eps}"*)];
1.49 val thy = (theory "Isac_Knowledge");
1.50 @@ -117,12 +117,12 @@
1.51 parseold thy "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < apx}";
1.52
1.53 " --- subproblem 2: linear-equation --- ";
1.54 -val origin = ["x + 4 = (0::real)","x::real"];
1.55 +val origin = ["x + 4 = (0::real)", "x::real"];
1.56 val formals = map (the o (parse thy)) origin;
1.57
1.58 val given = ["equation (l=(0::real))",
1.59 "bound_variable bdv"];
1.60 -val where_ = ["l is_linear_in bdv","bdv is_const"];
1.61 +val where_ = ["l is_linear_in bdv", "bdv is_const"];
1.62 val find = ["l::real"];
1.63 val with_ = ["l = (%x. l) bdv"];
1.64 val chkpbl = map (the o (parseold thy)) (given @ where_ @ find @ with_);
1.65 @@ -205,7 +205,7 @@
1.66 *)
1.67 val thy' = "Test";
1.68 val ct = "sqrt(9+4*x)=sqrt x + sqrt(5+x)";
1.69 -(*1*)val thm = ("square_equation_left","");
1.70 +(*1*)val thm = ("square_equation_left", "");
1.71 val (ct,asm) = the (rewrite thy' "tless_true" "tval_rls" true thm ct);
1.72 "9 + 4 * x = (sqrt x + sqrt (5 + x)) ^^^ 2";
1.73 (*2*)val rls = "Test_simplify";
1.74 @@ -220,7 +220,7 @@
1.75 (*5*)val rls = "Test_simplify";
1.76 val (ct,_) = the (rewrite_set thy' false rls ct);
1.77 "sqrt (x ^^^ 2 + 5 * x) = 2 + x";
1.78 -(*6*)val thm = ("square_equation_left","");
1.79 +(*6*)val thm = ("square_equation_left", "");
1.80 val (ct,asm') = the (rewrite thy' "tless_true" "tval_rls" true thm ct);
1.81 val asm = asm union asm';
1.82 "x ^^^ 2 + 5 * x = (2 + x) ^^^ 2";
1.83 @@ -235,7 +235,7 @@
1.84 "-4 + x = 0";
1.85 (*10*)val rls = "isolate_bdv";
1.86 val (ct,_) = the (rewrite_set_inst thy' false
1.87 - [("bdv","x")] rls ct);
1.88 + [("bdv", "x")] rls ct);
1.89 "x = 0 + -1 * -4";
1.90 (*11*)val rls = "Test_simplify";
1.91 val (ct,_) = the (rewrite_set thy' false rls ct);
1.92 @@ -249,10 +249,10 @@
1.93 " _________________ rewrite + cappend _________________ ";
1.94 val thy' = "Test";
1.95 val ct = str2term"sqrt(9+4*x)=sqrt x + sqrt(5+x)";
1.96 -val ctl = ["sqrt(9+4*x)=sqrt x + sqrt(5+x)","x::real","0"];
1.97 +val ctl = ["sqrt(9+4*x)=sqrt x + sqrt(5+x)", "x::real", "0"];
1.98 val oris = O_Model.init ctl thy
1.99 ((#ppc o Problem.from_store)
1.100 - ["sqroot-test","univariate","equation","test"]);
1.101 + ["sqroot-test", "univariate", "equation", "test"]);
1.102 val loc = Istate.empty;
1.103 val (pt,pos) = (e_ctree,[]);
1.104 val (pt,_) = cappend_problem pt pos loc Formalise.empty (oris,empty_spec,TermC.empty, ContextC.empty)
1.105 @@ -263,25 +263,25 @@
1.106 (*val pt = update_model pt [] (fst (get_obj g_origin pt [])); *)
1.107 val pt = update_domID pt [] "Test";
1.108 val pt = update_pblID pt [] ["Test",
1.109 - "equations","univariate","square-root"];
1.110 -val pt = update_metID pt [] ["Test","sqrt-equ-test"];
1.111 + "equations", "univariate", "square-root"];
1.112 +val pt = update_metID pt [] ["Test", "sqrt-equ-test"];
1.113 val pt = update_pbl pt [] [];
1.114 val pt = update_met pt [] [];
1.115 (*
1.116 > get_obj g_spec pt [];
1.117 -val it = ("empty_thy_id",["empty_probl_id"],("empty_thy_id","empty_meth_id")) : spec
1.118 +val it = ("empty_thy_id",["empty_probl_id"],("empty_thy_id", "empty_meth_id")) : spec
1.119 > val pt = update_domID pt [] "RatArith";
1.120 > get_obj g_spec pt [];
1.121 -val it = ("RatArith",["empty_probl_id"],("empty_thy_id","empty_meth_id")) : spec
1.122 +val it = ("RatArith",["empty_probl_id"],("empty_thy_id", "empty_meth_id")) : spec
1.123 > val pt = update_pblID pt [] ["RatArith",
1.124 - "equations","univariate","square-root"];
1.125 + "equations", "univariate", "square-root"];
1.126 > get_obj g_spec pt [];
1.127 -("RatArith",["RatArith","equations","univariate","square-root"],
1.128 - ("empty_thy_id","empty_meth_id")) : spec
1.129 -> val pt = update_metID pt [] ("RatArith","sqrt-equ-test");
1.130 +("RatArith",["RatArith", "equations", "univariate", "square-root"],
1.131 + ("empty_thy_id", "empty_meth_id")) : spec
1.132 +> val pt = update_metID pt [] ("RatArith", "sqrt-equ-test");
1.133 > get_obj g_spec pt [];
1.134 - ("RatArith",["RatArith","equations","univariate","square-root"],
1.135 - ("RatArith","sqrt-equ-test")) : spec
1.136 + ("RatArith",["RatArith", "equations", "univariate", "square-root"],
1.137 + ("RatArith", "sqrt-equ-test")) : spec
1.138 *)
1.139
1.140
1.141 @@ -289,7 +289,7 @@
1.142 val (pt,_) = cappend_parent pt pos loc ct (Tac "repeat") TransitiveB;
1.143
1.144 val pos = (lev_on o lev_dn) pos;
1.145 -val thm = ("square_equation_left",""); val ctold = ct;
1.146 +val thm = ("square_equation_left", ""); val ctold = ct;
1.147 val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") true thm (UnparseC.term ct));
1.148 val (pt,_) = cappend_atomic pt pos loc ctold (Tac (fst thm)) (str2term ct,[])Complete;
1.149 (*val pt = union_asm pt [] (map (rpair []) asm);*)
1.150 @@ -315,7 +315,7 @@
1.151 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;
1.152
1.153 val pos = lev_on pos;
1.154 -val thm = ("square_equation_left",""); val ctold = str2term ct;
1.155 +val thm = ("square_equation_left", ""); val ctold = str2term ct;
1.156 val (ct,asm) = the (rewrite thy' "tless_true" "tval_rls" true thm ct);
1.157 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;
1.158 (*val pt = union_asm pt [] (map (rpair []) asm);*)
1.159 @@ -339,13 +339,13 @@
1.160 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;
1.161
1.162 (* --- see comments in interface_ME_ISA/instantiate''
1.163 -val rlsdat' = instantiate_rls' thy' [("bdv","x")] ("isolate_bdv");
1.164 +val rlsdat' = instantiate_rls' thy' [("bdv", "x")] ("isolate_bdv");
1.165 val (ct,_) = the (rewrite_set thy' false
1.166 ("#isolate_bdv",rlsdat') ct); *)
1.167 val pos = lev_on pos;
1.168 val rls = ("isolate_bdv"); val ctold = str2term ct;
1.169 val (ct,_) = the (rewrite_set_inst thy' false
1.170 - [("bdv","x")] rls ct);
1.171 + [("bdv", "x")] rls ct);
1.172 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;
1.173
1.174 val pos = lev_on pos;
1.175 @@ -386,12 +386,12 @@
1.176 " _________________ me Free_Solve _________________ ";
1.177 " _________________ me Free_Solve _________________ ";
1.178 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
1.179 - "solveFor x","errorBound (eps=0)",
1.180 + "solveFor x", "errorBound (eps=0)",
1.181 "solutions L"(*,
1.182 "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < eps}"*)];
1.183 val (dI',pI',mI') =
1.184 - ("Test",["sqroot-test","univariate","equation","test"],
1.185 - ("Test","sqrt-equ-test"));
1.186 + ("Test",["sqroot-test", "univariate", "equation", "test"],
1.187 + ("Test", "sqrt-equ-test"));
1.188 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.189 (*val nxt = ("Add_Given", Add_Given "equation (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x) )");*)
1.190 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.191 @@ -403,13 +403,13 @@
1.192 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.193 (* val nxt = ("Specify_Theory",Specify_Theory "DiffAppl");
1.194 > get_obj g_spec pt (fst p);
1.195 -val it = ("empty_thy_id",["empty_probl_id"],("empty_thy_id","empty_meth_id")) : spec*)
1.196 +val it = ("empty_thy_id",["empty_probl_id"],("empty_thy_id", "empty_meth_id")) : spec*)
1.197 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.198 (*val nxt = ("Specify_Problem", Specify_Problem *)
1.199 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.200 -(*val nxt = ("Specify_Method",Specify_Method ("DiffAppl","sqrt-equ-test"));*)
1.201 +(*val nxt = ("Specify_Method",Specify_Method ("DiffAppl", "sqrt-equ-test"));*)
1.202 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.203 -(*val nxt = ("Apply_Method",Apply_Method ("DiffAppl","sqrt-equ-test"));*)
1.204 +(*val nxt = ("Apply_Method",Apply_Method ("DiffAppl", "sqrt-equ-test"));*)
1.205 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.206 val nxt = ("Free_Solve",Free_Solve);
1.207 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.208 @@ -426,9 +426,9 @@
1.209 me ("Begin_Trans",Begin_Trans) p [4] pt; *)
1.210
1.211 "--- 1 ---";
1.212 -get_form ("Rewrite_Asm",Rewrite_Asm ("square_equation_left","")) p pt;
1.213 +get_form ("Rewrite_Asm",Rewrite_Asm ("square_equation_left", "")) p pt;
1.214 val (p,_,f,nxt,_,pt)=
1.215 -me ("Rewrite_Asm",Rewrite_Asm ("square_equation_left","")) p [5] pt;
1.216 +me ("Rewrite_Asm",Rewrite_Asm ("square_equation_left", "")) p [5] pt;
1.217 "--- 2 ---";
1.218 get_form ("Rewrite_Set",Rewrite_Set "Test_simplify")p pt;
1.219 val (p,_,f,nxt,_,pt)=
1.220 @@ -446,9 +446,9 @@
1.221 val (p,_,f,nxt,_,pt)=
1.222 me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [9] pt;
1.223 "--- 6 ---";
1.224 -get_form ("Rewrite_Asm",Rewrite_Asm ("square_equation_left","")) p pt;
1.225 +get_form ("Rewrite_Asm",Rewrite_Asm ("square_equation_left", "")) p pt;
1.226 val (p,_,f,nxt,_,pt)=
1.227 -me ("Rewrite_Asm",Rewrite_Asm ("square_equation_left","")) p [10] pt;
1.228 +me ("Rewrite_Asm",Rewrite_Asm ("square_equation_left", "")) p [10] pt;
1.229 (* 15.4.
1.230 "--- ---";
1.231 get_form ("End_Trans",End_Trans) p pt;
1.232 @@ -475,9 +475,9 @@
1.233 val ((p,p_),_,f,nxt,_,pt)=
1.234 me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [16] pt;
1.235 (* 5.4.00.: ---
1.236 -get_form ("Check_Postcond",Check_Postcond ("Test","solve-root-equation")) (p,Met) pt;
1.237 +get_form ("Check_Postcond",Check_Postcond ("Test", "solve-root-equation")) (p,Met) pt;
1.238 val (p,_,f,nxt,_,pt)=
1.239 -me ("Check_Postcond",Check_Postcond ("Test","solve-root-equation")) (p,Met) [17] pt;
1.240 +me ("Check_Postcond",Check_Postcond ("Test", "solve-root-equation")) (p,Met) [17] pt;
1.241 --- *)
1.242 writeln (pr_ctree pr_short pt);
1.243 writeln("result: "^(get_obj g_result pt [])^"\n==================================================================="*;
1.244 @@ -488,16 +488,16 @@
1.245 " _________________ me + tacs input _________________ ";
1.246 " _________________ me + tacs input _________________ ";
1.247 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
1.248 - "solveFor x","errorBound (eps=0)",
1.249 + "solveFor x", "errorBound (eps=0)",
1.250 "solutions L"];
1.251 val (dI',pI',mI') =
1.252 - ("Test",["sqroot-test","univariate","equation","test"],
1.253 - ["Test","sqrt-equ-test"]);
1.254 + ("Test",["sqroot-test", "univariate", "equation", "test"],
1.255 + ["Test", "sqrt-equ-test"]);
1.256 "--- s1 ---";
1.257 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.258 "--- s1b ---";
1.259 val nxt = ("Model_Problem",
1.260 - Model_Problem(*["sqroot-test","univariate","equation","test"]*));
1.261 + Model_Problem(*["sqroot-test", "univariate", "equation", "test"]*));
1.262 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.263 "--- s2 ---";
1.264 val nxt = ("Add_Given",
1.265 @@ -517,16 +517,16 @@
1.266 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.267 "--- s7 ---";
1.268 val nxt = ("Specify_Problem",
1.269 -Specify_Problem ["sqroot-test","univariate","equation","test"]);
1.270 +Specify_Problem ["sqroot-test", "univariate", "equation", "test"]);
1.271 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.272 "--- s8 ---";
1.273 -val nxt = ("Specify_Method",Specify_Method ["Test","sqrt-equ-test"]);
1.274 +val nxt = ("Specify_Method",Specify_Method ["Test", "sqrt-equ-test"]);
1.275 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.276 "--- s9 ---";
1.277 -val nxt = ("Apply_Method",Apply_Method ["Test","sqrt-equ-test"]);
1.278 +val nxt = ("Apply_Method",Apply_Method ["Test", "sqrt-equ-test"]);
1.279 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.280 "--- 1 ---";
1.281 -val nxt = ("Rewrite",Rewrite ("square_equation_left",""));
1.282 +val nxt = ("Rewrite",Rewrite ("square_equation_left", ""));
1.283 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.284
1.285 (*.9.6.03
1.286 @@ -585,7 +585,7 @@
1.287 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
1.288 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.289 "--- 6 ---";
1.290 -val nxt = ("Rewrite",Rewrite ("square_equation_left",""));
1.291 +val nxt = ("Rewrite",Rewrite ("square_equation_left", ""));
1.292 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.293 "--- 7 ---";
1.294 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
1.295 @@ -609,7 +609,7 @@
1.296 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
1.297 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.298 "--- 1<> ---";
1.299 -val nxt = ("Check_Postcond",Check_Postcond ["sqroot-test","univariate","equation","test"]);
1.300 +val nxt = ("Check_Postcond",Check_Postcond ["sqroot-test", "univariate", "equation", "test"]);
1.301 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.302 (* val nxt = ("End_Proof'",End_Proof');*)
1.303 if f <> (Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 4]")))