15.4.785  src/lib/graph/renamed-graph-view.pkg

# renamed-graph-view.pkg
# This view adds some number k to all node ids of the graph,
# i.e. rename all node ids.
#
# -- Allen Leung

# Compiled by:
#     src/lib/graph/graphs.lib

stipulate
    package odg =  oop_digraph;                                                         # oop_digraph   is from   src/lib/graph/oop-digraph.pkg
herein

    api Renamed_Graph_View {
        #
        rename_view:  Int -> odg::Digraph(N,E,G) -> odg::Digraph(N,E,G);                # Here N,E,G stand stead for the types of client-package-supplied records associated with (respectively) nodes, edges and graphs.
    };
end;


stipulate
    package odg =  oop_digraph;                                                         # oop_digraph   is from   src/lib/graph/oop-digraph.pkg
herein

    package   renamed_graph_view
    : (weak)  Renamed_Graph_View                                                        # Renamed_Graph_View    is from   src/lib/graph/renamed-graph-view.pkg
    {
        fun rename_view k (odg::DIGRAPH graph)
            =
            {   fun rename_nodes ns     =   map' ns (\\ (i, n) = (i+k, n));
                fun rename_edges es     =   map' es (\\ (i, j, e) = (i+k, j+k, e));
                fun rename_node_ids ns  =   map' ns (\\ i = i+k);
                fun rename_node_ids' ns =  (map' ns (\\ i = i-k));

                odg::DIGRAPH
                  {
                    name            =>  graph.name,
                    graph_info      =>  graph.graph_info,
                    allot_node_id   =>  \\ n = graph.allot_node_id () + k,
                    add_node        =>  \\ (i, n) = graph.add_node (i-k, n),
                    add_edge        =>  \\ (i, j, e) = graph.add_edge (i-k, j-k, e),
                    remove_node     =>  \\ i = graph.remove_node (i-k),
                    set_out_edges   =>  \\ (i, es) = graph.set_out_edges (i-k,
                                          map' es (\\ (i, j, e) = (i-k, j-k, e))),
                    set_in_edges    =>  \\ (i, es) = graph.set_in_edges (i-k,
                                          map' es (\\ (i, j, e) = (i-k, j-k, e))),
                    set_entries     =>  \\ ns = graph.set_exits (rename_node_ids ns),
                    set_exits       =>  \\ ns = graph.set_entries (rename_node_ids ns),
                    garbage_collect =>  graph.garbage_collect,
                    nodes           =>  {. rename_nodes (graph.nodes ()); },
                    edges           =>  {. rename_edges (graph.edges ()); },
                    order           =>  graph.order,
                    size            =>  graph.size,
                    capacity        =>  graph.capacity,
                    out_edges       =>  \\ i = rename_edges (graph.out_edges (i-k)),
                    in_edges        =>  \\ i = rename_edges (graph.in_edges (i-k)),
                    next            =>  \\ i = rename_node_ids (graph.next (i-k)),
                    prior            =>  \\ i = rename_node_ids (graph.prior (i-k)),
                    has_edge        =>  \\ (i, j) = graph.has_edge (i-k, j-k),
                    has_node        =>  \\ i = graph.has_node (i-k),
                    node_info       =>  \\ i = graph.node_info (i-k),
                    entries         =>  {. rename_node_ids (graph.entries ()); },
                    exits           =>  {. rename_node_ids (graph.exits   ()); },
                    entry_edges     =>  \\ i = rename_edges (graph.entry_edges (i-k)),
                    exit_edges      =>  \\ i = rename_edges (graph.exit_edges (i-k)),
                    forall_nodes    =>  \\ f = graph.forall_nodes (\\ (i, n) = f (i+k, n)),
                    forall_edges    =>  \\ f = graph.forall_edges (\\ (i, j, e) = f (i+k, j+k, e))
                  };
            };
    };
end;