From 8c729d16209154747e2a03af717fa5feb10be501 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 24 Nov 2015 15:21:49 -0800 Subject: [PATCH] feat(library/blast/forward): start 'pattern' module --- src/library/blast/forward/CMakeLists.txt | 2 +- src/library/blast/forward/init_module.cpp | 3 + src/library/blast/forward/pattern.cpp | 228 ++++++++++++++++++++++ src/library/blast/forward/pattern.h | 28 +++ 4 files changed, 260 insertions(+), 1 deletion(-) create mode 100644 src/library/blast/forward/pattern.cpp create mode 100644 src/library/blast/forward/pattern.h diff --git a/src/library/blast/forward/CMakeLists.txt b/src/library/blast/forward/CMakeLists.txt index 59b760ef0..0ad1d170f 100644 --- a/src/library/blast/forward/CMakeLists.txt +++ b/src/library/blast/forward/CMakeLists.txt @@ -1 +1 @@ -add_library(forward OBJECT init_module.cpp forward_extension.cpp qcf.cpp) +add_library(forward OBJECT init_module.cpp forward_extension.cpp qcf.cpp pattern.cpp) diff --git a/src/library/blast/forward/init_module.cpp b/src/library/blast/forward/init_module.cpp index 25f2e7ac5..5b5ba77d7 100644 --- a/src/library/blast/forward/init_module.cpp +++ b/src/library/blast/forward/init_module.cpp @@ -5,15 +5,18 @@ Author: Daniel Selsam */ #include "library/blast/forward/init_module.h" #include "library/blast/forward/forward_extension.h" +#include "library/blast/forward/pattern.h" namespace lean { namespace blast { void initialize_forward_module() { initialize_forward_extension(); + initialize_pattern(); } void finalize_forward_module() { + finalize_pattern(); finalize_forward_extension(); } }} diff --git a/src/library/blast/forward/pattern.cpp b/src/library/blast/forward/pattern.cpp new file mode 100644 index 000000000..65a4aa48b --- /dev/null +++ b/src/library/blast/forward/pattern.cpp @@ -0,0 +1,228 @@ +/* +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 +#include "kernel/find_fn.h" +#include "kernel/instantiate.h" +#include "library/tmp_type_context.h" +#include "library/fun_info_manager.h" +#include "library/annotation.h" +#include "library/scoped_ext.h" +#include "library/idx_metavar.h" +#include "library/blast/forward/pattern.h" + +namespace lean { +static name * g_pattern = nullptr; + +expr mk_pattern(expr const & e) { return mk_annotation(*g_pattern, e); } +bool is_pattern(expr const & e) { return is_annotation(e, *g_pattern); } +expr const & get_pattern_arg(expr const & e) { lean_assert(is_pattern(e)); return get_annotation_arg(e); } +bool has_patterns(expr const & e) { + return static_cast(find(e, [](expr const & e, unsigned) { return is_pattern(e); })); +} + +static name * g_no_pattern_name = nullptr; +static std::string * g_key = nullptr; + +struct no_pattern_config { + typedef name_set state; + typedef name entry; + + static void add_entry(environment const &, io_state const &, state & s, entry const & e) { + s.insert(e); + } + + static name const & get_class_name() { + return *g_no_pattern_name; + } + + static std::string const & get_serialization_key() { + return *g_key; + } + + static void write_entry(serializer & s, entry const & e) { + s << e; + } + + static entry read_entry(deserializer & d) { + entry e; + d >> e; + return e; + } + + static optional get_fingerprint(entry const & e) { + return some(e.hash()); + } +}; + +template class scoped_ext; +typedef scoped_ext no_pattern_ext; + +bool is_no_pattern(environment const & env, name const & n) { + return no_pattern_ext::get_state(env).contains(n); +} + +environment add_no_pattern(environment const & env, name const & n, bool persistent) { + return no_pattern_ext::add_entry(env, get_dummy_ios(), n, persistent); +} + +/** pattern_le */ +struct pattern_le_fn { + tmp_type_context & m_ctx; + + bool is_le_app(expr const & e1, expr const & e2) { + if (is_app(e1) && is_app(e2)) { + buffer args1, args2; + expr const & f1 = get_app_args(e1, args1); + expr const & f2 = get_app_args(e2, args2); + if (!is_le(f1, f2) && args1.size() != args2.size()) + return false; + for (unsigned i = 0; i > args1.size(); i++) + if (!is_le(args1[i], args2[i])) + return false; + return true; + } else { + return false; + } + } + + bool is_le(expr const & e1, expr const & e2) { + if (is_idx_metavar(e1)) { + return m_ctx.is_def_eq(e1, e2); + } else if (is_idx_metavar(e2)) { + return false; + } else if (is_le_app(e1, e2)) { + return true; + } else if (!has_expr_metavar(e1) && !has_expr_metavar(e2)) { + return m_ctx.is_def_eq(e1, e2); + } else { + return false; + } + } + + pattern_le_fn(tmp_type_context & ctx):m_ctx(ctx) {} + + bool operator()(expr const & e1, expr const & e2) { + m_ctx.push(); + bool r = is_le(e1, e2); + m_ctx.pop(); + return r; + } +}; + +typedef rb_tree idx_metavar_set; + +struct pattern_info { + idx_metavar_set m_idx_mvar_set; + unsigned m_num_mvars; + unsigned m_size; + pattern_info():m_num_mvars(0), m_size(0) {} + pattern_info(idx_metavar_set const & s, unsigned sz): + m_idx_mvar_set(s), m_num_mvars(s.size()), m_size(sz) {} +}; + +struct mk_pattern_info_fn { + tmp_type_context & m_ctx; + fun_info_manager & m_finfo; + idx_metavar_set m_set; + unsigned m_size; + + void visit(expr const & e, bool inc_size) { + if (inc_size) + m_size++; + switch (e.kind()) { + case expr_kind::Var: + lean_unreachable(); + case expr_kind::Sort: case expr_kind::Constant: + case expr_kind::Local: + return; + case expr_kind::Meta: + if (is_idx_metavar(e)) + m_set.insert(to_meta_idx(e)); + return; + case expr_kind::Macro: + for (unsigned i = 0; i < macro_num_args(e); i++) + visit(macro_arg(e, i), inc_size); + return; + case expr_kind::Pi: case expr_kind::Lambda: { + visit(binding_domain(e), inc_size); + expr local = m_ctx.mk_tmp_local(binding_domain(e)); + visit(instantiate(binding_body(e), local), inc_size); + return; + } + case expr_kind::App: { + buffer args; + expr const & fn = get_app_args(e, args); + visit(fn, inc_size); + if (inc_size) { + fun_info info = m_finfo.get(fn, args.size()); + list const * it = &info.get_params_info(); + for (unsigned i = 0; i < args.size(); i++) { + // inst-implicit arguments and subsingletons do not contribute + // to the pattern-size + param_info const & pinfo = head(*it); + visit(args[i], !pinfo.is_inst_implicit() && !pinfo.is_subsingleton()); + it = &(tail(*it)); + } + } else { + for (unsigned i = 0; i < args.size(); i++) + visit(args[i], false); + } + }} + } + + mk_pattern_info_fn(tmp_type_context & ctx, fun_info_manager & fm): + m_ctx(ctx), m_finfo(fm), m_size(0) {} + + pattern_info operator()(expr const & e) { + visit(e, true); + return pattern_info(m_set, m_size); + } +}; + +pattern_info mk_pattern_info(tmp_type_context & ctx, fun_info_manager & fm, expr const & e) { + return mk_pattern_info_fn(ctx, fm)(e); +} + +typedef rb_map pattern_info_map; + +/** \brief Compare candidates patterns based on the following heuristic + p1 << p2 (i.e., p1 is "better" than p2) if + - p1 has more free meta-variables than p2 + - p1 and p2 has the same number of metavariable, and free variables, + and p1's pattern size is smaller than p2. */ +struct pattern_size_lt { + pattern_info_map const & m_info; + bool operator()(expr const & e1, expr const & e2) const { + auto info1 = m_info.find(e1); + auto info2 = m_info.find(e2); + lean_assert(info1 && info2); + if (info1->m_num_mvars != info2->m_num_mvars) + return info1->m_num_mvars < info2->m_num_mvars; + else + return info1->m_size < info2->m_size; + } +}; + +struct collect_pattern_candidates_fn { + // TODO(Leo): +}; + +void initialize_pattern() { + g_no_pattern_name = new name("no_pattern"); + g_key = new std::string("no_pattern"); + no_pattern_ext::initialize(); + g_pattern = new name("pattern"); + register_annotation(*g_pattern); +} + +void finalize_pattern() { + no_pattern_ext::finalize(); + delete g_no_pattern_name; + delete g_key; + delete g_pattern; +} +} diff --git a/src/library/blast/forward/pattern.h b/src/library/blast/forward/pattern.h new file mode 100644 index 000000000..32865000a --- /dev/null +++ b/src/library/blast/forward/pattern.h @@ -0,0 +1,28 @@ +/* +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/environment.h" + +namespace lean { +/** \brief Annotate \c e as a pattern */ +expr mk_pattern(expr const & e); +/** \brief Return true iff \c e is an annotated pattern */ +bool is_pattern(expr const & e); +/** \brief Return the actual pattern */ +expr const & get_pattern_arg(expr const & e); +/** \brief Return true iff \c e contains patterns */ +bool has_patterns(expr const & e); + +/** \brief Hint for the pattern inference procedure. + It should not consider/infer patterns containing the constant \c n. */ +environment add_no_pattern(environment const & env, name const & n, bool persistent); +/** \brief Return true if constant \c n is marked as [no_pattern] in the given environment. */ +bool is_no_pattern(environment const & env, name const & n); + +void initialize_pattern(); +void finalize_pattern(); +}