1.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Mon Apr 19 11:45:43 2021 +0200
1.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Mon Apr 19 15:02:00 2021 +0200
1.3 @@ -119,13 +119,13 @@
1.4 val fod = Derive.do_one (@{theory "Isac_Knowledge"}) Atools_erls
1.5 ((#rules o Rule_Set.rep) Test_simplify)
1.6 (sqrt_right false (@{theory "Pure"})) NONE
1.7 - (str2term "x + 1 + -1 * 2 = 0");
1.8 + (TermC.str2term "x + 1 + -1 * 2 = 0");
1.9 (writeln o Derive.trtas2str) fod;
1.10
1.11 val ifod = Derive.do_one (@{theory "Isac_Knowledge"}) Atools_erls
1.12 ((#rules o Rule_Set.rep) Test_simplify)
1.13 (sqrt_right false (@{theory "Pure"})) NONE
1.14 - (str2term "-2 * 1 + (1 + x) = 0");
1.15 + (TermC.str2term "-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,11 +637,11 @@
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 = str2term "Diff (x^^^2 + x + 1, x)";
1.24 +val t = TermC.str2term "Diff (x^^^2 + x + 1, x)";
1.25 case t of Const ("Diff.Diff", _) $ _ => ()
1.26 | _ => raise
1.27 error "diff.sml behav.changed for CAS Diff (..., x)";
1.28 -atomty t;
1.29 +TermC.atomty t;
1.30 "-----------------------------------------------------------------";
1.31 (*1>*)reset_states ();
1.32 (*2>*)CalcTree [([], ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]))];
1.33 @@ -901,13 +901,13 @@
1.34 "--------- build fun check_for' ------------------------------";
1.35 "--------- build fun check_for' ------------------------------";
1.36 "--------- build fun check_for' ------------------------------";
1.37 -val subst = [(str2term "bdv", str2term "x")]: subst;
1.38 +val subst = [(TermC.str2term "bdv", TermC.str2term "x")]: subst;
1.39 val rls = norm_Rational
1.40 -val pat = parse_patt @{theory} "(?a + ?b)/(?b + ?c) = ?a / ?c";
1.41 -val (res, inf) = (str2term "(2 + 3)/(3 + 4)", str2term "2 / 4");
1.42 -val (res, inf) = (str2term "(2 + 3)/(3 + 4)", str2term "1 / 2");
1.43 +val pat = TermC.parse_patt @{theory} "(?a + ?b)/(?b + ?c) = ?a / ?c";
1.44 +val (res, inf) = (TermC.str2term "(2 + 3)/(3 + 4)", TermC.str2term "2 / 4");
1.45 +val (res, inf) = (TermC.str2term "(2 + 3)/(3 + 4)", TermC.str2term "1 / 2");
1.46
1.47 -val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern matches in res*)
1.48 +val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern TermC.matches in res*)
1.49 rew_sub thy 1 [] e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
1.50 if rewritten then NONE else SOME "e_errpatID";
1.51
1.52 @@ -922,39 +922,39 @@
1.53 res' = inf;
1.54 norm_res = norm_inf;
1.55
1.56 -val pat = parse_patt @{theory} "(?a + ?b)/?a = ?b";
1.57 -val (res, inf) = (str2term "(2 + 3)/2", str2term "3");
1.58 +val pat = TermC.parse_patt @{theory} "(?a + ?b)/?a = ?b";
1.59 +val (res, inf) = (TermC.str2term "(2 + 3)/2", TermC.str2term "3");
1.60 if check_for' (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
1.61 then () else error "error patt example1 changed";
1.62
1.63 -val pat = parse_patt @{theory} "(?a + ?b)/(?a + ?c) = ?b / ?c";
1.64 -val (res, inf) = (str2term "(2 + 3)/(2 + 4)", str2term "3 / 4");
1.65 +val pat = TermC.parse_patt @{theory} "(?a + ?b)/(?a + ?c) = ?b / ?c";
1.66 +val (res, inf) = (TermC.str2term "(2 + 3)/(2 + 4)", TermC.str2term "3 / 4");
1.67 if check_for' (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
1.68 then () else error "error patt example2 changed";
1.69
1.70 -val pat = parse_patt @{theory} "(?a + ?b)/(?b + ?c) = ?a / ?c";
1.71 -val (res, inf) = (str2term "(2 + 3)/(3 + 4)", str2term "2 / 4");
1.72 +val pat = TermC.parse_patt @{theory} "(?a + ?b)/(?b + ?c) = ?a / ?c";
1.73 +val (res, inf) = (TermC.str2term "(2 + 3)/(3 + 4)", TermC.str2term "2 / 4");
1.74 if check_for' (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
1.75 then () else error "error patt example3 changed";
1.76
1.77 -val inf = str2term "1 / 2";
1.78 +val inf = TermC.str2term "1 / 2";
1.79 if check_for' (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
1.80 then () else error "error patt example3 changed";
1.81
1.82 "--------- build fun check_for' ?bdv -------------------------";
1.83 "--------- build fun check_for' ?bdv -------------------------";
1.84 "--------- build fun check_for' ?bdv -------------------------";
1.85 -val subst = [(str2term "bdv", str2term "x")]: subst;
1.86 -val t = str2term "d_d x (x ^^^ 2 + sin (x ^^^ 4))";
1.87 +val subst = [(TermC.str2term "bdv", TermC.str2term "x")]: subst;
1.88 +val t = TermC.str2term "d_d x (x ^^^ 2 + sin (x ^^^ 4))";
1.89 val SOME (t, _) = rewrite_set_inst_ thy false subst norm_diff t;
1.90 if UnparseC.term t = "2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3" then ()
1.91 else error "build fun check_for' ?bdv changed 1";
1.92
1.93 val rls = norm_diff
1.94 -val pat = parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)";
1.95 -val (res, inf) = (str2term "2 * x + d_d x (sin (x ^^^ 4))", str2term "2 * x + cos (4 * x ^^^ 3)");
1.96 +val pat = TermC.parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)";
1.97 +val (res, inf) = (TermC.str2term "2 * x + d_d x (sin (x ^^^ 4))", TermC.str2term "2 * x + cos (4 * x ^^^ 3)");
1.98
1.99 -val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern matches in res*)
1.100 +val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern TermC.matches in res*)
1.101 rew_sub thy 1 subst e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
1.102 if UnparseC.term res' = "2 * x + cos (d_d x (x ^^^ 4))" andalso rewritten then ()
1.103 else error "build fun check_for' ?bdv changed 2";
1.104 @@ -982,19 +982,19 @@
1.105 "--------- build fun check_for ------------------------";
1.106 "--------- build fun check_for ------------------------";
1.107 val (res, inf) =
1.108 - (str2term "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))",
1.109 - str2term "d_d x (x ^^^ 2) + cos (4 * x ^^^ 3)");
1.110 + (TermC.str2term "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))",
1.111 + TermC.str2term "d_d x (x ^^^ 2) + cos (4 * x ^^^ 3)");
1.112 val {errpats, nrls = rls, scr = Prog prog, ...} = MethodC.from_store ["diff", "differentiate_on_R"]
1.113
1.114 -val env = [(str2term "v_v", str2term "x")];
1.115 +val env = [(TermC.str2term "v_v", TermC.str2term "x")];
1.116 val errpats =
1.117 [Error_Pattern.empty, (*generalised for testing*)
1.118 ("chain-rule-diff-both",
1.119 - [parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)",
1.120 - parse_patt @{theory} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)",
1.121 - parse_patt @{theory} "d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1)",
1.122 - parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u",
1.123 - parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"],
1.124 + [TermC.parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)",
1.125 + TermC.parse_patt @{theory} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)",
1.126 + TermC.parse_patt @{theory} "d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1)",
1.127 + TermC.parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u",
1.128 + TermC.parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"],
1.129 [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain},
1.130 @{thm diff_ln_chain}, @{thm diff_exp_chain}])];
1.131 case Error_Pattern.check_for (res, inf) (prog, env) (errpats, rls) of SOME _ => ()
1.132 @@ -1276,7 +1276,7 @@
1.133 "--------- fun concat_deriv --------------------------------------";
1.134 (*
1.135 val ({rew_ord, erls, rules,...}, fo, ifo) =
1.136 - (Rule_Set.rep Test_simplify, str2term "x+1+ -1*2=0", str2term "-2*1+(x+1)=0");
1.137 + (Rule_Set.rep Test_simplify, TermC.str2term "x+1+ -1*2=0", TermC.str2term "-2*1+(x+1)=0");
1.138 (tracing o Derive.trtas2str) fod';
1.139 > ["
1.140 (x + 1 + -1 * 2 = 0, Thm ("radd_commute", "?m + ?n = ?n + ?m"), (-1 * 2 + (x + 1) = 0, []))", "