1.1 --- a/test/Tools/isac/Interpret/inform.sml	Mon May 21 07:59:57 2012 +0200
     1.2 +++ b/test/Tools/isac/Interpret/inform.sml	Mon May 21 16:56:01 2012 +0200
     1.3 @@ -35,6 +35,7 @@
     1.4  "--------- build fun check_err_patt ?bdv -------------------------";
     1.5  "--------- build fun check_error_patterns ------------------------";
     1.6  "--------- embed fun check_error_patterns ------------------------";
     1.7 +"--------- embed fun find_fillpatterns ---------------------------";
     1.8  "-----------------------------------------------------------------";
     1.9  "-----------------------------------------------------------------";
    1.10  "-----------------------------------------------------------------";
    1.11 @@ -956,3 +957,53 @@
    1.12    ("error pattern #chain-rule-diff-both#", calcstate') => ()
    1.13  | _ => error "inform with (positive) check_error_patterns broken"
    1.14  
    1.15 +"--------- embed fun find_fillpatterns ---------------------------";
    1.16 +"--------- embed fun find_fillpatterns ---------------------------";
    1.17 +"--------- embed fun find_fillpatterns ---------------------------";
    1.18 +states:=[];
    1.19 +CalcTree
    1.20 +[(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"], 
    1.21 +  ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
    1.22 +Iterator 1;
    1.23 +moveActiveRoot 1;
    1.24 +autoCalculate 1 CompleteCalcHead;
    1.25 +autoCalculate 1 (Step 1);
    1.26 +autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
    1.27 +appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)";
    1.28 +  (*<CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>*)
    1.29 +  (*TODO BACK TO <CALCMESSAGE> no derivation found </CALCMESSAGE>*)
    1.30 +
    1.31 +"~~~~~ fun FindFillpatterns, args:"; val (cI, errpatID) = (1, "chain-rule-diff-both");
    1.32 +  val ((pt, _), _) = get_calc cI
    1.33 +				val pos = get_pos cI 1;
    1.34 +			"~~~~~ fun find_fillpatterns, args:"; val ((pt, pos as (p, _)), errpatID) = ((pt, pos), errpatID);
    1.35 +	    val f_curr = get_pred_formula (pt, pos); (* = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"*)
    1.36 +    val pp = par_pblobj pt p
    1.37 +			    val {errpats, scr = Script prog, ...} = get_met (get_obj g_metID pt pp)
    1.38 +    val ScrState (env, _, _, _, _, _) = get_istate pt pos
    1.39 +    val subst = get_bdv_subst prog env
    1.40 +    val errpatthms = errpats
    1.41 +      |> filter ((curry op = errpatID) o (#1: errpat -> errpatID))
    1.42 +      |> map (#3: errpat -> thm list)
    1.43 +      |> flat;
    1.44 +
    1.45 +case map (get_fillpats subst f_curr errpatID) errpatthms |> flat of
    1.46 + ("fill-d_d-arg",
    1.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")
    1.48 +    :: _ => ()
    1.49 +| _ => error "find_fillpatterns changed"
    1.50 +
    1.51 +"~~~~~ fun get_fillpats, args:"; val (subst, form, errpatID, thm) =
    1.52 +  (subst, f_curr, errpatID, hd errpatthms);
    1.53 +        val thmDeriv = Thm.get_name_hint thm
    1.54 +        val (part, thyID) = thy_containing_thm thmDeriv
    1.55 +        val theID = [part, thyID, "Theorems", thmID_of_derivation_name thmDeriv]
    1.56 +        val Hthm {fillpats, ...} = get_the theID
    1.57 +        val some = map (get_fillform subst form errpatID) fillpats;
    1.58 +
    1.59 +case some |> filter is_some |> map the of
    1.60 +  ("fill-d_d-arg",
    1.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")
    1.62 +    :: _ => ()
    1.63 +| _ => error "get_fillpats changed"
    1.64 +