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

refactor(frontends/lean): elaborator_context

Browse source
This commit is contained in:
Leonardo de Moura 2016-04-05 16:19:06 -07:00
parent 2577be6344
commit 03809e7973
8 changed files with 61 additions and 57 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/frontends/lean/CMakeLists.txt
View file

@ -11,8 +11,7 @@ parse_tactic_location.cpp parse_rewrite_tactic.cpp builtin_tactics.cpp
type_util.cpp elaborator_exception.cpp local_ref_info.cpp
obtain_expr.cpp decl_attributes.cpp nested_declaration.cpp
parse_with_options_tactic.cpp opt_cmd.cpp prenum.cpp
parse_with_attributes_tactic.cpp print_cmd.cpp
parse_with_attributes_tactic.cpp print_cmd.cpp elaborator_context.cpp
# LEGACY
old_elaborator.cpp
old_elaborator_context.cpp
)

22
src/frontends/lean/old_elaborator_context.cpp → src/frontends/lean/elaborator_context.cpp
View file

@ -6,7 +6,7 @@ Author: Leonardo de Moura
*/
#include "util/sexpr/option_declarations.h"
#include "frontends/lean/parser.h"
#include "frontends/lean/old_elaborator_context.h"
#include "frontends/lean/elaborator_context.h"
#include "frontends/lean/opt_cmd.h"
#ifndef LEAN_DEFAULT_ELABORATOR_FLYCHECK_GOALS
@ -43,19 +43,19 @@ bool get_elaborator_coercions(options const & opts) {
// ==========================================
old_elaborator_context::old_elaborator_context(environment const & env, io_state const & ios, local_level_decls const & lls,
pos_info_provider const * pp, info_manager * info, bool check_unassigned):
elaborator_context::elaborator_context(environment const & env, io_state const & ios, local_level_decls const & lls,
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) {
set_options(ios.get_options());
}
old_elaborator_context::old_elaborator_context(old_elaborator_context const & ctx, options const & o):
elaborator_context::elaborator_context(elaborator_context const & ctx, options const & o):
m_env(ctx.m_env), m_ios(ctx.m_ios), m_lls(ctx.m_lls), m_pos_provider(ctx.m_pos_provider),
m_info_manager(ctx.m_info_manager), m_check_unassigned(ctx.m_check_unassigned) {
set_options(o);
}
void old_elaborator_context::set_options(options const & opts) {
void elaborator_context::set_options(options const & opts) {
m_options = opts;
m_flycheck_goals = get_elaborator_flycheck_goals(opts);
m_lift_coercions = get_elaborator_lift_coercions(opts);
@ -74,7 +74,7 @@ void old_elaborator_context::set_options(options const & opts) {
}
}
bool old_elaborator_context::has_show_goal_at(unsigned & line, unsigned & col) const {
bool elaborator_context::has_show_goal_at(unsigned & line, unsigned & col) const {
if (m_show_goal_at) {
line = m_show_goal_line;
col = m_show_goal_col;
@ -84,11 +84,11 @@ bool old_elaborator_context::has_show_goal_at(unsigned & line, unsigned & col) c
}
}
void old_elaborator_context::reset_show_goal_at() {
void elaborator_context::reset_show_goal_at() {
m_show_goal_at = false;
}
bool old_elaborator_context::has_show_hole_at(unsigned & line, unsigned & col) const {
bool elaborator_context::has_show_hole_at(unsigned & line, unsigned & col) const {
if (m_show_hole_at) {
line = m_show_hole_line;
col = m_show_hole_col;
@ -98,11 +98,11 @@ bool old_elaborator_context::has_show_hole_at(unsigned & line, unsigned & col) c
}
}
void old_elaborator_context::reset_show_hole_at() {
void elaborator_context::reset_show_hole_at() {
m_show_hole_at = false;
}
void initialize_old_elaborator_context() {
void initialize_elaborator_context() {
g_elaborator_flycheck_goals = new name{"elaborator", "flycheck_goals"};
g_elaborator_lift_coercions = new name{"elaborator", "lift_coercions"};
g_elaborator_coercions = new name{"elaborator", "coercions"};
@ -115,7 +115,7 @@ void initialize_old_elaborator_context() {
register_bool_option(*g_elaborator_coercions, LEAN_DEFAULT_ELABORATOR_COERCIONS,
"(elaborator) if true, the elaborator will automatically introduce coercions");
}
void finalize_old_elaborator_context() {
void finalize_elaborator_context() {
delete g_elaborator_flycheck_goals;
delete g_elaborator_lift_coercions;
delete g_elaborator_coercions;

36
src/frontends/lean/old_elaborator_context.h → src/frontends/lean/elaborator_context.h
View file

@ -7,13 +7,18 @@ Author: Leonardo de Moura
#pragma once
#include "kernel/environment.h"
#include "library/io_state.h"
#include "frontends/lean/local_decls.h"
#include "frontends/lean/local_level_decls.h"
#include "frontends/lean/info_manager.h"
namespace lean {
/** \brief Environment for elaboration, it contains all the information that is "scope-indenpendent" */
class old_elaborator_context {
/** \brief Context for the elaborator.
\remark It contains all the information that is "scope-indenpendent".
So, it does not contain the local context because it is context dependent. */
class elaborator_context {
friend class old_elaborator; // TODO(Leo): remove this line when done
friend class elaborator;
environment m_env;
io_state m_ios;
local_level_decls m_lls; // local universe levels
@ -25,15 +30,14 @@ class old_elaborator_context {
bool m_flycheck_goals;
bool m_lift_coercions;
bool m_coercions;
friend class old_elaborator;
bool m_show_goal_at;
unsigned m_show_goal_line;
unsigned m_show_goal_col;
bool m_show_goal_at;
unsigned m_show_goal_line;
unsigned m_show_goal_col;
bool m_show_hole_at;
unsigned m_show_hole_line;
unsigned m_show_hole_col;
bool m_show_hole_at;
unsigned m_show_hole_line;
unsigned m_show_hole_col;
void set_options(options const & opts);
@ -44,11 +48,11 @@ class old_elaborator_context {
bool has_show_hole_at(unsigned & line, unsigned & col) const;
void reset_show_hole_at();
public:
old_elaborator_context(environment const & env, io_state const & ios, local_level_decls const & lls,
pos_info_provider const * pp = nullptr, info_manager * info = nullptr,
bool check_unassigned = true);
old_elaborator_context(old_elaborator_context const & ctx, options const & o);
elaborator_context(environment const & env, io_state const & ios, local_level_decls const & lls,
pos_info_provider const * pp = nullptr, info_manager * info = nullptr,
bool check_unassigned = true);
elaborator_context(elaborator_context const & ctx, options const & o);
};
void initialize_old_elaborator_context();
void finalize_old_elaborator_context();
void initialize_elaborator_context();
void finalize_elaborator_context();
}

6
src/frontends/lean/init_module.cpp
View file

@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "frontends/lean/tokens.h"
#include "frontends/lean/old_elaborator_context.h"
#include "frontends/lean/elaborator_context.h"
#include "frontends/lean/old_elaborator.h"
#include "frontends/lean/parser.h"
#include "frontends/lean/info_annotation.h"
@ -43,7 +43,7 @@ void initialize_frontend_lean_module() {
initialize_builtin_cmds();
initialize_builtin_exprs();
initialize_builtin_tactics();
initialize_old_elaborator_context();
initialize_elaborator_context();
initialize_old_elaborator();
initialize_scanner();
initialize_parser();
@ -84,7 +84,7 @@ void finalize_frontend_lean_module() {
finalize_parser();
finalize_scanner();
finalize_old_elaborator();
finalize_old_elaborator_context();
finalize_elaborator_context();
finalize_builtin_tactics();
finalize_builtin_exprs();
finalize_builtin_cmds();

8
src/frontends/lean/old_elaborator.cpp
View file

@ -173,7 +173,7 @@ struct old_elaborator::choice_expr_elaborator : public choice_iterator {
}
};
old_elaborator::old_elaborator(old_elaborator_context & ctx, bool nice_mvar_names):
old_elaborator::old_elaborator(elaborator_context & ctx, bool nice_mvar_names):
m_ctx(ctx),
m_context(),
m_unifier_config(ctx.m_ios.get_options(), true /* use exceptions */, true /* discard */) {
@ -1881,7 +1881,7 @@ optional<tactic> old_elaborator::pre_tactic_to_tactic(expr const & pre_tac) {
return aux_elaborator.elaborate_nested(g.to_context(), expected_type, e,
use_tactic_hints, subst, report_unassigned);
} else {
old_elaborator_context aux_ctx(m_ctx, o);
elaborator_context aux_ctx(m_ctx, o);
old_elaborator aux_elaborator(aux_ctx);
return aux_elaborator.elaborate_nested(g.to_context(), expected_type, e,
use_tactic_hints, subst, report_unassigned);
@ -2446,12 +2446,12 @@ elaborate_result old_elaborator::elaborate_nested(list<expr> const & ctx, option
static name * g_tmp_prefix = nullptr;
std::tuple<expr, level_param_names> elaborate(old_elaborator_context & 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 ensure_type, bool nice_mvar_names) {
return old_elaborator(env, nice_mvar_names)(ctx, e, ensure_type);
}
std::tuple<expr, expr, level_param_names> elaborate(old_elaborator_context & env, name const & n, expr const & t,
std::tuple<expr, expr, level_param_names> elaborate(elaborator_context & env, name const & n, expr const & t,
expr const & v) {
return old_elaborator(env)(t, v, n);
}

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

@ -15,7 +15,7 @@ Author: Leonardo de Moura
#include "library/tactic/tactic.h"
#include "library/tactic/elaborate.h"
#include "library/old_type_checker.h"
#include "frontends/lean/old_elaborator_context.h"
#include "frontends/lean/elaborator_context.h"
#include "frontends/lean/coercion_elaborator.h"
#include "frontends/lean/util.h"
#include "frontends/lean/obtain_expr.h"
@ -29,7 +29,7 @@ class old_elaborator : public coercion_info_manager {
typedef name_map<expr> local_tactic_hints;
typedef rb_map<expr, pair<expr, constraint_seq>, expr_quick_cmp> cache;
typedef std::vector<pair<expr, expr>> to_check_sorts;
old_elaborator_context & m_ctx;
elaborator_context & m_ctx;
old_type_checker_ptr m_tc;
old_type_checker_ptr m_coercion_from_tc;
old_type_checker_ptr m_coercion_to_tc;
@ -191,15 +191,15 @@ class old_elaborator : public coercion_info_manager {
void show_goal(proof_state const & ps, expr const & start, expr const & end, expr const & curr);
public:
old_elaborator(old_elaborator_context & ctx, bool nice_mvar_names = false);
old_elaborator(elaborator_context & ctx, bool nice_mvar_names = false);
std::tuple<expr, level_param_names> operator()(list<expr> const & ctx, expr const & e, bool _ensure_type);
std::tuple<expr, expr, level_param_names> operator()(expr const & t, expr const & v, name const & n);
};
std::tuple<expr, level_param_names> elaborate(old_elaborator_context & 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 ensure_type = false, bool nice_mvar_names = false);
std::tuple<expr, expr, level_param_names> elaborate(old_elaborator_context & 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);
void initialize_old_elaborator();
void finalize_old_elaborator();
}

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

@ -863,17 +863,17 @@ level parser::parse_level(unsigned rbp) {
return left;
}
old_elaborator_context parser::mk_elaborator_context(pos_info_provider const & pp, bool check_unassigned) {
return old_elaborator_context(m_env, m_ios, m_local_level_decls, &pp, m_info_manager, check_unassigned);
elaborator_context parser::mk_elaborator_context(pos_info_provider const & pp, bool check_unassigned) {
return elaborator_context(m_env, m_ios, m_local_level_decls, &pp, m_info_manager, check_unassigned);
}
old_elaborator_context parser::mk_elaborator_context(environment const & env, pos_info_provider const & pp) {
return old_elaborator_context(env, m_ios, m_local_level_decls, &pp, m_info_manager, true);
elaborator_context parser::mk_elaborator_context(environment const & env, pos_info_provider const & pp) {
return elaborator_context(env, m_ios, m_local_level_decls, &pp, m_info_manager, true);
}
old_elaborator_context parser::mk_elaborator_context(environment const & env, local_level_decls const & lls,
elaborator_context parser::mk_elaborator_context(environment const & env, local_level_decls const & lls,
pos_info_provider const & pp) {
return old_elaborator_context(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::old_elaborate_relaxed(expr const & e, list<expr> const & ctx) {
@ -881,7 +881,7 @@ std::tuple<expr, level_param_names> parser::old_elaborate_relaxed(expr const & e
bool ensure_type = false;
bool nice_mvar_names = true;
parser_pos_provider pp = get_pos_provider();
old_elaborator_context env = mk_elaborator_context(pp, check_unassigned);
elaborator_context env = mk_elaborator_context(pp, check_unassigned);
auto r = ::lean::elaborate(env, ctx, e, ensure_type, nice_mvar_names);
m_pre_info_manager.clear();
return r;
@ -891,7 +891,7 @@ std::tuple<expr, level_param_names> parser::old_elaborate(expr const & e, list<e
bool check_unassigned = true;
bool ensure_type = false;
parser_pos_provider pp = get_pos_provider();
old_elaborator_context env = mk_elaborator_context(pp, check_unassigned);
elaborator_context env = mk_elaborator_context(pp, check_unassigned);
auto r = ::lean::elaborate(env, ctx, e, ensure_type);
m_pre_info_manager.clear();
return r;
@ -901,7 +901,7 @@ std::tuple<expr, level_param_names> parser::old_elaborate_type(expr const & e, l
bool check_unassigned = true;
bool ensure_type = true;
parser_pos_provider pp = get_pos_provider();
old_elaborator_context env = mk_elaborator_context(pp, check_unassigned);
elaborator_context env = mk_elaborator_context(pp, check_unassigned);
auto r = ::lean::elaborate(env, ctx, e, ensure_type);
if (clear_pre_info)
m_pre_info_manager.clear();
@ -910,7 +910,7 @@ std::tuple<expr, level_param_names> parser::old_elaborate_type(expr const & e, l
std::tuple<expr, level_param_names> parser::old_elaborate_at(environment const & env, expr const & e) {
parser_pos_provider pp = get_pos_provider();
old_elaborator_context eenv = mk_elaborator_context(env, pp);
elaborator_context eenv = mk_elaborator_context(env, pp);
auto r = ::lean::elaborate(eenv, list<expr>(), e);
m_pre_info_manager.clear();
return r;
@ -919,7 +919,7 @@ std::tuple<expr, level_param_names> parser::old_elaborate_at(environment const &
auto parser::old_elaborate_definition(name const & n, expr const & t, expr const & v)
-> std::tuple<expr, expr, level_param_names> {
parser_pos_provider pp = get_pos_provider();
old_elaborator_context eenv = mk_elaborator_context(pp);
elaborator_context eenv = mk_elaborator_context(pp);
auto r = ::lean::elaborate(eenv, n, t, v);
m_pre_info_manager.clear();
return r;
@ -929,7 +929,7 @@ auto parser::old_elaborate_definition_at(environment const & env, local_level_de
name const & n, expr const & t, expr const & v)
-> std::tuple<expr, expr, level_param_names> {
parser_pos_provider pp = get_pos_provider();
old_elaborator_context eenv = mk_elaborator_context(env, lls, pp);
elaborator_context eenv = mk_elaborator_context(env, lls, pp);
auto r = ::lean::elaborate(eenv, n, t, v);
m_pre_info_manager.clear();
return r;

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

@ -19,7 +19,7 @@ Author: Leonardo de Moura
#include "library/definition_cache.h"
#include "library/declaration_index.h"
#include "frontends/lean/scanner.h"
#include "frontends/lean/old_elaborator_context.h"
#include "frontends/lean/elaborator_context.h"
#include "frontends/lean/local_decls.h"
#include "frontends/lean/local_level_decls.h"
#include "frontends/lean/parser_config.h"
@ -233,9 +233,10 @@ class parser {
void commit_info(unsigned line, unsigned col);
void commit_info() { commit_info(m_scanner.get_line(), m_scanner.get_pos()); }
old_elaborator_context mk_elaborator_context(pos_info_provider const & pp, bool check_unassigned = true);
old_elaborator_context mk_elaborator_context(environment const & env, pos_info_provider const & pp);
old_elaborator_context mk_elaborator_context(environment const & env, local_level_decls const & lls, pos_info_provider const & pp);
elaborator_context mk_elaborator_context(pos_info_provider const & pp, bool check_unassigned = true);
elaborator_context mk_elaborator_context(environment const & env, pos_info_provider const & pp);
elaborator_context mk_elaborator_context(environment const & env, local_level_decls const & lls,
pos_info_provider const & pp);
bool m_in_backtick; // true if parser `expr` notation
expr parse_backtick_expr_core();