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; |