---- restore conditions for evalModule ---- restore conditions for evalPreModule ---- restore conditions for procModule3 ---- Full Maude specification version 2.1.2l ---- To be run on Maude Alpha86e fmod BANNER is pr STRING . op banner : -> String . eq banner = "Full Maude 2.2 (December 1st, 2005)" . endfm ---- last modification: December 1st, 2005 ---- 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 inclof the License, or (at your option) any later veq resersion. This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNSS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public Leicense along with this program; if not, write to the Free Software Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307, USA. ) ---- to do: ---- - continue . ---- - show search path . ---- - show path labels . ---- - show components . ---- - (alpha85a) Operator declarations may now take the metadata attribute ---- that was previously reserved for mbs/eqs/rls. ---- Last changes: ---- ---- - All sorts declared in modules used for parsing have been renamed. ---- Any sort S in one of these modules is nos called @S@. ---- Since some of these modules where added to the user defined modules ---- for dealing with ups, conditions, etc., he was getting error when ---- using sorts like Token or OpDecl in his specs. ---- ---- - Syntax for parameterization has been changed (again) !!! : ---- - module definition: FOO{X :: TRIV, Y :: TRIV} ---- - module instantiation: FOO{Bar,Baz} ---- - parameterized sorts: Foo{Bar,Baz} ---- ---- - Any module loaded in Core Maude can be used in Full Maude. ---- This may be particularly useful in the case of using the model checker. ---- ---- (mod CHECK-RESP is ---- protecting MODEL-CHECKER . ---- ... ---- endm) ---- ---- (red p(0) |= (<> Qstate) .) ---- ---- - Module renaming and summation consistent with Core Maude's. Built-ins ---- are now handled at the metalevel, instead of leaving the inclusions to ---- Core Maude. In this way, they can be renamed and redefined, as in ---- Core Maude. This makes Full Maude slower. ---- ---- - 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). ---- ---- - Tuples are built with the syntax ---- TUPLE[size]{comma_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. ---- ---- - 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 ---- ---- - Check: perhaps we need to convert constants 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`) . ---- ----load model-checker.maude ------------------------------------------------------------------------------- ******************************************************************************* *** *** 2 The Signature of Full Maude *** ******************************************************************************* ------------------------------------------------------------------------------- fmod EXTENDED-SORTS is ---- Any modification in this module must be reflected in the metamodule ---- used in eq addInfoConds in module UNIT-BUBBLE-PARSING 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@ [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 frozen ditto iter : -> @Attr@ . ops object msg message 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_ : @Sort@ @Token@ @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 _`{_`} : @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_. : @Sort@ @Token@ @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@ . *** parse commands op parse_. : @Bubble@ -> @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`vars`. : -> @Command@ . op show`vars_. : @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`eqs`. : -> @Command@ . op show`eqs_. : @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_on`. : @ModExp@ -> @Command@ . op set`protect_off`. : @ModExp@ -> @Command@ . op set`include_on`. : @ModExp@ -> @Command@ . op set`include_off`. : @ModExp@ -> @Command@ . op set`extend_on`. : @ModExp@ -> @Command@ . op set`extend_off`. : @ModExp@ -> @Command@ . *** miscellaneous op load_. : @ModExp@ -> @Command@ . endfm ------------------------------------------------------------------------------- ******************************************************************************* ------------------------------------------------------------------------------- fmod FULL-MAUDE-SIGN is including VIEWS . including COMMANDS . sort @Input@ . subsorts @Command@ @Module@ @View@ < @Input@ . endfm ------------------------------------------------------------------------------- ******************************************************************************* ------------------------------------------------------------------------------- *** 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. 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. *** 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}. Then, in the following module *** \texttt{META-FULL-MAUDE-SIGN} we declare a constant \texttt{GRAMMAR} of *** sort \texttt{FModule}, and 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 [memo] . 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. ******* ******* ERROR HANDLING, by Peter Olveczky ******* *** The following module defines a function 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{Module} *** ------------------------------------------------------------------------------- ******************************************************************************* ------------------------------------------------------------------------------- *** In this section we present the abstract data type \texttt{Module}, 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{Module} 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{} 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 qidList2Qid : QidList -> Qid . var QI : Qid . var QIL : QidList . var St : String . var N : Nat . var F : FindResult . eq qidList2Qid(('\s QIL)) = qid(" " + string(qidList2Qid(QIL))) . eq qidList2Qid((QI QIL)) = qid(string(QI) + " " + string(qidList2Qid(QIL))) [owise] . eq qidList2Qid(nil) = qid("") . op string2qidList : String -> QidList . eq string2qidList("") = nil . ceq string2qidList(St) = if F == notFound then qid(substr(St, findNonSpace(St), length(St))) else qid(substr(St, findNonSpace(St), F + 1)) string2qidList(substr(St, F + 1, length(St))) fi if F := find(substr(St, findNonSpace(St), length(St)), " ", 0) [owise] . op findNonSpace : String -> Nat . op findNonSpace : String Nat -> Nat . ---- returns the length of the string if not found eq findNonSpace(St) = findNonSpace(St, 0) . eq findNonSpace(St, N) = if substr(St, N, 1) =/= "" and substr(St, N, 1) == " " then findNonSpace(St, N + 1) else N fi . 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 Sort 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. ------------------------------------------------------------------------------- ******************************************************************************* ------------------------------------------------------------------------------- fmod VIEW-EXPR is pr META-MODULE . sort ViewExp . subsorts Sort < ViewExp < ModuleExpression NeParameterList . op mtViewExp : -> ViewExp . op _{_} : Sort ParameterList -> ViewExp [ctor prec 37]. op _;;_ : ViewExp ViewExp -> ViewExp [assoc id: mtViewExp] . *** view composition _;_ 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{parameter2Qid}, or, similarly, elements of sorts \texttt{Sort}, *** \texttt{SortList}, and \texttt{SortSet} 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 viewExp2Qid : ViewExp -> Qid . op parameterList2Qid : ParameterList -> Qid . op viewExp2QidList : ViewExp -> QidList . op parameterList2QidList : ParameterList -> QidList . var V : Sort . var QI : Qid . var QIL : QidList . var P : ViewExp . var PL : NeParameterList . vars VE VE' : ViewExp . eq parameterList2QidList(P) = viewExp2QidList(P) . ceq parameterList2QidList((P, PL)) = (if QI == '`) then QIL QI '\s else QIL QI fi) '`, parameterList2QidList(PL) if QIL QI := viewExp2QidList(P). eq viewExp2QidList(V{PL}) = (viewExp2QidList(V) '`{ parameterList2QidList(PL) '`}) . ceq viewExp2QidList(VE ;; VE') = (viewExp2QidList(VE) '; viewExp2QidList(VE')) if VE =/= mtViewExp /\ VE' =/= mtViewExp . eq viewExp2QidList(V) = V . eq parameterList2Qid(P) = viewExp2Qid(P) . eq parameterList2Qid((P, PL)) = qid(string(viewExp2Qid(P)) + ", " + string(parameterList2Qid(PL))) . eq viewExp2Qid(VE) = qidList2Qid(viewExp2QidList(VE)) . endfm ------------------------------------------------------------------------------- ******************************************************************************* ------------------------------------------------------------------------------- *** *** Parameterized Sorts *** *** In addition to the \texttt{Sort} sort, in the following module *** \texttt{EXT-SORT} we also define sorts \texttt{SortList} and *** \texttt{SortSet}. *** The operator \texttt{eSort} is declared to be a constructor for extended *** sorts. *** As for lists and sTS of quoted identifiers, we declare \verb~__~ and *** \verb~_;_~ as constructors for sorts \texttt{SortList} and *** \texttt{SortList}, and \texttt{SortSet}, respectively. ------------------------------------------------------------------------------- ******************************************************************************* ------------------------------------------------------------------------------- fmod EXT-SORT is pr META-LEVEL . pr EXT-BOOL . pr VIEW-EXPR . op size : TypeList -> Nat . eq size((nil).TypeList) = 0 . eq size(T:Type TL:TypeList) = 1 + size(TL:TypeList) . *** We define operations extending the built-in functions \texttt{sameKind} *** and \texttt{leastSort}, respectively, to lists of sorts and *** to lists of extended terms. The function \texttt{sameKind} 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{Sort} 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. op sameKind : Module TypeList TypeList -> Bool [ditto] . ceq sameKind(M:Module, (T:Type TL:TypeList), (T':Type TL':TypeList)) = sameKind(M:Module, T:Type, T':Type) and-then sameKind(M:Module, TL:TypeList, TL':TypeList) if TL:TypeList =/= nil or TL':TypeList =/= nil . eq sameKind(M:Module, (T:Type TL:TypeList), nil) = false . eq sameKind(M:Module, nil, (T:Type TL:TypeList)) = false . eq sameKind(M:Module, nil, nil) = true . eq sameKind(M:Module, cc(S:Sort ; SS:SortSet), S':Sort) = sameKind(M:Module, S:Sort, S':Sort) . eq sameKind(M:Module, S:Sort, cc(S':Sort ; SS:SortSet)) = sameKind(M:Module, S:Sort, S':Sort) . eq sameKind(M:Module, cc(S:Sort ; SS:SortSet), cc(S':Sort ; SS':SortSet)) = sameKind(M:Module, S:Sort, S':Sort) . op leastSort : Module TermList ~> TypeList [ditto] . op qidError : QidList -> [Sort] . op stringError : QidList -> [String] . eq string(qidError(QIL)) = stringError(QIL) . eq qid(stringError(QIL)) = qidError(QIL) . eq stringError(QIL) + St:String = stringError(QIL) . op getMsg : [Sort] -> QidList . eq getMsg(qidError(QIL:QidList)) = QIL:QidList . eq leastSort(M:Module, (T:Term, TL:TermList)) = (leastSort(M:Module, T:Term) leastSort(M:Module, TL:TermList)) . eq leastSort(M:Module, T:Term) = qidError('Error: 'non-valid 'module) . op _inSortSet_ : Sort SortSet -> Bool . eq S:Sort inSortSet (S:Sort ; SS:SortSet) = true . eq S:Sort inSortSet (S':Sort ; SS:SortSet) = (S:Sort == S':Sort) or-else (S:Sort inSortSet SS:SortSet) . eq S:Sort inSortSet none = false . op kind : TypeList -> Type . eq kind(S:Sort TL:TypeList) = qid("[" + string(S:Sort) + "]") kind(TL:TypeList) . eq kind(K:Kind TL:TypeList) = K:Kind kind(TL:TypeList) . eq kind(nil) = nil . op kind : SortSet -> Type . eq kind(S:Sort ; SS:SortSet) = qid("[" + string(S:Sort) + "]") . op cc : SortSet -> Type . op getSort : Kind -> Sort . eq getSort(K:Kind) = if find(string(K:Kind), "`,", 0) == notFound then qid(substr(string(K:Kind), 2, sd(length(string(K:Kind)), 4))) else qid(substr(string(K:Kind), 2, sd(find(string(K:Kind), "`,", 0), 2))) fi . op getSorts : Kind -> SortSet . eq getSorts(K:Kind) = if find(string(K:Kind), "`,", 0) == notFound then qid(substr(string(K:Kind), 2, sd(length(string(K:Kind)), 4))) else qid(substr(string(K:Kind), 2, sd(find(string(K:Kind), "`,", 0), 2))) ; getSorts(qid("[" + substr(string(K:Kind), sd(find(string(K:Kind), "`,", 0), 1), length(string(K:Kind))))) fi . ---- name of a sort (the name of S{P1, ..., Pn} is S) op getName : Sort -> Qid . eq getName(S:Sort) = if findOpening(string(S:Sort), "{", "}", sd(length(string(S:Sort)), 2)) == notFound then S:Sort else qid(substr(string(S:Sort), 0, findOpening(string(S:Sort), "{", "}", sd(length(string(S:Sort)), 2)))) fi . ---- parameters of a sort (the parameters of S{P1, ..., Pn} are P1 ... Pn) op getPars : Sort -> ParameterList . op getParsAux : String Nat Nat -> ParameterList . eq getPars(S:Sort) = if findOpening(string(S:Sort), "{", "}", sd(length(string(S:Sort)), 2)) == notFound then empty else getParsAux(string(S:Sort), findOpening(string(S:Sort), "{", "}", sd(length(string(S:Sort)), 2)) + 1, length(string(S:Sort))) fi . var St Pattern OpenPar ClosingPar : String . vars L R N OpenPars ClosingPars : Nat . eq getParsAux(St, L, R) = if findOut(St, ",", "{", "}", L) == notFound then qid(substr(St, L, sd(findClosing(St, "{", "}", L), L))) else (qid(substr(St, L, sd(findOut(St, ",", "{", "}", L), L))), getParsAux(St, findOut(St, ",", "{", "}", L) + 1, R)) fi . ---- finds a pattern out of balanced parentheses ---- findOut("S{P1, P2{P21, P22}, P3}", ",", "{", "}", 6) returns 18, not 12 op findOut : String String String String Nat -> FindResult . op findOut : String String String String Nat Nat -> FindResult . eq findOut(St, Pattern, OpenPar, ClosingPar, N) = findOut(St, Pattern, OpenPar, ClosingPar, 0, N) . eq findOut(St, Pattern, OpenPar, ClosingPar, OpenPars, N) = if N >= length(St) then notFound else if OpenPars == 0 and-then substr(St, N, length(Pattern)) == Pattern then N else if substr(St, N, length(OpenPar)) == OpenPar then findOut(St, Pattern, OpenPar, ClosingPar, OpenPars + 1, N + 1) else if substr(St, N, length(ClosingPar)) == ClosingPar then findOut(St, Pattern, OpenPar, ClosingPar, sd(OpenPars, 1), N + 1) else findOut(St, Pattern, OpenPar, ClosingPar, OpenPars, N + 1) fi fi fi fi . ---- finds the first closing unbalanced parenthesis ---- findOut("P1, P2{P21, P22}, P3}", "{", "}", 6) returns 21, not 16 op findClosing : String String String Nat -> FindResult . op findClosing : String String String Nat Nat -> FindResult . eq findClosing(St, OpenPar, ClosingPar, N) = findClosing(St, OpenPar, ClosingPar, 0, N) . eq findClosing(St, OpenPar, ClosingPar, OpenPars, N) = if N >= length(St) then notFound else if OpenPars == 0 and-then substr(St, N, length(ClosingPar)) == ClosingPar then N else if substr(St, N, length(OpenPar)) == OpenPar then findClosing(St, OpenPar, ClosingPar, OpenPars + 1, N + 1) else if substr(St, N, length(ClosingPar)) == ClosingPar then findClosing(St, OpenPar, ClosingPar, sd(OpenPars, 1), N + 1) else findClosing(St, OpenPar, ClosingPar, OpenPars, N + 1) fi fi fi fi . ---- finds the last opening unbalanced parenthesis ---- findOpening("S{P1, P2{P21, P22}, P3}", "{", "}", 21) returns 1, not 8 op findOpening : String String String Nat -> FindResult . op findOpening : String String String Nat Nat -> FindResult . eq findOpening(St, OpenPar, ClosingPar, N) = findOpening(St, OpenPar, ClosingPar, 0, N) . eq findOpening(St, OpenPar, ClosingPar, ClosingPars, N) = if N == 0 then notFound else if ClosingPars == 0 and-then substr(St, N, length(ClosingPar)) == OpenPar then N else if substr(St, N, length(OpenPar)) == ClosingPar then findOpening(St, OpenPar, ClosingPar, ClosingPars + 1, sd(N, 1)) else if substr(St, N, length(ClosingPar)) == OpenPar then findOpening(St, OpenPar, ClosingPar, sd(ClosingPars, 1), sd(N, 1)) else findOpening(St, OpenPar, ClosingPar, ClosingPars, sd(N, 1)) fi fi fi fi . ***( eq getParsAux(St, L, R) = if find(St, ",", L) == notFound then qid(substr(St, L, sd(find(St, "}", L), L))) else qid(substr(St, L, sd(find(St, ",", L), L))) getParsAux(St, find(St, ",", L) + 1, R) fi . ) op makeSort : Sort ParameterList -> Sort . op makeSort : Sort ParameterList ParameterList ParameterList -> Sort . op makeSort2 : Sort ParameterList -> Sort . op makePars : ParameterList -> String . vars S P : Sort . vars PL PL' PL'' PL3 : ParameterList . var VE : ViewExp . var QIL : QidList . eq makeSort(S, PL) = if PL == empty then S else makeSort(S, PL, empty, empty) fi . ----eq makeSort(S, P, PL, PL') = makeSort(S, empty, (PL, P), PL') . eq makeSort(S, (P, PL), PL', PL'') = makeSort(S, PL, (PL', P), PL'') . eq makeSort(S, (P{PL}, PL'), PL'', PL3) = makeSort(S, PL', (PL'', makeSort(P, PL)), PL3) . ----eq makeSort(S, (P ;; VE), PL, PL') ---- = makeSort(S, empty, (PL, P), (PL', VE)) ---- [owise] . eq makeSort(S, ((P ;; VE), PL), PL', PL'') = makeSort(S, PL, (PL', P), (PL'', VE)) [owise] . eq makeSort(S, empty, PL, PL') = if PL' == empty then makeSort2(S, PL) else makeSort(makeSort2(S, PL), PL') fi . eq makeSort2(S, empty) = S:Sort . eq makeSort2(S, P) = qid(string(S) + "{" + string(P) + "}") . eq makeSort2(S, (P, PL)) = qid(string(S) + "{" + string(P) + makePars(PL)) [owise] . eq makePars((P, PL)) = "," + string(P) + makePars(PL) . eq makePars(P) = "," + string(P) + "}" . eq makePars(empty) = "}" . endfm ------------------------------------------------------------------------------- ******************************************************************************* ------------------------------------------------------------------------------- fmod DEFAULT-VALUE{X :: TRIV} is sort Default{X} . subsort X$Elt < Default{X} . op null : -> Default{X} . endfm view Term from TRIV to META-TERM is sort Elt to Term . endv ------------------------------------------------------------------------------- ******************************************************************************* ------------------------------------------------------------------------------- *** *** 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 Modules *** *** 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 : S~} and \mbox{\verb~T :: S~}.} *** \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 sTS of such declarations. ------------------------------------------------------------------------------- ******************************************************************************* ------------------------------------------------------------------------------- fmod INT-LIST is pr META-MODULE . pr INT . sort IntList . subsort Int NatList < IntList . op __ : IntList IntList -> IntList [ctor ditto] . op numberError : QidList -> [Nat] . vars N M : Nat . op from_to_list : Nat Nat ~> NatList . ceq from N to M list = if N == M then N else N from N + 1 to M list fi if N <= M . endfm ------------------------------------------------------------------------------- ******************************************************************************* ------------------------------------------------------------------------------- fmod EXT-DECL is pr EXT-SORT . pr INT-LIST . vars QIL QIL' : QidList . var At : Attr . var AtS : AttrSet . var OPD OPD' : OpDecl . var OPDS : OpDeclSet . *** subsort declarations error op subsortDeclError : QidList -> [SubsortDeclSet] [ctor format (r o)] . 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 op opDeclError : QidList -> [OpDeclSet] [ctor format (r o)] . eq opDeclError(QIL) opDeclError(QIL') = opDeclError(QIL QIL') . *** extended membership axioms op membAxError : QidList -> [MembAxSet] [ctor format (r o)] . eq membAxError(QIL) membAxError(QIL') = membAxError(QIL QIL') . *** extended equations op equationError : QidList -> [EquationSet] [ctor format (r o)] . eq equationError(QIL) equationError(QIL') = equationError(QIL QIL') . *** extended rules op ruleError : QidList -> [RuleSet] [ctor format (r o)] . 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_ : OpDecl OpDeclSet -> Bool . eq OPD in (OPD OPDS) = true . eq OPD in (OPD' OPDS) = (OPD == OPD') or-else (OPD in OPDS) . eq OPD in none = false . endfm ------------------------------------------------------------------------------- ******************************************************************************* ------------------------------------------------------------------------------- *** *** Declarations for Object-Oriented Modules *** *** 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{Sort} for class identifiers, and *** \texttt{TypeList} and \texttt{SortSet} for lists and sTS 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 Sort -> 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_|_. : Sort 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_<_. : Sort Sort -> 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 MsgDeclSet . subsort MsgDecl < MsgDeclSet . op msg_:_->_. : Qid TypeList Sort -> MsgDecl . op none : -> MsgDeclSet . op __ : MsgDeclSet MsgDeclSet -> MsgDeclSet [assoc comm id: none] . eq MD:MsgDecl MD:MsgDecl = MD:MsgDecl . op msgDeclError : QidList -> [MsgDeclSet] [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 -> SortSet . eq classSet((class S:Sort | ADS:AttrDeclSet .) CDS:ClassDeclSet) = (S:Sort ; classSet(CDS:ClassDeclSet)) . eq classSet(none) = none . endfm ------------------------------------------------------------------------------- ******************************************************************************* ------------------------------------------------------------------------------- *** *** Renaming Maps *** *** We introduce the different types of renaming maps in the module *** \texttt{FMAP} 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 sTS of *** maps (\texttt{RenamingSet}) is then declared as supersort of \texttt{Map} *** with constructors \texttt{none} and \verb~_,_~. ------------------------------------------------------------------------------- ******************************************************************************* ------------------------------------------------------------------------------- fmod FMAP is inc META-MODULE . pr EXT-SORT . *** renamings op class_to_ : Sort Sort -> Renaming . op attr_._to_ : Qid Sort Qid -> Renaming . op msg_to_ : Qid Qid -> Renaming . op msg_:_->_to_ : Qid TypeList Sort Qid -> Renaming . op none : -> RenamingSet . eq (MAP, MAP) = MAP . eq (MAPS, none) = MAPS . ---- eq attr A . qidError(QIL) to A' = none . *** Given a set of maps, the function \texttt{sortMaps} returns the *** subset of sort maps in it. var MAP : Renaming . var MAPS : RenamingSet . vars S S' A A' : Sort . var QIL : QidList . op sortMaps : RenamingSet -> RenamingSet . eq sortMaps(sort S to S') = sort S to S' . eq sortMaps(((sort S to S'), MAPS)) = ((sort S to S'), sortMaps(MAPS)) . eq sortMaps(MAP) = none [owise] . eq sortMaps((MAP, MAPS)) = sortMaps(MAPS) [owise] . eq sortMaps(none) = none . endfm ------------------------------------------------------------------------------- ******************************************************************************* ------------------------------------------------------------------------------- *** *** Module Expressions and Module Names *** *** The abstract syntax for writing specifications in Maude can be seen as *** given by module expressions, where the notion of module expression is *** understood as an expression that defines a new module out of previously *** defined modules by combining and/or modifying them according to a specific *** set of operations. All module expressions will be evaluated generating *** modules with such module expressions as names. In the case of parameterized *** modules, each of the parameters in an interface will be used as the name *** of a new module created as a renamed copy of the parameter theory. *** *** Module Expressions *** *** The \texttt{TUPLE} is declared to be a new type of *** \texttt{ModuleExpression}. ------------------------------------------------------------------------------- ******************************************************************************* ------------------------------------------------------------------------------- fmod MOD-EXPR is inc META-MODULE . pr FMAP . op TUPLE`[_`] : NzNat -> ModuleExpression . eq ME:ModuleExpression * ( none ) = ME:ModuleExpression . 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{ViewExp} is *** declared as a subsort of \texttt{Header}, that is, terms of sort *** \texttt{ViewExp} are considered to be module names. The constructor *** operator for the sort \texttt{ViewExp} is \verb~par_::_~. ------------------------------------------------------------------------------- ******************************************************************************* ------------------------------------------------------------------------------- fmod MOD-NAME is inc MOD-EXPR . pr EXT-BOOL . op parameterError : QidList -> [ParameterDecl] . sort ModuleName . subsorts ModuleExpression < ModuleName < Header . op _{_} : ModuleExpression ParameterDeclList -> Header . op pd : ParameterDecl -> ModuleName . op nullHeader : -> Header . op getName : Header -> ModuleExpression . op getParDecls : Header -> ParameterDeclList . vars QI QI' : Qid . var ME : ModuleExpression . vars PDL PDL' : ParameterDeclList . var PL : NeParameterList . var MN : ModuleName . eq getName(ME{PDL}) = ME . eq getName(MN) = MN . eq getParDecls(ME{PDL}) = PDL . eq getParDecls(MN) = nil . op including_. : ModuleName -> Import [ctor] . op extending_. : ModuleName -> Import [ctor] . op protecting_. : ModuleName -> Import [ctor] . op fth_is_sorts_.____endfth : Header ImportList SortSet SubsortDeclSet OpDeclSet MembAxSet EquationSet -> FTheory [ctor gather (& & & & & & &) format (d d d n++i ni d d ni ni ni ni n--i d)] . op th_is_sorts_._____endth : Header ImportList SortSet SubsortDeclSet OpDeclSet MembAxSet EquationSet RuleSet -> STheory [ctor gather (& & & & & & & &) format (d d d n++i ni d d ni ni ni ni ni n--i d)] . *** The function \texttt{labelInParameterDeclList} checks whether the quoted *** identifier given as first argument is used as a label in the list of *** parameters given as second argument. op labelInParameterDeclList : Sort ParameterDeclList -> Bool . eq labelInParameterDeclList(QI, (PDL, (QI :: ME), PDL')) = true . eq labelInParameterDeclList(QI, PDL) = false [owise] . 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{header2Qid} and \texttt{header2QidList} in the module *** \texttt{MOD-NAME-TO-QID} below accomplish this transformation. In any *** language extensions, new equations for the function *** \texttt{header2QidList} 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 header2Qid : -> Qid . op header2QidList : Header -> QidList . op parameterDecl2Qid : ParameterDecl -> Qid . op parameterDecl2QidList : ParameterDecl -> QidList . op parameterDeclList2Qid : ParameterDeclList -> Qid . op parameterDeclList2QidList : ParameterDeclList -> QidList . vars QI X : Qid . var QIL : QidList . vars ME ME' : ModuleExpression . var PDL : ParameterDeclList . var PD : ParameterDecl . eq header2Qid(QI) = QI . eq header2Qid(nullHeader) = ' . eq header2Qid(pd(X :: ME)) = qidList2Qid(header2QidList(pd(X :: ME))) . eq header2QidList(pd(X :: ME)) = X ':: header2QidList(ME) . eq header2QidList(QI) = QI . eq header2QidList(nullHeader) = ' . eq header2Qid((ME { PDL })) = qidList2Qid(header2QidList((ME { PDL }))) . ceq header2QidList((ME { PDL })) = (if QI == '\s then QIL else QIL QI fi '`{ parameterDecl2QidList(PDL) '`} '\s) if QIL QI := header2QidList(ME) . eq parameterDecl2Qid(X :: ME) = qidList2Qid(X ':: header2Qid(ME)) . eq parameterDeclList2Qid(PDL) = qidList2Qid(parameterDeclList2QidList(PDL)) . eq parameterDeclList2QidList(X :: ME) = X ':: header2QidList(ME) . eq parameterDeclList2QidList((X :: ME, PDL)) = parameterDeclList2QidList(X :: ME) '`, parameterDeclList2QidList(PDL) [owise] . endfm ------------------------------------------------------------------------------- ******************************************************************************* ------------------------------------------------------------------------------- *** *** Modules *** *** 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{Module}. 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{Header}, *** \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 . op moduleName : Import -> ModuleName . eq moduleName(protecting MN .) = MN . eq moduleName(protecting ME{PL} .) = ME . eq moduleName(extending MN .) = MN . eq moduleName(extending ME{PL} .) = ME . eq moduleName(including MN .) = MN . eq moduleName(including ME{PL} .) = ME . op importError : QidList -> [ImportList] [ctor format (r o)] . eq importError(QIL) importError(QIL') = importError(QIL QIL') . sorts OModule OTheory . subsorts SModule < OModule < Module . subsorts STheory < OTheory < Module . op noModule : -> Module . *** Module op unitError : QidList -> [Module] [ctor format (r o)] . op omod_is_sorts_.________endom : Header ImportList SortSet SubsortDeclSet ClassDeclSet SubclassDeclSet OpDeclSet MsgDeclSet MembAxSet EquationSet RuleSet -> OModule [ctor gather (& & & & & & & & & & &) format (r! o r! n++io ni d d ni ni ni ni ni ni ni ni n--ir! o)] . op oth_is_sorts_.________endoth : Header ImportList SortSet SubsortDeclSet ClassDeclSet SubclassDeclSet OpDeclSet MsgDeclSet MembAxSet EquationSet RuleSet -> OTheory [ctor gather (& & & & & & & & & & &) format (r! o r! n++io 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_ : Import ImportList -> Bool . *** \item Selector functions for the different components of a Module. op getName : Module -> Header . op getPars : Module -> ParameterDeclList . op getClasses : Module -> ClassDeclSet . op getSubclasses : Module -> SubclassDeclSet . op getMsgs : Module -> MsgDeclSet . *** \item Functions to change the value of each of the components of a Module. op setName : Module ModuleExpression -> Module . op setName : Module ParameterDecl -> Module . op setPars : Module ParameterDeclList -> Module . op setImports : Module ImportList -> Module . op setSorts : Module SortSet -> Module . op setSubsorts : Module SubsortDeclSet -> Module . op setOps : Module OpDeclSet -> Module . op setMbs : Module MembAxSet -> Module . op setEqs : Module EquationSet -> Module . op setRls : Module RuleSet -> Module . op setClasses : Module ClassDeclSet -> Module . op setSubclasses : Module SubclassDeclSet -> Module . op setMsgs : Module MsgDeclSet -> Module . *** \item Functions to add new declarations to the set of declarations *** already in a unit. op addImports : ImportList Module -> Module . op addSorts : SortSet Module -> Module . op addSubsorts : [SubsortDeclSet] Module -> Module . op addOps : [OpDeclSet] Module -> Module . op addMbs : MembAxSet Module -> Module . op addEqs : EquationSet Module -> Module . op addRls : RuleSet Module -> Module . op addClasses : ClassDeclSet Module -> Module . op addSubclasses : SubclassDeclSet Module -> Module . op addMsgs : MsgDeclSet Module -> Module . *** \item There are functions and constants to create empty modules of the *** different types. For example, the function \texttt{emptyFTheory} *** returns an empty functional theory. There is also a *** function \texttt{empty} which takes a module as argument and returns *** an empty module of the same type. op emptyFModule : Header -> FModule . op emptyFModule : -> FModule . op emptySModule : -> SModule . op emptyOModule : -> OModule . op emptyFTheory : -> FModule . op emptySTheory : -> SModule . op emptyOTheory : -> OModule . op empty : Module -> Module . *** \item A function \texttt{addDecls} which returns the module resulting from *** adding all the declarations in the module passed as second argument *** to the module passed as first argument. op addDecls : Module Module -> Module . *** \end{itemize} *** Note that some of the `set' and `add' functions are partial functions. var M : Module . vars QI V : Qid . var S : Sort . vars SSDS SSDS' SSDS'' : SubsortDeclSet . vars OPD OPD' : OpDecl . vars OPDS OPDS' : OpDeclSet . var OPDS? : [OpDeclSet] . var At : Attr . vars MAS MAS' : MembAxSet . vars EqS EqS' : EquationSet . vars RlS RlS' : RuleSet . vars SS SS' : SortSet . vars IL IL' : ImportList . vars QIL QIL' : QidList . vars PL PL' : ParameterList . vars CDS CDS' : ClassDeclSet . vars SCD SCD' : SubclassDecl . vars SCDS SCDS' : SubclassDeclSet . vars U U' : Module . vars MDS MDS' : MsgDeclSet . vars I I' : Import . var T : Term . vars ME ME' : ModuleExpression . vars PD PD' : ParameterDecl . vars PDL PDL' : ParameterDeclList . var H : Header . vars MN MN' : ModuleName . eq I in (IL I IL') = true . eq I in IL = false [owise] . op eLeastSort : Module Term -> [Type] . eq eLeastSort(U, T) = leastSort(U, T) . eq eLeastSort(U, qidError(QIL)) = qidError(QIL) . op theory : Module -> Bool . eq theory(unitError(QIL)) = false . eq theory(mod H is IL sorts SS . SSDS OPDS MAS EqS RlS endm) = false . eq theory(th MN is IL sorts SS . SSDS OPDS MAS EqS RlS endth) = true . eq theory(fmod H is IL sorts SS . SSDS OPDS MAS EqS endfm) = false . eq theory(fth MN is IL sorts SS . SSDS OPDS MAS EqS endfth) = true . eq theory(omod H is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endom) = false . eq theory(oth MN is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endoth) = true . *** Selection functions for units eq getName(unitError(QIL)) = ' . eq getName(noModule) = ' . eq getName(mod ME is IL sorts SS . SSDS OPDS MAS EqS RlS endm) = ME . eq getName(mod ME{PDL} is IL sorts SS . SSDS OPDS MAS EqS RlS endm) = ME . eq getName(th MN is IL sorts SS . SSDS OPDS MAS EqS RlS endth) = MN . ----eq getName(th PD is IL sorts SS . SSDS OPDS MAS EqS RlS endth) = PD . eq getName(fmod ME is IL sorts SS . SSDS OPDS MAS EqS endfm) = ME . eq getName(fmod ME{PDL} is IL sorts SS . SSDS OPDS MAS EqS endfm) = ME . eq getName(fth MN is IL sorts SS . SSDS OPDS MAS EqS endfth) = MN . eq getName( omod ME is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endom) = ME . eq getName( omod ME{PDL} is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endom) = ME . eq getName( oth MN is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endoth) = MN . eq getImports(unitError(QIL)) = nil . eq getImports(noModule) = nil . eq getImports(mod H is IL sorts SS . SSDS OPDS MAS EqS RlS endm) = IL . eq getImports(th H is IL sorts SS . SSDS OPDS MAS EqS RlS endth) = IL . eq getImports(fmod H is IL sorts SS . SSDS OPDS MAS EqS endfm) = IL . eq getImports(fth H is IL sorts SS . SSDS OPDS MAS EqS endfth) = IL . eq getImports( omod H is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endom) = IL . eq getImports( oth H is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endoth) = IL . eq getPars(unitError(QIL)) = nil . eq getPars(noModule) = nil . eq getPars(mod ME is IL sorts SS . SSDS OPDS MAS EqS RlS endm) = nil . eq getPars(mod ME{PDL} is IL sorts SS . SSDS OPDS MAS EqS RlS endm) = PDL . eq getPars(mod nullHeader is IL sorts SS . SSDS OPDS MAS EqS RlS endm) = nil . eq getPars(th MN is IL sorts SS . SSDS OPDS MAS EqS RlS endth) = nil . eq getPars(th MN is IL sorts SS . SSDS OPDS MAS EqS RlS endth) = nil . eq getPars(fmod ME is IL sorts SS . SSDS OPDS MAS EqS endfm) = nil . eq getPars(fmod ME{PDL} is IL sorts SS . SSDS OPDS MAS EqS endfm) = PDL . eq getPars(fmod nullHeader is IL sorts SS . SSDS OPDS MAS EqS endfm) = nil . eq getPars(fth MN is IL sorts SS . SSDS OPDS MAS EqS endfth) = nil . eq getPars( omod ME is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endom) = nil . eq getPars( omod ME{PDL} is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endom) = PDL . eq getPars( omod nullHeader is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endom) = nil . eq getPars( oth MN is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endoth) = nil . eq getSorts(unitError(QIL)) = none . eq getSorts(mod H is IL sorts SS . SSDS OPDS MAS EqS RlS endm) = SS . eq getSorts(th H is IL sorts SS . SSDS OPDS MAS EqS RlS endth) = SS . eq getSorts(fmod H is IL sorts SS . SSDS OPDS MAS EqS endfm) = SS . eq getSorts(fth H is IL sorts SS . SSDS OPDS MAS EqS endfth) = SS . eq getSorts( omod H is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endom) = SS . eq getSorts( oth H is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endoth) = SS . op getAllSorts : Module -> SortSet . eq getAllSorts(M) = getSorts(M) . eq getSubsorts(unitError(QIL)) = none . eq getSubsorts(mod H is IL sorts SS . SSDS OPDS MAS EqS RlS endm) = SSDS . eq getSubsorts(th H is IL sorts SS . SSDS OPDS MAS EqS RlS endth) = SSDS . eq getSubsorts(fmod H is IL sorts SS . SSDS OPDS MAS EqS endfm) = SSDS . eq getSubsorts(fth H is IL sorts SS . SSDS OPDS MAS EqS endfth) = SSDS . eq getSubsorts( omod H is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endom) = SSDS . eq getSubsorts( oth H is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endoth) = SSDS . eq getOps(unitError(QIL)) = none . eq getOps(noModule) = none . eq getOps(mod H is IL sorts SS . SSDS OPDS MAS EqS RlS endm) = OPDS . eq getOps(th H is IL sorts SS . SSDS OPDS MAS EqS RlS endth) = OPDS . eq getOps(fmod H is IL sorts SS . SSDS OPDS MAS EqS endfm) = OPDS . eq getOps(fth H is IL sorts SS . SSDS OPDS MAS EqS endfth) = OPDS . eq getOps(omod H is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endom) = OPDS . eq getOps(oth H is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endoth) = OPDS . eq getMbs(unitError(QIL)) = none . eq getMbs(mod H is IL sorts SS . SSDS OPDS MAS EqS RlS endm) = MAS . eq getMbs(th H is IL sorts SS . SSDS OPDS MAS EqS RlS endth) = MAS . eq getMbs(fmod H is IL sorts SS . SSDS OPDS MAS EqS endfm) = MAS . eq getMbs(fth H is IL sorts SS . SSDS OPDS MAS EqS endfth) = MAS . eq getMbs(omod H is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endom) = MAS . eq getMbs(oth H is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endoth) = MAS . eq getEqs(unitError(QIL)) = none . eq getEqs(mod H is IL sorts SS . SSDS OPDS MAS EqS RlS endm) = EqS . eq getEqs(th H is IL sorts SS . SSDS OPDS MAS EqS RlS endth) = EqS . eq getEqs(fmod H is IL sorts SS . SSDS OPDS MAS EqS endfm) = EqS . eq getEqs(fth H is IL sorts SS . SSDS OPDS MAS EqS endfth) = EqS . eq getEqs(omod H is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endom) = EqS . eq getEqs(oth H is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endoth) = EqS . eq getRls(unitError(QIL)) = none . eq getRls(mod H is IL sorts SS . SSDS OPDS MAS EqS RlS endm) = RlS . eq getRls(th H is IL sorts SS . SSDS OPDS MAS EqS RlS endth) = RlS . eq getRls(fmod H is IL sorts SS . SSDS OPDS MAS EqS endfm) = none . eq getRls(fth H is IL sorts SS . SSDS OPDS MAS EqS endfth) = none . eq getRls(omod H is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endom) = RlS . eq getRls(oth H is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endoth) = RlS . eq getClasses(unitError(QIL)) = none . eq getClasses(mod H is IL sorts SS . SSDS OPDS MAS EqS RlS endm) = none . eq getClasses(th H is IL sorts SS . SSDS OPDS MAS EqS RlS endth) = none . eq getClasses(fmod H is IL sorts SS . SSDS OPDS MAS EqS endfm) = none . eq getClasses(fth H is IL sorts SS . SSDS OPDS MAS EqS endfth) = none . eq getClasses( omod H is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endom) = CDS . eq getClasses( oth H is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endoth) = CDS . eq getSubclasses(unitError(QIL)) = none . eq getSubclasses(mod H is IL sorts SS . SSDS OPDS MAS EqS RlS endm) = none . eq getSubclasses(th H is IL sorts SS . SSDS OPDS MAS EqS RlS endth) = none . eq getSubclasses(fmod H is IL sorts SS . SSDS OPDS MAS EqS endfm) = none . eq getSubclasses(fth H is IL sorts SS . SSDS OPDS MAS EqS endfth) = none . eq getSubclasses( omod H is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endom) = SCDS . eq getSubclasses( oth H is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endoth) = SCDS . eq getMsgs(unitError(QIL)) = none . eq getMsgs(mod H is IL sorts SS . SSDS OPDS MAS EqS RlS endm) = none . eq getMsgs(th H is IL sorts SS . SSDS OPDS MAS EqS RlS endth) = none . eq getMsgs(fmod H is IL sorts SS . SSDS OPDS MAS EqS endfm) = none . eq getMsgs(fth H is IL sorts SS . SSDS OPDS MAS EqS endfth) = none . eq getMsgs(omod H is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endom) = MDS . eq getMsgs(oth H is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endoth) = MDS . *** Set functions eq setImports(unitError(QIL), IL) = unitError(QIL) . eq setImports(noModule, IL) = noModule . eq setImports(mod H is IL sorts SS . SSDS OPDS MAS EqS RlS endm, IL') = mod H is IL' sorts SS . SSDS OPDS MAS EqS RlS endm . eq setImports(th H is IL sorts SS . SSDS OPDS MAS EqS RlS endth, IL') = th H is IL' sorts SS . SSDS OPDS MAS EqS RlS endth . eq setImports(fmod H is IL sorts SS . SSDS OPDS MAS EqS endfm, IL') = fmod H is IL' sorts SS . SSDS OPDS MAS EqS endfm . eq setImports(fth H is IL sorts SS . SSDS OPDS MAS EqS endfth, IL') = fth H is IL' sorts SS . SSDS OPDS MAS EqS endfth . eq setImports( omod H is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endom, IL') = omod H is IL' sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endom . eq setImports( oth H is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endoth, IL') = oth H is IL' sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endoth . eq setOps(unitError(QIL), OPDS) = unitError(QIL) . eq setOps(noModule, OPDS) = noModule . eq setOps(U, opDeclError(QIL) OPDS) = unitError(QIL) . eq setOps(unitError(QIL), opDeclError(QIL') OPDS) = unitError(QIL QIL') . eq setOps(mod H is IL sorts SS . SSDS OPDS MAS EqS RlS endm, OPDS') = mod H is IL sorts SS . SSDS OPDS' MAS EqS RlS endm . eq setOps(th MN is IL sorts SS . SSDS OPDS MAS EqS RlS endth, OPDS') = th MN is IL sorts SS . SSDS OPDS' MAS EqS RlS endth . eq setOps(fmod H is IL sorts SS . SSDS OPDS MAS EqS endfm, OPDS') = fmod H is IL sorts SS . SSDS OPDS' MAS EqS endfm . eq setOps(fth MN is IL sorts SS . SSDS OPDS MAS EqS endfth, OPDS') = fth MN is IL sorts SS . SSDS OPDS' MAS EqS endfth . eq setOps(omod H is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endom, OPDS') = omod H is IL sorts SS . SSDS CDS SCDS OPDS' MDS MAS EqS RlS endom . eq setOps(oth MN is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endoth, OPDS') = oth MN is IL sorts SS . SSDS CDS SCDS OPDS' MDS MAS EqS RlS endoth . eq setSubsorts(unitError(QIL), SSDS) = unitError(QIL) . eq setSubsorts(mod H is IL sorts SS . SSDS OPDS MAS EqS RlS endm, SSDS') = mod H is IL sorts SS . SSDS' OPDS MAS EqS RlS endm . eq setSubsorts(th MN is IL sorts SS . SSDS OPDS MAS EqS RlS endth, SSDS') = th MN is IL sorts SS . SSDS' OPDS MAS EqS RlS endth . eq setSubsorts(fmod H is IL sorts SS . SSDS OPDS MAS EqS endfm, SSDS') = fmod H is IL sorts SS . SSDS' OPDS MAS EqS endfm . eq setSubsorts(fth MN is IL sorts SS . SSDS OPDS MAS EqS endfth, SSDS') = fth MN is IL sorts SS . SSDS' OPDS MAS EqS endfth . eq setSubsorts( omod H is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endom, SSDS') = omod H is IL sorts SS . SSDS' CDS SCDS OPDS MDS MAS EqS RlS endom . eq setSubsorts( oth MN is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endoth, SSDS') = oth MN is IL sorts SS . SSDS' CDS SCDS OPDS MDS MAS EqS RlS endoth . eq setMbs(unitError(QIL), MAS) = unitError(QIL) . eq setMbs(U, membAxError(QIL) MAS) = unitError(QIL) . eq setMbs(mod H is IL sorts SS . SSDS OPDS MAS EqS RlS endm, MAS') = mod H is IL sorts SS . SSDS OPDS MAS' EqS RlS endm . eq setMbs(th MN is IL sorts SS . SSDS OPDS MAS EqS RlS endth, MAS') = th MN is IL sorts SS . SSDS OPDS MAS' EqS RlS endth . eq setMbs(fmod H is IL sorts SS . SSDS OPDS MAS EqS endfm, MAS') = fmod H is IL sorts SS . SSDS OPDS MAS' EqS endfm . eq setMbs(fth MN is IL sorts SS . SSDS OPDS MAS EqS endfth, MAS') = fth MN is IL sorts SS . SSDS OPDS MAS' EqS endfth . eq setMbs( omod H is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endom, MAS') = omod H is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS' EqS RlS endom . eq setMbs( oth MN is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endoth, MAS') = oth MN is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS' 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 H is IL sorts SS . SSDS OPDS MAS EqS RlS endm, EqS') = mod H is IL sorts SS . SSDS OPDS MAS EqS' RlS endm . eq setEqs(th MN is IL sorts SS . SSDS OPDS MAS EqS RlS endth, EqS') = th MN is IL sorts SS . SSDS OPDS MAS EqS' RlS endth . eq setEqs(fmod H is IL sorts SS . SSDS OPDS MAS EqS endfm, EqS') = fmod H is IL sorts SS . SSDS OPDS MAS EqS' endfm . eq setEqs(fth MN is IL sorts SS . SSDS OPDS MAS EqS endfth, EqS') = fth MN is IL sorts SS . SSDS OPDS MAS EqS' endfth . eq setEqs( omod H is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endom, EqS') = omod H is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS' RlS endom . eq setEqs( oth MN is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endoth, EqS') = oth MN is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS' RlS endoth . op setRls : [Module] [RuleSet] -> [Module] . var U? : [Module] . var RlS? : [RuleSet] . eq setRls(unitError(QIL), RlS?) = unitError(QIL) . eq setRls(U?, ruleError(QIL) RlS?) = unitError(QIL) . eq setRls(mod H is IL sorts SS . SSDS OPDS MAS EqS RlS endm, RlS') = mod H is IL sorts SS . SSDS OPDS MAS EqS RlS' endm . eq setRls(th MN is IL sorts SS . SSDS OPDS MAS EqS RlS endth, RlS') = th MN is IL sorts SS . SSDS OPDS MAS EqS RlS' endth . eq setRls(fmod H is IL sorts SS . SSDS OPDS MAS EqS endfm, RlS) = if RlS == none then fmod H is IL sorts SS . SSDS OPDS MAS EqS endfm else mod H is IL sorts SS . SSDS OPDS MAS EqS RlS endm fi . eq setRls(fth MN is IL sorts SS . SSDS OPDS MAS EqS endfth, RlS) = if RlS == none then fth MN is IL sorts SS . SSDS OPDS MAS EqS endfth else th MN is IL sorts SS . SSDS OPDS MAS EqS RlS endth fi . eq setRls(omod H is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endom, RlS') = omod H is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS' endom . eq setRls(oth MN is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endoth, RlS') = oth MN is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS' endoth . eq setSorts(unitError(QIL), SS) = unitError(QIL) . eq setSorts(mod H is IL sorts SS . SSDS OPDS MAS EqS RlS endm, SS') = mod H is IL sorts SS' . SSDS OPDS MAS EqS RlS endm . eq setSorts(th MN is IL sorts SS . SSDS OPDS MAS EqS RlS endth, SS') = th MN is IL sorts SS' . SSDS OPDS MAS EqS RlS endth . eq setSorts(fmod H is IL sorts SS . SSDS OPDS MAS EqS endfm, SS') = fmod H is IL sorts SS' . SSDS OPDS MAS EqS endfm . eq setSorts(fth MN is IL sorts SS . SSDS OPDS MAS EqS endfth, SS') = fth MN is IL sorts SS' . SSDS OPDS MAS EqS endfth . eq setSorts( omod H is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endom, SS') = omod H is IL sorts SS' . SSDS CDS SCDS OPDS MDS MAS EqS RlS endom . eq setSorts( oth MN is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endoth, SS') = oth MN is IL sorts SS' . SSDS CDS SCDS OPDS MDS MAS EqS RlS endoth . eq setPars(mod ME is IL sorts SS . SSDS OPDS MAS EqS RlS endm, PDL) = if PDL == nil then mod ME is IL sorts SS . SSDS OPDS MAS EqS RlS endm else mod ME{PDL} is IL sorts SS . SSDS OPDS MAS EqS RlS endm fi . eq setPars(mod ME{PDL} is IL sorts SS . SSDS OPDS MAS EqS RlS endm, PDL') = if PDL' == nil then mod ME is IL sorts SS . SSDS OPDS MAS EqS RlS endm else mod ME{PDL'} is IL sorts SS . SSDS OPDS MAS EqS RlS endm fi . eq setPars(th MN is IL sorts SS . SSDS OPDS MAS EqS RlS endth, PDL) = th MN is IL sorts SS . SSDS OPDS MAS EqS RlS endth . eq setPars(fmod ME is IL sorts SS . SSDS OPDS MAS EqS endfm, PDL) = if PDL == nil then fmod ME is IL sorts SS . SSDS OPDS MAS EqS endfm else fmod ME{PDL} is IL sorts SS . SSDS OPDS MAS EqS endfm fi . eq setPars(fmod ME{PDL} is IL sorts SS . SSDS OPDS MAS EqS endfm, PDL') = if PDL' == nil then fmod ME is IL sorts SS . SSDS OPDS MAS EqS endfm else fmod ME{PDL'} is IL sorts SS . SSDS OPDS MAS EqS endfm fi . eq setPars(fth MN is IL sorts SS . SSDS OPDS MAS EqS endfth, PDL) = fth MN is IL sorts SS . SSDS OPDS MAS EqS endfth . eq setPars( omod ME is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endom, PDL) = if PDL == nil then omod ME is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endom else omod ME{PDL} is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endom fi . eq setPars( omod ME{PDL} is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endom, PDL') = if PDL' == nil then omod ME is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endom else omod ME{PDL'} is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endom fi . eq setPars( oth MN is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endoth, PDL) = oth MN is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endoth . eq setClasses(fmod H is IL sorts SS . SSDS OPDS MAS EqS endfm, CDS) = if CDS == none then fmod H is IL sorts SS . SSDS OPDS MAS EqS endfm else omod H is IL sorts SS . SSDS CDS none OPDS none MAS EqS none endom fi . eq setClasses(fth H is IL sorts SS . SSDS OPDS MAS EqS endfth, CDS) = if CDS == none then fth H is IL sorts SS . SSDS OPDS MAS EqS endfth else oth H is IL sorts SS . SSDS CDS none OPDS none MAS EqS none endoth fi . eq setClasses(mod H is IL sorts SS . SSDS OPDS MAS EqS RlS endm, CDS) = if CDS == none then mod H is IL sorts SS . SSDS OPDS MAS EqS RlS endm else omod H is IL sorts SS . SSDS CDS none OPDS none MAS EqS RlS endom fi . eq setClasses(th H is IL sorts SS . SSDS OPDS MAS EqS RlS endth, CDS) = if CDS == none then th H is IL sorts SS . SSDS OPDS MAS EqS RlS endth else oth H is IL sorts SS . SSDS CDS none OPDS none MAS EqS RlS endoth fi . eq setClasses( omod H is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endom, CDS') = omod H is IL sorts SS . SSDS CDS' SCDS OPDS MDS MAS EqS RlS endom . eq setClasses( oth H is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endoth, CDS') = oth H is IL sorts SS . SSDS CDS' SCDS OPDS MDS MAS EqS RlS endoth . eq setClasses(M, CDS) = unitError(header2QidList(getName(M)) 'not 'an 'object-oriented 'module) [owise] . eq setSubclasses(fmod H is IL sorts SS . SSDS OPDS MAS EqS endfm, SCDS) = if SCDS == none then fmod H is IL sorts SS . SSDS OPDS MAS EqS endfm else omod H is IL sorts SS . SSDS none SCDS OPDS none MAS EqS none endom fi . eq setSubclasses(fth H is IL sorts SS . SSDS OPDS MAS EqS endfth, SCDS) = if SCDS == none then fth H is IL sorts SS . SSDS OPDS MAS EqS endfth else oth H is IL sorts SS . SSDS none SCDS OPDS none MAS EqS none endoth fi . eq setSubclasses(mod H is IL sorts SS . SSDS OPDS MAS EqS RlS endm, SCDS) = if SCDS == none then mod H is IL sorts SS . SSDS OPDS MAS EqS RlS endm else omod H is IL sorts SS . SSDS none SCDS OPDS none MAS EqS RlS endom fi . eq setSubclasses(th H is IL sorts SS . SSDS OPDS MAS EqS RlS endth, SCDS) = if SCDS == none then th H is IL sorts SS . SSDS OPDS MAS EqS RlS endth else oth H is IL sorts SS . SSDS none SCDS OPDS none MAS EqS RlS endoth fi . eq setSubclasses( omod H is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endom, SCDS') = omod H is IL sorts SS . SSDS CDS SCDS' OPDS MDS MAS EqS RlS endom . eq setSubclasses( oth H is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endoth, SCDS') = oth H is IL sorts SS . SSDS CDS SCDS' OPDS MDS MAS EqS RlS endoth . eq setSubclasses(M, SCDS) = unitError(header2QidList(getName(M)) 'not 'an 'object-oriented 'module) [owise] . eq setMsgs( fmod H is IL sorts SS . SSDS OPDS MAS EqS endfm, MDS) = if MDS == none then fmod H is IL sorts SS . SSDS OPDS MAS EqS endfm else omod H is IL sorts SS . SSDS none none OPDS MDS MAS EqS none endom fi . eq setMsgs( fth H is IL sorts SS . SSDS OPDS MAS EqS endfth, MDS) = if MDS == none then fth H is IL sorts SS . SSDS OPDS MAS EqS endfth else oth H is IL sorts SS . SSDS none none OPDS MDS MAS EqS none endoth fi . eq setMsgs( mod H is IL sorts SS . SSDS OPDS MAS EqS RlS endm, MDS) = if MDS == none then mod H is IL sorts SS . SSDS OPDS MAS EqS RlS endm else omod H is IL sorts SS . SSDS none none OPDS MDS MAS EqS RlS endom fi . eq setMsgs( th H is IL sorts SS . SSDS OPDS MAS EqS RlS endth, MDS) = if MDS == none then th H is IL sorts SS . SSDS OPDS MAS EqS RlS endth else oth H is IL sorts SS . SSDS none none OPDS MDS MAS EqS RlS endoth fi . eq setMsgs( omod H is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endom, MDS') = omod H is IL sorts SS . SSDS CDS SCDS OPDS MDS' MAS EqS RlS endom . eq setMsgs( oth H is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endoth, MDS') = oth H is IL sorts SS . SSDS CDS SCDS OPDS MDS' MAS EqS RlS endoth . eq setMsgs(M, MDS) = unitError(header2QidList(getName(M)) 'not 'an 'object-oriented 'module) [owise] . eq setName(mod ME is IL sorts SS . SSDS OPDS MAS EqS RlS endm, ME') = mod ME' is IL sorts SS . SSDS OPDS MAS EqS RlS endm . eq setName(mod ME{PDL} is IL sorts SS . SSDS OPDS MAS EqS RlS endm, ME') = mod ME'{PDL} is IL sorts SS . SSDS OPDS MAS EqS RlS endm . eq setName(fmod ME is IL sorts SS . SSDS OPDS MAS EqS endfm, ME') = fmod ME' is IL sorts SS . SSDS OPDS MAS EqS endfm . eq setName(fmod ME{PDL} is IL sorts SS . SSDS OPDS MAS EqS endfm, ME') = fmod ME'{PDL} is IL sorts SS . SSDS OPDS MAS EqS endfm . eq setName(fth MN is IL sorts SS . SSDS OPDS MAS EqS endfth, MN') = fth MN' is IL sorts SS . SSDS OPDS MAS EqS endfth . eq setName(th MN is IL sorts SS . SSDS OPDS MAS EqS RlS endth, MN') = th MN' is IL sorts SS . SSDS OPDS MAS EqS RlS endth . eq setName( omod ME is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endom, ME') = omod ME' is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endom . eq setName( omod ME{PDL} is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endom, ME') = omod ME'{PDL} is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endom . eq setName( oth MN is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endoth, MN') = oth MN' is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endoth . eq setName(noModule, ME) = noModule . eq setName(unitError(QIL), ME) = unitError(QIL) . eq setName(mod nullHeader is IL sorts SS . SSDS OPDS MAS EqS RlS endm, ME') = mod ME' is IL sorts SS . SSDS OPDS MAS EqS RlS endm . eq setName(fmod nullHeader is IL sorts SS . SSDS OPDS MAS EqS endfm, ME') = fmod ME' is IL sorts SS . SSDS OPDS MAS EqS endfm . eq setName(fth nullHeader is IL sorts SS . SSDS OPDS MAS EqS endfth, MN) = fth MN is IL sorts SS . SSDS OPDS MAS EqS endfth . eq setName(th nullHeader is IL sorts SS . SSDS OPDS MAS EqS RlS endth, MN) = th MN is IL sorts SS . SSDS OPDS MAS EqS RlS endth . eq setName( omod nullHeader is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endom, ME') = omod ME' is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endom . eq setName( oth nullHeader is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endoth, MN) = oth MN is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endoth . eq setName(noModule, ME) = noModule . eq setName(unitError(QIL), ME) = unitError(QIL) . *** Add functions eq addSorts(SS, U) = setSorts(U, (SS ; getSorts(U))) . eq addSubsorts(SSDS, U) = setSubsorts(U, (SSDS getSubsorts(U))) . eq addSubsorts(subsortDeclError(QIL), U) = unitError(QIL) . eq addOps(OPDS, U) = setOps(U, (OPDS getOps(U))) . eq addOps(OPDS?, unitError(QIL)) = unitError(QIL) . eq addOps(OPDS?, U) = U [owise] . eq addMbs(MAS, U) = setMbs(U, (MAS getMbs(U))) . eq addMbs(MAS, unitError(QIL)) = unitError(QIL) . eq addEqs(EqS, U) = setEqs(U, (EqS getEqs(U))) . eq addEqs(EqS, unitError(QIL)) = unitError(QIL) . eq addRls(RlS, U) = setRls(U, (RlS getRls(U))) . eq addRls(RlS, unitError(QIL)) = unitError(QIL) . eq addImports(IL, U) = setImports(U, (getImports(U) IL)) . eq addImports(IL, unitError(QIL)) = unitError(QIL) . eq addClasses(CDS, U) = setClasses(U, (getClasses(U) CDS)) . eq addClasses(CDS, unitError(QIL)) = unitError(QIL) . eq addSubclasses(SCDS, U) = setSubclasses(U, (getSubclasses(U) SCDS)) . eq addSubclasses(SCDS, unitError(QIL)) = unitError(QIL) . eq addMsgs(MDS, U) = setMsgs(U, (getMsgs(U) MDS)) . eq addMsgs(MDS, unitError(QIL)) = unitError(QIL) . *** Creation of empty units eq emptyFModule(ME) = fmod header2Qid(ME) is nil sorts none . none none none none endfm . eq emptyFModule = fmod nullHeader is nil sorts none . none none none none endfm . eq emptySModule = mod nullHeader is nil sorts none . none none none none none endm . eq emptyOModule = omod nullHeader is nil sorts none . none none none none none none none none endom . eq emptyFTheory = fth nullHeader is nil sorts none . none none none none endfth . eq emptySTheory = th nullHeader is nil sorts none . none none none none none endth . eq emptyOTheory = oth nullHeader is 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 H is IL sorts SS . SSDS OPDS MAS EqS RlS endm) = (mod H is nil sorts none . none none none none none endm) . eq empty(th MN is IL sorts SS . SSDS OPDS MAS EqS RlS endth) = (th MN is nil sorts none . none none none none none endth) . eq empty(fmod H is IL sorts SS . SSDS OPDS MAS EqS endfm) = (fmod H is nil sorts none . none none none none endfm) . eq empty(fth MN is IL sorts SS . SSDS OPDS MAS EqS endfth) = (fth MN is nil sorts none . none none none none endfth) . eq empty(omod H is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endom) = (omod H is nil sorts none . none none none none none none none none endom) . eq empty(oth MN is IL sorts SS . SSDS CDS SCDS OPDS MDS MAS EqS RlS endoth) = (oth MN is 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(noModule, U) = U . eq addDecls(U, noModule) = U . eq addDecls(unitError(QIL), U) = unitError(QIL) . eq addDecls(U, unitError(QIL)) = unitError(QIL) . eq addDecls(U, U') = addImports(getImports(U'), addSorts(getSorts(U'), addSubsorts(getSubsorts(U'), addOps(getOps(U'), addMbs(getMbs(U'), addEqs(getEqs(U'), if U' :: FModule or U' :: FTheory then U else addRls(getRls(U'), if U' :: SModule or U' :: STheory then U else addClasses(getClasses(U'), addSubclasses(getSubclasses(U'), addMsgs(getMsgs(U'), U))) fi) fi)))))) [owise] . 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 sTS of renaming maps *** in Section~\ref{renaming-maps}, we then introduce view maps and sTS 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{Renaming}, *** 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 FMAP . pr EXT-DECL . op termMap : Term Term -> ViewMap . sorts ViewMap Set{ViewMap} . subsorts Renaming < ViewMap . subsorts ViewMap RenamingSet < Set{ViewMap} . op _`,_ : Set{ViewMap} Set{ViewMap} -> Set{ViewMap} [ditto] . eq (VMAP, none) = VMAP . eq (VMAP, VMAP) = VMAP . var MAP : Renaming . var VMAP : ViewMap . var VMAPS : Set{ViewMap} . vars T T' : Term . vars S S' : Sort . *** As for sTS of maps, \texttt{SortRenamingSet} returns the subset of sort *** maps in a set of view maps. op sortMaps : Set{ViewMap} -> RenamingSet . eq sortMaps((sort S to S')) = (sort S to S') . eq sortMaps(((sort S to S'), VMAPS)) = ((sort S to S'), sortMaps(VMAPS)) . eq sortMaps(VMAP) = none [owise] . eq sortMaps((VMAP, VMAPS)) = none [owise] . eq sortMaps(none) = none . endfm ------------------------------------------------------------------------------- ******************************************************************************* ------------------------------------------------------------------------------- *** *** Views *** *** The \texttt{View} sort is introduced in the following module *** \texttt{VIEW}. In addition to the constructor for views (\texttt{view}), *** selector functions are added for each of the components of a *** view (\texttt{name}, \texttt{source}, \texttt{target}, and *** \texttt{mapSet}), and a constant \texttt{emptyView}, which is identified *** in an equation with the empty view, is defined. *** Although the declaration of the constructor for views includes an argument *** for the list of parameters, parameterized views are not handled yet, so at *** present this argument must be set to the \texttt{nil}. ------------------------------------------------------------------------------- ******************************************************************************* ------------------------------------------------------------------------------- fmod VIEW is pr META-MODULE . pr VIEW-EXPR . pr VIEW-MAP . sorts View ViewHeader . subsort ViewExp Header < ViewHeader . op view_from_to_is_endv : ViewHeader ModuleExpression ModuleExpression Set{ViewMap} -> View [ctor format (nir! o r! o r! o r! o r! o)] . op null : -> View [ctor] . op viewError : QidList -> [View] [ctor format (r o)] . eq VE{(nil).ParameterDeclList} = VE . var QI : Qid . vars VE VE' : ViewExp . vars PDL PDL' : ParameterDeclList . vars ME ME' ME'' : ModuleExpression . vars VMAPS VMAPS' : Set{ViewMap} . var QIL : QidList . var VH : ViewHeader . op name : View -> ViewExp . op getPars : [View] -> ParameterDeclList . op source : View -> ModuleExpression . op target : View -> ModuleExpression . op mapSet : View -> RenamingSet . eq name(view VE from ME to ME' is VMAPS endv) = VE . eq name(view VE{PDL} from ME to ME' is VMAPS endv) = VE . eq getPars(view VE from ME to ME' is VMAPS endv) = nil . eq getPars(view VE{PDL} from ME to ME' is VMAPS endv) = PDL . eq getPars(viewError(QIL)) = nil . eq source(view VH from ME to ME' is VMAPS endv) = ME . eq target(view VH from ME to ME' is VMAPS endv) = ME' . eq mapSet(view VH from ME to ME' is VMAPS endv) = VMAPS . op setName : View ViewExp ~> View . op setPars : View ParameterDeclList ~> View . op setTarget : View ModuleExpression ~> View . op sTSource : View ModuleExpression ~> View . op setMaps : View RenamingSet ~> View . eq setName(view VE from ME to ME' is VMAPS endv, VE') = view VE' from ME to ME' is VMAPS endv . eq setName(view VE{PDL} from ME to ME' is VMAPS endv, VE') = view VE'{PDL} from ME to ME' is VMAPS endv . eq setName(viewError(QIL), VE) = viewError(QIL) . eq setPars(view VE from ME to ME' is VMAPS endv, PDL) = view VE{PDL} from ME to ME' is VMAPS endv . eq setPars(view VE{PDL} from ME to ME' is VMAPS endv, PDL') = view VE{PDL'} from ME to ME' is VMAPS endv . eq setPars(viewError(QIL), PDL) = viewError(QIL) . eq sTSource(view VH from ME to ME' is VMAPS endv, ME'') = view VH from ME'' to ME' is VMAPS endv . eq sTSource(viewError(QIL), ME) = viewError(QIL) . eq setTarget(view VH from ME to ME' is VMAPS endv, ME'') = view VH from ME to ME'' is VMAPS endv . eq setTarget(viewError(QIL), ME) = viewError(QIL) . eq setMaps(view VH from ME to ME' is VMAPS endv, VMAPS') = view VH from ME to ME' is VMAPS' endv . eq setMaps(viewError(QIL), VMAPS) = viewError(QIL) . op emptyView : Qid ModuleExpression ModuleExpression -> View . eq emptyView(QI, ME, ME') = view QI from ME to ME' is none endv . 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 CONFIGURATION+ : -> SModule [memo] . eq CONFIGURATION+ = (mod 'CONFIGURATION+ is 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) . *** 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 : -> FModule [memo] . eq UP = (fmod 'UP is including 'QID-LIST . including 'MOD-EXPRS . sorts none . none op 'upTerm : '@ModExp@ '@Bubble@ -> 'Term [none] . op 'upModule : '@ModExp@ -> 'Module [none] . op '`[_`] : '@Token@ -> 'Module [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 ------------------------------------------------------------------------------- ******************************************************************************* ------------------------------------------------------------------------------- *** *** 7 The Evaluation of Views *** *** Before being entered into the database, besides containing bubbles, views *** have a somewhat different structure from that of the views given in *** Section~\ref{viewADT}. We introduce in the following module a sort *** \texttt{PreView} with constructor \texttt{view}, which is declared as the *** constructor for views of sort \texttt{View}, but with an additional *** argument, namely, a set of variable declarations to hold the declarations *** of variables in the view. During the processing of views (see *** Section~\ref{view-processing}), which takes place once the parsing process *** has concluded, these variables are associated with the corresponding maps *** where they are used, generating a term of sort \texttt{View}. *** We start by introducing in the following module \texttt{PRE-VIEW-MAP} the *** sorts \texttt{TermPreMap}, \texttt{PreViewMap}, and *** \texttt{Set{PreViewMap}}. A preview map is a view map with bubbles. Note *** that the bubbles can only appear in term maps. Elements of sort *** \texttt{TermPreMap} are built with the constructor \texttt{preTermMap}, *** which takes two terms of sort \texttt{Term}, that is, two bubbles. In the *** processing of views (see Section~\ref{view-processing}), elements of sort *** \texttt{PreTermMap} will be converted into elements of sort *** \texttt{TermMap} by parsing the bubbles in them, and by associating to *** them the variables in them defined in the view in which the maps appear. ------------------------------------------------------------------------------- ******************************************************************************* ------------------------------------------------------------------------------- fmod PRE-VIEW-MAP is pr VIEW-MAP . sort PreViewMap . subsorts Renaming < PreViewMap . op preTermMap : Term Term -> PreViewMap . sort Set{PreViewMap} . subsorts PreViewMap RenamingSet < Set{PreViewMap} . op _`,_ : Set{PreViewMap} Set{PreViewMap} -> Set{PreViewMap} [ditto] . eq (PVMAPS, none) = PVMAPS . var PVMAP : PreViewMap . var PVMAPS : Set{PreViewMap} . vars S S' : Sort . *** Given a set of maps, the function \texttt{sortMaps} returns the subset *** of sort maps in it. op sortMaps : Set{PreViewMap} -> RenamingSet . eq sortMaps(((sort S to S'), PVMAPS)) = ((sort S to S'), sortMaps(PVMAPS)) . eq sortMaps((PVMAP, PVMAPS)) = none [owise] . eq sortMaps(none) = none . endfm ------------------------------------------------------------------------------- ******************************************************************************* ------------------------------------------------------------------------------- fmod PRE-VIEW is pr VIEW . pr PRE-VIEW-MAP . sort PreView . op preview_from_to_is__endpv : ViewHeader ModuleExpression ModuleExpression OpDeclSet Set{PreViewMap} -> PreView [ctor format (nir! o r! o r! o r! o o r! o)] . op null : -> PreView . op name : PreView -> ViewExp . op getPars : PreView -> ParameterDeclList . op source : PreView -> ModuleExpression . op target : PreView -> ModuleExpression . op vars : PreView -> OpDeclSet . op mapSet : PreView -> Set{PreViewMap} . var QI : Qid . vars ME ME' : ModuleExpression . var VE : ViewExp . var VH : ViewHeader . vars PDL PDL' : ParameterDeclList . vars VDS VDS' : OpDeclSet . vars PVMAPS PVMAPS' : Set{PreViewMap} . eq name(preview VE from ME to ME' is VDS PVMAPS endpv) = VE . eq name(preview VE{PDL} from ME to ME' is VDS PVMAPS endpv) = VE . eq getPars(preview VE from ME to ME' is VDS PVMAPS endpv) = nil . eq getPars(preview VE{PDL} from ME to ME' is VDS PVMAPS endpv) = PDL . eq source(preview VH from ME to ME' is VDS PVMAPS endpv) = ME . eq target(preview VH from ME to ME' is VDS PVMAPS endpv) = ME' . eq vars(preview VH from ME to ME' is VDS PVMAPS endpv) = VDS . eq mapSet(preview VH from ME to ME' is VDS PVMAPS endpv) = PVMAPS . *** The following functions can be used to add new declarations to the set of *** declarations already in a preview. op addMaps : Set{PreViewMap} PreView -> PreView . op addVars : OpDeclSet PreView -> PreView . eq addMaps(PVMAPS, preview VH from ME to ME' is VDS PVMAPS' endpv) = preview VH from ME to ME' is VDS (PVMAPS, PVMAPS') endpv . eq addVars(VDS, preview VH from ME to ME' is VDS' PVMAPS' endpv) = preview VH from ME to ME' is (VDS VDS') PVMAPS' endpv . op setPars : PreView ParameterDeclList -> PreView . eq setPars(preview VE from ME to ME' is VDS PVMAPS endpv, PDL) = preview VE{PDL} from ME to ME' is VDS PVMAPS endpv . eq setPars(preview VE{PDL} from ME to ME' is VDS PVMAPS endpv, PDL') = preview VE{PDL'} from ME to ME' is VDS PVMAPS endpv . op emptyPreView : Qid ModuleExpression ModuleExpression -> PreView . eq emptyPreView(QI, ME, ME') = preview QI from ME to ME' is none none endpv . 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{ModuleInfo} and \texttt{ViewInfo}, in *** which we hold, respectively, the information concerning units and views. *** For each unit we save: *** \begin{itemize} *** \item Its original form, as introduced by the user, or, in case of an *** internally generated unit, as generated from the original form of *** some other unit. *** \item Its internal representation, in which variables have been renamed *** to avoid collisions with the names of variables in other units in *** the same hierarchy. In the case of object-oriented units, we store *** its equivalent system module, that is, the result of transforming *** it into a system module. *** \item Its signature, which is given as a functional module of sort *** \texttt{FModule} with no axioms, ready to be used in calls to *** \texttt{metaParse}. There can only be importation declarations *** including built-in modules in this module. These are the only *** inclusions handled by the Core Maude engine. *** \item Its flattened version, for which, as for signatures, only the *** importation of built-in modules is left unevaluated. *** \end{itemize} *** For each view we keep its name and the view itself. *** As a simple mechanism to keep the database consistent, for each unit we *** maintain the list of names of all the units and views ``depending'' on it. *** Similarly, for each view we maintain the list of names of all the units *** ``depending'' on it. The idea is that if a unit or view is redefined or *** removed, all those units and/or views depending on it will also be *** removed. This dependency does not only mean direct importation. For *** example, the module resulting from the renaming of some module also *** depends on the module being renamed; the instantiation of a parameterized *** module also depends on the parameterized module and on all the views used *** in its instantiation; a view depends on its source and target units, etc. *** This dependency is transitive: if a module, theory, or view has to be *** removed, all the units and/or views depending on them will be removed as *** well. The dependencies derived from the module expressions themselves are *** established by the function \texttt{setUpModExpDeps}. The function *** \texttt{setUpModuleDeps} calls \texttt{setUpModExpDeps}, *** and then \texttt{setUpImportSetDeps} to add the \emph{back *** references} in the modules being imported. The function *** \texttt{setUpViewDeps} sTS up the back references for the views *** being introduced. *** In addition to this set of information cells for units and views, we also *** keep lists with the names of all the units and views in the database, and *** a list of quoted identifiers in which we store the messages generated *** during the process of treatment of the inputs in order to simplify the *** communication with the read-eval-print loop process. ------------------------------------------------------------------------------- ******************************************************************************* ------------------------------------------------------------------------------- fmod 2TUPLE{X :: TRIV, Y :: TRIV} is sorts Tuple{X, Y} . op `(_`,_`) : X$Elt Y$Elt -> Tuple{X, Y} . op p1_ : Tuple{X, Y} -> X$Elt . op p2_ : Tuple{X, Y} -> Y$Elt . eq p1(V1:X$Elt,V2:Y$Elt) = V1:X$Elt . eq p2(V1:X$Elt,V2:Y$Elt) = V2:Y$Elt . endfm view ModuleName from TRIV to MOD-NAME is sort Elt to ModuleName . endv view ViewExp from TRIV to VIEW-EXPR is sort Elt to ViewExp . endv view ParameterDecl from TRIV to META-MODULE is sort Elt to ParameterDecl . endv fmod INFO is pr VIEW . pr DEFAULT-VALUE{Term} . pr (SET * (op _`,_ to _._, op empty to emptyModuleNameSet, op insert to insertModuleNameSet, op delete to deleteModuleNameSet, op _in_ to _inModuleNameSet_, op |_| to |_|ModuleNameSet, op $card to $cardModuleNameSet, op union to unionModuleNameSet, op intersection to intersectionModuleNameSet, op $intersect to $intersectModuleNameSet, op _\_ to _\ModuleNameSet_, op $diff to $diffModuleNameSet)){ModuleName} . pr (SET * (op _`,_ to _#_, op empty to emptyViewExpSet, op insert to insertViewExpSet, op delete to deleteViewExpSet, op _in_ to _inViewExpSet_, op |_| to |_|ViewExprSet, op $card to $cardViewExprSet, op union to unionViewExprSet, op intersection to intersectionViewExprSet, op $intersect to $intersectViewExprSet, op _\_ to _\ViewExprSet_, op $diff to $diffViewExprSet)){ViewExp} . pr (SET * (op _`,_ to _._)){ParameterDecl} . sort ModuleInfo . op <_;_;_;_;_;_;_;_> : ModuleName Default{Term} Module Module Module OpDeclSet Set{ModuleName} Set{ViewExp} -> ModuleInfo [ctor format (nig o g n+++io g nio g nio g nio g nio g nio g nio n---ig o)] . op <_;_;_;_;_;_;_;_> : ModuleName Module Module Module Module OpDeclSet Set{ModuleName} Set{ViewExp} -> ModuleInfo [ctor format (nig ur! g n+++io g nio g nio g nio g nio g nio g nio n---ig o)] . *** - Modules can be introduced by the user or can be generated internally. *** When introduced by the user the 2nd arg. keeps the term representation *** of the module as given, so that it can be recompiled later. If the *** module is generated internally as the result of the evaluation of a *** module expression, then this second arg. will be null, the default *** term value. The user can also enter modules with the procModule *** function, providing then the metarepresentation of a module, which *** is directly stored in the database as the 2nd arg. of one of these *** ModuleInfo units of the second kind. This is useful for the ITP for *** example, where the interaction with the database takes place at the *** metalevel and the modules given by the "user" are already at the *** metalevel but still wants the same treatment. *** - The sixth arg. stores the variables (corresponding ops.) in the top *** module. sort ViewInfo . op <_;_;_;_;_> : ViewExp Default{Term} View Set{ModuleName} Set{ViewExp} -> ViewInfo [ctor format (nig o g n+++io g nio g nio g nio n---ig o)] . op <_;_;_;_;_> : ViewExp View View Set{ModuleName} Set{ViewExp} -> ViewInfo [ctor format (nig o g n+++io g nio g nio g nio n---ig o)] . endfm view ModuleInfo from TRIV to INFO is sort Elt to ModuleInfo . endv view ViewInfo from TRIV to INFO is sort Elt to ViewInfo . endv fmod DATABASE-DECLS is pr (SET * (op _`,_ to __, op empty to emptyInfoSet)){ModuleInfo} . pr (SET * (op _`,_ to __, op empty to emptyInfoSet)){ViewInfo} . sort Database . op db : Set{ModuleInfo} *** module info tuples Set{ModuleName} *** names of the modules in the database Set{ViewInfo} *** view info tuples Set{ViewExp} *** names of the views in the db Set{ModuleName} *** modules with set protect on (by default empty) Set{ModuleName} *** modules with set extend on (by default empty) Set{ModuleName} *** modules with set include on (by default empty) QidList -> Database [ctor format (nib i++o)] . ops getDefPrs getDefExs getDefIncs : Database -> Set{ModuleName} . eq getDefPrs( db(MIS:Set{ModuleInfo}, MNS:Set{ModuleName}, VIS:Set{ViewInfo}, VES:Set{ViewExp}, MNS':Set{ModuleName}, MNS'':Set{ModuleName}, MNS3:Set{ModuleName}, QIL:QidList)) = MNS':Set{ModuleName} . eq getDefExs( db(MIS:Set{ModuleInfo}, MNS:Set{ModuleName}, VIS:Set{ViewInfo}, VES:Set{ViewExp}, MNS':Set{ModuleName}, MNS'':Set{ModuleName}, MNS3:Set{ModuleName}, QIL:QidList)) = MNS'':Set{ModuleName} . eq getDefIncs( db(MIS:Set{ModuleInfo}, MNS:Set{ModuleName}, VIS:Set{ViewInfo}, VES:Set{ViewExp}, MNS':Set{ModuleName}, MNS'':Set{ModuleName}, MNS3:Set{ModuleName}, QIL:QidList)) = MNS3:Set{ModuleName} . endfm view Database from TRIV to DATABASE-DECLS is sort Elt to Database . endv view ModuleExpression from TRIV to META-MODULE is sort Elt to ModuleExpression . endv fmod DATABASE is pr (2TUPLE * (op `(_`,_`) to <_;_>, op p1_ to database, op p2_ to modExp)) {Database, ModuleExpression} . pr PRE-VIEW . pr UNIT . pr VIEW-EXPR-TO-QID . op evalModule : Module OpDeclSet Database -> Database . *** its definition is in the module EVALUATION op procModule : Qid Database -> Database . op procView : Qid Database -> Database . *** their definitions are in the modules UNIT-PROCESSING and VIEW-PROCESSING op evalModExp : ModuleExpression Database -> Tuple{Database, ModuleExpression} . *** its definition is in the module MOD-EXPR-EVAL vars QI X Y F : Qid . vars QIL QIL' : QidList . vars VE VE' VE'' : ViewExp . vars VES VES' VES'' VES3 : Set{ViewExp} . vars MIS MIS' : Set{ModuleInfo} . var VIS : Set{ViewInfo} . vars MNS MNS' MNS'' MNS3 MNS4 MNS5 MNS6 : Set{ModuleName} . vars PL PL' : ParameterList . vars PDS PDS' PDS'' : Set{ParameterDecl} . var PDL : ParameterDeclList . var PD : ParameterDecl . vars ME ME' : ModuleExpression . vars VI VI' : View . var VMAPS : Set{ViewMap} . var PVMAPS : Set{PreViewMap} . vars PU PU' U U' U'' U3 U4 : Module . var M : Module . var DB : Database . vars IL IL' : ImportList . var VIf : ViewInfo . var UIf : ModuleInfo . vars OPDS VDS VDS' : OpDeclSet . var PV : PreView . vars T T' : Term . var DT : Default{Term} . var NL : IntList . var TyL : TypeList . var Ty : Type . var AtS : AttrSet . var B : Bool . var I : Import . var MN MN' : ModuleName . ops dincluded : ModuleExpression ImportList -> Bool . eq dincluded(ME, IL (protecting ME .) IL') = true . eq dincluded(ME, IL (extending ME .) IL') = true . eq dincluded(ME, IL (including ME .) IL') = true . eq dincluded(ME, IL) = false [owise] . ops included includedAux : ModuleExpression ImportList Database -> Bool . eq included(ME, IL (protecting ME .) IL', DB) = true . eq included(ME, IL (extending ME .) IL', DB) = true . eq included(ME, IL (including ME .) IL', DB) = true . eq included(ME, nil, DB) = false . eq included(ME, IL, DB) = includedAux(ME, IL, DB) [owise] . eq includedAux(ME, I IL, DB) = included(ME, getImports(getTopModule(moduleName(I), DB)), DB) or-else includedAux(ME, IL, DB) . eq includedAux(ME, nil, DB) = false . op defImports : Module Database -> ImportList . op defImports : ImportList ImportList Set{ModuleName} Set{ModuleName} Set{ModuleName} -> ImportList . eq defImports(M, DB) = if theory(M) then nil else defImports(getImports(M), nil, getDefPrs(DB), getDefExs(DB), getDefIncs(DB)) fi . eq defImports(IL, IL', MN . MNS, MNS', MNS'') = if dincluded(MN, IL IL') then defImports(IL, IL', MNS, MNS', MNS'') else defImports(IL, IL' (protecting MN .), MNS, MNS', MNS'') fi . eq defImports(IL, IL', MNS, MN . MNS', MNS'') = if dincluded(MN, IL IL') then defImports(IL, IL', MNS, MNS', MNS'') else defImports(IL, IL' (extending MN .), MNS, MNS', MNS'') fi . eq defImports(IL, IL', MNS, MNS', MN . MNS'') = if dincluded(MN, IL IL') then defImports(IL, IL', MNS, MNS', MNS'') else defImports(IL, IL' (including MN .), MNS, MNS', MNS'') fi . eq defImports(IL, IL', emptyModuleNameSet, emptyModuleNameSet, emptyModuleNameSet) = IL' . *** The constant \texttt{emptyDatabase} denotes the empty database, and there *** are predicates \texttt{viewInDatabase} and \texttt{unitInDb} to check, *** respectively, whether a view and a unit are in a database or not. op emptyDatabase : -> Database . eq emptyDatabase = db(emptyInfoSet, emptyModuleNameSet, emptyInfoSet, emptyViewExpSet, 'BOOL, emptyModuleNameSet, emptyModuleNameSet, nil) . op unitInDb : ModuleName Database -> Bool . eq unitInDb(MN, db(MIS, MNS, VIS, VES, MNS', MNS'', MNS3, QIL)) = MN inModuleNameSet MNS . op viewInDb : ViewExp Database -> Bool . eq viewInDb(VE, db(MIS, MNS, VIS, VES, MNS', MNS'', MNS3, QIL)) = VE inViewExpSet VES . op includeBOOL : Database -> Bool . eq includeBOOL(db(MIS, MNS, VIS, VES, MNS', MNS'', MNS3, QIL)) = 'BOOL inModuleNameSet MNS' . *** If a module, theory, or view is being redefined, that is, if there was *** already in the database a module, theory, or view with the same name, *** then all the units and/or views depending on it are removed using the *** functions \texttt{delModules} and \texttt{delViews}. Removing a view *** or a unit from the database means removing its info cell from the set of *** cells in the database. Those entered by the user are not completely *** removed, their term form is saved so that it can be recompiled later. op delModules : Set{ModuleName} Database -> Database . op delViews : Set{ViewExp} Database -> Database . eq delModules((MN . MNS), db(< MN ; T ; U ; U' ; U'' ; VDS ; MNS' ; VES > MIS, MN . MNS'', VIS, VES', MNS3, MNS4, MNS5, QIL)) = delModules((MNS . MNS'), delViews(VES, db(< MN ; T ; noModule ; noModule ; noModule ; VDS ; emptyModuleNameSet ; emptyViewExpSet > MIS, MN . MNS'', VIS, VES', MNS3, MNS4, MNS5, QIL))) . eq delModules((MN . MNS), db(< MN ; U ; U' ; U'' ; U3 ; VDS ; MNS' ; VES > MIS, MN . MNS'', VIS, VES', MNS3, MNS4, MNS5, QIL)) = delModules((MNS . MNS'), delViews(VES, db(< MN ; U ; noModule ; noModule ; noModule ; VDS ; emptyModuleNameSet ; emptyViewExpSet > MIS, MN . MNS'', VIS, VES', MNS3, MNS4, MNS5, QIL))) . eq delModules((MN . MNS), db(< MN ; null ; U ; U' ; U'' ; VDS ; MNS' ; VES > MIS, MN . MNS'', VIS, VES', MNS3, MNS4, MNS5, QIL)) = delModules((MNS . MNS'), delViews(VES, db(MIS, MNS'', VIS, VES', MNS3, MNS4, MNS5, QIL))) . eq delModules(emptyModuleNameSet, DB) = DB . eq delModules((MN . MNS), DB) = delModules(MNS, DB) [owise] . eq delViews(VE # VES, db(MIS, MNS, < VE ; T ; VI ; MNS' ; VES' > VIS, VE # VES'', MNS'', MNS3, MNS4, QIL)) = delViews(VES # VES', delModules(MNS', db(MIS, MNS, < VE ; T ; null ; emptyModuleNameSet ; emptyViewExpSet > VIS, VE # VES'', MNS'', MNS3, MNS4, QIL))) . eq delViews(VE # VES, db(MIS, MNS, < VE ; (null).Default{Term} ; VI ; MNS' ; VES' > VIS, VE # VES'', MNS'', MNS3, MNS4, QIL)) = delViews(VES # VES', delModules(MNS', db(MIS, MNS, VIS, VES'', MNS'', MNS3, MNS4, QIL))) . eq delViews(VE # VES, db(MIS, MNS, < VE ; VI ; VI' ; MNS' ; VES' > VIS, VE # VES'', MNS'', MNS3, MNS4, QIL)) = delViews(VES # VES', delModules(MNS', db(MIS, MNS, < VE ; VI ; null ; emptyModuleNameSet ; emptyViewExpSet > VIS, VE # VES'', MNS'', MNS3, MNS4, QIL))) . eq delViews(emptyViewExpSet, DB) = DB . eq delViews(VE # VES, DB) = delViews(VES, DB) [owise] . *** The \texttt{warning} function allows us to place messages (warning, error, *** or any other kind of messages) in the last argument of the database *** constructor. These messages are given in the form of quoted identifier *** lists,