# HG changeset patch
# User nipkow
# Date 1284732945 -7200
# Node ID c3d0414ba6df7adb281ff549134bf59be5486126
# Parent  742435a3a99225fa8c280b70d9924276db1e9255# Parent  8bb7f32a3a085961fcf066f2753b38e110d22c2b
merged

diff -r 8bb7f32a3a08 -r c3d0414ba6df src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Sep 17 16:15:33 2010 +0200
+++ b/src/HOL/IsaMakefile	Fri Sep 17 16:15:45 2010 +0200
@@ -271,6 +271,7 @@
   Tools/ATP/atp_proof.ML \
   Tools/ATP/atp_systems.ML \
   Tools/choice_specification.ML \
+  Tools/Datatype/datatype_selectors.ML \
   Tools/int_arith.ML \
   Tools/groebner.ML \
   Tools/list_code.ML \
diff -r 8bb7f32a3a08 -r c3d0414ba6df src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Fri Sep 17 16:15:33 2010 +0200
+++ b/src/HOL/SMT.thy	Fri Sep 17 16:15:45 2010 +0200
@@ -7,6 +7,7 @@
 theory SMT
 imports List
 uses
+  "Tools/Datatype/datatype_selectors.ML"
   ("Tools/SMT/smt_monomorph.ML")
   ("Tools/SMT/smt_normalize.ML")
   ("Tools/SMT/smt_translate.ML")
@@ -323,4 +324,13 @@
 hide_const Pattern term_eq
 hide_const (open) trigger pat nopat fun_app z3div z3mod
 
+
+
+subsection {* Selectors for datatypes *}
+
+setup {* Datatype_Selectors.setup *}
+
+declare [[ selector Pair 1 = fst, selector Pair 2 = snd ]]
+declare [[ selector Cons 1 = hd, selector Cons 2 = tl ]]
+
 end
diff -r 8bb7f32a3a08 -r c3d0414ba6df src/HOL/SMT_Examples/SMT_Tests.thy
--- a/src/HOL/SMT_Examples/SMT_Tests.thy	Fri Sep 17 16:15:33 2010 +0200
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Fri Sep 17 16:15:45 2010 +0200
@@ -607,7 +607,7 @@
 
 
 
-section {* Pairs *}
+section {* Pairs *}  (* FIXME: tests for datatypes and records *)
 
 lemma
   "x = fst (x, y)"
