    -- | Collection size.
    --
    --   For 'TermSize' see "Agda.Syntax.Internal".

    module Agda.Utils.Size
      ( Sized(..)
      , SizedThing(..)
      , sizeThing
      , module X
      ) where

    import Prelude hiding (null, length)

    import Data.Peano as X     ( Peano(Zero,Succ) )
    import Data.Foldable       (Foldable, length)
    import Data.HashMap.Strict (HashMap)
    import Data.HashSet        (HashSet)
    import Data.IntMap         (IntMap)
    import Data.IntSet         (IntSet)
    import qualified Data.IntSet as IntSet
    import Data.Map            (Map)
    import Data.Set            (Set)
    import Data.Sequence       (Seq)

    import Agda.Utils.List1    (List1)
    import Agda.Utils.Null

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

    class Sized a where
      -- | 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 .
      size :: a -> Int

      default size :: (Foldable t, t b ~ a) => a -> Int
      size = a -> Int
    t b -> Int
    forall a. t a -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length

      -- | Lazily compute a (possibly infinite) size.
      --
      -- Use when comparing a size against a fixed number.
      natSize :: a -> Peano

      default natSize :: (Foldable t, t b ~ a) => a -> Peano
      natSize = (b -> Peano -> Peano) -> Peano -> t b -> Peano
    forall a b. (a -> b -> b) -> b -> t a -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr ((Peano -> Peano) -> b -> Peano -> Peano
    forall a b. a -> b -> a
    const Peano -> Peano
    Succ) Peano
    Zero

    instance Sized [a]
    instance Sized (Set a)
    instance Sized (HashMap k a)
    instance Sized (HashSet a)
    instance Sized (IntMap a)
    instance Sized (List1 a)
    instance Sized (Map k a)
    instance Sized (Seq a)
    instance Sized IntSet where
      size :: IntSet -> Int
    size = IntSet -> Int
    IntSet.size
      natSize :: IntSet -> Peano
    natSize = Int -> Peano
    forall a. Enum a => Int -> a
    toEnum (Int -> Peano) -> (IntSet -> Int) -> IntSet -> Peano
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . IntSet -> Int
    forall a. Sized a => a -> Int
    size

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

    data SizedThing a = SizedThing
      { forall a. SizedThing a -> Int
    theSize    :: !Int
      , forall a. SizedThing a -> a
    sizedThing :: a
      }

    -- | Cache the size of an object.
    sizeThing :: Sized a => a -> SizedThing a
    sizeThing :: forall a. Sized a => a -> SizedThing a
    sizeThing a
    a = Int -> a -> SizedThing a
    forall a. Int -> a -> SizedThing a
    SizedThing (a -> Int
    forall a. Sized a => a -> Int
    size a
    a) a
    a

    -- | Return the cached size.
    instance Sized (SizedThing a) where
      size :: SizedThing a -> Int
    size = SizedThing a -> Int
    forall a. SizedThing a -> Int
    theSize
      natSize :: SizedThing a -> Peano
    natSize = Int -> Peano
    forall a. Enum a => Int -> a
    toEnum (Int -> Peano) -> (SizedThing a -> Int) -> SizedThing a -> Peano
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SizedThing a -> Int
    forall a. SizedThing a -> Int
    theSize

    instance Null a => Null (SizedThing a) where
      empty :: SizedThing a
    empty = Int -> a -> SizedThing a
    forall a. Int -> a -> SizedThing a
    SizedThing Int
    0 a
    forall a. Null a => a
    empty
      null :: SizedThing a -> Bool
    null  = a -> Bool
    forall a. Null a => a -> Bool
    null (a -> Bool) -> (SizedThing a -> a) -> SizedThing a -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SizedThing a -> a
    forall a. SizedThing a -> a
    sizedThing