{-# LANGUAGE BangPatterns          #-}
{-# LANGUAGE TupleSections         #-}

module Language.Fixpoint.Solver.Worklist
       ( -- * Worklist type is opaque
         Worklist, Stats

         -- * Initialize
       , init

         -- * Pop off a constraint
       , pop

         -- * Add a constraint and all its dependencies
       , push

         -- * Constraints with Concrete RHS
       , unsatCandidates

         -- * Statistics
       , wRanks
       )
       where

import           Prelude hiding (init)
import           Language.Fixpoint.Types.PrettyPrint
import qualified Language.Fixpoint.Types   as F
import           Language.Fixpoint.Graph.Types
import           Language.Fixpoint.Graph   (isTarget)

import           Control.Arrow             (first)
import qualified Data.HashMap.Strict       as M
import qualified Data.Set                  as S
import qualified Data.List                 as L
import           Text.PrettyPrint.HughesPJ (text)

-- | Worklist ------------------------------------------------------------------

data Worklist a = WL { Worklist a -> WorkSet
wCs     :: !WorkSet
                     , Worklist a -> CMap ()
wPend   :: !(CMap ())
                     , Worklist a -> CMap [SubcId]
wDeps   :: !(CMap [F.SubcId])
                     , Worklist a -> CMap (SimpC a)
wCm     :: !(CMap (F.SimpC a))
                     , Worklist a -> CMap Rank
wRankm  :: !(CMap Rank)
                     , Worklist a -> Maybe SubcId
wLast   :: !(Maybe F.SubcId)
                     , Worklist a -> Int
wRanks  :: !Int
                     , Worklist a -> Int
wTime   :: !Int
                     , Worklist a -> [SubcId]
wConcCs :: ![F.SubcId]
                     }

data Stats = Stats { Stats -> Int
numKvarCs  :: !Int
                   , Stats -> Int
numConcCs  :: !Int
                   , Stats -> Int
_numSccs   :: !Int
                   } deriving (Stats -> Stats -> Bool
(Stats -> Stats -> Bool) -> (Stats -> Stats -> Bool) -> Eq Stats
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Stats -> Stats -> Bool
$c/= :: Stats -> Stats -> Bool
== :: Stats -> Stats -> Bool
$c== :: Stats -> Stats -> Bool
Eq, Int -> Stats -> ShowS
[Stats] -> ShowS
Stats -> String
(Int -> Stats -> ShowS)
-> (Stats -> String) -> ([Stats] -> ShowS) -> Show Stats
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Stats] -> ShowS
$cshowList :: [Stats] -> ShowS
show :: Stats -> String
$cshow :: Stats -> String
showsPrec :: Int -> Stats -> ShowS
$cshowsPrec :: Int -> Stats -> ShowS
Show)

instance PPrint (Worklist a) where
  pprintTidy :: Tidy -> Worklist a -> Doc
pprintTidy Tidy
k = Tidy -> [WorkItem] -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k ([WorkItem] -> Doc)
-> (Worklist a -> [WorkItem]) -> Worklist a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WorkSet -> [WorkItem]
forall a. Set a -> [a]
S.toList (WorkSet -> [WorkItem])
-> (Worklist a -> WorkSet) -> Worklist a -> [WorkItem]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Worklist a -> WorkSet
forall a. Worklist a -> WorkSet
wCs

instance PTable Stats where
  ptable :: Stats -> DocTable
ptable Stats
s = [(Doc, Doc)] -> DocTable
DocTable [ (String -> Doc
text String
"# Sliced Constraints", Int -> Doc
forall a. PPrint a => a -> Doc
pprint (Stats -> Int
numKvarCs Stats
s))
                      , (String -> Doc
text String
"# Target Constraints", Int -> Doc
forall a. PPrint a => a -> Doc
pprint (Stats -> Int
numConcCs Stats
s))
                      ]

instance PTable (Worklist a) where
  ptable :: Worklist a -> DocTable
ptable = Stats -> DocTable
forall a. PTable a => a -> DocTable
ptable (Stats -> DocTable)
-> (Worklist a -> Stats) -> Worklist a -> DocTable
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Worklist a -> Stats
forall a. Worklist a -> Stats
stats


-- | WorkItems ------------------------------------------------------------

type WorkSet  = S.Set WorkItem

data WorkItem = WorkItem { WorkItem -> SubcId
wiCId  :: !F.SubcId   -- ^ Constraint Id
                         , WorkItem -> Int
wiTime :: !Int   -- ^ Time at which inserted
                         , WorkItem -> Rank
wiRank :: !Rank  -- ^ Rank of constraint
                         } deriving (WorkItem -> WorkItem -> Bool
(WorkItem -> WorkItem -> Bool)
-> (WorkItem -> WorkItem -> Bool) -> Eq WorkItem
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: WorkItem -> WorkItem -> Bool
$c/= :: WorkItem -> WorkItem -> Bool
== :: WorkItem -> WorkItem -> Bool
$c== :: WorkItem -> WorkItem -> Bool
Eq, Int -> WorkItem -> ShowS
[WorkItem] -> ShowS
WorkItem -> String
(Int -> WorkItem -> ShowS)
-> (WorkItem -> String) -> ([WorkItem] -> ShowS) -> Show WorkItem
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [WorkItem] -> ShowS
$cshowList :: [WorkItem] -> ShowS
show :: WorkItem -> String
$cshow :: WorkItem -> String
showsPrec :: Int -> WorkItem -> ShowS
$cshowsPrec :: Int -> WorkItem -> ShowS
Show)

instance PPrint WorkItem where
  pprintTidy :: Tidy -> WorkItem -> Doc
pprintTidy Tidy
_ = String -> Doc
text (String -> Doc) -> (WorkItem -> String) -> WorkItem -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WorkItem -> String
forall a. Show a => a -> String
show

instance Ord WorkItem where
  compare :: WorkItem -> WorkItem -> Ordering
compare (WorkItem SubcId
i1 Int
t1 Rank
r1) (WorkItem SubcId
i2 Int
t2 Rank
r2)
    = [Ordering] -> Ordering
forall a. Monoid a => [a] -> a
mconcat [ Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Rank -> Int
rScc Rank
r1) (Rank -> Int
rScc Rank
r2)   -- SCC
              , Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Int
t1 Int
t2                 -- TimeStamp
              , Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Rank -> Int
rIcc Rank
r1) (Rank -> Int
rIcc Rank
r2)   -- Inner SCC
              , Tag -> Tag -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Rank -> Tag
