absvtype
stkarray_vtype (a:vt@ype+, m:int, n:int) = ptr
それから次のようにいくつか短縮名を導入します:
stadef stkarray = stkarray_vtype vtypedef stkarray (a:vt0p) = [m,n:int] stkarray_vtype (a, m, n)型 T と整数 M, N が与えられたとき、型 [stkarray(T, M, N)] は次のような配列を用いたスタックを表わします; (1) スタックに格納された要素が型 T であり、 (2) スタックの容量が M であり、 (3) 現在のスタックのサイズが N である。 M >= N と N >= 0 が維持されていて、この特性は次の証明関数 [lemma_stkarray_param] の型にエンコードされていることは明確です:
praxi lemma_stkarray_param {a:vt0p}{m,n:int} (!stkarray (INV(a), m, n)): [m >= n; n >= 0] void // end of [lemma_stkarray_param]
いつものように、(線形の) stkarray 値を生成/破棄するために関数が必要になります:
// fun{a:vt0p} stkarray_make_cap {m:int} (cap: size_t(m)):<!wrt> stkarray (a, m, 0) // fun stkarray_free{a:vt0p}{m:int} (stkarray (a, m, 0)):<!wrt> void //サイズ M が与えられたとき、[stkarray_make_cap] は容量 M の空スタックを生成します。 スタックが解放された後にスタック内の線形な要素がリークしてしまうので、[stkarray_free] の型は要素を持たないスタックにのみこの関数を適用できることを示しています。
要素を挿入するために、次の関数を作ります:
fun{a:vt0p} stkarray_insert {m,n:int | m > n} ( stk: !stkarray (a, m, n) >> stkarray (a, m, n+1), x0: a ) :<!wrt> void // endfunスタックの現在サイズがその容量よりも厳密に小さいときのみ、[stkarray_insert] をスタックに対して呼び出すことができることに注意してください。 [stkarray_insert] の型は、1つ要素を挿入した後ではスタック引数のサイズが 1 増えることを示しています。
要素を取り出すために、次の関数を作ります:
fun{a:vt0p} stkarray_takeout {m,n:int | n > 0} (stk: !stkarray (a, m, n) >> stkarray (a, m, n-1)):<!wrt> (a) // end of [stkarray_takeout][stkarray_takeout] はスタックの現在サイズが正の場合のみ呼び出すことができることに注意してください。 [stkarray_takeout] の型は、要素がスタックから取り出された後ではスタックのサイズが 1 減少することを示しています。
typedef
struct {
atstype_ptr stkarray_beg ; // the beg pointer
atstype_ptr stkarray_end ; // the end pointer
atstype_ref stkarray_cur ; // the current pointer
} atslib_stkarray_struct ;
ポインタ [stkarray_beg] と [stkarray_end] は元になる配列の開始位置と終了位置を指しています。
ポインタ [stkarray_cur] は現在のスタックの一番上を指しています。
元になる配列の開始位置が表現されるスタックの底であることに注意してください。
ポインタ [stkarray_cur] にアクセスするために次の2つの関数を導入しましょう:
extern fun stkarray_get_ptrcur{a:vt0p} {m,n:int} (stk: !stkarray (INV(a), m, n)):<> ptr = "mac#atslib_stkarray_get_ptrcur" extern fun stkarray_set_ptrcur{a:vt0p} {m,n:int} (stk: !stkarray (INV(a), m, n), ptr):<!wrt> void = "mac#atslib_stkarray_set_ptrcur"予想できることですが、これら2つの関数はC言語で直接実装されています。 [stkarray_insert] の次の実装は、これら2つの関数および安全でない関数 [ptr0_set] を使用します:
implement{a} stkarray_insert {m,n} (stk, x0) = let // val p_cur = stkarray_get_ptrcur (stk) val ((*void*)) = $UN.ptr0_set<a> (p_cur, x0) val ((*void*)) = stkarray_set_ptrcur (stk, ptr_succ<a> (p_cur)) // prval () = __assert (stk) where { extern praxi __assert (!stkarray (a, m, n) >> stkarray (a, m, n+1)): void } (* end of [prval] *) // in // nothing end // end of [stkarray_insert][ptr0_set] は、メモリ位置に関連した (駐観 (at-view) の) 証明なしに、(第2引数の) 値を (第1引数の) 与えらえたメモリ位置に書き込むことに注意してください。 別の言い方をすると、[ptr0_set] はC言語が行なうのと正確に同じ方法で、メモリ更新を実行します。 また型検査を通る実装を可能にするために、証明関数 [__assert] が導入されていることに注意してください。 キーワード [praxi] は導入された証明関数が表明として取り扱われるべきで、要求された実装を持たないことを意味しています。
[stkarray_takeout] の次の実装は、メモリ位置に関連した (駐観の) 証明なしに与えられたポインタから読み出す、[ptr0_get] を使用しています。 また [stkarray_insert] の実装と同じく、型検査を通る [stkarray_takeout] の実装を作るために、証明関数は表明として扱われています。
implement{a} stkarray_takeout {m,n} (stk) = x0 where { // val p_cur = stkarray_get_ptrcur (stk) val p1_cur = ptr_pred<a> (p_cur) val x0 = $UN.ptr0_get<a> (p1_cur) val () = stkarray_set_ptrcur (stk, p1_cur) // prval () = __assert (stk) where { extern praxi __assert (!stkarray (a, m, n) >> stkarray (a, m, n-1)): void } (* end of [prval] *) // } // end of [stkarray_takeout][stkarray_get_ptrcur] と [stkarray_set_ptrcur] を実装するC言語コードは次のようになります:
ATSinline()
atstype_ptr
atslib_stkarray_get_ptrcur
(atstype_ptr p)
{
return ((atslib_stkarray_struct*)p)->stkarray_cur ;
} // end of [atslib_stkarray_get_ptrcur]
ATSinline()
atsvoid_t0ype
atslib_stkarray_set_ptrcur
(atstype_ptr p, atstype_ptr p2)
{
((atslib_stkarray_struct*)p)->stkarray_cur = p2 ; return ;
} // end of [atslib_stkarray_set_ptrcur]
[stkarray_get_ptrcur] と [stkarray_set_ptrcur] を表わすC言語の名前は、それぞれ
[atslib_stkarray_get_ptrcur] と [atslib_stkarray_set_ptrcur] が選ばれます。
配列を用いたスタック実装についての詳細は stkarray.sats , stkarray.dats , stkarray.cats から入手できます。
extern fun{a:vt0p} stkarray_insert_opt (stk: !stkarray (INV(a)) >> _, x0: a):<!wrt> Option_vt(a) implement{a} stkarray_insert_opt (stk, x0) = let // val isnot = stkarray_isnot_full (stk) // in // if isnot then let val () = stkarray_insert (stk, x0) in None_vt() end else Some_vt{a}(x0) // end // end of [stkarray_insert_opt]同様に、空であるスタックから要素を取り出そうとするかもしれません。 次の関数 [stkarray_takeout_opt] は、与えられたスタックから実際に要素が取り出されたかどうか呼び出し元が判別できるように、optional 値を返します:
extern fun{a:vt0p} stkarray_takeout_opt (stk: !stkarray (INV(a)) >> _):<!wrt> Option_vt(a) implement{a} stkarray_takeout_opt (stk) = let // val isnot = stkarray_isnot_nil (stk) // in // if isnot then let val x0 = stkarray_takeout (stk) in Some_vt{a}(x0) end else None_vt((*void*)) // end // end of [stkarray_takeout_opt]配列を用いたスタック実装を使ったサンプルコードは postfix_eval.dats から入手できます。 このサンプルコードは逆ポーランド記法 (postfix-notation) で書かれた算術式の評価器です。