neuper@37906
|
1 |
(* tests on calchead.sml
|
neuper@37906
|
2 |
author: Walther Neuper
|
neuper@37906
|
3 |
051013,
|
neuper@37906
|
4 |
(c) due to copyright terms
|
neuper@37906
|
5 |
|
neuper@37906
|
6 |
use"../smltest/ME/calchead.sml";
|
neuper@37906
|
7 |
use"calchead.sml";
|
neuper@37906
|
8 |
*)
|
neuper@37906
|
9 |
|
neuper@37906
|
10 |
"-----------------------------------------------------------------";
|
neuper@37906
|
11 |
"table of contents -----------------------------------------------";
|
neuper@37906
|
12 |
"-----------------------------------------------------------------";
|
neuper@37906
|
13 |
"--------- get_interval after replace} other 2 -------------------";
|
neuper@37906
|
14 |
"--------- maximum example with 'specify' ------------------------";
|
neuper@37906
|
15 |
"--------- maximum example with 'specify', fmz <> [] -------------";
|
neuper@37906
|
16 |
"--------- maximum example with 'specify', fmz = [] --------------";
|
neuper@37906
|
17 |
"--------- match_ags, is_cp, cpy_nam +with EqSystem (!)-----------";
|
neuper@37906
|
18 |
"-----------------------------------------------------------------";
|
neuper@37906
|
19 |
"-----------------------------------------------------------------";
|
neuper@37906
|
20 |
"-----------------------------------------------------------------";
|
neuper@37906
|
21 |
|
neuper@37906
|
22 |
|
neuper@37906
|
23 |
"--------- get_interval after replace} other 2 -------------------";
|
neuper@37906
|
24 |
"--------- get_interval after replace} other 2 -------------------";
|
neuper@37906
|
25 |
"--------- get_interval after replace} other 2 -------------------";
|
neuper@37906
|
26 |
states:=[];
|
neuper@37906
|
27 |
CalcTree
|
neuper@37906
|
28 |
[(["equality (x+1=2)", "solveFor x","solutions L"],
|
neuper@37906
|
29 |
("Test.thy",
|
neuper@37906
|
30 |
["sqroot-test","univariate","equation","test"],
|
neuper@37906
|
31 |
["Test","squ-equ-test-subpbl1"]))];
|
neuper@37906
|
32 |
Iterator 1;
|
neuper@37906
|
33 |
moveActiveRoot 1;
|
neuper@37906
|
34 |
autoCalculate 1 CompleteCalc;
|
neuper@37906
|
35 |
moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
|
neuper@37906
|
36 |
replaceFormula 1 "x = 1";
|
neuper@37906
|
37 |
(*... returns calcChangedEvent with ...*)
|
neuper@37906
|
38 |
val (unc, del, gen) = (([1],Res), ([4],Res), ([3,2],Res));
|
neuper@37906
|
39 |
val ((pt,_),_) = get_calc 1;
|
neuper@37906
|
40 |
|
neuper@37906
|
41 |
print_depth 99;map fst (get_interval ([],Pbl) ([],Res) 9999 pt);print_depth 3;
|
neuper@37906
|
42 |
if map fst (get_interval ([],Pbl) ([],Res) 9999 pt) =
|
neuper@37906
|
43 |
[([], Pbl), ([1], Frm),([1], Res), ([2], Res), ([3], Pbl), ([3, 1], Frm),
|
neuper@37906
|
44 |
([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
|
neuper@37906
|
45 |
([3, 2], Res)] then () else
|
neuper@37906
|
46 |
raise error "calchead.sml: diff.behav. get_interval after replace} other 2 a";
|
neuper@37906
|
47 |
|
neuper@37906
|
48 |
print_depth 99;map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt);
|
neuper@37906
|
49 |
print_depth 3;
|
neuper@37906
|
50 |
if map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt) =
|
neuper@37906
|
51 |
[([3, 2, 1], Res), ([3, 2, 2], Res), ([3, 2], Res)] then () else
|
neuper@37906
|
52 |
raise error "modspec.sml: diff.behav. get_interval after replace} other 2 b";
|
neuper@37906
|
53 |
|
neuper@37906
|
54 |
|
neuper@37906
|
55 |
|
neuper@37906
|
56 |
|
neuper@37906
|
57 |
"--------- maximum example with 'specify' ------------------------";
|
neuper@37906
|
58 |
"--------- maximum example with 'specify' ------------------------";
|
neuper@37906
|
59 |
"--------- maximum example with 'specify' ------------------------";
|
neuper@37906
|
60 |
(*" Specify_Problem (match_itms_oris) ";*)
|
neuper@37906
|
61 |
val fmz =
|
neuper@37906
|
62 |
["fixedValues [r=Arbfix]","maximum A",
|
neuper@37906
|
63 |
"valuesFor [a,b]",
|
neuper@37906
|
64 |
"relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
|
neuper@37906
|
65 |
"relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
|
neuper@37906
|
66 |
"relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
|
neuper@37906
|
67 |
|
neuper@37906
|
68 |
"boundVariable a","boundVariable b","boundVariable alpha",
|
neuper@37906
|
69 |
"interval {x::real. 0 <= x & x <= 2*r}",
|
neuper@37906
|
70 |
"interval {x::real. 0 <= x & x <= 2*r}",
|
neuper@37906
|
71 |
"interval {x::real. 0 <= x & x <= pi}",
|
neuper@37906
|
72 |
"errorBound (eps=(0::real))"];
|
neuper@37906
|
73 |
val (dI',pI',mI') =
|
neuper@37906
|
74 |
("DiffApp.thy",["maximum_of","function"],
|
neuper@37906
|
75 |
["DiffApp","max_by_calculus"]);
|
neuper@37906
|
76 |
val c = []:cid;
|
neuper@37906
|
77 |
|
neuper@37906
|
78 |
(*val nxt = Init_Proof' (fmz,(dI',pI',mI'));
|
neuper@37906
|
79 |
val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt e_pos' [] EmptyPtree;
|
neuper@37906
|
80 |
*)
|
neuper@37906
|
81 |
val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
82 |
val nxt = tac2tac_ pt p nxt;
|
neuper@37906
|
83 |
val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
|
neuper@37906
|
84 |
(*val nxt = Add_Given "fixedValues [(r::real) = Arbfix]" : tac*)
|
neuper@37906
|
85 |
|
neuper@37906
|
86 |
val nxt = tac2tac_ pt p nxt;
|
neuper@37906
|
87 |
val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
|
neuper@37906
|
88 |
(**)
|
neuper@37906
|
89 |
|
neuper@37906
|
90 |
(*---6.5.03
|
neuper@37906
|
91 |
val nxt = tac2tac_ pt p (Add_Find "valuesFor [(a::real)]");
|
neuper@37906
|
92 |
val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
|
neuper@37906
|
93 |
(*uncaught exception TYPE 6.5.03*)
|
neuper@37906
|
94 |
|
neuper@37906
|
95 |
if ppc<>(Problem [],
|
neuper@37906
|
96 |
{Find=[Incompl "maximum",Incompl "valuesFor [a]"],
|
neuper@37906
|
97 |
Given=[Correct "fixedValues [r = Arbfix]"],
|
neuper@37906
|
98 |
Relate=[Incompl "relations []"], Where=[],With=[]})
|
neuper@37906
|
99 |
then raise error "test-maximum.sml: model stepwise - different behaviour"
|
neuper@37906
|
100 |
else (); (*different with show_types !!!*)
|
neuper@37906
|
101 |
6.5.03---*)
|
neuper@37906
|
102 |
|
neuper@37906
|
103 |
(*-----appl_add should not create Error', but accept as Sup,Syn
|
neuper@37906
|
104 |
val nxt = tac2tac_ pt p (Add_Given "boundVariable a");
|
neuper@37906
|
105 |
val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
|
neuper@37906
|
106 |
(**)
|
neuper@37906
|
107 |
val nxt = tac2tac_ pt p (Add_Given "boundVariable a+");
|
neuper@37906
|
108 |
val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
|
neuper@37906
|
109 |
(**)---*)
|
neuper@37906
|
110 |
|
neuper@37906
|
111 |
val m = Specify_Problem ["maximum_of","function"];
|
neuper@37906
|
112 |
val nxt = tac2tac_ pt p m;
|
neuper@37906
|
113 |
val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
|
neuper@37906
|
114 |
(**)
|
neuper@37906
|
115 |
|
neuper@37906
|
116 |
if ppc<>(Problem ["maximum_of","function"],
|
neuper@37906
|
117 |
{Find=[Incompl "maximum",Incompl "valuesFor"],
|
neuper@37906
|
118 |
Given=[Correct "fixedValues [r = Arbfix]"],
|
neuper@37906
|
119 |
Relate=[Incompl "relations []"], Where=[],With=[]})
|
neuper@37906
|
120 |
then raise error "diffappl.sml: Specify_Problem different behaviour"
|
neuper@37906
|
121 |
else ();
|
neuper@37906
|
122 |
(* WN.3.9.03 (#391) Model_Specify did init_pbl newly
|
neuper@37906
|
123 |
if ppc<>(Problem ["maximum_of","function"],
|
neuper@37906
|
124 |
{Find=[Missing "maximum m_",Missing "valuesFor vs_"],
|
neuper@37906
|
125 |
Given=[Correct "fixedValues [r = Arbfix]"],
|
neuper@37906
|
126 |
Relate=[Missing "relations rs_"],Where=[],With=[]})
|
neuper@37906
|
127 |
then raise error "diffappl.sml: Specify_Problem different behaviour"
|
neuper@37906
|
128 |
else ();*)
|
neuper@37906
|
129 |
|
neuper@37906
|
130 |
val nxt = tac2tac_ pt p(Specify_Method ["DiffApp","max_by_calculus"]);
|
neuper@37906
|
131 |
val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
|
neuper@37906
|
132 |
(**)
|
neuper@37906
|
133 |
|
neuper@37906
|
134 |
if ppc<>(Method ["DiffApp","max_by_calculus"],
|
neuper@37906
|
135 |
{Find=[Incompl "maximum",Incompl "valuesFor"],
|
neuper@37981
|
136 |
Given=[Correct "fixedValues [r = Arbfix]",Missing "boundVariable v_v",
|
neuper@37906
|
137 |
Missing "interval itv_",Missing "errorBound err_"],
|
neuper@37906
|
138 |
Relate=[Incompl "relations []"],Where=[],With=[]})
|
neuper@37906
|
139 |
then raise error "diffappl.sml: Specify_Method different behaviour"
|
neuper@37906
|
140 |
else ();
|
neuper@37906
|
141 |
(* WN.3.9.03 (#391) Model_Specify did init_pbl newly
|
neuper@37906
|
142 |
if ppc<>(Method ["DiffApp","max_by_calculus"],
|
neuper@37906
|
143 |
{Find=[Missing "maximum m_",Missing "valuesFor vs_"],
|
neuper@37981
|
144 |
Given=[Correct "fixedValues [r = Arbfix]",Missing "boundVariable v_v",
|
neuper@37906
|
145 |
Missing "interval itv_",Missing "errorBound err_"],
|
neuper@37906
|
146 |
Relate=[Missing "relations rs_"],Where=[],With=[]})
|
neuper@37906
|
147 |
then raise error "diffappl.sml: Specify_Method different behaviour"
|
neuper@37906
|
148 |
else ();*)
|
neuper@37906
|
149 |
|
neuper@37906
|
150 |
|
neuper@37906
|
151 |
|
neuper@37906
|
152 |
"--------- maximum example with 'specify', fmz <> [] -------------";
|
neuper@37906
|
153 |
"--------- maximum example with 'specify', fmz <> [] -------------";
|
neuper@37906
|
154 |
"--------- maximum example with 'specify', fmz <> [] -------------";
|
neuper@37906
|
155 |
val fmz =
|
neuper@37906
|
156 |
["fixedValues [r=Arbfix]","maximum A",
|
neuper@37906
|
157 |
"valuesFor [a,b]",
|
neuper@37906
|
158 |
"relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
|
neuper@37906
|
159 |
"relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
|
neuper@37906
|
160 |
"relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
|
neuper@37906
|
161 |
|
neuper@37906
|
162 |
"boundVariable a","boundVariable b","boundVariable alpha",
|
neuper@37906
|
163 |
"interval {x::real. 0 <= x & x <= 2*r}",
|
neuper@37906
|
164 |
"interval {x::real. 0 <= x & x <= 2*r}",
|
neuper@37906
|
165 |
"interval {x::real. 0 <= x & x <= pi}",
|
neuper@37906
|
166 |
"errorBound (eps=(0::real))"];
|
neuper@37906
|
167 |
val (dI',pI',mI') =
|
neuper@37906
|
168 |
("DiffApp.thy",["maximum_of","function"],
|
neuper@37906
|
169 |
["DiffApp","max_by_calculus"]);
|
neuper@37906
|
170 |
val c = []:cid;
|
neuper@37906
|
171 |
(*val nxt = Init_Proof' (fmz,(dI',pI',mI'));*)
|
neuper@37906
|
172 |
val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
173 |
|
neuper@37906
|
174 |
val nxt = tac2tac_ pt p nxt;
|
neuper@37906
|
175 |
val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt e_pos' [] pt;
|
neuper@37906
|
176 |
val nxt = tac2tac_ pt p nxt;
|
neuper@37906
|
177 |
val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
|
neuper@37906
|
178 |
(*val nxt = Add_Given "fixedValues [(r::real) = Arbfix]" : tac*)
|
neuper@37906
|
179 |
|
neuper@37906
|
180 |
val nxt = tac2tac_ pt p nxt;
|
neuper@37906
|
181 |
val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
|
neuper@37906
|
182 |
(*val nxt = Add_Find "maximum (A::bool)" : tac*)
|
neuper@37906
|
183 |
|
neuper@37906
|
184 |
val nxt = tac2tac_ pt p nxt;
|
neuper@37906
|
185 |
val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
|
neuper@37906
|
186 |
(*val nxt = Add_Find "valuesFor [(a::real)]" : tac*)
|
neuper@37906
|
187 |
|
neuper@37906
|
188 |
val nxt = tac2tac_ pt p nxt;
|
neuper@37906
|
189 |
val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
|
neuper@37906
|
190 |
(*val nxt = Add_Find "valuesFor [(b::real)]" : tac*)
|
neuper@37906
|
191 |
|
neuper@37906
|
192 |
val nxt = tac2tac_ pt p nxt;
|
neuper@37906
|
193 |
val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
|
neuper@37906
|
194 |
(*val nxt = Add_Relation "relations [A = a * b]" *)
|
neuper@37906
|
195 |
|
neuper@37906
|
196 |
val nxt = tac2tac_ pt p nxt;
|
neuper@37906
|
197 |
val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
|
neuper@37906
|
198 |
(*Add_Relation "relations\n [((a::real) // (#2::real)) ..."*)
|
neuper@37906
|
199 |
|
neuper@37906
|
200 |
(*---------------------------- FIXXXXME.meNEW !!! partial Add-Relation !!!
|
neuper@37906
|
201 |
nxt_specif <> specify ?!
|
neuper@37906
|
202 |
|
neuper@37906
|
203 |
if nxt<>(Add_Relation
|
neuper@37906
|
204 |
"relations [(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]")
|
neuper@37906
|
205 |
then raise error "test specify, fmz <> []: nxt <> Add_Relation (a/2)^2.." else (); (*different with show_types !!!*)
|
neuper@37906
|
206 |
|
neuper@37906
|
207 |
val nxt = tac2tac_ pt p nxt;
|
neuper@37906
|
208 |
val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
|
neuper@37906
|
209 |
------------------------------ FIXXXXME.meNEW !!! ---*)
|
neuper@37906
|
210 |
|
neuper@37906
|
211 |
(*val nxt = Specify_Theory "DiffApp.thy" : tac*)
|
neuper@37906
|
212 |
|
neuper@37924
|
213 |
val itms = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt itms);
|
neuper@37906
|
214 |
|
neuper@37906
|
215 |
val nxt = tac2tac_ pt p nxt;
|
neuper@37906
|
216 |
val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
|
neuper@37906
|
217 |
(*val nxt = Specify_Problem ["maximum_of","function"]*)
|
neuper@37906
|
218 |
|
neuper@37906
|
219 |
val nxt = tac2tac_ pt p nxt;
|
neuper@37906
|
220 |
val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
|
neuper@37906
|
221 |
(*val nxt = Specify_Method ("DiffApp.thy","max_by_calculus")*)
|
neuper@37906
|
222 |
|
neuper@37906
|
223 |
val nxt = tac2tac_ pt p nxt;
|
neuper@37906
|
224 |
val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
|
neuper@37906
|
225 |
(*val nxt = Add_Given "boundVariable a" : tac*)
|
neuper@37906
|
226 |
|
neuper@37906
|
227 |
val nxt = tac2tac_ pt p nxt;
|
neuper@37906
|
228 |
val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
|
neuper@37906
|
229 |
(*val nxt = Add_Given "interval {x. #0 <= x & x <= #2 * r}" : *)
|
neuper@37906
|
230 |
|
neuper@37906
|
231 |
val nxt = tac2tac_ pt p nxt;
|
neuper@37906
|
232 |
val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
|
neuper@37906
|
233 |
(*val nxt = Add_Given "errorBound (eps = #0)" : tac*)
|
neuper@37906
|
234 |
|
neuper@37906
|
235 |
val nxt = tac2tac_ pt p nxt;
|
neuper@37906
|
236 |
val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
|
neuper@37906
|
237 |
(*val nxt = Apply_Method ("DiffApp.thy","max_by_calculus") *)
|
neuper@37906
|
238 |
if nxt<>(Apply_Method ["DiffApp","max_by_calculus"])
|
neuper@37906
|
239 |
then raise error "test specify, fmz <> []: nxt <> Apply_Method max_by_calculus" else ();
|
neuper@37906
|
240 |
|
neuper@37906
|
241 |
|
neuper@37906
|
242 |
"--------- maximum example with 'specify', fmz = [] --------------";
|
neuper@37906
|
243 |
"--------- maximum example with 'specify', fmz = [] --------------";
|
neuper@37906
|
244 |
"--------- maximum example with 'specify', fmz = [] --------------";
|
neuper@37906
|
245 |
val fmz = [];
|
neuper@37906
|
246 |
val (dI',pI',mI') = empty_spec;
|
neuper@37906
|
247 |
val c = []:cid;
|
neuper@37906
|
248 |
|
neuper@37906
|
249 |
val nxt = Init_Proof' (fmz,(dI',pI',mI'));(*!!!!!!!!*)
|
neuper@37906
|
250 |
(*val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; !!!*)
|
neuper@37906
|
251 |
val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt e_pos' []
|
neuper@37906
|
252 |
EmptyPtree;
|
neuper@37906
|
253 |
val nxt = tac2tac_ pt p nxt;
|
neuper@37906
|
254 |
val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
|
neuper@37906
|
255 |
(*val nxt = Specify_Theory "e_domID" : tac*)
|
neuper@37906
|
256 |
|
neuper@37906
|
257 |
val nxt = Specify_Theory "DiffApp.thy";
|
neuper@37906
|
258 |
val nxt = tac2tac_ pt p nxt;
|
neuper@37906
|
259 |
val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
|
neuper@37906
|
260 |
(*val nxt = Specify_Problem ["e_pblID"] : tac*)
|
neuper@37906
|
261 |
|
neuper@37906
|
262 |
val nxt = Specify_Problem ["maximum_of","function"];
|
neuper@37906
|
263 |
val nxt = tac2tac_ pt p nxt;
|
neuper@37906
|
264 |
val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
|
neuper@37906
|
265 |
(*val nxt = Add_Given "fixedValues" : tac*)
|
neuper@37906
|
266 |
|
neuper@37906
|
267 |
val nxt = Add_Given "fixedValues [r=Arbfix]";
|
neuper@37906
|
268 |
val nxt = tac2tac_ pt p nxt;
|
neuper@37906
|
269 |
val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
|
neuper@37906
|
270 |
(*val nxt = Add_Find "maximum" : tac*)
|
neuper@37906
|
271 |
|
neuper@37906
|
272 |
val nxt = Add_Find "maximum A";
|
neuper@37906
|
273 |
val nxt = tac2tac_ pt p nxt;
|
neuper@37906
|
274 |
|
neuper@37906
|
275 |
|
neuper@37906
|
276 |
val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
|
neuper@37906
|
277 |
(*val nxt = Add_Find "valuesFor" : tac*)
|
neuper@37906
|
278 |
|
neuper@37906
|
279 |
val nxt = Add_Find "valuesFor [a]";
|
neuper@37906
|
280 |
val nxt = tac2tac_ pt p nxt;
|
neuper@37906
|
281 |
val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
|
neuper@37906
|
282 |
(*val nxt = Add_Relation "relations" ---
|
neuper@37906
|
283 |
--- [b=Arbfix] KANN NICHT VERLANGT WERDEN !!!!*)
|
neuper@37906
|
284 |
|
neuper@37906
|
285 |
(*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....
|
neuper@37906
|
286 |
if nxt<>(Add_Relation "relations []")
|
neuper@37906
|
287 |
then raise error "test specify, fmz <> []: nxt <> Add_Relation.."
|
neuper@37906
|
288 |
else (); (*different with show_types !!!*)
|
neuper@37906
|
289 |
*)
|
neuper@37906
|
290 |
|
neuper@37906
|
291 |
val nxt = Add_Relation "relations [(A=a+b)]";
|
neuper@37906
|
292 |
val nxt = tac2tac_ pt p nxt;
|
neuper@37906
|
293 |
val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
|
neuper@37906
|
294 |
(*val nxt = Specify_Method ("e_domID","e_metID") : tac*)
|
neuper@37906
|
295 |
|
neuper@37906
|
296 |
val nxt = Specify_Method ["DiffApp","max_by_calculus"];
|
neuper@37906
|
297 |
val nxt = tac2tac_ pt p nxt;
|
neuper@37906
|
298 |
val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
|
neuper@37906
|
299 |
(*val nxt = Add_Given "boundVariable" : tac*)
|
neuper@37906
|
300 |
|
neuper@37906
|
301 |
val nxt = Add_Given "boundVariable alpha";
|
neuper@37906
|
302 |
val nxt = tac2tac_ pt p nxt;
|
neuper@37906
|
303 |
val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
|
neuper@37906
|
304 |
(*val nxt = Add_Given "interval" : tac*)
|
neuper@37906
|
305 |
|
neuper@37906
|
306 |
val nxt = Add_Given "interval {x. 2 <= x & x <= 3}";
|
neuper@37906
|
307 |
val nxt = tac2tac_ pt p nxt;
|
neuper@37906
|
308 |
val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
|
neuper@37906
|
309 |
(*val nxt = Add_Given "errorBound" : tac*)
|
neuper@37906
|
310 |
|
neuper@37906
|
311 |
val nxt = Add_Given "errorBound (eps=999)";
|
neuper@37906
|
312 |
val nxt = tac2tac_ pt p nxt;
|
neuper@37906
|
313 |
val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
|
neuper@37906
|
314 |
(*val nxt = Apply_Method ("DiffApp","max_by_calculus") *)
|
neuper@37906
|
315 |
(*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....
|
neuper@37906
|
316 |
if nxt<>(Apply_Method ("DiffApp.thy","max_by_calculus"))
|
neuper@37906
|
317 |
then raise error "test specify, fmz <> []: nxt <> Add_Relation.."
|
neuper@37906
|
318 |
else ();
|
neuper@37906
|
319 |
*)
|
neuper@37906
|
320 |
|
neuper@37906
|
321 |
(* 2.4.00 nach Transfer specify -> hard_gen
|
neuper@37906
|
322 |
val nxt = Apply_Method ("DiffApp.thy","max_by_calculus");
|
neuper@37906
|
323 |
val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; *)
|
neuper@37906
|
324 |
(*val nxt = Empty_Tac : tac*)
|
neuper@37906
|
325 |
|
neuper@37906
|
326 |
|
neuper@37906
|
327 |
"--------- match_ags, is_cp, cpy_nam +with EqSystem (!)-----------";
|
neuper@37906
|
328 |
"--------- match_ags, is_cp, cpy_nam +with EqSystem (!)-----------";
|
neuper@37906
|
329 |
"--------- match_ags, is_cp, cpy_nam +with EqSystem (!)-----------";
|
neuper@37906
|
330 |
val Const ("Script.SubProblem",_) $
|
neuper@37906
|
331 |
(Const ("Pair",_) $
|
neuper@37906
|
332 |
Free (dI',_) $
|
neuper@37906
|
333 |
(Const ("Pair",_) $ pI' $ mI')) $ ags' =
|
neuper@37906
|
334 |
(*...copied from stac2tac_*)
|
neuper@37906
|
335 |
str2term
|
neuper@37906
|
336 |
"SubProblem (EqSystem_, [linear, system], [no_met])\
|
neuper@37984
|
337 |
\ [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2],\
|
neuper@37984
|
338 |
\ REAL_LIST [c, c_2]]";
|
neuper@37906
|
339 |
val ags = isalist2list ags';
|
neuper@37906
|
340 |
val pI = ["linear","system"];
|
neuper@37906
|
341 |
val pats = (#ppc o get_pbt) pI;
|
neuper@37906
|
342 |
case match_ags Isac.thy pats ags of
|
neuper@37906
|
343 |
[(1, [1], "#Given", Const ("Descript.equalities", _), _),
|
neuper@37906
|
344 |
(2, [1], "#Given", Const ("EqSystem.solveForVars", _),
|
neuper@37906
|
345 |
[ _ $ Free ("c", _) $ _, _ $ Free ("c_2", _) $ _]),
|
neuper@37906
|
346 |
(3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss___", _)])]
|
neuper@37906
|
347 |
=>()
|
neuper@37906
|
348 |
| _ => raise error "calchead.sml match_ags 2 args OK -----------------";
|
neuper@37906
|
349 |
|
neuper@37906
|
350 |
|
neuper@37906
|
351 |
val Const ("Script.SubProblem",_) $
|
neuper@37906
|
352 |
(Const ("Pair",_) $
|
neuper@37906
|
353 |
Free (dI',_) $
|
neuper@37906
|
354 |
(Const ("Pair",_) $ pI' $ mI')) $ ags' =
|
neuper@37906
|
355 |
(*...copied from stac2tac_*)
|
neuper@37906
|
356 |
str2term
|
neuper@37906
|
357 |
"SubProblem (EqSystem_, [linear, system], [no_met])\
|
neuper@37984
|
358 |
\ [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2],\
|
neuper@37984
|
359 |
\ REAL_LIST [c, c_2], BOOL_LIST ss___]";
|
neuper@37906
|
360 |
val ags = isalist2list ags';
|
neuper@37906
|
361 |
val pI = ["linear","system"];
|
neuper@37906
|
362 |
val pats = (#ppc o get_pbt) pI;
|
neuper@37906
|
363 |
case match_ags Isac.thy pats ags of
|
neuper@37906
|
364 |
[(1, [1], "#Given", Const ("Descript.equalities", _), _),
|
neuper@37906
|
365 |
(2, [1], "#Given", Const ("EqSystem.solveForVars", _),
|
neuper@37906
|
366 |
[_ $ Free ("c", _) $ _,
|
neuper@37906
|
367 |
_ $ Free ("c_2", _) $ _]),
|
neuper@37906
|
368 |
(3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss___", _)])]
|
neuper@37906
|
369 |
(* type of Find: [Free ("ss___", "bool List.list")]*)
|
neuper@37906
|
370 |
=>()
|
neuper@37906
|
371 |
| _ => raise error "calchead.sml match_ags copy-named dropped --------";
|
neuper@37906
|
372 |
|
neuper@37906
|
373 |
|
neuper@37906
|
374 |
val stac as Const ("Script.SubProblem",_) $
|
neuper@37906
|
375 |
(Const ("Pair",_) $
|
neuper@37906
|
376 |
Free (dI',_) $
|
neuper@37906
|
377 |
(Const ("Pair",_) $ pI' $ mI')) $ ags' =
|
neuper@37906
|
378 |
(*...copied from stac2tac_*)
|
neuper@37906
|
379 |
str2term
|
neuper@37906
|
380 |
"SubProblem (EqSystem_, [linear, system], [no_met])\
|
neuper@37984
|
381 |
\ [REAL_LIST [c, c_2]]";
|
neuper@37906
|
382 |
val ags = isalist2list ags';
|
neuper@37906
|
383 |
val pI = ["linear","system"];
|
neuper@37906
|
384 |
val pats = (#ppc o get_pbt) pI;
|
neuper@37906
|
385 |
case ((match_ags Isac.thy pats ags)
|
neuper@37906
|
386 |
handle TYPE _ => []) of
|
neuper@37906
|
387 |
[] => match_ags_msg pI stac ags
|
neuper@37906
|
388 |
| _ => raise error "calchead.sml match_ags 1st arg missing --------";
|
neuper@37906
|
389 |
|
neuper@37906
|
390 |
(*
|
neuper@37906
|
391 |
use"../smltest/ME/calchead.sml";
|
neuper@37906
|
392 |
*)
|
neuper@37906
|
393 |
|
neuper@37906
|
394 |
val stac as Const ("Script.SubProblem",_) $
|
neuper@37906
|
395 |
(Const ("Pair",_) $
|
neuper@37906
|
396 |
Free (dI',_) $
|
neuper@37906
|
397 |
(Const ("Pair",_) $ pI' $ mI')) $ ags' =
|
neuper@37906
|
398 |
(*...copied from stac2tac_*)
|
neuper@37906
|
399 |
str2term
|
neuper@37906
|
400 |
"SubProblem (Test_,[univariate,equation,test],\
|
neuper@37984
|
401 |
\ [no_met]) [BOOL (x+1=2), REAL x]";
|
neuper@37906
|
402 |
val ags = isalist2list ags';
|
neuper@37906
|
403 |
val pI = ["univariate","equation","test"];
|
neuper@37906
|
404 |
val pats = (#ppc o get_pbt) pI;
|
neuper@37906
|
405 |
case match_ags Isac.thy pats ags of
|
neuper@37906
|
406 |
[(1, [1], "#Given",
|
neuper@37906
|
407 |
Const ("Descript.equality", _),
|
neuper@37906
|
408 |
[Const ("op =", _) $ (Const ("op +", _) $ Free ("x", _) $ _) $ _]),
|
neuper@37906
|
409 |
(2, [1], "#Given", Const ("Descript.solveFor", _), [Free ("x", _)]),
|
neuper@37906
|
410 |
(3, [1], "#Find", Const ("Descript.solutions", _), [Free ("x_i", _)])]
|
neuper@37906
|
411 |
(* type of Find: [Free ("x_i", "bool List.list")]*)
|
neuper@37906
|
412 |
=> ()
|
neuper@37906
|
413 |
| _ => raise error "calchead.sml match_ags [univariate,equation,test]--";
|