1.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml Sun Jan 29 14:31:56 2023 +0100
1.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml Mon Jan 30 09:47:18 2023 +0100
1.3 @@ -245,8 +245,8 @@
1.4 "----------- step through 'fun rewrite_terms_' ------------------------------------------------";
1.5 "----- step 0: args for rewrite_terms_, local fun";
1.6 val (thy, ord, asm_rls, equs, t) =
1.7 - (@{theory "Biegelinie"}, Rewrite_Ord.function_empty, Rule_Set.Empty, [TermC.parse_test @{context} "x = 0"],
1.8 - TermC.parse_test @{context} "M_b x = -1 * q_0 * x \<up> 2 / 2 + x * c + c_2");
1.9 + (@{theory "Biegelinie"}, Rewrite_Ord.function_empty, Rule_Set.Empty, [ParseC.parse_test @{context} "x = 0"],
1.10 + ParseC.parse_test @{context} "M_b x = -1 * q_0 * x \<up> 2 / 2 + x * c + c_2");
1.11 "----- step 1: args for rew_";
1.12 val ((t', asm'), (rules as r::rs), t) = ((TermC.empty, []), equs, t);
1.13 "----- step 2: rew_sub";
1.14 @@ -259,15 +259,15 @@
1.15 if UnparseC.term t' = "M_b 0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
1.16 else error "rewrite.sml rewrite_terms_ [x = 0]";
1.17
1.18 -val equs = [TermC.parse_test @{context} "M_b 0 = 0"];
1.19 -val t = TermC.parse_test @{context} "M_b 0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2";
1.20 +val equs = [ParseC.parse_test @{context} "M_b 0 = 0"];
1.21 +val t = ParseC.parse_test @{context} "M_b 0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2";
1.22 val SOME (t', _) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty equs t;
1.23 writeln "---------- rewrite_terms_ 2---------------------------";
1.24 if UnparseC.term t' = "0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
1.25 else error "rewrite.sml rewrite_terms_ [M_b 0 = 0]";
1.26
1.27 -val equs = [TermC.parse_test @{context} "x = 0", TermC.parse_test @{context}"M_b 0 = 0"];
1.28 -val t = TermC.parse_test @{context} "M_b x = - 1 * q_0 * x \<up> 2 / 2 + x * c + c_2";
1.29 +val equs = [ParseC.parse_test @{context} "x = 0", ParseC.parse_test @{context}"M_b 0 = 0"];
1.30 +val t = ParseC.parse_test @{context} "M_b x = - 1 * q_0 * x \<up> 2 / 2 + x * c + c_2";
1.31 val SOME (t', _) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty equs t;
1.32 writeln "---------- rewrite_terms_ 3---------------------------";
1.33 if UnparseC.term t' = "0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
1.34 @@ -278,11 +278,11 @@
1.35 "----------- rewrite_inst_ bdvs ----------------------------------------------------------------";
1.36 "----------- rewrite_inst_ bdvs ----------------------------------------------------------------";
1.37 (*see smltest/Scripts/term_G.sml: inst_bdv 2*)
1.38 -val t = TermC.parse_test @{context}"-1 * (q_0 * L \<up> 2) / 2 + (L * c_3 + c_4) = 0";
1.39 -val bdvs = [(TermC.parse_test @{context}"bdv_1",TermC.parse_test @{context}"c"),
1.40 - (TermC.parse_test @{context}"bdv_2",TermC.parse_test @{context}"c_2"),
1.41 - (TermC.parse_test @{context}"bdv_3",TermC.parse_test @{context}"c_3"),
1.42 - (TermC.parse_test @{context}"bdv_4",TermC.parse_test @{context}"c_4")];
1.43 +val t = ParseC.parse_test @{context}"-1 * (q_0 * L \<up> 2) / 2 + (L * c_3 + c_4) = 0";
1.44 +val bdvs = [(ParseC.parse_test @{context}"bdv_1",ParseC.parse_test @{context}"c"),
1.45 + (ParseC.parse_test @{context}"bdv_2",ParseC.parse_test @{context}"c_2"),
1.46 + (ParseC.parse_test @{context}"bdv_3",ParseC.parse_test @{context}"c_3"),
1.47 + (ParseC.parse_test @{context}"bdv_4",ParseC.parse_test @{context}"c_4")];
1.48 (*------------ outcommented WN071210, after inclusion into ROOT.ML
1.49 val SOME (t,_) =
1.50 rewrite_inst_ thy e_rew_ord
1.51 @@ -317,7 +317,7 @@
1.52 (or not: hen the Rrls not applied);
1.53 if pre1 and pre2 evaluate to @{term True} in this environment,
1.54 then the Rrls is applied. *)
1.55 -val t = TermC.parse_test @{context} "(a + b) / c ::real";
1.56 +val t = ParseC.parse_test @{context} "(a + b) / c ::real";
1.57 val pat = TermC.parse_patt thy "?r / ?s ::real";
1.58 val pres = [TermC.parse_patt thy "?r is_expanded", TermC.parse_patt thy "?s is_expanded"];
1.59 val prepat = [(pres, pat)];
1.60 @@ -335,7 +335,7 @@
1.61 "===== Rational.thy: add_fractions_p ===";
1.62 (* if each pat* TermC.matches with the current term, the Rrls is applied
1.63 (there are no preconditions to be checked, they are @{term True}) *)
1.64 -val t = TermC.parse_test @{context} "a / b + 1 / 2";
1.65 +val t = ParseC.parse_test @{context} "a / b + 1 / 2";
1.66 val pat = TermC.parse_patt thy "?r / ?s + ?u / ?v";
1.67 val pres = [@{term True}];
1.68 val prepat = [(pres, pat)];
1.69 @@ -349,7 +349,7 @@
1.70 "===== Poly.thy: order_mult_ ===";
1.71 (* ?p matched with the current term gives an environment,
1.72 which evaluates (the instantiated) "p is_multUnordered" to true*)
1.73 -val t = TermC.parse_test @{context} "x \<up> 2 * x";
1.74 +val t = ParseC.parse_test @{context} "x \<up> 2 * x";
1.75 val pat = TermC.parse_patt thy "?p :: real"
1.76 val pres = [TermC.parse_patt thy "?p is_multUnordered"];
1.77 val prepat = [(pres, pat)];
1.78 @@ -369,10 +369,10 @@
1.79 "----------- fun app_rev, Rrls, ----------------------------------------------------------------";
1.80 "----------- fun app_rev, Rrls, ----------------------------------------------------------------";
1.81 "----------- fun app_rev, Rrls, ----------------------------------------------------------------";
1.82 -val t = TermC.parse_test @{context} "x \<up> 2 * x";
1.83 +val t = ParseC.parse_test @{context} "x \<up> 2 * x";
1.84
1.85 if is_multUnordered t then () else error "rewrite.sml diff. is_multUnordered 2";
1.86 -val tm = TermC.parse_test @{context} "(x \<up> 2 * x) is_multUnordered";
1.87 +val tm = ParseC.parse_test @{context} "(x \<up> 2 * x) is_multUnordered";
1.88
1.89 (*+*)case eval_is_multUnordered "testid" "" tm ctxt of
1.90 (*+*) SOME
1.91 @@ -453,7 +453,7 @@
1.92 tracing "=== poly.sml: scan_ chk prepat end";
1.93
1.94 "----- chk ---";
1.95 -(*reestablish...*) val t = TermC.parse_test @{context} "x \<up> 2 * x";
1.96 +(*reestablish...*) val t = ParseC.parse_test @{context} "x \<up> 2 * x";
1.97 val [(pres, pat)] = prepat;
1.98 val subst: Type.tyenv * Envir.tenv =
1.99 Pattern.match thy (pat, t)
1.100 @@ -465,7 +465,7 @@
1.101 if UnparseC.terms asms = "[\"x \<up> 2 * x is_multUnordered\"]" then ()
1.102 else error "rewrite.sml: diff. is_multUnordered, asms";
1.103 val (thy, i, asms, bdv, rls) =
1.104 - (thy, (i+1), [TermC.parse_test @{context} "(x \<up> 2 * x) is_multUnordered"],
1.105 + (thy, (i+1), [ParseC.parse_test @{context} "(x \<up> 2 * x) is_multUnordered"],
1.106 [] : Subst.T, asm_rls);
1.107 case eval__true ctxt i asms bdv rls of
1.108 ([], true) => ()
1.109 @@ -477,7 +477,7 @@
1.110 val thm = @{thm div_by_1};
1.111 val prop = Thm.prop_of thm;
1.112 TermC.atom_trace_detail @{context} prop; (*Type 'a*)
1.113 -val t = TermC.parse_test @{context} "(2*x)/1"; (*Type real*)
1.114 +val t = ParseC.parse_test @{context} "(2*x)/1"; (*Type real*)
1.115
1.116 val (thy, ro, er, inst) =
1.117 (@{theory "Isac_Knowledge"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]);
1.118 @@ -680,7 +680,7 @@
1.119 (* norm_equation is defined in Test.thy, other rls see Knowledg/**)
1.120 val thy = @{theory};
1.121 val rls = norm_equation;
1.122 -val term = TermC.parse_test @{context} "x + 1 = 2";
1.123 +val term = ParseC.parse_test @{context} "x + 1 = 2";
1.124
1.125 (**)val SOME (t, asm) = rewrite_set_ ctxt false rls term;
1.126 (** )##### try thm: "root_ge0"