diff -r 8bb7f32a3a08 -r c3d0414ba6df src/HOL/Tools/Datatype/datatype_selectors.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Datatype/datatype_selectors.ML	Fri Sep 17 16:15:45 2010 +0200
@@ -0,0 +1,83 @@
+(*  Title:      HOL/Tools/Datatype/datatype_selectors.ML
+    Author:     Sascha Boehme, TU Muenchen
+
+Selector functions for datatype constructor arguments.
+*)
+
+signature DATATYPE_SELECTORS =
+sig
+  val add_selector: ((string * typ) * int) * (string * typ) ->
+    Context.generic -> Context.generic
+  val lookup_selector: Proof.context -> string * int -> string option
+  val setup: theory -> theory
+end
+
+structure Datatype_Selectors: DATATYPE_SELECTORS =
+struct
+
+structure Stringinttab = Table
+(
+  type key = string * int
+  val ord = prod_ord fast_string_ord int_ord
+)
+
+structure Data = Generic_Data
+(
+  type T = string Stringinttab.table
+  val empty = Stringinttab.empty
+  val extend = I
+  val merge = Stringinttab.merge (K true)
+)
+
+fun pretty_term context = Syntax.pretty_term (Context.proof_of context)
+
+fun sanity_check context (((con as (n, _), i), sel as (m, _))) =
+  let
+    val thy = Context.theory_of context
+    val varify_const =
+      Const #> Type.varify_global [] #> snd #> Term.dest_Const #>
+      snd #> Term.strip_type
+
+    val (Ts, T) = varify_const con
+    val (Us, U) = varify_const sel
+    val _ = (0 < i andalso i <= length Ts) orelse
+      error (Pretty.string_of (Pretty.block [
+        Pretty.str "The constructor ",
+        Pretty.quote (pretty_term context (Const con)),
+        Pretty.str " has no argument position ",
+        Pretty.str (string_of_int i),
+        Pretty.str "."]))
+    val _ = length Us = 1 orelse
+      error (Pretty.string_of (Pretty.block [
+        Pretty.str "The term ", Pretty.quote (pretty_term context (Const sel)),
+        Pretty.str " might not be a selector ",
+        Pretty.str "(it accepts more than one argument)."]))
+    val _ =
+     (Sign.typ_equiv thy (T, hd Us) andalso
+      Sign.typ_equiv thy (nth Ts (i-1), U)) orelse
+      error (Pretty.string_of (Pretty.block [
+        Pretty.str "The types of the constructor ",
+        Pretty.quote (pretty_term context (Const con)),
+        Pretty.str " and of the selector ",
+        Pretty.quote (pretty_term context (Const sel)),
+        Pretty.str " do not fit to each other."]))
+  in ((n, i), m) end
+
+fun add_selector (entry as ((con as (n, _), i), (_, T))) context =
+  (case Stringinttab.lookup (Data.get context) (n, i) of
+    NONE => Data.map (Stringinttab.update (sanity_check context entry)) context
+  | SOME c => error (Pretty.string_of (Pretty.block [
+      Pretty.str "There is already a selector assigned to constructor ",
+      Pretty.quote (pretty_term context (Const con)), Pretty.str ", namely ",
+      Pretty.quote (pretty_term context (Const (c, T))), Pretty.str "."])))
+
+fun lookup_selector ctxt = Stringinttab.lookup (Data.get (Context.Proof ctxt))
+
+val setup =
+  Attrib.setup @{binding selector}
+   ((Args.term >> Term.dest_Const) -- Scan.lift (Parse.nat) --|
+    Scan.lift (Parse.$$$ "=") -- (Args.term >> Term.dest_Const) >>
+    (Thm.declaration_attribute o K o add_selector))
+  "assign a selector function to a datatype constructor argument"
+
+end
diff -r 8bb7f32a3a08 -r c3d0414ba6df src/HOL/Tools/SMT/smt_normalize.ML
--- a/src/HOL/Tools/SMT/smt_normalize.ML	Fri Sep 17 16:15:33 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Fri Sep 17 16:15:45 2010 +0200
@@ -9,14 +9,16 @@
   * embed natural numbers into integers,
   * add extra rules specifying types and constants which occur frequently,
   * fully translate into object logic, add universal closure,
+  * monomorphize (create instances of schematic rules),
   * lift lambda terms,
   * make applications explicit for functions with varying number of arguments.
+  * add (hypothetical definitions for) missing datatype selectors,
 *)
 
 signature SMT_NORMALIZE =
 sig
   type extra_norm = thm list -> Proof.context -> thm list * Proof.context
-  val normalize: extra_norm -> thm list -> Proof.context ->
+  val normalize: extra_norm -> bool -> thm list -> Proof.context ->
     thm list * Proof.context
   val atomize_conv: Proof.context -> conv
   val eta_expand_conv: (Proof.context -> conv) -> Proof.context -> conv
@@ -427,13 +429,60 @@
 
 
 
+(* add missing datatype selectors via hypothetical definitions *)
+
+local
+  val add = (fn Type (n, _) => Symtab.update (n, ()) | _ => I)
+
+  fun collect t =
+    (case Term.strip_comb t of
+      (Abs (_, T, t), _) => add T #> collect t
+    | (Const (_, T), ts) => collects T ts
+    | (Free (_, T), ts) => collects T ts
+    | _ => I)
+  and collects T ts =
+    let val ((Ts, Us), U) = Term.strip_type T |> apfst (chop (length ts))
+    in fold add Ts #> add (Us ---> U) #> fold collect ts end
+
+  fun add_constructors thy n =
+    (case Datatype.get_info thy n of
+      NONE => I
+    | SOME {descr, ...} => fold (fn (_, (_, _, cs)) => fold (fn (n, ds) =>
+        fold (insert (op =) o pair n) (1 upto length ds)) cs) descr)
+
+  fun add_selector (c as (n, i)) ctxt =
+    (case Datatype_Selectors.lookup_selector ctxt c of
+      SOME _ => ctxt
+    | NONE =>
+        let
+          val T = Sign.the_const_type (ProofContext.theory_of ctxt) n
+          val U = Term.body_type T --> nth (Term.binder_types T) (i-1)
+        in
+          ctxt
+          |> yield_singleton Variable.variant_fixes Name.uu
+          |>> pair ((n, T), i) o rpair U
+          |-> Context.proof_map o Datatype_Selectors.add_selector
+        end)
+in
+
+fun datatype_selectors thms ctxt =
+  let
+    val ns = Symtab.keys (fold (collect o Thm.prop_of) thms Symtab.empty)
+    val cs = fold (add_constructors (ProofContext.theory_of ctxt)) ns []
+  in (thms, fold add_selector cs ctxt) end
+    (* FIXME: also generate hypothetical definitions for the selectors *)
+
+end
+
+
+
 (* combined normalization *)
 
 type extra_norm = thm list -> Proof.context -> thm list * Proof.context
 
 fun with_context f thms ctxt = (f ctxt thms, ctxt)
 
