wneuper/isa: test/Tools/isac/Interpret/me.sml@255c853ea2f0

     1 (* tests on me.sml

     2    author: Walther Neuper

     3    060225,

     4    (c) due to copyright terms

     6 use"../smltest/ME/me.sml";

     7 use"me.sml";

     8 *)

    10 "-----------------------------------------------------------------";

    11 "table of contents -----------------------------------------------";

    12 "-----------------------------------------------------------------";

    13 "=====new ctree 1: crippled by cut_level_'_ ======================";

    14 "-------------- get_interval from ctree with move_dn:modspec.sml -";

    15 "=====new ctree 2 without changes ================================";

    16 "-------------- getFormulaeFromTo --------------------------------";

    17 "autoCalculate";

    18 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";

    19 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-";

    20 "--------- maximum-example: complete_metitms ---------------------";

    21 "--------- maximum-example: complete_mod -------------------------";

    22 "-----------------------------------------------------------------";

    23 "-----------------------------------------------------------------";

    24 "-----------------------------------------------------------------";

    28 "=====new ctree 1: crippled by cut_level_'_ ======================";

    29 "=====new ctree 1: crippled by cut_level_'_ ======================";

    30 "=====new ctree 1: crippled by cut_level_'_ ======================";

    31 reset_states ();

    32 CalcTree

    33 [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",

    34 	   "solveFor x","solutions L"],

    35   ("RatEq",["univariate","equation"],["no_met"]))];

    36 Iterator 1; moveActiveRoot 1;

    37 autoCalculate 1 CompleteCalc;

    39 getTactic 1 ([1],Res);(*Rewrite_Set RatEq_simplify*)

    40 getTactic 1 ([2],Res);(*Rewrite_Set norm_Rational*)

    41 getTactic 1 ([3],Res);(*Rewrite_Set RatEq_eliminate*)

    42 getTactic 1 ([4,1],Res);(*Rewrite all_left*)

    43 getTactic 1 ([4,2],Res);(*Rewrite_Set expand_binoms*)

    44 getTactic 1 ([4,3],Res);(*Rewrite_Set_Inst make_ratpoly_in*)

    46 moveActiveFormula 1 ([1],Res)(*1.1...1.4*);

    47 moveActiveFormula 1 ([2],Res)(**ME_Isa: 'expand' not known*);

    48 moveActiveFormula 1 ([3],Res)(*3.1.*);

    49 moveActiveFormula 1 ([4,2],Res)(*4.2.1.*);

    50 moveActiveFormula 1 ([4,3],Res)(**one_scr_arg: called by Script Stepwise t_=*);

    52 moveActiveFormula 1 ([1],Res)(*1.1...1.4*);

    53 interSteps 1 ([1],Res)(*..is activeFormula !?!*);

    55 getTactic 1 ([1,1],Res);(*Rewrite real_diff_minus*)

    56 getTactic 1 ([1,2],Res);(*Rewrite real_diff_minus*)

    57 getTactic 1 ([1,3],Res);(*Rewrite real_diff_minus*)

    58 getTactic 1 ([1,4],Res);(*Rewrite real_rat_mult_1*)

    60 moveActiveFormula 1 ([4,2],Res)(*4.2.1.*);

    61 interSteps 1 ([4,2],Res)(*..is activeFormula !?!*);

    62 val ((pt,_),_) = get_calc 1;

    63 writeln(pr_ctree pr_short pt);

    64 (*delete [4,1] in order to make pos [4],[4,4] for pblobjs differen [4],[4,3]:

    65  ###########################################################################*)

    66 val (pt, _) = cut_level_'_ [] [] pt ([4,1],Frm);                         (*#*)

    67 (*##########################################################################*)

    68 writeln(pr_ctree pr_short pt);

    69 (*##########################################################################

    70   attention: the ctree in states is still the old (perfect) !!!

    71 ############################################################################*)

    75 "-------------- get_interval from ctree with move_dn:modspec.sml -";

    76 "-------------- get_interval from ctree with move_dn:modspec.sml -";

    77 "-------------- get_interval from ctree with move_dn:modspec.sml -";

    78 writeln(pr_ctree pr_short pt);

    79 writeln(posterms2str (get_interval ([],Frm) ([],Res) 99999 pt));

    81 case map fst (get_interval ([],Frm) ([],Res) 99999 pt) of

    82     [([], Frm),

    83      ([1], Frm),

    84      ([1, 1], Frm),

    85      ([1, 1], Res),

    86      ([1, 2], Res),

    87      ([1, 3], Res),

    88      ([1, 4], Res),

    89      ([1], Res),

    90      ([2], Res),

    91      ([3], Res),

    92      ([4], Pbl),

    93      ([4, 1], Frm),

    94      ([4, 1, 1], Frm),

    95      ([4, 1, 1], Res),

    96      ([4, 1], Res),

    97      ([4, 2], Res),

    98      ([4, 3], Pbl),

    99      ([4, 3, 1], Frm),

   100      ([4, 3, 1], Res),

   101      ([4, 3, 2], Res),

   102      ([4, 3, 3], Res),

   103      ([4, 3, 4], Res),

   104      ([4, 3, 5], Res),

   105      ([4, 3], Res),

   106      ([4], Res),

   107      ([5], Res),

   108      ([], Res)] => ()

   109   | _ => error "diff.behav.in ctree.sml: get_interval lev 1f";

   110 case map fst (get_interval ([],Frm) ([],Res) 1 pt) of

   111     [([], Frm),

   112      ([1], Frm),

   113      ([1], Res),

   114      ([2], Res),

   115      ([3], Res),

   116      ([4], Pbl),

   117      ([4], Res),

   118      ([5], Res),

   119      ([], Res)] => ()

   120   | _ => error "diff.behav.in ctree.sml: get_interval lev 1f";

   121 case map fst (get_interval ([],Frm) ([],Res) 0 pt) of

   122     [([], Frm),

   123      ([], Res)] => ()

   124   | _ => error "diff.behav.in ctree.sml: get_interval lev 1f";

   126 case map fst (get_interval ([1,3],Res) ([4,1,1],Frm) 99999 pt) of

   127     [([1, 3], Res),

   128      ([1, 4], Res),

   129      ([1], Res),

   130      ([2], Res),

   131      ([3], Res),

   132      ([4], Pbl),

   133      ([4, 1], Frm),

   134      ([4, 1, 1], Frm)] => ()

   135   | _ => error "diff.behav.in ctree.sml: get_interval lev 1a";

   137 (*this pos' is not generated bu move_dn:......vvv: goes to end of calc*)

   138 case map fst (get_interval ([2],Res) ([4,3,2],Frm) 99999 pt) of

   139     [([2], Res),

   140      ([3], Res),

   141      ([4], Pbl),

   142      ([4, 1], Frm),

   143      ([4, 1, 1], Frm),

   144      ([4, 1, 1], Res),

   145      ([4, 1], Res),

   146      ([4, 2], Res),

   147      ([4, 3], Pbl),

   148      ([4, 3, 1], Frm),

   149      ([4, 3, 1], Res),

   150      ([4, 3, 2], Res),

   151      ([4, 3, 3], Res),(*this is beyond 'to'*)

   152      ([4, 3, 4], Res),(*this is beyond 'to'*)

   153      ([4, 3, 5], Res),(*this is beyond 'to'*)

   154      ([4, 3], Res),   (*this is beyond 'to'*)

   155      ([4], Res),      (*this is beyond 'to'*)

   156      ([5], Res),      (*this is beyond 'to'*)

   157      ([], Res)] => () (*this is beyond 'to'*)

   158   | _ => error "diff.behav.in ctree.sml: get_interval lev 1b";

   159 case map fst (get_interval ([1,4],Res) ([4,3,1],Frm) 99999 pt) of

   160     [([1, 4], Res),

   161      ([1], Res),

   162      ([2], Res),

   163      ([3], Res),

   164      ([4], Pbl),

   165      ([4, 1], Frm),

   166      ([4, 1, 1], Frm),

   167      ([4, 1, 1], Res),

   168      ([4, 1], Res),

   169      ([4, 2], Res),

   170      ([4, 3], Pbl),

   171      ([4, 3, 1], Frm)] => ()

   172   | _ => error "diff.behav.in ctree.sml: get_interval lev 1c";

   173 case map fst (get_interval ([4,2],Res) ([5],Res) 99999 pt) of

   174     [([4, 2], Res),

   175      ([4, 3], Pbl),

   176      ([4, 3, 1], Frm),

   177      ([4, 3, 1], Res),

   178      ([4, 3, 2], Res),

   179      ([4, 3, 3], Res),

   180      ([4, 3, 4], Res),

   181      ([4, 3, 5], Res),

   182      ([4, 3], Res),

   183      ([4], Res),

   184      ([5], Res)]=>()

   185   | _ => error "diff.behav.in ctree.sml: get_interval lev 1d";

   186 case map fst (get_interval ([],Frm) ([4,3,2],Res) 99999 pt) of

   187     [([], Frm),

   188      ([1], Frm),

   189      ([1, 1], Frm),

   190      ([1, 1], Res),

   191      ([1, 2], Res),

   192      ([1, 3], Res),

   193      ([1, 4], Res),

   194      ([1], Res),

   195      ([2], Res),

   196      ([3], Res),

   197      ([4], Pbl),

   198      ([4, 1], Frm),

   199      ([4, 1, 1], Frm),

   200      ([4, 1, 1], Res),

   201      ([4, 1], Res),

   202      ([4, 2], Res),

   203      ([4, 3], Pbl),

   204      ([4, 3, 1], Frm),

   205      ([4, 3, 1], Res),

   206      ([4, 3, 2], Res)] => ()

   207   | _ => error "diff.behav.in ctree.sml: get_interval lev 1e";

   208 case map fst (get_interval ([4,3],Frm) ([4,3],Res) 99999 pt) of

   209     [([4, 3], Frm),

   210      ([4, 3, 1], Frm),

   211      ([4, 3, 1], Res),

   212      ([4, 3, 2], Res),

   213      ([4, 3, 3], Res),

   214      ([4, 3, 4], Res),

   215      ([4, 3, 5], Res),

   216      ([4, 3], Res)] => ()

   217   | _ => error "diff.behav.in ctree.sml: get_interval lev 1g";

   222 "=====new ctree 2 without changes ================================";

   223 "=====new ctree 2 without changes ================================";

   224 "=====new ctree 2 without changes ================================";

   225 reset_states ();

   226 CalcTree

   227 [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",

   228 	   "solveFor x","solutions L"],

   229   ("RatEq",["univariate","equation"],["no_met"]))];

   230 Iterator 1; moveActiveRoot 1;

   231 autoCalculate 1 CompleteCalc;

   232 val ((pt,_),_) = get_calc 1;

   233 val p = get_pos 1 1;

   234 val (Form f, tac, asms) = pt_extract (pt, p);

   235 if term2str f = "[x = 6 / 5]" andalso p = ([], Res) then ()

   236   else error "after ===new ctree 2 without changes ===";

   237 writeln(pr_ctree pr_short pt);

   240 "-------------- getFormulaeFromTo --------------------------------";

   241 "-------------- getFormulaeFromTo --------------------------------";

   242 "-------------- getFormulaeFromTo --------------------------------";

   243 getFormulaeFromTo 1 ([4, 2], Res) ([4, 4], Pbl) 000;

   244 (*

   245 "@@@@@begin@@@@@" //...................................................

   246 + " 1" //..............................................................

   247 + "<GETELEMENTSFROMTO>" //...................................................

   248 + "  <CALCID> 1 </CALCID>" //..........................................

   249 + "  <POSFORMHEADS>" //................................................

   250 + "    <POSFORM>" //...................................................

   251 + "      <GENERATED>" //...............................................

   252 + "        <INTLIST>" //...............................................

   253 + "          <INT> 4 </INT>" //........................................

   254 + "          <INT> 3 </INT>" //........................................

   255 + "        </INTLIST>" //..............................................

   256 + "        <POS> Res </POS>" //........................................

   257 + "      </GENERATED>" //..............................................

   258 + "      <FORMULA>" //.................................................

   259 + "        <MATHML>" //................................................

   260 + "          <ISA> -6 * x + 5 * x ^^^ 2 = 0 </ISA>" //.................

   261 + "        </MATHML>" //...............................................

   262 + "      </FORMULA>" //................................................

   263 + "    </POSFORM>" //..................................................

   264 + "    <POSHEAD>" //...................................................

   265 + "      <GENERATED>" //...............................................

   266 + "        <INTLIST>" //...............................................

   267 + "          <INT> 4 </INT>" //........................................

   268 + "          <INT> 4 </INT>" //........................................

   269 + "        </INTLIST>" //..............................................

   270 + "        <POS> Pbl </POS>" //........................................

   271 + "      </GENERATED>" //..............................................

   272 + "      <CALCHEAD status = "correct">" //.............................

   273 + "       <HEAD>" //...................................................

   274 + "         <MATHML>" //...............................................

   275 + "           <ISA> solve (-6 * x + 5 * x ^^^ 2 = 0, x) </ISA>" //.....

   276 + "         </MATHML>" //..............................................

   277 + "       </HEAD>" //..................................................

   278 + "        <MODEL>" //.................................................

   279 + "          <GIVEN>" //...............................................

   280 + "            <ITEM status="correct">" //.............................

   281 + "              <MATHML>" //..........................................

   282 + "                <ISA> equality (-6 * x + 5 * x ^^^ 2 = 0) </ISA>" //

   283 + "              </MATHML>" //.........................................

   284 + "            </ITEM>" //.............................................

   285 + "            <ITEM status="correct">" //.............................

   286 + "              <MATHML>" //..........................................

   287 + "                <ISA> solveFor x </ISA>" //.........................

   288 + "              </MATHML>" //.........................................

   289 + "            </ITEM>" //.............................................

   290 + "          </GIVEN>" //..............................................

   291 + "          <WHERE>" //...............................................

   292 + "            <ITEM status="correct">" //.............................

   293 + "              <MATHML>" //..........................................

   294 + "                <ISA> matches (?a * ?v_ + ?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) |"

   295 + "matches (?v_ + ?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) |" //......

   296 + "matches (?v_ + ?b * ?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) |"

   297 + "matches (?a * ?v_ + ?b * ?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) |"

   298 + "matches (?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) |" //............

   299 + "matches (?b * ?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) </ISA>" //..

   300 + "              </MATHML>" //.........................................

   301 + "            </ITEM>" //.............................................

   302 + "          </WHERE>" //..............................................

   303 + "          <FIND>" //................................................

   304 + "            <ITEM status="correct">" //.............................

   305 + "              <MATHML>" //..........................................

   306 + "                <ISA> solutions x_i </ISA>" //......................

   307 + "              </MATHML>" //.........................................

   308 + "            </ITEM>" //.............................................

   309 + "          </FIND>" //...............................................

   310 + "          <RELATE>  </RELATE>" //...................................

   311 + "        </MODEL>" //................................................

   312 + "        <BELONGSTO> Pbl </BELONGSTO>" //............................

   313 + "        <SPECIFICATION>" //.........................................

   314 + "          <THEORYID> PolyEq.thy </THEORYID>" //.....................

   315 + "          <PROBLEMID>" //...........................................

   316 + "            <STRINGLIST>" //........................................

   317 + "              <STRING> bdv_only </STRING>" //.......................

   318 + "              <STRING> degree_2 </STRING>" //.......................

   319 + "              <STRING> polynomial </STRING>" //.....................

   320 + "              <STRING> univariate </STRING>" //.....................

   321 + "              <STRING> equation </STRING>" //.......................

   322 + "            </STRINGLIST>" //.......................................

   323 + "          </PROBLEMID>" //..........................................

   324 + "          <METHODID>" //............................................

   325 + "            <STRINGLIST>" //........................................

   326 + "              <STRING> PolyEq </STRING>" //.........................

   327 + "              <STRING> solve_d2_polyeq_bdvonly_equation </STRING>"

   328 + "            </STRINGLIST>" //.......................................

   329 + "          </METHODID>" //...........................................

   330 + "        </SPECIFICATION>" //........................................

   331 + "      </CALCHEAD>" //...............................................

   332 + "    </POSHEAD>" //..................................................

   333 + "  <POSFORMHEADS>" //................................................

   334 + "</GETELEMENTSFROMTO>" //..................................................

   335 + "@@@@@end@@@@@"

   336 *)

   339 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";

   340 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";

   341 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";

   342  val c = [];

   343  val (p,_,f,nxt,_,pt) = CalcTreeTEST

   344      [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],

   345        ("Test",

   346 	["LINEAR","univariate","equation","test"],

   347 	["Test","solve_linear"]))];

   348  val (p,_,f,nxt,_,pt) = me nxt p c pt;

   349  val (p,_,f,nxt,_,pt) = me nxt p c pt;

   350  (*xt = Add_Given "solveFor x"*)

   351  writeln (itms2str_ ctxt (get_obj g_pbl pt (fst p)));

   352 (*[

   353 (0 ,[] ,false ,#Given ,Inc solveFor ,(??.empty, [])),

   354 (0 ,[] ,false ,#Find ,Inc solutions [] ,(??.empty, [])),

   355 (1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0]))]*)

   356  val (pt,p) = complete_mod (pt, p);

   357  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 ()

   358  else error "completetest.sml: new behav. in complete_mod 1";

   359  writeln (itms2str_ ctxt (get_obj g_pbl pt (fst p)));

   360 (*[

   361 (1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),

   362 (2 ,[1] ,true ,#Given ,Cor solveFor x ,(solveFor, [x])),

   363 (3 ,[1] ,true ,#Find ,Cor solutions L ,(solutions, [L]))]*)

   364  val mits = get_obj g_met pt (fst p);

   365  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]))]"

   366  then () else error "completetest.sml: new behav. in complete_mod 2";

   367  writeln (itms2str_ ctxt mits);

   368 (*[

   369 (1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),

   370 (2 ,[1] ,true ,#Given ,Cor solveFor x ,(solveFor, [x])),

   371 (3 ,[1] ,true ,#Find ,Cor solutions L ,(solutions, [L]))]*)

   375 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-";

   376 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-";

   377 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-";

   378  reset_states ();

   379  CalcTree      (*start of calculation, return No.1*)

   380      [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],

   381        ("Test",

   382 	["LINEAR","univariate","equation","test"],

   383 	["Test","solve_linear"]))];

   384  Iterator 1; moveActiveRoot 1;

   386 (*

   387  autoCalculate 1 CompleteCalcHead;

   388  autoCalculate 1 (Step 1);

   389  refFormula 1 (get_pos 1 1);

   391 ... works

   393  autoCalculate 1 CompleteCalcHead;

   394  fetchProposedTactic 1; (*-> Apply_Method*);

   395  setNextTactic 1 (Apply_Method ["Test","solve_linear"]);

   396  autoCalculate 1 (Step 1);

   397  refFormula 1 (get_pos 1 1);

   399 ... works *)

   401  autoCalculate 1 (Step 1);

   402  refFormula 1 (get_pos 1 1);

   404  autoCalculate 1 CompleteModel;

   405  refFormula 1 (get_pos 1 1);

   407  autoCalculate 1 CompleteCalcHead;

   408 (* *** complete_mod: only impl.for Pbl, called with ([], Met) FIXXXXXXXXXXME*)

   412 "--------- maximum-example: complete_metitms ---------------------";

   413 "--------- maximum-example: complete_metitms ---------------------";

   414 "--------- maximum-example: complete_metitms ---------------------";

   415  val (p,_,f,nxt,_,pt) =

   416      CalcTreeTEST

   417      [(["fixedValues [r=Arbfix]","maximum A",

   418 	"valuesFor [a,b]",

   419 	"relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",

   420 	"relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",

   421 	"relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",

   423 	"boundVariable a","boundVariable b","boundVariable alpha",

   424 	"interval {x::real. 0 <= x & x <= 2*r}",

   425 	"interval {x::real. 0 <= x & x <= 2*r}",

   426 	"interval {x::real. 0 <= x & x <= pi}",

   427 	"errorBound (eps=(0::real))"],

   428        ("DiffApp",["maximum_of","function"],["DiffApp","max_by_calculus"])

   429        )];

   430  val (p,_,f,nxt,_,pt) = me nxt p c pt;

   431  val (p,_,f,nxt,_,pt) = me nxt p c pt;

   432  val (p,_,f,nxt,_,pt) = me nxt p c pt;

   433  val (p,_,f,nxt,_,pt) = me nxt p c pt;

   434  val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => OldGoals.print_exn e;

   435  val (p,_,f,nxt,_,pt) = me nxt p c pt;

   436  val (p,_,f,nxt,_,pt) = me nxt p c pt;

   437  (*nxt = Specify_Theory "DiffApp"*)

   438  val (oris, _, _) = get_obj g_origin pt (fst p);

   439  writeln (oris2str oris);

   440 (*[

   441 (1, ["1","2","3"], #Given,fixedValues, ["[r = Arbfix]"]),

   442 (2, ["1","2","3"], #Find,maximum, ["A"]),

   443 (3, ["1","2","3"], #Find,valuesFor, ["[a]","[b]"]),

   444 (4, ["1","2"], #Relate,relations, ["[A = a * b]","[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]"]),

   445 (5, ["3"], #Relate,relations, ["[A = a * b]","[a / 2 = r * sin alpha]","[b / 2 = r * cos alpha]"]),

   446 (6, ["1"], #undef,boundVariable, ["a"]),

   447 (7, ["2"], #undef,boundVariable, ["b"]),

   448 (8, ["3"], #undef,boundVariable, ["alpha"]),

   449 (9, ["1","2"], #undef,interval, ["{x. 0 <= x & x <= 2 * r}"]),

   450 (10, ["3"], #undef,interval, ["{x. 0 <= x & x <= pi}"]),

   451 (11, ["1","2","3"], #undef,errorBound, ["eps = 0"])]*)

   452  val pits = get_obj g_pbl pt (fst p);

   453  writeln (itms2str_ ctxt pits);

   454 (*[

   455 (1 ,[1,2,3] ,true,#Given ,Cor fixedValues [r = Arbfix],(fix_, [[r = Arbfix]])),

   456 (2 ,[1,2,3] ,true,#Find ,Cor maximum A ,(m_, [A])),

   457 (3 ,[1,2,3] ,true,#Find ,Cor valuesFor [a, b] ,(vs_, [[a, b]])),

   458 (4 ,[1,2] ,true,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^

   459 2 = r ^^^ 2] ,(rs_, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]*)

   460  val mits = get_obj g_met pt (fst p);

   461  val mits = complete_metitms oris pits []

   462 			((#ppc o get_met) ["DiffApp","max_by_calculus"]);

   463  writeln (itms2str_ ctxt mits);

   464 (*[

   465 (1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),

   466 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),

   467 (3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a, b]])),

   468 (4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^

   469 2 = r ^^^ 2] ,(rs_, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),

   470 (6 ,[1] ,true ,#undef ,Cor boundVariable a ,(boundVariable, [a])),

   471 (9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x.

   472 0 <= x & x <= 2 * r}])),

   473 (11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*)

   474  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 ()

   475  else error "completetest.sml: new behav. in complete_metitms 1";

   478 "--------- maximum-example: complete_mod -------------------------";

   479 "--------- maximum-example: complete_mod -------------------------";

   480 "--------- maximum-example: complete_mod -------------------------";

   481  val (p,_,f,nxt,_,pt) =

   482      CalcTreeTEST

   483      [(["fixedValues [r=Arbfix]","maximum A",

   484 	"valuesFor [a,b]",

   485 	"relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",

   486 	"relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",

   487 	"relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",

   489 	"boundVariable a","boundVariable b","boundVariable alpha",

   490 	"interval {x::real. 0 <= x & x <= 2*r}",

   491 	"interval {x::real. 0 <= x & x <= 2*r}",

   492 	"interval {x::real. 0 <= x & x <= pi}",

   493 	"errorBound (eps=(0::real))"],

   494        ("DiffApp",["maximum_of","function"],["DiffApp","max_by_calculus"])

   495        )];

   496  val (p,_,f,nxt,_,pt) = me nxt p c pt;

   497  val (p,_,f,nxt,_,pt) = me nxt p c pt;

   498  val (p,_,f,nxt,_,pt) = me nxt p c pt;

   499  (*nxt = nxt = Add_Find "valuesFor [a]" FIXME.12.03 +handle Inc !*)

   500  val pits = get_obj g_pbl pt (fst p);

   501  writeln (itms2str_ ctxt pits);

   502 (*[

   503 (0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),

   504 (0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, [])),

   505 (1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),

   506 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A]))]*)

   507  val (pt,p) = complete_mod (pt,p);

   508  val pits = get_obj g_pbl pt (fst p);

   509  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]]))]"

   510  then () else error "completetest.sml: new behav. in complete_mod 3";

   511  writeln (itms2str_ ctxt pits);

   512 (*[

   513 (1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),

   514 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),

   515 (3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])),

   516 (4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^

   517 2 = r ^^^ 2] ,(relations, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]*)

   518  val mits = get_obj g_met pt (fst p);

   519  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]))]"

   520  then () else error "completetest.sml: new behav. in complete_mod 3";

   521  writeln (itms2str_ ctxt mits);

   522 (*[

   523 (1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),

   524 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),

   525 (3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])),

   526 (4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^

   527 2 = r ^^^ 2] ,(relations, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),

   528 (6 ,[1] ,true ,#undef ,Cor boundVariable a ,(boundVariable, [a])),

   529 (9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x.

   530 0 <= x & x <= 2 * r}])),

   531 (11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*)

author	Walther Neuper <wneuper@ist.tugraz.at>
	Thu, 22 Dec 2016 11:36:20 +0100
changeset 59279	255c853ea2f0
parent 59248	5eba5e6d5266
child 59582	23984b62804f
permissions	-rw-r--r--