From 019f40c48c24e8a2bc74a63ea2e3dffe66b65a72 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 10 Sep 2016 14:13:30 -0700
Subject: [PATCH] feat(frontends/lean/decl_util): avoid `_main` in nested
 auxiliary declarations

---
 src/frontends/lean/decl_util.cpp           | 15 +++++++++++++--
 tests/lean/aux_decl_zeta.lean.expected.out |  2 +-
 tests/lean/run/lift_nested_rec.lean        |  2 +-
 3 files changed, 15 insertions(+), 4 deletions(-)

diff --git a/src/frontends/lean/decl_util.cpp b/src/frontends/lean/decl_util.cpp
index 6908b94a3a..0d7ddbb2b8 100644
--- a/src/frontends/lean/decl_util.cpp
+++ b/src/frontends/lean/decl_util.cpp
@@ -326,11 +326,22 @@ equations_header mk_equations_header(name const & n) {
     return mk_equations_header(to_list(n));
 }
 
+/* Auxiliary function for creating names for auxiliary declarations.
+   We avoid propagating the suffix `_main` used by the top-level equations
+   to the nested declarations. */
+static name mk_decl_name(name const & prefix, name const & n) {
+    if (!prefix.is_atomic() && prefix.is_string() && strcmp(prefix.get_string(), "_main") == 0) {
+        return prefix.get_prefix() + n;
+    } else {
+        return prefix + n;
+    }
+}
+
 declaration_name_scope::declaration_name_scope(name const & n) {
     definition_info & info = get_definition_info();
     m_old_prefix          = info.m_prefix;
     m_old_next_match_idx  = info.m_next_match_idx;
-    info.m_prefix         = info.m_prefix + n;
+    info.m_prefix         = mk_decl_name(info.m_prefix, n);
     info.m_next_match_idx = 1;
     m_name                = info.m_prefix;
 }
@@ -343,7 +354,7 @@ declaration_name_scope::~declaration_name_scope() {
 
 match_definition_scope::match_definition_scope() {
     definition_info & info = get_definition_info();
-    m_name = info.m_prefix + name("_match").append_after(info.m_next_match_idx);
+    m_name = mk_decl_name(info.m_prefix, name("_match").append_after(info.m_next_match_idx));
     info.m_next_match_idx++;
 }
 }
diff --git a/tests/lean/aux_decl_zeta.lean.expected.out b/tests/lean/aux_decl_zeta.lean.expected.out
index 52d6e1b6e7..63a9e3f3ee 100644
--- a/tests/lean/aux_decl_zeta.lean.expected.out
+++ b/tests/lean/aux_decl_zeta.lean.expected.out
@@ -1,4 +1,4 @@
-aux_decl_zeta.lean:7:0: error: equation compiler failed to create auxiliary declaration 'f._main._match_1', auxiliary declaration has references to let-declarations (possible solution: use 'set_option eqn_compiler.zeta true')
+aux_decl_zeta.lean:7:0: error: equation compiler failed to create auxiliary declaration 'f._match_1', auxiliary declaration has references to let-declarations (possible solution: use 'set_option eqn_compiler.zeta true')
 nested exception message:
 type mismatch at application
   x = w
diff --git a/tests/lean/run/lift_nested_rec.lean b/tests/lean/run/lift_nested_rec.lean
index 91261e11af..ea2b61d6bf 100644
--- a/tests/lean/run/lift_nested_rec.lean
+++ b/tests/lean/run/lift_nested_rec.lean
@@ -9,4 +9,4 @@ definition f : nat → (nat × nat) → nat
 
 check @f._main.equations.eqn_1
 check @f._main.equations.eqn_2
-check @f._main._match_1.equations.eqn_1
+check @f._match_1.equations.eqn_1