-fun normalize extra_norm thms ctxt =
+fun normalize extra_norm with_datatypes thms ctxt =
   thms
   |> trivial_distinct ctxt
   |> rewrite_bool_cases ctxt
@@ -445,5 +494,6 @@
   |-> SMT_Monomorph.monomorph
   |-> lift_lambdas
   |-> with_context explicit_application
+  |-> (if with_datatypes then datatype_selectors else pair)
 
 end
diff -r 8bb7f32a3a08 -r c3d0414ba6df src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Fri Sep 17 16:15:33 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Fri Sep 17 16:15:45 2010 +0200
@@ -195,9 +195,11 @@
       ("timeout: " ^ string_of_int (Config.get ctxt timeout)) ::
       "arguments:" :: arguments
     val {extra_norm, translate} = interface
+    val {builtins, ...} = translate
+    val {has_datatypes, ...} = builtins
   in
     (prems, ctxt)
-    |-> SMT_Normalize.normalize extra_norm
+    |-> SMT_Normalize.normalize extra_norm has_datatypes
     |-> invoke translate comments command arguments
     |-> reconstruct
     |-> (fn thm => fn ctxt' => thm
diff -r 8bb7f32a3a08 -r c3d0414ba6df src/HOL/Tools/SMT/smt_translate.ML
--- a/src/HOL/Tools/SMT/smt_translate.ML	Fri Sep 17 16:15:33 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_translate.ML	Fri Sep 17 16:15:45 2010 +0200
@@ -291,28 +291,31 @@
     SOME (f, _) => (f, cx)
   | NONE => new_fun func_prefix t ss cx)
 
-fun inst_const f Ts t =
-  let
-    val (n, T) = Term.dest_Const (snd (Type.varify_global [] t))
-    val inst = map Term.dest_TVar (snd (Term.dest_Type (f T))) ~~ Ts
-  in Const (n, Term_Subst.instantiateT inst T) end
+fun mk_type (_, Tfs) (d as Datatype.DtTFree _) = the (AList.lookup (op =) Tfs d)
+  | mk_type Ts (Datatype.DtType (n, ds)) = Type (n, map (mk_type Ts) ds)
+  | mk_type (Tds, _) (Datatype.DtRec i) = nth Tds i
 
-fun inst_constructor Ts = inst_const Term.body_type Ts
-fun inst_selector Ts = inst_const Term.domain_type Ts
+fun mk_selector ctxt Ts T n (i, d) =
+  (case Datatype_Selectors.lookup_selector ctxt (n, i+1) of
+    NONE => raise Fail ("missing selector for datatype constructor " ^ quote n)
+  | SOME m => mk_type Ts d |> (fn U => (Const (m, T --> U), U)))
+
+fun mk_constructor ctxt Ts T (n, args) =
+  let val (sels, Us) = split_list (map_index (mk_selector ctxt Ts T n) args)
+  in (Const (n, Us ---> T), sels) end
 
