(* 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 (r: ('t, 'c) ureadcap_rep ref) = let rec loop () = 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 (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 (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 (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: ('a, 't) array) (ix: int) = liftBang (get a ix) let putAU (a: ('a, 't) array) (ix: int) (new: 'a) = let f (cap: 't writecap) = ((), set a ix new cap) in liftBang f end end type 't uwritecap = ('t, 1) ureadcap let test () = let n = 10 in let (a, cap) = new 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 ())