From c5dfe7f86e714fa4d892cdf708987df2fb46f4ef Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 19 Dec 2018 14:48:33 +0100
Subject: [PATCH] refactor(frontends/lean/decl_cmds): factor out and expose
 elaboration of variables and constants

---
 src/frontends/lean/decl_cmds.cpp | 35 ++++++++++++++++++--------------
 src/frontends/lean/decl_cmds.h   |  5 +++++
 2 files changed, 25 insertions(+), 15 deletions(-)

diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index 59c7cd1bbd..9d9221ce1f 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -26,6 +26,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/structure_cmd.h"
 #include "frontends/lean/definition_cmds.h"
 #include "frontends/lean/inductive_cmds.h"
+#include "frontends/lean/decl_cmds.h"
 
 namespace lean {
 // TODO(Leo): delete
@@ -73,8 +74,6 @@ static environment universes_cmd(parser & p) {
     return universes_cmd_core(p, true);
 }
 
-enum class variable_kind { Constant, Variable, Axiom };
-
 static environment declare_var(parser & p, environment env,
                                name const & n, names const & ls, expr const & type,
                                variable_kind k, optional<binder_info> const & _bi, pos_info const & pos,
@@ -172,6 +171,23 @@ public:
     }
 };
 
+environment elab_var(parser & p, variable_kind const & k, cmd_meta const & meta, pos_info const & pos,
+                     optional<binder_info> const & bi, name const & n, expr type, buffer<name> & ls_buffer) {
+    names ls;
+    if (ls_buffer.empty()) {
+        ls = to_names(collect_univ_params(type));
+    } else {
+        update_univ_parameters(p, ls_buffer, collect_univ_params(type));
+        ls = names(ls_buffer);
+    }
+    names new_ls;
+    list<expr> ctx = p.locals_to_context();
+    std::tie(type, new_ls) = p.elaborate_type("_variable", ctx, type);
+    if (k == variable_kind::Variable)
+        update_local_levels(p, new_ls, k == variable_kind::Variable);
+    return declare_var(p, p.env(), n, append(ls, new_ls), type, k, bi, pos, meta);
+}
+
 static environment variable_cmd_core(parser & p, variable_kind k, cmd_meta const & meta) {
     check_variable_kind(p, k);
     auto pos = p.pos();
@@ -255,19 +271,8 @@ static environment variable_cmd_core(parser & p, variable_kind k, cmd_meta const
     }
     p.parse_close_binder_info(bi);
     check_command_period_docstring_or_eof(p);
-    names ls;
-    if (ls_buffer.empty()) {
-        ls = to_names(collect_univ_params(type));
-    } else {
-        update_univ_parameters(p, ls_buffer, collect_univ_params(type));
-        ls = names(ls_buffer);
-    }
-    names new_ls;
-    list<expr> ctx = p.locals_to_context();
-    std::tie(type, new_ls) = p.elaborate_type("_variable", ctx, type);
-    if (k == variable_kind::Variable)
-        update_local_levels(p, new_ls, k == variable_kind::Variable);
-    return declare_var(p, p.env(), n, append(ls, new_ls), type, k, bi, pos, meta);
+    return elab_var(p, k, meta, pos, bi, n,
+                    type, ls_buffer);
 }
 static environment variable_cmd(parser & p, cmd_meta const & meta) {
     return variable_cmd_core(p, variable_kind::Variable, meta);
diff --git a/src/frontends/lean/decl_cmds.h b/src/frontends/lean/decl_cmds.h
index 76d2d7d325..c0b0865f54 100644
--- a/src/frontends/lean/decl_cmds.h
+++ b/src/frontends/lean/decl_cmds.h
@@ -22,6 +22,11 @@ bool parse_univ_params(parser & p, buffer<name> & ps);
     Then sort \c ls_buffer (using the order in which the universe levels were declared). */
 void update_univ_parameters(buffer<name> & ls_buffer, name_set const & found_ls, parser const & p);
 
+enum class variable_kind { Constant, Variable, Axiom };
+
+environment elab_var(parser & p, variable_kind const & k, cmd_meta const & meta, pos_info const & pos,
+                     optional <binder_info> const & bi, name const & n, expr type, buffer <name> & ls_buffer);
+
 /** \brief Parse a local attribute command */
 environment local_attribute_cmd(parser & p);
 void register_decl_cmds(cmd_table & r);