A signature consists of sorts and operators. The set of well-formed terms is defined from a given signature (and a set of sorted variables). The following expressions are well-formed terms of `NAT+`

:

`0`

`s(s(0))`

`s(s(s(0))) + s(s(s(s(0))))`

The following expressions are not well-formed terms of `NAT+`

(Note that `NAT+`

does not include `*`

):

`s(s(0)) 0`

`s(s(s(0))) * s(s(0))`

The `parse`

command shows the parse tree of a well-formed term as follows:

`parse `

*<term>*` .`

Example:

Let us show how to parse Term `s(s(0)) + s(s(s(0)))`

in Module `NAT+`

.

First, select Module `NAT+`

by using the `select`

command as follows:

CafeOBJ>select NAT+NAT+>

The prompt has been changed into the current selected module. Parse `s(s(0)) + s(s(s(0)))`

by using the `parse`

command as follows:

NAT+>parse s(s(0)) + s(s(s(0))) .(s(s(0)) + s(s(s(0)))) : Nat NAT+>

As the result of the `parse`

command, it is shown that the sort of `s(s(0)) + s(s(s(0)))`

is `Nat`

.

When an expression has more than one possible parse trees, it is called an ambiguous term. For example, Expression `s(0) + s(s(0)) + s(s(s(0)))`

is ambiguous. The `parse`

command returns the following warning for this input as follows:

NAT+>parse s(0) + s(s(0)) + s(s(s(0))) .[Warning]: Ambiguous term: * Please select a term from the followings: [1] _+_ : Nat Nat -> Nat ---------------------((s(0) + s(s(0))) + s(s(s(0)))) [2] _+_ : Nat Nat -> Nat ---------------------(s(0) + (s(s(0)) + s(s(s(0))))) * Please input your choice (a number from 1 to 2, default is 1)?1Taking the first as correct. ((s(0) + s(s(0))) + s(s(s(0)))) : Nat NAT+>

Because this expression has different parse trees: (1 + 2) + 3 and 1 + (2 + 3), CafeOBJ system asks the user which is correct. In the above example, the first candidate has been chosen by inputting `1`

. It is not recommended that ambiguous terms are possible. Ambiguous terms can be avoided by using brackets for example.

To show a parse tree, set the `verbose`

switch on by the `set`

command as follows:

NAT+>set verbose onNAT+>

Then, the `parse`

command shows a parse tree of an input term as follows:

NAT+>parse (s(0) + s(s(0))) + s(s(s(0))) .((s(0) + s(s(0))) + s(s(s(0)))) : Nat _+_:Nat / \ _+_:Nat s:Nat / \ | s:Nat s:Nat s:Nat | | | 0:Nat s:Nat s:Nat | | 0:Nat 0:Nat NAT+>

To cancel module selection, type as follows:

NAT+>select .CafeOBJ>

Original Copyright © Takahiro Seino, all rights reserved.