git.iko.soy/Idris-dev
on master help sign in
Friendly smart constructors for foreign integer types
308efeaBenjamin Saunders
effects/Effect/Memory.idr+5−5
compare with master
unifiedsplit
@@ -39,7 +39,7 @@ data RawMemory : Effect where
39private
39private
40do_malloc : Nat -> IOExcept String Ptr
40do_malloc : Nat -> IOExcept String Ptr
41do_malloc size with (fromInteger (cast size) == size)
41do_malloc size with (fromInteger (cast size) == size)
42− | True = do ptr <- ioe_lift $ mkForeign (FFun "malloc" [FInt ITNative] FPtr) (cast size)
42+ | True = do ptr <- ioe_lift $ mkForeign (FFun "malloc" [FInt] FPtr) (cast size)
43 fail <- ioe_lift $ nullPtr ptr
43 fail <- ioe_lift $ nullPtr ptr
44 if fail then ioe_fail "Cannot allocate memory"
44 if fail then ioe_fail "Cannot allocate memory"
45 else return ptr
45 else return ptr
@@ -48,7 +48,7 @@ do_malloc size with (fromInteger (cast size) == size)
48private
48private
49do_memset : Ptr -> Nat -> Bits8 -> Nat -> IO ()
49do_memset : Ptr -> Nat -> Bits8 -> Nat -> IO ()
50do_memset ptr offset c size
50do_memset ptr offset c size
51− = mkForeign (FFun "idris_memset" [FPtr, FInt ITNative, FAny Bits8, FInt ITNative] FUnit)
51+ = mkForeign (FFun "idris_memset" [FPtr, FInt, FChar, FInt] FUnit)
52 ptr (cast offset) c (cast size)
52 ptr (cast offset) c (cast size)
53
53
54private
54private
@@ -58,14 +58,14 @@ do_free ptr = mkForeign (FFun "free" [FPtr] FUnit) ptr
58private
58private
59do_memmove : Ptr -> Ptr -> Nat -> Nat -> Nat -> IO ()
59do_memmove : Ptr -> Ptr -> Nat -> Nat -> Nat -> IO ()
60do_memmove dest src dest_offset src_offset size
60do_memmove dest src dest_offset src_offset size
61− = mkForeign (FFun "idris_memmove" [FPtr, FPtr, FInt ITNative, FInt ITNative, FInt ITNative] FUnit)
61+ = mkForeign (FFun "idris_memmove" [FPtr, FPtr, FInt, FInt, FInt] FUnit)
62 dest src (cast dest_offset) (cast src_offset) (cast size)
62 dest src (cast dest_offset) (cast src_offset) (cast size)
63
63
64private
64private
65do_peek : Ptr -> Nat -> (size : Nat) -> IO (Vect Bits8 size)
65do_peek : Ptr -> Nat -> (size : Nat) -> IO (Vect Bits8 size)
66do_peek _ _ O = return (Prelude.Vect.Nil)
66do_peek _ _ O = return (Prelude.Vect.Nil)
67do_peek ptr offset (S n)
67do_peek ptr offset (S n)
68− = do b <- mkForeign (FFun "idris_peek" [FPtr, FInt ITNative] (FInt ITNative)) ptr (cast offset)
68+ = do b <- mkForeign (FFun "idris_peek" [FPtr, FInt] FInt) ptr (cast offset)
69 bs <- do_peek ptr (S offset) n
69 bs <- do_peek ptr (S offset) n
70 Prelude.Monad.return (Prelude.Vect.(::) (prim__intToB8 b) bs)
70 Prelude.Monad.return (Prelude.Vect.(::) (prim__intToB8 b) bs)
71
71
@@ -73,7 +73,7 @@ private
73do_poke : Ptr -> Nat -> Vect Bits8 size -> IO ()
73do_poke : Ptr -> Nat -> Vect Bits8 size -> IO ()
74do_poke _ _ [] = return ()
74do_poke _ _ [] = return ()
75do_poke ptr offset (b::bs)
75do_poke ptr offset (b::bs)
76− = do mkForeign (FFun "idris_poke" [FPtr, FInt ITNative, FAny Bits8] FUnit) ptr (cast offset) b
76+ = do mkForeign (FFun "idris_poke" [FPtr, FInt, FChar] FUnit) ptr (cast offset) b
77 do_poke ptr (S offset) bs
77 do_poke ptr (S offset) bs
78
78
79instance Handler RawMemory (IOExcept String) where
79instance Handler RawMemory (IOExcept String) where
lib/IO.idr+18−7
@@ -22,16 +22,27 @@ run__IO : IO () -> IO ()
22run__IO v = io_bind v (\v' => io_return v')
22run__IO v = io_bind v (\v' => io_return v')
23
23
24data IntTy = ITNative | IT8 | IT16 | IT32 | IT64
24data IntTy = ITNative | IT8 | IT16 | IT32 | IT64
25−data FTy = FInt IntTy | FFloat | FChar | FString | FPtr | FAny Type | FUnit
25+data FTy = FIntT IntTy | FFloat | FString | FPtr | FAny Type | FUnit
26+
27+FInt : FTy
28+FInt = FIntT ITNative
29+
30+FChar : FTy
31+FChar = FIntT IT8
32+
33+FShort : FTy
34+FShort = FIntT IT16
35+
36+FLong : FTy
37+FLong = FIntT IT64
26
38
27interpFTy : FTy -> Type
39interpFTy : FTy -> Type
28−interpFTy (FInt ITNative) = Int
40+interpFTy (FIntT ITNative) = Int
29−interpFTy (FInt IT8) = Bits8
41+interpFTy (FIntT IT8) = Bits8
30−interpFTy (FInt IT16) = Bits16
42+interpFTy (FIntT IT16) = Bits16
31−interpFTy (FInt IT32) = Bits32
43+interpFTy (FIntT IT32) = Bits32
32−interpFTy (FInt IT64) = Bits64
44+interpFTy (FIntT IT64) = Bits64
33interpFTy FFloat = Float
45interpFTy FFloat = Float
34−interpFTy FChar = Char
35interpFTy FString = String
46interpFTy FString = String
36interpFTy FPtr = Ptr
47interpFTy FPtr = Ptr
37interpFTy (FAny t) = t
48interpFTy (FAny t) = t
lib/Prelude.idr+5−5
@@ -251,11 +251,11 @@ getLine = return (prim__readString prim__stdin)
251
251
252partial
252partial
253putChar : Char -> IO ()
253putChar : Char -> IO ()
254−putChar c = mkForeign (FFun "putchar" [FChar] FUnit) c
254+putChar c = mkForeign (FFun "putchar" [FInt] FUnit) (cast c)
255
255
256partial
256partial
257getChar : IO Char
257getChar : IO Char
258−getChar = mkForeign (FFun "getchar" [] FChar)
258+getChar = fmap cast $ mkForeign (FFun "getchar" [] FInt)
259
259
260---- some basic file handling
260---- some basic file handling
261
261
@@ -307,7 +307,7 @@ fwrite (FHandle h) s = do_fwrite h s
307
307
308partial
308partial
309do_feof : Ptr -> IO Int
309do_feof : Ptr -> IO Int
310−do_feof h = mkForeign (FFun "fileEOF" [FPtr] (FInt ITNative)) h
310+do_feof h = mkForeign (FFun "fileEOF" [FPtr] FInt) h
311
311
312feof : File -> IO Bool
312feof : File -> IO Bool
313feof (FHandle h) = do eof <- do_feof h
313feof (FHandle h) = do eof <- do_feof h
@@ -315,7 +315,7 @@ feof (FHandle h) = do eof <- do_feof h
315
315
316partial
316partial
317do_ferror : Ptr -> IO Int
317do_ferror : Ptr -> IO Int
318−do_ferror h = mkForeign (FFun "fileError" [FPtr] (FInt ITNative)) h
318+do_ferror h = mkForeign (FFun "fileError" [FPtr] FInt) h
319
319
320ferror : File -> IO Bool
320ferror : File -> IO Bool
321ferror (FHandle h) = do err <- do_ferror h
321ferror (FHandle h) = do err <- do_ferror h
@@ -323,7 +323,7 @@ ferror (FHandle h) = do err <- do_ferror h
323
323
324partial
324partial
325nullPtr : Ptr -> IO Bool
325nullPtr : Ptr -> IO Bool
326−nullPtr p = do ok <- mkForeign (FFun "isNull" [FPtr] (FInt ITNative)) p
326+nullPtr p = do ok <- mkForeign (FFun "isNull" [FPtr] FInt) p
327 return (ok /= 0);
327 return (ok /= 0);
328
328
329partial
329partial
lib/System.idr+4−4
@@ -10,10 +10,10 @@ getArgs = do n <- numArgs
10 ga' [] 0 n
10 ga' [] 0 n
11 where
11 where
12 numArgs : IO Int
12 numArgs : IO Int
13− numArgs = mkForeign (FFun "idris_numArgs" [FPtr] (FInt ITNative)) prim__vm
13+ numArgs = mkForeign (FFun "idris_numArgs" [FPtr] FInt) prim__vm
14
14
15 getArg : Int -> IO String
15 getArg : Int -> IO String
16− getArg x = mkForeign (FFun "idris_getArg" [FPtr, FInt ITNative] (FAny String)) prim__vm x
16+ getArg x = mkForeign (FFun "idris_getArg" [FPtr, FInt] (FAny String)) prim__vm x
17
17
18 ga' : List String -> Int -> Int -> IO (List String)
18 ga' : List String -> Int -> Int -> IO (List String)
19 ga' acc i n = if (i == n) then (return $ reverse acc) else
19 ga' acc i n = if (i == n) then (return $ reverse acc) else
@@ -24,8 +24,8 @@ getEnv : String -> IO String
24getEnv x = mkForeign (FFun "getenv" [FString] FString) x
24getEnv x = mkForeign (FFun "getenv" [FString] FString) x
25
25
26exit : Int -> IO ()
26exit : Int -> IO ()
27−exit code = mkForeign (FFun "exit" [FInt ITNative] FUnit) code
27+exit code = mkForeign (FFun "exit" [FInt] FUnit) code
28
28
29usleep : Int -> IO ()
29usleep : Int -> IO ()
30−usleep i = mkForeign (FFun "usleep" [FInt ITNative] FUnit) i
30+usleep i = mkForeign (FFun "usleep" [FInt] FUnit) i
31
31
lib/System/Concurrency/Raw.idr+1−1
@@ -15,7 +15,7 @@ sendToThread {a} dest val
15
15
16checkMsgs : IO Bool
16checkMsgs : IO Bool
17checkMsgs = do msgs <- mkForeign (FFun "idris_checkMessage"
17checkMsgs = do msgs <- mkForeign (FFun "idris_checkMessage"
18− [FPtr] (FInt ITNative)) prim__vm
18+ [FPtr] FInt) prim__vm
19 return (intToBool msgs)
19 return (intToBool msgs)
20
20
21-- Check inbox for messages. If there are none, blocks until a message
21-- Check inbox for messages. If there are none, blocks until a message
src/IRTS/Compiler.hs+1−1
@@ -284,7 +284,7 @@ getFTypes tm = case unApply tm of
284 _ -> Nothing
284 _ -> Nothing
285
285
286mkIty' (P _ (UN ty) _) = mkIty ty
286mkIty' (P _ (UN ty) _) = mkIty ty
287−mkIty' (App (P _ (UN "FInt") _) (P _ (UN intTy) _)) = mkIntIty intTy
287+mkIty' (App (P _ (UN "FIntT") _) (P _ (UN intTy) _)) = mkIntIty intTy
288mkIty' _ = FAny
288mkIty' _ = FAny
289
289
290mkIty "FFloat" = FDouble
290mkIty "FFloat" = FDouble