# HG changeset patch
# User haftmann
# Date 1260279079 -3600
# Node ID f13b5c023e656c5312f8aba6dfe6b972118e1665
# Parent  f7480c5a34e876d072797ccbdab43627a4bdb3d4
simplified notion of empty module name

diff -r f7480c5a34e8 -r f13b5c023e65 src/Tools/Code/code_eval.ML
--- a/src/Tools/Code/code_eval.ML	Tue Dec 08 13:41:37 2009 +0100
+++ b/src/Tools/Code/code_eval.ML	Tue Dec 08 14:31:19 2009 +0100
@@ -21,14 +21,14 @@
 
 val target = "Eval";
 
-val eval_struct_name = "Code"
+val eval_struct_name = "Code";
 
 fun evaluation_code thy tycos consts =
   let
     val (consts', (naming, program)) = Code_Thingol.consts_program thy consts;
     val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos;
     val (ml_code, target_names) = Code_ML.evaluation_code_of thy target
-      (SOME eval_struct_name) naming program (consts' @ tycos');
+      eval_struct_name naming program (consts' @ tycos');
     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
@@ -56,7 +56,7 @@
               Code_Thingol.Fun (Term.dummy_patternN, (([], ty), [(([], t), (Drule.dummy_thm, true))])))
           |> fold (curry Graph.add_edge value_name) deps;
         val (value_code, [SOME value_name']) = Code_ML.evaluation_code_of thy
-          (the_default target some_target) NONE naming program' [value_name];
+          (the_default target some_target) "" naming program' [value_name];
         val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'
           ^ space_implode " " (map (enclose "(" ")") args) ^ " end";
       in ML_Context.evaluate ctxt false reff sml_code end;
diff -r f7480c5a34e8 -r f13b5c023e65 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Tue Dec 08 13:41:37 2009 +0100
+++ b/src/Tools/Code/code_ml.ML	Tue Dec 08 14:31:19 2009 +0100
@@ -7,7 +7,7 @@
 signature CODE_ML =
 sig
   val target_SML: string
-  val evaluation_code_of: theory -> string -> string option
+  val evaluation_code_of: theory -> string -> string
     -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
   val setup: theory -> theory
 end;
@@ -339,7 +339,9 @@
           end;
   in print_stmt end;
 
-fun print_sml_module name some_decls body = Pretty.chunks2 (
+fun print_sml_module name some_decls body = if name = ""
+  then Pretty.chunks2 body
+  else Pretty.chunks2 (
     Pretty.chunks (
       str ("structure " ^ name ^ (if is_some some_decls then " : sig" else " ="))
       :: (the_list o Option.map (Pretty.indent 2 o Pretty.chunks)) some_decls
@@ -663,7 +665,9 @@
           end;
   in print_stmt end;
 
-fun print_ocaml_module name some_decls body = Pretty.chunks2 (
+fun print_ocaml_module name some_decls body = if name = ""
+  then Pretty.chunks2 body
+  else Pretty.chunks2 (
     Pretty.chunks (
       str ("module " ^ name ^ (if is_some some_decls then " : sig" else " ="))
       :: (the_list o Option.map (Pretty.indent 2 o Pretty.chunks)) some_decls
@@ -938,13 +942,9 @@
 
 (** for instrumentalization **)
 
-fun evaluation_code_of thy target some_struct_name =
-  let
-    val serialize = if is_some some_struct_name then fn _ => fn [] =>
-        serialize_ml target (SOME (K ())) print_sml_module print_sml_stmt some_struct_name true
-      else fn _ => fn [] => 
-        serialize_ml target (SOME (K ())) ((K o K) Pretty.chunks2) print_sml_stmt some_struct_name true;
-  in Code_Target.serialize_custom thy (target, (serialize, literals_sml)) end;
+fun evaluation_code_of thy target struct_name =
+  Code_Target.serialize_custom thy (target, (fn _ => fn [] =>
+    serialize_ml target (SOME (K ())) print_sml_module print_sml_stmt (SOME struct_name) true, literals_sml));
 
 
 (** Isar setup **)