# HG changeset patch
# User Walther Neuper <neuper@ist.tugraz.at>
# Date 1285660878 -7200
# Node ID 491b133d154a67015992af8ecce20fa68dfcb0c8
# Parent  121765ba0a34c6fe05b8050b7845f17a417f2ef7
intermediate test/../calculate.sml

diff -r 121765ba0a34 -r 491b133d154a test/Tools/isac/ProgLang/calculate.sml
--- a/test/Tools/isac/ProgLang/calculate.sml	Tue Sep 28 09:37:41 2010 +0200
+++ b/test/Tools/isac/ProgLang/calculate.sml	Tue Sep 28 10:01:18 2010 +0200
@@ -35,36 +35,50 @@
 handle TERM _ => 
        error "calculate.sml: get_calculation_ must return Trueprop";
 
+"----------- fun calculate_ -----------------------------";
+"----------- fun calculate_ -----------------------------";
+"----------- fun calculate_ -----------------------------";
+val thy = theory "Test";
+"===== test 1";
+val t = (term_of o the o (parse thy)) "1+2";
+val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t;
+term2str (prop_of thm) = "1 + 2 = 3";
+
+"===== test 2";
+val t = (term_of o the o (parse thy)) "((1+2)*4/3)^^^2";
+val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t;
+val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
+term2str t = "(3 * 4 / 3) ^^^ 2";
+
+"===== test 3: step into code";
+
+val ttt = str2term "2*3";
+
+get_calculation_ thy (the(assoc(calclist, "TIMES"))) ttt;
 (*===== inhibit exn ?===========================================================
 
-"----------- fun calculate_ -----------------------------";
-"----------- fun calculate_ -----------------------------";
-"----------- fun calculate_ -----------------------------";
-val thy = theory "Test";
-val t = (term_of o the o (parse thy)) "1+2";
-val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t;
+"===== test 3b -- 2 contiued";
+val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"TIMES"))) t;
+val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
+term2str t;
+(*val it = "(#12 // #3) ^^^ #2" : string*)
 
-val t = (term_of o the o (parse thy)) "((1+2)*4/3)^^^2";
-val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t;
+"===== test 4";
+val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"DIVIDE")))t;
 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
-Sign.string_of_term (sign_of thy) t;
-(*val it = "(#3 * #4 // #3) ^^^ #2" : string*)
-val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"times"))) t;
+term2str t;
+(*it = "#4 ^^^ #2" : string*)
+
+"===== test 5";
+val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"POWER")))t;
 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
-Sign.string_of_term (sign_of thy) t;
-(*val it = "(#12 // #3) ^^^ #2" : string*)
-val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"divide_")))t;
-val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
-Sign.string_of_term (sign_of thy) t;
-(*it = "#4 ^^^ #2" : string*)
-val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_")))t;
-val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
-Sign.string_of_term (sign_of thy) t;
+term2str t;
 (*val it = "#16" : string*)
 if it <> "16" then error "calculate.sml: new behaviour in calculate_"
 else ();
 
 
+
 "----------- calculate from script ----------------------";
 "----------- calculate from script ----------------------";
 "----------- calculate from script ----------------------";
@@ -88,10 +102,10 @@
    ("#Find"  ,["realTestFind s_"])
    ],
   {rew_ord'="sqrt_right",rls'=tval_rls,srls=e_rls,prls=e_rls,
-   calc=[("plus"    ,("op +"        ,eval_binop "#add_")),
-	 ("times"   ,("op *"        ,eval_binop "#mult_")),
-	 ("divide_" ,("HOL.divide"  ,eval_cancel "#divide_")),
-	 ("power_"  ,("Atools.pow"  ,eval_binop "#power_"))],
+   calc=[("PLUS"    ,("op +"        ,eval_binop "#add_")),
+	 ("TIMES"   ,("op *"        ,eval_binop "#mult_")),
+	 ("DIVIDE" ,("HOL.divide"  ,eval_cancel "#divide_")),
+	 ("POWER"  ,("Atools.pow"  ,eval_binop "#power_"))],
    crls=tval_rls, nrls=e_rls(*,
    asm_rls=[],asm_thm=[]*)},
   "Script STest_simplify (t_::real) =          \
@@ -123,13 +137,13 @@
 (*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_calculate"))*)
 
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
-(*nxt = ("Calculate",Calculate "plus")*)
+(*nxt = ("Calculate",Calculate "PLUS")*)
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
-(*nxt = ("Calculate",Calculate "times")*)
+(*nxt = ("Calculate",Calculate "TIMES")*)
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
-(*nxt = ("Calculate",Calculate "divide_")*)
+(*nxt = ("Calculate",Calculate "DIVIDE")*)
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
-(*nxt = ("Calculate",Calculate "power_")*)
+(*nxt = ("Calculate",Calculate "POWER")*)
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 (*nxt = ("Check_Postcond",Check_Postcond ["calculate","test"])*)
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
@@ -152,7 +166,7 @@
 ie. cancel does not work properly
 *)
  val thy = "Test.thy";
- val op_ = "divide_";
+ val op_ = "DIVIDE";
  val ct = "sqrt (x ^^^ 2 + -3 * x) =\
  \(-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))";
  val SOME (ct,_) = calculate thy (the(assoc(calclist,op_))) ct;
@@ -385,35 +399,35 @@
 
 val thy = Test.thy;
 val t = (term_of o the o (parse thy)) "12 / 3";
-val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"divide_")))t;
+val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"DIVIDE")))t;
 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
 "12 / 3 = 4";
 val thy = Test.thy;
 val t = (term_of o the o (parse thy)) "4 ^^^ 2";
-val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_"))) t;
+val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"POWER"))) t;
 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
 "4 ^ 2 = 16";
 
  val t = (term_of o the o (parse thy)) "((1 + 2) * 4 / 3) ^^^ 2";
- val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t;
+ val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t;
 "1 + 2 = 3";
  val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
- Sign.string_of_term (sign_of thy) t;
+ term2str t;
 "(3 * 4 / 3) ^^^ 2";
- val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"times")))t;
+ val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"TIMES")))t;
 "3 * 4 = 12";
  val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
- Sign.string_of_term (sign_of thy) t;
+ term2str t;
 "(12 / 3) ^^^ 2";
- val SOME (thmID,thm) =get_calculation_ thy(the(assoc(calclist,"divide_")))t;
+ val SOME (thmID,thm) =get_calculation_ thy(the(assoc(calclist,"DIVIDE")))t;
 "12 / 3 = 4";
  val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
- Sign.string_of_term (sign_of thy) t;
+ term2str t;
 "4 ^^^ 2";
- val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_")))t;
+ val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"POWER")))t;
 "4 ^^^ 2 = 16";
  val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
- Sign.string_of_term (sign_of thy) t;
+ term2str t;
 "16";
  if it <> "16" then error "calculate.sml: new behaviour in calculate_"
  else ();
@@ -421,10 +435,10 @@
 (*13.9.02 *** calc: operator = pow not defined*)
   val t = (term_of o the o (parse thy)) "3^^^2";
   val SOME (thmID,thm) = 
-      get_calculation_ thy (the(assoc(calclist,"power_"))) t;
+      get_calculation_ thy (the(assoc(calclist,"POWER"))) t;
 (*** calc: operator = pow not defined*)
 
-  val (op_, eval_fn) = the (assoc(calclist,"power_"));
+  val (op_, eval_fn) = the (assoc(calclist,"POWER"));
   (*
 val op_ = "Atools.pow" : string
 val eval_fn = fn : string -> term -> theory -> (string * term) option*)