IORef.idr

module Data.IORef

%default total

||| A mutable variable in the IO monad.
export
data IORef a = MkIORef a

public export
interface HasReference (ffi : FFI) where
  newIORef' : a -> IO' ffi (IORef a)
  readIORef' : IORef a -> IO' ffi a
  writeIORef' : IORef a -> a -> IO' ffi ()

export
modifyIORef': HasReference ffi => IORef a -> (a -> a) -> IO' ffi ()
modifyIORef' ref fn =
  do
    val <- readIORef' ref
    writeIORef' ref (fn val)

export
implementation HasReference FFI_C where
  newIORef' val
    = do MkRaw ref <- foreign FFI_C "idris_newRef" (Raw a -> IO (Raw a)) (MkRaw val)
         pure (MkIORef ref)
  readIORef' (MkIORef ref)
    = do MkRaw val <- foreign FFI_C "idris_readRef" (Raw a -> IO (Raw a)) (MkRaw ref)
         pure val
  writeIORef' (MkIORef ref) val
    = foreign FFI_C "idris_writeRef" (Raw a -> Raw a -> IO ())
              (MkRaw ref) (MkRaw val)

export
implementation HasReference FFI_JS where
  newIORef' val =
    (MkIORef . believe_me) <$> foreign FFI_JS "{val: %0}" (Ptr -> JS_IO Ptr) (believe_me val)
  readIORef' (MkIORef ref) =
    believe_me <$> foreign FFI_JS "%0.val" (Ptr -> JS_IO Ptr) (believe_me ref)
  writeIORef' (MkIORef ref) val =
    foreign FFI_JS "%0.val = %1" (Ptr -> Ptr -> JS_IO ()) (believe_me ref) (believe_me val)

||| Build a new IORef
export
newIORef : a -> IO (IORef a)
newIORef = newIORef'

||| read the value of an IORef
export
readIORef : IORef a -> IO a
readIORef = readIORef'

||| write the value of an IORef
export
writeIORef : IORef a -> a -> IO ()
writeIORef = writeIORef'

||| mutate the contents of an IORef
export
modifyIORef : IORef a -> (a -> a) -> IO ()
modifyIORef = modifyIORef'