feat(library/definitional/projection): add projection macro
This commit is contained in:
parent
abc64fbab8
commit
01ce57e52e
3 changed files with 170 additions and 6 deletions
|
@ -753,7 +753,12 @@ struct structure_cmd_fn {
|
|||
expr coercion_value = parent_intro;
|
||||
for (unsigned idx : fmap) {
|
||||
expr const & field = m_fields[idx];
|
||||
expr proj = mk_app(mk_app(mk_constant(m_name + mlocal_name(field), st_ls), m_params), st);
|
||||
name proj_name = m_name + mlocal_name(field);
|
||||
expr proj;
|
||||
if (m_env.trust_lvl() == 0)
|
||||
proj = mk_app(mk_app(mk_constant(proj_name, st_ls), m_params), st);
|
||||
else
|
||||
proj = mk_projection_macro(proj_name, st);
|
||||
coercion_value = mk_app(coercion_value, proj);
|
||||
}
|
||||
coercion_value = Fun(m_params, Fun(st, coercion_value));
|
||||
|
|
|
@ -9,9 +9,12 @@ Author: Leonardo de Moura
|
|||
#include "kernel/instantiate.h"
|
||||
#include "kernel/abstract.h"
|
||||
#include "kernel/type_checker.h"
|
||||
#include "kernel/kernel_exception.h"
|
||||
#include "kernel/inductive/inductive.h"
|
||||
#include "library/reducible.h"
|
||||
#include "library/module.h"
|
||||
#include "library/util.h"
|
||||
#include "library/kernel_serializer.h"
|
||||
#include "library/definitional/projection.h"
|
||||
|
||||
namespace lean {
|
||||
|
@ -56,9 +59,9 @@ projection_info const * get_projection_info(environment const & env, name const
|
|||
return ext.m_info.find(p);
|
||||
}
|
||||
|
||||
static void projection_reader(deserializer & d, module_idx, shared_environment & senv,
|
||||
std::function<void(asynch_update_fn const &)> &,
|
||||
std::function<void(delayed_update_fn const &)> &) {
|
||||
static void projection_info_reader(deserializer & d, module_idx, shared_environment & senv,
|
||||
std::function<void(asynch_update_fn const &)> &,
|
||||
std::function<void(delayed_update_fn const &)> &) {
|
||||
name p, mk; unsigned nparams, i;
|
||||
d >> p >> mk >> nparams >> i;
|
||||
senv.update([=](environment const & env) -> environment {
|
||||
|
@ -66,15 +69,162 @@ static void projection_reader(deserializer & d, module_idx, shared_environment &
|
|||
});
|
||||
}
|
||||
|
||||
/** \brief If \c e is a constructor application, then return the name of the constructor.
|
||||
Otherwise, return none.
|
||||
*/
|
||||
optional<name> is_constructor_app(environment const & env, expr const & e) {
|
||||
expr const & fn = get_app_fn(e);
|
||||
if (is_constant(fn))
|
||||
if (auto I = inductive::is_intro_rule(env, const_name(fn)))
|
||||
return optional<name>(const_name(fn));
|
||||
return optional<name>();
|
||||
}
|
||||
|
||||
/** \brief If \c e is a constructor application, or a definition that wraps a
|
||||
constructor application, then return the name of the constructor.
|
||||
Otherwise, return none.
|
||||
*/
|
||||
optional<name> is_constructor_app_ext(environment const & env, expr const & e) {
|
||||
if (auto r = is_constructor_app(env, e))
|
||||
return r;
|
||||
expr const & f = get_app_fn(e);
|
||||
if (!is_constant(f))
|
||||
return optional<name>();
|
||||
auto decl = env.find(const_name(f));
|
||||
if (!decl || !decl->is_definition() || decl->is_opaque())
|
||||
return optional<name>();
|
||||
expr const * it = &decl->get_value();
|
||||
while (is_lambda(*it))
|
||||
it = &binding_body(*it);
|
||||
return is_constructor_app_ext(env, *it);
|
||||
}
|
||||
|
||||
static name * g_projection_macro_name = nullptr;
|
||||
static std::string * g_projection_opcode = nullptr;
|
||||
|
||||
class projection_macro_definition_cell : public macro_definition_cell {
|
||||
name m_proj_name;
|
||||
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 & n):m_proj_name(n) {}
|
||||
name const & get_proj_name() const { return m_proj_name; }
|
||||
virtual name get_name() const { return m_proj_name; } // *g_projection_macro_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> get_type(expr const & m, extension_context & ctx) const {
|
||||
check_macro(m);
|
||||
environment const & env = ctx.env();
|
||||
constraint_seq cs;
|
||||
expr s = macro_arg(m, 0);
|
||||
expr s_t = ctx.whnf(ctx.infer_type(s, cs), cs);
|
||||
buffer<expr> I_args;
|
||||
expr const & I = get_app_args(s_t, I_args);
|
||||
if (is_constant(I)) {
|
||||
declaration proj_decl = env.get(m_proj_name);
|
||||
if (length(const_levels(I)) != length(proj_decl.get_univ_params()))
|
||||
throw_kernel_exception(env, sstream() << "invalid projection application '" << m_proj_name
|
||||
<< "', incorrect number of universe parameters", m);
|
||||
expr t = instantiate_type_univ_params(proj_decl, const_levels(I));
|
||||
I_args.push_back(s);
|
||||
unsigned num = I_args.size();
|
||||
for (unsigned i = 0; i < num; i++) {
|
||||
if (!is_pi(t))
|
||||
throw_kernel_exception(env, sstream() << "invalid projection application '" << m_proj_name
|
||||
<< "', number of arguments mismatch", m);
|
||||
t = binding_body(t);
|
||||
}
|
||||
return mk_pair(instantiate_rev(t, I_args.size(), I_args.data()), cs);
|
||||
} else {
|
||||
// TODO(Leo)
|
||||
lean_unreachable();
|
||||
}
|
||||
}
|
||||
|
||||
// try to unfold projection argument into a \c c constructor application
|
||||
static optional<expr> process_proj_arg(environment const & env, name const & c, expr const & s) {
|
||||
if (optional<name> mk_name = is_constructor_app_ext(env, s)) {
|
||||
if (*mk_name == c) {
|
||||
expr new_s = s;
|
||||
while (is_app(new_s) && !is_constructor_app(env, new_s)) {
|
||||
if (auto next_new_s = unfold_app(env, new_s))
|
||||
new_s = *next_new_s;
|
||||
else
|
||||
return none_expr();
|
||||
}
|
||||
if (is_app(new_s))
|
||||
return some_expr(new_s);
|
||||
}
|
||||
}
|
||||
return none_expr();
|
||||
}
|
||||
|
||||
virtual optional<expr> expand(expr const & m, extension_context & ctx) const {
|
||||
check_macro(m);
|
||||
environment const & env = ctx.env();
|
||||
auto info = get_projection_info(env, m_proj_name);
|
||||
if (!info)
|
||||
throw_kernel_exception(env, sstream() << "invalid projection application '" << m_proj_name
|
||||
<< "', constant is not a projection function", m);
|
||||
expr const & s = macro_arg(m, 0);
|
||||
if (optional<expr> mk = process_proj_arg(env, info->m_constructor, s)) {
|
||||
// efficient version
|
||||
buffer<expr> mk_args;
|
||||
get_app_args(*mk, mk_args);
|
||||
unsigned i = info->m_nparams + info->m_i;
|
||||
lean_assert(i < mk_args.size());
|
||||
return some_expr(mk_args[i]);
|
||||
} else {
|
||||
// use definition
|
||||
constraint_seq cs;
|
||||
expr s_t = ctx.whnf(ctx.infer_type(s, cs), cs);
|
||||
if (cs)
|
||||
return none_expr();
|
||||
buffer<expr> I_args;
|
||||
expr const & I = get_app_args(s_t, I_args);
|
||||
if (!is_constant(I))
|
||||
return none_expr();
|
||||
return some_expr(mk_app(mk_app(mk_constant(m_proj_name, const_levels(I)), I_args), s));
|
||||
}
|
||||
}
|
||||
|
||||
virtual void write(serializer & s) const {
|
||||
s.write_string(*g_projection_opcode);
|
||||
s << m_proj_name;
|
||||
}
|
||||
};
|
||||
|
||||
expr mk_projection_macro(name const & proj_name, expr const & e) {
|
||||
macro_definition def(new projection_macro_definition_cell(proj_name));
|
||||
return mk_macro(def, 1, &e);
|
||||
}
|
||||
|
||||
void initialize_projection() {
|
||||
g_ext = new projection_ext_reg();
|
||||
g_proj_key = new std::string("proj");
|
||||
register_module_object_reader(*g_proj_key, projection_reader);
|
||||
register_module_object_reader(*g_proj_key, projection_info_reader);
|
||||
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 proj_name;
|
||||
d >> proj_name;
|
||||
return mk_projection_macro(proj_name, args[0]);
|
||||
});
|
||||
}
|
||||
|
||||
void finalize_projection() {
|
||||
delete g_proj_key;
|
||||
delete g_ext;
|
||||
delete g_projection_macro_name;
|
||||
delete g_projection_opcode;
|
||||
}
|
||||
|
||||
/** \brief Return true iff the type named \c S can be viewed as
|
||||
|
|
|
@ -8,7 +8,8 @@ Author: Leonardo de Moura
|
|||
#include "kernel/environment.h"
|
||||
|
||||
namespace lean {
|
||||
environment mk_projections(environment const & env, name const & n, buffer<name> const & proj_names, bool inst_implicit = false);
|
||||
environment mk_projections(environment const & env, name const & n, buffer<name> const & proj_names,
|
||||
bool inst_implicit = false);
|
||||
environment mk_projections(environment const & env, name const & n, bool inst_implicit = false);
|
||||
|
||||
/** \brief Return true iff the type named \c S can be viewed as
|
||||
|
@ -43,6 +44,14 @@ struct projection_info {
|
|||
*/
|
||||
projection_info const * get_projection_info(environment const & env, name const & p);
|
||||
|
||||
/** \brief Create a projection macro term that can peform the following reduction efficiently
|
||||
|
||||
pr_i A (mk A f_1 ... f_n) ==> f_i
|
||||
|
||||
\remark proj_name is the name of the definition that implements the actual projection.
|
||||
*/
|
||||
expr mk_projection_macro(name const & proj_name, expr const & e);
|
||||
|
||||
void initialize_projection();
|
||||
void finalize_projection();
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue