1.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy Fri Aug 03 15:44:39 2012 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy Sat Aug 04 10:43:07 2012 +0200
1.3 @@ -129,15 +129,15 @@
1.4
1.5 insert_fillpats ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"]
1.6 ([("fill-d_d-arg",
1.7 - parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),
1.8 - ("fill-both-args",
1.9 - parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos _ * d_d ?bdv _", "chain-rule-diff-both"),
1.10 - ("fill-d_d",
1.11 - parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * _ ?bdv ?u", "chain-rule-diff-both"),
1.12 - ("fill-inner-deriv",
1.13 - parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * _", "chain-rule-diff-both"),
1.14 - ("fill-all",
1.15 - parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = _", "chain-rule-diff-both")]: fillpat list);
1.16 + parse_patt thy "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),
1.17 + ("fill-both-args",
1.18 + parse_patt thy "d_d ?bdv (sin _) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),
1.19 + ("fill-d_d",
1.20 + parse_patt thy "d_d ?bdv (sin ?u) = cos ?u * _ ?bdv ?u", "chain-rule-diff-both"),
1.21 + ("fill-inner-deriv",
1.22 + parse_patt thy "d_d ?bdv (sin ?u) = cos ?u * _", "chain-rule-diff-both"),
1.23 + ("fill-all",
1.24 + parse_patt thy "d_d ?bdv (sin ?u) = _", "chain-rule-diff-both")]: fillpat list);
1.25
1.26 (*
1.27 val fillpats = [
2.1 --- a/test/Tools/isac/Test_Some.thy Fri Aug 03 15:44:39 2012 +0200
2.2 +++ b/test/Tools/isac/Test_Some.thy Sat Aug 04 10:43:07 2012 +0200
2.3 @@ -112,97 +112,8 @@
2.4 | _ => error "insert_fillpats changed"
2.5 *}
2.6 ML {* (*==================*)
2.7 -"--------- UC errpat, fillpat by input ---------------------------";
2.8 -states := [];
2.9 -CalcTree
2.10 -[(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
2.11 - ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
2.12 -Iterator 1;
2.13 -moveActiveRoot 1;
2.14 -autoCalculate 1 CompleteCalcHead;
2.15 -autoCalculate 1 (Step 1);
2.16 -autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
2.17 -appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)"; (*<<<<<<<=========================*)
2.18 -(* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),
2.19 - would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well.
2.20 - results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>
2.21 - instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)
2.22 - val ((pt,pos), _) = get_calc 1;
2.23 - val p = get_pos 1 1;
2.24 - val (Form f, _, asms) = pt_extract (pt, p);
2.25 -
2.26 - if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
2.27 - get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sum", "Diff.diff_sum"(*?!?*)))
2.28 - then () else error "embed fun get_fillform changed 1";
2.29 -
2.30 -findFillpatterns 1 "chain-rule-diff-both"; (*<<<<<<<=================================*)
2.31 -(*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =
2.32 - d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *)
2.33 - val ((pt,pos),_) = get_calc 1;
2.34 - val p = get_pos 1 1;
2.35 -
2.36 - val (Form f, _, asms) = pt_extract (pt, p);
2.37 - if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
2.38 - get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sum", "Diff.diff_sum"(*?!?*)))
2.39 - then ()
2.40 - else error "embed fun get_fillform changed 2";
2.41 -
2.42 -(* if we assume, that the fill-patterns are ordered such that the 1st has large gaps
2.43 - and the last has no gaps, then the number of fill-patterns would suffice
2.44 - for the DialogGuide to select appropriately. *)
2.45 -requestFillformula 1 ("chain-rule-diff-both", "fill-both-args");(*<<<<<<<============*)
2.46 - (*<AUTOCALC> ([1], Res) ([2], Res) ([2], Res) </AUTOCALC>*)
2.47 - val ((pt,pos),_) = get_calc 1;
2.48 - val p = get_pos 1 1;
2.49 - val (Form f, _, asms) = pt_extract (pt, p);
2.50 *}
2.51 -ML {*
2.52 -print_depth 99;
2.53 -p = ([1], Res);
2.54 -existpt [2] pt;
2.55 -term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))";
2.56 -get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sum", "Diff.diff_sum"));
2.57 -print_depth 99;
2.58 -*}
2.59 -ML {*
2.60 -*}
2.61 -ML {*
2.62 - if p = ([1], Res) andalso existpt [2] pt andalso
2.63 - term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
2.64 - get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sum", "Diff.diff_sum"))
2.65 - then () else error "embed fun get_fillform changed 3";
2.66 -*}
2.67 -ML {*
2.68 -
2.69 -inputFillFormula 1 "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)";(*<<<<<<<=====*)
2.70 - val ((pt, _),_) = get_calc 1;
2.71 - val p = get_pos 1 1;
2.72 - val (Form f, _, asms) = pt_extract (pt, p);
2.73 - if p = ([2], Res) andalso
2.74 - term2str f = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)" andalso
2.75 - get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", ""))
2.76 - then () else error "inputFillFormula changed 11";
2.77 -
2.78 -autoCalculate 1 CompleteCalc;
2.79 -
2.80 -"~~~~~ final check: the input formula is inserted as it would have been correct from beginning";
2.81 -val ((pt, _),_) = get_calc 1;
2.82 -val p = get_pos 1 1;
2.83 -val (Form f, _, asms) = pt_extract (pt, p);
2.84 -if p = ([], Res) andalso term2str f = "2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3"
2.85 -then () else error "inputFillFormula changed 12";
2.86 -show_pt pt;
2.87 -(*[
2.88 -(([], Frm), Diff (x ^^^ 2 + sin (x ^^^ 4), x)),
2.89 -(([1], Frm), d_d x (x ^^^ 2 + sin (x ^^^ 4))),
2.90 -(([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))),
2.91 -(([2], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)), (*<<<<<<<=====*)
2.92 -(([3], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * (4 * x ^^^ (4 - 1))),
2.93 -(([4], Res), 2 * x ^^^ (2 - 1) + cos (x ^^^ 4) * (4 * x ^^^ (4 - 1))),
2.94 -(([5], Res), 2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3),
2.95 -(([], Res), 2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3)] *)
2.96 -*}
2.97 -ML {*
2.98 +ML {* (*==================*)
2.99 *}
2.100 ML {*
2.101 *}
3.1 --- a/test/Tools/isac/xmlsrc/thy-hierarchy.sml Fri Aug 03 15:44:39 2012 +0200
3.2 +++ b/test/Tools/isac/xmlsrc/thy-hierarchy.sml Sat Aug 04 10:43:07 2012 +0200
3.3 @@ -438,15 +438,19 @@
3.4 "----------- fun insert_errpatIDs --------------------------------";
3.5 "----------- fun insert_errpatIDs --------------------------------";
3.6 "----------- fun insert_errpatIDs --------------------------------";
3.7 +(* isolate test: 10 secs *) val original = (! thehier);
3.8 +
3.9 (* still ununsed; planned for stepToErrorpattern *)
3.10 -val errpattIDs = ["chain-rule-diff-both", "cancel"];
3.11 +val path = ["IsacKnowledge", "Diff", "Rulesets", "norm_diff"]: theID;
3.12 +val errpattIDs = ["chain-rule-diff-both", "test-errpatID"];
3.13
3.14 -insert_errpatIDs ["IsacKnowledge", "Diff", "Rulesets", "norm_diff"] errpattIDs;
3.15 +insert_errpatIDs path errpattIDs;
3.16
3.17 -val Hrls {guh, coursedesign, mathauthors, thy_rls = (thyID, rls)} =
3.18 - get_the ["IsacKnowledge", "Diff", "Rulesets", "norm_diff"]
3.19 +val Hrls {guh, coursedesign, mathauthors, thy_rls = (thyID, rls)} = get_the path
3.20 val Rls {id, preconds, rew_ord, erls, srls, calc, rules, scr, errpatts} = rls;
3.21
3.22 -if errpatts = ["chain-rule-diff-both", "cancel"] then ()
3.23 +if errpattIDs = ["chain-rule-diff-both", "test-errpatID"] then ()
3.24 else error "insert_errpatIDs to norm_diff changed";
3.25
3.26 +(* isolate test: 10 secs *) thehier := original;
3.27 +