merged

--- a/src/Tools/Code/code_runtime.ML	Fri Sep 17 10:52:35 2010 +0200
+++ b/src/Tools/Code/code_runtime.ML	Fri Sep 17 12:26:57 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);

--- a/src/Tools/Code/code_simp.ML	Fri Sep 17 10:52:35 2010 +0200
+++ b/src/Tools/Code/code_simp.ML	Fri Sep 17 12:26:57 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;

--- a/src/Tools/Code/code_target.ML	Fri Sep 17 10:52:35 2010 +0200
+++ b/src/Tools/Code/code_target.ML	Fri Sep 17 12:26:57 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

--- a/src/Tools/Code/code_thingol.ML	Fri Sep 17 10:52:35 2010 +0200
+++ b/src/Tools/Code/code_thingol.ML	Fri Sep 17 12:26:57 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 **)