Agda-2.6.1: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Utils.SmallSet

Description

Small sets represented as immutable bit arrays for fast membership checking.

Membership checking is O(1), but all other operations are O(n) where n is the size of the element type. The element type needs to implement Bounded and Ix.

Mimics the interface of Set.

Import as: import qualified Agda.Utils.SmallSet as SmallSet import Agda.Utils.SmallSet (SmallSet)

Synopsis

Documentation

data SmallSet a Source #

Instances

Instances details
Ix a => Eq (SmallSet a) Source # 
Instance details

Defined in Agda.Utils.SmallSet

Methods

(==) :: SmallSet a -> SmallSet a -> Bool

(/=) :: SmallSet a -> SmallSet a -> Bool

(Data a, Ix a) => Data (SmallSet a) Source # 
Instance details

Defined in Agda.Utils.SmallSet

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SmallSet a -> c (SmallSet a)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (SmallSet a)

toConstr :: SmallSet a -> Constr

dataTypeOf :: SmallSet a -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (SmallSet a))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (SmallSet a))

gmapT :: (forall b. Data b => b -> b) -> SmallSet a -> SmallSet a

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SmallSet a -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SmallSet a -> r

gmapQ :: (forall d. Data d => d -> u) -> SmallSet a -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> SmallSet a -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> SmallSet a -> m (SmallSet a)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SmallSet a -> m (SmallSet a)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SmallSet a -> m (SmallSet a)

Ix a => Ord (SmallSet a) Source # 
Instance details

Defined in Agda.Utils.SmallSet

Methods

compare :: SmallSet a -> SmallSet a -> Ordering

(<) :: SmallSet a -> SmallSet a -> Bool

(<=) :: SmallSet a -> SmallSet a -> Bool

(>) :: SmallSet a -> SmallSet a -> Bool

(>=) :: SmallSet a -> SmallSet a -> Bool

max :: SmallSet a -> SmallSet a -> SmallSet a

min :: SmallSet a -> SmallSet a -> SmallSet a

(Ix a, Show a) => Show (SmallSet a) Source # 
Instance details

Defined in Agda.Utils.SmallSet

Methods

showsPrec :: Int -> SmallSet a -> ShowS

show :: SmallSet a -> String

showList :: [SmallSet a] -> ShowS

class Ord a => Ix a #

Minimal complete definition

range, (index | unsafeIndex), inRange

Instances

Instances details
Ix Bool 
Instance details

Defined in GHC.Arr

Methods

range :: (Bool, Bool) -> [Bool]

index :: (Bool, Bool) -> Bool -> Int

unsafeIndex :: (Bool, Bool) -> Bool -> Int

inRange :: (Bool, Bool) -> Bool -> Bool

rangeSize :: (Bool, Bool) -> Int

unsafeRangeSize :: (Bool, Bool) -> Int

Ix Char 
Instance details

Defined in GHC.Arr

Methods

range :: (Char, Char) -> [Char]

index :: (Char, Char) -> Char -> Int

unsafeIndex :: (Char, Char) -> Char -> Int

inRange :: (Char, Char) -> Char -> Bool

rangeSize :: (Char, Char) -> Int

unsafeRangeSize :: (Char, Char) -> Int

Ix Int 
Instance details

Defined in GHC.Arr

Methods

range :: (Int, Int) -> [Int]

index :: (Int, Int) -> Int -> Int

unsafeIndex :: (Int, Int) -> Int -> Int

inRange :: (Int, Int) -> Int -> Bool

rangeSize :: (Int, Int) -> Int

unsafeRangeSize :: (Int, Int) -> Int

Ix Int8 
Instance details

Defined in GHC.Int

Methods

range :: (Int8, Int8) -> [Int8]

index :: (Int8, Int8) -> Int8 -> Int

unsafeIndex :: (Int8, Int8) -> Int8 -> Int

inRange :: (Int8, Int8) -> Int8 -> Bool

rangeSize :: (Int8, Int8) -> Int

unsafeRangeSize :: (Int8, Int8) -> Int

Ix Int16 
Instance details

Defined in GHC.Int

Methods

range :: (Int16, Int16) -> [Int16]

index :: (Int16, Int16) -> Int16 -> Int

unsafeIndex :: (Int16, Int16) -> Int16 -> Int

inRange :: (Int16, Int16) -> Int16 -> Bool

rangeSize :: (Int16, Int16) -> Int

