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
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 :: (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 #

The Ix class is used to map a contiguous subrange of values in a type onto integers. It is used primarily for array indexing (see the array package).

The first argument (l,u) of each of these operations is a pair specifying the lower and upper bounds of a contiguous subrange of values.

An implementation is entitled to assume the following laws about these operations:

Minimal complete definition

range, (index | unsafeIndex), inRange

Instances
Ix Bool

Since: base-2.1

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

Since: base-2.1

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

Since: base-2.1

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

Since: base-2.1

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

Since: base-2.1

Instance details

Defined in GHC.Int

Ix Int32

Since: base-2.1

Instance details

Defined in GHC.Int

Ix Int64

Since: base-2.1

Instance details

Defined in GHC.Int

Ix Integer

Since: base-2.1

Instance details

Defined in GHC.Arr

Ix Natural

Since: base-4.8.0.0

Instance details

Defined in GHC.Arr

Ix Ordering

Since: base-2.1

Instance details

Defined in GHC.Arr

Ix Word

Since: base-4.6.0.0

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

Since: base-2.1

Instance details

Defined in GHC.Word

Ix Word16

Since: base-2.1

Instance details

Defined in GHC.Word

Ix Word32

Since: base-2.1

Instance details

Defined in GHC.Word

Ix Word64

Since: base-2.1

Instance details

Defined in GHC.Word

Ix ()

Since: base-2.1

Instance details

Defined in GHC.Arr

Methods

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

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

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

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

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

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

Ix Void

Since: base-4.8.0.0

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 SeekMode

Since: base-4.2.0.0

Instance details

Defined in GHC.IO.Device

Ix Associativity

Since: base-4.9.0.0

Instance details

Defined in GHC.Generics

Ix SourceUnpackedness

Since: base-4.9.0.0

Instance details

Defined in GHC.Generics

Ix SourceStrictness

Since: base-4.9.0.0

Instance details

Defined in GHC.Generics

Ix DecidedStrictness

Since: base-4.9.0.0

Instance details

Defined in GHC.Generics

Ix IOMode

Since: base-4.2.0.0

Instance details

Defined in GHC.IO.IOMode

Ix GeneralCategory

Since: base-2.1

Instance details

Defined in GHC.Unicode

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 AllowedReduction Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Ix a => Ix (Identity a)

Since: base-4.9.0.0

Instance details

Defined in Data.Functor.Identity

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)

Since: base-2.1

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)

Since: base-4.7.0.0

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)

Since: base-2.1

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)

Since: base-4.9.0.0

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)

Since: base-2.1

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)

Since: base-2.1

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).