-fun lookup_datatype ctxt n Ts = (* FIXME: use Datatype/Record.get_info *)
-  if n = @{type_name prod}
-  then SOME [
-    (Type (n, Ts), [
-      (inst_constructor Ts @{term Pair},
-        map (inst_selector Ts) [@{term fst}, @{term snd}])])]
-  else if n = @{type_name list}
-  then SOME [
-    (Type (n, Ts), [
-      (inst_constructor Ts @{term Nil}, []),
-      (inst_constructor Ts @{term Cons},
-        map (inst_selector Ts) [@{term hd}, @{term tl}])])]
-  else NONE
+fun lookup_datatype ctxt n Ts = if n = @{type_name bool} then NONE else
+  (case Datatype.get_info (ProofContext.theory_of ctxt) n of
+    NONE => NONE  (* FIXME: also use Record.get_info *)
+  | SOME {descr, ...} =>
+      let
+        val Tds = map (fn (_, (tn, _, _)) => Type (tn, Ts))
+          (sort (int_ord o pairself fst) descr)
+        val Tfs = (case hd descr of (_, (_, tfs, _)) => tfs ~~ Ts)
+      in
+        SOME (descr |> map (fn (i, (_, _, cs)) =>
+          (nth Tds i, map (mk_constructor ctxt (Tds, Tfs) (nth Tds i)) cs)))
+      end)
 
 fun relaxed thms = (([], thms), map prop_of thms)
 
