From e9ae5019ca67cfcd055b5bc800b180bf825036c4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 9 Jun 2016 16:06:40 -0700
Subject: [PATCH] feat(library/tactic): init intro tactic

---
 src/library/tactic/CMakeLists.txt   |  2 +-
 src/library/tactic/init_module.cpp  |  3 +++
 src/library/tactic/intro_tactic.cpp | 38 +++++++++++++++++++++++++++++
 src/library/tactic/intro_tactic.h   | 11 +++++++++
 4 files changed, 53 insertions(+), 1 deletion(-)
 create mode 100644 src/library/tactic/intro_tactic.cpp
 create mode 100644 src/library/tactic/intro_tactic.h

diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt
index 02a7fa203c..6f259d5330 100644
--- a/src/library/tactic/CMakeLists.txt
+++ b/src/library/tactic/CMakeLists.txt
@@ -1 +1 @@
-add_library(tactic OBJECT tactic_state.cpp init_module.cpp)
+add_library(tactic OBJECT tactic_state.cpp intro_tactic.cpp init_module.cpp)
diff --git a/src/library/tactic/init_module.cpp b/src/library/tactic/init_module.cpp
index a69e10052f..ca3d34850c 100644
--- a/src/library/tactic/init_module.cpp
+++ b/src/library/tactic/init_module.cpp
@@ -5,12 +5,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "library/tactic/tactic_state.h"
+#include "library/tactic/intro_tactic.h"
 
 namespace lean {
 void initialize_tactic_module() {
     initialize_tactic_state();
+    initialize_intro_tactic();
 }
 void finalize_tactic_module() {
+    finalize_intro_tactic();
     finalize_tactic_state();
 }
 }
diff --git a/src/library/tactic/intro_tactic.cpp b/src/library/tactic/intro_tactic.cpp
new file mode 100644
index 0000000000..1b963cff94
--- /dev/null
+++ b/src/library/tactic/intro_tactic.cpp
@@ -0,0 +1,38 @@
+/*
+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 "kernel/instantiate.h"
+#include "library/vm/vm_name.h"
+#include "library/tactic/tactic_state.h"
+
+namespace lean {
+vm_obj tactic_intro_core(name const & n, tactic_state const & s) {
+    optional<metavar_decl> g = s.get_main_goal();
+    if (!g) return mk_no_goals_exception();
+    metavar_context mctx = s.mctx();
+    type_context ctx     = mk_type_context_for(s, mctx);
+    expr type            = ctx.whnf(g->get_type());
+    if (!is_pi(type))
+        return mk_tactic_exception("intro tactic failed, Pi type expected");
+    local_context lctx   = g->get_context();
+    expr H               = lctx.mk_local_decl(binding_name(type), binding_domain(type), binding_info(type));
+    expr new_type        = instantiate(binding_body(type), H);
+    expr new_M           = mctx.mk_metavar_decl(lctx, new_type);
+    // TODO(Leo)
+    lean_unreachable();
+}
+
+vm_obj tactic_intro(vm_obj const & n, vm_obj const & s) {
+    return tactic_intro_core(to_name(n), to_tactic_state(s));
+}
+
+void initialize_intro_tactic() {
+    DECLARE_VM_BUILTIN(name({"tactic", "intro"}),   tactic_intro);
+}
+
+void finalize_intro_tactic() {
+}
+}
diff --git a/src/library/tactic/intro_tactic.h b/src/library/tactic/intro_tactic.h
new file mode 100644
index 0000000000..de386a9510
--- /dev/null
+++ b/src/library/tactic/intro_tactic.h
@@ -0,0 +1,11 @@
+/*
+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
+namespace lean {
+void initialize_intro_tactic();
+void finalize_intro_tactic();
+}