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 PositionState.
25 //
26
27 // utility stuff
28 #include "macros.hh"
29 #include "vector.hh"
30
31 // forward declarations
32 #include "interface.hh"
33 #include "core.hh"
34
35 // interface class definitions
36 #include "symbol.hh"
37 #include "dagNode.hh"
38 #include "extensionInfo.hh"
39 #include "substitution.hh"
40
41 // core class definitions
42 #include "positionState.hh"
43
PositionState(DagNode * top,int flags,int minDepth,int maxDepth)44 PositionState::PositionState(DagNode* top, int flags, int minDepth, int maxDepth)
45 : flags(flags),
46 minDepth(minDepth),
47 maxDepth(maxDepth)
48 {
49 Assert(!(flags & SET_UNSTACKABLE) || (flags & RESPECT_FROZEN),
50 "can't set unstackable if not respecting frozen");
51 positionQueue.append(RedexPosition(top, UNDEFINED, UNDEFINED));
52 depth.append(0);
53 extensionInfo = 0;
54 extensionInfoValid = true; // in case maxDepth = -1 for no extension
55 nextToReturn = -1;
56 nextToExplore = -1;
57 }
58
~PositionState()59 PositionState::~PositionState()
60 {
61 delete extensionInfo;
62 }
63
64 local_inline bool
exploreNextPosition()65 PositionState::exploreNextPosition()
66 {
67 int finish = positionQueue.length();
68 for(;;)
69 {
70 if (++nextToExplore >= finish)
71 return false;
72 int ourDepth = depth[nextToExplore];
73 if (ourDepth >= maxDepth)
74 return false;
75 DagNode* d = positionQueue[nextToExplore].node();
76 d->stackArguments(positionQueue, nextToExplore, flags & RESPECT_FROZEN);
77 int newFinish = positionQueue.length();
78 if (finish < newFinish)
79 {
80 ++ourDepth;
81 depth.expandTo(newFinish);
82 for (; finish < newFinish; finish++)
83 depth[finish] = ourDepth;
84 break;
85 }
86 else
87 {
88 //
89 // d didn't stack any arguments - check if we should make it
90 // unstackable.
91 //
92 if ((flags & SET_UNSTACKABLE) && d->isUnrewritable())
93 d->setUnstackable();
94 }
95 }
96 return true;
97 }
98
99 bool
findNextPosition()100 PositionState::findNextPosition()
101 {
102 do
103 {
104 if (++nextToReturn >= positionQueue.length() && !exploreNextPosition())
105 return false;
106 }
107 while (depth[nextToReturn] < minDepth);
108 if (maxDepth >= 0)
109 {
110 delete extensionInfo;
111 extensionInfo = 0;
112 //
113 // Force makeExtensionInfo() if getExtensionInfo() called.
114 //
115 extensionInfoValid = false;
116 }
117 return true;
118 }
119
120 PositionState::DagPair
rebuildDag(DagNode * replacement,ExtensionInfo * extInfo,PositionIndex index) const121 PositionState::rebuildDag(DagNode* replacement, ExtensionInfo* extInfo, PositionIndex index) const
122 {
123 //
124 // Extend the replacement term if needed.
125 //
126 if (extInfo != 0 && !(extInfo->matchedWhole()))
127 replacement = positionQueue[index].node()->partialConstruct(replacement, extInfo);
128 //
129 // Walk up the stack rebuilding.
130 //
131 DagNode* newDag = replacement;
132 int argIndex = positionQueue[index].argIndex();
133 for (PositionIndex i = positionQueue[index].parentIndex(); i != UNDEFINED;)
134 {
135 const RedexPosition& rp = positionQueue[i];
136 newDag = rp.node()->copyWithReplacement(argIndex, newDag);
137 argIndex = rp.argIndex();
138 i = rp.parentIndex();
139 }
140 //
141 // We return the rebuilt dag, and the extended replacement term since the caller may
142 // need the latter for tracing purposes.
143 //
144 return DagPair(newDag, replacement);
145 }
146
147 DagNode*
rebuildAndInstantiateDag(DagNode * replacement,Substitution & substitution,int firstVariable,int lastVariable,PositionIndex index) const148 PositionState::rebuildAndInstantiateDag(DagNode* replacement,
149 Substitution& substitution,
150 int firstVariable,
151 int lastVariable,
152 PositionIndex index) const
153 {
154 //
155 // We don't support extension for narrowing.
156 //
157 Assert(extensionInfo == 0 || extensionInfo->matchedWhole(), "Extension not supported");
158 //
159 // Walk up the stack rebuilding.
160 //
161 DagNode* newDag = replacement;
162 if (index == DEFAULT)
163 index = nextToReturn;
164 int argIndex = positionQueue[index].argIndex();
165 PositionIndex i = positionQueue[index].parentIndex();
166 if (i != UNDEFINED)
167 {
168 //
169 // Make eager copies of bindings we will use to avoid sharing dags that
170 // might rewrite between eager and lazy positions.
171 //
172 Vector<DagNode*> eagerCopies(lastVariable + 1);
173 for (int j = firstVariable; j <= lastVariable; ++j)
174 eagerCopies[j] = substitution.value(j)->copyEagerUptoReduced();
175 for (int j = firstVariable; j <= lastVariable; ++j)
176 substitution.value(j)->clearCopyPointers();
177
178 while (i != UNDEFINED)
179 {
180 const RedexPosition& rp = positionQueue[i];
181 newDag = rp.node()->instantiateWithReplacement(substitution, eagerCopies, argIndex, newDag);
182 argIndex = rp.argIndex();
183 i = rp.parentIndex();
184 }
185 }
186 //
187 // We return the rebuilt dag.
188 //
189 return newDag;
190 }
191