1.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Fri Oct 07 20:46:48 2022 +0200
1.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Sat Oct 08 11:40:48 2022 +0200
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_PIDE ctxt) ["Test", "squ-equ-test-subpbl1"];
1.8 + val Prog sc = (#scr 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_PIDE ctxt) ["Test", "solve_linear"];
1.11 + val Prog sc = (#scr o MethodC.from_store ctxt) ["Test", "solve_linear"];
1.12 (writeln o UnparseC.term) sc;
1.13
1.14 States.reset ();
1.15 @@ -986,7 +986,7 @@
1.16 val (res, inf) =
1.17 (TermC.str2term "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))",
1.18 TermC.str2term "d_d x (x \<up> 2) + cos (4 * x \<up> 3)");
1.19 -val {errpats, nrls = rls, scr = Prog prog, ...} = MethodC.from_store_PIDE ctxt ["diff", "differentiate_on_R"]
1.20 +val {errpats, nrls = rls, scr = Prog prog, ...} = MethodC.from_store ctxt ["diff", "differentiate_on_R"]
1.21
1.22 val env = [(TermC.str2term "v_v", TermC.str2term "x")];
1.23 val errpats =
1.24 @@ -1033,16 +1033,16 @@
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_PIDE ctxt metID
1.29 + (*old*)val {scr = 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_PIDE ctxt (Ctree.get_obj Ctree.g_metID pt pp) of
1.37 + val (errpats, nrls, prog) = case MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt pp) of
1.38 {errpats, nrls, scr = Rule.Prog prog, ...} => (errpats, nrls, prog)
1.39 - | _ => error "inform: uncovered case of MethodC.from_store_PIDE ctxt"
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 (*+*)then () else error "inform with (positive) Error_Pattern.check_for broken 3";
1.44 @@ -1085,9 +1085,9 @@
1.45 "~~~~~ fun find_fill_patterns , args:"; val ((pt, pos as (p, _)), errpatID) = ((pt, pos), errpatID);
1.46 val f_curr = Ctree.get_curr_formula (pt, pos);
1.47 val pp = Ctree.par_pblobj pt p
1.48 - val (errpats, prog) = case MethodC.from_store_PIDE ctxt (Ctree.get_obj Ctree.g_metID pt pp) of
1.49 + val (errpats, prog) = case MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt pp) of
1.50 {errpats, scr = Rule.Prog prog, ...} => (errpats, prog)
1.51 - | _ => error "find_fill_patterns: uncovered case of MethodC.from_store_PIDE ctxt"
1.52 + | _ => error "find_fill_patterns: uncovered case of MethodC.from_store ctxt"
1.53 val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
1.54 val subst = Subst.for_bdv prog env
1.55 val errpatthms = errpats