1.1 --- a/src/Tools/Code/code_haskell.ML Thu Aug 26 12:30:43 2010 +0200
1.2 +++ b/src/Tools/Code/code_haskell.ML Thu Aug 26 13:50:58 2010 +0200
1.3 @@ -261,9 +261,8 @@
1.4 end;
1.5 in print_stmt end;
1.6
1.7 -fun haskell_program_of_program labelled_name module_name module_prefix reserved raw_module_alias program =
1.8 +fun haskell_program_of_program labelled_name module_prefix reserved module_alias program =
1.9 let
1.10 - val module_alias = if is_some module_name then K module_name else raw_module_alias;
1.11 val reserved = Name.make_context reserved;
1.12 val mk_name_module = mk_name_module reserved module_prefix module_alias program;
1.13 fun add_stmt (name, (stmt, deps)) =
1.14 @@ -314,15 +313,14 @@
1.15 handle Option => error ("Unknown statement name: " ^ labelled_name name);
1.16 in (deresolver, hs_program) end;
1.17
1.18 -fun serialize_haskell module_prefix raw_module_name string_classes labelled_name
1.19 - raw_reserved includes raw_module_alias
1.20 - syntax_class syntax_tyco syntax_const (code_of_pretty, code_writeln) program stmt_names destination =
1.21 +fun serialize_haskell module_prefix module_name string_classes labelled_name
1.22 + raw_reserved includes module_alias
1.23 + syntax_class syntax_tyco syntax_const (code_of_pretty, code_writeln) program
1.24 + (stmt_names, presentation_stmt_names) destination =
1.25 let
1.26 - val presentation_stmt_names = Code_Target.stmt_names_of_destination destination;
1.27 - val module_name = if null presentation_stmt_names then raw_module_name else SOME "Code";
1.28 val reserved = fold (insert (op =) o fst) includes raw_reserved;
1.29 val (deresolver, hs_program) = haskell_program_of_program labelled_name
1.30 - module_name module_prefix reserved raw_module_alias program;
1.31 + module_prefix reserved module_alias program;
1.32 val contr_classparam_typs = Code_Thingol.contr_classparam_typs program;
1.33 fun deriving_show tyco =
1.34 let
2.1 --- a/src/Tools/Code/code_ml.ML Thu Aug 26 12:30:43 2010 +0200
2.2 +++ b/src/Tools/Code/code_ml.ML Thu Aug 26 13:50:58 2010 +0200
2.3 @@ -722,9 +722,8 @@
2.4
2.5 in
2.6
2.7 -fun ml_node_of_program labelled_name module_name reserved raw_module_alias program =
2.8 +fun ml_node_of_program labelled_name module_name reserved module_alias program =
2.9 let
2.10 - val module_alias = if is_some module_name then K module_name else raw_module_alias;
2.11 val reserved = Name.make_context reserved;
2.12 val empty_module = ((reserved, reserved), Graph.empty);
2.13 fun map_node [] f = f
2.14 @@ -907,15 +906,14 @@
2.15 error ("Unknown statement name: " ^ labelled_name name);
2.16 in (deresolver, nodes) end;
2.17
2.18 -fun serialize_ml target print_module print_stmt raw_module_name with_signatures labelled_name
2.19 - reserved includes raw_module_alias _ syntax_tyco syntax_const (code_of_pretty, code_writeln) program stmt_names destination =
2.20 +fun serialize_ml target print_module print_stmt module_name with_signatures labelled_name
2.21 + reserved includes module_alias _ syntax_tyco syntax_const (code_of_pretty, code_writeln) program
2.22 + (stmt_names, presentation_stmt_names) =
2.23 let
2.24 val is_cons = Code_Thingol.is_cons program;
2.25 - val presentation_stmt_names = Code_Target.stmt_names_of_destination destination;
2.26 val is_presentation = not (null presentation_stmt_names);
2.27 - val module_name = if is_presentation then SOME "Code" else raw_module_name;
2.28 val (deresolver, nodes) = ml_node_of_program labelled_name module_name
2.29 - reserved raw_module_alias program;
2.30 + reserved module_alias program;
2.31 val reserved = make_vars reserved;
2.32 fun print_node prefix (Dummy _) =
2.33 NONE
2.34 @@ -939,7 +937,7 @@
2.35 in
2.36 Code_Target.mk_serialization target
2.37 (fn NONE => code_writeln | SOME file => File.write file o code_of_pretty)
2.38 - (rpair stmt_names' o code_of_pretty) p destination
2.39 + (rpair stmt_names' o code_of_pretty) p
2.40 end;
2.41
2.42 end; (*local*)
3.1 --- a/src/Tools/Code/code_scala.ML Thu Aug 26 12:30:43 2010 +0200
3.2 +++ b/src/Tools/Code/code_scala.ML Thu Aug 26 13:50:58 2010 +0200
3.3 @@ -293,11 +293,10 @@
3.4
3.5 in
3.6
3.7 -fun scala_program_of_program labelled_name module_name reserved raw_module_alias program =
3.8 +fun scala_program_of_program labelled_name reserved module_alias program =
3.9 let
3.10
3.11 (* building module name hierarchy *)
3.12 - val module_alias = if is_some module_name then K module_name else raw_module_alias;
3.13 fun alias_fragments name = case module_alias name
3.14 of SOME name' => Long_Name.explode name'
3.15 | NONE => map (fn name => fst (yield_singleton Name.variants name reserved))
3.16 @@ -403,20 +402,15 @@
3.17
3.18 in (deresolve, sca_program) end;
3.19
3.20 -fun serialize_scala raw_module_name labelled_name
3.21 - raw_reserved includes raw_module_alias
3.22 +fun serialize_scala labelled_name raw_reserved includes module_alias
3.23 _ syntax_tyco syntax_const (code_of_pretty, code_writeln)
3.24 - program stmt_names destination =
3.25 + program (stmt_names, presentation_stmt_names) destination =
3.26 let
3.27
3.28 - (* generic nonsense *)
3.29 - val presentation_stmt_names = Code_Target.stmt_names_of_destination destination;
3.30 - val module_name = if null presentation_stmt_names then raw_module_name else SOME "Code";
3.31 -
3.32 (* preprocess program *)
3.33 val reserved = fold (insert (op =) o fst) includes raw_reserved;
3.34 val (deresolve, sca_program) = scala_program_of_program labelled_name
3.35 - module_name (Name.make_context reserved) raw_module_alias program;
3.36 + (Name.make_context reserved) module_alias program;
3.37
3.38 (* print statements *)
3.39 fun lookup_constr tyco constr = case Graph.get_node program tyco
3.40 @@ -498,9 +492,9 @@
3.41
3.42 (** Isar setup **)
3.43
3.44 -fun isar_serializer module_name =
3.45 +fun isar_serializer _ =
3.46 Code_Target.parse_args (Scan.succeed ())
3.47 - #> (fn () => serialize_scala module_name);
3.48 + #> (fn () => serialize_scala);
3.49
3.50 val setup =
3.51 Code_Target.add_target
4.1 --- a/src/Tools/Code/code_target.ML Thu Aug 26 12:30:43 2010 +0200
4.2 +++ b/src/Tools/Code/code_target.ML Thu Aug 26 13:50:58 2010 +0200
4.3 @@ -111,7 +111,7 @@
4.4 -> (string -> Code_Printer.activated_const_syntax option)
4.5 -> ((Pretty.T -> string) * (Pretty.T -> unit))
4.6 -> Code_Thingol.program
4.7 - -> string list (*selected statements*)
4.8 + -> (string list * string list) (*selected statements*)
4.9 -> serialization;
4.10
4.11 datatype description = Fundamental of { serializer: serializer, literals: Code_Printer.literals,
4.12 @@ -254,7 +254,7 @@
4.13 |>> map_filter I;
4.14
4.15 fun invoke_serializer thy abortable serializer literals reserved abs_includes
4.16 - module_alias class instance tyco const module width args naming program2 names1 =
4.17 + module_alias class instance tyco const module_name width args naming program2 (names1, presentation_names) =
4.18 let
4.19 val (names_class, class') =
4.20 activate_syntax (Code_Thingol.lookup_class naming) class;
4.21 @@ -275,14 +275,14 @@
4.22 val _ = if null empty_funs then () else error ("No code equations for "
4.23 ^ commas (map (Sign.extern_const thy) empty_funs));
4.24 in
4.25 - serializer module args (Code_Thingol.labelled_name thy program2) reserved includes
4.26 - (Symtab.lookup module_alias) (Symtab.lookup class')
4.27 - (Symtab.lookup tyco') (Symtab.lookup const')
4.28 + serializer module_name args (Code_Thingol.labelled_name thy program2) reserved includes
4.29 + (if is_some module_name then K module_name else Symtab.lookup module_alias)
4.30 + (Symtab.lookup class') (Symtab.lookup tyco') (Symtab.lookup const')
4.31 (Code_Printer.string_of_pretty width, Code_Printer.writeln_pretty width)
4.32 - program4 names1
4.33 + program4 (names1, presentation_names)
4.34 end;
4.35
4.36 -fun mount_serializer thy alt_serializer target some_width module args naming program names =
4.37 +fun mount_serializer thy alt_serializer target some_width raw_module_name args naming program names destination =
4.38 let
4.39 val ((targets, abortable), default_width) = Targets.get thy;
4.40 fun collapse_hierarchy target =
4.41 @@ -299,6 +299,9 @@
4.42 val (modify, data) = collapse_hierarchy target;
4.43 val serializer = the_default (case the_description data
4.44 of Fundamental seri => #serializer seri) alt_serializer;
4.45 + val presentation_names = stmt_names_of_destination destination;
4.46 + val module_name = if null presentation_names
4.47 + then raw_module_name else SOME "Code";
4.48 val reserved = the_reserved data;
4.49 fun select_include names_all (name, (content, cs)) =
4.50 if null cs then SOME (name, content)
4.51 @@ -308,13 +311,14 @@
4.52 then SOME (name, content) else NONE;
4.53 fun includes names_all = map_filter (select_include names_all)
4.54 ((Symtab.dest o the_includes) data);
4.55 - val module_alias = the_module_alias data;
4.56 + val module_alias = the_module_alias data
4.57 val { class, instance, tyco, const } = the_name_syntax data;
4.58 val literals = the_literals thy target;
4.59 val width = the_default default_width some_width;
4.60 in
4.61 invoke_serializer thy abortable serializer literals reserved
4.62 - includes module_alias class instance tyco const module width args naming (modify program) names
4.63 + includes module_alias class instance tyco const module_name width args
4.64 + naming (modify program) (names, presentation_names) destination
4.65 end;
4.66
4.67 in