alms-0.4.9: examples/ex26-let-bang-array.alms

(* An encoding of Wadler's let! construct.
   Allows temporarily viewing an array as unlimited/read-only. *)

#load "libarraycap"

open AArray

abstype ('t, 'c) ureadcap_rep qualifier A
  = Available of ('t, 'c) readcap
  | CheckedOut
  | Defunct
with
  abstype ('t, 'c) ureadcap qualifier U
    = MkCap of ('t, 'c) ureadcap_rep ref
  with

    (* We represent this thing with (essentially) as a spinlock.
       Acquire the spinlock: *)
    let acquireBang['t, 'c] (r: ('t, 'c) ureadcap_rep ref) =
      let rec loop (): ('t, 'c) readcap =
        match r <- CheckedOut with
        | Available c -> c
        | CheckedOut  -> loop ()
        | Defunct     -> failwith "letBang: attempt to use defunct ureadcap"
      in loop ()

    (* Given a capability, create a temporary, unlimited read capability
       and pass that to a call-back.  Return the result of the callback
       and the restored capability. *)
    let letBang['t, 'c, `a] (c: ('t, 'c) readcap)|
                                (k: ('t, 'c) ureadcap -o `a)
                                : `a * ('t, 'c) readcap =
      let r  = ref (Available c) in
      let uc = MkCap r in
      let a  = k uc in
      let c  = acquireBang r in
        r <- Defunct;
        (a, c)

    let applyBang['t,'c,`r]
             (k: ('t, 'c) readcap -o `r * ('t, 'c) readcap)
             |
             (MkCap r: ('t, 'c) ureadcap)
             : `r =
      let (result, c) = k (acquireBang r) in
        r <- Available c;
        result

    let liftBang['t,'c,`r]
             (k: ('t, 'c) readcap -> `r * ('t, 'c) readcap)
             (MkCap r: ('t, 'c) ureadcap)
             : `r =
      let (result, c) = k (acquireBang r) in
        r <- Available c;
        result

    let getAU['a,'t,'c] (a: ('a, 't) array) (ix: int) =
      liftBang (get['a,'t,'c] a ix)

    let putAU['a,'t] (a: ('a, 't) array) (ix: int) (new: 'a) =
      let f (cap: 't writecap) = ((), set['a,'t] a ix new cap) in
        liftBang f
  end
end

type 't uwritecap = ('t, 1) ureadcap

let test () =
  let n = 10 in
  let Pack('t, a, cap) = new[int] n 0 in
    let rec loop (i: int) (cap: 't writecap): 't writecap =
      if i >= n
        then cap
        else loop (i + 1) (set a i (i * i) cap) in
    let cap = loop 0 cap in
    let (r, cap) = letBang cap
      (fun (cap: 't uwritecap) ->
         getAU a 1 cap + getAU a 3 cap + getAU a 5 cap) in
      set a 0 (-1) cap;
      r

in print (test ())