Skip to content

Commit f32b545

Browse files
slavapestovslavapestov
committed
RequirementMachine: Move RewriteSystem::processTypeDifference() and friends from PropertyUnification.cpp to RewriteSystem.cpp
1 parent 12ba9bf commit f32b545

File tree

2 files changed

+192
-191
lines changed

2 files changed

+192
-191
lines changed

‎lib/AST/RequirementMachine/PropertyUnification.cpp

Lines changed: 0 additions & 191 deletions
Original file line numberDiff line numberDiff line change
@@ -364,197 +364,6 @@ void PropertyMap::addSuperclassProperty(
364364
}
365365
}
366366

367-
/// Given a rule (V.[LHS] => V) and a rewrite path (T.[RHS] => T) where
368-
/// T == U.V, build a rewrite path from T.[RHS] to T.[LHS].
369-
void RewriteSystem::buildRewritePathForUnifier(Term key,
370-
unsigned lhsRuleID,
371-
const RewritePath &rhsPath,
372-
RewritePath *path) const {
373-
unsigned lhsLength = getRule(lhsRuleID).getRHS().size();
374-
unsigned lhsPrefix = key.size() - lhsLength;
375-
376-
path->append(rhsPath);
377-
378-
// Apply the inverted rule U.(V => V.[LHS]).
379-
path->add(RewriteStep::forRewriteRule(
380-
/*startOffset=*/lhsPrefix, /*endOffset=*/0,
381-
/*ruleID=*/lhsRuleID, /*inverse=*/true));
382-
383-
// If the rule was actually (V.[LHS] => V) with T == U.V for some
384-
// |U| > 0, prefix each substitution of [LHS] with U.
385-
if (lhsPrefix > 0) {
386-
path->add(RewriteStep::forPrefixSubstitutions(/*prefix=*/lhsPrefix,
387-
/*endOffset=*/0,
388-
/*inverse=*/false));
389-
}
390-
}
391-
392-
/// Build a rewrite path for a rule induced by concrete type unification.
393-
///
394-
/// Consider two concrete type rules (T.[LHS] => T) and (T.[RHS] => T), a
395-
/// TypeDifference describing the transformation from LHS to RHS, and the
396-
/// index of a substitution Xn from [C] which is transformed into its
397-
/// replacement f(Xn).
398-
///
399-
/// The rewrite path should allow us to eliminate the induced rule
400-
/// (f(Xn) => Xn), so the induced rule will appear without context, and
401-
/// the concrete type rules (T.[LHS] => T) and (T.[RHS] => T) will appear
402-
/// in context.
403-
///
404-
/// There are two cases:
405-
///
406-
/// a) The substitution Xn remains a type parameter in [RHS], but becomes
407-
/// a canonical term Xn', so f(Xn) = Xn'.
408-
///
409-
/// In the first case, the induced rule (Xn => Xn'), described by a
410-
/// rewrite path as follows:
411-
///
412-
/// Xn
413-
/// Xn' T.[RHS] // RightConcreteProjection(n) pushes T.[RHS]
414-
/// Xn' T // Application of (T.[RHS] => T) in context
415-
/// Xn' T.[LHS] // Application of (T => T.[LHS]) in context
416-
/// Xn' // LeftConcreteProjection(n) pops T.[LHS]
417-
///
418-
/// Now when this path is composed with a rewrite step for the inverted
419-
/// induced rule (Xn' => Xn), we get a rewrite loop at Xn in which the
420-
/// new rule appears in empty context.
421-
///
422-
/// b) The substitution Xn becomes a concrete type [D] in [C'], so
423-
/// f(Xn) = Xn.[D].
424-
///
425-
/// In the second case, the induced rule is (Xn.[D] => Xn), described
426-
/// by a rewrite path (going in the other direction) as follows:
427-
///
428-
/// Xn
429-
/// Xn.[D] T.[RHS] // RightConcreteProjection(n) pushes T.[RHS]
430-
/// Xn.[D] T // Application of (T.[RHS] => T) in context
431-
/// Xn.[D] T.[LHS] // Application of (T => T.[LHS]) in context
432-
/// Xn.[D] // LeftConcreteProjection(n) pops T.[LHS]
433-
///
434-
/// Now when this path is composed with a rewrite step for the induced
435-
/// rule (Xn.[D] => Xn), we get a rewrite loop at Xn in which the
436-
/// new rule appears in empty context.
437-
///
438-
/// There is a minor complication; the concrete type rules T.[LHS] and
439-
/// T.[RHS] might actually be T.[LHS] and V.[RHS] where V is a suffix of
440-
/// T, so T = U.V for some |U| > 0, (or vice versa). In this case we need
441-
/// an additional step in the middle to prefix the concrete substitutions
442-
/// of [LHS] (or [LHS]) with U.
443-
static void buildRewritePathForInducedRule(Term key,
444-
unsigned differenceID,
445-
unsigned lhsRuleID,
446-
const RewritePath &rhsPath,
447-
unsigned substitutionIndex,
448-
const RewriteSystem &system,
449-
RewritePath *path) {
450-
// Replace f(Xn) with Xn and push T.[RHS] on the stack.
451-
path->add(RewriteStep::forRightConcreteProjection(
452-
differenceID, substitutionIndex, /*inverse=*/false));
453-
454-
system.buildRewritePathForUnifier(key, lhsRuleID, rhsPath, path);
455-
456-
// Pop T.[LHS] from the stack, leaving behind Xn.
457-
path->add(RewriteStep::forLeftConcreteProjection(
458-
differenceID, substitutionIndex, /*inverse=*/true));
459-
}
460-
461-
/// Given that LHS and RHS are known to simplify to the same term, build a
462-
/// rewrite path from RHS to LHS.
463-
void RewriteSystem::buildRewritePathForJoiningTerms(MutableTerm lhsTerm,
464-
MutableTerm rhsTerm,
465-
RewritePath *path) const {
466-
(void) simplify(rhsTerm, path);
467-
468-
RewritePath lhsPath;
469-
(void) simplify(lhsTerm, &lhsPath);
470-
lhsPath.invert();
471-
472-
path->append(lhsPath);
473-
474-
assert(lhsTerm == rhsTerm);
475-
}
476-
477-
/// Given two concrete type rules (T.[LHS] => T) and (T.[RHS] => T) and
478-
/// TypeDifference describing the transformation from LHS to RHS,
479-
/// record rules for transforming each substitution of LHS into a
480-
/// more canonical type parameter or concrete type from RHS.
481-
///
482-
/// This also records rewrite paths relating induced rules to the original
483-
/// concrete type rules, since the concrete type rules imply the induced
484-
/// rules and make them redundant.
485-
///
486-
/// Finally, builds a rewrite loop relating the two concrete type rules
487-
/// via the induced rules.
488-
void RewriteSystem::processTypeDifference(const TypeDifference &difference,
489-
unsigned differenceID,
490-
unsigned lhsRuleID,
491-
const RewritePath &rhsPath) {
492-
bool debug = Debug.contains(DebugFlags::ConcreteUnification);
493-
494-
if (debug) {
495-
difference.dump(llvm::dbgs());
496-
}
497-
498-
RewritePath unificationPath;
499-
500-
auto substitutions = difference.LHS.getSubstitutions();
501-
502-
// The term is at the top of the primary stack. Push all substitutions onto
503-
// the primary stack.
504-
unificationPath.add(RewriteStep::forDecompose(substitutions.size(),
505-
/*inverse=*/false));
506-
507-
// Move all substitutions but the first one to the secondary stack.
508-
for (unsigned i = 1; i < substitutions.size(); ++i)
509-
unificationPath.add(RewriteStep::forShift(/*inverse=*/false));
510-
511-
for (unsigned index : indices(substitutions)) {
512-
// Move the next substitution from the secondary stack to the primary stack.
513-
if (index != 0)
514-
unificationPath.add(RewriteStep::forShift(/*inverse=*/true));
515-
516-
auto lhsTerm = difference.getReplacementSubstitution(index);
517-
auto rhsTerm = difference.getOriginalSubstitution(index);
518-
519-
RewritePath inducedRulePath;
520-
buildRewritePathForInducedRule(difference.BaseTerm, differenceID,
521-
lhsRuleID, rhsPath, index,
522-
*this, &inducedRulePath);
523-
524-
if (debug) {
525-
llvm::dbgs() << "%% Induced rule " << lhsTerm
526-
<< " => " << rhsTerm << " with path ";
527-
inducedRulePath.dump(llvm::dbgs(), lhsTerm, *this);
528-
llvm::dbgs() << "\n";
529-
}
530-
531-
addRule(lhsTerm, rhsTerm, &inducedRulePath);
532-
buildRewritePathForJoiningTerms(lhsTerm, rhsTerm, &unificationPath);
533-
}
534-
535-
// All simplified substitutions are now on the primary stack. Collect them to
536-
// produce the new term.
537-
unificationPath.add(RewriteStep::forDecomposeConcrete(differenceID,
538-
/*inverse=*/true));
539-
540-
// We now have a unification path from T.[RHS] to T.[LHS] using the
541-
// newly-recorded induced rules. Close the loop with a path from
542-
// T.[RHS] to R.[LHS] via the concrete type rules being unified.
543-
buildRewritePathForUnifier(difference.BaseTerm, lhsRuleID, rhsPath,
544-
&unificationPath);
545-
546-
// Record a rewrite loop at T.[LHS].
547-
MutableTerm basepoint(difference.BaseTerm);
548-
basepoint.add(difference.LHS);
549-
recordRewriteLoop(basepoint, unificationPath);
550-
551-
// Optimization: If the LHS rule applies to the entire base term and not
552-
// a suffix, mark it substitution-simplified so that we can skip recording
553-
// the same rewrite loop in concretelySimplifyLeftHandSideSubstitutions().
554-
auto &lhsRule = getRule(lhsRuleID);
555-
if (lhsRule.getRHS() == difference.BaseTerm)
556-
lhsRule.markSubstitutionSimplified();
557-
}
558367

