Reading specifications

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-nat
processing 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.

Unix-like commands

CafeOBJ system supports Unix-like commands like ls, cd, etc.

List

ls <path>

Change directory

cd <path>

Print working directory

pwd

[Next] Comments

Original Copyright © Takahiro Seino, all rights reserved.