1.1 --- a/test/Tools/isac/ProgLang/rewrite.sml Fri Oct 01 16:29:33 2010 +0200
1.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml Fri Oct 01 17:27:55 2010 +0200
1.3 @@ -17,12 +17,12 @@
1.4 "----------- step through 'fun rewrite_terms_' ---------";
1.5 "----------- rewrite_inst_ bdvs -------------------------";
1.6 "----------- check diff 2002--2009-3 --------------------";
1.7 -"----------- fun app_rev, Rrls, prepat ------------------";
1.8 +"----------- compare all prepat's existing 2010 ---------";
1.9 +"----------- fun app_rev, Rrls, -------------------------";
1.10 "--------------------------------------------------------";
1.11 "--------------------------------------------------------";
1.12 "--------------------------------------------------------";
1.13
1.14 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
1.15
1.16 "----------- assemble rewrite ---------------------------";
1.17 "----------- assemble rewrite ---------------------------";
1.18 @@ -339,11 +339,10 @@
1.19 trace_rewrite := false; (*<<<<<<<<<<<<<<<<<<<<<###############################*)
1.20 "--------------------------------------------------------";
1.21
1.22 --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
1.23
1.24 -"----------- fun app_rev, Rrls, prepat ------------------";
1.25 -"----------- fun app_rev, Rrls, prepat ------------------";
1.26 -"----------- fun app_rev, Rrls, prepat ------------------";
1.27 +"----------- compare all prepat's existing 2010 ---------";
1.28 +"----------- compare all prepat's existing 2010 ---------";
1.29 +"----------- compare all prepat's existing 2010 ---------";
1.30 (* Christian Urban, 101001
1.31 theory Test
1.32 imports Main Complex
1.33 @@ -372,10 +371,11 @@
1.34 |> writeln
1.35 *}
1.36 end *)
1.37 +val thy = theory "Isac";
1.38 val t = @{term "a + b * x = (0 ::real)"};
1.39 val pat = parse_patt thy "?l = (?r ::real)";
1.40 val precond = parse_patt thy "is_polynomial (?l::real)";(*no infix def*)
1.41 -val precond = parse_patt thy " (?l::real) is_expanded";
1.42 +val precond = parse_patt thy "(?l::real) is_expanded";
1.43
1.44 val inst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
1.45 val preinst = Envir.subst_term inst precond;
1.46 @@ -433,8 +433,94 @@
1.47 then () else error "rewrite.sml: prepat order_mult_ eval__true";
1.48
1.49
1.50 -(*========== inhibit exn =======================================================
1.51 -============ inhibit exn =====================================================*)
1.52 +"----------- fun app_rev, Rrls, -------------------------";
1.53 +"----------- fun app_rev, Rrls, -------------------------";
1.54 +"----------- fun app_rev, Rrls, -------------------------";
1.55 +val t = str2term "x^^^2 * x";
1.56 +if is_multUnordered t then () else error "rewrite.sml diff. is_multUnordered 2";
1.57 +val tm = str2term "(x^^^2 * x) is_multUnordered";
1.58 +case eval_is_multUnordered "testid" "" tm thy of
1.59 + SOME (_, Const ("Trueprop", _) $
1.60 + (Const ("op =", _) $
1.61 + (Const ("Poly.is'_multUnordered", _) $ _) $
1.62 + Const ("True", _))) => ()
1.63 + | _ => error "rewrite.sml diff. eval_is_multUnordered 2";
1.64 +
1.65 +tracing "----- begin rewrite x^^^2 * x ---"; trace_rewrite := true;
1.66 +val SOME (t', _) = rewrite_set_ thy true order_mult_ t;
1.67 +tracing "----- end rewrite x^^^2 * x ---"; trace_rewrite := false;
1.68 +if term2str t' = "x * x ^^^ 2" then ()
1.69 +else error "rewrite.sml Poly.is'_multUnordered doesn't work";
1.70 +
1.71 +(* for achieving the previous result, the following code was taken apart *)
1.72 +"----- rewrite__set_ ---";
1.73 +val (thy, i, _, _, (rrls as Rrls _), t) = (thy, 0, true, [], order_mult_, tm);
1.74 + val (t', asm, rew) = app_rev thy (i+1) rrls t;
1.75 +"----- app_rev ---";
1.76 +val (thy, i, rrls, t) = (thy, (i+1), rrls, t);
1.77 + fun chk_prepat thy erls [] t = true
1.78 + | chk_prepat thy erls prepat t =
1.79 + let fun chk (pres, pat) =
1.80 + (let val subst: Type.tyenv * Envir.tenv =
1.81 + Pattern.match thy (pat, t)
1.82 + (Vartab.empty, Vartab.empty)
1.83 + in snd (eval__true thy (i+1)
1.84 + (map (Envir.subst_term subst) pres)
1.85 + [] erls)
1.86 + end)
1.87 + handle _ => false
1.88 + fun scan_ f [] = false (*scan_ NEVER called by []*)
1.89 + | scan_ f (pp::pps) = if f pp then true
1.90 + else scan_ f pps;
1.91 + in scan_ chk prepat end;
1.92 +
1.93 + (*.apply the normal_form of a rev-set.*)
1.94 + fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t =
1.95 + if chk_prepat thy erls prepat t
1.96 + then ((*tracing("### app_rev': t = "^(term2str t));*)
1.97 + normal_form t)
1.98 + else NONE;
1.99 +(*fixme val NONE = app_rev' thy rrls t;*)
1.100 +"----- app_rev' ---";
1.101 +val (thy, Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}, t) = (thy, rrls, t);
1.102 +(*fixme false*) chk_prepat thy erls prepat t;
1.103 +"----- chk_prepat ---";
1.104 +val (thy, erls, prepat, t) = (thy, erls, prepat, t);
1.105 + fun chk (pres, pat) =
1.106 + (let val subst: Type.tyenv * Envir.tenv =
1.107 + Pattern.match thy (pat, t)
1.108 + (Vartab.empty, Vartab.empty)
1.109 + in snd (eval__true thy (i+1)
1.110 + (map (Envir.subst_term subst) pres)
1.111 + [] erls)
1.112 + end)
1.113 + handle _ => false;
1.114 + fun scan_ f [] = false (*scan_ NEVER called by []*)
1.115 + | scan_ f (pp::pps) = if f pp then true
1.116 + else scan_ f pps;
1.117 +tracing "=== poly.sml: scan_ chk prepat begin";
1.118 +scan_ chk prepat;
1.119 +tracing "=== poly.sml: scan_ chk prepat end";
1.120 +
1.121 +
1.122 +"----- chk ---";
1.123 +(*reestablish...*) val t = str2term "x ^^^ 2 * x";
1.124 +val [(pres, pat)] = prepat;
1.125 + val subst: Type.tyenv * Envir.tenv =
1.126 + Pattern.match thy (pat, t)
1.127 + (Vartab.empty, Vartab.empty);
1.128 +
1.129 +(*fixme: asms = ["p is_multUnordered"]...instantiate*)
1.130 +"----- eval__true ---";
1.131 +val asms = (map (Envir.subst_term subst) pres);
1.132 +if terms2str asms = "[\"x ^^^ 2 * x is_multUnordered\"]" then ()
1.133 +else error "rewrite.sml: diff. is_multUnordered, asms";
1.134 +val (thy, i, asms, bdv, rls) =
1.135 + (thy, (i+1), [str2term "(x^^^2 * x) is_multUnordered"],
1.136 + [] : (term * term) list, erls);
1.137 +case eval__true thy i asms bdv rls of
1.138 + ([], true) => ()
1.139 + | _ => error "rewrite.sml: diff. is_multUnordered, eval__true";
1.140
1.141 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
1.142 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)