Metarepresenting terms

In the module META-TERM, terms are metarepresented as elements of the data type Term of terms. The base cases in the metarepresentation of terms are given by subsorts Constant and Variable of the sort Qid.

  sorts Constant Variable Term .
  subsorts Constant Variable < Qid Term .
  op <Qids> : -> Constant [special (...)] .
  op <Qids> : -> Variable [special (...)] .

Constants are quoted identifiers that contain the constant's name and its type separated by a `.', e.g., '0.Nat. Similarly, variables contain their name and type separated by a `:', e.g., 'N:Nat. Appropriate selectors then extract their names and types.

  op getName : Constant -> Qid .
  op getName : Variable -> Qid .
  op getType : Constant -> Type .
  op getType : Variable -> Type .

Since `.' and `:' are not allowed in sort names (see Section 3.3), the name and type of a constant or variable can be calculated easily. Note that there is no restriction in operator or in variable names, and thus the scanning for `.' or `:' is done from right to left in the identifier. That is,

  getName(':-D:Smile) = ':-D
  getType(':-.|.`[Smile`]) = '`[Smile`]

A term is constructed in the usual way, by applying an operator symbol to a list of terms.

  sort TermList .
  subsort Term < TermList .
  op _,_ : TermList TermList -> TermList 
      [ctor assoc gather (e E) prec 120] .
  op _[_] : Qid TermList -> Term [ctor] .

Since terms in the module META-TERM can be metarepresented just as terms in any other module, the metarepresentation of terms can be iterated.

For example, the term c q M:Marking in the module VENDING-MACHINE in Section 5.1 is metarepresented by

  '__['c.Item, '__['q.Coin, 'M:Marking]]

and meta-metarepresented by

  '_`[_`][''__.Qid,
          '_`,_[''c.Item.Constant,
                '_`[_`][''__.Qid,
                        '_`,_[''q.Coin.Constant,
                              ''M:Marking.Variable]]]]

Note that the metarepresentation of a natural number such as, e.g., 42 is 's_^42['0.Zero] instead of '42.NzNat, since, as explained in Section 7.2, 42 is just syntactic sugar for s_^42(0).