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