Lists over a given sort of elements (provided by the theory TRIV)
are constructed from the constant nil (representing
the empty list) and singleton lists (identified with the corresponding
elements by means of a subsort declaration) by means of an associative
concatenation operator written as juxtaposition with empty syntax __.
Since there are several operations that are not well defined over the empty list, it is most useful to define the subsort of non-empty lists.
fmod LIST{X :: TRIV} is
protecting NAT .
sorts NeList{X} List{X} .
subsort X$Elt < NeList{X} < List{X} .
op nil : -> List{X} [ctor] .
op __ : List{X} List{X} -> List{X} [ctor assoc id: nil prec 25] .
op __ : NeList{X} List{X} -> NeList{X} [ctor ditto] .
op __ : List{X} NeList{X} -> NeList{X} [ctor ditto] .
vars E E' : X$Elt .
vars A L : List{X} .
var C : Nat .
The operator append is just another name for concatenation.
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(A, L) = A L .
The operations head and tail take and discard, respectively, the first (leftmost) element in a list. Analogously, the operations last and front take and discard, respectively, the last (rightmost) element in a list. It is enough to have one equation for each operation, because the case of a singleton list is obtained by matching modulo identity with L = nil.
op head : NeList{X} -> X$Elt .
eq head(E L) = E .
op tail : NeList{X} -> List{X} .
eq tail(E L) = L .
op last : NeList{X} -> X$Elt .
eq last(L E) = E .
op front : NeList{X} -> List{X} .
eq front(L E) = L .
The predicate occurs checks whether an element appears in any position in a list. The two equations in its specification correspond to the typical case analysis (or structural induction) over lists: either the list is empty or we consider the corresponding first element (in the latter case, again one equation is enough).
op occurs : X$Elt List{X} -> Bool .
eq occurs(E, nil) = false .
eq occurs(E, E' L) = if E == E' then true else occurs(E, L) fi .
Reversing a list is accomplished by means of the operator reverse, which is efficiently defined through an auxiliary operator $reverse that has an additional accumulator argument. With this argument, $reverse has a simple tail-recursive and thus efficient definition.
op reverse : List{X} -> List{X} .
op reverse : NeList{X} -> NeList{X} .
eq reverse(L) = $reverse(L, nil) .
op $reverse : List{X} List{X} -> List{X} .
eq $reverse(nil, A) = A .
eq $reverse(E L, A) = $reverse(L, E A).
The tail-recursive method of definition just described will be used in the specification of several other operators, including the size operator on lists, which computes the number of elements in a list.
op size : List{X} -> Nat .
op size : NeList{X} -> NzNat .
eq size(L) = $size(L, 0) .
op $size : List{X} Nat -> Nat .
eq $size(nil, C) = C .
eq $size(E L, C) = $size(L, C + 1) .
endfm
In the Maude prelude there are two list instantiations on built-in data types (natural numbers and quoted identifiers) that are needed by the metalevel (see Chapter 11).
fmod NAT-LIST is
protecting LIST{Nat} * (sort NeList{Nat} to NeNatList,
sort List{Nat} to NatList) .
endfm
fmod QID-LIST is
protecting LIST{Qid} * (sort NeList{Qid} to NeQidList,
sort List{Qid} to QidList) .
endfm
Other instantiations can be built as desired. For example, we can use the view Int from TRIV to INT, and then test some reductions, as follows.
fmod INT-LIST is
pr LIST{Int} .
endfm
Maude> red in INT-LIST : reverse(0 -1 2 -3 4 -5 6) .
result NeList{Int}: 6 -5 4 -3 2 -1 0
Maude> red occurs(7, 0 -1 2 -3 4 -5 6) . result Bool: false
Maude> red size(0 -1 2 -3 4 -5 6) . result NzNat: 7