Prev Up Next
Go backward to 2.7.3 Parsing Terms in the Extended Signature of a Module
Go up to 2.7 Parsing, Bubbles and Meta-Parsing
Go forward to 2.7.5 Default Precedence and Gathering

2.7.4 Precedence and Gathering

BINARY-NAT contains a rich set of notational models for the specification of operators, and illustrates clearly the idea of an extended signature for a module. Nevertheless, the operators in this module will generate, in most cases, complex and subtle inconsistencies, ambiguities and unintuitive results, as shown in the following examples. The concepts of precedence and gathering provide a flexible way of avoiding these ambiguities without having to write unnecessary parentheses.

These syntactic problems (grammatical scope, precedence and syntactic order of evaluation of operators) are solved in OBJ3 [27] and in Maude by means of precedence and gathering patterns.

In Maude, each operator has associated to it a precedence value and a gathering pattern. They can be specified by the user by means of the precedence (abbreviated prec) and gather attributes. If not specified, Maude assigns default values as explained in Section 2.7.5.

A precedence value is an integer greater than or equal to 0, which may be understood as an output value associated to terms having the corresponding operator as their top symbol.

On the other hand, gathering patterns are associated to the arguments of an operator. Gathering patterns are given as nonempty sequences of the following possible pattern:

We can illustrate the notions of precedence and gathering by considering a variant BINARY-NAT-PREC of the module BINARY-NAT whose only difference is that we have now specified precedence values and gathering patterns for the operators as follows. 

  op __ : Bits Bits -> Bits [assoc prec 1 gather (e E)] .
  op |_| : Bits -> MachineInt .                      *** Length
  op not_ : Bits -> Bits [prec 2 gather (E)] .
  op normalize : Bits -> Bits .
  op _+_  : Bits Bits -> Bits [assoc comm prec 5 gather (E e)] .
  op _*_  : Bits Bits -> Bits [assoc comm prec 4 gather (E e)] .
  op _^_  : Bits Bits -> Bits [prec 3 gather (e E)] .
  op _>_  : Bits Bits -> Bool [prec 6 gather (E E)] .
  op _?_:_ : Bool Bits Bits -> Bits [prec 7 gather (& E E)] .

Constants have precedence 0. In our example, this rule is applied to 0, 1 and nil. The precedence value of an operator is associated to the terms generated by this operator. In our example, the term 1 has precedence 0, the term 1 0 1 has precedence 1, the term 1 0 + 1 has precedence 5, and 1 0 * 1 has precedence 4.

To illustrate the behavior of the gathering patterns, let us focus on the declaration of the _*_ operator. From it we can infer the following consequences:

The simultaneous use of precedence and gathering attributes allows specifying any kind of precedence relations between operators and different types of syntactic order of evaluation.

To show in practice how this strategy works, we analyze some of the problems detected in BINARY-NAT using the signature of BINARY-NAT-PREC.

The first problem appeared with the term 1 0 + 1 0. Without any information about precedence values and gathering patterns, we can think of two different analyses for this term: (1 0) + (1 0) and  1 (0 + 1) 0. This ambiguity can be solved by the use of different precedence values for the operators involved, namely, __ and _+_. In the module BINARY-NAT-PREC these operators have been defined as follows: 

  op __ : Bits Bits -> Bits [assoc id: nil prec 1 gather (e E)] .
  op _+_ : Bits Bits -> Bits [assoc comm prec 5 gather (E e)] .

Let us consider the two previous analyses proposed for the term  1 0 + 1 0:

Of course, using parentheses is always a way of resolving ambiguities. In fact, it is worth noting that the parentheses operator automatically included in the extended signature of a module has precedence 0. Therefore, the term 1 (0 + 1) 0 is grammatically correct in BINARY-NAT-PREC. 

  Maude> red 1 0 + 1 0 .
  result Bits: 1 0 0

  Maude> red 1 (0 + 1) 0 .
  result Bits: 1 1 0

Another subtle problem in the BINARY-NAT module was the different behaviors of the terms (1 0) + (1 0) * (1 0) and (1 0) * (1 0) + (1 0). In that module, both operators _+_ and _*_ had no precedence attribute explicitly given. As both had the assoc attribute, the gathering patterns generated by default for both of them was (e E), so the operators were associated from right to left.

In BINARY-NAT-PREC these two operators have different precedence values, and the gathering patterns have also been specified: 

  op _+_ : Bits Bits -> Bits [assoc comm prec 5 gather (E e)] .
  op _*_ : Bits Bits -> Bits [assoc comm prec 4 gather (E e)] .
  op _^_  : Bits Bits -> Bits [prec 3 gather (e E)] .

The main consequence of this definition is that, as already explained, an addition cannot be an argument of a multiplication unless it is enclosed in parentheses. Thus, we have the following reductions. 

  Maude> red (1 0) + (1 0) * (1 0) .
  result Bits: 1 1 0

  Maude> red (1 0) * (1 0) + (1 0) .
  result Bits: 1 1 0

The following examples illustrate how the precedence and gathering model of the operators of BINARY-NAT-PREC solves the problems of precedence and order of evaluation of operators.

Prev Up Next