From afc7a2af8450d595af91a7f4ce1190cf6b512675 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 7 Nov 2015 17:42:58 -0800 Subject: [PATCH] feat(library/blast): expose mk_congr_lemma_for_simp and get_fun_info --- src/library/blast/blast.cpp | 46 +++++++++++++++++++++++++++++++++++++ src/library/blast/blast.h | 22 ++++++++++++++++++ 2 files changed, 68 insertions(+) diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp index 7a5ef9e0e..ca50bf29f 100644 --- a/src/library/blast/blast.cpp +++ b/src/library/blast/blast.cpp @@ -14,6 +14,7 @@ Author: Leonardo de Moura #include "library/normalize.h" #include "library/class.h" #include "library/type_context.h" +#include "library/congr_lemma_manager.h" #include "library/projection.h" #include "library/tactic/goal.h" #include "library/blast/expr.h" @@ -29,6 +30,7 @@ static name * g_tmp_prefix = nullptr; class blastenv { friend class scope_assignment; typedef std::vector tmp_type_context_pool; + typedef std::unique_ptr tmp_type_context_ptr; environment m_env; io_state m_ios; @@ -44,6 +46,10 @@ class blastenv { name_map m_projection_info; state m_curr_state; // current state tmp_type_context_pool m_tmp_ctx_pool; + tmp_type_context_ptr m_tmp_ctx; // for app_builder and congr_lemma_manager + app_builder m_app_builder; + fun_info_manager m_fun_info_manager; + congr_lemma_manager m_congr_lemma_manager; class tctx : public type_context { blastenv & m_benv; @@ -366,6 +372,10 @@ public: m_not_reducible_pred(mk_not_reducible_pred(env)), m_class_pred(mk_class_pred(env)), m_instance_pred(mk_instance_pred(env)), + m_tmp_ctx(mk_tmp_type_context()), + m_app_builder(*m_tmp_ctx), + m_fun_info_manager(*m_tmp_ctx), + m_congr_lemma_manager(m_app_builder, m_fun_info_manager), m_tctx(*this) { } @@ -423,6 +433,22 @@ public: m_tmp_ctx_pool.push_back(ctx); } + optional mk_congr_lemma_for_simp(expr const & fn, unsigned num_args) { + return m_congr_lemma_manager.mk_congr_simp(fn, num_args); + } + + optional mk_congr_lemma_for_simp(expr const & fn) { + return m_congr_lemma_manager.mk_congr_simp(fn); + } + + fun_info get_fun_info(expr const & fn) { + return m_fun_info_manager.get(fn); + } + + fun_info get_fun_info(expr const & fn, unsigned nargs) { + return m_fun_info_manager.get(fn, nargs); + } + /** \brief Convert an external expression into a blast expression It converts meta-variables to blast meta-variables, and ensures the expressions are maximally shared. @@ -496,6 +522,26 @@ expr mk_fresh_local(expr const & type, binder_info const & bi) { return g_blastenv->mk_fresh_local(type, bi); } +optional mk_congr_lemma_for_simp(expr const & fn, unsigned num_args) { + lean_assert(g_blastenv); + return g_blastenv->mk_congr_lemma_for_simp(fn, num_args); +} + +optional mk_congr_lemma_for_simp(expr const & fn) { + lean_assert(g_blastenv); + return g_blastenv->mk_congr_lemma_for_simp(fn); +} + +fun_info get_fun_info(expr const & fn) { + lean_assert(g_blastenv); + return g_blastenv->get_fun_info(fn); +} + +fun_info get_fun_info(expr const & fn, unsigned nargs) { + lean_assert(g_blastenv); + return g_blastenv->get_fun_info(fn, nargs); +} + void display_curr_state() { curr_state().display(env(), ios()); display("\n"); diff --git a/src/library/blast/blast.h b/src/library/blast/blast.h index ac14368e9..cc2df029d 100644 --- a/src/library/blast/blast.h +++ b/src/library/blast/blast.h @@ -9,6 +9,8 @@ Author: Leonardo de Moura #include "kernel/environment.h" #include "library/io_state.h" #include "library/tmp_type_context.h" +#include "library/congr_lemma_manager.h" +#include "library/fun_info_manager.h" #include "library/blast/state.h" namespace lean { @@ -48,6 +50,26 @@ bool is_def_eq(expr const & e1, expr const & e2); /** \brief Try to synthesize an element of the given type class with respect to the blast local context. */ optional mk_class_instance(expr const & e); +/** \brief Create a congruence lemma for the given function. + \pre num_args <= arity of fn + \remark The procedure may fail when app_builder used by it fails. + Example: it fail to infer the type of fn. + + \remark The generated lemma is useful when performing rewriting. + For congruence closure, we must use a different lemma generator, or + at least, post-process the lemma generated by this procedure. + + \remark The type \c congr_lemma is defined at library/congr_lemma_manager.h */ +optional mk_congr_lemma_for_simp(expr const & fn, unsigned num_args); +/** \brief Similar to previous procedure, but num_args == arith of fn */ +optional mk_congr_lemma_for_simp(expr const & fn); + +/** \brief Retrieve information for the given function. */ +fun_info get_fun_info(expr const & fn); +/** \brief Retrieve information for the given function. + \pre nargs <= arity fn. */ +fun_info get_fun_info(expr const & fn, unsigned nargs); + /** \brief Display the current state of the blast tactic in the diagnostic channel. */ void display_curr_state(); /** \brief Display the given expression in the diagnostic channel. */