From 55894f01e369a8b5b8c998cc29a5f03f2a98181a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 5 Jul 2014 18:58:20 -0700 Subject: [PATCH] feat(frontends/lean): add 'opaque_hint' command Signed-off-by: Leonardo de Moura --- src/emacs/lean-mode.el | 2 +- src/frontends/lean/builtin_cmds.cpp | 43 +++++++++++++++++++++ src/frontends/lean/elaborator.cpp | 30 ++++++++------- src/frontends/lean/token_table.cpp | 4 +- src/library/CMakeLists.txt | 2 +- src/library/opaque_hints.cpp | 59 +++++++++++++++++++++++++++++ src/library/opaque_hints.h | 33 ++++++++++++++++ src/library/unifier.cpp | 31 +++++++-------- tests/lean/run/class4.lean | 21 ++++------ 9 files changed, 178 insertions(+), 47 deletions(-) create mode 100644 src/library/opaque_hints.cpp create mode 100644 src/library/opaque_hints.h diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el index a1abe4f6b..7fbd90be7 100644 --- a/src/emacs/lean-mode.el +++ b/src/emacs/lean-mode.el @@ -24,7 +24,7 @@ (define-generic-mode 'lean-mode ;; name of the mode to create '("--") ;; comments start with - '("import" "abbreviation" "definition" "parameter" "parameters" "proof" "qed" "conjecture" "hypothesis" "lemma" "corollary" "variable" "variables" "print" "theorem" "axiom" "inductive" "with" "universe" "alias" "help" "environment" "options" "precedence" "postfix" "prefix" "calc_trans" "calc_subst" "calc_refl" "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end" "using" "namespace" "builtin" "including" "class" "instance" "section" "set_option" "add_rewrite") ;; some keywords + '("import" "abbreviation" "opaque_hint" "definition" "hiding" "exposing" "parameter" "parameters" "proof" "qed" "conjecture" "hypothesis" "lemma" "corollary" "variable" "variables" "print" "theorem" "axiom" "inductive" "with" "universe" "alias" "help" "environment" "options" "precedence" "postfix" "prefix" "calc_trans" "calc_subst" "calc_refl" "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end" "using" "namespace" "builtin" "including" "class" "instance" "section" "set_option" "add_rewrite") ;; some keywords '(("\\_<\\(Bool\\|Int\\|Nat\\|Real\\|Type\\|TypeU\\|ℕ\\|ℤ\\)\\_>" . 'font-lock-type-face) ("\\_<\\(calc\\|have\\|show\\|by\\|in\\|let\\|forall\\|fun\\|exists\\|if\\|then\\|else\\|assume\\|take\\|obtain\\|from\\)\\_>" . font-lock-keyword-face) ("\"[^\"]*\"" . 'font-lock-string-face) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 140ede3fb..3df3a5f1d 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -14,6 +14,7 @@ Author: Leonardo de Moura #include "library/aliases.h" #include "library/locals.h" #include "library/coercion.h" +#include "library/opaque_hints.h" #include "frontends/lean/util.h" #include "frontends/lean/parser.h" #include "frontends/lean/calc.h" @@ -36,7 +37,9 @@ static name g_rbracket("]"); static name g_declarations("declarations"); static name g_decls("decls"); static name g_hiding("hiding"); +static name g_exposing("exposing"); static name g_renaming("renaming"); +static name g_module("[module]"); static name g_colon(":"); environment print_cmd(parser & p) { @@ -233,6 +236,45 @@ environment coercion_cmd(parser & p) { } } +environment opaque_hint_cmd(parser & p) { + environment env = p.env(); + bool found = false; + while (p.curr_is_token(g_lparen)) { + p.next(); + bool hiding; + auto pos = p.pos(); + if (p.curr_is_token_or_id(g_hiding)) + hiding = true; + else if (p.curr_is_token_or_id(g_exposing)) + hiding = false; + else + throw parser_error("invalid 'opaque_hint', 'hiding' or 'exposing' expected", pos); + p.next(); + while (!p.curr_is_token(g_rparen)) { + if (p.curr_is_token(g_module)) { + found = true; + p.next(); + env = set_main_module_opaque_defs(env, hiding); + } else { + auto pos = p.pos(); + name id = p.check_id_next("invalid 'opaque_hint', identifier expected"); + found = true; + expr e = p.id_to_expr(id, pos); + if (!is_constant(e)) + throw parser_error(sstream() << "'" << id << "' is not a constant", pos); + if (hiding) + env = hide_definition(env, const_name(e)); + else + env = expose_definition(env, const_name(e)); + } + } + p.next(); + } + if (!found) + throw exception("invalid empty 'opaque_hint' command"); + return env; +} + cmd_table init_cmd_table() { cmd_table r; add_cmd(r, cmd_info("using", "create aliases for declarations, and use objects defined in other namespaces", using_cmd)); @@ -244,6 +286,7 @@ cmd_table init_cmd_table() { add_cmd(r, cmd_info("end", "close the current namespace/section", end_scoped_cmd)); add_cmd(r, cmd_info("check", "type check given expression, and display its type", check_cmd)); add_cmd(r, cmd_info("coercion", "add a new coercion", coercion_cmd)); + add_cmd(r, cmd_info("opaque_hint", "add hints for the elaborator/unifier", opaque_hint_cmd)); add_cmd(r, cmd_info("#setline", "modify the current line number, it only affects error/report messages", set_line_cmd)); register_decl_cmds(r); register_inductive_cmd(r); diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 3c03ec58f..aa0ef3454 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -23,6 +23,7 @@ Author: Leonardo de Moura #include "library/choice.h" #include "library/explicit.h" #include "library/unifier.h" +#include "library/opaque_hints.h" #include "library/tactic/tactic.h" #include "library/tactic/expr_to_tactic.h" #include "library/error_handling/error_handling.h" @@ -47,11 +48,12 @@ class elaborator { typedef std::vector constraint_vect; typedef name_map tactic_hints; typedef name_map mvar2meta; + typedef std::unique_ptr type_checker_ptr; environment m_env; io_state m_ios; name_generator m_ngen; - type_checker m_tc; + type_checker_ptr m_tc; substitution m_subst; context m_ctx; pos_info_provider * m_pos_provider; @@ -77,12 +79,12 @@ class elaborator { lean_assert(m_main.m_accumulated.is_none()); m_old_ctx = m_main.m_ctx; m_main.m_ctx = ctx; - m_main.m_tc.push(); + m_main.m_tc->push(); m_main.m_subst = s; } ~scope() { m_main.m_ctx = m_old_ctx; - m_main.m_tc.pop(); + m_main.m_tc->pop(); m_main.m_constraints.clear(); m_main.m_accumulated = justification(); m_main.m_subst = substitution(); @@ -92,7 +94,7 @@ class elaborator { }; void consume_tc_cnstrs() { - while (auto c = m_tc.next_cnstr()) + while (auto c = m_tc->next_cnstr()) m_constraints.push_back(*c); } @@ -194,7 +196,7 @@ public: elaborator(environment const & env, io_state const & ios, name_generator const & ngen, pos_info_provider * pp, bool check_unassigned): m_env(env), m_ios(ios), - m_ngen(ngen), m_tc(env, m_ngen.mk_child(), mk_default_converter(m_env, true /* unfold opaque from the main module */)), + m_ngen(ngen), m_tc(mk_type_checker_with_hints(env, m_ngen.mk_child())), m_pos_provider(pp) { m_check_unassigned = check_unassigned; m_use_local_instances = get_elaborator_local_instances(ios.get_options()); @@ -206,10 +208,10 @@ public: expr infer_type(expr const & e) { lean_assert(closed(e)); - return m_tc.infer(e); } + return m_tc->infer(e); } expr whnf(expr const & e) { - return m_tc.whnf(e); + return m_tc->whnf(e); } /** \brief Clear constraint buffer \c m_constraints, and associated datastructures @@ -484,7 +486,7 @@ public: f_type = whnf(instantiate_metavars(f_type)); if (!is_pi(f_type) && is_meta(f_type)) { // let type checker add constraint - f_type = m_tc.ensure_pi(f_type, f); + f_type = m_tc->ensure_pi(f_type, f); } } if (!is_pi(f_type)) { @@ -568,12 +570,12 @@ public: return mk_delayed_coercion(r, d_type, a_type); } else { app_delayed_justification j(m_env, r, f_type, a_type); - if (!m_tc.is_def_eq(a_type, d_type, j)) { + if (!m_tc->is_def_eq(a_type, d_type, j)) { expr new_a = apply_coercion(a, a_type, d_type); bool coercion_worked = false; if (!is_eqp(a, new_a)) { expr new_a_type = instantiate_metavars(infer_type(new_a)); - coercion_worked = m_tc.is_def_eq(new_a_type, d_type, j); + coercion_worked = m_tc->is_def_eq(new_a_type, d_type, j); } if (coercion_worked) { r = update_app(r, f, new_a); @@ -650,7 +652,7 @@ public: return e; if (is_meta(t)) { // let type checker add constraint - m_tc.ensure_sort(t, e); + m_tc->ensure_sort(t, e); return e; } } @@ -818,7 +820,7 @@ public: l = subst.instantiate(l); mvar = update_mlocal(mvar, subst.instantiate(mlocal_type(mvar))); meta = ::lean::mk_app(mvar, locals); - expr type = m_tc.infer(*meta); + expr type = m_tc->infer(*meta); // first solve unassigned metavariables in type type = solve_unassigned_mvars(subst, type, visited); proof_state ps(goals(goal(*meta, type)), subst, m_ngen.mk_child()); @@ -913,7 +915,7 @@ public: justification j = mk_justification(e, [=](formatter const & fmt, options const & opts, substitution const & subst) { return pp_type_mismatch(fmt, env, opts, subst.instantiate(expected_type), subst.instantiate(r_type)); }); - if (!m_tc.is_def_eq(r_type, expected_type, j)) { + if (!m_tc->is_def_eq(r_type, expected_type, j)) { throw_kernel_exception(env, e, [=](formatter const & fmt, options const & o) { return pp_type_mismatch(fmt, env, o, expected_type, r_type); @@ -933,7 +935,7 @@ public: justification j = mk_justification(v, [=](formatter const & fmt, options const & o, substitution const & subst) { return pp_def_type_mismatch(fmt, env, o, n, subst.instantiate(r_t), subst.instantiate(r_v_type)); }); - if (!m_tc.is_def_eq(r_v_type, r_t, j)) { + if (!m_tc->is_def_eq(r_v_type, r_t, j)) { throw_kernel_exception(env, v, [=](formatter const & fmt, options const & o) { return pp_def_type_mismatch(fmt, env, o, n, r_t, r_v_type); diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 89172ae7b..154cbd008 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -63,8 +63,8 @@ token_table init_token_table() { {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {nullptr, 0}}; char const * commands[] = {"theorem", "axiom", "variable", "definition", "coercion", - "variables", "[private]", "[inline]", "[fact]", "[instance]", "[class]", "abbreviation", - "evaluate", "check", "print", "end", "namespace", "section", "import", + "variables", "[private]", "[inline]", "[fact]", "[instance]", "[class]", "[module]", + "abbreviation", "opaque_hint", "evaluate", "check", "print", "end", "namespace", "section", "import", "abbreviation", "inductive", "record", "structure", "module", "universe", "precedence", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "exit", "set_option", "using", "calc_subst", "calc_refl", "calc_trans", diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 728da6cea..daae5ee67 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -6,7 +6,7 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp update_declaration.cpp choice.cpp scoped_ext.cpp locals.cpp standard_kernel.cpp hott_kernel.cpp unifier.cpp unifier_plugin.cpp inductive_unifier_plugin.cpp - explicit.cpp num.cpp string.cpp) + explicit.cpp num.cpp string.cpp opaque_hints.cpp) # hop_match.cpp) target_link_libraries(library ${LEAN_LIBS}) diff --git a/src/library/opaque_hints.cpp b/src/library/opaque_hints.cpp new file mode 100644 index 000000000..efb6824a2 --- /dev/null +++ b/src/library/opaque_hints.cpp @@ -0,0 +1,59 @@ +/* +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/sstream.h" +#include "kernel/environment.h" +#include "kernel/type_checker.h" + +namespace lean { +struct opaque_hints_ext : public environment_extension { + name_set m_extra_opaque; + bool m_hide_module; + opaque_hints_ext():m_hide_module(false) {} +}; + +struct opaque_hints_ext_reg { + unsigned m_ext_id; + opaque_hints_ext_reg() { m_ext_id = environment::register_extension(std::make_shared()); } +}; +static opaque_hints_ext_reg g_ext; +static opaque_hints_ext const & get_extension(environment const & env) { + return static_cast(env.get_extension(g_ext.m_ext_id)); +} +static environment update(environment const & env, opaque_hints_ext const & ext) { + return env.update(g_ext.m_ext_id, std::make_shared(ext)); +} +static void check_definition(environment const & env, name const & n) { + declaration d = env.get(n); + if (!d.is_definition()) + throw exception(sstream() << "invalid opaque_hint, '" << n << "' is not a definition"); +} +environment hide_definition(environment const & env, name const & n) { + check_definition(env, n); + auto ext = get_extension(env); + ext.m_extra_opaque.insert(n); + return update(env, ext); +} +environment expose_definition(environment const & env, name const & n) { + check_definition(env, n); + auto ext = get_extension(env); + if (!ext.m_extra_opaque.contains(n)) + throw exception(sstream() << "invalid 'exposing' opaque_hint, '" << n << "' is not in the 'extra opaque' set"); + ext.m_extra_opaque.erase(n); + return update(env, ext); +} +environment set_main_module_opaque_defs(environment const & env, bool f) { + auto ext = get_extension(env); + ext.m_hide_module = f; + return update(env, ext); +} +std::unique_ptr mk_type_checker_with_hints(environment const & env, name_generator const & ngen) { + auto const & ext = get_extension(env); + return std::unique_ptr(new type_checker(env, ngen, mk_default_converter(env, !ext.m_hide_module, + true, ext.m_extra_opaque))); +} +} + diff --git a/src/library/opaque_hints.h b/src/library/opaque_hints.h new file mode 100644 index 000000000..1d7720068 --- /dev/null +++ b/src/library/opaque_hints.h @@ -0,0 +1,33 @@ +/* +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" + +namespace lean { +/* + Opaque hints are used to 'help/guide' the elaborator and unifier. + We can use them to mark additional definitions as opaque. + Note that we are not changing the status of the definitions, we are + only changing how the elaborator/unifier treats them. + + These hints are not used when we type check a definition before + adding it to the kernel. +*/ + +/** \brief Mark the definition named \c n as opaque for the elaborator/unifier. */ +environment hide_definition(environment const & env, name const & n); +/** \brief Undo the modification made with \c hide_definition. */ +environment expose_definition(environment const & env, name const & n); +/** + \brief By default, the elaborator/unifier will treat the opaque + definitions of the current/main module as transparent. We can + change this behavior using this function. +*/ +environment set_main_module_opaque_defs(environment const & env, bool f); +/** \brief Create a type checker that takes the hints into account. */ +std::unique_ptr mk_type_checker_with_hints(environment const & env, name_generator const & ngen); +} diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index b3cb54155..e8a2290b2 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -18,6 +18,7 @@ Author: Leonardo de Moura #include "kernel/type_checker.h" #include "library/occurs.h" #include "library/unifier.h" +#include "library/opaque_hints.h" #include "library/unifier_plugin.h" #include "library/kernel_bindings.h" @@ -279,12 +280,12 @@ struct unifier_fn { typedef rb_tree cnstr_set; typedef rb_tree cnstr_idx_set; typedef rb_map name_to_cnstrs; - + typedef std::unique_ptr type_checker_ptr; environment m_env; name_generator m_ngen; substitution m_subst; unifier_plugin m_plugin; - type_checker m_tc; + type_checker_ptr m_tc; bool m_use_exception; //!< True if we should throw an exception when there are no more solutions. unsigned m_max_steps; unsigned m_num_steps; @@ -335,14 +336,14 @@ struct unifier_fn { m_assumption_idx(u.m_next_assumption_idx), m_subst(u.m_subst), m_cnstrs(u.m_cnstrs), m_mvar_occs(u.m_mvar_occs), m_mlvl_occs(u.m_mlvl_occs) { u.m_next_assumption_idx++; - u.m_tc.push(); + u.m_tc->push(); } /** \brief Restore unifier's state with saved values, and update m_assumption_idx and m_failed_justifications. */ void restore_state(unifier_fn & u) { lean_assert(u.in_conflict()); - u.m_tc.pop(); // restore type checker state - u.m_tc.push(); + u.m_tc->pop(); // restore type checker state + u.m_tc->push(); u.m_subst = m_subst; u.m_cnstrs = m_cnstrs; u.m_mvar_occs = m_mvar_occs; @@ -377,7 +378,7 @@ struct unifier_fn { name_generator const & ngen, substitution const & s, bool use_exception, unsigned max_steps): m_env(env), m_ngen(ngen), m_subst(s), m_plugin(get_unifier_plugin(env)), - m_tc(env, m_ngen.mk_child(), mk_default_converter(env, true)), + m_tc(mk_type_checker_with_hints(env, m_ngen.mk_child())), m_use_exception(use_exception), m_max_steps(max_steps), m_num_steps(0) { m_next_assumption_idx = 0; m_next_cidx = 0; @@ -467,7 +468,7 @@ struct unifier_fn { } bool is_def_eq(expr const & t1, expr const & t2, justification const & j) { - if (m_tc.is_def_eq(t1, t2, j)) { + if (m_tc->is_def_eq(t1, t2, j)) { return true; } else { set_conflict(j); @@ -484,7 +485,7 @@ struct unifier_fn { lean_assert(is_metavar(m)); m_subst.d_assign(m, v, j); expr m_type = mlocal_type(m); - expr v_type = m_tc.infer(v); + expr v_type = m_tc->infer(v); if (in_conflict()) return false; if (!is_def_eq(m_type, v_type, j)) @@ -601,7 +602,7 @@ struct unifier_fn { if (is_eq_deltas(lhs, rhs)) { // we need to create a backtracking point for this one add_cnstr(c, &unassigned_lvls, &unassigned_exprs, cnstr_group::Basic); - } else if (m_plugin->delay_constraint(m_tc, c)) { + } else if (m_plugin->delay_constraint(*m_tc, c)) { add_cnstr(c, &unassigned_lvls, &unassigned_exprs, cnstr_group::PluginDelayed); } else if (is_meta(lhs) && is_meta(rhs)) { // flex-flex constraints are delayed the most. @@ -752,7 +753,7 @@ struct unifier_fn { return true; } } - m_tc.pop(); + m_tc->pop(); m_case_splits.pop_back(); } return false; @@ -806,7 +807,7 @@ struct unifier_fn { bool process_plugin_constraint(constraint const & c) { lean_assert(!is_choice_cnstr(c)); - lazy_list alts = m_plugin->solve(m_tc, c, m_ngen.mk_child()); + lazy_list alts = m_plugin->solve(*m_tc, c, m_ngen.mk_child()); return process_lazy_constraints(alts, c.get_justification()); } @@ -814,7 +815,7 @@ struct unifier_fn { lean_assert(is_choice_cnstr(c)); expr const & m = cnstr_expr(c); choice_fn const & fn = cnstr_choice_fn(c); - auto m_type_jst = m_subst.instantiate_metavars(m_tc.infer(m), nullptr, nullptr); + auto m_type_jst = m_subst.instantiate_metavars(m_tc->infer(m), nullptr, nullptr); lazy_list alts = fn(m, m_type_jst.first, m_subst, m_ngen.mk_child()); return process_lazy_constraints(alts, mk_composite1(c.get_justification(), m_type_jst.second)); } @@ -1051,7 +1052,7 @@ struct unifier_fn { buffer margs; expr m = get_app_args(lhs, margs); for (expr & marg : margs) - marg = m_tc.whnf(marg); + marg = m_tc->whnf(marg); buffer alts; switch (rhs.kind()) { case expr_kind::Var: case expr_kind::Meta: @@ -1124,7 +1125,7 @@ struct unifier_fn { while (true) { if (in_conflict()) return; - if (auto c = m_tc.next_cnstr()) { + if (auto c = m_tc->next_cnstr()) { process_constraint(*c); } else { break; @@ -1218,7 +1219,7 @@ lazy_list unify(environment const & env, expr const & lhs, expr co auto u = std::make_shared(env, 0, nullptr, ngen, s, false, max_steps); expr _lhs = s.instantiate(lhs); expr _rhs = s.instantiate(rhs); - if (!u->m_tc.is_def_eq(_lhs, _rhs)) + if (!u->m_tc->is_def_eq(_lhs, _rhs)) return lazy_list(); else return unify(u); diff --git a/tests/lean/run/class4.lean b/tests/lean/run/class4.lean index 2ea45df96..21e7907d2 100644 --- a/tests/lean/run/class4.lean +++ b/tests/lean/run/class4.lean @@ -71,25 +71,18 @@ variable div : Π (x y : nat) {H : not_zero y}, nat variables a b : nat +opaque_hint (hiding [module]) check div a (succ b) check (λ H : not_zero b, div a b) check (succ zero) check a + (succ zero) check div a (a + (succ b)) -exit +opaque_hint (exposing [module]) +check div a (a + (succ b)) -inductive not_zero : nat → Bool := -| not_zero_intro : Π (x : nat), not_zero (succ x) - -class not_zero -instance not_zero_intro - - -theorem not_zero (x : nat) (H : not_zero x) : → - -exit - - -axiom add_not_zero : ∀ {x y : nat}, not_zero x → not_zero y → not_zero (x + y) +opaque_hint (hiding add) +check div a (a + (succ b)) +opaque_hint (exposing add) +check div a (a + (succ b))