1.1 --- a/test/Tools/isac/ProgLang/evaluate.sml Thu Jul 28 11:43:27 2022 +0200
1.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml Sat Jul 30 16:47:45 2022 +0200
1.3 @@ -48,6 +48,7 @@
1.4 (* fun rewrite__set_ \<longrightarrow> fun rew_once works the same way *)
1.5 val t = TermC.str2term "((1+2)*4/3) \<up> 2";
1.6 val thy = @{theory};
1.7 +val ctxt = Proof_Context.init_global @{theory}
1.8 val times = ("Groups.times_class.times", eval_binop "#mult_") : string * Eval_Def.eval_fn;
1.9 val plus = ("Groups.plus_class.plus", eval_binop "#add_") : string * Eval_Def.eval_fn;
1.10 val divide = ("Rings.divide_class.divide", eval_cancel "#divide_e") : string * Eval_Def.eval_fn;
1.11 @@ -55,22 +56,22 @@
1.12
1.13 "~~~~~ fun calculate_ , args:"; val (thy, isa_fn, t) = (thy, plus, t);
1.14 val SOME ("#: 1 + 2 = 3", adh_thm) = adhoc_thm @{theory} isa_fn t;
1.15 -val SOME (t', []) = rewrite__ thy 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
1.16 +val SOME (t', []) = rewrite__ ctxt 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
1.17 if UnparseC.term t' = "(3 * 4 / 3) \<up> 2" then () else error "calculate_ 1 + 2 = 3 changed";
1.18
1.19 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, times, t');
1.20 val SOME ("#: 3 * 4 = 12", adh_thm) = adhoc_thm @{theory} isa_fn t';
1.21 -val SOME (t'', []) = rewrite__ thy 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
1.22 +val SOME (t'', []) = rewrite__ ctxt 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
1.23 if UnparseC.term t'' = "(12 / 3) \<up> 2" then () else error "calculate_ 3 * 4 = 12 changed";
1.24
1.25 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, divide, t'');
1.26 val SOME ("#divide_e12_3", adh_thm) = adhoc_thm @{theory} isa_fn t;
1.27 -val SOME (t''', []) = rewrite__ thy 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
1.28 +val SOME (t''', []) = rewrite__ ctxt 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
1.29 if UnparseC.term t''' = "4 \<up> 2" then () else error "calculate_ 12 / 3 = 4 changed";
1.30
1.31 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, pow, t''');
1.32 val SOME ("#: 4 \<up> 2 = 16", adh_thm) = adhoc_thm @{theory} isa_fn t;
1.33 -val SOME (t'''', []) = rewrite__ thy 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
1.34 +val SOME (t'''', []) = rewrite__ ctxt 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
1.35 if UnparseC.term t'''' = "16" then () else error "calculate_ 12 / 3 = 4 changed";
1.36
1.37 "----------- calculate from Prog --------------------------------- -----------------------------";
1.38 @@ -121,7 +122,7 @@
1.39 val op_ = the (LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE"));
1.40 val ct = @{term
1.41 "sqrt (x \<up> 2 + -3 * x) = (-9) / (- 2) + (-3 / (- 2) + (x * ((-4) / (- 2)) + x * (2 / (- 2))))"};
1.42 -case calculate_ thy op_ ct of
1.43 +case calculate_ ctxt op_ ct of
1.44 SOME _ => ()
1.45 | NONE => error "calculate_ test-root-equ changed";
1.46 (*
1.47 @@ -134,13 +135,13 @@
1.48 val ctxt = (ThyC.id_to_ctxt "Test")
1.49 val t = TermC.parseNEW' ctxt "6 / 2";
1.50 val rls = Test_simplify;
1.51 - val (t,_) = the (rewrite_set_ thy false rls t);
1.52 + val (t,_) = the (rewrite_set_ ctxt false rls t);
1.53 (*val t = Free ("3", "Real.real") : term*)
1.54
1.55 (*--------------(3): is_num works ?: -------------------------------------*)
1.56 val t = TermC.parseNEW' ctxt "2 is_num";
1.57 TermC.atomty t;
1.58 - rewrite_set_ @{theory Test} false tval_rls t;
1.59 + rewrite_set_ ctxt false tval_rls t;
1.60 (*val it = SOME (Const (\<^const_name>\<open>True\<close>, "bool"),[]) ... works*)
1.61
1.62 val t = TermC.str2term "2 * x is_num";
1.63 @@ -151,7 +152,6 @@
1.64 "----------- check calculate bottom up ------------------";
1.65 "----------- check calculate bottom up ------------------";
1.66 (*-------------- eval_cancel works: *)
1.67 - Rewrite.trace_on := false; (*true false*)
1.68 val thy = @{theory Test};
1.69 val rls = Test_simplify;
1.70 val t = TermC.parseNEW' ctxt "(-4) / 2";
1.71 @@ -160,21 +160,19 @@
1.72
1.73 (*--------------(5): reproduce (1) with simpler term: ------------*)
1.74 val t = TermC.parseNEW' ctxt "(3+5)/(2::real)";
1.75 -case rewrite_set_ thy false rls t of
1.76 +case rewrite_set_ ctxt false rls t of
1.77 SOME (t', []) =>
1.78 if UnparseC.term t' = "4" then ()
1.79 else error "rewrite_set_ (3+5)/2 changed 1"
1.80 | _ => error "rewrite_set_ (3+5)/2 changed 2";
1.81
1.82 val t = TermC.parseNEW' ctxt "(3+1+2*x)/(2::real)";
1.83 -case rewrite_set_ thy false rls t of
1.84 +case rewrite_set_ ctxt false rls t of
1.85 SOME (t', _) =>
1.86 if UnparseC.term t' = "2 + x" then () else error "rewrite_set_ (3+1+2*x)/2 changed 1"
1.87 | _ => error "rewrite_set_ (3+1+2*x)/2 changed 2";
1.88
1.89 - Rewrite.trace_on := false; (*true false*)
1.90 -
1.91 -(*--- Rewrite.trace_on before correction of ... --------------------
1.92 +(*--- trace_rewrite before correction of ... --------------------
1.93 val ct = "(-3 + 2 * x + - 1) / 2";
1.94 val (ct,_) = the (rewrite_set thy' false rls ct);
1.95 :
1.96 @@ -203,9 +201,8 @@
1.97
1.98
1.99 (*===================*)
1.100 - Rewrite.trace_on:=false; (*WN130722: =true stopped Test_Isac.thy*)
1.101 val t = TermC.parseNEW' ctxt "x + (- 1 + -3) / (2::real)";
1.102 -val SOME (res, []) = rewrite_set_ thy false rls t;
1.103 +val SOME (res, []) = rewrite_set_ ctxt false rls t;
1.104 if UnparseC.term res = "- 2 + x" then () else error "rewrite_set_ x + (- 1 + -3) / 2 changed";
1.105 "x + (-4) / 2";
1.106 (*
1.107 @@ -221,8 +218,6 @@
1.108 ### trying calc. 'pow'
1.109 *)
1.110
1.111 - Rewrite.trace_on:=false; (*WN130722: =true stopped Test_Isac.thy*)
1.112 -
1.113 " ================= evaluate.sml: calculate_ 2002 =================== ";
1.114 " ================= evaluate.sml: calculate_ 2002 =================== ";
1.115 " ================= evaluate.sml: calculate_ 2002 =================== ";
1.116 @@ -230,33 +225,33 @@
1.117 val thy = @{theory Test};
1.118 val t = TermC.parseNEW' ctxt "12 / 3";
1.119 val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t;
1.120 -val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.121 +val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
1.122 "12 / 3 = 4";
1.123 val thy = @{theory Test};
1.124 val t = TermC.parseNEW' ctxt "4 \<up> 2";
1.125 val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;
1.126 -val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.127 +val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
1.128 "4 ^ 2 = 16";
1.129
1.130 val t = TermC.parseNEW' ctxt "((1 + 2) * 4 / 3) \<up> 2";
1.131 val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t;
1.132 "1 + 2 = 3";
1.133 - val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.134 + val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
1.135 UnparseC.term t;
1.136 "(3 * 4 / 3) \<up> 2";
1.137 val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES")))t;
1.138 "3 * 4 = 12";
1.139 - val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.140 + val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
1.141 UnparseC.term t;
1.142 "(12 / 3) \<up> 2";
1.143 val SOME (thmID,thm) =adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t;
1.144 "12 / 3 = 4";
1.145 - val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.146 + val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
1.147 UnparseC.term t;
1.148 "4 \<up> 2";
1.149 val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER")))t;
1.150 "4 \<up> 2 = 16";
1.151 - val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.152 + val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
1.153 UnparseC.term t;
1.154 "16";
1.155 if it <> "16" then error "evaluate.sml: new behaviour in calculate_"
1.156 @@ -342,7 +337,7 @@
1.157 if UnparseC.term t' = "(2 * x is_num) = False" then ()
1.158 else error "is_num 2 * x is_num CHANGED";
1.159
1.160 -val SOME (t',_) = rewrite_set_ @{theory Test} false tval_rls t;
1.161 +val SOME (t',_) = rewrite_set_ ctxt false tval_rls t;
1.162 if UnparseC.term t' = "False" then ()
1.163 else error "rewrite_set_ 2 * x is_num CHANGED";
1.164