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

chore(frontends/lean): remove old elaborator

Browse source
This commit is contained in:
Leonardo de Moura 2016-09-19 17:10:28 -07:00
parent 9f1a576e98
commit f6aba503ff
9 changed files with 0 additions and 2242 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -9,10 +9,7 @@ type_util.cpp local_ref_info.cpp decl_attributes.cpp nested_declaration.cpp
opt_cmd.cpp prenum.cpp print_cmd.cpp elaborator.cpp
match_expr.cpp local_context_adapter.cpp decl_util.cpp definition_cmds.cpp
# LEGACY
old_elaborator.cpp
old_attributes.cpp
old_elaborator_exception.cpp
elaborator_context.cpp
# begin_end_annotation.cpp tactic_hint.cpp
# info_tactic.cpp
# parse_tactic_location.cpp parse_rewrite_tactic.cpp builtin_tactics.cpp

119
src/frontends/lean/elaborator_context.cpp
View file

@ -1,119 +0,0 @@
/*
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "util/sexpr/option_declarations.h"
#include "frontends/lean/parser.h"
#include "frontends/lean/elaborator_context.h"
#include "frontends/lean/opt_cmd.h"
#ifndef LEAN_DEFAULT_ELABORATOR_FLYCHECK_GOALS
#define LEAN_DEFAULT_ELABORATOR_FLYCHECK_GOALS false
#endif
#ifndef LEAN_DEFAULT_ELABORATOR_LIFT_COERCIONS
#define LEAN_DEFAULT_ELABORATOR_LIFT_COERCIONS true
#endif
#ifndef LEAN_DEFAULT_ELABORATOR_COERCIONS
#define LEAN_DEFAULT_ELABORATOR_COERCIONS false
#endif
namespace lean {
// ==========================================
// elaborator configuration options
static name * g_elaborator_flycheck_goals = nullptr;
static name * g_elaborator_lift_coercions = nullptr;
static name * g_elaborator_coercions = nullptr;
bool get_elaborator_flycheck_goals(options const & opts) {
return opts.get_bool(*g_elaborator_flycheck_goals, LEAN_DEFAULT_ELABORATOR_FLYCHECK_GOALS);
}
bool get_elaborator_lift_coercions(options const & opts) {
return opts.get_bool(*g_elaborator_lift_coercions, LEAN_DEFAULT_ELABORATOR_LIFT_COERCIONS);
}
bool get_elaborator_coercions(options const & opts) {
return opts.get_bool(*g_elaborator_coercions, LEAN_DEFAULT_ELABORATOR_COERCIONS);
}
// ==========================================
elaborator_context::elaborator_context(environment const & env, options const & opts, local_level_decls const & lls,
bool check_unassigned):
m_env(env), m_lls(lls), m_check_unassigned(check_unassigned) {
set_options(opts);
}
elaborator_context::elaborator_context(elaborator_context const & ctx, options const & o):
m_env(ctx.m_env), m_lls(ctx.m_lls),
m_check_unassigned(ctx.m_check_unassigned) {
set_options(o);
}
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);
m_coercions = get_elaborator_coercions(opts);
if (has_show_goal(opts, m_show_goal_line, m_show_goal_col)) {
m_show_goal_at = true;
} else {
m_show_goal_at = false;
}
if (has_show_hole(opts, m_show_hole_line, m_show_hole_col)) {
m_show_hole_at = true;
} else {
m_show_hole_at = false;
}
}
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;
return true;
} else {
return false;
}
}
void elaborator_context::reset_show_goal_at() {
m_show_goal_at = false;
}
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;
return true;
} else {
return false;
}
}
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"};
register_bool_option(*g_elaborator_flycheck_goals, LEAN_DEFAULT_ELABORATOR_FLYCHECK_GOALS,
"(elaborator) if true, then elaborator display current goals for flycheck before each "
"tactic is executed in a `begin ... end` block");
register_bool_option(*g_elaborator_lift_coercions, LEAN_DEFAULT_ELABORATOR_LIFT_COERCIONS,
"(elaborator) if true, the elaborator will automatically lift coercions from A to B "
"into coercions from (C -> A) to (C -> B)");
register_bool_option(*g_elaborator_coercions, LEAN_DEFAULT_ELABORATOR_COERCIONS,
"(elaborator) if true, the elaborator will automatically introduce coercions");
}
void finalize_elaborator_context() {
delete g_elaborator_flycheck_goals;
delete g_elaborator_lift_coercions;
delete g_elaborator_coercions;
}
}

53
src/frontends/lean/elaborator_context.h
View file

@ -1,53 +0,0 @@
/*
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "kernel/environment.h"
#include "library/io_state.h"
#include "frontends/lean/local_level_decls.h"
#include "frontends/lean/info_manager.h"
namespace lean {
/** \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;
local_level_decls m_lls; // local universe levels
// configuration
options m_options;
bool m_check_unassigned;
bool m_flycheck_goals;
bool m_lift_coercions;
bool m_coercions;
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;
void set_options(options const & opts);
/** \brief Support for showing information using hot-keys */
bool has_show_goal_at(unsigned & line, unsigned & col) const;
void reset_show_goal_at();
bool has_show_hole_at(unsigned & line, unsigned & col) const;
public:
elaborator_context(environment const & env, options const & opts, local_level_decls const & lls,
bool check_unassigned = true);
elaborator_context(elaborator_context const & ctx, options const & o);
};
void initialize_elaborator_context();
void finalize_elaborator_context();
}

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

