git.iko.soy/Idris-dev
on master help sign in
Fix up issues relating to changes in Idris.
0a4aac7Jan de Muijnck-Hughes
test/tutorial007/Providers.idr+4−1
compare with master
unifiedsplit
@@ -1,13 +1,16 @@
1module Providers
1module Providers
2
2
3+%access export
4+
3%dynamic "./nativetypes.so"
5%dynamic "./nativetypes.so"
4
6
5sizeOfSizeT : IO Int
7sizeOfSizeT : IO Int
6sizeOfSizeT = foreign FFI_C "sizeof_size_t" (IO Int)
8sizeOfSizeT = foreign FFI_C "sizeof_size_t" (IO Int)
7
9
10+public export
8data NativeTypeSize = OneByte | TwoBytes | FourBytes | EightBytes
11data NativeTypeSize = OneByte | TwoBytes | FourBytes | EightBytes
9
12
10−instance Show NativeTypeSize where
13+Show NativeTypeSize where
11 show OneByte = "1 byte"
14 show OneByte = "1 byte"
12 show TwoBytes = "2 bytes"
15 show TwoBytes = "2 bytes"
13 show FourBytes = "4 bytes"
16 show FourBytes = "4 bytes"
test/tutorial007/tutorial007.idr+2−1
@@ -1,11 +1,12 @@
1module Main
1module Main
2import Providers
2import Providers
3+
3%language TypeProviders
4%language TypeProviders
4%provide (szSizeT : NativeTypeSize) with getSizeOfSizeT
5%provide (szSizeT : NativeTypeSize) with getSizeOfSizeT
5
6
6main : IO ()
7main : IO ()
7main = do
8main = do
8− expected <- readFile "sizefromc.txt"
9+ (Right expected) <- readFile "sizefromc.txt" | (Left err) => printLn err
9 putStrLn $ if show szSizeT == expected
10 putStrLn $ if show szSizeT == expected
10 then "Pass"
11 then "Pass"
11 else "Fail: \"" ++ show szSizeT ++ "\" /= \"" ++ expected ++ "\""
12 else "Fail: \"" ++ show szSizeT ++ "\" /= \"" ++ expected ++ "\""