michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(kernel/inductive): simplify inductive datatype API

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-17 09:24:34 -07:00
parent 4ec89e8561
commit 36b070cb5b
3 changed files with 85 additions and 131 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
src/kernel/inductive/inductive.cpp
View file

@ -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<intro_rule> const & intro_rules,
optional<unsigned> const & univ_offset) {
return add_inductive(env, level_params, params, list<inductive_decl>(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<intro_rule> const & intro_rules) {
return add_inductive(env, level_params, num_params, list<inductive_decl>(inductive_decl(ind_name, type, intro_rules)));
}
environment add_inductive(environment const & env,
level_param_names const & level_params,
telescope const & params,
list<inductive_decl> const & decls,
optional<unsigned> const & univ_offset) {
unsigned num_params,
list<inductive_decl> 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;
}
}

29
src/kernel/inductive/inductive.h
View file

@ -18,42 +18,33 @@ namespace inductive {
std::unique_ptr<normalizer_extension> mk_extension();
/** \brief Introduction rule */
typedef std::tuple<name, // introduction rule name
telescope, // arguments
expr // result type
> intro_rule;
typedef std::pair<name, expr> 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<name, // datatype name
telescope, // indices
expr, // type
list<intro_rule> // 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<intro_rule> 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<inductive_decl> 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<unsigned> const & univ_offset = optional<unsigned>(0));
unsigned num_params,
list<inductive_decl> 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<intro_rule> const & intro_rules, // introduction rules
optional<unsigned> const & univ_offset = optional<unsigned>(0));
unsigned num_params, // number of params
expr const & type, // type of the form: params -> indices -> Type
list<intro_rule> const & intro_rules); // introduction rules
}
}

160
src/library/kernel_bindings.cpp
View file

@ -1704,111 +1704,73 @@ static void open_type_checker(lua_State * L) {
SET_GLOBAL_FUN(add_declaration, "add_decl");
}
template<typename T, typename F>
static std::pair<telescope, T> 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<int>(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<expr>(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<intro_rule> rs;
for (int i = sz; i >= 3; i--) {
lua_rawgeti(L, -1, i);
rs = list<intro_rule>(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<inductive_decl> abstract(list<inductive_decl> const & ds, expr const & a, unsigned i = 0) {
return map(ds, [&](inductive_decl const & d) { return abstract(d, a, i); });
}
static list<inductive_decl> 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<inductive_decl> r;
for (int i = sz; i >= 1; i--) {
lua_rawgeti(L, -1, i);
r = list<inductive_decl>(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<inductive_decl> ds = to_inductive_decls(L, 4);
optional<unsigned> offset(0);
if (nargs == 5) {
if (lua_isnil(L, 5))
offset = optional<unsigned>();
else
offset = lua_tonumber(L, 5);
buffer<intro_rule> 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<inductive_decl> 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<intro_rule> 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<list<inductive_decl>>(L, 3, ds,
[](list<inductive_decl> 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);
}
}