Chapter 17
Reflection, Metalevel Computation, and Internal Strategies

Informally, a reflective logic is a logic in which important aspects of its metatheory can be represented at the object level in a consistent way, so that the object-level representation correctly simulates the relevant metatheoretic aspects. In other words, a reflective logic is a logic which can be faithfully interpreted in itself. Maude’s language design and implementation make systematic use of the fact that rewriting logic is reflective [32, 25, 33, 34]. This makes the metatheory of rewriting logic accessible to the user in a clear and principled way. However, since a naive implementation of reflection can be computationally expensive, a good implementation must provide efficient ways of performing reflective computations. This chapter explains how this is achieved in Maude through its predefined META-LEVEL module, that can be found in the prelude.maude file.

17.1 Reflection and metalevel computation

Rewriting logic is reflective in a precise mathematical way, namely, there is a finitely presented rewrite theory 𝒰 that is universal in the sense that we can represent in 𝒰 any finitely presented rewrite theory ℛ (including 𝒰 itself) as a term ℛ, any terms t,t′ in ℛ as terms t,t′, and any pair (ℛ,t) as a term ⟨ℛ,t⟩, in such a way that we have the following equivalence

Since 𝒰 is representable in itself, we can achieve a “reflective tower” with an arbitrary number of levels of reflection:

In this chain of equivalences we say that the first rewriting computation takes place at level 0, the second at level 1, and so on. In a naive implementation, each step up the reflective tower comes at considerable computational cost, because simulating a single step of rewriting at one level involves many rewriting steps one level up. It is therefore important to have systematic ways of lowering the levels of reflective computations as much as possible, so that a rewriting subcomputation happens at a higher level in the tower only when this is strictly necessary.

In Maude, key functionality of the universal theory 𝒰 has been efficiently implemented in the functional module META-LEVEL. This module includes the modules META-VIEW, META-MODULE, META-STRATEGY, and META-TERM. As an overview,

• in the module META-TERM, Maude terms are metarepresented as elements of a data type Term of terms;
• in the module META-STRATEGY, the Maude strategy language is metarepresented as terms in a data type Strategy of strategy expressions;
• in the module META-MODULE, Maude modules are metarepresented as terms in a data type Module of modules;
• in the module META-VIEW, Maude views are metarepresented as terms in a data type View of views; and
• in the module META-LEVEL,
  • operations upModule, upTerm, downTerm, and others allow moving between reflection levels;
  • the process of reducing a term to canonical form using Maude’s reduce command is metarepresented by a built-in function metaReduce;
  • the processes of rewriting a term in a system module using Maude’s rewrite and frewrite commands are metarepresented by built-in functions metaRewrite and metaFrewrite;
  • the process of applying (without extension) a rule of a system module at the top of a term is metarepresented by a built-in function metaApply;
  • the process of applying (with extension) a rule of a system module at any position of a term is metarepresented by a built-in function metaXapply;
  • the process of matching (without extension) two terms at the top is reified by a built-in function metaMatch;
  • the process of matching (with extension) a pattern to any subterm of a term is reified by a built-in function metaXmatch;
  • the process of searching for a term satisfying some conditions starting in an initial term is reified by built-in functions metaSearch and metaSearchPath;
  • the processes of rewriting a term using Maude’s srewrite and dsrewrite commands are metarepresented by built-in functions metaSrewrite and metaDsrewrite; and
  • parsing and pretty-printing of a term in a module, as well as key sort operations such as comparing sorts in the subsort ordering of a signature, are also metarepresented by corresponding built-in functions.

The functions metaReduce, metaApply, metaXapply, metaRewrite, metaFrewrite, metaMatch, metaXmatch, metaSrewrite, and metaDsrewrite are called descent functions, since they allow us to descend levels in the reflective tower. The paper [28] provides a formal definition of the notion of descent function, and a detailed explanation of how they can be used to achieve a systematic, conservative way of lowering the levels of reflective computations.

The importation graph in Figure 17.1 shows the relationships between all the modules in the metalevel. The modules NAT-LIST and QID-LIST provide lists of natural numbers and quoted identifiers, respectively (see Section 7.13.1), and the module QID-SET provides sets of quoted identifiers (see Section 7.13.2). Notice that QID-SET is imported (in protecting mode) with renaming

 
(op empty to none, op _,_ to _;_ [prec 43])
     

