neuper@37906: (* the interface between the isac-kernel and the java-frontend;
neuper@37906:    the isac-kernel holds calc-trees; stdout in XML-format.
neuper@37906:    authors: Walther Neuper 2002
neuper@37906:    (c) due to copyright terms
neuper@37906: 
neuper@37947: use"Frontend/interface.sml";
neuper@37906: use"interface.sml";
neuper@37906: *)
neuper@37906: 
neuper@37906: signature INTERFACE =
neuper@37906:   sig
neuper@37906:     val CalcTree : fmz list -> unit
neuper@37906:     val DEconstrCalcTree : calcID -> unit
neuper@37906:     val Iterator : calcID -> unit
neuper@37906:     val IteratorTEST : calcID -> iterID
neuper@37906:     val appendFormula : calcID -> cterm' -> unit
neuper@37906:     val autoCalculate : calcID -> auto -> unit
neuper@37906:     val checkContext : calcID -> pos' -> guh -> unit
neuper@37906:     val fetchApplicableTactics : calcID -> int -> pos' -> unit
neuper@37906:     val fetchProposedTactic : calcID -> unit
neuper@37906:     val applyTactic : calcID -> pos' -> tac -> unit
neuper@37906:     val getAccumulatedAsms : calcID -> pos' -> unit
neuper@37906:     val getActiveFormula : calcID -> unit
neuper@37906:     val getAssumptions : calcID -> pos' -> unit
neuper@37906:     val initContext : calcID -> ketype -> pos' -> unit
neuper@37906:     val getFormulaeFromTo : calcID -> pos' -> pos' -> int -> bool -> unit
neuper@37906:     val getTactic : calcID -> pos' -> unit
neuper@37906:     val interSteps : calcID -> pos' -> unit
neuper@37906:     val modifyCalcHead : calcID -> icalhd -> unit
neuper@37906:     val moveActiveCalcHead : calcID -> unit
neuper@37906:     val moveActiveDown : calcID -> unit
neuper@37906:     val moveActiveDownTEST : calcID -> unit
neuper@37906:     val moveActiveFormula : calcID -> pos' -> unit
neuper@37906:     val moveActiveLevelDown : calcID -> unit
neuper@37906:     val moveActiveLevelUp : calcID -> unit
neuper@37906:     val moveActiveRoot : calcID -> unit
neuper@37906:     val moveActiveRootTEST : calcID -> unit
neuper@37906:     val moveActiveUp : calcID -> unit
neuper@37906:     val moveCalcHead : calcID -> pos' -> unit
neuper@37906:     val moveDown : calcID -> pos' -> unit
neuper@37906:     val moveLevelDown : calcID -> pos' -> unit
neuper@37906:     val moveLevelUp : calcID -> pos' -> unit
neuper@37906:     val moveRoot : calcID -> unit
neuper@37906:     val moveUp : calcID -> pos' -> unit
neuper@37906:     val refFormula : calcID -> pos' -> unit
neuper@37906:     val replaceFormula : calcID -> cterm' -> unit
neuper@37906:     val resetCalcHead : calcID -> unit
neuper@37906:     val modelProblem : calcID -> unit
neuper@37906:     val refineProblem : calcID -> pos' -> guh -> unit
neuper@37906:     val setContext : calcID -> pos' -> guh -> unit
neuper@37906:     val setMethod : calcID -> metID -> unit
neuper@37906:     val setNextTactic : calcID -> tac -> unit
neuper@37906:     val setProblem : calcID -> pblID -> unit
neuper@37906:     val setTheory : calcID -> thyID -> unit
neuper@37906:   end
neuper@37906: 
neuper@37906: 
neuper@37906: (*------------------------------------------------------------------*)
neuper@37906: structure interface : INTERFACE =
neuper@37906: struct
neuper@37906: (*------------------------------------------------------------------*)
neuper@37906: 
neuper@37906: (*.encode "Isabelle"-strings as seen by the user to the
neuper@37906:    format accepted by Isabelle.
neuper@37947:    encode "^" ---> "^^^"; see Knowledge/Atools.thy;
neuper@37906:    called for each cterm', icalhd, fmz in this interface;
neuper@37906:    + see "fun decode" in xmlsrc/mathml.sml.*)
neuper@37906: fun encode (str:cterm') = 
neuper@37906:     let fun enc [] = []
neuper@37906: 	  | enc ("^"::cs) = "^"::"^"::"^"::(enc cs)
neuper@37906: 	  | enc (c::cs) = c::(enc cs)
neuper@37906:     in (implode o enc o explode) str:cterm' end;
neuper@37906: fun encode_imodel (imodel:imodel) =
neuper@37906:     let fun enc (Given ifos) = Given (map encode ifos)
neuper@37906: 	  | enc (Find ifos) = Find (map encode ifos)
neuper@37906: 	  | enc (Relate ifos) = Relate (map encode ifos)
neuper@37906:     in map enc imodel:imodel end;
neuper@37906: fun encode_icalhd ((pos', headl, imodel, pos_, spec):icalhd) =
neuper@37906:     (pos', encode headl, encode_imodel imodel, pos_, spec):icalhd;
neuper@37906: fun encode_fmz ((ifos, spec):fmz) = (map encode ifos, spec):fmz;
neuper@37906: 
neuper@37906: 
neuper@37906: (***. CalcTree .***)
neuper@37906: 
neuper@37906: (** add and delete users **)
neuper@37906: 
neuper@37906: (*.'Iterator 1' must exist with each CalcTree;
neuper@37906:    the only for updating the calc-tree
neuper@37906:    WN.0411: only 'Iterator 1' is stored,
neuper@37906:    all others are just calculated on the fly
neuper@37906:    TODO: adapt Iterator, add_user(= add_iterator!),etc. accordingly .*)
neuper@37906: fun Iterator (cI:calcID) = (*returned ID unnecessary after WN.0411*)
neuper@37906:     (adduserOK2xml cI (add_user (cI:calcID)))
neuper@37906:     handle _ => sysERROR2xml cI "error in kernel";
neuper@37906: fun IteratorTEST (cI:calcID) = add_user (cI:calcID);
neuper@37906: (*fun DEconstructIterator (cI:calcID) (uI:iterID) =
neuper@37906:     deluserOK2xml (del_user cI uI);*)
neuper@37906: 
neuper@37906: (*.create a calc-tree; for calls from java: thus ^^^ decoded to ^;
neuper@37906:    compare "fun CalcTreeTEST" which does NOT decode.*)
neuper@37906: fun CalcTree
neuper@37906: 	[(fmz, sp):fmz] (*for several variants lateron*) =
neuper@37906: (* val[(fmz,sp):fmz]=[(["fixedValues [r=Arbfix]","maximum A","valuesFor [a,b]",
neuper@37906:              "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
neuper@37906:              "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
neuper@37906:              "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
neuper@37906:              "boundVariable a","boundVariable b","boundVariable alpha",
neuper@37906:              "interval {x::real. 0 <= x & x <= 2*r}",
neuper@37906:              "interval {x::real. 0 <= x & x <= 2*r}",
neuper@37906:              "interval {x::real. 0 <= x & x <= pi}",
neuper@37906:              "errorBound (eps=(0::real))"],
neuper@37906:        ("DiffApp.thy", ["maximum_of","function"],
neuper@37906:             ["DiffApp","max_by_calculus"]))];
neuper@37906: 
neuper@37906:    *)
neuper@37906: 	(let val cs = nxt_specify_init_calc (encode_fmz (fmz, sp))
neuper@37906: 	     (*FIXME.WN.8.03: error-handling missing*)
neuper@37906: 	     val cI = add_calc cs
neuper@37906: 	 in calctreeOK2xml cI end)
neuper@37906: 	handle _ => sysERROR2xml 0 "error in kernel";
neuper@37906: 
neuper@37906: fun DEconstrCalcTree (cI:calcID) =
neuper@37906:     deconstructcalctreeOK2xml (del_calc cI);
neuper@37906: 
neuper@37906: 
neuper@37906: fun getActiveFormula (cI:calcID) = iteratorOK2xml cI (get_pos cI 1);
neuper@37906: 
neuper@37906: fun moveActiveFormula (cI:calcID) (p:pos') =
neuper@37906:     let val ((pt,_),_) = get_calc cI
neuper@37906:     in if existpt' p pt then (upd_ipos cI 1 p; iteratorOK2xml cI p)
neuper@37906:        else sysERROR2xml cI "frontend sends a non-existing pos" end;
neuper@37906: 
neuper@37906: (*. set the next tactic to be applied: dont't change the calc-tree,
neuper@37906:     but remember the envisaged changes for fun autoCalculate;
neuper@37906:     compare force NextTactic .*)
neuper@37906: (* val (cI, tac) = (1, Add_Given "equality (x ^^^ 2 + 4 * x + 3 = 0)");
neuper@37906:    val (cI, tac) = (1, Specify_Theory "PolyEq.thy");
neuper@37906:    val (cI, tac) = (1, Specify_Problem ["normalize","polynomial",
neuper@37906: 				   "univariate","equation"]);
neuper@37906:    val (cI, tac) = (1, Subproblem ("Poly.thy",
neuper@37906: 			      ["polynomial","univariate","equation"]));
neuper@37906:    val (cI, tac) = (1, Model_Problem["linear","univariate","equation","test"]);
neuper@37906:    val (cI, tac) = (1, Detail_Set "Test_simplify");
neuper@37906:    val (cI, tac) = (1, Apply_Method ["Test", "solve_linear"]);
neuper@37906:    val (cI, tac) = (1, Rewrite_Set "Test_simplify");
neuper@37906:     *)
neuper@37906: fun setNextTactic (cI:calcID) tac =
neuper@37906:     let val ((pt, _), _) = get_calc cI
neuper@37906: 	val ip = get_pos cI 1
neuper@37906:     in case locatetac tac (pt, ip) of
neuper@37906: (* val ("ok", (tacis, c, (_,p'))) = locatetac tac (pt, ip);
neuper@37906:    *)
neuper@37906: 	   ("ok", (tacis, _, _)) =>
neuper@37906: 	   (upd_calc cI ((pt, ip), tacis); setnexttactic2xml cI "ok")
neuper@37906: 	 | ("unsafe-ok", (tacis, _, _)) =>
neuper@37906: 	   (upd_calc cI ((pt, ip), tacis); setnexttactic2xml cI "unsafe-ok")
neuper@37906: 	 | ("not-applicable",_) => setnexttactic2xml cI "not-applicable"
neuper@37906: 	 | ("end-of-calculation",_) =>
neuper@37906: 	   setnexttactic2xml cI "end-of-calculation"
neuper@37906: 	 | ("failure",_) => sysERROR2xml cI "failure"
neuper@37906:     end;
neuper@37906: 
neuper@37906: (*. apply a tactic at a position and update the calc-tree if applicable .*)
neuper@37947: (*WN080226 java-code is missing, errors smltest/Knowledge/polyminus.sml*)
neuper@37906: (* val (cI, ip, tac) = (1, p, hd appltacs);
neuper@37906:    val (cI, ip, tac) = (1, p, (hd (sel_appl_atomic_tacs pt p)));
neuper@37906:    *)
neuper@37906: fun applyTactic (cI:calcID) ip tac =
neuper@37906:     let val ((pt, _), _) = get_calc cI
neuper@37906: 	val p = get_pos cI 1
neuper@37906:     in case locatetac tac (pt, ip) of
neuper@37906: (* val ("ok", (tacis, c, (pt',p'))) = locatetac tac (pt, ip);
neuper@37906:    *)
neuper@37906: 	   ("ok", (_, c, ptp as (_,p'))) =>
neuper@37906: 	     (upd_calc cI (ptp, []); upd_ipos cI 1 p';
neuper@37906: 	      autocalculateOK2xml cI p (if null c then p'
neuper@37906: 					   else last_elem c) p')
neuper@37906: 	 | ("unsafe-ok", (_, c, ptp as (_,p'))) =>
neuper@37906: 	     (upd_calc cI (ptp, []); upd_ipos cI 1 p';
neuper@37906: 	      autocalculateOK2xml cI p (if null c then p'
neuper@37906: 					   else last_elem c) p')
neuper@37906: 	 | ("end-of-calculation", (_, c, ptp as (_,p'))) =>
neuper@37906: 	     (upd_calc cI (ptp, []); upd_ipos cI 1 p';
neuper@37906: 	      autocalculateOK2xml cI p (if null c then p'
neuper@37906: 					   else last_elem c) p')
neuper@37906: 
neuper@37906: 
neuper@37906: 	 | (str,_) => autocalculateERROR2xml cI "failure"
neuper@37906:     end;
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: (* val cI = 1;
neuper@37906:    *)
neuper@37906: fun fetchProposedTactic (cI:calcID) =
neuper@37906:     (case step (get_pos cI 1) (get_calc cI) of
neuper@37906: 	   ("ok", (tacis, _, _)) =>
neuper@37906: 	   let val _= upd_tacis cI tacis
neuper@37906: 	       val (tac,_,_) = last_elem tacis
neuper@37906: 	   in fetchproposedtacticOK2xml cI tac end
neuper@37906: 	 | ("helpless",_) => fetchproposedtacticERROR2xml cI "helpless"
neuper@37906: 	 | ("no-fmz-spec",_) => fetchproposedtacticERROR2xml cI "no-fmz-spec"
neuper@37906: 	 | ("end-of-calculation",_) =>
neuper@37906: 	   fetchproposedtacticERROR2xml cI "end-of-calculation")
neuper@37906:     handle _ => sysERROR2xml cI "error in kernel";
neuper@37906: 
neuper@37906: (*datatype auto = FIXXXME040624: does NOT match interfaces/ITOCalc.java
neuper@37906:   Step of int      (*1 do #int steps (may stop in model/specify)
neuper@37906: 		     IS VERY INEFFICIENT IN MODEL/SPECIY*)
neuper@37906: | CompleteModel    (*2 complete modeling
neuper@37906:                      if model complete, finish specifying*)
neuper@37906: | CompleteCalcHead (*3 complete model/specify in one go*)
neuper@37906: | CompleteToSubpbl (*4 stop at the next begin of a subproblem,
neuper@37906:                      if none, complete the actual (sub)problem*)
neuper@37906: | CompleteSubpbl   (*5 complete the actual (sub)problem (incl.ev.subproblems)*)
neuper@37906: | CompleteCalc;    (*6 complete the calculation as a whole*)*)
neuper@37906: fun autoCalculate (cI:calcID) auto =
neuper@37906: (* val (cI, auto) = (1,CompleteCalc);
neuper@37906:    val (cI, auto) = (1,CompleteModel);
neuper@37906:    val (cI, auto) = (1,CompleteCalcHead);
neuper@37906:    val (cI, auto) = (1,Step 1);
neuper@37906:    *)
neuper@37906:     (let val pold = get_pos cI 1
neuper@37906: 	 val x = autocalc [] pold (get_calc cI) auto
neuper@37906:      in
neuper@37906: 	 case x of
neuper@37906: (* val (str, c, ptp as (_,p)) = x;
neuper@37906:  *)
neuper@37906: 	     ("ok", c, ptp as (_,p)) =>
neuper@37906: 	     (upd_calc cI (ptp, []); upd_ipos cI 1 p;
neuper@37906: 	      autocalculateOK2xml cI pold (if null c then pold
neuper@37906: 					   else last_elem c) p)
neuper@37906: 	   | ("end-of-calculation", c, ptp as (_,p)) =>
neuper@37906: 	     (upd_calc cI (ptp, []); upd_ipos cI 1 p;
neuper@37906: 	      autocalculateOK2xml cI pold (if null c then pold
neuper@37906: 					   else last_elem c) p)
neuper@37906: 	   | (str, _, _) => autocalculateERROR2xml cI str
neuper@37906:      end)
neuper@37906:     handle _ => sysERROR2xml cI "error in kernel";
neuper@37906:     
neuper@37906: 
neuper@37906: (* val (cI:calcID, ichd as ((p,_),_,_,_,_):icalhd) =
neuper@37906:        (1, (([],Pbl), "not used here",
neuper@37906: 	[Given ["fixedValues [r=Arbfix]"],
neuper@37906: 	 Find ["maximum A", "valuesFor [a,b]"(*new input*)],
neuper@37906: 	 Relate ["relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]"]], Pbl,
neuper@37906:        ("DiffApp.thy", ["maximum_of","function"],
neuper@37906: 		   ["DiffApp","max_by_calculus"])));
neuper@37906:  val (cI:calcID, ichd as ((p,_),_,_,_,_):icalhd) =
neuper@37906:        (1, (([],Pbl),"solve (x+1=2, x)",
neuper@37906: 		  [Given ["equality (x+1=2)", "solveFor x"],
neuper@37906: 		   Find ["solutions L"]],
neuper@37906: 		  Pbl,
neuper@37906: 		  ("Test.thy", ["linear","univariate","equation","test"],
neuper@37906: 		   ["Test","solve_linear"])));
neuper@37906:  val (cI:calcID, ichd as ((p,_),_,_,_,_):icalhd) =
neuper@37906:        (1, (([],Pbl),"solveTest (1+-1*2+x=0,x)", [], Pbl, ("", [], [])));
neuper@37906:  val (cI, p:pos')=(1, ([1],Frm));
neuper@37906:  val (cI, p:pos')=(1, ([1,2,1,3],Res)); 
neuper@37906:    *)
neuper@37906: fun getTactic cI (p:pos') =
neuper@37906:     (let val ((pt,_),_) = get_calc cI
neuper@37906: 	 val (form, tac, asms) = pt_extract (pt, p)
neuper@37906:     in case tac of
neuper@37926: (* val SOME ta = tac;
neuper@37906:    *)
neuper@37926: 	   SOME ta => gettacticOK2xml cI ta
neuper@37926: 	 | NONE => gettacticERROR2xml cI ("no tactic at position "^pos'2str p)
neuper@37906:      end)
neuper@37906:     handle _ => sysERROR2xml cI "syserror in getTactic";
neuper@37906: 
neuper@37906: (*. see ICalcIterator#fetchApplicableTactics
neuper@37906:  @see #TACTICS_ALL
neuper@37906:  @see #TACTICS_CURRENT_THEORY
neuper@37906:  @see #TACTICS_CURRENT_METHOD  ..the only impl.WN040307.*)
neuper@37906: (*. fetch tactics to be applied to a particular step.*)
neuper@37906: (* WN071231 kept this version for later parametrisation*)
neuper@37906: (*.version 1: fetch _all_ tactics from script .*)
neuper@37906: fun fetchApplicableTactics cI (scope:int) (p:pos') =
neuper@37906:     (let val ((pt, _), _) = get_calc cI
neuper@37906:     in (applicabletacticsOK cI (sel_rules pt p))
neuper@37906:        handle PTREE str => sysERROR2xml cI str 
neuper@37906:      end)
neuper@37906:     handle _ => sysERROR2xml cI "error in kernel";
neuper@37906: (*.version 2: fetch _applicable_ _elementary_ (ie. recursively 
neuper@37906:               decompose rule-sets) Rewrite*, Calculate .*)
neuper@37906: fun fetchApplicableTactics cI (scope:int) (p:pos') =
neuper@37906:     (let val ((pt, _), _) = get_calc cI
neuper@37906:     in (applicabletacticsOK cI (sel_appl_atomic_tacs pt p))
neuper@37906:        handle PTREE str => sysERROR2xml cI str 
neuper@37906:      end)
neuper@37906:     handle _ => sysERROR2xml cI "error in kernel";
neuper@37906: 
neuper@37906: fun getAssumptions cI (p:pos') =
neuper@37906:     (let val ((pt,_),_) = get_calc cI
neuper@37906: 	 val (_, _, asms) = pt_extract (pt, p)
neuper@37906:      in getasmsOK2xml cI asms end)
neuper@37906:     handle _ => sysERROR2xml cI "syserror in getAssumptions";
neuper@37906: 
neuper@37906: (*WN0502 @see ME/ctree: type asms: illdesigned, thus no positions returned*)
neuper@37906: fun getAccumulatedAsms cI (p:pos') =
neuper@37906:     (let val ((pt, _), _) = get_calc cI
neuper@37906: 	 val ass = map fst (get_assumptions_ pt p)
neuper@37906:      in (*getaccuasmsOK2xml cI (get_assumptions_ pt p)*)
neuper@37906:      getasmsOK2xml cI ass end)
neuper@37906:     handle _ => sysERROR2xml cI "syserror in getAccumulatedAsms";
neuper@37906: 
neuper@37906: 
neuper@37906: (*since moveActive* does NOT transfer pos java --> sml (only sml --> java)
neuper@37906:   refFormula might become involved in far-off errors !!!*)
neuper@37906: fun refFormula cI (p:pos') = (*WN0501 rename to 'fun getElement' !*)
neuper@37906: (* val (cI, uI) = (1,1);
neuper@37906:    *)
neuper@37906:     (let val ((pt,_),_) = get_calc cI
neuper@37906: 	 val (form, tac, asms) = pt_extract (pt, p)
neuper@37906:     in refformulaOK2xml cI p form end)
neuper@37906:     handle _ => sysERROR2xml cI "error in kernel";
neuper@37906: 
neuper@37906: (*.get formulae 'from' 'to' w.r.t. ordering in Position#compareTo(Position p); 
neuper@37906:    in case of CalcHeads only the headline is taken
neuper@37906:    (the pos' allows distinction between PrfObj and PblObj anyway);
neuper@37906:    'level' is adjusted such that an 'interval' of formulae is returned;
neuper@37906:    'from' 'to' are designed for use by iterators of calcChangedEvent;
neuper@37906:    thus 'from' is the last unchanged position.*)
neuper@37906: fun getFormulaeFromTo cI (from as ([],Pbl):pos') (to as ([],Pbl):pos')_ false =
neuper@37906: (*special case because 'from' is _before_ the first elements to be returned*)
neuper@37906: (* val (cI, from, to, level) = (1, ([],Pbl), ([],Pbl), 1);
neuper@37906:    *)
neuper@37906:     ((let val ((pt,_),_) = get_calc cI
neuper@37906: 	val (ModSpec (_,_,headline,_,_,_),_,_) = pt_extract (pt, to)
neuper@37906:     in getintervalOK cI [(to, headline)] end)
neuper@37906:     handle _ => sysERROR2xml cI "error in kernel")
neuper@37906: 
neuper@37906:   | getFormulaeFromTo cI (from as ([],Pbl):pos') (to as ([],Met):pos')_ false =
neuper@37906:     getFormulaeFromTo cI ([],Pbl) ([],Pbl) (~00000) false
neuper@37906: 
neuper@37906:   | getFormulaeFromTo cI (from:pos') (to:pos') level false =
neuper@37906: (* val (cI, from, to, level) = (1, unc, gen, 0);
neuper@37906:    val (cI, from, to, level) = (1, unc, gen, 1);
neuper@37906:    val (cI, from, to, level) = (1, ([],Pbl), ([],Met), 1);
neuper@37906:    *)
neuper@37906:     (if from = to then sysERROR2xml cI "getFormulaeFromTo: From = To"
neuper@37906:      else
neuper@37906: 	 (case from of
neuper@37906: 	      ([],Res) => sysERROR2xml cI "getFormulaeFromTo does: moveDown \
neuper@37906: 					  \from=([],Res) .. goes beyond result"
neuper@37906: 	    | _ => let val ((pt,_),_) = get_calc cI
neuper@37906: 		       val f = move_dn [] pt from
neuper@37906: 		       fun max (a,b) = if a < b then b else a
neuper@37906: 		       (*must reach margins ...*)
neuper@37906: 		       val lev = max (level, max (lev_of from, lev_of to))
neuper@37906: 		   in getintervalOK cI (get_interval f to lev pt) end)
neuper@37906: 	 handle _ => sysERROR2xml cI "error in getFormulaeFromTo")
neuper@37906: 
neuper@37906:   | getFormulaeFromTo cI from to level true =
neuper@37906:     sysERROR2xml cI "getFormulaeFromTo impl.for formulae only,\
neuper@37906: 		    \i.e. last arg only impl. for false, _NOT_ true";
neuper@37906: 
neuper@37906: 
neuper@37906: (* val (cI, ip) = (1, ([1,9], Res));
neuper@37906:    val (cI, ip) = (1, ([], Res));
neuper@37906:    val (cI, ip) = (1, ([2], Res));
neuper@37906:    val (cI, ip) = (1, ([3,1], Res));
neuper@37906:    val (cI, ip) = (1, ([1,2,1], Res));
neuper@37906:    *)
neuper@37906: fun interSteps cI ip =
neuper@37906:     (let val ((pt,p), tacis) = get_calc cI
neuper@37906:      in if (not o is_interpos) ip
neuper@37906: 	then interStepsERROR cI "only formulae with position (_,Res) \
neuper@37906: 				\may have intermediate steps above them"
neuper@37906: 	else let val ip' = lev_pred' pt ip
neuper@37906: (* val (str, pt', lastpos) = detailstep pt ip;
neuper@37906:    *)
neuper@37906: 	     in case detailstep pt ip of
neuper@37906: 		    ("detailrls", pt(*, pos'forms*), lastpos) =>
neuper@37906: 		    (upd_calc cI ((pt, p), tacis);
neuper@37906: 		     interStepsOK cI (*pos'forms*) ip' ip' lastpos)
neuper@37906: 		  | ("no-Rewrite_Set...", _, _) =>
neuper@37906: 		    sysERROR2xml cI "no Rewrite_Set..."
neuper@37906: 		  | (_, _(*, pos'formshds*), lastpos) =>
neuper@37906: 		    interStepsOK cI (*pos'formshds*) ip' ip' lastpos
neuper@37906: 	     end
neuper@37906:      end)
neuper@37906:     handle _ => sysERROR2xml cI "error in kernel";
neuper@37906: 
neuper@37906: fun modifyCalcHead (cI:calcID) (ichd as ((p,_),_,_,_,_):icalhd) =
neuper@37906:     (let val ((pt,_),_) = get_calc cI
neuper@37906: 	val (pt, chd as (_,p_,_,_,_,_)) = input_icalhd pt ichd
neuper@37906:     in (upd_calc cI ((pt, (p,p_)), []); 
neuper@37906: 	modifycalcheadOK2xml cI chd) end)
neuper@37906:     handle _ => sysERROR2xml cI "error in kernel";
neuper@37906: 
neuper@37906: (*.at the activeFormula set the Model, the Guard and the Specification 
neuper@37906:    to empty and return a CalcHead;
neuper@37906:    the 'origin' remains (for reconstructing all that).*)
neuper@37906: fun resetCalcHead (cI:calcID) = 
neuper@37906:     (let val (ptp,_) = get_calc cI
neuper@37906: 	val ptp = reset_calchead ptp
neuper@37906:     in (upd_calc cI (ptp, []); 
neuper@37906: 	modifycalcheadOK2xml cI (get_ocalhd ptp)) end)
neuper@37906:     handle _ => sysERROR2xml cI "error in kernel";
neuper@37906: 
neuper@37906: (*.at the activeFormula insert all the Descriptions in the Model 
neuper@37906:    (_not_ in the Guard) and return a CalcHead;
neuper@37906:    the Descriptions are for user-guidance; the rest of the items 
neuper@37906:    are left empty for user-input; 
neuper@37906:    includes a resetCalcHead for the Model and the Guard.*)
neuper@37906: fun modelProblem (cI:calcID) = 
neuper@37906:     (let val (ptp, _) = get_calc cI
neuper@37906: 	val ptp = reset_calchead ptp
neuper@37906: 	val (_, _, ptp) = nxt_specif Model_Problem ptp
neuper@37906:     in (upd_calc cI (ptp, []); 
neuper@37906: 	modifycalcheadOK2xml cI (get_ocalhd ptp)) end)
neuper@37906:     handle _ => sysERROR2xml cI "error in kernel";
neuper@37906: 
neuper@37906: 
neuper@37906: (*.set the context determined on a knowledgebrowser to the current calc.*)
neuper@37906: fun setContext (cI:calcID) (ip as (_,p_):pos') (guh:guh) =
neuper@37906:     (case (implode o (take_fromto 1 4) o explode) guh of
neuper@37906: 	 "thy_" =>
neuper@37906: (* val (cI, ip as (_,p_), guh) = (1, p, "thy_isac_Test-rls-Test_simplify");
neuper@37906:    *)
neuper@37935: 	 if member op = [Pbl,Met] p_
neuper@37930:          then message2xml cI "thy-context not to calchead"
neuper@37906: 	 else if ip = ([],Res) then message2xml cI "no thy-context at result"
neuper@37906: 	 else if no_thycontext guh then message2xml cI ("no thy-context for '"^
neuper@37906: 							guh ^ "'")
neuper@37906: 	 else let val (ptp as (pt,pold),_) = get_calc cI
neuper@37906: 		  val is = get_istate pt ip
neuper@37906: 		  val subs = subs_from is "dummy" guh
neuper@37906: 		  val tac = guh2rewtac guh subs
neuper@37906: 	      in case locatetac tac (pt, ip) of (*='fun setNextTactic'+step*)
neuper@37906: 		     ("ok", (tacis, c, ptp as (_,p))) =>
neuper@37906: (* val (str, (tacis, c, ptp as (_,p))) = locatetac tac (pt, ip);
neuper@37906:    *)
neuper@37906: 		     (upd_calc cI ((pt,p), []); 
neuper@37906: 		      autocalculateOK2xml cI pold (if null c then pold
neuper@37906: 					   else last_elem c) p)
neuper@37906: 		   | ("unsafe-ok", (tacis, c, ptp as (_,p))) =>
neuper@37906: 		     (upd_calc cI ((pt,p), []); 
neuper@37906: 		      autocalculateOK2xml cI pold (if null c then pold
neuper@37906: 						   else last_elem c) p)
neuper@37906: 		   | ("end-of-calculation",_) =>
neuper@37906: 		     message2xml cI "end-of-calculation"
neuper@37906: 		   | ("failure",_) => sysERROR2xml cI "failure"
neuper@37906: 		   | ("not-applicable",_) => (*the rule comes from anywhere..*)
neuper@37906: 		     (case applicable_in ip pt tac of 
neuper@37906: 			  
neuper@37906: 			  Notappl e => message2xml cI ("'" ^ tac2str tac ^ 
neuper@37906: 						       "' not-applicable")
neuper@37906: 			| Appl m => 
neuper@37906: 			  let val (p,c,_,pt) = generate1 (assoc_thy"Isac.thy") 
neuper@37906: 							 m Uistate ip pt
neuper@37906: 			  in upd_calc cI ((pt,p),[]);
neuper@37906: 			  autocalculateOK2xml cI pold (if null c then pold
neuper@37906: 						       else last_elem c) p
neuper@37906: 			  end)
neuper@37906: 	      end
neuper@37906: (* val (cI, ip as (_,p_), guh) = (1, pos, guh);
neuper@37906:    *)
neuper@37906:        | "pbl_" =>
neuper@37906: 	 let val pI = guh2kestoreID guh
neuper@37906: 	     val ((pt, _), _) = get_calc cI
neuper@37906: 	     (*val ip as (_, p_) = get_pos cI 1*)
neuper@37942: 	 in if member op = [Pbl, Met] p_ 
neuper@37906: 	    then let val (pt, chd) = set_problem pI (pt, ip)
neuper@37906: 		 in (upd_calc cI ((pt, ip), []);
neuper@37906: 		     modifycalcheadOK2xml cI chd) end
neuper@37906: 	    else sysERROR2xml cI "setContext for pbl requires ActiveFormula \
neuper@37906: 				 \on CalcHead"
neuper@37906: 	 end
neuper@37906: (* val (cI, ip as (_,p_), guh) = (1, pos, "met_eq_lin");
neuper@37906:    *)
neuper@37906:        | "met_" =>
neuper@37906: 	 let val mI = guh2kestoreID guh
neuper@37906: 	     val ((pt, _), _) = get_calc cI
neuper@37942: 	 in if member op = [Pbl, Met] p_
neuper@37906: 	    then let val (pt, chd) = set_method mI (pt, ip)
neuper@37906: 		 in (upd_calc cI ((pt, ip), []);
neuper@37906: 		     modifycalcheadOK2xml cI chd) end
neuper@37906: 	    else sysERROR2xml cI "setContext for met requires ActiveFormula \
neuper@37906: 				 \on CalcHead"
neuper@37906: 	 end)
neuper@37906:     handle _ => sysERROR2xml cI "error in kernel";
neuper@37906: 
neuper@37906: 
neuper@37906: (*.specify the Method at the activeFormula and return a CalcHead
neuper@37906:    containing the Guard.
neuper@37906:    WN0512 impl.incomplete, see 'nxt_specif (Specify_Method '.*)
neuper@37906: fun setMethod (cI:calcID) (mI:metID) = 
neuper@37906: (* val (cI, mI) = (1, ["Test","solve_linear"]);
neuper@37906:    *)
neuper@37906:     (let val ((pt, _), _) = get_calc cI
neuper@37906: 	val ip as (_, p_) = get_pos cI 1
neuper@37935:     in if member op = [Pbl,Met] p_ 
neuper@37906:        then let val (pt, chd) = set_method mI (pt, ip)
neuper@37906: 	    in (upd_calc cI ((pt, ip), []);
neuper@37906: 		modifycalcheadOK2xml cI chd) end
neuper@37906:        else sysERROR2xml cI "setMethod requires ActiveFormula on CalcHead"
neuper@37906:  end)
neuper@37906:     handle _ => sysERROR2xml cI "error in kernel";
neuper@37906: 
neuper@37906: (*.specify the Problem at the activeFormula and return a CalcHead
neuper@37906:    containing the Model; special case of checkContext;
neuper@37906:    WN0512 impl.incomplete, see 'nxt_specif (Specify_Problem '.*)
neuper@37906: fun setProblem (cI:calcID) (pI:pblID) =
neuper@37906:     (let val ((pt, _), _) = get_calc cI
neuper@37906: 	val ip as (_, p_) = get_pos cI 1
neuper@37935:     in if member op = [Pbl,Met] p_
neuper@37906:        then let val (pt, chd) = set_problem pI (pt, ip)
neuper@37906: 	    in (upd_calc cI ((pt, ip), []);
neuper@37906: 		modifycalcheadOK2xml cI chd) end
neuper@37906:        else sysERROR2xml cI "setProblem requires ActiveFormula on CalcHead"
neuper@37906:  end)
neuper@37906:     handle _ => sysERROR2xml cI "error in kernel";
neuper@37906: 
neuper@37906: (*.specify the Theory at the activeFormula and return a CalcHead;
neuper@37906:    special case of checkContext;
neuper@37906:    WN0512 impl.incomplete, see 'nxt_specif (Specify_Method '.*)
neuper@37906: fun setTheory (cI:calcID) (tI:thyID) =
neuper@37906:     (let val ((pt, _), _) = get_calc cI
neuper@37906: 	val ip as (_, p_) = get_pos cI 1
neuper@37935:     in if member op = [Pbl,Met] p_
neuper@37906:        then let val (pt, chd) = set_theory tI (pt, ip)
neuper@37906: 	    in (upd_calc cI ((pt, ip), []);
neuper@37906: 		modifycalcheadOK2xml cI chd) end
neuper@37906:        else sysERROR2xml cI "setProblem requires ActiveFormula on CalcHead"
neuper@37906:  end)
neuper@37906:     handle _ => sysERROR2xml cI "error in kernel";
neuper@37906: 
neuper@37906: 
neuper@37906: (**. without update of CalcTree .**)
neuper@37906: 
neuper@37906: (*.match the model of a problem at pos p 
neuper@37906:    with the model-pattern of the problem with pblID*)
neuper@37906: (*fun tryMatchProblem cI pblID =
neuper@37906:     (let val ((pt,_),_) = get_calc cI
neuper@37906: 	 val p = get_pos cI 1
neuper@37906: 	 val chd = trymatch pblID pt p
neuper@37906:     in trymatchOK2xml cI chd end)
neuper@37906:     handle _ => sysERROR2xml cI "error in kernel";*)
neuper@37906: 
neuper@37906: (*.refinement for the parent-problem of the position.*)
neuper@37906: (* val (cI, (p,p_), guh) = (1, ([1],Res), "pbl_equ_univ");
neuper@37906:    *)
neuper@37906: fun refineProblem cI ((p,p_) : pos') (guh : guh) =
neuper@37906:     (let val pblID = guh2kestoreID guh
neuper@37906: 	 val ((pt,_),_) = get_calc cI
neuper@37906: 	 val pp = par_pblobj pt p
neuper@37906: 	 val chd = tryrefine pblID pt (pp, p_)
neuper@37906:     in matchpbl2xml cI chd end)
neuper@37906:     handle _ => sysERROR2xml cI "error in kernel";
neuper@37906: 
neuper@37906: (* val (cI, ifo) = (1, "-2 * 1 + (1 + x) = 0");
neuper@37906:    val (cI, ifo) = (1, "x = 2");
neuper@37906:    val (cI, ifo) = (1, "[x = 3 + -2*1]");
neuper@37906:    val (cI, ifo) = (1, "-1 + x = 0");
neuper@37906:    val (cI, ifo) = (1, "x - 4711 = 0");
neuper@37906:    val (cI, ifo) = (1, "2+ -1 + x = 2");
neuper@37906:    val (cI, ifo) = (1, " x - ");
neuper@37906:    val (cI, ifo) = (1, "(-3 * x + 4 * y + -1 * x * y) / (x * y)");
neuper@37906:    val (cI, ifo) = (1, "(4 * y + -3 * x) / (x * y) + -1");
neuper@37906:    *)
neuper@37906: fun appendFormula cI (ifo:cterm') =
neuper@37906:     (let val cs = get_calc cI
neuper@37906: 	 val pos as (_,p_) = get_pos cI 1
neuper@37906:      in case step pos cs of
neuper@37906: (* val (str, cs') = step pos cs;
neuper@37906:    *)
neuper@37906: 	    ("ok", cs') =>
neuper@37906: 	    (case inform cs' (encode ifo) of
neuper@37906: (* val (str, (_, c, ptp as (_,p))) = inform cs' (encode ifo);
neuper@37906:    *)
neuper@37906: 		 ("ok", (_(*use in DG !!!*), c, ptp as (_,p))) =>
neuper@37906: 		 (upd_calc cI (ptp, []); upd_ipos cI 1 p;
neuper@37906: 		  appendformulaOK2xml cI pos (if null c then pos
neuper@37906: 					      else last_elem c) p)
neuper@37906: 	       | ("same-formula", (_, c, ptp as (_,p))) =>
neuper@37906: 		 (upd_calc cI (ptp, []); upd_ipos cI 1 p;
neuper@37906: 		  appendformulaOK2xml cI pos (if null c then pos
neuper@37906: 					      else last_elem c) p)
neuper@37906: 	       | (msg, _) => appendformulaERROR2xml cI msg)
neuper@37906: 	  | (msg, cs') => appendformulaERROR2xml cI msg
neuper@37906:      end)
neuper@37906:     handle _ => sysERROR2xml cI "error in kernel";
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: (*.replace a formula with_in_ a calculation;
neuper@37906:    this situation applies for initial CAS-commands, too.*)
neuper@37906: (* val (cI, ifo) = (2, "-1 + x = 0");
neuper@37906:    val (cI, ifo) = (1, "-1 + x = 0");
neuper@37906:    val (cI, ifo) = (1, "x - 1 = 0");
neuper@37906:    val (cI, ifo) = (1, "x = 1");
neuper@37906:    val (cI, ifo) = (1, "solve(x+1=2,x)");
neuper@37906:    val (cI, ifo) = (1, "Simplify (2*a + 3*a)");
neuper@37906:    val (cI, ifo) = (1, "Diff (x^2 + x + 1, x)");
neuper@37906:    *)
neuper@37906: fun replaceFormula cI (ifo:cterm') =
neuper@37906:     (let val ((pt, _), _) = get_calc cI
neuper@37906: 	val p = get_pos cI 1
neuper@37906:     in case inform (([], [], (pt, p)): calcstate') (encode ifo) of
neuper@37906: 	   ("ok", (_(*tacs used for DG ?*), c, ptp' as (pt',p'))) =>
neuper@37906: (* val (str, (_,c, ptp' as (pt',p')))= inform ([], [], (pt, p)) (encode ifo);
neuper@37906:    *)
neuper@37906: 	   let val unc = if null (fst p) then p else move_up [] pt p
neuper@37906: 	       val _ = upd_calc cI (ptp', [])
neuper@37906: 	       val _ = upd_ipos cI 1 p'
neuper@37906: 	   in replaceformulaOK2xml cI unc
neuper@37906: 				   (if null c then unc
neuper@37906: 				    else last_elem c) p'(*' NEW*) end
neuper@37906: 	 | ("same-formula", _) =>
neuper@37906: 	   (*TODO.WN0501 MESSAGE !*)
neuper@37906: 	   replaceformulaERROR2xml cI "formula not changed"
neuper@37906: 	 | (msg, _) => replaceformulaERROR2xml cI msg
neuper@37906:     end)
neuper@37906:     handle _ => sysERROR2xml cI "error in kernel";
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: (***. CalcIterator
neuper@37906:     moveActive*: set the pos' of the active formula stored with the calctree
neuper@37906:                  could take pos' as argument for consistency checks
neuper@37906:     move*:       compute the new iterator from the old one on the fly
neuper@37906: 
neuper@37906: .***)
neuper@37906: 
neuper@37906: fun moveActiveRoot cI =
neuper@37906:     (let val _ = upd_ipos cI 1 ([],Pbl)
neuper@37906:     in iteratorOK2xml cI ([],Pbl) end)
neuper@37906:     handle e => sysERROR2xml cI "error in kernel";
neuper@37906: fun moveRoot cI =
neuper@37906:     (iteratorOK2xml cI ([],Pbl))
neuper@37906:     handle e => sysERROR2xml cI "";
neuper@37906: fun moveActiveRootTEST cI =
neuper@37906:     (let val _ = upd_ipos cI 1 ([],Pbl)
neuper@37906:     in (*iteratorOK2xml cI ([],Pbl)*)() end)
neuper@37906:     handle e => sysERROR2xml cI "error in kernel";
neuper@37906: 
neuper@37906: (* val (cI, uI) = (1,1);
neuper@37906:    val (cI, uI) = (1,2);
neuper@37906:    *)
neuper@37906: fun moveActiveDown cI =
neuper@37906:     ((let val ((pt,_),_) = get_calc cI
neuper@37906: (* val (P, (Nd (_, ns)), (p::(ps as (_::_)), p_)) =([]:pos, pt, get_pos cI uI);
neuper@37906:    val (P, (Nd (c, ns)), ([p], p_))               =([]:pos, pt, get_pos cI uI);
neuper@37906: 
neuper@37906:    print_depth 7;pt
neuper@37906:    *)
neuper@37906: 	  val ip' = move_dn [] pt (get_pos cI 1)
neuper@37906: 	  val _ = upd_ipos cI 1 ip'
neuper@37906:       in iteratorOK2xml cI ip' end)
neuper@37906:      handle (PTREE e) => iteratorERROR2xml cI)
neuper@37906:     handle _ => sysERROR2xml cI "error in kernel";
neuper@37906: fun moveDown cI (p:pos') =
neuper@37906:     ((let val ((pt,_),_) = get_calc cI
neuper@37906: (* val (P, (Nd (_, ns)), (p::(ps as (_::_)), p_)) =([]:pos, pt, get_pos cI uI);
neuper@37906:    val (P, (Nd (c, ns)), ([p], p_))               =([]:pos, pt, get_pos cI uI);
neuper@37906: 
neuper@37906:    print_depth 7;pt
neuper@37906:    *)
neuper@37906: 	  val ip' = move_dn [] pt p
neuper@37906:       in iteratorOK2xml cI ip' end)
neuper@37906:      handle (PTREE e) => iteratorERROR2xml cI)
neuper@37906:     handle _ => sysERROR2xml cI "error in kernel";
neuper@37906: fun moveActiveDownTEST cI =
neuper@37906:     let val ((pt,_),_) = get_calc cI
neuper@37906: 	val ip = get_pos cI 1
neuper@37906: 	  val ip' = (move_dn [] pt ip)
neuper@37906: 	      handle _ => ip
neuper@37906: 	  val _ = upd_ipos cI 1 ip'
neuper@37906:       in (*iteratorOK2xml cI uI*)() end;
neuper@37906: 
neuper@37906: fun moveActiveLevelDown cI =
neuper@37906:     ((let val ((pt,_),_) = get_calc cI
neuper@37906: 	  val ip' = movelevel_dn [] pt (get_pos cI 1)
neuper@37906: 	  val _ = upd_ipos cI 1 ip'
neuper@37906:       in iteratorOK2xml cI ip' end)
neuper@37906:      handle (PTREE e) => iteratorERROR2xml cI)
neuper@37906:     handle _ => sysERROR2xml cI "error in kernel";
neuper@37906: fun moveLevelDown cI (p:pos') =
neuper@37906:     ((let val ((pt,_),_) = get_calc cI
neuper@37906: 	  val ip' = movelevel_dn [] pt p
neuper@37906:       in iteratorOK2xml cI ip' end)
neuper@37906:      handle (PTREE e) => iteratorERROR2xml cI)
neuper@37906:     handle _ => sysERROR2xml cI "error in kernel";
neuper@37906: 
neuper@37906: fun moveActiveUp cI =
neuper@37906:     ((let val ((pt,_),_) = get_calc cI
neuper@37906: 	  val ip' = move_up [] pt (get_pos cI 1)
neuper@37906: 	  val _ = upd_ipos cI 1 ip'
neuper@37906:       in iteratorOK2xml cI ip' end)
neuper@37906:      handle PTREE e => iteratorERROR2xml cI)
neuper@37906:     handle _ => sysERROR2xml cI "error in kernel";
neuper@37906: fun moveUp cI (p:pos') =
neuper@37906:     ((let val ((pt,_),_) = get_calc cI
neuper@37906: 	  val ip' = move_up [] pt p
neuper@37906:       in iteratorOK2xml cI ip' end)
neuper@37906:      handle PTREE e => iteratorERROR2xml cI)
neuper@37906:     handle _ => sysERROR2xml cI "error in kernel";
neuper@37906: 
neuper@37906: fun moveActiveLevelUp cI =
neuper@37906:     ((let val ((pt,_),_) = get_calc cI
neuper@37906: 	  val ip' = movelevel_up [] pt (get_pos cI 1)
neuper@37906: 	  val _ = upd_ipos cI 1 ip'
neuper@37906:       in iteratorOK2xml cI ip' end)
neuper@37906:      handle PTREE e => iteratorERROR2xml cI)
neuper@37906:     handle _ => sysERROR2xml cI "error in kernel";
neuper@37906: fun moveLevelUp cI (p:pos') =
neuper@37906:     ((let val ((pt,_),_) = get_calc cI
neuper@37906: 	  val ip' = movelevel_up [] pt p
neuper@37906:       in iteratorOK2xml cI ip' end)
neuper@37906:      handle PTREE e => iteratorERROR2xml cI)
neuper@37906:     handle _ => sysERROR2xml cI "error in kernel";
neuper@37906: 
neuper@37906: fun moveActiveCalcHead cI =
neuper@37906:     ((let val ((pt,_),_) = get_calc cI
neuper@37906: 	  val ip' = movecalchd_up pt (get_pos cI 1)
neuper@37906: 	  val _ = upd_ipos cI 1 ip'
neuper@37906:       in iteratorOK2xml cI ip' end)
neuper@37906:      handle PTREE e => iteratorERROR2xml cI)
neuper@37906:     handle _ => sysERROR2xml cI "error in kernel";
neuper@37906: fun moveCalcHead cI (p:pos') =
neuper@37906:     ((let val ((pt,_),_) = get_calc cI
neuper@37906: 	  val ip' = movecalchd_up pt p
neuper@37906:       in iteratorOK2xml cI ip' end)
neuper@37906:      handle PTREE e => iteratorERROR2xml cI)
neuper@37906:     handle _ => sysERROR2xml cI "error in kernel";
neuper@37906: 
neuper@37906: 
neuper@37906: (*.initContext Thy_ is conceptually impossible at [Pbl,Met] 
neuper@37906:    and at positions with Check_Postcond and End_Trans;
neuper@37906:    at possible pos's there can be NO rewrite (returned as a context, too).*)
neuper@37906: (* val (cI, Thy_, (pos as (p,p_):pos')) = (1, Thy_, ([1], Frm));
neuper@37906:    val (cI, Thy_, (pos as (p,p_):pos')) = (1, Thy_, ([], Res));
neuper@37906:    val (cI, Thy_, (pos as (p,p_):pos')) = (1, Thy_, ([2], Res));
neuper@37906:    val (cI, Thy_, (pos as (p,p_):pos')) = (1, Thy_, ([1,1], Frm));
neuper@37906:    *)
neuper@37906: fun initContext (cI:calcID) Thy_ (pos as (p,p_):pos') =
neuper@37935:     ((if member op = [Pbl,Met] p_
neuper@37930:       then message2xml cI "thy-context not to calchead"
neuper@37906:       else if pos = ([],Res) then message2xml cI "no thy-context at result"
neuper@37906:       else let val cs as (ptp as (pt,_),_) = get_calc cI
neuper@37906: 	   in if exist_lev_on' pt pos
neuper@37906: 	      then let val pos' = lev_on' pt pos
neuper@37906: 		       val tac = get_tac_checked pt pos'
neuper@37906: 		   in if is_rewtac tac 
neuper@37906: 		      then contextthyOK2xml cI (context_thy (pt,pos) tac)
neuper@37906: 		      else message2xml cI ("no thy-context at tac '" ^
neuper@37906: 					   tac2str tac ^ "'")
neuper@37906: 		   end
neuper@37906: 	      else if is_curr_endof_calc pt pos
neuper@37906: 	      then case step pos cs of
neuper@37906: (* val (str, (tacis, _, (pt,_))) = step pos cs;
neuper@37906:    val ("ok", (tacis, _, (pt,_))) = step pos cs;
neuper@37906:    *)
neuper@37906: 		       ("ok", (tacis, _, (pt,_))) =>
neuper@37906: 		       let val tac = fst3 (last_elem tacis)
neuper@37906: 		       in if is_rewtac tac 
neuper@37906: 			  then contextthyOK2xml 
neuper@37906: 				   cI (context_thy ptp tac)
neuper@37906: 			  else message2xml cI ("no thy-context at tac '" ^
neuper@37906: 					       tac2str tac ^ "'")
neuper@37906: 		       end
neuper@37906: 		     | (msg, _) => message2xml cI msg
neuper@37906: 	      else message2xml cI "no thy-context at this position"
neuper@37906: 	   end)
neuper@37906:      handle _ => sysERROR2xml cI "error in kernel")
neuper@37906: 
neuper@37906: (* val (cI, Pbl_, pos as (p,p_)) = (1, Pbl_, ([],Pbl));
neuper@37906:    *)
neuper@37906:   | initContext cI Pbl_ (pos as (p,p_):pos') = 
neuper@37906:     ((let val ((pt,_),_) = get_calc cI
neuper@37906: 	  val pp = par_pblobj pt p
neuper@37906: 	  val chd = initcontext_pbl pt (pp,p_)
neuper@37906:       in matchpbl2xml cI chd end)
neuper@37906:      handle _ => sysERROR2xml cI "error in kernel")
neuper@37906: 
neuper@37906:   | initContext cI Met_ (pos as (p,p_):pos') =
neuper@37906:     ((let val ((pt,_),_) = get_calc cI
neuper@37906: 	  val pp = par_pblobj pt p
neuper@37906: 	  val chd = initcontext_met pt (pp,p_)
neuper@37906:       in matchmet2xml cI chd end)
neuper@37906:      handle _ => sysERROR2xml cI "error in kernel");
neuper@37906: 
neuper@37906: 
neuper@37906:     
neuper@37906: (*.match a theorem, a ruleset (etc., selected in the knowledge-browser)
neuper@37906: with the formula in the focus on the worksheet;
neuper@37906: string contains the thy, thus it is unique as thmID, rlsID for this thy;
neuper@37906: take the substitution from the istate of the formula.*)
neuper@37947: (* use"../smltest/Knowledge/poly.sml";
neuper@37906:    val (cI, pos as (p,p_), guh) = (1, ([1,1,1], Frm), 
neuper@37906: 				   "thy_Poly-thm-real_diff_minus");
neuper@37906:    val (cI, pos as (p,p_), guh) = (1, ([1,1], Frm), "norm_Poly");
neuper@37906:    val (cI, pos as (p,p_), guh) = 
neuper@37906:        (1, ([1], Res), "thy_isac_Test-rls-Test_simplify");
neuper@37906:    *)
neuper@37906: fun checkContext (cI:calcID) (pos:pos' as (p,p_)) (guh:guh) =
neuper@37906:     (case (implode o (take_fromto 1 4) o explode) guh of
neuper@37906: 	 "thy_" =>
neuper@37935: 	 if member op = [Pbl,Met] p_
neuper@37930:          then message2xml cI "thy-context not to calchead"
neuper@37906: 	 else if pos = ([],Res) then message2xml cI "no thy-context at result"
neuper@37906: 	 else if no_thycontext guh then message2xml cI ("no thy-context for '"^
neuper@37906: 							guh ^ "'")
neuper@37906: 	 else let val (ptp as (pt,_),_) = get_calc cI
neuper@37906: 		  val is = get_istate pt pos
neuper@37906: 		  val subs = subs_from is "dummy" guh
neuper@37906: 		  val tac = guh2rewtac guh subs
neuper@37906: 	      in contextthyOK2xml cI (context_thy (pt, pos) tac) end
neuper@37906: 		  
neuper@37906:        (*.match the model of a problem at pos p 
neuper@37906:           with the model-pattern of the problem with pblID.*)
neuper@37906: (* val (cI, pos:pos' as (p,p_), guh) =
neuper@37906:        (1, p, kestoreID2guh Pbl_ ["univariate","equation"]);
neuper@37906:    val (cI, pos:pos' as (p,p_), guh) =
neuper@37906:        (1, ([],Pbl), kestoreID2guh Pbl_ ["univariate","equation"]);
neuper@37906:    val (cI, pos:pos' as (p,p_), guh) =
neuper@37906:        (1, ([],Pbl), "pbl_equ_univ");
neuper@37906:    *)
neuper@37906:        | "pbl_" => 
neuper@37906: 	 let val ((pt,_),_) = get_calc cI
neuper@37906: 	     val pp = par_pblobj pt p
neuper@37906: 	     val keID = guh2kestoreID guh
neuper@37906: 	     val chd = context_pbl keID pt pp
neuper@37906: 	 in matchpbl2xml cI chd end
neuper@37906: (* val (cI, pos:pos' as (p,p_), guh) = 
neuper@37906:        (1, ([],Pbl), kestoreID2guh Met_ ["LinEq", "solve_lineq_equation"]);
neuper@37906:    *)
neuper@37906:        | "met_" => 
neuper@37906: 	 let val ((pt,_),_) = get_calc cI
neuper@37906: 	     val pp = par_pblobj pt p
neuper@37906: 	     val keID = guh2kestoreID guh
neuper@37906: 	     val chd = context_met keID pt pp
neuper@37906: 	 in matchmet2xml cI chd end)
neuper@37906:     handle _ => sysERROR2xml cI "error in kernel";
neuper@37906: 
neuper@37906: 
neuper@37906: (*------------------------------------------------------------------*)
neuper@37906: end
neuper@37906: open interface;
neuper@37906: (*------------------------------------------------------------------*)