Agda
Safe HaskellNone
LanguageHaskell2010

Agda.Utils.Size

Description

Collection size.

For TermSize see Agda.Syntax.Internal.

Synopsis

Documentation

class Sized a where Source #

The size of a collection (i.e., its length).

Minimal complete definition

Nothing

Methods

size :: a -> Int Source #

Strict size computation.

Anti-patterns: size xs == n where n is 0, 1 or another number that is likely smaller than size xs. Similar for size xs >= 1 etc. Use natSize instead.

See https://wiki.haskell.org/Haskell_programming_tips#Don.27t_ask_for_the_length_of_a_list_when_you_don.27t_need_it .

default size :: forall (t :: Type -> Type) b. (Foldable t, t b ~ a) => a -> Int Source #

natSize :: a -> Peano Source #

Lazily compute a (possibly infinite) size.

Use when comparing a size against a fixed number.

default natSize :: forall (t :: Type -> Type) b. (Foldable t, t b ~ a) => a -> Peano Source #

Instances

Instances details
Sized ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

size :: ModuleName -> Int Source #

natSize :: ModuleName -> Peano Source #

Sized QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

size :: QName -> Int Source #

natSize :: QName -> Peano Source #

Sized RawTopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

Methods

size :: RawTopLevelModuleName -> Int Source #

natSize :: RawTopLevelModuleName -> Peano Source #

Sized TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

Methods

size :: TopLevelModuleName -> Int Source #

natSize :: TopLevelModuleName -> Peano Source #

Sized OccursWhere Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

size :: OccursWhere -> Int Source #

natSize :: OccursWhere -> Peano Source #

Sized Permutation Source # 
Instance details

Defined in Agda.Utils.Permutation

Methods

size :: Permutation -> Int Source #

natSize :: Permutation -> Peano Source #

Sized IntSet Source # 
Instance details

Defined in Agda.Utils.Size

Methods

size :: IntSet -> Int Source #

natSize :: IntSet -> Peano Source #

Sized a => Sized (Abs a) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

size :: Abs a -> Int Source #

natSize :: Abs a -> Peano Source #

Sized (Tele a) Source #

The size of a telescope is its length (as a list).

Instance details

Defined in Agda.Syntax.Internal

Methods

size :: Tele a -> Int Source #

natSize :: Tele a -> Peano Source #

Sized (List1 a) Source # 
Instance details

Defined in Agda.Utils.Size

Methods

size :: List1 a -> Int Source #

natSize :: List1 a -> Peano Source #

Sized (SizedThing a) Source #

Return the cached size.

Instance details

Defined in Agda.Utils.Size

Methods

size :: SizedThing a -> Int Source #

natSize :: SizedThing a -> Peano Source #

Sized (IntMap a) Source # 
Instance details

Defined in Agda.Utils.Size

Methods

size :: IntMap a -> Int Source #

natSize :: IntMap a -> Peano Source #

Sized (Seq a) Source # 
Instance details

Defined in Agda.Utils.Size

Methods

size :: Seq a -> Int Source #

natSize :: Seq a -> Peano Source #

Sized (Set a) Source # 
Instance details

Defined in Agda.Utils.Size

Methods

size :: Set a -> Int Source #

natSize :: Set a -> Peano Source #

Sized (HashSet a) Source # 
Instance details

Defined in Agda.Utils.Size

Methods

size :: HashSet a -> Int Source #

natSize :: HashSet a -> Peano Source #

Sized [a] Source # 
Instance details

Defined in Agda.Utils.Size

Methods

size :: [a] -> Int Source #

natSize :: [a] -> Peano Source #

Sized (Map k a) Source # 
Instance details

Defined in Agda.Utils.Size

Methods

size :: Map k a -> Int Source #

natSize :: Map k a -> Peano Source #

Sized (HashMap k a) Source # 
Instance details

Defined in Agda.Utils.Size

Methods

size :: HashMap k a -> Int Source #

natSize :: HashMap k a -> Peano Source #

data SizedThing a Source #

Thing decorated with its size. The thing should fit into main memory, thus, the size is an Int.

Constructors

SizedThing 

Fields

Instances

Instances details
Null a => Null (SizedThing a) Source # 
Instance details

Defined in Agda.Utils.Size

Methods

empty :: SizedThing a Source #

null :: SizedThing a -> Bool Source #

Sized (SizedThing a) Source #

Return the cached size.

Instance details

