refactor(library/app_builder): remove app_builder Lua API

src/library/app_builder.cpp

@@ -247,61 +247,4 @@ optional<expr> app_builder::mk_app(name const & n, expr const & a1, expr const &
 }
 void app_builder::push() { m_ptr->push(); }
 void app_builder::pop() { m_ptr->pop(); }
-
-struct lua_app_builder {
-    type_checker_ref m_tc;
-    app_builder      m_builder;
-    lua_app_builder(type_checker_ref const & r):m_tc(r), m_builder(*r.get()) {}
-};
-
-typedef std::shared_ptr<lua_app_builder> app_builder_ref;
-
-DECL_UDATA(app_builder_ref)
-
-static int mk_app_builder(lua_State * L) {
-    return push_app_builder_ref(L, std::make_shared<lua_app_builder>(to_type_checker_ref(L, 1)));
-}
-
-static int app_builder_mk_app(lua_State * L) {
-    int nargs = lua_gettop(L);
-    buffer<expr> args;
-    app_builder & b = to_app_builder_ref(L, 1)->m_builder;
-    bool use_cache  = true;
-    name n          = to_name_ext(L, 2);
-    for (int i = 3; i <= nargs; i++) {
-        if (i < nargs || is_expr(L, i))
-            args.push_back(to_expr(L, i));
-        else
-            use_cache = lua_toboolean(L, i);
-    }
-    return push_optional_expr(L, b.mk_app(n, args.size(), args.data(), use_cache));
-}
-
-static int app_builder_push(lua_State * L) {
-    to_app_builder_ref(L, 1)->m_builder.push();
-    return 0;
-}
-
-static int app_builder_pop(lua_State * L) {
-    to_app_builder_ref(L, 1)->m_builder.pop();
-    return 0;
-}
-
-static const struct luaL_Reg app_builder_ref_m[] = {
-    {"__gc",    app_builder_ref_gc},
-    {"mk_app",  safe_function<app_builder_mk_app>},
-    {"push",    safe_function<app_builder_push>},
-    {"pop",     safe_function<app_builder_pop>},
-    {0, 0}
-};
-
-void open_app_builder(lua_State * L) {
-    luaL_newmetatable(L, app_builder_ref_mt);
-    lua_pushvalue(L, -1);
-    lua_setfield(L, -2, "__index");
-    setfuncs(L, app_builder_ref_m, 0);
-
-    SET_GLOBAL_FUN(mk_app_builder,       "app_builder");
-    SET_GLOBAL_FUN(app_builder_ref_pred, "is_app_builder");
-}
 }

src/library/app_builder.h

@@ -55,6 +55,4 @@ public:
     */
     void pop();
 };
-
-void open_app_builder(lua_State * L);
 }

src/library/register_module.h

@@ -17,7 +17,6 @@ Author: Leonardo de Moura
 #include "library/scoped_ext.h"
 #include "library/match.h"
 #include "library/reducible.h"
-#include "library/app_builder.h"
 
 namespace lean {
 inline void open_core_module(lua_State * L) {
@@ -32,7 +31,6 @@ inline void open_core_module(lua_State * L) {
     open_explicit(L);
     open_match(L);
     open_reducible(L);
-    open_app_builder(L);
 }
 inline void register_core_module() {
     script_state::register_module(open_core_module);

tests/lean/run/app_builder.lean

@@ -1,63 +0,0 @@
-definition a :num := 10
-
-constant b : num
-constant c : num
-constant H1 : a = b
-constant H2 : b = c
-constant d : nat
-constant f : nat → nat
-constant g : nat → nat
-
-set_option pp.implicit true
-set_option pp.universes true
-set_option pp.notation  false
-(*
- local env = get_env()
- local tc  = non_irreducible_type_checker()
- local b   = app_builder(tc)
- local a   = Const("a")
- local c   = Const("c")
- local d   = Const("d")
- local f   = Const("f")
- local g   = Const("g")
- function tst(n, ...)
-    local args = {...}
-    local r    = b:mk_app(n, unpack(args))
-    print(tostring(r) .. " : " .. tostring(tc:check(r)))
-    return r
- end
- tst("eq", a, c)
- tst("eq", a, c)
- tst("eq", c, a)
- tst("eq", a, a)
- tst("eq", d, d)
- tst({"eq", "refl"}, a)
- tst({"eq", "refl"}, a)
- tst({"eq", "refl"}, d)
- tst({"eq", "refl"}, d)
- tst({"eq", "refl"}, c)
- tst({"eq", "refl"}, c, false)
- tst({"eq", "refl"}, a)
- local H1  = Const("H1")
- local H2  = Const("H2")
- tst({"eq", "trans"}, H1, H2)
- H1sy = tst({"eq", "symm"}, H1)
- H2sy = tst({"eq", "symm"}, H2)
- tst({"eq", "trans"}, H2sy, H1sy)
- tst({"heq", "refl"}, a)
- H1h = tst({"heq", "of_eq"}, H1)
- H2h = tst({"heq", "of_eq"}, H2)
- tst({"heq", "trans"}, H1h, H2h)
- tst({"heq", "symm"}, H1h)
- tst({"heq", "symm"}, H1h)
- tst({"heq"}, a, c)
- tst({"heq"}, a, d)
- tst({"heq"}, d, a)
- tst({"heq"}, a, c)
- tst({"heq"}, a, d)
- tst({"heq"}, d, a)
- tst({"eq", "refl"}, f)
- tst({"eq", "refl"}, g)
- tst("eq", f, g)
- tst("eq", g, f)
-*)