From eee74ef1b4263a06ccfec39dad7cb6d05f2b1bd1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 26 Feb 2016 15:35:29 -0800 Subject: [PATCH] refactor(frontends/lean/pp): use abstract_type_context instead of type_checker --- src/frontends/lean/builtin_cmds.cpp | 63 -------------------- src/frontends/lean/pp.cpp | 40 ++++++++----- src/frontends/lean/pp.h | 66 ++++++++++----------- src/frontends/lean/token_table.cpp | 3 +- src/kernel/abstract_type_context.h | 7 +++ src/library/blast/blast.cpp | 13 ++-- src/library/tactic/contradiction_tactic.cpp | 2 +- src/library/type_context.h | 10 ++-- 8 files changed, 80 insertions(+), 124 deletions(-) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 72f0eb853..42ab8fe96 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -487,69 +487,6 @@ static environment init_hits_cmd(parser & p) { return module::declare_hits(p.env()); } -static environment compile_cmd(parser & p) { - name n = p.check_constant_next("invalid #compile command, constant expected"); - declaration d = p.env().get(n); - buffer aux_decls; - preprocess_rec(p.env(), d, aux_decls); - return p.env(); -} - -static void check_expr_and_print(parser & p, expr const & e) { - environment const & env = p.env(); - type_checker tc(env); - expr t = tc.check_ignore_undefined_universes(e).first; - regular(env, p.ios(), tc.get_type_context()) << e << " : " << t << "\n"; -} - -static environment app_builder_cmd(parser & p) { - environment const & env = p.env(); - auto pos = p.pos(); - app_builder b(env); - name c = p.check_constant_next("invalid #app_builder command, constant expected"); - bool has_mask = false; - buffer mask; - if (p.curr_is_token(get_lbracket_tk())) { - p.next(); - has_mask = true; - while (true) { - name flag = p.check_constant_next("invalid #app_builder command, constant (true, false) expected"); - mask.push_back(flag == get_true_name()); - if (!p.curr_is_token(get_comma_tk())) - break; - p.next(); - } - p.check_token_next(get_rbracket_tk(), "invalid #app_builder command, ']' expected"); - } - - buffer args; - while (true) { - expr e; level_param_names ls; - std::tie(e, ls) = parse_local_expr(p); - args.push_back(e); - if (!p.curr_is_token(get_comma_tk())) - break; - p.next(); - } - - if (has_mask && args.size() > mask.size()) - throw parser_error(sstream() << "invalid #app_builder command, too many arguments", pos); - - optional r; - if (has_mask) - r = b.mk_app(c, mask.size(), mask.data(), args.data()); - else - r = b.mk_app(c, args.size(), args.data()); - - if (r) { - check_expr_and_print(p, *r); - } else { - throw parser_error(sstream() << "failed to build application for '" << c << "'", pos); - } - - return env; -} - static environment simplify_cmd(parser & p) { name rel = p.check_constant_next("invalid #simplify command, constant expected"); name ns = p.check_id_next("invalid #simplify command, id expected"); diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 48fec4e21..525e5f958 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -252,9 +252,9 @@ expr pretty_fn::purify(expr const & e) { if (!has_expr_metavar(e) && !has_local(e) && (!m_universes || !has_univ_metavar(e))) return some_expr(e); else if (is_metavar(e) && m_purify_metavars) - return some_expr(mk_metavar(mk_metavar_name(mlocal_name(e)), mlocal_type(e))); + return some_expr(mk_metavar(mk_metavar_name(mlocal_name(e)), m_ctx.infer(e))); else if (is_local(e)) - return some_expr(mk_local(mlocal_name(e), mk_local_name(mlocal_name(e), local_pp_name(e)), mlocal_type(e), local_info(e))); + return some_expr(mk_local(mlocal_name(e), mk_local_name(mlocal_name(e), m_ctx.get_local_pp_name(e)), m_ctx.infer(e), local_info(e))); else if (is_constant(e)) return some_expr(update_constant(e, map(const_levels(e), [&](level const & l) { return purify(l); }))); else if (is_sort(e)) @@ -321,8 +321,13 @@ bool pretty_fn::is_implicit(expr const & f) { return false; } try { - binder_info bi = binding_info(m_tc.ensure_pi(m_tc.infer(f).first).first); - return bi.is_implicit() || bi.is_strict_implicit() || bi.is_inst_implicit(); + expr t = m_ctx.relaxed_whnf(m_ctx.infer(f)); + if (is_pi(t)) { + binder_info bi = binding_info(t); + return bi.is_implicit() || bi.is_strict_implicit() || bi.is_inst_implicit(); + } else { + return false; + } } catch (exception &) { return false; } @@ -330,7 +335,10 @@ bool pretty_fn::is_implicit(expr const & f) { bool pretty_fn::is_prop(expr const & e) { try { - return m_env.impredicative() && m_tc.is_prop(e).first; + if (!m_env.impredicative()) + return false; + expr t = m_ctx.relaxed_whnf(m_ctx.infer(e)); + return t == mk_Prop(); } catch (exception &) { return false; } @@ -625,13 +633,13 @@ bool pretty_fn::has_implicit_args(expr const & f) { return false; } try { - expr type = m_tc.whnf(m_tc.infer(f).first).first; + expr type = m_ctx.relaxed_whnf(m_ctx.infer(f)); while (is_pi(type)) { binder_info bi = binding_info(type); if (bi.is_implicit() || bi.is_strict_implicit() || bi.is_inst_implicit()) return true; - expr local = mk_local(mk_fresh_name(), binding_name(type), binding_domain(type), binding_info(type)); - type = m_tc.whnf(instantiate(binding_body(type), local)).first; + expr local = m_ctx.mk_tmp_local(binding_name(type), binding_domain(type), binding_info(type)); + type = m_ctx.relaxed_whnf(instantiate(binding_body(type), local)); } return false; } catch (exception &) { @@ -950,10 +958,12 @@ bool pretty_fn::match(expr const & p, expr const & e, buffer> & a return true; } else { try { - expr fn_type = m_tc.infer(e_fn).first; + expr fn_type = m_ctx.infer(e_fn); unsigned j = 0; for (unsigned i = 0; i < e_args.size(); i++) { - fn_type = m_tc.ensure_pi(fn_type).first; + fn_type = m_ctx.relaxed_whnf(fn_type); + if (!is_pi(fn_type)) + return false; expr const & body = binding_body(fn_type); binder_info const & info = binding_info(fn_type); if ((!consume || closed(body)) && is_explicit(info)) { @@ -966,7 +976,7 @@ bool pretty_fn::match(expr const & p, expr const & e, buffer> & a fn_type = instantiate(body, e_args[i]); } return j == p_args.size(); - } catch (exception&) { + } catch (exception &) { return false; } } @@ -1279,8 +1289,8 @@ auto pretty_fn::pp(expr const & e, bool ignore_hide) -> result { lean_unreachable(); // LCOV_EXCL_LINE } -pretty_fn::pretty_fn(environment const & env, options const & o): - m_env(env), m_tc(env), m_token_table(get_token_table(env)) { +pretty_fn::pretty_fn(environment const & env, options const & o, abstract_type_context & ctx): + m_env(env), m_ctx(ctx), m_token_table(get_token_table(env)) { set_options_core(o); m_meta_prefix = "M"; m_next_meta_idx = 1; @@ -1380,8 +1390,8 @@ format pretty_fn::operator()(expr const & e) { } formatter_factory mk_pretty_formatter_factory() { - return [](environment const & env, options const & o, abstract_type_context &) { // NOLINT - auto fn_ptr = std::make_shared(env, o); + return [](environment const & env, options const & o, abstract_type_context & ctx) { // NOLINT + auto fn_ptr = std::make_shared(env, o, ctx); return formatter(o, [=](expr const & e, options const & new_o) { fn_ptr->set_options(new_o); return (*fn_ptr)(e); diff --git a/src/frontends/lean/pp.h b/src/frontends/lean/pp.h index cd494512a..e07b7cf92 100644 --- a/src/frontends/lean/pp.h +++ b/src/frontends/lean/pp.h @@ -14,7 +14,7 @@ Author: Leonardo de Moura #include "util/sexpr/options.h" #include "util/sexpr/format.h" #include "kernel/environment.h" -#include "kernel/type_checker.h" +#include "kernel/abstract_type_context.h" #include "frontends/lean/token_table.h" namespace lean { @@ -38,38 +38,38 @@ public: format const & fmt() const { return m_fmt; } }; private: - environment m_env; - type_checker m_tc; - token_table const & m_token_table; - unsigned m_num_steps; - unsigned m_depth; - name m_meta_prefix; - unsigned m_next_meta_idx; - name_map m_purify_meta_table; - name_set m_purify_used_metas; - name_map m_purify_local_table; - name_set m_purify_used_locals; + environment m_env; + abstract_type_context & m_ctx; + token_table const & m_token_table; + unsigned m_num_steps; + unsigned m_depth; + name m_meta_prefix; + unsigned m_next_meta_idx; + name_map m_purify_meta_table; + name_set m_purify_used_metas; + name_map m_purify_local_table; + name_set m_purify_used_locals; // cached configuration - options m_options; - unsigned m_indent; - unsigned m_max_depth; - unsigned m_max_steps; - bool m_implict; //!< if true show implicit arguments - bool m_unicode; //!< if true use unicode chars - bool m_coercion; //!< if true show coercions - bool m_num_nat_coe; //!< truen when !m_coercion && env has coercion from num -> nat - bool m_notation; - bool m_universes; - bool m_full_names; - bool m_private_names; - bool m_metavar_args; - bool m_purify_metavars; - bool m_purify_locals; - bool m_beta; - bool m_numerals; - bool m_abbreviations; - bool m_hide_full_terms; - bool m_preterm; + options m_options; + unsigned m_indent; + unsigned m_max_depth; + unsigned m_max_steps; + bool m_implict; //!< if true show implicit arguments + bool m_unicode; //!< if true use unicode chars + bool m_coercion; //!< if true show coercions + bool m_num_nat_coe; //!< truen when !m_coercion && env has coercion from num -> nat + bool m_notation; + bool m_universes; + bool m_full_names; + bool m_private_names; + bool m_metavar_args; + bool m_purify_metavars; + bool m_purify_locals; + bool m_beta; + bool m_numerals; + bool m_abbreviations; + bool m_hide_full_terms; + bool m_preterm; name mk_metavar_name(name const & m); name mk_local_name(name const & n, name const & suggested); @@ -122,7 +122,7 @@ private: void set_options_core(options const & o); public: - pretty_fn(environment const & env, options const & o); + pretty_fn(environment const & env, options const & o, abstract_type_context & ctx); result pp(expr const & e, bool ignore_hide = false); void set_options(options const & o); options const & get_options() const { return m_options; } diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index ba2f59001..599cfd49d 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -119,8 +119,7 @@ void init_token_table(token_table & t) { "add_begin_end_tactic", "set_begin_end_tactic", "instance", "class", "multiple_instances", "find_decl", "attribute", "persistent", "include", "omit", "migrate", "init_quotient", "init_hits", "#erase_cache", "#projections", "#telescope_eq", - "#compile", "#decl_stats", "#relevant_thms", "#simplify", "#app_builder", "#refl", "#symm", - "#trans", "#congr", "#hcongr", "#congr_simp", "#congr_rel", "#normalizer", "#abstract_expr", "#unify", + "#compile", "#decl_stats", "#relevant_thms", "#simplify", "#normalizer", "#abstract_expr", "#unify", "#defeq_simplify", nullptr}; pair aliases[] = diff --git a/src/kernel/abstract_type_context.h b/src/kernel/abstract_type_context.h index fac3b678a..fd75e3f2e 100644 --- a/src/kernel/abstract_type_context.h +++ b/src/kernel/abstract_type_context.h @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once +#include "util/fresh_name.h" #include "kernel/expr.h" namespace lean { @@ -20,11 +21,17 @@ public: virtual ~abstract_type_context() {} virtual environment const & env() const = 0; virtual expr whnf(expr const & e) = 0; + virtual expr relaxed_whnf(expr const & e) { return whnf(e); } virtual bool is_def_eq(expr const & e1, expr const & e2) = 0; + virtual bool relaxed_is_def_eq(expr const & e1, expr const & e2) { return is_def_eq(e1, e2); } virtual expr infer(expr const & e) = 0; /** \brief Simular to \c infer, but also performs type checking. \remark Default implementation just invokes \c infer. */ virtual expr check(expr const & e) { return infer(e); } virtual optional is_stuck(expr const &) { return none_expr(); } + virtual name get_local_pp_name(expr const & e) { return local_pp_name(e); } + virtual expr mk_tmp_local(name const & pp_name, expr const & type, binder_info const & bi = binder_info()) { + return mk_local(mk_fresh_name(), pp_name, type, bi); + } }; } diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp index 4905bcdcc..c7793b195 100644 --- a/src/library/blast/blast.cpp +++ b/src/library/blast/blast.cpp @@ -245,11 +245,14 @@ class blastenv { virtual expr infer_metavar(expr const & m) const override { // Remark: we do not tolerate external meta-variables here. - lean_assert(is_mref(m)); - state const & s = m_benv.m_curr_state; - metavar_decl const * d = s.get_metavar_decl(m); - lean_assert(d); - return d->get_type(); + if (is_mref(m)) { + state const & s = m_benv.m_curr_state; + metavar_decl const * d = s.get_metavar_decl(m); + lean_assert(d); + return d->get_type(); + } else { + return mlocal_type(m); + } } virtual level mk_uvar() override { diff --git a/src/library/tactic/contradiction_tactic.cpp b/src/library/tactic/contradiction_tactic.cpp index ef26ef882..07952c3ef 100644 --- a/src/library/tactic/contradiction_tactic.cpp +++ b/src/library/tactic/contradiction_tactic.cpp @@ -14,7 +14,7 @@ Author: Leonardo de Moura namespace lean { tactic contradiction_tactic() { - auto fn = [=](environment const & env, io_state const & ios, proof_state const & s) { + auto fn = [=](environment const & env, io_state const &, proof_state const & s) { goals const & gs = s.get_goals(); if (empty(gs)) { throw_no_goal_if_enabled(s); diff --git a/src/library/type_context.h b/src/library/type_context.h index 5bfc9acb1..09007bd82 100644 --- a/src/library/type_context.h +++ b/src/library/type_context.h @@ -329,7 +329,7 @@ public: /** \brief Create a temporary local constant using the given pretty print name. The pretty printing name has not semantic significance. */ - expr mk_tmp_local(name const & pp_name, expr const & type, binder_info const & bi = binder_info()); + virtual expr mk_tmp_local(name const & pp_name, expr const & type, binder_info const & bi = binder_info()) override; /** \brief Create a temporary local constant based on the domain of the given binding (lambda/Pi) expression */ expr mk_tmp_local_from_binding(expr const & b) { @@ -440,10 +440,10 @@ public: expr instantiate_uvars_mvars(expr const & e); /** \brief Put the given term in weak-head-normal-form (modulo is_opaque predicate) */ - expr whnf(expr const & e); + virtual expr whnf(expr const & e) override; /** \brief Similar to previous method but ignores the is_extra_opaque predicate. */ - expr relaxed_whnf(expr const & e); + virtual expr relaxed_whnf(expr const & e) override; /** \brief Return true if \c e is a proposition */ bool is_prop(expr const & e); @@ -462,9 +462,9 @@ public: It is precise if \c e1 and \c e2 do not contain metavariables. */ - bool is_def_eq(expr const & e1, expr const & e2); + virtual bool is_def_eq(expr const & e1, expr const & e2) override; /** \brief Similar to \c is_def_eq, but sets m_relax_is_opaque */ - bool relaxed_is_def_eq(expr const & e1, expr const & e2); + virtual bool relaxed_is_def_eq(expr const & e1, expr const & e2) override; /** \brief Return the universe level for type A. If A is not a type return none. */ optional get_level_core(expr const & A);