signature INPUT_FORMULAS =

 signature INPUT_FORMULAS =

 sig

 sig

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

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

   type imodel = iitem list

   type imodel = iitem list

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   val check_error_patterns :

   val check_error_patterns :

     term * term ->

     term * term ->

 type imodel = iitem list

 type imodel = iitem list

 (*calc-head as input*)

 (*calc-head as input*)

 type icalhd =

 type icalhd =

   cterm' *   (*the headline*)

   cterm' *   (*the headline*)

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

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

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

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

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

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

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

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

 fun dtss2itm_ ppc (d, ts) =

 fun dtss2itm_ ppc (d, ts) =

   let

   let

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

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

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

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

 	  val its = Specify.add_id its_

 	  val its = Specify.add_id its_

 	  val mits = map flattup2 its

 	  val mits = map flattup2 its

 	  val pre = check_preconds thy prls pre mits

 	  val pre = check_preconds thy prls pre mits

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

   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 *)

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

 fun cas_input hdt =

 fun cas_input hdt =

 	      let

 	      let

           val dtss = argl2dtss argl

           val dtss = argl2dtss argl

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

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

 	        val spec = (dI, pI, mI)

 	        val spec = (dI, pI, mI)

 	        val (pt,_) = 

 	        val (pt,_) = 

 	      in

 	      in

 	      end

 	      end

   end

   end

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

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

 fun Isac _  = assoc_thy "Isac";

 fun Isac _  = assoc_thy "Isac";

   in xxx [] iitems end;

   in xxx [] iitems end;

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

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

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

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

     let

     let

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

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

         => (fmz, fmz_, oris, ospec, hdf', sspec, 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"

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

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

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

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

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

 				              (map itms2fstr probl), meth) end 

 				              (map itms2fstr probl), meth) end 

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

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

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

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

 		                     val mits = Chead.complete_metitms oris probl meth met

 		                     val mits = Chead.complete_metitms oris probl meth met

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

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

 		                   end 

 		                   end 

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

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

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

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

 			                  (imodel2fstr imodel), meth)

 			                  (imodel2fstr imodel), meth)

          in if pos_ = Pbl

          in if pos_ = Pbl

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

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

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

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

                  end

                  end

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

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

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

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

                   end

                   end

          end 

          end 

     end

     end

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

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

 (* 040214: version for concat_deriv *)

 (* 040214: version for concat_deriv *)

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

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

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

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

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

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

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

 (* fo = ifo excluded already in inform *)

 (* fo = ifo excluded already in inform *)

 fun concat_deriv rew_ord erls rules fo ifo =

 fun concat_deriv rew_ord erls rules fo ifo =

   let 

   let 

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

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

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

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

   let

   let

     val fo =

     val fo =

       case p_ of

       case p_ of

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

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

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

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

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

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

   in

   in

     if found

     if found

     then

     then

        let

        let

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

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

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

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

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

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

      else 

      else 

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

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

 	     else

 	     else

          let

          let

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

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

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

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

 			         let

 			         let

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

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

 			         in

 			         in

                end

                end

 			     | _ => cs';

 			     | _ => cs';

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

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

   end

   end

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

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

   case parse (assoc_thy "Isac") istr of

   case parse (assoc_thy "Isac") istr of

 	  SOME f_in =>

 	  SOME f_in =>

 	    let

 	    let

 	      val f_in = Thm.term_of f_in

 	      val f_in = Thm.term_of f_in

 			in

 			in

 			  if f_succ = f_in

 			  if f_succ = f_in

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

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

 			  else

 			  else

 			    case cas_input f_in of

 			    case cas_input f_in of

 			    | NONE =>

 			    | NONE =>

 			        let

 			        let

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

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

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

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

 			        in

 			        in

 			          case msg_calcstate' of

 			          case msg_calcstate' of

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

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

 			               let

 			               let

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

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

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

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

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

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

 			               in

 			               in

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

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

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

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

 			                 | NONE => msg_calcstate'

 			                 | NONE => msg_calcstate'

       Hthm {fillpats, ...} => fillpats

       Hthm {fillpats, ...} => fillpats

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

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

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

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

   in some |> filter is_some |> map the end

   in some |> filter is_some |> map the end

   let 

   let 

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

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

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

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

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

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

     val subst = Rtools.get_bdv_subst prog env

     val subst = Rtools.get_bdv_subst prog env

     val errpatthms = errpats

     val errpatthms = errpats

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

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

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

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

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

 (* 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". *)

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

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

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

   case parseNEW (assoc_thy "Isac" |> thy2ctxt) istr of

   case parseNEW (assoc_thy "Isac" |> thy2ctxt) istr of

   | SOME ifo => 

   | SOME ifo => 

       let

       let

       in 

       in 

         case Applicable.applicable_in pos pt tac of

         case Applicable.applicable_in pos pt tac of

         | Chead.Appl rew =>

         | Chead.Appl rew =>

             let

             let

               val res = case rew of

               val res = case rew of

             in 

             in 

               if not (ifo = res)

               if not (ifo = res)

               else ("ok", tac)

               else ("ok", tac)

             end

             end

       end

       end

 (* fetch errpatIDs from an arbitrary tactic *)

 (* fetch errpatIDs from an arbitrary tactic *)

 fun fetchErrorpatterns tac =

 fun fetchErrorpatterns tac =

   let

   let

     val rlsID =

     val rlsID =

       case tac of

       case tac of

       | _ => "e_rls"

       | _ => "e_rls"

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

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

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

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

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

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

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

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