Skip to content

Commit 6064671

Browse files
slavapestovslavapestov
committed
RequirementMachine: Replace RewriteStep::ConcreteTypeWitness with relations
1 parent 84e2a62 commit 6064671

File tree

7 files changed

+52
-99
lines changed

7 files changed

+52
-99
lines changed

‎lib/AST/RequirementMachine/HomotopyReduction.cpp

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -98,7 +98,6 @@ RewriteLoop::findRulesAppearingOnceInEmptyContext(
9898
case RewriteStep::Shift:
9999
case RewriteStep::Decompose:
100100
case RewriteStep::Relation:
101-
case RewriteStep::ConcreteTypeWitness:
102101
case RewriteStep::SameTypeWitness:
103102
break;
104103
}
@@ -219,7 +218,6 @@ RewritePath RewritePath::splitCycleAtRule(unsigned ruleID) const {
219218
case RewriteStep::Shift:
220219
case RewriteStep::Decompose:
221220
case RewriteStep::Relation:
222-
case RewriteStep::ConcreteTypeWitness:
223221
case RewriteStep::SameTypeWitness:
224222
break;
225223
}
@@ -318,7 +316,6 @@ bool RewritePath::replaceRuleWithPath(unsigned ruleID,
318316
case RewriteStep::Shift:
319317
case RewriteStep::Decompose:
320318
case RewriteStep::Relation:
321-
case RewriteStep::ConcreteTypeWitness:
322319
case RewriteStep::SameTypeWitness:
323320
newSteps.push_back(step);
324321
break;

‎lib/AST/RequirementMachine/MinimalConformances.cpp

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -138,7 +138,6 @@ void RewriteLoop::findProtocolConformanceRules(
138138
case RewriteStep::Shift:
139139
case RewriteStep::Decompose:
140140
case RewriteStep::Relation:
141-
case RewriteStep::ConcreteTypeWitness:
142141
case RewriteStep::SameTypeWitness:
143142
break;
144143
}

‎lib/AST/RequirementMachine/PropertyRelations.cpp

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -90,6 +90,34 @@ unsigned RewriteSystem::recordConcreteConformanceRelation(
9090
Term::get(rhsTerm, Context));
9191
}
9292

