max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/metavar_context): store user_name at metavar_decl

Browse source
This commit is contained in:
Leonardo de Moura 2018-06-05 14:29:55 -07:00
parent fc8aa30f0f
commit 330c9afbc0
2 changed files with 13 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/library/metavar_context.cpp
View file

@ -14,11 +14,8 @@ namespace lean {
static name * g_meta_prefix;
static expr * g_dummy_type;
static expr mk_meta_ref(name const & n, optional<name> const & pp_n) {
if (pp_n)
return mk_metavar(n, *pp_n, *g_dummy_type);
else
return mk_metavar(n, *g_dummy_type);
static expr mk_meta_ref(name const & n) {
return mk_metavar(n, *g_dummy_type);
}
bool is_metavar_decl_ref(level const & u) {
@ -49,11 +46,11 @@ level metavar_context::mk_univ_metavar_decl() {
return mk_meta_univ(mk_meta_decl_name());
}
expr metavar_context::mk_metavar_decl(optional<name> const & pp_n, local_context const & ctx, expr const & type) {
expr metavar_context::mk_metavar_decl(name const & user_name, local_context const & lctx, expr const & type) {
// TODO(Leo): should use name_generator
name n = mk_meta_decl_name();
m_decls.insert(n, metavar_decl(ctx, head_beta_reduce(type)));
return mk_meta_ref(n, pp_n);
m_decls.insert(n, metavar_decl(user_name, lctx, head_beta_reduce(type)));
return mk_meta_ref(n);
}
optional<metavar_decl> metavar_context::find_metavar_decl(expr const & e) const {
@ -215,7 +212,7 @@ void metavar_context::instantiate_mvars_at_type_of(expr const & m) {
expr type = d.get_type();
expr new_type = instantiate_mvars(type);
if (new_type != type) {
m_decls.insert(mlocal_name(m), metavar_decl(d.get_context(), new_type));
m_decls.insert(mlocal_name(m), metavar_decl(d.get_user_name(), d.get_context(), new_type));
}
}

13
src/library/metavar_context.h
View file

@ -9,14 +9,17 @@ Author: Leonardo de Moura
namespace lean {
class metavar_decl {
name m_user_name;
local_context m_context;
expr m_type;
friend class metavar_context;
metavar_decl(local_context const & ctx, expr const & type):m_context(ctx), m_type(type) {}
metavar_decl(name const & user_name, local_context const & ctx, expr const & type):
m_user_name(user_name), m_context(ctx), m_type(type) {}
public:
metavar_decl() {}
expr const & get_type() const { return m_type; }
local_context const & get_context() const { return m_context; }
name const & get_user_name() const { return m_user_name; }
};
bool is_metavar_decl_ref(level const & l);
@ -44,15 +47,13 @@ class metavar_context {
struct interface_impl;
friend struct interface_impl;
expr mk_metavar_decl(optional<name> const & pp_n, local_context const & ctx, expr const & type);
public:
level mk_univ_metavar_decl();
expr mk_metavar_decl(name const & user_name, local_context const & ctx, expr const & type);
expr mk_metavar_decl(local_context const & ctx, expr const & type) {
return mk_metavar_decl(optional<name>(), ctx, type);
}
expr mk_metavar_decl(name const & pp_name, local_context const & ctx, expr const & type) {
return mk_metavar_decl(optional<name>(pp_name), ctx, type);
return mk_metavar_decl(name(), ctx, type);
}
optional<metavar_decl> find_metavar_decl(expr const & mvar) const;