Defined in Agda.Utils.Size

Methods

size :: SizedThing a -> Int Source #

natSize :: SizedThing a -> Peano Source #

sizeThing :: Sized a => a -> SizedThing a Source #

Cache the size of an object.

data Peano #

The natural numbers in (lazy) unary notation.

Constructors

Zero 
Succ Peano 

Instances

Instances details
Data Peano # 
Instance details

Defined in Data.Peano

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Peano -> c Peano #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Peano #

toConstr :: Peano -> Constr #

dataTypeOf :: Peano -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Peano) #

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

gmapT :: (forall b. Data b => b -> b) -> Peano -> Peano #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Peano -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Peano -> r #

gmapQ :: (forall d. Data d => d -> u) -> Peano -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Peano -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Peano -> m Peano #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Peano -> m Peano #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Peano -> m Peano #

Bounded Peano # 
Instance details

Defined in Data.Peano

Methods

minBound :: Peano #

maxBound :: Peano #

Enum Peano # 
Instance details

Defined in Data.Peano

Methods

succ :: Peano -> Peano #

pred :: Peano -> Peano #

toEnum :: Int -> Peano #

fromEnum :: Peano -> Int #

enumFrom :: Peano -> [Peano] #

enumFromThen :: Peano -> Peano -> [Peano] #

enumFromTo :: Peano -> Peano -> [Peano] #

enumFromThenTo :: Peano -> Peano -> Peano -> [Peano] #

Generic Peano # 
Instance details

Defined in Data.Peano

Associated Types

type Rep Peano 
Instance details

Defined in Data.Peano

type Rep Peano = D1 ('MetaData "Peano" "Data.Peano" "peano-0.1.1.0-b0fc580119d081d6a1ee57458ffa4d247983093a4d2615a8d7c2a51ba8547bc8" 'False) (C1 ('MetaCons "Zero" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Succ" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Peano)))

Methods

from :: Peano -> Rep Peano x #

to :: Rep Peano x -> Peano #

Ix Peano # 
Instance details

Defined in Data.Peano

Methods

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

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

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

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

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

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

Num Peano # 
Instance details

Defined in Data.Peano

Methods

(+) :: Peano -> Peano -> Peano #

(-) :: Peano -> Peano -> Peano #

(*) :: Peano -> Peano -> Peano #

negate :: Peano -> Peano #

abs :: Peano -> Peano #

signum :: Peano -> Peano #

fromInteger :: Integer -> Peano #

Read Peano # 
Instance details

Defined in Data.Peano

Methods

readsPrec :: Int -> ReadS Peano #

readList :: ReadS [Peano] #

readPrec :: ReadPrec Peano #

readListPrec :: ReadPrec [Peano] #

Integral Peano # 
Instance details

Defined in Data.Peano

Methods

quot :: Peano -> Peano -> Peano #

rem :: Peano -> Peano -> Peano #

div :: Peano -> Peano -> Peano #

mod :: Peano -> Peano -> Peano #

quotRem :: Peano -> Peano -> (Peano, Peano) #

divMod :: Peano -> Peano -> (Peano, Peano) #

toInteger :: Peano -> Integer #

Real Peano # 
Instance details

Defined in Data.Peano

Methods

toRational :: Peano -> Rational #

Show Peano # 
Instance details

Defined in Data.Peano

Methods

showsPrec :: Int -> Peano -> ShowS #

show :: Peano -> String #

showList :: [Peano] -> ShowS #

Eq Peano # 
Instance details

Defined in Data.Peano

Methods

(==) :: Peano -> Peano -> Bool #

(/=) :: Peano -> Peano -> Bool #

Ord Peano # 
Instance details

Defined in Data.Peano

Methods

compare :: Peano -> Peano -> Ordering #

(<) :: Peano -> Peano -> Bool #

(<=) :: Peano -> Peano -> Bool #

(>) :: Peano -> Peano -> Bool #

(>=) :: Peano -> Peano -> Bool #

max :: Peano -> Peano -> Peano #

min :: Peano -> Peano -> Peano #

type Rep Peano # 
Instance details

Defined in Data.Peano

type Rep Peano = D1 ('MetaData "Peano" "Data.Peano" "peano-0.1.1.0-b0fc580119d081d6a1ee57458ffa4d247983093a4d2615a8d7c2a51ba8547bc8" 'False) (C1 ('MetaCons "Zero" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Succ" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Peano)))