diff -r a28b5fc129b7 -r 22235e4dbe5f src/Tools/isac/Frontend/interface.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/isac/Frontend/interface.sml Wed Aug 25 16:20:07 2010 +0200 @@ -0,0 +1,843 @@ +(* 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 + 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 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*) = +(* val[(fmz,sp):fmz]=[(["fixedValues [r=Arbfix]","maximum A","valuesFor [a,b]", + "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]", + "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]", + "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]", + "boundVariable a","boundVariable b","boundVariable alpha", + "interval {x::real. 0 <= x & x <= 2*r}", + "interval {x::real. 0 <= x & x <= 2*r}", + "interval {x::real. 0 <= x & x <= pi}", + "errorBound (eps=(0::real))"], + ("DiffApp.thy", ["maximum_of","function"], + ["DiffApp","max_by_calculus"]))]; + + *) + (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.thy"); + val (cI, tac) = (1, Specify_Problem ["normalize","polynomial", + "univariate","equation"]); + val (cI, tac) = (1, Subproblem ("Poly.thy", + ["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*) +(* val (cI, ip, tac) = (1, p, hd appltacs); + val (cI, ip, tac) = (1, p, (hd (sel_appl_atomic_tacs pt p))); + *) +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 +(* val ("ok", (tacis, c, (pt',p'))) = locatetac tac (pt, ip); + *) + ("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; + + + +(* val cI = 1; + *) +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 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 = +(* val (cI, auto) = (1,CompleteCalc); + val (cI, auto) = (1,CompleteModel); + val (cI, auto) = (1,CompleteCalcHead); + val (cI, auto) = (1,Step 1); + *) + (let val pold = get_pos cI 1 + val x = autocalc [] pold (get_calc cI) auto + in + case x of +(* val (str, c, ptp as (_,p)) = x; + *) + ("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.thy", ["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.thy", ["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"; +(*.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 = map fst (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 context 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 explode) guh of + "thy_" => +(* val (cI, ip as (_,p_), guh) = (1, p, "thy_isac_Test-rls-Test_simplify"); + *) + 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))) => +(* val (str, (tacis, c, ptp as (_,p))) = locatetac tac (pt, ip); + *) + (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 (p,c,_,pt) = generate1 (assoc_thy"Isac.thy") + m Uistate ip pt + in upd_calc cI ((pt,p),[]); + autocalculateOK2xml cI pold (if null c then pold + else last_elem c) p + end) + end +(* val (cI, ip as (_,p_), guh) = (1, pos, guh); + *) + | "pbl_" => + let val pI = guh2kestoreID guh + 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 "setContext for pbl requires ActiveFormula \ + \on CalcHead" + end +(* val (cI, ip as (_,p_), guh) = (1, pos, "met_eq_lin"); + *) + | "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"; + +(* val (cI, ifo) = (1, "-2 * 1 + (1 + x) = 0"); + val (cI, ifo) = (1, "x = 2"); + val (cI, ifo) = (1, "[x = 3 + -2*1]"); + val (cI, ifo) = (1, "-1 + x = 0"); + val (cI, ifo) = (1, "x - 4711 = 0"); + val (cI, ifo) = (1, "2+ -1 + x = 2"); + val (cI, ifo) = (1, " x - "); + val (cI, ifo) = (1, "(-3 * x + 4 * y + -1 * x * y) / (x * y)"); + val (cI, ifo) = (1, "(4 * y + -3 * x) / (x * y) + -1"); + *) +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 +(* val (str, cs') = step pos cs; + *) + ("ok", cs') => + (case inform cs' (encode ifo) of +(* val (str, (_, c, ptp as (_,p))) = inform cs' (encode ifo); + *) + ("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.*) +(* val (cI, ifo) = (2, "-1 + x = 0"); + val (cI, ifo) = (1, "-1 + x = 0"); + val (cI, ifo) = (1, "x - 1 = 0"); + val (cI, ifo) = (1, "x = 1"); + val (cI, ifo) = (1, "solve(x+1=2,x)"); + val (cI, ifo) = (1, "Simplify (2*a + 3*a)"); + val (cI, ifo) = (1, "Diff (x^2 + x + 1, x)"); + *) +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'))) => +(* val (str, (_,c, ptp' as (pt',p')))= inform ([], [], (pt, p)) (encode ifo); + *) + 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'(*' NEW*) end + | ("same-formula", _) => + (*TODO.WN0501 MESSAGE !*) + 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 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"; + + +(*------------------------------------------------------------------*) +end +open interface; +(*------------------------------------------------------------------*)