17.2 The META-TERM module

17.2.1 Metarepresenting sorts and kinds

In the META-TERM module, sorts and kinds are metarepresented as data in specific subsorts of the sort Qid of quoted identifiers.

A term of sort Sort is any quoted identifier not containing the following characters: ‘:’, ‘.’, ‘[’, and ‘]’. Moreover, the characters ‘{’, ‘}’, and ‘,’ can only appear in structured sort names (see Section 3.3). For example, ’Bool, ’NzNat, a‘{X‘}, a‘{X‘,Y‘}, a‘{b‘,c‘{d‘}‘}‘{e‘}, and a‘{‘(‘} are terms of sort Sort.

An element of sort Kind is a quoted identifier of the form ’‘[SortList‘] where SortList is a single identifier formed by a list of unquoted elements of sort Sort separated by backquoted commas. For example, ’‘[Bool‘] and ’‘[NzNat‘,Zero‘,Nat‘] are valid elements of the sort Kind. Note the use of backquotes to force them to be single identifiers.

Since commas and square brackets are used to metarepresent kinds, these characters are forbidden in sort names, in order to avoid undesirable ambiguities. Periods and colons are also forbidden, due to the metarepresentation of constants and variables, as explained in the next section.

Since operator declarations can use both sorts and kinds, we denote by Type the union of Sort and Kind.

 
sorts Sort Kind Type . 
subsorts Sort Kind < Type < Qid. 
op <Qids> : -> Sort [special (...)] . 
op <Qids> : -> Kind [special (...)] .
     

Remember from the introduction of Chapter 7 that <Qids> is a special operator declaration used to represent sets of constants that are not algebraically constructed, but are instead associated with appropriate C++ code by “hooks” which are specified following the special attribute; see the functional module META-TERM in file prelude.maude for the details omitted here.

17.2.2 Metarepresenting terms

In the module META-TERM, terms are metarepresented as elements of the data type Term of terms. The base cases in the metarepresentation of terms are given by subsorts Constant and Variable of the sort Qid.

 
sorts Constant Variable Term . 
subsorts Constant Variable < Qid Term . 
op <Qids> : -> Constant [special (...)] . 
op <Qids> : -> Variable [special (...)] .
     

Constants are quoted identifiers that contain the constant’s name and its type separated by a ‘.’, e.g., ’0.Nat. Similarly, variables contain their name and type separated by a ‘:’, e.g., ’N:Nat. Appropriate selectors then extract their names and types.

 
op getName : Constant -> Qid . 
op getName : Variable -> Qid . 
op getType : Constant -> Type . 
op getType : Variable -> Type .
     

 
getName(’:-D:Smile) = ’:-D 
getType(’:-.|.‘[Smile‘]) = ’‘[Smile‘]
     

A term different from a constant or a variable is constructed in the usual way, by applying an operator symbol to a nonempty list of terms.

 
sorts NeTermList TermList . 
subsorts Term < NeTermList < TermList . 
op _,_ : TermList TermList -> TermList 
   [ctor assoc id: empty gather (e E) prec 121] . 
op _,_ : NeTermList TermList -> NeTermList [ctor ditto] . 
op _,_ : TermList NeTermList -> NeTermList [ctor ditto] . 
op _[_] : Qid NeTermList -> Term [ctor] .
     

The actual sort infrastructure provided by the module META-TERM is a bit more complex, because there are also subsorts and operators for the metarepresentation of ground terms and the corresponding lists of ground terms that we do not describe here (see the file prelude.maude for details).

Since terms in the module META-TERM can be metarepresented just as terms in any other module, the metarepresentation of terms can be iterated.

For example, the term c q M:Marking in the module VENDING-MACHINE in Section 5.1 is metarepresented by

 
’__[’c.Item, ’__[’q.Coin, ’M:Marking]]
     

 
’_‘[_‘][’’__.Qid, 
      ’_‘,_[’’c.Item.Constant, 
          ’_‘[_‘][’’__.Qid, 
                ’_‘,_[’’q.Coin.Constant, 
                     ’’M:Marking.Variable]]]]
     

Note that the metarepresentation of a natural number such as, e.g., 42 is ’s_^42[’0.Zero] instead of ’42.NzNat, since, as explained in Section 7.2, 42 is just syntactic sugar for s_^42(0).

17.3 The META-STRATEGY module: Metarepresenting the strategy language

All components of the strategy language described in Section 10, including its modules and views, can be manipulated at the metalevel. The META-STRATEGY module metarepresents all the strategy combinators as terms of the sort Strategy, with two subsorts, RuleApplication for rule applications, and CallStrategy for strategy calls.

 
ops fail idle all : -> Strategy [ctor] . 
op _[_]{_} : Qid Substitution StrategyList -> RuleApplication [ctor prec 21] . 
op top : RuleApplication -> Strategy [ctor] . 
op match_s.t._ : Term EqCondition -> Strategy [ctor prec 21] . 
op xmatch_s.t._ : Term EqCondition -> Strategy [ctor prec 21] . 
op amatch_s.t._ : Term EqCondition -> Strategy [ctor prec 21] . 
op _|_ : Strategy Strategy -> Strategy 
                      [ctor assoc comm id: fail prec 41 gather (e E)] . 
op _;_ : Strategy Strategy -> Strategy [ctor assoc id: idle prec 39 gather (e E)] . 
op _+ : Strategy -> Strategy [ctor] . 
op _?_:_ : Strategy Strategy Strategy -> Strategy [ctor prec 55] . 
op matchrew_s.t._by_ : Term EqCondition VarStratList -> Strategy [ctor] . 
op xmatchrew_s.t._by_ : Term EqCondition VarStratList -> Strategy [ctor] . 
op amatchrew_s.t._by_ : Term EqCondition VarStratList -> Strategy [ctor] . 
op _[[_]] : Qid TermList -> CallStrategy [ctor prec 21] . 
op one : Strategy -> Strategy [ctor] .
     

 
op empty : -> StrategyList [ctor] . 
op _,_ : StrategyList StrategyList -> StrategyList [ctor assoc id: empty] . 
op _using_ : Variable Strategy -> UsingPair [ctor prec 21] . 
op _,_ : UsingPairSet UsingPairSet -> UsingPairSet [ctor assoc comm prec 61] . 
eq U:UsingPair, U:UsingPair = U:UsingPair .
     

 
fmod META-CONDITION is 
 protecting META-TERM . 
 
 sorts EqCondition Condition . 
 subsort EqCondition < Condition . 
 op nil : -> EqCondition [ctor] . 
 op _=_ : Term Term -> EqCondition [ctor prec 71] . 
 op _:_ : Term Sort -> EqCondition [ctor prec 71] . 
 op _:=_ : Term Term -> EqCondition [ctor prec 71] . 
 op _=>_ : Term Term -> Condition [ctor prec 71] . 
 op _/\_ : EqCondition EqCondition -> EqCondition 
     [ctor assoc id: nil prec 73] . 
 op _/\_ : Condition Condition -> Condition 
     [ctor assoc id: nil prec 73] . 
endfm
     

The derived strategy combinators, explained in the last part of Section 10.1, are also defined as constructors. For efficiency purposes they are encoded internally in a special form, different from the encoding of their equivalent expressions.

 
op _or-else_ : Strategy Strategy -> Strategy [ctor assoc prec 43 gather (e E)] . 
op _* : Strategy -> Strategy [ctor] . 
op _! : Strategy -> Strategy [ctor] . 
op not : Strategy -> Strategy [ctor] . 
op test : Strategy -> Strategy [ctor] . 
op try : Strategy -> Strategy [ctor] .
     

For example, the metarepresentation of the strategy one(move * ; amatch (0)[nil]) for the HANOI example in Section 10 is

 
one(’move[none]{empty} * ; amatch ’‘(_‘)‘[_‘][’0.Zero, ’nil.NatList] s.t. nil)
     

17.4 The META-MODULE module: Metarepresenting modules

In the module META-MODULE, which imports META-TERM, functional, system and strategy modules, as well as functional, system and strategy theories, are metarepresented in a syntax very similar to their original user syntax.

The main differences are that:

1.

terms in equations, membership axioms, and rules are now metarepresented as we have already explained in Section 17.2.2;

2.

in the metarepresentation of modules and theories we follow a fixed order in introducing the different kinds of declarations for sorts, subsort relations, equations, etc., whereas in the user syntax there is considerable flexibility for introducing such different declarations in an interleaved and piecemeal way;

3.

there is no need for variable declarations—in fact, there is no syntax for metarepresenting them—and

4.

sets of identifiers—used in declarations of sorts—are metarepresented as sets of quoted identifiers built with an associative and commutative operator _;_.

The syntax for the top-level operators metarepresenting modules and theories is as follows, where Header means just an identifier in the case of non-parameterized modules or an identifier together with a list of parameter declarations in the case of a parameterized module.

 
sorts FModule SModule StratModule FTheory STheory StratTheory Module . 
subsorts FModule < SModule < Module . 
subsorts FTheory < STheory < Module . 
subsorts StratModule StratTheory < Module . 
sort Header . 
subsort Qid < Header . 
op _{_} : Qid ParameterDeclList -> Header [ctor] . 
op fmod_is_sorts_.____endfm : Header ImportList SortSet 
   SubsortDeclSet OpDeclSet MembAxSet EquationSet -> FModule 
   [ctor gather (& & & & & & &)] . 
op mod_is_sorts_._____endm : Header ImportList SortSet 
   SubsortDeclSet OpDeclSet MembAxSet EquationSet RuleSet 
   -> SModule [ctor gather (& & & & & & & &)] . 
op smod_is_sorts_._______endsm : Header ImportList SortSet 
   SubsortDeclSet OpDeclSet MembAxSet EquationSet RuleSet 
   StratDeclSet StratDefSet -> StratModule 
   [ctor gather (& & & & & & & & & &)] . 
op fth_is_sorts_.____endfth : Qid ImportList SortSet SubsortDeclSet 
   OpDeclSet MembAxSet EquationSet -> FTheory 
   [ctor gather (& & & & & & &)] . 
op th_is_sorts_._____endth : Qid ImportList SortSet SubsortDeclSet 
   OpDeclSet MembAxSet EquationSet RuleSet -> STheory 
   [ctor gather (& & & & & & & &)] . 
op sth_is_sorts_._______endsth : Qid ImportList SortSet 
   SubsortDeclSet OpDeclSet MembAxSet EquationSet RuleSet 
   StratDeclSet StratDefSet -> StratTheory 
   [ctor gather (& & & & & & & & & &)] .
     

 
op getName : Module -> Qid . 
op getImports : Module -> ImportList . 
op getSorts : Module -> SortSet . 
op getSubsorts : Module -> SubsortDeclSet . 
op getOps : Module -> OpDeclSet . 
op getMbs : Module -> MembAxSet . 
op getEqs : Module -> EquationSet . 
op getRls : Module -> RuleSet . 
op getStrats : Module -> StratDeclSet . 
op getSds : Module -> StratDefSet .
     

Without going into all the syntactic details, we show only the operators used to metarepresent sets of sorts and kinds, equations, rules and strategies. The complete syntax used for metarepresenting modules can be found in the module META-MODULE in the file prelude.maude. Conditions are defined in the module META-CONDITION shown in Section 17.3 .

 
sorts EmptyTypeSet NeSortSet NeKindSet 
    NeTypeSet SortSet KindSet TypeSet . 
subsort EmptyTypeSet < SortSet KindSet < TypeSet < QidSet . 
subsort Sort < NeSortSet < SortSet . 
subsort Kind < NeKindSet < KindSet . 
subsort Type NeSortSet NeKindSet < NeTypeSet < TypeSet NeQidSet . 
op none : -> EmptyTypeSet [ctor] . 
op _;_ : TypeSet TypeSet -> TypeSet 
   [ctor assoc comm id: none prec 43] . 
op _;_ : SortSet SortSet -> SortSet [ctor ditto] . 
op _;_ : KindSet KindSet -> KindSet [ctor ditto] . 
 
sorts Equation EquationSet . 
subsort Equation < EquationSet . 
op eq_=_[_]. : Term Term AttrSet -> Equation [ctor] . 
op ceq_=_if_[_]. : Term Term EqCondition AttrSet -> Equation 
   [ctor] . 
op none : -> EquationSet [ctor] . 
op __ : EquationSet EquationSet -> EquationSet 
   [ctor assoc comm id: none] . 
 
sorts Rule RuleSet . 
subsort Rule < RuleSet . 
op rl_=>_[_]. : Term Term AttrSet -> Rule [ctor] . 
op crl_=>_if_[_]. : Term Term Condition AttrSet -> Rule [ctor] . 
op none : -> RuleSet [ctor] . 
op __ : RuleSet RuleSet -> RuleSet [ctor assoc comm id: none] . 
 
sorts StratDecl StratDeclSet . 
subsort StratDecl < StratDeclSet . 
op strat_:_@_[_]. : Qid TypeList Type AttrSet -> StratDecl [ctor] . 
op none : -> StratDeclSet [ctor] . 
op __ : StratDeclSet StratDeclSet -> StratDeclSet [ctor assoc comm id: none] . 
 
sorts StratDefinition StratDefSet . 
subsort StratDefinition < StratDefSet . 
op sd_:=_[_]. : CallStrategy Strategy AttrSet -> StratDefinition [ctor] . 
op csd_:=_if_[_]. : CallStrategy Strategy EqCondition AttrSet 
     -> StratDefinition [ctor] . 
op none : -> StratDefSet [ctor] . 
op __ : StratDefSet StratDefSet -> StratDefSet [ctor assoc comm id: none] .
     

For example, we show here the metarepresentations of the modules introduced in Section 5.1 VENDING-MACHINE-SIGNATURE and VENDING-MACHINE.

 
fmod ’VENDING-MACHINE-SIGNATURE is 
 nil 
 sorts ’Coin ; ’Item ; ’Marking . 
 subsort ’Coin < ’Marking . 
 subsort ’Item < ’Marking . 
 op ’__ : ’Marking ’Marking -> ’Marking 
      [assoc comm id(’null.Marking)] . 
 op ’a : nil -> ’Item [format(’b! ’o)] . 
 op ’null : nil -> ’Marking [none] . 
 op ’$ : nil -> ’Coin [format(’r! ’o)] . 
 op ’q : nil -> ’Coin [format(’r! ’o)] . 
 op ’c : nil -> ’Item [format(’b! ’o)] . 
 none 
 none 
endfm
     

 
mod ’VENDING-MACHINE is 
 including ’VENDING-MACHINE-SIGNATURE . 
 sorts none . 
 none 
 none 
 none 
 none 
 rl ’M:Marking => ’__[’M:Marking, ’q.Coin] [label(’add-q)] . 
 rl ’M:Marking => ’__[’M:Marking, ’$.Coin] [label(’add-$)] . 
 rl ’$.Coin => ’c.Item [label(’buy-c)] . 
 rl ’$.Coin => ’__[’a.Item, ’q.Coin] [label(’buy-a)] . 
 rl ’__[’q.Coin, ’__[’q.Coin, ’__[’q.Coin, ’q.Coin]]] 
   => ’$.Coin [label(’change)] . 
endm
     

Since VENDING-MACHINE-SIGNATURE has no list of imported submodules, no membership axioms, and no equations, those fields are filled, respectively, with the constants nil of sort ImportList, none of sort MembAxSet, and none of sort EquationSet. Similarly, since the module VENDING-MACHINE has no subsort declarations and no operator declarations, those fields are filled, respectively, with the constants none of sort SubsortDeclSet and none of sort OpDeclSet. Variable declarations are not metarepresented, but rather each variable is metarepresented in its “on the fly”-declaration form, i.e., with its sort or kind.

As mentioned above, parameterized modules are also metarepresented through the notion of a header, which is either an identifier (for non-parameterized modules) or an identifier together with a list of parameter declarations (for parameterized modules). Such parameter declarations are metarepresented again with a syntax similar to the user syntax.

 
sorts ParameterDecl NeParameterDeclList ParameterDeclList . 
subsorts ParameterDecl < NeParameterDeclList < ParameterDeclList . 
op _::_ : Sort ModuleExpression -> ParameterDecl . 
op nil : -> ParameterDeclList [ctor] . 
op _,_ : ParameterDeclList ParameterDeclList -> ParameterDeclList 
   [ctor assoc id: nil prec 121] .
     

Module expressions involving renamings and summations can also be metarepresented with the expected syntax:

 
sort ModuleExpression . 
subsort Qid < ModuleExpression . 
op _+_ : ModuleExpression ModuleExpression -> ModuleExpression 
   [ctor assoc comm] . 
op _*(_) : ModuleExpression RenamingSet -> ModuleExpression 
   [ctor prec 39 format (d d s n++i n--i d)] . 
 
sorts Renaming RenamingSet . 
subsort Renaming < RenamingSet . 
op sort_to_ : Qid Qid -> Renaming [ctor] . 
op op_to_[_] : Qid Qid AttrSet -> Renaming 
   [ctor format (d d d d s d d d)] . 
op op_:_->_to_[_] : Qid TypeList Type Qid AttrSet -> Renaming 
   [ctor format (d d d d d d d d s d d d)] . 
op label_to_ : Qid Qid -> Renaming [ctor] . 
op strat_to_ : Qid Qid -> Renaming [ctor] . 
op strat_:_@_to_ : Qid TypeList Type Qid -> Renaming [ctor] . 
op _,_ : RenamingSet RenamingSet -> RenamingSet 
   [ctor assoc comm prec 43 format (d d ni d)] .
     

Finally, the instantiation of a parameterized module is metarepresented as follows:

 
op _{_} : ModuleExpression ParameterList -> ModuleExpression 
   [ctor prec 37]. 
 
sort EmptyCommaList NeParameterList ParameterList . 
subsorts Sort < NeParameterList < ParameterList . 
subsort EmptyCommaList < GroundTermList ParameterList . 
op empty : -> EmptyCommaList [ctor] . 
op _,_ : ParameterList ParameterList -> ParameterList [ctor ditto] .
     

The rules for constructing parameterized metamodules and instantiating parameterized modules existing in the database reflect the object-level rules. In particular, bound parameters are permitted; for example, the following term metarepresents a parameterized module:

 
fmod ’PARMODEX{’X :: ’TRIV} is 
 including ’MAP{’String, ’X} . 
 sorts ’Foo . 
 none 
 none 
 none 
 none 
endfm
     

Although, as we will see in the following section, views can be metarepresented as terms of the View sort, it is not possible to use the views constructed at the metalevel in module expressions. The views used in the module expressions occurring in metamodules must have been declared at the object level, so that they are present in the database of modules and views declared in the given session. Such views are written in quoted form within metamodule expressions, like ’String in ’MAP{’String, ’X} in the example above.

Note that terms of sort Module can be metarepresented again, yielding then a term of sort Term, and this can be iterated an arbitrary number of times. This is in fact necessary when a metalevel computation has to operate at higher levels.

17.5 The META-VIEW module: Metarepresenting views

In the module META-VIEW, which imports META-MODULE, views are metarepresented in a syntax very similar to their original user syntax.

 
sort View . 
op view_from_to_is___endv : Header ModuleExpression ModuleExpression 
   SortMappingSet OpMappingSet StratMappingSet -> View [ctor gather (& & & & & &) 
   format (d d d d d d d n++i ni ni n--i d)] .
     

The first argument corresponds to the name of the view, while the second and third are module expressions corresponding to the source (usually a theory) and target (usually a module) of the view, respectively. The fourth, fifth and sixth arguments are the sort, operator and strategy mappings defining the view.

The following syntax defines sets of sort mappings in a way completely similar to the user syntax.

 
sorts SortMapping SortMappingSet . 
subsort SortMapping < SortMappingSet . 
op sort_to_. : Sort Sort -> SortMapping [ctor] . 
op none : -> SortMappingSet [ctor] . 
op __ : SortMappingSet SortMappingSet -> SortMappingSet 
   [ctor assoc comm id: none format (d ni d)] . 
eq S:SortMapping S:SortMapping = S:SortMapping .
     

Analogously, the following syntax is used to define set of operator mappings and strategy mappings.

 
sorts OpMapping OpMappingSet . 
subsort OpMapping < OpMappingSet . 
op (op_to_.) : Qid Qid -> OpMapping [ctor] . 
op (op_:_->_to_.) : Qid TypeList Type Qid -> OpMapping [ctor] . 
op (op_to term_.) : Term Term -> OpMapping [ctor] . 
op none : -> OpMappingSet [ctor] . 
op __ : OpMappingSet OpMappingSet -> OpMappingSet 
   [ctor assoc comm id: none format (d ni d)] . 
eq O:OpMapping O:OpMapping = O:OpMapping . 
 
sorts StratMapping StratMappingSet . 
subsort StratMapping < StratMappingSet . 
op (strat_to_.) : Qid Qid -> StratMapping [ctor] . 
op (strat_:_@_to_.) : Qid TypeList Type Qid -> StratMapping [ctor] . 
op (strat_to-expr_.) : CallStrategy Strategy -> StratMapping [ctor] . 
op none : -> StratMappingSet [ctor] . 
op __ : StratMappingSet StratMappingSet -> StratMappingSet 
   [ctor assoc comm id: none format (d ni d)] . 
eq S:StratMapping S:StratMapping = S:StratMapping .
     

Finally, appropriate selectors are used to extract from the metarepresentation of a view the corresponding components, namely, the metarepresentations of its name, of its source, of its target, of its set of sort mappings, and of its set of operator mappings.

 
op getName : View -> Qid . 
op getFrom : View -> ModuleExpression . 
op getTo : View -> ModuleExpression . 
op getSortMappings : View -> SortMappingSet . 
op getOpMappings : View -> OpMappingSet . 
op getStratMappings : View -> StratMappingSet .
     

For example, the metarepresentation of the view RingToRat (see Section 6.3.2) from the theory RING to the predefined RAT module is as follows:

 
view ’RingToRat from ’RING to ’RAT is 
 sort ’Ring to ’Rat . 
 op ’z to ’0 . 
 op ’e.Ring to term ’s_[’0.Zero] . 
 none 
endv
     

 
Maude> reduce in META-VIEW : 
       getFrom(view ’RingToRat from ’RING to ’RAT is 
               sort ’Ring to ’Rat . 
               op ’z to ’0 . 
               op ’e.Ring to term ’s_[’0.Zero] . 
               none 
             endv) . 
result Sort: ’RING 
 
Maude> reduce in META-VIEW : 
       getOpMappings(view ’RingToRat from ’RING to ’RAT is 
                   sort ’Ring to ’Rat . 
                   op ’z to ’0 . 
                   op ’e.Ring to term ’s_[’0.Zero] . 
                   none 
                  endv) . 
result OpMappingSet: 
 op ’z to ’0 . 
 op ’e.Ring to term ’s_[’0.Zero] .
     

17.6 The META-LEVEL module: Metalevel operations

The META-LEVEL module, which imports META-VIEW, 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] .
     

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 (...)] .
     

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.

