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

chore(kernel,library): remove task from the kernel and library

Browse source
This commit is contained in:
Leonardo de Moura 2018-05-18 08:00:14 -07:00
parent bba55aad47
commit 1bc7c0812c
19 changed files with 31 additions and 296 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
library/init/meta/declaration.lean
View file

@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import init.meta.expr init.meta.name init.meta.task
import init.meta.expr init.meta.name
/--
Reducibility hints are used in the convertibility checker.
@ -48,7 +48,7 @@ meta inductive declaration
/- definition: name, list universe parameters, type, value, is_trusted -/
| defn : name → list name → expr → expr → reducibility_hints → bool → declaration
/- theorem: name, list universe parameters, type, value (remark: theorems are always trusted) -/
| thm : name → list name → expr → task expr → declaration
| thm : name → list name → expr → expr → declaration
/- constant assumption: name, list universe parameters, type, is_trusted -/
| cnst : name → list name → expr → bool → declaration
/- axiom : name → list universe parameters, type (remark: axioms are always trusted) -/
@ -81,13 +81,8 @@ meta def type : declaration → expr
meta def value : declaration → expr
| (defn _ _ _ v _ _) := v
| (thm _ _ _ v) := v.get
| _ := default expr
meta def value_task : declaration → task expr
| (defn _ _ _ v _ _) := task.pure v
| (thm _ _ _ v) := v
| _ := task.pure (default expr)
| _ := default expr
meta def is_trusted : declaration → bool
| (defn _ _ _ _ _ t) := t
@ -108,22 +103,17 @@ meta def update_name : declaration → name → declaration
meta def update_value : declaration → expr → declaration
| (defn n ls t v h tr) new_v := defn n ls t new_v h tr
| (thm n ls t v) new_v := thm n ls t (task.pure new_v)
| d new_v := d
meta def update_value_task : declaration → task expr → declaration
| (defn n ls t v h tr) new_v := defn n ls t new_v.get h tr
| (thm n ls t v) new_v := thm n ls t new_v
| d new_v := d
meta def map_value : declaration → (expr → expr) → declaration
| (defn n ls t v h tr) f := defn n ls t (f v) h tr
| (thm n ls t v) f := thm n ls t (task.map f v)
| (thm n ls t v) f := thm n ls t (f v)
| d f := d
meta def to_definition : declaration → declaration
| (cnst n ls t tr) := defn n ls t (default expr) reducibility_hints.abbrev tr
| (ax n ls t) := thm n ls t (task.pure (default expr))
| (ax n ls t) := thm n ls t (default expr)
| d := d
meta def is_definition : declaration → bool

3
library/init/meta/tactic.lean
View file

@ -1272,9 +1272,6 @@ meta def monad_from_pure_bind {m : Type u → Type v}
(bind : Π {α β : Type u}, m α → (α → m β) → m β) : monad m :=
{pure := @pure, bind := @bind}
meta instance : monad task :=
{map := @task.map, bind := @task.bind, pure := @task.pure}
namespace tactic
meta def mk_id_proof (prop : expr) (pr : expr) : expr :=
expr.app (expr.app (expr.const ``id [level.zero]) prop) pr

20
library/init/meta/task.lean
View file

@ -1,20 +0,0 @@
prelude
import init.core
meta constant {u} task : Type u → Type u
namespace task
meta constant {u} get {α : Type u} (t : task α) : α
protected meta constant {u} pure {α : Type u} (t : α) : task α
protected meta constant {u v} map {α : Type u} {β : Type v} (f : α → β) (t : task α) : task β
protected meta constant {u} flatten {α : Type u} : task (task α) → task α
protected meta def {u v} bind {α : Type u} {β : Type v} (t : task α) (f : α → task β) : task β :=
task.flatten (task.map f t)
@[inline]
meta def {u} delay {α : Type u} (f : unit → α) : task α :=
task.map f (task.pure ())
end task

2
src/checker/text_import.cpp
View file

