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 QuotedIdentifierOpSymbol.
25 //
26
27 #include <sstream>
28
29 // utility stuff
30 #include "macros.hh"
31 #include "vector.hh"
32 #include "stringTable.hh"
33
34 // forward declarations
35 #include "interface.hh"
36 #include "core.hh"
37 #include "freeTheory.hh"
38 #include "NA_Theory.hh"
39 #include "builtIn.hh"
40 #include "mixfix.hh"
41
42 // interface class definitions
43 #include "symbol.hh"
44 #include "dagNode.hh"
45
46 // core class definitions
47 #include "dagArgumentIterator.hh"
48 #include "substitution.hh"
49 #include "rewritingContext.hh"
50 #include "symbolMap.hh"
51
52 // free theory class definitions
53 #include "freeDagNode.hh"
54
55 // built in class definitions
56 #include "stringSymbol.hh"
57 #include "stringDagNode.hh"
58 #include "bindingMacros.hh"
59
60 // front end class definitions
61 #include "userLevelRewritingContext.hh"
62 #include "quotedIdentifierSymbol.hh"
63 #include "quotedIdentifierDagNode.hh"
64 #include "quotedIdentifierOpSymbol.hh"
65 #include "token.hh"
66
67 #ifdef MOS
68 int QuotedIdentifierOpSymbol::counter = 1;
69 #endif
70
QuotedIdentifierOpSymbol(int id,int nrArgs)71 QuotedIdentifierOpSymbol::QuotedIdentifierOpSymbol(int id, int nrArgs)
72 : FreeSymbol(id, nrArgs)
73 {
74 op = NONE;
75 quotedIdentifierSymbol = 0;
76 stringSymbol = 0;
77 }
78
79 bool
attachData(const Vector<Sort * > & opDeclaration,const char * purpose,const Vector<const char * > & data)80 QuotedIdentifierOpSymbol::attachData(const Vector<Sort*>& opDeclaration,
81 const char* purpose,
82 const Vector<const char*>& data)
83 {
84 BIND_OP(purpose, QuotedIdentifierOpSymbol, op, data);
85 return FreeSymbol::attachData(opDeclaration, purpose, data);
86 }
87
88 bool
attachSymbol(const char * purpose,Symbol * symbol)89 QuotedIdentifierOpSymbol::attachSymbol(const char* purpose, Symbol* symbol)
90 {
91 BIND_SYMBOL(purpose, symbol, quotedIdentifierSymbol, QuotedIdentifierSymbol*);
92 BIND_SYMBOL(purpose, symbol, stringSymbol, StringSymbol*);
93 return FreeSymbol::attachSymbol(purpose, symbol);
94 }
95
96 void
copyAttachments(Symbol * original,SymbolMap * map)97 QuotedIdentifierOpSymbol::copyAttachments(Symbol* original, SymbolMap* map)
98 {
99 QuotedIdentifierOpSymbol* orig = safeCast(QuotedIdentifierOpSymbol*, original);
100 op = orig->op;
101 COPY_SYMBOL(orig, quotedIdentifierSymbol, map, QuotedIdentifierSymbol*);
102 COPY_SYMBOL(orig, stringSymbol, map, StringSymbol*);
103 FreeSymbol::copyAttachments(original, map);
104 }
105
106 void
getDataAttachments(const Vector<Sort * > & opDeclaration,Vector<const char * > & purposes,Vector<Vector<const char * >> & data)107 QuotedIdentifierOpSymbol::getDataAttachments(const Vector<Sort*>& opDeclaration,
108 Vector<const char*>& purposes,
109 Vector<Vector<const char*> >& data)
110 {
111 int nrDataAttachments = purposes.length();
112 purposes.resize(nrDataAttachments + 1);
113 purposes[nrDataAttachments] = "QuotedIdentifierOpSymbol";
114 data.resize(nrDataAttachments + 1);
115 data[nrDataAttachments].resize(1);
116 const char*& d = data[nrDataAttachments][0];
117 switch (op)
118 {
119 CODE_CASE(d, 's', 't', "string")
120 CODE_CASE(d, 'q', 'i', "qid")
121 #ifdef MOS
122 CODE_CASE(d, 'm', 'o', "mo")
123 #endif
124 default:
125 CantHappen("bad qid op");
126 }
127 FreeSymbol::getDataAttachments(opDeclaration, purposes, data);
128 }
129
130 void
getSymbolAttachments(Vector<const char * > & purposes,Vector<Symbol * > & symbols)131 QuotedIdentifierOpSymbol::getSymbolAttachments(Vector<const char*>& purposes,
132 Vector<Symbol*>& symbols)
133 {
134 APPEND_SYMBOL(purposes, symbols, quotedIdentifierSymbol);
135 APPEND_SYMBOL(purposes, symbols, stringSymbol);
136 FreeSymbol::getSymbolAttachments(purposes, symbols);
137 }
138
139 bool
eqRewrite(DagNode * subject,RewritingContext & context)140 QuotedIdentifierOpSymbol::eqRewrite(DagNode* subject, RewritingContext& context)
141 {
142 Assert(this == subject->symbol(), "bad symbol");
143 FreeDagNode* d = safeCast(FreeDagNode*, subject);
144 //
145 // Evaluate our arguments.
146 //
147 DagNode* a1 = d->getArgument(0);
148 a1->reduce(context);
149 switch (op)
150 {
151 case CODE('s', 't'):
152 {
153 if (a1->symbol() == quotedIdentifierSymbol)
154 {
155 QuotedIdentifierDagNode* d1 = static_cast<QuotedIdentifierDagNode*>(a1);
156 bool trace = RewritingContext::getTraceStatus();
157 if (trace)
158 {
159 context.tracePreEqRewrite(subject, 0, RewritingContext::BUILTIN);
160 if (context.traceAbort())
161 return false;
162 }
163 (void) new(subject) StringDagNode(stringSymbol, Token::name(d1->getIdIndex()));
164 context.incrementEqCount();
165 if (trace)
166 context.tracePostEqRewrite(subject);
167 return true;
168 }
169 break;
170 }
171 case CODE('q', 'i'):
172 {
173 if (a1->symbol() == stringSymbol)
174 {
175 int idIndex = Token::ropeToPrefixNameCode(static_cast<StringDagNode*>(a1)->getValue());
176 if (idIndex != NONE)
177 {
178 bool trace = RewritingContext::getTraceStatus();
179 if (trace)
180 {
181 context.tracePreEqRewrite(subject, 0, RewritingContext::BUILTIN);
182 if (context.traceAbort())
183 return false;
184 }
185 (void) new(subject) QuotedIdentifierDagNode(quotedIdentifierSymbol, idIndex);
186 context.incrementEqCount();
187 if (trace)
188 context.tracePostEqRewrite(subject);
189 return true;
190 }
191 }
192 break;
193 }
194 #ifdef MOS
195 case CODE('m', 'o'):
196 {
197 if (a1->symbol() == quotedIdentifierSymbol)
198 {
199 QuotedIdentifierDagNode* d1 = static_cast<QuotedIdentifierDagNode*>(a1);
200 const char* s1 = Token::name(d1->getIdIndex());
201 if (strcmp(s1, "RESET") == 0)
202 counter = 0;
203
204 ostringstream ost(s1);
205 ost << counter;
206 ++counter;
207 int idIndex = Token::encode(ost.str().c_str());
208
209 bool trace = RewritingContext::getTraceStatus();
210 if (trace)
211 {
212 context.tracePreEqRewrite(subject, 0, RewritingContext::BUILTIN);
213 if (context.traceAbort())
214 return false;
215 }
216 (void) new(subject) QuotedIdentifierDagNode(quotedIdentifierSymbol, idIndex);
217 context.incrementEqCount();
218 if (trace)
219 context.tracePostEqRewrite(subject);
220 return true;
221 }
222 break;
223 }
224 #endif
225 }
226 return FreeSymbol::eqRewrite(subject, context);
227 }
228