feat(kernel/context): add method for remove context entries at positions [s, s+n).

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/kernel/context.cpp

@@ -30,4 +30,20 @@ context_entry const & context::lookup(unsigned i) const {
     }
     throw exception("unknown free variable");
 }
+
+static list<context_entry> remove_core(list<context_entry> const & l, unsigned s, unsigned n) {
+    if (s == 0) {
+        if (n > 0) {
+            return remove_core(tail(l), 0, n-1);
+        } else {
+            return l;
+        }
+    } else {
+        return cons(head(l), remove_core(tail(l), s-1, n));
+    }
+}
+
+context context::remove(unsigned s, unsigned n) const {
+    return context(remove_core(m_list, s, n));
+}
 }

src/kernel/context.h

@@ -45,6 +45,12 @@ public:
     iterator begin() const { return m_list.begin(); }
     iterator end() const { return m_list.end(); }
     friend bool is_eqp(context const & c1, context const & c2) { return is_eqp(c1.m_list, c2.m_list); }
+    /**
+       \brief Return a new context where the entries at positions [s, s+n) were removed.
+
+       \pre size() >= s + n
+    */
+    context remove(unsigned s, unsigned n) const;
 };
 
 /**