From f86f8b040f1a4d93fbde1af6103ae21ca87a77ff Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 13 Jun 2016 10:12:00 -0700
Subject: [PATCH] feat(library/tactic): add 'by' annotation

---
 src/library/tactic/CMakeLists.txt  |  2 +-
 src/library/tactic/elaborate.cpp   | 23 +++++++++++++++++++++++
 src/library/tactic/elaborate.h     | 17 +++++++++++++++++
 src/library/tactic/init_module.cpp |  3 +++
 4 files changed, 44 insertions(+), 1 deletion(-)
 create mode 100644 src/library/tactic/elaborate.cpp
 create mode 100644 src/library/tactic/elaborate.h

diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt
index 0ef30c55a9..d8129c0395 100644
--- a/src/library/tactic/CMakeLists.txt
+++ b/src/library/tactic/CMakeLists.txt
@@ -1,2 +1,2 @@
 add_library(tactic OBJECT tactic_state.cpp intro_tactic.cpp assumption_tactic.cpp
-  revert_tactic.cpp rename_tactic.cpp clear_tactic.cpp init_module.cpp)
+  revert_tactic.cpp rename_tactic.cpp clear_tactic.cpp elaborate.cpp init_module.cpp)
diff --git a/src/library/tactic/elaborate.cpp b/src/library/tactic/elaborate.cpp
new file mode 100644
index 0000000000..3db091425f
--- /dev/null
+++ b/src/library/tactic/elaborate.cpp
@@ -0,0 +1,23 @@
+/*
+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/annotation.h"
+
+namespace lean {
+static name * g_by_name = nullptr;
+
+expr mk_by(expr const & e) { return mk_annotation(*g_by_name, e); }
+bool is_by(expr const & e) { return is_annotation(e, *g_by_name); }
+expr const & get_by_arg(expr const & e) { lean_assert(is_by(e)); return get_annotation_arg(e); }
+
+void initialize_elaborate() {
+    g_by_name           = new name("by");
+    register_annotation(*g_by_name);
+}
+void finalize_elaborate() {
+    delete g_by_name;
+}
+}
diff --git a/src/library/tactic/elaborate.h b/src/library/tactic/elaborate.h
new file mode 100644
index 0000000000..66757ae7e3
--- /dev/null
+++ b/src/library/tactic/elaborate.h
@@ -0,0 +1,17 @@
+/*
+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 "kernel/expr.h"
+
+namespace lean {
+expr mk_by(expr const & e);
+bool is_by(expr const & e);
+expr const & get_by_arg(expr const & e);
+
+void initialize_elaborate();
+void finalize_elaborate();
+}
diff --git a/src/library/tactic/init_module.cpp b/src/library/tactic/init_module.cpp
index 9d4f8b958b..aa77875ccb 100644
--- a/src/library/tactic/init_module.cpp
+++ b/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/elaborate.h"
 
 namespace lean {
 void initialize_tactic_module() {
@@ -19,8 +20,10 @@ void initialize_tactic_module() {
     initialize_revert_tactic();
     initialize_rename_tactic();
     initialize_clear_tactic();
+    initialize_elaborate();
 }
 void finalize_tactic_module() {
+    finalize_elaborate();
     finalize_clear_tactic();
     finalize_rename_tactic();
     finalize_revert_tactic();