feat(kernel/expr): add is_contextual binder info

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

src/kernel/expr.h

@@ -221,12 +221,15 @@ public:
    is only used for elaboration.
 */
 class expr_binder_info {
-    bool m_implicit; //! if true, binder argument is an implicit argument
-    bool m_cast;     //! if true, binder argument is a target for using cast
+    unsigned m_implicit:1;   //! if true, binder argument is an implicit argument
+    unsigned m_cast:1;       //! if true, binder argument is a target for using cast
+    unsigned m_contextual:1; //! if true, binder argument is assumed to be part of the context, and may be argument for metavariables.
 public:
-    expr_binder_info(bool implicit = false, bool cast = false):m_implicit(implicit), m_cast(cast) {}
+    expr_binder_info(bool implicit = false, bool cast = false, bool contextual = true):
+        m_implicit(implicit), m_cast(cast), m_contextual(contextual) {}
     bool is_implicit() const { return m_implicit; }
     bool is_cast() const { return m_cast; }
+    bool is_contextual() const { return m_contextual; }
 };
 
 /** \brief Super class for lambda and pi */

src/library/kernel_bindings.cpp

@@ -178,15 +178,19 @@ static int mk_binder_info(lua_State * L) {
         return push_expr_binder_info(L, expr_binder_info());
     else if (nargs == 1)
         return push_expr_binder_info(L, expr_binder_info(lua_toboolean(L, 1)));
-    else
+    else if (nargs == 2)
         return push_expr_binder_info(L, expr_binder_info(lua_toboolean(L, 1), lua_toboolean(L, 2)));
+    else
+        return push_expr_binder_info(L, expr_binder_info(lua_toboolean(L, 1), lua_toboolean(L, 2), lua_toboolean(L, 3)));
 }
 static int binder_info_is_implicit(lua_State * L) { return push_boolean(L, to_expr_binder_info(L, 1).is_implicit()); }
 static int binder_info_is_cast(lua_State * L) { return push_boolean(L, to_expr_binder_info(L, 1).is_cast()); }
+static int binder_info_is_contextual(lua_State * L) { return push_boolean(L, to_expr_binder_info(L, 1).is_contextual()); }
 static const struct luaL_Reg binder_info_m[] = {
     {"__gc",            expr_binder_info_gc},
     {"is_implicit",     safe_function<binder_info_is_implicit>},
     {"is_cast",         safe_function<binder_info_is_cast>},
+    {"is_contextual",   safe_function<binder_info_is_contextual>},
     {0, 0}
 };
 static void open_binder_info(lua_State * L) {

tests/lua/expr1.lua

@@ -6,4 +6,7 @@ assert(binder_info(true):is_implicit())
 assert(not binder_info(true):is_cast())
 assert(binder_info(true, true):is_implicit())
 assert(binder_info(true, true):is_cast())
+assert(binder_info():is_contextual())
+assert(not binder_info(true, true, false):is_contextual())
+assert(binder_info(false, false, true):is_contextual())