1.1 --- a/src/Tools/isac/Frontend/interface.sml Mon May 21 07:59:57 2012 +0200
1.2 +++ b/src/Tools/isac/Frontend/interface.sml Mon May 21 16:56:01 2012 +0200
1.3 @@ -52,6 +52,7 @@
1.4 val setNextTactic : calcID -> tac -> unit
1.5 val setProblem : calcID -> pblID -> unit
1.6 val setTheory : calcID -> thyID -> unit
1.7 + val FindFillpatterns : calcID -> errpatID -> unit
1.8 (*------------ for tests*)
1.9 val encode: cterm' -> cterm'
1.10 val encode_fmz: fmz -> fmz
1.11 @@ -734,18 +735,14 @@
1.12 in matchmet2xml cI chd end)
1.13 handle _ => sysERROR2xml cI "error in kernel");
1.14
1.15 -
1.16 -
1.17 -(*.match a theorem, a ruleset (etc., selected in the knowledge-browser)
1.18 -with the formula in the focus on the worksheet;
1.19 -string contains the thy, thus it is unique as thmID, rlsID for this thy;
1.20 -take the substitution from the istate of the formula.*)
1.21 +(* match a theorem, a ruleset (etc., selected in the knowledge-browser)
1.22 + with the formula in the focus on the worksheet;
1.23 + string contains the thy, thus it is unique as thmID, rlsID for this thy;
1.24 + take the substitution from the istate of the formula *)
1.25 (* use"../smltest/Knowledge/poly.sml";
1.26 - val (cI, pos as (p,p_), guh) = (1, ([1,1,1], Frm),
1.27 - "thy_Poly-thm-real_diff_minus");
1.28 + val (cI, pos as (p,p_), guh) = (1, ([1,1,1], Frm), "thy_Poly-thm-real_diff_minus");
1.29 val (cI, pos as (p,p_), guh) = (1, ([1,1], Frm), "norm_Poly");
1.30 - val (cI, pos as (p,p_), guh) =
1.31 - (1, ([1], Res), "thy_isac_Test-rls-Test_simplify");
1.32 + val (cI, pos as (p,p_), guh) = (1, ([1], Res), "thy_isac_Test-rls-Test_simplify");
1.33 *)
1.34 fun checkContext (cI:calcID) (pos:pos' as (p,p_)) (guh:guh) =
1.35 (case (implode o (take_fromto 1 4) o Symbol.explode) guh of
1.36 @@ -787,6 +784,15 @@
1.37 in matchmet2xml cI chd end)
1.38 handle _ => sysERROR2xml cI "error in kernel";
1.39
1.40 +(* for an errpatID find "(fillpatID, fillform)" list
1.41 + which dedicated to this errpat and which is applicable at current formula*)
1.42 +fun FindFillpatterns cI errpatID =
1.43 + let
1.44 + val ((pt, _), _) = get_calc cI
1.45 + val pos = get_pos cI 1;
1.46 + val fillpats = find_fillpatterns (pt, pos) errpatID
1.47 + (* the format for the message's arguments is waiting for generalisation of CalcMessage *)
1.48 + in calcMessage2xml cI ("fill patterns " ^ (fillpats |> map pair2str_ |> strs2str_)) end;
1.49
1.50 (*------------------------------------------------------------------*)
1.51 end
2.1 --- a/src/Tools/isac/Interpret/inform.sml Mon May 21 07:59:57 2012 +0200
2.2 +++ b/src/Tools/isac/Interpret/inform.sml Mon May 21 16:56:01 2012 +0200
2.3 @@ -694,7 +694,7 @@
2.4 val pos_pred = lev_back' pos
2.5 (* f_pred ---"step pos cs"---> f_succ in appendFormula *)
2.6 val f_pred = get_pred_formula (pt, pos_pred)
2.7 - val msg_calcstate' = compare_step ([], [], (pt, pos_pred)) f_in
2.8 + val msg_calcstate' = compare_step ([], [], (pt, pos_pred)) f_in (*<<=====*)
2.9 (*last step re-calc in compare_step TODO before WN09*)
2.10 in
2.11 case msg_calcstate' of
2.12 @@ -713,6 +713,36 @@
2.13 end
2.14 | NONE => ("syntax error in '" ^ istr ^ "'", e_calcstate');
2.15
2.16 +(* fill-in patterns an forms *)
2.17 +fun get_fillform subst form errpatID ((fillpatID, pat, erpaID): fillpat) =
2.18 + let
2.19 + val (form', _, _, rewritten) =
2.20 + rew_sub (Isac()) 1 subst e_rew_ord e_rls false [] (Trueprop $ pat) form;
2.21 + in (*the fillpat of the thm must be dedicated to errpatID*)
2.22 + if errpatID = erpaID andalso rewritten
2.23 + then SOME (fillpatID, term2str (HOLogic.mk_eq (form, form'))) else NONE end;
2.24 +
2.25 +fun get_fillpats subst form errpatID thm =
2.26 + let
2.27 + val thmDeriv = Thm.get_name_hint thm
2.28 + val (part, thyID) = thy_containing_thm thmDeriv
2.29 + val theID = [part, thyID, "Theorems", thmID_of_derivation_name thmDeriv]
2.30 + val Hthm {fillpats, ...} = get_the theID
2.31 + val some = map (get_fillform subst form errpatID) fillpats
2.32 + in some |> filter is_some |> map the end;
2.33 +
2.34 +fun find_fillpatterns (pt, pos as (p, _): pos') errpatID =
2.35 + let
2.36 + val f_curr = get_pred_formula (pt, pos); (* = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"*)
2.37 + val pp = par_pblobj pt p
2.38 + val {errpats, scr = Script prog, ...} = get_met (get_obj g_metID pt pp)
2.39 + val ScrState (env, _, _, _, _, _) = get_istate pt pos
2.40 + val subst = get_bdv_subst prog env
2.41 + val errpatthms = errpats
2.42 + |> filter ((curry op = errpatID) o (#1: errpat -> errpatID))
2.43 + |> map (#3: errpat -> thm list)
2.44 + |> flat
2.45 + in map (get_fillpats subst f_curr errpatID) errpatthms |> flat end;
2.46
2.47 (*------------------------------------------------------------------(**)
2.48 end
3.1 --- a/src/Tools/isac/calcelems.sml Mon May 21 07:59:57 2012 +0200
3.2 +++ b/src/Tools/isac/calcelems.sml Mon May 21 16:56:01 2012 +0200
3.3 @@ -638,7 +638,7 @@
3.4 in ass (!calclist') : calcID end;
3.5
3.6 fun term2str t = Print_Mode.setmp [] (Syntax.string_of_term
3.7 -(ProofContext.init_global (Thy_Info.get_theory "Isac"))) t;
3.8 + (ProofContext.init_global (Thy_Info.get_theory "Isac"))) t;
3.9
3.10 fun terms2str ts = (strs2str o (map term2str )) ts;
3.11 (*terms2str [t1,t2] = "[\"1 + 2\",\"abc\"]";*)
4.1 --- a/src/Tools/isac/library.sml Mon May 21 07:59:57 2012 +0200
4.2 +++ b/src/Tools/isac/library.sml Mon May 21 16:56:01 2012 +0200
4.3 @@ -214,10 +214,10 @@
4.4 fun ints2str ints = (strs2str o (map string_of_int)) ints;
4.5 fun ints2str' ints = (strs2str' o (map string_of_int)) ints;
4.6
4.7 -
4.8 -(* use"library.sml";
4.9 - *)
4.10 -
4.11 +(* FindFillpatterns: the message's format is waiting for generalisation of CalcMessage *)
4.12 +fun pair2str_ (s1,s2) = s1 ^ "#" ^ s2;
4.13 +val nos = space_implode "#";
4.14 +fun strs2str_ strl = "#" ^ (nos strl) ^ "#";
4.15
4.16 (*needed in Isa + ME*)
4.17 fun get_thy str =
5.1 --- a/src/Tools/isac/xmlsrc/interface-xml.sml Mon May 21 07:59:57 2012 +0200
5.2 +++ b/src/Tools/isac/xmlsrc/interface-xml.sml Mon May 21 16:56:01 2012 +0200
5.3 @@ -316,6 +316,11 @@
5.4 " <CALCMESSAGE> "^ e ^" </CALCMESSAGE>\n" ^
5.5 "@@@@@end@@@@@");
5.6
5.7 +fun calcMessage2xml (cI:calcID) e =
5.8 + writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
5.9 + " <CALCMESSAGE> "^ e ^" </CALCMESSAGE>\n" ^
5.10 + "@@@@@end@@@@@");
5.11 +
5.12 fun modifycalcheadOK2xml (cI:calcID) (chd as (complete,p_,_,_,_,_):ocalhd) =
5.13 writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
5.14 "<MODIFYCALCHEAD>\n" ^
6.1 --- a/test/Tools/isac/Frontend/interface.sml Mon May 21 07:59:57 2012 +0200
6.2 +++ b/test/Tools/isac/Frontend/interface.sml Mon May 21 16:56:01 2012 +0200
6.3 @@ -704,7 +704,7 @@
6.4 "--------- this is a matching model (all items correct): -------";
6.5 checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
6.6 "--------- this is a NOT matching model (some 'false': ---------";
6.7 -checkContext 1 ([],Pbl)(kestoreID2guh Pbl_["linear","univariate","equation"]);
6.8 +checkContext 1 ([],Pbl)(kestoreID2guh Pbl_ ["linear","univariate","equation"]);
6.9
6.10 "--------- find out a matching problem: ------------------------";
6.11 "--------- find out a matching problem (FAILING: no new pbl) ---";
7.1 --- a/test/Tools/isac/Interpret/inform.sml Mon May 21 07:59:57 2012 +0200
7.2 +++ b/test/Tools/isac/Interpret/inform.sml Mon May 21 16:56:01 2012 +0200
7.3 @@ -35,6 +35,7 @@
7.4 "--------- build fun check_err_patt ?bdv -------------------------";
7.5 "--------- build fun check_error_patterns ------------------------";
7.6 "--------- embed fun check_error_patterns ------------------------";
7.7 +"--------- embed fun find_fillpatterns ---------------------------";
7.8 "-----------------------------------------------------------------";
7.9 "-----------------------------------------------------------------";
7.10 "-----------------------------------------------------------------";
7.11 @@ -956,3 +957,53 @@
7.12 ("error pattern #chain-rule-diff-both#", calcstate') => ()
7.13 | _ => error "inform with (positive) check_error_patterns broken"
7.14
7.15 +"--------- embed fun find_fillpatterns ---------------------------";
7.16 +"--------- embed fun find_fillpatterns ---------------------------";
7.17 +"--------- embed fun find_fillpatterns ---------------------------";
7.18 +states:=[];
7.19 +CalcTree
7.20 +[(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
7.21 + ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
7.22 +Iterator 1;
7.23 +moveActiveRoot 1;
7.24 +autoCalculate 1 CompleteCalcHead;
7.25 +autoCalculate 1 (Step 1);
7.26 +autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
7.27 +appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)";
7.28 + (*<CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>*)
7.29 + (*TODO BACK TO <CALCMESSAGE> no derivation found </CALCMESSAGE>*)
7.30 +
7.31 +"~~~~~ fun FindFillpatterns, args:"; val (cI, errpatID) = (1, "chain-rule-diff-both");
7.32 + val ((pt, _), _) = get_calc cI
7.33 + val pos = get_pos cI 1;
7.34 + "~~~~~ fun find_fillpatterns, args:"; val ((pt, pos as (p, _)), errpatID) = ((pt, pos), errpatID);
7.35 + val f_curr = get_pred_formula (pt, pos); (* = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"*)
7.36 + val pp = par_pblobj pt p
7.37 + val {errpats, scr = Script prog, ...} = get_met (get_obj g_metID pt pp)
7.38 + val ScrState (env, _, _, _, _, _) = get_istate pt pos
7.39 + val subst = get_bdv_subst prog env
7.40 + val errpatthms = errpats
7.41 + |> filter ((curry op = errpatID) o (#1: errpat -> errpatID))
7.42 + |> map (#3: errpat -> thm list)
7.43 + |> flat;
7.44 +
7.45 +case map (get_fillpats subst f_curr errpatID) errpatthms |> flat of
7.46 + ("fill-d_d-arg",
7.47 + "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1")
7.48 + :: _ => ()
7.49 +| _ => error "find_fillpatterns changed"
7.50 +
7.51 +"~~~~~ fun get_fillpats, args:"; val (subst, form, errpatID, thm) =
7.52 + (subst, f_curr, errpatID, hd errpatthms);
7.53 + val thmDeriv = Thm.get_name_hint thm
7.54 + val (part, thyID) = thy_containing_thm thmDeriv
7.55 + val theID = [part, thyID, "Theorems", thmID_of_derivation_name thmDeriv]
7.56 + val Hthm {fillpats, ...} = get_the theID
7.57 + val some = map (get_fillform subst form errpatID) fillpats;
7.58 +
7.59 +case some |> filter is_some |> map the of
7.60 + ("fill-d_d-arg",
7.61 + "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1")
7.62 + :: _ => ()
7.63 +| _ => error "get_fillpats changed"
7.64 +
8.1 --- a/test/Tools/isac/Test_Some.thy Mon May 21 07:59:57 2012 +0200
8.2 +++ b/test/Tools/isac/Test_Some.thy Mon May 21 16:56:01 2012 +0200
8.3 @@ -1,7 +1,7 @@
8.4
8.5 theory Test_Some imports Isac begin
8.6
8.7 -use"../../../test/Tools/isac/xmlsrc/thy-hierarchy.sml"
8.8 +use"../../../test/Tools/isac/Interpret/inform.sml"
8.9
8.10 ML {*
8.11 val thy = @{theory "Isac"};
8.12 @@ -11,39 +11,6 @@
8.13 ML {*
8.14 *}
8.15 ML {* (*==================*)
8.16 -val fillpats = [
8.17 - ("fill-d_d-arg",
8.18 - parse_patt thy "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),
8.19 - ("fill-both-args",
8.20 - parse_patt thy "d_d ?bdv (sin _) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),
8.21 - ("fill-d_d",
8.22 - parse_patt thy "d_d ?bdv (sin ?u) = cos ?u * _ ?bdv ?u", "chain-rule-diff-both"),
8.23 - ("fill-inner-deriv",
8.24 - parse_patt thy "d_d ?bdv (sin ?u) = cos ?u * _", "chain-rule-diff-both"),
8.25 - ("fill-all",
8.26 - parse_patt thy "d_d ?bdv (sin ?u) = _", "chain-rule-diff-both")]: fillpat list;
8.27 -
8.28 -val Hthm {fillpats, ...} =
8.29 - get_the ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"];
8.30 -case fillpats of
8.31 - ("fill-d_d-arg", tm, "chain-rule-diff-both") :: _ => ()
8.32 -| _ => error "insert_fillpats changed"
8.33 -
8.34 -*}
8.35 -ML {*
8.36 -*}
8.37 -ML {*
8.38 -
8.39 -*}
8.40 -
8.41 -ML {* (*==================*)
8.42 -"--------- build fun get_fill_patt -------------------------------";
8.43 -val res = str2term "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"
8.44 -*}
8.45 -ML {*
8.46 -@{thm diff_sin_chain}
8.47 -*}
8.48 -ML {* (*==================*)
8.49 *}
8.50 ML {*
8.51 *}