# HG changeset patch # User Walther Neuper # Date 1337686806 -7200 # Node ID 7dc25d1526a56766baf698c14d31356bbc618cdc # Parent 22f0435fdfe2cb96c91d723186d1ae3e841b088f added "fun requestFillformula" given a fillpatID propose a fillform to the learner on the worksheet; the "ctree" is extended with fillpat and "ostate Inconsistent", the "istate" is NOT updated; returns CalcChanged. arg errpatID: required because there is no dialog-related state in the math-kernel. ATTENTION: the handling of "Inconsistent" and pos will be tested with "fun inputFillformula". diff -r 22f0435fdfe2 -r 7dc25d1526a5 src/Tools/isac/Frontend/interface.sml --- a/src/Tools/isac/Frontend/interface.sml Tue May 22 07:00:53 2012 +0200 +++ b/src/Tools/isac/Frontend/interface.sml Tue May 22 13:40:06 2012 +0200 @@ -53,6 +53,7 @@ val setProblem : calcID -> pblID -> unit val setTheory : calcID -> thyID -> unit val FindFillpatterns : calcID -> errpatID -> unit + val requestFillformula : calcID -> errpatID * fillpatID -> unit (*------------ for tests*) val encode: cterm' -> cterm' val encode_fmz: fmz -> fmz @@ -791,8 +792,35 @@ val ((pt, _), _) = get_calc cI val pos = get_pos cI 1; val fillpats = find_fillpatterns (pt, pos) errpatID + val args = "fill patterns " ^ ((map (apsnd term2str) fillpats) |> map pair2str_ |> strs2str_) (* the format for the message's arguments is waiting for generalisation of CalcMessage *) - in calcMessage2xml cI ("fill patterns " ^ (fillpats |> map pair2str_ |> strs2str_)) end; + in calcMessage2xml cI ("fill patterns " ^ args) end; + +(* given a fillpatID propose a fillform to the learner on the worksheet; + the "ctree" is extended with fillpat and "ostate Inconsistent", the "istate" is NOT updated; + returns CalcChanged. + arg errpatID: required because there is no dialog-related state in the math-kernel. +*) +fun requestFillformula cI (errpatID, fillpatID) = + let + val ((pt, _), _) = get_calc cI + val pos as (p, _) = get_pos cI 1 + val fillforms = find_fillpatterns (pt, pos) errpatID + in + case filter ((curry op = fillpatID) o (#1: (fillpatID * term -> fillpatID))) fillforms of + (fillpatID, fillform) :: _ => + let + val f_curr = get_curr_formula (pt, pos) (*already done in find_fillpatterns, too*) + val (pos', _, _, pt) = generate_inconsistent 0 + (Rewrite' ("","",e_rls,true, (fillpatID, ""(*errpatthm known in find_fillpatterns*)), + f_curr, (fillform, []))) + (get_loc pt pos) (lev_on p, Und) pt + in + (upd_calc cI ((pt, pos'), []); (*upd_ipos cI 1 pos';*) + autocalculateOK2xml cI pos pos' pos') + end + | _ => autocalculateERROR2xml cI "no fillpattern found" + end; (*------------------------------------------------------------------*) end diff -r 22f0435fdfe2 -r 7dc25d1526a5 src/Tools/isac/Interpret/calchead.sml --- a/src/Tools/isac/Interpret/calchead.sml Tue May 22 07:00:53 2012 +0200 +++ b/src/Tools/isac/Interpret/calchead.sml Tue May 22 13:40:06 2012 +0200 @@ -1945,38 +1945,35 @@ list .*) fun get_interval from to level pt = -(* val (from,level) = (f,lev); - val (from, to, level) = (([3, 2, 1], Res), ([],Res), 9999); - *) - let fun get_inter c (from:pos') (to:pos') lev pt = -(* val (c, from, to, lev) = ([], from, to, level); - ------for recursion....... - val (c, from:pos', to:pos') = (c @ [(from, f)], move_dn [] pt from, to); - *) + let + fun get_inter c (from:pos') (to:pos') lev pt = if eq_pos' from to orelse from = ([],Res) (*orelse ... avoids Exception- PTREE "end of calculation" raised, if 'to' has values NOT generated by move_dn, see systest/me.sml TODO.WN0501: introduce an order on pos' and check "from > to".. ...there is an order in Java! WN051224 the hack got worse with returning term instead ptform*) - then let val (f,_,_) = pt_extract (pt, from) - in case f of - ModSpec (_,_,headline,_,_,_) => c @ [(from, headline)] - | Form t => c @ [(from, t)] - end + then + let val (f,_,_) = pt_extract (pt, from) + in + case f of + ModSpec (_,_,headline,_,_,_) => c @ [(from, headline)] + | Form t => c @ [(from, t)] + end else - if lev < lev_of from - then (get_inter c (move_dn [] pt from) to lev pt) - handle (PTREE _(*from move_dn too far*)) => c - else let val (f,_,_) = pt_extract (pt, from) - val term = case f of - ModSpec (_,_,headline,_,_,_)=> headline - | Form t => t - in (get_inter (c @ [(from, term)]) - (move_dn [] pt from) to lev pt) - handle (PTREE _(*from move_dn too far*)) - => c @ [(from, term)] end - in get_inter [] from to level pt end; + if lev < lev_of from + then (get_inter c (move_dn [] pt from) to lev pt) + handle (PTREE _(*from move_dn too far*)) => c + else + let + val (f,_,_) = pt_extract (pt, from) + val term = case f of + ModSpec (_,_,headline,_,_,_) => headline + | Form t => t + in (get_inter (c @ [(from, term)]) (move_dn [] pt from) to lev pt) + handle (PTREE _(*from move_dn too far*)) => c @ [(from, term)] + end + in get_inter [] from to level pt end; (*for tests*) fun posform2str (pos:pos', form) = diff -r 22f0435fdfe2 -r 7dc25d1526a5 src/Tools/isac/Interpret/generate.sml --- a/src/Tools/isac/Interpret/generate.sml Tue May 22 07:00:53 2012 +0200 +++ b/src/Tools/isac/Interpret/generate.sml Tue May 22 13:40:06 2012 +0200 @@ -389,7 +389,7 @@ val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f (Rewrite thm') (f',asm) Complete val pt = update_branch pt p TransitiveB - in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt)end + in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end | generate1 thy (Rewrite_Asm' all) l p pt = generate1 thy (Rewrite' all) l p pt @@ -470,6 +470,13 @@ | generate1 thy m' _ _ _ = error ("generate1: not impl.for "^(tac_2str m')); +fun generate_inconsistent _ (Rewrite' (_,_,_,_, thm', f, (f', asm))) (is, ctxt) (p,_) pt = + let + val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f + (Rewrite thm') (f', asm) Inconsistent + val pt = update_branch pt p TransitiveB + in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt)end + fun generate_hard thy m' (p,p_) pt = let val p = diff -r 22f0435fdfe2 -r 7dc25d1526a5 src/Tools/isac/Interpret/inform.sml --- a/src/Tools/isac/Interpret/inform.sml Tue May 22 07:00:53 2012 +0200 +++ b/src/Tools/isac/Interpret/inform.sml Tue May 22 13:40:06 2012 +0200 @@ -720,7 +720,7 @@ rew_sub (Isac()) 1 subst e_rew_ord e_rls false [] (Trueprop $ pat) form; in (*the fillpat of the thm must be dedicated to errpatID*) if errpatID = erpaID andalso rewritten - then SOME (fillpatID, term2str (HOLogic.mk_eq (form, form'))) else NONE end; + then SOME (fillpatID, HOLogic.mk_eq (form, form')) else NONE end; fun get_fillpats subst form errpatID thm = let diff -r 22f0435fdfe2 -r 7dc25d1526a5 src/Tools/isac/Knowledge/Build_Thydata.thy --- a/src/Tools/isac/Knowledge/Build_Thydata.thy Tue May 22 07:00:53 2012 +0200 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy Tue May 22 13:40:06 2012 +0200 @@ -118,15 +118,15 @@ (*WN210512 DESIGN TODO: build thehier already in respective theories*) val fillpats = [ ("fill-d_d-arg", - parse_patt thy "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"), + parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"), ("fill-both-args", - parse_patt thy "d_d ?bdv (sin _) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"), + parse_patt @{theory Diff} "d_d ?bdv (sin _) = cos _ * d_d ?bdv _", "chain-rule-diff-both"), ("fill-d_d", - parse_patt thy "d_d ?bdv (sin ?u) = cos ?u * _ ?bdv ?u", "chain-rule-diff-both"), + parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * _ ?bdv ?u", "chain-rule-diff-both"), ("fill-inner-deriv", - parse_patt thy "d_d ?bdv (sin ?u) = cos ?u * _", "chain-rule-diff-both"), + parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * _", "chain-rule-diff-both"), ("fill-all", - parse_patt thy "d_d ?bdv (sin ?u) = _", "chain-rule-diff-both")]: fillpat list; + parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = _", "chain-rule-diff-both")]: fillpat list; insert_fillpats @{theory Diff} "IsacKnowledge" ("diff_sin_chain", @{thm diff_sin_chain}) fillpats; (* compare test/../thy-hierarchy.sml *) *} diff -r 22f0435fdfe2 -r 7dc25d1526a5 test/Tools/isac/Frontend/interface.sml --- a/test/Tools/isac/Frontend/interface.sml Tue May 22 07:00:53 2012 +0200 +++ b/test/Tools/isac/Frontend/interface.sml Tue May 22 13:40:06 2012 +0200 @@ -48,6 +48,7 @@ "--------- replaceFormula {SOL:MAN:FOR:replace} other----"; "--------- replaceFormula {SOL:MAN:FOR:replace} other 2--"; "--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----"; +"--------- UC errpat, fillpat ---------------------------"; "--------------------------------------------------------"; "within struct ---------------------------------------------------"; diff -r 22f0435fdfe2 -r 7dc25d1526a5 test/Tools/isac/Interpret/inform.sml --- a/test/Tools/isac/Interpret/inform.sml Tue May 22 07:00:53 2012 +0200 +++ b/test/Tools/isac/Interpret/inform.sml Tue May 22 13:40:06 2012 +0200 @@ -36,6 +36,7 @@ "--------- build fun check_error_patterns ------------------------"; "--------- embed fun check_error_patterns ------------------------"; "--------- embed fun find_fillpatterns ---------------------------"; +"--------- embed fun get_fillform --------------------------------"; "-----------------------------------------------------------------"; "-----------------------------------------------------------------"; "-----------------------------------------------------------------"; @@ -931,7 +932,7 @@ val pos_pred = lev_back' pos (* f_pred ---"step pos cs"---> f_succ in appendFormula TODO.WN120517: one starting point for redesign of pos' *) -val (f_pred, f_succ) = (get_pred_formula (pt, pos_pred), get_pred_formula (pt, pos)); +val (f_pred, f_succ) = (get_curr_formula (pt, pos_pred), get_curr_formula (pt, pos)); term2str f_pred = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"; term2str f_succ = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)"; @@ -971,13 +972,14 @@ autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*) appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)"; (* error pattern #chain-rule-diff-both# *) - (*TODO BACK TO no derivation found *) + (*or + no derivation found *) "~~~~~ fun FindFillpatterns, args:"; val (cI, errpatID) = (1, "chain-rule-diff-both"); val ((pt, _), _) = get_calc cI val pos = get_pos cI 1; - "~~~~~ fun find_fillpatterns, args:"; val ((pt, pos as (p, _)), errpatID) = ((pt, pos), errpatID); - val f_curr = get_pred_formula (pt, pos); (* = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"*) +"~~~~~ fun find_fillpatterns, args:"; val ((pt, pos as (p, _)), errpatID) = ((pt, pos), errpatID); + val f_curr = get_curr_formula (pt, pos); (* = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"*) val pp = par_pblobj pt p val {errpats, scr = Script prog, ...} = get_met (get_obj g_metID pt pp) val ScrState (env, _, _, _, _, _) = get_istate pt pos @@ -988,13 +990,13 @@ |> flat; case map (get_fillpats subst f_curr errpatID) errpatthms |> flat of - ("fill-d_d-arg", - "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1") - :: _ => () -| _ => error "find_fillpatterns changed" + ("fill-d_d-arg", tm) :: _ => if term2str tm = + "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1" + then () else error "find_fillpatterns changed 1a" +| _ => error "find_fillpatterns changed 1b" "~~~~~ fun get_fillpats, args:"; val (subst, form, errpatID, thm) = - (subst, f_curr, errpatID, hd errpatthms); + (subst, f_curr, errpatID, hd (*simulate beginning of "map"*) errpatthms); val thmDeriv = Thm.get_name_hint thm val (part, thyID) = thy_containing_thm thmDeriv val theID = [part, thyID, "Theorems", thmID_of_derivation_name thmDeriv] @@ -1002,8 +1004,104 @@ val some = map (get_fillform subst form errpatID) fillpats; case some |> filter is_some |> map the of - ("fill-d_d-arg", - "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1") - :: _ => () -| _ => error "get_fillpats changed" + ("fill-d_d-arg", tm) :: _ => if term2str tm = + "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1" + then () else error "find_fillpatterns changed 2a" +| _ => error "find_fillpatterns changed 2b" +"~~~~~ fun get_fillform, args:"; val (subst, form, errpatID, ((fillpatID, pat, erpaID): fillpat)) = + (subst, form, errpatID, hd (*simulate beginning of "map"*) fillpats); + val (form', _, _, rewritten) = + rew_sub (Isac()) 1 subst e_rew_ord e_rls false [] (Trueprop $ pat) form; + +if term2str form' = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1" then () +else error "find_fillpatterns changed 3"; + +"~~~~~ to FindFillpatterns return val:"; val (fillpats) = + (map (get_fillpats subst f_curr errpatID) errpatthms |> flat) (*only from "hd errpatthms"*); + +val msg = "fill patterns " ^ ((map (apsnd term2str) fillpats) |> map pair2str_ |> strs2str_); +if msg = + "fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" ^ + " =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1" ^ + "#fill-both-args#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" ^ + " =\nd_d x (x ^^^ 2) + cos ?_dummy_2 * d_d x ?_dummy_3" ^ + "#fill-d_d#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" ^ + " =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * ?_dummy_1 x (x ^^^ 4)" ^ + "#fill-inner-deriv#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" ^ + " =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * ?_dummy_1" ^ + "#fill-all#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) = d_d x (x ^^^ 2) + ?_dummy_1#" +then () else error "find_fillpatterns changed 4"; + + +"--------- embed fun get_fillform --------------------------------"; +"--------- embed fun get_fillform --------------------------------"; +"--------- embed fun get_fillform --------------------------------"; +states := []; +CalcTree +[(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"], + ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))]; +Iterator 1; +moveActiveRoot 1; +autoCalculate 1 CompleteCalcHead; +autoCalculate 1 (Step 1); +autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*) +appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)"; +(* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"), + would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well. + results in error pattern #chain-rule-diff-both# + instead of no derivation found *) +FindFillpatterns 1 "chain-rule-diff-both"; +(* fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) = + d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *) + +"~~~~~ fun requestFillformula, args:"; val (cI, (errpatID, fillpatID)) = + (1, ("chain-rule-diff-both", "fill-both-args")); +val ((pt, _), _) = get_calc cI +val pos = get_pos cI 1; (* = ([1], Res)*) + +"~~~~~ fun get_fillformula, args:"; val ((pt, pos as (p, _)), (errpatID, fillpatID)) = + ((pt, pos), (errpatID, fillpatID)); +val fillforms = find_fillpatterns (pt, pos) errpatID +val fillforms = + filter ((curry op = fillpatID) o (#1: (fillpatID * term -> fillpatID))) fillforms; + +val [(fillpatID, fillform)] = fillforms; +case (fillpatID, fillform) of + ("fill-both-args", tm) => if term2str tm = + "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos ?_dummy_2 * d_d x ?_dummy_3" + then () else error "get_fillformula changed 1a" +| _ => error "get_fillformula changed 1b"; + + val f_curr = get_curr_formula (pt, pos); (*already done in find_fillpatterns, too*) +term2str f_curr = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"; + +"~~~~~ fun generate_inconsistent, args:"; + val (_, (Rewrite' (_,_,_,_, thm', f, (f', asm))), (is, ctxt), (p,_), pt) = + (0, + (Rewrite' ("","",e_rls,true, (fillpatID, ""(*errpatthm known in find_fillpatterns*)), + f_curr, (fillform, []))), + (get_loc pt pos), (lev_on p, Und), pt); +if p = [2] then () else error "generate_inconsistent changed 1"; + +val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f + (Rewrite thm') (f', asm) Inconsistent +val pt = update_branch pt p TransitiveB; + +"~~~~~ to get_fillformula return val:"; val (pos', _, _, pt) = + ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt); +if pos' = ([2], Res) then () else error "generate_inconsistent changed 2"; + +upd_calc cI ((pt, pos'), []); upd_ipos cI 1 pos'; +autocalculateOK2xml cI pos pos' pos'; + +"~~~~~ final check:"; +val ((pt,pos),_) = get_calc 1; +val p = get_pos 1 1; +val (Form f, tac, asms) = pt_extract (pt, p); +if p = ([2], Res) andalso term2str f = + "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos ?_dummy_2 * d_d x ?_dummy_3" +then () else error ""; + +show_pt pt; (*ATTENTION: omits the last step, if pt is incomplete, ([2], Res) EXISTS !*) + diff -r 22f0435fdfe2 -r 7dc25d1526a5 test/Tools/isac/Test_Some.thy --- a/test/Tools/isac/Test_Some.thy Tue May 22 07:00:53 2012 +0200 +++ b/test/Tools/isac/Test_Some.thy Tue May 22 13:40:06 2012 +0200 @@ -10,7 +10,33 @@ *} ML {* *} -ML {* (*==================*) +ML {* (*================== --> test/../inform.sml*) +"--------- UC errpat, fillpat ---------------------------"; (*--> test/../interface.sml*) +"--------- embed fun get_fillform --------------------------------"; (*--> test/../inform.sml*) +states := []; +CalcTree +[(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"], + ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))]; +Iterator 1; +moveActiveRoot 1; +autoCalculate 1 CompleteCalcHead; +autoCalculate 1 (Step 1); +autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*) +appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)"; +(* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"), + would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well. + results in error pattern #chain-rule-diff-both# + instead of no derivation found *) +FindFillpatterns 1 "chain-rule-diff-both"; +(* fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) = + d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *) +*} +ML {* +requestFillformula 1 ("chain-rule-diff-both", "fill-both-args"); +*} +ML {* +*} +ML {* *} ML {* *}