src/Tools/Code/code_namespace.ML
changeset 55292 1e973b665b98
parent 55291 82780e5f7622
child 55293 42cf5802d36a
     1.1 --- a/src/Tools/Code/code_namespace.ML	Mon Feb 03 08:23:19 2014 +0100
     1.2 +++ b/src/Tools/Code/code_namespace.ML	Mon Feb 03 08:23:20 2014 +0100
     1.3 @@ -62,12 +62,19 @@
     1.4        module_names Symtab.empty
     1.5    end;
     1.6  
     1.7 -fun prep_symbol ctxt module_namespace force_module identifiers sym =
     1.8 +fun prep_symbol ctxt { module_namespace, force_module, identifiers } sym =
     1.9    case Code_Symbol.lookup identifiers sym of
    1.10 -      NONE => ((the o Symtab.lookup module_namespace o Code_Symbol.default_prefix ctxt) sym, Code_Symbol.default_base sym)
    1.11 +      NONE => ((the o Symtab.lookup module_namespace o Code_Symbol.default_prefix ctxt) sym,
    1.12 +        Code_Symbol.default_base sym)
    1.13      | SOME prefix_name => if null force_module then prefix_name
    1.14          else (force_module, snd prefix_name);
    1.15  
    1.16 +fun build_proto_program { empty, add_stmt, add_dep } program =
    1.17 +  empty
    1.18 +  |> Code_Symbol.Graph.fold (fn (sym, (stmt, _)) => add_stmt sym stmt) program
    1.19 +  |> Code_Symbol.Graph.fold (fn (sym, (_, (_, syms))) =>
    1.20 +      Code_Symbol.Graph.Keys.fold (add_dep sym) syms) program;
    1.21 +
    1.22  
    1.23  (** flat program structure **)
    1.24  
    1.25 @@ -80,7 +87,8 @@
    1.26      (* building module name hierarchy *)
    1.27      val module_namespace = build_module_namespace ctxt { module_prefix = module_prefix,
    1.28        module_name = module_name, identifiers = identifiers, reserved = reserved } program;
    1.29 -    val prep_sym = prep_symbol ctxt module_namespace (Long_Name.explode module_name) identifiers
    1.30 +    val prep_sym = prep_symbol ctxt { module_namespace = module_namespace,
    1.31 +      force_module = Long_Name.explode module_name, identifiers = identifiers }
    1.32        #>> Long_Name.implode;
    1.33  
    1.34      (* distribute statements over hierarchy *)
    1.35 @@ -91,7 +99,7 @@
    1.36          Graph.default_node (module_name, (Code_Symbol.Graph.empty, []))
    1.37          #> (Graph.map_node module_name o apfst) (Code_Symbol.Graph.new_node (sym, (base, stmt)))
    1.38        end;
    1.39 -    fun add_dependency sym sym' =
    1.40 +    fun add_dep sym sym' =
    1.41        let
    1.42          val (module_name, _) = prep_sym sym;
    1.43          val (module_name', _) = prep_sym sym';
    1.44 @@ -99,10 +107,8 @@
    1.45          then (Graph.map_node module_name o apfst) (Code_Symbol.Graph.add_edge (sym, sym'))
    1.46          else (Graph.map_node module_name o apsnd) (AList.map_default (op =) (module_name', []) (insert (op =) sym'))
    1.47        end;
    1.48 -    val proto_program = Graph.empty
    1.49 -      |> Code_Symbol.Graph.fold (fn (sym, (stmt, _)) => add_stmt sym stmt) program
    1.50 -      |> Code_Symbol.Graph.fold (fn (sym, (_, (_, syms))) =>
    1.51 -          Code_Symbol.Graph.Keys.fold (add_dependency sym) syms) program;
    1.52 +    val proto_program = build_proto_program
    1.53 +      { empty = Graph.empty, add_stmt = add_stmt, add_dep = add_dep } program;
    1.54  
    1.55      (* name declarations and statement modifications *)
    1.56      fun declare sym (base, stmt) (gr, nsp) = 
    1.57 @@ -169,7 +175,8 @@
    1.58      (* building module name hierarchy *)
    1.59      val module_namespace = build_module_namespace ctxt { module_prefix = "",
    1.60        module_name = module_name, identifiers = identifiers, reserved = reserved } program;
    1.61 -    val prep_sym = prep_symbol ctxt module_namespace (Long_Name.explode module_name) identifiers;
    1.62 +    val prep_sym = prep_symbol ctxt { module_namespace = module_namespace,
    1.63 +      force_module = Long_Name.explode module_name, identifiers = identifiers };
    1.64  
    1.65      (* building empty module hierarchy *)
    1.66      val empty_module = (empty_data, Code_Symbol.Graph.empty);
    1.67 @@ -194,7 +201,7 @@
    1.68        in
    1.69          (map_module name_fragments o apsnd) (Code_Symbol.Graph.new_node (sym, (base, Stmt stmt)))
    1.70        end;
    1.71 -    fun add_dependency sym sym' =
    1.72 +    fun add_dep sym sym' =
    1.73        let
    1.74          val (name_fragments, _) = prep_sym sym;
    1.75          val (name_fragments', _) = prep_sym sym';
    1.76 @@ -210,10 +217,8 @@
    1.77                ^ " would result in module dependency cycle"))
    1.78            else Code_Symbol.Graph.add_edge dep
    1.79        in (map_module name_fragments_common o apsnd) add_edge end;
    1.80 -    val proto_program = empty_program
    1.81 -      |> Code_Symbol.Graph.fold (fn (sym, (stmt, _)) => add_stmt sym stmt) program
    1.82 -      |> Code_Symbol.Graph.fold (fn (sym, (_, (_, syms))) =>
    1.83 -          Code_Symbol.Graph.Keys.fold (add_dependency sym) syms) program;
    1.84 +    val proto_program = build_proto_program
    1.85 +      { empty = empty_program, add_stmt = add_stmt, add_dep = add_dep } program;
    1.86  
    1.87      (* name declarations, data and statement modifications *)
    1.88      fun make_declarations nsps (data, nodes) =