1.1 --- a/src/Tools/isac/Frontend/interface.sml Mon May 14 14:47:45 2012 +0200
1.2 +++ b/src/Tools/isac/Frontend/interface.sml Wed May 16 08:59:09 2012 +0200
1.3 @@ -525,40 +525,25 @@
1.4 in matchpbl2xml cI chd end)
1.5 handle _ => sysERROR2xml cI "error in kernel";
1.6
1.7 -(* val (cI, ifo) = (1, "-2 * 1 + (1 + x) = 0");
1.8 - val (cI, ifo) = (1, "x = 2");
1.9 - val (cI, ifo) = (1, "[x = 3 + -2*1]");
1.10 - val (cI, ifo) = (1, "-1 + x = 0");
1.11 - val (cI, ifo) = (1, "x - 4711 = 0");
1.12 - val (cI, ifo) = (1, "2+ -1 + x = 2");
1.13 - val (cI, ifo) = (1, " x - ");
1.14 - val (cI, ifo) = (1, "(-3 * x + 4 * y + -1 * x * y) / (x * y)");
1.15 - val (cI, ifo) = (1, "(4 * y + -3 * x) / (x * y) + -1");
1.16 - *)
1.17 +(* append a formula to the calculation *)
1.18 fun appendFormula cI (ifo:cterm') =
1.19 - (let val cs = get_calc cI
1.20 - val pos as (_,p_) = get_pos cI 1
1.21 - in case step pos cs of
1.22 -(* val (str, cs') = step pos cs;
1.23 - *)
1.24 + (let
1.25 + val cs = get_calc cI
1.26 + val pos as (_,p_) = get_pos cI 1
1.27 + in
1.28 + case step pos cs of
1.29 ("ok", cs') =>
1.30 - (case inform cs' (encode ifo) of
1.31 -(* val (str, (_, c, ptp as (_,p))) = inform cs' (encode ifo);
1.32 - *)
1.33 - ("ok", (_(*use in DG !!!*), c, ptp as (_,p))) =>
1.34 - (upd_calc cI (ptp, []); upd_ipos cI 1 p;
1.35 - appendformulaOK2xml cI pos (if null c then pos
1.36 - else last_elem c) p)
1.37 - | ("same-formula", (_, c, ptp as (_,p))) =>
1.38 - (upd_calc cI (ptp, []); upd_ipos cI 1 p;
1.39 - appendformulaOK2xml cI pos (if null c then pos
1.40 - else last_elem c) p)
1.41 - | (msg, _) => appendformulaERROR2xml cI msg)
1.42 + (case inform cs' (encode ifo) of
1.43 + ("ok", (_(*use in DG !!!*), c, ptp as (_,p))) =>
1.44 + (upd_calc cI (ptp, []); upd_ipos cI 1 p;
1.45 + appendformulaOK2xml cI pos (if null c then pos else last_elem c) p)
1.46 + | ("same-formula", (_, c, ptp as (_,p))) =>
1.47 + (upd_calc cI (ptp, []); upd_ipos cI 1 p;
1.48 + appendformulaOK2xml cI pos (if null c then pos else last_elem c) p)
1.49 + | (msg, _) => appendformulaERROR2xml cI msg)
1.50 | (msg, cs') => appendformulaERROR2xml cI msg
1.51 - end)
1.52 - handle _ => sysERROR2xml cI "error in kernel";
1.53 -
1.54 -
1.55 + end)
1.56 + handle _ => sysERROR2xml cI "error in kernel";
1.57
1.58 (* replace a formula with_in_ a calculation;
1.59 this situation applies for initial CAS-commands, too *)
2.1 --- a/src/Tools/isac/Interpret/inform.sml Mon May 14 14:47:45 2012 +0200
2.2 +++ b/src/Tools/isac/Interpret/inform.sml Wed May 16 08:59:09 2012 +0200
2.3 @@ -604,7 +604,7 @@
2.4 | _ => e_term (*on PblObj is fo <> ifo*);
2.5 val {nrls, ...} = get_met (get_obj g_metID pt (par_pblobj pt p))
2.6 val {rew_ord, erls, rules, ...} = rep_rls nrls
2.7 - val (found, der) = concat_deriv rew_ord erls rules fo ifo;
2.8 + val (found, der) = concat_deriv rew_ord erls rules fo ifo; (*<---------------*)
2.9 in
2.10 if found
2.11 then
2.12 @@ -617,48 +617,85 @@
2.13 then ("no derivation found", (tacis, c, ptp): calcstate')
2.14 else
2.15 let
2.16 - val cs' as (tacis, c', ptp) = nxt_solve_ ptp;
2.17 + val cs' as (tacis, c', ptp) = nxt_solve_ ptp; (*<---------------------*)
2.18 val cs' as (tacis, c'', ptp) =
2.19 case tacis of
2.20 ((Subproblem _, _, _)::_) =>
2.21 let
2.22 val ptp as (pt, (p,_)) = all_modspec ptp
2.23 val mI = get_obj g_metID pt p
2.24 - in nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt))
2.25 - (e_istate, e_ctxt) ptp
2.26 + in
2.27 + nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt)) (e_istate, e_ctxt) ptp
2.28 end
2.29 | _ => cs';
2.30 in compare_step (tacis, c @ c' @ c'', ptp) ifo end
2.31 end;
2.32
2.33 +(* error patterns and fill patterns *)
2.34 +type errpatID = string
2.35 +type fillpatID = string
2.36 +type errpat =
2.37 + errpatID (* one identifier for a list of patterns *)
2.38 + * term list (* error patterns *)
2.39 + * thm list (* thms related to error patterns;
2.40 + note that respective lhs do not match
2.41 + (which reflects student's error) *)
2.42 +val e_errpat = ("e_errpatID", [parse_patt @{theory} "?a = ?b"], [@{thm refl}]): errpat
2.43 +
2.44 +(* check if (agreed result, input formula) matches an error pattern modulo simplifier rls*)
2.45 +fun check_err_patt (res, inf) (errpatID: errpatID, pat) rls =
2.46 + let
2.47 + val (res', _, _, rewritten) =
2.48 + rew_sub (Isac()) 1 [] e_rew_ord e_rls false [] (Trueprop $ pat) res;
2.49 + in
2.50 + if rewritten
2.51 + then
2.52 + let
2.53 + val norm_res = case rewrite_set_ (Isac()) false rls res' of
2.54 + NONE => res'
2.55 + | SOME (norm_res, _) => norm_res
2.56 + val norm_inf = case rewrite_set_ (Isac()) false rls inf of
2.57 + NONE => inf
2.58 + | SOME (norm_inf, _) => norm_inf
2.59 + in if norm_res = norm_inf then SOME errpatID else NONE
2.60 + end
2.61 + else NONE
2.62 + end;
2.63 +
2.64 (*.handle a user-input formula, which may be a CAS-command, too.
2.65 CAS-command:
2.66 create a calchead, and do 1 step
2.67 TOOODO.WN0602 works only for the root-problem !!!
2.68 formula, which is no CAS-command:
2.69 compare iform with calc-tree.form at pos by equ_nrls and all subsequent pos;
2.70 - collect all the tacs applied by the way.*)
2.71 -(*structure copied from autocalc*)
2.72 + collect all the tacs applied by the way;
2.73 + if "no derivation found" then check_error_patterns.*)
2.74 fun inform (cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate') istr =
2.75 - case parse (assoc_thy "Isac") istr of
2.76 - SOME ifo =>
2.77 - let val ifo = term_of ifo
2.78 - val fo = case p_ of Frm => get_obj g_form pt p
2.79 - | Res => (fst o (get_obj g_result pt)) p
2.80 - | _ => #3 (get_obj g_origin pt p)
2.81 - in if fo = ifo
2.82 - then ("same-formula", cs)
2.83 - (*thus ctree not cut with replaceFormula!*)
2.84 - else case cas_input ifo of
2.85 -(* val SOME (pt, _) = cas_input ifo;
2.86 - *)
2.87 - SOME (pt, _) => ("ok",([],[],(pt, (p, Met))))
2.88 - | NONE =>
2.89 - compare_step ([],[],(pt,
2.90 - (*last step re-calc in compare_step TODO*)
2.91 - lev_back pos)) ifo
2.92 - end
2.93 - | NONE => ("syntax error in '"^istr^"'", e_calcstate');
2.94 + case parse (assoc_thy "Isac") istr of
2.95 + SOME ifo =>
2.96 + let
2.97 + val ifo = term_of ifo
2.98 + val fo =
2.99 + case p_ of
2.100 + Frm => get_obj g_form pt p
2.101 + | Res => (fst o (get_obj g_result pt)) p
2.102 + | _ => #3 (get_obj g_origin pt p)
2.103 + in
2.104 + if fo = ifo
2.105 + then ("same-formula", cs) (* ctree not cut with replaceFormula *)
2.106 + else
2.107 + case cas_input ifo of
2.108 + SOME (pt, _) => ("ok",([], [], (pt, (p, Met))))
2.109 + | NONE =>
2.110 + let val msg_calcstate' = compare_step ([], [], (pt, lev_back pos)) ifo
2.111 + (*last step re-calc in compare_step TODO before WN09*)
2.112 + in
2.113 + case msg_calcstate' of
2.114 + ("no derivation found", _) => msg_calcstate' (*GOON*)
2.115 + | _ => msg_calcstate'
2.116 + end
2.117 + end
2.118 + | NONE => ("syntax error in '"^istr^"'", e_calcstate');
2.119
2.120
2.121 (*------------------------------------------------------------------(**)
3.1 --- a/src/Tools/isac/ProgLang/Tools.thy Mon May 14 14:47:45 2012 +0200
3.2 +++ b/src/Tools/isac/ProgLang/Tools.thy Wed May 16 08:59:09 2012 +0200
3.3 @@ -158,16 +158,17 @@
3.4
3.5 (*.does a pattern match some subterm ?.*)
3.6 fun matchsub thy t pat =
3.7 - let fun matchs (t as Const _) = matches thy t pat
3.8 - | matchs (t as Free _) = matches thy t pat
3.9 - | matchs (t as Var _) = matches thy t pat
3.10 - | matchs (Bound _) = false
3.11 - | matchs (t as Abs (_, _, body)) =
3.12 - if matches thy t pat then true else matches thy body pat
3.13 - | matchs (t as f1 $ f2) =
3.14 - if matches thy t pat then true
3.15 - else if matchs f1 then true else matchs f2
3.16 - in matchs t end;
3.17 + let
3.18 + fun matchs (t as Const _) = matches thy t pat
3.19 + | matchs (t as Free _) = matches thy t pat
3.20 + | matchs (t as Var _) = matches thy t pat
3.21 + | matchs (Bound _) = false
3.22 + | matchs (t as Abs (_, _, body)) =
3.23 + if matches thy t pat then true else matches thy body pat
3.24 + | matchs (t as f1 $ f2) =
3.25 + if matches thy t pat then true
3.26 + else if matchs f1 then true else matchs f2
3.27 + in matchs t end;
3.28
3.29 (*("matchsub",("Tools.matchsub",eval_matchsub "#matchsub_")):calc*)
3.30 fun eval_matchsub (thmid:string) "Tools.matchsub"
4.1 --- a/test/Tools/isac/Interpret/inform.sml Mon May 14 14:47:45 2012 +0200
4.2 +++ b/test/Tools/isac/Interpret/inform.sml Wed May 16 08:59:09 2012 +0200
4.3 @@ -31,6 +31,7 @@
4.4 "--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
4.5 "--------- Take as 1st tac, start from exp -----------------------";
4.6 "--------- init_form, start with <NEW> (CAS input) ---------------";
4.7 +"--------- build fun check_err_patt ------------------------------";
4.8 "-----------------------------------------------------------------";
4.9 "-----------------------------------------------------------------";
4.10 "-----------------------------------------------------------------";
4.11 @@ -786,3 +787,47 @@
4.12 [[from sml: </SYSERROR>
4.13 [[from sml: @@@@@end@@@@@*)
4.14 (*step into getFormulaeFromTo --- bug corrected...*)
4.15 +
4.16 +"--------- build fun check_err_patt ------------------------------";
4.17 +"--------- build fun check_err_patt ------------------------------";
4.18 +"--------- build fun check_err_patt ------------------------------";
4.19 +val rls = norm_Rational
4.20 +val pat = parse_patt @{theory} "(?a + ?b)/(?b + ?c) = ?a / ?c";
4.21 +val (res, inf) = (str2term "(2 + 3)/(3 + 4)", str2term "2 / 4");
4.22 +val (res, inf) = (str2term "(2 + 3)/(3 + 4)", str2term "1 / 2");
4.23 +
4.24 +val (res', _, _, rewritten) =
4.25 + rew_sub thy 1 [] e_rew_ord e_rls false [] (Trueprop $ pat) res;
4.26 +if rewritten then NONE else SOME "e_errpatID";
4.27 +
4.28 +val norm_res = case rewrite_set_ (Isac()) false rls res' of
4.29 + NONE => res'
4.30 +| SOME (norm_res, _) => norm_res
4.31 +
4.32 +val norm_inf = case rewrite_set_ (Isac()) false rls inf of
4.33 + NONE => inf
4.34 +| SOME (norm_inf, _) => norm_inf;
4.35 +
4.36 +res' = inf;
4.37 +norm_res = norm_inf;
4.38 +
4.39 +val pat = parse_patt @{theory} "(?a + ?b)/?a = ?b";
4.40 +val (res, inf) = (str2term "(2 + 3)/2", str2term "3");
4.41 +if check_err_patt (res, inf) ("errpatID", pat) rls = SOME "errpatID"
4.42 +then () else error "error patt example1 changed";
4.43 +
4.44 +val pat = parse_patt @{theory} "(?a + ?b)/(?a + ?c) = ?b / ?c";
4.45 +val (res, inf) = (str2term "(2 + 3)/(2 + 4)", str2term "3 / 4");
4.46 +if check_err_patt (res, inf) ("errpatID", pat) rls = SOME "errpatID"
4.47 +then () else error "error patt example2 changed";
4.48 +
4.49 +val pat = parse_patt @{theory} "(?a + ?b)/(?b + ?c) = ?a / ?c";
4.50 +val (res, inf) = (str2term "(2 + 3)/(3 + 4)", str2term "2 / 4");
4.51 +if check_err_patt (res, inf) ("errpatID", pat) rls = SOME "errpatID"
4.52 +then () else error "error patt example3 changed";
4.53 +
4.54 +val inf = str2term "1 / 2";
4.55 +if check_err_patt (res, inf) ("errpatID", pat) rls = SOME "errpatID"
4.56 +then () else error "error patt example3 changed";
4.57 +
4.58 +
5.1 --- a/test/Tools/isac/Test_Some.thy Mon May 14 14:47:45 2012 +0200
5.2 +++ b/test/Tools/isac/Test_Some.thy Wed May 16 08:59:09 2012 +0200
5.3 @@ -1,25 +1,116 @@
5.4
5.5 theory Test_Some imports Isac begin
5.6
5.7 -use"../../../test/Tools/isac/Knowledge/Inverse_Z_Transform/inverse_z_transform.sml"
5.8 +use"../../../test/Tools/isac/Interpret/inform.sml"
5.9
5.10 ML {*
5.11 val thy = @{theory "Isac"};
5.12 val ctxt = ProofContext.init_global thy;
5.13 print_depth 5;
5.14 *}
5.15 +ML {*
5.16 +*}
5.17 ML {* (*==================*)
5.18 *}
5.19 ML {*
5.20 *}
5.21 ML {*
5.22 *}
5.23 -ML {* (*==================*)
5.24 +ML {*
5.25 *}
5.26 ML {*
5.27 *}
5.28 ML {*
5.29 *}
5.30 +ML {*
5.31 +*}
5.32 +ML {* (*==================*)
5.33 +states:=[];
5.34 +CalcTree
5.35 +[(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
5.36 + ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
5.37 +Iterator 1;
5.38 +moveActiveRoot 1;
5.39 +autoCalculate 1 CompleteCalcHead;
5.40 +autoCalculate 1 (Step 1);
5.41 +autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
5.42 +(*autoCalculate 1 (Step 1);([2], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)*)
5.43 +*}
5.44 +ML {*
5.45 +"~~~~~ fun appendFormula, args:"; val (cI, (ifo:cterm')) = (1, "d_d x (x ^ 2) + cos (4 * x ^ 3)");
5.46 +val cs = get_calc cI
5.47 +val pos as (_,p_) = get_pos cI 1; (*pos = ([1], Res)*)
5.48 +val cs' =
5.49 + case step pos cs of
5.50 + ("ok", cs') => cs';
5.51 +
5.52 +val (_, _, (pt, ([2], Res))) = cs';
5.53 +(*show_pt pt;
5.54 + [(([], Frm), Diff (x ^^^ 2 + sin (x ^^^ 4), x)),
5.55 + (([1], Frm), d_d x (x ^^^ 2 + sin (x ^^^ 4))),
5.56 + (([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))),
5.57 + (([2], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4))] *)
5.58 +
5.59 +"~~~~~ fun inform, args:"; val ((cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate'), istr) =
5.60 + (cs', (encode ifo));
5.61 +val SOME ifo = parse (assoc_thy "Isac") istr
5.62 +val ifo = term_of ifo
5.63 +val fo =
5.64 + case p_ of
5.65 + Frm => get_obj g_form pt p
5.66 + | Res => (fst o (get_obj g_result pt)) p
5.67 + | _ => #3 (get_obj g_origin pt p);
5.68 +(*term2str fo = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)"*)
5.69 +fo = ifo; (* = false*)
5.70 +cas_input ifo; (* = NONE*)
5.71 +
5.72 +"~~~~~ fun compare_step, args:"; val (((tacis, c, ptp as (pt, pos as (p,p_))): calcstate'), ifo) =
5.73 + (([], [], (pt, lev_back pos)), ifo);
5.74 +*}
5.75 +ML {*
5.76 + val fo =
5.77 + case p_ of
5.78 + Frm => get_obj g_form pt p
5.79 + | Res => (fst o (get_obj g_result pt)) p
5.80 + | _ => e_term (*on PblObj is fo <> ifo*);
5.81 +*}
5.82 +ML {*
5.83 +*}
5.84 +ML {*
5.85 +*}
5.86 +ML {*
5.87 +compare_step;
5.88 +e_calcstate';
5.89 +*}
5.90 +ML {*
5.91 +
5.92 +*}
5.93 +text {*
5.94 +compare_step ([], [], (pt, lev_back pos)) ifo; (*("no derivation found", ([(...*)
5.95 +inform cs' (encode ifo);(*("no derivation found", ([(...*)
5.96 +step pos cs; (*("ok", ([(..., ...*)
5.97 +appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)";
5.98 + (*<CALCMESSAGE> no derivation found </CALCMESSAGE> --> error pattern #chain-rule-diff-both#*)
5.99 +*}
5.100 +ML {*
5.101 +*}
5.102 +ML {*
5.103 +*}
5.104 +ML {*
5.105 +val ((pt,p),_) = get_calc 1; show_pt pt;
5.106 +*}
5.107 +text {*
5.108 +val ((pt,p),_) = get_calc 1; show_pt pt;
5.109 +if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) =
5.110 + "2 * x + cos (3 * x ^^^ 4) * 12 * x ^^^ 3" then ()
5.111 +else error "check_error_pattern changed";
5.112 +*}
5.113 +ML {*
5.114 +*}
5.115 +ML {* (*==================*)
5.116 +*}
5.117 +ML {*
5.118 +*}
5.119 ML {* (*==================*)
5.120 "~~~~~ fun , args:"; val () = ();
5.121 "~~~~~ to return val:"; val () = ();