avoid strange special treatment of empty module names
authorhaftmann
Tue Aug 31 16:51:29 2010 +0200 (2010-08-31)
changeset 38933bd77e092f67c
parent 38932 515059ca8022
child 38934 94d239bbb618
avoid strange special treatment of empty module names
src/Tools/Code/code_eval.ML
src/Tools/Code/code_ml.ML
src/Tools/Code/code_target.ML
     1.1 --- a/src/Tools/Code/code_eval.ML	Tue Aug 31 16:51:29 2010 +0200
     1.2 +++ b/src/Tools/Code/code_eval.ML	Tue Aug 31 16:51:29 2010 +0200
     1.3 @@ -24,7 +24,7 @@
     1.4      val (consts', (naming, program)) = Code_Thingol.consts_program thy false consts;
     1.5      val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos;
     1.6      val (ml_code, target_names) = Code_Target.produce_code_for thy
     1.7 -      target NONE (SOME module_name) [] naming program (consts' @ tycos');
     1.8 +      target NONE module_name [] naming program (consts' @ tycos');
     1.9      val (consts'', tycos'') = chop (length consts') target_names;
    1.10      val consts_map = map2 (fn const => fn NONE =>
    1.11          error ("Constant " ^ (quote o Code.string_of_const thy) const
    1.12 @@ -52,7 +52,7 @@
    1.13                Code_Thingol.Fun (Term.dummy_patternN, ((([], ty), [(([], t), (NONE, true))]), NONE)))
    1.14            |> fold (curry Graph.add_edge value_name) deps;
    1.15          val (program_code, [SOME value_name']) = Code_Target.produce_code_for thy
    1.16 -          (the_default target some_target) NONE (SOME "Code") [] naming program' [value_name];
    1.17 +          (the_default target some_target) NONE "Code" [] naming program' [value_name];
    1.18          val value_code = space_implode " "
    1.19            (value_name' :: map (enclose "(" ")") args);
    1.20        in ML_Context.evaluate ctxt false reff (program_code, value_code) end;
     2.1 --- a/src/Tools/Code/code_ml.ML	Tue Aug 31 16:51:29 2010 +0200
     2.2 +++ b/src/Tools/Code/code_ml.ML	Tue Aug 31 16:51:29 2010 +0200
     2.3 @@ -339,9 +339,8 @@
     2.4            end;
     2.5    in print_stmt end;
     2.6  
     2.7 -fun print_sml_module name some_decls body = if name = ""
     2.8 -  then Pretty.chunks2 body
     2.9 -  else Pretty.chunks2 (
    2.10 +fun print_sml_module name some_decls body =
    2.11 +  Pretty.chunks2 (
    2.12      Pretty.chunks (
    2.13        str ("structure " ^ name ^ (if is_some some_decls then " : sig" else " ="))
    2.14        :: (the_list o Option.map (indent 2 o Pretty.chunks)) some_decls
    2.15 @@ -665,9 +664,8 @@
    2.16            end;
    2.17    in print_stmt end;
    2.18  
    2.19 -fun print_ocaml_module name some_decls body = if name = ""
    2.20 -  then Pretty.chunks2 body
    2.21 -  else Pretty.chunks2 (
    2.22 +fun print_ocaml_module name some_decls body =
    2.23 +  Pretty.chunks2 (
    2.24      Pretty.chunks (
    2.25        str ("module " ^ name ^ (if is_some some_decls then " : sig" else " ="))
    2.26        :: (the_list o Option.map (indent 2 o Pretty.chunks)) some_decls
     3.1 --- a/src/Tools/Code/code_target.ML	Tue Aug 31 16:51:29 2010 +0200
     3.2 +++ b/src/Tools/Code/code_target.ML	Tue Aug 31 16:51:29 2010 +0200
     3.3 @@ -9,21 +9,21 @@
     3.4    val cert_tyco: theory -> string -> string
     3.5    val read_tyco: theory -> string -> string
     3.6  
     3.7 -  val export_code_for: theory -> Path.T option -> string -> int option -> string option -> Token.T list
     3.8 +  val export_code_for: theory -> Path.T option -> string -> int option -> string -> Token.T list
     3.9      -> Code_Thingol.naming -> Code_Thingol.program -> string list -> unit
    3.10 -  val produce_code_for: theory -> string -> int option -> string option -> Token.T list
    3.11 +  val produce_code_for: theory -> string -> int option -> string -> Token.T list
    3.12      -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
    3.13 -  val present_code_for: theory -> string -> int option -> string option -> Token.T list
    3.14 +  val present_code_for: theory -> string -> int option -> string -> Token.T list
    3.15      -> Code_Thingol.naming -> Code_Thingol.program -> string list * string list -> string
    3.16    val check_code_for: theory -> string -> bool -> Token.T list
    3.17      -> Code_Thingol.naming -> Code_Thingol.program -> string list -> unit
    3.18  
    3.19    val export_code: theory -> string list
    3.20 -    -> (((string * string option) * Path.T option) * Token.T list) list -> unit
    3.21 +    -> (((string * string) * Path.T option) * Token.T list) list -> unit
    3.22    val produce_code: theory -> string list
    3.23 -    -> string -> int option -> string option -> Token.T list -> string * string option list
    3.24 +    -> string -> int option -> string -> Token.T list -> string * string option list
    3.25    val present_code: theory -> string list -> (Code_Thingol.naming -> string list)
    3.26 -    -> string -> int option -> string option -> Token.T list -> string
    3.27 +    -> string -> int option -> string -> Token.T list -> string
    3.28    val check_code: theory -> string list
    3.29      -> ((string * bool) * Token.T list) list -> unit
    3.30  
    3.31 @@ -319,7 +319,7 @@
    3.32        labelled_name = Code_Thingol.labelled_name thy proto_program,
    3.33        reserved_syms = reserved,
    3.34        includes = includes,
    3.35 -      module_alias = if is_some module_name then K module_name else Symtab.lookup module_alias,
    3.36 +      module_alias = if module_name = "" then Symtab.lookup module_alias else K (SOME module_name),
    3.37        class_syntax = Symtab.lookup class_syntax,
    3.38        tyco_syntax = Symtab.lookup tyco_syntax,
    3.39        const_syntax = Symtab.lookup const_syntax,
    3.40 @@ -336,7 +336,7 @@
    3.41       of Fundamental seri => #serializer seri;
    3.42      val presentation_names = stmt_names_of_destination destination;
    3.43      val module_name = if null presentation_names
    3.44 -      then raw_module_name else SOME "Code";
    3.45 +      then raw_module_name else "Code";
    3.46      val reserved = the_reserved data;
    3.47      fun select_include names_all (name, (content, cs)) =
    3.48        if null cs then SOME (name, content)
    3.49 @@ -356,20 +356,23 @@
    3.50          naming program (names, presentation_names) width destination
    3.51    end;
    3.52  
    3.53 +fun assert_module_name "" = error ("Empty module name not allowed.")
    3.54 +  | assert_module_name module_name = module_name;
    3.55 +
    3.56  in
    3.57  
    3.58  fun export_code_for thy some_path target some_width some_module_name args naming program names =
    3.59    export some_path (mount_serializer thy target some_width some_module_name args naming program names);
    3.60  
    3.61 -fun produce_code_for thy target some_width some_module_name args naming program names =
    3.62 -  produce (mount_serializer thy target some_width some_module_name args naming program names);
    3.63 +fun produce_code_for thy target some_width module_name args naming program names =
    3.64 +  produce (mount_serializer thy target some_width (assert_module_name module_name) args naming program names);
    3.65  
    3.66 -fun present_code_for thy target some_width some_module_name args naming program (names, selects) =
    3.67 -  present selects (mount_serializer thy target some_width some_module_name args naming program names);
    3.68 +fun present_code_for thy target some_width module_name args naming program (names, selects) =
    3.69 +  present selects (mount_serializer thy target some_width (assert_module_name module_name) args naming program names);
    3.70  
    3.71  fun check_code_for thy target strict args naming program names_cs =
    3.72    let
    3.73 -    val module_name = "Code_Test";
    3.74 +    val module_name = "Code";
    3.75      val { env_var, make_destination, make_command } =
    3.76        (#check o the_fundamental thy) target;
    3.77      val env_param = getenv env_var;
    3.78 @@ -377,7 +380,7 @@
    3.79        let 
    3.80          val destination = make_destination p;
    3.81          val _ = export (SOME destination) (mount_serializer thy target (SOME 80)
    3.82 -          (SOME module_name) args naming program names_cs);
    3.83 +          module_name args naming program names_cs);
    3.84          val cmd = make_command env_param module_name;
    3.85        in if bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
    3.86          then error ("Code check failed for " ^ target ^ ": " ^ cmd)
    3.87 @@ -518,15 +521,17 @@
    3.88  val add_include = gen_add_include (K I);
    3.89  val add_include_cmd = gen_add_include Code.read_const;
    3.90  
    3.91 -fun add_module_alias target (thyname, modlname) =
    3.92 -  let
    3.93 -    val xs = Long_Name.explode modlname;
    3.94 -    val xs' = map (Name.desymbolize true) xs;
    3.95 -  in if xs' = xs
    3.96 -    then map_module_alias target (Symtab.update (thyname, modlname))
    3.97 -    else error ("Invalid module name: " ^ quote modlname ^ "\n"
    3.98 -      ^ "perhaps try " ^ quote (Long_Name.implode xs'))
    3.99 -  end;
   3.100 +fun add_module_alias target (thyname, "") =
   3.101 +      map_module_alias target (Symtab.delete thyname)
   3.102 +  | add_module_alias target (thyname, modlname) =
   3.103 +      let
   3.104 +        val xs = Long_Name.explode modlname;
   3.105 +        val xs' = map (Name.desymbolize true) xs;
   3.106 +      in if xs' = xs
   3.107 +        then map_module_alias target (Symtab.update (thyname, modlname))
   3.108 +        else error ("Invalid module name: " ^ quote modlname ^ "\n"
   3.109 +          ^ "perhaps try " ^ quote (Long_Name.implode xs'))
   3.110 +      end;
   3.111  
   3.112  fun gen_allow_abort prep_const raw_c thy =
   3.113    let
   3.114 @@ -585,7 +590,7 @@
   3.115        -- ((Parse.$$$ "?" |-- Scan.succeed false) || Scan.succeed true) -- code_expr_argsP))
   3.116        >> (fn seris => check_code_cmd raw_cs seris)
   3.117      || Scan.repeat (Parse.$$$ inK |-- Parse.name
   3.118 -       -- Scan.option (Parse.$$$ module_nameK |-- Parse.name)
   3.119 +       -- Scan.optional (Parse.$$$ module_nameK |-- Parse.name) ""
   3.120         -- Scan.optional (Parse.$$$ fileK |-- Parse.name) ""
   3.121         -- code_expr_argsP) >> (fn seris => export_code_cmd raw_cs seris)));
   3.122