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

pint : sort.
zero : trm pint.
succ : 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 (cons (pair V E) G) (cons (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 (cons (pair V E) G) (cons (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 (cons 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 zero (zero)
%%
^ bfs nil S R 
      0=  ^ bfs' S zero 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'' (cons 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 (succ 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 (cons 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 zero (zero)
%%
^ dfs nil S R 
      0=  ^ dfs' S zero 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'' (cons 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 (succ 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
).