15.4.798  src/lib/graph/trace-view.pkg

# trace-view.pkg

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

# Trace subgraph adaptor.  This takes a linear list of node ids.
# The view returned is the part of the graph that lies on this linear list.


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

    api Trace_Subgraph_View {
        #
        trace_view:  List odg::Node_Id
                          ->
                          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.
                          -> 
                          odg::Digraph(N,E,G);
    };
end;



stipulate
    package odg =  oop_digraph;                                         # oop_digraph   is from   src/lib/graph/oop-digraph.pkg
    package a   =  sparse_rw_vector;                                    # sparse_rw_vector      is from   src/lib/src/sparse-rw-vector.pkg
    package s   =  subgraph_p_view;                                     # subgraph_p_view       is from   src/lib/graph/subgraph-p.pkg
herein

    package   trace_view
    : (weak)  Trace_Subgraph_View                                       # Trace_Subgraph_View   is from   src/lib/graph/trace-view.pkg
    {

        fun trace_view  nodes  (graph as odg::DIGRAPH g)
            =
            {   ord =  a::make_rw_vector (g.capacity (), -100);

                fun order (i, [])
                        =>
                        ();

                    order (i,  n ! ns)
                        =>
                        {   a::set (ord, n, i);
                            order (i+1, ns);
                        };
                end;

                order (0, nodes);

                fun node_p i      =  a::get (ord, i) >= 0; 
                fun edge_p (i, j) =  a::get (ord, i) + 1 == a::get (ord, j); 

                s::subgraph_p_view  nodes  node_p  edge_p  graph;
            };

    };
end;