haftmann@38970: (* Title: Tools/Code/code_namespace.ML haftmann@38970: Author: Florian Haftmann, TU Muenchen haftmann@38970: haftmann@38970: Mastering target language namespaces. haftmann@38970: *) haftmann@38970: haftmann@38970: signature CODE_NAMESPACE = haftmann@38970: sig haftmann@55681: datatype export = Private | Opaque | Public haftmann@55681: val is_public: export -> bool haftmann@55681: val not_private: export -> bool haftmann@55684: val join_exports: export list -> export haftmann@55681: haftmann@39208: type flat_program haftmann@55147: val flat_program: Proof.context haftmann@52138: -> { module_prefix: string, module_name: string, haftmann@52138: reserved: Name.context, identifiers: Code_Target.identifier_data, empty_nsp: 'a, haftmann@39208: namify_stmt: Code_Thingol.stmt -> string -> 'a -> string * 'a, haftmann@39208: modify_stmt: Code_Thingol.stmt -> Code_Thingol.stmt option } haftmann@55683: -> Code_Symbol.T list -> Code_Thingol.program haftmann@55150: -> { deresolver: string -> Code_Symbol.T -> string, haftmann@39208: flat_program: flat_program } haftmann@39208: haftmann@39017: datatype ('a, 'b) node = haftmann@38970: Dummy haftmann@55681: | Stmt of export * 'a haftmann@55147: | Module of ('b * (string * ('a, 'b) node) Code_Symbol.Graph.T) haftmann@39208: type ('a, 'b) hierarchical_program haftmann@55147: val hierarchical_program: Proof.context haftmann@52138: -> { module_name: string, haftmann@52138: reserved: Name.context, identifiers: Code_Target.identifier_data, haftmann@52138: empty_nsp: 'c, namify_module: string -> 'c -> string * 'c, haftmann@39022: namify_stmt: Code_Thingol.stmt -> string -> 'c -> string * 'c, haftmann@55684: cyclic_modules: bool, haftmann@55684: class_transitive: bool, class_relation_public: bool, haftmann@55684: empty_data: 'b, memorize_data: Code_Symbol.T -> 'b -> 'b, haftmann@55684: modify_stmts: (Code_Symbol.T * (export * Code_Thingol.stmt)) list -> (export * 'a) option list } haftmann@55683: -> Code_Symbol.T list -> Code_Thingol.program haftmann@55150: -> { deresolver: string list -> Code_Symbol.T -> string, haftmann@39147: hierarchical_program: ('a, 'b) hierarchical_program } haftmann@39147: val print_hierarchical: { print_module: string list -> string -> 'b -> 'c list -> 'c, haftmann@55681: print_stmt: string list -> Code_Symbol.T * (export * 'a) -> 'c, haftmann@39147: lift_markup: (Pretty.T -> Pretty.T) -> 'c -> 'c } haftmann@39147: -> ('a, 'b) hierarchical_program -> 'c list haftmann@38970: end; haftmann@38970: haftmann@38970: structure Code_Namespace : CODE_NAMESPACE = haftmann@38970: struct haftmann@38970: haftmann@55681: (** export **) haftmann@55681: haftmann@55681: datatype export = Private | Opaque | Public; haftmann@55681: haftmann@55681: fun is_public Public = true haftmann@55681: | is_public _ = false; haftmann@55681: haftmann@55681: fun not_private Public = true haftmann@55681: | not_private Opaque = true haftmann@55681: | not_private _ = false; haftmann@55681: haftmann@55684: fun mark_export Public _ = Public haftmann@55684: | mark_export _ Public = Public haftmann@55684: | mark_export Opaque _ = Opaque haftmann@55684: | mark_export _ Opaque = Opaque haftmann@55684: | mark_export _ _ = Private; haftmann@55684: haftmann@55684: fun join_exports exports = fold mark_export exports Private; haftmann@55684: haftmann@55684: fun dependent_exports { program = program, class_transitive = class_transitive } = haftmann@55684: let haftmann@55684: fun is_datatype_or_class (Code_Symbol.Type_Constructor _) = true haftmann@55684: | is_datatype_or_class (Code_Symbol.Type_Class _) = true haftmann@55684: | is_datatype_or_class _ = false; haftmann@55684: fun is_relevant (Code_Symbol.Class_Relation _) = true haftmann@55684: | is_relevant sym = is_datatype_or_class sym; haftmann@55684: val proto_gr = Code_Symbol.Graph.restrict is_relevant program; haftmann@55684: val gr = haftmann@55684: proto_gr haftmann@55684: |> Code_Symbol.Graph.fold haftmann@55684: (fn (sym, (_, (_, deps))) => haftmann@55684: if is_relevant sym haftmann@55684: then I haftmann@55684: else haftmann@55684: Code_Symbol.Graph.new_node (sym, Code_Thingol.NoStmt) haftmann@55684: #> Code_Symbol.Graph.Keys.fold haftmann@55684: (fn sym' => haftmann@55684: if is_relevant sym' haftmann@55684: then Code_Symbol.Graph.add_edge (sym, sym') haftmann@55684: else I) deps) program haftmann@55684: |> class_transitive ? haftmann@55684: Code_Symbol.Graph.fold (fn (sym as Code_Symbol.Type_Class _, _) => haftmann@55684: fold (curry Code_Symbol.Graph.add_edge sym) haftmann@55684: ((remove (op =) sym o Code_Symbol.Graph.all_succs proto_gr) [sym]) | _ => I) proto_gr haftmann@55684: fun deps_of sym = haftmann@55684: let haftmann@55684: val succs = Code_Symbol.Graph.Keys.dest o Code_Symbol.Graph.imm_succs gr; haftmann@55684: val deps1 = succs sym; haftmann@55776: val deps2 = [] |> fold (union (op =)) (map succs deps1) |> subtract (op =) deps1 haftmann@55684: in (deps1, deps2) end; haftmann@55684: in haftmann@55684: { is_datatype_or_class = is_datatype_or_class, haftmann@55684: deps_of = deps_of } haftmann@55684: end; haftmann@55684: haftmann@55684: fun mark_exports_aux { program = program, prefix_of = prefix_of, map_export = map_export, haftmann@55684: is_datatype_or_class = is_datatype_or_class, deps_of = deps_of, haftmann@55684: class_relation_public = class_relation_public } prefix sym = haftmann@55684: let haftmann@55684: val export = (if is_datatype_or_class sym then Opaque else Public); haftmann@55684: val (dependent_export1, dependent_export2) = haftmann@55684: case Code_Symbol.Graph.get_node program sym of haftmann@55684: Code_Thingol.Fun _ => (SOME Opaque, NONE) haftmann@55684: | Code_Thingol.Classinst _ => (SOME Opaque, NONE) haftmann@55684: | Code_Thingol.Datatypecons _ => (SOME Public, SOME Opaque) haftmann@55684: | Code_Thingol.Classparam _ => (SOME Public, SOME Opaque) haftmann@55776: | Code_Thingol.Class _ => (SOME Opaque, NONE) haftmann@55684: | Code_Thingol.Classrel _ => haftmann@55684: (if class_relation_public haftmann@55684: then (SOME Public, SOME Opaque) haftmann@55684: else (SOME Opaque, NONE)) haftmann@55684: | _ => (NONE, NONE); haftmann@55684: val dependent_exports = haftmann@55684: case dependent_export1 of haftmann@55684: SOME export1 => (case dependent_export2 of haftmann@55684: SOME export2 => haftmann@55684: let haftmann@55684: val (deps1, deps2) = deps_of sym haftmann@55684: in map (rpair export1) deps1 @ map (rpair export2) deps2 end haftmann@55684: | NONE => map (rpair export1) (fst (deps_of sym))) haftmann@55684: | NONE => []; haftmann@55684: in haftmann@55684: map_export prefix sym (mark_export export) haftmann@55684: #> fold (fn (sym, export) => map_export (prefix_of sym) sym (mark_export export)) haftmann@55684: dependent_exports haftmann@55684: end; haftmann@55684: haftmann@55684: fun mark_exports { program = program, prefix_of = prefix_of, map_export = map_export, haftmann@55684: class_transitive = class_transitive, class_relation_public = class_relation_public } = haftmann@55684: let haftmann@55684: val { is_datatype_or_class, deps_of } = haftmann@55684: dependent_exports { program = program, class_transitive = class_transitive }; haftmann@55684: in haftmann@55684: mark_exports_aux { program = program, prefix_of = prefix_of, map_export = map_export, haftmann@55684: is_datatype_or_class = is_datatype_or_class, deps_of = deps_of, haftmann@55684: class_relation_public = class_relation_public } haftmann@55684: end; haftmann@55684: haftmann@55681: haftmann@52138: (** fundamental module name hierarchy **) haftmann@52138: haftmann@55291: fun module_fragments' { identifiers, reserved } name = haftmann@55291: case Code_Symbol.lookup_module_data identifiers name of haftmann@55291: SOME (fragments, _) => fragments haftmann@55291: | NONE => map (fn fragment => fst (Name.variant fragment reserved)) (Long_Name.explode name); haftmann@55291: haftmann@55291: fun module_fragments { module_name, identifiers, reserved } = haftmann@55291: if module_name = "" haftmann@55291: then module_fragments' { identifiers = identifiers, reserved = reserved } haftmann@55291: else K (Long_Name.explode module_name); haftmann@39055: haftmann@56826: fun build_module_namespace ctxt enforce_upper { module_prefix, module_name, identifiers, reserved } program = haftmann@55291: let haftmann@55291: val module_names = Code_Symbol.Graph.fold (insert (op =) o Code_Symbol.default_prefix ctxt o fst) program []; haftmann@55291: val module_fragments' = module_fragments haftmann@55291: { module_name = module_name, identifiers = identifiers, reserved = reserved }; haftmann@56826: val adjust_case = if enforce_upper then map (Name.enforce_case true) else I; haftmann@55291: in haftmann@56826: fold (fn name => Symtab.update (name, adjust_case (Long_Name.explode module_prefix @ module_fragments' name))) haftmann@55291: module_names Symtab.empty haftmann@55291: end; haftmann@55291: haftmann@55292: fun prep_symbol ctxt { module_namespace, force_module, identifiers } sym = haftmann@55291: case Code_Symbol.lookup identifiers sym of haftmann@55292: NONE => ((the o Symtab.lookup module_namespace o Code_Symbol.default_prefix ctxt) sym, haftmann@55292: Code_Symbol.default_base sym) haftmann@53414: | SOME prefix_name => if null force_module then prefix_name haftmann@53414: else (force_module, snd prefix_name); haftmann@39055: haftmann@55293: fun has_priority identifiers = is_some o Code_Symbol.lookup identifiers; haftmann@55293: haftmann@55292: fun build_proto_program { empty, add_stmt, add_dep } program = haftmann@55292: empty haftmann@55292: |> Code_Symbol.Graph.fold (fn (sym, (stmt, _)) => add_stmt sym stmt) program haftmann@55292: |> Code_Symbol.Graph.fold (fn (sym, (_, (_, syms))) => haftmann@55292: Code_Symbol.Graph.Keys.fold (add_dep sym) syms) program; haftmann@55292: haftmann@55293: fun prioritize has_priority = uncurry append o List.partition has_priority; haftmann@55293: haftmann@39055: haftmann@39208: (** flat program structure **) haftmann@39208: haftmann@55681: type flat_program = ((string * (export * Code_Thingol.stmt) option) Code_Symbol.Graph.T * (string * Code_Symbol.T list) list) Graph.T; haftmann@39208: haftmann@55147: fun flat_program ctxt { module_prefix, module_name, reserved, haftmann@55683: identifiers, empty_nsp, namify_stmt, modify_stmt } exports program = haftmann@39208: let haftmann@39208: haftmann@39208: (* building module name hierarchy *) haftmann@56826: val module_namespace = build_module_namespace ctxt true { module_prefix = module_prefix, haftmann@55291: module_name = module_name, identifiers = identifiers, reserved = reserved } program; haftmann@55292: val prep_sym = prep_symbol ctxt { module_namespace = module_namespace, haftmann@55292: force_module = Long_Name.explode module_name, identifiers = identifiers } haftmann@52138: #>> Long_Name.implode; haftmann@55293: val sym_priority = has_priority identifiers; haftmann@39208: haftmann@39208: (* distribute statements over hierarchy *) haftmann@55684: val mark_exports = mark_exports { program = program, prefix_of = fst o prep_sym, haftmann@55684: map_export = fn module_name => fn sym => haftmann@55684: Graph.map_node module_name o apfst o Code_Symbol.Graph.map_node sym o apsnd o apfst, haftmann@55684: class_transitive = false, class_relation_public = false }; haftmann@55147: fun add_stmt sym stmt = haftmann@39208: let haftmann@55147: val (module_name, base) = prep_sym sym; haftmann@39208: in haftmann@55147: Graph.default_node (module_name, (Code_Symbol.Graph.empty, [])) haftmann@55680: #> (Graph.map_node module_name o apfst) haftmann@55684: (Code_Symbol.Graph.new_node (sym, (base, (if null exports then Public else Private, stmt)))) haftmann@39208: end; haftmann@55292: fun add_dep sym sym' = haftmann@39208: let haftmann@55147: val (module_name, _) = prep_sym sym; haftmann@55147: val (module_name', _) = prep_sym sym'; haftmann@39208: in if module_name = module_name' haftmann@55147: then (Graph.map_node module_name o apfst) (Code_Symbol.Graph.add_edge (sym, sym')) haftmann@55680: else (Graph.map_node module_name o apsnd) haftmann@55680: (AList.map_default (op =) (module_name', []) (insert (op =) sym')) haftmann@55684: #> mark_exports module_name' sym' haftmann@39208: end; haftmann@55292: val proto_program = build_proto_program haftmann@55684: { empty = Graph.empty, add_stmt = add_stmt, add_dep = add_dep } program haftmann@55684: |> fold (fn sym => mark_exports ((fst o prep_sym) sym) sym) exports; haftmann@39208: haftmann@39208: (* name declarations and statement modifications *) haftmann@55679: fun declare sym (base, (_, stmt)) (gr, nsp) = haftmann@39208: let haftmann@39208: val (base', nsp') = namify_stmt stmt base nsp; haftmann@55147: val gr' = (Code_Symbol.Graph.map_node sym o apfst) (K base') gr; haftmann@39208: in (gr', nsp') end; haftmann@39208: fun declarations gr = (gr, empty_nsp) haftmann@55293: |> fold (fn sym => declare sym (Code_Symbol.Graph.get_node gr sym)) haftmann@55293: (prioritize sym_priority (Code_Symbol.Graph.keys gr)) haftmann@39208: |> fst haftmann@55680: |> Code_Symbol.Graph.map_strong_conn (fn syms_bases_exports_stmts => haftmann@55680: map snd syms_bases_exports_stmts haftmann@55680: |> (map o apsnd) (fn (export, stmt) => Option.map (pair export) (modify_stmt stmt))); haftmann@39208: val flat_program = proto_program haftmann@39208: |> (Graph.map o K o apfst) declarations; haftmann@39208: haftmann@39208: (* qualified and unqualified imports, deresolving *) haftmann@55147: fun base_deresolver sym = fst (Code_Symbol.Graph.get_node haftmann@55147: (fst (Graph.get_node flat_program (fst (prep_sym sym)))) sym); haftmann@39208: fun classify_names gr imports = haftmann@39208: let haftmann@39208: val import_tab = maps haftmann@55147: (fn (module_name, syms) => map (rpair module_name) syms) imports; haftmann@55147: val imported_syms = map fst import_tab; haftmann@55147: val here_syms = Code_Symbol.Graph.keys gr; haftmann@39208: in haftmann@55147: Code_Symbol.Table.empty haftmann@55147: |> fold (fn sym => Code_Symbol.Table.update (sym, base_deresolver sym)) here_syms haftmann@55147: |> fold (fn sym => Code_Symbol.Table.update (sym, haftmann@55147: Long_Name.append (the (AList.lookup (op =) import_tab sym)) haftmann@55147: (base_deresolver sym))) imported_syms haftmann@39208: end; haftmann@40630: val deresolver_tab = Symtab.make (AList.make haftmann@40630: (uncurry classify_names o Graph.get_node flat_program) haftmann@40630: (Graph.keys flat_program)); haftmann@55147: fun deresolver "" sym = haftmann@55147: Long_Name.append (fst (prep_sym sym)) (base_deresolver sym) haftmann@55147: | deresolver module_name sym = haftmann@55147: the (Code_Symbol.Table.lookup (the (Symtab.lookup deresolver_tab module_name)) sym) haftmann@52138: handle Option.Option => error ("Unknown statement name: " haftmann@55147: ^ Code_Symbol.quote ctxt sym); haftmann@39208: haftmann@39208: in { deresolver = deresolver, flat_program = flat_program } end; haftmann@39208: haftmann@39208: haftmann@39055: (** hierarchical program structure **) haftmann@38970: haftmann@39017: datatype ('a, 'b) node = haftmann@38970: Dummy haftmann@55681: | Stmt of export * 'a haftmann@55147: | Module of ('b * (string * ('a, 'b) node) Code_Symbol.Graph.T); haftmann@38970: haftmann@55147: type ('a, 'b) hierarchical_program = (string * ('a, 'b) node) Code_Symbol.Graph.T; haftmann@39147: haftmann@55679: fun the_stmt (Stmt (export, stmt)) = (export, stmt); haftmann@55679: haftmann@39018: fun map_module_content f (Module content) = Module (f content); haftmann@39018: haftmann@39018: fun map_module [] = I haftmann@39018: | map_module (name_fragment :: name_fragments) = haftmann@55147: apsnd o Code_Symbol.Graph.map_node (Code_Symbol.Module name_fragment) o apsnd o map_module_content haftmann@39018: o map_module name_fragments; haftmann@39018: haftmann@55680: fun map_module_stmts f_module f_stmts sym_base_nodes = haftmann@55680: let haftmann@55680: val some_modules = haftmann@55680: sym_base_nodes haftmann@55684: |> map (fn (_, (base, Module content)) => SOME (base, content) | _ => NONE) haftmann@55680: |> (burrow_options o map o apsnd) f_module; haftmann@55680: val some_export_stmts = haftmann@55680: sym_base_nodes haftmann@55680: |> map (fn (sym, (base, Stmt export_stmt)) => SOME ((sym, export_stmt), base) | _ => NONE) haftmann@55680: |> (burrow_options o burrow_fst) (fn [] => [] | xs => f_stmts xs) haftmann@55680: in haftmann@55680: map2 (fn SOME (base, content) => (K (base, Module content)) haftmann@55680: | NONE => fn SOME (some_export_stmt, base) => haftmann@55680: (base, case some_export_stmt of SOME export_stmt => Stmt export_stmt | NONE => Dummy)) haftmann@55680: some_modules some_export_stmts haftmann@55680: end; haftmann@55680: haftmann@55147: fun hierarchical_program ctxt { module_name, reserved, identifiers, empty_nsp, haftmann@55684: namify_module, namify_stmt, cyclic_modules, haftmann@55684: class_transitive, class_relation_public, haftmann@55684: empty_data, memorize_data, modify_stmts } haftmann@55683: exports program = haftmann@38970: let haftmann@38970: haftmann@38970: (* building module name hierarchy *) haftmann@56826: val module_namespace = build_module_namespace ctxt false { module_prefix = "", haftmann@55291: module_name = module_name, identifiers = identifiers, reserved = reserved } program; haftmann@55292: val prep_sym = prep_symbol ctxt { module_namespace = module_namespace, haftmann@55293: force_module = Long_Name.explode module_name, identifiers = identifiers } haftmann@55293: val sym_priority = has_priority identifiers; haftmann@38970: haftmann@38970: (* building empty module hierarchy *) haftmann@55147: val empty_module = (empty_data, Code_Symbol.Graph.empty); haftmann@38970: fun ensure_module name_fragment (data, nodes) = haftmann@55147: if can (Code_Symbol.Graph.get_node nodes) (Code_Symbol.Module name_fragment) then (data, nodes) haftmann@38970: else (data, haftmann@55147: nodes |> Code_Symbol.Graph.new_node (Code_Symbol.Module name_fragment, (name_fragment, Module empty_module))); haftmann@38970: fun allocate_module [] = I haftmann@38970: | allocate_module (name_fragment :: name_fragments) = haftmann@38970: ensure_module name_fragment haftmann@55147: #> (apsnd o Code_Symbol.Graph.map_node (Code_Symbol.Module name_fragment) o apsnd o map_module_content o allocate_module) name_fragments; haftmann@52138: val empty_program = haftmann@52138: empty_module haftmann@55291: |> Symtab.fold (fn (_, fragments) => allocate_module fragments) module_namespace haftmann@55147: |> Code_Symbol.Graph.fold (allocate_module o these o Option.map fst haftmann@55291: o Code_Symbol.lookup identifiers o fst) program; haftmann@38970: haftmann@38970: (* distribute statements over hierarchy *) haftmann@55684: val mark_exports = mark_exports { program = program, prefix_of = fst o prep_sym, haftmann@55684: map_export = fn name_fragments => fn sym => fn f => haftmann@55684: (map_module name_fragments o apsnd o Code_Symbol.Graph.map_node sym o apsnd) haftmann@55684: (fn Stmt (export, stmt) => Stmt (f export, stmt)), haftmann@55684: class_transitive = class_transitive, class_relation_public = class_relation_public }; haftmann@55147: fun add_stmt sym stmt = haftmann@38970: let haftmann@55147: val (name_fragments, base) = prep_sym sym; haftmann@38970: in haftmann@55680: (map_module name_fragments o apsnd) haftmann@55684: (Code_Symbol.Graph.new_node (sym, (base, Stmt (if null exports then Public else Private, stmt)))) haftmann@38970: end; haftmann@55680: fun add_edge_acyclic_error error_msg dep gr = haftmann@55680: Code_Symbol.Graph.add_edge_acyclic dep gr haftmann@57428: handle Code_Symbol.Graph.CYCLES _ => error (error_msg ()) haftmann@55292: fun add_dep sym sym' = haftmann@38970: let haftmann@55147: val (name_fragments, _) = prep_sym sym; haftmann@55147: val (name_fragments', _) = prep_sym sym'; haftmann@38970: val (name_fragments_common, (diff, diff')) = haftmann@38970: chop_prefix (op =) (name_fragments, name_fragments'); haftmann@55680: val is_cross_module = not (null diff andalso null diff'); haftmann@55147: val dep = pairself hd (map Code_Symbol.Module diff @ [sym], map Code_Symbol.Module diff' @ [sym']); haftmann@55680: val add_edge = if is_cross_module andalso not cyclic_modules haftmann@55680: then add_edge_acyclic_error (fn _ => "Dependency " haftmann@55680: ^ Code_Symbol.quote ctxt sym ^ " -> " haftmann@55680: ^ Code_Symbol.quote ctxt sym' haftmann@55680: ^ " would result in module dependency cycle") dep haftmann@55680: else Code_Symbol.Graph.add_edge dep; haftmann@55684: in haftmann@55684: (map_module name_fragments_common o apsnd) add_edge haftmann@55684: #> (if is_cross_module then mark_exports name_fragments' sym' else I) haftmann@55684: end; haftmann@55292: val proto_program = build_proto_program haftmann@55684: { empty = empty_program, add_stmt = add_stmt, add_dep = add_dep } program haftmann@55684: |> fold (fn sym => mark_exports ((fst o prep_sym) sym) sym) exports; haftmann@38970: haftmann@39022: (* name declarations, data and statement modifications *) haftmann@38970: fun make_declarations nsps (data, nodes) = haftmann@38970: let haftmann@55293: val (module_fragments, stmt_syms) = haftmann@55293: Code_Symbol.Graph.keys nodes haftmann@55293: |> List.partition haftmann@55293: (fn sym => case Code_Symbol.Graph.get_node nodes sym haftmann@55293: of (_, Module _) => true | _ => false) haftmann@55293: |> pairself (prioritize sym_priority) haftmann@55147: fun declare namify sym (nsps, nodes) = haftmann@38970: let haftmann@55147: val (base, node) = Code_Symbol.Graph.get_node nodes sym; haftmann@38970: val (base', nsps') = namify node base nsps; haftmann@55147: val nodes' = Code_Symbol.Graph.map_node sym (K (base', node)) nodes; haftmann@38970: in (nsps', nodes') end; haftmann@38970: val (nsps', nodes') = (nsps, nodes) haftmann@39022: |> fold (declare (K namify_module)) module_fragments haftmann@55679: |> fold (declare (namify_stmt o snd o the_stmt)) stmt_syms; haftmann@55680: fun modify_stmts' syms_stmts = haftmann@55605: let haftmann@55680: val stmts' = modify_stmts syms_stmts haftmann@55680: in stmts' @ replicate (length syms_stmts - length stmts') NONE end; haftmann@55680: val nodes'' = haftmann@55680: nodes' haftmann@55684: |> Code_Symbol.Graph.map_strong_conn (map_module_stmts (make_declarations nsps') modify_stmts'); haftmann@55147: val data' = fold memorize_data stmt_syms data; haftmann@39018: in (data', nodes'') end; haftmann@38970: val (_, hierarchical_program) = make_declarations empty_nsp proto_program; haftmann@38970: haftmann@38970: (* deresolving *) haftmann@55147: fun deresolver prefix_fragments sym = haftmann@38970: let haftmann@55147: val (name_fragments, _) = prep_sym sym; haftmann@38970: val (_, (_, remainder)) = chop_prefix (op =) (prefix_fragments, name_fragments); haftmann@55147: val nodes = fold (fn name_fragment => fn nodes => case Code_Symbol.Graph.get_node nodes (Code_Symbol.Module name_fragment) haftmann@38970: of (_, Module (_, nodes)) => nodes) name_fragments hierarchical_program; haftmann@55147: val (base', _) = Code_Symbol.Graph.get_node nodes sym; haftmann@38970: in Long_Name.implode (remainder @ [base']) end haftmann@55147: handle Code_Symbol.Graph.UNDEF _ => error ("Unknown statement name: " haftmann@55147: ^ Code_Symbol.quote ctxt sym); haftmann@38970: haftmann@38970: in { deresolver = deresolver, hierarchical_program = hierarchical_program } end; haftmann@38970: haftmann@39147: fun print_hierarchical { print_module, print_stmt, lift_markup } = haftmann@39147: let haftmann@39147: fun print_node _ (_, Dummy) = haftmann@39147: NONE haftmann@55147: | print_node prefix_fragments (sym, Stmt stmt) = haftmann@55147: SOME (lift_markup (Code_Printer.markup_stmt sym) haftmann@55147: (print_stmt prefix_fragments (sym, stmt))) haftmann@55147: | print_node prefix_fragments (Code_Symbol.Module name_fragment, Module (data, nodes)) = haftmann@39147: let haftmann@39147: val prefix_fragments' = prefix_fragments @ [name_fragment] haftmann@39147: in haftmann@39147: Option.map (print_module prefix_fragments' haftmann@39147: name_fragment data) (print_nodes prefix_fragments' nodes) haftmann@39147: end haftmann@39147: and print_nodes prefix_fragments nodes = haftmann@39147: let haftmann@55147: val xs = (map_filter (fn sym => print_node prefix_fragments haftmann@55147: (sym, snd (Code_Symbol.Graph.get_node nodes sym))) o rev o flat o Code_Symbol.Graph.strong_conn) nodes haftmann@39147: in if null xs then NONE else SOME xs end; haftmann@39147: in these o print_nodes [] end; haftmann@39147: haftmann@55147: end;