neuper@38036
|
1 |
(* Title: tests on calchead.sml
|
neuper@38036
|
2 |
Author: Walther Neuper 051013,
|
neuper@37906
|
3 |
(c) due to copyright terms
|
neuper@37906
|
4 |
|
neuper@38011
|
5 |
12345678901234567890123456789012345678901234567890123456789012345678901234567890
|
neuper@38011
|
6 |
10 20 30 40 50 60 70 80
|
neuper@37906
|
7 |
*)
|
neuper@37906
|
8 |
|
neuper@38010
|
9 |
"--------------------------------------------------------";
|
neuper@38010
|
10 |
"table of contents --------------------------------------";
|
neuper@38010
|
11 |
"--------------------------------------------------------";
|
neuper@38010
|
12 |
"--------- get_interval after replace} other 2 ----------";
|
neuper@38010
|
13 |
"--------- maximum example with 'specify' ---------------";
|
neuper@38010
|
14 |
"--------- maximum example with 'specify', fmz <> [] ----";
|
neuper@38010
|
15 |
"--------- maximum example with 'specify', fmz = [] -----";
|
neuper@38010
|
16 |
"--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
|
neuper@38010
|
17 |
"--------- regression test fun is_copy_named ------------";
|
neuper@38011
|
18 |
"--------- regr.test fun cpy_nam ------------------------";
|
neuper@38051
|
19 |
"--------- check specify phase --------------------------";
|
neuper@38010
|
20 |
"--------------------------------------------------------";
|
neuper@38010
|
21 |
"--------------------------------------------------------";
|
neuper@38010
|
22 |
"--------------------------------------------------------";
|
neuper@38009
|
23 |
|
neuper@38036
|
24 |
(*========== inhibit exn =======================================================
|
neuper@38011
|
25 |
"--------- get_interval after replace} other 2 ----------";
|
neuper@38011
|
26 |
"--------- get_interval after replace} other 2 ----------";
|
neuper@38011
|
27 |
"--------- get_interval after replace} other 2 ----------";
|
neuper@38011
|
28 |
states := [];
|
neuper@41970
|
29 |
CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
|
neuper@41970
|
30 |
("Test", ["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@38031
|
46 |
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@38031
|
52 |
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@38058
|
74 |
("DiffApp",["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@38031
|
99 |
then 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@38031
|
120 |
then 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@38031
|
127 |
then 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@38031
|
139 |
then 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@38031
|
147 |
then 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@38058
|
168 |
("DiffApp",["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@38031
|
205 |
then 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@38058
|
211 |
(*val nxt = Specify_Theory "DiffApp" : 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@38058
|
221 |
(*val nxt = Specify_Method ("DiffApp","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@38058
|
237 |
(*val nxt = Apply_Method ("DiffApp","max_by_calculus") *)
|
neuper@37906
|
238 |
if nxt<>(Apply_Method ["DiffApp","max_by_calculus"])
|
neuper@38031
|
239 |
then 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@38058
|
257 |
val nxt = Specify_Theory "DiffApp";
|
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@38031
|
287 |
then 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@38058
|
316 |
if nxt<>(Apply_Method ("DiffApp","max_by_calculus"))
|
neuper@38031
|
317 |
then 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@38058
|
322 |
val nxt = Apply_Method ("DiffApp","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@38036
|
326 |
============ inhibit exn =====================================================*)
|
neuper@37906
|
327 |
|
neuper@38051
|
328 |
(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
|
neuper@38051
|
329 |
|
neuper@38011
|
330 |
"--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
|
neuper@38011
|
331 |
"--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
|
neuper@38011
|
332 |
"--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
|
neuper@37906
|
333 |
val Const ("Script.SubProblem",_) $
|
neuper@41972
|
334 |
(Const ("Product_Type.Pair",_) $
|
neuper@37906
|
335 |
Free (dI',_) $
|
neuper@41972
|
336 |
(Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
|
neuper@37906
|
337 |
(*...copied from stac2tac_*)
|
neuper@38011
|
338 |
str2term (
|
neuper@38011
|
339 |
"SubProblem (EqSystem', [linear, system], [no_met]) " ^
|
neuper@38011
|
340 |
" [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^
|
neuper@38011
|
341 |
" REAL_LIST [c, c_2]]");
|
neuper@37906
|
342 |
val ags = isalist2list ags';
|
neuper@37906
|
343 |
val pI = ["linear","system"];
|
neuper@37906
|
344 |
val pats = (#ppc o get_pbt) pI;
|
neuper@38011
|
345 |
"-a1-----------------------------------------------------";
|
neuper@38011
|
346 |
(*match_ags = fn : theory -> pat list -> term list -> ori list*)
|
neuper@38011
|
347 |
val xxx = match_ags (theory "EqSystem") pats ags;
|
neuper@38011
|
348 |
"-a2-----------------------------------------------------";
|
neuper@38011
|
349 |
case match_ags (theory "Isac") pats ags of
|
neuper@37906
|
350 |
[(1, [1], "#Given", Const ("Descript.equalities", _), _),
|
neuper@37906
|
351 |
(2, [1], "#Given", Const ("EqSystem.solveForVars", _),
|
neuper@37906
|
352 |
[ _ $ Free ("c", _) $ _, _ $ Free ("c_2", _) $ _]),
|
neuper@38011
|
353 |
(3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])]
|
neuper@37906
|
354 |
=>()
|
neuper@38031
|
355 |
| _ => error "calchead.sml match_ags 2 args Nok ----------------";
|
neuper@37906
|
356 |
|
neuper@37906
|
357 |
|
neuper@38011
|
358 |
"-b------------------------------------------------------";
|
neuper@37906
|
359 |
val Const ("Script.SubProblem",_) $
|
neuper@41972
|
360 |
(Const ("Product_Type.Pair",_) $
|
neuper@37906
|
361 |
Free (dI',_) $
|
neuper@41972
|
362 |
(Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
|
neuper@37906
|
363 |
(*...copied from stac2tac_*)
|
neuper@38011
|
364 |
str2term (
|
neuper@38011
|
365 |
"SubProblem (EqSystem', [linear, system], [no_met]) " ^
|
neuper@38011
|
366 |
" [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^
|
neuper@38011
|
367 |
" REAL_LIST [c, c_2], BOOL_LIST ss''']");
|
neuper@37906
|
368 |
val ags = isalist2list ags';
|
neuper@37906
|
369 |
val pI = ["linear","system"];
|
neuper@37906
|
370 |
val pats = (#ppc o get_pbt) pI;
|
neuper@38011
|
371 |
"-b1-----------------------------------------------------";
|
neuper@38011
|
372 |
val xxx = match_ags (theory "Isac") pats ags;
|
neuper@38011
|
373 |
"-b2-----------------------------------------------------";
|
neuper@38011
|
374 |
case match_ags (theory "EqSystem") pats ags of
|
neuper@37906
|
375 |
[(1, [1], "#Given", Const ("Descript.equalities", _), _),
|
neuper@37906
|
376 |
(2, [1], "#Given", Const ("EqSystem.solveForVars", _),
|
neuper@37906
|
377 |
[_ $ Free ("c", _) $ _,
|
neuper@37906
|
378 |
_ $ Free ("c_2", _) $ _]),
|
neuper@38011
|
379 |
(3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])]
|
neuper@38011
|
380 |
(* type of Find: [Free ("ss'''", "bool List.list")]*)
|
neuper@37906
|
381 |
=>()
|
neuper@38031
|
382 |
| _ => error "calchead.sml match_ags copy-named dropped --------";
|
neuper@37906
|
383 |
|
neuper@37906
|
384 |
|
neuper@38011
|
385 |
"-c---ERROR case: stac is missing #Given equalities e_s--";
|
neuper@37906
|
386 |
val stac as Const ("Script.SubProblem",_) $
|
neuper@41972
|
387 |
(Const ("Product_Type.Pair",_) $
|
neuper@37906
|
388 |
Free (dI',_) $
|
neuper@41972
|
389 |
(Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
|
neuper@37906
|
390 |
(*...copied from stac2tac_*)
|
neuper@38011
|
391 |
str2term (
|
neuper@38011
|
392 |
"SubProblem (EqSystem', [linear, system], [no_met]) " ^
|
neuper@38011
|
393 |
" [REAL_LIST [c, c_2]]");
|
neuper@38011
|
394 |
val ags = isalist2list ags';
|
neuper@37906
|
395 |
val pI = ["linear","system"];
|
neuper@37906
|
396 |
val pats = (#ppc o get_pbt) pI;
|
neuper@38051
|
397 |
(*---inhibit exn provided by this testcase--------------------------
|
neuper@38051
|
398 |
val xxx - match_ags (theory "EqSystem") pats ags;
|
neuper@38051
|
399 |
-------------------------------------------------------------------*)
|
neuper@38011
|
400 |
"-c1-----------------------------------------------------";
|
neuper@38011
|
401 |
"--------------------------step through code match_ags---";
|
neuper@38011
|
402 |
val (thy, pbt:pat list, ags) = (theory "EqSystem", pats, ags);
|
neuper@38011
|
403 |
fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
|
neuper@38011
|
404 |
val pbt' = filter_out is_copy_named pbt; (*=equalities, solveForVars*)
|
neuper@38011
|
405 |
val cy = filter is_copy_named pbt; (*=solution*)
|
neuper@38051
|
406 |
(*---inhibit exn provided by this testcase--------------------------
|
neuper@38051
|
407 |
val oris' - matc thy pbt' ags [];
|
neuper@38051
|
408 |
-------------------------------------------------------------------*)
|
neuper@38011
|
409 |
"-------------------------------step through code matc---";
|
neuper@38011
|
410 |
val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt', ags, []);
|
neuper@38011
|
411 |
(is_copy_named_idstr o free2str) t;
|
neuper@38011
|
412 |
"---if False:...";
|
neuper@38051
|
413 |
(*---inhibit exn provided by this testcase--------------------------
|
neuper@38051
|
414 |
val opt - mtc thy p a;
|
neuper@38051
|
415 |
-------------------------------------------------------------------*)
|
neuper@38011
|
416 |
"--------------------------------step through code mtc---";
|
neuper@38051
|
417 |
val (thy, (str, (dsc, _)):pat, ty $ var) - (thy, p, a);
|
neuper@38011
|
418 |
cterm_of;
|
neuper@38051
|
419 |
val ttt - (dsc $ var);
|
neuper@38051
|
420 |
(*---inhibit exn provided by this testcase--------------------------
|
neuper@38011
|
421 |
cterm_of thy (dsc $ var);
|
neuper@38051
|
422 |
-------------------------------------------------------------------*)
|
neuper@38011
|
423 |
"-------------------------------------step through end---";
|
neuper@38011
|
424 |
|
neuper@38011
|
425 |
case ((match_ags (theory "EqSystem") pats ags)
|
neuper@38011
|
426 |
handle ERROR _ => []) of (*why not TYPE ?WN100920*)
|
neuper@37906
|
427 |
[] => match_ags_msg pI stac ags
|
neuper@38031
|
428 |
| _ => error "calchead.sml match_ags 1st arg missing --------";
|
neuper@37906
|
429 |
|
neuper@37906
|
430 |
|
neuper@38011
|
431 |
"-d------------------------------------------------------";
|
neuper@37906
|
432 |
val stac as Const ("Script.SubProblem",_) $
|
neuper@41972
|
433 |
(Const ("Product_Type.Pair",_) $
|
neuper@37906
|
434 |
Free (dI',_) $
|
neuper@41972
|
435 |
(Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
|
neuper@37906
|
436 |
(*...copied from stac2tac_*)
|
neuper@38011
|
437 |
str2term (
|
neuper@38011
|
438 |
"SubProblem (Test',[univariate,equation,test]," ^
|
neuper@38011
|
439 |
" [no_met]) [BOOL (x+1=2), REAL x]");
|
neuper@38011
|
440 |
val AGS = isalist2list ags';
|
neuper@37906
|
441 |
val pI = ["univariate","equation","test"];
|
neuper@38011
|
442 |
val PATS = (#ppc o get_pbt) pI;
|
neuper@38011
|
443 |
"-d1-----------------------------------------------------";
|
neuper@38011
|
444 |
"--------------------------step through code match_ags---";
|
neuper@38011
|
445 |
val (thy, pbt:pat list, ags) = (theory "Test", PATS, AGS);
|
neuper@38011
|
446 |
fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
|
neuper@38011
|
447 |
val pbt' = filter_out is_copy_named pbt;
|
neuper@38011
|
448 |
val cy = filter is_copy_named pbt;
|
neuper@38011
|
449 |
val oris' = matc thy pbt' ags [];
|
neuper@38011
|
450 |
"-------------------------------step through code matc---";
|
neuper@38011
|
451 |
val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt', ags, []);
|
neuper@38011
|
452 |
(is_copy_named_idstr o free2str) t;
|
neuper@38011
|
453 |
"---if False:...";
|
neuper@38011
|
454 |
val opt = mtc thy p a;
|
neuper@38011
|
455 |
"--------------------------------step through code mtc---";
|
neuper@38011
|
456 |
val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
|
neuper@38011
|
457 |
val ttt = (dsc $ var);
|
neuper@38011
|
458 |
cterm_of thy (dsc $ var);
|
neuper@38011
|
459 |
val ori = ((([1], str, dsc, (*[var]*) split_dts' (dsc, var))): preori);
|
neuper@38011
|
460 |
|
neuper@38011
|
461 |
"-d2-----------------------------------------------------";
|
neuper@38011
|
462 |
pbt = []; (*false*)
|
neuper@38011
|
463 |
"-------------------------------step through code matc---";
|
neuper@38011
|
464 |
val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt, ags, oris @ [ori]);
|
neuper@38011
|
465 |
(is_copy_named_idstr o free2str) t;
|
neuper@38011
|
466 |
"---if False:...";
|
neuper@38011
|
467 |
val opt = mtc thy p a;
|
neuper@38011
|
468 |
"--------------------------------step through code mtc---";
|
neuper@38011
|
469 |
val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
|
neuper@38011
|
470 |
val ttt = (dsc $ var);
|
neuper@38011
|
471 |
cterm_of thy (dsc $ var);
|
neuper@38011
|
472 |
val ori = ((([1], str, dsc, (*[var]*) split_dts' (dsc, var))): preori);
|
neuper@38011
|
473 |
"-d3-----------------------------------------------------";
|
neuper@38011
|
474 |
pbt = []; (*true, base case*)
|
neuper@38011
|
475 |
"-----------------continue step through code match_ags---";
|
neuper@38011
|
476 |
val oris' = oris @ [ori]; (*result 2 oris, cpy_nam added later*)
|
neuper@38011
|
477 |
"--------------------------------step through cpy_nam----";
|
neuper@38011
|
478 |
val (pbt, oris, p as (field, (dsc, t)):pat) = (pbt', oris', hd cy);
|
neuper@38011
|
479 |
(*t = "v_v'i'" : term OLD: t = "v_i_"*)
|
neuper@38011
|
480 |
"--------------------------------------------------------";
|
neuper@38011
|
481 |
fun is_copy_named_generating_idstr str =
|
neuper@38011
|
482 |
if is_copy_named_idstr str
|
neuper@38011
|
483 |
then case (rev o explode) str of
|
neuper@38011
|
484 |
(*"_"::"_"::"_"::_ => false*)
|
neuper@38011
|
485 |
"'"::"'"::"'"::_ => false
|
neuper@38011
|
486 |
| _ => true
|
neuper@38011
|
487 |
else false;
|
neuper@38011
|
488 |
fun is_copy_named_generating (_, (_, t)) =
|
neuper@38011
|
489 |
(is_copy_named_generating_idstr o free2str) t;
|
neuper@38011
|
490 |
"--------------------------------------------------------";
|
neuper@38011
|
491 |
is_copy_named_generating p (*true*);
|
neuper@38011
|
492 |
fun sel (_,_,d,ts) = comp_ts (d, ts);
|
neuper@38011
|
493 |
val cy' = (implode o (drop_last_n 3) o explode o free2str) t;
|
neuper@38011
|
494 |
(*"v_v" OLD: "v_"*)
|
neuper@38011
|
495 |
val ext = (last_elem o drop_last o explode o free2str) t;
|
neuper@38011
|
496 |
(*"i" OLD: "i"*)
|
neuper@38011
|
497 |
val vars' = map (free2str o snd o snd) pbt(*cpy-nam filtered_out*);
|
neuper@38011
|
498 |
(*["e_e", "v_v"] OLD: ["e_", "v_"]*)
|
neuper@38011
|
499 |
val vals = map sel oris;
|
neuper@38011
|
500 |
(*[x+1=2, x] OLD: [x+1=2, x] : term list*)
|
neuper@38011
|
501 |
vars' ~~ vals;
|
neuper@38011
|
502 |
(*[("e_e", [x+1=2), ("v_v", x)] OLD: [("e_", [x+1=2), ("v_", x)]*)
|
neuper@38011
|
503 |
(assoc (vars'~~vals, cy'));
|
neuper@38032
|
504 |
(*SOME (Free ("x", "RealDef.real")) : term option*)
|
neuper@38011
|
505 |
val cy_ext = (free2str o the) (assoc (vars'~~vals, cy'))^"_"^ext;
|
neuper@38011
|
506 |
(*x_i*)
|
neuper@38011
|
507 |
"-----------------continue step through code match_ags---";
|
neuper@38011
|
508 |
val cy' = map (cpy_nam pbt' oris') cy;
|
neuper@38011
|
509 |
(*[([1], "#Find", "solutions, [x_i"] (*as terms*) )]*)
|
neuper@38011
|
510 |
"-------------------------------------step through end---";
|
neuper@38011
|
511 |
|
neuper@38011
|
512 |
case match_ags thy PATS AGS of
|
neuper@38011
|
513 |
[(1, [1], "#Given", Const ("Descript.equality", _),
|
neuper@41922
|
514 |
[Const ("HOL.eq", _) $ (Const ("Groups.plus_class.plus", _) $
|
neuper@38011
|
515 |
Free ("x", _) $ Free ("1", _)) $ Free ("2", _)]),
|
neuper@38011
|
516 |
(2, [1], "#Given", Const ("Descript.solveFor", _), [Free ("x", _)]),
|
neuper@38011
|
517 |
(3, [1], "#Find", Const ("Descript.solutions", _), [Free ("x_i", _)])]
|
neuper@37906
|
518 |
=> ()
|
neuper@38031
|
519 |
| _ => error "calchead.sml match_ags [univariate,equation,test]--";
|
neuper@38009
|
520 |
|
neuper@38010
|
521 |
|
neuper@38010
|
522 |
"--------- regression test fun is_copy_named ------------";
|
neuper@38010
|
523 |
"--------- regression test fun is_copy_named ------------";
|
neuper@38010
|
524 |
"--------- regression test fun is_copy_named ------------";
|
neuper@38010
|
525 |
val trm = (1, (2, @{term "v'i'"}));
|
neuper@38031
|
526 |
if is_copy_named trm then () else error "regr. is_copy_named 1";
|
neuper@38010
|
527 |
val trm = (1, (2, @{term "e_e"}));
|
neuper@38031
|
528 |
if is_copy_named trm then error "regr. is_copy_named 2" else ();
|
neuper@38010
|
529 |
val trm = (1, (2, @{term "L'''"}));
|
neuper@38031
|
530 |
if is_copy_named trm then () else error "regr. is_copy_named 3";
|
neuper@38010
|
531 |
|
neuper@38010
|
532 |
(* out-comment 'structure CalcHead'...
|
neuper@38010
|
533 |
val trm = (1, (2, @{term "v'i'"}));
|
neuper@38031
|
534 |
if is_copy_named_generating trm then () else error "regr. is_copy_named";
|
neuper@38010
|
535 |
val trm = (1, (2, @{term "L'''"}));
|
neuper@38031
|
536 |
if is_copy_named_generating trm then error "regr. is_copy_named" else ();
|
neuper@38010
|
537 |
*)
|
neuper@38011
|
538 |
|
neuper@38011
|
539 |
"--------- regr.test fun cpy_nam ------------------------";
|
neuper@38011
|
540 |
"--------- regr.test fun cpy_nam ------------------------";
|
neuper@38011
|
541 |
"--------- regr.test fun cpy_nam ------------------------";
|
neuper@38011
|
542 |
(*data from above - match_ags, is_cp, cpy_nam +with EqSystem (!)-:*)
|
neuper@38011
|
543 |
(*the model-pattern, is_copy_named are filter_out*)
|
neuper@38011
|
544 |
pbt = [("#Given", (@{term "equality"}, @{term "e_e :: bool"})),
|
neuper@38011
|
545 |
("#Given", (@{term "solveFor"}, @{term "v_v :: real"} ))];
|
neuper@38011
|
546 |
(*the model specific for an example*)
|
neuper@38011
|
547 |
oris = [([1], "#Given", @{term "equality"} , [str2term "x+1= 2"]),
|
neuper@38011
|
548 |
([1], "#Given", @{term "solveFor"} , [@{term "x :: real"} ])];
|
neuper@38011
|
549 |
cy = [("#Find", (@{term "solutions"}, @{term "v_v'i' :: bool list"}))];
|
neuper@38011
|
550 |
(*...all must be true*)
|
neuper@38011
|
551 |
|
neuper@38011
|
552 |
case cpy_nam pbt oris (hd cy) of
|
neuper@38011
|
553 |
([1], "#Find", Const ("Descript.solutions", _), [Free ("x_i", _)]) => ()
|
neuper@38031
|
554 |
| _ => error "calchead.sml regr.test cpy_nam-1-";
|
neuper@38011
|
555 |
|
neuper@38011
|
556 |
(*new data: cpy_nam without changing the name*)
|
neuper@38011
|
557 |
@{term "equalities"}; type_of @{term "[x_1+1=2,x_2=0]"};
|
neuper@38011
|
558 |
@{term "solveForVars"}; type_of @{term "[x_1,x_2]::real list"};
|
neuper@38011
|
559 |
@{term "solution"}; type_of @{term "ss''' :: bool list"};
|
neuper@38011
|
560 |
(*the model-pattern for ["linear", "system"], is_copy_named are filter_out*)
|
neuper@38011
|
561 |
val pbt = [("#Given", (@{term "equalities"}, @{term "e_s :: bool list"})),
|
neuper@38011
|
562 |
("#Given", (@{term "solveForVars v_s"}, @{term "v_s :: bool list"} ))];
|
neuper@38011
|
563 |
(*the model specific for an example*)
|
neuper@38011
|
564 |
val oris = [([1], "#Given", @{term "equalities"} ,[str2term "[x_1+1=2,x_2=0]"]),
|
neuper@38011
|
565 |
([1], "#Given", @{term "solveForVars"} , [@{term "[x_1,x_2]::real list"}])];
|
neuper@38011
|
566 |
val cy = [("#Find", (@{term "solution"}, @{term "ss''' :: bool list"}))
|
neuper@38011
|
567 |
(*could be more than 1*)];
|
neuper@38011
|
568 |
|
neuper@38011
|
569 |
case cpy_nam pbt oris (hd cy) of
|
neuper@38011
|
570 |
([1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)]) => ()
|
neuper@38031
|
571 |
| _ => error "calchead.sml regr.test cpy_nam-2-";
|
neuper@38051
|
572 |
|
neuper@38051
|
573 |
-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
|
neuper@38051
|
574 |
|
neuper@38051
|
575 |
|
neuper@38051
|
576 |
"--------- check specify phase --------------------------";
|
neuper@38051
|
577 |
"--------- check specify phase --------------------------";
|
neuper@38051
|
578 |
"--------- check specify phase --------------------------";
|
neuper@38051
|
579 |
(*val fmz = ["functionTerm (x^^^2 + 1)",*)
|
neuper@38051
|
580 |
val fmz = ["functionTerm (x + 1)",
|
neuper@38051
|
581 |
"integrateBy x","antiDerivative FF"];
|
neuper@38051
|
582 |
val (dI',pI',mI') =
|
neuper@38051
|
583 |
("Integrate",["integrate","function"],
|
neuper@38051
|
584 |
["diff","integration"]);
|
neuper@38051
|
585 |
val p = e_pos'; val c = [];
|
neuper@38051
|
586 |
"--- step 1 --";
|
neuper@38051
|
587 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@38051
|
588 |
(*> val it = "--- step 1 --" : string
|
neuper@38051
|
589 |
val f =
|
neuper@38051
|
590 |
Form'
|
neuper@38051
|
591 |
(PpcKF
|
neuper@38051
|
592 |
(0, EdUndef, 0, Nundef,
|
neuper@38051
|
593 |
(Problem [],
|
neuper@38051
|
594 |
{Find = [], With = [], Given = [], Where = [], Relate = []})))
|
neuper@38051
|
595 |
: mout
|
neuper@38051
|
596 |
val nxt = ("Model_Problem", Model_Problem) : string * tac
|
neuper@38051
|
597 |
val p = ([], Pbl) : pos'
|
neuper@38051
|
598 |
val pt =
|
neuper@38051
|
599 |
Nd (PblObj
|
neuper@38051
|
600 |
{env = None, fmz =
|
neuper@38051
|
601 |
(["functionTerm (x^^^2 + 1)", "integrateBy x",
|
neuper@38051
|
602 |
"antiDerivative FF"],
|
neuper@38058
|
603 |
("Integrate", ["integrate", "function"],
|
neuper@38051
|
604 |
["diff", "integration"])),
|
neuper@38051
|
605 |
loc =
|
neuper@38051
|
606 |
(Some (ScrState ([], [], None, Const ("empty", "'a"), Sundef, false)),
|
neuper@38051
|
607 |
None),
|
neuper@38051
|
608 |
cell = None, meth = [], spec = ("e_domID", ["e_pblID"], ["e_metID"]),
|
neuper@38051
|
609 |
probl = [], branch = TransitiveB,
|
neuper@38051
|
610 |
origin =
|
neuper@38051
|
611 |
([(1, [1], "#Given",
|
neuper@38051
|
612 |
Const ("Descript.functionTerm", "RealDef.real => Tools.una"),
|
neuper@38051
|
613 |
[Const ("op +",
|
neuper@38051
|
614 |
"[RealDef.real, RealDef.real] => RealDef.real") $
|
neuper@38051
|
615 |
(Const ("Atools.pow",
|
neuper@38051
|
616 |
"[RealDef.real, RealDef.real] => RealDef.real") $
|
neuper@38051
|
617 |
Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $
|
neuper@38051
|
618 |
Free ("1", "RealDef.real")]),
|
neuper@38051
|
619 |
(2, [1], "#Given",
|
neuper@38051
|
620 |
Const ("Integrate.integrateBy", "RealDef.real => Tools.una"),
|
neuper@38051
|
621 |
[Free ("x", "RealDef.real")]),
|
neuper@38051
|
622 |
(3, [1], "#Find",
|
neuper@38051
|
623 |
Const ("Integrate.antiDerivative", "RealDef.real => Tools.una"),
|
neuper@38051
|
624 |
[Free ("FF", "RealDef.real")])],
|
neuper@38058
|
625 |
("Integrate", ["integrate", "function"], ["diff", "integration"]),
|
neuper@38051
|
626 |
Const ("Integrate.Integrate",
|
neuper@38051
|
627 |
"(RealDef.real, RealDef.real) * => RealDef.real") $
|
neuper@41972
|
628 |
(Const ("Product_Type.Pair",
|
neuper@38051
|
629 |
"[RealDef.real, RealDef.real]
|
neuper@38051
|
630 |
=> (RealDef.real, RealDef.real) *") $
|
neuper@38051
|
631 |
(Const ("op +",
|
neuper@38051
|
632 |
"[RealDef.real, RealDef.real] => RealDef.real") $
|
neuper@38051
|
633 |
(Const ("Atools.pow",
|
neuper@38051
|
634 |
"[RealDef.real, RealDef.real] => RealDef.real") $
|
neuper@38051
|
635 |
Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $
|
neuper@38051
|
636 |
Free ("1", "RealDef.real")) $
|
neuper@38051
|
637 |
Free ("x", "RealDef.real"))),
|
neuper@38051
|
638 |
ostate = Incomplete, result = (Const ("empty", "'a"), [])},
|
neuper@38051
|
639 |
[]) : ptree*)
|
neuper@38051
|
640 |
"----- WN101007 worked until here (checked same as isac2002) ---";
|
neuper@38055
|
641 |
if nxt = ("Model_Problem", Model_Problem) then ()
|
neuper@38055
|
642 |
else error "clchead.sml: check specify phase step 1";
|
neuper@38051
|
643 |
"--- step 2 --";
|
neuper@38051
|
644 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; (*Florian: see response buffer, top*)
|
neuper@38051
|
645 |
(*val it = "--- step 2 --" : string
|
neuper@38051
|
646 |
val p = ([], Pbl) : pos'
|
neuper@38051
|
647 |
val f =
|
neuper@38051
|
648 |
Form'
|
neuper@38051
|
649 |
(PpcKF
|
neuper@38051
|
650 |
(0, EdUndef, 0, Nundef,
|
neuper@38051
|
651 |
(Problem [],
|
neuper@38051
|
652 |
{Find = [Incompl "Integrate.antiDerivative"],
|
neuper@38051
|
653 |
With = [],
|
neuper@38051
|
654 |
Given = [Incompl "functionTerm", Incompl "integrateBy"],
|
neuper@38051
|
655 |
Where = [],
|
neuper@38051
|
656 |
Relate = []}))) : mout
|
neuper@38051
|
657 |
val nxt = ("Add_Given", Add_Given "functionTerm (x ^^^ 2 + 1)") : tac'_
|
neuper@38051
|
658 |
val pt =
|
neuper@38051
|
659 |
Nd (PblObj
|
neuper@38051
|
660 |
{env = None, fmz =
|
neuper@38051
|
661 |
(["functionTerm (x^^^2 + 1)", "integrateBy x",
|
neuper@38051
|
662 |
"antiDerivative FF"],
|
neuper@38058
|
663 |
("Integrate", ["integrate", "function"],
|
neuper@38051
|
664 |
["diff", "integration"])),
|
neuper@38051
|
665 |
loc =
|
neuper@38051
|
666 |
(Some
|
neuper@38051
|
667 |
(ScrState ([], [], None, Const ("empty", "'a"), Sundef, false)),
|
neuper@38051
|
668 |
None),
|
neuper@38051
|
669 |
cell = None, meth = [], spec =
|
neuper@38051
|
670 |
("e_domID", ["e_pblID"], ["e_metID"]), probl =
|
neuper@38051
|
671 |
[(0, [], false, "#Given",
|
neuper@38051
|
672 |
Inc ((Const ("Descript.functionTerm",
|
neuper@38051
|
673 |
"RealDef.real => Tools.una"),[]),
|
neuper@38051
|
674 |
(Const ("empty", "'a"), []))),
|
neuper@38051
|
675 |
(0, [], false, "#Given",
|
neuper@38051
|
676 |
Inc ((Const ("Integrate.integrateBy",
|
neuper@38051
|
677 |
"RealDef.real => Tools.una"),[]),
|
neuper@38051
|
678 |
(Const ("empty", "'a"), []))),
|
neuper@38051
|
679 |
(0, [], false, "#Find",
|
neuper@38051
|
680 |
Inc ((Const ("Integrate.antiDerivative",
|
neuper@38051
|
681 |
"RealDef.real => Tools.una"),[]),
|
neuper@38051
|
682 |
(Const ("empty", "'a"), [])))],
|
neuper@38051
|
683 |
branch = TransitiveB, origin =
|
neuper@38051
|
684 |
([(1, [1], "#Given",
|
neuper@38051
|
685 |
Const ("Descript.functionTerm", "RealDef.real => Tools.una"),
|
neuper@38051
|
686 |
[Const ("op +",
|
neuper@38051
|
687 |
"[RealDef.real, RealDef.real] => RealDef.real") $
|
neuper@38051
|
688 |
(Const ("Atools.pow",
|
neuper@38051
|
689 |
"[RealDef.real, RealDef.real] => RealDef.real") $
|
neuper@38051
|
690 |
Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $
|
neuper@38051
|
691 |
Free ("1", "RealDef.real")]),
|
neuper@38051
|
692 |
(2, [1], "#Given",
|
neuper@38051
|
693 |
Const ("Integrate.integrateBy", "RealDef.real => Tools.una"),
|
neuper@38051
|
694 |
[Free ("x", "RealDef.real")]),
|
neuper@38051
|
695 |
(3, [1], "#Find",
|
neuper@38051
|
696 |
Const ("Integrate.antiDerivative", "RealDef.real => Tools.una"),
|
neuper@38051
|
697 |
[Free ("FF", "RealDef.real")])],
|
neuper@38058
|
698 |
("Integrate", ["integrate", "function"], ["diff", "integration"]),
|
neuper@38051
|
699 |
Const ("Integrate.Integrate",
|
neuper@38051
|
700 |
"(RealDef.real, RealDef.real) * => RealDef.real") $
|
neuper@41972
|
701 |
(Const ("Product_Type.Pair",
|
neuper@38051
|
702 |
"[RealDef.real, RealDef.real]
|
neuper@38051
|
703 |
=> (RealDef.real, RealDef.real) *") $
|
neuper@38051
|
704 |
(Const ("op +",
|
neuper@38051
|
705 |
"[RealDef.real, RealDef.real] => RealDef.real") $
|
neuper@38051
|
706 |
(Const ("Atools.pow",
|
neuper@38051
|
707 |
"[RealDef.real, RealDef.real] => RealDef.real") $
|
neuper@38051
|
708 |
Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $
|
neuper@38051
|
709 |
Free ("1", "RealDef.real")) $
|
neuper@38051
|
710 |
Free ("x", "RealDef.real"))),
|
neuper@38051
|
711 |
ostate = Incomplete, result = (Const ("empty", "'a"), [])},
|
neuper@38051
|
712 |
[]) : ptree*)
|
neuper@38052
|
713 |
"----- WN101007 ptree checked same as isac2002, diff. in nxt --- REPAIRED";
|
neuper@38055
|
714 |
if nxt = ("Add_Given", Add_Given "functionTerm (x + 1)") then ()
|
neuper@38055
|
715 |
else error "clchead.sml: check specify phase step 2";
|
neuper@38051
|
716 |
"--- step 3 --";
|
neuper@38051
|
717 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@38055
|
718 |
"----- WN101008 ptree checked same as isac2002, diff. in nxt --- REPAIRED";
|
neuper@38055
|
719 |
if nxt = ("Add_Given", Add_Given "integrateBy x") then ()
|
neuper@38055
|
720 |
else error "clchead.sml: check specify phase step 2";
|
neuper@38055
|
721 |
|
neuper@38052
|
722 |
(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
|
neuper@38051
|
723 |
-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
|