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/Frontend/interface.sml
branchisac-update-Isa09-2
changeset 38031 460c24a6a6ba
parent 37960 ec20007095f2
child 38050 4c52ad406c20
equal deleted inserted replaced
38030:95d956108461 38031:460c24a6a6ba 
    58 
    58 
    59 "--------- encode ^ -> ^^^ ---------------------------------------";
 
    59 "--------- encode ^ -> ^^^ ---------------------------------------";
 
    60 "--------- encode ^ -> ^^^ ---------------------------------------";
 
    60 "--------- encode ^ -> ^^^ ---------------------------------------";
 
    61 "--------- encode ^ -> ^^^ ---------------------------------------";
 
    61 "--------- encode ^ -> ^^^ ---------------------------------------";
 
    62 if encode "a^2+b^2=c^2" = "a^^^2+b^^^2=c^^^2" then ()
 
    62 if encode "a^2+b^2=c^2" = "a^^^2+b^^^2=c^^^2" then ()
 
    63 else raise error "interface.sml: diff.behav. in encode ^ -> ^^^ ";
 
    63 else error "interface.sml: diff.behav. in encode ^ -> ^^^ ";
 
    64 
    64 
    65 if (decode o encode) "a^2+b^2=c^2" = "a^2+b^2=c^2" then ()
 
    65 if (decode o encode) "a^2+b^2=c^2" = "a^2+b^2=c^2" then ()
 
    66 else raise error "interface.sml: diff.behav. in de/encode ^ <-> ^^^ ";
 
    66 else error "interface.sml: diff.behav. in de/encode ^ <-> ^^^ ";
 
    67 
    67 
    68 ==================================================================*)
 
    68 ==================================================================*)
 
    69 "exported from struct --------------------------------------------";
 
    69 "exported from struct --------------------------------------------";
 
    70 "exported from struct --------------------------------------------";
 
    70 "exported from struct --------------------------------------------";
 
    71 "exported from struct --------------------------------------------";
 
    71 "exported from struct --------------------------------------------";
 
   165  val ((pt,_),_) = get_calc 1;
 
   165  val ((pt,_),_) = get_calc 1;
 
   166  val ip = get_pos 1 1;
 
   166  val ip = get_pos 1 1;
 
   167  val (Form f, tac, asms) = pt_extract (pt, ip);
 
   167  val (Form f, tac, asms) = pt_extract (pt, ip);
 
   168      (*exception just above means: 'ModSpec' has been returned: error anyway*)
 
   168      (*exception just above means: 'ModSpec' has been returned: error anyway*)
 
   169  if term2str f = "[x = 1]" then () else 
   169  if term2str f = "[x = 1]" then () else 
   170  raise error "FE-Kernel-interface.sml: diff.behav. in solve_linear as rootpbl";
 
   170  error "FE-Kernel-interface.sml: diff.behav. in solve_linear as rootpbl";
 
   171 
   171 
   172 
   172 
   173 
   173 
   174 "--------- inspect the CalcTree No.1 with Iterator No.2 ---------";
 
   174 "--------- inspect the CalcTree No.1 with Iterator No.2 ---------";
 
   175 "--------- inspect the CalcTree No.1 with Iterator No.2 ---------";
 
   175 "--------- inspect the CalcTree No.1 with Iterator No.2 ---------";
 
   186  moveActiveCalcHead 1; refFormula 1 ([],Pbl);
 
   186  moveActiveCalcHead 1; refFormula 1 ([],Pbl);
 
   187  moveActiveDown 1;
 
   187  moveActiveDown 1;
 
   188  moveActiveDown 1;
 
   188  moveActiveDown 1;
 
   189  moveActiveDown 1;
 
   189  moveActiveDown 1;
 
   190  if get_pos 1 1 = ([2], Res) then () else 
   190  if get_pos 1 1 = ([2], Res) then () else 
   191  raise error "FE-interface.sml: diff.behav. in a inspect 1 with Iterator 2";
 
   191  error "FE-interface.sml: diff.behav. in a inspect 1 with Iterator 2";
 
   192  moveActiveDown 1; refFormula 1 ([], Res);
 
   192  moveActiveDown 1; refFormula 1 ([], Res);
 
   193  if get_pos 1 1 = ([], Res) then () else 
   193  if get_pos 1 1 = ([], Res) then () else 
   194  raise error "FE-interface.sml: diff.behav. in b inspect 1 with Iterator 2";
 
   194  error "FE-interface.sml: diff.behav. in b inspect 1 with Iterator 2";
 
   195  moveActiveCalcHead 1; refFormula 1 ([],Pbl);
 
   195  moveActiveCalcHead 1; refFormula 1 ([],Pbl);
 
   196 
   196 
   197 
   197 
   198 
   198 
   199 "---------------- miniscript with mini-subpbl --------------------";
 
   199 "---------------- miniscript with mini-subpbl --------------------";
 
   315  writeln str;
 
   315  writeln str;
 
   316  val ip = get_pos 1 1;
 
   316  val ip = get_pos 1 1;
 
   317  val (Form f, tac, asms) = pt_extract (pt, ip);
 
   317  val (Form f, tac, asms) = pt_extract (pt, ip);
 
   318      (*exception just above means: 'ModSpec' has been returned: error anyway*)
 
   318      (*exception just above means: 'ModSpec' has been returned: error anyway*)
 
   319  if term2str f = "[x = 1]" then () else 
   319  if term2str f = "[x = 1]" then () else 
   320  raise error "FE-interface.sml: diff.behav. in miniscript with mini-subpb";
 
   320  error "FE-interface.sml: diff.behav. in miniscript with mini-subpb";
 
   321 
   321 
   322  DEconstrCalcTree 1;
 
   322  DEconstrCalcTree 1;
 
   323 
   323 
   324 
   324 
   325 "--------- miniscript with mini-subpbl AUTOCALCULATE Step 1-------";
 
   325 "--------- miniscript with mini-subpbl AUTOCALCULATE Step 1-------";
 
   370  (*this checks the test for correctness..*)
 
   370  (*this checks the test for correctness..*)
 
   371  val ((pt,_),_) = get_calc 1;
 
   371  val ((pt,_),_) = get_calc 1;
 
   372  val p = get_pos 1 1;
 
   372  val p = get_pos 1 1;
 
   373  val (Form f, tac, asms) = pt_extract (pt, p);
 
   373  val (Form f, tac, asms) = pt_extract (pt, p);
 
   374  if term2str f = "[x = 1]" andalso p = ([], Res) then () else 
   374  if term2str f = "[x = 1]" andalso p = ([], Res) then () else 
   375  raise error "FE-interface.sml: diff.behav. in miniscript with mini-subpb";
 
   375  error "FE-interface.sml: diff.behav. in miniscript with mini-subpb";
 
   376 
   376 
   377  DEconstrCalcTree 1;
 
   377  DEconstrCalcTree 1;
 
   378 
   378 
   379 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalc ----";
 
   379 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalc ----";
 
   380 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalc ----";
 
   380 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalc ----";
 
   395 
   395 
   396  val ((pt,_),_) = get_calc 1;
 
   396  val ((pt,_),_) = get_calc 1;
 
   397  val p = get_pos 1 1;
 
   397  val p = get_pos 1 1;
 
   398  val (Form f, tac, asms) = pt_extract (pt, p);
 
   398  val (Form f, tac, asms) = pt_extract (pt, p);
 
   399  if term2str f = "[x = 1]" andalso p = ([], Res) then () else 
   399  if term2str f = "[x = 1]" andalso p = ([], Res) then () else 
   400  raise error "FE-interface.sml: diff.behav. in solve_linear/rt AUTOCALCULATE ";
 
   400  error "FE-interface.sml: diff.behav. in solve_linear/rt AUTOCALCULATE ";
 
   401 
   401 
   402 
   402 
   403 "--------- solve_linear as rootpbl AUTOCALC CompleteHead/Calc ----";
 
   403 "--------- solve_linear as rootpbl AUTOCALC CompleteHead/Calc ----";
 
   404 "--------- solve_linear as rootpbl AUTOCALC CompleteHead/Calc ----";
 
   404 "--------- solve_linear as rootpbl AUTOCALC CompleteHead/Calc ----";
 
   405 "--------- solve_linear as rootpbl AUTOCALC CompleteHead/Calc ----";
 
   405 "--------- solve_linear as rootpbl AUTOCALC CompleteHead/Calc ----";
 
   418 
   418 
   419 
   419 
   420  autoCalculate 1 CompleteCalc; 
   420  autoCalculate 1 CompleteCalc; 
   421  val ((pt,p),_) = get_calc 1;
 
   421  val ((pt,p),_) = get_calc 1;
 
   422  if p=([], Res) then () else 
   422  if p=([], Res) then () else 
   423  raise error "FE-interface.sml: diff.behav. in solve_linear AUTOC Head/Calc ";
 
   423  error "FE-interface.sml: diff.behav. in solve_linear AUTOC Head/Calc ";
 
   424 
   424 
   425 
   425 
   426 "--------- miniscript with mini-subpbl AUTOCALCULATE CompleteCalc-";
 
   426 "--------- miniscript with mini-subpbl AUTOCALCULATE CompleteCalc-";
 
   427 "--------- miniscript with mini-subpbl AUTOCALCULATE CompleteCalc-";
 
   427 "--------- miniscript with mini-subpbl AUTOCALCULATE CompleteCalc-";
 
   428 "--------- miniscript with mini-subpbl AUTOCALCULATE CompleteCalc-";
 
   428 "--------- miniscript with mini-subpbl AUTOCALCULATE CompleteCalc-";
 
   450 
   450 
   451  val ((pt,_),_) = get_calc 1;
 
   451  val ((pt,_),_) = get_calc 1;
 
   452  val p = get_pos 1 1;
 
   452  val p = get_pos 1 1;
 
   453  val (Form f, tac, asms) = pt_extract (pt, p);
 
   453  val (Form f, tac, asms) = pt_extract (pt, p);
 
   454  if term2str f = "[x = 1]" andalso p = ([], Res) then () else 
   454  if term2str f = "[x = 1]" andalso p = ([], Res) then () else 
   455  raise error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
 
   455  error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
 
   456 
   456 
   457 
   457 
   458 "--------- miniscript with mini-subpbl AUTO CompleteCalcHead------";
 
   458 "--------- miniscript with mini-subpbl AUTO CompleteCalcHead------";
 
   459 "--------- miniscript with mini-subpbl AUTO CompleteCalcHead------";
 
   459 "--------- miniscript with mini-subpbl AUTO CompleteCalcHead------";
 
   460 "--------- miniscript with mini-subpbl AUTO CompleteCalcHead------";
 
   460 "--------- miniscript with mini-subpbl AUTO CompleteCalcHead------";
 
   493  refFormula 1 (get_pos 1 1);
 
   493  refFormula 1 (get_pos 1 1);
 
   494  val ((pt,_),_) = get_calc 1;
 
   494  val ((pt,_),_) = get_calc 1;
 
   495  if get_obj g_spec pt [] = ("e_domID", 
   495  if get_obj g_spec pt [] = ("e_domID", 
   496 			    ["linear", "univariate","equation","test"],
 
   496 			    ["linear", "univariate","equation","test"],
 
   497 			    ["Test","solve_linear"]) then ()
 
   497 			    ["Test","solve_linear"]) then ()
 
   498  else raise error "FE-interface.sml: diff.behav. in setProblem, setMethod";
 
   498  else error "FE-interface.sml: diff.behav. in setProblem, setMethod";
 
   499 
   499 
   500  autoCalculate 1 CompleteCalcHead;
 
   500  autoCalculate 1 CompleteCalcHead;
 
   501  refFormula 1 (get_pos 1 1); 
   501  refFormula 1 (get_pos 1 1); 
   502  autoCalculate 1 CompleteCalc; 
   502  autoCalculate 1 CompleteCalc; 
   503  moveActiveDown 1;
 
   503  moveActiveDown 1;
 
   506  refFormula 1 (get_pos 1 1); 
   506  refFormula 1 (get_pos 1 1); 
   507  val ((pt,_),_) = get_calc 1;
 
   507  val ((pt,_),_) = get_calc 1;
 
   508  val p = get_pos 1 1;
 
   508  val p = get_pos 1 1;
 
   509  val (Form f, tac, asms) = pt_extract (pt, p);
 
   509  val (Form f, tac, asms) = pt_extract (pt, p);
 
   510  if term2str f = "[x = 1]" andalso p = ([], Res) then () else 
   510  if term2str f = "[x = 1]" andalso p = ([], Res) then () else 
   511  raise error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
 
   511  error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
 
   512 
   512 
   513 
   513 
   514 "--------- setContext..Thy ---------------------------------------";
 
   514 "--------- setContext..Thy ---------------------------------------";
 
   515 "--------- setContext..Thy ---------------------------------------";
 
   515 "--------- setContext..Thy ---------------------------------------";
 
   516 "--------- setContext..Thy ---------------------------------------";
 
   516 "--------- setContext..Thy ---------------------------------------";
 
   556  val ((pt,_),_) = get_calc 1;
 
   556  val ((pt,_),_) = get_calc 1;
 
   557  val str = pr_ptree pr_short pt;
 
   557  val str = pr_ptree pr_short pt;
 
   558  writeln str;
 
   558  writeln str;
 
   559  if str = ".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 + -1 * 2 = 0\n"
 
   559  if str = ".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 + -1 * 2 = 0\n"
 
   560  then () else 
   560  then () else 
   561  raise error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl-1";
 
   561  error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl-1";
 
   562 
   562 
   563  autoCalculate 1 (Step 1); (*proceeds only, of NOT 1 step before subplb*)
 
   563  autoCalculate 1 (Step 1); (*proceeds only, of NOT 1 step before subplb*)
 
   564  autoCalculate 1 CompleteToSubpbl;
 
   564  autoCalculate 1 CompleteToSubpbl;
 
   565  val ((pt,_),_) = get_calc 1;
 
   565  val ((pt,_),_) = get_calc 1;
 
   566  val str = pr_ptree pr_short pt;
 
   566  val str = pr_ptree pr_short pt;
 
   568  autoCalculate 1 CompleteCalc; (*das geht ohnehin !*);
 
   568  autoCalculate 1 CompleteCalc; (*das geht ohnehin !*);
 
   569  val ((pt,_),_) = get_calc 1;
 
   569  val ((pt,_),_) = get_calc 1;
 
   570  val p = get_pos 1 1;
 
   570  val p = get_pos 1 1;
 
   571  val (Form f, tac, asms) = pt_extract (pt, p);
 
   571  val (Form f, tac, asms) = pt_extract (pt, p);
 
   572  if term2str f = "[x = 1]" andalso p = ([], Res) then () else 
   572  if term2str f = "[x = 1]" andalso p = ([], Res) then () else 
   573  raise error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl 1";
 
   573  error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl 1";
 
   574 
   574 
   575 
   575 
   576 
   576 
   577 "---------------- rat-eq + subpbl: no_met, NO solution dropped ---";
 
   577 "---------------- rat-eq + subpbl: no_met, NO solution dropped ---";
 
   578 "---------------- rat-eq + subpbl: no_met, NO solution dropped ---";
 
   578 "---------------- rat-eq + subpbl: no_met, NO solution dropped ---";
 
   775  val ((pt,_),_) = get_calc 1;
 
   775  val ((pt,_),_) = get_calc 1;
 
   776  show_pt pt;
 
   776  show_pt pt;
 
   777  val p = get_pos 1 1;
 
   777  val p = get_pos 1 1;
 
   778  val (Form f, tac, asms) = pt_extract (pt, p);
 
   778  val (Form f, tac, asms) = pt_extract (pt, p);
 
   779  if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else 
   779  if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else 
   780  raise error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
 
   780  error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
 
   781 
   781 
   782 (*------------^^^-inserted-----------------------------------------------*)
 
   782 (*------------^^^-inserted-----------------------------------------------*)
 
   783 (*WN050904 the fetchProposedTactic's below may not have worked like that
 
   783 (*WN050904 the fetchProposedTactic's below may not have worked like that
 
   784   before, too, because there was no check*)
 
   784   before, too, because there was no check*)
 
   785  fetchProposedTactic 1;
 
   785  fetchProposedTactic 1;
 
   798 rootthy pt;
 
   798 rootthy pt;
 
   799  show_pt pt;
 
   799  show_pt pt;
 
   800  val p = get_pos 1 1;
 
   800  val p = get_pos 1 1;
 
   801  val (Form f, tac, asms) = pt_extract (pt, p);
 
   801  val (Form f, tac, asms) = pt_extract (pt, p);
 
   802  if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else 
   802  if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else 
   803  raise error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
 
   803  error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
 
   804 
   804 
   805 
   805 
   806 "--------- modifyCalcHead, resetCalcHead, modelProblem ------------";
 
   806 "--------- modifyCalcHead, resetCalcHead, modelProblem ------------";
 
   807 "--------- modifyCalcHead, resetCalcHead, modelProblem ------------";
 
   807 "--------- modifyCalcHead, resetCalcHead, modelProblem ------------";
 
   808 "--------- modifyCalcHead, resetCalcHead, modelProblem ------------";
 
   808 "--------- modifyCalcHead, resetCalcHead, modelProblem ------------";
 
   937  refFormula 1 (get_pos 1 1);
 
   937  refFormula 1 (get_pos 1 1);
 
   938  val ((pt,_),_) = get_calc 1;
 
   938  val ((pt,_),_) = get_calc 1;
 
   939  val p = get_pos 1 1;
 
   939  val p = get_pos 1 1;
 
   940  val (Form f, tac, asms) = pt_extract (pt, p);
 
   940  val (Form f, tac, asms) = pt_extract (pt, p);
 
   941  if term2str f = "[x = 1]" andalso p = ([], Res) then () else 
   941  if term2str f = "[x = 1]" andalso p = ([], Res) then () else 
   942  raise error "FE-interface.sml: diff.behav. in from pbl-hierarchy";
 
   942  error "FE-interface.sml: diff.behav. in from pbl-hierarchy";
 
   943  
   943  
   944 
   944 
   945 
   945 
   946 "--------- solve_linear as in an algebra system (CAS)-------------";
 
   946 "--------- solve_linear as in an algebra system (CAS)-------------";
 
   947 "--------- solve_linear as in an algebra system (CAS)-------------";
 
   947 "--------- solve_linear as in an algebra system (CAS)-------------";
 
   955  refFormula 1 (get_pos 1 1);
 
   955  refFormula 1 (get_pos 1 1);
 
   956  val ((pt,_),_) = get_calc 1;
 
   956  val ((pt,_),_) = get_calc 1;
 
   957  val p = get_pos 1 1;
 
   957  val p = get_pos 1 1;
 
   958  val (Form f, tac, asms) = pt_extract (pt, p);
 
   958  val (Form f, tac, asms) = pt_extract (pt, p);
 
   959  if term2str f = "[x = 1]" andalso p = ([], Res) then () else 
   959  if term2str f = "[x = 1]" andalso p = ([], Res) then () else 
   960  raise error "FE-interface.sml: diff.behav. in algebra system";
 
   960  error "FE-interface.sml: diff.behav. in algebra system";
 
   961 
   961 
   962 
   962 
   963 
   963 
   964 "--------- interSteps: on 'miniscript with mini-subpbl' ----------";
 
   964 "--------- interSteps: on 'miniscript with mini-subpbl' ----------";
 
   965 "--------- interSteps: on 'miniscript with mini-subpbl' ----------";
 
   965 "--------- interSteps: on 'miniscript with mini-subpbl' ----------";
 
  1096  autoCalculate 1 CompleteCalc; 
  1096  autoCalculate 1 CompleteCalc; 
  1097  val ((pt,_),_) = get_calc 1;
 
  1097  val ((pt,_),_) = get_calc 1;
 
  1098  val p = get_pos 1 1;
 
  1098  val p = get_pos 1 1;
 
  1099  val (Form f, tac, asms) = pt_extract (pt, p);
 
  1099  val (Form f, tac, asms) = pt_extract (pt, p);
 
  1100  if term2str f = "[x = 1]" andalso p = ([], Res) then () else 
  1100  if term2str f = "[x = 1]" andalso p = ([], Res) then () else 
  1101  raise error "FE-interface.sml: diff.behav. in combinations of steps";
 
  1101  error "FE-interface.sml: diff.behav. in combinations of steps";
 
  1102 
  1102 
  1103 
  1103 
  1104 "--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} right--";
 
  1104 "--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} right--";
 
  1105 "--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} right--";
 
  1105 "--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} right--";
 
  1106 "--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} right--";
 
  1106 "--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} right--";
 
  1122 
  1122 
  1123  val ((pt,_),_) = get_calc 1;
 
  1123  val ((pt,_),_) = get_calc 1;
 
  1124  val p = get_pos 1 1;
 
  1124  val p = get_pos 1 1;
 
  1125  val (Form f, tac, asms) = pt_extract (pt, p);
 
  1125  val (Form f, tac, asms) = pt_extract (pt, p);
 
  1126  if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else 
  1126  if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else 
  1127  raise error "FE-interface.sml: diff.behav. in FORMULA:enter} right";
 
  1127  error "FE-interface.sml: diff.behav. in FORMULA:enter} right";
 
  1128 
  1128 
  1129 "--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} other--";
 
  1129 "--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} other--";
 
  1130 "--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} other--";
 
  1130 "--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} other--";
 
  1131 "--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} other--";
 
  1131 "--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} other--";
 
  1132  states:=[];
 
  1132  states:=[];
 
  1147 
  1147 
  1148  val ((pt,_),_) = get_calc 1;
 
  1148  val ((pt,_),_) = get_calc 1;
 
  1149  val p = get_pos 1 1;
 
  1149  val p = get_pos 1 1;
 
  1150  val (Form f, tac, asms) = pt_extract (pt, p);
 
  1150  val (Form f, tac, asms) = pt_extract (pt, p);
 
  1151  if term2str f = "x - 1 = 0" andalso p = ([2], Res) then () else 
  1151  if term2str f = "x - 1 = 0" andalso p = ([2], Res) then () else 
  1152  raise error "FE-interface.sml: diff.behav. in FORMULA:enter} other";
 
  1152  error "FE-interface.sml: diff.behav. in FORMULA:enter} other";
 
  1153 
  1153 
  1154 "--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} oth 2--";
 
  1154 "--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} oth 2--";
 
  1155 "--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} oth 2--";
 
  1155 "--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} oth 2--";
 
  1156 "--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} oth 2--";
 
  1156 "--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} oth 2--";
 
  1157  states:=[];
 
  1157  states:=[];
 
  1173 
  1173 
  1174  val ((pt,_),_) = get_calc 1;
 
  1174  val ((pt,_),_) = get_calc 1;
 
  1175  val p = get_pos 1 1;
 
  1175  val p = get_pos 1 1;
 
  1176  val (Form f, tac, asms) = pt_extract (pt, p);
 
  1176  val (Form f, tac, asms) = pt_extract (pt, p);
 
  1177  if term2str f = "x = 1" andalso p = ([3,2], Res) then () else 
  1177  if term2str f = "x = 1" andalso p = ([3,2], Res) then () else 
  1178  raise error "FE-interface.sml: diff.behav. in FORMULA:enter} oth 2";
 
  1178  error "FE-interface.sml: diff.behav. in FORMULA:enter} oth 2";
 
  1179 
  1179 
  1180 
  1180 
  1181 "--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} NOTok--";
 
  1181 "--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} NOTok--";
 
  1182 "--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} NOTok--";
 
  1182 "--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} NOTok--";
 
  1183 "--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} NOTok--";
 
  1183 "--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} NOTok--";
 
  1197 
  1197 
  1198  val ((pt,_),_) = get_calc 1;
 
  1198  val ((pt,_),_) = get_calc 1;
 
  1199  val p = get_pos 1 1;
 
  1199  val p = get_pos 1 1;
 
  1200  val (Form f, tac, asms) = pt_extract (pt, p);
 
  1200  val (Form f, tac, asms) = pt_extract (pt, p);
 
  1201  if term2str f = "x + 1 + -1 * 2 = 0" andalso p = ([1], Res) then () else 
  1201  if term2str f = "x + 1 + -1 * 2 = 0" andalso p = ([1], Res) then () else 
  1202  raise error "FE-interface.sml: diff.behav. in FORMULA:enter} NOTok";
 
  1202  error "FE-interface.sml: diff.behav. in FORMULA:enter} NOTok";
 
  1203 
  1203 
  1204 
  1204 
  1205 "--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} right----";
 
  1205 "--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} right----";
 
  1206 "--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} right----";
 
  1206 "--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} right----";
 
  1207 "--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} right----";
 
  1207 "--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} right----";
 
  1220 
  1220 
  1221  val ((pt,_),_) = get_calc 1;
 
  1221  val ((pt,_),_) = get_calc 1;
 
  1222  val p = get_pos 1 1;
 
  1222  val p = get_pos 1 1;
 
  1223  val (Form f, tac, asms) = pt_extract (pt, p);
 
  1223  val (Form f, tac, asms) = pt_extract (pt, p);
 
  1224  if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else 
  1224  if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else 
  1225  raise error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
 
  1225  error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
 
  1226  if map fst (get_interval ([2],Res) ([],Res) 9999 pt) = 
  1226  if map fst (get_interval ([2],Res) ([],Res) 9999 pt) = 
  1227     [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
 
  1227     [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
 
  1228      ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else
 
  1228      ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else
 
  1229  raise error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2";
 
  1229  error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2";
 
  1230  
  1230  
  1231 (*WN050211 replaceFormula didn't work on second ctree: thus now tested...*)
 
  1231 (*WN050211 replaceFormula didn't work on second ctree: thus now tested...*)
 
  1232  CalcTree
 
  1232  CalcTree
 
  1233  [(["equality (x+1=2)", "solveFor x","solutions L"], 
  1233  [(["equality (x+1=2)", "solveFor x","solutions L"], 
  1234    ("Test.thy", 
  1234    ("Test.thy", 
  1243 
  1243 
  1244  val ((pt,_),_) = get_calc 2;
 
  1244  val ((pt,_),_) = get_calc 2;
 
  1245  val p = get_pos 2 1;
 
  1245  val p = get_pos 2 1;
 
  1246  val (Form f, tac, asms) = pt_extract (pt, p);
 
  1246  val (Form f, tac, asms) = pt_extract (pt, p);
 
  1247  if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else 
  1247  if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else 
  1248  raise error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
 
  1248  error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
 
  1249  if map fst (get_interval ([2],Res) ([],Res) 9999 pt) = 
  1249  if map fst (get_interval ([2],Res) ([],Res) 9999 pt) = 
  1250     [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
 
  1250     [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
 
  1251      ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else
 
  1251      ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else
 
  1252  raise error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2b";
 
  1252  error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2b";
 
  1253 
  1253 
  1254 "--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} other----";
 
  1254 "--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} other----";
 
  1255 "--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} other----";
 
  1255 "--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} other----";
 
  1256 "--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} other----";
 
  1256 "--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} other----";
 
  1257  states:=[];
 
  1257  states:=[];
 
  1272  val ((pt,_),_) = get_calc 1;
 
  1272  val ((pt,_),_) = get_calc 1;
 
  1273  show_pt pt;
 
  1273  show_pt pt;
 
  1274  val p = get_pos 1 1;
 
  1274  val p = get_pos 1 1;
 
  1275  val (Form f, tac, asms) = pt_extract (pt, p);
 
  1275  val (Form f, tac, asms) = pt_extract (pt, p);
 
  1276  if term2str f = "x - 1 = 0" andalso p = ([2], Res) then () else 
  1276  if term2str f = "x - 1 = 0" andalso p = ([2], Res) then () else 
  1277  raise error "FE-interface.sml: diff.behav. in FORMULA:replace} other 1";
 
  1277  error "FE-interface.sml: diff.behav. in FORMULA:replace} other 1";
 
  1278 (* for getting the list in whole length ...
 
  1278 (* for getting the list in whole length ...
 
  1279 print_depth 99;map fst (get_interval ([1],Res) ([],Res) 9999 pt);print_depth 3;
 
  1279 print_depth 99;map fst (get_interval ([1],Res) ([],Res) 9999 pt);print_depth 3;
 
  1280    *)
 
  1280    *)
 
  1281  if map fst (get_interval ([1],Res) ([],Res) 9999 pt) = 
  1281  if map fst (get_interval ([1],Res) ([],Res) 9999 pt) = 
  1282     [([1], Res), ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
 
  1282     [([1], Res), ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
 
  1283       ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2, 7], Res),
 
  1283       ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2, 7], Res),
 
  1284       ([2, 8], Res), ([2, 9], Res), ([2], Res)
 
  1284       ([2, 8], Res), ([2, 9], Res), ([2], Res)
 
  1285 (*WN060727 {cutlevup->test_trans} removed: , 
  1285 (*WN060727 {cutlevup->test_trans} removed: , 
  1286       ([], Res)(*dropped, if test_trans doesnt stop at PblNd*)*)] then () else
 
  1286       ([], Res)(*dropped, if test_trans doesnt stop at PblNd*)*)] then () else
 
  1287  raise error "FE-interface.sml: diff.behav. in FORMULA:replace} other 2";
 
  1287  error "FE-interface.sml: diff.behav. in FORMULA:replace} other 2";
 
  1288 
  1288 
  1289 
  1289 
  1290 
  1290 
  1291 "--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} other 2--";
 
  1291 "--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} other 2--";
 
  1292 "--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} other 2--";
 
  1292 "--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} other 2--";
 
  1312  val (t,_) = get_obj g_result pt [3,2]; term2str t;
 
  1312  val (t,_) = get_obj g_result pt [3,2]; term2str t;
 
  1313   if map fst (get_interval ([1],Res) ([],Res) 9999 pt) = 
  1313   if map fst (get_interval ([1],Res) ([],Res) 9999 pt) = 
  1314     [([1], Res), ([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res),
 
  1314     [([1], Res), ([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res),
 
  1315       ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res), 
  1315       ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res), 
  1316       ([3,2],Res)] then () else
 
  1316       ([3,2],Res)] then () else
 
  1317  raise error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 1";
 
  1317  error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 1";
 
  1318 
  1318 
  1319  val p = get_pos 1 1;
 
  1319  val p = get_pos 1 1;
 
  1320  val (Form f, tac, asms) = pt_extract (pt, p);
 
  1320  val (Form f, tac, asms) = pt_extract (pt, p);
 
  1321  if term2str f = "x = 1" andalso p = ([3,2], Res) then () else 
  1321  if term2str f = "x = 1" andalso p = ([3,2], Res) then () else 
  1322  raise error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 2";
 
  1322  error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 2";
 
  1323 
  1323 
  1324 
  1324 
  1325 
  1325 
  1326 "--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} NOTok----";
 
  1326 "--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} NOTok----";
 
  1327 "--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} NOTok----";
 
  1327 "--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} NOTok----";
 
  1342  val ((pt,_),_) = get_calc 1;
 
  1342  val ((pt,_),_) = get_calc 1;
 
  1343  show_pt pt;
 
  1343  show_pt pt;
 
  1344  val p = get_pos 1 1;
 
  1344  val p = get_pos 1 1;
 
  1345  val (Form f, tac, asms) = pt_extract (pt, p);
 
  1345  val (Form f, tac, asms) = pt_extract (pt, p);
 
  1346  if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else 
  1346  if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else 
  1347  raise error "FE-interface.sml: diff.behav. in FORMULA:replace} NOTok";
 
  1347  error "FE-interface.sml: diff.behav. in FORMULA:replace} NOTok";
 
  1348 
  1348 
  1349 
  1349
wneuper/isa