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

refactor(kernel): abstract_type_context::mk_fresh_name ==> abstract_type_context::next_name

Browse source
This commit is contained in:
Leonardo de Moura 2018-02-07 11:25:08 -08:00
parent 28d6326228
commit ce028d651d
5 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/parser.cpp
View file

@ -2344,7 +2344,7 @@ public:
virtual expr infer(expr const & e) override { return ctx().infer(e); }
virtual expr check(expr const & e) override { return ctx().check(e); }
virtual optional<expr> is_stuck(expr const & e) override { return ctx().is_stuck(e); }
virtual name mk_fresh_name() override { return ctx().mk_fresh_name(); }
virtual name next_name() override { return ctx().next_name(); }
};
void parser::parse_command(cmd_meta const & meta) {

2
src/kernel/abstract_type_context.cpp
View file

@ -10,7 +10,7 @@ Author: Leonardo de Moura
namespace lean {
expr abstract_type_context::push_local(name const & pp_name, expr const & type, binder_info const & bi) {
return mk_local(mk_fresh_name(), pp_name, type, bi);
return mk_local(next_name(), pp_name, type, bi);
}
void abstract_type_context::pop_local() {

2
src/kernel/abstract_type_context.h
View file

@ -20,7 +20,7 @@ public:
virtual ~abstract_type_context() {}
virtual environment const & env() const = 0;
virtual expr whnf(expr const & e) = 0;
virtual name mk_fresh_name() = 0;
virtual name next_name() = 0;
virtual expr relaxed_whnf(expr const & e) { return whnf(e); }
virtual bool is_def_eq(expr const & e1, expr const & e2) = 0;
virtual bool relaxed_is_def_eq(expr const & e1, expr const & e2) { return is_def_eq(e1, e2); }

2
src/kernel/type_checker.h
View file

@ -85,7 +85,7 @@ public:
virtual environment const & env() const { return m_env; }
virtual name mk_fresh_name() { return m_name_generator.next(); }
virtual name next_name() { return m_name_generator.next(); }
/** \brief Return the type of \c t.
It does not check whether the input expression is type correct or not.

4
src/library/type_context.h
View file

@ -714,7 +714,7 @@ public:
virtual environment const & env() const override { return m_cache->m_env; }
// TODO(Leo): avoid ::lean::mk_fresh_name
virtual name mk_fresh_name() override { return ::lean::mk_fresh_name(); }
virtual name next_name() override { return ::lean::mk_fresh_name(); }
options const & get_options() const { return m_cache->m_options; }
local_context const & lctx() const { return m_lctx; }
@ -1171,7 +1171,7 @@ public:
virtual expr infer(expr const & e) override;
virtual expr whnf(expr const & e) override;
virtual bool is_def_eq(expr const & e1, expr const & e2) override;
virtual name mk_fresh_name() override { return m_ctx.mk_fresh_name(); }
virtual name next_name() override { return m_ctx.next_name(); }
bool match(expr const & e1, expr const & e2);