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
class Sized a where
size :: a -> Int
default size :: (Foldable t, t b ~ a) => a -> Int
size = forall (t :: * -> *) a. Foldable t => t a -> Int
length
natSize :: a -> Peano
default natSize :: (Foldable t, t b ~ a) => a -> Peano
natSize = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (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 = forall a. Enum a => Int -> a
toEnum forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Sized a => a -> Int
size
data SizedThing a = SizedThing
{ forall a. SizedThing a -> Int
theSize :: !Int
, forall a. SizedThing a -> a
sizedThing :: a
}
sizeThing :: Sized a => a -> SizedThing a
sizeThing :: forall a. Sized a => a -> SizedThing a
sizeThing a
a = forall a. Int -> a -> SizedThing a
SizedThing (forall a. Sized a => a -> Int
size a
a) a
a
instance Sized (SizedThing a) where
size :: SizedThing a -> Int
size = forall a. SizedThing a -> Int
theSize
natSize :: SizedThing a -> Peano
natSize = forall a. Enum a => Int -> a
toEnum forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. SizedThing a -> Int
theSize
instance Null a => Null (SizedThing a) where
empty :: SizedThing a
empty = forall a. Int -> a -> SizedThing a
SizedThing Int
0 forall a. Null a => a
empty
null :: SizedThing a -> Bool
null = forall a. Null a => a -> Bool
null forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. SizedThing a -> a
sizedThing