Other metalevel operations: wellFormed

The operation wellFormed can take as arguments the metarepresentation of a module $\mathcal{R}$, or the metarepresentation of a module $\mathcal{R}$ and a term $t$, or the metarepresentation of a module $\mathcal{R}$ and a substitution $\sigma$. In the first case, it returns $\texttt{true}$ if $\mathcal{R}$ is a well-formed module, and false otherwise. In the second case, if $t$ is a well-formed term in $\mathcal{R}$, it returns $\texttt{true}$; otherwise, it returns false. Finally, in the third case, if $\sigma$ is a well-formed substitution in $\mathcal{R}$, it returns true; otherwise, it returns false.

  op wellFormed : Module -> Bool [special (...)] .
  op wellFormed : Module Term ~> Bool [special (...)] .
  op wellFormed : Module Substitution ~> Bool [special (...)] .

Note that the first operation is total, while the other two are partial (notice the form of the arrow in the declarations). The reason is that the last two are not defined when the term given as first argument does not represent a module, and then it does not make sense to check whether a term or substitution is well formed with respect to such a wrong ``module.''

For example,

  Maude> reduce in META-LEVEL :
           wellFormed(upModule('NUMBERS, false)) .
  result Bool: true

  Maude> reduce in META-LEVEL :
           wellFormed(upModule('NUMBERS, false), 'p['zero.Zero]) .
  result Bool: true

  Maude> reduce in META-LEVEL :
           wellFormed(upModule('NUMBERS, false), 
             's_['zero.Zero, 'zero.Zero]) .
  Advisory: could not find an operator s_ with appropriate domain
      in meta-module NUMBERS when trying to interprete metaterm 
      's_['zero.Zero,'zero.Zero].
  result Bool: false

  Maude> reduce in META-LEVEL :
           wellFormed(upModule('NUMBERS, false), 
             'N:Zero <- 'zero.Zero) .
  result Bool: true

  Maude> reduce in META-LEVEL :
           wellFormed(upModule('NUMBERS, false), 
             'N:Nat <- 'p['zero.Zero]) .
  result Bool: false

  Maude> reduce in META-LEVEL :
           wellFormed(upModule('NUMBERS, false), 
             'N:Zero <- 's_['zero.Zero,'zero.Zero]) .
  Advisory: could not find an operator s_ with appropriate domain 
      in meta-module NUMBERS when trying to interprete metaterm 
      's_['zero.Zero,'zero.Zero].
  result Bool: false