From 7fd502993b4527bb2c26b0fb3452d3a50e0df2dd Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 11 Jun 2014 11:44:16 -0700
Subject: [PATCH] refactor(frontends/lean/cmd_table): remove
 register_builtin_cmd procedures, they would cause initialization problems

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/CMakeLists.txt               |  4 ++--
 src/frontends/lean/builtin_cmds.cpp             | 14 ++++++++++++++
 src/frontends/lean/builtin_cmds.h               | 11 +++++++++++
 .../{cmd_table.cpp => builtin_tactic_cmds.cpp}  |  8 +-------
 src/frontends/lean/builtin_tactic_cmds.h        | 11 +++++++++++
 src/frontends/lean/cmd_table.h                  | 17 -----------------
 src/frontends/lean/parser_config.cpp            |  2 ++
 7 files changed, 41 insertions(+), 26 deletions(-)
 create mode 100644 src/frontends/lean/builtin_cmds.cpp
 create mode 100644 src/frontends/lean/builtin_cmds.h
 rename src/frontends/lean/{cmd_table.cpp => builtin_tactic_cmds.cpp} (66%)
 create mode 100644 src/frontends/lean/builtin_tactic_cmds.h

diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt
index 9b31edcde..c9f1ddc94 100644
--- a/src/frontends/lean/CMakeLists.txt
+++ b/src/frontends/lean/CMakeLists.txt
@@ -1,5 +1,5 @@
 add_library(lean_frontend register_module.cpp token_table.cpp
-scanner.cpp parse_table.cpp cmd_table.cpp parser_config.cpp parser.cpp
-parser_pos_provider.cpp)
+scanner.cpp parse_table.cpp parser_config.cpp parser.cpp
+parser_pos_provider.cpp builtin_cmds.cpp builtin_tactic_cmds.cpp)
 
 target_link_libraries(lean_frontend ${LEAN_LIBS})
diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
new file mode 100644
index 000000000..695932d48
--- /dev/null
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -0,0 +1,14 @@
+/*
+Copyright (c) 2014 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"
+
+namespace lean {
+cmd_table get_builtin_cmds() {
+    return cmd_table();
+}
+}
+
diff --git a/src/frontends/lean/builtin_cmds.h b/src/frontends/lean/builtin_cmds.h
new file mode 100644
index 000000000..fc64d3b18
--- /dev/null
+++ b/src/frontends/lean/builtin_cmds.h
@@ -0,0 +1,11 @@
+/*
+Copyright (c) 2014 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/cmd_table.h"
+namespace lean {
+cmd_table get_builtin_cmds();
+}
diff --git a/src/frontends/lean/cmd_table.cpp b/src/frontends/lean/builtin_tactic_cmds.cpp
similarity index 66%
rename from src/frontends/lean/cmd_table.cpp
rename to src/frontends/lean/builtin_tactic_cmds.cpp
index 9d8f94e6b..763b2e5a4 100644
--- a/src/frontends/lean/cmd_table.cpp
+++ b/src/frontends/lean/builtin_tactic_cmds.cpp
@@ -4,16 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include "frontends/lean/cmd_table.h"
+#include "frontends/lean/parser.h"
 
 namespace lean {
-cmd_table get_builtin_cmds() {
-    // TODO(Leo)
-    return cmd_table();
-}
-
 tactic_cmd_table get_builtin_tactic_cmds() {
-    // TODO(Leo)
     return tactic_cmd_table();
 }
 }
diff --git a/src/frontends/lean/builtin_tactic_cmds.h b/src/frontends/lean/builtin_tactic_cmds.h
new file mode 100644
index 000000000..3b82d2926
--- /dev/null
+++ b/src/frontends/lean/builtin_tactic_cmds.h
@@ -0,0 +1,11 @@
+/*
+Copyright (c) 2014 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/cmd_table.h"
+namespace lean {
+tactic_cmd_table get_builtin_tactic_cmds();
+}
diff --git a/src/frontends/lean/cmd_table.h b/src/frontends/lean/cmd_table.h
index 18204326c..0fb6b45f2 100644
--- a/src/frontends/lean/cmd_table.h
+++ b/src/frontends/lean/cmd_table.h
@@ -11,24 +11,10 @@ Author: Leonardo de Moura
 
 namespace lean {
 class tactic {};  // TODO(Leo): remove after tactic framework is ported to Lean 0.2
-
 class parser;
 
 typedef std::function<environment(parser&)> command_fn;
-void register_builtin_cmd(char const * name, char const * descr, command_fn const & fn);
-
 typedef std::function<tactic(parser&)> tactic_command_fn;
-void register_builtin_cmd(char const * name, char const * descr, tactic_command_fn const & fn);
-
-template<typename F>
-struct register_builtin_cmd_tmpl {
-    register_builtin_cmd_tmpl(char const * name, char const * descr, F const & fn) {
-        register_builtin_cmd(name, descr, fn);
-    }
-};
-
-typedef register_builtin_cmd_tmpl<command_fn>        register_builtin_cmd_fn;
-typedef register_builtin_cmd_tmpl<tactic_command_fn> register_builtin_tactic_fn;
 
 template<typename F>
 struct cmd_info_tmpl {
@@ -49,7 +35,4 @@ typedef cmd_info_tmpl<tactic_command_fn> tactic_cmd_info;
 
 typedef rb_map<name, cmd_info,        name_quick_cmp> cmd_table;
 typedef rb_map<name, tactic_cmd_info, name_quick_cmp> tactic_cmd_table;
-
-cmd_table        get_builtin_cmds();
-tactic_cmd_table get_builtin_tactic_cmds();
 }
diff --git a/src/frontends/lean/parser_config.cpp b/src/frontends/lean/parser_config.cpp
index b4f839f52..0532f13fc 100644
--- a/src/frontends/lean/parser_config.cpp
+++ b/src/frontends/lean/parser_config.cpp
@@ -5,6 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "frontends/lean/parser_config.h"
+#include "frontends/lean/builtin_cmds.h"
+#include "frontends/lean/builtin_tactic_cmds.h"
 
 namespace lean {
 parser_config::parser_config() {