1 open lock
2
3
4
5
6
7
8 data wref a =
9 WRef { contents: (r: unknown, lock (r @ ref a)) }
10
11
12
13 val new [a] (consumes x: a) : wref a =
14 let r = newref x in
15 let l : lock (r @ ref a) = new () in
16 WRef { contents = (r, l) }
17
18
19
20 val swap [a] (r: wref a, consumes y: a) : a =
21 let r, l = r.contents in
22 acquire l;
23 let x = r.contents in
24 r.contents <- y;
25 release l;
26 x
27
28
29
30
31
32
33
34
35
36
37
38 val get [a] duplicable a => (r: wref a) : a =
39 let r, l = r.contents in
40 acquire l;
41 let x = r.contents in
42 release l;
43 x
44
45
46
47 val set [a] (r: wref a, consumes y: a) : () =
48 let r, l = r.contents in
49 acquire l;
50 r.contents <- y;
51 release l
52
53
54
55 val update [a, b, p : perm] (r: wref a, f: (consumes (a | p)) -> (a, b) | consumes p) : b =
56 let r, l = r.contents in
57 acquire l;
58 let x = r.contents in
59 let y, result = f x in
60
61
62
63
64 if x != y then
65 r.contents <- y;
66 release l;
67 result
68
69 val borrow [a, b, p : perm] (r: wref a, f: (a | consumes p) -> b | consumes p) : b =
70 let r, l = r.contents in
71 acquire l;
72 let x = r.contents in
73 let result = f x in
74 release l;
75 result
76
77
78
79
80
81