***(

    This file is part of the Maude 2 interpreter.

    Copyright 1997-2003 SRI International, Menlo Park, CA 94025, USA.

    This program is free software; you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
    the Free Software Foundation; either version 2 of the License, or
    (at your option) any later version.

    This program is distributed in the hope that it will be useful,
    but WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
    GNU General Public License for more details.

    You should have received a copy of the GNU General Public License
    along with this program; if not, write to the Free Software
    Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307, USA.

)

***
***                                        Full Maude specification version 2.0
***
*** last modification: June 6th, 2003
*** author: Francisco Duran
*** 
*** Last changes:
***
*** - The lazy evaluation of modules is working. When a module is redefined 
***   its dependent modules are removed only if generated internally. Those 
***   introduced by the user save their term representation, from which the
***   whole processing can take place. They will be recompiled by need.
***
*** - Bugs fixed: 
***
***   - memberships in conditions are now correctly handled (thanks go to
***     Manolo and Miguel)
***
***   - kinds can now appear in op decl (thanks Manolo)
***
***   - and many others (thanks go to Steven, Peter, Dilia, Nirman, ...)
***
*** - The form of qualifying sorts coming from the parameters in 
***   parameterized modules has changed AGAIN: The sort Elt coming from 
***   X :: TRIV is now written as X@Elt (Note that sort names cannot contain
***   dots anymore). 
***
*** - Parameters are enclosed in parentheses (Note that square brackets
***   are now used for kinds, the unbiguity is unavoidable). Thus, for example,
***   now a module LIST(X :: TRIV) can have a sort List(X). If there are 
***   multiple parameters, these must be separated by a vertical bar (|),
***   instead of a comma. Commas are forbidden inside sort names because
***   they are used as part of the syntax for kinds. And to be consistent we 
***   do the same for defining module interfaces. Thus, a module 
***   PAIR(X :: TRIV, Y :: TRIV) is now written PAIR(X :: TRIV | Y :: TRIV), 
***   and a sort Pair(X, Y) in it as Pair(X | Y).
***   Note that | is not an special character, and therefore the white spaces
***   around it are important. Note that inside terms ---in membership axioms
***   and qualifications--- qualified sorts must appear in their equivalent
***   single identifier form. That is, Pair(X | Y) should be used in these 
***   cases as Pair`(X`|`Y`). The metarepresentation of this sort is 
***   'Pair`(X`|`Y`).
***
*** - Tuples are built with the syntax TUPLE[size](|_separated_list_of_views). 
***   For example, given a view Nat from TRIV to NAT we can define pairs of 
***   nats with TUPLE[2](Nat | Nat).
***
*** - The model-checker is loaded before the full maude modules, so that 
***   it can be used. 
***
*** - match, xmatch, search and frewrite work.
***
*** - The syntax for red and rew is finally as their syntax in Maude, i.e,
***   one can now write things like (rew [2] in FOO : foo .).
***
*** - Statements attributes (metadata and label) and the new syntax for 
***   statements in supported.
***
*** - The general case of conditions is handled.
***
*** - ~> supported.
***
*** - Kinds handled.
***
*** - The format, iter, and frozen attributes are supported.
***
*** - Object-oriented modules include a module CONFIGURATION+, which 
***   imports CONFIGURATION, defines a function
***     op class : Object -> Cid .
***   returning the actual class of the given object, and add syntax
***   for objects with no attributes <_:_| >. Classes without attributes
***   are defined with syntax class CLASS-NAME .
***
*** Things to come:
***
*** - Commands missing: continue ...
***
*** - On parameterized theories and views: linked parameters, composed and 
***   lifted views, and default views.
***
*** - The ditto attribute is not correctly handled.
***
*** - ops names in op declarations
***
*** known bugs:
***
*** - Check: possibly it's necessary to convert ctes back into vbles in 
***   procViewAux
***
*** - Parameterized sorts don't work in sort constraints (nor by themselves,
***   nor in the conditions of axioms. They are accepted in their equivalent
***   single token form but do not get instantiated
***     cmb (A, B) S : PFun(X, Y) if not(A in dom(S)) /\ S : PFun`(X`,Y`) .
***
*** Internal changes to be done:
***
*** - correct treatment of error terms
***
*** - perhaps should be good to distinguish between modules and premodules

load model-checker

*******************************************************************************
***
*** 2 The Signature of Full Maude
***
*******************************************************************************

fmod EXTENDED-SORTS is
  sorts SortToken ViewToken 
        Sort Kind Type SortList TypeList ViewExp ModExp .
        
  subsorts SortToken < Sort < SortList < TypeList .
  subsorts Sort Kind < Type < TypeList .
  subsort ViewToken < ViewExp .

  op _`(_`) : Sort ViewExp -> Sort [prec 40] .
  op __ : SortList SortList -> SortList [assoc] .
  op __ : TypeList TypeList -> TypeList [assoc] .
  op `[_`] : Sort -> Kind .

  op _|_ : ViewExp ViewExp -> ViewExp [assoc] .
  op _;_ : ViewExp ViewExp -> ViewExp [assoc] .
  op _`{_`} : ModExp ViewExp -> ViewExp .
  op _`(_`) : ViewExp ViewExp -> ViewExp [prec 40] .
endfm

******************************************************************************

fmod OPERATOR-ATTRIBUTES is
  sorts Attr AttrList Hook HookList Bubble Token NeTokenList .
  subsort Attr < AttrList .
  subsort Hook < HookList .

  op __ : AttrList AttrList -> AttrList [assoc] .
  ops assoc associative : -> Attr .
  ops comm commutative : -> Attr .
  ops idem idempotent : -> Attr .
  ops id:_ identity:_ : Bubble -> Attr .
  ops left`id:_ left`identity:_ : Bubble -> Attr .
  ops right`id:_ right`identity:_ : Bubble -> Attr .
  ops frozen`(_`) strat`(_`) strategy`(_`) : NeTokenList -> AttrList .
  ops memo memoization : -> Attr .
  ops prec_ precedence_ : Token -> Attr .
  ops gather`(_`) gathering`(_`) : NeTokenList -> Attr .
  ops format`(_`) : NeTokenList -> Attr .
  ops ctor constructor : -> Attr .
  ops ditto iter : -> Attr .

  op special`(_`) : HookList -> Attr .
  op __ : HookList HookList -> HookList [assoc] .
  op id-hook_ : Token -> Hook .
  op id-hook_`(_`) : Token NeTokenList -> Hook .
  op op-hook_`(_:_->_`) : Token Token NeTokenList Token -> Hook .
  op op-hook_`(_:`->_`) : Token Token Token -> Hook .
  op op-hook_`(_:_~>_`) : Token Token NeTokenList Token -> Hook .
  op op-hook_`(_:`~>_`) : Token Token Token -> Hook .
  op term-hook_`(_`) : Token Bubble -> Hook .
endfm

*******************************************************************************

fmod MOD-EXPRS is
  including OPERATOR-ATTRIBUTES .
  including EXTENDED-SORTS .

  sorts Map MapList .
  subsort Map < MapList .
  subsorts Token < ModExp .

  *** module expression
  op _*`(_`) : ModExp MapList -> ModExp .
  op _`(_`) : ModExp ViewExp -> ModExp .
  op TUPLE`[_`] : Token -> ModExp .
  op _+_ : ModExp ModExp -> ModExp [assoc prec 42] .

  *** renaming maps
  op op_to_ : Token Token -> Map .
  op op_:_->_to_ : Token TypeList Type Token -> Map .
  op op_: ->_to_ : Token Type Token -> Map .
  op op_to_`[_`] : Token Token AttrList -> Map .
  op op_:_->_to_`[_`] : Token TypeList Type Token AttrList -> Map .
  op op_:`->_to_`[_`] : Token Type Token AttrList -> Map .
  op sort_to_ : Sort Sort -> Map .
  op label_to_ : Token Token -> Map .
  op class_to_ : Sort Sort -> Map .
  op attr_._to_ : Token Sort Token -> Map .
  op msg_to_ : Token Token -> Map .
  op msg_:_->_to_ : Token TypeList Type Token -> Map .
  op msg_:`->_to_ : Token Type Token -> Map .

  op _`,_ : MapList MapList -> MapList [assoc prec 42] .
endfm

*******************************************************************************

fmod SIGNATURES is
  inc MOD-EXPRS .

  sorts SortDecl SubsortRel SubsortDecl OpDecl .

  op `(_`) : Token -> Token .

  *** sort declaration
  op sorts_. : SortList -> SortDecl .
  op sort_. : SortList -> SortDecl .

  *** subsort declaration
  op subsort_. : SubsortRel -> SubsortDecl .
  op subsorts_. : SubsortRel -> SubsortDecl .
  op _<_ : SortList SortList -> SubsortRel .
  op _<_ : SortList SubsortRel -> SubsortRel .

  *** operator declaration
  op op_:`->_. : Token Type -> OpDecl .
  op op_:`->_`[_`]. : Token Type AttrList -> OpDecl .
  op op_:_->_. : Token TypeList Type -> OpDecl .
  op op_:_->_`[_`]. : Token TypeList Type AttrList -> OpDecl .
  op ops_:`->_. : NeTokenList Type -> OpDecl .
  op ops_:`->_`[_`]. : NeTokenList Type AttrList -> OpDecl .
  op ops_:_->_. : NeTokenList TypeList Type -> OpDecl .
  op ops_:_->_`[_`]. : NeTokenList TypeList Type AttrList -> OpDecl .

  op op_:`~>_. : Token Sort -> OpDecl .
  op op_:`~>_`[_`]. : Token Sort AttrList -> OpDecl .
  op op_:_~>_. : Token TypeList Sort -> OpDecl .
  op op_:_~>_`[_`]. : Token TypeList Sort AttrList -> OpDecl .
  op ops_:`~>_. : NeTokenList Sort -> OpDecl .
  op ops_:`~>_`[_`]. : NeTokenList Sort AttrList -> OpDecl .
  op ops_:_~>_. : NeTokenList TypeList Sort -> OpDecl .
  op ops_:_~>_`[_`]. : NeTokenList TypeList Sort AttrList -> OpDecl .
endfm

*******************************************************************************

fmod F&S-MODS&THS is
  including SIGNATURES .

  sorts FDeclList SDeclList Module ImportDecl Parameter List`(Parameter`) 
        EqDecl RlDecl MbDecl VarDecl VarDeclList .

  subsort VarDecl < VarDeclList .
  subsorts VarDecl ImportDecl SortDecl SubsortDecl OpDecl MbDecl EqDecl 
           VarDeclList < FDeclList .
  subsorts RlDecl FDeclList < SDeclList .

  *** variable declaration
  op vars_:_. : NeTokenList Type -> VarDecl .
  op var_:_. : NeTokenList Type -> VarDecl .

  *** membership axiom declaration
  op mb_:_. : Bubble Sort -> MbDecl .
  op cmb_:_if_. : Bubble Sort Bubble -> MbDecl . 

  *** equation declaration
  op eq_=_. : Bubble Bubble -> EqDecl .
  op ceq_=_if_. : Bubble Bubble Bubble -> EqDecl .
  op cq_=_if_. : Bubble Bubble Bubble -> EqDecl .

  *** rule declaration
  *** op rl`[_`]:_=>_. : Token Bubble Bubble -> RlDecl .
  op rl_=>_. : Bubble Bubble -> RlDecl .
  *** op crl`[_`]:_=>_if_. : Token Bubble Bubble Bubble -> RlDecl .  
  op crl_=>_if_. : Bubble Bubble Bubble -> RlDecl .  

  *** importation declaration
  ops including_. inc_. : ModExp -> ImportDecl .
  ops protecting_. pr_. : ModExp -> ImportDecl .

  sorts Interface .
  subsort Parameter < List`(Parameter`) .
  subsorts Token < Interface .

  *** parameterized module interface
  op _::_ : Token ModExp -> Parameter [prec 40 gather (e &)] .
  op _::_ : Token Interface -> Parameter [prec 40 gather (e &)] .

  op _|_ : List`(Parameter`) List`(Parameter`) -> List`(Parameter`) [assoc] .

  ***op _`(_`) : Token List`(Parameter`) -> Interface .
  op _`(_`) : ModExp List`(Parameter`) -> Interface .

  *** declaration list
  op __ : VarDeclList VarDeclList -> VarDeclList [assoc] .
  op __ : SDeclList SDeclList -> SDeclList [assoc] .
  op __ : FDeclList FDeclList -> FDeclList [assoc] .

  *** functional and system module and theory
  op fmod_is_endfm : Interface FDeclList -> Module .
  op obj_is_jbo : Interface FDeclList -> Module .
  op obj_is_endo : Interface FDeclList -> Module .
  op mod_is_endm : Interface SDeclList -> Module .
  op fth_is_endfth : Interface FDeclList -> Module .
  op th_is_endth : Interface SDeclList -> Module .
endfm

*******************************************************************************

fmod O-MODS&THS is
  including F&S-MODS&THS .

  sorts ClassDecl AttrDecl AttrDeclList SubclassDecl MsgDecl ODeclList .
  subsorts SDeclList MsgDecl SubclassDecl ClassDecl < ODeclList .
  subsort AttrDecl < AttrDeclList .

  op __ : ODeclList ODeclList -> ODeclList [assoc] .

  *** object-oriented module and theory
  op omod_is_endom : Interface ODeclList -> Module .
  op oth_is_endoth : Interface ODeclList -> Module .

  *** class declaration
  op class_|_. : Sort AttrDeclList -> ClassDecl .
  op class_. : Sort -> ClassDecl .
  op _`,_ : AttrDeclList AttrDeclList -> AttrDeclList [assoc] .
  op _:_ : Token Sort -> AttrDecl [prec 40] .

  *** subclass declaration
  op subclass_. : SubsortRel -> SubclassDecl .
  op subclasses_. : SubsortRel -> SubclassDecl .

  *** message declaration
  op msg_:_->_. : Token SortList Sort -> MsgDecl .
  op msgs_:_->_. : NeTokenList SortList Sort -> MsgDecl .
  op msg_:`->_. : Token Sort -> MsgDecl .
  op msgs_:`->_. : NeTokenList Sort -> MsgDecl .
endfm

*******************************************************************************

fmod VIEWS is
  including O-MODS&THS .

  sorts ViewDecl ViewDeclList View .
  subsorts VarDecl < ViewDecl < ViewDeclList .
  subsort VarDeclList < ViewDeclList .

  *** view maps
  op op_to`term_. : Bubble Bubble -> ViewDecl .
  op op_to_. : Token Token -> ViewDecl .
  op op_:_->_to_. : Token TypeList Type Token -> ViewDecl .
  op op_:`->_to_. : Token Type Token -> ViewDecl .
  op sort_to_. : Sort Sort -> ViewDecl .
  op class_to_. : Sort Sort -> ViewDecl .
  op attr_._to_. : Token Sort Token -> ViewDecl .
  op msg_to_. : Token Token -> ViewDecl .
  op msg_:_->_to_. : Token TypeList Type Token -> ViewDecl .
  op msg_:`->_to_. : Token Type Token -> ViewDecl .

  *** view
  op view_from_to_is_endv : Interface ModExp ModExp ViewDeclList -> View .
  op __ : ViewDeclList ViewDeclList -> ViewDeclList [assoc] .
endfm

*******************************************************************************

fmod COMMANDS is
  including MOD-EXPRS .

  sorts Command .

  *** down function
  op down_:_ : ModExp Command -> Command .

  *** reduce commands
  op red_. : Bubble -> Command .
  op reduce_. : Bubble -> Command .

  *** rewrite commands
  op rew_. : Bubble -> Command .
  op rewrite_. : Bubble -> Command .

  *** frewrite commands
  op frew_. : Bubble -> Command .
  op frewrite_. : Bubble -> Command .

  *** search commands
  op search_=>_. : Bubble Bubble -> Command .
  op search_=>*_. : Bubble Bubble -> Command .
  op search_=>+_. : Bubble Bubble -> Command .
  op search_=>!_. : Bubble Bubble -> Command .

  *** matching commands
  op match_<=?_. : Bubble Bubble -> Command .
  op xmatch_<=?_. : Bubble Bubble -> Command .

  *** select command
  op select_. : ModExp -> Command .

  *** show commands
  op show`module`. : -> Command .
  op show`module_. : ModExp -> Command .
  op show`all`. : -> Command .
  op show`all_. : ModExp -> Command .
  op show`sorts`. : -> Command .
  op show`sorts_. : ModExp -> Command .
  op show`ops`. : -> Command .
  op show`ops_. : ModExp -> Command .
  op show`mbs`. : -> Command .
  op show`mbs_. : ModExp -> Command .
  op show`eqns`. : -> Command .
  op show`eqns_. : ModExp -> Command .
  op show`rls`. : -> Command .
  op show`rls_. : ModExp -> Command .
  op show`view_. : ViewExp -> Command .
  op show`modules`. : -> Command .
  op show`views`. : -> Command .
endfm

*******************************************************************************

fmod FULL-MAUDE-SIGN is
  including VIEWS .
  including COMMANDS .
  sort Input .
  subsorts Command Module View < Input .
endfm

*******************************************************************************

*** As explained in Section~\ref{bubbles}, to parse some input using the
*** built-in function \texttt{metaParse}, we need to give the
*** metarepresentation of the signature in which the input is going to be 
*** parsed.

*** But we do not need to give the complete metarepresentation of such a
*** module. As we saw in Section~\ref{bubbles}, in modules including
*** \texttt{META-LEVEL} it is possible to define terms of sort \texttt{Module}
*** that import built-in modules or any module introduced at the ``object
*** level'' of Core Maude. In this way, it is possible to get the equivalent
*** effect of having the explicit metarepresentation of a module by declaring
*** a constant and adding an equation identifying such a constant with the 
*** metarepresentation of an extended module that imports the original module 
*** at the object level.

