1.1 --- a/src/Tools/isac/FE-interface/interface.sml Wed Aug 25 15:15:01 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,843 +0,0 @@
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"FE-interface/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 IsacKnowledge/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/IsacKnowledge/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/IsacKnowledge/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 -(*------------------------------------------------------------------*)