1.1 --- a/src/Tools/isac/Frontend/interface.sml Mon May 18 13:22:43 2015 +0200
1.2 +++ b/src/Tools/isac/Frontend/interface.sml Mon May 18 14:08:09 2015 +0200
1.3 @@ -15,8 +15,8 @@
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 future
1.8 - val autoCalculate : calcID -> auto -> unit future
1.9 + val appendFormula : calcID -> cterm' -> unit (*future*)
1.10 + val autoCalculate : calcID -> auto -> unit (*future*)
1.11 val checkContext : calcID -> pos' -> guh -> unit
1.12 val fetchApplicableTactics : calcID -> int -> pos' -> unit
1.13 val fetchProposedTactic : calcID -> unit
1.14 @@ -202,8 +202,8 @@
1.15 | CompleteSubpbl (*5 complete the actual (sub)problem (incl.ev.subproblems)*)
1.16 | CompleteCalc; (*6 complete the calculation as a whole*)*)
1.17
1.18 -fun autoCalculate (cI:calcID) auto = Future.fork
1.19 - (fn () => ((let
1.20 +fun autoCalculate (cI:calcID) auto = (*Future.fork
1.21 + (fn () => (( *)let
1.22 val pold = get_pos cI 1
1.23 val x = autocalc [] pold (get_calc cI) auto
1.24 in
1.25 @@ -215,8 +215,8 @@
1.26 (upd_calc cI (ptp, []); upd_ipos cI 1 p;
1.27 autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)
1.28 | (str, _, _) => autocalculateERROR2xml cI str
1.29 - end)
1.30 - handle ERROR msg => sysERROR2xml cI ("error in kernel: " ^ msg)));
1.31 + end (* ) *)
1.32 + handle ERROR msg => sysERROR2xml cI ("error in kernel: " ^ msg)(* )) *);
1.33
1.34
1.35 (* val (cI:calcID, ichd as ((p,_),_,_,_,_):icalhd) =
1.36 @@ -531,7 +531,7 @@
1.37 end)
1.38 handle ERROR msg => sysERROR2xml cI ("error in kernel: " ^ msg);
1.39
1.40 -fun appendFormula cI ifo = Future.fork (fn () => appendFormula' cI ifo);
1.41 +fun appendFormula cI ifo = (*Future.fork (fn () => *)appendFormula' cI ifo(* ) *);
1.42
1.43 (* replace a formula with_in_ a calculation;
1.44 this situation applies for initial CAS-commands, too *)
2.1 --- a/test/Tools/isac/Frontend/states.sml Mon May 18 13:22:43 2015 +0200
2.2 +++ b/test/Tools/isac/Frontend/states.sml Mon May 18 14:08:09 2015 +0200
2.3 @@ -33,7 +33,7 @@
2.4 val ls = gen_ls n |> map add_calc;
2.5 fun auto_calc i = autoCalculate i CompleteCalc;
2.6 val t1 = Time.now ();
2.7 - val _ = map auto_calc ls |> map Future.join;
2.8 + val _ = map auto_calc ls (*|> map Future.join*);
2.9 val t2 = Time.now ();
2.10 fun check i = let
2.11 val ((pt, p), _) = get_calc i; (*retrieve result, e.g. no.1*)
3.1 --- a/test/Tools/isac/Frontend/use-cases.sml Mon May 18 13:22:43 2015 +0200
3.2 +++ b/test/Tools/isac/Frontend/use-cases.sml Mon May 18 14:08:09 2015 +0200
3.3 @@ -1128,7 +1128,7 @@
3.4 autoCalculate' 1 CompleteCalcHead;
3.5 autoCalculate' 1 (Step 1);
3.6 autoCalculate' 1 (Step 1);
3.7 - appendFormula 1 "-1 + x = 0" |> Future.join;
3.8 + appendFormula 1 "-1 + x = 0" (*|> Future.join*);
3.9 (*... returns calcChangedEvent with*)
3.10 val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res));
3.11 getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
3.12 @@ -1151,7 +1151,7 @@
3.13 autoCalculate' 1 CompleteCalcHead;
3.14 autoCalculate' 1 (Step 1);
3.15 autoCalculate' 1 (Step 1);
3.16 - appendFormula 1 "x - 1 = 0" |> Future.join;
3.17 + appendFormula 1 "x - 1 = 0" (*|> Future.join*);
3.18 val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res));
3.19 getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
3.20 (*11 elements !!!*)
3.21 @@ -1174,7 +1174,7 @@
3.22 autoCalculate' 1 CompleteCalcHead;
3.23 autoCalculate' 1 (Step 1);
3.24 autoCalculate' 1 (Step 1);
3.25 - appendFormula 1 "x = 1" |> Future.join;
3.26 + appendFormula 1 "x = 1" (*|> Future.join*);
3.27 (*... returns calcChangedEvent with*)
3.28 val (unc, del, gen) = (([1],Res), ([1],Res), ([3,2],Res));
3.29 getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
3.30 @@ -1198,7 +1198,7 @@
3.31 autoCalculate' 1 CompleteCalcHead;
3.32 autoCalculate' 1 (Step 1);
3.33 autoCalculate' 1 (Step 1);
3.34 - appendFormula 1 "x - 4711 = 0" |> Future.join;
3.35 + appendFormula 1 "x - 4711 = 0" (*|> Future.join*);
3.36 (*... returns <ERROR> no derivation found </ERROR>*)
3.37
3.38 val ((pt,_),_) = get_calc 1;
3.39 @@ -1354,7 +1354,7 @@
3.40 autoCalculate' 1 CompleteCalcHead;
3.41 autoCalculate' 1 (Step 1);
3.42 autoCalculate' 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
3.43 -appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)" |> Future.join; (*<<<<<<<=========================*)
3.44 +appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)" (*|> Future.join*); (*<<<<<<<=========================*)
3.45 (* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),
3.46 would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well.
3.47 results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>
3.48 @@ -1435,7 +1435,7 @@
3.49 replaceFormula 1 "Simplify (5 * x / (4 * y) + 3 * x / (4 * y))";
3.50 autoCalculate' 1 CompleteCalcHead;
3.51 autoCalculate' 1 (Step 1);
3.52 -appendFormula 1 "8 * x / (8 * y)" |> Future.join;
3.53 +appendFormula 1 "8 * x / (8 * y)" (*|> Future.join*);
3.54 (*<CALCMESSAGE> no derivation found </CALCMESSAGE>
3.55 --- but in BridgeLog Java <=> SML:
3.56 <CALCMESSAGE> error pattern #addition-of-fractions# </CALCMESSAGE>*)
4.1 --- a/test/Tools/isac/Interpret/generate.sml Mon May 18 13:22:43 2015 +0200
4.2 +++ b/test/Tools/isac/Interpret/generate.sml Mon May 18 14:08:09 2015 +0200
4.3 @@ -23,7 +23,7 @@
4.4 autoCalculate' 1 CompleteCalcHead;
4.5 autoCalculate' 1 (Step 1);
4.6 autoCalculate' 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
4.7 -appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)" |> Future.join;
4.8 +appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)" (*|> Future.join*);
4.9 (* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),
4.10 would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well.
4.11 results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>
5.1 --- a/test/Tools/isac/Interpret/inform.sml Mon May 18 13:22:43 2015 +0200
5.2 +++ b/test/Tools/isac/Interpret/inform.sml Mon May 18 14:08:09 2015 +0200
5.3 @@ -60,7 +60,7 @@
5.4 autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
5.5 autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
5.6
5.7 - appendFormula 1 "-2 * 1 + (1 + x) = 0" |> Future.join; refFormula 1 (get_pos 1 1);
5.8 + appendFormula 1 "-2 * 1 + (1 + x) = 0" (*|> Future.join*); refFormula 1 (get_pos 1 1);
5.9 val ((pt,_),_) = get_calc 1;
5.10 val str = pr_ptree pr_short pt;
5.11 if str =
5.12 @@ -143,7 +143,7 @@
5.13 Iterator 1; moveActiveRoot 1;
5.14 autoCalculate' 1 CompleteCalcHead;
5.15 autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1) (*x + 1 = 2*);
5.16 - appendFormula 1 "2+ -1 + x = 2" |> Future.join; refFormula 1 (get_pos 1 1);
5.17 + appendFormula 1 "2+ -1 + x = 2" (*|> Future.join*); refFormula 1 (get_pos 1 1);
5.18
5.19 moveDown 1 ([],Pbl); refFormula 1 ([1],Frm) (*x + 1 = 2*);
5.20
5.21 @@ -180,7 +180,7 @@
5.22 autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
5.23 autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
5.24
5.25 - appendFormula 1 "x = 2" |> Future.join;
5.26 + appendFormula 1 "x = 2" (*|> Future.join*);
5.27 val ((pt,p),_) = get_calc 1;
5.28 val str = pr_ptree pr_short pt;
5.29 writeln str;
5.30 @@ -210,7 +210,7 @@
5.31 autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
5.32 autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
5.33
5.34 - appendFormula 1 "x = 1" |> Future.join;
5.35 + appendFormula 1 "x = 1" (*|> Future.join*);
5.36 val ((pt,p),_) = get_calc 1;
5.37 val str = pr_ptree pr_short pt;
5.38 writeln str;
5.39 @@ -239,7 +239,7 @@
5.40 autoCalculate' 1 CompleteCalcHead;
5.41 autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
5.42 autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
5.43 - appendFormula 1 "[x = 3 + -2*1]" |> Future.join;
5.44 + appendFormula 1 "[x = 3 + -2*1]" (*|> Future.join*);
5.45 val ((pt,p),_) = get_calc 1;
5.46 val str = pr_ptree pr_short pt;
5.47 writeln str;
5.48 @@ -525,7 +525,7 @@
5.49 (([1], Res), a / b + c / d + e / f)]
5.50 *)
5.51 "--- (1) input an arbitrary next formula";
5.52 -appendFormula 1 "((a * d) + (c * b)) / (b * d) + e / f" |> Future.join;
5.53 +appendFormula 1 "((a * d) + (c * b)) / (b * d) + e / f" (*|> Future.join*);
5.54 val ((pt, p), _) = get_calc 1;
5.55 (*show_pt pt;
5.56 [
5.57 @@ -556,7 +556,7 @@
5.58 (([2], Res), (a * d + c * b) / (b * d) + e / f),
5.59 (([3], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f))] <--- input this
5.60 *)
5.61 -appendFormula 1 "(b * d * e + b * c * f + a * d * f) / (b * d * f)" |> Future.join;
5.62 +appendFormula 1 "(b * d * e + b * c * f + a * d * f) / (b * d * f)" (*|> Future.join*);
5.63 val ((pt, p), _) = get_calc 1;
5.64 (*show_pt pt;
5.65 [
5.66 @@ -573,7 +573,7 @@
5.67 else error ("inform.sml: [rational,simplification] 2");
5.68
5.69 "--- (3) input the exact final result";
5.70 -appendFormula 1 "(b * d * e + b * c * f + a * d * f) / (b * d * f)" |> Future.join;
5.71 +appendFormula 1 "(b * d * e + b * c * f + a * d * f) / (b * d * f)" (*|> Future.join*);
5.72 val ((pt, p), _) = get_calc 1;
5.73 (*show_pt pt;
5.74 [
5.75 @@ -1119,7 +1119,7 @@
5.76 autoCalculate' 1 CompleteCalcHead;
5.77 autoCalculate' 1 (Step 1);
5.78 autoCalculate' 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
5.79 -appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)" |> Future.join;
5.80 +appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)" (*|> Future.join*);
5.81 (*<CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>*)
5.82 (*or
5.83 <CALCMESSAGE> no derivation found </CALCMESSAGE>*)
5.84 @@ -1201,7 +1201,7 @@
5.85 autoCalculate' 1 CompleteCalcHead;
5.86 autoCalculate' 1 (Step 1);
5.87 autoCalculate' 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
5.88 -appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)" |> Future.join; (*<<<<<<<=========================*)
5.89 +appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)" (*|> Future.join*); (*<<<<<<<=========================*)
5.90 (* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),
5.91 would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well.
5.92 results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>
6.1 --- a/test/Tools/isac/Interpret/mathengine.sml Mon May 18 13:22:43 2015 +0200
6.2 +++ b/test/Tools/isac/Interpret/mathengine.sml Mon May 18 14:08:09 2015 +0200
6.3 @@ -693,7 +693,7 @@
6.4 val cs = get_calc cI (* we improve from the calcstate here [*] *);
6.5 val pos as (_,p_) = get_pos cI 1 (* we improve from the calcstate here [*] *);
6.6
6.7 -appendFormula 1 "x + 4 + -3 = 2" |> Future.join;
6.8 +appendFormula 1 "x + 4 + -3 = 2" (*|> Future.join*);
6.9 interSteps 1 ([1],Res); (* already done by appendFormula, now showed to frontend *)
6.10 getTactic 1 ([1,1], Res);
6.11 (*<ID> sym_#add_Float ((~3,0), (0,0)) __ ((4,0), (0,0)) </ID> <<<<<================== to improve
7.1 --- a/test/Tools/isac/Knowledge/diff.sml Mon May 18 13:22:43 2015 +0200
7.2 +++ b/test/Tools/isac/Knowledge/diff.sml Mon May 18 14:08:09 2015 +0200
7.3 @@ -464,7 +464,7 @@
7.4 autoCalculate' 1 (Step 1);
7.5 autoCalculate' 1 (Step 1);
7.6 val ((pt,p),_) = get_calc 1; show_pt pt;
7.7 -appendFormula 1 "2*x + d_d x x + d_d x 1" |> Future.join;
7.8 +appendFormula 1 "2*x + d_d x x + d_d x 1" (*|> Future.join*);
7.9 val ((pt,p),_) = get_calc 1; show_pt pt;
7.10 if existpt' ([3], Res) pt then ()
7.11 else error "diff.sml: inform d_d x (x^2 + x + 1) doesnt work";
8.1 --- a/test/Tools/isac/Knowledge/simplify.sml Mon May 18 13:22:43 2015 +0200
8.2 +++ b/test/Tools/isac/Knowledge/simplify.sml Mon May 18 14:08:09 2015 +0200
8.3 @@ -59,7 +59,7 @@
8.4 (([], Frm), Simplify (14 * x * y / (x * y))),
8.5 (([1], Frm), 14 * x * y / (x * y))] *)
8.6
8.7 -appendFormula 1 "14" |> Future.join;
8.8 +appendFormula 1 "14" (*|> Future.join*);
8.9 val ((pt,p),_) = get_calc 1; show_pt pt;
8.10 (*[
8.11 (([], Frm), Simplify (14 * x * y / (x * y))),
9.1 --- a/test/Tools/isac/Test_Isac.thy Mon May 18 13:22:43 2015 +0200
9.2 +++ b/test/Tools/isac/Test_Isac.thy Mon May 18 14:08:09 2015 +0200
9.3 @@ -44,7 +44,7 @@
9.4
9.5 ML {*
9.6 KEStore_Elems.set_ref_thy @{theory};
9.7 - fun autoCalculate' cI auto = autoCalculate cI auto |> Future.join;
9.8 + fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*);
9.9 *}
9.10
9.11 section {* trials with Isabelle's functions *}