1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/Frontend/interface.sml Wed Aug 25 16:20:07 2010 +0200
1.3 @@ -0,0 +1,843 @@
1.4 +(* the interface between the isac-kernel and the java-frontend;
1.5 + the isac-kernel holds calc-trees; stdout in XML-format.
1.6 + authors: Walther Neuper 2002
1.7 + (c) due to copyright terms
1.8 +
1.9 +use"Frontend/interface.sml";
1.10 +use"interface.sml";
1.11 +*)
1.12 +
1.13 +signature INTERFACE =
1.14 + sig
1.15 + val CalcTree : fmz list -> unit
1.16 + val DEconstrCalcTree : calcID -> unit
1.17 + val Iterator : calcID -> unit
1.18 + val IteratorTEST : calcID -> iterID
1.19 + val appendFormula : calcID -> cterm' -> unit
1.20 + val autoCalculate : calcID -> auto -> unit
1.21 + val checkContext : calcID -> pos' -> guh -> unit
1.22 + val fetchApplicableTactics : calcID -> int -> pos' -> unit
1.23 + val fetchProposedTactic : calcID -> unit
1.24 + val applyTactic : calcID -> pos' -> tac -> unit
1.25 + val getAccumulatedAsms : calcID -> pos' -> unit
1.26 + val getActiveFormula : calcID -> unit
1.27 + val getAssumptions : calcID -> pos' -> unit
1.28 + val initContext : calcID -> ketype -> pos' -> unit
1.29 + val getFormulaeFromTo : calcID -> pos' -> pos' -> int -> bool -> unit
1.30 + val getTactic : calcID -> pos' -> unit
1.31 + val interSteps : calcID -> pos' -> unit
1.32 + val modifyCalcHead : calcID -> icalhd -> unit
1.33 + val moveActiveCalcHead : calcID -> unit
1.34 + val moveActiveDown : calcID -> unit
1.35 + val moveActiveDownTEST : calcID -> unit
1.36 + val moveActiveFormula : calcID -> pos' -> unit
1.37 + val moveActiveLevelDown : calcID -> unit
1.38 + val moveActiveLevelUp : calcID -> unit
1.39 + val moveActiveRoot : calcID -> unit
1.40 + val moveActiveRootTEST : calcID -> unit
1.41 + val moveActiveUp : calcID -> unit
1.42 + val moveCalcHead : calcID -> pos' -> unit
1.43 + val moveDown : calcID -> pos' -> unit
1.44 + val moveLevelDown : calcID -> pos' -> unit
1.45 + val moveLevelUp : calcID -> pos' -> unit
1.46 + val moveRoot : calcID -> unit
1.47 + val moveUp : calcID -> pos' -> unit
1.48 + val refFormula : calcID -> pos' -> unit
1.49 + val replaceFormula : calcID -> cterm' -> unit
1.50 + val resetCalcHead : calcID -> unit
1.51 + val modelProblem : calcID -> unit
1.52 + val refineProblem : calcID -> pos' -> guh -> unit
1.53 + val setContext : calcID -> pos' -> guh -> unit
1.54 + val setMethod : calcID -> metID -> unit
1.55 + val setNextTactic : calcID -> tac -> unit
1.56 + val setProblem : calcID -> pblID -> unit
1.57 + val setTheory : calcID -> thyID -> unit
1.58 + end
1.59 +
1.60 +
1.61 +(*------------------------------------------------------------------*)
1.62 +structure interface : INTERFACE =
1.63 +struct
1.64 +(*------------------------------------------------------------------*)
1.65 +
1.66 +(*.encode "Isabelle"-strings as seen by the user to the
1.67 + format accepted by Isabelle.
1.68 + encode "^" ---> "^^^"; see Knowledge/Atools.thy;
1.69 + called for each cterm', icalhd, fmz in this interface;
1.70 + + see "fun decode" in xmlsrc/mathml.sml.*)
1.71 +fun encode (str:cterm') =
1.72 + let fun enc [] = []
1.73 + | enc ("^"::cs) = "^"::"^"::"^"::(enc cs)
1.74 + | enc (c::cs) = c::(enc cs)
1.75 + in (implode o enc o explode) str:cterm' end;
1.76 +fun encode_imodel (imodel:imodel) =
1.77 + let fun enc (Given ifos) = Given (map encode ifos)
1.78 + | enc (Find ifos) = Find (map encode ifos)
1.79 + | enc (Relate ifos) = Relate (map encode ifos)
1.80 + in map enc imodel:imodel end;
1.81 +fun encode_icalhd ((pos', headl, imodel, pos_, spec):icalhd) =
1.82 + (pos', encode headl, encode_imodel imodel, pos_, spec):icalhd;
1.83 +fun encode_fmz ((ifos, spec):fmz) = (map encode ifos, spec):fmz;
1.84 +
1.85 +
1.86 +(***. CalcTree .***)
1.87 +
1.88 +(** add and delete users **)
1.89 +
1.90 +(*.'Iterator 1' must exist with each CalcTree;
1.91 + the only for updating the calc-tree
1.92 + WN.0411: only 'Iterator 1' is stored,
1.93 + all others are just calculated on the fly
1.94 + TODO: adapt Iterator, add_user(= add_iterator!),etc. accordingly .*)
1.95 +fun Iterator (cI:calcID) = (*returned ID unnecessary after WN.0411*)
1.96 + (adduserOK2xml cI (add_user (cI:calcID)))
1.97 + handle _ => sysERROR2xml cI "error in kernel";
1.98 +fun IteratorTEST (cI:calcID) = add_user (cI:calcID);
1.99 +(*fun DEconstructIterator (cI:calcID) (uI:iterID) =
1.100 + deluserOK2xml (del_user cI uI);*)
1.101 +
1.102 +(*.create a calc-tree; for calls from java: thus ^^^ decoded to ^;
1.103 + compare "fun CalcTreeTEST" which does NOT decode.*)
1.104 +fun CalcTree
1.105 + [(fmz, sp):fmz] (*for several variants lateron*) =
1.106 +(* val[(fmz,sp):fmz]=[(["fixedValues [r=Arbfix]","maximum A","valuesFor [a,b]",
1.107 + "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
1.108 + "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
1.109 + "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
1.110 + "boundVariable a","boundVariable b","boundVariable alpha",
1.111 + "interval {x::real. 0 <= x & x <= 2*r}",
1.112 + "interval {x::real. 0 <= x & x <= 2*r}",
1.113 + "interval {x::real. 0 <= x & x <= pi}",
1.114 + "errorBound (eps=(0::real))"],
1.115 + ("DiffApp.thy", ["maximum_of","function"],
1.116 + ["DiffApp","max_by_calculus"]))];
1.117 +
1.118 + *)
1.119 + (let val cs = nxt_specify_init_calc (encode_fmz (fmz, sp))
1.120 + (*FIXME.WN.8.03: error-handling missing*)
1.121 + val cI = add_calc cs
1.122 + in calctreeOK2xml cI end)
1.123 + handle _ => sysERROR2xml 0 "error in kernel";
1.124 +
1.125 +fun DEconstrCalcTree (cI:calcID) =
1.126 + deconstructcalctreeOK2xml (del_calc cI);
1.127 +
1.128 +
1.129 +fun getActiveFormula (cI:calcID) = iteratorOK2xml cI (get_pos cI 1);
1.130 +
1.131 +fun moveActiveFormula (cI:calcID) (p:pos') =
1.132 + let val ((pt,_),_) = get_calc cI
1.133 + in if existpt' p pt then (upd_ipos cI 1 p; iteratorOK2xml cI p)
1.134 + else sysERROR2xml cI "frontend sends a non-existing pos" end;
1.135 +
1.136 +(*. set the next tactic to be applied: dont't change the calc-tree,
1.137 + but remember the envisaged changes for fun autoCalculate;
1.138 + compare force NextTactic .*)
1.139 +(* val (cI, tac) = (1, Add_Given "equality (x ^^^ 2 + 4 * x + 3 = 0)");
1.140 + val (cI, tac) = (1, Specify_Theory "PolyEq.thy");
1.141 + val (cI, tac) = (1, Specify_Problem ["normalize","polynomial",
1.142 + "univariate","equation"]);
1.143 + val (cI, tac) = (1, Subproblem ("Poly.thy",
1.144 + ["polynomial","univariate","equation"]));
1.145 + val (cI, tac) = (1, Model_Problem["linear","univariate","equation","test"]);
1.146 + val (cI, tac) = (1, Detail_Set "Test_simplify");
1.147 + val (cI, tac) = (1, Apply_Method ["Test", "solve_linear"]);
1.148 + val (cI, tac) = (1, Rewrite_Set "Test_simplify");
1.149 + *)
1.150 +fun setNextTactic (cI:calcID) tac =
1.151 + let val ((pt, _), _) = get_calc cI
1.152 + val ip = get_pos cI 1
1.153 + in case locatetac tac (pt, ip) of
1.154 +(* val ("ok", (tacis, c, (_,p'))) = locatetac tac (pt, ip);
1.155 + *)
1.156 + ("ok", (tacis, _, _)) =>
1.157 + (upd_calc cI ((pt, ip), tacis); setnexttactic2xml cI "ok")
1.158 + | ("unsafe-ok", (tacis, _, _)) =>
1.159 + (upd_calc cI ((pt, ip), tacis); setnexttactic2xml cI "unsafe-ok")
1.160 + | ("not-applicable",_) => setnexttactic2xml cI "not-applicable"
1.161 + | ("end-of-calculation",_) =>
1.162 + setnexttactic2xml cI "end-of-calculation"
1.163 + | ("failure",_) => sysERROR2xml cI "failure"
1.164 + end;
1.165 +
1.166 +(*. apply a tactic at a position and update the calc-tree if applicable .*)
1.167 +(*WN080226 java-code is missing, errors smltest/Knowledge/polyminus.sml*)
1.168 +(* val (cI, ip, tac) = (1, p, hd appltacs);
1.169 + val (cI, ip, tac) = (1, p, (hd (sel_appl_atomic_tacs pt p)));
1.170 + *)
1.171 +fun applyTactic (cI:calcID) ip tac =
1.172 + let val ((pt, _), _) = get_calc cI
1.173 + val p = get_pos cI 1
1.174 + in case locatetac tac (pt, ip) of
1.175 +(* val ("ok", (tacis, c, (pt',p'))) = locatetac tac (pt, ip);
1.176 + *)
1.177 + ("ok", (_, c, ptp as (_,p'))) =>
1.178 + (upd_calc cI (ptp, []); upd_ipos cI 1 p';
1.179 + autocalculateOK2xml cI p (if null c then p'
1.180 + else last_elem c) p')
1.181 + | ("unsafe-ok", (_, c, ptp as (_,p'))) =>
1.182 + (upd_calc cI (ptp, []); upd_ipos cI 1 p';
1.183 + autocalculateOK2xml cI p (if null c then p'
1.184 + else last_elem c) p')
1.185 + | ("end-of-calculation", (_, c, ptp as (_,p'))) =>
1.186 + (upd_calc cI (ptp, []); upd_ipos cI 1 p';
1.187 + autocalculateOK2xml cI p (if null c then p'
1.188 + else last_elem c) p')
1.189 +
1.190 +
1.191 + | (str,_) => autocalculateERROR2xml cI "failure"
1.192 + end;
1.193 +
1.194 +
1.195 +
1.196 +(* val cI = 1;
1.197 + *)
1.198 +fun fetchProposedTactic (cI:calcID) =
1.199 + (case step (get_pos cI 1) (get_calc cI) of
1.200 + ("ok", (tacis, _, _)) =>
1.201 + let val _= upd_tacis cI tacis
1.202 + val (tac,_,_) = last_elem tacis
1.203 + in fetchproposedtacticOK2xml cI tac end
1.204 + | ("helpless",_) => fetchproposedtacticERROR2xml cI "helpless"
1.205 + | ("no-fmz-spec",_) => fetchproposedtacticERROR2xml cI "no-fmz-spec"
1.206 + | ("end-of-calculation",_) =>
1.207 + fetchproposedtacticERROR2xml cI "end-of-calculation")
1.208 + handle _ => sysERROR2xml cI "error in kernel";
1.209 +
1.210 +(*datatype auto = FIXXXME040624: does NOT match interfaces/ITOCalc.java
1.211 + Step of int (*1 do #int steps (may stop in model/specify)
1.212 + IS VERY INEFFICIENT IN MODEL/SPECIY*)
1.213 +| CompleteModel (*2 complete modeling
1.214 + if model complete, finish specifying*)
1.215 +| CompleteCalcHead (*3 complete model/specify in one go*)
1.216 +| CompleteToSubpbl (*4 stop at the next begin of a subproblem,
1.217 + if none, complete the actual (sub)problem*)
1.218 +| CompleteSubpbl (*5 complete the actual (sub)problem (incl.ev.subproblems)*)
1.219 +| CompleteCalc; (*6 complete the calculation as a whole*)*)
1.220 +fun autoCalculate (cI:calcID) auto =
1.221 +(* val (cI, auto) = (1,CompleteCalc);
1.222 + val (cI, auto) = (1,CompleteModel);
1.223 + val (cI, auto) = (1,CompleteCalcHead);
1.224 + val (cI, auto) = (1,Step 1);
1.225 + *)
1.226 + (let val pold = get_pos cI 1
1.227 + val x = autocalc [] pold (get_calc cI) auto
1.228 + in
1.229 + case x of
1.230 +(* val (str, c, ptp as (_,p)) = x;
1.231 + *)
1.232 + ("ok", c, ptp as (_,p)) =>
1.233 + (upd_calc cI (ptp, []); upd_ipos cI 1 p;
1.234 + autocalculateOK2xml cI pold (if null c then pold
1.235 + else last_elem c) p)
1.236 + | ("end-of-calculation", c, ptp as (_,p)) =>
1.237 + (upd_calc cI (ptp, []); upd_ipos cI 1 p;
1.238 + autocalculateOK2xml cI pold (if null c then pold
1.239 + else last_elem c) p)
1.240 + | (str, _, _) => autocalculateERROR2xml cI str
1.241 + end)
1.242 + handle _ => sysERROR2xml cI "error in kernel";
1.243 +
1.244 +
1.245 +(* val (cI:calcID, ichd as ((p,_),_,_,_,_):icalhd) =
1.246 + (1, (([],Pbl), "not used here",
1.247 + [Given ["fixedValues [r=Arbfix]"],
1.248 + Find ["maximum A", "valuesFor [a,b]"(*new input*)],
1.249 + Relate ["relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]"]], Pbl,
1.250 + ("DiffApp.thy", ["maximum_of","function"],
1.251 + ["DiffApp","max_by_calculus"])));
1.252 + val (cI:calcID, ichd as ((p,_),_,_,_,_):icalhd) =
1.253 + (1, (([],Pbl),"solve (x+1=2, x)",
1.254 + [Given ["equality (x+1=2)", "solveFor x"],
1.255 + Find ["solutions L"]],
1.256 + Pbl,
1.257 + ("Test.thy", ["linear","univariate","equation","test"],
1.258 + ["Test","solve_linear"])));
1.259 + val (cI:calcID, ichd as ((p,_),_,_,_,_):icalhd) =
1.260 + (1, (([],Pbl),"solveTest (1+-1*2+x=0,x)", [], Pbl, ("", [], [])));
1.261 + val (cI, p:pos')=(1, ([1],Frm));
1.262 + val (cI, p:pos')=(1, ([1,2,1,3],Res));
1.263 + *)
1.264 +fun getTactic cI (p:pos') =
1.265 + (let val ((pt,_),_) = get_calc cI
1.266 + val (form, tac, asms) = pt_extract (pt, p)
1.267 + in case tac of
1.268 +(* val SOME ta = tac;
1.269 + *)
1.270 + SOME ta => gettacticOK2xml cI ta
1.271 + | NONE => gettacticERROR2xml cI ("no tactic at position "^pos'2str p)
1.272 + end)
1.273 + handle _ => sysERROR2xml cI "syserror in getTactic";
1.274 +
1.275 +(*. see ICalcIterator#fetchApplicableTactics
1.276 + @see #TACTICS_ALL
1.277 + @see #TACTICS_CURRENT_THEORY
1.278 + @see #TACTICS_CURRENT_METHOD ..the only impl.WN040307.*)
1.279 +(*. fetch tactics to be applied to a particular step.*)
1.280 +(* WN071231 kept this version for later parametrisation*)
1.281 +(*.version 1: fetch _all_ tactics from script .*)
1.282 +fun fetchApplicableTactics cI (scope:int) (p:pos') =
1.283 + (let val ((pt, _), _) = get_calc cI
1.284 + in (applicabletacticsOK cI (sel_rules pt p))
1.285 + handle PTREE str => sysERROR2xml cI str
1.286 + end)
1.287 + handle _ => sysERROR2xml cI "error in kernel";
1.288 +(*.version 2: fetch _applicable_ _elementary_ (ie. recursively
1.289 + decompose rule-sets) Rewrite*, Calculate .*)
1.290 +fun fetchApplicableTactics cI (scope:int) (p:pos') =
1.291 + (let val ((pt, _), _) = get_calc cI
1.292 + in (applicabletacticsOK cI (sel_appl_atomic_tacs pt p))
1.293 + handle PTREE str => sysERROR2xml cI str
1.294 + end)
1.295 + handle _ => sysERROR2xml cI "error in kernel";
1.296 +
1.297 +fun getAssumptions cI (p:pos') =
1.298 + (let val ((pt,_),_) = get_calc cI
1.299 + val (_, _, asms) = pt_extract (pt, p)
1.300 + in getasmsOK2xml cI asms end)
1.301 + handle _ => sysERROR2xml cI "syserror in getAssumptions";
1.302 +
1.303 +(*WN0502 @see ME/ctree: type asms: illdesigned, thus no positions returned*)
1.304 +fun getAccumulatedAsms cI (p:pos') =
1.305 + (let val ((pt, _), _) = get_calc cI
1.306 + val ass = map fst (get_assumptions_ pt p)
1.307 + in (*getaccuasmsOK2xml cI (get_assumptions_ pt p)*)
1.308 + getasmsOK2xml cI ass end)
1.309 + handle _ => sysERROR2xml cI "syserror in getAccumulatedAsms";
1.310 +
1.311 +
1.312 +(*since moveActive* does NOT transfer pos java --> sml (only sml --> java)
1.313 + refFormula might become involved in far-off errors !!!*)
1.314 +fun refFormula cI (p:pos') = (*WN0501 rename to 'fun getElement' !*)
1.315 +(* val (cI, uI) = (1,1);
1.316 + *)
1.317 + (let val ((pt,_),_) = get_calc cI
1.318 + val (form, tac, asms) = pt_extract (pt, p)
1.319 + in refformulaOK2xml cI p form end)
1.320 + handle _ => sysERROR2xml cI "error in kernel";
1.321 +
1.322 +(*.get formulae 'from' 'to' w.r.t. ordering in Position#compareTo(Position p);
1.323 + in case of CalcHeads only the headline is taken
1.324 + (the pos' allows distinction between PrfObj and PblObj anyway);
1.325 + 'level' is adjusted such that an 'interval' of formulae is returned;
1.326 + 'from' 'to' are designed for use by iterators of calcChangedEvent;
1.327 + thus 'from' is the last unchanged position.*)
1.328 +fun getFormulaeFromTo cI (from as ([],Pbl):pos') (to as ([],Pbl):pos')_ false =
1.329 +(*special case because 'from' is _before_ the first elements to be returned*)
1.330 +(* val (cI, from, to, level) = (1, ([],Pbl), ([],Pbl), 1);
1.331 + *)
1.332 + ((let val ((pt,_),_) = get_calc cI
1.333 + val (ModSpec (_,_,headline,_,_,_),_,_) = pt_extract (pt, to)
1.334 + in getintervalOK cI [(to, headline)] end)
1.335 + handle _ => sysERROR2xml cI "error in kernel")
1.336 +
1.337 + | getFormulaeFromTo cI (from as ([],Pbl):pos') (to as ([],Met):pos')_ false =
1.338 + getFormulaeFromTo cI ([],Pbl) ([],Pbl) (~00000) false
1.339 +
1.340 + | getFormulaeFromTo cI (from:pos') (to:pos') level false =
1.341 +(* val (cI, from, to, level) = (1, unc, gen, 0);
1.342 + val (cI, from, to, level) = (1, unc, gen, 1);
1.343 + val (cI, from, to, level) = (1, ([],Pbl), ([],Met), 1);
1.344 + *)
1.345 + (if from = to then sysERROR2xml cI "getFormulaeFromTo: From = To"
1.346 + else
1.347 + (case from of
1.348 + ([],Res) => sysERROR2xml cI "getFormulaeFromTo does: moveDown \
1.349 + \from=([],Res) .. goes beyond result"
1.350 + | _ => let val ((pt,_),_) = get_calc cI
1.351 + val f = move_dn [] pt from
1.352 + fun max (a,b) = if a < b then b else a
1.353 + (*must reach margins ...*)
1.354 + val lev = max (level, max (lev_of from, lev_of to))
1.355 + in getintervalOK cI (get_interval f to lev pt) end)
1.356 + handle _ => sysERROR2xml cI "error in getFormulaeFromTo")
1.357 +
1.358 + | getFormulaeFromTo cI from to level true =
1.359 + sysERROR2xml cI "getFormulaeFromTo impl.for formulae only,\
1.360 + \i.e. last arg only impl. for false, _NOT_ true";
1.361 +
1.362 +
1.363 +(* val (cI, ip) = (1, ([1,9], Res));
1.364 + val (cI, ip) = (1, ([], Res));
1.365 + val (cI, ip) = (1, ([2], Res));
1.366 + val (cI, ip) = (1, ([3,1], Res));
1.367 + val (cI, ip) = (1, ([1,2,1], Res));
1.368 + *)
1.369 +fun interSteps cI ip =
1.370 + (let val ((pt,p), tacis) = get_calc cI
1.371 + in if (not o is_interpos) ip
1.372 + then interStepsERROR cI "only formulae with position (_,Res) \
1.373 + \may have intermediate steps above them"
1.374 + else let val ip' = lev_pred' pt ip
1.375 +(* val (str, pt', lastpos) = detailstep pt ip;
1.376 + *)
1.377 + in case detailstep pt ip of
1.378 + ("detailrls", pt(*, pos'forms*), lastpos) =>
1.379 + (upd_calc cI ((pt, p), tacis);
1.380 + interStepsOK cI (*pos'forms*) ip' ip' lastpos)
1.381 + | ("no-Rewrite_Set...", _, _) =>
1.382 + sysERROR2xml cI "no Rewrite_Set..."
1.383 + | (_, _(*, pos'formshds*), lastpos) =>
1.384 + interStepsOK cI (*pos'formshds*) ip' ip' lastpos
1.385 + end
1.386 + end)
1.387 + handle _ => sysERROR2xml cI "error in kernel";
1.388 +
1.389 +fun modifyCalcHead (cI:calcID) (ichd as ((p,_),_,_,_,_):icalhd) =
1.390 + (let val ((pt,_),_) = get_calc cI
1.391 + val (pt, chd as (_,p_,_,_,_,_)) = input_icalhd pt ichd
1.392 + in (upd_calc cI ((pt, (p,p_)), []);
1.393 + modifycalcheadOK2xml cI chd) end)
1.394 + handle _ => sysERROR2xml cI "error in kernel";
1.395 +
1.396 +(*.at the activeFormula set the Model, the Guard and the Specification
1.397 + to empty and return a CalcHead;
1.398 + the 'origin' remains (for reconstructing all that).*)
1.399 +fun resetCalcHead (cI:calcID) =
1.400 + (let val (ptp,_) = get_calc cI
1.401 + val ptp = reset_calchead ptp
1.402 + in (upd_calc cI (ptp, []);
1.403 + modifycalcheadOK2xml cI (get_ocalhd ptp)) end)
1.404 + handle _ => sysERROR2xml cI "error in kernel";
1.405 +
1.406 +(*.at the activeFormula insert all the Descriptions in the Model
1.407 + (_not_ in the Guard) and return a CalcHead;
1.408 + the Descriptions are for user-guidance; the rest of the items
1.409 + are left empty for user-input;
1.410 + includes a resetCalcHead for the Model and the Guard.*)
1.411 +fun modelProblem (cI:calcID) =
1.412 + (let val (ptp, _) = get_calc cI
1.413 + val ptp = reset_calchead ptp
1.414 + val (_, _, ptp) = nxt_specif Model_Problem ptp
1.415 + in (upd_calc cI (ptp, []);
1.416 + modifycalcheadOK2xml cI (get_ocalhd ptp)) end)
1.417 + handle _ => sysERROR2xml cI "error in kernel";
1.418 +
1.419 +
1.420 +(*.set the context determined on a knowledgebrowser to the current calc.*)
1.421 +fun setContext (cI:calcID) (ip as (_,p_):pos') (guh:guh) =
1.422 + (case (implode o (take_fromto 1 4) o explode) guh of
1.423 + "thy_" =>
1.424 +(* val (cI, ip as (_,p_), guh) = (1, p, "thy_isac_Test-rls-Test_simplify");
1.425 + *)
1.426 + if member op = [Pbl,Met] p_
1.427 + then message2xml cI "thy-context not to calchead"
1.428 + else if ip = ([],Res) then message2xml cI "no thy-context at result"
1.429 + else if no_thycontext guh then message2xml cI ("no thy-context for '"^
1.430 + guh ^ "'")
1.431 + else let val (ptp as (pt,pold),_) = get_calc cI
1.432 + val is = get_istate pt ip
1.433 + val subs = subs_from is "dummy" guh
1.434 + val tac = guh2rewtac guh subs
1.435 + in case locatetac tac (pt, ip) of (*='fun setNextTactic'+step*)
1.436 + ("ok", (tacis, c, ptp as (_,p))) =>
1.437 +(* val (str, (tacis, c, ptp as (_,p))) = locatetac tac (pt, ip);
1.438 + *)
1.439 + (upd_calc cI ((pt,p), []);
1.440 + autocalculateOK2xml cI pold (if null c then pold
1.441 + else last_elem c) p)
1.442 + | ("unsafe-ok", (tacis, c, ptp as (_,p))) =>
1.443 + (upd_calc cI ((pt,p), []);
1.444 + autocalculateOK2xml cI pold (if null c then pold
1.445 + else last_elem c) p)
1.446 + | ("end-of-calculation",_) =>
1.447 + message2xml cI "end-of-calculation"
1.448 + | ("failure",_) => sysERROR2xml cI "failure"
1.449 + | ("not-applicable",_) => (*the rule comes from anywhere..*)
1.450 + (case applicable_in ip pt tac of
1.451 +
1.452 + Notappl e => message2xml cI ("'" ^ tac2str tac ^
1.453 + "' not-applicable")
1.454 + | Appl m =>
1.455 + let val (p,c,_,pt) = generate1 (assoc_thy"Isac.thy")
1.456 + m Uistate ip pt
1.457 + in upd_calc cI ((pt,p),[]);
1.458 + autocalculateOK2xml cI pold (if null c then pold
1.459 + else last_elem c) p
1.460 + end)
1.461 + end
1.462 +(* val (cI, ip as (_,p_), guh) = (1, pos, guh);
1.463 + *)
1.464 + | "pbl_" =>
1.465 + let val pI = guh2kestoreID guh
1.466 + val ((pt, _), _) = get_calc cI
1.467 + (*val ip as (_, p_) = get_pos cI 1*)
1.468 + in if member op = [Pbl, Met] p_
1.469 + then let val (pt, chd) = set_problem pI (pt, ip)
1.470 + in (upd_calc cI ((pt, ip), []);
1.471 + modifycalcheadOK2xml cI chd) end
1.472 + else sysERROR2xml cI "setContext for pbl requires ActiveFormula \
1.473 + \on CalcHead"
1.474 + end
1.475 +(* val (cI, ip as (_,p_), guh) = (1, pos, "met_eq_lin");
1.476 + *)
1.477 + | "met_" =>
1.478 + let val mI = guh2kestoreID guh
1.479 + val ((pt, _), _) = get_calc cI
1.480 + in if member op = [Pbl, Met] p_
1.481 + then let val (pt, chd) = set_method mI (pt, ip)
1.482 + in (upd_calc cI ((pt, ip), []);
1.483 + modifycalcheadOK2xml cI chd) end
1.484 + else sysERROR2xml cI "setContext for met requires ActiveFormula \
1.485 + \on CalcHead"
1.486 + end)
1.487 + handle _ => sysERROR2xml cI "error in kernel";
1.488 +
1.489 +
1.490 +(*.specify the Method at the activeFormula and return a CalcHead
1.491 + containing the Guard.
1.492 + WN0512 impl.incomplete, see 'nxt_specif (Specify_Method '.*)
1.493 +fun setMethod (cI:calcID) (mI:metID) =
1.494 +(* val (cI, mI) = (1, ["Test","solve_linear"]);
1.495 + *)
1.496 + (let val ((pt, _), _) = get_calc cI
1.497 + val ip as (_, p_) = get_pos cI 1
1.498 + in if member op = [Pbl,Met] p_
1.499 + then let val (pt, chd) = set_method mI (pt, ip)
1.500 + in (upd_calc cI ((pt, ip), []);
1.501 + modifycalcheadOK2xml cI chd) end
1.502 + else sysERROR2xml cI "setMethod requires ActiveFormula on CalcHead"
1.503 + end)
1.504 + handle _ => sysERROR2xml cI "error in kernel";
1.505 +
1.506 +(*.specify the Problem at the activeFormula and return a CalcHead
1.507 + containing the Model; special case of checkContext;
1.508 + WN0512 impl.incomplete, see 'nxt_specif (Specify_Problem '.*)
1.509 +fun setProblem (cI:calcID) (pI:pblID) =
1.510 + (let val ((pt, _), _) = get_calc cI
1.511 + val ip as (_, p_) = get_pos cI 1
1.512 + in if member op = [Pbl,Met] p_
1.513 + then let val (pt, chd) = set_problem pI (pt, ip)
1.514 + in (upd_calc cI ((pt, ip), []);
1.515 + modifycalcheadOK2xml cI chd) end
1.516 + else sysERROR2xml cI "setProblem requires ActiveFormula on CalcHead"
1.517 + end)
1.518 + handle _ => sysERROR2xml cI "error in kernel";
1.519 +
1.520 +(*.specify the Theory at the activeFormula and return a CalcHead;
1.521 + special case of checkContext;
1.522 + WN0512 impl.incomplete, see 'nxt_specif (Specify_Method '.*)
1.523 +fun setTheory (cI:calcID) (tI:thyID) =
1.524 + (let val ((pt, _), _) = get_calc cI
1.525 + val ip as (_, p_) = get_pos cI 1
1.526 + in if member op = [Pbl,Met] p_
1.527 + then let val (pt, chd) = set_theory tI (pt, ip)
1.528 + in (upd_calc cI ((pt, ip), []);
1.529 + modifycalcheadOK2xml cI chd) end
1.530 + else sysERROR2xml cI "setProblem requires ActiveFormula on CalcHead"
1.531 + end)
1.532 + handle _ => sysERROR2xml cI "error in kernel";
1.533 +
1.534 +
1.535 +(**. without update of CalcTree .**)
1.536 +
1.537 +(*.match the model of a problem at pos p
1.538 + with the model-pattern of the problem with pblID*)
1.539 +(*fun tryMatchProblem cI pblID =
1.540 + (let val ((pt,_),_) = get_calc cI
1.541 + val p = get_pos cI 1
1.542 + val chd = trymatch pblID pt p
1.543 + in trymatchOK2xml cI chd end)
1.544 + handle _ => sysERROR2xml cI "error in kernel";*)
1.545 +
1.546 +(*.refinement for the parent-problem of the position.*)
1.547 +(* val (cI, (p,p_), guh) = (1, ([1],Res), "pbl_equ_univ");
1.548 + *)
1.549 +fun refineProblem cI ((p,p_) : pos') (guh : guh) =
1.550 + (let val pblID = guh2kestoreID guh
1.551 + val ((pt,_),_) = get_calc cI
1.552 + val pp = par_pblobj pt p
1.553 + val chd = tryrefine pblID pt (pp, p_)
1.554 + in matchpbl2xml cI chd end)
1.555 + handle _ => sysERROR2xml cI "error in kernel";
1.556 +
1.557 +(* val (cI, ifo) = (1, "-2 * 1 + (1 + x) = 0");
1.558 + val (cI, ifo) = (1, "x = 2");
1.559 + val (cI, ifo) = (1, "[x = 3 + -2*1]");
1.560 + val (cI, ifo) = (1, "-1 + x = 0");
1.561 + val (cI, ifo) = (1, "x - 4711 = 0");
1.562 + val (cI, ifo) = (1, "2+ -1 + x = 2");
1.563 + val (cI, ifo) = (1, " x - ");
1.564 + val (cI, ifo) = (1, "(-3 * x + 4 * y + -1 * x * y) / (x * y)");
1.565 + val (cI, ifo) = (1, "(4 * y + -3 * x) / (x * y) + -1");
1.566 + *)
1.567 +fun appendFormula cI (ifo:cterm') =
1.568 + (let val cs = get_calc cI
1.569 + val pos as (_,p_) = get_pos cI 1
1.570 + in case step pos cs of
1.571 +(* val (str, cs') = step pos cs;
1.572 + *)
1.573 + ("ok", cs') =>
1.574 + (case inform cs' (encode ifo) of
1.575 +(* val (str, (_, c, ptp as (_,p))) = inform cs' (encode ifo);
1.576 + *)
1.577 + ("ok", (_(*use in DG !!!*), c, ptp as (_,p))) =>
1.578 + (upd_calc cI (ptp, []); upd_ipos cI 1 p;
1.579 + appendformulaOK2xml cI pos (if null c then pos
1.580 + else last_elem c) p)
1.581 + | ("same-formula", (_, c, ptp as (_,p))) =>
1.582 + (upd_calc cI (ptp, []); upd_ipos cI 1 p;
1.583 + appendformulaOK2xml cI pos (if null c then pos
1.584 + else last_elem c) p)
1.585 + | (msg, _) => appendformulaERROR2xml cI msg)
1.586 + | (msg, cs') => appendformulaERROR2xml cI msg
1.587 + end)
1.588 + handle _ => sysERROR2xml cI "error in kernel";
1.589 +
1.590 +
1.591 +
1.592 +(*.replace a formula with_in_ a calculation;
1.593 + this situation applies for initial CAS-commands, too.*)
1.594 +(* val (cI, ifo) = (2, "-1 + x = 0");
1.595 + val (cI, ifo) = (1, "-1 + x = 0");
1.596 + val (cI, ifo) = (1, "x - 1 = 0");
1.597 + val (cI, ifo) = (1, "x = 1");
1.598 + val (cI, ifo) = (1, "solve(x+1=2,x)");
1.599 + val (cI, ifo) = (1, "Simplify (2*a + 3*a)");
1.600 + val (cI, ifo) = (1, "Diff (x^2 + x + 1, x)");
1.601 + *)
1.602 +fun replaceFormula cI (ifo:cterm') =
1.603 + (let val ((pt, _), _) = get_calc cI
1.604 + val p = get_pos cI 1
1.605 + in case inform (([], [], (pt, p)): calcstate') (encode ifo) of
1.606 + ("ok", (_(*tacs used for DG ?*), c, ptp' as (pt',p'))) =>
1.607 +(* val (str, (_,c, ptp' as (pt',p')))= inform ([], [], (pt, p)) (encode ifo);
1.608 + *)
1.609 + let val unc = if null (fst p) then p else move_up [] pt p
1.610 + val _ = upd_calc cI (ptp', [])
1.611 + val _ = upd_ipos cI 1 p'
1.612 + in replaceformulaOK2xml cI unc
1.613 + (if null c then unc
1.614 + else last_elem c) p'(*' NEW*) end
1.615 + | ("same-formula", _) =>
1.616 + (*TODO.WN0501 MESSAGE !*)
1.617 + replaceformulaERROR2xml cI "formula not changed"
1.618 + | (msg, _) => replaceformulaERROR2xml cI msg
1.619 + end)
1.620 + handle _ => sysERROR2xml cI "error in kernel";
1.621 +
1.622 +
1.623 +
1.624 +(***. CalcIterator
1.625 + moveActive*: set the pos' of the active formula stored with the calctree
1.626 + could take pos' as argument for consistency checks
1.627 + move*: compute the new iterator from the old one on the fly
1.628 +
1.629 +.***)
1.630 +
1.631 +fun moveActiveRoot cI =
1.632 + (let val _ = upd_ipos cI 1 ([],Pbl)
1.633 + in iteratorOK2xml cI ([],Pbl) end)
1.634 + handle e => sysERROR2xml cI "error in kernel";
1.635 +fun moveRoot cI =
1.636 + (iteratorOK2xml cI ([],Pbl))
1.637 + handle e => sysERROR2xml cI "";
1.638 +fun moveActiveRootTEST cI =
1.639 + (let val _ = upd_ipos cI 1 ([],Pbl)
1.640 + in (*iteratorOK2xml cI ([],Pbl)*)() end)
1.641 + handle e => sysERROR2xml cI "error in kernel";
1.642 +
1.643 +(* val (cI, uI) = (1,1);
1.644 + val (cI, uI) = (1,2);
1.645 + *)
1.646 +fun moveActiveDown cI =
1.647 + ((let val ((pt,_),_) = get_calc cI
1.648 +(* val (P, (Nd (_, ns)), (p::(ps as (_::_)), p_)) =([]:pos, pt, get_pos cI uI);
1.649 + val (P, (Nd (c, ns)), ([p], p_)) =([]:pos, pt, get_pos cI uI);
1.650 +
1.651 + print_depth 7;pt
1.652 + *)
1.653 + val ip' = move_dn [] pt (get_pos cI 1)
1.654 + val _ = upd_ipos cI 1 ip'
1.655 + in iteratorOK2xml cI ip' end)
1.656 + handle (PTREE e) => iteratorERROR2xml cI)
1.657 + handle _ => sysERROR2xml cI "error in kernel";
1.658 +fun moveDown cI (p:pos') =
1.659 + ((let val ((pt,_),_) = get_calc cI
1.660 +(* val (P, (Nd (_, ns)), (p::(ps as (_::_)), p_)) =([]:pos, pt, get_pos cI uI);
1.661 + val (P, (Nd (c, ns)), ([p], p_)) =([]:pos, pt, get_pos cI uI);
1.662 +
1.663 + print_depth 7;pt
1.664 + *)
1.665 + val ip' = move_dn [] pt p
1.666 + in iteratorOK2xml cI ip' end)
1.667 + handle (PTREE e) => iteratorERROR2xml cI)
1.668 + handle _ => sysERROR2xml cI "error in kernel";
1.669 +fun moveActiveDownTEST cI =
1.670 + let val ((pt,_),_) = get_calc cI
1.671 + val ip = get_pos cI 1
1.672 + val ip' = (move_dn [] pt ip)
1.673 + handle _ => ip
1.674 + val _ = upd_ipos cI 1 ip'
1.675 + in (*iteratorOK2xml cI uI*)() end;
1.676 +
1.677 +fun moveActiveLevelDown cI =
1.678 + ((let val ((pt,_),_) = get_calc cI
1.679 + val ip' = movelevel_dn [] pt (get_pos cI 1)
1.680 + val _ = upd_ipos cI 1 ip'
1.681 + in iteratorOK2xml cI ip' end)
1.682 + handle (PTREE e) => iteratorERROR2xml cI)
1.683 + handle _ => sysERROR2xml cI "error in kernel";
1.684 +fun moveLevelDown cI (p:pos') =
1.685 + ((let val ((pt,_),_) = get_calc cI
1.686 + val ip' = movelevel_dn [] pt p
1.687 + in iteratorOK2xml cI ip' end)
1.688 + handle (PTREE e) => iteratorERROR2xml cI)
1.689 + handle _ => sysERROR2xml cI "error in kernel";
1.690 +
1.691 +fun moveActiveUp cI =
1.692 + ((let val ((pt,_),_) = get_calc cI
1.693 + val ip' = move_up [] pt (get_pos cI 1)
1.694 + val _ = upd_ipos cI 1 ip'
1.695 + in iteratorOK2xml cI ip' end)
1.696 + handle PTREE e => iteratorERROR2xml cI)
1.697 + handle _ => sysERROR2xml cI "error in kernel";
1.698 +fun moveUp cI (p:pos') =
1.699 + ((let val ((pt,_),_) = get_calc cI
1.700 + val ip' = move_up [] pt p
1.701 + in iteratorOK2xml cI ip' end)
1.702 + handle PTREE e => iteratorERROR2xml cI)
1.703 + handle _ => sysERROR2xml cI "error in kernel";
1.704 +
1.705 +fun moveActiveLevelUp cI =
1.706 + ((let val ((pt,_),_) = get_calc cI
1.707 + val ip' = movelevel_up [] pt (get_pos cI 1)
1.708 + val _ = upd_ipos cI 1 ip'
1.709 + in iteratorOK2xml cI ip' end)
1.710 + handle PTREE e => iteratorERROR2xml cI)
1.711 + handle _ => sysERROR2xml cI "error in kernel";
1.712 +fun moveLevelUp cI (p:pos') =
1.713 + ((let val ((pt,_),_) = get_calc cI
1.714 + val ip' = movelevel_up [] pt p
1.715 + in iteratorOK2xml cI ip' end)
1.716 + handle PTREE e => iteratorERROR2xml cI)
1.717 + handle _ => sysERROR2xml cI "error in kernel";
1.718 +
1.719 +fun moveActiveCalcHead cI =
1.720 + ((let val ((pt,_),_) = get_calc cI
1.721 + val ip' = movecalchd_up pt (get_pos cI 1)
1.722 + val _ = upd_ipos cI 1 ip'
1.723 + in iteratorOK2xml cI ip' end)
1.724 + handle PTREE e => iteratorERROR2xml cI)
1.725 + handle _ => sysERROR2xml cI "error in kernel";
1.726 +fun moveCalcHead cI (p:pos') =
1.727 + ((let val ((pt,_),_) = get_calc cI
1.728 + val ip' = movecalchd_up pt p
1.729 + in iteratorOK2xml cI ip' end)
1.730 + handle PTREE e => iteratorERROR2xml cI)
1.731 + handle _ => sysERROR2xml cI "error in kernel";
1.732 +
1.733 +
1.734 +(*.initContext Thy_ is conceptually impossible at [Pbl,Met]
1.735 + and at positions with Check_Postcond and End_Trans;
1.736 + at possible pos's there can be NO rewrite (returned as a context, too).*)
1.737 +(* val (cI, Thy_, (pos as (p,p_):pos')) = (1, Thy_, ([1], Frm));
1.738 + val (cI, Thy_, (pos as (p,p_):pos')) = (1, Thy_, ([], Res));
1.739 + val (cI, Thy_, (pos as (p,p_):pos')) = (1, Thy_, ([2], Res));
1.740 + val (cI, Thy_, (pos as (p,p_):pos')) = (1, Thy_, ([1,1], Frm));
1.741 + *)
1.742 +fun initContext (cI:calcID) Thy_ (pos as (p,p_):pos') =
1.743 + ((if member op = [Pbl,Met] p_
1.744 + then message2xml cI "thy-context not to calchead"
1.745 + else if pos = ([],Res) then message2xml cI "no thy-context at result"
1.746 + else let val cs as (ptp as (pt,_),_) = get_calc cI
1.747 + in if exist_lev_on' pt pos
1.748 + then let val pos' = lev_on' pt pos
1.749 + val tac = get_tac_checked pt pos'
1.750 + in if is_rewtac tac
1.751 + then contextthyOK2xml cI (context_thy (pt,pos) tac)
1.752 + else message2xml cI ("no thy-context at tac '" ^
1.753 + tac2str tac ^ "'")
1.754 + end
1.755 + else if is_curr_endof_calc pt pos
1.756 + then case step pos cs of
1.757 +(* val (str, (tacis, _, (pt,_))) = step pos cs;
1.758 + val ("ok", (tacis, _, (pt,_))) = step pos cs;
1.759 + *)
1.760 + ("ok", (tacis, _, (pt,_))) =>
1.761 + let val tac = fst3 (last_elem tacis)
1.762 + in if is_rewtac tac
1.763 + then contextthyOK2xml
1.764 + cI (context_thy ptp tac)
1.765 + else message2xml cI ("no thy-context at tac '" ^
1.766 + tac2str tac ^ "'")
1.767 + end
1.768 + | (msg, _) => message2xml cI msg
1.769 + else message2xml cI "no thy-context at this position"
1.770 + end)
1.771 + handle _ => sysERROR2xml cI "error in kernel")
1.772 +
1.773 +(* val (cI, Pbl_, pos as (p,p_)) = (1, Pbl_, ([],Pbl));
1.774 + *)
1.775 + | initContext cI Pbl_ (pos as (p,p_):pos') =
1.776 + ((let val ((pt,_),_) = get_calc cI
1.777 + val pp = par_pblobj pt p
1.778 + val chd = initcontext_pbl pt (pp,p_)
1.779 + in matchpbl2xml cI chd end)
1.780 + handle _ => sysERROR2xml cI "error in kernel")
1.781 +
1.782 + | initContext cI Met_ (pos as (p,p_):pos') =
1.783 + ((let val ((pt,_),_) = get_calc cI
1.784 + val pp = par_pblobj pt p
1.785 + val chd = initcontext_met pt (pp,p_)
1.786 + in matchmet2xml cI chd end)
1.787 + handle _ => sysERROR2xml cI "error in kernel");
1.788 +
1.789 +
1.790 +
1.791 +(*.match a theorem, a ruleset (etc., selected in the knowledge-browser)
1.792 +with the formula in the focus on the worksheet;
1.793 +string contains the thy, thus it is unique as thmID, rlsID for this thy;
1.794 +take the substitution from the istate of the formula.*)
1.795 +(* use"../smltest/Knowledge/poly.sml";
1.796 + val (cI, pos as (p,p_), guh) = (1, ([1,1,1], Frm),
1.797 + "thy_Poly-thm-real_diff_minus");
1.798 + val (cI, pos as (p,p_), guh) = (1, ([1,1], Frm), "norm_Poly");
1.799 + val (cI, pos as (p,p_), guh) =
1.800 + (1, ([1], Res), "thy_isac_Test-rls-Test_simplify");
1.801 + *)
1.802 +fun checkContext (cI:calcID) (pos:pos' as (p,p_)) (guh:guh) =
1.803 + (case (implode o (take_fromto 1 4) o explode) guh of
1.804 + "thy_" =>
1.805 + if member op = [Pbl,Met] p_
1.806 + then message2xml cI "thy-context not to calchead"
1.807 + else if pos = ([],Res) then message2xml cI "no thy-context at result"
1.808 + else if no_thycontext guh then message2xml cI ("no thy-context for '"^
1.809 + guh ^ "'")
1.810 + else let val (ptp as (pt,_),_) = get_calc cI
1.811 + val is = get_istate pt pos
1.812 + val subs = subs_from is "dummy" guh
1.813 + val tac = guh2rewtac guh subs
1.814 + in contextthyOK2xml cI (context_thy (pt, pos) tac) end
1.815 +
1.816 + (*.match the model of a problem at pos p
1.817 + with the model-pattern of the problem with pblID.*)
1.818 +(* val (cI, pos:pos' as (p,p_), guh) =
1.819 + (1, p, kestoreID2guh Pbl_ ["univariate","equation"]);
1.820 + val (cI, pos:pos' as (p,p_), guh) =
1.821 + (1, ([],Pbl), kestoreID2guh Pbl_ ["univariate","equation"]);
1.822 + val (cI, pos:pos' as (p,p_), guh) =
1.823 + (1, ([],Pbl), "pbl_equ_univ");
1.824 + *)
1.825 + | "pbl_" =>
1.826 + let val ((pt,_),_) = get_calc cI
1.827 + val pp = par_pblobj pt p
1.828 + val keID = guh2kestoreID guh
1.829 + val chd = context_pbl keID pt pp
1.830 + in matchpbl2xml cI chd end
1.831 +(* val (cI, pos:pos' as (p,p_), guh) =
1.832 + (1, ([],Pbl), kestoreID2guh Met_ ["LinEq", "solve_lineq_equation"]);
1.833 + *)
1.834 + | "met_" =>
1.835 + let val ((pt,_),_) = get_calc cI
1.836 + val pp = par_pblobj pt p
1.837 + val keID = guh2kestoreID guh
1.838 + val chd = context_met keID pt pp
1.839 + in matchmet2xml cI chd end)
1.840 + handle _ => sysERROR2xml cI "error in kernel";
1.841 +
1.842 +
1.843 +(*------------------------------------------------------------------*)
1.844 +end
1.845 +open interface;
1.846 +(*------------------------------------------------------------------*)