# HG changeset patch
# User haftmann
# Date 1285001003 -7200
# Node ID 5ee997fbe5cc746f2737ec2f887c563ecb3b04b2
# Parent  87a5704673f073c416d8ea3a17e3fcd0c34f93b4
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term

diff -r 87a5704673f0 -r 5ee997fbe5cc src/HOL/Code_Evaluation.thy
--- a/src/HOL/Code_Evaluation.thy	Mon Sep 20 18:43:18 2010 +0200
+++ b/src/HOL/Code_Evaluation.thy	Mon Sep 20 18:43:23 2010 +0200
@@ -62,6 +62,11 @@
 
 subsection {* Tools setup and evaluation *}
 
+lemma eq_eq_TrueD:
+  assumes "(x \<equiv> y) \<equiv> Trueprop True"
+  shows "x \<equiv> y"
+  using assms by simp
+
 use "Tools/code_evaluation.ML"
 
 code_reserved Eval Code_Evaluation
diff -r 87a5704673f0 -r 5ee997fbe5cc src/HOL/Tools/code_evaluation.ML
--- a/src/HOL/Tools/code_evaluation.ML	Mon Sep 20 18:43:18 2010 +0200
+++ b/src/HOL/Tools/code_evaluation.ML	Mon Sep 20 18:43:23 2010 +0200
@@ -12,6 +12,8 @@
   val static_value: theory -> string list -> typ list -> term -> term option
   val static_value_strict: theory -> string list -> typ list -> term -> term
   val static_value_exn: theory -> string list -> typ list -> term -> term Exn.result
+  val dynamic_eval_conv: conv
+  val static_eval_conv: theory -> string list -> typ list -> conv
   val put_term: (unit -> term) -> Proof.context -> Proof.context
   val tracing: string -> 'a -> 'a
   val setup: theory -> theory
@@ -180,6 +182,31 @@
 val static_value_strict = gen_static_value Code_Runtime.static_value_strict;
 val static_value_exn = gen_static_value Code_Runtime.static_value_exn;
 
+fun certify_eval thy value conv ct =
+  let
+    val t = Thm.term_of ct;
+    val T = fastype_of t;
+    val mk_eq = Thm.mk_binop (Thm.cterm_of thy (Const ("==", T --> T --> propT)));
+  in case value t
+   of NONE => Thm.reflexive ct
+    | SOME t' => conv (mk_eq ct (Thm.cterm_of thy t')) RS @{thm eq_eq_TrueD}
+        handle THM _ =>
+          error ("Failed to certify evaluation result of " ^ Syntax.string_of_term_global thy t)
+  end;
+
+val dynamic_eval_conv = Conv.tap_thy
+  (fn thy => certify_eval thy (dynamic_value thy) Code_Runtime.dynamic_holds_conv);
+
+fun static_eval_conv thy consts Ts =
+  let
+    val eqs = "==" :: @{const_name HOL.eq} ::
+      map (fn T => AxClass.unoverload_const thy (@{const_name HOL.equal}, T)) Ts;
+        (*assumes particular code equations for "==" etc.*)
+  in
+    certify_eval thy (static_value thy consts Ts)
+      (Code_Runtime.static_holds_conv thy (union (op =) eqs consts))
+  end;
+
 
 (** diagnostic **)