Quoted identifiers

The module QID is a wrapper for strings in order to provide a Maude representation for tokens of Maude syntax. Quoted identifiers are input and output by preceding a Maude identifier^7.4 with a (fore) quote sign. Thus 'abc is a quoted identifier whose underlying string is "abc". A quoted identifier is also an identifier, as are strings. Thus ''abc and '"abc" are both quoted identifiers.

  fmod QID is
    protecting STRING .
    sort Qid .
    op <Qids> : -> Qid [special (...)] .

    ***  qid <-> string conversions
    op string : Qid -> String [special (...)] .
    op qid : String ~> Qid [special (...)] .
  endfm

The operators qid and string do the wrapping and unwrapping. string is injective, since every quoted identifier has a unique corresponding string.

  Maude> red in QID : string('abc) .
  result String: "abc"

  Maude> red qid("abc") .
  result Qid: 'abc

  Maude> red string('a\b) .
  result String: "a\\b"

  Maude> red qid("a\\b") .
  result Qid: 'a\b

  Maude> red string('a`[b) .
  result String: "a`[b"

  Maude> red qid("a[b") .
  result Qid: 'a`[b

The operator qid is only injective on strings without white space, control characters, and certain other characters which are converted to backquote. Thus the equation qid(string(q)) = q holds for quoted identifiers q.

  Maude> red in QID : qid("a b c") .
  result Qid: 'a`b`c

  Maude> red string('a`b`c) .
  result String: "a`b`c"

  Maude> red qid("a\t b") .
  result Qid: 'a`b

  Maude> red string('a`b) .
  result String: "a`b"

An example of a string that cannot be converted to a quoted identifier is "a\"b" since identifiers are not allowed to have unpaired double quotes. Thus qid("a\"b") has kind [Qid] but does not reduce to something of sort Qid.