Default gathering patterns

As for precedence values, Maude assigns default gathering patterns to all those operators for which the user does not specify this information as part of the operator declaration. The default gathering patterns are also entirely similar to those used by OBJ3 [44]. The rules for the assignment of the default gathering patterns are:

• All arguments of prefix operators have a gathering value &, regardless of the user specification.

• If the underbar corresponding to an argument is not adjacent to another underbar, and it is neither the leftmost nor the rightmost token in the operator, then the default gathering value for such an argument is &. In other words, if an underbar appears between tokens different from the underbar, then its corresponding argument will have this default gathering pattern. For example, the default gathering pattern for the operator if_then_else_fi is (& & &), the default gathering pattern for the operator [_and then_] is (& &), and the default gathering pattern for the operator (_) is (&).

• If the underbar corresponding to an argument is adjacent to another underbar, or if it is the leftmost or the rightmost token in the operator, then the default gathering value for such an argument is E. Thus, e.g., the default gathering pattern for the operator not_ is (E), the default gathering pattern for the operator _?_:_ is (E & E), the default gathering pattern for the operator _+_ is (E E), and the default gathering pattern for the operator __ is (E E).

  Those binary operators which start with an underscore, end with an underscore, and have a precedence greater than 0 are handled as special cases:

  • The operator will have gathering pattern (e E) if it has the assoc attribute (see Section 4.4.1). For example, the following operators fall into this category.

      op _+_ : Nat Nat -> Nat [assoc] .
      op _*_ : Nat Nat -> Nat [assoc] .
      op __ : NatList NatList -> NatList [assoc] .
    

  • If the operator does not have the assoc attribute, but its first argument, its last argument, and its coarity are in the same connected component of sorts, then:
    1. if the subsort relations allow it to right-associate but not left-associate, then the first argument's gathering pattern will change to e, and
    2. if the subsort relations allow it to left-associate but not right-associate, then the last argument's gathering pattern will change to e.

    Assuming Int < IntList, then the operators

      op _<:_ : Int IntList -> IntList .
      op _:>_ : IntList Int -> IntList .
    

    have, by default, gathering patterns (e E) and (E e), respectively. According to the general rule, since their argument bars are the leftmost and the rightmost tokens, the gathering pattern should be (E E) for both of them. However, both operators fall into the second special case, since they are binary operators which start and end with underscores, have a precedence greater than 0 (by default 41), and are not declared associative. Given the subsort relation, the operator _<:_ may right-associate, but not left-associate, that is, 1 <: 2 <: 3 should be parsed as 1 <: (2 <: 3), but (1 <: 2) <: 3 should not be a valid parse. Therefore, _<:_ gets default gathering pattern (e E). And similarly for _:>_, although in this case it can left-associate, and therefore it gets default gathering pattern (E e).