fix(library/scope): make sure the local universe names do not conflict with universe parameter names when close a section, add declaration parameter name sanitizers

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/library/CMakeLists.txt

@@ -2,7 +2,7 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp
   kernel_bindings.cpp io_state_stream.cpp bin_app.cpp
   resolve_macro.cpp kernel_serializer.cpp max_sharing.cpp
   normalize.cpp shared_environment.cpp module.cpp coercion.cpp
-  private.cpp placeholder.cpp aliases.cpp scope.cpp
+  private.cpp placeholder.cpp aliases.cpp scope.cpp level_names.cpp
   update_declaration.cpp)
 # fo_unify.cpp hop_match.cpp)
 

src/library/level_names.cpp

@@ -0,0 +1,146 @@
+/*
+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 <utility>
+#include "util/name_set.h"
+#include "util/name_map.h"
+#include "util/list_fn.h"
+#include "kernel/declaration.h"
+#include "kernel/for_each_fn.h"
+#include "kernel/replace_fn.h"
+#include "kernel/inductive/inductive.h"
+#include "library/update_declaration.h"
+
+namespace lean {
+// Collect all universe global levels occurring in l into ls
+static void collect_global_levels(level const & l, name_set & ls) {
+    for_each(l, [&](level const & l) {
+            if (is_global(l))
+                ls.insert(global_id(l));
+            return true;
+        });
+}
+
+// Collect all universe global levels occurring in e into ls
+static void collect_global_levels(expr const & e, name_set & ls) {
+    for_each(e, [&](expr const & e, unsigned) {
+            if (is_constant(e)) {
+                for_each(const_levels(e), [&](level const & l) { collect_global_levels(l, ls); });
+            } else if (is_sort(e)) {
+                collect_global_levels(sort_level(e), ls);
+            }
+            return true;
+        });
+}
+
+// Return a new ls s.t. there is no conflict between the names in ls and globals.
+// Store the mapping between old and new names in param_name_map.
+static level_param_names sanitize_level_params(level_param_names const & ls, name_set const & globals,
+                                               name_map<name> & param_name_map) {
+    buffer<name> new_params;
+    for (name const & n : ls) {
+        if (globals.contains(n)) {
+            unsigned i = 1;
+            name new_n = n.append_after(i);
+            while (globals.contains(new_n)) {
+                i++;
+                name new_n = n.append_after(i);
+            }
+            param_name_map.insert(n, new_n);
+            new_params.push_back(new_n);
+        } else {
+            new_params.push_back(n);
+        }
+    }
+    if (param_name_map.empty())
+        return ls;
+    return to_list(new_params.begin(), new_params.end());
+}
+
+// Rename universe parameters occurring in l using the given mapping
+static level rename_param_levels(level const & l, name_map<name> const & param_name_map) {
+    return replace(l, [&](level const & l) {
+            if (is_param(l)) {
+                if (auto it = param_name_map.find(param_id(l))) {
+                    return some_level(mk_param_univ(*it));
+                }
+            }
+            return none_level();
+        });
+}
+
+static levels rename_param_levels(levels const & ls, name_map<name> const & param_name_map) {
+    return map(ls, [&](level const & l) { return rename_param_levels(l, param_name_map); });
+}
+
+// Rename universe parameters occurring in e using the given mapping
+static expr rename_param_levels(expr const & e, name_map<name> const & param_name_map) {
+    return replace(e, [&](expr const & e, unsigned) {
+            if (is_constant(e))
+                return some_expr(update_constant(e, rename_param_levels(const_levels(e), param_name_map)));
+            else if (is_sort(e))
+                return some_expr(update_sort(e, rename_param_levels(sort_level(e), param_name_map)));
+            else
+                return none_expr();
+        });
+}
+
+declaration sanitize_level_params(declaration const & d) {
+    name_set globals;
+    collect_global_levels(d.get_type(), globals);
+    if (d.is_definition())
+        collect_global_levels(d.get_value(), globals);
+    if (globals.empty())
+        return d;
+    name_map<name> param_name_map;
+    level_param_names new_ls = sanitize_level_params(d.get_params(), globals, param_name_map);
+    if (param_name_map.empty())
+        return d;
+    expr new_type = rename_param_levels(d.get_type(), param_name_map);
+    if (d.is_var_decl()) {
+        return update_declaration(d, new_ls, new_type);
+    } else {
+        expr new_value = rename_param_levels(d.get_value(), param_name_map);
+        return update_declaration(d, new_ls, new_type, new_value);
+    }
+}
+
+using inductive::inductive_decl;
+using inductive::inductive_decl_name;
+using inductive::inductive_decl_type;
+using inductive::inductive_decl_intros;
+using inductive::intro_rule;
+using inductive::intro_rule_name;
+using inductive::intro_rule_type;
+
+std::pair<level_param_names, list<inductive_decl>> sanitize_level_params(level_param_names const & ls, list<inductive_decl> const & decls) {
+    name_set globals;
+    for (auto const & d : decls) {
+        collect_global_levels(inductive_decl_type(d), globals);
+        for (auto const & r : inductive_decl_intros(d))
+            collect_global_levels(intro_rule_type(r), globals);
+    }
+    if (globals.empty())
+        return mk_pair(ls, decls);
+    name_map<name> param_name_map;
+    level_param_names new_ls = sanitize_level_params(ls, globals, param_name_map);
+    if (param_name_map.empty())
+        return mk_pair(ls, decls);
+    buffer<inductive_decl> new_decls;
+    for (auto const & d : decls) {
+        expr new_type = rename_param_levels(inductive_decl_type(d), param_name_map);
+        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_decls.push_back(inductive_decl(inductive_decl_name(d),
+                                           new_type,
+                                           to_list(new_rules.begin(), new_rules.end())));
+    }
+    return mk_pair(new_ls, to_list(new_decls.begin(), new_decls.end()));
+}
+}

src/library/level_names.h

@@ -0,0 +1,23 @@
+/*
+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 <utility>
+#include "kernel/declaration.h"
+#include "kernel/inductive/inductive.h"
+namespace lean {
+/**
+    \brief Return a declaration equivalent to \c d, but where level parameter names
+    do not conflict with global parameter names also used in \c d.
+*/
+declaration sanitize_level_params(declaration const & d);
+/**
+   \brief Return new level parameters and inductive decls equivalent to \c decls,
+   but where level parameter names do not conflict with global parameter names also used in \c decls.
+*/
+std::pair<level_param_names, list<inductive::inductive_decl>> sanitize_level_params(level_param_names const & ls,
+                                                                                    list<inductive::inductive_decl> const & decls);
+}

