walther@59633
|
1 |
(* Title: ProgLang/auto_prog.sml
|
walther@59633
|
2 |
Author: Walther Neuper 190922
|
walther@59633
|
3 |
(c) due to copyright terms
|
walther@59633
|
4 |
*)
|
walther@59633
|
5 |
|
walther@59633
|
6 |
"-----------------------------------------------------------------------------------------------";
|
walther@59633
|
7 |
"-----------------------------------------------------------------------------------------------";
|
walther@59633
|
8 |
"table of contents -----------------------------------------------------------------------------";
|
walther@59633
|
9 |
"-----------------------------------------------------------------------------------------------";
|
walther@59633
|
10 |
"-------- check auto-gen.script for Rewrite_Set_Inst -------------------------------------------";
|
walther@59633
|
11 |
"-------- test the same called by interSteps norm_Poly -----------------------------------------";
|
walther@59633
|
12 |
"-------- test the same called by interSteps norm_Rational -------------------------------------";
|
walther@59637
|
13 |
"-------- fun op #> ----------------------------------------------------------------------------";
|
walther@59633
|
14 |
"-------- fun rules2scr_Rls --------------------------------------------------------------------";
|
walther@59633
|
15 |
"-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------";
|
walther@59802
|
16 |
"-------- fun stacpbls, fun eval_leaf -----------------------------------";
|
walther@59633
|
17 |
"-------- fun is_calc, fun op_of_calc ----------------------------------------------------------";
|
walther@59636
|
18 |
"-------- fun subst_typ ------------------------------------------------------------------------";
|
walther@59636
|
19 |
"-------- fun subst_typs -----------------------------------------------------------------------";
|
walther@59633
|
20 |
"-----------------------------------------------------------------------------------------------";
|
walther@59633
|
21 |
"-----------------------------------------------------------------------------------------------";
|
walther@59633
|
22 |
"-----------------------------------------------------------------------------------------------";
|
walther@59633
|
23 |
|
walther@59633
|
24 |
|
walther@59633
|
25 |
"-------- check auto-gen.script for Rewrite_Set_Inst -------------------------------------------";
|
walther@59633
|
26 |
"-------- check auto-gen.script for Rewrite_Set_Inst -------------------------------------------";
|
walther@59633
|
27 |
"-------- check auto-gen.script for Rewrite_Set_Inst -------------------------------------------";
|
Walther@60543
|
28 |
val rls = get_rls @{context} "integration";
|
walther@59802
|
29 |
val thy' = @{theory "Integrate"}
|
Walther@60500
|
30 |
val ctxt = Proof_Context.init_global thy'
|
walther@59802
|
31 |
val t = @{term "ttt :: real"};
|
walther@59802
|
32 |
|
walther@59802
|
33 |
Auto_Prog.gen thy' t rls;
|
walther@59932
|
34 |
"~~~~~ fun gen , args:"; val (thy, t, rls) = (thy', t, rls);
|
walther@59802
|
35 |
val prog = case rls of
|
walther@59851
|
36 |
Rule_Set.Repeat {rules, ...} => rules2scr_Rls thy rules
|
walther@59878
|
37 |
| Rule_Set.Sequence {rules, ...} => rules2scr_Seq thy rules
|
walther@59802
|
38 |
val auto_script = subst_typs prog (type_of t) (TermC.guess_bdv_typ t) (*return from generate*);
|
walther@59802
|
39 |
|
walther@59868
|
40 |
if UnparseC.term auto_script =
|
walther@59802
|
41 |
"auto_generated_inst t_t v =\n" ^
|
walther@59802
|
42 |
"(Try (Rewrite_Set_Inst [(''bdv'', v)] ''integration_rules'') #>\n" ^
|
walther@59802
|
43 |
" Try (Rewrite_Set_Inst [(''bdv'', v)] ''add_new_c'') #>\n" ^
|
walther@59802
|
44 |
" Try (Rewrite_Set_Inst [(''bdv'', v)] ''simplify_Integral''))\n" ^
|
walther@59802
|
45 |
" ??.empty"
|
walther@59802
|
46 |
then () else error "Auto_Prog.gen integration CHANGED";
|
walther@59633
|
47 |
|
walther@59633
|
48 |
if contain_bdv (get_rules rls) then ()
|
walther@59633
|
49 |
else error "scrtools.sml: contain_bdv doesnt work for 'integration'";
|
walther@59633
|
50 |
|
walther@59997
|
51 |
if UnparseC.terms (formal_args auto_script) = "[\"t_t\", \"v\"]"
|
walther@59633
|
52 |
then () else error "formal_args of auto-gen.script changed";
|
walther@59802
|
53 |
|
walther@60230
|
54 |
Istate.init_detail (Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules")) (TermC.str2term "someTermWithBdv");
|
walther@59935
|
55 |
"~~~~~ fun init_detail , args:"; val ((Tactic.Rewrite_Set_Inst (subs, rls)), t)
|
walther@60230
|
56 |
= ((Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules")), TermC.str2term "someTermWithBdv");
|
Walther@60500
|
57 |
val v = case Subst.T_from_input ctxt subs of
|
walther@59802
|
58 |
(_, v) :: _ => v;
|
Walther@60543
|
59 |
(*case*) get_rls ctxt rls (*of*);
|
walther@59802
|
60 |
|
walther@59633
|
61 |
|
walther@59633
|
62 |
"-------- test the same called by interSteps norm_Poly -----------------------------------------";
|
walther@59633
|
63 |
"-------- test the same called by interSteps norm_Poly -----------------------------------------";
|
walther@59633
|
64 |
"-------- test the same called by interSteps norm_Poly -----------------------------------------";
|
walther@59802
|
65 |
val thy' = @{theory "Poly"}
|
Walther@60543
|
66 |
val ctxt = Proof_Context.init_global thy'
|
Walther@60543
|
67 |
val rls = get_rls ctxt "norm_Poly";
|
walther@59802
|
68 |
val t = @{term "ttt :: real"}
|
walther@59802
|
69 |
val auto_script = Auto_Prog.gen thy' t rls;
|
walther@59802
|
70 |
|
walther@59868
|
71 |
if UnparseC.term auto_script =
|
walther@59802
|
72 |
"auto_generated t_t =\n" ^
|
walther@59802
|
73 |
"(Try (Rewrite_Set ''discard_minus'') #>\n" ^
|
walther@59802
|
74 |
" Try (Rewrite_Set ''expand_poly_'') #>\n" ^
|
walther@59802
|
75 |
" Try (Repeat (Calculate ''TIMES'')) #>\n" ^
|
walther@59802
|
76 |
" Try (Rewrite_Set ''order_mult_rls_'') #>\n" ^
|
walther@59802
|
77 |
" Try (Rewrite_Set ''simplify_power_'') #>\n" ^
|
walther@59802
|
78 |
" Try (Rewrite_Set ''calc_add_mult_pow_'') #>\n" ^
|
walther@59802
|
79 |
" Try (Rewrite_Set ''reduce_012_mult_'') #>\n" ^
|
walther@59802
|
80 |
" Try (Rewrite_Set ''order_add_rls_'') #>\n" ^
|
walther@59802
|
81 |
" Try (Rewrite_Set ''collect_numerals_'') #>\n" ^
|
walther@59802
|
82 |
" Try (Rewrite_Set ''reduce_012_'') #>\n" ^
|
walther@59802
|
83 |
" Try (Rewrite_Set ''discard_parentheses1''))\n" ^
|
walther@59802
|
84 |
" ??.empty" (* ..WORKS, NEVERTHELESS*)
|
walther@59802
|
85 |
then () else error "Auto_Prog.gen norm_Poly CHANGED";
|
walther@59633
|
86 |
|
Walther@60549
|
87 |
States.reset (); (*<-- evaluate, if ML-blocks are edited below*)
|
walther@59633
|
88 |
CalcTree
|
walther@59633
|
89 |
[(["Term (b + a - b)", "normalform N"],
|
walther@59997
|
90 |
("Poly",["polynomial", "simplification"],
|
walther@59997
|
91 |
["simplification", "for_polynomials"]))];
|
walther@59633
|
92 |
Iterator 1;
|
walther@59633
|
93 |
moveActiveRoot 1;
|
walther@59633
|
94 |
|
walther@59633
|
95 |
autoCalculate 1 CompleteCalc;
|
Walther@60549
|
96 |
val ((pt,p),_) = States.get_calc 1;
|
walther@59983
|
97 |
Test_Tool.show_pt pt;
|
walther@59633
|
98 |
(* isabisac17 = 15 [
|
walther@59633
|
99 |
(([], Frm), Simplify (b + a - b)),
|
walther@59633
|
100 |
(([1], Frm), b + a - b),
|
walther@59633
|
101 |
(([1], Res), a),
|
walther@59633
|
102 |
(([], Res), a)] *)
|
walther@59633
|
103 |
|
walther@59633
|
104 |
interSteps 1 ([], Res);
|
Walther@60549
|
105 |
val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
|
walther@59983
|
106 |
Test_Tool.show_pt pt;
|
walther@59633
|
107 |
(* isabisac17 = 15 [
|
walther@59633
|
108 |
(([], Frm), Simplify (b + a - b)),
|
walther@59633
|
109 |
(([1], Frm), b + a - b),
|
walther@59633
|
110 |
(([1], Res), a),
|
walther@59633
|
111 |
(([], Res), a)] *)
|
walther@59633
|
112 |
|
walther@59633
|
113 |
interSteps 1 ([1], Res);(*<SYSERROR><CALCID>1</CALCID><ERROR>error in kernel 8</ERROR></SYSERROR>*)
|
walther@59633
|
114 |
"~~~~~ fun interSteps, args:"; val (cI, ip) = (1, ([1], Res));
|
Walther@60549
|
115 |
val ((pt, p), tacis) = States.get_calc cI;
|
walther@59633
|
116 |
(*if*) (not o is_interpos) ip = false;
|
walther@59633
|
117 |
val ip' = lev_pred' pt ip;
|
walther@59633
|
118 |
|
walther@59935
|
119 |
(*Detail_Step.go pt ip ..ERROR interSteps>..>init_detail: "norm_Poly" has Empty_Prog*)
|
walther@59833
|
120 |
val ("donesteps", ctree_BEFORE_step_into, pos'_BEFORE_step_into) = Detail_Step.go pt ip;
|
walther@59833
|
121 |
"~~~~~ fun go, args:"; val (pt, (pos as (p, _))) = (pt, ip);
|
walther@59633
|
122 |
val nd = Ctree.get_nd pt p
|
walther@59633
|
123 |
val cn = Ctree.children nd;
|
walther@59633
|
124 |
(*if*) null cn = false;
|
walther@59633
|
125 |
|
walther@59633
|
126 |
"~~~~~ to detailrls return val:";
|
walther@59633
|
127 |
(*else*)
|
walther@59694
|
128 |
val return_val = ("donesteps", pt, (p @ [length (Ctree.children (Ctree.get_nd pt p))], Pos.Res));
|
walther@59633
|
129 |
if p @ [length (Ctree.children (Ctree.get_nd pt p))] = [1, 4]
|
walther@59633
|
130 |
then () else error "detailrls: auto-generated norm_Poly doesnt work";
|
walther@59633
|
131 |
|
Walther@60549
|
132 |
val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
|
walther@59983
|
133 |
Test_Tool.show_pt pt; (*[
|
walther@59633
|
134 |
(([], Frm), Simplify (b + a - b)),
|
walther@59633
|
135 |
(([1], Frm), b + a - b),
|
walther@59633
|
136 |
(([1,1], Frm), b + a - b),
|
walther@59633
|
137 |
(([1,1], Res), b + a + -1 * b),
|
walther@59633
|
138 |
(([1,2], Res), a + b + -1 * b),
|
walther@59633
|
139 |
(([1,3], Res), a + 0 * b),
|
walther@59633
|
140 |
(([1,4], Res), a),
|
walther@59633
|
141 |
(([1], Res), a),
|
walther@59633
|
142 |
(([], Res), a)] *)
|
walther@59633
|
143 |
if existpt' ([1,4], Res) pt then ()
|
walther@59633
|
144 |
else error "auto-generated norm_Poly doesnt work";
|
walther@59633
|
145 |
|
walther@59802
|
146 |
|
walther@59633
|
147 |
"-------- test the same called by interSteps norm_Rational -------------------------------------";
|
walther@59633
|
148 |
"-------- test the same called by interSteps norm_Rational -------------------------------------";
|
walther@59633
|
149 |
"-------- test the same called by interSteps norm_Rational -------------------------------------";
|
Walther@60543
|
150 |
val thy = @{theory (** )"Poly" ( **) Rational(**) (*required for rls "norm_Rational"*)}
|
Walther@60543
|
151 |
val ctxt = Proof_Context.init_global thy
|
Walther@60543
|
152 |
val auto_script =
|
Walther@60543
|
153 |
Auto_Prog.gen thy @{term "ttt :: real"} (get_rls ctxt "norm_Rational");
|
walther@59868
|
154 |
writeln(UnparseC.term auto_script);
|
walther@60230
|
155 |
TermC.atomty auto_script;
|
walther@59633
|
156 |
(***
|
walther@59633
|
157 |
*** Const (Program.Stepwise, 'z => 'z => 'z)
|
walther@59633
|
158 |
*** . Free (t_t, 'z)
|
walther@59633
|
159 |
*** . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
|
walther@59633
|
160 |
*** . . Const (Program.Try, ('a => 'a) => 'a => 'a)
|
walther@60278
|
161 |
*** . . . Const (Program.Rewrite_Set, ID => 'a => 'a)
|
walther@59633
|
162 |
*** . . . . Free (discard_minus, ID)
|
walther@59633
|
163 |
*** . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
|
walther@59633
|
164 |
*** . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
|
walther@60278
|
165 |
*** . . . . Const (Program.Rewrite_Set, ID => 'a => 'a)
|
walther@59633
|
166 |
*** . . . . . Free (rat_mult_poly, ID)
|
walther@59633
|
167 |
*** . . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
|
walther@59633
|
168 |
*** . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
|
walther@60278
|
169 |
*** . . . . . Const (Program.Rewrite_Set, ID => 'a => 'a)
|
walther@59633
|
170 |
*** . . . . . . Free (make_rat_poly_with_parentheses, ID)
|
walther@59633
|
171 |
*** . . . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
|
walther@59633
|
172 |
*** . . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
|
walther@60278
|
173 |
*** . . . . . . Const (Program.Rewrite_Set, ID => 'a => 'a)
|
walther@59633
|
174 |
*** . . . . . . . Free (cancel_p_rls, ID)
|
walther@59633
|
175 |
*** . . . . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
|
walther@59633
|
176 |
*** . . . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
|
walther@60278
|
177 |
*** . . . . . . . Const (Program.Rewrite_Set, ID => 'a => 'a)
|
walther@59633
|
178 |
*** . . . . . . . . Free (norm_Rational_rls, ID)
|
walther@59633
|
179 |
*** . . . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
|
walther@60278
|
180 |
*** . . . . . . . Const (Program.Rewrite_Set, ID => 'a => 'a)
|
walther@59633
|
181 |
*** . . . . . . . . Free (discard_parentheses1, ID)
|
walther@59633
|
182 |
*** . . Const (empty, 'a)
|
walther@59633
|
183 |
***)
|
Walther@60549
|
184 |
States.reset ();
|
walther@59633
|
185 |
CalcTree
|
walther@59633
|
186 |
[(["Term (b + a - b)", "normalform N"],
|
Walther@60543
|
187 |
((** )"Poly"( **)"Rational"(**),["polynomial", "simplification"],
|
walther@59997
|
188 |
["simplification", "of_rationals"]))];
|
walther@59633
|
189 |
Iterator 1;
|
walther@59633
|
190 |
moveActiveRoot 1;
|
walther@59633
|
191 |
autoCalculate 1 CompleteCalc;
|
walther@59633
|
192 |
|
walther@59633
|
193 |
interSteps 1 ([], Res);
|
Walther@60549
|
194 |
val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
|
walther@59633
|
195 |
|
walther@59633
|
196 |
interSteps 1 ([1], Res);
|
Walther@60549
|
197 |
val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
|
walther@59633
|
198 |
|
walther@59633
|
199 |
(*with "Program SimplifyScript (t_::real) = \
|
walther@59635
|
200 |
\ ((Rewrite_Set norm_Rational) t_)"
|
walther@59983
|
201 |
val (Form form, SOME tac, asm) = ME_Misc.pt_extract (pt, ([1], Res));
|
walther@59633
|
202 |
*)
|
walther@59983
|
203 |
val (Form form, SOME tac, asm) = ME_Misc.pt_extract (pt, ([2], Res));
|
walther@59868
|
204 |
case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
|
walther@59633
|
205 |
("a", Check_Postcond ["polynomial", "simplification"], []) => ()
|
walther@59633
|
206 |
| _ => error "scrtools.sml: auto-generated norm_Rational doesnt work";
|
walther@59633
|
207 |
|
walther@59802
|
208 |
|
walther@59637
|
209 |
"-------- fun op #> ----------------------------------------------------------------------------";
|
walther@59637
|
210 |
"-------- fun op #> ----------------------------------------------------------------------------";
|
walther@59637
|
211 |
"-------- fun op #> ----------------------------------------------------------------------------";
|
walther@59852
|
212 |
val rules = (#rules o Rule_Set.rep) isolate_root;
|
walther@59633
|
213 |
val rs = map (rule2stac @{theory}) rules;
|
walther@59637
|
214 |
val t = #> rs;
|
walther@59868
|
215 |
if UnparseC.term t = "Try (Repeat (Rewrite ''rroot_to_lhs'')) #>\n" ^
|
walther@59637
|
216 |
"Try (Repeat (Rewrite ''rroot_to_lhs_mult'')) #>\n" ^
|
walther@59637
|
217 |
"Try (Repeat (Rewrite ''rroot_to_lhs_add_mult'')) #>\n" ^
|
walther@59637
|
218 |
"Try (Repeat (Rewrite ''risolate_root_add'')) #>\n" ^
|
walther@59637
|
219 |
"Try (Repeat (Rewrite ''risolate_root_mult'')) #>\n" ^
|
walther@59635
|
220 |
"Try (Repeat (Rewrite ''risolate_root_div''))"
|
walther@59637
|
221 |
then () else error "fun #> changed"
|
walther@59633
|
222 |
|
walther@59802
|
223 |
|
walther@59633
|
224 |
"-------- fun rules2scr_Rls --------------------------------------------------------------------";
|
walther@59633
|
225 |
"-------- fun rules2scr_Rls --------------------------------------------------------------------";
|
walther@59633
|
226 |
"-------- fun rules2scr_Rls --------------------------------------------------------------------";
|
walther@59633
|
227 |
(*compare Prog_Expr.*)
|
walther@60333
|
228 |
val prog = Auto_Prog.rules2scr_Rls @{theory} [\<^rule_thm>\<open>thm111\<close>, \<^rule_thm>\<open>refl\<close>]
|
walther@59633
|
229 |
;
|
walther@59870
|
230 |
writeln (UnparseC.term_in_thy @{theory} prog);
|
walther@59633
|
231 |
(*auto_generated t_t =
|
walther@59633
|
232 |
Repeat
|
walther@59637
|
233 |
((Try (Repeat (Rewrite ''thm111'')) #>
|
walther@59635
|
234 |
Try (Repeat (Rewrite ''refl'')))
|
walther@59633
|
235 |
??.empty)*)
|
walther@59633
|
236 |
;
|
walther@59870
|
237 |
if UnparseC.term_in_thy @{theory} prog =
|
walther@59635
|
238 |
"auto_generated t_t =\n" ^
|
walther@59635
|
239 |
"Repeat\n" ^
|
walther@59637
|
240 |
" ((Try (Repeat (Rewrite ''thm111'')) #> Try (Repeat (Rewrite ''refl'')))\n" ^
|
walther@59635
|
241 |
" ??.empty)"
|
walther@59635
|
242 |
then () else error "rules2scr_Rls auto_generated changed";
|
walther@59633
|
243 |
|
walther@59802
|
244 |
|
walther@59633
|
245 |
"-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------";
|
walther@59633
|
246 |
"-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------";
|
walther@59633
|
247 |
"-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------";
|
walther@60337
|
248 |
val t = rule2stac @{theory} (Thm ("real_diff_minus", @{thm real_diff_minus}));
|
walther@59868
|
249 |
if UnparseC.term t = "Try (Repeat (Rewrite ''real_diff_minus''))" then ()
|
walther@59633
|
250 |
else error "rule2stac Thm.. changed";
|
walther@59633
|
251 |
|
Walther@60516
|
252 |
val t = rule2stac @{theory} (Eval (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_"));
|
walther@59868
|
253 |
if UnparseC.term t = "Try (Repeat (Calculate ''PLUS''))" then ()
|
walther@59878
|
254 |
else error "rule2stac Eval.. changed";
|
walther@59633
|
255 |
|
walther@59633
|
256 |
val t = rule2stac @{theory} (Rls_ rearrange_assoc);
|
walther@59868
|
257 |
if UnparseC.term t = "Try (Rewrite_Set ''rearrange_assoc'')" then ()
|
walther@59633
|
258 |
else error "rule2stac Rls_.. changed";
|
walther@59633
|
259 |
|
walther@60337
|
260 |
val t = rule2stac_inst @{theory} (Thm ("risolate_bdv_add", @{thm risolate_bdv_add}));
|
walther@59868
|
261 |
if UnparseC.term t = "Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_add''))" then ()
|
walther@59633
|
262 |
else error "rule2stac_inst Thm.. changed";
|
walther@59633
|
263 |
case t of
|
walther@60336
|
264 |
(Const (\<^const_name>\<open>Try\<close>, _) $
|
walther@60336
|
265 |
(Const (\<^const_name>\<open>Repeat\<close>, _) $
|
walther@60336
|
266 |
(Const (\<^const_name>\<open>Rewrite_Inst\<close>, _) $
|
wenzelm@60309
|
267 |
(Const (\<^const_name>\<open>Cons\<close>, _) $
|
wenzelm@60309
|
268 |
(Const (\<^const_name>\<open>Pair\<close>, _) $
|
walther@59633
|
269 |
bdv $
|
walther@59633
|
270 |
Free ("v", _)) $
|
wenzelm@60309
|
271 |
Const (\<^const_name>\<open>Nil\<close>, _)) $
|
walther@59635
|
272 |
risolate_bdv_add))) =>
|
walther@59633
|
273 |
(if HOLogic.dest_string bdv = "bdv" andalso
|
walther@59633
|
274 |
HOLogic.dest_string risolate_bdv_add = "risolate_bdv_add" then ()
|
walther@59633
|
275 |
else error "rule2stac_inst changed 1")
|
walther@59633
|
276 |
| _ => error "rule2stac_inst changed 2";
|
walther@59633
|
277 |
|
walther@59802
|
278 |
|
walther@59802
|
279 |
"-------- fun stacpbls, fun eval_leaf -----------------------------------";
|
walther@59802
|
280 |
"-------- fun stacpbls, fun eval_leaf -----------------------------------";
|
walther@59802
|
281 |
"-------- fun stacpbls, fun eval_leaf -----------------------------------";
|
walther@60154
|
282 |
val {scr, ...} = MethodC.from_store ["Test", "sqrt-equ-test"]; val Prog sc = scr; val ts = stacpbls sc;
|
walther@59633
|
283 |
case stacpbls sc of
|
walther@60336
|
284 |
[Const (\<^const_name>\<open>Rewrite\<close>, _) $ square_equation_left,
|
walther@60336
|
285 |
Const (\<^const_name>\<open>Rewrite_Set\<close>, _) $ Test_simplify,
|
walther@60336
|
286 |
Const (\<^const_name>\<open>Rewrite_Set\<close>, _) $ rearrange_assoc,
|
walther@60336
|
287 |
Const (\<^const_name>\<open>Rewrite_Set\<close>, _) $ isolate_root,
|
walther@60336
|
288 |
Const (\<^const_name>\<open>Rewrite_Set\<close>, _) $ norm_equation,
|
walther@60336
|
289 |
Const (\<^const_name>\<open>Rewrite_Set_Inst\<close>, _) $
|
wenzelm@60309
|
290 |
(Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>Pair\<close>, _) $ bdv $ Free ("v_v", _)) $
|
wenzelm@60309
|
291 |
Const (\<^const_name>\<open>Nil\<close>, _)) $ isolate_bdv] =>
|
walther@59633
|
292 |
if HOLogic.dest_string square_equation_left = "square_equation_left" andalso
|
walther@59633
|
293 |
HOLogic.dest_string Test_simplify = "Test_simplify" andalso
|
walther@59633
|
294 |
HOLogic.dest_string rearrange_assoc = "rearrange_assoc" andalso
|
walther@59633
|
295 |
HOLogic.dest_string isolate_root = "isolate_root" andalso
|
walther@59633
|
296 |
HOLogic.dest_string norm_equation = "norm_equation" andalso
|
walther@59633
|
297 |
HOLogic.dest_string bdv = "bdv" andalso
|
walther@59633
|
298 |
HOLogic.dest_string isolate_bdv = "isolate_bdv"
|
walther@59633
|
299 |
then () else error "stacpbls (Test.Solve_root_equation) changed 2"
|
walther@59633
|
300 |
| _ => error "stacpbls (Test.Solve_root_equation) changed 1";
|
walther@59633
|
301 |
|
walther@59633
|
302 |
(* inappropriate input is skipped *)
|
walther@59633
|
303 |
val t = @{term "(a::real) = (rhs (NTH 1 sol_a))"};
|
walther@59633
|
304 |
case stacpbls t of [] => () | _ => error "stacpbls rhs (NTH 1 sol_a) changed";
|
walther@59633
|
305 |
|
walther@59633
|
306 |
@{term "(SubProblem (BiegelinieX,[vonBelastungZu,Biegelinien], [Biegelinien,ausBelastung]) [REAL q__q, REAL v_v])"};
|
walther@59633
|
307 |
case stacpbls t of [] => () | _ => error "stacpbls (SubProblem ...) changed";
|
walther@59633
|
308 |
|
walther@59802
|
309 |
|
walther@59633
|
310 |
"-------- fun is_calc, fun op_of_calc ----------------------------------------------------------";
|
walther@59633
|
311 |
"-------- fun is_calc, fun op_of_calc ----------------------------------------------------------";
|
walther@59633
|
312 |
"-------- fun is_calc, fun op_of_calc ----------------------------------------------------------";
|
walther@59633
|
313 |
val rls = prep_rls @{theory} Test_simplify; (* adds the Program *)
|
walther@59802
|
314 |
val sc = Auto_Prog.gen thy' t rls;
|
walther@59633
|
315 |
val stacs = stacpbls sc;
|
walther@59633
|
316 |
|
walther@59633
|
317 |
val calcs = filter is_calc stacs;
|
walther@59633
|
318 |
val ids = map op_of_calc calcs;
|
walther@59633
|
319 |
case ids of
|
walther@59633
|
320 |
["PLUS", "TIMES", "DIVIDE", "POWER"] => ()
|
walther@59633
|
321 |
| _ => error "op_of_calc";
|
walther@59633
|
322 |
|
walther@59633
|
323 |
val calcs = ((assoc_calc' @{theory} |> map) o (map Auto_Prog.op_of_calc) o
|
walther@59633
|
324 |
(filter Auto_Prog.is_calc) o Auto_Prog.stacpbls) sc;
|
walther@59633
|
325 |
case calcs of
|
wenzelm@60309
|
326 |
[("PLUS", (\<^const_name>\<open>plus\<close>, _)), ("TIMES", (\<^const_name>\<open>times\<close>, _)),
|
wenzelm@60405
|
327 |
("DIVIDE", (\<^const_name>\<open>divide\<close>, _)), ("POWER", (\<^const_name>\<open>realpow\<close>, _))] => ()
|
walther@59633
|
328 |
| _ => error "get_calcs changed"
|
walther@59636
|
329 |
|
walther@59802
|
330 |
|
walther@59636
|
331 |
"-------- fun subst_typ ------------------------------------------------------------------------";
|
walther@59636
|
332 |
"-------- fun subst_typ ------------------------------------------------------------------------";
|
walther@59636
|
333 |
"-------- fun subst_typ ------------------------------------------------------------------------";
|
Walther@60543
|
334 |
val thy = @{theory "Isac_Knowledge"}
|
Walther@60543
|
335 |
val ctxt = Proof_Context.init_global thy
|
Walther@60543
|
336 |
val prog = Auto_Prog.gen thy t (get_rls ctxt "isolate_bdv");
|
walther@59868
|
337 |
(* UnparseC.term prog |> writeln
|
walther@59636
|
338 |
auto_generated_inst t_t v =
|
walther@59636
|
339 |
Repeat
|
walther@59637
|
340 |
((Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_add'')) #>
|
walther@59637
|
341 |
Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_mult_add'')) #>
|
walther@59637
|
342 |
Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_mult'')) #>
|
walther@59637
|
343 |
Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''mult_square'')) #>
|
walther@59637
|
344 |
Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''constant_square'')) #>
|
walther@59636
|
345 |
Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''constant_mult_square'')))
|
walther@59636
|
346 |
??.empty)
|
walther@59636
|
347 |
*)
|
walther@59636
|
348 |
|
walther@59802
|
349 |
val frees = vars prog; (* = [Free ("t_t", "'z"), Free ("v", "real")]*)
|
walther@59802
|
350 |
if length frees = 2 then () else error "test setup Auto_Prog.subst_typ changed 1";
|
walther@59802
|
351 |
|
walther@59636
|
352 |
val args = formal_args prog; (* = [Free ("t_t", "'z"), Free ("v", "real")]*)
|
walther@59636
|
353 |
if length args = 2 then () else error "test setup Auto_Prog.subst_typ changed 2";
|
walther@59636
|
354 |
|
walther@59636
|
355 |
val typ_t = HOLogic.realT
|
walther@59636
|
356 |
val typ_bdv = HOLogic.realT
|
walther@59636
|
357 |
|
walther@59636
|
358 |
val vars_v = (* = [Free ("v", "real"), Free ("v", "'a")]*)
|
walther@59636
|
359 |
filter (fn t => curry op = (t |> dest_Free |> fst) "v") frees
|
walther@59636
|
360 |
val typs_v = (* = ["real", "'a"]*)
|
walther@59636
|
361 |
map (fn t => (t |> dest_Free |> snd)) vars_v;
|
walther@59636
|
362 |
|
walther@59802
|
363 |
val subst_ty = subst_typ "v" HOLogic.realT frees; (* = [("real", "real")]*)
|
walther@59802
|
364 |
if length subst_ty = 1 then () else error "Auto_Prog.subst_typ changed";
|
walther@59802
|
365 |
|
walther@59636
|
366 |
|
walther@59636
|
367 |
"-------- fun subst_typs -----------------------------------------------------------------------";
|
walther@59636
|
368 |
"-------- fun subst_typs -----------------------------------------------------------------------";
|
walther@59636
|
369 |
"-------- fun subst_typs -----------------------------------------------------------------------";
|
Walther@60543
|
370 |
val prog = Auto_Prog.gen thy' t (get_rls ctxt "isolate_bdv");
|
walther@59636
|
371 |
val frees = vars prog; (* = [Free ("t_t", "'z"), Free ("v", "real"), Free ("v", "'a")]*)
|
walther@59802
|
372 |
if length frees = 2 then () else error "test setup Auto_Prog.subst_typs changed 1";
|
walther@59802
|
373 |
|
walther@59636
|
374 |
val args = formal_args prog; (* = [Free ("t_t", "'z"), Free ("v", "real")]*)
|
walther@59636
|
375 |
if length args = 2 then () else error "test setup Auto_Prog.subst_typs changed 2";
|
walther@59636
|
376 |
|
walther@59636
|
377 |
val prog' = subst_typs prog HOLogic.realT HOLogic.realT
|
walther@59636
|
378 |
val frees' = vars prog'; (* = [Free ("t_t", "'z"), Free ("v", "real")]*);
|
walther@59636
|
379 |
if length frees' = 2 then () else error "Auto_Prog.subst_typs changed 2"
|