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

   author: Walther Neuper

   0603

   (c) due to copyright terms

use"ME/inform.sml";

use"inform.sml";

*)

signature INFORM =

  sig

    type icalhd

   (* type iitem *)

    datatype

      iitem =

          Find of cterm' list

        | Given of cterm' list

        | Relate of cterm' list

    type imodel

    val imodel2fstr : iitem list -> (string * cterm') list

    val Isac : 'a -> theory

    val appl_add' :

       theory' ->

       SpecifyTools.ori list ->

       SpecifyTools.itm list ->

       ('a * (Term.term * Term.term)) list ->

       string * cterm' -> SpecifyTools.itm

  (*  val appl_adds :

       theory' ->

       SpecifyTools.ori list ->

       SpecifyTools.itm list ->

       (string * (Term.term * Term.term)) list ->

       (string * string) list -> SpecifyTools.itm list *)

   (* val cas_input : string -> ptree * ocalhd *)

   (* val cas_input_ :

       spec ->

       (Term.term * Term.term list) list ->

       pblID * SpecifyTools.itm list * metID * SpecifyTools.itm list *

       (bool * Term.term) list  *)

    val compare_step :

       calcstate' -> Term.term -> string * calcstate'

   (* val concat_deriv :

       'a * ((Term.term * Term.term) list -> Term.term * Term.term -> bool)

       ->

       rls ->

       rule list ->

       Term.term ->

       Term.term ->

       bool * (Term.term * rule * (Term.term * Term.term list)) list *)

    val dropwhile' :   (* systest/auto-inform.sml *)

       ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list

   (* val dtss2itm_ :

       pbt_ list ->

       Term.term * Term.term list ->

       int list * bool * string * SpecifyTools.itm_ *)

   (* val e_icalhd : icalhd *)

    val eq7 : ''a * ''b -> ''a * (''b * 'c) -> bool

    val equal : ''a -> ''a -> bool

   (* val filter_dsc :

       SpecifyTools.ori list -> SpecifyTools.itm -> SpecifyTools.ori list *)

   (* val filter_sep : ('a -> bool) -> 'a list -> 'a list * 'a list *)

   (* val flattup2 : 'a * ('b * 'c * 'd * 'e) -> 'a * 'b * 'c * 'd * 'e *)

   (* val fstr2itm_ :

       theory ->

       (''a * (Term.term * Term.term)) list ->

       ''a * string -> int list * bool * ''a * SpecifyTools.itm_ *)

    val inform :

       calcstate' -> cterm' -> string * calcstate'   

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

   (* val is_Par : SpecifyTools.itm -> bool *)

   (* val is_casinput : cterm' -> fmz -> bool *)

   (* val is_e_ts : Term.term list -> bool *)

   (* val itms2fstr : SpecifyTools.itm -> string * string *)

   (* val mk_tacis :

       rew_ord' * 'a ->

       rls ->

       Term.term * rule * (Term.term * Term.term list) ->

       tac * tac_ * (pos' * istate)      *)

    val oris2itms :

       'a -> int -> SpecifyTools.ori list -> SpecifyTools.itm list

   (* val par2fstr : SpecifyTools.itm -> string * cterm' *)

   (* val parsitm : theory -> SpecifyTools.itm -> SpecifyTools.itm *)

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

   (* val unknown_expl :

       theory' ->

       (string * (Term.term * Term.term)) list ->

       (string * string) list -> SpecifyTools.itm list *)

  end

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

(*------------------------------------------------------------------(**)

structure inform :INFORM =

struct

(**)------------------------------------------------------------------*)

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, ...} = get_pbt pI

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

	  val its = add_id its_

	  val pits = map flattup2 its

	  val (pI, mI) =

      if mI <> ["no_met"]

      then (pI, mI)

		  else

        case refine_pbl thy pI pits of

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

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

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

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

	  val its = 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,b,f, Cor ((d,ts),_)):itm) =

    (let

      val t = comp_dts (d,ts);

      val s = 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)):itm))

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

    (let val t = (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,b,f, Typ str)) =

    (let val t = (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 s = 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)):itm))

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

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

	       val s = 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)):itm))

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

    (let val t = d $ t';

	       val s = 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)):itm))

  | parsitm dI (itm as (i,v,_,f, 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 (in modspec.sml)*)

(* val (sel,ct) = selct;

   val (dI, oris, ppc, pbt, (sel, ct))=

       (#1 (some_spec ospec spec), oris, []:itm list,

	((#ppc o get_pbt) (#2 (some_spec ospec spec))),

	hd (imodel2fstr imodel));

   *)

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 is_known ctxt sel oris t of

         ("", ori', all) =>

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

(* val (f, str) = hd selcts;

   *)

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

(* val SOME ct = parse thy str;

   *)

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

(* val (dI,oris,ppc,pbt,selcts) =((#1 (some_spec ospec spec)),oris,[(*!!*)],

			       ((#ppc o get_pbt) (#2 (some_spec ospec spec))),

			       (imodel2fstr imodel));

   *)

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

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

  | appl_adds dI oris ppc pbt [] = ppc

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

    (* val selct = (sel, string_of_cterm ct);

       *)

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

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

(* val (dI, oris, ppc, pbt, selct::ss) = 

       (dI, pors, probl, ppc, map itms2fstr probl);

   ...vvv

   *)

(* val (dI, oris, ppc, pbt, (selct::ss))=

       (#1 (some_spec ospec spec), oris, []:itm list,

	((#ppc o get_pbt) (#2 (some_spec ospec spec))),(imodel2fstr imodel));

   val iii = appl_adds dI oris ppc pbt (selct::ss); 

   tracing(itms2str_ thy iii);

 val itm = appl_add' dI oris ppc pbt selct;

 val ppc = insert_ppc' itm ppc;

 val _::selct::ss = (selct::ss);

 val itm = appl_add' dI oris ppc pbt selct;

 val ppc = insert_ppc' itm ppc;

 val _::selct::ss = (selct::ss);

 val itm = appl_add' dI oris ppc pbt selct;

 val ppc = insert_ppc' itm ppc;

 tracing(itms2str_ thy ppc);

 val _::selct::ss = (selct::ss);

 val itm = appl_add' dI oris ppc pbt selct;

 val ppc = insert_ppc' itm ppc;

   *)

fun oris2itms _ _ ([]:ori list) = ([]:itm list)

  | 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 filter_dsc oris itm = 

    filter_out ((curry op= ((d_in o #5) (itm:itm))) o 

		(#4:ori -> term)) oris;

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 (_,_,_,f, 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 PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'), 

		      spec = sspec as (sdI,spI,smI), probl, meth, ...} = 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 get_pbt) (#2(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 get_pbt) pI

			                   val dI' = #1 (some_spec ospec spec)

			                   val oris = if pI = #2 ospec then oris 

				                            else 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 get_met) mI

		                        val mits = 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 (some_spec ospec spec)) oris [(*!!!*)]

			                     ((#ppc o get_pbt) (#2 (some_spec ospec spec)))

			                     (imodel2fstr imodel), meth);

	         val pt = update_spec pt p spec;

         in if pos_ = Pbl

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

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

	               in (update_pbl pt p pits,

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

                 end

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

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

	                in (update_met pt p mits,

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

                  end

         end 

    end

  | input_icalhd pt ((p,_), hdf, imodel, _(*Met*), spec as (dI,pI,mI)) =

    error "input_icalhd Met not impl.";

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

(*

Untersuchung zur Formeleingabe (appendFormula, replaceFormla) zu einer Anregung von Alan Krempler:

Welche RICHTIGEN Formeln koennen NICHT abgeleitet werden, 

wenn Abteilungen nur auf gleichem Level gesucht werden ?

WN.040216 

Beispiele zum Equationsolver von Richard Lang aus /src/sml/kbtest/rlang.sml

------------------------------------------------------------------------------

"Schalk I s.87 Bsp 52a ((5*x)/(x - 2) - x/(x+2)=4)";

------------------------------------------------------------------------------

1. "5 * x / (x - 2) - x / (x + 2) = 4"

...

4. "12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2)",Subproblem["normalize", "poly"..

...

4.3. "16 + 12 * x = 0", Subproblem["degree_1", "polynomial", "univariate"..

...

4.3.3. "[x = -4 / 3]")), Check_elementwise "Assumptions"

...

"[x = -4 / 3]"

------------------------------------------------------------------------------

(1)..(6): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite verschiebt [Ableitung ware in 4.3.n]

(4.1)..(4.3): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite verschiebt [Ableitung ware in 4.3.n]

------------------------------------------------------------------------------

------------------------------------------------------------------------------

"Schalk I s.87 Bsp 55b (x/(x^^^2 - 6*x+9) - 1/(x^^^2 - 3*x) =1/x)";

------------------------------------------------------------------------------

1. "x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) = 1 / x"

...

4. "(3 + (-1 * x + x ^^^ 2)) * x = 1 * (9 * x + (x ^^^ 3 + -6 * x ^^^ 2))"

                         Subproblem["normalize", "polynomial", "univariate"..

...

4.4. "-6 * x + 5 * x ^^^ 2 = 0", Subproblem["bdv_only", "degree_2", "poly"..

...

4.4.4. "[x = 0, x = 6 / 5]", Check_elementwise "Assumptions"

4.4.5. "[x = 0, x = 6 / 5]"

...

5. "[x = 0, x = 6 / 5]", Check_elementwise "Assumptions"

   "[x = 6 / 5]"

------------------------------------------------------------------------------

(1)..(4): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite schiebt [Ableitung waere in 4.4.x]

(4.1)..(4.4.5): keine 'richtige' Eingabe kann abgeleitet werden, die dem Ergebnis "[x = 6 / 5]" aequivalent ist [Ableitung waere in 5.]

------------------------------------------------------------------------------

------------------------------------------------------------------------------

"Schalk II s.56 Bsp 73b (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))";

------------------------------------------------------------------------------

1. "sqrt (x + 1) + sqrt (4 * x + 4) = sqrt (9 * x + 9)"

...

6. "13 + 13 * x + -2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x"

                             Subproblem["sq", "root'", "univariate", "equation"]

...

6.6. "144 + 288 * x + 144 * x ^^^ 2 = 144 + x ^^^ 2 + 288 * x + 143 * x ^^^ 2"

                Subproblem["normalize", "polynomial", "univariate", "equation"]

...

6.6.3 "0 = 0"    Subproblem["degree_0", "polynomial", "univariate", "equation"]

...                                       Or_to_List

6.6.3.2 "UniversalList"

------------------------------------------------------------------------------

(1)..(6): keine 'richtige' Eingabe kann abgeleitet werden, die eine der Wurzeln auf die andere Seite verschieb [Ableitung ware in 6.6.n]

(6.1)..(6.3): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite verschiebt [Ableitung ware in 6.6.n]

------------------------------------------------------------------------------

*)

(*sh. comments auf 498*)

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";

(*

 fun equal a b = a=b;

 val foder = [0,1,2,3,4,5]; val ifoder = [11,12,3,4,5];

 val r_foder = rev foder;  val r_ifoder = rev ifoder;

 dropwhile' equal r_foder r_ifoder;

> vval it = ([0, 1, 2, 3], [3, 12, 11]) : int list * int list

 val foder = [3,4,5]; val ifoder = [11,12,3,4,5];

 val r_foder = rev foder;  val r_ifoder = rev ifoder;

 dropwhile' equal r_foder r_ifoder;

> val it = ([3], [3, 12, 11]) : int list * int list

 val foder = [5]; val ifoder = [11,12,3,4,5];

 val r_foder = rev foder;  val r_ifoder = rev ifoder;

 dropwhile' equal r_foder r_ifoder;

> val it = ([5], [5, 4, 3, 12, 11]) : int list * int list

 val foder = [10,11,12,13,14,15]; val ifoder = [11,12,3,4,5];

 val r_foder = rev foder;  val r_ifoder = rev ifoder;

 dropwhile' equal r_foder r_ifoder;

> *** dropwhile': did not start with equal elements*)

(*040214: version for concat_deriv*)

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

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

      (Rewrite (id, Thm.prop_of thm), 

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

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

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

      (Rewrite_Set (rule2rls' r), 

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

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

(*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 = make_deriv (Isac"") erls rules (snd rew_ord) NONE  fo

    val ifod = 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;

(*

 val ({rew_ord, erls, rules,...}, fo, ifo) = 

     (rep_rls Test_simplify, str2term "x+1+ -1*2=0", str2term "-2*1+(x+1)=0");

 (tracing o trtas2str) fod';

> ["

(x + 1 + -1 * 2 = 0, Thm ("radd_commute","?m + ?n = ?n + ?m"), (-1 * 2 + (x + 1) = 0, []))","

(-1 * 2 + (x + 1) = 0, Thm ("radd_commute","?m + ?n = ?n + ?m"), (-1 * 2 + (1 + x) = 0, []))","

(-1 * 2 + (1 + x) = 0, Thm ("radd_left_commute","?x + (?y + ?z) = ?y + (?x + ?z)"), (1 + (-1 * 2 + x) = 0, []))","

(1 + (-1 * 2 + x) = 0, Thm ("#mult_Float ((~1,0), (0,0)) __ ((2,0), (0,0))","-1 * 2 = -2"), (1 + (-2 + x) = 0, []))"]

val it = () : unit

 (tracing o trtas2str) (map rev_deriv' rifod');

> ["

(1 + (-2 + x) = 0, Thm ("sym_#mult_Float ((~2,0), (0,0)) __ ((1,0), (0,0))","-2 = -2 * 1"), (1 + (-2 * 1 + x) = 0, []))","

(1 + (-2 * 1 + x) = 0, Thm ("sym_radd_left_commute","?y + (?x + ?z) = ?x + (?y + ?z)"), (-2 * 1 + (1 + x) = 0, []))","

(-2 * 1 + (1 + x) = 0, Thm ("sym_radd_commute","?n + ?m = ?m + ?n"), (-2 * 1 + (x + 1) = 0, []))"]

val it = () : unit

*)

(* 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_))): 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, ...} = 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) = 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): calcstate') 

	     else

         let

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

		       val cs' as (tacis, c'', ptp) = 

			       case tacis of

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

			           let

                   val ptp as (pt, (p,_)) = 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) = 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 (_, _, ptp as (pt, pos as (p, p_))): 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, scr = Prog prog, ...} = get_met (get_obj g_metID pt pp)

			                 val ScrState (env, _, _, _, _, _) = get_istate pt pos

			               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 ^ "'", 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) = thy_containing_thm thmDeriv

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

        val Hthm {fillpats, ...} = get_the theID

        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, scr = Prog prog, ...} = get_met (get_obj g_metID pt pp)

    val ScrState (env, _, _, _, _, _) = get_istate pt pos

    val subst = 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

          Notappl msg => (msg, Tac "")

        | Appl rew =>

            let

              val res = case rew of

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

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

            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) = thy_containing_rls "Isac" rlsID;

    val Hrls {thy_rls = (_, rls), ...} = get_the [part, thyID, "Rulesets", rlsID]

  in case rls of

        Rls {errpatts, ...} => errpatts

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

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

      | Erls => []

  end

(*------------------------------------------------------------------(**)

end

open inform; 

(**)------------------------------------------------------------------*)