feat(bindings/lua): add cex_builder to Lua API

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

src/bindings/lua/CMakeLists.txt

@@ -2,7 +2,7 @@ add_library(lua util.cpp lua_exception.cpp name.cpp numerics.cpp
 lref.cpp splay_map.cpp options.cpp sexpr.cpp format.cpp level.cpp
 local_context.cpp expr.cpp context.cpp object.cpp environment.cpp
 formatter.cpp justification.cpp metavar_env.cpp type_inferer.cpp
-io_state.cpp goal.cpp proof_builder.cpp leanlua_state.cpp
+io_state.cpp goal.cpp proof_builder.cpp cex_builder.cpp
-frontend_lean.cpp)
+leanlua_state.cpp frontend_lean.cpp)
 
 target_link_libraries(lua ${LEAN_LIBS})

src/bindings/lua/cex_builder.cpp

@@ -0,0 +1,64 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <sstream>
+#include <lua.hpp>
+#include "util/optional.h"
+#include "kernel/environment.h"
+#include "library/tactic/cex_builder.h"
+#include "bindings/lua/util.h"
+#include "bindings/lua/name.h"
+#include "bindings/lua/expr.h"
+#include "bindings/lua/environment.h"
+#include "bindings/lua/proof_builder.h"
+#include "bindings/lua/lref.h"
+
+namespace lean {
+DECL_UDATA(cex_builder)
+
+static int mk_cex_builder(lua_State * L) {
+    luaL_checktype(L, 1, LUA_TFUNCTION); // user-fun
+    lref ref(L, 1);
+    return push_cex_builder(L,
+                            mk_cex_builder([=](name const & n, optional<counterexample> const & cex, assignment const & a) -> counterexample {
+                                      ref.push(); // push user-fun on the stack
+                                      push_name(L, n);
+                                      if (cex)
+                                          push_environment(L, *cex);
+                                      else
+                                          lua_pushnil(L);
+                                      push_assignment(L, a);
+                                      pcall(L, 3, 1, 0);
+                                      environment r = to_environment(L, -1);
+                                      lua_pop(L, 1);
+                                      return r;
+                                  }));
+}
+
+static int cex_builder_call(lua_State * L) {
+    if (is_environment(L, 3))
+        return push_environment(L, to_cex_builder(L, 1)(to_name_ext(L, 2), optional<counterexample>(to_environment(L, 3)), to_assignment(L, 4)));
+    else
+        return push_environment(L, to_cex_builder(L, 1)(to_name_ext(L, 2), optional<counterexample>(), to_assignment(L, 4)));
+}
+
+static const struct luaL_Reg cex_builder_m[] = {
+    {"__gc",            cex_builder_gc}, // never throws
+    {"__call",          safe_function<cex_builder_call>},
+    {0, 0}
+};
+
+void open_cex_builder(lua_State * L) {
+    luaL_newmetatable(L, cex_builder_mt);
+    lua_pushvalue(L, -1);
+    lua_setfield(L, -2, "__index");
+    setfuncs(L, cex_builder_m, 0);
+
+    SET_GLOBAL_FUN(cex_builder_pred, "is_cex_builder");
+    SET_GLOBAL_FUN(mk_cex_builder, "cex_builder");
+}
+
+}

src/bindings/lua/cex_builder.h

@@ -0,0 +1,12 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include <lua.hpp>
+namespace lean {
+UDATA_DEFS(cex_builder)
+void open_cex_builder(lua_State * L);
+}

src/bindings/lua/leanlua_state.cpp

@@ -35,6 +35,7 @@ Author: Leonardo de Moura
 #include "bindings/lua/metavar_env.h"
 #include "bindings/lua/goal.h"
 #include "bindings/lua/proof_builder.h"
+#include "bindings/lua/cex_builder.h"
 #include "bindings/lua/io_state.h"
 #include "bindings/lua/type_inferer.h"
 #include "bindings/lua/frontend_lean.h"
@@ -189,6 +190,7 @@ struct leanlua_state::imp {
         open_type_inferer(m_state);
         open_goal(m_state);
         open_proof_builder(m_state);
+        open_cex_builder(m_state);
         open_frontend_lean(m_state);
         open_thread(m_state);
         open_interrupt(m_state);

tests/lua/cex_builder1.lua

@@ -0,0 +1,14 @@
+local cex = cex_builder(function(n, cex, a)
+                          if cex then
+                             return cex
+                          else
+                             error("no counterexample")
+                          end
+end)
+assert(is_cex_builder(cex))
+local env = environment()
+env:add_var("T", Type())
+local a   = assignment()
+local env2 = cex("main", env, a)
+assert(env2:find_object("T"))
+assert(not pcall(function() cex("main", nil, a) end))