*** *** Full Maude specification version 2.1.1 *** To be run on Maude 2.1.1 *** *** *** last modification: July 20th, 2004 *** author: Francisco Duran *** ***( 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. ) *** Last changes: *** *** - ditto is correctly handled *** *** - poly is correctly handled *** *** - Error handling has been improved (thanks, Peter) *** *** - 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. *** *** - 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. *** *** - ops names in op declarations *** *** known bugs: *** *** - error messages could be given in down commands *** *** - the check for META-LEVEL inclusions is wrong, it assumes direct *** inclusions *** *** - Check: perhaps we need to convert constans 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: *** *** - 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`(_`) poly`(_`) 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 . ops object msg config : -> 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 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 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 . including QID-LIST . sorts FDeclList SDeclList Module ImportDecl Parameter List 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 extending_. ex_. : ModExp -> ImportDecl . ops protecting_. pr_. : ModExp -> ImportDecl . sorts Interface . subsort Parameter < List . subsorts Token < Interface . *** parameterized module interface op _::_ : Token ModExp -> Parameter [prec 40 gather (e &)] . op _::_ : Token Interface -> Parameter [prec 40 gather (e &)] . op _|_ : List List -> List [assoc] . ***op _`(_`) : Token List -> Interface . op _`(_`) : ModExp List -> 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 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_=>1_. : 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 . *** set commands op set`protect`BOOL`on`. : -> Command . op set`protect`BOOL`off`. : -> Command . endfm ------------------------------------------------------------------------------- ******************************************************************************* ------------------------------------------------------------------------------- fmod FULL-MAUDE-SIGN is including VIEWS . including COMMANDS . pr QID-LIST . 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, ', nil, 'Qid)))] . op 'viewToken : 'Qid -> 'ViewToken [special( (id-hook('Bubble, '1 '1) op-hook('qidSymbol, ', nil, 'Qid)))] . op 'sortToken : 'Qid -> 'SortToken [special( (id-hook('Bubble, '1 '1) op-hook('qidSymbol, ', nil, 'Qid) id-hook('Exclude, '`[ '`] '< 'to '`, '. '`( '`) '| ': 'ditto 'precedence 'prec 'gather 'assoc 'associative 'comm 'commutative 'ctor 'constructor 'id: 'strat 'strategy 'poly 'memo 'memoization 'iter 'frozen 'config 'object 'msg)))] . op 'neTokenList : 'QidList -> 'NeTokenList [special( (id-hook('Bubble, '1 '-1 '`( '`)) op-hook('qidListSymbol, '__, 'QidList 'QidList, 'QidList) op-hook('qidSymbol, ', nil, 'Qid) id-hook('Exclude, '.)))] . op 'bubble : 'QidList -> 'Bubble [special( (id-hook('Bubble, '1 '-1 '`( '`)) op-hook('qidListSymbol, '__, 'QidList 'QidList, 'QidList) op-hook('qidSymbol, ', 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. ******* ******* ERROR HANDLING, by Peter Olveczky ******* *** The following module defines a thing which prints up to n characters *** of a bubble, followed by the usual arrow <---*HERE* which points to the *** erroneous token: ------------------------------------------------------------------------------- ******************************************************************************* ------------------------------------------------------------------------------- fmod PRINT-SYNTAX-ERROR is protecting META-LEVEL . protecting INT . var QIL : QidList . var Q : Qid . var N : Nat . vars RP RP' : ResultPair . var RP? : [ResultPair?] . op printN : Nat QidList -> QidList . *** first N qid's in a qidList eq printN(N, nil) = nil . eq printN(0, QIL) = nil . eq printN(s N, Q QIL) = Q printN(N, QIL) . op removeFront : Nat QidList -> QidList . *** removes first N qid's eq removeFront(N, nil) = nil . eq removeFront(0, QIL) = QIL . eq removeFront(s N, Q QIL) = removeFront(N, QIL) . op printSyntaxError : [ResultPair?] QidList -> QidList . eq printSyntaxError(noParse(N), QIL) = '\r 'Parse 'error 'in '\o '\s printN(N + 1, QIL) '\r '<---*HERE* '\o . eq printSyntaxError(ambiguity(RP, RP'), QIL) = '\r 'Ambiguous 'parsing 'for '\o '\s QIL '\o . eq printSyntaxError(RP?, QIL) = QIL [owise] . endfm ------------------------------------------------------------------------------- ******************************************************************************* ------------------------------------------------------------------------------- *** *** 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. *** *** Extension \texttt{QID-LIST} *** *** 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 QID-LIST . op qidListToQid : QidList -> Qid . var QI : Qid . var QIL : QidList . eq qidListToQid(('\s QIL)) = qid(" " + string(qidListToQid(QIL))) . eq qidListToQid((QI QIL)) = qid(string(QI) + " " + string(qidListToQid(QIL))) [owise] . 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{Set}, 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~_inSet_~ 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 Set . subsort ViewExp < Set . op noneViewExpSet : -> Set . op _#_ : Set Set -> Set [assoc comm id: noneViewExpSet] . eq VE # VE = VE . vars VE VE' : ViewExp . var VES : Set . op _inSet_ : ViewExp Set -> Bool . eq VE inSet (VE' # VES) = (VE == VE') or-else (VE inSet VES) . eq VE inSet 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{Set} 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 [memo] . op viewExpToQidList : ViewExp -> QidList [memo] . 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{Set}. *** 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{Set}, respectively. ------------------------------------------------------------------------------- ******************************************************************************* ------------------------------------------------------------------------------- fmod EXT-SORT is pr META-LEVEL . pr VIEW-EXPR-TO-QID . sort ESort EType EKind . subsort Sort < ESort . subsort ESort EKind Type < EType . op eSort : ESort ViewExp -> ESort . op kind : Set -> EKind . op qidError : QidList -> [ESort] [ctor format (r o)] . var QIL : QidList . var VE : ViewExp . eq eSort(qidError(QIL), VE) = qidError(QIL) . ---eq kind(ES ; ES' ; ESS) = kind(ES) . sort List . subsort EType TypeList < List . op __ : List List -> List [assoc id: nil] . op kind : List -> EType . eq kind(ET ET' ETL) = kind(ET) kind(ET' ETL) . eq kind(nil) = nil . eq kind(kind(ET)) = kind(ET) . sort Set . subsort ESort SortSet < Set . op _;_ : Set Set -> Set [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' : Set . vars ETL ETL' : List . 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 : List -> TypeList . eq eTypeToType(QI) = QI . eq eTypeToType(kind(ES ; ESS)) = qid("[" + string(eTypeToType(ES)) + "]") . eq eTypeToType(eSort(ES, VE)) = qid(string(eTypeToType(ES)) + "(" + string(viewExpToQid(VE)) + ")") . eq eTypeToType(ET ETL) = eTypeToType(ET) eTypeToType(ETL) [owise] . eq eTypeToType(nil) = nil . op eSameKind : Module List List -> 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 -> List . eq termListLeastSort(M, (T, TL)) = (leastSort(M, T) termListLeastSort(M, TL)) . eq termListLeastSort(M, T) = leastSort(M, T) . eq leastSort(M, T) = qidError('Error: 'non-valid 'module) . op _inSortSet_ : ESort Set -> 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 INT . pr EXT-SORT . op eSortToQidList : ESort -> QidList . op eTypeListToQidList : List -> QidList . op eSortSetToQidList : Set -> QidList . op eSortToSort : [List] -> [List] . op eSortToSort : List -> TypeList . op eSortToSort : EType -> Type . op eSortToSort : Set -> 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 : List . var ESS : Set . vars St St' : String . op tokenize : String String -> QidList . eq tokenize(St, St') = if find(St, St', 0) == notFound then qid(St) else qid(substr(St, 0, find(St, St', 0))) tokenize(substr(St, find(St, St', 0) + 1, length(St)), St') fi . eq eSortToSort(qidError(QIL)) = qidError(QIL) . eq eSortToQidList(T) = if T :: Kind then '`[ tokenize(substr(string(T), 2, length(string(T)) + - 4), ",") '`] else T fi . 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) '`]) . eq eSortToSort((ET ETL)) = eSortToSort(ET) eSortToSort(ETL) [owise] . eq eSortToSort((nil).List) = nil . eq eSortToSort((ES ; ESS)) = eSortToSort(ES) ; eSortToSort(ESS) [owise] . eq eSortToSort((none).Set) = 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 . *** : QidList -> [Term] [ctor format (r o)] . sort Default . subsort Term < Default . ops noTerm noView : -> Default . 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 INT-LIST is pr META-MODULE . pr INT . sort IntList . subsort Int NatList < IntList . op __ : IntList IntList -> IntList [ctor assoc] . op numberError : QidList -> [Nat] . endfm ------------------------------------------------------------------------------- ******************************************************************************* ------------------------------------------------------------------------------- fmod EXT-DECL is pr EXT-SORT . pr EXT-TERM . pr INT-LIST . vars ES ES' : ESort . var ESS : Set . var VE : ViewExp . vars F S : Qid . var C : Constant . vars V V' : Variable . var ETL : TermList . var ET : Term . vars QIL QIL' : QidList . var At : Attr . var AtS : AttrSet . *** extended subsort declarations sorts ESubsortDecl Set . subsort SubsortDecl < ESubsortDecl . subsorts SubsortDeclSet ESubsortDecl < Set . op subsort_<_. : ESort ESort -> ESubsortDecl . op __ : Set Set -> Set [ditto] . op subsortDeclError : QidList -> [Set] [ctor format (r o)] . eq ESSD:ESubsortDecl ESSD:ESubsortDecl = ESSD:ESubsortDecl . eq subsortDeclError(QIL) subsortDeclError(QIL') = subsortDeclError(QIL QIL') . *** extended attribute declarations op strat : IntList -> Attr [ditto] . *** to handle on-demand strategies op ditto : -> Attr [ctor] . op _in_ : Attr AttrSet -> Bool . eq At in At AtS = true . *** extended operation declarations sorts EOpDecl Set . subsort OpDecl < EOpDecl . subsorts OpDeclSet EOpDecl < Set . op op_:_->_`[_`]. : Qid List EType AttrSet -> EOpDecl [ditto] . op __ : Set Set -> Set [ditto] . op opDeclError : QidList -> [Set] [ctor format (r o)] . vars EOPD EOPD' : EOpDecl . var EOPDS : Set . eq EOPD EOPD = EOPD . eq opDeclError(QIL) opDeclError(QIL') = opDeclError(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 Set . subsort MembAx < EMembAx . subsorts EMembAx MembAxSet < Set . op mb_:_`[_`]. : Term ESort AttrSet -> EMembAx [ditto] . op cmb_:_if_`[_`]. : Term ESort EEqCondition AttrSet -> EMembAx [ditto] . op __ : Set Set -> Set [ditto] . op membAxError : QidList -> [Set] [ctor format (r o)] . eq MB:EMembAx MB:EMembAx = MB:EMembAx . eq membAxError(QIL) membAxError(QIL') = membAxError(QIL QIL') . *** extended equations sorts EEquation Set . subsort Equation < EEquation EquationSet < Set . op ceq_=_if_`[_`]. : Term Term EEqCondition AttrSet -> EEquation [ditto] . op __ : Set Set -> Set [ditto] . op equationError : QidList -> [Set] [ctor format (r o)] . eq EQ:EEquation EQ:EEquation = EQ:EEquation . eq equationError(QIL) equationError(QIL') = equationError(QIL QIL') . *** extended rules sorts ERule Set . subsort Rule < ERule RuleSet < Set . op crl_=>_if_`[_`]. : Term Term ECondition AttrSet -> ERule [ditto] . op __ : Set Set -> Set [ditto] . op ruleError : QidList -> [Set] [ctor format (r o)] . eq RL:ERule RL:ERule = RL:ERule . eq ruleError(QIL) ruleError(QIL') = ruleError(QIL QIL') . *** The function \verb~_in_~ checks whether a given operator *** declaration is in a set of operator declarations. op _in_ : EOpDecl Set -> 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{List} and \texttt{Set} 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 classDeclError : QidList -> [ClassDeclSet] [ctor format (r o)] . eq classDeclError(QIL) classDeclError(QIL') = classDeclError(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 subclassDeclError : QidList -> [SubclassDeclSet] [ctor format (r o)] . eq subclassDeclError(QIL) subclassDeclError(QIL') = subclassDeclError(QIL QIL') . sorts MsgDecl Set . subsort MsgDecl < Set . op msg_:_->_. : Qid List ESort -> MsgDecl . op none : -> Set . op __ : Set Set -> Set [assoc comm id: none] . eq MD:MsgDecl MD:MsgDecl = MD:MsgDecl . op msgDeclError : QidList -> [Set] [ctor format (r o)] . eq msgDeclError(QIL) msgDeclError(QIL') = msgDeclError(QIL QIL') . *** The function \texttt{classSet} returns the set of class identifiers in *** the set of class declarations given as argument. op classSet : ClassDeclSet -> Set . 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 : Set -> SubsortDeclSet . op eSortToSort : Set -> OpDeclSet . op eSortToSort : Set -> MembAxSet . op eSortToSort : Set -> EquationSet . op eSortToSort : Set -> RuleSet . op eSortToSort : ECondition -> Condition . op eSortToSort : ClassDeclSet -> ClassDeclSet . op eSortToSort : SubclassDeclSet -> SubclassDeclSet . op eSortToSort : Set -> Set . op eSortToSort : AttrDeclSet -> AttrDeclSet . vars QI F V : Qid . var SS : SortSet . vars VE VE' : ViewExp . vars ES ES' : ESort . var ETL : List . var ET : EType . var ESS : Set . vars T T' T'' T''' : Term . var ESSDS : Set . var EOPDS : Set . var AtS : AttrSet . var EMAS : Set . var EqS : Set . var RlS : Set . var CDS : ClassDeclSet . var ADS : AttrDeclSet . var MDS : Set . var SCDS : SubclassDeclSet . vars Cond Cond' : Condition . eq eSortToSort(((subsort ES < ES' .) ESSDS)) = ((subsort eSortToSort(ES) < eSortToSort(ES') .) eSortToSort(ESSDS)) . eq eSortToSort((none).Set) = none . eq eSortToSort(((op F : ETL -> ET [AtS] .) EOPDS)) = ((op F : eSortToSort(ETL) -> eSortToSort(ET) [AtS] .) eSortToSort(EOPDS)) . eq eSortToSort((none).Set) = 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).Set) = 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).Set) = 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).Set) = 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).Set) = none . eq eSortToSort(Cond /\ Cond') = eSortToSort(Cond) /\ eSortToSort(Cond') [owise] . 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{Set}) is then declared as supersort of \texttt{Map} *** with constructors \texttt{none} and \verb~_,_~. ------------------------------------------------------------------------------- ******************************************************************************* ------------------------------------------------------------------------------- fmod MAP is pr EXT-SORT . pr DECL-EXT-SORT-TO-QID . sort Map . subsort Renaming < Map . ----op op_to_`[_`] : Qid Qid AttrSet -> Map [ctor] . op op_:_->_to_`[_`] : Qid List EType Qid AttrSet -> Map [ctor ditto] . op sort_to_ : ESort ESort -> Map [ctor ditto] . ----op label_to_ : Qid Qid -> Map [ctor] . op class_to_ : ESort ESort -> Map . op attr_._to_ : Qid ESort Qid -> Map . op msg_to_ : Qid Qid -> Map . op msg_:_->_to_ : Qid List ESort Qid -> Map . sort Set . subsort Map RenamingSet < Set . op none : -> Set . eq (MAP, MAP) = MAP . ----eq (MAPS, none) = MAPS . *** Given a set of maps, the function \texttt{sortMaps} returns the *** subset of sort maps in it. var MAP : Map . var MAPS : Set . vars F F' L L' : Qid . var AtS : AttrSet . vars ET ET' : EType . var ETL : List . vars ES ES' : ESort . op sortMaps : Set -> Set . eq sortMaps(sort ES to ES') = sort ES to ES' . eq sortMaps(((sort ES to ES'), MAPS)) = ((sort ES to ES'), sortMaps(MAPS)) . eq sortMaps(MAP) = none [owise] . eq sortMaps((MAP, MAPS)) = sortMaps(MAPS) [owise] . eq sortMaps(none) = none . op eSortToSort : Set -> Set . eq eSortToSort(op F : ETL -> ET to F' [AtS]) = op F : eSortToSort(ETL) -> eSortToSort(ET) to F' [AtS] . eq eSortToSort(((op F : ETL -> ET to F' [AtS]), MAPS)) = (op F : eSortToSort(ETL) -> eSortToSort(ET) to F' [AtS], eSortToSort(MAPS)) . eq eSortToSort(sort ES to ES') = sort eSortToSort(ES) to eSortToSort(ES') . eq eSortToSort(((sort ES to ES'), MAPS)) = ((sort eSortToSort(ES) to eSortToSort(ES')), eSortToSort(MAPS)) . eq eSortToSort(class ES to ES') = class eSortToSort(ES) to eSortToSort(ES') . eq eSortToSort(((class ES to ES'), MAPS)) = ((class eSortToSort(ES) to eSortToSort(ES')), eSortToSort(MAPS)) . eq eSortToSort(attr F . ES to F') = (attr F . eSortToSort(ES) to F') . eq eSortToSort(((attr F . ES to F'), MAPS)) = ((attr F . eSortToSort(ES) to F'), eSortToSort(MAPS)) . eq eSortToSort(msg F : ETL -> ET to F') = msg F : eSortToSort(ETL) -> eSortToSort(ET) to F' . eq eSortToSort(((msg F : ETL -> ET to F'), MAPS)) = ((msg F : eSortToSort(ETL) -> eSortToSort(ET) to F'), eSortToSort(MAPS)) . eq eSortToSort(MAP) = MAP [owise] . eq eSortToSort((MAP, MAPS)) = (MAP, eSortToSort(MAPS)) [owise] . eq eSortToSort((none).Set) = 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 Set -> ModExp . *** Renaming _*(_) op _plus_ : ModExp ModExp -> ModExp [assoc comm] . *** Union _+_ op TUPLE`[_`] : NzNat -> ModExp . eq ME:ModExp *< none > = ME: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{Set}, for *** sets of module names. The constructors of sort \texttt{Set} are *** \texttt{noneModNameSet} and \verb~_._~. The function \verb~_inSet_~ *** 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}, which is *** defined with constructors \texttt{parList} and \texttt{nilParList}. ---- fmod UP-DECLS is ---- protecting QID-LIST . ---- protecting META-MODULE . ---- sorts Token Bubble . ---- op token : Qid -> Token ---- [special( ---- id-hook Bubble (1 1) ---- op-hook qidSymbol ( : -> Qid))] . ---- op bubble : QidList -> Bubble ---- [special( ---- id-hook Bubble (1 -1 `( `)) ---- op-hook qidListSymbol (__ : QidList QidList ->QidList) ---- op-hook qidSymbol ( : -> Qid))] . ---- op up : Token Bubble -> Term . ---- op up : Token -> Module . ---- op `[_`] : Token -> Module . ---- endfm ------------------------------------------------------------------------------- ******************************************************************************* ------------------------------------------------------------------------------- fmod MOD-NAME is pr MOD-EXPR . pr EXT-BOOL . pr EXT-SORT . inc META-LEVEL . sorts Parameter Interface List . subsort Parameter < List . op par_::_ : Qid ModExp -> Parameter . *** _::_ op par_::_ : Qid Interface -> Parameter . *** _::_ op par : ModExp List -> Interface . *** _(_) op parameterError : QidList -> [Parameter] . op nilParList : -> List . op parList : List List -> List [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 Set . subsorts Parameter ModExp < ModName < Set . op noneModNameSet : -> Set . op _._ : Set Set -> Set [assoc comm id: noneModNameSet] . op nullModName : -> ModName . eq MN . MN = MN . vars MN MN' : ModName . var MNS : Set . op _inSet_ : ModName Set -> Bool . eq MN inSet (MN . MNS) = true . eq MN inSet MNS = false [owise] . *** 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 . var VE : ViewExp . op labelInParList : ViewExp List -> 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 . (if MN == 'META-LEVEL then including 'UP-DECLS . else nil fi) sorts none . none none none none endfm) . 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, ', nil, 'Qid)))] . op 'bubble : 'QidList -> 'Bubble [special( (id-hook('Bubble, '1 '-1 '`( '`)) op-hook('qidListSymbol, '__, 'QidList 'QidList, 'QidList) op-hook('qidSymbol, ', nil, 'Qid)))] . op 'up : 'Token 'Bubble -> 'Term [none] . op 'up : 'Token -> 'Module [none] . op '`[_`] : '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 -> Qid . op parListToQidList : List -> QidList . vars QI X : Qid . vars ME ME' : ModExp . var MN : ModName . var PL : List . 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) = ' . eq parListToQidList(parList((par X :: ME), PL)) = (modNameToQidList(par X :: ME) '| parListToQidList(PL)) [owise] . eq parListToQidList(parList((par X :: If), PL)) = (modNameToQidList(par X :: If) '| parListToQidList(PL)) [owise] . 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) = ' . eq parListToQid(parList((par X :: ME), PL)) = qidListToQid(modNameToQid(par X :: ME) '| parListToQid(PL)) [owise] . eq parListToQid(parList((par X :: If), PL)) = qidListToQid(modNameToQid(par X :: If) '| parListToQid(PL)) [owise] . 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}, 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 . subsort Import < EImport . subsorts ImportList EImport < List . op protecting_. : ModName -> EImport [ctor ditto] . op extending_. : ModName -> EImport [ctor ditto] . op including_. : ModName -> EImport [ctor ditto] . op __ : List List -> List [ctor ditto] . op modName : EImport -> ModName . eq modName(protecting MN .) = MN . eq modName(extending MN .) = MN . eq modName(including MN .) = MN . op importError : QidList -> [List] [ctor format (r o)] . eq importError(QIL) importError(QIL') = importError(QIL QIL') . *** eq (including MN:ModName .) EIL:List (including MN:ModName .) *** = (including MN:ModName .) EIL:List . *** eq (including MN:ModName .) EIL:List (protecting MN:ModName .) *** = (including MN:ModName .) EIL:List . *** eq (protecting MN:ModName .) EIL:List (including MN:ModName .) *** = (including MN:ModName .) EIL:List . *** 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 unitError : QidList -> [Unit] [ctor format (r o)] . op fmod_is__sorts_.____endfm : ModName List List Set Set Set Set Set -> 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 List Set Set Set Set Set -> 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 List Set Set Set Set Set Set -> 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 List Set Set Set Set Set Set -> 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 List Set Set ClassDeclSet SubclassDeclSet Set Set Set Set Set -> 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 List Set Set ClassDeclSet SubclassDeclSet Set Set Set Set Set -> 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 -> Bool . *** \item Selector functions for the different components of a unit. op getName : Unit -> ModName . op getImports : Unit -> List . op getParList : Unit -> List . op getSorts : Unit -> Set . op getSubsorts : Unit -> Set . op getOps : Unit -> Set . op getMbs : Unit -> Set . op getEqs : Unit -> Set . op getRls : Unit -> Set . op getClasses : Unit -> ClassDeclSet . op getSubclassDecls : Unit -> SubclassDeclSet . op getMsgs : Unit -> Set . *** \item Functions to change the value of each of the components of a unit. op setName : Unit ModName -> Unit . op setPars : Unit List -> Unit . op setImports : Unit List -> Unit . op setSorts : Unit Set -> Unit . op setSubsorts : Unit Set -> Unit . op setOps : Unit Set -> Unit . op setMbs : Unit Set -> Unit . op setEqs : Unit Set -> Unit . op setRls : Unit Set -> Unit . op setClasses : Unit ClassDeclSet -> Unit . op setSubclasses : Unit SubclassDeclSet -> Unit . op setMsgs : Unit Set -> Unit . *** \item Functions to add new declarations to the set of declarations *** already in a unit. op addImports : List Unit -> Unit . op addSorts : Set Unit -> Unit . op addSubsorts : [Set] Unit -> Unit . op addOps : [Set] Unit -> Unit . op addMbs : Set Unit -> Unit . op addEqs : Set Unit -> Unit . op addRls : Set Unit -> Unit . op addClasses : ClassDeclSet Unit -> Unit . op addSubclasses : SubclassDeclSet Unit -> Unit . op addMsgs : Set 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' : Set . vars OPDS OPDS' : OpDeclSet . vars EOPD EOPD' : EOpDecl . vars EOPDS EOPDS' : Set . var EOPDS? : [Set] . var At : Attr . vars EMAS EMAS' : Set . vars MAS MAS' : MembAxSet . vars EqS EqS' : Set . vars RlS RlS' : Set . vars ESS ESS' : Set . vars SS SS' : SortSet . vars IL IL' : ImportList . vars MN MN' : ModName . vars QIL QIL' : QidList . vars PL PL' : List . vars CDS CDS' : ClassDeclSet . vars SCD SCD' : SubclassDecl . vars SCDS SCDS' : SubclassDeclSet . vars U U' : Unit . vars MDS MDS' : Set . vars EI EI' : EImport . vars EIL EIL' : List . var T : Term . eq EI in (EIL EI EIL') = true . eq EI in EIL = false [owise] . op eLeastSort : Unit Term -> [Type] . eq eLeastSort(U, T) = leastSort(U, T) . eq eLeastSort(U, qidError(QIL)) = qidError(QIL) . *** = if (U : Module) *** and (T =/= error*) *** then leastSort(U, T) *** else errorSort(none) *** fi . *** Selection functions for units eq getName(unitError(QIL)) = 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(unitError(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(unitError(QIL)) = nilParList . eq getParList(noUnit) = 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(unitError(QIL)) = 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 . eq getAllSorts(M) = getSorts(M) . ***( 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(extending 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('SATISFACTION) = getSorts('LTL) ; 'State . eq getSorts('MODEL-CHECKER) = getSorts('QID) ; getSorts('SATISFACTION) ; 'RuleName ; 'Transition ; 'TransitionList ; 'ModelCheckResult . ) eq getSubsorts(unitError(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(unitError(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(unitError(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(unitError(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(unitError(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(unitError(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(unitError(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(unitError(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(unitError(QIL), EIL) = unitError(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(unitError(QIL), EOPDS) = unitError(QIL) . eq setOps(U, opDeclError(QIL) EOPDS) = unitError(QIL) . eq setOps(unitError(QIL), opDeclError(QIL') EOPDS) = unitError(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(unitError(QIL), ESSDS) = unitError(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(unitError(QIL), EMAS) = unitError(QIL) . eq setMbs(U, membAxError(QIL) EMAS) = unitError(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(unitError(QIL), EqS) = unitError(QIL) . eq setEqs(U, equationError(QIL) EqS?:[EquationSet]) = unitError(QIL) . eq setEqs(unitError(QIL), equationError(QIL') EqS?:[EquationSet]) = unitError(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(unitError(QIL), RlS?) = unitError(QIL) . eq setRls(U?, ruleError(QIL) RlS?) = unitError(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 fth MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS endfth else th MN is PL EIL sorts ESS . ESSDS EOPDS EMAS EqS RlS endth 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(unitError(QIL), ESS) = unitError(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(noUnit, MN) = noUnit . eq setName(unitError(QIL), MN) = unitError(QIL) . *** Add functions eq addSorts(ESS, U) = setSorts(U, (ESS ; getSorts(U))) . eq addSubsorts(ESSDS, U) = setSubsorts(U, (ESSDS getSubsorts(U))) . eq addSubsorts(subsortDeclError(QIL), U) = unitError(QIL) . eq addOps(EOPDS, U) = setOps(U, (EOPDS getOps(U))) . eq addOps(EOPDS?, unitError(QIL)) = unitError(QIL) . eq addOps(EOPDS?, U) = U [owise] . 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(noUnit, U) = U . eq addDecls(U, noUnit) = U . eq addDecls(unitError(QIL), U) = unitError(QIL) . eq addDecls(U, unitError(QIL)) = unitError(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 . subsorts Map TermMap < ViewMap . subsorts ViewMap Set < Set . op _`,_ : Set Set -> Set [ditto] . eq (VMAP, none) = VMAP . var MAP : Map . var VMAP : ViewMap . var VMAPS : Set . vars T T' : Term . vars ES ES' : ESort . *** As for sets of maps, \texttt{SortSet} returns the subset of sort *** maps in a set of view maps. op sortMaps : Set -> Set . eq sortMaps((sort ES to ES')) = (sort ES to ES') . eq sortMaps(((sort ES to ES'), VMAPS)) = ((sort ES to ES'), sortMaps(VMAPS)) . eq sortMaps(VMAP) = none [owise] . eq sortMaps((VMAP, VMAPS)) = sortMaps(VMAPS) [owise] . eq sortMaps(none) = none . op eSortToSort : Set -> Set . eq eSortToSort(termMap(T, T')) = termMap(T, T') . eq eSortToSort((termMap(T, T'), VMAPS)) = (termMap(T, T'), eSortToSort(VMAPS)) . eq eSortToSort(MAP) = eSortToSort(MAP) [owise] . eq eSortToSort((MAP, VMAPS)) = (eSortToSort(MAP), eSortToSort(VMAPS)) [owise] . 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 ModExp ModExp Set -> View [ctor format (nir! o)] . op noView : -> View [ctor] . op viewError : QidList -> [View] [ctor format (r o)] . var QI : Qid . vars VE VE' : ViewExp . vars PL PL' : List . vars ME ME' ME'' : ModExp . vars VMAPS VMAPS' : Set . var QIL : QidList . op name : View -> ViewExp . op getParList : [View] -> List . op source : View -> ModExp . op target : View -> ModExp . op mapSet : View -> Set . eq name(view(VE, PL, ME, ME', VMAPS)) = VE . eq getParList(view(VE, PL, ME, ME', VMAPS)) = PL . eq getParList(viewError(QIL)) = parameterError(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 ~> View . op setTarget : View ModExp ~> View . op setSource : View ModExp ~> View . op setMaps : View Set ~> View . eq setName(view(VE, PL, ME, ME', VMAPS), VE') = view(VE', PL, ME, ME', VMAPS) . eq setName(viewError(QIL), VE) = viewError(QIL) . eq setPars(view(VE, PL, ME, ME', VMAPS), PL') = view(VE, PL', ME, ME', VMAPS) . eq setPars(viewError(QIL), PL) = viewError(QIL) . eq setSource(view(VE, PL, ME, ME', VMAPS), ME'') = view(VE, PL, ME'', ME', VMAPS) . eq setSource(viewError(QIL), ME) = viewError(QIL) . eq setTarget(view(VE, PL, ME, ME', VMAPS), ME'') = view(VE, PL, ME, ME'', VMAPS) . eq setTarget(viewError(QIL), ME) = viewError(QIL) . eq setMaps(view(VE, PL, ME, ME', VMAPS), VMAPS') = view(VE, PL, ME, ME', VMAPS') . eq setMaps(viewError(QIL), VMAPS) = viewError(QIL) . 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, ', nil, 'Qid)))] . op 'bubble : 'QidList -> 'Bubble [special( (id-hook('Bubble, '1 '-1 '`( '`)) op-hook('qidListSymbol, '__, 'QidList 'QidList, 'QidList) op-hook('qidSymbol, ', nil, 'Qid)))] . op 'up : 'Token 'Bubble -> 'Term [none] . op 'up : 'Token -> 'Module [none] . op '`[_`] : '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{PreSet}. 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 PreSet . subsorts Map TermPreMap < PreViewMap . subsorts PreViewMap Set < PreSet . op _`,_ : PreSet PreSet -> PreSet [ditto] . eq (PVMAPS, none) = PVMAPS . var PVMAP : PreViewMap . var PVMAPS : PreSet . vars ES ES' : ESort . *** Given a set of maps, the function \texttt{sortMaps} returns the subset *** of sort maps in it. op sortMaps : PreSet -> Set . eq sortMaps(((sort ES to ES'), PVMAPS)) = ((sort ES to ES'), sortMaps(PVMAPS)) . eq sortMaps((PVMAP, PVMAPS)) = sortMaps(PVMAPS) [owise] . eq sortMaps(none) = none . endfm ------------------------------------------------------------------------------- ******************************************************************************* ------------------------------------------------------------------------------- fmod PRE-VIEW is pr UNIT . pr PRE-VIEW-MAP . sort PreView . op view : ViewExp List ModExp ModExp Set PreSet -> PreView . op noView : -> PreView . op name : PreView -> ViewExp . op getParList : PreView -> List . op source : PreView -> ModExp . op target : PreView -> ModExp . op vars : PreView -> Set . op mapSet : PreView -> PreSet . var QI : Qid . vars ME ME' : ModExp . var VE : ViewExp . vars PL PL' : List . vars VDS VDS' : Set . vars PVMAPS PVMAPS' : PreSet . 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 addMaps : PreSet PreView -> PreView . op addVars : OpDeclSet PreView -> PreView . eq addMaps(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 -> 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