test/Tools/isac/IsacKnowledge/diffapp.sml
branchisac-update-Isa09-2
changeset 37924 6c53fe2519e5
parent 37906 e2b23ba9df13
child 37926 e6fc98fbcb85
     1.1 --- a/test/Tools/isac/IsacKnowledge/diffapp.sml	Tue Aug 17 09:05:51 2010 +0200
     1.2 +++ b/test/Tools/isac/IsacKnowledge/diffapp.sml	Wed Aug 18 13:40:09 2010 +0200
     1.3 @@ -283,10 +283,10 @@
     1.4  	  | _ => raise error "diffapp.sml: max-exp me, nxt = Specify_Method";
     1.5  
     1.6  val oris = fst3 (get_obj g_origin pt (fst p)); writeln(oris2str oris);
     1.7 -val pits = get_obj g_pbl pt (fst p); writeln(itms2str thy pits);
     1.8 +val pits = get_obj g_pbl pt (fst p); writeln(itms2str_ ctxt pits);
     1.9  
    1.10  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.11 -val mits = get_obj g_met pt (fst p); writeln(itms2str thy mits);
    1.12 +val mits = get_obj g_met pt (fst p); writeln(itms2str_ ctxt mits);
    1.13  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.14  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.15  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.16 @@ -311,7 +311,7 @@
    1.17  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.18  
    1.19  val oris = fst3 (get_obj g_origin pt (fst p));writeln(oris2str oris);
    1.20 -val pits = get_obj g_pbl pt (fst p);writeln(itms2str thy pits);
    1.21 +val pits = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt pits);
    1.22  
    1.23  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.24  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.25 @@ -344,7 +344,7 @@
    1.26  (*val nxt = Refine_Tacitly ["univariate","equation"])*)
    1.27  
    1.28  val oris = fst3 (get_obj g_origin pt (fst p));writeln(oris2str oris);
    1.29 -val pits = get_obj g_pbl pt (fst p);writeln(itms2str thy pits);
    1.30 +val pits = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt pits);
    1.31  
    1.32  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.33  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.34 @@ -377,11 +377,11 @@
    1.35  
    1.36  val oris = fst3 (get_obj g_origin pt (fst p));writeln(oris2str oris);
    1.37  
    1.38 -val pits = get_obj g_pbl pt (fst p);writeln(itms2str thy pits);
    1.39 -val pits = get_obj g_pbl pt [];writeln(itms2str thy pits);
    1.40 +val pits = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt pits);
    1.41 +val pits = get_obj g_pbl pt [];writeln(itms2str_ ctxt pits);
    1.42  
    1.43 -val mits = get_obj g_met pt (fst p);writeln(itms2str thy mits);
    1.44 -val mits = get_obj g_met pt [];writeln(itms2str thy mits);
    1.45 +val mits = get_obj g_met pt (fst p);writeln(itms2str_ ctxt mits);
    1.46 +val mits = get_obj g_met pt [];writeln(itms2str_ ctxt mits);
    1.47  
    1.48  itms2args thy ["DiffApp","max_by_calculus"] mits;
    1.49  
    1.50 @@ -426,14 +426,14 @@
    1.51   fetchProposedTactic 1;
    1.52   val ((pt,p),_) = get_calc 1;
    1.53   val mits = get_obj g_met pt (fst p);
    1.54 - writeln (itms2str thy mits);
    1.55 + writeln (itms2str_ ctxt mits);
    1.56  (*
    1.57 - if itms2str thy mits = "[\n(1 ,[1] ,true ,#Given ,Cor functionEq (hd rs_) ,(t_, [hd rs_])),\n(2 ,[1] ,true ,#Given ,Cor boundVariable v_ ,(v_, [v_])),\n(3 ,[1] ,true ,#Given ,Cor interval itv_ ,(itv_, [itv_])),\n(4 ,[1] ,true ,#Find ,Cor maxArgument v__0 ,(v_0_, [v__0]))]" then ()
    1.58 + if itms2str_ ctxt mits = "[\n(1 ,[1] ,true ,#Given ,Cor functionEq (hd rs_) ,(t_, [hd rs_])),\n(2 ,[1] ,true ,#Given ,Cor boundVariable v_ ,(v_, [v_])),\n(3 ,[1] ,true ,#Given ,Cor interval itv_ ,(itv_, [itv_])),\n(4 ,[1] ,true ,#Find ,Cor maxArgument v__0 ,(v_0_, [v__0]))]" then ()
    1.59   else raise error "diffapp.sml: diff.behav. in autoCalc .. scripts for max 1";
    1.60  *)
    1.61   (*FIXME: the environments contain identifers, and NOT values ?!?!?*)
    1.62  (* WN051209 while extending 'fun step' for initac, this became better ...
    1.63 - if itms2str thy mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(itv_, [{x. 0 <= x & x <= 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(err_, [eps = 0]))]" then ()
    1.64 + if itms2str_ ctxt mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(itv_, [{x. 0 <= x & x <= 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(err_, [eps = 0]))]" then ()
    1.65   else raise error "diffapp.sml: diff.behav. in autoCalc .. scripts for max 1";
    1.66  *)
    1.67