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

refactor(frontends/lean): rename elaborator_env to elaborator_context

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-13 12:45:57 -07:00
parent 28d23390a6
commit d30854829d
4 changed files with 34 additions and 34 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

30
src/frontends/lean/elaborator.cpp
View file

@ -122,8 +122,8 @@ public:
expr operator()(expr const & e) { return apply(e); } expr operator()(expr const & e) { return apply(e); }
}; };
elaborator_env::elaborator_env(environment const & env, io_state const & ios, local_decls<level> const & lls, elaborator_context::elaborator_context(environment const & env, io_state const & ios, local_decls<level> const & lls,
pos_info_provider const * pp, info_manager * info, bool check_unassigned): pos_info_provider const * pp, info_manager * info, bool check_unassigned):
m_env(env), m_ios(ios), m_lls(lls), m_pos_provider(pp), m_info_manager(info), m_check_unassigned(check_unassigned) { m_env(env), m_ios(ios), m_lls(lls), m_pos_provider(pp), m_info_manager(info), m_check_unassigned(check_unassigned) {
m_use_local_instances = get_elaborator_local_instances(ios.get_options()); m_use_local_instances = get_elaborator_local_instances(ios.get_options());
} }
@ -292,19 +292,19 @@ class elaborator {
typedef name_map<expr> local_tactic_hints; typedef name_map<expr> local_tactic_hints;
typedef std::unique_ptr<type_checker> type_checker_ptr; typedef std::unique_ptr<type_checker> type_checker_ptr;
elaborator_env & m_env; elaborator_context & m_env;
name_generator m_ngen; name_generator m_ngen;
type_checker_ptr m_tc[2]; type_checker_ptr m_tc[2];
mvar2meta m_mvar2meta; // mapping from metavariable ?m to the (?m l_1 ... l_n) where [l_1 ... l_n] are the local constants mvar2meta m_mvar2meta; // mapping from metavariable ?m to the (?m l_1 ... l_n) where [l_1 ... l_n] are the local constants
// representing the context where ?m was created. // representing the context where ?m was created.
context m_context; // current local context: a list of local constants context m_context; // current local context: a list of local constants
context m_full_context; // superset of m_context, it also contains non-contextual locals. context m_full_context; // superset of m_context, it also contains non-contextual locals.
constraint_vect m_constraints; // constraints that must be solved for the elaborated term to be type correct. constraint_vect m_constraints; // constraints that must be solved for the elaborated term to be type correct.
local_tactic_hints m_local_tactic_hints; // mapping from metavariable name ?m to tactic expression that should be used to solve it. local_tactic_hints m_local_tactic_hints; // mapping from metavariable name ?m to tactic expression that should be used to solve it.
// this mapping is populated by the 'by tactic-expr' expression. // this mapping is populated by the 'by tactic-expr' expression.
name_set m_displayed_errors; // set of metavariables that we already reported unsolved/unassigned name_set m_displayed_errors; // set of metavariables that we already reported unsolved/unassigned
bool m_relax_main_opaque; // if true, then treat opaque definitions from the main module as transparent bool m_relax_main_opaque; // if true, then treat opaque definitions from the main module as transparent
std::vector<type_info_data> m_pre_info_data; std::vector<type_info_data> m_pre_info_data;
struct scope_ctx { struct scope_ctx {
@ -512,7 +512,7 @@ class elaborator {
} }
public: public:
elaborator(elaborator_env & env, list<expr> const & ctx, name_generator const & ngen): elaborator(elaborator_context & env, list<expr> const & ctx, name_generator const & ngen):
m_env(env), m_env(env),
m_ngen(ngen), m_ngen(ngen),
m_context(m_ngen, m_mvar2meta, ctx), m_context(m_ngen, m_mvar2meta, ctx),
@ -1285,12 +1285,12 @@ public:
static name g_tmp_prefix = name::mk_internal_unique_name(); static name g_tmp_prefix = name::mk_internal_unique_name();
std::tuple<expr, level_param_names> elaborate(elaborator_env & env, list<expr> const & ctx, expr const & e, std::tuple<expr, level_param_names> elaborate(elaborator_context & env, list<expr> const & ctx, expr const & e,
bool relax_main_opaque, bool ensure_type) { bool relax_main_opaque, bool ensure_type) {
return elaborator(env, ctx, name_generator(g_tmp_prefix))(e, ensure_type, relax_main_opaque); return elaborator(env, ctx, name_generator(g_tmp_prefix))(e, ensure_type, relax_main_opaque);
} }
std::tuple<expr, expr, level_param_names> elaborate(elaborator_env & env, name const & n, expr const & t, expr const & v, std::tuple<expr, expr, level_param_names> elaborate(elaborator_context & env, name const & n, expr const & t, expr const & v,
bool is_opaque) { bool is_opaque) {
return elaborator(env, list<expr>(), name_generator(g_tmp_prefix))(t, v, n, is_opaque); return elaborator(env, list<expr>(), name_generator(g_tmp_prefix))(t, v, n, is_opaque);
} }

10
src/frontends/lean/elaborator.h
View file

@ -15,7 +15,7 @@ Author: Leonardo de Moura
namespace lean { namespace lean {
/** \brief Environment for elaboration, it contains all the information that is "scope-indenpendent" */ /** \brief Environment for elaboration, it contains all the information that is "scope-indenpendent" */
class elaborator_env { class elaborator_context {
environment m_env; environment m_env;
io_state m_ios; io_state m_ios;
local_decls<level> m_lls; // local universe levels local_decls<level> m_lls; // local universe levels
@ -27,13 +27,13 @@ class elaborator_env {
bool m_use_local_instances; bool m_use_local_instances;
friend class elaborator; friend class elaborator;
public: public:
elaborator_env(environment const & env, io_state const & ios, local_decls<level> const & lls, elaborator_context(environment const & env, io_state const & ios, local_decls<level> const & lls,
pos_info_provider const * pp = nullptr, info_manager * info = nullptr, bool check_unassigned = true); pos_info_provider const * pp = nullptr, info_manager * info = nullptr, bool check_unassigned = true);
}; };
std::tuple<expr, level_param_names> elaborate(elaborator_env & env, list<expr> const & ctx, expr const & e, std::tuple<expr, level_param_names> elaborate(elaborator_context & env, list<expr> const & ctx, expr const & e,
bool relax_main_opaque, bool ensure_type = false); bool relax_main_opaque, bool ensure_type = false);
std::tuple<expr, expr, level_param_names> elaborate(elaborator_env & env, name const & n, expr const & t, expr const & v, std::tuple<expr, expr, level_param_names> elaborate(elaborator_context & env, name const & n, expr const & t, expr const & v,
bool is_opaque); bool is_opaque);
} }

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

@ -517,16 +517,16 @@ level parser::parse_level(unsigned rbp) {
return left; return left;
} }
elaborator_env parser::mk_elaborator_env(pos_info_provider const & pp, bool check_unassigned) { elaborator_context parser::mk_elaborator_context(pos_info_provider const & pp, bool check_unassigned) {
return elaborator_env(m_env, m_ios, m_local_level_decls, &pp, m_info_manager, check_unassigned); return elaborator_context(m_env, m_ios, m_local_level_decls, &pp, m_info_manager, check_unassigned);
} }
elaborator_env parser::mk_elaborator_env(environment const & env, pos_info_provider const & pp) { elaborator_context parser::mk_elaborator_context(environment const & env, pos_info_provider const & pp) {
return elaborator_env(env, m_ios, m_local_level_decls, &pp, m_info_manager, true); return elaborator_context(env, m_ios, m_local_level_decls, &pp, m_info_manager, true);
} }
elaborator_env parser::mk_elaborator_env(environment const & env, local_level_decls const & lls, pos_info_provider const & pp) { elaborator_context parser::mk_elaborator_context(environment const & env, local_level_decls const & lls, pos_info_provider const & pp) {
return elaborator_env(env, m_ios, lls, &pp, m_info_manager, true); return elaborator_context(env, m_ios, lls, &pp, m_info_manager, true);
} }
std::tuple<expr, level_param_names> parser::elaborate_relaxed(expr const & e, list<expr> const & ctx) { std::tuple<expr, level_param_names> parser::elaborate_relaxed(expr const & e, list<expr> const & ctx) {
@ -534,7 +534,7 @@ std::tuple<expr, level_param_names> parser::elaborate_relaxed(expr const & e, li
bool check_unassigned = false; bool check_unassigned = false;
bool ensure_type = false; bool ensure_type = false;
parser_pos_provider pp = get_pos_provider(); parser_pos_provider pp = get_pos_provider();
elaborator_env env = mk_elaborator_env(pp, check_unassigned); elaborator_context env = mk_elaborator_context(pp, check_unassigned);
auto r = ::lean::elaborate(env, ctx, e, relax, ensure_type); auto r = ::lean::elaborate(env, ctx, e, relax, ensure_type);
m_pre_info_data.clear(); m_pre_info_data.clear();
return r; return r;
@ -545,7 +545,7 @@ std::tuple<expr, level_param_names> parser::elaborate_type(expr const & e, list<
bool check_unassigned = true; bool check_unassigned = true;
bool ensure_type = true; bool ensure_type = true;
parser_pos_provider pp = get_pos_provider(); parser_pos_provider pp = get_pos_provider();
elaborator_env env = mk_elaborator_env(pp, check_unassigned); elaborator_context env = mk_elaborator_context(pp, check_unassigned);
auto r = ::lean::elaborate(env, ctx, e, relax, ensure_type); auto r = ::lean::elaborate(env, ctx, e, relax, ensure_type);
m_pre_info_data.clear(); m_pre_info_data.clear();
return r; return r;
@ -554,7 +554,7 @@ std::tuple<expr, level_param_names> parser::elaborate_type(expr const & e, list<
std::tuple<expr, level_param_names> parser::elaborate_at(environment const & env, expr const & e) { std::tuple<expr, level_param_names> parser::elaborate_at(environment const & env, expr const & e) {
bool relax = false; bool relax = false;
parser_pos_provider pp = get_pos_provider(); parser_pos_provider pp = get_pos_provider();
elaborator_env eenv = mk_elaborator_env(env, pp); elaborator_context eenv = mk_elaborator_context(env, pp);
auto r = ::lean::elaborate(eenv, list<expr>(), e, relax); auto r = ::lean::elaborate(eenv, list<expr>(), e, relax);
m_pre_info_data.clear(); m_pre_info_data.clear();
return r; return r;
@ -563,7 +563,7 @@ std::tuple<expr, level_param_names> parser::elaborate_at(environment const & env
std::tuple<expr, expr, level_param_names> parser::elaborate_definition(name const & n, expr const & t, expr const & v, std::tuple<expr, expr, level_param_names> parser::elaborate_definition(name const & n, expr const & t, expr const & v,
bool is_opaque) { bool is_opaque) {
parser_pos_provider pp = get_pos_provider(); parser_pos_provider pp = get_pos_provider();
elaborator_env eenv = mk_elaborator_env(pp); elaborator_context eenv = mk_elaborator_context(pp);
auto r = ::lean::elaborate(eenv, n, t, v, is_opaque); auto r = ::lean::elaborate(eenv, n, t, v, is_opaque);
m_pre_info_data.clear(); m_pre_info_data.clear();
return r; return r;
@ -572,7 +572,7 @@ std::tuple<expr, expr, level_param_names> parser::elaborate_definition(name cons
std::tuple<expr, expr, level_param_names> parser::elaborate_definition_at(environment const & env, local_level_decls const & lls, std::tuple<expr, expr, level_param_names> parser::elaborate_definition_at(environment const & env, local_level_decls const & lls,
name const & n, expr const & t, expr const & v, bool is_opaque) { name const & n, expr const & t, expr const & v, bool is_opaque) {
parser_pos_provider pp = get_pos_provider(); parser_pos_provider pp = get_pos_provider();
elaborator_env eenv = mk_elaborator_env(env, lls, pp); elaborator_context eenv = mk_elaborator_context(env, lls, pp);
auto r = ::lean::elaborate(eenv, n, t, v, is_opaque); auto r = ::lean::elaborate(eenv, n, t, v, is_opaque);
m_pre_info_data.clear(); m_pre_info_data.clear();
return r; return r;

6
src/frontends/lean/parser.h
View file

@ -163,9 +163,9 @@ class parser {
void save_type_info(expr const & e); void save_type_info(expr const & e);
void save_pre_info_data(); void save_pre_info_data();
elaborator_env mk_elaborator_env(pos_info_provider const & pp, bool check_unassigned = true); elaborator_context mk_elaborator_context(pos_info_provider const & pp, bool check_unassigned = true);
elaborator_env mk_elaborator_env(environment const & env, pos_info_provider const & pp); elaborator_context mk_elaborator_context(environment const & env, pos_info_provider const & pp);
elaborator_env mk_elaborator_env(environment const & env, local_level_decls const & lls, pos_info_provider const & pp); elaborator_context mk_elaborator_context(environment const & env, local_level_decls const & lls, pos_info_provider const & pp);
public: public:
parser(environment const & env, io_state const & ios, parser(environment const & env, io_state const & ios,