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