From cc18c0ef91a186f3b5088d9eef402d1a471957af Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 2 Oct 2019 10:05:55 -0700
Subject: [PATCH] feat(library/init/lean/expr): add `Expr.hasFVar` and
 `Expr.hasMVar`

cc @dselsam
---
 library/init/lean/expr.lean            |  6 ++++++
 src/kernel/expr.cpp                    | 11 +++++++++++
 src/util/object_ref.h                  |  3 +++
 tests/lean/mvar_fvar.lean              | 10 ++++++++++
 tests/lean/mvar_fvar.lean.expected.out |  6 ++++++
 5 files changed, 36 insertions(+)
 create mode 100644 tests/lean/mvar_fvar.lean
 create mode 100644 tests/lean/mvar_fvar.lean.expected.out

diff --git a/library/init/lean/expr.lean b/library/init/lean/expr.lean
index 755d088818..0d855a6723 100644
--- a/library/init/lean/expr.lean
+++ b/library/init/lean/expr.lean
@@ -100,6 +100,12 @@ constant eqv (a : @& Expr) (b : @& Expr) : Bool := default _
 
 instance : HasBeq Expr := ⟨Expr.eqv⟩
 
+@[extern "lean_expr_has_mvar"]
+constant hasMVar (a : @& Expr) : Bool := default _
+
+@[extern "lean_expr_has_fvar"]
+constant hasFVar (a : @& Expr) : Bool := default _
+
 def isSort : Expr → Bool
 | Expr.sort _ => true
 | _ => false
diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index 0d1ecf76fd..bc567a2cf6 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -788,6 +788,17 @@ expr infer_implicit(expr const & t, bool strict) {
     return infer_implicit(t, std::numeric_limits<unsigned>::max(), strict);
 }
 
+// =======================================
+// Extra exports
+
+extern "C" uint8 lean_expr_has_mvar(b_obj_arg o) {
+    return has_mvar(TO_REF(expr, o));
+}
+
+extern "C" uint8 lean_expr_has_fvar(b_obj_arg o) {
+    return has_fvar(TO_REF(expr, o));
+}
+
 // =======================================
 // Initialization & Finalization
 
diff --git a/src/util/object_ref.h b/src/util/object_ref.h
index b470e70d5d..f542e3cdec 100644
--- a/src/util/object_ref.h
+++ b/src/util/object_ref.h
@@ -216,4 +216,7 @@ template<typename T> T get_except_value(obj_arg o) {
         throw exception(err);
     }
 }
+
+// Remark: `T` must be an `object_ref`.
+#define TO_REF(T, o) reinterpret_cast<T const &>(o)
 }
diff --git a/tests/lean/mvar_fvar.lean b/tests/lean/mvar_fvar.lean
new file mode 100644
index 0000000000..26c752a714
--- /dev/null
+++ b/tests/lean/mvar_fvar.lean
@@ -0,0 +1,10 @@
+import init.lean
+open Lean
+
+#eval (Expr.fvar `a).hasFVar
+#eval (Expr.app (Expr.const `foo []) (Expr.fvar `a)).hasFVar
+#eval (Expr.app (Expr.const `foo []) (Expr.const `a [])).hasFVar
+
+#eval (Expr.mvar `a).hasMVar
+#eval (Expr.app (Expr.const `foo []) (Expr.mvar `a)).hasMVar
+#eval (Expr.app (Expr.const `foo []) (Expr.const `a [])).hasMVar
diff --git a/tests/lean/mvar_fvar.lean.expected.out b/tests/lean/mvar_fvar.lean.expected.out
new file mode 100644
index 0000000000..3e303073ab
--- /dev/null
+++ b/tests/lean/mvar_fvar.lean.expected.out
@@ -0,0 +1,6 @@
+true
+true
+false
+true
+true
+false