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

refactor(frontends/lean/elaborator): expose elaborator class

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-03 16:10:36 -07:00
parent dccf8a3a75
commit a1bb6d6017
8 changed files with 1159 additions and 1047 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -7,6 +7,6 @@ begin_end_ext.cpp class.cpp pp_options.cpp tactic_hint.cpp pp.cpp
theorem_queue.cpp structure_cmd.cpp info_manager.cpp no_info.cpp
extra_info.cpp local_context.cpp choice_iterator.cpp
placeholder_elaborator.cpp coercion_elaborator.cpp
proof_qed_elaborator.cpp init_module.cpp)
proof_qed_elaborator.cpp init_module.cpp elaborator_context.cpp)
target_link_libraries(lean_frontend ${LEAN_LIBS})

1
src/frontends/lean/coercion_elaborator.h
View file

@ -7,6 +7,7 @@ Author: Leonardo de Moura
#pragma once
#include "kernel/expr.h"
#include "kernel/type_checker.h"
#include "frontends/lean/choice_iterator.h"
namespace lean {
/** \brief Abstract class for hiding details of the info_manager from the coercion_elaborator */

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

File diff suppressed because it is too large Load diff

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

@ -7,28 +7,138 @@ Author: Leonardo de Moura
#pragma once
#include <utility>
#include "util/list.h"
#include "kernel/environment.h"
#include "kernel/metavar.h"
#include "library/io_state.h"
#include "frontends/lean/local_decls.h"
#include "frontends/lean/info_manager.h"
#include "kernel/type_checker.h"
#include "library/expr_lt.h"
#include "library/unifier.h"
#include "library/tactic/tactic.h"
#include "frontends/lean/elaborator_context.h"
#include "frontends/lean/coercion_elaborator.h"
#include "frontends/lean/util.h"
#include "frontends/lean/local_context.h"
namespace lean {
/** \brief Environment for elaboration, it contains all the information that is "scope-indenpendent" */
class elaborator_context {
environment m_env;
io_state m_ios;
local_decls<level> m_lls; // local universe levels
pos_info_provider const * m_pos_provider;
info_manager * m_info_manager;
/** \brief Mapping from metavariable names to metavariable applications (?M ...) */
typedef name_map<expr> mvar2meta;
// configuration
bool m_check_unassigned;
bool m_use_local_instances;
friend class elaborator;
/** \brief Helper class for implementing the \c elaborate functions. */
class 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;
elaborator_context & m_ctx;
name_generator m_ngen;
type_checker_ptr m_tc[2];
// 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.
local_context m_context; // current local context: a list of local constants
local_context m_full_context; // superset of m_context, it also contains non-contextual locals.
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;
// set of metavariables that we already reported unsolved/unassigned
name_set m_displayed_errors;
// if m_relax_main_opaque is true, then treat opaque definitions from the main module as transparent.
bool m_relax_main_opaque;
// 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;
info_manager m_pre_info_data;
bool m_has_sorry;
unifier_config m_unifier_config;
struct choice_expr_elaborator;
environment const & env() const { return m_ctx.m_env; }
io_state const & ios() const { return m_ctx.m_ios; }
local_decls<level> const & lls() const { return m_ctx.m_lls; }
bool use_local_instances() const { return m_ctx.m_use_local_instances; }
info_manager * infom() const { return m_ctx.m_info_manager; }
pos_info_provider const * pip() const { return m_ctx.m_pos_provider; }
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[m_relax_main_opaque]->infer(e); }
pair<expr, constraint_seq> whnf(expr const & e) { return m_tc[m_relax_main_opaque]->whnf(e); }
expr infer_type(expr const & e, constraint_seq & s) { return m_tc[m_relax_main_opaque]->infer(e, s); }
expr whnf(expr const & e, constraint_seq & s) { return m_tc[m_relax_main_opaque]->whnf(e, s); }
expr mk_app(expr const & f, expr const & a, tag g) { return ::lean::mk_app(f, a).set_tag(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_extra_type_data(expr const & e, expr const & r);
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);
virtual void save_coercion_info(expr const & e, expr const & c);
virtual void erase_coercion_info(expr const & e);
void copy_info_to_manager(substitution s);
expr mk_placeholder_meta(optional<expr> const & type, tag g, bool is_strict, constraint_seq & 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_proof_qed(expr const & e, optional<expr> const & t, constraint_seq & cs);
expr add_implict_args(expr e, constraint_seq & cs, bool relax);
pair<expr, expr> ensure_fun(expr f, constraint_seq & cs);
bool has_coercions_from(expr const & a_type);
bool has_coercions_to(expr d_type);
expr apply_coercion(expr const & a, expr a_type, expr d_type);
pair<expr, constraint_seq> mk_delayed_coercion(expr const & a, expr const & a_type, expr const & expected_type,
justification const & j);
pair<expr, constraint_seq> ensure_has_type(expr const & a, expr const & a_type, expr const & expected_type,
justification const & j, bool relax);
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);
expr visit_let_value(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_proof_state(expr const & mvar, proof_state const & ps, char const * msg);
void check_exact_tacs(expr const & pre_tac, substitution const & s);
optional<expr> get_pre_tactic_for(substitution & subst, expr const & mvar, name_set & visited);
optional<tactic> pre_tactic_to_tactic(expr const & pre_tac, expr const & mvar);
optional<tactic> get_local_tactic_hint(substitution & subst, expr const & mvar, name_set & visited);
bool try_using(substitution & subst, expr const & mvar, proof_state const & ps, tactic const & tac,
bool show_failure);
void solve_unassigned_mvar(substitution & subst, expr mvar, name_set & visited);
expr solve_unassigned_mvars(substitution & subst, expr e, name_set & visited);
expr solve_unassigned_mvars(substitution & subst, expr const & e);
void 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);
std::tuple<expr, level_param_names> apply(substitution & s, expr const & e);
public:
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);
elaborator(elaborator_context & ctx, name_generator const & ngen);
std::tuple<expr, level_param_names> operator()(list<expr> const & ctx, expr const & e, bool _ensure_type,
bool relax_main_opaque);
std::tuple<expr, expr, level_param_names> operator()(expr const & t, expr const & v, name const & n, bool is_opaque);
};
std::tuple<expr, level_param_names> elaborate(elaborator_context & env, list<expr> const & ctx, expr const & e,

38
src/frontends/lean/elaborator_context.cpp Normal file
View file

@ -0,0 +1,38 @@
/*
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/elaborator_context.h"
#ifndef LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES
#define LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES true
#endif
namespace lean {
// ==========================================
// elaborator configuration options
static name * g_elaborator_local_instances = nullptr;
bool get_elaborator_local_instances(options const & opts) {
return opts.get_bool(*g_elaborator_local_instances, LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES);
}
// ==========================================
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):
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());
}
void initialize_elaborator_context() {
g_elaborator_local_instances = new name{"elaborator", "local_instances"};
register_bool_option(*g_elaborator_local_instances, LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES,
"(lean elaborator) use local declarates as class instances");
}
void finalize_elaborator_context() {
delete g_elaborator_local_instances;
}
}

31
src/frontends/lean/elaborator_context.h Normal file
View file

@ -0,0 +1,31 @@
/*
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_decls.h"
#include "frontends/lean/info_manager.h"
namespace lean {
/** \brief Environment for elaboration, it contains all the information that is "scope-indenpendent" */
class elaborator_context {
environment m_env;
io_state m_ios;
local_decls<level> m_lls; // local universe levels
pos_info_provider const * m_pos_provider;
info_manager * m_info_manager;
// configuration
bool m_check_unassigned;
bool m_use_local_instances;
friend class elaborator;
public:
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);
};
void initialize_elaborator_context();
void finalize_elaborator_context();
}

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

@ -5,6 +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/elaborator_context.h"
#include "frontends/lean/elaborator.h"
#include "frontends/lean/pp_options.h"
#include "frontends/lean/parser.h"
@ -33,6 +34,7 @@ void initialize_frontend_lean_module() {
initialize_parse_table();
initialize_builtin_cmds();
initialize_builtin_exprs();
initialize_elaborator_context();
initialize_elaborator();
initialize_pp_options();
initialize_scanner();
@ -67,6 +69,7 @@ void finalize_frontend_lean_module() {
finalize_scanner();
finalize_pp_options();
finalize_elaborator();
finalize_elaborator_context();
finalize_builtin_exprs();
finalize_builtin_cmds();
finalize_parse_table();

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

@ -23,7 +23,7 @@ Author: Leonardo de Moura
#include "library/definition_cache.h"
#include "library/declaration_index.h"
#include "frontends/lean/scanner.h"
#include "frontends/lean/elaborator.h"
#include "frontends/lean/elaborator_context.h"
#include "frontends/lean/local_decls.h"
#include "frontends/lean/parser_config.h"
#include "frontends/lean/parser_pos_provider.h"