1.1 --- a/src/Tools/isac/ProgLang/rewrite.sml Fri Oct 01 17:27:55 2010 +0200
1.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml Fri Oct 01 18:25:06 2010 +0200
1.3 @@ -190,10 +190,6 @@
1.4 (let val subst: Type.tyenv * Envir.tenv =
1.5 Pattern.match thy (pat, t)
1.6 (Vartab.empty, Vartab.empty)
1.7 - val _ = tracing ("app_rev: pres=------------------");
1.8 - val _ = tracing ("app_rev: pres=" ^ terms2str pres);
1.9 - val _ = tracing ("app_rev: pat =" ^ term2str pat);
1.10 - val _ = tracing ("app_rev: t =" ^ term2str t);
1.11 in snd (eval__true thy (i+1)
1.12 (map (Envir.subst_term subst) pres)
1.13 [] erls)
2.1 --- a/test/Tools/isac/Knowledge/poly.sml Fri Oct 01 17:27:55 2010 +0200
2.2 +++ b/test/Tools/isac/Knowledge/poly.sml Fri Oct 01 18:25:06 2010 +0200
2.3 @@ -5,7 +5,6 @@
2.4 12345678901234567890123456789012345678901234567890123456789012345678901234567890
2.5 10 20 30 40 50 60 70 80
2.6 *)
2.7 -
2.8 (*******************************************************************************
2.9 WN060104 'SPB' came into 'exp_IsacCore_Simp_Poly_Book.xml'
2.10 'SPO' came into 'exp_IsacCore_Simp_Poly_Other.xml'
2.11 @@ -30,8 +29,6 @@
2.12 "--------------------------------------------------------";
2.13 "--------------------------------------------------------";
2.14
2.15 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
2.16 --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
2.17
2.18 "-------- check is'_polyexp is_polyexp ------------------";
2.19 "-------- check is'_polyexp is_polyexp ------------------";
2.20 @@ -80,9 +77,7 @@
2.21 val scr_expand_binoms =
2.22 "Script Expand_binoms t_t = t_t";
2.23 *)
2.24 -val ---------------------------------------------- = "11111";
2.25 parse thy scr_expand_binoms;
2.26 -val ---------------------------------------------- = "22222";
2.27
2.28
2.29 "-------- investigate (new) uniary minus ----------------";
2.30 @@ -163,8 +158,13 @@
2.31 "-------- fun is_multUnordered --------------------------";
2.32 "-------- fun is_multUnordered --------------------------";
2.33 val thy = theory "Isac";
2.34 -(* 100928 trace_rewrite gives the following (first occurring) difference:
2.35 -:
2.36 +"===== works for a simple example, see rewrite.sml -- fun app_rev ===";
2.37 +val t = str2term "x^^^2 * x";
2.38 +val SOME (t', _) = rewrite_set_ thy true order_mult_ t;
2.39 +if term2str t' = "x * x ^^^ 2" then ()
2.40 +else error "poly.sml Poly.is'_multUnordered doesn't work";
2.41 +
2.42 +(* 100928 trace_rewrite shows the first occurring difference in 267b:
2.43 ### rls: order_mult_ on: 5 * x ^^^ 2 * (2 * x ^^^ 7) + 5 * x ^^^ 2 * 3 + (6 * x ^^^ 7 + 9) + (-1 * (3 * x ^^^ 5 * (6 * x ^^^ 4)) + -1 * (3 * x ^^^ 5 * -1) +
2.44 (-48 * x ^^^ 4 + 8))
2.45 ###### rls: e_rls-is_multUnordered on: p is_multUnordered
2.46 @@ -190,18 +190,9 @@
2.47 Const ("True", _))) => ()
2.48 | _ => error "poly.sml diff. eval_is_multUnordered";
2.49
2.50 -"----- rewrite_set_ ---";
2.51 -val SOME (t, _) = rewrite_set_ thy true order_mult_ tm;
2.52 -
2.53 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
2.54 --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
2.55 -
2.56 -
2.57 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
2.58 --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
2.59 -
2.60 -(*===== inhibit exn ?===========================================================
2.61 -
2.62 +"----- rewrite_set_ STILL DIDN'T WORK";
2.63 +val SOME (t, _) = rewrite_set_ thy true order_mult_ t;
2.64 +term2str t;
2.65
2.66
2.67 "-------- examples from textbook Schalk I ---------------";
2.68 @@ -337,7 +328,6 @@
2.69 if term2str t = "d ^^^ 3" then ()
2.70 else error "poly.sml: diff.behav. in make_polynomial 14";
2.71
2.72 -
2.73 (*---------------------------------------------------------------------*)
2.74 (*------------------ Bsple bei denen es Probleme gibt------------------*)
2.75 (*---------------------------------------------------------------------*)
2.76 @@ -432,8 +422,8 @@
2.77 "-------- Script 'simplification for_polynomials' -------";
2.78 "-------- Script 'simplification for_polynomials' -------";
2.79 val str =
2.80 -"Script SimplifyScript (t_::real) = \
2.81 -\ ((Rewrite_Set norm_Poly False) t_)";
2.82 +"Script SimplifyScript (t_t::real) = \
2.83 +\ ((Rewrite_Set norm_Poly False) t_t)";
2.84 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
2.85 atomty sc;
2.86
2.87 @@ -445,6 +435,9 @@
2.88 \- (3*x^^^5 + 8) * (6*x^^^4 - 1))",
2.89 "normalform N"];
2.90 "-----0 ---";
2.91 +(*===== inhibit exn ============================================================
2.92 +GOON
2.93 +
2.94 case refine fmz ["polynomial","simplification"]of
2.95 [Matches (["polynomial", "simplification"], _)] => ()
2.96 | _ => error "poly.sml diff.behav. in check pbl, refine";
2.97 @@ -564,7 +557,6 @@
2.98 val t1 = str2term "2 * b + (3 * a + 3 * b)";
2.99 val t2 = str2term "3 * a + (2 * b + 3 * b)";
2.100
2.101 -
2.102 ===== inhibit exn ?===========================================================*)
2.103
2.104