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

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

import Prelude hiding (null)

import Data.HashMap.Strict (HashMap)
import qualified Data.HashMap.Strict as HashMap
import Data.HashSet (HashSet)
import qualified Data.HashSet as HashSet
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Sequence (Seq)
import qualified Data.Sequence as Seq
import qualified Data.List as List

import Agda.Utils.Null

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

class Sized a where
  size :: a -> Int

instance Sized [a] where
  size :: [a] -> Int
size = [a] -> Int
forall i a. Num i => [a] -> i
List.genericLength

instance Sized (IntMap a) where
  size :: IntMap a -> Int
size = IntMap a -> Int
forall a. IntMap a -> Int
IntMap.size

instance Sized IntSet where
  size :: IntSet -> Int
size = IntSet -> Int
IntSet.size

instance Sized (Map k a) where
  size :: Map k a -> Int
size = Map k a -> Int
forall k a. Map k a -> Int
Map.size

instance Sized (Set a) where
  size :: Set a -> Int
size = Set a -> Int
forall a. Set a -> Int
Set.size

instance Sized (HashMap k a) where
  size :: HashMap k a -> Int
size = HashMap k a -> Int
forall k a. HashMap k a -> Int
HashMap.size

instance Sized (HashSet a) where
  size :: HashSet a -> Int
size = HashSet a -> Int
forall a. HashSet a -> Int
HashSet.size

instance Sized (Seq a) where
  size :: Seq a -> Int
size = Seq a -> Int
forall a. Seq a -> Int
Seq.length


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

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

-- | Cache the size of an object.
sizeThing :: Sized a => a -> SizedThing a
sizeThing :: 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

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