content: {-@ LIQUID "--prune-unsorted" @-}
  
  module Graph () where
  
  import Data.Set
  
  
  type Size = Int
  data Map k v = Tip | Bin Size k v (Map k v) (Map k v)
               deriving (Eq, Ord)
  
  
  data Edges edge
  
  
  {-@ measure getEdgesIncoming :: (Edges edge) -> (Set edge) @-}
  
  {-@ measure getEdgesOutgoing :: (Edges edge) -> (Set edge) @-}
  
  data Graph node edge =
    Graph {
      graphMap ::
        Map node (Edges edge, Edges edge)
    }
  
  {-@ invariant {v: (Graph node edge) | (getGraphIncoming v) = (getGraphOutgoing v) } @-}
  
  {-@ measure getGraphIncoming :: (Graph node edge) -> (Set edge)
        getGraphIncoming (Graph m) = (getMapIncoming m)
    @-}
  
  {-@ measure getGraphOutgoing :: (Graph node edge) -> (Set edge)
        getGraphOutgoing (Graph m) = (getMapOutgoing m)
    @-}
  
  
  {-@ measure getMapIncoming :: (Map node (Edges edge, Edges e)) -> (Set edge)
        getMapIncoming Tip = {v | Set_emp v }
        getMapIncoming (Bin size k v lm rm) = (Set_cup (getPairIncoming v) (Set_cup (getMapIncoming lm) (getMapIncoming rm)))
    @-}
  
  
  {-@ measure getMapOutgoing :: (Map node (Edges edge, Edges edge)) -> (Set edge)
        getMapOutgoing Tip = {v | Set_emp v }
        getMapOutgoing (Bin size k v lm rm) = Set_cup (getPairOutgoing v) (Set_cup (getMapOutgoing lm) (getMapOutgoing rm))
    @-}
  
  {-@ measure getPairIncoming :: (Edges edge, Edges e) -> (Set edge)
        getPairIncoming (x, y) = (getEdgesIncoming x)
    @-}
  
  {-@ measure getPairOutgoing :: (Edges e, Edges edge) -> (Set edge)
        getPairOutgoing (x, y) = (getEdgesOutgoing y)
    @-}
  