1 /*
2
3 This file is part of the Maude 2 interpreter.
4
5 Copyright 1997-2003 SRI International, Menlo Park, CA 94025, USA.
6
7 This program is free software; you can redistribute it and/or modify
8 it under the terms of the GNU General Public License as published by
9 the Free Software Foundation; either version 2 of the License, or
10 (at your option) any later version.
11
12 This program is distributed in the hope that it will be useful,
13 but WITHOUT ANY WARRANTY; without even the implied warranty of
14 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 GNU General Public License for more details.
16
17 You should have received a copy of the GNU General Public License
18 along with this program; if not, write to the Free Software
19 Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307, USA.
20
21 */
22
23 //
24 // Class for modules which can import and be imported.
25 //
26 #ifndef _importModule_hh_
27 #define _importModule_hh_
28 #include <set>
29 #include <map>
30 #include "mixfixModule.hh"
31 #include "entity.hh"
32 #include "fileTable.hh"
33
34 class ImportModule
35 : public MixfixModule,
36 public Entity,
37 public Entity::User
38 {
39 NO_COPYING(ImportModule);
40
41 public:
42 enum ImportMode
43 {
44 PROTECTING,
45 EXTENDING,
46 INCLUDING
47 };
48
49 enum Origin
50 {
51 TEXT,
52 SUMMATION,
53 RENAMING,
54 PARAMETER,
55 INSTANTIATION,
56 VIEW_LOCAL
57 };
58
59 ImportModule(int name, ModuleType moduleType, Origin origin, Entity::User* parent);
60 ~ImportModule();
61
62 void addImport(ImportModule* importedModule,
63 ImportMode mode,
64 LineNumber lineNumber);
65 void addParameter(const Token parameterName,
66 ImportModule* parameterTheory);
67 void closeSortSet();
68 void closeSignature();
69 void deepSelfDestruct();
70 void importSorts();
71 void importOps();
72 void fixUpImportedOps();
73 void importStatements();
74 void resetImports();
75
76 void localStatementsComplete();
77 void protect();
78 bool unprotect();
79
80 Origin getOrigin() const;
81 int getNrParameters() const;
82 bool parametersBound() const;
83 ImportModule* getParameterTheory(int index) const;
84 int getParameterName(int index) const;
85 int getNrImportedSorts() const;
86 int getNrUserSorts() const;
87 int getNrImportedSubsorts(int sortIndex) const;
88 int getNrImportedSymbols() const;
89 int getNrImportedPolymorphs() const;
90 int getNrUserSymbols() const;
91 int getNrImportedDeclarations(int symbolIndex) const;
92 int getNrUserDeclarations(int symbolIndex) const;
93 int getNrOriginalMembershipAxioms() const;
94 int getNrOriginalEquations() const;
95 int getNrOriginalRules() const;
96 const set<int>& getLabels() const;
97 ImportModule* makeRenamedCopy(int name, Renaming* canonical, ModuleCache* moduleCache);
98 ImportModule* makeParameterCopy(int moduleName, int parameterName, ModuleCache* moduleCache);
99 ImportModule* makeInstantiation(int moduleName,
100 const Vector<View*>& arguments,
101 const Vector<int>& parameterArgs,
102 ModuleCache* moduleCache);
103 int findParameterIndex(int name) const;
104 bool moduleDeclared(Sort* sort) const;
105 bool moduleDeclared(Symbol* symbol) const;
106 bool moduleDeclaredPolymorph(int index) const;
107 bool parameterDeclared(Sort* sort) const;
108 bool parameterDeclared(Symbol* symbol) const;
109 bool parameterDeclaredPolymorph(int index) const;
110
111 private:
112 enum Phase
113 {
114 UNVISITED,
115 SORTS_IMPORTED,
116 OPS_IMPORTED,
117 OPS_FIXED_UP,
118 STATEMENTS_IMPORTED,
119 DOOMED
120 };
121
122 typedef map<int,int> ParameterMap;
123 typedef set<int> ParameterSet;
124
125 static Sort* localSort(ImportModule* copy, Renaming* renaming, const Sort* sort);
126 static Sort* localSort2(ImportModule* copy, Renaming* renaming, const Sort* sort);
127
128 static void deepCopyCondition(ImportTranslation* importTranslation,
129 const Vector<ConditionFragment*>& original,
130 Vector<ConditionFragment*>& copy);
131
132 static int instantiateSortName(int sortId,
133 const ParameterMap& parameterMap,
134 const ParameterSet& extraParameterSet);
135
136 static Renaming* instantiateRenaming(const Renaming* original,
137 const ParameterMap& parameterMap,
138 const ParameterSet& extraParameterSet);
139
140 ImportModule* instantiateBoundParameters(const Vector<View*>& arguments,
141 const Vector<int>& parameterArgs,
142 ModuleCache* moduleCache);
143
144 void regretToInform(Entity* doomedEntity);
145 void donateSorts(ImportModule* importer);
146 void donateSorts2(ImportModule* copy, Renaming* renaming = 0);
147 void donateOps(ImportModule* importer);
148 void donateOps2(ImportModule* copy, Renaming* renaming = 0);
149 void fixUpDonatedOps(ImportModule* importer);
150 void fixUpDonatedOps2(ImportModule* copy, Renaming* renaming = 0);
151 void donateStatements(ImportModule* importer);
152 void donateStatements2(ImportModule* importer, ImportTranslation& importTranslation);
153 void resetImportPhase();
154 void finishCopy(ImportModule* copy, Renaming* canonical);
155
156 void copyMetadata(ImportModule* importer,
157 ImportTranslation& importTranslation,
158 ItemType itemType,
159 PreEquation* original,
160 PreEquation* copy);
161
162 ConnectedComponent* translateComponent(const Renaming* renaming, const ConnectedComponent* component) const;
163
164 void addOpMappingsFromView(Renaming* canonical,
165 const ImportModule* parameterCopyOfTheory,
166 const View* view) const;
167 //
168 // Because makeInstantiation() is such complex procedure we split out 5 major
169 // subtasks.
170 //
171 void handleInstantiationByParameter(ImportModule* copy,
172 Renaming* canonical,
173 ParameterMap& parameterMap,
174 const Vector<View*>& arguments,
175 const Vector<int>& parameterArgs,
176 ModuleCache* moduleCache) const;
177
178 void handleInstantiationByTheoryView(ImportModule* copy,
179 Renaming* canonical,
180 ParameterMap& parameterMap,
181 ParameterSet& extraParameterSet,
182 const Vector<View*>& arguments,
183 ModuleCache* moduleCache) const;
184
185 void handleInstantiationByModuleView(ImportModule* copy,
186 Renaming* canonical,
187 ParameterMap& parameterMap,
188 const Vector<View*>& arguments) const;
189
190 void handleParameterizedSorts(Renaming* canonical,
191 const ParameterMap& parameterMap,
192 const ParameterSet& extraParameterSet) const;
193
194 void handleRegularImports(ImportModule* copy,
195 const Vector<View*>& arguments,
196 const Vector<int>& parameterArgs,
197 ModuleCache* moduleCache) const;
198
199 const Origin origin;
200 Phase importPhase;
201 //
202 // These are the theories and modules we directly import.
203 //
204 // 0,..., parameterNames.size() - 1 parameters
205 // parameterNames.size(),..., importedModules.size() - 1 regular imports
206 //
207 Vector<int> parameterNames;
208 Vector<ImportModule*> importedModules;
209 //
210 // Because for sorts, symbols, and polymorphs, stuff from parameter
211 // theories is inserted first we can keep track of what came from
212 // theories in order to stop it from being renamed. For modules
213 // without parameters these will be set to 0.
214 //
215 int nrSortsFromParameters;
216 int nrSymbolsFromParameters;
217 int nrPolymorphsFromParameters;
218 //
219 // If we are a renaming, parameter copy or instantiation of another
220 // module we need to store this info.
221 //
222 Renaming* canonicalRenaming;
223 ImportModule* baseModule;
224 //
225 // If we are are a instantiation, we keep track of any views that we
226 // a user of and if we have bound parameters, we also keep track
227 // track of the parameter arguments our base module was instantiated
228 // with so we can build a new instantiation when our bound
229 // parameters are instantiated.
230 //
231 Vector<View*> viewArgs;
232 Vector<int> paramArgs;
233 //
234 // These data structures are only filled out for theories and record
235 // the indices of any sorts and operators that were declared in an
236 // imported module and are therefore not eligible to be mapped by a
237 // view.
238 //
239 NatSet sortDeclaredInModule;
240 NatSet opDeclaredInModule;
241 NatSet polymorphDeclaredInModule;
242 //
243 // Need to keep track of what parts of MixfixModule actually belong
244 // to us (and need to be donated to our importers) and what parts
245 // we imported or otherwise generated.
246 //
247 // For sorts, symbols and op declarations, imports come first,
248 // then locals, then generated.
249 //
250 // For subsorts, imported subsort (relations) come first, then locals.
251 // The are no generated subsort relations.
252 //
253 // For mbs, eqs, and rls, locals come first, then imports.
254 // The reason for this different order is to avoid imports unless
255 // we ace actually going to do some work in the module.
256 //
257 int nrUserSorts; // total number of user declared sorts
258 int nrImportedSorts; // how many of these were imported
259 Vector<int> nrImportedSubsorts; // for each sort, how many subsorts were imported
260
261 int nrUserSymbols; // total number of user symbols
262 int nrImportedSymbols; // how many of these were imported
263 //
264 // For each symbol:
265 //
266 Vector<int> nrUserDecls; // total number of user declarations
267 Vector<int> nrImportedDecls; // total number of imported user declarations
268
269 int nrImportedPolymorphs; // number of polymorphs that were imported
270 int nrOriginalMembershipAxioms;
271 int nrOriginalEquations;
272 int nrOriginalRules;
273
274 set<int> labels;
275 int protectCount;
276 };
277
278 inline void
protect()279 ImportModule::protect()
280 {
281 ++protectCount;
282 }
283
284 inline ImportModule::Origin
getOrigin() const285 ImportModule::getOrigin() const
286 {
287 return origin;
288 }
289
290 inline int
getNrImportedSorts() const291 ImportModule::getNrImportedSorts() const
292 {
293 //
294 // Sorts with index < this value were imported.
295 //
296 return nrImportedSorts;
297 }
298
299 inline int
getNrParameters() const300 ImportModule::getNrParameters() const
301 {
302 return parameterNames.size();
303 }
304
305 inline ImportModule*
getParameterTheory(int index) const306 ImportModule::getParameterTheory(int index) const
307 {
308 Assert(index < getNrParameters(), "bad parameter index " << index << " in module " << (const MixfixModule*) this);
309 return importedModules[index]->baseModule;
310 }
311
312 inline int
getParameterName(int index) const313 ImportModule::getParameterName(int index) const
314 {
315 return parameterNames[index];
316 }
317
318 inline int
getNrUserSorts() const319 ImportModule::getNrUserSorts() const
320 {
321 //
322 // Sorts with index >= this value were generated (e.g. for kinds).
323 //
324 return nrUserSorts;
325 }
326
327 inline int
getNrImportedSubsorts(int sortIndex) const328 ImportModule::getNrImportedSubsorts(int sortIndex) const
329 {
330 //
331 // Subsorts with index < this value were imported.
332 //
333 return (sortIndex < nrImportedSorts) ? nrImportedSubsorts[sortIndex] : 0;
334 }
335
336 inline int
getNrImportedSymbols() const337 ImportModule::getNrImportedSymbols() const
338 {
339 //
340 // Symbols with index < this value were imported.
341 //
342 return nrImportedSymbols;
343 }
344
345 inline int
getNrImportedPolymorphs() const346 ImportModule::getNrImportedPolymorphs() const
347 {
348 //
349 // Symbols with index < this value were imported.
350 //
351 return nrImportedPolymorphs;
352 }
353
354 inline int
getNrUserSymbols() const355 ImportModule::getNrUserSymbols() const
356 {
357 //
358 // Symbols with index >= this value were generated (e.g. for polymorph instantiation).
359 //
360 return nrUserSymbols;
361 }
362
363 inline int
getNrImportedDeclarations(int symbolIndex) const364 ImportModule::getNrImportedDeclarations(int symbolIndex) const
365 {
366 //
367 // Declarations with index < this value were imported.
368 //
369 return (symbolIndex >= nrImportedSymbols) ? 0 : nrImportedDecls[symbolIndex];
370 }
371
372 inline int
getNrUserDeclarations(int symbolIndex) const373 ImportModule::getNrUserDeclarations(int symbolIndex) const
374 {
375 //
376 // Declarations with index >= this value were generated (e.g. for comm completion).
377 //
378 return nrUserDecls[symbolIndex];
379 }
380
381 inline int
getNrOriginalMembershipAxioms() const382 ImportModule::getNrOriginalMembershipAxioms() const
383 {
384 //
385 // Membership axioms with index >= this value were imported.
386 //
387 return nrOriginalMembershipAxioms;
388 }
389
390 inline int
getNrOriginalEquations() const391 ImportModule::getNrOriginalEquations() const
392 {
393 //
394 // Equations with index >= this value were imported.
395 //
396 return nrOriginalEquations;
397 }
398
399 inline int
getNrOriginalRules() const400 ImportModule::getNrOriginalRules() const
401 {
402 //
403 // Rules with index >= this value were imported.
404 //
405 return nrOriginalRules;
406 }
407
408 inline const set<int>&
getLabels() const409 ImportModule::getLabels() const
410 {
411 return labels;
412 }
413
414 inline bool
moduleDeclared(Sort * sort) const415 ImportModule::moduleDeclared(Sort* sort) const
416 {
417 Assert(sort->getModule() == this, "wrong module");
418 return sortDeclaredInModule.contains(sort->getIndexWithinModule());
419 }
420
421 inline bool
moduleDeclared(Symbol * symbol) const422 ImportModule::moduleDeclared(Symbol* symbol) const
423 {
424 Assert(symbol->getModule() == this, "wrong module");
425 return opDeclaredInModule.contains(symbol->getIndexWithinModule());
426 }
427
428 inline bool
moduleDeclaredPolymorph(int index) const429 ImportModule::moduleDeclaredPolymorph(int index) const
430 {
431 return polymorphDeclaredInModule.contains(index);
432 }
433
434 inline bool
parameterDeclared(Sort * sort) const435 ImportModule::parameterDeclared(Sort* sort) const
436 {
437 Assert(sort->getModule() == this, "wrong module");
438 return sort->getIndexWithinModule() < nrSortsFromParameters;
439 }
440
441 inline bool
parameterDeclared(Symbol * symbol) const442 ImportModule::parameterDeclared(Symbol* symbol) const
443 {
444 Assert(symbol->getModule() == this, "wrong module");
445 return symbol->getIndexWithinModule() < nrSymbolsFromParameters;
446 }
447
448 inline bool
parameterDeclaredPolymorph(int index) const449 ImportModule::parameterDeclaredPolymorph(int index) const
450 {
451 return index < nrPolymorphsFromParameters;
452 }
453
454 #ifndef NO_ASSERT
455 inline ostream&
operator <<(ostream & s,const ImportModule * m)456 operator<<(ostream& s, const ImportModule* m)
457 {
458 //
459 // Needed to avoid ambiguity.
460 //
461 s << static_cast<const MixfixModule*>(m);
462 return s;
463 }
464 #endif
465
466 #endif
467