git.iko.soy/Idris-dev
on master help sign in
Friendly smart constructors for foreign integer types
commit308efeab8b0fca9862ed46d207c8f2c867ec6a71 authorBenjamin Saunders <besaunde@sfu.ca> dateThu 2 May 2013, 09:30 (13 years ago) parentfadeecd
6 files changed+34−23
compare with master
unifiedsplit
effects/Effect/Memory.idr+5−5 lib/IO.idr+18−7 lib/Prelude.idr+5−5 lib/System.idr+4−4 lib/System/Concurrency/Raw.idr+1−1 src/IRTS/Compiler.hs+1−1
effects/Effect/Memory.idr+5−5
@@ -39,7 +39,7 @@ data RawMemory : Effect where
3939private
4040do_malloc : Nat -> IOExcept String Ptr
4141do_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)
4343 fail <- ioe_lift $ nullPtr ptr
4444 if fail then ioe_fail "Cannot allocate memory"
4545 else return ptr
@@ -48,7 +48,7 @@ do_malloc size with (fromInteger (cast size) == size)
4848private
4949do_memset : Ptr -> Nat -> Bits8 -> Nat -> IO ()
5050do_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)
5252 ptr (cast offset) c (cast size)
5353
5454private
@@ -58,14 +58,14 @@ do_free ptr = mkForeign (FFun "free" [FPtr] FUnit) ptr
5858private
5959do_memmove : Ptr -> Ptr -> Nat -> Nat -> Nat -> IO ()
6060do_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)
6262 dest src (cast dest_offset) (cast src_offset) (cast size)
6363
6464private
6565do_peek : Ptr -> Nat -> (size : Nat) -> IO (Vect Bits8 size)
6666do_peek _ _ O = return (Prelude.Vect.Nil)
6767do_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)
6969 bs <- do_peek ptr (S offset) n
7070 Prelude.Monad.return (Prelude.Vect.(::) (prim__intToB8 b) bs)
7171
@@ -73,7 +73,7 @@ private
7373do_poke : Ptr -> Nat -> Vect Bits8 size -> IO ()
7474do_poke _ _ [] = return ()
7575do_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
7777 do_poke ptr (S offset) bs
7878
7979instance Handler RawMemory (IOExcept String) where
lib/IO.idr+18−7
@@ -22,16 +22,27 @@ run__IO : IO () -> IO ()
2222run__IO v = io_bind v (\v' => io_return v')
2323
2424data 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
2638
2739interpFTy : FTy -> Type
28−interpFTy (FInt ITNative) = Int
29−interpFTy (FInt IT8) = Bits8
30−interpFTy (FInt IT16) = Bits16
31−interpFTy (FInt IT32) = Bits32
32−interpFTy (FInt IT64) = Bits64
40+interpFTy (FIntT ITNative) = Int
41+interpFTy (FIntT IT8) = Bits8
42+interpFTy (FIntT IT16) = Bits16
43+interpFTy (FIntT IT32) = Bits32
44+interpFTy (FIntT IT64) = Bits64
3345interpFTy FFloat = Float
34−interpFTy FChar = Char
3546interpFTy FString = String
3647interpFTy FPtr = Ptr
3748interpFTy (FAny t) = t
lib/Prelude.idr+5−5
@@ -251,11 +251,11 @@ getLine = return (prim__readString prim__stdin)
251251
252252partial
253253putChar : Char -> IO ()
254−putChar c = mkForeign (FFun "putchar" [FChar] FUnit) c
254+putChar c = mkForeign (FFun "putchar" [FInt] FUnit) (cast c)
255255
256256partial
257257getChar : IO Char
258−getChar = mkForeign (FFun "getchar" [] FChar)
258+getChar = fmap cast $ mkForeign (FFun "getchar" [] FInt)
259259
260260---- some basic file handling
261261
@@ -307,7 +307,7 @@ fwrite (FHandle h) s = do_fwrite h s
307307
308308partial
309309do_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
311311
312312feof : File -> IO Bool
313313feof (FHandle h) = do eof <- do_feof h
@@ -315,7 +315,7 @@ feof (FHandle h) = do eof <- do_feof h
315315
316316partial
317317do_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
319319
320320ferror : File -> IO Bool
321321ferror (FHandle h) = do err <- do_ferror h
@@ -323,7 +323,7 @@ ferror (FHandle h) = do err <- do_ferror h
323323
324324partial
325325nullPtr : 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
327327 return (ok /= 0);
328328
329329partial
lib/System.idr+4−4
@@ -10,10 +10,10 @@ getArgs = do n <- numArgs
1010 ga' [] 0 n
1111 where
1212 numArgs : IO Int
13− numArgs = mkForeign (FFun "idris_numArgs" [FPtr] (FInt ITNative)) prim__vm
13+ numArgs = mkForeign (FFun "idris_numArgs" [FPtr] FInt) prim__vm
1414
1515 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
1717
1818 ga' : List String -> Int -> Int -> IO (List String)
1919 ga' acc i n = if (i == n) then (return $ reverse acc) else
@@ -24,8 +24,8 @@ getEnv : String -> IO String
2424getEnv x = mkForeign (FFun "getenv" [FString] FString) x
2525
2626exit : Int -> IO ()
27−exit code = mkForeign (FFun "exit" [FInt ITNative] FUnit) code
27+exit code = mkForeign (FFun "exit" [FInt] FUnit) code
2828
2929usleep : Int -> IO ()
30−usleep i = mkForeign (FFun "usleep" [FInt ITNative] FUnit) i
30+usleep i = mkForeign (FFun "usleep" [FInt] FUnit) i
3131
lib/System/Concurrency/Raw.idr+1−1
@@ -15,7 +15,7 @@ sendToThread {a} dest val
1515
1616checkMsgs : IO Bool
1717checkMsgs = do msgs <- mkForeign (FFun "idris_checkMessage"
18− [FPtr] (FInt ITNative)) prim__vm
18+ [FPtr] FInt) prim__vm
1919 return (intToBool msgs)
2020
2121-- 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
284284 _ -> Nothing
285285
286286mkIty' (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
288288mkIty' _ = FAny
289289
290290mkIty "FFloat" = FDouble