From 45163acf25eeed4fdf5ee375eda2335fffc0ee1a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 24 Aug 2015 12:09:46 -0700
Subject: [PATCH] refactor(kernel/inductive): use local constants to represent
 introduction rules

---
 src/frontends/lean/inductive_cmd.cpp | 10 ++++++----
 src/frontends/lean/structure_cmd.cpp |  2 +-
 src/kernel/inductive/inductive.h     |  8 ++++----
 src/library/kernel_bindings.cpp      |  4 ++--
 src/library/kernel_serializer.cpp    |  2 +-
 src/library/level_names.cpp          |  3 ++-
 6 files changed, 16 insertions(+), 13 deletions(-)

diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp
index f5c42820c..0ab1c0322 100644
--- a/src/frontends/lean/inductive_cmd.cpp
+++ b/src/frontends/lean/inductive_cmd.cpp
@@ -40,6 +40,7 @@ using inductive::inductive_decl;
 using inductive::inductive_decl_name;
 using inductive::inductive_decl_type;
 using inductive::inductive_decl_intros;
+using inductive::mk_intro_rule;
 using inductive::intro_rule_name;
 using inductive::intro_rule_type;
 
@@ -52,7 +53,7 @@ inductive_decl update_inductive_decl(inductive_decl const & d, buffer<intro_rule
 }
 
 intro_rule update_intro_rule(intro_rule const & r, expr const & t) {
-    return intro_rule(intro_rule_name(r), t);
+    return mk_intro_rule(intro_rule_name(r), t);
 }
 
 static name * g_tmp_prefix  = nullptr;
@@ -255,10 +256,10 @@ struct inductive_cmd_fn {
             if (!m_params.empty() || m_p.curr_is_token(get_colon_tk())) {
                 m_p.check_token_next(get_colon_tk(), "invalid introduction rule, ':' expected");
                 expr intro_type = m_p.parse_expr();
-                intros.push_back(intro_rule(intro_name, intro_type));
+                intros.push_back(mk_intro_rule(intro_name, intro_type));
             } else {
                 expr intro_type = mk_constant(ind_name);
-                intros.push_back(intro_rule(intro_name, intro_type));
+                intros.push_back(mk_intro_rule(intro_name, intro_type));
             }
             if (!curr_is_intro_prefix())
                 break;
@@ -794,7 +795,8 @@ struct inductive_cmd_fn {
             out << "inductive " << d_name << " : " << d_type << "\n";
             for (auto const & ir : d_irules) {
                 name ir_name; expr ir_type;
-                std::tie(ir_name, ir_type) = ir;
+                ir_name = intro_rule_name(ir);
+                ir_type = intro_rule_type(ir);
                 out << "  | " << ir_name << " : " << ir_type << "\n";
             }
         }
diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp
index 1a9dfb019..756271480 100644
--- a/src/frontends/lean/structure_cmd.cpp
+++ b/src/frontends/lean/structure_cmd.cpp
@@ -680,7 +680,7 @@ struct structure_cmd_fn {
         expr intro_type     = mk_intro_type();
 
         level_param_names lnames = to_list(m_level_names.begin(), m_level_names.end());
-        inductive::intro_rule intro(m_mk, intro_type);
+        inductive::intro_rule intro = inductive::mk_intro_rule(m_mk, intro_type);
         inductive::inductive_decl  decl(m_name, structure_type, to_list(intro));
         m_env = module::add_inductive(m_env, lnames, m_params.size(), to_list(decl));
         save_info(m_name, "structure", m_name_pos);
diff --git a/src/kernel/inductive/inductive.h b/src/kernel/inductive/inductive.h
index 8cbf9f65d..6429b80a5 100644
--- a/src/kernel/inductive/inductive.h
+++ b/src/kernel/inductive/inductive.h
@@ -25,10 +25,10 @@ public:
 };
 
 /** \brief Introduction rule */
-typedef pair<name, expr> intro_rule;
-
-inline name const & intro_rule_name(intro_rule const & r) { return r.first; }
-inline expr const & intro_rule_type(intro_rule const & r) { return r.second; }
+typedef expr intro_rule;
+inline intro_rule mk_intro_rule(name const & n, expr const & t) { return mk_local(n, t); }
+inline name const & intro_rule_name(intro_rule const & r) { return mlocal_name(r); }
+inline expr const & intro_rule_type(intro_rule const & r) { return mlocal_type(r); }
 
 /** \brief Inductive datatype */
 typedef std::tuple<name,                // datatype name
diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp
index f5b1603ee..4e892d6f5 100644
--- a/src/library/kernel_bindings.cpp
+++ b/src/library/kernel_bindings.cpp
@@ -1878,7 +1878,7 @@ static int add_inductive1(lua_State * L) {
     int nargs = lua_gettop(L);
     buffer<intro_rule> irules;
     for (int i = idx+1; i <= nargs; i+=2)
-        irules.push_back(intro_rule(to_name_ext(L, i), to_expr(L, i+1)));
+        irules.push_back(mk_intro_rule(to_name_ext(L, i), to_expr(L, i+1)));
     return push_environment(L, module::add_inductive(env, Iname, ls, num_params, Itype, to_list(irules.begin(), irules.end())));
 }
 static int add_inductivek(lua_State * L) {
@@ -1904,7 +1904,7 @@ static int add_inductivek(lua_State * L) {
         for (int i = 3; i <= decl_sz; i+=2) {
             lua_rawgeti(L, idx, i);
             lua_rawgeti(L, idx, i+1);
-            irules.push_back(intro_rule(to_name_ext(L, -2), to_expr(L, -1)));
+            irules.push_back(mk_intro_rule(to_name_ext(L, -2), to_expr(L, -1)));
             lua_pop(L, 2);
         }
         decls.push_back(inductive_decl(Iname, Itype, to_list(irules.begin(), irules.end())));
diff --git a/src/library/kernel_serializer.cpp b/src/library/kernel_serializer.cpp
index c64e0386e..d51b045d3 100644
--- a/src/library/kernel_serializer.cpp
+++ b/src/library/kernel_serializer.cpp
@@ -352,7 +352,7 @@ inductive_decl read_inductive_decl(deserializer & d) {
     for (unsigned j = 0; j < num_intros; j++) {
         name r_name = read_name(d);
         expr r_type = read_expr(d);
-        rules.push_back(intro_rule(r_name, r_type));
+        rules.push_back(inductive::mk_intro_rule(r_name, r_type));
     }
     return inductive_decl(d_name, d_type, to_list(rules.begin(), rules.end()));
 }
diff --git a/src/library/level_names.cpp b/src/library/level_names.cpp
index 36a96c17c..348397c42 100644
--- a/src/library/level_names.cpp
+++ b/src/library/level_names.cpp
@@ -113,6 +113,7 @@ using inductive::inductive_decl_name;
 using inductive::inductive_decl_type;
 using inductive::inductive_decl_intros;
 using inductive::intro_rule;
+using inductive::mk_intro_rule;
 using inductive::intro_rule_name;
 using inductive::intro_rule_type;
 
@@ -135,7 +136,7 @@ pair<level_param_names, list<inductive_decl>> sanitize_level_params(level_param_
         buffer<intro_rule> new_rules;
         for (auto const & r : inductive_decl_intros(d)) {
             expr new_type = rename_param_levels(intro_rule_type(r), param_name_map);
-            new_rules.push_back(intro_rule(intro_rule_name(r), new_type));
+            new_rules.push_back(mk_intro_rule(intro_rule_name(r), new_type));
         }
         new_decls.push_back(inductive_decl(inductive_decl_name(d),
                                            new_type,