unsafeRangeSize :: (Int16, Int16) -> Int

Ix Int32 
Instance details

Defined in GHC.Int

Methods

range :: (Int32, Int32) -> [Int32]

index :: (Int32, Int32) -> Int32 -> Int

unsafeIndex :: (Int32, Int32) -> Int32 -> Int

inRange :: (Int32, Int32) -> Int32 -> Bool

rangeSize :: (Int32, Int32) -> Int

unsafeRangeSize :: (Int32, Int32) -> Int

Ix Int64 
Instance details

Defined in GHC.Int

Methods

range :: (Int64, Int64) -> [Int64]

index :: (Int64, Int64) -> Int64 -> Int

unsafeIndex :: (Int64, Int64) -> Int64 -> Int

inRange :: (Int64, Int64) -> Int64 -> Bool

rangeSize :: (Int64, Int64) -> Int

unsafeRangeSize :: (Int64, Int64) -> Int

Ix Integer 
Instance details

Defined in GHC.Arr

Methods

range :: (Integer, Integer) -> [Integer]

index :: (Integer, Integer) -> Integer -> Int

unsafeIndex :: (Integer, Integer) -> Integer -> Int

inRange :: (Integer, Integer) -> Integer -> Bool

rangeSize :: (Integer, Integer) -> Int

unsafeRangeSize :: (Integer, Integer) -> Int

Ix Natural 
Instance details

Defined in GHC.Arr

Methods

range :: (Natural, Natural) -> [Natural]

index :: (Natural, Natural) -> Natural -> Int

unsafeIndex :: (Natural, Natural) -> Natural -> Int

inRange :: (Natural, Natural) -> Natural -> Bool

rangeSize :: (Natural, Natural) -> Int

unsafeRangeSize :: (Natural, Natural) -> Int

Ix Ordering 
Instance details

Defined in GHC.Arr

Methods

range :: (Ordering, Ordering) -> [Ordering]

index :: (Ordering, Ordering) -> Ordering -> Int

unsafeIndex :: (Ordering, Ordering) -> Ordering -> Int

inRange :: (Ordering, Ordering) -> Ordering -> Bool

rangeSize :: (Ordering, Ordering) -> Int

unsafeRangeSize :: (Ordering, Ordering) -> Int

Ix Word 
Instance details

Defined in GHC.Arr

Methods

range :: (Word, Word) -> [Word]

index :: (Word, Word) -> Word -> Int

unsafeIndex :: (Word, Word) -> Word -> Int

inRange :: (Word, Word) -> Word -> Bool

rangeSize :: (Word, Word) -> Int

unsafeRangeSize :: (Word, Word) -> Int

Ix Word8 
Instance details

Defined in GHC.Word

Methods

range :: (Word8, Word8) -> [Word8]

index :: (Word8, Word8) -> Word8 -> Int

unsafeIndex :: (Word8, Word8) -> Word8 -> Int

inRange :: (Word8, Word8) -> Word8 -> Bool

rangeSize :: (Word8, Word8) -> Int

unsafeRangeSize :: (Word8, Word8) -> Int

Ix Word16 
Instance details

Defined in GHC.Word

Methods

range :: (Word16, Word16) -> [Word16]

index :: (Word16, Word16) -> Word16 -> Int

unsafeIndex :: (Word16, Word16) -> Word16 -> Int

inRange :: (Word16, Word16) -> Word16 -> Bool

rangeSize :: (Word16, Word16) -> Int

unsafeRangeSize :: (Word16, Word16) -> Int

Ix Word32 
Instance details

Defined in GHC.Word

Methods

range :: (Word32, Word32) -> [Word32]

index :: (Word32, Word32) -> Word32 -> Int

unsafeIndex :: (Word32, Word32) -> Word32 -> Int

inRange :: (Word32, Word32) -> Word32 -> Bool

rangeSize :: (Word32, Word32) -> Int

unsafeRangeSize :: (Word32, Word32) -> Int

Ix Word64 
Instance details

Defined in GHC.Word

Methods

range :: (Word64, Word64) -> [Word64]

index :: (Word64, Word64) -> Word64 -> Int

unsafeIndex :: (Word64, Word64) -> Word64 -> Int

inRange :: (Word64, Word64) -> Word64 -> Bool

rangeSize :: (Word64, Word64) -> Int

unsafeRangeSize :: (Word64, Word64) -> Int

Ix () 
Instance details

Defined in GHC.Arr

Methods

