1.1 --- a/src/Tools/isac/Frontend/interface.sml Sat Mar 08 11:07:52 2014 +0100
1.2 +++ b/src/Tools/isac/Frontend/interface.sml Mon Mar 10 21:07:35 2014 +0100
1.3 @@ -13,7 +13,7 @@
1.4 val DEconstrCalcTree : calcID -> unit
1.5 val Iterator : calcID -> unit
1.6 val IteratorTEST : calcID -> iterID
1.7 - val appendFormula : calcID -> cterm' -> unit
1.8 + val appendFormula : calcID -> cterm' -> unit future
1.9 val autoCalculate : calcID -> auto -> unit
1.10 val checkContext : calcID -> pos' -> guh -> unit
1.11 val fetchApplicableTactics : calcID -> int -> pos' -> unit
1.12 @@ -71,7 +71,7 @@
1.13 encode "^" ---> "^^^"; see Knowledge/Atools.thy;
1.14 called for each cterm', icalhd, fmz in this interface;
1.15 + see "fun decode" in xmlsrc/mathml.sml *)
1.16 -fun encode (str : cterm') =
1.17 +fun encode (str : cterm') =
1.18 let fun enc [] = []
1.19 | enc ("^" :: cs) = "^" :: "^" :: "^" :: (enc cs)
1.20 | enc (c :: cs) = c :: (enc cs)
1.21 @@ -137,7 +137,7 @@
1.22 val (cI, tac) = (1, Rewrite_Set "Test_simplify");
1.23 *)
1.24 fun setNextTactic (cI:calcID) tac =
1.25 - let
1.26 + let
1.27 val ((pt, _), _) = get_calc cI
1.28 val ip = get_pos cI 1
1.29 in case locatetac tac (pt, ip) of
1.30 @@ -159,7 +159,7 @@
1.31 let
1.32 val ((pt, _), _) = get_calc cI
1.33 val p = get_pos cI 1
1.34 - in
1.35 + in
1.36 case locatetac tac (pt, ip) of
1.37 ("ok", (_, c, ptp as (_,p'))) =>
1.38 (upd_calc cI (ptp, []);
1.39 @@ -214,7 +214,7 @@
1.40 | (str, _, _) => autocalculateERROR2xml cI str
1.41 end)
1.42 handle _ => sysERROR2xml cI "error in kernel";
1.43 -
1.44 +
1.45
1.46 (* val (cI:calcID, ichd as ((p,_),_,_,_,_):icalhd) =
1.47 (1, (([],Pbl), "not used here",
1.48 @@ -233,7 +233,7 @@
1.49 val (cI:calcID, ichd as ((p,_),_,_,_,_):icalhd) =
1.50 (1, (([],Pbl),"solveTest (1+-1*2+x=0,x)", [], Pbl, ("", [], [])));
1.51 val (cI, p:pos')=(1, ([1],Frm));
1.52 - val (cI, p:pos')=(1, ([1,2,1,3],Res));
1.53 + val (cI, p:pos')=(1, ([1,2,1,3],Res));
1.54 *)
1.55 fun getTactic cI (p:pos') =
1.56 (let val ((pt,_),_) = get_calc cI
1.57 @@ -256,16 +256,16 @@
1.58 fun fetchApplicableTactics cI (scope:int) (p:pos') =
1.59 (let val ((pt, _), _) = get_calc cI
1.60 in (applicabletacticsOK cI (sel_rules pt p))
1.61 - handle PTREE str => sysERROR2xml cI str
1.62 + handle PTREE str => sysERROR2xml cI str
1.63 end)
1.64 handle _ => sysERROR2xml cI "error in kernel";
1.65 (*WN120611 took version 1 again
1.66 - version 2: fetch _applicable_ _elementary_ (ie. recursively
1.67 + version 2: fetch _applicable_ _elementary_ (ie. recursively
1.68 decompose rule-sets) Rewrite*, Calculate
1.69 fun fetchApplicableTactics cI (scope:int) (p:pos') =
1.70 (let val ((pt, _), _) = get_calc cI
1.71 in (applicabletacticsOK cI (sel_appl_atomic_tacs pt p))
1.72 - handle PTREE str => sysERROR2xml cI str
1.73 + handle PTREE str => sysERROR2xml cI str
1.74 end)
1.75 handle _ => sysERROR2xml cI "error in kernel";
1.76 *)
1.77 @@ -294,7 +294,7 @@
1.78 in refformulaOK2xml cI p form end)
1.79 handle _ => sysERROR2xml cI "error in kernel";
1.80
1.81 -(*.get formulae 'from' 'to' w.r.t. ordering in Position#compareTo(Position p);
1.82 +(*.get formulae 'from' 'to' w.r.t. ordering in Position#compareTo(Position p);
1.83 in case of CalcHeads only the headline is taken
1.84 (the pos' allows distinction between PrfObj and PblObj anyway);
1.85 'level' is adjusted such that an 'interval' of formulae is returned;
1.86 @@ -364,62 +364,62 @@
1.87 fun modifyCalcHead (cI:calcID) (ichd as ((p,_),_,_,_,_):icalhd) =
1.88 (let val ((pt,_),_) = get_calc cI
1.89 val (pt, chd as (_,p_,_,_,_,_)) = input_icalhd pt ichd
1.90 - in (upd_calc cI ((pt, (p,p_)), []);
1.91 + in (upd_calc cI ((pt, (p,p_)), []);
1.92 modifycalcheadOK2xml cI chd) end)
1.93 handle _ => sysERROR2xml cI "error in kernel";
1.94
1.95 -(*.at the activeFormula set the Model, the Guard and the Specification
1.96 +(*.at the activeFormula set the Model, the Guard and the Specification
1.97 to empty and return a CalcHead;
1.98 the 'origin' remains (for reconstructing all that).*)
1.99 -fun resetCalcHead (cI:calcID) =
1.100 +fun resetCalcHead (cI:calcID) =
1.101 (let val (ptp,_) = get_calc cI
1.102 val ptp = reset_calchead ptp
1.103 - in (upd_calc cI (ptp, []);
1.104 + in (upd_calc cI (ptp, []);
1.105 modifycalcheadOK2xml cI (get_ocalhd ptp)) end)
1.106 handle _ => sysERROR2xml cI "error in kernel";
1.107
1.108 -(*.at the activeFormula insert all the Descriptions in the Model
1.109 +(*.at the activeFormula insert all the Descriptions in the Model
1.110 (_not_ in the Guard) and return a CalcHead;
1.111 - the Descriptions are for user-guidance; the rest of the items
1.112 - are left empty for user-input;
1.113 + the Descriptions are for user-guidance; the rest of the items
1.114 + are left empty for user-input;
1.115 includes a resetCalcHead for the Model and the Guard.*)
1.116 -fun modelProblem (cI:calcID) =
1.117 +fun modelProblem (cI:calcID) =
1.118 (let val (ptp, _) = get_calc cI
1.119 val ptp = reset_calchead ptp
1.120 val (_, _, ptp) = nxt_specif Model_Problem ptp
1.121 - in (upd_calc cI (ptp, []);
1.122 + in (upd_calc cI (ptp, []);
1.123 modifycalcheadOK2xml cI (get_ocalhd ptp)) end)
1.124 handle _ => sysERROR2xml cI "error in kernel";
1.125
1.126
1.127 (* set the UContext determined on a knowledgebrowser to the current calc *)
1.128 fun setContext (cI:calcID) (ip as (_,p_):pos') (guh:guh) =
1.129 - (case (implode o (take_fromto 1 4) o Symbol.explode) guh of
1.130 + (case (implode o (take_fromto 1 4) o Symbol.explode) guh of
1.131 "thy_" =>
1.132 if member op = [Pbl,Met] p_
1.133 then message2xml cI "thy-context not to calchead"
1.134 else if ip = ([],Res) then message2xml cI "no thy-context at result"
1.135 else if no_thycontext guh then message2xml cI ("no thy-context for '" ^ guh ^ "'")
1.136 - else
1.137 + else
1.138 let
1.139 val (ptp as (pt, pold), _) = get_calc cI
1.140 val is = get_istate pt ip
1.141 val subs = subs_from is "dummy" guh
1.142 val tac = guh2rewtac guh subs
1.143 - in
1.144 + in
1.145 case locatetac tac (pt, ip) of (*='fun setNextTactic'+step*)
1.146 ("ok", (tacis, c, ptp as (_,p))) =>
1.147 - (upd_calc cI ((pt,p), []);
1.148 + (upd_calc cI ((pt,p), []);
1.149 autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)
1.150 | ("unsafe-ok", (tacis, c, ptp as (_,p))) =>
1.151 - (upd_calc cI ((pt,p), []);
1.152 + (upd_calc cI ((pt,p), []);
1.153 autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)
1.154 | ("end-of-calculation",_) => message2xml cI "end-of-calculation"
1.155 | ("failure",_) => sysERROR2xml cI "failure"
1.156 | ("not-applicable",_) => (*the rule comes from anywhere..*)
1.157 - (case applicable_in ip pt tac of
1.158 + (case applicable_in ip pt tac of
1.159 Notappl e => message2xml cI ("'" ^ tac2str tac ^ "' not-applicable")
1.160 - | Appl m =>
1.161 + | Appl m =>
1.162 let
1.163 val ctxt = get_ctxt pt pold
1.164 val (p,c,_,pt) =
1.165 @@ -433,7 +433,7 @@
1.166 val pI = guh2kestoreID guh
1.167 val ((pt, _), _) = get_calc cI
1.168 in
1.169 - if member op = [Pbl, Met] p_
1.170 + if member op = [Pbl, Met] p_
1.171 then
1.172 let val (pt, chd) = set_problem pI (pt, ip)
1.173 in (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end
1.174 @@ -456,12 +456,12 @@
1.175 (*.specify the Method at the activeFormula and return a CalcHead
1.176 containing the Guard.
1.177 WN0512 impl.incomplete, see 'nxt_specif (Specify_Method '.*)
1.178 -fun setMethod (cI:calcID) (mI:metID) =
1.179 +fun setMethod (cI:calcID) (mI:metID) =
1.180 (* val (cI, mI) = (1, ["Test","solve_linear"]);
1.181 *)
1.182 (let val ((pt, _), _) = get_calc cI
1.183 val ip as (_, p_) = get_pos cI 1
1.184 - in if member op = [Pbl,Met] p_
1.185 + in if member op = [Pbl,Met] p_
1.186 then let val (pt, chd) = set_method mI (pt, ip)
1.187 in (upd_calc cI ((pt, ip), []);
1.188 modifycalcheadOK2xml cI chd) end
1.189 @@ -500,7 +500,7 @@
1.190
1.191 (**. without update of CalcTree .**)
1.192
1.193 -(*.match the model of a problem at pos p
1.194 +(*.match the model of a problem at pos p
1.195 with the model-pattern of the problem with pblID*)
1.196 (*fun tryMatchProblem cI pblID =
1.197 (let val ((pt,_),_) = get_calc cI
1.198 @@ -521,7 +521,7 @@
1.199 handle _ => sysERROR2xml cI "error in kernel";
1.200
1.201 (* append a formula to the calculation *)
1.202 -fun appendFormula cI (ifo:cterm') =
1.203 +fun appendFormula' cI (ifo:cterm') =
1.204 (let
1.205 val cs = get_calc cI
1.206 val pos as (_,p_) = get_pos cI 1
1.207 @@ -540,6 +540,8 @@
1.208 end)
1.209 handle _ => sysERROR2xml cI "error in kernel";
1.210
1.211 +fun appendFormula cI ifo = Future.fork (fn () => appendFormula' cI ifo);
1.212 +
1.213 (* replace a formula with_in_ a calculation;
1.214 this situation applies for initial CAS-commands, too *)
1.215 fun replaceFormula cI (ifo:cterm') =
1.216 @@ -671,7 +673,7 @@
1.217 handle _ => sysERROR2xml cI "error in kernel";
1.218
1.219
1.220 -(*.initContext Thy_ is conceptually impossible at [Pbl,Met]
1.221 +(*.initContext Thy_ is conceptually impossible at [Pbl,Met]
1.222 and at positions with Check_Postcond and End_Trans;
1.223 at possible pos's there can be NO rewrite (returned as a context, too).*)
1.224 (* val (cI, Thy_, (pos as (p,p_):pos')) = (1, Thy_, ([1], Frm));
1.225 @@ -687,7 +689,7 @@
1.226 in if exist_lev_on' pt pos
1.227 then let val pos' = lev_on' pt pos
1.228 val tac = get_tac_checked pt pos'
1.229 - in if is_rewtac tac
1.230 + in if is_rewtac tac
1.231 then contextthyOK2xml cI (context_thy (pt,pos) tac)
1.232 else message2xml cI ("no thy-context at tac '" ^
1.233 tac2str tac ^ "'")
1.234 @@ -699,8 +701,8 @@
1.235 *)
1.236 ("ok", (tacis, _, (pt,_))) =>
1.237 let val tac = fst3 (last_elem tacis)
1.238 - in if is_rewtac tac
1.239 - then contextthyOK2xml
1.240 + in if is_rewtac tac
1.241 + then contextthyOK2xml
1.242 cI (context_thy ptp tac)
1.243 else message2xml cI ("no thy-context at tac '" ^
1.244 tac2str tac ^ "'")
1.245 @@ -712,7 +714,7 @@
1.246
1.247 (* val (cI, Pbl_, pos as (p,p_)) = (1, Pbl_, ([],Pbl));
1.248 *)
1.249 - | initContext cI Pbl_ (pos as (p,p_):pos') =
1.250 + | initContext cI Pbl_ (pos as (p,p_):pos') =
1.251 ((let val ((pt,_),_) = get_calc cI
1.252 val pp = par_pblobj pt p
1.253 val chd = initcontext_pbl pt (pp,p_)
1.254 @@ -748,8 +750,8 @@
1.255 val subs = subs_from is "dummy" guh
1.256 val tac = guh2rewtac guh subs
1.257 in contextthyOK2xml cI (context_thy (pt, pos) tac) end
1.258 -
1.259 - (*.match the model of a problem at pos p
1.260 +
1.261 + (*.match the model of a problem at pos p
1.262 with the model-pattern of the problem with pblID.*)
1.263 (* val (cI, pos:pos' as (p,p_), guh) =
1.264 (1, p, kestoreID2guh Pbl_ ["univariate","equation"]);
1.265 @@ -758,16 +760,16 @@
1.266 val (cI, pos:pos' as (p,p_), guh) =
1.267 (1, ([],Pbl), "pbl_equ_univ");
1.268 *)
1.269 - | "pbl_" =>
1.270 + | "pbl_" =>
1.271 let val ((pt,_),_) = get_calc cI
1.272 val pp = par_pblobj pt p
1.273 val keID = guh2kestoreID guh
1.274 val chd = context_pbl keID pt pp
1.275 in matchpbl2xml cI chd end
1.276 -(* val (cI, pos:pos' as (p,p_), guh) =
1.277 +(* val (cI, pos:pos' as (p,p_), guh) =
1.278 (1, ([],Pbl), kestoreID2guh Met_ ["LinEq", "solve_lineq_equation"]);
1.279 *)
1.280 - | "met_" =>
1.281 + | "met_" =>
1.282 let val ((pt,_),_) = get_calc cI
1.283 val pp = par_pblobj pt p
1.284 val keID = guh2kestoreID guh
1.285 @@ -775,9 +777,9 @@
1.286 in matchmet2xml cI chd end)
1.287 handle _ => sysERROR2xml cI "error in kernel";
1.288
1.289 -(* for an errpatID find "(fillpatID, fillform)" list
1.290 +(* for an errpatID find "(fillpatID, fillform)" list
1.291 which dedicated to this errpat and which is applicable at current formula*)
1.292 -fun findFillpatterns cI errpatID =
1.293 +fun findFillpatterns cI errpatID =
1.294 let
1.295 val ((pt, _), _) = get_calc cI
1.296 val pos = get_pos cI 1;
1.297 @@ -794,9 +796,9 @@
1.298 let
1.299 val ((pt, _), _) = get_calc cI
1.300 val pos = get_pos cI 1
1.301 - val fillforms = find_fillpatterns (pt, pos) errpatID
1.302 + val fillforms = find_fillpatterns (pt, pos) errpatID
1.303 in
1.304 - case filter ((curry op = fillpatID) o
1.305 + case filter ((curry op = fillpatID) o
1.306 (#1: (fillpatID * term * thm * (subs option) -> fillpatID))) fillforms of
1.307 (_, fillform, thm, sube_opt) :: _ =>
1.308 let
1.309 @@ -806,8 +808,8 @@
1.310 (upd_calc cI ((pt, pos'), []); (*upd_ipos cI 1 pos';*)
1.311 autocalculateOK2xml cI pos pos' pos')
1.312 end
1.313 - | _ => autocalculateERROR2xml cI "no fillpattern found"
1.314 - end;
1.315 + | _ => autocalculateERROR2xml cI "no fillpattern found"
1.316 + end;
1.317
1.318 (* input a formula which exactly fills the gaps in a "fillformula"
1.319 presented to the learner immediately before by "requestFillformula (errpatID, fillpatID)":