git.iko.soy/Idris-dev
on master help sign in
New test: Type Provider backed by new FFI_C

The Type Provider tutorial currently depends on deprecated FFI (see the new FFI. Fixes to the tutorial will follow.

commitebbae35323e8328757641eda2423fb867589c62b authorJacob Mitchell <jmitchell@member.fsf.org> dateFri 30 Oct 2015, 22:58 (11 years ago) parente4a04b4
5 files changed+42
compare with master
unifiedsplit
test/tutorial007/Providers.idr+24 test/tutorial007/expected+1 test/tutorial007/nativetypes.c+3 test/tutorial007/run+5 test/tutorial007/tutorial007.idr+9
test/tutorial007/Providers.idrnew file+24
@@ -0,0 +1,24 @@
1+module Providers
2+
3+%dynamic "./nativetypes.so"
4+
5+sizeOfSizeT : IO Int
6+sizeOfSizeT = foreign FFI_C "sizeof_size_t" (IO Int)
7+
8+data NativeTypeSize = OneByte | TwoBytes | FourBytes | EightBytes
9+
10+instance Show NativeTypeSize where
11+ show OneByte = "1 byte"
12+ show TwoBytes = "2 bytes"
13+ show FourBytes = "4 bytes"
14+ show EightBytes = "8 bytes"
15+
16+bytesToType : Int -> Provider NativeTypeSize
17+bytesToType 1 = Provide OneByte
18+bytesToType 2 = Provide TwoBytes
19+bytesToType 4 = Provide FourBytes
20+bytesToType 8 = Provide EightBytes
21+bytesToType _ = Error "Unsupported size"
22+
23+getSizeOfSizeT : IO (Provider NativeTypeSize)
24+getSizeOfSizeT = map bytesToType sizeOfSizeT
test/tutorial007/expectednew file+1
@@ -0,0 +1 @@
1+sizeof(size_t): 8 bytes
test/tutorial007/nativetypes.cnew file+3
@@ -0,0 +1,3 @@
1+#include <stdio.h>
2+
3+int sizeof_size_t() { return sizeof(size_t); }
test/tutorial007/runnew file+5
@@ -0,0 +1,5 @@
1+#!/usr/bin/env bash
2+gcc -shared nativetypes.c -o nativetypes.so
3+idris $@ tutorial007.idr -o tutorial007
4+./tutorial007
5+rm -f tutorial007 *.ibc *.so
test/tutorial007/tutorial007.idrnew file+9
@@ -0,0 +1,9 @@
1+module Main
2+import Providers
3+%language TypeProviders
4+%provide (szSizeT : NativeTypeSize) with getSizeOfSizeT
5+
6+main : IO ()
7+main = do
8+ putStr "sizeof(size_t): "
9+ putStrLn (show szSizeT)