range :: ((), ()) -> [()]

index :: ((), ()) -> () -> Int

unsafeIndex :: ((), ()) -> () -> Int

inRange :: ((), ()) -> () -> Bool

rangeSize :: ((), ()) -> Int

unsafeRangeSize :: ((), ()) -> Int

Ix GeneralCategory 
Instance details

Defined in GHC.Unicode

Methods

range :: (GeneralCategory, GeneralCategory) -> [GeneralCategory]

index :: (GeneralCategory, GeneralCategory) -> GeneralCategory -> Int

unsafeIndex :: (GeneralCategory, GeneralCategory) -> GeneralCategory -> Int

inRange :: (GeneralCategory, GeneralCategory) -> GeneralCategory -> Bool

rangeSize :: (GeneralCategory, GeneralCategory) -> Int

unsafeRangeSize :: (GeneralCategory, GeneralCategory) -> Int

Ix Day 
Instance details

Defined in Data.Time.Calendar.Days

Methods

range :: (Day, Day) -> [Day]

index :: (Day, Day) -> Day -> Int

unsafeIndex :: (Day, Day) -> Day -> Int

inRange :: (Day, Day) -> Day -> Bool

rangeSize :: (Day, Day) -> Int

unsafeRangeSize :: (Day, Day) -> Int

Ix SeekMode 
Instance details

Defined in GHC.IO.Device

Methods

range :: (SeekMode, SeekMode) -> [SeekMode]

index :: (SeekMode, SeekMode) -> SeekMode -> Int

unsafeIndex :: (SeekMode, SeekMode) -> SeekMode -> Int

inRange :: (SeekMode, SeekMode) -> SeekMode -> Bool

rangeSize :: (SeekMode, SeekMode) -> Int

unsafeRangeSize :: (SeekMode, SeekMode) -> Int

Ix IOMode 
Instance details

Defined in GHC.IO.IOMode

Methods

range :: (IOMode, IOMode) -> [IOMode]

index :: (IOMode, IOMode) -> IOMode -> Int

unsafeIndex :: (IOMode, IOMode) -> IOMode -> Int

inRange :: (IOMode, IOMode) -> IOMode -> Bool

rangeSize :: (IOMode, IOMode) -> Int

unsafeRangeSize :: (IOMode, IOMode) -> Int

Ix Associativity 
Instance details

Defined in GHC.Generics

Methods

range :: (Associativity, Associativity) -> [Associativity]

index :: (Associativity, Associativity) -> Associativity -> Int

unsafeIndex :: (Associativity, Associativity) -> Associativity -> Int

inRange :: (Associativity, Associativity) -> Associativity -> Bool

rangeSize :: (Associativity, Associativity) -> Int

unsafeRangeSize :: (Associativity, Associativity) -> Int

Ix DecidedStrictness 
Instance details

Defined in GHC.Generics

Methods

range :: (DecidedStrictness, DecidedStrictness) -> [DecidedStrictness]

index :: (DecidedStrictness, DecidedStrictness) -> DecidedStrictness -> Int

unsafeIndex :: (DecidedStrictness, DecidedStrictness) -> DecidedStrictness -> Int

inRange :: (DecidedStrictness, DecidedStrictness) -> DecidedStrictness -> Bool

rangeSize :: (DecidedStrictness, DecidedStrictness) -> Int

unsafeRangeSize :: (DecidedStrictness, DecidedStrictness) -> Int

Ix SourceStrictness 
Instance details

Defined in GHC.Generics

Methods

range :: (SourceStrictness, SourceStrictness) -> [SourceStrictness]

index :: (SourceStrictness, SourceStrictness) -> SourceStrictness -> Int

unsafeIndex :: (SourceStrictness, SourceStrictness) -> SourceStrictness -> Int

inRange :: (SourceStrictness, SourceStrictness) -> SourceStrictness -> Bool

rangeSize :: (SourceStrictness, SourceStrictness) -> Int

unsafeRangeSize :: (SourceStrictness, SourceStrictness) -> Int

Ix SourceUnpackedness 
Instance details

Defined in GHC.Generics

Methods

range :: (SourceUnpackedness, SourceUnpackedness) -> [SourceUnpackedness]

index :: (SourceUnpackedness, SourceUnpackedness) -> SourceUnpackedness -> Int

unsafeIndex :: (SourceUnpackedness, SourceUnpackedness) -> SourceUnpackedness -> Int

