git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2116 from lenary/relax-io-types
b8a3f7eDavid Christiansen
libs/prelude/IO.idr+3−1
compare with master
unifiedsplit
@@ -152,13 +152,15 @@ FFI_C = MkFFI C_Types String String
152IO : Type -> Type
152IO : Type -> Type
153IO = IO' FFI_C
153IO = IO' FFI_C
154
154
155+-- Cannot be relaxed as is used by type providers and they expect IO a
156+-- in the first argument.
155run__provider : IO a -> PrimIO a
157run__provider : IO a -> PrimIO a
156run__provider (MkIO f) = f (TheWorld prim__TheWorld)
158run__provider (MkIO f) = f (TheWorld prim__TheWorld)
157
159
158prim_fork : PrimIO () -> PrimIO Ptr
160prim_fork : PrimIO () -> PrimIO Ptr
159prim_fork x = prim_io_return prim__vm -- compiled specially
161prim_fork x = prim_io_return prim__vm -- compiled specially
160
162
161−fork : IO () -> IO Ptr
163+fork : IO' l () -> IO' l Ptr
162fork (MkIO f) = MkIO (\w => prim_io_bind
164fork (MkIO f) = MkIO (\w => prim_io_bind
163 (prim_fork (prim_io_bind (f w)
165 (prim_fork (prim_io_bind (f w)
164 (\ x => prim_io_return x)))
166 (\ 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