@@ -200,18 +200,60 @@ bool RewriteSystem::simplify(MutableTerm &term) const {
200200 return changed;
201201}
202202
203- void RewriteSystem::simplifyRightHandSides () {
204- for (auto &rule : Rules) {
203+ // / Delete any rules whose left hand sides can be reduced by other rules,
204+ // / and reduce the right hand sides of all remaining rules as much as
205+ // / possible.
206+ // /
207+ // / Must be run after the completion procedure, since the deletion of
208+ // / rules is only valid to perform if the rewrite system is confluent.
209+ void RewriteSystem::simplifyRewriteSystem () {
210+ for (auto ruleID : indices (Rules)) {
211+ auto &rule = Rules[ruleID];
205212 if (rule.isDeleted ())
206213 continue ;
207214
215+ // First, see if the left hand side of this rule can be reduced using
216+ // some other rule.
217+ auto lhs = rule.getLHS ();
218+ auto begin = lhs.begin ();
219+ auto end = lhs.end ();
220+ while (begin < end) {
221+ if (auto otherRuleID = Trie.find (begin++, end)) {
222+ // A rule does not obsolete itself.
223+ if (*otherRuleID == ruleID)
224+ continue ;
225+
226+ // Ignore other deleted rules.
227+ if (Rules[*otherRuleID].isDeleted ())
228+ continue ;
229+
230+ if (DebugCompletion) {
231+ const auto &otherRule = Rules[ruleID];
232+ llvm::dbgs () << " $ Deleting rule " << rule << " because "
233+ << " its left hand side contains " << otherRule
234+ << " \n " ;
235+ }
236+
237+ rule.markDeleted ();
238+ break ;
239+ }
240+ }
241+
242+ // If the rule was deleted above, skip the rest.
243+ if (rule.isDeleted ())
244+ continue ;
245+
246+ // Now, try to reduce the right hand side.
208247 MutableTerm rhs (rule.getRHS ());
209248 if (!simplify (rhs))
210249 continue ;
211250
251+ // If the right hand side was further reduced, update the rule.
212252 rule = Rule (rule.getLHS (), Term::get (rhs, Context));
213253 }
254+ }
214255
256+ void RewriteSystem::verify () const {
215257#ifndef NDEBUG
216258
217259#define ASSERT_RULE (expr ) \
0 commit comments