1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/test/Tools/isac/OLDTESTS/script.sml Thu Aug 12 11:02:32 2010 +0200
1.3 @@ -0,0 +1,345 @@
1.4 +(* tests for ME/script.sml
1.5 + WN.13.3.00
1.6 +
1.7 + WN050908 OLD FILE, MERGE WITH smltest/ME/script.sml
1.8 +
1.9 +use"systest/script.sml";
1.10 +use"script.sml";
1.11 +*)
1.12 +
1.13 +
1.14 +" scripts: Variante 'funktional' ";
1.15 +"############## Make_fun_by_new_variable ##############";
1.16 +"############## Make_fun_by_explicit ##############";
1.17 +"################ Solve_root_equation #################";
1.18 +"------- Notlocatable: Free_Solve -------";
1.19 +
1.20 +" --- test100: nxt_tac order------------------------------------ ";
1.21 +" --- test100: order 1 3 1 2 ----------------------------------- ";
1.22 +" --- test200: nxt_tac order ------------------------------------- ";
1.23 +" --- test200: order 3 1 1 2 --------------------------------- ";
1.24 +
1.25 +" --- root-equation: nxt_tac order------------------------------ ";
1.26 +" --- root-equation: 1.norm_equation ------------------------------ ";
1.27 +(* --- test200: calculate -----------------------------------------*)
1.28 +" --- check_elementwise ------------------------------ ";
1.29 +
1.30 +" --- test 30.4.02 Testterm: Repeat Repeat Or ------------------ ";
1.31 +" --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ ";
1.32 +
1.33 +"--------- sel_rules ---------------------------------------------";
1.34 +"-----------------------------------------------------------------";
1.35 +
1.36 +
1.37 +
1.38 +
1.39 +
1.40 +" ################################################# 6.5.03";
1.41 +" scripts: Variante 'funktional' 6.5.03";
1.42 +" ################################################# 6.5.03 ";
1.43 +
1.44 +val c = (the o (parse DiffApp.thy))
1.45 + "Script Maximum_value(fix_::bool list)(m_::real) (rs_::bool list)\
1.46 + \ (v_::real) (itv_::real set) (err_::bool) = \
1.47 + \ (let e_ = (hd o (filterVar m_)) rs_; \
1.48 + \ t_ = (if 1 < length_ rs_ \
1.49 + \ then (SubProblem (Reals_,[make,function],[no_met])\
1.50 + \ [real_ m_, real_ v_, bool_list_ rs_])\
1.51 + \ else (hd rs_)); \
1.52 + \ (mx_::real) = SubProblem (Reals_,[on_interval,max_of,function], \
1.53 + \ [Isac,maximum_on_interval])\
1.54 + \ [bool_ t_, real_ v_, real_set_ itv_]\
1.55 + \ in ((SubProblem (Reals_,[find_values,tool],[Isac,find_values]) \
1.56 + \ [real_ mx_, real_ (Rhs t_), real_ v_, real_ m_, \
1.57 + \ bool_list_ (dropWhile (ident e_) rs_)])::bool list))";
1.58 +
1.59 +
1.60 +"################################################### 6.5.03";
1.61 +"############## Make_fun_by_new_variable ########### 6.5.03";
1.62 +"################################################### 6.5.03";
1.63 +
1.64 +val sc = (the o (parse DiffApp.thy)) (*start interpretieren*)
1.65 + "Script Make_fun_by_new_variable (f_::real) (v_::real) \
1.66 + \ (eqs_::bool list) = \
1.67 + \(let h_ = (hd o (filterVar f_)) eqs_; \
1.68 + \ es_ = dropWhile (ident h_) eqs_; \
1.69 + \ vs_ = dropWhile (ident f_) (Vars h_); \
1.70 + \ v_1 = nth_ 1 vs_; \
1.71 + \ v_2 = nth_ 2 vs_; \
1.72 + \ e_1 = (hd o (filterVar v_1)) es_; \
1.73 + \ e_2 = (hd o (filterVar v_2)) es_; \
1.74 + \ (s_1::bool list) = (SubProblem (Reals_,[univar,equation],[no_met])\
1.75 + \ [bool_ e_1, real_ v_1]);\
1.76 + \ (s_2::bool list) = (SubProblem (Reals_,[univar,equation],[no_met])\
1.77 + \ [bool_ e_2, real_ v_2])\
1.78 + \in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_)";
1.79 +
1.80 +val ags = map (term_of o the o (parse DiffApp.thy))
1.81 + ["A::real", "alpha::real",
1.82 + "[A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]"];
1.83 +val ll = [](*:loc_*);
1.84 +(* problem with exn PTREE + eval_to -------------------------
1.85 +"-------------- subproblem with empty formalizaton -------";
1.86 +val (mI1,m1) =
1.87 + ("Subproblem", tac2tac_ pt p
1.88 + (Subproblem (("Reals",["univar","equation","test"],
1.89 + (""(*"ANDERN !!!!!!!*),"no_met")),[])));
1.90 +val (mI2,m2) = (mI1,m1);
1.91 +val (mI3,m3) =
1.92 + ("Substitute", tac2tac_ pt p
1.93 + (Substitute [("a","#2*r*sin alpha"),("b","#2*r*cos alpha")]));
1.94 +"------- same_tacpbl + eval_to -------";
1.95 +val Some(l1,t1) = same_tacpbl sc ll (mI1,m1);
1.96 +loc_2str l1;
1.97 +(*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, L, R]"*)
1.98 +Sign.string_of_term (sign_of DiffApp.thy) t1;
1.99 +(*"solve_univar (Reals, [univar, equation], no_met) B.1 B.3 "?6 ?4 *)
1.100 +
1.101 +val Some(l2,t2) = same_tacpbl sc l1 (mI2,m2);
1.102 +loc_2str l2;
1.103 +(*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D, L, R]"*)
1.104 +Sign.string_of_term (sign_of DiffApp.thy) t2;
1.105 +(*"solve_univar (Reals, [univar, equation], no_met) B.1 B.3 "?7 ?3 *)
1.106 +
1.107 +val Some(l3,t3) = same_tacpbl sc l2 (mI3,m3);
1.108 +loc_2str l3;
1.109 +(*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D]"*)
1.110 +Sign.string_of_term (sign_of DiffApp.thy) t3;
1.111 +(*"Substitute [(v_1, (Rhs o hd) B.1), (v_2, (Rhs o hd) B.0)] B.8"*)
1.112 +
1.113 +
1.114 +"------- eq_tacIDs + eq_consts + eval_args -------";
1.115 +val eq_ids = eq_tacIDs (*start-loc_*)[] sc (mI,m) [];
1.116 +val eq_cons = filter (eq_consts m) eq_ids;
1.117 +val Ready (l,(_,m)::_,_) = eval_args sc (mI,m) [(1,ags)] eq_cons;
1.118 +"------- locate -------";
1.119 +
1.120 +
1.121 +"-------------- subproblem with formalizaton -------";
1.122 +val (mI,m) =
1.123 + ("Subproblem", tac2tac_ pt []
1.124 + (Subproblem (("Reals",["univar","equation","test"],
1.125 + (""(*"ANDERN !!!!!!!*),"no_met")),
1.126 + ["a//#2=r*sin alpha","a"])));
1.127 +"------- same_tacpbl + eval_to -------";
1.128 +
1.129 +
1.130 +"------- eq_tacIDs + eq_consts + eval_args -------";
1.131 +val eq_ids = eq_tacIDs [] sc (mI,m) [];
1.132 +val eq_cons = filter (eq_consts m) eq_ids;
1.133 +val Ready (l,(_,m)::_,_) = eval_args sc (mI,m) [(1,ags)] eq_cons;
1.134 +
1.135 +
1.136 +"------- locate -------";
1.137 +-------------------------------------------------------*)
1.138 +(* use"ME/script.sml";
1.139 + use"test-script.sml";
1.140 + *)
1.141 +
1.142 +
1.143 +
1.144 +"############## Make_fun_by_explicit ############## 6.5.03";
1.145 +"############## Make_fun_by_explicit ############## 6.5.03";
1.146 +"############## Make_fun_by_explicit ############## 6.5.03";
1.147 +val c = (the o (parse DiffApp.thy))
1.148 + "Script Make_fun_by_explicit (f_::real) (v_::real) \
1.149 + \ (eqs_::bool list) = \
1.150 + \ (let h_ = (hd o (filterVar f_)) eqs_; \
1.151 + \ e_1 = hd (dropWhile (ident h_) eqs_); \
1.152 + \ vs_ = dropWhile (ident f_) (Vars h_); \
1.153 + \ v_1 = hd (dropWhile (ident v_) vs_); \
1.154 + \ (s_1::bool list)=(SubProblem(Reals_,[univar,equation],[no_met])\
1.155 + \ [bool_ e_1, real_ v_1])\
1.156 + \ in Substitute [(v_1 = (rhs o hd) s_1)] h_)";
1.157 +
1.158 +
1.159 +(*#####################################################--------11.5.02
1.160 +"################ Solve_root_equation #################";
1.161 +(*#####################################################*)
1.162 +val sc = (term_of o the o (parse Test.thy))
1.163 + "Script Solve_root_equation (eq_::bool) (v_::real) (err_::bool) =\
1.164 + \ (let e_ = Rewrite square_equation_left True eq_; \
1.165 + \ e_ = Rewrite_Set Test_simplify False e_; \
1.166 + \ e_ = Rewrite_Set rearrange_assoc False e_; \
1.167 + \ e_ = Rewrite_Set isolate_root False e_; \
1.168 + \ e_ = Rewrite_Set Test_simplify False e_; \
1.169 +
1.170 + \ e_ = Rewrite square_equation_left True e_; \
1.171 + \ e_ = Rewrite_Set Test_simplify False e_; \
1.172 +
1.173 + \ e_ = Rewrite_Set norm_equation False e_; \
1.174 + \ e_ = Rewrite_Set Test_simplify False e_; \
1.175 + \ e_ = Rewrite_Set_Inst [(bdv,v_)] isolate_bdv False e_;\
1.176 + \ e_ = Rewrite_Set Test_simplify False e_ \
1.177 + \ in [e_::bool])";
1.178 +val ags = map (term_of o the o (parse Test.thy))
1.179 + ["sqrt(#9+#4*x)=sqrt x + sqrt(#5+x)", "x::real","#0"];
1.180 +val fmz =
1.181 + ["equality (sqrt(#9+#4*x)=sqrt x + sqrt(#5+x))",
1.182 + "solveFor x","errorBound (eps = #0)","solutions v_i_"];
1.183 +----------------------------------------------------------------11.5.02...*)
1.184 +
1.185 +
1.186 +(*################################# meNEW raises exception with not-locatable
1.187 +"--------------------- Notlocatable: Free_Solve ---------------------";
1.188 +"--------------------- Notlocatable: Free_Solve ---------------------";
1.189 +"--------------------- Notlocatable: Free_Solve ---------------------";
1.190 +val fmz = [];
1.191 +val (dI',pI',mI') =
1.192 + ("Test.thy",["sqroot-test","univariate","equation","test"],
1.193 + ["Test","sqrt-equ-test"]);
1.194 +(*val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.195 +val (p,_,f,nxt,_,pt) = me (mI,m) e_pos'[1] EmptyPtree;*)
1.196 +
1.197 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.198 +val nxt = ("Model_Problem",
1.199 + Model_Problem ["sqroot-test","univariate","equation","test"]);
1.200 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.201 +val nxt =
1.202 + ("Add_Given",
1.203 + Add_Given "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))");
1.204 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.205 +val nxt = ("Add_Given",Add_Given "solveFor x");
1.206 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.207 +val nxt = ("Add_Given",Add_Given "errorBound (eps = 0)");
1.208 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.209 +val nxt = ("Add_Find",Add_Find "solutions v_i_");
1.210 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.211 +val nxt = ("Specify_Theory",Specify_Theory "Test.thy");
1.212 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.213 +val nxt =
1.214 + ("Specify_Problem",Specify_Problem ["sqroot-test","univariate","equation","test"]);
1.215 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.216 +val nxt = ("Specify_Method",Specify_Method ["Test","sqrt-equ-test"]);
1.217 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.218 +
1.219 +"--- -1 ---";
1.220 +val nxt = ("Free_Solve",Free_Solve);
1.221 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.222 +
1.223 +"--- 0 ---";
1.224 +val nxt = ("Take",Take "sqrt(9+4*x)=sqrt x + sqrt(5+x)");
1.225 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.226 +(*me ("Begin_Trans" ////*)
1.227 +
1.228 +"--- 1 ---";
1.229 +val nxt = ("Rewrite_Asm",Rewrite_Asm ("square_equation_left",""));
1.230 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.231 +
1.232 +"--- 2 ---";
1.233 +val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
1.234 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.235 +
1.236 +"--- 3 ---";
1.237 +val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");
1.238 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.239 +if f = Form'
1.240 + (FormKF
1.241 + (~1,EdUndef,1,Nundef,
1.242 + "9 + 4 * x = 5 + 2 * x + 2 * sqrt (x ^^^ 2 + 5 * x)"))
1.243 +then () else raise error "behaviour in root-expl. Free_Solve changed";
1.244 +writeln (pr_ptree pr_short pt);
1.245 +---------------------------------meNEW raises exception with not-locatable*)
1.246 +
1.247 +
1.248 +val d = e_rls;
1.249 +
1.250 +" --- test100: nxt_tac order------------------------------------ ";
1.251 +" --- test100: nxt_tac order------------------------------------ ";
1.252 +
1.253 +val scr as (Script sc) = Script (((inst_abs Test.thy)
1.254 + o term_of o the o (parse thy))
1.255 + "Script Testeq (e_::bool) = \
1.256 + \(While (contains_root e_) Do \
1.257 + \((Try (Repeat (Rewrite rroot_square_inv False))) @@ \
1.258 + \ (Try (Repeat (Rewrite square_equation_left True))) @@ \
1.259 + \ (Try (Repeat (Rewrite radd_0 False)))))\
1.260 + \ e_ ");
1.261 +atomty sc;
1.262 +val (dI',pI',mI') = ("Test.thy",["sqroot-test","univariate","equation","test"],
1.263 + ["Test","sqrt-equ-test"]);
1.264 +val p = e_pos'; val c = [];
1.265 +val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI')));
1.266 +val (p,_,_,_,_,pt) = me (mI,m) p c EmptyPtree;
1.267 +val nxt = ("Specify_Theory",Specify_Theory "Test.thy");
1.268 +val (p,_,_,_,_,pt) = me nxt p c pt;
1.269 +val nxt = ("Specify_Method",Specify_Method ["Test","sqrt-equ-test"]); (*for asm in square_equation_left*)
1.270 +val (p,_,_,_,_,pt) = me nxt p c pt;
1.271 +val p = ([1],Res):pos';
1.272 +val eq_ = (term_of o the o (parse thy))"e_::bool";
1.273 +
1.274 +val ct = "0+(sqrt(sqrt(sqrt a))^^^2)^^^2=0";
1.275 +val ve0_= (term_of o the o (parse thy)) ct;
1.276 +val ets0=[([],(Tac_(Script.thy,"BS","",""),[(eq_,ve0_)],[(eq_,ve0_)],
1.277 + e_term,e_term,Safe)),
1.278 + ([],(User', [], [], e_term, e_term,Sundef))]:ets;
1.279 +val l0 = [];
1.280 +" --------------- 1. ---------------------------------------------";
1.281 +val (pt,_) = cappend_atomic pt[1]e_istate e_term(Rewrite("test",""))(str2term ct,[])Complete;
1.282 +(*12.10.03:*** Unknown theorem(s) "rroot_square_inv"
1.283 +val Appl m'=applicable_in p pt (Rewrite("rroot_square_inv",""));
1.284 +*)
1.285 +
1.286 +
1.287 +val scr as (Script sc) =
1.288 + Script (((inst_abs Test.thy) o term_of o the o (parse thy))
1.289 + "Script Testterm (g_::real) = (Calculate cancel g_)");
1.290 +(*
1.291 +val scr as (Script sc) =
1.292 + Script (((inst_abs Test.thy) o term_of o the o (parse thy))
1.293 + "Script Testterm (g_::real) = (Calculate power g_)");
1.294 +val scr as (Script sc) =
1.295 + Script (((inst_abs Test.thy) o term_of o the o (parse thy))
1.296 + "Script Testterm (g_::real) = (Calculate pow g_)");
1.297 +..............................................................*)
1.298 +writeln
1.299 +"%%%%%%%%%%TODO 7.9.00---vvvvvv--- conflicts with Isa-types \n\
1.300 +\ (Repeat (Calculate cancel g_)) Or \n\
1.301 +\ (Repeat (Calculate power g_)) Or \n\
1.302 +\%%%%%%%%%%%%%%%%%%%%%---^^^^^^--- conflicts with Isa-types \n\
1.303 +\%%%%%%%%%%%%%%%%%%%%%TODO before Detail Rewrite_Set";
1.304 +
1.305 +
1.306 +"--------- sel_rules ---------------------------------------------";
1.307 +"--------- sel_rules ---------------------------------------------";
1.308 +"--------- sel_rules ---------------------------------------------";
1.309 + states:=[];
1.310 + CalcTree
1.311 + [(["equality (x+1=2)", "solveFor x","solutions L"],
1.312 + ("Test.thy",
1.313 + ["sqroot-test","univariate","equation","test"],
1.314 + ["Test","squ-equ-test-subpbl1"]))];
1.315 + Iterator 1;
1.316 + moveActiveRoot 1;
1.317 + autoCalculate 1 CompleteCalc;
1.318 + val ((pt,_),_) = get_calc 1;
1.319 + show_pt pt;
1.320 +
1.321 + val tacs = sel_rules pt ([],Pbl);
1.322 + if tacs = [Apply_Method ["Test", "squ-equ-test-subpbl1"]] then ()
1.323 + else raise error "script.sml: diff.behav. in sel_rules ([],Pbl)";
1.324 +
1.325 + val tacs = sel_rules pt ([1],Res);
1.326 + if tacs = [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
1.327 + Subproblem ("Test.thy", ["linear", "univariate", "equation", "test"]),
1.328 + Check_elementwise "Assumptions"] then ()
1.329 + else raise error "script.sml: diff.behav. in sel_rules ([1],Res)";
1.330 +
1.331 + val tacs = sel_rules pt ([3],Pbl);
1.332 + if tacs = [Apply_Method ["Test", "solve_linear"]] then ()
1.333 + else raise error "script.sml: diff.behav. in sel_rules ([3],Pbl)";
1.334 +
1.335 + val tacs = sel_rules pt ([3,1],Res);
1.336 + if tacs = [Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv"),
1.337 + Rewrite_Set "Test_simplify"] then ()
1.338 + else raise error "script.sml: diff.behav. in sel_rules ([3,1],Res)";
1.339 +
1.340 + val tacs = sel_rules pt ([3],Res);
1.341 + if tacs = [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
1.342 + Subproblem ("Test.thy", ["linear", "univariate", "equation", "test"]),
1.343 + Check_elementwise "Assumptions"] then ()
1.344 + else raise error "script.sml: diff.behav. in sel_rules ([3],Res)";
1.345 +
1.346 + val tacs = (sel_rules pt ([],Res)) handle PTREE str => [Tac str];
1.347 + if tacs = [Tac "no tactics applicable at the end of a calculation"] then ()
1.348 + else raise error "script.sml: diff.behav. in sel_rules ([],Res)";