Prev Up
Go backward to 2.5.5 Descent Functions
Go up to 2.5 Reflection and the META-LEVEL

2.5.6 Parsing, Pretty Printing, and Sort Functions

Besides the descent functions already discussed, META-LEVEL provides several other functions that naturally belong to the universal theory and could have been equationally axiomatized in such a theory. However, for efficiency reasons they are provided as built-in functions. These functions allow parsing and pretty printing a term in a module at the metalevel, and performing efficiently a number of useful operations on the sorts declared in a module's signature.

The function meta-parse has syntax 

  op meta-parse : Module QidList -> Term [special ( ... )] .
It takes as arguments the representation of a module and the representation of a list of tokens as a list of quoted identifiers. It returns the meta-representation of the parsed term of that list of tokens for the signature of the module, which is assumed to be unambiguous. If such a parsed term does not exist, the error constant error* is returned instead. For example, given the module NAT presented in Section 2.5.4 and the input 's '0 '+ '0, we get 
  Maude> red meta-parse( |¯NAT¯| , ('s '0 '+ '0)) .
  result Term: '_+_['s_['0'Zero],'0'Zero]

The function meta-pretty-print has syntax 

  op meta-pretty-print : Module Term -> QidList 
        [special ( ... )] .
It takes as arguments the representation of a module M and the representation of a term t. It returns a list of quoted identifiers that encode the string of tokens produced by pretty printing t in the syntax given by M. In the event of an error an empty list is returned. Thus, given the module NAT presented in Section 2.5.4, we have, e.g., 
  Maude> red meta-pretty-print( |¯NAT¯| , 
              '_*_['_+_['s_['0'Zero], '0'Zero], 's_['0'Zero]]) .
  result QidList: '`( 's '0 '+ '0 '`) '* 's '0

Pretty printing a term involves more than just naively using the mixfix syntax for operators. Precedence and gathering information (see Section 2.7.4) 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. Also, 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 operations on sorts include sameComponent, leastSort, lesserSorts, sortLeq, and glbSorts. They provide commonly needed functions on the poset of sorts of a module in a built-in way at the metalevel. Their syntax is as follows 

  subsort Qid < Sort .

  op leastSort : Module Term -> Sort [special ( ... )] .
  op sortLeq : Module Sort Sort -> Bool [special ( ... )] .
  op sameComponent : Module Sort Sort -> Bool [special ( ... )] .
  op lesserSorts : Module Sort -> QidSet [special ( ... )] .
  op glbSorts : Module Sort Qid -> QidSet [special ( ... )] .
At the metalevel, the sorts given by the user in his/her module are represented as quoted identifiers, that is, terms of sort Qid. However, the module META-LEVEL has also a sort Sort defined to be a supersort of Qid. Sorts not defined by the user, as for example the "error supersorts" added by the system to complete each connected component, are in this sort Sort. The syntax of an error supersort uses the set of maximal sorts of its connected component and is as follows 
  op errorSort : QidSet -> Sort .

The function leastSort takes as arguments the representations of a module and a term and computes the (representation of the) least sort of that term in the module. This function can return an error sort not defined by the user. For example, we can compute the least sort of the term  |¯N + s M¯|  in the previous module NAT as follows. 

  Maude> red least-sort( |¯NAT¯| ,  |¯N + s M¯| ) .
  result Qid:  |¯Nat¯|

Given a module M with subsort relation < M, and sorts s,s' e S, where S is the set of sorts in M, the Boolean function sortLeq( |¯M¯| , |¯s¯| , |¯s'¯| ) is true if and only if s < M s'. Note that the sorts passed to the function are of sort Sort. 

  Maude> red sortLeq( |¯NAT¯| ,  |¯Nat¯| ,  |¯NzNat¯| ) .
  result Bool: false

Given a module M with subsort relation < M, and sorts s,s' e S, where S is the set of sorts in M, the Boolean function sameComponent( |¯M¯| ,  |¯s¯| , |¯s'¯| ) is true if and only if s and s' belong to the same connected component in the subsort ordering < M. Note that the sorts passed to the function are of sort Sort. 

  Maude> red sortLeq( |¯NAT¯| ,  |¯Nat¯| ,  |¯Bool¯| ) .
  result Bool: false
where it should be noted the sort Bool, although not explicitly present in the signature of NAT, is nevertheless present in its extended signature, as explained in Sections 2.1.1 and 2.7.2.

Given a module M and a sort s, the function lesserSorts takes their metalevel representations as arguments, and returns (the representation of the) set of sorts strictly smaller than s in M. For example: 

  Maude> red lesserSorts( |¯NAT¯| ,  |¯Nat¯| ) .
  result Qid:  |¯NzNat¯|
Note that in this case it returns only one sort (of sort Qid), but in general it returns a set of sorts. Since no error sorts can appear in such a set, that is, the sorts are all in fact quoted identifiers, the function lesserSorts returns a QidSet.

Finally, the function glbSorts takes the representations of two sorts and a module as input and computes the representation of the set of maximal lower bounds of the two sorts15. Note the asymmetry in the declaration of this function, having as arguments, together with the module, a sort of sort Sort and another of sort Qid. This asymmetry might be eliminated in a future version of the system. As an example for the use of this function, let us see how to compute the greatest lower bound for sorts Nat and NzNat in the module NAT presented above. 

  Maude> red glbSorts( |¯NAT¯| ,  |¯Nat¯| ,  |¯NzNat¯| ) .
  result Qid:  |¯NzNat¯|
As for lesserSorts, in general glbSorts returns a set of sorts.
Prev Up