1.1 --- a/test/Tools/isac/Interpret/ctree.sml Wed Jul 27 08:46:09 2011 +0200
1.2 +++ b/test/Tools/isac/Interpret/ctree.sml Wed Jul 27 13:04:57 2011 +0200
1.3 @@ -229,6 +229,8 @@
1.4 (*============ inhibit exn AK110726 ==============================================
1.5 if term2str res = "[x = 1]" (*WN050219 e_term in cut_tree!!!*) then () else
1.6 error "ctree.sml: diff:behav. in cut_level 1ab";
1.7 +============ inhibit exn AK110726 ==============================================*)
1.8 +(*============ inhibit exn AK110726 ==============================================
1.9 if map fst (get_interval ([],Frm) ([],Res) 9999 pt') =
1.10 [([], Frm),
1.11 ([1], Frm),
1.12 @@ -290,6 +292,11 @@
1.13 if term2str form = "x + 1 + -1 * 2 = 0" (*remained !!!*) then () else
1.14 error "ctree.sml: diff:behav. in cut_tree 1ab";
1.15 ============ inhibit exn AK110726 ==============================================*)
1.16 +(* AK110727 Debuging
1.17 + (* get_obj g_form pt' [2];
1.18 + (* ERROR: exception PTREE "get_obj: pos = [2] does not exist"
1.19 + raised (line 908 /src/Tools/isac/Interpret/ctree.sml")*)*)
1.20 +"~~~~~ fun get_obj, args:"; val (f, (Nd (b, bs)) ,(p::ps)) = (g_form, pt', [2]);*)
1.21
1.22 val (res,asm) = get_obj g_result pt' [];
1.23 if res = e_term (*WN050219 done by cut_tree*) then () else
1.24 @@ -373,11 +380,6 @@
1.25
1.26
1.27
1.28 -
1.29 -
1.30 -
1.31 -
1.32 -
1.33 "=====new ptree 2 miniscript with mini-subpbl ====================";
1.34 "=====new ptree 2 miniscript with mini-subpbl ====================";
1.35 "=====new ptree 2 miniscript with mini-subpbl ====================";
1.36 @@ -841,6 +843,7 @@
1.37 [[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],[4,3],[4,3,1]] => ()
1.38 | _ => error "diff.behav.in ctree.sml: get_interval lev 1c";
1.39
1.40 +
1.41 (*========== inhibit exn AK110719 ==============================================
1.42 case get_trace pt [4,2] [5] of
1.43 (*[([4,2],_),([4,3],_),([4,4],_),([4,4,1],_),([4,4,2],_),([4,4,3],_),
2.1 --- a/test/Tools/isac/ProgLang/calculate.sml Wed Jul 27 08:46:09 2011 +0200
2.2 +++ b/test/Tools/isac/ProgLang/calculate.sml Wed Jul 27 13:04:57 2011 +0200
2.3 @@ -199,30 +199,21 @@
2.4 val thy = @{theory Test};
2.5 val t = (term_of o the o (parse thy)) "(-4) / 2";
2.6
2.7 -(*===== inhibit exn AK110725 ===========================================================
2.8 -(* ERROR: Exception Bind raised *)
2.9 -val SOME (_, t) = eval_cancel "xxx" "HOL.divide" t thy;
2.10 -===== inhibit exn AK110725 ===========================================================*)
2.11 +val SOME (_, t) = eval_cancel "xxx" "Rings.inverse_class.divide" t thy;
2.12
2.13 term2str t;
2.14 "-4 / 2 = (-2)";
2.15 (*-------------- but ... *)
2.16 val ct = "x + (-4) / 2";
2.17
2.18 -(*===== inhibit exn AK110725 ===========================================================
2.19 -(* ERROR: Value or constructor (thy') has not been declared
2.20 - AK: replacing with thy doesn't work either...*)
2.21 +val thy' = "Test"; (* added AK110727 *)
2.22 val (ct,_) = the (rewrite_set thy' false rls ct);
2.23 -===== inhibit exn AK110725 ===========================================================*)
2.24
2.25 "(-2) + x";
2.26 (*-------------- while ... *)
2.27 val ct = "(-4) / 2";
2.28
2.29 -(*===== inhibit exn AK110725 ===========================================================
2.30 -(* ERROR: Value or constructor (thy') has not been declared *)
2.31 val (ct,_) = the (rewrite_set thy' false rls ct);
2.32 -===== inhibit exn AK110725 ===========================================================*)
2.33
2.34 "-2";
2.35
2.36 @@ -237,6 +228,7 @@
2.37 (*val t = "2 + x" ... works*)
2.38
2.39 trace_rewrite:=true; (*3.6.03*)
2.40 +
2.41 val thy = "Test";
2.42 val rls = "Test_simplify";
2.43 val t = "(3+(1+2*x))/2";
2.44 @@ -328,10 +320,9 @@
2.45 " ================= calculate.sml:10.8.02 2002:///->/ ======== ";
2.46 " ----------------- rewriting works ? -----------------------";
2.47 val thy = (@{theory "Isac"});
2.48 -(*===== inhibit exn AK110725 ===========================================================
2.49 -(* ERROR: real_divide_1 has not been declared
2.50 - - replace with Rings.division_ring_class.divide_1 - see line 387 *)
2.51 - val prop = (#prop o rep_thm) real_divide_1;
2.52 +
2.53 + val prop = (#prop o rep_thm) @{thm divide_1};
2.54 +(* AK110727 changed real_divide_1 to @{thm divide_1} *)
2.55 atomty prop;
2.56
2.57 (*** -------------
2.58 @@ -341,9 +332,9 @@
2.59 *** . . . Var ((x, 0), real)
2.60 *** . . . Const ( 1, real)
2.61 *** . . Var ((x, 0), real) *)
2.62 - val prop' = (#prop o rep_thm o num_str) real_divide_1;
2.63 + val prop' = (#prop o rep_thm o num_str) @{thm divide_1};
2.64 +(* AK110727 changed real_divide_1 to @{thm divide_1} *)
2.65 atomty prop';
2.66 -===== inhibit exn AK110725 ===========================================================*)
2.67
2.68 (*** -------------
2.69 *** Const ( Trueprop, bool => prop)
2.70 @@ -369,8 +360,8 @@
2.71 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
2.72 (*val t = Free ("aaa","RealDef.real") : term*)
2.73
2.74 -(*===== inhibit exn AK110725 ===========================================================
2.75 - val prop = (#prop o rep_thm) realpow_eq_one;
2.76 + val prop = (#prop o rep_thm) @{thm realpow_eq_oneI};
2.77 +(* AK110727 replaced realpow_eq_one with @{thm realpow_eq_oneI} *)
2.78 atomty prop;
2.79
2.80 (*** -------------
2.81 @@ -380,9 +371,9 @@
2.82 *** . . . Const ( 1, real)
2.83 *** . . . Var ((n, 0), nat)
2.84 *** . . Const ( 1, real) *)
2.85 - val prop' = (#prop o rep_thm o num_str) realpow_eq_one;
2.86 + val prop' = (#prop o rep_thm o num_str) @{thm realpow_eq_oneI};
2.87 +(* AK110727 replaced realpow_eq_one with @{thm realpow_eq_oneI} *)
2.88 atomty prop';
2.89 -===== inhibit exn AK110725 ===========================================================*)
2.90
2.91 (*** -------------
2.92 *** Const ( Trueprop, bool => prop)
2.93 @@ -403,10 +394,36 @@
2.94 *** Const ( Nat.power, [real, nat] => real)
2.95 *** . Free ( 1, real)
2.96 *** . Free ( aaa, nat) .......................... nat !!! *)
2.97 +
2.98 + val thm = num_str @{thm realpow_eq_oneI};
2.99 +(* AK110727 replaced realpow_eq_one with @{thm realpow_eq_oneI} *)
2.100 +
2.101 (*===== inhibit exn AK110725 ===========================================================
2.102 - val thm = num_str realpow_eq_one;
2.103 +(* ERROR: Exception Bind raised *)
2.104 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
2.105 ===== inhibit exn AK110725 ===========================================================*)
2.106 +(* (*AK110727 Debugging (not finished)*)
2.107 + rewrite_ thy tless_true tval_rls true thm t; (* returns NONE *)
2.108 +"~~~~~ fun rewrite_, args:"; val (thy, rew_ord, erls, bool, thm, term)
2.109 + = (thy, tless_true, tval_rls, true, thm, t);
2.110 + rewrite__ thy 1 [] rew_ord erls bool thm term; (* returns NONE *)
2.111 +
2.112 +"~~~~~ fun rewrite__, args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct)
2.113 + = (thy, 1, [], rew_ord, erls, bool, thm, term);
2.114 +
2.115 + rew_sub thy i bdv tless rls put_asm [(*root of the term*)]
2.116 + (((inst_bdv bdv) o norm o #prop o rep_thm) thm) ct; (* rew is FALSE -> returns SOME *)
2.117 + rew_sub;
2.118 +
2.119 + print_depth 999;
2.120 + val (t',asms,lrd,rew) =
2.121 + rew_sub thy i bdv tless rls put_asm [(*root of the term*)]
2.122 + (((inst_bdv bdv) o norm o #prop o rep_thm) thm) ct; (* rew is FALSE -> returns SOME *)
2.123 +
2.124 +"~~~~~ and rew_sub, args:";
2.125 + (* rew_sub returns (t1 $ t2,[], lrd, false) - see last line of function rew_sub *)
2.126 +*)
2.127 +
2.128 (*val t = Free ("1","RealDef.real") : term*)
2.129
2.130 " ================= calculate.sml: calculate_ 2002 =================== ";
3.1 --- a/test/Tools/isac/Test_Isac.thy Wed Jul 27 08:46:09 2011 +0200
3.2 +++ b/test/Tools/isac/Test_Isac.thy Wed Jul 27 13:04:57 2011 +0200
3.3 @@ -101,7 +101,7 @@
3.4 use "calcelems.sml"
3.5 use "ProgLang/termC.sml"
3.6 use "ProgLang/calculate.sml" (*part.*)
3.7 - use "ProgLang/rewrite.sml" (*part.*)
3.8 + use "ProgLang/rewrite.sml" (*?complete?*)
3.9 (*use "ProgLang/listC.sml" 2002*)
3.10 use "ProgLang/scrtools.sml" (*complete*)
3.11 use "ProgLang/tools.sml" (*complete*)
4.1 --- a/test/Tools/isac/Test_Some.thy Wed Jul 27 08:46:09 2011 +0200
4.2 +++ b/test/Tools/isac/Test_Some.thy Wed Jul 27 13:04:57 2011 +0200
4.3 @@ -7,7 +7,7 @@
4.4
4.5 ML{* writeln "**** run the test ***************************************" *}
4.6
4.7 -use"../../../test/Tools/isac/Interpret/appl.sml"
4.8 +use"../../../test/Tools/isac/ProgLang/rewrite.sml"
4.9
4.10 ML {*
4.11