1.1 --- a/test/Tools/isac/Interpret/inform.sml Thu May 24 17:13:58 2012 +0200
1.2 +++ b/test/Tools/isac/Interpret/inform.sml Thu May 24 18:40:07 2012 +0200
1.3 @@ -1106,72 +1106,4 @@
1.4 then () else error "";
1.5
1.6 show_pt pt; (*ATTENTION: omits the last step, if pt is incomplete, ([2], Res) EXISTS !*)
1.7 -"--------- embed fun get_fillformula -----------------------------";
1.8 -states := [];
1.9 -CalcTree
1.10 -[(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
1.11 - ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
1.12 -Iterator 1;
1.13 -moveActiveRoot 1;
1.14 -autoCalculate 1 CompleteCalcHead;
1.15 -autoCalculate 1 (Step 1);
1.16 -autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
1.17 -appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)";
1.18 -(* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),
1.19 - would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well.
1.20 - results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>
1.21 - instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)
1.22 -findFillpatterns 1 "chain-rule-diff-both";
1.23 -(*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =
1.24 - d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *)
1.25
1.26 -"~~~~~ fun requestFillformula, args:"; val (cI, (errpatID, fillpatID)) =
1.27 - (1, ("chain-rule-diff-both", "fill-both-args"));
1.28 -val ((pt, _), _) = get_calc cI
1.29 -val pos = get_pos cI 1; (* = ([1], Res)*)
1.30 -
1.31 -"~~~~~ fun get_fillformula, args:"; val ((pt, pos as (p, _)), (errpatID, fillpatID)) =
1.32 - ((pt, pos), (errpatID, fillpatID));
1.33 -val fillforms = find_fillpatterns (pt, pos) errpatID
1.34 -val fillforms =
1.35 - filter ((curry op = fillpatID) o (#1: (fillpatID * term * thm * (subs option) -> fillpatID))) fillforms;
1.36 -
1.37 -val [(fillpatID, fillform, thm, subs_opt)] = fillforms;
1.38 -case (fillpatID, fillform, thm, subs_opt) of
1.39 - ("fill-both-args", tm, thm, subs_opt) => if term2str tm =
1.40 - "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos ?_dummy_2 * d_d x ?_dummy_3"
1.41 - then () else error "get_fillformula changed 1a"
1.42 -| _ => error "get_fillformula changed 1b";
1.43 -
1.44 - val f_curr = get_curr_formula (pt, pos); (*already done in find_fillpatterns, too*)
1.45 -term2str f_curr = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))";
1.46 -
1.47 -"~~~~~ fun generate_inconsistent, args:";
1.48 - val (_, (Rewrite' (_,_,_,_, thm', f, (f', asm))), (is, ctxt), (p,_), pt) =
1.49 - (0,
1.50 - (Rewrite' ("","",e_rls,true, (fillpatID, ""(*errpatthm known in find_fillpatterns*)),
1.51 - f_curr, (fillform, []))),
1.52 - (get_loc pt pos), (lev_on p, Und), pt);
1.53 -if p = [2] then () else error "generate_inconsistent changed 1";
1.54 -
1.55 -val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
1.56 - (Rewrite thm') (f', asm) Inconsistent
1.57 -val pt = update_branch pt p TransitiveB;
1.58 -
1.59 -"~~~~~ to get_fillformula return val:"; val (pos', _, _, pt) =
1.60 - ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt);
1.61 -if pos' = ([2], Res) then () else error "generate_inconsistent changed 2";
1.62 -
1.63 -upd_calc cI ((pt, pos'), []); upd_ipos cI 1 pos';
1.64 -autocalculateOK2xml cI pos pos' pos';
1.65 -
1.66 -"~~~~~ final check:";
1.67 -val ((pt,pos),_) = get_calc 1;
1.68 -val p = get_pos 1 1;
1.69 -val (Form f, tac, asms) = pt_extract (pt, p);
1.70 -if p = ([2], Res) andalso term2str f =
1.71 - "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos ?_dummy_2 * d_d x ?_dummy_3"
1.72 -then () else error "";
1.73 -
1.74 -show_pt pt; (*ATTENTION: omits the last step, if pt is incomplete, ([2], Res) EXISTS !*)
1.75 -