To read your specification (`.mod`

file), use the `in`

command as follows:

`in`

`<filename>`

The extension `.mod`

of `<filename>` can be omitted.

The following is an example of reading specifications: reading the specification of natural numbers which is saved as `simple-nat.mod`

:

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

CafeOBJ reads the input file and shows its progress, and then the prompt is shown when the reading finished.

When an input CafeOBJ specification includes a syntax error, CafeOBJ shows the place of the syntax error by the number of characters from the head of the input file. You can find the error place by Emacs, for example, or using the Shell command `tail`

.

For example, assume 1354-th character is the place of error of `sample.mod`

. Type as follow:

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

Ten lines from 1354-th character of `sample.mod`

should be shown.

When reading the same file again, CafeOBJ show a warning as follows:

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>

The warning means that the specification is redefined.

`eof`

CafeOBJ system stops reading a file when the `eof`

command inputted.

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) . }

When reading the above file, CafeOBJ reads only `SIMPLE-NAT`

and ignores all descriptions after the `eof`

command (`NAT+`

). The `eof`

command is useful for debugging.

CafeOBJ system supports Unix-like commands like `ls`

, `cd`

, etc.

List

`ls`

`<path>`

Change directory

`cd`

`<path>`

Print working directory

`pwd`

Original Copyright © Takahiro Seino, all rights reserved.