# HG changeset patch # User Mathias Lehnfeld # Date 1394482055 -3600 # Node ID d580d7fc9b8ecfa9d151fa2bf1ea13bc6f36adad # Parent 7961cffaafcf41a534470a4f930873e51f80551d user session management now parallel appendFormula uses futures. diff -r 7961cffaafcf -r d580d7fc9b8e src/Tools/isac/Frontend/interface.sml --- a/src/Tools/isac/Frontend/interface.sml Sat Mar 08 11:07:52 2014 +0100 +++ b/src/Tools/isac/Frontend/interface.sml Mon Mar 10 21:07:35 2014 +0100 @@ -13,7 +13,7 @@ val DEconstrCalcTree : calcID -> unit val Iterator : calcID -> unit val IteratorTEST : calcID -> iterID - val appendFormula : calcID -> cterm' -> unit + val appendFormula : calcID -> cterm' -> unit future val autoCalculate : calcID -> auto -> unit val checkContext : calcID -> pos' -> guh -> unit val fetchApplicableTactics : calcID -> int -> pos' -> unit @@ -71,7 +71,7 @@ encode "^" ---> "^^^"; see Knowledge/Atools.thy; called for each cterm', icalhd, fmz in this interface; + see "fun decode" in xmlsrc/mathml.sml *) -fun encode (str : cterm') = +fun encode (str : cterm') = let fun enc [] = [] | enc ("^" :: cs) = "^" :: "^" :: "^" :: (enc cs) | enc (c :: cs) = c :: (enc cs) @@ -137,7 +137,7 @@ val (cI, tac) = (1, Rewrite_Set "Test_simplify"); *) fun setNextTactic (cI:calcID) tac = - let + let val ((pt, _), _) = get_calc cI val ip = get_pos cI 1 in case locatetac tac (pt, ip) of @@ -159,7 +159,7 @@ let val ((pt, _), _) = get_calc cI val p = get_pos cI 1 - in + in case locatetac tac (pt, ip) of ("ok", (_, c, ptp as (_,p'))) => (upd_calc cI (ptp, []); @@ -214,7 +214,7 @@ | (str, _, _) => autocalculateERROR2xml cI str end) handle _ => sysERROR2xml cI "error in kernel"; - + (* val (cI:calcID, ichd as ((p,_),_,_,_,_):icalhd) = (1, (([],Pbl), "not used here", @@ -233,7 +233,7 @@ val (cI:calcID, ichd as ((p,_),_,_,_,_):icalhd) = (1, (([],Pbl),"solveTest (1+-1*2+x=0,x)", [], Pbl, ("", [], []))); val (cI, p:pos')=(1, ([1],Frm)); - val (cI, p:pos')=(1, ([1,2,1,3],Res)); + val (cI, p:pos')=(1, ([1,2,1,3],Res)); *) fun getTactic cI (p:pos') = (let val ((pt,_),_) = get_calc cI @@ -256,16 +256,16 @@ fun fetchApplicableTactics cI (scope:int) (p:pos') = (let val ((pt, _), _) = get_calc cI in (applicabletacticsOK cI (sel_rules pt p)) - handle PTREE str => sysERROR2xml cI str + handle PTREE str => sysERROR2xml cI str end) handle _ => sysERROR2xml cI "error in kernel"; (*WN120611 took version 1 again - version 2: fetch _applicable_ _elementary_ (ie. recursively + version 2: fetch _applicable_ _elementary_ (ie. recursively decompose rule-sets) Rewrite*, Calculate fun fetchApplicableTactics cI (scope:int) (p:pos') = (let val ((pt, _), _) = get_calc cI in (applicabletacticsOK cI (sel_appl_atomic_tacs pt p)) - handle PTREE str => sysERROR2xml cI str + handle PTREE str => sysERROR2xml cI str end) handle _ => sysERROR2xml cI "error in kernel"; *) @@ -294,7 +294,7 @@ in refformulaOK2xml cI p form end) handle _ => sysERROR2xml cI "error in kernel"; -(*.get formulae 'from' 'to' w.r.t. ordering in Position#compareTo(Position p); +(*.get formulae 'from' 'to' w.r.t. ordering in Position#compareTo(Position p); in case of CalcHeads only the headline is taken (the pos' allows distinction between PrfObj and PblObj anyway); 'level' is adjusted such that an 'interval' of formulae is returned; @@ -364,62 +364,62 @@ fun modifyCalcHead (cI:calcID) (ichd as ((p,_),_,_,_,_):icalhd) = (let val ((pt,_),_) = get_calc cI val (pt, chd as (_,p_,_,_,_,_)) = input_icalhd pt ichd - in (upd_calc cI ((pt, (p,p_)), []); + in (upd_calc cI ((pt, (p,p_)), []); modifycalcheadOK2xml cI chd) end) handle _ => sysERROR2xml cI "error in kernel"; -(*.at the activeFormula set the Model, the Guard and the Specification +(*.at the activeFormula set the Model, the Guard and the Specification to empty and return a CalcHead; the 'origin' remains (for reconstructing all that).*) -fun resetCalcHead (cI:calcID) = +fun resetCalcHead (cI:calcID) = (let val (ptp,_) = get_calc cI val ptp = reset_calchead ptp - in (upd_calc cI (ptp, []); + in (upd_calc cI (ptp, []); modifycalcheadOK2xml cI (get_ocalhd ptp)) end) handle _ => sysERROR2xml cI "error in kernel"; -(*.at the activeFormula insert all the Descriptions in the Model +(*.at the activeFormula insert all the Descriptions in the Model (_not_ in the Guard) and return a CalcHead; - the Descriptions are for user-guidance; the rest of the items - are left empty for user-input; + the Descriptions are for user-guidance; the rest of the items + are left empty for user-input; includes a resetCalcHead for the Model and the Guard.*) -fun modelProblem (cI:calcID) = +fun modelProblem (cI:calcID) = (let val (ptp, _) = get_calc cI val ptp = reset_calchead ptp val (_, _, ptp) = nxt_specif Model_Problem ptp - in (upd_calc cI (ptp, []); + in (upd_calc cI (ptp, []); modifycalcheadOK2xml cI (get_ocalhd ptp)) end) handle _ => sysERROR2xml cI "error in kernel"; (* set the UContext determined on a knowledgebrowser to the current calc *) fun setContext (cI:calcID) (ip as (_,p_):pos') (guh:guh) = - (case (implode o (take_fromto 1 4) o Symbol.explode) guh of + (case (implode o (take_fromto 1 4) o Symbol.explode) guh of "thy_" => if member op = [Pbl,Met] p_ then message2xml cI "thy-context not to calchead" else if ip = ([],Res) then message2xml cI "no thy-context at result" else if no_thycontext guh then message2xml cI ("no thy-context for '" ^ guh ^ "'") - else + else let val (ptp as (pt, pold), _) = get_calc cI val is = get_istate pt ip val subs = subs_from is "dummy" guh val tac = guh2rewtac guh subs - in + in case locatetac tac (pt, ip) of (*='fun setNextTactic'+step*) ("ok", (tacis, c, ptp as (_,p))) => - (upd_calc cI ((pt,p), []); + (upd_calc cI ((pt,p), []); autocalculateOK2xml cI pold (if null c then pold else last_elem c) p) | ("unsafe-ok", (tacis, c, ptp as (_,p))) => - (upd_calc cI ((pt,p), []); + (upd_calc cI ((pt,p), []); autocalculateOK2xml cI pold (if null c then pold else last_elem c) p) | ("end-of-calculation",_) => message2xml cI "end-of-calculation" | ("failure",_) => sysERROR2xml cI "failure" | ("not-applicable",_) => (*the rule comes from anywhere..*) - (case applicable_in ip pt tac of + (case applicable_in ip pt tac of Notappl e => message2xml cI ("'" ^ tac2str tac ^ "' not-applicable") - | Appl m => + | Appl m => let val ctxt = get_ctxt pt pold val (p,c,_,pt) = @@ -433,7 +433,7 @@ val pI = guh2kestoreID guh val ((pt, _), _) = get_calc cI in - if member op = [Pbl, Met] p_ + if member op = [Pbl, Met] p_ then let val (pt, chd) = set_problem pI (pt, ip) in (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end @@ -456,12 +456,12 @@ (*.specify the Method at the activeFormula and return a CalcHead containing the Guard. WN0512 impl.incomplete, see 'nxt_specif (Specify_Method '.*) -fun setMethod (cI:calcID) (mI:metID) = +fun setMethod (cI:calcID) (mI:metID) = (* val (cI, mI) = (1, ["Test","solve_linear"]); *) (let val ((pt, _), _) = get_calc cI val ip as (_, p_) = get_pos cI 1 - in if member op = [Pbl,Met] p_ + in if member op = [Pbl,Met] p_ then let val (pt, chd) = set_method mI (pt, ip) in (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end @@ -500,7 +500,7 @@ (**. without update of CalcTree .**) -(*.match the model of a problem at pos p +(*.match the model of a problem at pos p with the model-pattern of the problem with pblID*) (*fun tryMatchProblem cI pblID = (let val ((pt,_),_) = get_calc cI @@ -521,7 +521,7 @@ handle _ => sysERROR2xml cI "error in kernel"; (* append a formula to the calculation *) -fun appendFormula cI (ifo:cterm') = +fun appendFormula' cI (ifo:cterm') = (let val cs = get_calc cI val pos as (_,p_) = get_pos cI 1 @@ -540,6 +540,8 @@ end) handle _ => sysERROR2xml cI "error in kernel"; +fun appendFormula cI ifo = Future.fork (fn () => appendFormula' cI ifo); + (* replace a formula with_in_ a calculation; this situation applies for initial CAS-commands, too *) fun replaceFormula cI (ifo:cterm') = @@ -671,7 +673,7 @@ handle _ => sysERROR2xml cI "error in kernel"; -(*.initContext Thy_ is conceptually impossible at [Pbl,Met] +(*.initContext Thy_ is conceptually impossible at [Pbl,Met] and at positions with Check_Postcond and End_Trans; at possible pos's there can be NO rewrite (returned as a context, too).*) (* val (cI, Thy_, (pos as (p,p_):pos')) = (1, Thy_, ([1], Frm)); @@ -687,7 +689,7 @@ in if exist_lev_on' pt pos then let val pos' = lev_on' pt pos val tac = get_tac_checked pt pos' - in if is_rewtac tac + in if is_rewtac tac then contextthyOK2xml cI (context_thy (pt,pos) tac) else message2xml cI ("no thy-context at tac '" ^ tac2str tac ^ "'") @@ -699,8 +701,8 @@ *) ("ok", (tacis, _, (pt,_))) => let val tac = fst3 (last_elem tacis) - in if is_rewtac tac - then contextthyOK2xml + in if is_rewtac tac + then contextthyOK2xml cI (context_thy ptp tac) else message2xml cI ("no thy-context at tac '" ^ tac2str tac ^ "'") @@ -712,7 +714,7 @@ (* val (cI, Pbl_, pos as (p,p_)) = (1, Pbl_, ([],Pbl)); *) - | initContext cI Pbl_ (pos as (p,p_):pos') = + | initContext cI Pbl_ (pos as (p,p_):pos') = ((let val ((pt,_),_) = get_calc cI val pp = par_pblobj pt p val chd = initcontext_pbl pt (pp,p_) @@ -748,8 +750,8 @@ val subs = subs_from is "dummy" guh val tac = guh2rewtac guh subs in contextthyOK2xml cI (context_thy (pt, pos) tac) end - - (*.match the model of a problem at pos p + + (*.match the model of a problem at pos p with the model-pattern of the problem with pblID.*) (* val (cI, pos:pos' as (p,p_), guh) = (1, p, kestoreID2guh Pbl_ ["univariate","equation"]); @@ -758,16 +760,16 @@ val (cI, pos:pos' as (p,p_), guh) = (1, ([],Pbl), "pbl_equ_univ"); *) - | "pbl_" => + | "pbl_" => let val ((pt,_),_) = get_calc cI val pp = par_pblobj pt p val keID = guh2kestoreID guh val chd = context_pbl keID pt pp in matchpbl2xml cI chd end -(* val (cI, pos:pos' as (p,p_), guh) = +(* val (cI, pos:pos' as (p,p_), guh) = (1, ([],Pbl), kestoreID2guh Met_ ["LinEq", "solve_lineq_equation"]); *) - | "met_" => + | "met_" => let val ((pt,_),_) = get_calc cI val pp = par_pblobj pt p val keID = guh2kestoreID guh @@ -775,9 +777,9 @@ in matchmet2xml cI chd end) handle _ => sysERROR2xml cI "error in kernel"; -(* for an errpatID find "(fillpatID, fillform)" list +(* for an errpatID find "(fillpatID, fillform)" list which dedicated to this errpat and which is applicable at current formula*) -fun findFillpatterns cI errpatID = +fun findFillpatterns cI errpatID = let val ((pt, _), _) = get_calc cI val pos = get_pos cI 1; @@ -794,9 +796,9 @@ let val ((pt, _), _) = get_calc cI val pos = get_pos cI 1 - val fillforms = find_fillpatterns (pt, pos) errpatID + val fillforms = find_fillpatterns (pt, pos) errpatID in - case filter ((curry op = fillpatID) o + case filter ((curry op = fillpatID) o (#1: (fillpatID * term * thm * (subs option) -> fillpatID))) fillforms of (_, fillform, thm, sube_opt) :: _ => let @@ -806,8 +808,8 @@ (upd_calc cI ((pt, pos'), []); (*upd_ipos cI 1 pos';*) autocalculateOK2xml cI pos pos' pos') end - | _ => autocalculateERROR2xml cI "no fillpattern found" - end; + | _ => autocalculateERROR2xml cI "no fillpattern found" + end; (* input a formula which exactly fills the gaps in a "fillformula" presented to the learner immediately before by "requestFillformula (errpatID, fillpatID)": diff -r 7961cffaafcf -r d580d7fc9b8e test/Tools/isac/Frontend/use-cases.sml --- a/test/Tools/isac/Frontend/use-cases.sml Sat Mar 08 11:07:52 2014 +0100 +++ b/test/Tools/isac/Frontend/use-cases.sml Mon Mar 10 21:07:35 2014 +0100 @@ -1128,7 +1128,7 @@ autoCalculate 1 CompleteCalcHead; autoCalculate 1 (Step 1); autoCalculate 1 (Step 1); - appendFormula 1 "-1 + x = 0"; + appendFormula 1 "-1 + x = 0" |> Future.join; (*... returns calcChangedEvent with*) val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res)); getFormulaeFromTo 1 unc gen 99999 (*all levels*) false; @@ -1151,7 +1151,7 @@ autoCalculate 1 CompleteCalcHead; autoCalculate 1 (Step 1); autoCalculate 1 (Step 1); - appendFormula 1 "x - 1 = 0"; + appendFormula 1 "x - 1 = 0" |> Future.join; val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res)); getFormulaeFromTo 1 unc gen 99999 (*all levels*) false; (*11 elements !!!*) @@ -1174,7 +1174,7 @@ autoCalculate 1 CompleteCalcHead; autoCalculate 1 (Step 1); autoCalculate 1 (Step 1); - appendFormula 1 "x = 1"; + appendFormula 1 "x = 1" |> Future.join; (*... returns calcChangedEvent with*) val (unc, del, gen) = (([1],Res), ([1],Res), ([3,2],Res)); getFormulaeFromTo 1 unc gen 99999 (*all levels*) false; @@ -1198,7 +1198,7 @@ autoCalculate 1 CompleteCalcHead; autoCalculate 1 (Step 1); autoCalculate 1 (Step 1); - appendFormula 1 "x - 4711 = 0"; + appendFormula 1 "x - 4711 = 0" |> Future.join; (*... returns no derivation found *) val ((pt,_),_) = get_calc 1; @@ -1354,7 +1354,7 @@ autoCalculate 1 CompleteCalcHead; autoCalculate 1 (Step 1); autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*) -appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)"; (*<<<<<<<=========================*) +appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)" |> Future.join; (*<<<<<<<=========================*) (* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"), would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well. results in error pattern #chain-rule-diff-both# @@ -1434,7 +1434,7 @@ replaceFormula 1 "Simplify (5 * x / (4 * y) + 3 * x / (4 * y))"; autoCalculate 1 CompleteCalcHead; autoCalculate 1 (Step 1); -appendFormula 1 "8 * x / (8 * y)"; +appendFormula 1 "8 * x / (8 * y)" |> Future.join; (* no derivation found --- but in BridgeLog Java <=> SML: error pattern #addition-of-fractions# *) diff -r 7961cffaafcf -r d580d7fc9b8e test/Tools/isac/Interpret/generate.sml --- a/test/Tools/isac/Interpret/generate.sml Sat Mar 08 11:07:52 2014 +0100 +++ b/test/Tools/isac/Interpret/generate.sml Mon Mar 10 21:07:35 2014 +0100 @@ -23,7 +23,7 @@ autoCalculate 1 CompleteCalcHead; autoCalculate 1 (Step 1); autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*) -appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)"; +appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)" |> Future.join; (* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"), would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well. results in error pattern #chain-rule-diff-both# diff -r 7961cffaafcf -r d580d7fc9b8e test/Tools/isac/Interpret/inform.sml --- a/test/Tools/isac/Interpret/inform.sml Sat Mar 08 11:07:52 2014 +0100 +++ b/test/Tools/isac/Interpret/inform.sml Mon Mar 10 21:07:35 2014 +0100 @@ -60,7 +60,7 @@ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*) autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*); - appendFormula 1 "-2 * 1 + (1 + x) = 0"; refFormula 1 (get_pos 1 1); + appendFormula 1 "-2 * 1 + (1 + x) = 0" |> Future.join; refFormula 1 (get_pos 1 1); val ((pt,_),_) = get_calc 1; val str = pr_ptree pr_short pt; if str = @@ -143,7 +143,7 @@ Iterator 1; moveActiveRoot 1; autoCalculate 1 CompleteCalcHead; autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*x + 1 = 2*); - appendFormula 1 "2+ -1 + x = 2"; refFormula 1 (get_pos 1 1); + appendFormula 1 "2+ -1 + x = 2" |> Future.join; refFormula 1 (get_pos 1 1); moveDown 1 ([],Pbl); refFormula 1 ([1],Frm) (*x + 1 = 2*); @@ -180,7 +180,7 @@ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*) autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*); - appendFormula 1 "x = 2"; + appendFormula 1 "x = 2" |> Future.join; val ((pt,p),_) = get_calc 1; val str = pr_ptree pr_short pt; writeln str; @@ -210,7 +210,7 @@ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*) autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*); - appendFormula 1 "x = 1"; + appendFormula 1 "x = 1" |> Future.join; val ((pt,p),_) = get_calc 1; val str = pr_ptree pr_short pt; writeln str; @@ -239,7 +239,7 @@ autoCalculate 1 CompleteCalcHead; autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*) autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*); - appendFormula 1 "[x = 3 + -2*1]"; + appendFormula 1 "[x = 3 + -2*1]" |> Future.join; val ((pt,p),_) = get_calc 1; val str = pr_ptree pr_short pt; writeln str; @@ -525,7 +525,7 @@ (([1], Res), a / b + c / d + e / f)] *) "--- (1) input an arbitrary next formula"; -appendFormula 1 "((a * d) + (c * b)) / (b * d) + e / f"; +appendFormula 1 "((a * d) + (c * b)) / (b * d) + e / f" |> Future.join; val ((pt, p), _) = get_calc 1; (*show_pt pt; [ @@ -556,7 +556,7 @@ (([2], Res), (a * d + c * b) / (b * d) + e / f), (([3], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f))] <--- input this *) -appendFormula 1 "(b * d * e + b * c * f + a * d * f) / (b * d * f)"; +appendFormula 1 "(b * d * e + b * c * f + a * d * f) / (b * d * f)" |> Future.join; val ((pt, p), _) = get_calc 1; (*show_pt pt; [ @@ -573,7 +573,7 @@ else error ("inform.sml: [rational,simplification] 2"); "--- (3) input the exact final result"; -appendFormula 1 "(b * d * e + b * c * f + a * d * f) / (b * d * f)"; +appendFormula 1 "(b * d * e + b * c * f + a * d * f) / (b * d * f)" |> Future.join; val ((pt, p), _) = get_calc 1; (*show_pt pt; [ @@ -1119,7 +1119,7 @@ autoCalculate 1 CompleteCalcHead; autoCalculate 1 (Step 1); autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*) -appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)"; +appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)" |> Future.join; (* error pattern #chain-rule-diff-both# *) (*or no derivation found *) @@ -1201,7 +1201,7 @@ autoCalculate 1 CompleteCalcHead; autoCalculate 1 (Step 1); autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*) -appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)"; (*<<<<<<<=========================*) +appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)" |> Future.join; (*<<<<<<<=========================*) (* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"), would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well. results in error pattern #chain-rule-diff-both# diff -r 7961cffaafcf -r d580d7fc9b8e test/Tools/isac/Knowledge/diff.sml --- a/test/Tools/isac/Knowledge/diff.sml Sat Mar 08 11:07:52 2014 +0100 +++ b/test/Tools/isac/Knowledge/diff.sml Mon Mar 10 21:07:35 2014 +0100 @@ -464,7 +464,7 @@ autoCalculate 1 (Step 1); autoCalculate 1 (Step 1); val ((pt,p),_) = get_calc 1; show_pt pt; -appendFormula 1 "2*x + d_d x x + d_d x 1"; +appendFormula 1 "2*x + d_d x x + d_d x 1" |> Future.join; val ((pt,p),_) = get_calc 1; show_pt pt; if existpt' ([3], Res) pt then () else error "diff.sml: inform d_d x (x^2 + x + 1) doesnt work"; diff -r 7961cffaafcf -r d580d7fc9b8e test/Tools/isac/Knowledge/simplify.sml --- a/test/Tools/isac/Knowledge/simplify.sml Sat Mar 08 11:07:52 2014 +0100 +++ b/test/Tools/isac/Knowledge/simplify.sml Mon Mar 10 21:07:35 2014 +0100 @@ -59,7 +59,7 @@ (([], Frm), Simplify (14 * x * y / (x * y))), (([1], Frm), 14 * x * y / (x * y))] *) -appendFormula 1 "14"; +appendFormula 1 "14" |> Future.join; val ((pt,p),_) = get_calc 1; show_pt pt; (*[ (([], Frm), Simplify (14 * x * y / (x * y))),