test/Tools/isac/Frontend/interface.sml
branchdecompose-isar
changeset 42048 6548da70f14e
parent 41971 329a5c90d0ab
child 42055 3da7095ac8d5
     1.1 --- a/test/Tools/isac/Frontend/interface.sml	Sat Jun 18 11:28:10 2011 +0200
     1.2 +++ b/test/Tools/isac/Frontend/interface.sml	Mon Jun 20 17:33:06 2011 +0200
     1.3 @@ -140,6 +140,7 @@
     1.4   val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
     1.5  
     1.6   setNextTactic 1 (Apply_Method ["Test","solve_linear"]);
     1.7 +   (*ERROR.110620 <SETNEXTTACTIC>..<MESSAGE> end-of-calculation*)
     1.8   val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
     1.9   is_complete_mod ptp;
    1.10   is_complete_spec ptp;
    1.11 @@ -167,8 +168,9 @@
    1.12       (*exception just above means: 'ModSpec' has been returned: error anyway*)
    1.13   if term2str f = "[x = 1]" then () else 
    1.14   error "FE-Kernel-interface.sml: diff.behav. in solve_linear as rootpbl";
    1.15 +============ inhibit exn 110310 ==============================================*)
    1.16  
    1.17 -
    1.18 +(*========== inhibit exn 110620 ================================================
    1.19  "--------- inspect the CalcTree No.1 with Iterator No.2 -";
    1.20  "--------- inspect the CalcTree No.1 with Iterator No.2 -";
    1.21  "--------- inspect the CalcTree No.1 with Iterator No.2 -";
    1.22 @@ -191,7 +193,7 @@
    1.23   if get_pos 1 1 = ([], Res) then () else 
    1.24   error "FE-interface.sml: diff.behav. in b inspect 1 with Iterator 2";
    1.25   moveActiveCalcHead 1; refFormula 1 ([],Pbl);
    1.26 -
    1.27 +============ inhibit exn 110620 ==============================================*)
    1.28  
    1.29  "--------- miniscript with mini-subpbl ------------------";
    1.30  "--------- miniscript with mini-subpbl ------------------";
    1.31 @@ -316,7 +318,6 @@
    1.32  
    1.33   DEconstrCalcTree 1;
    1.34  
    1.35 -
    1.36  "--------- mini-subpbl AUTOCALCULATE Step 1 -------------";
    1.37  "--------- mini-subpbl AUTOCALCULATE Step 1 -------------";
    1.38  "--------- mini-subpbl AUTOCALCULATE Step 1 -------------";
    1.39 @@ -369,6 +370,7 @@
    1.40  
    1.41   DEconstrCalcTree 1;
    1.42  
    1.43 +(*========== inhibit exn 110620 ================================================
    1.44  "--------- solve_linear as rootpbl AUTO CompleteCalc ----";
    1.45  "--------- solve_linear as rootpbl AUTO CompleteCalc ----";
    1.46  "--------- solve_linear as rootpbl AUTO CompleteCalc ----";
    1.47 @@ -392,7 +394,6 @@
    1.48   if term2str f = "[x = 1]" andalso p = ([], Res) then () else 
    1.49   error "FE-interface.sml: diff.behav. in solve_linear/rt AUTOCALCULATE ";
    1.50  
    1.51 -
    1.52  "--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
    1.53  "--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
    1.54  "--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
    1.55 @@ -408,13 +409,11 @@
    1.56   refFormula 1 (get_pos 1 1);
    1.57   val ((pt,p),_) = get_calc 1;
    1.58  
    1.59 -
    1.60 -
    1.61   autoCalculate 1 CompleteCalc; 
    1.62   val ((pt,p),_) = get_calc 1;
    1.63   if p=([], Res) then () else 
    1.64   error "FE-interface.sml: diff.behav. in solve_linear AUTOC Head/Calc ";
    1.65 -
    1.66 +============ inhibit exn 110620 ==============================================*)
    1.67  
    1.68  "--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
    1.69  "--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
    1.70 @@ -441,11 +440,15 @@
    1.71  
    1.72   val ((pt,_),_) = get_calc 1;
    1.73   val p = get_pos 1 1;
    1.74 +(*========== inhibit exn 110620 ================================================
    1.75   val (Form f, tac, asms) = pt_extract (pt, p);
    1.76 +(*    ModSpec........... =  ...................DIFFERENT !*)
    1.77   if term2str f = "[x = 1]" andalso p = ([], Res) then () else 
    1.78   error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
    1.79 +============ inhibit exn 110620 ==============================================*)
    1.80  
    1.81  
    1.82 +(*=== inhibit exn ?=============================================================
    1.83  "--------- mini-subpbl AUTO CompleteCalcHead ------------";
    1.84  "--------- mini-subpbl AUTO CompleteCalcHead ------------";
    1.85  "--------- mini-subpbl AUTO CompleteCalcHead ------------";
    1.86 @@ -454,6 +457,7 @@
    1.87     ("Test", ["sqroot-test","univariate","equation","test"],
    1.88      ["Test","squ-equ-test-subpbl1"]))];
    1.89   Iterator 1;
    1.90 + moveActiveRoot 1;
    1.91  (* doesn't terminate !!!
    1.92   autoCalculate 1 CompleteCalcHead; 
    1.93  *)
    1.94 @@ -1314,4 +1318,5 @@
    1.95   if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else 
    1.96   error "FE-interface.sml: diff.behav. in FORMULA:replace} NOTok";
    1.97  
    1.98 -============ inhibit exn 110310 ==============================================*)
    1.99 +===== inhibit exn ?===========================================================*)
   1.100 +