Chapter 14. 線形なデータ命題としてのデータ観 (dataview)

Table of Contents
オプショナル観
選言的な観
線形配列のデータ観
線形文字列のデータ観
片方向リストのデータ観
観変化のための証明関数

型 T とアドレス L について T@L をなす駐観 (at-view) は他の形の観をコンストラクトするブロックを形成します。 そのような形成されたブロックを一緒に配置するメカニズムはデータ観 (dataview) として宣言されます。 大部分においてそれはデータ命題 (dataprop) の宣言と同じです。 この章ではいくつかの一般なデータ観とその使い方を紹介します。

この章で解説するコードは オンライン から入手できます。

オプショナル観

データ観 option_v は次のように宣言されます:

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

この宣言はデータ観 option_v が1番目の引数に対して共変で、 関連する2つの証明コンストラクタ Some_vNone_v があることを示しています。 観 V が与えられ、b がブールの時、option_v(V, b) はしばしばオプショナル観 (optional view) と呼ばれます。 明確に観 option_v(V, true) の証明は観 V の証明を含んでいますが、観 option_v(V, false) の証明は何も含んでいません。

例として、次の関数インターフェイスはオプショナル観の典型的な使用例です:

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

型 T が与えられた時、 関数 ptr_alloc_opt<T> はオプショナル観の証明とポインタのペアを返します; もし返されたポインタが NULL でなければ、 ポインタが指す場所 L についてその証明は観 T?@L の証明に成ることができます; そうでなければ、返されたポインタに関連する駐観は含まれません。