Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Utils.Size

Description

Collection size.

For `TermSize` see Agda.Syntax.Internal.

Synopsis

- class Sized a where
  - size :: a -> Int
  - natSize :: a -> Peano
- data SizedThing a = SizedThing {
  - theSize :: !Int
  - sizedThing :: a
  }
- sizeThing :: Sized a => a -> SizedThing a
- data Peano
  - = Zero
  - | Succ Peano

# 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

- theSize :: !Int
- sizedThing :: a

#### 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 Source #

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 Source #

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

toConstr :: Peano -> Constr Source #

dataTypeOf :: Peano -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Bounded Peano |
Instance details Defined in Data.Peano Methods minBound :: Peano Source # maxBound :: Peano Source #
Enum Peano |
Instance details Defined in Data.Peano Methods succ :: Peano -> Peano Source # pred :: Peano -> Peano Source # toEnum :: Int -> Peano Source # fromEnum :: Peano -> Int Source # enumFrom :: Peano -> [Peano] Source # enumFromThen :: Peano -> Peano -> [Peano] Source # enumFromTo :: Peano -> Peano -> [Peano] Source # enumFromThenTo :: Peano -> Peano -> Peano -> [Peano] Source #
Ix Peano |
Instance details Defined in Data.Peano Methods range :: (Peano, Peano) -> [Peano] Source # index :: (Peano, Peano) -> Peano -> Int Source # unsafeIndex :: (Peano, Peano) -> Peano -> Int Source # inRange :: (Peano, Peano) -> Peano -> Bool Source # rangeSize :: (Peano, Peano) -> Int Source # unsafeRangeSize :: (Peano, Peano) -> Int Source #
Num Peano |
Instance details Defined in Data.Peano Methods (+) :: Peano -> Peano -> Peano Source # (-) :: Peano -> Peano -> Peano Source # (*) :: Peano -> Peano -> Peano Source # negate :: Peano -> Peano Source # abs :: Peano -> Peano Source # signum :: Peano -> Peano Source # fromInteger :: Integer -> Peano Source #
Read Peano |
Instance details Defined in Data.Peano Methods readsPrec :: Int -> ReadS Peano Source # readList :: ReadS [Peano] Source # readPrec :: ReadPrec Peano Source # readListPrec :: ReadPrec [Peano] Source #
Integral Peano |
Instance details Defined in Data.Peano Methods quot :: Peano -> Peano -> Peano Source # rem :: Peano -> Peano -> Peano Source # div :: Peano -> Peano -> Peano Source # mod :: Peano -> Peano -> Peano Source # quotRem :: Peano -> Peano -> (Peano, Peano) Source # divMod :: Peano -> Peano -> (Peano, Peano) Source # toInteger :: Peano -> Integer Source #
Real Peano |
Instance details Defined in Data.Peano Methods toRational :: Peano -> Rational Source #
Show Peano |
Instance details Defined in Data.Peano Methods showsPrec :: Int -> Peano -> ShowS Source # show :: Peano -> String Source # showList :: [Peano] -> ShowS Source #
Eq Peano |
Instance details Defined in Data.Peano Methods (==) :: Peano -> Peano -> Bool Source # (/=) :: Peano -> Peano -> Bool Source #
Ord Peano |
Instance details Defined in Data.Peano Methods compare :: Peano -> Peano -> Ordering Source # (<) :: Peano -> Peano -> Bool Source # (<=) :: Peano -> Peano -> Bool Source # (>) :: Peano -> Peano -> Bool Source # (>=) :: Peano -> Peano -> Bool Source # max :: Peano -> Peano -> Peano Source # min :: Peano -> Peano -> Peano Source #