packages feed

idris-0.11.1: test/tutorial007/Providers.idr

module Providers

%access export

%dynamic "./nativetypes.so"

sizeOfSizeT : IO Int
sizeOfSizeT = foreign FFI_C "sizeof_size_t" (IO Int)

public export
data NativeTypeSize = OneByte | TwoBytes | FourBytes | EightBytes

Show NativeTypeSize where
  show OneByte = "1 byte"
  show TwoBytes = "2 bytes"
  show FourBytes = "4 bytes"
  show EightBytes = "8 bytes"

bytesToType : Int -> Provider NativeTypeSize
bytesToType 1 = Provide OneByte
bytesToType 2 = Provide TwoBytes
bytesToType 4 = Provide FourBytes
bytesToType 8 = Provide EightBytes
bytesToType _ = Error "Unsupported size"

getSizeOfSizeT : IO (Provider NativeTypeSize)
getSizeOfSizeT = map bytesToType sizeOfSizeT