1.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml Mon Jun 21 22:08:01 2021 +0200
1.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml Sun Jul 18 18:15:27 2021 +0200
1.3 @@ -1,4 +1,4 @@
1.4 -(* Title: "ProgLang/rewrite.sml"
1.5 +(* Title: "MathEngBasic/rewrite.sml"
1.6 Author: Walther Neuper 050908
1.7 (c) copyright due to lincense terms.
1.8 *)
1.9 @@ -256,21 +256,21 @@
1.10
1.11 val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
1.12 writeln "---------- rewrite_terms_ 1---------------------------";
1.13 -if UnparseC.term t' = "M_b 0 = -1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
1.14 +if UnparseC.term t' = "M_b 0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
1.15 else error "rewrite.sml rewrite_terms_ [x = 0]";
1.16
1.17 val equs = [TermC.str2term "M_b 0 = 0"];
1.18 -val t = TermC.str2term "M_b 0 = -1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2";
1.19 +val t = TermC.str2term "M_b 0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2";
1.20 val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
1.21 writeln "---------- rewrite_terms_ 2---------------------------";
1.22 -if UnparseC.term t' = "0 = -1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
1.23 +if UnparseC.term t' = "0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
1.24 else error "rewrite.sml rewrite_terms_ [M_b 0 = 0]";
1.25
1.26 val equs = [TermC.str2term "x = 0", TermC.str2term"M_b 0 = 0"];
1.27 -val t = TermC.str2term "M_b x = -1 * q_0 * x \<up> 2 / 2 + x * c + c_2";
1.28 +val t = TermC.str2term "M_b x = - 1 * q_0 * x \<up> 2 / 2 + x * c + c_2";
1.29 val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
1.30 writeln "---------- rewrite_terms_ 3---------------------------";
1.31 -if UnparseC.term t' = "0 = -1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
1.32 +if UnparseC.term t' = "0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
1.33 else error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]";
1.34
1.35
1.36 @@ -295,7 +295,7 @@
1.37 (writeln o UnparseC.term) t;
1.38 if UnparseC.term t = "L * c_3 + c_4 = 0 + -1 * (-1 * (q_0 * L \<up> 2) / 2)"
1.39 then () else error "rewrite.sml rewrite_inst_ bdvs";
1.40 -> Rewrite.trace_on:=true;
1.41 +> Rewrite.trace_on:=true;false
1.42 Rewrite.trace_on:=false;--------------------------------------------*)
1.43
1.44
1.45 @@ -328,6 +328,7 @@
1.46 val asms = map (Envir.subst_term subst) pres;
1.47 if UnparseC.terms asms = "[\"a + b is_expanded\", \"c is_expanded\"]"
1.48 then () else error "rewrite.sml: prepat cancel subst";
1.49 +
1.50 if ([], true) = eval__true thy 0 asms [] erls
1.51 then () else error "rewrite.sml: prepat cancel eval__true";
1.52
1.53 @@ -360,6 +361,7 @@
1.54 val asms = map (Envir.subst_term subst) pres;
1.55 if UnparseC.terms asms = "[\"x \<up> 2 * x is_multUnordered\"]"
1.56 then () else error "rewrite.sml: prepat order_mult_ subst";
1.57 +
1.58 if ([], true) = eval__true thy 0 asms [] erls
1.59 then () else error "rewrite.sml: prepat order_mult_ eval__true";
1.60
1.61 @@ -371,7 +373,21 @@
1.62
1.63 if is_multUnordered t then () else error "rewrite.sml diff. is_multUnordered 2";
1.64 val tm = TermC.str2term "(x \<up> 2 * x) is_multUnordered";
1.65 -eval_is_multUnordered "testid" "" tm thy;
1.66 +
1.67 +(*+*)case eval_is_multUnordered "testid" "" tm thy of
1.68 +(*+*) SOME
1.69 +(*+*) ("testidx \<up> 2 * x_",
1.70 +(*+*) Const ("HOL.Trueprop", _) $
1.71 +(*+*) (Const ("HOL.eq", _) $
1.72 +(*+*) (Const ("Poly.is_multUnordered", _) $
1.73 +(*+*) (Const ("Groups.times_class.times", _) $
1.74 +(*+*) (Const ("Transcendental.powr", _) $ Free ("x", _) $ _ ) $ Free ("x", _))) $
1.75 +(*+*) Const ("HOL.True", _))) => ()
1.76 +(*+*)(* ^^^^^^ compare ---vvv *)
1.77 +(*+*)| _ => error "rewrite.sml diff. eval_is_multUnordered 2b CHANGED";
1.78 +
1.79 +
1.80 + eval_is_multUnordered "testid" "" tm thy;
1.81
1.82 case eval_is_multUnordered "testid" "" tm thy of
1.83 SOME (_, Const (\<^const_name>\<open>Trueprop\<close>, _) $
1.84 @@ -380,9 +396,9 @@
1.85 Const (\<^const_name>\<open>True\<close>, _))) => ()
1.86 | _ => error "rewrite.sml diff. eval_is_multUnordered 2b";
1.87
1.88 -tracing "----- begin rewrite x \<up> 2 * x ---"; Rewrite.trace_on := false;
1.89 +tracing "----- begin rewrite x \<up> 2 * x ---"; Rewrite.trace_on := false; (*true false*)
1.90 val SOME (t', _) = rewrite_set_ thy true order_mult_ t;
1.91 -tracing "----- end rewrite x \<up> 2 * x ---"; Rewrite.trace_on := false;
1.92 +tracing "----- end rewrite x \<up> 2 * x ---"; Rewrite.trace_on := false; (*true false*)
1.93 if UnparseC.term t' = "x * x \<up> 2" then ()
1.94 else error "rewrite.sml Poly.is_multUnordered doesn't work";
1.95
1.96 @@ -613,7 +629,7 @@
1.97
1.98 rewrite__set_ thy (i + 1) false bdv rls a (*of*);
1.99
1.100 -(*+*)Rewrite.trace_on := true;
1.101 +(*+*)Rewrite.trace_on := false; (*true false*)
1.102
1.103 (*this was False; vvvv--- means: indeterminate*)
1.104 val (* SOME (t, a') *)NONE = (*case*)
1.105 @@ -634,7 +650,7 @@
1.106 :
1.107 ### asms accepted: [x \<noteq> 0] stored: []
1.108 : *)
1.109 -Rewrite.trace_on := false;
1.110 +Rewrite.trace_on := false; (*true false*)
1.111 ( *\------- outcomment this code: otherwise the re-definition could infect tests lateron ------/*)
1.112
1.113
1.114 @@ -671,7 +687,7 @@
1.115 exception TERM raised (line 271 of "~~/src/HOL/Tools/hologic.ML"):
1.116 dest_eq
1.117 0 \<le> ?a \<Longrightarrow> (0 \<le> sqrt ?a) = True( **)
1.118 -if UnparseC.term t = "x + 1 + -1 * 2 = 0" then () else error "rewrite_set_ norm_equation CHANGED";
1.119 +if UnparseC.term t = "x + 1 + - 1 * 2 = 0" then () else error "rewrite_set_ norm_equation CHANGED";
1.120
1.121 "~~~~~ fun rewrite_set_ , args:"; val (thy, bool, rls, term) = (thy, false, rls, term);
1.122 "~~~~~ and rewrite__set_ , args:"; val (thy, i, put_asm, bdv, rls, ct) =