max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(kernel/declaration,*): all theorems are delayed, and are revealed on delta-reduction

Browse source
This commit is contained in:
Gabriel Ebner 2016-11-17 18:33:44 -05:00 • committed by Leonardo de Moura
parent 339ade623d
commit 385ea13688
20 changed files with 170 additions and 224 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
extras/latex/lstlean.tex
View file

@ -19,7 +19,7 @@ open, as, export, override, axiom, axioms, inductive, with, structure, record, u
alias, help, environment, options, precedence, reserve,
match, infix, infixl, infixr, notation, postfix, prefix,
tactic_infix, tactic_infixl, tactic_infixr, tactic_notation, tactic_postfix, tactic_prefix,
eval, check, coercion, end, reveal, this, suppose,
eval, check, coercion, end, this, suppose,
using, namespace, section, fields, find_decl,
attribute, local, set_option, extends, include, omit, classes,
instances, coercions, attributes, raw, migrate, replacing,

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

@ -16,7 +16,7 @@
"structure" "record" "universe" "universes"
"alias" "help" "precedence" "reserve" "declare_trace" "add_key_equivalence"
"match" "infix" "infixl" "infixr" "notation" "postfix" "prefix" "instance"
"eval" "vm_eval" "check" "end" "reveal" "this" "suppose"
"eval" "vm_eval" "check" "end" "this" "suppose"
"using" "using_well_founded" "namespace" "section" "fields"
"attribute" "local" "set_option" "extends" "include" "omit" "classes" "class"
"instances" "coercions" "attributes" "raw" "replacing"

12
src/frontends/lean/decl_cmds.cpp
View file

