1 (* Title: \<open>\<close>
2 Author: Walther Neuper 061019
3 (c) due to copyright terms
6 "--------------------------------------------------------";
7 "--------------------------------------------------------";
8 "table of contents --------------------------------------";
9 "--------------------------------------------------------";
10 (*"----------- CAS-command Simplify -----------------------";*)
11 "----------- append inform with final result ------------";
12 "--------------------------------------------------------";
13 "--------------------------------------------------------";
14 "--------------------------------------------------------";
16 val thy = @{theory "Simplify"};
19 This test is postponed within Isabelle/PIDE/isac development,
20 because respective user-requirements are not clarified.
21 See test/../cas-command.sml --- start Calculation with CAS_Cmd ---
22 and test/../Test_VSCode_Example.thy subsubsection \<open>Start Example with a CAS_Cmd\<close>
23 "----------- CAS-command Simplify -----------------------";
24 "----------- CAS-command Simplify -----------------------";
25 "----------- CAS-command Simplify -----------------------";
27 CalcTree [([], References.empty)];
30 replaceFormula 1 "Simplify (2*a + 3*a)";
31 autoCalculate 1 (Steps 1);
32 autoCalculate 1 CompleteCalc;
33 val ((pt,p),_) = States.get_calc 1;
34 val Form res = (#1 o ME_Misc.pt_extract) (pt, ([],Res)); Test_Tool.show_pt pt; UnparseC.term res;
35 if p = ([], Res) andalso UnparseC.term res = "5 * a" then ()
36 else error "simplify.sml: diff.behav. CAScmd: Simplify (2*a + 3*a)";
39 "----------- append inform with final result ------------";
40 "----------- append inform with final result ------------";
41 "----------- append inform with final result ------------";
43 CalcTree [(["Term ((14 * x * y) / ( x * y ))", "normalform N"],
44 ("Rational", ["rational", "simplification"], ["simplification", "of_rationals"]))];
47 autoCalculate 1 CompleteCalcHead;
48 val ((pt,p),_) = States.get_calc 1;
49 Test_Tool.show_pt pt; (*[
50 (([], Frm), Simplify (14 * x * y / (x * y)))] *)
51 ME_Misc.pt_extract (pt, p); (*determines SOME (Apply_Method ["simplification", "of_rationals"])*)
53 (*/------------------- step into autoCalculate 1 (Steps 1) \<longrightarrow> Apply_Method ----------------\*)
54 "~~~~~ fun autoCalculate , args:"; val (cI, auto) = (1, Steps 1);
55 val pold = States.get_pos cI 1
57 (** )val ("ok", [], (_, ([], Met))) = (*case*) ( *isa*)
58 (**)val ("ok", [], (_, ([1], Frm))) = (*case*) (*isa2*)
59 Math_Engine.autocalc [] pold (States.get_calc cI) auto (*of*);
60 "~~~~~ fun autocalc , args:"; val (c, ip, cs, (Solve.Steps s)) = ([], pold, (States.get_calc cI), auto);
61 (*if*) s <= 1 (*then*);
63 (** ) val ("ok", ( (*isa*)
64 [(Specify_Method ["simplification", "of_rationals"], _, (([], Met), (Uistate, _)))],
65 [], (_, ([], Met)))) = ( **)
66 (**) val ("ok", ( (*isa2*)
67 [(Apply_Method ["simplification", "of_rationals"], _, (([1], Frm), (pstate, _)))],
68 [], (_, ([1], Frm)))) = (**)
70 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (ip, cs);
71 (*if*) Pos.on_calc_end ip (*else*);
72 val ("Rational", probl_id as ["rational", "simplification"], ["simplification", "of_rationals"]) =
73 Calc.references (pt, p); (*isa == isa2*)
75 (*case*) tacis (*of*);
76 (*if*) probl_id = Problem.id_empty (*else*);
78 (** ) val ("ok", ( (*isa*)
79 [(Specify_Method ["simplification", "of_rationals"], _, (([], Met), (Uistate, _)))],
80 [], (_, ([], Met)))) = ( **)
81 (**) val ("ok", ( (*isa2*)
82 [(Apply_Method ["simplification", "of_rationals"], _, (([1], Frm), (pstate, _)))],
83 [], (_, ([1], Frm)))) = (**)
84 switch_specify_solve p_ (pt, ip);
85 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
86 (*if*) Pos.on_specification ([], state_pos) (*then*);
88 (** ) val ("ok", ( (*isa*)
89 [(Specify_Method ["simplification", "of_rationals"], _, (([], Met), (Uistate, _)))],
90 [], (_, ([], Met)))) = ( **)
91 (**) val ("ok", ( (*isa2*)
92 [(Apply_Method ["simplification", "of_rationals"], _, (([1], Frm), (pstate, _)))],
93 [], (_, ([1], Frm)))) = (**)
94 specify_do_next (pt, input_pos);
95 "~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
96 val (_, (p_', tac)) = Specify.find_next_step ptp
98 (** ) val (_, (Met, Specify_Method ["simplification", "of_rationals"])) = ( *isa*)
99 (**) val (_, (Met, Apply_Method ["simplification", "of_rationals"])) = (*isa2*)
100 Specify.find_next_step ptp;
101 "~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp);
102 val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
103 spec = refs, ...} = Calc.specify_data (pt, pos);
104 (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
105 (*if*) p_ = Pos.Pbl (*else*);
107 (** ) val (_, (Met, Specify_Method ["simplification", "of_rationals"])) = ( *isa*)
108 (**) val (_, (Met, Apply_Method ["simplification", "of_rationals"])) = (*isa2*)
109 for_method oris (o_refs, refs) (pbl, met);
110 "~~~~~ fun for_method , args:"; val (oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
111 (oris, (o_refs, refs), (pbl, met));
112 val cmI = if mI = MethodC.id_empty then mI' else mI;
113 val {ppc = mpc, prls, pre, ...} = MethodC.from_store cmI; (*..MethodC ?*)
115 (** ) val (preok as false, _) = Pre_Conds.check prls pre pbl 0; ( *isa*)
116 (**) val (preok as true, _) = Pre_Conds.check prls pre pbl 0; (*isa2*)
117 (*#### eval asms: "14 * x * y / (x * y) is_ratpolyexp = False" (*isa*)
119 (*\------------------- step into autoCalculate 1 (Steps 1) \<longrightarrow> Apply_Method ----------------/*)
120 val ((pt,p),_) = States.get_calc 1;
121 Test_Tool.show_pt pt;
123 (([], Frm), Simplify (14 * x * y / (x * y))),
124 (([1], Frm), 14 * x * y / (x * y))] *)
126 appendFormula 1 "14::real"
127 (* INPUT WITHOUT ^^^^^^^^ VARIABLES (WITH TYPE FROM ctxt) WOULD REQUIRE ADDITIONAL ATTENTION*);
128 val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
130 (([], Frm), Simplify (14 * x * y / (x * y))),
131 (([1], Frm), 14 * x * y / (x * y)),
132 (([1,1], Frm), 14 * x * y / (x * y)),
133 (([1,1], Res), 14 * (x * y) / (x * y)),
134 (([1,2], Res), 14 / 1),
138 autoCalculate 1 (Steps 1);
139 val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
141 (([], Frm), Simplify (14 * x * y / (x * y))),
142 (([1], Frm), 14 * x * y / (x * y)),
143 (([1,1], Frm), 14 * x * y / (x * y)),
144 (([1,1], Res), 14 * (x * y) / (x * y)),
145 (([1,2], Res), 14 / 1),
149 val Form res = (#1 o ME_Misc.pt_extract) (pt, ([],Res));
151 if p = ([], Res) andalso UnparseC.term res = "14" then ()
152 else error "simplify.sml: append inform with final result changed";