neuper@37906
|
1 |
(* tests for sml/ME/ctree.sml
|
neuper@37906
|
2 |
authors: Walther Neuper 060113
|
neuper@37906
|
3 |
(c) due to copyright terms
|
neuper@37906
|
4 |
|
neuper@37906
|
5 |
use"../smltest/ME/ctree.sml";
|
neuper@37906
|
6 |
use"ctree.sml";
|
neuper@37906
|
7 |
*)
|
neuper@37906
|
8 |
|
neuper@37906
|
9 |
"-----------------------------------------------------------------";
|
neuper@37906
|
10 |
"table of contents -----------------------------------------------";
|
neuper@37906
|
11 |
"-----------------------------------------------------------------";
|
neuper@37906
|
12 |
"-----------------------------------------------------------------";
|
neuper@37906
|
13 |
"-------------- build miniscript stepwise BEFORE ALL TESTS -------";
|
neuper@41968
|
14 |
"-------------- check positions in miniscript --------------------";
|
neuper@37906
|
15 |
"-------------- get_allpos' (from ptree above)--------------------";
|
neuper@37906
|
16 |
(**#####################################################################(**)
|
neuper@37906
|
17 |
"-------------- cut_level (from ptree above)----------------------";
|
neuper@37906
|
18 |
"-------------- cut_tree (from ptree above)-----------------------";
|
neuper@37906
|
19 |
"=====new ptree 1a miniscript with mini-subpbl ===================";
|
neuper@37906
|
20 |
"-------------- cut_level ( ,Frm) on Incomplete Nd ---------------";
|
neuper@37906
|
21 |
(**)#####################################################################**)
|
neuper@37906
|
22 |
"=====new ptree 2 miniscript with mini-subpbl ====================";
|
neuper@37906
|
23 |
"-------------- cut_tree (intermedi.ptree: 3rd level)-------------";
|
neuper@37906
|
24 |
"-------------- cappend (from ptree above)------------------------";
|
neuper@37906
|
25 |
"-------------- cappend minisubpbl -------------------------------";
|
neuper@37906
|
26 |
|
neuper@37906
|
27 |
"=====new ptree 3 ================================================";
|
neuper@37906
|
28 |
"-------------- move_dn ------------------------------------------";
|
neuper@37906
|
29 |
"-------------- move_dn: Frm -> Res ------------------------------";
|
neuper@37906
|
30 |
"-------------- move_up ------------------------------------------";
|
neuper@37906
|
31 |
"------ move into detail -----------------------------------------";
|
neuper@37906
|
32 |
"=====new ptree 3a ===============================================";
|
neuper@37906
|
33 |
"-------------- move_dn in Incomplete ctree ----------------------";
|
neuper@37906
|
34 |
|
neuper@37906
|
35 |
"=====new ptree 4: crooked by cut_level_'_ =======================";
|
neuper@37906
|
36 |
(*############## development stopped 0501 ########################*)
|
neuper@37906
|
37 |
(******************************************************************)
|
neuper@37906
|
38 |
(* val SAVE_get_trace = get_trace; *)
|
neuper@37906
|
39 |
(******************************************************************)
|
neuper@37906
|
40 |
"-------------- get_interval from ctree: incremental development--";
|
neuper@37906
|
41 |
(******************************************************************)
|
neuper@37906
|
42 |
(* val get_trace = SAVE_get_trace; *)
|
neuper@37906
|
43 |
(******************************************************************)
|
neuper@37906
|
44 |
(*############## development stopped 0501 ########################*)
|
neuper@37906
|
45 |
|
neuper@37906
|
46 |
"=====new ptree 4 ratequation ====================================";
|
neuper@37906
|
47 |
"-------------- pt_extract form, tac, asm<>[] --------------------";
|
neuper@37906
|
48 |
"=====new ptree 5 minisubpbl =====================================";
|
neuper@37906
|
49 |
"-------------- pt_extract form, tac, asm ------------------------";
|
neuper@37906
|
50 |
|
neuper@37906
|
51 |
(**#####################################################################(**)
|
neuper@37906
|
52 |
"=====new ptree 6 minisubpbl intersteps ==========================";
|
neuper@37906
|
53 |
"-------------- get_allpos' new ----------------------------------";
|
neuper@37906
|
54 |
"-------------- cut_tree new (from ptree above)-------------------";
|
neuper@37906
|
55 |
(**)#####################################################################**)
|
neuper@37906
|
56 |
|
neuper@37906
|
57 |
"-----------------------------------------------------------------";
|
neuper@37906
|
58 |
"-----------------------------------------------------------------";
|
neuper@37906
|
59 |
"-----------------------------------------------------------------";
|
neuper@37906
|
60 |
|
neuper@37906
|
61 |
|
neuper@37906
|
62 |
"-------------- build miniscript stepwise BEFORE ALL TESTS -------";
|
neuper@37906
|
63 |
"-------------- build miniscript stepwise BEFORE ALL TESTS -------";
|
neuper@37906
|
64 |
"-------------- build miniscript stepwise BEFORE ALL TESTS -------";
|
neuper@41968
|
65 |
"this build should be detailed each time a test fails later ";
|
neuper@41968
|
66 |
"i.e. all the tests should be caught here first ";
|
neuper@41968
|
67 |
"and linked with a reference to the respective test environment ";
|
neuper@41968
|
68 |
val fmz = ["equality (x+1=(2::int))", (*FIRST OF ALL TESTS*) "solveFor x", "solutions L"];
|
neuper@41968
|
69 |
val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"],
|
neuper@41968
|
70 |
["Test","squ-equ-test-subpbl1"]);
|
neuper@41968
|
71 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@41968
|
72 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@41968
|
73 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@41968
|
74 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@41968
|
75 |
|
neuper@41968
|
76 |
|
neuper@41968
|
77 |
|
neuper@41968
|
78 |
|
neuper@41968
|
79 |
"-------------- check positions in miniscript --------------------";
|
neuper@41968
|
80 |
"-------------- check positions in miniscript --------------------";
|
neuper@41968
|
81 |
"-------------- check positions in miniscript --------------------";
|
e0726734@41957
|
82 |
val fmz = ["equality (x+1=(2::int))",
|
bonzai@41950
|
83 |
"solveFor x","solutions L"];
|
neuper@37906
|
84 |
val (dI',pI',mI') =
|
neuper@38058
|
85 |
("Test",["sqroot-test","univariate","equation","test"],
|
neuper@37906
|
86 |
["Test","squ-equ-test-subpbl1"]);
|
neuper@37906
|
87 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
bonzai@41951
|
88 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
89 |
(* nxt = Add_Given "equality (x + 1 = 2)"
|
neuper@37924
|
90 |
(writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
|
neuper@37906
|
91 |
*)
|
bonzai@41950
|
92 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37924
|
93 |
(* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
|
neuper@37906
|
94 |
*)
|
neuper@37906
|
95 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37924
|
96 |
(* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
|
neuper@37906
|
97 |
*)
|
neuper@37906
|
98 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
99 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
100 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
101 |
"ctree.sml-------------- get_allpos' new ------------------------\"";
|
neuper@37906
|
102 |
val (PP, pp) = split_last [1];
|
neuper@37906
|
103 |
val ((pt', cuts), clevup) = cut_bottom (PP, pp) (get_nd pt PP);
|
neuper@37906
|
104 |
|
neuper@37906
|
105 |
val cuts = get_allp [] ([], ([],Frm)) pt;
|
neuper@37906
|
106 |
val cuts2 = get_allps [] [1] (children pt);
|
neuper@37906
|
107 |
"ctree.sml-------------- cut_tree new (from ptree above)----------";
|
neuper@37906
|
108 |
val (pt', cuts) = cut_tree pt ([1],Frm);
|
neuper@37906
|
109 |
"ctree.sml-------------- cappend on complete ctree from above ----";
|
bonzai@41949
|
110 |
val (pt', cuts) = cappend_form pt [1] (e_istate, e_ctxt) (str2term "Inform[1]");
|
neuper@37906
|
111 |
"----------------------------------------------------------------/";
|
neuper@41938
|
112 |
(*========== inhibit exn WN110319 ==============================================
|
neuper@37906
|
113 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_form: pos =[1]*);
|
neuper@37906
|
114 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[1]*);
|
neuper@37906
|
115 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[2]*);
|
neuper@37906
|
116 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_problem: pos =[3]*);
|
neuper@37906
|
117 |
|
neuper@37906
|
118 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
119 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
120 |
(*val nxt = ("Add_Given", Add_Given "equality (-1 + x = 0)").....*)
|
neuper@37906
|
121 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
122 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
123 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
124 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
125 |
(*val nxt = ("Apply_Method", Apply_Method ["Test", "solve_linear"])*)
|
neuper@37906
|
126 |
|
neuper@37906
|
127 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_form: pos =[3,1]*);
|
neuper@37906
|
128 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[3,1]*);
|
neuper@37906
|
129 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[3,2]*);
|
neuper@37906
|
130 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*.append_result: pos =[3]*);
|
neuper@37906
|
131 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[4]*);
|
neuper@37906
|
132 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*.append_result: pos =[]*);
|
neuper@37906
|
133 |
val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
|
neuper@37906
|
134 |
if (snd nxt)=End_Proof' andalso res="[x = 1]" then ()
|
neuper@38031
|
135 |
else error "new behaviour in test: miniscript with mini-subpbl";
|
neuper@37906
|
136 |
|
neuper@37906
|
137 |
show_pt pt;
|
neuper@41938
|
138 |
============ inhibit exn WN110319 ============================================*)
|
neuper@37906
|
139 |
|
neuper@41938
|
140 |
(*=== inhibit exn ?=============================================================
|
neuper@37906
|
141 |
|
neuper@37906
|
142 |
"-------------- get_allpos' (from ptree above)--------------------";
|
neuper@37906
|
143 |
"-------------- get_allpos' (from ptree above)--------------------";
|
neuper@37906
|
144 |
"-------------- get_allpos' (from ptree above)--------------------";
|
neuper@37906
|
145 |
if get_allpos' ([], 1) pt =
|
neuper@37906
|
146 |
[([], Frm),
|
neuper@37906
|
147 |
([1], Frm),
|
neuper@37906
|
148 |
([1], Res),
|
neuper@37906
|
149 |
([2], Res),
|
neuper@37906
|
150 |
([3], Frm),
|
neuper@37906
|
151 |
([3, 1], Frm),
|
neuper@37906
|
152 |
([3, 1], Res),
|
neuper@37906
|
153 |
([3, 2], Res),
|
neuper@37906
|
154 |
([3], Res),
|
neuper@37906
|
155 |
([4], Res),
|
neuper@37906
|
156 |
([], Res)]
|
neuper@38031
|
157 |
then () else error "ctree.sml: diff:behav. in get_allpos' 1";
|
neuper@37906
|
158 |
|
neuper@37906
|
159 |
if get_allpos's ([], 1) (children pt) =
|
neuper@37906
|
160 |
[([1], Frm),
|
neuper@37906
|
161 |
([1], Res),
|
neuper@37906
|
162 |
([2], Res),
|
neuper@37906
|
163 |
([3], Frm),
|
neuper@37906
|
164 |
([3, 1], Frm),
|
neuper@37906
|
165 |
([3, 1], Res),
|
neuper@37906
|
166 |
([3, 2], Res),
|
neuper@37906
|
167 |
([3], Res),
|
neuper@37906
|
168 |
([4], Res)]
|
neuper@38031
|
169 |
then () else error "ctree.sml: diff:behav. in get_allpos' 2";
|
neuper@37906
|
170 |
|
neuper@37906
|
171 |
if get_allpos's ([], 2) (takerest (1, children pt)) =
|
neuper@37906
|
172 |
[([2], Res),
|
neuper@37906
|
173 |
([3], Frm),
|
neuper@37906
|
174 |
([3, 1], Frm),
|
neuper@37906
|
175 |
([3, 1], Res),
|
neuper@37906
|
176 |
([3, 2], Res),
|
neuper@37906
|
177 |
([3], Res),
|
neuper@37906
|
178 |
([4], Res)]
|
neuper@38031
|
179 |
then () else error "ctree.sml: diff:behav. in get_allpos' 3";
|
neuper@37906
|
180 |
|
neuper@37906
|
181 |
if get_allpos's ([], 3) (takerest (2, children pt)) =
|
neuper@37906
|
182 |
[([3], Frm),
|
neuper@37906
|
183 |
([3, 1], Frm),
|
neuper@37906
|
184 |
([3, 1], Res),
|
neuper@37906
|
185 |
([3, 2], Res),
|
neuper@37906
|
186 |
([3], Res),
|
neuper@37906
|
187 |
([4], Res)]
|
neuper@38031
|
188 |
then () else error "ctree.sml: diff:behav. in get_allpos' 4";
|
neuper@37906
|
189 |
|
neuper@37906
|
190 |
if get_allpos's ([3], 1) (children (nth 3 (children pt))) =
|
neuper@37906
|
191 |
[([3, 1], Frm),
|
neuper@37906
|
192 |
([3, 1], Res),
|
neuper@37906
|
193 |
([3, 2], Res)]
|
neuper@38031
|
194 |
then () else error "ctree.sml: diff:behav. in get_allpos' 5";
|
neuper@37906
|
195 |
|
neuper@37906
|
196 |
if get_allpos' ([3], 1) (nth 3 (children pt)) =
|
neuper@37906
|
197 |
[([3], Frm),
|
neuper@37906
|
198 |
([3, 1], Frm),
|
neuper@37906
|
199 |
([3, 1], Res),
|
neuper@37906
|
200 |
([3, 2], Res),
|
neuper@37906
|
201 |
([3], Res)]
|
neuper@38031
|
202 |
then () else error "ctree.sml: diff:behav. in get_allpos' 6";
|
neuper@37906
|
203 |
|
neuper@37906
|
204 |
|
neuper@37906
|
205 |
(**##############################################################(**)
|
neuper@37906
|
206 |
|
neuper@37906
|
207 |
"-------------- cut_level (from ptree above)----------------------";
|
neuper@37906
|
208 |
"-------------- cut_level (from ptree above)----------------------";
|
neuper@37906
|
209 |
"-------------- cut_level (from ptree above)----------------------";
|
neuper@37906
|
210 |
show_pt pt;
|
neuper@37906
|
211 |
show_pt pt';
|
neuper@37906
|
212 |
print_depth 99; cuts; print_depth 3;
|
neuper@37906
|
213 |
|
neuper@37906
|
214 |
(*if cuts = [([2], Res),
|
neuper@37906
|
215 |
([3], Frm),
|
neuper@37906
|
216 |
([3, 1], Frm),
|
neuper@37906
|
217 |
([3, 1], Res),
|
neuper@37906
|
218 |
([3, 2], Res),
|
neuper@37906
|
219 |
([3], Res),
|
neuper@37906
|
220 |
([4], Res)]
|
neuper@38031
|
221 |
then () else error "ctree.sml: diff:behav. in cut_level 1a";
|
neuper@37906
|
222 |
val (res,asm) = get_obj g_result pt' [2];
|
neuper@37906
|
223 |
if res = e_term andalso asm = [] then () else
|
neuper@38031
|
224 |
error "ctree.sml: diff:behav. in cut_level 1aa" WN050219*);
|
neuper@37906
|
225 |
if not (existpt [2] pt') then () else
|
neuper@38031
|
226 |
error "ctree.sml: diff:behav. in cut_level 1aa2" (*WN050220*);
|
neuper@37906
|
227 |
|
neuper@37906
|
228 |
val (res,asm) = get_obj g_result pt' [];
|
neuper@37906
|
229 |
if term2str res = "[x = 1]" (*WN050219 e_term in cut_tree!!!*) then () else
|
neuper@38031
|
230 |
error "ctree.sml: diff:behav. in cut_level 1ab";
|
neuper@37906
|
231 |
if map fst (get_interval ([],Frm) ([],Res) 9999 pt') =
|
neuper@37906
|
232 |
[([], Frm),
|
neuper@37906
|
233 |
([1], Frm),
|
neuper@37906
|
234 |
([1], Res),
|
neuper@37906
|
235 |
([2], Res),(*, e_term in cut_tree!!!*)
|
neuper@37906
|
236 |
([], Res)] then () else
|
neuper@38031
|
237 |
error "ctree.sml: diff:behav. in cut_level 1b";
|
neuper@37906
|
238 |
|
neuper@37906
|
239 |
|
neuper@37906
|
240 |
val (pt',cuts) = cut_level [] [] pt ([2],Res);
|
neuper@37906
|
241 |
if cuts = [([3], Frm),
|
neuper@37906
|
242 |
([3, 1], Frm),
|
neuper@37906
|
243 |
([3, 1], Res),
|
neuper@37906
|
244 |
([3, 2], Res),
|
neuper@37906
|
245 |
([3], Res),
|
neuper@37906
|
246 |
([4], Res)]
|
neuper@38031
|
247 |
then () else error "ctree.sml: diff:behav. in cut_level 2a";
|
neuper@37906
|
248 |
|
neuper@37906
|
249 |
if pr_ptree pr_short pt' = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n"
|
neuper@38031
|
250 |
then () else error "ctree.sml: diff:behav. in cut_level 2b";
|
neuper@37906
|
251 |
|
neuper@37906
|
252 |
val (pt',cuts) = cut_level [] [3] pt ([3,1],Frm);
|
neuper@37906
|
253 |
if cuts = [([3, 1], Res), ([3, 2], Res)]
|
neuper@38031
|
254 |
then () else error "ctree.sml: diff:behav. in cut_level 3a";
|
neuper@37906
|
255 |
if pr_ptree pr_short pt' = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n3. ----- pblobj -----\n3.1. -1 + x = 0\n4. [x = 1]\n"
|
neuper@38031
|
256 |
then () else error "ctree.sml: diff:behav. in cut_level 3b";
|
neuper@37906
|
257 |
|
neuper@37906
|
258 |
val (pt',cuts) = cut_level [] [3] pt ([3,1],Res);
|
neuper@37906
|
259 |
if cuts = [([3, 2], Res)]
|
neuper@38031
|
260 |
then () else error "ctree.sml: diff:behav. in cut_level 4a";
|
neuper@37906
|
261 |
if pr_ptree pr_short pt' = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n3. ----- pblobj -----\n3.1. -1 + x = 0\n4. [x = 1]\n"
|
neuper@38031
|
262 |
then () else error "ctree.sml: diff:behav. in cut_level 4b";
|
neuper@37906
|
263 |
|
neuper@37906
|
264 |
|
neuper@37906
|
265 |
"-------------- cut_tree (from ptree above)-----------------------";
|
neuper@37906
|
266 |
"-------------- cut_tree (from ptree above)-----------------------";
|
neuper@37906
|
267 |
"-------------- cut_tree (from ptree above)-----------------------";
|
neuper@37906
|
268 |
val (pt', cuts) = cut_tree pt ([2],Frm);(*not created by move_dn -- not on WS*)
|
neuper@37906
|
269 |
if cuts = [([2], Res),
|
neuper@37906
|
270 |
([3], Frm),
|
neuper@37906
|
271 |
([3, 1], Frm),
|
neuper@37906
|
272 |
([3, 1], Res),
|
neuper@37906
|
273 |
([3, 2], Res),
|
neuper@37906
|
274 |
([3], Res),
|
neuper@37906
|
275 |
([4], Res),
|
neuper@37906
|
276 |
([], Res)]
|
neuper@38031
|
277 |
then () else error "ctree.sml: diff:behav. in cut_tree 1a";
|
neuper@37906
|
278 |
|
neuper@37906
|
279 |
val (res,asm) = get_obj g_result pt' [2];
|
neuper@37906
|
280 |
if res = e_term (*WN050219 done by cut_level*) then () else
|
neuper@38031
|
281 |
error "ctree.sml: diff:behav. in cut_tree 1aa";
|
neuper@37906
|
282 |
|
neuper@37906
|
283 |
val form = get_obj g_form pt' [2];
|
neuper@37906
|
284 |
if term2str form = "x + 1 + -1 * 2 = 0" (*remained !!!*) then () else
|
neuper@38031
|
285 |
error "ctree.sml: diff:behav. in cut_tree 1ab";
|
neuper@37906
|
286 |
|
neuper@37906
|
287 |
val (res,asm) = get_obj g_result pt' [];
|
neuper@37906
|
288 |
if res = e_term (*WN050219 done by cut_tree*) then () else
|
neuper@38031
|
289 |
error "ctree.sml: diff:behav. in cut_tree 1ac";
|
neuper@37906
|
290 |
|
neuper@37906
|
291 |
if map fst (get_interval ([],Frm) ([],Res) 9999 pt') =
|
neuper@37906
|
292 |
[([], Frm),
|
neuper@37906
|
293 |
([1], Frm),
|
neuper@37906
|
294 |
([1], Res)] then () else
|
neuper@38031
|
295 |
error "ctree.sml: diff:behav. in cut_tree 1ad";
|
neuper@37906
|
296 |
|
neuper@37906
|
297 |
val (pt', cuts) = cut_tree pt ([2],Res);
|
neuper@37906
|
298 |
if cuts = [([3], Frm),
|
neuper@37906
|
299 |
([3, 1], Frm),
|
neuper@37906
|
300 |
([3, 1], Res),
|
neuper@37906
|
301 |
([3, 2], Res),
|
neuper@37906
|
302 |
([3], Res),
|
neuper@37906
|
303 |
([4], Res),
|
neuper@37906
|
304 |
([], Res)]
|
neuper@38031
|
305 |
then () else error "ctree.sml: diff:behav. in cut_tree 2";
|
neuper@37906
|
306 |
|
neuper@37906
|
307 |
val (pt', cuts) = cut_tree pt ([3,1],Frm);
|
neuper@37906
|
308 |
if cuts = [([3, 1], Res),
|
neuper@37906
|
309 |
([3, 2], Res),
|
neuper@37906
|
310 |
([3], Res),
|
neuper@37906
|
311 |
([4], Res),
|
neuper@37906
|
312 |
([], Res)]
|
neuper@38031
|
313 |
then () else error "ctree.sml: diff:behav. in cut_tree 3";
|
neuper@37906
|
314 |
|
neuper@37906
|
315 |
val (pt', cuts) = cut_tree pt ([3,1],Res);
|
neuper@37906
|
316 |
if cuts = [([3, 2], Res),
|
neuper@37906
|
317 |
([3], Res),
|
neuper@37906
|
318 |
([4], Res),
|
neuper@37906
|
319 |
([], Res)]
|
neuper@38031
|
320 |
then () else error "ctree.sml: diff:behav. in cut_tree 4";
|
neuper@37906
|
321 |
|
neuper@37906
|
322 |
|
neuper@37906
|
323 |
"=====new ptree 1a miniscript with mini-subpbl ===================";
|
neuper@37906
|
324 |
"=====new ptree 1a miniscript with mini-subpbl ===================";
|
neuper@37906
|
325 |
"=====new ptree 1a miniscript with mini-subpbl ===================";
|
neuper@37906
|
326 |
val fmz = ["equality (x+1=2)",
|
neuper@37906
|
327 |
"solveFor x","solutions L"];
|
neuper@37906
|
328 |
val (dI',pI',mI') =
|
neuper@38058
|
329 |
("Test",["sqroot-test","univariate","equation","test"],
|
neuper@37906
|
330 |
["Test","squ-equ-test-subpbl1"]);
|
neuper@37906
|
331 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
332 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
333 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
334 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
335 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
336 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
337 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
338 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
339 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
340 |
show_pt pt;
|
neuper@37906
|
341 |
|
neuper@37906
|
342 |
"-------------- cut_level ( ,Frm) on Incomplete Nd ---------------";
|
neuper@37906
|
343 |
"-------------- cut_level ( ,Frm) on Incomplete Nd ---------------";
|
neuper@37906
|
344 |
"-------------- cut_level ( ,Frm) on Incomplete Nd ---------------";
|
neuper@37906
|
345 |
|
neuper@37906
|
346 |
val (pt',cuts) = cut_level [] [3] pt ([1],Frm);(*([1],Frm) is stored*)
|
neuper@37906
|
347 |
if cuts = [](*([1],Res) is not yet stored (Nd.ostate=Incomplete)*)
|
neuper@38031
|
348 |
then () else error "ctree.sml: diff:behav. in cut_tree 4a";
|
neuper@37906
|
349 |
|
neuper@37906
|
350 |
val (pt', cuts) = cut_tree pt ([1],Frm);
|
neuper@37906
|
351 |
if cuts = []
|
neuper@38031
|
352 |
then () else error "ctree.sml: diff:behav. in cut_tree 4a";
|
neuper@37906
|
353 |
|
neuper@37906
|
354 |
(*WN050219
|
neuper@37906
|
355 |
val pos as ([p],_) = ([1],Frm);
|
neuper@37906
|
356 |
val pt as Nd (b,_) = pt;
|
neuper@37906
|
357 |
|
neuper@37906
|
358 |
|
neuper@37906
|
359 |
show_pt pt;
|
neuper@37906
|
360 |
show_pt pt';
|
neuper@37906
|
361 |
print_depth 99;cuts;print_depth 3;
|
neuper@37906
|
362 |
print_depth 99;map fst (get_interval ([],Frm) ([],Res) 9999 pt');print_depth 3;
|
neuper@37906
|
363 |
####################################################################*)*)
|
neuper@37906
|
364 |
|
neuper@37906
|
365 |
"=====new ptree 2 miniscript with mini-subpbl ====================";
|
neuper@37906
|
366 |
"=====new ptree 2 miniscript with mini-subpbl ====================";
|
neuper@37906
|
367 |
"=====new ptree 2 miniscript with mini-subpbl ====================";
|
neuper@37906
|
368 |
states:=[];
|
neuper@37906
|
369 |
CalcTree
|
neuper@37906
|
370 |
[(["equality (x+1=2)", "solveFor x","solutions L"],
|
neuper@38058
|
371 |
("Test",
|
neuper@37906
|
372 |
["sqroot-test","univariate","equation","test"],
|
neuper@37906
|
373 |
["Test","squ-equ-test-subpbl1"]))];
|
neuper@37906
|
374 |
Iterator 1; moveActiveRoot 1;
|
neuper@37906
|
375 |
autoCalculate 1 CompleteCalc;
|
neuper@37906
|
376 |
|
neuper@37906
|
377 |
interSteps 1 ([3,2],Res);
|
neuper@37906
|
378 |
|
neuper@37906
|
379 |
val ((pt,_),_) = get_calc 1;
|
neuper@37906
|
380 |
show_pt pt;
|
neuper@37906
|
381 |
|
neuper@37906
|
382 |
"-------------- cut_tree (intermedi.ptree: 3rd level)-------------";
|
neuper@37906
|
383 |
"-------------- cut_tree (intermedi.ptree: 3rd level)-------------";
|
neuper@37906
|
384 |
"-------------- cut_tree (intermedi.ptree: 3rd level)-------------";
|
neuper@37906
|
385 |
(*WN050225 intermed. outcommented
|
neuper@37906
|
386 |
val (pt', cuts) = cut_tree pt ([3,2,1],Frm);
|
neuper@37906
|
387 |
if cuts = [([3, 2, 1], Res),
|
neuper@37906
|
388 |
([3, 2, 2], Res),
|
neuper@37906
|
389 |
([3, 2], Res),
|
neuper@37906
|
390 |
([3], Res),
|
neuper@37906
|
391 |
([4], Res)]
|
neuper@38031
|
392 |
then () else error "ctree.sml: diff:behav. in cut_tree 3rd level 1";
|
neuper@37906
|
393 |
|
neuper@37906
|
394 |
val (pt', cuts) = cut_tree pt ([3,2,1],Res);
|
neuper@37906
|
395 |
if cuts = [([3, 2, 2], Res),
|
neuper@37906
|
396 |
([3, 2], Res),
|
neuper@37906
|
397 |
([3], Res),
|
neuper@37906
|
398 |
([4], Res)]
|
neuper@38031
|
399 |
then () else error "ctree.sml: diff:behav. in cut_tree 3rd level 2";
|
neuper@37906
|
400 |
|
neuper@37906
|
401 |
|
neuper@37906
|
402 |
"-------------- cappend (from ptree above)------------------------";
|
neuper@37906
|
403 |
"-------------- cappend (from ptree above)------------------------";
|
neuper@37906
|
404 |
"-------------- cappend (from ptree above)------------------------";
|
neuper@37906
|
405 |
val (pt',cuts) = cappend_form pt [3,2,1] e_istate (str2term "newnew");
|
neuper@37906
|
406 |
if cuts = [([3, 2, 1], Res),
|
neuper@37906
|
407 |
([3, 2, 2], Res),
|
neuper@37906
|
408 |
([3, 2], Res),
|
neuper@37906
|
409 |
([3], Res),
|
neuper@37906
|
410 |
([4], Res),
|
neuper@37906
|
411 |
([], Res)]
|
neuper@38031
|
412 |
then () else error "ctree.sml: diff:behav. in cappend_form";
|
neuper@37906
|
413 |
if term2str (get_obj g_form pt' [3,2,1]) = "newnew" andalso
|
neuper@37906
|
414 |
get_obj g_tac pt' [3,2,1] = Empty_Tac andalso
|
neuper@37906
|
415 |
term2str (fst (get_obj g_result pt' [3,2,1])) = "??.empty"
|
neuper@38031
|
416 |
then () else error "ctree.sml: diff:behav. in cappend 1";
|
neuper@37906
|
417 |
|
neuper@37906
|
418 |
val (pt',cuts) = cappend_atomic pt [3,2,1] e_istate (str2term "newform")
|
neuper@37906
|
419 |
(Tac "test") (str2term "newresult",[]) Complete;
|
neuper@37906
|
420 |
if cuts = [([3, 2, 1], Res), (*?????????????*)
|
neuper@37906
|
421 |
([3, 2, 2], Res),
|
neuper@37906
|
422 |
([3, 2], Res),
|
neuper@37906
|
423 |
([3], Res),
|
neuper@37906
|
424 |
([4], Res),
|
neuper@37906
|
425 |
([], Res)]
|
neuper@38031
|
426 |
then () else error "ctree.sml: diff:behav. in cappend_atomic";
|
neuper@37906
|
427 |
|
neuper@37906
|
428 |
|
neuper@37906
|
429 |
|
neuper@37906
|
430 |
"-------------- cappend minisubpbl -------------------------------";
|
neuper@37906
|
431 |
"-------------- cappend minisubpbl -------------------------------";
|
neuper@37906
|
432 |
"-------------- cappend minisubpbl -------------------------------";
|
neuper@37906
|
433 |
"=====new ptree 1 miniscript with mini-subpbl ====================";
|
neuper@37906
|
434 |
val fmz = ["equality (x+1=2)",
|
neuper@37906
|
435 |
"solveFor x","solutions L"];
|
neuper@37906
|
436 |
val (dI',pI',mI') =
|
neuper@38058
|
437 |
("Test",["sqroot-test","univariate","equation","test"],
|
neuper@37906
|
438 |
["Test","squ-equ-test-subpbl1"]);
|
neuper@37906
|
439 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
440 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
441 |
(* nxt = Add_Given "equality (x + 1 = 2)"
|
neuper@37924
|
442 |
(writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
|
neuper@37906
|
443 |
*)
|
neuper@37906
|
444 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37924
|
445 |
(* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
|
neuper@37906
|
446 |
*)
|
neuper@37906
|
447 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37924
|
448 |
(* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
|
neuper@37906
|
449 |
*)
|
neuper@37906
|
450 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
451 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
452 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
453 |
(*###cappend_form: pos =[1] ... while calculating nxt, which pt is dropped
|
neuper@37906
|
454 |
val nxt = ("Apply_Method", Apply_Method ["Test", "squ-equ-test-subpbl1"])*)
|
neuper@37906
|
455 |
|
neuper@37906
|
456 |
(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_form: pos =[1]*);
|
neuper@37906
|
457 |
val p = ([1], Frm);
|
neuper@37906
|
458 |
val (pt,cuts) = cappend_form pt (fst p) e_istate (str2term "x + 1 = 2");
|
neuper@37906
|
459 |
val form = get_obj g_form pt (fst p);
|
neuper@37906
|
460 |
val (res,_) = get_obj g_result pt (fst p);
|
neuper@37906
|
461 |
if term2str form = "x + 1 = 2" andalso res = e_term then () else
|
neuper@38031
|
462 |
error "ctree.sml, diff.behav. cappend minisubpbl ([1],Frm)";
|
neuper@37906
|
463 |
if not (existpt ((lev_on o fst) p) pt) then () else
|
neuper@38031
|
464 |
error "ctree.sml, diff.behav. cappend minisubpbl ([1],Frm) nxt";
|
neuper@37906
|
465 |
|
neuper@37906
|
466 |
(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[1]*);
|
neuper@37906
|
467 |
val p = ([1], Res);
|
neuper@37906
|
468 |
val (pt,cuts) =
|
neuper@37906
|
469 |
cappend_atomic pt (fst p) e_istate (str2term "x + 1 = 2")
|
neuper@37906
|
470 |
Empty_Tac (str2term "x + 1 + -1 * 2 = 0",[]) Incomplete;
|
neuper@37906
|
471 |
val form = get_obj g_form pt (fst p);
|
neuper@37906
|
472 |
val (res,_) = get_obj g_result pt (fst p);
|
neuper@37906
|
473 |
if term2str form = "x + 1 = 2" andalso term2str res = "x + 1 + -1 * 2 = 0"
|
neuper@38031
|
474 |
then () else error "ctree.sml, diff.behav. cappend minisubpbl ([1],Res)";
|
neuper@37906
|
475 |
if not (existpt ((lev_on o fst) p) pt) then () else
|
neuper@38031
|
476 |
error "ctree.sml, diff.behav. cappend minisubpbl ([1],Res) nxt";
|
neuper@37906
|
477 |
|
neuper@37906
|
478 |
(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[2]*);
|
neuper@37906
|
479 |
val p = ([2], Res);
|
neuper@37906
|
480 |
val (pt,cuts) =
|
neuper@37906
|
481 |
cappend_atomic pt (fst p) e_istate (str2term "x + 1 + -1 * 2 = 0")
|
neuper@37906
|
482 |
Empty_Tac (str2term "-1 + x = 0",[]) Incomplete;
|
neuper@37906
|
483 |
val form = get_obj g_form pt (fst p);
|
neuper@37906
|
484 |
val (res,_) = get_obj g_result pt (fst p);
|
neuper@37906
|
485 |
if term2str form = "x + 1 + -1 * 2 = 0" andalso term2str res = "-1 + x = 0"
|
neuper@38031
|
486 |
then () else error "ctree.sml, diff.behav. cappend minisubpbl ([2],Res)";
|
neuper@37906
|
487 |
if not (existpt ((lev_on o fst) p) pt) then () else
|
neuper@38031
|
488 |
error "ctree.sml, diff.behav. cappend minisubpbl ([2],Res) nxt";
|
neuper@37906
|
489 |
|
neuper@37906
|
490 |
|
neuper@37906
|
491 |
(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(**)cappend_problem: pos =[3]*)
|
neuper@37906
|
492 |
val p = ([3], Pbl);
|
neuper@37906
|
493 |
val (pt,cuts) = cappend_problem pt (fst p) e_istate e_fmz ([],e_spec,e_term);
|
neuper@37906
|
494 |
if is_pblobj (get_obj I pt (fst p)) then () else
|
neuper@38031
|
495 |
error "ctree.sml, diff.behav. cappend minisubpbl ([3],Pbl)";
|
neuper@37906
|
496 |
if not (existpt ((lev_on o fst) p) pt) then () else
|
neuper@38031
|
497 |
error "ctree.sml, diff.behav. cappend minisubpbl ([3],Pbl) nxt";
|
neuper@37906
|
498 |
|
neuper@37906
|
499 |
(* ...complete calchead skipped...*)
|
neuper@37906
|
500 |
|
neuper@37906
|
501 |
(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_form: pos =[3,1]*);
|
neuper@37906
|
502 |
val p = ([3, 1], Frm);
|
neuper@37906
|
503 |
val (pt,cuts) = cappend_form pt (fst p) e_istate (str2term "-1 + x = 0");
|
neuper@37906
|
504 |
val form = get_obj g_form pt (fst p);
|
neuper@37906
|
505 |
val (res,_) = get_obj g_result pt (fst p);
|
neuper@37906
|
506 |
if term2str form = "-1 + x = 0" andalso res = e_term then () else
|
neuper@38031
|
507 |
error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Frm)";
|
neuper@37906
|
508 |
if not (existpt ((lev_on o fst) p) pt) then () else
|
neuper@38031
|
509 |
error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Frm) nxt";
|
neuper@37906
|
510 |
|
neuper@37906
|
511 |
(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(**)cappend_atomic: pos =[3,1]*)
|
neuper@37906
|
512 |
val p = ([3, 1], Res);
|
neuper@37906
|
513 |
val (pt,cuts) =
|
neuper@37906
|
514 |
cappend_atomic pt (fst p) e_istate (str2term "-1 + x = 0")
|
neuper@37906
|
515 |
Empty_Tac (str2term "x = 0 + -1 * -1",[]) Incomplete;
|
neuper@37906
|
516 |
val form = get_obj g_form pt (fst p);
|
neuper@37906
|
517 |
val (res,_) = get_obj g_result pt (fst p);
|
neuper@37906
|
518 |
if term2str form = "-1 + x = 0" andalso term2str res = "x = 0 + -1 * -1" then()
|
neuper@38031
|
519 |
else error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Res)";
|
neuper@37906
|
520 |
if not (existpt ((lev_on o fst) p) pt) then () else
|
neuper@38031
|
521 |
error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Res) nxt";
|
neuper@37906
|
522 |
|
neuper@37906
|
523 |
(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_form: pos =[3,1]*);
|
neuper@37906
|
524 |
(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[3,1]*);
|
neuper@37906
|
525 |
(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[3,2]*);
|
neuper@37906
|
526 |
(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**).append_result: pos =[3]*);
|
neuper@37906
|
527 |
(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[4]*);
|
neuper@37906
|
528 |
(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**).append_result: pos =[]*);
|
neuper@37906
|
529 |
|
neuper@37906
|
530 |
WN050225 intermed. outcommented---*)
|
neuper@37906
|
531 |
|
neuper@37906
|
532 |
"=====new ptree 3 ================================================";
|
neuper@37906
|
533 |
"=====new ptree 3 ================================================";
|
neuper@37906
|
534 |
"=====new ptree 3 ================================================";
|
neuper@37906
|
535 |
states:=[];
|
neuper@37906
|
536 |
CalcTree
|
neuper@37906
|
537 |
[(["equality (x+1=2)", "solveFor x","solutions L"],
|
neuper@38058
|
538 |
("Test",
|
neuper@37906
|
539 |
["sqroot-test","univariate","equation","test"],
|
neuper@37906
|
540 |
["Test","squ-equ-test-subpbl1"]))];
|
neuper@37906
|
541 |
Iterator 1; moveActiveRoot 1;
|
neuper@37906
|
542 |
autoCalculate 1 CompleteCalc;
|
neuper@37906
|
543 |
|
neuper@37906
|
544 |
val ((pt,_),_) = get_calc 1;
|
neuper@37906
|
545 |
show_pt pt;
|
neuper@37906
|
546 |
|
neuper@37906
|
547 |
"-------------- move_dn ------------------------------------------";
|
neuper@37906
|
548 |
"-------------- move_dn ------------------------------------------";
|
neuper@37906
|
549 |
"-------------- move_dn ------------------------------------------";
|
neuper@37906
|
550 |
val p = move_dn [] pt ([],Pbl) (*-> ([1],Frm)*);
|
neuper@37906
|
551 |
val p = move_dn [] pt p (*-> ([1],Res)*);
|
neuper@37906
|
552 |
val p = move_dn [] pt p (*-> ([2],Res)*);
|
neuper@37906
|
553 |
val p = move_dn [] pt p (*-> ([3],Pbl)*);
|
neuper@37906
|
554 |
val p = move_dn [] pt p (*-> ([3,1],Frm)*);
|
neuper@37906
|
555 |
val p = move_dn [] pt p (*-> ([3,1],Res)*);
|
neuper@37906
|
556 |
val p = move_dn [] pt p (*-> ([3,2],Res)*);
|
neuper@37906
|
557 |
val p = move_dn [] pt p (*-> ([3],Res)*);
|
neuper@37906
|
558 |
(* term2str (get_obj g_res pt [3]);
|
neuper@37906
|
559 |
term2str (get_obj g_form pt [4]);
|
neuper@37906
|
560 |
*)
|
neuper@37906
|
561 |
val p = move_dn [] pt p (*-> ([4],Res)*);
|
neuper@37906
|
562 |
val p = move_dn [] pt p (*-> ([],Res)*);
|
neuper@37906
|
563 |
(*
|
neuper@37906
|
564 |
val p = (move_dn [] pt p) handle e => print_exn_G e;
|
neuper@37906
|
565 |
Exception PTREE end of calculation*)
|
neuper@38031
|
566 |
if p=([],Res) then () else error "ctree.sml: diff:behav. in move_dn";
|
neuper@37906
|
567 |
|
neuper@37906
|
568 |
|
neuper@37906
|
569 |
"-------------- move_dn: Frm -> Res ------------------------------";
|
neuper@37906
|
570 |
"-------------- move_dn: Frm -> Res ------------------------------";
|
neuper@37906
|
571 |
"-------------- move_dn: Frm -> Res ------------------------------";
|
neuper@37906
|
572 |
states := [];
|
neuper@37906
|
573 |
CalcTree (*start of calculation, return No.1*)
|
neuper@37906
|
574 |
[(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
|
neuper@38058
|
575 |
("Test",
|
neuper@37906
|
576 |
["linear","univariate","equation","test"],
|
neuper@37906
|
577 |
["Test","solve_linear"]))];
|
neuper@37906
|
578 |
Iterator 1; moveActiveRoot 1;
|
neuper@37906
|
579 |
autoCalculate 1 CompleteCalcHead;
|
neuper@37906
|
580 |
autoCalculate 1 (Step 1);
|
neuper@37906
|
581 |
refFormula 1 (get_pos 1 1);
|
neuper@37906
|
582 |
|
neuper@37906
|
583 |
moveActiveRoot 1;
|
neuper@37906
|
584 |
moveActiveDown 1;
|
neuper@37906
|
585 |
if get_pos 1 1 = ([1], Frm) then ()
|
neuper@38031
|
586 |
else error "ctree.sml: diff.behav. in move_dn: Frm -> Res (1)";
|
neuper@37906
|
587 |
moveActiveDown 1; (*<ERROR> pos does not exist </ERROR>*)
|
neuper@37906
|
588 |
|
neuper@37906
|
589 |
autoCalculate 1 (Step 1);
|
neuper@37906
|
590 |
refFormula 1 (get_pos 1 1);
|
neuper@37906
|
591 |
|
neuper@37906
|
592 |
moveActiveDown 1; (*<ERROR> pos does not exist </ERROR>*)
|
neuper@37906
|
593 |
if get_pos 1 1 = ([1], Res) then ()
|
neuper@38031
|
594 |
else error "ctree.sml: diff.behav. in move_dn: Frm -> Res (1)";
|
neuper@37906
|
595 |
moveActiveDown 1; (*<ERROR> pos does not exist </ERROR>*)
|
neuper@37906
|
596 |
|
neuper@37906
|
597 |
|
neuper@37906
|
598 |
"-------------- move_up ------------------------------------------";
|
neuper@37906
|
599 |
"-------------- move_up ------------------------------------------";
|
neuper@37906
|
600 |
"-------------- move_up ------------------------------------------";
|
neuper@37906
|
601 |
val p = move_up [] pt ([],Res); (*-> ([4],Res)*)
|
neuper@37906
|
602 |
val p = move_up [] pt p; (*-> ([3],Res)*)
|
neuper@37906
|
603 |
val p = move_up [] pt p; (*-> ([3,2],Res)*)
|
neuper@37906
|
604 |
val p = move_up [] pt p; (*-> ([3,1],Res)*)
|
neuper@37906
|
605 |
val p = move_up [] pt p; (*-> ([3,1],Frm)*)
|
neuper@37906
|
606 |
val p = move_up [] pt p; (*-> ([3],Pbl)*)
|
neuper@37906
|
607 |
val p = move_up [] pt p; (*-> ([2],Res)*)
|
neuper@37906
|
608 |
val p = move_up [] pt p; (*-> ([1],Res)*)
|
neuper@37906
|
609 |
val p = move_up [] pt p; (*-> ([1],Frm)*)
|
neuper@37906
|
610 |
val p = move_up [] pt p; (*-> ([],Pbl)*)
|
neuper@37906
|
611 |
(*val p = (move_up [] pt p) handle e => print_exn_G e;
|
neuper@37906
|
612 |
Exception PTREE begin of calculation*)
|
neuper@38031
|
613 |
if p=([],Pbl) then () else error "ctree.sml: diff.behav. in move_up";
|
neuper@37906
|
614 |
|
neuper@37906
|
615 |
|
neuper@37906
|
616 |
"------ move into detail -----------------------------------------";
|
neuper@37906
|
617 |
"------ move into detail -----------------------------------------";
|
neuper@37906
|
618 |
"------ move into detail -----------------------------------------";
|
neuper@37906
|
619 |
states:=[];
|
neuper@37906
|
620 |
CalcTree
|
neuper@37906
|
621 |
[(["equality (x+1=2)", "solveFor x","solutions L"],
|
neuper@38058
|
622 |
("Test",
|
neuper@37906
|
623 |
["sqroot-test","univariate","equation","test"],
|
neuper@37906
|
624 |
["Test","squ-equ-test-subpbl1"]))];
|
neuper@37906
|
625 |
Iterator 1; moveActiveRoot 1;
|
neuper@37906
|
626 |
autoCalculate 1 CompleteCalc;
|
neuper@37906
|
627 |
moveActiveRoot 1;
|
neuper@37906
|
628 |
moveActiveDown 1;
|
neuper@37906
|
629 |
moveActiveDown 1;
|
neuper@37906
|
630 |
moveActiveDown 1;
|
neuper@37906
|
631 |
refFormula 1 (get_pos 1 1) (* 2 Res, <ISA> -1 + x = 0 </ISA> *);
|
neuper@37906
|
632 |
|
neuper@37906
|
633 |
interSteps 1 ([2],Res);
|
neuper@37906
|
634 |
|
neuper@37906
|
635 |
val ((pt,_),_) = get_calc 1; show_pt pt;
|
neuper@37906
|
636 |
val p = get_pos 1 1;
|
neuper@37906
|
637 |
|
neuper@37906
|
638 |
val p = move_up [] pt p; (*([2, 6], Res)*);
|
neuper@37906
|
639 |
val p = movelevel_up [] pt p;(*([2], Frm)*);
|
neuper@37906
|
640 |
val p = move_dn [] pt p; (*([2, 1], Frm)*);
|
neuper@37906
|
641 |
val p = move_dn [] pt p; (*([2, 1], Res)*);
|
neuper@37906
|
642 |
val p = move_dn [] pt p; (*([2, 2], Res)*);
|
neuper@37906
|
643 |
val p = move_dn [] pt p; (*([2, 3], Res)*);
|
neuper@37906
|
644 |
val p = move_dn [] pt p; (*([2, 4], Res)*);
|
neuper@37906
|
645 |
val p = move_dn [] pt p; (*([2, 5], Res)*);
|
neuper@37906
|
646 |
val p = move_dn [] pt p; (*([2, 6], Res)*);
|
neuper@37906
|
647 |
if p = ([2, 6], Res) then()
|
neuper@38031
|
648 |
else error "ctree.sml: diff.behav. in move into detail";
|
neuper@37906
|
649 |
|
neuper@37906
|
650 |
"=====new ptree 3a ===============================================";
|
neuper@37906
|
651 |
"=====new ptree 3a ===============================================";
|
neuper@37906
|
652 |
"=====new ptree 3a ===============================================";
|
neuper@37906
|
653 |
states:=[];
|
neuper@37906
|
654 |
CalcTree
|
neuper@37906
|
655 |
[(["equality (x+1=2)", "solveFor x","solutions L"],
|
neuper@38058
|
656 |
("Test",
|
neuper@37906
|
657 |
["sqroot-test","univariate","equation","test"],
|
neuper@37906
|
658 |
["Test","squ-equ-test-subpbl1"]))];
|
neuper@37906
|
659 |
Iterator 1; moveActiveRoot 1;
|
neuper@37906
|
660 |
autoCalculate 1 CompleteCalcHead;
|
neuper@37906
|
661 |
autoCalculate 1 (Step 1);
|
neuper@37906
|
662 |
autoCalculate 1 (Step 1);
|
neuper@37906
|
663 |
autoCalculate 1 (Step 1);
|
neuper@37906
|
664 |
val ((pt,_),_) = get_calc 1;
|
neuper@37906
|
665 |
val p = move_dn [] pt ([],Pbl) (*-> ([1], Frm)*);
|
neuper@37906
|
666 |
val p = move_dn [] pt ([1], Frm) (*-> ([1], Res)*);
|
neuper@37906
|
667 |
val p = move_dn [] pt ([1], Res) (*-> ([2], Res)*);
|
neuper@37906
|
668 |
(*val p = move_dn [] pt ([2], Res) ->Exception- PTREE "[] not complete"*);
|
neuper@37906
|
669 |
|
neuper@37906
|
670 |
moveDown 1 ([],Pbl) (*-> ([1], Frm)*);
|
neuper@37906
|
671 |
moveDown 1 ([1],Frm) (*-> ([1],Res)*);
|
neuper@37906
|
672 |
moveDown 1 ([1],Res) (*-> ([2],Res)*);
|
neuper@37906
|
673 |
moveDown 1 ([2],Res) (*-> pos does not exist*);
|
neuper@37906
|
674 |
(*
|
neuper@37906
|
675 |
get_obj g_ostate pt [1];
|
neuper@37906
|
676 |
show_pt pt;
|
neuper@37906
|
677 |
*)
|
neuper@37906
|
678 |
|
neuper@37906
|
679 |
"-------------- move_dn in Incomplete ctree ----------------------";
|
neuper@37906
|
680 |
"-------------- move_dn in Incomplete ctree ----------------------";
|
neuper@37906
|
681 |
"-------------- move_dn in Incomplete ctree ----------------------";
|
neuper@37906
|
682 |
|
neuper@37906
|
683 |
|
neuper@37906
|
684 |
|
neuper@37906
|
685 |
"=====new ptree 4: crooked by cut_level_'_ =======================";
|
neuper@37906
|
686 |
"=====new ptree 4: crooked by cut_level_'_ =======================";
|
neuper@37906
|
687 |
"=====new ptree 4: crooked by cut_level_'_ =======================";
|
neuper@37906
|
688 |
states:=[];
|
neuper@37906
|
689 |
CalcTree
|
neuper@37906
|
690 |
[(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
|
neuper@37906
|
691 |
"solveFor x","solutions L"],
|
neuper@38058
|
692 |
("RatEq",["univariate","equation"],["no_met"]))];
|
neuper@37906
|
693 |
Iterator 1; moveActiveRoot 1;
|
neuper@37906
|
694 |
autoCalculate 1 CompleteCalc;
|
neuper@37906
|
695 |
|
neuper@37906
|
696 |
getTactic 1 ([1],Res);(*Rewrite_Set RatEq_simplify*)
|
neuper@37906
|
697 |
getTactic 1 ([2],Res);(*Rewrite_Set norm_Rational*)
|
neuper@37906
|
698 |
getTactic 1 ([3],Res);(*Rewrite_Set RatEq_eliminate*)
|
neuper@37906
|
699 |
getTactic 1 ([4,1],Res);(*Rewrite all_left*)
|
neuper@37906
|
700 |
getTactic 1 ([4,2],Res);(*Rewrite_Set expand_binoms*)
|
neuper@37906
|
701 |
getTactic 1 ([4,3],Res);(*Rewrite_Set_Inst make_ratpoly_in*)
|
neuper@37906
|
702 |
|
neuper@37906
|
703 |
moveActiveFormula 1 ([1],Res)(*1.1...1.4*);
|
neuper@37906
|
704 |
moveActiveFormula 1 ([2],Res)(**ME_Isa: 'expand' not known*);
|
neuper@37906
|
705 |
moveActiveFormula 1 ([3],Res)(*3.1.*);
|
neuper@37906
|
706 |
moveActiveFormula 1 ([4,2],Res)(*4.2.1.*);
|
neuper@37906
|
707 |
moveActiveFormula 1 ([4,3],Res)(**one_scr_arg: called by Script Stepwise t_=*);
|
neuper@37906
|
708 |
|
neuper@37906
|
709 |
moveActiveFormula 1 ([1],Res)(*1.1...1.4*);
|
neuper@37906
|
710 |
interSteps 1 ([1],Res)(*..is activeFormula !?!*);
|
neuper@37906
|
711 |
|
neuper@37906
|
712 |
getTactic 1 ([1,1],Res);(*Rewrite real_diff_minus*)
|
neuper@37906
|
713 |
getTactic 1 ([1,2],Res);(*Rewrite real_diff_minus*)
|
neuper@37906
|
714 |
getTactic 1 ([1,3],Res);(*Rewrite real_diff_minus*)
|
neuper@37906
|
715 |
getTactic 1 ([1,4],Res);(*Rewrite real_rat_mult_1*)
|
neuper@37906
|
716 |
|
neuper@37906
|
717 |
moveActiveFormula 1 ([4,2],Res)(*4.2.1.*);
|
neuper@37906
|
718 |
interSteps 1 ([4,2],Res)(*..is activeFormula !?!*);
|
neuper@37906
|
719 |
val ((pt,_),_) = get_calc 1;
|
neuper@37906
|
720 |
writeln(pr_ptree pr_short pt);
|
neuper@37906
|
721 |
(*delete [4,1] in order to make pos [4],[4,4] for pblobjs differen [4],[4,3]:
|
neuper@37906
|
722 |
###########################################################################*)
|
neuper@37906
|
723 |
val (pt, ppp) = cut_level_'_ [] [] pt ([4,1],Frm);
|
neuper@37906
|
724 |
writeln(pr_ptree pr_short pt);
|
neuper@37906
|
725 |
|
neuper@37906
|
726 |
|
neuper@37906
|
727 |
"-------------- get_interval from ctree: incremental development--";
|
neuper@37906
|
728 |
"-------------- get_interval from ctree: incremental development--";
|
neuper@37906
|
729 |
"-------------- get_interval from ctree: incremental development--";
|
neuper@37906
|
730 |
"--- level 1: get pos from start b to end p ----------------------";
|
neuper@37906
|
731 |
"--- level 1: get pos from start b to end p ----------------------";
|
neuper@37906
|
732 |
"--- level 1: get pos from start b to end p ----------------------";
|
neuper@37906
|
733 |
(******************************************************************)
|
neuper@37906
|
734 |
(**) val SAVE_get_trace = get_trace; (**)
|
neuper@37906
|
735 |
(******************************************************************)
|
neuper@37906
|
736 |
(*'getnds' below is structured as such:*)
|
neuper@37906
|
737 |
fun www _ [x] = "l+r-margin"
|
neuper@37906
|
738 |
| www true [x1,x2] = "l-margin, r-margin"
|
neuper@37906
|
739 |
| www _ [x1,x2] = "intern, r-margin"
|
neuper@37906
|
740 |
| www true (x::(xs as _::_)) = "l-margin " ^ www false xs
|
neuper@37906
|
741 |
| www _ (x::(xs as _::_)) = "intern " ^ www false xs;
|
neuper@37906
|
742 |
www true [1,2,3,4,5];
|
neuper@37906
|
743 |
(*val it = "from intern intern intern to" : string*)
|
neuper@37906
|
744 |
www true [1,2];
|
neuper@37906
|
745 |
(*val it = "from to" : string*)
|
neuper@37906
|
746 |
www true [1];
|
neuper@37906
|
747 |
(*val it = "from+to" : string*)
|
neuper@37906
|
748 |
|
neuper@37906
|
749 |
local
|
neuper@37906
|
750 |
(*specific values of hd of pos p,q for simple handling take_fromto,
|
neuper@37906
|
751 |
from-pos p, to-pos q: take_fromto (hdp p) (hdq q) (children pt) ...
|
neuper@37906
|
752 |
... can be used even for positions _below_ p or q*)
|
neuper@37906
|
753 |
fun hdp [] = 1 | hdp [0] = 1 | hdp x = hd x;(*start with first*)
|
neuper@37906
|
754 |
fun hdq [] = 99999 | hdq [0] = 99999 | hdq x = hd x;(*take until last*)
|
neuper@37906
|
755 |
(*analoguous for tl*)
|
neuper@37906
|
756 |
fun tlp [] = [0] | tlp [_] = [0] | tlp x = tl x;
|
neuper@37906
|
757 |
fun tlq [] = [99999] | tlq [_] = [99999] | tlq x = tl x;
|
neuper@37906
|
758 |
|
neuper@37906
|
759 |
(*see modspec.sml#pt_form
|
neuper@37906
|
760 |
fun pt_form (PrfObj {form,...}) = term2str form
|
neuper@37906
|
761 |
| pt_form (PblObj {probl,spec,origin=(_,spec',_),...}) =
|
neuper@37906
|
762 |
let val (dI, pI, _) = get_somespec' spec spec'
|
neuper@37906
|
763 |
val {cas,...} = get_pbt pI
|
neuper@37906
|
764 |
in case cas of
|
neuper@37926
|
765 |
NONE => term2str (pblterm dI pI)
|
neuper@37926
|
766 |
| SOME t => term2str (subst_atomic (mk_env probl) t)
|
neuper@37906
|
767 |
end;
|
neuper@37906
|
768 |
*)
|
neuper@37906
|
769 |
(*.get an 'interval' from ptree down to a certain level
|
neuper@37906
|
770 |
by 'take_fromto children' of the nodes with specific 'from' and 'to';
|
neuper@37906
|
771 |
'i > 0' suppresses output during recursive descent towards 'from'
|
neuper@37906
|
772 |
b: the 'from' incremented to the actual pos
|
neuper@37906
|
773 |
p,q: specific 'from','to' for simple use of 'take_fromto'*)
|
neuper@37906
|
774 |
fun getnd i (b,p) q (Nd (po, nds)) =
|
neuper@37906
|
775 |
(if i <= 0 then [(*[(b, pt_form po)]*) (**)[b](**)] else [])
|
neuper@37906
|
776 |
|
neuper@37906
|
777 |
@ (writeln("getnd : b="^(ints2str' b)^", p="^
|
neuper@37906
|
778 |
(ints2str' p)^", q="^(ints2str' q));
|
neuper@37906
|
779 |
|
neuper@37906
|
780 |
getnds (i-1) true (b@[hdp p], tlp p) (tlq q)
|
neuper@37906
|
781 |
(take_fromto (hdp p) (hdq q) nds))
|
neuper@37906
|
782 |
|
neuper@37906
|
783 |
and getnds _ _ _ _ [] = [] (*no children*)
|
neuper@37906
|
784 |
| getnds i _ (b,p) q [nd] = (getnd i (b,p) q nd) (*l+r-margin*)
|
neuper@37906
|
785 |
| getnds i true (b,p) q [n1, n2] = (*l-margin, r-margin*)
|
neuper@37906
|
786 |
(writeln("getnds3: b="^ ints2str' b ^", p="^ ints2str' p ^
|
neuper@37906
|
787 |
", q="^ ints2str' q);
|
neuper@37906
|
788 |
(getnd i ( b, p ) [99999] n1) @
|
neuper@37906
|
789 |
(getnd ~99999 (lev_on b,[0]) q n2))
|
neuper@37906
|
790 |
| getnds i _ (b,p) q [n1, n2] = (*intern, r-margin*)
|
neuper@37906
|
791 |
(writeln("getnds4: b="^ ints2str' b ^", p="^ ints2str' p ^
|
neuper@37906
|
792 |
", q="^ ints2str' q);
|
neuper@37906
|
793 |
(getnd i ( b,[0]) [99999] n1) @
|
neuper@37906
|
794 |
(getnd ~99999 (lev_on b,[0]) q n2))
|
neuper@37906
|
795 |
| getnds i true (b,p) q (nd::(nds as _::_)) = (*l-margin, intern*)
|
neuper@37906
|
796 |
(writeln("getnds5: b="^ ints2str' b ^", p="^ ints2str' p ^
|
neuper@37906
|
797 |
", q="^ ints2str' q);
|
neuper@37906
|
798 |
(getnd i ( b, p ) [99999] nd) @
|
neuper@37906
|
799 |
(getnds ~99999 false (lev_on b,[0]) q nds))
|
neuper@37906
|
800 |
| getnds i _ (b,p) q (nd::(nds as _::_)) = (*intern, ...*)
|
neuper@37906
|
801 |
(getnd i ( b,[0]) [99999] nd) @
|
neuper@37906
|
802 |
(getnds ~99999 false (lev_on b,[0]) q nds);
|
neuper@37906
|
803 |
in
|
neuper@37906
|
804 |
(*get an 'interval from to' from a ptree as 'intervals f t' of respective nodes
|
neuper@37906
|
805 |
where 'from' are pos, i.e. a key as int list, 'f' an int (to,t analoguous)
|
neuper@37906
|
806 |
(1) the 'f' are given
|
neuper@37906
|
807 |
(1a) by 'from' if 'f' = the respective element of 'from' (left margin)
|
neuper@37906
|
808 |
(1b) -inifinity, if 'f' > the respective element of 'from' (internal node)
|
neuper@37906
|
809 |
(2) the 't' ar given
|
neuper@37906
|
810 |
(2a) by 'to' if 't' = the respective element of 'to' (right margin)
|
neuper@37906
|
811 |
(2b) inifinity, if 't' < the respective element of 'to (internal node)'
|
neuper@37906
|
812 |
the 'f' and 't' are set by hdp,... *)
|
neuper@37906
|
813 |
fun get_trace pt p q =
|
neuper@37906
|
814 |
(flat o (getnds ((length p) -1) true ([hdp p], tlp p) (tlq q)))
|
neuper@37906
|
815 |
(take_fromto (hdp p) (hdq q) (children pt));
|
neuper@37906
|
816 |
end;
|
neuper@37906
|
817 |
|
neuper@37906
|
818 |
writeln(pr_ptree pr_short pt);
|
neuper@37906
|
819 |
case get_trace pt [1,3] [4,1,1] of
|
neuper@37906
|
820 |
[[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1]] => ()
|
neuper@38031
|
821 |
| _ => error "diff.behav.in ctree.sml: get_interval lev 1a";
|
neuper@37906
|
822 |
case get_trace pt [2] [4,3,2] of
|
neuper@37906
|
823 |
[[2],[3],[4],[4,1],[4,1,1],[4,2],[4,3],[4,3,1],[4,3,2]] => ()
|
neuper@38031
|
824 |
| _ => error "diff.behav.in ctree.sml: get_interval lev 1b";
|
neuper@37906
|
825 |
case get_trace pt [1,4] [4,3,1] of
|
neuper@37906
|
826 |
[[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],[4,3],[4,3,1]] => ()
|
neuper@38031
|
827 |
| _ => error "diff.behav.in ctree.sml: get_interval lev 1c";
|
neuper@37906
|
828 |
case get_trace pt [4,2] [5] of
|
neuper@37906
|
829 |
(*[([4,2],_),([4,3],_),([4,4],_),([4,4,1],_),([4,4,2],_),([4,4,3],_),
|
neuper@37906
|
830 |
([4,4,4],_),([4,4,5],_),([5],_)] => () ..with pt_form*)
|
neuper@37906
|
831 |
[[4,2],[4,3],[4,3,1],[4,3,2],[4,3,3],[4,3,4],[4,3,5],[5]]=>()
|
neuper@38031
|
832 |
| _ => error "diff.behav.in ctree.sml: get_interval lev 1d";
|
neuper@37906
|
833 |
case get_trace pt [] [4,4,2] of
|
neuper@37906
|
834 |
[[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],
|
neuper@37906
|
835 |
[4,3],[4,3,1],[4,3,2]] => ()
|
neuper@38031
|
836 |
| _ => error "diff.behav.in ctree.sml: get_interval lev 1e";
|
neuper@37906
|
837 |
case get_trace pt [] [] of
|
neuper@37906
|
838 |
[[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],
|
neuper@37906
|
839 |
[4,3],[4,3,1],[4,3,2],[4,3,3],[4,3,4],[4,3,5],[5]] => ()
|
neuper@38031
|
840 |
| _ => error "diff.behav.in ctree.sml: get_interval lev 1f";
|
neuper@37906
|
841 |
case get_trace pt [4,3] [4,3] of
|
neuper@37906
|
842 |
[[4,3],[4,3,1],[4,3,2],[4,3,3],[4,3,4],[4,3,5]] => ()
|
neuper@38031
|
843 |
| _ => error "diff.behav.in ctree.sml: get_interval lev 1g";
|
neuper@37906
|
844 |
|
neuper@37906
|
845 |
"--- level 2: get pos' from start b to end p ---------------------";
|
neuper@37906
|
846 |
"--- level 2: get pos' from start b to end p ---------------------";
|
neuper@37906
|
847 |
"--- level 2: get pos' from start b to end p ---------------------";
|
neuper@37906
|
848 |
(*idea: pos_ is _ONLY_ relevant exactly at (endpoint of) from, to
|
neuper@37906
|
849 |
development stopped in favour of move_dn, see get_interval
|
neuper@37906
|
850 |
actually used (inefficient) version with move_dn: see modspec.sml
|
neuper@37906
|
851 |
*)
|
neuper@37906
|
852 |
(*
|
neuper@37906
|
853 |
case get_trace pt ([1,4],Res) ([4,4,1],Frm) of
|
neuper@37906
|
854 |
[[2],[3],[4],[4,1],[4,2],[4,2,1],[4,3],[4,4],[4,4,1]] => ()
|
neuper@38031
|
855 |
| _ => error "diff.behav.in ctree.sml: get_interval lev 1b";
|
neuper@37906
|
856 |
case get_trace pt ([],Pbl) ([],Res) of
|
neuper@37906
|
857 |
[[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,2],[4,2,1],[4,3],
|
neuper@37906
|
858 |
[4,4],[4,4,1],[4,4,2],[4,4,3],[4,4,4],[4,4,5],[5]] => ()
|
neuper@38031
|
859 |
| _ => error "diff.behav.in ctree.sml: get_interval lev 1e";
|
neuper@37906
|
860 |
*)
|
neuper@37906
|
861 |
|
neuper@37906
|
862 |
(******************************************************************)
|
neuper@37906
|
863 |
(**) val get_trace = SAVE_get_trace; (**)
|
neuper@37906
|
864 |
(******************************************************************)
|
neuper@37906
|
865 |
|
neuper@37906
|
866 |
|
neuper@37906
|
867 |
"=====new ptree 4 ratequation ====================================";
|
neuper@37906
|
868 |
"=====new ptree 4 ratequation ====================================";
|
neuper@37906
|
869 |
"=====new ptree 4 ratequation ====================================";
|
neuper@37906
|
870 |
states:=[];
|
neuper@37906
|
871 |
CalcTree
|
neuper@37906
|
872 |
[(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
|
neuper@37906
|
873 |
"solveFor x","solutions L"],
|
neuper@38058
|
874 |
("RatEq",["univariate","equation"],["no_met"]))];
|
neuper@37906
|
875 |
Iterator 1; moveActiveRoot 1;
|
neuper@37906
|
876 |
autoCalculate 1 CompleteCalc;
|
neuper@37906
|
877 |
val ((pt,_),_) = get_calc 1;
|
neuper@37906
|
878 |
show_pt pt;
|
neuper@37906
|
879 |
|
neuper@37906
|
880 |
|
neuper@37906
|
881 |
"-------------- pt_extract form, tac, asm<>[] --------------------";
|
neuper@37906
|
882 |
"-------------- pt_extract form, tac, asm<>[] --------------------";
|
neuper@37906
|
883 |
"-------------- pt_extract form, tac, asm<>[] --------------------";
|
neuper@37926
|
884 |
val (Form form, SOME tac, asm) = pt_extract (pt, ([3], Res));
|
neuper@37906
|
885 |
case (term2str form, tac, terms2strs asm) of
|
neuper@37906
|
886 |
("(3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)",
|
neuper@37906
|
887 |
Subproblem
|
neuper@38058
|
888 |
("PolyEq",
|
neuper@37906
|
889 |
["normalize", "polynomial", "univariate", "equation"]),
|
neuper@37906
|
890 |
["9 * x + -6 * x ^^^ 2 + x ^^^ 3 ~= 0"]) => ()
|
neuper@38031
|
891 |
| _ => error "diff.behav.in ctree.sml: pt_extract asm<>[]";
|
neuper@37906
|
892 |
(*WN060717 unintentionally changed some rls/ord while
|
neuper@37906
|
893 |
completing knowl. for thes2file...
|
neuper@37906
|
894 |
|
neuper@37906
|
895 |
case (term2str form, tac, terms2strs asm) of
|
neuper@37906
|
896 |
((*"(3 + (-1 * x + x ^^^ 2)) * x = 1 * (9 * x + (x ^^^ 3 + -6 * x ^^^ 2))",
|
neuper@37906
|
897 |
*)Subproblem
|
neuper@38058
|
898 |
("PolyEq",
|
neuper@37906
|
899 |
["normalize", "polynomial", "univariate", "equation"]),
|
neuper@37906
|
900 |
["9 * x + (x ^^^ 3 + -6 * x ^^^ 2) ~= 0"]) => ()
|
neuper@38031
|
901 |
| _ => error "diff.behav.in ctree.sml: pt_extract asm<>[]";
|
neuper@37906
|
902 |
|
neuper@37906
|
903 |
.... but it became even better*)
|
neuper@37906
|
904 |
|
neuper@37906
|
905 |
|
neuper@37906
|
906 |
|
neuper@37906
|
907 |
"=====new ptree 5 minisubpbl =====================================";
|
neuper@37906
|
908 |
"=====new ptree 5 minisubpbl =====================================";
|
neuper@37906
|
909 |
"=====new ptree 5 minisubpbl =====================================";
|
neuper@37906
|
910 |
states:=[];
|
neuper@37906
|
911 |
CalcTree
|
neuper@37906
|
912 |
[(["equality (x+1=2)", "solveFor x","solutions L"],
|
neuper@38058
|
913 |
("Test",
|
neuper@37906
|
914 |
["sqroot-test","univariate","equation","test"],
|
neuper@37906
|
915 |
["Test","squ-equ-test-subpbl1"]))];
|
neuper@37906
|
916 |
Iterator 1; moveActiveRoot 1;
|
neuper@37906
|
917 |
autoCalculate 1 CompleteCalc;
|
neuper@37906
|
918 |
val ((pt,_),_) = get_calc 1;
|
neuper@37906
|
919 |
show_pt pt;
|
neuper@37906
|
920 |
|
neuper@37906
|
921 |
"-------------- pt_extract form, tac, asm ------------------------";
|
neuper@37906
|
922 |
"-------------- pt_extract form, tac, asm ------------------------";
|
neuper@37906
|
923 |
"-------------- pt_extract form, tac, asm ------------------------";
|
neuper@37926
|
924 |
val (ModSpec (_,_,form,_,_,_), SOME tac, asm) = pt_extract (pt, ([], Frm));
|
neuper@37906
|
925 |
case (term2str form, tac, terms2strs asm) of
|
neuper@37906
|
926 |
("solve (x + 1 = 2, x)",
|
neuper@37906
|
927 |
Apply_Method ["Test", "squ-equ-test-subpbl1"],
|
neuper@37906
|
928 |
[]) => ()
|
neuper@38031
|
929 |
| _ => error "diff.behav.in ctree.sml: pt_extract ([], Pbl)";
|
neuper@37906
|
930 |
|
neuper@37926
|
931 |
val (Form form, SOME tac, asm) = pt_extract (pt, ([1], Frm));
|
neuper@37906
|
932 |
case (term2str form, tac, terms2strs asm) of
|
neuper@37906
|
933 |
("x + 1 = 2", Rewrite_Set "norm_equation", []) => ()
|
neuper@38031
|
934 |
| _ => error "diff.behav.in ctree.sml: pt_extract ([1], Frm)";
|
neuper@37906
|
935 |
|
neuper@37926
|
936 |
val (Form form, SOME tac, asm) = pt_extract (pt, ([1], Res));
|
neuper@37906
|
937 |
case (term2str form, tac, terms2strs asm) of
|
neuper@37906
|
938 |
("x + 1 + -1 * 2 = 0", Rewrite_Set "Test_simplify", []) => ()
|
neuper@38031
|
939 |
| _ => error "diff.behav.in ctree.sml: pt_extract ([1], Res)";
|
neuper@37906
|
940 |
|
neuper@37926
|
941 |
val (Form form, SOME tac, asm) = pt_extract (pt, ([2], Res));
|
neuper@37906
|
942 |
case (term2str form, tac, terms2strs asm) of
|
neuper@37906
|
943 |
("-1 + x = 0",
|
neuper@38058
|
944 |
Subproblem ("Test", ["linear", "univariate", "equation", "test"]),
|
neuper@37906
|
945 |
[]) => ()
|
neuper@38031
|
946 |
| _ => error "diff.behav.in ctree.sml: pt_extract ([2], Res)";
|
neuper@37906
|
947 |
|
neuper@37926
|
948 |
val (ModSpec (_,_,form,_,_,_), SOME tac, asm) = pt_extract (pt, ([3], Pbl));
|
neuper@37906
|
949 |
case (term2str form, tac, terms2strs asm) of
|
neuper@37906
|
950 |
("solve (-1 + x = 0, x)", Apply_Method ["Test", "solve_linear"], []) => ()
|
neuper@38031
|
951 |
| _ => error "diff.behav.in ctree.sml: pt_extract ([3], Pbl)";
|
neuper@37906
|
952 |
|
neuper@37926
|
953 |
val (Form form, SOME tac, asm) = pt_extract (pt, ([3,1], Frm));
|
neuper@37906
|
954 |
case (term2str form, tac, terms2strs asm) of
|
neuper@37906
|
955 |
("-1 + x = 0", Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv"), []) => ()
|
neuper@38031
|
956 |
| _ => error "diff.behav.in ctree.sml: pt_extract ([3,1], Frm)";
|
neuper@37906
|
957 |
|
neuper@37926
|
958 |
val (Form form, SOME tac, asm) = pt_extract (pt, ([3,1], Res));
|
neuper@37906
|
959 |
case (term2str form, tac, terms2strs asm) of
|
neuper@37906
|
960 |
("x = 0 + -1 * -1", Rewrite_Set "Test_simplify", []) => ()
|
neuper@38031
|
961 |
| _ => error "diff.behav.in ctree.sml: pt_extract ([3,1], Res)";
|
neuper@37906
|
962 |
|
neuper@37926
|
963 |
val (Form form, SOME tac, asm) = pt_extract (pt, ([3,2], Res));
|
neuper@37906
|
964 |
case (term2str form, tac, terms2strs asm) of
|
neuper@37906
|
965 |
("x = 1", Check_Postcond ["linear", "univariate", "equation", "test"],
|
neuper@37906
|
966 |
[]) => ()
|
neuper@38031
|
967 |
| _ => error "diff.behav.in ctree.sml: pt_extract ([3,2], Res)";
|
neuper@37906
|
968 |
|
neuper@37926
|
969 |
val (Form form, SOME tac, asm) = pt_extract (pt, ([3], Res));
|
neuper@37906
|
970 |
case (term2str form, tac, terms2strs asm) of
|
neuper@37906
|
971 |
("[x = 1]", Check_elementwise "Assumptions", []) => ()
|
neuper@38031
|
972 |
| _ => error "diff.behav.in ctree.sml: pt_extract ([3], Res)";
|
neuper@37906
|
973 |
|
neuper@37926
|
974 |
val (Form form, SOME tac, asm) = pt_extract (pt, ([4], Res));
|
neuper@37906
|
975 |
case (term2str form, tac, terms2strs asm) of
|
neuper@37906
|
976 |
("[x = 1]",
|
neuper@37906
|
977 |
Check_Postcond ["sqroot-test", "univariate", "equation", "test"],
|
neuper@37906
|
978 |
[]) => ()
|
neuper@38031
|
979 |
| _ => error "diff.behav.in ctree.sml: pt_extract ([4], Res)";
|
neuper@37906
|
980 |
|
neuper@37906
|
981 |
val (Form form, tac, asm) = pt_extract (pt, ([], Res));
|
neuper@37906
|
982 |
case (term2str form, tac, terms2strs asm) of
|
neuper@37926
|
983 |
("[x = 1]", NONE, []) => ()
|
neuper@38031
|
984 |
| _ => error "diff.behav.in ctree.sml: pt_extract ([], Res)";
|
neuper@37906
|
985 |
|
neuper@37906
|
986 |
"=====new ptree 6 minisubpbl intersteps ==========================";
|
neuper@37906
|
987 |
"=====new ptree 6 minisubpbl intersteps ==========================";
|
neuper@37906
|
988 |
"=====new ptree 6 minisubpbl intersteps ==========================";
|
neuper@37906
|
989 |
states:=[];
|
neuper@37906
|
990 |
CalcTree
|
neuper@37906
|
991 |
[(["equality (x+1=2)", "solveFor x","solutions L"],
|
neuper@38058
|
992 |
("Test",
|
neuper@37906
|
993 |
["sqroot-test","univariate","equation","test"],
|
neuper@37906
|
994 |
["Test","squ-equ-test-subpbl1"]))];
|
neuper@37906
|
995 |
Iterator 1; moveActiveRoot 1;
|
neuper@37906
|
996 |
autoCalculate 1 CompleteCalc;
|
neuper@37906
|
997 |
interSteps 1 ([2],Res);
|
neuper@37906
|
998 |
interSteps 1 ([3,2],Res);
|
neuper@37906
|
999 |
val ((pt,_),_) = get_calc 1;
|
neuper@37906
|
1000 |
show_pt pt;
|
neuper@37906
|
1001 |
|
neuper@37906
|
1002 |
(**##############################################################**)
|
neuper@37906
|
1003 |
"-------------- get_allpos' new ----------------------------------";
|
neuper@37906
|
1004 |
"-------------- get_allpos' new ----------------------------------";
|
neuper@37906
|
1005 |
"-------------- get_allpos' new ----------------------------------";
|
neuper@37906
|
1006 |
"--- whole ctree";
|
neuper@37906
|
1007 |
print_depth 99;
|
neuper@37906
|
1008 |
val cuts = get_allp [] ([], ([],Frm)) pt;
|
neuper@37906
|
1009 |
print_depth 3;
|
neuper@37906
|
1010 |
if cuts =
|
neuper@37906
|
1011 |
[(*never returns the first pos'*)
|
neuper@37906
|
1012 |
([1], Frm),
|
neuper@37906
|
1013 |
([1], Res),
|
neuper@37906
|
1014 |
([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
|
neuper@37906
|
1015 |
([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
|
neuper@37906
|
1016 |
([2], Res),
|
neuper@37906
|
1017 |
([3], Pbl),
|
neuper@37906
|
1018 |
([3, 1], Frm), ([3, 1], Res),
|
neuper@37906
|
1019 |
([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
|
neuper@37906
|
1020 |
([3, 2], Res),
|
neuper@37906
|
1021 |
([3], Res),
|
neuper@37906
|
1022 |
([4], Res),
|
neuper@37906
|
1023 |
([], Res)] then () else
|
neuper@38031
|
1024 |
error "ctree.sml diff.behav. get_allp new []";
|
neuper@37906
|
1025 |
|
neuper@37906
|
1026 |
print_depth 99;
|
neuper@37906
|
1027 |
val cuts2 = get_allps [] [1] (children pt);
|
neuper@37906
|
1028 |
print_depth 3;
|
neuper@37906
|
1029 |
if cuts = cuts2 @ [([], Res)] then () else
|
neuper@38031
|
1030 |
error "ctree.sml diff.behav. get_allps new []";
|
neuper@37906
|
1031 |
|
neuper@37906
|
1032 |
"---(3) on S(606)..S(608)--------";
|
neuper@37906
|
1033 |
"--- nd [2] with 6 children---------------------------------";
|
neuper@37906
|
1034 |
val cuts = get_allp [] ([2], ([],Frm)) (get_nd pt [2]);
|
neuper@37906
|
1035 |
if cuts =
|
neuper@37906
|
1036 |
[([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
|
neuper@37906
|
1037 |
([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
|
neuper@37906
|
1038 |
([2], Res)] then () else
|
neuper@38031
|
1039 |
error "ctree.sml diff.behav. get_allp new [2]";
|
neuper@37906
|
1040 |
|
neuper@37906
|
1041 |
val cuts2 = get_allps [] [2,1] (children (get_nd pt [2]));
|
neuper@37906
|
1042 |
if cuts = cuts2 @ [([2], Res)] then () else
|
neuper@38031
|
1043 |
error "ctree.sml diff.behav. get_allps new [2]";
|
neuper@37906
|
1044 |
|
neuper@37906
|
1045 |
|
neuper@37906
|
1046 |
"---(4) on S(606)..S(608)--------";
|
neuper@37906
|
1047 |
"--- nd [3] subproblem--------------------------------------";
|
neuper@37906
|
1048 |
val cuts = get_allp [] ([3], ([],Frm)) (get_nd pt [3]);
|
neuper@37906
|
1049 |
if cuts =
|
neuper@37906
|
1050 |
[([3, 1], Frm),
|
neuper@37906
|
1051 |
([3, 1], Res),
|
neuper@37906
|
1052 |
([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
|
neuper@37906
|
1053 |
([3, 2], Res),
|
neuper@37906
|
1054 |
([3], Res)] then () else
|
neuper@38031
|
1055 |
error "ctree.sml diff.behav. get_allp new [3]";
|
neuper@37906
|
1056 |
|
neuper@37906
|
1057 |
val cuts2 = get_allps [] [3,1] (children (get_nd pt [3]));
|
neuper@37906
|
1058 |
if cuts = cuts2 @ [([3], Res)] then () else
|
neuper@38031
|
1059 |
error "ctree.sml diff.behav. get_allps new [3]";
|
neuper@37906
|
1060 |
|
neuper@37906
|
1061 |
"--- nd [3,2] with 2 children--------------------------------";
|
neuper@37906
|
1062 |
val cuts = get_allp [] ([3,2], ([],Frm)) (get_nd pt [3,2]);
|
neuper@37906
|
1063 |
if cuts =
|
neuper@37906
|
1064 |
[([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
|
neuper@37906
|
1065 |
([3, 2], Res)] then () else
|
neuper@38031
|
1066 |
error "ctree.sml diff.behav. get_allp new [3,2]";
|
neuper@37906
|
1067 |
|
neuper@37906
|
1068 |
val cuts2 = get_allps [] [3,2,1] (children (get_nd pt [3,2]));
|
neuper@37906
|
1069 |
if cuts = cuts2 @ [([3, 2], Res)] then () else
|
neuper@38031
|
1070 |
error "ctree.sml diff.behav. get_allps new [3,2]";
|
neuper@37906
|
1071 |
|
neuper@37906
|
1072 |
"---(5a) on S(606)..S(608)--------";
|
neuper@37906
|
1073 |
"--- nd [3,2,1] with 0 children------------------------------";
|
neuper@37906
|
1074 |
val cuts = get_allp [] ([3,2,1], ([],Frm)) (get_nd pt [3,2,1]);
|
neuper@37906
|
1075 |
if cuts =
|
neuper@37906
|
1076 |
[] then () else
|
neuper@38031
|
1077 |
error "ctree.sml diff.behav. get_allp new [3,2,1]";
|
neuper@37906
|
1078 |
|
neuper@37906
|
1079 |
val cuts2 = get_allps [] [3,2,1,1] (children (get_nd pt [3,2,1]));
|
neuper@37906
|
1080 |
if cuts = cuts2 @ [] then () else
|
neuper@38031
|
1081 |
error "ctree.sml diff.behav. get_allps new [3,2,1]";
|
neuper@37906
|
1082 |
|
neuper@37906
|
1083 |
|
neuper@37906
|
1084 |
(**#################################################################**)
|
neuper@37906
|
1085 |
"-------------- cut_tree new (from ptree above)-------------------";
|
neuper@37906
|
1086 |
"-------------- cut_tree new (from ptree above)-------------------";
|
neuper@37906
|
1087 |
"-------------- cut_tree new (from ptree above)-------------------";
|
neuper@37906
|
1088 |
show_pt pt;
|
neuper@37906
|
1089 |
val b = get_obj g_branch pt [];
|
neuper@37906
|
1090 |
if b = TransitiveB then () else
|
neuper@38031
|
1091 |
error ("ctree.sml diff.behav. in [] branch="^branch2str b);
|
neuper@37906
|
1092 |
val b = get_obj g_branch pt [3];
|
neuper@37906
|
1093 |
if b = TransitiveB then () else
|
neuper@38031
|
1094 |
error ("ctree.sml diff.behav. in [3] branch="^branch2str b);
|
neuper@37906
|
1095 |
|
neuper@37906
|
1096 |
"---(2) on S(606)..S(608)--------";
|
neuper@37906
|
1097 |
val (pt', cuts) = cut_tree pt ([1],Res);
|
neuper@37906
|
1098 |
print_depth 99;
|
neuper@37906
|
1099 |
cuts;
|
neuper@37906
|
1100 |
print_depth 3;
|
neuper@37906
|
1101 |
if cuts = [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
|
neuper@37906
|
1102 |
([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res), ([3], Pbl),
|
neuper@37906
|
1103 |
([3, 1], Frm), ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res),
|
neuper@37906
|
1104 |
([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res),
|
neuper@37906
|
1105 |
(*WN060727 after replacing cutlevup by test_trans:*)([], Res)] then () else
|
neuper@38031
|
1106 |
error "ctree.sml: diff.behav. cut_tree ([1],Res)";
|
neuper@37906
|
1107 |
|
neuper@37906
|
1108 |
|
neuper@37906
|
1109 |
"---(3) on S(606)..S(608)--------";
|
neuper@37906
|
1110 |
val (pt', cuts) = cut_tree pt ([2],Res);
|
neuper@37906
|
1111 |
print_depth 99;
|
neuper@37906
|
1112 |
cuts;
|
neuper@37906
|
1113 |
print_depth 3;
|
neuper@37906
|
1114 |
if cuts = [(*preceding step on WS was ([1]),Res*)
|
neuper@37906
|
1115 |
([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
|
neuper@37906
|
1116 |
([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
|
neuper@37906
|
1117 |
([2], Res),
|
neuper@37906
|
1118 |
([3], Pbl),
|
neuper@37906
|
1119 |
([3, 1], Frm),
|
neuper@37906
|
1120 |
([3, 1], Res),
|
neuper@37906
|
1121 |
([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
|
neuper@37906
|
1122 |
([3, 2], Res),
|
neuper@37906
|
1123 |
([3], Res),
|
neuper@37906
|
1124 |
([4], Res),
|
neuper@37906
|
1125 |
(*WN060727 added after replacing cutlevup by test_trans:*)([],Res)] then ()
|
neuper@38031
|
1126 |
else error "ctree.sml: diff.behav. cut_tree ([2],Res)";
|
neuper@37906
|
1127 |
|
neuper@37906
|
1128 |
"---(4) on S(606)..S(608)--------";
|
neuper@37906
|
1129 |
val (pt', cuts) = cut_tree pt ([3],Pbl);
|
neuper@37906
|
1130 |
print_depth 99;
|
neuper@37906
|
1131 |
cuts;
|
neuper@37906
|
1132 |
print_depth 3;
|
neuper@37906
|
1133 |
if cuts = [([3], Pbl),
|
neuper@37906
|
1134 |
([3, 1], Frm), ([3, 1], Res),
|
neuper@37906
|
1135 |
([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
|
neuper@37906
|
1136 |
([3, 2], Res),
|
neuper@37906
|
1137 |
([3], Res),
|
neuper@37906
|
1138 |
([4], Res),
|
neuper@37906
|
1139 |
(*WN060727 added after replacing cutlevup by test_trans:*)([], Res)]
|
neuper@38031
|
1140 |
then () else error "ctree.sml: diff.behav. cut_tree ([3],Pbl)";
|
neuper@37906
|
1141 |
|
neuper@37906
|
1142 |
"---(5a) on S(606)..S(608) cut_tree --------";
|
neuper@37906
|
1143 |
val (pt', cuts) = cut_tree pt ([3,2,1],Res);
|
neuper@37906
|
1144 |
print_depth 99;
|
neuper@37906
|
1145 |
cuts;
|
neuper@37906
|
1146 |
print_depth 1;
|
neuper@37906
|
1147 |
if cuts = [([3, 2, 2], Res), ([3, 2], Res),
|
neuper@37906
|
1148 |
(*WN060727 added after replacing cutlevup by test_trans:*)
|
neuper@37906
|
1149 |
([3], Res), ([4], Res),([],Res)] then ()
|
neuper@38031
|
1150 |
else error "ctree.sml: diff.behav. cut_tree ([3,2,1],Res)";
|
neuper@37906
|
1151 |
show_pt pt';
|
neuper@37906
|
1152 |
|
neuper@37906
|
1153 |
|
neuper@37906
|
1154 |
"-------------- cappend on complete ctree from above -------------";
|
neuper@37906
|
1155 |
"-------------- cappend on complete ctree from above -------------";
|
neuper@37906
|
1156 |
"-------------- cappend on complete ctree from above -------------";
|
neuper@37906
|
1157 |
show_pt pt;
|
neuper@37906
|
1158 |
|
neuper@37906
|
1159 |
"---(2) on S(606)..S(608)--------";
|
neuper@37906
|
1160 |
val (pt', cuts) = cappend_atomic pt [1] e_istate (str2term "Inform[1]")
|
neuper@37906
|
1161 |
(Tac "test") (str2term "Inres[1]",[]) Complete;
|
neuper@37906
|
1162 |
print_depth 99;
|
neuper@37906
|
1163 |
cuts;
|
neuper@37906
|
1164 |
print_depth 3;
|
neuper@37906
|
1165 |
if cuts = [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
|
neuper@37906
|
1166 |
([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res), ([3], Pbl),
|
neuper@37906
|
1167 |
([3, 1], Frm), ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res),
|
neuper@37906
|
1168 |
([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res),
|
neuper@37906
|
1169 |
(*WN060727 added after replacing cutlevup by test_trans:*) ([], Res)] then ()
|
neuper@38031
|
1170 |
else error "ctree.sml: diff:behav. in complete pt:append_atomic[1] cuts";
|
neuper@37906
|
1171 |
val afterins = get_allp [] ([], ([],Frm)) pt';
|
neuper@37906
|
1172 |
print_depth 99;
|
neuper@37906
|
1173 |
afterins;
|
neuper@37906
|
1174 |
print_depth 3;
|
neuper@37906
|
1175 |
if afterins = [([1], Frm), ([1], Res)
|
neuper@37906
|
1176 |
(*, WN060727 removed after replacing cutlevup by test_trans:([], Res)*)] then()
|
neuper@38031
|
1177 |
else error "ctree.sml: diff:behav. in complete pt: append_atomic[1] afterins";
|
neuper@37906
|
1178 |
show_pt pt';
|
neuper@37906
|
1179 |
|
neuper@37906
|
1180 |
"---(3) on S(606)..S(608)--------";
|
neuper@37906
|
1181 |
show_pt pt;
|
neuper@37906
|
1182 |
val (pt', cuts) = cappend_atomic pt [2] e_istate (str2term "Inform[2]")
|
neuper@37906
|
1183 |
(Tac "test") (str2term "Inres[2]",[]) Complete;
|
neuper@37906
|
1184 |
print_depth 99;
|
neuper@37906
|
1185 |
cuts;
|
neuper@37906
|
1186 |
print_depth 3;
|
neuper@37906
|
1187 |
if cuts = [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
|
neuper@37906
|
1188 |
([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res), ([3], Pbl),
|
neuper@37906
|
1189 |
([3, 1], Frm),([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res),
|
neuper@37906
|
1190 |
([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res),
|
neuper@37906
|
1191 |
(*WN060727 added after replacing cutlevup by test_trans:*) ([], Res)] then ()
|
neuper@38031
|
1192 |
else error "ctree.sml: diff:behav.in complete pt: append_atomic[2] cuts";
|
neuper@37906
|
1193 |
val afterins = get_allp [] ([], ([],Frm)) pt';
|
neuper@37906
|
1194 |
print_depth 99;
|
neuper@37906
|
1195 |
afterins;
|
neuper@37906
|
1196 |
print_depth 3;
|
neuper@37906
|
1197 |
if afterins = [([1], Frm), ([1], Res), ([2], Frm), ([2], Res)
|
neuper@37906
|
1198 |
(*, WN060727 removed after replacing cutlevup by test_trans:([], Res)*)]
|
neuper@37906
|
1199 |
then () else
|
neuper@38031
|
1200 |
error "ctree.sml: diff:behav. in complete pt: append_atomic[2] afterins";
|
neuper@37906
|
1201 |
show_pt pt';
|
neuper@37906
|
1202 |
(*
|
neuper@37906
|
1203 |
val p = move_dn [] pt' ([],Pbl) (*-> ([1],Frm)*);
|
neuper@37906
|
1204 |
val p = move_dn [] pt' p (*-> ([1],Res)*);
|
neuper@37906
|
1205 |
val p = move_dn [] pt' p (*-> ([2],Frm)*);
|
neuper@37906
|
1206 |
val p = move_dn [] pt' p (*-> ([2],Res)*);
|
neuper@37906
|
1207 |
|
neuper@37906
|
1208 |
term2str (get_obj g_form pt' [2]);
|
neuper@37906
|
1209 |
term2str (get_obj g_res pt' [2]);
|
neuper@37906
|
1210 |
ostate2str (get_obj g_ostate pt' [2]);
|
neuper@37906
|
1211 |
*)
|
neuper@37906
|
1212 |
|
neuper@37906
|
1213 |
"---(4) on S(606)..S(608)--------";
|
neuper@37906
|
1214 |
val (pt', cuts) = cappend_problem pt [3] e_istate ([],e_spec)
|
neuper@37906
|
1215 |
([],e_spec, str2term "Inhead[3]");
|
neuper@37906
|
1216 |
print_depth 99;
|
neuper@37906
|
1217 |
cuts;
|
neuper@37906
|
1218 |
print_depth 3;
|
neuper@37906
|
1219 |
if cuts = [([3], Pbl),
|
neuper@37906
|
1220 |
([3, 1], Frm), ([3, 1], Res),
|
neuper@37906
|
1221 |
([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
|
neuper@37906
|
1222 |
([3, 2], Res),
|
neuper@37906
|
1223 |
([3], Res), ([4], Res),
|
neuper@37906
|
1224 |
(*WN060727 added after replacing cutlevup by test_trans*)([], Res)] then ()else
|
neuper@38031
|
1225 |
error "ctree.sml: diff:behav. in ccomplete pt: append_problem[3] cuts";
|
neuper@37906
|
1226 |
val afterins = get_allp [] ([], ([],Frm)) pt';
|
neuper@37906
|
1227 |
print_depth 99;
|
neuper@37906
|
1228 |
afterins;
|
neuper@37906
|
1229 |
print_depth 3;
|
neuper@37906
|
1230 |
if afterins =
|
neuper@37906
|
1231 |
[([1], Frm), ([1], Res),([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
|
neuper@37906
|
1232 |
([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res),
|
neuper@37906
|
1233 |
([3], Pbl)] then () else
|
neuper@38031
|
1234 |
error "ctree.sml: diff:behav.in complete pt: append_problem[3] afterins";
|
neuper@37906
|
1235 |
(* use"systest/ctree.sml";
|
neuper@37906
|
1236 |
use"ctree.sml";
|
neuper@37906
|
1237 |
*)
|
neuper@37906
|
1238 |
|
neuper@37906
|
1239 |
"---(6-1) on S(606)..S(608)--------";
|
neuper@37906
|
1240 |
val (pt', cuts) = cappend_atomic pt [3,1] e_istate (str2term "Inform[3,1]")
|
neuper@37906
|
1241 |
(Tac "test") (str2term "Inres[3,1]",[]) Complete;
|
neuper@37906
|
1242 |
print_depth 99;
|
neuper@37906
|
1243 |
cuts;
|
neuper@37906
|
1244 |
print_depth 3;
|
neuper@37906
|
1245 |
if cuts = [([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
|
neuper@37906
|
1246 |
([3, 2], Res),
|
neuper@37906
|
1247 |
(*WN060727 added*)([3], Res), ([4], Res), ([], Res)] then () else
|
neuper@38031
|
1248 |
error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] cuts";
|
neuper@37906
|
1249 |
val afterins = get_allp [] ([], ([],Frm)) pt';
|
neuper@37906
|
1250 |
print_depth 99;
|
neuper@37906
|
1251 |
afterins;
|
neuper@37906
|
1252 |
print_depth 3;
|
neuper@37906
|
1253 |
(*WN060727 replaced after overwriting cutlevup by test_trans
|
neuper@37906
|
1254 |
if afterins = [([1], Frm), ([1], Res),
|
neuper@37906
|
1255 |
([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
|
neuper@37906
|
1256 |
([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
|
neuper@37906
|
1257 |
([2], Res),
|
neuper@37906
|
1258 |
([3], Pbl),
|
neuper@37906
|
1259 |
([3, 1], Frm), ([3, 1], Res)(*replaced*), (*([3, 2], Res) cut!*)
|
neuper@37906
|
1260 |
([3], Res)(*cutlevup=false*),
|
neuper@37906
|
1261 |
([4], Res),
|
neuper@37906
|
1262 |
([], Res)(*cutlevup=false*)] then () else
|
neuper@38031
|
1263 |
error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] insrtd";
|
neuper@37906
|
1264 |
*)
|
neuper@37906
|
1265 |
if afterins = [([1], Frm), ([1], Res),
|
neuper@37906
|
1266 |
([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
|
neuper@37906
|
1267 |
([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
|
neuper@37906
|
1268 |
([2], Res),
|
neuper@37906
|
1269 |
([3], Pbl),
|
neuper@37906
|
1270 |
([3, 1], Frm), ([3, 1], Res)] then () else
|
neuper@38031
|
1271 |
error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] insrtd";
|
neuper@37906
|
1272 |
|
neuper@37906
|
1273 |
if term2str (get_obj g_form pt' [3,1]) = "Inform [3, 1]" then () else
|
neuper@38031
|
1274 |
error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] Inform";
|
neuper@37906
|
1275 |
|
neuper@37906
|
1276 |
"---(6) on S(606)..S(608)--------";
|
neuper@37906
|
1277 |
val (pt', cuts) = cappend_atomic pt [3,2] e_istate (str2term "Inform[3,2]")
|
neuper@37906
|
1278 |
(Tac "test") (str2term "Inres[3,2]",[]) Complete;
|
neuper@37906
|
1279 |
print_depth 99;
|
neuper@37906
|
1280 |
cuts;
|
neuper@37906
|
1281 |
print_depth 3;
|
neuper@37906
|
1282 |
if cuts = [(*just after is: cutlevup=false in [3]*)
|
neuper@37906
|
1283 |
(*WN060727 after test_trans instead cutlevup added:*)
|
neuper@37906
|
1284 |
([3], Res), ([4], Res), ([], Res)] then () else
|
neuper@38031
|
1285 |
error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] cuts";
|
neuper@37906
|
1286 |
val afterins = get_allp [] ([], ([],Frm)) pt';
|
neuper@37906
|
1287 |
print_depth 99;
|
neuper@37906
|
1288 |
afterins;
|
neuper@37906
|
1289 |
print_depth 3;
|
neuper@37906
|
1290 |
(*WN060727 replaced after overwriting cutlevup by test_trans
|
neuper@37906
|
1291 |
if afterins = [([1], Frm), ([1], Res),
|
neuper@37906
|
1292 |
([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
|
neuper@37906
|
1293 |
([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
|
neuper@37906
|
1294 |
([2], Res),
|
neuper@37906
|
1295 |
([3], Pbl),
|
neuper@37906
|
1296 |
([3, 1], Frm), ([3, 1], Res), ([3, 2], Frm), ([3, 2], Res),
|
neuper@37906
|
1297 |
([3], Res),
|
neuper@37906
|
1298 |
([4], Res), ([], Res)] then () else
|
neuper@38031
|
1299 |
error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] insrtd";
|
neuper@37906
|
1300 |
*)
|
neuper@37906
|
1301 |
if afterins = [([1], Frm), ([1], Res),
|
neuper@37906
|
1302 |
([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
|
neuper@37906
|
1303 |
([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
|
neuper@37906
|
1304 |
([2], Res),
|
neuper@37906
|
1305 |
([3], Pbl),
|
neuper@37906
|
1306 |
([3, 1], Frm), ([3, 1], Res), ([3, 2], Frm), ([3, 2], Res)]
|
neuper@37906
|
1307 |
then () else
|
neuper@38031
|
1308 |
error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] insrtd";
|
neuper@37906
|
1309 |
|
neuper@37906
|
1310 |
if term2str (get_obj g_form pt' [3,2]) = "Inform [3, 2]" then () else
|
neuper@38031
|
1311 |
error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] Inform";
|
neuper@37906
|
1312 |
|
neuper@37906
|
1313 |
"---(6++) on S(606)..S(608)--------";
|
neuper@37906
|
1314 |
(**)
|
neuper@37906
|
1315 |
val (pt', cuts) = cappend_atomic pt [3,2,1] e_istate (str2term "Inform[3,2,1]")
|
neuper@37906
|
1316 |
(Tac "test") (str2term "Inres[3,2,1]",[]) Complete;
|
neuper@37906
|
1317 |
print_depth 99;
|
neuper@37906
|
1318 |
cuts;
|
neuper@37906
|
1319 |
print_depth 1;
|
neuper@37906
|
1320 |
if cuts = [([3, 2, 2], Res), ([3, 2], Res),
|
neuper@37906
|
1321 |
(*WN060727 {cutlevup->test_trans} added:*)([3], Res), ([4], Res), ([], Res)]
|
neuper@37906
|
1322 |
then () else
|
neuper@38031
|
1323 |
error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2,1] cuts";
|
neuper@37906
|
1324 |
val afterins = get_allp [] ([], ([],Frm)) pt';
|
neuper@37906
|
1325 |
print_depth 99;
|
neuper@37906
|
1326 |
afterins;
|
neuper@37906
|
1327 |
print_depth 3;
|
neuper@37906
|
1328 |
if afterins = [([1], Frm), ([1], Res),
|
neuper@37906
|
1329 |
([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
|
neuper@37906
|
1330 |
([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
|
neuper@37906
|
1331 |
([2], Res),
|
neuper@37906
|
1332 |
([3], Pbl),
|
neuper@37906
|
1333 |
([3, 1], Frm), ([3, 1], Res),
|
neuper@37906
|
1334 |
([3, 2, 1], Frm), ([3, 2, 1], Res)] then () else
|
neuper@38031
|
1335 |
error "ctree.sml: diff:behav. in complete pt: append_atom[3,2,1] insrtd";
|
neuper@37906
|
1336 |
if term2str (get_obj g_form pt' [3,2,1]) = "Inform [3, 2, 1]" then () else
|
neuper@38031
|
1337 |
error "ctree.sml: diff:behav. complete pt: append_atomic[3,2,1] Inform";
|
neuper@37906
|
1338 |
(*
|
neuper@37906
|
1339 |
show_pt pt';
|
neuper@37906
|
1340 |
show_pt pt;
|
neuper@37906
|
1341 |
*)
|
neuper@37906
|
1342 |
|
neuper@41938
|
1343 |
===== inhibit exn ?===========================================================*)
|