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

feat(frontends/lean): add 'opaque_hint' command

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-05 18:58:20 -07:00
parent e68a3e5251
commit 55894f01e3
9 changed files with 178 additions and 47 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/emacs/lean-mode.el
View file

@ -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)

43
src/frontends/lean/builtin_cmds.cpp
View file

@ -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);

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

@ -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> constraint_vect;
typedef name_map<expr> tactic_hints;
typedef name_map<expr> mvar2meta;
typedef std::unique_ptr<type_checker> 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);

4
src/frontends/lean/token_table.cpp
View file

@ -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",

2
src/library/CMakeLists.txt
View file

@ -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})

59
src/library/opaque_hints.cpp Normal file
View file

@ -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<opaque_hints_ext>()); }
};
static opaque_hints_ext_reg g_ext;
static opaque_hints_ext const & get_extension(environment const & env) {
return static_cast<opaque_hints_ext const &>(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<opaque_hints_ext>(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<type_checker> mk_type_checker_with_hints(environment const & env, name_generator const & ngen) {
auto const & ext = get_extension(env);
return std::unique_ptr<type_checker>(new type_checker(env, ngen, mk_default_converter(env, !ext.m_hide_module,
true, ext.m_extra_opaque)));
}
}

33
src/library/opaque_hints.h Normal file
View file

@ -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<type_checker> mk_type_checker_with_hints(environment const & env, name_generator const & ngen);
}

31
src/library/unifier.cpp
View file

@ -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, cnstr_cmp> cnstr_set;
typedef rb_tree<unsigned, unsigned_cmp> cnstr_idx_set;
typedef rb_map<name, cnstr_idx_set, name_quick_cmp> name_to_cnstrs;
typedef std::unique_ptr<type_checker> 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<constraints> alts = m_plugin->solve(m_tc, c, m_ngen.mk_child());
lazy_list<constraints> 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<constraints> 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<expr> margs;
expr m = get_app_args(lhs, margs);
for (expr & marg : margs)
marg = m_tc.whnf(marg);
marg = m_tc->whnf(marg);
buffer<constraints> 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<substitution> unify(environment const & env, expr const & lhs, expr co
auto u = std::make_shared<unifier_fn>(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<substitution>();
else
return unify(u);

21
tests/lean/run/class4.lean
View file

@ -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))