diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp index e78a7c4f2..ffd91b27a 100644 --- a/src/kernel/inductive/inductive.cpp +++ b/src/kernel/inductive/inductive.cpp @@ -8,28 +8,29 @@ Author: Leonardo de Moura namespace lean { namespace inductive { -environment add_inductive(environment const & env, name const & ind_name, level_param_names const & level_params, - telescope const & params, telescope const & indices, list const & intro_rules, - optional const & univ_offset) { - return add_inductive(env, level_params, params, list(std::make_tuple(ind_name, indices, intro_rules)), univ_offset); +environment add_inductive(environment const & env, name const & ind_name, level_param_names const & level_params, + unsigned num_params, expr const & type, list const & intro_rules) { + return add_inductive(env, level_params, num_params, list(inductive_decl(ind_name, type, intro_rules))); } environment add_inductive(environment const & env, level_param_names const & level_params, - telescope const & params, - list const & decls, - optional const & univ_offset) { + unsigned num_params, + list const & decls) { // TODO(Leo) - std::cout << "add_inductive\n"; - if (!is_nil(level_params)) { for (auto l : level_params) { std::cout << l << " "; } std::cout << "\n"; } - if (!is_nil(params)) { for (auto e : params) { std::cout << e.get_name() << " "; } std::cout << "\n"; } + std::cout << "\nadd_inductive\n"; + if (!is_nil(level_params)) { + std::cout << "level params: "; + for (auto l : level_params) { std::cout << l << " "; } + std::cout << "\n"; + } + std::cout << "num params: " << num_params << "\n"; for (auto d : decls) { - std::cout << inductive_decl_name(d) << "\n"; + std::cout << inductive_decl_name(d) << " : " << inductive_decl_type(d) << "\n"; for (auto ir : inductive_decl_intros(d)) { - std::cout << " " << intro_rule_name(ir) << " #" << length(intro_rule_args(ir)) << " " << intro_rule_type(ir) << "\n"; + std::cout << " " << intro_rule_name(ir) << " : " << intro_rule_type(ir) << "\n"; } } - if (univ_offset) std::cout << "offset: " << *univ_offset << "\n"; return env; } } diff --git a/src/kernel/inductive/inductive.h b/src/kernel/inductive/inductive.h index 61f0a4690..6f7db7137 100644 --- a/src/kernel/inductive/inductive.h +++ b/src/kernel/inductive/inductive.h @@ -18,42 +18,33 @@ namespace inductive { std::unique_ptr mk_extension(); /** \brief Introduction rule */ -typedef std::tuple intro_rule; +typedef std::pair intro_rule; -inline name const & intro_rule_name(intro_rule const & r) { return std::get<0>(r); } -inline telescope const & intro_rule_args(intro_rule const & r) { return std::get<1>(r); } -inline expr const & intro_rule_type(intro_rule const & r) { return std::get<2>(r); } +inline name const & intro_rule_name(intro_rule const & r) { return r.first; } +inline expr const & intro_rule_type(intro_rule const & r) { return r.second; } /** \brief Inductive datatype */ typedef std::tuple // introduction rules for this datatype > inductive_decl; inline name const & inductive_decl_name(inductive_decl const & d) { return std::get<0>(d); } -inline telescope const & inductive_decl_indices(inductive_decl const & d) { return std::get<1>(d); } +inline expr const & inductive_decl_type(inductive_decl const & d) { return std::get<1>(d); } inline list const & inductive_decl_intros(inductive_decl const & d) { return std::get<2>(d); } /** \brief Declare a finite set of mutually dependent inductive datatypes. */ environment add_inductive(environment const & env, level_param_names const & level_params, - telescope const & params, - list const & decls, - // By default the resultant inductive datatypes live in max(level_params), - // we can add an offset/lift k, and the resultant type is succ^k(max(level_params)). - // If none is provided, then for impredicative environments the result types are Bool/Prop (level 0) - optional const & univ_offset = optional(0)); + unsigned num_params, + list const & decls); /** \brief Declare a single inductive datatype. */ environment add_inductive(environment const & env, name const & ind_name, // name of new inductive datatype level_param_names const & level_params, // level parameters - telescope const & params, // parameters - telescope const & indices, // indices - list const & intro_rules, // introduction rules - optional const & univ_offset = optional(0)); + unsigned num_params, // number of params + expr const & type, // type of the form: params -> indices -> Type + list const & intro_rules); // introduction rules } } diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index a0bfffd87..cb3d8841f 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -1704,111 +1704,73 @@ static void open_type_checker(lua_State * L) { SET_GLOBAL_FUN(add_declaration, "add_decl"); } -template -static std::pair to_telescope(lua_State * L, int idx, T const & v, F const & v_abst) { - luaL_checktype(L, idx, LUA_TTABLE); - lua_pushvalue(L, idx); // push table on the top - int sz = objlen(L, -1); // get table size - telescope r; - T new_v = v; - for (int i = sz; i >= 1; i--) { - auto const & t = get_binder_from_table(L, -1, i); - expr const & a = std::get<0>(t); - expr const & a_ty = std::get<1>(t); - binder_info const & bi = std::get<2>(t); - r = telescope(binder(const_name(a), a_ty, bi), abstract(r, a)); - new_v = v_abst(new_v, a, sz-i); - } - lua_pop(L, 1); // pop table from the top - return mk_pair(r, new_v); -} -static telescope to_telescope(lua_State * L, int idx) { - return to_telescope(L, idx, 0, [](int, expr const &, int) { return 0; }).first; -} - namespace inductive { -static intro_rule to_intro_rule(lua_State * L, int idx) { - luaL_checktype(L, idx, LUA_TTABLE); - lua_pushvalue(L, idx); // push table on the top - if (objlen(L, idx) != 3) - throw exception("invalid introduction rule, it must have three arguments: name, telescope (arguments), type"); - lua_rawgeti(L, -1, 1); - lua_rawgeti(L, -2, 2); - lua_rawgeti(L, -3, 3); - name n = to_name_ext(L, -3); - expr ty = to_expr(L, -1); - auto args_ty = to_telescope(L, -2, ty, - [](expr const & v, expr const & a, unsigned i) -> expr { - return abstract(v, a, i); - }); - lua_pop(L, 4); - return intro_rule(n, args_ty.first, args_ty.second); -} - -static inductive_decl to_inductive_decl(lua_State * L, int idx) { - luaL_checktype(L, idx, LUA_TTABLE); - lua_pushvalue(L, idx); // push table on the top - int sz = objlen(L, idx); - if (sz < 2) - throw exception("invalid inductive decl, it must have at least two arguments: name, indices"); - list rs; - for (int i = sz; i >= 3; i--) { - lua_rawgeti(L, -1, i); - rs = list(to_intro_rule(L, -1), rs); - lua_pop(L, 1); +/** \brief Get the number of indices (if available), if they are, increment idx */ +static unsigned get_num_params(lua_State * L, int & idx) { + if (lua_isnumber(L, idx)) { + if (lua_tonumber(L, idx) < 0) + throw exception(sstream() << "arg #" << idx << " (number of parameters) must be nonnegative"); + unsigned r = lua_tonumber(L, idx); + idx++; + return r; + } else { + return 0; } - lua_rawgeti(L, -1, 2); - telescope const & indices = to_telescope(L, -1); - lua_pop(L, 1); - lua_rawgeti(L, -1, 1); - name const & n = to_name_ext(L, -1); - lua_pop(L, 2); - return inductive_decl(n, indices, rs); } - -inductive_decl abstract(inductive_decl const & d, expr const & a, unsigned i = 0) { - telescope const & indices = inductive_decl_indices(d); - return inductive_decl(inductive_decl_name(d), abstract(indices, a, i), inductive_decl_intros(d)); -} - -list abstract(list const & ds, expr const & a, unsigned i = 0) { - return map(ds, [&](inductive_decl const & d) { return abstract(d, a, i); }); -} - -static list to_inductive_decls(lua_State * L, int idx) { - luaL_checktype(L, idx, LUA_TTABLE); - lua_pushvalue(L, idx); // push table on the top - int sz = objlen(L, idx); - list r; - for (int i = sz; i >= 1; i--) { - lua_rawgeti(L, -1, i); - r = list(to_inductive_decl(L, -1), r); - lua_pop(L, 1); +static int add_inductive1(lua_State * L) { + environment env = to_environment(L, 1); + name const & Iname = to_name_ext(L, 2); + int idx = 3; + level_param_names ls; + if (!is_expr(L, idx) && !lua_isnumber(L, idx)) { + ls = to_level_param_names(L, idx); + idx++; } - lua_pop(L, 1); - return r; -} - -static int add_inductive(lua_State * L) { + unsigned num_params = get_num_params(L, idx); + expr Itype = to_expr(L, idx); int nargs = lua_gettop(L); - environment env = to_environment(L, 1); - level_param_names ls = to_level_param_names(L, 2); - list ds = to_inductive_decls(L, 4); - optional offset(0); - if (nargs == 5) { - if (lua_isnil(L, 5)) - offset = optional(); - else - offset = lua_tonumber(L, 5); + buffer irules; + for (int i = idx+1; i <= nargs; i+=2) + irules.push_back(intro_rule(to_name_ext(L, i), to_expr(L, i+1))); + return push_environment(L, add_inductive(env, Iname, ls, num_params, Itype, to_list(irules.begin(), irules.end()))); +} +static int add_inductivek(lua_State * L) { + environment env = to_environment(L, 1); + level_param_names ls = to_level_param_names(L, 2); + int idx = 3; + unsigned num_params = get_num_params(L, idx); + int nargs = lua_gettop(L); + buffer decls; + for (; idx <= nargs; idx++) { + luaL_checktype(L, idx, LUA_TTABLE); + int decl_sz = objlen(L, idx); + if (decl_sz < 2) + throw exception("invalid add_inductive, datatype declaration must have at least a name and type"); + if (decl_sz % 2 != 0) + throw exception("invalid add_inductive, datatype declaration must have an even number of fields: (name, type)+"); + lua_rawgeti(L, idx, 1); + lua_rawgeti(L, idx, 2); + name Iname = to_name_ext(L, -2); + expr Itype = to_expr(L, -1); + lua_pop(L, 2); + buffer irules; + for (int i = 3; i <= decl_sz; i+=2) { + lua_rawgeti(L, idx, i); + lua_rawgeti(L, idx, i+1); + irules.push_back(intro_rule(to_name_ext(L, -2), to_expr(L, -1))); + lua_pop(L, 2); + } + decls.push_back(inductive_decl(Iname, Itype, to_list(irules.begin(), irules.end()))); } - auto params_ds = - to_telescope>(L, 3, ds, - [](list const & ds, expr const & a, int i) { - return abstract(ds, a, i); - }); - ds = params_ds.second; - telescope const & ps = params_ds.first; - return push_environment(L, add_inductive(env, ls, ps, ds, offset)); + if (decls.empty()) + throw exception("invalid add_inductive, at least one inductive type must be defined"); + return push_environment(L, add_inductive(env, ls, num_params, to_list(decls.begin(), decls.end()))); +} +static int add_inductive(lua_State * L) { + if (is_name(L, 2) || lua_isstring(L, 2)) + return add_inductive1(L); + else + return add_inductivek(L); } }