dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
authorhaftmann
Mon Sep 20 18:43:23 2010 +0200 (2010-09-20)
changeset 395675ee997fbe5cc
parent 39566 87a5704673f0
child 39568 839a0446630b
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
src/HOL/Code_Evaluation.thy
src/HOL/Tools/code_evaluation.ML
     1.1 --- a/src/HOL/Code_Evaluation.thy	Mon Sep 20 18:43:18 2010 +0200
     1.2 +++ b/src/HOL/Code_Evaluation.thy	Mon Sep 20 18:43:23 2010 +0200
     1.3 @@ -62,6 +62,11 @@
     1.4  
     1.5  subsection {* Tools setup and evaluation *}
     1.6  
     1.7 +lemma eq_eq_TrueD:
     1.8 +  assumes "(x \<equiv> y) \<equiv> Trueprop True"
     1.9 +  shows "x \<equiv> y"
    1.10 +  using assms by simp
    1.11 +
    1.12  use "Tools/code_evaluation.ML"
    1.13  
    1.14  code_reserved Eval Code_Evaluation
     2.1 --- a/src/HOL/Tools/code_evaluation.ML	Mon Sep 20 18:43:18 2010 +0200
     2.2 +++ b/src/HOL/Tools/code_evaluation.ML	Mon Sep 20 18:43:23 2010 +0200
     2.3 @@ -12,6 +12,8 @@
     2.4    val static_value: theory -> string list -> typ list -> term -> term option
     2.5    val static_value_strict: theory -> string list -> typ list -> term -> term
     2.6    val static_value_exn: theory -> string list -> typ list -> term -> term Exn.result
     2.7 +  val dynamic_eval_conv: conv
     2.8 +  val static_eval_conv: theory -> string list -> typ list -> conv
     2.9    val put_term: (unit -> term) -> Proof.context -> Proof.context
    2.10    val tracing: string -> 'a -> 'a
    2.11    val setup: theory -> theory
    2.12 @@ -180,6 +182,31 @@
    2.13  val static_value_strict = gen_static_value Code_Runtime.static_value_strict;
    2.14  val static_value_exn = gen_static_value Code_Runtime.static_value_exn;
    2.15  
    2.16 +fun certify_eval thy value conv ct =
    2.17 +  let
    2.18 +    val t = Thm.term_of ct;
    2.19 +    val T = fastype_of t;
    2.20 +    val mk_eq = Thm.mk_binop (Thm.cterm_of thy (Const ("==", T --> T --> propT)));
    2.21 +  in case value t
    2.22 +   of NONE => Thm.reflexive ct
    2.23 +    | SOME t' => conv (mk_eq ct (Thm.cterm_of thy t')) RS @{thm eq_eq_TrueD}
    2.24 +        handle THM _ =>
    2.25 +          error ("Failed to certify evaluation result of " ^ Syntax.string_of_term_global thy t)
    2.26 +  end;
    2.27 +
    2.28 +val dynamic_eval_conv = Conv.tap_thy
    2.29 +  (fn thy => certify_eval thy (dynamic_value thy) Code_Runtime.dynamic_holds_conv);
    2.30 +
    2.31 +fun static_eval_conv thy consts Ts =
    2.32 +  let
    2.33 +    val eqs = "==" :: @{const_name HOL.eq} ::
    2.34 +      map (fn T => AxClass.unoverload_const thy (@{const_name HOL.equal}, T)) Ts;
    2.35 +        (*assumes particular code equations for "==" etc.*)
    2.36 +  in
    2.37 +    certify_eval thy (static_value thy consts Ts)
    2.38 +      (Code_Runtime.static_holds_conv thy (union (op =) eqs consts))
    2.39 +  end;
    2.40 +
    2.41  
    2.42  (** diagnostic **)
    2.43