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

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

   This is the only file which does not adhere to Isabelle coding standards,

   rather the function names are according to the respective Java methods.

   authors: Walther Neuper 2002

   (c) due to copyright terms

use"Frontend/interface.sml";

use"interface.sml";

*)

signature KERNEL =

  sig

    val appendFormula : calcID -> cterm' -> XML.tree (*unit future*)

    val autoCalculate : calcID -> auto -> XML.tree (*unit future*)

    val applyTactic : calcID -> pos' -> tac -> XML.tree

    val CalcTree : fmz list -> XML.tree

    val checkContext : calcID -> pos' -> guh -> XML.tree

    val DEconstrCalcTree : calcID -> XML.tree

    val fetchApplicableTactics : calcID -> int -> pos' -> XML.tree

    val fetchProposedTactic : calcID -> XML.tree

    val findFillpatterns : calcID -> errpatID -> XML.tree

    val getAccumulatedAsms : calcID -> pos' -> XML.tree

    val getActiveFormula : calcID -> XML.tree

    val getAssumptions : calcID -> pos' -> XML.tree

    val getFormulaeFromTo : calcID -> pos' -> pos' -> int -> bool -> XML.tree

    val getTactic : calcID -> pos' -> XML.tree

    val initContext : calcID -> ketype -> pos' -> XML.tree

    val inputFillFormula: calcID -> string -> XML.tree

    val interSteps : calcID -> pos' -> XML.tree

    val Iterator : calcID -> XML.tree

    val IteratorTEST : calcID -> iterID

    val modelProblem : calcID -> XML.tree

    val modifyCalcHead : calcID -> Inform.icalhd -> XML.tree

    val moveActiveCalcHead : calcID -> XML.tree

    val moveActiveDown : calcID -> XML.tree

    val moveActiveFormula : calcID -> pos' -> XML.tree

    val moveActiveLevelDown : calcID -> XML.tree

    val moveActiveLevelUp : calcID -> XML.tree

    val moveActiveRoot : calcID -> XML.tree

    val moveActiveRootTEST : calcID -> XML.tree

    val moveActiveUp : calcID -> XML.tree

    val moveCalcHead : calcID -> pos' -> XML.tree

    val moveDown : calcID -> pos' -> XML.tree

    val moveLevelDown : calcID -> pos' -> XML.tree

    val moveLevelUp : calcID -> pos' -> XML.tree

    val moveRoot : calcID -> XML.tree

    val moveUp : calcID -> pos' -> XML.tree

    val refFormula : calcID -> pos' -> XML.tree

    val refineProblem : calcID -> pos' -> guh -> XML.tree

    val replaceFormula : calcID -> cterm' -> XML.tree

    val requestFillformula : calcID -> errpatID * fillpatID -> XML.tree

    val resetCalcHead : calcID -> XML.tree

    val setContext : calcID -> pos' -> guh -> XML.tree

    val setMethod : calcID -> metID -> XML.tree

    val setNextTactic : calcID -> tac -> XML.tree

    val setProblem : calcID -> pblID -> XML.tree

    val setTheory : calcID -> thyID -> XML.tree

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

    (* NONE *)

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

  end

(**)

structure Kernel(**): KERNEL(**) =

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 en/decode" in xmlsrc/mathml.sml *)

fun encode_imodel (imodel : Inform.imodel) =

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

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

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

  in map enc imodel:Inform.imodel end;

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

  (pos', encode headl, encode_imodel imodel, pos_, spec) : Inform.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 1";

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

(*.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 = Chead.nxt_specify_init_calc (encode_fmz (fmz, sp))

  	    val cI = add_calc cs (*FIXME.WN.8.03: error-handling missing*)

  	   in calctreeOK2xml cI end)

  	 handle _ => sysERROR2xml 0 "error in kernel 2")

	| CalcTree [] = error "CalcTree: called with []"

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

fun setNextTactic (cI:calcID) tac =

  let

    val ((pt, _), _) = get_calc cI                     (* retrieve calcstate from states *)

    val ip = get_pos cI 1                              (* retrieve position from states  *)

  in

    case Math_Engine.locatetac tac (pt, ip) of                               

      ("ok", (tacis, _, _)) =>                         (* update calcstate in states     *)

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

  	| (msg, _) => sysERROR2xml cI ("setNextTactic: locatetac returns " ^ msg)

  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 Math_Engine.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 ("applyTactic: locatetac returns " ^ str)

  end;

