From f6aba503ff74395df53668c2129f7773d7919bef Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 19 Sep 2016 17:10:28 -0700 Subject: [PATCH] chore(frontends/lean): remove old elaborator --- src/frontends/lean/CMakeLists.txt | 3 - src/frontends/lean/elaborator_context.cpp | 119 -- src/frontends/lean/elaborator_context.h | 53 - src/frontends/lean/init_module.cpp | 6 - src/frontends/lean/old_elaborator.cpp | 1827 ----------------- src/frontends/lean/old_elaborator.h | 187 -- .../lean/old_elaborator_exception.cpp | 26 - src/frontends/lean/old_elaborator_exception.h | 16 - src/frontends/lean/parser.h | 5 - 9 files changed, 2242 deletions(-) delete mode 100644 src/frontends/lean/elaborator_context.cpp delete mode 100644 src/frontends/lean/elaborator_context.h delete mode 100644 src/frontends/lean/old_elaborator.cpp delete mode 100644 src/frontends/lean/old_elaborator.h delete mode 100644 src/frontends/lean/old_elaborator_exception.cpp delete mode 100644 src/frontends/lean/old_elaborator_exception.h diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt index 3a7657ad01..7d7403ff61 100644 --- a/src/frontends/lean/CMakeLists.txt +++ b/src/frontends/lean/CMakeLists.txt @@ -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 diff --git a/src/frontends/lean/elaborator_context.cpp b/src/frontends/lean/elaborator_context.cpp deleted file mode 100644 index a50122362d..0000000000 --- a/src/frontends/lean/elaborator_context.cpp +++ /dev/null @@ -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; -} -} diff --git a/src/frontends/lean/elaborator_context.h b/src/frontends/lean/elaborator_context.h deleted file mode 100644 index 59dfd667db..0000000000 --- a/src/frontends/lean/elaborator_context.h +++ /dev/null @@ -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(); -} diff --git a/src/frontends/lean/init_module.cpp b/src/frontends/lean/init_module.cpp index 80af2fbc42..112add627f 100644 --- a/src/frontends/lean/init_module.cpp +++ b/src/frontends/lean/init_module.cpp @@ -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(); diff --git a/src/frontends/lean/old_elaborator.cpp b/src/frontends/lean/old_elaborator.cpp deleted file mode 100644 index 380668b5e5..0000000000 --- a/src/frontends/lean/old_elaborator.cpp +++ /dev/null @@ -1,1827 +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 -#include -#include -#include -#include -#include "util/flet.h" -#include "util/list_fn.h" -#include "util/lazy_list_fn.h" -#include "util/sstream.h" -#include "util/name_map.h" -#include "kernel/abstract.h" -#include "kernel/instantiate.h" -#include "kernel/for_each_fn.h" -#include "kernel/find_fn.h" -#include "kernel/replace_fn.h" -#include "kernel/kernel_exception.h" -#include "kernel/error_msgs.h" -#include "kernel/free_vars.h" -#include "kernel/inductive/inductive.h" -#include "library/placeholder.h" -#include "library/choice.h" -#include "library/explicit.h" -#include "library/reducible.h" -#include "library/locals.h" -#include "library/sorry.h" -#include "library/flycheck.h" -#include "library/deep_copy.h" -#include "library/typed_expr.h" -#include "library/old_local_context.h" -#include "library/constants.h" -#include "library/util.h" -#include "library/choice_iterator.h" -#include "library/projection.h" -#include "library/trace.h" -#include "library/pp_options.h" -#include "library/class_instance_resolution.h" -#include "library/error_handling.h" -#include "library/scope_pos_info_provider.h" -#include "library/equations_compiler/equations.h" -#include "library/equations_compiler/old_compiler.h" -#include "library/compiler/rec_fn_macro.h" -#include "library/compiler/vm_compiler.h" -#include "library/vm/vm.h" -#include "library/tactic/elaborate.h" -#include "library/tactic/tactic_state.h" -#include "frontends/lean/elaborator.h" -#include "frontends/lean/local_decls.h" -#include "frontends/lean/structure_instance.h" -#include "frontends/lean/info_manager.h" -#include "frontends/lean/info_annotation.h" -#include "frontends/lean/old_elaborator.h" -#include "frontends/lean/match_expr.h" -// #include "frontends/lean/info_tactic.h" -// #include "frontends/lean/begin_end_annotation.h" -#include "frontends/lean/old_elaborator_exception.h" -#include "frontends/lean/nested_declaration.h" -#include "frontends/lean/calc.h" -#include "frontends/lean/decl_cmds.h" -#include "frontends/lean/opt_cmd.h" -#include "frontends/lean/prenum.h" - -/* IMPORTANT: coercion module has been removed. All comments regarding coercions should be ignored. - This file will be eventually deleted */ - -namespace lean { -typedef pair fname_pos_info; - -struct fname_pos_info_hash_fn { - bool operator()(fname_pos_info const & p) const { - return hash(hash_str(p.first.size(), p.first.c_str(), 17u), hash(p.second.first, p.second.second)); - } -}; - -typedef std::unordered_set fname_pos_info_set; - -/** \brief Auxiliary class used to avoid "don't know how to synthesize placeholder" message when - tactic failures have already been reported. We only use this class when flycheck is enabled. - The idea is to minimize the amount of redundant information in the flycheck pannel. */ -class elaborator_reported_errors { - /* This object may be accessed by different threads. Recall that the elaborator may indirectly - create threads when invoking tactics. */ - mutex m_mutex; - fname_pos_info_set m_reported_positions; -public: - /* \brief Return true if this is the first time we store information for the position associated with \c e. - Otherwise, return false. - \remark We also return true if \c pip is nullptr, or if there is no position information associated with \c e. */ - bool save(pos_info_provider const * pip, expr const & e) { - if (!pip) return true; - if (auto p = pip->get_pos_info(e)) { - lock_guard lc(m_mutex); - fname_pos_info entry(pip->get_file_name(), *p); - if (m_reported_positions.find(entry) == m_reported_positions.end()) { - m_reported_positions.insert(entry); - return true; - } else { - return false; // have already been saved - } - } else { - return true; - } - } -}; - -static elaborator_reported_errors * g_elaborator_reported_errors = nullptr; - -static bool save_error(pos_info_provider const * pip, expr const & e) { - return g_elaborator_reported_errors->save(pip, e); -} - -/** \brief 'Choice' expressions (choice e_1 ... e_n) are mapped into a metavariable \c ?m - and a choice constraints (?m in fn) where \c fn is a choice function. - The choice function produces a stream of alternatives. In this case, it produces a stream of - size \c n, one alternative for each \c e_i. - This is a helper class for implementing this choice functions. -*/ -struct old_elaborator::choice_expr_elaborator : public choice_iterator { - old_elaborator & m_elab; - old_local_context m_context; - bool m_in_equation_lhs; - expr m_meta; - expr m_type; - expr m_choice; - unsigned m_idx; - - choice_expr_elaborator(old_elaborator & elab, old_local_context const & ctx, bool in_equation_lhs, - expr const & meta, expr const & type, expr const & c): - m_elab(elab), m_context(ctx), m_in_equation_lhs(in_equation_lhs), m_meta(meta), - m_type(type), m_choice(c), m_idx(get_num_choices(m_choice)) { - } - - virtual optional next() { - while (m_idx > 0) { - --m_idx; - expr const & c = get_choice(m_choice, m_idx); - expr const & f = get_app_fn(c); - m_elab.save_identifier_info(f); - try { - flet set1(m_elab.m_context, m_context); - flet set2(m_elab.m_in_equation_lhs, m_in_equation_lhs); - pair rcs = m_elab.visit(c); - expr r = rcs.first; - constraint_seq cs = rcs.second; - if (!has_expr_metavar_relaxed(m_type)) { - // we only try coercions here if the m_type and r_type do not contain metavariables. - constraint_seq new_cs = cs; - expr r_type = m_elab.infer_type(r, new_cs); - if (!has_expr_metavar_relaxed(r_type)) { - cs = new_cs; - auto new_rcs = m_elab.ensure_has_type(r, r_type, m_type, justification()); - r = new_rcs.first; - cs += new_rcs.second; - } - } - cs = mk_eq_cnstr(m_meta, r, justification()) + cs; - return optional(cs.to_list()); - } catch (exception &) {} - } - return optional(); - } -}; - -old_elaborator::old_elaborator(elaborator_context & ctx, bool nice_mvar_names): - m_ctx(ctx), - m_context(), - m_unifier_config(ctx.m_options, true /* use exceptions */, true /* discard */) { - m_has_sorry = has_sorry(m_ctx.m_env); - m_use_tactic_hints = true; - m_no_info = false; - m_in_equation_lhs = false; - m_tc = mk_type_checker(ctx.m_env); - m_nice_mvar_names = nice_mvar_names; -} - -expr old_elaborator::mk_local(name const & n, expr const & t, binder_info const & bi) { - return ::lean::mk_local(mk_fresh_name(), n, t, bi); -} - -void old_elaborator::register_meta(expr const & meta) { - lean_assert(is_meta(meta)); - name const & n = mlocal_name(get_app_fn(meta)); - m_mvar2meta.insert(n, meta); -} - -/** \brief Convert the metavariable to the metavariable application that captures - the context where it was defined. -*/ -optional old_elaborator::mvar_to_meta(expr const & mvar) { - lean_assert(is_metavar(mvar)); - name const & m = mlocal_name(mvar); - if (auto it = m_mvar2meta.find(m)) - return some_expr(*it); - else - return none_expr(); -} - -static pos_info_provider * pip() { return get_pos_info_provider(); } -static info_manager * infom() { return get_info_manager(); } - -/** \brief Store the pair (pos(e), type(r)) in the info_data if m_info_manager is available. */ -void old_elaborator::save_type_data(expr const & e, expr const & r) { - // std::cout << ">> infom: " << infom() << ", pip: " << pip() << "\n"; - if (!m_no_info && infom() && pip() && - (is_constant(e) || is_local(e) || is_placeholder(e) || is_as_atomic(e) || - is_notation_info(e))) { - if (auto p = pip()->get_pos_info(e)) { - expr t = m_tc->infer(r).first; - m_pre_info_data.add_type_info(p->first, p->second, t); - } - } -} - -/** \brief Store the pair (pos(e), r) in the info_data if m_info_manager is available. */ -void old_elaborator::save_binder_type(expr const & e, expr const & r) { - if (!m_no_info && infom() && pip()) { - if (auto p = pip()->get_pos_info(e)) { - m_pre_info_data.add_type_info(p->first, p->second, r); - } - } -} - -/** \brief Store type information at pos(e) for r if \c e is marked as "extra" in the info_manager */ -void old_elaborator::save_extra_type_data(expr const & e, expr const & r) { - if (!m_no_info && infom() && pip()) { - if (auto p = pip()->get_pos_info(e)) { - expr t = m_tc->infer(r).first; - m_pre_info_data.add_extra_type_info(p->first, p->second, r, t); - } - } -} - -/** \brief Store proof_state information at pos(e) in the info_manager */ -/* -void old_elaborator::save_proof_state_info(proof_state const & ps, expr const & e) { - if (!m_no_info && infom() && pip()) { - if (auto p = pip()->get_pos_info(e)) { - m_pre_info_data.add_proof_state_info(p->first, p->second, ps); - } - } -} -*/ - -/** \brief Auxiliary function for saving information about which overloaded identifier was used by the elaborator. */ -void old_elaborator::save_identifier_info(expr const & f) { - if (!m_no_info && infom() && pip() && is_constant(f)) { - if (auto p = pip()->get_pos_info(f)) - m_pre_info_data.add_identifier_info(p->first, p->second, const_name(f)); - } -} - -/** \brief Store actual term that was synthesized for an explicit placeholders */ -void old_elaborator::save_synth_data(expr const & e, expr const & r) { - if (!m_no_info && infom() && pip() && is_placeholder(e)) { - if (auto p = pip()->get_pos_info(e)) - m_pre_info_data.add_synth_info(p->first, p->second, r); - } -} - -void old_elaborator::save_placeholder_info(expr const & e, expr const & r) { - if (is_explicit_placeholder(e)) { - save_type_data(e, r); - save_synth_data(e, r); - } - unsigned line, col; - if (m_ctx.has_show_hole_at(line, col)) { - if (auto p = pip()->get_pos_info(e)) { - if (p->first == line && p->second == col) { - m_to_show_hole = r; - m_to_show_hole_ref = e; - m_ctx.reset_show_goal_at(); - } - } - } -} - -void old_elaborator::instantiate_info(substitution s) { -/* - if (m_to_show_hole) { - expr meta = s.instantiate(*m_to_show_hole); - expr meta_type = s.instantiate(old_type_checker(env()).infer(meta).first); - goal g(meta, meta_type); - proof_state ps(goals(g), s, constraints()); - auto out = regular(env(), ios(), m_tc->get_type_context()); - print_lean_info_header(out.get_stream()); - out << ps.pp(out.get_formatter()) << endl; - print_lean_info_footer(out.get_stream()); - } -*/ - if (infom()) { - m_pre_info_data.instantiate(s); - bool overwrite = true; - infom()->merge(m_pre_info_data, overwrite); - m_pre_info_data.clear(); - } -} - -optional old_elaborator::mk_mvar_suffix(expr const & b) { - if (!infom() && !m_nice_mvar_names) - return optional(); - else - return optional(binding_name(b)); -} - -/** \brief Create a metavariable, and attach choice constraint for generating - solutions using class-instances and tactic-hints. -*/ -expr old_elaborator::mk_placeholder_meta(optional const & suffix, optional const & type, - tag g, bool is_strict, bool is_inst_implicit, constraint_seq & cs) { - if (is_inst_implicit) { - auto ec = mk_class_instance_elaborator( - env(), get_global_ios(), m_context, suffix, - true, is_strict, type, g); - register_meta(ec.first); - cs += ec.second; - return ec.first; - } else { - expr m = m_context.mk_meta(suffix, type, g); - register_meta(m); - return m; - } -} - -expr old_elaborator::visit_expecting_type(expr const & e, constraint_seq & cs) { - if (is_placeholder(e) && !placeholder_type(e)) { - expr r = m_context.mk_type_meta(e.get_tag()); - save_placeholder_info(e, r); - return r; - } else if (is_no_info(e)) { - flet let(m_no_info, true); - return visit_expecting_type(get_annotation_arg(e), cs); - } else { - return visit(e, cs); - } -} - -expr old_elaborator::visit_by(expr const & e, optional const & t, constraint_seq & cs) { - lean_assert(is_by(e)); - expr tac = visit(get_by_arg(e), cs); - expr m = m_context.mk_meta(t, e.get_tag()); - register_meta(m); - m_local_tactic_hints.insert(mlocal_name(get_app_fn(m)), tac); - return m; -} - -expr old_elaborator::visit_expecting_type_of(expr const & e, expr const & t, constraint_seq & cs) { - if (is_placeholder(e) && !placeholder_type(e)) { - bool inst_imp = true; - expr r = mk_placeholder_meta(some_expr(t), e.get_tag(), is_strict_placeholder(e), inst_imp, cs); - save_placeholder_info(e, r); - return r; - } else if (is_no_info(e)) { - flet let(m_no_info, true); - return visit_expecting_type_of(get_annotation_arg(e), t, cs); - } else if (is_choice(e)) { - return visit_choice(e, some_expr(t), cs); - } else if (is_by(e)) { - return visit_by(e, some_expr(t), cs); - } else if (is_calc_annotation(e)) { - return visit_calc_proof(e, some_expr(t), cs); - } else { - return visit(e, cs); - } -} - -expr old_elaborator::visit_choice(expr const & e, optional const & t, constraint_seq & cs) { - lean_assert(is_choice(e)); - // Possible optimization: try to lookahead and discard some of the alternatives. - expr m = m_context.mk_meta(t, e.get_tag()); - register_meta(m); - old_local_context ctx = m_context; - bool in_equation_lhs = m_in_equation_lhs; - auto fn = [=](expr const & meta, expr const & type, substitution const & /* s */) { - return choose(std::make_shared(*this, ctx, in_equation_lhs, meta, type, e)); - }; - auto pp_fn = [=](formatter const & fmt, pos_info_provider const * pos_prov, substitution const &, bool is_main, bool) { - format r = pp_previous_error_header(fmt, pos_prov, some_expr(e), is_main); - r += format("none of the overloads is applicable:"); - for (unsigned i = 0; i < get_num_choices(e); i++) { - expr const & c = get_choice(e, i); - expr const & f = get_app_fn(c); - optional fn; - if (is_constant(f)) - fn = const_name(f); - else if (is_local(f)) - fn = local_pp_name(f); - r += space(); - if (fn) { - r += format(*fn); - } else { - r += format("[nontrivial]"); - } - } - return r; - }; - justification j = mk_justification(some_expr(e), pp_fn); - cs += mk_choice_cnstr(m, fn, to_delay_factor(cnstr_group::Basic), true, j); - return m; -} - -expr old_elaborator::visit_calc_proof(expr const & e, optional const & t, constraint_seq & cs) { - lean_assert(is_calc_annotation(e)); - if (t) - return visit_expecting_type_of(get_annotation_arg(e), *t, cs); - else - return visit_core(get_annotation_arg(e), cs); -} - -static bool is_implicit_pi(expr const & e) { - if (!is_pi(e)) - return false; - binder_info bi = binding_info(e); - return bi.is_strict_implicit() || bi.is_implicit() || bi.is_inst_implicit(); -} - -/** \brief Auxiliary function for adding implicit arguments to coercions to function-class */ -expr old_elaborator::add_implict_args(expr e, constraint_seq & cs) { - old_type_checker & tc = *m_tc; - constraint_seq new_cs; - expr type = tc.whnf(tc.infer(e, new_cs), new_cs); - if (!is_implicit_pi(type)) - return e; - cs += new_cs; - while (true) { - lean_assert(is_pi(type)); - tag g = e.get_tag(); - bool is_strict = true; - bool inst_imp = binding_info(type).is_inst_implicit(); - expr imp_arg = mk_placeholder_meta(mk_mvar_suffix(type), some_expr(binding_domain(type)), - g, is_strict, inst_imp, cs); - e = mk_app(e, imp_arg, g); - type = instantiate(binding_body(type), imp_arg); - constraint_seq new_cs; - type = tc.whnf(type, new_cs); - if (!is_implicit_pi(type)) - return e; - cs += new_cs; - } -} - -/** \brief Make sure \c f is really a function, if it is not, try to apply coercions. - The result is a pair new_f, f_type, where new_f is the new value for \c f, - and \c f_type is its type (and a Pi-expression) -*/ -pair old_elaborator::ensure_fun(expr f, constraint_seq & cs) { - expr f_type = infer_type(f, cs); - expr saved_f_type = f_type; - constraint_seq saved_cs = cs; - if (!is_pi(f_type)) - f_type = whnf(f_type, cs); - if (is_pi(f_type)) { - // do nothing - } else { - if (m_tc->is_stuck(f_type)) { - f_type = m_tc->ensure_pi(f_type, f, cs); - } else { - cs = saved_cs; - throw_kernel_exception(env(), f, [=](formatter const & fmt) { return pp_function_expected(fmt, f); }); - } - } - lean_assert(is_pi(f_type)); - return mk_pair(f, f_type); -} - -/** \brief Given a term a : a_type, ensure it has type \c expected_type. Apply coercions if needed */ -pair old_elaborator::ensure_has_type_core( - expr const & a, expr const & a_type, expr const & expected_type, bool /* use_expensive_coercions */, justification const & j) { - pair dcs; - try { - dcs = m_tc->is_def_eq(a_type, expected_type, j); - } catch (exception&) { - dcs.first = false; - } - if (dcs.first) { - return to_ecs(a, dcs.second); - } else { - throw unifier_exception(j, substitution()); - } -} - -bool old_elaborator::is_choice_app(expr const & e) { - expr const & f = get_app_fn(e); - return is_choice(f) || (is_annotation(f) && is_choice(get_nested_annotation_arg(f))); -} - -/** \brief Process ((choice f_1 ... f_n) a_1 ... a_k) as - (choice (f_1 a_1 ... a_k) ... (f_n a_1 ... a_k)) -*/ -expr old_elaborator::visit_choice_app(expr const & e, constraint_seq & cs) { - buffer args; - expr r = get_app_rev_args(e, args); - expr f = get_nested_annotation_arg(r); - lean_assert(is_choice(f)); - buffer new_choices; - unsigned num = get_num_choices(f); - for (unsigned i = 0; i < num; i++) { - expr f_i = get_choice(f, i); - f_i = copy_annotations(r, f_i); - new_choices.push_back(mk_rev_app(f_i, args)); - } - return visit_choice(copy_tag(e, mk_choice(new_choices.size(), new_choices.data())), none_expr(), cs); -} - -expr old_elaborator::visit_app(expr const & e, constraint_seq & cs) { - if (is_choice_app(e)) - return visit_choice_app(e, cs); - constraint_seq f_cs; - bool expl = is_nested_explicit(get_app_fn(e)); - bool partial_expl = is_nested_partial_explicit(get_app_fn(e)); - expr f = visit(app_fn(e), f_cs); - auto f_t = ensure_fun(f, f_cs); - f = f_t.first; - expr f_type = f_t.second; - lean_assert(is_pi(f_type)); - if (!expl) { - bool first = true; - while (binding_info(f_type).is_strict_implicit() || - binding_info(f_type).is_implicit() || - binding_info(f_type).is_inst_implicit()) { - expr const & d_type = binding_domain(f_type); - if (partial_expl && is_pi(whnf(d_type).first)) - break; - lean_assert(binding_info(f_type).is_strict_implicit() || !first); - tag g = f.get_tag(); - bool is_strict = true; - bool inst_imp = binding_info(f_type).is_inst_implicit(); - expr imp_arg = mk_placeholder_meta(mk_mvar_suffix(f_type), some_expr(d_type), - g, is_strict, inst_imp, f_cs); - f = mk_app(f, imp_arg, g); - auto f_t = ensure_fun(f, f_cs); - f = f_t.first; - f_type = f_t.second; - first = false; - } - if (!first) { - // we save the info data again for application of functions with strict implicit arguments - save_type_data(get_app_fn(e), f); - } - } - constraint_seq a_cs; - expr d_type = binding_domain(f_type); - if (false) { - /* - d_type == get_tactic_expr_type() || d_type == get_tactic_identifier_type() || - d_type == get_tactic_using_expr_type() || d_type == get_tactic_location_type() || - d_type == get_tactic_with_expr_type()) { - expr const & a = app_arg(e); - expr r; - if (is_local(a) && - (mlocal_type(a) == get_tactic_expr_type() - || mlocal_type(a) == get_tactic_identifier_type() - || m_in_equation_lhs)) { - r = mk_app(f, a, e.get_tag()); - } else { - r = mk_app(f, mk_tactic_expr(a), e.get_tag()); - } - cs += f_cs + a_cs; - return r; - */ - lean_unreachable(); - } else { - expr a = visit_expecting_type_of(app_arg(e), d_type, a_cs); - expr a_type = infer_type(a, a_cs); - expr r = mk_app(f, a, e.get_tag()); - justification j = mk_app_justification(r, f_type, a, a_type); - bool use_expensive_coercions = false; - auto new_a_cs = ensure_has_type_core(a, a_type, d_type, use_expensive_coercions, j); - expr new_a = new_a_cs.first; - cs += f_cs + new_a_cs.second + a_cs; - return update_app(r, app_fn(r), new_a); - } -} - -expr old_elaborator::visit_placeholder(expr const & e, constraint_seq & cs) { - bool inst_implicit = true; - expr r = mk_placeholder_meta(placeholder_type(e), e.get_tag(), is_strict_placeholder(e), inst_implicit, cs); - save_placeholder_info(e, r); - return r; -} - -level old_elaborator::replace_univ_placeholder(level const & l) { - auto fn = [&](level const & l) { - if (is_one_placeholder(l)) - return some_level(mk_level_one()); - else if (is_placeholder(l)) - return some_level(mk_meta_univ(mk_fresh_name())); - else - return none_level(); - }; - return replace(l, fn); -} - -static bool contains_placeholder(level const & l) { - bool contains = false; - auto fn = [&](level const & l) { - if (contains) return false; - if (is_placeholder(l) || is_one_placeholder(l)) - contains = true; - return true; - }; - for_each(l, fn); - return contains; -} - -expr old_elaborator::visit_sort(expr const & e) { - expr r = update_sort(e, replace_univ_placeholder(sort_level(e))); - if (contains_placeholder(sort_level(e))) - m_to_check_sorts.emplace_back(e, r); - return r; -} - -expr old_elaborator::visit_macro(expr const & e, constraint_seq & cs) { - if (is_as_is(e)) { - return get_as_is_arg(e); - } else if (is_rec_fn_macro(e)) { - if (!m_type) - throw_elaborator_exception("unexpected occurrence of recursive call", e); - return mk_rec_fn_macro(get_rec_fn_name(e), *m_type); - } else { - buffer args; - for (unsigned i = 0; i < macro_num_args(e); i++) - args.push_back(visit(macro_arg(e, i), cs)); - return update_macro(e, args.size(), args.data()); - } -} - -expr old_elaborator::visit_constant(expr const & e) { - declaration d = env().get(const_name(e)); - buffer ls; - for (level const & l : const_levels(e)) - ls.push_back(replace_univ_placeholder(l)); - unsigned num_univ_params = d.get_num_univ_params(); - if (num_univ_params < ls.size()) - throw_kernel_exception(env(), sstream() << "incorrect number of universe levels parameters for '" - << const_name(e) << "', #" << num_univ_params - << " expected, #" << ls.size() << " provided"); - // "fill" with meta universe parameters - for (unsigned i = ls.size(); i < num_univ_params; i++) - ls.push_back(mk_meta_univ(mk_fresh_name())); - lean_assert(num_univ_params == ls.size()); - return update_constant(e, to_list(ls.begin(), ls.end())); -} - -/** \brief Make sure \c e is a type. If it is not, then try to apply coercions. */ -expr old_elaborator::ensure_type(expr const & e, constraint_seq & cs) { - expr t = infer_type(e, cs); - if (is_sort(t)) - return e; - expr saved_t = t; - constraint_seq saved_cs = cs; - t = whnf(t, cs); - if (is_sort(t)) - return e; - if (has_metavar(t)) { - t = whnf(t, cs); - if (is_sort(t)) - return e; - if (is_meta(t)) { - // let type checker add constraint - m_tc->ensure_sort(t, e, cs); - return e; - } - } - cs = saved_cs; - throw_kernel_exception(env(), e, [=](formatter const & fmt) { return pp_type_expected(fmt, e); }); -} - -/** \brief Similar to instantiate_rev, but assumes that subst contains only local constants. - When replacing a variable with a local, we copy the local constant and inherit the tag - associated with the variable. This is a trick for getter better error messages */ -expr old_elaborator::instantiate_rev_locals(expr const & a, unsigned n, expr const * subst) { - if (closed(a)) - return a; - auto fn = [=](expr const & m, unsigned offset) -> optional { - if (offset >= get_free_var_range(m)) - return some_expr(m); // expression m does not contain free variables with idx >= offset - if (is_var(m)) { - unsigned vidx = var_idx(m); - if (vidx >= offset) { - unsigned h = offset + n; - if (h < offset /* overflow, h is bigger than any vidx */ || vidx < h) { - expr local = subst[n - (vidx - offset) - 1]; - lean_assert(is_local(local)); - return some_expr(copy_tag(m, copy(local))); - } else { - return some_expr(copy_tag(m, mk_var(vidx - n))); - } - } - } - return none_expr(); - }; - return replace(a, fn); -} - -expr old_elaborator::visit_binding(expr e, expr_kind k, constraint_seq & cs) { - flet save1(m_context, m_context); - buffer ds, ls, es; - while (e.kind() == k) { - es.push_back(e); - expr const & d0 = binding_domain(e); - expr d = d0; - d = instantiate_rev_locals(d, ls.size(), ls.data()); - d = ensure_type(visit_expecting_type(d, cs), cs); - - if (is_placeholder(d0) && !is_explicit_placeholder(d0)) - save_binder_type(d0, d); - - ds.push_back(d); - expr l = mk_local(binding_name(e), d, binding_info(e)); - if (!is_match_binder_name(binding_name(e))) { - m_context.add_local(l); - } - ls.push_back(l); - e = binding_body(e); - } - lean_assert(ls.size() == es.size() && ls.size() == ds.size()); - e = instantiate_rev_locals(e, ls.size(), ls.data()); - e = (k == expr_kind::Pi) ? ensure_type(visit_expecting_type(e, cs), cs) : visit(e, cs); - e = abstract_locals(e, ls.size(), ls.data()); - unsigned i = ls.size(); - while (i > 0) { - --i; - e = update_binding(es[i], abstract_locals(ds[i], i, ls.data()), e); - } - return e; -} -expr old_elaborator::visit_pi(expr const & e, constraint_seq & cs) { - return visit_binding(e, expr_kind::Pi, cs); -} -expr old_elaborator::visit_lambda(expr const & e, constraint_seq & cs) { - return visit_binding(e, expr_kind::Lambda, cs); -} - -expr old_elaborator::visit_typed_expr(expr const & e, constraint_seq & cs) { - constraint_seq t_cs; - expr t = ensure_type(visit_expecting_type(get_typed_expr_type(e), t_cs), t_cs); - constraint_seq v_cs; - expr v = visit_expecting_type_of(get_typed_expr_expr(e), t, v_cs); - expr v_type = infer_type(v, v_cs); - justification j = mk_type_mismatch_jst(v, v_type, t, e); - auto new_vcs = ensure_has_type(v, v_type, t, j); - v = new_vcs.first; - cs += t_cs + new_vcs.second + v_cs; - return v; -} - -bool old_elaborator::is_sorry(expr const & e) const { - return m_has_sorry && ::lean::is_sorry(e); -} - -expr old_elaborator::visit_sorry(expr const & e) { - level u = mk_meta_univ(mk_fresh_name()); - expr t = mk_sort(u); - expr m = m_context.mk_meta(some_expr(t), e.get_tag()); - return mk_app(update_constant(e, to_list(u)), m, e.get_tag()); -} - -expr const & old_elaborator::get_equation_fn(expr const & eq) const { - expr it = eq; - while (is_lambda(it)) - it = binding_body(it); - if (!is_equation(it)) - throw_elaborator_exception("ill-formed equation", eq); - expr const & fn = get_app_fn(equation_lhs(it)); - if (!is_local(fn)) - throw_elaborator_exception("ill-formed equation", eq); - return fn; -} - -/** - \brief Given two binding expressions \c source and \c target - s.t. they have at least \c num binders, replace the first \c num binders of \c target with \c source. - The binder types are wrapped with \c mk_as_is to make sure the elaborator will not process - them again. -*/ -static expr copy_domain(unsigned num, expr const & source, expr const & target) { - if (num == 0) { - return target; - } else { - lean_assert(is_binding(source) && is_binding(target)); - return update_binding(source, mk_as_is(binding_domain(source)), - copy_domain(num-1, binding_body(source), binding_body(target))); - } -} - - -enum lhs_meta_kind { None, Accessible, Inaccessible }; - -/** - \brief Auxiliary function for searching for metavariable (applications) on the left-hand-side (lhs) of equations. - The possible results are: - - None: lhs does not contain meta-variables - - Accessible: lhs contains meta-variable, and it is located in a position considered by the pattern-matcher. - - Inaccessible: lhs contains meta-variable, and it is located in a possible inaccessible/ignored by the pattern-matcher, - or its type also contains meta-variables - - \remark If the lhs contains accessible and inaccessible metavariables, an accessible is returned. -*/ -static pair find_lhs_meta(old_type_checker & tc, expr const & e) { - if (!has_metavar(e)) - return mk_pair(None, expr()); - environment const & env = tc.env(); - optional acc, inacc; - std::function visit = [&](expr const & e, bool accessible) { - if (acc || !has_metavar(e)) { - return; // done - } else if (is_inaccessible(e)) { - visit(get_annotation_arg(e), false); - } else if (is_meta(e)) { - if (accessible && !acc) { - expr type = tc.infer(e).first; - if (!has_expr_metavar_strict(type)) - acc = e; - else if (!inacc) - inacc = e; - } else if (!accessible && !inacc) { - inacc = e; - } - } else if (is_app(e)) { - if (!accessible) { - visit(app_fn(e), false); - visit(app_arg(e), false); - } else { - buffer args; - expr const & fn = get_app_args(e, args); - if (is_constant(fn) && inductive::is_intro_rule(env, const_name(fn))) { - name I = *inductive::is_intro_rule(env, const_name(fn)); - unsigned num_params = *inductive::get_num_params(env, I); - for (unsigned i = 0; i < num_params; i++) - visit(args[i], false); - for (unsigned i = num_params; i < args.size(); i++) - visit(args[i], accessible); - } else { - visit(fn, false); - for (expr const & arg : args) - visit(arg, false); - } - } - } else if (is_macro(e)) { - for (unsigned i = 0; i < macro_num_args(e); i++) - visit(macro_arg(e, i), false); - } else if (is_binding(e)) { - visit(binding_domain(e), false); - visit(binding_body(e), false); - } - }; - buffer args; - get_app_args(e, args); - for (expr const & arg : args) - visit(arg, true); - if (acc) - return mk_pair(Accessible, *acc); - else if (inacc) - return mk_pair(Inaccessible, *inacc); - else - return mk_pair(None, expr()); -} - -/** - \brief The left-hand-side of recursive equations may contain metavariables associated with - implicit parameters. This procedure replaces them with fresh local constants. - - \remark only "accessible" metavariables are replaced - - Example 1) - Suppose we are defining - map : Pi {n}, vec A n -> vec B n -> vec C n, - map nil nil := nil, - map (a :: va) (b :: vb) := f a b :: map va vb - - After elaboration the second equation will be - - @map (succ ?M) (@cons A ?M a va) (@cons A ?M b vb) := @cons A ?M (f ab) (@map ?M va vb) - - This procedure replaces ?M with (x_1 : nat), where x_1 is a new local constant. - The resultant eqns object is: - [equations - (λ (map : Π {n : ℕ}, vector A n → vector B n → vector C n), [equation (map nil nil) nil]) - (λ (map : Π {n : ℕ}, vector A n → vector B n → vector C n) (a : A) (x_1 : ℕ) (va : vector A x_1) (b : B) - (vb : vector B x_1), - [equation (map (a :: va) (b :: vb)) (f a b :: map va vb)])] - - - Example 2) - Suppose we are defining - definition ideq : Π {A : Type} {a b : A}, a = b → a = b, - ideq H := H - - After elaboration the equation is: - @ideq ?M1 ?M2 ?M3 H := H - - This procedure replaces ?M1 ?M2 ?M3 with - (x_1 : Type) (x_2 : x_1) (x_3 : x_1) - The resultant eqns object is - - [equations - (λ (ideq : ∀ {A : Type} {a b : A}, @eq A a b → @eq A a b) (x_1 : Type) (x_2 x_3 : x_1) (H : @eq x_1 x_2 x_3), - [equation (@ideq x_1 x_2 x_3 H) H])] -*/ -static expr assign_equation_lhs_metas(old_type_checker & tc, expr const & eqns) { - lean_assert(is_equations(eqns)); - if (!has_metavar(eqns)) - return eqns; - buffer eqs; - buffer new_eqs; - to_equations(eqns, eqs); - unsigned num_fns = equations_num_fns(eqns); - - auto replace_meta = [](expr const & e, expr const & meta, expr const & local) { - expr mvar = get_app_fn(meta); - return replace(e, [&](expr const & e, unsigned) { - if (is_meta(e) && mlocal_name(get_app_fn(e)) == mlocal_name(mvar)) { - return some_expr(local); - } else if (!has_metavar(e)) { - return some_expr(e); - } else { - return none_expr(); - } - }); - }; - - for (expr eq : eqs) { - if (!has_metavar(eq)) { - new_eqs.push_back(eq); - } else { - buffer locals; - eq = fun_to_telescope(eq, locals, optional()); - if (is_equation(eq)) { - name x("x"); - lean_assert(num_fns <= locals.size()); - lean_assert(is_equation(eq)); - unsigned idx = 1; - while (true) { - expr lhs = equation_lhs(eq); - auto r = find_lhs_meta(tc, lhs); - if (r.first == None) { - break; - } else if (r.first == Accessible) { - expr const & meta = r.second; - expr meta_type = tc.infer(meta).first; - expr new_local = mk_local(mk_fresh_name(), x.append_after(idx), meta_type, binder_info()); - for (expr & local : locals) - local = update_mlocal(local, replace_meta(mlocal_type(local), meta, new_local)); - eq = replace_meta(eq, meta, new_local); - unsigned i = num_fns; - for (; i < locals.size(); i++) { - if (depends_on(mlocal_type(locals[i]), new_local)) - break; - } - locals.insert(i, new_local); - idx++; - } else { - lean_assert(r.first == Inaccessible); - throw_elaborator_exception(eqns, [=](formatter const & fmt) { - options o = fmt.get_options().update_if_undef(get_pp_implicit_name(), true); - o = o.update_if_undef(get_pp_notation_name(), false); - formatter new_fmt = fmt.update_options(o); - expr const & f = get_app_fn(lhs); - format r; - if (is_local(f) && is_match_binder_name(local_pp_name(f))) { - r = format("invalid 'match' expression, left-hand-side contains meta-variable"); - r += pp_indent_expr(new_fmt, app_arg(lhs)); - } else { - r = format("invalid recursive equation, left-hand-side contains meta-variable"); - r += format(" (possible solution: provide implicit parameters occurring in left-hand-side explicitly)"); - r += pp_indent_expr(new_fmt, lhs); - } - return r; - }); - } - } - } else { - lean_assert(is_no_equation(eq)); - } - new_eqs.push_back(Fun(locals, eq)); - } - } - return update_equations(eqns, new_eqs); -} - -// \remark original_eqns is eqns before elaboration -constraint old_elaborator::mk_equations_cnstr(expr const & m, expr const & eqns) { - environment const & _env = env(); - io_state const & _ios = get_global_ios(); - justification j = mk_failed_to_synthesize_jst(_env, m); - auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & s) { - substitution new_s = s; - expr new_eqns = new_s.instantiate_all(eqns); - bool reject_type_is_meta = false; - new_eqns = solve_unassigned_mvars(new_s, new_eqns, reject_type_is_meta); - if (display_unassigned_mvars(new_eqns, new_s)) { - return lazy_list(); - } - old_type_checker_ptr tc = mk_type_checker(_env); - new_eqns = assign_equation_lhs_metas(*tc, new_eqns); - expr val = compile_equations(*tc, _ios, new_eqns, meta, meta_type); - justification j = mk_justification("equation compilation", some_expr(eqns)); - constraint c = mk_eq_cnstr(meta, val, j); - return lazy_list(to_list(c)); - }; - bool owner = true; - return mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::MaxDelayed), owner, j); -} - -expr old_elaborator::visit_equations(expr const & eqns, constraint_seq & cs) { - buffer eqs; - buffer new_eqs; - optional new_R; - optional new_Hwf; - - to_equations(eqns, eqs); - - if (eqs.empty()) - throw_elaborator_exception("invalid empty set of recursive equations", eqns); - - if (is_wf_equations(eqns)) { - new_R = visit(equations_wf_rel(eqns), cs); - new_Hwf = visit(equations_wf_proof(eqns), cs); - expr Hwf_type = infer_type(*new_Hwf, cs); - expr wf = visit(mk_constant(get_well_founded_name()), cs); - wf = ::lean::mk_app(wf, *new_R); - justification j = mk_type_mismatch_jst(*new_Hwf, Hwf_type, wf, equations_wf_proof(eqns)); - auto new_Hwf_cs = ensure_has_type(*new_Hwf, Hwf_type, wf, j); - new_Hwf = new_Hwf_cs.first; - cs += new_Hwf_cs.second; - } - - flet> set1(m_equation_R, new_R); - unsigned num_fns = equations_num_fns(eqns); - - optional first_eq; - for (expr const & eq : eqs) { - expr new_eq; - constraint_seq new_cs; - buffer fns_locals; - fun_to_telescope(eq, fns_locals, optional()); - list locals = to_list(fns_locals.begin() + num_fns, fns_locals.end()); - if (first_eq) { - // Replace first num_fns domains of eq with the ones in first_eq. - // This is a trick/hack to ensure the fns in each equation have - // the same elaborated type. - new_eq = visit(copy_domain(num_fns, *first_eq, eq), new_cs); - } else { - new_eq = visit(eq, new_cs); - first_eq = new_eq; - } - // To produce more helpful error messages, we decorate all - // justifications created when processing eq with the list of local variables declared in the - // left-hand-side of the equation. - buffer tmp_cs; - new_cs.linearize(tmp_cs); - for (constraint const & c : tmp_cs) { - justification j = c.get_justification(); - auto pp_fn = [=](formatter const & fmt, pos_info_provider const * pp, substitution const & s, bool is_main, bool) { - if (!is_main) - return format(); - format r = j.pp(fmt, pp, s); - r += compose(line(), format("The following identifier(s) are introduced as free variables by the " - "left-hand-side of the equation:")); - format aux; - for (expr const & l : locals) - aux += compose(format(local_pp_name(l)), space()); - r += nest(get_pp_indent(fmt.get_options()), compose(line(), aux)); - return r; - }; - justification new_j = mk_wrapper(j, j.get_main_expr(), pp_fn); - cs += update_justification(c, new_j); - } - new_eqs.push_back(new_eq); - } - - expr new_eqns; - if (new_R) { - new_eqns = copy_tag(eqns, mk_equations(num_fns, new_eqs.size(), new_eqs.data(), *new_R, *new_Hwf)); - } else { - new_eqns = copy_tag(eqns, mk_equations(num_fns, new_eqs.size(), new_eqs.data())); - } - - lean_assert(first_eq && is_lambda(*first_eq)); - expr type = binding_domain(*first_eq); - expr m = m_context.mk_meta(some_expr(type), eqns.get_tag()); - register_meta(m); - constraint c = mk_equations_cnstr(m, new_eqns); - /* We use stack policy for processing MaxDelayed constraints */ - cs = c + cs; - return m; -} - -expr old_elaborator::visit_equation(expr const & eq, constraint_seq & cs) { - expr const & lhs = equation_lhs(eq); - expr const & rhs = equation_rhs(eq); - expr lhs_fn = get_app_fn(lhs); - if (is_explicit_or_partial_explicit(lhs_fn)) - lhs_fn = get_explicit_or_partial_explicit_arg(lhs_fn); - if (!is_local(lhs_fn)) - throw exception("ill-formed equation"); - expr new_lhs, new_rhs; - { - flet set(m_in_equation_lhs, true); - new_lhs = visit(lhs, cs); - } - { - optional some_new_lhs(new_lhs); - flet> set1(m_equation_lhs, some_new_lhs); - new_rhs = visit(rhs, cs); - } - - expr lhs_type = infer_type(new_lhs, cs); - expr rhs_type = infer_type(new_rhs, cs); - justification j = mk_justification(eq, [=](formatter const & fmt, substitution const & subst, bool as_error) { - substitution s(subst); - name n = local_pp_name(lhs_fn); - if (is_match_binder_name(n)) - n = "match"; - return pp_def_type_mismatch(fmt, n, s.instantiate(lhs_type), s.instantiate(rhs_type), as_error); - }); - pair new_rhs_cs = ensure_has_type(new_rhs, rhs_type, lhs_type, j); - new_rhs = new_rhs_cs.first; - cs += new_rhs_cs.second; - return copy_tag(eq, mk_equation(new_lhs, new_rhs)); -} - -expr old_elaborator::visit_inaccessible(expr const & e, constraint_seq & cs) { - if (!m_in_equation_lhs) - throw_elaborator_exception("invalid occurrence of 'inaccessible' annotation, it must only occur in the " - "left-hand-side of recursive equations", e); - return mk_inaccessible(visit(get_annotation_arg(e), cs)); -} - -bool old_elaborator::is_structure_like(expr const & S) { - expr const & I = get_app_fn(S); - return is_constant(I) && ::lean::is_structure_like(env(), const_name(I)); -} - -expr old_elaborator::visit_structure_instance(expr const & e, constraint_seq & cs) { - expr S; - buffer field_names; - buffer field_values, using_exprs; - destruct_structure_instance(e, S, field_names, field_values, using_exprs); - lean_assert(field_names.size() == field_values.size()); - expr new_S = visit(S, cs); - if (!is_structure_like(new_S)) - throw_elaborator_exception("invalid structure instance, given type is not a structure", S); - buffer new_S_args; - expr I = get_app_args(new_S, new_S_args); - expr new_S_type = whnf(infer_type(new_S, cs), cs); - tag S_tag = S.get_tag(); - while (is_pi(new_S_type)) { - expr m = m_context.mk_meta(some_expr(binding_domain(new_S_type)), S_tag); - register_meta(m); - new_S_args.push_back(m); - new_S = mk_app(new_S, m, S_tag); - new_S_type = whnf(instantiate(binding_body(new_S_type), m), cs); - } - buffer field_used; - field_used.resize(field_names.size(), false); - buffer new_field_values; - for (expr const & v : field_values) - new_field_values.push_back(visit(v, cs)); - buffer using_exprs_used; - using_exprs_used.resize(using_exprs.size(), false); - buffer new_using_exprs; - buffer new_using_types; - for (expr const & u : using_exprs) { - expr new_u = visit(u, cs); - expr new_u_type = whnf(infer_type(new_u, cs), cs); - if (!is_structure_like(new_u_type)) - throw_elaborator_exception("invalid structure instance, type of 'using' argument is not a structure", u); - new_using_exprs.push_back(new_u); - new_using_types.push_back(new_u_type); - } - buffer intro_names; - get_intro_rule_names(env(), const_name(I), intro_names); - lean_assert(intro_names.size() == 1); - name const & S_mk_name = intro_names[0]; - tag result_tag = e.get_tag(); - expr S_mk = mk_constant(S_mk_name, const_levels(I), result_tag); - for (expr & arg : new_S_args) - S_mk = mk_app(S_mk, arg, result_tag); - expr S_mk_type = whnf(infer_type(S_mk, cs), cs); - while (is_pi(S_mk_type)) { - name n = binding_name(S_mk_type); - expr d_type = binding_domain(S_mk_type); - expr v; - unsigned i = 0; - for (; i < field_names.size(); i++) { - if (!field_used[i] && field_names[i] == n) { - field_used[i] = true; - v = new_field_values[i]; - break; - } - } - if (i == new_field_values.size()) { - // did not find explicit field - unsigned i = 0; - for (; i < new_using_exprs.size(); i++) { - // check if u_type structure has the given field. - expr const & u_type = new_using_types[i]; - buffer u_type_args; - expr const & J = get_app_args(u_type, u_type_args); - lean_assert(is_constant(J)); - name J_field_name = const_name(J) + n; - if (env().find(J_field_name)) { - tag u_tag = using_exprs[i].get_tag(); - v = mk_constant(J_field_name, const_levels(J), u_tag); - for (expr const & arg : u_type_args) - v = mk_app(v, arg, u_tag); - v = mk_app(v, new_using_exprs[i], u_tag); - using_exprs_used[i] = true; - break; - } - } - if (i == using_exprs.size()) { - // did not find field in using structure - v = m_context.mk_meta(some_expr(d_type), result_tag); - register_meta(v); - } - } - S_mk = mk_app(S_mk, v, result_tag); - expr v_type = infer_type(v, cs); - justification j = mk_app_justification(S_mk, S_mk_type, v, v_type); - auto new_v_cs = ensure_has_type(v, v_type, d_type, j); - expr new_v = new_v_cs.first; - cs += new_v_cs.second; - S_mk = update_app(S_mk, app_fn(S_mk), new_v); - S_mk_type = whnf(instantiate(binding_body(S_mk_type), new_v), cs); - } - for (unsigned i = 0; i < field_used.size(); i++) { - if (!field_used[i]) - throw_elaborator_exception(sstream() << "invalid structure instance, invalid field name '" - << field_names[i] << "'", field_values[i]); - } - for (unsigned i = 0; i < using_exprs_used.size(); i++) { - if (!using_exprs_used[i]) - throw_elaborator_exception(sstream() << "invalid structure instance, 'using' clause #" - << i + 1 << " is unnecessary", using_exprs[i]); - } - return S_mk; -} - -expr old_elaborator::visit_prenum(expr const & e, constraint_seq & cs) { - lean_assert(is_prenum(e)); - mpz const & v = prenum_value(e); - tag e_tag = e.get_tag(); - expr A = m_context.mk_meta(none_expr(), e_tag); - level A_lvl = sort_level(m_tc->ensure_type(A, cs)); - levels ls(A_lvl); - bool is_strict = true; - bool inst_imp = true; - if (v.is_neg()) - throw_elaborator_exception("invalid pre-numeral, it must be a non-negative value", e); - if (v.is_zero()) { - expr has_zero_A = mk_app(mk_constant(get_has_zero_name(), ls), A, e_tag); - expr S = mk_placeholder_meta(optional(), some_expr(has_zero_A), - e_tag, is_strict, inst_imp, cs); - return mk_app(mk_app(mk_constant(get_zero_name(), ls), A, e_tag), S, e_tag); - } else { - expr has_one_A = mk_app(mk_constant(get_has_one_name(), ls), A, e_tag); - expr S_one = mk_placeholder_meta(optional(), some_expr(has_one_A), - e_tag, is_strict, inst_imp, cs); - expr one = mk_app(mk_app(mk_constant(get_one_name(), ls), A, e_tag), S_one, e_tag); - if (v == 1) { - return one; - } else { - expr has_add_A = mk_app(mk_constant(get_has_add_name(), ls), A, e_tag); - expr S_add = mk_placeholder_meta(optional(), some_expr(has_add_A), - e_tag, is_strict, inst_imp, cs); - std::function convert = [&](mpz const & v) { - lean_assert(v > 0); - if (v == 1) - return one; - else if (v % mpz(2) == 0) { - expr r = convert(v / 2); - return mk_app(mk_app(mk_app(mk_constant(get_bit0_name(), ls), A, e_tag), S_add, e_tag), r, e_tag); - } else { - expr r = convert(v / 2); - return mk_app(mk_app(mk_app(mk_app(mk_constant(get_bit1_name(), ls), A, e_tag), S_one, e_tag), S_add, e_tag), r, e_tag); - } - }; - return convert(v); - } - } -} - -expr old_elaborator::visit_checkpoint_expr(expr const & e, constraint_seq & cs) { - expr arg = get_annotation_arg(e); - expr m; - m = m_context.mk_meta(none_expr(), e.get_tag()); - register_meta(m); - old_local_context ctx = m_context; - bool in_equation_lhs = m_in_equation_lhs; - auto fn = [=](expr const & meta, expr const & /* type */, substitution const & /* s */) { - flet set1(m_context, ctx); - flet set2(m_in_equation_lhs, in_equation_lhs); - pair rcs = visit(arg); - expr r = rcs.first; - constraint_seq cs = rcs.second; - cs = mk_eq_cnstr(meta, r, justification()) + cs; - return lazy_list(cs.to_list()); - }; - justification j; - cs += mk_choice_cnstr(m, fn, to_delay_factor(cnstr_group::Checkpoint), true, j); - return m; -} - -expr old_elaborator::visit_core(expr const & e, constraint_seq & cs) { - if (is_prenum(e)) { - return visit_prenum(e, cs); - } else if (is_placeholder(e)) { - return visit_placeholder(e, cs); - } else if (is_choice(e)) { - return visit_choice(e, none_expr(), cs); - } else if (is_by(e)) { - return visit_by(e, none_expr(), cs); - } else if (is_calc_annotation(e)) { - return visit_calc_proof(e, none_expr(), cs); - } else if (is_no_info(e)) { - flet let(m_no_info, true); - return visit(get_annotation_arg(e), cs); - } else if (is_typed_expr(e)) { - return visit_typed_expr(e, cs); - } else if (is_as_atomic(e)) { - // ignore annotation - return visit_core(get_as_atomic_arg(e), cs); - } else if (is_explicit_or_partial_explicit(e)) { - // ignore annotation - return visit_core(get_explicit_or_partial_explicit_arg(e), cs); - } else if (is_sorry(e)) { - return visit_sorry(e); - } else if (is_equations(e)) { - lean_unreachable(); - } else if (is_equation(e)) { - return visit_equation(e, cs); - } else if (is_inaccessible(e)) { - return visit_inaccessible(e, cs); - } else if (is_structure_instance(e)) { - return visit_structure_instance(e, cs); - } else if (is_checkpoint_annotation(e)) { - return visit_checkpoint_expr(e, cs); - } else { - switch (e.kind()) { - case expr_kind::Local: return e; - case expr_kind::Meta: return e; - case expr_kind::Sort: return visit_sort(e); - case expr_kind::Var: lean_unreachable(); // LCOV_EXCL_LINE - case expr_kind::Constant: return visit_constant(e); - case expr_kind::Macro: return visit_macro(e, cs); - case expr_kind::Lambda: return visit_lambda(e, cs); - case expr_kind::Pi: return visit_pi(e, cs); - case expr_kind::App: return visit_app(e, cs); - case expr_kind::Let: - // NOT IMPLEMENTED YET - lean_unreachable(); - } - lean_unreachable(); // LCOV_EXCL_LINE - } -} - -pair old_elaborator::visit(expr const & e) { - if (is_extra_info(e)) { - auto ecs = visit(get_annotation_arg(e)); - save_extra_type_data(e, ecs.first); - return ecs; - } - if (is_notation_info(e)) { - pair ecs; - { - flet let(m_no_info, true); - ecs = visit(get_annotation_arg(e)); - } - save_type_data(e, ecs.first); - return ecs; - } - expr r; - expr b = e; - constraint_seq cs; - if (is_explicit(e)) { - b = get_explicit_arg(e); - if (is_sorry(b)) { - r = visit_constant(b); - } else { - r = visit_core(b, cs); - } - } else if (is_equations(e)) { - r = visit_equations(e, cs); - } else if (is_explicit(get_app_fn(e))) { - r = visit_core(e, cs); - } else if (is_partial_explicit(get_app_fn(e))) { - r = visit_core(e, cs); - tag g = e.get_tag(); - expr r_type = whnf(infer_type(r, cs), cs); - expr imp_arg; - bool is_strict = true; - while (is_pi(r_type)) { - binder_info bi = binding_info(r_type); - if (!bi.is_implicit() && !bi.is_inst_implicit()) { - break; - } - expr const & d_type = binding_domain(r_type); - if (is_pi(whnf(d_type).first)) { - break; - } - bool inst_imp = bi.is_inst_implicit(); - imp_arg = mk_placeholder_meta(mk_mvar_suffix(r_type), some_expr(d_type), - g, is_strict, inst_imp, cs); - r = mk_app(r, imp_arg, g); - r_type = whnf(instantiate(binding_body(r_type), imp_arg), cs); - } - } else { - bool consume_args = false; - if (is_as_atomic(e)) { - flet let(m_no_info, true); - r = get_as_atomic_arg(e); - if (is_explicit_or_partial_explicit(r)) r = get_explicit_or_partial_explicit_arg(r); - r = visit_core(r, cs); - } else { - r = visit_core(e, cs); - } - tag g = e.get_tag(); - expr r_type = whnf(infer_type(r, cs), cs); - expr imp_arg; - bool is_strict = true; - while (is_pi(r_type)) { - binder_info bi = binding_info(r_type); - if (!bi.is_implicit() && !bi.is_inst_implicit()) { - if (!consume_args) - break; - if (!has_free_var(binding_body(r_type), 0)) { - // if the rest of the type does not reference argument, - // then we also stop consuming arguments - break; - } - } - bool inst_imp = bi.is_inst_implicit(); - imp_arg = mk_placeholder_meta(mk_mvar_suffix(r_type), some_expr(binding_domain(r_type)), - g, is_strict, inst_imp, cs); - r = mk_app(r, imp_arg, g); - r_type = whnf(instantiate(binding_body(r_type), imp_arg), cs); - } - } - save_type_data(b, r); - return mk_pair(r, cs); -} - -expr old_elaborator::visit(expr const & e, constraint_seq & cs) { - auto r = visit(e); - cs += r.second; - return r.first; -} - -unify_result_seq old_elaborator::solve(constraint_seq const & cs) { - buffer tmp; - cs.linearize(tmp); - return unify(env(), tmp.size(), tmp.data(), substitution(), m_unifier_config); -} - -optional old_elaborator::get_tactic_for(expr const & mvar) { - if (auto it = m_local_tactic_hints.find(mlocal_name(mvar))) { - m_used_local_tactic_hints.insert(mlocal_name(mvar)); - return some_expr(*it); - } else { - return none_expr(); - } -} - -void old_elaborator::display_unsolved_tactic_state(expr const & mvar, tactic_state const & ts, format const & fmt, - expr const & pos) { - lean_assert(is_metavar(mvar)); - if (!m_displayed_errors.contains(mlocal_name(mvar))) { - m_displayed_errors.insert(mlocal_name(mvar)); - type_context ctx = mk_type_context_for(ts); - auto out = regular(env(), get_global_ios(), ctx); - flycheck_error err(get_global_ios()); - if (!err.enabled() || save_error(pip(), pos)) { - display_error_pos(out.get_stream(), out.get_options(), pip(), pos); - out << " " << fmt << "\nstate:\n" << ts.pp(get_global_ios().get_formatter_factory()) << endl; - } - } -} - -void old_elaborator::display_unsolved_tactic_state(expr const & mvar, tactic_state const & ts, char const * msg, - expr const & pos) { - return display_unsolved_tactic_state(mvar, ts, format(msg), pos); -} - -void old_elaborator::display_unsolved_tactic_state(expr const & mvar, tactic_state const & ps, char const * msg) { - display_unsolved_tactic_state(mvar, ps, msg, mvar); -} - -static tactic_state to_tactic_state(environment const & env, options const & opts, expr const & meta, expr const & type, buffer & new_ctx) { - buffer old_ctx; - get_app_args(meta, old_ctx); - local_context lctx; - for (unsigned i = 0; i < old_ctx.size(); i++) { - expr old_local_type = mlocal_type(old_ctx[i]); - if (i > 0) - old_local_type = instantiate_rev(abstract_locals(old_local_type, i, old_ctx.data()), i, new_ctx.data()); - expr new_local = lctx.mk_local_decl(local_pp_name(old_ctx[i]), old_local_type, local_info(old_ctx[i])); - new_ctx.push_back(new_local); - } - lean_assert(old_ctx.size() == new_ctx.size()); - expr new_type = instantiate_rev(abstract_locals(type, old_ctx.size(), old_ctx.data()), new_ctx.size(), new_ctx.data()); - return mk_tactic_state_for(env, opts, lctx, new_type); -} - -optional old_elaborator::execute_tactic(expr const & tactic, tactic_state const & s, expr const & mvar) { - elaborate_fn fn(nested_elaborate); - scope_elaborate_fn scope(fn); - - name tactic_name("_tactic"); - expr tactic_type = ::lean::mk_app(mk_constant("tactic"), mk_constant("unit")); - /* compile tactic */ - environment new_env = env(); - options const & opts = m_ctx.m_options; - bool use_conv_opt = true; - bool is_trusted = false; - auto cd = check(new_env, mk_definition(new_env, tactic_name, {}, tactic_type, tactic, use_conv_opt, is_trusted)); - new_env = new_env.add(cd); - new_env = vm_compile(new_env, new_env.get(tactic_name)); - vm_state S(new_env); - vm_obj r = S.invoke(tactic_name, to_obj(s)); - if (optional new_s = is_tactic_success(r)) { - return some_tactic_state(*new_s); - } else if (optional> ex = is_tactic_exception(S, opts, r)) { - display_unsolved_tactic_state(mvar, ex->second, ex->first, mvar); - return none_tactic_state(); - } else { - return none_tactic_state(); - } -} - -// The parameters univs_fixed is true if the elaborator has instantiated the universe metavariables with universe parameters. -// See issue #771 -void old_elaborator::solve_unassigned_mvar(substitution & subst, expr mvar, name_set & visited, bool reject_type_is_meta) { - if (visited.contains(mlocal_name(mvar))) - return; - visited.insert(mlocal_name(mvar)); - auto meta = mvar_to_meta(mvar); - if (!meta) - return; - meta = instantiate_meta(*meta, subst); - // TODO(Leo): we are discarding constraints here - expr type = m_tc->infer(*meta).first; - // first solve unassigned metavariables in type - type = solve_unassigned_mvars(subst, type, visited, reject_type_is_meta); - if (reject_type_is_meta && is_meta(type)) { - throw_elaborator_exception("failed to synthesize placeholder, type is a unknown (i.e., it is a metavariable) " - "(solution: provide type explicitly)", mvar); - } - options const & opts = m_ctx.m_options; - buffer new_locals; - tactic_state ts = to_tactic_state(env(), opts, *meta, type, new_locals); - if (optional tac = get_tactic_for(mvar)) { - expr tactic = subst.instantiate(*tac); - if (optional new_ts = execute_tactic(tactic, ts, mvar)) { - metavar_context mctx = new_ts->mctx(); - expr r = mctx.instantiate_mvars(new_ts->main()); - if (has_expr_metavar(r)) { - display_unsolved_tactic_state(mvar, *new_ts, "tactic failed, result contains meta-variables"); - throw_elaborator_exception("tactic failed, result contains meta-variables", r); - } - metavar_decl main_decl = *mctx.get_metavar_decl(new_ts->main()); - type_context aux_ctx(env(), opts, mctx, main_decl.get_context()); - r = aux_ctx.mk_lambda(new_locals, r); - subst.assign(mvar, r); - } - } - return; -} - -/** \brief Execute \c fn on every metavariable occurring in \c e. - \remark The left-hand-side of equations is ignored. -*/ -static void visit_unassigned_mvars(expr const & e, std::function const & fn) { - if (!has_metavar(e)) - return; - - expr_set visited; - - auto should_visit = [&](expr const & e) { - if (!is_shared(e)) - return true; - if (visited.find(e) != visited.end()) - return false; - visited.insert(e); - return true; - }; - - std::function visit = [&](expr const & e) { - check_interrupted(); - if (!has_metavar(e)) - return; - switch (e.kind()) { - case expr_kind::Var: case expr_kind::Local: - case expr_kind::Constant: case expr_kind::Sort: - break; // do nothing - case expr_kind::Meta: - if (should_visit(e)) - fn(e); - break; - case expr_kind::Macro: - if (should_visit(e)) { - if (is_equation(e)) { - visit(equation_rhs(e)); - } else { - for (unsigned i = 0; i < macro_num_args(e); i++) - visit(macro_arg(e, i)); - } - } - break; - case expr_kind::App: - if (should_visit(e)) { - visit(app_fn(e)); - visit(app_arg(e)); - } - break; - case expr_kind::Lambda: - case expr_kind::Pi: - if (should_visit(e)) { - visit(binding_domain(e)); - visit(binding_body(e)); - } - break; - case expr_kind::Let: - if (should_visit(e)) { - visit(let_type(e)); - visit(let_value(e)); - visit(let_body(e)); - } - break; - } - }; - - visit(e); -} - -expr old_elaborator::solve_unassigned_mvars(substitution & subst, expr e, name_set & visited, bool reject_type_is_meta) { - e = subst.instantiate(e); - visit_unassigned_mvars(e, [&](expr const & mvar) { - solve_unassigned_mvar(subst, mvar, visited, reject_type_is_meta); - }); - return subst.instantiate(e); -} - -expr old_elaborator::solve_unassigned_mvars(substitution & subst, expr const & e, bool reject_type_is_meta) { - name_set visited; - return solve_unassigned_mvars(subst, e, visited, reject_type_is_meta); -} - -bool old_elaborator::display_unassigned_mvars(expr const & e, substitution const & s) { - bool r = false; - if (check_unassigned() && has_metavar(e)) { - substitution tmp_s(s); - visit_unassigned_mvars(e, [&](expr const & mvar) { - if (auto it = mvar_to_meta(mvar)) { - expr meta = tmp_s.instantiate(*it); - expr meta_type = tmp_s.instantiate(type_checker(env()).infer(meta)); - buffer new_ctx; - tactic_state ts = to_tactic_state(env(), m_ctx.m_options, meta, meta_type, new_ctx); - display_unsolved_tactic_state(mvar, ts, "don't know how to synthesize placeholder"); - r = true; - } - }); - } - return r; -} - -/** \brief Check whether the solution found by the elaborator is producing too specific - universes. - - \remark For now, we only check if a term Type.{?u} was solved by assigning ?u to 0. - In this case, the user should write Prop instead of Type. -*/ -void old_elaborator::check_sort_assignments(substitution const & s) { - for (auto const & p : m_to_check_sorts) { - expr pre = p.first; - expr post = p.second; - lean_assert(is_sort(post)); - for_each(sort_level(post), [&](level const & u) { - if (is_meta(u) && s.is_assigned(u)) { - level r = *s.get_level(u); - if (is_explicit(r)) { - substitution saved_s(s); - throw_kernel_exception(env(), pre, [=](formatter const & fmt) { - options o = fmt.get_options(); - o = o.update(get_pp_universes_name(), true); - format r("solution computed by the elaborator forces a universe placeholder" - " to be a fixed value, computed sort is"); - r += pp_indent_expr(fmt.update_options(o), substitution(saved_s).instantiate(post)); - return r; - }); - } - } - return true; - }); - } -} - -/** \brief Apply substitution and solve remaining metavariables using tactics. */ -expr old_elaborator::apply(substitution & s, expr const & e, name_set & univ_params, buffer & new_params, bool is_def_value) { - expr r = s.instantiate(e); - if (has_univ_metavar(r)) - r = univ_metavars_to_params(env(), lls(), s, univ_params, new_params, r); - bool reject_type_is_meta = is_def_value; - r = solve_unassigned_mvars(s, r, reject_type_is_meta); - display_unassigned_mvars(r, s); - return r; -} - -std::tuple old_elaborator::apply(substitution & s, expr const & e, bool is_def_value) { - auto ps = collect_univ_params(e); - buffer new_ps; - expr r = apply(s, e, ps, new_ps, is_def_value); - return std::make_tuple(r, to_list(new_ps.begin(), new_ps.end())); -} - -struct pos_info_hash { - unsigned operator()(pos_info const & p) const { return hash(p.first, p.second); } -}; - -void old_elaborator::check_used_local_tactic_hints() { - std::unordered_set> pos_set; - // The same pretac may be processed several times because of choice-exprs. - // The pretactics may be structurally different in each branch (because of unique local constant names). - // So, we use their positions to identify which tactic hints were used - if (!pip()) - return; // position information is not available - m_local_tactic_hints.for_each([&](name const & n, expr const & e) { - if (m_used_local_tactic_hints.contains(n)) { - if (auto p = pip()->get_pos_info(e)) { - pos_set.insert(*p); - } - } - }); - m_local_tactic_hints.for_each([&](name const & n, expr const & e) { - if (m_used_local_tactic_hints.contains(n)) - return; // local hint was used - if (auto p = pip()->get_pos_info(e)) { - if (pos_set.find(*p) == pos_set.end()) { - char const * msg = "unnecessary tactic was provided, placeholder was automatically " - "synthesized by the elaborator"; - if (auto it = m_mvar2meta.find(n)) - throw_elaborator_exception(msg, *it); - else - throw exception(msg); - } - } - // Remark: we are ignoring expressions that do not have location information. - // This is a little bit hackish - }); -} - -auto old_elaborator::operator()(list const & ctx, expr const & e, bool _ensure_type) --> std::tuple { - m_context.set_ctx(ctx); - constraint_seq cs; - expr r = visit(e, cs); - if (_ensure_type) - r = ensure_type(r, cs); - auto p = solve(cs).pull(); - lean_assert(p); - substitution s = p->first.first; - bool is_value = false; - auto result = apply(s, r, is_value); - check_sort_assignments(s); - instantiate_info(s); - check_used_local_tactic_hints(); - return result; -} - -std::tuple old_elaborator::operator()(expr const & t, expr const & v, name const & n) { - constraint_seq t_cs; - expr r_t = ensure_type(visit(t, t_cs), t_cs); - // Opaque definitions in the main module may treat other opaque definitions (in the main module) as transparent. - m_type = r_t; - constraint_seq v_cs; - expr r_v = visit(v, v_cs); - expr r_v_type = infer_type(r_v, v_cs); - justification j = mk_justification(r_v, [=](formatter const & fmt, substitution const & subst, bool as_error) { - substitution s(subst); - return pp_def_type_mismatch(fmt, n, s.instantiate(r_t), s.instantiate(r_v_type), as_error); - }); - pair r_v_cs = ensure_has_type(r_v, r_v_type, r_t, j); - r_v = r_v_cs.first; - constraint_seq cs = t_cs + r_v_cs.second + v_cs; - auto p = solve(cs).pull(); - lean_assert(p); - substitution s = p->first.first; - name_set univ_params = collect_univ_params(r_v, collect_univ_params(r_t)); - buffer new_params; - bool is_value = false; - expr new_r_t = apply(s, r_t, univ_params, new_params, is_value); - is_value = true; - expr new_r_v = apply(s, r_v, univ_params, new_params, is_value); - check_sort_assignments(s); - instantiate_info(s); - check_used_local_tactic_hints(); - return std::make_tuple(new_r_t, new_r_v, to_list(new_params.begin(), new_params.end())); -} - -static name * g_tmp_prefix = nullptr; - -std::tuple elaborate(elaborator_context & env, list 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 elaborate(elaborator_context & env, name const & n, expr const & t, - expr const & v) { - return old_elaborator(env)(t, v, n); -} - -void initialize_old_elaborator() { - g_tmp_prefix = new name(name::mk_internal_unique_name()); - g_elaborator_reported_errors = new elaborator_reported_errors(); -} - -void finalize_old_elaborator() { - delete g_tmp_prefix; - delete g_elaborator_reported_errors; -} -} diff --git a/src/frontends/lean/old_elaborator.h b/src/frontends/lean/old_elaborator.h deleted file mode 100644 index d769561b42..0000000000 --- a/src/frontends/lean/old_elaborator.h +++ /dev/null @@ -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 -#include -#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 mvar2meta; -/** \brief Helper class for implementing the \c elaborate functions. */ -class old_elaborator { - typedef name_map local_tactic_hints; - typedef rb_map, expr_quick_cmp> cache; - typedef std::vector> 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 m_equation_lhs; - // if m_equation_R is not none when elaborator is processing recursive equation using the well-founded relation R. - optional 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 m_type; - - optional 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 infer_type(expr const & e) { return m_tc->infer(e); } - pair 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 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 mk_mvar_suffix(expr const & b); - expr mk_placeholder_meta(optional const & suffix, optional const & type, - tag g, bool is_strict, bool inst_implicit, constraint_seq & cs); - expr mk_placeholder_meta(optional const & type, tag g, bool is_strict, bool inst_implicit, constraint_seq & cs) { - return mk_placeholder_meta(optional(), 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 const & t, constraint_seq & cs); - expr visit_by(expr const & e, optional const & t, constraint_seq & cs); - expr visit_calc_proof(expr const & e, optional const & t, constraint_seq & cs); - expr add_implict_args(expr e, constraint_seq & cs); - pair ensure_fun(expr f, constraint_seq & cs); - pair ensure_has_type_core(expr const & a, expr const & a_type, expr const & expected_type, - bool use_expensive_coercions, justification const & j); - pair 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 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 get_tactic_for(expr const & mvar); - optional execute_tactic(expr const & tactic, tactic_state const & s, expr const & mvar); - // optional 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 & new_params, bool is_def_value); - std::tuple apply(substitution & s, expr const & e, bool is_def_value); - // elaborate_result elaborate_nested(list const & ctx, optional 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 operator()(list const & ctx, expr const & e, bool _ensure_type); - std::tuple operator()(expr const & t, expr const & v, name const & n); -}; - -std::tuple elaborate(elaborator_context & env, list const & ctx, expr const & e, - bool ensure_type = false, bool nice_mvar_names = false); - -std::tuple elaborate(elaborator_context & env, name const & n, expr const & t, expr const & v); -void initialize_old_elaborator(); -void finalize_old_elaborator(); -} diff --git a/src/frontends/lean/old_elaborator_exception.cpp b/src/frontends/lean/old_elaborator_exception.cpp deleted file mode 100644 index d76feaf501..0000000000 --- a/src/frontends/lean/old_elaborator_exception.cpp +++ /dev/null @@ -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; }); -} -} diff --git a/src/frontends/lean/old_elaborator_exception.h b/src/frontends/lean/old_elaborator_exception.h deleted file mode 100644 index 8feb37016c..0000000000 --- a/src/frontends/lean/old_elaborator_exception.h +++ /dev/null @@ -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); -} diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 36b39739d9..ac1d63c452 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -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);