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 user level rewriting contexts
25 //
26 #ifndef _userLevelRewritingContext_hh_
27 #define _userLevelRewritingContext_hh_
28 #include <signal.h>
29 #ifdef USE_LIBSIGSEGV
30 #include "sigsegv.h"
31 #endif
32 #include "objectSystemRewritingContext.hh"
33 #include "metadataStore.hh"
34 #include "rule.hh"
35 class Token; // HACK
36
37 class UserLevelRewritingContext : public ObjectSystemRewritingContext
38 {
39 NO_COPYING(UserLevelRewritingContext);
40
41 public:
42 enum OtherPurpose
43 {
44 TOP_LEVEL_EVAL = OTHER + 1,
45 META_EVAL
46 };
47
48 enum ParseResult
49 {
50 NORMAL,
51 QUIT,
52 RESUME,
53 ABORT,
54 STEP,
55 WHERE
56 };
57
58 UserLevelRewritingContext(DagNode* root);
59 UserLevelRewritingContext(DagNode* root,
60 UserLevelRewritingContext* parent,
61 int purpose,
62 bool localTraceFlag);
63
64
65 static void setHandlers(bool handleCtrlC);
66 static ParseResult commandLoop();
67 static bool interrupted();
68 static bool aborted();
69 static void setInteractive(bool status);
70 static void setPrintAttributeStream(ostream* s);
71 static void beginCommand();
72 static void setDebug();
73 static void clearDebug();
74 static void clearInterrupt();
75 static void clearTrialCount();
76
77 RewritingContext* makeSubcontext(DagNode* root, int purpose);
78 void beAdoptedBy(UserLevelRewritingContext* newParent);
79 int traceBeginEqTrial(DagNode* subject, const Equation* equation);
80 int traceBeginRuleTrial(DagNode* subject, const Rule* rule);
81 int traceBeginScTrial(DagNode* subject, const SortConstraint* sc);
82 void traceEndTrial(int trailRef, bool success);
83 void traceExhausted(int trialRef);
84
85 void tracePreEqRewrite(DagNode* redex, const Equation* equation, int type);
86 void tracePostEqRewrite(DagNode* replacement);
87 void tracePreRuleRewrite(DagNode* redex, const Rule* rule);
88 void tracePostRuleRewrite(DagNode* replacement);
89 void tracePreScApplication(DagNode* subject, const SortConstraint* sc);
90 bool traceAbort();
91 void traceBeginFragment(int trialRef,
92 const PreEquation* preEquation,
93 int fragmentIndex,
94 bool firstAttempt);
95 void traceEndFragment(int trialRef,
96 const PreEquation* preEquation,
97 int fragmentIndex,
98 bool success);
99
100 void traceNarrowingStep(Rule* rule,
101 DagNode* redex,
102 DagNode* replacement,
103 const NarrowingVariableInfo* variableInfo,
104 const Substitution* substitution,
105 DagNode* newState);
106
107 void traceVariantNarrowingStep(Equation* equation,
108 const Vector<DagNode*>& oldVariantSubstitution,
109 DagNode* redex,
110 DagNode* replacement,
111 const NarrowingVariableInfo& variableInfo,
112 const Substitution* substitution,
113 DagNode* newState,
114 const Vector<DagNode*>& newVariantSubstitution,
115 const NarrowingVariableInfo& originalVariables);
116
117 static void printSubstitution(const Substitution& substitution,
118 const VariableInfo& varInfo,
119 const NatSet& ignoredIndices = NatSet());
120
121
122
123 private:
124 static void interruptHandler(int);
125 static void interruptHandler2(...);
126
127 #ifdef USE_LIBSIGSEGV
128 static void stackOverflowHandler(int emergency, stackoverflow_context_t scp);
129 static int sigsegvHandler(void *fault_address, int serious);
130 #endif
131 static void internalErrorHandler(int signalNr);
132
133 static void changePrompt();
134 static bool dontTrace(const DagNode* redex, const PreEquation* pe);
135 void checkForPrintAttribute(MetadataStore::ItemType itemType, const PreEquation* item);
136 bool handleDebug(const DagNode* subject, const PreEquation* pe);
137 void where();
138
139 static bool tracePostFlag;
140 static int trialCount;
141 static const char header[];
142
143 static bool interactiveFlag;
144 static bool ctrlC_Flag;
145 static bool stepFlag;
146 static bool abortFlag;
147 static int debugLevel;
148
149 static AutoWrapBuffer* wrapOut;
150 static AutoWrapBuffer* wrapErr;
151
152 static ostream* printAttrStream;
153
154 UserLevelRewritingContext* parent;
155 const int purpose;
156 bool localTraceFlag;
157 };
158
159 inline void
setPrintAttributeStream(ostream * s)160 UserLevelRewritingContext::setPrintAttributeStream(ostream* s)
161 {
162 printAttrStream = s;
163 }
164
165 inline void
clearTrialCount()166 UserLevelRewritingContext::clearTrialCount()
167 {
168 trialCount = 0;
169 }
170
171 inline bool
interrupted()172 UserLevelRewritingContext::interrupted()
173 {
174 return ctrlC_Flag;
175 }
176
177 inline bool
aborted()178 UserLevelRewritingContext::aborted()
179 {
180 return abortFlag;
181 }
182
183 inline void
setDebug()184 UserLevelRewritingContext::setDebug()
185 {
186 setTraceStatus(true);
187 stepFlag = true;
188 }
189
190 inline void
beAdoptedBy(UserLevelRewritingContext * newParent)191 UserLevelRewritingContext::beAdoptedBy(UserLevelRewritingContext* newParent)
192 {
193 parent = newParent;
194 }
195
196 #endif
197