ほとんどのプログラミング言語と異なり、ATS では配列はプリミティブなデータ構造ではありません。 もっと正確に言えば、永続的な配列はプログラマが安全に解放できる線形配列を用いて実装できます。 その線形配列は駐観を用いて実装できます。 直観的には、N 個の駐観からなる 型 T の N 個の要素が保存されている配列の観: T@L0, T@L1, ..., T@LN-1 です。 ここで、L0 は配列の開始アドレスで、L に続くそれぞれの要素は直前の要素に T のサイズを加えたものと等しくなります。 すなわち、型 T の値を保存するのに必要なバイト数です。 次に宣言するデータ観 array_v はこの直感を正確に捕捉しています:
dataview array_v ( a:t@ype+ // covariant argument , addr(*beg*) , int(*size*) ) = // array_v | {l:addr} array_v_nil (a, l, 0) | {l:addr}{n:nat} array_v_cons (a, l, n+1) of (a @ l, array_v (a, l+sizeof(a), n)) // end of [array_v]
型 T, アドレス L, 整数 N が与えられた時、array_v(T, L, N) は型 T の N 個の要素を保存する L からはじまる配列の観です。 すぐに予想できることですが、 配列をアクセスしたり更新する関数テンプレートは次のインターフェイスで与えられます:
// fun{ a:t@ype } arrget{l:addr}{n,i:nat | i < n} (pf: !array_v (a, l, n) | p: ptr l, i: int i): a // end of [arrget] // end of [fun] // fun{ a:t@ype } arrset{l:addr}{n,i:nat | i < n} (pf: !array_v (a, l, n) | p: ptr l, i: int i, x: a): void // end of [arrset] // end of [fun] //
arrget と arrset を実装する前に、空でない配列の最初の要素にアクセスする関数テンプレートを実装する次のコードを紹介します:
fun{ a:t@ype } arrgetfst{l:addr}{n:pos} ( pf: !array_v (a, l, n) | p: ptr l ) : a = x where { prval array_v_cons (pf1, pf2) = pf // pf1: a @ l; pf2: array_v (a, l+sizeof(a), n-1) val x = !p prval () = pf := array_v_cons (pf1, pf2) } // end of [arrgetfst]
明らかに、関数テンプレート arrget は arrgetfst を用いて実装することができます:
implement {a}(*tmp*) arrget (pf | p, i) = if i > 0 then let prval array_v_cons (pf1, pf2) = pf val x = arrget (pf2 | ptr_succ<a> (p), i-1) prval () = pf := array_v_cons (pf1, pf2) in x end else arrgetfst (pf | p) // end of [if]
これは末尾再帰的な実装で時間的計算量は O(n) です。 けれども、配列の重要なメリットは O(1) の時間でアクセスと更新操作ができることにあります。 (実行時のコストなしに) 観の変更をサポートするような証明関数をコンストラクトする必要性に気づき、私は最初にそのような即時的な操作を実装することに注力しました。
明確に、型 T の N 個の要素を保存する L から開始する配列は2つの方法で考えることができます: 一つは I 個の要素が L から保管されていると考える方法で、もう一つは N-I 個の要素が L+I*sizeof(T) から保管されていると考える方法です。このとき I は N 以下の自然数です。 形式的には、この文は証明関数 array_v_split の型にエンコードできます:
prfun array_v_split {a:t@ype} {l:addr}{n,i:nat | i <= n} ( pfarr: array_v (a, l, n) ) : (array_v (a, l, i), array_v (a, l+i*sizeof(a), n-i))
上記の文のもう一方は証明関数 array_v_unsplit の型にエンコードできます:
prfun array_v_unsplit {a:t@ype} {l:addr}{n1,n2:nat} ( pf1arr: array_v (a, l, n1), pf2arr: array_v (a, l+n1*sizeof(a), n2) ) : array_v (a, l, n1+n2)
array_v_split と array_v_unsplit を使って、 O(1) 時間の arrget と arrset をたやすく実装することができます:
implement {a}(*tmp*) arrget{l}{n,i} (pf | p, i) = x where { prval (pf1, pf2) = array_v_split{a}{l}{n,i}(pf) prval array_v_cons (pf21, pf22) = pf2 val x = ptr_get1<a> (pf21 | ptr_add<a> (p, i)) prval pf2 = array_v_cons (pf21, pf22) prval () = pf := array_v_unsplit{a}{l}{i,n-i}(pf1, pf2) } (* end of [arrget] *) implement {a}(*tmp*) arrset{l}{n,i} (pf | p, i, x) = () where { prval (pf1, pf2) = array_v_split{a}{l}{n,i}(pf) prval array_v_cons (pf21, pf22) = pf2 val () = ptr_set1<a> (pf21 | ptr_add<a> (p, i), x) prval pf2 = array_v_cons (pf21, pf22) prval () = pf := array_v_unsplit{a}{l}{i,n-i}(pf1, pf2) } (* end of [arrset] *)
もちろん、証明関数 array_v_split と array_v_split はまだ実装されていません。 これは、観の変更に関するトピックを紹介するときに説明します。
型 T, アドレス L, 自然数 N が与えられた時、 観 array_v(T?, L, N) の証明は関数 malloc と free をそれぞれ使って獲得と解放をすることができます。 これについては別の章で詳細を解説します。 ここで、次のような配列を初期化する関数テンプレートの実装を見てみましょう:
typedef natLt (n:int) = [i:nat | i < n] int (i) fun{a:t@ype} array_ptr_tabulate {l:addr}{n:nat} ( pf: !array_v (a?,l,n) >> array_v (a,l,n) | p: ptr (l), n: int (n), f: natLt(n) -<cloref1> a ) : void = let fun loop{l:addr} {i:nat | i <= n} .<n-i>. ( pf: !array_v (a?,l,n-i) >> array_v (a,l,n-i) | p: ptr l, n: int n, f: natLt(n) -<cloref1> a, i: int i ) : void = if i < n then let prval array_v_cons (pf1, pf2) = pf val () = !p := f (i) val () = loop (pf2 | ptr_succ<a> (p), n, f, i+1) in pf := array_v_cons (pf1, pf2) end else let prval array_v_nil () = pf in pf := array_v_nil {a} () end // end of [if] // end of [loop] in loop (pf | p, n, f, 0) end // end of [array_ptr_tabulate]
自然数 n が与えられた時、型 natLt(n) は n より小さい全ての自然数です。 型 T が与えられた時、関数 array_ptr_tabulate<T> は未初期化配列へのポインタ、 その配列のサイズ、そして型 T の値に n より小さい自然数それぞれをマップする関数 f を取ります。 そしてこの関数は配列を f(0), f(1), ..., f(n-1) の値のシーケンスで初期化します。 言い方をかえると、初期化が終わるとこの配列は与えられた関数 f の表を保存していることになります。
型 T と自然数 N が与えられた時、@[T][N] は ATS のビルトイン型で 型 T の N 個連続した値を表わします。 したがって、与えられたアドレス L について駐観 @[T][N]@L は配列観 array_v(T, L, N) と等価です。 参照渡しの機能を使えば、以前示した関数 arrget と arrset に次のインターフェイスを割り当てることができます:
// fun{ a:t@ype } arrget {n,i:nat | i < n} (A: &(@[a][n]), i: int i): (a) // fun{ a:t@ype } arrset {n,i:nat | i < n} (A: &(@[a][n]), i: int i, x: a): void //
上記で紹介したコードの全体は オンライン から入手できます。