1.1 --- a/test/Tools/isac/Interpret/ctree.sml Tue Jul 26 09:10:01 2011 +0200
1.2 +++ b/test/Tools/isac/Interpret/ctree.sml Tue Jul 26 09:38:07 2011 +0200
1.3 @@ -1,6 +1,3 @@
1.4 -
1.5 -
1.6 -
1.7 (* tests for sml/ME/ctree.sml
1.8 authors: Walther Neuper 060113
1.9 (c) due to copyright terms
1.10 @@ -202,6 +199,10 @@
1.11 then () else error "ctree.sml: diff:behav. in get_allpos' 6";
1.12
1.13
1.14 +
1.15 +
1.16 +
1.17 +
1.18 "-------------- cut_level (from ptree above)----------------------";
1.19 "-------------- cut_level (from ptree above)----------------------";
1.20 "-------------- cut_level (from ptree above)----------------------";
1.21 @@ -224,6 +225,7 @@
1.22 error "ctree.sml: diff:behav. in cut_level 1aa2" (*WN050220*);
1.23
1.24 val (res,asm) = get_obj g_result pt' [];
1.25 +(*============ inhibit exn AK110725 ==============================================
1.26 if term2str res = "[x = 1]" (*WN050219 e_term in cut_tree!!!*) then () else
1.27 error "ctree.sml: diff:behav. in cut_level 1ab";
1.28 if map fst (get_interval ([],Frm) ([],Res) 9999 pt') =
1.29 @@ -233,6 +235,7 @@
1.30 ([2], Res),(*, e_term in cut_tree!!!*)
1.31 ([], Res)] then () else
1.32 error "ctree.sml: diff:behav. in cut_level 1b";
1.33 +============ inhibit exn AK110725 ==============================================*)
1.34
1.35
1.36 val (pt',cuts) = cut_level [] [] pt ([2],Res);
1.37 @@ -264,6 +267,7 @@
1.38 "-------------- cut_tree (from ptree above)-----------------------";
1.39 "-------------- cut_tree (from ptree above)-----------------------";
1.40 val (pt', cuts) = cut_tree pt ([2],Frm);(*not created by move_dn -- not on WS*)
1.41 +(*============ inhibit exn AK110725 ==============================================
1.42 if cuts = [([2], Res),
1.43 ([3], Frm),
1.44 ([3, 1], Frm),
1.45 @@ -281,6 +285,7 @@
1.46 val form = get_obj g_form pt' [2];
1.47 if term2str form = "x + 1 + -1 * 2 = 0" (*remained !!!*) then () else
1.48 error "ctree.sml: diff:behav. in cut_tree 1ab";
1.49 +============ inhibit exn AK110725 ==============================================*)
1.50
1.51 val (res,asm) = get_obj g_result pt' [];
1.52 if res = e_term (*WN050219 done by cut_tree*) then () else
1.53 @@ -293,6 +298,7 @@
1.54 error "ctree.sml: diff:behav. in cut_tree 1ad";
1.55
1.56 val (pt', cuts) = cut_tree pt ([2],Res);
1.57 +(*============ inhibit exn AK110725 ==============================================
1.58 if cuts = [([3], Frm),
1.59 ([3, 1], Frm),
1.60 ([3, 1], Res),
1.61 @@ -301,14 +307,17 @@
1.62 ([4], Res),
1.63 ([], Res)]
1.64 then () else error "ctree.sml: diff:behav. in cut_tree 2";
1.65 +============ inhibit exn AK110725 ==============================================*)
1.66
1.67 val (pt', cuts) = cut_tree pt ([3,1],Frm);
1.68 +(*============ inhibit exn AK110725 ==============================================
1.69 if cuts = [([3, 1], Res),
1.70 ([3, 2], Res),
1.71 ([3], Res),
1.72 ([4], Res),
1.73 ([], Res)]
1.74 then () else error "ctree.sml: diff:behav. in cut_tree 3";
1.75 +============ inhibit exn AK110725 ==============================================*)
1.76
1.77 val (pt', cuts) = cut_tree pt ([3,1],Res);
1.78 if cuts = [([3, 2], Res),
1.79 @@ -317,7 +326,6 @@
1.80 ([], Res)]
1.81 then () else error "ctree.sml: diff:behav. in cut_tree 4";
1.82
1.83 -
1.84 "=====new ptree 1a miniscript with mini-subpbl ===================";
1.85 "=====new ptree 1a miniscript with mini-subpbl ===================";
1.86 "=====new ptree 1a miniscript with mini-subpbl ===================";
1.87 @@ -357,7 +365,14 @@
1.88 show_pt pt';
1.89 print_depth 99;cuts;print_depth 3;
1.90 print_depth 99;map fst (get_interval ([],Frm) ([],Res) 9999 pt');print_depth 3;
1.91 -####################################################################*)*)
1.92 +####################################################################*)
1.93 +
1.94 +
1.95 +
1.96 +
1.97 +
1.98 +
1.99 +
1.100
1.101 "=====new ptree 2 miniscript with mini-subpbl ====================";
1.102 "=====new ptree 2 miniscript with mini-subpbl ====================";
1.103 @@ -724,6 +739,9 @@
1.104 writeln(pr_ptree pr_short pt);
1.105
1.106
1.107 +
1.108 +
1.109 +
1.110 "-------------- get_interval from ctree: incremental development--";
1.111 "-------------- get_interval from ctree: incremental development--";
1.112 "-------------- get_interval from ctree: incremental development--";
1.113 @@ -816,6 +834,7 @@
1.114 end;
1.115
1.116 writeln(pr_ptree pr_short pt);
1.117 +(*========== inhibit exn AK110719 ==============================================
1.118 case get_trace pt [1,3] [4,1,1] of
1.119 [[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1]] => ()
1.120 | _ => error "diff.behav.in ctree.sml: get_interval lev 1a";
1.121 @@ -825,18 +844,15 @@
1.122 case get_trace pt [1,4] [4,3,1] of
1.123 [[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],[4,3],[4,3,1]] => ()
1.124 | _ => error "diff.behav.in ctree.sml: get_interval lev 1c";
1.125 -(*========== inhibit exn AK110719 ==============================================
1.126 case get_trace pt [4,2] [5] of
1.127 (*[([4,2],_),([4,3],_),([4,4],_),([4,4,1],_),([4,4,2],_),([4,4,3],_),
1.128 ([4,4,4],_),([4,4,5],_),([5],_)] => () ..with pt_form*)
1.129 [[4,2],[4,3],[4,3,1],[4,3,2],[4,3,3],[4,3,4],[4,3,5],[5]]=>()
1.130 | _ => error "diff.behav.in ctree.sml: get_interval lev 1d";
1.131 -========== inhibit exn AK110719 ==============================================*)
1.132 case get_trace pt [] [4,4,2] of
1.133 [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],
1.134 [4,3],[4,3,1],[4,3,2]] => ()
1.135 | _ => error "diff.behav.in ctree.sml: get_interval lev 1e";
1.136 -(*========== inhibit exn AK110719 ==============================================
1.137 case get_trace pt [] [] of
1.138 [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],
1.139 [4,3],[4,3,1],[4,3,2],[4,3,3],[4,3,4],[4,3,5],[5]] => ()
1.140 @@ -1347,7 +1363,3 @@
1.141 show_pt pt;
1.142 *)
1.143 ========== inhibit exn AK110719 ==============================================*)
1.144 -
1.145 -
1.146 -
1.147 -
2.1 --- a/test/Tools/isac/Test_Some.thy Tue Jul 26 09:10:01 2011 +0200
2.2 +++ b/test/Tools/isac/Test_Some.thy Tue Jul 26 09:38:07 2011 +0200
2.3 @@ -7,12 +7,27 @@
2.4
2.5 ML{* writeln "**** run the test ***************************************" *}
2.6
2.7 -use"../../../test/Tools/isac/Interpret/calchead.sml"
2.8 +use"../../../test/Tools/isac/Interpret/ctree.sml"
2.9
2.10 ML {*
2.11
2.12
2.13
2.14 +
2.15 +
2.16 +
2.17 +
2.18 +
2.19 +
2.20 +
2.21 +
2.22 +
2.23 +
2.24 +
2.25 +
2.26 +
2.27 +
2.28 +
2.29 *}
2.30 ML{*
2.31 *}