metaPrettyPrint

The (partial) operation metaPrettyPrint takes as arguments the metarepresentations of a module $\mathcal{R}$ and of a term $t$ together with a set of printing options, and it returns a list of quoted identifiers that metarepresents the string of tokens produced by pretty-printing the term $t$ in the signature of $\mathcal{R}$. In the event of an error an empty list of quoted identifiers is returned.

  op metaPrettyPrint : Module Term PrintOptionSet ~> QidList 
       [special (...)] .

Pretty-printing a term involves more than just naively using the mixfix syntax for operators. Precedence and gathering information and the relative positions of underscores in an operator and its parent in the term must be considered to determine whether parentheses need to be inserted around any given subterm to avoid ambiguity. If there is ad-hoc overloading in the module, additional checks must be done to determine if and where sort disambiguation syntax is needed.

The print options argument is built with the following syntax:

  sorts PrintOption PrintOptionSet .
  subsort PrintOption < PrintOptionSet .
  ops mixfix with-parens flat format number rat : -> PrintOption 
        [ctor] .
  op none : -> PrintOptionSet [ctor] .
  op __ : PrintOptionSet PrintOptionSet -> PrintOptionSet
          [ctor assoc comm id: none] .

The available print options form a subset of the global print options described in Section 16.6, which are ignored by this operation.

As an example, we can use metaPrettyPrint to pretty print the result of parsing at the metalevel the list of tokens $ q q q in the module VENDING-MACHINE, first with prefix syntax, then with mixfix syntax, and finally with mixfix syntax and taking into account the format attribute.

  Maude> reduce in META-LEVEL :
           metaPrettyPrint(upModule('VENDING-MACHINE, false),
             '__['$.Coin, '__['q.Coin, '__['q.Coin, 'q.Coin]]], 
             none) .
  result NeQidList: 
    '__ '`( '$ '`, '__ '`( 'q '`, '__ '`( 'q '`, 'q '`) '`) '`)

  Maude> reduce in META-LEVEL :
           metaPrettyPrint(upModule('VENDING-MACHINE, false),
             '__['$.Coin, '__['q.Coin, '__['q.Coin, 'q.Coin]]], 
             mixfix) .
  result NeTypeList: '$ 'q 'q 'q

  Maude> reduce in META-LEVEL :
           metaPrettyPrint(upModule('VENDING-MACHINE, false),
             '__['$.Coin, '__['q.Coin, '__['q.Coin, 'q.Coin]]], 
             mixfix format) .
  result NeTypeList: 
    '\r '\! '$ '\o '\r '\! 'q '\o '\r '\! 'q '\o '\r '\! 'q '\o

It is important to notice that metaPrettyPrint uses the information provided by the format attribute in the last reduction above. For example, the operator $ in the module VENDING-MACHINE-SIGNATURE in Section 5.1 was declared with attribute format (r! o), and therefore it is meta-pretty-printed as '\r '\! '$ '\o.

For backwards compatibility there is available the following variation of the metaPrettyPrint operation, which provides a set of default print options.

  op metaPrettyPrint : Module Term ~> QidList .
  eq metaPrettyPrint(M:Module, T:Term) 
    = metaPrettyPrint(M:Module, T:Term, 
        mixfix flat format number rat) .

For example,

  Maude> reduce in META-LEVEL :
           metaPrettyPrint(upModule('VENDING-MACHINE, false),
             '__['$.Coin, '__['q.Coin, '__['q.Coin, 'q.Coin]]]) .
  result NeTypeList: 
    '\r '\! '$ '\o '\r '\! 'q '\o '\r '\! 'q '\o '\r '\! 'q '\o