1.1 --- a/test/Tools/isac/Scripts/calculate.sml Wed Aug 18 13:53:15 2010 +0200
1.2 +++ b/test/Tools/isac/Scripts/calculate.sml Wed Aug 18 13:55:23 2010 +0200
1.3 @@ -31,23 +31,23 @@
1.4
1.5 val thy = Test.thy;
1.6 val t = (term_of o the o (parse thy)) "1+2";
1.7 -val Some (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t;
1.8 +val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t;
1.9
1.10 val t = (term_of o the o (parse thy)) "((1+2)*4/3)^^^2";
1.11 -val Some (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t;
1.12 -val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.13 +val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t;
1.14 +val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.15 Sign.string_of_term (sign_of thy) t;
1.16 (*val it = "(#3 * #4 // #3) ^^^ #2" : string*)
1.17 -val Some (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"times"))) t;
1.18 -val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.19 +val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"times"))) t;
1.20 +val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.21 Sign.string_of_term (sign_of thy) t;
1.22 (*val it = "(#12 // #3) ^^^ #2" : string*)
1.23 -val Some (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"divide_")))t;
1.24 -val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.25 +val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"divide_")))t;
1.26 +val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.27 Sign.string_of_term (sign_of thy) t;
1.28 (*it = "#4 ^^^ #2" : string*)
1.29 -val Some (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_")))t;
1.30 -val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.31 +val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_")))t;
1.32 +val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.33 Sign.string_of_term (sign_of thy) t;
1.34 (*val it = "#16" : string*)
1.35 if it <> "16" then raise error "calculate.sml: new behaviour in calculate_"
1.36 @@ -61,14 +61,14 @@
1.37 (prep_pbt Test.thy "pbl_ttest" [] e_pblID
1.38 (["test"],
1.39 [],
1.40 - e_rls, None, []));
1.41 + e_rls, NONE, []));
1.42 store_pbt
1.43 (prep_pbt Test.thy "pbl_ttest_calc" [] e_pblID
1.44 (["calculate","test"],
1.45 [("#Given" ,["realTestGiven t_"]),
1.46 ("#Find" ,["realTestFind s_"])
1.47 ],
1.48 - e_rls, None, [["Test","test_calculate"]]));
1.49 + e_rls, NONE, [["Test","test_calculate"]]));
1.50
1.51 store_met
1.52 (prep_met Test.thy "met_testcal" [] e_metID
1.53 @@ -145,7 +145,7 @@
1.54 val op_ = "divide_";
1.55 val ct = "sqrt (x ^^^ 2 + -3 * x) =\
1.56 \(-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))";
1.57 - val Some (ct,_) = calculate thy (the(assoc(calclist,op_))) ct;
1.58 + val SOME (ct,_) = calculate thy (the(assoc(calclist,op_))) ct;
1.59 writeln ct;
1.60 (*
1.61 sqrt (x ^^^ 2 + -3 * x) =\
1.62 @@ -171,10 +171,10 @@
1.63 val t = (term_of o the o (parse Test.thy)) "2 is_const";
1.64 atomty t;
1.65 rewrite_set_ Test.thy false tval_rls t;
1.66 -(*val it = Some (Const ("True","bool"),[]) ... works*)
1.67 +(*val it = SOME (Const ("True","bool"),[]) ... works*)
1.68
1.69 val t = str2term "2 * x is_const";
1.70 - val Some (str,t') = eval_const "" "" t Isac.thy;
1.71 + val SOME (str,t') = eval_const "" "" t Isac.thy;
1.72 term2str t';
1.73
1.74
1.75 @@ -185,7 +185,7 @@
1.76 trace_rewrite:=true;
1.77 val thy = Test.thy;
1.78 val t = (term_of o the o (parse thy)) "(-4) / 2";
1.79 - val Some (_,t) = eval_cancel "xxx" "HOL.divide" t thy;
1.80 + val SOME (_,t) = eval_cancel "xxx" "HOL.divide" t thy;
1.81 term2str t;
1.82 "-4 / 2 = (-2)";
1.83 (*-------------- but ... *)
1.84 @@ -219,7 +219,7 @@
1.85 val thy = Test.thy;
1.86 val rls = Test_simplify;
1.87 val t = str2term "(3+(1+2*x))/2";
1.88 - val Some (t',asm) = rewrite_set_ thy false rls t;
1.89 + val SOME (t',asm) = rewrite_set_ thy false rls t;
1.90 term2str t';
1.91 (*val t = "2 + x" ... works: give up----------------------------------------*)
1.92 trace_rewrite:=false;
1.93 @@ -267,12 +267,12 @@
1.94 ### trying calc. 'cancel'
1.95 @@@ get_pair: binop, t = x + (-4) / 2
1.96 @@@ get_pair: t else
1.97 -@@@ get_pair: t else -> None
1.98 +@@@ get_pair: t else -> NONE
1.99 @@@ get_pair: binop, t = (-4) / 2
1.100 @@@ get_pair: then 1
1.101 -@@@ get_pair: t -> None
1.102 -@@@ get_pair: t1 -> None
1.103 -@@@ get_calculation: None
1.104 +@@@ get_pair: t -> NONE
1.105 +@@@ get_pair: t1 -> NONE
1.106 +@@@ get_calculation: NONE
1.107 ### trying calc. 'pow'
1.108 *)
1.109
1.110 @@ -286,10 +286,10 @@
1.111 ### trying calc. 'cancel'
1.112 @@@ get_pair: binop, t = x + -4 / 2
1.113 @@@ get_pair: t else
1.114 -@@@ get_pair: t else -> None
1.115 +@@@ get_pair: t else -> NONE
1.116 @@@ get_pair: binop, t = -4 / 2
1.117 @@@ get_pair: then 1
1.118 -@@@ get_calculation: Some #cancel_-4_2
1.119 +@@@ get_calculation: SOME #cancel_-4_2
1.120 ### calc. to: x + (-2)
1.121 ### trying calc. 'cancel'
1.122 *)
1.123 @@ -331,7 +331,7 @@
1.124 *** . Free ( aaa, real)
1.125 *** . Free ( 1, real) *)
1.126 val thm = num_str real_divide_1;
1.127 - val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.128 + val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.129 (*val t = Free ("aaa","RealDef.real") : term*)
1.130
1.131
1.132 @@ -366,7 +366,7 @@
1.133 *** . Free ( 1, real)
1.134 *** . Free ( aaa, nat) .......................... nat !!! *)
1.135 val thm = num_str realpow_eq_one;
1.136 - val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.137 + val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.138 (*val t = Free ("1","RealDef.real") : term*)
1.139
1.140 " ================= calculate.sml: calculate_ 2002 =================== ";
1.141 @@ -375,34 +375,34 @@
1.142
1.143 val thy = Test.thy;
1.144 val t = (term_of o the o (parse thy)) "12 / 3";
1.145 -val Some (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"divide_")))t;
1.146 -val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.147 +val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"divide_")))t;
1.148 +val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.149 "12 / 3 = 4";
1.150 val thy = Test.thy;
1.151 val t = (term_of o the o (parse thy)) "4 ^^^ 2";
1.152 -val Some (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_"))) t;
1.153 -val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.154 +val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_"))) t;
1.155 +val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.156 "4 ^ 2 = 16";
1.157
1.158 val t = (term_of o the o (parse thy)) "((1 + 2) * 4 / 3) ^^^ 2";
1.159 - val Some (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t;
1.160 + val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t;
1.161 "1 + 2 = 3";
1.162 - val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.163 + val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.164 Sign.string_of_term (sign_of thy) t;
1.165 "(3 * 4 / 3) ^^^ 2";
1.166 - val Some (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"times")))t;
1.167 + val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"times")))t;
1.168 "3 * 4 = 12";
1.169 - val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.170 + val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.171 Sign.string_of_term (sign_of thy) t;
1.172 "(12 / 3) ^^^ 2";
1.173 - val Some (thmID,thm) =get_calculation_ thy(the(assoc(calclist,"divide_")))t;
1.174 + val SOME (thmID,thm) =get_calculation_ thy(the(assoc(calclist,"divide_")))t;
1.175 "12 / 3 = 4";
1.176 - val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.177 + val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.178 Sign.string_of_term (sign_of thy) t;
1.179 "4 ^^^ 2";
1.180 - val Some (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_")))t;
1.181 + val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_")))t;
1.182 "4 ^^^ 2 = 16";
1.183 - val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.184 + val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.185 Sign.string_of_term (sign_of thy) t;
1.186 "16";
1.187 if it <> "16" then raise error "calculate.sml: new behaviour in calculate_"
1.188 @@ -410,7 +410,7 @@
1.189
1.190 (*13.9.02 *** calc: operator = pow not defined*)
1.191 val t = (term_of o the o (parse thy)) "3^^^2";
1.192 - val Some (thmID,thm) =
1.193 + val SOME (thmID,thm) =
1.194 get_calculation_ thy (the(assoc(calclist,"power_"))) t;
1.195 (*** calc: operator = pow not defined*)
1.196
1.197 @@ -419,14 +419,14 @@
1.198 val op_ = "Atools.pow" : string
1.199 val eval_fn = fn : string -> term -> theory -> (string * term) option*)
1.200
1.201 - val Some (thmid,t') = get_pair thy op_ eval_fn t;
1.202 + val SOME (thmid,t') = get_pair thy op_ eval_fn t;
1.203 (*** calc: operator = pow not defined*)
1.204
1.205 - val Some (id,t') = eval_fn op_ t thy;
1.206 + val SOME (id,t') = eval_fn op_ t thy;
1.207 (*** calc: operator = pow not defined*)
1.208
1.209 val (thmid, (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) = (op_, t);
1.210 - val Some (id,t') = eval_binop thmid op_ t thy;
1.211 + val SOME (id,t') = eval_binop thmid op_ t thy;
1.212 (*** calc: operator = pow not defined*)
1.213
1.214
1.215 @@ -439,7 +439,7 @@
1.216 str2term
1.217 "[] from_ [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) / 2"
1.218 );
1.219 -val Some (str, simpl) = get_pair thy op_ ef arg;
1.220 +val SOME (str, simpl) = get_pair thy op_ ef arg;
1.221 if str =
1.222 "[] from_ [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) / 2 = True"
1.223 then () else raise error "calculate.sml get_pair with 3 args:occur_exactly_in";
1.224 @@ -462,10 +462,10 @@
1.225 "------------------ 3.6.03 (2 * x is_const) ---------------------------";
1.226 "------------------ 3.6.03 (2 * x is_const) ---------------------------";
1.227 val t = str2term "2 * x is_const";
1.228 -val Some (str, t') = eval_const "" "" t Test.thy;
1.229 +val SOME (str, t') = eval_const "" "" t Test.thy;
1.230 term2str t';
1.231 "(2 * x is_const) = False";
1.232
1.233 -val Some (t',_) = rewrite_set_ Test.thy false tval_rls t;
1.234 +val SOME (t',_) = rewrite_set_ Test.thy false tval_rls t;
1.235 term2str t';
1.236 "False";