rTag Rank
r1) (Rank -> Tag
rTag Rank
r2)   -- Tag
              , SubcId -> SubcId -> Ordering
forall a. Ord a => a -> a -> Ordering
compare SubcId
i1         SubcId
i2         -- Otherwise Set drops items
              ]

--------------------------------------------------------------------------------
-- | Initialize worklist and slice out irrelevant constraints ------------------
--------------------------------------------------------------------------------
init :: SolverInfo a b -> Worklist a
--------------------------------------------------------------------------------
init :: SolverInfo a b -> Worklist a
init SolverInfo a b
sI    = WL :: forall a.
WorkSet
-> CMap ()
-> CMap [SubcId]
-> CMap (SimpC a)
-> CMap Rank
-> Maybe SubcId
-> Int
-> Int
-> [SubcId]
-> Worklist a
WL { wCs :: WorkSet
wCs     = WorkSet
items
                , wPend :: CMap ()
wPend   = CMap () -> [SubcId] -> CMap ()
addPends CMap ()
forall k v. HashMap k v
M.empty [SubcId]
kvarCs
                , wDeps :: CMap [SubcId]
wDeps   = CDeps -> CMap [SubcId]
cSucc CDeps
cd
                , wCm :: CMap (SimpC a)
wCm     = CMap (SimpC a)
cm
                , wRankm :: CMap Rank
wRankm  = {- F.tracepp "W.init ranks" -} CMap Rank
rankm
                , wLast :: Maybe SubcId
wLast   = Maybe SubcId
forall a. Maybe a
Nothing
                , wRanks :: Int
wRanks  = CDeps -> Int
cNumScc CDeps
cd
                , wTime :: Int
wTime   = Int
0
                , wConcCs :: [SubcId]
wConcCs = [SubcId]
concCs
                }
  where
    cm :: CMap (SimpC a)
cm        = GInfo SimpC a -> CMap (SimpC a)
forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
F.cm  (SolverInfo a b -> GInfo SimpC a
forall a b. SolverInfo a b -> SInfo a
siQuery SolverInfo a b
sI)
    cd :: CDeps
cd        = SolverInfo a b -> CDeps
forall a b. SolverInfo a b -> CDeps
siDeps SolverInfo a b
sI
    rankm :: CMap Rank
rankm     = CDeps -> CMap Rank
cRank CDeps
cd
    items :: WorkSet
