# HG changeset patch # User haftmann # Date 1283627680 -7200 # Node ID b6530978c14de4a36480c24e397eb583a43c0065 # Parent 142f1425e0747dbd1d3a472cad1bf61911b16a5d# Parent 3c284a152bd671ba1720468a46a93a86d049913d merged diff -r 142f1425e074 -r b6530978c14d src/Tools/Code/code_ml.ML --- 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 diff -r 142f1425e074 -r b6530978c14d src/Tools/Code/code_namespace.ML --- 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 diff -r 142f1425e074 -r b6530978c14d src/Tools/Code/code_scala.ML --- 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