feat(kernel/context): add find, a version of lookup that does not throw an exception

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

src/kernel/context.cpp

@@ -31,6 +31,17 @@ context_entry const & context::lookup(unsigned i) const {
     throw exception("unknown free variable");
 }
 
+optional<context_entry> context::find(unsigned i) const {
+    list<context_entry> const * it1 = &m_list;
+    while (*it1) {
+        if (i == 0)
+            return some(head(*it1));
+        --i;
+        it1 = &tail(*it1);
+    }
+    return optional<context_entry>();
+}
+
 static list<context_entry> remove_core(list<context_entry> const & l, unsigned s, unsigned n) {
     if (s == 0) {
         if (n > 0) {

src/kernel/context.h

@@ -44,6 +44,8 @@ public:
     explicit context(list<context_entry> const & l):m_list(l) {}
     context_entry const & lookup(unsigned vidx) const;
     std::pair<context_entry const &, context> lookup_ext(unsigned vidx) const;
+    /** \brief Similar to lookup, but always succeed */
+    optional<context_entry> find(unsigned vidx) const;
     bool empty() const { return is_nil(m_list); }
     explicit operator bool() const { return !empty(); }
     unsigned size() const { return length(m_list); }
@@ -75,6 +77,7 @@ inline std::pair<context_entry const &, context> lookup_ext(context const & c, u
    Bruijn index \c i.
 */
 inline context_entry const & lookup(context const & c, unsigned i) { return c.lookup(i); }
+inline optional<context_entry> find(context const & c, unsigned i) { return c.find(i); }
 inline context extend(context const & c, name const & n, optional<expr> const & d, expr const & b) { return context(c, n, d, b); }
 inline context extend(context const & c, name const & n, expr const & d, optional<expr> const & b) { return context(c, n, d, b); }
 inline context extend(context const & c, name const & n, expr const & d, expr const & b) { return context(c, n, d, b); }

src/kernel/printer.cpp

@@ -99,13 +99,14 @@ struct print_expr_fn {
         case expr_kind::MetaVar:
             print_metavar(a, c);
             break;
-        case expr_kind::Var:
-            try {
-                out() << lookup(c, var_idx(a)).get_name();
-            } catch (exception & ex) {
+        case expr_kind::Var: {
+            auto e = find(c, var_idx(a));
+            if (e)
+                out() << e->get_name();
+            else
                 out() << "#" << var_idx(a);
-            }
             break;
+        }
         case expr_kind::Constant:
             out() << const_name(a);
             break;

src/library/elaborator/elaborator.cpp

@@ -513,12 +513,9 @@ class elaborator::imp {
     /** \brief Replace variables by their definition if the context contains it. */
     void process_var(context const & ctx, expr & a) {
         if (is_var(a)) {
-            try {
-                context_entry const & e = lookup(ctx, var_idx(a));
-                if (e.get_body())
-                    a = *(e.get_body());
-            } catch (exception&) {
-            }
+            auto e = find(ctx, var_idx(a));
+            if (e && e->get_body())
+                a = *(e->get_body());
         }
     }
 
@@ -652,13 +649,8 @@ class elaborator::imp {
 
     /** \brief Return true iff the variable with id \c vidx has a body/definition in the context \c ctx. */
     static bool has_body(context const & ctx, unsigned vidx) {
-        try {
-            context_entry const & e = lookup(ctx, vidx);
-            if (e.get_body())
-                return true;
-        } catch (exception&) {
-        }
-        return false;
+        auto e = find(ctx, vidx);
+        return e && e->get_body();
     }
 
     /**