module UVMHS.Lib.Graph where

import UVMHS.Core

-- | A `Graph` has node elements `a`, and is just a relation between nodes.
--
-- Notation: 
--
--     kvss : Graph a
--
-- (same as general dictionaries)
type Graph a = a ⇰ 𝑃 a

-- | Property:
--
--     (v ↦ ks) ∈ graph-transpose(kvss) ⟺ ∀ (k ↦ vs) ∈ kvss. k ∈ ks ⟺ v ∈ vs
graphTranspose ∷ ∀ a. (Ord a) ⇒ Graph a → Graph a
graphTranspose :: forall a. Ord a => Graph a -> Graph a
graphTranspose Graph a
kvss = [Graph a] -> Graph a
forall a t. (JoinLattice a, ToIter a t) => t -> a
joins
  [ 𝐼 (Graph a) -> Graph a
forall (d :: * -> *) t a k s.
(Dict k s d, ToIter (d a) t) =>
t -> d a
dict (𝐼 (Graph a) -> Graph a) -> 𝐼 (Graph a) -> Graph a
forall a b. (a -> b) -> a -> b
$ 𝐼 a -> (a -> Graph a) -> 𝐼 (Graph a)
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn (𝑃 a -> 𝐼 a
forall a t. ToIter a t => t -> 𝐼 a
iter (𝑃 a -> 𝐼 a) -> 𝑃 a -> 𝐼 a
forall a b. (a -> b) -> a -> b
$ Graph a -> 𝑃 a
forall a. (a ⇰ a) -> 𝑃 a
forall k s (d :: * -> *) a. Dict k s d => d a -> s
dkeys Graph a
kvss) ((a -> Graph a) -> 𝐼 (Graph a)) -> (a -> Graph a) -> 𝐼 (Graph a)
forall a b. (a -> b) -> a -> b
$ \ a
k → a
k a -> 𝑃 a -> Graph a
forall a. a -> a -> a ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ 𝑃 a
forall e s. Set e s => s
pø
  , 𝐼 (Graph a) -> Graph a
forall a t. (JoinLattice a, ToIter a t) => t -> a
joins (𝐼 (Graph a) -> Graph a) -> 𝐼 (Graph a) -> Graph a
forall a b. (a -> b) -> a -> b
$ 𝐼 (a ∧ 𝑃 a) -> ((a ∧ 𝑃 a) -> Graph a) -> 𝐼 (Graph a)
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn (Graph a -> 𝐼 (a ∧ 𝑃 a)
forall a t. ToIter a t => t -> 𝐼 a
iter Graph a
kvss) (((a ∧ 𝑃 a) -> Graph a) -> 𝐼 (Graph a))
-> ((a ∧ 𝑃 a) -> Graph a) -> 𝐼 (Graph a)
forall a b. (a -> b) -> a -> b
$ \ (a
k :* 𝑃 a
vs) →
      𝐼 (Graph a) -> Graph a
forall (d :: * -> *) t a k s.
(Dict k s d, ToIter (d a) t) =>
t -> d a
dict (𝐼 (Graph a) -> Graph a) -> 𝐼 (Graph a) -> Graph a
forall a b. (a -> b) -> a -> b
$ 𝐼 a -> (a -> Graph a) -> 𝐼 (Graph a)
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn (𝑃 a -> 𝐼 a
forall a t. ToIter a t => t -> 𝐼 a
iter 𝑃 a
vs) ((a -> Graph a) -> 𝐼 (Graph a)) -> (a -> Graph a) -> 𝐼 (Graph a)
forall a b. (a -> b) -> a -> b
$ \ a
v → a
v a -> 𝑃 a -> Graph a
forall a. a -> a -> a ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ a -> 𝑃 a
forall a t. Single a t => a -> t
single a
k
  ]

