Mercurial Mercurial > wneuper > isa / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
test/Tools/isac/Interpret/inform.sml
branchisac-update-Isa09-2
changeset 38031 460c24a6a6ba
parent 37967 bd4f7a35e892
child 38050 4c52ad406c20
equal deleted inserted replaced
38030:95d956108461 38031:460c24a6a6ba 
    62  appendFormula 1 "-2 * 1 + (1 + x) = 0"; refFormula 1 (get_pos 1 1);
 
    62  appendFormula 1 "-2 * 1 + (1 + x) = 0"; refFormula 1 (get_pos 1 1);
 
    63  val ((pt,_),_) = get_calc 1;
 
    63  val ((pt,_),_) = get_calc 1;
 
    64  val str = pr_ptree pr_short pt;
 
    64  val str = pr_ptree pr_short pt;
 
    65  writeln str;
 
    65  writeln str;
 
    66  if str = ".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 + -1 * 2 = 0\n2.1.   x + 1 + -1 * 2 = 0\n2.2.   -1 * 2 + (x + 1) = 0\n2.3.   -1 * 2 + (1 + x) = 0\n2.4.   1 + (-1 * 2 + x) = 0\n2.5.   1 + (-2 + x) = 0\n2.6.   1 + (-2 * 1 + x) = 0\n" then ()
 
    66  if str = ".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 + -1 * 2 = 0\n2.1.   x + 1 + -1 * 2 = 0\n2.2.   -1 * 2 + (x + 1) = 0\n2.3.   -1 * 2 + (1 + x) = 0\n2.4.   1 + (-1 * 2 + x) = 0\n2.5.   1 + (-2 + x) = 0\n2.6.   1 + (-2 * 1 + x) = 0\n" then ()
 
    67  else raise error "inform.sml: diff.behav.appendFormula: on Res + equ 1";
 
    67  else error "inform.sml: diff.behav.appendFormula: on Res + equ 1";
 
    68 
    68 
    69  moveDown 1 ([ ],Pbl); refFormula 1 ([1],Frm); (*x + 1 = 2*)
 
    69  moveDown 1 ([ ],Pbl); refFormula 1 ([1],Frm); (*x + 1 = 2*)
 
    70  moveDown 1 ([1],Frm); refFormula 1 ([1],Res); (*x + 1 + -1 * 2 = 0*)
 
    70  moveDown 1 ([1],Frm); refFormula 1 ([1],Res); (*x + 1 + -1 * 2 = 0*)
 
    71 
    71 
    72  (*the seven steps of detailed derivation*)
 
    72  (*the seven steps of detailed derivation*)
 
    77  moveDown 1 ([2,3],Res); refFormula 1 ([2,4],Res);
 
    77  moveDown 1 ([2,3],Res); refFormula 1 ([2,4],Res);
 
    78  moveDown 1 ([2,4],Res); refFormula 1 ([2,5],Res);
 
    78  moveDown 1 ([2,4],Res); refFormula 1 ([2,5],Res);
 
    79  moveDown 1 ([2,5],Res); refFormula 1 ([2,6],Res);
 
    79  moveDown 1 ([2,5],Res); refFormula 1 ([2,6],Res);
 
    80  val ((pt,_),_) = get_calc 1;
 
    80  val ((pt,_),_) = get_calc 1;
 
    81  if "-2 * 1 + (1 + x) = 0" = term2str (fst (get_obj g_result pt [2,6])) then()
 
    81  if "-2 * 1 + (1 + x) = 0" = term2str (fst (get_obj g_result pt [2,6])) then()
 
    82  else raise error "inform.sml: diff.behav.appendFormula: on Res + equ 2";
 
    82  else error "inform.sml: diff.behav.appendFormula: on Res + equ 2";
 
    83 
    83 
    84  fetchProposedTactic 1; (*takes Iterator 1 _1_*)
 
    84  fetchProposedTactic 1; (*takes Iterator 1 _1_*)
 
    85  val (_,(tac,_,_)::_) = get_calc 1;
 
    85  val (_,(tac,_,_)::_) = get_calc 1;
 
    86  if tac = Rewrite_Set "Test_simplify" then ()
 
    86  if tac = Rewrite_Set "Test_simplify" then ()
 
    87  else raise error "inform.sml: diff.behav.appendFormula: on Res + equ 3";
 
    87  else error "inform.sml: diff.behav.appendFormula: on Res + equ 3";
 
    88  autoCalculate 1 CompleteCalc;
 
    88  autoCalculate 1 CompleteCalc;
 
    89  val ((pt,_),_) = get_calc 1;
 
    89  val ((pt,_),_) = get_calc 1;
 
    90  if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
 
    90  if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
 
    91  else raise error "inform.sml: diff.behav.appendFormula: on Res + equ 4";
 
    91  else error "inform.sml: diff.behav.appendFormula: on Res + equ 4";
 
    92  (* autoCalculate 1 CompleteCalc;
 
    92  (* autoCalculate 1 CompleteCalc;
 
    93    val ((pt,p),_) = get_calc 1;
 
    93    val ((pt,p),_) = get_calc 1;
 
    94    (writeln o istates2str) (get_obj g_loc pt [ ]);  
    94    (writeln o istates2str) (get_obj g_loc pt [ ]);  
    95    (writeln o istates2str) (get_obj g_loc pt [1]);  
    95    (writeln o istates2str) (get_obj g_loc pt [1]);  
    96    (writeln o istates2str) (get_obj g_loc pt [2]);  
    96    (writeln o istates2str) (get_obj g_loc pt [2]);  
   142  moveDown 1 ([1,3],Res); refFormula 1 ([1,4],Res); 
   142  moveDown 1 ([1,3],Res); refFormula 1 ([1,4],Res); 
   143  moveDown 1 ([1,4],Res); refFormula 1 ([1,5],Res); 
   143  moveDown 1 ([1,4],Res); refFormula 1 ([1,5],Res); 
   144  moveDown 1 ([1,5],Res); refFormula 1 ([1,6],Res); 
   144  moveDown 1 ([1,5],Res); refFormula 1 ([1,6],Res); 
   145  val ((pt,_),_) = get_calc 1;
 
   145  val ((pt,_),_) = get_calc 1;
 
   146  if "2 + -1 + x = 2" = term2str (fst (get_obj g_result pt [1,6])) then()
 
   146  if "2 + -1 + x = 2" = term2str (fst (get_obj g_result pt [1,6])) then()
 
   147  else raise error "inform.sml: diff.behav.appendFormula: on Frm + equ 1";
 
   147  else error "inform.sml: diff.behav.appendFormula: on Frm + equ 1";
 
   148 
   148 
   149  fetchProposedTactic 1; (*takes Iterator 1 _1_*)
 
   149  fetchProposedTactic 1; (*takes Iterator 1 _1_*)
 
   150  val (_,(tac,_,_)::_) = get_calc 1;
 
   150  val (_,(tac,_,_)::_) = get_calc 1;
 
   151  if tac = Rewrite_Set "norm_equation" then ()
 
   151  if tac = Rewrite_Set "norm_equation" then ()
 
   152  else raise error "inform.sml: diff.behav.appendFormula: on Frm + equ 2";
 
   152  else error "inform.sml: diff.behav.appendFormula: on Frm + equ 2";
 
   153  autoCalculate 1 CompleteCalc;
 
   153  autoCalculate 1 CompleteCalc;
 
   154  val ((pt,_),_) = get_calc 1;
 
   154  val ((pt,_),_) = get_calc 1;
 
   155  if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
 
   155  if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
 
   156  else raise error "inform.sml: diff.behav.appendFormula: on Frm + equ 3";
 
   156  else error "inform.sml: diff.behav.appendFormula: on Frm + equ 3";
 
   157 
   157 
   158 
   158 
   159 "--------- appendFormula: on Res + NO deriv ----------------------";
 
   159 "--------- appendFormula: on Res + NO deriv ----------------------";
 
   160 "--------- appendFormula: on Res + NO deriv ----------------------";
 
   160 "--------- appendFormula: on Res + NO deriv ----------------------";
 
   161 "--------- appendFormula: on Res + NO deriv ----------------------";
 
   161 "--------- appendFormula: on Res + NO deriv ----------------------";
 
   173  val ((pt,p),_) = get_calc 1;
 
   173  val ((pt,p),_) = get_calc 1;
 
   174  val str = pr_ptree pr_short pt;
 
   174  val str = pr_ptree pr_short pt;
 
   175  writeln str;
 
   175  writeln str;
 
   176  if str = ".    ----- pblobj -----\n1.   x + 1 = 2\n" andalso p = ([1], Res)
 
   176  if str = ".    ----- pblobj -----\n1.   x + 1 = 2\n" andalso p = ([1], Res)
 
   177  then ()
 
   177  then ()
 
   178  else raise error "inform.sml: diff.behav.appendFormula: Res + NOder 1";
 
   178  else error "inform.sml: diff.behav.appendFormula: Res + NOder 1";
 
   179 
   179 
   180  fetchProposedTactic 1;
 
   180  fetchProposedTactic 1;
 
   181  val (_,(tac,_,_)::_) = get_calc 1;
 
   181  val (_,(tac,_,_)::_) = get_calc 1;
 
   182  if tac = Rewrite_Set "Test_simplify" then ()
 
   182  if tac = Rewrite_Set "Test_simplify" then ()
 
   183  else raise error "inform.sml: diff.behav.appendFormula: Res + NOder 2";
 
   183  else error "inform.sml: diff.behav.appendFormula: Res + NOder 2";
 
   184  autoCalculate 1 CompleteCalc;
 
   184  autoCalculate 1 CompleteCalc;
 
   185  val ((pt,_),_) = get_calc 1;
 
   185  val ((pt,_),_) = get_calc 1;
 
   186  if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
 
   186  if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
 
   187  else raise error "inform.sml: diff.behav.appendFormula: on Frm + equ 3";
 
   187  else error "inform.sml: diff.behav.appendFormula: on Frm + equ 3";
 
   188 
   188 
   189 
   189 
   190 "--------- appendFormula: on Res + late deriv --------------------";
 
   190 "--------- appendFormula: on Res + late deriv --------------------";
 
   191 "--------- appendFormula: on Res + late deriv --------------------";
 
   191 "--------- appendFormula: on Res + late deriv --------------------";
 
   192 "--------- appendFormula: on Res + late deriv --------------------";
 
   192 "--------- appendFormula: on Res + late deriv --------------------";
 
   204  val ((pt,p),_) = get_calc 1;
 
   204  val ((pt,p),_) = get_calc 1;
 
   205  val str = pr_ptree pr_short pt;
 
   205  val str = pr_ptree pr_short pt;
 
   206  writeln str;
 
   206  writeln str;
 
   207  if str = ".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 + -1 * 2 = 0\n3.    ----- pblobj -----\n3.1.   -1 + x = 0\n3.2.   x = 0 + -1 * -1\n3.2.1.   x = 0 + -1 * -1\n3.2.2.   x = 0 + 1\n" andalso p = ([3,2], Res)
 
   207  if str = ".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 + -1 * 2 = 0\n3.    ----- pblobj -----\n3.1.   -1 + x = 0\n3.2.   x = 0 + -1 * -1\n3.2.1.   x = 0 + -1 * -1\n3.2.2.   x = 0 + 1\n" andalso p = ([3,2], Res)
 
   208  then () (*finds 1 step too early: ([3,2], Res) "x = 1" also by script !!!*)
 
   208  then () (*finds 1 step too early: ([3,2], Res) "x = 1" also by script !!!*)
 
   209  else raise error "inform.sml: diff.behav.appendFormula: Res + late d 1";
 
   209  else error "inform.sml: diff.behav.appendFormula: Res + late d 1";
 
   210  
   210  
   211  fetchProposedTactic 1;
 
   211  fetchProposedTactic 1;
 
   212  val (_,(tac,_,_)::_) = get_calc 1;
 
   212  val (_,(tac,_,_)::_) = get_calc 1;
 
   213  if tac = Check_Postcond ["linear", "univariate", "equation", "test"] then ()
 
   213  if tac = Check_Postcond ["linear", "univariate", "equation", "test"] then ()
 
   214  else raise error "inform.sml: diff.behav.appendFormula: Res + late d 2";
 
   214  else error "inform.sml: diff.behav.appendFormula: Res + late d 2";
 
   215  autoCalculate 1 CompleteCalc;
 
   215  autoCalculate 1 CompleteCalc;
 
   216  val ((pt,_),_) = get_calc 1;
 
   216  val ((pt,_),_) = get_calc 1;
 
   217  if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
 
   217  if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
 
   218  else raise error "inform.sml: diff.behav.appendFormula: Res + late d 3";
 
   218  else error "inform.sml: diff.behav.appendFormula: Res + late d 3";
 
   219 
   219 
   220 
   220 
   221 "--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
 
   221 "--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
 
   222 "--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
 
   222 "--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
 
   223 "--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
 
   223 "--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
 
   233  appendFormula 1 "[x = 3 + -2*1]";
 
   233  appendFormula 1 "[x = 3 + -2*1]";
 
   234  val ((pt,p),_) = get_calc 1;
 
   234  val ((pt,p),_) = get_calc 1;
 
   235  val str = pr_ptree pr_short pt;
 
   235  val str = pr_ptree pr_short pt;
 
   236  writeln str;
 
   236  writeln str;
 
   237  if str=".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 + -1 * 2 = 0\n3.    ----- pblobj -----\n3.1.   -1 + x = 0\n3.2.   x = 0 + -1 * -1\n4.   [x = 1]\n4.1.   [x = 1]\n4.2.   [x = -2 + 3]\n4.3.   [x = 3 + -2]\n" then ()
 
   237  if str=".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 + -1 * 2 = 0\n3.    ----- pblobj -----\n3.1.   -1 + x = 0\n3.2.   x = 0 + -1 * -1\n4.   [x = 1]\n4.1.   [x = 1]\n4.2.   [x = -2 + 3]\n4.3.   [x = 3 + -2]\n" then ()
 
   238  else raise error "inform.sml: diff.behav.appendFormula: Res + latEE 1";
 
   238  else error "inform.sml: diff.behav.appendFormula: Res + latEE 1";
 
   239  autoCalculate 1 CompleteCalc;
 
   239  autoCalculate 1 CompleteCalc;
 
   240  val ((pt,p),_) = get_calc 1;
 
   240  val ((pt,p),_) = get_calc 1;
 
   241  if "[x = 3 + -2 * 1]" = term2str (fst (get_obj g_result pt [])) then ()
 
   241  if "[x = 3 + -2 * 1]" = term2str (fst (get_obj g_result pt [])) then ()
 
   242  (*       ~~~~~~~~~~ simplify as last step in any script ?!*)
 
   242  (*       ~~~~~~~~~~ simplify as last step in any script ?!*)
 
   243  else raise error "inform.sml: diff.behav.appendFormula: Res + latEE 2";
 
   243  else error "inform.sml: diff.behav.appendFormula: Res + latEE 2";
 
   244 
   244 
   245 
   245 
   246 
   246 
   247 "--------- replaceFormula: on Res + = ----------------------------";
 
   247 "--------- replaceFormula: on Res + = ----------------------------";
 
   248 "--------- replaceFormula: on Res + = ----------------------------";
 
   248 "--------- replaceFormula: on Res + = ----------------------------";
 
   261  replaceFormula 1 "-2 * 1 + (1 + x) = 0"; refFormula 1 (get_pos 1 1);
 
   261  replaceFormula 1 "-2 * 1 + (1 + x) = 0"; refFormula 1 (get_pos 1 1);
 
   262  val ((pt,_),_) = get_calc 1;
 
   262  val ((pt,_),_) = get_calc 1;
 
   263  val str = pr_ptree pr_short pt;
 
   263  val str = pr_ptree pr_short pt;
 
   264  writeln str;
 
   264  writeln str;
 
   265  if str=".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 + -1 * 2 = 0\n2.1.   x + 1 + -1 * 2 = 0\n2.2.   -1 * 2 + (x + 1) = 0\n2.3.   -1 * 2 + (1 + x) = 0\n2.4.   1 + (-1 * 2 + x) = 0\n2.5.   1 + (-2 + x) = 0\n2.6.   1 + (-2 * 1 + x) = 0\n" then()
 
   265  if str=".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 + -1 * 2 = 0\n2.1.   x + 1 + -1 * 2 = 0\n2.2.   -1 * 2 + (x + 1) = 0\n2.3.   -1 * 2 + (1 + x) = 0\n2.4.   1 + (-1 * 2 + x) = 0\n2.5.   1 + (-2 + x) = 0\n2.6.   1 + (-2 * 1 + x) = 0\n" then()
 
   266  else raise error "inform.sml: diff.behav.replaceFormula: on Res += 1";
 
   266  else error "inform.sml: diff.behav.replaceFormula: on Res += 1";
 
   267  autoCalculate 1 CompleteCalc;
 
   267  autoCalculate 1 CompleteCalc;
 
   268  val ((pt,pos as(p,_)),_) = get_calc 1;
 
   268  val ((pt,pos as(p,_)),_) = get_calc 1;
 
   269  if pos=([],Res)andalso"[x = 1]"=(term2str o fst)(get_obj g_result pt p)then()
 
   269  if pos=([],Res)andalso"[x = 1]"=(term2str o fst)(get_obj g_result pt p)then()
 
   270  else raise error "inform.sml: diff.behav.replaceFormula: on Res + = 2";
 
   270  else error "inform.sml: diff.behav.replaceFormula: on Res + = 2";
 
   271  
   271  
   272 
   272 
   273 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
 
   273 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
 
   274 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
 
   274 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
 
   275 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
 
   275 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
 
   286  replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
 
   286  replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
 
   287  val ((pt,_),_) = get_calc 1;
 
   287  val ((pt,_),_) = get_calc 1;
 
   288  val str = pr_ptree pr_short pt;
 
   288  val str = pr_ptree pr_short pt;
 
   289  writeln str;
 
   289  writeln str;
 
   290  if str=".    ----- pblobj -----\n1.   x + 1 = 2\n1.1.   x + 1 = 2\n1.2.   1 + x = 2\n1.3.   1 + x = -2 + 4\n1.4.   x + 1 = -2 + 4\n" then ()
 
   290  if str=".    ----- pblobj -----\n1.   x + 1 = 2\n1.1.   x + 1 = 2\n1.2.   1 + x = 2\n1.3.   1 + x = -2 + 4\n1.4.   x + 1 = -2 + 4\n" then ()
 
   291  else raise error "inform.sml: diff.behav.replaceFormula: on Res 1 + = 1";
 
   291  else error "inform.sml: diff.behav.replaceFormula: on Res 1 + = 1";
 
   292  autoCalculate 1 CompleteCalc;
 
   292  autoCalculate 1 CompleteCalc;
 
   293  val ((pt,pos as(p,_)),_) = get_calc 1;
 
   293  val ((pt,pos as(p,_)),_) = get_calc 1;
 
   294  if pos=([],Res)andalso"[x = 1]"=(term2str o fst)(get_obj g_result pt p)then()
 
   294  if pos=([],Res)andalso"[x = 1]"=(term2str o fst)(get_obj g_result pt p)then()
 
   295  else raise error "inform.sml: diff.behav.replaceFormula: on Res + = 2";
 
   295  else error "inform.sml: diff.behav.replaceFormula: on Res + = 2";
 
   296 
   296 
   297 
   297 
   298 "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
 
   298 "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
 
   299 "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
 
   299 "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
 
   300 "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
 
   300 "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
 
   310  replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
 
   310  replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
 
   311  val ((pt,_),_) = get_calc 1;
 
   311  val ((pt,_),_) = get_calc 1;
 
   312  val str = pr_ptree pr_short pt;
 
   312  val str = pr_ptree pr_short pt;
 
   313  writeln str;
 
   313  writeln str;
 
   314  if str=".    ----- pblobj -----\n1.   x + 1 = 2\n1.1.   x + 1 = 2\n1.2.   1 + x = 2\n1.3.   1 + x = -2 + 4\n1.4.   x + 1 = -2 + 4\n" then ()
 
   314  if str=".    ----- pblobj -----\n1.   x + 1 = 2\n1.1.   x + 1 = 2\n1.2.   1 + x = 2\n1.3.   1 + x = -2 + 4\n1.4.   x + 1 = -2 + 4\n" then ()
 
   315  else raise error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 1";
 
   315  else error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 1";
 
   316  autoCalculate 1 CompleteCalc;
 
   316  autoCalculate 1 CompleteCalc;
 
   317  val ((pt,pos as(p,_)),_) = get_calc 1;
 
   317  val ((pt,pos as(p,_)),_) = get_calc 1;
 
   318  if pos=([],Res)andalso"[x = 1]"=(term2str o fst)(get_obj g_result pt p)then()
 
   318  if pos=([],Res)andalso"[x = 1]"=(term2str o fst)(get_obj g_result pt p)then()
 
   319  else raise error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 2";
 
   319  else error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 2";
 
   320 
   320 
   321 
   321 
   322 "--------- replaceFormula: cut calculation -----------------------";
 
   322 "--------- replaceFormula: cut calculation -----------------------";
 
   323 "--------- replaceFormula: cut calculation -----------------------";
 
   323 "--------- replaceFormula: cut calculation -----------------------";
 
   324 "--------- replaceFormula: cut calculation -----------------------";
 
   324 "--------- replaceFormula: cut calculation -----------------------";
 
   329 	     ["Test","squ-equ-test-subpbl1"]))];
 
   329 	     ["Test","squ-equ-test-subpbl1"]))];
 
   330  Iterator 1; moveActiveRoot 1;
 
   330  Iterator 1; moveActiveRoot 1;
 
   331  autoCalculate 1 CompleteCalc;
 
   331  autoCalculate 1 CompleteCalc;
 
   332  moveActiveRoot 1; moveActiveDown 1;
 
   332  moveActiveRoot 1; moveActiveDown 1;
 
   333  if get_pos 1 1 = ([1], Frm) then ()
 
   333  if get_pos 1 1 = ([1], Frm) then ()
 
   334  else raise error "inform.sml: diff.behav. cut calculation 1";
 
   334  else error "inform.sml: diff.behav. cut calculation 1";
 
   335 
   335 
   336  replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
 
   336  replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
 
   337  val ((pt,p),_) = get_calc 1;
 
   337  val ((pt,p),_) = get_calc 1;
 
   338  val str = pr_ptree pr_short pt;
 
   338  val str = pr_ptree pr_short pt;
 
   339  writeln str;
 
   339  writeln str;
 
   340  if p = ([1], Res) then ()
 
   340  if p = ([1], Res) then ()
 
   341  else raise error "inform.sml: diff.behav. cut calculation 2";
 
   341  else error "inform.sml: diff.behav. cut calculation 2";
 
   342 
   342 
   343 
   343 
   344 
   344 
   345 (* 040307 copied from informtest.sml; ... old version 
   345 (* 040307 copied from informtest.sml; ... old version 
   346  "---------------- maximum-example, UC: Modeling / modifyCalcHead -";
 
   346  "---------------- maximum-example, UC: Modeling / modifyCalcHead -";
 
   383 (0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))]*)
 
   383 (0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))]*)
 
   384 
   384 
   385  (*the empty CalcHead is checked w.r.t the model and re-established as such*)
 
   385  (*the empty CalcHead is checked w.r.t the model and re-established as such*)
 
   386  val (b,pt,ocalhd) = input_icalhd pt (p,"", empty_model, Pbl, e_spec);
 
   386  val (b,pt,ocalhd) = input_icalhd pt (p,"", empty_model, Pbl, e_spec);
 
   387  val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl; 
   387  val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl; 
   388  if ocalhd2str ocalhd = "(Pbl, ??.empty, [\n(0 ,[] ,false ,#Given ,Inc fixedValues [] ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),\n(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))], [], \n(\"e_domID\", [\"e_pblID\"], [\"e_metID\"]) )" then () else raise error "informtest.sml: diff.behav. max 1";
 
   388  if ocalhd2str ocalhd = "(Pbl, ??.empty, [\n(0 ,[] ,false ,#Given ,Inc fixedValues [] ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),\n(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))], [], \n(\"e_domID\", [\"e_pblID\"], [\"e_metID\"]) )" then () else error "informtest.sml: diff.behav. max 1";
 
   389 
   389 
   390  (*there is one input to the model (could be more)*)
 
   390  (*there is one input to the model (could be more)*)
 
   391  val (b,pt,ocalhd) = 
   391  val (b,pt,ocalhd) = 
   392      input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"],
 
   392      input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"],
 
   393 			     Find ["maximum", "valuesFor"],
 
   393 			     Find ["maximum", "valuesFor"],
 
   394 			     Relate ["relations"]], Pbl, e_spec);
 
   394 			     Relate ["relations"]], Pbl, e_spec);
 
   395  val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl; 
   395  val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl; 
   396  if ocalhd2str ocalhd = "(Pbl, ??.empty, [\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),\n(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))], [], \n(\"e_domID\", [\"e_pblID\"], [\"e_metID\"]) )" then () 
   396  if ocalhd2str ocalhd = "(Pbl, ??.empty, [\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),\n(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))], [], \n(\"e_domID\", [\"e_pblID\"], [\"e_metID\"]) )" then () 
   397  else raise error "informtest.sml: diff.behav. max 2";
 
   397  else error "informtest.sml: diff.behav. max 2";
 
   398 
   398 
   399  (*this input is complete in variant 3, but the ME doesn't recognize FIXXXXME
 
   399  (*this input is complete in variant 3, but the ME doesn't recognize FIXXXXME
 
   400  val (b,pt''''',ocalhd) = 
   400  val (b,pt''''',ocalhd) = 
   401      input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"],
 
   401      input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"],
 
   402 			     Find ["maximum A", "valuesFor [a,b]"],
 
   402 			     Find ["maximum A", "valuesFor [a,b]"],
 
   433  appendFormula 1 " x - "; (*<ERROR> syntax error in ' x - ' </ERROR>*)
 
   433  appendFormula 1 " x - "; (*<ERROR> syntax error in ' x - ' </ERROR>*)
 
   434  val ((pt,_),_) = get_calc 1;
 
   434  val ((pt,_),_) = get_calc 1;
 
   435  val str = pr_ptree pr_short pt;
 
   435  val str = pr_ptree pr_short pt;
 
   436  writeln str;
 
   436  writeln str;
 
   437  if str = ".    ----- pblobj -----\n1.   x + 1 = 2\n" then ()
 
   437  if str = ".    ----- pblobj -----\n1.   x + 1 = 2\n" then ()
 
   438  else raise error "inform.sml: diff.behav.appendFormula: syntax error";
 
   438  else error "inform.sml: diff.behav.appendFormula: syntax error";
 
   439 
   439 
   440 
   440 
   441 "--------- CAS-command on ([],Pbl) -------------------------------";
 
   441 "--------- CAS-command on ([],Pbl) -------------------------------";
 
   442 "--------- CAS-command on ([],Pbl) -------------------------------";
 
   442 "--------- CAS-command on ([],Pbl) -------------------------------";
 
   443 "--------- CAS-command on ([],Pbl) -------------------------------";
 
   443 "--------- CAS-command on ([],Pbl) -------------------------------";
 
   447 val (_,(_,c,(pt,p))) = inform ([],[],(pt,p)) "solve(x+1=2,x)";
 
   447 val (_,(_,c,(pt,p))) = inform ([],[],(pt,p)) "solve(x+1=2,x)";
 
   448 show_pt pt;
 
   448 show_pt pt;
 
   449 val nxt = ("Apply_Method",Apply_Method ["Test","squ-equ-test-subpbl1"]);
 
   449 val nxt = ("Apply_Method",Apply_Method ["Test","squ-equ-test-subpbl1"]);
 
   450 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   450 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   451 if p = ([1], Frm) andalso f2str f = "x + 1 = 2" then ()
 
   451 if p = ([1], Frm) andalso f2str f = "x + 1 = 2" then ()
 
   452 else raise error "inform.sml: diff.behav. CAScmd ([],Pbl)";
 
   452 else error "inform.sml: diff.behav. CAScmd ([],Pbl)";
 
   453 
   453 
   454 
   454 
   455 "--------- CAS-command on ([],Pbl) FE-interface ------------------";
 
   455 "--------- CAS-command on ([],Pbl) FE-interface ------------------";
 
   456 "--------- CAS-command on ([],Pbl) FE-interface ------------------";
 
   456 "--------- CAS-command on ([],Pbl) FE-interface ------------------";
 
   457 "--------- CAS-command on ([],Pbl) FE-interface ------------------";
 
   457 "--------- CAS-command on ([],Pbl) FE-interface ------------------";
 
   462 replaceFormula 1 "solve(x+1=2,x)";
 
   462 replaceFormula 1 "solve(x+1=2,x)";
 
   463 autoCalculate 1 CompleteCalc;
 
   463 autoCalculate 1 CompleteCalc;
 
   464 val ((pt,p),_) = get_calc 1;
 
   464 val ((pt,p),_) = get_calc 1;
 
   465 show_pt pt;
 
   465 show_pt pt;
 
   466 if p = ([], Res) then ()
 
   466 if p = ([], Res) then ()
 
   467 else raise error "inform.sml: diff.behav. CAScmd ([],Pbl) FE-interface";
 
   467 else error "inform.sml: diff.behav. CAScmd ([],Pbl) FE-interface";
 
   468 
   468 
   469 
   469 
   470 "--------- inform [rational,simplification] ----------------------";
 
   470 "--------- inform [rational,simplification] ----------------------";
 
   471 "--------- inform [rational,simplification] ----------------------";
 
   471 "--------- inform [rational,simplification] ----------------------";
 
   472 "--------- inform [rational,simplification] ----------------------";
 
   472 "--------- inform [rational,simplification] ----------------------";
 
   482 autoCalculate 1 (Step 1);
 
   482 autoCalculate 1 (Step 1);
 
   483 "--- input the next formula that _should_ be presented by mat-engine";
 
   483 "--- input the next formula that _should_ be presented by mat-engine";
 
   484 appendFormula 1 "(4 * y + -3 * x) / (x * y) + -1";
 
   484 appendFormula 1 "(4 * y + -3 * x) / (x * y) + -1";
 
   485 val ((pt,p),_) = get_calc 1;
 
   485 val ((pt,p),_) = get_calc 1;
 
   486 if p = ([4], Res) andalso (length o children o (get_nd pt)) (fst p) = 2 then ()
 
   486 if p = ([4], Res) andalso (length o children o (get_nd pt)) (fst p) = 2 then ()
 
   487 else raise error ("inform.sml: [rational,simplification] 1");
 
   487 else error ("inform.sml: [rational,simplification] 1");
 
   488 
   488 
   489 "--- input the next formula that would be presented by mat-engine";
 
   489 "--- input the next formula that would be presented by mat-engine";
 
   490 (*autoCalculate 1 (Step 1);*)
 
   490 (*autoCalculate 1 (Step 1);*)
 
   491 appendFormula 1 "(4 * y + -3 * x + -1 * (x * y)) / (x * y)";
 
   491 appendFormula 1 "(4 * y + -3 * x + -1 * (x * y)) / (x * y)";
 
   492 val ((pt,p),_) = get_calc 1;
 
   492 val ((pt,p),_) = get_calc 1;
 
   493 if p = ([5], Res) andalso (length o children o (get_nd pt)) (fst p) = 0 then ()
 
   493 if p = ([5], Res) andalso (length o children o (get_nd pt)) (fst p) = 0 then ()
 
   494 else raise error ("inform.sml: [rational,simplification] 2");
 
   494 else error ("inform.sml: [rational,simplification] 2");
 
   495 
   495 
   496 "--- input the exact final result";(*TODO: Exception- LIST "last_elem" raised*)
 
   496 "--- input the exact final result";(*TODO: Exception- LIST "last_elem" raised*)
 
   497 appendFormula 1 "(-3 * x + 4 * y + -1 * x * y) / (x * y)";
 
   497 appendFormula 1 "(-3 * x + 4 * y + -1 * x * y) / (x * y)";
 
   498 val ((pt,p),_) = get_calc 1;
 
   498 val ((pt,p),_) = get_calc 1;
 
   499 if p = ([6], Res) andalso (length o children o (get_nd pt)) (fst p) = 2 then ()
 
   499 if p = ([6], Res) andalso (length o children o (get_nd pt)) (fst p) = 2 then ()
 
   500 else raise error ("inform.sml: [rational,simplification] 3");
 
   500 else error ("inform.sml: [rational,simplification] 3");
 
   501 show_pt pt;
 
   501 show_pt pt;
 
   502 
   502 
   503 "--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
 
   503 "--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
 
   504 "--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
 
   504 "--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
 
   505 "--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
 
   505 "--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
 
   563 autoCalculate 1 CompleteCalc;
 
   563 autoCalculate 1 CompleteCalc;
 
   564 val ((pt,p),_) = get_calc 1;
 
   564 val ((pt,p),_) = get_calc 1;
 
   565 val Form res = (#1 o pt_extract) (pt, ([],Res));
 
   565 val Form res = (#1 o pt_extract) (pt, ([],Res));
 
   566 show_pt pt;
 
   566 show_pt pt;
 
   567 if p = ([], Res) andalso term2str res = "1 + 2 * x" then ()
 
   567 if p = ([], Res) andalso term2str res = "1 + 2 * x" then ()
 
   568 else raise error "diff.sml behav.changed for Diff (x^2 + x + 1, x)";
 
   568 else error "diff.sml behav.changed for Diff (x^2 + x + 1, x)";
 
   569 
   569 
   570 
   570 
   571 "--------- Take as 1st tac, start from exp -----------------------";
 
   571 "--------- Take as 1st tac, start from exp -----------------------";
 
   572 "--------- Take as 1st tac, start from exp -----------------------";
 
   572 "--------- Take as 1st tac, start from exp -----------------------";
 
   573 "--------- Take as 1st tac, start from exp -----------------------";
 
   573 "--------- Take as 1st tac, start from exp -----------------------";
 
   607 
   607 
   608 autoCalculate 1 (Step 1);
 
   608 autoCalculate 1 (Step 1);
 
   609 val ((pt,p),_) = get_calc 1;
 
   609 val ((pt,p),_) = get_calc 1;
 
   610 val Form res = (#1 o pt_extract) (pt, p);
 
   610 val Form res = (#1 o pt_extract) (pt, p);
 
   611 if term2str res = "d_d x (x ^^^ 2 + x + 1)" then ()
 
   611 if term2str res = "d_d x (x ^^^ 2 + x + 1)" then ()
 
   612 else raise error "diff.sml Diff (x^2 + x + 1, x) from exp";
 
   612 else error "diff.sml Diff (x^2 + x + 1, x) from exp";
 
   613 
   613 
   614 
   614 
   615 "--------- init_form, start with <NEW> (CAS input) ---------------";
 
   615 "--------- init_form, start with <NEW> (CAS input) ---------------";
 
   616 "--------- init_form, start with <NEW> (CAS input) ---------------";
 
   616 "--------- init_form, start with <NEW> (CAS input) ---------------";
 
   617 "--------- init_form, start with <NEW> (CAS input) ---------------";
 
   617 "--------- init_form, start with <NEW> (CAS input) ---------------";
wneuper/isa