diff -r 8bb7f32a3a08 -r c3d0414ba6df src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Fri Sep 17 16:15:33 2010 +0200
+++ b/src/Tools/Code/code_runtime.ML	Fri Sep 17 16:15:45 2010 +0200
@@ -47,17 +47,23 @@
 
 val _ = Context.>> (Context.map_theory
   (Code_Target.extend_target (target, (Code_ML.target_SML, K I))
-  #> Code_Target.add_tyco_syntax target @{type_name prop} (SOME (0, (K o K o K) (Code_Printer.str s_truth)))
-  #> Code_Target.add_const_syntax target @{const_name Code_Generator.holds} (SOME (Code_Printer.plain_const_syntax s_Holds))
+  #> Code_Target.add_tyco_syntax target @{type_name prop}
+       (SOME (0, (K o K o K) (Code_Printer.str s_truth)))
+  #> Code_Target.add_const_syntax target @{const_name Code_Generator.holds}
+       (SOME (Code_Printer.plain_const_syntax s_Holds))
   #> Code_Target.add_reserved target this
-  #> fold (Code_Target.add_reserved target) ["oo", "ooo", "oooo", "upto", "downto", "orf", "andf"])); (*avoid further pervasive infix names*)
+  #> fold (Code_Target.add_reserved target) ["oo", "ooo", "oooo", "upto", "downto", "orf", "andf"]));
+       (*avoid further pervasive infix names*)
 
 
 (* evaluation into target language values *)
 
 type 'a cookie = (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string;
 
-fun base_evaluator cookie thy some_target naming program ((vs, ty), t) deps args =
+fun obtain_serializer thy some_target = Code_Target.produce_code_for thy
+  (the_default target some_target) NONE "Code" [];
+
+fun base_evaluator cookie serializer naming thy program ((vs, ty), t) deps args =
   let
     val ctxt = ProofContext.init_global thy;
     val _ = if Code_Thingol.contains_dictvar t then
@@ -70,8 +76,7 @@
       |> Graph.new_node (value_name,
           Code_Thingol.Fun (Term.dummy_patternN, (((vs', ty'), [(([IVar NONE], t), (NONE, true))]), NONE)))
       |> fold (curry Graph.add_edge value_name) deps;
-    val (program_code, [SOME value_name']) = Code_Target.produce_code_for thy
-      (the_default target some_target) NONE "Code" [] naming program' [value_name];
+    val (program_code, [SOME value_name']) = serializer naming program' [value_name];
     val value_code = space_implode " "
       (value_name' :: "()" :: map (enclose "(" ")") args);
   in Exn.capture (ML_Context.value ctxt cookie) (program_code, value_code) end;
@@ -84,7 +89,7 @@
 fun dynamic_value_exn cookie thy some_target postproc t args =
   let
     fun evaluator naming program ((_, vs_ty), t) deps =
-      base_evaluator cookie thy some_target naming program (vs_ty, t) deps args;
+      base_evaluator cookie (obtain_serializer thy some_target) naming thy program (vs_ty, t) deps args;
   in Code_Thingol.dynamic_eval_value thy (Exn.map_result o postproc) evaluator t end;
 
 fun dynamic_value_strict cookie thy some_target postproc t args =
@@ -95,8 +100,9 @@
 
 fun static_value_exn cookie thy some_target postproc consts =
   let
+    val serializer = obtain_serializer thy some_target;
     fun evaluator naming program thy ((_, vs_ty), t) deps =
-      base_evaluator cookie thy some_target naming program (vs_ty, t) deps [];
+      base_evaluator cookie serializer naming thy program (vs_ty, t) deps [];
   in Code_Thingol.static_eval_value thy (Exn.map_result o postproc) consts evaluator end;
 
 fun static_value_strict cookie thy some_target postproc consts t =
@@ -115,14 +121,14 @@
 val put_truth = Truth_Result.put;
 val truth_cookie = (Truth_Result.get, put_truth, Long_Name.append this "put_truth");
 
-fun check_holds thy naming program vs_t deps ct =
+fun check_holds serializer naming thy program vs_t deps ct =
   let
     val t = Thm.term_of ct;
     val _ = if fastype_of t <> propT
       then error ("Not a proposition: " ^ Syntax.string_of_term_global thy t)
       else ();
     val iff = Thm.cterm_of thy (Term.Const ("==", propT --> propT --> propT));
-    val result = case partiality_as_none (base_evaluator truth_cookie thy NONE naming program vs_t deps [])
+    val result = case partiality_as_none (base_evaluator truth_cookie serializer naming thy program vs_t deps [])
      of SOME Holds => true
       | _ => false;
   in
@@ -131,15 +137,21 @@
 
 val (_, raw_check_holds_oracle) = Context.>>> (Context.map_theory_result
   (Thm.add_oracle (Binding.name "holds_by_evaluation",
-  fn (thy, naming, program, vs_t, deps, ct) => check_holds thy naming program vs_t deps ct)));
+  fn (serializer, naming, thy, program, vs_t, deps, ct) => check_holds serializer naming thy program vs_t deps ct)));
 
-fun check_holds_oracle thy naming program ((_, vs_ty), t) deps ct =
-  raw_check_holds_oracle (thy, naming, program, (vs_ty, t), deps, ct);
+fun check_holds_oracle serializer naming thy program ((_, vs_ty), t) deps ct =
+  raw_check_holds_oracle (serializer, naming, thy, program, (vs_ty, t), deps, ct);
+
+val dynamic_holds_conv = Conv.tap_thy (fn thy => Code_Thingol.dynamic_eval_conv thy
+  (fn naming => check_holds_oracle (obtain_serializer thy NONE) naming thy));
 
-val dynamic_holds_conv = Conv.tap_thy (fn thy => Code_Thingol.dynamic_eval_conv thy (check_holds_oracle thy));
-
-fun static_holds_conv thy consts = Code_Thingol.static_eval_conv thy consts
-  (fn naming => fn program => fn thy => check_holds_oracle thy naming program);
+fun static_holds_conv thy consts =
+  let
+    val serializer = obtain_serializer thy NONE;
+  in
+    Code_Thingol.static_eval_conv thy consts
+      (fn naming => fn program => fn thy => check_holds_oracle serializer naming thy program)
+  end;
 
 
 (** instrumentalization **)
@@ -253,7 +265,7 @@
 fun add_eval_const (const, const') = Code_Target.add_const_syntax target
   const (SOME (Code_Printer.simple_const_syntax (0, (K o K o K) const')));
 
-fun process (code_body, (tyco_map, (constr_map, const_map))) module_name NONE thy =
+fun process_reflection (code_body, (tyco_map, (constr_map, const_map))) module_name NONE thy =
       thy
       |> Code_Target.add_reserved target module_name
       |> Context.theory_map
@@ -261,7 +273,7 @@
       |> fold (add_eval_tyco o apsnd Code_Printer.str) tyco_map
       |> fold (add_eval_constr o apsnd Code_Printer.str) constr_map
       |> fold (add_eval_const o apsnd Code_Printer.str) const_map
-  | process (code_body, _) _ (SOME file_name) thy =
+  | process_reflection (code_body, _) _ (SOME file_name) thy =
       let
         val preamble =
           "(* Generated from " ^ Path.implode (Thy_Header.thy_path (Context.theory_name thy))
@@ -283,7 +295,7 @@
       |> (apsnd o apsnd) (chop (length constrs));
   in
     thy
-    |> process result module_name some_file
+    |> process_reflection result module_name some_file
   end;
 
 val code_reflect = gen_code_reflect Code_Target.cert_tyco (K I);
diff -r 8bb7f32a3a08 -r c3d0414ba6df src/Tools/Code/code_simp.ML
--- a/src/Tools/Code/code_simp.ML	Fri Sep 17 16:15:33 2010 +0200
+++ b/src/Tools/Code/code_simp.ML	Fri Sep 17 16:15:45 2010 +0200
@@ -66,7 +66,7 @@
 fun conclude_tac thy some_ss = Simplifier.full_simp_tac (simpset_default thy some_ss);
 
 
-(* evaluation with current code context *)
+(* evaluation with dynamic code context *)
 
 fun dynamic_eval_conv thy = no_frees_conv (Code_Thingol.dynamic_eval_conv thy
   (fn naming => fn program => fn t => fn deps => rewrite_modulo thy NONE program));
@@ -81,11 +81,11 @@
   #> Value.add_evaluator ("simp", dynamic_eval_value o ProofContext.theory_of);
 
 
-(* evaluation with freezed code context *)
+(* evaluation with static code context *)
 
 fun static_eval_conv thy some_ss consts = no_frees_conv
   (Code_Thingol.static_eval_conv_simple thy consts
-    (fn program => fn thy => rewrite_modulo thy some_ss program));
+    (fn program => fn thy => fn _ => fn _ => rewrite_modulo thy some_ss program));
 
 fun static_eval_tac thy some_ss consts = CONVERSION (static_eval_conv thy some_ss consts)
   THEN' conclude_tac thy some_ss;
diff -r 8bb7f32a3a08 -r c3d0414ba6df src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Fri Sep 17 16:15:33 2010 +0200
+++ b/src/Tools/Code/code_target.ML	Fri Sep 17 16:15:45 2010 +0200
@@ -241,7 +241,7 @@
 
 local
 
-fun activate_target_for thy target naming program =
+fun activate_target thy target =
   let
     val ((targets, abortable), default_width) = Targets.get thy;
     fun collapse_hierarchy target =
@@ -250,13 +250,13 @@
          of SOME data => data
           | NONE => error ("Unknown code target language: " ^ quote target);
       in case the_description data
-       of Fundamental _ => (I, data)
+       of Fundamental _ => (K I, data)
         | Extension (super, modify) => let
             val (modify', data') = collapse_hierarchy super
-          in (modify' #> modify naming, merge_target false target (data', data)) end
+          in (fn naming => modify' naming #> modify naming, merge_target false target (data', data)) end
       end;
     val (modify, data) = collapse_hierarchy target;
-  in (default_width, abortable, data, modify program) end;
+  in (default_width, abortable, data, modify) end;
 
 fun activate_syntax lookup_name src_tab = Symtab.empty
   |> fold_map (fn thing_identifier => fn tab => case lookup_name thing_identifier
@@ -303,7 +303,7 @@
     val program4 = Graph.subgraph (member (op =) names4) program3;
   in (names4, program4) end;
 
-fun invoke_serializer thy abortable serializer literals reserved abs_includes 
+fun invoke_serializer thy abortable serializer literals reserved all_includes
     module_alias proto_class_syntax proto_instance_syntax proto_tyco_syntax proto_const_syntax
     module_name args naming proto_program names =
   let
@@ -311,7 +311,12 @@
       activate_symbol_syntax thy literals naming
         proto_class_syntax proto_instance_syntax proto_tyco_syntax proto_const_syntax;
     val (names_all, program) = project_program thy abortable names_hidden names proto_program;
-    val includes = abs_includes names_all;
+    fun select_include (name, (content, cs)) =
+      if null cs orelse exists (fn c => case Code_Thingol.lookup_const naming c
+       of SOME name => member (op =) names_all name
+        | NONE => false) cs
+      then SOME (name, content) else NONE;
+    val includes = map_filter select_include (Symtab.dest all_includes);
   in
     serializer args {
       labelled_name = Code_Thingol.labelled_name thy proto_program,
@@ -324,29 +329,20 @@
       program = program }
   end;
 
-fun mount_serializer thy target some_width module_name args naming proto_program names =
+fun mount_serializer thy target some_width module_name args =
   let
-    val (default_width, abortable, data, program) =
-      activate_target_for thy target naming proto_program;
+    val (default_width, abortable, data, modify) = activate_target thy target;
     val serializer = case the_description data
      of Fundamental seri => #serializer seri;
     val reserved = the_reserved data;
-    fun select_include names_all (name, (content, cs)) =
-      if null cs then SOME (name, content)
-      else if exists (fn c => case Code_Thingol.lookup_const naming c
-       of SOME name => member (op =) names_all name
-        | NONE => false) cs
-      then SOME (name, content) else NONE;
-    fun includes names_all = map_filter (select_include names_all)
-      ((Symtab.dest o the_includes) data);
     val module_alias = the_module_alias data 
     val { class, instance, tyco, const } = the_symbol_syntax data;
     val literals = the_literals thy target;
     val width = the_default default_width some_width;
-  in
+  in fn naming => fn program => fn names =>
     invoke_serializer thy abortable serializer literals reserved
-      includes module_alias class instance tyco const module_name args
-        naming program names width
+      (the_includes data) module_alias class instance tyco const module_name args
+        naming (modify naming program) names width
   end;
 
 fun assert_module_name "" = error ("Empty module name not allowed.")
@@ -354,16 +350,22 @@
 
 in
 
-fun export_code_for thy some_path target some_width some_module_name args naming program names =
-  export some_path (mount_serializer thy target some_width some_module_name args naming program names);
+fun export_code_for thy some_path target some_width module_name args =
+  export some_path ooo mount_serializer thy target some_width module_name args;
 
-fun produce_code_for thy target some_width module_name args naming program names =
+fun produce_code_for thy target some_width module_name args =
   let
-    val (s, deresolve) = produce (mount_serializer thy target some_width (assert_module_name module_name) args naming program names)
-  in (s, map deresolve names) end;
+    val serializer = mount_serializer thy target some_width (assert_module_name module_name) args;
+  in fn naming => fn program => fn names =>
+    produce (serializer naming program names) |> apsnd (fn deresolve => map deresolve names)
+  end;
 
-fun present_code_for thy target some_width module_name args naming program (names, selects) =
-  present selects (mount_serializer thy target some_width (assert_module_name module_name) args naming program names);
+fun present_code_for thy target some_width module_name args =
+  let
+    val serializer = mount_serializer thy target some_width (assert_module_name module_name) args;
+  in fn naming => fn program => fn (names, selects) =>
+    present selects (serializer naming program names)
+  end;
 
 fun check_code_for thy target strict args naming program names_cs =
   let
diff -r 8bb7f32a3a08 -r c3d0414ba6df src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Fri Sep 17 16:15:33 2010 +0200
+++ b/src/Tools/Code/code_thingol.ML	Fri Sep 17 16:15:45 2010 +0200
@@ -92,19 +92,20 @@
 
   val read_const_exprs: theory -> string list -> string list * string list
   val consts_program: theory -> bool -> string list -> string list * (naming * program)
-  val dynamic_eval_conv: theory
-    -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> conv)
+  val dynamic_eval_conv: theory -> (naming -> program
+    -> ((string * sort) list * typscheme) * iterm -> string list -> conv)
     -> conv
-  val dynamic_eval_value: theory -> ((term -> term) -> 'a -> 'a)
-    -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
+  val dynamic_eval_value: theory -> ((term -> term) -> 'a -> 'a) -> (naming -> program
+    -> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
     -> term -> 'a
-  val static_eval_conv: theory -> string list
-    -> (naming -> program -> theory -> ((string * sort) list * typscheme) * iterm -> string list -> conv)
+  val static_eval_conv: theory -> string list -> (naming -> program
+    -> theory -> ((string * sort) list * typscheme) * iterm -> string list -> conv)
     -> conv
   val static_eval_conv_simple: theory -> string list
-    -> (program -> theory -> conv) -> conv
-  val static_eval_value: theory -> ((term -> term) -> 'a -> 'a) -> string list
-    -> (naming -> program -> theory -> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
+    -> (program -> theory -> (string * sort) list -> term -> conv) -> conv
+  val static_eval_value: theory -> ((term -> term) -> 'a -> 'a) -> string list ->
+    (naming -> program
+      -> theory -> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
     -> term -> 'a
 end;
 
@@ -844,17 +845,17 @@
 
 (* program generation *)
 
-fun consts_program thy permissive cs =
+fun consts_program thy permissive consts =
   let
-    fun project_consts cs (naming, program) = (*FIXME only necessary for cache_generation*)
-      let
-        val cs_all = Graph.all_succs program cs;
-      in (cs, (naming, Graph.subgraph (member (op =) cs_all) program)) end;
+    fun project_consts consts (naming, program) =
+      if permissive then (consts, (naming, program))
+      else (consts, (naming, Graph.subgraph
+        (member (op =) (Graph.all_succs program consts)) program));
     fun generate_consts thy algebra eqngr =
       fold_map (ensure_const thy algebra eqngr permissive);
   in
-    invoke_generation (not permissive) thy (Code_Preproc.obtain false thy cs [])
-      generate_consts cs
+    invoke_generation permissive thy (Code_Preproc.obtain false thy consts [])
+      generate_consts consts
     |-> project_consts
   end;
 
@@ -887,15 +888,14 @@
     #> term_value
   end;
 
-fun base_evaluator evaluator algebra eqngr thy vs t =
+fun original_sorts vs =
+  map (fn (v, _) => (v, (the o AList.lookup (op =) vs o prefix "'") v));
+
+fun dynamic_evaluator thy evaluator algebra eqngr vs t =
   let
     val (((naming, program), (((vs', ty'), t'), deps)), _) =
       invoke_generation false thy (algebra, eqngr) ensure_value t;
-    val vs'' = map (fn (v, _) => (v, (the o AList.lookup (op =) vs o prefix "'") v)) vs';
-  in evaluator naming program thy ((vs'', (vs', ty')), t') deps end;
-
-fun dynamic_evaluator thy evaluator algebra eqngr vs t =
-  base_evaluator (fn naming => fn program => fn _ => evaluator naming program) algebra eqngr thy vs t;
+  in evaluator naming program ((original_sorts vs vs', (vs', ty')), t') deps end;
 
 fun dynamic_eval_conv thy evaluator =
   Code_Preproc.dynamic_eval_conv thy (dynamic_evaluator thy evaluator);
@@ -903,18 +903,32 @@
 fun dynamic_eval_value thy postproc evaluator =
   Code_Preproc.dynamic_eval_value thy postproc (dynamic_evaluator thy evaluator);
 
+fun provide_program thy consts f algebra eqngr =
+  let
+    fun generate_consts thy algebra eqngr =
+      fold_map (ensure_const thy algebra eqngr false);
+    val (_, (naming, program)) = invoke_generation true thy (algebra, eqngr)
+      generate_consts consts;
+  in f algebra eqngr naming program end;
+
+fun static_evaluator evaluator algebra eqngr naming program thy vs t =
+  let
+    val (((_, program'), (((vs', ty'), t'), deps)), _) =
+      ensure_value thy algebra eqngr t (NONE, (naming, program));
+  in evaluator naming program' thy ((original_sorts vs vs', (vs', ty')), t') deps end;
+
 fun static_eval_conv thy consts conv =
-  Code_Preproc.static_eval_conv thy consts (base_evaluator conv); (*FIXME avoid re-generation*)
+  Code_Preproc.static_eval_conv thy consts
+    (provide_program thy consts (static_evaluator conv));
 
 fun static_eval_conv_simple thy consts conv =
-  Code_Preproc.static_eval_conv thy consts (fn algebra => fn eqngr => fn thy => fn _ => fn _ => fn ct =>
-    conv ((NONE, (empty_naming, Graph.empty)) (*FIXME provide abstraction for this kind of invocation*)
-      |> fold_map (ensure_const thy algebra eqngr false) consts
-      |> (snd o snd o snd)) thy ct);
+  Code_Preproc.static_eval_conv thy consts
+    (provide_program thy consts ((K o K o K) conv));
 
-fun static_eval_value thy postproc consts conv =
-  Code_Preproc.static_eval_value thy postproc consts (base_evaluator conv); (*FIXME avoid re-generation*)
-  
+fun static_eval_value thy postproc consts evaluator =
+  Code_Preproc.static_eval_value thy postproc consts
+    (provide_program thy consts (static_evaluator evaluator));
+
 
 (** diagnostic commands **)