1.1 --- a/src/Tools/isac/Interpret/inform.sml Mon May 14 14:47:45 2012 +0200
1.2 +++ b/src/Tools/isac/Interpret/inform.sml Wed May 16 08:59:09 2012 +0200
1.3 @@ -604,7 +604,7 @@
1.4 | _ => e_term (*on PblObj is fo <> ifo*);
1.5 val {nrls, ...} = get_met (get_obj g_metID pt (par_pblobj pt p))
1.6 val {rew_ord, erls, rules, ...} = rep_rls nrls
1.7 - val (found, der) = concat_deriv rew_ord erls rules fo ifo;
1.8 + val (found, der) = concat_deriv rew_ord erls rules fo ifo; (*<---------------*)
1.9 in
1.10 if found
1.11 then
1.12 @@ -617,48 +617,85 @@
1.13 then ("no derivation found", (tacis, c, ptp): calcstate')
1.14 else
1.15 let
1.16 - val cs' as (tacis, c', ptp) = nxt_solve_ ptp;
1.17 + val cs' as (tacis, c', ptp) = nxt_solve_ ptp; (*<---------------------*)
1.18 val cs' as (tacis, c'', ptp) =
1.19 case tacis of
1.20 ((Subproblem _, _, _)::_) =>
1.21 let
1.22 val ptp as (pt, (p,_)) = all_modspec ptp
1.23 val mI = get_obj g_metID pt p
1.24 - in nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt))
1.25 - (e_istate, e_ctxt) ptp
1.26 + in
1.27 + nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt)) (e_istate, e_ctxt) ptp
1.28 end
1.29 | _ => cs';
1.30 in compare_step (tacis, c @ c' @ c'', ptp) ifo end
1.31 end;
1.32
1.33 +(* error patterns and fill patterns *)
1.34 +type errpatID = string
1.35 +type fillpatID = string
1.36 +type errpat =
1.37 + errpatID (* one identifier for a list of patterns *)
1.38 + * term list (* error patterns *)
1.39 + * thm list (* thms related to error patterns;
1.40 + note that respective lhs do not match
1.41 + (which reflects student's error) *)
1.42 +val e_errpat = ("e_errpatID", [parse_patt @{theory} "?a = ?b"], [@{thm refl}]): errpat
1.43 +
1.44 +(* check if (agreed result, input formula) matches an error pattern modulo simplifier rls*)
1.45 +fun check_err_patt (res, inf) (errpatID: errpatID, pat) rls =
1.46 + let
1.47 + val (res', _, _, rewritten) =
1.48 + rew_sub (Isac()) 1 [] e_rew_ord e_rls false [] (Trueprop $ pat) res;
1.49 + in
1.50 + if rewritten
1.51 + then
1.52 + let
1.53 + val norm_res = case rewrite_set_ (Isac()) false rls res' of
1.54 + NONE => res'
1.55 + | SOME (norm_res, _) => norm_res
1.56 + val norm_inf = case rewrite_set_ (Isac()) false rls inf of
1.57 + NONE => inf
1.58 + | SOME (norm_inf, _) => norm_inf
1.59 + in if norm_res = norm_inf then SOME errpatID else NONE
1.60 + end
1.61 + else NONE
1.62 + end;
1.63 +
1.64 (*.handle a user-input formula, which may be a CAS-command, too.
1.65 CAS-command:
1.66 create a calchead, and do 1 step
1.67 TOOODO.WN0602 works only for the root-problem !!!
1.68 formula, which is no CAS-command:
1.69 compare iform with calc-tree.form at pos by equ_nrls and all subsequent pos;
1.70 - collect all the tacs applied by the way.*)
1.71 -(*structure copied from autocalc*)
1.72 + collect all the tacs applied by the way;
1.73 + if "no derivation found" then check_error_patterns.*)
1.74 fun inform (cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate') istr =
1.75 - case parse (assoc_thy "Isac") istr of
1.76 - SOME ifo =>
1.77 - let val ifo = term_of ifo
1.78 - val fo = case p_ of Frm => get_obj g_form pt p
1.79 - | Res => (fst o (get_obj g_result pt)) p
1.80 - | _ => #3 (get_obj g_origin pt p)
1.81 - in if fo = ifo
1.82 - then ("same-formula", cs)
1.83 - (*thus ctree not cut with replaceFormula!*)
1.84 - else case cas_input ifo of
1.85 -(* val SOME (pt, _) = cas_input ifo;
1.86 - *)
1.87 - SOME (pt, _) => ("ok",([],[],(pt, (p, Met))))
1.88 - | NONE =>
1.89 - compare_step ([],[],(pt,
1.90 - (*last step re-calc in compare_step TODO*)
1.91 - lev_back pos)) ifo
1.92 - end
1.93 - | NONE => ("syntax error in '"^istr^"'", e_calcstate');
1.94 + case parse (assoc_thy "Isac") istr of
1.95 + SOME ifo =>
1.96 + let
1.97 + val ifo = term_of ifo
1.98 + val fo =
1.99 + case p_ of
1.100 + Frm => get_obj g_form pt p
1.101 + | Res => (fst o (get_obj g_result pt)) p
1.102 + | _ => #3 (get_obj g_origin pt p)
1.103 + in
1.104 + if fo = ifo
1.105 + then ("same-formula", cs) (* ctree not cut with replaceFormula *)
1.106 + else
1.107 + case cas_input ifo of
1.108 + SOME (pt, _) => ("ok",([], [], (pt, (p, Met))))
1.109 + | NONE =>
1.110 + let val msg_calcstate' = compare_step ([], [], (pt, lev_back pos)) ifo
1.111 + (*last step re-calc in compare_step TODO before WN09*)
1.112 + in
1.113 + case msg_calcstate' of
1.114 + ("no derivation found", _) => msg_calcstate' (*GOON*)
1.115 + | _ => msg_calcstate'
1.116 + end
1.117 + end
1.118 + | NONE => ("syntax error in '"^istr^"'", e_calcstate');
1.119
1.120
1.121 (*------------------------------------------------------------------(**)