diff --git a/src/init/init.cpp b/src/init/init.cpp index 3e69bde31..2b5eb9510 100644 --- a/src/init/init.cpp +++ b/src/init/init.cpp @@ -34,8 +34,8 @@ void initialize() { initialize_hits_module(); init_default_print_fn(); initialize_library_module(); - initialize_simplifier_module(); initialize_tactic_module(); + initialize_simplifier_module(); initialize_definitional_module(); initialize_frontend_lean_module(); register_modules(); @@ -44,8 +44,8 @@ void finalize() { run_thread_finalizers(); finalize_frontend_lean_module(); finalize_definitional_module(); - finalize_tactic_module(); finalize_simplifier_module(); + finalize_tactic_module(); finalize_library_module(); finalize_hits_module(); finalize_quotient_module(); diff --git a/src/library/simplifier/init_module.cpp b/src/library/simplifier/init_module.cpp index 3c4397154..d4e530c00 100644 --- a/src/library/simplifier/init_module.cpp +++ b/src/library/simplifier/init_module.cpp @@ -5,12 +5,15 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "library/simplifier/rewrite_rule_set.h" +#include "library/simplifier/simp_tactic.h" namespace lean { void initialize_simplifier_module() { initialize_rewrite_rule_set(); + initialize_simp_tactic(); } void finalize_simplifier_module() { + finalize_simp_tactic(); finalize_rewrite_rule_set(); } } diff --git a/src/library/simplifier/simp_tactic.cpp b/src/library/simplifier/simp_tactic.cpp index 960c0f53f..fa52f9aaa 100644 --- a/src/library/simplifier/simp_tactic.cpp +++ b/src/library/simplifier/simp_tactic.cpp @@ -5,13 +5,118 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "library/constants.h" +#include "library/util.h" +#include "library/tactic/expr_to_tactic.h" +#include "library/tactic/relation_tactics.h" #include "library/simplifier/simp_tactic.h" namespace lean { -expr mk_simp_tactic_expr(buffer const & /* ls */, buffer const & /* ns */, - buffer const & /* ex */, optional const & /* pre_tac */, - location const & /* loc */) { - // TODO(Leo) - return mk_constant(get_tactic_fail_name()); +expr const * g_simp_tactic = nullptr; + +expr mk_simp_tactic_expr(buffer const & ls, buffer const & ns, + buffer const & ex, optional const & pre_tac, + location const & loc) { + expr e = mk_expr_list(ls.size(), ls.data()); + expr n = ids_to_tactic_expr(ns); + expr x = ids_to_tactic_expr(ex); + expr t; + if (pre_tac) { + t = mk_app(mk_constant(get_option_some_name()), *pre_tac); + } else { + + t = mk_constant(get_option_none_name()); + } + expr l = mk_location_expr(loc); + expr r = mk_app({*g_simp_tactic, e, n, x, t, l}); + return r; +} + +class simp_tactic_fn { + environment m_env; + io_state m_ios; + name_generator m_ngen; + optional m_tactic; + +public: + simp_tactic_fn(environment const & env, io_state const & ios, name_generator && ngen, + buffer const & /* ls */, buffer const & /* ns */, buffer const & /* ex */, + optional const & tac):m_env(env), m_ios(ios), m_ngen(ngen), m_tactic(tac) { + } + + pair operator()(goal const & g, location const & /* loc */, substitution const & s) { + // TODO(Leo) + return mk_pair(g, s); + } +}; + +tactic mk_simp_tactic(elaborate_fn const & elab, buffer const & ls, buffer const & ns, + buffer const & ex, optional tac, location const & loc) { + return tactic([=](environment const & env, io_state const & ios, proof_state const & s) { + goals const & gs = s.get_goals(); + if (empty(gs)) { + throw_no_goal_if_enabled(s); + return proof_state_seq(); + } + goal const & g = head(gs); + name_generator new_ngen = s.get_ngen(); + substitution new_subst = s.get_subst(); + buffer new_ls; + for (expr const & l : ls) { + expr new_l; constraints cs; + bool report_unassigned = true; + std::tie(new_l, new_subst, cs) = elab(g, new_ngen.mk_child(), l, none_expr(), new_subst, report_unassigned); + if (cs) + throw_tactic_exception_if_enabled(s, "invalid 'simp' tactic, fail to resolve generated constraints"); + new_ls.push_back(new_l); + } + simp_tactic_fn simp(env, ios, new_ngen.mk_child(), new_ls, ns, ex, tac); + pair r = simp(g, loc, new_subst); + goal new_g = r.first; + new_subst = r.second; + proof_state new_s(s, cons(new_g, tail(gs)), new_subst, new_ngen); + + bool fail_if_metavars = true; + tactic post_tac = try_tactic(refl_tactic(elab, fail_if_metavars)); + // TODO(Leo): remove now_tactic + post_tac = then(post_tac, now_tactic()); + return post_tac(env, ios, new_s); + }); +} + +void initialize_simp_tactic() { + name simp_name{"tactic", "simp_tac"}; + g_simp_tactic = new expr(mk_constant(simp_name)); + + register_tac(simp_name, + [](type_checker & tc, elaborate_fn const & elab, expr const & e, pos_info_provider const * p) { + buffer args; + get_app_args(e, args); + if (args.size() != 5) + throw expr_to_tactic_exception(e, "invalid 'simp' tactic, incorrect number of arguments"); + buffer lemmas; + get_tactic_expr_list_elements(args[0], lemmas, "invalid 'simp' tactic, invalid argument #1"); + buffer ns, ex; + get_tactic_id_list_elements(args[1], ns, "invalid 'simp' tactic, invalid argument #2"); + get_tactic_id_list_elements(args[2], ex, "invalid 'simp' tactic, invalid argument #3"); + optional tac; + expr A, t; + if (is_some(args[3], A, t)) { + tac = expr_to_tactic(tc, elab, t, p); + } else if (is_none(args[3], A)) { + // do nothing + } else { + throw expr_to_tactic_exception(e, "invalid 'simp' tactic, invalid argument #4"); + } + check_tactic_expr(args[4], "invalid 'simp' tactic, invalid argument #5"); + expr loc_expr = get_tactic_expr_expr(args[4]); + if (!is_location_expr(loc_expr)) + throw expr_to_tactic_exception(e, "invalid 'simp' tactic, invalid argument #5"); + location loc = get_location_expr_location(loc_expr); + return mk_simp_tactic(elab, lemmas, ns, ex, tac, loc); + }); +} + +void finalize_simp_tactic() { + delete g_simp_tactic; } } diff --git a/src/library/simplifier/simp_tactic.h b/src/library/simplifier/simp_tactic.h index 16d3478c3..1b8de320d 100644 --- a/src/library/simplifier/simp_tactic.h +++ b/src/library/simplifier/simp_tactic.h @@ -18,4 +18,7 @@ namespace lean { */ expr mk_simp_tactic_expr(buffer const & ls, buffer const & ns, buffer const & ex, optional const & pre_tac, location const & loc); + +void initialize_simp_tactic(); +void finalize_simp_tactic(); } diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/tactic/expr_to_tactic.cpp index a056316ed..c8dd99ff0 100644 --- a/src/library/tactic/expr_to_tactic.cpp +++ b/src/library/tactic/expr_to_tactic.cpp @@ -14,6 +14,7 @@ Author: Leonardo de Moura #include "library/annotation.h" #include "library/string.h" #include "library/explicit.h" +#include "library/placeholder.h" #include "library/num.h" #include "library/constants.h" #include "library/projection.h" @@ -148,6 +149,14 @@ expr mk_expr_list(unsigned num, expr const * args) { return r; } +expr ids_to_tactic_expr(buffer const & args) { + buffer es; + for (name const & id : args) { + es.push_back(mk_local(id, mk_expr_placeholder())); + } + return mk_expr_list(es.size(), es.data()); +} + void get_tactic_expr_list_elements(expr l, buffer & r, char const * error_msg) { while (true) { if (l == *g_expr_list_nil) diff --git a/src/library/tactic/location.cpp b/src/library/tactic/location.cpp index 70b2abbd5..88a48a8c0 100644 --- a/src/library/tactic/location.cpp +++ b/src/library/tactic/location.cpp @@ -154,15 +154,17 @@ public: location const & get_info() const { return m_info; } }; -expr mk_location_expr(location const & loc) { - macro_definition def(new location_macro_cell(loc)); - return mk_macro(def); -} - bool is_location_expr(expr const & e) { return is_macro(e) && macro_def(e).get_name() == *g_location_name; } +expr mk_location_expr(location const & loc) { + macro_definition def(new location_macro_cell(loc)); + expr r = mk_macro(def); + lean_assert(is_location_expr(r)); + return r; +} + location const & get_location_expr_location(expr const & e) { lean_assert(is_location_expr(e)); return static_cast(macro_def(e).raw())->get_info(); diff --git a/src/library/tactic/unfold_rec.cpp b/src/library/tactic/unfold_rec.cpp index f082ca2fd..74a89f375 100644 --- a/src/library/tactic/unfold_rec.cpp +++ b/src/library/tactic/unfold_rec.cpp @@ -299,7 +299,7 @@ class unfold_rec_fn : public replace_visitor_aux { return unfold_simple(fn, args); } name rec_name; - unsigned main_pos; + unsigned main_pos = 0; buffer indices_pos; buffer rec_arg_pos; rec_kind k = get_rec_kind(fn_body, fn_locals, rec_name, indices_pos, main_pos, rec_arg_pos); diff --git a/src/library/util.cpp b/src/library/util.cpp index ab9441f22..7898ee6c0 100644 --- a/src/library/util.cpp +++ b/src/library/util.cpp @@ -712,6 +712,29 @@ expr mk_sigma_mk(type_checker & tc, buffer const & ts, buffer const return mk_sigma_mk(tc, ts.size(), ts.data(), as.data(), cs); } +bool is_none(expr const & e, expr & A) { + buffer args; + expr const & fn = get_app_args(e, args); + if (is_constant(fn) && const_name(fn) == get_option_none_name() && args.size() == 1) { + A = args[0]; + return true; + } else { + return false; + } +} + +bool is_some(expr const & e, expr & A, expr & a) { + buffer args; + expr const & fn = get_app_args(e, args); + if (is_constant(fn) && const_name(fn) == get_option_some_name() && args.size() == 2) { + A = args[0]; + a = args[1]; + return true; + } else { + return false; + } +} + expr infer_implicit_params(expr const & type, unsigned nparams, implicit_infer_kind k) { switch (k) { case implicit_infer_kind::Implicit: { diff --git a/src/library/util.h b/src/library/util.h index 07b8aacdf..a0f315112 100644 --- a/src/library/util.h +++ b/src/library/util.h @@ -197,6 +197,11 @@ level mk_max(levels const & ls); expr mk_sigma_mk(type_checker & tc, buffer const & ts, buffer const & as, constraint_seq & cs); +/** \brief Return true iff \c e is of the form (@option.none A), and update \c A */ +bool is_none(expr const & e, expr & A); +/** \brief Return true iff \c e is of the form (@option.some A a), and update \c A and \c a */ +bool is_some(expr const & e, expr & A, expr & a); + enum class implicit_infer_kind { Implicit, RelaxedImplicit, None }; /** \brief Infer implicit parameter annotations for the first \c nparams using mode