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

     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 castab : castab ref

     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

 		 pos' as (p,p_) where p_ is neglected due to pos_ below*) 

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

 (*.association list with cas-commands, for generating a complete calc-head.*)

 type castab = 

      (term *         (*cas-command, eg. 'solve'*)

       (spec * 	     (*theory, problem, method*)

        		     (*the function generating a kind of formalization*)

        (term list -> (*the arguments of the cas-command, eg. (x+1=2, x)*)

 	(term *      (*description of an element*)

 	 term list)  (*value of the element (always put into a list)*)

 	    list)))  (*of elements in the formalization*)

 	 list;       (*of cas-entries in the association list*)

 val castab = ref ([]: castab);

 (*..*)

 (* val (dI,pI,mI) = spec;

    *)

 (*fun cas_input_ ((dI,pI,mI): spec) dtss =

     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 let val SOME (pI,_) = refine_pbl thy pI pits

 			in (pI, (hd o #met o get_pbt) pI) end

 	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

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

 (* val (dI,pI,mI) = spec;

    *)

 fun cas_input_ ((dI,pI,mI): spec) dtss =

     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

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

 (*.check if the input term is a CAScmd and return a ptree with 

    a _complete_ calchead.*)

 (* val hdt = ifo;

    *)

 fun cas_input hdt =

     let val (h,argl) = strip_comb hdt

     in case assoc (!castab, h) of

 	   NONE => NONE

 	 (*let val (pt,_) = 

 		   cappend_problem e_ptree [] e_istate 

 				   ([], e_spec) ([], e_spec, e_term)

 	   in (pt, (false, Pbl, e_term(*FIXXME031:'not found'*),

 		    [], [], e_spec)) end*)

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

 	   (* val SOME (spec as (dI,_,_), argl2dtss ) = assoc (!castab, h);

 	    *)

 	   let val dtss = argl2dtss argl

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

 	       val spec = (dI, pI, mI)

 	       val (pt,_) = 

 		   cappend_problem e_ptree [] e_istate ([], e_spec) 

 				   ([], e_spec, hdt)

 	       val pt = update_spec pt [] spec

 	       val pt = update_pbl pt [] pits

 	       val pt = update_met pt [] mits

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

     end;

 (*lazy evaluation for Isac.thy*)

 fun Isac _  = assoc_thy "Isac.thy";

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

 (* val itm as (i,v,b,f, Cor ((d,ts),_)) = hd probl;

    *)

     (let val t = (comp_dts (Isac "delay")) (d,ts);

 	 val s = Syntax.string_of_term (thy2ctxt 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 = (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 = (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 (Isac "delay")) (d,ts);

 	 val s = Syntax.string_of_term (thy2ctxt 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 (Isac"delay" )) (d,ts);

 	 val s = Syntax.string_of_term (thy2ctxt 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 = Syntax.string_of_term (thy2ctxt 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 _)) = 

     raise 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 thy = assoc_thy dI;

     in case parse thy ct of

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

 	 | SOME ct => (* val SOME ct = parse thy ct;

 		          *)

     (case is_known thy sel oris (term_of ct) of

 	 (* val ("",ori'(*ts='ct'*), all) = is_known thy sel oris (term_of ct);

 	     *)

 	 ("",ori'(*ts='ct'*), all) => 

 	 (case is_notyet_input thy ppc all ori' pbt of

 	      (* val ("",itm) = is_notyet_input thy ppc all ori' pbt;

 	          *)

 	      ("",itm)  => itm

 	 (* val (msg,xx) = is_notyet_input thy ppc all ori' pbt;

 	    *)

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

 	 (* val (msg,(_,_,_,d,ts),all) = is_known thy sel oris (term_of ct);

 	    *)

        | (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 thy) o 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); 

    writeln(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;

  writeln(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 = raise 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 _)) = 

     raise 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 CAS-command via a whole calchead;

    dWN0602 ropped due to change of design in the front-end.*)

 (*since previous calc-head _only_ has changed:

   EITHER _1_ part of the specification OR some items in the model;

   the hdform is left as is except in cas_input .*)

 (*FIXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX___Met___XXXXXXXXXXXME.TODO.WN:11.03*)

 (*   val ((p,_), hdf, imodel, Pbl, spec as (dI,pI,mI)) = 

        (p, "xxx", empty_model, Pbl, e_spec);

    val ((p,_), hdf, imodel, Pbl, spec as (dI,pI,mI)) = 

        (p,"", [Given ["fixedValues [r=Arbfix]"],

 	       Find ["maximum A", "valuesFor [a,b]"],

 	       Relate ["relations [A=a*b, a/2=r*sin alpha, \

 		       \b/2=r*cos alpha]"]], Pbl, e_spec);   

    val ((p,_), hdf, imodel, Pbl, spec as (dI,pI,mI)) = 

        (([],Pbl), "not used here",

 	[Given ["fixedValues [r=Arbfix]"],

 	 Find ["maximum A", "valuesFor [a,b]"(*new input*)], 

 	 Relate ["relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]"]], Pbl, 

         ("DiffApp.thy", ["e_pblID"], ["e_metID"]));

    val ((p,_), hdf, imodel, Pbl, spec as (dI,pI,mI)) = ichd;

    *)

 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.thy") pbt;

 		    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.thy")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.thy") 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)) =

     raise 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 raise error "dropwhile': did not start with equal elements"

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

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

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

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

     if equal f i then ([f], i::is)

     else raise 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_Thm r, (t, a));

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

     (Rewrite (rule2thm' r), 

      Rewrite' ("Isac.thy", fst ro, erls, false, 

 	       rule2thm' r, t, (t', a)),

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

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

     (Rewrite_Set (rule2rls' r), 

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

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

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

  (writeln 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

  (writeln 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'*)

 (* val (tacis, c, ptp as (pt, pos as (p,p_))) = (tacis, ptp);

    val (tacis, c, ptp as (pt, pos as (p,p_))) = cs';

    val (tacis, c, ptp as (pt, pos as (p,p_))) = ([],[],(pt, lev_back pos));

    -----rec.call:

    val (tacis, c, ptp as (pt, pos as (p,p_))) = cs';

    *)

 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) 

 	   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_istate ptp end

 			  | _ => cs';

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

     end;

 (* writeln (trtas2str der);

    *)

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

 (*structure copied from autocalc*)

 (* val (cs as (_,  _, (pt, pos as (p, p_))): calcstate') = cs';

    val ifo = str2term ifo;

    val ((cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate'), istr) =

        (cs', encode ifo);

    val ((cs as (_, _, ptp as (pt, pos as (p, p_)))), istr)=(cs', (encode ifo));

    val ((cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate'), istr) =

        (([],[],(pt,p)), (encode ifo));

    *)

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

     case parse (assoc_thy "Isac.thy") istr of

 (* val SOME ifo = parse (assoc_thy "Isac.thy") istr;

    *)

 	SOME ifo =>

 	let val ifo = term_of ifo

 	    val fo = case p_ of Frm => get_obj g_form pt p

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

 			      | _ => #3 (get_obj g_origin pt p)

 	in if fo = ifo

 	   then ("same-formula", cs)

 	   (*thus ctree not cut with replaceFormula!*)

 	   else case cas_input ifo of

 (* val SOME (pt, _) = cas_input ifo;

    *)

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

 		  | NONE =>

 		    compare_step ([],[],(pt,

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

 					 lev_back pos)) ifo

 	end

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

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

 end

 open inform; 

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