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

refactor(frontends/lean): cleanup add_delayed_theorem method

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-26 14:01:20 -07:00
parent 70ef92cd5e
commit 78a1670905
3 changed files with 13 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -267,18 +267,9 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
if (is_theorem) {
if (p.num_threads() > 1) {
// add as axiom, and create a task to prove the theorem
expr saved_type = type;
expr saved_value = value;
environment saved_env = env;
local_level_decls saved_lls = p.get_local_level_decls();
p.add_delayed_theorem(env, real_n, ls, type, value);
std::tie(type, new_ls) = p.elaborate_type(type);
env = module::add(env, check(env, mk_axiom(real_n, append(ls, new_ls), type)));
p.add_delayed_theorem([=, &p]() {
level_param_names new_ls;
expr type, value;
std::tie(type, value, new_ls) = p.elaborate_definition_at(saved_env, saved_lls, n, saved_type, saved_value);
return check(saved_env, mk_theorem(real_n, append(ls, new_ls), type, value));
});
} else {
std::tie(type, value, new_ls) = p.elaborate_definition(n, type, value);
env = module::add(env, check(env, mk_theorem(real_n, append(ls, new_ls), type, value)));

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

@ -17,6 +17,7 @@ Author: Leonardo de Moura
#include "kernel/replace_fn.h"
#include "kernel/abstract.h"
#include "kernel/instantiate.h"
#include "kernel/type_checker.h"
#include "library/parser_nested_exception.h"
#include "library/aliases.h"
#include "library/private.h"
@ -1077,6 +1078,16 @@ bool parser::parse_commands() {
return !m_found_errors;
}
void parser::add_delayed_theorem(environment const & env, name const & n, level_param_names const & ls, expr const & t, expr const & v) {
local_level_decls saved_lls = get_local_level_decls();
m_theorem_queue.add([=]() {
level_param_names new_ls;
expr type, value;
std::tie(type, value, new_ls) = elaborate_definition_at(env, saved_lls, n, t, v);
return check(env, mk_theorem(n, append(ls, new_ls), type, value));
});
}
bool parse_commands(environment & env, io_state & ios, std::istream & in, char const * strm_name, bool use_exceptions,
unsigned num_threads) {
parser p(env, ios, in, strm_name, use_exceptions, num_threads);

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

@ -162,7 +162,7 @@ public:
expr mk_app(std::initializer_list<expr> const & args, pos_info const & p);
unsigned num_threads() const { return m_num_threads; }
void add_delayed_theorem(std::function<certified_declaration()> const & fn) { m_theorem_queue.add(fn); }
void add_delayed_theorem(environment const & env, name const & n, level_param_names const & ls, expr const & t, expr const & v);
/** \brief Read the next token. */
void scan() { m_curr = m_scanner.scan(m_env); }