1.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Mon Oct 31 18:28:36 2022 +0100
1.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Mon Nov 07 17:37:20 2022 +0100
1.3 @@ -47,9 +47,9 @@
1.4 "--------- appendFormula: on Res + equ_nrls ----------------------";
1.5 "--------- appendFormula: on Res + equ_nrls ----------------------";
1.6 "--------- appendFormula: on Res + equ_nrls ----------------------";
1.7 - val Prog sc = (#scr o MethodC.from_store ctxt) ["Test", "squ-equ-test-subpbl1"];
1.8 + val Prog sc = (#program o MethodC.from_store ctxt) ["Test", "squ-equ-test-subpbl1"];
1.9 (writeln o UnparseC.term) sc;
1.10 - val Prog sc = (#scr o MethodC.from_store ctxt) ["Test", "solve_linear"];
1.11 + val Prog sc = (#program o MethodC.from_store ctxt) ["Test", "solve_linear"];
1.12 (writeln o UnparseC.term) sc;
1.13
1.14 States.reset ();
1.15 @@ -993,7 +993,7 @@
1.16 val (res, inf) =
1.17 (TermC.parse_test @{context} "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))",
1.18 TermC.parse_test @{context} "d_d x (x \<up> 2) + cos (4 * x \<up> 3)");
1.19 -val {errpats, nrls = rls, scr = Prog prog, ...} = MethodC.from_store ctxt ["diff", "differentiate_on_R"]
1.20 +val {errpats, rew_rls = rls, program = Prog prog, ...} = MethodC.from_store ctxt ["diff", "differentiate_on_R"]
1.21
1.22 val env = [(TermC.parse_test @{context} "v_v", TermC.parse_test @{context} "x")];
1.23 val errpats =
1.24 @@ -1040,15 +1040,15 @@
1.25 (*if*) f_pred = f_in; (*else*)
1.26 val NONE = (*case*) CAS_Cmd.input f_in (*of*);
1.27 (*old* )val (_, _, metID) = get_obj g_spec pt (par_pblobj pt p)
1.28 - (*old*)val {scr = prog, ...} = MethodC.from_store ctxt metID
1.29 + (*old*)val {program = prog, ...} = MethodC.from_store ctxt metID
1.30 (*old*)val istate = get_istate_LI pt pos
1.31 (*old*)val ctxt = get_ctxt pt pos
1.32 ( *old*)
1.33 val LI.Not_Derivable =
1.34 (*case*) LI.locate_input_term (pt, pos) f_in (*of*);
1.35 val pp = Ctree.par_pblobj pt p
1.36 - val (errpats, nrls, prog) = case MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt pp) of
1.37 - {errpats, nrls, scr = Rule.Prog prog, ...} => (errpats, nrls, prog)
1.38 + val (errpats, rew_rls, prog) = case MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt pp) of
1.39 + {errpats, rew_rls, program = Rule.Prog prog, ...} => (errpats, rew_rls, prog)
1.40 | _ => error "inform: uncovered case of MethodC.from_store ctxt"
1.41 ;
1.42 (*+*)if Error_Pattern.s_to_string 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 \<up> ?n) = ?n * ?u \<up> (?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 \<up> ?n) = ?n * ?u \<up> (?n - 1) * d_d ?bdv ?u\", \"d_d ?bdv (LogExp.ln ?u) = d_d ?bdv ?u / ?u\", \"d_d ?bdv (exp ?u) = exp ?u * d_d ?x ?u\"]]"
1.43 @@ -1060,7 +1060,7 @@
1.44 (*+*) UnparseC.term f_in = "d_d x (x \<up> 2) + cos (4 * x \<up> 3)"
1.45 (*+*)then () else error "inform with (positive) Error_Pattern.check_for broken 2";
1.46
1.47 - val SOME "chain-rule-diff-both" = (*case*) Error_Pattern.check_for ctxt (f_pred, f_in) (prog, env) (errpats, nrls) (*of*);
1.48 + val SOME "chain-rule-diff-both" = (*case*) Error_Pattern.check_for ctxt (f_pred, f_in) (prog, env) (errpats, rew_rls) (*of*);
1.49
1.50 "--- final check:";
1.51 (*+*)val (_, _, ptp') = cs';
1.52 @@ -1093,7 +1093,7 @@
1.53 val f_curr = Ctree.get_curr_formula (pt, pos);
1.54 val pp = Ctree.par_pblobj pt p
1.55 val (errpats, prog) = case MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt pp) of
1.56 - {errpats, scr = Rule.Prog prog, ...} => (errpats, prog)
1.57 + {errpats, program = Rule.Prog prog, ...} => (errpats, prog)
1.58 | _ => error "find_fill_patterns: uncovered case of MethodC.from_store ctxt"
1.59 val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
1.60 val subst = Subst.for_bdv prog env
1.61 @@ -1167,7 +1167,7 @@
1.62 autoCalculate 1 (Steps 1);
1.63 autoCalculate 1 (Steps 1);(*([1], Res), d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))*)
1.64 appendFormula 1 "d_d x (x \<up> 2) + cos (4 * x \<up> 3)" (*|> Future.join*); (*<<<<<<<=========================*)
1.65 -(* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),
1.66 +(* the check for errpat is maximally liberal (whole term modulo "rew_rls" from "type met"),
1.67 would recognize "cos (4 * x \<up> (4 - 1)) + 2 * x" as well.
1.68 results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>
1.69 instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)
1.70 @@ -1253,37 +1253,37 @@
1.71 "--------- fun appl_adds -----------------------------------------";
1.72 "--------- fun appl_adds -----------------------------------------";
1.73 "--------- fun appl_adds -----------------------------------------";
1.74 -(* val (dI, oris, ppc, pbt, selct::ss) =
1.75 - (dI, pors, probl, ppc, map itms2fstr probl);
1.76 +(* val (dI, oris, model, pbt, selct::ss) =
1.77 + (dI, pors, probl, model, map itms2fstr probl);
1.78 ...vvv
1.79 *)
1.80 -(* val (dI, oris, ppc, pbt, (selct::ss))=
1.81 +(* val (dI, oris, model, pbt, (selct::ss))=
1.82 (#1 (References.select_input ospec spec), oris, []:I_Model.T,
1.83 - ((#ppc o Problem.from_store) (#2 (References.select_input ospec spec))),(imodel2fstr imodel));
1.84 - val iii = appl_adds dI oris ppc pbt (selct::ss);
1.85 + ((#model o Problem.from_store) (#2 (References.select_input ospec spec))),(imodel2fstr imodel));
1.86 + val iii = appl_adds dI oris model pbt (selct::ss);
1.87 tracing(I_Model.to_string thy iii);
1.88
1.89 - val itm = add_single' dI oris ppc pbt selct;
1.90 - val ppc = I_Model.add itm ppc;
1.91 + val itm = add_single' dI oris model pbt selct;
1.92 + val model = I_Model.add itm model;
1.93
1.94 val _::selct::ss = (selct::ss);
1.95 - val itm = add_single' dI oris ppc pbt selct;
1.96 - val ppc = I_Model.add itm ppc;
1.97 + val itm = add_single' dI oris model pbt selct;
1.98 + val model = I_Model.add itm model;
1.99
1.100 val _::selct::ss = (selct::ss);
1.101 - val itm = add_single' dI oris ppc pbt selct;
1.102 - val ppc = I_Model.add itm ppc;
1.103 - tracing(I_Model.to_string thy ppc);
1.104 + val itm = add_single' dI oris model pbt selct;
1.105 + val model = I_Model.add itm model;
1.106 + tracing(I_Model.to_string thy model);
1.107
1.108 val _::selct::ss = (selct::ss);
1.109 - val itm = add_single' dI oris ppc pbt selct;
1.110 - val ppc = I_Model.add itm ppc;
1.111 + val itm = add_single' dI oris model pbt selct;
1.112 + val model = I_Model.add itm model;
1.113 *)
1.114 "--------- fun concat_deriv --------------------------------------";
1.115 "--------- fun concat_deriv --------------------------------------";
1.116 "--------- fun concat_deriv --------------------------------------";
1.117 (*
1.118 - val ({rew_ord, erls, rules,...}, fo, ifo) =
1.119 + val ({rew_ord, asm_rls, rules,...}, fo, ifo) =
1.120 (Rule_Set.rep Test_simplify, TermC.parse_test @{context} "x+1+ - 1*2=0", TermC.parse_test @{context} "-2*1+(x+1)=0");
1.121 (tracing o Derive.trtas2str) fod';
1.122 > ["