git.iko.soy/Idris-dev
on master help sign in
Type Signatures use IO' l where they can instead of IO
674459bSam Elliott
libs/prelude/IO.idr+3−3
compare with master
unifiedsplit
@@ -152,13 +152,13 @@ FFI_C = MkFFI C_Types String String
152IO : Type -> Type
152IO : Type -> Type
153IO = IO' FFI_C
153IO = IO' FFI_C
154
154
155−run__provider : IO a -> PrimIO a
155+run__provider : IO' l a -> PrimIO a
156−run__provider (MkIO f) = f (TheWorld prim__TheWorld)
156+run__provider = call__IO
157
157
158prim_fork : PrimIO () -> PrimIO Ptr
158prim_fork : PrimIO () -> PrimIO Ptr
159prim_fork x = prim_io_return prim__vm -- compiled specially
159prim_fork x = prim_io_return prim__vm -- compiled specially
160
160
161−fork : IO () -> IO Ptr
161+fork : IO' l () -> IO' l Ptr
162fork (MkIO f) = MkIO (\w => prim_io_bind
162fork (MkIO f) = MkIO (\w => prim_io_bind
163 (prim_fork (prim_io_bind (f w)
163 (prim_fork (prim_io_bind (f w)
164 (\ x => prim_io_return x)))
164 (\ x => prim_io_return x)))
libs/prelude/Prelude.idr+1−1
@@ -526,7 +526,7 @@ validFile (FHandle h) = do x <- nullPtr h
526||| @ test the condition of the loop
526||| @ test the condition of the loop
527||| @ body the loop body
527||| @ body the loop body
528partial -- obviously
528partial -- obviously
529−while : (test : IO Bool) -> (body : IO ()) -> IO ()
529+while : (test : IO' l Bool) -> (body : IO' l ()) -> IO' l ()
530while t b = do v <- t
530while t b = do v <- t
531 if v then do b
531 if v then do b
532 while t b
532 while t b