%
% a breadth first search-- takes a graph and returns the list of 
%     nodes with their bfs numbering
%

pint : sort.
z : trm pint.
s : trm pint -> trm pint.
omega : trm pint.

gtype = list (cross int (list int)).
rtype = list (cross pint int).

nodes : trm gtype -> atm.
node : trm (cross int (list int)) -> atm.
used : trm (cross pint int) -> atm.
next : trm (cross int pint) -> atm.

finish : trm gtype -> trm rtype -> atm.

bfs_main : trm gtype 
	    -> trm int 
	    -> trm rtype
	    -> atm.

bfs : trm gtype
       -> trm int
       -> trm rtype
       -> atm.

bfs' : trm int -> trm pint -> trm rtype -> atm.

bfs'' : trm (list int) -> trm pint -> trm rtype -> atm.


dfs_main : trm gtype 
	    -> trm int 
	    -> trm rtype
	    -> atm.

dfs : trm gtype
       -> trm int
       -> trm rtype
       -> atm.

dfs' : trm int -> trm pint -> trm rtype -> atm.

dfs'' : trm (list int) -> trm pint -> trm rtype -> atm.


%%% Packaging up the results %%%

finish1 : prog(
%%
%% all done.
%%
^ finish nil nil
).

finish2 : prog(
%%
%% add a node that was visited to R
%%       
^ finish ((pair V E) | G) ((pair D V) | R)  
       0= ^ used (pair D V)  
       0= ^ finish G R
).

finish3 : prog(
%%
%% add a node that wasn't visited to R
%%       
^ finish ((pair V E) | G) ((pair omega V) | R) 
       0= ^ node (pair V E) 
       0= ^ finish G R
).


%%% BFS %%%

bfs1 : prog(
%%
%% G is the graph. 
%% S is the start node. 
%% R is the resulting (int * Pint) list of distances for each node from S.
%%
%% make a copy of the given graph so we can gracefully exit
%%   even if graph is not fully connnected.
%%
^ bfs_main G S R  
      <= (^ nodes G => ^ bfs G S R)
).

bfs2 : prog(
%%
%% place each node of graph into linear context
%%
^ bfs (N | G) S R 
      0=  (^ node N =0 ^ bfs G S R)
).

bfs3 : prog(
%%
%% start the breadth-first traversal from start node
%%   S and distance z (zero)
%%
^ bfs nil S R 
      0=  ^ bfs' S z R
).

bfs4 : prog(
%%
%% read the unvisited specified node (V) out of the linear context.
%%   replace it in the linear context with correct distance.
%%   put the edges of node V into ordered context.
%% 
^ bfs' V D R  
      0=  ^ node (pair V E)  
      <<= (^ used (pair D V) =0 ^ bfs'' E D R)
).

bfs5 : prog(
%%
%% read the already visited specified node (V) from linear context.
%%   replace it. then add no edges to ordered context.
%%
^ bfs' V D R  
      0=  ^ used (pair D' V) 
      <<= (^ used (pair D' V) =0 ^ bfs'' nil D R)
).

bfs6 : prog(
%%
%% put an edge into the left side of ordered context
%%   also record distance to this edge
%%
^ bfs'' (E | Es) D R  
      <<=  (^ next (pair E D) >=> ^ bfs'' Es D R)
).

bfs7 : prog(
%%
%% done adding edges to ordered context.
%%   read a new edge to explore from right side of ordered context.
%%   continue breadth-first traversal with incremented distance.
%%
^ bfs'' nil D R  
      <<= ^ next (pair V D')  
      <<= ^ bfs' V (s D') R
).

bfs8 : prog(
%%
%% done adding edges to ordered context.
%%   no more edges left to explore.
%%   package up the results (the linear context) into R
%%
^ bfs'' nil D R 
      <= ^ nodes G  
      0= ^ finish G R
).

%%% DFS  ( same as above with the >=> replaced by =>>)

dfs1 : prog(
%%
%% G is the graph. 
%% S is the start node. 
%% R is the resulting (int * Pint) list of distances for each node from S.
%%
%% make a copy of the given graph so we can gracefully exit
%%   even if graph is not fully connnected.
%%
^ dfs_main G S R  
      <= (^ nodes G => ^ dfs G S R)
).

dfs2 : prog(
%%
%% place each node of graph into linear context
%%
^ dfs (N | G) S R 
      0=  (^ node N =0 ^ dfs G S R)
).

dfs3 : prog(
%%
%% start the depth-first traversal from start node
%%   S and distance z (zero)
%%
^ dfs nil S R 
      0=  ^ dfs' S z R
).

dfs4 : prog(
%%
%% read the unvisited specified node (V) out of the linear context.
%%   replace it in the linear context with correct distance.
%%   put the edges of node V into ordered context.
%% 
^ dfs' V D R  
      0=  ^ node (pair V E)  
      <<= (^ used (pair D V) =0 ^ dfs'' E D R)
).

dfs5 : prog(
%%
%% read the already visited specified node (V) from linear context.
%%   replace it. then add no edges to ordered context.
%%
^ dfs' V D R  
      0=  ^ used (pair D' V) 
      <<= (^ used (pair D' V) =0 ^ dfs'' nil D R)
).

dfs6 : prog(
%%
%% put an edge into the right side of ordered context
%%   also record distance to this edge
%%
^ dfs'' (E | Es) D R  
      <<=  (^ next (pair E D) =>> ^ dfs'' Es D R)
).

dfs7 : prog(
%%
%% done adding edges to ordered context.
%%   read a new edge to explore from right side of ordered context.
%%   continue depth-first traversal with incremented distance.
%%
^ dfs'' nil D R  
      <<= ^ next (pair V D')  
      <<= ^ dfs' V (s D') R
).

dfs8 : prog(
%%
%% done adding edges to ordered context.
%%   no more edges left to explore.
%%   package up the results (the linear context) into R
%%
^ dfs'' nil D R 
      <= ^ nodes G  
      0= ^ finish G R
).



%%% queries %%%

edge1 = 2 | 3 | nil.  % cons 2 (cons 3 nil).
edge2 = 1 | 4 | nil.  % cons 1 (cons 4 nil).
edge3 = 1 | 4 | nil.  % cons 1 (cons 4 nil).
edge4 = 2 | 3 | nil.  % cons 2 (cons 3 nil).

% g1 = cons (pair 1 edge1) (cons (pair 2 edge2) (cons (pair 3 edge3) (cons (pair 4 edge4) nil))).
g1 = (pair 1 edge1) | (pair 2 edge2) | (pair 3 edge3) | (pair 4 edge4) | nil.

e1 = 2 | 3 | nil. % cons 2 (cons 3 nil).
e2 = 1 | 3 | nil. % cons 1 (cons 3 nil).
e3 = 1 | 2 | nil. % cons 1 (cons 2 nil).
% g2 = cons (pair 1 e1) (cons (pair 2 e2) (cons (pair 3 e3) nil)).
g2 = (pair 1 e1) | (pair 2 e2) | (pair 3 e3) | nil.