module Data.IORef %cg chicken (use box) -- Implemented externally-- e.g., in Scheme, passed around as a boxdata Mut : Type -> Type where [external] %extern prim__newIORef : forall a . a -> (1 x : %World) -> IORes (Mut a)%extern prim__readIORef : forall a . Mut a -> (1 x : %World) -> IORes a%extern prim__writeIORef : forall a . Mut a -> (1 val : a) -> (1 x : %World) -> IORes () exportdata IORef : Type -> Type where     MkRef : Mut a -> IORef a exportnewIORef : a -> IO (IORef a)newIORef val    = do m <- primIO (prim__newIORef val)         pure (MkRef m) exportreadIORef : IORef a -> IO areadIORef (MkRef m) = primIO (prim__readIORef m) exportwriteIORef : IORef a -> (1 val : a) -> IO ()writeIORef (MkRef m) val = primIO (prim__writeIORef m val) exportmodifyIORef : IORef a -> (a -> a) -> IO ()modifyIORef ref f    = do val <- readIORef ref         writeIORef ref (f val)