559368
/// Utility used by addSuperclassProperty() and addConcreteTypeProperty().
560369
void PropertyMap::unifyConcreteTypes(

‎lib/AST/RequirementMachine/SimplifySubstitutions.cpp

Lines changed: 192 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,198 @@
1616
using namespace swift;
1717
using namespace rewriting;
1818

19+
/// Given a rule (V.[LHS] => V) and a rewrite path (T.[RHS] => T) where
20+
/// T == U.V, build a rewrite path from T.[RHS] to T.[LHS].
21+
void RewriteSystem::buildRewritePathForUnifier(Term key,
22+
unsigned lhsRuleID,
23+
const RewritePath &rhsPath,
24+
RewritePath *path) const {
25+
unsigned lhsLength = getRule(lhsRuleID).getRHS().size();
26+
unsigned lhsPrefix = key.size() - lhsLength;
27+
28+
path->append(rhsPath);
29+
30+
// Apply the inverted rule U.(V => V.[LHS]).
31+
path->add(RewriteStep::forRewriteRule(
32+
/*startOffset=*/lhsPrefix, /*endOffset=*/0,
33+
/*ruleID=*/lhsRuleID, /*inverse=*/true));
34+
35+
// If the rule was actually (V.[LHS] => V) with T == U.V for some
36+
// |U| > 0, prefix each substitution of [LHS] with U.
37+
if (lhsPrefix > 0) {
38+
path->add(RewriteStep::forPrefixSubstitutions(/*prefix=*/lhsPrefix,
39+
/*endOffset=*/0,
40+
/*inverse=*/false));
41+
}
42+
}
43+
44+
/// Build a rewrite path for a rule induced by concrete type unification.
45+
///
46+
/// Consider two concrete type rules (T.[LHS] => T) and (T.[RHS] => T), a
47+
/// TypeDifference describing the transformation from LHS to RHS, and the
48+
/// index of a substitution Xn from [C] which is transformed into its
49+
/// replacement f(Xn).
50+
///
51+
/// The rewrite path should allow us to eliminate the induced rule
52+
/// (f(Xn) => Xn), so the induced rule will appear without context, and
53+
/// the concrete type rules (T.[LHS] => T) and (T.[RHS] => T) will appear
54+
/// in context.
55+
///
56+
/// There are two cases:
57+
///
58+
/// a) The substitution Xn remains a type parameter in [RHS], but becomes
59+
/// a canonical term Xn', so f(Xn) = Xn'.
60+
///
61+
/// In the first case, the induced rule (Xn => Xn'), described by a
62+
/// rewrite path as follows:
63+
///
64+
/// Xn
65+
/// Xn' T.[RHS] // RightConcreteProjection(n) pushes T.[RHS]
66+
/// Xn' T // Application of (T.[RHS] => T) in context
67+
/// Xn' T.[LHS] // Application of (T => T.[LHS]) in context
68+
/// Xn' // LeftConcreteProjection(n) pops T.[LHS]
69+
///
70+
/// Now when this path is composed with a rewrite step for the inverted
71+
/// induced rule (Xn' => Xn), we get a rewrite loop at Xn in which the
72+
/// new rule appears in empty context.
73+
///
74+
/// b) The substitution Xn becomes a concrete type [D] in [C'], so
75+
/// f(Xn) = Xn.[D].
76+
///
77+
/// In the second case, the induced rule is (Xn.[D] => Xn), described
78+
/// by a rewrite path (going in the other direction) as follows:
79+
///
80+
/// Xn
81+
/// Xn.[D] T.[RHS] // RightConcreteProjection(n) pushes T.[RHS]
82+
/// Xn.[D] T // Application of (T.[RHS] => T) in context
83+
/// Xn.[D] T.[LHS] // Application of (T => T.[LHS]) in context
84+
/// Xn.[D] // LeftConcreteProjection(n) pops T.[LHS]
85+
///
86+
/// Now when this path is composed with a rewrite step for the induced
87+
/// rule (Xn.[D] => Xn), we get a rewrite loop at Xn in which the
88+
/// new rule appears in empty context.
89+
///
90+
/// There is a minor complication; the concrete type rules T.[LHS] and
91+
/// T.[RHS] might actually be T.[LHS] and V.[RHS] where V is a suffix of
92+
/// T, so T = U.V for some |U| > 0, (or vice versa). In this case we need
93+
/// an additional step in the middle to prefix the concrete substitutions
94+
/// of [LHS] (or [LHS]) with U.
95+
static void buildRewritePathForInducedRule(Term key,
96+
unsigned differenceID,
97+
unsigned lhsRuleID,
98+
const RewritePath &rhsPath,
99+
unsigned substitutionIndex,
100+
const RewriteSystem &system,
101+
RewritePath *path) {
102+
// Replace f(Xn) with Xn and push T.[RHS] on the stack.
103+
path->add(RewriteStep::forRightConcreteProjection(
104+
differenceID, substitutionIndex, /*inverse=*/false));
105+
106+
system.buildRewritePathForUnifier(key, lhsRuleID, rhsPath, path);
107+
108+
// Pop T.[LHS] from the stack, leaving behind Xn.
109+
path->add(RewriteStep::forLeftConcreteProjection(
110+
differenceID, substitutionIndex, /*inverse=*/true));
111+
}
112+
113+
/// Given that LHS and RHS are known to simplify to the same term, build a
114+
/// rewrite path from RHS to LHS.
115+
void RewriteSystem::buildRewritePathForJoiningTerms(MutableTerm lhsTerm,
116+
MutableTerm rhsTerm,
117+
RewritePath *path) const {
118+
(void) simplify(rhsTerm, path);
119+
120+
RewritePath lhsPath;
121+
(void) simplify(lhsTerm, &lhsPath);
122+
lhsPath.invert();
123+
124+
path->append(lhsPath);
125+
126+
assert(lhsTerm == rhsTerm);
127+
}
128+
129+
/// Given two concrete type rules (T.[LHS] => T) and (T.[RHS] => T) and
130+
/// TypeDifference describing the transformation from LHS to RHS,
131+
/// record rules for transforming each substitution of LHS into a
132+
/// more canonical type parameter or concrete type from RHS.
133+
///
134+
/// This also records rewrite paths relating induced rules to the original
135+
/// concrete type rules, since the concrete type rules imply the induced
136+
/// rules and make them redundant.
137+
///
138+
/// Finally, builds a rewrite loop relating the two concrete type rules
139+
/// via the induced rules.
140+
void RewriteSystem::processTypeDifference(const TypeDifference &difference,
141+
unsigned differenceID,
142+
unsigned lhsRuleID,
143+
const RewritePath &rhsPath) {
144+
bool debug = Debug.contains(DebugFlags::ConcreteUnification);
145+
146+
if (debug) {
147+
difference.dump(llvm::dbgs());
148+
}
149+
150+
RewritePath unificationPath;
151+
152+
auto substitutions = difference.LHS.getSubstitutions();
153+
154+
// The term is at the top of the primary stack. Push all substitutions onto
155+
// the primary stack.
156+
unificationPath.add(RewriteStep::forDecompose(substitutions.size(),
157+
/*inverse=*/false));
158+
159+
// Move all substitutions but the first one to the secondary stack.
160+
for (unsigned i = 1; i < substitutions.size(); ++i)
161+
unificationPath.add(RewriteStep::forShift(/*inverse=*/false));
162+
163+
for (unsigned index : indices(substitutions)) {
164+
// Move the next substitution from the secondary stack to the primary stack.
165+
if (index != 0)
166+
unificationPath.add(RewriteStep::forShift(/*inverse=*/true));
167+
168+
auto lhsTerm = difference.getReplacementSubstitution(index);
169+
auto rhsTerm = difference.getOriginalSubstitution(index);
170+
171+
RewritePath inducedRulePath;
172+
buildRewritePathForInducedRule(difference.BaseTerm, differenceID,
173+
lhsRuleID, rhsPath, index,
174+
*this, &inducedRulePath);
175+
176+
if (debug) {
177+
llvm::dbgs() << "%% Induced rule " << lhsTerm
178+
<< " => " << rhsTerm << " with path ";
179+
inducedRulePath.dump(llvm::dbgs(), lhsTerm, *this);
180+
llvm::dbgs() << "\n";
181+
}
182+
183+
addRule(lhsTerm, rhsTerm, &inducedRulePath);
184+
buildRewritePathForJoiningTerms(lhsTerm, rhsTerm, &unificationPath);
185+
}
186+
187+
// All simplified substitutions are now on the primary stack. Collect them to
188+
// produce the new term.
189+
unificationPath.add(RewriteStep::forDecomposeConcrete(differenceID,
190+
/*inverse=*/true));
191+
192+
// We now have a unification path from T.[RHS] to T.[LHS] using the
193+
// newly-recorded induced rules. Close the loop with a path from
194+
// T.[RHS] to R.[LHS] via the concrete type rules being unified.
195+
buildRewritePathForUnifier(difference.BaseTerm, lhsRuleID, rhsPath,
196+
&unificationPath);
197+
198+
// Record a rewrite loop at T.[LHS].
199+
MutableTerm basepoint(difference.BaseTerm);
200+
basepoint.add(difference.LHS);
201+
recordRewriteLoop(basepoint, unificationPath);
202+
203+
// Optimization: If the LHS rule applies to the entire base term and not
204+
// a suffix, mark it substitution-simplified so that we can skip recording
205+
// the same rewrite loop in concretelySimplifyLeftHandSideSubstitutions().
206+
auto &lhsRule = getRule(lhsRuleID);
207+
if (lhsRule.getRHS() == difference.BaseTerm)
208+
lhsRule.markSubstitutionSimplified();
209+
}
210+
19211
/// Simplify terms appearing in the substitutions of the last symbol of \p term,
20212
/// which must be a superclass or concrete type symbol.
21213
///

0 commit comments

Comments
 (0)