blob: 69c6c9a9ff716c75416123cac597d720320c8765 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
viewtypedef initializable (vt:viewt@ype) =
[initialized: bool] @{ initialized = bool initialized, obj = opt (vt, initialized) }
fun {vt:viewt@ype} uninitialized (v : opt(vt,false)): initializable vt
fun {vt:viewt@ype} exec_void (r: ref(initializable vt)):<!refwrt> void
fun {vt:viewt@ype} exec_void$fwork (v : &vt):<!wrt> void
fun {vt:viewt@ype} {a: t@ype} exec (r: ref(initializable vt)):<!refwrt> a
fun {vt:viewt@ype} {a: t@ype} exec$fwork (v : &vt):<!wrt> a
fun {vt:viewt@ype} initialize (r: ref(initializable vt)):<!ref,!wrt> void
fun {vt:viewt@ype} initialize$fwork (v: &vt? >> opt(vt,success)):<!wrt> #[success : bool] bool success
|
