# HG changeset patch # User haftmann # Date 1391412199 -3600 # Node ID 82780e5f7622a2c390a8bcbbd5b582f79ae8c3dc # Parent 3951ced4156cad9c729d0cb80038aac626fea1c9 tuned storage of code identifiers diff -r 3951ced4156c -r 82780e5f7622 src/Tools/Code/code_namespace.ML --- a/src/Tools/Code/code_namespace.ML Mon Feb 03 17:55:50 2014 +0100 +++ b/src/Tools/Code/code_namespace.ML Mon Feb 03 08:23:19 2014 +0100 @@ -42,27 +42,32 @@ (** fundamental module name hierarchy **) -fun lookup_identifier identifiers sym = - Code_Symbol.lookup identifiers sym - |> Option.map (split_last o Long_Name.explode); +fun module_fragments' { identifiers, reserved } name = + case Code_Symbol.lookup_module_data identifiers name of + SOME (fragments, _) => fragments + | NONE => map (fn fragment => fst (Name.variant fragment reserved)) (Long_Name.explode name); + +fun module_fragments { module_name, identifiers, reserved } = + if module_name = "" + then module_fragments' { identifiers = identifiers, reserved = reserved } + else K (Long_Name.explode module_name); -fun force_identifier ctxt fragments_tab force_module identifiers sym = - case lookup_identifier identifiers sym of - NONE => ((the o Symtab.lookup fragments_tab o Code_Symbol.default_prefix ctxt) sym, Code_Symbol.default_base sym) +fun build_module_namespace ctxt { module_prefix, module_name, identifiers, reserved } program = + let + val module_names = Code_Symbol.Graph.fold (insert (op =) o Code_Symbol.default_prefix ctxt o fst) program []; + val module_fragments' = module_fragments + { module_name = module_name, identifiers = identifiers, reserved = reserved }; + in + fold (fn name => Symtab.update (name, Long_Name.explode module_prefix @ module_fragments' name)) + module_names Symtab.empty + end; + +fun prep_symbol ctxt module_namespace force_module identifiers sym = + case Code_Symbol.lookup identifiers sym of + NONE => ((the o Symtab.lookup module_namespace o Code_Symbol.default_prefix ctxt) sym, Code_Symbol.default_base sym) | SOME prefix_name => if null force_module then prefix_name else (force_module, snd prefix_name); -fun build_module_namespace ctxt { module_prefix, module_identifiers, reserved } program = - let - fun alias_fragments name = case module_identifiers name - of SOME name' => Long_Name.explode name' - | NONE => map (fn name => fst (Name.variant name reserved)) (Long_Name.explode name); - val module_names = Code_Symbol.Graph.fold (insert (op =) o Code_Symbol.default_prefix ctxt o fst) program []; - in - fold (fn name => Symtab.update (name, Long_Name.explode module_prefix @ alias_fragments name)) - module_names Symtab.empty - end; - (** flat program structure **) @@ -73,12 +78,9 @@ let (* building module name hierarchy *) - val module_identifiers = if module_name = "" - then Code_Symbol.lookup_module_data identifiers - else K (SOME module_name); - val fragments_tab = build_module_namespace ctxt { module_prefix = module_prefix, - module_identifiers = module_identifiers, reserved = reserved } program; - val prep_sym = force_identifier ctxt fragments_tab (Long_Name.explode module_name) identifiers + val module_namespace = build_module_namespace ctxt { module_prefix = module_prefix, + module_name = module_name, identifiers = identifiers, reserved = reserved } program; + val prep_sym = prep_symbol ctxt module_namespace (Long_Name.explode module_name) identifiers #>> Long_Name.implode; (* distribute statements over hierarchy *) @@ -165,12 +167,9 @@ let (* building module name hierarchy *) - val module_identifiers = if module_name = "" - then Code_Symbol.lookup_module_data identifiers - else K (SOME module_name); - val fragments_tab = build_module_namespace ctxt { module_prefix = "", - module_identifiers = module_identifiers, reserved = reserved } program; - val prep_sym = force_identifier ctxt fragments_tab (Long_Name.explode module_name) identifiers; + val module_namespace = build_module_namespace ctxt { module_prefix = "", + module_name = module_name, identifiers = identifiers, reserved = reserved } program; + val prep_sym = prep_symbol ctxt module_namespace (Long_Name.explode module_name) identifiers; (* building empty module hierarchy *) val empty_module = (empty_data, Code_Symbol.Graph.empty); @@ -184,9 +183,9 @@ #> (apsnd o Code_Symbol.Graph.map_node (Code_Symbol.Module name_fragment) o apsnd o map_module_content o allocate_module) name_fragments; val empty_program = empty_module - |> Symtab.fold (fn (_, fragments) => allocate_module fragments) fragments_tab + |> Symtab.fold (fn (_, fragments) => allocate_module fragments) module_namespace |> Code_Symbol.Graph.fold (allocate_module o these o Option.map fst - o lookup_identifier identifiers o fst) program; + o Code_Symbol.lookup identifiers o fst) program; (* distribute statements over hierarchy *) fun add_stmt sym stmt = diff -r 3951ced4156c -r 82780e5f7622 src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Mon Feb 03 17:55:50 2014 +0100 +++ b/src/Tools/Code/code_target.ML Mon Feb 03 08:23:19 2014 +0100 @@ -81,7 +81,8 @@ class * (string * 'c option) list, (class * class) * (string * 'd option) list, (class * string) * (string * 'e option) list, string * (string * 'f option) list) Code_Symbol.attr; -type identifier_data = (string, string, string, string, string, string) Code_Symbol.data; +type identifier_data = (string list * string, string list * string, string list * string, string list * string, + string list * string, string list * string) Code_Symbol.data; type tyco_syntax = Code_Printer.tyco_syntax; type raw_const_syntax = Code_Printer.raw_const_syntax; @@ -144,7 +145,7 @@ val y' = Name.desymbolize false y; in ys' @ [y'] end; in if xs' = xs - then s + then if is_module then (xs, "") else split_last xs else error ("Invalid code name: " ^ quote s ^ "\n" ^ "better try " ^ quote (Long_Name.implode xs')) end; @@ -372,11 +373,12 @@ val width = the_default default_width some_width; in (fn program => prepared_serializer program width, prepared_program) end; -fun invoke_serializer thy target some_width module_name args program syms = +fun invoke_serializer thy target some_width raw_module_name args program syms = let - val check = if module_name = "" then I else check_name true; + val module_name = if raw_module_name = "" then "" + else (check_name true raw_module_name; raw_module_name) val (mounted_serializer, prepared_program) = mount_serializer thy - target some_width (check module_name) args program syms; + target some_width module_name args program syms; in mounted_serializer prepared_program end; fun assert_module_name "" = error "Empty module name not allowed here"