# HG changeset patch
# User Walther Neuper <neuper@ist.tugraz.at>
# Date 1285673429 -7200
# Node ID cd7854f2636dba06654bb5e1189142efa670d928
# Parent  928cebc9c4aaa8c99751e04543da56f586b4f425
interrupted test/../calculate.sml for 'rewrite_'

diff -r 928cebc9c4aa -r cd7854f2636d test/Tools/isac/ProgLang/calculate.sml
--- a/test/Tools/isac/ProgLang/calculate.sml	Tue Sep 28 10:10:26 2010 +0200
+++ b/test/Tools/isac/ProgLang/calculate.sml	Tue Sep 28 13:30:29 2010 +0200
@@ -50,13 +50,6 @@
 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 ?===========================================================
-
 "===== 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;
@@ -77,29 +70,27 @@
 if it <> "16" then error "calculate.sml: new behaviour in calculate_"
 else ();
 
-
-
 "----------- calculate from script ----------------------";
 "----------- calculate from script ----------------------";
 "----------- calculate from script ----------------------";
 store_pbt
- (prep_pbt Test.thy "pbl_ttest" [] e_pblID
+ (prep_pbt (theory "Test") "pbl_ttest" [] e_pblID
  (["test"],
   [],
   e_rls, NONE, []));
 store_pbt
- (prep_pbt Test.thy "pbl_ttest_calc" [] e_pblID
+ (prep_pbt (theory "Test") "pbl_ttest_calc" [] e_pblID
  (["calculate","test"],
-  [("#Given" ,["realTestGiven t_"]),
-   ("#Find"  ,["realTestFind s_"])
+  [("#Given" ,["realTestGiven t_t"]),
+   ("#Find"  ,["realTestFind s_s"])
    ],
   e_rls, NONE, [["Test","test_calculate"]]));
 
 store_met
- (prep_met Test.thy "met_testcal" [] e_metID
+ (prep_met (theory "Test") "met_testcal" [] e_metID
  (["Test","test_calculate"]:metID,
-  [("#Given" ,["realTestGiven t_"]),
-   ("#Find"  ,["realTestFind s_"])
+  [("#Given" ,["realTestGiven t_t"]),
+   ("#Find"  ,["realTestFind s_s"])
    ],
   {rew_ord'="sqrt_right",rls'=tval_rls,srls=e_rls,prls=e_rls,
    calc=[("PLUS"    ,("op +"        ,eval_binop "#add_")),
@@ -108,33 +99,35 @@
 	 ("POWER"  ,("Atools.pow"  ,eval_binop "#power_"))],
    crls=tval_rls, nrls=e_rls(*,
    asm_rls=[],asm_thm=[]*)},
-  "Script STest_simplify (t_::real) =          \
+  "Script STest_simplify (t_t::real) =          \
   \(Repeat                                        \
-  \ ((Try (Repeat (Calculate plus))) @@   \
-  \  (Try (Repeat (Calculate times))) @@  \
-  \  (Try (Repeat (Calculate divide_))) @@ \
-  \  (Try (Repeat (Calculate power_))))) t_"
+  \ ((Try (Repeat (Calculate PLUS))) @@   \
+  \  (Try (Repeat (Calculate TIMES))) @@  \
+  \  (Try (Repeat (Calculate DIVIDE))) @@ \
+  \  (Try (Repeat (Calculate POWER))))) t_t"
    ));
 
 val fmz = ["realTestGiven (((1+2)*4/3)^^^2)","realTestFind s"];
 val (dI',pI',mI') =
-  ("Test.thy",["calculate","test"],["Test","test_calculate"]);
-(*val p = e_pos'; val c = []; 
-val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
-val (p,_,f,nxt,_,pt) = me (mI,m) p c  EmptyPtree;*)
+  ("Test",["calculate","test"],["Test","test_calculate"]);
+
+
+(*===== inhibit exn ?===========================================================
+GOON after rewriting works
+
 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 (*nxt =("Add_Given",Add_Given "realTestGiven (((#1 + #2) * #4 // #3) ^^^#2)")*)
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 (*nxt = ("Add_Find",Add_Find "realTestFind s") : string * tac*)
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
-(*nxt = ("Specify_Theory",Specify_Theory "Test.thy") : string * tac*)
+(*nxt = ("Specify_Theory",Specify_Theory "Test") : string * tac*)
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 (*nxt = ("Specify_Problem",Specify_Problem ["calculate","test"])*)
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
-(*nxt = ("Specify_Method",Specify_Method ("Test.thy","test_calculate"))*)
+(*nxt = ("Specify_Method",Specify_Method ("Test","test_calculate"))*)
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
-(*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_calculate"))*)
+(*nxt = ("Apply_Method",Apply_Method ("Test","test_calculate"))*)
 
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 (*nxt = ("Calculate",Calculate "PLUS")*)
@@ -165,7 +158,7 @@
 (-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))";
 ie. cancel does not work properly
 *)
- val thy = "Test.thy";
+ val thy = "Test";
  val op_ = "DIVIDE";
  val ct = "sqrt (x ^^^ 2 + -3 * x) =\
  \(-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))";
@@ -183,7 +176,7 @@
  val (t,_) = the (rewrite_set_ thy false rls t);
 (*val t = Free ("3","RealDef.real") : term*)
 
- val thy = "Test.thy";
+ val thy = "Test";
  val t = "6 / 2";
  val rls = "Test_simplify";
  val (t,_) = the (rewrite_set thy false rls t);
@@ -222,7 +215,7 @@
 "-2";
 
 (*--------------(5): reproduce (1) with simpler term: ------------*)
- val thy = "Test.thy";
+ val thy = "Test";
  val t = "(3+5)/2";
  val (t,_) = the (rewrite_set thy false rls t);
 (*val t = "4" ... works*)
@@ -232,7 +225,7 @@
 (*val t = "2 + x" ... works*)
 
  trace_rewrite:=true; (*3.6.03*)
- val thy = "Test.thy";
+ val thy = "Test";
  val rls = "Test_simplify";
  val t = "(3+(1+2*x))/2";
  val (t,_) = the (rewrite_set thy false rls t);
@@ -282,7 +275,7 @@
  toggle trace_rewrite;
 (*===================*)
  trace_rewrite:=true;
- val thy' = "Test.thy";
+ val thy' = "Test";
  val rls = "Test_simplify";		
  val ct = "x + (-1 + -3) / 2";
  val (ct,_) = the (rewrite_set thy'  false rls ct);	
@@ -301,7 +294,7 @@
 *)
 
  trace_rewrite:=true;
- val thy' = "Test.thy";
+ val thy' = "Test";
  val rls = "Test_simplify";		
  val ct = "x + (-4) / 2";
  val (ct,_) = the (rewrite_set thy'  false rls ct);