@ -577,17 +577,6 @@ static environment omit_cmd(parser & p) {
return include_cmd_core(p, false);
}
static environment reveal_cmd(parser & p) {
buffer<name> ds;
name d = p.check_constant_next("invalid 'reveal' command, constant expected");
ds.push_back(d);
while (p.curr_is_identifier()) {
ds.push_back(p.check_constant_next("invalid 'reveal' command, constant expected"));
}
return p.reveal_theorems(ds);
}
void register_decl_cmds(cmd_table & r) {
add_cmd(r, cmd_info("universe", "declare a universe level", universe_cmd));
add_cmd(r, cmd_info("universes", "declare universe levels", universes_cmd));
@ -608,7 +597,6 @@ void register_decl_cmds(cmd_table & r) {
add_cmd(r, cmd_info("theorem", "add new theorem", definition_cmd, false));
add_cmd(r, cmd_info("instance", "add new instance", definition_cmd, false));
add_cmd(r, cmd_info("example", "add new example", definition_cmd, false));
add_cmd(r, cmd_info("reveal", "reveal given theorems", reveal_cmd));
add_cmd(r, cmd_info("include", "force section parameter/variable to be included", include_cmd));
add_cmd(r, cmd_info("attribute", "set declaration attributes", attribute_cmd));
add_cmd(r, cmd_info("@[", "declaration attributes", compact_attribute_cmd));

9
src/frontends/lean/definition_cmds.cpp
View file

@ -345,7 +345,7 @@ static expr fix_rec_fn_name(expr const & e, name const & c_name, name const & c_
static pair<environment, name>
declare_definition(parser & p, environment const & env, def_cmd_kind kind, buffer<name> const & lp_names,
name const & c_name, expr const & type, optional<expr> const & _val,
name const & c_name, expr const & type, optional<expr> const & _val, task_result<expr> const & proof,
decl_modifiers const & modifiers, decl_attributes attrs, optional<std::string> const & doc_string,
pos_info const & pos) {
auto env_n = mk_real_name(env, c_name, modifiers.m_is_private, pos);
@ -357,7 +357,7 @@ declare_definition(parser & p, environment const & env, def_cmd_kind kind, buffe
bool use_conv_opt = true;
bool is_trusted = !modifiers.m_is_meta;
auto def =
!val ? mk_axiom(c_real_name, to_list(lp_names), type) : (kind == Theorem ?
!val ? mk_theorem(c_real_name, to_list(lp_names), type, proof) : (kind == Theorem ?
mk_theorem(c_real_name, to_list(lp_names), type, *val) :
mk_definition(new_env, c_real_name, to_list(lp_names), type, *val, use_conv_opt, is_trusted));
auto cdef = check(p, new_env, c_name, def, pos);
@ -764,9 +764,8 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif
decl_env, p.get_options(), params_vec, new_fn, val,
elab.mctx(), elab.lctx(), p.get_parser_pos_provider(header_pos));
env_n = declare_definition(p, elab.env(), kind, lp_names, c_name, type, opt_val, modifiers, attrs,
env_n = declare_definition(p, elab.env(), kind, lp_names, c_name, type, opt_val, elab_task, modifiers, attrs,
doc_string, header_pos);
p.add_delayed_theorem(delayed_theorem {false, decl_env, env_n.first.get(env_n.second), elab_task, {}});
} else if (kind == Example) {
std::vector<expr> params_vec(new_params.begin(), new_params.end());
get_global_task_queue().submit<example_checking_task>(
@ -789,7 +788,7 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif
}
finalize_definition(elab, new_params, type, val, lp_names);
opt_val = optional<expr>(val);
env_n = declare_definition(p, elab.env(), kind, lp_names, c_name, type, opt_val, modifiers, attrs, doc_string, header_pos);
env_n = declare_definition(p, elab.env(), kind, lp_names, c_name, type, opt_val, {}, modifiers, attrs, doc_string, header_pos);
}
environment new_env = env_n.first;
name c_real_name = env_n.second;

77
src/frontends/lean/parser.cpp
View file

@ -183,7 +183,6 @@ parser::parser(environment const & env, io_state const & ios,
if (s) {
m_env = s->m_env;
m_ios.set_options(s->m_options);
m_delayed_thms = s->m_delayed_thms;
m_old_buckets_from_snapshot = s->m_sub_buckets;
m_local_level_decls = s->m_lds;
m_local_decls = s->m_eds;
@ -2111,11 +2110,9 @@ void parser::process_imports() {
unsigned fingerprint = 0;
auto imports = parse_imports(fingerprint);
name_map<task_result<certified_declaration>> del_thms;
for (auto & n : imports) {
try {
m_env = import_module(m_env, m_file_name, n, del_thms, m_import_fn);
m_env = import_module(m_env, m_file_name, n, m_import_fn);
} catch (exception & ex) {
m_found_errors = true;
parser_exception error((sstream() << "invalid import '" << n.m_name << "'").str(),
@ -2127,13 +2124,6 @@ void parser::process_imports() {
}
}
del_thms.for_each([=] (name const & thm_name, task_result<certified_declaration> const & cdecl) {
delayed_theorem del_thm;
del_thm.m_imported = true;
del_thm.m_cert_decl = cdecl;
m_delayed_thms.insert(thm_name, del_thm);
});
m_env = update_fingerprint(m_env, fingerprint);
m_env = activate_export_decls(m_env, {}); // explicitly activate exports in root namespace
m_env = replay_export_decls_core(m_env, m_ios);
@ -2241,43 +2231,11 @@ bool parser::curr_is_command_like() const {
}
}
static void replace_theorem(certified_declaration const & thm, environment & env, bool ignore_noncomputable) {
// TODO(gabriel): move somewhere else
env = env.replace(thm);
name const & thm_name = thm.get_declaration().get_name();
if (!ignore_noncomputable && !check_computable(env, thm_name)) {
throw exception(sstream() << "declaration '" << thm_name
<< "' was marked as a theorem, but it is a noncomputable definition");
}
}
environment parser::reveal_theorems(buffer<name> const & ds) {
environment env = m_env;
for (auto & d : ds) {
if (auto * dt = m_delayed_thms.find(d)) {
replace_theorem(dt->m_cert_decl.get(), env, m_ignore_noncomputable);
} else {
throw exception(sstream() << "not a delayed theorem: " << d);
}
}
return env;
}
environment parser::reveal_all_theorems() {
buffer<name> ds;
m_delayed_thms.for_each([&] (name const & d, delayed_theorem const &) { ds.push_back(d); });
return reveal_theorems(ds);
}
bool parser::is_delayed_theorem(name const & n) {
return m_delayed_thms.contains(n);
}
void parser::save_snapshot(scope_message_context & smc) {
if (!m_snapshot_vector)
return;
if (m_snapshot_vector->empty() || m_snapshot_vector->back().m_pos != m_scanner.get_pos_info()) {
m_snapshot_vector->push_back(snapshot(m_env, smc.get_sub_buckets(), m_delayed_thms, m_local_level_decls, m_local_decls,
m_snapshot_vector->push_back(snapshot(m_env, smc.get_sub_buckets(), m_local_level_decls, m_local_decls,
m_level_variables, m_variables, m_include_vars,
m_ios.get_options(), m_imports_parsed, m_parser_scope_stack, m_scanner.get_pos_info()));
}
@ -2309,37 +2267,6 @@ message_builder parser::mk_message(message_severity severity) {
return mk_message(pos(), severity);
}
class proof_checking_task : public module_task<certified_declaration> {
delayed_theorem m_del_thm;
public:
proof_checking_task(delayed_theorem const & del_thm, pos_info const & pos) :
module_task(optional<pos_info>(pos), task_kind::elab), m_del_thm(del_thm) {}
void description(std::ostream & out) const override {
out << "checking " << m_del_thm.m_ax_decl.get_name() << " (" << get_module() << ")";
}
std::vector<generic_task_result> get_dependencies() override { return { m_del_thm.m_proof }; }
certified_declaration execute_core() override {
auto & ax_decl = m_del_thm.m_ax_decl;
auto thm_decl = mk_theorem(ax_decl.get_name(), ax_decl.get_univ_params(),
ax_decl.get_type(), m_del_thm.m_proof.get());
// TODO(gabriel): noncomputability check
return check(m_del_thm.m_decl_env, thm_decl);
}
};
void parser::add_delayed_theorem(delayed_theorem del_thm) {
del_thm.m_imported = false;
del_thm.m_cert_decl = get_global_task_queue().submit<proof_checking_task>(del_thm, m_last_cmd_pos);
if (m_stop_at) {
// TODO(gabriel): check whether the theorem covers the line we stop at
del_thm.m_proof.get();
}
m_delayed_thms.insert(del_thm.m_ax_decl.get_name(), del_thm);
}
bool parse_commands(environment & env, io_state & ios, char const * fname, optional<std::string> const & base_dir,
bool use_exceptions, unsigned num_threads) {
st_task_queue tq;

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

@ -53,19 +53,10 @@ struct parser_scope {
};
typedef list<parser_scope> parser_scope_stack;
struct delayed_theorem {
bool m_imported;
environment m_decl_env;
declaration m_ax_decl;
task_result<expr> m_proof;
task_result<certified_declaration> m_cert_decl;
};
/** \brief Snapshot of the state of the Lean parser */
struct snapshot {
environment m_env;
name_set m_sub_buckets;
name_map<delayed_theorem> m_delayed_thms;
local_level_decls m_lds;
local_expr_decls m_eds;
name_set m_lvars; // subset of m_lds that is tagged as level variable
@ -75,11 +66,11 @@ struct snapshot {
bool m_imports_parsed;
parser_scope_stack m_parser_scope_stack;
pos_info m_pos;
snapshot(environment const & env, name_set const & sub_buckets, name_map<delayed_theorem> delayed_thms, local_level_decls const & lds,
snapshot(environment const & env, name_set const & sub_buckets, local_level_decls const & lds,
local_expr_decls const & eds, name_set const & lvars, name_set const & vars,
name_set const & includes, options const & opts, bool imports_parsed, parser_scope_stack const & pss,
pos_info const & pos):
m_env(env), m_sub_buckets(sub_buckets), m_delayed_thms(delayed_thms), m_lds(lds), m_eds(eds), m_lvars(lvars), m_vars(vars), m_include_vars(includes),
m_env(env), m_sub_buckets(sub_buckets), m_lds(lds), m_eds(eds), m_lvars(lvars), m_vars(vars), m_include_vars(includes),
m_options(opts), m_imports_parsed(imports_parsed), m_parser_scope_stack(pss), m_pos(pos) {}
};
@ -157,9 +148,6 @@ class parser : public abstract_parser {
// Docgen
optional<std::string> m_doc_string;
// delayed theorems
name_map<delayed_theorem> m_delayed_thms;
void throw_parser_exception(char const * msg, pos_info p);
void throw_nested_exception(throwable const & ex, pos_info p);
@ -253,9 +241,6 @@ public:
environment const & env() const { return m_env; }
io_state const & ios() const { return m_ios; }
name_map<delayed_theorem> get_delayed_theorems() const { return m_delayed_thms; }
void add_delayed_theorem(delayed_theorem);
message_builder mk_message(pos_info const & p, message_severity severity);
message_builder mk_message(message_severity severity);
@ -286,10 +271,6 @@ public:
expr mk_app(expr fn, buffer<expr> const & args, pos_info const & p);
expr mk_app(std::initializer_list<expr> const & args, pos_info const & p);
bool is_delayed_theorem(name const &);
environment reveal_theorems(buffer<name> const & ds);
environment reveal_all_theorems();
/** \brief Read the next token. */
void scan();
/** \brief Return the current token */

12
src/frontends/lean/print_cmd.cpp
View file

@ -72,7 +72,7 @@ struct print_axioms_deps {
static void print_axioms(parser & p, message_builder & out) {
if (p.curr_is_identifier()) {
name c = p.check_constant_next("invalid 'print axioms', constant expected");
auto env = p.reveal_all_theorems(); // FIXME
auto env = p.env();
type_context tc(env, p.get_options());
auto new_out = io_state_stream(env, p.ios(), tc, out.get_text_stream().get_channel());
print_axioms_deps(env, new_out)(c);
@ -80,7 +80,7 @@ static void print_axioms(parser & p, message_builder & out) {
bool has_axioms = false;
p.env().for_each_declaration([&](declaration const & d) {
name const & n = d.get_name();
if (!d.is_definition() && !p.env().is_builtin(n) && d.is_trusted() && !p.is_delayed_theorem(n)) {
if (!d.is_definition() && !p.env().is_builtin(n) && d.is_trusted()) {
out << n << " : " << d.get_type() << endl;
has_axioms = true;
}
@ -216,7 +216,7 @@ static void print_definition(environment const & env, message_builder & out, nam
declaration d = env.get(n);
if (d.is_axiom())
throw parser_error(sstream() << "invalid 'print definition', theorem '" << to_user_name(env, n)
<< "' is not available (suggestion: use command 'reveal " << to_user_name(env, n) << "')", pos);
<< "' is not available", pos);
if (!d.is_definition())
throw parser_error(sstream() << "invalid 'print definition', '" << to_user_name(env, n) << "' is not a definition", pos);
options opts = out.get_text_stream().get_options();
@ -357,12 +357,6 @@ bool print_id_info(parser & p, message_builder & out, name const & id, bool show
print_constant(p, out, "eliminator", d);
} else if (is_quotient_decl(env, c)) {
print_constant(p, out, "builtin-quotient-type-constant", d);
} else if (d.is_axiom() && p.is_delayed_theorem(c)) {
buffer<name> ns; ns.push_back(c);
auto revealed_env = p.reveal_theorems(ns);
print_constant(p, out, "[delayed] theorem", revealed_env.get(c), show_value);
if (show_value)
print_definition(revealed_env, out, c, pos);
} else if (d.is_axiom()) {
print_constant(p, out, "axiom", d);
} else {

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

@ -99,7 +99,7 @@ void init_token_table(token_table & t) {
{"renaming", 0}, {"extends", 0}, {nullptr, 0}};
char const * commands[] =
{"theorem", "axiom", "axioms", "variable", "protected", "private", "reveal",
{"theorem", "axiom", "axioms", "variable", "protected", "private",
"definition", "meta", "mutual", "example", "coercion", "noncomputable",
"variables", "parameter", "parameters", "constant", "constants",
"evaluate", "check", "eval", "vm_eval", "using_well_founded", "[whnf]",

23
src/kernel/declaration.cpp
View file

@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <util/task_queue.h>
#include "kernel/declaration.h"
#include "kernel/environment.h"
#include "kernel/for_each_fn.h"
@ -48,7 +49,7 @@ declaration::~declaration() { if (m_ptr) m_ptr->dec_ref(); }
declaration & declaration::operator=(declaration const & s) { LEAN_COPY_REF(s); }
declaration & declaration::operator=(declaration && s) { LEAN_MOVE_REF(s); }
bool declaration::is_definition() const { return static_cast<bool>(m_ptr->m_value); }
bool declaration::is_definition() const { return static_cast<bool>(m_ptr->m_value) || static_cast<bool>(m_ptr->m_proof); }
bool declaration::is_constant_assumption() const { return !is_definition(); }
bool declaration::is_axiom() const { return is_constant_assumption() && m_ptr->m_theorem; }
bool declaration::is_theorem() const { return is_definition() && m_ptr->m_theorem; }
@ -59,12 +60,23 @@ level_param_names const & declaration::get_univ_params() const { return m_ptr->m
unsigned declaration::get_num_univ_params() const { return length(get_univ_params()); }
expr const & declaration::get_type() const { return m_ptr->m_type; }
expr const & declaration::get_value() const { lean_assert(is_definition()); return *(m_ptr->m_value); }
task_result<expr> const & declaration::get_value_task() const {
lean_assert(is_definition());
return m_ptr->m_proof;
}
expr const & declaration::get_value() const {
lean_assert(is_definition());
if (m_ptr->m_proof) {
return m_ptr->m_proof.get();
} else {
return *(m_ptr->m_value);
}
}
reducibility_hints const & declaration::get_hints() const { return m_ptr->m_hints; }
declaration mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v,
reducibility_hints const & h, bool trusted) {
return declaration(new declaration::cell(n, params, t, false, v, h, trusted));
return declaration(new declaration::cell(n, params, t, v, h, trusted));
}
static unsigned get_max_height(environment const & env, expr const & v) {
unsigned h = 0;
@ -84,8 +96,11 @@ declaration mk_definition(environment const & env, name const & n, level_param_n
unsigned h = get_max_height(env, v);
return mk_definition(n, params, t, v, reducibility_hints::mk_regular(h+1, use_self_opt), trusted);
}
declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, task_result<expr> const & v) {
return declaration(new declaration::cell(n, params, t, v));
}
declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v) {
return declaration(new declaration::cell(n, params, t, true, v, reducibility_hints::mk_opaque(), true));
return mk_theorem(n, params, t, mk_pure_task_result(v, {}));
}
declaration mk_axiom(name const & n, level_param_names const & params, expr const & t) {
return declaration(new declaration::cell(n, params, t, true, true));

13
src/kernel/declaration.h
View file

@ -9,6 +9,7 @@ Author: Leonardo de Moura
#include <string>
#include <limits>
#include "util/rc.h"
#include "util/task_queue.h"
#include "kernel/expr.h"
namespace lean {
@ -75,6 +76,7 @@ class declaration {
expr m_type;
bool m_theorem;
optional<expr> m_value; // if none, then declaration is actually a postulate
task_result<expr> m_proof;
reducibility_hints m_hints;
/* Definitions are trusted by default, and nested macros are expanded when kernel is instantiated with
trust level 0. When this flag is false, then we do not expand nested macros. We say the
@ -86,10 +88,13 @@ class declaration {
cell(name const & n, level_param_names const & params, expr const & t, bool is_axiom, bool trusted):
m_rc(1), m_name(n), m_params(params), m_type(t), m_theorem(is_axiom),
m_hints(reducibility_hints::mk_opaque()), m_trusted(trusted) {}
cell(name const & n, level_param_names const & params, expr const & t, bool is_thm, expr const & v,
cell(name const & n, level_param_names const & params, expr const & t, expr const & v,
reducibility_hints const & h, bool trusted):
m_rc(1), m_name(n), m_params(params), m_type(t), m_theorem(is_thm),
m_rc(1), m_name(n), m_params(params), m_type(t), m_theorem(false),
m_value(v), m_hints(h), m_trusted(trusted) {}
cell(name const & n, level_param_names const & params, expr const & t, task_result<expr> const & v):
m_rc(1), m_name(n), m_params(params), m_type(t), m_theorem(true),
m_proof(v), m_hints(reducibility_hints::mk_opaque()), m_trusted(true) {}
};
cell * m_ptr;
explicit declaration(cell * ptr);
@ -127,6 +132,7 @@ public:
unsigned get_num_univ_params() const;
expr const & get_type() const;
task_result<expr> const & get_value_task() const;
expr const & get_value() const;
reducibility_hints const & get_hints() const;
@ -135,7 +141,7 @@ public:
reducibility_hints const & hints, bool trusted);
friend declaration mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t,
expr const & v, bool use_conv_opt, bool trusted);
friend declaration mk_theorem(name const &, level_param_names const &, expr const &, expr const &);
friend declaration mk_theorem(name const &, level_param_names const &, expr const &, task_result<expr> const &);
friend declaration mk_axiom(name const & n, level_param_names const & params, expr const & t);
friend declaration mk_constant_assumption(name const & n, level_param_names const & params, expr const & t, bool trusted);
};
@ -149,6 +155,7 @@ declaration mk_definition(name const & n, level_param_names const & params, expr
declaration mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t, expr const & v,
bool use_conv_opt = true, bool trusted = true);
declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v);
declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, task_result<expr> const & v);
declaration mk_axiom(name const & n, level_param_names const & params, expr const & t);
declaration mk_constant_assumption(name const & n, level_param_names const & params, expr const & t, bool trusted = true);

62
src/kernel/type_checker.cpp
View file

@ -6,6 +6,8 @@ Author: Leonardo de Moura
*/
#include <utility>
#include <vector>
#include <util/task_queue.h>
#include <library/module_mgr.h>
#include "util/interrupt.h"
#include "util/lbool.h"
#include "util/flet.h"
@ -745,7 +747,7 @@ static void check_duplicated_params(environment const & env, declaration const &
}
}
certified_declaration check(environment const & env, declaration const & d) {
static void check_core(environment const & env, declaration const & d) {
if (d.is_definition())
check_no_mlocal(env, d.get_name(), d.get_value(), false);
check_no_mlocal(env, d.get_name(), d.get_type(), true);
@ -759,8 +761,66 @@ certified_declaration check(environment const & env, declaration const & d) {
expr val_type = checker.check(d.get_value(), d.get_univ_params());
if (!checker.is_def_eq(val_type, d.get_type())) {
throw_kernel_exception(env, d.get_value(), [=](formatter const & fmt) {
return pp_def_type_mismatch(fmt, d.get_name(), d.get_type(), val_type, true);
});
}
}
}
class proof_checking_task : public module_task<expr> {
environment m_env;
declaration m_decl;
public:
proof_checking_task(environment const & env, declaration const & d) :
module_task({}, task_kind::elab), m_env(env), m_decl(d) {
lean_assert(d.is_theorem());
}
void description(std::ostream & out) const override {
out << "type-checking " << m_decl.get_name();
}
std::vector<generic_task_result> get_dependencies() override {
return { m_decl.get_value_task() };
}
expr execute_core() override {
// TODO(gabriel): noncomputable check
bool memoize = true;
bool trusted_only = m_decl.is_trusted();
type_checker checker(m_env, memoize, trusted_only);
expr val_type = checker.check(m_decl.get_value(), m_decl.get_univ_params());
if (!checker.is_def_eq(val_type, m_decl.get_type())) {
throw_kernel_exception(m_env, m_decl.get_value(), [=](formatter const &fmt) {
return pp_def_type_mismatch(fmt, m_decl.get_name(), m_decl.get_type(), val_type, true);
});
}
return m_decl.get_value();
}
};
certified_declaration check(environment const & env, declaration const & d) {
if (d.is_definition())
check_no_mlocal(env, d.get_name(), d.get_value(), false);
check_no_mlocal(env, d.get_name(), d.get_type(), true);
check_name(env, d.get_name());
check_duplicated_params(env, d);
bool memoize = true; bool trusted_only = d.is_trusted();
type_checker checker(env, memoize, trusted_only);
expr sort = checker.check(d.get_type(), d.get_univ_params());
checker.ensure_sort(sort, d.get_type());
if (d.is_definition()) {
if (env.trust_lvl() != 0 && d.is_theorem()) {
auto checked_proof = get_global_task_queue().submit<proof_checking_task>(env, d);
return certified_declaration(env.get_id(),
mk_theorem(d.get_name(), d.get_univ_params(), d.get_type(), checked_proof));
} else {
expr val_type = checker.check(d.get_value(), d.get_univ_params());
if (!checker.is_def_eq(val_type, d.get_type())) {
throw_kernel_exception(env, d.get_value(), [=](formatter const &fmt) {
return pp_def_type_mismatch(fmt, d.get_name(), d.get_type(), val_type, true);
});
}
}
}
return certified_declaration(env.get_id(), d);

100
src/library/module.cpp
View file

@ -182,6 +182,19 @@ deserializer & operator>>(deserializer & d, module_name & r) {
return d;
}
LEAN_THREAD_PTR(std::vector<task_result<expr>>, g_export_delayed_proofs);
class scoped_delayed_proofs {
std::vector<task_result<expr>> * m_old;
public:
scoped_delayed_proofs(std::vector<task_result<expr>> & r) {
m_old = g_export_delayed_proofs;
g_export_delayed_proofs = &r;
}
~scoped_delayed_proofs() {
g_export_delayed_proofs = m_old;
}
};
void export_module(std::ostream & out, environment const & env) {
module_ext const & ext = get_extension(env);
@ -219,6 +232,13 @@ void export_module(std::ostream & out, environment const & env) {
s2.write_char(r[i]);
}
std::vector<task_result<expr>> export_module_delayed(std::ostream & out, environment const & env) {
std::vector<task_result<expr>> delayed_proofs;
scoped_delayed_proofs _(delayed_proofs);
export_module(out, env);
return delayed_proofs;
}
typedef std::unordered_map<std::string, module_object_reader> object_readers;
static object_readers * g_object_readers = nullptr;
static object_readers & get_object_readers() { return *g_object_readers; }
@ -262,10 +282,21 @@ environment update_module_defs(environment const & env, declaration const & d) {
}
}
static declaration theorem2axiom(declaration const & decl) {
lean_assert(decl.is_theorem());
return mk_axiom(decl.get_name(), decl.get_univ_params(), decl.get_type());
}
static environment export_decl(environment const & env, declaration const & d) {
name n = d.get_name();
return add(env, *g_decl_key, [=](environment const & env, serializer & s) {
s << env.get(n);
auto d = env.get(n);
if (g_export_delayed_proofs && d.is_theorem()) {
s << true << theorem2axiom(d) << static_cast<unsigned>(g_export_delayed_proofs->size());
g_export_delayed_proofs->push_back(d.get_value_task());
} else {
s << false << d;
}
});
}
@ -354,85 +385,45 @@ struct import_helper {
}
};
class theorem_import_task : public module_task<certified_declaration> {
environment m_decl_env;
declaration m_ax_decl;
task_result<expr> m_proof;
public:
theorem_import_task(environment const & decl_env, declaration ax_decl, task_result<expr> const & proof) :
module_task(optional<pos_info>(), task_kind::elab),
m_decl_env(decl_env), m_ax_decl(ax_decl), m_proof(proof) {}
certified_declaration execute_core() override {
auto proof = m_proof.get();
auto decl = mk_theorem(m_ax_decl.get_name(), m_ax_decl.get_univ_params(),
m_ax_decl.get_type(), proof);
return import_helper::certify_or_check(m_decl_env, decl);
}
void description(std::ostream & out) const override {
out << "importing theorem " << m_ax_decl.get_name();
}
bool is_tiny() const override { return m_decl_env.trust_lvl() != 0; }
std::vector<generic_task_result> get_dependencies() override {
return {m_proof};
}
};
static void import_module(environment & env, std::string const & module_file_name, module_name const & ref,
name_map<task_result<certified_declaration>> & del_thms, module_loader const & mod_ldr) {
module_loader const & mod_ldr) {
auto res = mod_ldr(module_file_name, ref);
if (get_extension(env).m_imported.contains(res.m_module_name)) return;
std::istringstream in(res.m_obj_code, std::ios_base::binary);
auto olean = parse_olean(in, res.m_module_name, false);
for (auto & dep : olean.first) {
import_module(env, res.m_module_name, dep, del_thms, mod_ldr);
import_module(env, res.m_module_name, dep, mod_ldr);
}
auto ext = get_extension(env);
ext.m_imported.insert(res.m_module_name);
env = update(env, ext);
import_module(olean.second, res.m_module_name, env);
res.m_delayed_proofs.for_each([&] (name const & n, task_result<expr> const & delayed_proof) {
del_thms.insert(n, get_global_task_queue().submit<theorem_import_task>(
env, env.get(n), delayed_proof));
});
import_module(olean.second, res.m_module_name, env, res.m_delayed_proofs);
}
environment import_module(environment const & env0, std::string const & module_file_name,
module_name const & ref,
name_map<task_result<certified_declaration>> & del_thms,
module_loader const & mod_ldr) {
environment env = env0;
module_ext ext = get_extension(env);
ext.m_direct_imports = cons(ref, ext.m_direct_imports);
env = update(env, ext);
import_module(env, module_file_name, ref, del_thms, mod_ldr);
import_module(env, module_file_name, ref, mod_ldr);
return env;
}
environment import_module(environment const & env, std::string const & current_mod, module_name const & ref,
module_loader const & mod_ldr) {
name_map<task_result<certified_declaration>> del_thms;
return import_module(env, current_mod, ref, del_thms, mod_ldr);
}
static declaration theorem2axiom(declaration const & decl) {
lean_assert(decl.is_theorem());
return mk_axiom(decl.get_name(), decl.get_univ_params(), decl.get_type());
}
static optional<name> import_decl(deserializer & d, environment & env) {
static optional<name> import_decl(deserializer & d, environment & env,
std::vector<task_result<expr>> const & delayed_proofs) {
bool is_delayed; d >> is_delayed;
declaration decl = read_declaration(d);
decl = unfold_untrusted_macros(env, decl);
if (decl.get_name() == get_sorry_name() && has_sorry(env)) {
// TODO(gabriel): not sure why this is here
return optional<name>();
}
if (decl.is_theorem() && false) { // TODO(gabriel): was proof already revealed?
decl = theorem2axiom(decl);
// TODO(gabriel): delay proofs
if (is_delayed) {
unsigned i; d >> i;
auto delayed_proof = delayed_proofs.at(i);
decl = mk_theorem(decl.get_name(), decl.get_univ_params(), decl.get_type(), delayed_proof);
}
env = import_helper::add_unchecked(env, decl);
return optional<name>(decl.get_name());
@ -443,7 +434,8 @@ static void import_universe(deserializer & d, environment & env) {
env = env.add_universe(l);
}
void import_module(std::vector<char> const & olean_code, std::string const & file_name, environment & env) {
void import_module(std::vector<char> const & olean_code, std::string const & file_name, environment & env,
std::vector<task_result<expr>> const & delayed_proofs) {
// TODO(gabriel): update extension
std::string s(olean_code.data(), olean_code.size());
std::istringstream in(s, std::ios_base::binary);
@ -455,7 +447,7 @@ void import_module(std::vector<char> const & olean_code, std::string const & fil
if (k == g_olean_end_file) {
break;
} else if (k == *g_decl_key) {
if (auto decl_name = import_decl(d, env))
if (auto decl_name = import_decl(d, env, delayed_proofs))
env = add_decl_olean(env, *decl_name, file_name);
} else if (k == *g_glvl_key) {
import_universe(d, env);

12
src/library/module.h
View file

@ -30,7 +30,7 @@ struct module_name {
struct loaded_module {
std::string m_module_name;
std::string m_obj_code;
name_map<task_result<expr>> m_delayed_proofs;
std::vector<task_result<expr>> m_delayed_proofs;
};
using module_loader = std::function<loaded_module(std::string const &, module_name const &)>;
module_loader mk_olean_loader();
@ -50,12 +50,6 @@ list<module_name> get_curr_module_imports(environment const & env);
If \c keep_proofs is false, then the proof of the imported theorems is discarded after being
checked. The idea is to save memory.
*/
environment
import_module(environment const & env,
std::string const & current_mod, module_name const & ref,
name_map<task_result<certified_declaration>> & del_thms,
module_loader const & mod_ldr);
environment
import_module(environment const & env,
std::string const & current_mod, module_name const & ref,
@ -74,10 +68,12 @@ environment add_transient_decl_pos_info(environment const & env, name const & de
/** \brief Store/Export module using \c env to the output stream \c out. */
void export_module(std::ostream & out, environment const & env);
std::vector<task_result<expr>> export_module_delayed(std::ostream & out, environment const & env);
std::pair<std::vector<module_name>, std::vector<char>> parse_olean(
std::istream & in, std::string const & file_name, bool check_hash = true);
void import_module(std::vector<char> const & olean_code, std::string const & file_name, environment & env);
void import_module(std::vector<char> const & olean_code, std::string const & file_name, environment & env,
std::vector<task_result<expr>> const & delayed_proofs);
/** \brief A reader for importing data from a stream using deserializer \c d.
There is one way to update the environment being constructed.

26
src/library/module_mgr.cpp
View file

@ -66,16 +66,10 @@ public:
std::get<1>(d).m_relative == import.m_relative) {
auto mod_info = std::get<2>(d);
name_map<task_result<expr>> delayed_thms;
mod_info.m_result.get().m_delayed_theorems.for_each(
[&] (name const & thm_name, delayed_theorem const & del_thm) {
if (!del_thm.m_imported) delayed_thms.insert(thm_name, del_thm.m_proof);
});
return loaded_module {
mod_info.m_mod,
mod_info.m_result.get().m_obj_code,
delayed_thms
mod_info.m_result.get().m_obj_code_delayed_proofs,
};
}
}
@ -96,12 +90,12 @@ public:
{
std::ostringstream obj_code_buf(std::ios_base::binary);
export_module(obj_code_buf, p.env());
mod.m_obj_code_delayed_proofs =
export_module_delayed(obj_code_buf, p.env());
mod.m_obj_code = obj_code_buf.str();
}
mod.m_env = optional<environment>(p.env());
mod.m_delayed_theorems = p.get_delayed_theorems();
mod.m_ok = parsed_ok; // TODO(gabriel): what should this be?
@ -120,11 +114,9 @@ public:
std::vector<generic_task_result> get_dependencies() override {
if (auto res = m_mod.m_result.peek()) {
std::vector<generic_task_result> deps;
res->m_delayed_theorems.for_each(
[&] (name const &, delayed_theorem const & del_thm) {
if (!del_thm.m_imported)
deps.push_back(del_thm.m_cert_decl);
});
res->m_env->for_each_declaration([&] (declaration const & d) {
if (d.is_theorem()) deps.push_back(d.get_value_task());
});
return deps;
} else {
return {m_mod.m_result};
@ -141,12 +133,6 @@ public:
auto res = m_mod.m_result.get();
auto env = *res.m_env;
res.m_delayed_theorems.for_each(
[&] (name const &, delayed_theorem const & del_thm) {
if (!del_thm.m_imported)
env = env.replace(del_thm.m_cert_decl.get());
});
auto olean_fn = olean_of_lean(m_mod.m_mod);
exclusive_file_lock output_lock(olean_fn);
std::ofstream out(olean_fn, std::ios_base::binary);

6
src/library/module_mgr.h
View file

@ -41,9 +41,11 @@ struct module_info {
struct parse_result {
optional<environment> m_env;
name_map<delayed_theorem> m_delayed_theorems;
std::string m_obj_code;
bool m_ok = false;
std::string m_obj_code;
std::vector<task_result<expr>> m_obj_code_delayed_proofs;
snapshot_vector m_snapshots;
};

4
src/util/mt_task_queue.cpp
View file

@ -205,8 +205,10 @@ void mt_task_queue::wait(generic_task_result const & t) {
} else {
m_wake_up_worker.notify_one();
}
t->m_task->m_has_finished.wait(lock);
} else {
t->m_task->m_has_finished.wait(lock);
}
t->m_task->m_has_finished.wait(lock);
}
switch (t->m_state.load()) {
case task_result_state::FAILED: std::rethrow_exception(t->m_ex);

6
src/util/task_queue.h
View file

@ -170,7 +170,7 @@ public:
task_result<T> & operator=(task_result<T> const & t) { LEAN_COPY_REF(t); }
task_result<T> & operator=(task_result<T> && t) { LEAN_MOVE_REF(t); }
T get() const;
T const & get() const;
optional<T> peek() const {
if (m_ptr->m_state.load() == task_result_state::FINISHED) {
@ -219,7 +219,7 @@ public:
}
template <typename T>
T get_result(task_result<T> const & t) {
T const & get_result(task_result<T> const & t) {
wait(t);
lean_assert(t.get_ptr()->m_result);
return *t.get_ptr()->m_result;
@ -243,7 +243,7 @@ public:
task_queue & get_global_task_queue();
template <class T>
T task_result<T>::get() const {
T const & task_result<T>::get() const {
return get_global_task_queue().get_result(*this);
}

1
tests/lean/run/calc_heq_symm.lean
View file

@ -5,5 +5,4 @@ calc d == c : heq.symm H₃
... == a₂ : heq.symm H₁
... = a₁ : eq.symm H₀
reveal tst
print definition tst

1
tests/lean/run/class2.lean
View file

@ -2,5 +2,4 @@ open tactic
theorem H {A B : Type} (H1 : inhabited A) : inhabited (Prop × A × (B → num))
:= by apply_instance
reveal H
print H

1
tests/lean/run/class3.lean
View file

@ -10,5 +10,4 @@ section
end
reveal tst
print tst