1.1 --- a/src/Tools/isac/Frontend/interface.sml Thu Nov 17 16:40:27 2016 +0100
1.2 +++ b/src/Tools/isac/Frontend/interface.sml Mon Nov 21 12:47:02 2016 +0100
1.3 @@ -9,7 +9,7 @@
1.4 use"interface.sml";
1.5 *)
1.6
1.7 -signature MATH_ENGINE =
1.8 +signature KERNEL =
1.9 sig
1.10 val appendFormula : calcID -> cterm' -> XML.tree (*unit future*)
1.11 val autoCalculate : calcID -> auto -> XML.tree (*unit future*)
1.12 @@ -56,29 +56,27 @@
1.13 val setNextTactic : calcID -> tac -> XML.tree
1.14 val setProblem : calcID -> pblID -> XML.tree
1.15 val setTheory : calcID -> thyID -> XML.tree
1.16 -(*------------ for tests*)
1.17 -(*val encode: cterm' -> cterm' GONE TO xmlsrc/mathml.sml*)
1.18 -val encode_fmz: fmz -> fmz
1.19 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*
1.20 + (* NONE *)
1.21 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.22 end
1.23
1.24 -
1.25 -(*------------------------------------------------------------------*)
1.26 -structure Math_Engine : MATH_ENGINE =
1.27 +(**)
1.28 +structure Kernel(**): KERNEL(**) =
1.29 struct
1.30 -(*------------------------------------------------------------------*)
1.31 -
1.32 +(**)
1.33 (* encode "Isabelle"-strings as seen by the user to the
1.34 format accepted by Isabelle.
1.35 encode "^" ---> "^^^"; see Knowledge/Atools.thy;
1.36 called for each cterm', icalhd, fmz in this interface;
1.37 + see "fun en/decode" in xmlsrc/mathml.sml *)
1.38 fun encode_imodel (imodel:imodel) =
1.39 - let fun enc (Given ifos) = Given (map encode ifos)
1.40 - | enc (Find ifos) = Find (map encode ifos)
1.41 - | enc (Relate ifos) = Relate (map encode ifos)
1.42 - in map enc imodel:imodel end;
1.43 + let fun enc (Given ifos) = Given (map encode ifos)
1.44 + | enc (Find ifos) = Find (map encode ifos)
1.45 + | enc (Relate ifos) = Relate (map encode ifos)
1.46 + in map enc imodel:imodel end;
1.47 fun encode_icalhd ((pos', headl, imodel, pos_, spec):icalhd) =
1.48 - (pos', encode headl, encode_imodel imodel, pos_, spec):icalhd;
1.49 + (pos', encode headl, encode_imodel imodel, pos_, spec):icalhd;
1.50 fun encode_fmz ((ifos, spec) : fmz) = (map encode ifos, spec) : fmz;
1.51
1.52
1.53 @@ -92,58 +90,48 @@
1.54 all others are just calculated on the fly
1.55 TODO: adapt Iterator, add_user(= add_iterator!),etc. accordingly .*)
1.56 fun Iterator (cI:calcID) = (*returned ID unnecessary after WN.0411*)
1.57 - (adduserOK2xml cI (add_user (cI:calcID)))
1.58 - handle _ => sysERROR2xml cI "error in kernel 1";
1.59 + (adduserOK2xml cI (add_user (cI:calcID)))
1.60 + handle _ => sysERROR2xml cI "error in kernel 1";
1.61 fun IteratorTEST (cI:calcID) = add_user (cI:calcID);
1.62
1.63 (*.create a calc-tree; for calls from java: thus ^^^ decoded to ^;
1.64 compare "fun CalcTreeTEST" which does NOT decode.*)
1.65 fun CalcTree [(fmz, sp) : fmz] (*for several variants lateron*) =
1.66 - (let val cs = nxt_specify_init_calc (encode_fmz (fmz, sp))
1.67 - (*FIXME.WN.8.03: error-handling missing*)
1.68 - val cI = add_calc cs
1.69 - in calctreeOK2xml cI end)
1.70 - handle _ => sysERROR2xml 0 "error in kernel 2";
1.71 + ((let
1.72 + val cs = nxt_specify_init_calc (encode_fmz (fmz, sp))
1.73 + val cI = add_calc cs (*FIXME.WN.8.03: error-handling missing*)
1.74 + in calctreeOK2xml cI end)
1.75 + handle _ => sysERROR2xml 0 "error in kernel 2")
1.76 + | CalcTree [] = error "CalcTree: called with []"
1.77
1.78 -fun DEconstrCalcTree (cI:calcID) =
1.79 - deconstructcalctreeOK2xml (del_calc cI);
1.80 -
1.81 -
1.82 +fun DEconstrCalcTree (cI:calcID) = deconstructcalctreeOK2xml (del_calc cI);
1.83 fun getActiveFormula (cI:calcID) = iteratorOK2xml cI (get_pos cI 1);
1.84
1.85 fun moveActiveFormula (cI:calcID) (p:pos') =
1.86 - let val ((pt,_),_) = get_calc cI
1.87 - in if existpt' p pt then (upd_ipos cI 1 p; iteratorOK2xml cI p)
1.88 - else sysERROR2xml cI "frontend sends a non-existing pos" end;
1.89 + let val ((pt,_),_) = get_calc cI
1.90 + in
1.91 + if existpt' p pt
1.92 + then (upd_ipos cI 1 p; iteratorOK2xml cI p)
1.93 + else sysERROR2xml cI "frontend sends a non-existing pos"
1.94 + end
1.95
1.96 (*. set the next tactic to be applied: dont't change the calc-tree,
1.97 but remember the envisaged changes for fun autoCalculate;
1.98 compare force NextTactic .*)
1.99 -(* val (cI, tac) = (1, Add_Given "equality (x ^^^ 2 + 4 * x + 3 = 0)");
1.100 - val (cI, tac) = (1, Specify_Theory "PolyEq");
1.101 - val (cI, tac) = (1, Specify_Problem ["normalize","polynomial",
1.102 - "univariate","equation"]);
1.103 - val (cI, tac) = (1, Subproblem ("Poly",
1.104 - ["polynomial","univariate","equation"]));
1.105 - val (cI, tac) = (1, Model_Problem["linear","univariate","equation","test"]);
1.106 - val (cI, tac) = (1, Detail_Set "Test_simplify");
1.107 - val (cI, tac) = (1, Apply_Method ["Test", "solve_linear"]);
1.108 - val (cI, tac) = (1, Rewrite_Set "Test_simplify");
1.109 - *)
1.110 fun setNextTactic (cI:calcID) tac =
1.111 let
1.112 val ((pt, _), _) = get_calc cI (* retrieve calcstate from states *)
1.113 val ip = get_pos cI 1 (* retrieve position from states *)
1.114 - in case locatetac tac (pt, ip) of
1.115 - ("ok", (tacis, _, _)) => (* update calcstate in states *)
1.116 - (upd_calc cI ((pt, ip), tacis); setnexttactic2xml cI "ok")
1.117 - | ("unsafe-ok", (tacis, _, _)) =>
1.118 - (upd_calc cI ((pt, ip), tacis); setnexttactic2xml cI "unsafe-ok")
1.119 - | ("not-applicable",_) => setnexttactic2xml cI "not-applicable"
1.120 - | ("end-of-calculation",_) =>
1.121 - setnexttactic2xml cI "end-of-calculation"
1.122 - | ("failure",_) => sysERROR2xml cI "failure"
1.123 - end;
1.124 + in
1.125 + case locatetac tac (pt, ip) of
1.126 + ("ok", (tacis, _, _)) => (* update calcstate in states *)
1.127 + (upd_calc cI ((pt, ip), tacis); setnexttactic2xml cI "ok")
1.128 + | ("unsafe-ok", (tacis, _, _)) =>
1.129 + (upd_calc cI ((pt, ip), tacis); setnexttactic2xml cI "unsafe-ok")
1.130 + | ("not-applicable", _) => setnexttactic2xml cI "not-applicable"
1.131 + | ("end-of-calculation", _) => setnexttactic2xml cI "end-of-calculation"
1.132 + | (msg, _) => sysERROR2xml cI ("setNextTactic: locatetac returns " ^ msg)
1.133 + end;
1.134
1.135 (*. apply a tactic at a position and update the calc-tree if applicable .*)
1.136 (*WN080226 java-code is missing, errors smltest/Knowledge/polyminus.sml*)
1.137 @@ -153,174 +141,131 @@
1.138 val p = get_pos cI 1
1.139 in
1.140 case locatetac tac (pt, ip) of
1.141 - ("ok", (_, c, ptp as (_,p'))) =>
1.142 + ("ok", (_, c, ptp as (_, p'))) =>
1.143 (upd_calc cI (ptp, []);
1.144 upd_ipos cI 1 p';
1.145 autocalculateOK2xml cI p (if null c then p' else last_elem c) p')
1.146 - | ("unsafe-ok", (_, c, ptp as (_,p'))) =>
1.147 + | ("unsafe-ok", (_, c, ptp as (_, p'))) =>
1.148 (upd_calc cI (ptp, []);
1.149 upd_ipos cI 1 p';
1.150 autocalculateOK2xml cI p (if null c then p' else last_elem c) p')
1.151 - | ("end-of-calculation", (_, c, ptp as (_,p'))) =>
1.152 + | ("end-of-calculation", (_, c, ptp as (_, p'))) =>
1.153 (upd_calc cI (ptp, []);
1.154 upd_ipos cI 1 p';
1.155 autocalculateOK2xml cI p (if null c then p' else last_elem c) p')
1.156 - | (str,_) => autocalculateERROR2xml cI "failure"
1.157 + | (str, _) => autocalculateERROR2xml cI ("applyTactic: locatetac returns " ^ str)
1.158 end;
1.159
1.160 fun fetchProposedTactic (cI:calcID) =
1.161 - (case step (get_pos cI 1) (get_calc cI) of
1.162 - ("ok", (tacis, _, _)) =>
1.163 - let val _= upd_tacis cI tacis
1.164 - val (tac,_,_) = last_elem tacis
1.165 - in fetchproposedtacticOK2xml cI tac (fetchErrorpatterns tac) end
1.166 - | ("helpless",_) => fetchproposedtacticERROR2xml cI "helpless"
1.167 - | ("no-fmz-spec",_) => fetchproposedtacticERROR2xml cI "no-fmz-spec"
1.168 - | ("end-of-calculation",_) =>
1.169 - fetchproposedtacticERROR2xml cI "end-of-calculation")
1.170 - handle _ => sysERROR2xml cI "error in kernel 3";
1.171 -
1.172 -(*original see ~~/src/Tools/isac/Interpret/solve.sml:
1.173 - datatype auto = FIXXXME040624: does NOT match interfaces/ITOCalc.java
1.174 - Step of int (*1 do #int steps (may stop in model/specify)
1.175 - IS VERY INEFFICIENT IN MODEL/SPECIY*)
1.176 -| CompleteModel (*2 complete modeling
1.177 - if model complete, finish specifying*)
1.178 -| CompleteCalcHead (*3 complete model/specify in one go*)
1.179 -| CompleteToSubpbl (*4 stop at the next begin of a subproblem,
1.180 - if none, complete the actual (sub)problem*)
1.181 -| CompleteSubpbl (*5 complete the actual (sub)problem (incl.ev.subproblems)*)
1.182 -| CompleteCalc; (*6 complete the calculation as a whole*)*)
1.183 + (case step (get_pos cI 1) (get_calc cI) of
1.184 + ("ok", (tacis, _, _)) =>
1.185 + let
1.186 + val _= upd_tacis cI tacis
1.187 + val (tac, _, _) = last_elem tacis
1.188 + in fetchproposedtacticOK2xml cI tac (fetchErrorpatterns tac) end
1.189 + | ("helpless", _) => fetchproposedtacticERROR2xml cI "helpless"
1.190 + | ("no-fmz-spec", _) => fetchproposedtacticERROR2xml cI "no-fmz-spec"
1.191 + | ("end-of-calculation", _) =>
1.192 + fetchproposedtacticERROR2xml cI "end-of-calculation")
1.193 + handle _ => sysERROR2xml cI "error in kernel 3";
1.194
1.195 fun autoCalculate (cI:calcID) auto = (*Future.fork
1.196 - (fn () => (( *)let
1.197 - val pold = get_pos cI 1
1.198 - val x = autocalc [] pold (get_calc cI) auto
1.199 - in
1.200 - case x of
1.201 - ("ok", c, ptp as (_,p)) =>
1.202 - (upd_calc cI (ptp, []); upd_ipos cI 1 p;
1.203 - autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)
1.204 - | ("end-of-calculation", c, ptp as (_,p)) =>
1.205 - (upd_calc cI (ptp, []); upd_ipos cI 1 p;
1.206 - autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)
1.207 - | (str, _, _) => autocalculateERROR2xml cI str
1.208 - end (* ) *)
1.209 - handle ERROR msg => sysERROR2xml cI ("error in kernel 4: " ^ msg)(* )) *);
1.210 + (fn () => (( *)let
1.211 + val pold = get_pos cI 1
1.212 + val x = autocalc [] pold (get_calc cI) auto
1.213 + in
1.214 + case x of
1.215 + ("ok", c, ptp as (_,p)) =>
1.216 + (upd_calc cI (ptp, []); upd_ipos cI 1 p;
1.217 + autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)
1.218 + | ("end-of-calculation", c, ptp as (_,p)) =>
1.219 + (upd_calc cI (ptp, []); upd_ipos cI 1 p;
1.220 + autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)
1.221 + | (str, _, _) => autocalculateERROR2xml cI str
1.222 + end (* ) *)
1.223 + handle ERROR msg => sysERROR2xml cI ("error in kernel 4: " ^ msg)(* )) *);
1.224
1.225 -
1.226 -(* val (cI:calcID, ichd as ((p,_),_,_,_,_):icalhd) =
1.227 - (1, (([],Pbl), "not used here",
1.228 - [Given ["fixedValues [r=Arbfix]"],
1.229 - Find ["maximum A", "valuesFor [a,b]"(*new input*)],
1.230 - Relate ["relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]"]], Pbl,
1.231 - ("DiffApp", ["maximum_of","function"],
1.232 - ["DiffApp","max_by_calculus"])));
1.233 - val (cI:calcID, ichd as ((p,_),_,_,_,_):icalhd) =
1.234 - (1, (([],Pbl),"solve (x+1=2, x)",
1.235 - [Given ["equality (x+1=2)", "solveFor x"],
1.236 - Find ["solutions L"]],
1.237 - Pbl,
1.238 - ("Test", ["linear","univariate","equation","test"],
1.239 - ["Test","solve_linear"])));
1.240 - val (cI:calcID, ichd as ((p,_),_,_,_,_):icalhd) =
1.241 - (1, (([],Pbl),"solveTest (1+-1*2+x=0,x)", [], Pbl, ("", [], [])));
1.242 - val (cI, p:pos')=(1, ([1],Frm));
1.243 - val (cI, p:pos')=(1, ([1,2,1,3],Res));
1.244 - *)
1.245 fun getTactic cI (p:pos') =
1.246 - (let val ((pt,_),_) = get_calc cI
1.247 - val (form, tac, asms) = pt_extract (pt, p)
1.248 - in case tac of
1.249 - SOME ta => gettacticOK2xml cI ta
1.250 - | NONE => gettacticERROR2xml cI ("no tactic at position " ^ pos'2str p)
1.251 - end)
1.252 + (let
1.253 + val ((pt, _), _) = get_calc cI
1.254 + val (_, tac, _) = pt_extract (pt, p)
1.255 + in
1.256 + case tac of
1.257 + SOME ta => gettacticOK2xml cI ta
1.258 + | NONE => gettacticERROR2xml cI ("no tactic at position " ^ pos'2str p)
1.259 + end)
1.260 handle _ => sysERROR2xml cI "syserror in getTactic";
1.261
1.262 -(*. see ICalcIterator#fetchApplicableTactics
1.263 - @see #TACTICS_ALL
1.264 - @see #TACTICS_CURRENT_THEORY
1.265 - @see #TACTICS_CURRENT_METHOD ..the only impl.WN040307.*)
1.266 -(*. fetch tactics to be applied to a particular step.*)
1.267 -(* WN071231 kept this version for later parametrisation*)
1.268 -(*.version 1: fetch _all_ tactics from script .*)
1.269 -(* WN120611 took version 1 again -------------------------vvv
1.270 - version 2: fetch _applicable_ _elementary_ (ie. recursively
1.271 - decompose rule-sets) Rewrite*, Calculate
1.272 -fun fetchApplicableTactics cI (scope:int) (p:pos') =
1.273 - (let val ((pt, _), _) = get_calc cI
1.274 - in (applicabletacticsOK cI (sel_appl_atomic_tacs pt p))
1.275 - handle PTREE str => sysERROR2xml cI str
1.276 - end)
1.277 - handle _ => sysERROR2xml cI "error in kernel 5";
1.278 +(* Fetch tactics to be applied to a particular step.
1.279 + Requirements are not yet implemented, see ICalcIterator#fetchApplicableTactics"
1.280 + @see #TACTICS_ALL
1.281 + @see #TACTICS_CURRENT_THEORY
1.282 + @see #TACTICS_CURRENT_METHOD ..the only impl.WN040307
1.283 + Lucin.sel_appl_atomic_tacs waits to be used here
1.284 *)
1.285 -fun fetchApplicableTactics cI (scope:int) (p:pos') = (*---^^^*)
1.286 - (let val ((pt, _), _) = get_calc cI
1.287 - in (applicabletacticsOK cI (Lucin.sel_rules pt p))
1.288 - handle PTREE str => sysERROR2xml cI str
1.289 - end)
1.290 +fun fetchApplicableTactics cI (_(*scope*): int) (p : pos') =
1.291 + (let val ((pt, _), _) = get_calc cI
1.292 + in (applicabletacticsOK cI (Lucin.sel_rules pt p))
1.293 + handle PTREE str => sysERROR2xml cI str
1.294 + end)
1.295 handle _ => sysERROR2xml cI "error in kernel 5";
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 + (let
1.303 + val ((pt, _), _) = get_calc cI
1.304 + val (_, _, asms) = pt_extract (pt, p)
1.305 + in getasmsOK2xml cI asms end)
1.306 + handle _ => sysERROR2xml cI "syserror in getAssumptions"
1.307
1.308 (*WN0502 @see ME/ctree: type asms: illdesigned, thus no positions returned*)
1.309 fun getAccumulatedAsms cI (p:pos') =
1.310 - (let val ((pt, _), _) = get_calc cI
1.311 - val ass = get_assumptions_ pt p
1.312 - in (*getaccuasmsOK2xml cI (get_assumptions_ pt p)*)
1.313 - getasmsOK2xml cI ass end)
1.314 - handle _ => sysERROR2xml cI "syserror in getAccumulatedAsms";
1.315 + (let
1.316 + val ((pt, _), _) = get_calc cI
1.317 + val ass = get_assumptions_ pt p
1.318 + in getasmsOK2xml cI ass end)
1.319 + handle _ => sysERROR2xml cI "syserror in getAccumulatedAsms"
1.320
1.321 -(*since moveActive* does NOT transfer pos java --> sml (only sml --> java)
1.322 - refFormula might become involved in far-off errors !!!*)
1.323 -fun refFormula cI (p: pos') = (*WN0501 rename to 'fun getElement' !*)
1.324 +fun refFormula cI (p: pos') = (*WN0501 rename to "fun getElement" !*)
1.325 (let
1.326 val ((pt, _), _) = get_calc cI
1.327 val (form, _, _) = pt_extract (pt, p)
1.328 in refformulaOK2xml cI p form end)
1.329 - handle _ =>
1.330 - sysERROR2xml cI ("error in kernel 6: refFormula " ^ int2str cI ^
1.331 - " " ^ pos'2str p);
1.332 + handle _ => sysERROR2xml cI ("error in kernel 6: refFormula " ^ int2str cI ^ " " ^ pos'2str p)
1.333
1.334 -(*.get formulae 'from' 'to' w.r.t. ordering in Position#compareTo(Position p);
1.335 - in case of CalcHeads only the headline is taken
1.336 - (the pos' allows distinction between PrfObj and PblObj anyway);
1.337 - 'level' is adjusted such that an 'interval' of formulae is returned;
1.338 - 'from' 'to' are designed for use by iterators of calcChangedEvent;
1.339 - thus 'from' is the last unchanged position.*)
1.340 -fun getFormulaeFromTo cI (from as ([],Pbl):pos') (to as ([],Pbl):pos')_ false =
1.341 - (*special case because 'from' is _before_ the first elements to be returned*)
1.342 +(* get formulae "from" "to" w.r.t. ordering in Position#compareTo(Position p);
1.343 + "level" is adjusted such that an "interval" of formulae is returned;
1.344 + "from" "to" are designed for use by iterators of calcChangedEvent,
1.345 + thus "from" is the last unchanged position *)
1.346 +fun getFormulaeFromTo cI (([], Pbl) : pos') (to as ([], Pbl) : pos') _ false =
1.347 ((let
1.348 - val ((pt,_),_) = get_calc cI
1.349 - val (ModSpec (_,_,headline,_,_,_),_,_) = pt_extract (pt, to)
1.350 - in getintervalOK cI [(to, headline)] end)
1.351 - handle _ => sysERROR2xml cI "error in kernel 7")
1.352 - | getFormulaeFromTo cI (from as ([],Pbl):pos') (to as ([],Met):pos')_ false =
1.353 - getFormulaeFromTo cI ([],Pbl) ([],Pbl) (~00000) false
1.354 - | getFormulaeFromTo cI (from:pos') (to:pos') level false =
1.355 - (if from = to then sysERROR2xml cI "getFormulaeFromTo: From = To"
1.356 - else
1.357 - (case from of
1.358 - ([],Res) => sysERROR2xml cI ("getFormulaeFromTo does: moveDown " ^
1.359 - "from=([],Res) .. goes beyond result")
1.360 - | _ =>
1.361 - let val ((pt,_),_) = get_calc cI
1.362 - val f = move_dn [] pt from
1.363 - fun max (a,b) = if a < b then b else a
1.364 - (*must reach margins ...*)
1.365 - val lev = max (level, max (lev_of from, lev_of to))
1.366 - in getintervalOK cI (get_interval f to lev pt) end)
1.367 + val ((pt,_),_) = get_calc cI
1.368 + val (ModSpec (_, _, headline, _, _, _), _, _) = pt_extract (pt, to)
1.369 + in getintervalOK cI [(to, headline)] end)
1.370 + handle _ => sysERROR2xml cI "error in kernel 7")
1.371 + | getFormulaeFromTo cI ([], Pbl) ([], Met) _ false =
1.372 + getFormulaeFromTo cI ([], Pbl) ([], Pbl) (~00000) false
1.373 + (* ^^^ separated cases, because "from" is _before_ the first elements to be returned*)
1.374 + | getFormulaeFromTo cI from to level false =
1.375 + (if from = to
1.376 + then sysERROR2xml cI "getFormulaeFromTo: From = To"
1.377 + else
1.378 + (case from of
1.379 + ([], Res) => sysERROR2xml cI ("getFormulaeFromTo does: moveDown " ^
1.380 + "from=([],Res) .. goes beyond result")
1.381 + | _ =>
1.382 + let
1.383 + val ((pt,_),_) = get_calc cI
1.384 + val f = move_dn [] pt from
1.385 + fun max (a,b) = if a < b then b else a
1.386 + val lev = max (level, max (lev_of from, lev_of to)) (*... must reach margins *)
1.387 + in getintervalOK cI (get_interval f to lev pt) end)
1.388 handle _ => sysERROR2xml cI "error in getFormulaeFromTo")
1.389 | getFormulaeFromTo cI from to level true =
1.390 sysERROR2xml cI ("getFormulaeFromTo impl.for formulae only, " ^
1.391 "i.e. last arg only impl. for false, _NOT_ true");
1.392
1.393 fun interSteps cI ip =
1.394 - (let val ((pt,p), tacis) = get_calc cI
1.395 + (let val ((pt, p), tacis) = get_calc cI
1.396 in
1.397 if (not o is_interpos) ip
1.398 then interStepsERROR cI ("only formulae with position (_,Res) " ^
1.399 @@ -328,137 +273,126 @@
1.400 else
1.401 let val ip' = lev_pred' pt ip
1.402 in case detailstep pt ip of
1.403 - ("detailrls", pt, lastpos) => (upd_calc cI ((pt, p), tacis);
1.404 - interStepsOK cI ip' ip' lastpos)
1.405 - | ("no-Rewrite_Set...", _, _) => sysERROR2xml cI "no Rewrite_Set..."
1.406 - | (_, _, lastpos) => interStepsOK cI ip' ip' lastpos
1.407 + ("detailrls", pt, lastpos) =>
1.408 + (upd_calc cI ((pt, p), tacis); interStepsOK cI ip' ip' lastpos)
1.409 + | ("no-Rewrite_Set...", _, _) => sysERROR2xml cI "no Rewrite_Set..."
1.410 + | (_, _, lastpos) => interStepsOK cI ip' ip' lastpos
1.411 end
1.412 end)
1.413 - handle _ => sysERROR2xml cI "error in kernel 8";
1.414 + handle _ => sysERROR2xml cI "error in kernel 8";
1.415
1.416 -fun modifyCalcHead (cI:calcID) (ichd as ((p,_),_,_,_,_):icalhd) =
1.417 - (let val ((pt,_),_) = get_calc cI
1.418 - val (pt, chd as (_,p_,_,_,_,_)) = input_icalhd pt ichd
1.419 - in (upd_calc cI ((pt, (p,p_)), []);
1.420 - modifycalcheadOK2xml cI chd) end)
1.421 +fun modifyCalcHead cI (ichd as ((p,_),_,_,_,_):icalhd) =
1.422 + (let
1.423 + val ((pt,_),_) = get_calc cI
1.424 + val (pt, chd as (_,p_,_,_,_,_)) = input_icalhd pt ichd
1.425 + in (upd_calc cI ((pt, (p,p_)), []); modifycalcheadOK2xml cI chd) end)
1.426 handle _ => sysERROR2xml cI "error in kernel 9";
1.427
1.428 -(*.at the activeFormula set the Model, the Guard and the Specification
1.429 - to empty and return a CalcHead;
1.430 - the 'origin' remains (for reconstructing all that).*)
1.431 -fun resetCalcHead (cI:calcID) =
1.432 - (let val (ptp,_) = get_calc cI
1.433 - val ptp = reset_calchead ptp
1.434 - in (upd_calc cI (ptp, []);
1.435 - modifycalcheadOK2xml cI (get_ocalhd ptp)) end)
1.436 +(* at the activeFormula set the Model, the Guard and the Specification to empty
1.437 + and return a CalcHead; the 'origin' remains (for reconstructing all that) *)
1.438 +fun resetCalcHead cI =
1.439 + (let
1.440 + val (ptp,_) = get_calc cI
1.441 + val ptp = reset_calchead ptp
1.442 + in (upd_calc cI (ptp, []); modifycalcheadOK2xml cI (get_ocalhd ptp)) end)
1.443 handle _ => sysERROR2xml cI "error in kernel 10";
1.444
1.445 -(*.at the activeFormula insert all the Descriptions in the Model
1.446 - (_not_ in the Guard) and return a CalcHead;
1.447 - the Descriptions are for user-guidance; the rest of the items
1.448 - are left empty for user-input;
1.449 - includes a resetCalcHead for the Model and the Guard.*)
1.450 -fun modelProblem (cI:calcID) =
1.451 - (let val (ptp, _) = get_calc cI
1.452 - val ptp = reset_calchead ptp
1.453 - val (_, _, ptp) = nxt_specif Model_Problem ptp
1.454 - in (upd_calc cI (ptp, []);
1.455 - modifycalcheadOK2xml cI (get_ocalhd ptp)) end)
1.456 +(* at the activeFormula insert all the Descriptions in the Model and return a CalcHead;
1.457 + the Descriptions are for user-guidance; the rest of the items are left empty for user-input *)
1.458 +fun modelProblem cI =
1.459 + (let val (ptp, _) = get_calc cI
1.460 + val ptp = reset_calchead ptp
1.461 + val (_, _, ptp) = nxt_specif Model_Problem ptp
1.462 + in (upd_calc cI (ptp, []); modifycalcheadOK2xml cI (get_ocalhd ptp)) end)
1.463 handle _ => sysERROR2xml cI "error in kernel 11";
1.464
1.465 -
1.466 (* set the UContext determined on a knowledgebrowser to the current calc
1.467 WN0825: not implemented in isac-java.
1.468 - This is indicated by the absence of use-cases in isac-docu.ps.gz
1.469 - and of JUnit tests in isac-java/../java-tests/.
1.470 -
1.471 Recalling the state of development after summer-term 2006 (Robert Koenishofer et.al.):
1.472 - Main success was showing UCntext from Worksheet to the Example/Method/Problem/TheoryBrowser,
1.473 + Main success was showing UContext from Worksheet to the Example/Method/Problem/TheoryBrowser,
1.474 while the buttons on these browsers <To Worksheet> <Try Refine> have no
1.475 code in isac-java (and only partial, untested code in isabisac).
1.476 *)
1.477 -fun setContext (cI:calcID) (ip as (_,p_):pos') (guh:guh) =
1.478 +fun setContext cI (ip as (_,p_):pos') (guh:guh) =
1.479 case (implode o (take_fromto 1 4) o Symbol.explode) guh of
1.480 - "thy_" =>
1.481 - if member op = [Pbl,Met] p_
1.482 - then message2xml cI "thy-context not to calchead"
1.483 - else if ip = ([],Res) then message2xml cI "no thy-context at result"
1.484 - else if no_thycontext guh then message2xml cI ("no thy-context for '" ^ guh ^ "'")
1.485 - else
1.486 - ((let
1.487 - val (ptp as (pt, pold), _) = get_calc cI
1.488 - val is = get_istate pt ip
1.489 - val subs = subs_from is "dummy" guh
1.490 - val tac = guh2rewtac guh subs
1.491 - in
1.492 - case locatetac tac (pt, ip) of (*='fun setNextTactic'+step*)
1.493 - ("ok", (tacis, c, ptp as (_,p))) =>
1.494 - (upd_calc cI ((pt,p), []);
1.495 - autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)
1.496 - | ("unsafe-ok", (tacis, c, ptp as (_,p))) =>
1.497 - (upd_calc cI ((pt,p), []);
1.498 - autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)
1.499 - | ("end-of-calculation",_) => message2xml cI "end-of-calculation"
1.500 - | ("failure",_) => sysERROR2xml cI "failure"
1.501 - | ("not-applicable",_) => (*the rule comes from anywhere..*)
1.502 - (case applicable_in ip pt tac of
1.503 - Notappl e => message2xml cI ("'" ^ tac2str tac ^ "' not-applicable")
1.504 - | Appl m =>
1.505 - let
1.506 - val ctxt = get_ctxt pt pold
1.507 - val (p,c,_,pt) =
1.508 - generate1 (assoc_thy "Isac") m (Uistate, ctxt) ip pt
1.509 - in upd_calc cI ((pt,p),[]);
1.510 + "thy_" =>
1.511 + if member op = [Pbl, Met] p_
1.512 + then message2xml cI "thy-context not to calchead"
1.513 + else if ip = ([], Res) then message2xml cI "no thy-context at result"
1.514 + else if no_thycontext guh then message2xml cI ("no thy-context for '" ^ guh ^ "'")
1.515 + else
1.516 + ((let
1.517 + val (ptp as (pt, pold), _) = get_calc cI
1.518 + val is = get_istate pt ip
1.519 + val subs = subs_from is "dummy" guh
1.520 + val tac = guh2rewtac guh subs
1.521 + in
1.522 + case locatetac tac (pt, ip) of (*='fun setNextTactic'+step*)
1.523 + ("ok", (tacis, c, ptp as (_, p))) =>
1.524 + (upd_calc cI ((pt, p), []);
1.525 + autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)
1.526 + | ("unsafe-ok", (tacis, c, ptp as (_ ,p))) =>
1.527 + (upd_calc cI ((pt, p), []);
1.528 + autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)
1.529 + | ("end-of-calculation", _) => message2xml cI "end-of-calculation"
1.530 + | ("failure", _) => sysERROR2xml cI "failure"
1.531 + | ("not-applicable", _) => (*the rule comes from anywhere..*)
1.532 + (case applicable_in ip pt tac of
1.533 + Notappl e => message2xml cI ("'" ^ tac2str tac ^ "' not-applicable")
1.534 + | Appl m =>
1.535 + let
1.536 + val ctxt = get_ctxt pt pold
1.537 + val (p, c, _, pt) =
1.538 + generate1 (assoc_thy "Isac") m (Uistate, ctxt) ip pt
1.539 + in upd_calc cI ((pt, p), []);
1.540 autocalculateOK2xml cI pold (if null c then pold else last_elem c) p
1.541 - end)
1.542 - end
1.543 - ) handle _ => sysERROR2xml cI "setContext: thy_ ???")
1.544 - | "pbl_" =>
1.545 - ((let
1.546 - val pI = guh2kestoreID guh
1.547 - val ((pt, _), _) = get_calc cI
1.548 - in
1.549 - if member op = [Pbl, Met] p_
1.550 - then
1.551 - let val (pt, chd) = set_problem pI (pt, ip)
1.552 - in (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end
1.553 - else sysERROR2xml cI "setContext for pbl requires ActiveFormula on CalcHead"
1.554 - end
1.555 - )handle _ => sysERROR2xml cI "setContext: pbl_ ???")
1.556 - | "met_" =>
1.557 - ((let
1.558 - val mI = guh2kestoreID guh
1.559 - val ((pt, _), _) = get_calc cI
1.560 - in
1.561 - if member op = [Pbl, Met] p_
1.562 - then
1.563 - let val (pt, chd) = set_method mI (pt, ip)
1.564 - in (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end
1.565 - else sysERROR2xml cI "setContext for met requires ActiveFormula on CalcHead"
1.566 - end
1.567 - )handle _ => sysERROR2xml cI "setContext: met_ ???")
1.568 + end)
1.569 + end
1.570 + ) handle _ => sysERROR2xml cI "setContext: thy_ ???")
1.571 + | "pbl_" =>
1.572 + ((let
1.573 + val pI = guh2kestoreID guh
1.574 + val ((pt, _), _) = get_calc cI
1.575 + in
1.576 + if member op = [Pbl, Met] p_
1.577 + then
1.578 + let val (pt, chd) = set_problem pI (pt, ip)
1.579 + in (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end
1.580 + else sysERROR2xml cI "setContext for pbl requires ActiveFormula on CalcHead"
1.581 + end
1.582 + ) handle _ => sysERROR2xml cI "setContext: pbl_ ???")
1.583 + | "met_" =>
1.584 + ((let
1.585 + val mI = guh2kestoreID guh
1.586 + val ((pt, _), _) = get_calc cI
1.587 + in
1.588 + if member op = [Pbl, Met] p_
1.589 + then
1.590 + let val (pt, chd) = set_method mI (pt, ip)
1.591 + in (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end
1.592 + else sysERROR2xml cI "setContext for met requires ActiveFormula on CalcHead"
1.593 + end
1.594 + ) handle _ => sysERROR2xml cI "setContext: met_ ???")
1.595
1.596
1.597 -(*.specify the Method at the activeFormula and return a CalcHead
1.598 - containing the Guard.
1.599 - WN0512 impl.incomplete, see 'nxt_specif (Specify_Method '.*)
1.600 -fun setMethod (cI:calcID) (mI:metID) =
1.601 +(* specify the Method at the activeFormula and return a CalcHead containing the Guard.
1.602 + WN0512 impl.incomplete, see "nxt_specif (Specify_Method" *)
1.603 +fun setMethod cI mI =
1.604 (let
1.605 val ((pt, _), _) = get_calc cI
1.606 val ip as (_, p_) = get_pos cI 1
1.607 - in
1.608 - if member op = [Pbl,Met] p_
1.609 - then
1.610 - let val (pt, chd) = set_method mI (pt, ip)
1.611 - in (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end
1.612 - else sysERROR2xml cI "setMethod requires ActiveFormula on CalcHead"
1.613 - end
1.614 - ) handle _ => sysERROR2xml cI "error in kernel 12";
1.615 + in
1.616 + if member op = [Pbl,Met] p_
1.617 + then
1.618 + let val (pt, chd) = set_method mI (pt, ip)
1.619 + in (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end
1.620 + else sysERROR2xml cI "setMethod requires ActiveFormula on CalcHead"
1.621 + end
1.622 + ) handle _ => sysERROR2xml cI "error in kernel 12";
1.623
1.624 -(*.specify the Problem at the activeFormula and return a CalcHead
1.625 - containing the Model; special case of checkContext;
1.626 - WN0512 impl.incomplete, see 'nxt_specif (Specify_Problem '.*)
1.627 -fun setProblem (cI:calcID) (pI:pblID) =
1.628 +(* specify the Problem at the activeFormula and return a CalcHead containing the Model;
1.629 + special case of checkContext; WN0512 impl.incomplete, see "nxt_specif (Specify_Problem" *)
1.630 +fun setProblem cI pI =
1.631 (let
1.632 val ((pt, _), _) = get_calc cI
1.633 val ip as (_, p_) = get_pos cI 1
1.634 @@ -471,77 +405,62 @@
1.635 end
1.636 ) handle _ => sysERROR2xml cI "error in kernel 13";
1.637
1.638 -(*.specify the Theory at the activeFormula and return a CalcHead;
1.639 - special case of checkContext;
1.640 - WN0512 impl.incomplete, see 'nxt_specif (Specify_Method '.*)
1.641 -fun setTheory (cI:calcID) (tI:thyID) =
1.642 +(* specify the Theory at the activeFormula and return a CalcHead;
1.643 + special case of checkContext; WN0512 impl.incomplete, see "nxt_specif (Specify_Method" *)
1.644 +fun setTheory cI tI =
1.645 (let
1.646 val ((pt, _), _) = get_calc cI
1.647 val ip as (_, p_) = get_pos cI 1
1.648 - in
1.649 - if member op = [Pbl,Met] p_
1.650 - then
1.651 - let val (pt, chd) = set_theory tI (pt, ip)
1.652 - in (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end
1.653 - else sysERROR2xml cI "setProblem requires ActiveFormula on CalcHead"
1.654 + in
1.655 + if member op = [Pbl,Met] p_
1.656 + then
1.657 + let val (pt, chd) = set_theory tI (pt, ip)
1.658 + in (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end
1.659 + else sysERROR2xml cI "setProblem requires ActiveFormula on CalcHead"
1.660 end
1.661 ) handle _ => sysERROR2xml cI "error in kernel 14";
1.662
1.663 -
1.664 -(**. without update of CalcTree .**)
1.665 -
1.666 -(*.match the model of a problem at pos p
1.667 - with the model-pattern of the problem with pblID*)
1.668 -(*fun tryMatchProblem cI pblID =
1.669 - (let val ((pt,_),_) = get_calc cI
1.670 - val p = get_pos cI 1
1.671 - val chd = trymatch pblID pt p
1.672 - in trymatchOK2xml cI chd end)
1.673 - handle _ => sysERROR2xml cI "error in kernel 15";*)
1.674 -
1.675 -(*.refinement for the parent-problem of the position.*)
1.676 -(* Not used in isac-java (see comment WN0825 for setContext),
1.677 - but tryrefine is used within isabisac.
1.678 -*)
1.679 -fun refineProblem cI ((p,p_) : pos') (guh : guh) =
1.680 - (let val pblID = guh2kestoreID guh
1.681 - val ((pt,_),_) = get_calc cI
1.682 - val pp = par_pblobj pt p
1.683 - val chd = tryrefine pblID pt (pp, p_)
1.684 - in contextpblOK2xml cI chd end)
1.685 +(* refinement for the parent-problem of the position,
1.686 + Not used in isac-java (see comment WN0825 for setContext) but tryrefine is used within isabisac *)
1.687 +fun refineProblem cI (p, p_) guh =
1.688 + (let
1.689 + val pblID = guh2kestoreID guh
1.690 + val ((pt,_),_) = get_calc cI
1.691 + val pp = par_pblobj pt p
1.692 + val chd = tryrefine pblID pt (pp, p_)
1.693 + in contextpblOK2xml cI chd end)
1.694 handle _ => sysERROR2xml cI "error in kernel 16";
1.695
1.696 (* append a formula to the calculation *)
1.697 fun appendFormula' cI (ifo:cterm') =
1.698 (let
1.699 val cs = get_calc cI
1.700 - val pos as (_,p_) = get_pos cI 1
1.701 + val pos = get_pos cI 1
1.702 in
1.703 case step pos cs of
1.704 ("ok", cs') =>
1.705 (case inform cs' (encode ifo) of
1.706 - ("ok", (_(*use in DG !!!*), c, ptp as (_,p))) =>
1.707 + ("ok", (_(*use in DG !!!*), c, ptp as (_, p))) =>
1.708 (upd_calc cI (ptp, []); upd_ipos cI 1 p;
1.709 appendformulaOK2xml cI pos (if null c then pos else last_elem c) p)
1.710 - | ("same-formula", (_, c, ptp as (_,p))) =>
1.711 + | ("same-formula", (_, c, ptp as (_, p))) =>
1.712 (upd_calc cI (ptp, []); upd_ipos cI 1 p;
1.713 appendformulaOK2xml cI pos (if null c then pos else last_elem c) p)
1.714 | (msg, _) => appendformulaERROR2xml cI msg)
1.715 - | (msg, cs') => appendformulaERROR2xml cI msg
1.716 + | (msg, _) => appendformulaERROR2xml cI msg
1.717 end)
1.718 handle ERROR msg => sysERROR2xml cI ("error in kernel 17: " ^ msg);
1.719
1.720 fun appendFormula cI ifo = (*Future.fork (fn () => *)appendFormula' cI ifo(* ) *);
1.721
1.722 -(* replace a formula with_in_ a calculation;
1.723 - this situation applies for initial CAS-commands, too *)
1.724 +(* replace a formula with_in_ a calculation; this applies for initial CAS-commands, too *)
1.725 fun replaceFormula cI (ifo:cterm') =
1.726 - (let
1.727 + (let
1.728 val ((pt, _), _) = get_calc cI
1.729 val p = get_pos cI 1
1.730 in
1.731 case inform (([], [], (pt, p)): calcstate') (encode ifo) of
1.732 - ("ok", (_(*tacs used for DG ?*), c, ptp' as (pt',p'))) =>
1.733 + ("ok", (_(*tacs used for DG ?*), c, ptp' as (_, p'))) =>
1.734 let
1.735 val unc = if null (fst p) then p else move_up [] pt p
1.736 val _ = upd_calc cI (ptp', [])
1.737 @@ -552,115 +471,98 @@
1.738 end)
1.739 handle _ => sysERROR2xml cI "error in kernel 18";
1.740
1.741 -
1.742 -
1.743 -(***. CalcIterator
1.744 +(*** CalcIterator
1.745 moveActive*: set the pos' of the active formula stored with the calctree
1.746 could take pos' as argument for consistency checks
1.747 move*: compute the new iterator from the old one on the fly
1.748 -
1.749 -.***)
1.750 +***)
1.751
1.752 fun moveActiveRoot cI =
1.753 - (let val _ = upd_ipos cI 1 ([],Pbl)
1.754 - in iteratorOK2xml cI ([],Pbl) end)
1.755 - handle e => sysERROR2xml cI "error in kernel 19";
1.756 + (let val _ = upd_ipos cI 1 ([], Pbl)
1.757 + in iteratorOK2xml cI ([], Pbl) end)
1.758 + handle _ => sysERROR2xml cI "error in kernel 19"
1.759 fun moveRoot cI =
1.760 - (iteratorOK2xml cI ([],Pbl))
1.761 - handle e => sysERROR2xml cI "";
1.762 + (iteratorOK2xml cI ([], Pbl))
1.763 + handle _ => sysERROR2xml cI "";
1.764 fun moveActiveRootTEST cI =
1.765 - (let val _ = upd_ipos cI 1 ([],Pbl)
1.766 - in iteratorOK2xml cI ([],Pbl) end)
1.767 - handle e => sysERROR2xml cI "error in kernel 20";
1.768 + (let val _ = upd_ipos cI 1 ([], Pbl)
1.769 + in iteratorOK2xml cI ([], Pbl) end)
1.770 + handle _ => sysERROR2xml cI "error in kernel 20"
1.771
1.772 -(* val (cI, uI) = (1,1);
1.773 - val (cI, uI) = (1,2);
1.774 - *)
1.775 fun moveActiveDown cI =
1.776 - ((let val ((pt,_),_) = get_calc cI
1.777 -(* val (P, (Nd (_, ns)), (p::(ps as (_::_)), p_)) =([]:pos, pt, get_pos cI uI);
1.778 - val (P, (Nd (c, ns)), ([p], p_)) =([]:pos, pt, get_pos cI uI);
1.779 -
1.780 - print_depth 7;pt
1.781 - *)
1.782 + ((let
1.783 + val ((pt, _), _) = get_calc cI
1.784 val ip' = move_dn [] pt (get_pos cI 1)
1.785 val _ = upd_ipos cI 1 ip'
1.786 - in iteratorOK2xml cI ip' end)
1.787 - handle (PTREE e) => iteratorERROR2xml cI)
1.788 - handle _ => sysERROR2xml cI "error in kernel 21";
1.789 -fun moveDown cI (p:pos') =
1.790 - ((let val ((pt,_),_) = get_calc cI
1.791 -(* val (P, (Nd (_, ns)), (p::(ps as (_::_)), p_)) =([]:pos, pt, get_pos cI uI);
1.792 - val (P, (Nd (c, ns)), ([p], p_)) =([]:pos, pt, get_pos cI uI);
1.793 -
1.794 - print_depth 7;pt
1.795 - *)
1.796 + in iteratorOK2xml cI ip' end)
1.797 + handle (PTREE _) => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 21"
1.798 +fun moveDown cI p =
1.799 + ((let
1.800 + val ((pt, _), _) = get_calc cI
1.801 val ip' = move_dn [] pt p
1.802 - in iteratorOK2xml cI ip' end)
1.803 - handle (PTREE e) => iteratorERROR2xml cI)
1.804 - handle _ => sysERROR2xml cI "error in kernel 22";
1.805 + in iteratorOK2xml cI ip' end)
1.806 + handle (PTREE _) => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 22"
1.807
1.808 fun moveActiveLevelDown cI =
1.809 - ((let val ((pt,_),_) = get_calc cI
1.810 + ((let
1.811 + val ((pt, _) ,_) = get_calc cI
1.812 val ip' = movelevel_dn [] pt (get_pos cI 1)
1.813 val _ = upd_ipos cI 1 ip'
1.814 - in iteratorOK2xml cI ip' end)
1.815 - handle (PTREE e) => iteratorERROR2xml cI)
1.816 - handle _ => sysERROR2xml cI "error in kernel 23";
1.817 -fun moveLevelDown cI (p:pos') =
1.818 - ((let val ((pt,_),_) = get_calc cI
1.819 - val ip' = movelevel_dn [] pt p
1.820 - in iteratorOK2xml cI ip' end)
1.821 - handle (PTREE e) => iteratorERROR2xml cI)
1.822 - handle _ => sysERROR2xml cI "error in kernel 24";
1.823 + in iteratorOK2xml cI ip' end)
1.824 + handle (PTREE _) => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 23"
1.825 +fun moveLevelDown cI p =
1.826 + ((let
1.827 + val ((pt, _), _) = get_calc cI
1.828 + val ip' = movelevel_dn [] pt p
1.829 + in iteratorOK2xml cI ip' end)
1.830 + handle (PTREE _) => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 24"
1.831
1.832 fun moveActiveUp cI =
1.833 - ((let val ((pt,_),_) = get_calc cI
1.834 + ((let
1.835 + val ((pt, _), _) = get_calc cI
1.836 val ip' = move_up [] pt (get_pos cI 1)
1.837 val _ = upd_ipos cI 1 ip'
1.838 - in iteratorOK2xml cI ip' end)
1.839 - handle PTREE e => iteratorERROR2xml cI)
1.840 - handle _ => sysERROR2xml cI "error in kernel 25";
1.841 -fun moveUp cI (p:pos') =
1.842 - ((let val ((pt,_),_) = get_calc cI
1.843 + in iteratorOK2xml cI ip' end)
1.844 + handle PTREE _ => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 25"
1.845 +fun moveUp cI p =
1.846 + ((let
1.847 + val ((pt, _), _) = get_calc cI
1.848 val ip' = move_up [] pt p
1.849 - in iteratorOK2xml cI ip' end)
1.850 - handle PTREE e => iteratorERROR2xml cI)
1.851 - handle _ => sysERROR2xml cI "error in kernel 26";
1.852 + in iteratorOK2xml cI ip' end)
1.853 + handle PTREE _ => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 26"
1.854
1.855 fun moveActiveLevelUp cI =
1.856 - ((let val ((pt,_),_) = get_calc cI
1.857 - val ip' = movelevel_up [] pt (get_pos cI 1)
1.858 - val _ = upd_ipos cI 1 ip'
1.859 - in iteratorOK2xml cI ip' end)
1.860 - handle PTREE e => iteratorERROR2xml cI)
1.861 - handle _ => sysERROR2xml cI "error in kernel 27";
1.862 -fun moveLevelUp cI (p:pos') =
1.863 - ((let val ((pt,_),_) = get_calc cI
1.864 + ((let
1.865 + val ((pt, _), _) = get_calc cI
1.866 + val ip' = movelevel_up [] pt (get_pos cI 1)
1.867 + val _ = upd_ipos cI 1 ip'
1.868 + in iteratorOK2xml cI ip' end)
1.869 + handle PTREE _ => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 27"
1.870 +fun moveLevelUp cI p =
1.871 + ((let
1.872 + val ((pt, _), _) = get_calc cI
1.873 val ip' = movelevel_up [] pt p
1.874 - in iteratorOK2xml cI ip' end)
1.875 - handle PTREE e => iteratorERROR2xml cI)
1.876 - handle _ => sysERROR2xml cI "error in kernel 28";
1.877 + in iteratorOK2xml cI ip' end)
1.878 + handle PTREE _ => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 28"
1.879
1.880 fun moveActiveCalcHead cI =
1.881 - ((let val ((pt,_),_) = get_calc cI
1.882 + ((let
1.883 + val ((pt, _), _) = get_calc cI
1.884 val ip' = movecalchd_up pt (get_pos cI 1)
1.885 val _ = upd_ipos cI 1 ip'
1.886 - in iteratorOK2xml cI ip' end)
1.887 - handle PTREE e => iteratorERROR2xml cI)
1.888 - handle _ => sysERROR2xml cI "error in kernel 29";
1.889 -fun moveCalcHead cI (p:pos') =
1.890 - ((let val ((pt,_),_) = get_calc cI
1.891 + in iteratorOK2xml cI ip' end)
1.892 + handle PTREE _ => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 29"
1.893 +fun moveCalcHead cI p =
1.894 + ((let
1.895 + val ((pt, _), _) = get_calc cI
1.896 val ip' = movecalchd_up pt p
1.897 - in iteratorOK2xml cI ip' end)
1.898 - handle PTREE e => iteratorERROR2xml cI)
1.899 - handle _ => sysERROR2xml cI "error in kernel 30";
1.900 -
1.901 + in iteratorOK2xml cI ip' end)
1.902 + handle PTREE _ => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 30"
1.903
1.904 (*.initContext Thy_ is conceptually impossible at [Pbl,Met]
1.905 and at positions with Check_Postcond and End_Trans;
1.906 at possible pos's there can be NO rewrite (returned as a context, too).*)
1.907 -fun initContext (cI:calcID) Thy_ (pos as (p, p_):pos') =
1.908 +fun initContext cI Thy_ (pos as (p, p_):pos') =
1.909 ((if member op = [Pbl, Met] p_
1.910 then message2xml cI "thy-context not to calchead"
1.911 else if pos = ([], Res) then message2xml cI "no thy-context at result"
1.912 @@ -691,35 +593,35 @@
1.913 else message2xml cI "no thy-context at this position"
1.914 end)
1.915 handle _ => sysERROR2xml cI "error in kernel 31")
1.916 -
1.917 - | initContext cI Pbl_ (pos as (p,p_):pos') =
1.918 - ((let val ((pt,_),_) = get_calc cI
1.919 - val pp = par_pblobj pt p
1.920 - val chd = initcontext_pbl pt (pp,p_)
1.921 - in contextpblOK2xml cI chd end)
1.922 - handle _ => sysERROR2xml cI "error in kernel 32")
1.923 -
1.924 - | initContext cI Met_ (pos as (p,p_):pos') =
1.925 - ((let val ((pt,_),_) = get_calc cI
1.926 - val pp = par_pblobj pt p
1.927 - val chd = initcontext_met pt (pp,p_)
1.928 - in contextmetOK2xml cI chd end)
1.929 - handle _ => sysERROR2xml cI "error in kernel 33");
1.930 + | initContext cI Pbl_ (p, p_) =
1.931 + ((let
1.932 + val ((pt, _), _) = get_calc cI
1.933 + val pp = par_pblobj pt p
1.934 + val chd = initcontext_pbl pt (pp,p_)
1.935 + in contextpblOK2xml cI chd end)
1.936 + handle _ => sysERROR2xml cI "error in kernel 32")
1.937 + | initContext cI Met_ (p, p_) =
1.938 + ((let
1.939 + val ((pt,_),_) = get_calc cI
1.940 + val pp = par_pblobj pt p
1.941 + val chd = initcontext_met pt (pp,p_)
1.942 + in contextmetOK2xml cI chd end)
1.943 + handle _ => sysERROR2xml cI "error in kernel 33");
1.944
1.945 (* match a theorem, a ruleset (etc., selected in the knowledge-browser)
1.946 with the formula in the focus on the worksheet;
1.947 string contains the thy, thus it is unique as thmID, rlsID for this thy;
1.948 take the substitution from the istate of the formula *)
1.949 -fun checkContext (cI:calcID) (pos:pos' as (p,p_)) (guh:guh) =
1.950 +fun checkContext cI (pos as (p, p_)) guh =
1.951 case (implode o (take_fromto 1 4) o Symbol.explode) guh of
1.952 "thy_" =>
1.953 - if member op = [Pbl,Met] p_
1.954 + if member op = [Pbl, Met] p_
1.955 then message2xml cI "thy-context not to calchead"
1.956 else if pos = ([],Res) then message2xml cI "no thy-context at result"
1.957 else if no_thycontext guh then message2xml cI ("no thy-context for '" ^ guh ^ "'")
1.958 else
1.959 ((let
1.960 - val (ptp as (pt,_),_) = get_calc cI
1.961 + val ((pt,_),_) = get_calc cI
1.962 val is = get_istate pt pos
1.963 val subs = subs_from is "dummy" guh
1.964 val tac = guh2rewtac guh subs
1.965 @@ -729,7 +631,7 @@
1.966 with the model-pattern of the problem with pblID.*)
1.967 | "pbl_" =>
1.968 ((let
1.969 - val ((pt,_),_) = get_calc cI
1.970 + val ((pt, _), _) = get_calc cI
1.971 val pp = par_pblobj pt p
1.972 val keID = guh2kestoreID guh
1.973 val chd = context_pbl keID pt pp
1.974 @@ -737,7 +639,7 @@
1.975 ) handle _ => sysERROR2xml cI "error in kernel 35")
1.976 | "met_" =>
1.977 ((let
1.978 - val ((pt,_),_) = get_calc cI
1.979 + val ((pt, _), _) = get_calc cI
1.980 val pp = par_pblobj pt p
1.981 val keID = guh2kestoreID guh
1.982 val chd = context_met keID pt pp
1.983 @@ -746,13 +648,13 @@
1.984 | str => sysERROR2xml cI ("checkContext: str = " ^ str)
1.985
1.986 (* for an errpatID find "(fillpatID, fillform)" list
1.987 - which dedicated to this errpat and which is applicable at current formula*)
1.988 + which dedicated to this errpat and which is applicable at current formula *)
1.989 fun findFillpatterns cI errpatID =
1.990 let
1.991 val ((pt, _), _) = get_calc cI
1.992 - val pos = get_pos cI 1;
1.993 - val fillpats = find_fillpatterns (pt, pos) errpatID
1.994 - in findFillpatterns2xml cI (map #1 fillpats) end;
1.995 + val pos = get_pos cI 1;
1.996 + val fillpats = find_fillpatterns (pt, pos) errpatID
1.997 + in findFillpatterns2xml cI (map #1 fillpats) end
1.998
1.999 (* given a fillpatID propose a fillform to the learner on the worksheet;
1.1000 the "ctree" is extended with fillpat and "ostate Inconsistent",
1.1001 @@ -805,12 +707,10 @@
1.1002 (upd_calc cI (ptp, []);
1.1003 upd_ipos cI 1 p';
1.1004 autocalculateOK2xml cI pos (if null c then p' else last_elem c) p')
1.1005 - | (str,_) => autocalculateERROR2xml cI "failure"
1.1006 + | _ => autocalculateERROR2xml cI "failure"
1.1007 end
1.1008 | (msg, _) => message2xml cI msg
1.1009 - end
1.1010 -
1.1011 -(*------------------------------------------------------------------*)
1.1012 + end
1.1013 +(**)
1.1014 end
1.1015 -open Math_Engine;
1.1016 -(*------------------------------------------------------------------*)
1.1017 +(**)
2.1 --- a/src/Tools/isac/Interpret/script.sml Thu Nov 17 16:40:27 2016 +0100
2.2 +++ b/src/Tools/isac/Interpret/script.sml Mon Nov 21 12:47:02 2016 +0100
2.3 @@ -27,21 +27,24 @@
2.4 val rule2thm'' : rule -> thm''
2.5 val rule2rls' : rule -> string
2.6
2.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
2.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*
2.9 datatype asap = Aundef | AssOnly | AssGen
2.10 + datatype appy = Appy of tac_ * scrstate | Napp of env | Skip of term * env
2.11 datatype appy_ = Napp_ | Skip_
2.12 - val itms2args : 'a -> metID -> itm list -> term list
2.13 + val appy : theory' * rls -> ptree * pos' -> env -> lrd list -> term -> term option -> term -> appy
2.14 + val formal_args : term -> term list
2.15 val get_stac : 'a -> term -> term option
2.16 + val go : loc_ -> term -> term
2.17 val handle_leaf : string -> theory' -> rls -> env -> term option -> term -> term ->
2.18 term option * stacexpr
2.19 - val formal_args : term -> term list
2.20 - val go : loc_ -> term -> term
2.21 val id_of_scr : term -> string
2.22 - type appy
2.23 - val appy : theory' * rls -> ptree * pos' -> env -> lrd list -> term -> term option -> term -> appy
2.24 - val sel_appl_atomic_tacs : ptree -> pos' -> tac list
2.25 + val is_spec_pos : pos_ -> bool
2.26 + val itms2args : 'a -> metID -> itm list -> term list
2.27 val nstep_up : theory' * rls -> ptree * pos' -> scr -> env -> lrd list -> appy_ ->
2.28 term option -> term -> appy
2.29 + val sel_appl_atomic_tacs : ptree -> pos' -> tac list
2.30 + val stac2tac : ptree -> theory -> term -> tac
2.31 + val stac2tac_ : ptree -> theory -> term -> tac * tac_
2.32 val upd_env_opt : env -> term option * term -> env
2.33 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
2.34 end
2.35 @@ -50,7 +53,7 @@
2.36 val trace_script = Unsynchronized.ref false; (* TODO: how are traces done in Isabelle? *)
2.37
2.38 (**)
2.39 -structure Lucin: LUCAS_INTERPRETER(**) =
2.40 +structure Lucin(**): LUCAS_INTERPRETER(**) =
2.41 struct
2.42 (**)
2.43 (* data for creating a new node in ctree; designed for use as:
2.44 @@ -1209,4 +1212,3 @@
2.45 (**)
2.46 end
2.47 (**)
2.48 -(*open Lucin;*)
3.1 --- a/src/Tools/isac/Interpret/solve.sml Thu Nov 17 16:40:27 2016 +0100
3.2 +++ b/src/Tools/isac/Interpret/solve.sml Mon Nov 21 12:47:02 2016 +0100
3.3 @@ -371,15 +371,15 @@
3.4 (*FIXXXME040624: does NOT match interfaces/ITOCalc.java
3.5 TODO.WN0512 redesign togehter with autocalc ?*)
3.6 datatype auto =
3.7 - Step of int (*1 do #int steps; may stop in model/specify:
3.8 - IS VERY INEFFICIENT IN MODEL/SPECIY*)
3.9 + Step of int (*1 do #int steps (may stop in model/specify)
3.10 + IS VERY INEFFICIENT IN MODEL/SPECIY *)
3.11 | CompleteModel (*2 complete modeling
3.12 - if model complete, finish specifying + start solving*)
3.13 -| CompleteCalcHead (*3 complete model/specify in one go + start solving*)
3.14 + if model complete, finish specifying *)
3.15 +| CompleteCalcHead (*3 complete model/specify in one go *)
3.16 | CompleteToSubpbl (*4 stop at the next begin of a subproblem,
3.17 - if none, complete the actual (sub)problem*)
3.18 -| CompleteSubpbl (*5 complete the actual (sub)problem (incl.ev.subproblems)*)
3.19 -| CompleteCalc; (*6 complete the calculation as a whole*)
3.20 + if none, complete the actual (sub)problem *)
3.21 +| CompleteSubpbl (*5 complete the actual (sub)problem (incl.ev.subproblems) *)
3.22 +| CompleteCalc; (*6 complete the calculation as a whole *)
3.23
3.24 fun autoord (Step _ ) = 1
3.25 | autoord CompleteModel = 2
4.1 --- a/src/Tools/isac/Isac_Protocol.thy Thu Nov 17 16:40:27 2016 +0100
4.2 +++ b/src/Tools/isac/Isac_Protocol.thy Mon Nov 21 12:47:02 2016 +0100
4.3 @@ -11,7 +11,7 @@
4.4 XML.Elem (("CALCID", []), [XML.Text ci]),
4.5 form]) => (ci |> int_of_str', form |> xml_to_term_NEW |> term2str)
4.6 | x => raise ERROR ("append_form: WRONG intree = " ^ xmlstr 0 x)
4.7 - val result = Math_Engine.appendFormula calcid cterm'
4.8 + val result = Kernel.appendFormula calcid cterm'
4.9 in result end)
4.10 handle ERROR msg => appendformulaERROR2xml 4711 msg\<close>
4.11
4.12 @@ -27,7 +27,7 @@
4.13 | tree => raise ERROR ("autocalculate: WRONG intree = " ^ xmlstr 0 tree)
4.14 val SOME calcid = int_of_str ci
4.15 val auto = xml_to_auto a
4.16 - val result = Math_Engine.autoCalculate calcid auto
4.17 + val result = Kernel.autoCalculate calcid auto
4.18 in result end)
4.19 handle ERROR msg => autocalculateERROR2xml 4711 msg)}\<close>
4.20
4.21 @@ -42,7 +42,7 @@
4.22 XML.Elem (("CALCID", []), [XML.Text ci]),
4.23 pos, tac]) => (str2int ci, xml_to_pos pos, xml_to_tac tac)
4.24 | tree => raise ERROR ("apply_tac: WRONG intree = " ^ xmlstr 0 tree)
4.25 - val result = Math_Engine.applyTactic ci pos tac
4.26 + val result = Kernel.applyTactic ci pos tac
4.27 in result end)
4.28 handle ERROR msg => autocalculateERROR2xml 4711 msg)}\<close>
4.29
4.30 @@ -55,7 +55,7 @@
4.31 val fmz = case intree of
4.32 tree as XML.Elem (("FORMALIZATION", []), vars) => xml_to_fmz tree
4.33 | tree => raise ERROR ("calctree: WRONG intree = " ^ xmlstr 0 tree)
4.34 - val result = Math_Engine.CalcTree fmz
4.35 + val result = Kernel.CalcTree fmz
4.36 in result end)
4.37 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.38
4.39 @@ -72,7 +72,7 @@
4.40 XML.Elem (("GUH", []), [XML.Text guh])])
4.41 => (str2int ci, xml_to_pos pos, guh)
4.42 | tree => raise ERROR ("check_ctxt: WRONG intree = " ^ xmlstr 0 tree)
4.43 - val result = Math_Engine.checkContext ci pos guh
4.44 + val result = Kernel.checkContext ci pos guh
4.45 in result end)
4.46 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.47
4.48 @@ -82,7 +82,7 @@
4.49 to_lib = Codec.tree,
4.50 action = (fn calcid =>
4.51 let
4.52 - val result = Math_Engine.DEconstrCalcTree calcid
4.53 + val result = Kernel.DEconstrCalcTree calcid
4.54 in result end)}\<close>
4.55
4.56 (* val fetchApplicableTactics : calcID -> int -> pos' -> XML.tree *)
4.57 @@ -98,7 +98,7 @@
4.58 pos as XML.Elem (("POSITION", []), _)])
4.59 => (str2int ci, str2int i, xml_to_pos pos)
4.60 | tree => raise ERROR ("fetch_applicable_tacs: WRONG intree = " ^ xmlstr 0 tree)
4.61 - val result = Math_Engine.fetchApplicableTactics ci i pos
4.62 + val result = Kernel.fetchApplicableTactics ci i pos
4.63 in result end)
4.64 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.65
4.66 @@ -112,7 +112,7 @@
4.67 XML.Elem (("NEXTTAC", []), [
4.68 XML.Elem (("CALCID", []), [XML.Text ci])]) => (str2int ci)
4.69 | tree => raise ERROR ("fetch_proposed_tac: WRONG intree = " ^ xmlstr 0 tree)
4.70 - val result = Math_Engine.fetchProposedTactic ci
4.71 + val result = Kernel.fetchProposedTactic ci
4.72 in result end)
4.73 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.74
4.75 @@ -128,7 +128,7 @@
4.76 XML.Elem (("STRING", []), [XML.Text err_pat_id])])
4.77 => (str2int ci, err_pat_id)
4.78 | tree => raise ERROR ("find_fill_patts: WRONG intree = " ^ xmlstr 0 tree)
4.79 - val result = Math_Engine.findFillpatterns ci err_pat_id
4.80 + val result = Kernel.findFillpatterns ci err_pat_id
4.81 in result end)
4.82 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.83
4.84 @@ -144,7 +144,7 @@
4.85 pos as XML.Elem (("POSITION", []), _)])
4.86 => (str2int ci, xml_to_pos pos)
4.87 | tree => raise ERROR ("autocalculate: WRONG intree = " ^ xmlstr 0 tree)
4.88 - val result = Math_Engine.getAccumulatedAsms ci pos
4.89 + val result = Kernel.getAccumulatedAsms ci pos
4.90 in result end)
4.91 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.92
4.93 @@ -159,7 +159,7 @@
4.94 XML.Elem (("CALCID", []), [XML.Text ci])])
4.95 => (str2int ci)
4.96 | tree => raise ERROR ("get_active_form: WRONG intree = " ^ xmlstr 0 tree)
4.97 - val result = Math_Engine.getActiveFormula ci
4.98 + val result = Kernel.getActiveFormula ci
4.99 in result end)
4.100 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.101
4.102 @@ -175,7 +175,7 @@
4.103 pos as XML.Elem (("POSITION", []), _)])
4.104 => (str2int ci, xml_to_pos pos)
4.105 | tree => raise ERROR ("get_asms: WRONG intree = " ^ xmlstr 0 tree)
4.106 - val result = Math_Engine.getAssumptions ci pos
4.107 + val result = Kernel.getAssumptions ci pos
4.108 in result end)
4.109 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.110
4.111 @@ -198,7 +198,7 @@
4.112 XML.Elem (("BOOL", []), [XML.Text rules])])
4.113 => (str2int calcid, xml_to_pos from, xml_to_pos to, str2int level, string_to_bool rules)
4.114 | tree => raise ERROR ("getformulaefromto: WRONG intree = " ^ xmlstr 0 tree)
4.115 - val result = Math_Engine.getFormulaeFromTo calcid from to level rules
4.116 + val result = Kernel.getFormulaeFromTo calcid from to level rules
4.117 in result end)
4.118 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.119
4.120 @@ -214,7 +214,7 @@
4.121 pos as XML.Elem (("POSITION", []), _)])
4.122 => (str2int ci, xml_to_pos pos)
4.123 | tree => raise ERROR ("get_tac: WRONG intree = " ^ xmlstr 0 tree)
4.124 - val result = Math_Engine.getTactic ci pos
4.125 + val result = Kernel.getTactic ci pos
4.126 in result end)
4.127 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.128
4.129 @@ -231,7 +231,7 @@
4.130 pos as XML.Elem (("POSITION", []), _)])
4.131 => (str2int ci, xml_to_ketype ketype, xml_to_pos pos)
4.132 | tree => raise ERROR ("init_ctxt: WRONG intree = " ^ xmlstr 0 tree)
4.133 - val result = Math_Engine.initContext ci ketype pos
4.134 + val result = Kernel.initContext ci ketype pos
4.135 in result end)
4.136 handle ERROR msg => sysERROR2xml 4711 msg)
4.137 handle _ => sysERROR2xml 4711 "Protocol.operation_setup init_ctxt UNKNOWN exn")}\<close>
4.138 @@ -248,7 +248,7 @@
4.139 XML.Elem (("STRING", []), [XML.Text str])])
4.140 => (str2int ci, str)
4.141 | tree => raise ERROR ("input_fill_form: WRONG intree = " ^ xmlstr 0 tree)
4.142 - val result = Math_Engine.inputFillFormula ci str
4.143 + val result = Kernel.inputFillFormula ci str
4.144 in result end)
4.145 handle ERROR msg => message2xml 4711 msg)}\<close>
4.146
4.147 @@ -264,7 +264,7 @@
4.148 pos as XML.Elem (("POSITION", []), _)])
4.149 => (str2int ci, xml_to_pos pos)
4.150 | tree => raise ERROR ("inter_steps: WRONG intree = " ^ xmlstr 0 tree)
4.151 - val result = Math_Engine.interSteps ci pos
4.152 + val result = Kernel.interSteps ci pos
4.153 in result end)
4.154 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.155
4.156 @@ -274,7 +274,7 @@
4.157 to_lib = Codec.tree,
4.158 action = (fn calcid =>
4.159 let
4.160 - val result = Math_Engine.Iterator calcid
4.161 + val result = Kernel.Iterator calcid
4.162 in result end)}\<close>
4.163
4.164 (* val IteratorTEST : calcID -> iterID *)
4.165 @@ -290,7 +290,7 @@
4.166 XML.Elem (("CALCID", []), [XML.Text ci])])
4.167 => (str2int ci)
4.168 | tree => raise ERROR ("model_pbl: WRONG intree = " ^ xmlstr 0 tree)
4.169 - val result = Math_Engine.modelProblem ci
4.170 + val result = Kernel.modelProblem ci
4.171 in result end)
4.172 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.173
4.174 @@ -306,7 +306,7 @@
4.175 icalhd])
4.176 => (str2int ci, xml_to_icalhd icalhd)
4.177 | tree => raise ERROR ("modify_calchead: WRONG intree = " ^ xmlstr 0 tree)
4.178 - val result = Math_Engine.modifyCalcHead ci icalhd
4.179 + val result = Kernel.modifyCalcHead ci icalhd
4.180 in result end)
4.181 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.182
4.183 @@ -321,7 +321,7 @@
4.184 XML.Elem (("CALCID", []), [XML.Text ci])])
4.185 => (str2int ci)
4.186 | tree => raise ERROR ("move_active_calchead: WRONG intree = " ^ xmlstr 0 tree)
4.187 - val result = Math_Engine.moveActiveCalcHead ci
4.188 + val result = Kernel.moveActiveCalcHead ci
4.189 in result end)
4.190 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.191
4.192 @@ -336,7 +336,7 @@
4.193 XML.Elem (("CALCID", []), [XML.Text ci])])
4.194 => (str2int ci)
4.195 | tree => raise ERROR ("move_active_down: WRONG intree = " ^ xmlstr 0 tree)
4.196 - val result = Math_Engine.moveActiveDown ci
4.197 + val result = Kernel.moveActiveDown ci
4.198 in result end)
4.199 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.200
4.201 @@ -352,7 +352,7 @@
4.202 pos as XML.Elem (("POSITION", []), _)])
4.203 => (str2int ci, xml_to_pos pos)
4.204 | tree => raise ERROR ("move_active_form: WRONG intree = " ^ xmlstr 0 tree)
4.205 - val result = Math_Engine.moveActiveFormula ci pos
4.206 + val result = Kernel.moveActiveFormula ci pos
4.207 in result end)
4.208 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.209
4.210 @@ -367,7 +367,7 @@
4.211 XML.Elem (("CALCID", []), [XML.Text ci])])
4.212 => (str2int ci)
4.213 | tree => raise ERROR ("move_active_levdown: WRONG intree = " ^ xmlstr 0 tree)
4.214 - val result = Math_Engine.moveActiveLevelDown ci
4.215 + val result = Kernel.moveActiveLevelDown ci
4.216 in result end)
4.217 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.218
4.219 @@ -382,7 +382,7 @@
4.220 XML.Elem (("CALCID", []), [XML.Text ci])])
4.221 => (str2int ci)
4.222 | tree => raise ERROR ("move_active_levup: WRONG intree = " ^ xmlstr 0 tree)
4.223 - val result = Math_Engine.moveActiveLevelUp ci
4.224 + val result = Kernel.moveActiveLevelUp ci
4.225 in result end)
4.226 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.227
4.228 @@ -392,7 +392,7 @@
4.229 to_lib = Codec.tree,
4.230 action = (fn calcid =>
4.231 let
4.232 - val result = Math_Engine.moveActiveRoot calcid
4.233 + val result = Kernel.moveActiveRoot calcid
4.234 in result end)}\<close>
4.235
4.236 (* val moveActiveRootTEST : calcID -> XML.tree *)
4.237 @@ -408,7 +408,7 @@
4.238 XML.Elem (("CALCID", []), [XML.Text ci])])
4.239 => (str2int ci)
4.240 | tree => raise ERROR ("move_active_up: WRONG intree = " ^ xmlstr 0 tree)
4.241 - val result = Math_Engine.moveActiveUp ci
4.242 + val result = Kernel.moveActiveUp ci
4.243 in result end)
4.244 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.245
4.246 @@ -424,7 +424,7 @@
4.247 pos as XML.Elem (("POSITION", []), _)])
4.248 => (str2int ci, xml_to_pos pos)
4.249 | tree => raise ERROR ("move_active_calchead: WRONG intree = " ^ xmlstr 0 tree)
4.250 - val result = Math_Engine.moveCalcHead ci pos
4.251 + val result = Kernel.moveCalcHead ci pos
4.252 in result end)
4.253 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.254
4.255 @@ -440,7 +440,7 @@
4.256 pos as XML.Elem (("POSITION", []), _)])
4.257 => (str2int ci, xml_to_pos pos)
4.258 | tree => raise ERROR ("move_down: WRONG intree = " ^ xmlstr 0 tree)
4.259 - val result = Math_Engine.moveDown ci pos
4.260 + val result = Kernel.moveDown ci pos
4.261 in result end)
4.262 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.263
4.264 @@ -456,7 +456,7 @@
4.265 pos as XML.Elem (("POSITION", []), _)])
4.266 => (str2int ci, xml_to_pos pos)
4.267 | tree => raise ERROR ("move_levdn: WRONG intree = " ^ xmlstr 0 tree)
4.268 - val result = Math_Engine.moveLevelDown ci pos
4.269 + val result = Kernel.moveLevelDown ci pos
4.270 in result end)
4.271 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.272
4.273 @@ -472,7 +472,7 @@
4.274 pos as XML.Elem (("POSITION", []), _)])
4.275 => (str2int ci, xml_to_pos pos)
4.276 | tree => raise ERROR ("move_levup: WRONG intree = " ^ xmlstr 0 tree)
4.277 - val result = Math_Engine.moveLevelUp ci pos
4.278 + val result = Kernel.moveLevelUp ci pos
4.279 in result end)
4.280 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.281
4.282 @@ -487,7 +487,7 @@
4.283 XML.Elem (("CALCID", []), [XML.Text ci])])
4.284 => (str2int ci)
4.285 | tree => raise ERROR ("move_root: WRONG intree = " ^ xmlstr 0 tree)
4.286 - val result = Math_Engine.moveRoot ci
4.287 + val result = Kernel.moveRoot ci
4.288 in result end)
4.289 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.290
4.291 @@ -503,7 +503,7 @@
4.292 pos as XML.Elem (("POSITION", []), _)])
4.293 => (str2int ci, xml_to_pos pos)
4.294 | tree => raise ERROR ("move_up: WRONG intree = " ^ xmlstr 0 tree)
4.295 - val result = Math_Engine.moveUp ci pos
4.296 + val result = Kernel.moveUp ci pos
4.297 in result end)
4.298 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.299
4.300 @@ -520,7 +520,7 @@
4.301 | tree => raise ERROR ("refformula: WRONG intree = " ^ xmlstr 0 tree)
4.302 val SOME calcid = int_of_str ci
4.303 val pos = xml_to_pos p
4.304 - val result = Math_Engine.refFormula calcid pos
4.305 + val result = Kernel.refFormula calcid pos
4.306 in result end)
4.307 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.308
4.309 @@ -537,7 +537,7 @@
4.310 XML.Elem (("GUH", []), [XML.Text guh])])
4.311 => (str2int ci, xml_to_pos pos, guh)
4.312 | tree => raise ERROR ("refine_pbl: WRONG intree = " ^ xmlstr 0 tree)
4.313 - val result = Math_Engine.refineProblem ci pos guh
4.314 + val result = Kernel.refineProblem ci pos guh
4.315 in result end)
4.316 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.317
4.318 @@ -552,7 +552,7 @@
4.319 XML.Elem (("CALCID", []), [XML.Text ci]), form])
4.320 => (ci |> int_of_str', form |> xml_to_term_NEW |> term2str)
4.321 | tree => raise ERROR ("replace_form: WRONG intree = " ^ xmlstr 0 tree)
4.322 - val result = Math_Engine.replaceFormula calcid cterm'
4.323 + val result = Kernel.replaceFormula calcid cterm'
4.324 in result end)
4.325 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.326
4.327 @@ -569,7 +569,7 @@
4.328 XML.Elem (("FILLPATTID", []), [XML.Text fillpat_id])])
4.329 => (str2int ci, errpat_id, fillpat_id)
4.330 | tree => raise ERROR ("request_fill_form: WRONG intree = " ^ xmlstr 0 tree)
4.331 - val result = Math_Engine.requestFillformula ci (errpat_id, fillpat_id)
4.332 + val result = Kernel.requestFillformula ci (errpat_id, fillpat_id)
4.333 in result end)
4.334 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.335
4.336 @@ -584,7 +584,7 @@
4.337 XML.Elem (("CALCID", []), [XML.Text ci])])
4.338 => (str2int ci)
4.339 | tree => raise ERROR ("reset_calchead: WRONG intree = " ^ xmlstr 0 tree)
4.340 - val result = Math_Engine.resetCalcHead ci
4.341 + val result = Kernel.resetCalcHead ci
4.342 in result end)
4.343 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.344
4.345 @@ -601,7 +601,7 @@
4.346 XML.Elem (("GUH", []), [XML.Text guh])])
4.347 => (str2int ci, xml_to_pos pos, guh)
4.348 | tree => raise ERROR ("set_ctxt: WRONG intree = " ^ xmlstr 0 tree)
4.349 - val result = Math_Engine.setContext ci pos guh
4.350 + val result = Kernel.setContext ci pos guh
4.351 in result end)
4.352 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.353
4.354 @@ -619,7 +619,7 @@
4.355 XML.Elem (("METHODID", []), [met_id])])
4.356 => (str2int ci, xml_to_strs met_id)
4.357 | tree => raise ERROR ("set_met: WRONG intree = " ^ xmlstr 0 tree)
4.358 - val result = Math_Engine.setMethod ci met_id
4.359 + val result = Kernel.setMethod ci met_id
4.360 in result end)
4.361 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.362
4.363 @@ -635,7 +635,7 @@
4.364 tac])
4.365 => (str2int ci, xml_to_tac tac)
4.366 | tree => raise ERROR ("set_next_tac: WRONG intree = " ^ xmlstr 0 tree)
4.367 - val result = Math_Engine.setNextTactic ci tac
4.368 + val result = Kernel.setNextTactic ci tac
4.369 in result end)
4.370 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.371
4.372 @@ -653,7 +653,7 @@
4.373 XML.Elem (("PROBLEMID", []), [pbl_id])])
4.374 => (str2int ci, xml_to_strs pbl_id)
4.375 | tree => raise ERROR ("set_pbl: WRONG intree = " ^ xmlstr 0 tree)
4.376 - val result = Math_Engine.setProblem ci pbl_id
4.377 + val result = Kernel.setProblem ci pbl_id
4.378 in result end)
4.379 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.380
4.381 @@ -669,7 +669,7 @@
4.382 XML.Elem (("THEORYID", []), [XML.Text thy_id])])
4.383 => (str2int ci, thy_id)
4.384 | tree => raise ERROR ("set_thy: WRONG intree = " ^ xmlstr 0 tree)
4.385 - val result = Math_Engine.setTheory ci thy_id
4.386 + val result = Kernel.setTheory ci thy_id
4.387 in result end)
4.388 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.389
5.1 --- a/src/Tools/isac/xmlsrc/mathml.sml Thu Nov 17 16:40:27 2016 +0100
5.2 +++ b/src/Tools/isac/xmlsrc/mathml.sml Mon Nov 21 12:47:02 2016 +0100
5.3 @@ -13,7 +13,7 @@
5.4 ad(1) decode "^^^" ---> "^"; see Knowledge/Atools.thy;
5.5 ad(2) decode "<" ---> "<", decode ">" ---> ">"
5.6 decode "&" ---> "&"
5.7 - called for term2xml; + see "fun encode" in Frontend/interface.sml.*)
5.8 + called for term2xml; + see "fun encode" below*)
5.9 fun decode (str:cterm') =
5.10 let fun dec [] = []
5.11 | dec ("^"::"^"::"^"::cs) = "^"::(dec cs)
6.1 --- a/test/Tools/isac/Test_Isac.thy Thu Nov 17 16:40:27 2016 +0100
6.2 +++ b/test/Tools/isac/Test_Isac.thy Mon Nov 21 12:47:02 2016 +0100
6.3 @@ -20,12 +20,14 @@
6.4
6.5 In order to maintain these tests without changes, this has to be done before running tests:
6.6 (1) Query replace in src/Tools/isac:
6.7 - "--- ! aktivate for Test_Isac BEGIN ---\* )" --> "--- ! aktivate for Test_Isac BEGIN ---\*)"
6.8 - "( *\--- ! aktivate for Test_Isac END ---" --> "(*\--- ! aktivate for Test_Isac END ---"
6.9 + "--- ! aktivate for Test_Isac BEGIN ---\* )" \<longrightarrow> "--- ! aktivate for Test_Isac BEGIN ---\*)"
6.10 + "( *\--- ! aktivate for Test_Isac END ---" \<longrightarrow> "(*\--- ! aktivate for Test_Isac END ---"
6.11 This extends the signatures with some functions required for some tests.
6.12
6.13 Running Test_Isac.thy opens all structures, see code after "begin" below.
6.14
6.15 +* before running Test_Isac.thy ^^^ \<longrightarrow> ^^^ in src/Tools/isac
6.16 +* after running Test_Isac.thy ^^^ <-- ^^^ in src/Tools/isac
6.17 *********************** DON'T FORGET TO REVERSE CHANGE (1) AFTER TESTS ***********************
6.18 \<close>
6.19
6.20 @@ -65,6 +67,7 @@
6.21 ML {*
6.22 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
6.23 open Lucin;
6.24 + open Kernel;
6.25 (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
6.26 *}
6.27 ML {*