Generalized lists

With the construction of parameterized lists described in Section 7.12.1, we can build, for example, lists of integers, or lists of lists of integers, but we cannot build lists in which we have as elements both integers and lists of integers; for this, we specify in this section the container of generalized or nestable lists.

In this specification we cannot use empty syntax in the same way as in Section 7.12.1, because we need something to distinguish the different levels of nesting of lists inside lists. We use an auxiliary sort Item, whose data are both elements and generalized lists (see the subsort declarations below); then we put such items next to each other by juxtaposition, getting in this way data of another auxiliary sort PreList, and finally we put square brackets around a ``prelist'' in order to get a generalized list. Notice that there is no empty ``prelist'' and that the empty generalized list [] is declared separately.

  fmod LIST*{X :: TRIV} is
    protecting NAT .
    sorts Item{X} PreList{X} NeList{X} List{X} .
    subsort X$Elt List{X} < Item{X} < PreList{X} .
    subsort NeList{X} < List{X} .

    op __ : PreList{X} PreList{X} -> PreList{X} [ctor assoc prec 25] .
    op [_] : PreList{X} -> NeList{X} [ctor] .
    op [] : -> List{X} [ctor] .

    vars A P : PreList{X} .
    var  L : List{X} .
    vars E E' : Item{X} .
    var  C : Nat .

The operator append now corresponds to concatenation of generalized lists and its definition is based on the juxtaposition of the ``prelists'' inside the generalized lists.

    op append : List{X} List{X} -> List{X} .
    op append : NeList{X} List{X} -> NeList{X} .
    op append : List{X} NeList{X} -> NeList{X} .
    eq append([], L) = L .
    eq append(L, []) = L .
    eq append([P], [A]) = [P A] .

The operations head, tail, last, and front work as for ``standard'' lists, but now they refer to the first or last item in the list, which can be either an element or a nested list. Now we need two equations for each operation, because the singleton case needs to be treated separately (recall that there is no empty ``prelist'').

    op head : NeList{X} -> Item{X} .
    eq head([E]) = E .
    eq head([E P]) = E .

    op tail : NeList{X} -> List{X} .
    eq tail([E]) = [] .
    eq tail([E P]) = [P] .

    op last : NeList{X} -> Item{X} .
    eq last([E]) = E .
    eq last([P E]) = E .

    op front : NeList{X} -> List{X} .
    eq front([E]) = [] .
    eq front([P E]) = [P] .

The predicate occurs checks whether an item (either an element or a list) appears in any position of the first level of a generalized list (but it does not go into deeper levels, that is, into nested lists). The three equations in its specification correspond to the typical case analysis (or structural induction) over these lists: either the list is empty, or it is a list with a single item, or it is a list with two or more items.

    op occurs : Item{X} List{X} -> Bool .
    eq occurs(E, []) = false .
    eq occurs(E, [E']) = (E == E') .
    eq occurs(E, [E' P]) 
      = if E == E' then true else occurs(E, [P]) fi .

The operators reverse and size for generalized lists work in a similar way to the operators with the same names in Section 7.12.1, and they are also defined by means of auxiliary operators $reverse and $size, respectively, with a tail-recursive definition. Notice, however, that these auxiliary operators work on ``prelists'' instead of lists. Moreover, size counts the number of items in the first level of a generalized list, but it does not count the items inside nested lists at deeper levels.

    op reverse : List{X} -> List{X} .
    op reverse : NeList{X} -> NeList{X} .
    eq reverse([]) = [] .
    eq reverse([E]) = [E] .
    eq reverse([E P]) = [$reverse(P, E)] .

    op $reverse : PreList{X} PreList{X} -> PreList{X} .
    eq $reverse(E, A) = E A .
    eq $reverse(E P, A) = $reverse(P, E A).

    op size : List{X} -> Nat .
    op size : NeList{X} -> NzNat .
    eq size([]) = 0 .
    eq size([P]) = $size(P, 0) .

    op $size : PreList{X} Nat -> NzNat .
    eq $size(E, C) = C + 1 .
    eq $size(E P, C) = $size(P, C + 1) .
  endfm

We consider the following instantiation and sample reductions:

  fmod INT-LIST* is
    pr LIST*{Int} .
  endfm

  Maude> red in INT-LIST* : append([1 []], [[] 2]) .
  result NeList{Int}: [1 [] [] 2]

  Maude> red reverse([[1 []] [[] 2]]) .
  result NeList{Int}: [[[] 2] [1 []]]

  Maude> red occurs(1, [[[] 2] [1 []]]) .
  result Bool: false

  Maude> red size([[[] 2] [1 []]]) .
  result NzNat: 2