1.1 --- a/src/Tools/isac/Interpret/inform.sml	Thu May 17 16:44:13 2012 +0200
     1.2 +++ b/src/Tools/isac/Interpret/inform.sml	Thu May 17 19:09:48 2012 +0200
     1.3 @@ -631,7 +631,7 @@
     1.4  		     in compare_step (tacis, c @ c' @ c'', ptp) ifo end
     1.5    end;
     1.6  
     1.7 -(* check if (agreed result, input formula) matches an error pattern modulo simplifier rls*)
     1.8 +(* check if (agreed result, input formula) matches the error pattern "pat" modulo simplifier rls *)
     1.9  fun check_err_patt (res, inf) (subst: subst) (errpatID: errpatID, pat) rls =
    1.10    let 
    1.11      val (res', _, _, rewritten) =
    1.12 @@ -651,6 +651,23 @@
    1.13      else NONE
    1.14    end;
    1.15  
    1.16 +(* check if (agreed result, input formula) matches SOME error pattern modulo simplifier rls;
    1.17 +   (prog, env) for retrieval of casual substitution for bdv in the pattern. *)
    1.18 +fun check_error_patterns (res, inf) (prog, env) (errpats, rls) =
    1.19 +  let
    1.20 +    val subst = get_bdv_subst prog env
    1.21 +    fun scan (_, [], _) = NONE
    1.22 +      | scan (errpatID, errpat :: errpats, _) =
    1.23 +          case check_err_patt (res, inf) (subst: subst) (errpatID, errpat) rls of
    1.24 +            NONE => scan (errpatID, errpats, [])
    1.25 +          | SOME errpatID => SOME errpatID
    1.26 +    fun scans [] = NONE
    1.27 +      | scans (group :: groups) =
    1.28 +          case scan group of
    1.29 +            NONE => scans groups
    1.30 +          | SOME errpatID => SOME errpatID
    1.31 +  in scans errpats end;
    1.32 +
    1.33  (*.handle a user-input formula, which may be a CAS-command, too.
    1.34  CAS-command:
    1.35     create a calchead, and do 1 step
    1.36 @@ -665,11 +682,7 @@
    1.37  	  SOME f_in =>
    1.38  	    let
    1.39  	      val f_in = term_of f_in
    1.40 -	      val f_succ = (* the formula from "step pos cs" in appendFormula*)
    1.41 -	        case p_ of
    1.42 -	          Frm => get_obj g_form pt p
    1.43 -			    | Res => (fst o (get_obj g_result pt)) p
    1.44 -			    | _ => #3 (get_obj g_origin pt p)
    1.45 +	      val f_succ = get_pred_formula (pt, pos);
    1.46  			in
    1.47  			  if f_succ = f_in
    1.48  			  then ("same-formula", cs) (* ctree not cut with replaceFormula *)
    1.49 @@ -677,23 +690,24 @@
    1.50  			    case cas_input f_in of
    1.51  			      SOME (pt, _) => ("ok",([], [], (pt, (p, Met))))
    1.52  			    | NONE =>
    1.53 -			        let val msg_calcstate' = compare_step ([], [], (pt, lev_back' pos)) f_in
    1.54 +			        let
    1.55 +			          val pos_pred = lev_back' pos
    1.56 +			          (* f_pred ---"step pos cs"---> f_succ in appendFormula *)
    1.57 +			          val f_pred = get_pred_formula (pt, pos_pred)
    1.58 +			          val msg_calcstate' = compare_step ([], [], (pt, pos_pred)) f_in
    1.59  			          (*last step re-calc in compare_step TODO before WN09*)
    1.60  			        in
    1.61  			          case msg_calcstate' of
    1.62  			            ("no derivation found", calcstate') => 
    1.63 -(*GOON
    1.64  			               let
    1.65  			                 val pp = par_pblobj pt p
    1.66  			                 val {errpats, nrls, scr = Script prog, ...} = get_met (get_obj g_metID pt pp)
    1.67  			                 val ScrState (env, _, _, _, _, _) = get_istate pt pos
    1.68  			               in
    1.69 -			                 case check_error_patterns (f_succ, f_in) (prog, env) (errpats, nrls) of
    1.70 +			                 case check_error_patterns (f_pred, f_in) (prog, env) (errpats, nrls) of
    1.71  			                   SOME errpatID => ("error pattern #" ^ errpatID ^ "#", calcstate')
    1.72  			                 | NONE => msg_calcstate'
    1.73  			               end
    1.74 -GOON*)
    1.75 -                       msg_calcstate'
    1.76  			          | _ => msg_calcstate'
    1.77  			        end
    1.78  			end