neuper@37906
|
1 |
(* tests on tools for scripts
|
neuper@37906
|
2 |
author: Walther Neuper
|
neuper@37906
|
3 |
060605,
|
neuper@37906
|
4 |
(c) due to copyright terms
|
neuper@37906
|
5 |
|
neuper@37906
|
6 |
use"../smltest/Scripts/scrtools.sml";
|
neuper@37906
|
7 |
use"scrtools.sml";
|
neuper@37906
|
8 |
*)
|
neuper@37906
|
9 |
"-----------------------------------------------------------------";
|
neuper@37906
|
10 |
"table of contents -----------------------------------------------";
|
neuper@37906
|
11 |
"-----------------------------------------------------------------";
|
neuper@37906
|
12 |
"-------- test auto-generated script '(Repeat (Calculate times))'-";
|
neuper@37906
|
13 |
"-------- test the same called by interSteps norm_Poly -----------";
|
neuper@37906
|
14 |
"-------- test the same called by interSteps norm_Rational -------";
|
neuper@37906
|
15 |
"-------- check auto-gen.script for Rewrite_Set_Inst -------------";
|
neuper@37906
|
16 |
"-----------------------------------------------------------------";
|
neuper@37906
|
17 |
"-----------------------------------------------------------------";
|
neuper@37906
|
18 |
"-----------------------------------------------------------------";
|
neuper@37906
|
19 |
|
neuper@37906
|
20 |
|
neuper@37906
|
21 |
"-------- test auto-generated script '(Repeat (Calculate times))'-";
|
neuper@37906
|
22 |
"-------- test auto-generated script '(Repeat (Calculate times))'-";
|
neuper@37906
|
23 |
"-------- test auto-generated script '(Repeat (Calculate times))'-";
|
neuper@37906
|
24 |
val Seq {scr = Script auto_script,...} = assoc_rls "norm_Poly";
|
neuper@37906
|
25 |
writeln(term2str auto_script);
|
neuper@37906
|
26 |
atomty auto_script;
|
neuper@37906
|
27 |
|
neuper@37906
|
28 |
store_met
|
neuper@37906
|
29 |
(prep_met Test.thy "met_testinter" [] e_metID
|
neuper@37906
|
30 |
(["Test","test_interSteps_1"]:metID,
|
neuper@37906
|
31 |
[("#Given" ,["term t_"]),
|
neuper@37906
|
32 |
("#Find" ,["normalform n_"])
|
neuper@37906
|
33 |
],
|
neuper@37906
|
34 |
{rew_ord'="dummy_ord",rls'=tval_rls,calc=[],srls=e_rls,prls=e_rls,
|
neuper@37906
|
35 |
crls=tval_rls, nrls=e_rls},
|
neuper@37906
|
36 |
"Script Stepwise t_ = \
|
neuper@37906
|
37 |
\(Try (Rewrite_Set discard_minus_ False) @@ \
|
neuper@37906
|
38 |
\ Try (Rewrite_Set expand_poly_ False) @@ \
|
neuper@37906
|
39 |
\ Try (Repeat (Calculate times)) @@ \
|
neuper@37906
|
40 |
\ Try (Rewrite_Set order_mult_rls_ False) @@ \
|
neuper@37906
|
41 |
\ Try (Rewrite_Set simplify_power_ False) @@ \
|
neuper@37906
|
42 |
\ Try (Rewrite_Set calc_add_mult_pow_ False) @@\
|
neuper@37906
|
43 |
\ Try (Rewrite_Set reduce_012_mult_ False) @@ \
|
neuper@37906
|
44 |
\ Try (Rewrite_Set order_add_rls_ False) @@ \
|
neuper@37906
|
45 |
\ Try (Rewrite_Set collect_numerals_ False) @@ \
|
neuper@37906
|
46 |
\ Try (Rewrite_Set reduce_012_ False) @@ \
|
neuper@37906
|
47 |
\ Try (Rewrite_Set discard_parentheses_ False))\
|
neuper@37906
|
48 |
\ t_"
|
neuper@37906
|
49 |
(*presently this script cannot become equal in types to auto_script, because:
|
neuper@37906
|
50 |
this t_ must be either 'real' or 'bool' #1#,
|
neuper@37906
|
51 |
while the auto_script must be 'z and type-instantiated before usage*)
|
neuper@37906
|
52 |
));
|
neuper@37906
|
53 |
show_mets();
|
neuper@37906
|
54 |
val {scr = Script parsed_script,...} = get_met ["Test","test_interSteps_1"];
|
neuper@37906
|
55 |
writeln(term2str parsed_script);
|
neuper@37906
|
56 |
atomty parsed_script;
|
neuper@37906
|
57 |
|
neuper@37906
|
58 |
(*the structure of the auto-gen. script is interpreted correctly*)
|
neuper@37906
|
59 |
states:=[];
|
neuper@37906
|
60 |
CalcTree
|
neuper@37906
|
61 |
[(["term (b + a - b)",(*this is Schalk 299b*)
|
neuper@37906
|
62 |
"normalform N"],
|
neuper@37906
|
63 |
("Poly.thy",["polynomial","simplification"],
|
neuper@37906
|
64 |
["Test","test_interSteps_1"]))];
|
neuper@37906
|
65 |
Iterator 1;
|
neuper@37906
|
66 |
moveActiveRoot 1;
|
neuper@37906
|
67 |
autoCalculate 1 CompleteCalcHead;
|
neuper@37906
|
68 |
|
neuper@37906
|
69 |
fetchProposedTactic 1 (*..Apply_Method*);
|
neuper@37906
|
70 |
autoCalculate 1 (Step 1);
|
neuper@37906
|
71 |
getTactic 1 ([1], Frm) (*still empty*);
|
neuper@37906
|
72 |
|
neuper@37906
|
73 |
fetchProposedTactic 1 (*discard_minus_*);
|
neuper@37906
|
74 |
autoCalculate 1 (Step 1);
|
neuper@37906
|
75 |
|
neuper@37906
|
76 |
fetchProposedTactic 1 (*order_add_rls_*);
|
neuper@37906
|
77 |
autoCalculate 1 (Step 1);
|
neuper@37906
|
78 |
|
neuper@37906
|
79 |
fetchProposedTactic 1 (*collect_numerals_*);
|
neuper@37906
|
80 |
autoCalculate 1 (Step 1);
|
neuper@37906
|
81 |
|
neuper@37906
|
82 |
autoCalculate 1 CompleteCalc;
|
neuper@37906
|
83 |
|
neuper@37906
|
84 |
val ((pt,p),_) = get_calc 1; show_pt pt;
|
neuper@37906
|
85 |
if existpt' ([1], Frm) pt then ()
|
neuper@37906
|
86 |
else raise error "scrtools.sml: test-script test_interSteps_1 doesnt work";
|
neuper@37906
|
87 |
|
neuper@37906
|
88 |
|
neuper@37906
|
89 |
"-------- test the same called by interSteps norm_Poly -----------";
|
neuper@37906
|
90 |
"-------- test the same called by interSteps norm_Poly -----------";
|
neuper@37906
|
91 |
"-------- test the same called by interSteps norm_Poly -----------";
|
neuper@37906
|
92 |
val Seq {scr = Script auto_script,...} = assoc_rls "norm_Poly";
|
neuper@37906
|
93 |
writeln(term2str auto_script);
|
neuper@37906
|
94 |
atomty auto_script;
|
neuper@37906
|
95 |
|
neuper@37906
|
96 |
states:=[];
|
neuper@37906
|
97 |
CalcTree
|
neuper@37906
|
98 |
[(["term (b + a - b)", "normalform N"],
|
neuper@37906
|
99 |
("Poly.thy",["polynomial","simplification"],
|
neuper@37906
|
100 |
["simplification","for_polynomials"]))];
|
neuper@37906
|
101 |
Iterator 1;
|
neuper@37906
|
102 |
moveActiveRoot 1;
|
neuper@37906
|
103 |
autoCalculate 1 CompleteCalc;
|
neuper@37906
|
104 |
|
neuper@37906
|
105 |
interSteps 1 ([], Res);
|
neuper@37906
|
106 |
val ((pt,p),_) = get_calc 1; show_pt pt;
|
neuper@37906
|
107 |
|
neuper@37906
|
108 |
interSteps 1 ([1], Res);
|
neuper@37906
|
109 |
val ((pt,p),_) = get_calc 1; show_pt pt;
|
neuper@37906
|
110 |
if existpt' ([1,4], Res) pt then ()
|
neuper@37906
|
111 |
else raise error "scrtools.sml: auto-generated norm_Poly doesnt work";
|
neuper@37906
|
112 |
|
neuper@37906
|
113 |
|
neuper@37906
|
114 |
|
neuper@37906
|
115 |
"-------- test the same called by interSteps norm_Rational -------";
|
neuper@37906
|
116 |
"-------- test the same called by interSteps norm_Rational -------";
|
neuper@37906
|
117 |
"-------- test the same called by interSteps norm_Rational -------";
|
neuper@37906
|
118 |
val Seq {scr = Script auto_script,...} = assoc_rls "norm_Rational";
|
neuper@37906
|
119 |
writeln(term2str auto_script);
|
neuper@37906
|
120 |
atomty auto_script;
|
neuper@37906
|
121 |
(***
|
neuper@37906
|
122 |
*** Const (Script.Stepwise, ['z, 'z] => 'z)
|
neuper@37906
|
123 |
*** . Free (t_, 'z)
|
neuper@37906
|
124 |
*** . Const (Script.Seq, ['a => 'a, 'a => 'a, 'a] => 'a)
|
neuper@37906
|
125 |
*** . . Const (Script.Try, ['a => 'a, 'a] => 'a)
|
neuper@37906
|
126 |
*** . . . Const (Script.Rewrite'_Set, [Script.ID, bool, 'a] => 'a)
|
neuper@37906
|
127 |
*** . . . . Free (discard_minus_, Script.ID)
|
neuper@37906
|
128 |
*** . . . . Const (False, bool)
|
neuper@37906
|
129 |
*** . . Const (Script.Seq, ['a => 'a, 'a => 'a, 'a] => 'a)
|
neuper@37906
|
130 |
*** . . . Const (Script.Try, ['a => 'a, 'a] => 'a)
|
neuper@37906
|
131 |
*** . . . . Const (Script.Rewrite'_Set, [Script.ID, bool, 'a] => 'a)
|
neuper@37906
|
132 |
*** . . . . . Free (rat_mult_poly, Script.ID)
|
neuper@37906
|
133 |
*** . . . . . Const (False, bool)
|
neuper@37906
|
134 |
*** . . . Const (Script.Seq, ['a => 'a, 'a => 'a, 'a] => 'a)
|
neuper@37906
|
135 |
*** . . . . Const (Script.Try, ['a => 'a, 'a] => 'a)
|
neuper@37906
|
136 |
*** . . . . . Const (Script.Rewrite'_Set, [Script.ID, bool, 'a] => 'a)
|
neuper@37906
|
137 |
*** . . . . . . Free (make_rat_poly_with_parentheses, Script.ID)
|
neuper@37906
|
138 |
*** . . . . . . Const (False, bool)
|
neuper@37906
|
139 |
*** . . . . Const (Script.Seq, ['a => 'a, 'a => 'a, 'a] => 'a)
|
neuper@37906
|
140 |
*** . . . . . Const (Script.Try, ['a => 'a, 'a] => 'a)
|
neuper@37906
|
141 |
*** . . . . . . Const (Script.Rewrite'_Set, [Script.ID, bool, 'a] => 'a)
|
neuper@37906
|
142 |
*** . . . . . . . Free (cancel_p_rls, Script.ID)
|
neuper@37906
|
143 |
*** . . . . . . . Const (False, bool)
|
neuper@37906
|
144 |
*** . . . . . Const (Script.Seq, ['a => 'a, 'a => 'a, 'a] => 'a)
|
neuper@37906
|
145 |
*** . . . . . . Const (Script.Try, ['a => 'a, 'a] => 'a)
|
neuper@37906
|
146 |
*** . . . . . . . Const (Script.Rewrite'_Set, [Script.ID, bool, 'a] => 'a)
|
neuper@37906
|
147 |
*** . . . . . . . . Free (norm_Rational_rls, Script.ID)
|
neuper@37906
|
148 |
*** . . . . . . . . Const (False, bool)
|
neuper@37906
|
149 |
*** . . . . . . Const (Script.Try, ['a => 'a, 'a] => 'a)
|
neuper@37906
|
150 |
*** . . . . . . . Const (Script.Rewrite'_Set, [Script.ID, bool, 'a] => 'a)
|
neuper@37906
|
151 |
*** . . . . . . . . Free (discard_parentheses_, Script.ID)
|
neuper@37906
|
152 |
*** . . . . . . . . Const (False, bool)
|
neuper@37906
|
153 |
*** . . Free (t_, 'a)
|
neuper@37906
|
154 |
***)
|
neuper@37906
|
155 |
states:=[];
|
neuper@37906
|
156 |
CalcTree
|
neuper@37906
|
157 |
[(["term (b + a - b)", "normalform N"],
|
neuper@37906
|
158 |
("Poly.thy",["polynomial","simplification"],
|
neuper@37906
|
159 |
["simplification","of_rationals"]))];
|
neuper@37906
|
160 |
Iterator 1;
|
neuper@37906
|
161 |
moveActiveRoot 1;
|
neuper@37906
|
162 |
autoCalculate 1 CompleteCalc;
|
neuper@37906
|
163 |
|
neuper@37906
|
164 |
interSteps 1 ([], Res);
|
neuper@37906
|
165 |
val ((pt,p),_) = get_calc 1; show_pt pt;
|
neuper@37906
|
166 |
|
neuper@37906
|
167 |
interSteps 1 ([1], Res);
|
neuper@37906
|
168 |
val ((pt,p),_) = get_calc 1; show_pt pt;
|
neuper@37906
|
169 |
|
neuper@37906
|
170 |
(*with "Script SimplifyScript (t_::real) = \
|
neuper@37906
|
171 |
\ ((Rewrite_Set norm_Rational False) t_)"
|
neuper@37926
|
172 |
val (Form form, SOME tac, asm) = pt_extract (pt, ([1], Res));
|
neuper@37906
|
173 |
*)
|
neuper@37926
|
174 |
val (Form form, SOME tac, asm) = pt_extract (pt, ([2], Res));
|
neuper@37906
|
175 |
case (term2str form, tac, terms2strs asm) of
|
neuper@37906
|
176 |
("a", Check_Postcond ["polynomial", "simplification"], []) => ()
|
neuper@37906
|
177 |
| _ => raise error "scrtools.sml: auto-generated norm_Rational doesnt work";
|
neuper@37906
|
178 |
|
neuper@37906
|
179 |
|
neuper@37906
|
180 |
|
neuper@37906
|
181 |
"-------- check auto-gen.script for Rewrite_Set_Inst -------------";
|
neuper@37906
|
182 |
"-------- check auto-gen.script for Rewrite_Set_Inst -------------";
|
neuper@37906
|
183 |
"-------- check auto-gen.script for Rewrite_Set_Inst -------------";
|
neuper@37906
|
184 |
val rls = assoc_rls "integration";
|
neuper@37906
|
185 |
val Seq {scr = Script auto_script,...} = rls;
|
neuper@37906
|
186 |
writeln(term2str auto_script);
|
neuper@37906
|
187 |
|
neuper@37906
|
188 |
if contain_bdv (get_rules rls) then ()
|
neuper@37906
|
189 |
else raise error "scrtools.sml: contain_bdv doesnt work for 'integration'";
|
neuper@37906
|
190 |
|
neuper@37906
|
191 |
two_scr_arg auto_script;
|
neuper@37906
|
192 |
init_istate (Rewrite_Set_Inst (["(bdv, x)"], "integration_rules"))
|
neuper@37906
|
193 |
(str2term "someTermWithBdv");
|