1.1 --- a/test/Tools/isac/ProgLang/rewrite.sml Mon Sep 27 13:35:06 2010 +0200
1.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml Tue Sep 28 07:28:10 2010 +0200
1.3 @@ -14,7 +14,7 @@
1.4 "----------- test rewriting without Isac's thys ---------";
1.5 "----------- conditional rewriting without Isac's thys --";
1.6 "----------- step through 'and rew_sub': ----------------";
1.7 -"----------- rewrite_terms_ ----------------------------";
1.8 +"----------- step through 'fun rewrite_terms_' ---------";
1.9 "----------- rewrite_inst_ bdvs -------------------------";
1.10 "----------- check diff 2002--2009-3 --------------------";
1.11 "--------------------------------------------------------";
1.12 @@ -155,6 +155,7 @@
1.13 "----------- step through 'and rew_sub': ----------------";
1.14 "----------- step through 'and rew_sub': ----------------";
1.15 (*and make asms without Trueprop, beginning with the result:*)
1.16 +val tm = @{term "x*y / y::real"};
1.17 val (t', asm, _, _) = rew_sub thy 0 [] dummy_ord e_rls true [] (prop_of thm) tm;
1.18 show_types := false;
1.19 "----- evaluate arguments";
1.20 @@ -163,11 +164,11 @@
1.21 "----- step 1: lhs, rhs of rule";
1.22 val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
1.23 o Logic.strip_imp_concl) r;
1.24 -term2str r = "?b ~= (0::?'a) ==> ?a * ?b / ?b = ?a";
1.25 +term2str r = "?b ~= (0::?'a) ==> ?a * ?b / ?b = ?a";
1.26 term2str lhs = "?a * ?b / ?b"; term2str rhs = "?a";
1.27 "----- step 2: the rule instantiated";
1.28 - val r' = Envir.subst_term (Pattern.match thy (lhs, t)
1.29 - (Vartab.empty, Vartab.empty)) r;
1.30 + val r' = Envir.subst_term
1.31 + (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r;
1.32 term2str r' = "y ~= 0 ==> x * y / y = x";
1.33 "----- step 3: get the (instantiated) assumption(s)";
1.34 val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
1.35 @@ -185,28 +186,38 @@
1.36 o Logic.strip_imp_concl) r';
1.37 term2str t' = "x";
1.38
1.39 -(*===== inhibit exn ============================================================
1.40 -"----------- rewrite_terms_ ----------------------------";
1.41 -"----------- rewrite_terms_ ----------------------------";
1.42 -"----------- rewrite_terms_ ----------------------------";
1.43 -val subte = [str2term "x = 0"];
1.44 -val t = str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2";
1.45 -val SOME (t',_) = rewrite_terms_ thy dummy_ord Erls subte t; (*NONE..TODO*)
1.46 +"----------- step through 'fun rewrite_terms_' ---------";
1.47 +"----------- step through 'fun rewrite_terms_' ---------";
1.48 +"----------- step through 'fun rewrite_terms_' ---------";
1.49 +"----- step 0: args for rewrite_terms_, local fun";
1.50 +val (thy, ord, erls, equs, t) =
1.51 + (theory "Biegelinie", dummy_ord, Erls, [str2term "x = 0"],
1.52 + str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2");
1.53 +"----- step 1: args for rew_";
1.54 +val ((t', asm'), (rules as r::rs), t) = ((e_term, []), equs, t);
1.55 +"----- step 2: rew_sub";
1.56 +rew_sub thy 1 [] ord erls false [] (Trueprop $ r) t;
1.57 +"----- step 3: step through rew_sub -- inefficient: goes into subterms";
1.58 +
1.59 +
1.60 +val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t;
1.61 +writeln "----------- rewrite_terms_ 1---------------------------";
1.62 if term2str t' = "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
1.63 else raise error "rewrite.sml rewrite_terms_ [x = 0]";
1.64
1.65 -val subte = [str2term "M_b 0 = 0"];
1.66 -val t = str2term"M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2";
1.67 -val SOME (t',_) = rewrite_terms_ thy dummy_ord Erls subte t;
1.68 +val equs = [str2term "M_b 0 = 0"];
1.69 +val t = str2term "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2";
1.70 +val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t;
1.71 +writeln "----------- rewrite_terms_ 2---------------------------";
1.72 if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
1.73 else raise error "rewrite.sml rewrite_terms_ [M_b 0 = 0]";
1.74
1.75 -val subte = [str2term"x = 0", str2term"M_b 0 = 0"];
1.76 -val t = str2term"M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2";
1.77 -val SOME (t',_) = rewrite_terms_ thy dummy_ord Erls subte t;
1.78 +val equs = [str2term "x = 0", str2term"M_b 0 = 0"];
1.79 +val t = str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2";
1.80 +val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t;
1.81 +writeln "----------- rewrite_terms_ 3---------------------------";
1.82 if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
1.83 else raise error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]";
1.84 -===== inhibit exn ============================================================*)
1.85
1.86
1.87 "----------- rewrite_inst_ bdvs -------------------------";
1.88 @@ -233,6 +244,7 @@
1.89 trace_rewrite:=true;
1.90 trace_rewrite:=false;--------------------------------------------*)
1.91
1.92 +
1.93 "----------- check diff 2002--2009-3 --------------------";
1.94 "----------- check diff 2002--2009-3 --------------------";
1.95 "----------- check diff 2002--2009-3 --------------------";
1.96 @@ -323,3 +335,10 @@
1.97 (* ^^^^^ goes with '====== calc. to: False' above from beginning*)
1.98 trace_rewrite := false; (*<<<<<<<<<<<<<<<<<<<<<###############################*)
1.99 "--------------------------------------------------------";
1.100 +
1.101 +
1.102 +(*===== inhibit exn ============================================================
1.103 +===== inhibit exn ============================================================*)
1.104 +
1.105 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.
1.106 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.*)