@ -5,8 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "frontends/lean/tokens.h"
#include "frontends/lean/elaborator_context.h"
#include "frontends/lean/old_elaborator.h"
#include "frontends/lean/parser.h"
#include "frontends/lean/info_annotation.h"
#include "frontends/lean/parser_config.h"
@ -40,8 +38,6 @@ void initialize_frontend_lean_module() {
initialize_parse_table();
initialize_builtin_cmds();
initialize_builtin_exprs();
initialize_elaborator_context();
initialize_old_elaborator();
initialize_scanner();
initialize_parser();
initialize_parser_config();
@ -75,8 +71,6 @@ void finalize_frontend_lean_module() {
finalize_parser_config();
finalize_parser();
finalize_scanner();
finalize_old_elaborator();
finalize_elaborator_context();
finalize_builtin_exprs();
finalize_builtin_cmds();
finalize_parse_table();

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

File diff suppressed because it is too large Load diff

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

@ -1,187 +0,0 @@
/*
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include <utility>
#include <vector>
#include "util/list.h"
#include "library/metavar.h"
#include "library/expr_lt.h"
#include "library/unifier.h"
#include "library/old_local_context.h"
#include "library/old_type_checker.h"
#include "library/tactic/tactic_state.h"
#include "frontends/lean/elaborator_context.h"
#include "frontends/lean/util.h"
namespace lean {
/** \brief Mapping from metavariable names to metavariable applications (?M ...) */
typedef name_map<expr> mvar2meta;
/** \brief Helper class for implementing the \c elaborate functions. */
class old_elaborator {
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;
elaborator_context & m_ctx;
old_type_checker_ptr m_tc;
// 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.
old_local_context m_context; // current local context: a list of local constants
mvar2meta m_mvar2meta;
cache m_cache;
// The following vector contains sorts that we should check
// whether the computed universe is too specific or not.
to_check_sorts m_to_check_sorts;
// 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.
local_tactic_hints m_local_tactic_hints;
name_set m_used_local_tactic_hints;
// set of metavariables that we already reported unsolved/unassigned
name_set m_displayed_errors;
// if m_no_info is true, we do not collect information when true,
// we set is to true whenever we find no_info annotation.
bool m_no_info;
// if m_in_equation_lhs is true, we are processing the left-hand-side of an equation
// and inaccessible expressions are allowed
bool m_in_equation_lhs;
// if m_equation_lhs is not none, we are processing the right-hand-side of an equation
optional<expr> m_equation_lhs;
// if m_equation_R is not none when elaborator is processing recursive equation using the well-founded relation R.
optional<expr> m_equation_R;
bool m_use_tactic_hints;
info_manager m_pre_info_data;
bool m_has_sorry;
unifier_config m_unifier_config;
// If m_nice_mvar_names is true, we append (when possible) a more informative name for a metavariable.
// That is, whenever a metavariables comes from a binding, we add the binding name as a suffix
bool m_nice_mvar_names;
optional<expr> m_type;
optional<expr> m_to_show_hole; // type information for "show hole" command line
expr m_to_show_hole_ref; // provide position information
struct choice_expr_elaborator;
environment const & env() const { return m_ctx.m_env; }
local_level_decls const & lls() const { return m_ctx.m_lls; }
bool check_unassigned() const { return m_ctx.m_check_unassigned; }
expr mk_local(name const & n, expr const & t, binder_info const & bi);
pair<expr, constraint_seq> infer_type(expr const & e) { return m_tc->infer(e); }
pair<expr, constraint_seq> whnf(expr const & e) { return m_tc->whnf(e); }
expr infer_type(expr const & e, constraint_seq & s) { return m_tc->infer(e, s); }
expr whnf(expr const & e, constraint_seq & s) { return m_tc->whnf(e, s); }
bool is_def_eq(expr const & e1, expr const & e2, justification const & j, constraint_seq & cs) {
return m_tc->is_def_eq(e1, e2, j, cs);
}
expr mk_app(expr const & f, expr const & a, tag g) { return ::lean::mk_app(f, a, g); }
void register_meta(expr const & meta);
optional<expr> mvar_to_meta(expr const & mvar);
void save_type_data(expr const & e, expr const & r);
void save_binder_type(expr const & e, expr const & r);
void save_extra_type_data(expr const & e, expr const & r);
// void save_proof_state_info(proof_state const & ps, expr const & e);
void save_identifier_info(expr const & f);
void save_synth_data(expr const & e, expr const & r);
void save_placeholder_info(expr const & e, expr const & r);
void instantiate_info(substitution s);
/** \brief If info manager is being used, then create a metavariable suffix based on binding_name(b) */
optional<name> mk_mvar_suffix(expr const & b);
expr mk_placeholder_meta(optional<name> const & suffix, optional<expr> const & type,
tag g, bool is_strict, bool inst_implicit, constraint_seq & cs);
expr mk_placeholder_meta(optional<expr> const & type, tag g, bool is_strict, bool inst_implicit, constraint_seq & cs) {
return mk_placeholder_meta(optional<name>(), type, g, is_strict, inst_implicit, cs);
}
expr visit_expecting_type(expr const & e, constraint_seq & cs);
expr visit_expecting_type_of(expr const & e, expr const & t, constraint_seq & cs);
expr visit_choice(expr const & e, optional<expr> const & t, constraint_seq & cs);
expr visit_by(expr const & e, optional<expr> const & t, constraint_seq & cs);
expr visit_calc_proof(expr const & e, optional<expr> const & t, constraint_seq & cs);
expr add_implict_args(expr e, constraint_seq & cs);
pair<expr, expr> ensure_fun(expr f, constraint_seq & cs);
pair<expr, constraint_seq> ensure_has_type_core(expr const & a, expr const & a_type, expr const & expected_type,
bool use_expensive_coercions, justification const & j);
pair<expr, constraint_seq> ensure_has_type(expr const & a, expr const & a_type, expr const & expected_type,
justification const & j) {
return ensure_has_type_core(a, a_type, expected_type, true, j);
}
bool is_choice_app(expr const & e);
expr visit_choice_app(expr const & e, constraint_seq & cs);
expr visit_app(expr const & e, constraint_seq & cs);
expr visit_placeholder(expr const & e, constraint_seq & cs);
level replace_univ_placeholder(level const & l);
expr visit_sort(expr const & e);
expr visit_macro(expr const & e, constraint_seq & cs);
expr visit_constant(expr const & e);
expr ensure_type(expr const & e, constraint_seq & cs);
expr instantiate_rev_locals(expr const & a, unsigned n, expr const * subst);
expr visit_binding(expr e, expr_kind k, constraint_seq & cs);
expr visit_pi(expr const & e, constraint_seq & cs);
expr visit_lambda(expr const & e, constraint_seq & cs);
expr visit_typed_expr(expr const & e, constraint_seq & cs);
bool is_sorry(expr const & e) const;
expr visit_sorry(expr const & e);
expr visit_core(expr const & e, constraint_seq & cs);
pair<expr, constraint_seq> visit(expr const & e);
expr visit(expr const & e, constraint_seq & cs);
unify_result_seq solve(constraint_seq const & cs);
void display_unsolved_tactic_state(expr const & mvar, tactic_state const & ts, format const & fmt,
expr const & pos);
void display_unsolved_tactic_state(expr const & mvar, tactic_state const & ts, char const * msg,
expr const & pos);
void display_unsolved_tactic_state(expr const & mvar, tactic_state const & ps, char const * msg);
// void display_unsolved_subgoals(expr const & mvar, proof_state const & ps, expr const & pos);
// void display_unsolved_subgoals(expr const & mvar, proof_state const & ps);
// void display_tactic_exception(tactic_exception const & ex, proof_state const & ps, expr const & pre_tac);
optional<expr> get_tactic_for(expr const & mvar);
optional<tactic_state> execute_tactic(expr const & tactic, tactic_state const & s, expr const & mvar);
// optional<tactic> pre_tactic_to_tactic(expr const & pre_tac);
// bool try_using(substitution & subst, expr const & mvar, proof_state const & ps,
// expr const & pre_tac, tactic const & tac, bool show_failure);
// bool try_using_begin_end(substitution & subst, expr const & mvar, proof_state ps, expr const & pre_tac);
void solve_unassigned_mvar(substitution & subst, expr mvar, name_set & visited, bool reject_type_is_meta);
expr solve_unassigned_mvars(substitution & subst, expr e, name_set & visited, bool reject_type_is_meta);
expr solve_unassigned_mvars(substitution & subst, expr const & e, bool reject_type_is_meta);
bool display_unassigned_mvars(expr const & e, substitution const & s);
void check_sort_assignments(substitution const & s);
expr apply(substitution & s, expr const & e, name_set & univ_params, buffer<name> & new_params, bool is_def_value);
std::tuple<expr, level_param_names> apply(substitution & s, expr const & e, bool is_def_value);
// elaborate_result elaborate_nested(list<expr> const & ctx, optional<expr> const & expected_type, expr const & e,
// bool use_tactic_hints, substitution const &, bool report_unassigned);
expr const & get_equation_fn(expr const & eq) const;
expr visit_equations(expr const & eqns, constraint_seq & cs);
expr visit_equation(expr const & e, constraint_seq & cs);
expr visit_inaccessible(expr const & e, constraint_seq & cs);
constraint mk_equations_cnstr(expr const & m, expr const & eqns);
bool is_structure_like(expr const & S);
expr visit_structure_instance(expr const & e, constraint_seq & cs);
expr visit_prenum(expr const & e, constraint_seq & cs);
expr visit_checkpoint_expr(expr const & e, constraint_seq & cs);
void check_used_local_tactic_hints();
// void show_goal(proof_state const & ps, expr const & start, expr const & end, expr const & curr);
public:
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(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(elaborator_context & env, name const & n, expr const & t, expr const & v);
void initialize_old_elaborator();
void finalize_old_elaborator();
}

26
src/frontends/lean/old_elaborator_exception.cpp
View file

@ -1,26 +0,0 @@
/*
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "library/exception.h"
#include "frontends/lean/old_elaborator_exception.h"
namespace lean {
[[ noreturn ]] void throw_elaborator_exception(char const * msg, expr const & m) {
throw generic_exception(m, msg);
}
[[ noreturn ]] void throw_elaborator_exception(sstream const & strm, expr const & m) {
throw generic_exception(m, strm);
}
[[ noreturn ]] void throw_elaborator_exception(expr const & m, pp_fn const & fn) {
throw generic_exception(m, fn);
}
[[ noreturn ]] void throw_elaborator_exception(expr const & m, format const & msg) {
throw_elaborator_exception(m, [=](formatter const &) { return msg; });
}
}

16
src/frontends/lean/old_elaborator_exception.h
View file

@ -1,16 +0,0 @@
/*
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "kernel/environment.h"
#include "kernel/formatter.h"
namespace lean {
[[ noreturn ]] void throw_elaborator_exception(char const * msg, expr const & m);
[[ noreturn ]] void throw_elaborator_exception(sstream const & strm, expr const & m);
[[ noreturn ]] void throw_elaborator_exception(expr const & m, format const & msg);
[[ noreturn ]] void throw_elaborator_exception(expr const & m, pp_fn const & fn);
}

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

@ -19,7 +19,6 @@ Author: Leonardo de Moura
#include "library/definition_cache.h"
#include "library/declaration_index.h"
#include "frontends/lean/scanner.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"
@ -222,10 +221,6 @@ class parser : public abstract_parser {
void commit_info(unsigned line, unsigned col);
void commit_info() { commit_info(m_scanner.get_line(), m_scanner.get_pos()); }
elaborator_context mk_elaborator_context(bool check_unassigned = true);
elaborator_context mk_elaborator_context(environment const & env);
elaborator_context mk_elaborator_context(environment const & env, local_level_decls const & lls);
void init_stop_at(options const & opts);
void replace_theorem(certified_declaration const & thm);