*** As also mentioned in Section~\ref{bubbles}, the declaration of
*** constructors for bubble sorts at the object level is not supported in the
*** current version of Core Maude. The \texttt{special} attributes linking the
*** constructors for the bubble sorts to the built-in ones are only supported
*** at the metalevel, that is, the declarations of the constructor operators 
*** for bubble sorts have to be given in the metarepresentation of a module.

*** To allow the greatest generality and flexibility in future extensions of
*** Full Maude, we have declared its signature as a module
*** \texttt{FULL-MAUDE-SIGN}\ (see Appendix~\ref{signature-full-maude}). Then,
*** in the following module \texttt{META-FULL-MAUDE-SIGN} we declare a
*** constant \texttt{GRAMMAR} of sort \texttt{FModule}, and using the
*** technique described in Section~\ref{bubbles} to import the
*** metarepresentation of a module by name, we give an equation identifying
*** such constant with the metarepresentation of a module \texttt{GRAMMAR} in
*** which there is a declaration importing \texttt{FULL-MAUDE-SIGN}.
*** Declarations for the constructors of the bubble sorts are also included in
*** this module. Note that the bubble sorts \texttt{Token}, \texttt{Bubble},
*** \texttt{SortToken}, and \texttt{NeTokenList} are declared in the module 
*** \texttt{SIGN\&VIEW-EXPR}, which is imported by \texttt{FULL-MAUDE-SIGN}. 
*** These sorts are used in the declarations describing the syntax of the 
*** system.

