1.1 --- a/test/Tools/isac/ProgLang/evaluate.sml Fri Aug 05 11:41:06 2022 +0200
1.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml Fri Aug 05 12:30:16 2022 +0200
1.3 @@ -37,7 +37,7 @@
1.4 val thy = @{theory "Poly"};
1.5 val cal = snd (assoc_calc' thy "is_polyexp");
1.6 val t = @{term "(x / x) is_polyexp"};
1.7 -val SOME (thmID, thm) = adhoc_thm thy cal t;
1.8 +val SOME (thmID, thm) = adhoc_thm ctxt cal t;
1.9 (HOLogic.dest_Trueprop (Thm.prop_of thm); writeln "all thms wrapped by Trueprop")
1.10 handle TERM _ =>
1.11 error "evaluate.sml: adhoc_thm must return Trueprop";
1.12 @@ -55,22 +55,22 @@
1.13 val pow = (\<^const_name>\<open>realpow\<close>, Calc_Binop.numeric "#power_") : string * Eval_Def.eval_fn;
1.14
1.15 "~~~~~ fun calculate_ , args:"; val (thy, isa_fn, t) = (thy, plus, t);
1.16 -val SOME ("#: 1 + 2 = 3", adh_thm) = adhoc_thm @{theory} isa_fn t;
1.17 +val SOME ("#: 1 + 2 = 3", adh_thm) = adhoc_thm @{context} isa_fn t;
1.18 val SOME (t', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t;
1.19 if UnparseC.term t' = "(3 * 4 / 3) \<up> 2" then () else error "calculate_ 1 + 2 = 3 changed";
1.20
1.21 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, times, t');
1.22 -val SOME ("#: 3 * 4 = 12", adh_thm) = adhoc_thm @{theory} isa_fn t';
1.23 +val SOME ("#: 3 * 4 = 12", adh_thm) = adhoc_thm @{context} isa_fn t';
1.24 val SOME (t'', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t;
1.25 if UnparseC.term t'' = "(12 / 3) \<up> 2" then () else error "calculate_ 3 * 4 = 12 changed";
1.26
1.27 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, divide, t'');
1.28 -val SOME ("#divide_e12_3", adh_thm) = adhoc_thm @{theory} isa_fn t;
1.29 +val SOME ("#divide_e12_3", adh_thm) = adhoc_thm @{context} isa_fn t;
1.30 val SOME (t''', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t;
1.31 if UnparseC.term t''' = "4 \<up> 2" then () else error "calculate_ 12 / 3 = 4 changed";
1.32
1.33 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, pow, t''');
1.34 -val SOME ("#: 4 \<up> 2 = 16", adh_thm) = adhoc_thm @{theory} isa_fn t;
1.35 +val SOME ("#: 4 \<up> 2 = 16", adh_thm) = adhoc_thm @{context} isa_fn t;
1.36 val SOME (t'''', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t;
1.37 if UnparseC.term t'''' = "16" then () else error "calculate_ 12 / 3 = 4 changed";
1.38
1.39 @@ -224,32 +224,32 @@
1.40
1.41 val thy = @{theory Test};
1.42 val t = TermC.parseNEW' ctxt "12 / 3";
1.43 -val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t;
1.44 +val SOME (thmID,thm) = adhoc_thm ctxt(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t;
1.45 val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
1.46 "12 / 3 = 4";
1.47 val thy = @{theory Test};
1.48 val t = TermC.parseNEW' ctxt "4 \<up> 2";
1.49 -val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;
1.50 +val SOME (thmID,thm) = adhoc_thm ctxt(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;
1.51 val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
1.52 "4 ^ 2 = 16";
1.53
1.54 val t = TermC.parseNEW' ctxt "((1 + 2) * 4 / 3) \<up> 2";
1.55 - val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t;
1.56 + val SOME (thmID,thm) = adhoc_thm ctxt (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t;
1.57 "1 + 2 = 3";
1.58 val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
1.59 UnparseC.term t;
1.60 "(3 * 4 / 3) \<up> 2";
1.61 - val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES")))t;
1.62 + val SOME (thmID,thm) = adhoc_thm ctxt (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES")))t;
1.63 "3 * 4 = 12";
1.64 val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
1.65 UnparseC.term t;
1.66 "(12 / 3) \<up> 2";
1.67 - val SOME (thmID,thm) =adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t;
1.68 + val SOME (thmID,thm) =adhoc_thm ctxt(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t;
1.69 "12 / 3 = 4";
1.70 val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
1.71 UnparseC.term t;
1.72 "4 \<up> 2";
1.73 - val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER")))t;
1.74 + val SOME (thmID,thm) = adhoc_thm ctxt(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER")))t;
1.75 "4 \<up> 2 = 16";
1.76 val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
1.77 UnparseC.term t;
1.78 @@ -260,7 +260,7 @@
1.79 (*13.9.02 *** calc: operator = pow not defined*)
1.80 val t = TermC.parseNEW' ctxt "3 \<up> 2";
1.81 val SOME (thmID,thm) =
1.82 - adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;
1.83 + adhoc_thm ctxt (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;
1.84 (*** calc: operator = pow not defined*)
1.85
1.86 val (op_, eval_fn) = the (LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"));
1.87 @@ -388,7 +388,7 @@
1.88 (*--------------------------------------------------------------------vvvvvvvvvv*)
1.89 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "is_num");
1.90 val t = @{term "9 is_num"};
1.91 -val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
1.92 +val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
1.93 if str = "#is_num_9_" andalso ThmC_Def.string_of_thm thm = "(9 is_num) = True"
1.94 then () else error "adhoc_thm 9 is_num changed";
1.95
1.96 @@ -398,23 +398,23 @@
1.97 if isa_str = "Orderings.ord_class.less" then () else error "adhoc_thm (4 < 4) = False CHANGED";
1.98
1.99 val t = @{term "4 < (4 :: real)"};
1.100 -val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
1.101 +val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
1.102 if str = "#less_4_4" andalso ThmC_Def.string_of_thm thm = "(4 < 4) = False"
1.103 then () else error "adhoc_thm 4 < 4 changed";
1.104
1.105 val SOME t = parseNEW @{context} "a < 4";
1.106 -case adhoc_thm thy (isa_str, eval_fn) t of
1.107 +case adhoc_thm ctxt (isa_str, eval_fn) t of
1.108 NONE => () | _ => error "adhoc_thm a < 4 does NOT result in NONE";
1.109
1.110 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "PLUS");
1.111 val SOME t = parseNEW @{context} "1 + (2::real)";
1.112 -val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
1.113 +val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
1.114 if str = "#: 1 + 2 = 3" andalso ThmC_Def.string_of_thm thm = "1 + 2 = 3"
1.115 then () else error "adhoc_thm 1 + 2 changed";
1.116
1.117 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE");
1.118 val t = @{term "6 / -8 :: real"};
1.119 -val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
1.120 +val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
1.121 if str = "#divide_e6_~8" andalso ThmC_Def.string_of_thm thm = "6 / - 8 = - 3 / 4"
1.122 then () else error "adhoc_thm 6 / -8 = - 3 / 4 changed";
1.123
1.124 @@ -423,12 +423,12 @@
1.125 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "ident");
1.126
1.127 val t = @{term "3 =!= (3 :: real)"};
1.128 -val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
1.129 +val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
1.130 if str = "#ident_(3)_(3)" andalso ThmC_Def.string_of_thm thm = "(3 =!= 3) = True"
1.131 then () else error "adhoc_thm (3 =!= 3) changed";
1.132
1.133 val t = @{term "\<not> ((4 :: real) + (4 * x + x \<up> 2) =!= 0)"};
1.134 -val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
1.135 +val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
1.136 if str = "#ident_(4 + (4 * x + x \<up> 2))_(0)" andalso ThmC_Def.string_of_thm thm = "(4 + (4 * x + x \<up> 2) =!= 0) = False"
1.137 then () else error "adhoc_thm (\<not> (4 + (4 * x + x ^ 2) =!= 0)) changed";
1.138
1.139 @@ -448,7 +448,7 @@
1.140
1.141 STEP-INTO BEVORE REMOVING THE ERROR:
1.142 val SOME ("#divide_e~1_2", adhoc_thm) =
1.143 - Eval.adhoc_thm @{theory} eval_ t;
1.144 + Eval.adhoc_thm @{context} eval_ t;
1.145 "~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), t) = (@{theory}, eval_, t);
1.146 val SOME
1.147 ("#divide_e~1_2", t'') =
1.148 @@ -460,7 +460,7 @@
1.149 (*+*)ThmC.string_of_thm adhoc_thm = "- 1 / 2 = - 1 / 2"
1.150 *)
1.151
1.152 -val NONE = adhoc_thm @{theory} eval_ t;
1.153 +val NONE = adhoc_thm @{context} eval_ t;
1.154 "~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), t) = (@{theory}, eval_, t);
1.155 val NONE =
1.156 (*case*) get_pair ctxt op_ eval_fn t (*of*);
1.157 @@ -470,7 +470,7 @@
1.158 "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
1.159 "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
1.160 val t = TermC.str2term "sqrt 4";
1.161 -Eval.adhoc_thm (ThyC.get_theory "Isac_Knowledge") ("NthRoot.sqrt", eval_sqrt "#sqrt_") t;
1.162 +Eval.adhoc_thm @{context} ("NthRoot.sqrt", eval_sqrt "#sqrt_") t;
1.163
1.164 "~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), ct) =
1.165 ((ThyC.get_theory "Isac_Knowledge"),