1.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Sun Oct 09 06:53:03 2022 +0200
1.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Sun Oct 09 07:44:22 2022 +0200
1.3 @@ -119,13 +119,13 @@
1.4 val fod = Derive.do_one (Proof_Context.init_global @{theory "Isac_Knowledge"}) Atools_erls
1.5 ((#rules o Rule_Set.rep) Test_simplify)
1.6 (sqrt_right false (@{theory "Pure"})) NONE
1.7 - (TermC.str2term "x + 1 + - 1 * 2 = 0");
1.8 + (TermC.parse_test @{context} "x + 1 + - 1 * 2 = 0");
1.9 (writeln o Derive.trtas2str) fod;
1.10
1.11 val ifod = Derive.do_one (Proof_Context.init_global @{theory "Isac_Knowledge"}) Atools_erls
1.12 ((#rules o Rule_Set.rep) Test_simplify)
1.13 (sqrt_right false (@{theory "Pure"})) NONE
1.14 - (TermC.str2term "- 2 * 1 + (1 + x) = 0");
1.15 + (TermC.parse_test @{context} "- 2 * 1 + (1 + x) = 0");
1.16 (writeln o Derive.trtas2str) ifod;
1.17 fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1 = t2;
1.18 val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod);
1.19 @@ -637,7 +637,7 @@
1.20 "--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
1.21 "--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
1.22 "--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
1.23 -val t = TermC.str2term "Diff (x \<up> 2 + x + 1, x)";
1.24 +val t = TermC.parse_test @{context} "Diff (x \<up> 2 + x + 1, x)";
1.25 case t of Const (\<^const_name>\<open>Diff\<close>, _) $ _ => ()
1.26 | _ => raise
1.27 error "diff.sml behav.changed for CAS Diff (..., x)";
1.28 @@ -902,11 +902,11 @@
1.29 "--------- build fun check_for' ------------------------------";
1.30 "--------- build fun check_for' ------------------------------";
1.31 "--------- build fun check_for' ------------------------------";
1.32 -val subst = [(TermC.str2term "bdv", TermC.str2term "x")]: subst;
1.33 +val subst = [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "x")]: subst;
1.34 val rls = norm_Rational
1.35 val pat = TermC.parse_patt @{theory} "(?a + ?b)/(?b + ?c) = ?a / ?c";
1.36 -val (res, inf) = (TermC.str2term "(2 + 3)/(3 + 4)", TermC.str2term "2 / 4");
1.37 -val (res, inf) = (TermC.str2term "(2 + 3)/(3 + 4)", TermC.str2term "1 / 2");
1.38 +val (res, inf) = (TermC.parse_test @{context} "(2 + 3)/(3 + 4)", TermC.parse_test @{context} "2 / 4");
1.39 +val (res, inf) = (TermC.parse_test @{context} "(2 + 3)/(3 + 4)", TermC.parse_test @{context} "1 / 2");
1.40
1.41 val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern TermC.matches in res*)
1.42 rew_sub ctxt 1 [] Rewrite_Ord.function_empty Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
1.43 @@ -924,21 +924,21 @@
1.44 norm_res = norm_inf;
1.45
1.46 val pat = TermC.parse_patt @{theory} "(?a + ?b)/?a = ?b";
1.47 -val (res, inf) = (TermC.str2term "(2 + 3)/2", TermC.str2term "3");
1.48 +val (res, inf) = (TermC.parse_test @{context} "(2 + 3)/2", TermC.parse_test @{context} "3");
1.49 if check_for' ctxt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
1.50 then () else error "error patt example1 changed";
1.51
1.52 val pat = TermC.parse_patt @{theory} "(?a + ?b)/(?a + ?c) = ?b / ?c";
1.53 -val (res, inf) = (TermC.str2term "(2 + 3)/(2 + 4)", TermC.str2term "3 / 4");
1.54 +val (res, inf) = (TermC.parse_test @{context} "(2 + 3)/(2 + 4)", TermC.parse_test @{context} "3 / 4");
1.55 if check_for' ctxt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
1.56 then () else error "error patt example2 changed";
1.57
1.58 val pat = TermC.parse_patt @{theory} "(?a + ?b)/(?b + ?c) = ?a / ?c";
1.59 -val (res, inf) = (TermC.str2term "(2 + 3)/(3 + 4)", TermC.str2term "2 / 4");
1.60 +val (res, inf) = (TermC.parse_test @{context} "(2 + 3)/(3 + 4)", TermC.parse_test @{context} "2 / 4");
1.61 if check_for' ctxt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
1.62 then () else error "error patt example3 changed";
1.63
1.64 -val inf = TermC.str2term "1 / 2";
1.65 +val inf = TermC.parse_test @{context} "1 / 2";
1.66 if check_for' ctxt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
1.67 then () else error "error patt example3 changed";
1.68
1.69 @@ -946,15 +946,15 @@
1.70 "--------- build fun check_for' ?bdv -------------------------";
1.71 "--------- build fun check_for' ?bdv -------------------------";
1.72 val ctxt = Proof_Context.init_global @{theory}
1.73 -val subst = [(TermC.str2term "bdv", TermC.str2term "x")]: subst;
1.74 -val t = TermC.str2term "d_d x (x \<up> 2 + sin (x \<up> 4))";
1.75 +val subst = [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "x")]: subst;
1.76 +val t = TermC.parse_test @{context} "d_d x (x \<up> 2 + sin (x \<up> 4))";
1.77 val SOME (t, _) = rewrite_set_inst_ ctxt false subst norm_diff t;
1.78 if UnparseC.term t = "2 * x + cos (x \<up> 4) * 4 * x \<up> 3" then ()
1.79 else error "build fun check_for' ?bdv changed 1";
1.80
1.81 val rls = norm_diff
1.82 val pat = TermC.parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)";
1.83 -val (res, inf) = (TermC.str2term "2 * x + d_d x (sin (x \<up> 4))", TermC.str2term "2 * x + cos (4 * x \<up> 3)");
1.84 +val (res, inf) = (TermC.parse_test @{context} "2 * x + d_d x (sin (x \<up> 4))", TermC.parse_test @{context} "2 * x + cos (4 * x \<up> 3)");
1.85
1.86 val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern TermC.matches in res*)
1.87 rew_sub ctxt 1 subst Rewrite_Ord.function_empty Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
1.88 @@ -984,11 +984,11 @@
1.89 "--------- build fun check_for ------------------------";
1.90 "--------- build fun check_for ------------------------";
1.91 val (res, inf) =
1.92 - (TermC.str2term "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))",
1.93 - TermC.str2term "d_d x (x \<up> 2) + cos (4 * x \<up> 3)");
1.94 + (TermC.parse_test @{context} "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))",
1.95 + TermC.parse_test @{context} "d_d x (x \<up> 2) + cos (4 * x \<up> 3)");
1.96 val {errpats, nrls = rls, scr = Prog prog, ...} = MethodC.from_store ctxt ["diff", "differentiate_on_R"]
1.97
1.98 -val env = [(TermC.str2term "v_v", TermC.str2term "x")];
1.99 +val env = [(TermC.parse_test @{context} "v_v", TermC.parse_test @{context} "x")];
1.100 val errpats =
1.101 [Error_Pattern.empty, (*generalised for testing*)
1.102 ("chain-rule-diff-both",
1.103 @@ -1277,7 +1277,7 @@
1.104 "--------- fun concat_deriv --------------------------------------";
1.105 (*
1.106 val ({rew_ord, erls, rules,...}, fo, ifo) =
1.107 - (Rule_Set.rep Test_simplify, TermC.str2term "x+1+ - 1*2=0", TermC.str2term "-2*1+(x+1)=0");
1.108 + (Rule_Set.rep Test_simplify, TermC.parse_test @{context} "x+1+ - 1*2=0", TermC.parse_test @{context} "-2*1+(x+1)=0");
1.109 (tracing o Derive.trtas2str) fod';
1.110 > ["
1.111 (x + 1 + - 1 * 2 = 0, Thm ("radd_commute", "?m + ?n = ?n + ?m"), (- 1 * 2 + (x + 1) = 0, []))", "