Operator declarations

In a Maude module, an operator is declared with the keyword op followed by its name, followed by a colon, followed by the list of sorts for its arguments (called the operator's arity or domain sorts), followed by ->, followed by the sort of its result (called the operator's coarity or range sort), optionally followed by an attribute declaration (the discussion of operator attributes is postponed to Section 4.4), followed by white space and a period. Thus the general scheme has the form

  op $\langle$OpName$\rangle$ : $\langle$Sort-1$\rangle$ ... $\langle$Sort-k$\rangle$ -> $\langle$Sort$\rangle$ [$\langle$OperatorAttributes$\rangle$] .

Here are some operator declarations for our NUMBERS module.

  op zero : -> Zero .
  op s_ : Nat -> NzNat .
  op sd : Nat Nat -> Nat .
  ops _+_ _*_ : Nat Nat -> Nat .

If the argument list is empty, the operator is called a constant. Thus zero is a constant.

The name of the operator is a string of characters that may consist of several identifiers, due to the presence of blanks or other special characters. Underscores (_) play a special role in these strings. If no underscore character occurs in the operator string--as in the case of the operator sd above--then the operator is declared in prefix form. If underscore characters occur in the string, then their number must coincide with the number of sorts declared as arguments of the operator (in particular, constant names cannot include any underscore character). The operator is then in mixfix form, with the $n$-th underscore indicating the place where arguments of the $n$-th sort must be placed in expressions formed with that operator. In the above example the operators s_, _+_, and _*_ are in mixfix form.

There may or may not be any other characters before or after any of the underbars. If no other characters appear, we say that the operator has been declared with empty syntax. For example, we could declare a sort NatSeq of sequences of natural numbers formed with empty syntax as follows:

  sort NatSeq .
  subsort Nat < NatSeq .
  op __ : NatSeq NatSeq -> NatSeq [assoc] .

where assoc is an attribute declaring that sequence concatenation is associative (see Section 4.4.1). With this operator declaration we can write number sequences such as

  zero (s zero) (s s zero)

Operators having the same arity and coarity can be declared simultaneously by using the keyword ops and giving the non-empty list of their corresponding names after the ops keyword and before the :, as is done for the declarations of _+_ and _*_ in the example above.

An operator can also be declared using several identifiers. This can be due to the presence of special characters, or to blank spaces, or both. Consider for example the operator declaration

  op [_] and then [_] : Command Command -> Command .

that may allow a natural language style in the syntax of a programming language. It uses eight identifiers in the Maude sense, but declares a single binary operator, with the underscores indicating the place of the arguments in the mixfix notation. Internally, Maude also associates to this operator a corresponding single-identifier form by using backquotes. We could have equivalently defined the operator using the single-identifier form, namely,

  op `[_`]and`then`[_`] : Command Command -> Command .

Of course, both variants are equivalent and have the same mixfix display, but the version without backquotes is obviously more convenient.^3.2

The declaration of an operator requires an extra pair of parentheses if we already use parentheses as part of the syntax of the operator. Suppose we had in a programming language a binary operator (_ only after _). Then, we have to declare it as follows:

  op ((_ only after _)) : Command Command -> Command .

Since an operator may be declared using several identifiers, in an ops declaration involving several operators each operator declaration can be enclosed in parentheses if necessary, to indicate where the syntax of each operator begins and ends. We could have declared both operators together, as follows:

  ops ([_] and then [_]) ((_ only after _)) : 
    Command Command -> Command .

Thus, one or several Maude identifiers can be used in operator declarations. Regarding style, the preferred one, particularly for single-identifier operators with prefix syntax, is to use lower case names. However, for a composed name such as a meta parse operator, the subsequent names will be juxtaposed and will typically begin with a capital letter to enhance readability, e.g., metaParse.