Maude Manual -- 2.7.3 Parsing Terms in the Extended Signature of a Module

Go backward to 2.7.2 Mixfix Parsing of Terms in a Module
Go up to 2.7 Parsing, Bubbles and Meta-Parsing
Go forward to 2.7.4 Precedence and Gathering

2.7.3 Parsing Terms in the Extended Signature of a Module

In BINARY-NAT it is possible to reduce the following terms.

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

  Maude> red ((1 0) > 1) and ((1 1) > (1 0)) .
  result Bool: true

  Maude> red (1).Bit * 0 .
  result Bit: 0

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

But, parentheses, logical operators such as and, sort tests, and qualification operators are not a proper part of the module. These structures belong to the so-called extended signature of a module. That is, the process of grammar generation from the user-defined signature adds automatically more information than that strictly contained in the signature. From the user's viewpoint, the main structures added in the extended signature of a module are:

Sort Disambiguation: For each sort S in the signature of the module, Maude generates the operator
```
  op (_).S : S -> S .
```
This helps in the disambiguation of ad-hoc overloaded constants and terms. For example, in the module BINARY-NAT, because of the presence of machine integers, the constants 0 and 1 and the operator _+_ are ad hoc overloaded (see Section 2.1.1). Thus, terms such as 0, 1 or 1 + 1 are ambiguous. We can eliminate this ambiguity by using sort disambiguation operators, that is, by qualifying the ambiguous terms with their sorts.
```
  Maude> red (1).Bit .
  result Bit: 1

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

  Maude> red 1 + (1).MachineInt .
  result NzMachineInt: 2
```
Parentheses: For each sort S in the signature of a module, the extended signature of that module contains the following operator.
```
  op (_) : S -> S .
```
These operators allow the use of parentheses without having to declare a parentheses operator for each sort.
```
  Maude> red not (1 0 1 1) .
  result Bits: 0 1 0 0
```
Prefix Form of Mixfix Operators or Simple Identifier Form: Each operator declared in mixfix form, may also be used in its single identifier prefix form. For example:
```
Maude> red _>_(1 0, 1) .
result Bool: true

Maude> red _?_:_(1 > 1 0, 1, 0) .
result Bit: 0
```
Flattened Associative Argument Lists: Operators with the attribute assoc may be used in Maude in a nonparenthesized form.
```
  Maude> red (1 1) + (1 1) + (1 1) + (1 1) .
  result Bits: 1 1 0 0
```
Furthermore, if the associative operator is given in prefix notation, it can take not only two, but arbitrarily many more arguments.
```
  Maude> red _+_(1 1, 1 1, 1 1, 1 1) .
  result Bits: 1 1 0 0
```
Polymorphic Operators and the BOOL Module: All the information contained in the predefined modules TRUTH-VALUE, TRUTH and BOOL (see Section 2.4) is included in the extended signature of each module. In particular, appropriate instances of the polymorphic operators contained in TRUTH (that is, if_then_else_fi, _==_ and _=/=_) are generated for each sort in the module. In addition, for each sort S sort predicates _:S and _::S are also added.
Note that this extension of the signature has allowed the specification of operators, variables, and equations such as the following ones in BINARY-NAT.
```
  op _?_:_ : Bool Bits Bits -> Bits .

  var L : Bool .

  eq B S > C T 
    = if | normalize(B S) | > | normalize(C T) |
      then true
      else if | normalize(B S) | < | normalize(C T) |
           then false
           else (S > T)
           fi
      fi .
```
The extended signature includes also the error supersorts, and the overloaded lifting to those supersorts of all operators to support error terms.