1.1 --- a/TODO.md	Sat Aug 06 15:57:46 2022 +0200
     1.2 +++ b/TODO.md	Sat Aug 06 17:36:59 2022 +0200
     1.3 @@ -55,7 +55,7 @@
     1.4  ***** priority of WN items is top down, most urgent/simple on top
     1.5  
     1.6  * WN: rewriting with ctxt not complete (cause errors hard to indentify later)
     1.7 -    - Error_Pattern.check_for', fill_form
     1.8 +    - Error_Pattern.fill_form
     1.9      - Derive.steps
    1.10      - Fetch_Tacs.specific_from_prog ?
    1.11      - Eval.adhoc_thm, adhoc_thm1_

     2.1 --- a/src/Tools/isac/Interpret/error-pattern.sml	Sat Aug 06 15:57:46 2022 +0200
     2.2 +++ b/src/Tools/isac/Interpret/error-pattern.sml	Sat Aug 06 17:36:59 2022 +0200
     2.3 @@ -22,12 +22,12 @@
     2.4  
     2.5    val from_store: Tactic.input -> Error_Pattern_Def.id list
     2.6    val filled_exactly: Calc.T -> string -> string * Tactic.input
     2.7 -  val check_for: term * term -> term * Env.T -> T list * Rule_Set.T -> id option
     2.8 +  val check_for: Proof.context -> term * term -> term * Env.T -> T list * Rule_Set.T -> id option
     2.9  
    2.10    val find_fill_patterns: Calc.T -> id -> record list
    2.11  
    2.12  \<^isac_test>\<open>
    2.13 -  val check_for': term * term -> subst -> id * term -> Rule_Set.T -> id option
    2.14 +  val check_for': Proof.context -> term * term -> subst -> id * term -> Rule_Set.T -> id option
    2.15    val fill_from_store: Subst.input option * Subst.T -> term -> id -> thm ->
    2.16      record list
    2.17    val fill_form: Subst.input option * Subst.T -> thm * term -> id -> fill_in ->
    2.18 @@ -54,9 +54,8 @@
    2.19  (*
    2.20    check if (agreed result, input formula) matches the error pattern "pat" modulo simplifier rls
    2.21  *)
    2.22 -fun check_for' (res, inf) subst (id, pat) rls =
    2.23 +fun check_for' ctxt (res, inf) subst (id, pat) rls =
    2.24    let
    2.25 -    val ctxt = Proof_Context.init_global ((ThyC.Isac()))
    2.26      val (res', _, _, rewritten) =
    2.27        Rewrite.rew_sub ctxt 1 subst Rewrite_Ord.function_empty
    2.28          Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
    2.29 @@ -79,12 +78,12 @@
    2.30    check if (agreed result, input formula) matches SOME error pattern modulo simplifier rls;
    2.31    (prog, env) for retrieval of casual substitution for bdv in the pattern.
    2.32  *)
    2.33 -fun check_for (res, inf) (prog, env) (errpats, rls) =
    2.34 +fun check_for ctxt (res, inf) (prog, env) (errpats, rls) =
    2.35    let
    2.36      val (_, subst) = Subst.for_bdv prog env
    2.37      fun scan (_, [], _) = NONE
    2.38        | scan (id, T :: errpats, _) =
    2.39 -          case check_for' (res, inf) subst (id, T) rls of
    2.40 +          case check_for' ctxt (res, inf) subst (id, T) rls of
    2.41              NONE => scan (id, errpats, [])
    2.42            | SOME id => SOME id
    2.43      fun scans [] = NONE

     3.1 --- a/src/Tools/isac/Interpret/step-solve.sml	Sat Aug 06 15:57:46 2022 +0200
     3.2 +++ b/src/Tools/isac/Interpret/step-solve.sml	Sat Aug 06 17:36:59 2022 +0200
     3.3 @@ -113,7 +113,7 @@
     3.4            		  | _ => raise ERROR "inform: uncovered case of get_met"
     3.5            	  val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
     3.6            	in
     3.7 -          	  case Error_Pattern.check_for (f_pred, f_in) (prog, env) (errpats, nrls) of
     3.8 +          	  case Error_Pattern.check_for (Ctree.get_ctxt pt pos) (f_pred, f_in) (prog, env) (errpats, nrls) of
     3.9            	    SOME errpatID => ("error pattern #" ^ errpatID ^ "#", Calc.state_empty_post)
    3.10            	  | NONE => ("no derivation found", Calc.state_empty_post)
    3.11              end

     4.1 --- a/test/Tools/isac/Interpret/error-pattern.sml	Sat Aug 06 15:57:46 2022 +0200
     4.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml	Sat Aug 06 17:36:59 2022 +0200
     4.3 @@ -284,7 +284,7 @@
     4.4  2.5.   1 + (x + -2 * 1) = 0\n
     4.5  2.6.   1 + x + -2 * 1 = 0\n";
     4.6  *)
     4.7 -if str = 
     4.8 +if str =
     4.9  ".    ----- pblobj -----\n"^
    4.10  "1.   x + 1 = 2\n"^
    4.11  "2.   x + 1 + - 1 * 2 = 0\n"^
    4.12 @@ -925,21 +925,21 @@
    4.13  
    4.14  val pat = TermC.parse_patt @{theory} "(?a + ?b)/?a = ?b";
    4.15  val (res, inf) = (TermC.str2term "(2 + 3)/2", TermC.str2term "3");
    4.16 -if check_for' (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
    4.17 +if check_for' ctxt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
    4.18  then () else error "error patt example1 changed";
    4.19  
    4.20  val pat = TermC.parse_patt @{theory} "(?a + ?b)/(?a + ?c) = ?b / ?c";
    4.21  val (res, inf) = (TermC.str2term "(2 + 3)/(2 + 4)", TermC.str2term "3 / 4");
    4.22 -if check_for' (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
    4.23 +if check_for' ctxt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
    4.24  then () else error "error patt example2 changed";
    4.25  
    4.26  val pat = TermC.parse_patt @{theory} "(?a + ?b)/(?b + ?c) = ?a / ?c";
    4.27  val (res, inf) = (TermC.str2term "(2 + 3)/(3 + 4)", TermC.str2term "2 / 4");
    4.28 -if check_for' (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
    4.29 +if check_for' ctxt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
    4.30  then () else error "error patt example3 changed";
    4.31  
    4.32  val inf =  TermC.str2term "1 / 2";
    4.33 -if check_for' (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
    4.34 +if check_for' ctxt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
    4.35  then () else error "error patt example3 changed";
    4.36  
    4.37  "--------- build fun check_for' ?bdv -------------------------";
    4.38 @@ -977,7 +977,7 @@
    4.39  if norm_res = norm_inf then ()
    4.40  else error "build fun check_for' ?bdv changed 5";
    4.41  
    4.42 -if Error_Pattern.check_for' (res, inf) (subst: subst) ("errpatID": Error_Pattern.id, pat) rls = SOME "errpatID"
    4.43 +if Error_Pattern.check_for' ctxt (res, inf) (subst: subst) ("errpatID": Error_Pattern.id, pat) rls = SOME "errpatID"
    4.44  then () else error "error patt example1 changed";
    4.45  
    4.46  "--------- build fun check_for ------------------------";
    4.47 @@ -999,7 +999,7 @@
    4.48        TermC.parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"],
    4.49       [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain}, 
    4.50        @{thm diff_ln_chain}, @{thm  diff_exp_chain}])];
    4.51 -case Error_Pattern.check_for (res, inf) (prog, env) (errpats, rls) of SOME _ => () 
    4.52 +case Error_Pattern.check_for ctxt (res, inf) (prog, env) (errpats, rls) of SOME _ => () 
    4.53  | NONE => error "Error_Pattern.check_for broken";
    4.54  DEconstrCalcTree 1;
    4.55  
    4.56 @@ -1053,7 +1053,7 @@
    4.57  (*+*)   UnparseC.term f_in = "d_d x (x \<up> 2) + cos (4 * x \<up> 3)"
    4.58  (*+*)then () else error "inform with (positive) Error_Pattern.check_for broken 2";
    4.59  
    4.60 -             val SOME "chain-rule-diff-both" = (*case*) Error_Pattern.check_for (f_pred, f_in) (prog, env) (errpats, nrls) (*of*);
    4.61 +             val SOME "chain-rule-diff-both" = (*case*) Error_Pattern.check_for ctxt (f_pred, f_in) (prog, env) (errpats, nrls) (*of*);
    4.62  
    4.63  "--- final check:";
    4.64  (*+*)val (_, _, ptp') = cs';