From 1bc7c0812c90dc638cceefaf98751146668bf167 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 18 May 2018 08:00:14 -0700 Subject: [PATCH] chore(kernel,library): remove `task` from the kernel and library --- library/init/meta/declaration.lean | 20 +--- library/init/meta/tactic.lean | 3 - library/init/meta/task.lean | 20 ---- src/checker/text_import.cpp | 2 +- src/frontends/lean/definition_cmds.cpp | 19 ++- src/kernel/declaration.cpp | 19 +-- src/kernel/declaration.h | 12 +- src/kernel/environment.cpp | 17 --- src/kernel/environment.h | 5 +- src/kernel/type_checker.cpp | 14 +-- src/kernel/type_checker.h | 2 +- src/library/aux_definition.cpp | 2 +- .../equations_compiler/unbounded_rec.cpp | 2 +- src/library/module.cpp | 53 +-------- src/library/vm/CMakeLists.txt | 2 +- src/library/vm/init_module.cpp | 3 - src/library/vm/vm_declaration.cpp | 5 +- src/library/vm/vm_task.cpp | 108 ------------------ src/library/vm/vm_task.h | 19 --- 19 files changed, 31 insertions(+), 296 deletions(-) delete mode 100644 library/init/meta/task.lean delete mode 100644 src/library/vm/vm_task.cpp delete mode 100644 src/library/vm/vm_task.h diff --git a/library/init/meta/declaration.lean b/library/init/meta/declaration.lean index 22361c54e1..aa76f89c13 100644 --- a/library/init/meta/declaration.lean +++ b/library/init/meta/declaration.lean @@ -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 diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index 84927fc6cc..ef228080f9 100644 --- a/library/init/meta/tactic.lean +++ b/library/init/meta/tactic.lean @@ -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 diff --git a/library/init/meta/task.lean b/library/init/meta/task.lean deleted file mode 100644 index ca553cecc0..0000000000 --- a/library/init/meta/task.lean +++ /dev/null @@ -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 diff --git a/src/checker/text_import.cpp b/src/checker/text_import.cpp index efb17dac2b..689a93c125 100644 --- a/src/checker/text_import.cpp +++ b/src/checker/text_import.cpp @@ -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) { diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp index e6ad243951..259a28f21f 100644 --- a/src/frontends/lean/definition_cmds.cpp +++ b/src/frontends/lean/definition_cmds.cpp @@ -233,7 +233,7 @@ static environment compile_decl(parser & p, environment const & env, static pair declare_definition(parser & p, environment const & env, decl_cmd_kind kind, buffer const & lp_names, - name const & c_name, name const & prv_name, expr type, optional val, task const & proof, cmd_meta const & meta, + name const & c_name, name const & prv_name, expr type, optional 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 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([=] { - 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; diff --git a/src/kernel/declaration.cpp b/src/kernel/declaration.cpp index 3418bf424c..28c8b09e10 100644 --- a/src/kernel/declaration.cpp +++ b/src/kernel/declaration.cpp @@ -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(m_ptr->m_value) || static_cast(m_ptr->m_proof); } +bool declaration::is_definition() const { return static_cast(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 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 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)); diff --git a/src/kernel/declaration.h b/src/kernel/declaration.h index db12e5468d..861200ffeb 100644 --- a/src/kernel/declaration.h +++ b/src/kernel/declaration.h @@ -9,7 +9,6 @@ Author: Leonardo de Moura #include #include #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 m_value; // if none, then declaration is actually a postulate - task 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 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 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 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 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); diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 4f01d1b370..3deaf7ea46 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -191,21 +191,4 @@ environment environment::update(unsigned id, std::shared_ptr const & f) const { m_declarations.for_each([&](name const &, declaration const & d) { return f(d); }); } - -task environment::is_correct() const { - std::vector deps; - for_each_declaration([&] (declaration const & d) { - if (d.is_theorem()) - deps.push_back(d.get_value_task()); - }); - - auto env = *this; - return task_builder([env] { - env.for_each_declaration([&] (declaration const & d) { - if (d.is_definition()) d.get_value(); - }); - return true; - }).depends_on(std::move(deps)).build(); -} - } diff --git a/src/kernel/environment.h b/src/kernel/environment.h index 04583e909f..bb10a6ca80 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -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 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) {} diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 7c8bfef62d..abc2d21a73 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -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(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); diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h index 5c9c6d5546..cff75574c1 100644 --- a/src/kernel/type_checker.h +++ b/src/kernel/type_checker.h @@ -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(); diff --git a/src/library/aux_definition.cpp b/src/library/aux_definition.cpp index 360d1c7e5c..041c267974 100644 --- a/src/library/aux_definition.cpp +++ b/src/library/aux_definition.cpp @@ -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 ls; get_level_closure(ls); buffer ps; diff --git a/src/library/equations_compiler/unbounded_rec.cpp b/src/library/equations_compiler/unbounded_rec.cpp index 6db15bd9c2..1b7c528aba 100644 --- a/src/library/equations_compiler/unbounded_rec.cpp +++ b/src/library/equations_compiler/unbounded_rec.cpp @@ -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); diff --git a/src/library/module.cpp b/src/library/module.cpp index b477f8c8b3..e3dfce7082 100644 --- a/src/library/module.cpp +++ b/src/library/module.cpp @@ -348,16 +348,11 @@ struct decl_modification : public modification { void get_introduced_exprs(std::vector> & 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 & deps) const override { - if (m_decl.is_theorem()) - deps.push_back(m_decl.get_value_task()); + void get_task_dependencies(buffer &) 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(e.get()) != nullptr; -} - -static task error_already_reported() { - for (auto & e : logtree().get_entries()) - if (is_sorry_warning_or_error(e)) - return mk_pure_task(true); - - std::vector> 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(_d, env.trust_lvl())); - - if (_d.is_theorem()) { - // report errors from kernel type-checker - add_library_task(task_builder([_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(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()); - } - return unit {}; - }).depends_on(_d.is_theorem() ? _d.get_value_task() : nullptr)); - return add_decl_pos_info(new_env, _d.get_name()); } diff --git a/src/library/vm/CMakeLists.txt b/src/library/vm/CMakeLists.txt index d8985a0078..9a44162e4f 100644 --- a/src/library/vm/CMakeLists.txt +++ b/src/library/vm/CMakeLists.txt @@ -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) diff --git a/src/library/vm/init_module.cpp b/src/library/vm/init_module.cpp index 13a87157f1..2e0d8a53aa 100644 --- a/src/library/vm/init_module.cpp +++ b/src/library/vm/init_module.cpp @@ -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(); diff --git a/src/library/vm/vm_declaration.cpp b/src/library/vm/vm_declaration.cpp index 0febcfbe60..d1a02f9c4c 100644 --- a/src/library/vm/vm_declaration.cpp +++ b/src/library/vm/vm_declaration.cpp @@ -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 & 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; diff --git a/src/library/vm/vm_task.cpp b/src/library/vm/vm_task.cpp deleted file mode 100644 index 729b0a1192..0000000000 --- a/src/library/vm/vm_task.cpp +++ /dev/null @@ -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 -#include -#include -#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 m_val; - vm_task(task 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(to_external(o)); -} - -task const & to_task(vm_obj const & o) { - lean_vm_check(dynamic_cast(to_external(o))); - return static_cast(to_external(o))->m_val; -} - -vm_obj to_obj(task const & n) { - return mk_vm_external(new vm_task(n)); -} - -vm_obj to_obj(task const & n) { - return to_obj(map(n, [] (expr const & e) { return ts_vm_obj(to_obj(e)); }).execute_eagerly().build()); -} - -task to_expr_task(vm_obj const & o) { - return map(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(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([t] { - return get(to_task(get(t).to_vm_obj())); - }).depends_on_fn([t] (buffer & 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() { -} - -} diff --git a/src/library/vm/vm_task.h b/src/library/vm/vm_task.h deleted file mode 100644 index 5f8af30a9b..0000000000 --- a/src/library/vm/vm_task.h +++ /dev/null @@ -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 const & n); -vm_obj to_obj(task const & n); -bool is_task(vm_obj const & o); -task to_expr_task(vm_obj const & o); -task const & to_task(vm_obj const & o); - -void initialize_vm_task(); -void finalize_vm_task(); -}