tuned storage of code identifiers
authorhaftmann
Mon Feb 03 08:23:19 2014 +0100 (2014-02-03)
changeset 5529182780e5f7622
parent 55290 3951ced4156c
child 55292 1e973b665b98
tuned storage of code identifiers
src/Tools/Code/code_namespace.ML
src/Tools/Code/code_target.ML
     1.1 --- a/src/Tools/Code/code_namespace.ML	Mon Feb 03 17:55:50 2014 +0100
     1.2 +++ b/src/Tools/Code/code_namespace.ML	Mon Feb 03 08:23:19 2014 +0100
     1.3 @@ -42,27 +42,32 @@
     1.4  
     1.5  (** fundamental module name hierarchy **)
     1.6  
     1.7 -fun lookup_identifier identifiers sym =
     1.8 -  Code_Symbol.lookup identifiers sym
     1.9 -  |> Option.map (split_last o Long_Name.explode);
    1.10 +fun module_fragments' { identifiers, reserved } name =
    1.11 +  case Code_Symbol.lookup_module_data identifiers name of
    1.12 +      SOME (fragments, _) => fragments
    1.13 +    | NONE => map (fn fragment => fst (Name.variant fragment reserved)) (Long_Name.explode name);
    1.14 +
    1.15 +fun module_fragments { module_name, identifiers, reserved } =
    1.16 +  if module_name = ""
    1.17 +  then module_fragments' { identifiers = identifiers, reserved = reserved }
    1.18 +  else K (Long_Name.explode module_name);
    1.19  
    1.20 -fun force_identifier ctxt fragments_tab force_module identifiers sym =
    1.21 -  case lookup_identifier identifiers sym of
    1.22 -      NONE => ((the o Symtab.lookup fragments_tab o Code_Symbol.default_prefix ctxt) sym, Code_Symbol.default_base sym)
    1.23 +fun build_module_namespace ctxt { module_prefix, module_name, identifiers, reserved } program =
    1.24 +  let
    1.25 +    val module_names = Code_Symbol.Graph.fold (insert (op =) o Code_Symbol.default_prefix ctxt o fst) program [];
    1.26 +    val module_fragments' = module_fragments
    1.27 +      { module_name = module_name, identifiers = identifiers, reserved = reserved };
    1.28 +  in
    1.29 +    fold (fn name => Symtab.update (name, Long_Name.explode module_prefix @ module_fragments' name))
    1.30 +      module_names Symtab.empty
    1.31 +  end;
    1.32 +
    1.33 +fun prep_symbol ctxt module_namespace force_module identifiers sym =
    1.34 +  case Code_Symbol.lookup identifiers sym of
    1.35 +      NONE => ((the o Symtab.lookup module_namespace o Code_Symbol.default_prefix ctxt) sym, Code_Symbol.default_base sym)
    1.36      | SOME prefix_name => if null force_module then prefix_name
    1.37          else (force_module, snd prefix_name);
    1.38  
    1.39 -fun build_module_namespace ctxt { module_prefix, module_identifiers, reserved } program =
    1.40 -  let
    1.41 -    fun alias_fragments name = case module_identifiers name
    1.42 -     of SOME name' => Long_Name.explode name'
    1.43 -      | NONE => map (fn name => fst (Name.variant name reserved)) (Long_Name.explode name);
    1.44 -    val module_names = Code_Symbol.Graph.fold (insert (op =) o Code_Symbol.default_prefix ctxt o fst) program [];
    1.45 -  in
    1.46 -    fold (fn name => Symtab.update (name, Long_Name.explode module_prefix @ alias_fragments name))
    1.47 -      module_names Symtab.empty
    1.48 -  end;
    1.49 -
    1.50  
    1.51  (** flat program structure **)
    1.52  
    1.53 @@ -73,12 +78,9 @@
    1.54    let
    1.55  
    1.56      (* building module name hierarchy *)
    1.57 -    val module_identifiers = if module_name = ""
    1.58 -      then Code_Symbol.lookup_module_data identifiers
    1.59 -      else K (SOME module_name);
    1.60 -    val fragments_tab = build_module_namespace ctxt { module_prefix = module_prefix,
    1.61 -      module_identifiers = module_identifiers, reserved = reserved } program;
    1.62 -    val prep_sym = force_identifier ctxt fragments_tab (Long_Name.explode module_name) identifiers
    1.63 +    val module_namespace = build_module_namespace ctxt { module_prefix = module_prefix,
    1.64 +      module_name = module_name, identifiers = identifiers, reserved = reserved } program;
    1.65 +    val prep_sym = prep_symbol ctxt module_namespace (Long_Name.explode module_name) identifiers
    1.66        #>> Long_Name.implode;
    1.67  
    1.68      (* distribute statements over hierarchy *)
    1.69 @@ -165,12 +167,9 @@
    1.70    let
    1.71  
    1.72      (* building module name hierarchy *)
    1.73 -    val module_identifiers = if module_name = ""
    1.74 -      then Code_Symbol.lookup_module_data identifiers
    1.75 -      else K (SOME module_name);
    1.76 -    val fragments_tab = build_module_namespace ctxt { module_prefix = "",
    1.77 -      module_identifiers = module_identifiers, reserved = reserved } program;
    1.78 -    val prep_sym = force_identifier ctxt fragments_tab (Long_Name.explode module_name) identifiers;
    1.79 +    val module_namespace = build_module_namespace ctxt { module_prefix = "",
    1.80 +      module_name = module_name, identifiers = identifiers, reserved = reserved } program;
    1.81 +    val prep_sym = prep_symbol ctxt module_namespace (Long_Name.explode module_name) identifiers;
    1.82  
    1.83      (* building empty module hierarchy *)
    1.84      val empty_module = (empty_data, Code_Symbol.Graph.empty);
    1.85 @@ -184,9 +183,9 @@
    1.86            #> (apsnd o Code_Symbol.Graph.map_node (Code_Symbol.Module name_fragment) o apsnd o map_module_content o allocate_module) name_fragments;
    1.87      val empty_program =
    1.88        empty_module
    1.89 -      |> Symtab.fold (fn (_, fragments) => allocate_module fragments) fragments_tab
    1.90 +      |> Symtab.fold (fn (_, fragments) => allocate_module fragments) module_namespace
    1.91        |> Code_Symbol.Graph.fold (allocate_module o these o Option.map fst
    1.92 -          o lookup_identifier identifiers o fst) program;
    1.93 +          o Code_Symbol.lookup identifiers o fst) program;
    1.94  
    1.95      (* distribute statements over hierarchy *)
    1.96      fun add_stmt sym stmt =
     2.1 --- a/src/Tools/Code/code_target.ML	Mon Feb 03 17:55:50 2014 +0100
     2.2 +++ b/src/Tools/Code/code_target.ML	Mon Feb 03 08:23:19 2014 +0100
     2.3 @@ -81,7 +81,8 @@
     2.4      class * (string * 'c option) list, (class * class) * (string * 'd option) list,
     2.5      (class * string) * (string * 'e option) list,
     2.6      string * (string * 'f option) list) Code_Symbol.attr;
     2.7 -type identifier_data = (string, string, string, string, string, string) Code_Symbol.data;
     2.8 +type identifier_data = (string list * string, string list * string, string list * string, string list * string,
     2.9 +  string list * string, string list * string) Code_Symbol.data;
    2.10  
    2.11  type tyco_syntax = Code_Printer.tyco_syntax;
    2.12  type raw_const_syntax = Code_Printer.raw_const_syntax;
    2.13 @@ -144,7 +145,7 @@
    2.14            val y' = Name.desymbolize false y;
    2.15          in ys' @ [y'] end;
    2.16    in if xs' = xs
    2.17 -    then s
    2.18 +    then if is_module then (xs, "") else split_last xs
    2.19      else error ("Invalid code name: " ^ quote s ^ "\n"
    2.20        ^ "better try " ^ quote (Long_Name.implode xs'))
    2.21    end;
    2.22 @@ -372,11 +373,12 @@
    2.23      val width = the_default default_width some_width;
    2.24    in (fn program => prepared_serializer program width, prepared_program) end;
    2.25  
    2.26 -fun invoke_serializer thy target some_width module_name args program syms =
    2.27 +fun invoke_serializer thy target some_width raw_module_name args program syms =
    2.28    let
    2.29 -    val check = if module_name = "" then I else check_name true;
    2.30 +    val module_name = if raw_module_name = "" then ""
    2.31 +      else (check_name true raw_module_name; raw_module_name)
    2.32      val (mounted_serializer, prepared_program) = mount_serializer thy
    2.33 -      target some_width (check module_name) args program syms;
    2.34 +      target some_width module_name args program syms;
    2.35    in mounted_serializer prepared_program end;
    2.36  
    2.37  fun assert_module_name "" = error "Empty module name not allowed here"