src/Tools/Code/code_ml.ML
changeset 39148 b6530978c14d
parent 39142 f63715f00fdd
parent 39147 3c284a152bd6
child 40627 becf5d5187cc
equal deleted inserted replaced
39146:142f1425e074 39148:b6530978c14d
   783     Code_Namespace.hierarchical_program labelled_name { module_alias = module_alias, reserved = reserved,
   783     Code_Namespace.hierarchical_program labelled_name { module_alias = module_alias, reserved = reserved,
   784       empty_nsp = (reserved, reserved), namify_module = pair, namify_stmt = namify_stmt,
   784       empty_nsp = (reserved, reserved), namify_module = pair, namify_stmt = namify_stmt,
   785       cyclic_modules = false, empty_data = (), memorize_data = K I, modify_stmts = modify_stmts } program
   785       cyclic_modules = false, empty_data = (), memorize_data = K I, modify_stmts = modify_stmts } program
   786   end;
   786   end;
   787 
   787 
   788 fun serialize_ml target print_module print_stmt with_signatures
   788 fun serialize_ml target print_ml_module print_ml_stmt with_signatures
   789     { labelled_name, reserved_syms, includes, module_alias,
   789     { labelled_name, reserved_syms, includes, module_alias,
   790       class_syntax, tyco_syntax, const_syntax, program } =
   790       class_syntax, tyco_syntax, const_syntax, program } =
   791   let
   791   let
   792     val is_cons = Code_Thingol.is_cons program;
   792 
       
   793     (* build program *)
   793     val { deresolver, hierarchical_program = ml_program } =
   794     val { deresolver, hierarchical_program = ml_program } =
   794       ml_program_of_program labelled_name (Name.make_context reserved_syms) module_alias program;
   795       ml_program_of_program labelled_name (Name.make_context reserved_syms) module_alias program;
   795     val print_stmt = print_stmt labelled_name tyco_syntax const_syntax
   796 
   796       (make_vars reserved_syms) is_cons;
   797     (* print statements *)
   797     fun print_node _ (_, Code_Namespace.Dummy) =
   798     fun print_stmt prefix_fragments (_, stmt) = print_ml_stmt
   798           NONE
   799       labelled_name tyco_syntax const_syntax (make_vars reserved_syms)
   799       | print_node prefix_fragments (name, Code_Namespace.Stmt stmt) =
   800       (Code_Thingol.is_cons program) (deresolver prefix_fragments) stmt
   800           SOME (apsnd (markup_stmt name) (print_stmt (deresolver prefix_fragments) stmt))
   801       |> apfst SOME;
   801       | print_node prefix_fragments (name_fragment, Code_Namespace.Module (_, nodes)) =
   802 
   802           let
   803     (* print modules *)
   803             val (decls, body) = print_nodes (prefix_fragments @ [name_fragment]) nodes;
   804     fun print_module prefix_fragments base _ xs =
   804             val p = print_module name_fragment
   805       let
   805                 (if with_signatures then SOME decls else NONE) body;
   806         val (raw_decls, body) = split_list xs;
   806           in SOME ([], p) end
   807         val decls = if with_signatures then SOME (maps these raw_decls) else NONE 
   807     and print_nodes prefix_fragments nodes = (map_filter
   808       in (NONE, print_ml_module base decls body) end;
   808         (fn name => print_node prefix_fragments (name, snd (Graph.get_node nodes name)))
   809 
   809         o rev o flat o Graph.strong_conn) nodes
   810     (* serialization *)
   810       |> split_list
   811     val p = Pretty.chunks2 (map snd includes
   811       |> (fn (decls, body) => (flat decls, body))
   812       @ map snd (Code_Namespace.print_hierarchical {
   812     val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] ml_program));
   813         print_module = print_module, print_stmt = print_stmt,
       
   814         lift_markup = apsnd } ml_program));
   813     fun write width NONE = writeln o format [] width
   815     fun write width NONE = writeln o format [] width
   814       | write width (SOME p) = File.write p o format [] width;
   816       | write width (SOME p) = File.write p o format [] width;
   815   in
   817   in
   816     Code_Target.serialization write (rpair (try (deresolver [])) ooo format) p
   818     Code_Target.serialization write (rpair (try (deresolver [])) ooo format) p
   817   end;
   819   end;