fun fetchProposedTactic (cI:calcID) =

  (case Math_Engine.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 (Inform.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 3";

fun autoCalculate (cI:calcID) auto = (*Future.fork

  (fn () => (( *)let

     val pold = get_pos cI 1

     val x = Math_Engine.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 ERROR msg => sysERROR2xml cI ("error in kernel 4: " ^ msg)(* )) *);

fun getTactic cI (p:pos') =

  (let 

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

    val (_, tac, _) = Chead.pt_extract (pt, p)

  in 

    case tac of

 	    SOME ta => gettacticOK2xml cI ta

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

  end)

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

(* Fetch tactics to be applied to a particular step.

  Requirements are not yet implemented, see ICalcIterator#fetchApplicableTactics"

    @see #TACTICS_ALL

    @see #TACTICS_CURRENT_THEORY

    @see #TACTICS_CURRENT_METHOD  ..the only impl.WN040307

  Lucin.sel_appl_atomic_tacs waits to be used here

*)

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

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

  in (applicabletacticsOK cI (Lucin.sel_rules pt p))

     handle PTREE str => sysERROR2xml cI str

  end)

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

fun getAssumptions cI (p:pos') =

  (let 

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

	  val (_, _, asms) = Chead.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 getasmsOK2xml cI ass end)

    handle _ => sysERROR2xml cI "syserror in getAccumulatedAsms"

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

  (let 

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

	  val (form, _, _) = Chead.pt_extract (pt, p)

  in refformulaOK2xml cI p form end)

    handle _ => sysERROR2xml cI ("error in kernel 6: refFormula " ^ int2str cI ^ " " ^ pos'2str p)

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

   "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 (([], Pbl) : pos') (to as ([], Pbl) : pos') _ false =

    ((let 

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

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

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

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

  | getFormulaeFromTo cI ([], Pbl) ([], Met) _ false =

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

  (* ^^^ separated cases, because "from" is _before_ the first elements to be returned*)

  | getFormulaeFromTo cI from to level false =

    (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

           val lev = max (level, max (lev_of from, lev_of to)) (*... must reach margins *)

         in getintervalOK cI (Chead.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");

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

      in case Math_Engine.detailstep pt ip of

        ("detailrls", pt, lastpos) =>

          (upd_calc cI ((pt, p), tacis); interStepsOK cI ip' ip' lastpos)

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

      | (_, _, lastpos) => interStepsOK cI ip' ip' lastpos

      end

  end)

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

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

  (let 

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

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

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

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

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

  (let 

    val (ptp,_) = get_calc cI

    val ptp = Chead.reset_calchead ptp

  in (upd_calc cI (ptp, []); modifycalcheadOK2xml cI (Chead.get_ocalhd ptp)) end)

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

(* at the activeFormula insert all the Descriptions in the Model and return a CalcHead;

   the Descriptions are for user-guidance; the rest of the items are left empty for user-input *)

fun modelProblem cI =

  (let val (ptp, _) = get_calc cI

  	val ptp = Chead.reset_calchead ptp

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

  in (upd_calc cI (ptp, []); modifycalcheadOK2xml cI (Chead.get_ocalhd ptp)) end)

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

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

  WN0825: not implemented in isac-java.

  Recalling the state of development after summer-term 2006 (Robert Koenishofer et.al.):

  Main success was showing UContext from Worksheet to the Example/Method/Problem/TheoryBrowser,

  while the buttons on these browsers <To Worksheet> <Try Refine> have no

  code in isac-java (and only partial, untested code in isabisac).

*)

fun setContext cI (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 Rtools.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 = Rtools.subs_from is "dummy" guh

		      val tac = Rtools.guh2rewtac guh subs

  	    in

          case Math_Engine.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

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

	            | Chead.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

     ) handle _ => sysERROR2xml cI "setContext: thy_ ???")

  | "pbl_" =>

	  ((let

        val pI = guh2kestoreID guh

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

	    in

        if member op = [Pbl, Met] p_

	      then

          let val (pt, chd) = Math_Engine.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

    ) handle _ => sysERROR2xml cI "setContext: pbl_ ???")

  | "met_" =>

	  ((let

        val mI = guh2kestoreID guh

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

	    in

        if member op = [Pbl, Met] p_

	      then            

          let val (pt, chd) = Math_Engine.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 "setContext: met_ ???")

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

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

fun setMethod cI mI =

  (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) = Math_Engine.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 12";

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

  (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) = Math_Engine.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 13";

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

  (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) = Math_Engine.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 14";

(* refinement for the parent-problem of the position,

  Not used in isac-java (see comment WN0825 for setContext) but tryrefine is used within isabisac *)

fun refineProblem cI (p, p_) guh =

  (let 

    val pblID = guh2kestoreID guh

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

	  val pp = par_pblobj pt p

	  val chd = Math_Engine.tryrefine pblID pt (pp, p_)

  in contextpblOK2xml cI chd end)

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

(* append a formula to the calculation *)

fun appendFormula' cI (ifo:cterm') =

  (let

    val cs = get_calc cI

    val pos = get_pos cI 1

  in

    case Math_Engine.step pos cs of

	    ("ok", cs') =>

	      (case Inform.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, _) => appendformulaERROR2xml cI msg

  end)

  handle ERROR msg => sysERROR2xml cI ("error in kernel 17: " ^ msg);

fun appendFormula cI ifo = (*Future.fork (fn () => *)appendFormula' cI ifo(* ) *);

(* replace a formula with_in_ a calculation; this 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.inform (([], [], (pt, p)): Chead.calcstate') (encode ifo) of

	    ("ok", (_(*tacs used for DG ?*), c, ptp' as (_, 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 18";

(*** 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 _ => sysERROR2xml cI "error in kernel 19"

fun moveRoot cI =

  (iteratorOK2xml cI ([], Pbl))

  handle _ => sysERROR2xml cI "";

fun moveActiveRootTEST cI =

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

  in iteratorOK2xml cI ([], Pbl) end)

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

fun moveActiveDown cI =

  ((let 

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

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

	  val _ = upd_ipos cI 1 ip'

  in iteratorOK2xml cI ip' end)

    handle (PTREE _) => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 21"

fun moveDown cI p =

  ((let 

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

	  val ip' = move_dn [] pt p

  in iteratorOK2xml cI ip' end)

    handle (PTREE _) => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 22"

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 _) => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 23"

fun moveLevelDown cI p =

  ((let 

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

    val ip' = movelevel_dn [] pt p

  in iteratorOK2xml cI ip' end)

    handle (PTREE _) => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 24"

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 _ => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 25"

fun moveUp cI p =

  ((let 

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

	  val ip' = move_up [] pt p

  in iteratorOK2xml cI ip' end)

    handle PTREE _ => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 26"

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 _ => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 27"

fun moveLevelUp cI p =

  ((let

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

	  val ip' = movelevel_up [] pt p

  in iteratorOK2xml cI ip' end)

    handle PTREE _ => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 28"

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 _ => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 29"

fun moveCalcHead cI p =

  ((let

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

	  val ip' = movecalchd_up pt p

  in iteratorOK2xml cI ip' end)

    handle PTREE _ => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 30"

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

fun initContext cI 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 = Rtools.get_tac_checked pt pos'

            in

              if is_rewtac tac

              then contextthyOK2xml cI (Rtools.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 Math_Engine.step pos cs of

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

                let val tac = fst3 (last_elem tacis)

                in 

                  if is_rewtac tac

                  then contextthyOK2xml cI (Rtools.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 31")

  | initContext cI Pbl_ (p, p_) =

    ((let 

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

      val pp = par_pblobj pt p

      val chd = Math_Engine.initcontext_pbl pt (pp,p_)

    in contextpblOK2xml cI chd end)

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

  | initContext cI Met_ (p, p_) =

    ((let

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

      val pp = par_pblobj pt p

      val chd = Math_Engine.initcontext_met pt (pp,p_)

    in contextmetOK2xml cI chd end)

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

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

fun checkContext cI (pos as (p, p_)) 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 Rtools.no_thycontext guh then message2xml cI ("no thy-context for '" ^ guh ^ "'")

      else 

        ((let 

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

    		  val is = get_istate pt pos

    		  val subs = Rtools.subs_from is "dummy" guh

    		  val tac = Rtools.guh2rewtac guh subs

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

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

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

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

  | "pbl_" =>

	    ((let 

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

  	    val pp = par_pblobj pt p

  	    val keID = guh2kestoreID guh

  	    val chd = Math_Engine.context_pbl keID pt pp

	    in contextpblOK2xml cI chd end

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

   | "met_" =>

	     ((let 

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

	       val pp = par_pblobj pt p

	       val keID = guh2kestoreID guh

	       val chd = Math_Engine.context_met keID pt pp

	     in contextmetOK2xml cI chd end

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

   | str => sysERROR2xml cI ("checkContext: str = " ^ str)

(* 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 = Inform.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 = Inform.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 Inform.is_exactly_equal (pt, pos) ifo of

      ("ok", tac) =>

        let

        in (* cp from applyTactic *)

          case Math_Engine.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')

          | _ => autocalculateERROR2xml cI "failure"

        end

    | (msg, _) => message2xml cI msg

  end

(**)

end

(**)