@@ -64,23 +64,38 @@ void HomotopyGenerator::findProtocolConformanceRules(
6464 &result,
6565 const RewriteSystem &system) const {
6666
67+ auto redundantRules = Path.findRulesAppearingOnceInEmptyContext ();
68+
69+ bool foundAny = false ;
70+ for (unsigned ruleID : redundantRules) {
71+ const auto &rule = system.getRule (ruleID);
72+ if (auto *proto = rule.isProtocolConformanceRule ()) {
73+ result[proto].first .push_back (ruleID);
74+ foundAny = true ;
75+ }
76+ }
77+
78+ if (!foundAny)
79+ return ;
80+
6781 MutableTerm term = Basepoint;
6882
83+ // Now look for rewrite steps with conformance rules in empty right context,
84+ // that is something like X.(Y.[P] => Z) (or it's inverse, X.(Z => Y.[P])).
6985 for (const auto &step : Path) {
7086 switch (step.Kind ) {
7187 case RewriteStep::ApplyRewriteRule: {
7288 const auto &rule = system.getRule (step.RuleID );
73- if (!rule.isProtocolConformanceRule ())
74- break ;
75-
76- auto *proto = rule.getLHS ().back ().getProtocol ();
77-
78- if (!step.isInContext ()) {
79- result[proto].first .push_back (step.RuleID );
80- } else if (step.StartOffset > 0 &&
81- step.EndOffset == 0 ) {
82- MutableTerm prefix (term.begin (), term.begin () + step.StartOffset );
83- result[proto].second .emplace_back (prefix, step.RuleID );
89+ if (auto *proto = rule.isProtocolConformanceRule ()) {
90+ if (step.StartOffset > 0 &&
91+ step.EndOffset == 0 ) {
92+ // Record the prefix term that is left unchanged by this rewrite step.
93+ //
94+ // In the above example where the rewrite step is X.(Y.[P] => Z),
95+ // the prefix term is 'X'.
96+ MutableTerm prefix (term.begin (), term.begin () + step.StartOffset );
97+ result[proto].second .emplace_back (prefix, step.RuleID );
98+ }
8499 }
85100
86101 break ;
0 commit comments