test/Tools/isac/Interpret/me.sml
branchisac-update-Isa09-2
changeset 38031 460c24a6a6ba
parent 37960 ec20007095f2
child 38043 6a36acec95d9
equal deleted inserted replaced
38030:95d956108461 38031:460c24a6a6ba
   104      ([4, 3, 5], Res), 
   104      ([4, 3, 5], Res), 
   105      ([4, 3], Res), 
   105      ([4, 3], Res), 
   106      ([4], Res), 
   106      ([4], Res), 
   107      ([5], Res), 
   107      ([5], Res), 
   108      ([], Res)] => () 
   108      ([], Res)] => () 
   109   | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1f";
   109   | _ => error "diff.behav.in ctree.sml: get_interval lev 1f";
   110 case map fst (get_interval ([],Frm) ([],Res) 1 pt) of
   110 case map fst (get_interval ([],Frm) ([],Res) 1 pt) of
   111     [([], Frm), 
   111     [([], Frm), 
   112      ([1], Frm), 
   112      ([1], Frm), 
   113      ([1], Res), 
   113      ([1], Res), 
   114      ([2], Res), 
   114      ([2], Res), 
   115      ([3], Res),
   115      ([3], Res),
   116      ([4], Pbl), 
   116      ([4], Pbl), 
   117      ([4], Res), 
   117      ([4], Res), 
   118      ([5], Res), 
   118      ([5], Res), 
   119      ([], Res)] => () 
   119      ([], Res)] => () 
   120   | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1f";
   120   | _ => error "diff.behav.in ctree.sml: get_interval lev 1f";
   121 case map fst (get_interval ([],Frm) ([],Res) 0 pt) of
   121 case map fst (get_interval ([],Frm) ([],Res) 0 pt) of
   122     [([], Frm), 
   122     [([], Frm), 
   123      ([], Res)] => () 
   123      ([], Res)] => () 
   124   | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1f";
   124   | _ => error "diff.behav.in ctree.sml: get_interval lev 1f";
   125 
   125 
   126 case map fst (get_interval ([1,3],Res) ([4,1,1],Frm) 99999 pt) of
   126 case map fst (get_interval ([1,3],Res) ([4,1,1],Frm) 99999 pt) of
   127     [([1, 3], Res), 
   127     [([1, 3], Res), 
   128      ([1, 4], Res), 
   128      ([1, 4], Res), 
   129      ([1], Res), 
   129      ([1], Res), 
   130      ([2], Res), 
   130      ([2], Res), 
   131      ([3], Res),
   131      ([3], Res),
   132      ([4], Pbl), 
   132      ([4], Pbl), 
   133      ([4, 1], Frm), 
   133      ([4, 1], Frm), 
   134      ([4, 1, 1], Frm)] => () 
   134      ([4, 1, 1], Frm)] => () 
   135   | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1a";
   135   | _ => error "diff.behav.in ctree.sml: get_interval lev 1a";
   136 
   136 
   137 (*this pos' is not generated bu move_dn:......vvv: goes to end of calc*)
   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
   138 case map fst (get_interval ([2],Res) ([4,3,2],Frm) 99999 pt) of
   139     [([2], Res), 
   139     [([2], Res), 
   140      ([3], Res), 
   140      ([3], Res), 
   153      ([4, 3, 5], Res),(*this is beyond 'to'*) 
   153      ([4, 3, 5], Res),(*this is beyond 'to'*) 
   154      ([4, 3], Res),   (*this is beyond 'to'*)
   154      ([4, 3], Res),   (*this is beyond 'to'*)
   155      ([4], Res),      (*this is beyond 'to'*)
   155      ([4], Res),      (*this is beyond 'to'*)
   156      ([5], Res),      (*this is beyond 'to'*)
   156      ([5], Res),      (*this is beyond 'to'*)
   157      ([], Res)] => () (*this is beyond 'to'*)
   157      ([], Res)] => () (*this is beyond 'to'*)
   158   | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1b";
   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
   159 case map fst (get_interval ([1,4],Res) ([4,3,1],Frm) 99999 pt) of
   160     [([1, 4], Res), 
   160     [([1, 4], Res), 
   161      ([1], Res), 
   161      ([1], Res), 
   162      ([2], Res), 
   162      ([2], Res), 
   163      ([3], Res), 
   163      ([3], Res), 
   167      ([4, 1, 1], Res), 
   167      ([4, 1, 1], Res), 
   168      ([4, 1], Res),
   168      ([4, 1], Res),
   169      ([4, 2], Res), 
   169      ([4, 2], Res), 
   170      ([4, 3], Pbl), 
   170      ([4, 3], Pbl), 
   171      ([4, 3, 1], Frm)] => () 
   171      ([4, 3, 1], Frm)] => () 
   172   | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1c";
   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
   173 case map fst (get_interval ([4,2],Res) ([5],Res) 99999 pt) of
   174     [([4, 2], Res), 
   174     [([4, 2], Res), 
   175      ([4, 3], Pbl), 
   175      ([4, 3], Pbl), 
   176      ([4, 3, 1], Frm), 
   176      ([4, 3, 1], Frm), 
   177      ([4, 3, 1], Res),
   177      ([4, 3, 1], Res),
   180      ([4, 3, 4], Res), 
   180      ([4, 3, 4], Res), 
   181      ([4, 3, 5], Res),
   181      ([4, 3, 5], Res),
   182      ([4, 3], Res), 
   182      ([4, 3], Res), 
   183      ([4], Res), 
   183      ([4], Res), 
   184      ([5], Res)]=>()
   184      ([5], Res)]=>()
   185   | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1d";
   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
   186 case map fst (get_interval ([],Frm) ([4,3,2],Res) 99999 pt) of
   187     [([], Frm), 
   187     [([], Frm), 
   188      ([1], Frm), 
   188      ([1], Frm), 
   189      ([1, 1], Frm), 
   189      ([1, 1], Frm), 
   190      ([1, 1], Res), 
   190      ([1, 1], Res), 
   202      ([4, 2], Res), 
   202      ([4, 2], Res), 
   203      ([4, 3], Pbl), 
   203      ([4, 3], Pbl), 
   204      ([4, 3, 1], Frm),
   204      ([4, 3, 1], Frm),
   205      ([4, 3, 1], Res), 
   205      ([4, 3, 1], Res), 
   206      ([4, 3, 2], Res)] => () 
   206      ([4, 3, 2], Res)] => () 
   207   | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1e";
   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
   208 case map fst (get_interval ([4,3],Frm) ([4,3],Res) 99999 pt) of
   209     [([4, 3], Frm), 
   209     [([4, 3], Frm), 
   210      ([4, 3, 1], Frm), 
   210      ([4, 3, 1], Frm), 
   211      ([4, 3, 1], Res), 
   211      ([4, 3, 1], Res), 
   212      ([4, 3, 2], Res),
   212      ([4, 3, 2], Res),
   213      ([4, 3, 3], Res), 
   213      ([4, 3, 3], Res), 
   214      ([4, 3, 4], Res), 
   214      ([4, 3, 4], Res), 
   215      ([4, 3, 5], Res), 
   215      ([4, 3, 5], Res), 
   216      ([4, 3], Res)] => () 
   216      ([4, 3], Res)] => () 
   217   | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1g";
   217   | _ => error "diff.behav.in ctree.sml: get_interval lev 1g";
   218 
   218 
   219 
   219 
   220 
   220 
   221 
   221 
   222 "=====new ptree 2 without changes ================================";
   222 "=====new ptree 2 without changes ================================";
   349 (0 ,[] ,false ,#Given ,Inc solveFor ,(??.empty, [])),
   349 (0 ,[] ,false ,#Given ,Inc solveFor ,(??.empty, [])),
   350 (0 ,[] ,false ,#Find ,Inc solutions [] ,(??.empty, [])),
   350 (0 ,[] ,false ,#Find ,Inc solutions [] ,(??.empty, [])),
   351 (1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0]))]*)
   351 (1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0]))]*)
   352  val (pt,p) = complete_mod (pt, p);
   352  val (pt,p) = complete_mod (pt, p);
   353  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 ()
   353  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 ()
   354  else raise error "completetest.sml: new behav. in complete_mod 1";
   354  else error "completetest.sml: new behav. in complete_mod 1";
   355  writeln (itms2str_ ctxt (get_obj g_pbl pt (fst p)));   
   355  writeln (itms2str_ ctxt (get_obj g_pbl pt (fst p)));   
   356 (*[
   356 (*[
   357 (1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),
   357 (1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),
   358 (2 ,[1] ,true ,#Given ,Cor solveFor x ,(solveFor, [x])),
   358 (2 ,[1] ,true ,#Given ,Cor solveFor x ,(solveFor, [x])),
   359 (3 ,[1] ,true ,#Find ,Cor solutions L ,(solutions, [L]))]*)
   359 (3 ,[1] ,true ,#Find ,Cor solutions L ,(solutions, [L]))]*)
   360  val mits = get_obj g_met pt (fst p);
   360  val mits = get_obj g_met pt (fst p);
   361  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]))]" 
   361  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]))]" 
   362  then () else raise error "completetest.sml: new behav. in complete_mod 2";
   362  then () else error "completetest.sml: new behav. in complete_mod 2";
   363  writeln (itms2str_ ctxt mits);   
   363  writeln (itms2str_ ctxt mits);   
   364 (*[
   364 (*[
   365 (1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),
   365 (1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),
   366 (2 ,[1] ,true ,#Given ,Cor solveFor x ,(solveFor, [x])),
   366 (2 ,[1] ,true ,#Given ,Cor solveFor x ,(solveFor, [x])),
   367 (3 ,[1] ,true ,#Find ,Cor solutions L ,(solutions, [L]))]*)
   367 (3 ,[1] ,true ,#Find ,Cor solutions L ,(solutions, [L]))]*)
   466 (6 ,[1] ,true ,#undef ,Cor boundVariable a ,(boundVariable, [a])),
   466 (6 ,[1] ,true ,#undef ,Cor boundVariable a ,(boundVariable, [a])),
   467 (9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x.
   467 (9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x.
   468 0 <= x & x <= 2 * r}])),
   468 0 <= x & x <= 2 * r}])),
   469 (11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*)
   469 (11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*)
   470  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 ()
   470  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 ()
   471  else raise error "completetest.sml: new behav. in complete_metitms 1";
   471  else error "completetest.sml: new behav. in complete_metitms 1";
   472 
   472 
   473 
   473 
   474 "--------- maximum-example: complete_mod -------------------------";
   474 "--------- maximum-example: complete_mod -------------------------";
   475 "--------- maximum-example: complete_mod -------------------------";
   475 "--------- maximum-example: complete_mod -------------------------";
   476 "--------- maximum-example: complete_mod -------------------------";
   476 "--------- maximum-example: complete_mod -------------------------";
   501 (1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
   501 (1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
   502 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A]))]*) 
   502 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A]))]*) 
   503  val (pt,p) = complete_mod (pt,p);
   503  val (pt,p) = complete_mod (pt,p);
   504  val pits = get_obj g_pbl pt (fst p);
   504  val pits = get_obj g_pbl pt (fst p);
   505  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]]))]" 
   505  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]]))]" 
   506  then () else raise error "completetest.sml: new behav. in complete_mod 3";
   506  then () else error "completetest.sml: new behav. in complete_mod 3";
   507  writeln (itms2str_ ctxt pits);
   507  writeln (itms2str_ ctxt pits);
   508 (*[
   508 (*[
   509 (1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
   509 (1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
   510 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
   510 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
   511 (3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])),
   511 (3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])),
   512 (4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
   512 (4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
   513 2 = r ^^^ 2] ,(relations, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]*)
   513 2 = r ^^^ 2] ,(relations, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]*)
   514  val mits = get_obj g_met pt (fst p);
   514  val mits = get_obj g_met pt (fst p);
   515  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]))]" 
   515  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]))]" 
   516  then () else raise error "completetest.sml: new behav. in complete_mod 3";
   516  then () else error "completetest.sml: new behav. in complete_mod 3";
   517  writeln (itms2str_ ctxt mits);
   517  writeln (itms2str_ ctxt mits);
   518 (*[
   518 (*[
   519 (1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
   519 (1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
   520 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
   520 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
   521 (3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])),
   521 (3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])),