
   0 | module Data.Linear.Ref1
   1 | 
   2 | import public Data.Linear.Token
   3 | 
   4 | %default total
   5 | 
   6 | --------------------------------------------------------------------------------
   7 | -- Prim Calls
   8 | --------------------------------------------------------------------------------
   9 | 
  10 | -- Implemented externally
  11 | -- e.g., in Scheme, passed around as a box
  12 | data Mut : Type -> Type where [external]
  13 | 
  14 | %extern prim__newIORef : forall a . a -> (1 x : %World) -> IORes (Mut a)
  15 | %extern prim__readIORef : forall a . Mut a -> (1 x : %World) -> IORes a
  16 | %extern prim__writeIORef : forall a . Mut a -> (1 val : a) -> (1 x : %World) -> IORes ()
  17 | 
  18 | 
  19 | %foreign "scheme:(lambda (a x v w) (if (box-cas! x v w) 1 0))"
  20 |          "javascript:lambda:(a,x,v,w) => {if (x.value === v) {x.value = w; return 1;} else {return 0;}}"
  21 | prim__casWrite : Mut a -> (prev,val : a) -> Bits8
  22 | 
  23 | --------------------------------------------------------------------------------
  24 | -- Ref1: A linearily mutable reference
  25 | --------------------------------------------------------------------------------
  26 | 
  27 | ||| A linear mutable reference
  28 | export
  29 | data Ref : (s,a : Type) -> Type where
  30 |   R1 : (mut : Mut a) -> Ref s a
  31 | 
  32 | ||| Alias for `Ref RIO`
  33 | public export
  34 | 0 IORef : Type -> Type
  35 | IORef = Ref World
  36 | 
  37 | --------------------------------------------------------------------------------
  38 | -- utilities
  39 | --------------------------------------------------------------------------------
  40 | 
  41 | ||| Creates a new mutable reference tagged with `tag` and holding
  42 | ||| initial value `v`.
  43 | export %inline
  44 | ref1 : (v : a) -> F1 s (Ref s a)
  45 | ref1 v t = let m # t := ffi (prim__newIORef v) t in R1 m # t
  46 | 
  47 | |||
  48 | export %inline
  49 | newref : Lift1 s f => (v : a) -> f (Ref s a)
  50 | newref = lift1 . ref1
  51 | 
  52 | ||| Creates a mutable reference in `IO` land.
  53 | |||
  54 | ||| Deprecated: Use `newref` instead
  55 | export %inline %deprecate
  56 | newIORef : HasIO io => (v : a) -> io (IORef a)
  57 | newIORef v = runIO (ref1 v)
  58 | 
  59 | ||| Reads the current value at a mutable reference tagged with `tag`.
  60 | export %inline
  61 | read1 : (r : Ref s a) -> F1 s a
  62 | read1 (R1 m) = ffi (prim__readIORef m)
  63 | 
  64 | ||| Convenience alias for `runIO $ read1 r` for reading a reference in
  65 | ||| `IO`.
  66 | export %inline
  67 | readref : Lift1 s f => Ref s a -> f a
  68 | readref = lift1 . read1
  69 | 
  70 | ||| Updates the mutable reference tagged with `tag`.
  71 | export %inline
  72 | write1 : (r : Ref s a) -> (val : a) -> F1' s
  73 | write1 (R1 m) val = ffi (prim__writeIORef m val)
  74 | 
  75 | ||| Convenience alias for `runIO $ write1 r v` for writing to a reference in
  76 | ||| `IO`.
  77 | export %inline
  78 | writeref : Lift1 s f => Ref s a -> a -> f ()
  79 | writeref r = lift1 . write1 r
  80 | 
  81 | ||| Atomically writes `val` to the mutable reference if its current
  82 | ||| value is equal to `pre`.
  83 | |||
  84 | ||| This is supported and has been tested on the Chez and Racket backends.
  85 | ||| It trivially works on the JavaScript backends, which are single-threaded
  86 | ||| anyway.
  87 | export %inline
  88 | caswrite1 : (r : Ref s a) -> (pre,val : a) -> F1 s Bool
  89 | caswrite1 (R1 m) pre val t =
  90 |   -- The use of `believe_me` is justified because the foreign call
  91 |   -- returns 0 for `False` and 1 for `True`. These are exactly
  92 |   -- the values a `Bool` is converted to during codegen.
  93 |   believe_me (prim__casWrite m pre val) # t
  94 | 
  95 | ||| Atomic overwrite of a mutable reference using a CAS-loop
  96 | ||| internally
  97 | |||
  98 | ||| This is supported and has been tested on the Chez and Racket backends.
  99 | ||| It trivially works on the JavaScript backends, which are single-threaded
 100 | ||| anyway.
 101 | export
 102 | casswap1 : (r : Ref s a) -> a -> F1' s
 103 | casswap1 r v t = assert_total (loop t)
 104 |   where
 105 |     covering loop : F1' s
 106 |     loop t =
 107 |       let cur  # t := read1 r t
 108 |           True # t := caswrite1 r cur v t | _ # t => loop t
 109 |        in () # t
 110 | 
 111 | ||| Atomic modification of a mutable reference using a CAS-loop
 112 | ||| internally
 113 | |||
 114 | ||| This is supported and has been tested on the Chez and Racket backends.
 115 | ||| It trivially works on the JavaScript backends, which are single-threaded
 116 | ||| anyway.
 117 | export
 118 | casupdate1 : (r : Ref s a) -> (a -> (a,b)) -> F1 s b
 119 | casupdate1 r f t = assert_total (loop t)
 120 |   where
 121 |     covering loop : F1 s b
 122 |     loop t =
 123 |       let cur # t  := read1 r t
 124 |           (new,v)  := f cur
 125 |           True # t := caswrite1 r cur new t | _ # t => loop t
 126 |        in v # t
 127 | 
 128 | ||| Atomically updates and reads a mutable reference in `IO`.
 129 | |||
 130 | ||| This uses `casupdate1` internally.
 131 | export %inline
 132 | update : Lift1 s f => Ref s a -> (a -> (a,b)) -> f b
 133 | update r = lift1 . casupdate1 r
 134 | 
 135 | ||| Atomic modification of a mutable reference using a CAS-loop
 136 | ||| internally
 137 | |||
 138 | ||| This is supported and has been tested on the Chez and Racket backends.
 139 | ||| It trivially works on the JavaScript backends, which are single-threaded
 140 | ||| anyway.
 141 | export
 142 | casmod1 : (r : Ref s a) -> (a -> a) -> F1' s
 143 | casmod1 r f t = assert_total (loop t)
 144 |   where
 145 |     covering loop : F1' s
 146 |     loop t =
 147 |       let cur  # t := read1 r t
 148 |           True # t := caswrite1 r cur (f cur) t | _ # t => loop t
 149 |        in () # t
 150 | 
 151 | ||| Modifies the value stored in mutable reference tagged with `tag`.
 152 | export %inline
 153 | mod1 : (r : Ref s a) -> (f : a -> a) -> F1' s
 154 | mod1 r f t = let v # t2 := read1 r t in write1 r (f v) t2
 155 | 
 156 | ||| Atomically modifies a mutable reference in `IO`.
 157 | |||
 158 | ||| This uses `casmod1` internally.
 159 | export %inline
 160 | mod : Lift1 s f => Ref s a -> (a -> a) -> f ()
 161 | mod r = lift1 . casmod1 r
 162 | 
 163 | ||| Modifies the value stored in mutable reference tagged with `tag`
 164 | ||| and returns the updated value.
 165 | export
 166 | modAndRead1 : (r : Ref s a) -> (f : a -> a) -> F1 s a
 167 | modAndRead1 r f t =
 168 |   let _ # t := mod1 r f t
 169 |    in read1 r t
 170 | 
 171 | ||| Modifies the value stored in mutable reference tagged with `tag`
 172 | ||| and returns the previous value.
 173 | export
 174 | readAndMod1 : (r : Ref s a) -> (f : a -> a) -> F1 s a
 175 | readAndMod1 r f t =
 176 |   let v # t := read1 r t
 177 |       _ # t := write1 r (f v) t
 178 |    in v # t
 179 | 
 180 | ||| Runs the given stateful computation only when given boolean flag
 181 | ||| is currently at `True`
 182 | export
 183 | whenRef1 : (r : Ref s Bool) -> Lazy (F1' s) -> F1' s
 184 | whenRef1 r f t = let b # t1 := read1 r t in when1 b f t1
 185 | 
 186 | --------------------------------------------------------------------------------
 187 | -- Allocating mutable references
 188 | --------------------------------------------------------------------------------
 189 | 
 190 | ||| Alias for a function taking a linear mutable refernce as
 191 | ||| an auto-implicit argument.
 192 | public export
 193 | 0 WithRef1 : (a,b : Type) -> Type
 194 | WithRef1 a b = forall s . (r : Ref s a) -> F1 s b
 195 | 
 196 | ||| Runs a function requiring a linear mutable reference.
 197 | export
 198 | withRef1 : a -> WithRef1 a b -> b
 199 | withRef1 v f = run1 $ \t => let r # t := ref1 v t in f r t
 200 |