src/library/scope.cpp

@@ -17,6 +17,7 @@ Author: Leonardo de Moura
 #include "library/scope.h"
 #include "library/module.h"
 #include "library/update_declaration.h"
+#include "library/level_names.h"
 
 namespace lean {
 namespace scope {
@@ -172,8 +173,9 @@ public:
         m_next_local_pos++;
     }
 
-    void add_definition(declaration const & d) {
+    void add_definition(declaration d) {
         lean_assert(d.is_definition());
+        d = sanitize_level_params(d);
         expr new_type  = convert(d.get_type());
         expr new_value = convert(d.get_value());
         level_param_names level_deps = mk_level_deps();
@@ -323,8 +325,11 @@ environment add_inductive(environment                  env,
         environment new_env = inductive::add_inductive(env, level_params, num_params, decls);
         return add(new_env, [=](abstraction_context & ctx) {
                 // abstract types
+                auto new_ls_decls   = sanitize_level_params(level_params, decls);
+                auto s_level_params = new_ls_decls.first;
+                auto s_decls        = new_ls_decls.second;
                 buffer<inductive_decl> tmp_decls;
-                for (auto const & d : decls) {
+                for (auto const & d : s_decls) {
                     expr new_type = ctx.convert(inductive_decl_type(d));
                     buffer<intro_rule> new_rules;
                     for (auto const & r : inductive_decl_intros(d)) {
@@ -340,7 +345,7 @@ environment add_inductive(environment                  env,
                 levels extra_lvls          = map2<level>(extra_ls, [](name const & n) { return mk_param_univ(n); });
                 dependencies extra_ps      = ctx.mk_var_deps();
                 unsigned new_num_params    = num_params + extra_ps.size();
-                level_param_names new_ls   = append(extra_ls, level_params);
+                level_param_names new_ls   = append(extra_ls, s_level_params);
                 // create Pi(extra_ps, T) where T are the types in the declarations
                 buffer<inductive_decl> new_decls;
                 for (auto const & d : tmp_decls) {
@@ -348,7 +353,7 @@ environment add_inductive(environment                  env,
                     ctx.add_decl_info(inductive_decl_name(d), extra_ls, extra_ps, new_type);
                     buffer<intro_rule> new_rules;
                     for (auto const & r : inductive_decl_intros(d)) {
-                        expr new_rule_type = update_inductive_types(intro_rule_type(r), num_params, decls,
+                        expr new_rule_type = update_inductive_types(intro_rule_type(r), num_params, s_decls,
                                                                     extra_lvls, extra_ps);
                         new_rule_type = ctx.Pi(new_rule_type, extra_ps);
                         new_rules.push_back(intro_rule(intro_rule_name(r), new_rule_type));

tests/lua/sect10.lua

@@ -0,0 +1,34 @@
+local env = environment()
+env = env:begin_section_scope()
+env = env:begin_section_scope()
+local nat      = Const("nat")
+env = add_inductive(env,
+                    "nat", Type,
+                    "zero", nat,
+                    "succ", mk_arrow(nat, nat))
+local zero     = Const("zero")
+local succ     = Const("succ")
+local one      = succ(zero)
+env = env:add_global_level("l")
+local l = mk_global_univ("l")
+env = env:add(check(env, mk_var_decl("A", mk_sort(l))), binder_info(true))
+env = env:add(check(env, mk_var_decl("B", mk_sort(l))), binder_info(true))
+local A = Const("A")
+local l1 = mk_param_univ("l")
+local D = Const("D", {l1})
+local n = Local("n", nat)
+env = add_inductive(env,
+                    "D", {l1}, 1, mk_arrow(nat, nat, mk_sort(max_univ(l1, l, 1))),
+                    "mk1", Pi(n, mk_arrow(A, D(n, one))),
+                    "mk0", Pi(n, mk_arrow(A, A, D(n, zero))))
+print(env:find("D_rec"):type())
+env = env:end_scope()
+env = env:end_scope()
+print(env:find("D_rec"):type())
+
+local l  = mk_param_univ("l")
+local A  = Local("A", mk_sort(l))
+local l1 = mk_param_univ("l_1")
+local D  = Const("D", {l, l1})
+print(env:find("mk1"):type())
+assert(env:find("mk1"):type() == Pi({A, n}, mk_arrow(A, D(A, n, one))))

tests/lua/sect1c.lua

@@ -0,0 +1,13 @@
+local env = environment()
+env = env:begin_section_scope()
+env = env:add_global_level("l")
+local l  = mk_global_univ("l")
+local l1 = mk_param_univ("l")
+env = add_decl(env, mk_definition("A", {l1}, mk_sort(max_univ(l, l1)+1), mk_sort(max_univ(l, l1))))
+env = env:end_scope()
+print (env:find("A"):type())
+local ls = env:find("A"):univ_params()
+assert(#ls == 2)
+print(ls:head())
+assert(ls:head() == name("l"))
+assert(ls:tail():head() == name("l_1"))