1 (* Title: tests on solve.sml
2 Author: Walther Neuper 060508,
3 (c) due to copyright terms
5 is NOT ONLY dependent on Test, but on other thys:
6 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
7 uses from Rational.ML: Rrls cancel_p, Rrls cancel
9 uses from Poly.ML: Rls make_polynomial, Rls expand_binom
12 default_print_depth 5;
13 trace_rewrite := false;
14 trace_script := false;
15 "-----------------------------------------------------------------";
16 "table of contents -----------------------------------------------";
17 "-----------------------------------------------------------------";
18 "--------- interSteps on norm_Rational ---------------------------";
19 (*/------- these test have been deleted, because "detail" is discontinued -------\
20 "###### val intermediate_ptyps = !ptyps; val intermediate_mets = !mets";
21 "--------- prepare pbl, met --------------------------------------";
22 "-------- cancel, without detail ------------------------------";
23 "-------- cancel, detail rev-rew (cancel) afterwards ----------";
24 "-------------- cancel_p, without detail ------------------------------";
25 "-------------- cancel_p, detail rev-rew (cancel) afterwards ----------";
26 (*---^^^ NOT working*)
27 "on 'miniscript with mini-subpbl':";
28 "------ interSteps'donesteps': on 'miniscript with mini-subpbl'---";
29 "------ interSteps'detailrls' after CompleteCalc -----------------";
30 "------ interSteps after appendFormula ---------------------------";
31 (*---vvv not brought to work 0403*)
32 "------ Detail_Set -----------------------------------------------";
33 "###### ptyps:= intermediate_ptyps; met:= intermediate_mets;#######";
34 \------- these test have been deleted, because "detail" is discontinued -------/*)
35 "-----------------------------------------------------------------";
36 "-----------------------------------------------------------------";
37 "-----------------------------------------------------------------";
39 val thy= @{theory Isac};
40 "--------- interSteps on norm_Rational ---------------------------";
41 "--------- interSteps on norm_Rational ---------------------------";
42 "--------- interSteps on norm_Rational ---------------------------";
43 reset_states (); (*exp_IsacCore_Simp_Rat_Double_No-7.xml*)
44 CalcTree [(["Term ((2/(x+3) + 2/(x - 3)) / (8*x/(x^2 - 9)))", "normalform N"],
45 ("Rational", ["rational","simplification"], ["simplification","of_rationals"]))];
47 autoCalculate 1 CompleteCalc;
48 val ((pt, _), _) = get_calc 1; show_pt pt;
49 case pt of Nd (PblObj _, [Nd _, Nd _, Nd _, Nd _, Nd _, Nd _]) => ()
50 | _ => error "solve.sml: interSteps on norm_Rational 1";
51 interSteps 1 ([6], Res);
53 getTactic 1 ([6,1], Frm) (*here get the tactic, and ...*);
54 interSteps 1 ([6,1], Res) (*... here get the intermediate steps above*);
56 getTactic 1 ([6,1,1], Frm); (*WN130909 <ERROR> syserror in getTactic </ERROR>*)
57 val ((pt,_),_) = get_calc 1; show_pt pt;
58 val (Form form, SOME tac, asm) = pt_extract (pt, ([6], Res));
59 case (term2str form, tac, terms2strs asm) of
60 ("1 / 2", Check_Postcond ["rational", "simplification"], []) => ()
61 | _ => error "solve.sml: interSteps on norm_Rational 2";
63 val (t, asm) = get_obj g_result pt [];
64 if terms2str asm = "[\"8 * x ~= 0\",\"-9 + x ^^^ 2 ~= 0\"," ^
65 "\"(2 / (x + 3) + 2 / (x - 3)) / (8 * x / (x ^^^ 2 - 9)) is_ratpolyexp\"]"
66 then () else error "solve.sml: interSteps on norm_Rational 2, asms";