1.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Thu Dec 22 17:06:19 2022 +0100
1.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Fri Jan 06 08:04:36 2023 +0100
1.3 @@ -1046,12 +1046,12 @@
1.4 ( *old*)
1.5 val LI.Not_Derivable =
1.6 (*case*) LI.locate_input_term (pt, pos) f_in (*of*);
1.7 - val pp = Ctree.par_pblobj pt p
1.8 - val (errpats, rew_rls, prog) = case MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt pp) of
1.9 + val met_id = Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p)
1.10 + val (errpats, rew_rls, prog) = case MethodC.from_store' (Know_Store.get_via_last_thy "Build_Thydata") met_id of
1.11 {errpats, rew_rls, program = Rule.Prog prog, ...} => (errpats, rew_rls, prog)
1.12 | _ => error "inform: uncovered case of MethodC.from_store ctxt"
1.13 ;
1.14 -(*+*)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.15 +(*+*)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)\"],\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\"]]"
1.16 (*+*)then () else error "inform with (positive) Error_Pattern.check_for broken 3";
1.17
1.18 val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
1.19 @@ -1069,6 +1069,115 @@
1.20 | _ => error "inform with (positive) Error_Pattern.check_for broken"
1.21
1.22
1.23 +"----------- re-build: fill_from_store without thy-hierarchy -----------------------------------";
1.24 +"----------- re-build: fill_from_store without thy-hierarchy -----------------------------------";
1.25 +"----------- re-build: fill_from_store without thy-hierarchy -----------------------------------";
1.26 +open Error_Pattern
1.27 +val c = []: int list
1.28 +val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context}
1.29 +[(["functionTerm (x \<up> 2 + sin (x \<up> 4))", "differentiateFor x", "derivative f_f'"],
1.30 + ("Isac_Knowledge", ["derivative_of", "function"], ["diff", "differentiate_on_R"]))];
1.31 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.32 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.33 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.34 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.35 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.36 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.37 +val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Apply_Method ["diff", "differentiate_on_R"]*)
1.38 +val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Rewrite_Inst (["(''bdv'', x)"], ("diff_sum", "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v"))*)
1.39 + val ([1], Frm) = p;
1.40 + val "d_d x (x \<up> 2 + sin (x \<up> 4))" = f2str f;
1.41 +val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Rewrite_Inst (["(''bdv'', x)"], ("diff_sin_chain", "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u"))*)
1.42 + val ([1], Res) = p;
1.43 + val "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" = f2str f
1.44 +
1.45 +val return_of_me = me nxt p c pt; (*nxt = Rewrite_Inst (["(''bdv'', x)"], ("diff_pow", "d_d ?bdv (?bdv \<up> ?n) = ?n * ?bdv \<up> (?n - 1)"))*)
1.46 + val ([1], Res) = p
1.47 + val "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" = f2str f;
1.48 + (* "d_d x (x \<up> 2) + cos (x \<up> 4)" .. wrong user input within next step *)
1.49 +(*//------------------ step into find_fill_patterns ----------------------------------------\\*)
1.50 +(* INSTEAD OF STEPPING INTO me WE DO SO FOR Kernel.findFillpatterns cI errpatID =
1.51 + let
1.52 + val ((pt, _), _) = States.get_calc cI
1.53 + val pos = States.get_pos cI 1;
1.54 + val fillpats = Error_Pattern.find_fill_patterns (pt, pos) errpatID
1.55 +*)
1.56 +"~~~~~ fun findFillpatterns , args:"; val (pt, p, errpatID) = (pt, p, "chain-rule-diff-both");
1.57 +"~~~~~ fun find_fill_patterns , args:"; val ((pt, pos as (p, _)), id) = ((pt, p), errpatID);
1.58 +(*old-------\* )
1.59 + val f_curr = Ctree.get_curr_formula (pt, pos);
1.60 + val pp = Ctree.par_pblobj pt p
1.61 + val (errpats, prog) = case MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt pp) of
1.62 + {errpats, program = Rule.Prog prog, ...} => (errpats, prog)
1.63 + | _ => error "find_fill_patterns: uncovered case of MethodC.from_store ctxt"
1.64 +( *new-------\*)
1.65 + val ctxt = Ctree.get_ctxt pt pos
1.66 + val f_curr = Ctree.get_curr_formula (pt, pos)
1.67 + val met_id = Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p)
1.68 + val (errpats, prog) = case MethodC.from_store' (Know_Store.get_via_last_thy "Build_Thydata") met_id of
1.69 + {errpats, program = Rule.Prog prog, ...} => (errpats, prog)
1.70 + | _ => error "find_fill_patterns: uncovered case of MethodC.from_store ctxt"
1.71 +(*new-------/*)
1.72 +
1.73 +(*+*)val 1 = length errpats(*ONLY WITH from_store' @{theory (*!!!*)Build_Thydata}*)
1.74 + val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
1.75 + val subst = Subst.for_bdv ctxt prog env
1.76 + val errpatthms = errpats
1.77 + |> filter ((curry op = errpatID) o (#1: Error_Pattern.T -> Error_Pattern.id))
1.78 + |> map (#3: Error_Pattern.T -> thm list)
1.79 + |> flat;
1.80 +
1.81 +(*+*)val 3 = length errpatthms;
1.82 +(*+*)val 5 = length (get_fill_ins @{theory} "diff_sin_chain");
1.83 +
1.84 +(*case*) map (
1.85 + fill_from_store ctxt subst f_curr errpatID) errpatthms |> flat (*of*);
1.86 +"~~~~~ fun fill_from_store , args:"; val (ctxt, subst, form, (*id*)errpat_id, thm) =
1.87 + (ctxt, subst, f_curr, errpatID, hd errpatthms);
1.88 + val thm_id_long = Thm.get_name_hint thm
1.89 +
1.90 +(*+*)val "Diff.diff_sin_chain" = thm_id_long;
1.91 +(*+*)val "diff_sin_chain" = ThmC.cut_id thm_id_long;
1.92 +
1.93 + val thm_id = ThmC.cut_id thm_id_long
1.94 + val fill_ins =
1.95 +
1.96 +Error_Pattern.get_fill_ins (Proof_Context.theory_of ctxt) thm_id;
1.97 +"~~~~~ fun get_fill_ins , args:"; val (thy, thm_id) =
1.98 + ((Proof_Context.theory_of ctxt), thm_id);
1.99 + (*case*) AList.lookup (op =) (get_fill_inss thy) thm_id (*of*);
1.100 +val ERROR "fill_ins for thm \"diff_sin_chain\" missing in theory \"Isac_Knowledge\" (and ancestors)\nTODO exception hierarchy needs to be established." =
1.101 + ERROR ("fill_ins for thm \"" ^ thm_id ^ "\" missing in theory \"" ^
1.102 + (thy |> ThyC.id_of) ^ "\" (and ancestors)" ^
1.103 + "\nTODO exception hierarchy needs to be established.");
1.104 +
1.105 +(*return to fill_from_store..*)
1.106 + val some = map (fill_form ctxt subst (thm, form) errpat_id) fill_ins;
1.107 +val return_fill_from_store = some |> filter is_some |> map the;
1.108 +
1.109 +(* final test ... ----------------------------------------------------------------------------*)
1.110 +(*+*)if length return_fill_from_store = 5 then
1.111 +(*+*) case return_fill_from_store of
1.112 +(*+*) ("fill-d_d-arg", tm, thm, subsopt) :: _ => if UnparseC.term tm =
1.113 +(*+*) "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4)) =\nd_d x (x \<up> 2) + cos (x \<up> 4) * d_d x ?_dummy_1"
1.114 +(*+*) then () else error "find_fill_patterns changed 2a"
1.115 +(*+*) | _ => error "find_fill_patterns changed 2b"
1.116 +(*+*)else error "find_fill_patterns changed 2c";
1.117 +(*-------------------- stop step into find_fill_patterns -------------------------------------*)
1.118 +(*\\------------------ step into find_fill_patterns ----------------------------------------//*)
1.119 +
1.120 +val (p,_,f,nxt,_,pt) = return_of_me
1.121 +val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Rewrite_Inst (["(''bdv'', x)"], ("diff_pow", "d_d ?bdv (?bdv \<up> ?n) = ?n * ?bdv \<up> (?n - 1)"))*)
1.122 + val ([3], Res) = p
1.123 + val "d_d x (x \<up> 2) + cos (x \<up> 4) * (4 * x \<up> (4 - 1))" = f2str f;
1.124 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.125 +val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Check_Postcond ["derivative_of", "function"]*)
1.126 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.127 + val ([], Res) = p;
1.128 + val "2 * x + cos (x \<up> 4) * 4 * x \<up> 3" = f2str f
1.129 + val End_Proof' = nxt;
1.130 +
1.131 +
1.132 "--------- embed fun find_fill_patterns ---------------------------";
1.133 "--------- embed fun find_fill_patterns ---------------------------";
1.134 "--------- embed fun find_fill_patterns ---------------------------";
1.135 @@ -1081,78 +1190,27 @@
1.136 autoCalculate 1 CompleteCalcHead;
1.137 autoCalculate 1 (Steps 1);
1.138 autoCalculate 1 (Steps 1);(*([1], Res), d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))*)
1.139 -appendFormula 1 "d_d x (x \<up> 2) + cos (4 * x \<up> 3)" (*|> Future.join*);
1.140 +appendFormula 1 "d_d x (x \<up> 2) + cos (4 * x \<up> 3)";
1.141 (*<CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>*)
1.142 (*or
1.143 <CALCMESSAGE> no derivation found </CALCMESSAGE>*)
1.144 -
1.145 "~~~~~ fun findFillpatterns, args:"; val (cI, errpatID) = (1, "chain-rule-diff-both");
1.146 val ((pt, _), _) = States.get_calc cI
1.147 val pos = States.get_pos cI 1;
1.148 -"~~~~~ fun find_fill_patterns , args:"; val ((pt, pos as (p, _)), errpatID) = ((pt, pos), errpatID);
1.149 - val f_curr = Ctree.get_curr_formula (pt, pos);
1.150 - val pp = Ctree.par_pblobj pt p
1.151 - val (errpats, prog) = case MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt pp) of
1.152 - {errpats, program = Rule.Prog prog, ...} => (errpats, prog)
1.153 - | _ => error "find_fill_patterns: uncovered case of MethodC.from_store ctxt"
1.154 - val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
1.155 - val subst = Subst.for_bdv ctxt prog env
1.156 - val errpatthms = errpats
1.157 - |> filter ((curry op = errpatID) o (#1: Error_Pattern.T -> Error_Pattern.id))
1.158 - |> map (#3: Error_Pattern.T -> thm list)
1.159 - |> flat;
1.160
1.161 -case map (Error_Pattern.fill_from_store ctxt subst f_curr errpatID) errpatthms |> flat of
1.162 - ("fill-d_d-arg", tm, thm, subs_opt) :: _ => if UnparseC.term tm =
1.163 - "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4)) =\nd_d x (x \<up> 2) + cos (x \<up> 4) * d_d x ?_dummy_1"
1.164 - then () else error "find_fill_patterns changed 1a"
1.165 -| _ => error "find_fill_patterns changed 1b"
1.166 +val return_from_find_fill_patterns = find_fill_patterns (pt, pos) errpatID;
1.167 +DEconstrCalcTree 1;
1.168
1.169 -"~~~~~ fun fill_from_store, args:"; val (ctxt, subst, form, errpatID, thm) =
1.170 - (ctxt, subst, f_curr, errpatID, hd (*simulate beginning of "map"*) errpatthms);
1.171 - val thmDeriv = Thm.get_name_hint thm
1.172 - val (part, thyID) = Thy_Read.thy_containing_thm thmDeriv
1.173 - val theID = [part, thyID, "Theorems", ThmC.cut_id thmDeriv]
1.174 - val Thy_Write.Hthm {fillpats, ...} = Thy_Read.from_store ctxt theID
1.175 - val some = map (Error_Pattern.fill_form ctxt subst (thm, form) errpatID) fillpats;
1.176 +(* final test ... ----------------------------------------------------------------------------*)
1.177 +val 6 = length return_from_find_fill_patterns
1.178 +val (fill_in_id, term, thm, subst) :: _ = return_from_find_fill_patterns
1.179
1.180 -case some |> filter is_some |> map the of
1.181 - ("fill-d_d-arg", tm, thm, subsopt) :: _ => if UnparseC.term tm =
1.182 - "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4)) =\nd_d x (x \<up> 2) + cos (x \<up> 4) * d_d x ?_dummy_1"
1.183 - then () else error "find_fill_patterns changed 2a"
1.184 -| _ => error "find_fill_patterns changed 2b"
1.185 +val "fill-d_d-arg" = fill_in_id
1.186 +val "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4)) =\nd_d x (x \<up> 2) + cos (x \<up> 4) * d_d x ?_dummy_1" =
1.187 + UnparseC.term_in_ctxt @{context} term
1.188 +val "Diff.diff_sin_chain" = Thm.get_name_hint thm
1.189 +val "[(''bdv'', x)]" = subst |> the |> Subst.string_of_input;
1.190
1.191 -"~~~~~ fun fill_form, args:";
1.192 - val ((subs_opt, subst), (thm, form), errpatID, (fillpatID, pat, erpaID)) =
1.193 - (subst, (thm, form), errpatID, hd (*simulate beginning of "map"*) fillpats);
1.194 -val (form', _, _, rewritten) =
1.195 - rew_sub ctxt 1 subst Rewrite_Ord.function_empty Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form;
1.196 -
1.197 -if UnparseC.term form' = "d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x ?_dummy_1" then ()
1.198 -else error "find_fill_patterns changed 3";
1.199 -
1.200 -"~~~~~ to findFillpatterns return val:"; val (fillpats) =
1.201 - (map (Error_Pattern.fill_from_store ctxt (subs_opt, subst) f_curr errpatID) errpatthms |> flat) (*only from "hd errpatthms"*);
1.202 -
1.203 -"vvv--- dropped this code WN120730";
1.204 -val msg = "fill patterns " ^
1.205 - ((map ((apsnd UnparseC.term) o quad2pair) fillpats) |> map pair2str_ |> strs2str_);
1.206 -msg =
1.207 - "fill patterns #fill-d_d-arg#d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" ^
1.208 - " =\nd_d x (x \<up> 2) + cos (x \<up> 4) * d_d x ?_dummy_1" ^
1.209 - "#fill-both-args#d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" ^
1.210 - " =\nd_d x (x \<up> 2) + cos ?_dummy_2 * d_d x ?_dummy_3" ^
1.211 - "#fill-d_d#d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" ^
1.212 - " =\nd_d x (x \<up> 2) + cos (x \<up> 4) * ?_dummy_1 x (x \<up> 4)" ^
1.213 - "#fill-inner-deriv#d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" ^
1.214 - " =\nd_d x (x \<up> 2) + cos (x \<up> 4) * ?_dummy_1" ^
1.215 - "#fill-all#d_d x (x \<up> 2) + d_d x (sin (x \<up> 4)) = d_d x (x \<up> 2) + ?_dummy_1#";
1.216 -" \<up> --- dropped this code WN120730";
1.217 -
1.218 -if (map #1 fillpats) =
1.219 - ["fill-d_d-arg", "fill-both-args", "fill-d_d", "fill-inner-deriv", "fill-all"]
1.220 -then () else error "find_fill_patterns changed 4b";
1.221 -DEconstrCalcTree 1;
1.222
1.223 "--------- build fun is_exactly_equal, inputFillFormula ----------";
1.224 "--------- build fun is_exactly_equal, inputFillFormula ----------";