1.1 --- a/test/Tools/isac/Interpret/solve.sml Mon Sep 16 11:28:43 2013 +0200
1.2 +++ b/test/Tools/isac/Interpret/solve.sml Mon Sep 16 12:20:00 2013 +0200
1.3 @@ -17,7 +17,7 @@
1.4 "-----------------------------------------------------------------";
1.5 "--------- interSteps on norm_Rational ---------------------------";
1.6 (*---vvv NOT working after meNEW.04mmdd*)
1.7 -"###### val intermediate_ptyps = !ptyps;val intermediate_mets = !mets";
1.8 +"###### val intermediate_ptyps = !ptyps; val intermediate_mets = !mets";
1.9 "--------- prepare pbl, met --------------------------------------";
1.10 "-------- cancel, without detail ------------------------------";
1.11 "-------- cancel, detail rev-rew (cancel) afterwards ----------";
1.12 @@ -30,7 +30,7 @@
1.13 "------ interSteps after appendFormula ---------------------------";
1.14 (*---vvv not brought to work 0403*)
1.15 "------ Detail_Set -----------------------------------------------";
1.16 -"###### ptyps:= intermediate_ptyps;met:= intermediate_mets;#######";
1.17 +"###### ptyps:= intermediate_ptyps; met:= intermediate_mets;#######";
1.18 "-----------------------------------------------------------------";
1.19 "-----------------------------------------------------------------";
1.20 "-----------------------------------------------------------------";
1.21 @@ -39,52 +39,30 @@
1.22 "--------- interSteps on norm_Rational ---------------------------";
1.23 "--------- interSteps on norm_Rational ---------------------------";
1.24 "--------- interSteps on norm_Rational ---------------------------";
1.25 - states:=[];(*exp_IsacCore_Simp_Rat_Double_No-7.xml*)
1.26 - CalcTree [(["Term ((2/(x+3) + 2/(x - 3)) / (8*x/(x^2 - 9)))","normalform N"],
1.27 - ("Rational",
1.28 - ["rational","simplification"],
1.29 - ["simplification","of_rationals"]))];
1.30 - moveActiveRoot 1;
1.31 - autoCalculate 1 CompleteCalc;
1.32 - val ((pt,_),_) = get_calc 1; show_pt pt;
1.33 -
1.34 -(*with "Script SimplifyScript (t_::real) = -----------------
1.35 - \ ((Rewrite_Set norm_Rational False) t_)"
1.36 -case pt of Nd (PblObj _, [Nd _]) => ((*met only applies norm_Rational*))
1.37 - | _ => error "solve.sml: interSteps on norm_Rational 1";
1.38 -interSteps 1 ([1], Res);
1.39 -getFormulaeFromTo 1 ([1], Frm) ([1,12], Res) 99999 false;
1.40 -interSteps 1 ([1,3], Res);
1.41 -
1.42 -getTactic 1 ([1,4], Res) (*here get the tactic, and ...*);
1.43 -interSteps 1 ([1,5], Res) (*... here get the intermediate steps above*);
1.44 -
1.45 -getTactic 1 ([1,5,1], Frm);
1.46 -val ((pt,_),_) = get_calc 1; show_pt pt;
1.47 -
1.48 -getTactic 1 ([1,8], Res) (*Rewrite_Set "common_nominator_p" *);
1.49 -interSteps 1 ([1,9], Res)(*TODO.WN060606 reverse rew*);
1.50 ---------------------------------------------------------------------*)
1.51 -
1.52 +states := []; (*exp_IsacCore_Simp_Rat_Double_No-7.xml*)
1.53 +CalcTree [(["Term ((2/(x+3) + 2/(x - 3)) / (8*x/(x^2 - 9)))", "normalform N"],
1.54 + ("Rational", ["rational","simplification"], ["simplification","of_rationals"]))];
1.55 +moveActiveRoot 1;
1.56 +autoCalculate 1 CompleteCalc;
1.57 +val ((pt, _), _) = get_calc 1; show_pt pt;
1.58 case pt of Nd (PblObj _, [Nd _, Nd _, Nd _, Nd _, Nd _, Nd _]) => ()
1.59 | _ => error "solve.sml: interSteps on norm_Rational 1";
1.60 -(*these have been done now by the script ^^^ immediately...
1.61 -interSteps 1 ([1], Res);
1.62 -getFormulaeFromTo 1 ([1], Frm) ([1,12], Res) 99999 false;
1.63 -*)
1.64 interSteps 1 ([6], Res);
1.65
1.66 getTactic 1 ([6,1], Frm) (*here get the tactic, and ...*);
1.67 interSteps 1 ([6,1], Res) (*... here get the intermediate steps above*);
1.68
1.69 -getTactic 1 ([3,4,1], Frm);
1.70 +getTactic 1 ([6,1,1], Frm); (*WN130909 <ERROR> syserror in getTactic </ERROR>*)
1.71 val ((pt,_),_) = get_calc 1; show_pt pt;
1.72 val (Form form, SOME tac, asm) = pt_extract (pt, ([6], Res));
1.73 case (term2str form, tac, terms2strs asm) of
1.74 - ("1 / 2", Check_Postcond ["rational", "simplification"],
1.75 - ["-36 * x + 4 * x ^^^ 3 ~= 0"]) => ()
1.76 + ("1 / 2", Check_Postcond ["rational", "simplification"], []) => ()
1.77 | _ => error "solve.sml: interSteps on norm_Rational 2";
1.78 -
1.79 +get_obj g_res pt [];
1.80 +val (t, asm) = get_obj g_result pt [];
1.81 +if terms2str asm = "[\"8 * x ~= 0\",\"-9 + x ^^^ 2 ~= 0\"," ^
1.82 + "\"(2 / (x + 3) + 2 / (x - 3)) / (8 * x / (x ^^^ 2 - 9)) is_ratpolyexp\"]"
1.83 +then () else error "solve.sml: interSteps on norm_Rational 2, asms";
1.84
1.85
1.86 "###### val intermediate_ptyps = !ptyps;val intermediate_mets = !mets";
1.87 @@ -97,54 +75,38 @@
1.88 "--------- prepare pbl, met --------------------------------------";
1.89 "--------- prepare pbl, met --------------------------------------";
1.90 store_pbt
1.91 - (prep_pbt @{theory Test} "pbl_ttestt" [] e_pblID
1.92 - (["test"],
1.93 - [],
1.94 - e_rls, NONE, []));
1.95 + (prep_pbt @{theory Test} "pbl_ttestt" [] e_pblID
1.96 + (["test"], [], e_rls, NONE, []));
1.97 store_pbt
1.98 - (prep_pbt @{theory Test} "pbl_ttestt_detail" [] e_pblID
1.99 - (["detail","test"],
1.100 - [("#Given" ,["realTestGiven t_t"]),
1.101 - ("#Find" ,["realTestFind s_s"])
1.102 - ],
1.103 - e_rls, NONE, [["Test","test_detail"]]));
1.104 + (prep_pbt @{theory Test} "pbl_ttestt_detail" [] e_pblID
1.105 + (["detail","test"],
1.106 + [("#Given", ["realTestGiven t_t"]), ("#Find", ["realTestFind s_s"])],
1.107 + e_rls, NONE, [["Test","test_detail"]]));
1.108
1.109 store_met
1.110 - (prep_met @{theory Test} "met_detbin" [] e_metID
1.111 - (["Test","test_detail_binom"]:metID,
1.112 - [("#Given" ,["realTestGiven t_t"]),
1.113 - ("#Find" ,["realTestFind s_s"])
1.114 - ],
1.115 - {rew_ord' = "sqrt_right", rls' = tval_rls, calc = [], srls = e_rls, prls = e_rls,
1.116 - crls = tval_rls, errpats = [], nrls = e_rls(*,
1.117 - asm_rls=[],asm_thm=[("real_mult_div_cancel2","")]*)},
1.118 - "Script Testterm (g_g::real) = \
1.119 - \(((Rewrite_Set expand_binoms False) @@\
1.120 - \ (Rewrite_Set cancel False)) g_g)"
1.121 - ));
1.122 + (prep_met @{theory Test} "met_detbin" [] e_metID
1.123 + (["Test", "test_detail_binom"] : metID,
1.124 + [("#Given", ["realTestGiven t_t"]), ("#Find", ["realTestFind s_s"])],
1.125 + {rew_ord' = "sqrt_right", rls' = tval_rls, calc = [], srls = e_rls, prls = e_rls,
1.126 + crls = tval_rls, errpats = [], nrls = e_rls},
1.127 + "Script Testterm (g_g::real) =" ^
1.128 + "(((Rewrite_Set expand_binoms False) @@" ^
1.129 + "(Rewrite_Set cancel_p False)) g_g)"));
1.130 store_met
1.131 - (prep_met @{theory Test} "met_detpoly" [] e_metID
1.132 - (["Test","test_detail_poly"]:metID,
1.133 - [("#Given" ,["realTestGiven t_t"]),
1.134 - ("#Find" ,["realTestFind s_s"])
1.135 - ],
1.136 - {rew_ord' = "sqrt_right", rls' = tval_rls, calc = [], srls = e_rls, prls = e_rls,
1.137 - crls = tval_rls, errpats = [], nrls = e_rls(*,
1.138 - asm_rls=[],asm_thm=[("real_mult_div_cancel2","")]*)},
1.139 - "Script Testterm (g_g::real) = \
1.140 - \(((Rewrite_Set make_polynomial False) @@\
1.141 - \ (Rewrite_Set cancel_p False)) g_g)"
1.142 - ));
1.143 -
1.144 -(*---- funktionieren mit Rationals.ML: dummy-Funktionen(1)--------*)
1.145 + (prep_met @{theory Test} "met_detpoly" [] e_metID
1.146 + (["Test","test_detail_poly"] : metID,
1.147 + [("#Given", ["realTestGiven t_t"]), ("#Find", ["realTestFind s_s"])],
1.148 + {rew_ord' = "sqrt_right", rls' = tval_rls, calc = [], srls = e_rls, prls = e_rls,
1.149 + crls = tval_rls, errpats = [], nrls = e_rls},
1.150 + "Script Testterm (g_g::real) =" ^
1.151 + "(((Rewrite_Set make_polynomial False) @@" ^
1.152 + "(Rewrite_Set cancel_p False)) g_g)"));
1.153
1.154 "-------- cancel, without detail ------------------------------";
1.155 "-------- cancel, without detail ------------------------------";
1.156 "-------- cancel, without detail ------------------------------";
1.157 -val fmz = ["realTestGiven (((3 + x) * (3 - x)) / ((3 + x) * (3 + x)))",
1.158 - "realTestFind s"];
1.159 -val (dI',pI',mI') =
1.160 - ("Test",["detail","test"],["Test","test_detail_binom"]);
1.161 +val fmz = ["realTestGiven (((3 + x) * (3 + -1*x)) / ((3 + x) * (3 + x)))", "realTestFind s"];
1.162 +val (dI',pI',mI') = ("Test", ["detail", "test"], ["Test", "test_detail_binom"]);
1.163
1.164 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.165 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.166 @@ -158,13 +120,11 @@
1.167 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.168 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.169 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.170 -(*"(3 + -1 * x) / (3 + x)"*)
1.171 +(*WN130909: detail will be discontinued
1.172 if nxt = ("End_Proof'",End_Proof') then ()
1.173 else error "details.sml, changed behaviour in: without detail";
1.174 -
1.175 - val str = pr_ptree pr_short pt;
1.176 - writeln str;
1.177 -
1.178 +*)
1.179 +val str = pr_ptree pr_short pt;
1.180
1.181 "-------- cancel, detail rev-rew (cancel) afterwards ----------";
1.182 "-------- cancel, detail rev-rew (cancel) afterwards ----------";
1.183 @@ -196,10 +156,10 @@
1.184 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.185 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.186 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.187 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.188 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;src
1.189 (*val nxt = ("End_Detail",End_Detail)*)
1.190 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.191 - (*val nxt = ("Rewrite_Set",Rewrite_Set "cancel")*)
1.192 + (*val nxt = ("Rewrite_Set",Rewrite_Set "cancel")*)src
1.193 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)
1.194 val nxt = ("Detail",Detail);"----------------------";
1.195 val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => OldGoals.print_exn e;