feat(library/blast): parse blast tactic and invoke stub

hott/init/tactic.hlean

@@ -100,6 +100,10 @@ definition krewrite_tac (e : expr_list) : tactic := builtin
 --  - t : tactic for discharging conditions
 --  - l : location
 definition simp_tac (e : expr_list) (n : identifier_list) (x : identifier_list) (t : option tactic) (l : expr) : tactic := builtin
+-- Arguments:
+--  - ls : lemmas to be used (if not provided, then blast will choose them)
+--  - ds : definitions that can be unfolded (if not provided, then blast will choose them)
+definition blast (ls : opt_identifier_list) (ds : opt_identifier_list) : tactic := builtin
 
 -- with_options_tac is just a marker for the builtin 'with_options' notation
 definition with_options_tac (o : expr) (t : tactic) : tactic := builtin

library/init/tactic.lean

@@ -100,6 +100,10 @@ definition krewrite_tac (e : expr_list) : tactic := builtin
 --  - t : tactic for discharging conditions
 --  - l : location
 definition simp_tac (e : expr_list) (n : identifier_list) (x : identifier_list) (t : option tactic) (l : expr) : tactic := builtin
+-- Arguments:
+--  - ls : lemmas to be used (if not provided, then blast will choose them)
+--  - ds : definitions that can be unfolded (if not provided, then blast will choose them)
+definition blast (ls : opt_identifier_list) (ds : opt_identifier_list) : tactic := builtin
 
 -- with_options_tac is just a marker for the builtin 'with_options' notation
 definition with_options_tac (o : expr) (t : tactic) : tactic := builtin

src/emacs/lean-syntax.el

@@ -158,7 +158,7 @@
                 "apply" "fapply" "eapply" "rename" "intro" "intros" "all_goals" "fold" "focus" "focus_at"
                 "generalize" "generalizes" "clear" "clears" "revert" "reverts" "back" "beta" "done" "exact" "rexact"
                 "refine" "repeat" "whnf" "rotate" "rotate_left" "rotate_right" "inversion" "cases" "rewrite"
-                "xrewrite" "krewrite" "simp" "esimp" "unfold" "change" "check_expr" "contradiction"
+                "xrewrite" "krewrite" "blast" "simp" "esimp" "unfold" "change" "check_expr" "contradiction"
                 "exfalso" "split" "existsi" "constructor" "fconstructor" "left" "right" "injection" "congruence" "reflexivity"
                 "symmetry" "transitivity" "state" "induction" "induction_using" "fail" "append"
                 "substvars" "now" "with_options"))

src/init/init.cpp

@@ -15,6 +15,7 @@ Author: Leonardo de Moura
 #include "kernel/hits/hits.h"
 #include "library/init_module.h"
 #include "library/simplifier/init_module.h"
+#include "library/blast/init_module.h"
 #include "library/tactic/init_module.h"
 #include "library/definitional/init_module.h"
 #include "library/print.h"
