From 28a48598327feb5c6c668ac4e44532d213c4eb38 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 30 Dec 2019 11:21:22 -0800
Subject: [PATCH] feat: expose `evalConst`

@Kha Could you please check `lean_eval_const`?
---
 src/Init/Lean/Environment.lean          |  3 +++
 src/library/compiler/ir_interpreter.cpp | 13 +++++++++++++
 tests/lean/run/evalconst.lean           | 11 +++++++++++
 3 files changed, 27 insertions(+)
 create mode 100644 tests/lean/run/evalconst.lean

diff --git a/src/Init/Lean/Environment.lean b/src/Init/Lean/Environment.lean
index a324e06236..385380198b 100644
--- a/src/Init/Lean/Environment.lean
+++ b/src/Init/Lean/Environment.lean
@@ -579,6 +579,9 @@ pExtDescrs.forM $ fun extDescr => do {
 };
 pure ()
 
+@[extern "lean_eval_const"]
+unsafe constant evalConst (α) [s : @& Inhabited α] (env : @& Environment) (constName : @& Name) : Except String α := arbitrary _
+
 end Environment
 
 /- Helper functions for accessing environment -/
diff --git a/src/library/compiler/ir_interpreter.cpp b/src/library/compiler/ir_interpreter.cpp
index 43246de9c8..e7de45e30f 100644
--- a/src/library/compiler/ir_interpreter.cpp
+++ b/src/library/compiler/ir_interpreter.cpp
@@ -890,6 +890,19 @@ object * run_boxed(environment const & env, name const & fn, unsigned n, object
 uint32 run_main(environment const & env, int argv, char * argc[]) {
     return interpreter(env).run_main(argv, argc);
 }
+
+extern "C" object * lean_eval_const(object * /* inh */, object * env, object * c) {
+    try {
+        if (g_interpreter == nullptr) {
+            return mk_cnstr(1, run_boxed(TO_REF(environment, env), TO_REF(name, c), 0, 0)).steal();
+        } else {
+            flet<interpreter*> reset(g_interpreter, nullptr);
+            return mk_cnstr(1, run_boxed(TO_REF(environment, env), TO_REF(name, c), 0, 0)).steal();
+        }
+    } catch (exception & ex) {
+        return mk_cnstr(0, string_ref(ex.what())).steal();
+    }
+}
 }
 
 void initialize_ir_interpreter() {
diff --git a/tests/lean/run/evalconst.lean b/tests/lean/run/evalconst.lean
new file mode 100644
index 0000000000..79465c6367
--- /dev/null
+++ b/tests/lean/run/evalconst.lean
@@ -0,0 +1,11 @@
+import Init.Lean
+open Lean
+
+def x := 10
+
+unsafe def tst : MetaIO Unit := do
+env ← MetaIO.getEnv;
+IO.println $ env.evalConst Nat `x;
+pure ()
+
+#eval tst