# HG changeset patch
# User haftmann
# Date 1163606737 -3600
# Node ID cedfce6fc725a267db41a5ca7321d042b77d9808
# Parent  c29146dc14f10f9ddec4545f58a56b5127c7e868
added evaluation oracle

diff -r c29146dc14f1 -r cedfce6fc725 src/HOL/Code_Generator.thy
--- a/src/HOL/Code_Generator.thy	Wed Nov 15 16:23:55 2006 +0100
+++ b/src/HOL/Code_Generator.thy	Wed Nov 15 17:05:37 2006 +0100
@@ -110,7 +110,55 @@
 code_reserved Haskell error
 
 
-subsection {* normalization by evaluation *}
+subsection {* Evaluation oracle *}
+
+ML {*
+signature HOL_EVAL =
+sig
+  val eval_ref: bool option ref
+  val oracle: string * (theory * exn -> term)
+  val tac: int -> tactic
+  val method: Method.src -> Proof.context -> Method.method
+end;
+
+structure HOLEval : HOL_EVAL =
+struct
+
+val eval_ref : bool option ref = ref NONE;
+
+fun eval_prop thy t =
+  CodegenPackage.eval_term
+    thy (("HOLEval.eval_ref", eval_ref), t);
+
+exception Eval of term;
+
+val oracle = ("Eval", fn (thy, Eval t) =>
+  Logic.mk_equals (t, if eval_prop thy t then HOLogic.true_const else HOLogic.false_const));
+
+val oracle_name = NameSpace.pack [Context.theory_name (the_context ()), fst oracle];
+
+fun conv ct =
+  let
+    val {thy, t, ...} = rep_cterm ct;
+  in Thm.invoke_oracle_i thy oracle_name (thy, Eval t) end;
+
+fun tac i = Tactical.PRIMITIVE (Drule.fconv_rule
+  (Drule.goals_conv (equal i) (HOL.Trueprop_conv conv)));
+
+val method =
+  Method.no_args (Method.METHOD (fn _ =>
+    tac 1 THEN rtac TrueI 1));
+
+end;
+*}
+
+setup {*
+  Theory.add_oracle HOLEval.oracle
+  #> Method.add_method ("eval", HOLEval.method, "solve goal by evaluation")
+*}
+
+
+subsection {* Normalization by evaluation *}
 
 setup {*
 let