src/Tools/Code/code_namespace.ML
changeset 55291 82780e5f7622
parent 55150 0940309ed8f1
child 55292 1e973b665b98
     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 =