1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Pure/isac/smltest/Scripts/scrtools.sml Wed Jul 21 13:53:39 2010 +0200
1.3 @@ -0,0 +1,193 @@
1.4 +(* tests on tools for scripts
1.5 + author: Walther Neuper
1.6 + 060605,
1.7 + (c) due to copyright terms
1.8 +
1.9 +use"../smltest/Scripts/scrtools.sml";
1.10 +use"scrtools.sml";
1.11 +*)
1.12 +"-----------------------------------------------------------------";
1.13 +"table of contents -----------------------------------------------";
1.14 +"-----------------------------------------------------------------";
1.15 +"-------- test auto-generated script '(Repeat (Calculate times))'-";
1.16 +"-------- test the same called by interSteps norm_Poly -----------";
1.17 +"-------- test the same called by interSteps norm_Rational -------";
1.18 +"-------- check auto-gen.script for Rewrite_Set_Inst -------------";
1.19 +"-----------------------------------------------------------------";
1.20 +"-----------------------------------------------------------------";
1.21 +"-----------------------------------------------------------------";
1.22 +
1.23 +
1.24 +"-------- test auto-generated script '(Repeat (Calculate times))'-";
1.25 +"-------- test auto-generated script '(Repeat (Calculate times))'-";
1.26 +"-------- test auto-generated script '(Repeat (Calculate times))'-";
1.27 +val Seq {scr = Script auto_script,...} = assoc_rls "norm_Poly";
1.28 +writeln(term2str auto_script);
1.29 +atomty auto_script;
1.30 +
1.31 +store_met
1.32 + (prep_met Test.thy "met_testinter" [] e_metID
1.33 + (["Test","test_interSteps_1"]:metID,
1.34 + [("#Given" ,["term t_"]),
1.35 + ("#Find" ,["normalform n_"])
1.36 + ],
1.37 + {rew_ord'="dummy_ord",rls'=tval_rls,calc=[],srls=e_rls,prls=e_rls,
1.38 + crls=tval_rls, nrls=e_rls},
1.39 +"Script Stepwise t_ = \
1.40 + \(Try (Rewrite_Set discard_minus_ False) @@ \
1.41 + \ Try (Rewrite_Set expand_poly_ False) @@ \
1.42 + \ Try (Repeat (Calculate times)) @@ \
1.43 + \ Try (Rewrite_Set order_mult_rls_ False) @@ \
1.44 + \ Try (Rewrite_Set simplify_power_ False) @@ \
1.45 + \ Try (Rewrite_Set calc_add_mult_pow_ False) @@\
1.46 + \ Try (Rewrite_Set reduce_012_mult_ False) @@ \
1.47 + \ Try (Rewrite_Set order_add_rls_ False) @@ \
1.48 + \ Try (Rewrite_Set collect_numerals_ False) @@ \
1.49 + \ Try (Rewrite_Set reduce_012_ False) @@ \
1.50 + \ Try (Rewrite_Set discard_parentheses_ False))\
1.51 + \ t_"
1.52 +(*presently this script cannot become equal in types to auto_script, because:
1.53 + this t_ must be either 'real' or 'bool' #1#,
1.54 + while the auto_script must be 'z and type-instantiated before usage*)
1.55 + ));
1.56 +show_mets();
1.57 +val {scr = Script parsed_script,...} = get_met ["Test","test_interSteps_1"];
1.58 +writeln(term2str parsed_script);
1.59 +atomty parsed_script;
1.60 +
1.61 +(*the structure of the auto-gen. script is interpreted correctly*)
1.62 +states:=[];
1.63 +CalcTree
1.64 +[(["term (b + a - b)",(*this is Schalk 299b*)
1.65 + "normalform N"],
1.66 + ("Poly.thy",["polynomial","simplification"],
1.67 + ["Test","test_interSteps_1"]))];
1.68 +Iterator 1;
1.69 +moveActiveRoot 1;
1.70 +autoCalculate 1 CompleteCalcHead;
1.71 +
1.72 +fetchProposedTactic 1 (*..Apply_Method*);
1.73 +autoCalculate 1 (Step 1);
1.74 +getTactic 1 ([1], Frm) (*still empty*);
1.75 +
1.76 +fetchProposedTactic 1 (*discard_minus_*);
1.77 +autoCalculate 1 (Step 1);
1.78 +
1.79 +fetchProposedTactic 1 (*order_add_rls_*);
1.80 +autoCalculate 1 (Step 1);
1.81 +
1.82 +fetchProposedTactic 1 (*collect_numerals_*);
1.83 +autoCalculate 1 (Step 1);
1.84 +
1.85 +autoCalculate 1 CompleteCalc;
1.86 +
1.87 +val ((pt,p),_) = get_calc 1; show_pt pt;
1.88 +if existpt' ([1], Frm) pt then ()
1.89 +else raise error "scrtools.sml: test-script test_interSteps_1 doesnt work";
1.90 +
1.91 +
1.92 +"-------- test the same called by interSteps norm_Poly -----------";
1.93 +"-------- test the same called by interSteps norm_Poly -----------";
1.94 +"-------- test the same called by interSteps norm_Poly -----------";
1.95 +val Seq {scr = Script auto_script,...} = assoc_rls "norm_Poly";
1.96 +writeln(term2str auto_script);
1.97 +atomty auto_script;
1.98 +
1.99 +states:=[];
1.100 +CalcTree
1.101 +[(["term (b + a - b)", "normalform N"],
1.102 + ("Poly.thy",["polynomial","simplification"],
1.103 + ["simplification","for_polynomials"]))];
1.104 +Iterator 1;
1.105 +moveActiveRoot 1;
1.106 +autoCalculate 1 CompleteCalc;
1.107 +
1.108 +interSteps 1 ([], Res);
1.109 +val ((pt,p),_) = get_calc 1; show_pt pt;
1.110 +
1.111 +interSteps 1 ([1], Res);
1.112 +val ((pt,p),_) = get_calc 1; show_pt pt;
1.113 +if existpt' ([1,4], Res) pt then ()
1.114 +else raise error "scrtools.sml: auto-generated norm_Poly doesnt work";
1.115 +
1.116 +
1.117 +
1.118 +"-------- test the same called by interSteps norm_Rational -------";
1.119 +"-------- test the same called by interSteps norm_Rational -------";
1.120 +"-------- test the same called by interSteps norm_Rational -------";
1.121 +val Seq {scr = Script auto_script,...} = assoc_rls "norm_Rational";
1.122 +writeln(term2str auto_script);
1.123 +atomty auto_script;
1.124 +(***
1.125 +*** Const (Script.Stepwise, ['z, 'z] => 'z)
1.126 +*** . Free (t_, 'z)
1.127 +*** . Const (Script.Seq, ['a => 'a, 'a => 'a, 'a] => 'a)
1.128 +*** . . Const (Script.Try, ['a => 'a, 'a] => 'a)
1.129 +*** . . . Const (Script.Rewrite'_Set, [Script.ID, bool, 'a] => 'a)
1.130 +*** . . . . Free (discard_minus_, Script.ID)
1.131 +*** . . . . Const (False, bool)
1.132 +*** . . Const (Script.Seq, ['a => 'a, 'a => 'a, 'a] => 'a)
1.133 +*** . . . Const (Script.Try, ['a => 'a, 'a] => 'a)
1.134 +*** . . . . Const (Script.Rewrite'_Set, [Script.ID, bool, 'a] => 'a)
1.135 +*** . . . . . Free (rat_mult_poly, Script.ID)
1.136 +*** . . . . . Const (False, bool)
1.137 +*** . . . Const (Script.Seq, ['a => 'a, 'a => 'a, 'a] => 'a)
1.138 +*** . . . . Const (Script.Try, ['a => 'a, 'a] => 'a)
1.139 +*** . . . . . Const (Script.Rewrite'_Set, [Script.ID, bool, 'a] => 'a)
1.140 +*** . . . . . . Free (make_rat_poly_with_parentheses, Script.ID)
1.141 +*** . . . . . . Const (False, bool)
1.142 +*** . . . . Const (Script.Seq, ['a => 'a, 'a => 'a, 'a] => 'a)
1.143 +*** . . . . . Const (Script.Try, ['a => 'a, 'a] => 'a)
1.144 +*** . . . . . . Const (Script.Rewrite'_Set, [Script.ID, bool, 'a] => 'a)
1.145 +*** . . . . . . . Free (cancel_p_rls, Script.ID)
1.146 +*** . . . . . . . Const (False, bool)
1.147 +*** . . . . . Const (Script.Seq, ['a => 'a, 'a => 'a, 'a] => 'a)
1.148 +*** . . . . . . Const (Script.Try, ['a => 'a, 'a] => 'a)
1.149 +*** . . . . . . . Const (Script.Rewrite'_Set, [Script.ID, bool, 'a] => 'a)
1.150 +*** . . . . . . . . Free (norm_Rational_rls, Script.ID)
1.151 +*** . . . . . . . . Const (False, bool)
1.152 +*** . . . . . . Const (Script.Try, ['a => 'a, 'a] => 'a)
1.153 +*** . . . . . . . Const (Script.Rewrite'_Set, [Script.ID, bool, 'a] => 'a)
1.154 +*** . . . . . . . . Free (discard_parentheses_, Script.ID)
1.155 +*** . . . . . . . . Const (False, bool)
1.156 +*** . . Free (t_, 'a)
1.157 +***)
1.158 +states:=[];
1.159 +CalcTree
1.160 +[(["term (b + a - b)", "normalform N"],
1.161 + ("Poly.thy",["polynomial","simplification"],
1.162 + ["simplification","of_rationals"]))];
1.163 +Iterator 1;
1.164 +moveActiveRoot 1;
1.165 +autoCalculate 1 CompleteCalc;
1.166 +
1.167 +interSteps 1 ([], Res);
1.168 +val ((pt,p),_) = get_calc 1; show_pt pt;
1.169 +
1.170 +interSteps 1 ([1], Res);
1.171 +val ((pt,p),_) = get_calc 1; show_pt pt;
1.172 +
1.173 +(*with "Script SimplifyScript (t_::real) = \
1.174 + \ ((Rewrite_Set norm_Rational False) t_)"
1.175 +val (Form form, Some tac, asm) = pt_extract (pt, ([1], Res));
1.176 +*)
1.177 +val (Form form, Some tac, asm) = pt_extract (pt, ([2], Res));
1.178 +case (term2str form, tac, terms2strs asm) of
1.179 + ("a", Check_Postcond ["polynomial", "simplification"], []) => ()
1.180 + | _ => raise error "scrtools.sml: auto-generated norm_Rational doesnt work";
1.181 +
1.182 +
1.183 +
1.184 +"-------- check auto-gen.script for Rewrite_Set_Inst -------------";
1.185 +"-------- check auto-gen.script for Rewrite_Set_Inst -------------";
1.186 +"-------- check auto-gen.script for Rewrite_Set_Inst -------------";
1.187 +val rls = assoc_rls "integration";
1.188 +val Seq {scr = Script auto_script,...} = rls;
1.189 +writeln(term2str auto_script);
1.190 +
1.191 +if contain_bdv (get_rules rls) then ()
1.192 +else raise error "scrtools.sml: contain_bdv doesnt work for 'integration'";
1.193 +
1.194 +two_scr_arg auto_script;
1.195 +init_istate (Rewrite_Set_Inst (["(bdv, x)"], "integration_rules"))
1.196 + (str2term "someTermWithBdv");