@ -74,7 +74,7 @@ struct text_importer {
mk_theorem(m_name.at(name_idx), ls, m_expr.at(type_idx), m_expr.at(val_idx)) :
mk_definition(m_env, m_name.at(name_idx), ls, m_expr.at(type_idx), m_expr.at(val_idx), true, true);
m_env = m_env.add(check(m_env, decl, true));
m_env = m_env.add(check(m_env, decl));
}
void handle_ax(std::istream & in) {

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

@ -233,7 +233,7 @@ static environment compile_decl(parser & p, environment const & env,
static pair<environment, name>
declare_definition(parser & p, environment const & env, decl_cmd_kind kind, buffer<name> const & lp_names,
name const & c_name, name const & prv_name, expr type, optional<expr> val, task<expr> const & proof, cmd_meta const & meta,
name const & c_name, name const & prv_name, expr type, optional<expr> val, cmd_meta const & meta,
bool is_abbrev, pos_info const & pos) {
name c_real_name;
environment new_env = env;
@ -254,7 +254,6 @@ declare_definition(parser & p, environment const & env, decl_cmd_kind kind, buff
bool use_conv_opt = true;
bool is_trusted = !meta.m_modifiers.m_is_meta;
auto def =
!val ? mk_theorem(c_real_name, to_list(lp_names), type, proof) :
(kind == decl_cmd_kind::Theorem ?
mk_theorem(c_real_name, to_list(lp_names), type, *val) :
(is_abbrev ? mk_definition(c_real_name, to_list(lp_names), type, *val, reducibility_hints::mk_abbreviation(), is_trusted) :
@ -437,7 +436,7 @@ static environment copy_equation_lemmas(environment const & env, buffer<name> co
new_eqn_value = mk_app(mk_constant(eqn_name, eqn_levels), args);
new_eqn_value = locals.mk_lambda(new_eqn_value);
declaration new_decl = mk_theorem(new_eqn_name, lps, new_eqn_type, new_eqn_value);
new_env = module::add(new_env, check(new_env, new_decl, true));
new_env = module::add(new_env, check(new_env, new_decl));
if (is_rfl_lemma(env, eqn_name))
new_env = mark_rfl_lemma(new_env, new_eqn_name);
new_env = add_eqn_lemma(new_env, new_eqn_name);
@ -500,7 +499,7 @@ static environment mutual_definition_cmd_core(parser & p, decl_cmd_kind kind, cm
name c_real_name;
bool is_abbrev = false;
std::tie(env, c_real_name) = declare_definition(p, env, kind, lp_names, c_name, prv_names[i],
curr_type, some_expr(curr), {}, meta, is_abbrev, header_pos);
curr_type, some_expr(curr), meta, is_abbrev, header_pos);
env = add_local_ref(p, env, c_name, c_real_name, lp_names, params);
new_d_names.push_back(c_real_name);
elab.set_env(env);
@ -786,12 +785,10 @@ environment single_definition_cmd_core(parser & p, decl_cmd_kind kind, cmd_meta
auto pos_provider = p.get_parser_pos_provider(header_pos);
bool use_info_manager = get_global_info_manager() != nullptr;
std::string file_name = p.get_file_name();
auto proof = add_library_task(task_builder<expr>([=] {
return elaborate_proof(decl_env, opts, header_pos, new_params_list,
new_fn, val, thm_finfo, is_rfl, type,
mctx, lctx, pos_provider, use_info_manager, file_name);
}), log_tree::ElaborationLevel);
env_n = declare_definition(p, elab.env(), kind, lp_names, c_name, prv_name, type, opt_val, proof, meta, is_abbrev, header_pos);
opt_val = elaborate_proof(decl_env, opts, header_pos, new_params_list,
new_fn, val, thm_finfo, is_rfl, type,
mctx, lctx, pos_provider, use_info_manager, file_name);
env_n = declare_definition(p, elab.env(), kind, lp_names, c_name, prv_name, type, opt_val, meta, is_abbrev, header_pos);
} else if (kind == decl_cmd_kind::Example) {
auto env = p.env();
auto opts = p.get_options();
@ -819,7 +816,7 @@ environment single_definition_cmd_core(parser & p, decl_cmd_kind kind, cmd_meta
val = get_equations_result(val, 0);
}
finalize_definition(elab, new_params, type, val, lp_names, meta.m_modifiers.m_is_meta);
env_n = declare_definition(p, elab.env(), kind, lp_names, c_name, prv_name, type, some_expr(val), {}, meta, is_abbrev, header_pos);
env_n = declare_definition(p, elab.env(), kind, lp_names, c_name, prv_name, type, some_expr(val), meta, is_abbrev, header_pos);
}
time_task _("decl post-processing", p.mk_message(header_pos, INFORMATION), p.get_options(), c_name);
environment new_env = env_n.first;

19
src/kernel/declaration.cpp
View file

@ -7,7 +7,6 @@ Author: Leonardo de Moura
#include "kernel/declaration.h"
#include "kernel/environment.h"
#include "kernel/for_each_fn.h"
#include "util/task_builder.h"
namespace lean {
int compare(reducibility_hints const & h1, reducibility_hints const & h2) {
@ -49,7 +48,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) || static_cast<bool>(m_ptr->m_proof); }
bool declaration::is_definition() const { return static_cast<bool>(m_ptr->m_value); }
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; }
@ -60,17 +59,9 @@ 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; }
task<expr> const & declaration::get_value_task() const {
lean_assert(is_theorem());
return m_ptr->m_proof;
}
expr const & declaration::get_value() const {
lean_assert(is_definition());
if (m_ptr->m_proof) {
return get(m_ptr->m_proof);
} else {
return *(m_ptr->m_value);
}
return *(m_ptr->m_value);
}
reducibility_hints const & declaration::get_hints() const { return m_ptr->m_hints; }
@ -96,12 +87,8 @@ 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<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 mk_axiom(n, params, t);
return mk_theorem(n, params, t, mk_pure_task(v));
return declaration(new declaration::cell(n, params, t, 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));

12
src/kernel/declaration.h
View file

@ -9,7 +9,6 @@ Author: Leonardo de Moura
#include <string>
#include <limits>
#include "util/rc.h"
#include "util/task.h"
#include "kernel/expr.h"
namespace lean {
@ -76,7 +75,6 @@ class declaration {
expr m_type;
bool m_theorem;
optional<expr> m_value; // if none, then declaration is actually a postulate
task<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
@ -92,9 +90,9 @@ class declaration {
reducibility_hints const & h, bool trusted):
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<expr> const & v):
cell(name const & n, level_param_names const & params, expr const & t, 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) {}
m_value(v), m_hints(reducibility_hints::mk_opaque()), m_trusted(true) {}
};
cell * m_ptr;
explicit declaration(cell * ptr);
@ -131,8 +129,6 @@ public:
level_param_names const & get_univ_params() const;
unsigned get_num_univ_params() const;
expr const & get_type() const;
task<expr> const & get_value_task() const;
expr const & get_value() const;
reducibility_hints const & get_hints() const;
@ -141,7 +137,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 &, task<expr> const &);
friend declaration mk_theorem(name const &, level_param_names const &, expr const &, 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);
};
@ -155,7 +151,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<expr> const & v);
declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, 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);

17
src/kernel/environment.cpp
View file

@ -191,21 +191,4 @@ environment environment::update(unsigned id, std::shared_ptr<environment_extensi
void environment::for_each_declaration(std::function<void(declaration const & d)> const & f) const {
m_declarations.for_each([&](name const &, declaration const & d) { return f(d); });
}
task<bool> environment::is_correct() const {
std::vector<gtask> deps;
for_each_declaration([&] (declaration const & d) {
if (d.is_theorem())
deps.push_back(d.get_value_task());
});
auto env = *this;
return task_builder<bool>([env] {
env.for_each_declaration([&] (declaration const & d) {
if (d.is_definition()) d.get_value();
});
return true;
}).depends_on(std::move(deps)).build();
}
}

5
src/kernel/environment.h
View file

@ -188,9 +188,6 @@ public:
friend bool is_decl_eqp(environment const & e1, environment const & e2) {
return is_eqp(e1.m_declarations, e2.m_declarations);
}
/** \brief Returns a task that returns true iff all proofs are correct. May throw an exception otherwise. */
task<bool> is_correct() const;
};
void initialize_environment();
@ -204,7 +201,7 @@ class name_generator;
*/
class certified_declaration {
friend class certify_unchecked;
friend certified_declaration check(environment const & env, declaration const & d, bool immediately);
friend certified_declaration check(environment const & env, declaration const & d);
environment_id m_id;
declaration m_declaration;
certified_declaration(environment_id const & id, declaration const & d):m_id(id), m_declaration(d) {}

14
src/kernel/type_checker.cpp
View file

@ -756,7 +756,7 @@ static void check_definition(environment const & env, declaration const & d, typ
}
}
certified_declaration check(environment const & env, declaration const & d, bool immediately) {
certified_declaration check(environment const & env, declaration const & d) {
check_no_mlocal(env, d.get_name(), d.get_type(), true);
check_name(env, d.get_name());
check_duplicated_params(env, d);
@ -765,18 +765,6 @@ certified_declaration check(environment const & env, declaration const & d, bool
expr sort = checker.check(d.get_type(), d.get_univ_params());
checker.ensure_sort(sort, d.get_type());
if (d.is_definition()) {
if (!immediately && env.trust_lvl() != 0 && d.is_theorem()) {
// TODO(gabriel): cancellation
auto checked_proof =
map<expr>(d.get_value_task(),
[d, env, memoize, trusted_only] (expr const & val) -> expr {
type_checker checker(env, memoize, trusted_only);
check_definition(env, d, checker);
return val;
}).build();
return certified_declaration(env.get_id(),
mk_theorem(d.get_name(), d.get_univ_params(), d.get_type(), checked_proof));
}
check_definition(env, d, checker);
}
return certified_declaration(env.get_id(), d);

2
src/kernel/type_checker.h
View file

@ -145,7 +145,7 @@ void check_no_mlocal(environment const & env, name const & n, expr const & e, bo
/** \brief Type check the given declaration, and return a certified declaration if it is type correct.
Throw an exception if the declaration is type incorrect. */
certified_declaration check(environment const & env, declaration const & d, bool immediately = false);
certified_declaration check(environment const & env, declaration const & d);
void initialize_type_checker();
void finalize_type_checker();

2
src/library/aux_definition.cpp
View file

@ -177,7 +177,7 @@ struct mk_aux_definition_fn : public closure_helper {
bool use_self_opt = true;
d = mk_definition(env, c, get_norm_level_names(), def_type, def_value, use_self_opt, !untrusted);
}
environment new_env = module::add(env, check(env, d, true));
environment new_env = module::add(env, check(env, d));
buffer<level> ls;
get_level_closure(ls);
buffer<expr> ps;

2
src/library/equations_compiler/unbounded_rec.cpp
View file

@ -161,7 +161,7 @@ eqn_compiler_result unbounded_rec(environment & env, elaborator & elab,
bool use_self_opt = true;
bool trusted = false;
declaration d = mk_definition(env, fn_name, lvl_names, fn_type, fn, use_self_opt, trusted);
env = module::add(env, check(env, d, true));
env = module::add(env, check(env, d));
expr result_fn = mk_app(mk_constant(fn_name, to_list(closure_lvl_params)), closure_params);

53
src/library/module.cpp
View file

@ -348,16 +348,11 @@ struct decl_modification : public modification {
void get_introduced_exprs(std::vector<task<expr>> & es) const override {
es.push_back(mk_pure_task(m_decl.get_type()));
if (m_decl.is_theorem()) {
es.push_back(m_decl.get_value_task());
} else if (m_decl.is_definition()) {
if (m_decl.is_definition())
es.push_back(mk_pure_task(m_decl.get_value()));
}
}
void get_task_dependencies(buffer<gtask> & deps) const override {
if (m_decl.is_theorem())
deps.push_back(m_decl.get_value_task());
void get_task_dependencies(buffer<gtask> &) const override {
}
};
@ -451,21 +446,6 @@ static name sorry_decl_name(name const & n) {
}
struct sorry_warning_tag : public log_entry_cell {};
static bool is_sorry_warning_or_error(log_entry const & e) {
return is_error_message(e) || dynamic_cast<sorry_warning_tag const *>(e.get()) != nullptr;
}
static task<bool> error_already_reported() {
for (auto & e : logtree().get_entries())
if (is_sorry_warning_or_error(e))
return mk_pure_task(true);
std::vector<task<bool>> children;
logtree().get_used_children().for_each([&] (name const &, log_tree::node const & c) {
children.push_back(c.has_entry(is_sorry_warning_or_error));
});
return any(children, [] (bool already_reported) { return already_reported; });
}
environment add(environment const & env, certified_declaration const & d) {
environment new_env = env.add(d);
@ -474,35 +454,6 @@ environment add(environment const & env, certified_declaration const & d) {
new_env = mark_noncomputable(new_env, _d.get_name());
new_env = update_module_defs(new_env, _d);
new_env = add(new_env, std::make_shared<decl_modification>(_d, env.trust_lvl()));
if (_d.is_theorem()) {
// report errors from kernel type-checker
add_library_task(task_builder<unit>([_d, env] {
message_builder msg(env, get_global_ios(),
logtree().get_location().m_file_name, logtree().get_location().m_range.m_begin,
ERROR);
try {
_d.get_value();
} catch (std::exception & ex) {
msg.set_exception(ex).report();
} catch (...) {
msg << "unknown exception while type-checking theorem";
msg.report();
}
return unit();
}).depends_on(_d.is_theorem() ? _d.get_value_task() : nullptr));
}
add_library_task(map<unit>(error_already_reported(), [_d] (bool already_reported) {
if (!already_reported && has_sorry(_d)) {
report_message(message(logtree().get_location().m_file_name,
logtree().get_location().m_range.m_begin, WARNING,
(sstream() << "declaration '" << sorry_decl_name(_d.get_name()) << "' uses sorry").str()));
logtree().add(std::make_shared<sorry_warning_tag>());
}
return unit {};
}).depends_on(_d.is_theorem() ? _d.get_value_task() : nullptr));
return add_decl_pos_info(new_env, _d.get_name());
}

2
src/library/vm/CMakeLists.txt
View file

@ -1,4 +1,4 @@
add_library(vm OBJECT vm.cpp optimize.cpp vm_nat.cpp vm_string.cpp vm_aux.cpp vm_io.cpp vm_name.cpp
vm_options.cpp vm_format.cpp vm_rb_map.cpp vm_level.cpp vm_expr.cpp vm_exceptional.cpp
vm_declaration.cpp vm_environment.cpp vm_list.cpp vm_pexpr.cpp vm_task.cpp
vm_declaration.cpp vm_environment.cpp vm_list.cpp vm_pexpr.cpp
vm_int.cpp init_module.cpp vm_parser.cpp vm_array.cpp vm_pos_info.cpp vm_platform.cpp)

3
src/library/vm/init_module.cpp
View file

@ -20,7 +20,6 @@ Author: Leonardo de Moura
#include "library/vm/vm_exceptional.h"
#include "library/vm/vm_declaration.h"
#include "library/vm/vm_environment.h"
#include "library/vm/vm_task.h"
#include "library/vm/vm_parser.h"
#include "library/vm/vm_array.h"
#include "library/vm/vm_string.h"
@ -42,7 +41,6 @@ void initialize_vm_core_module() {
initialize_vm_pexpr();
initialize_vm_list();
initialize_vm_exceptional();
initialize_vm_task();
initialize_vm_declaration();
initialize_vm_environment();
initialize_vm_parser();
@ -58,7 +56,6 @@ void finalize_vm_core_module() {
finalize_vm_parser();
finalize_vm_environment();
finalize_vm_declaration();
finalize_vm_task();
finalize_vm_exceptional();
finalize_vm_list();
finalize_vm_pexpr();

5
src/library/vm/vm_declaration.cpp
View file

@ -11,7 +11,6 @@ Author: Leonardo de Moura
#include "library/vm/vm_list.h"
#include "library/vm/vm_nat.h"
#include "library/vm/vm_option.h"
#include "library/vm/vm_task.h"
namespace lean {
/*
@ -66,7 +65,7 @@ vm_obj declaration_defn(vm_obj const & n, vm_obj const & ls, vm_obj const & type
}
vm_obj declaration_thm(vm_obj const & n, vm_obj const & ls, vm_obj const & type, vm_obj const & value) {
return to_obj(mk_theorem(to_name(n), to_list_name(ls), to_expr(type), to_expr_task(value)));
return to_obj(mk_theorem(to_name(n), to_list_name(ls), to_expr(type), to_expr(value)));
}
vm_obj declaration_cnst(vm_obj const & n, vm_obj const & ls, vm_obj const & type, vm_obj const & trusted) {
@ -83,7 +82,7 @@ unsigned declaration_cases_on(vm_obj const & o, buffer<vm_obj> & data) {
data.push_back(to_obj(d.get_univ_params()));
data.push_back(to_obj(d.get_type()));
if (d.is_theorem()) {
data.push_back(to_obj(d.get_value_task()));
data.push_back(to_obj(d.get_value()));
return 1;
} else if (d.is_axiom()) {
return 3;

108
src/library/vm/vm_task.cpp
View file

@ -1,108 +0,0 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Gabriel Ebner
*/
#include "library/vm/vm_task.h"
#include <string>
#include <iostream>
#include <vector>
#include "library/trace.h"
#include "library/type_context.h"
#include "frontends/lean/info_manager.h"
#include "frontends/lean/elaborator.h"
#include "library/tactic/elaborate.h"
#include "library/vm/vm.h"
#include "library/vm/vm_string.h"
#include "library/vm/vm_expr.h"
#include "library/library_task_builder.h"
namespace lean {
struct vm_task : public vm_external {
task<ts_vm_obj> m_val;
vm_task(task<ts_vm_obj> const & v) : m_val(v) {}
virtual ~vm_task() {}
virtual void dealloc() override { delete this; }
virtual vm_external * ts_clone(vm_clone_fn const &) override {
return new vm_task(m_val);
}
virtual vm_external * clone(vm_clone_fn const &) override {
lean_unreachable();
}
};
bool is_task(vm_obj const & o) {
return is_external(o) && dynamic_cast<vm_task *>(to_external(o));
}
task<ts_vm_obj> const & to_task(vm_obj const & o) {
lean_vm_check(dynamic_cast<vm_task *>(to_external(o)));
return static_cast<vm_task*>(to_external(o))->m_val;
}
vm_obj to_obj(task<ts_vm_obj> const & n) {
return mk_vm_external(new vm_task(n));
}
vm_obj to_obj(task<expr> const & n) {
return to_obj(map<ts_vm_obj>(n, [] (expr const & e) { return ts_vm_obj(to_obj(e)); }).execute_eagerly().build());
}
task<expr> to_expr_task(vm_obj const & o) {
return map<expr>(to_task(o), [] (ts_vm_obj const & o) { return to_expr(o.to_vm_obj()); }).execute_eagerly().build();
}
vm_obj vm_task_get(vm_obj const &, vm_obj const & t) {
return get(to_task(t)).to_vm_obj();
}
vm_obj vm_task_pure(vm_obj const &, vm_obj const & t) {
return to_obj(mk_pure_task(ts_vm_obj(t)));
}
vm_obj vm_task_map(vm_obj const &, vm_obj const &, vm_obj const & fn, vm_obj const & t) {
auto env = get_vm_state().env();
auto opts = get_vm_state().get_options();
auto has_infom = get_global_info_manager() != nullptr;
auto ts_fn = ts_vm_obj(fn);
return to_obj(add_library_task(map<ts_vm_obj>(to_task(t), [env, opts, has_infom, ts_fn] (ts_vm_obj const & arg) {
auto file_name = logtree().get_location().m_file_name;
// Tracing
type_context_old tc(env);
scope_trace_env scope_trace(env, opts, tc);
scope_traces_as_messages scope_traces_as_msg(file_name, logtree().get_location().m_range.m_begin);
// Info manager
auto_reporting_info_manager_scope scope_infom(file_name, has_infom);
vm_state state(env, opts);
scope_vm_state scope_vm(state);
return ts_vm_obj(state.invoke(ts_fn.to_vm_obj(), arg.to_vm_obj()));
}).wrap(exception_reporter())));
}
vm_obj vm_task_flatten(vm_obj const &, vm_obj const & o) {
auto t = to_task(o);
return to_obj(task_builder<ts_vm_obj>([t] {
return get(to_task(get(t).to_vm_obj()));
}).depends_on_fn([t] (buffer<gtask> & deps) {
deps.push_back(t);
if (auto res = peek(t))
deps.push_back(to_task(res->to_vm_obj()));
}).execute_eagerly().build());
}
void initialize_vm_task() {
DECLARE_VM_BUILTIN(name({"task", "get"}), vm_task_get);
DECLARE_VM_BUILTIN(name({"task", "pure"}), vm_task_pure);
DECLARE_VM_BUILTIN(name({"task", "map"}), vm_task_map);
DECLARE_VM_BUILTIN(name({"task", "flatten"}), vm_task_flatten);
}
void finalize_vm_task() {
}
}

19
src/library/vm/vm_task.h
View file

@ -1,19 +0,0 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Gabriel Ebner
*/
#pragma once
#include "library/vm/vm.h"
namespace lean {
vm_obj to_obj(task<ts_vm_obj> const & n);
vm_obj to_obj(task<expr> const & n);
bool is_task(vm_obj const & o);
task<expr> to_expr_task(vm_obj const & o);
task<ts_vm_obj> const & to_task(vm_obj const & o);
void initialize_vm_task();
void finalize_vm_task();
}