Parsing examples

Maude provides the parse command for parsing terms. The command does not do anything other than parsing the given term in the extended signature of the module. This is exactly what is done when a term appears in a command, before executing such a command. For example, when we try to reduce a term (2 + 3) * 5, the system first parses it and then reduces it. If the term is ambiguous, or there is no parse for it, an error message is given and no further action takes place.

  Maude> reduce in NAT : 2 + true .
  Warning: <standard input>, line 1: 
    didn't expect token true: 2 + true <---*HERE*
  Warning: <standard input>, line 1: no parse for term.

For testing the parsing of terms we can use the parse command.

  Maude> parse in NAT : 2 + true .
  Warning: <standard input>, line 1: 
    didn't expect token true: 2 + true <---*HERE*
  Warning: <standard input>, line 1: no parse for term.

As other commands, parsing can take place either in the module explicitly mentioned in the command or in the current module.

We illustrate the use of the parse command for the examples introduced in the previous sections. Let us first consider a module PARSING-EX1 with constants 1, 2, and 3, and binary operators _+_ and _*_.

  fmod PARSING-EX1 is
    sort Nat .
    ops 1 2 3 : -> Nat .
    ops _+_ _*_ : Nat Nat -> Nat .
  endfm

Since _+_ and _*_ are declared without precedence values, and therefore both get the default value 41, we obtain the following result.

  Maude> parse 1 + 2 * 3 .
  Warning: <standard input>, line 13: ambiguous term, two parses are:
  1 + (2 * 3) -versus- (1 + 2) * 3

  Arbitrarily taking the first as correct. Nat: 1 + (2 * 3)

As a first solution, we may consider using parentheses.

  Maude> parse in PARSING-EX1 : 1 + (2 * 3) .
  Nat: 1 + (2 * 3)

  Maude> parse in PARSING-EX1 : (1 + 2) * 3 .
  Nat: (1 + 2) * 3

Let us now consider the module PARSING-EX2, where _+_ and _*_ are declared with precedences 33 and 31, respectively.

  fmod PARSING-EX2 is
    sort Nat .
    ops 1 2 3 : -> Nat .
    op _+_ : Nat Nat -> Nat [prec 33] .
    op _*_ : Nat Nat -> Nat [prec 31] .
  endfm

Now, parentheses are not necessary for parsing the term 1 + 2 * 3.

  Maude> parse in PARSING-EX2 : 1 + 2 * 3 .
  Nat: 1 + 2 * 3

Of course, we may still use parentheses.

  Maude> parse in PARSING-EX2 : (1 + 2) * 3 .
  Nat: (1 + 2) * 3

Since the default gathering patterns for binary operators like _+_ and _*_ is (E E), a term like 1 + 2 + 3 is ambiguous.

  Maude> parse in PARSING-EX2 : 1 + 2 + 3 .
  Warning: <standard input>, line 30: ambiguous term, two parses are:
  1 + (2 + 3) -versus- (1 + 2) + 3

  Arbitrarily taking the first as correct. Nat: 1 + (2 + 3)

As above, we may use parentheses to parse such terms.

  Maude> parse in PARSING-EX2 : (1 + 2) + 3 .
  Nat: (1 + 2) + 3

  Maude> parse in PARSING-EX2 : 1 + (2 + 3) .
  Nat: 1 + (2 + 3)

Let us now consider the module PARSING-EX3, where _+_ and _*_ are declared to be left-associative, that is, with gathering patterns (E e).

  fmod PARSING-EX3 is
    sort Nat .
    ops 1 2 3 : -> Nat .
    op _+_ : Nat Nat -> Nat [prec 33 gather (E e)] .
    op _*_ : Nat Nat -> Nat [prec 31 gather (E e)] .
  endfm

Now, the terms above have unambiguous parses.

  Maude> parse in PARSING-EX3 : 1 + 2 * 3 .
  Nat: 1 + 2 * 3

  Maude> parse in PARSING-EX3 : 1 + 2 + 3 .
  Nat: 1 + 2 + 3

Let us now consider the module PARSING-EX4, where _+_ and _*_ are declared to be associative. Note that in this case, by default, they are assigned gathering patterns (E e).

  fmod PARSING-EX4 is
    sort Nat .
    ops 1 2 3 : -> Nat .
    op _+_ : Nat Nat -> Nat [prec 33 assoc] .
    op _*_ : Nat Nat -> Nat [prec 31 assoc] .
  endfm

  Maude> parse in PARSING-EX4 : 1 + 2 * 3 .
  Nat: 1 + 2 * 3

  Maude> parse in PARSING-EX4 : 1 + 2 + 3 .
  Nat: 1 + 2 + 3

We illustrate the use of the extended signature in which all terms are parsed with the following examples.

  Maude> parse in PARSING-EX1 : (2 + 3).Nat .
  Nat: 2 + 3

  Maude> parse in PARSING-EX1 : (2).Nat + 3 .
  Nat: 2 + 3

  Maude> parse in PARSING-EX1 : (2).Nat + (3).Nat .
  Nat: 2 + 3

  Maude> parse in PARSING-EX1 : ((1) + ((2) + (3))) .
  Nat: 1 + (2 + 3)

  Maude> parse in PARSING-EX1 : _+_(1, _+_(2, 3)) .
  Nat: 1 + (2 + 3)

  Maude> parse in PARSING-EX4 : _+_(1, 2, 3) .
  Nat: 1 + 2 + 3

  Maude> parse in PARSING-EX4 : if 1 == 2 then 1 + 2 else _+_(1, 2) fi .
  Nat: if 1 == 2 then 1 + 2 else 1 + 2 fi

  Maude> parse in PARSING-EX4 :
           if _==_(1, 2)
           then if_then_else_fi(1 + 2 :: Nat, 1 * 1, 2 * 1)
           else _+_(1, 2)
           fi .
  Nat: if 1 == 2
       then if (1 + 2) :: Nat
            then 1 * 1
            else 2 * 1
            fi
       else 1 + 2
       fi