1.1 --- a/test/Tools/isac/Interpret/inform.sml	Thu May 17 16:44:13 2012 +0200
     1.2 +++ b/test/Tools/isac/Interpret/inform.sml	Thu May 17 19:09:48 2012 +0200
     1.3 @@ -33,6 +33,8 @@
     1.4  "--------- init_form, start with <NEW> (CAS input) ---------------";
     1.5  "--------- build fun check_err_patt ------------------------------";
     1.6  "--------- build fun check_err_patt ?bdv -------------------------";
     1.7 +"--------- build fun check_error_patterns ------------------------";
     1.8 +"--------- embed fun check_error_patterns ------------------------";
     1.9  "-----------------------------------------------------------------";
    1.10  "-----------------------------------------------------------------";
    1.11  "-----------------------------------------------------------------";
    1.12 @@ -869,4 +871,88 @@
    1.13  if check_err_patt (res, inf) (subst: subst) ("errpatID": errpatID, pat) rls = SOME "errpatID"
    1.14  then () else error "error patt example1 changed";
    1.15  
    1.16 +"--------- build fun check_error_patterns ------------------------";
    1.17 +"--------- build fun check_error_patterns ------------------------";
    1.18 +"--------- build fun check_error_patterns ------------------------";
    1.19 +val (res, inf) =
    1.20 +  (str2term "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))",
    1.21 +   str2term "d_d x (x ^^^ 2) + cos (4 * x ^^^ 3)");
    1.22 +val {errpats, nrls = rls, scr = Script prog, ...} = get_met ["diff", "differentiate_on_R"]
    1.23  
    1.24 +val env = [(str2term "v_v", str2term "x")];
    1.25 +val errpats =
    1.26 +  [e_errpat, (*generalised for testing*)
    1.27 +   ("chain-rule-diff-both",
    1.28 +     [parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)",
    1.29 +      parse_patt @{theory} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)",
    1.30 +      parse_patt @{theory} "d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1)",
    1.31 +      parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u",
    1.32 +      parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"],
    1.33 +     [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain}, 
    1.34 +      @{thm diff_ln_chain}, @{thm  diff_exp_chain}])]: errpat list;
    1.35 +
    1.36 +case check_error_patterns (res, inf) (prog, env) (errpats, rls) of SOME _ => () 
    1.37 +| NONE => error "check_error_patterns broken";
    1.38 +
    1.39 +
    1.40 +"--------- embed fun check_error_patterns ------------------------";
    1.41 +"--------- embed fun check_error_patterns ------------------------";
    1.42 +"--------- embed fun check_error_patterns ------------------------";
    1.43 +states:=[];
    1.44 +CalcTree
    1.45 +[(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"], 
    1.46 +  ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
    1.47 +Iterator 1;
    1.48 +moveActiveRoot 1;
    1.49 +autoCalculate 1 CompleteCalcHead;
    1.50 +autoCalculate 1 (Step 1);
    1.51 +autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
    1.52 +(*autoCalculate 1 (Step 1);([2], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)*)
    1.53 +
    1.54 +"~~~~~ fun appendFormula, args:"; val (cI, (ifo:cterm')) = (1, "d_d x (x ^ 2) + cos (4 * x ^ 3)");
    1.55 +val cs = get_calc cI
    1.56 +val pos as (_,p_) = get_pos cI 1; (*pos = ([1], Res)*)
    1.57 +val cs' = 
    1.58 +    case step pos cs of
    1.59 +	    ("ok", cs') => cs';
    1.60 +
    1.61 +val (_, _, (pt, ([2], Res))) = cs';
    1.62 +(*show_pt pt;
    1.63 +  [(([], Frm), Diff (x ^^^ 2 + sin (x ^^^ 4), x)),
    1.64 +   (([1], Frm), d_d x (x ^^^ 2 + sin (x ^^^ 4))),
    1.65 +   (([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))), <<=== input follos: "...+ cos(4.x^3)"
    1.66 +   (([2], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4))] *)
    1.67 +
    1.68 +"~~~~~ fun inform, args:"; val ((cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate'), istr) =
    1.69 +  (cs', (encode ifo));
    1.70 +val 	SOME f_in = parse (assoc_thy "Isac") istr
    1.71 +val f_in = term_of f_in
    1.72 +val pos_pred = lev_back' pos
    1.73 +			(* f_pred ---"step pos cs"---> f_succ in appendFormula
    1.74 +   TODO.WN120517: one starting point for redesign of pos' *)
    1.75 +val (f_pred, f_succ) = (get_pred_formula (pt, pos_pred), get_pred_formula (pt, pos));
    1.76 +	
    1.77 +term2str f_pred = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))";
    1.78 +term2str f_succ = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)";
    1.79 +
    1.80 +			f_succ = f_in; (* = false*)
    1.81 +cas_input f_in; (* = NONE*)
    1.82 +val msg_calcstate' = compare_step ([], [], (pt, pos_pred)) f_in
    1.83 +val ("no derivation found", calcstate') = msg_calcstate';
    1.84 +			                 val pp = par_pblobj pt p
    1.85 +			                 val {errpats, nrls, scr = Script prog, ...} = get_met (get_obj g_metID pt pp)
    1.86 +			                 val ScrState (env, _, _, _, _, _) = get_istate pt pos;
    1.87 +                 case check_error_patterns (f_pred, f_in) (prog, env) (errpats, nrls) of
    1.88 +			                   SOME errpatID => ("error pattern #" ^ errpatID ^ "#", calcstate')
    1.89 +			                 | NONE => msg_calcstate';
    1.90 +
    1.91 +"~~~~~ from inform return val:"; val () = ();
    1.92 +case check_error_patterns (f_pred, f_in) (prog, env) (errpats, nrls) of
    1.93 +			  SOME errpatID => ()
    1.94 +			| NONE => error "check_error_patterns broken";
    1.95 +
    1.96 +"--- final check:";
    1.97 +case inform cs' (encode ifo) of
    1.98 +  ("error pattern #chain-rule-diff-both#", calcstate') => ()
    1.99 +| _ => error "inform with (positive) check_error_patterns broken"
   1.100 +