aboutsummaryrefslogtreecommitdiff
path: root/lib/SATS/init.sats
blob: 9fe8581477528e34db460140fa22f948e87c75b1 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
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

// function will also inialize if not yet initalized
fun {vt:viewt@ype} exec_init (r: ref(initializable vt)):<!refwrt> 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