17.6.1 Moving between reflection levels: upModule, upTerm, downTerm, and others

For a module ℛ that has already been loaded into Maude, the operations upSorts, upSubsortDecl, upOpDecls, upMbs, upEqs, upRls, upStratDecls, upSds, and upModule take as arguments the metarepresentation of the name of ℛ and a Boolean value b, and return, respectively, the metarepresentations of the module ℛ, of its sorts, subsort declarations, operator declarations, membership axioms, equations, and rules. If the second argument of these functions is true, then the resulting metarepresentations will include the corresponding statements that ℛ imports from its submodules; but if the second argument is false, the resulting metarepresentations will only contain the metarepresentations of the statements explicitly declared in ℛ.

 
op upModule : Qid Bool ~> Module [special (...)] . 
op upSorts : Qid Bool ~> SortSet [special (...)] . 
op upSubsortDecls : Qid Bool ~> SubsortDeclSet [special (...)] . 
op upOpDecls : Qid Bool ~> OpDeclSet [special (...)] . 
op upMbs : Qid Bool ~> MembAxSet [special (...)] . 
op upEqs : Qid Bool ~> EquationSet [special (...)] . 
op upRls : Qid Bool ~> RuleSet [special (...)] . 
op upStratDecls : Qid Bool ~> StratDeclSet [special (...)] . 
op upSds : Qid Bool ~> StratDefSet [special (...)] .
     

