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