Parse

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.

Ambiguous terms

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)? 1
Taking 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.

Verbose mode

To show a parse tree, set the verbose switch on by the set command as follows:

NAT+> set verbose on
NAT+>

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+> 

Tips

To cancel module selection, type as follows:

NAT+> select .
CafeOBJ> 

[Next] Reduce

Original Copyright © Takahiro Seino, all rights reserved.