(* 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 cterm' list | Given of cterm' list | Relate of cterm' list

   type imodel = iitem list

   type icalhd = pos' * cterm' * imodel * pos_ * spec

   val fetchErrorpatterns : tac -> errpatID list

   val input_icalhd : ptree -> icalhd -> ptree * ocalhd

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

   val find_fillpatterns : ptree * pos' -> errpatID -> (fillpatID * term * thm * subs option) list

   val is_exactly_equal : ptree * (pos * pos_) -> string -> string * tac

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

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

   val cas_input : term -> (ptree * ocalhd) option

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

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

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

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

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

   val check_error_patterns :

     term * term ->

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

   val get_fillform :

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

   val get_fillpats :

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

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

 end

 (**)

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

 struct

 (**)

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

 datatype iitem = 

   Given of cterm' list

 (*Where is never input*) 

 | Find  of cterm' list

 | Relate  of cterm' list

 type imodel = iitem list

 (*calc-head as input*)

 type icalhd =

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

   cterm' *   (*the headline*)

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

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

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

 val e_icalhd = (e_pos', "", [Given [""]], Pbl, e_spec) : icalhd

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

   hdf <> "" andalso fmz_ = [] andalso spec = 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: pbt_ -> (term * term))) ppc)

   in

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

   end

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

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

   let

     val thy = 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 = check_preconds thy prls pre mits

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

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

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

 fun cas_input hdt =

   let

     val (h, argl) = strip_comb hdt

   in

     case assoc_cas (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,_) = 

 		        cappend_problem e_ptree [] (e_istate, e_ctxt) ([], e_spec) ([], e_spec, hdt)

 	        val pt = update_spec pt [] spec

 	        val pt = update_pbl pt [] pits

 	        val pt = update_met pt [] mits

 	        val pt = update_ctxt pt [] ctxt

 	      in

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

 	      end

   end

 (*lazy evaluation for (Thy_Info.get_theory "Isac")*)

 fun Isac _  = 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, Cor ((d, ts), _)) : itm) =

     (let val t = comp_dts (d, ts)

      val _ = (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, Syn (term2str t)) : itm))

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

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

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

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

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

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

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

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

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

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

 	       val _ = term_to_string''' dI t;

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

      in itm end

      handle _ => (i, v, false, f, Syn (term2str t)))

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

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

 	       val _ = term_to_string''' dI t;

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

     in itm end

     handle _ => (i, v, false, f, Syn (term2str t)))

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

     (let val t = d $ t';

 	       val _ = term_to_string''' dI t;

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

     in itm end

     handle _ => (i, v, false, f, Syn (term2str t)))

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

     error ("parsitm (" ^ itm2str_ (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 ((_, _, _, _,Par _) : itm) = 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 = assoc_thy dI |> thy2ctxt;

   in

     case parseNEW ctxt ct of

 	    NONE => (0,[],false,sel, Syn ct):itm

 	  | 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, Inc ((d, ts), (e_term, [])))

         else (i, v, false, sel, 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 = parse thy str

   in

     case topt of

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

     | SOME ct => 

 	    let

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

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

 	    in

 	      case popt of

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

 	      | SOME (f, (d, id)) => ([1], true, f, 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 = assoc_thy dI

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

     val its = Specify.add_id its_ 

   in

     (map flattup2 its): itm list

   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 _  _ [] = ([] : itm list) (* WN161130: similar in ptyps ?!? *)

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

     if member op = vat v 

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

     else oris2itms pbt vat os

 fun par2fstr ((_, _, _, f, Par s) : itm) = (f, s)

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

 fun itms2fstr ((_, _, _, f, Cor ((d, ts), _)) : itm) = (f, comp_dts'' (d, ts))

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

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

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

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

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

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

     error ("parsitm ("^itm2str_ (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, Pbl, spec as (dI, pI, mI)) : icalhd) =

     let

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

 		    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 (str2term hdf)) 

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

          let val (pos_, pits, mits) = 

 	         if dI <> sdI

 	         then let val its = map (parsitm (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 (Pbl, appl_adds dI oris its pbt  (map par2fstr trms), meth) end 

            else

              if pI <> spI 

 	           then if pI = snd3 ospec then (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_(assoc_thy"Isac") pbt |> #1;

 		                in (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 (Pbl, probl, mits) else (Met, probl, mits) 

 		                   end 

                   else (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 = update_spec pt p spec;

          in if pos_ = Pbl

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

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

 	               in (update_pbl pt p pits,

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

                  end

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

 		                val pre = check_preconds (assoc_thy"Isac") prls pre mits

 	                in (update_met pt p mits,

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

                   end

          end 

     end

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

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

 fun equal a b = a = b

 (*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 Thm (id, thm), (t', a)) = 

       (Rewrite (id, thm), 

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

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

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

       (Rewrite_Set (Lucin.rule2rls' r), 

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

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

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

 (* fo = ifo excluded already in inform *)

 fun concat_deriv rew_ord erls rules fo ifo =

   let 

     fun derivat ([]:(term * rule * (term * term list)) list) = 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 *)

 (* structure 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

         Frm => get_obj g_form pt p

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

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

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

 	  val {rew_ord, erls, rules, ...} = 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) = Ctree.embed_deriv tacis' ptp;

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

      else 

 	     if pos = ([], 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) = nxt_solve_ ptp; (*<---------------------*)

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

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

 			         let

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

 				         val mI = get_obj g_metID pt p

 			         in

 			           nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt)) (e_istate, 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: subst) (errpatID: errpatID, pat) rls =

   let 

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

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

   in

     if rewritten

     then 

       let

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

           NONE => res'

         | SOME (norm_res, _) => norm_res

         val norm_inf = case 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: 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 parse (assoc_thy "Isac") istr of

 	  SOME f_in =>

 	    let

 	      val f_in = Thm.term_of f_in

 	      val f_succ = 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, Met))))

 			    | NONE =>

 			        let

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

 			          val f_pred = 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 = par_pblobj pt p

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

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

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

 			                 val env = case get_istate pt pos of

 			                   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): fillpat) =

   let

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

       rew_sub (Isac()) 1 subst e_rew_ord e_rls false [] (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", thmID_of_derivation_name thmDeriv]

     val fillpats = case Specify.get_the theID of

       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, _): pos') errpatID =

   let 

     val f_curr = get_curr_formula (pt, pos);

     val pp = par_pblobj pt p

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

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

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

     val env = case get_istate pt pos of

 		  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: errpat -> errpatID))

       |> map (#3: 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 parseNEW (assoc_thy "Isac" |> thy2ctxt) istr of

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

   | SOME ifo => 

       let

         val p' = lev_on p;

         val tac = get_obj g_tac pt p';

       in 

         case applicable_in pos pt tac of

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

         | Chead.Appl rew =>

             let

               val res = case rew of

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

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

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

             in 

               if not (ifo = res)

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

               else ("ok", tac)

             end

       end

 (* fetch errpatIDs from an arbitrary tactic *)

 fun fetchErrorpatterns tac =

   let

     val rlsID =

       case tac of

         Rewrite_Set rlsID => rlsID

       | 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

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

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

   in case rls of

     Rls {errpatts, ...} => errpatts

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

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

   | Erls => []

   end

 (**)

 end

 (**)