1.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Tue Mar 31 14:05:10 2020 +0200
1.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Tue Mar 31 15:43:33 2020 +0200
1.3 @@ -29,8 +29,8 @@
1.4 "--------- init_form, start with <NEW> (CAS input) ---------------";
1.5 "--------- build fun check_err_patt ------------------------------";
1.6 "--------- build fun check_err_patt ?bdv -------------------------";
1.7 -"--------- build fun check_error_patterns ------------------------";
1.8 -"--------- embed fun check_error_patterns ------------------------";
1.9 +"--------- build fun Error_Pattern.check_for ------------------------";
1.10 +"--------- embed fun Error_Pattern.check_for ------------------------";
1.11 "--------- build fun get_fillpats --------------------------------";
1.12 "--------- embed fun find_fillpatterns ---------------------------";
1.13 "--------- build fun is_exactly_equal, inputFillFormula ----------";
1.14 @@ -648,7 +648,7 @@
1.15 spec;
1.16 writeln (itms2str_ ctxt probl);
1.17 writeln (itms2str_ ctxt meth);
1.18 -writeln (istate2str (fst istate));
1.19 +writeln (Istate.string_of (fst istate));
1.20
1.21 refFormula 1 ([],Pbl) (*--> correct CalcHead*);
1.22 (*081016 NOT necessary (but leave it in Java):*)
1.23 @@ -661,7 +661,7 @@
1.24 val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];
1.25 val NONE = env;
1.26 val (SOME istate, NONE) = loc;
1.27 -(*default_print_depth 5;*) writeln (istate2str (fst istate)); (*default_print_depth 3;*)
1.28 +(*default_print_depth 5;*) writeln (Istate.string_of (fst istate)); (*default_print_depth 3;*)
1.29 (*Pstate ([],
1.30 [], NONE,
1.31 ??.empty, Sundef, false)*)
1.32 @@ -705,7 +705,7 @@
1.33 val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];
1.34 val NONE = env;
1.35 val (SOME istate, NONE) = loc;
1.36 -(*default_print_depth 5;*) writeln (istate2str (fst istate)); (*default_print_depth 3;*)
1.37 +(*default_print_depth 5;*) writeln (Istate.string_of (fst istate)); (*default_print_depth 3;*)
1.38 (*Pstate ([],
1.39 [], NONE,
1.40 ??.empty, Sundef, false)*)
1.41 @@ -971,9 +971,9 @@
1.42 if check_err_patt (res, inf) (subst: subst) ("errpatID": errpatID, pat) rls = SOME "errpatID"
1.43 then () else error "error patt example1 changed";
1.44
1.45 -"--------- build fun check_error_patterns ------------------------";
1.46 -"--------- build fun check_error_patterns ------------------------";
1.47 -"--------- build fun check_error_patterns ------------------------";
1.48 +"--------- build fun Error_Pattern.check_for ------------------------";
1.49 +"--------- build fun Error_Pattern.check_for ------------------------";
1.50 +"--------- build fun Error_Pattern.check_for ------------------------";
1.51 val (res, inf) =
1.52 (str2term "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))",
1.53 str2term "d_d x (x ^^^ 2) + cos (4 * x ^^^ 3)");
1.54 @@ -990,13 +990,13 @@
1.55 parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"],
1.56 [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain},
1.57 @{thm diff_ln_chain}, @{thm diff_exp_chain}])]: errpat list;
1.58 -case check_error_patterns (res, inf) (prog, env) (errpats, rls) of SOME _ => ()
1.59 -| NONE => error "check_error_patterns broken";
1.60 +case Error_Pattern.check_for (res, inf) (prog, env) (errpats, rls) of SOME _ => ()
1.61 +| NONE => error "Error_Pattern.check_for broken";
1.62 DEconstrCalcTree 1;
1.63
1.64 -"--------- embed fun check_error_patterns ------------------------";
1.65 -"--------- embed fun check_error_patterns ------------------------";
1.66 -"--------- embed fun check_error_patterns ------------------------";
1.67 +"--------- embed fun Error_Pattern.check_for ------------------------";
1.68 +"--------- embed fun Error_Pattern.check_for ------------------------";
1.69 +"--------- embed fun Error_Pattern.check_for ------------------------";
1.70 reset_states ();
1.71 CalcTree
1.72 [(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
1.73 @@ -1012,7 +1012,7 @@
1.74 "~~~~~ fun appendFormula' , args:"; val (cI, (ifo: Rule.cterm')) = (cI, ifo);
1.75 val cs = get_calc cI
1.76 val pos = get_pos cI 1;
1.77 -(*+*)if pos = ([1], Res) then () else error "inform with (positive) check_error_patterns broken 1";
1.78 +(*+*)if pos = ([1], Res) then () else error "inform with (positive) Error_Pattern.check_for broken 1";
1.79 val ("ok", cs' as (_, _, ptp)) = (*case*) Step.do_next pos cs (*of*);
1.80 (*case*) Step_Solve.by_term ptp (encode ifo) (*of*); (*ERROR WAS: "no derivation found"*)
1.81 "~~~~~ fun Step_Solve.by_term , args:"; val (((*next_*)cs as (_, _, (pt, pos as (p, _))): Chead.calcstate'), istr)
1.82 @@ -1037,21 +1037,21 @@
1.83 | _ => error "inform: uncovered case of get_met"
1.84 ;
1.85 (*+*)if errpats2str errpats = "[(\"chain-rule-diff-both\",\n[\"d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)\",\"d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)\",\"d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1)\",\"d_d ?bdv (LogExp.ln ?u) = 1 / ?u\",\"d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u\"],\n[\"d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u\",\"d_d ?bdv (cos ?u) = - sin ?u * d_d ?bdv ?u\",\"d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1) * d_d ?bdv ?u\",\"d_d ?bdv (LogExp.ln ?u) = d_d ?bdv ?u / ?u\",\"d_d ?bdv (E_ ^^^ ?u) = E_ ^^^ ?u * d_d ?x ?u\"]]"
1.86 -(*+*)then () else error "inform with (positive) check_error_patterns broken 3";
1.87 +(*+*)then () else error "inform with (positive) Error_Pattern.check_for broken 3";
1.88
1.89 val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
1.90 ;
1.91 (*+*)if term2str f_pred = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
1.92 (*+*) term2str f_in = "d_d x (x ^^^ 2) + cos (4 * x ^^^ 3)"
1.93 -(*+*)then () else error "inform with (positive) check_error_patterns broken 2";
1.94 +(*+*)then () else error "inform with (positive) Error_Pattern.check_for broken 2";
1.95
1.96 - val SOME "chain-rule-diff-both" = (*case*) Error_Pattern.check_error_patterns (f_pred, f_in) (prog, env) (errpats, nrls) (*of*);
1.97 + val SOME "chain-rule-diff-both" = (*case*) Error_Pattern.Error_Pattern.check_for (f_pred, f_in) (prog, env) (errpats, nrls) (*of*);
1.98
1.99 "--- final check:";
1.100 (*+*)val (_, _, ptp') = cs';
1.101 case Step_Solve.by_term ptp' (encode ifo) of
1.102 ("error pattern #chain-rule-diff-both#", calcstate') => ()
1.103 -| _ => error "inform with (positive) check_error_patterns broken"
1.104 +| _ => error "inform with (positive) Error_Pattern.check_for broken"
1.105
1.106
1.107 "--------- embed fun find_fillpatterns ---------------------------";