items     = [WorkItem] -> WorkSet
forall a. Ord a => [a] -> Set a
S.fromList ([WorkItem] -> WorkSet) -> [WorkItem] -> WorkSet
forall a b. (a -> b) -> a -> b
$ CMap Rank -> Int -> SubcId -> WorkItem
workItemsAt CMap Rank
rankm Int
0 (SubcId -> WorkItem) -> [SubcId] -> [WorkItem]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SubcId]
kvarCs
    concCs :: [SubcId]
concCs    = (SubcId, SimpC a) -> SubcId
forall a b. (a, b) -> a
fst ((SubcId, SimpC a) -> SubcId) -> [(SubcId, SimpC a)] -> [SubcId]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(SubcId, SimpC a)]
ics
    kvarCs :: [SubcId]
kvarCs    = (SubcId, SimpC a) -> SubcId
forall a b. (a, b) -> a
fst ((SubcId, SimpC a) -> SubcId) -> [(SubcId, SimpC a)] -> [SubcId]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(SubcId, SimpC a)]
iks
    ([(SubcId, SimpC a)]
ics,[(SubcId, SimpC a)]
iks) = ((SubcId, SimpC a) -> Bool)
-> [(SubcId, SimpC a)]
-> ([(SubcId, SimpC a)], [(SubcId, SimpC a)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition (SimpC a -> Bool
forall (c :: * -> *) a. TaggedC c a => c a -> Bool
isTarget (SimpC a -> Bool)
-> ((SubcId, SimpC a) -> SimpC a) -> (SubcId, SimpC a) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SubcId, SimpC a) -> SimpC a
forall a b. (a, b) -> b
snd) (CMap (SimpC a) -> [(SubcId, SimpC a)]
forall k v. HashMap k v -> [(k, v)]
M.toList CMap (SimpC a)
cm)

---------------------------------------------------------------------------
-- | Candidate Constraints to be checked AFTER computing Fixpoint ---------
---------------------------------------------------------------------------
unsatCandidates   :: Worklist a -> [F.SimpC a]
---------------------------------------------------------------------------
unsatCandidates :: Worklist a -> [SimpC a]
unsatCandidates Worklist a
w = [ CMap (SimpC a) -> SubcId -> SimpC a
forall a. (?callStack::CallStack) => CMap a -> SubcId -> a
lookupCMap (Worklist a -> CMap (SimpC a)
forall a. Worklist a -> CMap (SimpC a)
wCm Worklist a
w) SubcId
i | SubcId
i <- Worklist a -> [SubcId]
forall a. Worklist a -> [SubcId]
wConcCs Worklist a
w ]


---------------------------------------------------------------------------
pop  :: Worklist a -> Maybe (F.SimpC a, Worklist a, Bool, Int)
---------------------------------------------------------------------------
pop :: Worklist a -> Maybe (SimpC a, Worklist a, Bool, Int)
pop Worklist a
w = do
  (SubcId
i, WorkSet
is) <- WorkSet -> Maybe (SubcId, WorkSet)
sPop (WorkSet -> Maybe (SubcId, WorkSet))
-> WorkSet -> Maybe (SubcId, WorkSet)
forall a b. (a -> b) -> a -> b
$ Worklist a -> WorkSet
forall a. Worklist a -> WorkSet
wCs Worklist a
w
  (SimpC a, Worklist a, Bool, Int)
-> Maybe (SimpC a, Worklist a, Bool, Int)
forall a. a -> Maybe a
Just ( CMap (SimpC a) -> SubcId -> SimpC a
forall a. (?callStack::CallStack) => CMap a -> SubcId -> a
lookupCMap (Worklist a -> CMap (SimpC a)
forall a. Worklist a -> CMap (SimpC a)
wCm Worklist a
w) SubcId
i
       , Worklist a -> SubcId -> WorkSet -> Worklist a
forall a. Worklist a -> SubcId -> WorkSet -> Worklist a
popW Worklist a
w SubcId
i WorkSet
is
       , Worklist a -> SubcId -> Bool
forall a. Worklist a -> SubcId -> Bool
newSCC Worklist a
w SubcId
i
       , Worklist a -> SubcId -> Int
forall a. Worklist a -> SubcId -> Int
rank Worklist a
w SubcId
i
       )

popW :: Worklist a -> F.SubcId -> WorkSet -> Worklist a
popW :: Worklist a -> SubcId -> WorkSet -> Worklist a
popW Worklist a
w SubcId
i WorkSet
is = Worklist a
w { wCs :: WorkSet
wCs   = WorkSet
is
                , wLast :: Maybe SubcId
wLast = SubcId -> Maybe SubcId
forall a. a -> Maybe a
Just SubcId
i
                , wPend :: CMap ()
wPend = CMap () -> SubcId -> CMap ()
remPend (Worklist a -> CMap ()
forall a. Worklist a -> CMap ()
wPend Worklist a
w) SubcId
i }


newSCC :: Worklist a -> F.SubcId -> Bool
newSCC :: Worklist a -> SubcId -> Bool
newSCC Worklist a
oldW SubcId
i = (Rank -> Int
rScc (Rank -> Int) -> Maybe Rank -> Maybe Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Rank
oldRank) Maybe Int -> Maybe Int -> Bool
forall a. Eq a => a -> a -> Bool
/= (Rank -> Int
rScc (Rank -> Int) -> Maybe Rank -> Maybe Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Rank
newRank)
  where
    oldRank :: Maybe Rank
oldRank   = CMap Rank -> SubcId -> Rank
forall a. (?callStack::CallStack) => CMap a -> SubcId -> a
lookupCMap CMap Rank
rankm (SubcId -> Rank) -> Maybe SubcId -> Maybe Rank
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Worklist a -> Maybe SubcId
forall a. Worklist a -> Maybe SubcId
wLast Worklist a
oldW
    newRank :: Maybe Rank
newRank   = Rank -> Maybe Rank
forall a. a -> Maybe a
Just              (Rank -> Maybe Rank) -> Rank -> Maybe Rank
forall a b. (a -> b) -> a -> b
$  CMap Rank -> SubcId -> Rank
forall a. (?callStack::CallStack) => CMap a -> SubcId -> a
lookupCMap CMap Rank
rankm SubcId
i
    rankm :: CMap Rank
rankm     = Worklist a -> CMap Rank
forall a. Worklist a -> CMap Rank
wRankm Worklist a
oldW

rank :: Worklist a -> F.SubcId -> Int
rank :: Worklist a -> SubcId -> Int
rank Worklist a
w SubcId
i = Rank -> Int
rScc (Rank -> Int) -> Rank -> Int
forall a b. (a -> b) -> a -> b
$ CMap Rank -> SubcId -> Rank
forall a. (?callStack::CallStack) => CMap a -> SubcId -> a
lookupCMap (Worklist a -> CMap Rank
forall a. Worklist a -> CMap Rank
wRankm Worklist a
w) SubcId
i

---------------------------------------------------------------------------
push :: F.SimpC a -> Worklist a -> Worklist a
---------------------------------------------------------------------------
push :: SimpC a -> Worklist a -> Worklist a
push SimpC a
c Worklist a
w = Worklist a
w { wCs :: WorkSet
wCs   = WorkSet -> [WorkItem] -> WorkSet
sAdds (Worklist a -> WorkSet
forall a. Worklist a -> WorkSet
wCs Worklist a
w) [WorkItem]
wis'
             , wTime :: Int
wTime = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
t
             , wPend :: CMap ()
wPend = CMap () -> [SubcId] -> CMap ()
addPends CMap ()
wp [SubcId]
is'
             }
  where
    i :: SubcId
i    = SimpC a -> SubcId
forall (c :: * -> *) a. TaggedC c a => c a -> SubcId
F.subcId SimpC a
c
    is' :: [SubcId]
is'  = (SubcId -> Bool) -> [SubcId] -> [SubcId]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (SubcId -> Bool) -> SubcId -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CMap () -> SubcId -> Bool
isPend CMap ()
wp) ([SubcId] -> [SubcId]) -> [SubcId] -> [SubcId]
forall a b. (a -> b) -> a -> b
$ [SubcId] -> SubcId -> CMap [SubcId] -> [SubcId]
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault [] SubcId
i (Worklist a -> CMap [SubcId]
forall a. Worklist a -> CMap [SubcId]
wDeps Worklist a
w)
    wis' :: [WorkItem]
