RequirementMachine: Allow MutableTerm::rewriteSubTerm() to make the term longer

I'm about to change the reduction order so that terms with more
name symbols always order after terms with fewer name symbols,
so for example

    [P].A > [P:T].[Q:U].[R:V]

This will be used to implement protocol typealiases.

Author: slavapestov

lib/AST/RequirementMachine/Term.cpp

@@ -170,36 +170,33 @@ MutableTerm::compare(const MutableTerm &other, RewriteContext &ctx) const {
   return shortlexCompare(begin(), end(), other.begin(), other.end(), ctx);
 }
 
-/// Replace the subterm in the range [from,to) with \p rhs. The subrange must
-/// be part of this term itself.
-///
-/// Note that \p rhs must precede [from,to) in the linear order on terms.
+/// Replace the subterm in the range [from,to) of this term with \p rhs.
 void MutableTerm::rewriteSubTerm(Symbol *from, Symbol *to, Term rhs) {
   auto oldSize = size();
   unsigned lhsLength = (unsigned)(to - from);
-  assert(rhs.size() <= lhsLength);
-
-  // Overwrite the occurrence of the left hand side with the
-  // right hand side.
-  auto newIter = std::copy(rhs.begin(), rhs.end(), from);
-
-  // If the right hand side is shorter than the left hand side,
-  // then newIter will point to a location before oldIter, eg
-  // if this term is 'T.A.B.C', lhs is 'A.B' and rhs is 'X',
-  // then we now have:
-  //
-  // T.X  .C
-  //       ^--- oldIter
-  //     ^--- newIter
-  //
-  // Shift everything over to close the gap (by one location,
-  // in this case).
-  if (newIter != to) {
-    auto newEnd = std::copy(to, end(), newIter);
-
-    // Now, we've moved the gap to the end of the term; close
-    // it by shortening the term.
-    Symbols.erase(newEnd, end());
+
+  if (lhsLength == rhs.size()) {
+    // Copy the RHS to the LHS.
+    auto newTo = std::copy(rhs.begin(), rhs.end(), from);
+
+    // The RHS has the same length as the LHS, so we're done.
+    assert(newTo == to);
+    (void) newTo;
+  } else if (lhsLength > rhs.size()) {
+    // Copy the RHS to the LHS.
+    auto newTo = std::copy(rhs.begin(), rhs.end(), from);
+
+    // Shorten the term.
+    Symbols.erase(newTo, to);
+  } else {
+    assert(lhsLength < rhs.size());
+
+    // Copy the LHS-sized prefix of RHS to the LHS.
+    auto newTo = std::copy(rhs.begin(), rhs.begin() + lhsLength, from);
+    assert(newTo == to);
+
+    // Insert the remainder of the RHS term.
+    Symbols.insert(to, rhs.begin() + lhsLength, rhs.end());
   }
 
   assert(size() == oldSize - lhsLength + rhs.size());