From 14d6b6d043d88982cb668ab5b13bc5be62acd327 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 15 Aug 2014 18:02:41 -0700
Subject: [PATCH] fix(frontends/lean/inductive_cmd): generate index for
 inductive decls, introduction rules, and recursor/eliminator

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/inductive_cmd.cpp | 21 ++++++++++++++++-----
 1 file changed, 16 insertions(+), 5 deletions(-)

diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp
index 75986c56d..f8b41bb41 100644
--- a/src/frontends/lean/inductive_cmd.cpp
+++ b/src/frontends/lean/inductive_cmd.cpp
@@ -85,16 +85,27 @@ struct inductive_cmd_fn {
     [[ noreturn ]] void throw_error(char const * error_msg) { throw parser_error(error_msg, m_pos); }
     [[ noreturn ]] void throw_error(sstream const & strm) { throw parser_error(strm, m_pos); }
 
+    name mk_rec_name(name const & n) {
+        return n.append_after("_rec");
+    }
+
     /** \brief Parse the name of an inductive datatype or introduction rule,
         prefix the current namespace to it and return it.
     */
-    name parse_decl_name() {
+    name parse_decl_name(bool is_intro) {
         m_pos   = m_p.pos();
         name id = m_p.check_id_next("invalid declaration, identifier expected");
         check_atomic(id);
-        return m_namespace + id;
+        name full_id = m_namespace + id;
+        m_p.add_decl_index(full_id, m_pos);
+        if (!is_intro)
+            m_p.add_decl_index(mk_rec_name(full_id), m_pos);
+        return full_id;
     }
 
+    name parse_inductive_decl_name() { return parse_decl_name(false); }
+    name parse_intro_decl_name() { return parse_decl_name(true); }
+
     /** \brief Parse inductive declaration universe parameters.
         If this is the first declaration in a mutually recursive block, then this method
         stores the levels in m_explict_levels, and set m_using_explicit_levels to true (iff they were provided).
@@ -249,7 +260,7 @@ struct inductive_cmd_fn {
         buffer<intro_rule> intros;
         while (m_p.curr_is_token(g_bar)) {
             m_p.next();
-            name intro_name = parse_decl_name();
+            name intro_name = parse_intro_decl_name();
             bool strict = true;
             if (m_p.curr_is_token(g_lcurly)) {
                 m_p.next();
@@ -271,7 +282,7 @@ struct inductive_cmd_fn {
         optional<level_param_names> first_d_lvls;
         while (true) {
             parser::local_scope l_scope(m_p);
-            name d_name = parse_decl_name();
+            name d_name = parse_inductive_decl_name();
             parse_inductive_univ_params();
             expr d_type = parse_datatype_type();
             bool empty_type = true;
@@ -505,7 +516,7 @@ struct inductive_cmd_fn {
             name d_name = inductive_decl_name(d);
             name d_short_name(d_name.get_string());
             env = create_alias(env, d_name, section_levels, section_params);
-            env = create_alias(env, d_name.append_after("_rec"), section_levels, section_params);
+            env = create_alias(env, mk_rec_name(d_name), section_levels, section_params);
             for (intro_rule const & ir : inductive_decl_intros(d)) {
                 name ir_name = intro_rule_name(ir);
                 env = create_alias(env, ir_name, section_levels, section_params);