{- Assignment #1: Labeled Digraph ADT, Using Haskell Lists
   CSci 556: Multiparadigm Programming, Spring 2015
   H. Conrad Cunningham, Professor
   Computer and Information Science
   University of Mississippi

1234567890123456789012345678901234567890123456789012345678901234567890

2015-01-30: Began development
2015-02-03: Completed prototype ADT module with spec, basic
            functionality, and docs; partial testing
2015-02-05: Refine comments and code a few places

-}

module DigraphADT_List
(   Digraph,        -- constrain ops (Eq a, Show a, Show b, Show c) 
    new_graph,      -- Digraph a b c
    is_empty,       -- Digraph a b c -> Bool
    add_vertex,     -- Digraph a b c -> a -> b -> Digraph a b c
    remove_vertex,  -- Digraph a b c -> a -> Digraph a b c
    update_vertex,  -- Digraph a b c -> a -> b -> Digraph a b c
    get_vertex,     -- Digraph a b c -> a -> b
    has_vertex,     -- Digraph a b c -> a -> Bool
    add_edge,       -- Digraph a b c -> a -> a -> c -> Digraph a b c
    remove_edge,    -- Digraph a b c -> a -> a -> Digraph a b c
    update_edge,    -- Digraph a b c -> a -> a -> c -> Digraph a b c
    get_edge,       -- Digraph a b c -> a -> a -> c
    has_edge,       -- Digraph a b c -> a -> a -> Bool
    all_vertices,   -- Digraph a b c -> [a]
    from_edges,     -- Digraph a b c -> a -> [a]
    all_vertices_labels,-- Digraph a b c -> [(a,b)]
    from_edges_labels   -- Digraph a b c -> a -> [(a,c)]
  )
where

