The META-MODULE module: Metarepresenting modules

In the module META-MODULE, which imports META-TERM, functional and system modules, as well as functional and system 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 11.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 functional and system modules and functional and system theories (just modules in general) 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 FTheory STheory Module .
  subsorts FModule < SModule < Module .
  subsorts FTheory < STheory < 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 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 (& & & & & & & &)] .

Appropriate selectors then extract from the metarepresentation of modules the metarepresentations of their names, imported submodules, and declared sorts, subsorts, operators, memberships, equations, and rules.

  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 .

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

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

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

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 _,_ : 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

Views are not reflected; there are no metaviews and no way to construct new views or inspect existing views at the metalevel. Therefore, 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.