--- a/NEWS Thu Sep 18 14:06:58 2008 +0200
+++ b/NEWS Thu Sep 18 19:39:44 2008 +0200
@@ -22,6 +22,13 @@
*** Pure ***
+* Simplified ML oracle interface Thm.add_oracle promotes 'a -> cterm
+to 'a -> thm, at the cost of internal tagging of results with an
+authentic oracle name. The Isar command 'oracle' is now polymorphic,
+no argument type is specified. INCOMPATIBILITY, need to simplify
+existing oracle code accordingly. Note that extra performance may be
+gained by producing the cterm carefully, not via Thm.cterm_of.
+
* Changed defaults for unify configuration options:
unify_trace_bound = 50 (formerly 25)
--- a/doc-src/IsarImplementation/Thy/logic.thy Thu Sep 18 14:06:58 2008 +0200
+++ b/doc-src/IsarImplementation/Thy/logic.thy Thu Sep 18 19:39:44 2008 +0200
@@ -595,12 +595,12 @@
@{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\
@{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\
@{index_ML Thm.get_axiom_i: "theory -> string -> thm"} \\
- @{index_ML Thm.invoke_oracle_i: "theory -> string -> theory * Object.T -> thm"} \\
+ @{index_ML Thm.add_oracle: "bstring * ('a -> cterm) -> theory
+ -> (string * ('a -> thm)) * theory"} \\
\end{mldecls}
\begin{mldecls}
@{index_ML Theory.add_axioms_i: "(string * term) list -> theory -> theory"} \\
@{index_ML Theory.add_deps: "string -> string * typ -> (string * typ) list -> theory -> theory"} \\
- @{index_ML Theory.add_oracle: "string * (theory * Object.T -> term) -> theory -> theory"} \\
@{index_ML Theory.add_defs_i: "bool -> bool -> (bstring * term) list -> theory -> theory"} \\
\end{mldecls}
@@ -651,16 +651,13 @@
\item @{ML Thm.get_axiom_i}~@{text "thy name"} retrieves a named
axiom, cf.\ @{text "axiom"} in \figref{fig:prim-rules}.
- \item @{ML Thm.invoke_oracle_i}~@{text "thy name arg"} invokes a
- named oracle function, cf.\ @{text "axiom"} in
- \figref{fig:prim-rules}.
+ \item @{ML Thm.add_oracle}~@{text "(name, oracle)"} produces a named
+ oracle rule, essentially generating arbitrary axioms on the fly,
+ cf.\ @{text "axiom"} in \figref{fig:prim-rules}.
\item @{ML Theory.add_axioms_i}~@{text "[(name, A), \<dots>]"} declares
arbitrary propositions as axioms.
- \item @{ML Theory.add_oracle}~@{text "(name, f)"} declares an oracle
- function for generating arbitrary axioms on the fly.
-
\item @{ML Theory.add_deps}~@{text "name c\<^isub>\<tau>
\<^vec>d\<^isub>\<sigma>"} declares dependencies of a named specification
for constant @{text "c\<^isub>\<tau>"}, relative to existing
--- a/doc-src/IsarRef/Thy/Spec.thy Thu Sep 18 14:06:58 2008 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy Thu Sep 18 19:39:44 2008 +0200
@@ -1136,9 +1136,8 @@
@{command_def "oracle"} & : & \isartrans{theory}{theory} \\
\end{matharray}
- The oracle interface promotes a given ML function @{ML_text
- "theory -> T -> term"} to @{ML_text "theory -> T -> thm"}, for some
- type @{ML_text T} given by the user. This acts like an infinitary
+ The oracle interface promotes a given ML function @{ML_text "'a -> cterm"}
+ to @{ML_text "'a -> thm"}. This acts like an infinitary
specification of axioms -- there is no internal check of the
correctness of the results! The inference kernel records oracle
invocations within the internal derivation object of theorems, and
@@ -1146,18 +1145,16 @@
that are not fully checked by Isabelle inferences.
\begin{rail}
- 'oracle' name '(' type ')' '=' text
+ 'oracle' name '=' text
;
\end{rail}
\begin{descr}
- \item [@{command "oracle"}~@{text "name (type) = text"}] turns the
- given ML expression @{text "text"} of type
- @{ML_text "theory ->"}~@{text "type"}~@{ML_text "-> term"} into an
- ML function of type
- @{ML_text "theory ->"}~@{text "type"}~@{ML_text "-> thm"}, which is
- bound to the global identifier @{ML_text name}.
+ \item [@{command "oracle"}~@{text "name = text"}] turns the given ML
+ expression @{text "text"} of type @{ML_text "'a -> cterm"} into an
+ ML function of type @{ML_text "'a -> thm"}, which is bound to the
+ global identifier @{ML_text name}.
\end{descr}
*}
--- a/src/FOL/ex/IffOracle.thy Thu Sep 18 14:06:58 2008 +0200
+++ b/src/FOL/ex/IffOracle.thy Thu Sep 18 19:39:44 2008 +0200
@@ -18,14 +18,14 @@
and positive.
*}
-oracle iff_oracle (int) = {*
+oracle iff_oracle = {*
let
fun mk_iff 1 = Var (("P", 0), @{typ o})
| mk_iff n = FOLogic.iff $ Var (("P", 0), @{typ o}) $ mk_iff (n - 1);
in
- fn thy => fn n =>
+ fn (thy, n) =>
if n > 0 andalso n mod 2 = 0
- then FOLogic.mk_Trueprop (mk_iff n)
+ then Thm.cterm_of thy (FOLogic.mk_Trueprop (mk_iff n))
else raise Fail ("iff_oracle: " ^ string_of_int n)
end
*}
@@ -33,19 +33,19 @@
subsection {* Oracle as low-level rule *}
-ML {* iff_oracle @{theory} 2 *}
-ML {* iff_oracle @{theory} 10 *}
-ML {* #der (Thm.rep_thm (iff_oracle @{theory} 10)) *}
+ML {* iff_oracle (@{theory}, 2) *}
+ML {* iff_oracle (@{theory}, 10) *}
+ML {* #der (Thm.rep_thm (iff_oracle (@{theory}, 10))) *}
text {* These oracle calls had better fail. *}
ML {*
- (iff_oracle @{theory} 5; error "?")
+ (iff_oracle (@{theory}, 5); error "?")
handle Fail _ => warning "Oracle failed, as expected"
*}
ML {*
- (iff_oracle @{theory} 1; error "?")
+ (iff_oracle (@{theory}, 1); error "?")
handle Fail _ => warning "Oracle failed, as expected"
*}
@@ -55,7 +55,7 @@
method_setup iff = {*
Method.simple_args OuterParse.nat (fn n => fn ctxt =>
Method.SIMPLE_METHOD
- (HEADGOAL (Tactic.rtac (iff_oracle (ProofContext.theory_of ctxt) n))
+ (HEADGOAL (Tactic.rtac (iff_oracle (ProofContext.theory_of ctxt, n)))
handle Fail _ => no_tac))
*} "iff oracle"
--- a/src/HOL/ATP_Linkup.thy Thu Sep 18 14:06:58 2008 +0200
+++ b/src/HOL/ATP_Linkup.thy Thu Sep 18 19:39:44 2008 +0200
@@ -101,9 +101,9 @@
use "Tools/res_atp_provers.ML"
-oracle vampire_oracle ("string * int") = {* ResAtpProvers.vampire_o *}
-oracle eprover_oracle ("string * int") = {* ResAtpProvers.eprover_o *}
-oracle spass_oracle ("string * int") = {* ResAtpProvers.spass_o *}
+oracle vampire_oracle = {* ResAtpProvers.vampire_o *}
+oracle eprover_oracle = {* ResAtpProvers.eprover_o *}
+oracle spass_oracle = {* ResAtpProvers.spass_o *}
use "Tools/res_atp_methods.ML"
setup ResAtpMethods.setup --{*Oracle ATP methods: still useful?*}
--- a/src/HOL/Code_Setup.thy Thu Sep 18 14:06:58 2008 +0200
+++ b/src/HOL/Code_Setup.thy Thu Sep 18 19:39:44 2008 +0200
@@ -129,17 +129,22 @@
end;
*}
-oracle eval_oracle ("term") = {* fn thy => fn t =>
- if Code_ML.eval_term ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy
- (HOLogic.dest_Trueprop t) []
- then t
- else HOLogic.Trueprop $ HOLogic.true_const (*dummy*)
+oracle eval_oracle = {* fn ct =>
+ let
+ val thy = Thm.theory_of_cterm ct;
+ val t = Thm.term_of ct;
+ in
+ if Code_ML.eval_term ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy
+ (HOLogic.dest_Trueprop t) []
+ then ct
+ else @{cprop True} (*dummy*)
+ end
*}
method_setup eval = {*
let
fun eval_tac thy =
- SUBGOAL (fn (t, i) => rtac (eval_oracle thy t) i)
+ CSUBGOAL (fn (ct, i) => rtac (eval_oracle ct) i)
in
Method.ctxt_args (fn ctxt =>
Method.SIMPLE_METHOD' (eval_tac (ProofContext.theory_of ctxt)))
--- a/src/HOL/Complex/ex/MIR.thy Thu Sep 18 14:06:58 2008 +0200
+++ b/src/HOL/Complex/ex/MIR.thy Thu Sep 18 19:39:44 2008 +0200
@@ -5791,7 +5791,7 @@
(*export_code mircfrqe mirlfrqe
in SML module_name Mir file "raw_mir.ML"*)
-oracle mirfr_oracle ("bool * term") = {*
+oracle mirfr_oracle = {* fn (proofs, ct) =>
let
fun num_of_term vs (t as Free (xn, xT)) = (case AList.lookup (op =) vs t
@@ -5891,13 +5891,15 @@
| term_of_fm vs (@{code Iff} (t1, t2)) =
@{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ term_of_fm vs t1 $ term_of_fm vs t2;
-in fn thy => fn (proofs, t) =>
+in
let
+ val thy = Thm.theory_of_cterm ct;
+ val t = Thm.term_of ct;
val fs = term_frees t;
val vs = fs ~~ (0 upto (length fs - 1));
val qe = if proofs then @{code mirlfrqe} else @{code mircfrqe};
val t' = (term_of_fm vs o qe o fm_of_term vs) t;
- in (HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end
+ in (cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end
end;
*}
--- a/src/HOL/Complex/ex/ReflectedFerrack.thy Thu Sep 18 14:06:58 2008 +0200
+++ b/src/HOL/Complex/ex/ReflectedFerrack.thy Thu Sep 18 19:39:44 2008 +0200
@@ -1997,7 +1997,7 @@
ML {* @{code ferrack_test} () *}
-oracle linr_oracle ("term") = {*
+oracle linr_oracle = {*
let
fun num_of_term vs (t as Free (xn, xT)) = (case AList.lookup (op =) vs t
@@ -2066,11 +2066,14 @@
term_of_fm vs t1 $ term_of_fm vs t2
| term_of_fm vs _ = error "If this is raised, Isabelle/HOL or generate_code is inconsistent.";
-in fn thy => fn t =>
+in fn ct =>
let
+ val thy = Thm.theory_of_cterm ct;
+ val t = Thm.term_of ct;
val fs = term_frees t;
val vs = fs ~~ (0 upto (length fs - 1));
- in HOLogic.mk_Trueprop (HOLogic.mk_eq (t, term_of_fm vs (@{code linrqe} (fm_of_term vs t)))) end
+ val res = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, term_of_fm vs (@{code linrqe} (fm_of_term vs t))));
+ in Thm.cterm_of thy res end
end;
*}
--- a/src/HOL/Complex/ex/linrtac.ML Thu Sep 18 14:06:58 2008 +0200
+++ b/src/HOL/Complex/ex/linrtac.ML Thu Sep 18 19:39:44 2008 +0200
@@ -86,7 +86,7 @@
(* The result of the quantifier elimination *)
val (th, tac) = case (prop_of pre_thm) of
Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
- let val pth = linr_oracle thy (Pattern.eta_long [] t1)
+ let val pth = linr_oracle (cterm_of thy (Pattern.eta_long [] t1))
in
(trace_msg ("calling procedure with term:\n" ^
Syntax.string_of_term ctxt t1);
--- a/src/HOL/Complex/ex/mirtac.ML Thu Sep 18 14:06:58 2008 +0200
+++ b/src/HOL/Complex/ex/mirtac.ML Thu Sep 18 19:39:44 2008 +0200
@@ -87,9 +87,9 @@
fun mir_tac ctxt q i =
(ObjectLogic.atomize_prems_tac i)
- THEN (simp_tac (HOL_basic_ss addsimps [@{thm "abs_ge_zero"}] addsimps simp_thms) i)
- THEN (REPEAT_DETERM (split_tac [@{thm "split_min"}, @{thm "split_max"},@{thm "abs_split"}] i))
- THEN (fn st =>
+ THEN (simp_tac (HOL_basic_ss addsimps [@{thm "abs_ge_zero"}] addsimps simp_thms) i)
+ THEN (REPEAT_DETERM (split_tac [@{thm "split_min"}, @{thm "split_max"},@{thm "abs_split"}] i))
+ THEN (fn st =>
let
val g = List.nth (prems_of st, i - 1)
val thy = ProofContext.theory_of ctxt
@@ -97,13 +97,13 @@
val (t,np,nh) = prepare_for_mir thy q g
(* Some simpsets for dealing with mod div abs and nat*)
val mod_div_simpset = HOL_basic_ss
- addsimps [refl,nat_mod_add_eq,
- @{thm "mod_self"}, @{thm "zmod_self"},
- @{thm "zdiv_zero"},@{thm "zmod_zero"},@{thm "div_0"}, @{thm "mod_0"},
- @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"}, @{thm "mod_1"},
- @{thm "Suc_plus1"}]
- addsimps @{thms add_ac}
- addsimprocs [cancel_div_mod_proc]
+ addsimps [refl,nat_mod_add_eq,
+ @{thm "mod_self"}, @{thm "zmod_self"},
+ @{thm "zdiv_zero"},@{thm "zmod_zero"},@{thm "div_0"}, @{thm "mod_0"},
+ @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"}, @{thm "mod_1"},
+ @{thm "Suc_plus1"}]
+ addsimps @{thms add_ac}
+ addsimprocs [cancel_div_mod_proc]
val simpset0 = HOL_basic_ss
addsimps [mod_div_equality', Suc_plus1]
addsimps comp_ths
@@ -131,11 +131,11 @@
(* The result of the quantifier elimination *)
val (th, tac) = case (prop_of pre_thm) of
Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
- let val pth =
+ let val pth =
(* If quick_and_dirty then run without proof generation as oracle*)
- if !quick_and_dirty
- then mirfr_oracle thy (false, Pattern.eta_long [] t1)
- else mirfr_oracle thy (true, Pattern.eta_long [] t1)
+ if !quick_and_dirty
+ then mirfr_oracle (false, cterm_of thy (Pattern.eta_long [] t1))
+ else mirfr_oracle (true, cterm_of thy (Pattern.eta_long [] t1))
in
(trace_msg ("calling procedure with term:\n" ^
Syntax.string_of_term ctxt t1);
--- a/src/HOL/Library/Eval_Witness.thy Thu Sep 18 14:06:58 2008 +0200
+++ b/src/HOL/Library/Eval_Witness.thy Thu Sep 18 19:39:44 2008 +0200
@@ -55,8 +55,10 @@
end;
*}
-oracle eval_witness_oracle ("term * string list") = {* fn thy => fn (goal, ws) =>
+oracle eval_witness_oracle = {* fn (cgoal, ws) =>
let
+ val thy = Thm.theory_of_cterm cgoal;
+ val goal = Thm.term_of cgoal;
fun check_type T =
if Sorts.of_sort (Sign.classes_of thy) (T, ["Eval_Witness.ml_equiv"])
then T
@@ -69,8 +71,8 @@
val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal);
in
if Code_ML.eval_term ("Eval_Witness_Method.eval_ref", Eval_Witness_Method.eval_ref) thy t ws
- then goal
- else HOLogic.Trueprop $ HOLogic.true_const (*dummy*)
+ then Thm.cterm_of thy goal
+ else @{cprop True} (*dummy*)
end
*}
@@ -78,12 +80,11 @@
method_setup eval_witness = {*
let
-fun eval_tac ws thy =
- SUBGOAL (fn (t, i) => rtac (eval_witness_oracle thy (t, ws)) i)
+fun eval_tac ws = CSUBGOAL (fn (ct, i) => rtac (eval_witness_oracle (ct, ws)) i)
-in
- Method.simple_args (Scan.repeat Args.name) (fn ws => fn ctxt =>
- Method.SIMPLE_METHOD' (eval_tac ws (ProofContext.theory_of ctxt)))
+in
+ Method.simple_args (Scan.repeat Args.name) (fn ws => fn _ =>
+ Method.SIMPLE_METHOD' (eval_tac ws))
end
*} "Evaluation with ML witnesses"
--- a/src/HOL/Modelcheck/EindhovenSyn.thy Thu Sep 18 14:06:58 2008 +0200
+++ b/src/HOL/Modelcheck/EindhovenSyn.thy Thu Sep 18 19:39:44 2008 +0200
@@ -30,7 +30,7 @@
val trace_eindhoven = ref false;
*}
-oracle mc_eindhoven_oracle ("term") =
+oracle mc_eindhoven_oracle =
{*
let
val eindhoven_term = PrintMode.setmp ["Eindhoven"] o Syntax.string_of_term_global;
@@ -43,15 +43,17 @@
else eindhoven_home ^ "/pmu";
in #1 (system_out ("echo \"" ^ s ^ "\" | " ^ pmu ^ " -w")) end;
in
- fn thy => fn goal =>
+ fn cgoal =>
let
+ val thy = Thm.theory_of_cterm cgoal;
+ val goal = Thm.term_of cgoal;
val s = eindhoven_term thy goal;
val debug = tracing ("MC debugger: " ^ s);
val result = call_mc s;
in
if ! trace_eindhoven then writeln (cat_lines [s, "----", result]) else ();
(case result of
- "TRUE\n" => goal |
+ "TRUE\n" => cgoal |
"FALSE\n" => error "MC oracle yields FALSE" |
_ => error ("MC syntax error: " ^ result))
end
@@ -62,7 +64,7 @@
fun mc_eindhoven_tac i state = SUBGOAL (fn (goal, _) =>
let
val thy = Thm.theory_of_thm state;
- val assertion = mc_eindhoven_oracle thy (Logic.strip_imp_concl goal);
+ val assertion = mc_eindhoven_oracle (Thm.cterm_of thy (Logic.strip_imp_concl goal));
in cut_facts_tac [assertion] i THEN atac i end) i state;
val pair_eta_expand = Thm.symmetric (mk_meta_eq (thm "split_eta"));
--- a/src/HOL/Modelcheck/MuckeSyn.thy Thu Sep 18 14:06:58 2008 +0200
+++ b/src/HOL/Modelcheck/MuckeSyn.thy Thu Sep 18 19:39:44 2008 +0200
@@ -68,8 +68,7 @@
will be replaced by the expression between the two asterisks
following "case" and the asterisk after esac will be deleted *)
-oracle mc_mucke_oracle ("term") =
- mk_mc_mucke_oracle
+oracle mc_mucke_oracle = mk_mc_mucke_oracle
ML {*
(* search_mu t searches for Mu terms in term t. In the case of nested Mu's,
@@ -154,12 +153,9 @@
end;
-fun call_mucke_tac i state =
-let val thy = Thm.theory_of_thm state;
- val OraAss = mc_mucke_oracle thy (Logic.nth_prem (i, Thm.prop_of state))
-in
-(cut_facts_tac [OraAss] i) state
-end;
+val call_mucke_tac = CSUBGOAL (fn (cgoal, i) =>
+let val OraAss = mc_mucke_oracle cgoal
+in cut_facts_tac [OraAss] i end);
(* transforming fun-defs into lambda-defs *)
--- a/src/HOL/Modelcheck/mucke_oracle.ML Thu Sep 18 14:06:58 2008 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML Thu Sep 18 19:39:44 2008 +0200
@@ -1012,8 +1012,12 @@
(**********************************************************)
-fun mk_mc_mucke_oracle sign subgoal =
- let val Freesubgoal = freeze_thaw subgoal;
+fun mk_mc_mucke_oracle csubgoal =
+ let
+ val sign = Thm.theory_of_cterm csubgoal;
+ val subgoal = Thm.term_of csubgoal;
+
+ val Freesubgoal = freeze_thaw subgoal;
val prems = Logic.strip_imp_prems Freesubgoal;
val concl = Logic.strip_imp_concl Freesubgoal;
@@ -1047,6 +1051,6 @@
(writeln ("\nmodelchecker input:\n" ^ MCstr ^ "\n/**** end ****/"))
else ();
(case (extract_result concl_str result) of
- true => (Logic.strip_imp_concl subgoal) |
+ true => cterm_of sign (Logic.strip_imp_concl subgoal) |
false => (error ("Mucke couldn't solve subgoal: \n" ^result))))
end;
--- a/src/HOL/Presburger.thy Thu Sep 18 14:06:58 2008 +0200
+++ b/src/HOL/Presburger.thy Thu Sep 18 19:39:44 2008 +0200
@@ -440,7 +440,7 @@
by simp_all
use "Tools/Qelim/cooper.ML"
-oracle linzqe_oracle ("term") = Coopereif.cooper_oracle
+oracle linzqe_oracle = Coopereif.cooper_oracle
use "Tools/Qelim/presburger.ML"
--- a/src/HOL/Tools/Qelim/cooper.ML Thu Sep 18 14:06:58 2008 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Thu Sep 18 19:39:44 2008 +0200
@@ -633,12 +633,14 @@
| NClosed n => term_of_qf ps vs (Nota (Closed n))
| _ => cooper "If this is raised, Isabelle/HOL or generate_code is inconsistent!";
-fun cooper_oracle thy t =
+fun cooper_oracle ct =
let
+ val thy = Thm.theory_of_cterm ct;
+ val t = Thm.term_of ct;
val (vs, ps) = pairself (map_index swap) (term_frees t, term_bools [] t);
in
- Logic.mk_equals (HOLogic.mk_Trueprop t,
- HOLogic.mk_Trueprop (term_of_qf ps vs (pa (qf_of_term ps vs t))))
+ Thm.cterm_of thy (Logic.mk_equals (HOLogic.mk_Trueprop t,
+ HOLogic.mk_Trueprop (term_of_qf ps vs (pa (qf_of_term ps vs t)))))
end;
end;
--- a/src/HOL/Tools/Qelim/presburger.ML Thu Sep 18 14:06:58 2008 +0200
+++ b/src/HOL/Tools/Qelim/presburger.ML Thu Sep 18 19:39:44 2008 +0200
@@ -152,8 +152,8 @@
let
val cpth =
if !quick_and_dirty
- then linzqe_oracle (ProofContext.theory_of ctxt)
- (Envir.beta_norm (Pattern.eta_long [] (term_of (Thm.dest_arg p))))
+ then linzqe_oracle (Thm.cterm_of (ProofContext.theory_of ctxt)
+ (Envir.beta_norm (Pattern.eta_long [] (term_of (Thm.dest_arg p)))))
else arg_conv (Cooper.cooper_conv ctxt) p
val p' = Thm.rhs_of cpth
val th = implies_intr p' (equal_elim (symmetric cpth) (assume p'))
--- a/src/HOL/Tools/res_atp_methods.ML Thu Sep 18 14:06:58 2008 +0200
+++ b/src/HOL/Tools/res_atp_methods.ML Thu Sep 18 19:39:44 2008 +0200
@@ -27,7 +27,7 @@
Meson.skolemize_tac,
METAHYPS (fn negs =>
HEADGOAL (Tactic.rtac
- (res_atp_oracle (ProofContext.theory_of ctxt)
+ (res_atp_oracle
(ResAtp.write_subgoal_file dfg mode ctxt negs user_thms i, timeLimit))))] i st) handle Fail _ => Seq.empty;
--- a/src/HOL/Tools/res_atp_provers.ML Thu Sep 18 14:06:58 2008 +0200
+++ b/src/HOL/Tools/res_atp_provers.ML Thu Sep 18 19:39:44 2008 +0200
@@ -40,19 +40,19 @@
in seek_line "SPASS beiseite: Proof found.\n" instr
end;
-fun vampire_o _ (file,time) =
+fun vampire_o (file,time) =
if call_vampire (file,time)
- then (warning file; ResAtp.cond_rm_tmp file; HOLogic.mk_Trueprop HOLogic.false_const)
+ then (warning file; ResAtp.cond_rm_tmp file; @{cprop False})
else (ResAtp.cond_rm_tmp file; raise Fail ("vampire oracle failed"));
-fun eprover_o _ (file,time) =
+fun eprover_o (file,time) =
if call_eprover (file,time)
- then (warning file; ResAtp.cond_rm_tmp file; HOLogic.mk_Trueprop HOLogic.false_const)
+ then (warning file; ResAtp.cond_rm_tmp file; @{cprop False})
else (ResAtp.cond_rm_tmp file; raise Fail ("eprover oracle failed"));
-fun spass_o _ (file,time) =
+fun spass_o (file,time) =
if call_spass (file,time)
- then (warning file; ResAtp.cond_rm_tmp file; HOLogic.mk_Trueprop HOLogic.false_const)
+ then (warning file; ResAtp.cond_rm_tmp file; @{cprop False})
else (ResAtp.cond_rm_tmp file; raise Fail ("SPASS oracle failed"));
end;
--- a/src/HOL/ex/Reflected_Presburger.thy Thu Sep 18 14:06:58 2008 +0200
+++ b/src/HOL/ex/Reflected_Presburger.thy Thu Sep 18 19:39:44 2008 +0200
@@ -1920,7 +1920,7 @@
export_code pa in SML module_name GeneratedCooper file "~~/src/HOL/Tools/Qelim/raw_generated_cooper.ML"
*)
-oracle linzqe_oracle ("term") = {*
+oracle linzqe_oracle = {*
let
fun num_of_term vs (t as Free (xn, xT)) = (case AList.lookup (op =) vs t
@@ -2035,14 +2035,16 @@
| _ => if is_ty t orelse is_op t then acc else insert (op aconv) t acc
end;
-in fn thy => fn t =>
- let
+in fn ct =>
+ let
+ val thy = Thm.theory_of_cterm ct;
+ val t = Thm.term_of ct;
val fs = term_frees t;
val bs = term_bools [] t;
val vs = fs ~~ (0 upto (length fs - 1))
val ps = bs ~~ (0 upto (length bs - 1))
val t' = (term_of_fm ps vs o @{code pa} o fm_of_term ps vs) t;
- in (HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end
+ in (Thm.cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end
end;
*}
--- a/src/HOL/ex/SVC_Oracle.thy Thu Sep 18 14:06:58 2008 +0200
+++ b/src/HOL/ex/SVC_Oracle.thy Thu Sep 18 19:39:44 2008 +0200
@@ -19,8 +19,7 @@
hide const iff_keep iff_unfold
-oracle
- svc_oracle ("term") = Svc.oracle
+oracle svc_oracle = Svc.oracle
ML {*
(*
@@ -110,12 +109,13 @@
abstracted. Use via compose_tac, which performs no lifting but will
instantiate variables.*)
-fun svc_tac i st =
+val svc_tac = CSUBGOAL (fn (ct, i) =>
let
- val (abs_goal, _) = svc_abstract (Logic.get_goal (Thm.prop_of st) i)
- val th = svc_oracle (Thm.theory_of_thm st) abs_goal
- in compose_tac (false, th, 0) i st end
- handle TERM _ => no_tac st;
+ val thy = Thm.theory_of_cterm ct;
+ val (abs_goal, _) = svc_abstract (Thm.term_of ct);
+ val th = svc_oracle (Thm.cterm_of thy abs_goal);
+ in compose_tac (false, th, 0) i end
+ handle TERM _ => no_tac);
*}
end
--- a/src/HOL/ex/coopertac.ML Thu Sep 18 14:06:58 2008 +0200
+++ b/src/HOL/ex/coopertac.ML Thu Sep 18 19:39:44 2008 +0200
@@ -104,7 +104,7 @@
(* The result of the quantifier elimination *)
val (th, tac) = case (prop_of pre_thm) of
Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
- let val pth = linzqe_oracle thy (Pattern.eta_long [] t1)
+ let val pth = linzqe_oracle (cterm_of thy (Pattern.eta_long [] t1))
in
((pth RS iffD2) RS pre_thm,
assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))
--- a/src/HOL/ex/svc_funcs.ML Thu Sep 18 14:06:58 2008 +0200
+++ b/src/HOL/ex/svc_funcs.ML Thu Sep 18 19:39:44 2008 +0200
@@ -237,10 +237,14 @@
end;
- (*The oracle proves the given formula t, if possible*)
- fun oracle thy t =
- (if ! trace then tracing ("SVC oracle: problem is\n" ^ Syntax.string_of_term_global thy t)
- else ();
- if valid (expr_of false t) then t else fail t);
+ (*The oracle proves the given formula, if possible*)
+ fun oracle ct =
+ let
+ val thy = Thm.theory_of_cterm ct;
+ val t = Thm.term_of ct;
+ val _ =
+ if ! trace then tracing ("SVC oracle: problem is\n" ^ Syntax.string_of_term_global thy t)
+ else ();
+ in if valid (expr_of false t) then ct else fail t end;
end;
--- a/src/HOLCF/IOA/Modelcheck/MuIOA.thy Thu Sep 18 14:06:58 2008 +0200
+++ b/src/HOLCF/IOA/Modelcheck/MuIOA.thy Thu Sep 18 19:39:44 2008 +0200
@@ -178,8 +178,12 @@
in
-fun mk_sim_oracle sign (subgoal, thl) = (
+fun mk_sim_oracle (csubgoal, thl) =
let
+ val sign = Thm.theory_of_cterm csubgoal;
+ val subgoal = Thm.term_of csubgoal;
+ in
+ (let
val weak_case_congs = (map (#weak_case_cong o snd) o Symtab.dest o DatatypePackage.get_datatypes) sign;
val concl = Logic.strip_imp_concl subgoal;
val ic_str = delete_ul_string(Syntax.string_of_term_global sign (IntC sign concl));
@@ -287,11 +291,12 @@
by (atac 1);
result();
OldGoals.pop_proof();
-Logic.strip_imp_concl subgoal
+Thm.cterm_of sign (Logic.strip_imp_concl subgoal)
)
end)
handle malformed =>
-error("No suitable match to IOA types in " ^ (Syntax.string_of_term_global sign subgoal));
+error("No suitable match to IOA types in " ^ (Syntax.string_of_term_global sign subgoal))
+end;
end
--- a/src/HOLCF/IOA/Modelcheck/MuIOAOracle.thy Thu Sep 18 14:06:58 2008 +0200
+++ b/src/HOLCF/IOA/Modelcheck/MuIOAOracle.thy Thu Sep 18 19:39:44 2008 +0200
@@ -5,16 +5,13 @@
imports MuIOA
begin
-oracle sim_oracle ("term * thm list") =
- mk_sim_oracle
+oracle sim_oracle = mk_sim_oracle
ML {*
(* call_sim_tac invokes oracle "Sim" *)
-fun call_sim_tac thm_list i state =
-let val thy = Thm.theory_of_thm state;
- val (subgoal::_) = Library.drop(i-1,prems_of state);
- val OraAss = sim_oracle thy (subgoal,thm_list);
-in cut_facts_tac [OraAss] i state end;
+fun call_sim_tac thm_list = CSUBGOAL (fn (csubgoal, i) =>
+let val OraAss = sim_oracle (csubgoal,thm_list);
+in cut_facts_tac [OraAss] i end);
val ioa_implements_def = thm "ioa_implements_def";
--- a/src/Pure/Isar/isar_cmd.ML Thu Sep 18 14:06:58 2008 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Thu Sep 18 19:39:44 2008 +0200
@@ -13,8 +13,7 @@
val print_translation: bool * (string * Position.T) -> theory -> theory
val typed_print_translation: bool * (string * Position.T) -> theory -> theory
val print_ast_translation: bool * (string * Position.T) -> theory -> theory
- val oracle: bstring -> SymbolPos.text * Position.T -> SymbolPos.text * Position.T ->
- theory -> theory
+ val oracle: bstring -> SymbolPos.text * Position.T -> theory -> theory
val add_axioms: ((Name.binding * string) * Attrib.src list) list -> theory -> theory
val add_defs: (bool * bool) * ((Name.binding * string) * Attrib.src list) list -> theory -> theory
val declaration: string * Position.T -> local_theory -> local_theory
@@ -152,22 +151,15 @@
(* oracles *)
-fun oracle name typ_pos (oracle_txt, pos) =
+fun oracle name (oracle_txt, pos) =
let
- val typ = SymbolPos.content (SymbolPos.explode typ_pos);
val oracle = SymbolPos.content (SymbolPos.explode (oracle_txt, pos));
val txt =
- "local\
- \ type T = " ^ typ ^ ";\
- \ val oracle: theory -> T -> term = " ^ oracle ^ ";\n\
+ "local\n\
\ val name = " ^ quote name ^ ";\n\
- \ exception Arg of T;\n\
- \ val _ = Context.>> (Context.map_theory\n\
- \ (Theory.add_oracle (name, fn (thy, Arg x) => oracle thy x)));\n\
- \ val thy = ML_Context.the_global_context ();\n\
- \ val invoke_" ^ name ^ " = Thm.invoke_oracle_i thy (Sign.full_name thy name);\n\
+ \ val oracle = " ^ oracle ^ ";\n\
\in\n\
- \ fun " ^ name ^ " thy x = invoke_" ^ name ^ " (thy, Arg x);\n\
+ \ val " ^ name ^ " = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (name, oracle))));\n\
\end;\n";
in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval false pos txt)) end;
--- a/src/Pure/Isar/isar_syn.ML Thu Sep 18 14:06:58 2008 +0200
+++ b/src/Pure/Isar/isar_syn.ML Thu Sep 18 19:39:44 2008 +0200
@@ -371,8 +371,7 @@
val _ =
OuterSyntax.command "oracle" "declare oracle" (K.tag_ml K.thy_decl)
- (P.name -- (P.$$$ "(" |-- P.ML_source --| P.$$$ ")" --| P.$$$ "=")
- -- P.ML_source >> (fn ((x, y), z) => Toplevel.theory (IsarCmd.oracle x y z)));
+ (P.name -- (P.$$$ "=" |-- P.ML_source) >> (fn (x, y) => Toplevel.theory (IsarCmd.oracle x y)));
(* local theories *)
--- a/src/Pure/Isar/skip_proof.ML Thu Sep 18 14:06:58 2008 +0200
+++ b/src/Pure/Isar/skip_proof.ML Thu Sep 18 19:39:44 2008 +0200
@@ -20,20 +20,15 @@
(* oracle setup *)
-exception SkipProof of term;
-
-fun skip_proof (_, SkipProof prop) =
- if ! quick_and_dirty then prop
- else error "Proof may be skipped in quick_and_dirty mode only!";
-
-val _ = Context.>> (Context.map_theory
- (Theory.add_oracle ("skip_proof", skip_proof)));
+val (_, skip_proof) = Context.>>> (Context.map_theory_result
+ (Thm.add_oracle ("skip_proof", fn (thy, prop) =>
+ if ! quick_and_dirty then Thm.cterm_of thy prop
+ else error "Proof may be skipped in quick_and_dirty mode only!")));
(* basic cheating *)
-fun make_thm thy prop =
- Thm.invoke_oracle_i thy "Pure.skip_proof" (thy, SkipProof prop);
+fun make_thm thy prop = skip_proof (thy, prop);
fun cheat_tac thy st =
ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
--- a/src/Pure/display.ML Thu Sep 18 14:06:58 2008 +0200
+++ b/src/Pure/display.ML Thu Sep 18 19:39:44 2008 +0200
@@ -178,7 +178,6 @@
Pretty.block ([prt_const' const, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]);
val axioms = (Theory.axiom_space thy, Theory.axiom_table thy);
- val oracles = (Theory.oracle_space thy, Theory.oracle_table thy);
val defs = Theory.defs_of thy;
val {restricts, reducts} = Defs.dest defs;
val {naming, syn = _, tsig, consts} = Sign.rep_sg thy;
@@ -202,7 +201,6 @@
val cnstrs = NameSpace.extern_table constraints;
val axms = NameSpace.extern_table axioms;
- val oras = NameSpace.extern_table oracles;
val (reds0, (reds1, reds2)) = filter_out (prune_const o fst o fst) reducts
|> map (fn (lhs, rhs) =>
@@ -223,7 +221,7 @@
Pretty.big_list "abbreviations:" (map pretty_abbrev abbrevs),
Pretty.big_list "constraints:" (map (Pretty.block o prt_const) cnstrs),
Pretty.big_list "axioms:" (map pretty_axm axms),
- Pretty.strs ("oracles:" :: (map #1 oras)),
+ Pretty.strs ("oracles:" :: Thm.extern_oracles thy),
Pretty.big_list "definitions:"
[pretty_finals reds0,
Pretty.big_list "non-overloaded:" (map pretty_reduct reds1),
--- a/src/Pure/theory.ML Thu Sep 18 14:06:58 2008 +0200
+++ b/src/Pure/theory.ML Thu Sep 18 19:39:44 2008 +0200
@@ -2,7 +2,7 @@
ID: $Id$
Author: Lawrence C Paulson and Markus Wenzel
-Logical theory content: axioms, definitions, oracles.
+Logical theory content: axioms, definitions, and begin/end wrappers.
*)
signature THEORY =
@@ -22,8 +22,6 @@
val requires: theory -> string -> string -> unit
val axiom_space: theory -> NameSpace.T
val axiom_table: theory -> term Symtab.table
- val oracle_space: theory -> NameSpace.T
- val oracle_table: theory -> ((theory * Object.T -> term) * stamp) Symtab.table
val axioms_of: theory -> (string * term) list
val all_axioms_of: theory -> (string * term) list
val defs_of: theory -> Defs.T
@@ -39,7 +37,6 @@
val add_finals: bool -> string list -> theory -> theory
val add_finals_i: bool -> term list -> theory -> theory
val specify_const: Properties.T -> (Name.binding * typ) * mixfix -> theory -> term * theory
- val add_oracle: bstring * (theory * Object.T -> term) -> theory -> theory
end
structure Theory: THEORY =
@@ -86,55 +83,41 @@
datatype thy = Thy of
{axioms: term NameSpace.table,
defs: Defs.T,
- oracles: ((theory * Object.T -> term) * stamp) NameSpace.table,
wrappers: wrapper list * wrapper list};
-fun make_thy (axioms, defs, oracles, wrappers) =
- Thy {axioms = axioms, defs = defs, oracles = oracles, wrappers = wrappers};
+fun make_thy (axioms, defs, wrappers) = Thy {axioms = axioms, defs = defs, wrappers = wrappers};
fun err_dup_axm dup = error ("Duplicate axiom: " ^ quote dup);
-fun err_dup_ora dup = error ("Duplicate oracle: " ^ quote dup);
structure ThyData = TheoryDataFun
(
type T = thy;
- val empty = make_thy (NameSpace.empty_table, Defs.empty, NameSpace.empty_table, ([], []));
+ val empty = make_thy (NameSpace.empty_table, Defs.empty, ([], []));
val copy = I;
- fun extend (Thy {axioms, defs, oracles, wrappers}) =
- make_thy (NameSpace.empty_table, defs, oracles, wrappers);
+ fun extend (Thy {axioms, defs, wrappers}) = make_thy (NameSpace.empty_table, defs, wrappers);
fun merge pp (thy1, thy2) =
let
- val Thy {axioms = _, defs = defs1, oracles = oracles1, wrappers = (bgs1, ens1)} = thy1;
- val Thy {axioms = _, defs = defs2, oracles = oracles2, wrappers = (bgs2, ens2)} = thy2;
+ val Thy {axioms = _, defs = defs1, wrappers = (bgs1, ens1)} = thy1;
+ val Thy {axioms = _, defs = defs2, wrappers = (bgs2, ens2)} = thy2;
val axioms' = NameSpace.empty_table;
val defs' = Defs.merge pp (defs1, defs2);
- val oracles' = NameSpace.merge_tables (eq_snd (op =)) (oracles1, oracles2)
- handle Symtab.DUP dup => err_dup_ora dup;
val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2);
val ens' = Library.merge (eq_snd op =) (ens1, ens2);
- in make_thy (axioms', defs', oracles', (bgs', ens')) end;
+ in make_thy (axioms', defs', (bgs', ens')) end;
);
fun rep_theory thy = ThyData.get thy |> (fn Thy args => args);
-fun map_thy f = ThyData.map (fn (Thy {axioms, defs, oracles, wrappers}) =>
- make_thy (f (axioms, defs, oracles, wrappers)));
+fun map_thy f = ThyData.map (fn (Thy {axioms, defs, wrappers}) =>
+ make_thy (f (axioms, defs, wrappers)));
-fun map_axioms f = map_thy
- (fn (axioms, defs, oracles, wrappers) => (f axioms, defs, oracles, wrappers));
-
-fun map_defs f = map_thy
- (fn (axioms, defs, oracles, wrappers) => (axioms, f defs, oracles, wrappers));
-
-fun map_oracles f = map_thy
- (fn (axioms, defs, oracles, wrappers) => (axioms, defs, f oracles, wrappers));
-
-fun map_wrappers f = map_thy
- (fn (axioms, defs, oracles, wrappers) => (axioms, defs, oracles, f wrappers));
+fun map_axioms f = map_thy (fn (axioms, defs, wrappers) => (f axioms, defs, wrappers));
+fun map_defs f = map_thy (fn (axioms, defs, wrappers) => (axioms, f defs, wrappers));
+fun map_wrappers f = map_thy (fn (axioms, defs, wrappers) => (axioms, defs, f wrappers));
(* basic operations *)
@@ -142,9 +125,6 @@
val axiom_space = #1 o #axioms o rep_theory;
val axiom_table = #2 o #axioms o rep_theory;
-val oracle_space = #1 o #oracles o rep_theory;
-val oracle_table = #2 o #oracles o rep_theory;
-
val axioms_of = Symtab.dest o #2 o #axioms o rep_theory;
fun all_axioms_of thy = maps axioms_of (thy :: ancestors_of thy);
@@ -323,13 +303,4 @@
end;
-
-
-(** add oracle **)
-
-fun add_oracle (bname, oracle) thy = thy |> map_oracles (fn oracles =>
- NameSpace.extend_table (Sign.naming_of thy) [(bname, (oracle, stamp ()))] oracles
- handle Symtab.DUP dup => err_dup_ora dup);
-
end;
-
--- a/src/Pure/thm.ML Thu Sep 18 14:06:58 2008 +0200
+++ b/src/Pure/thm.ML Thu Sep 18 19:39:44 2008 +0200
@@ -112,8 +112,8 @@
val compose_no_flatten: bool -> thm * int -> int -> thm -> thm Seq.seq
val bicompose: bool -> bool * thm * int -> int -> thm -> thm Seq.seq
val biresolution: bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
- val invoke_oracle: theory -> xstring -> theory * Object.T -> thm
- val invoke_oracle_i: theory -> string -> theory * Object.T -> thm
+ val extern_oracles: theory -> xstring list
+ val add_oracle: bstring * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
end;
signature THM =
@@ -1557,36 +1557,53 @@
(*** Oracles ***)
-fun invoke_oracle_i thy1 name =
- let
- val oracle =
- (case Symtab.lookup (Theory.oracle_table thy1) name of
- NONE => raise THM ("Unknown oracle: " ^ name, 0, [])
- | SOME (f, _) => f);
- val thy_ref1 = Theory.check_thy thy1;
- in
- fn (thy2, data) =>
- let
- val thy' = Theory.merge (Theory.deref thy_ref1, thy2);
- val (prop, T, maxidx) = Sign.certify_term thy' (oracle (thy', data));
- val shyps' = Sorts.insert_term prop [];
- val der = Deriv.oracle name prop;
- in
- if T <> propT then
- raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
- else
- Thm {thy_ref = Theory.check_thy thy', der = der, tags = [],
- maxidx = maxidx, shyps = shyps', hyps = [], tpairs = [], prop = prop}
- end
+(* oracle rule *)
+
+fun invoke_oracle thy_ref1 name oracle arg =
+ let val {thy_ref = thy_ref2, t = prop, T, maxidx, sorts} = rep_cterm (oracle arg) in
+ if T <> propT then
+ raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
+ else
+ Thm {thy_ref = Theory.merge_refs (thy_ref1, thy_ref2),
+ der = Deriv.oracle name prop,
+ tags = [],
+ maxidx = maxidx,
+ shyps = sorts,
+ hyps = [],
+ tpairs = [],
+ prop = prop}
end;
-fun invoke_oracle thy =
- invoke_oracle_i thy o NameSpace.intern (Theory.oracle_space thy);
-
-
end;
end;
end;
+
+
+(* authentic derivation names *)
+
+fun err_dup_ora dup = error ("Duplicate oracle: " ^ quote dup);
+
+structure Oracles = TheoryDataFun
+(
+ type T = stamp NameSpace.table;
+ val empty = NameSpace.empty_table;
+ val copy = I;
+ val extend = I;
+ fun merge _ oracles = NameSpace.merge_tables (op =) oracles
+ handle Symtab.DUP dup => err_dup_ora dup;
+);
+
+val extern_oracles = map #1 o NameSpace.extern_table o Oracles.get;
+
+fun add_oracle (bname, oracle) thy =
+ let
+ val naming = Sign.naming_of thy;
+ val name = NameSpace.full naming bname;
+ val thy' = thy |> Oracles.map (fn (space, tab) =>
+ (NameSpace.declare naming name space,
+ Symtab.update_new (name, stamp ()) tab handle Symtab.DUP dup => err_dup_ora dup));
+ in ((name, invoke_oracle (Theory.check_thy thy') name oracle), thy') end;
+
end;
structure BasicThm: BASIC_THM = Thm;
--- a/src/Tools/Compute_Oracle/Compute_Oracle.thy Thu Sep 18 14:06:58 2008 +0200
+++ b/src/Tools/Compute_Oracle/Compute_Oracle.thy Thu Sep 18 19:39:44 2008 +0200
@@ -9,6 +9,4 @@
uses "am.ML" "am_compiler.ML" "am_interpreter.ML" "am_ghc.ML" "am_sml.ML" "report.ML" "compute.ML" "linker.ML"
begin
-setup {* Compute.setup_compute *}
-
end
\ No newline at end of file
--- a/src/Tools/Compute_Oracle/compute.ML Thu Sep 18 14:06:58 2008 +0200
+++ b/src/Tools/Compute_Oracle/compute.ML Thu Sep 18 19:39:44 2008 +0200
@@ -35,8 +35,6 @@
(* ! *) val evaluate_prem : computer -> int -> theorem -> theorem
(* ! *) val modus_ponens : computer -> int -> thm -> theorem -> theorem
- val setup_compute : theory -> theory
-
end
structure Compute :> COMPUTE = struct
@@ -362,8 +360,6 @@
(* An oracle for exporting theorems; must only be accessible from inside this structure! *)
(* ------------------------------------------------------------------------------------- *)
-exception ExportThm of term list * sort list * term
-
fun merge_hyps hyps1 hyps2 =
let
fun add hyps tab = fold (fn h => fn tab => Termtab.update (h, ()) tab) hyps tab
@@ -375,7 +371,8 @@
fun merge_shyps shyps1 shyps2 = Sorttab.keys (add_shyps shyps2 (add_shyps shyps1 Sorttab.empty))
-fun export_oracle (thy, ExportThm (hyps, shyps, prop)) =
+val (_, export_oracle) = Context.>>> (Context.map_theory_result
+ (Thm.add_oracle ("compute", fn (thy, hyps, shyps, prop) =>
let
val shyptab = add_shyps shyps Sorttab.empty
fun delete s shyptab = Sorttab.delete s shyptab handle Sorttab.UNDEF _ => shyptab
@@ -385,15 +382,12 @@
val shyps = if Sorttab.is_empty shyptab then [] else Sorttab.keys (fold delete_term (prop::hyps) shyptab)
val _ = if not (null shyps) then raise Compute ("dangling sort hypotheses: "^(makestring shyps)) else ()
in
- fold_rev (fn hyp => fn p => Logic.mk_implies (hyp, p)) hyps prop
- end
- | export_oracle _ = raise Match
-
-val setup_compute = (fn thy => Theory.add_oracle ("compute", export_oracle) thy)
+ Thm.cterm_of thy (fold_rev (fn hyp => fn p => Logic.mk_implies (hyp, p)) hyps prop)
+ end)));
fun export_thm thy hyps shyps prop =
let
- val th = invoke_oracle_i thy "Compute_Oracle.compute" (thy, ExportThm (hyps, shyps, prop))
+ val th = export_oracle (thy, hyps, shyps, prop)
val hyps = map (fn h => assume (cterm_of thy h)) hyps
in
fold (fn h => fn p => implies_elim p h) hyps th
--- a/src/Tools/nbe.ML Thu Sep 18 14:06:58 2008 +0200
+++ b/src/Tools/nbe.ML Thu Sep 18 19:39:44 2008 +0200
@@ -403,15 +403,9 @@
(* evaluation oracle *)
-exception Norm of term * Code_Thingol.program
- * (Code_Thingol.typscheme * Code_Thingol.iterm) * string list;
-
-fun norm_oracle (thy, Norm (t, program, vs_ty_t, deps)) =
- Logic.mk_equals (t, eval thy t program vs_ty_t deps);
-
-fun norm_invoke thy t program vs_ty_t deps =
- Thm.invoke_oracle_i thy "HOL.norm" (thy, Norm (t, program, vs_ty_t, deps));
- (*FIXME get rid of hardwired theory name*)
+val (_, norm_oracle) = Context.>>> (Context.map_theory_result
+ (Thm.add_oracle ("norm", fn (thy, t, program, vs_ty_t, deps) =>
+ Thm.cterm_of thy (Logic.mk_equals (t, eval thy t program vs_ty_t deps)))));
fun add_triv_classes thy =
let
@@ -425,7 +419,7 @@
fun norm_conv ct =
let
val thy = Thm.theory_of_cterm ct;
- fun evaluator' t program vs_ty_t deps = norm_invoke thy t program vs_ty_t deps;
+ fun evaluator' t program vs_ty_t deps = norm_oracle (thy, t, program, vs_ty_t, deps);
fun evaluator t = (add_triv_classes thy t, evaluator' t);
in Code_Thingol.eval_conv thy evaluator ct end;
@@ -455,8 +449,8 @@
let val ctxt = Toplevel.context_of state
in norm_print_term ctxt modes (Syntax.read_term ctxt s) end;
-val setup = Theory.add_oracle ("norm", norm_oracle)
- #> Value.add_evaluator ("nbe", norm_term o ProofContext.theory_of);
+val setup =
+ Value.add_evaluator ("nbe", norm_term o ProofContext.theory_of);
local structure P = OuterParse and K = OuterKeyword in