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

feat(library/metavar_context): add method for setting metavar user facing name

Browse source
This commit is contained in:
Leonardo de Moura 2017-08-17 09:43:02 -07:00
parent 9927f331f4
commit 0660e18943
2 changed files with 15 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/library/metavar_context.cpp
View file

@ -13,12 +13,15 @@ namespace lean {
static name * g_meta_prefix;
static expr * g_dummy_type;
name mk_meta_decl_name() {
static name mk_meta_decl_name() {
return mk_tagged_fresh_name(*g_meta_prefix);
}
expr mk_meta_ref(name const & n) {
return mk_metavar(n, *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);
}
bool is_metavar_decl_ref(level const & u) {
@ -46,10 +49,10 @@ level metavar_context::mk_univ_metavar_decl() {
return mk_meta_univ(mk_meta_decl_name());
}
expr metavar_context::mk_metavar_decl(local_context const & ctx, expr const & type) {
expr metavar_context::mk_metavar_decl(optional<name> const & pp_n, local_context const & ctx, expr const & type) {
name n = mk_meta_decl_name();
m_decls.insert(n, metavar_decl(ctx, head_beta_reduce(type)));
return mk_meta_ref(n);
return mk_meta_ref(n, pp_n);
}
optional<metavar_decl> metavar_context::find_metavar_decl(expr const & e) const {

8
src/library/metavar_context.h
View file

@ -31,9 +31,15 @@ class metavar_context {
name_map<expr> m_eassignment;
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(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);
}
optional<metavar_decl> find_metavar_decl(expr const & mvar) const;