    -- | This module contains the type definitions and basic operations
    -- for the graph that
    -- "Futhark.Optimise.ReduceDeviceSyncs.MigrationTable" internally uses
    -- to construct a migration table.  It is however completely
    -- Futhark-agnostic and implements a generic graph abstraction.
    --
    -- = Overview
    --
    -- The 'Graph' type is a data flow dependency graph of program variables, each
    -- variable represented by a 'Vertex'. A vertex may have edges to other vertices
    -- or to a sink, which is a special vertex with no graph representation. Each
    -- edge to a vertex is either from another vertex or from a source, which also
    -- is a special vertex with no graph representation.
    --
    -- The primary graph operation provided by this module is 'route'. Given the
    -- vertex that some unspecified source has an edge to, a path is attempted
    -- found to a sink. If a sink can be reached from the source, all edges along
    -- the path are reversed. The path in the opposite direction of reversed edges
    -- from a source to some sink is a route.
    --
    -- Routes can be used to find a minimum vertex cut in the graph through what
    -- amounts to a specialized depth-first search implementation of the
    -- Ford-Fulkerson method. When viewed in this way each graph edge has a capacity
    -- of 1 and the reversing of edges to create routes amounts to sending reverse
    -- flow through a residual network (the current state of the graph).
    -- The max-flow min-cut theorem allows one to determine a minimum edge cut that
    -- separates the sources and sinks.
    --
    -- If each vertex @v@ in the graph is viewed as two vertices, @v_in@ and
    -- @v_out@, with all ingoing edges to @v@ going to @v_in@, all outgoing edges
    -- from @v@ going from @v_out@, and @v_in@ connected to @v_out@ with a single
    -- edge, then the minimum edge cut of the view amounts to a minimum vertex cut
    -- in the actual graph. The view need not be manifested as whether @v_in@ or
    -- @v_out@ is reached by an edge to @v@ can be determined from whether that edge
    -- is reversed or not. The presence of an outgoing, reversed edge also gives the
    -- state of the virtual edge that connects @v_in@ to @v_out@.
    --
    -- When routing fails to find a sink in some subgraph reached via an edge then
    -- that edge is marked exhausted. No sink can be reached via an exhausted edge,
    -- and any subsequent routing attempt will skip pathfinding along such edge.
    module Futhark.Optimise.ReduceDeviceSyncs.MigrationTable.Graph
      ( -- * Types
        Graph,
        Id,
        IdSet,
        Vertex (..),
        Routing (..),
        Exhaustion (..),
        Edges (..),
        EdgeType (..),
        Visited,
        Result (..),

        -- * Construction
        empty,
        vertex,
        declareEdges,
        oneEdge,
        none,

        -- * Insertion
        insert,

        -- * Update
        adjust,
        connectToSink,
        addEdges,

        -- * Query
        member,
        lookup,
        isSinkConnected,

        -- * Routing
        route,
        routeMany,

        -- * Traversal
        fold,
        reduce,
      )
    where

    import Data.IntMap.Strict qualified as IM
    import Data.IntSet qualified as IS
    import Data.List qualified as L
    import Data.Map.Strict qualified as M
    import Data.Maybe (fromJust)
    import Prelude hiding (lookup)

    --------------------------------------------------------------------------------
    --                                   TYPES                                    --
    --------------------------------------------------------------------------------

    -- | A data flow dependency graph of program variables, each variable
    -- represented by a 'Vertex'.
    newtype Graph m = Graph (IM.IntMap (Vertex m))

    -- | A handle that identifies a specific 'Vertex'.
    type Id = Int

    -- | A set of 'Id's.
    type IdSet = IS.IntSet

    -- | A graph representation of some program variable.
    data Vertex m = Vertex
      { -- | The handle for this vertex in the graph.
        forall m. Vertex m -> Id
    vertexId :: Id,
        -- | Custom data associated with the variable.
        forall m. Vertex m -> m
    vertexMeta :: m,
        -- | Whether a route passes through this vertex, and from where.
        forall m. Vertex m -> Routing
    vertexRouting :: Routing,
        -- | Handles of vertices that this vertex has an edge to.
        forall m. Vertex m -> Edges
    vertexEdges :: Edges
      }

    -- | Route tracking for some vertex.
    -- If a route passes through the vertex then both an ingoing and an outgoing
    -- edge to/from that vertex will have been reversed, and the vertex will in
    -- effect have lost one edge and gained another. The gained edge will be to
    -- the prior vertex along the route that passes through.
    data Routing
      = -- | No route passes through the vertex, and no edges have been reversed,
        -- added, nor deleted compared to what was declared.
        NoRoute
      | -- | A route passes through the vertex, and the prior vertex is the source
        -- of that route. The edge gained by reversal is by definition exhausted.
        FromSource
      | -- | A route passes through the vertex, and this is the handle of the prior
        -- vertex. The edge gained by reversal may be exhausted. Routing assumes
        -- that at most one 'FromNode' routing exists to each vertex in a graph.
        FromNode Id Exhaustion
      deriving (Id -> Routing -> ShowS
    [Routing] -> ShowS
    Routing -> String
    (Id -> Routing -> ShowS)
    -> (Routing -> String) -> ([Routing] -> ShowS) -> Show Routing
    forall a.
    (Id -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Id -> Routing -> ShowS
    showsPrec :: Id -> Routing -> ShowS
    $cshow :: Routing -> String
    show :: Routing -> String
    $cshowList :: [Routing] -> ShowS
    showList :: [Routing] -> ShowS
    Show, Routing -> Routing -> Bool
    (Routing -> Routing -> Bool)
    -> (Routing -> Routing -> Bool) -> Eq Routing
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Routing -> Routing -> Bool
    == :: Routing -> Routing -> Bool
    $c/= :: Routing -> Routing -> Bool
    /= :: Routing -> Routing -> Bool
    Eq, Eq Routing
    Eq Routing =>
    (Routing -> Routing -> Ordering)
    -> (Routing -> Routing -> Bool)
    -> (Routing -> Routing -> Bool)
    -> (Routing -> Routing -> Bool)
    -> (Routing -> Routing -> Bool)
    -> (Routing -> Routing -> Routing)
    -> (Routing -> Routing -> Routing)
    -> Ord Routing
    Routing -> Routing -> Bool
    Routing -> Routing -> Ordering
    Routing -> Routing -> Routing
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: Routing -> Routing -> Ordering
    compare :: Routing -> Routing -> Ordering
    $c< :: Routing -> Routing -> Bool
    < :: Routing -> Routing -> Bool
    $c<= :: Routing -> Routing -> Bool
    <= :: Routing -> Routing -> Bool
    $c> :: Routing -> Routing -> Bool
    > :: Routing -> Routing -> Bool
    $c>= :: Routing -> Routing -> Bool
    >= :: Routing -> Routing -> Bool
    $cmax :: Routing -> Routing -> Routing
    max :: Routing -> Routing -> Routing
    $cmin :: Routing -> Routing -> Routing
    min :: Routing -> Routing -> Routing
    Ord)

    -- | Whether some edge is exhausted or not. No sink can be reached via an
    -- exhausted edge.
    data Exhaustion = Exhausted | NotExhausted
      deriving (Id -> Exhaustion -> ShowS
    [Exhaustion] -> ShowS
    Exhaustion -> String
    (Id -> Exhaustion -> ShowS)
    -> (Exhaustion -> String)
    -> ([Exhaustion] -> ShowS)
    -> Show Exhaustion
    forall a.
    (Id -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Id -> Exhaustion -> ShowS
    showsPrec :: Id -> Exhaustion -> ShowS
    $cshow :: Exhaustion -> String
    show :: Exhaustion -> String
    $cshowList :: [Exhaustion] -> ShowS
    showList :: [Exhaustion] -> ShowS
    Show, Exhaustion -> Exhaustion -> Bool
    (Exhaustion -> Exhaustion -> Bool)
    -> (Exhaustion -> Exhaustion -> Bool) -> Eq Exhaustion
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Exhaustion -> Exhaustion -> Bool
    == :: Exhaustion -> Exhaustion -> Bool
    $c/= :: Exhaustion -> Exhaustion -> Bool
    /= :: Exhaustion -> Exhaustion -> Bool
    Eq, Eq Exhaustion
    Eq Exhaustion =>
    (Exhaustion -> Exhaustion -> Ordering)
    -> (Exhaustion -> Exhaustion -> Bool)
    -> (Exhaustion -> Exhaustion -> Bool)
    -> (Exhaustion -> Exhaustion -> Bool)
    -> (Exhaustion -> Exhaustion -> Bool)
    -> (Exhaustion -> Exhaustion -> Exhaustion)
    -> (Exhaustion -> Exhaustion -> Exhaustion)
    -> Ord Exhaustion
    Exhaustion -> Exhaustion -> Bool
    Exhaustion -> Exhaustion -> Ordering
    Exhaustion -> Exhaustion -> Exhaustion
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: Exhaustion -> Exhaustion -> Ordering
    compare :: Exhaustion -> Exhaustion -> Ordering
    $c< :: Exhaustion -> Exhaustion -> Bool
    < :: Exhaustion -> Exhaustion -> Bool
    $c<= :: Exhaustion -> Exhaustion -> Bool
    <= :: Exhaustion -> Exhaustion -> Bool
    $c> :: Exhaustion -> Exhaustion -> Bool
    > :: Exhaustion -> Exhaustion -> Bool
    $c>= :: Exhaustion -> Exhaustion -> Bool
    >= :: Exhaustion -> Exhaustion -> Bool
    $cmax :: Exhaustion -> Exhaustion -> Exhaustion
    max :: Exhaustion -> Exhaustion -> Exhaustion
    $cmin :: Exhaustion -> Exhaustion -> Exhaustion
    min :: Exhaustion -> Exhaustion -> Exhaustion
    Ord)

    -- | All relevant edges that have been declared from some vertex, plus
    -- bookkeeping to track their exhaustion and reversal.
    data Edges
      = -- | The vertex has an edge to a sink; all other declared edges are
        -- irrelevant. The edge cannot become exhausted, and it is reversed if a
        -- route passes through the vertex (@vertexRouting v /= NoRoute@).
        ToSink
      | -- | All vertices that the vertex has a declared edge to, and which of
        -- those edges that are not exhausted nor reversed, if not all.
        ToNodes IdSet (Maybe IdSet)
      deriving (Id -> Edges -> ShowS
    [Edges] -> ShowS
    Edges -> String
    (Id -> Edges -> ShowS)
    -> (Edges -> String) -> ([Edges] -> ShowS) -> Show Edges
    forall a.
    (Id -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Id -> Edges -> ShowS
    showsPrec :: Id -> Edges -> ShowS
    $cshow :: Edges -> String
    show :: Edges -> String
    $cshowList :: [Edges] -> ShowS
    showList :: [Edges] -> ShowS
    Show, Edges -> Edges -> Bool
    (Edges -> Edges -> Bool) -> (Edges -> Edges -> Bool) -> Eq Edges
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Edges -> Edges -> Bool
    == :: Edges -> Edges -> Bool
    $c/= :: Edges -> Edges -> Bool
    /= :: Edges -> Edges -> Bool
    Eq, Eq Edges
    Eq Edges =>
    (Edges -> Edges -> Ordering)
    -> (Edges -> Edges -> Bool)
    -> (Edges -> Edges -> Bool)
    -> (Edges -> Edges -> Bool)
    -> (Edges -> Edges -> Bool)
    -> (Edges -> Edges -> Edges)
    -> (Edges -> Edges -> Edges)
    -> Ord Edges
    Edges -> Edges -> Bool
    Edges -> Edges -> Ordering
    Edges -> Edges -> Edges
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: Edges -> Edges -> Ordering
    compare :: Edges -> Edges -> Ordering
    $c< :: Edges -> Edges -> Bool
    < :: Edges -> Edges -> Bool
    $c<= :: Edges -> Edges -> Bool
    <= :: Edges -> Edges -> Bool
    $c> :: Edges -> Edges -> Bool
    > :: Edges -> Edges -> Bool
    $c>= :: Edges -> Edges -> Bool
    >= :: Edges -> Edges -> Bool
    $cmax :: Edges -> Edges -> Edges
    max :: Edges -> Edges -> Edges
    $cmin :: Edges -> Edges -> Edges
    min :: Edges -> Edges -> Edges
    Ord)

    instance Semigroup Edges where
      Edges
    ToSink <> :: Edges -> Edges -> Edges
    <> Edges
    _ = Edges
    ToSink
      Edges
    _ <> Edges
    ToSink = Edges
    ToSink
      (ToNodes IdSet
    a1 Maybe IdSet
    Nothing) <> (ToNodes IdSet
    a2 Maybe IdSet
    Nothing) =
        IdSet -> Maybe IdSet -> Edges
    ToNodes (IdSet
    a1 IdSet -> IdSet -> IdSet
    forall a. Semigroup a => a -> a -> a
    <> IdSet
    a2) Maybe IdSet
    forall a. Maybe a
    Nothing
      (ToNodes IdSet
    a1 (Just IdSet
    e1)) <> (ToNodes IdSet
    a2 Maybe IdSet
    Nothing) =
        IdSet -> Maybe IdSet -> Edges
    ToNodes (IdSet
    a1 IdSet -> IdSet -> IdSet
    forall a. Semigroup a => a -> a -> a
    <> IdSet
    a2) (Maybe IdSet -> Edges) -> Maybe IdSet -> Edges
    forall a b. (a -> b) -> a -> b
    $ IdSet -> Maybe IdSet
    forall a. a -> Maybe a
    Just (IdSet
    e1 IdSet -> IdSet -> IdSet
    forall a. Semigroup a => a -> a -> a
    <> IdSet -> IdSet -> IdSet
    IS.difference IdSet
    a2 IdSet
    a1)
      (ToNodes IdSet
    a1 Maybe IdSet
    Nothing) <> (ToNodes IdSet
    a2 (Just IdSet
    e2)) =
        IdSet -> Maybe IdSet -> Edges
    ToNodes (IdSet
    a1 IdSet -> IdSet -> IdSet
    forall a. Semigroup a => a -> a -> a
    <> IdSet
    a2) (Maybe IdSet -> Edges) -> Maybe IdSet -> Edges
    forall a b. (a -> b) -> a -> b
    $ IdSet -> Maybe IdSet
    forall a. a -> Maybe a
    Just (IdSet
    e2 IdSet -> IdSet -> IdSet
    forall a. Semigroup a => a -> a -> a
    <> IdSet -> IdSet -> IdSet
    IS.difference IdSet
    a1 IdSet
    a2)
      (ToNodes IdSet
    a1 (Just IdSet
    e1)) <> (ToNodes IdSet
    a2 (Just IdSet
    e2)) =
        let a :: IdSet
    a = IdSet -> IdSet -> IdSet
    IS.difference IdSet
    e2 (IdSet -> IdSet -> IdSet
    IS.difference IdSet
    a1 IdSet
    e1)
            b :: IdSet
    b = IdSet -> IdSet -> IdSet
    IS.difference IdSet
    e1 (IdSet -> IdSet -> IdSet
    IS.difference IdSet
    a2 IdSet
    e2)
         in IdSet -> Maybe IdSet -> Edges
    ToNodes (IdSet
    a1 IdSet -> IdSet -> IdSet
    forall a. Semigroup a => a -> a -> a
    <> IdSet
    a2) (Maybe IdSet -> Edges) -> Maybe IdSet -> Edges
    forall a b. (a -> b) -> a -> b
    $ IdSet -> Maybe IdSet
    forall a. a -> Maybe a
    Just (IdSet
    a IdSet -> IdSet -> IdSet
    forall a. Semigroup a => a -> a -> a
    <> IdSet
    b)

    instance Monoid Edges where
      -- The empty set of edges.
      mempty :: Edges
    mempty = IdSet -> Maybe IdSet -> Edges
    ToNodes IdSet
    IS.empty Maybe IdSet
    forall a. Maybe a
    Nothing

    -- | Whether a vertex is reached via a normal or reversed edge.
    data EdgeType = Normal | Reversed
      deriving (EdgeType -> EdgeType -> Bool
    (EdgeType -> EdgeType -> Bool)
    -> (EdgeType -> EdgeType -> Bool) -> Eq EdgeType
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: EdgeType -> EdgeType -> Bool
    == :: EdgeType -> EdgeType -> Bool
    $c/= :: EdgeType -> EdgeType -> Bool
    /= :: EdgeType -> EdgeType -> Bool
    Eq, Eq EdgeType
    Eq EdgeType =>
    (EdgeType -> EdgeType -> Ordering)
    -> (EdgeType -> EdgeType -> Bool)
    -> (EdgeType -> EdgeType -> Bool)
    -> (EdgeType -> EdgeType -> Bool)
    -> (EdgeType -> EdgeType -> Bool)
    -> (EdgeType -> EdgeType -> EdgeType)
    -> (EdgeType -> EdgeType -> EdgeType)
    -> Ord EdgeType
    EdgeType -> EdgeType -> Bool
    EdgeType -> EdgeType -> Ordering
    EdgeType -> EdgeType -> EdgeType
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: EdgeType -> EdgeType -> Ordering
    compare :: EdgeType -> EdgeType -> Ordering
    $c< :: EdgeType -> EdgeType -> Bool
    < :: EdgeType -> EdgeType -> Bool
    $c<= :: EdgeType -> EdgeType -> Bool
    <= :: EdgeType -> EdgeType -> Bool
    $c> :: EdgeType -> EdgeType -> Bool
    > :: EdgeType -> EdgeType -> Bool
    $c>= :: EdgeType -> EdgeType -> Bool
    >= :: EdgeType -> EdgeType -> Bool
    $cmax :: EdgeType -> EdgeType -> EdgeType
    max :: EdgeType -> EdgeType -> EdgeType
    $cmin :: EdgeType -> EdgeType -> EdgeType
    min :: EdgeType -> EdgeType -> EdgeType
    Ord)

    -- | State that tracks which vertices a traversal has visited, caching immediate
    -- computations.
    newtype Visited a = Visited {forall a. Visited a -> Map (EdgeType, Id) a
    visited :: M.Map (EdgeType, Id) a}

    -- | The result of a graph traversal that may abort early in case a sink is
    -- reached.
    data Result a
      = -- | The traversal finished without encountering a sink, producing this
        -- value.
        Produced a
      | -- | The traversal was aborted because a sink was reached.
        FoundSink
      deriving (Result a -> Result a -> Bool
    (Result a -> Result a -> Bool)
    -> (Result a -> Result a -> Bool) -> Eq (Result a)
    forall a. Eq a => Result a -> Result a -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: forall a. Eq a => Result a -> Result a -> Bool
    == :: Result a -> Result a -> Bool
    $c/= :: forall a. Eq a => Result a -> Result a -> Bool
    /= :: Result a -> Result a -> Bool
    Eq)

    instance (Semigroup a) => Semigroup (Result a) where
      Result a
    FoundSink <> :: Result a -> Result a -> Result a
    <> Result a
    _ = Result a
    forall a. Result a
    FoundSink
      Result a
    _ <> Result a
    FoundSink = Result a
    forall a. Result a
    FoundSink
      Produced a
    x <> Produced a
    y = a -> Result a
    forall a. a -> Result a
    Produced (a
    x a -> a -> a
    forall a. Semigroup a => a -> a -> a
    <> a
    y)

    --------------------------------------------------------------------------------
    --                                CONSTRUCTION                                --
    --------------------------------------------------------------------------------

    -- | The empty graph.
    empty :: Graph m
    empty :: forall m. Graph m
    empty = IntMap (Vertex m) -> Graph m
    forall m. IntMap (Vertex m) -> Graph m
    Graph IntMap (Vertex m)
    forall a. IntMap a
    IM.empty

    -- | Constructs a 'Vertex' without any edges.
    vertex :: Id -> m -> Vertex m
    vertex :: forall m. Id -> m -> Vertex m
    vertex Id
    i m
    m =
      Vertex
        { vertexId :: Id
    vertexId = Id
    i,
          vertexMeta :: m
    vertexMeta = m
    m,
          vertexRouting :: Routing
    vertexRouting = Routing
    NoRoute,
          vertexEdges :: Edges
    vertexEdges = Edges
    forall a. Monoid a => a
    mempty
        }

    -- | Creates a set of edges where no edge is reversed or exhausted.
    declareEdges :: [Id] -> Edges
    declareEdges :: [Id] -> Edges
    declareEdges [Id]
    is = IdSet -> Maybe IdSet -> Edges
    ToNodes ([Id] -> IdSet
    IS.fromList [Id]
    is) Maybe IdSet
    forall a. Maybe a
    Nothing

    -- | Like 'declareEdges' but for a single vertex.
    oneEdge :: Id -> Edges
    oneEdge :: Id -> Edges
    oneEdge Id
    i = IdSet -> Maybe IdSet -> Edges
    ToNodes (Id -> IdSet
    IS.singleton Id
    i) Maybe IdSet
    forall a. Maybe a
    Nothing

    -- | Initial 'Visited' state before any vertex has been visited.
    none :: Visited a
    none :: forall a. Visited a
    none = Map (EdgeType, Id) a -> Visited a
    forall a. Map (EdgeType, Id) a -> Visited a
    Visited Map (EdgeType, Id) a
    forall k a. Map k a
    M.empty

    --------------------------------------------------------------------------------
    --                                 INSERTION                                  --
    --------------------------------------------------------------------------------

    -- | Insert a new vertex into the graph. If its variable already is represented
    -- in the graph, the original graph is returned.
    insert :: Vertex m -> Graph m -> Graph m
    insert :: forall m. Vertex m -> Graph m -> Graph m
    insert Vertex m
    v (Graph IntMap (Vertex m)
    m) = IntMap (Vertex m) -> Graph m
    forall m. IntMap (Vertex m) -> Graph m
    Graph (IntMap (Vertex m) -> Graph m) -> IntMap (Vertex m) -> Graph m
    forall a b. (a -> b) -> a -> b
    $ (Vertex m -> Vertex m -> Vertex m)
    -> Id -> Vertex m -> IntMap (Vertex m) -> IntMap (Vertex m)
    forall a. (a -> a -> a) -> Id -> a -> IntMap a -> IntMap a
    IM.insertWith Vertex m -> Vertex m -> Vertex m
    forall a b. a -> b -> a
    const (Vertex m -> Id
    forall m. Vertex m -> Id
    vertexId Vertex m
    v) Vertex m
    v IntMap (Vertex m)
    m

    --------------------------------------------------------------------------------
    --                                   UPDATE                                   --
    --------------------------------------------------------------------------------

    -- | Adjust the vertex with this specific id. When no vertex with that id is a
    -- member of the graph, the original graph is returned.
    adjust :: (Vertex m -> Vertex m) -> Id -> Graph m -> Graph m
    adjust :: forall m. (Vertex m -> Vertex m) -> Id -> Graph m -> Graph m
    adjust Vertex m -> Vertex m
    f Id
    i (Graph IntMap (Vertex m)
    m) = IntMap (Vertex m) -> Graph m
    forall m. IntMap (Vertex m) -> Graph m
    Graph (IntMap (Vertex m) -> Graph m) -> IntMap (Vertex m) -> Graph m
    forall a b. (a -> b) -> a -> b
    $ (Vertex m -> Vertex m)
    -> Id -> IntMap (Vertex m) -> IntMap (Vertex m)
    forall a. (a -> a) -> Id -> IntMap a -> IntMap a
    IM.adjust Vertex m -> Vertex m
    f Id
    i IntMap (Vertex m)
    m

    -- | Connect the vertex with this id to a sink. When no vertex with that id is a
    -- member of the graph, the original graph is returned.
    connectToSink :: Id -> Graph m -> Graph m
    connectToSink :: forall m. Id -> Graph m -> Graph m
    connectToSink = (Vertex m -> Vertex m) -> Id -> Graph m -> Graph m
    forall m. (Vertex m -> Vertex m) -> Id -> Graph m -> Graph m
    adjust ((Vertex m -> Vertex m) -> Id -> Graph m -> Graph m)
    -> (Vertex m -> Vertex m) -> Id -> Graph m -> Graph m
    forall a b. (a -> b) -> a -> b
    $ \Vertex m
    v -> Vertex m
    v {vertexEdges = ToSink}

    -- | Add these edges to the vertex with this id. When no vertex with that id is
    -- a member of the graph, the original graph is returned.
    addEdges :: Edges -> Id -> Graph m -> Graph m
    addEdges :: forall m. Edges -> Id -> Graph m -> Graph m
    addEdges Edges
    es = (Vertex m -> Vertex m) -> Id -> Graph m -> Graph m
    forall m. (Vertex m -> Vertex m) -> Id -> Graph m -> Graph m
    adjust ((Vertex m -> Vertex m) -> Id -> Graph m -> Graph m)
    -> (Vertex m -> Vertex m) -> Id -> Graph m -> Graph m
    forall a b. (a -> b) -> a -> b
    $ \Vertex m
    v -> Vertex m
    v {vertexEdges = es <> vertexEdges v}

    --------------------------------------------------------------------------------
    --                                   QUERY                                    --
    --------------------------------------------------------------------------------

    -- | Does a vertex for the given id exist in the graph?
    member :: Id -> Graph m -> Bool
    member :: forall m. Id -> Graph m -> Bool
    member Id
    i (Graph IntMap (Vertex m)
    m) = Id -> IntMap (Vertex m) -> Bool
    forall a. Id -> IntMap a -> Bool
    IM.member Id
    i IntMap (Vertex m)
    m

    -- | Returns the vertex with the given id.
    lookup :: Id -> Graph m -> Maybe (Vertex m)
    lookup :: forall m. Id -> Graph m -> Maybe (Vertex m)
    lookup Id
    i (Graph IntMap (Vertex m)
    m) = Id -> IntMap (Vertex m) -> Maybe (Vertex m)
    forall a. Id -> IntMap a -> Maybe a
    IM.lookup Id
    i IntMap (Vertex m)
    m

    -- | Returns whether a vertex with the given id exists in the
    -- graph and is connected directly to a sink.
    isSinkConnected :: Id -> Graph m -> Bool
    isSinkConnected :: forall m. Id -> Graph m -> Bool
    isSinkConnected Id
    i Graph m
    g =
      Bool -> (Vertex m -> Bool) -> Maybe (Vertex m) -> Bool
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Bool
    False ((Edges
    ToSink Edges -> Edges -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (Edges -> Bool) -> (Vertex m -> Edges) -> Vertex m -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Vertex m -> Edges
    forall m. Vertex m -> Edges
    vertexEdges) (Id -> Graph m -> Maybe (Vertex m)
    forall m. Id -> Graph m -> Maybe (Vertex m)
    lookup Id
    i Graph m
    g)

    --                                  ROUTING                                   --
    --------------------------------------------------------------------------------

    -- | @route src g@ attempts to find a path in @g@ from the source connected
    -- vertex with id @src@. If a sink is found, all edges along the path will be
    -- reversed to create a route, and the id of the vertex that connects to the
    -- sink is returned.
    route :: Id -> Graph m -> (Maybe Id, Graph m)
    route :: forall m. Id -> Graph m -> (Maybe Id, Graph m)
    route Id
    src Graph m
    g =
      case Pending
    -> Id
    -> Maybe Id
    -> EdgeType
    -> Id
    -> Graph m
    -> (RoutingResult m, Graph m)
    forall m.
    Pending
    -> Id
    -> Maybe Id
    -> EdgeType
    -> Id
    -> Graph m
    -> (RoutingResult m, Graph m)
    route' Pending
    forall a. IntMap a
    IM.empty Id
    0 Maybe Id
    forall a. Maybe a
    Nothing EdgeType
    Normal Id
    src Graph m
    g of
        (RoutingResult m
    DeadEnd, Graph m
    g') -> (Maybe Id
    forall a. Maybe a
    Nothing, Graph m
    g')
        (SinkFound Id
    snk, Graph m
    g') -> (Id -> Maybe Id
    forall a. a -> Maybe a
    Just Id
    snk, Graph m
    g')
        (CycleDetected {}, Graph m
    _) ->
          String -> (Maybe Id, Graph m)
    forall a. HasCallStack => String -> a
    error
            String
    "Routing did not escape cycle in Futhark.Analysis.MigrationTable.Graph."

    -- | @routeMany srcs g@ attempts to create a 'route' in @g@ from every vertex
    -- in @srcs@. Returns the ids for the vertices connected to each found sink.
    routeMany :: [Id] -> Graph m -> ([Id], Graph m)
    routeMany :: forall m. [Id] -> Graph m -> ([Id], Graph m)
    routeMany [Id]
    srcs Graph m
    graph =
      (([Id], Graph m) -> Id -> ([Id], Graph m))
    -> ([Id], Graph m) -> [Id] -> ([Id], Graph m)
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    L.foldl' ([Id], Graph m) -> Id -> ([Id], Graph m)
    forall {m}. ([Id], Graph m) -> Id -> ([Id], Graph m)
    f ([], Graph m
    graph) [Id]
    srcs
      where
        f :: ([Id], Graph m) -> Id -> ([Id], Graph m)
    f ([Id]
    snks, Graph m
    g) Id
    src =
          case Id -> Graph m -> (Maybe Id, Graph m)
    forall m. Id -> Graph m -> (Maybe Id, Graph m)
    route Id
    src Graph m
    g of
            (Maybe Id
    Nothing, Graph m
    g') -> ([Id]
    snks, Graph m
    g')
            (Just Id
    snk, Graph m
    g') -> (Id
    snk Id -> [Id] -> [Id]
    forall a. a -> [a] -> [a]
    : [Id]
    snks, Graph m
    g')

    --------------------------------------------------------------------------------
    --                                 TRAVERSAL                                  --
    --------------------------------------------------------------------------------

    -- | @fold g f (a, vs) et i@ folds @f@ over the vertices in @g@ that can be
    -- reached from the vertex with handle @i@ accessed via an edge of type @et@.
    -- Each vertex @v@ may be visited up to two times, once for each type of edge
    -- @e@ pointing to it, and each time @f a e v@ is evaluated to produce an
    -- updated @a@ value to be used in future @f@ evaluations or to be returned.
    -- The @vs@ set records which @f a e v@ evaluations already have taken place.
    -- The function returns an updated 'Visited' set recording the evaluations it
    -- has performed.
    fold ::
      Graph m ->
      (a -> EdgeType -> Vertex m -> a) ->
      (a, Visited ()) ->
      EdgeType ->
      Id ->
      (a, Visited ())
    fold :: forall m a.
    Graph m
    -> (a -> EdgeType -> Vertex m -> a)
    -> (a, Visited ())
    -> EdgeType
    -> Id
    -> (a, Visited ())
    fold Graph m
    g a -> EdgeType -> Vertex m -> a
    f (a
    res, Visited ()
    vs) EdgeType
    et Id
    i
      | (EdgeType, Id) -> Map (EdgeType, Id) () -> Bool
    forall k a. Ord k => k -> Map k a -> Bool
    M.notMember (EdgeType
    et, Id
    i) (Visited () -> Map (EdgeType, Id) ()
    forall a. Visited a -> Map (EdgeType, Id) a
    visited Visited ()
    vs),
        Just Vertex m
    v <- Id -> Graph m -> Maybe (Vertex m)
    forall m. Id -> Graph m -> Maybe (Vertex m)
    lookup Id
    i Graph m
    g =
          let res' :: a
    res' = a -> EdgeType -> Vertex m -> a
    f a
    res EdgeType
    et Vertex m
    v
              vs' :: Visited ()
    vs' = Map (EdgeType, Id) () -> Visited ()
    forall a. Map (EdgeType, Id) a -> Visited a
    Visited (Map (EdgeType, Id) () -> Visited ())
    -> Map (EdgeType, Id) () -> Visited ()
    forall a b. (a -> b) -> a -> b
    $ (EdgeType, Id)
    -> () -> Map (EdgeType, Id) () -> Map (EdgeType, Id) ()
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    M.insert (EdgeType
    et, Id
    i) () (Visited () -> Map (EdgeType, Id) ()
    forall a. Visited a -> Map (EdgeType, Id) a
    visited Visited ()
    vs)
              st :: (a, Visited ())
    st = (a
    res', Visited ()
    vs')
           in case (EdgeType
    et, Vertex m -> Routing
    forall m. Vertex m -> Routing
    vertexRouting Vertex m
    v) of
                (EdgeType
    Normal, Routing
    FromSource) -> (a, Visited ())
    st
                (EdgeType
    Normal, FromNode Id
    rev Exhaustion
    _) -> (a, Visited ()) -> Id -> (a, Visited ())
    foldReversed (a, Visited ())
    st Id
    rev
                (EdgeType
    Reversed, FromNode Id
    rev Exhaustion
    _) -> (a, Visited ()) -> Id -> Edges -> (a, Visited ())
    foldAll (a, Visited ())
    st Id
    rev (Vertex m -> Edges
    forall m. Vertex m -> Edges
    vertexEdges Vertex m
    v)
                (EdgeType, Routing)
    _ -> (a, Visited ()) -> Edges -> (a, Visited ())
    foldNormals (a, Visited ())
    st (Vertex m -> Edges
    forall m. Vertex m -> Edges
    vertexEdges Vertex m
    v)
      | Bool
    otherwise =
          (a
    res, Visited ()
    vs)
      where
        foldReversed :: (a, Visited ()) -> Id -> (a, Visited ())
    foldReversed (a, Visited ())
    st = Graph m
    -> (a -> EdgeType -> Vertex m -> a)
    -> (a, Visited ())
    -> EdgeType
    -> Id
    -> (a, Visited ())
    forall m a.
    Graph m
    -> (a -> EdgeType -> Vertex m -> a)
    -> (a, Visited ())
    -> EdgeType
    -> Id
    -> (a, Visited ())
    fold Graph m
    g a -> EdgeType -> Vertex m -> a
    f (a, Visited ())
    st EdgeType
    Reversed

        foldAll :: (a, Visited ()) -> Id -> Edges -> (a, Visited ())
    foldAll (a, Visited ())
    st Id
    rev Edges
    es = (a, Visited ()) -> Id -> (a, Visited ())
    foldReversed ((a, Visited ()) -> Edges -> (a, Visited ())
    foldNormals (a, Visited ())
    st Edges
    es) Id
    rev

        foldNormals :: (a, Visited ()) -> Edges -> (a, Visited ())
    foldNormals (a, Visited ())
    st Edges
    ToSink = (a, Visited ())
    st
        foldNormals (a, Visited ())
    st (ToNodes IdSet
    es Maybe IdSet
    _) =
          ((a, Visited ()) -> Id -> (a, Visited ()))
    -> (a, Visited ()) -> IdSet -> (a, Visited ())
    forall a. (a -> Id -> a) -> a -> IdSet -> a
    IS.foldl' (\(a, Visited ())
    s -> Graph m
    -> (a -> EdgeType -> Vertex m -> a)
    -> (a, Visited ())
    -> EdgeType
    -> Id
    -> (a, Visited ())
    forall m a.
    Graph m
    -> (a -> EdgeType -> Vertex m -> a)
    -> (a, Visited ())
    -> EdgeType
    -> Id
    -> (a, Visited ())
    fold Graph m
    g a -> EdgeType -> Vertex m -> a
    f (a, Visited ())
    s EdgeType
    Normal) (a, Visited ())
    st IdSet
    es

    -- | @reduce g r vs et i@ returns 'FoundSink' if a sink can be reached via the
    -- vertex @v@ with id @i@ in @g@. Otherwise it returns 'Produced' @(r x et v)@
    -- where @x@ is the '<>' aggregate of all values produced by reducing the
    -- vertices that are available via the edges of @v@.
    -- @et@ identifies the type of edge that @v@ is accessed by and thereby which
    -- edges of @v@ that are available. @vs@ caches reductions of vertices that
    -- previously have been visited in the graph.
    --
    -- The reduction of a cyclic reference resolves to 'mempty'.
    reduce ::
      (Monoid a) =>
      Graph m ->
      (a -> EdgeType -> Vertex m -> a) ->
      Visited (Result a) ->
      EdgeType ->
      Id ->
      (Result a, Visited (Result a))
    reduce :: forall a m.
    Monoid a =>
    Graph m
    -> (a -> EdgeType -> Vertex m -> a)
    -> Visited (Result a)
    -> EdgeType
    -> Id
    -> (Result a, Visited (Result a))
    reduce Graph m
    g a -> EdgeType -> Vertex m -> a
    r Visited (Result a)
    vs EdgeType
    et Id
    i
      | Just Result a
    res <- (EdgeType, Id) -> Map (EdgeType, Id) (Result a) -> Maybe (Result a)
    forall k a. Ord k => k -> Map k a -> Maybe a
    M.lookup (EdgeType
    et, Id
    i) (Visited (Result a) -> Map (EdgeType, Id) (Result a)
    forall a. Visited a -> Map (EdgeType, Id) a
    visited Visited (Result a)
    vs) =
          (Result a
    res, Visited (Result a)
    vs)
      | Just Vertex m
    v <- Id -> Graph m -> Maybe (Vertex m)
    forall m. Id -> Graph m -> Maybe (Vertex m)
    lookup Id
    i Graph m
    g =
          Vertex m -> (Result a, Visited (Result a))
    reduceVertex Vertex m
    v
      | Bool
    otherwise =
          (a -> Result a
    forall a. a -> Result a
    Produced a
    forall a. Monoid a => a
    mempty, Visited (Result a)
    vs) -- shouldn't happen
      where
        reduceVertex :: Vertex m -> (Result a, Visited (Result a))
    reduceVertex Vertex m
    v =
          let (Result a
    res, Visited (Result a)
    vs') = Vertex m -> (Result a, Visited (Result a))
    forall {m}. Vertex m -> (Result a, Visited (Result a))
    reduceEdges Vertex m
    v
           in case Result a
    res of
                Produced a
    x -> Result a -> Visited (Result a) -> (Result a, Visited (Result a))
    forall {a}. a -> Visited a -> (a, Visited a)
    cached (a -> Result a
    forall a. a -> Result a
    Produced (a -> Result a) -> a -> Result a
    forall a b. (a -> b) -> a -> b
    $ a -> EdgeType -> Vertex m -> a
    r a
    x EdgeType
    et Vertex m
    v) Visited (Result a)
    vs'
                Result a
    FoundSink -> Result a -> Visited (Result a) -> (Result a, Visited (Result a))
    forall {a}. a -> Visited a -> (a, Visited a)
    cached Result a
    res Visited (Result a)
    vs'

        cached :: a -> Visited a -> (a, Visited a)
    cached a
    res Visited a
    vs0 =
          let vs1 :: Visited a
    vs1 = Map (EdgeType, Id) a -> Visited a
    forall a. Map (EdgeType, Id) a -> Visited a
    Visited ((EdgeType, Id) -> a -> Map (EdgeType, Id) a -> Map (EdgeType, Id) a
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    M.insert (EdgeType
    et, Id
    i) a
    res (Map (EdgeType, Id) a -> Map (EdgeType, Id) a)
    -> Map (EdgeType, Id) a -> Map (EdgeType, Id) a
    forall a b. (a -> b) -> a -> b
    $ Visited a -> Map (EdgeType, Id) a
    forall a. Visited a -> Map (EdgeType, Id) a
    visited Visited a
    vs0)
           in (a
    res, Visited a
    vs1)

        reduceEdges :: Vertex m -> (Result a, Visited (Result a))
    reduceEdges Vertex m
    v =
          case (EdgeType
    et, Vertex m -> Routing
    forall m. Vertex m -> Routing
    vertexRouting Vertex m
    v) of
            (EdgeType
    Normal, Routing
    FromSource) -> (a -> Result a
    forall a. a -> Result a
    Produced a
    forall a. Monoid a => a
    mempty, Visited (Result a)
    vs)
            (EdgeType
    Normal, FromNode Id
    rev Exhaustion
    _) -> (Visited (Result a) -> (Result a, Visited (Result a)))
    -> (Result a, Visited (Result a))
    forall {b}. (Visited (Result a) -> b) -> b
    entry (Id -> Visited (Result a) -> (Result a, Visited (Result a))
    reduceReversed Id
    rev)
            (EdgeType
    Reversed, FromNode Id
    rev Exhaustion
    _) -> (Visited (Result a) -> (Result a, Visited (Result a)))
    -> (Result a, Visited (Result a))
    forall {b}. (Visited (Result a) -> b) -> b
    entry (Id -> Edges -> Visited (Result a) -> (Result a, Visited (Result a))
    reduceAll Id
    rev (Edges -> Visited (Result a) -> (Result a, Visited (Result a)))
    -> Edges -> Visited (Result a) -> (Result a, Visited (Result a))
    forall a b. (a -> b) -> a -> b
    $ Vertex m -> Edges
    forall m. Vertex m -> Edges
    vertexEdges Vertex m
    v)
            (EdgeType, Routing)
    _ -> (Visited (Result a) -> (Result a, Visited (Result a)))
    -> (Result a, Visited (Result a))
    forall {b}. (Visited (Result a) -> b) -> b
    entry (Edges -> Visited (Result a) -> (Result a, Visited (Result a))
    reduceNormals (Edges -> Visited (Result a) -> (Result a, Visited (Result a)))
    -> Edges -> Visited (Result a) -> (Result a, Visited (Result a))
    forall a b. (a -> b) -> a -> b
    $ Vertex m -> Edges
    forall m. Vertex m -> Edges
    vertexEdges Vertex m
    v)

        -- Handle cycles
        entry :: (Visited (Result a) -> b) -> b
    entry Visited (Result a) -> b
    f = Visited (Result a) -> b
    f (Visited (Result a) -> b) -> Visited (Result a) -> b
    forall a b. (a -> b) -> a -> b
    $ Map (EdgeType, Id) (Result a) -> Visited (Result a)
    forall a. Map (EdgeType, Id) a -> Visited a
    Visited (Map (EdgeType, Id) (Result a) -> Visited (Result a))
    -> Map (EdgeType, Id) (Result a) -> Visited (Result a)
    forall a b. (a -> b) -> a -> b
    $ (EdgeType, Id)
    -> Result a
    -> Map (EdgeType, Id) (Result a)
    -> Map (EdgeType, Id) (Result a)
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    M.insert (EdgeType
    et, Id
    i) (a -> Result a
    forall a. a -> Result a
    Produced a
    forall a. Monoid a => a
    mempty) (Visited (Result a) -> Map (EdgeType, Id) (Result a)
    forall a. Visited a -> Map (EdgeType, Id) a
    visited Visited (Result a)
    vs)

        reduceReversed :: Id -> Visited (Result a) -> (Result a, Visited (Result a))
    reduceReversed Id
    rev Visited (Result a)
    vs' = Graph m
    -> (a -> EdgeType -> Vertex m -> a)
    -> Visited (Result a)
    -> EdgeType
    -> Id
    -> (Result a, Visited (Result a))
    forall a m.
    Monoid a =>
    Graph m
    -> (a -> EdgeType -> Vertex m -> a)
    -> Visited (Result a)
    -> EdgeType
    -> Id
    -> (Result a, Visited (Result a))
    reduce Graph m
    g a -> EdgeType -> Vertex m -> a
    r Visited (Result a)
    vs' EdgeType
    Reversed Id
    rev

        reduceAll :: Id -> Edges -> Visited (Result a) -> (Result a, Visited (Result a))
    reduceAll Id
    rev Edges
    es Visited (Result a)
    vs0 =
          let (Result a
    res, Visited (Result a)
    vs1) = Edges -> Visited (Result a) -> (Result a, Visited (Result a))
    reduceNormals Edges
    es Visited (Result a)
    vs0
           in case Result a
    res of
                Produced a
    _ ->
                  let (Result a
    res', Visited (Result a)
    vs2) = Id -> Visited (Result a) -> (Result a, Visited (Result a))
    reduceReversed Id
    rev Visited (Result a)
    vs1
                   in (Result a
    res Result a -> Result a -> Result a
    forall a. Semigroup a => a -> a -> a
    <> Result a
    res', Visited (Result a)
    vs2)
                Result a
    FoundSink -> (Result a
    res, Visited (Result a)
    vs1)

        reduceNormals :: Edges -> Visited (Result a) -> (Result a, Visited (Result a))
    reduceNormals Edges
    ToSink Visited (Result a)
    vs' = (Result a
    forall a. Result a
    FoundSink, Visited (Result a)
    vs')
        reduceNormals (ToNodes IdSet
    es Maybe IdSet
    _) Visited (Result a)
    vs' = a -> [Id] -> Visited (Result a) -> (Result a, Visited (Result a))
    reduceNorms a
    forall a. Monoid a => a
    mempty (IdSet -> [Id]
    IS.elems IdSet
    es) Visited (Result a)
    vs'

        reduceNorms :: a -> [Id] -> Visited (Result a) -> (Result a, Visited (Result a))
    reduceNorms a
    x [] Visited (Result a)
    vs0 = (a -> Result a
    forall a. a -> Result a
    Produced a
    x, Visited (Result a)
    vs0)
        reduceNorms a
    x (Id
    e : [Id]
    es) Visited (Result a)
    vs0 =
          let (Result a
    res, Visited (Result a)
    vs1) = Graph m
    -> (a -> EdgeType -> Vertex m -> a)
    -> Visited (Result a)
    -> EdgeType
    -> Id
    -> (Result a, Visited (Result a))
    forall a m.
    Monoid a =>
    Graph m
    -> (a -> EdgeType -> Vertex m -> a)
    -> Visited (Result a)
    -> EdgeType
    -> Id
    -> (Result a, Visited (Result a))
    reduce Graph m
    g a -> EdgeType -> Vertex m -> a
    r Visited (Result a)
    vs0 EdgeType
    Normal Id
    e
           in case Result a
    res of
                Produced a
    y -> a -> [Id] -> Visited (Result a) -> (Result a, Visited (Result a))
    reduceNorms (a
    x a -> a -> a
    forall a. Semigroup a => a -> a -> a
    <> a
    y) [Id]
    es Visited (Result a)
    vs1
                Result a
    FoundSink -> (Result a
    res, Visited (Result a)
    vs1)

    --------------------------------------------------------------------------------
    --                             ROUTING INTERNALS                              --
    --------------------------------------------------------------------------------

    -- | A set of vertices visited by a graph traversal, and at what depth they were
    -- encountered. Used to detect cycles.
    type Pending = IM.IntMap Depth

    -- | Search depth. Distance to some vertex from some search root.
    type Depth = Int

    -- | The outcome of attempted to find a route through a vertex.
    data RoutingResult a
      = -- | No sink could be reached through this vertex.
        DeadEnd
      | -- | A cycle was detected. A sink can be reached through this vertex if a
        -- sink can be reached from the vertex at this depth. If no sink can be
        -- reached from the vertex at this depth, then the graph should be updated
        -- by these actions. Until the vertex is reached, the status of these
        -- vertices are pending.
        CycleDetected Depth [Graph a -> Graph a] Pending
      | -- | A sink was found. This is the id of the vertex connected to it.
        SinkFound Id

    instance Semigroup (RoutingResult a) where
      SinkFound Id
    i <> :: RoutingResult a -> RoutingResult a -> RoutingResult a
    <> RoutingResult a
    _ = Id -> RoutingResult a
    forall a. Id -> RoutingResult a
    SinkFound Id
    i
      RoutingResult a
    _ <> SinkFound Id
    i = Id -> RoutingResult a
    forall a. Id -> RoutingResult a
    SinkFound Id
    i
      CycleDetected Id
    d1 [Graph a -> Graph a]
    as1 Pending
    _ <> CycleDetected Id
    d2 [Graph a -> Graph a]
    as2 Pending
    p2 =
        Id -> [Graph a -> Graph a] -> Pending -> RoutingResult a
    forall a. Id -> [Graph a -> Graph a] -> Pending -> RoutingResult a
    CycleDetected (Id -> Id -> Id
    forall a. Ord a => a -> a -> a
    min Id
    d1 Id
    d2) ([Graph a -> Graph a]
    as1 [Graph a -> Graph a]
    -> [Graph a -> Graph a] -> [Graph a -> Graph a]
    forall a. [a] -> [a] -> [a]
    ++ [Graph a -> Graph a]
    as2) Pending
    p2
      RoutingResult a
    _ <> CycleDetected Id
    d [Graph a -> Graph a]
    as Pending
    p = Id -> [Graph a -> Graph a] -> Pending -> RoutingResult a
    forall a. Id -> [Graph a -> Graph a] -> Pending -> RoutingResult a
    CycleDetected Id
    d [Graph a -> Graph a]
    as Pending
    p
      CycleDetected Id
    d [Graph a -> Graph a]
    as Pending
    p <> RoutingResult a
    _ = Id -> [Graph a -> Graph a] -> Pending -> RoutingResult a
    forall a. Id -> [Graph a -> Graph a] -> Pending -> RoutingResult a
    CycleDetected Id
    d [Graph a -> Graph a]
    as Pending
    p
      RoutingResult a
    DeadEnd <> RoutingResult a
    DeadEnd = RoutingResult a
    forall a. RoutingResult a
    DeadEnd

    instance Monoid (RoutingResult a) where
      mempty :: RoutingResult a
    mempty = RoutingResult a
    forall a. RoutingResult a
    DeadEnd

    route' ::
      Pending ->
      Depth ->
      Maybe Id ->
      EdgeType ->
      Id ->
      Graph m ->
      (RoutingResult m, Graph m)
    route' :: forall m.
    Pending
    -> Id
    -> Maybe Id
    -> EdgeType
    -> Id
    -> Graph m
    -> (RoutingResult m, Graph m)
    route' Pending
    p Id
    d Maybe Id
    prev EdgeType
    et Id
    i Graph m
    g
      | Just Id
    d' <- Id -> Pending -> Maybe Id
    forall a. Id -> IntMap a -> Maybe a
    IM.lookup Id
    i Pending
    p =
          let found_cycle :: (RoutingResult a, Graph m)
    found_cycle = (Id -> [Graph a -> Graph a] -> Pending -> RoutingResult a
    forall a. Id -> [Graph a -> Graph a] -> Pending -> RoutingResult a
    CycleDetected Id
    d' [] Pending
    p, Graph m
    g)
           in case EdgeType
    et of
                -- Accessing some vertex v via a normal edge corresponds to accessing
                -- v_in via a normal edge. If v_in has a reversed edge then that is
                -- the only outgoing edge that is available.
                -- All outgoing edges available via this ingoing edge were already
                -- available via the edge that first reached the vertex.
                EdgeType
    Normal -> (RoutingResult m, Graph m)
    forall {a}. (RoutingResult a, Graph m)
    found_cycle
                -- Accessing some vertex v via a reversed edge corresponds to
                -- accessing v_out via a reversed edge. All other edges of v_out are
                -- available, and the edge from v_in to v_out has been reversed,
                -- implying that v_in has a single reversed edge that also is
                -- available.
                -- There exists at most one reversed edge to each vertex. Since this
                -- vertex was reached via one, and the vertex already have been
                -- reached, then the first reach must have been via a normal edge
                -- that only could traverse a reversed edge. The reversed edge from
                -- v_out to v_in thus completes a cycle, but a sink might be
                -- reachable via any of the other edges from v_out.
                -- The depth for the vertex need not be updated as this is the only
                -- edge to v_out and 'prev' is already in the 'Pending' map.
                -- It follows that no (new) cycle can start here.
                EdgeType
    Reversed ->
                  let (RoutingResult m
    res, Graph m
    g') = Vertex m -> Graph m -> Pending -> (RoutingResult m, Graph m)
    forall {a}.
    Vertex a -> Graph a -> Pending -> (RoutingResult a, Graph a)
    routeNormals (Maybe (Vertex m) -> Vertex m
    forall a. HasCallStack => Maybe a -> a
    fromJust (Maybe (Vertex m) -> Vertex m) -> Maybe (Vertex m) -> Vertex m
    forall a b. (a -> b) -> a -> b
    $ Id -> Graph m -> Maybe (Vertex m)
    forall m. Id -> Graph m -> Maybe (Vertex m)
    lookup Id
    i Graph m
    g) Graph m
    g Pending
    p
                   in ((RoutingResult m, Graph m) -> RoutingResult m
    forall a b. (a, b) -> a
    fst (RoutingResult m, Graph m)
    forall {a}. (RoutingResult a, Graph m)
    found_cycle RoutingResult m -> RoutingResult m -> RoutingResult m
    forall a. Semigroup a => a -> a -> a
    <> RoutingResult m
    res, Graph m
    g')
      | Just Vertex m
    v <- Id -> Graph m -> Maybe (Vertex m)
    forall m. Id -> Graph m -> Maybe (Vertex m)
    lookup Id
    i Graph m
    g =
          Vertex m -> (RoutingResult m, Graph m)
    routeVertex Vertex m
    v
      | Bool
    otherwise =
          (RoutingResult m, Graph m)
    forall {a}. (RoutingResult a, Graph m)
    backtrack
      where
        backtrack :: (RoutingResult a, Graph m)
    backtrack = (RoutingResult a
    forall a. RoutingResult a
    DeadEnd, Graph m
    g)

        routeVertex :: Vertex m -> (RoutingResult m, Graph m)
    routeVertex Vertex m
    v =
          case (EdgeType
    et, Vertex m -> Routing
    forall m. Vertex m -> Routing
    vertexRouting Vertex m
    v) of
            (EdgeType
    Normal, Routing
    FromSource) -> (RoutingResult m, Graph m)
    forall {a}. (RoutingResult a, Graph m)
    backtrack
            (EdgeType
    Normal, FromNode Id
    _ Exhaustion
    Exhausted) -> (RoutingResult m, Graph m)
    forall {a}. (RoutingResult a, Graph m)
    backtrack
            (EdgeType
    Normal, FromNode Id
    rev Exhaustion
    _) -> (Graph m -> Pending -> (RoutingResult m, Graph m))
    -> (RoutingResult m, Graph m)
    forall {a}.
    (Graph m -> Pending -> (RoutingResult a, Graph a))
    -> (RoutingResult a, Graph a)
    entry (Id -> Graph m -> Pending -> (RoutingResult m, Graph m)
    forall {m}. Id -> Graph m -> Pending -> (RoutingResult m, Graph m)
    routeReversed Id
    rev)
            (EdgeType
    Reversed, FromNode Id
    rev Exhaustion
    _) -> (Graph m -> Pending -> (RoutingResult m, Graph m))
    -> (RoutingResult m, Graph m)
    forall {a}.
    (Graph m -> Pending -> (RoutingResult a, Graph a))
    -> (RoutingResult a, Graph a)
    entry (Id -> Vertex m -> Graph m -> Pending -> (RoutingResult m, Graph m)
    forall {m}.
    Id -> Vertex m -> Graph m -> Pending -> (RoutingResult m, Graph m)
    routeAll Id
    rev Vertex m
    v)
            (EdgeType, Routing)
    _ -> (Graph m -> Pending -> (RoutingResult m, Graph m))
    -> (RoutingResult m, Graph m)
    forall {a}.
    (Graph m -> Pending -> (RoutingResult a, Graph a))
    -> (RoutingResult a, Graph a)
    entry (Vertex m -> Graph m -> Pending -> (RoutingResult m, Graph m)
    forall {a}.
    Vertex a -> Graph a -> Pending -> (RoutingResult a, Graph a)
    routeNormals Vertex m
    v)

        entry :: (Graph m -> Pending -> (RoutingResult a, Graph a))
    -> (RoutingResult a, Graph a)
    entry Graph m -> Pending -> (RoutingResult a, Graph a)
    f =
          let (RoutingResult a
    res, Graph a
    g0) = Graph m -> Pending -> (RoutingResult a, Graph a)
    f Graph m
    g (Id -> Id -> Pending -> Pending
    forall a. Id -> a -> IntMap a -> IntMap a
    IM.insert Id
    i Id
    d Pending
    p)
           in case RoutingResult a
    res of
                CycleDetected Id
    d' [Graph a -> Graph a]
    as Pending
    _
                  | Id
    d Id -> Id -> Bool
    forall a. Eq a => a -> a -> Bool
    == Id
    d' -> (RoutingResult a
    forall a. RoutingResult a
    DeadEnd, (Graph a -> (Graph a -> Graph a) -> Graph a)
    -> Graph a -> [Graph a -> Graph a] -> Graph a
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    L.foldl' (\Graph a
    g1 Graph a -> Graph a
    a -> Graph a -> Graph a
    a Graph a
    g1) Graph a
    g0 [Graph a -> Graph a]
    as)
                RoutingResult a
    _ | Bool
    otherwise -> (RoutingResult a
    res, Graph a
    g0)

        routeAll :: Id -> Vertex m -> Graph m -> Pending -> (RoutingResult m, Graph m)
    routeAll Id
    rev Vertex m
    v Graph m
    g0 Pending
    p0 =
          let (RoutingResult m
    res, Graph m
    g1) = Vertex m -> Graph m -> Pending -> (RoutingResult m, Graph m)
    forall {a}.
    Vertex a -> Graph a -> Pending -> (RoutingResult a, Graph a)
    routeNormals Vertex m
    v Graph m
    g0 Pending
    p0
           in case RoutingResult m
    res of
                RoutingResult m
    DeadEnd -> Id -> Graph m -> Pending -> (RoutingResult m, Graph m)
    forall {m}. Id -> Graph m -> Pending -> (RoutingResult m, Graph m)
    routeReversed Id
    rev Graph m
    g1 Pending
    p0
                CycleDetected Id
    _ [Graph m -> Graph m]
    _ Pending
    p1 ->
                  let (RoutingResult m
    res', Graph m
    g2) = Id -> Graph m -> Pending -> (RoutingResult m, Graph m)
    forall {m}. Id -> Graph m -> Pending -> (RoutingResult m, Graph m)
    routeReversed Id
    rev Graph m
    g1 Pending
    p1
                   in (RoutingResult m
    res RoutingResult m -> RoutingResult m -> RoutingResult m
    forall a. Semigroup a => a -> a -> a
    <> RoutingResult m
    res', Graph m
    g2)
                SinkFound Id
    _ -> (RoutingResult m
    res, Graph m
    g1)

        routeReversed :: Id -> Graph m -> Pending -> (RoutingResult m, Graph m)
    routeReversed Id
    rev Graph m
    g0 Pending
    p0 =
          let (RoutingResult m
    res, Graph m
    g') = Pending
    -> Id
    -> Maybe Id
    -> EdgeType
    -> Id
    -> Graph m
    -> (RoutingResult m, Graph m)
    forall m.
    Pending
    -> Id
    -> Maybe Id
    -> EdgeType
    -> Id
    -> Graph m
    -> (RoutingResult m, Graph m)
    route' Pending
    p0 (Id
    d Id -> Id -> Id
    forall a. Num a => a -> a -> a
    + Id
    1) (Id -> Maybe Id
    forall a. a -> Maybe a
    Just Id
    i) EdgeType
    Reversed Id
    rev Graph m
    g0
              exhaust :: Graph m -> Graph m
    exhaust = ((Vertex m -> Vertex m) -> Id -> Graph m -> Graph m)
    -> Id -> (Vertex m -> Vertex m) -> Graph m -> Graph m
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (Vertex m -> Vertex m) -> Id -> Graph m -> Graph m
    forall m. (Vertex m -> Vertex m) -> Id -> Graph m -> Graph m
    adjust Id
    i ((Vertex m -> Vertex m) -> Graph m -> Graph m)
    -> (Vertex m -> Vertex m) -> Graph m -> Graph m
    forall a b. (a -> b) -> a -> b
    $
                \Vertex m
    v -> Vertex m
    v {vertexRouting = FromNode rev Exhausted}
           in case (RoutingResult m
    res, EdgeType
    et) of
                (RoutingResult m
    DeadEnd, EdgeType
    _) ->
                  (RoutingResult m
    res, Graph m -> Graph m
    forall {m}. Graph m -> Graph m
    exhaust Graph m
    g')
                (CycleDetected Id
    d' [Graph m -> Graph m]
    as Pending
    p', EdgeType
    _) ->
                  (Id -> [Graph m -> Graph m] -> Pending -> RoutingResult m
    forall a. Id -> [Graph a -> Graph a] -> Pending -> RoutingResult a
    CycleDetected Id
    d' (Graph m -> Graph m
    forall {m}. Graph m -> Graph m
    exhaust (Graph m -> Graph m)
    -> [Graph m -> Graph m] -> [Graph m -> Graph m]
    forall a. a -> [a] -> [a]
    : [Graph m -> Graph m]
    as) Pending
    p', Graph m
    g')
                (SinkFound Id
    _, EdgeType
    Normal) ->
                  (RoutingResult m
    res, Graph m -> Graph m
    forall {m}. Graph m -> Graph m
    setRoute Graph m
    g')
                (SinkFound Id
    _, EdgeType
    Reversed) ->
                  let f :: Vertex m -> Vertex m
    f Vertex m
    v =
                        Vertex m
    v
                          { vertexEdges = withPrev (vertexEdges v),
                            vertexRouting = NoRoute
                          }
                   in (RoutingResult m
    res, (Vertex m -> Vertex m) -> Id -> Graph m -> Graph m
    forall m. (Vertex m -> Vertex m) -> Id -> Graph m -> Graph m
    adjust Vertex m -> Vertex m
    forall {m}. Vertex m -> Vertex m
    f Id
    i Graph m
    g')

        setRoute :: Graph m -> Graph m
    setRoute = (Vertex m -> Vertex m) -> Id -> Graph m -> Graph m
    forall m. (Vertex m -> Vertex m) -> Id -> Graph m -> Graph m
    adjust (\Vertex m
    v -> Vertex m
    v {vertexRouting = routing}) Id
    i

        routing :: Routing
    routing =
          case Maybe Id
    prev of
            Maybe Id
    Nothing -> Routing
    FromSource
            Just Id
    i' -> Id -> Exhaustion -> Routing
    FromNode Id
    i' Exhaustion
    NotExhausted

        withPrev :: Edges -> Edges
    withPrev Edges
    edges
          | Just Id
    i' <- Maybe Id
    prev,
            ToNodes IdSet
    es (Just IdSet
    es') <- Edges
    edges =
              IdSet -> Maybe IdSet -> Edges
    ToNodes IdSet
    es (IdSet -> Maybe IdSet
    forall a. a -> Maybe a
    Just (IdSet -> Maybe IdSet) -> IdSet -> Maybe IdSet
    forall a b. (a -> b) -> a -> b
    $ Id -> IdSet -> IdSet
    IS.insert Id
    i' IdSet
    es')
          | Bool
    otherwise =
              Edges
    edges -- shouldn't happen
        routeNormals :: Vertex a -> Graph a -> Pending -> (RoutingResult a, Graph a)
    routeNormals Vertex a
    v Graph a
    g0 Pending
    p0
          | Edges
    ToSink <- Vertex a -> Edges
    forall m. Vertex m -> Edges
    vertexEdges Vertex a
    v =
              -- There cannot be a reversed edge to a vertex with an edge to a sink.
              (Id -> RoutingResult a
    forall a. Id -> RoutingResult a
    SinkFound Id
    i, Graph a -> Graph a
    forall {m}. Graph m -> Graph m
    setRoute Graph a
    g0)
          | ToNodes IdSet
    es Maybe IdSet
    nx <- Vertex a -> Edges
    forall m. Vertex m -> Edges
    vertexEdges Vertex a
    v =
              let (RoutingResult a
    res, Graph a
    g', [Id]
    nx') =
                    case Maybe IdSet
    nx of
                      Just IdSet
    es' -> [Id] -> Graph a -> Pending -> (RoutingResult a, Graph a, [Id])
    forall {a}.
    [Id] -> Graph a -> Pending -> (RoutingResult a, Graph a, [Id])
    routeNorms (IdSet -> [Id]
    IS.toAscList IdSet
    es') Graph a
    g0 Pending
    p0
                      Maybe IdSet
    Nothing -> [Id] -> Graph a -> Pending -> (RoutingResult a, Graph a, [Id])
    forall {a}.
    [Id] -> Graph a -> Pending -> (RoutingResult a, Graph a, [Id])
    routeNorms (IdSet -> [Id]
    IS.toAscList IdSet
    es) Graph a
    g0 Pending
    p0
                  edges :: Edges
    edges = IdSet -> Maybe IdSet -> Edges
    ToNodes IdSet
    es (IdSet -> Maybe IdSet
    forall a. a -> Maybe a
    Just (IdSet -> Maybe IdSet) -> IdSet -> Maybe IdSet
    forall a b. (a -> b) -> a -> b
    $ [Id] -> IdSet
    IS.fromDistinctAscList [Id]
    nx')
                  exhaust :: Graph m -> Graph m
    exhaust = ((Vertex m -> Vertex m) -> Id -> Graph m -> Graph m)
    -> Id -> (Vertex m -> Vertex m) -> Graph m -> Graph m
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (Vertex m -> Vertex m) -> Id -> Graph m -> Graph m
    forall m. (Vertex m -> Vertex m) -> Id -> Graph m -> Graph m
    adjust Id
    i ((Vertex m -> Vertex m) -> Graph m -> Graph m)
    -> (Vertex m -> Vertex m) -> Graph m -> Graph m
    forall a b. (a -> b) -> a -> b
    $ \Vertex m
    v' ->
                    Vertex m
    v' {vertexEdges = ToNodes es (Just IS.empty)}
               in case (RoutingResult a
    res, EdgeType
    et) of
                    (RoutingResult a
    DeadEnd, EdgeType
    _) -> (RoutingResult a
    res, Graph a -> Graph a
    forall {m}. Graph m -> Graph m
    exhaust Graph a
    g')
                    (CycleDetected Id
    d' [Graph a -> Graph a]
    as Pending
    p', EdgeType
    _) ->
                      let res' :: RoutingResult a
    res' = Id -> [Graph a -> Graph a] -> Pending -> RoutingResult a
    forall a. Id -> [Graph a -> Graph a] -> Pending -> RoutingResult a
    CycleDetected Id
    d' (Graph a -> Graph a
    forall {m}. Graph m -> Graph m
    exhaust (Graph a -> Graph a)
    -> [Graph a -> Graph a] -> [Graph a -> Graph a]
    forall a. a -> [a] -> [a]
    : [Graph a -> Graph a]
    as) Pending
    p'
                          v' :: Vertex a
    v' = Vertex a
    v {vertexEdges = edges}
                       in (RoutingResult a
    res', Vertex a -> Graph a -> Graph a
    forall m. Vertex m -> Graph m -> Graph m
    insert Vertex a
    v' Graph a
    g')
                    (SinkFound Id
    _, EdgeType
    Normal) ->
                      let v' :: Vertex a
    v' = Vertex a
    v {vertexEdges = edges, vertexRouting = routing}
                       in (RoutingResult a
    res, Vertex a -> Graph a -> Graph a
    forall m. Vertex m -> Graph m -> Graph m
    insert Vertex a
    v' Graph a
    g')
                    (SinkFound Id
    _, EdgeType
    Reversed) ->
                      let v' :: Vertex a
    v' = Vertex a
    v {vertexEdges = withPrev edges}
                       in (RoutingResult a
    res, Vertex a -> Graph a -> Graph a
    forall m. Vertex m -> Graph m -> Graph m
    insert Vertex a
    v' Graph a
    g')

        routeNorms :: [Id] -> Graph a -> Pending -> (RoutingResult a, Graph a, [Id])
    routeNorms [] Graph a
    g0 Pending
    _ = (RoutingResult a
    forall a. RoutingResult a
    DeadEnd, Graph a
    g0, [])
        routeNorms (Id
    e : [Id]
    es) Graph a
    g0 Pending
    p0 =
          let (RoutingResult a
    res, Graph a
    g1) = Pending
    -> Id
    -> Maybe Id
    -> EdgeType
    -> Id
    -> Graph a
    -> (RoutingResult a, Graph a)
    forall m.
    Pending
    -> Id
    -> Maybe Id
    -> EdgeType
    -> Id
    -> Graph m
    -> (RoutingResult m, Graph m)
    route' Pending
    p0 (Id
    d Id -> Id -> Id
    forall a. Num a => a -> a -> a
    + Id
    1) (Id -> Maybe Id
    forall a. a -> Maybe a
    Just Id
    i) EdgeType
    Normal Id
    e Graph a
    g0
           in case RoutingResult a
    res of
                RoutingResult a
    DeadEnd -> [Id] -> Graph a -> Pending -> (RoutingResult a, Graph a, [Id])
    routeNorms [Id]
    es Graph a
    g1 Pending
    p0
                SinkFound Id
    _ -> (RoutingResult a
    res, Graph a
    g1, [Id]
    es)
                CycleDetected Id
    _ [Graph a -> Graph a]
    _ Pending
    p1 ->
                  let (RoutingResult a
    res', Graph a
    g2, [Id]
    es') = [Id] -> Graph a -> Pending -> (RoutingResult a, Graph a, [Id])
    routeNorms [Id]
    es Graph a
    g1 Pending
    p1
                   in (RoutingResult a
    res RoutingResult a -> RoutingResult a -> RoutingResult a
    forall a. Semigroup a => a -> a -> a
    <> RoutingResult a
    res', Graph a
    g2, Id
    e Id -> [Id] -> [Id]
    forall a. a -> [a] -> [a]
    : [Id]
    es')