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@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@39208: -> 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@39017: | Stmt of '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@55150: cyclic_modules: bool, empty_data: 'b, memorize_data: Code_Symbol.T -> 'b -> 'b, haftmann@55150: modify_stmts: (Code_Symbol.T * Code_Thingol.stmt) list -> 'a option list } haftmann@38970: -> 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@55150: print_stmt: string list -> Code_Symbol.T * '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@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@55291: fun build_module_namespace ctxt { 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@55291: in haftmann@55291: fold (fn name => Symtab.update (name, 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@55150: type flat_program = ((string * 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@52138: identifiers, empty_nsp, namify_stmt, modify_stmt } program = haftmann@39208: let haftmann@39208: haftmann@39208: (* building module name hierarchy *) haftmann@55291: val module_namespace = build_module_namespace ctxt { 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@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@55147: #> (Graph.map_node module_name o apfst) (Code_Symbol.Graph.new_node (sym, (base, 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@55147: else (Graph.map_node module_name o apsnd) (AList.map_default (op =) (module_name', []) (insert (op =) sym')) haftmann@39208: end; haftmann@55292: val proto_program = build_proto_program haftmann@55292: { empty = Graph.empty, add_stmt = add_stmt, add_dep = add_dep } program; haftmann@39208: haftmann@39208: (* name declarations and statement modifications *) haftmann@55147: 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@55147: |> (Code_Symbol.Graph.map o K o apsnd) modify_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@39017: | Stmt of '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@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@55147: fun hierarchical_program ctxt { module_name, reserved, identifiers, empty_nsp, haftmann@39023: namify_module, namify_stmt, cyclic_modules, empty_data, memorize_data, modify_stmts } program = haftmann@38970: let haftmann@38970: haftmann@38970: (* building module name hierarchy *) haftmann@55291: val module_namespace = build_module_namespace ctxt { 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@55147: fun add_stmt sym stmt = haftmann@38970: let haftmann@55147: val (name_fragments, base) = prep_sym sym; haftmann@38970: in haftmann@55147: (map_module name_fragments o apsnd) (Code_Symbol.Graph.new_node (sym, (base, Stmt stmt))) haftmann@38970: end; 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@39023: val is_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@38970: val add_edge = if is_module andalso not cyclic_modules haftmann@55147: then (fn node => Code_Symbol.Graph.add_edge_acyclic dep node haftmann@38970: handle Graph.CYCLES _ => error ("Dependency " haftmann@55147: ^ Code_Symbol.quote ctxt sym ^ " -> " haftmann@55147: ^ Code_Symbol.quote ctxt sym' haftmann@38970: ^ " would result in module dependency cycle")) haftmann@55147: else Code_Symbol.Graph.add_edge dep haftmann@39018: in (map_module name_fragments_common o apsnd) add_edge end; haftmann@55292: val proto_program = build_proto_program haftmann@55292: { empty = empty_program, add_stmt = add_stmt, add_dep = add_dep } program; 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@55147: |> fold (declare (namify_stmt o (fn Stmt stmt => stmt))) stmt_syms; haftmann@39029: fun zip_fillup xs ys = xs ~~ ys @ replicate (length xs - length ys) NONE; haftmann@55147: fun select_syms syms = case filter (member (op =) stmt_syms) syms haftmann@39029: of [] => NONE haftmann@55147: | syms => SOME syms; haftmann@55147: val modify_stmts' = AList.make (snd o Code_Symbol.Graph.get_node nodes) haftmann@39023: #> split_list haftmann@39023: ##> map (fn Stmt stmt => stmt) haftmann@55147: #> (fn (syms, stmts) => zip_fillup syms (modify_stmts (syms ~~ stmts))); haftmann@55147: val stmtss' = (maps modify_stmts' o map_filter select_syms o Code_Symbol.Graph.strong_conn) nodes; haftmann@55147: val nodes'' = Code_Symbol.Graph.map (fn sym => apsnd (fn Module content => Module (make_declarations nsps' content) haftmann@55147: | _ => case AList.lookup (op =) stmtss' sym of SOME (SOME stmt) => Stmt stmt | _ => Dummy)) nodes'; 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;