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 = a -> Int
t b -> Int
forall a. t a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length
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
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 = Int -> a -> SizedThing a
forall a. Int -> a -> SizedThing a
SizedThing (a -> Int
forall a. Sized a => a -> Int
size a
a) a
a
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