git.iko.soy/Idris-dev
on master help sign in
Type Signatures use IO' l where they can instead of IO
commit674459b9a42a17ead35c036b43f1fc40923821b0 authorSam Elliott <sam@lenary.co.uk> dateSat 4 Apr 2015, 19:28 (12 years ago) parent927fc19
2 files changed+4−4
compare with master
unifiedsplit
libs/prelude/IO.idr+3−3 libs/prelude/Prelude.idr+1−1
libs/prelude/IO.idr+3−3
@@ -152,13 +152,13 @@ FFI_C = MkFFI C_Types String String
152152IO : Type -> Type
153153IO = IO' FFI_C
154154
155−run__provider : IO a -> PrimIO a
156−run__provider (MkIO f) = f (TheWorld prim__TheWorld)
155+run__provider : IO' l a -> PrimIO a
156+run__provider = call__IO
157157
158158prim_fork : PrimIO () -> PrimIO Ptr
159159prim_fork x = prim_io_return prim__vm -- compiled specially
160160
161−fork : IO () -> IO Ptr
161+fork : IO' l () -> IO' l Ptr
162162fork (MkIO f) = MkIO (\w => prim_io_bind
163163 (prim_fork (prim_io_bind (f w)
164164 (\ x => prim_io_return x)))
libs/prelude/Prelude.idr+1−1
@@ -526,7 +526,7 @@ validFile (FHandle h) = do x <- nullPtr h
526526||| @ test the condition of the loop
527527||| @ body the loop body
528528partial -- obviously
529−while : (test : IO Bool) -> (body : IO ()) -> IO ()
529+while : (test : IO' l Bool) -> (body : IO' l ()) -> IO' l ()
530530while t b = do v <- t
531531 if v then do b
532532 while t b