1.1 --- a/test/Tools/isac/ProgLang/rewrite.sml Tue Sep 28 13:30:29 2010 +0200
1.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml Fri Oct 01 10:23:38 2010 +0200
1.3 @@ -1,6 +1,6 @@
1.4 -(* tests for ME/rewrite.sml
1.5 +(* Title: tests for ProgLang/rewrite.sml
1.6 TODO.WN0509 collect typical tests from systest here !!!!!
1.7 - author: Walther Neuper 050908
1.8 + Author: Walther Neuper 050908
1.9 (c) copyright due to lincense terms.
1.10
1.11 12345678901234567890123456789012345678901234567890123456789012345678901234567890
1.12 @@ -17,10 +17,13 @@
1.13 "----------- step through 'fun rewrite_terms_' ---------";
1.14 "----------- rewrite_inst_ bdvs -------------------------";
1.15 "----------- check diff 2002--2009-3 --------------------";
1.16 +"----------- fun app_rev, Rrls, prepat ------------------";
1.17 "--------------------------------------------------------";
1.18 "--------------------------------------------------------";
1.19 "--------------------------------------------------------";
1.20
1.21 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
1.22 +
1.23 "----------- assemble rewrite ---------------------------";
1.24 "----------- assemble rewrite ---------------------------";
1.25 "----------- assemble rewrite ---------------------------";
1.26 @@ -336,9 +339,102 @@
1.27 trace_rewrite := false; (*<<<<<<<<<<<<<<<<<<<<<###############################*)
1.28 "--------------------------------------------------------";
1.29
1.30 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
1.31
1.32 -(*===== inhibit exn ============================================================
1.33 -===== inhibit exn ============================================================*)
1.34 +"----------- fun app_rev, Rrls, prepat ------------------";
1.35 +"----------- fun app_rev, Rrls, prepat ------------------";
1.36 +"----------- fun app_rev, Rrls, prepat ------------------";
1.37 +(* Christian Urban, 101001
1.38 +theory Test
1.39 +imports Main Complex
1.40 +begin
1.41 +
1.42 +ML {*
1.43 +let
1.44 + val parser = Args.context -- Scan.lift Args.name_source
1.45 + fun term_pat (ctxt, str) = str |> ProofContext.read_term_pattern ctxt
1.46 + |> ML_Syntax.print_term |> ML_Syntax.atomic
1.47 +in
1.48 + ML_Antiquote.inline "term_pat" (parser >> term_pat)
1.49 +end
1.50 +*}
1.51 +
1.52 +ML {*
1.53 + val t = @{term "a + b * x = (0 ::real)"};
1.54 + val pat = @{term_pat "?l = (?r ::real)"};
1.55 + val precond = @{term_pat "is_polynomial (?l::real)"};
1.56 + val inst = Pattern.match @{theory} (pat, t) (Vartab.empty, Vartab.empty);
1.57 +*}
1.58 +
1.59 +ML {*
1.60 + Envir.subst_term inst precond
1.61 + |> Syntax.string_of_term @{context}
1.62 + |> writeln
1.63 +*}
1.64 +end *)
1.65 +val t = @{term "a + b * x = (0 ::real)"};
1.66 +val pat = parse_patt thy "?l = (?r ::real)";
1.67 +val precond = parse_patt thy "is_polynomial (?l::real)";(*no infix def*)
1.68 +val precond = parse_patt thy " (?l::real) is_expanded";
1.69 +
1.70 +val inst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
1.71 +val preinst = Envir.subst_term inst precond;
1.72 +term2str preinst;
1.73 +
1.74 +"===== Rational.thy: cancel ===";
1.75 +(* pat matched with the current term gives an environment
1.76 + (or not: hen the Rrls not applied);
1.77 + if pre1 and pre2 evaluate to HOLogic.true_const in this environment,
1.78 + then the Rrls is applied. *)
1.79 +val t = str2term "(a + b) / c ::real";
1.80 +val pat = parse_patt thy "?r / ?s ::real";
1.81 +val pres = [parse_patt thy "?r is_expanded", parse_patt thy "?s is_expanded"];
1.82 +val prepat = [(pres, pat)];
1.83 +val erls = rational_erls;
1.84 +(* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
1.85 +
1.86 +val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
1.87 +val asms = map (Envir.subst_term subst) pres;
1.88 +if terms2str asms = "[\"a + b is_expanded\",\"c is_expanded\"]"
1.89 +then () else error "rewrite.sml: prepat cancel subst";
1.90 +if ([], true) = eval__true thy 0 asms [] erls
1.91 +then () else error "rewrite.sml: prepat cancel eval__true";
1.92 +
1.93 +"===== Rational.thy: common_nominator_p ===";
1.94 +(* if each pat* matches with the current term, the Rrls is applied
1.95 + (there are no preconditions to be checked, they are HOLogic.true_const) *)
1.96 +val t = str2term "a / b + 1 / 2";
1.97 +val pat = parse_patt thy "?r / ?s + ?u / ?v";
1.98 +val pres = [HOLogic.true_const];
1.99 +val prepat = [(pres, pat)];
1.100 +val erls = rational_erls;
1.101 +(* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
1.102 +
1.103 +val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
1.104 +if ([], true) = eval__true thy 0 (map (Envir.subst_term subst) pres) [] erls
1.105 +then () else error "rewrite.sml: prepat common_nominator_p";
1.106 +
1.107 +"===== Poly.thy: order_mult_ ===";
1.108 + (* ?p matched with the current term gives an environment,
1.109 + which evaluates (the instantiated) "p is_multUnordered" to true*)
1.110 +val t = str2term "x^^^2 * x";
1.111 +val pat = parse_patt thy "?p :: real"
1.112 +val pres = [parse_patt thy "?p is_multUnordered"];
1.113 +val prepat = [(pres, pat)];
1.114 +val erls = append_rls "e_rls-is_multUnordered" e_rls
1.115 + [Calc ("Poly.is'_multUnordered",
1.116 + eval_is_multUnordered "")];
1.117 +
1.118 +val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
1.119 +val asms = map (Envir.subst_term subst) pres;
1.120 +if terms2str asms = "[\"x ^^^ 2 * x is_multUnordered\"]"
1.121 +then () else error "rewrite.sml: prepat order_mult_ subst";
1.122 +if ([], true) = eval__true thy 0 asms [] erls
1.123 +then () else error "rewrite.sml: prepat order_mult_ eval__true";
1.124 +
1.125 +
1.126 +(*========== inhibit exn =======================================================
1.127 +============ inhibit exn =====================================================*)
1.128
1.129 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
1.130 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)