wneuper@59546
|
1 |
(* Title: "ProgLang/scrtools.sml"
|
wneuper@59546
|
2 |
tests on tools for scripts
|
akargl@42145
|
3 |
Author: Walther Neuper 060605
|
neuper@37906
|
4 |
(c) due to copyright terms
|
neuper@37906
|
5 |
*)
|
neuper@37906
|
6 |
"-----------------------------------------------------------------";
|
neuper@37906
|
7 |
"table of contents -----------------------------------------------";
|
neuper@37906
|
8 |
"-----------------------------------------------------------------";
|
neuper@37906
|
9 |
"-------- test the same called by interSteps norm_Poly -----------";
|
neuper@37906
|
10 |
"-------- test the same called by interSteps norm_Rational -------";
|
neuper@37906
|
11 |
"-------- check auto-gen.script for Rewrite_Set_Inst -------------";
|
wneuper@59376
|
12 |
"-------- distinguish input to Model -----------------------------------------";
|
wneuper@59376
|
13 |
"-------- fun subpbl, fun pblterm --------------------------------------------";
|
wneuper@59377
|
14 |
"-------- fun stacpbls, fun subst_stacexpr -----------------------------------";
|
wneuper@59376
|
15 |
"-------- fun is_calc, fun op_of_calc ----------------------------------------";
|
wneuper@59376
|
16 |
"-------- fun rule2stac, fun rule2stac_inst ----------------------------------";
|
wneuper@59378
|
17 |
"-------- fun op @@ ----------------------------------------------------------";
|
wneuper@59507
|
18 |
"-------- fun get_fun_id -----------------------------------------------------";
|
wneuper@59547
|
19 |
"-------- fun rules2scr_Rls --------------------------------------------------";
|
wneuper@59376
|
20 |
"-----------------------------------------------------------------------------";
|
wneuper@59376
|
21 |
"-----------------------------------------------------------------------------";
|
wneuper@59376
|
22 |
"-----------------------------------------------------------------------------";
|
neuper@37906
|
23 |
|
neuper@37906
|
24 |
"-------- test the same called by interSteps norm_Poly -----------";
|
neuper@37906
|
25 |
"-------- test the same called by interSteps norm_Poly -----------";
|
neuper@37906
|
26 |
"-------- test the same called by interSteps norm_Poly -----------";
|
neuper@48790
|
27 |
val Seq {scr = Prog auto_script,...} = assoc_rls "norm_Poly";
|
neuper@37906
|
28 |
writeln(term2str auto_script);
|
wneuper@59412
|
29 |
(*Script Stepwise t_t =
|
wneuper@59412
|
30 |
(Try (Rewrite_Set discard_minus False) @@
|
wneuper@59412
|
31 |
Try (Rewrite_Set expand_poly_ False) @@
|
wneuper@59412
|
32 |
Try (Repeat (Calculate TIMES)) @@
|
wneuper@59412
|
33 |
Try (Rewrite_Set order_mult_rls_ False) @@
|
wneuper@59412
|
34 |
Try (Rewrite_Set simplify_power_ False) @@
|
wneuper@59412
|
35 |
Try (Rewrite_Set calc_add_mult_pow_ False) @@
|
wneuper@59412
|
36 |
Try (Rewrite_Set reduce_012_mult_ False) @@
|
wneuper@59412
|
37 |
Try (Rewrite_Set order_add_rls_ False) @@
|
wneuper@59412
|
38 |
Try (Rewrite_Set collect_numerals_ False) @@
|
wneuper@59412
|
39 |
Try (Rewrite_Set reduce_012_ False) @@
|
wneuper@59412
|
40 |
Try (Rewrite_Set discard_parentheses1 False))
|
wneuper@59412
|
41 |
??.empty ..WORKS, NEVERTHELESS *)
|
neuper@37906
|
42 |
atomty auto_script;
|
neuper@37906
|
43 |
|
wneuper@59412
|
44 |
reset_states (); (*<-- evaluate, if ML-blocks are edited below*)
|
neuper@37906
|
45 |
CalcTree
|
neuper@38083
|
46 |
[(["Term (b + a - b)", "normalform N"],
|
neuper@38058
|
47 |
("Poly",["polynomial","simplification"],
|
neuper@37906
|
48 |
["simplification","for_polynomials"]))];
|
neuper@37906
|
49 |
Iterator 1;
|
neuper@37906
|
50 |
moveActiveRoot 1;
|
wneuper@59412
|
51 |
|
wneuper@59248
|
52 |
autoCalculate 1 CompleteCalc;
|
wneuper@59412
|
53 |
val ((pt,p),_) = get_calc 1;
|
wneuper@59412
|
54 |
show_pt pt;
|
wneuper@59412
|
55 |
(* isabisac17 = 15 [
|
wneuper@59412
|
56 |
(([], Frm), Simplify (b + a - b)),
|
wneuper@59412
|
57 |
(([1], Frm), b + a - b),
|
wneuper@59412
|
58 |
(([1], Res), a),
|
wneuper@59412
|
59 |
(([], Res), a)] *)
|
neuper@37906
|
60 |
|
neuper@37906
|
61 |
interSteps 1 ([], Res);
|
neuper@37906
|
62 |
val ((pt,p),_) = get_calc 1; show_pt pt;
|
wneuper@59412
|
63 |
show_pt pt;
|
wneuper@59412
|
64 |
(* isabisac17 = 15 [
|
wneuper@59412
|
65 |
(([], Frm), Simplify (b + a - b)),
|
wneuper@59412
|
66 |
(([1], Frm), b + a - b),
|
wneuper@59412
|
67 |
(([1], Res), a),
|
wneuper@59412
|
68 |
(([], Res), a)] *)
|
neuper@37906
|
69 |
|
wneuper@59412
|
70 |
interSteps 1 ([1], Res);(*<SYSERROR><CALCID>1</CALCID><ERROR>error in kernel 8</ERROR></SYSERROR>*)
|
wneuper@59412
|
71 |
"~~~~~ fun interSteps, args:"; val (cI, ip) = (1, ([1], Res));
|
wneuper@59412
|
72 |
val ((pt, p), tacis) = get_calc cI;
|
wneuper@59412
|
73 |
(*if*) (not o is_interpos) ip = false;
|
wneuper@59412
|
74 |
val ip' = lev_pred' pt ip;
|
wneuper@59412
|
75 |
|
wneuper@59412
|
76 |
(*Math_Engine.detailstep pt ip ..ERROR interSteps>..>init_istate: "norm_Poly" has EmptyScr*)
|
wneuper@59412
|
77 |
val ("donesteps", ctree_BEFORE_step_into, pos'_BEFORE_step_into) = Math_Engine.detailstep pt ip;
|
wneuper@59412
|
78 |
"~~~~~ fun detailstep, args:"; val (pt, (pos as (p, _))) = (pt, ip);
|
wneuper@59412
|
79 |
val nd = Ctree.get_nd pt p
|
wneuper@59412
|
80 |
val cn = Ctree.children nd;
|
wneuper@59412
|
81 |
(*if*) null cn = false;
|
wneuper@59412
|
82 |
|
wneuper@59412
|
83 |
"~~~~~ to detailrls return val:";
|
wneuper@59412
|
84 |
(*else*)
|
wneuper@59412
|
85 |
val return_val = ("donesteps", pt, (p @ [length (Ctree.children (Ctree.get_nd pt p))], Ctree.Res));
|
wneuper@59412
|
86 |
if p @ [length (Ctree.children (Ctree.get_nd pt p))] = [1, 4]
|
wneuper@59412
|
87 |
then () else error "detailrls: auto-generated norm_Poly doesnt work";
|
wneuper@59412
|
88 |
|
neuper@37906
|
89 |
val ((pt,p),_) = get_calc 1; show_pt pt;
|
wneuper@59412
|
90 |
show_pt pt; (*[
|
wneuper@59412
|
91 |
(([], Frm), Simplify (b + a - b)),
|
wneuper@59412
|
92 |
(([1], Frm), b + a - b),
|
wneuper@59412
|
93 |
(([1,1], Frm), b + a - b),
|
wneuper@59412
|
94 |
(([1,1], Res), b + a + -1 * b),
|
wneuper@59412
|
95 |
(([1,2], Res), a + b + -1 * b),
|
wneuper@59412
|
96 |
(([1,3], Res), a + 0 * b),
|
wneuper@59412
|
97 |
(([1,4], Res), a),
|
wneuper@59412
|
98 |
(([1], Res), a),
|
wneuper@59412
|
99 |
(([], Res), a)] *)
|
neuper@37906
|
100 |
if existpt' ([1,4], Res) pt then ()
|
wneuper@59412
|
101 |
else error "auto-generated norm_Poly doesnt work";
|
neuper@37906
|
102 |
|
neuper@37906
|
103 |
|
neuper@37906
|
104 |
"-------- test the same called by interSteps norm_Rational -------";
|
neuper@37906
|
105 |
"-------- test the same called by interSteps norm_Rational -------";
|
neuper@37906
|
106 |
"-------- test the same called by interSteps norm_Rational -------";
|
akargl@42145
|
107 |
|
neuper@48790
|
108 |
val Seq {scr = Prog auto_script,...} = assoc_rls "norm_Rational";
|
neuper@37906
|
109 |
writeln(term2str auto_script);
|
neuper@37906
|
110 |
atomty auto_script;
|
akargl@42145
|
111 |
(***
|
akargl@42145
|
112 |
*** Const (Script.Stepwise, 'z => 'z => 'z)
|
akargl@42145
|
113 |
*** . Free (t_t, 'z)
|
akargl@42145
|
114 |
*** . Const (Script.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
|
akargl@42145
|
115 |
*** . . Const (Script.Try, ('a => 'a) => 'a => 'a)
|
akargl@42145
|
116 |
*** . . . Const (Script.Rewrite'_Set, ID => bool => 'a => 'a)
|
akargl@42145
|
117 |
*** . . . . Free (discard_minus, ID)
|
akargl@42145
|
118 |
*** . . . . Const (HOL.False, bool)
|
akargl@42145
|
119 |
*** . . Const (Script.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
|
akargl@42145
|
120 |
*** . . . Const (Script.Try, ('a => 'a) => 'a => 'a)
|
akargl@42145
|
121 |
*** . . . . Const (Script.Rewrite'_Set, ID => bool => 'a => 'a)
|
akargl@42145
|
122 |
*** . . . . . Free (rat_mult_poly, ID)
|
akargl@42145
|
123 |
*** . . . . . Const (HOL.False, bool)
|
akargl@42145
|
124 |
*** . . . Const (Script.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
|
akargl@42145
|
125 |
*** . . . . Const (Script.Try, ('a => 'a) => 'a => 'a)
|
akargl@42145
|
126 |
*** . . . . . Const (Script.Rewrite'_Set, ID => bool => 'a => 'a)
|
akargl@42145
|
127 |
*** . . . . . . Free (make_rat_poly_with_parentheses, ID)
|
akargl@42145
|
128 |
*** . . . . . . Const (HOL.False, bool)
|
akargl@42145
|
129 |
*** . . . . Const (Script.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
|
akargl@42145
|
130 |
*** . . . . . Const (Script.Try, ('a => 'a) => 'a => 'a)
|
akargl@42145
|
131 |
*** . . . . . . Const (Script.Rewrite'_Set, ID => bool => 'a => 'a)
|
akargl@42145
|
132 |
*** . . . . . . . Free (cancel_p_rls, ID)
|
akargl@42145
|
133 |
*** . . . . . . . Const (HOL.False, bool)
|
akargl@42145
|
134 |
*** . . . . . Const (Script.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
|
akargl@42145
|
135 |
*** . . . . . . Const (Script.Try, ('a => 'a) => 'a => 'a)
|
akargl@42145
|
136 |
*** . . . . . . . Const (Script.Rewrite'_Set, ID => bool => 'a => 'a)
|
akargl@42145
|
137 |
*** . . . . . . . . Free (norm_Rational_rls, ID)
|
akargl@42145
|
138 |
*** . . . . . . . . Const (HOL.False, bool)
|
akargl@42145
|
139 |
*** . . . . . . Const (Script.Try, ('a => 'a) => 'a => 'a)
|
akargl@42145
|
140 |
*** . . . . . . . Const (Script.Rewrite'_Set, ID => bool => 'a => 'a)
|
akargl@42145
|
141 |
*** . . . . . . . . Free (discard_parentheses1, ID)
|
akargl@42145
|
142 |
*** . . . . . . . . Const (HOL.False, bool)
|
akargl@42145
|
143 |
*** . . Const (empty, 'a)
|
neuper@37906
|
144 |
***)
|
s1210629013@55445
|
145 |
reset_states ();
|
neuper@37906
|
146 |
CalcTree
|
neuper@38083
|
147 |
[(["Term (b + a - b)", "normalform N"],
|
neuper@38058
|
148 |
("Poly",["polynomial","simplification"],
|
neuper@37906
|
149 |
["simplification","of_rationals"]))];
|
neuper@37906
|
150 |
Iterator 1;
|
neuper@37906
|
151 |
moveActiveRoot 1;
|
wneuper@59248
|
152 |
autoCalculate 1 CompleteCalc;
|
neuper@37906
|
153 |
|
neuper@37906
|
154 |
interSteps 1 ([], Res);
|
neuper@37906
|
155 |
val ((pt,p),_) = get_calc 1; show_pt pt;
|
neuper@37906
|
156 |
|
neuper@37906
|
157 |
interSteps 1 ([1], Res);
|
neuper@37906
|
158 |
val ((pt,p),_) = get_calc 1; show_pt pt;
|
neuper@37906
|
159 |
|
neuper@37906
|
160 |
(*with "Script SimplifyScript (t_::real) = \
|
neuper@37906
|
161 |
\ ((Rewrite_Set norm_Rational False) t_)"
|
neuper@37926
|
162 |
val (Form form, SOME tac, asm) = pt_extract (pt, ([1], Res));
|
neuper@37906
|
163 |
*)
|
neuper@37926
|
164 |
val (Form form, SOME tac, asm) = pt_extract (pt, ([2], Res));
|
neuper@37906
|
165 |
case (term2str form, tac, terms2strs asm) of
|
neuper@37906
|
166 |
("a", Check_Postcond ["polynomial", "simplification"], []) => ()
|
neuper@38031
|
167 |
| _ => error "scrtools.sml: auto-generated norm_Rational doesnt work";
|
neuper@37906
|
168 |
|
neuper@37906
|
169 |
"-------- check auto-gen.script for Rewrite_Set_Inst -------------";
|
neuper@37906
|
170 |
"-------- check auto-gen.script for Rewrite_Set_Inst -------------";
|
neuper@37906
|
171 |
"-------- check auto-gen.script for Rewrite_Set_Inst -------------";
|
neuper@37906
|
172 |
val rls = assoc_rls "integration";
|
neuper@48790
|
173 |
val Seq {scr = Prog auto_script,...} = rls;
|
neuper@37906
|
174 |
writeln(term2str auto_script);
|
neuper@37906
|
175 |
|
neuper@37906
|
176 |
if contain_bdv (get_rules rls) then ()
|
neuper@38031
|
177 |
else error "scrtools.sml: contain_bdv doesnt work for 'integration'";
|
neuper@37906
|
178 |
|
wneuper@59549
|
179 |
if terms2str (formal_args auto_script) = "[\"t_t\",\"v\"]"
|
wneuper@59549
|
180 |
then () else error "formal_args of auto-gen.script changed";
|
wneuper@59495
|
181 |
init_istate (Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules"))
|
neuper@37906
|
182 |
(str2term "someTermWithBdv");
|
neuper@42426
|
183 |
|
wneuper@59376
|
184 |
|
wneuper@59376
|
185 |
"-------- distinguish input to Model -----------------------------------------";
|
wneuper@59376
|
186 |
"-------- distinguish input to Model -----------------------------------------";
|
wneuper@59376
|
187 |
"-------- distinguish input to Model -----------------------------------------";
|
wneuper@59377
|
188 |
"----- fun is_booll_dsc -----";
|
wneuper@59377
|
189 |
val t as Const ("Descript.relations",
|
wneuper@59377
|
190 |
Type ("fun", [Type ("List.list", [Type ("HOL.bool",[])]),
|
wneuper@59377
|
191 |
Type ("Tools.una", [])])) = @{term "relations"};
|
wneuper@59377
|
192 |
atomtyp (type_of t);
|
wneuper@59377
|
193 |
if is_booll_dsc t then () else error "is_booll_dsc changed";
|
wneuper@59377
|
194 |
"----- fun is_reall_dsc -----";
|
wneuper@59377
|
195 |
if not (is_reall_dsc t) then () else error "is_reall_dsc changed";
|
wneuper@59376
|
196 |
|
wneuper@59377
|
197 |
"----- fun is_list_dsc -----";
|
wneuper@59377
|
198 |
val t = @{term "someList"};
|
wneuper@59377
|
199 |
if is_list_dsc t then () else error "is_list_dsc changed 1";
|
wneuper@59376
|
200 |
|
wneuper@59377
|
201 |
val t = @{term "additionalRels [a=b,c=(d::real)]"};
|
wneuper@59377
|
202 |
if is_list_dsc t then () else error "is_list_dsc changed 2";
|
wneuper@59377
|
203 |
if is_list_dsc (head_of t) then () else error "is_list_dsc changed 3";
|
wneuper@59376
|
204 |
|
wneuper@59377
|
205 |
"----- fun is_list_dsc -----";
|
wneuper@59377
|
206 |
val t = @{term "maximum"};
|
wneuper@59377
|
207 |
if is_dsc t then () else error "is_dsc changed 1";
|
wneuper@59376
|
208 |
|
wneuper@59377
|
209 |
val t = head_of @{term "maximum A"};
|
wneuper@59377
|
210 |
if is_dsc t then () else error "is_dsc changed 2";
|
wneuper@59376
|
211 |
|
wneuper@59377
|
212 |
val t = head_of @{term "fixedValues [R=(R::real)]"};
|
wneuper@59377
|
213 |
if is_dsc t then () else error "is_dsc changed 3";
|
wneuper@59376
|
214 |
|
wneuper@59377
|
215 |
"-------- fun stacpbls, fun subst_stacexpr -----------------------------------";
|
wneuper@59377
|
216 |
"-------- fun stacpbls, fun subst_stacexpr -----------------------------------";
|
wneuper@59377
|
217 |
"-------- fun subst_stacexpr, fun stacpbls -----------------------------------";
|
wneuper@59377
|
218 |
val {scr, ...} = get_met ["Test","sqrt-equ-test"]; val Prog sc = scr; val ts = stacpbls sc;
|
wneuper@59377
|
219 |
case stacpbls sc of
|
wneuper@59490
|
220 |
[Const ("Script.Rewrite", _) $ square_equation_left $ Const ("HOL.True", _),
|
wneuper@59490
|
221 |
Const ("Script.Rewrite'_Set", _) $ Test_simplify $ Const ("HOL.False", _),
|
wneuper@59490
|
222 |
Const ("Script.Rewrite'_Set", _) $ rearrange_assoc $ Const ("HOL.False", _),
|
wneuper@59490
|
223 |
Const ("Script.Rewrite'_Set", _) $ isolate_root $ Const ("HOL.False", _),
|
wneuper@59490
|
224 |
Const ("Script.Rewrite'_Set", _) $ norm_equation $ Const ("HOL.False", _),
|
wneuper@59377
|
225 |
Const ("Script.Rewrite'_Set'_Inst", _) $
|
wneuper@59490
|
226 |
(Const ("List.list.Cons", _) $ (Const ("Product_Type.Pair", _) $ bdv $ Free ("v_v", _)) $
|
wneuper@59377
|
227 |
Const ("List.list.Nil", _)) $
|
wneuper@59490
|
228 |
isolate_bdv $ Const ("HOL.False", _)] =>
|
wneuper@59490
|
229 |
if HOLogic.dest_string square_equation_left = "square_equation_left" andalso
|
wneuper@59490
|
230 |
HOLogic.dest_string Test_simplify = "Test_simplify" andalso
|
wneuper@59490
|
231 |
HOLogic.dest_string rearrange_assoc = "rearrange_assoc" andalso
|
wneuper@59490
|
232 |
HOLogic.dest_string isolate_root = "isolate_root" andalso
|
wneuper@59490
|
233 |
HOLogic.dest_string norm_equation = "norm_equation" andalso
|
wneuper@59490
|
234 |
HOLogic.dest_string bdv = "bdv" andalso
|
wneuper@59490
|
235 |
HOLogic.dest_string isolate_bdv = "isolate_bdv"
|
wneuper@59490
|
236 |
then () else error "stacpbls (Test.Solve_root_equation) changed 2"
|
wneuper@59377
|
237 |
| _ => error "stacpbls (Test.Solve_root_equation) changed 1";
|
wneuper@59376
|
238 |
|
wneuper@59377
|
239 |
(* inappropriate input is skipped *)
|
wneuper@59377
|
240 |
val t = @{term "(a::real) = (rhs (NTH 1 sol_a))"};
|
wneuper@59377
|
241 |
case stacpbls t of [] => () | _ => error "stacpbls rhs (NTH 1 sol_a) changed";
|
wneuper@59377
|
242 |
|
wneuper@59476
|
243 |
@{term "(SubProblem (BiegelinieX,[vonBelastungZu,Biegelinien], [Biegelinien,ausBelastung]) [REAL q__q, REAL v_v])"};
|
wneuper@59377
|
244 |
case stacpbls t of [] => () | _ => error "stacpbls (SubProblem ...) changed";
|
wneuper@59377
|
245 |
|
wneuper@59377
|
246 |
(* --- fun subst_stacexpr *)
|
wneuper@59377
|
247 |
case subst_stacexpr [] NONE e_term sc of
|
wneuper@59546
|
248 |
(NONE, Expr (Const ("HOL.eq", _) $
|
wneuper@59546
|
249 |
(Const ("Test.solve_root_equ", _) $ Free ("e_e", _) $ Free ("v_v", _)) $
|
wneuper@59377
|
250 |
(Const ("HOL.Let", _) $
|
wneuper@59377
|
251 |
(Const ("Script.Seq", _) $
|
wneuper@59377
|
252 |
(Const ("Script.While", _) $ _ $
|
wneuper@59377
|
253 |
_ ) $
|
wneuper@59377
|
254 |
(_) $
|
wneuper@59377
|
255 |
Free ("e_e", _)) $
|
wneuper@59377
|
256 |
Abs ("e_e", _, Const ("List.list.Cons", _) $ Free ("e_e", _) $ Const ("List.list.Nil", _)) )
|
wneuper@59377
|
257 |
)) => ()
|
wneuper@59546
|
258 |
| _ => error "subst_stacexpr [] NONE e_term";
|
wneuper@59376
|
259 |
|
wneuper@59376
|
260 |
"-------- fun is_calc, fun op_of_calc ----------------------------------------";
|
wneuper@59376
|
261 |
"-------- fun is_calc, fun op_of_calc ----------------------------------------";
|
wneuper@59376
|
262 |
"-------- fun is_calc, fun op_of_calc ----------------------------------------";
|
wneuper@59377
|
263 |
val rls = prep_rls @{theory} Test_simplify; (* adds the Program *)
|
wneuper@59377
|
264 |
val Prog sc = (#scr o rep_rls) rls;
|
wneuper@59377
|
265 |
val stacs = stacpbls sc;
|
wneuper@59376
|
266 |
|
wneuper@59377
|
267 |
val calcs = filter is_calc stacs;
|
wneuper@59377
|
268 |
val ids = map op_of_calc calcs;
|
wneuper@59377
|
269 |
case ids of
|
wneuper@59377
|
270 |
["PLUS", "TIMES", "DIVIDE", "POWER"] => ()
|
wneuper@59377
|
271 |
| _ => error "op_of_calc";
|
wneuper@59376
|
272 |
|
wneuper@59490
|
273 |
val calcs = ((assoc_calc' @{theory} |> map) o (map LTool.op_of_calc) o
|
wneuper@59377
|
274 |
(filter LTool.is_calc) o LTool.stacpbls) sc;
|
wneuper@59377
|
275 |
case calcs of
|
wneuper@59377
|
276 |
[("PLUS", ("Groups.plus_class.plus", _)), ("TIMES", ("Groups.times_class.times", _)),
|
wneuper@59377
|
277 |
("DIVIDE", ("Rings.divide_class.divide", _)), ("POWER", ("Atools.pow", _))] => ()
|
wneuper@59377
|
278 |
| _ => error "get_calcs changed"
|
wneuper@59376
|
279 |
|
wneuper@59376
|
280 |
"-------- fun rule2stac, fun rule2stac_inst ----------------------------------";
|
wneuper@59376
|
281 |
"-------- fun rule2stac, fun rule2stac_inst ----------------------------------";
|
wneuper@59376
|
282 |
"-------- fun rule2stac, fun rule2stac_inst ----------------------------------";
|
wneuper@59377
|
283 |
val t = rule2stac @{theory} (Thm ("real_diff_minus", num_str @{thm real_diff_minus}));
|
wneuper@59490
|
284 |
if term2str t = "Try (Repeat (Rewrite ''real_diff_minus'' False))" then ()
|
wneuper@59377
|
285 |
else error "rule2stac Thm.. changed";
|
wneuper@59376
|
286 |
|
wneuper@59377
|
287 |
val t = rule2stac @{theory} (Calc ("Groups.plus_class.plus", eval_binop "#add_"));
|
wneuper@59490
|
288 |
if term2str t = "Try (Repeat (Calculate ''PLUS''))" then ()
|
wneuper@59377
|
289 |
else error "rule2stac Calc.. changed";
|
wneuper@59377
|
290 |
|
wneuper@59377
|
291 |
val t = rule2stac @{theory} (Rls_ rearrange_assoc);
|
wneuper@59490
|
292 |
if term2str t = "Try (Rewrite_Set ''rearrange_assoc'' False)" then ()
|
wneuper@59377
|
293 |
else error "rule2stac Rls_.. changed";
|
wneuper@59377
|
294 |
|
wneuper@59492
|
295 |
val t = rule2stac_inst @{theory} (Thm ("risolate_bdv_add", num_str @{thm risolate_bdv_add}));
|
wneuper@59492
|
296 |
if term2str t = "Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_add'' False))" then ()
|
wneuper@59492
|
297 |
else error "rule2stac_inst Thm.. changed";
|
wneuper@59492
|
298 |
case t of
|
wneuper@59492
|
299 |
(Const ("Script.Try", _) $
|
wneuper@59492
|
300 |
(Const ("Script.Repeat", _) $
|
wneuper@59492
|
301 |
(Const ("Script.Rewrite'_Inst", _) $
|
wneuper@59492
|
302 |
(Const ("List.list.Cons", _) $
|
wneuper@59492
|
303 |
(Const ("Product_Type.Pair", _) $
|
wneuper@59492
|
304 |
bdv $
|
wneuper@59492
|
305 |
Free ("v", _)) $
|
wneuper@59492
|
306 |
Const ("List.list.Nil", _)) $
|
wneuper@59492
|
307 |
risolate_bdv_add $
|
wneuper@59492
|
308 |
Const ("HOL.False", _)))) =>
|
wneuper@59492
|
309 |
(if HOLogic.dest_string bdv = "bdv" andalso
|
wneuper@59492
|
310 |
HOLogic.dest_string risolate_bdv_add = "risolate_bdv_add" then ()
|
wneuper@59492
|
311 |
else error "rule2stac_inst changed 1")
|
wneuper@59492
|
312 |
| _ => error "rule2stac_inst changed 2"
|
wneuper@59492
|
313 |
|
wneuper@59377
|
314 |
"-------- fun op @@ ----------------------------------------------------------";
|
wneuper@59377
|
315 |
"-------- fun op @@ ----------------------------------------------------------";
|
wneuper@59377
|
316 |
"-------- fun op @@ ----------------------------------------------------------";
|
wneuper@59376
|
317 |
val rules = (#rules o rep_rls) isolate_root;
|
wneuper@59377
|
318 |
val rs = map (rule2stac @{theory}) rules;
|
wneuper@59377
|
319 |
val t = @@ rs;
|
wneuper@59490
|
320 |
if term2str t = "Try (Repeat (Rewrite ''rroot_to_lhs'' False)) @@\n" ^
|
wneuper@59490
|
321 |
"Try (Repeat (Rewrite ''rroot_to_lhs_mult'' False)) @@\n" ^
|
wneuper@59490
|
322 |
"Try (Repeat (Rewrite ''rroot_to_lhs_add_mult'' False)) @@\n" ^
|
wneuper@59490
|
323 |
"Try (Repeat (Rewrite ''risolate_root_add'' False)) @@\n" ^
|
wneuper@59490
|
324 |
"Try (Repeat (Rewrite ''risolate_root_mult'' False)) @@\n" ^
|
wneuper@59490
|
325 |
"Try (Repeat (Rewrite ''risolate_root_div'' False))"
|
wneuper@59377
|
326 |
then () else error "fun @@ changed"
|
wneuper@59478
|
327 |
|
wneuper@59507
|
328 |
"-------- fun get_fun_id -----------------------------------------------------";
|
wneuper@59507
|
329 |
"-------- fun get_fun_id -----------------------------------------------------";
|
wneuper@59507
|
330 |
"-------- fun get_fun_id -----------------------------------------------------";
|
wneuper@59507
|
331 |
(* fun_id is nested into arguments, compare ... *)
|
wneuper@59507
|
332 |
val Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $
|
wneuper@59549
|
333 |
(((((((Const (const_id, const_typ) $ _) $ _) $ _) $ _) $ _) $ _) $ _) $ _) =
|
wneuper@59507
|
334 |
Thm.prop_of @{thm biegelinie.simps};
|
wneuper@59507
|
335 |
(* ... to: *)
|
wneuper@59507
|
336 |
val Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $
|
wneuper@59507
|
337 |
(Const (const_id, const_typ) $ _) $ _) =
|
wneuper@59507
|
338 |
Thm.prop_of @{thm simplify.simps};
|
wneuper@59507
|
339 |
|
wneuper@59507
|
340 |
(* get fun_id out of nesting *)
|
wneuper@59507
|
341 |
val Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $
|
wneuper@59507
|
342 |
nested $ _) =
|
wneuper@59507
|
343 |
Thm.prop_of @{thm biegelinie.simps};
|
wneuper@59549
|
344 |
val (Const ("Biegelinie.biegelinie", _) $
|
wneuper@59549
|
345 |
Var (("l", 0), _) $
|
wneuper@59549
|
346 |
Var (("q", 0), _) $
|
wneuper@59549
|
347 |
Var (("v", 0), _) $
|
wneuper@59549
|
348 |
Var (("b", 0), _) $
|
wneuper@59549
|
349 |
Var (("s", 0), _) $
|
wneuper@59549
|
350 |
Var (("vs", 0), _) $
|
wneuper@59549
|
351 |
Var (("id_abl", 0), _)) = nested;
|
wneuper@59507
|
352 |
strip_comb nested;
|
wneuper@59507
|
353 |
(*val it =
|
wneuper@59507
|
354 |
(Const ("Biegelinie.biegelinie", "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool list \<Rightarrow> bool")
|
wneuper@59507
|
355 |
,
|
wneuper@59507
|
356 |
[Var (("l", 0), "real"), Var (("q", 0), "real"), Var (("v", 0), "real"),
|
wneuper@59507
|
357 |
Var (("b", 0), "real \<Rightarrow> real"), Var (("s", 0), "bool list")]):
|
wneuper@59507
|
358 |
term * term list*)
|
wneuper@59507
|
359 |
|
wneuper@59549
|
360 |
case get_fun_id (prep_program @{thm biegelinie.simps}) of
|
wneuper@59507
|
361 |
("Biegelinie.biegelinie", _) => ()
|
wneuper@59507
|
362 |
| _ => error "get_fun_id changed";
|
wneuper@59549
|
363 |
case get_fun_id (prep_program @{thm simplify.simps}) of
|
wneuper@59507
|
364 |
("PolyMinus.simplify", _) => ()
|
wneuper@59507
|
365 |
| _ => error "get_fun_id changed";
|
wneuper@59547
|
366 |
|
wneuper@59547
|
367 |
"-------- fun rules2scr_Rls --------------------------------------------------";
|
wneuper@59547
|
368 |
"-------- fun rules2scr_Rls --------------------------------------------------";
|
wneuper@59547
|
369 |
"-------- fun rules2scr_Rls --------------------------------------------------";
|
wneuper@59547
|
370 |
(*compare Atools.*)
|
wneuper@59547
|
371 |
val prog = LTool.rules2scr_Rls @{theory} [Rule.Thm ("thm111", @{thm thm111}), Rule.Thm ("refl", @{thm refl})]
|
wneuper@59547
|
372 |
;
|
wneuper@59547
|
373 |
writeln (t2str @{theory} prog);
|
wneuper@59547
|
374 |
(*auto_generated t_t =
|
wneuper@59547
|
375 |
Repeat
|
wneuper@59547
|
376 |
((Try (Repeat (Rewrite ''thm111'' False)) @@
|
wneuper@59547
|
377 |
Try (Repeat (Rewrite ''refl'' False)))
|
wneuper@59547
|
378 |
??.empty)*)
|
wneuper@59547
|
379 |
;
|
wneuper@59547
|
380 |
if t2str @{theory} prog =
|
wneuper@59547
|
381 |
"auto_generated t_t =\nRepeat\n ((Try (Repeat (Rewrite ''thm111'' False)) @@\n Try (Repeat (Rewrite ''refl'' False)))\n ??.empty)"
|
wneuper@59547
|
382 |
then () else error "rules2scr_Rls auto_generated changed"
|