ATS の静的/動的ファイル

ATS のファイル名の拡張子である satsdats の最初の文字はそれぞれ、 単語 staticdynamic に由来しています。 例えば、foo.sats は静的ファイルの名前で、bar.dats は動的ファイルの名前です。 静的ファイルはしばしば SATS ファイルと呼ばれ、通常は関数, 値, データ型宣言, 型定義などのインターフェイス宣言を含んでいます。 SATS ファイルの主要な目的は、静的/動的にかかわらず別々のATSファイルでその中身を共用することにあります。

静的ファイルの典型的な使い方を知るために、シンプルな例を見てみましょう。 まずアッカーマン関数を実装することになったとします。 この関数は原始再帰ではない再帰として有名です。 acker.sats という名前の静的ファイルに、次の関数インターフェイスを宣言します:

fun acker (m: int, n: int): int

静的ファイル内で関数や値のインターフェイス宣言をする際には、 extern キーワード を使わないことに注意してください。 acker.dats という名前の動的ファイルに、次ような実装を書きます:

staload "acker.sats" implement acker (m, n) = if m > 0 then if n > 0 then acker (m-1, acker (m, n-1)) else acker (m-1, 1) else n+1 // end of [acker]

キーワード staload は指定したファイルを型検査中に静的にロードするよう、ATS の型検査器に指示します。 本質的にファイルの静的なロードは、 後続のコードがアクセスできるようにファイルの中身を名前空間に配置することです。 注目すべきなのは、静的なロードは単純なファイルの埋め込みとは異なるということです。 ATS では後者もまたサポートしています。その機能は別の章で解説します。

acker 関数宣言に対して次のような実装をすることもできます:

staload ACKER = "acker.sats" implement $ACKER.acker (m, n) = acker (m, n) where { fun acker (m: int, n:int): int = if m > 0 then if n > 0 then acker (m-1, acker (m, n-1)) else acker (m-1, 1) else n+1 } // end of [$ACKER.acker]

この場合、ACKER という名前の名前空間が acker.sats ファイルの中身を保持しています。 また接頭辞 $ACKER. (ドル記号の後にACKERを、その後にドット記号です) を acker.sats で宣言されている関数, 値, データ型, コンストラクタ, 型宣言 などの名前に付記する必要があります。 多数の静的ファイルがロードされた時、それらのファイルの持つ名前空間に名前を割り当てるのは、 しばしば良い習慣です。 それぞれの要素が宣言されている元のソースコードをすぐに見つけ出せるからです。

別のファイル test_acker.dats に次のコードを書いてみましょう:

// #include "share/atspre_staload.hats" // staload "acker.sats" dynload "acker.dats" implement main0 () = () where { // // acker (3, 3) should return 61 // val () = assertloc (acker (3, 3) = 61) } // end of [main0]

キーワード dynloadacker.dats ファイルに関連する初期化関数呼び出しを生成するよう、ATS コンパイラに指示します。 これは必須で、さもないとリンク時にエラーが発生してしまいます。 通常、動的ファイルに関連するこの初期化関数は、そのファイルの中で値が実装されている時のみ必要になります。 この例では acker.dats の中には関数の実装しかありません。 もし次の行を acker.dats の中のどこかに書けば:

#define ATS_DYNLOADFLAG 0 // no need for dynloading at run-time

test_acker.dats 中の dynload キーワード行はもはや不要です。 assertloc 関数は、その引数を評価してブール値 true になるか実行時に検証します。 この例では引数は false に評価されるので、関数呼び出しは中断されてファイル名 (この例では test_acker.dats) とそのファイルで呼び出したソースコードの位置を含むメッセージが表示されます。 もし少し混乱してしまったら false に対して assertloc を呼び出してみてください。 何が起きるのか明確になるでしょう。

次のコマンドラインを実行すれば、 2つのファイル acker.datstest_acker.dats を簡単にコンパイルできます:


atscc -o test_acker acker.dats test_acker.dats

現在のワーキングディレクトリに実行可能ファイル test_acker が生成されるはずです。 次のように分割コンパイルをすることもできます:


atscc -c acker.dats
atscc -c test_acker.dats
atscc -o test_acker acker_dats.o test_acker_dats.o

この分割コンパイルのスタイルは make ユーティリティから呼び出す際に特に有用です。

望むなら acker.satsacker.dats を次のような1つのファイルにまとめることも可能です:

extern fun acker (m: int, m: int): int implement acker (m, n) = if m > 0 then if n > 0 then acker (m-1, acker (m, n-1)) else acker (m-1, 1) else n+1 // end of [acker]

acker3.dats の名前で上記のファイルを作ったとしましょう。 するとテストコードは次のように書けます:

// #include "share/atspre_staload.hats" // staload "acker3.dats" dynload "acker3.dats" implement main0 () = () where { // // acker (3, 3) should return 61 // val () = assertloc (acker (3, 3) = 61) } // end of [main0]

ATS の動的ファイルを静的ロードすることが正常であることに注意してください。 実際 ATS の静的ファイルは、関数や値の実装を含まないATSの動的ファイルの単なる特殊形です。