wis' = CMap Rank -> Int -> SubcId -> WorkItem
workItemsAt (Worklist a -> CMap Rank
forall a. Worklist a -> CMap Rank
wRankm Worklist a
w) Int
t (SubcId -> WorkItem) -> [SubcId] -> [WorkItem]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SubcId]
is'
    t :: Int
t    = Worklist a -> Int
forall a. Worklist a -> Int
wTime Worklist a
w
    wp :: CMap ()
wp   = Worklist a -> CMap ()
forall a. Worklist a -> CMap ()
wPend Worklist a
w

workItemsAt :: CMap Rank -> Int -> F.SubcId -> WorkItem
workItemsAt :: CMap Rank -> Int -> SubcId -> WorkItem
workItemsAt !CMap Rank
r !Int
t !SubcId
i = WorkItem :: SubcId -> Int -> Rank -> WorkItem
WorkItem { wiCId :: SubcId
wiCId  = SubcId
i
                                , wiTime :: Int
wiTime = Int
t
                                , wiRank :: Rank
wiRank = CMap Rank -> SubcId -> Rank
forall a. (?callStack::CallStack) => CMap a -> SubcId -> a
lookupCMap CMap Rank
r SubcId
i }



---------------------------------------------------------------------------
stats :: Worklist a -> Stats
---------------------------------------------------------------------------
stats :: Worklist a -> Stats
stats Worklist a
w = Int -> Int -> Int -> Stats
Stats (Worklist a -> Int
forall a. Worklist a -> Int
kn Worklist a
w) (Worklist a -> Int
forall a. Worklist a -> Int
cn Worklist a
w) (Worklist a -> Int
forall a. Worklist a -> Int
wRanks Worklist a
w)
  where
    kn :: Worklist a -> Int
