@@ -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 existence 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
@@ -212,8 +270,56 @@ RewriteSystem::computeCriticalPair(ArrayRef<Symbol>::const_iterator from,
212
270
return false ;
213
271
}
214
272
215
- // Add the pair (XV, TY).
216
- pairs.emplace_back (xv, ty, path);
273
+ // If Y == UW for some W, then the critical pair is (XV, TUW),
274
+ // and we have
275
+ // - lhs == (TU -> X)
276
+ // - rhs == (UV -> UW).
277
+ //
278
+ // We explicitly apply the rewrite step (TU => X) to the rewrite path,
279
+ // transforming the critical pair to (XV, XW).
280
+ //
281
+ // In particular, if T == X, U == [P] for some protocol P, and
282
+ // V == W.[p] for some property symbol p, then we in fact have a pair
283
+ // of property rules:
284
+ //
285
+ // - lhs == (T.[P] => T)
286
+ // - rhs == ([P].W.[p] => [P].W)
287
+ //
288
+ // Without this hack, the critical pair would be:
289
+ //
290
+ // (T.W.[p] => T.[P].W)
291
+ //
292
+ // With this hack, the critical pair becomes:
293
+ //
294
+ // (T.W.[p] => T.W)
295
+ //
296
+ // This ensures that the newly-added rule is itself a property rule;
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.
299
+ //
300
+ // While completion will eventually simplify all such rules down into
301
+ // property rules, their existence in the first place breaks subtle
302
+ // invariants in the minimal conformances algorithm, which expects
303
+ // homotopy generators describing redundant protocol conformance rules
304
+ // to have a certain structure.
305
+ if (lhs.getLHS ().size () <= ty.size () &&
306
+ std::equal (lhs.getLHS ().begin (),
307
+ lhs.getLHS ().end (),
308
+ ty.begin ())) {
309
+ unsigned endOffset = ty.size () - lhs.getLHS ().size ();
310
+ path.add (RewriteStep::forRewriteRule (/* startOffset=*/ 0 ,
311
+ endOffset,
312
+ getRuleID (lhs),
313
+ /* inverse=*/ false ));
314
+
315
+ // Compute the term XW.
316
+ MutableTerm xw (lhs.getRHS ());
317
+ xw.append (ty.end () - endOffset, ty.end ());
318
+
319
+ pairs.emplace_back (xv, xw, path);
320
+ } else {
321
+ pairs.emplace_back (xv, ty, path);
322
+ }
217
323
}
218
324
219
325
return true ;
@@ -241,7 +347,7 @@ RewriteSystem::computeConfluentCompletion(unsigned maxRuleCount,
241
347
assert (!Minimized);
242
348
assert (!Frozen);
243
349
244
- // ' Complete' might already be set, if we're re-running completion after
350
+ // Complete might already be set, if we're re-running completion after
245
351
// adding new rules in the property map's concrete type unification procedure.
246
352
Complete = 1 ;
247
353
@@ -253,7 +359,7 @@ RewriteSystem::computeConfluentCompletion(unsigned maxRuleCount,
253
359
do {
254
360
ruleCount = Rules.size ();
255
361
256
- // For every rule, look for other rules that overlap with this rule.
362
+ // For every rule, looking for other rules that overlap with this rule.
257
363
for (unsigned i = FirstLocalRule, e = Rules.size (); i < e; ++i) {
258
364
const auto &lhs = getRule (i);
259
365
if (lhs.isLHSSimplified () ||
0 commit comments