1.1 --- a/test/Tools/isac/Interpret/inform.sml	Fri May 25 09:58:20 2012 +0200
     1.2 +++ b/test/Tools/isac/Interpret/inform.sml	Fri May 25 16:30:15 2012 +0200
     1.3 @@ -1030,3 +1030,84 @@
     1.4    "#fill-all#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) = d_d x (x ^^^ 2) + ?_dummy_1#"
     1.5  then () else error "find_fillpatterns changed 4";
     1.6  
     1.7 +"--------- build fun is_exactly_equal, inputFillFormula ----------";
     1.8 +"--------- build fun is_exactly_equal, inputFillFormula ----------";
     1.9 +"--------- build fun is_exactly_equal, inputFillFormula ----------";
    1.10 +states := [];
    1.11 +CalcTree
    1.12 +[(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"], 
    1.13 +  ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
    1.14 +Iterator 1;
    1.15 +moveActiveRoot 1;
    1.16 +autoCalculate 1 CompleteCalcHead;
    1.17 +autoCalculate 1 (Step 1);
    1.18 +autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
    1.19 +appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)"; (*<<<<<<<=========================*)
    1.20 +(* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),
    1.21 +  would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well.
    1.22 +  results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>
    1.23 +  instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)
    1.24 +  val ((pt,pos), _) = get_calc 1;
    1.25 +  val p = get_pos 1 1;
    1.26 +  val (Form f, _, asms) = pt_extract (pt, p);
    1.27 +
    1.28 +  if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
    1.29 +    get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sum", "Diff.diff_sum"(*?!?*)))
    1.30 +  then () else error "embed fun get_fillform changed 1";
    1.31 +
    1.32 +findFillpatterns 1 "chain-rule-diff-both"; (*<<<<<<<=================================*)
    1.33 +(*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =
    1.34 +  d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *)
    1.35 +  val ((pt,pos),_) = get_calc 1;
    1.36 +  val p = get_pos 1 1;
    1.37 +
    1.38 +  val (Form f, _, asms) = pt_extract (pt, p);
    1.39 +  if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
    1.40 +    get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sum", "Diff.diff_sum"(*?!?*)))
    1.41 +  then ()
    1.42 +  else error "embed fun get_fillform changed 2";
    1.43 +
    1.44 +requestFillformula 1 ("chain-rule-diff-both", "fill-both-args");(*<<<<<<<============*)
    1.45 +  (*<AUTOCALC> ([1], Res) ([2], Res) ([2], Res) </AUTOCALC>*)
    1.46 +  val ((pt,pos),_) = get_calc 1;
    1.47 +  val p = get_pos 1 1;
    1.48 +  val (Form f, _, asms) = pt_extract (pt, p);
    1.49 +  if p = ([1], Res) andalso existpt [2] pt andalso
    1.50 +    term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
    1.51 +    get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sum", "Diff.diff_sum"))
    1.52 +  then () else error "embed fun get_fillform changed 3";
    1.53 +
    1.54 +(* input a formula which exactly fills the gaps in a "fillformula"
    1.55 +   presented to the learner immediately before by "requestFillformula (errpatID, fillpatID)":
    1.56 +   errpatID: lhs of the respective thm = lhs of fillformula with fillpatID.
    1.57 +   the respective thm is in the ctree ................
    1.58 +*)
    1.59 +"~~~~~ fun inputFillFormula, args:"; val (cI, ifo) =
    1.60 +  (1, "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)");
    1.61 +    val ((pt, _), _) = get_calc cI
    1.62 +    val pos = get_pos cI 1;
    1.63 +
    1.64 +"~~~~~ fun is_exactly_equal, args:"; val ((pt, pos as (p, p_)), istr) = ((pt, pos), ifo);
    1.65 +  val SOME ifo = parseNEW (assoc_thy "Isac" |> thy2ctxt) istr
    1.66 +  val p' = lev_on p;
    1.67 +  val tac = get_obj g_tac pt p';
    1.68 +  if tac = Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", "")) then ()
    1.69 +  else error "inputFillFormula changed 10";
    1.70 +  val Appl rew = applicable_in pos pt tac;
    1.71 +  val Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) = rew;
    1.72 +
    1.73 +"~~~~~ to inputFillFormula return val:"; val ("ok", tac) = ("ok", tac);
    1.74 +  val ("ok", (_, c, ptp as (_,p'))) = locatetac tac (pt, pos);
    1.75 +    upd_calc cI (ptp, []);
    1.76 +    upd_ipos cI 1 p';
    1.77 +    autocalculateOK2xml cI pos (if null c then p' else last_elem c) p';
    1.78 +
    1.79 +"~~~~~ final check:";
    1.80 +val ((pt, _),_) = get_calc 1;
    1.81 +val p = get_pos 1 1;
    1.82 +val (Form f, _, asms) = pt_extract (pt, p);
    1.83 +if p = ([2], Res) andalso
    1.84 +  term2str f = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)" andalso
    1.85 +  get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", ""))
    1.86 +then () else error "inputFillFormula changed 11";
    1.87 +