From 0a44c6859a447aa9082084bc5de60bcae9102f7e Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Sat, 21 Sep 2024 11:39:10 +0200
Subject: [PATCH] feat: expose Kernel.check for debugging purposes

along `Kernel.isDefEq` and `Kernel.whnf`.
---
 src/Lean/Environment.lean   |  7 +++++++
 src/kernel/type_checker.cpp |  6 ++++++
 tests/lean/run/kernel2.lean | 10 ++++++++++
 3 files changed, 23 insertions(+)

diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index 8bceddada3b8..5ce4c18b486c 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -1096,6 +1096,13 @@ def isDefEqGuarded (env : Environment) (lctx : LocalContext) (a b : Expr) : Bool
 @[extern "lean_kernel_whnf"]
 opaque whnf (env : Environment) (lctx : LocalContext) (a : Expr) : Except KernelException Expr
 
+/--
+  Kernel typecheck function. We use it mainly for debugging purposes.
+  Recall that the Kernel type checker does not support metavariables.
+  When implementing automation, consider using the `MetaM` methods. -/
+@[extern "lean_kernel_check"]
+opaque check (env : Environment) (lctx : LocalContext) (a : Expr) : Except KernelException Expr
+
 end Kernel
 
 class MonadEnv (m : Type → Type) where
diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index 54b7192dccd1..012ae00de913 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -1203,6 +1203,12 @@ extern "C" LEAN_EXPORT lean_object * lean_kernel_whnf(lean_object * env, lean_ob
     });
 }
 
+extern "C" LEAN_EXPORT lean_object * lean_kernel_check(lean_object * env, lean_object * lctx, lean_object * a) {
+    return catch_kernel_exceptions<object*>([&]() {
+        return type_checker(environment(env), local_ctx(lctx)).check(expr(a)).steal();
+    });
+}
+
 inline static expr * new_persistent_expr_const(name const & n) {
     expr * e = new expr(mk_const(n));
     mark_persistent(e->raw());
diff --git a/tests/lean/run/kernel2.lean b/tests/lean/run/kernel2.lean
index f5a25a8e141f..2c115f1548c6 100644
--- a/tests/lean/run/kernel2.lean
+++ b/tests/lean/run/kernel2.lean
@@ -15,6 +15,12 @@ def whnf (a : Name) : CoreM Unit := do
   let r ← ofExceptKernelException (Kernel.whnf env {} a)
   IO.println (toString a ++ " ==> " ++ toString r)
 
+def check (a : Name) : CoreM Unit := do
+  let env ← getEnv
+  let a := mkConst a
+  let r ← ofExceptKernelException (Kernel.check env {} a)
+  IO.println (toString a ++ " ==> " ++ toString r)
+
 partial def fact : Nat → Nat
 | 0     => 1
 | (n+1) => (n+1)*fact n
@@ -93,3 +99,7 @@ def c12 : Nat := 'a'.toNat
 /-- info: c12 ==> 97 -/
 #guard_msgs in
 #eval whnf `c12
+
+/-- info: c11 ==> Bool -/
+#guard_msgs in
+#eval check `c11