(* the interface between the isac-kernel and the java-frontend;

   the isac-kernel holds calc-trees; stdout in XML-format.

   authors: Walther Neuper 2002

   (c) due to copyright terms

use"Frontend/interface.sml";

use"interface.sml";

*)

signature INTERFACE =

  sig

    val CalcTree : fmz list -> unit

    val DEconstrCalcTree : calcID -> unit

    val Iterator : calcID -> unit

    val IteratorTEST : calcID -> iterID

    val appendFormula : calcID -> cterm' -> unit

    val autoCalculate : calcID -> auto -> unit

    val checkContext : calcID -> pos' -> guh -> unit

    val fetchApplicableTactics : calcID -> int -> pos' -> unit

    val fetchProposedTactic : calcID -> unit

    val applyTactic : calcID -> pos' -> tac -> unit

    val getAccumulatedAsms : calcID -> pos' -> unit

    val getActiveFormula : calcID -> unit

    val getAssumptions : calcID -> pos' -> unit

    val initContext : calcID -> ketype -> pos' -> unit

    val getFormulaeFromTo : calcID -> pos' -> pos' -> int -> bool -> unit

    val getTactic : calcID -> pos' -> unit

    val interSteps : calcID -> pos' -> unit

    val modifyCalcHead : calcID -> icalhd -> unit

    val moveActiveCalcHead : calcID -> unit

    val moveActiveDown : calcID -> unit

    val moveActiveDownTEST : calcID -> unit

    val moveActiveFormula : calcID -> pos' -> unit

    val moveActiveLevelDown : calcID -> unit

    val moveActiveLevelUp : calcID -> unit

    val moveActiveRoot : calcID -> unit

    val moveActiveRootTEST : calcID -> unit

    val moveActiveUp : calcID -> unit

    val moveCalcHead : calcID -> pos' -> unit

    val moveDown : calcID -> pos' -> unit

    val moveLevelDown : calcID -> pos' -> unit

    val moveLevelUp : calcID -> pos' -> unit

    val moveRoot : calcID -> unit

    val moveUp : calcID -> pos' -> unit

    val refFormula : calcID -> pos' -> unit

    val replaceFormula : calcID -> cterm' -> unit

    val resetCalcHead : calcID -> unit

    val modelProblem : calcID -> unit

    val refineProblem : calcID -> pos' -> guh -> unit

    val setContext : calcID -> pos' -> guh -> unit

    val setMethod : calcID -> metID -> unit

    val setNextTactic : calcID -> tac -> unit

    val setProblem : calcID -> pblID -> unit

    val setTheory : calcID -> thyID -> unit

    val findFillpatterns : calcID -> errpatID -> unit

    val requestFillformula : calcID -> errpatID * fillpatID -> unit

    val inputFillFormula: calcID -> string -> unit

(*------------ for tests*)

val encode: cterm' -> cterm'

val encode_fmz: fmz -> fmz

  end

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

structure interface : INTERFACE =

struct

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

(* encode "Isabelle"-strings as seen by the user to the

   format accepted by Isabelle.

   encode "^" ---> "^^^"; see Knowledge/Atools.thy;

   called for each cterm', icalhd, fmz in this interface;

   + see "fun decode" in xmlsrc/mathml.sml *)

