git.iko.soy/Idris-dev
on 385dcbf help sign in
Idris-dev/test/tutorial007/Providers.idr
27 lines 671 B history raw
1module Providers
3%access export
5%dynamic "./nativetypes.so"
7sizeOfSizeT : IO Int
8sizeOfSizeT = foreign FFI_C "sizeof_size_t" (IO Int)
10public export
11data NativeTypeSize = OneByte | TwoBytes | FourBytes | EightBytes
13Show NativeTypeSize where
14 show OneByte = "1 byte"
15 show TwoBytes = "2 bytes"
16 show FourBytes = "4 bytes"
17 show EightBytes = "8 bytes"
19bytesToType : Int -> Provider NativeTypeSize
20bytesToType 1 = Provide OneByte
21bytesToType 2 = Provide TwoBytes
22bytesToType 4 = Provide FourBytes
23bytesToType 8 = Provide EightBytes
24bytesToType _ = Error "Unsupported size"
26getSizeOfSizeT : IO (Provider NativeTypeSize)
27getSizeOfSizeT = map bytesToType sizeOfSizeT