src/Tools/Code/code_runtime.ML

--- a/src/Tools/Code/code_runtime.ML	Sat Jan 25 23:50:49 2014 +0100
+++ b/src/Tools/Code/code_runtime.ML	Sat Jan 25 23:50:49 2014 +0100
@@ -52,7 +52,7 @@
 datatype truth = Holds;
 
 val _ = Theory.setup
-  (Code_Target.extend_target (target, (Code_ML.target_SML, K I))
+  (Code_Target.extend_target (target, (Code_ML.target_SML, I))
   #> Code_Target.set_printings (Code_Symbol.Type_Constructor (@{type_name prop},
     [(target, SOME (0, (K o K o K) (Code_Printer.str s_truth)))]))
   #> Code_Target.set_printings (Code_Symbol.Constant (@{const_name Code_Generator.holds},
@@ -87,10 +87,13 @@
     val ctxt = Proof_Context.init_global thy;
   in ((Sign.no_frees ctxt o Sign.no_vars ctxt o map_types (K dummyT)) t; t) end;
 
-fun obtain_evaluator thy some_target naming program consts expr =
-  Code_Target.evaluator thy (the_default target some_target) naming program consts expr
+fun obtain_evaluator thy some_target program consts expr =
+  Code_Target.evaluator thy (the_default target some_target) program consts expr
   |> apfst (fn ml_modules => space_implode "\n\n" (map snd ml_modules));
 
+fun obtain_evaluator' thy some_target program =
+  obtain_evaluator thy some_target program o map Code_Symbol.Constant;
+
 fun evaluation cookie thy evaluator vs_t args =
   let
     val ctxt = Proof_Context.init_global thy;
@@ -110,8 +113,8 @@
     val _ = if ! trace
       then tracing ("Evaluation of term " ^ quote (Syntax.string_of_term_global thy t))
       else ()
-    fun evaluator naming program ((_, vs_ty), t) deps =
-      evaluation cookie thy (obtain_evaluator thy some_target naming program deps) (vs_ty, t) args;
+    fun evaluator program ((_, vs_ty), t) deps =
+      evaluation cookie thy (obtain_evaluator thy some_target program deps) (vs_ty, t) args;
   in Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t end;
 
 fun dynamic_value_strict cookie thy some_target postproc t args =
@@ -120,9 +123,9 @@
 fun dynamic_value cookie thy some_target postproc t args =
   partiality_as_none (dynamic_value_exn cookie thy some_target postproc t args);
 
-fun static_evaluator cookie thy some_target naming program consts' =
+fun static_evaluator cookie thy some_target program consts' =
   let
-    val evaluator = obtain_evaluator thy some_target naming program consts'
+    val evaluator = obtain_evaluator' thy some_target program consts'
   in fn ((_, vs_ty), t) => fn _ => evaluation cookie thy evaluator (vs_ty, t) [] end;
 
 fun static_value_exn cookie thy some_target postproc consts =
@@ -175,13 +178,13 @@
 in
 
 fun dynamic_holds_conv thy = Code_Thingol.dynamic_conv thy
-  (fn naming => fn program => fn vs_t => fn deps =>
-    check_holds_oracle thy (obtain_evaluator thy NONE naming program deps) vs_t deps)
+  (fn program => fn vs_t => fn deps =>
+    check_holds_oracle thy (obtain_evaluator thy NONE program deps) vs_t deps)
       o reject_vars thy;
 
 fun static_holds_conv thy consts = Code_Thingol.static_conv thy consts
-  (fn naming => fn program => fn consts' =>
-    check_holds_oracle thy (obtain_evaluator thy NONE naming program consts'))
+  (fn program => fn consts' =>
+    check_holds_oracle thy (obtain_evaluator' thy NONE program consts'))
       o reject_vars thy;
 
 end; (*local*)
@@ -192,23 +195,22 @@
 fun evaluation_code thy module_name tycos consts =
   let
     val ctxt = Proof_Context.init_global thy;
-    val (consts', (naming, program)) = Code_Thingol.consts_program thy false consts;
-    val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos;
+    val program = Code_Thingol.consts_program thy false consts;
     val (ml_modules, target_names) =
       Code_Target.produce_code_for thy
-        target NONE module_name [] naming program (consts' @ tycos');
+        target NONE module_name [] program (map Code_Symbol.Constant consts @ map Code_Symbol.Type_Constructor tycos);
     val ml_code = space_implode "\n\n" (map snd ml_modules);
-    val (consts'', tycos'') = chop (length consts') target_names;
+    val (consts', tycos') = chop (length consts) target_names;
     val consts_map = map2 (fn const =>
       fn NONE =>
           error ("Constant " ^ (quote o Code.string_of_const thy) const ^
             "\nhas a user-defined serialization")
-       | SOME const'' => (const, const'')) consts consts''
+       | SOME const' => (const, const')) consts consts'
     val tycos_map = map2 (fn tyco =>
       fn NONE =>
           error ("Type " ^ quote (Proof_Context.extern_type ctxt tyco) ^
             "\nhas a user-defined serialization")
-        | SOME tyco'' => (tyco, tyco'')) tycos tycos'';
+        | SOME tyco' => (tyco, tyco')) tycos tycos';
   in (ml_code, (tycos_map, consts_map)) end;