diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h index 1f0adcb85..1e03bb4a5 100644 --- a/src/kernel/type_checker.h +++ b/src/kernel/type_checker.h @@ -48,20 +48,19 @@ public: \brief Create a type checker for the given environment. The auxiliary names created by this type checker are based on the given name generator. - The following set of options is supported: - - mod_idx: if a module index is provided, then opaque definitions in module mod_idx - are considered transparent if they are not in extra_opaque. - - memoize: inferred types are memoized/cached - - extra_opaque: additional definitions that should be treated as opaque + memoize: if true, then inferred types are memoized/cached */ - type_checker(environment const & env, name_generator const & g, constraint_handler & h, std::unique_ptr && conv, bool memoize = true); - type_checker(environment const & env, name_generator const & g, constraint_handler & h, bool memoize = true):type_checker(env, g, h, mk_default_converter(env), memoize) {} + type_checker(environment const & env, name_generator const & g, constraint_handler & h, std::unique_ptr && conv, + bool memoize = true); + type_checker(environment const & env, name_generator const & g, constraint_handler & h, bool memoize = true): + type_checker(env, g, h, mk_default_converter(env), memoize) {} /** \brief Similar to the previous constructor, but if a method tries to create a constraint, then an exception is thrown. */ type_checker(environment const & env, name_generator const & g, std::unique_ptr && conv, bool memoize = true); - type_checker(environment const & env, name_generator const & g, bool memoize = true):type_checker(env, g, mk_default_converter(env), memoize) {} + type_checker(environment const & env, name_generator const & g, bool memoize = true): + type_checker(env, g, mk_default_converter(env), memoize) {} ~type_checker(); /** diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index b0b5c4eba..badcddfd6 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -10,12 +10,14 @@ Author: Leonardo de Moura #include "util/script_state.h" #include "util/list_lua.h" #include "util/pair_lua.h" +#include "util/luaref.h" #include "kernel/abstract.h" #include "kernel/for_each_fn.h" #include "kernel/free_vars.h" #include "kernel/instantiate.h" #include "kernel/metavar.h" #include "kernel/error_msgs.h" +#include "kernel/type_checker.h" #include "library/occurs.h" #include "library/io_state_stream.h" #include "library/expr_lt.h" @@ -1374,6 +1376,95 @@ static void open_substitution(lua_State * L) { SET_GLOBAL_FUN(substitution_pred, "is_substitution"); } +// constraint_handler +class lua_constraint_handler : public constraint_handler { + luaref m_f; +public: + lua_constraint_handler(luaref const & f):m_f(f) {} + virtual void add_cnstr(constraint const & c) { + lua_State * L = m_f.get_state(); + m_f.push(); + push_constraint(L, c); + pcall(L, 1, 0, 0); + } +}; +DECL_UDATA(lua_constraint_handler) +int mk_constraint_handler(lua_State * L) { + luaL_checktype(L, 1, LUA_TFUNCTION); // user-fun + return push_lua_constraint_handler(L, lua_constraint_handler(luaref(L, 1))); +} + +static const struct luaL_Reg lua_constraint_handler_m[] = { + {"__gc", lua_constraint_handler_gc}, + {0, 0} +}; + +static void open_constraint_handler(lua_State * L) { + luaL_newmetatable(L, lua_constraint_handler_mt); + lua_pushvalue(L, -1); + lua_setfield(L, -2, "__index"); + setfuncs(L, lua_constraint_handler_m, 0); + + SET_GLOBAL_FUN(mk_constraint_handler, "constraint_handler"); + SET_GLOBAL_FUN(lua_constraint_handler_pred, "is_constraint_handler"); +} + +// type_checker +typedef std::shared_ptr type_checker_ref; +DECL_UDATA(type_checker_ref) + +int mk_type_checker(lua_State * L) { + int nargs = lua_gettop(L); + if (nargs <= 2) { + return push_type_checker_ref(L, std::make_shared(to_environment(L, 1), to_name_generator(L, 2))); + } else if (nargs == 3 && is_lua_constraint_handler(L, 3)) { + return push_type_checker_ref(L, std::make_shared(to_environment(L, 1), to_name_generator(L, 2), + to_lua_constraint_handler(L, 3))); + } else if (nargs == 3) { + // TODO(Leo) + } else { + // TODO(Leo) + } + return 0; +} +int type_checker_whnf(lua_State * L) { return push_expr(L, to_type_checker_ref(L, 1)->whnf(to_expr(L, 2))); } +int type_checker_ensure_pi(lua_State * L) { return push_expr(L, to_type_checker_ref(L, 1)->ensure_pi(to_expr(L, 2))); } +int type_checker_ensure_sort(lua_State * L) { return push_expr(L, to_type_checker_ref(L, 1)->ensure_sort(to_expr(L, 2))); } +int type_checker_check(lua_State * L) { + int nargs = lua_gettop(L); + if (nargs <= 2) + return push_expr(L, to_type_checker_ref(L, 1)->check(to_expr(L, 2), param_names())); + else + return push_expr(L, to_type_checker_ref(L, 1)->check(to_expr(L, 2), to_list_name(L, 3))); +} +int type_checker_infer(lua_State * L) { return push_expr(L, to_type_checker_ref(L, 1)->infer(to_expr(L, 2))); } +int type_checker_is_conv(lua_State * L) { return push_boolean(L, to_type_checker_ref(L, 1)->is_conv(to_expr(L, 2), to_expr(L, 3))); } +int type_checker_is_def_eq(lua_State * L) { return push_boolean(L, to_type_checker_ref(L, 1)->is_def_eq(to_expr(L, 2), to_expr(L, 3))); } +int type_checker_is_prop(lua_State * L) { return push_boolean(L, to_type_checker_ref(L, 1)->is_prop(to_expr(L, 2))); } + +static const struct luaL_Reg type_checker_ref_m[] = { + {"__gc", type_checker_ref_gc}, + {"whnf", safe_function}, + {"ensure_pi", safe_function}, + {"ensure_sort", safe_function}, + {"check", safe_function}, + {"infer", safe_function}, + {"is_conv", safe_function}, + {"is_def_eq", safe_function}, + {"is_prop", safe_function}, + {0, 0} +}; + +static void open_type_checker(lua_State * L) { + luaL_newmetatable(L, type_checker_ref_mt); + lua_pushvalue(L, -1); + lua_setfield(L, -2, "__index"); + setfuncs(L, type_checker_ref_m, 0); + + SET_GLOBAL_FUN(mk_type_checker, "type_checker"); + SET_GLOBAL_FUN(type_checker_ref_pred, "is_type_checker"); +} + void open_kernel_module(lua_State * L) { open_level(L); open_list_level(L); @@ -1392,5 +1483,7 @@ void open_kernel_module(lua_State * L) { open_justification(L); open_constraint(L); open_substitution(L); + open_constraint_handler(L); + open_type_checker(L); } } diff --git a/tests/lua/tc1.lua b/tests/lua/tc1.lua new file mode 100644 index 000000000..31a457a38 --- /dev/null +++ b/tests/lua/tc1.lua @@ -0,0 +1,20 @@ +local env = empty_environment() +local g = name_generator("tst") +local tc = type_checker(env, g) +assert(is_type_checker(tc)) +local a = Const("a") +local t = Fun(a, Bool, a) +local b = Const("b") +print(t(b)) +assert(tc:whnf(t(b)) == b) +local cs = {} +local tc2 = type_checker(env, g, constraint_handler(function (c) print(c); cs[#cs+1] = c end)) +assert(tc:check(Bool) == mk_sort(mk_level_one())) +print(tc:infer(t)) +local m = mk_metavar("m1", mk_metavar("m2", mk_sort(mk_meta_univ("u")))) +print(tc:infer(m)) +local t2 = Fun(a, Bool, m(a)) +print(t2) +print(tc2:check(t)) +print(tc2:check(t2)) +assert(#cs == 2)