fmod META-FULL-MAUDE-SIGN is
  including META-LEVEL .

  op GRAMMAR : -> FModule .

  eq GRAMMAR
    = (fmod 'GRAMMAR is
        including 'QID-LIST .
        including 'FULL-MAUDE-SIGN .
        sorts none .
        none
        op 'token : 'Qid -> 'Token 
             [special(
               (id-hook('Bubble, '1 '1)
                op-hook('qidSymbol, '<Qids>, nil, 'Qid)))] .
        op 'viewToken : 'Qid -> 'ViewToken 
             [special(
               (id-hook('Bubble, '1 '1)
                op-hook('qidSymbol, '<Qids>, nil, 'Qid)))] .
        op 'sortToken : 'Qid -> 'SortToken 
             [special(
               (id-hook('Bubble, '1 '1)
                op-hook('qidSymbol, '<Qids>, nil, 'Qid)
                id-hook('Exclude, '`[ '`] '< 'to ': '`, '. '`( '`)  '|
                                  'ditto 'precedence 'prec 'gather 
                                  'assoc 'associative 'comm 'commutative 
                                  'ctor 'constructor 'id: 'strat 'strategy 
                                  'memo 'memoization 'iter 'frozen)))] .
        op 'neTokenList : 'QidList -> 'NeTokenList 
             [special(
               (id-hook('Bubble, '1 '-1 '`( '`))
                op-hook('qidListSymbol, '__, 'QidList 'QidList, 'QidList)
                op-hook('qidSymbol, '<Qids>, nil, 'Qid)
                id-hook('Exclude, '.)))] .
        op 'bubble : 'QidList -> 'Bubble 
             [special(
               (id-hook('Bubble, '1 '-1 '`( '`))
                op-hook('qidListSymbol, '__, 'QidList 'QidList, 'QidList)
                op-hook('qidSymbol, '<Qids>, nil, 'Qid)))] .
        none
        none
     endfm) .
endfm

*******************************************************************************

*** The \texttt{GRAMMAR} module will be used in calls to the \texttt{metaParse}
*** function in order to get the input parsed in this signature. Note that
*** this module is not the data type in which we shall represent the inputs.
*** From the call to \texttt{metaParse} we shall get a term representing the
*** parse tree of the input. This term will then be transformed into terms of 
*** other appropriate data types if necessary.

*** Future extensions to Full Maude will require extending the signature as
*** well. The addition of new commands, new module expressions, or additions
*** of any other kind will require adding new declarations to the present Full
*** Maude signature and defining the corresponding extensions to the data
*** types and functions to deal with the new cases introduced by the
*** extensions. We shall see in Section~\ref{extension} how the system can be
*** easily extended to handle some new module expressions in addition to the
*** renaming and instantiation module expressions presented in
*** Section~\ref{module-expressions} and further discussed in
*** Sections~\ref{renaming} and~\ref{instantiation}. In Chapter~\ref{crc} we 
*** shall explain how to combine a proving tool like a Church-Rosser 
*** checker~\cite{ClavelDuranEkerMeseguer98a,ClavelDuranEkerMeseguer98} with 
*** Full Maude.

*** 
*** The Abstract Data Type \texttt{Unit}
*** 

*** In this section we present the abstract data type \texttt{Unit}, which can
*** be seen as an extension of the predefined sort \texttt{Module} in several
*** ways. There are constructors for functional, system, and object-oriented
*** modules and theories, which can be parameterized and can import module
*** expressions. There can also be parameterized sorts in Full Maude modules,
*** and therefore, the constructors for the different declarations that can 
*** appear in a module have to be appropriately extended.

*** The section is structured as follows. After introducing some modules
*** defining some functions on the predefined sorts \texttt{Bool} and
*** \texttt{QidList} in Section~\ref{BOOL-QID-LIST}, we present in
*** Sections~\ref{EXT-SORT} and~\ref{EXT-DECL} the data types for extended
*** sorts and extended declarations. In Section~\ref{mod-exp-mod-id} we 
*** introduce module expressions and module names, and in 
*** Section~\ref{unitADT} the abstract data type \texttt{Unit} itself.

*** 
*** Extensions to \texttt{BOOL} and \texttt{QID-LIST}
***

*** The module \texttt{EXT-BOOL} extends the predefined \texttt{BOOL} module
*** with operations \verb~_and-then_~ and \verb~_or-else_~. The semantics of
*** \verb~_and-then_~ and \verb~_or-else_~ are, respectively, as the semantics
*** of the boolean operators \verb~_and_~ and \verb~_or_~, but they are not
*** declared to be associative, and their second arguments are evaluated
*** lazily thanks to the evaluation strategy \verb~(1 0 2 0)~ (see
*** \cite{OBJ92,Eker98,ClavelDuranEkerLincolnMarti-OlietMeseguerQuesada99} for 
*** more on evaluation strategies).
*** 
*** fmod EXT-BOOL is
***   pr BOOL .
*** 
***   op _and-then_ : Bool [Bool] -> Bool [assoc strat (1 0 2 0) prec 55] .
***   op _or-else_ : Bool [Bool] -> Bool [assoc strat (1 0 2 0) prec 59] .
*** 
***   var B : [Bool] .
*** 
***   eq true and-then B = B .
***   eq false and-then B = false .
***   eq true or-else B = true .
***   eq false or-else B = B .
*** endfm

*******************************************************************************

fmod EXT-QID is
  pr QID .
  pr CONVERSION .

  op conc : Qid Qid -> Qid .
  op index : Qid Int -> Qid .
  op strip : Qid -> Qid .
  op convert : Qid ~> Int .
  op _<_ : Qid Qid -> Bool .

  vars Q P : Qid .
  var M : Int .

  eq conc(Q, P) = qid(string(Q) + string(P)) .
  eq index(Q, M) = qid(string(Q) + string(M, 10)) .
  eq strip(Q) = qid(substr(string(Q), 1, length(string(Q)))) .
  eq convert(Q) = trunc(rat(string(Q), 10)) .
  eq Q < P = string(Q) < string(P) .
endfm

*******************************************************************************

*** The conversion of lists of quoted identifiers into single quoted 
*** identifiers by concatenating them is heavily used in the coming modules.
*** This is the task of the \texttt{qidListToQid} function, which is
*** introduced in the following module \texttt{EXT-QID-LIST} extending the 
*** predefined module \texttt{QID-LIST}.

fmod EXT-QID-LIST is
  pr EXT-QID .
  pr QID-LIST .

  op qidListToQid : QidList -> Qid .

  var QI : Qid .
  var QIL : QidList .

  eq qidListToQid((QI QIL)) 
    = qid(string(QI) + " " + string(qidListToQid(QIL))) .
  eq qidListToQid(nil) = qid("") .
endfm

*******************************************************************************

*** 3.2 View Expressions and Extended Sorts

*** To allow the use of parameterized sorts, or sorts qualified by the view
*** expression with which the parameterized module in which the given sorts
*** appear is instantiated, we add the sort ESort of ``extended sorts'' as a
*** supersort of the predefined sort Sort.  View expressions and extended 
*** sorts are introduced in the following modules.

*** 3.2.1 View Expressions

*** A view expression is given by a single quoted identifier, by a sequence of
*** view expressions (at the user level, separated by commas), or by the
*** composition of view expressions. In the current version, the composition
*** of view expressions is only used internally; we plan to make it available
*** to the user with syntax \verb~_;_~ in the future. View expressions are
*** used in the instantiation of parameterized modules and in parameterized
*** sorts.  We plan to support parameterized views in the future as well. We 
*** use operators \verb~_|_~ and \verb~_;;_~ to represent, respectively, 
*** sequences and composition of view expressions.

*** The \texttt{VIEW-EXPR} module below also includes declarations for sets of
*** view expressions, which will be used in the database structure to hold the
*** list of the names of the views in it. The elements of sort
*** \texttt{ViewExpSet}, for sets of view expressions, are given using the
*** constructor \verb~_#_~, which is declared to be associative, commutative, 
*** and with identity element \texttt{noneViewExpSet}.

*** The function \verb~_inViewExpSet_~ checks whether the view expression given
*** as first argument is in the set of view expressions given as second 
*** argument or not.

fmod VIEW-EXPR is
  pr EXT-BOOL .
  pr QID .

  sort ViewExp .
  subsort Qid < ViewExp .
  op nullViewExp : -> ViewExp .
  op _|_ : ViewExp ViewExp -> ViewExp             *** view sequence      _|_
      [assoc id: nullViewExp] .
  op _;;_ : ViewExp ViewExp -> ViewExp [assoc] .  *** view composition   _;_
  op _<<_>> : Qid ViewExp -> ViewExp [prec 40] .  *** view instantiation _(_)
  op _`{_`} : Qid ViewExp -> ViewExp .            *** view lifting       _{_}

  sort ViewExpSet .
  subsort ViewExp < ViewExpSet .
  op noneViewExpSet : -> ViewExpSet .
  op _#_ : ViewExpSet ViewExpSet -> ViewExpSet 
      [assoc comm id: noneViewExpSet] .

  vars VE VE' : ViewExp .
  vars VES : ViewExpSet .

  op _inViewExpSet_ : ViewExp ViewExpSet -> Bool .

  eq VE inViewExpSet (VE' # VES) = (VE == VE') or-else (VE inViewExpSet VES) .
  eq VE inViewExpSet noneViewExpSet = false .

endfm

*******************************************************************************

*** Since the Core Maude engine does not know about view expressions, or, as we
*** shall see, about extended sorts, extended module expressions, extended
*** modules, and other declarations that we introduce, to be able to use them
*** with built-in functions such as \texttt{sameComponent}, \texttt{leastSort},
*** \texttt{metaReduce}, etc., we shall have to convert them into terms which
*** only use the built-in constructors.  Thus, for example, view expressions
*** in sort \texttt{ViewExp} will be converted into quoted identifiers of sort
*** \texttt{Qid} by means of function \texttt{viewExpToQid}, or, similarly,
*** elements of sorts \texttt{ESort}, \texttt{ESortList}, and \texttt{ESortSet}
*** are transformed into elements of sorts \texttt{Qid}, \texttt{QidList}, and 
*** \texttt{QidSet}, respectively, with functions \texttt{eSortToQid} defined 
*** on the appropriate sorts.

fmod VIEW-EXPR-TO-QID is
  pr VIEW-EXPR .
  pr EXT-QID-LIST .

  op viewExpToQid : ViewExp -> Qid .
  op viewExpToQidList : ViewExp -> QidList .

  var  QI : Qid .
  var  QIL : QidList .
  vars VE VE' : ViewExp .

  eq viewExpToQidList(QI) = QI .
  eq viewExpToQidList((VE ;; VE')) 
    = (viewExpToQidList(VE) '; viewExpToQidList(VE')) .
  ceq viewExpToQidList((VE | VE'))
    = (if QI == '`) then QIL QI '\s else QIL QI fi) '| viewExpToQidList(VE')
    if (VE =/= nullViewExp) /\ (VE' =/= nullViewExp) 
       /\ QIL QI := viewExpToQidList(VE).
  ceq viewExpToQidList(VE << VE' >>)
    = (viewExpToQidList(VE) '`( viewExpToQidList(VE') '`))
    if (VE =/= nullViewExp) and (VE' =/= nullViewExp) .

  eq viewExpToQid(QI) = QI .
  eq viewExpToQid((VE ;; VE')) 
    = qidListToQid(viewExpToQid(VE) '; viewExpToQid(VE')) .
  ceq viewExpToQid((VE | VE'))
    = qid(string(viewExpToQid(VE)) + " | " + string(viewExpToQid(VE')))
    if (VE =/= nullViewExp) and (VE' =/= nullViewExp) .
  ceq viewExpToQid(VE << VE' >>)
    = qidListToQid(viewExpToQid(VE) '`( viewExpToQid(VE') '`))
    if (VE =/= nullViewExp) and (VE' =/= nullViewExp) .

***  eq viewExpToQid(VE) = qidListToQid(viewExpToQidList(VE)) .
endfm

*******************************************************************************

***
*** Parameterized Sorts
***

*** In addition to the \texttt{ESort} sort, in the following module
*** \texttt{EXT-SORT} we also define sorts \texttt{ESortList} and 
*** \texttt{ESortSet}.

*** The operator \texttt{eSort} is declared to be a constructor for extended 
*** sorts.

*** As for lists and sets of quoted identifiers, we declare \verb~__~ and
*** \verb~_;_~ as constructors for sorts \texttt{SortList} and 
*** \texttt{ESortList}, and \texttt{ESortSet}, respectively.


fmod EXT-SORT is
  pr META-LEVEL .
  pr VIEW-EXPR-TO-QID .

  sort ESort EType EKind .
  subsort Sort < ESort .
  subsort Kind Sort < Type .
  subsort ESort EKind Type < EType .

  op eSort : ESort ViewExp -> ESort .
  op kind : ESortSet -> EKind .
  op error : QidList -> [ESort] [ctor format (r o)] .

  var QIL : QidList .
  var VE : ViewExp .

  eq eSort(error(QIL), VE) = error(QIL) .

  eq kind(ES ; ES' ; ESS) = kind(ES) .

  sort ETypeList .
  subsort EType TypeList < ETypeList .
  op __ : ETypeList ETypeList -> ETypeList [assoc id: nil] .

  sort ESortSet .
  subsort ESort SortSet < ESortSet .
  op _;_ : ESortSet ESortSet -> ESortSet [assoc comm id: none] .

  eq (ES ; ES ; ESS) = (ES ; ESS) .

*** We define operations extending the built-in functions \texttt{sameKind}
*** and \texttt{leastSort}, respectively, to lists of
*** sorts (\texttt{eSameKind}) and to lists of extended
*** terms (\texttt{termListLeastSort}). The function \texttt{eSameKind} takes
*** a module and two lists of extended sorts as arguments, and returns
*** \texttt{true} if the $i$-th elements of both lists are in the same
*** connected component of sorts. This function will be used, for example, to
*** check whether two operators are in the same family of subsort overloaded
*** operators. \texttt{leastSort} returns a list of sorts where the $i$-th
*** element of the list is the least sort, computed by the homonymous built-in
*** function, of the $i$-th term in the list of terms given as argument.
*** Moreover, we define a function \verb~_inSortSet_~ to check whether an
*** extended sort is in a given set of extended sorts.  Note that before
*** calling the built-in function \texttt{sameComponent}, extended sorts of
*** sort \texttt{ESort} have to be `desugared' into sorts of sort
*** \texttt{Sort} as defined in the predefined \texttt{META-LEVEL} module.
*** This conversion is done by the \texttt{eTypeToType} function. Basically, 
*** user-defined sorts are converted into quoted identifiers by concatenating 
*** the list of identifiers composing the name of the sort. For example, sorts 
*** \texttt{'Nat} and \texttt{'List['Nat]} are converted, respectively, into 
*** \texttt{'Nat} and \texttt{'List`[Nat`]}. Error 
*** sorts~\cite{ClavelDuranEkerLincolnMarti-OlietMeseguerQuesada99} are left 
*** as such.

  vars QI S S' : Qid .
  var  SS : SortSet .
  vars ES ES' : ESort .
  vars ESS ESS' : ESortSet .
  vars ETL ETL' : ETypeList .
  vars ET ET' : EType .
  var  M : Module .
  var  T : Term .
  var  TL : TermList .
  var  IL : ImportList .
  var  SSDS : SubsortDeclSet .
  var  OPDS : OpDeclSet .
  var  MAS : MembAxSet .
  var  EqS : EquationSet .
  var  RlS : RuleSet .

  op eTypeToType : EType -> Type .

  eq eTypeToType(QI) = QI .
  eq eTypeToType(kind(ES ; ESS)) = kind(eTypeToType(ES)) .
  eq eTypeToType(eSort(ES, VE)) 
    = qid(string(eTypeToType(ES)) + "(" + string(viewExpToQid(VE)) + ")") .

  op eSameKind : Module ETypeList ETypeList -> Bool .

  eq eSameKind(M, (ET ETL), (ET' ETL'))
    = sameKind(M, eTypeToType(ET), eTypeToType(ET')) 
      and-then eSameKind(M, ETL, ETL')  .
  eq eSameKind(M, (ET ETL), nil) = false .
  eq eSameKind(M, nil, (ET ETL)) = false .
  eq eSameKind(M, nil, nil) = true .

  op termListLeastSort : Module TermList -> ETypeList .

  eq termListLeastSort(M, (T, TL)) 
    = (leastSort(M, T) termListLeastSort(M, TL)) .
  eq termListLeastSort(M, T) = leastSort(M, T) .

  op _inSortSet_ : ESort ESortSet -> Bool .

  eq ES inSortSet (ES ; ESS) = true .
  eq ES inSortSet (ES' ; ESS) = (ES == ES') or-else (ES inSortSet ESS) .
  eq ES inSortSet none = false .
endfm

*******************************************************************************

***
*** Transforming Extended Sorts into Quoted Identifiers
***

*** Since eventually all units will have to be given as arguments in some of
*** the calls to the built-in functions, and since the engine does not know
*** about parameterized sorts, we need to transform all parameterized sorts
*** appearing in any of the declarations that can appear in a unit into quoted
*** identifiers. This is the task of the \texttt{eSortToQid} function, which
*** is defined in the module \texttt{EXT-SORT-TO-QID}. These functions will be
*** used with terms not containing error sorts\footnote{The Core Maude system
*** automatically adds error supersorts above each of the connected components
*** of the poset of sorts declared by the user, using the set of maximal sorts
*** in each connected component to qualify the corresponding error sort. Such
*** error sorts are called {\em kinds} in the theory of membership
*** algebras~\cite{Meseguer98,BouhoulaJouannaudMeseguer97a}.}. Although the
*** user cannot use error sorts, calls to built-in functions may generate 
*** such error sorts, and some built-in functions can handle them. The 
*** function \texttt{eTypeToType} presented in the previous module will be 
*** used in the calls to the built-in functions that may use such error sorts.

fmod EXT-SORT-TO-QID is
  pr EXT-SORT .

  op eSortToQidList : ESort -> QidList .
  op eTypeListToQidList : ETypeList -> QidList .
  op eSortSetToQidList : ESortSet -> QidList .

  op eSortToSort : [ETypeList] -> [ETypeList] .
  op eSortToSort : ETypeList -> TypeList .
  op eSortToSort : EType -> Type .
  op eSortToSort : ESortSet -> SortSet .
  op eSortToSort : ESort -> Sort .

  var QI : Qid .
  var QIL : QidList .
  var T : Type .
  var SS : SortSet .
  var VE : ViewExp .
  var ES : ESort .
  var ET : EType .
  var ETL : ETypeList .
  var ESS : ESortSet .

  eq eSortToSort(error(QIL)) = error(QIL) .

  eq eSortToQidList(T) = T .
  eq eSortToQidList(kind(ES ; ESS)) = '`[ eSortToQidList(ES) '`] .
  ceq eSortToQidList(eSort(ES, VE)) 
    = (if QI == '\s then QIL else QIL QI fi '`( viewExpToQidList(VE) '`) '\s) 
    if QIL QI := eSortToQidList(ES) .
***  eq eSortToQidList(eSort(ES, VE)) 
***    = (eSortToQidList(ES) '`( viewExpToQidList(VE) '`)) .

  eq eTypeListToQidList((ET ETL))
    = if ETL == nil 
      then eSortToQidList(ET)
      else (eSortToQidList(ET) eTypeListToQidList(ETL)) 
      fi .
  eq eTypeListToQidList(nil) = nil .

  eq eSortSetToQidList((ES ; ESS))
    = if ESS == none
      then eSortToQidList(ES)
      else (eSortToQidList(ES) '; eSortSetToQidList(ESS)) 
      fi .
  eq eSortSetToQidList(none) = nil .

***  eq eSortToSort(ET) = qidListToQid(eSortToQidList(ET)) .
  eq eSortToSort(T) = T .
  eq eSortToSort(eSort(ES, VE)) 
    = qidListToQid(eSortToSort(ES) '`( viewExpToQid(VE) '`)) .
  eq eSortToSort(kind(ES)) = qidListToQid('`[ eSortToSort(ES) '`]) .

  ceq eSortToSort((ET ETL)) 
    = eSortToSort(ET) eSortToSort(ETL)
    if ETL =/= nil .
  eq eSortToSort((nil).ETypeList) = nil .

  ceq eSortToSort((ES ; ESS))
    = eSortToSort(ES) ; eSortToSort(ESS) 
    if ESS =/= none .
  eq eSortToSort((none).ESortSet) = none .
endfm

*******************************************************************************

fmod EXT-TERM is 
  pr META-TERM .
  pr QID-LIST .
  
***  pr EXT-SORT .
***  sorts ETerm ETermList .
***  subsorts EVariable EConstant < ETerm < ETermList .
***  op _,_ : ETermList ETermList -> ETermList 
***     [ctor assoc gather (e E) prec 120] .
***  op _[_] : Qid ETermList -> ETerm [ctor] . 
***  op const : Qid ESort -> EConstant [ctor] .
***  op var : Qid ESort -> EVariable [ctor] .
***
***  ops (_::_) (_:::_) : ETerm ESort -> ETerm .

***  op error : QidList -> [Term] [ctor format (r o)] .  

  sort Default`(Term`) .
  subsort Term < Default`(Term`) .
  ops noTerm noView : -> Default`(Term`) .

  var  Ct : Constant .
  var  V  : Variable .
  op myGetName : Constant -> Qid [memo] .
  op myGetName : Variable -> Qid [memo] .
  eq myGetName(Ct) = getName(Ct) .
  eq myGetName(V) = getName(V) .

endfm

*******************************************************************************

***
*** Extended Declarations
***

*** In this section we discuss modules \texttt{EXT-DECL} and \texttt{O-O-DECL}
*** which introduce, respectively, the declarations extending the sorts and
*** constructors for declarations of the predefined data type \texttt{Module}
*** in the \texttt{META-LEVEL} module to allow the use of extended sorts in
*** them, and the declarations appearing in object-oriented units, namely 
*** class declarations, subclass relation declarations, and message 
*** declarations.

***
*** Declarations of Functional and System Units
***

*** In the following module \texttt{EXT-DECL}, we introduce the declarations
*** extending those in \texttt{META-LEVEL} to allow the use of extended sorts
*** in declarations of sorts, subsort relations, operators, variables, and 
*** membership axioms.

*** \begin{comment}
*** \footnote{In the future, the declarations for operators,
*** membership axioms, equations, and rules will be extended to allow
*** the use of extended sorts in sort tests, that is, terms of the
*** form \mbox{\verb~T : ES~} and \mbox{\verb~T :: ES~}.}
*** \end{comment}

*** The extension is accomplished by adding new supersorts for each of the
*** sorts in \texttt{META-LEVEL} involved, and by adding new constructors for 
*** these new sorts.

*** We start introducing the declarations for the supersorts and their 
*** corresponding constructors. The \texttt{EXT-DECL} module also contains the
*** declarations for sets of such declarations.


fmod EXT-DECL is
  pr EXT-SORT .
  pr EXT-TERM .

  vars ES ES' : ESort .
  var  ESS : ESortSet .
  var  VE : ViewExp .
  vars F S : Qid .
  var  C : Constant .
  vars V V' : Variable .
  var  ETL : TermList .
  var  ET : Term .
  vars QIL QIL' : QidList .

*** extended subsort declarations
  sorts ESubsortDecl ESubsortDeclSet .
  subsort SubsortDecl < ESubsortDecl .
  subsorts SubsortDeclSet ESubsortDecl < ESubsortDeclSet .
  op subsort_<_. : ESort ESort -> ESubsortDecl .
  op __ : ESubsortDeclSet ESubsortDeclSet -> ESubsortDeclSet [ditto] .
  op error : QidList -> [ESubsortDeclSet] [ctor format (r o)] .

  eq ESSD:ESubsortDecl ESSD:ESubsortDecl = ESSD:ESubsortDecl .

  eq (error(QIL) error(QIL')).[ESubsortDeclSet] = error(QIL QIL') .

*** extended hooks
  sorts EHook EHookList .
  subsort Hook < EHook HookList < EHookList .
  op term-hook : Qid Term -> EHook [ctor] .
  op __ : EHookList EHookList -> EHookList [ditto] .

*** extended attributes
  sorts EAttr EAttrSet .
  subsort Attr < AttrSet EAttr < EAttrSet .

  op id : Term -> EAttr [ctor] .
  op left-id : Term -> EAttr [ctor] .
  op right-id : Term -> EAttr [ctor] .
  op special : EHookList -> EAttr [ctor] .

  op nonexec : -> Attr [ctor] .

  op __ : EAttrSet EAttrSet -> EAttrSet [ditto] .
  eq A:EAttr A:EAttr = A:EAttr .

*** extended operation declarations
  sorts EOpDecl EOpDeclSet .
  subsort OpDecl < EOpDecl .
  subsorts OpDeclSet EOpDecl < EOpDeclSet .
  op op_:_->_`[_`]. : Qid ETypeList EType EAttrSet -> EOpDecl [ditto] .
  op __ : EOpDeclSet EOpDeclSet -> EOpDeclSet [ditto] .

  op error : QidList -> [EOpDeclSet] [ctor format (r o)] .

  vars EOPD EOPD' : EOpDecl .
  var EOPDS : EOpDeclSet .

  eq EOPD EOPD = EOPD .

  eq (error(QIL) error(QIL')).[EOpDeclSet] = error(QIL QIL') .

*** extended conditions
  sorts EEqCondition ECondition .
  subsort EEqCondition < ECondition .
  subsort Condition < ECondition .
  subsort EqCondition < EEqCondition .
  op _:_ : Term ESort -> EEqCondition [ditto] .
  op _/\_ : EEqCondition EEqCondition -> EEqCondition [ditto] .
  op _/\_ : ECondition ECondition -> ECondition [ditto] .

*** extended membership axioms 
  sorts EMembAx EMembAxSet .
  subsort MembAx < EMembAx .
  subsorts EMembAx MembAxSet < EMembAxSet .
  op mb_:_`[_`]. : Term ESort EAttrSet -> EMembAx [ditto] .
  op cmb_:_if_`[_`]. : Term ESort EEqCondition EAttrSet -> EMembAx [ditto] .
  op __ : EMembAxSet EMembAxSet -> EMembAxSet [ditto] .
  op error : QidList -> [EMembAxSet] [ctor format (r o)] .

  eq MB:EMembAx MB:EMembAx = MB:EMembAx .

  eq (error(QIL) error(QIL')).[EMembAxSet] = error(QIL QIL') .

*** extended equations
  sorts EEquation EEquationSet .
  subsort Equation < EEquation EquationSet < EEquationSet .
  op eq_=_`[_`]. : Term Term EAttrSet -> EEquation [ditto] .
  op ceq_=_if_`[_`]. : Term Term EEqCondition EAttrSet -> EEquation [ditto] .
  op __ : EEquationSet EEquationSet -> EEquationSet [ditto] .
  op error : QidList -> [EEquationSet] [ctor format (r o)] .

  eq EQ:EEquation EQ:EEquation = EQ:EEquation .

  eq (error(QIL) error(QIL')).[EEquationSet] = error(QIL QIL') .

*** extended rules
  sorts ERule ERuleSet .
  subsort Rule < ERule RuleSet < ERuleSet .
  op rl_=>_`[_`]. : Term Term EAttrSet -> ERule [ditto] .
  op crl_=>_if_`[_`]. : Term Term ECondition EAttrSet -> ERule [ditto] .
  op __ : ERuleSet ERuleSet -> ERuleSet [ditto] .
  op error : QidList -> [ERuleSet] [ctor format (r o)] .

  eq RL:ERule RL:ERule = RL:ERule .

  eq (error(QIL) error(QIL')).[EEquationSet] = error(QIL QIL') .

*** The function \verb~_in_~ checks whether a given operator
*** declaration is in a set of operator declarations.

  op _in_ : EOpDecl EOpDeclSet -> Bool .

  eq EOPD in (EOPD EOPDS) = true .
  eq EOPD in (EOPD' EOPDS) = (EOPD == EOPD') or-else (EOPD in EOPDS) .
  eq EOPD in none = false .

*** There are also some other functions to deal with variables.  The function
*** \texttt{getVarsInTerm} returns the set of the variable declarations in the
*** given module for those variables that appear in the term given as second
*** argument.  The function \texttt{varDeclsDiff} computes the set-theoretic
*** difference between the two sets of variables given as arguments. Note that
*** the difference is not between the declarations themselves, but just
*** between the names of the variables in the declarations; the sorts with 
*** which they are declared are not taken into consideration.

*** The predicate \texttt{varInVarDeclSet} checks whether there is a variable
*** with the name given as first argument in the set of variable declarations 
*** given as second argument.

endfm

*******************************************************************************

***
*** Declarations for Object-Oriented Units
***

*** In the \texttt{O-O-DECL} module we introduce the sorts and constructors
*** for declarations of classes, subclass relations, and messages in 
*** object-oriented units.

*** Note that we follow the same naming conventions for classes as for
*** extended sorts (see Section~\ref{parameterized-modules}), and therefore
*** we use the sort \texttt{ESort} for class identifiers, and
*** \texttt{ETypeList} and \texttt{ESortSet} for lists and sets of class
*** identifiers, respectively.  We use the operator \verb~attr_:_~ as a
*** constructor for declarations of attributes. Since the operator name
*** \texttt{\_\,:\_\,} is used for sort  tests in the \texttt{META-LEVEL}
*** module, we use \texttt{attr\_\,:\_\,} as  constructor for declarations of
*** attributes to satisfy the preregularity  condition.

fmod O-O-DECL is
  pr EXT-SORT .

  vars QIL QIL' : QidList .

  sorts AttrDecl AttrDeclSet . 
  subsort AttrDecl < AttrDeclSet .
  op attr_:_ : Qid ESort -> AttrDecl .
  op none : -> AttrDeclSet .
  op _`,_ : AttrDeclSet AttrDeclSet -> AttrDeclSet [assoc comm id: none] .

  eq AD:AttrDecl, AD:AttrDecl = AD:AttrDecl .

  sorts ClassDecl ClassDeclSet . 
  subsort ClassDecl < ClassDeclSet .
  op class_|_. : ESort AttrDeclSet -> ClassDecl .
  op none : -> ClassDeclSet .
  op __ : ClassDeclSet ClassDeclSet -> ClassDeclSet [assoc comm id: none] .

  op error : QidList -> [ClassDeclSet] [ctor format (r o)] .
  eq (error(QIL) error(QIL')).[ClassDeclSet] = error(QIL QIL') .

  eq CD:ClassDecl CD:ClassDecl = CD:ClassDecl .

  sorts SubclassDecl SubclassDeclSet . 
  subsort SubclassDecl < SubclassDeclSet .
  op subclass_<_. : ESort ESort -> SubclassDecl .
  op none : -> SubclassDeclSet .
  op __ : SubclassDeclSet SubclassDeclSet -> SubclassDeclSet 
     [assoc comm id: none] .

  eq SCD:SubclassDecl SCD:SubclassDecl = SCD:SubclassDecl .

  op error : QidList -> [SubclassDeclSet] [ctor format (r o)] .
  eq (error(QIL) error(QIL')).[SubclassDeclSet] = error(QIL QIL') .

  sorts MsgDecl MsgDeclSet . 
  subsort MsgDecl < MsgDeclSet .
  op msg_:_->_. : Qid ETypeList ESort -> MsgDecl .
  op none : -> MsgDeclSet .
  op __ : MsgDeclSet MsgDeclSet -> MsgDeclSet [assoc comm id: none] .

  eq MD:MsgDecl MD:MsgDecl = MD:MsgDecl .

  op error : QidList -> [MsgDeclSet] [ctor format (r o)] .
  eq (error(QIL) error(QIL')).[MsgDeclSet] = error(QIL QIL') .

*** The function \texttt{classSet} returns the set of class identifiers in
*** the set of class declarations given as argument.

  op classSet : ClassDeclSet -> ESortSet .

  eq classSet((class ES:ESort | ADS:AttrDeclSet .) CDS:ClassDeclSet) 
    = (ES:ESort ; classSet(CDS:ClassDeclSet)) .
  eq classSet(none) = none .
endfm

*******************************************************************************

***
*** `Desugaring' of Extended Sorts in Declarations
***

*** In the following module we define the \texttt{eSortToSort} function on the
*** sorts for the different declarations introduced in the previous modules.


fmod DECL-EXT-SORT-TO-QID is
  pr EXT-SORT-TO-QID .
  pr EXT-DECL .
  pr O-O-DECL .

  op eSortToSort : ESubsortDeclSet -> SubsortDeclSet .
  op eSortToSort : EOpDeclSet -> OpDeclSet .
  op eSortToSort : EMembAxSet -> MembAxSet .
  op eSortToSort : EEquationSet -> EquationSet .
  op eSortToSort : ERuleSet -> RuleSet .
  op eSortToSort : ECondition -> Condition .
  op eSortToSort : ClassDeclSet -> ClassDeclSet .
  op eSortToSort : SubclassDeclSet -> SubclassDeclSet .
  op eSortToSort : MsgDeclSet -> MsgDeclSet .
  op eSortToSort : AttrDeclSet -> AttrDeclSet .

  vars QI F V : Qid .
  var  SS : SortSet .
  vars VE VE' : ViewExp .
  vars ES ES' : ESort .
  var  ETL : ETypeList .
  var  ET : EType .
  var  ESS : ESortSet .
  vars T T' T'' T''' : Term .
  var  ESSDS : ESubsortDeclSet .
  var  EOPDS : EOpDeclSet .
  var  AtS : EAttrSet .
  var  EMAS : EMembAxSet .
  var  EqS : EEquationSet .
  var  RlS : ERuleSet .
  var  CDS : ClassDeclSet .
  var  ADS : AttrDeclSet .
  var  MDS : MsgDeclSet .
  var  SCDS : SubclassDeclSet .
  vars Cond Cond' : Condition .

  eq eSortToSort(((subsort ES < ES' .) ESSDS))
    = ((subsort eSortToSort(ES) < eSortToSort(ES') .) eSortToSort(ESSDS)) .
  eq eSortToSort((none).ESubsortDeclSet) = none .

  eq eSortToSort(((op F : ETL -> ET [AtS] .) EOPDS))
    = ((op F : eSortToSort(ETL) -> eSortToSort(ET) [AtS] .) 
       eSortToSort(EOPDS)) .
  eq eSortToSort((none).EOpDeclSet) = none .

  eq eSortToSort(((eq T = T' [AtS] .) EqS)) 
    = ((eq T = T' [AtS] .) eSortToSort(EqS)) .
  eq eSortToSort(((ceq T = T' if Cond [AtS] .) EqS))
    = ((ceq T = T' if eSortToSort(Cond) [AtS] .) eSortToSort(EqS)) .
  eq eSortToSort((none).EEquationSet) = none .

  eq eSortToSort(((rl T => T' [AtS] .) RlS)) 
    = ((rl T => T' [AtS] .) eSortToSort(RlS)) .
  eq eSortToSort(((crl T => T' if Cond [AtS] .) RlS))
    = ((crl T => T' if eSortToSort(Cond) [AtS] .) eSortToSort(RlS)) .
  eq eSortToSort((none).ERuleSet) = none .

  eq eSortToSort(((mb T : ES [AtS] .) EMAS)) 
    = ((mb T : eSortToSort(ES) [AtS] .) eSortToSort(EMAS)) .
  eq eSortToSort(((cmb T : ES if Cond [AtS] .) EMAS))
    = ((cmb T : eSortToSort(ES) if eSortToSort(Cond) [AtS] .) 
       eSortToSort(EMAS)) .
  eq eSortToSort((none).EMembAxSet) = none .

  eq eSortToSort(((class ES | ADS .) CDS))
    = ((class eSortToSort(ES) | eSortToSort(ADS) .) eSortToSort(CDS)) .
  eq eSortToSort((none).ClassDeclSet) = none .

  eq eSortToSort(((attr F : ET), ADS)) 
    = ((attr F : eSortToSort(ET)), eSortToSort(ADS)) .
  eq eSortToSort((none).AttrDeclSet) = none .

  eq eSortToSort(((subclass ES < ES' .) SCDS))
    = ((subclass eSortToSort(ES) < eSortToSort(ES') .) eSortToSort(SCDS)) .
  eq eSortToSort((none).SubclassDeclSet) = none .

  eq eSortToSort(((msg F : ETL -> ET .) MDS))
    = ((msg F : eSortToSort(ETL) -> eSortToSort(ET) .) eSortToSort(MDS)) .
  eq eSortToSort((none).MsgDeclSet) = none .

  ceq eSortToSort(Cond /\ Cond') 
    = eSortToSort(Cond) /\ eSortToSort(Cond') 
    if Cond =/= nil and Cond' =/= nil .
  eq eSortToSort(T = T') = T = T' .
  eq eSortToSort(T : ES) = T : eSortToSort(ES) .
  eq eSortToSort(T := T') = T := T' .
  eq eSortToSort(T => T') = T => T' .

endfm

*******************************************************************************

***
*** Renaming Maps
***

*** We introduce the different types of renaming maps in the module
*** \texttt{MAP} below. A sort is introduced for each of these types of maps,
*** with the appropriate constructors for each sort (see
*** Section~\ref{module-expressions}). All these sorts are declared to be
*** subsorts of the sort \texttt{Map}. A sort for sets of 
*** maps (\texttt{MapSet}) is then declared as supersort of \texttt{Map} with 
*** constructors \texttt{none} and \verb~_,_~.

fmod MAP is
  pr EXT-SORT .

  sorts OpMap SortMap LabelMap ClassMap MsgMap AttrMap Map .
  subsorts OpMap SortMap LabelMap ClassMap MsgMap AttrMap < Map .
  op op_to_`[_`] : Qid Qid AttrSet -> OpMap .
  op op_:_->_to_`[_`] : Qid ETypeList ESort Qid AttrSet -> OpMap .
  op sort_to_ : ESort ESort -> SortMap .
  op label_to_ : Qid Qid -> LabelMap .
  op class_to_ : ESort ESort -> ClassMap .
  op attr_._to_ : Qid ESort Qid -> AttrMap .
  op msg_to_ : Qid Qid -> MsgMap .
  op msg_:_->_to_ : Qid ETypeList ESort Qid -> MsgMap .

  sort MapSet .
  subsort Map < MapSet .
  op none : -> MapSet .
  op _`,_ : MapSet MapSet -> MapSet [assoc comm id: none] .

*** Given a set of maps, the function \texttt{sortMapSet} returns the
*** subset of sort maps in it.

  var MAP : Map .
  var MAPS : MapSet .

  op sortMapSet : MapSet -> MapSet .

  eq sortMapSet((MAP, MAPS))
    = if MAP :: SortMap
      then (MAP, sortMapSet(MAPS))
      else sortMapSet(MAPS)
      fi .
  eq sortMapSet(none) = none .

endfm

*******************************************************************************

***
*** Module Expressions and Module Names
***

*** The abstract syntax for writing specifications in Maude can be seen as
*** given by module expressions, where the notion of module expression is
*** understood as an expression that defines a new module out of previously
*** defined modules by combining and/or modifying them according to a specific
*** set of operations.  All module expressions will be evaluated generating
*** modules with such module expressions as names. In the case of parameterized
*** modules, each of the parameters in an interface will be used as the name
*** of a new module created as a renamed copy of the parameter theory.

***
*** Module Expressions
***

*** In the following \texttt{MOD-EXPR} module the sort \texttt{ModExp} is
*** introduced as a supersort of \texttt{Qid}. Module expressions for module
*** renaming and for module instantiation will be introduced, respectively,
*** in the modules \texttt{RENAMING-EXPR-EVALUATION} and
*** \texttt{INST-EXPR-EVALUATION}, in Sections~\ref{renaming}
*** and~\ref{instantiation}, which will be defined as extensions of
*** \texttt{MOD-EXPR}. We shall see in Section~\ref{extension} how new module 
*** combining and/or transforming operators can be easily added, showing the 
*** flexibility and extensibility of the module algebra being defined.

fmod MOD-EXPR is
  pr QID .
  pr VIEW-EXPR .
  pr MAP .

  sort ModExp .
  subsort Qid < ModExp .

  op _<_> : ModExp ViewExp -> ModExp .  *** Parameterization _(_)
  op _*<_> : ModExp MapSet -> ModExp .  *** Renaming         _*(_)

  op _+_ : ModExp ModExp -> ModExp [assoc comm] .
  op TUPLE`[_`] : NzNat -> ModExp .

endfm

*******************************************************************************

***
*** Module Names
***

*** As we shall see in the coming sections, the evaluation of module
*** expressions may produce the creation of new modules, whose \emph{names}
*** are given by the module expressions themselves. If there is already a
*** module in the database with the module expression being evaluated as name,
*** the evaluation of such module expression does not produce any change in
*** the database. However, the evaluation of a module expression may involve 
*** the evaluation of some other module expressions contained in the modules 
*** involved, which in turn may generate new modules.

*** Given a parameterized module $\texttt{N[L}_1\texttt{\ ::\ T}_1
*** \texttt{\ |\ }\ldots\texttt{\ |\ L}_n\texttt{\ ::\ T}_n\texttt{]}$, with
*** $\texttt{L}_1\ldots\texttt{L}_n$ labels and
*** $\texttt{T}_1\ldots\texttt{T}_n$ theory identifiers, we say that
*** \texttt{N} is the name of the module and that
*** $\texttt{[L}_1\texttt{\ ::\ T}_1\texttt{\ |\ }
*** \ldots\texttt{\ |\ L}_n\texttt{\ ::\ T}_n\texttt{]}$ 
*** is its \emph{interface}.
*** As we shall see in Sections~\ref{instantiation} and~\ref{unit-processing},
*** for each parameter $\texttt{L}_i\texttt{\ ::\ T}_i$ in the interface of a
*** module, a new module is generated with such a parameter expression as its
*** name, and a declaration importing it in the parameterized module is added.
***  We regard the relationship between the body of a parameterized module and
*** the parameters in its interface, not as an inclusion, but as mediated by 
*** a module constructor that generates renamed copies of the parameters, 
*** which are then included. Therefore, the sort \texttt{Parameter} is 
*** declared as a subsort of \texttt{ModName}, that is, terms of sort 
*** \texttt{Parameter} are considered to be module names. The constructor 
*** operator for the sort \texttt{Parameter} is \verb~par_::_~.

*** The \texttt{MOD-NAME} module also includes a sort \texttt{ModNameSet}, for
*** sets of module names. The constructors of sort \texttt{ModNameSet} are
*** \texttt{noneModNameSet} and \verb~_._~. The function \verb~_inModNameSet_~
*** checks whether the module name given as first argument is in the set of 
*** module names given as second argument.

*** The sort for lists of parameters is \texttt{List`(Parameter`)}, which is
*** defined with constructors \texttt{parList} and \texttt{nilParList}.

fmod MOD-NAME is
  pr MOD-EXPR .
  pr EXT-BOOL .
  pr EXT-SORT .
  inc META-LEVEL .

  sorts Parameter Interface List`(Parameter`) .
  subsort Parameter < List`(Parameter`) .

  op par_::_ : Qid ModExp -> Parameter .           *** _::_
  op par_::_ : Qid Interface -> Parameter .        *** _::_
  op par     : ModExp List`(Parameter`) -> Interface . *** _(_)

  op nilParList : -> List`(Parameter`) .
  op parList : List`(Parameter`) List`(Parameter`) -> List`(Parameter`) 
       [assoc id: nilParList] .

*** For example,
***
*** X1 :: T1[X11 :: T11 | ... | X1n :: Tmn] | ... |
*** Xm :: Tm[Xm1 :: Tm1 | ... | Xmn :: Tmn]
***
*** is represented as
***
*** parList(
***    par 'X1 :: par(up(T1), 
***                   parList(par 'X11 :: up(T11),
***                                 ...,
***                                 par 'X1n :: up(T1n))),
***    ...,
***    par 'Xm :: par(up(Tm), 
***                   parList(par 'Xm1 :: up(Tm1),
***                                 ...,
***                                 par 'Xmn :: up(Tmn))))

  sorts ModName ModNameSet .
  subsorts Parameter ModExp < ModName < ModNameSet .
  op noneModNameSet : -> ModNameSet .
  op _._ : ModNameSet ModNameSet -> ModNameSet 
      [assoc comm id: noneModNameSet] .
  op nullModName : -> ModName .

  vars MN MN' : ModName .
  var MNS : ModNameSet .

  op _inModNameSet_ : ModName ModNameSet -> Bool .

  eq MN inModNameSet (MN' . MNS) = (MN == MN') or-else (MN inModNameSet MNS) .
  eq MN inModNameSet noneModNameSet = false .

*** The function \texttt{labelInParList} checks whether the quoted
*** identifier given as first argument is used as a label in the list of 
*** parameters given as second argument.

  vars QI QI' : Qid .
  var ME : ModExp .
  vars PL PL' : List`(Parameter`) .
  var VE : ViewExp .

  op labelInParList : ViewExp List`(Parameter`) -> Bool .

  eq labelInParList(QI << VE >>, parList((par QI' :: ME), PL))
    = labelInParList(QI << VE >>, PL) .
  eq labelInParList(QI << VE >>, parList((par QI' :: par(ME, PL)), PL'))
    = (QI == QI' and-then labelInParList(VE, PL))
       or-else
       labelInParList(QI << VE >>, PL') .
  ceq labelInParList((QI | VE), PL)
    = labelInParList(QI, PL) 
    if VE =/= nullViewExp .
  eq labelInParList(QI, parList((par QI' :: ME), PL))
    = (QI == QI') or-else labelInParList(QI, PL) .
  eq labelInParList(QI, parList((par QI' :: par(ME, PL)), PL'))
    = (QI == QI') 
      or-else 
      (labelInParList(QI, PL) 
       or-else labelInParList(QI, PL')) .
  eq labelInParList(VE, nilParList) = false .

  op DUMMY : ModName -> Module .
  eq DUMMY(MN)
    = (fmod 'DUMMY is
        including MN .
        sorts (if MN == 'META-LEVEL then 'Token ; 'Bubble else none fi) .
        none 
        (if MN == 'META-LEVEL 
         then op 'token : 'Qid -> 'Token 
                   [special(
                     (id-hook('Bubble, '1 '1)
                      op-hook('qidSymbol, '<Qids>, nil, 'Qid)))] .
              op 'bubble : 'QidList -> 'Bubble 
                   [special(
                     (id-hook('Bubble, '1 '-1 '`( '`))
                      op-hook('qidListSymbol, '__, 'QidList 'QidList, 'QidList)
                      op-hook('qidSymbol, '<Qids>, nil, 'Qid)))] .
              op 'up : 'Token 'Bubble -> 'Term [none] .
              op 'up : 'Token -> 'Module [none] .
         else none
         fi)
        none
        none
     endfm) .
endfm

*******************************************************************************

*** Since the Core Maude engine assumes that module names are identifiers and
*** does not know about term-structured module names (such as parameterized
*** module interfaces or module expressions), for evaluation purposes we need
*** to transform them into quoted identifiers. The functions
*** \texttt{modNameToQid} and \texttt{modNameToQidList} in the module
*** \texttt{MOD-NAME-TO-QID} below accomplish this transformation. In any
*** language extensions, new equations for the function
*** \texttt{modNameToQidList} should be added for each new module expression
*** constructor introduced. In Sections~\ref{renaming} and~\ref{instantiation} 
*** we shall see how the corresponding equalities are added for renaming and 
*** instantiation expressions, and in Section~\ref{extension} for other new 
*** module expressions in extensions of Full Maude.

fmod MOD-NAME-TO-QID is
  pr MOD-NAME .
  pr EXT-QID-LIST .

  op modNameToQid : ModName -> Qid .
  op modNameToQidList : ModName -> QidList .
  op parListToQid : List`(Parameter`) -> Qid .
  op parListToQidList : List`(Parameter`) -> QidList .

  vars QI X : Qid .
  vars ME ME' : ModExp .
  var  MN : ModName .
  var  PL : List`(Parameter`) .
  var  If : Interface .

  eq modNameToQidList(QI) = QI .
  eq modNameToQidList(par X :: ME) = (X ':: modNameToQidList(ME)) .
  eq modNameToQidList(par X :: par(ME, PL)) 
    = (X ':: modNameToQidList(ME) '`( parListToQidList(PL) '`)) .
  eq modNameToQidList(nullModName) = ' .

  ceq parListToQidList(parList((par X :: ME), PL))
    = (modNameToQidList(par X :: ME) '`, parListToQidList(PL)) 
    if PL =/= nilParList .
  ceq parListToQidList(parList((par X :: If), PL))
    = (modNameToQidList(par X :: If) '`, parListToQidList(PL)) 
    if PL =/= nilParList .
  eq parListToQidList((par X :: ME)) = modNameToQidList(par X :: ME) .
  eq parListToQidList((par X :: If)) = modNameToQidList(par X :: If) .

  eq modNameToQid(QI) = QI .
  eq modNameToQid(par X :: ME) = qidListToQid(X ':: modNameToQid(ME)) .
  eq modNameToQid(par X :: par(ME, PL)) 
    = qidListToQid(X ':: modNameToQid(ME) '`( parListToQid(PL) '`)) .
  eq modNameToQid(nullModName) = ' .

  ceq parListToQid(parList((par X :: ME), PL))
    = qidListToQid(modNameToQid(par X :: ME) '`, parListToQid(PL)) 
    if PL =/= nilParList .
  ceq parListToQid(parList((par X :: If), PL))
    = qidListToQid(modNameToQid(par X :: If) '`, parListToQid(PL)) 
    if PL =/= nilParList .
  eq parListToQid((par X :: ME)) = modNameToQid(par X :: ME) .
  eq parListToQid((par X :: If)) = modNameToQid(par X :: If) .

***  eq modNameToQid(MN) = qidListToQid(modNameToQidList(MN)) .

endfm

*******************************************************************************

***
*** Units
***

*** We handle six different types of units: functional, system, and
*** object-oriented modules, and functional, system, and object-oriented
*** theories.  Modules and theories of any kind are considered to be elements
*** in specific subsorts of the sort \texttt{Unit}. A constructor
*** \texttt{error} is also included to represent incorrect units.
*** \texttt{error} has a list of quoted identifiers as argument, which is
*** used to report the error. Besides considering functional and system
*** theories and object-oriented theories and modules, the declarations 
*** presented in the following module extend the declarations for sort 
*** \texttt{Module} in the \texttt{META-LEVEL} module in three different ways:

*** \begin{itemize}
*** \item the name of a module can be any term of sort \texttt{ModName},
*** \item parameterized modules are handled, for which a list of
***       parameters is added to the constructors of modules,
*** \item the importation declaration is extended to module names, and
*** \item parameterized sorts are supported.  
*** \end{itemize}


fmod UNIT is
  pr EXT-DECL .
  pr O-O-DECL .
  pr MOD-NAME-TO-QID .
  inc META-LEVEL .

*** We start by introducing declarations for sorts \texttt{EImport} and
*** \texttt{List`(EImport`)}, which are declared as supersorts of \texttt{Import}
*** and \texttt{ImportList}, respectively. We declare the constructor
*** \verb~including_.~ for importation declarations on module names. We shall
*** see in Section~\ref{parsing-unit-declarations} that importations in both 
*** \texttt{protecting} and \texttt{including} modes are represented using 
*** this constructor.

  sorts EImport List`(EImport`) .
  subsort Import < EImport  .
  subsorts ImportList EImport < List`(EImport`) .
  op protecting_. : ModName -> EImport [ctor ditto] .
  op including_. : ModName -> EImport [ctor ditto] .
  op __ : List`(EImport`) List`(EImport`) -> List`(EImport`) [ctor ditto] .

  op error : QidList -> [List`(EImport`)] [ctor format (r o)] .
  eq (error(QIL) error(QIL')).[List`(EImport`)] = error(QIL QIL') .

***  eq (including MN:ModName .) EIL:List`(EImport`) (including MN:ModName .) 
***    = (including MN:ModName .) EIL:List`(EImport`) .
***  eq (including MN:ModName .) EIL:List`(EImport`) (protecting MN:ModName .) 
***    = (including MN:ModName .) EIL:List`(EImport`) .
***  eq (protecting MN:ModName .) EIL:List`(EImport`) (including MN:ModName .) 
***    = (including MN:ModName .) EIL:List`(EImport`) .

*** Next, we introduce the different sorts for the different types of modules
*** and theories, with the subsort relation among them, and their
*** constructors. The structure of the hierarchy of sorts can be seen in 
*** Figure~\ref{unit-sort-hierarchy}.
*** \begin{figure}
*** \begin{center}
*** \scalebox{.8}{
***   \includegraphics{module-sort-hierarchy.eps}
*** }
*** \end{center}
*** \caption{\label{unit-sort-hierarchy}Hierarchy of Unit Sorts.}
*** \end{figure}

  sorts Unit FUnit SUnit OUnit StrFModule StrSModule StrOModule StrModule 
        StrFTheory StrSTheory StrOTheory StrTheory .
  subsorts FModule < StrFModule < FUnit StrSModule .
  subsorts Module < StrSModule < SUnit StrOModule .
  subsorts StrFTheory < StrSTheory FUnit .
  subsorts StrSTheory < StrOTheory SUnit .
  subsort FUnit < SUnit .
  subsort StrOTheory < StrTheory .
  subsorts StrOTheory SUnit StrOModule < OUnit .
  subsort StrOModule < StrModule .
  subsorts StrTheory OUnit StrModule < Unit .

  op noUnit : -> Unit .   *** Module
  op error : QidList -> [Unit] [ctor format (r o)] .

  op fmod_is__sorts_.____endfm : ModName List`(Parameter`) List`(EImport`) ESortSet 
        ESubsortDeclSet EOpDeclSet EMembAxSet EquationSet -> StrFModule 
        [ctor 
         gather (& & & & & & & &)
         format (r! o r! n++io ni ni d d ni ni ni ni n--ir! o)] .
  op fth_is__sorts_.____endfth : ModName List`(Parameter`) List`(EImport`) ESortSet
        ESubsortDeclSet EOpDeclSet EMembAxSet EquationSet -> StrFTheory 
        [ctor 
         gather (& & & & & & & &)
         format (r! o r! n++io ni ni d d ni ni ni ni n--ir! o)] .
  op mod_is__sorts_._____endm : ModName List`(Parameter`) List`(EImport`) ESortSet
        ESubsortDeclSet EOpDeclSet EMembAxSet EquationSet RuleSet -> StrSModule
        [ctor 
         gather (& & & & & & & & &)
         format (r! o r! n++io ni ni d d ni ni ni ni ni n--ir! o)] .
  op th_is__sorts_._____endth : ModName List`(Parameter`) List`(EImport`) ESortSet
        ESubsortDeclSet EOpDeclSet EMembAxSet EquationSet RuleSet -> StrSTheory
        [ctor 
         gather (& & & & & & & & &)
         format (r! o r! n++io ni ni d d ni ni ni ni ni n--ir! o)] .
  op omod_is__sorts_.________endom : ModName List`(Parameter`) List`(EImport`)
        ESortSet ESubsortDeclSet ClassDeclSet SubclassDeclSet EOpDeclSet 
        MsgDeclSet EMembAxSet EquationSet RuleSet -> StrOModule 
        [ctor 
         gather (& & & & & & & & & & & &)
         format (r! o r! n++io ni ni d d ni ni ni ni ni ni ni ni n--ir! o)] .
  op oth_is__sorts_.________endoth : ModName List`(Parameter`) List`(EImport`)
        ESortSet ESubsortDeclSet ClassDeclSet SubclassDeclSet EOpDeclSet 
        MsgDeclSet EMembAxSet EquationSet RuleSet -> StrOTheory 
        [ctor 
         gather (& & & & & & & & & & & &)
         format (r! o r! n++io ni ni d d ni ni ni ni ni ni ni ni n--ir! o)] .

*** In addition to the constructor operators, the following functions are
*** introduced in the \texttt{UNIT} module:
*** \begin{itemize}
*** \item A function \verb~_in_~ to check whether a given importation
***       declaration is in a set of importation declarations or not.

  op _in_ : EImport List`(EImport`) -> Bool .

*** \item Selector functions for the different components of a unit.

  op getName : Unit -> ModName .
  op getImports : Unit -> List`(EImport`) .
  op getParList : Unit -> List`(Parameter`) .
  op getSorts : Unit -> ESortSet .
  op getSubsorts : Unit -> ESubsortDeclSet .
  op getOps : Unit -> EOpDeclSet .
  op getMbs : Unit -> EMembAxSet .
  op getEqs : Unit -> EquationSet .
  op getRls : Unit -> RuleSet .
  op getClasses : Unit -> ClassDeclSet .
  op getSubclassDecls : Unit -> SubclassDeclSet .
  op getMsgs : Unit -> MsgDeclSet .

*** \item Functions to change the value of each of the components of a unit.

  op setName : Unit ModName -> Unit .
  op setPars : Unit List`(Parameter`) -> Unit .
  op setImports : Unit List`(EImport`) -> Unit .
  op setSorts : Unit ESortSet -> Unit .
  op setSubsorts : Unit ESubsortDeclSet -> Unit .
  op setOps : Unit EOpDeclSet -> Unit .
  op setMbs : Unit EMembAxSet -> Unit .
  op setEqs : Unit EquationSet -> Unit .
  op setRls : Unit RuleSet -> Unit .
  op setClasses : Unit ClassDeclSet -> Unit .
  op setSubclasses : Unit SubclassDeclSet -> Unit .
  op setMsgs : Unit MsgDeclSet -> Unit .

*** \item Functions to add new declarations to the set of declarations 
*** already in a unit.

  op addImports : List`(EImport`) Unit -> Unit .
  op addSorts : ESortSet Unit -> Unit .
  op addSubsorts : [ESubsortDeclSet] Unit -> Unit .
  op addOps : [EOpDeclSet] Unit -> Unit .
  op addMbs : EMembAxSet Unit -> Unit .
  op addEqs : EquationSet Unit -> Unit .
  op addRls : RuleSet Unit -> Unit .
  op addClasses : ClassDeclSet Unit -> Unit .
  op addSubclasses : SubclassDeclSet Unit -> Unit .
  op addMsgs : MsgDeclSet Unit -> Unit .

*** \item There are functions and constants to create empty units of the
***       different types. For example, the function \texttt{emptyStrFTheory}
***       returns an empty structured functional theory. There is also a
***       function \texttt{empty} which takes a unit as argument and returns 
***       an empty unit of the same type.

  op emptyFModule : ModName -> FModule .
  op emptyStrFModule : -> StrFModule .
  op emptyStrSModule : -> StrSModule .
  op emptyStrOModule : -> StrOModule .
  op emptyStrFTheory : -> StrFTheory .
  op emptyStrSTheory : -> StrSTheory .
  op emptyStrOTheory : -> StrOTheory .
  op empty : Unit -> Unit .

*** \item A function \texttt{addDecls} which returns the unit resulting from
***       adding all the declarations in the unit passed as second argument 
***       to the unit passed as first argument.
 
  op addDecls : Unit Unit -> Unit .

*** \end{itemize}

*** Note that some of the `set' and `add' functions are partial functions.

  var  M : Module .
  vars QI V : Qid .
  var  ES : ESort .
  vars SSDS SSDS' SSDS'' : SubsortDeclSet .
  vars ESSDS ESSDS' : ESubsortDeclSet .
  vars OPDS OPDS' : OpDeclSet .
  vars EOPD EOPD' : EOpDecl .
  vars EOPDS EOPDS' : EOpDeclSet .
  var  EOPDS? : [EOpDeclSet] .
  var  At : Attr .
  vars EMAS EMAS' : EMembAxSet .
  vars MAS MAS' : MembAxSet .
  vars EqS EqS' : EquationSet .
  vars RlS RlS' : RuleSet .
  vars ESS ESS' : ESortSet .
  vars SS SS' : SortSet .
  vars IL IL' : ImportList .
  vars MN MN' : ModName .
  vars QIL QIL' : QidList .
  vars PL PL' : List`(Parameter`) .
  vars CDS CDS' : ClassDeclSet .
  vars SCD SCD' : SubclassDecl .
  vars SCDS SCDS' : SubclassDeclSet .
  vars U U' : Unit .
  vars MDS MDS' : MsgDeclSet .
  vars EI EI' : EImport .
  vars EIL EIL' : List`(EImport`) .
  var  T : Term .

  eq EI in (EI EIL) = true .
  eq EI in (EI' EIL) = (EI == EI') or-else (EI in EIL) .
  eq EI in nil = false .

  op eLeastSort : Unit Term -> [Type] .
  eq eLeastSort(U, T) = leastSort(U, T) .
  eq eLeastSort(U, error(QIL)) = error(QIL) .
***    = if (U : Module)                         *** and (T =/= error*)
***      then leastSort(U, T)
***      else errorSort(none) 
***      fi .

*** Selection functions for units

  eq getName((error(QIL)).Unit) = nullModName .
  eq getName(mod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endm) = MN .
  eq getName(th MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endth) = MN .
  eq getName(fmod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfm) = MN .
  eq getName(fth MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfth) 
    = MN .
  eq getName(
        omod MN is 
          PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
        endom) 
    = MN .
  eq getName(
        oth MN is 
           PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
        endoth) 
    = MN .

  eq getImports(error(QIL)) = nil .
  eq getImports(mod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endm) 
    = EIL .
  eq getImports(th MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endth) 
    = EIL .
  eq getImports(fmod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfm) 
    = EIL .
  eq getImports(fth MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfth) 
    = EIL .
  eq getImports(
       omod MN is 
          PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
       endom) 
    = EIL .
  eq getImports(
       oth MN is 
          PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
       endoth) 
    = EIL .

  eq getParList(error(QIL)) = nilParList .
  eq getParList(mod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endm) 
    = PL .
  eq getParList(mod QI is IL sorts SS . SSDS OPDS MAS EqS RlS endm) =
     nilParList .
  eq getParList(th MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endth) 
    = PL .
  eq getParList(fmod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfm) 
    = PL .
  eq getParList(fmod QI is IL sorts SS . SSDS OPDS MAS EqS endfm) 
    = nilParList .
  eq getParList(fth MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfth) 
    = PL .
  eq getParList(
       omod MN is 
          PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
       endom) 
    = PL .
  eq getParList(
       oth MN is 
          PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
       endoth) 
    = PL .

  eq getSorts((error(QIL)).Unit) = none .
  eq getSorts(mod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endm) 
    = ESS .
  eq getSorts(th MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endth) 
    = ESS .
  eq getSorts(fmod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfm) 
    = ESS .
  eq getSorts(fth MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfth) 
    = ESS .
  eq getSorts(
       omod MN is 
          PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
       endom) 
    = ESS .
  eq getSorts(
       oth MN is 
          PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
       endoth) 
    = ESS .

  op getAllSorts : Module -> SortSet .
  op getSortsIncld : ImportList -> SortSet .
  op getSorts : ModName -> SortSet .

  eq getAllSorts(M) = getSorts(M) ; getSortsIncld(getImports(M)) .
  *** only declared for flattened modules, which only imports built-ins

  eq getSortsIncld(including MN . EIL) = getSorts(MN) ; getSortsIncld(EIL) .
  eq getSortsIncld(protecting MN . EIL) = getSorts(MN) ; getSortsIncld(EIL) .
  eq getSortsIncld(nil) = none .

  eq getSorts('TRUTH-VALUE) = 'Bool .
  eq getSorts('THUTH) = getSorts('TRUTH-VALUE) .
  eq getSorts('BOOL) = getSorts('THUTH) .
  eq getSorts('EXT-BOOL) = getSorts('BOOL) .
  eq getSorts('IDENTICAL) = getSorts('BOOL) .
  eq getSorts('NAT) = getSorts('BOOL) ; 'Zero ; 'NzNat ; 'Nat .
  eq getSorts('INT) = getSorts('NAT) ; 'NzInt ; 'Int .
  eq getSorts('RAT) = getSorts('INT) ; 'NzRat ; 'Rat .
  eq getSorts('FLOAT) = getSorts('INT) ; 'FiniteFloat ; 'Float .
  eq getSorts('STRING) = getSorts('NAT) ; 'String ; 'Char ; 'FindResult .
  eq getSorts('CONVERSION ) 
    = getSorts('RAT) ; getSorts('FLOAT) ; getSorts('STRING) ; 'DecFloat .
  eq getSorts('QID) = getSorts('STRING) ; 'Qid .
  eq getSorts('QID-LIST) = getSorts('QID) ; 'QidList .
  eq getSorts('META-TERM) 
    = getSorts('QID) ; 'Sort ; 'Kind ; 'Type ; 'Constant ; 'Variable ; 
      'GroundTerm ; 'Term ; 'GroundTermList ; 'TermList ; 'Assignment ; 
      'Substitution ; 'Context ; 'CTermList ; 'GTermList . 
  eq getSorts('META-MODULE) 
    = getSorts('META-TERM) ; getSorts('QID-LIST) ; 'ModuleExpression ; 
      'Import ; 'ImportList ; 'SortSet ; 'SubsortDecl ; 'SubsortDeclSet ; 
      'TypeList ; 'NatList ; 'Hook ; 'HookList ; 'Attr ; 'AttrSet ; 'OpDecl ; 
      'OpDeclSet ; 'EqCondition ; 'Condition ; 'MembAx ; 'MembAxSet ; 
      'Equation ; 'EquationSet ; 'Rule ; 'RuleSet ; 'FModule ; 'Module .
  eq getSorts('META-LEVEL) 
    = getSorts('META-MODULE) ; 'Bound ; 'KindSet ; 'Type? ; 'ResultPair ; 
      'ResultTriple ; 'Result4Tuple ; 'MatchPair ; 'ResultPair? ; 
      'ResultTriple? ; 'Result4Tuple? ; 'MatchPair? ; 'Substitution? .
  eq getSorts('CONFIGURATION) 
    = 'Attribute ; 'AttributeSet ; 'Oid ; 'Cid ; 'Object ; 'Msg ; 
      'Configuration .
  eq getSorts('LTL) 
    = 'Prop ; 'Formula .
  eq getSorts('LTL-SIMPLIFIER) 
    = getSorts('LTL) ; 'TrueFormula ; 'FalseFormula ; 'PureFormula ; 
      'PE-Formula ; 'PU-Formula .
  eq getSorts('SAT-SOLVER) 
    = getSorts('LTL) ; 'FormulaList ; 'SatSolveResult ; 'TautCheckResult .
  eq getSorts('MODEL-CHECKER) 
    = getSorts('QID) ; getSorts('LTL) ; 'State ; 'RuleName ; 'Transition ; 
      'TransitionList ; 'ModelCheckResult .
   
  eq getSubsorts(error(QIL)) = none .
  eq getSubsorts(mod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endm) 
    = ESSDS .
  eq getSubsorts(th MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endth) 
    = ESSDS .
  eq getSubsorts(fmod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfm) 
    = ESSDS .
  eq getSubsorts(fth MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfth) 
    = ESSDS .
  eq getSubsorts(
       omod MN is 
          PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
       endom) 
    = ESSDS .
  eq getSubsorts(
       oth MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
       endoth)
    = ESSDS .
   
  eq getOps(error(QIL)) = none .
  eq getOps(mod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endm) 
    = EOPDS .
  eq getOps(th MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endth) 
    = EOPDS .
  eq getOps(fmod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfm) 
    = EOPDS .
  eq getOps(fth MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfth) 
    = EOPDS .
  eq getOps(
       omod MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
       endom) 
    = EOPDS .
  eq getOps(
       oth MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
       endoth) 
    = EOPDS .
   
  eq getMbs(error(QIL)) = none .
  eq getMbs(mod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endm) 
    = EMAS .
  eq getMbs(th MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endth) 
    = EMAS .
  eq getMbs(fmod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfm) = EMAS .
  eq getMbs(fth MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfth) = EMAS .
  eq getMbs(
       omod MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
       endom) 
    = EMAS .
  eq getMbs(
       oth MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
       endoth) 
    = EMAS .
   
  eq getEqs(error(QIL)) = none .
  eq getEqs(mod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endm) = EqS .
  eq getEqs(th MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endth) = EqS .
  eq getEqs(fmod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfm) = EqS .
  eq getEqs(fth MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfth) = EqS .
  eq getEqs(
       omod MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
       endom) 
    = EqS .
  eq getEqs(
       oth MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
       endoth) 
    = EqS .
   
  eq getRls(error(QIL)) = none .
  eq getRls(mod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endm) = RlS .
  eq getRls(th MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endth) = RlS .
  eq getRls(fmod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfm) = none .
  eq getRls(fth MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfth) = none .
  eq getRls(
       omod MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
       endom) 
    = RlS .
  eq getRls(
       oth MN is 
          PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
       endoth) 
    = RlS .
   
  eq getClasses(error(QIL)) = none .
  eq getClasses(mod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endm) 
    = none .
  eq getClasses(mod MN is IL sorts SS . SSDS OPDS MAS EqS RlS endm) = none .
  eq getClasses(th MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endth) 
    = none .
  eq getClasses(fmod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfm) 
    = none .
  eq getClasses(fmod MN is IL sorts SS . SSDS OPDS MAS EqS endfm) = none .
  eq getClasses(fth MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfth) 
    = none .
  eq getClasses(
       omod MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
       endom) 
    = CDS .
  eq getClasses(
       oth MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
       endoth) 
    = CDS .

  eq getSubclassDecls(error(QIL)) = none .
  eq getSubclassDecls(
       mod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endm) 
    = none .
  eq getSubclassDecls(mod MN is IL sorts SS . SSDS OPDS MAS EqS RlS endm) 
    = none .
  eq getSubclassDecls(
       th MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endth) 
    = none .
  eq getSubclassDecls(
       fmod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfm) 
    = none .
  eq getSubclassDecls(fmod MN is IL sorts SS . SSDS OPDS MAS EqS endfm) 
    = none .
  eq getSubclassDecls(
       fth MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfth) 
    = none .
  eq getSubclassDecls(
       omod MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
       endom)
    = SCDS .
  eq getSubclassDecls(
       oth MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
       endoth)
    = SCDS .

  eq getMsgs(error(QIL)) = none .
  eq getMsgs(mod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endm) 
    = none .
  eq getMsgs(mod MN is IL sorts SS . SSDS OPDS EMAS EqS RlS endm) = none .
  eq getMsgs(th MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endth) 
    = none .
  eq getMsgs(fmod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfm) = none .
  eq getMsgs(fmod MN is IL sorts SS . SSDS OPDS MAS EqS endfm) = none .
  eq getMsgs(fth MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfth) = none .
  eq getMsgs(
       omod MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
       endom) 
    = MDS .
  eq getMsgs(
       oth MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
       endoth) 
    = MDS .

*** Set functions

  eq setImports(error(QIL), EIL) = error(QIL) .
  eq setImports(mod MN is IL sorts SS . SSDS OPDS MAS EqS RlS endm, IL')
    = mod MN is IL' sorts SS . SSDS OPDS MAS EqS RlS endm .
  eq setImports(
       mod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS 
       endm, 
       EIL')
    = mod MN is PL EIL' sorts ESS . ESSDS EOPDS EMAS EqS RlS endm .
  eq setImports(
       th MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS 
       endth, 
       EIL')
    = th MN is PL EIL' sorts ESS . ESSDS EOPDS EMAS EqS RlS endth .
  eq setImports(fmod MN is IL sorts SS . SSDS OPDS MAS EqS endfm, IL')
    = fmod MN is IL' sorts SS . SSDS OPDS MAS EqS endfm .
  eq setImports(fmod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfm, EIL')
    = fmod MN is PL EIL' sorts ESS . ESSDS EOPDS EMAS EqS endfm .
  eq setImports(fth MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfth, EIL')
    = fth MN is PL EIL' sorts ESS . ESSDS EOPDS EMAS EqS endfth .
  eq setImports(
       omod MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
       endom, EIL')
    = omod MN is PL EIL' sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
      endom .
  eq setImports(
       oth MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
       endoth, 
       EIL')
    = oth MN is PL EIL' sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
      endoth .

  eq setOps(error(QIL), EOPDS) = error(QIL) .
  eq setOps(U, error(QIL)) = error(QIL) .
  eq setOps(error(QIL), error(QIL') EOPDS) = error(QIL QIL') .
  eq setOps(mod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endm, EOPDS')
    = mod MN is PL EIL sorts ESS . ESSDS EOPDS' EMAS EqS RlS endm .
  eq setOps(mod MN is IL sorts SS . SSDS OPDS MAS EqS RlS endm, OPDS')
    = mod MN is IL sorts SS . SSDS OPDS' MAS EqS RlS endm .
  eq setOps(th MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endth, EOPDS')
    = th MN is PL EIL sorts ESS . ESSDS EOPDS' EMAS EqS RlS endth .
  eq setOps(fmod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfm, EOPDS')
    = fmod MN is PL EIL sorts ESS . ESSDS EOPDS' EMAS EqS endfm .
  eq setOps(fmod MN is IL sorts SS . SSDS OPDS MAS EqS endfm, OPDS')
    = fmod MN is IL sorts SS . SSDS OPDS' MAS EqS endfm .
  eq setOps(fth MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfth, EOPDS')
    = fth MN is PL EIL sorts ESS . ESSDS EOPDS' EMAS EqS endfth .
  eq setOps(
        omod MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
        endom, 
        EOPDS')
    = omod MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS' MDS EMAS EqS RlS 
      endom .
  eq setOps(
        oth MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
        endoth, 
        EOPDS')
    = oth MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS' MDS EMAS EqS RlS 
      endoth .

  eq setSubsorts(error(QIL), ESSDS) = error(QIL) .
  eq setSubsorts(mod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endm, 
        ESSDS')
    = mod MN is PL EIL sorts ESS . ESSDS' EOPDS EMAS EqS RlS endm .
  eq setSubsorts(mod MN is IL sorts SS . SSDS OPDS MAS EqS RlS endm, SSDS')
    = mod MN is IL sorts SS . SSDS' OPDS MAS EqS RlS endm . 
  eq setSubsorts(th MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endth, 
        ESSDS')
    = th MN is PL EIL sorts ESS . ESSDS' EOPDS EMAS EqS RlS endth .
  eq setSubsorts(fmod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfm, 
        ESSDS')
    = fmod MN is PL EIL sorts ESS . ESSDS' EOPDS EMAS EqS endfm .
  eq setSubsorts(fmod MN is IL sorts SS . SSDS OPDS MAS EqS endfm, SSDS')
    = fmod MN is IL sorts SS . SSDS' OPDS MAS EqS endfm .
  eq setSubsorts(fth MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfth, 
        ESSDS')
    = fth MN is PL EIL sorts ESS . ESSDS' EOPDS EMAS EqS endfth .
  eq setSubsorts(
        omod MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
        endom, 
        ESSDS')
    = omod MN is PL EIL sorts ESS . ESSDS' CDS SCDS EOPDS MDS EMAS EqS RlS 
      endom .
  eq setSubsorts(
        oth MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
        endoth, 
        ESSDS')
    = oth MN is PL EIL sorts ESS . ESSDS' CDS SCDS EOPDS MDS EMAS EqS RlS 
      endoth . 

  eq setMbs(error(QIL), EMAS) = error(QIL) .
  eq setMbs(U, error(QIL) EMAS) = error(QIL) .
  eq setMbs(mod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endm, EMAS')
    = mod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS' EqS RlS endm .
  eq setMbs(mod MN is IL sorts SS . SSDS OPDS MAS EqS RlS endm, MAS')
    = mod MN is IL sorts SS . SSDS OPDS MAS' EqS RlS endm .
  eq setMbs(th MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endth, EMAS')
    = th MN is PL EIL sorts ESS . ESSDS EOPDS EMAS' EqS RlS endth .
  eq setMbs(fmod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfm, EMAS')
    = fmod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS' EqS endfm .
  eq setMbs(fmod MN is IL sorts SS . SSDS OPDS MAS EqS endfm, MAS')
    = fmod MN is IL sorts SS . SSDS OPDS MAS' EqS endfm .
  eq setMbs(fth MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfth, EMAS')
    = fth MN is PL EIL sorts ESS . ESSDS EOPDS EMAS' EqS endfth .
  eq setMbs(
        omod MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
        endom, 
        EMAS')
    = omod MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS' EqS RlS 
        endom .
  eq setMbs(
        oth MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
        endoth, 
        EMAS')
    = oth MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS' EqS RlS 
      endoth .

  eq setEqs(error(QIL), EqS) = error(QIL) .
  eq setEqs(U, error(QIL) EqS?:[EquationSet]) = error(QIL) .
  eq setEqs(error(QIL), error(QIL') EqS?:[EquationSet]) = error(QIL QIL') .
  eq setEqs(mod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endm, EqS')
    = mod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS' RlS endm .
  eq setEqs(mod MN is IL sorts SS . SSDS OPDS MAS EqS RlS endm, EqS')
    = mod MN is IL sorts SS . SSDS OPDS MAS EqS' RlS endm .
  eq setEqs(th MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endth, EqS')
    = th MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS' RlS endth .
  eq setEqs(fmod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfm, EqS')
    = fmod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS' endfm .
  eq setEqs(fmod QI is IL sorts SS . SSDS OPDS MAS EqS endfm, EqS')
    = fmod QI is IL sorts SS . SSDS OPDS MAS EqS' endfm .
  eq setEqs(fth MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfth, EqS')
    = fth MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS' endfth .
  eq setEqs(
        omod MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
        endom, 
        EqS')
    = omod MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS' RlS 
      endom .
  eq setEqs(
        oth MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
        endoth, 
        EqS')
    = oth MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS' RlS 
      endoth .

  op setRls : [Unit] [RuleSet] -> [Unit] .
  var U? : [Unit] .
  var RlS? : [RuleSet] .

  eq setRls(error(QIL), RlS?) = error(QIL) .
  eq setRls(U?, error(QIL) RlS?) = error(QIL) .
  eq setRls(mod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endm, RlS')
    = mod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS' endm .
  eq setRls(mod MN is IL sorts SS . SSDS OPDS MAS EqS RlS endm, RlS')
    = mod MN is IL sorts SS . SSDS OPDS MAS EqS RlS' endm .
  eq setRls(th MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endth, RlS')
    = th MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS' endth .
  eq setRls(fmod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfm, RlS)
    = if RlS == none 
      then fmod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfm
      else mod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endm
      fi .
  eq setRls(fmod QI is IL sorts SS . SSDS OPDS MAS EqS endfm, RlS)
    = if RlS == none 
      then fmod QI is IL sorts SS . SSDS OPDS MAS EqS endfm
      else mod QI is IL sorts SS . SSDS OPDS MAS EqS RlS endm
      fi .
  eq setRls(fth MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfth, RlS)
    = if RlS == none 
      then fmod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfm
      else mod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endm
      fi .
  eq setRls(omod MN is 
              PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
            endom, RlS')
    = omod MN is 
        PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS' 
      endom .
  eq setRls(oth MN is 
              PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
            endoth, RlS')
    = oth MN is 
        PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS' 
      endoth .

  eq setSorts(error(QIL), ESS) = error(QIL) .
  eq setSorts(mod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endm, ESS')
    = mod MN is PL EIL sorts ESS' . ESSDS EOPDS EMAS EqS RlS endm .
  eq setSorts(mod MN is IL sorts SS . SSDS OPDS MAS EqS RlS endm, SS')
    = mod MN is IL sorts SS' . SSDS OPDS MAS EqS RlS endm .
  eq setSorts(th MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endth, ESS')
    = th MN is PL EIL sorts ESS' . ESSDS EOPDS EMAS EqS RlS endth .
  eq setSorts(fmod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfm, ESS')
    = fmod MN is PL EIL sorts ESS' . ESSDS EOPDS EMAS EqS endfm .
  eq setSorts(fmod MN is IL sorts SS . SSDS OPDS MAS EqS endfm, SS')
    = fmod MN is IL sorts SS' . SSDS OPDS MAS EqS endfm .
  eq setSorts(fth MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfth, ESS')
    = fth MN is PL EIL sorts ESS' . ESSDS EOPDS EMAS EqS endfth .
  eq setSorts(
        omod MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
        endom, 
        ESS')
    = omod MN is PL EIL sorts ESS' . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
      endom .
  eq setSorts(
        oth MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
        endoth, 
        ESS')
    = oth MN is PL EIL sorts ESS' . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
      endoth .

  eq setPars(mod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endm, PL')
    = mod MN is PL' EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endm .
  eq setPars(th MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endth, PL')
    = th MN is PL' EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endth .
  eq setPars(fmod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfm, PL')
    = fmod MN is PL' EIL sorts ESS . ESSDS EOPDS EMAS EqS endfm .
  eq setPars(fth MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfth, PL')
    = fth MN is PL' EIL sorts ESS . ESSDS EOPDS EMAS EqS endfth .
  eq setPars(
        omod MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
        endom, 
        PL')
    = omod MN is PL' EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
      endom .
  eq setPars(
        oth MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
        endoth, 
        PL')
    = oth MN is PL' EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
      endoth .

  eq setClasses(
        omod MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
        endom, 
        CDS')
    = omod MN is PL EIL sorts ESS . ESSDS CDS' SCDS EOPDS MDS EMAS EqS RlS 
      endom .
  eq setClasses(
        oth MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
        endoth, 
        CDS')
    = oth MN is PL EIL sorts ESS . ESSDS CDS' SCDS EOPDS MDS EMAS EqS RlS 
      endoth .

  eq setSubclasses(
        omod MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
        endom,
        SCDS')
    = omod MN is PL EIL sorts ESS . ESSDS CDS SCDS' EOPDS MDS EMAS EqS RlS 
      endom .
  eq setSubclasses(
        oth MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
        endoth,
        SCDS')
    = oth MN is PL EIL sorts ESS . ESSDS CDS SCDS' EOPDS MDS EMAS EqS RlS 
      endoth .

  eq setMsgs(
        omod MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
        endom, 
        MDS')
    = omod MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS' EMAS EqS RlS 
      endom .
  eq setMsgs(
        oth MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
        endoth, 
        MDS')
    = oth MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS' EMAS EqS RlS 
      endoth .

  eq setName(mod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endm, MN') 
    = mod MN' is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endm .
  eq setName(mod MN is IL sorts SS . SSDS OPDS MAS EqS RlS endm, MN') 
    = mod MN' is IL sorts SS . SSDS OPDS MAS EqS RlS endm .
  eq setName(fmod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfm, MN') 
    = fmod MN' is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfm .
  eq setName(fmod MN is IL sorts SS . SSDS OPDS MAS EqS endfm, MN') 
    = fmod MN' is IL sorts SS . SSDS OPDS MAS EqS endfm .
  eq setName(fth MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfth, MN') 
    = fth MN' is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfth .
  eq setName(th MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endth, MN') 
    = th MN' is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endth .
  eq setName(
        omod MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
        endom, 
        MN') 
    = omod MN' is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
      endom .
  eq setName(
        oth MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
        endoth, 
        MN') 
    = oth MN' is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
      endoth .
  eq setName(error(QIL), MN') = error(QIL) .

*** Add functions

  eq addSorts(ESS, U) = setSorts(U, (ESS ; getSorts(U))) .

  eq addSubsorts(ESSDS, U) = setSubsorts(U, (ESSDS getSubsorts(U))) .
  eq addSubsorts(error(QIL), U) = error(QIL) .

  eq addOps(EOPDS, U) = setOps(U, (EOPDS getOps(U))) .
  eq addOps(EOPDS?, error(QIL)) = error(QIL) .

  eq addMbs(EMAS, U) = setMbs(U, (EMAS getMbs(U))) .
  eq addEqs(EqS, U) = setEqs(U, (EqS getEqs(U))) .
  eq addRls(RlS, U) = setRls(U, (RlS getRls(U))) .
  eq addImports(EIL, U) = setImports(U, (getImports(U) EIL)) .
  eq addClasses(CDS, U) = setClasses(U, (getClasses(U) CDS)) .
  eq addSubclasses(SCDS, U) = setSubclasses(U, (getSubclassDecls(U) SCDS)) .
  eq addMsgs(MDS, U) = setMsgs(U, (getMsgs(U) MDS)) .

*** Creation of empty units

  eq emptyFModule(MN) 
    = fmod modNameToQid(MN) is nil sorts none . none none none none endfm .
  eq emptyStrFModule 
    = fmod nullModName is nilParList nil sorts none . none none none none 
      endfm .
  eq emptyStrSModule
    = mod nullModName is nilParList nil sorts none . none none none none none 
      endm . 
  eq emptyStrOModule
    = omod 
        nullModName is nilParList nil sorts none . 
        none none none none none none none none
      endom . 

  eq emptyStrFTheory
    = fth nullModName is nilParList nil sorts none . none none none none 
      endfth .

  eq emptyStrSTheory
    = th nullModName is nilParList nil sorts none . none none none none none 
      endth .

  eq emptyStrOTheory
    = oth nullModName is
         nilParList nil sorts none . none none none none none none none none
      endoth .

*** \texttt{empty} returns an empty unit of the same type of the one given as argument.
  
  eq empty(mod MN is IL sorts SS . SSDS OPDS MAS EqS RlS endm)
    = (mod MN is nil sorts none . none none none none none endm) .
  eq empty(mod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endm)
    = (mod MN is nilParList nil sorts none . none none none none none endm) .
  eq empty(th MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endth)
    = (th MN is nilParList nil sorts none . none none none none none endth) .
  eq empty(fmod MN is IL sorts SS . SSDS OPDS MAS EqS endfm)
    = (fmod MN is nil sorts none . none none none none endfm) .
  eq empty(fmod MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfm)
    = (fmod MN is nilParList nil sorts none . none none none none endfm) .
  eq empty(fth MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfth)
    = (fth MN is nilParList nil sorts none . none none none none endfth) .
  eq empty(
        omod MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
        endom)
    = (omod MN is 
         nilParList nil sorts none . none none none none none none none none 
       endom) .
  eq empty(
        oth MN is PL EIL sorts ESS . ESSDS CDS SCDS EOPDS MDS EMAS EqS RlS 
        endoth)
    = (oth MN is 
          nilParList nil sorts none . none none none none none none none none 
       endoth) .

*** In the following \texttt{addDecls} function, the declarations of the unit
*** given as second argument are added to the unit given as first argument.

  eq addDecls(error(QIL), U) = error(QIL) .
  eq addDecls(U, error(QIL)) = error(QIL) .
  ceq addDecls(U, U')
    = addImports(getImports(U'),
        addSorts(getSorts(U'),
          addSubsorts(getSubsorts(U'),
            addOps(getOps(U'),
              addMbs(getMbs(U'),
                addEqs(getEqs(U'), 
                  if U :: FUnit 
                  then U
                  else addRls(getRls(U'), 
                         if U :: SUnit 
                         then U
                         else addClasses(getClasses(U'),
                                addSubclasses(getSubclassDecls(U'),
                                  addMsgs(getMsgs(U'), U)))
                         fi)
                  fi))))))
    if ((U :: StrModule) or (U :: StrTheory)) 
       and ((U' :: StrModule) or (U' :: StrTheory)) .
endfm

*******************************************************************************

***
*** The Abstract Data Type \texttt{View}
***

*** In this section we present the data type \texttt{View} for views.
*** Basically, the data elements of sort \texttt{View} are composed by the
*** name of the view, the names of the source and target units, and a set of
*** maps representing the maps asserting how the given target unit is claimed 
*** to satisfy the source theory (see Section~\ref{Views}).

*** Internally, renaming maps are considered to be a particular case of view
*** maps. The sort \texttt{ViewMap} is declared as a supersort of
*** \texttt{Map}. The only kind of maps in sort \texttt{ViewMap} not in sort
*** \texttt{Map} are maps of operators going to derived operators. We start
*** introducing the declarations for renaming maps and sets of renaming maps
*** in Section~\ref{renaming-maps}, we then introduce view maps and sets of
*** view maps in Section~\ref{view-maps}, and finally we introduce the sort 
*** \texttt{View}, its constructor, and some operations on it in 
*** Section~\ref{viewADT}.

***
*** View Maps
***

*** In addition to the maps of sort \texttt{Map} declared in the \texttt{MAP}
*** module, in views there can also be maps from operators to derived
*** operators, that is, terms with variables (see Section~\ref{Views}). Maps
*** of this kind are given with the constructor \texttt{termMap}, which, in
*** addition to the source and target terms, takes the set of variable
*** declarations for the variables used in the map. The source term must be of
*** the form $\texttt{F(X}_1\texttt{,}\ldots,\texttt{X}_n\texttt{)}$, where
*** \texttt{F} is an operator name declared with $n$ arguments of sorts in the
*** connected components of the variables $\texttt{X}_1\ldots\texttt{X}_n$,
*** respectively. We will see in Section~\ref{view-processing} how in the 
*** initial processing of a view the variables declared in it are associated 
*** to each of the maps in which they are used.

fmod VIEW-MAP is
  pr MAP .
  pr EXT-DECL .

  sort TermMap .
  op termMap : Term Term -> TermMap .

  sorts ViewMap Set`(ViewMap`) .
  subsorts Map TermMap < ViewMap .
  subsorts ViewMap MapSet < Set`(ViewMap`) .
  op _,_ : Set`(ViewMap`) Set`(ViewMap`) -> Set`(ViewMap`) [assoc comm id: none] .

  var VMAP : ViewMap .
  var VMAPS : Set`(ViewMap`) .

*** As for sets of maps, \texttt{SortMapSet} returns the subset of sort maps 
*** in a set of view maps.

  op sortMapSet : Set`(ViewMap`) -> MapSet .

  eq sortMapSet((VMAP, VMAPS))
    = if VMAP :: SortMap
      then (VMAP, sortMapSet(VMAPS))
      else sortMapSet(VMAPS)
      fi .
  eq sortMapSet(none) = none .
endfm

*******************************************************************************

***
*** Views
***

*** The \texttt{View} sort is introduced in the following module
*** \texttt{VIEW}.  In addition to the constructor for views (\texttt{view}),
*** selector functions are added for each of the components of a
*** view (\texttt{name}, \texttt{source}, \texttt{target}, and 
*** \texttt{mapSet}), and a constant \texttt{emptyView}, which is identified 
*** in an equation with the empty view, is defined.

*** Although the declaration of the constructor for views includes an argument
*** for the list of parameters, parameterized views are not handled yet, so at
*** present this argument must be set to the \texttt{nilParList}.


fmod VIEW is
  pr UNIT .
  pr VIEW-MAP .

  sort View .
  op view : ViewExp List`(Parameter`) ModExp ModExp Set`(ViewMap`) -> View 
       [ctor format (nir! o)] .
  op noView : -> View [ctor] .
  op error : QidList -> [View] [ctor format (r o)] .

  var  QI : Qid .
  vars VE VE' : ViewExp .
  vars PL PL' : List`(Parameter`) .
  vars ME ME' ME'' : ModExp .
  vars VMAPS VMAPS' : Set`(ViewMap`) .
  var  QIL : QidList .

  op name : View -> ViewExp .
  op getParList : [View] -> List`(Parameter`) .
  op source : View -> ModExp .
  op target : View -> ModExp .
  op mapSet : View -> Set`(ViewMap`) .

  eq name(view(VE, PL, ME, ME', VMAPS)) = VE .
  eq getParList(view(VE, PL, ME, ME', VMAPS)) = PL .
  eq getParList((error(QIL)).View) = error(QIL) .
  eq target(view(VE, PL, ME, ME', VMAPS)) = ME' .
  eq source(view(VE, PL, ME, ME', VMAPS)) = ME .
  eq mapSet(view(VE, PL, ME, ME', VMAPS)) = VMAPS .

  op setName : View ViewExp -> View .
  op setPars : View List`(Parameter`) -> View .
  op setTarget : View ModExp -> View .
  op setSource : View ModExp -> View .
  op setMapSet : View Set`(ViewMap`) -> View .

  eq setName(view(VE, PL, ME, ME', VMAPS), VE') 
    = view(VE', PL, ME, ME', VMAPS) .
  eq setPars(view(VE, PL, ME, ME', VMAPS), PL') 
    = view(VE, PL', ME, ME', VMAPS) .
  eq setSource(view(VE, PL, ME, ME', VMAPS), ME'') 
    = view(VE, PL, ME'', ME', VMAPS) .
  eq setTarget(view(VE, PL, ME, ME', VMAPS), ME'') 
    = view(VE, PL, ME, ME'', VMAPS) .
  eq setMapSet(view(VE, PL, ME, ME', VMAPS), VMAPS') 
    = view(VE, PL, ME, ME', VMAPS') .

  op emptyView : Qid ModExp ModExp -> View .

  eq emptyView(QI, ME, ME') = view(QI, nilParList, ME, ME', none) .
endfm

*******************************************************************************

***
*** The Abstract Data Type \texttt{Database}
***

*** In this section we present the data type \texttt{Database}, which will be
*** used to store information about the units and views in the system. Before
*** discussing this data type in Section~\ref{databaseADT}, we present the
*** predefined units added in Full Maude to those already available in Core 
*** Maude.

*** 
*** Non-Built-In Predefined Modules
***

*** As we shall see in the following section, except for the
*** \texttt{LOOP-MODE} module, all the predefined modules that are available
*** in Core Maude are also available in Full Maude. In addition to these Core
*** Maude predefined modules, in Full Maude there are some additional
*** predefined units. In the present system, the only units with which the
*** database is initialized are the functional theory \texttt{TRIV}, the
*** module \texttt{CONFIGURATION}, and the module \texttt{UP}, which will be 
*** used to evaluate the \texttt{up} functions. We shall see in 
*** Section~\ref{main-module} how new predefined modules can be added to the 
*** initial database.

fmod PREDEF-UNITS is
  pr UNIT .

  op TRIV : -> StrFTheory .
  eq TRIV = (fth 'TRIV is 
                nilParList
                nil
                sorts 'Elt . 
                none 
                none 
                none 
                none 
             endfth) .

  op CONFIGURATION+ : -> StrModule .
  eq CONFIGURATION+ 
    = (mod 'CONFIGURATION+ is
          nilParList
          including 'CONFIGURATION .
          sorts none .
          none
          op '<_:_|`> : 'Oid 'Cid -> 'Object [none] .
          op 'class : 'Object -> 'Cid [none] .
          none
          eq '<_:_|`>['O:Oid, 'C:Cid] 
            = '<_:_|_>['O:Oid, 'C:Cid, 'none.AttributeSet] 
            [none] .
          eq 'class['<_:_|_>['O:Oid, 'C:Cid, 'A:AttributeSet]] 
            = 'C:Cid 
            [none] .
          none
       endm) .

***(
  eq CONFIGURATION+ 
    = (mod 'CONFIGURATION+ is
          *** nilParList
          including 'CONFIGURATION .
          sorts none .
          none
          op '<_:_|`> : 'Oid 'Cid -> 'Object [none] .
          op 'class : 'Object -> 'Cid [none] .
          none
          eq 'bubble['< 'O:Oid ': 'C:Cid '| '>]
            = 'bubble['< 'O:Oid ': 'C:Cid '| 'none.AttributeSet '>] 
            [none] .
          eq 'bubble['class '`( '< 'O:Oid ': 'C:Cid '| 'A:AttributeSet '>]
            = 'bubble['C:Cid] 
            [none] .
          none
       endm) .
)

*** The following module \texttt{UP} contains the necessary declarations to
*** be able to parse the \texttt{up} functions presented in
*** Section~\ref{structured-specifications}. We shall see in
*** Section~\ref{evaluation} how a declaration importing the following module
*** \texttt{UP} is added to all the modules importing the predefined module
*** \texttt{META-LEVEL}. With this declaration, it is possible to parse the
*** \texttt{up} commands in the bubbles of such modules or in commands being 
*** evaluated in such modules. We shall see in Section~\ref{bubble-parsing} 
*** how these commands are then evaluated.

  op UP : -> StrFModule .
  eq UP
    = (fmod 'UP is
          *** nilParList
          including 'QID-LIST .
          including 'META-LEVEL .
          sorts 'Token ; 'Bubble .
          none
          op 'token : 'Qid -> 'Token 
               [special(
                 (id-hook('Bubble, '1 '1)
                  op-hook('qidSymbol, '<Qids>, nil, 'Qid)))] .
          op 'bubble : 'QidList -> 'Bubble 
               [special(
                 (id-hook('Bubble, '1 '-1 '`( '`))
                  op-hook('qidListSymbol, '__, 'QidList 'QidList, 'QidList)
                  op-hook('qidSymbol, '<Qids>, nil, 'Qid)))] .
          op 'up : 'Token 'Bubble -> 'Term [none] .
          op 'up : 'Token -> 'Module [none] .
          none
          none
       endfm) .

  op SET : -> StrFModule .
  eq SET
    = (fmod 'SET is
          par 'X :: 'TRIV
          protecting par 'X :: 'TRIV .
          protecting 'BOOL .
          sorts eSort('Set, 'X) .
          subsort 'X@Elt < eSort('Set, 'X) .
          op '__ : eSort('Set, 'X) eSort('Set, 'X) -> eSort('Set, 'X) 
             [assoc comm ctor id('mt.Set`(X`))] .
          op 'mt : nil -> eSort('Set, 'X) [ctor] .
          none
          none
       endfm)  .

endfm


*******************************************************************************

***
*** 7 The Evaluation of Views
***

*** Before being entered into the database, besides containing bubbles, views
*** have a somewhat different structure from that of the views given in
*** Section~\ref{viewADT}. We introduce in the following module a sort
*** \texttt{PreView} with constructor \texttt{view}, which is declared as the
*** constructor for views of sort \texttt{View}, but with an additional
*** argument, namely, a set of variable declarations to hold the declarations
*** of variables in the view. During the processing of views (see
*** Section~\ref{view-processing}), which takes place once the parsing process 
*** has concluded, these variables are associated with the corresponding maps 
*** where they are used, generating a term of sort \texttt{View}.

*** We start by introducing in the following module \texttt{PRE-VIEW-MAP} the
*** sorts \texttt{TermPreMap}, \texttt{PreViewMap}, and
*** \texttt{Set`(PreViewMap`)}. A preview map is a view map with bubbles. Note
*** that the bubbles can only appear in term maps. Elements of sort
*** \texttt{TermPreMap} are built with the constructor \texttt{preTermMap},
*** which takes two terms of sort \texttt{Term}, that is, two bubbles. In the
*** processing of views (see Section~\ref{view-processing}), elements of sort
*** \texttt{PreTermMap} will be converted into elements of sort 
*** \texttt{TermMap} by parsing the bubbles in them, and by associating to 
*** them the variables in them defined in the view in which the maps appear.

fmod PRE-VIEW-MAP is
  pr VIEW-MAP .

  sort TermPreMap .
  op preTermMap : Term Term -> TermPreMap .

  sorts PreViewMap Set`(PreViewMap`) .
  subsorts Map TermPreMap < PreViewMap .
  subsorts PreViewMap Set`(ViewMap`) < Set`(PreViewMap`) .
  op _,_ : Set`(PreViewMap`) Set`(PreViewMap`) -> Set`(PreViewMap`) [assoc comm id: none] .

  var PVMAP : PreViewMap .
  var PVMAPS : Set`(PreViewMap`) .

*** Given a set of maps, the function \texttt{sortMapSet} returns the subset 
*** of sort maps in it.

  op sortMapSet : Set`(PreViewMap`) -> MapSet .

  eq sortMapSet((PVMAP, PVMAPS))
    = if PVMAP :: SortMap
      then (PVMAP, sortMapSet(PVMAPS))
      else sortMapSet(PVMAPS)
      fi .
  eq sortMapSet(none) = none .

endfm

*******************************************************************************

fmod PRE-VIEW is
  pr UNIT .
  pr PRE-VIEW-MAP .

  sort PreView .
  op view : ViewExp List`(Parameter`) ModExp ModExp EOpDeclSet Set`(PreViewMap`) 
       -> PreView .
  op noView : -> PreView .

  op name : PreView -> ViewExp .
  op getParList : PreView -> List`(Parameter`) .
  op source : PreView -> ModExp .
  op target : PreView -> ModExp .
  op vars : PreView -> EOpDeclSet .
  op mapSet : PreView -> Set`(PreViewMap`) .

  var  QI : Qid .
  vars ME ME' : ModExp .
  var  VE : ViewExp .
  vars PL PL' : List`(Parameter`) .
  vars VDS VDS' : EOpDeclSet .
  vars PVMAPS PVMAPS' : Set`(PreViewMap`) .

  eq name(view(VE, PL, ME, ME', VDS, PVMAPS)) = VE .
  eq getParList(view(VE, PL, ME, ME', VDS, PVMAPS)) = PL .
  eq target(view(VE, PL, ME, ME', VDS, PVMAPS)) = ME' .
  eq source(view(VE, PL, ME, ME', VDS, PVMAPS)) = ME .
  eq vars(view(VE, PL, ME, ME', VDS, PVMAPS)) = VDS .
  eq mapSet(view(VE, PL, ME, ME', VDS, PVMAPS)) = PVMAPS .

*** The following functions can be used to add new declarations to the set of
*** declarations already in a preview.

  op addMapSet : Set`(PreViewMap`) PreView -> PreView .
  op addVars : OpDeclSet PreView -> PreView .

  eq addMapSet(PVMAPS, view(VE, PL, ME, ME', VDS, PVMAPS')) 
    = view(VE, PL, ME, ME', VDS, (PVMAPS, PVMAPS')) .

  eq addVars(VDS, view(VE, PL, ME, ME', VDS', PVMAPS)) 
    = view(VE, PL, ME, ME', VDS VDS', PVMAPS) .

  op setPars : PreView List`(Parameter`) -> PreView .
  eq setPars(view(VE, PL, ME, ME', VDS, PVMAPS), PL') 
    = view(VE, PL', ME, ME', VDS, PVMAPS) .

  op emptyPreView : Qid ModExp ModExp -> PreView .
  eq emptyPreView(QI, ME, ME') 
    = view(QI, nilParList, ME, ME', none, none, none) .

endfm

*******************************************************************************

***
*** The Database
***

*** In order to be able to refer to modules by name, which is extremely useful
*** for module definition purposes at the user level, the evaluation of module
*** expressions takes place in the context of a database, in which we keep
*** information about the modules already introduced in the system, and also
*** about those modules generated internally.  This information is stored as
*** a set of elements of sort \texttt{UnitInfo} and \texttt{ViewInfo}, in
*** which we hold, respectively, the information concerning units and views. 
*** For each unit we save: 
*** \begin{itemize} 
*** \item Its original form, as introduced by the user, or, in case of an 
***       internally generated unit, as generated from the original form of 
***       some other unit.  
*** \item Its internal representation, in which variables have been renamed 
***       to avoid collisions with the names of variables in other units in 
***       the same hierarchy.  In the case of object-oriented units, we store 
***       its equivalent system module, that is, the result of transforming 
***       it into a system module.  
*** \item Its signature, which is given as a functional module of sort 
***       \texttt{FModule} with no axioms, ready to be used in calls to 
***       \texttt{metaParse}. There can only be importation declarations 
***       including built-in modules in this module. These are the only 
***       inclusions handled by the Core Maude engine.  
*** \item Its flattened version, for which, as for signatures, only the 
***       importation of built-in modules is left unevaluated.  
*** \end{itemize} 
*** For each view we keep its name and the view itself.

*** As a simple mechanism to keep the database consistent, for each unit we
*** maintain the list of names of all the units and views ``depending'' on it.
*** Similarly, for each view we maintain the list of names of all the units
*** ``depending'' on it. The idea is that if a unit or view is redefined or
*** removed, all those units and/or views depending on it will also be
*** removed. This dependency does not only mean direct importation. For
*** example, the module resulting from the renaming of some module also
*** depends on the module being renamed; the instantiation of a parameterized
*** module also depends on the parameterized module and on all the views used
*** in its instantiation; a view depends on its source and target units, etc.
*** This dependency is transitive: if a module, theory, or view has to be
*** removed, all the units and/or views depending on them will be removed as
*** well. The dependencies derived from the module expressions themselves are
*** established by the function \texttt{setUpModExpDeps}. The function
*** \texttt{setUpUnitDependencies} calls \texttt{setUpModExpDeps}, 
*** and then \texttt{setUpImportSetDependencies} to add the \emph{back 
*** references} in the modules being imported. The function 
*** \texttt{setUpViewDeps} sets up the back references for the views 
*** being introduced.

*** In addition to this set of information cells for units and views, we also
*** keep lists with the names of all the units and views in the database, and
*** a list of quoted identifiers in which we store the messages generated
*** during the process of treatment of the inputs in order to simplify the 
*** communication with the read-eval-print loop process.

fmod DATABASE is
  pr VIEW .
  pr PRE-VIEW .

  op procUnit : Qid Database -> Database .
  op procView : Qid Database -> Database .
  *** their definitions are in UNIT-PROCESSING and VIEW-PROCESSING

  op evalModExp : ModExp Database -> Database .
  *** it's definition is in MOD-EXPR-EVAL 

  sort UnitInfo .
  op <_;_;_;_;_;_;_;_> : ModName Default`(Term`) Unit Unit Unit OpDeclSet 
       ModNameSet ViewExpSet -> UnitInfo
       [ctor
        format (nig o g n+++io g nio g nio g nio g nio g nio g nio n---ig o)] .
  op <_;_;_;_;_;_;_;_> : ModName Unit Unit Unit Unit OpDeclSet 
       ModNameSet ViewExpSet -> UnitInfo
       [ctor
        format (nig o g n+++io g nio g nio g nio g nio g nio g nio n---ig o)] .

  *** The sixth arg stores the variables (corresponding ops) in the top
  *** module.

  sort ViewInfo .
  op <_;_;_;_;_> : 
       ViewExp Default`(Term`) View ModNameSet ViewExpSet -> ViewInfo 
       [ctor format (nig o g n+++io g nio g nio g nio n---ig o)] .

  sort InfoSet .
  subsort UnitInfo ViewInfo < InfoSet .
  op emptyInfoSet : -> InfoSet .
  op __ : InfoSet InfoSet -> InfoSet [assoc comm id: emptyInfoSet] .

  sort Database .
  op db : InfoSet ModNameSet ViewExpSet QidList -> Database 
      [ctor
       format (nib i++o)] .

  vars QI X Y : Qid .
  vars QIL QIL' : QidList .
  vars VE VE' VE'' : ViewExp .
  vars VES VES' VES'' VES''' : ViewExpSet .
  var  IS : InfoSet .
  vars MNS MNS' MNS'' : ModNameSet .
  var  PL : List`(Parameter`) .
  vars ME ME' : ModExp .
  var  VI : View .
  var  VMAPS : Set`(ViewMap`) .
  var  PVMAPS : Set`(PreViewMap`) .
  vars PU PU' U U' U'' U''' : Unit .
  var  DB : Database .
  vars M M' M'' DM DM' : Unit .
  var  EIL : List`(EImport`) .
  vars MN MN' : ModName .
  var  If : Interface .
  var  VIf : ViewInfo .
  var  UIf : UnitInfo . 
  vars VDS VDS' : OpDeclSet .
  var  PV : PreView .
  vars T T' : Term .
  vars DT DT' : Default`(Term`) .

*** The constant \texttt{emptyDatabase} denotes the empty database, and there
*** are predicates \texttt{viewInDatabase} and \texttt{unitInDb} to check,
*** respectively, whether a view and a unit are in a database or not.

  op emptyDatabase : -> Database .
  eq emptyDatabase 
    = db(emptyInfoSet, noneModNameSet, noneViewExpSet, nil) .

  op unitInDb : ModName Database -> Bool .
  op viewInDb : ViewExp Database -> Bool .

  eq viewInDb(VE, db(IS, MNS, VES, QIL)) = VE inViewExpSet VES .

  eq unitInDb(MN, db(IS, MNS, VES, QIL)) = MN inModNameSet MNS .

*** If a module, theory, or view is being redefined, that is, if there was
*** already in the database a module, theory, or view with the same name,
*** then all the units and/or views depending on it are removed using the
*** functions \texttt{delUnits} and \texttt{delViews}. Removing a view 
*** or a unit from the database means removing its info cell from the set of 
*** cells in the database. Those entered by the user are not completely 
*** removed, their term form is saved so that it can be recompiled later.

  op delUnits : ModNameSet Database -> Database .
  op delViews : ViewExpSet Database -> Database .

  eq delUnits((MN . MNS), 
       db(< MN ; DT ; U ; U' ; M ; VDS ; MNS' ; VES > IS, 
          MN . MNS'', VES', QIL))
    = if DT :: Term 
      then delUnits((MNS . MNS'), 
             delViews(VES, 
               db(< MN ; DT ; noUnit ; noUnit ; noUnit ; VDS ; MNS' ; VES > IS,
                  MN . MNS'', VES', QIL )))
      else delUnits((MNS . MNS'), delViews(VES, db(IS, MNS'', VES', QIL)))
      fi .
  eq delUnits((MN . MNS), 
       db(< MN ; DM ; U ; U' ; M ; VDS ; MNS' ; VES > IS, 
          MN . MNS'', VES', QIL))
    = delUnits((MNS . MNS'), 
        delViews(VES, 
          db(< MN ; DM ; noUnit ; noUnit ; noUnit ; VDS ; MNS' ; VES > IS,
            MN . MNS'', VES', QIL ))) .
  ceq delUnits((MN . MNS), DB) = delUnits(MNS, DB) if not unitInDb(MN, DB) .
  eq delUnits(noneModNameSet, DB) = DB .

  ceq delViews((VE # VES), 
       db((< VE ; DT ; VI ; MNS ; VES' > IS), MNS', VES'', QIL))
    = if DT :: Term
      then delViews(VES # VES', 
             delUnits(MNS, 
               db(< VE ; DT ; noView ; MNS ; VES' > IS, MNS', VES'', QIL )))
      else delViews(VES # VES', delUnits(MNS,  db(IS, MNS', VES''', QIL)))
      fi
    if VE # VES''' := VES'' .
  ceq delViews(VE # VES, DB) = delViews(VES, DB) if not viewInDb(VE, DB) .
  eq delViews(noneViewExpSet, DB) = DB .

*** The \texttt{warning} function allows us to place messages (warning, error,
*** or any other kind of messages) in the last argument of the database
*** constructor. These messages are given in the form of quoted identifier
*** lists, and will be passed to the third argument of the read-eval-print 
*** loop, to be printed in the terminal.

  op warning : Database QidList -> Database .
  eq warning(db(IS, MNS, VES, QIL), QIL') 
    = if QIL == nil 
      then db(IS, MNS, VES, QIL') 
      else db(IS, MNS, VES, QIL)
      fi .

*** The constant \texttt{builtIns} denotes the set of identifiers of the
*** predefined modules of Core Maude. It will be used to check whether a
*** particular module is a built-in Core Maude module or not.

  op builtIns : -> ModNameSet .
  eq builtIns 
    = 'TRUTH-VALUE . 'THUTH . 'BOOL . 'EXT-BOOL . 'IDENTICAL . 'NAT . 'INT . 
      'RAT . 'FLOAT . 'STRING . 'CONVERSION . 'QID . 'QID-LIST . 'META-TERM . 
      'META-MODULE . 'META-LEVEL . 'CONFIGURATION . 'LTL . 'LTL-SIMPLIFIER .
      'SAT-SOLVER . 'MODEL-CHECKER .

*** Core Maude built-in modules are handled in a special way in the current
*** version of the system. They are not explicitly defined in the Full Maude
*** database; their importation is directly handled by Core Maude. This has
*** some drawbacks: Core Maude built-in modules cannot be renamed; they cannot
*** be directly used with built-in functions, such as \texttt{metaReduce} or
*** \texttt{sameComponent}, although they can be imported in modules being
*** used in the calls to these functions; and, in general, any function taking
*** as argument or returning as result the metarepresentation of a module
*** cannot take one of these built-in modules as argument. This is the case,
*** for example, for the \texttt{up} function presented in
*** Section~\ref{changing-levels}, or for functions or commands in which the
*** name of a module has to be specified, as the \texttt{select} or
*** \texttt{down} commands, or the \texttt{up} function presented in
*** Section~\ref{structured-specifications}. Nevertheless, there are also 
*** some advantages: The flattening of the built-in part of the structure is 
*** accomplished more efficiently, and, since these modules do not have to be 
*** stored in the database of Full Maude, the size of the database is reduced.

*** Our plan is to have in the future a hybrid solution. Once we have some way
*** of storing the modules entered to Full Maude in Core Maude's database, it
*** will be enough to keep in the Full Maude database just the original form
*** of the top of all the modules, including built-ins, leaving all the
*** importation declarations to be resolved by the engine. The structures will
*** be normalized as they are now, so that the engine will have to deal just
*** with inclusions, but it will be possible to use the predefined modules as 
*** any other module. Moreover, the Full Maude database will be relatively 
*** smaller and the flattening will be computed more efficiently.

*** When a new module or theory is entered, the names of all the modules,
*** theories, and views depending on it are included in its lists of
*** dependencies with functions \texttt{setUpUnitDependencies} and
*** \texttt{setUpViewDeps}. Notice that if new module expressions are
*** defined, the function \texttt{setUpModExpDeps} will have to be 
*** extended accordingly.

  op setUpUnitDeps : Unit Database -> Database .
  op setUpModExpDeps : ModName Database -> Database .
  op setUpModExpDeps : ModName ModName Database -> Database .
  op setUpModExpDeps : ModName ViewExp Database -> Database .
  op setUpImportDeps : ModName List`(EImport`) Database -> Database .

  eq setUpUnitDeps(U, DB)
    = setUpImportDeps(getName(U), getImports(U), 
        setUpModExpDeps(getName(U), DB)) .

  eq setUpModExpDeps((par X :: ME), 
       db((< ME ; DT ; U ; U' ; M ; VDS ; MNS ; VES > IS), 
         MNS', VES', QIL))
    = db((< ME ; DT ; U ; U' ; M ; VDS ; MNS . (par X :: ME) ; VES > IS),
         MNS', VES', QIL) .
  eq setUpModExpDeps((par X :: ME), 
       db((< ME ; DM ; U ; U' ; M ; VDS ; MNS ; VES > IS), 
         MNS', VES', QIL))
    = db((< ME ; DM ; U ; U' ; M ; VDS ; MNS . (par X :: ME) ; VES > IS),
         MNS', VES', QIL) .
  ceq setUpModExpDeps((par X :: ME), DB)
    = warning(DB, 
        ('\r 'Error: '\o 'Module modNameToQidList(ME) 'not 'in 'database. '\n))
    if not unitInDb(ME, DB) .
  eq setUpModExpDeps(QI, DB) = DB .

  eq setUpModExpDeps((par X :: If), DB)
    = setUpModExpDeps((par X :: If), (par X :: If), DB) .

  eq setUpModExpDeps((par X :: par(ME, parList(par Y :: ME', PL))), MN,
       db((< ME' ; DT ; U ; U' ; M ; VDS ; MNS ; VES > IS), 
         MNS', VES', QIL))
    = setUpModExpDeps((par X :: par(ME, PL)), MN,
        db((< ME' ; DT ; U ; U' ; M ; VDS ; MNS . MN ; VES > IS), 
          MNS', VES', QIL)) .
  eq setUpModExpDeps((par X :: par(ME, parList(par Y :: ME', PL))), MN,
       db((< ME' ; DM ; U ; U' ; M ; VDS ; MNS ; VES > IS), 
         MNS', VES', QIL))
    = setUpModExpDeps((par X :: par(ME, PL)), MN,
        db((< ME' ; DM ; U ; U' ; M ; VDS ; MNS . MN ; VES > IS), 
          MNS', VES', QIL)) .
  ceq setUpModExpDeps((par X :: par(ME, parList(par Y :: ME', PL))), 
        MN, DB)
    = setUpModExpDeps((par X :: par(ME, PL)), MN,
        warning(DB, 
          ('\r 'Error: '\o 'Module modNameToQidList(ME') 'not 'in 'database. 
           '\n)))
    if not unitInDb(ME', DB) .
  eq setUpModExpDeps((par X :: par(ME, nilParList)), MN,
       db((< ME ; DT ; U ; U' ; M ; VDS ; MNS ; VES > IS), 
         MNS', VES', QIL))
    = db((< ME ; DT ; U ; U' ; M ; VDS ; MNS . MN ; VES > IS), 
        MNS', VES', QIL) .
  eq setUpModExpDeps((par X :: par(ME, nilParList)), MN,
       db((< ME ; DM ; U ; U' ; M ; VDS ; MNS ; VES > IS), 
         MNS', VES', QIL))
    = db((< ME ; DM ; U ; U' ; M ; VDS ; MNS . MN ; VES > IS), 
        MNS', VES', QIL) .
  ceq setUpModExpDeps((par X :: par(ME, nilParList)), MN, DB)
    = warning(DB, 
        ('\r 'Error: '\o 'Module modNameToQidList(ME) 'not 'in 'database. '\n))
    if not unitInDb(ME, DB) .
  eq setUpModExpDeps(QI, DB) = DB .

  eq setUpImportDeps(MN, ((including MN' .) EIL), 
       db((< MN' ; DT ; U ; U' ; M ; VDS ; MNS ; VES > IS), MNS', VES', QIL))
    = setUpImportDeps(MN, EIL, 
        db((< MN' ; DT ; U ; U' ; M ; VDS ; MNS . MN ; VES > IS), 
           MNS', VES', QIL)) .
  eq setUpImportDeps(MN, ((including MN' .) EIL), 
       db((< MN' ; DM ; U ; U' ; M ; VDS ; MNS ; VES > IS), MNS', VES', QIL))
    = setUpImportDeps(MN, EIL, 
        db((< MN' ; DM ; U ; U' ; M ; VDS ; MNS . MN ; VES > IS), 
           MNS', VES', QIL)) .
  eq setUpImportDeps(MN, ((protecting MN' .) EIL), 
       db((< MN' ; DT ; U ; U' ; M ; VDS ; MNS ; VES > IS), MNS', VES', QIL))
    = setUpImportDeps(MN, EIL, 
        db((< MN' ; DT ; U ; U' ; M ; VDS ; MNS . MN ; VES > IS), 
           MNS', VES', QIL)) .
  eq setUpImportDeps(MN, ((protecting MN' .) EIL), 
       db((< MN' ; DM ; U ; U' ; M ; VDS ; MNS ; VES > IS), MNS', VES', QIL))
    = setUpImportDeps(MN, EIL, 
        db((< MN' ; DM ; U ; U' ; M ; VDS ; MNS . MN ; VES > IS), 
           MNS', VES', QIL)) .
  ceq setUpImportDeps(MN, ((including MN' .) EIL), DB)
    = if MN' inModNameSet builtIns
      then setUpImportDeps(MN, EIL, DB)
      else warning(DB, 
             ('\r 'Error: '\o 'Module modNameToQidList(MN') 'not 'in 'database.
              '\n))
      fi
    if not unitInDb(MN', DB) .
  ceq setUpImportDeps(MN, ((protecting MN' .) EIL), DB)
    = if MN' inModNameSet builtIns
      then setUpImportDeps(MN, EIL, DB)
      else warning(DB, 
             '\r 'Error: '\o 'Module modNameToQidList(MN') 'not 'in 'database. 
             '\n)
      fi
    if not unitInDb(MN', DB) .
  eq setUpImportDeps(MN, nil, DB) = DB .

  op setUpViewDeps : ModExp ViewExp Database -> Database .
  op setUpViewExpDeps : ViewExp Database -> Database .
  op setUpViewExpDeps : ViewExp ViewExp Database -> Database .

  eq setUpViewDeps(ME, VE, 
       db(< ME ; DT ; U ; U' ; M ; VDS ; MNS' ; VES > IS, MNS'', VES', QIL))
    = db(< ME ; DT ; U ; U' ; M ; VDS ; MNS' ; VES # VE > IS, 
        MNS'', VES', QIL) .
  eq setUpViewDeps(ME, VE, 
       db(< ME ; DM ; U ; U' ; M ; VDS ; MNS' ; VES > IS, MNS'', VES', QIL))
    = db(< ME ; DM ; U ; U' ; M ; VDS ; MNS' ; VES # VE > IS, 
        MNS'', VES', QIL) .
  ceq setUpViewDeps(ME, VE, DB)
    = if ME inModNameSet builtIns
      then DB
      else warning(DB, 
             '\r 'Error: '\o 'Module modNameToQidList(ME) 'not 'in 'database. 
             '\n)
      fi
    if not unitInDb(ME, DB) .

  eq setUpViewExpDeps(QI, DB) = DB .
  eq setUpViewExpDeps(QI << VE >>, DB) 
    = setUpViewExpDeps(QI << VE >>, VE, DB) .
  *** eq setUpViewExpDeps(QI { VE }, DB) 
  ***  = setUpViewExpDeps(QI { VE }, VE, DB) .
  *** _;;_

  eq setUpViewExpDeps(VE, QI | VE', 
       db(< QI ; DT ; VI ; MNS ; VES > IS, MNS', VES', QIL))
    = setUpViewExpDeps(VE, VE', 
        db(< QI ; DT ; VI ; MNS ; VE # VES > IS, MNS', VES', QIL)) .
  eq setUpViewExpDeps(VE, QI | VE', DB)
    = setUpViewExpDeps(VE, VE', DB) 
      [owise] .
  eq setUpViewExpDeps(VE, ((QI << VE' >>) |