
  0 | module Data.C.SizeOf
  1 | 
  2 | import Data.C.Integer
  3 | 
  4 | %default total
  5 | 
  6 | ||| Interface for returning the size of a C object in bytes
  7 | public export
  8 | interface SizeOf a where
  9 |   sizeof_ : Bits32
 10 | 
 11 | public export %inline
 12 | sizeof : (0 a : Type) -> SizeOf a => Bits32
 13 | sizeof a = sizeof_ {a}
 14 | 
 15 | --------------------------------------------------------------------------------
 16 | -- Implementations
 17 | --------------------------------------------------------------------------------
 18 | 
 19 | public export %inline
 20 | SizeOf Int8 where
 21 |   sizeof_ = 1
 22 | 
 23 | public export %inline
 24 | SizeOf Bits8 where
 25 |   sizeof_ = 1
 26 | 
 27 | public export %inline
 28 | SizeOf Int16 where
 29 |   sizeof_ = 2
 30 | 
 31 | public export %inline
 32 | SizeOf Bits16 where
 33 |   sizeof_ = 2
 34 | 
 35 | public export %inline
 36 | SizeOf Int32 where
 37 |   sizeof_ = 4
 38 | 
 39 | public export %inline
 40 | SizeOf Bits32 where
 41 |   sizeof_ = 4
 42 | 
 43 | public export %inline
 44 | SizeOf Int64 where
 45 |   sizeof_ = 8
 46 | 
 47 | public export %inline
 48 | SizeOf Bits64 where
 49 |   sizeof_ = 8
 50 | 
 51 | public export %inline
 52 | SizeOf String where
 53 |   sizeof_ = AnyPtrSize
 54 | 
 55 | public export %inline
 56 | SizeOf (Maybe String) where
 57 |   sizeof_ = AnyPtrSize
 58 | 
 59 | public export %inline
 60 | SizeOf AnyPtr where
 61 |   sizeof_ = AnyPtrSize
 62 |