Algorithm.hs 1.46 KB
Newer Older
1
{-# LANGUAGE AllowAmbiguousTypes #-}
2
module MA.Algorithm
3
  ( refine
4
5
  ) where

6
import           Control.Monad.ST
7
import           Data.Proxy
8

9
import           Control.Monad.Extra (whileM)
10
import           Control.Monad.Reader
11

12
13
import           Data.BlockQueue (BlockQueue)
import qualified Data.BlockQueue as Queue
14
import           Data.MorphismEncoding
15
16
import           Data.Partition (Partition)
import qualified Data.RefinablePartition as Partition
17
import           MA.RefinementInterface (RefinementInterface)
18
import           MA.Coalgebra.RefinementTypes
19
20
21
import           MA.Algorithm.Types
import           MA.Algorithm.Initialize
import           MA.Algorithm.Split
22
import           MA.Algorithm.Internal
23

24
processQueue  :: RefinementInterface h => BlockQueue s -> AlgoState s h -> ST s ()
25
processQueue queue as = whileM $
26
27
  Queue.dequeue queue >>= \case
    Nothing -> return False
28
    Just block -> do
29
      runReaderT (split block) (as, queue)
30
      return True
31
{-# SPECIALIZE processQueue :: BlockQueue s -> AlgoState s TheFunctor -> ST s () #-}
32

33
refine :: forall f s.
34
35
36
37
     RefinementInterface f
  => Proxy f
  -> Encoding (Label f) (H1 f)
  -> ST s Partition
38
refine Proxy encoding = do
39
  queue <- Queue.empty (size encoding)
40
  (blocks, state) <- initialize @f encoding
41
  mapM_ (Queue.enqueue queue) blocks
42

43
  processQueue  queue state
44
45

  Partition.freeze (partition state)
46
{-# SPECIALIZE refine :: Proxy TheFunctor -> Encoding (Label TheFunctor) (H1 TheFunctor) -> ST s Partition #-}