inRange :: (SourceUnpackedness, SourceUnpackedness) -> SourceUnpackedness -> Bool

rangeSize :: (SourceUnpackedness, SourceUnpackedness) -> Int

unsafeRangeSize :: (SourceUnpackedness, SourceUnpackedness) -> Int

Ix Void 
Instance details

Defined in Data.Void

Methods

range :: (Void, Void) -> [Void]

index :: (Void, Void) -> Void -> Int

unsafeIndex :: (Void, Void) -> Void -> Int

inRange :: (Void, Void) -> Void -> Bool

rangeSize :: (Void, Void) -> Int

unsafeRangeSize :: (Void, Void) -> Int

Ix AllowedReduction Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Ix a => Ix (Identity a) 
Instance details

Defined in Data.Functor.Identity

Methods

range :: (Identity a, Identity a) -> [Identity a]

index :: (Identity a, Identity a) -> Identity a -> Int

unsafeIndex :: (Identity a, Identity a) -> Identity a -> Int

inRange :: (Identity a, Identity a) -> Identity a -> Bool

rangeSize :: (Identity a, Identity a) -> Int

unsafeRangeSize :: (Identity a, Identity a) -> Int

Ix i => Ix (MIx i) Source # 
Instance details

Defined in Agda.Termination.SparseMatrix

Methods

range :: (MIx i, MIx i) -> [MIx i]

index :: (MIx i, MIx i) -> MIx i -> Int

unsafeIndex :: (MIx i, MIx i) -> MIx i -> Int

inRange :: (MIx i, MIx i) -> MIx i -> Bool

rangeSize :: (MIx i, MIx i) -> Int

unsafeRangeSize :: (MIx i, MIx i) -> Int

(Ix a, Ix b) => Ix (a, b) 
Instance details

Defined in GHC.Arr

Methods

range :: ((a, b), (a, b)) -> [(a, b)]

index :: ((a, b), (a, b)) -> (a, b) -> Int

unsafeIndex :: ((a, b), (a, b)) -> (a, b) -> Int

inRange :: ((a, b), (a, b)) -> (a, b) -> Bool

rangeSize :: ((a, b), (a, b)) -> Int

unsafeRangeSize :: ((a, b), (a, b)) -> Int

Ix (Proxy s) 
Instance details

Defined in Data.Proxy

Methods

range :: (Proxy s, Proxy s) -> [Proxy s]

index :: (Proxy s, Proxy s) -> Proxy s -> Int

unsafeIndex :: (Proxy s, Proxy s) -> Proxy s -> Int

inRange :: (Proxy s, Proxy s) -> Proxy s -> Bool

rangeSize :: (Proxy s, Proxy s) -> Int

unsafeRangeSize :: (Proxy s, Proxy s) -> Int

(Ix a1, Ix a2, Ix a3) => Ix (a1, a2, a3) 
Instance details

Defined in GHC.Arr

Methods

range :: ((a1, a2, a3), (a1, a2, a3)) -> [(a1, a2, a3)]

index :: ((a1, a2, a3), (a1, a2, a3)) -> (a1, a2, a3) -> Int

unsafeIndex :: ((a1, a2, a3), (a1, a2, a3)) -> (a1, a2, a3) -> Int

inRange :: ((a1, a2, a3), (a1, a2, a3)) -> (a1, a2, a3) -> Bool

rangeSize :: ((a1, a2, a3), (a1, a2, a3)) -> Int

unsafeRangeSize :: ((a1, a2, a3), (a1, a2, a3)) -> Int

Ix a => Ix (Const a b) 
Instance details

Defined in Data.Functor.Const

Methods

range :: (Const a b, Const a b) -> [Const a b]

index :: (Const a b, Const a b) -> Const a b -> Int

unsafeIndex :: (Const a b, Const a b) -> Const a b -> Int

inRange :: (Const a b, Const a b) -> Const a b -> Bool

rangeSize :: (Const a b, Const a b) -> Int

unsafeRangeSize :: (Const a b, Const a b) -> Int

Ix b => Ix (Tagged s b) 
Instance details

Defined in Data.Tagged

Methods

range :: (Tagged s b, Tagged s b) -> [Tagged s b]

index :: (Tagged s b, Tagged s b) -> Tagged s b -> Int

unsafeIndex :: (Tagged s b, Tagged s b) -> Tagged s b -> Int

inRange :: (Tagged s b, Tagged s b) -> Tagged s b -> Bool

