1.1 --- a/src/Tools/isac/Interpret/ctree.sml Thu May 17 12:43:04 2012 +0200
1.2 +++ b/src/Tools/isac/Interpret/ctree.sml Thu May 17 16:44:13 2012 +0200
1.3 @@ -797,9 +797,9 @@
1.4 in (drop_last pos) @ [(nth len pos)+1] end;
1.5 fun lev_onFrm ((p,_):pos') = (lev_on p,Frm):pos'
1.6 | lev_onFrm p = raise PTREE ("*** lev_onFrm: pos'="^(pos'2str p));
1.7 -(*040216: for inform --> embed_deriv: remains on same level*)
1.8 -fun lev_back (([],_):pos') = raise PTREE "lev_on_back: called by ([],_)"
1.9 - | lev_back (p,_) =
1.10 +(*040216: for inform --> embed_deriv: remains on same level TODO.WN120517 compare lev_pred*)
1.11 +fun lev_back' (([],_):pos') = raise PTREE "lev_back': called by ([],_)"
1.12 + | lev_back' (p,_) =
1.13 if last_elem p <= 1 then (p, Frm):pos'
1.14 else ((drop_last p) @ [(nth (length p) p) - 1], Res);
1.15 (*.increase pos by n within a level.*)
1.16 @@ -807,8 +807,6 @@
1.17 | pos_plus n ((p,Frm):pos') = pos_plus (n-1) (p, Res)
1.18 | pos_plus n ((p, _):pos') = pos_plus (n-1) (lev_on p, Res);
1.19
1.20 -
1.21 -
1.22 fun lev_pred ([]:pos) = raise PTREE "lev_pred []"
1.23 | lev_pred (pos:pos) =
1.24 let val len = length pos
1.25 @@ -1627,7 +1625,7 @@
1.26 then (p, Pbl) else (par_pblobj pt p, Pbl);
1.27
1.28 (*.determine the previous pos' on the same level.*)
1.29 -(*WN0502 made for interSteps; _only_ works for branch TransitiveB*)
1.30 +(*WN0502 made for interSteps; _only_ works for branch TransitiveB WN120517 compare lev_back*)
1.31 fun lev_pred' pt (pos:pos' as ([],Res)) = ([],Pbl):pos'
1.32 | lev_pred' pt (pos:pos' as (p, Res)) =
1.33 let val (p', last) = split_last p
1.34 @@ -1638,6 +1636,7 @@
1.35 else if (is_pblobj o (get_obj I pt)) p then (p,Pbl) else (p, Frm)
1.36 end;
1.37
1.38 +
1.39 (*.determine the next pos' on the same level.*)
1.40 fun lev_on' pt (([],Pbl):pos') = ([],Res):pos'
1.41 | lev_on' pt (p, Res) =
2.1 --- a/src/Tools/isac/Interpret/inform.sml Thu May 17 12:43:04 2012 +0200
2.2 +++ b/src/Tools/isac/Interpret/inform.sml Thu May 17 16:44:13 2012 +0200
2.3 @@ -659,25 +659,25 @@
2.4 compare iform with calc-tree.form at pos by equ_nrls and all subsequent pos;
2.5 collect all the tacs applied by the way;
2.6 if "no derivation found" then check_error_patterns.
2.7 - ALTERNATIVE to check_error_patterns within compare_step seems too expensive.*)
2.8 + ALTERNATIVE: check_error_patterns _within_ compare_step seems too expensive.*)
2.9 fun inform (cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate') istr =
2.10 case parse (assoc_thy "Isac") istr of
2.11 - SOME ifo =>
2.12 + SOME f_in =>
2.13 let
2.14 - val ifo = term_of ifo
2.15 - val fo =
2.16 + val f_in = term_of f_in
2.17 + val f_succ = (* the formula from "step pos cs" in appendFormula*)
2.18 case p_ of
2.19 Frm => get_obj g_form pt p
2.20 | Res => (fst o (get_obj g_result pt)) p
2.21 | _ => #3 (get_obj g_origin pt p)
2.22 in
2.23 - if fo = ifo
2.24 + if f_succ = f_in
2.25 then ("same-formula", cs) (* ctree not cut with replaceFormula *)
2.26 else
2.27 - case cas_input ifo of
2.28 + case cas_input f_in of
2.29 SOME (pt, _) => ("ok",([], [], (pt, (p, Met))))
2.30 | NONE =>
2.31 - let val msg_calcstate' = compare_step ([], [], (pt, lev_back pos)) ifo
2.32 + let val msg_calcstate' = compare_step ([], [], (pt, lev_back' pos)) f_in
2.33 (*last step re-calc in compare_step TODO before WN09*)
2.34 in
2.35 case msg_calcstate' of
2.36 @@ -685,9 +685,10 @@
2.37 (*GOON
2.38 let
2.39 val pp = par_pblobj pt p
2.40 - val {errpats, nrls, ...} = get_met (get_obj g_metID pt pp)
2.41 + val {errpats, nrls, scr = Script prog, ...} = get_met (get_obj g_metID pt pp)
2.42 + val ScrState (env, _, _, _, _, _) = get_istate pt pos
2.43 in
2.44 - case check_error_patterns (fo, ifo) ?subst? errpats nrls of
2.45 + case check_error_patterns (f_succ, f_in) (prog, env) (errpats, nrls) of
2.46 SOME errpatID => ("error pattern #" ^ errpatID ^ "#", calcstate')
2.47 | NONE => msg_calcstate'
2.48 end
3.1 --- a/src/Tools/isac/Knowledge/Diff.thy Thu May 17 12:43:04 2012 +0200
3.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Thu May 17 16:44:13 2012 +0200
3.3 @@ -287,7 +287,14 @@
3.4 ("#Find" ,["derivative f_f'"])
3.5 ],
3.6 {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = e_rls,
3.7 - prls=e_rls, crls = Atools_erls, errpats = [], nrls = norm_diff},
3.8 + prls=e_rls, crls = Atools_erls, errpats = [("chain-rule-diff-both",
3.9 + [parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)",
3.10 + parse_patt @{theory} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)",
3.11 + parse_patt @{theory} "d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1)",
3.12 + parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u",
3.13 + parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"],
3.14 + [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain},
3.15 + @{thm diff_ln_chain}, @{thm diff_exp_chain}])], nrls = norm_diff},
3.16 "Script DiffScr (f_f::real) (v_v::real) = " ^
3.17 " (let f_f' = Take (d_d v_v f_f) " ^
3.18 " in (((Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@ " ^
4.1 --- a/test/Tools/isac/Test_Some.thy Thu May 17 12:43:04 2012 +0200
4.2 +++ b/test/Tools/isac/Test_Some.thy Thu May 17 16:44:13 2012 +0200
4.3 @@ -11,37 +11,73 @@
4.4 ML {*
4.5 *}
4.6 ML {* (*==================*)
4.7 -fun is_bdv_subst (Const ("List.list.Cons", _) $
4.8 - (Const ("Product_Type.Pair", _) $ Free (str, _) $ _) $ _) = is_bdv str
4.9 - | is_bdv_subst _ = false;
4.10 +"--------- build fun check_error_patterns ------------------------";
4.11 +val (fo, ifo) =
4.12 + (str2term "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)",
4.13 + str2term "d_d x (x ^^^ 2) + cos (4 * x ^^^ 3)");
4.14 +val {errpats, nrls = rls, scr = Script prog, ...} = get_met ["diff", "differentiate_on_R"]
4.15 +val env = [(str2term "v_v", str2term "x")];
4.16 +val errpats =
4.17 + [e_errpat, (*generalised for testing*)
4.18 + ("chain-rule-diff-both",
4.19 + [parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)",
4.20 + parse_patt @{theory} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)",
4.21 + parse_patt @{theory} "d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1)",
4.22 + parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u",
4.23 + parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"],
4.24 + [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain},
4.25 + @{thm diff_ln_chain}, @{thm diff_exp_chain}])]: errpat list;
4.26 *}
4.27 -ML {* (*==================*)
4.28 -"-------- build fun get_bdv_subst --------------------------------";
4.29 -(* get a substitution for "bdv*" from the current program and environment*)
4.30 -fun get_bdv_subst prog env =
4.31 +ML {*
4.32 +fun check_error_patterns (fo, ifo) (prog, env) (errpats, nrls) =
4.33 let
4.34 - fun scan (Const _) = NONE
4.35 - | scan (Free _) = NONE
4.36 - | scan (Var _) = NONE
4.37 - | scan (Bound _) = NONE
4.38 - | scan (t as Const ("List.list.Cons", _) $
4.39 - (Const ("Product_Type.Pair", _) $ Free (str, _) $ _) $ _) =
4.40 - if is_bdv_subst t then SOME t else NONE
4.41 - | scan (Abs (_, _, body)) = scan body
4.42 - | scan (t1 $ t2) =
4.43 - case scan t1 of
4.44 - NONE => scan t2
4.45 - | SOME subst => SOME subst
4.46 - in
4.47 - case scan prog of
4.48 - NONE => []: subst
4.49 - | SOME subs =>
4.50 - (subs |> subst_atomic env |> isalist2list |> map isapair2pair)
4.51 - (*"[(bdv,v_v)]": term
4.52 - |> "[(bdv,x)]": term |> ["(bdv,x)"]: term list
4.53 - |> [("bdv","x")]: (term * term) list*)
4.54 - end;
4.55 -
4.56 + fun xxx err = 111
4.57 + in 222 end;
4.58 +*}
4.59 +ML {*
4.60 +fun scan (_, [], _) = NONE
4.61 + | scan (errpatID, errpat :: errpats, _) =
4.62 + (writeln (term2str errpat);
4.63 + case check_err_patt (fo, ifo) (env: subst) (errpatID, errpat) rls of
4.64 + NONE => scan (errpatID, errpats, [])
4.65 + | SOME errpatID => SOME errpatID
4.66 + )
4.67 +fun scans [] = NONE
4.68 + | scans (group :: groups) =
4.69 + case scan group of
4.70 + NONE => scans groups
4.71 + | SOME errpatID => SOME errpatID
4.72 +*}
4.73 +ML {*
4.74 +term2str fo;
4.75 +*}
4.76 +ML {*
4.77 +*}
4.78 +ML {*
4.79 +*}
4.80 +ML {*
4.81 +scans errpats = NONE;
4.82 +*}
4.83 +ML {*
4.84 +*}
4.85 +ML {*
4.86 +*}
4.87 +ML {*
4.88 +*}
4.89 +ML {*
4.90 +*}
4.91 +text {*
4.92 +fun scans [] = NONE
4.93 + | scans ((errpatID, errpat :: errpats, xxx) :: eps) =
4.94 + case check_err_patt (fo, ifo) subst (errpatID, errpat) nrls of
4.95 + SOME errpatID => SOME errpatID
4.96 + | NONE =>
4.97 +*}
4.98 +ML {*
4.99 +*}
4.100 +ML {*
4.101 +*}
4.102 +ML {*
4.103 *}
4.104 ML {*
4.105 *}
4.106 @@ -52,23 +88,7 @@
4.107 ML {*
4.108 *}
4.109 ML {* (*==================*)
4.110 -val errpats = [e_errpat]: errpat list;
4.111 -val errpats =
4.112 -[("chain-rule-diff-both",
4.113 - [parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)",
4.114 - parse_patt @{theory} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)",
4.115 - parse_patt @{theory} "d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1)",
4.116 - parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u",
4.117 - parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"],
4.118 - [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain},
4.119 - @{thm diff_ln_chain}, @{thm diff_exp_chain}])]: errpat list;
4.120 -*}
4.121 -ML {*
4.122 -*}
4.123 -ML {*
4.124 -*}
4.125 -ML {* (*==================*)
4.126 -"--------- build fun check_error_patterns ------------------------";
4.127 +"--------- embed fun check_error_patterns ------------------------";
4.128 states:=[];
4.129 CalcTree
4.130 [(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
4.131 @@ -92,24 +112,34 @@
4.132 (*show_pt pt;
4.133 [(([], Frm), Diff (x ^^^ 2 + sin (x ^^^ 4), x)),
4.134 (([1], Frm), d_d x (x ^^^ 2 + sin (x ^^^ 4))),
4.135 - (([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))),
4.136 + (([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))), <<=== input follos: "...+ cos(4.x^3)"
4.137 (([2], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4))] *)
4.138
4.139 "~~~~~ fun inform, args:"; val ((cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate'), istr) =
4.140 (cs', (encode ifo));
4.141 -val SOME ifo = parse (assoc_thy "Isac") istr
4.142 -val ifo = term_of ifo
4.143 -val fo =
4.144 - case p_ of
4.145 - Frm => get_obj g_form pt p
4.146 - | Res => (fst o (get_obj g_result pt)) p
4.147 - | _ => #3 (get_obj g_origin pt p);
4.148 -(*term2str fo = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)"*)
4.149 -fo = ifo; (* = false*)
4.150 -cas_input ifo; (* = NONE*)
4.151 -val msg_calcstate' = compare_step ([], [], (pt, lev_back pos)) ifo
4.152 *}
4.153 ML {* (*###################### new code ######################*)
4.154 +val SOME f_in = parse (assoc_thy "Isac") istr
4.155 +val f_in = term_of f_in
4.156 +(* f_pred ---"step pos cs"---> f_succ in appendFormula
4.157 + TODO.WN120517: one starting point for redesign of pos' *)
4.158 +val (f_pred, f_succ) =
4.159 + case p_ of
4.160 + Frm => (e_term (*TODO.WN120517*), get_obj g_form pt p)
4.161 + | Res => ((get_obj g_form pt) p, (fst o (get_obj g_result pt)) p)
4.162 + | _ => (#3 (get_obj g_origin pt p) (*TODO.WN120517*), #3 (get_obj g_origin pt p))
4.163 + *}
4.164 +ML {*
4.165 +lev_pred' pt pos*}
4.166 +ML {*
4.167 +term2str f_succ = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)";
4.168 +fo = f_in; (* = false*)
4.169 +*}
4.170 +ML {*
4.171 +cas_input f_in; (* = NONE*)
4.172 +val msg_calcstate' = compare_step ([], [], (pt, lev_back' pos)) f_in
4.173 +*}
4.174 +ML {*
4.175 val pp = par_pblobj pt p
4.176 *}
4.177 ML {*
4.178 @@ -121,8 +151,10 @@
4.179 ML {*
4.180 *}
4.181 ML {*
4.182 -val [a,b,c] = env;
4.183 -(str2term "v_v", str2term "x") = b
4.184 +*}
4.185 +ML {*
4.186 +*}
4.187 +ML {*
4.188 *}
4.189 ML {*
4.190 *}
4.191 @@ -141,8 +173,8 @@
4.192
4.193 *}
4.194 text {*
4.195 -compare_step ([], [], (pt, lev_back pos)) ifo; (*("no derivation found", ([(...*)
4.196 -inform cs' (encode ifo);(*("no derivation found", ([(...*)
4.197 +compare_step ([], [], (pt, lev_back pos)) f_in; (*("no derivation found", ([(...*)
4.198 +inform cs' (encode f_in);(*("no derivation found", ([(...*)
4.199 step pos cs; (*("ok", ([(..., ...*)
4.200 appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)";
4.201 (*<CALCMESSAGE> no derivation found </CALCMESSAGE> --> error pattern #chain-rule-diff-both#*)