feat(library/blast/forward): start 'pattern' module

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)

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();
 }
 }}

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 <string>
+#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<bool>(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<unsigned> get_fingerprint(entry const & e) {
+        return some(e.hash());
+    }
+};
+
+template class scoped_ext<no_pattern_config>;
+typedef scoped_ext<no_pattern_config> 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<expr> 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<unsigned, unsigned_cmp> 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<expr> 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<param_info> 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<expr, pattern_info, expr_quick_cmp> 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;
+}
+}

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();
+}