Quoted identifiers have the following signature:
fmod QID is
protecting MACHINE-INT .
sort Qid .
op <Qids> : -> Qid [special ( ... )] .
op conc : Qid Qid -> Qid [special ( ... )] .
op index : Qid MachineInt -> Qid [special ( ... )] .
op strip : Qid -> Qid [special ( ... )] .
endfm
Typical constants of sort Qid are quoted identifiers such as 'a,
'aa, 'f`(x`), '-1, "123abc, and 'A_quoted_identifier. Every quoted identifier is a legal Maude
identifier. That is, it satisfies the conventions for Maude identifiers
explained in Section 2.1.1 and, in addition, it begins with the
quote character. Of course, in syntax declarations for sorts, variables,
etc., of a module that includes QID we should avoid using quoted names,
since they are now used for constants of sort Qid. In fact, that is the
whole point of using a module of quoted identifiers instead of a module of
general identifiers, since that could create massive ambiguities.
Quoted identifiers are defined in a built-in way by the first operator declaration. The operation conc concatenates two quoted identifiers, omitting the quote of the second. The operation index appends the result of the machine integer expression at the end of the quoted identifier. The operation strip strips off the first character after the quote. Their semantics can be inferred from the following examples:
conc('a, 'b) = 'ab
conc('a, '42) = 'a42
index('a, 2 * 21) = 'a42
conc('a, index(' , 1 - 43)) = 'a-42
strip('abcd) = 'bcd
For different purposes it is useful to have not only quoted identifiers, but also a data type of lists of quoted identifiers. In particular, the remaining two predefined modules in the standard library, namely META-LEVEL and LOOP-MODE--discussed in Sections 2.5 and 2.8, respectively--both import the following QID-LIST module.
fmod QID-LIST is
protecting QID .
sort QidList .
subsort Qid < QidList .
op nil : -> QidList .
op __ : QidList QidList -> QidList [assoc id: nil] .
endfm