1.1 --- a/src/Tools/isac/Frontend/interface.sml Thu May 24 19:07:15 2012 +0200
1.2 +++ b/src/Tools/isac/Frontend/interface.sml Fri May 25 09:58:20 2012 +0200
1.3 @@ -806,7 +806,7 @@
1.4 fun requestFillformula cI (errpatID, fillpatID) =
1.5 let
1.6 val ((pt, _), _) = get_calc cI
1.7 - val pos as (p, _) = get_pos cI 1
1.8 + val pos = get_pos cI 1
1.9 val fillforms = find_fillpatterns (pt, pos) errpatID
1.10 in
1.11 case filter ((curry op = fillpatID) o
1.12 @@ -814,7 +814,7 @@
1.13 (_, fillform, thm, sube_opt) :: _ =>
1.14 let
1.15 val (pt, pos') = generate_inconsistent_rew (sube_opt, thm'_of_thm thm)
1.16 - (fillform, []) (get_loc pt pos) (lev_on p, Und) pt
1.17 + (fillform, []) (get_loc pt pos) pos pt
1.18 in
1.19 (upd_calc cI ((pt, pos'), []); (*upd_ipos cI 1 pos';*)
1.20 autocalculateOK2xml cI pos pos' pos')
2.1 --- a/src/Tools/isac/Interpret/generate.sml Thu May 24 19:07:15 2012 +0200
2.2 +++ b/src/Tools/isac/Interpret/generate.sml Fri May 25 09:58:20 2012 +0200
2.3 @@ -472,7 +472,7 @@
2.4
2.5 fun generate_inconsistent_rew (subs_opt, thm') (f', asm) (is, ctxt) (pos as (p,_)) pt =
2.6 let
2.7 - val f = get_curr_formula (pt, pos) (*already done in find_fillpatterns, too*)
2.8 + val f = get_curr_formula (pt, lev_back' pos)
2.9 val (pt,c) =
2.10 case subs_opt of
2.11 NONE => cappend_atomic pt p (is, insert_assumptions asm ctxt) f
3.1 --- a/src/Tools/isac/Interpret/inform.sml Thu May 24 19:07:15 2012 +0200
3.2 +++ b/src/Tools/isac/Interpret/inform.sml Fri May 25 09:58:20 2012 +0200
3.3 @@ -734,7 +734,7 @@
3.4
3.5 fun find_fillpatterns (pt, pos as (p, _): pos') errpatID =
3.6 let
3.7 - val f_curr = get_curr_formula (pt, pos); (* = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"*)
3.8 + val f_curr = get_curr_formula (pt, pos);
3.9 val pp = par_pblobj pt p
3.10 val {errpats, scr = Script prog, ...} = get_met (get_obj g_metID pt pp)
3.11 val ScrState (env, _, _, _, _, _) = get_istate pt pos
4.1 --- a/test/Tools/isac/Interpret/generate.sml Thu May 24 19:07:15 2012 +0200
4.2 +++ b/test/Tools/isac/Interpret/generate.sml Fri May 25 09:58:20 2012 +0200
4.3 @@ -6,8 +6,75 @@
4.4 "-----------------------------------------------------------------";
4.5 "table of contents -----------------------------------------------";
4.6 "-----------------------------------------------------------------";
4.7 -"----------- test TODO -------------------------------------------";
4.8 +"--------- embed fun generate_inconsistent_rew -------------------";
4.9 "-----------------------------------------------------------------";
4.10 "-----------------------------------------------------------------";
4.11 "-----------------------------------------------------------------";
4.12
4.13 +"--------- embed fun generate_inconsistent_rew -------------------";
4.14 +"--------- embed fun generate_inconsistent_rew -------------------";
4.15 +"--------- embed fun generate_inconsistent_rew -------------------";
4.16 +states := [];
4.17 +CalcTree
4.18 +[(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
4.19 + ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
4.20 +Iterator 1;
4.21 +moveActiveRoot 1;
4.22 +autoCalculate 1 CompleteCalcHead;
4.23 +autoCalculate 1 (Step 1);
4.24 +autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
4.25 +appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)";
4.26 +(* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),
4.27 + would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well.
4.28 + results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>
4.29 + instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)
4.30 +findFillpatterns 1 "chain-rule-diff-both";
4.31 +(*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =
4.32 + d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *)
4.33 +
4.34 +"~~~~~ fun requestFillformula, args:"; val (cI, (errpatID, fillpatID)) =
4.35 + (1, ("chain-rule-diff-both", "fill-both-args"));
4.36 + val ((pt, _), _) = get_calc cI
4.37 + val pos as (p, _) = get_pos cI 1;
4.38 + val fillforms = find_fillpatterns (pt, pos) errpatID;
4.39 +
4.40 +if pos = ([1], Res) then () else error "requestFillformula changed 1";
4.41 +
4.42 + val (_, fillform, thm, sube_opt) :: _ = filter ((curry op = fillpatID) o
4.43 + (#1: (fillpatID * term * thm * (subs option) -> fillpatID))) fillforms;
4.44 +
4.45 +"~~~~~ fun generate_inconsistent_rew, args:";
4.46 + val ((subs_opt, thm'), f', (is, ctxt), pos, pt) =
4.47 + ((sube_opt, thm'_of_thm thm), fillform, (get_loc pt pos), pos, pt);
4.48 +
4.49 + val f = get_curr_formula (pt, pos);
4.50 + val pos' as (p', _) = (lev_on p, Res);
4.51 +
4.52 +if pos = ([1], Res) then () else error "requestFillformula changed 2a";
4.53 +if term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"
4.54 + then () else error "requestFillformula changed 2b";
4.55 +
4.56 + val (pt,c) =
4.57 + case subs_opt of
4.58 + NONE => cappend_atomic pt p' (is, insert_assumptions [] ctxt) f
4.59 + (Rewrite thm') (f', []) Inconsistent
4.60 + | SOME subs => cappend_atomic pt p' (is, insert_assumptions [] ctxt) f
4.61 + (Rewrite_Inst (subs, thm')) (f', []) Inconsistent
4.62 + val pt = update_branch pt p TransitiveB;
4.63 +
4.64 +"~~~~~ to requestFillformula return val:"; val (pt, pos') = (pt, pos');
4.65 +(*val (pt, pos') = generate_inconsistent_rew (sube_opt, thm'_of_thm thm)
4.66 + (fillform, []) (get_loc pt pos) pos' pt*)
4.67 +upd_calc cI ((pt, pos'), []); upd_ipos cI 1 pos';
4.68 +autocalculateOK2xml cI pos pos' pos';
4.69 +
4.70 +"~~~~~ final check:";
4.71 +val ((pt,pos),_) = get_calc 1;
4.72 +val p = get_pos 1 1;
4.73 +val (Form f, tac, asms) = pt_extract (pt, p);
4.74 +if p = ([2], Res) andalso term2str f =
4.75 + "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos ?_dummy_2 * d_d x ?_dummy_3"
4.76 +then () else error "";
4.77 +
4.78 +show_pt pt; (*ATTENTION: omits the last step, if pt is incomplete, ([2], Res) EXISTS !*)
4.79 +
5.1 --- a/test/Tools/isac/Interpret/inform.sml Thu May 24 19:07:15 2012 +0200
5.2 +++ b/test/Tools/isac/Interpret/inform.sml Fri May 25 09:58:20 2012 +0200
5.3 @@ -36,16 +36,11 @@
5.4 "--------- build fun check_error_patterns ------------------------";
5.5 "--------- embed fun check_error_patterns ------------------------";
5.6 "--------- embed fun find_fillpatterns ---------------------------";
5.7 -"--------- embed fun get_fillformula -----------------------------";
5.8 "-----------------------------------------------------------------";
5.9 "-----------------------------------------------------------------";
5.10 "-----------------------------------------------------------------";
5.11
5.12
5.13 -
5.14 -
5.15 -
5.16 -
5.17 "--------- appendFormula: on Res + equ_nrls ----------------------";
5.18 "--------- appendFormula: on Res + equ_nrls ----------------------";
5.19 "--------- appendFormula: on Res + equ_nrls ----------------------";
5.20 @@ -1035,75 +1030,3 @@
5.21 "#fill-all#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) = d_d x (x ^^^ 2) + ?_dummy_1#"
5.22 then () else error "find_fillpatterns changed 4";
5.23
5.24 -
5.25 -"--------- embed fun get_fillformula -----------------------------";
5.26 -"--------- embed fun get_fillformula -----------------------------";
5.27 -"--------- embed fun get_fillformula -----------------------------";
5.28 -states := [];
5.29 -CalcTree
5.30 -[(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
5.31 - ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
5.32 -Iterator 1;
5.33 -moveActiveRoot 1;
5.34 -autoCalculate 1 CompleteCalcHead;
5.35 -autoCalculate 1 (Step 1);
5.36 -autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
5.37 -appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)";
5.38 -(* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),
5.39 - would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well.
5.40 - results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>
5.41 - instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)
5.42 -findFillpatterns 1 "chain-rule-diff-both";
5.43 -(*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =
5.44 - d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *)
5.45 -
5.46 -"~~~~~ fun requestFillformula, args:"; val (cI, (errpatID, fillpatID)) =
5.47 - (1, ("chain-rule-diff-both", "fill-both-args"));
5.48 -val ((pt, _), _) = get_calc cI
5.49 -val pos = get_pos cI 1; (* = ([1], Res)*)
5.50 -
5.51 -"~~~~~ fun get_fillformula, args:"; val ((pt, pos as (p, _)), (errpatID, fillpatID)) =
5.52 - ((pt, pos), (errpatID, fillpatID));
5.53 -val fillforms = find_fillpatterns (pt, pos) errpatID
5.54 -val fillforms =
5.55 - filter ((curry op = fillpatID) o (#1: (fillpatID * term * thm * (subs option) -> fillpatID))) fillforms;
5.56 -
5.57 -val [(fillpatID, fillform, thm, subs_opt)] = fillforms;
5.58 -case (fillpatID, fillform, thm, subs_opt) of
5.59 - ("fill-both-args", tm, thm, subs_opt) => if term2str tm =
5.60 - "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos ?_dummy_2 * d_d x ?_dummy_3"
5.61 - then () else error "get_fillformula changed 1a"
5.62 -| _ => error "get_fillformula changed 1b";
5.63 -
5.64 - val f_curr = get_curr_formula (pt, pos); (*already done in find_fillpatterns, too*)
5.65 -term2str f_curr = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))";
5.66 -
5.67 -"~~~~~ fun generate_inconsistent, args:";
5.68 - val (_, (Rewrite' (_,_,_,_, thm', f, (f', asm))), (is, ctxt), (p,_), pt) =
5.69 - (0,
5.70 - (Rewrite' ("","",e_rls,true, (fillpatID, ""(*errpatthm known in find_fillpatterns*)),
5.71 - f_curr, (fillform, []))),
5.72 - (get_loc pt pos), (lev_on p, Und), pt);
5.73 -if p = [2] then () else error "generate_inconsistent changed 1";
5.74 -
5.75 -val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
5.76 - (Rewrite thm') (f', asm) Inconsistent
5.77 -val pt = update_branch pt p TransitiveB;
5.78 -
5.79 -"~~~~~ to get_fillformula return val:"; val (pos', _, _, pt) =
5.80 - ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt);
5.81 -if pos' = ([2], Res) then () else error "generate_inconsistent changed 2";
5.82 -
5.83 -upd_calc cI ((pt, pos'), []); upd_ipos cI 1 pos';
5.84 -autocalculateOK2xml cI pos pos' pos';
5.85 -
5.86 -"~~~~~ final check:";
5.87 -val ((pt,pos),_) = get_calc 1;
5.88 -val p = get_pos 1 1;
5.89 -val (Form f, tac, asms) = pt_extract (pt, p);
5.90 -if p = ([2], Res) andalso term2str f =
5.91 - "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos ?_dummy_2 * d_d x ?_dummy_3"
5.92 -then () else error "";
5.93 -
5.94 -show_pt pt; (*ATTENTION: omits the last step, if pt is incomplete, ([2], Res) EXISTS !*)
5.95 -
6.1 --- a/test/Tools/isac/Test_Some.thy Thu May 24 19:07:15 2012 +0200
6.2 +++ b/test/Tools/isac/Test_Some.thy Fri May 25 09:58:20 2012 +0200
6.3 @@ -10,7 +10,7 @@
6.4 *}
6.5 ML {*
6.6 *}
6.7 -text {* (*================== --> test/../inform.sml*)
6.8 +ML {* (*================== --> test/../inform.sml*)
6.9 "--------- UC errpat, fillpat ---------------------------"; (*--> test/../interface.sml*)
6.10 "--------- build fun is_exactly_equal, .....----------------------"; (*--> test/../inform.sml*)
6.11 "--------- build fun is_exactly_equal, .....----------------------"; (*--> test/../inform.sml*)
6.12 @@ -39,15 +39,24 @@
6.13 d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *)
6.14 val ((pt,pos),_) = get_calc 1;
6.15 val p = get_pos 1 1;
6.16 +
6.17 val (Form f, tac, asms) = pt_extract (pt, p);
6.18 if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" then ()
6.19 else error "embed fun get_fillform changed 2";
6.20
6.21 +*}
6.22 +ML {*
6.23 requestFillformula 1 ("chain-rule-diff-both", "fill-both-args");(*<<<<<<<============*)
6.24 (*<AUTOCALC> ([1], Res) ([2], Res) ([2], Res) </AUTOCALC>*)
6.25 val ((pt,pos),_) = get_calc 1;
6.26 val p = get_pos 1 1;
6.27 val (Form f, tac, asms) = pt_extract (pt, p);
6.28 +*}
6.29 +ML {*
6.30 +*}
6.31 +ML {*
6.32 +*}
6.33 +text {*
6.34 if p = ([1], Res) andalso existpt [2] pt andalso
6.35 term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
6.36 tac = SOME (Rewrite ("fill-both-args", "")) then ()
6.37 @@ -55,7 +64,7 @@
6.38 *}
6.39 ML {*
6.40 (* input a formula which exactly fills the gaps in a "fillformula"
6.41 - presented to the learner immediately before by requestFillformula (errpatID, fillpatID):
6.42 + presented to the learner immediately before by "requestFillformula (errpatID, fillpatID)":
6.43 errpatID: lhs of the respective thm = lhs of fillformula with fillpatID.
6.44 the respective thm is in the ctree ................
6.45 *)
6.46 @@ -87,13 +96,13 @@
6.47 Thm.get_name_hint;
6.48 Thm.derivation_name;
6.49 *}
6.50 -ML {* (*================== already in code*)
6.51 +ML {*
6.52 *}
6.53 ML {*
6.54 *}
6.55 -
6.56 -ML {* (*==================*)
6.57 -
6.58 +ML {*
6.59 +*}
6.60 +ML {*
6.61 *}
6.62 ML {*
6.63 *}