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