src/Tools/Code/code_namespace.ML
changeset 55680 bc5edc5dbf18
parent 55679 59244fc1a7ca
child 55681 7714287dc044
     1.1 --- a/src/Tools/Code/code_namespace.ML	Sun Feb 23 10:33:43 2014 +0100
     1.2 +++ b/src/Tools/Code/code_namespace.ML	Sun Feb 23 10:33:43 2014 +0100
     1.3 @@ -102,7 +102,8 @@
     1.4          val (module_name, base) = prep_sym sym;
     1.5        in
     1.6          Graph.default_node (module_name, (Code_Symbol.Graph.empty, []))
     1.7 -        #> (Graph.map_node module_name o apfst) (Code_Symbol.Graph.new_node (sym, (base, (true, stmt))))
     1.8 +        #> (Graph.map_node module_name o apfst)
     1.9 +          (Code_Symbol.Graph.new_node (sym, (base, (true, stmt))))
    1.10        end;
    1.11      fun add_dep sym sym' =
    1.12        let
    1.13 @@ -110,7 +111,8 @@
    1.14          val (module_name', _) = prep_sym sym';
    1.15        in if module_name = module_name'
    1.16          then (Graph.map_node module_name o apfst) (Code_Symbol.Graph.add_edge (sym, sym'))
    1.17 -        else (Graph.map_node module_name o apsnd) (AList.map_default (op =) (module_name', []) (insert (op =) sym'))
    1.18 +        else (Graph.map_node module_name o apsnd)
    1.19 +          (AList.map_default (op =) (module_name', []) (insert (op =) sym'))
    1.20        end;
    1.21      val proto_program = build_proto_program
    1.22        { empty = Graph.empty, add_stmt = add_stmt, add_dep = add_dep } program;
    1.23 @@ -125,8 +127,9 @@
    1.24        |> fold (fn sym => declare sym (Code_Symbol.Graph.get_node gr sym))
    1.25            (prioritize sym_priority (Code_Symbol.Graph.keys gr))
    1.26        |> fst
    1.27 -      |> (Code_Symbol.Graph.map o K o apsnd)
    1.28 -        (fn (export, stmt) => Option.map (pair export) (modify_stmt stmt));
    1.29 +      |> Code_Symbol.Graph.map_strong_conn (fn syms_bases_exports_stmts =>
    1.30 +        map snd syms_bases_exports_stmts
    1.31 +        |> (map o apsnd) (fn (export, stmt) => Option.map (pair export) (modify_stmt stmt)));
    1.32      val flat_program = proto_program
    1.33        |> (Graph.map o K o apfst) declarations;
    1.34  
    1.35 @@ -177,6 +180,23 @@
    1.36        apsnd o Code_Symbol.Graph.map_node (Code_Symbol.Module name_fragment) o apsnd o map_module_content
    1.37          o map_module name_fragments;
    1.38  
    1.39 +fun map_module_stmts f_module f_stmts sym_base_nodes =
    1.40 +  let
    1.41 +    val some_modules =
    1.42 +      sym_base_nodes
    1.43 +      |> map (fn (sym, (base, Module content)) => SOME (base, content) | _ => NONE)
    1.44 +      |> (burrow_options o map o apsnd) f_module;
    1.45 +    val some_export_stmts =
    1.46 +      sym_base_nodes
    1.47 +      |> map (fn (sym, (base, Stmt export_stmt)) => SOME ((sym, export_stmt), base) | _ => NONE)
    1.48 +      |> (burrow_options o burrow_fst) (fn [] => [] | xs => f_stmts xs)
    1.49 +  in
    1.50 +    map2 (fn SOME (base, content) => (K (base, Module content))
    1.51 +      | NONE => fn SOME (some_export_stmt, base) =>
    1.52 +          (base, case some_export_stmt of SOME export_stmt => Stmt export_stmt | NONE => Dummy))
    1.53 +      some_modules some_export_stmts
    1.54 +  end;
    1.55 +
    1.56  fun hierarchical_program ctxt { module_name, reserved, identifiers, empty_nsp,
    1.57        namify_module, namify_stmt, cyclic_modules, empty_data, memorize_data, modify_stmts } program =
    1.58    let
    1.59 @@ -209,23 +229,26 @@
    1.60        let
    1.61          val (name_fragments, base) = prep_sym sym;
    1.62        in
    1.63 -        (map_module name_fragments o apsnd) (Code_Symbol.Graph.new_node (sym, (base, Stmt (true, stmt))))
    1.64 +        (map_module name_fragments o apsnd)
    1.65 +          (Code_Symbol.Graph.new_node (sym, (base, Stmt (true, stmt))))
    1.66        end;
    1.67 +    fun add_edge_acyclic_error error_msg dep gr =
    1.68 +      Code_Symbol.Graph.add_edge_acyclic dep gr
    1.69 +        handle Graph.CYCLES _ => error (error_msg ())
    1.70      fun add_dep sym sym' =
    1.71        let
    1.72          val (name_fragments, _) = prep_sym sym;
    1.73          val (name_fragments', _) = prep_sym sym';
    1.74          val (name_fragments_common, (diff, diff')) =
    1.75            chop_prefix (op =) (name_fragments, name_fragments');
    1.76 -        val is_module = not (null diff andalso null diff');
    1.77 +        val is_cross_module = not (null diff andalso null diff');
    1.78          val dep = pairself hd (map Code_Symbol.Module diff @ [sym], map Code_Symbol.Module diff' @ [sym']);
    1.79 -        val add_edge = if is_module andalso not cyclic_modules
    1.80 -          then (fn node => Code_Symbol.Graph.add_edge_acyclic dep node
    1.81 -            handle Graph.CYCLES _ => error ("Dependency "
    1.82 -              ^ Code_Symbol.quote ctxt sym ^ " -> "
    1.83 -              ^ Code_Symbol.quote ctxt sym'
    1.84 -              ^ " would result in module dependency cycle"))
    1.85 -          else Code_Symbol.Graph.add_edge dep
    1.86 +        val add_edge = if is_cross_module andalso not cyclic_modules
    1.87 +          then add_edge_acyclic_error (fn _ => "Dependency "
    1.88 +            ^ Code_Symbol.quote ctxt sym ^ " -> "
    1.89 +            ^ Code_Symbol.quote ctxt sym'
    1.90 +            ^ " would result in module dependency cycle") dep
    1.91 +          else Code_Symbol.Graph.add_edge dep;
    1.92        in (map_module name_fragments_common o apsnd) add_edge end;
    1.93      val proto_program = build_proto_program
    1.94        { empty = empty_program, add_stmt = add_stmt, add_dep = add_dep } program;
    1.95 @@ -248,20 +271,18 @@
    1.96          val (nsps', nodes') = (nsps, nodes)
    1.97            |> fold (declare (K namify_module)) module_fragments
    1.98            |> fold (declare (namify_stmt o snd o the_stmt)) stmt_syms;
    1.99 -        fun select_syms syms = case filter (member (op =) stmt_syms) syms
   1.100 -         of [] => NONE
   1.101 -          | syms => SOME syms;
   1.102 -        fun select_stmt (sym, (export, SOME stmt)) = SOME (sym, (export, stmt))
   1.103 -          | select_stmt _ = NONE;
   1.104 -        fun modify_stmts' syms =
   1.105 +        fun modify_stmts' syms_stmts =
   1.106            let
   1.107 -            val (exports, stmts) = map_split (the_stmt o snd o Code_Symbol.Graph.get_node nodes) syms;
   1.108 -            val stmts' = modify_stmts (syms ~~ stmts);
   1.109 -            val stmts'' = stmts' @ replicate (length syms - length stmts') NONE;
   1.110 -          in map_filter select_stmt (syms ~~ (exports ~~ stmts'')) end;
   1.111 -        val stmtss' = (maps modify_stmts' o map_filter select_syms o Code_Symbol.Graph.strong_conn) nodes;
   1.112 -        val nodes'' = Code_Symbol.Graph.map (fn sym => apsnd (fn Module content => Module (make_declarations nsps' content)
   1.113 -            | _ => case AList.lookup (op =) stmtss' sym of SOME stmt => Stmt stmt | _ => Dummy)) nodes';
   1.114 +            val stmts' = modify_stmts syms_stmts
   1.115 +          in stmts' @ replicate (length syms_stmts - length stmts') NONE end;
   1.116 +        fun modify_stmts'' syms_exports_stmts =
   1.117 +          syms_exports_stmts
   1.118 +          |> map (fn (sym, (export, stmt)) => ((sym, stmt), export))
   1.119 +          |> burrow_fst modify_stmts'
   1.120 +          |> map (fn (SOME stmt, export) => SOME (export, stmt) | _ => NONE);
   1.121 +        val nodes'' =
   1.122 +          nodes'
   1.123 +          |> Code_Symbol.Graph.map_strong_conn (map_module_stmts (make_declarations nsps') modify_stmts'');
   1.124          val data' = fold memorize_data stmt_syms data;
   1.125        in (data', nodes'') end;
   1.126      val (_, hierarchical_program) = make_declarations empty_nsp proto_program;