1.1 --- a/src/Tools/isac/Interpret/ctree.sml Thu May 17 16:44:13 2012 +0200
1.2 +++ b/src/Tools/isac/Interpret/ctree.sml Thu May 17 19:09:48 2012 +0200
1.3 @@ -921,7 +921,6 @@
1.4 | get_nd (Nd (_,nds)) (pos as p::(ps:pos)) = (get_nd (nth p nds) ps)
1.5 handle _ => raise PTREE ("get_nd: not existent pos = "^(ints2str' pos));
1.6
1.7 -
1.8 (* for use by get_obj *)
1.9 fun g_cell (PblObj {cell = c,...}) = NONE
1.10 | g_cell (PrfObj {cell = c,...}) = c;(*WN0607 hack for quick introduction of lrd + rewrite-at (thms, calcs)*)
1.11 @@ -968,6 +967,13 @@
1.12 fun gpt_cell (Nd (PblObj {cell = c,...},_)) = NONE
1.13 | gpt_cell (Nd (PrfObj {cell = c,...},_)) = c;
1.14
1.15 +(* get the formula preceeding the current position in a calculation *)
1.16 +fun get_pred_formula (pt, pos as (p, p_)) =
1.17 + case p_ of
1.18 + Frm => get_obj g_form pt p
1.19 + | Res => (fst o (get_obj g_result pt)) p
1.20 + | _ => #3 (get_obj g_origin pt p);
1.21 +
1.22 (*in CalcTree/Subproblem an 'just_created_' model is created;
1.23 this is filled to 'untouched' by Model/Refine_Problem*)
1.24 fun just_created_ (PblObj {meth, probl, spec, ...}) =
2.1 --- a/src/Tools/isac/Interpret/inform.sml Thu May 17 16:44:13 2012 +0200
2.2 +++ b/src/Tools/isac/Interpret/inform.sml Thu May 17 19:09:48 2012 +0200
2.3 @@ -631,7 +631,7 @@
2.4 in compare_step (tacis, c @ c' @ c'', ptp) ifo end
2.5 end;
2.6
2.7 -(* check if (agreed result, input formula) matches an error pattern modulo simplifier rls*)
2.8 +(* check if (agreed result, input formula) matches the error pattern "pat" modulo simplifier rls *)
2.9 fun check_err_patt (res, inf) (subst: subst) (errpatID: errpatID, pat) rls =
2.10 let
2.11 val (res', _, _, rewritten) =
2.12 @@ -651,6 +651,23 @@
2.13 else NONE
2.14 end;
2.15
2.16 +(* check if (agreed result, input formula) matches SOME error pattern modulo simplifier rls;
2.17 + (prog, env) for retrieval of casual substitution for bdv in the pattern. *)
2.18 +fun check_error_patterns (res, inf) (prog, env) (errpats, rls) =
2.19 + let
2.20 + val subst = get_bdv_subst prog env
2.21 + fun scan (_, [], _) = NONE
2.22 + | scan (errpatID, errpat :: errpats, _) =
2.23 + case check_err_patt (res, inf) (subst: subst) (errpatID, errpat) rls of
2.24 + NONE => scan (errpatID, errpats, [])
2.25 + | SOME errpatID => SOME errpatID
2.26 + fun scans [] = NONE
2.27 + | scans (group :: groups) =
2.28 + case scan group of
2.29 + NONE => scans groups
2.30 + | SOME errpatID => SOME errpatID
2.31 + in scans errpats end;
2.32 +
2.33 (*.handle a user-input formula, which may be a CAS-command, too.
2.34 CAS-command:
2.35 create a calchead, and do 1 step
2.36 @@ -665,11 +682,7 @@
2.37 SOME f_in =>
2.38 let
2.39 val f_in = term_of f_in
2.40 - val f_succ = (* the formula from "step pos cs" in appendFormula*)
2.41 - case p_ of
2.42 - Frm => get_obj g_form pt p
2.43 - | Res => (fst o (get_obj g_result pt)) p
2.44 - | _ => #3 (get_obj g_origin pt p)
2.45 + val f_succ = get_pred_formula (pt, pos);
2.46 in
2.47 if f_succ = f_in
2.48 then ("same-formula", cs) (* ctree not cut with replaceFormula *)
2.49 @@ -677,23 +690,24 @@
2.50 case cas_input f_in of
2.51 SOME (pt, _) => ("ok",([], [], (pt, (p, Met))))
2.52 | NONE =>
2.53 - let val msg_calcstate' = compare_step ([], [], (pt, lev_back' pos)) f_in
2.54 + let
2.55 + val pos_pred = lev_back' pos
2.56 + (* f_pred ---"step pos cs"---> f_succ in appendFormula *)
2.57 + val f_pred = get_pred_formula (pt, pos_pred)
2.58 + val msg_calcstate' = compare_step ([], [], (pt, pos_pred)) f_in
2.59 (*last step re-calc in compare_step TODO before WN09*)
2.60 in
2.61 case msg_calcstate' of
2.62 ("no derivation found", calcstate') =>
2.63 -(*GOON
2.64 let
2.65 val pp = par_pblobj pt p
2.66 val {errpats, nrls, scr = Script prog, ...} = get_met (get_obj g_metID pt pp)
2.67 val ScrState (env, _, _, _, _, _) = get_istate pt pos
2.68 in
2.69 - case check_error_patterns (f_succ, f_in) (prog, env) (errpats, nrls) of
2.70 + case check_error_patterns (f_pred, f_in) (prog, env) (errpats, nrls) of
2.71 SOME errpatID => ("error pattern #" ^ errpatID ^ "#", calcstate')
2.72 | NONE => msg_calcstate'
2.73 end
2.74 -GOON*)
2.75 - msg_calcstate'
2.76 | _ => msg_calcstate'
2.77 end
2.78 end
3.1 --- a/test/Tools/isac/Interpret/inform.sml Thu May 17 16:44:13 2012 +0200
3.2 +++ b/test/Tools/isac/Interpret/inform.sml Thu May 17 19:09:48 2012 +0200
3.3 @@ -33,6 +33,8 @@
3.4 "--------- init_form, start with <NEW> (CAS input) ---------------";
3.5 "--------- build fun check_err_patt ------------------------------";
3.6 "--------- build fun check_err_patt ?bdv -------------------------";
3.7 +"--------- build fun check_error_patterns ------------------------";
3.8 +"--------- embed fun check_error_patterns ------------------------";
3.9 "-----------------------------------------------------------------";
3.10 "-----------------------------------------------------------------";
3.11 "-----------------------------------------------------------------";
3.12 @@ -869,4 +871,88 @@
3.13 if check_err_patt (res, inf) (subst: subst) ("errpatID": errpatID, pat) rls = SOME "errpatID"
3.14 then () else error "error patt example1 changed";
3.15
3.16 +"--------- build fun check_error_patterns ------------------------";
3.17 +"--------- build fun check_error_patterns ------------------------";
3.18 +"--------- build fun check_error_patterns ------------------------";
3.19 +val (res, inf) =
3.20 + (str2term "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))",
3.21 + str2term "d_d x (x ^^^ 2) + cos (4 * x ^^^ 3)");
3.22 +val {errpats, nrls = rls, scr = Script prog, ...} = get_met ["diff", "differentiate_on_R"]
3.23
3.24 +val env = [(str2term "v_v", str2term "x")];
3.25 +val errpats =
3.26 + [e_errpat, (*generalised for testing*)
3.27 + ("chain-rule-diff-both",
3.28 + [parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)",
3.29 + parse_patt @{theory} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)",
3.30 + parse_patt @{theory} "d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1)",
3.31 + parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u",
3.32 + parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"],
3.33 + [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain},
3.34 + @{thm diff_ln_chain}, @{thm diff_exp_chain}])]: errpat list;
3.35 +
3.36 +case check_error_patterns (res, inf) (prog, env) (errpats, rls) of SOME _ => ()
3.37 +| NONE => error "check_error_patterns broken";
3.38 +
3.39 +
3.40 +"--------- embed fun check_error_patterns ------------------------";
3.41 +"--------- embed fun check_error_patterns ------------------------";
3.42 +"--------- embed fun check_error_patterns ------------------------";
3.43 +states:=[];
3.44 +CalcTree
3.45 +[(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
3.46 + ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
3.47 +Iterator 1;
3.48 +moveActiveRoot 1;
3.49 +autoCalculate 1 CompleteCalcHead;
3.50 +autoCalculate 1 (Step 1);
3.51 +autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
3.52 +(*autoCalculate 1 (Step 1);([2], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)*)
3.53 +
3.54 +"~~~~~ fun appendFormula, args:"; val (cI, (ifo:cterm')) = (1, "d_d x (x ^ 2) + cos (4 * x ^ 3)");
3.55 +val cs = get_calc cI
3.56 +val pos as (_,p_) = get_pos cI 1; (*pos = ([1], Res)*)
3.57 +val cs' =
3.58 + case step pos cs of
3.59 + ("ok", cs') => cs';
3.60 +
3.61 +val (_, _, (pt, ([2], Res))) = cs';
3.62 +(*show_pt pt;
3.63 + [(([], Frm), Diff (x ^^^ 2 + sin (x ^^^ 4), x)),
3.64 + (([1], Frm), d_d x (x ^^^ 2 + sin (x ^^^ 4))),
3.65 + (([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))), <<=== input follos: "...+ cos(4.x^3)"
3.66 + (([2], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4))] *)
3.67 +
3.68 +"~~~~~ fun inform, args:"; val ((cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate'), istr) =
3.69 + (cs', (encode ifo));
3.70 +val SOME f_in = parse (assoc_thy "Isac") istr
3.71 +val f_in = term_of f_in
3.72 +val pos_pred = lev_back' pos
3.73 + (* f_pred ---"step pos cs"---> f_succ in appendFormula
3.74 + TODO.WN120517: one starting point for redesign of pos' *)
3.75 +val (f_pred, f_succ) = (get_pred_formula (pt, pos_pred), get_pred_formula (pt, pos));
3.76 +
3.77 +term2str f_pred = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))";
3.78 +term2str f_succ = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)";
3.79 +
3.80 + f_succ = f_in; (* = false*)
3.81 +cas_input f_in; (* = NONE*)
3.82 +val msg_calcstate' = compare_step ([], [], (pt, pos_pred)) f_in
3.83 +val ("no derivation found", calcstate') = msg_calcstate';
3.84 + val pp = par_pblobj pt p
3.85 + val {errpats, nrls, scr = Script prog, ...} = get_met (get_obj g_metID pt pp)
3.86 + val ScrState (env, _, _, _, _, _) = get_istate pt pos;
3.87 + case check_error_patterns (f_pred, f_in) (prog, env) (errpats, nrls) of
3.88 + SOME errpatID => ("error pattern #" ^ errpatID ^ "#", calcstate')
3.89 + | NONE => msg_calcstate';
3.90 +
3.91 +"~~~~~ from inform return val:"; val () = ();
3.92 +case check_error_patterns (f_pred, f_in) (prog, env) (errpats, nrls) of
3.93 + SOME errpatID => ()
3.94 + | NONE => error "check_error_patterns broken";
3.95 +
3.96 +"--- final check:";
3.97 +case inform cs' (encode ifo) of
3.98 + ("error pattern #chain-rule-diff-both#", calcstate') => ()
3.99 +| _ => error "inform with (positive) check_error_patterns broken"
3.100 +
4.1 --- a/test/Tools/isac/Test_Some.thy Thu May 17 16:44:13 2012 +0200
4.2 +++ b/test/Tools/isac/Test_Some.thy Thu May 17 19:09:48 2012 +0200
4.3 @@ -1,7 +1,7 @@
4.4
4.5 theory Test_Some imports Isac begin
4.6
4.7 -use"../../../test/Tools/isac/ProgLang/termC.sml"
4.8 +use"../../../test/Tools/isac/Interpret/inform.sml"
4.9
4.10 ML {*
4.11 val thy = @{theory "Isac"};
4.12 @@ -11,186 +11,6 @@
4.13 ML {*
4.14 *}
4.15 ML {* (*==================*)
4.16 -"--------- build fun check_error_patterns ------------------------";
4.17 -val (fo, ifo) =
4.18 - (str2term "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)",
4.19 - str2term "d_d x (x ^^^ 2) + cos (4 * x ^^^ 3)");
4.20 -val {errpats, nrls = rls, scr = Script prog, ...} = get_met ["diff", "differentiate_on_R"]
4.21 -val env = [(str2term "v_v", str2term "x")];
4.22 -val errpats =
4.23 - [e_errpat, (*generalised for testing*)
4.24 - ("chain-rule-diff-both",
4.25 - [parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)",
4.26 - parse_patt @{theory} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)",
4.27 - parse_patt @{theory} "d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1)",
4.28 - parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u",
4.29 - parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"],
4.30 - [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain},
4.31 - @{thm diff_ln_chain}, @{thm diff_exp_chain}])]: errpat list;
4.32 -*}
4.33 -ML {*
4.34 -fun check_error_patterns (fo, ifo) (prog, env) (errpats, nrls) =
4.35 - let
4.36 - fun xxx err = 111
4.37 - in 222 end;
4.38 -*}
4.39 -ML {*
4.40 -fun scan (_, [], _) = NONE
4.41 - | scan (errpatID, errpat :: errpats, _) =
4.42 - (writeln (term2str errpat);
4.43 - case check_err_patt (fo, ifo) (env: subst) (errpatID, errpat) rls of
4.44 - NONE => scan (errpatID, errpats, [])
4.45 - | SOME errpatID => SOME errpatID
4.46 - )
4.47 -fun scans [] = NONE
4.48 - | scans (group :: groups) =
4.49 - case scan group of
4.50 - NONE => scans groups
4.51 - | SOME errpatID => SOME errpatID
4.52 -*}
4.53 -ML {*
4.54 -term2str fo;
4.55 -*}
4.56 -ML {*
4.57 -*}
4.58 -ML {*
4.59 -*}
4.60 -ML {*
4.61 -scans errpats = NONE;
4.62 -*}
4.63 -ML {*
4.64 -*}
4.65 -ML {*
4.66 -*}
4.67 -ML {*
4.68 -*}
4.69 -ML {*
4.70 -*}
4.71 -text {*
4.72 -fun scans [] = NONE
4.73 - | scans ((errpatID, errpat :: errpats, xxx) :: eps) =
4.74 - case check_err_patt (fo, ifo) subst (errpatID, errpat) nrls of
4.75 - SOME errpatID => SOME errpatID
4.76 - | NONE =>
4.77 -*}
4.78 -ML {*
4.79 -*}
4.80 -ML {*
4.81 -*}
4.82 -ML {*
4.83 -*}
4.84 -ML {*
4.85 -*}
4.86 -ML {*
4.87 -*}
4.88 -ML {*
4.89 -*}
4.90 -ML {*
4.91 -*}
4.92 -ML {* (*==================*)
4.93 -"--------- embed fun check_error_patterns ------------------------";
4.94 -states:=[];
4.95 -CalcTree
4.96 -[(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
4.97 - ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
4.98 -Iterator 1;
4.99 -moveActiveRoot 1;
4.100 -autoCalculate 1 CompleteCalcHead;
4.101 -autoCalculate 1 (Step 1);
4.102 -autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
4.103 -(*autoCalculate 1 (Step 1);([2], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)*)
4.104 -*}
4.105 -ML {*
4.106 -"~~~~~ fun appendFormula, args:"; val (cI, (ifo:cterm')) = (1, "d_d x (x ^ 2) + cos (4 * x ^ 3)");
4.107 -val cs = get_calc cI
4.108 -val pos as (_,p_) = get_pos cI 1; (*pos = ([1], Res)*)
4.109 -val cs' =
4.110 - case step pos cs of
4.111 - ("ok", cs') => cs';
4.112 -
4.113 -val (_, _, (pt, ([2], Res))) = cs';
4.114 -(*show_pt pt;
4.115 - [(([], Frm), Diff (x ^^^ 2 + sin (x ^^^ 4), x)),
4.116 - (([1], Frm), d_d x (x ^^^ 2 + sin (x ^^^ 4))),
4.117 - (([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))), <<=== input follos: "...+ cos(4.x^3)"
4.118 - (([2], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4))] *)
4.119 -
4.120 -"~~~~~ fun inform, args:"; val ((cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate'), istr) =
4.121 - (cs', (encode ifo));
4.122 -*}
4.123 -ML {* (*###################### new code ######################*)
4.124 -val SOME f_in = parse (assoc_thy "Isac") istr
4.125 -val f_in = term_of f_in
4.126 -(* f_pred ---"step pos cs"---> f_succ in appendFormula
4.127 - TODO.WN120517: one starting point for redesign of pos' *)
4.128 -val (f_pred, f_succ) =
4.129 - case p_ of
4.130 - Frm => (e_term (*TODO.WN120517*), get_obj g_form pt p)
4.131 - | Res => ((get_obj g_form pt) p, (fst o (get_obj g_result pt)) p)
4.132 - | _ => (#3 (get_obj g_origin pt p) (*TODO.WN120517*), #3 (get_obj g_origin pt p))
4.133 - *}
4.134 -ML {*
4.135 -lev_pred' pt pos*}
4.136 -ML {*
4.137 -term2str f_succ = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)";
4.138 -fo = f_in; (* = false*)
4.139 -*}
4.140 -ML {*
4.141 -cas_input f_in; (* = NONE*)
4.142 -val msg_calcstate' = compare_step ([], [], (pt, lev_back' pos)) f_in
4.143 -*}
4.144 -ML {*
4.145 -val pp = par_pblobj pt p
4.146 -*}
4.147 -ML {*
4.148 -val {errpats, nrls, ...} = get_met (get_obj g_metID pt pp);
4.149 -*}
4.150 -ML {*
4.151 -val ScrState (env, loc_, topt, t, safe, bool) = get_istate pt pos
4.152 -*}
4.153 -ML {*
4.154 -*}
4.155 -ML {*
4.156 -*}
4.157 -ML {*
4.158 -*}
4.159 -ML {*
4.160 -*}
4.161 -ML {*
4.162 -*}
4.163 -ML {* (*###################### new code ######################*)
4.164 -*}
4.165 -ML {*
4.166 -*}
4.167 -ML {*
4.168 -*}
4.169 -ML {*
4.170 -compare_step;
4.171 -e_calcstate';
4.172 -writeln ("#####"^env2str env^"#####"); (*----- (v_v, x) -----*)
4.173 -*}
4.174 -ML {*
4.175 -
4.176 -*}
4.177 -text {*
4.178 -compare_step ([], [], (pt, lev_back pos)) f_in; (*("no derivation found", ([(...*)
4.179 -inform cs' (encode f_in);(*("no derivation found", ([(...*)
4.180 -step pos cs; (*("ok", ([(..., ...*)
4.181 -appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)";
4.182 - (*<CALCMESSAGE> no derivation found </CALCMESSAGE> --> error pattern #chain-rule-diff-both#*)
4.183 -*}
4.184 -ML {*
4.185 -*}
4.186 -ML {*
4.187 -*}
4.188 -ML {*
4.189 -val ((pt,p),_) = get_calc 1; show_pt pt;
4.190 -*}
4.191 -text {*
4.192 -val ((pt,p),_) = get_calc 1; show_pt pt;
4.193 -if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) =
4.194 - "2 * x + cos (3 * x ^^^ 4) * 12 * x ^^^ 3" then ()
4.195 -else error "check_error_pattern changed";
4.196 *}
4.197 ML {*
4.198 *}
4.199 @@ -199,10 +19,6 @@
4.200 ML {*
4.201 *}
4.202 ML {* (*==================*)
4.203 -*}
4.204 -ML {* (*==================*)
4.205 -*}
4.206 -ML {* (*==================*)
4.207 "~~~~~ fun , args:"; val () = ();
4.208 "~~~~~ to return val:"; val () = ();
4.209