git.iko.soy/Idris-dev
on master help sign in
Make some IO types more specific
eb041bcEdwin Brady
CHANGELOG+2
compare with master
unifiedsplit
@@ -19,6 +19,8 @@ Language updates
19* Name binding in patterns follows the same rule as name binding for implicits
19* Name binding in patterns follows the same rule as name binding for implicits
20 in types: names which begin with lower case letters, not applied to any
20 in types: names which begin with lower case letters, not applied to any
21 arguments, are treated as bound pattern variables.
21 arguments, are treated as bound pattern variables.
22+* Added %deprecate directive, which gives a warning and a message when a
23+ deprecated name is referenced.
22
24
23Library updates
25Library updates
24---------------
26---------------
libs/prelude/IO.idr+6−3
@@ -117,11 +117,11 @@ io_return x = MkIO (\w => prim_io_return x)
117liftPrimIO : (World -> PrimIO a) -> IO' l a
117liftPrimIO : (World -> PrimIO a) -> IO' l a
118liftPrimIO = MkIO
118liftPrimIO = MkIO
119
119
120−call__IO : IO' l a -> PrimIO a
120+call__IO : IO' ffi a -> PrimIO a
121call__IO (MkIO f) = f (TheWorld prim__TheWorld)
121call__IO (MkIO f) = f (TheWorld prim__TheWorld)
122
122
123-- Concrete type makes it easier to elaborate at top level
123-- Concrete type makes it easier to elaborate at top level
124−run__IO : IO' l () -> PrimIO ()
124+run__IO : IO' ffi () -> PrimIO ()
125run__IO f = call__IO f
125run__IO f = call__IO f
126
126
127unsafePerformIO : IO' ffi a -> a
127unsafePerformIO : IO' ffi a -> a
@@ -176,8 +176,11 @@ namespace FFI_C
176 FFI_C : FFI
176 FFI_C : FFI
177 FFI_C = MkFFI C_Types String String
177 FFI_C = MkFFI C_Types String String
178
178
179+||| The type of interactive programs, performing some I/O side effects
180+||| and returning a value.
181+||| @res The result type of the program
179%error_reverse
182%error_reverse
180−IO : Type -> Type
183+IO : (res : Type) -> Type
181IO = IO' FFI_C
184IO = IO' FFI_C
182
185
183-- Cannot be relaxed as is used by type providers and they expect IO a
186-- Cannot be relaxed as is used by type providers and they expect IO a
libs/prelude/Prelude/Interactive.idr+39−14
@@ -25,33 +25,58 @@ import IO
25
25
26---- some basic io
26---- some basic io
27
27
28+||| Output a string to stdout without a trailing newline, for any FFI
29+||| descriptor
30+putStr' : String -> IO' ffi ()
31+putStr' x = do prim_write x
32+ return ()
33+
28||| Output a string to stdout without a trailing newline
34||| Output a string to stdout without a trailing newline
29−putStr : String -> IO' ffi ()
35+putStr : String -> IO ()
30−putStr x = do prim_write x
36+putStr = putStr'
31− return ()
37+
38+||| Output a string to stdout with a trailing newline, for any FFI
39+||| descriptor
40+putStrLn' : String -> IO' ffi ()
41+putStrLn' x = putStr' (x ++ "\n")
32
42
33||| Output a string to stdout with a trailing newline
43||| Output a string to stdout with a trailing newline
34−putStrLn : String -> IO' ffi ()
44+putStrLn : String -> IO ()
45+putStrLn = putStrLn'
46+
47+||| Output something showable to stdout, without a trailing newline, for any FFI
48+||| descriptor
49+print' : Show a => a -> IO' ffi ()
35−putStrLn x = putStr (x ++ "\n")
50+print' x = putStr' (show x)
36
51
37||| Output something showable to stdout, without a trailing newline
52||| Output something showable to stdout, without a trailing newline
38−print : Show a => a -> IO' ffi ()
53+print : Show a => a -> IO ()
39−print x = putStr (show x)
54+print = print'
40
55
41−||| Output something showable to stdout, with a trailing newline
56+||| Output something showable to stdout, with a trailing newline, for any FFI
57+||| descriptor
42−printLn : Show a => a -> IO' ffi ()
58+printLn' : Show a => a -> IO' ffi ()
43−printLn x = putStrLn (show x)
59+printLn' x = putStrLn' (show x)
44
60
61+||| Output something showable to stdout, with a trailing newline
62+printLn : Show a => a -> IO ()
63+printLn = printLn'
64+
45−||| Read one line of input from stdin, without the trailing newline
65+||| Read one line of input from stdin, without the trailing newline, for any FFI
66+||| descriptor
46−getLine : IO' ffi String
67+getLine' : IO' ffi String
47−getLine = do x <- prim_read
68+getLine' = do x <- prim_read
48− return (reverse (trimNL (reverse x)))
69+ return (reverse (trimNL (reverse x)))
49 where trimNL : String -> String
70 where trimNL : String -> String
50 trimNL str with (strM str)
71 trimNL str with (strM str)
51 trimNL "" | StrNil = ""
72 trimNL "" | StrNil = ""
52 trimNL (strCons '\n' xs) | StrCons _ _ = xs
73 trimNL (strCons '\n' xs) | StrCons _ _ = xs
53 trimNL (strCons x xs) | StrCons _ _ = strCons x xs
74 trimNL (strCons x xs) | StrCons _ _ = strCons x xs
54
75
76+||| Read one line of input from stdin, without the trailing newline
77+getLine : IO String
78+getLine = getLine'
79+
55||| Write a single character to stdout
80||| Write a single character to stdout
56putChar : Char -> IO ()
81putChar : Char -> IO ()
57putChar c = foreign FFI_C "putchar" (Int -> IO ()) (cast c)
82putChar c = foreign FFI_C "putchar" (Int -> IO ()) (cast c)
src/Idris/Elab/Value.hs+2−1
@@ -127,7 +127,8 @@ elabExec fc tm = runtm (PAlternative [] FirstSuccess
127 printtm tm
127 printtm tm
128 ])
128 ])
129 where
129 where
130− runtm t = PApp fc (PRef fc [] (sUN "run__IO")) [pexp t]
130+ runtm t = PApp fc (PRef fc [] (sUN "run__IO"))
131+ [pimp (sUN "ffi") (PRef fc [] (sUN "FFI_C")) False, pexp t]
131 printtm t = PApp fc (PRef fc [] (sUN "printLn"))
132 printtm t = PApp fc (PRef fc [] (sUN "printLn"))
132 [pimp (sUN "ffi") (PRef fc [] (sUN "FFI_C")) False, pexp t]
133 [pimp (sUN "ffi") (PRef fc [] (sUN "FFI_C")) False, pexp t]
133
134