We give below simple examples of using these functions. Note that, since BOOL is automatically imported by all modules, its equations are shown when upEqs is called with true as its second argument. For the same reason, the metarepresentation of the VENDING-MACHINE-SIGNATURE module includes an including declaration that was not explicit in that module. Here, and in the rest of this section, we assume that the modules NUMBERS and SIEVE from Chapter 4, as well as the modules VENDING-MACHINE-SIGNATURE and VENDING-MACHINE from Chapter 5, have already been loaded into Maude.

 
Maude> reduce in META-LEVEL : 
      upModule(’VENDING-MACHINE-SIGNATURE, false) . 
result FModule: 
 fmod ’VENDING-MACHINE-SIGNATURE is 
 including ’BOOL . 
 sorts ’Coin ; ’Item ; ’Marking . 
 subsort ’Coin < ’Marking . 
 subsort ’Item < ’Marking . 
 op ’$ : nil -> ’Coin [format(’r! ’o)] . 
 op ’__ : ’Marking ’Marking -> ’Marking 
      [assoc comm id(’null.Marking)] . 
 op ’a : nil -> ’Item [format(’b! ’o)] . 
 op ’c : nil -> ’Item [format(’b! ’o)] . 
 op ’null : nil -> ’Marking [none] . 
 op ’q : nil -> ’Coin [format(’r! ’o)] . 
 none 
 none 