@@ -37,6 +38,7 @@ void initialize() {
     initialize_library_module();
     initialize_tactic_module();
     initialize_simplifier_module();
+    initialize_blast_module();
     initialize_definitional_module();
     initialize_compiler_module();
     initialize_frontend_lean_module();
@@ -47,6 +49,7 @@ void finalize() {
     finalize_frontend_lean_module();
     finalize_compiler_module();
     finalize_definitional_module();
+    finalize_blast_module();
     finalize_simplifier_module();
     finalize_tactic_module();
     finalize_library_module();

src/library/blast/CMakeLists.txt

@@ -1 +1 @@
-add_library(blast OBJECT state.cpp expr.cpp)
+add_library(blast OBJECT state.cpp expr.cpp blast_tactic.cpp init_module.cpp blast.cpp)

src/library/blast/blast.cpp

@@ -0,0 +1,33 @@
+/*
+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/expr.h"
+#include "library/blast/state.h"
+#include "library/blast/blast.h"
+
+namespace lean {
+namespace blast {
+class context {
+    environment m_env;
+    io_state    m_ios;
+    name_set    m_lemma_hints;
+    name_set    m_unfold_hints;
+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)) {
+    }
+    optional<expr> operator()(goal const &) {
+        return none_expr();
+    }
+};
+}
+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 scope;
+    blast::context c(env, ios, ls, ds);
+    return c(g);
+}
+}

src/library/blast/blast.h

@@ -0,0 +1,13 @@
+/*
+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 "library/tactic/goal.h"
+
+namespace lean {
+optional<expr> blast_goal(environment const & env, io_state const & ios, list<name> const & ls, list<name> const & ds,
+                          goal const & g);
+}

src/library/blast/blast_tactic.cpp

@@ -0,0 +1,47 @@
+/*
+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/tactic/expr_to_tactic.h"
+#include "library/blast/blast.h"
+
+namespace lean {
+tactic mk_blast_tactic(list<name> const & ls, list<name> const & ds) {
+    return tactic01([=](environment const & env, io_state const & ios, proof_state const & _s) {
+            proof_state s = apply_substitution(_s);
+            goals const & gs = s.get_goals();
+            if (empty(gs)) {
+                throw_no_goal_if_enabled(s);
+                return none_proof_state();
+            }
+            goal const & g = head(gs);
+            if (auto pr = blast_goal(env, ios, ls, ds, g)) {
+                goals new_gs           = tail(gs);
+                substitution new_subst = s.get_subst();
+                assign(new_subst, g, *pr);
+                return some_proof_state(proof_state(s, new_gs, new_subst));
+            } else {
+                throw_tactic_exception_if_enabled(s, "blast tactic failed");
+                return none_proof_state();
+            }
+        });
+}
+
+void initialize_blast_tactic() {
+    register_tac(name{"tactic", "blast"},
+                 [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
+                     buffer<expr> args;
+                     get_app_args(e, args);
+                     if (args.size() != 2)
+                         throw expr_to_tactic_exception(e, "invalid 'blast' tactic, incorrect number of arguments");
+                     buffer<name> ls, ds;
+                     get_tactic_id_list_elements(args[0], ls, "invalid 'blast' tactic, list of identifiers expected");
+                     get_tactic_id_list_elements(args[1], ds, "invalid 'blast' tactic, list of identifiers expected");
+                     return mk_blast_tactic(to_list(ls), to_list(ds));
+                 });
+}
+void finalize_blast_tactic() {
+}
+}

src/library/blast/blast_tactic.h

@@ -0,0 +1,13 @@
+/*
+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 {
+void initialize_blast_tactic();
+void finalize_blast_tactic();
+}

src/library/blast/hypothesis.h

@@ -12,13 +12,13 @@ Author: Leonardo de Moura
 namespace lean {
 namespace blast {
 class hypothesis;
+class branch;
 class state;
-class goal;
 
 typedef rb_tree<unsigned, unsigned_cmp> hypothesis_set;
 
 class hypothesis {
-    friend class goal;
+    friend class branch;
     bool           m_active;
     unsigned       m_depth;
     hypothesis_set m_backward_deps;
@@ -36,5 +36,4 @@ public:
     optional<expr> const & get_value() const { return m_value; }
     optional<expr> const & get_justification() const { return m_justification; }
 };
-}
-}
+}}

src/library/blast/init_module.cpp

@@ -0,0 +1,16 @@
+/*
+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/blast_tactic.h"
+
+namespace lean {
+void initialize_blast_module() {
+    initialize_blast_tactic();
+}
+void finalize_blast_module() {
+    finalize_blast_tactic();
+}
+}

src/library/blast/init_module.h

@@ -0,0 +1,12 @@
+/*
+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
+
+namespace lean {
+void initialize_blast_module();
+void finalize_blast_module();
+}

src/library/blast/state.h

@@ -18,6 +18,8 @@ class metavar_decl {
 
 class state {
     typedef rb_map<unsigned, metavar_decl, unsigned_cmp> metavar_decls;
+    typedef rb_map<unsigned, expr, unsigned_cmp>         assignment;
     metavar_decls m_metavar_decls;
+    assignment    m_assignment;
 };
 }}

src/util/name_set.cpp

@@ -18,13 +18,6 @@ name mk_unique(name_set const & s, name const & suggestion) {
     }
 }
 
-name_set to_name_set(buffer<name> const & ns) {
-    name_set r;
-    for (name const & n : ns)
-        r.insert(n);
-    return r;
-}
-
 DECL_UDATA(name_set)
 static int mk_name_set(lua_State * L) {
     name_set r;

src/util/name_set.h

@@ -13,7 +13,13 @@ typedef rb_tree<name, name_quick_cmp> name_set;
 /** \brief Make a name that does not occur in \c s, based on the given suggestion. */
 name mk_unique(name_set const & s, name const & suggestion);
 
-name_set to_name_set(buffer<name> const & ns);
+template<typename C>
+name_set to_name_set(C const & ns) {
+    name_set r;
+    for (name const & n : ns)
+        r.insert(n);
+    return r;
+}
 
 UDATA_DEFS_CORE(name_set)
 void open_name_set(lua_State * L);