1.1 --- a/test/Tools/isac/ProgLang/calculate.sml Tue Sep 28 10:10:26 2010 +0200
1.2 +++ b/test/Tools/isac/ProgLang/calculate.sml Tue Sep 28 13:30:29 2010 +0200
1.3 @@ -50,13 +50,6 @@
1.4 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.5 term2str t = "(3 * 4 / 3) ^^^ 2";
1.6
1.7 -"===== test 3: step into code";
1.8 -
1.9 -val ttt = str2term "2*3";
1.10 -
1.11 -get_calculation_ thy (the(assoc(calclist, "TIMES"))) ttt;
1.12 -(*===== inhibit exn ?===========================================================
1.13 -
1.14 "===== test 3b -- 2 contiued";
1.15 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"TIMES"))) t;
1.16 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.17 @@ -77,29 +70,27 @@
1.18 if it <> "16" then error "calculate.sml: new behaviour in calculate_"
1.19 else ();
1.20
1.21 -
1.22 -
1.23 "----------- calculate from script ----------------------";
1.24 "----------- calculate from script ----------------------";
1.25 "----------- calculate from script ----------------------";
1.26 store_pbt
1.27 - (prep_pbt Test.thy "pbl_ttest" [] e_pblID
1.28 + (prep_pbt (theory "Test") "pbl_ttest" [] e_pblID
1.29 (["test"],
1.30 [],
1.31 e_rls, NONE, []));
1.32 store_pbt
1.33 - (prep_pbt Test.thy "pbl_ttest_calc" [] e_pblID
1.34 + (prep_pbt (theory "Test") "pbl_ttest_calc" [] e_pblID
1.35 (["calculate","test"],
1.36 - [("#Given" ,["realTestGiven t_"]),
1.37 - ("#Find" ,["realTestFind s_"])
1.38 + [("#Given" ,["realTestGiven t_t"]),
1.39 + ("#Find" ,["realTestFind s_s"])
1.40 ],
1.41 e_rls, NONE, [["Test","test_calculate"]]));
1.42
1.43 store_met
1.44 - (prep_met Test.thy "met_testcal" [] e_metID
1.45 + (prep_met (theory "Test") "met_testcal" [] e_metID
1.46 (["Test","test_calculate"]:metID,
1.47 - [("#Given" ,["realTestGiven t_"]),
1.48 - ("#Find" ,["realTestFind s_"])
1.49 + [("#Given" ,["realTestGiven t_t"]),
1.50 + ("#Find" ,["realTestFind s_s"])
1.51 ],
1.52 {rew_ord'="sqrt_right",rls'=tval_rls,srls=e_rls,prls=e_rls,
1.53 calc=[("PLUS" ,("op +" ,eval_binop "#add_")),
1.54 @@ -108,33 +99,35 @@
1.55 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))],
1.56 crls=tval_rls, nrls=e_rls(*,
1.57 asm_rls=[],asm_thm=[]*)},
1.58 - "Script STest_simplify (t_::real) = \
1.59 + "Script STest_simplify (t_t::real) = \
1.60 \(Repeat \
1.61 - \ ((Try (Repeat (Calculate plus))) @@ \
1.62 - \ (Try (Repeat (Calculate times))) @@ \
1.63 - \ (Try (Repeat (Calculate divide_))) @@ \
1.64 - \ (Try (Repeat (Calculate power_))))) t_"
1.65 + \ ((Try (Repeat (Calculate PLUS))) @@ \
1.66 + \ (Try (Repeat (Calculate TIMES))) @@ \
1.67 + \ (Try (Repeat (Calculate DIVIDE))) @@ \
1.68 + \ (Try (Repeat (Calculate POWER))))) t_t"
1.69 ));
1.70
1.71 val fmz = ["realTestGiven (((1+2)*4/3)^^^2)","realTestFind s"];
1.72 val (dI',pI',mI') =
1.73 - ("Test.thy",["calculate","test"],["Test","test_calculate"]);
1.74 -(*val p = e_pos'; val c = [];
1.75 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.76 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.77 + ("Test",["calculate","test"],["Test","test_calculate"]);
1.78 +
1.79 +
1.80 +(*===== inhibit exn ?===========================================================
1.81 +GOON after rewriting works
1.82 +
1.83 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.84 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.85 (*nxt =("Add_Given",Add_Given "realTestGiven (((#1 + #2) * #4 // #3) ^^^#2)")*)
1.86 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.87 (*nxt = ("Add_Find",Add_Find "realTestFind s") : string * tac*)
1.88 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.89 -(*nxt = ("Specify_Theory",Specify_Theory "Test.thy") : string * tac*)
1.90 +(*nxt = ("Specify_Theory",Specify_Theory "Test") : string * tac*)
1.91 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.92 (*nxt = ("Specify_Problem",Specify_Problem ["calculate","test"])*)
1.93 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.94 -(*nxt = ("Specify_Method",Specify_Method ("Test.thy","test_calculate"))*)
1.95 +(*nxt = ("Specify_Method",Specify_Method ("Test","test_calculate"))*)
1.96 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.97 -(*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_calculate"))*)
1.98 +(*nxt = ("Apply_Method",Apply_Method ("Test","test_calculate"))*)
1.99
1.100 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.101 (*nxt = ("Calculate",Calculate "PLUS")*)
1.102 @@ -165,7 +158,7 @@
1.103 (-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))";
1.104 ie. cancel does not work properly
1.105 *)
1.106 - val thy = "Test.thy";
1.107 + val thy = "Test";
1.108 val op_ = "DIVIDE";
1.109 val ct = "sqrt (x ^^^ 2 + -3 * x) =\
1.110 \(-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))";
1.111 @@ -183,7 +176,7 @@
1.112 val (t,_) = the (rewrite_set_ thy false rls t);
1.113 (*val t = Free ("3","RealDef.real") : term*)
1.114
1.115 - val thy = "Test.thy";
1.116 + val thy = "Test";
1.117 val t = "6 / 2";
1.118 val rls = "Test_simplify";
1.119 val (t,_) = the (rewrite_set thy false rls t);
1.120 @@ -222,7 +215,7 @@
1.121 "-2";
1.122
1.123 (*--------------(5): reproduce (1) with simpler term: ------------*)
1.124 - val thy = "Test.thy";
1.125 + val thy = "Test";
1.126 val t = "(3+5)/2";
1.127 val (t,_) = the (rewrite_set thy false rls t);
1.128 (*val t = "4" ... works*)
1.129 @@ -232,7 +225,7 @@
1.130 (*val t = "2 + x" ... works*)
1.131
1.132 trace_rewrite:=true; (*3.6.03*)
1.133 - val thy = "Test.thy";
1.134 + val thy = "Test";
1.135 val rls = "Test_simplify";
1.136 val t = "(3+(1+2*x))/2";
1.137 val (t,_) = the (rewrite_set thy false rls t);
1.138 @@ -282,7 +275,7 @@
1.139 toggle trace_rewrite;
1.140 (*===================*)
1.141 trace_rewrite:=true;
1.142 - val thy' = "Test.thy";
1.143 + val thy' = "Test";
1.144 val rls = "Test_simplify";
1.145 val ct = "x + (-1 + -3) / 2";
1.146 val (ct,_) = the (rewrite_set thy' false rls ct);
1.147 @@ -301,7 +294,7 @@
1.148 *)
1.149
1.150 trace_rewrite:=true;
1.151 - val thy' = "Test.thy";
1.152 + val thy' = "Test";
1.153 val rls = "Test_simplify";
1.154 val ct = "x + (-4) / 2";
1.155 val (ct,_) = the (rewrite_set thy' false rls ct);