1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/test/Tools/isac/Interpret/me.sml Mon Aug 30 14:35:51 2010 +0200
1.3 @@ -0,0 +1,528 @@
1.4 +(* tests on me.sml
1.5 + author: Walther Neuper
1.6 + 060225,
1.7 + (c) due to copyright terms
1.8 +
1.9 +use"../smltest/ME/me.sml";
1.10 +use"me.sml";
1.11 +*)
1.12 +
1.13 +"-----------------------------------------------------------------";
1.14 +"table of contents -----------------------------------------------";
1.15 +"-----------------------------------------------------------------";
1.16 +"=====new ptree 1: crippled by cut_level_'_ ======================";
1.17 +"-------------- get_interval from ctree with move_dn:modspec.sml -";
1.18 +"=====new ptree 2 without changes ================================";
1.19 +"-------------- getFormulaeFromTo --------------------------------";
1.20 +"autoCalculate";
1.21 +"--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";
1.22 +"--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-";
1.23 +"--------- maximum-example: complete_metitms ---------------------";
1.24 +"--------- maximum-example: complete_mod -------------------------";
1.25 +"-----------------------------------------------------------------";
1.26 +"-----------------------------------------------------------------";
1.27 +"-----------------------------------------------------------------";
1.28 +
1.29 +
1.30 +
1.31 +"=====new ptree 1: crippled by cut_level_'_ ======================";
1.32 +"=====new ptree 1: crippled by cut_level_'_ ======================";
1.33 +"=====new ptree 1: crippled by cut_level_'_ ======================";
1.34 +states:=[];
1.35 +CalcTree
1.36 +[(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
1.37 + "solveFor x","solutions L"],
1.38 + ("RatEq.thy",["univariate","equation"],["no_met"]))];
1.39 +Iterator 1; moveActiveRoot 1;
1.40 +autoCalculate 1 CompleteCalc;
1.41 +
1.42 +getTactic 1 ([1],Res);(*Rewrite_Set RatEq_simplify*)
1.43 +getTactic 1 ([2],Res);(*Rewrite_Set norm_Rational*)
1.44 +getTactic 1 ([3],Res);(*Rewrite_Set RatEq_eliminate*)
1.45 +getTactic 1 ([4,1],Res);(*Rewrite all_left*)
1.46 +getTactic 1 ([4,2],Res);(*Rewrite_Set expand_binoms*)
1.47 +getTactic 1 ([4,3],Res);(*Rewrite_Set_Inst make_ratpoly_in*)
1.48 +
1.49 +moveActiveFormula 1 ([1],Res)(*1.1...1.4*);
1.50 +moveActiveFormula 1 ([2],Res)(**ME_Isa: 'expand' not known*);
1.51 +moveActiveFormula 1 ([3],Res)(*3.1.*);
1.52 +moveActiveFormula 1 ([4,2],Res)(*4.2.1.*);
1.53 +moveActiveFormula 1 ([4,3],Res)(**one_scr_arg: called by Script Stepwise t_=*);
1.54 +
1.55 +moveActiveFormula 1 ([1],Res)(*1.1...1.4*);
1.56 +interSteps 1 ([1],Res)(*..is activeFormula !?!*);
1.57 +
1.58 +getTactic 1 ([1,1],Res);(*Rewrite real_diff_minus*)
1.59 +getTactic 1 ([1,2],Res);(*Rewrite real_diff_minus*)
1.60 +getTactic 1 ([1,3],Res);(*Rewrite real_diff_minus*)
1.61 +getTactic 1 ([1,4],Res);(*Rewrite real_rat_mult_1*)
1.62 +
1.63 +moveActiveFormula 1 ([4,2],Res)(*4.2.1.*);
1.64 +interSteps 1 ([4,2],Res)(*..is activeFormula !?!*);
1.65 +val ((pt,_),_) = get_calc 1;
1.66 +writeln(pr_ptree pr_short pt);
1.67 +(*delete [4,1] in order to make pos [4],[4,4] for pblobjs differen [4],[4,3]:
1.68 + ###########################################################################*)
1.69 +val (pt, _) = cut_level_'_ [] [] pt ([4,1],Frm); (*#*)
1.70 +(*##########################################################################*)
1.71 +writeln(pr_ptree pr_short pt);
1.72 +(*##########################################################################
1.73 + attention: the ctree in states is still the old (perfect) !!!
1.74 +############################################################################*)
1.75 +
1.76 +
1.77 +
1.78 +"-------------- get_interval from ctree with move_dn:modspec.sml -";
1.79 +"-------------- get_interval from ctree with move_dn:modspec.sml -";
1.80 +"-------------- get_interval from ctree with move_dn:modspec.sml -";
1.81 +writeln(pr_ptree pr_short pt);
1.82 +writeln(posterms2str (get_interval ([],Frm) ([],Res) 99999 pt));
1.83 +
1.84 +case map fst (get_interval ([],Frm) ([],Res) 99999 pt) of
1.85 + [([], Frm),
1.86 + ([1], Frm),
1.87 + ([1, 1], Frm),
1.88 + ([1, 1], Res),
1.89 + ([1, 2], Res),
1.90 + ([1, 3], Res),
1.91 + ([1, 4], Res),
1.92 + ([1], Res),
1.93 + ([2], Res),
1.94 + ([3], Res),
1.95 + ([4], Pbl),
1.96 + ([4, 1], Frm),
1.97 + ([4, 1, 1], Frm),
1.98 + ([4, 1, 1], Res),
1.99 + ([4, 1], Res),
1.100 + ([4, 2], Res),
1.101 + ([4, 3], Pbl),
1.102 + ([4, 3, 1], Frm),
1.103 + ([4, 3, 1], Res),
1.104 + ([4, 3, 2], Res),
1.105 + ([4, 3, 3], Res),
1.106 + ([4, 3, 4], Res),
1.107 + ([4, 3, 5], Res),
1.108 + ([4, 3], Res),
1.109 + ([4], Res),
1.110 + ([5], Res),
1.111 + ([], Res)] => ()
1.112 + | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1f";
1.113 +case map fst (get_interval ([],Frm) ([],Res) 1 pt) of
1.114 + [([], Frm),
1.115 + ([1], Frm),
1.116 + ([1], Res),
1.117 + ([2], Res),
1.118 + ([3], Res),
1.119 + ([4], Pbl),
1.120 + ([4], Res),
1.121 + ([5], Res),
1.122 + ([], Res)] => ()
1.123 + | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1f";
1.124 +case map fst (get_interval ([],Frm) ([],Res) 0 pt) of
1.125 + [([], Frm),
1.126 + ([], Res)] => ()
1.127 + | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1f";
1.128 +
1.129 +case map fst (get_interval ([1,3],Res) ([4,1,1],Frm) 99999 pt) of
1.130 + [([1, 3], Res),
1.131 + ([1, 4], Res),
1.132 + ([1], Res),
1.133 + ([2], Res),
1.134 + ([3], Res),
1.135 + ([4], Pbl),
1.136 + ([4, 1], Frm),
1.137 + ([4, 1, 1], Frm)] => ()
1.138 + | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1a";
1.139 +
1.140 +(*this pos' is not generated bu move_dn:......vvv: goes to end of calc*)
1.141 +case map fst (get_interval ([2],Res) ([4,3,2],Frm) 99999 pt) of
1.142 + [([2], Res),
1.143 + ([3], Res),
1.144 + ([4], Pbl),
1.145 + ([4, 1], Frm),
1.146 + ([4, 1, 1], Frm),
1.147 + ([4, 1, 1], Res),
1.148 + ([4, 1], Res),
1.149 + ([4, 2], Res),
1.150 + ([4, 3], Pbl),
1.151 + ([4, 3, 1], Frm),
1.152 + ([4, 3, 1], Res),
1.153 + ([4, 3, 2], Res),
1.154 + ([4, 3, 3], Res),(*this is beyond 'to'*)
1.155 + ([4, 3, 4], Res),(*this is beyond 'to'*)
1.156 + ([4, 3, 5], Res),(*this is beyond 'to'*)
1.157 + ([4, 3], Res), (*this is beyond 'to'*)
1.158 + ([4], Res), (*this is beyond 'to'*)
1.159 + ([5], Res), (*this is beyond 'to'*)
1.160 + ([], Res)] => () (*this is beyond 'to'*)
1.161 + | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1b";
1.162 +case map fst (get_interval ([1,4],Res) ([4,3,1],Frm) 99999 pt) of
1.163 + [([1, 4], Res),
1.164 + ([1], Res),
1.165 + ([2], Res),
1.166 + ([3], Res),
1.167 + ([4], Pbl),
1.168 + ([4, 1], Frm),
1.169 + ([4, 1, 1], Frm),
1.170 + ([4, 1, 1], Res),
1.171 + ([4, 1], Res),
1.172 + ([4, 2], Res),
1.173 + ([4, 3], Pbl),
1.174 + ([4, 3, 1], Frm)] => ()
1.175 + | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1c";
1.176 +case map fst (get_interval ([4,2],Res) ([5],Res) 99999 pt) of
1.177 + [([4, 2], Res),
1.178 + ([4, 3], Pbl),
1.179 + ([4, 3, 1], Frm),
1.180 + ([4, 3, 1], Res),
1.181 + ([4, 3, 2], Res),
1.182 + ([4, 3, 3], Res),
1.183 + ([4, 3, 4], Res),
1.184 + ([4, 3, 5], Res),
1.185 + ([4, 3], Res),
1.186 + ([4], Res),
1.187 + ([5], Res)]=>()
1.188 + | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1d";
1.189 +case map fst (get_interval ([],Frm) ([4,3,2],Res) 99999 pt) of
1.190 + [([], Frm),
1.191 + ([1], Frm),
1.192 + ([1, 1], Frm),
1.193 + ([1, 1], Res),
1.194 + ([1, 2], Res),
1.195 + ([1, 3], Res),
1.196 + ([1, 4], Res),
1.197 + ([1], Res),
1.198 + ([2], Res),
1.199 + ([3], Res),
1.200 + ([4], Pbl),
1.201 + ([4, 1], Frm),
1.202 + ([4, 1, 1], Frm),
1.203 + ([4, 1, 1], Res),
1.204 + ([4, 1], Res),
1.205 + ([4, 2], Res),
1.206 + ([4, 3], Pbl),
1.207 + ([4, 3, 1], Frm),
1.208 + ([4, 3, 1], Res),
1.209 + ([4, 3, 2], Res)] => ()
1.210 + | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1e";
1.211 +case map fst (get_interval ([4,3],Frm) ([4,3],Res) 99999 pt) of
1.212 + [([4, 3], Frm),
1.213 + ([4, 3, 1], Frm),
1.214 + ([4, 3, 1], Res),
1.215 + ([4, 3, 2], Res),
1.216 + ([4, 3, 3], Res),
1.217 + ([4, 3, 4], Res),
1.218 + ([4, 3, 5], Res),
1.219 + ([4, 3], Res)] => ()
1.220 + | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1g";
1.221 +
1.222 +
1.223 +
1.224 +
1.225 +"=====new ptree 2 without changes ================================";
1.226 +"=====new ptree 2 without changes ================================";
1.227 +"=====new ptree 2 without changes ================================";
1.228 +states:=[];
1.229 +CalcTree
1.230 +[(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
1.231 + "solveFor x","solutions L"],
1.232 + ("RatEq.thy",["univariate","equation"],["no_met"]))];
1.233 +Iterator 1; moveActiveRoot 1;
1.234 +autoCalculate 1 CompleteCalc;
1.235 +val ((pt,_),_) = get_calc 1;
1.236 +writeln(pr_ptree pr_short pt);
1.237 +
1.238 +
1.239 +"-------------- getFormulaeFromTo --------------------------------";
1.240 +"-------------- getFormulaeFromTo --------------------------------";
1.241 +"-------------- getFormulaeFromTo --------------------------------";
1.242 +getFormulaeFromTo 1 ([4, 2], Res) ([4, 4], Pbl) 000;
1.243 +(*
1.244 +"@@@@@begin@@@@@" //...................................................
1.245 ++ " 1" //..............................................................
1.246 ++ "<GETELEMENTSFROMTO>" //...................................................
1.247 ++ " <CALCID> 1 </CALCID>" //..........................................
1.248 ++ " <POSFORMHEADS>" //................................................
1.249 ++ " <POSFORM>" //...................................................
1.250 ++ " <GENERATED>" //...............................................
1.251 ++ " <INTLIST>" //...............................................
1.252 ++ " <INT> 4 </INT>" //........................................
1.253 ++ " <INT> 3 </INT>" //........................................
1.254 ++ " </INTLIST>" //..............................................
1.255 ++ " <POS> Res </POS>" //........................................
1.256 ++ " </GENERATED>" //..............................................
1.257 ++ " <FORMULA>" //.................................................
1.258 ++ " <MATHML>" //................................................
1.259 ++ " <ISA> -6 * x + 5 * x ^^^ 2 = 0 </ISA>" //.................
1.260 ++ " </MATHML>" //...............................................
1.261 ++ " </FORMULA>" //................................................
1.262 ++ " </POSFORM>" //..................................................
1.263 ++ " <POSHEAD>" //...................................................
1.264 ++ " <GENERATED>" //...............................................
1.265 ++ " <INTLIST>" //...............................................
1.266 ++ " <INT> 4 </INT>" //........................................
1.267 ++ " <INT> 4 </INT>" //........................................
1.268 ++ " </INTLIST>" //..............................................
1.269 ++ " <POS> Pbl </POS>" //........................................
1.270 ++ " </GENERATED>" //..............................................
1.271 ++ " <CALCHEAD status = "correct">" //.............................
1.272 ++ " <HEAD>" //...................................................
1.273 ++ " <MATHML>" //...............................................
1.274 ++ " <ISA> solve (-6 * x + 5 * x ^^^ 2 = 0, x) </ISA>" //.....
1.275 ++ " </MATHML>" //..............................................
1.276 ++ " </HEAD>" //..................................................
1.277 ++ " <MODEL>" //.................................................
1.278 ++ " <GIVEN>" //...............................................
1.279 ++ " <ITEM status="correct">" //.............................
1.280 ++ " <MATHML>" //..........................................
1.281 ++ " <ISA> equality (-6 * x + 5 * x ^^^ 2 = 0) </ISA>" //
1.282 ++ " </MATHML>" //.........................................
1.283 ++ " </ITEM>" //.............................................
1.284 ++ " <ITEM status="correct">" //.............................
1.285 ++ " <MATHML>" //..........................................
1.286 ++ " <ISA> solveFor x </ISA>" //.........................
1.287 ++ " </MATHML>" //.........................................
1.288 ++ " </ITEM>" //.............................................
1.289 ++ " </GIVEN>" //..............................................
1.290 ++ " <WHERE>" //...............................................
1.291 ++ " <ITEM status="correct">" //.............................
1.292 ++ " <MATHML>" //..........................................
1.293 ++ " <ISA> matches (?a * ?v_ + ?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) |"
1.294 ++ "matches (?v_ + ?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) |" //......
1.295 ++ "matches (?v_ + ?b * ?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) |"
1.296 ++ "matches (?a * ?v_ + ?b * ?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) |"
1.297 ++ "matches (?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) |" //............
1.298 ++ "matches (?b * ?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) </ISA>" //..
1.299 ++ " </MATHML>" //.........................................
1.300 ++ " </ITEM>" //.............................................
1.301 ++ " </WHERE>" //..............................................
1.302 ++ " <FIND>" //................................................
1.303 ++ " <ITEM status="correct">" //.............................
1.304 ++ " <MATHML>" //..........................................
1.305 ++ " <ISA> solutions x_i </ISA>" //......................
1.306 ++ " </MATHML>" //.........................................
1.307 ++ " </ITEM>" //.............................................
1.308 ++ " </FIND>" //...............................................
1.309 ++ " <RELATE> </RELATE>" //...................................
1.310 ++ " </MODEL>" //................................................
1.311 ++ " <BELONGSTO> Pbl </BELONGSTO>" //............................
1.312 ++ " <SPECIFICATION>" //.........................................
1.313 ++ " <THEORYID> PolyEq.thy </THEORYID>" //.....................
1.314 ++ " <PROBLEMID>" //...........................................
1.315 ++ " <STRINGLIST>" //........................................
1.316 ++ " <STRING> bdv_only </STRING>" //.......................
1.317 ++ " <STRING> degree_2 </STRING>" //.......................
1.318 ++ " <STRING> polynomial </STRING>" //.....................
1.319 ++ " <STRING> univariate </STRING>" //.....................
1.320 ++ " <STRING> equation </STRING>" //.......................
1.321 ++ " </STRINGLIST>" //.......................................
1.322 ++ " </PROBLEMID>" //..........................................
1.323 ++ " <METHODID>" //............................................
1.324 ++ " <STRINGLIST>" //........................................
1.325 ++ " <STRING> PolyEq </STRING>" //.........................
1.326 ++ " <STRING> solve_d2_polyeq_bdvonly_equation </STRING>"
1.327 ++ " </STRINGLIST>" //.......................................
1.328 ++ " </METHODID>" //...........................................
1.329 ++ " </SPECIFICATION>" //........................................
1.330 ++ " </CALCHEAD>" //...............................................
1.331 ++ " </POSHEAD>" //..................................................
1.332 ++ " <POSFORMHEADS>" //................................................
1.333 ++ "</GETELEMENTSFROMTO>" //..................................................
1.334 ++ "@@@@@end@@@@@"
1.335 +*)
1.336 +
1.337 +
1.338 +"--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";
1.339 +"--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";
1.340 +"--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";
1.341 + val c = [];
1.342 + val (p,_,f,nxt,_,pt) = CalcTreeTEST
1.343 + [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
1.344 + ("Test.thy",
1.345 + ["linear","univariate","equation","test"],
1.346 + ["Test","solve_linear"]))];
1.347 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.348 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.349 + (*xt = Add_Given "solveFor x"*)
1.350 + writeln (itms2str_ ctxt (get_obj g_pbl pt (fst p)));
1.351 +(*[
1.352 +(0 ,[] ,false ,#Given ,Inc solveFor ,(??.empty, [])),
1.353 +(0 ,[] ,false ,#Find ,Inc solutions [] ,(??.empty, [])),
1.354 +(1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0]))]*)
1.355 + val (pt,p) = complete_mod (pt, p);
1.356 + if itms2str_ ctxt (get_obj g_pbl pt (fst p)) = "[\n(1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),\n(2 ,[1] ,true ,#Given ,Cor solveFor x ,(v_, [x])),\n(3 ,[1] ,true ,#Find ,Cor solutions L ,(v_i_, [L]))]" then ()
1.357 + else raise error "completetest.sml: new behav. in complete_mod 1";
1.358 + writeln (itms2str_ ctxt (get_obj g_pbl pt (fst p)));
1.359 +(*[
1.360 +(1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),
1.361 +(2 ,[1] ,true ,#Given ,Cor solveFor x ,(solveFor, [x])),
1.362 +(3 ,[1] ,true ,#Find ,Cor solutions L ,(solutions, [L]))]*)
1.363 + val mits = get_obj g_met pt (fst p);
1.364 + if itms2str_ ctxt mits = "[\n(1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),\n(2 ,[1] ,true ,#Given ,Cor solveFor x ,(v_, [x])),\n(3 ,[1] ,true ,#Find ,Cor solutions L ,(v_i_, [L]))]"
1.365 + then () else raise error "completetest.sml: new behav. in complete_mod 2";
1.366 + writeln (itms2str_ ctxt mits);
1.367 +(*[
1.368 +(1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),
1.369 +(2 ,[1] ,true ,#Given ,Cor solveFor x ,(solveFor, [x])),
1.370 +(3 ,[1] ,true ,#Find ,Cor solutions L ,(solutions, [L]))]*)
1.371 +
1.372 +
1.373 +
1.374 +"--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-";
1.375 +"--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-";
1.376 +"--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-";
1.377 + states:=[];
1.378 + CalcTree (*start of calculation, return No.1*)
1.379 + [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
1.380 + ("Test.thy",
1.381 + ["linear","univariate","equation","test"],
1.382 + ["Test","solve_linear"]))];
1.383 + Iterator 1; moveActiveRoot 1;
1.384 +
1.385 +(*
1.386 + autoCalculate 1 CompleteCalcHead;
1.387 + autoCalculate 1 (Step 1);
1.388 + refFormula 1 (get_pos 1 1);
1.389 +
1.390 +... works
1.391 +
1.392 + autoCalculate 1 CompleteCalcHead;
1.393 + fetchProposedTactic 1; (*-> Apply_Method*);
1.394 + setNextTactic 1 (Apply_Method ["Test","solve_linear"]);
1.395 + autoCalculate 1 (Step 1);
1.396 + refFormula 1 (get_pos 1 1);
1.397 +
1.398 +... works *)
1.399 +
1.400 + autoCalculate 1 (Step 1);
1.401 + refFormula 1 (get_pos 1 1);
1.402 +
1.403 + autoCalculate 1 CompleteModel;
1.404 + refFormula 1 (get_pos 1 1);
1.405 +
1.406 + autoCalculate 1 CompleteCalcHead;
1.407 +(* *** complete_mod: only impl.for Pbl, called with ([], Met) FIXXXXXXXXXXME*)
1.408 +
1.409 +
1.410 +
1.411 +"--------- maximum-example: complete_metitms ---------------------";
1.412 +"--------- maximum-example: complete_metitms ---------------------";
1.413 +"--------- maximum-example: complete_metitms ---------------------";
1.414 + val (p,_,f,nxt,_,pt) =
1.415 + CalcTreeTEST
1.416 + [(["fixedValues [r=Arbfix]","maximum A",
1.417 + "valuesFor [a,b]",
1.418 + "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
1.419 + "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
1.420 + "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
1.421 +
1.422 + "boundVariable a","boundVariable b","boundVariable alpha",
1.423 + "interval {x::real. 0 <= x & x <= 2*r}",
1.424 + "interval {x::real. 0 <= x & x <= 2*r}",
1.425 + "interval {x::real. 0 <= x & x <= pi}",
1.426 + "errorBound (eps=(0::real))"],
1.427 + ("DiffApp.thy",["maximum_of","function"],["DiffApp","max_by_calculus"])
1.428 + )];
1.429 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.430 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.431 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.432 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.433 + val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => print_exn e;
1.434 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.435 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.436 + (*nxt = Specify_Theory "DiffApp.thy"*)
1.437 + val (oris, _, _) = get_obj g_origin pt (fst p);
1.438 + writeln (oris2str oris);
1.439 +(*[
1.440 +(1, ["1","2","3"], #Given,fixedValues, ["[r = Arbfix]"]),
1.441 +(2, ["1","2","3"], #Find,maximum, ["A"]),
1.442 +(3, ["1","2","3"], #Find,valuesFor, ["[a]","[b]"]),
1.443 +(4, ["1","2"], #Relate,relations, ["[A = a * b]","[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]"]),
1.444 +(5, ["3"], #Relate,relations, ["[A = a * b]","[a / 2 = r * sin alpha]","[b / 2 = r * cos alpha]"]),
1.445 +(6, ["1"], #undef,boundVariable, ["a"]),
1.446 +(7, ["2"], #undef,boundVariable, ["b"]),
1.447 +(8, ["3"], #undef,boundVariable, ["alpha"]),
1.448 +(9, ["1","2"], #undef,interval, ["{x. 0 <= x & x <= 2 * r}"]),
1.449 +(10, ["3"], #undef,interval, ["{x. 0 <= x & x <= pi}"]),
1.450 +(11, ["1","2","3"], #undef,errorBound, ["eps = 0"])]*)
1.451 + val pits = get_obj g_pbl pt (fst p);
1.452 + writeln (itms2str_ ctxt pits);
1.453 +(*[
1.454 +(1 ,[1,2,3] ,true,#Given ,Cor fixedValues [r = Arbfix],(fix_, [[r = Arbfix]])),
1.455 +(2 ,[1,2,3] ,true,#Find ,Cor maximum A ,(m_, [A])),
1.456 +(3 ,[1,2,3] ,true,#Find ,Cor valuesFor [a, b] ,(vs_, [[a, b]])),
1.457 +(4 ,[1,2] ,true,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
1.458 +2 = r ^^^ 2] ,(rs_, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]*)
1.459 + val mits = get_obj g_met pt (fst p);
1.460 + val mits = complete_metitms oris pits []
1.461 + ((#ppc o get_met) ["DiffApp","max_by_calculus"]);
1.462 + writeln (itms2str_ ctxt mits);
1.463 +(*[
1.464 +(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
1.465 +(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
1.466 +(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a, b]])),
1.467 +(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
1.468 +2 = r ^^^ 2] ,(rs_, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),
1.469 +(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(boundVariable, [a])),
1.470 +(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x.
1.471 +0 <= x & x <= 2 * r}])),
1.472 +(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*)
1.473 + if itms2str_ ctxt mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a, b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(itv_, [{x. 0 <= x & x <= 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(err_, [eps = 0]))]" then ()
1.474 + else raise error "completetest.sml: new behav. in complete_metitms 1";
1.475 +
1.476 +
1.477 +"--------- maximum-example: complete_mod -------------------------";
1.478 +"--------- maximum-example: complete_mod -------------------------";
1.479 +"--------- maximum-example: complete_mod -------------------------";
1.480 + val (p,_,f,nxt,_,pt) =
1.481 + CalcTreeTEST
1.482 + [(["fixedValues [r=Arbfix]","maximum A",
1.483 + "valuesFor [a,b]",
1.484 + "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
1.485 + "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
1.486 + "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
1.487 +
1.488 + "boundVariable a","boundVariable b","boundVariable alpha",
1.489 + "interval {x::real. 0 <= x & x <= 2*r}",
1.490 + "interval {x::real. 0 <= x & x <= 2*r}",
1.491 + "interval {x::real. 0 <= x & x <= pi}",
1.492 + "errorBound (eps=(0::real))"],
1.493 + ("DiffApp.thy",["maximum_of","function"],["DiffApp","max_by_calculus"])
1.494 + )];
1.495 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.496 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.497 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.498 + (*nxt = nxt = Add_Find "valuesFor [a]" FIXME.12.03 +handle Inc !*)
1.499 + val pits = get_obj g_pbl pt (fst p);
1.500 + writeln (itms2str_ ctxt pits);
1.501 +(*[
1.502 +(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),
1.503 +(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, [])),
1.504 +(1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
1.505 +(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A]))]*)
1.506 + val (pt,p) = complete_mod (pt,p);
1.507 + val pits = get_obj g_pbl pt (fst p);
1.508 + if itms2str_ ctxt pits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]"
1.509 + then () else raise error "completetest.sml: new behav. in complete_mod 3";
1.510 + writeln (itms2str_ ctxt pits);
1.511 +(*[
1.512 +(1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
1.513 +(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
1.514 +(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])),
1.515 +(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
1.516 +2 = r ^^^ 2] ,(relations, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]*)
1.517 + val mits = get_obj g_met pt (fst p);
1.518 + if itms2str_ ctxt mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(itv_, [{x. 0 <= x & x <= 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(err_, [eps = 0]))]"
1.519 + then () else raise error "completetest.sml: new behav. in complete_mod 3";
1.520 + writeln (itms2str_ ctxt mits);
1.521 +(*[
1.522 +(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
1.523 +(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
1.524 +(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])),
1.525 +(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
1.526 +2 = r ^^^ 2] ,(relations, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),
1.527 +(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(boundVariable, [a])),
1.528 +(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x.
1.529 +0 <= x & x <= 2 * r}])),
1.530 +(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*)
1.531 +