    {-# OPTIONS_GHC -Wunused-imports #-}

    module Agda.Utils.Graph.TopSort
        ( topSort
        ) where

    import Data.Set (Set)
    import qualified Data.Set as Set
    import qualified Data.Map as Map
    import qualified Agda.Utils.Graph.AdjacencyMap.Unidirectional as G

    -- NB:: Defined but not used
    mergeBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]
    mergeBy :: forall a. (a -> a -> Bool) -> [a] -> [a] -> [a]
    mergeBy a -> a -> Bool
    _ [] [a]
    xs = [a]
    xs
    mergeBy a -> a -> Bool
    _ [a]
    xs [] = [a]
    xs
    mergeBy a -> a -> Bool
    f (a
    x:[a]
    xs) (a
    y:[a]
    ys)
        | a -> a -> Bool
    f a
    x a
    y = a
    xa -> [a] -> [a]
    forall a. a -> [a] -> [a]
    : (a -> a -> Bool) -> [a] -> [a] -> [a]
    forall a. (a -> a -> Bool) -> [a] -> [a] -> [a]
    mergeBy a -> a -> Bool
    f [a]
    xs (a
    ya -> [a] -> [a]
    forall a. a -> [a] -> [a]
    :[a]
    ys)
        | Bool
    otherwise = a
    ya -> [a] -> [a]
    forall a. a -> [a] -> [a]
    : (a -> a -> Bool) -> [a] -> [a] -> [a]
    forall a. (a -> a -> Bool) -> [a] -> [a] -> [a]
    mergeBy a -> a -> Bool
    f (a
    xa -> [a] -> [a]
    forall a. a -> [a] -> [a]
    :[a]
    xs) [a]
    ys

    -- | topoligical sort with smallest-numbered available vertex first
    -- | input: nodes, edges
    -- | output is Nothing if the graph is not a DAG
    --   Note: should be stable to preserve order of generalizable variables. Algorithm due to Richard
    --   Eisenberg, and works by walking over the list left-to-right and moving each node the minimum
    --   distance left to guarantee topological ordering.
    topSort :: Ord n => Set n -> [(n, n)] -> Maybe [n]
    topSort :: forall n. Ord n => Set n -> [(n, n)] -> Maybe [n]
    topSort Set n
    nodes [(n, n)]
    edges = [(n, Map n (Maybe ()))] -> [n] -> Maybe [n]
    go [] (Set n -> [n]
    forall a. Set a -> [a]
    Set.toList Set n
    nodes)
      where
        -- #4253: The input edges do not necessarily include transitive dependencies, so take transitive
        --        closure before sorting.
        w :: Maybe ()
    w      = () -> Maybe ()
    forall a. a -> Maybe a
    Just () -- () is not a good edge label since it counts as a "zero" edge and will be ignored
        g :: Graph n (Maybe ())
    g      = Graph n (Maybe ()) -> Graph n (Maybe ())
    forall n e. (Ord n, Eq e, StarSemiRing e) => Graph n e -> Graph n e
    G.transitiveClosure (Graph n (Maybe ()) -> Graph n (Maybe ()))
    -> Graph n (Maybe ()) -> Graph n (Maybe ())
    forall a b. (a -> b) -> a -> b
    $
                   Set n -> Graph n (Maybe ())
    forall n e. Ord n => Set n -> Graph n e
    G.fromNodeSet Set n
    nodes Graph n (Maybe ()) -> Graph n (Maybe ()) -> Graph n (Maybe ())
    forall n e. Ord n => Graph n e -> Graph n e -> Graph n e
    `G.union`
                   [Edge n (Maybe ())] -> Graph n (Maybe ())
    forall n e. Ord n => [Edge n e] -> Graph n e
    G.fromEdges [n -> n -> Maybe () -> Edge n (Maybe ())
    forall n e. n -> n -> e -> Edge n e
    G.Edge n
    a n
    b Maybe ()
    w | (n
    a, n
    b) <- [(n, n)]
    edges]
        -- Only the keys of these maps are used.
        deps :: n -> Map n (Maybe ())
    deps n
    a = Graph n (Maybe ()) -> Map n (Map n (Maybe ()))
    forall n e. Graph n e -> Map n (Map n e)
    G.graph Graph n (Maybe ())
    g Map n (Map n (Maybe ())) -> n -> Map n (Maybe ())
    forall k a. Ord k => Map k a -> k -> a
    Map.! n
    a

        -- acc: Already sorted nodes in reverse order paired with accumulated set of nodes that must
        -- come before it
        go :: [(n, Map n (Maybe ()))] -> [n] -> Maybe [n]
    go [(n, Map n (Maybe ()))]
    acc [] = [n] -> Maybe [n]
    forall a. a -> Maybe a
    Just ([n] -> Maybe [n]) -> [n] -> Maybe [n]
    forall a b. (a -> b) -> a -> b
    $ [n] -> [n]
    forall a. [a] -> [a]
    reverse ([n] -> [n]) -> [n] -> [n]
    forall a b. (a -> b) -> a -> b
    $ ((n, Map n (Maybe ())) -> n) -> [(n, Map n (Maybe ()))] -> [n]
    forall a b. (a -> b) -> [a] -> [b]
    map (n, Map n (Maybe ())) -> n
    forall a b. (a, b) -> a
    fst [(n, Map n (Maybe ()))]
    acc
        go [(n, Map n (Maybe ()))]
    acc (n
    n : [n]
    ns) = ([(n, Map n (Maybe ()))] -> [n] -> Maybe [n]
    `go` [n]
    ns) ([(n, Map n (Maybe ()))] -> Maybe [n])
    -> Maybe [(n, Map n (Maybe ()))] -> Maybe [n]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< n -> [(n, Map n (Maybe ()))] -> Maybe [(n, Map n (Maybe ()))]
    insert n
    n [(n, Map n (Maybe ()))]
    acc

        insert :: n -> [(n, Map n (Maybe ()))] -> Maybe [(n, Map n (Maybe ()))]
    insert n
    a [] = [(n, Map n (Maybe ()))] -> Maybe [(n, Map n (Maybe ()))]
    forall a. a -> Maybe a
    Just [(n
    a, n -> Map n (Maybe ())
    deps n
    a)]
        insert n
    a bs0 :: [(n, Map n (Maybe ()))]
    bs0@((n
    b, Map n (Maybe ())
    before_b) : [(n, Map n (Maybe ()))]
    bs)
          | Bool
    before Bool -> Bool -> Bool
    && Bool
    after = Maybe [(n, Map n (Maybe ()))]
    forall a. Maybe a
    Nothing
          | Bool
    before          = ((n
    b, Map n (Maybe ()) -> Map n (Maybe ()) -> Map n (Maybe ())
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    Map.union Map n (Maybe ())
    before_a Map n (Maybe ())
    before_b) (n, Map n (Maybe ()))
    -> [(n, Map n (Maybe ()))] -> [(n, Map n (Maybe ()))]
    forall a. a -> [a] -> [a]
    :) ([(n, Map n (Maybe ()))] -> [(n, Map n (Maybe ()))])
    -> Maybe [(n, Map n (Maybe ()))] -> Maybe [(n, Map n (Maybe ()))]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> n -> [(n, Map n (Maybe ()))] -> Maybe [(n, Map n (Maybe ()))]
    insert n
    a [(n, Map n (Maybe ()))]
    bs  -- a must come before b
          | Bool
    otherwise       = [(n, Map n (Maybe ()))] -> Maybe [(n, Map n (Maybe ()))]
    forall a. a -> Maybe a
    Just ([(n, Map n (Maybe ()))] -> Maybe [(n, Map n (Maybe ()))])
    -> [(n, Map n (Maybe ()))] -> Maybe [(n, Map n (Maybe ()))]
    forall a b. (a -> b) -> a -> b
    $ (n
    a, Map n (Maybe ()) -> Map n (Maybe ()) -> Map n (Maybe ())
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    Map.union Map n (Maybe ())
    before_a Map n (Maybe ())
    before_b) (n, Map n (Maybe ()))
    -> [(n, Map n (Maybe ()))] -> [(n, Map n (Maybe ()))]
    forall a. a -> [a] -> [a]
    : [(n, Map n (Maybe ()))]
    bs0
          where
            before_a :: Map n (Maybe ())
    before_a = n -> Map n (Maybe ())
    deps n
    a
            before :: Bool
    before = n -> Map n (Maybe ()) -> Bool
    forall k a. Ord k => k -> Map k a -> Bool
    Map.member n
    a Map n (Maybe ())
    before_b
            after :: Bool
    after  = n -> Map n (Maybe ()) -> Bool
    forall k a. Ord k => k -> Map k a -> Bool
    Map.member n
    b Map n (Maybe ())
    before_a