2.8.1 The Use of the Loop

We can illustrate the basic ideas with a toy example, namely a system in which the loop is used to echo each input twice. In this case there is no need to maintain any state, so we can just declare a constant null to represent the empty state.

  mod DUPLICATE is
    including LOOP-MODE .
    op null : -> State .
    vars Input Output : QidList .
    crl [duplicate] : 
       [Input, null, Output] 
       => [nil, null, Output Input Input] 
          if Input =/= nil .
  endm

Once this module has been entered, we must first initialize the loop by setting its initial state using the loop command. That is, we must give to the loop command the term of sort State that we desire as initial state. For this example, we can start a loop with empty input and output channels by typing

  Maude> loop [nil, null, nil] .

Since in the current release only one input channel is supported (the current terminal), the way to distinguish the input passed to the loop from the input to the Maude system--modules or commands--is by enclosing them in parentheses. When something is written in the Maude prompt enclosed in parentheses it is converted into a list of quoted identifiers. This is done by first breaking the input stream into a sequence of tokens--that is, into a sequence of Maude identifiers--and then converting each of these tokens into a quoted identifier by putting a quote in front of it, and appending the results into a list of quoted identifiers, which is then placed in the first slot of the loop object. The output is handled in the reverse way, that is, the list of quoted identifiers placed in the third slot of the loop is printed on the terminal after applying the inverse process of "unquoting" each of the tokens in the list. However, the output channel is not cleared at the time when the output is printed; it is instead cleared when the next input is entered. We can think of the input and output events as implicit rewrites that transfer--in a slightly modified, quoted or unquoted form--the input and output data between two objects, namely the loop object and the "user" or "terminal" object.

Once the loop has been initialized we can input any data by writing it after the prompt enclosed in parentheses. For example, we can write

  Maude> (a s d )

  a s d a s d

A somewhat more interesting example is a loop that echoes the input, but only after every ten tokens, that is, it keeps the input until the number of tokens stored in the state is ten. In this case the input introduced so far has to be stored. Therefore we now really need a persistent state, albeit a simple one. We can represent the state as a pair consisting of a list of quoted identifiers--the tokens seen so far since the last printing--and a counter measuring the length of such a list.

  mod DUPLICATE-TEN is
    including LOOP-MODE .
    protecting MACHINE-INT .
    op <_;_> : QidList MachineInt -> State .
    op init : -> System .
    vars Input StoredInput Output : QidList .
    vars QI QI0 QI1 QI2 QI3 QI4 QI5 QI6 QI7 QI8 QI9 : Qid .
    var Counter : MachineInt .
    rl [init] :
       init => [nil, <  nil ; 0 >, nil] .
    rl [in] : 
       [QI Input, < StoredInput ; Counter >, Output] 
       => [Input, < StoredInput QI ; Counter + 1 >, Output] .
    rl [out] :
       [Input, 
        < QI0 QI1 QI2 QI3 QI4 QI5 QI6 QI7 QI8 QI9 StoredInput ; 
          Counter >, 
        Output] 
       => [Input, 
           < StoredInput ; Counter - 10 >, 
           Output QI0 QI1 QI2 QI3 QI4 QI5 QI6 QI7 QI8 QI9] .
  endm

  Maude> loop init .

  Maude> (a b)

  Maude> (c d e f g h i)

  Maude> (j k l)

  a b c d e f g h i j

We can see the state of the loop with the continue command as follows.

  Maude> cont .
  result System: [nil,< 'k 'l ; 2 >,'a 'b 'c 'd 'e 'f 'g 'h 'i 'j]