delegate inclusion of required dictionaries to user-space instead of half-working magic
authorhaftmann
Thu May 26 15:27:50 2016 +0200 (2016-05-26)
changeset 631612660ba498798
parent 63160 80a91e0e236e
child 63162 93e75d2f0d01
delegate inclusion of required dictionaries to user-space instead of half-working magic
NEWS
src/Doc/Codegen/Evaluation.thy
src/HOL/Code_Evaluation.thy
src/HOL/Tools/code_evaluation.ML
     1.1 --- a/NEWS	Thu May 26 15:27:50 2016 +0200
     1.2 +++ b/NEWS	Thu May 26 15:27:50 2016 +0200
     1.3 @@ -101,6 +101,11 @@
     1.4  permutations of a set, i.e. the set of all lists that contain every 
     1.5  element of the carrier set exactly once.
     1.6  
     1.7 +* Static evaluators (Code_Evaluation.static_* in Isabelle/ML) rely on
     1.8 +explicitly provided auxiliary definitions for required type class
     1.9 +dictionaries rather than half-working magic.  INCOMPATIBILITY, see
    1.10 +the tutorial on code generation for details.
    1.11 +
    1.12  * New abbreviations for negated existence (but not bounded existence):
    1.13  
    1.14    \<nexists>x. P x \<equiv> \<not> (\<exists>x. P x)
     2.1 --- a/src/Doc/Codegen/Evaluation.thy	Thu May 26 15:27:50 2016 +0200
     2.2 +++ b/src/Doc/Codegen/Evaluation.thy	Thu May 26 15:27:50 2016 +0200
     2.3 @@ -143,7 +143,7 @@
     2.4      \item Evaluation of @{term t} terminates with a result @{term
     2.5        "t'"}.
     2.6  
     2.7 -    \item Evaluation of @{term t} terminates which en exception
     2.8 +    \item Evaluation of @{term t} terminates which an exception
     2.9        indicating a pattern match failure or a non-implemented
    2.10        function.  As sketched in \secref{sec:partiality}, this can be
    2.11        interpreted as partiality.
    2.12 @@ -195,18 +195,36 @@
    2.13    \end{tabular}
    2.14  \<close>
    2.15  
    2.16 +text \<open>
    2.17 +  \noindent Note that @{ML Code_Evaluation.static_value} and
    2.18 +  @{ML Code_Evaluation.static_conv} require certain code equations to
    2.19 +  reconstruct Isabelle terms from results and certify results.  This is
    2.20 +  achieved as follows:
    2.21 +
    2.22 +  \<^enum> Identify which result types are expected.
    2.23 +
    2.24 +  \<^enum> Define an auxiliary operation which for each possible result type @{text \<tau>}
    2.25 +    contains a term @{const Code_Evaluation.TERM_OF} of type @{text "\<tau> itself"}
    2.26 +    (for @{ML Code_Evaluation.static_value}) or
    2.27 +    a term @{const Code_Evaluation.TERM_OF_EQUAL} of type @{text "\<tau> itself"}
    2.28 +    (for @{ML Code_Evaluation.static_conv}) respectively.
    2.29 +
    2.30 +  \<^enum> Include that auxiliary operation into the set of constants when generating
    2.31 +    the static conversion.
    2.32 +\<close>
    2.33 +
    2.34  
    2.35  subsection \<open>Preprocessing HOL terms into evaluable shape\<close>
    2.36  
    2.37  text \<open>
    2.38 -  When integration decision procedures developed inside HOL into HOL itself,
    2.39 +  When integrating decision procedures developed inside HOL into HOL itself,
    2.40    it is necessary to somehow get from the Isabelle/ML representation to
    2.41    the representation used by the decision procedure itself (``reification'').
    2.42    One option is to hardcode it using code antiquotations (see \secref{sec:code_antiq}).
    2.43    Another option is to use pre-existing infrastructure in HOL:
    2.44    @{ML "Reification.conv"} and @{ML "Reification.tac"}
    2.45  
    2.46 -  An simplistic example:
    2.47 +  A simplistic example:
    2.48  \<close>
    2.49  
    2.50  datatype %quote form_ord = T | F | Less nat nat
     3.1 --- a/src/HOL/Code_Evaluation.thy	Thu May 26 15:27:50 2016 +0200
     3.2 +++ b/src/HOL/Code_Evaluation.thy	Thu May 26 15:27:50 2016 +0200
     3.3 @@ -68,6 +68,19 @@
     3.4  
     3.5  subsection \<open>Tools setup and evaluation\<close>
     3.6  
     3.7 +context
     3.8 +begin
     3.9 +
    3.10 +qualified definition TERM_OF :: "'a::term_of itself"
    3.11 +where
    3.12 +  "TERM_OF = snd (Code_Evaluation.term_of :: 'a \<Rightarrow> _, TYPE('a))"
    3.13 +
    3.14 +qualified definition TERM_OF_EQUAL :: "'a::term_of itself"
    3.15 +where
    3.16 +  "TERM_OF_EQUAL = snd (\<lambda>(a::'a). (Code_Evaluation.term_of a, HOL.eq a), TYPE('a))"
    3.17 +
    3.18 +end
    3.19 +
    3.20  lemma eq_eq_TrueD:
    3.21    fixes x y :: "'a::{}"
    3.22    assumes "(x \<equiv> y) \<equiv> Trueprop True"
     4.1 --- a/src/HOL/Tools/code_evaluation.ML	Thu May 26 15:27:50 2016 +0200
     4.2 +++ b/src/HOL/Tools/code_evaluation.ML	Thu May 26 15:27:50 2016 +0200
     4.3 @@ -9,14 +9,14 @@
     4.4    val dynamic_value: Proof.context -> term -> term option
     4.5    val dynamic_value_strict: Proof.context -> term -> term
     4.6    val dynamic_value_exn: Proof.context -> term -> term Exn.result
     4.7 -  val static_value: { ctxt: Proof.context, consts: string list, Ts: typ list }
     4.8 +  val static_value: { ctxt: Proof.context, consts: string list }
     4.9      -> Proof.context -> term -> term option
    4.10 -  val static_value_strict: { ctxt: Proof.context, consts: string list, Ts: typ list }
    4.11 +  val static_value_strict: { ctxt: Proof.context, consts: string list }
    4.12      -> Proof.context -> term -> term
    4.13 -  val static_value_exn: { ctxt: Proof.context, consts: string list, Ts: typ list }
    4.14 +  val static_value_exn: { ctxt: Proof.context, consts: string list }
    4.15      -> Proof.context -> term -> term Exn.result
    4.16    val dynamic_conv: Proof.context -> conv
    4.17 -  val static_conv: { ctxt: Proof.context, consts: string list, Ts: typ list }
    4.18 +  val static_conv: { ctxt: Proof.context, consts: string list }
    4.19      -> Proof.context -> conv
    4.20    val put_term: (unit -> term) -> Proof.context -> Proof.context
    4.21    val tracing: string -> 'a -> 'a
    4.22 @@ -183,8 +183,6 @@
    4.23  
    4.24  fun mk_term_of t = HOLogic.mk_term_of (fastype_of t) t;
    4.25  
    4.26 -fun term_of_const_for thy = Axclass.unoverload_const thy o dest_Const o HOLogic.term_of_const;
    4.27 -
    4.28  fun gen_dynamic_value computation ctxt t =
    4.29    computation cookie ctxt NONE I (mk_term_of t) [];
    4.30  
    4.31 @@ -192,11 +190,10 @@
    4.32  val dynamic_value_strict = gen_dynamic_value Code_Runtime.dynamic_value_strict;
    4.33  val dynamic_value_exn = gen_dynamic_value Code_Runtime.dynamic_value_exn;
    4.34  
    4.35 -fun gen_static_value computation { ctxt, consts, Ts } =
    4.36 +fun gen_static_value computation { ctxt, consts } =
    4.37    let
    4.38      val computation' = computation cookie
    4.39 -      { ctxt = ctxt, target = NONE, lift_postproc = I, consts =
    4.40 -        union (op =) (map (term_of_const_for (Proof_Context.theory_of ctxt)) Ts) consts }
    4.41 +      { ctxt = ctxt, target = NONE, lift_postproc = I, consts = consts }
    4.42    in fn ctxt' => computation' ctxt' o mk_term_of end;
    4.43  
    4.44  val static_value = gen_static_value Code_Runtime.static_value;
    4.45 @@ -219,13 +216,12 @@
    4.46  fun dynamic_conv ctxt = certify_eval ctxt dynamic_value
    4.47    Code_Runtime.dynamic_holds_conv;
    4.48  
    4.49 -fun static_conv { ctxt, consts, Ts }  =
    4.50 +fun static_conv { ctxt, consts }  =
    4.51    let
    4.52 -    val eqs = @{const_name Pure.eq} :: @{const_name HOL.eq} ::
    4.53 -      map (fn T => Axclass.unoverload_const (Proof_Context.theory_of ctxt)
    4.54 -        (@{const_name HOL.equal}, T)) Ts; (*assumes particular code equations for Pure.eq etc.*)
    4.55 -    val value = static_value { ctxt = ctxt, consts = consts, Ts = Ts };
    4.56 -    val holds = Code_Runtime.static_holds_conv { ctxt = ctxt, consts = union (op =) eqs consts };
    4.57 +    val value = static_value { ctxt = ctxt, consts = consts };
    4.58 +    val holds = Code_Runtime.static_holds_conv { ctxt = ctxt,
    4.59 +      consts = insert (op =) @{const_name Pure.eq} consts
    4.60 +        (*assumes particular code equation for Pure.eq*) };
    4.61    in
    4.62      fn ctxt' => certify_eval ctxt' value holds
    4.63    end;