feat(library/blast): add whnf for blast tactic

src/library/blast/CMakeLists.txt

@@ -1,2 +1,2 @@
-add_library(blast OBJECT expr.cpp branch.cpp state.cpp blast.cpp
+add_library(blast OBJECT expr.cpp branch.cpp state.cpp infer_type.cpp blast.cpp
   blast_tactic.cpp init_module.cpp)

src/library/blast/blast.cpp

@@ -10,8 +10,10 @@ Author: Leonardo de Moura
 #include "library/util.h"
 #include "library/reducible.h"
 #include "library/normalize.h"
+#include "library/projection.h"
 #include "library/blast/expr.h"
 #include "library/blast/state.h"
+#include "library/blast/infer_type.h"
 #include "library/blast/blast.h"
 #include "library/blast/blast_context.h"
 #include "library/blast/blast_exception.h"
@@ -39,12 +41,14 @@ level to_blast_level(level const & l) {
 static name * g_prefix = nullptr;
 
 class context {
-    environment    m_env;
-    io_state       m_ios;
-    name_set       m_lemma_hints;
-    name_set       m_unfold_hints;
-    name_map<expr> m_mvar2mref;    // map goal metavariables to blast mref's
-    state          m_curr_state;   // current state
+    environment               m_env;
+    io_state                  m_ios;
+    name_set                  m_lemma_hints;
+    name_set                  m_unfold_hints;
+    name_map<expr>            m_mvar2mref;    // map goal metavariables to blast mref's
+    name_predicate            m_not_reducible_pred;
+    name_map<projection_info> m_projection_info;
+    state                     m_curr_state;   // current state
 
     class to_blast_expr_fn : public replace_visitor {
         type_checker                 m_tc;
@@ -214,7 +218,8 @@ class context {
 
 public:
     context(environment const & env, io_state const & ios, list<name> const & ls, list<name> const & ds):
-        m_env(env), m_ios(ios), m_lemma_hints(to_name_set(ls)), m_unfold_hints(to_name_set(ds)) {
+        m_env(env), m_ios(ios), m_lemma_hints(to_name_set(ls)), m_unfold_hints(to_name_set(ds)),
+        m_not_reducible_pred(mk_not_reducible_pred(env)) {
     }
 
     optional<expr> operator()(goal const & g) {
@@ -231,7 +236,17 @@ public:
 
     io_state const & get_ios() const { return m_ios; }
 
-    state const & get_curr_state() const { return m_curr_state; }
+    state & get_curr_state() { return m_curr_state; }
+
+    bool is_reducible(name const & n) const {
+        if (m_not_reducible_pred(n))
+            return false;
+        return !m_projection_info.contains(n);
+    }
+
+    projection_info const * get_projection_info(name const & n) const {
+        return m_projection_info.find(n);
+    }
 };
 
 LEAN_THREAD_PTR(context, g_context);
@@ -252,11 +267,21 @@ io_state const & ios() {
     return g_context->get_ios();
 }
 
-state const & curr_state() {
+state & curr_state() {
     lean_assert(g_context);
     return g_context->get_curr_state();
 }
 
+bool is_reducible(name const & n) {
+    lean_assert(g_context);
+    return g_context->is_reducible(n);
+}
+
+projection_info const * get_projection_info(name const & n) {
+    lean_assert(g_context);
+    return g_context->get_projection_info(n);
+}
+
 void display_curr_state() {
     curr_state().display(env(), ios());
     display("\n");
@@ -269,12 +294,54 @@ void display(char const * msg) {
 void display(sstream const & msg) {
     ios().get_diagnostic_channel() << msg.str();
 }
+
+/** \brief Auxiliary object to interface blast state with existing kernel extensions */
+class ext_context : public extension_context {
+    name_generator m_ngen;
+public:
+    virtual environment const & env() const { return env(); }
+
+    virtual pair<expr, constraint_seq> whnf(expr const & e) {
+        return mk_pair(blast::whnf(e), constraint_seq());
+    }
+
+    virtual pair<bool, constraint_seq> is_def_eq(expr const & e1, expr const & e2, delayed_justification &) {
+        return mk_pair(blast::is_def_eq(e1, e2), constraint_seq());
+    }
+
+    virtual pair<expr, constraint_seq> check_type(expr const & e, bool) {
+        return mk_pair(blast::infer_type(e), constraint_seq());
+    }
+
+    virtual name mk_fresh_name() {
+        return m_ngen.next();
+    }
+
+    virtual optional<expr> is_stuck(expr const &) {
+        return none_expr();
+    }
+};
+
+LEAN_THREAD_PTR(ext_context, g_ext_context);
+struct scope_ext_context {
+    ext_context * m_prev_context;
+public:
+    scope_ext_context(ext_context & c):m_prev_context(g_ext_context) { g_ext_context = &c; }
+    ~scope_ext_context() { g_ext_context = m_prev_context; }
+};
+
+extension_context & ext_ctx() {
+    lean_assert(g_ext_context);
+    return *g_ext_context;
+}
 }
 optional<expr> blast_goal(environment const & env, io_state const & ios, list<name> const & ls, list<name> const & ds,
                           goal const & g) {
     blast::scope_hash_consing scope1;
     blast::context c(env, ios, ls, ds);
+    blast::ext_context x;
     blast::scope_context scope2(c);
+    blast::scope_ext_context scope3(x);
     return c(g);
 }
 void initialize_blast() {

src/library/blast/blast_context.h

@@ -11,6 +11,7 @@ Remark: the API is implemented in the file blast.cpp
 */
 #pragma once
 #include "util/sstream.h"
+#include "library/projection.h"
 #include "library/blast/state.h"
 
 namespace lean {
@@ -20,7 +21,14 @@ environment const & env();
 /** \brief Return the thread local io_state being used by the blast tactic. */
 io_state const & ios();
 /** \brief Return the thread local current state begin processed by the blast tactic. */
-state const & curr_state();
+state & curr_state();
+/** \brief Return the thead local extension context associated with the blast tactic. */
+extension_context & ext_ctx();
+/** \brief Return true iff the given constant name is marked as reducible in env() */
+bool is_reducible(name const & n);
+/** \brief Return a nonnull projection_info object if \c n is the name of a projection in env() */
+projection_info const * get_projection_info(name const & n);
+
 /** \brief Display the current state of the blast tactic in the diagnostic channel. */
 void display_curr_state();
 /** \brief Display message in the blast tactic diagnostic channel. */

src/library/blast/expr.cpp

@@ -195,16 +195,17 @@ expr mk_var(unsigned idx) {
 }
 
 expr mk_app(expr const & f, expr const & a) {
-    lean_assert(is_cached(f));
-    lean_assert(is_cached(a));
+    lean_assert(is_cached(f) && is_cached(a));
     return lean::mk_app(f, a);
 }
 
+bool is_cached(unsigned num, expr const * args) {
+    return std::all_of(args, args+num, [](expr const & e) { return is_cached(e); });
+}
+
 expr mk_app(expr const & f, unsigned num_args, expr const * args) {
-    expr r = f;
-    for (unsigned i = 0; i < num_args; i++)
-        r = blast::mk_app(r, args[i]);
-    return r;
+    lean_assert(is_cached(f) && is_cached(num_args, args));
+    return lean::mk_app(f, num_args, args);
 }
 
 expr mk_app(unsigned num_args, expr const * args) {
@@ -212,6 +213,16 @@ expr mk_app(unsigned num_args, expr const * args) {
     return blast::mk_app(blast::mk_app(args[0], args[1]), num_args - 2, args+2);
 }
 
+expr mk_rev_app(expr const & f, unsigned num_args, expr const * args) {
+    lean_assert(is_cached(f) && is_cached(num_args, args));
+    return lean::mk_rev_app(f, num_args, args);
+}
+
+expr mk_rev_app(unsigned num_args, expr const * args) {
+    lean_assert(num_args >= 2);
+    return blast::mk_rev_app(blast::mk_app(args[num_args-1], args[num_args-2]), num_args-2, args);
+}
+
 expr mk_sort(level const & l) {
     lean_assert(is_cached(l));
     return lean::mk_sort(l);
@@ -223,13 +234,12 @@ expr mk_constant(name const & n, levels const & ls) {
 }
 
 expr mk_binding(expr_kind k, name const & n, expr const & t, expr const & e, binder_info const & bi) {
-    lean_assert(is_cached(t));
-    lean_assert(is_cached(e));
+    lean_assert(is_cached(t) && is_cached(e));
     return lean::mk_binding(k, n, t, e, bi);
 }
 
 expr mk_macro(macro_definition const & m, unsigned num, expr const * args) {
-    lean_assert(std::all_of(args, args+num, [](expr const & e) { return is_cached(e); }));
+    lean_assert(is_cached(num, args));
     return lean::mk_macro(m, num, args);
 }
 

src/library/blast/expr.h

@@ -46,6 +46,8 @@ expr mk_local(unsigned idx, expr const & t);
 expr mk_app(expr const & f, expr const & a);
 expr mk_app(expr const & f, unsigned num_args, expr const * args);
 expr mk_app(unsigned num_args, expr const * args);
+expr mk_rev_app(expr const & f, unsigned num_args, expr const * args);
+expr mk_rev_app(unsigned num_args, expr const * args);
 expr mk_binding(expr_kind k, name const & n, expr const & t, expr const & e, binder_info const & bi);
 inline expr mk_pi(name const & n, expr const & t, expr const & e, binder_info const & bi) {
     return blast::mk_binding(expr_kind::Pi, n, t, e, bi);

src/library/blast/infer_type.cpp

@@ -0,0 +1,115 @@
+/*
+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 "util/interrupt.h"
+#include "kernel/instantiate.h"
+#include "library/blast/infer_type.h"
+#include "library/blast/blast_context.h"
+
+namespace lean {
+namespace blast {
+static optional<expr> expand_macro(expr const & m) {
+    lean_assert(is_macro(m));
+    return macro_def(m).expand(m, ext_ctx());
+}
+
+static optional<expr> reduce_projection(expr const & e) {
+    expr const & f = get_app_fn(e);
+    if (!is_constant(f))
+        return none_expr();
+    projection_info const * info = get_projection_info(const_name(f));
+    if (!info)
+        return none_expr();
+    buffer<expr> args;
+    get_app_args(e, args);
+    if (args.size() <= info->m_nparams)
+        return none_expr();
+    unsigned mkidx  = info->m_nparams;
+    expr const & mk = args[mkidx];
+    expr new_mk     = whnf(mk);
+    expr const & new_mk_fn = get_app_fn(new_mk);
+    if (!is_constant(new_mk_fn) || const_name(new_mk_fn) != info->m_constructor)
+        return none_expr();
+    buffer<expr> mk_args;
+    get_app_args(new_mk, mk_args);
+    unsigned i = info->m_nparams + info->m_i;
+    if (i >= mk_args.size())
+        none_expr();
+    expr r = mk_args[i];
+    r = blast::mk_app(r, args.size() - mkidx - 1, args.data() + mkidx + 1);
+    return some_expr(r);
+}
+
+static optional<expr> norm_ext(expr const & e) {
+    if (auto r = reduce_projection(e)) {
+        return r;
+    } else if (auto r = env().norm_ext()(e, ext_ctx())) {
+        return some_expr(r->first);
+    } else {
+        return none_expr();
+    }
+}
+
+static expr whnf_core(expr const & e) {
+    check_system("whnf");
+
+    switch (e.kind()) {
+    case expr_kind::Var:  case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local:
+    case expr_kind::Pi:   case expr_kind::Lambda:
+        return e;
+    case expr_kind::Constant:
+        if (blast::is_reducible(const_name(e)))
+            return whnf_core(instantiate_value_univ_params(env().get(const_name(e)), const_levels(e)));
+        else
+            return e;
+    case expr_kind::Macro:
+        if (auto m = expand_macro(e))
+            return whnf_core(*m);
+        else
+            return e;
+    case expr_kind::App: {
+        buffer<expr> args;
+        expr f0 = get_app_rev_args(e, args);
+        expr f = whnf_core(f0);
+        if (is_lambda(f)) {
+            unsigned m = 1;
+            unsigned num_args = args.size();
+            while (is_lambda(binding_body(f)) && m < num_args) {
+                f = binding_body(f);
+                m++;
+            }
+            lean_assert(m <= num_args);
+            return whnf_core(blast::mk_rev_app(instantiate(binding_body(f), m, args.data() + (num_args - m)),
+                                               num_args - m, args.data()));
+        } else {
+            return f == f0 ? e : whnf_core(blast::mk_rev_app(f, args.size(), args.data()));
+        }
+    }}
+    lean_unreachable();
+}
+
+expr whnf(expr const & e) {
+    expr t = e;
+    while (true) {
+        expr t1 = whnf_core(t);
+        if (auto new_t = norm_ext(t1)) {
+            t  = *new_t;
+        } else {
+            return t1;
+        }
+    }
+}
+
+bool is_def_eq(expr const & e1, expr const & e2) {
+    // TODO(Leo)
+    return e1 == e2;
+}
+
+expr infer_type(expr const & e) {
+    // TODO(Leo)
+    return e;
+}
+}}

src/library/blast/infer_type.h

@@ -0,0 +1,27 @@
+/*
+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"
+
+namespace lean {
+namespace blast {
+/** \brief Put the given expression in weak-head-normal-form with respect to the
+    current state being processed by the blast tactic. */
+expr whnf(expr const & e);
+/** \brief Return true iff the two expressions are definitionally equal in the
+    current state being processed by the blast tactic.
+
+    \remark: (potential side-effect) this procedure may update the meta-variable assignment
+    associated with the current state. */
+bool is_def_eq(expr const & e1, expr const & e2);
+/** \brief Return the type of the given expression with respect to the current state being
+    processed by the blast tactic.
+
+    \remark: (potential side-effect) this procedure may update the meta-variable assignment
+    associated with the current state. */
+expr infer_type(expr const & e);
+}}