1.1 --- a/src/Tools/isac/Frontend/interface.sml Fri May 25 09:58:20 2012 +0200
1.2 +++ b/src/Tools/isac/Frontend/interface.sml Fri May 25 16:30:15 2012 +0200
1.3 @@ -54,6 +54,7 @@
1.4 val setTheory : calcID -> thyID -> unit
1.5 val findFillpatterns : calcID -> errpatID -> unit
1.6 val requestFillformula : calcID -> errpatID * fillpatID -> unit
1.7 + val inputFillFormula: calcID -> string -> unit
1.8 (*------------ for tests*)
1.9 val encode: cterm' -> cterm'
1.10 val encode_fmz: fmz -> fmz
1.11 @@ -154,36 +155,27 @@
1.12
1.13 (*. apply a tactic at a position and update the calc-tree if applicable .*)
1.14 (*WN080226 java-code is missing, errors smltest/Knowledge/polyminus.sml*)
1.15 -(* val (cI, ip, tac) = (1, p, hd appltacs);
1.16 - val (cI, ip, tac) = (1, p, (hd (sel_appl_atomic_tacs pt p)));
1.17 - *)
1.18 fun applyTactic (cI:calcID) ip tac =
1.19 - let val ((pt, _), _) = get_calc cI
1.20 - val p = get_pos cI 1
1.21 - in
1.22 - case locatetac tac (pt, ip)
1.23 - of
1.24 -(* val ("ok", (tacis, c, (pt',p'))) = locatetac tac (pt, ip);*)
1.25 - ("ok", (_, c, ptp as (_,p'))) =>
1.26 - (upd_calc cI (ptp, []); upd_ipos cI 1 p';
1.27 - autocalculateOK2xml cI p (if null c then p'
1.28 - else last_elem c) p')
1.29 - | ("unsafe-ok", (_, c, ptp as (_,p'))) =>
1.30 - (upd_calc cI (ptp, []); upd_ipos cI 1 p';
1.31 - autocalculateOK2xml cI p (if null c then p'
1.32 - else last_elem c) p')
1.33 - | ("end-of-calculation", (_, c, ptp as (_,p'))) =>
1.34 - (upd_calc cI (ptp, []); upd_ipos cI 1 p';
1.35 - autocalculateOK2xml cI p (if null c then p'
1.36 - else last_elem c) p')
1.37 + let
1.38 + val ((pt, _), _) = get_calc cI
1.39 + val p = get_pos cI 1
1.40 + in
1.41 + case locatetac tac (pt, ip) of
1.42 + ("ok", (_, c, ptp as (_,p'))) =>
1.43 + (upd_calc cI (ptp, []);
1.44 + upd_ipos cI 1 p';
1.45 + autocalculateOK2xml cI p (if null c then p' else last_elem c) p')
1.46 + | ("unsafe-ok", (_, c, ptp as (_,p'))) =>
1.47 + (upd_calc cI (ptp, []);
1.48 + upd_ipos cI 1 p';
1.49 + autocalculateOK2xml cI p (if null c then p' else last_elem c) p')
1.50 + | ("end-of-calculation", (_, c, ptp as (_,p'))) =>
1.51 + (upd_calc cI (ptp, []);
1.52 + upd_ipos cI 1 p';
1.53 + autocalculateOK2xml cI p (if null c then p' else last_elem c) p')
1.54 + | (str,_) => autocalculateERROR2xml cI "failure"
1.55 + end;
1.56
1.57 - | (str,_) => autocalculateERROR2xml cI "failure"
1.58 - end;
1.59 -
1.60 -
1.61 -
1.62 -(* val cI = 1;
1.63 - *)
1.64 fun fetchProposedTactic (cI:calcID) =
1.65 (case step (get_pos cI 1) (get_calc cI) of
1.66 ("ok", (tacis, _, _)) =>
1.67 @@ -550,23 +542,20 @@
1.68 (* replace a formula with_in_ a calculation;
1.69 this situation applies for initial CAS-commands, too *)
1.70 fun replaceFormula cI (ifo:cterm') =
1.71 - (let val ((pt, _), _) = get_calc cI
1.72 - val p = get_pos cI 1
1.73 - in case inform (([], [], (pt, p)): calcstate') (encode ifo) of
1.74 - ("ok", (_(*tacs used for DG ?*), c, ptp' as (pt',p'))) =>
1.75 -(* val (str, (_,c, ptp' as (pt',p')))= inform ([], [], (pt, p)) (encode ifo);
1.76 - *)
1.77 - let val unc = if null (fst p) then p else move_up [] pt p
1.78 - val _ = upd_calc cI (ptp', [])
1.79 - val _ = upd_ipos cI 1 p'
1.80 - in replaceformulaOK2xml cI unc
1.81 - (if null c then unc
1.82 - else last_elem c) p'(*' NEW*) end
1.83 - | ("same-formula", _) =>
1.84 - (*TODO.WN0501 MESSAGE !*)
1.85 - replaceformulaERROR2xml cI "formula not changed"
1.86 - | (msg, _) => replaceformulaERROR2xml cI msg
1.87 - end)
1.88 + (let
1.89 + val ((pt, _), _) = get_calc cI
1.90 + val p = get_pos cI 1
1.91 + in
1.92 + case inform (([], [], (pt, p)): calcstate') (encode ifo) of
1.93 + ("ok", (_(*tacs used for DG ?*), c, ptp' as (pt',p'))) =>
1.94 + let
1.95 + val unc = if null (fst p) then p else move_up [] pt p
1.96 + val _ = upd_calc cI (ptp', [])
1.97 + val _ = upd_ipos cI 1 p'
1.98 + in replaceformulaOK2xml cI unc (if null c then unc else last_elem c) p' end
1.99 + | ("same-formula", _) => replaceformulaERROR2xml cI "formula not changed"
1.100 + | (msg, _) => replaceformulaERROR2xml cI msg
1.101 + end)
1.102 handle _ => sysERROR2xml cI "error in kernel";
1.103
1.104
1.105 @@ -814,7 +803,7 @@
1.106 (_, fillform, thm, sube_opt) :: _ =>
1.107 let
1.108 val (pt, pos') = generate_inconsistent_rew (sube_opt, thm'_of_thm thm)
1.109 - (fillform, []) (get_loc pt pos) pos pt
1.110 + fillform (get_loc pt pos) pos pt
1.111 in
1.112 (upd_calc cI ((pt, pos'), []); (*upd_ipos cI 1 pos';*)
1.113 autocalculateOK2xml cI pos pos' pos')
1.114 @@ -822,6 +811,37 @@
1.115 | _ => autocalculateERROR2xml cI "no fillpattern found"
1.116 end;
1.117
1.118 +(* input a formula which exactly fills the gaps in a "fillformula"
1.119 + presented to the learner immediately before by "requestFillformula (errpatID, fillpatID)":
1.120 + errpatID: lhs of the respective thm = lhs of fillformula with fillpatID.
1.121 + The respective thm is stored in the ctree. *)
1.122 +fun inputFillFormula cI ifo =
1.123 + let
1.124 + val ((pt, _), _) = get_calc cI
1.125 + val pos = get_pos cI 1;
1.126 + in
1.127 + case is_exactly_equal (pt, pos) ifo of
1.128 + ("ok", tac) =>
1.129 + let
1.130 + in (* cp from applyTactic *)
1.131 + case locatetac tac (pt, pos) of
1.132 + ("ok", (_, c, ptp as (_,p'))) =>
1.133 + (upd_calc cI (ptp, []);
1.134 + upd_ipos cI 1 p';
1.135 + autocalculateOK2xml cI pos (if null c then p' else last_elem c) p')
1.136 + | ("unsafe-ok", (_, c, ptp as (_,p'))) =>
1.137 + (upd_calc cI (ptp, []);
1.138 + upd_ipos cI 1 p';
1.139 + autocalculateOK2xml cI pos (if null c then p' else last_elem c) p')
1.140 + | ("end-of-calculation", (_, c, ptp as (_,p'))) =>
1.141 + (upd_calc cI (ptp, []);
1.142 + upd_ipos cI 1 p';
1.143 + autocalculateOK2xml cI pos (if null c then p' else last_elem c) p')
1.144 + | (str,_) => autocalculateERROR2xml cI "failure"
1.145 + end
1.146 + | (msg, _) => message2xml cI msg
1.147 + end
1.148 +
1.149 (*------------------------------------------------------------------*)
1.150 end
1.151 open interface;
2.1 --- a/src/Tools/isac/Interpret/calchead.sml Fri May 25 09:58:20 2012 +0200
2.2 +++ b/src/Tools/isac/Interpret/calchead.sml Fri May 25 16:30:15 2012 +0200
2.3 @@ -1841,46 +1841,42 @@
2.4 (by application of another tac to the preceding formula !)
2.5 pos is assumed to come from the frontend, ie. generated by moveDown.*)
2.6 (*cannot be in ctree.sml, because ModSpec has to be calculated*)
2.7 -fun pt_extract (pt,([],Res)) =
2.8 -(* val (pt,([],Res)) = ptp;
2.9 - *)
2.10 +fun pt_extract (pt,([],Res)) = (* WN120512: --returns--> Check_Postcondition WRONGLY
2.11 + see --- build fun is_exactly_equal*)
2.12 (* ML_TODO 110417 get assumptions from ctxt !? *)
2.13 - let val (f, asm) = get_obj g_result pt []
2.14 - in (Form f, NONE, asm) end
2.15 -(* val p = [3,2];
2.16 - *)
2.17 + let val (f, asm) = get_obj g_result pt []
2.18 + in (Form f, NONE, asm) end
2.19 | pt_extract (pt,(p,Res)) =
2.20 -(* val (pt,(p,Res)) = ptp;
2.21 - *)
2.22 - let val (f, asm) = get_obj g_result pt p
2.23 - val tac = if last_onlev pt p
2.24 - then if is_pblobj' pt (lev_up p)
2.25 - then let val (PblObj{spec=(_,pI,_),...}) =
2.26 - get_obj I pt (lev_up p)
2.27 - in if pI = e_pblID then NONE
2.28 - else SOME (Check_Postcond pI) end
2.29 - else SOME End_Trans (*WN0502 TODO for other branches*)
2.30 - else let val p' = lev_on p
2.31 - in if is_pblobj' pt p'
2.32 - then let val (PblObj{origin = (_,(dI,pI,_),_),...}) =
2.33 - get_obj I pt p'
2.34 - in SOME (Subproblem (dI, pI)) end
2.35 - else if f = get_obj g_form pt p'
2.36 - then SOME (get_obj g_tac pt p')
2.37 - (*because this Frm ~~~is not on worksheet*)
2.38 - else SOME (Take (term2str (get_obj g_form pt p')))
2.39 - end
2.40 - in (Form f, tac, asm) end
2.41 -
2.42 + let
2.43 + val (f, asm) = get_obj g_result pt p
2.44 + val tac =
2.45 + if last_onlev pt p
2.46 + then
2.47 + if is_pblobj' pt (lev_up p)
2.48 + then
2.49 + let
2.50 + val (PblObj{spec=(_,pI,_),...}) = get_obj I pt (lev_up p)
2.51 + in if pI = e_pblID then NONE else SOME (Check_Postcond pI) end
2.52 + else SOME End_Trans (*WN0502 TODO for other branches*)
2.53 + else
2.54 + let val p' = lev_on p
2.55 + in
2.56 + if is_pblobj' pt p'
2.57 + then
2.58 + let val (PblObj{origin = (_,(dI,pI,_),_),...}) = get_obj I pt p'
2.59 + in SOME (Subproblem (dI, pI)) end
2.60 + else
2.61 + if f = get_obj g_form pt p'
2.62 + then SOME (get_obj g_tac pt p') (*because this Frm ~~~is not on worksheet*)
2.63 + else SOME (Take (term2str (get_obj g_form pt p')))
2.64 + end
2.65 + in (Form f, tac, asm) end
2.66 | pt_extract (pt, pos as (p,p_(*Frm,Pbl*))) =
2.67 -(* val (pt, pos as (p,p_(*Frm,Pbl*))) = ptp;
2.68 - val (pt, pos as (p,p_(*Frm,Pbl*))) = (pt, p);
2.69 - *)
2.70 - let val ppobj = get_obj I pt p
2.71 - val f = if is_pblobj ppobj then pt_model ppobj p_
2.72 - else get_obj pt_form pt p
2.73 - val tac = g_tac ppobj
2.74 - in (f, SOME tac, []) end;
2.75 + let
2.76 + val ppobj = get_obj I pt p
2.77 + val f = if is_pblobj ppobj then pt_model ppobj p_ else get_obj pt_form pt p
2.78 + val tac = g_tac ppobj
2.79 + in (f, SOME tac, []) end;
2.80
2.81
2.82 (**. get the formula from a ctree-node:
3.1 --- a/src/Tools/isac/Interpret/generate.sml Fri May 25 09:58:20 2012 +0200
3.2 +++ b/src/Tools/isac/Interpret/generate.sml Fri May 25 16:30:15 2012 +0200
3.3 @@ -470,17 +470,18 @@
3.4 | generate1 thy m' _ _ _ =
3.5 error ("generate1: not impl.for "^(tac_2str m'));
3.6
3.7 -fun generate_inconsistent_rew (subs_opt, thm') (f', asm) (is, ctxt) (pos as (p,_)) pt =
3.8 +fun generate_inconsistent_rew (subs_opt, thm') f' (is, ctxt) (pos as (p,_)) pt =
3.9 let
3.10 - val f = get_curr_formula (pt, lev_back' pos)
3.11 + val f = get_curr_formula (pt, pos);
3.12 + val pos' as (p', _) = (lev_on p, Res);
3.13 val (pt,c) =
3.14 case subs_opt of
3.15 - NONE => cappend_atomic pt p (is, insert_assumptions asm ctxt) f
3.16 - (Rewrite thm') (f', asm) Inconsistent
3.17 - | SOME subs => cappend_atomic pt p (is, insert_assumptions asm ctxt) f
3.18 - (Rewrite_Inst (subs, thm')) (f', asm) Inconsistent
3.19 - val pt = update_branch pt p TransitiveB
3.20 - in (pt, (p,Res)) end
3.21 + NONE => cappend_atomic pt p' (is, insert_assumptions [] ctxt) f
3.22 + (Rewrite thm') (f', []) Inconsistent
3.23 + | SOME subs => cappend_atomic pt p' (is, insert_assumptions [] ctxt) f
3.24 + (Rewrite_Inst (subs, thm')) (f', []) Inconsistent
3.25 + val pt = update_branch pt p' TransitiveB;
3.26 + in (pt, pos') end
3.27
3.28 fun generate_hard thy m' (p,p_) pt =
3.29 let
4.1 --- a/src/Tools/isac/Interpret/inform.sml Fri May 25 09:58:20 2012 +0200
4.2 +++ b/src/Tools/isac/Interpret/inform.sml Fri May 25 16:30:15 2012 +0200
4.3 @@ -745,6 +745,30 @@
4.4 |> flat
4.5 in map (get_fillpats subst f_curr errpatID) errpatthms |> flat end;
4.6
4.7 +(* check if an input formula is exactly equal the rewrite from a rule
4.8 + which is stored at the pos where the input is stored of "ok". *)
4.9 +fun is_exactly_equal (pt, pos as (p, _)) istr =
4.10 + case parseNEW (assoc_thy "Isac" |> thy2ctxt) istr of
4.11 + NONE => ("syntax error in '" ^ istr ^ "'", Tac "")
4.12 + | SOME ifo =>
4.13 + let
4.14 + val p' = lev_on p;
4.15 + val tac = get_obj g_tac pt p';
4.16 + in
4.17 + case applicable_in pos pt tac of
4.18 + Notappl msg => (msg, Tac "")
4.19 + | Appl rew =>
4.20 + let
4.21 + val res = case rew of
4.22 + Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) => res
4.23 + | Rewrite' (_, _, _, _, _, _, (res, _)) => res
4.24 + in
4.25 + if not (ifo = res)
4.26 + then ("input does not exactly fill the gaps", Tac "")
4.27 + else ("ok", tac)
4.28 + end
4.29 + end
4.30 +
4.31 (*------------------------------------------------------------------(**)
4.32 end
4.33 open inform;
5.1 --- a/src/Tools/isac/calcelems.sml Fri May 25 09:58:20 2012 +0200
5.2 +++ b/src/Tools/isac/calcelems.sml Fri May 25 16:30:15 2012 +0200
5.3 @@ -154,9 +154,6 @@
5.4
5.5 fun thmID_of_derivation_name dn = last_elem (space_explode "." dn);
5.6 fun thyID_of_derivation_name dn = hd (space_explode "." dn);
5.7 -fun thm'_of_thm thm =
5.8 - ((thyID_of_derivation_name o Thm.get_name_hint) thm,
5.9 - (thmID_of_derivation_name o Thm.get_name_hint) thm): thm'
5.10
5.11 fun eq_thmI ((thmid1 : thmID, _ : thm), (thmid2 : thmID, _ : thm)) =
5.12 (strip_thy thmid1) = (strip_thy thmid2);
5.13 @@ -166,8 +163,10 @@
5.14 fun eq_thmI' ((thmid1, _), (thmid2, _)) =
5.15 (thmID_of_derivation_name thmid1) = (thmID_of_derivation_name thmid2);
5.16
5.17 +val string_of_thm = Thm.get_name_hint; (*FIXME.2009*)
5.18 +fun thm'_of_thm thm =
5.19 + ((thmID_of_derivation_name o Thm.get_name_hint) thm, ""): thm'
5.20
5.21 -val string_of_thm = Thm.get_name_hint; (*FIXME.2009*)
5.22 (*check for [.] as caused by "fun assoc_thm'"*)
5.23 fun string_of_thmI thm =
5.24 let val ct' = (de_quote o string_of_thm) thm
6.1 --- a/test/Tools/isac/Frontend/interface.sml Fri May 25 09:58:20 2012 +0200
6.2 +++ b/test/Tools/isac/Frontend/interface.sml Fri May 25 16:30:15 2012 +0200
6.3 @@ -48,7 +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 +"--------- UC errpat, fillpat ------------------------------------";
6.9 "--------------------------------------------------------";
6.10
6.11 "within struct ---------------------------------------------------";
6.12 @@ -1336,4 +1336,78 @@
6.13 error "FE-interface.sml: diff.behav. in FORMULA:replace} NOTok";
6.14 DEconstrCalcTree 1;
6.15
6.16 +"--------- UC errpat, fillpat ------------------------------------";
6.17 +"--------- UC errpat, fillpat ------------------------------------";
6.18 +"--------- UC errpat, fillpat ------------------------------------";
6.19 +states := [];
6.20 +CalcTree
6.21 +[(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
6.22 + ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
6.23 +Iterator 1;
6.24 +moveActiveRoot 1;
6.25 +autoCalculate 1 CompleteCalcHead;
6.26 +autoCalculate 1 (Step 1);
6.27 +autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
6.28 +appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)"; (*<<<<<<<=========================*)
6.29 +(* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),
6.30 + would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well.
6.31 + results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>
6.32 + instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)
6.33 + val ((pt,pos), _) = get_calc 1;
6.34 + val p = get_pos 1 1;
6.35 + val (Form f, _, asms) = pt_extract (pt, p);
6.36
6.37 + if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
6.38 + get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sum", "Diff.diff_sum"(*?!?*)))
6.39 + then () else error "embed fun get_fillform changed 1";
6.40 +
6.41 +findFillpatterns 1 "chain-rule-diff-both"; (*<<<<<<<=================================*)
6.42 +(*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =
6.43 + d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *)
6.44 + val ((pt,pos),_) = get_calc 1;
6.45 + val p = get_pos 1 1;
6.46 +
6.47 + val (Form f, _, asms) = pt_extract (pt, p);
6.48 + if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
6.49 + get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sum", "Diff.diff_sum"(*?!?*)))
6.50 + then ()
6.51 + else error "embed fun get_fillform changed 2";
6.52 +
6.53 +requestFillformula 1 ("chain-rule-diff-both", "fill-both-args");(*<<<<<<<============*)
6.54 + (*<AUTOCALC> ([1], Res) ([2], Res) ([2], Res) </AUTOCALC>*)
6.55 + val ((pt,pos),_) = get_calc 1;
6.56 + val p = get_pos 1 1;
6.57 + val (Form f, _, asms) = pt_extract (pt, p);
6.58 + if p = ([1], Res) andalso existpt [2] pt andalso
6.59 + term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
6.60 + get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sum", "Diff.diff_sum"))
6.61 + then () else error "embed fun get_fillform changed 3";
6.62 +
6.63 +inputFillFormula 1 "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)";(*<<<<<<<=====*)
6.64 + val ((pt, _),_) = get_calc 1;
6.65 + val p = get_pos 1 1;
6.66 + val (Form f, _, asms) = pt_extract (pt, p);
6.67 + if p = ([2], Res) andalso
6.68 + term2str f = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)" andalso
6.69 + get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", ""))
6.70 + then () else error "inputFillFormula changed 11";
6.71 +
6.72 +autoCalculate 1 CompleteCalc;
6.73 +
6.74 +"~~~~~ final check: the input formula is inserted as it would have been correct from beginning";
6.75 +val ((pt, _),_) = get_calc 1;
6.76 +val p = get_pos 1 1;
6.77 +val (Form f, _, asms) = pt_extract (pt, p);
6.78 +if p = ([], Res) andalso term2str f = "2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3"
6.79 +then () else error "inputFillFormula changed 12";
6.80 +show_pt pt;
6.81 +(*[
6.82 +(([], Frm), Diff (x ^^^ 2 + sin (x ^^^ 4), x)),
6.83 +(([1], Frm), d_d x (x ^^^ 2 + sin (x ^^^ 4))),
6.84 +(([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))),
6.85 +(([2], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)), (*<<<<<<<=====*)
6.86 +(([3], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * (4 * x ^^^ (4 - 1))),
6.87 +(([4], Res), 2 * x ^^^ (2 - 1) + cos (x ^^^ 4) * (4 * x ^^^ (4 - 1))),
6.88 +(([5], Res), 2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3),
6.89 +(([], Res), 2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3)] *)
6.90 +
7.1 --- a/test/Tools/isac/Interpret/generate.sml Fri May 25 09:58:20 2012 +0200
7.2 +++ b/test/Tools/isac/Interpret/generate.sml Fri May 25 16:30:15 2012 +0200
7.3 @@ -38,7 +38,7 @@
7.4 val pos as (p, _) = get_pos cI 1;
7.5 val fillforms = find_fillpatterns (pt, pos) errpatID;
7.6
7.7 -if pos = ([1], Res) then () else error "requestFillformula changed 1";
7.8 +if pos = ([1], Res) then () else error "generate_inconsistent_rew changed 1";
7.9
7.10 val (_, fillform, thm, sube_opt) :: _ = filter ((curry op = fillpatID) o
7.11 (#1: (fillpatID * term * thm * (subs option) -> fillpatID))) fillforms;
7.12 @@ -50,9 +50,9 @@
7.13 val f = get_curr_formula (pt, pos);
7.14 val pos' as (p', _) = (lev_on p, Res);
7.15
7.16 -if pos = ([1], Res) then () else error "requestFillformula changed 2a";
7.17 +if pos = ([1], Res) then () else error "generate_inconsistent_rew changed 2a";
7.18 if term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"
7.19 - then () else error "requestFillformula changed 2b";
7.20 + then () else error "generate_inconsistent_rew changed 2b";
7.21
7.22 val (pt,c) =
7.23 case subs_opt of
7.24 @@ -60,19 +60,24 @@
7.25 (Rewrite thm') (f', []) Inconsistent
7.26 | SOME subs => cappend_atomic pt p' (is, insert_assumptions [] ctxt) f
7.27 (Rewrite_Inst (subs, thm')) (f', []) Inconsistent
7.28 - val pt = update_branch pt p TransitiveB;
7.29 + val pt = update_branch pt p' TransitiveB;
7.30 +
7.31 +if get_obj g_tac pt p' = Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", ""))
7.32 + andalso pos = ([1], Res) andalso pos' = ([2], Res) andalso p' = [2]
7.33 +then () else error "generate_inconsistent_rew changed 3";
7.34
7.35 "~~~~~ to requestFillformula return val:"; val (pt, pos') = (pt, pos');
7.36 (*val (pt, pos') = generate_inconsistent_rew (sube_opt, thm'_of_thm thm)
7.37 (fillform, []) (get_loc pt pos) pos' pt*)
7.38 upd_calc cI ((pt, pos'), []); upd_ipos cI 1 pos';
7.39 -autocalculateOK2xml cI pos pos' pos';
7.40
7.41 "~~~~~ final check:";
7.42 -val ((pt,pos),_) = get_calc 1;
7.43 +val ((pt, _),_) = get_calc 1;
7.44 val p = get_pos 1 1;
7.45 -val (Form f, tac, asms) = pt_extract (pt, p);
7.46 -if p = ([2], Res) andalso term2str f =
7.47 +val (Form f, _, asms) = pt_extract (pt, p);
7.48 +if p = ([2], Res) andalso
7.49 + get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", "")) andalso
7.50 + term2str f =
7.51 "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.52 then () else error "";
7.53
8.1 --- a/test/Tools/isac/Interpret/inform.sml Fri May 25 09:58:20 2012 +0200
8.2 +++ b/test/Tools/isac/Interpret/inform.sml Fri May 25 16:30:15 2012 +0200
8.3 @@ -1030,3 +1030,84 @@
8.4 "#fill-all#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) = d_d x (x ^^^ 2) + ?_dummy_1#"
8.5 then () else error "find_fillpatterns changed 4";
8.6
8.7 +"--------- build fun is_exactly_equal, inputFillFormula ----------";
8.8 +"--------- build fun is_exactly_equal, inputFillFormula ----------";
8.9 +"--------- build fun is_exactly_equal, inputFillFormula ----------";
8.10 +states := [];
8.11 +CalcTree
8.12 +[(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
8.13 + ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
8.14 +Iterator 1;
8.15 +moveActiveRoot 1;
8.16 +autoCalculate 1 CompleteCalcHead;
8.17 +autoCalculate 1 (Step 1);
8.18 +autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
8.19 +appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)"; (*<<<<<<<=========================*)
8.20 +(* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),
8.21 + would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well.
8.22 + results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>
8.23 + instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)
8.24 + val ((pt,pos), _) = get_calc 1;
8.25 + val p = get_pos 1 1;
8.26 + val (Form f, _, asms) = pt_extract (pt, p);
8.27 +
8.28 + if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
8.29 + get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sum", "Diff.diff_sum"(*?!?*)))
8.30 + then () else error "embed fun get_fillform changed 1";
8.31 +
8.32 +findFillpatterns 1 "chain-rule-diff-both"; (*<<<<<<<=================================*)
8.33 +(*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =
8.34 + d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *)
8.35 + val ((pt,pos),_) = get_calc 1;
8.36 + val p = get_pos 1 1;
8.37 +
8.38 + val (Form f, _, asms) = pt_extract (pt, p);
8.39 + if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
8.40 + get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sum", "Diff.diff_sum"(*?!?*)))
8.41 + then ()
8.42 + else error "embed fun get_fillform changed 2";
8.43 +
8.44 +requestFillformula 1 ("chain-rule-diff-both", "fill-both-args");(*<<<<<<<============*)
8.45 + (*<AUTOCALC> ([1], Res) ([2], Res) ([2], Res) </AUTOCALC>*)
8.46 + val ((pt,pos),_) = get_calc 1;
8.47 + val p = get_pos 1 1;
8.48 + val (Form f, _, asms) = pt_extract (pt, p);
8.49 + if p = ([1], Res) andalso existpt [2] pt andalso
8.50 + term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
8.51 + get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sum", "Diff.diff_sum"))
8.52 + then () else error "embed fun get_fillform changed 3";
8.53 +
8.54 +(* input a formula which exactly fills the gaps in a "fillformula"
8.55 + presented to the learner immediately before by "requestFillformula (errpatID, fillpatID)":
8.56 + errpatID: lhs of the respective thm = lhs of fillformula with fillpatID.
8.57 + the respective thm is in the ctree ................
8.58 +*)
8.59 +"~~~~~ fun inputFillFormula, args:"; val (cI, ifo) =
8.60 + (1, "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)");
8.61 + val ((pt, _), _) = get_calc cI
8.62 + val pos = get_pos cI 1;
8.63 +
8.64 +"~~~~~ fun is_exactly_equal, args:"; val ((pt, pos as (p, p_)), istr) = ((pt, pos), ifo);
8.65 + val SOME ifo = parseNEW (assoc_thy "Isac" |> thy2ctxt) istr
8.66 + val p' = lev_on p;
8.67 + val tac = get_obj g_tac pt p';
8.68 + if tac = Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", "")) then ()
8.69 + else error "inputFillFormula changed 10";
8.70 + val Appl rew = applicable_in pos pt tac;
8.71 + val Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) = rew;
8.72 +
8.73 +"~~~~~ to inputFillFormula return val:"; val ("ok", tac) = ("ok", tac);
8.74 + val ("ok", (_, c, ptp as (_,p'))) = locatetac tac (pt, pos);
8.75 + upd_calc cI (ptp, []);
8.76 + upd_ipos cI 1 p';
8.77 + autocalculateOK2xml cI pos (if null c then p' else last_elem c) p';
8.78 +
8.79 +"~~~~~ final check:";
8.80 +val ((pt, _),_) = get_calc 1;
8.81 +val p = get_pos 1 1;
8.82 +val (Form f, _, asms) = pt_extract (pt, p);
8.83 +if p = ([2], Res) andalso
8.84 + term2str f = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)" andalso
8.85 + get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", ""))
8.86 +then () else error "inputFillFormula changed 11";
8.87 +
9.1 --- a/test/Tools/isac/Test_Some.thy Fri May 25 09:58:20 2012 +0200
9.2 +++ b/test/Tools/isac/Test_Some.thy Fri May 25 16:30:15 2012 +0200
9.3 @@ -1,7 +1,7 @@
9.4
9.5 theory Test_Some imports Isac begin
9.6
9.7 -use"../../../test/Tools/isac/Interpret/inform.sml"
9.8 +use"../../../test/Tools/isac/Frontend/interface.sml"
9.9
9.10 ML {*
9.11 val thy = @{theory "Isac"};
9.12 @@ -10,101 +10,7 @@
9.13 *}
9.14 ML {*
9.15 *}
9.16 -ML {* (*================== --> test/../inform.sml*)
9.17 -"--------- UC errpat, fillpat ---------------------------"; (*--> test/../interface.sml*)
9.18 -"--------- build fun is_exactly_equal, .....----------------------"; (*--> test/../inform.sml*)
9.19 -"--------- build fun is_exactly_equal, .....----------------------"; (*--> test/../inform.sml*)
9.20 -states := [];
9.21 -CalcTree
9.22 -[(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
9.23 - ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
9.24 -Iterator 1;
9.25 -moveActiveRoot 1;
9.26 -autoCalculate 1 CompleteCalcHead;
9.27 -autoCalculate 1 (Step 1);
9.28 -autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
9.29 -appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)"; (*<<<<<<<=========================*)
9.30 -(* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),
9.31 - would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well.
9.32 - results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>
9.33 - instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)
9.34 - val ((pt,pos), _) = get_calc 1;
9.35 - val p = get_pos 1 1;
9.36 - val (Form f, tac, asms) = pt_extract (pt, p);
9.37 - if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" then ()
9.38 - else error "embed fun get_fillform changed 1";
9.39 -
9.40 -findFillpatterns 1 "chain-rule-diff-both"; (*<<<<<<<=================================*)
9.41 -(*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =
9.42 - d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *)
9.43 - val ((pt,pos),_) = get_calc 1;
9.44 - val p = get_pos 1 1;
9.45 -
9.46 - val (Form f, tac, asms) = pt_extract (pt, p);
9.47 - if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" then ()
9.48 - else error "embed fun get_fillform changed 2";
9.49 -
9.50 -*}
9.51 -ML {*
9.52 -requestFillformula 1 ("chain-rule-diff-both", "fill-both-args");(*<<<<<<<============*)
9.53 - (*<AUTOCALC> ([1], Res) ([2], Res) ([2], Res) </AUTOCALC>*)
9.54 - val ((pt,pos),_) = get_calc 1;
9.55 - val p = get_pos 1 1;
9.56 - val (Form f, tac, asms) = pt_extract (pt, p);
9.57 -*}
9.58 -ML {*
9.59 -*}
9.60 -ML {*
9.61 -*}
9.62 -text {*
9.63 - if p = ([1], Res) andalso existpt [2] pt andalso
9.64 - term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
9.65 - tac = SOME (Rewrite ("fill-both-args", "")) then ()
9.66 - else error "embed fun get_fillform changed 3";
9.67 -*}
9.68 -ML {*
9.69 -(* input a formula which exactly fills the gaps in a "fillformula"
9.70 - presented to the learner immediately before by "requestFillformula (errpatID, fillpatID)":
9.71 - errpatID: lhs of the respective thm = lhs of fillformula with fillpatID.
9.72 - the respective thm is in the ctree ................
9.73 -*)
9.74 -"~~~~~ fun inputFillFormula, args:"; val (cI, ifo) =
9.75 - (1, "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)");
9.76 - val ((pt, _), _) = get_calc cI
9.77 - val pos as (p, p_) = get_pos cI 1;
9.78 -"~~~~~ fun is_exactly_equal, args:"; val () = ();
9.79 -
9.80 -*}
9.81 -text {*
9.82 -print_depth 999;
9.83 -get_obj g_tac pt (lev_on p);
9.84 -print_depth 999;
9.85 -*}
9.86 -ML {*
9.87 -Rewrite_Inst';
9.88 -("",""): thm';
9.89 -*}
9.90 -ML {*
9.91 -val Appl (rewtac as Rewrite' (_, _, _, _, _, _, (res, _))) =
9.92 - applicable_in pos pt (Rewrite ("diff_sin_chain", "")); (*get*)
9.93 -*}
9.94 -text {*
9.95 -(thmID_of_derivation_name o Thm.get_name_hint) thm;
9.96 -thmID_of_derivation_name
9.97 -*}
9.98 -ML {*
9.99 -Thm.get_name_hint;
9.100 -Thm.derivation_name;
9.101 -*}
9.102 -ML {*
9.103 -*}
9.104 -ML {*
9.105 -*}
9.106 -ML {*
9.107 -*}
9.108 -ML {*
9.109 -*}
9.110 -ML {*
9.111 +ML {* (*==================*)
9.112 *}
9.113 ML {*
9.114 *}
9.115 @@ -112,8 +18,6 @@
9.116 *}
9.117 ML {*
9.118 *}
9.119 -ML {*
9.120 -*}
9.121 ML {* (*==================*)
9.122 "~~~~~ fun , args:"; val () = ();
9.123 "~~~~~ to return val:"; val () = ();