feat(library/tactic): add tactic.mk_app for using app_builder

library/init/meta/tactic.lean

@@ -76,6 +76,20 @@ meta_constant get_local     : name → tactic expr
 meta_constant local_context : tactic (list expr)
 /- Return the number of goals that need to be solved -/
 meta_constant num_goals     : tactic nat
+/-  Helper tactic for creating simple applications where some arguments are inferred using
+    type inference.
+
+    Example, given
+        rel.{l_1 l_2} : Pi (A : Type.{l_1}) (B : A -> Type.{l_2}), (Pi x : A, B x) -> (Pi x : A, B x) -> , Prop
+        nat     : Type.{1}
+        real    : Type.{1}
+        vec.{l} : Pi (A : Type.{l}) (n : nat), Type.{l1}
+        f g     : Pi (n : nat), vec real n
+    then
+        mk_app "rel" [f, g]
+    returns the application
+        rel.{1 2} nat (fun n : nat, vec real n) f g -/
+meta_constant mk_app        : name → list expr → tactic expr
 open list nat
 
 meta_definition intros : tactic unit :=

src/library/app_builder.h

@@ -69,7 +69,7 @@ public:
 class app_builder_exception : public exception {
 public:
     // We may provide more information in the future.
-    app_builder_exception():exception("app_builder_exception") {}
+    app_builder_exception():exception("app_builder_exception, more information can be obtained using commad `set_option trace.app_builder true`") {}
 };
 
 /** \brief Helper for creating simple applications where some arguments are inferred using
@@ -102,8 +102,7 @@ class app_builder {
     level get_level(expr const & A);
 
 public:
-    app_builder(type_context & ctx, app_builder_cache & cache);
-    ~app_builder();
+    app_builder(type_context & ctx, app_builder_cache & cache):m_ctx(ctx), m_cache(cache) {}
     /** \brief Create an application (d.{_ ... _} _ ... _ args[0] ... args[nargs-1]).
         The missing arguments and universes levels are inferred using type inference.
 

src/library/init_module.cpp

@@ -49,12 +49,11 @@ Author: Leonardo de Moura
 #include "library/defeq_simp_lemmas.h"
 #include "library/defeq_simplifier.h"
 #include "library/lazy_abstraction.h"
+#include "library/app_builder.h"
 
 // #include "library/congr_lemma_manager.h"
 // #include "library/light_lt_manager.h"
 // #include "library/fun_info_manager.h"
-// #include "library/app_builder.h"
-
 
 #include "library/old_converter.h"
 #include "library/old_default_converter.h"
@@ -121,9 +120,9 @@ void initialize_library_module() {
     initialize_class_instance_resolution();
     initialize_old_type_context();
     initialize_legacy_type_context();
+    initialize_app_builder();
     // initialize_light_rule_set();
     // initialize_congr_lemma_manager();
-    // initialize_app_builder();
     // initialize_fun_info_manager();
     initialize_unification_hint();
     initialize_defeq_simp_lemmas();
@@ -139,9 +138,9 @@ void finalize_library_module() {
     finalize_defeq_simp_lemmas();
     finalize_unification_hint();
     // finalize_fun_info_manager();
-    // finalize_app_builder();
     // finalize_congr_lemma_manager();
     // finalize_light_rule_set();
+    finalize_app_builder();
     finalize_legacy_type_context();
     finalize_old_type_context();
     finalize_class_instance_resolution();

src/library/tactic/CMakeLists.txt

@@ -1,2 +1,3 @@
 add_library(tactic OBJECT tactic_state.cpp intro_tactic.cpp assumption_tactic.cpp
-  revert_tactic.cpp rename_tactic.cpp clear_tactic.cpp elaborate.cpp init_module.cpp)
+  revert_tactic.cpp rename_tactic.cpp clear_tactic.cpp
+  app_builder_tactics.cpp elaborate.cpp init_module.cpp)

src/library/tactic/app_builder_tactics.cpp

@@ -0,0 +1,54 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "library/vm/vm.h"
+#include "library/vm/vm_list.h"
+#include "library/vm/vm_name.h"
+#include "library/vm/vm_expr.h"
+#include "library/tactic/tactic_state.h"
+#include "library/tactic/app_builder_tactics.h"
+
+namespace lean {
+struct app_builder_cache_helper {
+    typedef std::unique_ptr<app_builder_cache> cache_ptr;
+    cache_ptr m_cache_ptr;
+
+    void ensure_compatible(environment const & env) {
+        if (!m_cache_ptr || !is_eqp(env, m_cache_ptr->env())) {
+            m_cache_ptr.reset(new app_builder_cache(env));
+        }
+    }
+};
+
+MK_THREAD_LOCAL_GET_DEF(app_builder_cache_helper, get_abch);
+
+app_builder_cache & get_app_builder_cache_for(environment const & env) {
+    get_abch().ensure_compatible(env);
+    return *get_abch().m_cache_ptr.get();
+}
+
+vm_obj tactic_mk_app(vm_obj const & c, vm_obj const & as, vm_obj const & _s) {
+    tactic_state const & s = to_tactic_state(_s);
+    try {
+        metavar_context mctx   = s.mctx();
+        type_context ctx       = mk_type_context_for(s, mctx);
+        app_builder b          = mk_app_builder_for(ctx);
+        buffer<expr> args;
+        to_buffer_expr(as, args);
+        expr r                 = b.mk_app(to_name(c), args.size(), args.data());
+        return mk_tactic_success(to_obj(r), s);
+    } catch (exception & ex) {
+        return mk_tactic_exception(ex, s);
+    }
+}
+
+void initialize_app_builder_tactics() {
+    DECLARE_VM_BUILTIN(name({"tactic", "mk_app"}),   tactic_mk_app);
+}
+
+void finalize_app_builder_tactics() {
+}
+}

src/library/tactic/app_builder_tactics.h

@@ -0,0 +1,19 @@
+/*
+Copyright (c) 2016 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/app_builder.h"
+
+namespace lean {
+app_builder_cache & get_app_builder_cache_for(environment const & env);
+
+inline app_builder mk_app_builder_for(type_context & ctx) {
+    return app_builder(ctx, get_app_builder_cache_for(ctx.env()));
+}
+
+void initialize_app_builder_tactics();
+void finalize_app_builder_tactics();
+}

src/library/tactic/init_module.cpp

@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "library/tactic/revert_tactic.h"
 #include "library/tactic/rename_tactic.h"
 #include "library/tactic/clear_tactic.h"
+#include "library/tactic/app_builder_tactics.h"
 #include "library/tactic/elaborate.h"
 
 namespace lean {
@@ -20,10 +21,12 @@ void initialize_tactic_module() {
     initialize_revert_tactic();
     initialize_rename_tactic();
     initialize_clear_tactic();
+    initialize_app_builder_tactics();
     initialize_elaborate();
 }
 void finalize_tactic_module() {
     finalize_elaborate();
+    finalize_app_builder_tactics();
     finalize_clear_tactic();
     finalize_rename_tactic();
     finalize_revert_tactic();

tests/lean/run/app_builder_tac1.lean

@@ -0,0 +1,15 @@
+open tactic list nat name
+
+set_option trace.app_builder true
+set_option pp.all true
+
+example (a b : nat) : nat :=
+by do a ← get_local "a",
+      b ← get_local "b",
+      mk_app "add" [a, b] >>= trace_expr,
+      mk_app "mul" [a, b] >>= trace_expr,
+      mk_app "sub" [a, b] >>= trace_expr,
+      c ← mk_app "eq" [a, b],
+      trace_expr c,
+      assumption,
+      return ()