packages feed

Agda-2.8.0.2: src/full/Agda/Utils/SmallSet.hs

{-# LANGUAGE CPP #-}

{-# OPTIONS_GHC -Wunused-imports #-}

-- | Small sets represented as a bitmask for fast membership checking.
--
-- With the exception of converting to/from lists, all operations are O(1).
--
-- Mimics the interface of 'Data.Set'.
--
-- Import as:
-- @
--    import qualified Agda.Utils.SmallSet as SmallSet
--    import Agda.Utils.SmallSet (SmallSet)
-- @

module Agda.Utils.SmallSet
  ( SmallSet(..)
  , SmallSetElement
  , Ix
  , (\\)
  , complement
  , delete
  , difference
  , elems
  , empty
  , fromList, fromAscList, fromDistinctAscList
  , insert
  , intersection
  , member
  , notMember
  , null
  , singleton
  , toList, toAscList
  , total
  , union
  ) where

import Prelude hiding (null)

import Control.DeepSeq

import Data.Word (Word64)
#if !MIN_VERSION_base(4,20,0)
import Data.List (foldl')
#endif
import Data.Bits hiding (complement)
import qualified Data.Bits as Bits
import Data.Ix

import qualified Agda.Utils.Null as Null

-- | An element in a small set.
--
-- This must implement 'Bounded' and 'Ix', and contain at most 64 values.
class (Bounded a, Ix a) => SmallSetElement a where

newtype SmallSet a = SmallSet { theSmallSet :: Word64 }
  deriving (Eq, Ord, Show, NFData)


instance SmallSetElement a => Null.Null (SmallSet a) where
  empty = empty
  null = null

instance SmallSetElement a => Semigroup (SmallSet a) where
  (<>) = union

instance SmallSetElement a => Monoid (SmallSet a) where
  mempty = empty

-- * Query

-- | Time O(1).
null :: SmallSetElement a => SmallSet a -> Bool
null s = theSmallSet s == 0

-- | Time O(1).
member :: SmallSetElement a => a -> SmallSet a -> Bool
member a s = theSmallSet s `testBit` idx a

-- | @not . member a@.  Time O(1).
notMember :: SmallSetElement a => a -> SmallSet a -> Bool
notMember a = not . member a

-- * Construction

-- | The empty set.  Time O(1).
empty :: SmallSetElement a => SmallSet a
empty = SmallSet 0

-- | The full set.  Time O(1).
total :: forall a. SmallSetElement a => SmallSet a
total = SmallSet $ Bits.complement 0

-- | A singleton set.  Time O(1).
singleton :: SmallSetElement a => a -> SmallSet a
singleton a = SmallSet $ bit (idx a)

-- | Time O(1).
insert :: SmallSetElement a => a -> SmallSet a -> SmallSet a
insert a s = SmallSet $ theSmallSet s `setBit` idx a

-- | Time O(1).
delete :: SmallSetElement a => a -> SmallSet a -> SmallSet a
delete a s = SmallSet $ theSmallSet s `clearBit` idx a

-- * Combine

-- | Time O(n).
complement :: SmallSetElement a => SmallSet a -> SmallSet a
complement = SmallSet . Bits.complement . theSmallSet

-- | Time O(1).
difference, (\\) :: SmallSetElement a => SmallSet a -> SmallSet a -> SmallSet a
difference s t = SmallSet $ theSmallSet s .&. Bits.complement (theSmallSet t)
(\\)       = difference

-- | Time O(1).
intersection ::  SmallSetElement a => SmallSet a -> SmallSet a -> SmallSet a
intersection s t = SmallSet $ theSmallSet s .&. theSmallSet t

-- | Time O(n).
union ::  SmallSetElement a => SmallSet a -> SmallSet a -> SmallSet a
union s t = SmallSet $ theSmallSet s .|. theSmallSet t

-- * Conversion

-- | Time O(n).
elems, toList, toAscList :: SmallSetElement a => SmallSet a -> [a]
elems s   = filter (\i -> theSmallSet s `testBit` idx i) (range bounds)
toList    = elems
toAscList = elems

-- | Time O(n).
fromList, fromAscList, fromDistinctAscList :: SmallSetElement a => [a] -> SmallSet a
fromList            = foldl' (flip insert) empty
fromAscList         = fromList
fromDistinctAscList = fromList

-- * Internals

bounds :: SmallSetElement a => (a, a)
bounds = (minBound, maxBound)

idx :: SmallSetElement a => a -> Int
idx a = index bounds a