28 lines
1.0 KiB
Agda
28 lines
1.0 KiB
Agda
module Data.IORef
|
|
|
|
import Prelude
|
|
|
|
-- We should test this at some point
|
|
|
|
ptype IORef : U → U
|
|
pfunc primNewIORef uses (MkIORes MkUnit) : ∀ a. a → IO (IORef a) := `(_, a) => (w) => MkIORes(undefined, [a], w)`
|
|
pfunc primReadIORef uses (MkIORes MkUnit) : ∀ a. IORef a → IO a := `(_, ref) => (w) => MkIORes(undefined, ref[0], w)`
|
|
pfunc primWriteIORef uses (MkIORes MkUnit) : ∀ a. IORef a → a → IO Unit := `(_, ref, a) => (w) => {
|
|
ref[0] = a
|
|
return MkIORes(undefined,MkUnit,w)
|
|
}`
|
|
|
|
newIORef : ∀ io a. {{HasIO io}} → a → io (IORef a)
|
|
newIORef a = liftIO $ primNewIORef a
|
|
|
|
readIORef : ∀ io a. {{HasIO io}} → IORef a → io a
|
|
readIORef ref = liftIO $ primReadIORef ref
|
|
|
|
writeIORef : ∀ io a. {{HasIO io}} → IORef a -> a -> io Unit
|
|
writeIORef ref a = liftIO $ primWriteIORef ref a
|
|
|
|
-- Idris HasIO constraints to monad, we don't have those constraints yet
|
|
modifyIORef : ∀ io a. {{Monad io}} {{HasIO io}} → IORef a -> (a -> a) -> io Unit
|
|
modifyIORef {io} ref f =
|
|
bind {io} (readIORef ref) $ \a => writeIORef ref (f a)
|