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

feat(library/definitional/projection): define projections using auxiliary macro

Browse source
This commit is contained in:
Leonardo de Moura 2015-07-02 10:38:58 -07:00
parent c15bcf1354
commit 7de7c5b73d
3 changed files with 143 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/library/definitional/init_module.cpp
View file

@ -6,13 +6,16 @@ Author: Leonardo de Moura
*/
#include "library/util.h"
#include "library/definitional/equations.h"
#include "library/definitional/projection.h"
namespace lean{
void initialize_definitional_module() {
initialize_equations();
initialize_def_projection();
}
void finalize_definitional_module() {
finalize_def_projection();
finalize_equations();
}
}

137
src/library/definitional/projection.cpp
View file

@ -16,6 +16,7 @@ Author: Leonardo de Moura
#include "library/module.h"
#include "library/util.h"
#include "library/normalize.h"
#include "library/kernel_serializer.h"
#include "library/definitional/projection.h"
namespace lean {
@ -51,6 +52,130 @@ static bool is_prop(expr type) {
return is_sort(type) && is_zero(sort_level(type));
}
static name * g_projection_macro_name = nullptr;
static std::string * g_projection_opcode = nullptr;
/** \brief Auxiliary macro used to implement projections efficiently.
They bypass the recursor.
These macros are only used to speedup type checking when sending declarations to the kernel.
During elaboration, we use a custom converter that never unfolds projections.
*/
class projection_macro_definition_cell : public macro_definition_cell {
name m_I_name;
name m_constructor_name;
name m_proj_name;
unsigned m_idx;
level_param_names m_ps;
expr m_type;
expr m_val; // expanded form
void check_macro(expr const & m) const {
if (!is_macro(m) || macro_num_args(m) != 1)
throw exception(sstream() << "invalid '" << m_proj_name
<< "' projection macro, incorrect number of arguments");
}
public:
projection_macro_definition_cell(name const & I, name const & c, name const & p, unsigned i,
level_param_names const & ps, expr const & type, expr const & val):
m_I_name(I), m_constructor_name(c), m_proj_name(p), m_idx(i), m_ps(ps), m_type(type), m_val(val) {}
virtual name get_name() const { return m_proj_name; }
virtual format pp(formatter const &) const { return format(m_proj_name); }
virtual void display(std::ostream & out) const { out << m_proj_name; }
virtual pair<expr, constraint_seq> check_type(expr const & m, extension_context & ctx, bool infer_only) const {
check_macro(m);
environment const & env = ctx.env();
constraint_seq cs;
expr s = macro_arg(m, 0);
expr s_t = ctx.whnf(ctx.check_type(s, cs, infer_only), cs);
buffer<expr> I_args;
expr const & I = get_app_args(s_t, I_args);
if (!is_constant(I)) {
// remark: this is not an issue since this macro should not be used during elaboration.
throw_kernel_exception(env, sstream() << "projection macros do not support arbitrary terms "
<< "containing metavariables yet (solution: use trust-level 0)", m);
}
if (length(const_levels(I)) != length(m_ps))
throw_kernel_exception(env, sstream() << "invalid projection application '" << m_proj_name
<< "', incorrect number of universe parameters", m);
expr t = instantiate_univ_params(m_type, m_ps, const_levels(I));
I_args.push_back(s);
return mk_pair(instantiate_rev(t, I_args.size(), I_args.data()), cs);
}
virtual optional<expr> expand(expr const & m, extension_context & ctx) const {
check_macro(m);
expr const & s = macro_arg(m, 0);
constraint_seq cs;
expr new_s = ctx.whnf(s, cs);
if (cs)
return none_expr();
buffer<expr> c_args;
expr const & c = get_app_args(new_s, c_args);
if (is_constant(c) && const_name(c) == m_constructor_name && m_idx < c_args.size()) {
return some_expr(c_args[m_idx]);
} else {
// expand into recursor
expr s_type = ctx.whnf(ctx.infer_type(s, cs), cs);
if (cs)
return none_expr();
buffer<expr> args;
expr const & I = get_app_args(s_type, args);
if (!is_constant(I) || length(m_ps) != length(const_levels(I)))
return none_expr();
expr r = instantiate_univ_params(m_val, m_ps, const_levels(I));
args.push_back(new_s);
return some(instantiate_rev(r, args.size(), args.data()));
}
}
virtual void write(serializer & s) const {
s.write_string(*g_projection_opcode);
s << m_I_name << m_constructor_name << m_proj_name << m_idx << m_ps << m_type << m_val;
}
virtual bool operator==(macro_definition_cell const & other) const {
if (auto other_ptr = dynamic_cast<projection_macro_definition_cell const *>(&other)) {
return m_proj_name == other_ptr->m_proj_name;
} else {
return false;
}
}
virtual unsigned hash() const {
return m_proj_name.hash();
}
};
static expr mk_projection_macro(name const & I, name const & c, name const & p, unsigned i,
level_param_names const & ps, expr const & type, expr const & val, expr const & arg) {
macro_definition m(new projection_macro_definition_cell(I, c, p, i, ps, type, val));
return mk_macro(m, 1, &arg);
}
void initialize_def_projection() {
g_projection_macro_name = new name("projection");
g_projection_opcode = new std::string("Proj");
register_macro_deserializer(*g_projection_opcode,
[](deserializer & d, unsigned num, expr const * args) {
if (num != 1)
throw corrupted_stream_exception();
name I_name, c_name, proj_name; unsigned idx;
level_param_names ps; expr type, val;
d >> I_name >> c_name >> proj_name >> idx >> ps >> type >> val;
return mk_projection_macro(I_name, c_name, proj_name, idx,
ps, type, val, args[0]);
});
}
void finalize_def_projection() {
delete g_projection_macro_name;
delete g_projection_opcode;
}
environment mk_projections(environment const & env, name const & n, buffer<name> const & proj_names,
implicit_infer_kind infer_k, bool inst_implicit) {
// Given an inductive datatype C A (where A represent parameters)
@ -116,6 +241,18 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
expr proj_type = Pi(proj_args, result_type);
proj_type = infer_implicit_params(proj_type, nparams, infer_k);
expr proj_val = Fun(proj_args, rec_app);
if (new_env.trust_lvl() > 0) {
// use macros
expr mval = proj_val;
expr mtype = proj_type;
for (unsigned i = 0; i < proj_args.size(); i++) {
mval = binding_body(mval);
mtype = binding_body(mtype);
}
proj_val = mk_projection_macro(n, inductive::intro_rule_name(intro), proj_name,
nparams + i, lvl_params, mtype, mval, proj_args.back());
proj_val = Fun(proj_args, proj_val);
}
bool use_conv_opt = false;
declaration new_d = mk_definition(env, proj_name, lvl_params, proj_type, proj_val,
use_conv_opt);

3
src/library/definitional/projection.h
View file

@ -22,4 +22,7 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
implicit_infer_kind infer_k = implicit_infer_kind::Implicit, bool inst_implicit = false);
environment mk_projections(environment const & env, name const & n,
implicit_infer_kind infer_k = implicit_infer_kind::Implicit, bool inst_implicit = false);
void initialize_def_projection();
void finalize_def_projection();
}