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 // Implementation for class UserLevelRewritingContext
25 //
26
27 //#include <unistd.h> // HACK
28
29 // utility stuff
30 #include "macros.hh"
31 #include "vector.hh"
32 #include "pointerSet.hh"
33 #include "bddUser.hh"
34
35 // forward declarations
36 #include "interface.hh"
37 #include "core.hh"
38 #include "variable.hh"
39 #include "strategyLanguage.hh"
40 #include "mixfix.hh"
41
42 // interface class definitions
43 #include "symbol.hh"
44 #include "dagNode.hh"
45 #include "higher.hh"
46
47 // core class definitions
48 #include "redexPosition.hh"
49 #include "variableSymbol.hh"
50 #include "rewritingContext.hh"
51 #include "conditionFragment.hh"
52 #include "sortConstraint.hh"
53 #include "equation.hh"
54 #include "rule.hh"
55 #include "narrowingVariableInfo.hh"
56
57 // variable class definitions
58 #include "variableTerm.hh"
59 #include "variableDagNode.hh"
60
61 // front end class definitions
62 #include "token.hh"
63 #include "userLevelRewritingContext.hh"
64 //#include "preModule.hh" // HACK
65 #include "autoWrapBuffer.hh"
66
67 #include "interpreter.hh" // HACK
68 #include "global.hh" // HACK shouldn't be accessing global variables
69
70 // our stuff
71 #include "interact.cc"
72 #include "trial.cc"
73
74 bool UserLevelRewritingContext::tracePostFlag = false;
75 const char UserLevelRewritingContext::header[] = "*********** ";
76 ostream* UserLevelRewritingContext::printAttrStream = &cout;
77
UserLevelRewritingContext(DagNode * root)78 UserLevelRewritingContext::UserLevelRewritingContext(DagNode* root)
79 : ObjectSystemRewritingContext(root),
80 parent(0),
81 purpose(TOP_LEVEL_EVAL),
82 localTraceFlag(true)
83 {
84 }
85
UserLevelRewritingContext(DagNode * root,UserLevelRewritingContext * parent,int purpose,bool localTraceFlag)86 UserLevelRewritingContext::UserLevelRewritingContext(DagNode* root,
87 UserLevelRewritingContext* parent,
88 int purpose,
89 bool localTraceFlag)
90 : ObjectSystemRewritingContext(root),
91 parent(parent),
92 purpose(purpose),
93 localTraceFlag(localTraceFlag)
94 {
95 }
96
97 RewritingContext*
makeSubcontext(DagNode * root,int purpose)98 UserLevelRewritingContext::makeSubcontext(DagNode* root, int purpose)
99 {
100 return new UserLevelRewritingContext(root, this, purpose,
101 localTraceFlag &&
102 (purpose != CONDITION_EVAL || interpreter.getFlag(Interpreter::TRACE_CONDITION)));
103 }
104
105 bool
dontTrace(const DagNode * redex,const PreEquation * pe)106 UserLevelRewritingContext::dontTrace(const DagNode* redex, const PreEquation* pe)
107 {
108 Symbol* symbol = redex->symbol();
109 return (interpreter.getFlag(Interpreter::TRACE_SELECT) &&
110 !(interpreter.traceId(symbol->id()) ||
111 (pe != 0 && interpreter.traceId(pe->getLabel().id())))) ||
112 interpreter.excludedModule(symbol->getModule()->id()) ||
113 (pe == 0 && !interpreter.getFlag(Interpreter::TRACE_BUILTIN));
114 }
115
116 void
checkForPrintAttribute(MixfixModule::ItemType itemType,const PreEquation * item)117 UserLevelRewritingContext::checkForPrintAttribute(MixfixModule::ItemType itemType, const PreEquation* item)
118 {
119 if (item != 0)
120 {
121 MixfixModule* m = safeCast(MixfixModule*, item->getModule());
122 const PrintAttribute* pa = m->getPrintAttribute(itemType, item);
123 if (pa != 0)
124 {
125 pa->print(*printAttrStream, *this);
126 if (interpreter.getFlag(Interpreter::PRINT_ATTRIBUTE_NEWLINE))
127 *printAttrStream << '\n';
128 printAttrStream->flush();
129 }
130 }
131 }
132
133 void
tracePreEqRewrite(DagNode * redex,const Equation * equation,int type)134 UserLevelRewritingContext::tracePreEqRewrite(DagNode* redex,
135 const Equation* equation,
136 int type)
137 {
138 if (interpreter.getFlag(Interpreter::PROFILE))
139 {
140 safeCast(ProfileModule*, root()->symbol()->getModule())->
141 profileEqRewrite(redex, equation, type);
142 }
143 if (interpreter.getFlag(Interpreter::PRINT_ATTRIBUTE))
144 checkForPrintAttribute(MetadataStore::EQUATION, equation);
145
146 if (handleDebug(redex, equation) ||
147 !localTraceFlag ||
148 !(interpreter.getFlag(Interpreter::TRACE_EQ)) ||
149 dontTrace(redex, equation))
150 {
151 tracePostFlag = false;
152 return;
153 }
154 tracePostFlag = true;
155
156 if (interpreter.getFlag(Interpreter::TRACE_BODY))
157 cout << header << "equation\n";
158 if (equation == 0)
159 {
160 if (type == RewritingContext::BUILTIN)
161 cout << "(built-in equation for symbol " << redex->symbol() << ")\n";
162 else if (type == RewritingContext::MEMOIZED)
163 cout << "(memo table lookup for symbol " << redex->symbol() << ")\n";
164 }
165 else
166 {
167 if (interpreter.getFlag(Interpreter::TRACE_BODY))
168 {
169 cout << equation << '\n';
170 if (interpreter.getFlag(Interpreter::TRACE_SUBSTITUTION))
171 printSubstitution(*this, *equation);
172 }
173 else
174 {
175 const Label& label = equation->getLabel();
176 if (label.id() == NONE)
177 cout << "(unlabeled equation)\n";
178 else
179 cout << &label << '\n';
180 }
181 }
182 if (interpreter.getFlag(Interpreter::TRACE_WHOLE))
183 cout << "Old: " << root() << '\n';
184 if (interpreter.getFlag(Interpreter::TRACE_REWRITE))
185 cout << redex << "\n--->\n";
186 DebugAdvisory(static_cast<void*>(redex));
187 }
188
189 void
tracePostEqRewrite(DagNode * replacement)190 UserLevelRewritingContext::tracePostEqRewrite(DagNode* replacement)
191 {
192 if (tracePostFlag)
193 {
194 Assert(!abortFlag, "abort flag set");
195 if (interpreter.getFlag(Interpreter::TRACE_REWRITE))
196 cout << replacement << '\n';
197 DebugAdvisory(static_cast<void*>(replacement));
198 if (interpreter.getFlag(Interpreter::TRACE_WHOLE))
199 cout << "New: " << root() << '\n';
200 }
201 }
202
203 void
tracePreRuleRewrite(DagNode * redex,const Rule * rule)204 UserLevelRewritingContext::tracePreRuleRewrite(DagNode* redex, const Rule* rule)
205 {
206 if (interpreter.getFlag(Interpreter::PROFILE))
207 {
208 safeCast(ProfileModule*, root()->symbol()->getModule())->
209 profileRlRewrite(redex, rule);
210 }
211 if (interpreter.getFlag(Interpreter::PRINT_ATTRIBUTE))
212 checkForPrintAttribute(MetadataStore::RULE, rule);
213
214 if (handleDebug(redex, rule) ||
215 !localTraceFlag ||
216 !(interpreter.getFlag(Interpreter::TRACE_RL)) ||
217 dontTrace(redex, rule))
218 {
219 tracePostFlag = false;
220 return;
221 }
222 tracePostFlag = true;
223 if (interpreter.getFlag(Interpreter::TRACE_BODY))
224 cout << header << "rule\n";
225 if (rule == 0)
226 cout << "(built-in rule for symbol " << redex->symbol() << ")\n";
227 else
228 {
229 if (interpreter.getFlag(Interpreter::TRACE_BODY))
230 {
231 cout << rule << '\n';
232 if (interpreter.getFlag(Interpreter::TRACE_SUBSTITUTION))
233 printSubstitution(*this, *rule);
234 }
235 else
236 {
237 const Label& label = rule->getLabel();
238 if (label.id() == NONE)
239 cout << "(unlabeled rule)\n";
240 else
241 cout << &label << '\n';
242 }
243 }
244 if (interpreter.getFlag(Interpreter::TRACE_WHOLE))
245 cout << "Old: " << root() << '\n';
246 if (interpreter.getFlag(Interpreter::TRACE_REWRITE))
247 cout << redex << "\n--->\n";
248 }
249
250 void
tracePostRuleRewrite(DagNode * replacement)251 UserLevelRewritingContext::tracePostRuleRewrite(DagNode* replacement)
252 {
253 if (tracePostFlag)
254 {
255 if (interpreter.getFlag(Interpreter::TRACE_REWRITE))
256 cout << replacement << '\n';
257 if (interpreter.getFlag(Interpreter::TRACE_WHOLE))
258 cout << "New: " << root() << '\n';
259 }
260 }
261
262 void
traceNarrowingStep(Rule * rule,DagNode * redex,DagNode * replacement,const NarrowingVariableInfo * variableInfo,const Substitution * substitution,DagNode * newState)263 UserLevelRewritingContext::traceNarrowingStep(Rule* rule,
264 DagNode* redex,
265 DagNode* replacement,
266 const NarrowingVariableInfo* variableInfo,
267 const Substitution* substitution,
268 DagNode* newState)
269 {
270 if (handleDebug(redex, rule) ||
271 !localTraceFlag ||
272 !(interpreter.getFlag(Interpreter::TRACE_RL)) ||
273 dontTrace(redex, rule))
274 return;
275
276 if (interpreter.getFlag(Interpreter::TRACE_BODY))
277 {
278 cout << Tty(Tty::MAGENTA) << header << "narrowing step\n" << Tty(Tty::RESET) << rule << '\n';
279 if (interpreter.getFlag(Interpreter::TRACE_SUBSTITUTION))
280 {
281 cout << "Rule variable bindings:\n";
282 printSubstitution(*substitution, *rule);
283
284 cout << "Subject variable bindings:\n";
285 int nrSubjectVariables = variableInfo->getNrVariables();
286 if (nrSubjectVariables == 0)
287 cout << "empty substitution\n";
288 else
289 {
290 int variableBase = rule->getModule()->getMinimumSubstitutionSize();
291 for (int i = 0; i < nrSubjectVariables; ++i)
292 {
293 DagNode* v = variableInfo->index2Variable(i);
294 DagNode* d = substitution->value(variableBase + i);
295 Assert(v != 0, "null variable");
296 cout << v << " --> ";
297 if (d == 0)
298 cout << "(unbound)\n";
299 else
300 cout << d << '\n';
301 }
302 }
303 }
304 }
305 if (interpreter.getFlag(Interpreter::TRACE_WHOLE))
306 cout << "Old: " << root() << '\n';
307 if (interpreter.getFlag(Interpreter::TRACE_REWRITE))
308 cout << redex << "\n--->\n" << replacement << '\n';
309 if (interpreter.getFlag(Interpreter::TRACE_WHOLE))
310 cout << "New: " << newState << '\n';
311 }
312
313 void
traceVariantNarrowingStep(Equation * equation,const Vector<DagNode * > & oldVariantSubstitution,DagNode * redex,DagNode * replacement,const NarrowingVariableInfo & variableInfo,const Substitution * substitution,DagNode * newState,const Vector<DagNode * > & newVariantSubstitution,const NarrowingVariableInfo & originalVariables)314 UserLevelRewritingContext::traceVariantNarrowingStep(Equation* equation,
315 const Vector<DagNode*>& oldVariantSubstitution,
316 DagNode* redex,
317 DagNode* replacement,
318 const NarrowingVariableInfo& variableInfo,
319 const Substitution* substitution,
320 DagNode* newState,
321 const Vector<DagNode*>& newVariantSubstitution,
322 const NarrowingVariableInfo& originalVariables)
323 {
324 if (handleDebug(redex, equation) ||
325 !localTraceFlag ||
326 !(interpreter.getFlag(Interpreter::TRACE_EQ)) ||
327 dontTrace(redex, equation))
328 return;
329
330 if (interpreter.getFlag(Interpreter::TRACE_BODY))
331 {
332 cout << Tty(Tty::CYAN) << header << "variant narrowing step\n" << Tty(Tty::RESET) << equation << '\n';
333 if (interpreter.getFlag(Interpreter::TRACE_SUBSTITUTION))
334 {
335 cout << "Equation variable bindings:\n";
336 printSubstitution(*substitution, *equation);
337
338 cout << "Old variant variable bindings:\n";
339 int nrSubjectVariables = variableInfo.getNrVariables();
340 if (nrSubjectVariables == 0)
341 cout << "empty substitution\n";
342 else
343 {
344 int variableBase = equation->getModule()->getMinimumSubstitutionSize();
345 for (int i = 0; i < nrSubjectVariables; ++i)
346 {
347 DagNode* v = variableInfo.index2Variable(i);
348 DagNode* d = substitution->value(variableBase + i);
349 Assert(v != 0, "null variable");
350 /*
351 DebugAdvisory(static_cast<void*>(v) << " --> " <<
352 static_cast<void*>(d) << " / " <<
353 static_cast<void*>(d->symbol()));
354 */
355
356 cout << v << " --> ";
357 if (d == 0)
358 cout << "(unbound)\n";
359 else
360 cout << d << '\n';
361 }
362 }
363 }
364 }
365 if (interpreter.getFlag(Interpreter::TRACE_WHOLE))
366 {
367 cout << "\nOld variant: " << root() << '\n';
368 int nrBindings = oldVariantSubstitution.size();
369 for (int i = 0; i < nrBindings; ++i)
370 {
371 DagNode* v = originalVariables.index2Variable(i);
372 DagNode* d = oldVariantSubstitution[i];
373 cout << v << " --> " << d << '\n';
374 }
375 cout << '\n';
376 }
377 if (interpreter.getFlag(Interpreter::TRACE_REWRITE))
378 cout << redex << "\n--->\n" << replacement << '\n';
379 if (interpreter.getFlag(Interpreter::TRACE_WHOLE))
380 {
381 cout << "\nNew variant: " << newState << '\n';
382 int nrBindings = newVariantSubstitution.size();
383 for (int i = 0; i < nrBindings; ++i)
384 {
385 DagNode* v = originalVariables.index2Variable(i);
386 DagNode* d = newVariantSubstitution[i];
387 cout << v << " --> " << d << '\n';
388 }
389 cout << '\n';
390 }
391 }
392
393 void
tracePreScApplication(DagNode * subject,const SortConstraint * sc)394 UserLevelRewritingContext::tracePreScApplication(DagNode* subject, const SortConstraint* sc)
395 {
396 if (interpreter.getFlag(Interpreter::PROFILE))
397 {
398 safeCast(ProfileModule*, root()->symbol()->getModule())->
399 profileMbRewrite(subject, sc);
400 }
401 if (interpreter.getFlag(Interpreter::PRINT_ATTRIBUTE))
402 checkForPrintAttribute(MetadataStore::MEMB_AX, sc);
403
404 if (handleDebug(subject, sc) ||
405 !localTraceFlag ||
406 !(interpreter.getFlag(Interpreter::TRACE_MB)) ||
407 dontTrace(subject, sc))
408 return;
409 if (interpreter.getFlag(Interpreter::TRACE_BODY))
410 cout << header << "membership axiom\n";
411 if (sc == 0)
412 cout << "(built-in membership axiom for symbol " << subject->symbol() << ")\n";
413 else
414 {
415 if (interpreter.getFlag(Interpreter::TRACE_BODY))
416 {
417 cout << sc << '\n';
418 if (interpreter.getFlag(Interpreter::TRACE_SUBSTITUTION))
419 printSubstitution(*this, *sc);
420 }
421 else
422 {
423 const Label& label = sc->getLabel();
424 if (label.id() == NONE)
425 cout << "(unlabeled membership axiom)\n";
426 else
427 cout << &label << '\n';
428 }
429 }
430 if (interpreter.getFlag(Interpreter::TRACE_WHOLE))
431 cout << "Whole: " << root() << '\n';
432 //
433 // Coverity discovered bug - sc could be 0.
434 //
435 if (interpreter.getFlag(Interpreter::TRACE_REWRITE))
436 cout << subject->getSort() << ": " << subject << " becomes " << sc->getSort() << '\n'; // BUG
437 }
438
439 void
printSubstitution(const Substitution & substitution,const VariableInfo & varInfo,const NatSet & ignoredIndices)440 UserLevelRewritingContext::printSubstitution(const Substitution& substitution,
441 const VariableInfo& varInfo,
442 const NatSet& ignoredIndices)
443 {
444 int nrVars = varInfo.getNrRealVariables();
445 bool printedVariable = false;
446 for (int i = 0; i < nrVars; i++)
447 {
448 if (ignoredIndices.contains(i))
449 continue;
450
451 Term* v = varInfo.index2Variable(i);
452 DagNode* d = substitution.value(i);
453 /*
454 DebugAdvisory(static_cast<void*>(v) << " --> " <<
455 static_cast<void*>(d) << " / " <<
456 ((d == 0) ? static_cast<void*>(0) : static_cast<void*>(d->symbol())));
457 */
458 Assert(v != 0, "null variable");
459 cout << v << " --> ";
460 if (d == 0)
461 cout << "(unbound)\n";
462 else
463 cout << d << '\n';
464 printedVariable = true;
465 }
466 if (!printedVariable)
467 cout << "empty substitution\n";
468 }
469