The META-LEVEL module, which imports META-MODULE, has several
built-in descent functions that provide useful and efficient ways of reducing
metalevel computations to object-level ones, as well as several useful
operations on sorts and kinds. Since, in general, these operations take
among their arguments the metarepresentations of modules, sorts, kinds, terms,
and so on,
the META-LEVEL modules also provides several built-in functions
for moving conveniently between reflection levels.
Notice that most of the operations in the module META-LEVEL are partial
(as explicitly stated by using the arrow ~> in the corresponding operator declaration).
This is due to the fact that they do not make sense on terms that, although
may be of the correct sort, for example, Module or Term, either are not
correct metarepresentations of modules or are not correct metarepresentations of terms
in the module provided as another argument.
Concerning partial operations, the criteria used to choose between using a supersort for the result and having an operator map to a kind is as follows.
If the error return value is built from constructors, say
op noParse : Nat -> ResultPair? [ctor] . op ambiguity : ResultPair ResultPair -> ResultPair? [ctor] .
it goes to a supersort. In some sense these are not errors, but merely exceptions or out-of-band results for which there is a carefully defined semantics.
The kind is reserved for nonconstructors which may not be able to reduce at all on illegal arguments, like, for example, in the function (notice the form of the arrow)
op metaParse : Module QidList Type? ~> ResultPair? [special (...)] .
In this second case, an expression that does not evaluate to the appropriate sort represents a real error.
So, for example, a call to metaParse with an ill-formed module would produce an unreduced term metaParse(...) in the kind, whereas a call to metaParse with valid arguments but a list of tokens that could not be parsed to a term of the desired type in the metamodule would produce a term noParse(...) of sort ResultPair? indicating where the parse first failed.