packages feed

moonlight-core-0.1.0.0: src-solver/Moonlight/Core/Fixpoint/Internal/Combinators.hs

-- | Bounded fixpoint iteration, once-only integer worklists, and transitive
-- closure. Pure combinators over 'Moonlight.Core.Queue'; no mutation.
module Moonlight.Core.Fixpoint.Internal.Combinators
  ( FixpointDivergence (..),
    fixpointBounded,
    fixpointBoundedM,
    worklistFold,
    traverseOnceIntSet,
    reschedulingWorklistFoldIntSet,
    closureUnder,
    closureUnderInt,
    reachabilityFrom,
    reachabilityFromInt,
  )
where

import Data.Functor.Identity (Identity (..), runIdentity)
import Data.IntSet (IntSet)
import Data.IntSet qualified as IntSet
import Data.Set (Set)
import Data.Set qualified as Set
import Moonlight.Core.Queue (Queue, dequeue, enqueueAll, queueFromList)
import Numeric.Natural (Natural)
import Prelude

data FixpointDivergence a = FixpointDivergence
  { fixpointDivergenceBudget :: !Natural,
    fixpointDivergenceLast :: !a
  }
  deriving stock (Eq, Ord, Show, Read)

fixpointBounded :: Eq a => Natural -> (a -> a) -> a -> Either (FixpointDivergence a) a
fixpointBounded budget step =
  runIdentity . fixpointBoundedM budget (Identity . step)

fixpointBoundedM :: (Monad m, Eq a) => Natural -> (a -> m a) -> a -> m (Either (FixpointDivergence a) a)
fixpointBoundedM budget =
  fixpointBoundedWorker budget budget

fixpointBoundedWorker ::
  (Monad m, Eq a) =>
  Natural ->
  Natural ->
  (a -> m a) ->
  a ->
  m (Either (FixpointDivergence a) a)
fixpointBoundedWorker budget remaining step current
  | remaining == 0 = pure (Left (FixpointDivergence budget current))
  | otherwise = do
      next <- step current
      if next == current
        then pure (Right current)
        else fixpointBoundedWorker budget (remaining - 1) step next

worklistFold :: (state -> item -> (state, [item])) -> state -> Queue item -> state
worklistFold step state frontier =
  case dequeue frontier of
    Nothing -> state
    Just (item, remainingFrontier) ->
      case step state item of
        (nextState, queuedItems) ->
          nextState `seq` worklistFold step nextState (enqueueAll queuedItems remainingFrontier)

-- | Reachability primitive: each integer key is expanded at most once.
traverseOnceIntSet :: (state -> Int -> (state, IntSet)) -> state -> IntSet -> state
traverseOnceIntSet step =
  freshIntSetWorklist step IntSet.empty

-- | Fixpoint-style integer worklist: an item may run again after it has been
-- dequeued, but duplicate queued copies are collapsed while it is waiting.
reschedulingWorklistFoldIntSet :: (state -> Int -> (state, IntSet)) -> state -> IntSet -> state
reschedulingWorklistFoldIntSet step initialState initialFrontier =
  reschedulingIntSetWorklist
    step
    initialState
    (queueFromList (IntSet.toAscList initialFrontier))
    initialFrontier

reschedulingIntSetWorklist ::
  (state -> Int -> (state, IntSet)) ->
  state ->
  Queue Int ->
  IntSet ->
  state
reschedulingIntSetWorklist step state frontier queued =
  case dequeue frontier of
    Nothing ->
      state
    Just (item, remainingFrontier) ->
      let queuedAfterPop =
            IntSet.delete item queued
       in case step state item of
            (nextState, requestedItems) ->
              let freshItems =
                    IntSet.difference requestedItems queuedAfterPop
               in nextState `seq`
                    reschedulingIntSetWorklist
                      step
                      nextState
                      (enqueueAll (IntSet.toAscList freshItems) remainingFrontier)
                      (IntSet.union queuedAfterPop freshItems)

freshIntSetWorklist :: (state -> Int -> (state, IntSet)) -> IntSet -> state -> IntSet -> state
freshIntSetWorklist step processed state frontier =
  case IntSet.minView frontier of
    Nothing -> state
    Just (item, rest)
      | IntSet.member item processed ->
          freshIntSetWorklist step processed state rest
      | otherwise ->
          case step state item of
            (nextState, queued) ->
              let nextProcessed = IntSet.insert item processed
               in nextState `seq`
                    freshIntSetWorklist
                      step
                      nextProcessed
                      nextState
                      (IntSet.union rest (IntSet.difference queued nextProcessed))

closureUnder :: Ord value => (value -> Set value) -> Set value -> Set value
closureUnder =
  reachabilityFrom

closureUnderInt :: (Int -> IntSet) -> IntSet -> IntSet
closureUnderInt =
  reachabilityFromInt

reachabilityFrom :: Ord value => (value -> Set value) -> Set value -> Set value
reachabilityFrom expand seeds =
  worklistClosureSet expand seeds (queueFromList (Set.toAscList seeds))

reachabilityFromInt :: (Int -> IntSet) -> IntSet -> IntSet
reachabilityFromInt expand seeds =
  traverseOnceIntSet step seeds seeds
  where
    step visited value =
      let freshValues = IntSet.difference (expand value) visited
       in (IntSet.union visited freshValues, freshValues)

worklistClosureSet :: Ord value => (value -> Set value) -> Set value -> Queue value -> Set value
worklistClosureSet expand =
  worklistFold step
  where
    step visited value =
      let freshValues = Set.difference (expand value) visited
       in (Set.union visited freshValues, Set.toAscList freshValues)