1.1 --- a/src/Tools/isac/Frontend/interface.sml Thu Oct 20 10:26:29 2016 +0200
1.2 +++ b/src/Tools/isac/Frontend/interface.sml Thu Oct 27 09:53:54 2016 +0200
1.3 @@ -132,11 +132,11 @@
1.4 *)
1.5 fun setNextTactic (cI:calcID) tac =
1.6 let
1.7 - val ((pt, _), _) = get_calc cI
1.8 - val ip = get_pos cI 1
1.9 + val ((pt, _), _) = get_calc cI (* retrieve calcstate from states *)
1.10 + val ip = get_pos cI 1 (* retrieve position from states *)
1.11 in case locatetac tac (pt, ip) of
1.12 - ("ok", (tacis, _, _)) =>
1.13 - (upd_calc cI ((pt, ip), tacis); setnexttactic2xml cI "ok")
1.14 + ("ok", (tacis, _, _)) => (* update calcstate in states *)
1.15 + (upd_calc cI ((pt, ip), tacis); setnexttactic2xml cI "ok")
1.16 | ("unsafe-ok", (tacis, _, _)) =>
1.17 (upd_calc cI ((pt, ip), tacis); setnexttactic2xml cI "unsafe-ok")
1.18 | ("not-applicable",_) => setnexttactic2xml cI "not-applicable"
2.1 --- a/src/Tools/isac/Frontend/states.sml Thu Oct 20 10:26:29 2016 +0200
2.2 +++ b/src/Tools/isac/Frontend/states.sml Thu Oct 27 09:53:54 2016 +0200
2.3 @@ -138,12 +138,14 @@
2.4 | is_detail _ _ _ = false;
2.5 ----------------------------------------*)
2.6
2.7 -val states = Synchronized.var "isac_states"
2.8 - ([]:(calcID *
2.9 - (calcstate *
2.10 - (iterID * (*1 sets the 'active formula'*)
2.11 - pos' (*for iterator of a user *)
2.12 - ) list)) list);
2.13 +(* holds calculations; these are read/updated from the java-frontend at each interaction*)
2.14 +val states = Synchronized.var "isac_states" ([] :
2.15 + (calcID * (* the id unique for a calculation *)
2.16 + (calcstate * (* the interpreter state *)
2.17 + (iterID * (* 1 sets the 'active formula': a calc. can have several visitors*)
2.18 + pos' (* for iterator of a user *)
2.19 + (* TODO iterID * pos' should go to java-frontend *)
2.20 + ) list)) list);
2.21
2.22 fun reset_states () = Synchronized.change states (fn _ => []);
2.23 (*
3.1 --- a/test/Tools/isac/Frontend/use-cases.sml Thu Oct 20 10:26:29 2016 +0200
3.2 +++ b/test/Tools/isac/Frontend/use-cases.sml Thu Oct 27 09:53:54 2016 +0200
3.3 @@ -619,7 +619,7 @@
3.4 autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.5 setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);
3.6 autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.7 - setNextTactic 1 (Rewrite ("all_left", @{thm all_left}));
3.8 + setNextTactic 1 (Rewrite ("all_left", num_str @{thm all_left}));
3.9 autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.10 setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "make_ratpoly_in"));
3.11 autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.12 @@ -1348,7 +1348,7 @@
3.13 val (Form f, tac, asms) = pt_extract (pt, p);
3.14 if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
3.15 error "FE-interface.sml: diff.behav. in FORMULA:replace} NOTok";
3.16 -DEconstrCalcTree 1;
3.17 + DEconstrCalcTree 1;
3.18
3.19 "--------- UC errpat chain-rule-diff-both, fillpat by input ------";
3.20 "--------- UC errpat chain-rule-diff-both, fillpat by input ------";
3.21 @@ -1370,12 +1370,11 @@
3.22 val p = get_pos 1 1;
3.23 val (Form f, _, asms) = pt_extract (pt, p);
3.24
3.25 - if p = ([2], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"
3.26 + if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"
3.27 then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(bdv, x)"],
3.28 ("diff_sum", thm)) => () | _ => error "embed fun get_fillform changed 0"
3.29 | _ => error "embed fun get_fillform changed 1"
3.30 else error "embed fun get_fillform changed 2";
3.31 -============ inhibit exn WN161019 TODO ========================================================*)
3.32
3.33 (*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ====================
3.34 findFillpatterns 1 "chain-rule-diff-both"; (*<<<<<<<=================================*)
3.35 @@ -1437,7 +1436,7 @@
3.36 "--------- UC errpat add-fraction, fillpat by input --------------";
3.37 "--------- UC errpat add-fraction, fillpat by input --------------";
3.38 (*cp from BridgeLog Java <=> SML*)
3.39 -=CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
3.40 +CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
3.41 Iterator 1;
3.42 moveActiveRoot 1;
3.43 moveActiveFormula 1 ([],Pbl);
3.44 @@ -1454,7 +1453,7 @@
3.45 "--------- UC errpat, fillpat step to Rewrite --------------------";
3.46 "--------- UC errpat, fillpat step to Rewrite --------------------";
3.47 (*TODO*)
3.48 -=CalcTree
3.49 +CalcTree
3.50 [(["functionTerm ((x ^ 2) ^ 3 + sin (x ^ 4))",
3.51 "differentiateFor x", "derivative f_f'"],
3.52 ("Isac", ["derivative_of","function"],