endfm
     

 
Maude> reduce in META-LEVEL : upEqs(’VENDING-MACHINE, true) . 
result EquationSet: 
 eq ’_and_[’true.Bool, ’A:Bool] = ’A:Bool [none] . 
 eq ’_and_[’A:Bool, ’A:Bool] = ’A:Bool [none] . 
 eq ’_and_[’A:Bool, ’_xor_[’B:Bool, ’C:Bool]] 
   = ’_xor_[’_and_[’A:Bool, ’B:Bool], ’_and_[’A:Bool, ’C:Bool]] 
   [none] . 
 eq ’_and_[’false.Bool, ’A:Bool] = ’false.Bool [none] . 
 eq ’_or_[’A:Bool,’B:Bool] 
   = ’_xor_[’_and_[’A:Bool, ’B:Bool],’_xor_[’A:Bool, ’B:Bool]] 
   [none] . 
 eq ’_xor_[’A:Bool, ’A:Bool] = ’false.Bool [none] . 
 eq ’_xor_[’false.Bool, ’A:Bool] = ’A:Bool [none] . 
 eq ’not_[’A:Bool] = ’_xor_[’true.Bool, ’A:Bool] [none] . 
 eq ’_implies_[’A:Bool, ’B:Bool] 
   = ’not_[’_xor_[’A:Bool, ’_and_[’A:Bool, ’B:Bool]]] [none] .
     

 
