From 42831111981a7812b749bf0d062afb8e4bba6014 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 28 Apr 2015 10:55:04 -0700
Subject: [PATCH] fix(frontends/lean): missing files

---
 src/frontends/lean/builtin_tactics.cpp | 72 ++++++++++++++++++++++++++
 src/frontends/lean/builtin_tactics.h   | 14 +++++
 2 files changed, 86 insertions(+)
 create mode 100644 src/frontends/lean/builtin_tactics.cpp
 create mode 100644 src/frontends/lean/builtin_tactics.h

diff --git a/src/frontends/lean/builtin_tactics.cpp b/src/frontends/lean/builtin_tactics.cpp
new file mode 100644
index 000000000..0b6ee54d9
--- /dev/null
+++ b/src/frontends/lean/builtin_tactics.cpp
@@ -0,0 +1,72 @@
+/*
+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 "frontends/lean/parser.h"
+#include "frontends/lean/parse_rewrite_tactic.h"
+
+namespace lean {
+namespace notation {
+static expr parse_rewrite_tactic_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
+    return p.save_pos(parse_rewrite_tactic(p), pos);
+}
+
+static expr parse_esimp_tactic_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
+    return p.save_pos(parse_esimp_tactic(p), pos);
+}
+
+static expr parse_unfold_tactic_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
+    return p.save_pos(parse_unfold_tactic(p), pos);
+}
+
+static expr parse_fold_tactic_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
+    return p.save_pos(parse_fold_tactic(p), pos);
+}
+
+static expr parse_rparen(parser &, unsigned, expr const * args, pos_info const &) {
+    return args[0];
+}
+
+parse_table init_tactic_nud_table() {
+    action Expr(mk_expr_action());
+    expr x0 = mk_var(0);
+    parse_table r;
+    r = r.add({transition("(", Expr), transition(")", mk_ext_action(parse_rparen))}, x0);
+    r = r.add({transition("rewrite", mk_ext_action(parse_rewrite_tactic_expr))}, x0);
+    r = r.add({transition("esimp",   mk_ext_action(parse_esimp_tactic_expr))}, x0);
+    r = r.add({transition("unfold",  mk_ext_action(parse_unfold_tactic_expr))}, x0);
+    r = r.add({transition("fold",    mk_ext_action(parse_fold_tactic_expr))}, x0);
+    return r;
+}
+
+parse_table init_tactic_led_table() {
+    parse_table r(false);
+    return r;
+}
+}
+
+static parse_table * g_nud_table = nullptr;
+static parse_table * g_led_table = nullptr;
+
+parse_table get_builtin_tactic_nud_table() {
+    return *g_nud_table;
+}
+
+parse_table get_builtin_tactic_led_table() {
+    return *g_led_table;
+}
+
+void initialize_builtin_tactics() {
+    g_nud_table             = new parse_table();
+    *g_nud_table            = notation::init_tactic_nud_table();
+    g_led_table             = new parse_table();
+    *g_led_table            = notation::init_tactic_led_table();
+}
+
+void finalize_builtin_tactics() {
+    delete g_led_table;
+    delete g_nud_table;
+}
+}
diff --git a/src/frontends/lean/builtin_tactics.h b/src/frontends/lean/builtin_tactics.h
new file mode 100644
index 000000000..ba788123c
--- /dev/null
+++ b/src/frontends/lean/builtin_tactics.h
@@ -0,0 +1,14 @@
+/*
+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 "frontends/lean/parse_table.h"
+namespace lean {
+parse_table get_builtin_tactic_nud_table();
+parse_table get_builtin_tactic_led_table();
+void initialize_builtin_tactics();
+void finalize_builtin_tactics();
+}