93+
/// Record a relation ([concrete: C : P].[P:X].[concrete: C.X] =>
94+
/// [concrete: C : P].[P:X]) which "concretizes" a nested type C.X of a
95+
/// type parameter conforming to P known to equal the concrete type C.
96+
unsigned RewriteSystem::recordConcreteTypeWitnessRelation(
97+
Symbol concreteConformanceSymbol,
98+
Symbol associatedTypeSymbol,
99+
Symbol typeWitnessSymbol) {
100+
assert(concreteConformanceSymbol.getKind() ==
101+
Symbol::Kind::ConcreteConformance);
102+
assert(associatedTypeSymbol.getKind() ==
103+
Symbol::Kind::AssociatedType);
104+
assert(associatedTypeSymbol.getProtocols().size() == 1);
105+
assert(concreteConformanceSymbol.getProtocol() ==
106+
associatedTypeSymbol.getProtocols()[0]);
107+
assert(typeWitnessSymbol.getKind() == Symbol::Kind::ConcreteType);
108+
109+
MutableTerm rhsTerm;
110+
rhsTerm.add(concreteConformanceSymbol);
111+
rhsTerm.add(associatedTypeSymbol);
112+
113+
MutableTerm lhsTerm(rhsTerm);
114+
lhsTerm.add(typeWitnessSymbol);
115+
116+
return recordRelation(
117+
Term::get(lhsTerm, Context),
118+
Term::get(rhsTerm, Context));
119+
}
120+
93121
RewriteSystem::TypeWitness::TypeWitness(
94122
Term lhs, llvm::PointerUnion<Symbol, Term> rhs)
95123
: LHS(lhs), RHS(rhs) {

‎lib/AST/RequirementMachine/PropertyUnification.cpp

Lines changed: 16 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -898,6 +898,15 @@ MutableTerm PropertyMap::computeConstraintTermForTypeWitness(
898898
typeWitnessSymbol);
899899
unsigned witnessID = System.recordTypeWitness(witness);
900900

901+
auto concreteConformanceSymbol = *(subjectType.end() - 2);
902+
auto associatedTypeSymbol = *(subjectType.end() - 1);
903+
904+
// Record the relation before simplifying typeWitnessSymbol below.
905+
unsigned relationID = System.recordConcreteTypeWitnessRelation(
906+
concreteConformanceSymbol,
907+
associatedTypeSymbol,
908+
typeWitnessSymbol);
909+
901910
// Simplify the substitution terms in the type witness symbol.
902911
RewritePath substPath;
903912
System.simplifySubstitutions(typeWitnessSymbol, &substPath);
@@ -914,7 +923,7 @@ MutableTerm PropertyMap::computeConstraintTermForTypeWitness(
914923

915924
// Add a rule T.[concrete: C : P] => T.[concrete: C : P].[P:X].
916925
MutableTerm result(key);
917-
result.add(witness.getConcreteConformance());
926+
result.add(concreteConformanceSymbol);
918927

919928
// ([concrete: C : P] => [concrete: C : P].[P:X].[concrete: C])
920929
path.add(RewriteStep::forSameTypeWitness(
@@ -924,8 +933,9 @@ MutableTerm PropertyMap::computeConstraintTermForTypeWitness(
924933
path.append(substPath);
925934

926935
// T.([concrete: C : P].[P:X].[concrete: C.X] => [concrete: C : P].[P:X])
927-
path.add(RewriteStep::forConcreteTypeWitness(
928-
witnessID, /*inverse=*/false));
936+
path.add(RewriteStep::forRelation(
937+
/*startOffset=*/key.size(), relationID,
938+
/*inverse=*/false));
929939

930940
return result;
931941
}
@@ -944,8 +954,9 @@ MutableTerm PropertyMap::computeConstraintTermForTypeWitness(
944954
path.append(substPath);
945955

946956
// T.([concrete: C : P].[P:X].[concrete: C.X] => [concrete: C : P].[P:X])
947-
path.add(RewriteStep::forConcreteTypeWitness(
948-
witnessID, /*inverse=*/false));
957+
path.add(RewriteStep::forRelation(
958+
/*startOffset=*/key.size(), relationID,
959+
/*inverse=*/false));
949960

950961
return constraintType;
951962
}

‎lib/AST/RequirementMachine/RewriteLoop.cpp

Lines changed: 0 additions & 69 deletions
Original file line numberDiff line numberDiff line change
@@ -79,13 +79,6 @@ void RewriteStep::dump(llvm::raw_ostream &out,
7979

8080
break;
8181
}
82-
case ConcreteTypeWitness: {
83-
evaluator.applyConcreteTypeWitness(*this, system);
84-
85-
out << (Inverse ? "ConcreteTypeWitness⁻¹"
86-
: "ConcreteTypeWitness");
87-
break;
88-
}
8982
case SameTypeWitness: {
9083
evaluator.applySameTypeWitness(*this, system);
9184

@@ -389,64 +382,6 @@ RewritePathEvaluator::applyRelation(const RewriteStep &step,
389382
return {lhs, rhs, prefix, suffix};
390383
}
391384

392-
void RewritePathEvaluator::applyConcreteTypeWitness(const RewriteStep &step,
393-
const RewriteSystem &system) {
394-
checkPrimary();
395-
auto &term = Primary.back();
396-
397-
const auto &witness = system.getTypeWitness(step.Arg);
398-
auto fail = [&]() {
399-
llvm::errs() << "Bad concrete type witness term:\n";
400-
llvm::errs() << term << "\n\n";
401-
witness.dump(llvm::errs());
402-
llvm::errs() << "End offset: " << step.EndOffset << "\n";
403-
llvm::errs() << "Inverse: " << step.Inverse << "\n";
404-
abort();
405-
};
406-
407-
if (!step.Inverse) {
408-
// Make sure the term takes the following form, where |V| == EndOffset:
409-
//
410-
// U.[concrete: C : P].[P:X].[concrete: C.X].V
411-
if (term.size() <= step.EndOffset + 3 ||
412-
*(term.end() - step.EndOffset - 3) != witness.getConcreteConformance() ||
413-
*(term.end() - step.EndOffset - 2) != witness.getAssocType() ||
414-
*(term.end() - step.EndOffset - 1) != witness.getConcreteType()) {
415-
fail();
416-
}
417-
418-
// Get the subterm U.[concrete: C : P].[P:X].
419-
MutableTerm newTerm(term.begin(), term.end() - step.EndOffset - 1);
420-
421-
// Add the subterm V, to get U.[concrete: C : P].[P:X].V.
422-
newTerm.append(term.end() - step.EndOffset, term.end());
423-
424-
term = newTerm;
425-
} else {
426-
// Make sure the term takes the following form, where |V| == EndOffset:
427-
//
428-
// U.[concrete: C : P].[P:X].V
429-
if (term.size() <= step.EndOffset + 2 ||
430-
*(term.end() - step.EndOffset - 2) != witness.getConcreteConformance() ||
431-
*(term.end() - step.EndOffset - 1) != witness.getAssocType()) {
432-
fail();
433-
}
434-
435-
// Get the subterm U.[concrete: C : P].[P:X].
436-
MutableTerm newTerm(term.begin(), term.end() - step.EndOffset);
437-
438-
// Add the symbol [concrete: C.X].
439-
newTerm.add(witness.getConcreteType());
440-
441-
// Add the subterm V, to get
442-
//
443-
// U.[concrete: C : P].[P:X].[concrete: C.X].V
444-
newTerm.append(term.end() - step.EndOffset, term.end());
445-
446-
term = newTerm;
447-
}
448-
}
449-
450385
void RewritePathEvaluator::applySameTypeWitness(const RewriteStep &step,
451386
const RewriteSystem &system) {
452387
checkPrimary();
@@ -542,10 +477,6 @@ void RewritePathEvaluator::apply(const RewriteStep &step,
542477
applyRelation(step, system);
543478
break;
544479

545-
case RewriteStep::ConcreteTypeWitness:
546-
applyConcreteTypeWitness(step, system);
547-
break;
548-
549480
case RewriteStep::SameTypeWitness:
550481
applySameTypeWitness(step, system);
551482
break;

‎lib/AST/RequirementMachine/RewriteLoop.h

Lines changed: 0 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -100,17 +100,6 @@ struct RewriteStep {
100100
/// RewriteSystem::recordRelation().
101101
Relation,
102102

103-
/// If not inverted: the top of the primary stack must be a term ending in a
104-
/// concrete conformance symbol [concrete: C : P] followed by an associated
105-
/// type symbol [P:X], and the concrete type symbol [concrete: C.X] for the
106-
/// type witness of 'X' in the conformance 'C : P'. The concrete type symbol
107-
/// is eliminated.
108-
///
109-
/// If inverted: the concrete type symbol [concrete: C.X] is introduced.
110-
///
111-
/// The Arg field stores the result of RewriteSystem::recordTypeWitness().
112-
ConcreteTypeWitness,
113-
114103
/// If not inverted: the top of the primary stack must be a term ending in a
115104
/// concrete conformance symbol [concrete: C : P] followed by an associated
116105
/// type symbol [P:X]. The associated type symbol is eliminated.
@@ -184,11 +173,6 @@ struct RewriteStep {
184173
/*arg=*/relationID, inverse);
185174
}
186175

187-
static RewriteStep forConcreteTypeWitness(unsigned witnessID, bool inverse) {
188-
return RewriteStep(ConcreteTypeWitness, /*startOffset=*/0, /*endOffset=*/0,
189-
/*arg=*/witnessID, inverse);
190-
}
191-
192176
static RewriteStep forSameTypeWitness(unsigned witnessID, bool inverse) {
193177
return RewriteStep(SameTypeWitness, /*startOffset=*/0, /*endOffset=*/0,
194178
/*arg=*/witnessID, inverse);
@@ -386,9 +370,6 @@ struct RewritePathEvaluator {
386370
void applyConcreteConformance(const RewriteStep &step,
387371
const RewriteSystem &system);
388372

389-
void applyConcreteTypeWitness(const RewriteStep &step,
390-
const RewriteSystem &system);
391-
392373
void applySameTypeWitness(const RewriteStep &step,
393374
const RewriteSystem &system);
394375

‎lib/AST/RequirementMachine/RewriteSystem.h

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -346,9 +346,15 @@ class RewriteSystem final {
346346
Relation getRelation(unsigned index) const;
347347

348348
unsigned recordRelation(Symbol lhs, Symbol rhs);
349+
349350
unsigned recordConcreteConformanceRelation(
350-
Symbol concreteSymbol, Symbol protocolSymbol,
351-
Symbol concreteConformanceSymbol);
351+
Symbol concreteSymbol, Symbol protocolSymbol,
352+
Symbol concreteConformanceSymbol);
353+
354+
unsigned recordConcreteTypeWitnessRelation(
355+
Symbol concreteConformanceSymbol,
356+
Symbol associatedTypeSymbol,
357+
Symbol typeWitnessSymbol);
352358

353359
/// A type witness has a subject type, stored in LHS, which takes the form:
354360
///

0 commit comments

Comments
 (0)