fun encode (str : cterm') = 

    let fun enc [] = []

	  | enc ("^" :: cs) = "^" :: "^" :: "^" :: (enc cs)

	  | enc (c :: cs) = c :: (enc cs)

    in (implode o enc o Symbol.explode) str:cterm' end;

fun encode_imodel (imodel:imodel) =

    let fun enc (Given ifos) = Given (map encode ifos)

	  | enc (Find ifos) = Find (map encode ifos)

	  | enc (Relate ifos) = Relate (map encode ifos)

    in map enc imodel:imodel end;

fun encode_icalhd ((pos', headl, imodel, pos_, spec):icalhd) =

    (pos', encode headl, encode_imodel imodel, pos_, spec):icalhd;

fun encode_fmz ((ifos, spec) : fmz) = (map encode ifos, spec) : fmz;

(***. CalcTree .***)

(** add and delete users **)

(*.'Iterator 1' must exist with each CalcTree;

   the only for updating the calc-tree

   WN.0411: only 'Iterator 1' is stored,

   all others are just calculated on the fly

   TODO: adapt Iterator, add_user(= add_iterator!),etc. accordingly .*)

fun Iterator (cI:calcID) = (*returned ID unnecessary after WN.0411*)

    (adduserOK2xml cI (add_user (cI:calcID)))

    handle _ => sysERROR2xml cI "error in kernel";

fun IteratorTEST (cI:calcID) = add_user (cI:calcID);

(*fun DEconstructIterator (cI:calcID) (uI:iterID) =

    deluserOK2xml (del_user cI uI);*)

(*.create a calc-tree; for calls from java: thus ^^^ decoded to ^;

   compare "fun CalcTreeTEST" which does NOT decode.*)

fun CalcTree [(fmz, sp) : fmz] (*for several variants lateron*) =

	(let val cs = nxt_specify_init_calc (encode_fmz (fmz, sp))

	     (*FIXME.WN.8.03: error-handling missing*)

	     val cI = add_calc cs

	 in calctreeOK2xml cI end)

	handle _ => sysERROR2xml 0 "error in kernel";

fun DEconstrCalcTree (cI:calcID) =

    deconstructcalctreeOK2xml (del_calc cI);

fun getActiveFormula (cI:calcID) = iteratorOK2xml cI (get_pos cI 1);

fun moveActiveFormula (cI:calcID) (p:pos') =

    let val ((pt,_),_) = get_calc cI

    in if existpt' p pt then (upd_ipos cI 1 p; iteratorOK2xml cI p)

       else sysERROR2xml cI "frontend sends a non-existing pos" end;

(*. set the next tactic to be applied: dont't change the calc-tree,

    but remember the envisaged changes for fun autoCalculate;

    compare force NextTactic .*)

(* val (cI, tac) = (1, Add_Given "equality (x ^^^ 2 + 4 * x + 3 = 0)");

   val (cI, tac) = (1, Specify_Theory "PolyEq");

   val (cI, tac) = (1, Specify_Problem ["normalize","polynomial",

				   "univariate","equation"]);

   val (cI, tac) = (1, Subproblem ("Poly",

			      ["polynomial","univariate","equation"]));

   val (cI, tac) = (1, Model_Problem["linear","univariate","equation","test"]);

   val (cI, tac) = (1, Detail_Set "Test_simplify");

   val (cI, tac) = (1, Apply_Method ["Test", "solve_linear"]);

   val (cI, tac) = (1, Rewrite_Set "Test_simplify");

    *)

fun setNextTactic (cI:calcID) tac =

  let 

    val ((pt, _), _) = get_calc cI

	  val ip = get_pos cI 1

  in case locatetac tac (pt, ip) of

(* val ("ok", (tacis, c, (_,p'))) = locatetac tac (pt, ip);

   *)

	   ("ok", (tacis, _, _)) =>

	   (upd_calc cI ((pt, ip), tacis); setnexttactic2xml cI "ok")

	 | ("unsafe-ok", (tacis, _, _)) =>

	   (upd_calc cI ((pt, ip), tacis); setnexttactic2xml cI "unsafe-ok")

	 | ("not-applicable",_) => setnexttactic2xml cI "not-applicable"

	 | ("end-of-calculation",_) =>

	   setnexttactic2xml cI "end-of-calculation"

	 | ("failure",_) => sysERROR2xml cI "failure"

    end;

(*. apply a tactic at a position and update the calc-tree if applicable .*)

(*WN080226 java-code is missing, errors smltest/Knowledge/polyminus.sml*)

fun applyTactic (cI:calcID) ip tac =

  let

    val ((pt, _), _) = get_calc cI

	  val p = get_pos cI 1

  in 

    case locatetac tac (pt, ip) of

	    ("ok", (_, c, ptp as (_,p'))) =>

	      (upd_calc cI (ptp, []);

	       upd_ipos cI 1 p';

	       autocalculateOK2xml cI p (if null c then p' else last_elem c) p')

	  | ("unsafe-ok", (_, c, ptp as (_,p'))) =>

	      (upd_calc cI (ptp, []);

	       upd_ipos cI 1 p';

	       autocalculateOK2xml cI p (if null c then p' else last_elem c) p')

	  | ("end-of-calculation", (_, c, ptp as (_,p'))) =>

	      (upd_calc cI (ptp, []);

	       upd_ipos cI 1 p';

	       autocalculateOK2xml cI p (if null c then p' else last_elem c) p')

	  | (str,_) => autocalculateERROR2xml cI "failure"

  end;

fun fetchProposedTactic (cI:calcID) =

    (case step (get_pos cI 1) (get_calc cI) of

	   ("ok", (tacis, _, _)) =>

	   let val _= upd_tacis cI tacis

	       val (tac,_,_) = last_elem tacis

	   in fetchproposedtacticOK2xml cI tac (fetchErrorpatterns tac) end

	 | ("helpless",_) => fetchproposedtacticERROR2xml cI "helpless"

	 | ("no-fmz-spec",_) => fetchproposedtacticERROR2xml cI "no-fmz-spec"

	 | ("end-of-calculation",_) =>

	   fetchproposedtacticERROR2xml cI "end-of-calculation")

    handle _ => sysERROR2xml cI "error in kernel";

(*datatype auto = FIXXXME040624: does NOT match interfaces/ITOCalc.java

  Step of int      (*1 do #int steps (may stop in model/specify)

		     IS VERY INEFFICIENT IN MODEL/SPECIY*)

| CompleteModel    (*2 complete modeling

                     if model complete, finish specifying*)

| CompleteCalcHead (*3 complete model/specify in one go*)

| CompleteToSubpbl (*4 stop at the next begin of a subproblem,

                     if none, complete the actual (sub)problem*)

| CompleteSubpbl   (*5 complete the actual (sub)problem (incl.ev.subproblems)*)

| CompleteCalc;    (*6 complete the calculation as a whole*)*)

fun autoCalculate (cI:calcID) auto =

 (let

    val pold = get_pos cI 1

    val x = autocalc [] pold (get_calc cI) auto

  in

	  case x of

	    ("ok", c, ptp as (_,p)) =>

	      (upd_calc cI (ptp, []); upd_ipos cI 1 p;

	       autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)

	  | ("end-of-calculation", c, ptp as (_,p)) =>

	      (upd_calc cI (ptp, []); upd_ipos cI 1 p;

	       autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)

	  | (str, _, _) => autocalculateERROR2xml cI str

  end)

  handle _ => sysERROR2xml cI "error in kernel";

(* val (cI:calcID, ichd as ((p,_),_,_,_,_):icalhd) =

       (1, (([],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", ["maximum_of","function"],

		   ["DiffApp","max_by_calculus"])));

 val (cI:calcID, ichd as ((p,_),_,_,_,_):icalhd) =

       (1, (([],Pbl),"solve (x+1=2, x)",

		  [Given ["equality (x+1=2)", "solveFor x"],

		   Find ["solutions L"]],

		  Pbl,

		  ("Test", ["linear","univariate","equation","test"],

		   ["Test","solve_linear"])));

 val (cI:calcID, ichd as ((p,_),_,_,_,_):icalhd) =

       (1, (([],Pbl),"solveTest (1+-1*2+x=0,x)", [], Pbl, ("", [], [])));

 val (cI, p:pos')=(1, ([1],Frm));

 val (cI, p:pos')=(1, ([1,2,1,3],Res)); 

   *)

fun getTactic cI (p:pos') =

    (let val ((pt,_),_) = get_calc cI

	 val (form, tac, asms) = pt_extract (pt, p)

    in case tac of

(* val SOME ta = tac;

   *)

	   SOME ta => gettacticOK2xml cI ta

	 | NONE => gettacticERROR2xml cI ("no tactic at position "^pos'2str p)

     end)

    handle _ => sysERROR2xml cI "syserror in getTactic";

(*. see ICalcIterator#fetchApplicableTactics

 @see #TACTICS_ALL

 @see #TACTICS_CURRENT_THEORY

 @see #TACTICS_CURRENT_METHOD  ..the only impl.WN040307.*)

(*. fetch tactics to be applied to a particular step.*)

(* WN071231 kept this version for later parametrisation*)

(*.version 1: fetch _all_ tactics from script .*)

fun fetchApplicableTactics cI (scope:int) (p:pos') =

    (let val ((pt, _), _) = get_calc cI

    in (applicabletacticsOK cI (sel_rules pt p))

       handle PTREE str => sysERROR2xml cI str 

     end)

    handle _ => sysERROR2xml cI "error in kernel";

(*WN120611 took version 1 again

  version 2: fetch _applicable_ _elementary_ (ie. recursively 

              decompose rule-sets) Rewrite*, Calculate

fun fetchApplicableTactics cI (scope:int) (p:pos') =

    (let val ((pt, _), _) = get_calc cI

    in (applicabletacticsOK cI (sel_appl_atomic_tacs pt p))

       handle PTREE str => sysERROR2xml cI str 

     end)

    handle _ => sysERROR2xml cI "error in kernel";

*)

fun getAssumptions cI (p:pos') =

    (let val ((pt,_),_) = get_calc cI

	 val (_, _, asms) = pt_extract (pt, p)

     in getasmsOK2xml cI asms end)

    handle _ => sysERROR2xml cI "syserror in getAssumptions";

(*WN0502 @see ME/ctree: type asms: illdesigned, thus no positions returned*)

fun getAccumulatedAsms cI (p:pos') =

    (let val ((pt, _), _) = get_calc cI

	 val ass = get_assumptions_ pt p

     in (*getaccuasmsOK2xml cI (get_assumptions_ pt p)*)

     getasmsOK2xml cI ass end)

    handle _ => sysERROR2xml cI "syserror in getAccumulatedAsms";

(*since moveActive* does NOT transfer pos java --> sml (only sml --> java)

  refFormula might become involved in far-off errors !!!*)

fun refFormula cI (p:pos') = (*WN0501 rename to 'fun getElement' !*)

(* val (cI, uI) = (1,1);

   *)

    (let val ((pt,_),_) = get_calc cI

	 val (form, tac, asms) = pt_extract (pt, p)

    in refformulaOK2xml cI p form end)

    handle _ => sysERROR2xml cI "error in kernel";

(*.get formulae 'from' 'to' w.r.t. ordering in Position#compareTo(Position p); 

   in case of CalcHeads only the headline is taken

   (the pos' allows distinction between PrfObj and PblObj anyway);

   'level' is adjusted such that an 'interval' of formulae is returned;

   'from' 'to' are designed for use by iterators of calcChangedEvent;

   thus 'from' is the last unchanged position.*)

fun getFormulaeFromTo cI (from as ([],Pbl):pos') (to as ([],Pbl):pos')_ false =

(*special case because 'from' is _before_ the first elements to be returned*)

(* val (cI, from, to, level) = (1, ([],Pbl), ([],Pbl), 1);

   *)

    ((let val ((pt,_),_) = get_calc cI

	val (ModSpec (_,_,headline,_,_,_),_,_) = pt_extract (pt, to)

    in getintervalOK cI [(to, headline)] end)

    handle _ => sysERROR2xml cI "error in kernel")

  | getFormulaeFromTo cI (from as ([],Pbl):pos') (to as ([],Met):pos')_ false =

    getFormulaeFromTo cI ([],Pbl) ([],Pbl) (~00000) false

  | getFormulaeFromTo cI (from:pos') (to:pos') level false =

(* val (cI, from, to, level) = (1, unc, gen, 0);

   val (cI, from, to, level) = (1, unc, gen, 1);

   val (cI, from, to, level) = (1, ([],Pbl), ([],Met), 1);

   *)

    (if from = to then sysERROR2xml cI "getFormulaeFromTo: From = To"

     else

	 (case from of

	      ([],Res) => sysERROR2xml cI "getFormulaeFromTo does: moveDown \

					  \from=([],Res) .. goes beyond result"

	    | _ => let val ((pt,_),_) = get_calc cI

		       val f = move_dn [] pt from

		       fun max (a,b) = if a < b then b else a

		       (*must reach margins ...*)

		       val lev = max (level, max (lev_of from, lev_of to))

		   in getintervalOK cI (get_interval f to lev pt) end)

	 handle _ => sysERROR2xml cI "error in getFormulaeFromTo")

  | getFormulaeFromTo cI from to level true =

    sysERROR2xml cI "getFormulaeFromTo impl.for formulae only,\

		    \i.e. last arg only impl. for false, _NOT_ true";

(* val (cI, ip) = (1, ([1,9], Res));

   val (cI, ip) = (1, ([], Res));

   val (cI, ip) = (1, ([2], Res));

   val (cI, ip) = (1, ([3,1], Res));

   val (cI, ip) = (1, ([1,2,1], Res));

   *)

fun interSteps cI ip =

    (let val ((pt,p), tacis) = get_calc cI

     in if (not o is_interpos) ip

	then interStepsERROR cI "only formulae with position (_,Res) \

				\may have intermediate steps above them"

	else let val ip' = lev_pred' pt ip

(* val (str, pt', lastpos) = detailstep pt ip;

   *)

	     in case detailstep pt ip of

		    ("detailrls", pt(*, pos'forms*), lastpos) =>

		    (upd_calc cI ((pt, p), tacis);

		     interStepsOK cI (*pos'forms*) ip' ip' lastpos)

		  | ("no-Rewrite_Set...", _, _) =>

		    sysERROR2xml cI "no Rewrite_Set..."

		  | (_, _(*, pos'formshds*), lastpos) =>

		    interStepsOK cI (*pos'formshds*) ip' ip' lastpos

	     end

     end)

    handle _ => sysERROR2xml cI "error in kernel";

fun modifyCalcHead (cI:calcID) (ichd as ((p,_),_,_,_,_):icalhd) =

    (let val ((pt,_),_) = get_calc cI

	val (pt, chd as (_,p_,_,_,_,_)) = input_icalhd pt ichd

    in (upd_calc cI ((pt, (p,p_)), []); 

	modifycalcheadOK2xml cI chd) end)

    handle _ => sysERROR2xml cI "error in kernel";

(*.at the activeFormula set the Model, the Guard and the Specification 

   to empty and return a CalcHead;

   the 'origin' remains (for reconstructing all that).*)

fun resetCalcHead (cI:calcID) = 

    (let val (ptp,_) = get_calc cI

	val ptp = reset_calchead ptp

    in (upd_calc cI (ptp, []); 

	modifycalcheadOK2xml cI (get_ocalhd ptp)) end)

    handle _ => sysERROR2xml cI "error in kernel";

(*.at the activeFormula insert all the Descriptions in the Model 

   (_not_ in the Guard) and return a CalcHead;

   the Descriptions are for user-guidance; the rest of the items 

   are left empty for user-input; 

   includes a resetCalcHead for the Model and the Guard.*)

fun modelProblem (cI:calcID) = 

    (let val (ptp, _) = get_calc cI

	val ptp = reset_calchead ptp

	val (_, _, ptp) = nxt_specif Model_Problem ptp

    in (upd_calc cI (ptp, []); 

	modifycalcheadOK2xml cI (get_ocalhd ptp)) end)

    handle _ => sysERROR2xml cI "error in kernel";

(* set the UContext determined on a knowledgebrowser to the current calc *)

fun setContext (cI:calcID) (ip as (_,p_):pos') (guh:guh) =

  (case (implode o (take_fromto 1 4) o Symbol.explode) guh of 

     "thy_" =>

	     if member op = [Pbl,Met] p_

       then message2xml cI "thy-context not to calchead"

       else if ip = ([],Res) then message2xml cI "no thy-context at result"

	     else if no_thycontext guh then message2xml cI ("no thy-context for '" ^ guh ^ "'")

  	   else 

         let

           val (ptp as (pt, pold), _) = get_calc cI

		       val is = get_istate pt ip

		       val subs = subs_from is "dummy" guh

		       val tac = guh2rewtac guh subs

  	     in 

           case locatetac tac (pt, ip) of (*='fun setNextTactic'+step*)

		         ("ok", (tacis, c, ptp as (_,p))) =>

		           (upd_calc cI ((pt,p), []); 

		            autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)

		       | ("unsafe-ok", (tacis, c, ptp as (_,p))) =>

  		         (upd_calc cI ((pt,p), []); 

	  	          autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)

		       | ("end-of-calculation",_) => message2xml cI "end-of-calculation"

		       | ("failure",_) => sysERROR2xml cI "failure"

		       | ("not-applicable",_) => (*the rule comes from anywhere..*)

		           (case applicable_in ip pt tac of 

		              Notappl e => message2xml cI ("'" ^ tac2str tac ^ "' not-applicable")

	              | Appl m => 

		                let

                      val ctxt = get_ctxt pt pold

                      val (p,c,_,pt) =

                        generate1 (assoc_thy "Isac") m (Uistate, ctxt) ip pt

                    in upd_calc cI ((pt,p),[]);

	                  autocalculateOK2xml cI pold (if null c then pold else last_elem c) p

		  	            end)

	       end

   | "pbl_" =>

	     let

         val pI = guh2kestoreID guh

	       val ((pt, _), _) = get_calc cI

	       in

           if member op = [Pbl, Met] p_ 

	         then

             let val (pt, chd) = set_problem pI (pt, ip)

		         in (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end

	         else sysERROR2xml cI "setContext for pbl requires ActiveFormula on CalcHead"

	     end

   | "met_" =>

	     let

         val mI = guh2kestoreID guh

	       val ((pt, _), _) = get_calc cI

	       in

           if member op = [Pbl, Met] p_

	         then

             let val (pt, chd) = set_method mI (pt, ip)

		         in (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end

	         else sysERROR2xml cI "setContext for met requires ActiveFormula on CalcHead"

	       end)

   handle _ => sysERROR2xml cI "error in kernel";

(*.specify the Method at the activeFormula and return a CalcHead

   containing the Guard.

   WN0512 impl.incomplete, see 'nxt_specif (Specify_Method '.*)

fun setMethod (cI:calcID) (mI:metID) = 

(* val (cI, mI) = (1, ["Test","solve_linear"]);

   *)

    (let val ((pt, _), _) = get_calc cI

	val ip as (_, p_) = get_pos cI 1

    in if member op = [Pbl,Met] p_ 

       then let val (pt, chd) = set_method mI (pt, ip)

	    in (upd_calc cI ((pt, ip), []);

		modifycalcheadOK2xml cI chd) end

       else sysERROR2xml cI "setMethod requires ActiveFormula on CalcHead"

 end)

    handle _ => sysERROR2xml cI "error in kernel";

(*.specify the Problem at the activeFormula and return a CalcHead

   containing the Model; special case of checkContext;

   WN0512 impl.incomplete, see 'nxt_specif (Specify_Problem '.*)

fun setProblem (cI:calcID) (pI:pblID) =

    (let val ((pt, _), _) = get_calc cI

	val ip as (_, p_) = get_pos cI 1

    in if member op = [Pbl,Met] p_

       then let val (pt, chd) = set_problem pI (pt, ip)

	    in (upd_calc cI ((pt, ip), []);

		modifycalcheadOK2xml cI chd) end

       else sysERROR2xml cI "setProblem requires ActiveFormula on CalcHead"

 end)

    handle _ => sysERROR2xml cI "error in kernel";

(*.specify the Theory at the activeFormula and return a CalcHead;

   special case of checkContext;

   WN0512 impl.incomplete, see 'nxt_specif (Specify_Method '.*)

fun setTheory (cI:calcID) (tI:thyID) =

    (let val ((pt, _), _) = get_calc cI

	val ip as (_, p_) = get_pos cI 1

    in if member op = [Pbl,Met] p_

       then let val (pt, chd) = set_theory tI (pt, ip)

	    in (upd_calc cI ((pt, ip), []);

		modifycalcheadOK2xml cI chd) end

       else sysERROR2xml cI "setProblem requires ActiveFormula on CalcHead"

 end)

    handle _ => sysERROR2xml cI "error in kernel";

(**. without update of CalcTree .**)

(*.match the model of a problem at pos p 

   with the model-pattern of the problem with pblID*)

(*fun tryMatchProblem cI pblID =

    (let val ((pt,_),_) = get_calc cI

	 val p = get_pos cI 1

	 val chd = trymatch pblID pt p

    in trymatchOK2xml cI chd end)

    handle _ => sysERROR2xml cI "error in kernel";*)

(*.refinement for the parent-problem of the position.*)

(* val (cI, (p,p_), guh) = (1, ([1],Res), "pbl_equ_univ");

   *)

fun refineProblem cI ((p,p_) : pos') (guh : guh) =

    (let val pblID = guh2kestoreID guh

	 val ((pt,_),_) = get_calc cI

	 val pp = par_pblobj pt p

	 val chd = tryrefine pblID pt (pp, p_)

    in matchpbl2xml cI chd end)

    handle _ => sysERROR2xml cI "error in kernel";

(* append a formula to the calculation *)

fun appendFormula cI (ifo:cterm') =

  (let

    val cs = get_calc cI

    val pos as (_,p_) = get_pos cI 1

  in

    case step pos cs of

	    ("ok", cs') =>

	      (case inform cs' (encode ifo) of

	        ("ok", (_(*use in DG !!!*), c, ptp as (_,p))) =>

	          (upd_calc cI (ptp, []); upd_ipos cI 1 p;

	          appendformulaOK2xml cI pos (if null c then pos else last_elem c) p)

	      | ("same-formula", (_, c, ptp as (_,p))) =>

	          (upd_calc cI (ptp, []); upd_ipos cI 1 p;

	          appendformulaOK2xml cI pos (if null c then pos else last_elem c) p)

	      | (msg, _) => appendformulaERROR2xml cI msg)

	  | (msg, cs') => appendformulaERROR2xml cI msg

  end)

  handle _ => sysERROR2xml cI "error in kernel";

(* replace a formula with_in_ a calculation;

   this situation applies for initial CAS-commands, too *)

fun replaceFormula cI (ifo:cterm') =

 (let

    val ((pt, _), _) = get_calc cI

    val p = get_pos cI 1

  in

    case inform (([], [], (pt, p)): calcstate') (encode ifo) of

	    ("ok", (_(*tacs used for DG ?*), c, ptp' as (pt',p'))) =>

	      let

	        val unc = if null (fst p) then p else move_up [] pt p

	        val _ = upd_calc cI (ptp', [])

	        val _ = upd_ipos cI 1 p'

	      in replaceformulaOK2xml cI unc (if null c then unc else last_elem c) p' end

	  | ("same-formula", _) => replaceformulaERROR2xml cI "formula not changed"

	  | (msg, _) => replaceformulaERROR2xml cI msg

  end)

    handle _ => sysERROR2xml cI "error in kernel";

(***. CalcIterator

    moveActive*: set the pos' of the active formula stored with the calctree

                 could take pos' as argument for consistency checks

    move*:       compute the new iterator from the old one on the fly

.***)

fun moveActiveRoot cI =

    (let val _ = upd_ipos cI 1 ([],Pbl)

    in iteratorOK2xml cI ([],Pbl) end)

    handle e => sysERROR2xml cI "error in kernel";

fun moveRoot cI =

    (iteratorOK2xml cI ([],Pbl))

    handle e => sysERROR2xml cI "";

fun moveActiveRootTEST cI =

    (let val _ = upd_ipos cI 1 ([],Pbl)

    in (*iteratorOK2xml cI ([],Pbl)*)() end)

    handle e => sysERROR2xml cI "error in kernel";

(* val (cI, uI) = (1,1);

   val (cI, uI) = (1,2);

   *)

fun moveActiveDown cI =

    ((let val ((pt,_),_) = get_calc cI

(* val (P, (Nd (_, ns)), (p::(ps as (_::_)), p_)) =([]:pos, pt, get_pos cI uI);

   val (P, (Nd (c, ns)), ([p], p_))               =([]:pos, pt, get_pos cI uI);

   print_depth 7;pt

   *)

	  val ip' = move_dn [] pt (get_pos cI 1)

	  val _ = upd_ipos cI 1 ip'

      in iteratorOK2xml cI ip' end)

     handle (PTREE e) => iteratorERROR2xml cI)

    handle _ => sysERROR2xml cI "error in kernel";

fun moveDown cI (p:pos') =

    ((let val ((pt,_),_) = get_calc cI

(* val (P, (Nd (_, ns)), (p::(ps as (_::_)), p_)) =([]:pos, pt, get_pos cI uI);

   val (P, (Nd (c, ns)), ([p], p_))               =([]:pos, pt, get_pos cI uI);

   print_depth 7;pt

   *)

	  val ip' = move_dn [] pt p

      in iteratorOK2xml cI ip' end)

     handle (PTREE e) => iteratorERROR2xml cI)

    handle _ => sysERROR2xml cI "error in kernel";

fun moveActiveDownTEST cI =

    let val ((pt,_),_) = get_calc cI

	val ip = get_pos cI 1

	  val ip' = (move_dn [] pt ip)

	      handle _ => ip

	  val _ = upd_ipos cI 1 ip'

      in (*iteratorOK2xml cI uI*)() end;

fun moveActiveLevelDown cI =

    ((let val ((pt,_),_) = get_calc cI

	  val ip' = movelevel_dn [] pt (get_pos cI 1)

	  val _ = upd_ipos cI 1 ip'

      in iteratorOK2xml cI ip' end)

     handle (PTREE e) => iteratorERROR2xml cI)

    handle _ => sysERROR2xml cI "error in kernel";

fun moveLevelDown cI (p:pos') =

    ((let val ((pt,_),_) = get_calc cI

	  val ip' = movelevel_dn [] pt p

      in iteratorOK2xml cI ip' end)

     handle (PTREE e) => iteratorERROR2xml cI)

    handle _ => sysERROR2xml cI "error in kernel";

fun moveActiveUp cI =

    ((let val ((pt,_),_) = get_calc cI

	  val ip' = move_up [] pt (get_pos cI 1)

	  val _ = upd_ipos cI 1 ip'

      in iteratorOK2xml cI ip' end)

     handle PTREE e => iteratorERROR2xml cI)

    handle _ => sysERROR2xml cI "error in kernel";

fun moveUp cI (p:pos') =

    ((let val ((pt,_),_) = get_calc cI

	  val ip' = move_up [] pt p

      in iteratorOK2xml cI ip' end)

     handle PTREE e => iteratorERROR2xml cI)

    handle _ => sysERROR2xml cI "error in kernel";

fun moveActiveLevelUp cI =

    ((let val ((pt,_),_) = get_calc cI

	  val ip' = movelevel_up [] pt (get_pos cI 1)

	  val _ = upd_ipos cI 1 ip'

      in iteratorOK2xml cI ip' end)

     handle PTREE e => iteratorERROR2xml cI)

    handle _ => sysERROR2xml cI "error in kernel";

fun moveLevelUp cI (p:pos') =

    ((let val ((pt,_),_) = get_calc cI

	  val ip' = movelevel_up [] pt p

      in iteratorOK2xml cI ip' end)

     handle PTREE e => iteratorERROR2xml cI)

    handle _ => sysERROR2xml cI "error in kernel";

fun moveActiveCalcHead cI =

    ((let val ((pt,_),_) = get_calc cI

	  val ip' = movecalchd_up pt (get_pos cI 1)

	  val _ = upd_ipos cI 1 ip'

      in iteratorOK2xml cI ip' end)

     handle PTREE e => iteratorERROR2xml cI)

    handle _ => sysERROR2xml cI "error in kernel";

fun moveCalcHead cI (p:pos') =

    ((let val ((pt,_),_) = get_calc cI

	  val ip' = movecalchd_up pt p

      in iteratorOK2xml cI ip' end)

     handle PTREE e => iteratorERROR2xml cI)

    handle _ => sysERROR2xml cI "error in kernel";

(*.initContext Thy_ is conceptually impossible at [Pbl,Met] 

   and at positions with Check_Postcond and End_Trans;

   at possible pos's there can be NO rewrite (returned as a context, too).*)

(* val (cI, Thy_, (pos as (p,p_):pos')) = (1, Thy_, ([1], Frm));

   val (cI, Thy_, (pos as (p,p_):pos')) = (1, Thy_, ([], Res));

   val (cI, Thy_, (pos as (p,p_):pos')) = (1, Thy_, ([2], Res));

   val (cI, Thy_, (pos as (p,p_):pos')) = (1, Thy_, ([1,1], Frm));

   *)

fun initContext (cI:calcID) Thy_ (pos as (p,p_):pos') =

    ((if member op = [Pbl,Met] p_

      then message2xml cI "thy-context not to calchead"

      else if pos = ([],Res) then message2xml cI "no thy-context at result"

      else let val cs as (ptp as (pt,_),_) = get_calc cI

	   in if exist_lev_on' pt pos

	      then let val pos' = lev_on' pt pos

		       val tac = get_tac_checked pt pos'

		   in if is_rewtac tac 

		      then contextthyOK2xml cI (context_thy (pt,pos) tac)

		      else message2xml cI ("no thy-context at tac '" ^

					   tac2str tac ^ "'")

		   end

	      else if is_curr_endof_calc pt pos

	      then case step pos cs of

(* val (str, (tacis, _, (pt,_))) = step pos cs;

   val ("ok", (tacis, _, (pt,_))) = step pos cs;

   *)

		       ("ok", (tacis, _, (pt,_))) =>

		       let val tac = fst3 (last_elem tacis)

		       in if is_rewtac tac 

			  then contextthyOK2xml 

				   cI (context_thy ptp tac)

			  else message2xml cI ("no thy-context at tac '" ^

					       tac2str tac ^ "'")

		       end

		     | (msg, _) => message2xml cI msg

	      else message2xml cI "no thy-context at this position"

	   end)

     handle _ => sysERROR2xml cI "error in kernel")

(* val (cI, Pbl_, pos as (p,p_)) = (1, Pbl_, ([],Pbl));

   *)

  | initContext cI Pbl_ (pos as (p,p_):pos') = 

    ((let val ((pt,_),_) = get_calc cI

	  val pp = par_pblobj pt p

	  val chd = initcontext_pbl pt (pp,p_)

      in matchpbl2xml cI chd end)

     handle _ => sysERROR2xml cI "error in kernel")

  | initContext cI Met_ (pos as (p,p_):pos') =

    ((let val ((pt,_),_) = get_calc cI

	  val pp = par_pblobj pt p

	  val chd = initcontext_met pt (pp,p_)

      in matchmet2xml cI chd end)

     handle _ => sysERROR2xml cI "error in kernel");

(* match a theorem, a ruleset (etc., selected in the knowledge-browser)

  with the formula in the focus on the worksheet;

  string contains the thy, thus it is unique as thmID, rlsID for this thy;

  take the substitution from the istate of the formula *)

(* use"../smltest/Knowledge/poly.sml";

   val (cI, pos as (p,p_), guh) = (1, ([1,1,1], Frm), "thy_Poly-thm-real_diff_minus");

   val (cI, pos as (p,p_), guh) = (1, ([1,1], Frm), "norm_Poly");

   val (cI, pos as (p,p_), guh) = (1, ([1], Res), "thy_isac_Test-rls-Test_simplify");

   *)

fun checkContext (cI:calcID) (pos:pos' as (p,p_)) (guh:guh) =

    (case (implode o (take_fromto 1 4) o Symbol.explode) guh of

	 "thy_" =>

	 if member op = [Pbl,Met] p_

         then message2xml cI "thy-context not to calchead"

	 else if pos = ([],Res) then message2xml cI "no thy-context at result"

	 else if no_thycontext guh then message2xml cI ("no thy-context for '"^

							guh ^ "'")

	 else let val (ptp as (pt,_),_) = get_calc cI

		  val is = get_istate pt pos

		  val subs = subs_from is "dummy" guh

		  val tac = guh2rewtac guh subs

	      in contextthyOK2xml cI (context_thy (pt, pos) tac) end

       (*.match the model of a problem at pos p 

          with the model-pattern of the problem with pblID.*)

(* val (cI, pos:pos' as (p,p_), guh) =

       (1, p, kestoreID2guh Pbl_ ["univariate","equation"]);

   val (cI, pos:pos' as (p,p_), guh) =

       (1, ([],Pbl), kestoreID2guh Pbl_ ["univariate","equation"]);

   val (cI, pos:pos' as (p,p_), guh) =

       (1, ([],Pbl), "pbl_equ_univ");

   *)

       | "pbl_" => 

	 let val ((pt,_),_) = get_calc cI

	     val pp = par_pblobj pt p

	     val keID = guh2kestoreID guh

	     val chd = context_pbl keID pt pp

	 in matchpbl2xml cI chd end

(* val (cI, pos:pos' as (p,p_), guh) = 

       (1, ([],Pbl), kestoreID2guh Met_ ["LinEq", "solve_lineq_equation"]);

   *)

       | "met_" => 

	 let val ((pt,_),_) = get_calc cI

	     val pp = par_pblobj pt p

	     val keID = guh2kestoreID guh

	     val chd = context_met keID pt pp

	 in matchmet2xml cI chd end)

    handle _ => sysERROR2xml cI "error in kernel";

(* for an errpatID find "(fillpatID, fillform)" list 

  which dedicated to this errpat and which is applicable at current formula*)

fun findFillpatterns cI errpatID = 

  let

    val ((pt, _), _) = get_calc cI

		    val pos = get_pos cI 1;

		    val fillpats = find_fillpatterns (pt, pos) errpatID

			  in findFillpatterns2xml cI (map #1 fillpats) end;

(* given a fillpatID propose a fillform to the learner on the worksheet;

  the "ctree" is extended with fillpat and "ostate Inconsistent",

  the "istate" is copied and NOT updated;

  returns CalcChanged.

  arg errpatID: required because there is no dialog-related state in the math-kernel.

*)

fun requestFillformula cI (errpatID, fillpatID) =

  let

    val ((pt, _), _) = get_calc cI

		val pos = get_pos cI 1

    val fillforms = find_fillpatterns (pt, pos) errpatID 

  in

    case filter ((curry op = fillpatID) o 

        (#1: (fillpatID * term * thm * (subs option) -> fillpatID))) fillforms of

      (_, fillform, thm, sube_opt) :: _ =>

        let

          val (pt, pos') = generate_inconsistent_rew (sube_opt, thm'_of_thm thm)

            fillform (get_loc pt pos) pos pt

        in

          (upd_calc cI ((pt, pos'), []); (*upd_ipos cI 1 pos';*)

           autocalculateOK2xml cI pos pos' pos')

        end

    | _ => autocalculateERROR2xml cI "no fillpattern found"    

  end;    

(* input a formula which exactly fills the gaps in a "fillformula"

   presented to the learner immediately before by "requestFillformula (errpatID, fillpatID)":

   errpatID: lhs of the respective thm = lhs of fillformula with fillpatID.

   The respective thm is stored in the ctree. *)

fun inputFillFormula cI ifo =

  let

    val ((pt, _), _) = get_calc cI

    val pos = get_pos cI 1;

  in

    case is_exactly_equal (pt, pos) ifo of

      ("ok", tac) =>

        let

        in (* cp from applyTactic *)

          case locatetac tac (pt, pos) of

            ("ok", (_, c, ptp as (_,p'))) =>

              (upd_calc cI (ptp, []);

               upd_ipos cI 1 p';

               autocalculateOK2xml cI pos (if null c then p' else last_elem c) p')

          | ("unsafe-ok", (_, c, ptp as (_,p'))) =>

              (upd_calc cI (ptp, []);

               upd_ipos cI 1 p';

               autocalculateOK2xml cI pos (if null c then p' else last_elem c) p')

          | ("end-of-calculation", (_, c, ptp as (_,p'))) =>

              (upd_calc cI (ptp, []);

               upd_ipos cI 1 p';

               autocalculateOK2xml cI pos (if null c then p' else last_elem c) p')

          | (str,_) => autocalculateERROR2xml cI "failure"

        end

    | (msg, _) => message2xml cI msg

 end

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

end

open interface;

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