{- SPECIFICATION OF LABELED DIGRAPH ADT

** Notation **

(ForAll x, y :: p(x,y)) is true if and only if predicate p(x,y) is
true for all values of x and y.

(Exists x, y :: p(x,y)) is true if and only if there is at least one
pair of values x and y for which p(x,y) is true.

(# x, y :: p(x,y)) yields a count of pairs (x,y) for which p(x,y) is
true.

"<=>" denotes logical equivalence. p <=> q is true if and only if the
logical (Boolean) values p and q are equal (i.e., both true or both
false).

"x IN C" is true if and only if value x is member of a collection C
(such as a set or sequence).  Similarly, "x NOT_IN C" denotes the
negation of "x IN C".

A type consists of a set of values and a set of operations. We
sometimes say a value is IN a type to mean the value is IN the set
associated with the type.

For sets C and D, "C UNION D" denotes set union, that is, a set that
includes all the element of both C and D.

For sets C and D, "C INTERSECT D" denotes set intersection, that is, a
set that includes all elements that are both in C and in D.

For sets C and D, "C - D" denotes set difference, that is, the set C
with all elements of set D removed.

For sets C and D, "C SUBSET_OF D" denotes that C is subset of D, that
is, all the elements of C also occur in D.

A tuple such as "(x,*)" appearing in a collection such as "{ (x,*) }"
denotes element x grouped with all possible values of the second
component.  Note: We could also write { (x,*) } using quantification
as { (x,c) :: c IN some_domain } or { (x,c) :: c IN some_domain }.

A function is a special case of a relation and relation is a set of
ordered pairs (tuples). We sometimes manipulate functions or relations
using set notation for convenience.

A total function is defined for all elements of its domain. A partial function is defined for a subset of the elements of its domain.

** Abstract Model **

The abstract model for the Labeled Digraph ADT is parameterized by the
following types.

    VertexType is the set of possible vertices (i.e., vertex
        identifiers).

    VertexLabelType is the set of possible labels on vertices. (Values
        of this type may have several components.)

    EdgeLabelType is the set of possible labels on edges. (Values of
        this type may have several components.)

We model the state of the instance of the Labeled Digraph ADT with an
abstract value G such that G = (V,E,VL,EL) with G's components
satisfying the following Labeled Digraph Properties.

    V is a finite subset of values from the set VertexType. V denotes
        the vertices (or nodes) of the digraph.

    E is a binary relation on the set V. A pair (v1,v2) in E denotes
        that there is a directed edge from v1 to v2 in the digraph.

    VL is a total function from set V to the set VertexLabelType. 

    EL is a total function from set E to the set EdgeLabelType.

** Interface Invariant **

    Any valid labeled digraph instance G, appearing in either the
    arguments or return value of a public ADT operation, must satisfy 
    the Labeled Digraph Properties.

** Constructive Semantics of Operations **

The preconditions and postconditions of each ADT operation are given
below with the implementations of the operations.  These are part of
the (implementation-independent) specification of the ADT.

In these assertions, for a digraph g that satisfies the invariants,
G(g) denotes its abstract model (V,E,VL,EL) as described above.

-}

{- LIST IMPLEMENTATION OF LABELED DIAGRAPH ADT

** Type Parameters **

    VertexType is an instance of Haskell classes Eq and Show (i.e.,
    can be compared for equality and converted to strings)

    VertexLabelType is an instance of Haskell class Show.

    EdgeLabelType is an instance of Haskell class Show.

Note: It may be desirable to require VertexType to be from class Ord
(totally ordered) and VertexLabelType and EdgeLabelType to be from
class Eq.  These were not necessary for the List implementation (in
this file), but were necessary for the Map implementation given
separately.

** Labeled Digraph Representation **

This implementation represents a labeled digraph as an instance of the
Haskell algebraic data type Digraph, in particular data constructor
(Graph vs es).

In an instance (Graph vs es):
    vs is a list of tuples (v,vl) where
      - v has VertexType and represents a vertex of the digraph
      - vl has VertexLabelType and is the unique label associated
        with vertex v
      - a vertex v occurs at most once in vs
        (i.e., vs encodes a function from vertices to vertex labels)

    es is a list of tuples ((v1,v2),el) where
      - v1 and v2 are vertices occurring in vs, representing a 
        directed edge from v1 to v2
      - el has EdgeLabelType and is the unique label associated with
        edge (v1,v2)
      - an edge (v1,v2) occurs at most once in vs
        (i.e., es encodes a function from edges to edge labels)

In terms of the abstract model, vs encodes VL directly and, because VL
is a total function on V, it encodes V indirectly.  Similarly, es
encodes EL directly and E indirectly.

** Implementation Invariant **

    Any Haskell Digraph value (Graph vs es) with abstract model 
    G = (V,E,VL,EL), appearing in either the arguments or return
    value of an operation, must also satisfy the following:

        (ForAll v, l :: (v,l) IN vs  <=> (v,l) IN VL ) &&
        (ForAll v1, v2, m :: (v1,v2,m) IN es  <=> ((v1,v2),m) IN EL )

-}

data Digraph a b c = Graph [(a,b)] [(a,a,c)]

instance (Show a, Show b, Show c) => Show (Digraph a b c) where
    show (Graph vs es) = "(Digraph " ++ show vs ++ ", " ++
                         show es ++ ")"

{- new_graph creates and returns a new instance of the graph ADT.

   Pre:  True
   Post: G(Result) == ({},{},{},{})
-}

new_graph :: (Eq a, Show a, Show b, Show c) => Digraph a b c
new_graph = Graph [] []


{- is_empty g returns true if and only if graph g is empty.

   Pre:  G(g) = (V,E,VL,EL)
   Post: Result == (V == {} && E == {}) 
-}

is_empty :: (Eq a, Show a, Show b, Show c) => Digraph a b c -> Bool
is_empty (Graph [] _ ) = True
is_empty _             = False


{- add_vertex g nv nl inserts vertex nv with label nl into graph g and
   returns the resulting graph.

   Pre:  G(g) = (V,E,VL,EL) && nv NOT_IN V 
   Post: G(Result) == (V UNION {nv}, E, VL UNION {(nv,nl)}, EL)
-}

add_vertex :: (Eq a, Show a, Show b, Show c) =>
                  Digraph a b c -> a -> b -> Digraph a b c
add_vertex g@(Graph vs es) nv nl
    | not (has_vertex g nv) = Graph ((nv,nl):vs) es
    | otherwise             = error has_nv
    where has_nv = "Vertex " ++ show nv ++ " already in digraph"


{- remove_vertex g ov deletes vertex ov from graph g and returns the
   resulting graph.

   Pre:  G(g) =  (V,E,VL,EL) && ov IN V
   Post: G(Result) == (V', E', VL', EL')
         where V'  = V  - {ov}
               E'  = E  - {(ov,*),(*,ov)}
               VL' = VL - {(ov,*)}
               EL' = EL - {((ov,*),*),((*,ov),*)}
-}

remove_vertex :: (Eq a, Show a, Show b, Show c) =>
                     Digraph a b c -> a -> Digraph a b c
remove_vertex g@(Graph vs es) ov
    | has_vertex g ov = Graph ws fs
    | otherwise       = error no_ov
    where ws    = [ (w,m)     | (w,m) <- vs, w /= ov ]
          fs    = [ (v1,v2,m) | (v1,v2,m) <- es, v1 /= ov, v2 /= ov ]
          no_ov = "Vertex " ++ show ov ++ " not in digraph"


{- update_vertex g ov nl changes the label on vertex ov in graph g to
   be nl and returns the resulting graph.

   Pre:  G(g) =  (V,E,VL,EL) && ov IN V
   Post: G(Result) == (V - {ov}, E, VL', EL)
         where VL' = (VL - {(ov,VL(ov))}) UNION {(ov,nl)}
-}

update_vertex :: (Eq a, Show a, Show b, Show c) =>
                     Digraph a b c -> a -> b -> Digraph a b c
update_vertex g@(Graph vs es) ov nl
    | has_vertex g ov = Graph (map chg vs) es
    | otherwise       = error no_ov
    where chg (w,m) = (if w == ov then (ov,nl) else (w,m))
          no_ov     = "Vertex " ++ show ov ++ " not in digraph"

{- get_vertex g ov returns the label from vertex ov in graph g

   Pre:   G(g) = (V,E,VL,EL) && ov IN V
   Post:  Result == VL(ov)
-}

get_vertex :: (Eq a, Show a, Show b, Show c) =>
                  Digraph a b c -> a -> b
get_vertex (Graph vs _)  ov
    | not (null ls) = head ls
    | otherwise     = error no_ov
    where ls    = [ l | (w,l) <- vs, w == ov]
          no_ov = "Vertex " ++ show ov ++ " not in digraph"

{- has_vertex g ov returns true if and only if ov is a vertex of 
   graph g.

   Pre:  G(g) = (V,E,VL,EL) && ov IN VertexLabelType
   Post: G(Result) == ov IN V
-}

has_vertex :: (Eq a, Show a, Show b, Show c) =>
                  Digraph a b c -> a -> Bool
has_vertex (Graph vs _) ov = not (null [ n | (n,_) <- vs, n == ov])


{- add_edge g v1 v2 nl inserts an edge from vertex v1 to vertex v2 in
   graph g and returns the resulting graph.

   Pre:  G(g) = (V,E,VL,EL) && v1 IN V && v2 IN V && (v1,v2) NOT_IN E
   Post: G(Result) == (V, E', VL, EL')
         where E'  = E  UNION {(v1,v2)}
               EL' = EL UNION {((v1,v2),nl)}
-}

add_edge :: (Eq a, Show a, Show b, Show c) =>
                Digraph a b c -> a -> a -> c -> Digraph a b c
add_edge g@(Graph vs es) v1 v2 nl
    | not (has_vertex g v1) = error no_v1
    | not (has_vertex g v2) = error no_v2
    | has_edge g v1 v2      = error has_e
    | otherwise             = Graph vs ((v1,v2,nl):es)
    where no_v1 = "Cannot add edge. Vertex " ++ show v1 ++
                   " not in digraph"
          no_v2 = "Cannot add edge. Vertex " ++ show v2 ++
                   " not in digraph"
          has_e = "Edge (" ++ show v1 ++ "," ++ show v2 ++
                  ") already in digraph"


{- remove_edge g v1 v2 deletes the edge from vertex v1 to vertex v2 
   from graph g and returns the resulting graph.

   Pre:  G(g) =  (V,E,VL,EL) V - {ov} && (v1,v2) IN E
   Post: G(Result) == (V, E - {(v1,v2)}, VL, EL - { ((v1,v2),*) }
-}

remove_edge :: (Eq a, Show a, Show b, Show c) =>
                   Digraph a b c -> a -> a -> Digraph a b c
remove_edge g@(Graph vs es) v1 v2 
    | has_edge g v1 v2 = Graph vs (filter notv1v2 es)
    | otherwise        = error no_e
    where notv1v2 (v,w,_) = ((v1,v2) /= (v,w))
          no_e    = "Edge (" ++ show v1 ++ "," ++ show v2 ++
                    ") not in digraph"


{- update_edge g v1 v2 nl changes the label on the edge from vertex v1
   to vertex v2 in graph g to have label nl and returns the resulting
   graph.

   Pre:  G(g) = (V,E,VL,EL) && (v1,v2) IN E
   Post: G(Result) == (V, E, VL, EL')
         where EL' == (EL - {((v1,v2),*)}) UNION {((v2,v2),nl)
-}

update_edge :: (Eq a, Show a, Show b, Show c) =>
                   Digraph a b c -> a -> a -> c -> Digraph a b c
update_edge g@(Graph vs es) v1 v2 nl
    | has_edge g v1 v2 = Graph vs fs
    | otherwise        = error no_e
    where fs   = [ if (v1,v2) == (v,w) then (v1,v2,nl) else (v,w,m) |
                     (v,w,m) <- es ]
          no_e = "Edge (" ++ show v1 ++ "," ++ show v2 ++
                 ") not in digraph"


{- get_edge g v1 v2 returns the label on the edge from vertex v1 to 
   vertex v2 in graph g.

   Pre:  G(g) = (V,E,VL,EL) && (v1,v2) IN E
   Post: Result == EL((v1,v2))
-}

get_edge :: (Eq a, Show a, Show b, Show c) =>
                Digraph a b c -> a -> a -> c
get_edge g@(Graph vs es) v1 v2
    | not (null fs) = head fs
    | otherwise     = error no_e
    where fs   = [ m | (v,w,m) <- es, (v1,v2) == (v,w) ]
          no_e = "Edge (" ++ show v1 ++ "," ++ show v2 ++
                 ") not in digraph"


{- has_edge g v1 v2 returns true if and only if there is an edge
   from a vertex v1 to a vertex v2 in graph g.

   Pre:  G(g) = (V,E,VL,EL) 
   Post: Result == (v1,v2) IN E
-}

has_edge :: (Eq a, Show a, Show b, Show c) =>
                Digraph a b c -> a -> a -> Bool
has_edge (Graph vs es) v1 v2 =
    not (null [ (v,w) | (v,w,_) <- es, (v1,v2) == (v,w) ])


{- all_vertices g returns a sequence of all the vertices in graph g. 
   The sequence is represented by a builtin Haskell list.

   Pre:  G(g) = (V,E,VL,EL)
   Post: (ForAll ov: ov IN Result <=> ov IN V) && 
         length(Result) == size(V)
-}

all_vertices :: (Eq a, Show a, Show b, Show c) =>
                    Digraph a b c -> [a]
all_vertices (Graph vs _) = map fst vs


{- from_edges g v1 returns a sequence of all vertices v2 such that
   there is an edge from vertex v1 to vertex v2 in graph g.  The
   sequence is represented by a builtin Haskell list.

   Pre:  G(g) = (V,E,VL,EL) && v1 IN V
   Post: (ForAll v2: v2 IN Result <=> (v1,v2) IN E) &&
         length(Result) == (# v2 :: (v1,v2) IN E)
-}

from_edges :: (Eq a, Show a, Show b, Show c) =>
                  Digraph a b c -> a -> [a]
from_edges g@(Graph vs es) v1
    | has_vertex g v1 = [ w | (v,w,_) <- es, v == v1 ]
    | otherwise       = error no_v1
    where no_v1 = "Vertex " ++ show v1 ++ " not in digraph"


{- all_vertices_labels g returns a sequence of all pairs (v,l) such
   that v is a vertex and l is it's label in graph g.  The sequence is
   represented by a builtin Haskell list.

   Pre:  G(g) = (V,E,VL,EL)
   Post: (ForAll v, l: (v,l) IN Result <=> (v,l) IN VL) && 
         length(Result) == size(VL)
-}

all_vertices_labels :: (Eq a, Show a, Show b, Show c) =>
                           Digraph a b c -> [(a,b)]
all_vertices_labels (Graph vs _) = vs


{- from_edges_labels g v1 returns a sequence of all pairs (v2,l) such
   that there is an edge (v1,v2) labeled with l in graph g.

   Pre:  G(g) = (V,E,VL,EL) && v1 IN V
   Post: (ForAll v2, l :: (v2,l) IN Result <=> ((v1,v2),l) IN EL) &&
         length(Result) == (# v2 :: (v1,v2 ) IN E)
-}

from_edges_labels :: (Eq a, Show a, Show b, Show c) =>
                         Digraph a b c -> a -> [(a,c)]
from_edges_labels g@(Graph vs es) v1 
    | has_vertex g v1 = [ (w,m) | (v,w,m) <- es, v == v1 ]
    | otherwise       = error no_v1
    where no_v1 = "Vertex " ++ show v1 ++ " not in digraph"