diff --git a/src/library/blast/CMakeLists.txt b/src/library/blast/CMakeLists.txt index 772ceeeba0..79e80259c1 100644 --- a/src/library/blast/CMakeLists.txt +++ b/src/library/blast/CMakeLists.txt @@ -1,3 +1,4 @@ add_library(blast OBJECT expr.cpp state.cpp blast.cpp blast_tactic.cpp init_module.cpp simplifier.cpp simple_actions.cpp intros.cpp proof_expr.cpp - options.cpp choice_point.cpp simple_strategy.cpp backward.cpp util.cpp) + options.cpp choice_point.cpp simple_strategy.cpp backward.cpp util.cpp + gexpr.cpp) diff --git a/src/library/blast/backward.cpp b/src/library/blast/backward.cpp index d21f48082b..7d8328efe6 100644 --- a/src/library/blast/backward.cpp +++ b/src/library/blast/backward.cpp @@ -9,6 +9,7 @@ Author: Leonardo de Moura #include "library/blast/blast.h" #include "library/blast/proof_expr.h" #include "library/blast/choice_point.h" +#include "library/blast/gexpr.h" namespace lean { namespace blast { @@ -46,16 +47,10 @@ struct backward_proof_step_cell : public proof_step_cell { } }; -static action_result try_lemma(name const & fname, bool prop_only_branches) { +static action_result try_lemma(gexpr const & e, bool prop_only_branches) { state & s = curr_state(); - declaration const & fdecl = env().get(fname); - buffer ls_buffer; - unsigned num_univ_ps = fdecl.get_num_univ_params(); - for (unsigned i = 0; i < num_univ_ps; i++) - ls_buffer.push_back(mk_fresh_uref()); - levels ls = to_list(ls_buffer.begin(), ls_buffer.end()); - expr f = mk_constant(fname, ls); - expr type = instantiate_type_univ_params(fdecl, ls); + expr f = e.to_expr(); + expr type = infer_type(f); expr pr = f; buffer mvars; while (true) { @@ -99,19 +94,19 @@ static action_result try_lemma(name const & fname, bool prop_only_branches) { } class backward_choice_point_cell : public choice_point_cell { - state m_state; - list m_fnames; - bool m_prop_only; + state m_state; + list m_lemmas; + bool m_prop_only; public: - backward_choice_point_cell(state const & s, list const & fnames, bool prop_only): - m_state(s), m_fnames(fnames), m_prop_only(prop_only) {} + backward_choice_point_cell(state const & s, list const & lemmas, bool prop_only): + m_state(s), m_lemmas(lemmas), m_prop_only(prop_only) {} virtual action_result next() { - while (!empty(m_fnames)) { - curr_state() = m_state; - name fname = head(m_fnames); - m_fnames = tail(m_fnames); - action_result r = try_lemma(fname, m_prop_only); + while (!empty(m_lemmas)) { + curr_state() = m_state; + gexpr lemma = head(m_lemmas); + m_lemmas = tail(m_lemmas); + action_result r = try_lemma(lemma, m_prop_only); if (!failed(r)) return r; } @@ -119,9 +114,9 @@ public: } }; -action_result backward_action(list const & fnames, bool prop_only_branches) { +action_result backward_action(list const & lemmas, bool prop_only_branches) { state s = curr_state(); - auto it = fnames; + auto it = lemmas; while (!empty(it)) { action_result r = try_lemma(head(it), prop_only_branches); it = tail(it); @@ -143,6 +138,9 @@ action_result constructor_action(bool prop_only_branches) { return action_result::failed(); buffer c_names; get_intro_rule_names(env(), const_name(I), c_names); - return backward_action(to_list(c_names), prop_only_branches); + buffer lemmas; + for (name c_name : c_names) + lemmas.push_back(gexpr(c_name)); + return backward_action(to_list(lemmas), prop_only_branches); } }} diff --git a/src/library/blast/backward.h b/src/library/blast/backward.h index f667c5dcb5..b9bea24349 100644 --- a/src/library/blast/backward.h +++ b/src/library/blast/backward.h @@ -6,9 +6,10 @@ Author: Leonardo de Moura */ #pragma once #include "library/blast/action_result.h" +#include "library/blast/gexpr.h" namespace lean { namespace blast { -action_result backward_action(list const & fnames, bool prop_only_branches = true); +action_result backward_action(list const & lemmas, bool prop_only_branches = true); action_result constructor_action(bool prop_only_branches = true); }} diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp index 6a556e5cad..8b048c55d1 100644 --- a/src/library/blast/blast.cpp +++ b/src/library/blast/blast.cpp @@ -489,6 +489,10 @@ public: app_builder & get_app_builder() { return m_app_builder; } + + type_context & get_type_context() { + return m_tctx; + } }; LEAN_THREAD_PTR(blastenv, g_blastenv); @@ -509,6 +513,11 @@ io_state const & ios() { return g_blastenv->get_ios(); } +type_context & get_type_context() { + lean_assert(g_blastenv); + return g_blastenv->get_type_context(); +} + app_builder & get_app_builder() { lean_assert(g_blastenv); return g_blastenv->get_app_builder(); diff --git a/src/library/blast/blast.h b/src/library/blast/blast.h index 53f0a26d5c..27b3b337af 100644 --- a/src/library/blast/blast.h +++ b/src/library/blast/blast.h @@ -24,6 +24,8 @@ environment const & env(); io_state const & ios(); /** \brief Return reference to blast thread local app_builder */ app_builder & get_app_builder(); +/** \brief Return reference to the main type context used by the blast tactic */ +type_context & get_type_context(); /** \brief Return the thread local current state being processed by the blast tactic. */ state & curr_state(); /** \brief Return a thread local fresh local constant. */ diff --git a/src/library/blast/gexpr.cpp b/src/library/blast/gexpr.cpp new file mode 100644 index 0000000000..ecfa02a907 --- /dev/null +++ b/src/library/blast/gexpr.cpp @@ -0,0 +1,29 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "library/blast/gexpr.h" +#include "library/blast/blast.h" + +namespace lean { +namespace blast { +expr gexpr::to_expr(type_context & ctx) const { + if (m_univ_poly) { + declaration const & fdecl = ctx.env().get(const_name(m_expr)); + buffer ls_buffer; + unsigned num_univ_ps = fdecl.get_num_univ_params(); + for (unsigned i = 0; i < num_univ_ps; i++) + ls_buffer.push_back(ctx.mk_uvar()); + levels ls = to_list(ls_buffer.begin(), ls_buffer.end()); + return mk_constant(const_name(m_expr), ls); + } else { + return m_expr; + } +} + +expr gexpr::to_expr() const { + return to_expr(get_type_context()); +} +}} diff --git a/src/library/blast/gexpr.h b/src/library/blast/gexpr.h new file mode 100644 index 0000000000..bf3be1477c --- /dev/null +++ b/src/library/blast/gexpr.h @@ -0,0 +1,42 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "kernel/expr.h" +#include "library/type_context.h" + +namespace lean { +namespace blast { + +/** \brief Generalized expressions. It is a mechanism for representing + regular expression and universe polymorphic lemmas. + + A universe polymorphic lemma can be converted into a regular expression + by instantiating it with fresh universe meta-variables. + + We use the abstraction to provide a uniform API to some of the actions + available in blast. */ +struct gexpr { + bool m_univ_poly; + expr m_expr; +public: + gexpr(name const & n):m_univ_poly(true), m_expr(mk_constant(n)) {} + gexpr(expr const & e):m_univ_poly(false), m_expr(e) {} + + bool is_universe_polymorphic() const { + return m_univ_poly; + } + + /** \brief Convert generalized expression into a regular expression. + If it is universe polymorphic, we accomplish that by creating + meta-variables using \c ctx. */ + expr to_expr(type_context & ctx) const; + + /** \brief Similar to previous method, but uses \c mk_fresh_uref to + create fresh universe meta-variables */ + expr to_expr() const; +}; +}}