2.7.5 Default Precedence and Gathering

This section sketches the rules used by Maude to generate the default precedence values and gathering patterns for operators; they are entirely similar to those used by OBJ3 [27]. These values will be associated to those operators for which the user does not specify this information as part of the operator declaration.

The rules for the assignment of default precedence values are:

• Prefix operators always have precedence 0, regardless of user settings. This rule is applied, for example, to the operator normalize in the module BINARY-NAT.
• Outfix operators have precedence 0. This is the case, for example, for the operator |_|.
• Unary mixfix operators have precedence 15. In the module BINARY-NAT this rule is applied to the operator not_.
• Multi-ary mixfix operators (with arity greater than 1) have precedence 41. In BINARY-NAT this rule is applied to the operators __, _+_, _*_, __, _>_, and _?_:_.

The rules for the generation of the default gathering patterns are:

• All arguments of prefix operators have a gathering pattern &, regardless of the user specification.
• For operators with mixfix notation, the gathering patterns are by default & for each argument. There are three exceptions to this rule (with exceptions 2 and 3 mutually exclusive, and with either of them overruling exception 1):

  • Exception 1: The gathering pattern of an argument will be E if the argument position (the corresponding underscore `_' in the operator name) is:
    1. the leftmost token in the operator name, or
    2. the rightmost token in the operator name, or
    3. it is adjacent to another underscore in the operator name.

    In BINARY-NAT, this exception changes to E the gathering pattern of the unique argument of the operator not_, and of the first and last arguments of the operators _?_:_, _-_, __, __, _<_ and _<=_.

  • Exception 2: An operator will have gathering pattern (e E) if:
    1. starts with an underscore `_', and
    2. ends with an underscore `_', and
    3. has precedence (if supplied by the user) greater than 0, and
    4. has the assoc attribute.

    These conditions are fulfilled by the operators _+_, _*_ and __ of the BINARY-NAT module.

  • Exception 3: If an operator
    1. starts with an underscore `_', and
    2. ends with an underscore `_', and
    3. has precedence (if supplied by the user) greater than 0, and
    4. has the first and last arguments and its coarity in the same sort connected component, and
    5. does not have the assoc attribute.

    then:

    1. the first argument's gathering pattern will change to e if and only if the subsort relations allow it to right associate but not left-associate, and
    2. the last argument's gathering pattern will change to e if and only if the subsort relations allow it to left associate but not right-associate.

    This exception will apply, for example, to the operator _;_ in the following module.

      fmod LIST is
        including MACHINE-INT .
        sorts Elt List .
        subsort MachineInt < Elt < List .
        op _;_ : Elt List -> List .
      endfm
    

    According to the general rule, the gathering pattern should be gather (& &). Since exception 1 may be applied to the two arguments of the operator, this exception would change the gathering pattern to gather (E E). But exception 3 prevails over exception 1 and should be applied to the first argument, so that the real gathering pattern of this operator is: gather (e E).

To illustrate these rules, we show below the default precedence and gathering patterns generated by Maude for the module BINARY-NAT presented in Section 2.7.2.

  op 0 : -> Bit .
  op 1 : -> Bit .
  op nil : -> Bits .
  op __ : Bits Bits -> Bits [assoc id: nil prec 41 gather (e E)] .
  op |_| : Bits -> MachineInt [prec 0 gather (&)] .
  op normalize : Bits -> Bits .
  op _+_ : Bits Bits -> Bits [assoc comm prec 41 gather (e E)] .
  op _*_ : Bits Bits -> Bits [assoc comm prec 41 gather (e E)] .
  op _^_ : Bits Bits -> Bits [prec 41 gather (E E)] .
  op _>_ : Bits Bits -> Bool [prec 41 gather (E E)] .
  op _?_:_ : Bool Bits Bits -> Bits [prec 41 gather (E & E)] .
  op not_ : Bits -> Bits [prec 15 gather (E)] .