1.1 --- a/test/Tools/isac/ProgLang/calculate.sml Tue Sep 28 09:37:41 2010 +0200
1.2 +++ b/test/Tools/isac/ProgLang/calculate.sml Tue Sep 28 10:01:18 2010 +0200
1.3 @@ -35,36 +35,50 @@
1.4 handle TERM _ =>
1.5 error "calculate.sml: get_calculation_ must return Trueprop";
1.6
1.7 +"----------- fun calculate_ -----------------------------";
1.8 +"----------- fun calculate_ -----------------------------";
1.9 +"----------- fun calculate_ -----------------------------";
1.10 +val thy = theory "Test";
1.11 +"===== test 1";
1.12 +val t = (term_of o the o (parse thy)) "1+2";
1.13 +val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t;
1.14 +term2str (prop_of thm) = "1 + 2 = 3";
1.15 +
1.16 +"===== test 2";
1.17 +val t = (term_of o the o (parse thy)) "((1+2)*4/3)^^^2";
1.18 +val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t;
1.19 +val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.20 +term2str t = "(3 * 4 / 3) ^^^ 2";
1.21 +
1.22 +"===== test 3: step into code";
1.23 +
1.24 +val ttt = str2term "2*3";
1.25 +
1.26 +get_calculation_ thy (the(assoc(calclist, "TIMES"))) ttt;
1.27 (*===== inhibit exn ?===========================================================
1.28
1.29 -"----------- fun calculate_ -----------------------------";
1.30 -"----------- fun calculate_ -----------------------------";
1.31 -"----------- fun calculate_ -----------------------------";
1.32 -val thy = theory "Test";
1.33 -val t = (term_of o the o (parse thy)) "1+2";
1.34 -val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t;
1.35 +"===== test 3b -- 2 contiued";
1.36 +val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"TIMES"))) t;
1.37 +val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.38 +term2str t;
1.39 +(*val it = "(#12 // #3) ^^^ #2" : string*)
1.40
1.41 -val t = (term_of o the o (parse thy)) "((1+2)*4/3)^^^2";
1.42 -val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t;
1.43 +"===== test 4";
1.44 +val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"DIVIDE")))t;
1.45 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.46 -Sign.string_of_term (sign_of thy) t;
1.47 -(*val it = "(#3 * #4 // #3) ^^^ #2" : string*)
1.48 -val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"times"))) t;
1.49 +term2str t;
1.50 +(*it = "#4 ^^^ #2" : string*)
1.51 +
1.52 +"===== test 5";
1.53 +val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"POWER")))t;
1.54 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.55 -Sign.string_of_term (sign_of thy) t;
1.56 -(*val it = "(#12 // #3) ^^^ #2" : string*)
1.57 -val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"divide_")))t;
1.58 -val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.59 -Sign.string_of_term (sign_of thy) t;
1.60 -(*it = "#4 ^^^ #2" : string*)
1.61 -val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_")))t;
1.62 -val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.63 -Sign.string_of_term (sign_of thy) t;
1.64 +term2str t;
1.65 (*val it = "#16" : string*)
1.66 if it <> "16" then error "calculate.sml: new behaviour in calculate_"
1.67 else ();
1.68
1.69
1.70 +
1.71 "----------- calculate from script ----------------------";
1.72 "----------- calculate from script ----------------------";
1.73 "----------- calculate from script ----------------------";
1.74 @@ -88,10 +102,10 @@
1.75 ("#Find" ,["realTestFind s_"])
1.76 ],
1.77 {rew_ord'="sqrt_right",rls'=tval_rls,srls=e_rls,prls=e_rls,
1.78 - calc=[("plus" ,("op +" ,eval_binop "#add_")),
1.79 - ("times" ,("op *" ,eval_binop "#mult_")),
1.80 - ("divide_" ,("HOL.divide" ,eval_cancel "#divide_")),
1.81 - ("power_" ,("Atools.pow" ,eval_binop "#power_"))],
1.82 + calc=[("PLUS" ,("op +" ,eval_binop "#add_")),
1.83 + ("TIMES" ,("op *" ,eval_binop "#mult_")),
1.84 + ("DIVIDE" ,("HOL.divide" ,eval_cancel "#divide_")),
1.85 + ("POWER" ,("Atools.pow" ,eval_binop "#power_"))],
1.86 crls=tval_rls, nrls=e_rls(*,
1.87 asm_rls=[],asm_thm=[]*)},
1.88 "Script STest_simplify (t_::real) = \
1.89 @@ -123,13 +137,13 @@
1.90 (*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_calculate"))*)
1.91
1.92 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.93 -(*nxt = ("Calculate",Calculate "plus")*)
1.94 +(*nxt = ("Calculate",Calculate "PLUS")*)
1.95 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.96 -(*nxt = ("Calculate",Calculate "times")*)
1.97 +(*nxt = ("Calculate",Calculate "TIMES")*)
1.98 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.99 -(*nxt = ("Calculate",Calculate "divide_")*)
1.100 +(*nxt = ("Calculate",Calculate "DIVIDE")*)
1.101 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.102 -(*nxt = ("Calculate",Calculate "power_")*)
1.103 +(*nxt = ("Calculate",Calculate "POWER")*)
1.104 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.105 (*nxt = ("Check_Postcond",Check_Postcond ["calculate","test"])*)
1.106 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.107 @@ -152,7 +166,7 @@
1.108 ie. cancel does not work properly
1.109 *)
1.110 val thy = "Test.thy";
1.111 - val op_ = "divide_";
1.112 + val op_ = "DIVIDE";
1.113 val ct = "sqrt (x ^^^ 2 + -3 * x) =\
1.114 \(-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))";
1.115 val SOME (ct,_) = calculate thy (the(assoc(calclist,op_))) ct;
1.116 @@ -385,35 +399,35 @@
1.117
1.118 val thy = Test.thy;
1.119 val t = (term_of o the o (parse thy)) "12 / 3";
1.120 -val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"divide_")))t;
1.121 +val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"DIVIDE")))t;
1.122 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.123 "12 / 3 = 4";
1.124 val thy = Test.thy;
1.125 val t = (term_of o the o (parse thy)) "4 ^^^ 2";
1.126 -val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_"))) t;
1.127 +val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"POWER"))) t;
1.128 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.129 "4 ^ 2 = 16";
1.130
1.131 val t = (term_of o the o (parse thy)) "((1 + 2) * 4 / 3) ^^^ 2";
1.132 - val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t;
1.133 + val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t;
1.134 "1 + 2 = 3";
1.135 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.136 - Sign.string_of_term (sign_of thy) t;
1.137 + term2str t;
1.138 "(3 * 4 / 3) ^^^ 2";
1.139 - val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"times")))t;
1.140 + val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"TIMES")))t;
1.141 "3 * 4 = 12";
1.142 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.143 - Sign.string_of_term (sign_of thy) t;
1.144 + term2str t;
1.145 "(12 / 3) ^^^ 2";
1.146 - val SOME (thmID,thm) =get_calculation_ thy(the(assoc(calclist,"divide_")))t;
1.147 + val SOME (thmID,thm) =get_calculation_ thy(the(assoc(calclist,"DIVIDE")))t;
1.148 "12 / 3 = 4";
1.149 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.150 - Sign.string_of_term (sign_of thy) t;
1.151 + term2str t;
1.152 "4 ^^^ 2";
1.153 - val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_")))t;
1.154 + val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"POWER")))t;
1.155 "4 ^^^ 2 = 16";
1.156 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.157 - Sign.string_of_term (sign_of thy) t;
1.158 + term2str t;
1.159 "16";
1.160 if it <> "16" then error "calculate.sml: new behaviour in calculate_"
1.161 else ();
1.162 @@ -421,10 +435,10 @@
1.163 (*13.9.02 *** calc: operator = pow not defined*)
1.164 val t = (term_of o the o (parse thy)) "3^^^2";
1.165 val SOME (thmID,thm) =
1.166 - get_calculation_ thy (the(assoc(calclist,"power_"))) t;
1.167 + get_calculation_ thy (the(assoc(calclist,"POWER"))) t;
1.168 (*** calc: operator = pow not defined*)
1.169
1.170 - val (op_, eval_fn) = the (assoc(calclist,"power_"));
1.171 + val (op_, eval_fn) = the (assoc(calclist,"POWER"));
1.172 (*
1.173 val op_ = "Atools.pow" : string
1.174 val eval_fn = fn : string -> term -> theory -> (string * term) option*)