The at-views of the form T@L for types T and addresses L are building blocks for constructing other forms of views. One mechanism for putting together such building blocks is by declaring dataviews, which is mostly identical to declaring dataprops. I now present in this chapter some commonly encountered dataviews and their uses.
Please find on-line the code presented for illustration in this chapter.
The dataview option_v is declared as follows:
This declaration indicates that 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, the following function interface involves a typical use of optional view:
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.