@@ -157,8 +157,66 @@ RewriteSystem::computeCriticalPair(ArrayRef<Symbol>::const_iterator from,
157
157
return false ;
158
158
}
159
159
160
- // Add the pair (X, TYV).
161
- pairs.emplace_back (x, tyv, path);
160
+ // If X == TUW for some W, then the critical pair is (TUW, TYV),
161
+ // and we have
162
+ // - lhs == (TUV => TUW)
163
+ // - rhs == (U => Y).
164
+ //
165
+ // We explicitly apply the rewrite step (Y => U) to the beginning of the
166
+ // rewrite path, transforming the critical pair to (TYW, TYV).
167
+ //
168
+ // In particular, if V == W.[P] for some protocol P, then we in fact have
169
+ // a property rule and a same-type rule:
170
+ //
171
+ // - lhs == (TUW.[P] => TUW)
172
+ // - rhs == (U => Y)
173
+ //
174
+ // Without this hack, the critical pair would be:
175
+ //
176
+ // (TUW => TYW.[P])
177
+ //
178
+ // With this hack, the critical pair becomes:
179
+ //
180
+ // (TYW.[P] => TYW)
181
+ //
182
+ // This ensures that the newly-added rule is itself a property rule;
183
+ // otherwise, this would only be the case if addRule() reduced TUW
184
+ // into TYW without immediately reducing some subterm of TUW first.
185
+ //
186
+ // While completion will eventually simplify all such rules down into
187
+ // property rules, their existance in the first place breaks subtle
188
+ // invariants in the minimal conformances algorithm, which expects
189
+ // homotopy generators describing redundant protocol conformance rules
190
+ // to have a certain structure.
191
+ if (t.size () + rhs.getLHS ().size () <= x.size () &&
192
+ std::equal (rhs.getLHS ().begin (),
193
+ rhs.getLHS ().end (),
194
+ x.begin () + t.size ())) {
195
+ // We have a path from TUW to TYV. Invert to get a path from TYV to
196
+ // TUW.
197
+ path.invert ();
198
+
199
+ // Compute the term W.
200
+ MutableTerm w (x.begin () + t.size () + rhs.getLHS ().size (), x.end ());
201
+
202
+ // Now add a rewrite step T.(U => Y).W to get a path from TYV to
203
+ // TYW.
204
+ path.add (RewriteStep::forRewriteRule (/* startOffset=*/ t.size (),
205
+ /* endOffset=*/ w.size (),
206
+ getRuleID (rhs),
207
+ /* inverse=*/ false ));
208
+
209
+ // Compute the term TYW.
210
+ MutableTerm tyw (t);
211
+ tyw.append (rhs.getRHS ());
212
+ tyw.append (w);
213
+
214
+ // Add the pair (TYV, TYW).
215
+ pairs.emplace_back (tyv, tyw, path);
216
+ } else {
217
+ // Add the pair (X, TYV).
218
+ pairs.emplace_back (x, tyv, path);
219
+ }
162
220
} else {
163
221
// lhs == TU -> X, rhs == UV -> Y.
164
222
@@ -217,7 +275,7 @@ RewriteSystem::computeCriticalPair(ArrayRef<Symbol>::const_iterator from,
217
275
// - lhs == (TU -> X)
218
276
// - rhs == (UV -> UW).
219
277
//
220
- // We explicitly apply the rewrite step (TU = X) to the rewrite path,
278
+ // We explicitly apply the rewrite step (TU => X) to the rewrite path,
221
279
// transforming the critical pair to (XV, XW).
222
280
//
223
281
// In particular, if T == X, U == [P] for some protocol P, and
@@ -229,15 +287,15 @@ RewriteSystem::computeCriticalPair(ArrayRef<Symbol>::const_iterator from,
229
287
//
230
288
// Without this hack, the critical pair would be:
231
289
//
232
- // (T.w .[p] => T.[P].w )
290
+ // (T.W .[p] => T.[P].W )
233
291
//
234
292
// With this hack, the critical pair becomes:
235
293
//
236
- // (T.w .[p] => T.w )
294
+ // (T.W .[p] => T.W )
237
295
//
238
296
// This ensures that the newly-added rule is itself a property rule;
239
- // otherwise, this would only be the case if addRule() reduced T.[P].w
240
- // into T.w without immediately reducing some subterm of T first.
297
+ // otherwise, this would only be the case if addRule() reduced T.[P].W
298
+ // into T.W without immediately reducing some subterm of T first.
241
299
//
242
300
// While completion will eventually simplify all such rules down into
243
301
// property rules, their existance in the first place breaks subtle
0 commit comments