(* Handle user-input during the specify- and the solve-phase. 

   author: Walther Neuper

   0603

   (c) due to copyright terms

*)

signature INPUT_FORMULAS =

sig

  datatype iitem = Find of Rule.cterm' list | Given of Rule.cterm' list | Relate of Rule.cterm' list

  type imodel = iitem list

  type icalhd = Ctree.pos' * Rule.cterm' * imodel * Ctree.pos_ * Celem.spec

  val fetchErrorpatterns : Tac.tac -> Rule.errpatID list

  val input_icalhd : Ctree.ctree -> icalhd -> Ctree.ctree * Ctree.ocalhd

  val inform : Chead.calcstate' -> string -> string * Chead.calcstate'

  val find_fillpatterns : Ctree.state -> Rule.errpatID -> (Celem.fillpatID * term * thm * Selem.subs option) list

  val is_exactly_equal : Ctree.state -> string -> string * Tac.tac

(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)

  (*  NONE *)

(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )

  val dropwhile' : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list

  val cas_input : term -> (Ctree.ctree * Ctree.ocalhd) option

  val rev_deriv' : 'a * Rule.rule * ('b * 'c) -> 'b * Rule.rule * ('a * 'c)

  val compare_step : Generate.taci list * Ctree.pos' list * (Ctree.state) -> term -> string * Chead.calcstate'

  val check_err_patt : term * term -> Rule.subst -> Rule.errpatID * term -> Rule.rls -> Rule.errpatID option

  val concat_deriv : 'a * ((term * term) list -> term * term -> bool) ->

    Rule.rls -> Rule.rule list -> term -> term -> bool * (term * Rule.rule * (term * term list)) list

  val check_error_patterns :

    term * term ->

    term * (term * term) list -> (Rule.errpatID * term list * 'a list) list * Rule.rls -> Rule.errpatID option

  val get_fillform :

     'a * (term * term) list -> 'b * term -> Rule.errpatID -> Celem.fillpat -> (Celem.fillpatID * term * 'b * 'a) option

  val get_fillpats :

     'a * (term * term) list -> term -> Rule.errpatID -> thm -> (Celem.fillpatID * term * thm * 'a) list

( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

(*----- unused code, kept as hints to design ideas ---------------------------------------------*)

  val e_icalhd : icalhd

  val oris2itms : 'a -> ''b list -> ('c * ''b * 'd * term * term list) list ->

    ('c * ''b * bool * 'd * Model.itm_) list

end

structure Inform(**): INPUT_FORMULAS(**) =

struct

(*** handle an input calc-head ***)

datatype iitem = 

  Given of Rule.cterm' list

(*Where is never input*) 

| Find  of Rule.cterm' list

| Relate  of Rule.cterm' list

type imodel = iitem list

(*calc-head as input*)

type icalhd =

  Ctree.pos' *     (*the position of the calc-head in the calc-tree*) 

  Rule.cterm' *   (*the headline*)

  imodel *         (*the model (without Find) of the calc-head*)

  Ctree.pos_ *     (*model belongs to Pbl or Met*)

  Celem.spec;      (*specification: domID, pblID, metID*)

val e_icalhd = (Ctree.e_pos', "", [Given [""]], Ctree.Pbl, Celem.e_spec)

fun is_casinput (hdf : Rule.cterm') ((fmz_, spec) : Selem.fmz) =

  hdf <> "" andalso fmz_ = [] andalso spec = Celem.e_spec

(*.handle an input as into an algebra system.*)

fun dtss2itm_ ppc (d, ts) =

  let

    val (f, (d, id)) = the (find_first ((curry op= d) o 

  		(#1: (term * term) -> term) o

  		(#2: Celem.pbt_ -> (term * term))) ppc)

  in

    ([1], true, f, Model.Cor ((d, ts), (id, ts)))

  end

fun flattup2 (a, (b ,c, d, e)) = (a, b, c, d, e)

fun cas_input_ ((dI, pI, mI): Celem.spec) dtss = (*WN110515 reconsider thy..ctxt*)

  let

    val thy = Celem.assoc_thy dI

	  val {ppc, ...} = Specify.get_pbt pI

	  val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)

	  val its = Specify.add_id its_

	  val pits = map flattup2 its

	  val (pI, mI) =

      if mI <> ["no_met"]

      then (pI, mI)

		  else

        case Specify.refine_pbl thy pI pits of

			    SOME (pI,_) => (pI, (hd o #met o Specify.get_pbt) pI)

			  | NONE => (pI, (hd o #met o Specify.get_pbt) pI)

	  val {ppc, pre, prls, ...} = Specify.get_met mI

	  val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)

	  val its = Specify.add_id its_

	  val mits = map flattup2 its

	  val pre = Stool.check_preconds thy prls pre mits

    val ctxt = Selem.e_ctxt (*WN110515 cas_input_ DOESNT WORK*)

  in (pI, pits, mI, mits, pre, ctxt) end;

(* check if the input term is a CAScmd and return a ctree with a _complete_ calchead *)

fun cas_input hdt =

  let

    val (h, argl) = strip_comb hdt

  in

    case assoc_cas (Celem.assoc_thy "Isac") h of

      NONE => NONE

    | SOME (spec as (dI,_,_), argl2dtss) =>

	      let

          val dtss = argl2dtss argl

	        val (pI, pits, mI, mits, pre, ctxt) = cas_input_ spec dtss

	        val spec = (dI, pI, mI)

	        val (pt,_) = 

		        Ctree.cappend_problem Ctree.e_ctree [] (Selem.e_istate, Selem.e_ctxt) ([], Celem.e_spec) ([], Celem.e_spec, hdt)

	        val pt = Ctree.update_spec pt [] spec

	        val pt = Ctree.update_pbl pt [] pits

	        val pt = Ctree.update_met pt [] mits

	        val pt = Ctree.update_ctxt pt [] ctxt

	      in

	        SOME (pt, (true, Ctree.Met, hdt, mits, pre, spec) : Ctree.ocalhd)

	      end

  end

(*lazy evaluation for (Thy_Info_get_theory "Isac")*)

fun Isac _  = Celem.assoc_thy "Isac";

(* re-parse itms with a new thy and prepare for checking with ori list *)

fun parsitm dI (itm as (i, v, _, f, Model.Cor ((d, ts), _))) =

    (let val t = Model.comp_dts (d, ts)

     val _ = (Rule.term_to_string''' dI t)

     (*t his ^^^^^^^^^^^^ should raise the exn on unability of re-parsing dts *)

    in itm end

    handle _ => (i, v, false, f, Model.Syn (Rule.term2str Rule.e_term (*t  ..(t) has not been declared*))))

  | parsitm dI (i, v, b, f, Model.Syn str) =

    (let val _ = (Thm.term_of o the o (TermC.parse dI)) str

    in (i, v, b ,f, Model.Par str) end

    handle _ => (i, v, b, f, Model.Syn str))

  | parsitm dI (i, v, b, f, Model.Typ str) =

    (let val _ = (Thm.term_of o the o (TermC.parse dI)) str

     in (i, v, b, f, Model.Par str) end

     handle _ => (i, v, b, f, Model.Syn str))

  | parsitm dI (itm as (i, v, _, f, Model.Inc ((d, ts), _))) =

    (let val t = Model.comp_dts (d,ts);

	       val _ = Rule.term_to_string''' dI t;

     (*this    ^ should raise the exn on unability of re-parsing dts*)

     in itm end

     handle _ => (i, v, false, f, Model.Syn (Rule.term2str Rule.e_term (*t  ..(t) has not been declared*))))

  | parsitm dI (itm as (i, v, _, f, Model.Sup (d, ts))) =

    (let val t = Model.comp_dts (d,ts);

	       val _ = Rule.term_to_string''' dI t;

     (*this    ^ should raise the exn on unability of re-parsing dts*)

    in itm end

    handle _ => (i, v, false, f, Model.Syn (Rule.term2str Rule.e_term (*t  ..(t) has not been declared*))))

  | parsitm dI (itm as (i, v, _, f, Model.Mis (d, t'))) =

    (let val t = d $ t';

	       val _ = Rule.term_to_string''' dI t;

     (*this    ^ should raise the exn on unability of re-parsing dts*)

    in itm end

    handle _ => (i, v, false, f, Model.Syn (Rule.term2str Rule.e_term (*t  ..(t) has not been declared*))))

  | parsitm dI (itm as (_, _, _, _, Model.Par _)) = 

    error ("parsitm (" ^ Model.itm2str_ (Rule.thy2ctxt dI) itm ^ "): Par should be internal");

(*separate a list to a pair of elements that do NOT satisfy the predicate,

 and of elements that satisfy the predicate, i.e. (false, true)*)

fun filter_sep pred xs =

  let

    fun filt ab [] = ab

      | filt (a, b) (x :: xs) =

        if pred x 

			  then filt (a, b @ [x]) xs 

			  else filt (a @ [x], b) xs

  in filt ([], []) xs end;

fun is_Par (_, _, _, _, Model.Par _) = true

  | is_Par _ = false;

fun is_e_ts [] = true

  | is_e_ts [Const ("List.list.Nil", _)] = true

  | is_e_ts _ = false;

(* WN.9.11.03 copied from fun appl_add *)

fun appl_add' dI oris ppc pbt (sel, ct) = 

  let 

     val ctxt = Celem.assoc_thy dI |> Rule.thy2ctxt;

  in

    case TermC.parseNEW ctxt ct of

	    NONE => (0, [], false, sel, Model.Syn ct)

	  | SOME t =>

	    (case Chead.is_known ctxt sel oris t of

        ("", ori', all) =>

          (case Chead.is_notyet_input ctxt ppc all ori' pbt of

            ("",itm)  => itm

          | (msg,_) => error ("appl_add': " ^ msg))

      | (_, (i, v, _, d, ts), _) =>

        if is_e_ts ts

        then (i, v, false, sel, Model.Inc ((d, ts), (Rule.e_term, [])))

        else (i, v, false, sel, Model.Sup (d, ts)))

   end

(* generate preliminary itm_ from a strin (with field "#Given" etc.) *)

fun eq7 (f, d) (f', (d', _)) = f = f' andalso d = d';

fun fstr2itm_ thy pbt (f, str) =

  let

    val topt = TermC.parse thy str

  in

    case topt of

      NONE => ([], false, f, Model.Syn str)

    | SOME ct => 

	    let

	      val (d, ts) = (Model.split_dts o Thm.term_of) ct

	      val popt = find_first (eq7 (f, d)) pbt

	    in

	      case popt of

	        NONE => ([1](*??*), true(*??*), f, Model.Sup (d, ts))

	      | SOME (f, (d, id)) => ([1], true, f, Model.Cor ((d, ts), (id, ts))) 

	    end

  end

(*.input into empty PblObj, i.e. empty fmz+origin (unknown example).*)

fun unknown_expl dI pbt selcts =

  let

    val thy = Celem.assoc_thy dI

    val its_ = map (fstr2itm_ thy pbt) selcts (*([1],true,"#Given",Cor (...))*)

    val its = Specify.add_id its_ 

  in map flattup2 its end

(* WN.11.03 for input_icalhd, ~ specify_additem for Add_Given/_Find/_Relation

   appl_add': generate 1 item 

   appl_add' . is_known: parse, get data from oris (vats, all (elems if list)..)

   appl_add' . is_notyet_input: compare with items in model already input

   insert_ppc': insert this 1 item*)

fun appl_adds dI [] _ pbt selcts = unknown_expl dI pbt selcts

    (*already present itms in model are being overwritten*)

  | appl_adds _ _ ppc _ [] = ppc

  | appl_adds dI oris ppc pbt (selct :: ss) =

    let val itm = appl_add' dI oris ppc pbt selct;

    in appl_adds dI oris (Chead.insert_ppc' itm ppc) pbt ss end

fun oris2itms _  _ [] = [] (* WN161130: similar in ptyps ?!? *)

  | oris2itms pbt vat ((i, v, f, d, ts) :: os) =

    if member op = vat v 

    then (i, v, true, f, Model.Cor ((d, ts), (Rule.e_term, []))) :: (oris2itms pbt vat os)

    else oris2itms pbt vat os

fun par2fstr (_, _, _, f, Model.Par s) = (f, s)

  | par2fstr itm = error ("par2fstr: called with " ^ Model.itm2str_ (Rule.thy2ctxt' "Isac") itm)

fun itms2fstr (_, _, _, f, Model.Cor ((d, ts), _)) = (f, Model.comp_dts'' (d, ts))

  | itms2fstr (_, _, _, f, Model.Syn str) = (f, str)

  | itms2fstr (_, _, _, f, Model.Typ str) = (f, str)

  | itms2fstr (_, _, _, f, Model.Inc ((d, ts), _)) = (f, Model.comp_dts'' (d,ts))

  | itms2fstr (_, _, _, f, Model.Sup (d, ts)) = (f, Model.comp_dts'' (d, ts))

  | itms2fstr (_, _, _, f, Model.Mis (d, t)) = (f, Rule.term2str (d $ t))

  | itms2fstr (itm as (_, _, _, _, Model.Par _)) = 

    error ("parsitm (" ^ Model.itm2str_ (Rule.thy2ctxt' "Isac") itm ^ "): Par should be internal");

fun imodel2fstr iitems = 

  let 

    fun xxx is [] = is

	    | xxx is ((Given strs)::iis) = xxx (is @ (map (pair "#Given") strs)) iis

	    | xxx is ((Find strs)::iis) = xxx (is @ (map (pair "#Find") strs)) iis

	    | xxx is ((Relate strs)::iis) = xxx (is @ (map (pair "#Relate") strs)) iis

  in xxx [] iitems end;

(* input a calchead, WN110505 "prep_oris -> (_, ctxt)" not handled properly *)

fun input_icalhd pt (((p, _), hdf, imodel, Ctree.Pbl, spec as (dI, pI, mI)) : icalhd) =

    let

		  val (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth) = case Ctree.get_obj I pt p of

		    Ctree.PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'), 

		      spec = sspec as (sdI, spI, smI), probl, meth, ...}

        => (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth)

      | _ => error "input_icalhd: uncovered case of get_obj I pt p"

    in if is_casinput hdf fmz then the (cas_input (TermC.str2term hdf)) 

       else        (*hacked WN0602 ~~~            ~~~~~~~~~,   ..dropped !*)

         let val (pos_, pits, mits) = 

	         if dI <> sdI

	         then let val its = map (parsitm (Celem.assoc_thy dI)) probl;

			            val (its, trms) = filter_sep is_Par its;

			            val pbt = (#ppc o Specify.get_pbt) (#2 (Chead.some_spec ospec sspec))

		            in (Ctree.Pbl, appl_adds dI oris its pbt  (map par2fstr trms), meth) end 

           else

             if pI <> spI 

	           then if pI = snd3 ospec then (Ctree.Pbl, probl, meth) 

                  else

		                let val pbt = (#ppc o Specify.get_pbt) pI

			                val dI' = #1 (Chead.some_spec ospec spec)

			                val oris = if pI = #2 ospec then oris 

				                         else Specify.prep_ori fmz_(Celem.assoc_thy"Isac") pbt |> #1;

		                in (Ctree.Pbl, appl_adds dI' oris probl pbt 

				              (map itms2fstr probl), meth) end 

             else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)

	                then let val met = (#ppc o Specify.get_met) mI

		                     val mits = Chead.complete_metitms oris probl meth met

		                   in if foldl and_ (true, map #3 mits)

		                      then (Ctree.Pbl, probl, mits) else (Ctree.Met, probl, mits) 

		                   end 

                  else (Ctree.Pbl, appl_adds (#1 (Chead.some_spec ospec spec)) oris [(*!!!*)]

			                  ((#ppc o Specify.get_pbt) (#2 (Chead.some_spec ospec spec)))

			                  (imodel2fstr imodel), meth)

	         val pt = Ctree.update_spec pt p spec;

         in if pos_ = Ctree.Pbl

	          then let val {prls,where_,...} = Specify.get_pbt (#2 (Chead.some_spec ospec spec))

		               val pre = Stool.check_preconds (Celem.assoc_thy"Isac") prls where_ pits

	               in (Ctree.update_pbl pt p pits,

		                 (Chead.ocalhd_complete pits pre spec, Ctree.Pbl, hdf', pits, pre, spec): Ctree.ocalhd) 

                 end

	           else let val {prls,pre,...} = Specify.get_met (#3 (Chead.some_spec ospec spec))

		                val pre = Stool.check_preconds (Celem.assoc_thy"Isac") prls pre mits

	                in (Ctree.update_met pt p mits,

		                  (Chead.ocalhd_complete mits pre spec, Ctree.Met, hdf', mits, pre, spec) : Ctree.ocalhd)

                  end

         end 

    end

  | input_icalhd _ (_, _, _, _(*Met*), _) = error "input_icalhd Met not impl."

(***. handle an input formula .***)

(*the lists contain eq-al elem-pairs at the beginning;

  return first list reverted (again) - ie. in order as required subsequently*)

fun dropwhile' equal (f1::f2::fs) (i1::i2::is) =

    if equal f1 i1

    then

      if equal f2 i2 then dropwhile' equal (f2 :: fs) (i2 :: is)

      else (rev (f1 :: f2 :: fs), i1 :: i2 :: is)

    else error "dropwhile': did not start with equal elements"

  | dropwhile' equal (f::fs) [i] =

    if equal f i

    then (rev (f::fs), [i])

    else error "dropwhile': did not start with equal elements"

  | dropwhile' equal [f] (i::is) =

    if equal f i

    then ([f], i::is)

    else error "dropwhile': did not start with equal elements"

  | dropwhile' _ _ _ = error "dropwhile': uncovered case"

(* 040214: version for concat_deriv *)

fun rev_deriv' (t, r, (t', a)) = (t', Rtools.sym_rule r, (t, a));

fun mk_tacis ro erls (t, r as Rule.Thm (id, thm), (t', a)) = 

      (Tac.Rewrite (id, thm), 

        Tac.Rewrite' ("Isac", fst ro, erls, false, Lucin.rule2thm'' r, t, (t', a)),

       (Ctree.e_pos'(*to be updated before generate tacis!!!*), (Selem.Uistate, Selem.e_ctxt)))

  | mk_tacis _ _ (t, r as Rule.Rls_ rls, (t', a)) = 

      (Tac.Rewrite_Set (Lucin.rule2rls' r), 

        Tac.Rewrite_Set' ("Isac", false, rls, t, (t', a)),

       (Ctree.e_pos'(*to be updated before generate tacis!!!*), (Selem.Uistate, Selem.e_ctxt)))

  | mk_tacis _ _ (t, r, _) = error ("mk_tacis: not impl. for " ^ Rule.rule2str r ^ " at " ^ Rule.term2str t)

(* fo = ifo excluded already in inform *)

fun concat_deriv rew_ord erls rules fo ifo =

  let 

    fun derivat ([]:(term * Rule.rule * (term * term list)) list) = Rule.e_term

      | derivat dt = (#1 o #3 o last_elem) dt

    fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1=t2

    val  fod = Rtools.make_deriv (Isac"") erls rules (snd rew_ord) NONE  fo

    val ifod = Rtools.make_deriv (Isac"") erls rules (snd rew_ord) NONE ifo

  in 

    case (fod, ifod) of

      ([], []) => if fo = ifo then (true, []) else (false, [])

    | (fod, []) => if derivat fod = ifo then (true, fod) (*ifo is normal form*) else (false, [])

    | ([], ifod) => if fo = derivat ifod then (true, ((map rev_deriv') o rev) ifod) else (false, [])

    | (fod, ifod) =>

      if derivat fod = derivat ifod (*common normal form found*)

      then

        let 

          val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod)

        in (true, fod' @ (map rev_deriv' rifod')) end

      else (false, [])

  end

(* compare inform with ctree.form at current pos by nrls;

   if found, embed the derivation generated during comparison

   if not, let the mat-engine compute the next ctree.form *)

(* code's structure is copied from complete_solve

   CAUTION: tacis in returned calcstate' do NOT construct resulting ptp --

            all_modspec etc. has to be inserted at Subproblem'*)

fun compare_step ((tacis, c, ptp as (pt, pos as (p,p_))): Chead.calcstate') ifo =

  let

    val fo =

      case p_ of

        Ctree.Frm => Ctree.get_obj Ctree.g_form pt p

			| Ctree.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p

			| _ => Rule.e_term (*on PblObj is fo <> ifo*);

	  val {nrls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))

	  val {rew_ord, erls, rules, ...} = Rule.rep_rls nrls

	  val (found, der) = concat_deriv rew_ord erls rules fo ifo; (*<---------------*)

  in

    if found

    then

       let

         val tacis' = map (mk_tacis rew_ord erls) der;

		     val (c', ptp) = Generate.embed_deriv tacis' ptp;

	     in ("ok", (tacis (*@ tacis'?WN050408*), c @ c', ptp)) end

     else 

	     if pos = ([], Ctree.Res) (*TODO: we should stop earlier with trying subproblems *)

	     then ("no derivation found", (tacis, c, ptp): Chead.calcstate') 

	     else

         let

           val cs' as (tacis, c', ptp) = Solve.nxt_solve_ ptp; (*<---------------------*)

		       val (tacis, c'', ptp) = case tacis of

			       ((Tac.Subproblem _, _, _)::_) => 

			         let

                 val ptp as (pt, (p,_)) = Chead.all_modspec ptp (*<--------------------*)

				         val mI = Ctree.get_obj Ctree.g_metID pt p

			         in

			           Solve.nxt_solv (Tac.Apply_Method' (mI, NONE, Selem.e_istate, Selem.e_ctxt)) (Selem.e_istate, Selem.e_ctxt) ptp

               end

			     | _ => cs';

		     in compare_step (tacis, c @ c' @ c'', ptp) ifo end

  end

(* check if (agreed result, input formula) matches the error pattern "pat" modulo simplifier rls *)

fun check_err_patt (res, inf) subst (errpatID, pat) rls =

  let 

    val (res', _, _, rewritten) =

      Rewrite.rew_sub (Isac()) 1 subst Rule.e_rew_ord Rule.e_rls false [] (HOLogic.Trueprop $ pat) res;

  in

    if rewritten

    then 

      let

        val norm_res = case Rewrite.rewrite_set_inst_ (Isac()) false subst rls  res' of

          NONE => res'

        | SOME (norm_res, _) => norm_res

        val norm_inf = case Rewrite.rewrite_set_inst_ (Isac()) false subst rls inf of

          NONE => inf

        | SOME (norm_inf, _) => norm_inf

      in if norm_res = norm_inf then SOME errpatID else NONE

      end

    else NONE

  end;

(* check if (agreed result, input formula) matches SOME error pattern modulo simplifier rls;

   (prog, env) for retrieval of casual substitution for bdv in the pattern. *)

fun check_error_patterns (res, inf) (prog, env) (errpats, rls) =

  let

    val (_, subst) = Rtools.get_bdv_subst prog env

    fun scan (_, [], _) = NONE

      | scan (errpatID, errpat :: errpats, _) =

          case check_err_patt (res, inf) subst (errpatID, errpat) rls of

            NONE => scan (errpatID, errpats, [])

          | SOME errpatID => SOME errpatID

    fun scans [] = NONE

      | scans (group :: groups) =

          case scan group of

            NONE => scans groups

          | SOME errpatID => SOME errpatID

  in scans errpats end;

(*.handle a user-input formula, which may be a CAS-command, too.

CAS-command:

   create a calchead, and do 1 step

   TOOODO.WN0602 works only for the root-problem !!!

formula, which is no CAS-command:

   compare iform with calc-tree.form at pos by equ_nrls and all subsequent pos;

   collect all the tacs applied by the way;

   if "no derivation found" then check_error_patterns.

   ALTERNATIVE: check_error_patterns _within_ compare_step seems too expensive.*)

fun inform (cs as (_, _, (pt, pos as (p, _))): Chead.calcstate') istr =

  case TermC.parse (Celem.assoc_thy "Isac") istr of

	  SOME f_in =>

	    let

	      val f_in = Thm.term_of f_in

	      val f_succ = Ctree.get_curr_formula (pt, pos);

			in

			  if f_succ = f_in

			  then ("same-formula", cs) (* ctree not cut with replaceFormula *)

			  else

			    case cas_input f_in of

			      SOME (pt, _) => ("ok",([], [], (pt, (p, Ctree.Met))))

			    | NONE =>

			        let

			          val pos_pred = Ctree.lev_back' pos (*f_pred ---"step pos cs"---> f_succ in appendFormula*)

			          val f_pred = Ctree.get_curr_formula (pt, pos_pred)

			          val msg_calcstate' = compare_step ([], [], (pt, pos_pred)) f_in (*<<=====*)

			          (*last step re-calc in compare_step TODO before WN09*)

			        in

			          case msg_calcstate' of

			            ("no derivation found", calcstate') => 

			               let

			                 val pp = Ctree.par_pblobj pt p

			                 val (errpats, nrls, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of

			                   {errpats, nrls, scr = Rule.Prog prog, ...} => (errpats, nrls, prog)

			                 | _ => error "inform: uncovered case of get_met"

			                 val env = case Ctree.get_istate pt pos of

			                   Selem.ScrState (env, _, _, _, _, _) => env

			                 | _ => error "inform: uncovered case of get_istate"

			               in

			                 case check_error_patterns (f_pred, f_in) (prog, env) (errpats, nrls) of

			                   SOME errpatID => ("error pattern #" ^ errpatID ^ "#", calcstate')

			                 | NONE => msg_calcstate'

			               end

			          | _ => msg_calcstate'

			        end

			end

    | NONE => ("syntax error in '" ^ istr ^ "'", Chead.e_calcstate')

(* fill-in patterns an forms.

  returns thm required by "fun in_fillform *)

fun get_fillform (subs_opt, subst) (thm, form) errpatID (fillpatID, pat, erpaID) =

  let

    val (form', _, _, rewritten) =

      Rewrite.rew_sub (Isac()) 1 subst Rule.e_rew_ord Rule.e_rls false [] (HOLogic.Trueprop $ pat) form;

  in (*the fillpat of the thm must be dedicated to errpatID*)

    if errpatID = erpaID andalso rewritten

    then SOME (fillpatID, HOLogic.mk_eq (form, form'), thm, subs_opt) 

    else NONE

  end

fun get_fillpats subst form errpatID thm =

  let

    val thmDeriv = Thm.get_name_hint thm

    val (part, thyID) = Rtools.thy_containing_thm thmDeriv

    val theID = [part, thyID, "Theorems", Celem.thmID_of_derivation_name thmDeriv]

    val fillpats = case Specify.get_the theID of

      Celem.Hthm {fillpats, ...} => fillpats

    | _ => error "get_fillpats: uncovered case of get_the"

    val some = map (get_fillform subst (thm, form) errpatID) fillpats

  in some |> filter is_some |> map the end

fun find_fillpatterns (pt, pos as (p, _): Ctree.pos') errpatID =

  let 

    val f_curr = Ctree.get_curr_formula (pt, pos);

    val pp = Ctree.par_pblobj pt p

    val (errpats, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of

      {errpats, scr = Rule.Prog prog, ...} => (errpats, prog)

    | _ => error "find_fillpatterns: uncovered case of get_met"

    val env = case Ctree.get_istate pt pos of

		  Selem.ScrState (env, _, _, _, _, _) => env

		| _ => error "inform: uncovered case of get_istate"

    val subst = Rtools.get_bdv_subst prog env

    val errpatthms = errpats

      |> filter ((curry op = errpatID) o (#1: Rule.errpat -> Rule.errpatID))

      |> map (#3: Rule.errpat -> thm list)

      |> flat

  in map (get_fillpats subst f_curr errpatID) errpatthms |> flat end

(* check if an input formula is exactly equal the rewrite from a rule

   which is stored at the pos where the input is stored of "ok". *)

fun is_exactly_equal (pt, pos as (p, _)) istr =

  case TermC.parseNEW (Celem.assoc_thy "Isac" |> Rule.thy2ctxt) istr of

    NONE => ("syntax error in '" ^ istr ^ "'", Tac.Tac "")

  | SOME ifo => 

      let

        val p' = Ctree.lev_on p;

        val tac = Ctree.get_obj Ctree.g_tac pt p';

      in 

        case Applicable.applicable_in pos pt tac of

          Chead.Notappl msg => (msg, Tac.Tac "")

        | Chead.Appl rew =>

            let

              val res = case rew of

               Tac.Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) => res

              |Tac.Rewrite' (_, _, _, _, _, _, (res, _)) => res

              | t => error ("is_exactly_equal: uncovered case for " ^ Tac.tac_2str t)

            in 

              if not (ifo = res)

              then ("input does not exactly fill the gaps", Tac.Tac "")

              else ("ok", tac)

            end

      end

(* fetch errpatIDs from an arbitrary tactic *)

fun fetchErrorpatterns tac =

  let

    val rlsID =

      case tac of

       Tac.Rewrite_Set rlsID => rlsID

      |Tac.Rewrite_Set_Inst (_, rlsID) => rlsID

      | _ => "e_rls"

    val (part, thyID) = Rtools.thy_containing_rls "Isac" rlsID;

    val rls = case Specify.get_the [part, thyID, "Rulesets", rlsID] of

      Celem.Hrls {thy_rls = (_, rls), ...} => rls

    | _ => error "fetchErrorpatterns: uncovered case of get_the"

  in case rls of

    Rule.Rls {errpatts, ...} => errpatts

  | Rule.Seq {errpatts, ...} => errpatts

  | Rule.Rrls {errpatts, ...} => errpatts

  | Rule.Erls => []

  end

(**)

end

(**)