--- a/src/Tools/Code/code_ml.ML Sat Sep 04 21:12:42 2010 +0200
+++ b/src/Tools/Code/code_ml.ML Sat Sep 04 21:14:40 2010 +0200
@@ -785,31 +785,33 @@
cyclic_modules = false, empty_data = (), memorize_data = K I, modify_stmts = modify_stmts } program
end;
-fun serialize_ml target print_module print_stmt with_signatures
+fun serialize_ml target print_ml_module print_ml_stmt with_signatures
{ labelled_name, reserved_syms, includes, module_alias,
class_syntax, tyco_syntax, const_syntax, program } =
let
- val is_cons = Code_Thingol.is_cons program;
+
+ (* build program *)
val { deresolver, hierarchical_program = ml_program } =
ml_program_of_program labelled_name (Name.make_context reserved_syms) module_alias program;
- val print_stmt = print_stmt labelled_name tyco_syntax const_syntax
- (make_vars reserved_syms) is_cons;
- fun print_node _ (_, Code_Namespace.Dummy) =
- NONE
- | print_node prefix_fragments (name, Code_Namespace.Stmt stmt) =
- SOME (apsnd (markup_stmt name) (print_stmt (deresolver prefix_fragments) stmt))
- | print_node prefix_fragments (name_fragment, Code_Namespace.Module (_, nodes)) =
- let
- val (decls, body) = print_nodes (prefix_fragments @ [name_fragment]) nodes;
- val p = print_module name_fragment
- (if with_signatures then SOME decls else NONE) body;
- in SOME ([], p) end
- and print_nodes prefix_fragments nodes = (map_filter
- (fn name => print_node prefix_fragments (name, snd (Graph.get_node nodes name)))
- o rev o flat o Graph.strong_conn) nodes
- |> split_list
- |> (fn (decls, body) => (flat decls, body))
- val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] ml_program));
+
+ (* print statements *)
+ fun print_stmt prefix_fragments (_, stmt) = print_ml_stmt
+ labelled_name tyco_syntax const_syntax (make_vars reserved_syms)
+ (Code_Thingol.is_cons program) (deresolver prefix_fragments) stmt
+ |> apfst SOME;
+
+ (* print modules *)
+ fun print_module prefix_fragments base _ xs =
+ let
+ val (raw_decls, body) = split_list xs;
+ val decls = if with_signatures then SOME (maps these raw_decls) else NONE
+ in (NONE, print_ml_module base decls body) end;
+
+ (* serialization *)
+ val p = Pretty.chunks2 (map snd includes
+ @ map snd (Code_Namespace.print_hierarchical {
+ print_module = print_module, print_stmt = print_stmt,
+ lift_markup = apsnd } ml_program));
fun write width NONE = writeln o format [] width
| write width (SOME p) = File.write p o format [] width;
in
--- a/src/Tools/Code/code_namespace.ML Sat Sep 04 21:12:42 2010 +0200
+++ b/src/Tools/Code/code_namespace.ML Sat Sep 04 21:14:40 2010 +0200
@@ -10,7 +10,8 @@
datatype ('a, 'b) node =
Dummy
| Stmt of 'a
- | Module of ('b * (string * ('a, 'b) node) Graph.T);
+ | Module of ('b * (string * ('a, 'b) node) Graph.T)
+ type ('a, 'b) hierarchical_program = (string * ('a, 'b) node) Graph.T
val hierarchical_program: (string -> string) -> { module_alias: string -> string option,
reserved: Name.context, empty_nsp: 'c, namify_module: string -> 'c -> string * 'c,
namify_stmt: Code_Thingol.stmt -> string -> 'c -> string * 'c,
@@ -18,7 +19,11 @@
modify_stmts: (string * Code_Thingol.stmt) list -> 'a option list }
-> Code_Thingol.program
-> { deresolver: string list -> string -> string,
- hierarchical_program: (string * ('a, 'b) node) Graph.T }
+ hierarchical_program: ('a, 'b) hierarchical_program }
+ val print_hierarchical: { print_module: string list -> string -> 'b -> 'c list -> 'c,
+ print_stmt: string list -> string * 'a -> 'c,
+ lift_markup: (Pretty.T -> Pretty.T) -> 'c -> 'c }
+ -> ('a, 'b) hierarchical_program -> 'c list
end;
structure Code_Namespace : CODE_NAMESPACE =
@@ -37,6 +42,8 @@
| Stmt of 'a
| Module of ('b * (string * ('a, 'b) node) Graph.T);
+type ('a, 'b) hierarchical_program = (string * ('a, 'b) node) Graph.T;
+
fun map_module_content f (Module content) = Module (f content);
fun map_module [] = I
@@ -140,4 +147,25 @@
in { deresolver = deresolver, hierarchical_program = hierarchical_program } end;
+fun print_hierarchical { print_module, print_stmt, lift_markup } =
+ let
+ fun print_node _ (_, Dummy) =
+ NONE
+ | print_node prefix_fragments (name, Stmt stmt) =
+ SOME (lift_markup (Code_Printer.markup_stmt name)
+ (print_stmt prefix_fragments (name, stmt)))
+ | print_node prefix_fragments (name_fragment, Module (data, nodes)) =
+ let
+ val prefix_fragments' = prefix_fragments @ [name_fragment]
+ in
+ Option.map (print_module prefix_fragments'
+ name_fragment data) (print_nodes prefix_fragments' nodes)
+ end
+ and print_nodes prefix_fragments nodes =
+ let
+ val xs = (map_filter (fn name => print_node prefix_fragments
+ (name, snd (Graph.get_node nodes name))) o rev o flat o Graph.strong_conn) nodes
+ in if null xs then NONE else SOME xs end;
+ in these o print_nodes [] end;
+
end;
\ No newline at end of file
--- a/src/Tools/Code/code_scala.ML Sat Sep 04 21:12:42 2010 +0200
+++ b/src/Tools/Code/code_scala.ML Sat Sep 04 21:14:40 2010 +0200
@@ -333,7 +333,7 @@
let
(* build program *)
- val { deresolver, hierarchical_program = sca_program } =
+ val { deresolver, hierarchical_program = scala_program } =
scala_program_of_program labelled_name (Name.make_context reserved_syms) module_alias program;
(* print statements *)
@@ -353,38 +353,27 @@
fun is_singleton_constr c = case Graph.get_node program c
of Code_Thingol.Datatypecons (_, tyco) => null (lookup_constr tyco c)
| _ => false;
- val print_stmt = print_scala_stmt labelled_name tyco_syntax const_syntax
- (make_vars reserved_syms) args_num is_singleton_constr;
+ fun print_stmt prefix_fragments = print_scala_stmt labelled_name
+ tyco_syntax const_syntax (make_vars reserved_syms) args_num
+ is_singleton_constr (deresolver prefix_fragments, deresolver []);
- (* print nodes *)
- fun print_module base implicit_ps p = Pretty.chunks2
- ([str ("object " ^ base ^ " {")]
- @ (if null implicit_ps then [] else (single o Pretty.block)
- (str "import /*implicits*/" :: Pretty.brk 1 :: commas implicit_ps))
- @ [p, str ("} /* object " ^ base ^ " */")]);
+ (* print modules *)
fun print_implicit prefix_fragments implicit =
let
val s = deresolver prefix_fragments implicit;
in if length (Long_Name.explode s) = 1 then NONE else SOME (str s) end;
- fun print_node _ (_, Code_Namespace.Dummy) = NONE
- | print_node prefix_fragments (name, Code_Namespace.Stmt stmt) =
- SOME (markup_stmt name (print_stmt (deresolver prefix_fragments, deresolver []) (name, stmt)))
- | print_node prefix_fragments (name_fragment, Code_Namespace.Module (implicits, nodes)) =
- let
- val prefix_fragments' = prefix_fragments @ [name_fragment];
- in
- Option.map (print_module name_fragment
- (map_filter (print_implicit prefix_fragments') implicits))
- (print_nodes prefix_fragments' nodes)
- end
- and print_nodes prefix_fragments nodes = let
- val ps = map_filter (fn name => print_node prefix_fragments (name,
- snd (Graph.get_node nodes name)))
- ((rev o flat o Graph.strong_conn) nodes);
- in if null ps then NONE else SOME (Pretty.chunks2 ps) end;
+ fun print_module prefix_fragments base implicits ps = Pretty.chunks2
+ ([str ("object " ^ base ^ " {")]
+ @ (case map_filter (print_implicit prefix_fragments) implicits
+ of [] => [] | implicit_ps => (single o Pretty.block)
+ (str "import /*implicits*/" :: Pretty.brk 1 :: commas implicit_ps))
+ @ ps @ [str ("} /* object " ^ base ^ " */")]);
(* serialization *)
- val p = Pretty.chunks2 (map snd includes @ the_list (print_nodes [] sca_program));
+ val p = Pretty.chunks2 (map snd includes
+ @ Code_Namespace.print_hierarchical {
+ print_module = print_module, print_stmt = print_stmt,
+ lift_markup = I } scala_program);
fun write width NONE = writeln o format [] width
| write width (SOME p) = File.write p o format [] width;
in