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 // Abstract base class for function/variable symbol definitions.
25 //
26 #ifndef _symbol_hh_
27 #define _symbol_hh_
28 #include "fullCompiler.hh"
29
30 #include "namedEntity.hh"
31 #include "lineNumber.hh"
32 #include "moduleItem.hh"
33 #include "sort.hh"
34 #include "connectedComponent.hh"
35 #include "sortTable.hh"
36 #include "sortConstraintTable.hh"
37 #include "equationTable.hh"
38 #include "ruleTable.hh"
39 #include "strategy.hh"
40 #include "memoTable.hh"
41
42 class Symbol
43 : public RuleTable,
44 public NamedEntity,
45 public LineNumber,
46 public SortTable,
47 public SortConstraintTable,
48 public EquationTable,
49 public Strategy,
50 public MemoTable
51 {
52 NO_COPYING(Symbol);
53
54 static const Vector<DagNode*> noArgs;
55
56 public:
57 Symbol(int id, int arity, bool memoFlag = false);
58 virtual ~Symbol();
59
60 unsigned int getHashValue() const;
61 int compare(const Symbol* other) const;
62 bool mightMatchPattern(Term* pattern);
63 void fastComputeTrueSort(DagNode* subject, RewritingContext& context); // maybe should be const?
64 int getUniqueSortIndex() const;
65 //
66 // Functions needed for sophisticated sort analysis.
67 //
68 virtual bool rangeSortNeverLeqThan(Sort* sort);
69 virtual bool rangeSortAlwaysLeqThan(Sort* sort);
70 virtual bool domainSortAlwaysLeqThan(Sort* sort, int argNr);
71 void computePossibleDomainSorts(const NatSet& rangeSorts,
72 Vector<NatSet>& domainSorts);
73 //
74 // These functions must be defined for each derived class.
75 //
76 virtual bool eqRewrite(DagNode* subject, RewritingContext& context) = 0;
77 virtual void computeBaseSort(DagNode* subject) = 0;
78 virtual void normalizeAndComputeTrueSort(DagNode* subject, RewritingContext& context) = 0;
79 virtual Term* makeTerm(const Vector<Term*>& args) = 0;
80 virtual DagNode* makeDagNode(const Vector<DagNode*>& args = noArgs) = 0;
81 virtual void stackArguments(DagNode* subject,
82 Vector<RedexPosition>& stack,
83 int parentIndex) = 0;
84 virtual Term* termify(DagNode* dagNode) = 0;
85 //
86 // These functions may be redefined for each derived class.
87 //
88 // interSymbolPass() is called on each symbol in turn until all
89 // return false. It is use for resolving interdependencies.
90 //
91 // postInterSymbolPass() is called on each symbol after the above
92 // completes.
93 //
94 // postOpDeclarationPass() is called on each symbol after its sort
95 // table has been calculated.
96 //
97 virtual bool interSymbolPass();
98 virtual void postInterSymbolPass();
99 virtual void postOpDeclarationPass();
100 //
101 // Clear state information such as caches that affects performance but not result.
102 //
103 virtual void reset();
104 void finalizeSortInfo(); // virtual in base class SortTable
105 void fillInSortInfo(Term* subject); // virtual in base class SortTable
106 //
107 // These functions may be redefined to attach data/symbols/terms to
108 // support "special" operators.
109 //
110 virtual bool attachData(const Vector<Sort*>& opDeclaration,
111 const char* purpose,
112 const Vector<const char*>& data);
113 virtual bool attachSymbol(const char* purpose, Symbol* symbol);
114 virtual bool attachTerm(const char* purpose, Term* term);
115 virtual void copyAttachments(Symbol* original, SymbolMap* map);
116 virtual void getDataAttachments(const Vector<Sort*>& opDeclaration,
117 Vector<const char*>& purposes,
118 Vector<Vector<const char*> >& data);
119 virtual void getSymbolAttachments(Vector<const char*>& purposes,
120 Vector<Symbol*>& symbols);
121 virtual void getTermAttachments(Vector<const char*>& purposes,
122 Vector<Term*>& terms);
123 //
124 // This function might be redefined to provide better performance
125 // or special constructor semantics.
126 //
127 virtual bool isConstructor(DagNode* subject);
128
129 //
130 // Interface for unification.
131 //
132 virtual UnificationSubproblem* makeUnificationSubproblem();
133 virtual int unificationPriority() const;
134 //
135 // Symbols that can disappear under substitution must redefine this to return false.
136 //
137 virtual bool isStable() const = 0;
138 //
139 // Symbols that can resolved theory clashes (typically by collapsing) should
140 // redefined this to return true and be ready to handle alien right hand sides
141 // by restricted unification in unification problem passed to their unification
142 // subproblems.
143 //
144 virtual bool canResolveTheoryClash();
145 //
146 // Interface for hash consing.
147 //
148 virtual DagNode* makeCanonical(DagNode* original, HashConsSet* hcs) = 0;
149 //
150 // Same as above but copying is forced - original can never be the canonical dagnode.
151 //
152 virtual DagNode* makeCanonicalCopy(DagNode* original, HashConsSet* hcs) = 0;
153
154 //
155 // Generate instructions for MVM.
156 //
157 virtual Instruction* generateFinalInstruction(const Vector<int>& argumentSlots);
158 virtual Instruction* generateInstruction(int destination, const Vector<int>& argumentSlots, Instruction* nextInstruction);
159 //
160 // For symbols that want to do some post-processing after
161 // equations have been compiled for stack based interpreter.
162 //
163 virtual void stackMachinePostProcess();
164
165 int getMatchIndex() const;
166 void setMatchIndex(int index);
167
168 #ifdef COMPILER
169 void fullCompile(CompilationContext& context, bool inLine) const;
170 virtual void generateCode(CompilationContext& context) const;
171 #endif
172
173 #ifdef DUMP
174 virtual void dump(ostream& s, int indentLevel = 0);
175 #endif
176
177 protected:
178 bool acceptSortConstraint(SortConstraint* sortConstraint);
179 bool acceptEquation(Equation* equation);
180 bool acceptRule(Rule* rule);
181
182 private:
183 bool mightMatchSymbol(Symbol* symbol);
184 void slowComputeTrueSort(DagNode* subject, RewritingContext& context);
185
186 static int symbolCount;
187
188 const int orderInt; // unique integer for comparing symbols
189 int uniqueSortIndex; // > 0 for symbols that only produce an unique sort; -1 for fast case; 0 for slow case
190 int matchIndex; // for fast matching in new engine
191 };
192
193 inline unsigned int
getHashValue() const194 Symbol::getHashValue() const
195 {
196 return orderInt;
197 }
198
199 inline int
compare(const Symbol * other) const200 Symbol::compare(const Symbol* other) const
201 {
202 return orderInt - other->orderInt;
203 }
204
205 inline int
getUniqueSortIndex() const206 Symbol::getUniqueSortIndex() const
207 {
208 return uniqueSortIndex;
209 }
210
211 inline int
getMatchIndex() const212 Symbol::getMatchIndex() const
213 {
214 return matchIndex;
215 }
216
217 inline void
setMatchIndex(int index)218 Symbol::setMatchIndex(int index)
219 {
220 Assert(matchIndex == 0, "trying to set match index of " << this << " to " << index << " when it is already " << matchIndex);
221 matchIndex = index;
222 }
223
224 #endif
225