kn  = HashMap SubcId (SimpC a) -> Int
forall k v. HashMap k v -> Int
M.size (HashMap SubcId (SimpC a) -> Int)
-> (Worklist a -> HashMap SubcId (SimpC a)) -> Worklist a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Worklist a -> HashMap SubcId (SimpC a)
forall a. Worklist a -> CMap (SimpC a)
wCm
    cn :: Worklist a -> Int
cn  = [SubcId] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([SubcId] -> Int) -> (Worklist a -> [SubcId]) -> Worklist a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Worklist a -> [SubcId]
forall a. Worklist a -> [SubcId]
wConcCs

---------------------------------------------------------------------------
-- | Pending API
---------------------------------------------------------------------------

addPends :: CMap () -> [F.SubcId] -> CMap ()
addPends :: CMap () -> [SubcId] -> CMap ()
addPends = (CMap () -> SubcId -> CMap ()) -> CMap () -> [SubcId] -> CMap ()
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' CMap () -> SubcId -> CMap ()
addPend

addPend :: CMap () -> F.SubcId -> CMap ()
addPend :: CMap () -> SubcId -> CMap ()
addPend CMap ()
m SubcId
i = SubcId -> () -> CMap () -> CMap ()
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert SubcId
i () CMap ()
m

remPend :: CMap () -> F.SubcId -> CMap ()
remPend :: CMap () -> SubcId -> CMap ()
remPend CMap ()
m SubcId
i = SubcId -> CMap () -> CMap ()
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> HashMap k v
M.delete SubcId
i CMap ()
m

isPend :: CMap () -> F.SubcId -> Bool
isPend :: CMap () -> SubcId -> Bool
isPend CMap ()
w SubcId
i = SubcId -> CMap () -> Bool
forall k a. (Eq k, Hashable k) => k -> HashMap k a -> Bool
M.member SubcId
i CMap ()
w

---------------------------------------------------------------------------
-- | Set API --------------------------------------------------------------
---------------------------------------------------------------------------

sAdds :: WorkSet -> [WorkItem] -> WorkSet
sAdds :: WorkSet -> [WorkItem] -> WorkSet
sAdds = (WorkSet -> WorkItem -> WorkSet)
-> WorkSet -> [WorkItem] -> WorkSet
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' ((WorkItem -> WorkSet -> WorkSet) -> WorkSet -> WorkItem -> WorkSet
forall a b c. (a -> b -> c) -> b -> a -> c
flip WorkItem -> WorkSet -> WorkSet
forall a. Ord a => a -> Set a -> Set a
S.insert)

sPop :: WorkSet -> Maybe (F.SubcId, WorkSet)
sPop :: WorkSet -> Maybe (SubcId, WorkSet)
sPop = ((WorkItem, WorkSet) -> (SubcId, WorkSet))
-> Maybe (WorkItem, WorkSet) -> Maybe (SubcId, WorkSet)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((WorkItem -> SubcId) -> (WorkItem, WorkSet) -> (SubcId, WorkSet)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first WorkItem -> SubcId
wiCId) (Maybe (WorkItem, WorkSet) -> Maybe (SubcId, WorkSet))
-> (WorkSet -> Maybe (WorkItem, WorkSet))
-> WorkSet
-> Maybe (SubcId, WorkSet)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WorkSet -> Maybe (WorkItem, WorkSet)
forall a. Set a -> Maybe (a, Set a)
S.minView