Maude> reduce in META-LEVEL : upEqs(’VENDING-MACHINE, false) . 
result EquationSet: (none).EquationSet
     

 
Maude> reduce in META-LEVEL : upRls(’VENDING-MACHINE, true) . 
result RuleSet: 
 rl ’$.Coin => ’c.Item [label(’buy-c)] . 
 rl ’$.Coin => ’__[’q.Coin,’a.Item] [label(’buy-a)] . 
 rl ’M:Marking => ’__[’$.Coin,’M:Marking] [label(’add-$)] . 
 rl ’M:Marking => ’__[’q.Coin,’M:Marking] [label(’add-q)] . 
 rl ’__[’q.Coin,’q.Coin,’q.Coin,’q.Coin] => ’$.Coin 
   [label(’change)] .
     

In addition to the upModule operator, there is another operator allowing the use of an already loaded module at the metalevel. This operator is defined in the module META-MODULE as follows:

 
op [_] : Qid -> Module . 
eq [Q:Qid] = (sth Q:Qid is including Q:Qid . 
          sorts none . none none none none none none none endsth) .
     

This operator is just syntactic sugar for accessing the corresponding module. Notice that the module is not moved up to the metalevel as upModule does, it is just a way of referring to it, and therefore more efficient.

The META-LEVEL module also provides a function upImports that takes as argument the metarepresentation of the name of a module ℛ . When ℛ is already in the Maude module database, then upImports returns the metarepresentation of its list of imported submodules. The function upImports does not take a Boolean argument, as the previous up-functions, since it is not useful to ask for the list of imported submodules of a flattened module.

 
op upImports : Qid ~> ImportList [special (...)] .
     

In the same way, the META-LEVEL module provides a function upView that takes as argument the metarepresentation of the name of a view; when such a view is in the Maude view database, then upView returns the corresponding metarepresentation.

 
op upView : Qid ~> View [special (...)] .
     

As a simple example, let us consider the view String0 from the predefined theory DEFAULT to the predefined module STRING, all of them provided in prelude.maude; then,

 
Maude> reduce in META-LEVEL : upView(’String0) . 
result View: 
 view ’String0 from ’DEFAULT to ’STRING is 
   sort ’Elt to ’String . 
   op ’0.Elt to term ’"".String . 
 endv