module UVMHS.Lib.Graph where

import UVMHS.Core

type Graph a = a ⇰ 𝑃 a

graphTranspose ∷ ∀ a. (Ord a) ⇒ Graph a → Graph a
graphTranspose :: forall a. Ord a => Graph a -> Graph a
graphTranspose Graph a
kvs = [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
kvs) ((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
kvs) (((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
  ]

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ᵣ

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)
        , -- varianble 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

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

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