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 to hold interpreter state.
25 //
26 #ifndef _interpreter_hh_
27 #define _interpreter_hh_
28 #include <set>
29 #include "environment.hh"
30 #include "moduleDatabase.hh"
31 #include "moduleCache.hh"
32 #include "compiler.hh"
33 #include "viewDatabase.hh"
34
35 class Interpreter
36 : public Environment,
37 public ModuleDatabase,
38 public ModuleCache,
39 #ifdef COMPILER
40 public Compiler,
41 #endif
42 public ViewDatabase
43 {
44 NO_COPYING(Interpreter);
45
46 public:
47 enum SearchKind
48 {
49 SEARCH,
50 NARROW,
51 XG_NARROW,
52 SMT_SEARCH
53 };
54
55 enum Flags
56 {
57 //
58 // Show (information) flags.
59 //
60 SHOW_COMMAND = 0x1,
61 SHOW_STATS = 0x2,
62 SHOW_TIMING = 0x4,
63 SHOW_BREAKDOWN = 0x8,
64 //
65 // Loop mode flags.
66 //
67 SHOW_LOOP_STATS = 0x10,
68 SHOW_LOOP_TIMING = 0x20,
69 //
70 // Memoization flags.
71 //
72 AUTO_CLEAR_MEMO = 0x100,
73 //
74 // Profiler flags.
75 //
76 PROFILE = 0x200,
77 AUTO_CLEAR_PROFILE = 0x400,
78 //
79 // Debugger flags.
80 //
81 BREAK = 0x800,
82 //
83 // Tracer flags.
84 //
85 TRACE = 0x1000,
86 TRACE_CONDITION = 0x2000,
87 TRACE_WHOLE = 0x4000,
88 TRACE_SUBSTITUTION = 0x8000,
89 TRACE_SELECT = 0x10000,
90 TRACE_MB = 0x20000,
91 TRACE_EQ = 0x40000,
92 TRACE_RL = 0x80000,
93 TRACE_REWRITE = 0x100000,
94 TRACE_BODY = 0x200000,
95 TRACE_BUILTIN = 0x400000,
96 //
97 // Print attribute flags
98 //
99 PRINT_ATTRIBUTE = 0x800000,
100 PRINT_ATTRIBUTE_NEWLINE = 0x1000000,
101 /*
102 PRINT_ATTRIBUTE_MB = 0x2000000,
103 PRINT_ATTRIBUTE_EQ = 0x4000000,
104 PRINT_ATTRIBUTE_RL = 0x8000000,
105 */
106 //
107 // Counter flags.
108 //
109 AUTO_CLEAR_RULES = 0x40000000,
110 //
111 // Compiler flags.
112 //
113 COMPILE_COUNT = 0x80000000,
114 //
115 // Flag groups.
116 //
117 EXCEPTION_FLAGS = TRACE | BREAK | PROFILE | PRINT_ATTRIBUTE,
118
119 DEFAULT_FLAGS = SHOW_COMMAND | SHOW_STATS | SHOW_TIMING | SHOW_LOOP_TIMING |
120 COMPILE_COUNT |
121 TRACE_CONDITION | TRACE_SUBSTITUTION | TRACE_MB | TRACE_EQ | TRACE_RL | TRACE_REWRITE | TRACE_BODY | TRACE_BUILTIN |
122 AUTO_CLEAR_PROFILE | AUTO_CLEAR_RULES | PRINT_ATTRIBUTE_NEWLINE
123 };
124
125 enum PrintFlags
126 {
127 //
128 // General prettyprinter flags.
129 //
130 PRINT_GRAPH = 0x1, // print as a set of DAG nodes
131 PRINT_CONCEAL = 0x2, // respect concealed argument lists
132 PRINT_FORMAT = 0x4, // respect format attribute
133 PRINT_MIXFIX = 0x8, // mixfix notation
134 PRINT_WITH_PARENS = 0x10, // maximal parens
135 PRINT_COLOR = 0x20, // dag node coloring based on ctor/reduced status
136 //
137 // Prettyprinter flags for particular symbol types.
138 //
139 PRINT_WITH_ALIASES = 0x100, // for variables
140 PRINT_FLAT = 0x200, // for assoc symbols
141 PRINT_NUMBER = 0x400, // for nats & ints
142 PRINT_RAT = 0x800, // for rats
143
144 DEFAULT_PRINT_FLAGS = PRINT_FORMAT | PRINT_MIXFIX | PRINT_WITH_ALIASES |
145 PRINT_FLAT | PRINT_NUMBER | PRINT_RAT
146 };
147
148 Interpreter();
149 ~Interpreter();
150
151 void beginXmlLog(const char* fileName);
152 void endXmlLog();
153 MaudemlBuffer* getXmlBuffer() const;
154
155 void setFlag(Flags flag, bool polarity);
156 bool getFlag(Flags flag) const;
157 void setPrintFlag(PrintFlags flag, bool polarity);
158 bool getPrintFlag(PrintFlags flag) const;
159 int getPrintFlags() const;
160
161 SyntacticPreModule* getCurrentModule() const;
162 bool setCurrentModule(const Vector<Token>& moduleExpr, int start = 0);
163 void setCurrentModule(SyntacticPreModule* module);
164 void makeClean(int lineNumber);
165
166 View* getCurrentView() const;
167 bool setCurrentView(const Vector<Token>& viewExpr);
168 void setCurrentView(View* view);
169
170 void parse(const Vector<Token>& subject);
171 void reduce(const Vector<Token>& subject, bool debug);
172 void creduce(const Vector<Token>& subject);
173 void sreduce(const Vector<Token>& subject);
174 void rewrite(const Vector<Token>& subject, Int64 limit, bool debug);
175 void fRewrite(const Vector<Token>& subject, Int64 limit, Int64 gas, bool debug);
176 void eRewrite(const Vector<Token>& subject, Int64 limit, Int64 gas, bool debug);
177 void sRewrite(const Vector<Token>& subjectAndStrategy, Int64 limit, bool debug);
178 void cont(Int64 limit, bool debug);
179 void check(const Vector<Token>& subject);
180 //
181 // This is just a utility command for development.
182 //
183 void test(const Vector<Token>& subject);
184
185 void match(const Vector<Token>& bubble, bool withExtension, Int64 limit);
186 void unify(const Vector<Token>& bubble, Int64 limit);
187 void search(const Vector<Token>& bubble, Int64 limit, Int64 depth, SearchKind searchKind);
188 void getVariants(const Vector<Token>& bubble, Int64 limit, bool irredundant, bool debug);
189 void variantUnify(const Vector<Token>& bubble, Int64 limit, bool debug);
190 void smtSearch(const Vector<Token>& subject, int limit, int depth);
191
192 void showSearchPath(int stateNr);
193 void showSearchPathLabels(int stateNr);
194 void showSearchGraph();
195
196 void loop(const Vector<Token>& subject);
197 void contLoop(const Vector<Token>& input);
198
199 void addSelected(const Vector<Token>& opName);
200 void traceSelect(bool add);
201 void breakSelect(bool add);
202 void traceExclude(bool add);
203 void printConceal(bool add);
204
205 bool traceId(int id);
206 bool breakId(int id);
207 bool excludedModule(int id);
208 bool concealedSymbol(Symbol* symbol);
209
210 void showProfile() const;
211 void showKinds() const;
212 void showSummary() const;
213 void showSortsAndSubsorts() const;
214 void showModule(bool all = true) const;
215 void showModules(bool all) const;
216 void showView() const;
217 void showVars() const;
218 void showOps(bool all = true) const;
219 void showMbs(bool all = true) const;
220 void showEqs(bool all = true) const;
221 void showRls(bool all = true) const;
222
223 ImportModule* getModuleOrIssueWarning(int name, const LineNumber& lineNumber);
224 ImportModule* makeModule(const ModuleExpression* expr, ImportModule* enclosingModule = 0);
225
226 private:
227 typedef void (Interpreter::*ContinueFuncPtr)(Int64 limit, bool debug);
228
229 static DagNode* makeDag(Term* subjectTerm);
230 static void beginRewriting(bool debug);
231 static void printTiming(Int64 nrRewrites, Int64 cpu, Int64 real);
232 static void printBubble(ostream& s, const Vector<int>& bubble);
233
234 void clearContinueInfo();
235 DagNode* makeDag(const Vector<Token>& subject);
236 void startUsingModule(VisibleModule* module);
237 void printModifiers(Int64 number, Int64 number2);
238 void printStats(const Timer& timer, RewritingContext& context, bool timingFlag);
239 void endRewriting(Timer& timer,
240 UserLevelRewritingContext* context,
241 VisibleModule* module,
242 ContinueFuncPtr cf = 0);
243 void rewriteCont(Int64 limit, bool debug);
244 void fRewriteCont(Int64 limit, bool debug);
245 void eRewriteCont(Int64 limit, bool debug);
246 bool contLoop2(const Vector<Token>& input);
247 void doLoop(DagNode* d, VisibleModule* module);
248 void searchCont(Int64 limit, bool debug);
249 void sRewriteCont(Int64 limit, bool debug);
250 void doSearching(Timer& timer,
251 VisibleModule* module,
252 RewriteSequenceSearch* state,
253 int solutionCount,
254 int limit);
255 void doNarrowing(Timer& timer,
256 VisibleModule* module,
257 NarrowingSequenceSearch* state,
258 int solutionCount,
259 int limit);
260 void doExternalRewriting(UserLevelRewritingContext* context, Int64 limit);
261 void doStrategicSearch(Timer& timer,
262 VisibleModule* module,
263 StrategicSearch* state,
264 int solutionCount,
265 int limit);
266 void printDecisionTime(const Timer& timer);
267 void printSearchTiming(const Timer& timer, RewriteSequenceSearch* state);
268 void doMatching(Timer& timer,
269 VisibleModule* module,
270 MatchSearchState* state,
271 int solutionCount,
272 int limit);
273
274 void matchCont(Int64 limit, bool debug);
275 void doUnification(Timer& timer,
276 VisibleModule* module,
277 UnificationProblem* problem,
278 int solutionCount,
279 int limit);
280 void unifyCont(Int64 limit, bool debug);
281 void updateSet(set<int>& target, bool add);
282
283 ofstream* xmlLog;
284 MaudemlBuffer* xmlBuffer;
285
286 int flags;
287 int printFlags;
288 SyntacticPreModule* currentModule;
289 View* currentView;
290 //
291 // Continuation information.
292 //
293 UserLevelRewritingContext* savedContext;
294 MatchSearchState* savedMatchSearchState;
295 UnificationProblem* savedUnificationProblem;
296 RewriteSequenceSearch* savedRewriteSequenceSearch;
297 StrategicSearch* savedStrategicSearch;
298 int savedSolutionCount;
299 VisibleModule* savedModule;
300 ContinueFuncPtr continueFunc;
301 Vector<Token> savedLoopSubject;
302
303 set<int> selected; // temporary for building set of identifiers
304 set<int> traceIds; // names of symbols/labels selected for tracing
305 set<int> breakIds; // names of symbols/labels selected as break points
306 set<int> excludedModules; // names of modules to be excluded from tracing
307 set<int> concealedSymbols; // names of symbols to have their arguments concealed during printing
308 };
309
310 inline void
traceSelect(bool add)311 Interpreter::traceSelect(bool add)
312 {
313 updateSet(traceIds, add);
314 }
315
316 inline void
breakSelect(bool add)317 Interpreter::breakSelect(bool add)
318 {
319 updateSet(breakIds, add);
320 }
321
322 inline void
traceExclude(bool add)323 Interpreter::traceExclude(bool add)
324 {
325 updateSet(excludedModules, add);
326 }
327
328 inline void
printConceal(bool add)329 Interpreter::printConceal(bool add)
330 {
331 updateSet(concealedSymbols, add);
332 }
333
334 inline bool
traceId(int id)335 Interpreter::traceId(int id)
336 {
337 return traceIds.find(id) != traceIds.end();
338 }
339
340 inline bool
breakId(int id)341 Interpreter::breakId(int id)
342 {
343 return breakIds.find(id) != breakIds.end();
344 }
345
346 inline bool
excludedModule(int id)347 Interpreter::excludedModule(int id)
348 {
349 return excludedModules.find(id) != excludedModules.end();
350 }
351
352 inline MaudemlBuffer*
getXmlBuffer() const353 Interpreter::getXmlBuffer() const
354 {
355 return xmlBuffer;
356 }
357
358 inline bool
getFlag(Flags flag) const359 Interpreter::getFlag(Flags flag) const
360 {
361 return flags & flag;
362 }
363
364 inline bool
getPrintFlag(PrintFlags flag) const365 Interpreter::getPrintFlag(PrintFlags flag) const
366 {
367 return printFlags & flag;
368 }
369
370 inline int
getPrintFlags() const371 Interpreter::getPrintFlags() const
372 {
373 return printFlags;
374 }
375
376 inline SyntacticPreModule*
getCurrentModule() const377 Interpreter::getCurrentModule() const
378 {
379 return currentModule;
380 }
381
382 inline View*
getCurrentView() const383 Interpreter::getCurrentView() const
384 {
385 return currentView;
386 }
387
388 inline void
setCurrentView(View * view)389 Interpreter::setCurrentView(View* view)
390 {
391 currentView = view;
392 }
393
394 #endif
395