Module templates serve as a slightly more flexible data-structure than the ones provided in the prelude for expressing syntactic theories.
First, we'll need a way to generate variables at the object level because writing all our syntax at the meta-level can be a pain. Additionally, we'll need a way to have "structured" sort names and operator names. For this, a few constructors are provided.
var<X>, whereXis some sort, will create an object-level variable of the given sort by first creating a meta-level variable and then downing it.
fmod STRUCTURED-NAME is
extending META-LEVEL .
vars I I' : Import . vars IL IL' : ImportList . vars S S' : Sort . var SS : SortSet . var SSDS : SubsortDeclSet .
vars H H' : Header . vars Q Q' : Qid . vars A A' : Attr . var AS : AttrSet . var SU : Substitution .
vars OP OP' : OpDecl . var OPDS : OpDeclSet . vars MB MB' : MembAx . var MAS : MembAxSet .
vars EQ EQ' : Equation . var EQS : EquationSet . vars RL RL' : Rule . var RLS : RuleSet .
var TYPE : Type . vars NeTL NeTL' : NeTypeList . var TL : TypeList . vars COND COND' : Condition . vars EQC EQC' : EqCondition .
vars TERM TERM' : Term . var TERML : TermList . vars NeTERML NeTERML' : NeTermList . var VAR : Variable . var CONST : Constant . var N : Nat .
op _<_> : Qid TypeList -> Qid [ctor prec 23] .
op _{_} : Sort TypeList -> Sort [ctor prec 23] .
op _@_ : Sort Sort -> Sort [ctor prec 23] .
op _? : Sort -> Sort [ctor prec 23] .
op _==>_ : Sort Sort -> Sort [ctor prec 25] .
op _/\_ : Header Header -> Header [ctor prec 25] .
op const : Qid Sort -> Constant [ctor] .
op var : Qid Sort -> Variable [ctor] .
---------------------------------------------
op downQidError? : -> [Qid] .
op downSubstitutionError? : -> [Substitution] .
op downImportListError? : -> [ImportList] .
op downSortsError? : -> [SortSet] .
op downSubsortsError? : -> [SubsortDeclSet] .
op downAttrSetError? : -> [AttrSet] .
op downOpSetError? : -> [OpDeclSet] .
op downMembAxSetError? : -> [MembAxSet] .
op downEqSetError? : -> [EquationSet] .
op downRuleSetError? : -> [RuleSet] .
------------------------------------------
op var<Qid> : Qid -> Qid .
op var<Substitution> : Qid -> Substitution .
op var<ImportList> : Qid -> ImportList .
op var<Sort> : Qid -> Sort .
op var<SortSet> : Qid -> SortSet .
op var<SubsortDeclSet> : Qid -> SubsortDeclSet .
op var<AttrSet> : Qid -> AttrSet .
op var<OpDeclSet> : Qid -> OpDeclSet .
op var<MembAxSet> : Qid -> MembAxSet .
op var<EquationSet> : Qid -> EquationSet .
op var<RuleSet> : Qid -> RuleSet .
-----------------------------------------
ceq var<Qid> (Q) = Q' if Q' := downTerm(qid(string(Q) + ":Qid"), downQidError?) .
ceq var<Substitution> (Q) = SU if SU := downTerm(qid(string(Q) + ":Substitution"), downSubstitutionError?) .
ceq var<ImportList> (Q) = IL if IL := downTerm(qid(string(Q) + ":ImportList"), downImportListError?) .
ceq var<Sort> (Q) = S if S := downTerm(qid(string(Q) + ":Sort"), downSortsError?) .
ceq var<SortSet> (Q) = SS if SS := downTerm(qid(string(Q) + ":SortSet"), downSortsError?) .
ceq var<SubsortDeclSet> (Q) = SSDS if SSDS := downTerm(qid(string(Q) + ":SubsortDeclSet"), downSubsortsError?) .
ceq var<AttrSet> (Q) = AS if AS := downTerm(qid(string(Q) + ":AttrSet"), downAttrSetError?) .
ceq var<OpDeclSet> (Q) = OPDS if OPDS := downTerm(qid(string(Q) + ":OpDeclSet"), downOpSetError?) .
ceq var<MembAxSet> (Q) = MAS if MAS := downTerm(qid(string(Q) + ":MembAxSet"), downMembAxSetError?) .
ceq var<EquationSet> (Q) = EQS if EQS := downTerm(qid(string(Q) + ":EquationSet"), downEqSetError?) .
ceq var<RuleSet> (Q) = RLS if RLS := downTerm(qid(string(Q) + ":RuleSet"), downRuleSetError?) .
It's useful when building universal constructions to generate the same structure, but with incremented variable names.
primewill add a prime'to every variable in a given term.#primeis the meta-level version, which does the same over aTerm.
op prime : Sort -> Sort .
op prime : Nat Sort -> Sort .
-----------------------------
eq prime(S) = prime(1, S) .
ceq prime(N, S) = S' if S' := downTerm(#prime(N, upTerm(S)), downSortsError?) .
op #prime : Nat TermList -> TermList .
------------------------------------------
eq #prime(N, VAR) = qid(string(getName(VAR)) + #primes(N) + ":" + string(getType(VAR))) .
eq #prime(N, CONST) = CONST .
eq #prime(N, Q[NeTERML]) = Q[#prime(N, NeTERML)] .
eq #prime(N, (NeTERML , NeTERML')) = #prime(N, NeTERML) , #prime(N, NeTERML') .
op #primes : Nat -> String .
----------------------------
eq #primes(0) = "" .
eq #primes(s(N)) = "'" + #primes(N) .
We'll need the ability to get the free variables of some specific sorts.
#fv<Sort>is a meta-level operation which gets all the variables of sortSortfrom aTerm.
op #fv<Sort> : TermList -> SortSet .
------------------------------------
eq #fv<Sort>(VAR) = if getType(VAR) == 'Sort then var<Sort>(getName(VAR)) else none fi .
eq #fv<Sort>(CONST) = none .
eq #fv<Sort>(Q[NeTERML]) = #fv<Sort>(Q) ; #fv<Sort>(NeTERML) .
eq #fv<Sort>((NeTERML , NeTERML')) = #fv<Sort>(NeTERML) ; #fv<Sort>(NeTERML') .
eq #fv<Sort>(Q) = none [owise] .
We'll also need ways to "resolve" these names into proper Maude names, so that we can do execution in Maude with the results. Here we provide the "base" resolution, as well as lifting it over the various meta-level data.
resolveNamesprovides the reduction of structured names to unstructured Core Maude names (a single quoted identifier).
TODO: resolveNames should be defined over just a few primitives (the ones that
we have structured names for), and #resolveNames should be a META-LEVEL
version which descends to those points in the term and then calls the object
level version. This should fix the preregularity issue with this as well.
op resolveNames : Header -> Header .
------------------------------------
eq resolveNames(H) = H [owise] .
eq resolveNames(H /\ H') = qid(string(resolveNames(H)) + "/\\" + string(resolveNames(H'))) .
op #tl-string : TypeList -> String .
------------------------------------
eq #tl-string(nil) = "" .
eq #tl-string(S) = string(S) .
eq #tl-string(NeTL NeTL') = #tl-string(NeTL) + ";" + #tl-string(NeTL') .
op resolveNames : TypeList -> TypeList .
----------------------------------------
eq resolveNames((nil).TypeList) = nil .
eq resolveNames(NeTL NeTL') = resolveNames(NeTL) resolveNames(NeTL') .
op resolveNames : Qid -> Qid .
------------------------------
eq resolveNames(Q < TL >) = qid(string(resolveNames(Q)) + "<" + #tl-string(resolveNames(TL)) + ">") .
eq resolveNames(Q) = Q [owise] .
op resolveNames : TermList -> TermList .
----------------------------------------
eq resolveNames(const(Q, S)) = qid(string(resolveNames(Q)) + "." + string(resolveNames(S))) .
eq resolveNames(var(Q, S)) = qid(string(resolveNames(Q)) + ":" + string(resolveNames(S))) .
eq resolveNames(Q[TERML]) = resolveNames(Q)[resolveNames(TERML)] .
eq resolveNames((NeTERML , NeTERML')) = resolveNames(NeTERML) , resolveNames(NeTERML') .
eq resolveNames(TERM) = TERM [owise] .
op resolveNames : SortSet -> SortSet .
--------------------------------------
eq resolveNames((none).SortSet) = none .
eq resolveNames(S { TL }) = qid(string(resolveNames(S)) + "{" + #tl-string(resolveNames(TL)) + "}") .
eq resolveNames(Q @ S) = qid(string(resolveNames(Q)) + "@" + string(resolveNames(S))) .
eq resolveNames(S ==> S') = qid(string(resolveNames(S)) + "==>" + string(resolveNames(S'))) .
eq resolveNames(S ?) = qid(string(resolveNames(S)) + "?") .
eq resolveNames(S ; S' ; SS) = resolveNames(S) ; resolveNames(S') ; resolveNames(SS) .
eq resolveNames(S) = S [owise] .
op resolveNames : AttrSet -> AttrSet .
--------------------------------------
eq resolveNames((none).AttrSet) = none .
eq resolveNames(id(TERM)) = id(resolveNames(TERM)) .
eq resolveNames(A A' AS) = resolveNames(A) resolveNames(A') resolveNames(AS) .
eq resolveNames(A) = A [owise] .
op resolveNames : SubsortDecl -> SubsortDecl .
----------------------------------------------
eq resolveNames(subsort S < S' .) = ( subsort resolveNames(S) < resolveNames(S') . ) .
op resolveNames : Condition -> Condition .
------------------------------------------
eq resolveNames((nil).Condition) = nil .
eq resolveNames(TERM : S) = resolveNames(TERM) : resolveNames(S) .
eq resolveNames(TERM = TERM') = resolveNames(TERM) = resolveNames(TERM') .
eq resolveNames(TERM := TERM') = resolveNames(TERM) := resolveNames(TERM') .
eq resolveNames(TERM => TERM') = resolveNames(TERM) => resolveNames(TERM') .
ceq resolveNames(COND /\ COND') = resolveNames(COND) /\ resolveNames(COND') if not (COND == nil or COND' == nil) .
op resolveNames : OpDecl -> OpDecl .
------------------------------------
eq resolveNames(op Q : TL -> TYPE [AS] .) = (op resolveNames(Q) : resolveNames(TL) -> resolveNames(TYPE) [resolveNames(AS)] .) .
op resolveNames : MembAxSet -> MembAxSet .
------------------------------------------
eq resolveNames( mb TERM : S [AS] .) = ( mb resolveNames(TERM) : resolveNames(S) [resolveNames(AS)] .) .
eq resolveNames(cmb TERM : S if EQC [AS] .) = (cmb resolveNames(TERM) : resolveNames(S) if resolveNames(EQC) [resolveNames(AS)] .) .
op resolveNames : EquationSet -> EquationSet .
----------------------------------------------
eq resolveNames( eq TERM = TERM' [AS] .) = ( eq resolveNames(TERM) = resolveNames(TERM') [resolveNames(AS)] .) .
eq resolveNames(ceq TERM = TERM' if EQC [AS] .) = (ceq resolveNames(TERM) = resolveNames(TERM') if resolveNames(EQC) [resolveNames(AS)] .) .
op resolveNames : RuleSet -> RuleSet .
--------------------------------------
eq resolveNames( rl TERM => TERM' [AS] .) = ( rl resolveNames(TERM) => resolveNames(TERM') [resolveNames(AS)] .) .
eq resolveNames(crl TERM => TERM' if COND [AS] .) = (crl resolveNames(TERM) => resolveNames(TERM') if resolveNames(COND) [resolveNames(AS)] .) .
endfm
Module declarations include all of the individual declarations defined in the
prelude, but extend them by adding a common supersort ModuleDecl, as well as a
common subsort for each declaration set NullDeclSet. Additionally, extra sorts
are added for the non-empty versions of each declaration (for preregularity).
load constrained-terms.maude
fmod MODULE-DECLARATION is
protecting STRUCTURED-NAME .
protecting CTERM-SET .
sorts ImportDecl ImportDeclSet .
--------------------------------
subsort ImportDecl < ImportDeclSet .
sorts SortPoset SortDecl SortDeclSet .
--------------------------------------
subsort SortSet < SortPoset .
subsort SortDecl < SortDeclSet .
sorts NeImportDeclSet NeSortDeclSet NeSubsortDeclSet NeOpDeclSet NeMembAxSet NeEquationSet NeRuleSet .
------------------------------------------------------------------------------------------------------
subsorts ImportDecl < NeImportDeclSet < ImportDeclSet .
subsorts SortDecl < NeSortDeclSet < SortDeclSet .
subsorts SubsortDecl < NeSubsortDeclSet < SubsortDeclSet .
subsorts OpDecl < NeOpDeclSet < OpDeclSet .
subsorts MembAx < NeMembAxSet < MembAxSet .
subsorts Equation < NeEquationSet < EquationSet .
subsorts Rule < NeRuleSet < RuleSet .
sorts ModuleDecl NeModuleDeclSet ModuleDeclSet NullDeclSet .
------------------------------------------------------------
subsorts ModuleDecl < NeModuleDeclSet < ModuleDeclSet .
subsorts ImportDecl SortDecl SubsortDecl OpDecl MembAx Equation Rule < ModuleDecl .
subsorts NullDeclSet < ImportDeclSet SortDeclSet SubsortDeclSet OpDeclSet MembAxSet EquationSet RuleSet < ModuleDeclSet .
subsorts NeImportDeclSet NeSortDeclSet NeSubsortDeclSet NeOpDeclSet NeMembAxSet NeEquationSet NeRuleSet < NeModuleDeclSet .
var Q : Qid . var ME : ModuleExpression .
vars I I' : Import . var IL : ImportList . vars ID : ImportDecl . var NeIDS : NeImportDeclSet . var IDS : ImportDeclSet .
vars S S' S'' : Sort . vars SS SS' : SortSet . var SPS : SortPoset .
var SU : Substitution . var SUBSTS : SubstitutionSet .
vars NeMDS NeMDS' : NeModuleDeclSet . vars MDS MDS' : ModuleDeclSet .
op __ : ImportDeclSet NeImportDeclSet -> NeImportDeclSet [ctor ditto] .
op __ : SortDeclSet NeSortDeclSet -> NeSortDeclSet [ctor ditto] .
op __ : SubsortDeclSet NeSubsortDeclSet -> NeSubsortDeclSet [ctor ditto] .
op __ : OpDeclSet NeOpDeclSet -> NeOpDeclSet [ctor ditto] .
op __ : MembAxSet NeMembAxSet -> NeMembAxSet [ctor ditto] .
op __ : EquationSet NeEquationSet -> NeEquationSet [ctor ditto] .
op __ : RuleSet NeRuleSet -> NeRuleSet [ctor ditto] .
--------------------------------------------------------------------------
op none : -> NullDeclSet [ctor] .
op __ : NullDeclSet NullDeclSet -> NullDeclSet [ctor ditto] .
-------------------------------------------------------------
op __ : ModuleDeclSet ModuleDeclSet -> ModuleDeclSet [ctor ditto] .
op __ : ModuleDeclSet NeModuleDeclSet -> NeModuleDeclSet [ctor ditto] .
-----------------------------------------------------------------------
eq NeMDS NeMDS = NeMDS .
Using the syntax of the prelude, imports and sort declarations are treated
specially. Here we add the notion of ImportDecl and SortDecl, so that they
can be treated uniformly with the rest of the declarations.
ops (pr_.) (ex_.) (in_.) : ModuleExpression -> ImportDecl .
op __ : ImportDeclSet ImportDeclSet -> ImportDeclSet [ctor ditto] .
-------------------------------------------------------------------
eq ( pr ME . ) ( ex ME . ) = ( ex ME . ) .
eq ( pr ME . ) ( in ME . ) = ( in ME . ) .
eq ( ex ME . ) ( in ME . ) = ( in ME . ) .
op importDecls : ImportList -> ImportDeclSet .
----------------------------------------------
eq importDecls(nil) = none .
eq importDecls(protecting ME .) = (pr ME .) .
eq importDecls(extending ME .) = (ex ME .) .
eq importDecls(including ME .) = (in ME .) .
eq importDecls(I I' IL) = importDecls(I) importDecls(I') importDecls(IL) .
op importList : ImportDeclSet -> ImportList .
---------------------------------------------
eq importList(none) = nil .
eq importList(pr ME .) = (protecting ME .) .
eq importList(ex ME .) = (extending ME .) .
eq importList(in ME .) = (including ME .) .
eq importList(ID NeIDS) = importList(ID) importList(NeIDS) .
op (sorts_.) : SortSet -> SortDecl [prec 60] .
op __ : SortDeclSet SortDeclSet -> SortDeclSet [ditto] .
--------------------------------------------------------
eq ( sorts none . ) = none .
eq ( sorts SS . ) ( sorts SS' . ) = ( sorts SS ; SS' . ) .
op _<_ : SortPoset SortPoset -> SortPoset [assoc id: none prec 122] .
op (subsorts_.) : SortPoset -> SubsortDeclSet .
-----------------------------------------------
eq ( subsorts SS . ) = none .
eq ( subsorts S < S' . ) = ( subsort S < S' . ) .
eq ( subsorts S < S' ; S'' ; SS' . )
= ( subsorts S < S' .
subsorts S < S'' .
subsorts S < SS' .
) .
eq ( subsorts S ; S' ; SS < S'' ; SS' . )
= ( subsorts S < S'' ; SS' .
subsorts S' < S'' ; SS' .
subsorts SS < S'' ; SS' .
) .
eq ( subsorts S ; SS < S' ; SS' < SPS . )
= ( subsorts S < S' ; SS' .
subsorts SS < S' ; SS' .
subsorts S' ; SS' < SPS .
) .
top-sort : ModuleDeclSet Sort -> [Sort]gives the top sort of a connected component with the given sort in it.connected-component : ModuleDeclSet ModuleDeclSet -> ModuleDeclSetwill complete the second module declaration set with all the sorts and subsorts in the intersection of the two connected components.tag-sorts : Qid ModuleDeclSet -> [ModuleDeclSet]will take a sort structure (aModuleDeclSetwhich only consists ofSortDeclandSubsortDecl) and produce a "tagged" version. For each sortXin the original sort structure it will produceX{Q}, forQthe suppliedQid.
op top-sort : ModuleDeclSet Sort -> [Sort] .
--------------------------------------------
eq top-sort( ( subsort S < S' . ) MDS , S ) = top-sort( MDS , S' ) .
eq top-sort( MDS , S ) = S [owise] .
op connected-component : ModuleDeclSet ModuleDeclSet -> [ModuleDeclSet] .
-------------------------------------------------------------------------
eq connected-component(MDS, MDS') = MDS' [owise] .
eq connected-component( ( sorts S ; S' ; SS . ) ( subsort S < S' . ) MDS
, ( sorts S ; SS' . ) MDS'
)
= connected-component( ( sorts S ; S' ; SS . ) MDS
, ( sorts S ; S' ; SS' . ) ( subsort S < S' . ) MDS'
) .
eq connected-component( ( sorts S ; S' ; SS . ) ( subsort S' < S . ) MDS
, ( sorts S ; SS' . ) MDS'
)
= connected-component( ( sorts S ; S' ; SS . ) MDS
, ( sorts S ; S' ; SS' . ) ( subsort S' < S . ) MDS'
) .
op tag-sorts : Qid ModuleDeclSet -> [ModuleDeclSet] .
-----------------------------------------------------
eq tag-sorts(Q, none) = none .
eq tag-sorts(Q, (NeMDS NeMDS')) = tag-sorts(Q, NeMDS) tag-sorts(Q, NeMDS') .
eq tag-sorts(Q, ( sorts S . )) = ( sorts S{Q} . ) .
eq tag-sorts(Q, ( subsort S < S' . )) = ( subsort S{Q} < S'{Q} . ) .
eq tag-sorts(Q, ( sorts S ; S' ; SS . )) = tag-sorts(Q, ( sorts S . ))
tag-sorts(Q, ( sorts S' . ))
tag-sorts(Q, ( sorts SS . )) .
_<<_ : ModuleDeclSet Substitution -> [ModuleDeclSet]lifts the substitution application operator_<<_overModuleDeclSet.match_with_ : ModuleDeclSet ModuleDeclSet -> [SubstitutionSet]gives all the ways that the firstModuleDeclSetmatches the second with variable extension.resolveNamesandfv<Sort>are simply the lifting ofresolveNamesandfv<Sort>ofSTRUCTURED-NAMEtoModuleDeclSet.
op error<ModuleDeclSet> : -> [ModuleDeclSet] .
op var<ModuleDeclSet> : Qid -> [ModuleDeclSet] .
------------------------------------------------
ceq var<ModuleDeclSet>(Q) = MDS if MDS := downTerm(qid(string(Q) + ":ModuleDeclSet"), error<ModuleDeclSet>) .
op _<<_ : ModuleDeclSet Substitution -> [ModuleDeclSet] .
---------------------------------------------------------
eq MDS << empty = (none).NullDeclSet .
eq (none).NullDeclSet << SU = none .
ceq NeMDS << SU = NeMDS' if NeMDS' := downTerm(upTerm(NeMDS) << SU, error<ModuleDeclSet>) .
op match_with_ : ModuleDeclSet ModuleDeclSet -> [SubstitutionSet] .
-------------------------------------------------------------------
eq match MDS with none = empty .
ceq match MDS with NeMDS = SUBSTS if NeMDS' := MDS ( sorts var<SortSet>('##SSCTX##) . ) var<ModuleDeclSet>('##MDSCTX##)
/\ SUBSTS := #subsumesWith(upModule('MODULE-DECLARATION, true), upTerm(NeMDS'), upTerm(NeMDS)) .
op resolveNames : ModuleDeclSet -> ModuleDeclSet .
--------------------------------------------------
eq resolveNames(IDS) = IDS .
eq resolveNames(( sorts SS . )) = ( sorts resolveNames(SS) . ) .
eq resolveNames((none).NullDeclSet) = none .
eq resolveNames(NeMDS NeMDS') = resolveNames(NeMDS) resolveNames(NeMDS') .
op fv<Sort> : ModuleDeclSet -> SortSet .
----------------------------------------
eq fv<Sort>(MDS) = #fv<Sort>(upTerm(MDS)) .
endfm
Module templates serve as more flexible module data-structures than what the prelude provides for modules. Every ModuleDeclSet is a ModuleTemplateSet.
The main functionality exported is:
_|_and_\_serve asModuleTemplateSetunion and difference, respectively.++ : ModuleTemplateSet -> ModuleDeclSetunions together the givenModuleTemplateSetinto a singleModuleDeclSet._<<_ : ModuleTemplateSet SubstitutionSet -> [ModuleTemplateSet]is lifted pointwise over both of its arguments.match_with_ : ModuleTemplateSet ModuleDeclSet -> [SubstitionSet]allows to specify a union or difference of source templates to match from.resolveNamesandfv<Sort>are lifted overModuleTemplateSet.
fmod MODULE-TEMPLATE-SET is
protecting MODULE-DECLARATION .
sorts NeModuleTemplateSet ModuleTemplateSet .
subsorts ModuleDeclSet < ModuleTemplateSet .
subsorts NeModuleDeclSet < NeModuleTemplateSet < ModuleTemplateSet .
vars NeMDS NeMDS' : NeModuleDeclSet . var MDS : ModuleDeclSet .
vars NeMTS NeMTS' NeMTS'' : NeModuleTemplateSet . var MTS : ModuleTemplateSet .
vars SU SU' SU'' : Substitution . var SUBSTS : SubstitutionSet .
op _|_ : ModuleTemplateSet ModuleTemplateSet -> ModuleTemplateSet [ctor assoc comm id: (none).NullDeclSet prec 73] .
op _|_ : ModuleTemplateSet NeModuleTemplateSet -> NeModuleTemplateSet [ctor ditto] .
------------------------------------------------------------------------------------
eq NeMTS | NeMTS = NeMTS .
op _\_ : ModuleTemplateSet ModuleTemplateSet -> ModuleTemplateSet [ctor right id: none prec 74] .
-------------------------------------------------------------------------------------------------
eq NeMTS \ (NeMTS | MTS) = none .
eq none \ NeMTS = none .
eq (NeMTS | NeMTS') \ NeMTS'' = (NeMTS \ NeMTS'') | (NeMTS' \ NeMTS'') .
eq (NeMTS \ NeMTS') \ NeMTS'' = NeMTS \ (NeMTS' | NeMTS'') .
op ++ : ModuleTemplateSet -> ModuleDeclSet .
--------------------------------------------
eq ++(none) = none .
eq ++(NeMDS) = NeMDS .
eq ++(NeMDS | NeMTS) = NeMDS ++(NeMTS) .
op error<ModuleTemplateSet> : -> [ModuleTemplateSet] .
op _<<_ : ModuleTemplateSet SubstitutionSet -> [ModuleTemplateSet] .
--------------------------------------------------------------------
eq MTS << empty = MTS .
eq MTS << (SU | SU' | SUBSTS) = (MTS << SU) | (MTS << SU') | (MTS << SUBSTS) .
eq (NeMTS | NeMTS') << SUBSTS = (NeMTS << SUBSTS) | (NeMTS' << SUBSTS) .
eq (NeMTS \ NeMTS') << SUBSTS = (NeMTS << SUBSTS) \ (NeMTS' << SUBSTS) .
op match_with_ : ModuleTemplateSet ModuleDeclSet -> [SubstitutionSet] .
-----------------------------------------------------------------------
eq match NeMTS | NeMTS' with MDS = (match NeMTS with MDS) | (match NeMTS' with MDS) .
ceq match NeMTS \ NeMTS' with MDS = SUBSTS if SUBSTS := not-instance-with?(NeMTS', MDS, match NeMTS with MDS) .
var B : [Bool] .
op {_in_|_} : Substitution SubstitutionSet [Bool] -> SubstitutionSet [strat(2 0)] .
-----------------------------------------------------------------------------------
eq { SU in empty | B } = empty .
eq { SU in SU' | B } = if downTerm(upTerm(B) << (upTerm(SU) <- upTerm(SU')), false) then SU' else empty fi .
eq { SU in (SU' | SU'' | SUBSTS) | B } = { SU in SU' | B } | { SU in SU'' | B } | { SU in SUBSTS | B } .
op empty? : SubstitutionSet -> Bool .
-------------------------------------
eq empty?(empty) = true .
eq empty?(SU | SUBSTS) = false .
op not-instance-with? : ModuleTemplateSet ModuleDeclSet SubstitutionSet -> SubstitutionSet .
--------------------------------------------------------------------------------------------
eq not-instance-with?(MTS, MDS, empty) = empty .
ceq not-instance-with?(MTS, MDS, SU) = if SUBSTS == empty then SU else empty fi if SUBSTS := match (MTS << SU) with MDS .
eq not-instance-with?(MTS, MDS, (SU | SU' | SUBSTS)) = not-instance-with?(MTS, MDS, SU) | not-instance-with?(MTS, MDS, SU') | not-instance-with?(MTS, MDS, SUBSTS) .
op resolveNames : ModuleTemplateSet -> ModuleTemplateSet .
----------------------------------------------------------
eq resolveNames(NeMTS | NeMTS') = resolveNames(NeMTS) | resolveNames(NeMTS') .
eq resolveNames(NeMTS \ NeMTS') = resolveNames(NeMTS) \ resolveNames(NeMTS') .
op fv<Sort> : ModuleTemplateSet -> SortSet .
--------------------------------------------
eq fv<Sort>(NeMTS | NeMTS') = fv<Sort>(NeMTS) ; fv<Sort>(NeMTS') .
eq fv<Sort>(NeMTS \ NeMTS') = fv<Sort>(NeMTS) ; fv<Sort>(NeMTS') .
endfm
To actually do execution in the modules generated by a module template, we need functions to convert between Module and ModuleTemplate.
asTemplate : Module -> ModuleTemplate,asTemplate : ModuleExpression -> ModuleTemplateandfromTemplate : ModuleTemplate -> Moduleprovide functions between the normal Maude modules and the module templates defined here._++_ : Module ModuleTemplateSet -> Moduleand_++_ : Module Module -> Moduleare the lifting of operator_++_inMODULE-TEMPLATE-DATAto work directly on Maude modules.resolveModule: ModuleTemplate -> ModuleTemplateresolves the structured names of a module into proper Core Maude names.
fmod MODULE-TEMPLATE is
protecting MODULE-TEMPLATE-SET .
protecting META-LEVEL .
var H : Header . var IL : ImportList . var SS : SortSet .
var IS : ImportDeclSet . var SSDS : SubsortDeclSet . var OPDS : OpDeclSet .
var MAS : MembAxSet . var EQS : EquationSet . var RLS : RuleSet . var NeRLS : NeRuleSet .
var ME : ModuleExpression . vars MOD MOD' : Module . var NeMTS : NeModuleTemplateSet .
op asTemplate : ModuleExpression -> [ModuleDeclSet] .
op asTemplate : Module -> [ModuleDeclSet] .
-------------------------------------------
eq asTemplate(ME) = asTemplate(upModule(ME, false)) .
eq asTemplate(fmod H is IL sorts SS . SSDS OPDS MAS EQS endfm) = (importDecls(IL) (sorts SS .) SSDS OPDS MAS EQS) .
eq asTemplate (mod H is IL sorts SS . SSDS OPDS MAS EQS RLS endm) = (importDecls(IL) (sorts SS .) SSDS OPDS MAS EQS RLS) .
op fromTemplate : Header ModuleDeclSet -> [Module] .
----------------------------------------------------
eq fromTemplate(H, (IS (sorts SS .) SSDS OPDS MAS EQS)) = (fmod H is importList(IS) sorts SS . SSDS OPDS MAS EQS endfm) .
eq fromTemplate(H, (IS (sorts SS .) SSDS OPDS MAS EQS NeRLS)) = (mod H is importList(IS) sorts SS . SSDS OPDS MAS EQS NeRLS endm) .
op _++_ : Module ModuleTemplateSet -> [Module] [right id: none prec 72] .
-------------------------------------------------------------------------
eq MOD ++ NeMTS = fromTemplate(getName(MOD), ++(NeMTS | asTemplate(MOD))) .
op _++_ : Module Module -> [Module] [assoc prec 73] .
-----------------------------------------------------
eq MOD ++ MOD' = MOD ++ asTemplate(MOD') .
op resolveNames : Module -> [Module] .
--------------------------------------
eq resolveNames(MOD) = fromTemplate(getName(MOD), resolveNames(asTemplate(MOD))) .
endfm