In the META-TERM module, sorts and kinds are metarepresented as data in specific subsorts of the sort Qid of quoted identifiers.
A term of sort Sort is any quoted identifier not containing the
following characters: `:', `.', `[', and
`]'. Moreover, the characters `{', `}', and `,'
can only appear in structured sort names (see Section 3.3).
For example, 'Bool,
'NzNat, a`{X`}, a`{X`,Y`}, a`{b`,c`{d`}`}`{e`}, and
a`{`(`} are terms of sort Sort.
An element of sort Kind is a quoted identifier of the
form '`[SortList`] where SortList is a single
identifier formed by a list of unquoted elements of sort Sort
separated by backquoted commas. For example, '`[Bool`] and
'`[NzNat`,Zero`,Nat`] are valid elements of the sort Kind. Note
the use of backquotes to force them to be single identifiers.
Since commas and square brackets are used to metarepresent kinds, these characters are forbidden in sort names, in order to avoid undesirable ambiguities. Periods and colons are also forbidden, due to the metarepresentation of constants and variables, as explained in the next section.
Since operator declarations can use both sorts and kinds, we denote by Type the union of Sort and Kind.
sorts Sort Kind Type . subsorts Sort Kind < Type < Qid. op <Qids> : -> Sort [special (...)] . op <Qids> : -> Kind [special (...)] .
Remember from the introduction of Chapter 7 that <Qids> is a special operator declaration used to represent sets of constants that are not algebraically constructed, but are instead associated with appropriate C++ code by ``hooks'' which are specified following the special attribute; see the functional module META-TERM in file prelude.maude for the details omitted here.