Optional Views

The dataview option_v is declared as follows:

dataview option_v (v:view+, bool) =
  | Some_v (v, true) of (v) | None_v (v, false) of ()
// end of [option_v]

By the declaration, the dataview option_v is covariant in its first argument and there are two proof constructors associated with it: Some_v and None_v. Given a view V, option_v(V, b) is often called an optional view, where b is a boolean. Clearly, a proof of the view option_v(V, true) contains a proof of the view V while a proof the view option_v(V, false) contains nothing. As an example, let us take a look at the following function template interface:

fun{a:t@ype}
ptr_alloc_opt (): [l:addr] (option_v (a? @ l, l > null) | ptr l)

Given a type T, the function ptr_alloc_opt<T> returns a pointer paired with a proof of an optional view; if the returned pointer is not null, then the proof can be turned into a proof of the view T?@L, where L is the location to which the pointer points; otherwise, there is no at-view associated with the returned pointer.

To see another example, let us assume that get_width is given the interface below:

fun get_width (x: &window): int

where window is some (unboxed) abstract type. One may think that get_width returns the width of a window object. The following code shows a typical use of an optional view:

viewdef optat
  (a:t@ype, l:addr) = option_v (a @ l, l > null)
// end of [optat]

fun get_width_alt {l:addr} (
  pf: !optat (int?, l) >> optat (int, l)
| x: &window, p: ptr l
) : void =
  if p > null then let
    prval Some_v (pf1) = pf
    val () = !p := get_width (x)
  in
    pf := Some_v (pf1)
  end else let
    prval None_v () = pf in pf := None_v ()
  end // end of [val]
// end of [get_width_alt]

The function get_width_alt is a variation of get_width. In addtion to the window object, it takes a pointer which, if not null, points to the location where the width information should be stored.

Please find the entirety of the above presented code on-line.