From 1e065d495bd9706858b04545d9c9b84cee87a19c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 9 Nov 2019 12:24:34 -0800
Subject: [PATCH] feat: expose `hasLooseBVar`

---
 library/Init/Lean/Expr.lean |  3 +++
 src/kernel/expr.cpp         |  6 ++++++
 tests/lean/run/expr1.lean   | 21 +++++++++++++++++++++
 3 files changed, 30 insertions(+)

diff --git a/library/Init/Lean/Expr.lean b/library/Init/Lean/Expr.lean
index 0ae306db5c..28d899c160 100644
--- a/library/Init/Lean/Expr.lean
+++ b/library/Init/Lean/Expr.lean
@@ -319,6 +319,9 @@ constant getLooseBVarRange (e : @& Expr) : Nat := arbitrary _
 def hasLooseBVars (e : Expr) : Bool :=
 getLooseBVarRange e > 0
 
+@[extern "lean_expr_has_loose_bvar"]
+constant hasLooseBVar (e : @& Expr) (bvarIdx : @& Nat) : Bool := arbitrary _
+
 /-- Instantiate the loose bound variables in `e` using `subst`.
     That is, a loose `Expr.bvar i` is replaced with `subst[i]`. -/
 @[extern "lean_expr_instantiate"]
diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index 71828d884e..95d9bcd913 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -805,6 +805,12 @@ bool has_loose_bvar(expr const & e, unsigned i) {
     return found;
 }
 
+extern "C" uint8 lean_expr_has_loose_bvar(b_obj_arg e, b_obj_arg i) {
+    if (!lean_is_scalar(i))
+        return false;
+    return has_loose_bvar(TO_REF(expr, e), lean_unbox(i));
+}
+
 expr lower_loose_bvars(expr const & e, unsigned s, unsigned d) {
     if (d == 0 || s >= get_loose_bvar_range(e))
         return e;
diff --git a/tests/lean/run/expr1.lean b/tests/lean/run/expr1.lean
index 23f3da9833..e88d13c6bc 100644
--- a/tests/lean/run/expr1.lean
+++ b/tests/lean/run/expr1.lean
@@ -37,3 +37,24 @@ do let f   := Expr.const `f [];
    pure ()
 
 #eval tst3
+
+
+def tst4 : IO Unit :=
+do let f   := Expr.const `f [];
+   let a   := Expr.const `a [];
+   let b   := Expr.const `b [];
+   let x0   := Expr.bvar 0;
+   let x1   := Expr.bvar 1;
+   let t1   := mkApp f #[a, b];
+   let t2   := mkApp f #[a, x0];
+   let t3   := Expr.lam `x BinderInfo.default (Expr.sort Level.zero) (mkApp f #[a, x0]);
+   let t4   := Expr.lam `x BinderInfo.default (Expr.sort Level.zero) (mkApp f #[a, x1]);
+   unless (!t1.hasLooseBVar 0) $ throw "failed-1";
+   unless (t2.hasLooseBVar 0) $ throw "failed-2";
+   unless (!t3.hasLooseBVar 0) $ throw "failed-3";
+   unless (t4.hasLooseBVar 0) $ throw "failed-4";
+   unless (!t4.hasLooseBVar 1) $ throw "failed-4";
+   unless (!t2.hasLooseBVar 1) $ throw "failed-5";
+   pure ()
+
+#eval tst4