1.1 --- a/src/Tools/isac/Frontend/interface.sml Tue May 22 07:00:53 2012 +0200
1.2 +++ b/src/Tools/isac/Frontend/interface.sml Tue May 22 13:40:06 2012 +0200
1.3 @@ -53,6 +53,7 @@
1.4 val setProblem : calcID -> pblID -> unit
1.5 val setTheory : calcID -> thyID -> unit
1.6 val FindFillpatterns : calcID -> errpatID -> unit
1.7 + val requestFillformula : calcID -> errpatID * fillpatID -> unit
1.8 (*------------ for tests*)
1.9 val encode: cterm' -> cterm'
1.10 val encode_fmz: fmz -> fmz
1.11 @@ -791,8 +792,35 @@
1.12 val ((pt, _), _) = get_calc cI
1.13 val pos = get_pos cI 1;
1.14 val fillpats = find_fillpatterns (pt, pos) errpatID
1.15 + val args = "fill patterns " ^ ((map (apsnd term2str) fillpats) |> map pair2str_ |> strs2str_)
1.16 (* the format for the message's arguments is waiting for generalisation of CalcMessage *)
1.17 - in calcMessage2xml cI ("fill patterns " ^ (fillpats |> map pair2str_ |> strs2str_)) end;
1.18 + in calcMessage2xml cI ("fill patterns " ^ args) end;
1.19 +
1.20 +(* given a fillpatID propose a fillform to the learner on the worksheet;
1.21 + the "ctree" is extended with fillpat and "ostate Inconsistent", the "istate" is NOT updated;
1.22 + returns CalcChanged.
1.23 + arg errpatID: required because there is no dialog-related state in the math-kernel.
1.24 +*)
1.25 +fun requestFillformula cI (errpatID, fillpatID) =
1.26 + let
1.27 + val ((pt, _), _) = get_calc cI
1.28 + val pos as (p, _) = get_pos cI 1
1.29 + val fillforms = find_fillpatterns (pt, pos) errpatID
1.30 + in
1.31 + case filter ((curry op = fillpatID) o (#1: (fillpatID * term -> fillpatID))) fillforms of
1.32 + (fillpatID, fillform) :: _ =>
1.33 + let
1.34 + val f_curr = get_curr_formula (pt, pos) (*already done in find_fillpatterns, too*)
1.35 + val (pos', _, _, pt) = generate_inconsistent 0
1.36 + (Rewrite' ("","",e_rls,true, (fillpatID, ""(*errpatthm known in find_fillpatterns*)),
1.37 + f_curr, (fillform, [])))
1.38 + (get_loc pt pos) (lev_on p, Und) pt
1.39 + in
1.40 + (upd_calc cI ((pt, pos'), []); (*upd_ipos cI 1 pos';*)
1.41 + autocalculateOK2xml cI pos pos' pos')
1.42 + end
1.43 + | _ => autocalculateERROR2xml cI "no fillpattern found"
1.44 + end;
1.45
1.46 (*------------------------------------------------------------------*)
1.47 end
2.1 --- a/src/Tools/isac/Interpret/calchead.sml Tue May 22 07:00:53 2012 +0200
2.2 +++ b/src/Tools/isac/Interpret/calchead.sml Tue May 22 13:40:06 2012 +0200
2.3 @@ -1945,38 +1945,35 @@
2.4 list
2.5 .*)
2.6 fun get_interval from to level pt =
2.7 -(* val (from,level) = (f,lev);
2.8 - val (from, to, level) = (([3, 2, 1], Res), ([],Res), 9999);
2.9 - *)
2.10 - let fun get_inter c (from:pos') (to:pos') lev pt =
2.11 -(* val (c, from, to, lev) = ([], from, to, level);
2.12 - ------for recursion.......
2.13 - val (c, from:pos', to:pos') = (c @ [(from, f)], move_dn [] pt from, to);
2.14 - *)
2.15 + let
2.16 + fun get_inter c (from:pos') (to:pos') lev pt =
2.17 if eq_pos' from to orelse from = ([],Res)
2.18 (*orelse ... avoids Exception- PTREE "end of calculation" raised,
2.19 if 'to' has values NOT generated by move_dn, see systest/me.sml
2.20 TODO.WN0501: introduce an order on pos' and check "from > to"..
2.21 ...there is an order in Java!
2.22 WN051224 the hack got worse with returning term instead ptform*)
2.23 - then let val (f,_,_) = pt_extract (pt, from)
2.24 - in case f of
2.25 - ModSpec (_,_,headline,_,_,_) => c @ [(from, headline)]
2.26 - | Form t => c @ [(from, t)]
2.27 - end
2.28 + then
2.29 + let val (f,_,_) = pt_extract (pt, from)
2.30 + in
2.31 + case f of
2.32 + ModSpec (_,_,headline,_,_,_) => c @ [(from, headline)]
2.33 + | Form t => c @ [(from, t)]
2.34 + end
2.35 else
2.36 - if lev < lev_of from
2.37 - then (get_inter c (move_dn [] pt from) to lev pt)
2.38 - handle (PTREE _(*from move_dn too far*)) => c
2.39 - else let val (f,_,_) = pt_extract (pt, from)
2.40 - val term = case f of
2.41 - ModSpec (_,_,headline,_,_,_)=> headline
2.42 - | Form t => t
2.43 - in (get_inter (c @ [(from, term)])
2.44 - (move_dn [] pt from) to lev pt)
2.45 - handle (PTREE _(*from move_dn too far*))
2.46 - => c @ [(from, term)] end
2.47 - in get_inter [] from to level pt end;
2.48 + if lev < lev_of from
2.49 + then (get_inter c (move_dn [] pt from) to lev pt)
2.50 + handle (PTREE _(*from move_dn too far*)) => c
2.51 + else
2.52 + let
2.53 + val (f,_,_) = pt_extract (pt, from)
2.54 + val term = case f of
2.55 + ModSpec (_,_,headline,_,_,_) => headline
2.56 + | Form t => t
2.57 + in (get_inter (c @ [(from, term)]) (move_dn [] pt from) to lev pt)
2.58 + handle (PTREE _(*from move_dn too far*)) => c @ [(from, term)]
2.59 + end
2.60 + in get_inter [] from to level pt end;
2.61
2.62 (*for tests*)
2.63 fun posform2str (pos:pos', form) =
3.1 --- a/src/Tools/isac/Interpret/generate.sml Tue May 22 07:00:53 2012 +0200
3.2 +++ b/src/Tools/isac/Interpret/generate.sml Tue May 22 13:40:06 2012 +0200
3.3 @@ -389,7 +389,7 @@
3.4 val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
3.5 (Rewrite thm') (f',asm) Complete
3.6 val pt = update_branch pt p TransitiveB
3.7 - in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt)end
3.8 + in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end
3.9
3.10 | generate1 thy (Rewrite_Asm' all) l p pt = generate1 thy (Rewrite' all) l p pt
3.11
3.12 @@ -470,6 +470,13 @@
3.13 | generate1 thy m' _ _ _ =
3.14 error ("generate1: not impl.for "^(tac_2str m'));
3.15
3.16 +fun generate_inconsistent _ (Rewrite' (_,_,_,_, thm', f, (f', asm))) (is, ctxt) (p,_) pt =
3.17 + let
3.18 + val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
3.19 + (Rewrite thm') (f', asm) Inconsistent
3.20 + val pt = update_branch pt p TransitiveB
3.21 + in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt)end
3.22 +
3.23 fun generate_hard thy m' (p,p_) pt =
3.24 let
3.25 val p =
4.1 --- a/src/Tools/isac/Interpret/inform.sml Tue May 22 07:00:53 2012 +0200
4.2 +++ b/src/Tools/isac/Interpret/inform.sml Tue May 22 13:40:06 2012 +0200
4.3 @@ -720,7 +720,7 @@
4.4 rew_sub (Isac()) 1 subst e_rew_ord e_rls false [] (Trueprop $ pat) form;
4.5 in (*the fillpat of the thm must be dedicated to errpatID*)
4.6 if errpatID = erpaID andalso rewritten
4.7 - then SOME (fillpatID, term2str (HOLogic.mk_eq (form, form'))) else NONE end;
4.8 + then SOME (fillpatID, HOLogic.mk_eq (form, form')) else NONE end;
4.9
4.10 fun get_fillpats subst form errpatID thm =
4.11 let
5.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy Tue May 22 07:00:53 2012 +0200
5.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy Tue May 22 13:40:06 2012 +0200
5.3 @@ -118,15 +118,15 @@
5.4 (*WN210512 DESIGN TODO: build thehier already in respective theories*)
5.5 val fillpats = [
5.6 ("fill-d_d-arg",
5.7 - parse_patt thy "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),
5.8 + parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),
5.9 ("fill-both-args",
5.10 - parse_patt thy "d_d ?bdv (sin _) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),
5.11 + parse_patt @{theory Diff} "d_d ?bdv (sin _) = cos _ * d_d ?bdv _", "chain-rule-diff-both"),
5.12 ("fill-d_d",
5.13 - parse_patt thy "d_d ?bdv (sin ?u) = cos ?u * _ ?bdv ?u", "chain-rule-diff-both"),
5.14 + parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * _ ?bdv ?u", "chain-rule-diff-both"),
5.15 ("fill-inner-deriv",
5.16 - parse_patt thy "d_d ?bdv (sin ?u) = cos ?u * _", "chain-rule-diff-both"),
5.17 + parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * _", "chain-rule-diff-both"),
5.18 ("fill-all",
5.19 - parse_patt thy "d_d ?bdv (sin ?u) = _", "chain-rule-diff-both")]: fillpat list;
5.20 + parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = _", "chain-rule-diff-both")]: fillpat list;
5.21 insert_fillpats @{theory Diff} "IsacKnowledge" ("diff_sin_chain", @{thm diff_sin_chain}) fillpats;
5.22 (* compare test/../thy-hierarchy.sml *)
5.23 *}
6.1 --- a/test/Tools/isac/Frontend/interface.sml Tue May 22 07:00:53 2012 +0200
6.2 +++ b/test/Tools/isac/Frontend/interface.sml Tue May 22 13:40:06 2012 +0200
6.3 @@ -48,6 +48,7 @@
6.4 "--------- replaceFormula {SOL:MAN:FOR:replace} other----";
6.5 "--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
6.6 "--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
6.7 +"--------- UC errpat, fillpat ---------------------------";
6.8 "--------------------------------------------------------";
6.9
6.10 "within struct ---------------------------------------------------";
7.1 --- a/test/Tools/isac/Interpret/inform.sml Tue May 22 07:00:53 2012 +0200
7.2 +++ b/test/Tools/isac/Interpret/inform.sml Tue May 22 13:40:06 2012 +0200
7.3 @@ -36,6 +36,7 @@
7.4 "--------- build fun check_error_patterns ------------------------";
7.5 "--------- embed fun check_error_patterns ------------------------";
7.6 "--------- embed fun find_fillpatterns ---------------------------";
7.7 +"--------- embed fun get_fillform --------------------------------";
7.8 "-----------------------------------------------------------------";
7.9 "-----------------------------------------------------------------";
7.10 "-----------------------------------------------------------------";
7.11 @@ -931,7 +932,7 @@
7.12 val pos_pred = lev_back' pos
7.13 (* f_pred ---"step pos cs"---> f_succ in appendFormula
7.14 TODO.WN120517: one starting point for redesign of pos' *)
7.15 -val (f_pred, f_succ) = (get_pred_formula (pt, pos_pred), get_pred_formula (pt, pos));
7.16 +val (f_pred, f_succ) = (get_curr_formula (pt, pos_pred), get_curr_formula (pt, pos));
7.17
7.18 term2str f_pred = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))";
7.19 term2str f_succ = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)";
7.20 @@ -971,13 +972,14 @@
7.21 autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
7.22 appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)";
7.23 (*<CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>*)
7.24 - (*TODO BACK TO <CALCMESSAGE> no derivation found </CALCMESSAGE>*)
7.25 + (*or
7.26 + <CALCMESSAGE> no derivation found </CALCMESSAGE>*)
7.27
7.28 "~~~~~ fun FindFillpatterns, args:"; val (cI, errpatID) = (1, "chain-rule-diff-both");
7.29 val ((pt, _), _) = get_calc cI
7.30 val pos = get_pos cI 1;
7.31 - "~~~~~ fun find_fillpatterns, args:"; val ((pt, pos as (p, _)), errpatID) = ((pt, pos), errpatID);
7.32 - val f_curr = get_pred_formula (pt, pos); (* = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"*)
7.33 +"~~~~~ fun find_fillpatterns, args:"; val ((pt, pos as (p, _)), errpatID) = ((pt, pos), errpatID);
7.34 + val f_curr = get_curr_formula (pt, pos); (* = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"*)
7.35 val pp = par_pblobj pt p
7.36 val {errpats, scr = Script prog, ...} = get_met (get_obj g_metID pt pp)
7.37 val ScrState (env, _, _, _, _, _) = get_istate pt pos
7.38 @@ -988,13 +990,13 @@
7.39 |> flat;
7.40
7.41 case map (get_fillpats subst f_curr errpatID) errpatthms |> flat of
7.42 - ("fill-d_d-arg",
7.43 - "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1")
7.44 - :: _ => ()
7.45 -| _ => error "find_fillpatterns changed"
7.46 + ("fill-d_d-arg", tm) :: _ => if term2str tm =
7.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"
7.48 + then () else error "find_fillpatterns changed 1a"
7.49 +| _ => error "find_fillpatterns changed 1b"
7.50
7.51 "~~~~~ fun get_fillpats, args:"; val (subst, form, errpatID, thm) =
7.52 - (subst, f_curr, errpatID, hd errpatthms);
7.53 + (subst, f_curr, errpatID, hd (*simulate beginning of "map"*) errpatthms);
7.54 val thmDeriv = Thm.get_name_hint thm
7.55 val (part, thyID) = thy_containing_thm thmDeriv
7.56 val theID = [part, thyID, "Theorems", thmID_of_derivation_name thmDeriv]
7.57 @@ -1002,8 +1004,104 @@
7.58 val some = map (get_fillform subst form errpatID) fillpats;
7.59
7.60 case some |> filter is_some |> map the of
7.61 - ("fill-d_d-arg",
7.62 - "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1")
7.63 - :: _ => ()
7.64 -| _ => error "get_fillpats changed"
7.65 + ("fill-d_d-arg", tm) :: _ => if term2str tm =
7.66 + "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1"
7.67 + then () else error "find_fillpatterns changed 2a"
7.68 +| _ => error "find_fillpatterns changed 2b"
7.69
7.70 +"~~~~~ fun get_fillform, args:"; val (subst, form, errpatID, ((fillpatID, pat, erpaID): fillpat)) =
7.71 + (subst, form, errpatID, hd (*simulate beginning of "map"*) fillpats);
7.72 + val (form', _, _, rewritten) =
7.73 + rew_sub (Isac()) 1 subst e_rew_ord e_rls false [] (Trueprop $ pat) form;
7.74 +
7.75 +if term2str form' = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1" then ()
7.76 +else error "find_fillpatterns changed 3";
7.77 +
7.78 +"~~~~~ to FindFillpatterns return val:"; val (fillpats) =
7.79 + (map (get_fillpats subst f_curr errpatID) errpatthms |> flat) (*only from "hd errpatthms"*);
7.80 +
7.81 +val msg = "fill patterns " ^ ((map (apsnd term2str) fillpats) |> map pair2str_ |> strs2str_);
7.82 +if msg =
7.83 + "fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" ^
7.84 + " =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1" ^
7.85 + "#fill-both-args#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" ^
7.86 + " =\nd_d x (x ^^^ 2) + cos ?_dummy_2 * d_d x ?_dummy_3" ^
7.87 + "#fill-d_d#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" ^
7.88 + " =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * ?_dummy_1 x (x ^^^ 4)" ^
7.89 + "#fill-inner-deriv#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" ^
7.90 + " =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * ?_dummy_1" ^
7.91 + "#fill-all#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) = d_d x (x ^^^ 2) + ?_dummy_1#"
7.92 +then () else error "find_fillpatterns changed 4";
7.93 +
7.94 +
7.95 +"--------- embed fun get_fillform --------------------------------";
7.96 +"--------- embed fun get_fillform --------------------------------";
7.97 +"--------- embed fun get_fillform --------------------------------";
7.98 +states := [];
7.99 +CalcTree
7.100 +[(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
7.101 + ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
7.102 +Iterator 1;
7.103 +moveActiveRoot 1;
7.104 +autoCalculate 1 CompleteCalcHead;
7.105 +autoCalculate 1 (Step 1);
7.106 +autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
7.107 +appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)";
7.108 +(* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),
7.109 + would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well.
7.110 + results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>
7.111 + instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)
7.112 +FindFillpatterns 1 "chain-rule-diff-both";
7.113 +(*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =
7.114 + d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *)
7.115 +
7.116 +"~~~~~ fun requestFillformula, args:"; val (cI, (errpatID, fillpatID)) =
7.117 + (1, ("chain-rule-diff-both", "fill-both-args"));
7.118 +val ((pt, _), _) = get_calc cI
7.119 +val pos = get_pos cI 1; (* = ([1], Res)*)
7.120 +
7.121 +"~~~~~ fun get_fillformula, args:"; val ((pt, pos as (p, _)), (errpatID, fillpatID)) =
7.122 + ((pt, pos), (errpatID, fillpatID));
7.123 +val fillforms = find_fillpatterns (pt, pos) errpatID
7.124 +val fillforms =
7.125 + filter ((curry op = fillpatID) o (#1: (fillpatID * term -> fillpatID))) fillforms;
7.126 +
7.127 +val [(fillpatID, fillform)] = fillforms;
7.128 +case (fillpatID, fillform) of
7.129 + ("fill-both-args", tm) => if term2str tm =
7.130 + "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos ?_dummy_2 * d_d x ?_dummy_3"
7.131 + then () else error "get_fillformula changed 1a"
7.132 +| _ => error "get_fillformula changed 1b";
7.133 +
7.134 + val f_curr = get_curr_formula (pt, pos); (*already done in find_fillpatterns, too*)
7.135 +term2str f_curr = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))";
7.136 +
7.137 +"~~~~~ fun generate_inconsistent, args:";
7.138 + val (_, (Rewrite' (_,_,_,_, thm', f, (f', asm))), (is, ctxt), (p,_), pt) =
7.139 + (0,
7.140 + (Rewrite' ("","",e_rls,true, (fillpatID, ""(*errpatthm known in find_fillpatterns*)),
7.141 + f_curr, (fillform, []))),
7.142 + (get_loc pt pos), (lev_on p, Und), pt);
7.143 +if p = [2] then () else error "generate_inconsistent changed 1";
7.144 +
7.145 +val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
7.146 + (Rewrite thm') (f', asm) Inconsistent
7.147 +val pt = update_branch pt p TransitiveB;
7.148 +
7.149 +"~~~~~ to get_fillformula return val:"; val (pos', _, _, pt) =
7.150 + ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt);
7.151 +if pos' = ([2], Res) then () else error "generate_inconsistent changed 2";
7.152 +
7.153 +upd_calc cI ((pt, pos'), []); upd_ipos cI 1 pos';
7.154 +autocalculateOK2xml cI pos pos' pos';
7.155 +
7.156 +"~~~~~ final check:";
7.157 +val ((pt,pos),_) = get_calc 1;
7.158 +val p = get_pos 1 1;
7.159 +val (Form f, tac, asms) = pt_extract (pt, p);
7.160 +if p = ([2], Res) andalso term2str f =
7.161 + "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos ?_dummy_2 * d_d x ?_dummy_3"
7.162 +then () else error "";
7.163 +
7.164 +show_pt pt; (*ATTENTION: omits the last step, if pt is incomplete, ([2], Res) EXISTS !*)
7.165 +
8.1 --- a/test/Tools/isac/Test_Some.thy Tue May 22 07:00:53 2012 +0200
8.2 +++ b/test/Tools/isac/Test_Some.thy Tue May 22 13:40:06 2012 +0200
8.3 @@ -10,7 +10,33 @@
8.4 *}
8.5 ML {*
8.6 *}
8.7 -ML {* (*==================*)
8.8 +ML {* (*================== --> test/../inform.sml*)
8.9 +"--------- UC errpat, fillpat ---------------------------"; (*--> test/../interface.sml*)
8.10 +"--------- embed fun get_fillform --------------------------------"; (*--> test/../inform.sml*)
8.11 +states := [];
8.12 +CalcTree
8.13 +[(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
8.14 + ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
8.15 +Iterator 1;
8.16 +moveActiveRoot 1;
8.17 +autoCalculate 1 CompleteCalcHead;
8.18 +autoCalculate 1 (Step 1);
8.19 +autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
8.20 +appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)";
8.21 +(* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),
8.22 + would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well.
8.23 + results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>
8.24 + instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)
8.25 +FindFillpatterns 1 "chain-rule-diff-both";
8.26 +(*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =
8.27 + d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *)
8.28 +*}
8.29 +ML {*
8.30 +requestFillformula 1 ("chain-rule-diff-both", "fill-both-args");
8.31 +*}
8.32 +ML {*
8.33 +*}
8.34 +ML {*
8.35 *}
8.36 ML {*
8.37 *}