仕様の読み込み

テキストファイルとして記述した仕様を CafeOBJ に読み込ませるには、in コマンドを使用する。in コマンドの構文は、次の通りである。

in <filename>

<filename> には、CafeOBJ に読み込ませたいファイル名を指定する。拡張子 .mod は省略してよい。

先ほど、 simple-nat.mod と名前を付けて保存した自然数の仕様を読み込ませてみよう。次のように入力すると、CafeOBJ は simple-nat.mod を読み込む。

CafeOBJ> in simple-nat
processing input : simple-nat.mod
-- defining module! SIMPLE-NAT..._* done.
-- defining module! NAT+.._..* done.
CafeOBJ> 

CafeOBJ は進捗状況を表示しながらファイルを読み込み、読み込みが終了すると、再びプロンプトを表示する。

CafeOBJ は仕様に文法エラーが含まれるとき、文法エラーの位置をファイルの先頭からの文字数で表示する。この表示はエラーの位置を探すには少し不親切であるが、先頭からの文字数でカーソルを移動させる機能のあるエディタ (Emacs など) を用いるか、tail コマンドを使えば表示できる。

例えば、sample.mod を読み込んだとき、1354 文字目にエラーがあることが分かったならば、シェルプロンプトから次のようにタイプする:

% tail -c 1354 sample.mod | head -10

sample.mod の 1354文字目から 10行表示されるはずである。

同じファイルを再度読み込ませると、CafeOBJ は次のように警告を表示する。

CafeOBJ> in simple-nat
processing input : simple-nat.mod
-- defining module! SIMPLE-NAT
[Warning]: redefining module SIMPLE-NAT ..._* done.
-- defining module! NAT+
[Warning]: redefining module NAT+ .._..* done.
CafeOBJ> 

既に定義済みのモジュールが再定義されたことを示す警告であり、この場合は無視してよい。

eof コマンド

CafeOBJ はファイルの読み込み中に、eof コマンドに出会うと、その位置で読み込みを停止する。例えば、次のように使用する:

mod! SIMPLE-NAT {
  [ Nat ]
  op 0 : -> Nat
  op s : Nat -> Nat
}

eof

mod! NAT+ {
  pr(SIMPLE-NAT)
  op _+_ : Nat Nat -> Nat
  eq 0 + M:Nat = M .
  eq s (N:Nat) + M:Nat = s (N + M) .
}

eof は仕様のデバッグの際に有用である。

ファイルの一覧、ディレクトリの移動

CafeOBJ では、Unix コマンドと同様のコマンドが存在する。以下では、そのようなコマンドの構文を紹介する。

ファイルの一覧

ls <path>

カレントディレクトリの変更

cd <path>

カレントディレクトリの表示

pwd

使い方は Unix の同名のコマンドと同じであるので、説明は割愛する。

[Next] コメント

Original Copyright © Takahiro Seino, all rights reserved.