ddc-code-0.4.2.1: tetra/base/Data/Ref.ds

module Data.Ref
export { allocRef; readRef; writeRef }

import foreign boxed type
 Ref       : Region ~> Data ~> Data

import foreign c value
 allocRef  : [r: Region]. [a: Data]. a  -> S (Alloc r) (Ref r a)
 readRef   : [r: Region]. [a: Data]. Ref r a -> S (Read r) a
 writeRef_ : [r: Region]. [a: Data]. Ref r a -> a -> S (Write r) Void#

where


-- | Wrap up the primitive writeRef to return a unit result.
writeRef (ref: Ref r a) (x: a): S (Write r) Unit
 = do   writeRef_ ref x
        ()