From 891d22b3defde24bfd8711c8aff7261a2cfbc57a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 22 Oct 2013 15:52:24 -0700 Subject: [PATCH] feat(kernel/context): add method for remove context entries at positions [s, s+n). Signed-off-by: Leonardo de Moura --- src/kernel/context.cpp | 16 ++++++++++++++++ src/kernel/context.h | 6 ++++++ 2 files changed, 22 insertions(+) diff --git a/src/kernel/context.cpp b/src/kernel/context.cpp index 33a5904fe..14da07abc 100644 --- a/src/kernel/context.cpp +++ b/src/kernel/context.cpp @@ -30,4 +30,20 @@ context_entry const & context::lookup(unsigned i) const { } throw exception("unknown free variable"); } + +static list remove_core(list 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)); +} } diff --git a/src/kernel/context.h b/src/kernel/context.h index 0f182d6d6..0963e7e91 100644 --- a/src/kernel/context.h +++ b/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; }; /**