1.1 --- a/test/Tools/isac/Interpret/ctree.sml Tue Jul 26 09:38:07 2011 +0200
1.2 +++ b/test/Tools/isac/Interpret/ctree.sml Tue Jul 26 11:36:35 2011 +0200
1.3 @@ -225,7 +225,8 @@
1.4 error "ctree.sml: diff:behav. in cut_level 1aa2" (*WN050220*);
1.5
1.6 val (res,asm) = get_obj g_result pt' [];
1.7 -(*============ inhibit exn AK110725 ==============================================
1.8 +
1.9 +(*============ inhibit exn AK110726 ==============================================
1.10 if term2str res = "[x = 1]" (*WN050219 e_term in cut_tree!!!*) then () else
1.11 error "ctree.sml: diff:behav. in cut_level 1ab";
1.12 if map fst (get_interval ([],Frm) ([],Res) 9999 pt') =
1.13 @@ -235,8 +236,7 @@
1.14 ([2], Res),(*, e_term in cut_tree!!!*)
1.15 ([], Res)] then () else
1.16 error "ctree.sml: diff:behav. in cut_level 1b";
1.17 -============ inhibit exn AK110725 ==============================================*)
1.18 -
1.19 +============ inhibit exn AK110726 ==============================================*)
1.20
1.21 val (pt',cuts) = cut_level [] [] pt ([2],Res);
1.22 if cuts = [([3], Frm),
1.23 @@ -267,7 +267,8 @@
1.24 "-------------- cut_tree (from ptree above)-----------------------";
1.25 "-------------- cut_tree (from ptree above)-----------------------";
1.26 val (pt', cuts) = cut_tree pt ([2],Frm);(*not created by move_dn -- not on WS*)
1.27 -(*============ inhibit exn AK110725 ==============================================
1.28 +
1.29 +(*============ inhibit exn AK110726 ==============================================
1.30 if cuts = [([2], Res),
1.31 ([3], Frm),
1.32 ([3, 1], Frm),
1.33 @@ -279,13 +280,16 @@
1.34 then () else error "ctree.sml: diff:behav. in cut_tree 1a";
1.35
1.36 val (res,asm) = get_obj g_result pt' [2];
1.37 +============ inhibit exn AK110726 ==============================================*)
1.38 +
1.39 if res = e_term (*WN050219 done by cut_level*) then () else
1.40 error "ctree.sml: diff:behav. in cut_tree 1aa";
1.41
1.42 +(*============ inhibit exn AK110726 ==============================================
1.43 val form = get_obj g_form pt' [2];
1.44 if term2str form = "x + 1 + -1 * 2 = 0" (*remained !!!*) then () else
1.45 error "ctree.sml: diff:behav. in cut_tree 1ab";
1.46 -============ inhibit exn AK110725 ==============================================*)
1.47 +============ inhibit exn AK110726 ==============================================*)
1.48
1.49 val (res,asm) = get_obj g_result pt' [];
1.50 if res = e_term (*WN050219 done by cut_tree*) then () else
1.51 @@ -298,7 +302,7 @@
1.52 error "ctree.sml: diff:behav. in cut_tree 1ad";
1.53
1.54 val (pt', cuts) = cut_tree pt ([2],Res);
1.55 -(*============ inhibit exn AK110725 ==============================================
1.56 +(*============ inhibit exn AK110726 ==============================================
1.57 if cuts = [([3], Frm),
1.58 ([3, 1], Frm),
1.59 ([3, 1], Res),
1.60 @@ -307,17 +311,17 @@
1.61 ([4], Res),
1.62 ([], Res)]
1.63 then () else error "ctree.sml: diff:behav. in cut_tree 2";
1.64 -============ inhibit exn AK110725 ==============================================*)
1.65 +============ inhibit exn AK110726 ==============================================*)
1.66
1.67 val (pt', cuts) = cut_tree pt ([3,1],Frm);
1.68 -(*============ inhibit exn AK110725 ==============================================
1.69 +(*============ inhibit exn AK110726 ==============================================
1.70 if cuts = [([3, 1], Res),
1.71 ([3, 2], Res),
1.72 ([3], Res),
1.73 ([4], Res),
1.74 ([], Res)]
1.75 then () else error "ctree.sml: diff:behav. in cut_tree 3";
1.76 -============ inhibit exn AK110725 ==============================================*)
1.77 +============ inhibit exn AK110726 ==============================================*)
1.78
1.79 val (pt', cuts) = cut_tree pt ([3,1],Res);
1.80 if cuts = [([3, 2], Res),
1.81 @@ -545,8 +549,6 @@
1.82 "=====new ptree 3 ================================================";
1.83 "=====new ptree 3 ================================================";
1.84
1.85 -(*========== inhibit exn AK110719 ==============================================
1.86 -(* ERROR: get_pos *)
1.87 states:=[];
1.88 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.89 ("Test", ["sqroot-test","univariate","equation","test"],
1.90 @@ -556,7 +558,6 @@
1.91
1.92 val ((pt,_),_) = get_calc 1;
1.93 show_pt pt;
1.94 -============ inhibit exn AK110719 ============================================*)
1.95
1.96 "-------------- move_dn ------------------------------------------";
1.97 "-------------- move_dn ------------------------------------------";
1.98 @@ -577,11 +578,8 @@
1.99 (*
1.100 val p = (move_dn [] pt p) handle e => print_exn_G e;
1.101 Exception PTREE end of calculation*)
1.102 -(*========== inhibit exn AK110719 ==============================================
1.103 +
1.104 if p=([],Res) then () else error "ctree.sml: diff:behav. in move_dn";
1.105 -============ inhibit exn AK110719 ============================================*)
1.106 -
1.107 -
1.108
1.109 "-------------- move_dn: Frm -> Res ------------------------------";
1.110 "-------------- move_dn: Frm -> Res ------------------------------";
1.111 @@ -627,10 +625,8 @@
1.112 val p = move_up [] pt p; (*-> ([],Pbl)*)
1.113 (*val p = (move_up [] pt p) handle e => print_exn_G e;
1.114 Exception PTREE begin of calculation*)
1.115 -(*========== inhibit exn AK110719 ==============================================
1.116 +
1.117 if p=([],Pbl) then () else error "ctree.sml: diff.behav. in move_up";
1.118 -========== inhibit exn AK110719 ==============================================*)
1.119 -
1.120
1.121 "------ move into detail -----------------------------------------";
1.122 "------ move into detail -----------------------------------------";
1.123 @@ -834,7 +830,7 @@
1.124 end;
1.125
1.126 writeln(pr_ptree pr_short pt);
1.127 -(*========== inhibit exn AK110719 ==============================================
1.128 +
1.129 case get_trace pt [1,3] [4,1,1] of
1.130 [[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1]] => ()
1.131 | _ => error "diff.behav.in ctree.sml: get_interval lev 1a";
1.132 @@ -844,15 +840,21 @@
1.133 case get_trace pt [1,4] [4,3,1] of
1.134 [[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],[4,3],[4,3,1]] => ()
1.135 | _ => error "diff.behav.in ctree.sml: get_interval lev 1c";
1.136 +
1.137 +(*========== inhibit exn AK110719 ==============================================
1.138 case get_trace pt [4,2] [5] of
1.139 (*[([4,2],_),([4,3],_),([4,4],_),([4,4,1],_),([4,4,2],_),([4,4,3],_),
1.140 ([4,4,4],_),([4,4,5],_),([5],_)] => () ..with pt_form*)
1.141 [[4,2],[4,3],[4,3,1],[4,3,2],[4,3,3],[4,3,4],[4,3,5],[5]]=>()
1.142 | _ => error "diff.behav.in ctree.sml: get_interval lev 1d";
1.143 +========== inhibit exn AK110719 ==============================================*)
1.144 +
1.145 case get_trace pt [] [4,4,2] of
1.146 [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],
1.147 [4,3],[4,3,1],[4,3,2]] => ()
1.148 | _ => error "diff.behav.in ctree.sml: get_interval lev 1e";
1.149 +
1.150 +(*========== inhibit exn AK110719 ==============================================
1.151 case get_trace pt [] [] of
1.152 [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],
1.153 [4,3],[4,3,1],[4,3,2],[4,3,3],[4,3,4],[4,3,5],[5]] => ()
1.154 @@ -1174,9 +1176,9 @@
1.155 "-------------- cappend on complete ctree from above -------------";
1.156 show_pt pt;
1.157
1.158 -(*========== inhibit exn AK110719 ==============================================
1.159 -
1.160 "---(2) on S(606)..S(608)--------";
1.161 +(*========== inhibit exn AK110726 ==============================================
1.162 +(* ERROR: Can't unify istate to istate * Proof.context *)
1.163 val (pt', cuts) = cappend_atomic pt [1] e_istate (str2term "Inform[1]")
1.164 (Tac "test") (str2term "Inres[1]",[]) Complete;
1.165
1.166 @@ -1198,7 +1200,6 @@
1.167 (*, WN060727 removed after replacing cutlevup by test_trans:([], Res)*)] then()
1.168 else error "ctree.sml: diff:behav. in complete pt: append_atomic[1] afterins";
1.169 show_pt pt';
1.170 -
1.171 "---(3) on S(606)..S(608)--------";
1.172 show_pt pt;
1.173 val (pt', cuts) = cappend_atomic pt [2] e_istate (str2term "Inform[2]")
1.174 @@ -1206,21 +1207,27 @@
1.175 print_depth 99;
1.176 cuts;
1.177 print_depth 3;
1.178 +
1.179 if cuts = [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
1.180 ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res), ([3], Pbl),
1.181 ([3, 1], Frm),([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res),
1.182 ([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res),
1.183 (*WN060727 added after replacing cutlevup by test_trans:*) ([], Res)] then ()
1.184 else error "ctree.sml: diff:behav.in complete pt: append_atomic[2] cuts";
1.185 +
1.186 +
1.187 val afterins = get_allp [] ([], ([],Frm)) pt';
1.188 print_depth 99;
1.189 afterins;
1.190 print_depth 3;
1.191 +
1.192 if afterins = [([1], Frm), ([1], Res), ([2], Frm), ([2], Res)
1.193 (*, WN060727 removed after replacing cutlevup by test_trans:([], Res)*)]
1.194 then () else
1.195 error "ctree.sml: diff:behav. in complete pt: append_atomic[2] afterins";
1.196 show_pt pt';
1.197 +
1.198 +
1.199 (*
1.200 val p = move_dn [] pt' ([],Pbl) (*-> ([1],Frm)*);
1.201 val p = move_dn [] pt' p (*-> ([1],Res)*);
1.202 @@ -1362,4 +1369,5 @@
1.203 show_pt pt';
1.204 show_pt pt;
1.205 *)
1.206 -========== inhibit exn AK110719 ==============================================*)
1.207 +========== inhibit exn AK110726 ==============================================*)
1.208 +