ATSプログラミングチュートリアル:
Prev		Next

Chapter 24. 線形型のリスト

ATS における線形型のリストは線形リストとも呼ばれ、本質的にはC言語における片方向リストに対応します。次の線形データ型宣言は、線形リストを表わす線形型 list_vt を導入しています:

//
datavtype
list_vt(a:vt@ype, int) =
| list_vt_nil(a, 0) of ()
| {n:nat}
  list_vt_cons(a, n+1) of (a, list_vt(a, n))
//

キーワード datavtype は dataviewtype とも書けることに注意してください。 (おそらく線形の) 型 T と整数 N が与えられたとき、型 list_vt(T,N) は型 T の要素を持つ長さ N のリストを表わします。線形リストに対する様々な関数のインターフェイスが SATS ファイル prelude/SATS/list_vt.sats にあります。このファイルは atsopt によって自動的にロードされます。

次の関数 list_vt_length は、読み込みのみ許された線形リストをあつかう典型的な方法を示しています:

//
fun
{a:vt@ype}
list_vt_length
  (xs: !list_vt(a, n)): int(n) =
(
case+ xs of
| list_vt_nil() => 0
| list_vt_cons(x, xs2) => 1 + list_vt_length<a> (xs2)
)
//

xs が list_vt_nil() にパターンマッチするとき、xs の型は list_vt(a, 0) です。 xs が list_vt_cons(x, xs2) にパターンマッチするとき、xs の型はなんらかの自然数 N について list_vt(a, N+1) で、x と xs2 の型はそれぞれ a と list_vt(a, N) です。 x と xs2 は両方とも値を表わす名前で、それらの型は不変でなければならないことに注意してください。

次の関数 list_vt_foreach は、線形リストに保管された要素を変更する典型的な方法を示しています:

//
fun
{a:vt@ype}
list_vt_foreach
(
  xs: !list_vt(a, n)
, fwork: (&(a) >> _) -<cloref1> void
) : void =
(
case+ xs of
| list_vt_nil() => ()
| @list_vt_cons(x, xs2) => (fwork(x); list_vt_foreach<a> (xs2, fwork); fold@(xs))
)
//

xs が @list_vt_cons(x,xs2) にパターンマッチするとき、xs の型はなんらかの自然数 N について list_vt(a, N+1) で、x と xs2 の型はそれぞれ a と list_vt(a, N) です。 x と xs2 の両方が (左辺値をなす) 値であることに注意してください。パターン @list_vt_cons(x,xs2) ではじまる関数本体の最初では、xs の型は list_vt_cons_unfold(L0, L1, L2) であると推測されます。このとき、その型は list_vt_cons を呼び出してリストノードを表わす観型で、そのノードは L0 に配置されます。さらに list_vt_cons の2つの引数は L1 と L2 に配置されていて、L1 と L2 に関連した駐観の証明が現在有効な証明として保管されています。したがって、左辺値として x と xs2 はそれぞれアドレス L1 と L2 を持ち、L1 と L2 に関連した証明である観はそれぞれ a@L1 と list_vt_cons(a, N)@L2 です。関数適用 fold@(xs) は、L1 と L2 に関連した証明を消費して、xs を型 list_vt(a, N+1) の値に変化させます。 xs の型は、割り当てられていた元と fold が終わった後で異なる可能性があることに注意してください: 次のコードはそのような例です:

//
fun
{a:vt@ype}
list_vt_append
  {m,n:nat}
(
  xs: list_vt(a, m), ys: list_vt(a, n)
) : list_vt(a, m+n) = let
//
fun
loop{m:nat}
(
  xs: &list_vt(a, m) >> list_vt(a, m+n), ys: list_vt(a, n)
) : void =
(
case+ xs of
| ~list_vt_nil() => (xs := ys)
| @list_vt_cons(x, xs2) => (loop(xs2, ys); fold@(xs))
)
//
in
  case+ xs of
  | ~list_vt_nil () => ys
  | @list_vt_cons (x, xs2) => (loop(xs2, ys); fold@(xs); xs)
end // end of [list_vt_append]
//

パターンの前にあるシンボル ~ は以前説明しました。 list_vt_append の実装は、C言語における2つの片方向リストの連結の標準的な実装に正確に一致しています: 2つのリストとして xs と ys を与えます; もし xs が空であれば ys が返ります; そうでなければ、xs の最後のノードとして配置され、ys はその次として予約されたノードの要素に格納されます。

次の関数 list_vt_free は、与えられた非線形の要素を含む線形リストを解放します:

//
fun
{a:vt@ype}
list_vt_free
  {n:nat}
(
  xs: list_vt(a?, n)
) : void =
(
case+ xs of
| ~list_vt_nil() => ()
| ~list_vt_cons(x, xs2) => list_vt_free<a> (xs2)
)
//

xs がパターン ~list_vt_nil() にマッチするとき、xs の型は、その xs の型が変更され、xs がその後では使用できないことを示しています。 xs がパターン ~list_vt_cons(x,xs2) にマッチするとき、xs の型は、その xs の型が変更され、やはり xs がその後では使用できないことを示しています。後者の場合、リスト xs の head と tail を表わす2つの値は、それぞれ x と xs2 として参照できます。 xs として参照されるリストの最初のリストノードのメモリを解放していることがわかります。

この章で紹介したコード全体とテストコードはオンラインから入手できます。

Prev	Home	Next
遅延ストリーム	Up	高度なチュートリアル