-- | Run the Kosaraju algorithm, which computes strongly connected components.
-- The algorithm computes a canonical node for each strongly connected
-- component, and maps each node to the canonical node for strongly connected
-- component in which it lives.
--
-- Definition: 
--
--     strongly-connected ∈ ℘(Graph)
--     strongly-connected(kvss) ≜ 
--       ∀ k₁,k₂ ∈ nodes(kvss). ∃ path(k₁,k₂)
--     strongly-connected-components ∈ ℘(℘(Graph))
--     strongly-connected-components(kvsss) ≜ 
--         (∀ kvss ∈ kvsss. strongly-connected(kvss))
--       ∧ (∀ kvss₁,kvss₂ ∈ kvsss. ¬strongly-connected(kvss₁ ∪kvss₂))
--
-- Property: 
-- 
--     ∀ kvss. 
--       strongly-connected-components(
--         values(
--           graph-transpose(
--             { k ↦ {v} 
--             | (k ↦ v) ∈ kosaraju(kvss)
--             }
kosaraju ∷ ∀ a. (Ord a) ⇒ Graph a → a ⇰ a
kosaraju :: forall a. Ord a => Graph a -> a ⇰ a
kosaraju Graph a
g =
  let gᵀ :: Graph a
gᵀ = Graph a -> Graph a
forall a. Ord a => Graph a -> Graph a
graphTranspose Graph a
g

      visit ∷ a → 𝑃 a → 𝐿 a → 𝑃 a ∧ 𝐿 a
      visit :: a -> 𝑃 a -> 𝐿 a -> 𝑃 a ∧ 𝐿 a
visit a
u 𝑃 a
visited 𝐿 a
stack =
        if a
u a -> 𝑃 a -> 𝔹
forall e s. Set e s => e -> s -> 𝔹
∈ 𝑃 a
visited
        then 𝑃 a
visited 𝑃 a -> 𝐿 a -> 𝑃 a ∧ 𝐿 a
forall a b. a -> b -> a ∧ b
:* 𝐿 a
stack
        else
          let visited' :: 𝑃 a
visited' = a -> 𝑃 a
forall a t. Single a t => a -> t
single a
u 𝑃 a -> 𝑃 a -> 𝑃 a
forall e s. Set e s => s -> s -> s
∪ 𝑃 a
visited
              𝑃 a
visited'' :* 𝐿 a
stack' =
                𝑃 a -> (𝑃 a ∧ 𝐿 a) -> (a -> (𝑃 a ∧ 𝐿 a) -> 𝑃 a ∧ 𝐿 a) -> 𝑃 a ∧ 𝐿 a
forall a t b. ToIter a t => t -> b -> (a -> b -> b) -> b
foldOnFrom (Graph a
g Graph a -> a -> 𝑃 a
forall k v t. (Lookup k v t, STACK) => t -> k -> v
⋕! a
u) (𝑃 a
visited' 𝑃 a -> 𝐿 a -> 𝑃 a ∧ 𝐿 a
forall a b. a -> b -> a ∧ b
:* 𝐿 a
stack) ((a -> (𝑃 a ∧ 𝐿 a) -> 𝑃 a ∧ 𝐿 a) -> 𝑃 a ∧ 𝐿 a)
-> (a -> (𝑃 a ∧ 𝐿 a) -> 𝑃 a ∧ 𝐿 a) -> 𝑃 a ∧ 𝐿 a
forall a b. (a -> b) -> a -> b
$ \ a
v (𝑃 a
visitedᵢ :* 𝐿 a
stackᵢ) →
                  a -> 𝑃 a -> 𝐿 a -> 𝑃 a ∧ 𝐿 a
visit a
v 𝑃 a
visitedᵢ 𝐿 a
stackᵢ
              stack'' :: 𝐿 a
stack'' = a
u a -> 𝐿 a -> 𝐿 a
forall a. a -> 𝐿 a -> 𝐿 a
:& 𝐿 a
stack'
          in 𝑃 a
visited'' 𝑃 a -> 𝐿 a -> 𝑃 a ∧ 𝐿 a
forall a b. a -> b -> a ∧ b
:* 𝐿 a
stack''

      assign ∷ a → a → a ⇰ a → a ⇰ a
      assign :: a -> a -> (a ⇰ a) -> a ⇰ a
assign a
u a
anchor a ⇰ a
sccs =
        if a
u a -> (a ⇰ a) -> 𝔹
forall a. a -> (a ⇰ a) -> 𝔹
forall k s (d :: * -> *) a. Dict k s d => k -> d a -> 𝔹
⋿ a ⇰ a
sccs
        then a ⇰ a
sccs
        else
          let sccs' :: a ⇰ a
sccs' = (a
u a -> a -> a ⇰ a
forall a. a -> a -> a ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ a
anchor) (a ⇰ a) -> (a ⇰ a) -> a ⇰ a
forall a. (a ⇰ a) -> (a ⇰ a) -> a ⇰ a
forall k s (d :: * -> *) a. Dict k s d => d a -> d a -> d a
⩌ a ⇰ a
sccs
              sccs'' :: a ⇰ a
sccs'' = 𝑃 a -> (a ⇰ a) -> (a -> (a ⇰ a) -> a ⇰ a) -> a ⇰ a
forall a t b. ToIter a t => t -> b -> (a -> b -> b) -> b
foldOnFrom (Graph a
gᵀ Graph a -> a -> 𝑃 a
forall k v t. (Lookup k v t, STACK) => t -> k -> v
⋕! a
u) a ⇰ a
sccs' ((a -> (a ⇰ a) -> a ⇰ a) -> a ⇰ a)
-> (a -> (a ⇰ a) -> a ⇰ a) -> a ⇰ a
forall a b. (a -> b) -> a -> b
$ \ a
v a ⇰ a
sccsᵢ → a -> a -> (a ⇰ a) -> a ⇰ a
assign a
v a
anchor a ⇰ a
sccsᵢ
          in a ⇰ a
sccs''

      visited₀ ∷ 𝑃 a
      visited₀ :: 𝑃 a
visited₀ = 𝑃 a
forall e s. Set e s => s
pø
      stack₀ ∷ 𝐿 a
      stack₀ :: 𝐿 a
stack₀ = 𝐿 a
forall a. 𝐿 a
Nil
      sccs₀ :: a ⇰ a
sccs₀ = a ⇰ a
forall a. a ⇰ a
forall k s (d :: * -> *) a. Dict k s d => d a
dø

      stackᵣ :: 𝐿 a
stackᵣ = (𝑃 a ∧ 𝐿 a) -> 𝐿 a
forall a b. (a ∧ b) -> b
snd ((𝑃 a ∧ 𝐿 a) -> 𝐿 a) -> (𝑃 a ∧ 𝐿 a) -> 𝐿 a
forall a b. (a -> b) -> a -> b
$ 𝑃 a -> (𝑃 a ∧ 𝐿 a) -> (a -> (𝑃 a ∧ 𝐿 a) -> 𝑃 a ∧ 𝐿 a) -> 𝑃 a ∧ 𝐿 a
forall a t b. ToIter a t => t -> b -> (a -> b -> b) -> b
foldOnFrom (Graph a -> 𝑃 a
forall a. (a ⇰ a) -> 𝑃 a
forall k s (d :: * -> *) a. Dict k s d => d a -> s
dkeys Graph a
g) (𝑃 a
visited₀ 𝑃 a -> 𝐿 a -> 𝑃 a ∧ 𝐿 a
forall a b. a -> b -> a ∧ b
:* 𝐿 a
stack₀) ((a -> (𝑃 a ∧ 𝐿 a) -> 𝑃 a ∧ 𝐿 a) -> 𝑃 a ∧ 𝐿 a)
-> (a -> (𝑃 a ∧ 𝐿 a) -> 𝑃 a ∧ 𝐿 a) -> 𝑃 a ∧ 𝐿 a
forall a b. (a -> b) -> a -> b
$ \ a
u (𝑃 a
visitedᵢ :* 𝐿 a
stackᵢ) →
        a -> 𝑃 a -> 𝐿 a -> 𝑃 a ∧ 𝐿 a
visit a
u 𝑃 a
visitedᵢ 𝐿 a
stackᵢ

      sccsᵣ :: a ⇰ a
sccsᵣ = 𝐿 a -> (a ⇰ a) -> (a -> (a ⇰ a) -> a ⇰ a) -> a ⇰ a
forall a t b. ToIter a t => t -> b -> (a -> b -> b) -> b
foldOnFrom 𝐿 a
stackᵣ a ⇰ a
forall a. a ⇰ a
sccs₀ ((a -> (a ⇰ a) -> a ⇰ a) -> a ⇰ a)
-> (a -> (a ⇰ a) -> a ⇰ a) -> a ⇰ a
forall a b. (a -> b) -> a -> b
$ \ a
u a ⇰ a
sccsᵢ → a -> a -> (a ⇰ a) -> a ⇰ a
assign a
u a
u a ⇰ a
sccsᵢ

  in a ⇰ a
sccsᵣ

-- | In the context of this function, we treat the element `a` like variables
-- that have a definition/use structure. The first argument `deps` encodes
-- dependencies from definitions of things to uses of things.
--
-- From a dependency relation, compute two elements:
-- 1. The strongly connected components for the dependency relation,
--    represented as a map from variables to a canonical SCC elements for its
--    dependency group
-- 2. A map from canonical SCC elements to:
--    (a). All variables in its dependency group (i.e., the inverse of (1))
--    (b). All dependencies of all variables in the dependnecy group
--
-- (1) is computed using `kosaraju`, but with an additional bit of information
-- in the node representation that encodes def/use information, following these
-- two semantic ideas:
-- - *Use* of any variable `x` depends on the *definition* of that variable `x`
-- - If `{x ↦ y}` appears in `deps`, this means that *definition* of variable
--   `x` depends on *use* of variable `y`.
sccGroups ∷ ∀ a. (Ord a) ⇒ a ⇰ 𝑃 a → (a ⇰ a) ∧ (a ⇰ 𝑃 a ∧ 𝑃 a)
sccGroups :: forall a. Ord a => (a ⇰ 𝑃 a) -> (a ⇰ a) ∧ (a ⇰ (𝑃 a ∧ 𝑃 a))
sccGroups a ⇰ 𝑃 a
deps =
  let graph ∷ a ∧ 𝔹 ⇰ 𝑃 (a ∧ 𝔹)
      graph :: (a ∧ 𝔹) ⇰ 𝑃 (a ∧ 𝔹)
graph = 𝐼 ((a ∧ 𝔹) ⇰ 𝑃 (a ∧ 𝔹)) -> (a ∧ 𝔹) ⇰ 𝑃 (a ∧ 𝔹)
forall a t. (JoinLattice a, ToIter a t) => t -> a
joins (𝐼 ((a ∧ 𝔹) ⇰ 𝑃 (a ∧ 𝔹)) -> (a ∧ 𝔹) ⇰ 𝑃 (a ∧ 𝔹))
-> 𝐼 ((a ∧ 𝔹) ⇰ 𝑃 (a ∧ 𝔹)) -> (a ∧ 𝔹) ⇰ 𝑃 (a ∧ 𝔹)
forall a b. (a -> b) -> a -> b
$ 𝐼 (a ∧ 𝑃 a)
-> ((a ∧ 𝑃 a) -> (a ∧ 𝔹) ⇰ 𝑃 (a ∧ 𝔹)) -> 𝐼 ((a ∧ 𝔹) ⇰ 𝑃 (a ∧ 𝔹))
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn ((a ⇰ 𝑃 a) -> 𝐼 (a ∧ 𝑃 a)
forall a t. ToIter a t => t -> 𝐼 a
iter a ⇰ 𝑃 a
deps) (((a ∧ 𝑃 a) -> (a ∧ 𝔹) ⇰ 𝑃 (a ∧ 𝔹)) -> 𝐼 ((a ∧ 𝔹) ⇰ 𝑃 (a ∧ 𝔹)))
-> ((a ∧ 𝑃 a) -> (a ∧ 𝔹) ⇰ 𝑃 (a ∧ 𝔹)) -> 𝐼 ((a ∧ 𝔹) ⇰ 𝑃 (a ∧ 𝔹))
forall a b. (a -> b) -> a -> b
$ \ (a
x :* 𝑃 a
xs) → [(a ∧ 𝔹) ⇰ 𝑃 (a ∧ 𝔹)] -> (a ∧ 𝔹) ⇰ 𝑃 (a ∧ 𝔹)
forall (d :: * -> *) t a k s.
(Dict k s d, ToIter (d a) t) =>
t -> d a
dict
        [ -- variable use (False) depends (↦) on its definition (True)
          (a
x a -> 𝔹 -> a ∧ 𝔹
forall a b. a -> b -> a ∧ b
:* 𝔹
False) (a ∧ 𝔹) -> 𝑃 (a ∧ 𝔹) -> (a ∧ 𝔹) ⇰ 𝑃 (a ∧ 𝔹)
forall a. (a ∧ 𝔹) -> a -> (a ∧ 𝔹) ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ (a ∧ 𝔹) -> 𝑃 (a ∧ 𝔹)
forall a t. Single a t => a -> t
single (a
x a -> 𝔹 -> a ∧ 𝔹
forall a b. a -> b -> a ∧ b
:* 𝔹
True)
        , -- variable definition (True) depends (↦) on dependency uses (False)
          (a
x a -> 𝔹 -> a ∧ 𝔹
forall a b. a -> b -> a ∧ b
:* 𝔹
True) (a ∧ 𝔹) -> 𝑃 (a ∧ 𝔹) -> (a ∧ 𝔹) ⇰ 𝑃 (a ∧ 𝔹)
forall a. (a ∧ 𝔹) -> a -> (a ∧ 𝔹) ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ 𝐼 (a ∧ 𝔹) -> 𝑃 (a ∧ 𝔹)
forall s t e. (ToIter e t, Set e s) => t -> s
pow ((a -> a ∧ 𝔹) -> 𝐼 a -> 𝐼 (a ∧ 𝔹)
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (a -> 𝔹 -> a ∧ 𝔹
forall a b. a -> b -> a ∧ b
:* 𝔹
False) (𝐼 a -> 𝐼 (a ∧ 𝔹)) -> 𝐼 a -> 𝐼 (a ∧ 𝔹)
forall a b. (a -> b) -> a -> b
$ 𝑃 a -> 𝐼 a
forall a t. ToIter a t => t -> 𝐼 a
iter 𝑃 a
xs)
        ]
      -- mapping from def/use to a canonical representative for its scc equivalence class
      sccsDefuse ∷ a ∧ 𝔹 ⇰ a ∧ 𝔹
      sccsDefuse :: (a ∧ 𝔹) ⇰ (a ∧ 𝔹)
sccsDefuse = ((a ∧ 𝔹) ⇰ 𝑃 (a ∧ 𝔹)) -> (a ∧ 𝔹) ⇰ (a ∧ 𝔹)
forall a. Ord a => Graph a -> a ⇰ a
kosaraju (a ∧ 𝔹) ⇰ 𝑃 (a ∧ 𝔹)
graph
      -- throw out def/use information and just map variables to groups
      sccs ∷ a ⇰ a
      sccs :: a ⇰ a
sccs = 𝐼 (a ⇰ a) -> a ⇰ a
forall (d :: * -> *) t a k s.
(Dict k s d, ToIter (d a) t) =>
t -> d a
dict (𝐼 (a ⇰ a) -> a ⇰ a) -> 𝐼 (a ⇰ a) -> a ⇰ a
forall a b. (a -> b) -> a -> b
$ 𝐼 ((a ∧ 𝔹) ∧ (a ∧ 𝔹))
-> (((a ∧ 𝔹) ∧ (a ∧ 𝔹)) -> a ⇰ a) -> 𝐼 (a ⇰ a)
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn (((a ∧ 𝔹) ⇰ (a ∧ 𝔹)) -> 𝐼 ((a ∧ 𝔹) ∧ (a ∧ 𝔹))
forall a t. ToIter a t => t -> 𝐼 a
iter (a ∧ 𝔹) ⇰ (a ∧ 𝔹)
sccsDefuse) ((((a ∧ 𝔹) ∧ (a ∧ 𝔹)) -> a ⇰ a) -> 𝐼 (a ⇰ a))
-> (((a ∧ 𝔹) ∧ (a ∧ 𝔹)) -> a ⇰ a) -> 𝐼 (a ⇰ a)
forall a b. (a -> b) -> a -> b
$ \ ((a
x₁ :* 𝔹
b) :* (a
x₂ :* 𝔹
_)) →
        if 𝔹
b then a
x₁ a -> a -> a ⇰ a
forall a. a -> a -> a ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ a
x₂ else a ⇰ a
forall a. Null a => a
null
      -- map group ids to variables in that group, and all dependencies of
      -- that group
      groups ∷ a ⇰ 𝑃 a ∧ 𝑃 a
      groups :: a ⇰ (𝑃 a ∧ 𝑃 a)
groups = 𝐼 (a ⇰ (𝑃 a ∧ 𝑃 a)) -> a ⇰ (𝑃 a ∧ 𝑃 a)
forall a t. (JoinLattice a, ToIter a t) => t -> a
joins (𝐼 (a ⇰ (𝑃 a ∧ 𝑃 a)) -> a ⇰ (𝑃 a ∧ 𝑃 a))
-> 𝐼 (a ⇰ (𝑃 a ∧ 𝑃 a)) -> a ⇰ (𝑃 a ∧ 𝑃 a)
forall a b. (a -> b) -> a -> b
$ 𝐼 (a ∧ a) -> ((a ∧ a) -> a ⇰ (𝑃 a ∧ 𝑃 a)) -> 𝐼 (a ⇰ (𝑃 a ∧ 𝑃 a))
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn ((a ⇰ a) -> 𝐼 (a ∧ a)
forall a t. ToIter a t => t -> 𝐼 a
iter a ⇰ a
sccs) (((a ∧ a) -> a ⇰ (𝑃 a ∧ 𝑃 a)) -> 𝐼 (a ⇰ (𝑃 a ∧ 𝑃 a)))
-> ((a ∧ a) -> a ⇰ (𝑃 a ∧ 𝑃 a)) -> 𝐼 (a ⇰ (𝑃 a ∧ 𝑃 a))
forall a b. (a -> b) -> a -> b
$ \ (a
x₁ :* a
x₂) →
        a
x₂ a -> (𝑃 a ∧ 𝑃 a) -> a ⇰ (𝑃 a ∧ 𝑃 a)
forall a. a -> a -> a ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ a -> 𝑃 a
forall a t. Single a t => a -> t
single a
x₁ 𝑃 a -> 𝑃 a -> 𝑃 a ∧ 𝑃 a
forall a b. a -> b -> a ∧ b
:* (a ⇰ 𝑃 a
deps (a ⇰ 𝑃 a) -> a -> 𝑃 a
forall k v t. (Lookup k v t, STACK) => t -> k -> v
⋕! a
x₁)
  in a ⇰ a
sccs (a ⇰ a) -> (a ⇰ (𝑃 a ∧ 𝑃 a)) -> (a ⇰ a) ∧ (a ⇰ (𝑃 a ∧ 𝑃 a))
forall a b. a -> b -> a ∧ b
:* a ⇰ (𝑃 a ∧ 𝑃 a)
groups

-- | Compute strongly connected components following a dependency map, and
-- process each component with a monadic action.
-- 
--     sccEachGroupM xs deps f
--
-- - `xs` represents a desired ordering in which to process variables (e.g., if
--   definitions `x` and `y` do not depend on each other, and `x` comes before
--   `y` in `xs`, then call `f` on the SCC group for `x` before doing the same
--   for `y`.)
-- - `deps` represents dependency information. See `sccGroups` for how these
--   are processed.
-- - `f b xs′` represents an action to perform on each SCC group. If the group
--   is non-recursive, then `b` will be `False` and `|xs′| = 1`. If the group
--   is recursive, then `b` will be `True` and `|xs′| ≥ 1`.
sccEachGroupM ∷ ∀ a b m. (Ord a,Monad m) ⇒ 𝐼 a → a ⇰ 𝑃 a → (𝔹 → 𝐼 a → m (𝐼 b)) → m (𝐼 b)
sccEachGroupM :: forall a b (m :: * -> *).
(Ord a, Monad m) =>
𝐼 a -> (a ⇰ 𝑃 a) -> (𝔹 -> 𝐼 a -> m (𝐼 b)) -> m (𝐼 b)
sccEachGroupM 𝐼 a
xs a ⇰ 𝑃 a
deps 𝔹 -> 𝐼 a -> m (𝐼 b)
f =
  let a ⇰ a
sccs :* a ⇰ (𝑃 a ∧ 𝑃 a)
groups = (a ⇰ 𝑃 a) -> (a ⇰ a) ∧ (a ⇰ (𝑃 a ∧ 𝑃 a))
forall a. Ord a => (a ⇰ 𝑃 a) -> (a ⇰ a) ∧ (a ⇰ (𝑃 a ∧ 𝑃 a))
sccGroups a ⇰ 𝑃 a
deps
      visitVar ∷ a → RWST () (𝐼 b) (𝑃 a) m ()
      visitVar :: a -> RWST () (𝐼 b) (𝑃 a) m ()
visitVar a
x = do
        -- lookup the group this element is in
        let g :: a
g = a ⇰ a
sccs (a ⇰ a) -> a -> a
forall k v t. (Lookup k v t, STACK) => t -> k -> v
⋕! a
x
        -- if we have already processed this group, then skip
        𝑃 a
seen ← RWST () (𝐼 b) (𝑃 a) m (𝑃 a)
forall s (m :: * -> *). MonadState s m => m s
get
        if a
g a -> 𝑃 a -> 𝔹
forall e s. Set e s => e -> s -> 𝔹
∈ 𝑃 a
seen then RWST () (𝐼 b) (𝑃 a) m ()
forall (m :: * -> *). Return m => m ()
skip
        else do
          -- mark that we have already processed this group
          (𝑃 a -> 𝑃 a) -> RWST () (𝐼 b) (𝑃 a) m ()
forall (m :: * -> *) s.
(Monad m, MonadState s m) =>
(s -> s) -> m ()
modify ((𝑃 a -> 𝑃 a) -> RWST () (𝐼 b) (𝑃 a) m ())
-> (𝑃 a -> 𝑃 a) -> RWST () (𝐼 b) (𝑃 a) m ()
forall a b. (a -> b) -> a -> b
$ 𝑃 a -> 𝑃 a -> 𝑃 a
forall e s. Set e s => s -> s -> s
(∪) (𝑃 a -> 𝑃 a -> 𝑃 a) -> 𝑃 a -> 𝑃 a -> 𝑃 a
forall a b. (a -> b) -> a -> b
$ a -> 𝑃 a
forall a t. Single a t => a -> t
single a
g
          -- look up elements and dependencies in this group
          let 𝑃 a
gdefs :* 𝑃 a
gdeps = a ⇰ (𝑃 a ∧ 𝑃 a)
groups (a ⇰ (𝑃 a ∧ 𝑃 a)) -> a -> 𝑃 a ∧ 𝑃 a
forall k v t. (Lookup k v t, STACK) => t -> k -> v
⋕! a
g
              cyclic :: 𝔹
cyclic = 𝑃 a
gdefs 𝑃 a -> 𝑃 a -> 𝑃 a
forall e s. Set e s => s -> s -> s
∩ 𝑃 a
gdeps 𝑃 a -> 𝑃 a -> 𝔹
forall a. Eq a => a -> a -> 𝔹
≢ 𝑃 a
forall e s. Set e s => s
pø
          -- sequentialize all dependencies (that aren't cyclic)
          𝑃 a -> (a -> RWST () (𝐼 b) (𝑃 a) m ()) -> RWST () (𝐼 b) (𝑃 a) m ()
forall (m :: * -> *) a t.
(Monad m, ToIter a t) =>
t -> (a -> m ()) -> m ()
eachOn (𝑃 a
gdeps 𝑃 a -> 𝑃 a -> 𝑃 a
forall e s. Set e s => s -> s -> s
∖ 𝑃 a
gdefs) a -> RWST () (𝐼 b) (𝑃 a) m ()
visitVar
          -- build a list of results
          𝐼 b -> RWST () (𝐼 b) (𝑃 a) m ()
forall o (m :: * -> *). MonadWriter o m => o -> m ()
tell (𝐼 b -> RWST () (𝐼 b) (𝑃 a) m ())
-> RWST () (𝐼 b) (𝑃 a) m (𝐼 b) -> RWST () (𝐼 b) (𝑃 a) m ()
forall (m :: * -> *) a b. Bind m => (a -> m b) -> m a -> m b
*$ m (𝐼 b) -> RWST () (𝐼 b) (𝑃 a) m (𝐼 b)
forall (m :: * -> *) a. Monad m => m a -> RWST () (𝐼 b) (𝑃 a) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(Transformer t, Monad m) =>
m a -> t m a
lift (m (𝐼 b) -> RWST () (𝐼 b) (𝑃 a) m (𝐼 b))
-> m (𝐼 b) -> RWST () (𝐼 b) (𝑃 a) m (𝐼 b)
forall a b. (a -> b) -> a -> b
$ 𝔹 -> 𝐼 a -> m (𝐼 b)
f 𝔹
cyclic (𝐼 a -> m (𝐼 b)) -> 𝐼 a -> m (𝐼 b)
forall a b. (a -> b) -> a -> b
$ 𝑃 a -> 𝐼 a
forall a t. ToIter a t => t -> 𝐼 a
iter 𝑃 a
gdefs
    in () -> 𝑃 a -> RWST () (𝐼 b) (𝑃 a) m (𝐼 b) -> m (𝐼 b)
forall r o s (m :: * -> *) a.
Monad m =>
r -> s -> RWST r o s m a -> m a
evalRWST () 𝑃 a
forall e s. Set e s => s
pø (RWST () (𝐼 b) (𝑃 a) m (𝐼 b) -> m (𝐼 b))
-> RWST () (𝐼 b) (𝑃 a) m (𝐼 b) -> m (𝐼 b)
forall a b. (a -> b) -> a -> b
$ RWST () (𝐼 b) (𝑃 a) m () -> RWST () (𝐼 b) (𝑃 a) m (𝐼 b)
forall o (m :: * -> *) a. (Monad m, MonadWriter o m) => m a -> m o
retOut (RWST () (𝐼 b) (𝑃 a) m () -> RWST () (𝐼 b) (𝑃 a) m (𝐼 b))
-> RWST () (𝐼 b) (𝑃 a) m () -> RWST () (𝐼 b) (𝑃 a) m (𝐼 b)
forall a b. (a -> b) -> a -> b
$ 𝐼 a -> (a -> RWST () (𝐼 b) (𝑃 a) m ()) -> RWST () (𝐼 b) (𝑃 a) m ()
forall (m :: * -> *) a t.
(Monad m, ToIter a t) =>
t -> (a -> m ()) -> m ()
eachOn 𝐼 a
xs a -> RWST () (𝐼 b) (𝑃 a) m ()
visitVar

-- | Similar to `sccEachGroupM`, but specialized to the identity monad.
sccEachGroup ∷ ∀ a b. (Ord a) ⇒ 𝐼 a → a ⇰ 𝑃 a → (𝔹 → 𝐼 a → 𝐼 b) → 𝐼 b
sccEachGroup :: forall a b. Ord a => 𝐼 a -> (a ⇰ 𝑃 a) -> (𝔹 -> 𝐼 a -> 𝐼 b) -> 𝐼 b
sccEachGroup 𝐼 a
xs a ⇰ 𝑃 a
deps 𝔹 -> 𝐼 a -> 𝐼 b
f = ID (𝐼 b) -> 𝐼 b
forall a. ID a -> a
unID (ID (𝐼 b) -> 𝐼 b) -> ID (𝐼 b) -> 𝐼 b
forall a b. (a -> b) -> a -> b
$ 𝐼 a -> (a ⇰ 𝑃 a) -> (𝔹 -> 𝐼 a -> ID (𝐼 b)) -> ID (𝐼 b)
forall a b (m :: * -> *).
(Ord a, Monad m) =>
𝐼 a -> (a ⇰ 𝑃 a) -> (𝔹 -> 𝐼 a -> m (𝐼 b)) -> m (𝐼 b)
sccEachGroupM 𝐼 a
xs a ⇰ 𝑃 a
deps ((𝔹 -> 𝐼 a -> ID (𝐼 b)) -> ID (𝐼 b))
-> (𝔹 -> 𝐼 a -> ID (𝐼 b)) -> ID (𝐼 b)
forall a b. (a -> b) -> a -> b
$ 𝐼 b -> ID (𝐼 b)
forall a. a -> ID a
ID (𝐼 b -> ID (𝐼 b)) -> (𝔹 -> 𝐼 a -> 𝐼 b) -> 𝔹 -> 𝐼 a -> ID (𝐼 b)
forall c d a b. (c -> d) -> (a -> b -> c) -> a -> b -> d
∘∘ 𝔹 -> 𝐼 a -> 𝐼 b
f