rangeSize :: (Tagged s b, Tagged s b) -> Int

unsafeRangeSize :: (Tagged s b, Tagged s b) -> Int

(Ix a1, Ix a2, Ix a3, Ix a4) => Ix (a1, a2, a3, a4) 
Instance details

Defined in GHC.Arr

Methods

range :: ((a1, a2, a3, a4), (a1, a2, a3, a4)) -> [(a1, a2, a3, a4)]

index :: ((a1, a2, a3, a4), (a1, a2, a3, a4)) -> (a1, a2, a3, a4) -> Int

unsafeIndex :: ((a1, a2, a3, a4), (a1, a2, a3, a4)) -> (a1, a2, a3, a4) -> Int

inRange :: ((a1, a2, a3, a4), (a1, a2, a3, a4)) -> (a1, a2, a3, a4) -> Bool

rangeSize :: ((a1, a2, a3, a4), (a1, a2, a3, a4)) -> Int

unsafeRangeSize :: ((a1, a2, a3, a4), (a1, a2, a3, a4)) -> Int

(Ix a1, Ix a2, Ix a3, Ix a4, Ix a5) => Ix (a1, a2, a3, a4, a5) 
Instance details

Defined in GHC.Arr

Methods

range :: ((a1, a2, a3, a4, a5), (a1, a2, a3, a4, a5)) -> [(a1, a2, a3, a4, a5)]

index :: ((a1, a2, a3, a4, a5), (a1, a2, a3, a4, a5)) -> (a1, a2, a3, a4, a5) -> Int

unsafeIndex :: ((a1, a2, a3, a4, a5), (a1, a2, a3, a4, a5)) -> (a1, a2, a3, a4, a5) -> Int

inRange :: ((a1, a2, a3, a4, a5), (a1, a2, a3, a4, a5)) -> (a1, a2, a3, a4, a5) -> Bool

rangeSize :: ((a1, a2, a3, a4, a5), (a1, a2, a3, a4, a5)) -> Int

unsafeRangeSize :: ((a1, a2, a3, a4, a5), (a1, a2, a3, a4, a5)) -> Int

(\\) :: SmallSetElement a => SmallSet a -> SmallSet a -> SmallSet a Source #

Time O(n).

complement :: SmallSetElement a => SmallSet a -> SmallSet a Source #

Time O(n).

delete :: SmallSetElement a => a -> SmallSet a -> SmallSet a Source #

Time O(n).

difference :: SmallSetElement a => SmallSet a -> SmallSet a -> SmallSet a Source #

Time O(n).

elems :: SmallSetElement a => SmallSet a -> [a] Source #

Time O(n).

empty :: SmallSetElement a => SmallSet a Source #

The empty set. Time O(n).

fromList :: SmallSetElement a => [a] -> SmallSet a Source #

Time O(n).

fromAscList :: SmallSetElement a => [a] -> SmallSet a Source #

Time O(n).

fromDistinctAscList :: SmallSetElement a => [a] -> SmallSet a Source #

Time O(n).

insert :: SmallSetElement a => a -> SmallSet a -> SmallSet a Source #

Time O(n).

intersection :: SmallSetElement a => SmallSet a -> SmallSet a -> SmallSet a Source #

Time O(n).

isSubsetOf :: SmallSetElement a => SmallSet a -> SmallSet a -> Bool Source #

Time O(n).

mapMemberShip :: SmallSetElement a => (Bool -> Bool) -> SmallSet a -> SmallSet a Source #

Time O(n).

member :: SmallSetElement a => a -> SmallSet a -> Bool Source #

Time O(1).

notMember :: SmallSetElement a => a -> SmallSet a -> Bool Source #

not . member a. Time O(1).

null :: SmallSetElement a => SmallSet a -> Bool Source #

Time O(n)!

singleton :: SmallSetElement a => a -> SmallSet a Source #

A singleton set. Time O(n).

toList :: SmallSetElement a => SmallSet a -> [a] Source #

Time O(n).

toAscList :: SmallSetElement a => SmallSet a -> [a] Source #

Time O(n).

total :: SmallSetElement a => SmallSet a Source #

The full set. Time O(n).

union :: SmallSetElement a => SmallSet a -> SmallSet a -> SmallSet a Source #

Time O(n).

zipMemberShipWith :: SmallSetElement a => (Bool -> Bool -> Bool) -> SmallSet a -> SmallSet a -> SmallSet a Source #

Time O(n).