wneuper/isa: comparison test/Tools/isac/ProgLang/evaluate.sml

equal deleted inserted replaced

-:a4d8e2874627
+:70b30d910fd5
 "----------- check return value of adhoc_thm  ----";
 "----------- check return value of adhoc_thm  ----";
 val thy = @{theory "Poly"};
 val cal = snd (assoc_calc' thy "is_polyexp");
 val t = @{term "(x / x) is_polyexp"};
-val SOME (thmID, thm) = adhoc_thm thy cal t;
+val SOME (thmID, thm) = adhoc_thm ctxt cal t;
 (HOLogic.dest_Trueprop (Thm.prop_of thm); writeln "all thms wrapped by Trueprop")
 handle TERM _ =>
 error "evaluate.sml: adhoc_thm must return Trueprop";
 "----------- fun calculate_ --------------------------------------------------------------------";
 val plus =   ("Groups.plus_class.plus", Calc_Binop.numeric "#add_") : string * Eval_Def.eval_fn;
 val divide = ("Rings.divide_class.divide", eval_cancel "#divide_e") : string * Eval_Def.eval_fn;
 val pow =    (\<^const_name>\<open>realpow\<close>, Calc_Binop.numeric "#power_") : string * Eval_Def.eval_fn;
 "~~~~~ fun calculate_ , args:"; val (thy, isa_fn, t) = (thy, plus, t);
-val SOME ("#: 1 + 2 = 3", adh_thm) = adhoc_thm @{theory} isa_fn t;
+val SOME ("#: 1 + 2 = 3", adh_thm) = adhoc_thm @{context} isa_fn t;
 val SOME (t', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t;
 if UnparseC.term t' = "(3 * 4 / 3) \<up> 2" then () else error "calculate_  1 + 2 = 3  changed";
 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, times, t');
-val SOME ("#: 3 * 4 = 12", adh_thm) = adhoc_thm @{theory} isa_fn t';
+val SOME ("#: 3 * 4 = 12", adh_thm) = adhoc_thm @{context} isa_fn t';
 val SOME (t'', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t;
 if UnparseC.term t'' = "(12 / 3) \<up> 2" then () else error "calculate_  3 * 4 = 12  changed";
 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, divide, t'');
-val SOME ("#divide_e12_3", adh_thm) = adhoc_thm @{theory} isa_fn t;
+val SOME ("#divide_e12_3", adh_thm) = adhoc_thm @{context} isa_fn t;
 val SOME (t''', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t;
 if UnparseC.term t''' = "4 \<up> 2" then () else error "calculate_  12 / 3 = 4  changed";
 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, pow, t''');
-val SOME ("#: 4 \<up> 2 = 16", adh_thm) = adhoc_thm @{theory} isa_fn t;
+val SOME ("#: 4 \<up> 2 = 16", adh_thm) = adhoc_thm @{context} isa_fn t;
 val SOME (t'''', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t;
 if UnparseC.term t'''' = "16" then () else error "calculate_  12 / 3 = 4  changed";
 "----------- calculate from Prog --------------------------------- -----------------------------";
 "----------- calculate from Prog --------------------------------- -----------------------------";
 " ================= evaluate.sml: calculate_ 2002 =================== ";
 " ================= evaluate.sml: calculate_ 2002 =================== ";
 val thy = @{theory Test};
 val t = TermC.parseNEW' ctxt "12 / 3";
-val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t;
+val SOME (thmID,thm) = adhoc_thm ctxt(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t;
 val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
 "12 / 3 = 4";
 val thy = @{theory Test};
 val t = TermC.parseNEW' ctxt "4 \<up> 2";
-val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;
+val SOME (thmID,thm) = adhoc_thm ctxt(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;
 val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
 "4 ^ 2 = 16";
 val t = TermC.parseNEW' ctxt "((1 + 2) * 4 / 3) \<up> 2";
-val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t;
+val SOME (thmID,thm) = adhoc_thm ctxt (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t;
 "1 + 2 = 3";
 val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
 UnparseC.term t;
 "(3 * 4 / 3) \<up> 2";
-val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES")))t;
+val SOME (thmID,thm) = adhoc_thm ctxt (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES")))t;
 "3 * 4 = 12";
 val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
 UnparseC.term t;
 "(12 / 3) \<up> 2";
-val SOME (thmID,thm) =adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t;
+val SOME (thmID,thm) =adhoc_thm ctxt(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t;
 "12 / 3 = 4";
 val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
 UnparseC.term t;
 "4 \<up> 2";
-val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER")))t;
+val SOME (thmID,thm) = adhoc_thm ctxt(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER")))t;
 "4 \<up> 2 = 16";
 val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
 UnparseC.term t;
 "16";
 if it <> "16" then error "evaluate.sml: new behaviour in calculate_"
 else ();
 (*13.9.02 *** calc: operator = pow not defined*)
 val t = TermC.parseNEW' ctxt  "3 \<up> 2";
 val SOME (thmID,thm) =
-adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;
+adhoc_thm ctxt (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;
 (*** calc: operator = pow not defined*)
 val (op_, eval_fn) = the (LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"));
 (*
 val op_ = \<^const_name>\<open>realpow\<close> : string
 "----------- fun adhoc_thm: examples -----------------------------------------------------------";
 "----------- fun adhoc_thm: examples -----------------------------------------------------------";
 (*--------------------------------------------------------------------vvvvvvvvvv*)
 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "is_num");
 val t = @{term "9 is_num"};
-val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
+val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
 if str = "#is_num_9_" andalso ThmC_Def.string_of_thm thm = "(9 is_num) = True"
 then () else error "adhoc_thm  9 is_num  changed";
 case assoc_calc thy \<^const_name>\<open>less\<close> of
 "le" => () | _ => error "Orderings.ord_class.less <-> le changed";
 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "le");
 if isa_str = "Orderings.ord_class.less" then () else error "adhoc_thm (4 < 4) = False CHANGED";
 val t = @{term "4 < (4 :: real)"};
-val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
+val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
 if str = "#less_4_4" andalso ThmC_Def.string_of_thm thm = "(4 < 4) = False"
 then () else error "adhoc_thm  4 < 4  changed";
 val SOME t = parseNEW @{context} "a < 4";
-case adhoc_thm thy (isa_str, eval_fn) t of
+case adhoc_thm ctxt (isa_str, eval_fn) t of
 NONE => () | _ => error "adhoc_thm  a < 4  does NOT result in NONE";
 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "PLUS");
 val SOME t = parseNEW @{context} "1 + (2::real)";
-val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
+val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
 if str = "#: 1 + 2 = 3" andalso ThmC_Def.string_of_thm thm = "1 + 2 = 3"
 then () else error "adhoc_thm  1 + 2  changed";
 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE");
 val t = @{term "6 / -8 :: real"};
-val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
+val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
 if str = "#divide_e6_~8" andalso ThmC_Def.string_of_thm thm = "6 / - 8 = - 3 / 4"
 then () else error "adhoc_thm  6 / -8 = - 3 / 4  changed";
 case assoc_calc thy "Prog_Expr.ident" of
 "ident" => () | _ => error "Prog_Expr.ident <-> ident  changed";
 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "ident");
 val t = @{term "3 =!= (3 :: real)"};
-val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
+val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
 if str = "#ident_(3)_(3)" andalso ThmC_Def.string_of_thm thm = "(3 =!= 3) = True"
 then () else error "adhoc_thm  (3 =!= 3)  changed";
 val t = @{term "\<not> ((4 :: real) + (4 * x + x \<up> 2) =!= 0)"};
-val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
+val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
 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"
 then () else error "adhoc_thm  (\<not> (4 + (4 * x + x ^ 2) =!= 0))  changed";
 "----------- fun adhoc_thm + fun eval_cancel ---------------------------------------------------";
 "----------- fun adhoc_thm + fun eval_cancel ---------------------------------------------------";
 Eval.get_pair for \<^const_name>\<open>divide\<close> \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2")
 but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE
 STEP-INTO BEVORE REMOVING THE ERROR:
 val SOME ("#divide_e~1_2", adhoc_thm) =
-Eval.adhoc_thm @{theory} eval_ t;
+Eval.adhoc_thm @{context} eval_ t;
 "~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), t) = (@{theory}, eval_, t);
 val SOME
 ("#divide_e~1_2", t'') =
 (*case*) get_pair ctxt op_ eval_fn t (*of*);
 (*
 \<^ML_type>\<open>eval_fn\<close>. In case of \<^ML>\<open>eval_cancel\<close> the return value WAS the same as the input..
 *)
 (*+*)ThmC.string_of_thm adhoc_thm = "- 1 / 2 = - 1 / 2"
 *)
-val NONE = adhoc_thm @{theory} eval_ t;
+val NONE = adhoc_thm @{context} eval_ t;
 "~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), t) = (@{theory}, eval_, t);
 val NONE =
 (*case*) get_pair ctxt op_ eval_fn t (*of*);
 "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
 "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
 "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
 val t = TermC.str2term "sqrt 4";
-Eval.adhoc_thm (ThyC.get_theory "Isac_Knowledge") ("NthRoot.sqrt", eval_sqrt "#sqrt_") t;
+Eval.adhoc_thm @{context} ("NthRoot.sqrt", eval_sqrt "#sqrt_") t;
 "~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), ct) =
 ((ThyC.get_theory "Isac_Knowledge"),
 ("NthRoot.sqrt", eval_sqrt "#sqrt_": string -> term -> Proof.context -> (string * term) option), t);

changeset 60519	70b30d910fd5
parent 60516	795d1352493a
child 60538	b44ed7b738f4