test/Tools/isac/Interpret/calchead.sml
branchdecompose-isar
changeset 42108 23b6b0033454
parent 41972 22c5483e9bfb
child 42181 77f1173be5c0
     1.1 --- a/test/Tools/isac/Interpret/calchead.sml	Mon Jul 18 09:51:51 2011 +0200
     1.2 +++ b/test/Tools/isac/Interpret/calchead.sml	Tue Jul 19 09:43:01 2011 +0200
     1.3 @@ -1,4 +1,5 @@
     1.4 -(* Title: tests on calchead.sml
     1.5 +
     1.6 +  (* Title: tests on calchead.sml
     1.7     Author: Walther Neuper 051013,
     1.8     (c) due to copyright terms
     1.9  
    1.10 @@ -21,7 +22,7 @@
    1.11  "--------------------------------------------------------";
    1.12  "--------------------------------------------------------";
    1.13  
    1.14 -(*========== inhibit exn =======================================================
    1.15 +
    1.16  "--------- get_interval after replace} other 2 ----------";
    1.17  "--------- get_interval after replace} other 2 ----------";
    1.18  "--------- get_interval after replace} other 2 ----------";
    1.19 @@ -75,9 +76,6 @@
    1.20     ["DiffApp","max_by_calculus"]);
    1.21  val c = []:cid;
    1.22  
    1.23 -(*val nxt = Init_Proof' (fmz,(dI',pI',mI'));
    1.24 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt e_pos' [] EmptyPtree;
    1.25 -*)
    1.26  val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    1.27  val nxt = tac2tac_ pt p nxt; 
    1.28  val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
    1.29 @@ -87,7 +85,7 @@
    1.30  val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
    1.31  (**)
    1.32  
    1.33 -(*---6.5.03
    1.34 +(*========== inhibit exn AK110718 =======================================================
    1.35  val nxt = tac2tac_ pt p (Add_Find "valuesFor [(a::real)]"); 
    1.36  val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
    1.37  (*uncaught exception TYPE 6.5.03*)
    1.38 @@ -98,21 +96,21 @@
    1.39  	  Relate=[Incompl "relations []"], Where=[],With=[]})
    1.40  then error "test-maximum.sml: model stepwise - different behaviour" 
    1.41  else (); (*different with show_types !!!*)
    1.42 -6.5.03---*)
    1.43 +========== inhibit exn AK110718 =======================================================*)
    1.44  
    1.45 -(*-----appl_add should not create Error', but accept as Sup,Syn
    1.46 +(*========== inhibit exn AK110718 =======================================================
    1.47  val nxt = tac2tac_ pt p (Add_Given "boundVariable a"); 
    1.48  val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
    1.49 -(**)
    1.50 +
    1.51  val nxt = tac2tac_ pt p (Add_Given "boundVariable a+"); 
    1.52  val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
    1.53 -(**)---*)
    1.54 +========== inhibit exn AK110718 =======================================================*)
    1.55  
    1.56  val m = Specify_Problem ["maximum_of","function"];
    1.57  val nxt = tac2tac_ pt p m; 
    1.58  val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
    1.59  (**)
    1.60 -
    1.61 +(*========== inhibit exn AK110718 =======================================================
    1.62  if ppc<>(Problem ["maximum_of","function"],  
    1.63           {Find=[Incompl "maximum",Incompl "valuesFor"],
    1.64  	  Given=[Correct "fixedValues [r = Arbfix]"],
    1.65 @@ -146,7 +144,7 @@
    1.66      Relate=[Missing "relations rs_"],Where=[],With=[]})
    1.67  then error "diffappl.sml: Specify_Method different behaviour" 
    1.68  else ();*)
    1.69 -
    1.70 +========== inhibit exn AK110718 =======================================================*)
    1.71  
    1.72  
    1.73  "--------- maximum example with 'specify', fmz <> [] -------------";
    1.74 @@ -282,11 +280,13 @@
    1.75  (*val nxt = Add_Relation "relations" --- 
    1.76    --- [b=Arbfix] KANN NICHT VERLANGT WERDEN !!!!*)
    1.77  
    1.78 +(*========== inhibit exn 010830 =======================================================
    1.79  (*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....
    1.80  if nxt<>(Add_Relation "relations []")
    1.81  then error "test specify, fmz <> []: nxt <> Add_Relation.." 
    1.82  else (); (*different with show_types !!!*)
    1.83  *)
    1.84 +========== inhibit exn 010830 =======================================================*)
    1.85  
    1.86  val nxt = Add_Relation "relations [(A=a+b)]";
    1.87  val nxt = tac2tac_ pt p nxt; 
    1.88 @@ -312,18 +312,22 @@
    1.89  val nxt = tac2tac_ pt p nxt; 
    1.90  val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
    1.91  (*val nxt = Apply_Method ("DiffApp","max_by_calculus") *)
    1.92 +
    1.93 +(*========== inhibit exn 010830 =======================================================
    1.94  (*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....
    1.95  if nxt<>(Apply_Method ("DiffApp","max_by_calculus"))
    1.96  then error "test specify, fmz <> []: nxt <> Add_Relation.." 
    1.97  else ();
    1.98  *)
    1.99 +========== inhibit exn 010830 =======================================================*)
   1.100  
   1.101 +(*========== inhibit exn 000402 =======================================================
   1.102  (* 2.4.00 nach Transfer specify -> hard_gen
   1.103  val nxt = Apply_Method ("DiffApp","max_by_calculus");
   1.104  val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; *)
   1.105  (*val nxt = Empty_Tac : tac*)
   1.106 +========== inhibit exn 000402 =======================================================*)
   1.107  
   1.108 -============ inhibit exn =====================================================*)
   1.109  
   1.110  (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
   1.111  
   1.112 @@ -721,3 +725,4 @@
   1.113  
   1.114  (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
   1.115  -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
   1.116 +