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 +