delegate inclusion of required dictionaries to user-space instead of half-working magic

--- a/NEWS	Thu May 26 15:27:50 2016 +0200
+++ b/NEWS	Thu May 26 15:27:50 2016 +0200
@@ -101,6 +101,11 @@
 permutations of a set, i.e. the set of all lists that contain every 
 element of the carrier set exactly once.
 
+* Static evaluators (Code_Evaluation.static_* in Isabelle/ML) rely on
+explicitly provided auxiliary definitions for required type class
+dictionaries rather than half-working magic.  INCOMPATIBILITY, see
+the tutorial on code generation for details.
+
 * New abbreviations for negated existence (but not bounded existence):
 
   \<nexists>x. P x \<equiv> \<not> (\<exists>x. P x)

--- a/src/Doc/Codegen/Evaluation.thy	Thu May 26 15:27:50 2016 +0200
+++ b/src/Doc/Codegen/Evaluation.thy	Thu May 26 15:27:50 2016 +0200
@@ -143,7 +143,7 @@
     \item Evaluation of @{term t} terminates with a result @{term
       "t'"}.
 
-    \item Evaluation of @{term t} terminates which en exception
+    \item Evaluation of @{term t} terminates which an exception
       indicating a pattern match failure or a non-implemented
       function.  As sketched in \secref{sec:partiality}, this can be
       interpreted as partiality.
@@ -195,18 +195,36 @@
   \end{tabular}
 \<close>
 
+text \<open>
+  \noindent Note that @{ML Code_Evaluation.static_value} and
+  @{ML Code_Evaluation.static_conv} require certain code equations to
+  reconstruct Isabelle terms from results and certify results.  This is
+  achieved as follows:
+
+  \<^enum> Identify which result types are expected.
+
+  \<^enum> Define an auxiliary operation which for each possible result type @{text \<tau>}
+    contains a term @{const Code_Evaluation.TERM_OF} of type @{text "\<tau> itself"}
+    (for @{ML Code_Evaluation.static_value}) or
+    a term @{const Code_Evaluation.TERM_OF_EQUAL} of type @{text "\<tau> itself"}
+    (for @{ML Code_Evaluation.static_conv}) respectively.
+
+  \<^enum> Include that auxiliary operation into the set of constants when generating
+    the static conversion.
+\<close>
+
 
 subsection \<open>Preprocessing HOL terms into evaluable shape\<close>
 
 text \<open>
-  When integration decision procedures developed inside HOL into HOL itself,
+  When integrating decision procedures developed inside HOL into HOL itself,
   it is necessary to somehow get from the Isabelle/ML representation to
   the representation used by the decision procedure itself (``reification'').
   One option is to hardcode it using code antiquotations (see \secref{sec:code_antiq}).
   Another option is to use pre-existing infrastructure in HOL:
   @{ML "Reification.conv"} and @{ML "Reification.tac"}
 
-  An simplistic example:
+  A simplistic example:
 \<close>
 
 datatype %quote form_ord = T | F | Less nat nat

--- a/src/HOL/Code_Evaluation.thy	Thu May 26 15:27:50 2016 +0200
+++ b/src/HOL/Code_Evaluation.thy	Thu May 26 15:27:50 2016 +0200
@@ -68,6 +68,19 @@
 
 subsection \<open>Tools setup and evaluation\<close>
 
+context
+begin
+
+qualified definition TERM_OF :: "'a::term_of itself"
+where
+  "TERM_OF = snd (Code_Evaluation.term_of :: 'a \<Rightarrow> _, TYPE('a))"
+
+qualified definition TERM_OF_EQUAL :: "'a::term_of itself"
+where
+  "TERM_OF_EQUAL = snd (\<lambda>(a::'a). (Code_Evaluation.term_of a, HOL.eq a), TYPE('a))"
+
+end
+
 lemma eq_eq_TrueD:
   fixes x y :: "'a::{}"
   assumes "(x \<equiv> y) \<equiv> Trueprop True"

--- a/src/HOL/Tools/code_evaluation.ML	Thu May 26 15:27:50 2016 +0200
+++ b/src/HOL/Tools/code_evaluation.ML	Thu May 26 15:27:50 2016 +0200
@@ -9,14 +9,14 @@
   val dynamic_value: Proof.context -> term -> term option
   val dynamic_value_strict: Proof.context -> term -> term
   val dynamic_value_exn: Proof.context -> term -> term Exn.result
-  val static_value: { ctxt: Proof.context, consts: string list, Ts: typ list }
+  val static_value: { ctxt: Proof.context, consts: string list }
     -> Proof.context -> term -> term option
-  val static_value_strict: { ctxt: Proof.context, consts: string list, Ts: typ list }
+  val static_value_strict: { ctxt: Proof.context, consts: string list }
     -> Proof.context -> term -> term
-  val static_value_exn: { ctxt: Proof.context, consts: string list, Ts: typ list }
+  val static_value_exn: { ctxt: Proof.context, consts: string list }
     -> Proof.context -> term -> term Exn.result
   val dynamic_conv: Proof.context -> conv
-  val static_conv: { ctxt: Proof.context, consts: string list, Ts: typ list }
+  val static_conv: { ctxt: Proof.context, consts: string list }
     -> Proof.context -> conv
   val put_term: (unit -> term) -> Proof.context -> Proof.context
   val tracing: string -> 'a -> 'a
@@ -183,8 +183,6 @@
 
 fun mk_term_of t = HOLogic.mk_term_of (fastype_of t) t;
 
-fun term_of_const_for thy = Axclass.unoverload_const thy o dest_Const o HOLogic.term_of_const;
-
 fun gen_dynamic_value computation ctxt t =
   computation cookie ctxt NONE I (mk_term_of t) [];
 
@@ -192,11 +190,10 @@
 val dynamic_value_strict = gen_dynamic_value Code_Runtime.dynamic_value_strict;
 val dynamic_value_exn = gen_dynamic_value Code_Runtime.dynamic_value_exn;
 
-fun gen_static_value computation { ctxt, consts, Ts } =
+fun gen_static_value computation { ctxt, consts } =
   let
     val computation' = computation cookie
-      { ctxt = ctxt, target = NONE, lift_postproc = I, consts =
-        union (op =) (map (term_of_const_for (Proof_Context.theory_of ctxt)) Ts) consts }
+      { ctxt = ctxt, target = NONE, lift_postproc = I, consts = consts }
   in fn ctxt' => computation' ctxt' o mk_term_of end;
 
 val static_value = gen_static_value Code_Runtime.static_value;
@@ -219,13 +216,12 @@
 fun dynamic_conv ctxt = certify_eval ctxt dynamic_value
   Code_Runtime.dynamic_holds_conv;
 
-fun static_conv { ctxt, consts, Ts }  =
+fun static_conv { ctxt, consts }  =
   let
-    val eqs = @{const_name Pure.eq} :: @{const_name HOL.eq} ::
-      map (fn T => Axclass.unoverload_const (Proof_Context.theory_of ctxt)
-        (@{const_name HOL.equal}, T)) Ts; (*assumes particular code equations for Pure.eq etc.*)
-    val value = static_value { ctxt = ctxt, consts = consts, Ts = Ts };
-    val holds = Code_Runtime.static_holds_conv { ctxt = ctxt, consts = union (op =) eqs consts };
+    val value = static_value { ctxt = ctxt, consts = consts };
+    val holds = Code_Runtime.static_holds_conv { ctxt = ctxt,
+      consts = insert (op =) @{const_name Pure.eq} consts
+        (*assumes particular code equation for Pure.eq*) };
   in
     fn ctxt' => certify_eval ctxt' value holds
   end;