1 /*
2
3 This file is part of the Maude 2 interpreter.
4
5 Copyright 1997-2010 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 substitutions.
25 //
26 // Substitutions are used to hold partly built dags as well as variable
27 // variable bindings so that the same dag construction code can handle
28 // variable and non-variable operator arguments without branching.
29 //
30 // For normal rewriting purposes a substitution is divided in to a fragile
31 // part which holds variables bindings and construction subdags that are shared
32 // between conditions fragments and/or the rhs, and local construction
33 // temporaries. The former need to be protected from the garbage collector
34 // and are copied when making a copy of the substitution. The latter are
35 // assumed to valid only during the construction of a single dag, and can
36 // be trashed afterwards.
37 //
38 #ifndef _substitution_hh_
39 #define _substitution_hh_
40
41 class Substitution
42 {
43 NO_COPYING(Substitution);
44
45 public:
46 Substitution(int size); // for local substitutions in lhs automata
47 Substitution(int size, int cSize); // rewriting contexts
48 static void notify(int size);
49
50 void clear(long size);
51 void finished();
52 DagNode* value(int index) const;
53 void bind(int index, DagNode* value);
54 void copy(const Substitution& original);
55 void clone(const Substitution& original);
56 LocalBinding* operator-(const Substitution& original) const;
57 int nrFragileBindings() const;
58
59 protected:
60 int addNewVariable();
61
62 private:
63 Vector<DagNode*> values; // only allow even sizes
64 int copySize;
65 };
66
67 inline
Substitution(int size)68 Substitution::Substitution(int size) : values(size)
69 {
70 Assert(size >= 0, "-ve substitution size" << size);
71 DebugAdvisoryCheck(size != 0, "made a zero length substitution");
72 copySize = size;
73 }
74
75 inline
Substitution(int size,int cSize)76 Substitution::Substitution(int size, int cSize) : values(size)
77 {
78 Assert(size >= 0, "-ve substitution size " << size);
79 Assert(cSize >= 0, "-ve substitution cSize " << cSize);
80 Assert(cSize <= size, "cSize > size " << cSize << ' ' << size);
81 DebugAdvisoryCheck(size != 0, "made a zero length substitution");
82 copySize = cSize;
83 }
84
85
86 inline void
clear(long size)87 Substitution::clear(long size)
88 {
89 //cout << "Substitution::clear() values.size() = " << values.size() <<
90 // " copySize " << copySize << endl;
91 //
92 // Take a long argument to avoid the need for an explicit extension instruction on x86-64.
93 //
94 Assert(size >= 0, "-ve size");
95 Assert(size <= values.length(), "size > length");
96 Assert(values.length() != 0, "clearing of zero length substitutions is not supported");
97 //
98 // Save size early so we don't tie up a register.
99 //
100 copySize = size;
101 //
102 // We alway clear at least 1 value in order to get a faster loop
103 // since the case size = 0 occurs very infrequently, and clearing
104 // 1 value in this case does no harm.
105 //
106 Vector<DagNode*>::iterator i = values.begin();
107 Vector<DagNode*>::iterator e = i + size;
108 do
109 {
110 *i = 0;
111 }
112 while (++i < e); // i > e possible if size = 0
113 }
114
115 inline DagNode*
value(int index) const116 Substitution::value(int index) const
117 {
118 Assert(index >= 0, "-ve index " << index);
119 Assert(index < static_cast<int>(values.size()), "index too big " << index << " vs " << values.size());
120 return values[index];
121 }
122
123 inline void
bind(int index,DagNode * value)124 Substitution::bind(int index, DagNode* value)
125 {
126 Assert(index >= 0, "-ve index " << index);
127 Assert(index < static_cast<int>(values.size()), "index too big " << index << " vs " << values.size());
128 values[index] = value;
129 }
130
131 inline int
nrFragileBindings() const132 Substitution::nrFragileBindings() const
133 {
134 return copySize;
135 }
136
137 inline void
finished()138 Substitution::finished()
139 {
140 copySize = 0;
141 }
142
143 inline void
copy(const Substitution & original)144 Substitution::copy(const Substitution& original)
145 {
146 //cout << "Substitution::copy() values.size() = " << values.size() <<
147 // " copySize " << copySize << " original.copySize = " << original.copySize << endl;
148 Assert(copySize == original.copySize, "size mismatch (" << copySize <<
149 " vs " << original.copySize << ')');
150 if (copySize > 0)
151 {
152 Vector<DagNode*>::iterator dest = values.begin();
153 Vector<DagNode*>::const_iterator source = original.values.begin();
154 Vector<DagNode*>::const_iterator end = source + copySize;
155 do
156 {
157 *dest = *source;
158 ++dest;
159 ++source;
160 }
161 while (source != end);
162 }
163 }
164
165 inline int
addNewVariable()166 Substitution::addNewVariable()
167 {
168 int index = copySize;
169 ++copySize;
170 //
171 // We make the underlying substitution larger if necessary. We never make it smaller
172 // since some slots may be reserved for construction purposes (not part of the copy size)
173 // and we must not lose them.
174 //
175 if (copySize > values.length())
176 values.expandTo(copySize);
177 values[index] = 0;
178 return index;
179 }
180
181 #endif
182