今までは、駐観と駐観の上に構築された観にもっぱら注目して観の表現を見てきました。 駐観が実際にもっとも広く使われる観の形であり、また ATS がサポートした観の最初の形であることが、その大きな理由です。 けれども、抽象的な観の他の形を ATS に導入することもできます。 観を駐観 (もしくは観の他の形) を元にして定義できる場合においてさえ、(観変化する証明関数をともなう) 抽象観として導入したいと思うかもしれません。 しばしばプログラマが本当に必要とすることは、抽象的に定義された観とそれらを操作する証明関数が実際に意味をなすかどうか、概念的に 理解することです。 これは関数が計算可能かどうか根拠を示すことに少し似ています: 例え、計算可能であることを立証するためにチューリングマシンに関数を実際にエンコードするとしても、まれにその必要があります。 私見ですが、抽象観と抽象的な観型 (viewtype) の適切な使い方を学ぶことは、実際にリソースに関連するプログラミングの問題に取り組むために、効果的に線形型を使うのに必要なステップです。
物理世界のオブジェクトが線形であることははっきりしています: それらは無から生成することはできませんし、単に消し去って無へと帰すこともできません。 従って、物理オブジェクトを表現する値に線形型を割り当てることは極めて自然です。 継承をサポートするビルトインの仕組みを含まないようなある種のオブジェクトを表わす線形値を表わすのに、ここでは 単純な線形オブジェクト (simple linear object) という名前を使います。
単純な線形オブジェクトの具体的な例を見てみましょう。 次のコードは、タイマー (つまりストップウォッチです) のインターフェイスを表わしています:
// absvtype timer_vtype vtypedef timer = timer_vtype // fun timer_new (): timer fun timer_free (x: timer): void fun timer_start (x: !timer): void fun timer_finish (x: !timer): void fun timer_pause (x: !timer): void fun timer_resume (x: !timer): void fun timer_get_ntick (x: !timer): uint fun timer_reset (x: !timer): void //
// typedef timer_struct = @{ started= bool // the timer has started , running= bool // the timer is running // the tick number recorded when the timer , ntick_beg= uint // was turned on last time , ntick_acc= uint // the number of accumulated ticks } (* end of [timer_struct] *) //
タイマーに関する各種の関数をこれですぐに実装できます。 はじめにタイマーの生成と解放をするコードを見てみましょう:
implement timer_new () = let // val timer = TIMER (_) val TIMER (x) = timer // val () = x.started := false val () = x.running := false val () = x.ntick_beg := 0u val () = x.ntick_acc := 0u // prval () = fold@ (timer) // in timer end // end of [timer_new] implement timer_free (timer) = let val ~TIMER _ = timer in (*nothing*) end // end of [timer_free]
タイマーを開始する関数は次のように実装できます:
implement timer_start (timer) = let val+@TIMER(x) = timer val () = x.started := true val () = x.running := true val () = x.ntick_beg := the_current_tick_get () val () = x.ntick_acc := 0u prval () = fold@ (timer) in // nothing end // end of [timer_start]
タイマーは停止したり休止したりすることができます。 タイマーを停止させる関数は次のように実装できます:
implement timer_finish (timer) = let val+@TIMER(x) = timer val () = x.started := false val () = if x.running then { val () = x.running := false val () = x.ntick_acc := x.ntick_acc + the_current_tick_get () - x.ntick_beg } (* end of [val] *) prval () = fold@ (timer) in // nothing end // end of [timer_finish]
タイマーは休止した後に再開することができます。 次のコードはタイマーの休止と再開の関数を実装しています:
implement timer_pause (timer) = let val+@TIMER(x) = timer val () = if x.running then { val () = x.running := false val () = x.ntick_acc := x.ntick_acc + the_current_tick_get () - x.ntick_beg } (* end of [val] *) prval () = fold@ (timer) in // nothing end // end of [timer_pause] implement timer_resume (timer) = let val+@TIMER(x) = timer val () = if x.started && ~(x.running) then { val () = x.running := true val () = x.ntick_beg := the_current_tick_get () } (* end of [if] *) // end of [val] prval () = fold@ (timer) in // nothing end // end of [timer_resume]
関数 timer_reset を呼び出すことでタイマーをリセットすることもまた可能です:
implement timer_reset (timer) = let val+@TIMER(x) = timer val () = x.started := false val () = x.running := false val () = x.ntick_beg := 0u val () = x.ntick_acc := 0u prval () = fold@ (timer) in // nothing end // end of [timer_reset]
関数 timer_get_ntick を呼び出すことで、 タイマーにたまった時間を読み出すことができます:
implement timer_get_ntick (timer) = let val+@TIMER(x) = timer var ntick: uint = x.ntick_acc val () = if x.running then ( ntick := ntick + the_current_tick_get () - x.ntick_beg ) (* end of [if] *) // end of [val] prval () = fold@ (timer) in ntick end // end of [timer_get_ntick]
the_current_tick_get を実装するわかりやすいアプローチは、関数 clock_gettime を直接用いることでしょう:
local staload "libc/SATS/time.sats" in (* in-of-local *) implement the_current_tick_get () = let var tv: timespec // uninitialized val err = clock_gettime (CLOCK_REALTIME, tv) val ((*void*)) = assertloc (err >= 0) prval ((*void*)) = opt_unsome{timespec}(tv) in $UNSAFE.cast2uint(tv.tv_sec) end // end of [the_current_tick_get] end // end of [local]
この章で紹介したコード全体とテストコードは オンライン から入手できます。