The dataview VOR is declared as follows:
dataview VOR (v0:view+, v1:view+, int) = | VORleft (v0, v1, 0) of (v0) | VORright (v0, v1, 1) of (v1)
Let T be some type. The following function interface states that getopt takes an unintialized pointer and returns an integers indicating whether the pointer is initialized:
The following code shows a typical use of getopt:fun foo (): void = let var x: T? val (pfor | i) = getopt (view@(x) | addr@(x)) in // if i = 0 then let prval VORleft (pf0) = pfor in view@(x) := pf0 // uninitialized end // end of [then] else let prval VORright (pf1) = pfor in view@(x) := pf1 // initialized end // end of [else] // end of [if] // end // end of [foo]
In ATS, there is a type constructor opt that takes a type T and a boolean B to form an opt-type opt(T, B) such that opt(T, B) equals T if B is true and it equals T? if B is false. The function getopt can be given the following interface that makes use of an opt-type:
The code that calls getopt can now be implemented as follows: where the proof functions opt_unsome and opt_unnone are assgined the following types: Compared to the version that uses VOR, this version based on opt-type is considerably less verbose.