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
xforall a. a -> [a] -> [a]
: forall a. (a -> a -> Bool) -> [a] -> [a] -> [a]
mergeBy a -> a -> Bool
f [a]
xs (a
yforall a. a -> [a] -> [a]
:[a]
ys)
    | Bool
otherwise = a
yforall a. a -> [a] -> [a]
: forall a. (a -> a -> Bool) -> [a] -> [a] -> [a]
mergeBy a -> a -> Bool
f (a
xforall 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 [] (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      = 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      = forall n e. (Ord n, Eq e, StarSemiRing e) => Graph n e -> Graph n e
G.transitiveClosure forall a b. (a -> b) -> a -> b
$
               forall n e. Ord n => Set n -> Graph n e
G.fromNodeSet Set n
nodes forall n e. Ord n => Graph n e -> Graph n e -> Graph n e
`G.union`
               forall n e. Ord n => [Edge n e] -> Graph n e
G.fromEdges [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 = forall n e. Graph n e -> Map n (Map n e)
G.graph Graph n (Maybe ())
g 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 [] = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map 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) 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 [] = 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 = forall a. Maybe a
Nothing
      | Bool
before          = ((n
b, 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) forall a. a -> [a] -> [a]
:) 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       = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ (n
a, 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) 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 = forall k a. Ord k => k -> Map k a -> Bool
Map.member n
a Map n (Maybe ())
before_b
        after :: Bool
after  = forall k a. Ord k => k -> Map k a -> Bool
Map.member n
b Map n (Maybe ())
before_a